-- Mathlib/Algebra/ContinuedFractions/Determinant.lean
theorem determinant_aux (hyp : n = 0 ∨ ¬(↑s : GenContFract K).TerminatedAt (n - 1)) :
    ((↑s : GenContFract K).contsAux n).a * ((↑s : GenContFract K).contsAux (n + 1)).b -
      ((↑s : GenContFract K).contsAux n).b * ((↑s : GenContFract K).contsAux (n + 1)).a =
        (-1) ^ n

Proof state:
K : Type u_1
inst✝ : Field K
s : SimpContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬(↑s).TerminatedAt (n + 1 - 1)
g : GenContFract K := ↑s
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH : n = 0 ∨ ¬(↑s).TerminatedAt (n - 1) → ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = (-1) ^ n
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
not_terminated_at_n : ¬g.TerminatedAt n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
this : ppA * pB - ppB * pA = (-1) ^ n
pow_succ_n : (-1) ^ (n + 1) = -1 * (-1) ^ n
⊢ pA * ppB - pB * ppA = (-1) ^ (n + 1)

Tactic:
rw [pow_succ_n, ← this]

Result:
K : Type u_1
inst✝ : Field K
s : SimpContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬(↑s).TerminatedAt (n + 1 - 1)
g : GenContFract K := ↑s
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH : n = 0 ∨ ¬(↑s).TerminatedAt (n - 1) → ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = (-1) ^ n
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
not_terminated_at_n : ¬g.TerminatedAt n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
this : ppA * pB - ppB * pA = (-1) ^ n
pow_succ_n : (-1) ^ (n + 1) = -1 * (-1) ^ n
⊢ pA * ppB - pB * ppA = -1 * (ppA * pB - ppB * pA)

Proof state:
case succ.intro
K : Type u_1
inst✝ : Field K
s : SimpContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬(↑s).TerminatedAt (n + 1 - 1)
g : GenContFract K := ↑s
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH : n = 0 ∨ ¬(↑s).TerminatedAt (n - 1) → ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = (-1) ^ n
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
not_terminated_at_n : ¬g.TerminatedAt n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
⊢ ppA * pB - ppB * pA = (-1) ^ n

Tactic:
exact IH <| Or.inr <| mt (terminated_stable <| n.sub_le 1) not_terminated_at_n

Result:
no goals

Proof state:
case succ
K : Type u_1
inst✝ : Field K
s : SimpContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬(↑s).TerminatedAt (n + 1 - 1)
g : GenContFract K := ↑s
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH : n = 0 ∨ ¬(↑s).TerminatedAt (n - 1) → ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = (-1) ^ n
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
⊢ pred_conts.a * ((↑s).contsAux (n + 1 + 1)).b - pred_conts.b * ((↑s).contsAux (n + 1 + 1)).a = (-1) ^ (n + 1)

Tactic:
let ppA := ppred_conts.a

Result:
case succ
K : Type u_1
inst✝ : Field K
s : SimpContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬(↑s).TerminatedAt (n + 1 - 1)
g : GenContFract K := ↑s
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH : n = 0 ∨ ¬(↑s).TerminatedAt (n - 1) → ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = (-1) ^ n
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
⊢ pred_conts.a * ((↑s).contsAux (n + 1 + 1)).b - pred_conts.b * ((↑s).contsAux (n + 1 + 1)).a = (-1) ^ (n + 1)

Proof state:
K : Type u_1
inst✝ : Field K
s : SimpContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬(↑s).TerminatedAt (n + 1 - 1)
g : GenContFract K := ↑s
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH : n = 0 ∨ ¬(↑s).TerminatedAt (n - 1) → ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = (-1) ^ n
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
not_terminated_at_n : ¬g.TerminatedAt n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
this : ppA * pB - ppB * pA = (-1) ^ n
⊢ pA * ppB - pB * ppA = (-1) ^ (n + 1)

Tactic:
have pow_succ_n : (-1 : K) ^ (n + 1) = -1 * (-1) ^ n := pow_succ' (-1) n

Result:
K : Type u_1
inst✝ : Field K
s : SimpContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬(↑s).TerminatedAt (n + 1 - 1)
g : GenContFract K := ↑s
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH : n = 0 ∨ ¬(↑s).TerminatedAt (n - 1) → ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = (-1) ^ n
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
not_terminated_at_n : ¬g.TerminatedAt n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
this : ppA * pB - ppB * pA = (-1) ^ n
pow_succ_n : (-1) ^ (n + 1) = -1 * (-1) ^ n
⊢ pA * ppB - pB * ppA = (-1) ^ (n + 1)

Proof state:
case succ.intro
K : Type u_1
inst✝ : Field K
s : SimpContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬(↑s).TerminatedAt (n + 1 - 1)
g : GenContFract K := ↑s
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH : n = 0 ∨ ¬(↑s).TerminatedAt (n - 1) → ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = (-1) ^ n
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
not_terminated_at_n : ¬g.TerminatedAt n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
⊢ pA * ppB - pB * ppA = (-1) ^ (n + 1)

Tactic:
suffices ppA * pB - ppB * pA = (-1) ^ n by
  have pow_succ_n : (-1 : K) ^ (n + 1) = -1 * (-1) ^ n := pow_succ' (-1) n
  rw [pow_succ_n, ← this]
  ring

Result:
case succ.intro
K : Type u_1
inst✝ : Field K
s : SimpContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬(↑s).TerminatedAt (n + 1 - 1)
g : GenContFract K := ↑s
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH : n = 0 ∨ ¬(↑s).TerminatedAt (n - 1) → ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = (-1) ^ n
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
not_terminated_at_n : ¬g.TerminatedAt n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
⊢ ppA * pB - ppB * pA = (-1) ^ n

Proof state:
K : Type u_1
inst✝ : Field K
s : SimpContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬(↑s).TerminatedAt (n + 1 - 1)
g : GenContFract K := ↑s
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH : n = 0 ∨ ¬(↑s).TerminatedAt (n - 1) → ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = (-1) ^ n
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
not_terminated_at_n : ¬g.TerminatedAt n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
this : pA * ppB - pB * ppA = (-1) ^ (n + 1)
⊢ pA * ppB - pB * ppA = (-1) ^ (n + 1)

Tactic:
assumption

Result:
no goals