-- Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean
theorem squashSeq_succ_n_tail_eq_squashSeq_tail_n :
    (squashSeq s (n + 1)).tail = squashSeq s.tail n

Proof state:
case some.intro.h.inr.none
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : s.get? (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
s_succ_mth_eq : s.get? (m + 1) = none
⊢ (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m

Tactic:
simp only [*, squashSeq, Stream'.Seq.get?_tail, Stream'.Seq.get?_zipWith,
  Option.map₂_none_right]

Result:
no goals

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

Tactic:
ext1 m

Result:
case some.intro.h
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : s.get? (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
m : ℕ
⊢ (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m

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

Tactic:
obtain ⟨gp_succ_n, s_succ_nth_eq⟩ : ∃ gp_succ_n, s.get? (n + 1) = some gp_succ_n :=
  s.ge_stable (n + 1).le_succ s_succ_succ_nth_eq

Result:
case some.intro
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : s.get? (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
⊢ (squashSeq s (n + 1)).tail = squashSeq s.tail n

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

Tactic:
cases s_succ_nth_eq : s.get? (n + 1) <;>
  simp only [squashSeq, Stream'.Seq.get?_tail, s_succ_nth_eq, s_succ_succ_nth_eq]

Result:
no goals

Proof state:
case some.intro.h.inl
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : s.get? (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
m : ℕ
m_eq_n : m = n
⊢ (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m

Tactic:
simp [*, squashSeq]

Result:
no goals

Proof state:
case some.intro.h.inr.some
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : s.get? (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
val✝ : Pair K
s_succ_mth_eq : s.get? (m + 1) = some val✝
⊢ (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m

Tactic:
simp [*, squashSeq]

Result:
no goals

Proof state:
case some.intro.h
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : s.get? (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
m : ℕ
⊢ (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m

Tactic:
rcases Decidable.em (m = n) with m_eq_n | m_ne_n

Result:
case some.intro.h.inl
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : s.get? (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
m : ℕ
m_eq_n : m = n
⊢ (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m

case some.intro.h.inr
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : s.get? (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
⊢ (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m

Proof state:
case some.intro.h.inr
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : s.get? (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
⊢ (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m

Tactic:
cases s_succ_mth_eq : s.get? (m + 1)

Result:
case some.intro.h.inr.none
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : s.get? (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
s_succ_mth_eq : s.get? (m + 1) = none
⊢ (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m

case some.intro.h.inr.some
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : s.get? (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
val✝ : Pair K
s_succ_mth_eq : s.get? (m + 1) = some val✝
⊢ (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m