awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
terminates : (of v).Terminates
n : ℕ
v_eq_conv : v = (of v).convs n
q : ℚ
conv_eq_q : (of v).convs n = (↑q : K)
this : v = (↑q : K)
w : ℚ
h : v = (↑q : K)
⊢ ∃ (q : ℚ), v = (↑q : K)

Tactic:
use q, this
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
⊢ mapFr Rat.cast (IntFractPair.of q) = IntFractPair.of v

Tactic:
simp [IntFractPair.of, v_eq_q]

Premises used: GenContFract.IntFractPair.of
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q 0) = IntFractPair.stream v 0

Tactic:
simp only [IntFractPair.stream, Option.map_some, coe_of_rat_eq v_eq_q]

Premises used: GenContFract.IntFractPair.stream, GenContFract.IntFractPair.coe_of_rat_eq, Option.map_some
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream v n
⊢ Eq.{u_1 + 1} (α := Option (IntFractPair K)) (Option.map (mapFr Rat.cast) (IntFractPair.stream q n))
    (IntFractPair.stream (↑q : K) n)

Tactic:
rw [v_eq_q] at IH
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
n : ℕ
IH :
  Eq.{u_1 + 1} (α := Option (IntFractPair K)) (Option.map (mapFr Rat.cast) (IntFractPair.stream q n))
    (IntFractPair.stream (↑q : K) n)
stream_q_nth_eq : IntFractPair.stream q n = none
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)

Tactic:
simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq]

Premises used: GenContFract.IntFractPair.stream, Eq.symm
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
n : ℕ
IH :
  Eq.{u_1 + 1} (α := Option (IntFractPair K)) (Option.map (mapFr Rat.cast) (IntFractPair.stream q n))
    (IntFractPair.stream (↑q : K) n)
ifp_n : IntFractPair ℚ
stream_q_nth_eq : IntFractPair.stream q n = some ifp_n
succ :
  ∀ (b : ℤ) (fr : ℚ) (stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }),
    Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)

Tactic:
obtain ⟨b, fr⟩ := ifp_n

Premises used: GenContFract.IntFractPair.b, GenContFract.IntFractPair.fr
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
n : ℕ
IH :
  Eq.{u_1 + 1} (α := Option (IntFractPair K)) (Option.map (mapFr Rat.cast) (IntFractPair.stream q n))
    (IntFractPair.stream (↑q : K) n)
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
succ : ∀ (fr_zero : fr = 0), Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)
succ₁ :
  ∀ (fr_ne_zero : ¬fr = 0), Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)

Tactic:
rcases Decidable.em (fr = 0) with fr_zero | fr_ne_zero

Premises used: Decidable.em, OfNat.ofNat, Eq
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
n : ℕ
IH :
  Eq.{u_1 + 1} (α := Option (IntFractPair K)) (Option.map (mapFr Rat.cast) (IntFractPair.stream q n))
    (IntFractPair.stream (↑q : K) 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 (n + 1)) = IntFractPair.stream v (n + 1)

Tactic:
simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq, fr_zero]

Premises used: GenContFract.IntFractPair.stream, Eq.symm
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
n : ℕ
IH :
  Eq.{u_1 + 1} (α := Option (IntFractPair K)) (Option.map (mapFr Rat.cast) (IntFractPair.stream q n))
    (IntFractPair.stream (↑q : K) n)
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_ne_zero : ¬fr = 0
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (IH :
      Eq.{u_1 + 1} (α := Option (IntFractPair K))
        (Option.map (mapFr Rat.cast) (some { b := b, fr := fr : IntFractPair ℚ })) (IntFractPair.stream (↑q : K) n))
    (stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }) (fr_ne_zero : ¬fr = 0),
    Eq.{u_1 + 1} (α := Option (IntFractPair K)) (some { b := b, fr := (↑fr : K) }) (IntFractPair.stream (↑q : K) n)
⊢ Eq.{u_1 + 1} (α := Option (IntFractPair K)) (some { b := b, fr := (↑fr : K) }) (IntFractPair.stream (↑q : K) n)

Tactic:
rwa [stream_q_nth_eq] at IH
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
n : ℕ
IH :
  Eq.{u_1 + 1} (α := Option (IntFractPair K)) (Option.map (mapFr Rat.cast) (IntFractPair.stream q n))
    (IntFractPair.stream (↑q : K) n)
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_ne_zero : ¬fr = 0
⊢ Eq.{u_1 + 1} (α := Option (IntFractPair K)) (some { b := b, fr := (↑fr : K) }) (IntFractPair.stream (↑q : K) n)

Tactic:
replace IH : some (IntFractPair.mk b (fr : K)) = IntFractPair.stream (↑q) n := by
          rwa [stream_q_nth_eq] at IH
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
n : ℕ
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_ne_zero : ¬fr = 0
IH : Eq.{u_1 + 1} (α := Option (IntFractPair K)) (some { b := b, fr := (↑fr : K) }) (IntFractPair.stream (↑q : K) n)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : fr⁻¹ = fr⁻¹
⊢ Eq.{u_1 + 1} (α := K) (↑fr : K)⁻¹ (↑fr⁻¹ : K)

Tactic:
norm_cast
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
n : ℕ
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_ne_zero : ¬fr = 0
IH : Eq.{u_1 + 1} (α := Option (IntFractPair K)) (some { b := b, fr := (↑fr : K) }) (IntFractPair.stream (↑q : K) n)
⊢ Eq.{u_1 + 1} (α := K) (↑fr : K)⁻¹ (↑fr⁻¹ : K)

Tactic:
have : (fr : K)⁻¹ = ((fr⁻¹ : ℚ) : K) := by norm_cast
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
n : ℕ
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_ne_zero : ¬fr = 0
IH : Eq.{u_1 + 1} (α := Option (IntFractPair K)) (some { b := b, fr := (↑fr : K) }) (IntFractPair.stream (↑q : K) n)
this : Eq.{u_1 + 1} (α := K) (↑fr : K)⁻¹ (↑fr⁻¹ : K)
⊢ Eq.{u_1 + 1} (α := IntFractPair K) (mapFr Rat.cast (IntFractPair.of fr⁻¹)) (IntFractPair.of (↑fr : K)⁻¹)

Tactic:
have coe_of_fr := coe_of_rat_eq this
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
n : ℕ
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_ne_zero : ¬fr = 0
IH : Eq.{u_1 + 1} (α := Option (IntFractPair K)) (some { b := b, fr := (↑fr : K) }) (IntFractPair.stream (↑q : K) n)
this : Eq.{u_1 + 1} (α := K) (↑fr : K)⁻¹ (↑fr⁻¹ : K)
coe_of_fr : Eq.{u_1 + 1} (α := IntFractPair K) (mapFr Rat.cast (IntFractPair.of fr⁻¹)) (IntFractPair.of (↑fr : K)⁻¹)
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)

Tactic:
simpa [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq, fr_ne_zero]

Premises used: GenContFract.IntFractPair.stream, Eq.symm
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
n : ℕ
IH :
  Eq.{u_1 + 1} (α := Option (IntFractPair K)) (Option.map (mapFr Rat.cast) (IntFractPair.stream q n))
    (IntFractPair.stream (↑q : K) n)
succ :
  ∀ (x : Option (IntFractPair ℚ)) (stream_q_nth_eq : IntFractPair.stream q n = x),
    Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)

Tactic:
cases stream_q_nth_eq : IntFractPair.stream q n with
    | none => simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq]
    | some ifp_n =>
      obtain ⟨b, fr⟩ := ifp_n
      rcases 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 := by
          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]

Premises used: GenContFract.IntFractPair.stream, Option.some, Option.none, Decidable.em, GenContFract.IntFractPair.b, GenContFract.IntFractPair.fr, OfNat.ofNat, Eq.symm, Eq
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
n : ℕ
zero : Option.map (mapFr Rat.cast) (IntFractPair.stream q 0) = IntFractPair.stream v 0
succ :
  ∀ (n : ℕ) (IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream v n),
    Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream v n

Tactic:
induction n with
  | zero =>
    simp only [IntFractPair.stream, Option.map_some, coe_of_rat_eq v_eq_q]
  | succ n IH =>
    rw [v_eq_q] at IH
    cases stream_q_nth_eq : IntFractPair.stream q n with
    | none => simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq]
    | some ifp_n =>
      obtain ⟨b, fr⟩ := ifp_n
      rcases 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 := by
          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]

Premises used: GenContFract.IntFractPair.stream, Option.some, GenContFract.IntFractPair.coe_of_rat_eq, Option.none, Decidable.em, Option.map_some, GenContFract.IntFractPair.b, GenContFract.IntFractPair.fr, OfNat.ofNat, Eq
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
h : ∀ (n : ℕ), Stream'.map (Option.map (mapFr Rat.cast)) (IntFractPair.stream q) n = IntFractPair.stream v n
⊢ Stream'.map (Option.map (mapFr Rat.cast)) (IntFractPair.stream q) = IntFractPair.stream v

Tactic:
funext n
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
n : ℕ
⊢ Stream'.map (Option.map (mapFr Rat.cast)) (IntFractPair.stream q) n = IntFractPair.stream v n

Tactic:
IntFractPair.coe_stream_nth_rat_eq v_eq_q n

Premises used: GenContFract.IntFractPair.coe_stream_nth_rat_eq, Stream'.get, Stream'.map
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
n : ℕ
⊢ Stream'.map (Option.map (mapFr Rat.cast)) (IntFractPair.stream q) n = IntFractPair.stream v n

Tactic:
exact IntFractPair.coe_stream_nth_rat_eq v_eq_q n

Premises used: GenContFract.IntFractPair.coe_stream_nth_rat_eq
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
⊢ (↑(of q).h : K) = (of v).h

Tactic:
simp_all
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
n : ℕ
simp :
  Eq (α := Option (Pair K))
    (Option.map (Pair.map Rat.cast)
      (Option.map (fun (p : IntFractPair ℚ) ↦ { a := 1, b := (↑p.b : ℚ) })
        (Stream'.Seq.get?
          (Subtype.mk (p := fun (f : Stream' (Option (IntFractPair ℚ))) ↦ f.IsSeq) (IntFractPair.stream q) ⋯) (n + 1))))
    (Option.map (fun (p : IntFractPair K) ↦ { a := 1, b := (↑p.b : K) })
      (Stream'.Seq.get?
        (Subtype.mk (p := fun (f : Stream' (Option (IntFractPair K))) ↦ f.IsSeq) (IntFractPair.stream v) ⋯) (n + 1)))
⊢ Option.map (Pair.map Rat.cast) ((of q).s.get? n) = (of v).s.get? n

Tactic:
simp only [of, IntFractPair.seq1, Stream'.Seq.map_get?, Stream'.Seq.get?_tail]

Premises used: Stream'.Seq.get?_tail, GenContFract.of, Stream'.Seq.map_get?, GenContFract.IntFractPair.seq1
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
n : ℕ
simp :
  Eq (α := Option (Pair K))
    (Option.map (Pair.map Rat.cast)
      (Option.map (fun (p : IntFractPair ℚ) ↦ { a := 1, b := (↑p.b : ℚ) }) (IntFractPair.stream q (n + 1))))
    (Option.map (fun (p : IntFractPair K) ↦ { a := 1, b := (↑p.b : K) }) (IntFractPair.stream v (n + 1)))
⊢ Eq (α := Option (Pair K))
    (Option.map (Pair.map Rat.cast)
      (Option.map (fun (p : IntFractPair ℚ) ↦ { a := 1, b := (↑p.b : ℚ) })
        (Stream'.Seq.get?
          (Subtype.mk (p := fun (f : Stream' (Option (IntFractPair ℚ))) ↦ f.IsSeq) (IntFractPair.stream q) ⋯) (n + 1))))
    (Option.map (fun (p : IntFractPair K) ↦ { a := 1, b := (↑p.b : K) })
      (Stream'.Seq.get?
        (Subtype.mk (p := fun (f : Stream' (Option (IntFractPair K))) ↦ f.IsSeq) (IntFractPair.stream v) ⋯) (n + 1)))

Tactic:
simp only [Stream'.Seq.get?]

Premises used: Stream'.Seq.get?
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
n : ℕ
rw :
  Eq.{u_1 + 1} (α := Option (Pair K))
    (Option.map (Pair.map Rat.cast)
      (Option.map (fun (p : IntFractPair ℚ) ↦ { a := 1, b := (↑p.b : ℚ) }) (IntFractPair.stream q (n + 1))))
    (Option.map (fun (p : IntFractPair K) ↦ { a := 1, b := (↑p.b : K) })
      (Stream'.map (Option.map (IntFractPair.mapFr Rat.cast)) (IntFractPair.stream q) (n + 1)))
⊢ Eq (α := Option (Pair K))
    (Option.map (Pair.map Rat.cast)
      (Option.map (fun (p : IntFractPair ℚ) ↦ { a := 1, b := (↑p.b : ℚ) }) (IntFractPair.stream q (n + 1))))
    (Option.map (fun (p : IntFractPair K) ↦ { a := 1, b := (↑p.b : K) }) (IntFractPair.stream v (n + 1)))

Tactic:
rw [← IntFractPair.coe_stream'_rat_eq v_eq_q]

Premises used: GenContFract.IntFractPair.coe_stream'_rat_eq
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
n : ℕ
none :
  ∀ (succ_nth_stream_eq : IntFractPair.stream q (n + 1) = Option.none),
    Eq.{u_1 + 1} (α := Option (Pair K))
      (Option.map (Pair.map Rat.cast) (Option.map (fun (p : IntFractPair ℚ) ↦ { a := 1, b := (↑p.b : ℚ) }) Option.none))
      (Option.map (fun (p : IntFractPair K) ↦ { a := 1, b := (↑p.b : K) })
        (Stream'.map (Option.map (IntFractPair.mapFr Rat.cast)) (IntFractPair.stream q) (n + 1)))
some :
  ∀ (b : ℤ) (fr : ℚ) (succ_nth_stream_eq : IntFractPair.stream q (n + 1) = Option.some { b := b, fr := fr }),
    Eq.{u_1 + 1} (α := Option (Pair K))
      (Option.map (Pair.map Rat.cast)
        (Option.map (fun (p : IntFractPair ℚ) ↦ { a := 1, b := (↑p.b : ℚ) })
          (Option.some { b := b, fr := fr : IntFractPair ℚ })))
      (Option.map (fun (p : IntFractPair K) ↦ { a := 1, b := (↑p.b : K) })
        (Stream'.map (Option.map (IntFractPair.mapFr Rat.cast)) (IntFractPair.stream q) (n + 1)))
⊢ Eq.{u_1 + 1} (α := Option (Pair K))
    (Option.map (Pair.map Rat.cast)
      (Option.map (fun (p : IntFractPair ℚ) ↦ { a := 1, b := (↑p.b : ℚ) }) (IntFractPair.stream q (n + 1))))
    (Option.map (fun (p : IntFractPair K) ↦ { a := 1, b := (↑p.b : K) })
      (Stream'.map (Option.map (IntFractPair.mapFr Rat.cast)) (IntFractPair.stream q) (n + 1)))

Tactic:
rcases succ_nth_stream_eq : IntFractPair.stream q (n + 1) with (_ | ⟨_, _⟩)

Premises used: GenContFract.IntFractPair.stream, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
n : ℕ
succ_nth_stream_eq : IntFractPair.stream q (n + 1) = none
⊢ Eq.{u_1 + 1} (α := Option (Pair K))
    (Option.map (Pair.map Rat.cast) (Option.map (fun (p : IntFractPair ℚ) ↦ { a := 1, b := (↑p.b : ℚ) }) none))
    (Option.map (fun (p : IntFractPair K) ↦ { a := 1, b := (↑p.b : K) })
      (Stream'.map (Option.map (IntFractPair.mapFr Rat.cast)) (IntFractPair.stream q) (n + 1)))

Tactic:
simp [Stream'.map, Stream'.get, succ_nth_stream_eq]

Premises used: Stream'.get, Stream'.map
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
n : ℕ
b : ℤ
fr : ℚ
succ_nth_stream_eq : IntFractPair.stream q (n + 1) = some { b := b, fr := fr }
⊢ Eq.{u_1 + 1} (α := Option (Pair K))
    (Option.map (Pair.map Rat.cast)
      (Option.map (fun (p : IntFractPair ℚ) ↦ { a := 1, b := (↑p.b : ℚ) })
        (some { b := b, fr := fr : IntFractPair ℚ })))
    (Option.map (fun (p : IntFractPair K) ↦ { a := 1, b := (↑p.b : K) })
      (Stream'.map (Option.map (IntFractPair.mapFr Rat.cast)) (IntFractPair.stream q) (n + 1)))

Tactic:
simp [Stream'.map, Stream'.get, succ_nth_stream_eq]

Premises used: Stream'.get, Stream'.map
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
h :
  ∀ (n : ℕ) (a : Pair K),
    Stream'.Seq.get? (Stream'.Seq.map (Pair.map Rat.cast) (of q).s) n = some a ↔ (of v).s.get? n = some a
⊢ Stream'.Seq.map (Pair.map Rat.cast) (of q).s = (of v).s

Tactic:
ext n
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
n : ℕ
a : Pair K
h :
  Stream'.Seq.get? (Stream'.Seq.map (Pair.map Rat.cast) (of q).s) n = some a ↔
    Option.map (Pair.map Rat.cast) ((of q).s.get? n) = some a
⊢ Stream'.Seq.get? (Stream'.Seq.map (Pair.map Rat.cast) (of q).s) n = some a ↔ (of v).s.get? n = some a

Tactic:
rw [← coe_of_s_get?_rat_eq v_eq_q]

Premises used: GenContFract.coe_of_s_get?_rat_eq
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
n : ℕ
a : Pair K
⊢ Stream'.Seq.get? (Stream'.Seq.map (Pair.map Rat.cast) (of q).s) n = some a ↔
    Option.map (Pair.map Rat.cast) ((of q).s.get? n) = some a

Tactic:
rfl
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
rcases :
  ∀ (h : K) (s : Stream'.Seq (Pair K)) (gcf_v_eq : of v = { h := h, s := s }),
    { h := (↑(of q).h : K), s := Stream'.Seq.map (Pair.map Rat.cast) (of q).s } = { h := h, s := s : GenContFract K }
⊢ { h := (↑(of q).h : K), s := Stream'.Seq.map (Pair.map Rat.cast) (of q).s } = of v

Tactic:
rcases gcf_v_eq : of v with ⟨h, s⟩

Premises used: GenContFract.s, GenContFract.of, GenContFract.h
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
h : K
s : Stream'.Seq (Pair K)
gcf_v_eq : of v = { h := h, s := s }
⊢ of (↑q : K) = { h := h, s := s : GenContFract K }

Tactic:
subst v
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
q : ℚ
h : K
s : Stream'.Seq (Pair K)
gcf_v_eq : of (↑q : K) = { h := h, s := s : GenContFract K }
⊢ (↑(Int.floor.{u_1} (α := K) (↑q : K)) : K) = h

Tactic:
injection gcf_v_eq
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
q : ℚ
h : K
s : Stream'.Seq (Pair K)
gcf_v_eq : of (↑q : K) = { h := h, s := s : GenContFract K }
obtain :
  ∀ (gcf_v_eq : of (↑q : K) = { h := (↑(Int.floor.{u_1} (α := K) (↑q : K)) : K), s := s : GenContFract K }),
    { h := (↑(of q).h : K), s := Stream'.Seq.map (Pair.map Rat.cast) (of q).s } =
      { h := (↑(Int.floor.{u_1} (α := K) (↑q : K)) : K), s := s : GenContFract K }
⊢ { h := (↑(of q).h : K), s := Stream'.Seq.map (Pair.map Rat.cast) (of q).s } = { h := h, s := s : GenContFract K }

Tactic:
obtain rfl : ↑⌊(q : K)⌋ = h := by injection gcf_v_eq

Premises used: Rat.cast, rfl
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
q : ℚ
s : Stream'.Seq (Pair K)
gcf_v_eq : of (↑q : K) = { h := (↑(Int.floor.{u_1} (α := K) (↑q : K)) : K), s := s : GenContFract K }
⊢ { h := (↑(of q).h : K), s := Stream'.Seq.map (Pair.map Rat.cast) (of q).s } =
    { h := (↑(Int.floor.{u_1} (α := K) (↑q : K)) : K), s := s : GenContFract K }

Tactic:
simp [coe_of_s_rat_eq rfl, gcf_v_eq]

Premises used: GenContFract.coe_of_s_rat_eq, rfl