awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q : ℚ
nr : ℤ
hnr : q.num = nr * nr
dr : ℕ
hdr : q.den = dr * dr
⊢ q = HDiv.hDiv (α := ℚ) (↑nr : ℚ) (↑dr : ℚ) * HDiv.hDiv (α := ℚ) (↑nr : ℚ) (↑dr : ℚ)
have mpr : q = HMul.hMul (α := ℚ) (↑nr : ℚ) (↑nr : ℚ) / HMul.hMul (α := ℚ) (↑dr : ℚ) (↑dr : ℚ)
Tactic: rw [div_mul_div_comm, ← Int.cast_mul, ← Nat.cast_mul, ← hnr, ← hdr, num_div_den]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q : ℚ
nr : ℤ
hnr : q.num = nr * nr
dr : ℕ
hdr : q.den = dr * dr
mpr : q = HMul.hMul (α := ℚ) (↑nr : ℚ) (↑nr : ℚ) / HMul.hMul (α := ℚ) (↑dr : ℚ) (↑dr : ℚ)
⊢ q = HDiv.hDiv (α := ℚ) (↑nr : ℚ) (↑dr : ℚ) * HDiv.hDiv (α := ℚ) (↑nr : ℚ) (↑dr : ℚ)
have mpr₁ : q = (↑(nr * nr) : ℚ) / HMul.hMul (α := ℚ) (↑dr : ℚ) (↑dr : ℚ)
Tactic: rw [div_mul_div_comm, ← Int.cast_mul, ← Nat.cast_mul, ← hnr, ← hdr, num_div_den]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
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 : ℚ)
⊢ q = HDiv.hDiv (α := ℚ) (↑nr : ℚ) (↑dr : ℚ) * HDiv.hDiv (α := ℚ) (↑nr : ℚ) (↑dr : ℚ)
have mpr₂ : q = HDiv.hDiv (α := ℚ) (↑(nr * nr) : ℚ) (↑(dr * dr) : ℚ)
Tactic: rw [div_mul_div_comm, ← Int.cast_mul, ← Nat.cast_mul, ← hnr, ← hdr, num_div_den]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
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) : ℚ)
⊢ q = HDiv.hDiv (α := ℚ) (↑nr : ℚ) (↑dr : ℚ) * HDiv.hDiv (α := ℚ) (↑nr : ℚ) (↑dr : ℚ)
have mpr₃ : q = HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑(dr * dr) : ℚ)
Tactic: rw [div_mul_div_comm, ← Int.cast_mul, ← Nat.cast_mul, ← hnr, ← hdr, num_div_den]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
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) : ℚ)
⊢ q = HDiv.hDiv (α := ℚ) (↑nr : ℚ) (↑dr : ℚ) * HDiv.hDiv (α := ℚ) (↑nr : ℚ) (↑dr : ℚ)
have mpr₄ : q = HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)
Tactic: rw [div_mul_div_comm, ← Int.cast_mul, ← Nat.cast_mul, ← hnr, ← hdr, num_div_den]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
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 : ℚ)
⊢ q = HDiv.hDiv (α := ℚ) (↑nr : ℚ) (↑dr : ℚ) * HDiv.hDiv (α := ℚ) (↑nr : ℚ) (↑dr : ℚ)
have mpr₅ : q = q
Tactic: rw [div_mul_div_comm, ← Int.cast_mul, ← Nat.cast_mul, ← hnr, ← hdr, num_div_den]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
n : ℕ
⊢ IsSquare (α := ℚ) (↑n : ℚ) ↔ IsSquare n
have simp_rw : IsSquare (num (↑n : ℚ)) ∧ IsSquare (den (↑n : ℚ)) ↔ IsSquare n
Tactic: simp_rw [isSquare_iff, num_natCast, den_natCast, IsSquare.one, and_true, Int.isSquare_natCast_iff]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
n : ℕ
simp_rw : IsSquare (num (↑n : ℚ)) ∧ IsSquare (den (↑n : ℚ)) ↔ IsSquare n
⊢ IsSquare (α := ℚ) (↑n : ℚ) ↔ IsSquare n
have simp_rw₁ : IsSquare (α := ℤ) (↑n : ℤ) ∧ IsSquare (den (↑n : ℚ)) ↔ IsSquare n
Tactic: simp_rw [isSquare_iff, num_natCast, den_natCast, IsSquare.one, and_true, Int.isSquare_natCast_iff]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
n : ℕ
simp_rw : IsSquare (num (↑n : ℚ)) ∧ IsSquare (den (↑n : ℚ)) ↔ IsSquare n
simp_rw₁ : IsSquare (α := ℤ) (↑n : ℤ) ∧ IsSquare (den (↑n : ℚ)) ↔ IsSquare n
⊢ IsSquare (α := ℚ) (↑n : ℚ) ↔ IsSquare n
have simp_rw₂ : IsSquare (α := ℤ) (↑n : ℤ) ∧ IsSquare (α := ℕ) 1 ↔ IsSquare n
Tactic: simp_rw [isSquare_iff, num_natCast, den_natCast, IsSquare.one, and_true, Int.isSquare_natCast_iff]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
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
⊢ IsSquare (α := ℚ) (↑n : ℚ) ↔ IsSquare n
have simp_rw₃ : IsSquare (α := ℤ) (↑n : ℤ) ∧ True ↔ IsSquare n
Tactic: simp_rw [isSquare_iff, num_natCast, den_natCast, IsSquare.one, and_true, Int.isSquare_natCast_iff]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
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
⊢ IsSquare (α := ℚ) (↑n : ℚ) ↔ IsSquare n
have simp_rw₄ : IsSquare (α := ℤ) (↑n : ℤ) ↔ IsSquare n
Tactic: simp_rw [isSquare_iff, num_natCast, den_natCast, IsSquare.one, and_true, Int.isSquare_natCast_iff]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
z : ℤ
⊢ IsSquare (α := ℚ) (↑z : ℚ) ↔ IsSquare z
have simp_rw : IsSquare (num (↑z : ℚ)) ∧ IsSquare (den (↑z : ℚ)) ↔ IsSquare z
Tactic: simp_rw [isSquare_iff, num_intCast, den_intCast, IsSquare.one, and_true]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
z : ℤ
simp_rw : IsSquare (num (↑z : ℚ)) ∧ IsSquare (den (↑z : ℚ)) ↔ IsSquare z
⊢ IsSquare (α := ℚ) (↑z : ℚ) ↔ IsSquare z
have simp_rw₁ : IsSquare z ∧ IsSquare (den (↑z : ℚ)) ↔ IsSquare z
Tactic: simp_rw [isSquare_iff, num_intCast, den_intCast, IsSquare.one, and_true]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
z : ℤ
simp_rw : IsSquare (num (↑z : ℚ)) ∧ IsSquare (den (↑z : ℚ)) ↔ IsSquare z
simp_rw₁ : IsSquare z ∧ IsSquare (den (↑z : ℚ)) ↔ IsSquare z
⊢ IsSquare (α := ℚ) (↑z : ℚ) ↔ IsSquare z
have simp_rw₂ : IsSquare z ∧ IsSquare (α := ℕ) 1 ↔ IsSquare z
Tactic: simp_rw [isSquare_iff, num_intCast, den_intCast, IsSquare.one, and_true]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
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
⊢ IsSquare (α := ℚ) (↑z : ℚ) ↔ IsSquare z
have simp_rw₃ : IsSquare z ∧ True ↔ IsSquare z
Tactic: simp_rw [isSquare_iff, num_intCast, den_intCast, IsSquare.one, and_true]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
n₁ n₂ : ℤ
d : ℕ
h : d ≠ 0
⊢ mkRat n₁ d + mkRat n₂ d = mkRat (n₁ + n₂) d
have rw : mkRat (n₁ * (↑d : ℤ) + n₂ * (↑d : ℤ)) (d * d) = mkRat (n₁ + n₂) d
Tactic: rw [mkRat_add_mkRat _ _ h h, ← add_mul, mkRat_mul_right h]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
n₁ n₂ : ℤ
d : ℕ
h : d ≠ 0
rw : mkRat (n₁ * (↑d : ℤ) + n₂ * (↑d : ℤ)) (d * d) = mkRat (n₁ + n₂) d
⊢ mkRat n₁ d + mkRat n₂ d = mkRat (n₁ + n₂) d
have rw₁ : mkRat ((n₁ + n₂) * (↑d : ℤ)) (d * d) = mkRat (n₁ + n₂) d
Tactic: rw [mkRat_add_mkRat _ _ h h, ← add_mul, mkRat_mul_right h]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
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
⊢ mkRat n₁ d + mkRat n₂ d = mkRat (n₁ + n₂) d
have rw₂ : mkRat (n₁ + n₂) d = mkRat (n₁ + n₂) d
Tactic: rw [mkRat_add_mkRat _ _ h h, ← add_mul, mkRat_mul_right h]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
n d : ℤ
d_ne_zero : d ≠ 0
⊢ HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) = n /. d
have rw : n /. d = n /. d
Tactic: rw [← Rat.divInt_eq_div]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (hypothesis)
Goal:
q r : ℚ
s : ℚ := q.num * r.num /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
⊢ (q * r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = q.num * r.num * (↑(q * r).den : ℤ)
have hs : 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)
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q r : ℚ
s : ℚ := q.num * r.num /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hs : HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) ≠ 0
⊢ (q * r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = q.num * r.num * (↑(q * r).den : ℤ)
have 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 : ℤ)
Tactic: obtain ⟨c, ⟨c_mul_num, c_mul_den⟩⟩ :=
    exists_eq_mul_div_num_and_eq_mul_div_den (q.num * r.num) hs
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
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 : ℤ)
⊢ (q * r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = q.num * r.num * (↑(q * r).den : ℤ)
have 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 : ℤ)
Tactic: rw [c_mul_num, mul_assoc, mul_comm]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
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 : ℤ)
⊢ 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 : ℤ)
have 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 : ℤ)
Tactic: nth_rw 1 [c_mul_den]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
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 : ℤ)
⊢ 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 : ℤ)
have 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 : ℤ)
Tactic: rw [Int.mul_assoc, Int.mul_assoc, mul_eq_mul_left_iff, or_iff_not_imp_right]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (hypothesis)
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
⊢ (↑(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 : ℤ)
have h : q.num /. (↑q.den : ℤ) * (r.num /. (↑r.den : ℤ)) = s
Tactic: have h : _ = s := divInt_mul_divInt q.num r.num
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (hypothesis)
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_1 : ¬c = 0
h : q.num /. (↑q.den : ℤ) * (r.num /. (↑r.den : ℤ)) = s
⊢ (↑(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 : ℤ)
have h₁ : q * r = s
Tactic: rw [num_divInt_den, num_divInt_den] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
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_1 : ¬c = 0
h : q * r = s
⊢ (↑(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 : ℤ)
have rw : (↑(HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den : ℤ) * s.num =
  (HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num * (↑s.den : ℤ)
Tactic: rw [h, mul_comm, ← Rat.eq_iff_mul_eq_mul, ← divInt_eq_div]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
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_1 : ¬c = 0
h : q * r = s
rw :
  (↑(HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den : ℤ) * s.num =
    (HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num * (↑s.den : ℤ)
⊢ (↑(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 : ℤ)
have rw₁ : s.num * (↑(HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den : ℤ) =
  (HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num * (↑s.den : ℤ)
Tactic: rw [h, mul_comm, ← Rat.eq_iff_mul_eq_mul, ← divInt_eq_div]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
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_1 : ¬c = 0
h : q * r = s
rw :
  (↑(HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den : ℤ) * s.num =
    (HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num * (↑s.den : ℤ)
rw₁ :
  s.num * (↑(HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den : ℤ) =
    (HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num * (↑s.den : ℤ)
⊢ (↑(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 : ℤ)
have rw₂ : s = HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)
Tactic: rw [h, mul_comm, ← Rat.eq_iff_mul_eq_mul, ← divInt_eq_div]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
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_1 : ¬c = 0
h : q * r = s
rw :
  (↑(HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den : ℤ) * s.num =
    (HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num * (↑s.den : ℤ)
rw₁ :
  s.num * (↑(HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den : ℤ) =
    (HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num * (↑s.den : ℤ)
rw₂ : s = HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)
⊢ (↑(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 : ℤ)
have rw₃ : s = q.num * r.num /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
Tactic: rw [h, mul_comm, ← Rat.eq_iff_mul_eq_mul, ← divInt_eq_div]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (hypothesis)
Goal:
q r : ℚ
s : ℚ := (q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
⊢ (q + r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = (q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) * (↑(q + r).den : ℤ)
have hs : 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)
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q r : ℚ
s : ℚ := (q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hs : HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) ≠ 0
⊢ (q + r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = (q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) * (↑(q + r).den : ℤ)
have obtain : ∀ (c : ℤ)
  (c_mul_num :
    q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ) =
      c *
        (HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
            (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num)
  (c_mul_den :
    HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) =
      c *
        (↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
                (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
          ℤ)),
  (q + r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = (q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) * (↑(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.den + r.num * q.den) hs
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q r : ℚ
s : ℚ := (q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hs : HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) ≠ 0
c : ℤ
c_mul_num :
  q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ) =
    c *
      (HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
          (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num
c_mul_den :
  HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) =
    c *
      (↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
              (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
        ℤ)
⊢ (q + r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = (q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) * (↑(q + r).den : ℤ)
have rw : HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) * (q + r).num =
  c *
      (HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
          (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num *
    (↑(q + r).den : ℤ)
Tactic: rw [c_mul_num, mul_assoc, mul_comm]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q r : ℚ
s : ℚ := (q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hs : HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) ≠ 0
c : ℤ
c_mul_num :
  q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ) =
    c *
      (HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
          (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num
c_mul_den :
  HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) =
    c *
      (↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
              (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
        ℤ)
⊢ HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) * (q + r).num =
    c *
        (HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
            (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num *
      (↑(q + r).den : ℤ)
have nth_rw : c *
      (↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
              (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
        ℤ) *
    (q + r).num =
  c *
      (HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
          (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num *
    (↑(q + r).den : ℤ)
Tactic: nth_rw 1 [c_mul_den]