awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
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⁻¹
⊢ ((↑⌊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
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
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)
succ :
  (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
⊢ (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB) = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr

Tactic:
dsimp only [conts, pconts, ppconts]
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
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)
⊢ (IntFractPair.of (1 / ifp_n.fr)).fr = f

Tactic:
have hfr : (IntFractPair.of (1 / ifp_n.fr)).fr = f := rfl
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
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
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)
⊢ (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

Tactic:
simp [compExactValue, contsAux_recurrence s_nth_eq ppconts_eq pconts_eq,
        nextConts, nextNum, nextDen]

Premises used: GenContFract.nextDen, GenContFract.nextConts, GenContFract.compExactValue, GenContFract.nextNum, GenContFract.contsAux_recurrence
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
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) =
    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:
grind
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
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 0 = none
⊢ v = (of v).convs (HSub.hSub (α := ℕ) 0 1)

Tactic:
contradiction
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
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 : v = g.convs n
⊢ v = (of v).convs (n + 1 - 1)

Tactic:
change v = g.convs n

Premises used: GenContFract.convs
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
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
⊢ IntFractPair.stream v n = none ∨ ∃ (ifp : IntFractPair K), IntFractPair.stream v n = some ifp ∧ ifp.fr = 0

Tactic:
IntFractPair.succ_nth_stream_eq_none_iff.1 nth_stream_eq_none

Premises used: GenContFract.IntFractPair.succ_nth_stream_eq_none_iff, Iff.mp
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
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
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
⊢ 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

Premises used: GenContFract.IntFractPair.stream, GenContFract.IntFractPair.succ_nth_stream_eq_none_iff, Option.none, Iff.mp
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n : ℕ
inst_2 : FloorRing K
g : GenContFract K := of v
IH : ∀ (nth_stream_eq_none : IntFractPair.stream v 0 = none), v = (of v).convs (HSub.hSub (α := ℕ) 0 1)
nth_stream_eq_none_1 : IntFractPair.stream v (HAdd.hAdd (α := ℕ) 0 1) = none
nth_stream_eq_none : IntFractPair.stream v 0 = none
⊢ v = g.convs 0

Tactic:
contradiction
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
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
⊢ g.TerminatedAt n'

Tactic:
have : g.TerminatedAt n' :=
          of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none.2
            nth_stream_eq_none
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
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'
⊢ g.convs (n' + 1) = g.convs n'

Tactic:
have : g.convs (n' + 1) = g.convs n' :=
          convs_stable_of_terminated n'.le_succ this
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
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'
succ : v = g.convs n'
⊢ v = g.convs (n' + 1)

Tactic:
rw [this]
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
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'

Tactic:
IH nth_stream_eq_none

Premises used: Nat.pred
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
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'

Tactic:
exact IH nth_stream_eq_none
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
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
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)
⊢ v = g.convs n

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
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
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
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:
simpa [nth_stream_fr_eq_zero, compExactValue] using
        compExactValue_correctness_of_stream_eq_some nth_stream_eq

Premises used: GenContFract.compExactValue_correctness_of_stream_eq_some, GenContFract.compExactValue
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
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)
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)
⊢ v = (of v).convs (n - 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

Premises used: GenContFract.IntFractPair.stream, GenContFract.IntFractPair.succ_nth_stream_eq_none_iff, Option.none, Iff.mp, GenContFract.compExactValue
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
n : ℕ
inst_2 : FloorRing K
terminatedAt_n : (of v).TerminatedAt n
⊢ v = (of v).convs n

Tactic:
have : IntFractPair.stream v (n + 1) = none :=
    of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none.1 terminatedAt_n
  of_correctness_of_nth_stream_eq_none this

Premises used: GenContFract.of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none, Iff.mp, GenContFract.of_correctness_of_nth_stream_eq_none, Nat.pred
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
inst_2 : FloorRing K
terminates : (of v).Terminates
⊢ ∃ (n : ℕ), v = (of v).convs n

Tactic:
Exists.elim terminates fun n terminatedAt_n =>
    Exists.intro n (of_correctness_of_terminatedAt terminatedAt_n)

Premises used: Exists.intro, GenContFract.of_correctness_of_terminatedAt, Exists.elim
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
inst_2 : FloorRing K
terminates : (of v).Terminates
rw : ∃ (a : ℕ), ∀ b ≥ a, v = (of v).convs b
⊢ ∀ᶠ (n : ℕ) in atTop, v = (of v).convs n

Tactic:
rw [eventually_atTop]

Premises used: Filter.eventually_atTop
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
inst_2 : FloorRing K
terminates : (of v).Terminates
⊢ ∃ (n : ℕ), (of v).TerminatedAt n

Tactic:
terminates

Premises used: Stream'.Seq.Terminates, GenContFract.Terminates, GenContFract.TerminatedAt
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
v : K
inst_2 : FloorRing K
terminates : (of v).Terminates
obtain : ∀ (n : ℕ) (terminatedAt_n : (of v).TerminatedAt n), ∃ (a : ℕ), ∀ b ≥ a, v = (of v).convs b
⊢ ∃ (a : ℕ), ∀ b ≥ a, v = (of v).convs b

Tactic:
obtain ⟨n, terminatedAt_n⟩ : ∃ n, (of v).TerminatedAt n := terminates
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
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
h : ∀ b ≥ n, v = (of v).convs b
⊢ ∃ (a : ℕ), ∀ b ≥ a, v = (of v).convs b

Tactic:
use n
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
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
h : v = (of v).convs n
⊢ v = (of v).convs m

Tactic:
rw [convs_stable_of_terminated m_geq_n terminatedAt_n]

Premises used: GenContFract.convs_stable_of_terminated
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
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 n

Tactic:
of_correctness_of_terminatedAt terminatedAt_n

Premises used: GenContFract.of_correctness_of_terminatedAt
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
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 n

Tactic:
exact of_correctness_of_terminatedAt terminatedAt_n

Premises used: GenContFract.of_correctness_of_terminatedAt
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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
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
succ :
  ∀ (IH : ∀ m < HAdd.hAdd (α := ℕ) 0 1, ∃ (conts : Pair ℚ), (of v).contsAux m = Pair.map Rat.cast conts),
    ∃ (conts : Pair ℚ), (of v).contsAux (HAdd.hAdd (α := ℕ) 0 1) = Pair.map Rat.cast conts
succ₁ :
  ∀ (n : ℕ) (IH : ∀ m < n + 1 + 1, ∃ (conts : Pair ℚ), (of v).contsAux m = Pair.map Rat.cast conts),
    ∃ (conts : Pair ℚ), (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts
⊢ ∃ (conts : Pair ℚ), (of v).contsAux n = Pair.map Rat.cast conts

Tactic:
rcases n with (_ | _ | n)
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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
IH : ∀ m < 0, ∃ (conts : Pair ℚ), (of v).contsAux m = Pair.map Rat.cast conts
this : ∃ (gp : Pair ℚ), Eq.{u_1 + 1} (α := Pair K) { a := 1, b := 0 } (Pair.map Rat.cast gp)
⊢ ∃ (conts : Pair ℚ), (of v).contsAux 0 = Pair.map Rat.cast conts

Tactic:
simpa [contsAux]

Premises used: GenContFract.contsAux
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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
IH : ∀ m < 0, ∃ (conts : Pair ℚ), (of v).contsAux m = Pair.map Rat.cast conts
zero : ∃ (gp : Pair ℚ), Eq.{u_1 + 1} (α := Pair K) { a := 1, b := 0 } (Pair.map Rat.cast gp)
⊢ ∃ (conts : Pair ℚ), (of v).contsAux 0 = Pair.map Rat.cast conts

Tactic:
suffices ∃ gp : Pair ℚ, Pair.mk (1 : K) 0 = gp.map (↑) by simpa [contsAux]