awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
oneltm : 1 < m
s : ℝ := logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hs : s = logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
n : ℕ
h : n < 1
inl :
  ∀ (h : LT.lt (α := ℕ) 0 1), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑0 : ℚ) : ℝ) s⁻¹ = (real : (a : ℚ) → ℝ) (↑0 : ℚ)
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) s⁻¹ = (real : (a : ℚ) → ℝ) (↑n : ℚ)

Tactic:
obtain rfl : n = 0 := by lia

Premises used: rfl
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
oneltm : 1 < m
s : ℝ := logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hs : s = logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
h : LT.lt (α := ℕ) 0 1
simp :
  ¬m = 0 ∧
    ¬m = 1 ∧
      ¬Eq (α := ℝ) (↑m : ℝ) (-1) ∧
        ¬m = 0 ∧
          ¬Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) ∧ ¬Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (-1 : ℝ)
⊢ (logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ)))⁻¹ ≠ 0

Tactic:
simp only [ne_eq, inv_eq_zero, logb_eq_zero, Nat.cast_eq_zero, Nat.cast_eq_one, map_eq_zero,
        not_or]

Premises used: inv_eq_zero, Real.logb_eq_zero, map_eq_zero, ne_eq, not_or, Nat.cast_eq_zero, Nat.cast_eq_one
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
oneltm : 1 < m
s : ℝ := logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hs : s = logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
h : LT.lt (α := ℕ) 0 1
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ¬False
⊢ ¬Eq (α := ℝ) (↑m : ℝ) (-1)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
oneltm : 1 < m
s : ℝ := logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hs : s = logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
h : LT.lt (α := ℕ) 0 1
linarith :
  Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (-1 : ℝ) →
    -1 + HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (-1 : ℝ) +
        HSub.hSub (α := ℝ) (β := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) =
      0
⊢ ¬Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (-1 : ℝ)

Tactic:
linarith only [apply_nonneg f ↑m]

Premises used: NonnegHomClass.apply_nonneg
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
oneltm : 1 < m
s : ℝ := logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hs : s = logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
h : LT.lt (α := ℕ) 0 1
⊢ ¬m = 0 ∧
    ¬m = 1 ∧
      ¬Eq (α := ℝ) (↑m : ℝ) (-1) ∧
        ¬m = 0 ∧
          ¬Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) ∧ ¬Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (-1 : ℝ)

Tactic:
exact ⟨ne_zero_of_lt oneltm, oneltm.ne', by norm_cast,
        ne_zero_of_lt oneltm, ne_of_not_le hm, by linarith only [apply_nonneg f ↑m]⟩
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
oneltm : 1 < m
s : ℝ := logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hs : s = logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
h : LT.lt (α := ℕ) 0 1
⊢ (logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ)))⁻¹ ≠ 0

Tactic:
have : (logb (↑m) (f ↑m))⁻¹ ≠ 0 := by
      simp only [ne_eq, inv_eq_zero, logb_eq_zero, Nat.cast_eq_zero, Nat.cast_eq_one, map_eq_zero,
        not_or]
      exact ⟨ne_zero_of_lt oneltm, oneltm.ne', by norm_cast,
        ne_zero_of_lt oneltm, ne_of_not_le hm, by linarith only [apply_nonneg f ↑m]⟩
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
oneltm : 1 < m
s : ℝ := logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hs : s = logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
h : LT.lt (α := ℕ) 0 1
this : (logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ)))⁻¹ ≠ 0
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑0 : ℚ) : ℝ) s⁻¹ = (real : (a : ℚ) → ℝ) (↑0 : ℚ)

Tactic:
simp [hs, this]
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
oneltm : 1 < m
s : ℝ := logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hs : s = logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑1 : ℚ) : ℝ) s⁻¹ = (real : (a : ℚ) → ℝ) (↑1 : ℚ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
oneltm : 1 < m
s : ℝ := logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hs : s = logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
n : ℕ
h : 1 < n
inr : HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) s⁻¹ = (↑n : ℝ)
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) s⁻¹ = (real : (a : ℚ) → ℝ) (↑n : ℚ)

Tactic:
simp only [real_eq_abs, abs_cast, Rat.cast_natCast]

Premises used: Nat.abs_cast, Rat.cast_natCast, Rat.AbsoluteValue.real_eq_abs
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
oneltm : 1 < m
s : ℝ := logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hs : s = logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
n : ℕ
h : 1 < n
linarith :
  LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (0 : ℝ) →
    -1 + HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (0 : ℝ) +
        HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) =
      0
⊢ LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ)

Tactic:
linarith only [hm]
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
oneltm : 1 < m
s : ℝ := logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hs : s = logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
n : ℕ
h : 1 < n
linarith :
  Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
    HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) +
        HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) =
      0
⊢ Ne (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)

Tactic:
linarith only [hm]
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
oneltm : 1 < m
s : ℝ := logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hs : s = logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
n : ℕ
h : 1 < n
inr : (f : (a : ℚ) → ℝ) (↑n : ℚ) = HPow.hPow (α := ℝ) (↑n : ℝ) (logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ)))
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) s⁻¹ = (↑n : ℝ)

Tactic:
rw [rpow_inv_eq (apply_nonneg f ↑n) (Nat.cast_nonneg n)
      (logb_ne_zero_of_pos_of_ne_one (one_lt_cast.mpr oneltm) (by linarith only [hm])
      (by linarith only [hm]))]

Premises used: Iff.mpr, Nat.cast_nonneg, Real.logb_ne_zero_of_pos_of_ne_one, Nat.one_lt_cast, Real.rpow_inv_eq, NonnegHomClass.apply_nonneg
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
oneltm : 1 < m
s : ℝ := logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hs : s = logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
n : ℕ
h : 1 < n
rw rw₁ : Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ)
⊢ (f : (a : ℚ) → ℝ) (↑m : ℚ) = HPow.hPow (α := ℝ) (↑m : ℝ) s

Tactic:
rw [rpow_logb (mod_cast zero_lt_of_lt oneltm) (mod_cast oneltm.ne') (by linarith only [hm])]

Premises used: Real.rpow_logb
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
oneltm : 1 < m
s : ℝ := logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hs : s = logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
n : ℕ
h : 1 < n
⊢ (f : (a : ℚ) → ℝ) (↑m : ℚ) = HPow.hPow (α := ℝ) (↑m : ℝ) s

Tactic:
have hfm : f m = m ^ s := by
      rw [rpow_logb (mod_cast zero_lt_of_lt oneltm) (mod_cast oneltm.ne') (by linarith only [hm])]
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
oneltm : 1 < m
s : ℝ := logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hs : s = logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
n : ℕ
h : 1 < n
hfm : (f : (a : ℚ) → ℝ) (↑m : ℚ) = HPow.hPow (α := ℝ) (↑m : ℝ) s
hx : Ne (α := ℚ) (↑n : ℚ) 0
⊢ LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ)

Tactic:
apply map_pos_of_ne_zero

Premises used: map_pos_of_ne_zero
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
oneltm : 1 < m
s : ℝ := logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hs : s = logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
n : ℕ
h : 1 < n
hfm : (f : (a : ℚ) → ℝ) (↑m : ℚ) = HPow.hPow (α := ℝ) (↑m : ℝ) s
⊢ Ne (α := ℚ) (↑n : ℚ) 0

Tactic:
exact_mod_cast ne_zero_of_lt h

Premises used: ne_zero_of_lt
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
oneltm : 1 < m
s : ℝ := logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hs : s = logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
n : ℕ
h : 1 < n
hfm : (f : (a : ℚ) → ℝ) (↑m : ℚ) = HPow.hPow (α := ℝ) (↑m : ℝ) s
rw rw₁ : Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ)
⊢ (f : (a : ℚ) → ℝ) (↑n : ℚ) = HPow.hPow (α := ℝ) (↑n : ℝ) (logb (↑n : ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ)))

Tactic:
rw [rpow_logb (mod_cast zero_lt_of_lt h) (mod_cast h.ne')
        (by apply map_pos_of_ne_zero; exact_mod_cast ne_zero_of_lt h)]

Premises used: Real.rpow_logb
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
oneltm : 1 < m
s : ℝ := logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hs : s = logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
n : ℕ
h : 1 < n
hfm : (f : (a : ℚ) → ℝ) (↑m : ℚ) = HPow.hPow (α := ℝ) (↑m : ℝ) s
⊢ (f : (a : ℚ) → ℝ) (↑n : ℚ) = HPow.hPow (α := ℝ) (↑n : ℝ) (logb (↑n : ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ)))

Tactic:
have hfn : f n = n ^ logb n (f n) := by
      rw [rpow_logb (mod_cast zero_lt_of_lt h) (mod_cast h.ne')
        (by apply map_pos_of_ne_zero; exact_mod_cast ne_zero_of_lt h)]
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
oneltm : 1 < m
s : ℝ := logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hs : s = logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
n : ℕ
h : 1 < n
hfm : (f : (a : ℚ) → ℝ) (↑m : ℚ) = HPow.hPow (α := ℝ) (↑m : ℝ) s
hfn : (f : (a : ℚ) → ℝ) (↑n : ℚ) = HPow.hPow (α := ℝ) (↑n : ℝ) (logb (↑n : ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ)))
inr : (f : (a : ℚ) → ℝ) (↑n : ℚ) = HPow.hPow (α := ℝ) (↑n : ℝ) s
inr₁ inr₂ inr₃ inr₄ :
  (f : (a : ℚ) → ℝ) (↑n : ℚ) = HPow.hPow (α := ℝ) (↑n : ℝ) (logb (↑n : ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ)))
⊢ (f : (a : ℚ) → ℝ) (↑n : ℚ) = HPow.hPow (α := ℝ) (↑n : ℝ) (logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ)))

Tactic:
rwa [← hs, eq_of_eq_pow oneltm h notbdd hfm hfn]

Premises used: _private.0.Rat.AbsoluteValue.eq_of_eq_pow
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
pos :
  ∀ (bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)),
    f ≈ real ∨ ∃! p : ℕ, ∃ (x : Fact (Nat.Prime p)), f ≈ padic p
neg :
  ∀ (bdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)),
    f ≈ real ∨ ∃! p : ℕ, ∃ (x : Fact (Nat.Prime p)), f ≈ padic p
⊢ f ≈ real ∨ ∃! p : ℕ, ∃ (x : Fact (Nat.Prime p)), f ≈ padic p

Tactic:
by_cases bdd : ∀ n : ℕ, f n ≤ 1
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
⊢ f ≈ real ∨ ∃! p : ℕ, ∃ (x : Fact (Nat.Prime p)), f ≈ padic p

Tactic:
.inr <| equiv_padic_of_bounded hf_nontriv bdd

Premises used: Rat.AbsoluteValue.equiv_padic_of_bounded, Or.inr
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
⊢ f ≈ real ∨ ∃! p : ℕ, ∃ (x : Fact (Nat.Prime p)), f ≈ padic p

Tactic:
exact .inr <| equiv_padic_of_bounded hf_nontriv bdd

Premises used: Rat.AbsoluteValue.equiv_padic_of_bounded
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
⊢ f ≈ real ∨ ∃! p : ℕ, ∃ (x : Fact (Nat.Prime p)), f ≈ padic p

Tactic:
.inl <| equiv_real_of_unbounded bdd

Premises used: Rat.AbsoluteValue.equiv_real_of_unbounded, Or.inl
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
⊢ f ≈ real ∨ ∃! p : ℕ, ∃ (x : Fact (Nat.Prime p)), f ≈ padic p

Tactic:
exact .inl <| equiv_real_of_unbounded bdd

Premises used: Rat.AbsoluteValue.equiv_real_of_unbounded
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
rw :
  ¬∃ (c : ℝ),
      0 < c ∧
        Eq (α := ℚ → ℝ) (fun (x : ℚ) ↦ HPow.hPow (α := ℝ) ((real : (a : ℚ) → ℝ) x : ℝ) c) (⇑(padic p) : (a : ℚ) → ℝ)
⊢ ¬real.IsEquiv (padic p)

Tactic:
rw [isEquiv_iff_exists_rpow_eq]

Premises used: AbsoluteValue.isEquiv_iff_exists_rpow_eq
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
c : ℝ
hc₀ : 0 < c
hc : Eq (α := ℚ → ℝ) (fun (x : ℚ) ↦ HPow.hPow (α := ℝ) ((real : (a : ℚ) → ℝ) x : ℝ) c) (⇑(padic p) : (a : ℚ) → ℝ)
⊢ Eq (α := ℝ) ((fun (x : ℚ) ↦ HPow.hPow (α := ℝ) ((real : (a : ℚ) → ℝ) x : ℝ) c) 2 : ℝ) ((padic p : (a : ℚ) → ℝ) 2 : ℝ)

Tactic:
apply_fun (· 2) at hc
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
c : ℝ
hc₀ : 0 < c
hc :
  Eq (α := ℝ) ((fun (x : ℚ) ↦ HPow.hPow (α := ℝ) ((real : (a : ℚ) → ℝ) x : ℝ) c) 2 : ℝ) ((padic p : (a : ℚ) → ℝ) 2 : ℝ)
⊢ HPow.hPow (α := ℝ) 2 c = (padic p : (a : ℚ) → ℝ) 2

Tactic:
simp only [real_eq_abs, abs_ofNat, cast_ofNat] at hc

Premises used: Rat.cast_ofNat, Rat.AbsoluteValue.real_eq_abs, Nat.abs_ofNat
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
c : ℝ
hc₀ : 0 < c
hc : HPow.hPow (α := ℝ) 2 c = (padic p : (a : ℚ) → ℝ) 2
⊢ False

Tactic:
((padic_le_one p 2).trans_lt <| one_lt_rpow one_lt_two hc₀).ne' hc

Premises used: LT.lt.ne', Rat.AbsoluteValue.padic_le_one, one_lt_two, OfNat.ofNat, Real.one_lt_rpow, LE.le.trans_lt
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
c : ℝ
hc₀ : 0 < c
hc : HPow.hPow (α := ℝ) 2 c = (padic p : (a : ℚ) → ℝ) 2
⊢ False

Tactic:
exact ((padic_le_one p 2).trans_lt <| one_lt_rpow one_lt_two hc₀).ne' hc

Premises used: LT.lt.ne', Rat.AbsoluteValue.padic_le_one, one_lt_two, OfNat.ofNat, Real.one_lt_rpow, LE.le.trans_lt
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ φ⁻¹ = -ψ

Tactic:
grind
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
rw : -ψ = φ⁻¹
⊢ ψ⁻¹ = -φ

Tactic:
rw [inv_eq_iff_eq_inv, ← neg_inv, ← neg_eq_iff_eq_neg]

Premises used: neg_eq_iff_eq_neg, neg_inv, inv_eq_iff_eq_inv
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ -ψ = φ⁻¹

Tactic:
inv_goldenRatio.symm

Premises used: Real.inv_goldenRatio, Eq.symm
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ -ψ = φ⁻¹

Tactic:
exact inv_goldenRatio.symm

Premises used: Real.inv_goldenRatio, Eq.symm
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ φ * ψ = -1

Tactic:
grind
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
rw : φ * ψ = -1
⊢ ψ * φ = -1

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ φ * ψ = -1

Tactic:
goldenRatio_mul_goldenConj

Premises used: Real.goldenRatio_mul_goldenConj
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ φ * ψ = -1

Tactic:
exact goldenRatio_mul_goldenConj

Premises used: Real.goldenRatio_mul_goldenConj
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ (1 + √5) / 2 + (1 - √5) / 2 = 1

Tactic:
ring
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
linarith : 1 - φ < ψ → 1 - φ - ψ + (φ + ψ - 1) = 0
linarith₁ : ψ < 1 - φ → ψ - (1 - φ) + -(φ + ψ - 1) = 0
⊢ 1 - φ = ψ

Tactic:
linarith [goldenRatio_add_goldenConj]

Premises used: Real.goldenRatio_add_goldenConj
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
linarith : 1 - ψ < φ → 1 - ψ - φ + (φ + ψ - 1) = 0
linarith₁ : φ < 1 - ψ → φ - (1 - ψ) + -(φ + ψ - 1) = 0
⊢ 1 - ψ = φ

Tactic:
linarith [goldenRatio_add_goldenConj]

Premises used: Real.goldenRatio_add_goldenConj
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ φ - ψ = √5

Tactic:
ring
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
n : ℕ
⊢ φ ^ (n + 2) - φ ^ (n + 1) = φ ^ n

Tactic:
grind
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ HPow.hPow (β := ℕ) φ 2 = φ + 1

Tactic:
grind
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ HPow.hPow (β := ℕ) ψ 2 = ψ + 1

Tactic:
grind
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
ha : LT.lt (α := ℝ) 0 1
hb : 0 < √5
⊢ 0 < 1 + √5

Tactic:
apply add_pos

Premises used: add_pos
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ LT.lt (α := ℝ) 0 1

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ 0 < √5

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ φ ≠ 0

Tactic:
ne_of_gt goldenRatio_pos

Premises used: ne_of_gt, Real.goldenRatio_pos
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ 1 < φ

Tactic:
lt_of_mul_lt_mul_left ?_ (le_of_lt goldenRatio_pos)

Premises used: lt_of_mul_lt_mul_left, le_of_lt, Real.goldenRatio_pos
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
refine : φ * 1 < φ * φ
⊢ 1 < φ

Tactic:
refine lt_of_mul_lt_mul_left ?_ (le_of_lt goldenRatio_pos)

Premises used: lt_of_mul_lt_mul_left, le_of_lt, Real.goldenRatio_pos
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ φ * 1 < φ * φ

Tactic:
simp [← sq, zero_lt_one]

Premises used: sq, zero_lt_one
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
h : √5 < 3
⊢ (1 + √5) / 2 < HAdd.hAdd (α := ℝ) 1 3 / 2

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
h : 5 < HPow.hPow (α := ℝ) (β := ℕ) 3 2
h₁ : LT.lt (α := ℝ) 0 3
⊢ √5 < 3

Tactic:
rw [sqrt_lt']

Premises used: Real.sqrt_lt'
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ 5 < HPow.hPow (α := ℝ) (β := ℕ) 3 2

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ LT.lt (α := ℝ) 0 3

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ HAdd.hAdd (α := ℝ) 1 3 / 2 = 2

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
by : (1 + √5) / 2 < HAdd.hAdd (α := ℝ) 1 3 / 2
by₁ : HAdd.hAdd (α := ℝ) 1 3 / 2 = 2
⊢ φ < 2

Tactic:
calc
  (1 + √5) / 2 < (1 + 3) / 2 := by gcongr; rw [sqrt_lt'] <;> norm_num
  _ = 2 := by norm_num

Premises used: HAdd.hAdd, Real.sqrt, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
linarith : 0 ≤ ψ → 0 - ψ + -(1 - φ - ψ) + (1 - φ) = 0
⊢ ψ < 0

Tactic:
linarith [one_sub_goldenConj, one_lt_goldenRatio]

Premises used: Real.one_lt_goldenRatio, Real.one_sub_goldenConj
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ ψ ≠ 0

Tactic:
ne_of_lt goldenConj_neg

Premises used: Real.goldenConj_neg, ne_of_lt
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
rw : φ⁻¹ < 1
⊢ -1 < ψ

Tactic:
rw [neg_lt, ← inv_goldenRatio]

Premises used: Real.inv_goldenRatio, neg_lt
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ φ⁻¹ < 1

Tactic:
inv_lt_one_of_one_lt₀ one_lt_goldenRatio

Premises used: Real.one_lt_goldenRatio, inv_lt_one_of_one_lt₀
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ φ⁻¹ < 1

Tactic:
exact inv_lt_one_of_one_lt₀ one_lt_goldenRatio

Premises used: Real.one_lt_goldenRatio, inv_lt_one_of_one_lt₀
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ Nat.Prime 5

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ Irrational √(↑5 : ℝ)

Tactic:
have := Nat.Prime.irrational_sqrt (show Nat.Prime 5 by norm_num)
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
this : Irrational √(↑5 : ℝ)
⊢ Irrational ((↑1 : ℝ) + √(↑5 : ℝ))

Tactic:
have := this.ratCast_add 1
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
this_1 : Irrational √(↑5 : ℝ)
this : Irrational ((↑1 : ℝ) + √(↑5 : ℝ))
⊢ Ne (α := ℚ) 0.5 0

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
this_1 : Irrational √(↑5 : ℝ)
this : Irrational ((↑1 : ℝ) + √(↑5 : ℝ))
h : φ = (↑0.5 : ℝ) * ((↑1 : ℝ) + √(↑5 : ℝ))
⊢ Irrational φ

Tactic:
convert! this.ratCast_mul (show (0.5 : ℚ) ≠ 0 by norm_num)

Premises used: Irrational.ratCast_mul
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
this_1 : Irrational √(↑5 : ℝ)
this : Irrational ((↑1 : ℝ) + √(↑5 : ℝ))
h : φ = 0.5 * (1 + √5)
⊢ φ = (↑0.5 : ℝ) * ((↑1 : ℝ) + √(↑5 : ℝ))

Tactic:
simp
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
this_1 : Irrational √(↑5 : ℝ)
this : Irrational ((↑1 : ℝ) + √(↑5 : ℝ))
⊢ φ = 0.5 * (1 + √5)

Tactic:
ring
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
this : Irrational √(↑5 : ℝ)
⊢ Irrational ((↑1 : ℝ) - √(↑5 : ℝ))

Tactic:
have := this.ratCast_sub 1
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
this_1 : Irrational √(↑5 : ℝ)
this : Irrational ((↑1 : ℝ) - √(↑5 : ℝ))
⊢ Ne (α := ℚ) 0.5 0

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
this_1 : Irrational √(↑5 : ℝ)
this : Irrational ((↑1 : ℝ) - √(↑5 : ℝ))
h : ψ = (↑0.5 : ℝ) * ((↑1 : ℝ) - √(↑5 : ℝ))
⊢ Irrational ψ

Tactic:
convert! this.ratCast_mul (show (0.5 : ℚ) ≠ 0 by norm_num)

Premises used: Irrational.ratCast_mul
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
this_1 : Irrational √(↑5 : ℝ)
this : Irrational ((↑1 : ℝ) - √(↑5 : ℝ))
h : ψ = 0.5 * (1 - √5)
⊢ ψ = (↑0.5 : ℝ) * ((↑1 : ℝ) - √(↑5 : ℝ))

Tactic:
simp
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
this_1 : Irrational √(↑5 : ℝ)
this : Irrational ((↑1 : ℝ) - √(↑5 : ℝ))
⊢ ψ = 0.5 * (1 - √5)

Tactic:
ring
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
β : Type u_2
inst : CommRing β
rw :
  HSub.hSub (α := β[X])
      ((monomial (LinearRecurrence.order.{u_2} (R := β) { order := 2, coeffs := ![1, 1] : LinearRecurrence β }) :
          (a : β) → β[X])
        1)
      (∑ i : Fin { order := 2, coeffs := ![1, 1] }.order,
        (monomial (↑i : ℕ) : (a : β) → β[X])
          (LinearRecurrence.coeffs { order := 2, coeffs := ![1, 1] : LinearRecurrence β } i)) =
    HPow.hPow (α := β[X]) (β := ℕ) X 2 - HAdd.hAdd (α := β[X]) X 1
⊢ LinearRecurrence.charPoly fibRec = HPow.hPow (α := β[X]) (β := ℕ) X 2 - HAdd.hAdd (α := β[X]) X 1

Tactic:
rw [fibRec, LinearRecurrence.charPoly]

Premises used: LinearRecurrence.charPoly, Real.fibRec