awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
g : GenContFract K := of v
inl : ∀ (terminated : g.partDens.TerminatedAt n), (of v).dens n ≤ (of v).dens (n + 1)
inr : ∀ (not_terminated : ¬g.partDens.TerminatedAt n), (of v).dens n ≤ (of v).dens (n + 1)
⊢ (of v).dens n ≤ (of v).dens (n + 1)

Tactic:
rcases Decidable.em <| g.partDens.TerminatedAt n with terminated | not_terminated

Premises used: Stream'.Seq.TerminatedAt, Decidable.em, GenContFract.partDens
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
g : GenContFract K := of v
terminated : g.partDens.TerminatedAt n
rwa rwa₁ rwa₂ rwa₃ : ∀ (terminated : g.partDens.get? n = none), g.partDens.get? n = none
⊢ g.partDens.get? n = none

Tactic:
rwa [Stream'.Seq.TerminatedAt] at terminated

Premises used: Stream'.Seq.TerminatedAt
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
g : GenContFract K := of v
terminated : g.partDens.TerminatedAt n
⊢ g.partDens.get? n = none

Tactic:
have : g.partDens.get? n = none := by rwa [Stream'.Seq.TerminatedAt] at terminated
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
g : GenContFract K := of v
terminated : g.partDens.TerminatedAt n
this : g.partDens.get? n = none
rwa rwa₁ rwa₂ rwa₃ : ∀ (terminated this : g.partDens.get? n = none), g.partDens.get? n = none
⊢ g.partDens.get? n = none

Tactic:
rwa [Stream'.Seq.TerminatedAt] at terminated

Premises used: Stream'.Seq.TerminatedAt
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
g : GenContFract K := of v
terminated : g.partDens.TerminatedAt n
this : g.partDens.get? n = none
⊢ g.TerminatedAt n

Tactic:
have : g.TerminatedAt n :=
      terminatedAt_iff_partDen_none.2 (by rwa [Stream'.Seq.TerminatedAt] at terminated)
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
g : GenContFract K := of v
terminated : g.partDens.TerminatedAt n
this_1 : g.partDens.get? n = none
this : g.TerminatedAt n
⊢ g.dens (n + 1) = g.dens n

Tactic:
have : g.dens (n + 1) = g.dens n :=
      dens_stable_of_terminated n.le_succ this
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
g : GenContFract K := of v
terminated : g.partDens.TerminatedAt n
this_1 : g.partDens.get? n = none
this_2 : g.TerminatedAt n
this : g.dens (n + 1) = g.dens n
inl inl₁ : (of v).dens n ≤ (of v).dens n
⊢ (of v).dens n ≤ (of v).dens (n + 1)

Tactic:
rw [this]
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
g : GenContFract K := of v
not_terminated : ¬g.partDens.TerminatedAt n
⊢ ∃ (b : K), g.partDens.get? n = some b

Tactic:
Option.ne_none_iff_exists'.mp not_terminated

Premises used: Option.ne_none_iff_exists', Iff.mp
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
g : GenContFract K := of v
not_terminated : ¬g.partDens.TerminatedAt n
inr : ∀ (b : K) (nth_partDen_eq : g.partDens.get? n = some b), (of v).dens n ≤ (of v).dens (n + 1)
⊢ (of v).dens n ≤ (of v).dens (n + 1)

Tactic:
obtain ⟨b, nth_partDen_eq⟩ : ∃ b, g.partDens.get? n = some b :=
      Option.ne_none_iff_exists'.mp not_terminated

Premises used: Option.ne_none_iff_exists', Iff.mp, GenContFract.partDens, Stream'.Seq.get?
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
g : GenContFract K := of v
not_terminated : ¬g.partDens.TerminatedAt n
b : K
nth_partDen_eq : g.partDens.get? n = some b
⊢ 1 ≤ b

Tactic:
have : 1 ≤ b := of_one_le_get?_partDen nth_partDen_eq
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
g : GenContFract K := of v
not_terminated : ¬g.partDens.TerminatedAt n
b : K
nth_partDen_eq : g.partDens.get? n = some b
this : 1 ≤ b
⊢ g.dens n ≤ b * g.dens n

Tactic:
simpa using mul_le_mul_of_nonneg_right this zero_le_of_den

Premises used: GenContFract.zero_le_of_den, mul_le_mul_of_nonneg_right
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
g : GenContFract K := of v
not_terminated : ¬g.partDens.TerminatedAt n
b : K
nth_partDen_eq : g.partDens.get? n = some b
this : 1 ≤ b
⊢ b * g.dens n ≤ g.dens (n + 1)

Tactic:
le_of_succ_get?_den nth_partDen_eq

Premises used: GenContFract.le_of_succ_get?_den
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
g : GenContFract K := of v
not_terminated : ¬g.partDens.TerminatedAt n
b : K
nth_partDen_eq : g.partDens.get? n = some b
this : 1 ≤ b
n₁ : g.dens n ≤ b * g.dens n
⊢ (of v).dens n ≤ (of v).dens (n + 1)

Tactic:
calc
      g.dens n ≤ b * g.dens n := by
        simpa using mul_le_mul_of_nonneg_right this zero_le_of_den
      _ ≤ g.dens (n + 1) := le_of_succ_get?_den nth_partDen_eq

Premises used: GenContFract.dens, HAdd.hAdd, GenContFract.le_of_succ_get?_den, OfNat.ofNat
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
⊢ v = GenContFract.compExactValue pred_conts conts ifp.fr

Tactic:
have g_finite_correctness :
    v = GenContFract.compExactValue pred_conts conts ifp.fr :=
    compExactValue_correctness_of_stream_eq_some stream_nth_eq
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
g_finite_correctness : v = GenContFract.compExactValue pred_conts conts ifp.fr
inl :
  ∀ (ifp_fr_eq_zero : ifp.fr = 0),
    let g := of v;
    let B := (g.contsAux (n + 1)).b;
    let pB := (g.contsAux n).b;
    v - g.convs n = if ifp.fr = 0 then 0 else HPow.hPow (α := K) (-1) n / (B * (ifp.fr⁻¹ * B + pB))
inr :
  ∀ (ifp_fr_ne_zero : ifp.fr ≠ 0),
    let g := of v;
    let B := (g.contsAux (n + 1)).b;
    let pB := (g.contsAux n).b;
    v - g.convs n = if ifp.fr = 0 then 0 else HPow.hPow (α := K) (-1) n / (B * (ifp.fr⁻¹ * B + pB))
⊢ let g := of v;
  let B := (g.contsAux (n + 1)).b;
  let pB := (g.contsAux n).b;
  v - g.convs n = if ifp.fr = 0 then 0 else HPow.hPow (α := K) (-1) n / (B * (ifp.fr⁻¹ * B + pB))

Tactic:
obtain (ifp_fr_eq_zero | ifp_fr_ne_zero) := eq_or_ne ifp.fr 0

Premises used: GenContFract.IntFractPair.fr, eq_or_ne, OfNat.ofNat
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
g_finite_correctness : v = GenContFract.compExactValue pred_conts conts ifp.fr
ifp_fr_eq_zero : ifp.fr = 0
this : v - g.convs n = 0
⊢ let g := of v;
  let B := (g.contsAux (n + 1)).b;
  let pB := (g.contsAux n).b;
  v - g.convs n = if ifp.fr = 0 then 0 else HPow.hPow (α := K) (-1) n / (B * (ifp.fr⁻¹ * B + pB))

Tactic:
simpa [ifp_fr_eq_zero]
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
g_finite_correctness : v = GenContFract.compExactValue pred_conts conts ifp.fr
ifp_fr_eq_zero : ifp.fr = 0
inl : v - g.convs n = 0
⊢ let g := of v;
  let B := (g.contsAux (n + 1)).b;
  let pB := (g.contsAux n).b;
  v - g.convs n = if ifp.fr = 0 then 0 else HPow.hPow (α := K) (-1) n / (B * (ifp.fr⁻¹ * B + pB))

Tactic:
suffices v - g.convs n = 0 by simpa [ifp_fr_eq_zero]
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
g_finite_correctness : v = GenContFract.compExactValue pred_conts conts ifp.fr
ifp_fr_eq_zero : ifp.fr = 0
⊢ v = g.convs n

Tactic:
simpa [GenContFract.compExactValue, ifp_fr_eq_zero] using g_finite_correctness

Premises used: GenContFract.compExactValue
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
g_finite_correctness : v = GenContFract.compExactValue pred_conts conts ifp.fr
ifp_fr_eq_zero : ifp.fr = 0
⊢ v = g.convs n

Tactic:
replace g_finite_correctness : v = g.convs n := by
      simpa [GenContFract.compExactValue, ifp_fr_eq_zero] using g_finite_correctness
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_eq_zero : ifp.fr = 0
g_finite_correctness : v = g.convs n
⊢ v - g.convs n = 0

Tactic:
sub_eq_zero.2 g_finite_correctness

Premises used: Iff.mpr, sub_eq_zero
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_eq_zero : ifp.fr = 0
g_finite_correctness : v = g.convs n
⊢ v - g.convs n = 0

Tactic:
exact sub_eq_zero.2 g_finite_correctness

Premises used: Iff.mpr, sub_eq_zero
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
g_finite_correctness : v = GenContFract.compExactValue pred_conts conts ifp.fr
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
this : v - A / B = HPow.hPow (α := K) (-1) n / (B * (ifp.fr⁻¹ * B + pB))
⊢ let g := of v;
  let B := (g.contsAux (n + 1)).b;
  let pB := (g.contsAux n).b;
  v - g.convs n = if ifp.fr = 0 then 0 else HPow.hPow (α := K) (-1) n / (B * (ifp.fr⁻¹ * B + pB))

Tactic:
simpa [ifp_fr_ne_zero]
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
g_finite_correctness : v = GenContFract.compExactValue pred_conts conts ifp.fr
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
inr : v - A / B = HPow.hPow (α := K) (-1) n / (B * (ifp.fr⁻¹ * B + pB))
⊢ let g := of v;
  let B := (g.contsAux (n + 1)).b;
  let pB := (g.contsAux n).b;
  v - g.convs n = if ifp.fr = 0 then 0 else HPow.hPow (α := K) (-1) n / (B * (ifp.fr⁻¹ * B + pB))

Tactic:
suffices v - A / B = (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB)) by simpa [ifp_fr_ne_zero]
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
g_finite_correctness : v = GenContFract.compExactValue pred_conts conts ifp.fr
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
⊢ v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)

Tactic:
simpa [GenContFract.compExactValue, ifp_fr_ne_zero, nextConts, nextNum, nextDen, add_comm]
        using g_finite_correctness

Premises used: GenContFract.nextDen, add_comm, GenContFract.nextConts, GenContFract.compExactValue, GenContFract.nextNum
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
g_finite_correctness : v = GenContFract.compExactValue pred_conts conts ifp.fr
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
⊢ v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)

Tactic:
replace g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B) := by
      simpa [GenContFract.compExactValue, ifp_fr_ne_zero, nextConts, nextNum, nextDen, add_comm]
        using g_finite_correctness
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
this : (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B) - A / B = HPow.hPow (α := K) (-1) n / (B * (ifp.fr⁻¹ * B + pB))
rwa rwa₁ rwa₂ rwa₃ :
  (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B) - A / B = HPow.hPow (α := K) (-1) n / (B * (ifp.fr⁻¹ * B + pB))
⊢ v - A / B = HPow.hPow (α := K) (-1) n / (B * (ifp.fr⁻¹ * B + pB))

Tactic:
rwa [g_finite_correctness]
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
inr : (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B) - A / B = HPow.hPow (α := K) (-1) n / (B * (ifp.fr⁻¹ * B + pB))
⊢ v - A / B = HPow.hPow (α := K) (-1) n / (B * (ifp.fr⁻¹ * B + pB))

Tactic:
suffices
      (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B) - A / B = (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB)) by
      rwa [g_finite_correctness]
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
zero :
  ∀ (stream_nth_eq : IntFractPair.stream v 0 = some ifp),
    let conts := g.contsAux (HAdd.hAdd (α := ℕ) 0 1);
    let pred_conts := g.contsAux 0;
    let A := conts.a;
    let B := conts.b;
    let pA := pred_conts.a;
    let pB := pred_conts.b;
    ∀ (g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)),
      Eq (α := ℕ) 0 0 ∨ ¬g.TerminatedAt (HSub.hSub (α := ℕ) 0 1)
succ :
  ∀ (n' : ℕ) (stream_nth_eq : IntFractPair.stream v (n' + 1) = some ifp),
    let conts := g.contsAux (n' + 1 + 1);
    let pred_conts := g.contsAux (n' + 1);
    let A := conts.a;
    let B := conts.b;
    let pA := pred_conts.a;
    let pB := pred_conts.b;
    ∀ (g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)), n' + 1 = 0 ∨ ¬g.TerminatedAt (n' + 1 - 1)
⊢ n = 0 ∨ ¬g.TerminatedAt (n - 1)

Tactic:
rcases n with - | n'
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
ifp : IntFractPair K
g : GenContFract K := of v
ifp_fr_ne_zero : ifp.fr ≠ 0
stream_nth_eq : IntFractPair.stream v 0 = some ifp
conts : Pair K := g.contsAux (HAdd.hAdd (α := ℕ) 0 1)
pred_conts : Pair K := g.contsAux 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
⊢ Eq (α := ℕ) 0 0 ∨ ¬g.TerminatedAt (HSub.hSub (α := ℕ) 0 1)

Tactic:
simp
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
ifp : IntFractPair K
g : GenContFract K := of v
ifp_fr_ne_zero : ifp.fr ≠ 0
n' : ℕ
stream_nth_eq : IntFractPair.stream v (n' + 1) = some ifp
conts : Pair K := g.contsAux (n' + 1 + 1)
pred_conts : Pair K := g.contsAux (n' + 1)
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
⊢ IntFractPair.stream v (n' + 1) ≠ none

Tactic:
simp [stream_nth_eq]
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
ifp : IntFractPair K
g : GenContFract K := of v
ifp_fr_ne_zero : ifp.fr ≠ 0
n' : ℕ
stream_nth_eq : IntFractPair.stream v (n' + 1) = some ifp
conts : Pair K := g.contsAux (n' + 1 + 1)
pred_conts : Pair K := g.contsAux (n' + 1)
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
⊢ IntFractPair.stream v (n' + 1) ≠ none

Tactic:
have : IntFractPair.stream v (n' + 1) ≠ none := by simp [stream_nth_eq]
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
ifp : IntFractPair K
g : GenContFract K := of v
ifp_fr_ne_zero : ifp.fr ≠ 0
n' : ℕ
stream_nth_eq : IntFractPair.stream v (n' + 1) = some ifp
conts : Pair K := g.contsAux (n' + 1 + 1)
pred_conts : Pair K := g.contsAux (n' + 1)
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
this : IntFractPair.stream v (n' + 1) ≠ none
⊢ ¬g.TerminatedAt n'

Tactic:
have : ¬g.TerminatedAt n' :=
          (not_congr of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none).2 this
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
ifp : IntFractPair K
g : GenContFract K := of v
ifp_fr_ne_zero : ifp.fr ≠ 0
n' : ℕ
stream_nth_eq : IntFractPair.stream v (n' + 1) = some ifp
conts : Pair K := g.contsAux (n' + 1 + 1)
pred_conts : Pair K := g.contsAux (n' + 1)
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
this_1 : IntFractPair.stream v (n' + 1) ≠ none
this : ¬g.TerminatedAt n'
⊢ n' + 1 = 0 ∨ ¬g.TerminatedAt (n' + 1 - 1)

Tactic:
Or.inr this

Premises used: Or.inr
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
ifp : IntFractPair K
g : GenContFract K := of v
ifp_fr_ne_zero : ifp.fr ≠ 0
n' : ℕ
stream_nth_eq : IntFractPair.stream v (n' + 1) = some ifp
conts : Pair K := g.contsAux (n' + 1 + 1)
pred_conts : Pair K := g.contsAux (n' + 1)
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
this_1 : IntFractPair.stream v (n' + 1) ≠ none
this : ¬g.TerminatedAt n'
⊢ n' + 1 = 0 ∨ ¬g.TerminatedAt (n' + 1 - 1)

Tactic:
exact Or.inr this

Premises used: Or.inr
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
⊢ n = 0 ∨ ¬g.TerminatedAt (n - 1)

Tactic:
have n_eq_zero_or_not_terminatedAt_pred_n : n = 0 ∨ ¬g.TerminatedAt (n - 1) := by
      rcases n with - | n'
      · simp
      · have : IntFractPair.stream v (n' + 1) ≠ none := by simp [stream_nth_eq]
        have : ¬g.TerminatedAt n' :=
          (not_congr of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none).2 this
        exact Or.inr this