[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
nth_fr_eq_zero : ifp_n.fr = 0
⊢ IntFractPair.stream v (n + 1) = none
[PROOFSTEP]
cases' ifp_n with _ fr
[GOAL]
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
b✝ : ℤ
fr : K
stream_nth_eq : IntFractPair.stream v n = some { b := b✝, fr := fr }
nth_fr_eq_zero : { b := b✝, fr := fr }.fr = 0
⊢ IntFractPair.stream v (n + 1) = none
[PROOFSTEP]
change fr = 0 at nth_fr_eq_zero
[GOAL]
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
b✝ : ℤ
fr : K
stream_nth_eq : IntFractPair.stream v n = some { b := b✝, fr := fr }
nth_fr_eq_zero : fr = 0
⊢ IntFractPair.stream v (n + 1) = none
[PROOFSTEP]
simp [IntFractPair.stream, stream_nth_eq, nth_fr_eq_zero]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ IntFractPair.stream v (n + 1) = none ↔
    IntFractPair.stream v n = none ∨ ∃ ifp, IntFractPair.stream v n = some ifp ∧ ifp.fr = 0
[PROOFSTEP]
rw [IntFractPair.stream]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ (Option.bind (IntFractPair.stream v n) fun ap_n => if ap_n.fr = 0 then none else some (IntFractPair.of ap_n.fr⁻¹)) =
      none ↔
    IntFractPair.stream v n = none ∨ ∃ ifp, IntFractPair.stream v n = some ifp ∧ ifp.fr = 0
[PROOFSTEP]
cases IntFractPair.stream v n
[GOAL]
case none
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ (Option.bind none fun ap_n => if ap_n.fr = 0 then none else some (IntFractPair.of ap_n.fr⁻¹)) = none ↔
    none = none ∨ ∃ ifp, none = some ifp ∧ ifp.fr = 0
[PROOFSTEP]
simp [imp_false]
[GOAL]
case some
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
val✝ : IntFractPair K
⊢ (Option.bind (some val✝) fun ap_n => if ap_n.fr = 0 then none else some (IntFractPair.of ap_n.fr⁻¹)) = none ↔
    some val✝ = none ∨ ∃ ifp, some val✝ = some ifp ∧ ifp.fr = 0
[PROOFSTEP]
simp [imp_false]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_succ_n : IntFractPair K
⊢ IntFractPair.stream v (n + 1) = some ifp_succ_n ↔
    ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0 ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
[PROOFSTEP]
simp [IntFractPair.stream, ite_eq_iff]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
a : ℤ
n : ℕ
⊢ IntFractPair.stream (↑a) (n + 1) = none
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a : ℤ
⊢ IntFractPair.stream (↑a) (Nat.zero + 1) = none
[PROOFSTEP]
refine' IntFractPair.stream_eq_none_of_fr_eq_zero (IntFractPair.stream_zero (a : K)) _
[GOAL]
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a : ℤ
⊢ (IntFractPair.of ↑a).fr = 0
[PROOFSTEP]
simp only [IntFractPair.of, Int.fract_intCast]
[GOAL]
case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
a : ℤ
n : ℕ
ih : IntFractPair.stream (↑a) (n + 1) = none
⊢ IntFractPair.stream (↑a) (Nat.succ n + 1) = none
[PROOFSTEP]
exact IntFractPair.succ_nth_stream_eq_none_iff.mpr (Or.inl ih)
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_succ_n : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
succ_nth_fr_eq_zero : ifp_succ_n.fr = 0
⊢ ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋
[PROOFSTEP]
rcases succ_nth_stream_eq_some_iff.mp stream_succ_nth_eq with ⟨ifp_n, seq_nth_eq, _, rfl⟩
[GOAL]
case intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_n : IntFractPair K
seq_nth_eq : IntFractPair.stream v n = some ifp_n
left✝ : ifp_n.fr ≠ 0
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
succ_nth_fr_eq_zero : (IntFractPair.of ifp_n.fr⁻¹).fr = 0
⊢ ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋
[PROOFSTEP]
refine' ⟨ifp_n, seq_nth_eq, _⟩
[GOAL]
case intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_n : IntFractPair K
seq_nth_eq : IntFractPair.stream v n = some ifp_n
left✝ : ifp_n.fr ≠ 0
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
succ_nth_fr_eq_zero : (IntFractPair.of ifp_n.fr⁻¹).fr = 0
⊢ ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋
[PROOFSTEP]
simpa only [IntFractPair.of, Int.fract, sub_eq_zero] using succ_nth_fr_eq_zero
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
h : Int.fract v ≠ 0
n : ℕ
⊢ IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : Int.fract v ≠ 0
⊢ IntFractPair.stream v (Nat.zero + 1) = IntFractPair.stream (Int.fract v)⁻¹ Nat.zero
[PROOFSTEP]
have H : (IntFractPair.of v).fr = Int.fract v := rfl
[GOAL]
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : Int.fract v ≠ 0
H : (IntFractPair.of v).fr = Int.fract v
⊢ IntFractPair.stream v (Nat.zero + 1) = IntFractPair.stream (Int.fract v)⁻¹ Nat.zero
[PROOFSTEP]
rw [stream_zero, stream_succ_of_some (stream_zero v) (ne_of_eq_of_ne H h), H]
[GOAL]
case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n
⊢ IntFractPair.stream v (Nat.succ n + 1) = IntFractPair.stream (Int.fract v)⁻¹ (Nat.succ n)
[PROOFSTEP]
cases' eq_or_ne (IntFractPair.stream (Int.fract v)⁻¹ n) none with hnone hsome
[GOAL]
case succ.inl
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n
hnone : IntFractPair.stream (Int.fract v)⁻¹ n = none
⊢ IntFractPair.stream v (Nat.succ n + 1) = IntFractPair.stream (Int.fract v)⁻¹ (Nat.succ n)
[PROOFSTEP]
rw [hnone] at ih
[GOAL]
case succ.inl
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = none
hnone : IntFractPair.stream (Int.fract v)⁻¹ n = none
⊢ IntFractPair.stream v (Nat.succ n + 1) = IntFractPair.stream (Int.fract v)⁻¹ (Nat.succ n)
[PROOFSTEP]
rw [succ_nth_stream_eq_none_iff.mpr (Or.inl hnone), succ_nth_stream_eq_none_iff.mpr (Or.inl ih)]
[GOAL]
case succ.inr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
⊢ IntFractPair.stream v (Nat.succ n + 1) = IntFractPair.stream (Int.fract v)⁻¹ (Nat.succ n)
[PROOFSTEP]
obtain ⟨p, hp⟩ := Option.ne_none_iff_exists'.mp hsome
[GOAL]
case succ.inr.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
p : IntFractPair K
hp : IntFractPair.stream (Int.fract v)⁻¹ n = some p
⊢ IntFractPair.stream v (Nat.succ n + 1) = IntFractPair.stream (Int.fract v)⁻¹ (Nat.succ n)
[PROOFSTEP]
rw [hp] at ih
[GOAL]
case succ.inr.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
h : Int.fract v ≠ 0
n : ℕ
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
p : IntFractPair K
ih : IntFractPair.stream v (n + 1) = some p
hp : IntFractPair.stream (Int.fract v)⁻¹ n = some p
⊢ IntFractPair.stream v (Nat.succ n + 1) = IntFractPair.stream (Int.fract v)⁻¹ (Nat.succ n)
[PROOFSTEP]
cases' eq_or_ne p.fr 0 with hz hnz
[GOAL]
case succ.inr.intro.inl
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
h : Int.fract v ≠ 0
n : ℕ
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
p : IntFractPair K
ih : IntFractPair.stream v (n + 1) = some p
hp : IntFractPair.stream (Int.fract v)⁻¹ n = some p
hz : p.fr = 0
⊢ IntFractPair.stream v (Nat.succ n + 1) = IntFractPair.stream (Int.fract v)⁻¹ (Nat.succ n)
[PROOFSTEP]
rw [stream_eq_none_of_fr_eq_zero hp hz, stream_eq_none_of_fr_eq_zero ih hz]
[GOAL]
case succ.inr.intro.inr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
h : Int.fract v ≠ 0
n : ℕ
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
p : IntFractPair K
ih : IntFractPair.stream v (n + 1) = some p
hp : IntFractPair.stream (Int.fract v)⁻¹ n = some p
hnz : p.fr ≠ 0
⊢ IntFractPair.stream v (Nat.succ n + 1) = IntFractPair.stream (Int.fract v)⁻¹ (Nat.succ n)
[PROOFSTEP]
rw [stream_succ_of_some hp hnz, stream_succ_of_some ih hnz]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
⊢ (of v).h = ↑(IntFractPair.seq1 v).fst.b
[PROOFSTEP]
cases aux_seq_eq : IntFractPair.seq1 v
[GOAL]
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
fst✝ : IntFractPair K
snd✝ : Stream'.Seq (IntFractPair K)
aux_seq_eq : IntFractPair.seq1 v = (fst✝, snd✝)
⊢ (of v).h = ↑(fst✝, snd✝).fst.b
[PROOFSTEP]
simp [of, aux_seq_eq]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
⊢ (of v).h = ↑⌊v⌋
[PROOFSTEP]
simp [of_h_eq_intFractPair_seq1_fst_b, IntFractPair.of]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ TerminatedAt (of v) n ↔ IntFractPair.stream v (n + 1) = none
[PROOFSTEP]
rw [of_terminatedAt_iff_intFractPair_seq1_terminatedAt, Stream'.Seq.TerminatedAt,
  IntFractPair.get?_seq1_eq_succ_get?_stream]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
gp_n : Pair K
s_nth_eq : Stream'.Seq.get? (of v).s n = some gp_n
⊢ ∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ ↑ifp.b = gp_n.b
[PROOFSTEP]
obtain ⟨ifp, stream_succ_nth_eq, gp_n_eq⟩ :
  ∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ Pair.mk 1 (ifp.b : K) = gp_n :=
  by
  unfold of IntFractPair.seq1 at s_nth_eq
  simpa [Stream'.Seq.get?_tail, Stream'.Seq.map_get?] using s_nth_eq
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
gp_n : Pair K
s_nth_eq : Stream'.Seq.get? (of v).s n = some gp_n
⊢ ∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ { a := 1, b := ↑ifp.b } = gp_n
[PROOFSTEP]
unfold of IntFractPair.seq1 at s_nth_eq
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
gp_n : Pair K
s_nth_eq :
  Stream'.Seq.get?
      (match
          (IntFractPair.of v,
            Stream'.Seq.tail
              { val := IntFractPair.stream v, property := (_ : Stream'.IsSeq (IntFractPair.stream v)) }) with
        | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p => { a := 1, b := ↑p.b }) s }).s
      n =
    some gp_n
⊢ ∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ { a := 1, b := ↑ifp.b } = gp_n
[PROOFSTEP]
simpa [Stream'.Seq.get?_tail, Stream'.Seq.map_get?] using s_nth_eq
[GOAL]
case intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
gp_n : Pair K
s_nth_eq : Stream'.Seq.get? (of v).s n = some gp_n
ifp : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp
gp_n_eq : { a := 1, b := ↑ifp.b } = gp_n
⊢ ∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ ↑ifp.b = gp_n.b
[PROOFSTEP]
cases gp_n_eq
[GOAL]
case intro.intro.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
ifp : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp
s_nth_eq : Stream'.Seq.get? (of v).s n = some { a := 1, b := ↑ifp.b }
⊢ ∃ ifp_1, IntFractPair.stream v (n + 1) = some ifp_1 ∧ ↑ifp_1.b = { a := 1, b := ↑ifp.b }.b
[PROOFSTEP]
simp_all only [Option.some.injEq, exists_eq_left']
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_succ_n : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
⊢ Stream'.Seq.get? (of v).s n = some { a := 1, b := ↑ifp_succ_n.b }
[PROOFSTEP]
unfold of IntFractPair.seq1
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_succ_n : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
⊢ Stream'.Seq.get?
      (match
          (IntFractPair.of v,
            Stream'.Seq.tail
              { val := IntFractPair.stream v, property := (_ : Stream'.IsSeq (IntFractPair.stream v)) }) with
        | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p => { a := 1, b := ↑p.b }) s }).s
      n =
    some { a := 1, b := ↑ifp_succ_n.b }
[PROOFSTEP]
simp [Stream'.Seq.map_tail, Stream'.Seq.get?_tail, Stream'.Seq.map_get?, stream_succ_nth_eq]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
nth_fr_ne_zero : ifp_n.fr ≠ 0
⊢ IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
[PROOFSTEP]
cases ifp_n
[GOAL]
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
b✝ : ℤ
fr✝ : K
stream_nth_eq : IntFractPair.stream v n = some { b := b✝, fr := fr✝ }
nth_fr_ne_zero : { b := b✝, fr := fr✝ }.fr ≠ 0
⊢ IntFractPair.stream v (n + 1) = some (IntFractPair.of { b := b✝, fr := fr✝ }.fr⁻¹)
[PROOFSTEP]
simp [IntFractPair.stream, stream_nth_eq, nth_fr_ne_zero]
[GOAL]
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
b✝ : ℤ
fr✝ : K
stream_nth_eq : IntFractPair.stream v n = some { b := b✝, fr := fr✝ }
nth_fr_ne_zero : { b := b✝, fr := fr✝ }.fr ≠ 0
⊢ fr✝ = 0 → False
[PROOFSTEP]
intro
[GOAL]
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
b✝ : ℤ
fr✝ : K
stream_nth_eq : IntFractPair.stream v n = some { b := b✝, fr := fr✝ }
nth_fr_ne_zero : { b := b✝, fr := fr✝ }.fr ≠ 0
a✝ : fr✝ = 0
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
n : ℕ
v : K
⊢ Stream'.Seq.get? (of v).s 0 = Option.bind (IntFractPair.stream v 1) (some ∘ fun p => { a := 1, b := ↑p.b })
[PROOFSTEP]
rw [of, IntFractPair.seq1]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
n : ℕ
v : K
⊢ Stream'.Seq.get?
      (match
          (IntFractPair.of v,
            Stream'.Seq.tail
              { val := IntFractPair.stream v, property := (_ : Stream'.IsSeq (IntFractPair.stream v)) }) with
        | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p => { a := 1, b := ↑p.b }) s }).s
      0 =
    Option.bind (IntFractPair.stream v 1) (some ∘ fun p => { a := 1, b := ↑p.b })
[PROOFSTEP]
simp only [of, Stream'.Seq.map_tail, Stream'.Seq.map, Stream'.Seq.tail, Stream'.Seq.head, Stream'.Seq.get?, Stream'.map]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
n : ℕ
v : K
⊢ Option.map (fun p => { a := 1, b := ↑p.b }) (Stream'.nth (Stream'.tail (IntFractPair.stream v)) 0) =
    Option.bind (IntFractPair.stream v 1) (some ∘ fun p => { a := 1, b := ↑p.b })
[PROOFSTEP]
rw [← Stream'.nth_succ, Stream'.nth, Option.map]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
n : ℕ
v : K
⊢ (match IntFractPair.stream v (Nat.succ 0) with
    | some x => some { a := 1, b := ↑x.b }
    | none => none) =
    Option.bind (IntFractPair.stream v 1) (some ∘ fun p => { a := 1, b := ↑p.b })
[PROOFSTEP]
split
[GOAL]
case h_1
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
n : ℕ
v : K
x✝¹ : Option (IntFractPair K)
x✝ : IntFractPair K
heq✝ : IntFractPair.stream v (Nat.succ 0) = some x✝
⊢ some { a := 1, b := ↑x✝.b } = Option.bind (IntFractPair.stream v 1) (some ∘ fun p => { a := 1, b := ↑p.b })
[PROOFSTEP]
simp_all only [Option.some_bind, Option.none_bind, Function.comp_apply]
[GOAL]
case h_2
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
n : ℕ
v : K
x✝ : Option (IntFractPair K)
heq✝ : IntFractPair.stream v (Nat.succ 0) = none
⊢ none = Option.bind (IntFractPair.stream v 1) (some ∘ fun p => { a := 1, b := ↑p.b })
[PROOFSTEP]
simp_all only [Option.some_bind, Option.none_bind, Function.comp_apply]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : fract v ≠ 0
⊢ Stream'.Seq.head (of v).s = some { a := 1, b := ↑⌊(fract v)⁻¹⌋ }
[PROOFSTEP]
change (of v).s.get? 0 = _
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : fract v ≠ 0
⊢ Stream'.Seq.get? (of v).s 0 = some { a := 1, b := ↑⌊(fract v)⁻¹⌋ }
[PROOFSTEP]
rw [of_s_head_aux, stream_succ_of_some (stream_zero v) h, Option.bind]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : fract v ≠ 0
⊢ (match some (IntFractPair.of (IntFractPair.of v).fr⁻¹), some ∘ fun p => { a := 1, b := ↑p.b } with
    | none, x => none
    | some a, b => b a) =
    some { a := 1, b := ↑⌊(fract v)⁻¹⌋ }
[PROOFSTEP]
rfl
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a : ℤ
⊢ ∀ (n : ℕ), Stream'.Seq.get? (of ↑a).s n = none
[PROOFSTEP]
intro n
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
a : ℤ
n : ℕ
⊢ Stream'.Seq.get? (of ↑a).s n = none
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a : ℤ
⊢ Stream'.Seq.get? (of ↑a).s Nat.zero = none
[PROOFSTEP]
rw [of_s_head_aux, stream_succ_of_int, Option.bind]
[GOAL]
case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
a : ℤ
n : ℕ
ih : Stream'.Seq.get? (of ↑a).s n = none
⊢ Stream'.Seq.get? (of ↑a).s (Nat.succ n) = none
[PROOFSTEP]
exact (of (a : K)).s.prop ih
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ n : ℕ
⊢ Stream'.Seq.get? (of v).s (n + 1) = Stream'.Seq.get? (of (fract v)⁻¹).s n
[PROOFSTEP]
cases' eq_or_ne (fract v) 0 with h h
[GOAL]
case inl
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ n : ℕ
h : fract v = 0
⊢ Stream'.Seq.get? (of v).s (n + 1) = Stream'.Seq.get? (of (fract v)⁻¹).s n
[PROOFSTEP]
obtain ⟨a, rfl⟩ : ∃ a : ℤ, v = a := ⟨⌊v⌋, eq_of_sub_eq_zero h⟩
[GOAL]
case inl.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
n✝ n : ℕ
a : ℤ
h : fract ↑a = 0
⊢ Stream'.Seq.get? (of ↑a).s (n + 1) = Stream'.Seq.get? (of (fract ↑a)⁻¹).s n
[PROOFSTEP]
rw [fract_intCast, inv_zero, of_s_of_int, ← cast_zero, of_s_of_int, Stream'.Seq.get?_nil, Stream'.Seq.get?_nil]
[GOAL]
case inr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ n : ℕ
h : fract v ≠ 0
⊢ Stream'.Seq.get? (of v).s (n + 1) = Stream'.Seq.get? (of (fract v)⁻¹).s n
[PROOFSTEP]
cases' eq_or_ne ((of (fract v)⁻¹).s.get? n) none with h₁ h₁
[GOAL]
case inr.inl
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ n : ℕ
h : fract v ≠ 0
h₁ : Stream'.Seq.get? (of (fract v)⁻¹).s n = none
⊢ Stream'.Seq.get? (of v).s (n + 1) = Stream'.Seq.get? (of (fract v)⁻¹).s n
[PROOFSTEP]
rwa [h₁, ← terminatedAt_iff_s_none, of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none, stream_succ h, ←
  of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none, terminatedAt_iff_s_none]
[GOAL]
case inr.inr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ n : ℕ
h : fract v ≠ 0
h₁ : Stream'.Seq.get? (of (fract v)⁻¹).s n ≠ none
⊢ Stream'.Seq.get? (of v).s (n + 1) = Stream'.Seq.get? (of (fract v)⁻¹).s n
[PROOFSTEP]
obtain ⟨p, hp⟩ := Option.ne_none_iff_exists'.mp h₁
[GOAL]
case inr.inr.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ n : ℕ
h : fract v ≠ 0
h₁ : Stream'.Seq.get? (of (fract v)⁻¹).s n ≠ none
p : Pair K
hp : Stream'.Seq.get? (of (fract v)⁻¹).s n = some p
⊢ Stream'.Seq.get? (of v).s (n + 1) = Stream'.Seq.get? (of (fract v)⁻¹).s n
[PROOFSTEP]
obtain ⟨p', hp'₁, _⟩ := exists_succ_get?_stream_of_gcf_of_get?_eq_some hp
[GOAL]
case inr.inr.intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ n : ℕ
h : fract v ≠ 0
h₁ : Stream'.Seq.get? (of (fract v)⁻¹).s n ≠ none
p : Pair K
hp : Stream'.Seq.get? (of (fract v)⁻¹).s n = some p
p' : IntFractPair K
hp'₁ : IntFractPair.stream (fract v)⁻¹ (n + 1) = some p'
right✝ : ↑p'.b = p.b
⊢ Stream'.Seq.get? (of v).s (n + 1) = Stream'.Seq.get? (of (fract v)⁻¹).s n
[PROOFSTEP]
have Hp := get?_of_eq_some_of_succ_get?_intFractPair_stream hp'₁
[GOAL]
case inr.inr.intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ n : ℕ
h : fract v ≠ 0
h₁ : Stream'.Seq.get? (of (fract v)⁻¹).s n ≠ none
p : Pair K
hp : Stream'.Seq.get? (of (fract v)⁻¹).s n = some p
p' : IntFractPair K
hp'₁ : IntFractPair.stream (fract v)⁻¹ (n + 1) = some p'
right✝ : ↑p'.b = p.b
Hp : Stream'.Seq.get? (of (fract v)⁻¹).s n = some { a := 1, b := ↑p'.b }
⊢ Stream'.Seq.get? (of v).s (n + 1) = Stream'.Seq.get? (of (fract v)⁻¹).s n
[PROOFSTEP]
rw [← stream_succ h] at hp'₁
[GOAL]
case inr.inr.intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ n : ℕ
h : fract v ≠ 0
h₁ : Stream'.Seq.get? (of (fract v)⁻¹).s n ≠ none
p : Pair K
hp : Stream'.Seq.get? (of (fract v)⁻¹).s n = some p
p' : IntFractPair K
hp'₁ : IntFractPair.stream v (n + 1 + 1) = some p'
right✝ : ↑p'.b = p.b
Hp : Stream'.Seq.get? (of (fract v)⁻¹).s n = some { a := 1, b := ↑p'.b }
⊢ Stream'.Seq.get? (of v).s (n + 1) = Stream'.Seq.get? (of (fract v)⁻¹).s n
[PROOFSTEP]
rw [Hp, get?_of_eq_some_of_succ_get?_intFractPair_stream hp'₁]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a : ℤ
⊢ convergents' (of ↑a) n = ↑a
[PROOFSTEP]
induction' n with n
[GOAL]
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a : ℤ
⊢ convergents' (of ↑a) Nat.zero = ↑a
[PROOFSTEP]
simp only [zeroth_convergent'_eq_h, of_h_eq_floor, floor_intCast, Nat.zero_eq]
[GOAL]
case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
a : ℤ
n : ℕ
n_ih✝ : convergents' (of ↑a) n = ↑a
⊢ convergents' (of ↑a) (Nat.succ n) = ↑a
[PROOFSTEP]
rw [convergents', of_h_eq_floor, floor_intCast, add_right_eq_self]
[GOAL]
case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
a : ℤ
n : ℕ
n_ih✝ : convergents' (of ↑a) n = ↑a
⊢ convergents'Aux (of ↑a).s (Nat.succ n) = 0
[PROOFSTEP]
exact convergents'Aux_succ_none ((of_s_of_int K a).symm ▸ Stream'.Seq.get?_nil 0) _
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ convergents' (of v) (n + 1) = ↑⌊v⌋ + 1 / convergents' (of (fract v)⁻¹) n
[PROOFSTEP]
cases' eq_or_ne (fract v) 0 with h h
[GOAL]
case inl
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : fract v = 0
⊢ convergents' (of v) (n + 1) = ↑⌊v⌋ + 1 / convergents' (of (fract v)⁻¹) n
[PROOFSTEP]
obtain ⟨a, rfl⟩ : ∃ a : ℤ, v = a := ⟨⌊v⌋, eq_of_sub_eq_zero h⟩
[GOAL]
case inl.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
n : ℕ
a : ℤ
h : fract ↑a = 0
⊢ convergents' (of ↑a) (n + 1) = ↑⌊↑a⌋ + 1 / convergents' (of (fract ↑a)⁻¹) n
[PROOFSTEP]
rw [convergents'_of_int, fract_intCast, inv_zero, ← cast_zero, convergents'_of_int, cast_zero, div_zero, add_zero,
  floor_intCast]
[GOAL]
case inr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : fract v ≠ 0
⊢ convergents' (of v) (n + 1) = ↑⌊v⌋ + 1 / convergents' (of (fract v)⁻¹) n
[PROOFSTEP]
rw [convergents', of_h_eq_floor, add_right_inj, convergents'Aux_succ_some (of_s_head h)]
[GOAL]
case inr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : fract v ≠ 0
⊢ { a := 1, b := ↑⌊(fract v)⁻¹⌋ }.a /
      ({ a := 1, b := ↑⌊(fract v)⁻¹⌋ }.b + convergents'Aux (Stream'.Seq.tail (of v).s) n) =
    1 / convergents' (of (fract v)⁻¹) n
[PROOFSTEP]
exact congr_arg ((· / ·) 1) (by rw [convergents', of_h_eq_floor, add_right_inj, of_s_tail])
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : fract v ≠ 0
⊢ { a := 1, b := ↑⌊(fract v)⁻¹⌋ }.b + convergents'Aux (Stream'.Seq.tail (of v).s) n = convergents' (of (fract v)⁻¹) n
[PROOFSTEP]
rw [convergents', of_h_eq_floor, add_right_inj, of_s_tail]


[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ), m < n → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts) →
      ∃ conts, continuantsAux (of v) n = Pair.map Rat.cast conts
[PROOFSTEP]
clear n
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ), m < n → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts) →
      ∃ conts, continuantsAux (of v) n = Pair.map Rat.cast conts
[PROOFSTEP]
let g := of v
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ), m < n → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts) →
      ∃ conts, continuantsAux (of v) n = Pair.map Rat.cast conts
[PROOFSTEP]
intro n IH
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH : ∀ (m : ℕ), m < n → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
⊢ ∃ conts, continuantsAux (of v) n = Pair.map Rat.cast conts
[PROOFSTEP]
rcases n with
  (_ | _ | n)
    -- n = 0
[GOAL]
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
IH : ∀ (m : ℕ), m < Nat.zero → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
⊢ ∃ conts, continuantsAux (of v) Nat.zero = Pair.map Rat.cast conts
[PROOFSTEP]
suffices ∃ gp : Pair ℚ, Pair.mk (1 : K) 0 = gp.map (↑) by simpa [continuantsAux]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
IH : ∀ (m : ℕ), m < Nat.zero → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
this : ∃ gp, { a := 1, b := 0 } = Pair.map Rat.cast gp
⊢ ∃ conts, continuantsAux (of v) Nat.zero = Pair.map Rat.cast conts
[PROOFSTEP]
simpa [continuantsAux]
[GOAL]
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
IH : ∀ (m : ℕ), m < Nat.zero → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
⊢ ∃ gp, { a := 1, b := 0 } = Pair.map Rat.cast gp
[PROOFSTEP]
use Pair.mk 1 0
[GOAL]
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
IH : ∀ (m : ℕ), m < Nat.zero → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
⊢ { a := 1, b := 0 } = Pair.map Rat.cast { a := 1, b := 0 }
[PROOFSTEP]
simp
  -- n = 1
[GOAL]
case succ.zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
IH : ∀ (m : ℕ), m < Nat.succ Nat.zero → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
⊢ ∃ conts, continuantsAux (of v) (Nat.succ Nat.zero) = Pair.map Rat.cast conts
[PROOFSTEP]
suffices ∃ conts : Pair ℚ, Pair.mk g.h 1 = conts.map (↑) by simpa [continuantsAux]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
IH : ∀ (m : ℕ), m < Nat.succ Nat.zero → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
this : ∃ conts, { a := g.h, b := 1 } = Pair.map Rat.cast conts
⊢ ∃ conts, continuantsAux (of v) (Nat.succ Nat.zero) = Pair.map Rat.cast conts
[PROOFSTEP]
simpa [continuantsAux]
[GOAL]
case succ.zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
IH : ∀ (m : ℕ), m < Nat.succ Nat.zero → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
⊢ ∃ conts, { a := g.h, b := 1 } = Pair.map Rat.cast conts
[PROOFSTEP]
use Pair.mk ⌊v⌋ 1
[GOAL]
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
IH : ∀ (m : ℕ), m < Nat.succ Nat.zero → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
⊢ { a := g.h, b := 1 } = Pair.map Rat.cast { a := ↑⌊v⌋, b := 1 }
[PROOFSTEP]
simp
  -- 2 ≤ n
[GOAL]
case succ.succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH : ∀ (m : ℕ), m < Nat.succ (Nat.succ n) → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
⊢ ∃ conts, continuantsAux (of v) (Nat.succ (Nat.succ n)) = Pair.map Rat.cast conts
[PROOFSTEP]
cases' IH (n + 1) <| lt_add_one (n + 1) with pred_conts pred_conts_eq
[GOAL]
case succ.succ.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH : ∀ (m : ℕ), m < Nat.succ (Nat.succ n) → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : continuantsAux (of v) (n + 1) = Pair.map Rat.cast pred_conts
⊢ ∃ conts, continuantsAux (of v) (Nat.succ (Nat.succ n)) = Pair.map Rat.cast conts
[PROOFSTEP]
cases' s_ppred_nth_eq : g.s.get? n with gp_n
[GOAL]
case succ.succ.intro.none
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH : ∀ (m : ℕ), m < Nat.succ (Nat.succ n) → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : continuantsAux (of v) (n + 1) = Pair.map Rat.cast pred_conts
s_ppred_nth_eq : Stream'.Seq.get? g.s n = none
⊢ ∃ conts, continuantsAux (of v) (Nat.succ (Nat.succ n)) = Pair.map Rat.cast conts
[PROOFSTEP]
use pred_conts
[GOAL]
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH : ∀ (m : ℕ), m < Nat.succ (Nat.succ n) → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : continuantsAux (of v) (n + 1) = Pair.map Rat.cast pred_conts
s_ppred_nth_eq : Stream'.Seq.get? g.s n = none
⊢ continuantsAux (of v) (Nat.succ (Nat.succ n)) = Pair.map Rat.cast pred_conts
[PROOFSTEP]
have : g.continuantsAux (n + 2) = g.continuantsAux (n + 1) :=
  continuantsAux_stable_of_terminated (n + 1).le_succ s_ppred_nth_eq
[GOAL]
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH : ∀ (m : ℕ), m < Nat.succ (Nat.succ n) → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : continuantsAux (of v) (n + 1) = Pair.map Rat.cast pred_conts
s_ppred_nth_eq : Stream'.Seq.get? g.s n = none
this : continuantsAux g (n + 2) = continuantsAux g (n + 1)
⊢ continuantsAux (of v) (Nat.succ (Nat.succ n)) = Pair.map Rat.cast pred_conts
[PROOFSTEP]
simp only [this, pred_conts_eq]
  -- option.some
[GOAL]
case succ.succ.intro.some
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH : ∀ (m : ℕ), m < Nat.succ (Nat.succ n) → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : continuantsAux (of v) (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : Stream'.Seq.get? g.s n = some gp_n
⊢ ∃ conts, continuantsAux (of v) (Nat.succ (Nat.succ n)) = Pair.map Rat.cast conts
[PROOFSTEP]
cases' IH n <| lt_of_le_of_lt n.le_succ <| lt_add_one <| n + 1 with ppred_conts ppred_conts_eq
[GOAL]
case succ.succ.intro.some.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH : ∀ (m : ℕ), m < Nat.succ (Nat.succ n) → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : continuantsAux (of v) (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : Stream'.Seq.get? g.s n = some gp_n
ppred_conts : Pair ℚ
ppred_conts_eq : continuantsAux (of v) n = Pair.map Rat.cast ppred_conts
⊢ ∃ conts, continuantsAux (of v) (Nat.succ (Nat.succ n)) = Pair.map Rat.cast conts
[PROOFSTEP]
obtain ⟨a_eq_one, z, b_eq_z⟩ : gp_n.a = 1 ∧ ∃ z : ℤ, gp_n.b = (z : K)
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH : ∀ (m : ℕ), m < Nat.succ (Nat.succ n) → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : continuantsAux (of v) (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : Stream'.Seq.get? g.s n = some gp_n
ppred_conts : Pair ℚ
ppred_conts_eq : continuantsAux (of v) n = Pair.map Rat.cast ppred_conts
⊢ gp_n.a = 1 ∧ ∃ z, gp_n.b = ↑z
case succ.succ.intro.some.intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH : ∀ (m : ℕ), m < Nat.succ (Nat.succ n) → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : continuantsAux (of v) (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : Stream'.Seq.get? g.s n = some gp_n
ppred_conts : Pair ℚ
ppred_conts_eq : continuantsAux (of v) n = Pair.map Rat.cast ppred_conts
a_eq_one : gp_n.a = 1
z : ℤ
b_eq_z : gp_n.b = ↑z
⊢ ∃ conts, continuantsAux (of v) (Nat.succ (Nat.succ n)) = Pair.map Rat.cast conts
[PROOFSTEP]
exact of_part_num_eq_one_and_exists_int_part_denom_eq s_ppred_nth_eq
[GOAL]
case succ.succ.intro.some.intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH : ∀ (m : ℕ), m < Nat.succ (Nat.succ n) → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : continuantsAux (of v) (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : Stream'.Seq.get? g.s n = some gp_n
ppred_conts : Pair ℚ
ppred_conts_eq : continuantsAux (of v) n = Pair.map Rat.cast ppred_conts
a_eq_one : gp_n.a = 1
z : ℤ
b_eq_z : gp_n.b = ↑z
⊢ ∃ conts, continuantsAux (of v) (Nat.succ (Nat.succ n)) = Pair.map Rat.cast conts
[PROOFSTEP]
simp only [a_eq_one, b_eq_z, continuantsAux_recurrence s_ppred_nth_eq ppred_conts_eq pred_conts_eq]
[GOAL]
case succ.succ.intro.some.intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH : ∀ (m : ℕ), m < Nat.succ (Nat.succ n) → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : continuantsAux (of v) (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : Stream'.Seq.get? g.s n = some gp_n
ppred_conts : Pair ℚ
ppred_conts_eq : continuantsAux (of v) n = Pair.map Rat.cast ppred_conts
a_eq_one : gp_n.a = 1
z : ℤ
b_eq_z : gp_n.b = ↑z
⊢ ∃ conts,
    { a := ↑z * (Pair.map Rat.cast pred_conts).a + 1 * (Pair.map Rat.cast ppred_conts).a,
        b := ↑z * (Pair.map Rat.cast pred_conts).b + 1 * (Pair.map Rat.cast ppred_conts).b } =
      Pair.map Rat.cast conts
[PROOFSTEP]
use nextContinuants 1 (z : ℚ) ppred_conts pred_conts
[GOAL]
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH : ∀ (m : ℕ), m < Nat.succ (Nat.succ n) → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : continuantsAux (of v) (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : Stream'.Seq.get? g.s n = some gp_n
ppred_conts : Pair ℚ
ppred_conts_eq : continuantsAux (of v) n = Pair.map Rat.cast ppred_conts
a_eq_one : gp_n.a = 1
z : ℤ
b_eq_z : gp_n.b = ↑z
⊢ { a := ↑z * (Pair.map Rat.cast pred_conts).a + 1 * (Pair.map Rat.cast ppred_conts).a,
      b := ↑z * (Pair.map Rat.cast pred_conts).b + 1 * (Pair.map Rat.cast ppred_conts).b } =
    Pair.map Rat.cast (nextContinuants 1 (↑z) ppred_conts pred_conts)
[PROOFSTEP]
cases ppred_conts
[GOAL]
case h.mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH : ∀ (m : ℕ), m < Nat.succ (Nat.succ n) → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : continuantsAux (of v) (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : Stream'.Seq.get? g.s n = some gp_n
a_eq_one : gp_n.a = 1
z : ℤ
b_eq_z : gp_n.b = ↑z
a✝ b✝ : ℚ
ppred_conts_eq : continuantsAux (of v) n = Pair.map Rat.cast { a := a✝, b := b✝ }
⊢ { a := ↑z * (Pair.map Rat.cast pred_conts).a + 1 * (Pair.map Rat.cast { a := a✝, b := b✝ }).a,
      b := ↑z * (Pair.map Rat.cast pred_conts).b + 1 * (Pair.map Rat.cast { a := a✝, b := b✝ }).b } =
    Pair.map Rat.cast (nextContinuants 1 ↑z { a := a✝, b := b✝ } pred_conts)
[PROOFSTEP]
cases pred_conts
[GOAL]
case h.mk.mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GeneralizedContinuedFraction K := of v
n : ℕ
IH : ∀ (m : ℕ), m < Nat.succ (Nat.succ n) → ∃ conts, continuantsAux (of v) m = Pair.map Rat.cast conts
gp_n : Pair K
s_ppred_nth_eq : Stream'.Seq.get? g.s n = some gp_n
a_eq_one : gp_n.a = 1
z : ℤ
b_eq_z : gp_n.b = ↑z
a✝¹ b✝¹ : ℚ
ppred_conts_eq : continuantsAux (of v) n = Pair.map Rat.cast { a := a✝¹, b := b✝¹ }
a✝ b✝ : ℚ
pred_conts_eq : continuantsAux (of v) (n + 1) = Pair.map Rat.cast { a := a✝, b := b✝ }
⊢ { a := ↑z * (Pair.map Rat.cast { a := a✝, b := b✝ }).a + 1 * (Pair.map Rat.cast { a := a✝¹, b := b✝¹ }).a,
      b := ↑z * (Pair.map Rat.cast { a := a✝, b := b✝ }).b + 1 * (Pair.map Rat.cast { a := a✝¹, b := b✝¹ }).b } =
    Pair.map Rat.cast (nextContinuants 1 ↑z { a := a✝¹, b := b✝¹ } { a := a✝, b := b✝ })
[PROOFSTEP]
simp [nextContinuants, nextNumerator, nextDenominator]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ ∃ conts, continuants (of v) n = Pair.map Rat.cast conts
[PROOFSTEP]
rw [nth_cont_eq_succ_nth_cont_aux]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ ∃ conts, continuantsAux (of v) (n + 1) = Pair.map Rat.cast conts
[PROOFSTEP]
exact exists_gcf_pair_rat_eq_of_nth_conts_aux v <| n + 1
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ ∃ q, numerators (of v) n = ↑q
[PROOFSTEP]
rcases exists_gcf_pair_rat_eq_nth_conts v n with ⟨⟨a, _⟩, nth_cont_eq⟩
[GOAL]
case intro.mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a b✝ : ℚ
nth_cont_eq : continuants (of v) n = Pair.map Rat.cast { a := a, b := b✝ }
⊢ ∃ q, numerators (of v) n = ↑q
[PROOFSTEP]
use a
[GOAL]
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a b✝ : ℚ
nth_cont_eq : continuants (of v) n = Pair.map Rat.cast { a := a, b := b✝ }
⊢ numerators (of v) n = ↑a
[PROOFSTEP]
simp [num_eq_conts_a, nth_cont_eq]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ ∃ q, denominators (of v) n = ↑q
[PROOFSTEP]
rcases exists_gcf_pair_rat_eq_nth_conts v n with ⟨⟨_, b⟩, nth_cont_eq⟩
[GOAL]
case intro.mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a✝ b : ℚ
nth_cont_eq : continuants (of v) n = Pair.map Rat.cast { a := a✝, b := b }
⊢ ∃ q, denominators (of v) n = ↑q
[PROOFSTEP]
use b
[GOAL]
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a✝ b : ℚ
nth_cont_eq : continuants (of v) n = Pair.map Rat.cast { a := a✝, b := b }
⊢ denominators (of v) n = ↑b
[PROOFSTEP]
simp [denom_eq_conts_b, nth_cont_eq]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ ∃ q, convergents (of v) n = ↑q
[PROOFSTEP]
rcases exists_rat_eq_nth_numerator v n with ⟨Aₙ, nth_num_eq⟩
[GOAL]
case intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
Aₙ : ℚ
nth_num_eq : numerators (of v) n = ↑Aₙ
⊢ ∃ q, convergents (of v) n = ↑q
[PROOFSTEP]
rcases exists_rat_eq_nth_denominator v n with ⟨Bₙ, nth_denom_eq⟩
[GOAL]
case intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
Aₙ : ℚ
nth_num_eq : numerators (of v) n = ↑Aₙ
Bₙ : ℚ
nth_denom_eq : denominators (of v) n = ↑Bₙ
⊢ ∃ q, convergents (of v) n = ↑q
[PROOFSTEP]
use Aₙ / Bₙ
[GOAL]
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
Aₙ : ℚ
nth_num_eq : numerators (of v) n = ↑Aₙ
Bₙ : ℚ
nth_denom_eq : denominators (of v) n = ↑Bₙ
⊢ convergents (of v) n = ↑(Aₙ / Bₙ)
[PROOFSTEP]
simp [nth_num_eq, nth_denom_eq, convergent_eq_num_div_denom]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
terminates : Terminates (of v)
⊢ ∃ q, v = ↑q
[PROOFSTEP]
obtain ⟨n, v_eq_conv⟩ : ∃ n, v = (of v).convergents n
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
terminates : Terminates (of v)
⊢ ∃ n, v = convergents (of v) n
case intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
terminates : Terminates (of v)
n : ℕ
v_eq_conv : v = convergents (of v) n
⊢ ∃ q, v = ↑q
[PROOFSTEP]
exact of_correctness_of_terminates terminates
[GOAL]
case intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
terminates : Terminates (of v)
n : ℕ
v_eq_conv : v = convergents (of v) n
⊢ ∃ q, v = ↑q
[PROOFSTEP]
obtain ⟨q, conv_eq_q⟩ : ∃ q : ℚ, (of v).convergents n = (↑q : K)
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
terminates : Terminates (of v)
n : ℕ
v_eq_conv : v = convergents (of v) n
⊢ ∃ q, convergents (of v) n = ↑q
case intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
terminates : Terminates (of v)
n : ℕ
v_eq_conv : v = convergents (of v) n
q : ℚ
conv_eq_q : convergents (of v) n = ↑q
⊢ ∃ q, v = ↑q
[PROOFSTEP]
exact exists_rat_eq_nth_convergent v n
[GOAL]
case intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
terminates : Terminates (of v)
n : ℕ
v_eq_conv : v = convergents (of v) n
q : ℚ
conv_eq_q : convergents (of v) n = ↑q
⊢ ∃ q, v = ↑q
[PROOFSTEP]
have : v = (↑q : K) := Eq.trans v_eq_conv conv_eq_q
[GOAL]
case intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
terminates : Terminates (of v)
n : ℕ
v_eq_conv : v = convergents (of v) n
q : ℚ
conv_eq_q : convergents (of v) n = ↑q
this : v = ↑q
⊢ ∃ q, v = ↑q
[PROOFSTEP]
use q, this
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ mapFr Rat.cast (IntFractPair.of q) = IntFractPair.of v
[PROOFSTEP]
simp [IntFractPair.of, v_eq_q]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream v n
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q Nat.zero) = IntFractPair.stream v Nat.zero
case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream v n
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
case zero =>
  -- Porting note: was
      -- simp [IntFractPair.stream, coe_of_rat_eq v_eq_q]simp only [IntFractPair.stream, Option.map_some',
    coe_of_rat_eq v_eq_q]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q Nat.zero) = IntFractPair.stream v Nat.zero
[PROOFSTEP]
case zero =>
  -- Porting note: was
      -- simp [IntFractPair.stream, coe_of_rat_eq v_eq_q]simp only [IntFractPair.stream, Option.map_some',
    coe_of_rat_eq v_eq_q]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q Nat.zero) = IntFractPair.stream v Nat.zero
[PROOFSTEP]
simp only [IntFractPair.stream, Option.map_some', coe_of_rat_eq v_eq_q]
[GOAL]
case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream v n
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
case succ =>
  rw [v_eq_q] at IH
  cases' stream_q_nth_eq : IntFractPair.stream q n with ifp_n
  case none => simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq]
  case some =>
    cases' ifp_n with b fr
    cases' Decidable.em (fr = 0) with fr_zero fr_ne_zero
    · simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq, fr_zero]
    · replace IH : some (IntFractPair.mk b (fr : K)) = IntFractPair.stream (↑q) n; · rwa [stream_q_nth_eq] at IH
      have : (fr : K)⁻¹ = ((fr⁻¹ : ℚ) : K) := by norm_cast
      have coe_of_fr := coe_of_rat_eq this
      simpa [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq, fr_ne_zero]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream v n
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
case succ =>
  rw [v_eq_q] at IH
  cases' stream_q_nth_eq : IntFractPair.stream q n with ifp_n
  case none => simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq]
  case some =>
    cases' ifp_n with b fr
    cases' Decidable.em (fr = 0) with fr_zero fr_ne_zero
    · simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq, fr_zero]
    · replace IH : some (IntFractPair.mk b (fr : K)) = IntFractPair.stream (↑q) n; · rwa [stream_q_nth_eq] at IH
      have : (fr : K)⁻¹ = ((fr⁻¹ : ℚ) : K) := by norm_cast
      have coe_of_fr := coe_of_rat_eq this
      simpa [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq, fr_ne_zero]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream v n
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
rw [v_eq_q] at IH
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
cases' stream_q_nth_eq : IntFractPair.stream q n with ifp_n
[GOAL]
case none
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
stream_q_nth_eq : IntFractPair.stream q n = none
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
case some
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
ifp_n : IntFractPair ℚ
stream_q_nth_eq : IntFractPair.stream q n = some ifp_n
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
case none => simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
stream_q_nth_eq : IntFractPair.stream q n = none
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
case none => simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
stream_q_nth_eq : IntFractPair.stream q n = none
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq]
[GOAL]
case some
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
ifp_n : IntFractPair ℚ
stream_q_nth_eq : IntFractPair.stream q n = some ifp_n
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
case some =>
  cases' ifp_n with b fr
  cases' Decidable.em (fr = 0) with fr_zero fr_ne_zero
  · simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq, fr_zero]
  · replace IH : some (IntFractPair.mk b (fr : K)) = IntFractPair.stream (↑q) n; · rwa [stream_q_nth_eq] at IH
    have : (fr : K)⁻¹ = ((fr⁻¹ : ℚ) : K) := by norm_cast
    have coe_of_fr := coe_of_rat_eq this
    simpa [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq, fr_ne_zero]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
ifp_n : IntFractPair ℚ
stream_q_nth_eq : IntFractPair.stream q n = some ifp_n
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
case some =>
  cases' ifp_n with b fr
  cases' Decidable.em (fr = 0) with fr_zero fr_ne_zero
  · simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq, fr_zero]
  · replace IH : some (IntFractPair.mk b (fr : K)) = IntFractPair.stream (↑q) n; · rwa [stream_q_nth_eq] at IH
    have : (fr : K)⁻¹ = ((fr⁻¹ : ℚ) : K) := by norm_cast
    have coe_of_fr := coe_of_rat_eq this
    simpa [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq, fr_ne_zero]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
ifp_n : IntFractPair ℚ
stream_q_nth_eq : IntFractPair.stream q n = some ifp_n
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
cases' ifp_n with b fr
[GOAL]
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
cases' Decidable.em (fr = 0) with fr_zero fr_ne_zero
[GOAL]
case mk.inl
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_zero : fr = 0
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq, fr_zero]
[GOAL]
case mk.inr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_ne_zero : ¬fr = 0
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
replace IH : some (IntFractPair.mk b (fr : K)) = IntFractPair.stream (↑q) n
[GOAL]
case IH
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_ne_zero : ¬fr = 0
⊢ some { b := b, fr := ↑fr } = IntFractPair.stream (↑q) n
[PROOFSTEP]
rwa [stream_q_nth_eq] at IH
[GOAL]
case mk.inr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_ne_zero : ¬fr = 0
IH : some { b := b, fr := ↑fr } = IntFractPair.stream (↑q) n
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
have : (fr : K)⁻¹ = ((fr⁻¹ : ℚ) : K) := by norm_cast
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_ne_zero : ¬fr = 0
IH : some { b := b, fr := ↑fr } = IntFractPair.stream (↑q) n
⊢ (↑fr)⁻¹ = ↑fr⁻¹
[PROOFSTEP]
norm_cast
[GOAL]
case mk.inr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_ne_zero : ¬fr = 0
IH : some { b := b, fr := ↑fr } = IntFractPair.stream (↑q) n
this : (↑fr)⁻¹ = ↑fr⁻¹
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
have coe_of_fr := coe_of_rat_eq this
[GOAL]
case mk.inr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_ne_zero : ¬fr = 0
IH : some { b := b, fr := ↑fr } = IntFractPair.stream (↑q) n
this : (↑fr)⁻¹ = ↑fr⁻¹
coe_of_fr : mapFr Rat.cast (IntFractPair.of fr⁻¹) = IntFractPair.of (↑fr)⁻¹
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (Nat.succ n)) = IntFractPair.stream v (Nat.succ n)
[PROOFSTEP]
simpa [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq, fr_ne_zero]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Stream'.map (Option.map (mapFr Rat.cast)) (IntFractPair.stream q) = IntFractPair.stream v
[PROOFSTEP]
funext n
[GOAL]
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
⊢ Stream'.map (Option.map (mapFr Rat.cast)) (IntFractPair.stream q) n = IntFractPair.stream v n
[PROOFSTEP]
exact IntFractPair.coe_stream_nth_rat_eq v_eq_q n
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ ↑(of q).h = (of v).h
[PROOFSTEP]
unfold of IntFractPair.seq1
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ ↑(match
          (IntFractPair.of q,
            Stream'.Seq.tail
              { val := IntFractPair.stream q, property := (_ : Stream'.IsSeq (IntFractPair.stream q)) }) with
        | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p => { a := 1, b := ↑p.b }) s }).h =
    (match
        (IntFractPair.of v,
          Stream'.Seq.tail
            { val := IntFractPair.stream v, property := (_ : Stream'.IsSeq (IntFractPair.stream v)) }) with
      | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p => { a := 1, b := ↑p.b }) s }).h
[PROOFSTEP]
rw [← IntFractPair.coe_of_rat_eq v_eq_q]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ ↑(match
          (IntFractPair.of q,
            Stream'.Seq.tail
              { val := IntFractPair.stream q, property := (_ : Stream'.IsSeq (IntFractPair.stream q)) }) with
        | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p => { a := 1, b := ↑p.b }) s }).h =
    (match
        (IntFractPair.mapFr Rat.cast (IntFractPair.of q),
          Stream'.Seq.tail
            { val := IntFractPair.stream v, property := (_ : Stream'.IsSeq (IntFractPair.stream v)) }) with
      | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p => { a := 1, b := ↑p.b }) s }).h
[PROOFSTEP]
simp
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Option.map (Pair.map Rat.cast) (Stream'.Seq.get? (of q).s n) = Stream'.Seq.get? (of v).s n
[PROOFSTEP]
simp only [of, IntFractPair.seq1, Stream'.Seq.map_get?, Stream'.Seq.get?_tail]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Option.map (Pair.map Rat.cast)
      (Option.map (fun p => { a := 1, b := ↑p.b })
        (Stream'.Seq.get? { val := IntFractPair.stream q, property := (_ : Stream'.IsSeq (IntFractPair.stream q)) }
          (n + 1))) =
    Option.map (fun p => { a := 1, b := ↑p.b })
      (Stream'.Seq.get? { val := IntFractPair.stream v, property := (_ : Stream'.IsSeq (IntFractPair.stream v)) }
        (n + 1))
[PROOFSTEP]
simp only [Stream'.Seq.get?]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Option.map (Pair.map Rat.cast) (Option.map (fun p => { a := 1, b := ↑p.b }) (IntFractPair.stream q (n + 1))) =
    Option.map (fun p => { a := 1, b := ↑p.b }) (IntFractPair.stream v (n + 1))
[PROOFSTEP]
rw [← IntFractPair.coe_stream'_rat_eq v_eq_q]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Option.map (Pair.map Rat.cast) (Option.map (fun p => { a := 1, b := ↑p.b }) (IntFractPair.stream q (n + 1))) =
    Option.map (fun p => { a := 1, b := ↑p.b })
      (Stream'.map (Option.map (IntFractPair.mapFr Rat.cast)) (IntFractPair.stream q) (n + 1))
[PROOFSTEP]
rcases succ_nth_stream_eq : IntFractPair.stream q (n + 1) with (_ | ⟨_, _⟩)
[GOAL]
case none
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
succ_nth_stream_eq : IntFractPair.stream q (n + 1) = none
⊢ Option.map (Pair.map Rat.cast) (Option.map (fun p => { a := 1, b := ↑p.b }) none) =
    Option.map (fun p => { a := 1, b := ↑p.b })
      (Stream'.map (Option.map (IntFractPair.mapFr Rat.cast)) (IntFractPair.stream q) (n + 1))
[PROOFSTEP]
simp [Stream'.map, Stream'.nth, succ_nth_stream_eq]
[GOAL]
case some.mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
b✝ : ℤ
fr✝ : ℚ
succ_nth_stream_eq : IntFractPair.stream q (n + 1) = some { b := b✝, fr := fr✝ }
⊢ Option.map (Pair.map Rat.cast) (Option.map (fun p => { a := 1, b := ↑p.b }) (some { b := b✝, fr := fr✝ })) =
    Option.map (fun p => { a := 1, b := ↑p.b })
      (Stream'.map (Option.map (IntFractPair.mapFr Rat.cast)) (IntFractPair.stream q) (n + 1))
[PROOFSTEP]
simp [Stream'.map, Stream'.nth, succ_nth_stream_eq]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Stream'.Seq.map (Pair.map Rat.cast) (of q).s = (of v).s
[PROOFSTEP]
ext n
[GOAL]
case h.a
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
a✝ : Pair K
⊢ a✝ ∈ Stream'.Seq.get? (Stream'.Seq.map (Pair.map Rat.cast) (of q).s) n ↔ a✝ ∈ Stream'.Seq.get? (of v).s n
[PROOFSTEP]
rw [← coe_of_s_get?_rat_eq v_eq_q]
[GOAL]
case h.a
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n✝ n : ℕ
a✝ : Pair K
⊢ a✝ ∈ Stream'.Seq.get? (Stream'.Seq.map (Pair.map Rat.cast) (of q).s) n ↔
    a✝ ∈ Option.map (Pair.map Rat.cast) (Stream'.Seq.get? (of q).s n)
[PROOFSTEP]
rfl
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ { h := ↑(of q).h, s := Stream'.Seq.map (Pair.map Rat.cast) (of q).s } = of v
[PROOFSTEP]
cases' gcf_v_eq : of v with h s
[GOAL]
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
h : K
s : Stream'.Seq (Pair K)
gcf_v_eq : of v = { h := h, s := s }
⊢ { h := ↑(of q).h, s := Stream'.Seq.map (Pair.map Rat.cast) (of q).s } = { h := h, s := s }
[PROOFSTEP]
subst v
[GOAL]
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
h : K
s : Stream'.Seq (Pair K)
gcf_v_eq : of ↑q = { h := h, s := s }
⊢ { h := ↑(of q).h, s := Stream'.Seq.map (Pair.map Rat.cast) (of q).s } = { h := h, s := s }
[PROOFSTEP]
obtain rfl : ↑⌊(q : K)⌋ = h := by injection gcf_v_eq
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
h : K
s : Stream'.Seq (Pair K)
gcf_v_eq : of ↑q = { h := h, s := s }
⊢ ↑⌊↑q⌋ = h
[PROOFSTEP]
injection gcf_v_eq
[GOAL]
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
s : Stream'.Seq (Pair K)
gcf_v_eq : of ↑q = { h := ↑⌊↑q⌋, s := s }
⊢ { h := ↑(of q).h, s := Stream'.Seq.map (Pair.map Rat.cast) (of q).s } = { h := ↑⌊↑q⌋, s := s }
[PROOFSTEP]
simp only [gcf_v_eq, Int.cast_inj, Rat.floor_cast, of_h_eq_floor, eq_self_iff_true, Rat.cast_coe_int, and_self,
  coe_of_h_rat_eq rfl, coe_of_s_rat_eq rfl]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
⊢ Terminates (of v) ↔ Terminates (of q)
[PROOFSTEP]
constructor
[GOAL]
case mp
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
⊢ Terminates (of v) → Terminates (of q)
[PROOFSTEP]
intro h
[GOAL]
case mpr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
⊢ Terminates (of q) → Terminates (of v)
[PROOFSTEP]
intro h
[GOAL]
case mp
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
h : Terminates (of v)
⊢ Terminates (of q)
[PROOFSTEP]
cases' h with n h
[GOAL]
case mpr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
h : Terminates (of q)
⊢ Terminates (of v)
[PROOFSTEP]
cases' h with n h
[GOAL]
case mp.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n✝ : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
h : Stream'.Seq.TerminatedAt (of v).s n
⊢ Terminates (of q)
[PROOFSTEP]
use n
[GOAL]
case mpr.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n✝ : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
h : Stream'.Seq.TerminatedAt (of q).s n
⊢ Terminates (of v)
[PROOFSTEP]
use n
[GOAL]
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n✝ : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
h : Stream'.Seq.TerminatedAt (of v).s n
⊢ Stream'.Seq.TerminatedAt (of q).s n
[PROOFSTEP]
simp only [Stream'.Seq.TerminatedAt, (coe_of_s_get?_rat_eq v_eq_q n).symm] at h ⊢
[GOAL]
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n✝ : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
h : Stream'.Seq.TerminatedAt (of q).s n
⊢ Stream'.Seq.TerminatedAt (of v).s n
[PROOFSTEP]
simp only [Stream'.Seq.TerminatedAt, (coe_of_s_get?_rat_eq v_eq_q n).symm] at h ⊢
[GOAL]
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n✝ : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
h : Option.map (Pair.map Rat.cast) (Stream'.Seq.get? (of q).s n) = none
⊢ Stream'.Seq.get? (of q).s n = none
[PROOFSTEP]
cases h' : (of q).s.get? n
[GOAL]
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n✝ : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
h : Stream'.Seq.get? (of q).s n = none
⊢ Option.map (Pair.map Rat.cast) (Stream'.Seq.get? (of q).s n) = none
[PROOFSTEP]
cases h' : (of q).s.get? n
[GOAL]
case h.none
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n✝ : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
h : Option.map (Pair.map Rat.cast) (Stream'.Seq.get? (of q).s n) = none
h' : Stream'.Seq.get? (of q).s n = none
⊢ none = none
[PROOFSTEP]
simp only [h'] at h
[GOAL]
case h.some
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n✝ : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
h : Option.map (Pair.map Rat.cast) (Stream'.Seq.get? (of q).s n) = none
val✝ : Pair ℚ
h' : Stream'.Seq.get? (of q).s n = some val✝
⊢ some val✝ = none
[PROOFSTEP]
simp only [h'] at h
[GOAL]
case h.none
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n✝ : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
h h' : Stream'.Seq.get? (of q).s n = none
⊢ Option.map (Pair.map Rat.cast) none = none
[PROOFSTEP]
simp only [h'] at h
[GOAL]
case h.some
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n✝ : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
h : Stream'.Seq.get? (of q).s n = none
val✝ : Pair ℚ
h' : Stream'.Seq.get? (of q).s n = some val✝
⊢ Option.map (Pair.map Rat.cast) (some val✝) = none
[PROOFSTEP]
simp only [h'] at h
[GOAL]
case h.none
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n✝ : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
h' : Stream'.Seq.get? (of q).s n = none
h : Option.map (Pair.map Rat.cast) none = none
⊢ none = none
[PROOFSTEP]
trivial
[GOAL]
case h.some
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n✝ : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
val✝ : Pair ℚ
h' : Stream'.Seq.get? (of q).s n = some val✝
h : Option.map (Pair.map Rat.cast) (some val✝) = none
⊢ some val✝ = none
[PROOFSTEP]
trivial
[GOAL]
case h.none
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v✝ : K
q✝ : ℚ
v_eq_q✝ : v✝ = ↑q✝
n✝ : ℕ
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
h' : Stream'.Seq.get? (of q).s n = none
h : True
⊢ Option.map (Pair.map Rat.cast) none = none
[PROOFSTEP]
trivial
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
⊢ ifp_succ_n.fr.num < ifp_n.fr.num
[PROOFSTEP]
obtain ⟨ifp_n', stream_nth_eq', ifp_n_fract_ne_zero, IntFractPair.of_eq_ifp_succ_n⟩ :
  ∃ ifp_n', IntFractPair.stream q n = some ifp_n' ∧ ifp_n'.fr ≠ 0 ∧ IntFractPair.of ifp_n'.fr⁻¹ = ifp_succ_n
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
⊢ ∃ ifp_n', IntFractPair.stream q n = some ifp_n' ∧ ifp_n'.fr ≠ 0 ∧ IntFractPair.of ifp_n'.fr⁻¹ = ifp_succ_n
case intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
ifp_n' : IntFractPair ℚ
stream_nth_eq' : IntFractPair.stream q n = some ifp_n'
ifp_n_fract_ne_zero : ifp_n'.fr ≠ 0
IntFractPair.of_eq_ifp_succ_n : IntFractPair.of ifp_n'.fr⁻¹ = ifp_succ_n
⊢ ifp_succ_n.fr.num < ifp_n.fr.num
[PROOFSTEP]
exact succ_nth_stream_eq_some_iff.mp stream_succ_nth_eq
[GOAL]
case intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
ifp_n' : IntFractPair ℚ
stream_nth_eq' : IntFractPair.stream q n = some ifp_n'
ifp_n_fract_ne_zero : ifp_n'.fr ≠ 0
IntFractPair.of_eq_ifp_succ_n : IntFractPair.of ifp_n'.fr⁻¹ = ifp_succ_n
⊢ ifp_succ_n.fr.num < ifp_n.fr.num
[PROOFSTEP]
have : ifp_n = ifp_n' := by injection Eq.trans stream_nth_eq.symm stream_nth_eq'
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
ifp_n' : IntFractPair ℚ
stream_nth_eq' : IntFractPair.stream q n = some ifp_n'
ifp_n_fract_ne_zero : ifp_n'.fr ≠ 0
IntFractPair.of_eq_ifp_succ_n : IntFractPair.of ifp_n'.fr⁻¹ = ifp_succ_n
⊢ ifp_n = ifp_n'
[PROOFSTEP]
injection Eq.trans stream_nth_eq.symm stream_nth_eq'
[GOAL]
case intro.intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
ifp_n' : IntFractPair ℚ
stream_nth_eq' : IntFractPair.stream q n = some ifp_n'
ifp_n_fract_ne_zero : ifp_n'.fr ≠ 0
IntFractPair.of_eq_ifp_succ_n : IntFractPair.of ifp_n'.fr⁻¹ = ifp_succ_n
this : ifp_n = ifp_n'
⊢ ifp_succ_n.fr.num < ifp_n.fr.num
[PROOFSTEP]
cases this
[GOAL]
case intro.intro.intro.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
stream_nth_eq' : IntFractPair.stream q n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
IntFractPair.of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
⊢ ifp_succ_n.fr.num < ifp_n.fr.num
[PROOFSTEP]
rw [← IntFractPair.of_eq_ifp_succ_n]
[GOAL]
case intro.intro.intro.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
stream_nth_eq' : IntFractPair.stream q n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
IntFractPair.of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
⊢ (IntFractPair.of ifp_n.fr⁻¹).fr.num < ifp_n.fr.num
[PROOFSTEP]
cases' nth_stream_fr_nonneg_lt_one stream_nth_eq with zero_le_ifp_n_fract ifp_n_fract_lt_one
[GOAL]
case intro.intro.intro.refl.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
stream_nth_eq' : IntFractPair.stream q n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
IntFractPair.of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
zero_le_ifp_n_fract : 0 ≤ ifp_n.fr
ifp_n_fract_lt_one : ifp_n.fr < 1
⊢ (IntFractPair.of ifp_n.fr⁻¹).fr.num < ifp_n.fr.num
[PROOFSTEP]
have : 0 < ifp_n.fr := lt_of_le_of_ne zero_le_ifp_n_fract <| ifp_n_fract_ne_zero.symm
[GOAL]
case intro.intro.intro.refl.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
stream_nth_eq' : IntFractPair.stream q n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
IntFractPair.of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
zero_le_ifp_n_fract : 0 ≤ ifp_n.fr
ifp_n_fract_lt_one : ifp_n.fr < 1
this : 0 < ifp_n.fr
⊢ (IntFractPair.of ifp_n.fr⁻¹).fr.num < ifp_n.fr.num
[PROOFSTEP]
exact of_inv_fr_num_lt_num_of_pos this
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
⊢ ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
⊢ ∀ {ifp_n : IntFractPair ℚ},
    IntFractPair.stream q Nat.zero = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑Nat.zero
case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n✝ n : ℕ
IH : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
⊢ ∀ {ifp_n : IntFractPair ℚ},
    IntFractPair.stream q (Nat.succ n) = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑(Nat.succ n)
[PROOFSTEP]
case zero =>
  intro ifp_zero stream_zero_eq
  have : IntFractPair.of q = ifp_zero := by injection stream_zero_eq
  simp [le_refl, this.symm]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
⊢ ∀ {ifp_n : IntFractPair ℚ},
    IntFractPair.stream q Nat.zero = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑Nat.zero
[PROOFSTEP]
case zero =>
  intro ifp_zero stream_zero_eq
  have : IntFractPair.of q = ifp_zero := by injection stream_zero_eq
  simp [le_refl, this.symm]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
⊢ ∀ {ifp_n : IntFractPair ℚ},
    IntFractPair.stream q Nat.zero = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑Nat.zero
[PROOFSTEP]
intro ifp_zero stream_zero_eq
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
ifp_zero : IntFractPair ℚ
stream_zero_eq : IntFractPair.stream q Nat.zero = some ifp_zero
⊢ ifp_zero.fr.num ≤ (IntFractPair.of q).fr.num - ↑Nat.zero
[PROOFSTEP]
have : IntFractPair.of q = ifp_zero := by injection stream_zero_eq
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
ifp_zero : IntFractPair ℚ
stream_zero_eq : IntFractPair.stream q Nat.zero = some ifp_zero
⊢ IntFractPair.of q = ifp_zero
[PROOFSTEP]
injection stream_zero_eq
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n : ℕ
ifp_zero : IntFractPair ℚ
stream_zero_eq : IntFractPair.stream q Nat.zero = some ifp_zero
this : IntFractPair.of q = ifp_zero
⊢ ifp_zero.fr.num ≤ (IntFractPair.of q).fr.num - ↑Nat.zero
[PROOFSTEP]
simp [le_refl, this.symm]
[GOAL]
case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n✝ n : ℕ
IH : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
⊢ ∀ {ifp_n : IntFractPair ℚ},
    IntFractPair.stream q (Nat.succ n) = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑(Nat.succ n)
[PROOFSTEP]
case succ =>
  intro ifp_succ_n stream_succ_nth_eq
  suffices ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - n
    by
    rw [Int.ofNat_succ, sub_add_eq_sub_sub]
    solve_by_elim [le_sub_right_of_add_le]
  rcases succ_nth_stream_eq_some_iff.mp stream_succ_nth_eq with ⟨ifp_n, stream_nth_eq, -⟩
  have : ifp_succ_n.fr.num < ifp_n.fr.num := stream_succ_nth_fr_num_lt_nth_fr_num_rat stream_nth_eq stream_succ_nth_eq
  have : ifp_succ_n.fr.num + 1 ≤ ifp_n.fr.num := Int.add_one_le_of_lt this
  exact le_trans this (IH stream_nth_eq)
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n✝ n : ℕ
IH : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
⊢ ∀ {ifp_n : IntFractPair ℚ},
    IntFractPair.stream q (Nat.succ n) = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑(Nat.succ n)
[PROOFSTEP]
case succ =>
  intro ifp_succ_n stream_succ_nth_eq
  suffices ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - n
    by
    rw [Int.ofNat_succ, sub_add_eq_sub_sub]
    solve_by_elim [le_sub_right_of_add_le]
  rcases succ_nth_stream_eq_some_iff.mp stream_succ_nth_eq with ⟨ifp_n, stream_nth_eq, -⟩
  have : ifp_succ_n.fr.num < ifp_n.fr.num := stream_succ_nth_fr_num_lt_nth_fr_num_rat stream_nth_eq stream_succ_nth_eq
  have : ifp_succ_n.fr.num + 1 ≤ ifp_n.fr.num := Int.add_one_le_of_lt this
  exact le_trans this (IH stream_nth_eq)
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n✝ n : ℕ
IH : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
⊢ ∀ {ifp_n : IntFractPair ℚ},
    IntFractPair.stream q (Nat.succ n) = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑(Nat.succ n)
[PROOFSTEP]
intro ifp_succ_n stream_succ_nth_eq
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n✝ n : ℕ
IH : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
ifp_succ_n : IntFractPair ℚ
stream_succ_nth_eq : IntFractPair.stream q (Nat.succ n) = some ifp_succ_n
⊢ ifp_succ_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑(Nat.succ n)
[PROOFSTEP]
suffices ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - n
  by
  rw [Int.ofNat_succ, sub_add_eq_sub_sub]
  solve_by_elim [le_sub_right_of_add_le]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n✝ n : ℕ
IH : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
ifp_succ_n : IntFractPair ℚ
stream_succ_nth_eq : IntFractPair.stream q (Nat.succ n) = some ifp_succ_n
this : ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - ↑n
⊢ ifp_succ_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑(Nat.succ n)
[PROOFSTEP]
rw [Int.ofNat_succ, sub_add_eq_sub_sub]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n✝ n : ℕ
IH : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
ifp_succ_n : IntFractPair ℚ
stream_succ_nth_eq : IntFractPair.stream q (Nat.succ n) = some ifp_succ_n
this : ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - ↑n
⊢ ifp_succ_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n - 1
[PROOFSTEP]
solve_by_elim [le_sub_right_of_add_le]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n✝ n : ℕ
IH : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
ifp_succ_n : IntFractPair ℚ
stream_succ_nth_eq : IntFractPair.stream q (Nat.succ n) = some ifp_succ_n
⊢ ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - ↑n
[PROOFSTEP]
rcases succ_nth_stream_eq_some_iff.mp stream_succ_nth_eq with ⟨ifp_n, stream_nth_eq, -⟩
[GOAL]
case intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n✝ n : ℕ
IH : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
ifp_succ_n : IntFractPair ℚ
stream_succ_nth_eq : IntFractPair.stream q (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
⊢ ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - ↑n
[PROOFSTEP]
have : ifp_succ_n.fr.num < ifp_n.fr.num := stream_succ_nth_fr_num_lt_nth_fr_num_rat stream_nth_eq stream_succ_nth_eq
[GOAL]
case intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n✝ n : ℕ
IH : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
ifp_succ_n : IntFractPair ℚ
stream_succ_nth_eq : IntFractPair.stream q (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
this : ifp_succ_n.fr.num < ifp_n.fr.num
⊢ ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - ↑n
[PROOFSTEP]
have : ifp_succ_n.fr.num + 1 ≤ ifp_n.fr.num := Int.add_one_le_of_lt this
[GOAL]
case intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
n✝ n : ℕ
IH : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
ifp_succ_n : IntFractPair ℚ
stream_succ_nth_eq : IntFractPair.stream q (Nat.succ n) = some ifp_succ_n
ifp_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
this✝ : ifp_succ_n.fr.num < ifp_n.fr.num
this : ifp_succ_n.fr.num + 1 ≤ ifp_n.fr.num
⊢ ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - ↑n
[PROOFSTEP]
exact le_trans this (IH stream_nth_eq)
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q✝ : ℚ
n : ℕ
q : ℚ
⊢ ∃ n, IntFractPair.stream q n = none
[PROOFSTEP]
let fract_q_num := (Int.fract q).num
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q✝ : ℚ
n : ℕ
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
⊢ ∃ n, IntFractPair.stream q n = none
[PROOFSTEP]
let n := fract_q_num.natAbs + 1
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q✝ : ℚ
n✝ : ℕ
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := Int.natAbs fract_q_num + 1
⊢ ∃ n, IntFractPair.stream q n = none
[PROOFSTEP]
cases' stream_nth_eq : IntFractPair.stream q n with ifp
[GOAL]
case none
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q✝ : ℚ
n✝ : ℕ
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := Int.natAbs fract_q_num + 1
stream_nth_eq : IntFractPair.stream q n = none
⊢ ∃ n, IntFractPair.stream q n = none
[PROOFSTEP]
use n, stream_nth_eq
[GOAL]
case some
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q✝ : ℚ
n✝ : ℕ
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := Int.natAbs fract_q_num + 1
ifp : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp
⊢ ∃ n, IntFractPair.stream q n = none
[PROOFSTEP]
have ifp_fr_num_le_q_fr_num_sub_n : ifp.fr.num ≤ fract_q_num - n := stream_nth_fr_num_le_fr_num_sub_n_rat stream_nth_eq
[GOAL]
case some
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q✝ : ℚ
n✝ : ℕ
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := Int.natAbs fract_q_num + 1
ifp : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp
ifp_fr_num_le_q_fr_num_sub_n : ifp.fr.num ≤ fract_q_num - ↑n
⊢ ∃ n, IntFractPair.stream q n = none
[PROOFSTEP]
have : fract_q_num - n = -1 :=
  by
  have : 0 ≤ fract_q_num :=
    Rat.num_nonneg_iff_zero_le.mpr
      (Int.fract_nonneg q)
        -- Porting note: was
              -- simp [Int.natAbs_of_nonneg this, sub_add_eq_sub_sub_swap, sub_right_comm]
  simp only [Nat.cast_add, Int.natAbs_of_nonneg this, Nat.cast_one, sub_add_eq_sub_sub_swap, sub_right_comm, sub_self,
    zero_sub]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q✝ : ℚ
n✝ : ℕ
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := Int.natAbs fract_q_num + 1
ifp : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp
ifp_fr_num_le_q_fr_num_sub_n : ifp.fr.num ≤ fract_q_num - ↑n
⊢ fract_q_num - ↑n = -1
[PROOFSTEP]
have : 0 ≤ fract_q_num :=
  Rat.num_nonneg_iff_zero_le.mpr
    (Int.fract_nonneg q)
      -- Porting note: was
            -- simp [Int.natAbs_of_nonneg this, sub_add_eq_sub_sub_swap, sub_right_comm]
[GOAL]
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q✝ : ℚ
n✝ : ℕ
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := Int.natAbs fract_q_num + 1
ifp : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp
ifp_fr_num_le_q_fr_num_sub_n : ifp.fr.num ≤ fract_q_num - ↑n
this : 0 ≤ fract_q_num
⊢ fract_q_num - ↑n = -1
[PROOFSTEP]
simp only [Nat.cast_add, Int.natAbs_of_nonneg this, Nat.cast_one, sub_add_eq_sub_sub_swap, sub_right_comm, sub_self,
  zero_sub]
[GOAL]
case some
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q✝ : ℚ
n✝ : ℕ
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := Int.natAbs fract_q_num + 1
ifp : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp
ifp_fr_num_le_q_fr_num_sub_n : ifp.fr.num ≤ fract_q_num - ↑n
this : fract_q_num - ↑n = -1
⊢ ∃ n, IntFractPair.stream q n = none
[PROOFSTEP]
have : 0 ≤ ifp.fr := (nth_stream_fr_nonneg_lt_one stream_nth_eq).left
[GOAL]
case some
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q✝ : ℚ
n✝ : ℕ
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := Int.natAbs fract_q_num + 1
ifp : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp
ifp_fr_num_le_q_fr_num_sub_n : ifp.fr.num ≤ fract_q_num - ↑n
this✝ : fract_q_num - ↑n = -1
this : 0 ≤ ifp.fr
⊢ ∃ n, IntFractPair.stream q n = none
[PROOFSTEP]
have : 0 ≤ ifp.fr.num := Rat.num_nonneg_iff_zero_le.mpr this
[GOAL]
case some
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q✝ : ℚ
n✝ : ℕ
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := Int.natAbs fract_q_num + 1
ifp : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp
ifp_fr_num_le_q_fr_num_sub_n : ifp.fr.num ≤ fract_q_num - ↑n
this✝¹ : fract_q_num - ↑n = -1
this✝ : 0 ≤ ifp.fr
this : 0 ≤ ifp.fr.num
⊢ ∃ n, IntFractPair.stream q n = none
[PROOFSTEP]
linarith


[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : MulZeroClass M₀
a✝ b✝ a b : M₀
h : a ≠ 0 → b = 0
ha : a = 0
⊢ a * b = 0
[PROOFSTEP]
rw [ha, zero_mul]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : MulZeroClass M₀
a✝ b✝ a b : M₀
h : a ≠ 0 → b = 0
ha : ¬a = 0
⊢ a * b = 0
[PROOFSTEP]
rw [h ha, mul_zero]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : MulZeroOneClass M₀
h : 0 = 1
a : M₀
⊢ a = 0
[PROOFSTEP]
rw [← mul_one a, ← h, mul_zero]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : CancelMonoidWithZero M₀
a b c : M₀
⊢ a * c = b * c ↔ a = b ∨ c = 0
[PROOFSTEP]
by_cases hc : c = 0 <;> [simp [hc]; simp [mul_left_inj', hc]]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : CancelMonoidWithZero M₀
a b c : M₀
⊢ a * c = b * c ↔ a = b ∨ c = 0
[PROOFSTEP]
by_cases hc : c = 0
[GOAL]
case pos
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : CancelMonoidWithZero M₀
a b c : M₀
hc : c = 0
⊢ a * c = b * c ↔ a = b ∨ c = 0
[PROOFSTEP]
simp [hc]
[GOAL]
case neg
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : CancelMonoidWithZero M₀
a b c : M₀
hc : ¬c = 0
⊢ a * c = b * c ↔ a = b ∨ c = 0
[PROOFSTEP]
simp [mul_left_inj', hc]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : CancelMonoidWithZero M₀
a b c : M₀
⊢ a * b = a * c ↔ b = c ∨ a = 0
[PROOFSTEP]
by_cases ha : a = 0 <;> [simp [ha]; simp [mul_right_inj', ha]]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : CancelMonoidWithZero M₀
a b c : M₀
⊢ a * b = a * c ↔ b = c ∨ a = 0
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : CancelMonoidWithZero M₀
a b c : M₀
ha : a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0
[PROOFSTEP]
simp [ha]
[GOAL]
case neg
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : CancelMonoidWithZero M₀
a b c : M₀
ha : ¬a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0
[PROOFSTEP]
simp [mul_right_inj', ha]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : CancelMonoidWithZero M₀
a b c : M₀
⊢ a * b = a ↔ a * b = a * 1
[PROOFSTEP]
rw [mul_one]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : CancelMonoidWithZero M₀
a b c : M₀
⊢ a * b = b ↔ a * b = 1 * b
[PROOFSTEP]
rw [one_mul]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : CancelMonoidWithZero M₀
a b c : M₀
ha : a ≠ 0
⊢ a * b = a ↔ b = 1
[PROOFSTEP]
rw [Iff.comm, ← mul_right_inj' ha, mul_one]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : CancelMonoidWithZero M₀
a b c : M₀
hb : b ≠ 0
⊢ a * b = b ↔ a = 1
[PROOFSTEP]
rw [Iff.comm, ← mul_left_inj' hb, one_mul]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : CancelMonoidWithZero M₀
a b c : M₀
ha : a ≠ 0
⊢ a = a * b ↔ b = 1
[PROOFSTEP]
rw [eq_comm, mul_eq_left₀ ha]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : CancelMonoidWithZero M₀
a b c : M₀
hb : b ≠ 0
⊢ b = a * b ↔ a = 1
[PROOFSTEP]
rw [eq_comm, mul_eq_right₀ hb]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b c g h✝ x : G₀
h : b ≠ 0
a : G₀
⊢ a * (b * b⁻¹) = a
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a b✝ c g h✝ x : G₀
h : a ≠ 0
b : G₀
⊢ a * a⁻¹ * b = b
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a b c g h✝ x : G₀
h : a ≠ 0
a_eq_0 : a⁻¹ = 0
⊢ False
[PROOFSTEP]
have := mul_inv_cancel h
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a b c g h✝ x : G₀
h : a ≠ 0
a_eq_0 : a⁻¹ = 0
this : a * a⁻¹ = 1
⊢ False
[PROOFSTEP]
simp [a_eq_0] at this
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a b c g h✝ x : G₀
h : a ≠ 0
⊢ a⁻¹ * a = a⁻¹ * a * a⁻¹ * a⁻¹⁻¹
[PROOFSTEP]
simp [inv_ne_zero h]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a b c g h✝ x : G₀
h : a ≠ 0
⊢ a⁻¹ * a * a⁻¹ * a⁻¹⁻¹ = a⁻¹ * a⁻¹⁻¹
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a b c g h✝ x : G₀
h : a ≠ 0
⊢ a⁻¹ * a⁻¹⁻¹ = 1
[PROOFSTEP]
simp [inv_ne_zero h]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a b c g h✝ x : G₀
h : x ≠ 0
y y' : G₀
w : (fun y => x * y) y = (fun y => x * y) y'
⊢ y = y'
[PROOFSTEP]
simpa only [← mul_assoc, inv_mul_cancel h, one_mul] using congr_arg (fun y => x⁻¹ * y) w
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a b c g h✝ x : G₀
h : x ≠ 0
y y' : G₀
w : (fun y => y * x) y = (fun y => y * x) y'
⊢ y = y'
[PROOFSTEP]
simpa only [mul_assoc, mul_inv_cancel _ h, mul_one] using congr_arg (fun y => y * x⁻¹) w
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b c g h✝ x : G₀
h : b ≠ 0
a : G₀
⊢ a * (b⁻¹ * b) = a
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a b✝ c g h✝ x : G₀
h : a ≠ 0
b : G₀
⊢ a⁻¹ * a * b = b
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a b c g h✝ x : G₀
h : a * b = 1
⊢ a⁻¹ = b
[PROOFSTEP]
rw [← inv_mul_cancel_left₀ (left_ne_zero_of_mul_eq_one h) b, h, mul_one]
  -- See note [lower instance priority]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b c g h x : G₀
src✝ : GroupWithZero G₀ := inst✝
a : G₀
⊢ a⁻¹⁻¹ = a
[PROOFSTEP]
by_cases h : a = 0
[GOAL]
case pos
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b c g h✝ x : G₀
src✝ : GroupWithZero G₀ := inst✝
a : G₀
h : a = 0
⊢ a⁻¹⁻¹ = a
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b c g h✝ x : G₀
src✝ : GroupWithZero G₀ := inst✝
a : G₀
h : ¬a = 0
⊢ a⁻¹⁻¹ = a
[PROOFSTEP]
exact left_inv_eq_right_inv (inv_mul_cancel <| inv_ne_zero h) (inv_mul_cancel h)
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b✝ c g h x : G₀
src✝ : GroupWithZero G₀ := inst✝
a b : G₀
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b✝ c g h x : G₀
src✝ : GroupWithZero G₀ := inst✝
a b : G₀
ha : a = 0
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹
[PROOFSTEP]
simp [ha]
[GOAL]
case neg
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b✝ c g h x : G₀
src✝ : GroupWithZero G₀ := inst✝
a b : G₀
ha : ¬a = 0
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹
[PROOFSTEP]
by_cases hb : b = 0
[GOAL]
case pos
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b✝ c g h x : G₀
src✝ : GroupWithZero G₀ := inst✝
a b : G₀
ha : ¬a = 0
hb : b = 0
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹
[PROOFSTEP]
simp [hb]
[GOAL]
case neg
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b✝ c g h x : G₀
src✝ : GroupWithZero G₀ := inst✝
a b : G₀
ha : ¬a = 0
hb : ¬b = 0
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹
[PROOFSTEP]
refine' inv_eq_of_mul _
[GOAL]
case neg
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b✝ c g h x : G₀
src✝ : GroupWithZero G₀ := inst✝
a b : G₀
ha : ¬a = 0
hb : ¬b = 0
⊢ a * b * (b⁻¹ * a⁻¹) = 1
[PROOFSTEP]
simp [mul_assoc, ha, hb]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a b c g h✝ x✝ : G₀
src✝ : GroupWithZero G₀ := inst✝
x y z : G₀
hx : x ≠ 0
h : x * y = x * z
⊢ y = z
[PROOFSTEP]
rw [← inv_mul_cancel_left₀ hx y, h, inv_mul_cancel_left₀ hx z]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a b c g h✝ x✝ : G₀
src✝ : GroupWithZero G₀ := inst✝
x y z : G₀
hy : y ≠ 0
h : x * y = z * y
⊢ x = z
[PROOFSTEP]
rw [← mul_inv_cancel_right₀ hy x, h, mul_inv_cancel_right₀ hy z]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
⊢ 0 / a = 0
[PROOFSTEP]
rw [div_eq_mul_inv, zero_mul]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
⊢ a / 0 = 0
[PROOFSTEP]
rw [div_eq_mul_inv, inv_zero, mul_zero]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
⊢ a * a * a⁻¹ = a
[PROOFSTEP]
by_cases h : a = 0
[GOAL]
case pos
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
h : a = 0
⊢ a * a * a⁻¹ = a
[PROOFSTEP]
rw [h, inv_zero, mul_zero]
[GOAL]
case neg
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
h : ¬a = 0
⊢ a * a * a⁻¹ = a
[PROOFSTEP]
rw [mul_assoc, mul_inv_cancel h, mul_one]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
⊢ a * a⁻¹ * a = a
[PROOFSTEP]
by_cases h : a = 0
[GOAL]
case pos
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
h : a = 0
⊢ a * a⁻¹ * a = a
[PROOFSTEP]
rw [h, inv_zero, mul_zero]
[GOAL]
case neg
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
h : ¬a = 0
⊢ a * a⁻¹ * a = a
[PROOFSTEP]
rw [mul_inv_cancel h, one_mul]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
⊢ a⁻¹ * a * a = a
[PROOFSTEP]
by_cases h : a = 0
[GOAL]
case pos
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
h : a = 0
⊢ a⁻¹ * a * a = a
[PROOFSTEP]
rw [h, inv_zero, mul_zero]
[GOAL]
case neg
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
h : ¬a = 0
⊢ a⁻¹ * a * a = a
[PROOFSTEP]
rw [inv_mul_cancel h, one_mul]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
⊢ a * a / a = a
[PROOFSTEP]
rw [div_eq_mul_inv, mul_self_mul_inv a]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
⊢ a / a * a = a
[PROOFSTEP]
rw [div_eq_mul_inv, mul_inv_mul_self a]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
⊢ a / (a * a) = a⁻¹⁻¹ * a⁻¹ * a⁻¹
[PROOFSTEP]
simp [mul_inv_rev]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
h : a ≠ 0
⊢ 1 / a ≠ 0
[PROOFSTEP]
simpa only [one_div] using inv_ne_zero h
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
⊢ a⁻¹ = 0 ↔ a = 0
[PROOFSTEP]
rw [inv_eq_iff_eq_inv, inv_zero]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
⊢ a / (a / a) = a
[PROOFSTEP]
rw [div_div_eq_mul_div]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
⊢ a * a / a = a
[PROOFSTEP]
exact mul_self_div_self a
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
h : 1 / a ≠ 0
ha : a = 0
⊢ False
[PROOFSTEP]
rw [ha, div_zero] at h
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
h : 0 ≠ 0
ha : a = 0
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
h : a ≠ 0
g : G₀
⊢ (fun g => a * g) (a⁻¹ * g) = g
[PROOFSTEP]
simp [← mul_assoc, mul_inv_cancel h]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
h : a ≠ 0
g : G₀
⊢ (fun g => g * a) (g * a⁻¹) = g
[PROOFSTEP]
simp [mul_assoc, inv_mul_cancel h]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : CommGroupWithZero G₀
a✝ b✝ c✝ d a b c : G₀
⊢ a / c * b = a * b / c
[PROOFSTEP]
simp_rw [div_eq_mul_inv, mul_assoc, mul_comm c⁻¹]