awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
rw : (↑(q₁.den.gcd q₂.den) : ℤ) ∣ q₁.num * (↑q₂.den : ℤ) + q₂.num * (↑q₁.den : ℤ)
⊢ q₁.den.gcd q₂.den ∣ (q₁.num * (↑q₂.den : ℤ) + q₂.num * (↑q₁.den : ℤ)).natAbs

Tactic:
rw [← Int.natCast_dvd_natCast, Int.dvd_natAbs]

Premises used: Int.dvd_natAbs, Int.natCast_dvd_natCast
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
a : (↑(q₁.den.gcd q₂.den) : ℤ) ∣ q₁.num * (↑q₂.den : ℤ)
a₁ : (↑(q₁.den.gcd q₂.den) : ℤ) ∣ q₂.num * (↑q₁.den : ℤ)
⊢ (↑(q₁.den.gcd q₂.den) : ℤ) ∣ q₁.num * (↑q₂.den : ℤ) + q₂.num * (↑q₁.den : ℤ)

Tactic:
apply Int.dvd_add

Premises used: Int.dvd_add
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
a : Dvd.dvd (α := ℤ) (↑(q₁.den.gcd q₂.den) : ℤ) (↑q₂.den : ℤ)
⊢ (↑(q₁.den.gcd q₂.den) : ℤ) ∣ q₁.num * (↑q₂.den : ℤ)

Tactic:
apply dvd_mul_of_dvd_right

Premises used: dvd_mul_of_dvd_right
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
a : Dvd.dvd (α := ℤ) (↑(q₁.den.gcd q₂.den) : ℤ) (↑q₁.den : ℤ)
⊢ (↑(q₁.den.gcd q₂.den) : ℤ) ∣ q₂.num * (↑q₁.den : ℤ)

Tactic:
apply dvd_mul_of_dvd_right

Premises used: dvd_mul_of_dvd_right
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
a : q₁.den.gcd q₂.den ∣ q₂.den
⊢ Dvd.dvd (α := ℤ) (↑(q₁.den.gcd q₂.den) : ℤ) (↑q₂.den : ℤ)

Tactic:
rw [Int.natCast_dvd_natCast]

Premises used: Int.natCast_dvd_natCast
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
a : q₁.den.gcd q₂.den ∣ q₁.den
⊢ Dvd.dvd (α := ℤ) (↑(q₁.den.gcd q₂.den) : ℤ) (↑q₁.den : ℤ)

Tactic:
rw [Int.natCast_dvd_natCast]

Premises used: Int.natCast_dvd_natCast
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
⊢ q₁.den.gcd q₂.den ∣ q₂.den

Tactic:
Nat.gcd_dvd_right _ _

Premises used: Nat.gcd_dvd_right
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
⊢ q₁.den.gcd q₂.den ∣ q₂.den

Tactic:
exact Nat.gcd_dvd_right _ _

Premises used: Nat.gcd_dvd_right
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
⊢ q₁.den.gcd q₂.den ∣ q₁.den

Tactic:
Nat.gcd_dvd_left _ _

Premises used: Nat.gcd_dvd_left
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
⊢ q₁.den.gcd q₂.den ∣ q₁.den

Tactic:
exact Nat.gcd_dvd_left _ _

Premises used: Nat.gcd_dvd_left
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
a : (↑(q₁.den.gcd q₂.den) : ℤ) ∣ q₁.num * (↑q₂.den : ℤ)
a₁ : (↑(q₁.den.gcd q₂.den) : ℤ) ∣ q₂.num * (↑q₁.den : ℤ)
a₂ : (↑(q₁.den.gcd q₂.den) : ℤ) ∣ q₁.num * (↑q₂.den : ℤ)
a₃ : (↑(q₁.den.gcd q₂.den) : ℤ) ∣ q₂.num * (↑q₁.den : ℤ)
a₄ : (↑(q₁.den.gcd q₂.den) : ℤ) ∣ q₁.num * (↑q₂.den : ℤ)
a₅ : (↑(q₁.den.gcd q₂.den) : ℤ) ∣ q₂.num * (↑q₁.den : ℤ)
a₆ : (↑(q₁.den.gcd q₂.den) : ℤ) ∣ q₁.num * (↑q₂.den : ℤ)
a₇ : (↑(q₁.den.gcd q₂.den) : ℤ) ∣ q₂.num * (↑q₁.den : ℤ)
a₈ : Dvd.dvd (α := ℤ) (↑(q₁.den.gcd q₂.den) : ℤ) (↑q₂.den : ℤ)
a₉ : Dvd.dvd (α := ℤ) (↑(q₁.den.gcd q₂.den) : ℤ) (↑q₁.den : ℤ)
a₁₀ : Dvd.dvd (α := ℤ) (↑(q₁.den.gcd q₂.den) : ℤ) (↑q₂.den : ℤ)
a₁₁ : Dvd.dvd (α := ℤ) (↑(q₁.den.gcd q₂.den) : ℤ) (↑q₁.den : ℤ)
a₁₂ : Dvd.dvd (α := ℤ) (↑(q₁.den.gcd q₂.den) : ℤ) (↑q₂.den : ℤ)
a₁₃ : Dvd.dvd (α := ℤ) (↑(q₁.den.gcd q₂.den) : ℤ) (↑q₁.den : ℤ)
a₁₄ : Dvd.dvd (α := ℤ) (↑(q₁.den.gcd q₂.den) : ℤ) (↑q₂.den : ℤ)
a₁₅ : Dvd.dvd (α := ℤ) (↑(q₁.den.gcd q₂.den) : ℤ) (↑q₁.den : ℤ)
a₁₆ : q₁.den.gcd q₂.den ∣ q₂.den
a₁₇ : q₁.den.gcd q₂.den ∣ q₁.den
a₁₈ : q₁.den.gcd q₂.den ∣ q₂.den
a₁₉ : q₁.den.gcd q₂.den ∣ q₁.den
⊢ (↑(q₁.den.gcd q₂.den) : ℤ) ∣ q₁.num * (↑q₂.den : ℤ) + q₂.num * (↑q₁.den : ℤ)

Tactic:
apply Int.dvd_add
    <;> apply dvd_mul_of_dvd_right <;> rw [Int.natCast_dvd_natCast]
    <;> [exact Nat.gcd_dvd_right _ _; exact Nat.gcd_dvd_left _ _]

Premises used: Nat.gcd_dvd_left, dvd_mul_of_dvd_right, Int.dvd_add, Nat.gcd_dvd_right, Int.natCast_dvd_natCast
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
⊢ (q₁ - q₂).den ∣ q₁.den.lcm q₂.den

Tactic:
simpa only [sub_eq_add_neg, neg_den] using add_den_dvd_lcm q₁ (-q₂)

Premises used: Rat.add_den_dvd_lcm, sub_eq_add_neg, Rat.neg_den, Neg.neg
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
⊢ (q₁ + q₂).den ∣ q₁.den * q₂.den

Tactic:
(add_den_dvd_lcm _ _).trans (Nat.lcm_dvd_mul _ _)

Premises used: Rat.add_den_dvd_lcm, Nat.lcm_dvd_mul, Dvd.dvd.trans
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
⊢ (q₁ - q₂).den ∣ q₁.den * q₂.den

Tactic:
(sub_den_dvd_lcm _ _).trans (Nat.lcm_dvd_mul _ _)

Premises used: Rat.sub_den_dvd_lcm, Nat.lcm_dvd_mul, Dvd.dvd.trans
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
rw :
  { num := q₁.num * q₂.num / (↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) : ℤ),
        den := q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den), den_nz := ⋯, reduced := ⋯ : ℚ }.den ∣
    q₁.den * q₂.den
⊢ (q₁ * q₂).den ∣ q₁.den * q₂.den

Tactic:
rw [mul_def, normalize_eq]

Premises used: Rat.mul_def, Rat.normalize_eq
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
h : (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den) ∣ q₁.den * q₂.den
⊢ { num := q₁.num * q₂.num / (↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) : ℤ),
        den := q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den), den_nz := ⋯, reduced := ⋯ : ℚ }.den ∣
    q₁.den * q₂.den

Tactic:
apply Nat.div_dvd_of_dvd

Premises used: Nat.div_dvd_of_dvd
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
⊢ (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den) ∣ q₁.den * q₂.den

Tactic:
apply Nat.gcd_dvd_right

Premises used: Nat.gcd_dvd_right
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
rw :
  (normalize (q₁.num * q₂.num) (q₁.den * q₂.den) ⋯).num =
    q₁.num * q₂.num / (↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) : ℤ)
rw₁ rw₂ :
  { num := q₁.num * q₂.num / (↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) : ℤ),
        den := q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den), den_nz := ⋯, reduced := ⋯ : ℚ }.num =
    q₁.num * q₂.num / (↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) : ℤ)
⊢ (q₁ * q₂).num = q₁.num * q₂.num / (↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) : ℤ)

Tactic:
rw [mul_def, normalize_eq]

Premises used: Rat.mul_def, Rat.normalize_eq
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
rw :
  (normalize (q₁.num * q₂.num) (q₁.den * q₂.den) ⋯).den =
    q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)
rw₁ rw₂ :
  { num := q₁.num * q₂.num / (↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) : ℤ),
        den := q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den), den_nz := ⋯, reduced := ⋯ : ℚ }.den =
    q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)
⊢ (q₁ * q₂).den = q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)

Tactic:
rw [mul_def, normalize_eq]

Premises used: Rat.mul_def, Rat.normalize_eq
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
n : ℤ
a : (q + (↑n : ℚ)).den ∣ q.den
a₁ : q.den ∣ (q + (↑n : ℚ)).den
⊢ (q + (↑n : ℚ)).den = q.den

Tactic:
apply Nat.dvd_antisymm

Premises used: Nat.dvd_antisymm
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
n : ℤ
⊢ (q + (↑n : ℚ)).den ∣ q.den

Tactic:
simpa using add_den_dvd q n

Premises used: Int.cast, Rat.add_den_dvd
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
n : ℤ
⊢ q.den ∣ (q + (↑n : ℚ)).den

Tactic:
simpa using add_den_dvd (q + n) (-n)

Premises used: Int.cast, HAdd.hAdd, Rat.add_den_dvd, Neg.neg
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
n : ℤ
q : ℚ
rw : (q + (↑n : ℚ)).den = q.den
rw₁ rw₂ : q.den = q.den
⊢ ((↑n : ℚ) + q).den = q.den

Tactic:
rw [add_comm, add_intCast_den]

Premises used: add_comm, Rat.add_intCast_den
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
n : ℤ
rw : (q + -(↑n : ℚ)).den = q.den
rw₁ : (q + (↑(-n) : ℚ)).den = q.den
rw₂ rw₃ : q.den = q.den
⊢ (q - (↑n : ℚ)).den = q.den

Tactic:
rw [sub_eq_add_neg, ← Int.cast_neg, add_intCast_den]

Premises used: Int.cast_neg, sub_eq_add_neg, Rat.add_intCast_den
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
n : ℤ
q : ℚ
rw : ((↑n : ℚ) + -q).den = q.den
rw₁ : (-q).den = q.den
rw₂ rw₃ : q.den = q.den
⊢ ((↑n : ℚ) - q).den = q.den

Tactic:
rw [sub_eq_add_neg, intCast_add_den, neg_den]

Premises used: sub_eq_add_neg, Rat.intCast_add_den, Rat.neg_den
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
n : ℕ
⊢ (q + (↑n : ℚ)).den = q.den

Tactic:
mod_cast add_intCast_den q n

Premises used: Int.cast_natCast, congrArg, cast, Rat.den, Nat.cast, Rat.add_intCast_den, HAdd.hAdd, congrFun', Eq
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
n : ℕ
q : ℚ
⊢ ((↑n : ℚ) + q).den = q.den

Tactic:
mod_cast intCast_add_den n q

Premises used: Int.cast_natCast, congrArg, cast, Rat.den, Rat.intCast_add_den, Nat.cast, HAdd.hAdd, congrFun', Eq
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
n : ℕ
⊢ (q - (↑n : ℚ)).den = q.den

Tactic:
mod_cast sub_intCast_den q n

Premises used: Int.cast_natCast, congrArg, HSub.hSub, cast, Rat.den, Nat.cast, congrFun', Eq, Rat.sub_intCast_den
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
n : ℕ
q : ℚ
⊢ ((↑n : ℚ) - q).den = q.den

Tactic:
mod_cast intCast_sub_den n q

Premises used: Int.cast_natCast, congrArg, HSub.hSub, cast, Rat.den, Nat.cast, Rat.intCast_sub_den, congrFun', Eq
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
n : ℕ
⊢ (q + OfNat.ofNat n).den = q.den

Tactic:
add_natCast_den q n

Premises used: Rat.add_natCast_den
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
n : ℕ
q : ℚ
⊢ (OfNat.ofNat n + q).den = q.den

Tactic:
natCast_add_den n q

Premises used: Rat.natCast_add_den
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
n : ℕ
⊢ (q - OfNat.ofNat n).den = q.den

Tactic:
sub_natCast_den ..

Premises used: Rat.sub_natCast_den
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
n : ℕ
q : ℚ
⊢ (OfNat.ofNat n - q).den = q.den

Tactic:
natCast_sub_den ..

Premises used: Rat.natCast_sub_den
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
rw :
  q₁.den * q₂.den =
    q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den) * (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)
⊢ q₁.den * q₂.den = (q₁ * q₂).den * (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)

Tactic:
rw [mul_den]

Premises used: Rat.mul_den
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
⊢ q₁.den * q₂.den =
    q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den) * (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)

Tactic:
((Nat.dvd_iff_div_mul_eq _ _).mp (Nat.gcd_dvd_right _ _)).symm

Premises used: Nat.dvd_iff_div_mul_eq, Iff.mp, Nat.gcd_dvd_right, Eq.symm
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
⊢ q₁.den * q₂.den =
    q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den) * (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)

Tactic:
exact ((Nat.dvd_iff_div_mul_eq _ _).mp (Nat.gcd_dvd_right _ _)).symm

Premises used: Nat.dvd_iff_div_mul_eq, Iff.mp, Nat.gcd_dvd_right, Eq.symm
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
rw :
  q₁.num * q₂.num =
    q₁.num * q₂.num / (↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) : ℤ) *
      (↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) : ℤ)
⊢ q₁.num * q₂.num = (q₁ * q₂).num * (↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) : ℤ)

Tactic:
rw [mul_num]

Premises used: Rat.mul_num
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
⊢ q₁.num * q₂.num =
    q₁.num * q₂.num / (↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) : ℤ) *
      (↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) : ℤ)

Tactic:
(Int.ediv_mul_cancel ?_).symm

Premises used: Int.ediv_mul_cancel, Eq.symm
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
refine : (↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) : ℤ) ∣ q₁.num * q₂.num
⊢ q₁.num * q₂.num =
    q₁.num * q₂.num / (↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) : ℤ) *
      (↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) : ℤ)

Tactic:
refine (Int.ediv_mul_cancel ?_).symm

Premises used: Int.ediv_mul_cancel, Eq.symm
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
rw : Dvd.dvd (α := ℤ) (↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) : ℤ) (↑(q₁.num * q₂.num).natAbs : ℤ)
⊢ (↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) : ℤ) ∣ q₁.num * q₂.num

Tactic:
rw [← Int.dvd_natAbs]

Premises used: Int.dvd_natAbs
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
⊢ Dvd.dvd (α := ℤ) (↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) : ℤ) (↑(q₁.num * q₂.num).natAbs : ℤ)

Tactic:
Int.ofNat_dvd.mpr (Nat.gcd_dvd_left _ _)

Premises used: Iff.mpr, Nat.gcd_dvd_left, Int.ofNat_dvd
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
⊢ Dvd.dvd (α := ℤ) (↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) : ℤ) (↑(q₁.num * q₂.num).natAbs : ℤ)

Tactic:
exact Int.ofNat_dvd.mpr (Nat.gcd_dvd_left _ _)

Premises used: Iff.mpr, Nat.gcd_dvd_left, Int.ofNat_dvd
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
rw : (q.num.natAbs * q.num.natAbs).Coprime (q.den * q.den)
⊢ (q * q).num = q.num * q.num

Tactic:
rw [mul_num, Int.natAbs_mul, Nat.Coprime.gcd_eq_one, Int.ofNat_one, Int.ediv_one]

Premises used: Int.natAbs_mul, Int.ediv_one, Nat.Coprime.gcd_eq_one, Int.ofNat_one, Rat.mul_num
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
⊢ (q.num.natAbs * q.num.natAbs).Coprime (q.den * q.den)

Tactic:
(q.reduced.mul_right q.reduced).mul_left (q.reduced.mul_right q.reduced)

Premises used: Rat.reduced, Nat.Coprime.mul_right, Nat.Coprime.mul_left
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
⊢ (q.num.natAbs * q.num.natAbs).Coprime (q.den * q.den)

Tactic:
exact (q.reduced.mul_right q.reduced).mul_left (q.reduced.mul_right q.reduced)

Premises used: Rat.reduced, Nat.Coprime.mul_right, Nat.Coprime.mul_left
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
rw : (q.num.natAbs * q.num.natAbs).Coprime (q.den * q.den)
⊢ (q * q).den = q.den * q.den

Tactic:
rw [Rat.mul_den, Int.natAbs_mul, Nat.Coprime.gcd_eq_one, Nat.div_one]

Premises used: Int.natAbs_mul, Nat.div_one, Nat.Coprime.gcd_eq_one, Rat.mul_den
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q r : ℚ
⊢ Ne (α := ℤ) (↑q.den : ℤ) 0

Tactic:
have hqd : (q.den : ℤ) ≠ 0 := Int.natCast_ne_zero_iff_pos.2 q.den_pos
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q r : ℚ
hqd : Ne (α := ℤ) (↑q.den : ℤ) 0
⊢ Ne (α := ℤ) (↑r.den : ℤ) 0

Tactic:
have hrd : (r.den : ℤ) ≠ 0 := Int.natCast_ne_zero_iff_pos.2 r.den_pos
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q r : ℚ
hqd : Ne (α := ℤ) (↑q.den : ℤ) 0
hrd : Ne (α := ℤ) (↑r.den : ℤ) 0
rw : (q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
| q + r

Tactic:
rw [← num_divInt_den q, ← num_divInt_den r, divInt_add_divInt _ _ hqd hrd]

Premises used: Rat.num_divInt_den, Rat.divInt_add_divInt
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q r : ℚ
hqd : Ne (α := ℤ) (↑q.den : ℤ) 0
hrd : Ne (α := ℤ) (↑r.den : ℤ) 0
conv_lhs :
  (q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) =
    (q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
⊢ q + r = (q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)

Tactic:
conv_lhs => rw [← num_divInt_den q, ← num_divInt_den r, divInt_add_divInt _ _ hqd hrd]

Premises used: Rat.num_divInt_den, Rat.divInt_add_divInt
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q r : ℚ
hqd : Ne (α := ℤ) (↑q.den : ℤ) 0
hrd : Ne (α := ℤ) (↑r.den : ℤ) 0
rw rw₁ :
  (q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) =
    (q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
⊢ (q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) =
    (q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)

Tactic:
rw [mul_comm r.num q.den]

Premises used: Rat.num, Rat.den, Nat.cast, mul_comm
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
mp : IsSquare q → IsSquare q.num ∧ IsSquare q.den
mpr : IsSquare q.num ∧ IsSquare q.den → IsSquare q
⊢ IsSquare q ↔ IsSquare q.num ∧ IsSquare q.den

Tactic:
constructor
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
qr : ℚ
mp : IsSquare (qr.num * qr.num) ∧ IsSquare (qr.den * qr.den)
⊢ IsSquare (qr * qr).num ∧ IsSquare (qr * qr).den

Tactic:
rw [Rat.mul_self_num, mul_self_den]

Premises used: Rat.mul_self_num, Rat.mul_self_den
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
qr : ℚ
⊢ IsSquare (qr.num * qr.num) ∧ IsSquare (qr.den * qr.den)

Tactic:
simp only [IsSquare.mul_self, and_self]

Premises used: and_self, IsSquare.mul_self
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
nr : ℤ
hnr : q.num = nr * nr
dr : ℕ
hdr : q.den = dr * dr
⊢ IsSquare q

Tactic:
⟨nr / dr, ?_⟩

Premises used: Int.cast, HDiv.hDiv, Nat.cast, IsSquare, Exists.intro
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
nr : ℤ
hnr : q.num = nr * nr
dr : ℕ
hdr : q.den = dr * dr
mpr : q = HDiv.hDiv (α := ℚ) (↑nr : ℚ) (↑dr : ℚ) * HDiv.hDiv (α := ℚ) (↑nr : ℚ) (↑dr : ℚ)
⊢ IsSquare q

Tactic:
refine ⟨nr / dr, ?_⟩
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
nr : ℤ
hnr : q.num = nr * nr
dr : ℕ
hdr : q.den = dr * dr
mpr : q = HMul.hMul (α := ℚ) (↑nr : ℚ) (↑nr : ℚ) / HMul.hMul (α := ℚ) (↑dr : ℚ) (↑dr : ℚ)
mpr₁ : q = (↑(nr * nr) : ℚ) / HMul.hMul (α := ℚ) (↑dr : ℚ) (↑dr : ℚ)
mpr₂ : q = HDiv.hDiv (α := ℚ) (↑(nr * nr) : ℚ) (↑(dr * dr) : ℚ)
mpr₃ : q = HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑(dr * dr) : ℚ)
mpr₄ : q = HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)
mpr₅ mpr₆ : q = q
⊢ q = HDiv.hDiv (α := ℚ) (↑nr : ℚ) (↑dr : ℚ) * HDiv.hDiv (α := ℚ) (↑nr : ℚ) (↑dr : ℚ)

Tactic:
rw [div_mul_div_comm, ← Int.cast_mul, ← Nat.cast_mul, ← hnr, ← hdr, num_div_den]

Premises used: Rat.num_div_den, div_mul_div_comm, Int.cast_mul, Nat.cast_mul
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
n : ℕ
simp_rw : IsSquare (num (↑n : ℚ)) ∧ IsSquare (den (↑n : ℚ)) ↔ IsSquare n
simp_rw₁ : IsSquare (α := ℤ) (↑n : ℤ) ∧ IsSquare (den (↑n : ℚ)) ↔ IsSquare n
simp_rw₂ : IsSquare (α := ℤ) (↑n : ℤ) ∧ IsSquare (α := ℕ) 1 ↔ IsSquare n
simp_rw₃ : IsSquare (α := ℤ) (↑n : ℤ) ∧ True ↔ IsSquare n
simp_rw₄ : IsSquare (α := ℤ) (↑n : ℤ) ↔ IsSquare n
⊢ IsSquare (α := ℚ) (↑n : ℚ) ↔ IsSquare n

Tactic:
simp_rw [isSquare_iff, num_natCast, den_natCast, IsSquare.one, and_true, Int.isSquare_natCast_iff]

Premises used: and_true, Rat.num_natCast, Rat.isSquare_iff, IsSquare.one, Rat.den_natCast, Int.isSquare_natCast_iff
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
z : ℤ
simp_rw : IsSquare (num (↑z : ℚ)) ∧ IsSquare (den (↑z : ℚ)) ↔ IsSquare z
simp_rw₁ : IsSquare z ∧ IsSquare (den (↑z : ℚ)) ↔ IsSquare z
simp_rw₂ : IsSquare z ∧ IsSquare (α := ℕ) 1 ↔ IsSquare z
simp_rw₃ : IsSquare z ∧ True ↔ IsSquare z
⊢ IsSquare (α := ℚ) (↑z : ℚ) ↔ IsSquare z

Tactic:
simp_rw [isSquare_iff, num_intCast, den_intCast, IsSquare.one, and_true]

Premises used: and_true, Rat.den_intCast, Rat.isSquare_iff, IsSquare.one, Rat.num_intCast
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
n : ℕ
⊢ IsSquare (α := ℚ) (OfNat.ofNat n) ↔ IsSquare (α := ℕ) (OfNat.ofNat n)

Tactic:
isSquare_natCast_iff

Premises used: Rat.isSquare_natCast_iff
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
n₁ n₂ : ℤ
d : ℕ
h : d ≠ 0
rw : mkRat (n₁ * (↑d : ℤ) + n₂ * (↑d : ℤ)) (d * d) = mkRat (n₁ + n₂) d
rw₁ : mkRat ((n₁ + n₂) * (↑d : ℤ)) (d * d) = mkRat (n₁ + n₂) d
rw₂ rw₃ : mkRat (n₁ + n₂) d = mkRat (n₁ + n₂) d
⊢ mkRat n₁ d + mkRat n₂ d = mkRat (n₁ + n₂) d

Tactic:
rw [mkRat_add_mkRat _ _ h h, ← add_mul, mkRat_mul_right h]

Premises used: add_mul, Rat.mkRat_mul_right, Rat.mkRat_add_mkRat
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
n d : ℤ
d_ne_zero : d ≠ 0
rw rw₁ : n /. d = n /. d
⊢ HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) = n /. d

Tactic:
rw [← Rat.divInt_eq_div]

Premises used: Rat.divInt_eq_div
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q r : ℚ
s : ℚ := q.num * r.num /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
⊢ HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) ≠ 0

Tactic:
have hs : (q.den * r.den : ℤ) ≠ 0 := Int.natCast_ne_zero_iff_pos.mpr (Nat.mul_pos q.pos r.pos)
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q r : ℚ
s : ℚ := q.num * r.num /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hs : HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) ≠ 0
obtain :
  ∀ (c : ℤ)
    (c_mul_num :
      q.num * r.num =
        c * (HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num)
    (c_mul_den :
      HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) =
        c *
          (↑(HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den : ℤ)),
    (q * r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = q.num * r.num * (↑(q * r).den : ℤ)
⊢ (q * r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = q.num * r.num * (↑(q * r).den : ℤ)

Tactic:
obtain ⟨c, ⟨c_mul_num, c_mul_den⟩⟩ :=
    exists_eq_mul_div_num_and_eq_mul_div_den (q.num * r.num) hs

Premises used: Rat.num, HMul.hMul, Rat.exists_eq_mul_div_num_and_eq_mul_div_den
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q r : ℚ
s : ℚ := q.num * r.num /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hs : HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) ≠ 0
c : ℤ
c_mul_num :
  q.num * r.num =
    c * (HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num
c_mul_den :
  HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) =
    c * (↑(HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den : ℤ)
rw :
  HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) * (q * r).num =
    c * (HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num *
      (↑(q * r).den : ℤ)
⊢ (q * r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = q.num * r.num * (↑(q * r).den : ℤ)

Tactic:
rw [c_mul_num, mul_assoc, mul_comm]

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q r : ℚ
s : ℚ := q.num * r.num /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hs : HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) ≠ 0
c : ℤ
c_mul_num :
  q.num * r.num =
    c * (HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num
c_mul_den :
  HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) =
    c * (↑(HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den : ℤ)
nth_rw :
  c * (↑(HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den : ℤ) *
      (q * r).num =
    c * (HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num *
      (↑(q * r).den : ℤ)
⊢ HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) * (q * r).num =
    c * (HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num *
      (↑(q * r).den : ℤ)

Tactic:
nth_rw 1 [c_mul_den]
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q r : ℚ
s : ℚ := q.num * r.num /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hs : HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) ≠ 0
c : ℤ
c_mul_num :
  q.num * r.num =
    c * (HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num
c_mul_den :
  HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) =
    c * (↑(HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den : ℤ)
rw :
  ¬c = 0 →
    (↑(HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den : ℤ) *
        (q * r).num =
      (HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num *
        (↑(q * r).den : ℤ)
⊢ c * (↑(HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den : ℤ) *
      (q * r).num =
    c * (HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num *
      (↑(q * r).den : ℤ)

Tactic:
rw [Int.mul_assoc, Int.mul_assoc, mul_eq_mul_left_iff, or_iff_not_imp_right]

Premises used: Classical.or_iff_not_imp_right, Int.mul_assoc, mul_eq_mul_left_iff
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q r : ℚ
s : ℚ := q.num * r.num /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hs : HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) ≠ 0
c : ℤ
c_mul_num :
  q.num * r.num =
    c * (HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num
c_mul_den :
  HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) =
    c * (↑(HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den : ℤ)
h : ¬c = 0
⊢ q.num /. (↑q.den : ℤ) * (r.num /. (↑r.den : ℤ)) = s

Tactic:
have h : _ = s := divInt_mul_divInt q.num r.num