awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℕ
inl : ∀ (h : n < 1), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) s⁻¹ = (real : (a : ℚ) → ℝ) (↑n : ℚ)
inr : HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑1 : ℚ) : ℝ) s⁻¹ = (real : (a : ℚ) → ℝ) (↑1 : ℚ)
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) s⁻¹ = (real : (a : ℚ) → ℝ) (↑n : ℚ)
have inr₁ : ∀ (h : 1 < n), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) s⁻¹ = (real : (a : ℚ) → ℝ) (↑n : ℚ)
Tactic: rcases lt_trichotomy n 1 with h | rfl | h
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) s⁻¹ = (real : (a : ℚ) → ℝ) (↑n : ℚ)
have inl : ∀ (h : LT.lt (α := ℕ) 0 1), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑0 : ℚ) : ℝ) s⁻¹ = (real : (a : ℚ) → ℝ) (↑0 : ℚ)
Tactic: obtain rfl : n = 0 := by lia
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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
have simp : ¬m = 0 ∧
  ¬m = 1 ∧
    ¬Eq (α := ℝ) (↑m : ℝ) (-1) ∧
      ¬m = 0 ∧
        ¬Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) ∧ ¬Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (-1 : ℝ)
Tactic: simp only [ne_eq, inv_eq_zero, logb_eq_zero, Nat.cast_eq_zero, Nat.cast_eq_one, map_eq_zero,
        not_or]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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
⊢ ¬Eq (α := ℝ) (↑m : ℝ) (-1)
have norm_cast : ¬False
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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
⊢ ¬Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (-1 : ℝ)
have linarith : Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (-1 : ℝ) →
  -1 + HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (-1 : ℝ) +
      HSub.hSub (α := ℝ) (β := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) =
    0
Tactic: linarith only [apply_nonneg f ↑m]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (hypothesis)
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
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑0 : ℚ) : ℝ) s⁻¹ = (real : (a : ℚ) → ℝ) (↑0 : ℚ)
have this : (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]⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) s⁻¹ = (real : (a : ℚ) → ℝ) (↑n : ℚ)
have inr : HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) s⁻¹ = (↑n : ℝ)
Tactic: simp only [real_eq_abs, abs_cast, Rat.cast_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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
⊢ LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ)
have linarith : LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (0 : ℝ) →
  -1 + HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (0 : ℝ) +
      HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) =
    0
Tactic: linarith only [hm]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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
⊢ Ne (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
have linarith : Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
  HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) +
      HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) =
    0
Tactic: linarith only [hm]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) s⁻¹ = (↑n : ℝ)
have inr : (f : (a : ℚ) → ℝ) (↑n : ℚ) = HPow.hPow (α := ℝ) (↑n : ℝ) (logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ)))
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]))]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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
have rw : Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ)
Tactic: rw [rpow_logb (mod_cast zero_lt_of_lt oneltm) (mod_cast oneltm.ne') (by linarith only [hm])]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (hypothesis)
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 : ℚ) → ℝ) (↑n : ℚ) = HPow.hPow (α := ℝ) (↑n : ℝ) (logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ)))
have hfm : (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])]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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
⊢ LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ)
have hx : Ne (α := ℚ) (↑n : ℚ) 0
Tactic: apply map_pos_of_ne_zero
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℚ)))
have rw : Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑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)]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (hypothesis)
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 (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ)))
have hfn : (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)]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
⊢ f ≈ real ∨ ∃! p : ℕ, ∃ (x : Fact (Nat.Prime p)), f ≈ padic p
have pos : ∀ (bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)),
  f ≈ real ∨ ∃! p : ℕ, ∃ (x : Fact (Nat.Prime p)), f ≈ padic p
Tactic: by_cases bdd : ∀ n : ℕ, f n ≤ 1
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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
⊢ f ≈ real ∨ ∃! p : ℕ, ∃ (x : Fact (Nat.Prime p)), f ≈ padic p
have neg : ∀ (bdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)),
  f ≈ real ∨ ∃! p : ℕ, ∃ (x : Fact (Nat.Prime p)), f ≈ padic p
Tactic: by_cases bdd : ∀ n : ℕ, f n ≤ 1
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ ¬real.IsEquiv (padic p)
have rw : ¬∃ (c : ℝ),
    0 < c ∧ Eq (α := ℚ → ℝ) (fun (x : ℚ) ↦ HPow.hPow (α := ℝ) ((real : (a : ℚ) → ℝ) x : ℝ) c) (⇑(padic p) : (a : ℚ) → ℝ)
Tactic: rw [isEquiv_iff_exists_rpow_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
c : ℝ
hc₀ : 0 < c
hc : Eq (α := ℚ → ℝ) (fun (x : ℚ) ↦ HPow.hPow (α := ℝ) ((real : (a : ℚ) → ℝ) x : ℝ) c) (⇑(padic p) : (a : ℚ) → ℝ)
⊢ False
have hc₁ : Eq (α := ℝ) ((fun (x : ℚ) ↦ HPow.hPow (α := ℝ) ((real : (a : ℚ) → ℝ) x : ℝ) c) 2 : ℝ) ((padic p : (a : ℚ) → ℝ) 2 : ℝ)
Tactic: apply_fun (· 2) at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (hypothesis)
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 : ℝ)
⊢ False
have hc₁ : HPow.hPow (α := ℝ) 2 c = (padic p : (a : ℚ) → ℝ) 2
Tactic: simp only [real_eq_abs, abs_ofNat, cast_ofNat] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
⊢ ψ⁻¹ = -φ
have rw : -ψ = φ⁻¹
Tactic: rw [inv_eq_iff_eq_inv, ← neg_inv, ← neg_eq_iff_eq_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
⊢ ψ * φ = -1
have rw : φ * ψ = -1
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
⊢ 1 - φ = ψ
have linarith : 1 - φ < ψ → 1 - φ - ψ + (φ + ψ - 1) = 0
Tactic: linarith [goldenRatio_add_goldenConj]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
linarith : 1 - φ < ψ → 1 - φ - ψ + (φ + ψ - 1) = 0
⊢ 1 - φ = ψ
have linarith₁ : ψ < 1 - φ → ψ - (1 - φ) + -(φ + ψ - 1) = 0
Tactic: linarith [goldenRatio_add_goldenConj]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
⊢ 1 - ψ = φ
have linarith : 1 - ψ < φ → 1 - ψ - φ + (φ + ψ - 1) = 0
Tactic: linarith [goldenRatio_add_goldenConj]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
linarith : 1 - ψ < φ → 1 - ψ - φ + (φ + ψ - 1) = 0
⊢ 1 - ψ = φ
have linarith₁ : φ < 1 - ψ → φ - (1 - ψ) + -(φ + ψ - 1) = 0
Tactic: linarith [goldenRatio_add_goldenConj]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
⊢ 0 < 1 + √5
have ha : LT.lt (α := ℝ) 0 1
Tactic: apply add_pos
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
ha : LT.lt (α := ℝ) 0 1
⊢ 0 < 1 + √5
have hb : 0 < √5
Tactic: apply add_pos
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
⊢ 1 < φ
have refine : φ * 1 < φ * φ
Tactic: refine lt_of_mul_lt_mul_left ?_ (le_of_lt goldenRatio_pos)
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
⊢ (1 + √5) / 2 < HAdd.hAdd (α := ℝ) 1 3 / 2
have h : √5 < 3
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
⊢ √5 < 3
have h : 5 < HPow.hPow (α := ℝ) (β := ℕ) 3 2
Tactic: rw [sqrt_lt']
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
h : 5 < HPow.hPow (α := ℝ) (β := ℕ) 3 2
⊢ √5 < 3
have h₁ : LT.lt (α := ℝ) 0 3
Tactic: rw [sqrt_lt']
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
⊢ φ < 2
have by : (1 + √5) / 2 < HAdd.hAdd (α := ℝ) 1 3 / 2
Tactic: calc
  (1 + √5) / 2 < (1 + 3) / 2 := by gcongr; rw [sqrt_lt'] <;> norm_num
  _ = 2 := by norm_num
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
by : (1 + √5) / 2 < HAdd.hAdd (α := ℝ) 1 3 / 2
⊢ φ < 2
have by₁ : HAdd.hAdd (α := ℝ) 1 3 / 2 = 2
Tactic: calc
  (1 + √5) / 2 < (1 + 3) / 2 := by gcongr; rw [sqrt_lt'] <;> norm_num
  _ = 2 := by norm_num
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
⊢ ψ < 0
have linarith : 0 ≤ ψ → 0 - ψ + -(1 - φ - ψ) + (1 - φ) = 0
Tactic: linarith [one_sub_goldenConj, one_lt_goldenRatio]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
⊢ -1 < ψ
have rw : φ⁻¹ < 1
Tactic: rw [neg_lt, ← inv_goldenRatio]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (hypothesis)
Goal:
⊢ Irrational φ
have this : Irrational √(↑5 : ℝ)
Tactic: have := Nat.Prime.irrational_sqrt (show Nat.Prime 5 by norm_num)
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (hypothesis)
Goal:
this : Irrational √(↑5 : ℝ)
⊢ Irrational φ
have this₁ : Irrational ((↑1 : ℝ) + √(↑5 : ℝ))
Tactic: have := this.ratCast_add 1
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
this_1 : Irrational √(↑5 : ℝ)
this : Irrational ((↑1 : ℝ) + √(↑5 : ℝ))
⊢ Irrational φ
have h : φ = (↑0.5 : ℝ) * ((↑1 : ℝ) + √(↑5 : ℝ))
Tactic: convert! this.ratCast_mul (show (0.5 : ℚ) ≠ 0 by norm_num)
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
this_1 : Irrational √(↑5 : ℝ)
this : Irrational ((↑1 : ℝ) + √(↑5 : ℝ))
⊢ φ = (↑0.5 : ℝ) * ((↑1 : ℝ) + √(↑5 : ℝ))
have h : φ = 0.5 * (1 + √5)
Tactic: simp
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (hypothesis)
Goal:
⊢ Irrational ψ
have this : Irrational √(↑5 : ℝ)
Tactic: have := Nat.Prime.irrational_sqrt (show Nat.Prime 5 by norm_num)
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (hypothesis)
Goal:
this : Irrational √(↑5 : ℝ)
⊢ Irrational ψ
have this₁ : Irrational ((↑1 : ℝ) - √(↑5 : ℝ))
Tactic: have := this.ratCast_sub 1
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
this_1 : Irrational √(↑5 : ℝ)
this : Irrational ((↑1 : ℝ) - √(↑5 : ℝ))
⊢ Irrational ψ
have h : ψ = (↑0.5 : ℝ) * ((↑1 : ℝ) - √(↑5 : ℝ))
Tactic: convert! this.ratCast_mul (show (0.5 : ℚ) ≠ 0 by norm_num)
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
this_1 : Irrational √(↑5 : ℝ)
this : Irrational ((↑1 : ℝ) - √(↑5 : ℝ))
⊢ ψ = (↑0.5 : ℝ) * ((↑1 : ℝ) - √(↑5 : ℝ))
have h : ψ = 0.5 * (1 - √5)
Tactic: simp
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
β : Type u_2
inst : CommRing β
⊢ LinearRecurrence.charPoly fibRec = HPow.hPow (α := β[X]) (β := ℕ) X 2 - HAdd.hAdd (α := β[X]) X 1
have 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
Tactic: rw [fibRec, LinearRecurrence.charPoly]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
α : Type u_1
inst : CommSemiring α
n : ℕ
⊢ Eq.{u_1 + 1} (α := α)
    ((fun (x : ℕ) ↦ ((↑(Nat.fib x) : α) : α))
      (n + LinearRecurrence.order.{u_1} (R := α) { order := 2, coeffs := ![1, 1] : LinearRecurrence α }))
    (∑ i : Fin { order := 2, coeffs := ![1, 1] }.order,
      LinearRecurrence.coeffs { order := 2, coeffs := ![1, 1] : LinearRecurrence α } i *
        (fun (x : ℕ) ↦ ((↑(Nat.fib x) : α) : α)) (n + (↑i : ℕ)))
have simp : Eq.{u_1 + 1} (α := α) (↑(Nat.fib (n + 2)) : α)
  (∑ x : Fin 2, HMul.hMul (α := α) (![1, 1] x) (↑(Nat.fib (n + (↑x : ℕ))) : α))
Tactic: simp only
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
α : Type u_1
inst : CommSemiring α
n : ℕ
⊢ Eq.{u_1 + 1} (α := α) (↑(Nat.fib (n + 2)) : α)
    (∑ x : Fin 2, HMul.hMul (α := α) (![1, 1] x) (↑(Nat.fib (n + (↑x : ℕ))) : α))
have rw : Eq.{u_1 + 1} (α := α) (↑(Nat.fib (n + 1) + Nat.fib n) : α)
  (∑ x : Fin 2, HMul.hMul (α := α) (![1, 1] x) (↑(Nat.fib (n + (↑x : ℕ))) : α))
Tactic: rw [Nat.fib_add_two, add_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
⊢ LinearRecurrence.IsSolution (R := ℝ) fibRec fun (x : ℕ) ↦ φ ^ x
have rw : (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 - HAdd.hAdd (α := ℝ[X]) X 1).IsRoot φ
Tactic: rw [fibRec.geom_sol_iff_root_charPoly, fibRec_charPoly_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
⊢ LinearRecurrence.IsSolution (R := ℝ) fibRec fun (x : ℕ) ↦ ψ ^ x
have rw : (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 - HAdd.hAdd (α := ℝ[X]) X 1).IsRoot ψ
Tactic: rw [fibRec.geom_sol_iff_root_charPoly, fibRec_charPoly_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
⊢ Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ (↑(Nat.fib n) : ℝ)) fun (n : ℕ) ↦ (φ ^ n - ψ ^ n) / √5
have rw : Set.EqOn (β := ℝ) (fun (n : ℕ) ↦ (↑(Nat.fib n) : ℝ)) (fun (n : ℕ) ↦ (φ ^ n - ψ ^ n) / √5)
  (↑(Finset.range (LinearRecurrence.order (R := ℝ) fibRec)) : Set ℕ)
Tactic: rw [fibRec.eq_iff_eqOn_range_order]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
rw :
  Set.EqOn (β := ℝ) (fun (n : ℕ) ↦ (↑(Nat.fib n) : ℝ)) (fun (n : ℕ) ↦ (φ ^ n - ψ ^ n) / √5)
    (↑(Finset.range (LinearRecurrence.order (R := ℝ) fibRec)) : Set ℕ)
⊢ Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ (↑(Nat.fib n) : ℝ)) fun (n : ℕ) ↦ (φ ^ n - ψ ^ n) / √5
have hu : LinearRecurrence.IsSolution (R := ℝ) fibRec fun (n : ℕ) ↦ (↑(Nat.fib n) : ℝ)
Tactic: rw [fibRec.eq_iff_eqOn_range_order]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
rw :
  Set.EqOn (β := ℝ) (fun (n : ℕ) ↦ (↑(Nat.fib n) : ℝ)) (fun (n : ℕ) ↦ (φ ^ n - ψ ^ n) / √5)
    (↑(Finset.range (LinearRecurrence.order (R := ℝ) fibRec)) : Set ℕ)
hu : LinearRecurrence.IsSolution (R := ℝ) fibRec fun (n : ℕ) ↦ (↑(Nat.fib n) : ℝ)
⊢ Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ (↑(Nat.fib n) : ℝ)) fun (n : ℕ) ↦ (φ ^ n - ψ ^ n) / √5
have hv : LinearRecurrence.IsSolution (R := ℝ) fibRec fun (n : ℕ) ↦ (φ ^ n - ψ ^ n) / √5
Tactic: rw [fibRec.eq_iff_eqOn_range_order]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (hypothesis)
Goal:
i : ℕ
hi : i ∈ (↑(Finset.range (LinearRecurrence.order (R := ℝ) fibRec)) : Set ℕ)
⊢ Eq (α := ℝ) ((fun (n : ℕ) ↦ ((↑(Nat.fib n) : ℝ) : ℝ)) i) ((fun (n : ℕ) ↦ (φ ^ n - ψ ^ n) / √5) i)
have hi₁ : i ∈ Finset.range (LinearRecurrence.order (R := ℝ) fibRec)
Tactic: norm_cast at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
i : ℕ
hi : i ∈ Finset.range (LinearRecurrence.order (R := ℝ) fibRec)
⊢ Eq (α := ℝ) ((fun (n : ℕ) ↦ ((↑(Nat.fib n) : ℝ) : ℝ)) i) ((fun (n : ℕ) ↦ (φ ^ n - ψ ^ n) / √5) i)
have 0 : Eq (α := ℝ) ((fun (n : ℕ) ↦ ((↑(Nat.fib n) : ℝ) : ℝ)) 0) ((fun (n : ℕ) ↦ (φ ^ n - ψ ^ n) / √5) 0)
Tactic: fin_cases hi
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
i : ℕ
hi : i ∈ Finset.range (LinearRecurrence.order (R := ℝ) fibRec)
0 : Eq (α := ℝ) ((fun (n : ℕ) ↦ ((↑(Nat.fib n) : ℝ) : ℝ)) 0) ((fun (n : ℕ) ↦ (φ ^ n - ψ ^ n) / √5) 0)
⊢ Eq (α := ℝ) ((fun (n : ℕ) ↦ ((↑(Nat.fib n) : ℝ) : ℝ)) i) ((fun (n : ℕ) ↦ (φ ^ n - ψ ^ n) / √5) i)
have 1 : Eq (α := ℝ) ((fun (n : ℕ) ↦ ((↑(Nat.fib n) : ℝ) : ℝ)) 1) ((fun (n : ℕ) ↦ (φ ^ n - ψ ^ n) / √5) 1)
Tactic: fin_cases hi
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
this :
  LinearRecurrence.IsSolution fibRec
    (HSub.hSub (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ (√5)⁻¹ * φ ^ n) fun (n : ℕ) ↦ (√5)⁻¹ * ψ ^ n)
⊢ LinearRecurrence.IsSolution (R := ℝ) fibRec fun (n : ℕ) ↦ (φ ^ n - ψ ^ n) / √5
have h : ∀ (x : ℕ),
  (φ ^ x - ψ ^ x) / √5 =
    HSub.hSub (α := (n : ℕ) → ℝ) (β := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ (√5)⁻¹ * φ ^ n) (fun (n : ℕ) ↦ (√5)⁻¹ * ψ ^ n) x
Tactic: convert! this
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
⊢ LinearRecurrence.IsSolution (R := ℝ) fibRec fun (n : ℕ) ↦ (φ ^ n - ψ ^ n) / √5
have hv : LinearRecurrence.IsSolution fibRec
  (HSub.hSub (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ (√5)⁻¹ * φ ^ n) fun (n : ℕ) ↦ (√5)⁻¹ * ψ ^ n)
Tactic: suffices LinearRecurrence.IsSolution fibRec
        ((fun n ↦ (√5)⁻¹ * φ ^ n) - (fun n ↦ (√5)⁻¹ * ψ ^ n)) by
      convert! this
      rw [Pi.sub_apply]
      ring
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
⊢ LinearRecurrence.IsSolution fibRec
    (HSub.hSub (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ (√5)⁻¹ * φ ^ n) fun (n : ℕ) ↦ (√5)⁻¹ * ψ ^ n)
have hv : Membership.mem (γ := Submodule ℝ (ℕ → ℝ)) (LinearRecurrence.solSpace fibRec) fun (n : ℕ) ↦ (√5)⁻¹ * φ ^ n
Tactic: apply (@fibRec ℝ _).solSpace.sub_mem
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
hv : Membership.mem (γ := Submodule ℝ (ℕ → ℝ)) (LinearRecurrence.solSpace fibRec) fun (n : ℕ) ↦ (√5)⁻¹ * φ ^ n
⊢ LinearRecurrence.IsSolution fibRec
    (HSub.hSub (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ (√5)⁻¹ * φ ^ n) fun (n : ℕ) ↦ (√5)⁻¹ * ψ ^ n)
have hv₁ : Membership.mem (γ := Submodule ℝ (ℕ → ℝ)) (LinearRecurrence.solSpace fibRec) fun (n : ℕ) ↦ (√5)⁻¹ * ψ ^ n
Tactic: apply (@fibRec ℝ _).solSpace.sub_mem
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
⊢ ∀ (n : ℕ), (↑(Nat.fib n) : ℝ) = (φ ^ n - ψ ^ n) / √5
have rw : Eq (α := (x : ℕ) → ℝ) (fun (n : ℕ) ↦ (↑(Nat.fib n) : ℝ)) fun (n : ℕ) ↦ (φ ^ n - ψ ^ n) / √5
Tactic: rw [← funext_iff, Real.coe_fib_eq']