-- Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean
theorem succ_succ_nth_conv'Aux_eq_succ_nth_conv'Aux_squashSeq :
    convs'Aux s (n + 2) = convs'Aux (squashSeq s n) (n + 1)

Proof state:
case some.zero.intro
K : Type u_1
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (0 + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : s.head = some gp_head
this : (squashSeq s 0).head = some { a := gp_head.a, b := gp_head.b + gp_succ_n.a / gp_succ_n.b }
⊢ convs'Aux s (0 + 2) = convs'Aux (squashSeq s 0) (0 + 1)

Tactic:
simp_all [convs'Aux, Stream'.Seq.head, Stream'.Seq.get?_tail]

Result:
no goals

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

Tactic:
rw [squashSeq_eq_self_of_terminated s_succ_nth_eq,
  convs'Aux_stable_step_of_terminated s_succ_nth_eq]

Result:
no goals

Proof state:
case some.zero.intro
K : Type u_1
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (0 + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : s.head = some gp_head
⊢ convs'Aux s (0 + 2) = convs'Aux (squashSeq s 0) (0 + 1)

Tactic:
have : (squashSeq s 0).head = some ⟨gp_head.a, gp_head.b + gp_succ_n.a / gp_succ_n.b⟩ :=
  squashSeq_nth_of_not_terminated s_head_eq s_succ_nth_eq

Result:
case some.zero.intro
K : Type u_1
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (0 + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : s.head = some gp_head
this : (squashSeq s 0).head = some { a := gp_head.a, b := gp_head.b + gp_succ_n.a / gp_succ_n.b }
⊢ convs'Aux s (0 + 2) = convs'Aux (squashSeq s 0) (0 + 1)

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

Tactic:
suffices
  gp_head.a / (gp_head.b + convs'Aux s.tail (m + 2)) =
    convs'Aux (squashSeq s (m + 1)) (m + 2)
  by simpa only [convs'Aux, s_head_eq]

Result:
case some.succ.intro
K : Type u_1
inst✝ : DivisionRing K
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K),
    s.get? (m + 1) = some gp_succ_n → convs'Aux s (m + 2) = convs'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (m + 1 + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : s.head = some gp_head
⊢ gp_head.a / (gp_head.b + convs'Aux s.tail (m + 2)) = convs'Aux (squashSeq s (m + 1)) (m + 2)

Proof state:
case some.succ.intro
K : Type u_1
inst✝ : DivisionRing K
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K),
    s.get? (m + 1) = some gp_succ_n → convs'Aux s (m + 2) = convs'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (m + 1 + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : s.head = some gp_head
⊢ gp_head.a / (gp_head.b + convs'Aux s.tail (m + 2)) = convs'Aux (squashSeq s (m + 1)) (m + 2)

Tactic:
have : (squashSeq s (m + 1)).head = some gp_head :=
  (squashSeq_nth_of_lt m.succ_pos).trans s_head_eq

Result:
case some.succ.intro
K : Type u_1
inst✝ : DivisionRing K
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K),
    s.get? (m + 1) = some gp_succ_n → convs'Aux s (m + 2) = convs'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (m + 1 + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : s.head = some gp_head
this : (squashSeq s (m + 1)).head = some gp_head
⊢ gp_head.a / (gp_head.b + convs'Aux s.tail (m + 2)) = convs'Aux (squashSeq s (m + 1)) (m + 2)

Proof state:
case some.succ
K : Type u_1
inst✝ : DivisionRing K
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K),
    s.get? (m + 1) = some gp_succ_n → convs'Aux s (m + 2) = convs'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (m + 1 + 1) = some gp_succ_n
⊢ convs'Aux s (m + 1 + 2) = convs'Aux (squashSeq s (m + 1)) (m + 1 + 1)

Tactic:
obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head :=
  s.ge_stable (m + 2).zero_le s_succ_nth_eq

Result:
case some.succ.intro
K : Type u_1
inst✝ : DivisionRing K
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K),
    s.get? (m + 1) = some gp_succ_n → convs'Aux s (m + 2) = convs'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (m + 1 + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : s.head = some gp_head
⊢ convs'Aux s (m + 1 + 2) = convs'Aux (squashSeq s (m + 1)) (m + 1 + 1)

Proof state:
K : Type u_1
inst✝ : DivisionRing K
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K),
    s.get? (m + 1) = some gp_succ_n → convs'Aux s (m + 2) = convs'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (m + 1 + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : s.head = some gp_head
this : gp_head.a / (gp_head.b + convs'Aux s.tail (m + 2)) = convs'Aux (squashSeq s (m + 1)) (m + 2)
⊢ convs'Aux s (m + 1 + 2) = convs'Aux (squashSeq s (m + 1)) (m + 1 + 1)

Tactic:
simpa only [convs'Aux, s_head_eq]

Result:
no goals

Proof state:
case some.succ.intro
K : Type u_1
inst✝ : DivisionRing K
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K),
    s.get? (m + 1) = some gp_succ_n → convs'Aux s (m + 2) = convs'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (m + 1 + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : s.head = some gp_head
this : (squashSeq s (m + 1)).head = some gp_head
⊢ gp_head.a / (gp_head.b + convs'Aux s.tail (m + 2)) = convs'Aux (squashSeq s (m + 1)) (m + 2)

Tactic:
simp_all [convs'Aux, squashSeq_succ_n_tail_eq_squashSeq_tail_n]

Result:
no goals

Proof state:
case some.zero
K : Type u_1
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (0 + 1) = some gp_succ_n
⊢ convs'Aux s (0 + 2) = convs'Aux (squashSeq s 0) (0 + 1)

Tactic:
obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head :=
  s.ge_stable zero_le_one s_succ_nth_eq

Result:
case some.zero.intro
K : Type u_1
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (0 + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : s.head = some gp_head
⊢ convs'Aux s (0 + 2) = convs'Aux (squashSeq s 0) (0 + 1)

Proof state:
case some
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
⊢ convs'Aux s (n + 2) = convs'Aux (squashSeq s n) (n + 1)

Tactic:
induction n generalizing s gp_succ_n with
| zero =>
  obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head :=
    s.ge_stable zero_le_one s_succ_nth_eq
  have : (squashSeq s 0).head = some ⟨gp_head.a, gp_head.b + gp_succ_n.a / gp_succ_n.b⟩ :=
    squashSeq_nth_of_not_terminated s_head_eq s_succ_nth_eq
  simp_all [convs'Aux, Stream'.Seq.head, Stream'.Seq.get?_tail]
| succ m IH =>
  obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head :=
    s.ge_stable (m + 2).zero_le s_succ_nth_eq
  suffices
    gp_head.a / (gp_head.b + convs'Aux s.tail (m + 2)) =
      convs'Aux (squashSeq s (m + 1)) (m + 2)
    by simpa only [convs'Aux, s_head_eq]
  have : (squashSeq s (m + 1)).head = some gp_head :=
    (squashSeq_nth_of_lt m.succ_pos).trans s_head_eq
  simp_all [convs'Aux, squashSeq_succ_n_tail_eq_squashSeq_tail_n]

Result:
no goals