-- Mathlib/Algebra/ContinuedFractions/TerminatedStable.lean
theorem convs'Aux_stable_step_of_terminated {s : Stream'.Seq <| Pair K}
    (terminatedAt_n : s.TerminatedAt n) : convs'Aux s (n + 1) = convs'Aux s n

Proof state:
K : Type u_1
n : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
terminatedAt_n : s.TerminatedAt n
⊢ convs'Aux s (n + 1) = convs'Aux s n

Tactic:
change s.get? n = none at terminatedAt_n

Result:
K : Type u_1
n : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? n = none
⊢ convs'Aux s (n + 1) = convs'Aux s n

Proof state:
case succ.some
K : Type u_1
n✝ : ℕ
inst✝ : DivisionRing K
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, s.get? n = none → convs'Aux s (n + 1) = convs'Aux s n
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? (n + 1) = none
gp_head : Pair K
s_head_eq : s.head = some gp_head
this✝ : s.tail.TerminatedAt n
this : convs'Aux s.tail (n + 1) = convs'Aux s.tail n
⊢ convs'Aux s (n + 1 + 1) = convs'Aux s (n + 1)

Tactic:
rw [convs'Aux] at this

Result:
case succ.some
K : Type u_1
n✝ : ℕ
inst✝ : DivisionRing K
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, s.get? n = none → convs'Aux s (n + 1) = convs'Aux s n
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? (n + 1) = none
gp_head : Pair K
s_head_eq : s.head = some gp_head
this✝ : s.tail.TerminatedAt n
this :
  (match s.tail.head with
    | none => 0
    | some gp => gp.a / (gp.b + convs'Aux s.tail.tail n)) =
    convs'Aux s.tail n
⊢ convs'Aux s (n + 1 + 1) = convs'Aux s (n + 1)

Proof state:
case zero
K : Type u_1
n : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? 0 = none
⊢ convs'Aux s (0 + 1) = convs'Aux s 0

Tactic:
simp only [convs'Aux, terminatedAt_n, Stream'.Seq.head]

Result:
no goals

Proof state:
case succ.some
K : Type u_1
n✝ : ℕ
inst✝ : DivisionRing K
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, s.get? n = none → convs'Aux s (n + 1) = convs'Aux s n
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? (n + 1) = none
gp_head : Pair K
s_head_eq : s.head = some gp_head
⊢ convs'Aux s (n + 1 + 1) = convs'Aux s (n + 1)

Tactic:
have : s.tail.TerminatedAt n := by
  simp only [Stream'.Seq.TerminatedAt, s.get?_tail, terminatedAt_n]

Result:
case succ.some
K : Type u_1
n✝ : ℕ
inst✝ : DivisionRing K
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, s.get? n = none → convs'Aux s (n + 1) = convs'Aux s n
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? (n + 1) = none
gp_head : Pair K
s_head_eq : s.head = some gp_head
this : s.tail.TerminatedAt n
⊢ convs'Aux s (n + 1 + 1) = convs'Aux s (n + 1)

Proof state:
case succ.some
K : Type u_1
n✝ : ℕ
inst✝ : DivisionRing K
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, s.get? n = none → convs'Aux s (n + 1) = convs'Aux s n
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? (n + 1) = none
gp_head : Pair K
s_head_eq : s.head = some gp_head
this✝ : s.tail.TerminatedAt n
this :
  (match s.tail.head with
    | none => 0
    | some gp => gp.a / (gp.b + convs'Aux s.tail.tail n)) =
    convs'Aux s.tail n
⊢ convs'Aux s (n + 1 + 1) = convs'Aux s (n + 1)

Tactic:
simp [this, Nat.add_eq, add_zero, convs'Aux, s_head_eq]

Result:
no goals

Proof state:
K : Type u_1
n✝ : ℕ
inst✝ : DivisionRing K
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, s.get? n = none → convs'Aux s (n + 1) = convs'Aux s n
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? (n + 1) = none
gp_head : Pair K
s_head_eq : s.head = some gp_head
⊢ s.tail.TerminatedAt n

Tactic:
simp only [Stream'.Seq.TerminatedAt, s.get?_tail, terminatedAt_n]

Result:
no goals

Proof state:
case succ
K : Type u_1
n✝ : ℕ
inst✝ : DivisionRing K
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, s.get? n = none → convs'Aux s (n + 1) = convs'Aux s n
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? (n + 1) = none
⊢ convs'Aux s (n + 1 + 1) = convs'Aux s (n + 1)

Tactic:
cases s_head_eq : s.head with
| none => simp only [convs'Aux, s_head_eq]
| some gp_head =>
  have : s.tail.TerminatedAt n := by
    simp only [Stream'.Seq.TerminatedAt, s.get?_tail, terminatedAt_n]
  have := IH this
  rw [convs'Aux] at this
  simp [this, Nat.add_eq, add_zero, convs'Aux, s_head_eq]

Result:
no goals

Proof state:
K : Type u_1
n : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? n = none
⊢ convs'Aux s (n + 1) = convs'Aux s n

Tactic:
induction n generalizing s with
| zero => simp only [convs'Aux, terminatedAt_n, Stream'.Seq.head]
| succ n IH =>
  cases s_head_eq : s.head with
  | none => simp only [convs'Aux, s_head_eq]
  | some gp_head =>
    have : s.tail.TerminatedAt n := by
      simp only [Stream'.Seq.TerminatedAt, s.get?_tail, terminatedAt_n]
    have := IH this
    rw [convs'Aux] at this
    simp [this, Nat.add_eq, add_zero, convs'Aux, s_head_eq]

Result:
no goals

Proof state:
case succ.some
K : Type u_1
n✝ : ℕ
inst✝ : DivisionRing K
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, s.get? n = none → convs'Aux s (n + 1) = convs'Aux s n
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? (n + 1) = none
gp_head : Pair K
s_head_eq : s.head = some gp_head
this : s.tail.TerminatedAt n
⊢ convs'Aux s (n + 1 + 1) = convs'Aux s (n + 1)

Tactic:
have := IH this

Result:
case succ.some
K : Type u_1
n✝ : ℕ
inst✝ : DivisionRing K
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, s.get? n = none → convs'Aux s (n + 1) = convs'Aux s n
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? (n + 1) = none
gp_head : Pair K
s_head_eq : s.head = some gp_head
this✝ : s.tail.TerminatedAt n
this : convs'Aux s.tail (n + 1) = convs'Aux s.tail n
⊢ convs'Aux s (n + 1 + 1) = convs'Aux s (n + 1)

Proof state:
case succ.none
K : Type u_1
n✝ : ℕ
inst✝ : DivisionRing K
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, s.get? n = none → convs'Aux s (n + 1) = convs'Aux s n
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? (n + 1) = none
s_head_eq : s.head = none
⊢ convs'Aux s (n + 1 + 1) = convs'Aux s (n + 1)

Tactic:
simp only [convs'Aux, s_head_eq]

Result:
no goals