case zero
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
terminated_at_n : TerminatedAt g Nat.zero
⊢ squashGCF g Nat.zero = g

case succ
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n✝ : ℕ
terminated_at_n : TerminatedAt g (Nat.succ n✝)
⊢ squashGCF g (Nat.succ n✝) = g
K : Type u_1
n : ℕ
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
terminated_at_n : TerminatedAt g n
⊢ squashGCF g n = g
cases n
case succ
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n✝ : ℕ
terminated_at_n : TerminatedAt g (Nat.succ n✝)
⊢ squashGCF g (Nat.succ n✝) = g
case zero
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
terminated_at_n : TerminatedAt g Nat.zero
⊢ squashGCF g Nat.zero = g

case succ
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n✝ : ℕ
terminated_at_n : TerminatedAt g (Nat.succ n✝)
⊢ squashGCF g (Nat.succ n✝) = g
case zero =>
  change g.s.get? 0 = none at terminated_at_n
  simp only [convergents', squashGCF, convergents'Aux, terminated_at_n]
no goals
case succ
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n✝ : ℕ
terminated_at_n : TerminatedAt g (Nat.succ n✝)
⊢ squashGCF g (Nat.succ n✝) = g
case succ =>
  cases g
  simp only [squashGCF, mk.injEq, true_and]
  exact squashSeq_eq_self_of_terminated terminated_at_n
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
terminated_at_n : Stream'.Seq.get? g.s 0 = none
⊢ squashGCF g Nat.zero = g
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
terminated_at_n : TerminatedAt g Nat.zero
⊢ squashGCF g Nat.zero = g
change g.s.get? 0 = none at terminated_at_n
no goals
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
terminated_at_n : Stream'.Seq.get? g.s 0 = none
⊢ squashGCF g Nat.zero = g
simp only [convergents', squashGCF, convergents'Aux, terminated_at_n]
case mk
K : Type u_1
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n✝ : ℕ
h✝ : K
s✝ : Stream'.Seq (Pair K)
terminated_at_n : TerminatedAt { h := h✝, s := s✝ } (Nat.succ n✝)
⊢ squashGCF { h := h✝, s := s✝ } (Nat.succ n✝) = { h := h✝, s := s✝ }
K : Type u_1
g : GeneralizedContinuedFraction K
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n✝ : ℕ
terminated_at_n : TerminatedAt g (Nat.succ n✝)
⊢ squashGCF g (Nat.succ n✝) = g
cases g
case mk
K : Type u_1
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n✝ : ℕ
h✝ : K
s✝ : Stream'.Seq (Pair K)
terminated_at_n : TerminatedAt { h := h✝, s := s✝ } (Nat.succ n✝)
⊢ squashSeq s✝ n✝ = s✝
case mk
K : Type u_1
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n✝ : ℕ
h✝ : K
s✝ : Stream'.Seq (Pair K)
terminated_at_n : TerminatedAt { h := h✝, s := s✝ } (Nat.succ n✝)
⊢ squashGCF { h := h✝, s := s✝ } (Nat.succ n✝) = { h := h✝, s := s✝ }
simp only [squashGCF, mk.injEq, true_and]
no goals
case mk
K : Type u_1
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
n✝ : ℕ
h✝ : K
s✝ : Stream'.Seq (Pair K)
terminated_at_n : TerminatedAt { h := h✝, s := s✝ } (Nat.succ n✝)
⊢ squashSeq s✝ n✝ = s✝
exact squashSeq_eq_self_of_terminated terminated_at_n