awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
q r : ℚ≥0
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
hr : Ne.{u_3 + 1} (α := α) (↑r.den : α) 0
⊢ (↑(q * r) : α) = HMul.hMul (α := α) (↑q : α) (↑r : α)
have rw : HDiv.hDiv (α := α) (↑(q.num * r.num) : α) (↑(q.den * r.den) : α) =
  HMul.hMul (α := α) (↑q.num : α) (↑r.num : α) / HMul.hMul (α := α) (↑q.den : α) (↑r.den : α)
Tactic: rw [mul_def, cast_divNat_of_ne_zero, cast_def, cast_def,
    (Nat.commute_cast _ _).div_mul_div_comm (Nat.commute_cast _ _)]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
q r : ℚ≥0
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
hr : Ne.{u_3 + 1} (α := α) (↑r.den : α) 0
rw :
  HDiv.hDiv (α := α) (↑(q.num * r.num) : α) (↑(q.den * r.den) : α) =
    HMul.hMul (α := α) (↑q.num : α) (↑r.num : α) / HMul.hMul (α := α) (↑q.den : α) (↑r.den : α)
⊢ (↑(q * r) : α) = HMul.hMul (α := α) (↑q : α) (↑r : α)
have hb : Ne.{u_3 + 1} (α := α) (↑(q.den * r.den) : α) 0
Tactic: rw [mul_def, cast_divNat_of_ne_zero, cast_def, cast_def,
    (Nat.commute_cast _ _).div_mul_div_comm (Nat.commute_cast _ _)]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
q r : ℚ≥0
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
hr : Ne.{u_3 + 1} (α := α) (↑r.den : α) 0
⊢ HDiv.hDiv (α := α) (↑(q.num * r.num) : α) (↑(q.den * r.den) : α) =
    HMul.hMul (α := α) (↑q.num : α) (↑r.num : α) / HMul.hMul (α := α) (↑q.den : α) (↑r.den : α)
have push_cast : HMul.hMul (α := α) (↑q.num : α) (↑r.num : α) / HMul.hMul (α := α) (↑q.den : α) (↑r.den : α) =
  HMul.hMul (α := α) (↑q.num : α) (↑r.num : α) / HMul.hMul (α := α) (↑q.den : α) (↑r.den : α)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
q : ℚ≥0
hq : Ne.{u_3 + 1} (α := α) (↑q.num : α) 0
⊢ Eq.{u_3 + 1} (α := α) (↑q⁻¹ : α) (↑q : α)⁻¹
have rw : Eq.{u_3 + 1} (α := α) (↑(divNat q.den q.num) : α) (↑q : α)⁻¹
Tactic: rw [inv_def, cast_divNat_of_ne_zero _ hq, cast_def, inv_div]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
q : ℚ≥0
hq : Ne.{u_3 + 1} (α := α) (↑q.num : α) 0
rw : Eq.{u_3 + 1} (α := α) (↑(divNat q.den q.num) : α) (↑q : α)⁻¹
⊢ Eq.{u_3 + 1} (α := α) (↑q⁻¹ : α) (↑q : α)⁻¹
have rw₁ : HDiv.hDiv (α := α) (↑q.den : α) (↑q.num : α) = (↑q : α)⁻¹
Tactic: rw [inv_def, cast_divNat_of_ne_zero _ hq, cast_def, inv_div]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
q : ℚ≥0
hq : Ne.{u_3 + 1} (α := α) (↑q.num : α) 0
rw : Eq.{u_3 + 1} (α := α) (↑(divNat q.den q.num) : α) (↑q : α)⁻¹
rw₁ : HDiv.hDiv (α := α) (↑q.den : α) (↑q.num : α) = (↑q : α)⁻¹
⊢ Eq.{u_3 + 1} (α := α) (↑q⁻¹ : α) (↑q : α)⁻¹
have rw₂ : HDiv.hDiv (α := α) (↑q.den : α) (↑q.num : α) = (HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α))⁻¹
Tactic: rw [inv_def, cast_divNat_of_ne_zero _ hq, cast_def, inv_div]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
q : ℚ≥0
hq : Ne.{u_3 + 1} (α := α) (↑q.num : α) 0
rw : Eq.{u_3 + 1} (α := α) (↑(divNat q.den q.num) : α) (↑q : α)⁻¹
rw₁ : HDiv.hDiv (α := α) (↑q.den : α) (↑q.num : α) = (↑q : α)⁻¹
rw₂ : HDiv.hDiv (α := α) (↑q.den : α) (↑q.num : α) = (HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α))⁻¹
⊢ Eq.{u_3 + 1} (α := α) (↑q⁻¹ : α) (↑q : α)⁻¹
have rw₃ : HDiv.hDiv (α := α) (↑q.den : α) (↑q.num : α) = HDiv.hDiv (α := α) (↑q.den : α) (↑q.num : α)
Tactic: rw [inv_def, cast_divNat_of_ne_zero _ hq, cast_def, inv_div]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
q r : ℚ≥0
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
hr : Ne.{u_3 + 1} (α := α) (↑r.num : α) 0
⊢ (↑(q / r) : α) = HDiv.hDiv (α := α) (↑q : α) (↑r : α)
have rw : HDiv.hDiv (α := α) (↑(q.num * r.den) : α) (↑(q.den * r.num) : α) =
  HMul.hMul (α := α) (↑q.num : α) (↑r.den : α) / HMul.hMul (α := α) (↑q.den : α) (↑r.num : α)
Tactic: rw [div_def, cast_divNat_of_ne_zero, cast_def, cast_def, div_eq_mul_inv (_ / _),
    inv_div, (Nat.commute_cast _ _).div_mul_div_comm (Nat.commute_cast _ _)]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
q r : ℚ≥0
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
hr : Ne.{u_3 + 1} (α := α) (↑r.num : α) 0
rw :
  HDiv.hDiv (α := α) (↑(q.num * r.den) : α) (↑(q.den * r.num) : α) =
    HMul.hMul (α := α) (↑q.num : α) (↑r.den : α) / HMul.hMul (α := α) (↑q.den : α) (↑r.num : α)
⊢ (↑(q / r) : α) = HDiv.hDiv (α := α) (↑q : α) (↑r : α)
have hb : Ne.{u_3 + 1} (α := α) (↑(q.den * r.num) : α) 0
Tactic: rw [div_def, cast_divNat_of_ne_zero, cast_def, cast_def, div_eq_mul_inv (_ / _),
    inv_div, (Nat.commute_cast _ _).div_mul_div_comm (Nat.commute_cast _ _)]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
q r : ℚ≥0
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
hr : Ne.{u_3 + 1} (α := α) (↑r.num : α) 0
⊢ HDiv.hDiv (α := α) (↑(q.num * r.den) : α) (↑(q.den * r.num) : α) =
    HMul.hMul (α := α) (↑q.num : α) (↑r.den : α) / HMul.hMul (α := α) (↑q.den : α) (↑r.num : α)
have push_cast : HMul.hMul (α := α) (↑q.num : α) (↑r.den : α) / HMul.hMul (α := α) (↑q.den : α) (↑r.num : α) =
  HMul.hMul (α := α) (↑q.num : α) (↑r.den : α) / HMul.hMul (α := α) (↑q.den : α) (↑r.num : α)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
q r : ℚ≥0
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
hr : Ne.{u_3 + 1} (α := α) (↑r.num : α) 0
⊢ Ne.{u_3 + 1} (α := α) (↑(q.den * r.num) : α) 0
have hb : HMul.hMul (α := α) (↑q.den : α) (↑r.num : α) ≠ 0
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
n : ℤ
⊢ HDiv.hDiv (α := α) (↑n : α) (↑1 : α) = (↑n : α)
have rw : HDiv.hDiv (α := α) (↑n : α) 1 = (↑n : α)
Tactic: rw [Nat.cast_one, div_one]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
n : ℤ
rw : HDiv.hDiv (α := α) (↑n : α) 1 = (↑n : α)
⊢ HDiv.hDiv (α := α) (↑n : α) (↑1 : α) = (↑n : α)
have rw₁ : Eq.{u_3 + 1} (α := α) (↑n : α) (↑n : α)
Tactic: rw [Nat.cast_one, div_one]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
n : ℕ
⊢ Eq.{u_3 + 1} (α := α) (↑(↑n : ℚ) : α) (↑n : α)
have rw : Eq.{u_3 + 1} (α := α) (↑(↑(↑n : ℤ) : ℚ) : α) (↑n : α)
Tactic: rw [← Int.cast_natCast, cast_intCast, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
n : ℕ
rw : Eq.{u_3 + 1} (α := α) (↑(↑(↑n : ℤ) : ℚ) : α) (↑n : α)
⊢ Eq.{u_3 + 1} (α := α) (↑(↑n : ℚ) : α) (↑n : α)
have rw₁ : Eq.{u_3 + 1} (α := α) (↑(↑n : ℤ) : α) (↑n : α)
Tactic: rw [← Int.cast_natCast, cast_intCast, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
n : ℕ
rw : Eq.{u_3 + 1} (α := α) (↑(↑(↑n : ℤ) : ℚ) : α) (↑n : α)
rw₁ : Eq.{u_3 + 1} (α := α) (↑(↑n : ℤ) : α) (↑n : α)
⊢ Eq.{u_3 + 1} (α := α) (↑(↑n : ℚ) : α) (↑n : α)
have rw₂ : Eq.{u_3 + 1} (α := α) (↑n : α) (↑n : α)
Tactic: rw [← Int.cast_natCast, cast_intCast, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
⊢ b ≠ 0
have refine : b = 0 → Eq.{u_3 + 1} (α := α) (↑b : α) 0
Tactic: refine mt ?_ b0
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (hypothesis)
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
⊢ (↑(a /. b) : α) = HDiv.hDiv (α := α) (↑a : α) (↑b : α)
have b0' : b ≠ 0
Tactic: have b0' : b ≠ 0 := by
    refine mt ?_ b0
    simp +contextual
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
b0' : b ≠ 0
⊢ (↑(a /. b) : α) = HDiv.hDiv (α := α) (↑a : α) (↑b : α)
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 } : α) = HDiv.hDiv (α := α) (↑a : α) (↑b : α)
Tactic: rcases e : a /. b with ⟨n, d, h, c⟩
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (hypothesis)
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
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 }
d0 : Eq.{u_3 + 1} (α := α) (↑d : α) 0
⊢ False
have dd : (↑(a /. b).den : ℤ) ∣ b
Tactic: have dd := den_dvd a b
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
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 }
d0 : Eq.{u_3 + 1} (α := α) (↑d : α) 0
dd : (↑(a /. b).den : ℤ) ∣ b
⊢ (↑d : ℤ) ∣ b
have rwa : ∀ (dd : (↑{ num := n, den := d, den_nz := h, reduced := c }.den : ℤ) ∣ b), (↑d : ℤ) ∣ b
Tactic: rwa [e] at dd
Cleared hypotheses: dd
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
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 }
d0 : Eq.{u_3 + 1} (α := α) (↑d : α) 0
dd : (↑(a /. b).den : ℤ) ∣ b
⊢ False
have rcases : ∀ (k : ℤ) (ke : b = (↑d : ℤ) * k), False
Tactic: rcases show (d : ℤ) ∣ b by rwa [e] at dd with ⟨k, ke⟩
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
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 }
d0 : Eq.{u_3 + 1} (α := α) (↑d : α) 0
dd : (↑(a /. b).den : ℤ) ∣ b
k : ℤ
ke : b = (↑d : ℤ) * k
⊢ (↑b : α) = HMul.hMul (α := α) (↑d : α) (↑k : α)
have rw : (↑((↑d : ℤ) * k) : α) = HMul.hMul (α := α) (↑d : α) (↑k : α)
Tactic: rw [ke, Int.cast_mul, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
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 }
d0 : Eq.{u_3 + 1} (α := α) (↑d : α) 0
dd : (↑(a /. b).den : ℤ) ∣ b
k : ℤ
ke : b = (↑d : ℤ) * k
rw : (↑((↑d : ℤ) * k) : α) = HMul.hMul (α := α) (↑d : α) (↑k : α)
⊢ (↑b : α) = HMul.hMul (α := α) (↑d : α) (↑k : α)
have rw₁ : HMul.hMul (α := α) (↑(↑d : ℤ) : α) (↑k : α) = HMul.hMul (α := α) (↑d : α) (↑k : α)
Tactic: rw [ke, Int.cast_mul, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
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 }
d0 : Eq.{u_3 + 1} (α := α) (↑d : α) 0
dd : (↑(a /. b).den : ℤ) ∣ b
k : ℤ
ke : b = (↑d : ℤ) * k
rw : (↑((↑d : ℤ) * k) : α) = HMul.hMul (α := α) (↑d : α) (↑k : α)
rw₁ : HMul.hMul (α := α) (↑(↑d : ℤ) : α) (↑k : α) = HMul.hMul (α := α) (↑d : α) (↑k : α)
⊢ (↑b : α) = HMul.hMul (α := α) (↑d : α) (↑k : α)
have rw₂ : HMul.hMul (α := α) (↑d : α) (↑k : α) = HMul.hMul (α := α) (↑d : α) (↑k : α)
Tactic: rw [ke, Int.cast_mul, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (hypothesis)
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
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 }
d0 : Eq.{u_3 + 1} (α := α) (↑d : α) 0
dd : (↑(a /. b).den : ℤ) ∣ b
k : ℤ
ke : b = (↑d : ℤ) * k
⊢ False
have this : (↑b : α) = HMul.hMul (α := α) (↑d : α) (↑k : α)
Tactic: have : (b : α) = (d : α) * (k : α) := by rw [ke, Int.cast_mul, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (hypothesis)
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
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 }
d0 : Eq.{u_3 + 1} (α := α) (↑d : α) 0
dd : (↑(a /. b).den : ℤ) ∣ b
k : ℤ
ke : b = (↑d : ℤ) * k
this : (↑b : α) = HMul.hMul (α := α) (↑d : α) (↑k : α)
⊢ False
have this₁ : Eq.{u_3 + 1} (α := α) (↑b : α) 0
Tactic: rw [d0, zero_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (hypothesis)
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
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 } : α) = HDiv.hDiv (α := α) (↑a : α) (↑b : α)
have d0 : Ne.{u_3 + 1} (α := α) (↑d : α) 0
Tactic: have d0 : (d : α) ≠ 0 := by
    intro d0
    have dd := den_dvd a b
    rcases show (d : ℤ) ∣ b by rwa [e] at dd with ⟨k, ke⟩
    have : (b : α) = (d : α) * (k : α) := by rw [ke, Int.cast_mul, Int.cast_natCast]
    rw [d0, zero_mul] at this
    contradiction
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (hypothesis)
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
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 }
d0 : Ne.{u_3 + 1} (α := α) (↑d : α) 0
⊢ (↑{ num := n, den := d, den_nz := h, reduced := c } : α) = HDiv.hDiv (α := α) (↑a : α) (↑b : α)
have e₁ : a /. b = n /. (↑d : ℤ)
Tactic: rw [mk_eq_divInt] at e
Cleared hypotheses: e, d0
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (hypothesis)
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = n /. (↑d : ℤ)
d0 : Ne.{u_3 + 1} (α := α) (↑d : α) 0
⊢ (↑{ num := n, den := d, den_nz := h, reduced := c } : α) = HDiv.hDiv (α := α) (↑a : α) (↑b : α)
have this : Eq.{u_3 + 1} (α := α) (↑(a * (↑d : ℤ)) : α) (↑(n * b) : α)
Tactic: have := congr_arg ((↑) : ℤ → α)
    ((divInt_eq_divInt_iff b0' <| ne_of_gt <| Int.natCast_pos.2 h.bot_lt).1 e)
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (hypothesis)
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = n /. (↑d : ℤ)
d0 : Ne.{u_3 + 1} (α := α) (↑d : α) 0
this : Eq.{u_3 + 1} (α := α) (↑(a * (↑d : ℤ)) : α) (↑(n * b) : α)
⊢ (↑{ num := n, den := d, den_nz := h, reduced := c } : α) = HDiv.hDiv (α := α) (↑a : α) (↑b : α)
have this₁ : HMul.hMul (α := α) (↑a : α) (↑d : α) = HMul.hMul (α := α) (↑n : α) (↑b : α)
Tactic: rw [Int.cast_mul, Int.cast_mul, Int.cast_natCast] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = n /. (↑d : ℤ)
d0 : Ne.{u_3 + 1} (α := α) (↑d : α) 0
this : HMul.hMul (α := α) (↑a : α) (↑d : α) = HMul.hMul (α := α) (↑n : α) (↑b : α)
⊢ (↑{ num := n, den := d, den_nz := h, reduced := c } : α) = HDiv.hDiv (α := α) (↑a : α) (↑b : α)
have rw : HDiv.hDiv (α := α) (↑a : α) (↑b : α) = (↑{ num := n, den := d, den_nz := h, reduced := c } : α)
Tactic: rw [eq_comm, cast_def, div_eq_mul_inv, eq_div_iff_mul_eq d0, mul_assoc, (d.commute_cast _).eq,
    ← mul_assoc, this, mul_assoc, mul_inv_cancel₀ b0, mul_one]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = n /. (↑d : ℤ)
d0 : Ne.{u_3 + 1} (α := α) (↑d : α) 0
this : HMul.hMul (α := α) (↑a : α) (↑d : α) = HMul.hMul (α := α) (↑n : α) (↑b : α)
rw : HDiv.hDiv (α := α) (↑a : α) (↑b : α) = (↑{ num := n, den := d, den_nz := h, reduced := c } : α)
⊢ (↑{ num := n, den := d, den_nz := h, reduced := c } : α) = HDiv.hDiv (α := α) (↑a : α) (↑b : α)
have rw₁ : HDiv.hDiv (α := α) (↑a : α) (↑b : α) =
  HDiv.hDiv (α := α) (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
    (↑{ num := n, den := d, den_nz := h, reduced := c }.den : α)
Tactic: rw [eq_comm, cast_def, div_eq_mul_inv, eq_div_iff_mul_eq d0, mul_assoc, (d.commute_cast _).eq,
    ← mul_assoc, this, mul_assoc, mul_inv_cancel₀ b0, mul_one]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = n /. (↑d : ℤ)
d0 : Ne.{u_3 + 1} (α := α) (↑d : α) 0
this : HMul.hMul (α := α) (↑a : α) (↑d : α) = HMul.hMul (α := α) (↑n : α) (↑b : α)
rw : HDiv.hDiv (α := α) (↑a : α) (↑b : α) = (↑{ num := n, den := d, den_nz := h, reduced := c } : α)
rw₁ :
  HDiv.hDiv (α := α) (↑a : α) (↑b : α) =
    HDiv.hDiv (α := α) (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
      (↑{ num := n, den := d, den_nz := h, reduced := c }.den : α)
⊢ (↑{ num := n, den := d, den_nz := h, reduced := c } : α) = HDiv.hDiv (α := α) (↑a : α) (↑b : α)
have rw₂ : HMul.hMul (α := α) (↑a : α) (↑b : α)⁻¹ =
  HDiv.hDiv (α := α) (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
    (↑{ num := n, den := d, den_nz := h, reduced := c }.den : α)
Tactic: rw [eq_comm, cast_def, div_eq_mul_inv, eq_div_iff_mul_eq d0, mul_assoc, (d.commute_cast _).eq,
    ← mul_assoc, this, mul_assoc, mul_inv_cancel₀ b0, mul_one]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = n /. (↑d : ℤ)
d0 : Ne.{u_3 + 1} (α := α) (↑d : α) 0
this : HMul.hMul (α := α) (↑a : α) (↑d : α) = HMul.hMul (α := α) (↑n : α) (↑b : α)
rw : HDiv.hDiv (α := α) (↑a : α) (↑b : α) = (↑{ num := n, den := d, den_nz := h, reduced := c } : α)
rw₁ :
  HDiv.hDiv (α := α) (↑a : α) (↑b : α) =
    HDiv.hDiv (α := α) (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
      (↑{ num := n, den := d, den_nz := h, reduced := c }.den : α)
rw₂ :
  HMul.hMul (α := α) (↑a : α) (↑b : α)⁻¹ =
    HDiv.hDiv (α := α) (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
      (↑{ num := n, den := d, den_nz := h, reduced := c }.den : α)
⊢ (↑{ num := n, den := d, den_nz := h, reduced := c } : α) = HDiv.hDiv (α := α) (↑a : α) (↑b : α)
have rw₃ : HMul.hMul (α := α) (↑a : α) (↑b : α)⁻¹ * (↑d : α) = (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
Tactic: rw [eq_comm, cast_def, div_eq_mul_inv, eq_div_iff_mul_eq d0, mul_assoc, (d.commute_cast _).eq,
    ← mul_assoc, this, mul_assoc, mul_inv_cancel₀ b0, mul_one]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = n /. (↑d : ℤ)
d0 : Ne.{u_3 + 1} (α := α) (↑d : α) 0
this : HMul.hMul (α := α) (↑a : α) (↑d : α) = HMul.hMul (α := α) (↑n : α) (↑b : α)
rw : HDiv.hDiv (α := α) (↑a : α) (↑b : α) = (↑{ num := n, den := d, den_nz := h, reduced := c } : α)
rw₁ :
  HDiv.hDiv (α := α) (↑a : α) (↑b : α) =
    HDiv.hDiv (α := α) (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
      (↑{ num := n, den := d, den_nz := h, reduced := c }.den : α)
rw₂ :
  HMul.hMul (α := α) (↑a : α) (↑b : α)⁻¹ =
    HDiv.hDiv (α := α) (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
      (↑{ num := n, den := d, den_nz := h, reduced := c }.den : α)
rw₃ : HMul.hMul (α := α) (↑a : α) (↑b : α)⁻¹ * (↑d : α) = (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
⊢ (↑{ num := n, den := d, den_nz := h, reduced := c } : α) = HDiv.hDiv (α := α) (↑a : α) (↑b : α)
have rw₄ : (↑a : α) * HMul.hMul (α := α) (↑b : α)⁻¹ (↑d : α) = (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
Tactic: rw [eq_comm, cast_def, div_eq_mul_inv, eq_div_iff_mul_eq d0, mul_assoc, (d.commute_cast _).eq,
    ← mul_assoc, this, mul_assoc, mul_inv_cancel₀ b0, mul_one]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = n /. (↑d : ℤ)
d0 : Ne.{u_3 + 1} (α := α) (↑d : α) 0
this : HMul.hMul (α := α) (↑a : α) (↑d : α) = HMul.hMul (α := α) (↑n : α) (↑b : α)
rw : HDiv.hDiv (α := α) (↑a : α) (↑b : α) = (↑{ num := n, den := d, den_nz := h, reduced := c } : α)
rw₁ :
  HDiv.hDiv (α := α) (↑a : α) (↑b : α) =
    HDiv.hDiv (α := α) (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
      (↑{ num := n, den := d, den_nz := h, reduced := c }.den : α)
rw₂ :
  HMul.hMul (α := α) (↑a : α) (↑b : α)⁻¹ =
    HDiv.hDiv (α := α) (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
      (↑{ num := n, den := d, den_nz := h, reduced := c }.den : α)
rw₃ : HMul.hMul (α := α) (↑a : α) (↑b : α)⁻¹ * (↑d : α) = (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
rw₄ : (↑a : α) * HMul.hMul (α := α) (↑b : α)⁻¹ (↑d : α) = (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
⊢ (↑{ num := n, den := d, den_nz := h, reduced := c } : α) = HDiv.hDiv (α := α) (↑a : α) (↑b : α)
have rw₅ : (↑a : α) * HMul.hMul (α := α) (↑d : α) (↑b : α)⁻¹ = (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
Tactic: rw [eq_comm, cast_def, div_eq_mul_inv, eq_div_iff_mul_eq d0, mul_assoc, (d.commute_cast _).eq,
    ← mul_assoc, this, mul_assoc, mul_inv_cancel₀ b0, mul_one]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = n /. (↑d : ℤ)
d0 : Ne.{u_3 + 1} (α := α) (↑d : α) 0
this : HMul.hMul (α := α) (↑a : α) (↑d : α) = HMul.hMul (α := α) (↑n : α) (↑b : α)
rw : HDiv.hDiv (α := α) (↑a : α) (↑b : α) = (↑{ num := n, den := d, den_nz := h, reduced := c } : α)
rw₁ :
  HDiv.hDiv (α := α) (↑a : α) (↑b : α) =
    HDiv.hDiv (α := α) (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
      (↑{ num := n, den := d, den_nz := h, reduced := c }.den : α)
rw₂ :
  HMul.hMul (α := α) (↑a : α) (↑b : α)⁻¹ =
    HDiv.hDiv (α := α) (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
      (↑{ num := n, den := d, den_nz := h, reduced := c }.den : α)
rw₃ : HMul.hMul (α := α) (↑a : α) (↑b : α)⁻¹ * (↑d : α) = (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
rw₄ : (↑a : α) * HMul.hMul (α := α) (↑b : α)⁻¹ (↑d : α) = (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
rw₅ : (↑a : α) * HMul.hMul (α := α) (↑d : α) (↑b : α)⁻¹ = (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
⊢ (↑{ num := n, den := d, den_nz := h, reduced := c } : α) = HDiv.hDiv (α := α) (↑a : α) (↑b : α)
have rw₆ : HMul.hMul (α := α) (↑a : α) (↑d : α) * (↑b : α)⁻¹ = (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
Tactic: rw [eq_comm, cast_def, div_eq_mul_inv, eq_div_iff_mul_eq d0, mul_assoc, (d.commute_cast _).eq,
    ← mul_assoc, this, mul_assoc, mul_inv_cancel₀ b0, mul_one]