-- Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean
theorem sub_convs_eq {ifp : IntFractPair K}
    (stream_nth_eq : IntFractPair.stream v n = some ifp) :
    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 (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))

Proof state:
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : 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)
⊢ 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 (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))

Tactic:
let pred_conts := g.contsAux n

Result:
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : 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
⊢ 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 (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))

Proof state:
case inl
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : 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

Tactic:
replace g_finite_correctness : v = g.convs n := by
  simpa [GenContFract.compExactValue, ifp_fr_eq_zero] using g_finite_correctness

Result:
case inl
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : 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

Proof state:
case succ
K : Type u_1
v : K
inst✝¹ : LinearOrderedField K
inst✝ : 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
this : ¬g.TerminatedAt n'
⊢ n' + 1 = 0 ∨ ¬g.TerminatedAt (n' + 1 - 1)

Tactic:
exact Or.inr this

Result:
no goals

Proof state:
case inl
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : 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

Result:
no goals

Proof state:
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : 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 = (-1) ^ n
pB_ineq : ↑(fib n) ≤ pB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
this✝¹ : 0 ≤ pB
this✝ : 0 < ifp.fr
this : pB + ifp.fr⁻¹ * B ≠ 0
⊢ (pA * B + ifp.fr⁻¹ * A * B - (pB + ifp.fr⁻¹ * B) * A) / ((pB + ifp.fr⁻¹ * B) * B) =
    (pA * B + ifp.fr⁻¹ * A * B - (pB * A + ifp.fr⁻¹ * B * A)) / ?m.70620

Tactic:
rw [add_mul]

Result:
no goals

Proof state:
case inr
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : 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 = (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))

Tactic:
have determinant_eq : pA * B - pB * A = (-1) ^ n :=
  (SimpContFract.of v).determinant_aux n_eq_zero_or_not_terminatedAt_pred_n

Result:
case inr
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : 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 = (-1) ^ n
⊢ (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B) - A / B = (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))

Proof state:
K : Type u_1
v : K
inst✝¹ : LinearOrderedField K
inst✝ : 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]

Result:
no goals

Proof state:
case inr
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : 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 = (-1) ^ n
pB_ineq : ↑(fib n) ≤ pB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
this✝ : 0 ≤ pB
this : 0 < ifp.fr
⊢ (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B) - A / B = (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))

Tactic:
have : pB + ifp.fr⁻¹ * B ≠ 0 := by positivity

Result:
case inr
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : 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 = (-1) ^ n
pB_ineq : ↑(fib n) ≤ pB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
this✝¹ : 0 ≤ pB
this✝ : 0 < ifp.fr
this : pB + ifp.fr⁻¹ * B ≠ 0
⊢ (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B) - A / B = (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))