awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
β : Type u_2
inst : CommRing β
⊢ 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:
simp [Finset.sum_fin_eq_sum_range, Finset.sum_range_succ', ← smul_X_eq_monomial]

Premises used: Finset.sum_fin_eq_sum_range, Polynomial.smul_X_eq_monomial, Finset.sum_range_succ'
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
α : Type u_1
inst : CommSemiring α
n : ℕ
simp :
  Eq.{u_1 + 1} (α := α) (↑(Nat.fib (n + 2)) : α)
    (∑ x : Fin 2, HMul.hMul (α := α) (![1, 1] x) (↑(Nat.fib (n + (↑x : ℕ))) : α))
⊢ 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 : ℕ)))

Tactic:
simp only
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
α : Type u_1
inst : CommSemiring α
n : ℕ
rw :
  Eq.{u_1 + 1} (α := α) (↑(Nat.fib (n + 1) + Nat.fib n) : α)
    (∑ x : Fin 2, HMul.hMul (α := α) (![1, 1] x) (↑(Nat.fib (n + (↑x : ℕ))) : α))
⊢ Eq.{u_1 + 1} (α := α) (↑(Nat.fib (n + 2)) : α)
    (∑ x : Fin 2, HMul.hMul (α := α) (![1, 1] x) (↑(Nat.fib (n + (↑x : ℕ))) : α))

Tactic:
rw [Nat.fib_add_two, add_comm]

Premises used: Nat.fib_add_two, add_comm
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
α : Type u_1
inst : CommSemiring α
n : ℕ
⊢ Eq.{u_1 + 1} (α := α) (↑(Nat.fib (n + 1) + Nat.fib n) : α)
    (∑ x : Fin 2, HMul.hMul (α := α) (![1, 1] x) (↑(Nat.fib (n + (↑x : ℕ))) : α))

Tactic:
simp [Finset.sum_fin_eq_sum_range, Finset.sum_range_succ']

Premises used: Finset.sum_fin_eq_sum_range, Finset.sum_range_succ'
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
rw : (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 - HAdd.hAdd (α := ℝ[X]) X 1).IsRoot φ
⊢ LinearRecurrence.IsSolution (R := ℝ) fibRec fun (x : ℕ) ↦ φ ^ x

Tactic:
rw [fibRec.geom_sol_iff_root_charPoly, fibRec_charPoly_eq]

Premises used: Real.fibRec_charPoly_eq, LinearRecurrence.geom_sol_iff_root_charPoly, Real.fibRec
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 - HAdd.hAdd (α := ℝ[X]) X 1).IsRoot φ

Tactic:
simp
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
rw : (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 - HAdd.hAdd (α := ℝ[X]) X 1).IsRoot ψ
⊢ LinearRecurrence.IsSolution (R := ℝ) fibRec fun (x : ℕ) ↦ ψ ^ x

Tactic:
rw [fibRec.geom_sol_iff_root_charPoly, fibRec_charPoly_eq]

Premises used: Real.fibRec_charPoly_eq, LinearRecurrence.geom_sol_iff_root_charPoly, Real.fibRec
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 - HAdd.hAdd (α := ℝ[X]) X 1).IsRoot ψ

Tactic:
simp
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
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) : ℝ)
hv : LinearRecurrence.IsSolution (R := ℝ) fibRec fun (n : ℕ) ↦ (φ ^ n - ψ ^ n) / √5
⊢ Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ (↑(Nat.fib n) : ℝ)) fun (n : ℕ) ↦ (φ ^ n - ψ ^ n) / √5

Tactic:
rw [fibRec.eq_iff_eqOn_range_order]

Premises used: LinearRecurrence.eq_iff_eqOn_range_order, Real.fibRec
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
i : ℕ
hi : i ∈ (↑(Finset.range (LinearRecurrence.order (R := ℝ) fibRec)) : Set ℕ)
⊢ i ∈ Finset.range (LinearRecurrence.order (R := ℝ) fibRec)

Tactic:
norm_cast at hi
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
i : ℕ
hi : i ∈ Finset.range (LinearRecurrence.order (R := ℝ) fibRec)
0 : Eq (α := ℝ) ((fun (n : ℕ) ↦ ((↑(Nat.fib n) : ℝ) : ℝ)) 0) ((fun (n : ℕ) ↦ (φ ^ n - ψ ^ n) / √5) 0)
1 : Eq (α := ℝ) ((fun (n : ℕ) ↦ ((↑(Nat.fib n) : ℝ) : ℝ)) 1) ((fun (n : ℕ) ↦ (φ ^ n - ψ ^ n) / √5) 1)
⊢ Eq (α := ℝ) ((fun (n : ℕ) ↦ ((↑(Nat.fib n) : ℝ) : ℝ)) i) ((fun (n : ℕ) ↦ (φ ^ n - ψ ^ n) / √5) i)

Tactic:
fin_cases hi
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ Eq (α := ℝ) ((fun (n : ℕ) ↦ ((↑(Nat.fib n) : ℝ) : ℝ)) 0) ((fun (n : ℕ) ↦ (φ ^ n - ψ ^ n) / √5) 0)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ Eq (α := ℝ) ((fun (n : ℕ) ↦ ((↑(Nat.fib n) : ℝ) : ℝ)) 1) ((fun (n : ℕ) ↦ (φ ^ n - ψ ^ n) / √5) 1)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ LinearRecurrence.IsSolution (R := ℝ) fibRec fun (n : ℕ) ↦ (↑(Nat.fib n) : ℝ)

Tactic:
fib_isSol_fibRec

Premises used: Real.fib_isSol_fibRec
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ LinearRecurrence.IsSolution (R := ℝ) fibRec fun (n : ℕ) ↦ (↑(Nat.fib n) : ℝ)

Tactic:
exact fib_isSol_fibRec

Premises used: Real.fib_isSol_fibRec
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
this :
  LinearRecurrence.IsSolution fibRec
    (HSub.hSub (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ (√5)⁻¹ * φ ^ n) fun (n : ℕ) ↦ (√5)⁻¹ * ψ ^ n)
⊢ LinearRecurrence.IsSolution fibRec
    (HSub.hSub (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ (√5)⁻¹ * φ ^ n) fun (n : ℕ) ↦ (√5)⁻¹ * ψ ^ n)

Tactic:
this
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
this :
  LinearRecurrence.IsSolution fibRec
    (HSub.hSub (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ (√5)⁻¹ * φ ^ n) fun (n : ℕ) ↦ (√5)⁻¹ * ψ ^ n)
h :
  ∀ (x : ℕ),
    (φ ^ x - ψ ^ x) / √5 =
      HSub.hSub (α := (n : ℕ) → ℝ) (β := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ (√5)⁻¹ * φ ^ n) (fun (n : ℕ) ↦ (√5)⁻¹ * ψ ^ n) x
⊢ LinearRecurrence.IsSolution (R := ℝ) fibRec fun (n : ℕ) ↦ (φ ^ n - ψ ^ n) / √5

Tactic:
convert! this
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
this :
  LinearRecurrence.IsSolution fibRec
    (HSub.hSub (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ (√5)⁻¹ * φ ^ n) fun (n : ℕ) ↦ (√5)⁻¹ * ψ ^ n)
x : ℕ
⊢ (φ ^ x - ψ ^ x) / √5 = (√5)⁻¹ * φ ^ x - (√5)⁻¹ * ψ ^ x

Tactic:
ring
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
hv :
  LinearRecurrence.IsSolution fibRec
    (HSub.hSub (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ (√5)⁻¹ * φ ^ n) fun (n : ℕ) ↦ (√5)⁻¹ * ψ ^ n)
⊢ LinearRecurrence.IsSolution (R := ℝ) fibRec fun (n : ℕ) ↦ (φ ^ n - ψ ^ n) / √5

Tactic:
suffices LinearRecurrence.IsSolution fibRec
        ((fun n ↦ (√5)⁻¹ * φ ^ n) - (fun n ↦ (√5)⁻¹ * ψ ^ n)) by
      convert! this
      rw [Pi.sub_apply]
      ring
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
hv : Membership.mem (γ := Submodule ℝ (ℕ → ℝ)) (LinearRecurrence.solSpace fibRec) fun (n : ℕ) ↦ (√5)⁻¹ * φ ^ n
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)

Tactic:
apply (@fibRec ℝ _).solSpace.sub_mem

Premises used: LinearRecurrence.solSpace, Real.fibRec, Submodule.sub_mem
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ Membership.mem (γ := Submodule ℝ (ℕ → ℝ)) (LinearRecurrence.solSpace fibRec) fun (n : ℕ) ↦ (√5)⁻¹ * φ ^ n

Tactic:
Submodule.smul_mem fibRec.solSpace (√5)⁻¹ geom_goldenRatio_isSol_fibRec

Premises used: Real.geom_goldenRatio_isSol_fibRec, Set.Mem, setOf, LinearRecurrence.solSpace, Inv.inv, Real.sqrt, Real.fibRec, OfNat.ofNat, Submodule.smul_mem
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ Membership.mem (γ := Submodule ℝ (ℕ → ℝ)) (LinearRecurrence.solSpace fibRec) fun (n : ℕ) ↦ (√5)⁻¹ * φ ^ n

Tactic:
exact Submodule.smul_mem fibRec.solSpace (√5)⁻¹ geom_goldenRatio_isSol_fibRec

Premises used: Real.geom_goldenRatio_isSol_fibRec, LinearRecurrence.solSpace, Inv.inv, Real.sqrt, Real.fibRec, OfNat.ofNat, Submodule.smul_mem
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ Membership.mem (γ := Submodule ℝ (ℕ → ℝ)) (LinearRecurrence.solSpace fibRec) fun (n : ℕ) ↦ (√5)⁻¹ * ψ ^ n

Tactic:
Submodule.smul_mem fibRec.solSpace (√5)⁻¹ geom_goldenConj_isSol_fibRec

Premises used: Set.Mem, setOf, LinearRecurrence.solSpace, Inv.inv, Real.sqrt, Real.fibRec, OfNat.ofNat, Real.geom_goldenConj_isSol_fibRec, Submodule.smul_mem
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ Membership.mem (γ := Submodule ℝ (ℕ → ℝ)) (LinearRecurrence.solSpace fibRec) fun (n : ℕ) ↦ (√5)⁻¹ * ψ ^ n

Tactic:
exact Submodule.smul_mem fibRec.solSpace (√5)⁻¹ geom_goldenConj_isSol_fibRec

Premises used: LinearRecurrence.solSpace, Inv.inv, Real.sqrt, Real.fibRec, OfNat.ofNat, Real.geom_goldenConj_isSol_fibRec, Submodule.smul_mem
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
rw : Eq (α := (x : ℕ) → ℝ) (fun (n : ℕ) ↦ (↑(Nat.fib n) : ℝ)) fun (n : ℕ) ↦ (φ ^ n - ψ ^ n) / √5
rw₁ rw₂ : Eq (α := (x : ℕ) → ℝ) (fun (n : ℕ) ↦ (φ ^ n - ψ ^ n) / √5) fun (n : ℕ) ↦ (φ ^ n - ψ ^ n) / √5
⊢ ∀ (n : ℕ), (↑(Nat.fib n) : ℝ) = (φ ^ n - ψ ^ n) / √5

Tactic:
rw [← funext_iff, Real.coe_fib_eq']

Premises used: funext_iff, Real.coe_fib_eq'
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
n : ℤ
inl : ∀ (n : ℕ), (↑(Int.fib (↑n : ℤ)) : ℝ) = (HPow.hPow (β := ℤ) φ (↑n : ℤ) - HPow.hPow (β := ℤ) ψ (↑n : ℤ)) / √5
inr :
  ∀ (n : ℕ), (↑(Int.fib (-(↑n : ℤ))) : ℝ) = (HPow.hPow (β := ℤ) φ (-(↑n : ℤ)) - HPow.hPow (β := ℤ) ψ (-(↑n : ℤ))) / √5
⊢ (↑(Int.fib n) : ℝ) = (φ ^ n - ψ ^ n) / √5

Tactic:
obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
n : ℕ
⊢ (↑(Int.fib (↑n : ℤ)) : ℝ) = (HPow.hPow (β := ℤ) φ (↑n : ℤ) - HPow.hPow (β := ℤ) ψ (↑n : ℤ)) / √5

Tactic:
coe_fib_eq n

Premises used: Int.fib, Real.coe_fib_eq, zpowRec, Int.toNat, ite
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
n : ℕ
⊢ (↑(Int.fib (↑n : ℤ)) : ℝ) = (HPow.hPow (β := ℤ) φ (↑n : ℤ) - HPow.hPow (β := ℤ) ψ (↑n : ℤ)) / √5

Tactic:
exact coe_fib_eq n

Premises used: Real.coe_fib_eq
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
n : ℕ
inr :
  (if Even n then -(↑(Nat.fib n) : ℝ) else (↑(Nat.fib n) : ℝ)) =
    ((if Even n then 1 else -1) * ψ ^ n - (if Even n then 1 else -1) * φ ^ n) / √5
⊢ (↑(Int.fib (-(↑n : ℤ))) : ℝ) = (HPow.hPow (β := ℤ) φ (-(↑n : ℤ)) - HPow.hPow (β := ℤ) ψ (-(↑n : ℤ))) / √5

Tactic:
simp only [Int.fib_neg, Int.even_coe_nat, Int.fib_natCast, Int.cast_ite, Int.cast_neg,
      Int.cast_natCast, zpow_neg, zpow_natCast, ← inv_pow, inv_goldenRatio, inv_goldenConj,
      ← neg_one_mul ψ, ← neg_one_mul φ, mul_pow, neg_one_pow_eq_ite]

Premises used: neg_one_pow_eq_ite, zpow_natCast, Int.cast_neg, Int.cast_natCast, Real.inv_goldenConj, Real.inv_goldenRatio, neg_one_mul, Int.fib_natCast, Real.goldenConj, Real.goldenRatio, Int.fib_neg, inv_pow, zpow_neg, mul_pow, Int.cast_ite, Int.even_coe_nat
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
n : ℕ
⊢ (if Even n then -(↑(Nat.fib n) : ℝ) else (↑(Nat.fib n) : ℝ)) =
    ((if Even n then 1 else -1) * ψ ^ n - (if Even n then 1 else -1) * φ ^ n) / √5

Tactic:
grind [coe_fib_eq]

Premises used: Real.coe_fib_eq
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
n : ℕ
rw : (φ ^ (n + 1) - ψ ^ (n + 1)) / √5 - φ * (↑(Nat.fib n) : ℝ) = ψ ^ n
⊢ (↑(Nat.fib (n + 1)) : ℝ) - φ * (↑(Nat.fib n) : ℝ) = ψ ^ n

Tactic:
rw [coe_fib_eq]

Premises used: Real.coe_fib_eq
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
n : ℕ
rw : (φ ^ (n + 1) - ψ ^ (n + 1)) / √5 - φ * ((φ ^ n - ψ ^ n) / √5) = ψ ^ n
⊢ (φ ^ (n + 1) - ψ ^ (n + 1)) / √5 - φ * (↑(Nat.fib n) : ℝ) = ψ ^ n

Tactic:
rw [coe_fib_eq]

Premises used: Real.coe_fib_eq
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
n : ℕ
repeat : (φ ^ (n + 1) - ψ ^ (n + 1)) / √5 - φ * ((φ ^ n - ψ ^ n) / √5) = ψ ^ n
⊢ (↑(Nat.fib (n + 1)) : ℝ) - φ * (↑(Nat.fib n) : ℝ) = ψ ^ n

Tactic:
repeat rw [coe_fib_eq]

Premises used: Real.coe_fib_eq
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
n : ℕ
rw : (φ ^ (n + 1) - ψ ^ (n + 1) - (φ ^ (n + 1) - φ * ψ ^ n)) / √5 = ψ ^ n
⊢ (φ ^ (n + 1) - ψ ^ (n + 1)) / √5 - φ * ((φ ^ n - ψ ^ n) / √5) = ψ ^ n

Tactic:
rw [mul_div, div_sub_div_same, mul_sub, ← pow_succ']

Premises used: mul_div, mul_sub, div_sub_div_same, pow_succ'
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
n : ℕ
ring_nf : √5 * (√5)⁻¹ * (1 / 2 + √5 * (-1 / 2)) ^ n = (1 / 2 + √5 * (-1 / 2)) ^ n
⊢ (φ ^ (n + 1) - ψ ^ (n + 1) - (φ ^ (n + 1) - φ * ψ ^ n)) / √5 = ψ ^ n

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
n : ℕ
⊢ √5 ≠ 0

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
n : ℕ
⊢ √5 ≠ 0

Tactic:
have nz : √5 ≠ 0 := by norm_num
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
n : ℕ
nz : √5 ≠ 0
rw : 1 * (1 / 2 + √5 * (-1 / 2)) ^ n = (1 / 2 + √5 * (-1 / 2)) ^ n
rw₁ rw₂ : (1 / 2 + √5 * (-1 / 2)) ^ n = (1 / 2 + √5 * (-1 / 2)) ^ n
⊢ √5 * (√5)⁻¹ * (1 / 2 + √5 * (-1 / 2)) ^ n = (1 / 2 + √5 * (-1 / 2)) ^ n

Tactic:
rw [← (mul_inv_cancel₀ nz).symm, one_mul]

Premises used: mul_inv_cancel₀, Eq.symm, one_mul
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
n : ℕ
⊢ ψ * (↑(Nat.fib (n + 1)) : ℝ) + (↑(Nat.fib n) : ℝ) = ψ ^ (n + 1)

Tactic:
grind [fib_succ_sub_goldenRatio_mul_fib]

Premises used: Real.fib_succ_sub_goldenRatio_mul_fib
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
⊢ φ * (↑(Nat.fib (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + (↑(Nat.fib 0) : ℝ) = φ ^ HAdd.hAdd (α := ℕ) 0 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
n : ℕ
ih : φ * (↑(Nat.fib (n + 1)) : ℝ) + (↑(Nat.fib n) : ℝ) = φ ^ (n + 1)
simp :
  φ * HAdd.hAdd (α := ℝ) (↑(Nat.fib n) : ℝ) (↑(Nat.fib n.succ) : ℝ) + (↑(Nat.fib (n + 1)) : ℝ) =
    φ * (↑(Nat.fib n) : ℝ) + (φ + 1) * (↑(Nat.fib (n + 1)) : ℝ)
⊢ φ * (↑(Nat.fib (n + 1 + 1)) : ℝ) + (↑(Nat.fib (n + 1)) : ℝ) =
    φ * (↑(Nat.fib n) : ℝ) + HPow.hPow (β := ℕ) φ 2 * (↑(Nat.fib (n + 1)) : ℝ)

Tactic:
simp only [Nat.fib_add_one (Nat.succ_ne_zero n), Nat.succ_sub_succ_eq_sub,
          Nat.cast_add, goldenRatio_sq, Nat.sub_zero]

Premises used: Nat.cast_add, Nat.succ_ne_zero, Nat.sub_zero, Nat.succ_sub_succ_eq_sub, Nat.fib_add_one, Real.goldenRatio_sq
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
n : ℕ
ih : φ * (↑(Nat.fib (n + 1)) : ℝ) + (↑(Nat.fib n) : ℝ) = φ ^ (n + 1)
⊢ φ * HAdd.hAdd (α := ℝ) (↑(Nat.fib n) : ℝ) (↑(Nat.fib n.succ) : ℝ) + (↑(Nat.fib (n + 1)) : ℝ) =
    φ * (↑(Nat.fib n) : ℝ) + (φ + 1) * (↑(Nat.fib (n + 1)) : ℝ)

Tactic:
ring
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
n : ℕ
ih : φ * (↑(Nat.fib (n + 1)) : ℝ) + (↑(Nat.fib n) : ℝ) = φ ^ (n + 1)
⊢ φ * (↑(Nat.fib n) : ℝ) + HPow.hPow (β := ℕ) φ 2 * (↑(Nat.fib (n + 1)) : ℝ) =
    φ * ((↑(Nat.fib n) : ℝ) + φ * (↑(Nat.fib (n + 1)) : ℝ))

Tactic:
ring
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
n : ℕ
ih : φ * (↑(Nat.fib (n + 1)) : ℝ) + (↑(Nat.fib n) : ℝ) = φ ^ (n + 1)
rw : φ * φ ^ (n + 1) = φ ^ (n + 2)
⊢ φ * ((↑(Nat.fib n) : ℝ) + φ * (↑(Nat.fib (n + 1)) : ℝ)) = φ ^ (n + 2)

Tactic:
rw [add_comm, ih]

Premises used: add_comm
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
n : ℕ
ih : φ * (↑(Nat.fib (n + 1)) : ℝ) + (↑(Nat.fib n) : ℝ) = φ ^ (n + 1)
⊢ φ * φ ^ (n + 1) = φ ^ (n + 2)

Tactic:
ring
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
n : ℕ
ih : φ * (↑(Nat.fib (n + 1)) : ℝ) + (↑(Nat.fib n) : ℝ) = φ ^ (n + 1)
_ :
  φ * (↑(Nat.fib (n + 1 + 1)) : ℝ) + (↑(Nat.fib (n + 1)) : ℝ) =
    φ * (↑(Nat.fib n) : ℝ) + HPow.hPow (β := ℕ) φ 2 * (↑(Nat.fib (n + 1)) : ℝ)
_₁ :
  φ * (↑(Nat.fib n) : ℝ) + HPow.hPow (β := ℕ) φ 2 * (↑(Nat.fib (n + 1)) : ℝ) =
    φ * ((↑(Nat.fib n) : ℝ) + φ * (↑(Nat.fib (n + 1)) : ℝ))
_₂ : φ * ((↑(Nat.fib n) : ℝ) + φ * (↑(Nat.fib (n + 1)) : ℝ)) = φ ^ (n + 2)
⊢ φ * (↑(Nat.fib (n + 1 + 1)) : ℝ) + (↑(Nat.fib (n + 1)) : ℝ) = φ ^ (n + 1 + 1)

Tactic:
calc
      _ = φ * (Nat.fib n) + φ ^ 2 * (Nat.fib (n + 1)) := by
        simp only [Nat.fib_add_one (Nat.succ_ne_zero n), Nat.succ_sub_succ_eq_sub,
          Nat.cast_add, goldenRatio_sq, Nat.sub_zero]; ring
      _ = φ * ((Nat.fib n) + φ * (Nat.fib (n + 1))) := by ring
      _ = φ ^ (n + 2) := by rw [add_comm, ih]; ring

Premises used: HMul.hMul, Real.goldenRatio, Nat.cast, HAdd.hAdd, Nat.fib, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
n : ℕ
zero : φ * (↑(Nat.fib (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + (↑(Nat.fib 0) : ℝ) = φ ^ HAdd.hAdd (α := ℕ) 0 1
succ :
  ∀ (n : ℕ) (ih : φ * (↑(Nat.fib (n + 1)) : ℝ) + (↑(Nat.fib n) : ℝ) = φ ^ (n + 1)),
    φ * (↑(Nat.fib (n + 1 + 1)) : ℝ) + (↑(Nat.fib (n + 1)) : ℝ) = φ ^ (n + 1 + 1)
⊢ φ * (↑(Nat.fib (n + 1)) : ℝ) + (↑(Nat.fib n) : ℝ) = φ ^ (n + 1)

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    calc
      _ = φ * (Nat.fib n) + φ ^ 2 * (Nat.fib (n + 1)) := by
        simp only [Nat.fib_add_one (Nat.succ_ne_zero n), Nat.succ_sub_succ_eq_sub,
          Nat.cast_add, goldenRatio_sq, Nat.sub_zero]; ring
      _ = φ * ((Nat.fib n) + φ * (Nat.fib (n + 1))) := by ring
      _ = φ ^ (n + 2) := by rw [add_comm, ih]; ring

Premises used: HMul.hMul, Real.goldenRatio, Nat.cast, HAdd.hAdd, Nat.fib, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Real.GoldenRatio
Goal:
n : ℕ
⊢ (↑(Nat.fib (n + 1)) : ℝ) - ψ * (↑(Nat.fib n) : ℝ) = φ ^ n

Tactic:
grind [goldenRatio_mul_fib_succ_add_fib]

Premises used: Real.goldenRatio_mul_fib_succ_add_fib
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
ι : Type u_5
inst : CompleteLattice α
s : ι → α
⊢ Eq.{u_2 + 1} (α := α) (⨆ (i : ι), s i) (⨆ (t : Finset ι), ⨆ i ∈ t, s i)

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
ι : Type u_5
inst : CompleteLattice α
s : ι → α
refine_1 : LE.le.{u_2} (α := α) (⨆ (i : ι), s i) (⨆ (t : Finset ι), ⨆ i ∈ t, s i)
refine_2 : LE.le.{u_2} (α := α) (⨆ (t : Finset ι), ⨆ i ∈ t, s i) (⨆ (i : ι), s i)
⊢ Eq.{u_2 + 1} (α := α) (⨆ (i : ι), s i) (⨆ (t : Finset ι), ⨆ i ∈ t, s i)

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
ι : Type u_5
inst : CompleteLattice α
s : ι → α
b : ι
⊢ Membership.mem (γ := Finset ι) {b} b

Tactic:
simp
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
ι : Type u_5
inst : CompleteLattice α
s : ι → α
⊢ LE.le.{u_2} (α := α) (⨆ (i : ι), s i) (⨆ (t : Finset ι), ⨆ i ∈ t, s i)

Tactic:
exact iSup_le fun b => le_iSup_of_le {b} <| le_iSup_of_le b <| le_iSup_of_le (by simp) <| le_rfl

Premises used: le_iSup_of_le, iSup_le
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
ι : Type u_5
inst : CompleteLattice α
s : ι → α
⊢ LE.le.{u_2} (α := α) (⨆ (t : Finset ι), ⨆ i ∈ t, s i) (⨆ (i : ι), s i)

Tactic:
iSup_le fun t => iSup_le fun b => iSup_le fun _ => le_iSup _ _

Premises used: le_iSup, iSup_le
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
ι : Type u_5
inst : CompleteLattice α
s : ι → α
⊢ LE.le.{u_2} (α := α) (⨆ (t : Finset ι), ⨆ i ∈ t, s i) (⨆ (i : ι), s i)

Tactic:
exact iSup_le fun t => iSup_le fun b => iSup_le fun _ => le_iSup _ _

Premises used: le_iSup, iSup_le
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
ι : Type u_5
inst : CompleteLattice α
s : ι → α
refine_1 : LE.le.{u_2} (α := α) (⨆ (i : ι), s i) (⨆ (t : Finset ι), ⨆ i ∈ t, s i)
refine_2 refine_2₁ : LE.le.{u_2} (α := α) (⨆ (t : Finset ι), ⨆ i ∈ t, s i) (⨆ (i : ι), s i)
⊢ Eq.{u_2 + 1} (α := α) (⨆ (i : ι), s i) (⨆ (t : Finset ι), ⨆ i ∈ t, s i)

Tactic:
classical
  refine le_antisymm ?_ ?_
  · exact iSup_le fun b => le_iSup_of_le {b} <| le_iSup_of_le b <| le_iSup_of_le (by simp) <| le_rfl
  · exact iSup_le fun t => iSup_le fun b => iSup_le fun _ => le_iSup _ _

Premises used: le_iSup, le_antisymm, le_iSup_of_le, iSup_le
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
ι' : Sort u_7
inst : CompleteLattice α
s : ι' → α
rw : Eq.{u_2 + 1} (α := α) (⨆ (x : PLift ι'), s ((Equiv.plift : (a : PLift ι') → ι') x)) (⨆ (i : PLift ι'), s i.down)
⊢ Eq.{u_2 + 1} (α := α) (⨆ (i : ι'), s i) (⨆ (t : Finset (PLift ι')), ⨆ i ∈ t, s i.down)

Tactic:
rw [← iSup_eq_iSup_finset, ← Equiv.plift.surjective.iSup_comp]

Premises used: Function.Surjective.iSup_comp, iSup_eq_iSup_finset, Equiv.plift, Equiv.surjective
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
ι' : Sort u_7
inst : CompleteLattice α
s : ι' → α
⊢ Eq.{u_2 + 1} (α := α) (⨆ (x : PLift ι'), s ((Equiv.plift : (a : PLift ι') → ι') x)) (⨆ (i : PLift ι'), s i.down)

Tactic:
rfl
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
ι : Type u_5
s : ι → Set α
⊢ Eq.{u_2 + 1} (α := Set α) (⋃ (i : ι), s i) (⋃ (t : Finset ι), ⋃ i ∈ t, s i)

Tactic:
iSup_eq_iSup_finset s

Premises used: iSup_eq_iSup_finset, Set.iUnion
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
ι' : Sort u_7
s : ι' → Set α
⊢ Eq.{u_2 + 1} (α := Set α) (⋃ (i : ι'), s i) (⋃ (t : Finset (PLift ι')), ⋃ i ∈ t, s i.down)

Tactic:
iSup_eq_iSup_finset' s

Premises used: iSup_eq_iSup_finset', Set.iUnion
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
ι : Type u_5
s : ι → Set α
⊢ Eq.{u_2 + 1} (α := Set α) (⋂ (i : ι), s i) (⋂ (t : Finset ι), ⋂ i ∈ t, s i)

Tactic:
iInf_eq_iInf_finset s

Premises used: Set.iInter, iInf_eq_iInf_finset
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
ι' : Sort u_7
s : ι' → Set α
⊢ Eq.{u_2 + 1} (α := Set α) (⋂ (i : ι'), s i) (⋂ (t : Finset (PLift ι')), ⋂ i ∈ t, s i.down)

Tactic:
iInf_eq_iInf_finset' s

Premises used: iInf_eq_iInf_finset', Set.iInter
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
ι : Type u_5
s : Set ι
h :
  ∀ (x : ι),
    Membership.mem (γ := Set ι)
        (⋃ (s' : Finset (↑s : Type u_5)), Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set (↑s : Type u_5))) x ↔
      x ∈ s
⊢ ⋃ (s' : Finset (↑s : Type u_5)), Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set (↑s : Type u_5)) = s

Tactic:
ext x
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
ι : Type u_5
s : Set ι
x : ι
h : (∃ (i : Finset (↑s : Type u_5)) (x_1 : x ∈ s), Subtype.mk (p := fun (a : ι) ↦ a ∈ s) x ⋯ ∈ i) ↔ x ∈ s
⊢ Membership.mem (γ := Set ι)
      (⋃ (s' : Finset (↑s : Type u_5)), Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set (↑s : Type u_5))) x ↔
    x ∈ s

Tactic:
simp only [Set.mem_iUnion, Set.mem_image, SetLike.mem_coe, Subtype.exists,
    exists_and_right, exists_eq_right]

Premises used: Set.mem_iUnion, Set.mem_image, Subtype.exists, exists_eq_right, exists_and_right, SetLike.mem_coe
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
ι : Type u_5
s : Set ι
x : ι
hx : x ∈ s
⊢ Membership.mem (γ := Finset (↑s : Type u_5)) {Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx}
    (Subtype.mk (p := fun (a : ι) ↦ a ∈ s) x ⋯)

Tactic:
simp
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
ι : Type u_5
s : Set ι
x : ι
⊢ (∃ (i : Finset (↑s : Type u_5)) (x_1 : x ∈ s), Subtype.mk (p := fun (a : ι) ↦ a ∈ s) x ⋯ ∈ i) ↔ x ∈ s

Tactic:
exact ⟨fun ⟨_, hx, _⟩ ↦ hx, fun hx ↦ ⟨{⟨x, hx⟩}, hx, by simp⟩⟩
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
inst : DecidableEq α
P : Finset α → Prop
s : Finset α
hP : ∀ ⦃s t : Finset α⦄, P t → s ⊆ t → P s
simp : P s → ((∀ ⦃y : Finset α⦄, P y → s ≤ y → y ≤ s) ↔ ∀ x ∉ s, ¬P (insert x s))
⊢ Maximal P s ↔ P s ∧ ∀ x ∉ s, ¬P (insert x s)

Tactic:
simp only [Maximal, and_congr_right_iff]

Premises used: and_congr_right_iff, Maximal
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
inst : DecidableEq α
P : Finset α → Prop
s : Finset α
hP : ∀ ⦃s t : Finset α⦄, P t → s ⊆ t → P s
⊢ P s → ((∀ ⦃y : Finset α⦄, P y → s ≤ y → y ≤ s) ↔ ∀ x ∉ s, ¬P (insert x s))

Tactic:
fun _ ↦ ⟨fun h x hxs hx ↦ hxs <| h hx (subset_insert _ _) (mem_insert_self x s),
    fun h t ht hst x hxt ↦ by_contra fun hxs ↦ h x hxs (hP ht (insert_subset hxt hst))⟩

Premises used: Finset.mem_insert_self, Finset.insert_subset, Iff.intro, Finset.subset_insert, by_contra
-- Module: Mathlib.Order.CompleteLattice.Finset
Goal:
α : Type u_2
inst : DecidableEq α
P : Finset α → Prop
s : Finset α
hP : ∀ ⦃s t : Finset α⦄, P t → s ⊆ t → P s
⊢ P s → ((∀ ⦃y : Finset α⦄, P y → s ≤ y → y ≤ s) ↔ ∀ x ∉ s, ¬P (insert x s))

Tactic:
exact fun _ ↦ ⟨fun h x hxs hx ↦ hxs <| h hx (subset_insert _ _) (mem_insert_self x s),
    fun h t ht hst x hxt ↦ by_contra fun hxs ↦ h x hxs (hP ht (insert_subset hxt hst))⟩