awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
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)
have 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)
Tactic: rwa [stream_q_nth_eq] at IH
Cleared hypotheses: IH, stream_q_nth_eq, fr_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (hypothesis)
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
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)
have IH₁ : 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
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
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)
have norm_cast : fr⁻¹ = fr⁻¹
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (hypothesis)
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)
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)
have this : Eq.{u_1 + 1} (α := K) (↑fr : K)⁻¹ (↑fr⁻¹ : K)
Tactic: have : (fr : K)⁻¹ = ((fr⁻¹ : ℚ) : K) := by norm_cast
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (hypothesis)
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)
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)
have coe_of_fr : 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
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
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)
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
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 : ℕ
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream v n
have zero : Option.map (mapFr Rat.cast) (IntFractPair.stream q 0) = IntFractPair.stream v 0
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
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
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream v n
have 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)
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
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)
⊢ Stream'.map (Option.map (mapFr Rat.cast)) (IntFractPair.stream q) = IntFractPair.stream v
have h : ∀ (n : ℕ), Stream'.map (Option.map (mapFr Rat.cast)) (IntFractPair.stream q) n = IntFractPair.stream v n
Tactic: funext n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
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 : ℕ
⊢ Option.map (Pair.map Rat.cast) ((of q).s.get? n) = (of v).s.get? n
have 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) sorry) (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) sorry) (n + 1)))
Tactic: simp only [of, IntFractPair.seq1, Stream'.Seq.map_get?, Stream'.Seq.get?_tail]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
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 : ℕ
⊢ 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)))
have 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)))
Tactic: simp only [Stream'.Seq.get?]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
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 : ℕ
⊢ 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)))
have 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)))
Tactic: rw [← IntFractPair.coe_stream'_rat_eq v_eq_q]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
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 : ℕ
⊢ 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)))
have none : ∀ (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: rcases succ_nth_stream_eq : IntFractPair.stream q (n + 1) with (_ | ⟨_, _⟩)
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
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)))
⊢ 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)))
have some : ∀ (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: rcases succ_nth_stream_eq : IntFractPair.stream q (n + 1) with (_ | ⟨_, _⟩)
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
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)
⊢ Stream'.Seq.map (Pair.map Rat.cast) (of q).s = (of v).s
have 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
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
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 ↔ (of v).s.get? n = some a
have 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
Tactic: rw [← coe_of_s_get?_rat_eq v_eq_q]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
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 := (↑(of q).h : K), s := Stream'.Seq.map (Pair.map Rat.cast) (of q).s } = of v
have 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 }
Tactic: rcases gcf_v_eq : of v with ⟨h, s⟩
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (hypothesis)
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 }
⊢ { h := (↑(of q).h : K), s := Stream'.Seq.map (Pair.map Rat.cast) (of q).s } = { h := h, s := s : GenContFract K }
have gcf_v_eq₁ : of (↑q : K) = { h := h, s := s : GenContFract K }
Tactic: subst v
Cleared hypotheses: v, v_eq_q, gcf_v_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
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 }
⊢ { h := (↑(of q).h : K), s := Stream'.Seq.map (Pair.map Rat.cast) (of q).s } = { h := h, s := s : GenContFract K }
have 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 }
Tactic: obtain rfl : ↑⌊(q : K)⌋ = h := by injection gcf_v_eq
Cleared hypotheses: h, gcf_v_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
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 v).Terminates ↔ (of q).Terminates
have mp : (of v).Terminates → (of q).Terminates
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
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)
mp : (of v).Terminates → (of q).Terminates
⊢ (of v).Terminates ↔ (of q).Terminates
have mpr : (of q).Terminates → (of v).Terminates
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
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 : (of v).Terminates
⊢ (of q).Terminates
have mp : ∀ (n : ℕ) (h : (of v).s.TerminatedAt n), (of q).Terminates
Tactic: obtain ⟨n, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
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 : (of q).Terminates
⊢ (of v).Terminates
have mpr : ∀ (n : ℕ) (h : (of q).s.TerminatedAt n), (of v).Terminates
Tactic: obtain ⟨n, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
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 : ℕ
h : (of v).s.TerminatedAt n
⊢ (of q).Terminates
have h₁ : (of q).s.TerminatedAt n
Tactic: use n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
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 : ℕ
h : (of q).s.TerminatedAt n
⊢ (of v).Terminates
have h₁ : (of v).s.TerminatedAt n
Tactic: use n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (hypothesis)
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 : ℕ
h : (of v).s.TerminatedAt n
⊢ (of q).s.TerminatedAt n
have h₁ : Eq.{u_1 + 1} (α := Option (Pair K)) (Option.map (Pair.map Rat.cast) ((of q).s.get? n)) none
Tactic: simp only [Stream'.Seq.TerminatedAt, (coe_of_s_get?_rat_eq v_eq_q n).symm] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
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 : ℕ
h : (of q).s.TerminatedAt n
⊢ (of v).s.TerminatedAt n
have h₁ : Eq.{u_1 + 1} (α := Option (Pair K)) (Option.map (Pair.map Rat.cast) ((of q).s.get? n)) none
Tactic: simp only [Stream'.Seq.TerminatedAt, (coe_of_s_get?_rat_eq v_eq_q n).symm] at h ⊢
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
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 : ℕ
h : Eq.{u_1 + 1} (α := Option (Pair K)) (Option.map (Pair.map Rat.cast) ((of q).s.get? n)) none
⊢ (of q).s.get? n = none
have h₁ : ∀ (h' : (of q).s.get? n = none), Eq (α := Option (Pair ℚ)) none none
Tactic: cases h' : (of q).s.get? n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
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 : ℕ
h : Eq.{u_1 + 1} (α := Option (Pair K)) (Option.map (Pair.map Rat.cast) ((of q).s.get? n)) none
h₁ : ∀ (h' : (of q).s.get? n = none), Eq (α := Option (Pair ℚ)) none none
⊢ (of q).s.get? n = none
have h₂ : ∀ (val : Pair ℚ) (h' : (of q).s.get? n = some val), some val = none
Tactic: cases h' : (of q).s.get? n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
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 : ℕ
h : (of q).s.get? n = none
⊢ Eq.{u_1 + 1} (α := Option (Pair K)) (Option.map (Pair.map Rat.cast) ((of q).s.get? n)) none
have h₁ : ∀ (h' : (of q).s.get? n = none), Eq.{u_1 + 1} (α := Option (Pair K)) (Option.map (Pair.map Rat.cast) none) none
Tactic: cases h' : (of q).s.get? n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
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 : ℕ
h : (of q).s.get? n = none
h₁ : ∀ (h' : (of q).s.get? n = none), Eq.{u_1 + 1} (α := Option (Pair K)) (Option.map (Pair.map Rat.cast) none) none
⊢ Eq.{u_1 + 1} (α := Option (Pair K)) (Option.map (Pair.map Rat.cast) ((of q).s.get? n)) none
have h₂ : ∀ (val : Pair ℚ) (h' : (of q).s.get? n = some val),
  Eq.{u_1 + 1} (α := Option (Pair K)) (Option.map (Pair.map Rat.cast) (some val)) none
Tactic: cases h' : (of q).s.get? n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (hypothesis)
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 : ℕ
h : Eq.{u_1 + 1} (α := Option (Pair K)) (Option.map (Pair.map Rat.cast) ((of q).s.get? n)) none
h' : (of q).s.get? n = none
⊢ Eq (α := Option (Pair ℚ)) none none
have h₁ : Eq.{u_1 + 1} (α := Option (Pair K)) (Option.map (Pair.map Rat.cast) none) none
Tactic: simp only [h'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (hypothesis)
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 : ℕ
h : Eq.{u_1 + 1} (α := Option (Pair K)) (Option.map (Pair.map Rat.cast) ((of q).s.get? n)) none
val : Pair ℚ
h' : (of q).s.get? n = some val
⊢ some val = none
have h₁ : Eq.{u_1 + 1} (α := Option (Pair K)) (Option.map (Pair.map Rat.cast) (some val)) none
Tactic: simp only [h'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (hypothesis)
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 : ℕ
h h' : (of q).s.get? n = none
⊢ Eq.{u_1 + 1} (α := Option (Pair K)) (Option.map (Pair.map Rat.cast) none) none
have h₁ : True
Tactic: simp only [h'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (hypothesis)
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 : ℕ
h : (of q).s.get? n = none
val : Pair ℚ
h' : (of q).s.get? n = some val
⊢ Eq.{u_1 + 1} (α := Option (Pair K)) (Option.map (Pair.map Rat.cast) (some val)) none
have h₁ : some val = none
Tactic: simp only [h'] at h
Cleared hypotheses: h