awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n_1 : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : (IntFractPair.of ifp_n.fr⁻¹).fr ≠ 0
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
have s_nth_eq : g.s.get? n = some { a := 1, b := (↑⌊ifp_n.fr⁻¹⌋ : K) }
Tactic: have s_nth_eq : g.s.get? n = some ⟨1, (⌊ifp_n.fr⁻¹⌋ : K)⟩ :=
        get?_of_eq_some_of_get?_intFractPair_stream_fr_ne_zero nth_stream_eq ifp_n_fract_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n_1 : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : (IntFractPair.of ifp_n.fr⁻¹).fr ≠ 0
s_nth_eq : g.s.get? n = some { a := 1, b := (↑⌊ifp_n.fr⁻¹⌋ : K) }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
⊢ compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
have simp : (ifp_n.fr⁻¹ * pconts.a + ppconts.a) / (ifp_n.fr⁻¹ * pconts.b + ppconts.b) =
  (ppconts.a + ifp_n.fr⁻¹ * pA) / (ppconts.b + ifp_n.fr⁻¹ * pB)
Tactic: simp only [compExactValue, ifp_n_fract_ne_zero, ↓reduceIte, nextConts, nextNum, one_mul,
          nextDen, ppA, ppB]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n_1 : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : (IntFractPair.of ifp_n.fr⁻¹).fr ≠ 0
s_nth_eq : g.s.get? n = some { a := 1, b := (↑⌊ifp_n.fr⁻¹⌋ : K) }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
have this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
Tactic: have : compExactValue ppconts pconts ifp_n.fr =
          (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB) := by
        -- unfold compExactValue and the convergent computation once
        simp only [compExactValue, ifp_n_fract_ne_zero, ↓reduceIte, nextConts, nextNum, one_mul,
          nextDen, ppA, ppB]
        ac_rfl
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n_1 : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : (IntFractPair.of ifp_n.fr⁻¹).fr ≠ 0
s_nth_eq : g.s.get? n = some { a := 1, b := (↑⌊ifp_n.fr⁻¹⌋ : K) }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
have succ : (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB) = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n_1 : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : (IntFractPair.of ifp_n.fr⁻¹).fr ≠ 0
s_nth_eq : g.s.get? n = some { a := 1, b := (↑⌊ifp_n.fr⁻¹⌋ : K) }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
⊢ (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB) = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
have tmp_calc : ((↑⌊ifp_n.fr⁻¹⌋ : K) * pA + ppA) / Int.fract ifp_n.fr⁻¹ + pA = (pA * ifp_n.fr⁻¹ + ppA) / Int.fract ifp_n.fr⁻¹
Tactic: have tmp_calc :=
        compExactValue_correctness_of_stream_eq_some_aux_comp pA ppA ifp_succ_n_fr_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n_1 : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : (IntFractPair.of ifp_n.fr⁻¹).fr ≠ 0
s_nth_eq : g.s.get? n = some { a := 1, b := (↑⌊ifp_n.fr⁻¹⌋ : K) }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc : ((↑⌊ifp_n.fr⁻¹⌋ : K) * pA + ppA) / Int.fract ifp_n.fr⁻¹ + pA = (pA * ifp_n.fr⁻¹ + ppA) / Int.fract ifp_n.fr⁻¹
⊢ (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB) = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
have tmp_calc' : ((↑⌊ifp_n.fr⁻¹⌋ : K) * pB + ppB) / Int.fract ifp_n.fr⁻¹ + pB = (pB * ifp_n.fr⁻¹ + ppB) / Int.fract ifp_n.fr⁻¹
Tactic: have tmp_calc' :=
        compExactValue_correctness_of_stream_eq_some_aux_comp pB ppB ifp_succ_n_fr_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n_1 : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : (IntFractPair.of ifp_n.fr⁻¹).fr ≠ 0
s_nth_eq : g.s.get? n = some { a := 1, b := (↑⌊ifp_n.fr⁻¹⌋ : K) }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc : ((↑⌊ifp_n.fr⁻¹⌋ : K) * pA + ppA) / Int.fract ifp_n.fr⁻¹ + pA = (pA * ifp_n.fr⁻¹ + ppA) / Int.fract ifp_n.fr⁻¹
tmp_calc' :
  ((↑⌊ifp_n.fr⁻¹⌋ : K) * pB + ppB) / Int.fract ifp_n.fr⁻¹ + pB = (pB * ifp_n.fr⁻¹ + ppB) / Int.fract ifp_n.fr⁻¹
f : K := Int.fract (1 / ifp_n.fr)
⊢ (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB) =
    compExactValue (g.contsAux (n + 1)) (g.contsAux (n + 2)) (IntFractPair.of ifp_n.fr⁻¹).fr
have hfr : (IntFractPair.of (1 / ifp_n.fr)).fr = f
Tactic: have hfr : (IntFractPair.of (1 / ifp_n.fr)).fr = f := rfl
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n_1 : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : (IntFractPair.of ifp_n.fr⁻¹).fr ≠ 0
s_nth_eq : g.s.get? n = some { a := 1, b := (↑⌊ifp_n.fr⁻¹⌋ : K) }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc : ((↑⌊ifp_n.fr⁻¹⌋ : K) * pA + ppA) / Int.fract ifp_n.fr⁻¹ + pA = (pA * ifp_n.fr⁻¹ + ppA) / Int.fract ifp_n.fr⁻¹
tmp_calc' :
  ((↑⌊ifp_n.fr⁻¹⌋ : K) * pB + ppB) / Int.fract ifp_n.fr⁻¹ + pB = (pB * ifp_n.fr⁻¹ + ppB) / Int.fract ifp_n.fr⁻¹
f : K := Int.fract (1 / ifp_n.fr)
hfr : (IntFractPair.of (1 / ifp_n.fr)).fr = f
⊢ (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB) =
    compExactValue (g.contsAux (n + 1)) (g.contsAux (n + 2)) (IntFractPair.of ifp_n.fr⁻¹).fr
have succ : (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB) =
  if (IntFractPair.of ifp_n.fr⁻¹).fr = 0 then
    ((↑⌊ifp_n.fr⁻¹⌋ : K) * (g.contsAux (n + 1)).a + (g.contsAux n).a) /
      ((↑⌊ifp_n.fr⁻¹⌋ : K) * (g.contsAux (n + 1)).b + (g.contsAux n).b)
  else
    ((IntFractPair.of ifp_n.fr⁻¹).fr⁻¹ * ((↑⌊ifp_n.fr⁻¹⌋ : K) * (g.contsAux (n + 1)).a + (g.contsAux n).a) +
        (g.contsAux (n + 1)).a) /
      ((IntFractPair.of ifp_n.fr⁻¹).fr⁻¹ * ((↑⌊ifp_n.fr⁻¹⌋ : K) * (g.contsAux (n + 1)).b + (g.contsAux n).b) +
        (g.contsAux (n + 1)).b)
Tactic: simp [compExactValue, contsAux_recurrence s_nth_eq ppconts_eq pconts_eq,
        nextConts, nextNum, nextDen]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n_1 : ℕ
inst_2 : FloorRing K
n : ℕ
IH : ∀ (nth_stream_eq_none : IntFractPair.stream v n = none), v = (of v).convs (n - 1)
nth_stream_eq_none : IntFractPair.stream v (n + 1) = none
g : GenContFract K := of v
⊢ v = (of v).convs (n + 1 - 1)
have succ : v = g.convs n
Tactic: change v = g.convs n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n_1 : ℕ
inst_2 : FloorRing K
n : ℕ
IH : ∀ (nth_stream_eq_none : IntFractPair.stream v n = none), v = (of v).convs (n - 1)
nth_stream_eq_none : IntFractPair.stream v (n + 1) = none
g : GenContFract K := of v
⊢ v = g.convs n
have succ : ∀ (nth_stream_eq_none : IntFractPair.stream v n = none), v = g.convs n
Tactic: obtain ⟨nth_stream_eq_none⟩ | ⟨ifp_n, nth_stream_eq, nth_stream_fr_eq_zero⟩ :
      IntFractPair.stream v n = none ∨ ∃ ifp, IntFractPair.stream v n = some ifp ∧ ifp.fr = 0 :=
      IntFractPair.succ_nth_stream_eq_none_iff.1 nth_stream_eq_none
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n_1 : ℕ
inst_2 : FloorRing K
n : ℕ
IH : ∀ (nth_stream_eq_none : IntFractPair.stream v n = none), v = (of v).convs (n - 1)
nth_stream_eq_none : IntFractPair.stream v (n + 1) = none
g : GenContFract K := of v
succ : ∀ (nth_stream_eq_none : IntFractPair.stream v n = none), v = g.convs n
⊢ v = g.convs n
have succ₁ : ∀ (ifp_n : IntFractPair K) (nth_stream_eq : IntFractPair.stream v n = some ifp_n)
  (nth_stream_fr_eq_zero : ifp_n.fr = 0), v = g.convs n
Tactic: obtain ⟨nth_stream_eq_none⟩ | ⟨ifp_n, nth_stream_eq, nth_stream_fr_eq_zero⟩ :
      IntFractPair.stream v n = none ∨ ∃ ifp, IntFractPair.stream v n = some ifp ∧ ifp.fr = 0 :=
      IntFractPair.succ_nth_stream_eq_none_iff.1 nth_stream_eq_none
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
n' : ℕ
IH : ∀ (nth_stream_eq_none : IntFractPair.stream v (n' + 1) = none), v = (of v).convs (n' + 1 - 1)
nth_stream_eq_none_1 : IntFractPair.stream v (n' + 1 + 1) = none
nth_stream_eq_none : IntFractPair.stream v (n' + 1) = none
⊢ v = g.convs (n' + 1)
have this : g.TerminatedAt n'
Tactic: have : g.TerminatedAt n' :=
          of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none.2
            nth_stream_eq_none
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
n' : ℕ
IH : ∀ (nth_stream_eq_none : IntFractPair.stream v (n' + 1) = none), v = (of v).convs (n' + 1 - 1)
nth_stream_eq_none_1 : IntFractPair.stream v (n' + 1 + 1) = none
nth_stream_eq_none : IntFractPair.stream v (n' + 1) = none
this : g.TerminatedAt n'
⊢ v = g.convs (n' + 1)
have this₁ : g.convs (n' + 1) = g.convs n'
Tactic: have : g.convs (n' + 1) = g.convs n' :=
          convs_stable_of_terminated n'.le_succ this
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
n' : ℕ
IH : ∀ (nth_stream_eq_none : IntFractPair.stream v (n' + 1) = none), v = (of v).convs (n' + 1 - 1)
nth_stream_eq_none_1 : IntFractPair.stream v (n' + 1 + 1) = none
nth_stream_eq_none : IntFractPair.stream v (n' + 1) = none
this_1 : g.TerminatedAt n'
this : g.convs (n' + 1) = g.convs n'
⊢ v = g.convs (n' + 1)
have succ : v = g.convs n'
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n_1 : ℕ
inst_2 : FloorRing K
n : ℕ
IH : ∀ (nth_stream_eq_none : IntFractPair.stream v n = none), v = (of v).convs (n - 1)
nth_stream_eq_none_1 : IntFractPair.stream v (n + 1) = none
g : GenContFract K := of v
nth_stream_eq_none : IntFractPair.stream v n = none
⊢ v = g.convs n
have succ : ∀ (IH : ∀ (nth_stream_eq_none : IntFractPair.stream v 0 = none), v = (of v).convs (HSub.hSub (α := ℕ) 0 1))
  (nth_stream_eq_none : IntFractPair.stream v (HAdd.hAdd (α := ℕ) 0 1) = none)
  (nth_stream_eq_none : IntFractPair.stream v 0 = none), v = g.convs 0
Tactic: cases n with
      | zero => contradiction
      | succ n' =>
        -- IntFractPair.stream v 0 ≠ none
        have : g.TerminatedAt n' :=
          of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none.2
            nth_stream_eq_none
        have : g.convs (n' + 1) = g.convs n' :=
          convs_stable_of_terminated n'.le_succ this
        rw [this]
        exact IH nth_stream_eq_none
Cleared hypotheses: n, IH, nth_stream_eq_none_1, nth_stream_eq_none
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n_1 : ℕ
inst_2 : FloorRing K
n : ℕ
IH : ∀ (nth_stream_eq_none : IntFractPair.stream v n = none), v = (of v).convs (n - 1)
nth_stream_eq_none_1 : IntFractPair.stream v (n + 1) = none
g : GenContFract K := of v
nth_stream_eq_none : IntFractPair.stream v n = none
succ :
  ∀ (IH : ∀ (nth_stream_eq_none : IntFractPair.stream v 0 = none), v = (of v).convs (HSub.hSub (α := ℕ) 0 1))
    (nth_stream_eq_none : IntFractPair.stream v (HAdd.hAdd (α := ℕ) 0 1) = none)
    (nth_stream_eq_none : IntFractPair.stream v 0 = none), v = g.convs 0
⊢ v = g.convs n
have succ₁ : ∀ (n' : ℕ) (IH : ∀ (nth_stream_eq_none : IntFractPair.stream v (n' + 1) = none), v = (of v).convs (n' + 1 - 1))
  (nth_stream_eq_none : IntFractPair.stream v (n' + 1 + 1) = none)
  (nth_stream_eq_none : IntFractPair.stream v (n' + 1) = none), v = g.convs (n' + 1)
Tactic: cases n with
      | zero => contradiction
      | succ n' =>
        -- IntFractPair.stream v 0 ≠ none
        have : g.TerminatedAt n' :=
          of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none.2
            nth_stream_eq_none
        have : g.convs (n' + 1) = g.convs n' :=
          convs_stable_of_terminated n'.le_succ this
        rw [this]
        exact IH nth_stream_eq_none
Cleared hypotheses: n, IH, nth_stream_eq_none_1, nth_stream_eq_none
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n : ℕ
inst_2 : FloorRing K
nth_stream_eq_none : IntFractPair.stream v n = none
⊢ v = (of v).convs (n - 1)
have zero : ∀ (nth_stream_eq_none : IntFractPair.stream v 0 = none), v = (of v).convs (HSub.hSub (α := ℕ) 0 1)
Tactic: induction n with
  | zero => contradiction
  -- IntFractPair.stream v 0 ≠ none
  | succ n IH =>
    let g := of v
    change v = g.convs n
    obtain ⟨nth_stream_eq_none⟩ | ⟨ifp_n, nth_stream_eq, nth_stream_fr_eq_zero⟩ :
      IntFractPair.stream v n = none ∨ ∃ ifp, IntFractPair.stream v n = some ifp ∧ ifp.fr = 0 :=
      IntFractPair.succ_nth_stream_eq_none_iff.1 nth_stream_eq_none
    · cases n with
      | zero => contradiction
      | succ n' =>
        -- IntFractPair.stream v 0 ≠ none
        have : g.TerminatedAt n' :=
          of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none.2
            nth_stream_eq_none
        have : g.convs (n' + 1) = g.convs n' :=
          convs_stable_of_terminated n'.le_succ this
        rw [this]
        exact IH nth_stream_eq_none
    · simpa [nth_stream_fr_eq_zero, compExactValue] using
        compExactValue_correctness_of_stream_eq_some nth_stream_eq
Cleared hypotheses: nth_stream_eq_none
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n : ℕ
inst_2 : FloorRing K
nth_stream_eq_none : IntFractPair.stream v n = none
zero : ∀ (nth_stream_eq_none : IntFractPair.stream v 0 = none), v = (of v).convs (HSub.hSub (α := ℕ) 0 1)
⊢ v = (of v).convs (n - 1)
have succ : ∀ (n : ℕ) (IH : ∀ (nth_stream_eq_none : IntFractPair.stream v n = none), v = (of v).convs (n - 1))
  (nth_stream_eq_none : IntFractPair.stream v (n + 1) = none), v = (of v).convs (n + 1 - 1)
Tactic: induction n with
  | zero => contradiction
  -- IntFractPair.stream v 0 ≠ none
  | succ n IH =>
    let g := of v
    change v = g.convs n
    obtain ⟨nth_stream_eq_none⟩ | ⟨ifp_n, nth_stream_eq, nth_stream_fr_eq_zero⟩ :
      IntFractPair.stream v n = none ∨ ∃ ifp, IntFractPair.stream v n = some ifp ∧ ifp.fr = 0 :=
      IntFractPair.succ_nth_stream_eq_none_iff.1 nth_stream_eq_none
    · cases n with
      | zero => contradiction
      | succ n' =>
        -- IntFractPair.stream v 0 ≠ none
        have : g.TerminatedAt n' :=
          of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none.2
            nth_stream_eq_none
        have : g.convs (n' + 1) = g.convs n' :=
          convs_stable_of_terminated n'.le_succ this
        rw [this]
        exact IH nth_stream_eq_none
    · simpa [nth_stream_fr_eq_zero, compExactValue] using
        compExactValue_correctness_of_stream_eq_some nth_stream_eq
Cleared hypotheses: nth_stream_eq_none
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
inst_2 : FloorRing K
terminates : (of v).Terminates
⊢ ∀ᶠ (n : ℕ) in atTop, v = (of v).convs n
have rw : ∃ (a : ℕ), ∀ b ≥ a, v = (of v).convs b
Tactic: rw [eventually_atTop]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
inst_2 : FloorRing K
terminates : (of v).Terminates
⊢ ∃ (a : ℕ), ∀ b ≥ a, v = (of v).convs b
have obtain : ∀ (n : ℕ) (terminatedAt_n : (of v).TerminatedAt n), ∃ (a : ℕ), ∀ b ≥ a, v = (of v).convs b
Tactic: obtain ⟨n, terminatedAt_n⟩ : ∃ n, (of v).TerminatedAt n := terminates
Cleared hypotheses: terminates
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
inst_2 : FloorRing K
n : ℕ
terminatedAt_n : (of v).TerminatedAt n
⊢ ∃ (a : ℕ), ∀ b ≥ a, v = (of v).convs b
have h : ∀ b ≥ n, v = (of v).convs b
Tactic: use n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
inst_2 : FloorRing K
n : ℕ
terminatedAt_n : (of v).TerminatedAt n
m : ℕ
m_geq_n : m ≥ n
⊢ v = (of v).convs m
have h : v = (of v).convs n
Tactic: rw [convs_stable_of_terminated m_geq_n terminatedAt_n]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n, ∃ (conts : Pair ℚ), (of v).contsAux m = Pair.map Rat.cast conts
⊢ ∃ (conts : Pair ℚ), (of v).contsAux n = Pair.map Rat.cast conts
have zero : ∀ (IH : ∀ m < 0, ∃ (conts : Pair ℚ), (of v).contsAux m = Pair.map Rat.cast conts),
  ∃ (conts : Pair ℚ), (of v).contsAux 0 = Pair.map Rat.cast conts
Tactic: rcases n with (_ | _ | n)
Cleared hypotheses: n, IH