awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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
⊢ 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))
have 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))
Tactic: obtain (ifp_fr_eq_zero | ifp_fr_ne_zero) := eq_or_ne ifp.fr 0
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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))
⊢ 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))
have 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))
Tactic: obtain (ifp_fr_eq_zero | ifp_fr_ne_zero) := eq_or_ne ifp.fr 0
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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
⊢ 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))
have inl : v - g.convs n = 0
Tactic: suffices v - g.convs n = 0 by simpa [ifp_fr_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (hypothesis)
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 = 0
have g_finite_correctness₁ : 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
Cleared hypotheses: g_finite_correctness
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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
⊢ 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))
have inr : v - A / B = 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]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (hypothesis)
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 - A / B = HPow.hPow (α := K) (-1) n / (B * (ifp.fr⁻¹ * B + pB))
have g_finite_correctness₁ : 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
Cleared hypotheses: g_finite_correctness
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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)
⊢ v - A / B = HPow.hPow (α := K) (-1) n / (B * (ifp.fr⁻¹ * B + pB))
have inr : (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B) - 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]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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)
have 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)
Tactic: rcases n with - | n'
Cleared hypotheses: n, stream_nth_eq, conts, pred_conts, A, B, pA, pB, g_finite_correctness
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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)
⊢ n = 0 ∨ ¬g.TerminatedAt (n - 1)
have 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)
Tactic: rcases n with - | n'
Cleared hypotheses: n, stream_nth_eq, conts, pred_conts, A, B, pA, pB, g_finite_correctness
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (hypothesis)
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)
⊢ n' + 1 = 0 ∨ ¬g.TerminatedAt (n' + 1 - 1)
have this : IntFractPair.stream v (n' + 1) ≠ none
Tactic: have : IntFractPair.stream v (n' + 1) ≠ none := by simp [stream_nth_eq]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (hypothesis)
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
⊢ n' + 1 = 0 ∨ ¬g.TerminatedAt (n' + 1 - 1)
have this₁ : ¬g.TerminatedAt n'
Tactic: have : ¬g.TerminatedAt n' :=
          (not_congr of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none).2 this
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (hypothesis)
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)
⊢ (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B) - A / B = HPow.hPow (α := K) (-1) n / (B * (ifp.fr⁻¹ * B + pB))
have n_eq_zero_or_not_terminatedAt_pred_n : 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
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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
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)
stream_nth_eq : IntFractPair.stream v 0 = some ifp
n_eq_zero_or_not_terminatedAt_pred_n : Eq (α := ℕ) 0 0 ∨ ¬g.TerminatedAt (HSub.hSub (α := ℕ) 0 1)
hn : n = 0
⊢ pA * B - pB * A = HPow.hPow (α := K) (β := ℕ) (-1) 0
have subst : 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)),
  pA * B - pB * A = HPow.hPow (α := K) (β := ℕ) (-1) 0
Tactic: subst n
Cleared hypotheses: n, conts, pred_conts, A, B, pA, pB, g_finite_correctness, hn
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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
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' : ℕ
stream_nth_eq : IntFractPair.stream v (n' + 1) = some ifp
n_eq_zero_or_not_terminatedAt_pred_n : n' + 1 = 0 ∨ ¬g.TerminatedAt (n' + 1 - 1)
hn : n = n'.succ
⊢ pA * B - pB * A = HPow.hPow (α := K) (-1) (n' + 1)
have subst : let conts := g.contsAux (n'.succ + 1);
let pred_conts := g.contsAux n'.succ;
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)),
  pA * B - pB * A = HPow.hPow (α := K) (-1) (n' + 1)
Tactic: subst n
Cleared hypotheses: n, conts, pred_conts, A, B, pA, pB, g_finite_correctness, hn
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (hypothesis)
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
n_eq_zero_or_not_terminatedAt_pred_n : n' + 1 = 0 ∨ ¬g.TerminatedAt (n' + 1 - 1)
conts : Pair K := g.contsAux (n'.succ + 1)
pred_conts : Pair K := g.contsAux n'.succ
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)
⊢ pA * B - pB * A = HPow.hPow (α := K) (-1) (n' + 1)
have n_eq_zero_or_not_terminatedAt_pred_n₁ : ¬g.TerminatedAt (n' + 1 - 1)
Tactic: simp only [succ_ne_zero, false_or] at n_eq_zero_or_not_terminatedAt_pred_n
Cleared hypotheses: n_eq_zero_or_not_terminatedAt_pred_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (hypothesis)
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'.succ + 1)
pred_conts : Pair K := g.contsAux n'.succ
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_eq_zero_or_not_terminatedAt_pred_n : ¬g.TerminatedAt (n' + 1 - 1)
⊢ pA * B - pB * A = HPow.hPow (α := K) (-1) (n' + 1)
have n_eq_zero_or_not_terminatedAt_pred_n₁ : ¬g.TerminatedAt n'
Tactic: rw [add_tsub_cancel_right] at n_eq_zero_or_not_terminatedAt_pred_n
Cleared hypotheses: n_eq_zero_or_not_terminatedAt_pred_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (hypothesis)
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_eq_zero_or_not_terminatedAt_pred_n : n = 0 ∨ ¬g.TerminatedAt (n - 1)
⊢ (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B) - A / B = HPow.hPow (α := K) (-1) n / (B * (ifp.fr⁻¹ * B + pB))
have determinant_eq : pA * B - pB * A = HPow.hPow (α := K) (-1) n
Tactic: have determinant_eq : pA * B - pB * A = (-1) ^ n := by
      match hn : n with
      | 0 => subst n; simp [pA, pB, A, B, pred_conts, conts]
      | n' + 1 =>
        subst n
        simp only [succ_ne_zero, false_or] at n_eq_zero_or_not_terminatedAt_pred_n
        rw [add_tsub_cancel_right] at n_eq_zero_or_not_terminatedAt_pred_n
        exact (SimpContFract.of v).determinant n_eq_zero_or_not_terminatedAt_pred_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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_eq_zero_or_not_terminatedAt_pred_n : n = 0 ∨ ¬g.TerminatedAt (n - 1)
determinant_eq : pA * B - pB * A = HPow.hPow (α := K) (-1) n
⊢ n ≤ 1 ∨ ¬g.TerminatedAt (n - 2)
have inl : ∀ (n_eq_zero : n = 0), n ≤ 1 ∨ ¬g.TerminatedAt (n - 2)
Tactic: rcases n_eq_zero_or_not_terminatedAt_pred_n with n_eq_zero | not_terminatedAt_pred_n
Cleared hypotheses: n_eq_zero_or_not_terminatedAt_pred_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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_eq_zero_or_not_terminatedAt_pred_n : n = 0 ∨ ¬g.TerminatedAt (n - 1)
determinant_eq : pA * B - pB * A = HPow.hPow (α := K) (-1) n
inl : ∀ (n_eq_zero : n = 0), n ≤ 1 ∨ ¬g.TerminatedAt (n - 2)
⊢ n ≤ 1 ∨ ¬g.TerminatedAt (n - 2)
have inr : ∀ (not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)), n ≤ 1 ∨ ¬g.TerminatedAt (n - 2)
Tactic: rcases n_eq_zero_or_not_terminatedAt_pred_n with n_eq_zero | not_terminatedAt_pred_n
Cleared hypotheses: n_eq_zero_or_not_terminatedAt_pred_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (hypothesis)
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_eq_zero_or_not_terminatedAt_pred_n : n = 0 ∨ ¬g.TerminatedAt (n - 1)
determinant_eq : pA * B - pB * A = HPow.hPow (α := K) (-1) n
⊢ (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B) - A / B = HPow.hPow (α := K) (-1) n / (B * (ifp.fr⁻¹ * B + pB))
have pB_ineq : (↑(fib n) : K) ≤ pB
Tactic: have pB_ineq : (fib n : K) ≤ pB :=
      haveI : n ≤ 1 ∨ ¬g.TerminatedAt (n - 2) := by
        rcases n_eq_zero_or_not_terminatedAt_pred_n with n_eq_zero | not_terminatedAt_pred_n
        · simp [n_eq_zero]
        · exact Or.inr <| mt (terminated_stable (n - 1).pred_le) not_terminatedAt_pred_n
      fib_le_of_contsAux_b this
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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_eq_zero_or_not_terminatedAt_pred_n : n = 0 ∨ ¬g.TerminatedAt (n - 1)
determinant_eq : pA * B - pB * A = HPow.hPow (α := K) (-1) n
pB_ineq : (↑(fib n) : K) ≤ pB
⊢ n + 1 ≤ 1 ∨ ¬g.TerminatedAt (n + 1 - 2)
have inl : ∀ (n_eq_zero : n = 0), n + 1 ≤ 1 ∨ ¬g.TerminatedAt (n + 1 - 2)
Tactic: rcases n_eq_zero_or_not_terminatedAt_pred_n with n_eq_zero | not_terminatedAt_pred_n
Cleared hypotheses: n_eq_zero_or_not_terminatedAt_pred_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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_eq_zero_or_not_terminatedAt_pred_n : n = 0 ∨ ¬g.TerminatedAt (n - 1)
determinant_eq : pA * B - pB * A = HPow.hPow (α := K) (-1) n
pB_ineq : (↑(fib n) : K) ≤ pB
inl : ∀ (n_eq_zero : n = 0), n + 1 ≤ 1 ∨ ¬g.TerminatedAt (n + 1 - 2)
⊢ n + 1 ≤ 1 ∨ ¬g.TerminatedAt (n + 1 - 2)
have inr : ∀ (not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)), n + 1 ≤ 1 ∨ ¬g.TerminatedAt (n + 1 - 2)
Tactic: rcases n_eq_zero_or_not_terminatedAt_pred_n with n_eq_zero | not_terminatedAt_pred_n
Cleared hypotheses: n_eq_zero_or_not_terminatedAt_pred_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (hypothesis)
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_eq_zero_or_not_terminatedAt_pred_n : n = 0 ∨ ¬g.TerminatedAt (n - 1)
determinant_eq : pA * B - pB * A = HPow.hPow (α := K) (-1) n
pB_ineq : (↑(fib n) : K) ≤ pB
⊢ (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B) - A / B = HPow.hPow (α := K) (-1) n / (B * (ifp.fr⁻¹ * B + pB))
have B_ineq : (↑(fib (n + 1)) : K) ≤ B
Tactic: have B_ineq : (fib (n + 1) : K) ≤ B :=
      haveI : n + 1 ≤ 1 ∨ ¬g.TerminatedAt (n + 1 - 2) := by
        rcases n_eq_zero_or_not_terminatedAt_pred_n with n_eq_zero | not_terminatedAt_pred_n
        · simp [n_eq_zero]
        · exact Or.inr not_terminatedAt_pred_n
      fib_le_of_contsAux_b this