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
q : ℚ
v_eq_q : v = (↑q : K)
mp : (of v).Terminates → (of q).Terminates
mpr : (of q).Terminates → (of v).Terminates
⊢ (of v).Terminates ↔ (of q).Terminates

Tactic:
constructor
-- 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 : (of v).Terminates
mp : ∀ (n : ℕ) (h : (of v).s.TerminatedAt n), (of q).Terminates
⊢ (of q).Terminates

Tactic:
obtain ⟨n, h⟩ := 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 : (of q).Terminates
mpr : ∀ (n : ℕ) (h : (of q).s.TerminatedAt n), (of v).Terminates
⊢ (of v).Terminates

Tactic:
obtain ⟨n, h⟩ := 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)
n : ℕ
h : (of v).s.TerminatedAt n
h₁ : (of q).s.TerminatedAt n
⊢ (of q).Terminates

Tactic:
use 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 : ℕ
h : (of q).s.TerminatedAt n
h₁ : (of v).s.TerminatedAt n
⊢ (of v).Terminates

Tactic:
use 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 : ℕ
h : (of v).s.TerminatedAt n
⊢ 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 ⊢

Premises used: Stream'.Seq.TerminatedAt, GenContFract.coe_of_s_get?_rat_eq, 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 : ℕ
h : (of q).s.TerminatedAt n
h₁ : Eq.{u_1 + 1} (α := Option (Pair K)) (Option.map (Pair.map Rat.cast) ((of q).s.get? n)) none
⊢ (of v).s.TerminatedAt n

Tactic:
simp only [Stream'.Seq.TerminatedAt, (coe_of_s_get?_rat_eq v_eq_q n).symm] at h ⊢

Premises used: Stream'.Seq.TerminatedAt, GenContFract.coe_of_s_get?_rat_eq, 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 : ℕ
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
h₂ : ∀ (val : Pair ℚ) (h' : (of q).s.get? n = some val), some val = none
⊢ (of q).s.get? n = none

Tactic:
cases h' : (of q).s.get? n

Premises used: GenContFract.s, GenContFract.of, 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 : ℕ
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
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
⊢ Eq.{u_1 + 1} (α := Option (Pair K)) (Option.map (Pair.map Rat.cast) ((of q).s.get? n)) none

Tactic:
cases h' : (of q).s.get? n

Premises used: GenContFract.s, GenContFract.of, 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 : ℕ
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.{u_1 + 1} (α := Option (Pair K)) (Option.map (Pair.map Rat.cast) none) none

Tactic:
simp only [h'] at 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)
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
⊢ Eq.{u_1 + 1} (α := Option (Pair K)) (Option.map (Pair.map Rat.cast) (some val)) none

Tactic:
simp only [h'] at 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)
n : ℕ
h h' : (of q).s.get? n = none
⊢ True

Tactic:
simp only [h'] at 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)
n : ℕ
h : (of q).s.get? n = none
val : Pair ℚ
h' : (of q).s.get? n = some val
⊢ some val = none

Tactic:
simp only [h'] at 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)
n : ℕ
h' : (of q).s.get? n = none
h : Eq.{u_1 + 1} (α := Option (Pair K)) (Option.map (Pair.map Rat.cast) none) none
⊢ Eq (α := Option (Pair ℚ)) none none

Tactic:
trivial
-- 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 : ℕ
val : Pair ℚ
h' : (of q).s.get? n = some val
h : Eq.{u_1 + 1} (α := Option (Pair K)) (Option.map (Pair.map Rat.cast) (some val)) none
⊢ some val = none

Tactic:
trivial
-- 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 : ℕ
h' : (of q).s.get? n = none
h : True
⊢ Eq.{u_1 + 1} (α := Option (Pair K)) (Option.map (Pair.map Rat.cast) none) none

Tactic:
trivial
-- 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 : ℕ
val : Pair ℚ
h' : (of q).s.get? n = some val
h : some val = none
⊢ Eq.{u_1 + 1} (α := Option (Pair K)) (Option.map (Pair.map Rat.cast) (some val)) none

Tactic:
trivial
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
q : ℚ
q_pos : 0 < q
⊢ (IntFractPair.of q⁻¹).fr.num < q.num

Tactic:
Rat.fract_inv_num_lt_num_of_pos q_pos

Premises used: Rat.fract_inv_num_lt_num_of_pos
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
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 ℚ),
    IntFractPair.stream q n = some ifp_n' ∧ ifp_n'.fr ≠ 0 ∧ IntFractPair.of ifp_n'.fr⁻¹ = ifp_succ_n

Tactic:
succ_nth_stream_eq_some_iff.mp stream_succ_nth_eq

Premises used: Iff.mp, GenContFract.IntFractPair.succ_nth_stream_eq_some_iff
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
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
obtain :
  ∀ (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
⊢ ifp_succ_n.fr.num < ifp_n.fr.num

Tactic:
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 :=
    succ_nth_stream_eq_some_iff.mp stream_succ_nth_eq

Premises used: GenContFract.IntFractPair.stream, Iff.mp, GenContFract.IntFractPair.succ_nth_stream_eq_some_iff
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
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'

Tactic:
injection Eq.trans stream_nth_eq.symm stream_nth_eq'

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
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'

Tactic:
have : ifp_n = ifp_n' := by injection Eq.trans stream_nth_eq.symm stream_nth_eq'
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
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'
⊢ IntFractPair.stream q n = some ifp_n

Tactic:
cases this
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
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'
stream_nth_eq'₁ : IntFractPair.stream q n = some ifp_n
⊢ ifp_n.fr ≠ 0

Tactic:
cases this
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
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'
stream_nth_eq'₁ : IntFractPair.stream q n = some ifp_n
ifp_n_fract_ne_zero₁ : ifp_n.fr ≠ 0
⊢ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n

Tactic:
cases this
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
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
refl : (IntFractPair.of ifp_n.fr⁻¹).fr.num < ifp_n.fr.num
⊢ ifp_succ_n.fr.num < ifp_n.fr.num

Tactic:
rw [← IntFractPair.of_eq_ifp_succ_n]
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
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
⊢ 0 ≤ ifp_n.fr

Tactic:
obtain ⟨zero_le_ifp_n_fract, _⟩ := nth_stream_fr_nonneg_lt_one stream_nth_eq

Premises used: GenContFract.IntFractPair.nth_stream_fr_nonneg_lt_one
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
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.fr < 1

Tactic:
obtain ⟨zero_le_ifp_n_fract, _⟩ := nth_stream_fr_nonneg_lt_one stream_nth_eq

Premises used: GenContFract.IntFractPair.nth_stream_fr_nonneg_lt_one
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
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
right : ifp_n.fr < 1
⊢ 0 < ifp_n.fr

Tactic:
have : 0 < ifp_n.fr := lt_of_le_of_ne zero_le_ifp_n_fract <| ifp_n_fract_ne_zero.symm
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
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
right : ifp_n.fr < 1
this : 0 < ifp_n.fr
⊢ (IntFractPair.of ifp_n.fr⁻¹).fr.num < ifp_n.fr.num

Tactic:
of_inv_fr_num_lt_num_of_pos this

Premises used: GenContFract.IntFractPair.of_inv_fr_num_lt_num_of_pos
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
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
right : ifp_n.fr < 1
this : 0 < ifp_n.fr
⊢ (IntFractPair.of ifp_n.fr⁻¹).fr.num < ifp_n.fr.num

Tactic:
exact of_inv_fr_num_lt_num_of_pos this

Premises used: GenContFract.IntFractPair.of_inv_fr_num_lt_num_of_pos
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
q : ℚ
n : ℕ
ifp_zero : IntFractPair ℚ
stream_zero_eq : IntFractPair.stream q 0 = some ifp_zero
⊢ IntFractPair.of q = ifp_zero

Tactic:
injection stream_zero_eq
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
q : ℚ
n : ℕ
ifp_zero : IntFractPair ℚ
stream_zero_eq : IntFractPair.stream q 0 = some ifp_zero
⊢ IntFractPair.of q = ifp_zero

Tactic:
have : IntFractPair.of q = ifp_zero := by injection stream_zero_eq
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
q : ℚ
n : ℕ
ifp_zero : IntFractPair ℚ
stream_zero_eq : IntFractPair.stream q 0 = some ifp_zero
this : IntFractPair.of q = ifp_zero
⊢ ifp_zero.fr.num ≤ (IntFractPair.of q).fr.num - (↑0 : ℤ)

Tactic:
simp [this.symm]

Premises used: Eq.symm
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
q : ℚ
n_1 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 (n + 1) = some ifp_succ_n
this : ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - (↑n : ℤ)
rw : ifp_succ_n.fr.num ≤ (IntFractPair.of q).fr.num - (↑n : ℤ) - 1
⊢ ifp_succ_n.fr.num ≤ (IntFractPair.of q).fr.num - (↑(n + 1) : ℤ)

Tactic:
rw [Int.natCast_succ, sub_add_eq_sub_sub]

Premises used: Int.natCast_succ, sub_add_eq_sub_sub
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
q : ℚ
n_1 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 (n + 1) = 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

Tactic:
solve_by_elim [le_sub_right_of_add_le]

Premises used: le_sub_right_of_add_le
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
q : ℚ
n_1 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 (n + 1) = some ifp_succ_n
succ : ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - (↑n : ℤ)
⊢ ifp_succ_n.fr.num ≤ (IntFractPair.of q).fr.num - (↑(n + 1) : ℤ)

Tactic:
suffices ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - n by
      rw [Int.natCast_succ, sub_add_eq_sub_sub]
      solve_by_elim [le_sub_right_of_add_le]
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
q : ℚ
n_1 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 (n + 1) = some ifp_succ_n
succ :
  ∀ (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 : ℤ)
⊢ ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - (↑n : ℤ)

Tactic:
rcases succ_nth_stream_eq_some_iff.mp stream_succ_nth_eq with ⟨ifp_n, stream_nth_eq, -⟩

Premises used: Iff.mp, GenContFract.IntFractPair.succ_nth_stream_eq_some_iff
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
q : ℚ
n_1 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 (n + 1) = some ifp_succ_n
ifp_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
⊢ ifp_succ_n.fr.num < ifp_n.fr.num

Tactic:
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
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
q : ℚ
n_1 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 (n + 1) = 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 : ℤ)

Tactic:
le_trans this (IH stream_nth_eq)

Premises used: le_trans
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
q : ℚ
n_1 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 (n + 1) = 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 : ℤ)

Tactic:
exact le_trans this (IH stream_nth_eq)

Premises used: le_trans
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
q : ℚ
n : ℕ
zero :
  ∀ {ifp_n : IntFractPair ℚ},
    IntFractPair.stream q 0 = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - (↑0 : ℤ)
succ :
  ∀ (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 (n + 1) = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - (↑(n + 1) : ℤ)
⊢ ∀ {ifp_n : IntFractPair ℚ},
    IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - (↑n : ℤ)

Tactic:
induction n with
  | zero =>
    intro ifp_zero stream_zero_eq
    have : IntFractPair.of q = ifp_zero := by injection stream_zero_eq
    simp [this.symm]
  | succ n IH =>
    intro ifp_succ_n stream_succ_nth_eq
    suffices ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - n by
      rw [Int.natCast_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
    exact le_trans this (IH stream_nth_eq)
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := fract_q_num.natAbs + 1
none : ∀ (stream_nth_eq : IntFractPair.stream q n = Option.none), ∃ (n : ℕ), IntFractPair.stream q n = Option.none
some :
  ∀ (ifp : IntFractPair ℚ) (stream_nth_eq : IntFractPair.stream q n = Option.some ifp),
    ∃ (n : ℕ), IntFractPair.stream q n = Option.none
⊢ ∃ (n : ℕ), IntFractPair.stream q n = Option.none

Tactic:
rcases stream_nth_eq : IntFractPair.stream q n with ifp | ifp

Premises used: GenContFract.IntFractPair.stream
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := fract_q_num.natAbs + 1
stream_nth_eq : IntFractPair.stream q n = none
w : ℕ
h : IntFractPair.stream q n = none
⊢ ∃ (n : ℕ), IntFractPair.stream q n = none

Tactic:
use n, stream_nth_eq
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := fract_q_num.natAbs + 1
ifp : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp
⊢ ifp.fr.num ≤ fract_q_num - (↑n : ℤ)

Tactic:
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
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := fract_q_num.natAbs + 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 : ℤ)
⊢ 0 ≤ fract_q_num

Tactic:
have : 0 ≤ fract_q_num := Rat.num_nonneg.mpr (Int.fract_nonneg q)
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := fract_q_num.natAbs + 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

Tactic:
simp only [n, Nat.cast_add, Int.natAbs_of_nonneg this, Nat.cast_one,
        sub_add_eq_sub_sub_swap, sub_right_comm, sub_self, zero_sub]

Premises used: sub_self, sub_right_comm, Int.natAbs_of_nonneg, Nat.cast_add, Nat.cast_one, zero_sub, sub_add_eq_sub_sub_swap