awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
a b : ℤ
b0 : b ≠ 0
⊢ (a /. b).num ∣ a
have rcases : ∀ (n : ℤ) (d : ℕ) (h : d ≠ 0) (c : n.natAbs.Coprime d) (e : a /. b = { num := n, den := d, den_nz := h, reduced := c }),
  { num := n, den := d, den_nz := h, reduced := c : ℚ }.num ∣ a
Tactic: rcases e : a /. b with ⟨n, d, h, c⟩
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (hypothesis)
Goal:
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
⊢ { num := n, den := d, den_nz := h, reduced := c : ℚ }.num ∣ a
have e₁ : a * (↑d : ℤ) = n * b
Tactic: rw [Rat.mk_eq_divInt, divInt_eq_divInt_iff b0 (mod_cast h)] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * (↑d : ℤ) = n * b
⊢ { num := n, den := d, den_nz := h, reduced := c : ℚ }.num ∣ a
have refine : n.natAbs ∣ a.natAbs * d
Tactic: refine Int.natAbs_dvd.1 <| Int.dvd_natAbs.1 <| Int.natCast_dvd_natCast.2 <|
    c.dvd_of_dvd_mul_right ?_
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (hypothesis)
Goal:
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * (↑d : ℤ) = n * b
⊢ n.natAbs ∣ a.natAbs * d
have this : (a * (↑d : ℤ)).natAbs = (n * b).natAbs
Tactic: have := congr_arg Int.natAbs e
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (hypothesis)
Goal:
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * (↑d : ℤ) = n * b
this : (a * (↑d : ℤ)).natAbs = (n * b).natAbs
⊢ n.natAbs ∣ a.natAbs * d
have this₁ : a.natAbs * d = n.natAbs * b.natAbs
Tactic: simp only [Int.natAbs_mul, Int.natAbs_natCast] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
a b : ℤ
⊢ (↑(a /. b).den : ℤ) ∣ b
have pos : ∀ (b0 : b = 0), (↑(a /. b).den : ℤ) ∣ b
Tactic: by_cases b0 : b = 0
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
a b : ℤ
pos : ∀ (b0 : b = 0), (↑(a /. b).den : ℤ) ∣ b
⊢ (↑(a /. b).den : ℤ) ∣ b
have neg : ∀ (b0 : ¬b = 0), (↑(a /. b).den : ℤ) ∣ b
Tactic: by_cases b0 : b = 0
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
a b : ℤ
b0 : ¬b = 0
⊢ (↑(a /. b).den : ℤ) ∣ b
have neg : ∀ (n : ℤ) (d : ℕ) (h : d ≠ 0) (c : n.natAbs.Coprime d) (e : a /. b = { num := n, den := d, den_nz := h, reduced := c }),
  (↑{ num := n, den := d, den_nz := h, reduced := c }.den : ℤ) ∣ b
Tactic: rcases e : a /. b with ⟨n, d, h, c⟩
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (hypothesis)
Goal:
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
⊢ (↑{ num := n, den := d, den_nz := h, reduced := c }.den : ℤ) ∣ b
have e₁ : a * (↑d : ℤ) = n * b
Tactic: rw [mk_eq_divInt,
    divInt_eq_divInt_iff b0 (ne_of_gt (Int.natCast_pos.2 (Nat.pos_of_ne_zero h)))] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * (↑d : ℤ) = n * b
⊢ (↑{ num := n, den := d, den_nz := h, reduced := c }.den : ℤ) ∣ b
have neg : d ∣ n.natAbs * b.natAbs
Tactic: refine Int.dvd_natAbs.1 <| Int.natCast_dvd_natCast.2 <| c.symm.dvd_of_dvd_mul_left ?_
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * (↑d : ℤ) = n * b
⊢ d ∣ n.natAbs * b.natAbs
have neg : (↑d : ℤ) ∣ a * (↑d : ℤ)
Tactic: rw [← Int.natAbs_mul, ← Int.natCast_dvd_natCast, Int.dvd_natAbs, ← e]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
⊢ ∃ (c : ℤ), n = c * q.num ∧ d = c * (↑q.den : ℤ)
have inl : ∀ (qdf : q = 0 /. d), ∃ (c : ℤ), 0 = c * q.num ∧ d = c * (↑q.den : ℤ)
Tactic: obtain rfl | hn := eq_or_ne n 0
Cleared hypotheses: n, qdf
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
inl : ∀ (qdf : q = 0 /. d), ∃ (c : ℤ), 0 = c * q.num ∧ d = c * (↑q.den : ℤ)
⊢ ∃ (c : ℤ), n = c * q.num ∧ d = c * (↑q.den : ℤ)
have inr : ∀ (hn : n ≠ 0), ∃ (c : ℤ), n = c * q.num ∧ d = c * (↑q.den : ℤ)
Tactic: obtain rfl | hn := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
⊢ q.num * d = n * (↑q.den : ℤ)
have refine_1 : Ne (α := ℤ) (↑q.den : ℤ) 0
Tactic: refine (divInt_eq_divInt_iff ?_ hd).mp ?_
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
refine_1 : Ne (α := ℤ) (↑q.den : ℤ) 0
⊢ q.num * d = n * (↑q.den : ℤ)
have refine_2 : q.num /. (↑q.den : ℤ) = n /. d
Tactic: refine (divInt_eq_divInt_iff ?_ hd).mp ?_
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (hypothesis)
Goal:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
⊢ ∃ (c : ℤ), n = c * q.num ∧ d = c * (↑q.den : ℤ)
have this : q.num * d = n * (↑q.den : ℤ)
Tactic: have : q.num * d = n * ↑q.den := by
    refine (divInt_eq_divInt_iff ?_ hd).mp ?_
    · exact Int.natCast_ne_zero.mpr (Rat.den_nz _)
    · rwa [num_divInt_den]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * (↑q.den : ℤ)
⊢ q.num ∣ n
have rw : (n /. d).num ∣ n
Tactic: rw [qdf]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (hypothesis)
Goal:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * (↑q.den : ℤ)
⊢ ∃ (c : ℤ), n = c * q.num ∧ d = c * (↑q.den : ℤ)
have hqdn : q.num ∣ n
Tactic: have hqdn : q.num ∣ n := by
    rw [qdf]
    exact Rat.num_dvd _ hd
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * (↑q.den : ℤ)
hqdn : q.num ∣ n
⊢ ∃ (c : ℤ), n = c * q.num ∧ d = c * (↑q.den : ℤ)
have inr : n = n / q.num * q.num
Tactic: refine ⟨n / q.num, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * (↑q.den : ℤ)
hqdn : q.num ∣ n
inr : n = n / q.num * q.num
⊢ ∃ (c : ℤ), n = c * q.num ∧ d = c * (↑q.den : ℤ)
have inr₁ : d = n / q.num * (↑q.den : ℤ)
Tactic: refine ⟨n / q.num, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * (↑q.den : ℤ)
hqdn : q.num ∣ n
⊢ n = n / q.num * q.num
have inr : n = n
Tactic: rw [Int.ediv_mul_cancel hqdn]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * (↑q.den : ℤ)
hqdn : q.num ∣ n
⊢ d = n / q.num * (↑q.den : ℤ)
have inr : q.num ≠ 0
Tactic: refine Int.eq_mul_div_of_mul_eq_mul_of_dvd_left ?_ hqdn this
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * (↑q.den : ℤ)
hqdn : q.num ∣ n
⊢ q.num ≠ 0
have inr : (n /. d).num ≠ 0
Tactic: rw [qdf]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ
⊢ (q₁ + q₂).den ∣ q₁.den.lcm q₂.den
have rw : q₁.den.gcd q₂.den ∣ (q₁.num * (↑q₂.den : ℤ) + q₂.num * (↑q₁.den : ℤ)).natAbs ∧
  q₁.den.gcd q₂.den ∣ q₁.den.gcd q₂.den * q₁.den.lcm q₂.den
Tactic: rw [add_def, normalize_eq, Nat.div_dvd_iff_dvd_mul (Nat.gcd_dvd_right _ _)
    (Nat.gcd_pos_of_pos_right _ (by simp [Nat.pos_iff_ne_zero])), ← Nat.gcd_mul_lcm,
    mul_dvd_mul_iff_right (Nat.lcm_ne_zero (by simp) (by simp)), Nat.dvd_gcd_iff]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ
⊢ q₁.den.gcd q₂.den ∣ (q₁.num * (↑q₂.den : ℤ) + q₂.num * (↑q₁.den : ℤ)).natAbs ∧
    q₁.den.gcd q₂.den ∣ q₁.den.gcd q₂.den * q₁.den.lcm q₂.den
have refine : q₁.den.gcd q₂.den ∣ (q₁.num * (↑q₂.den : ℤ) + q₂.num * (↑q₁.den : ℤ)).natAbs
Tactic: refine ⟨?_, dvd_mul_right _ _⟩
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ
⊢ q₁.den.gcd q₂.den ∣ (q₁.num * (↑q₂.den : ℤ) + q₂.num * (↑q₁.den : ℤ)).natAbs
have rw : (↑(q₁.den.gcd q₂.den) : ℤ) ∣ q₁.num * (↑q₂.den : ℤ) + q₂.num * (↑q₁.den : ℤ)
Tactic: rw [← Int.natCast_dvd_natCast, Int.dvd_natAbs]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ
⊢ (↑(q₁.den.gcd q₂.den) : ℤ) ∣ q₁.num * (↑q₂.den : ℤ) + q₂.num * (↑q₁.den : ℤ)
have a : (↑(q₁.den.gcd q₂.den) : ℤ) ∣ q₁.num * (↑q₂.den : ℤ)
Tactic: apply Int.dvd_add
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ
a : (↑(q₁.den.gcd q₂.den) : ℤ) ∣ q₁.num * (↑q₂.den : ℤ)
⊢ (↑(q₁.den.gcd q₂.den) : ℤ) ∣ q₁.num * (↑q₂.den : ℤ) + q₂.num * (↑q₁.den : ℤ)
have a₁ : (↑(q₁.den.gcd q₂.den) : ℤ) ∣ q₂.num * (↑q₁.den : ℤ)
Tactic: apply Int.dvd_add
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ
⊢ (↑(q₁.den.gcd q₂.den) : ℤ) ∣ q₁.num * (↑q₂.den : ℤ)
have a : Dvd.dvd (α := ℤ) (↑(q₁.den.gcd q₂.den) : ℤ) (↑q₂.den : ℤ)
Tactic: apply dvd_mul_of_dvd_right
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ
⊢ (↑(q₁.den.gcd q₂.den) : ℤ) ∣ q₂.num * (↑q₁.den : ℤ)
have a : Dvd.dvd (α := ℤ) (↑(q₁.den.gcd q₂.den) : ℤ) (↑q₁.den : ℤ)
Tactic: apply dvd_mul_of_dvd_right
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ
⊢ Dvd.dvd (α := ℤ) (↑(q₁.den.gcd q₂.den) : ℤ) (↑q₂.den : ℤ)
have a : q₁.den.gcd q₂.den ∣ q₂.den
Tactic: rw [Int.natCast_dvd_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ
⊢ Dvd.dvd (α := ℤ) (↑(q₁.den.gcd q₂.den) : ℤ) (↑q₁.den : ℤ)
have a : q₁.den.gcd q₂.den ∣ q₁.den
Tactic: rw [Int.natCast_dvd_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ
⊢ (↑(q₁.den.gcd q₂.den) : ℤ) ∣ q₁.num * (↑q₂.den : ℤ) + q₂.num * (↑q₁.den : ℤ)
have a : (↑(q₁.den.gcd 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 _ _]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ
a : (↑(q₁.den.gcd q₂.den) : ℤ) ∣ q₁.num * (↑q₂.den : ℤ)
⊢ (↑(q₁.den.gcd q₂.den) : ℤ) ∣ q₁.num * (↑q₂.den : ℤ) + q₂.num * (↑q₁.den : ℤ)
have a₁ : (↑(q₁.den.gcd 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 _ _]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
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 : ℤ)
⊢ (↑(q₁.den.gcd q₂.den) : ℤ) ∣ q₁.num * (↑q₂.den : ℤ) + q₂.num * (↑q₁.den : ℤ)
have a₈ : Dvd.dvd (α := ℤ) (↑(q₁.den.gcd q₂.den) : ℤ) (↑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 _ _]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
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 : ℤ)
⊢ (↑(q₁.den.gcd q₂.den) : ℤ) ∣ q₁.num * (↑q₂.den : ℤ) + q₂.num * (↑q₁.den : ℤ)
have a₉ : Dvd.dvd (α := ℤ) (↑(q₁.den.gcd q₂.den) : ℤ) (↑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 _ _]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
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 : ℤ)
⊢ (↑(q₁.den.gcd q₂.den) : ℤ) ∣ q₁.num * (↑q₂.den : ℤ) + q₂.num * (↑q₁.den : ℤ)
have a₁₆ : q₁.den.gcd q₂.den ∣ 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 _ _]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
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
⊢ (↑(q₁.den.gcd q₂.den) : ℤ) ∣ q₁.num * (↑q₂.den : ℤ) + q₂.num * (↑q₁.den : ℤ)
have a₁₇ : q₁.den.gcd q₂.den ∣ 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 _ _]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ
⊢ (q₁ * q₂).den ∣ q₁.den * q₂.den
have 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 := sorry, reduced := sorry : ℚ }.den ∣
  q₁.den * q₂.den
Tactic: rw [mul_def, normalize_eq]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ
⊢ { 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
have h : (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den) ∣ q₁.den * q₂.den
Tactic: apply Nat.div_dvd_of_dvd
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ
⊢ (q₁ * q₂).num = q₁.num * q₂.num / (↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) : ℤ)
have rw : (normalize (q₁.num * q₂.num) (q₁.den * q₂.den) sorry).num =
  q₁.num * q₂.num / (↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) : ℤ)
Tactic: rw [mul_def, normalize_eq]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
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)) : ℤ)
⊢ (q₁ * q₂).num = q₁.num * q₂.num / (↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) : ℤ)
have 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 := sorry, reduced := sorry : ℚ }.num =
  q₁.num * q₂.num / (↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) : ℤ)
Tactic: rw [mul_def, normalize_eq]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ
⊢ (q₁ * q₂).den = q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)
have rw : (normalize (q₁.num * q₂.num) (q₁.den * q₂.den) sorry).den = q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)
Tactic: rw [mul_def, normalize_eq]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
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)
⊢ (q₁ * q₂).den = q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)
have 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 := sorry, reduced := sorry : ℚ }.den =
  q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)
Tactic: rw [mul_def, normalize_eq]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q : ℚ
n : ℤ
⊢ (q + (↑n : ℚ)).den = q.den
have a : (q + (↑n : ℚ)).den ∣ q.den
Tactic: apply Nat.dvd_antisymm
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q : ℚ
n : ℤ
a : (q + (↑n : ℚ)).den ∣ q.den
⊢ (q + (↑n : ℚ)).den = q.den
have a₁ : q.den ∣ (q + (↑n : ℚ)).den
Tactic: apply Nat.dvd_antisymm
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
n : ℤ
q : ℚ
⊢ ((↑n : ℚ) + q).den = q.den
have rw : (q + (↑n : ℚ)).den = q.den
Tactic: rw [add_comm, add_intCast_den]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
n : ℤ
q : ℚ
rw : (q + (↑n : ℚ)).den = q.den
⊢ ((↑n : ℚ) + q).den = q.den
have rw₁ : q.den = q.den
Tactic: rw [add_comm, add_intCast_den]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q : ℚ
n : ℤ
⊢ (q - (↑n : ℚ)).den = q.den
have rw : (q + -(↑n : ℚ)).den = q.den
Tactic: rw [sub_eq_add_neg, ← Int.cast_neg, add_intCast_den]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q : ℚ
n : ℤ
rw : (q + -(↑n : ℚ)).den = q.den
⊢ (q - (↑n : ℚ)).den = q.den
have rw₁ : (q + (↑(-n) : ℚ)).den = q.den
Tactic: rw [sub_eq_add_neg, ← Int.cast_neg, add_intCast_den]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q : ℚ
n : ℤ
rw : (q + -(↑n : ℚ)).den = q.den
rw₁ : (q + (↑(-n) : ℚ)).den = q.den
⊢ (q - (↑n : ℚ)).den = q.den
have rw₂ : q.den = q.den
Tactic: rw [sub_eq_add_neg, ← Int.cast_neg, add_intCast_den]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
n : ℤ
q : ℚ
⊢ ((↑n : ℚ) - q).den = q.den
have rw : ((↑n : ℚ) + -q).den = q.den
Tactic: rw [sub_eq_add_neg, intCast_add_den, neg_den]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
n : ℤ
q : ℚ
rw : ((↑n : ℚ) + -q).den = q.den
⊢ ((↑n : ℚ) - q).den = q.den
have rw₁ : (-q).den = q.den
Tactic: rw [sub_eq_add_neg, intCast_add_den, neg_den]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
n : ℤ
q : ℚ
rw : ((↑n : ℚ) + -q).den = q.den
rw₁ : (-q).den = q.den
⊢ ((↑n : ℚ) - q).den = q.den
have rw₂ : q.den = q.den
Tactic: rw [sub_eq_add_neg, intCast_add_den, neg_den]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ
⊢ q₁.den * q₂.den = (q₁ * q₂).den * (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)
have 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)
Tactic: rw [mul_den]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ
⊢ q₁.num * q₂.num = (q₁ * q₂).num * (↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) : ℤ)
have 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)) : ℤ)
Tactic: rw [mul_num]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
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)) : ℤ)
have refine : (↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) : ℤ) ∣ q₁.num * q₂.num
Tactic: refine (Int.ediv_mul_cancel ?_).symm
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ
⊢ (↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) : ℤ) ∣ q₁.num * q₂.num
have rw : Dvd.dvd (α := ℤ) (↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) : ℤ) (↑(q₁.num * q₂.num).natAbs : ℤ)
Tactic: rw [← Int.dvd_natAbs]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q : ℚ
⊢ (q * q).num = q.num * q.num
have rw : (q.num.natAbs * q.num.natAbs).Coprime (q.den * q.den)
Tactic: rw [mul_num, Int.natAbs_mul, Nat.Coprime.gcd_eq_one, Int.ofNat_one, Int.ediv_one]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q : ℚ
⊢ (q * q).den = q.den * q.den
have rw : (q.num.natAbs * q.num.natAbs).Coprime (q.den * q.den)
Tactic: rw [Rat.mul_den, Int.natAbs_mul, Nat.Coprime.gcd_eq_one, Nat.div_one]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (hypothesis)
Goal:
q r : ℚ
⊢ q + r = (q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
have hqd : Ne (α := ℤ) (↑q.den : ℤ) 0
Tactic: have hqd : (q.den : ℤ) ≠ 0 := Int.natCast_ne_zero_iff_pos.2 q.den_pos
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (hypothesis)
Goal:
q r : ℚ
hqd : Ne (α := ℤ) (↑q.den : ℤ) 0
⊢ q + r = (q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
have hrd : Ne (α := ℤ) (↑r.den : ℤ) 0
Tactic: have hrd : (r.den : ℤ) ≠ 0 := Int.natCast_ne_zero_iff_pos.2 r.den_pos
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q r : ℚ
hqd : Ne (α := ℤ) (↑q.den : ℤ) 0
hrd : Ne (α := ℤ) (↑r.den : ℤ) 0
| q + r
have rw : (q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
Tactic: rw [← num_divInt_den q, ← num_divInt_den r, divInt_add_divInt _ _ hqd hrd]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q r : ℚ
hqd : Ne (α := ℤ) (↑q.den : ℤ) 0
hrd : Ne (α := ℤ) (↑r.den : ℤ) 0
⊢ q + r = (q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
have 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 : ℤ)
Tactic: conv_lhs => rw [← num_divInt_den q, ← num_divInt_den r, divInt_add_divInt _ _ hqd hrd]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q r : ℚ
hqd : Ne (α := ℤ) (↑q.den : ℤ) 0
hrd : Ne (α := ℤ) (↑r.den : ℤ) 0
⊢ (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 : ℤ)
have 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 : ℤ)
Tactic: rw [mul_comm r.num q.den]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q : ℚ
⊢ IsSquare q ↔ IsSquare q.num ∧ IsSquare q.den
have mp : IsSquare q → IsSquare q.num ∧ IsSquare q.den
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q : ℚ
mp : IsSquare q → IsSquare q.num ∧ IsSquare q.den
⊢ IsSquare q ↔ IsSquare q.num ∧ IsSquare q.den
have mpr : IsSquare q.num ∧ IsSquare q.den → IsSquare q
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
qr : ℚ
⊢ IsSquare (qr * qr).num ∧ IsSquare (qr * qr).den
have mp : IsSquare (qr.num * qr.num) ∧ IsSquare (qr.den * qr.den)
Tactic: rw [Rat.mul_self_num, mul_self_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
⊢ IsSquare q
have mpr : q = HDiv.hDiv (α := ℚ) (↑nr : ℚ) (↑dr : ℚ) * HDiv.hDiv (α := ℚ) (↑nr : ℚ) (↑dr : ℚ)
Tactic: refine ⟨nr / dr, ?_⟩