awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : α)
rw₆ : HMul.hMul (α := α) (↑a : α) (↑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 (α := α) (↑n : α) (↑b : α) * (↑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 : α)
rw₆ : HMul.hMul (α := α) (↑a : α) (↑d : α) * (↑b : α)⁻¹ = (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
rw₇ : HMul.hMul (α := α) (↑n : α) (↑b : α) * (↑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₈ : (↑n : α) * HMul.hMul (α := α) (↑b : α) (↑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 : α)
rw₆ : HMul.hMul (α := α) (↑a : α) (↑d : α) * (↑b : α)⁻¹ = (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
rw₇ : HMul.hMul (α := α) (↑n : α) (↑b : α) * (↑b : α)⁻¹ = (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
rw₈ : (↑n : α) * HMul.hMul (α := α) (↑b : α) (↑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 (α := α) (↑n : α) 1 = (↑{ 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 : α)
rw₆ : HMul.hMul (α := α) (↑a : α) (↑d : α) * (↑b : α)⁻¹ = (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
rw₇ : HMul.hMul (α := α) (↑n : α) (↑b : α) * (↑b : α)⁻¹ = (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
rw₈ : (↑n : α) * HMul.hMul (α := α) (↑b : α) (↑b : α)⁻¹ = (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
rw₉ : HMul.hMul (α := α) (↑n : α) 1 = (↑{ 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₁₀ : Eq.{u_3 + 1} (α := α) (↑n : α) (↑{ 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 : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
⊢ (↑(mkRat a b) : α) = HDiv.hDiv (α := α) (↑a : α) (↑b : α)
have b0 : Ne.{u_3 + 1} (α := α) (↑(↑b : ℤ) : α) 0
Tactic: rw [Rat.mkRat_eq_divInt, cast_divInt_of_ne_zero, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
q r : ℚ
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
hr : Ne.{u_3 + 1} (α := α) (↑r.den : α) 0
⊢ (↑(q + r) : α) = HAdd.hAdd (α := α) (↑q : α) (↑r : α)
have rw : HDiv.hDiv (α := α) (↑(q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num) : α) (↑(q.den * r.den) : α) =
  (HMul.hMul (α := α) (↑q.num : α) (↑r.den : α) + HMul.hMul (α := α) (↑q.den : α) (↑r.num : α)) /
    HMul.hMul (α := α) (↑q.den : α) (↑r.den : α)
Tactic: rw [add_def', cast_mkRat_of_ne_zero, cast_def, cast_def, mul_comm r.num,
    (Nat.cast_commute _ _).div_add_div (Nat.commute_cast _ _) hq hr]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
q r : ℚ
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
hr : Ne.{u_3 + 1} (α := α) (↑r.den : α) 0
rw :
  HDiv.hDiv (α := α) (↑(q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num) : α) (↑(q.den * r.den) : α) =
    (HMul.hMul (α := α) (↑q.num : α) (↑r.den : α) + HMul.hMul (α := α) (↑q.den : α) (↑r.num : α)) /
      HMul.hMul (α := α) (↑q.den : α) (↑r.den : α)
⊢ (↑(q + r) : α) = HAdd.hAdd (α := α) (↑q : α) (↑r : α)
have hb : Ne.{u_3 + 1} (α := α) (↑(q.den * r.den) : α) 0
Tactic: rw [add_def', cast_mkRat_of_ne_zero, cast_def, cast_def, mul_comm r.num,
    (Nat.cast_commute _ _).div_add_div (Nat.commute_cast _ _) hq hr]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
q r : ℚ
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
hr : Ne.{u_3 + 1} (α := α) (↑r.den : α) 0
⊢ HDiv.hDiv (α := α) (↑(q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num) : α) (↑(q.den * r.den) : α) =
    (HMul.hMul (α := α) (↑q.num : α) (↑r.den : α) + HMul.hMul (α := α) (↑q.den : α) (↑r.num : α)) /
      HMul.hMul (α := α) (↑q.den : α) (↑r.den : α)
have push_cast : (HMul.hMul (α := α) (↑q.num : α) (↑r.den : α) + HMul.hMul (α := α) (↑q.den : α) (↑r.num : α)) /
    HMul.hMul (α := α) (↑q.den : α) (↑r.den : α) =
  (HMul.hMul (α := α) (↑q.num : α) (↑r.den : α) + HMul.hMul (α := α) (↑q.den : α) (↑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 : DivisionRing α
q r : ℚ
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
hr : Ne.{u_3 + 1} (α := α) (↑r.den : α) 0
⊢ Ne.{u_3 + 1} (α := α) (↑(q.den * r.den) : α) 0
have hb : HMul.hMul (α := α) (↑q.den : α) (↑r.den : α) ≠ 0
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
p q : ℚ
hp : Ne.{u_3 + 1} (α := α) (↑p.den : α) 0
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
⊢ (↑(p * q) : α) = HMul.hMul (α := α) (↑p : α) (↑q : α)
have rw : HDiv.hDiv (α := α) (↑(p.num * q.num) : α) (↑(p.den * q.den) : α) =
  HMul.hMul (α := α) (↑p.num : α) (↑q.num : α) / HMul.hMul (α := α) (↑p.den : α) (↑q.den : α)
Tactic: rw [mul_eq_mkRat, cast_mkRat_of_ne_zero, cast_def, cast_def,
    (Nat.commute_cast _ _).div_mul_div_comm (Int.commute_cast _ _)]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
p q : ℚ
hp : Ne.{u_3 + 1} (α := α) (↑p.den : α) 0
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
rw :
  HDiv.hDiv (α := α) (↑(p.num * q.num) : α) (↑(p.den * q.den) : α) =
    HMul.hMul (α := α) (↑p.num : α) (↑q.num : α) / HMul.hMul (α := α) (↑p.den : α) (↑q.den : α)
⊢ (↑(p * q) : α) = HMul.hMul (α := α) (↑p : α) (↑q : α)
have hb : Ne.{u_3 + 1} (α := α) (↑(p.den * q.den) : α) 0
Tactic: rw [mul_eq_mkRat, cast_mkRat_of_ne_zero, cast_def, cast_def,
    (Nat.commute_cast _ _).div_mul_div_comm (Int.commute_cast _ _)]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
p q : ℚ
hp : Ne.{u_3 + 1} (α := α) (↑p.den : α) 0
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
⊢ HDiv.hDiv (α := α) (↑(p.num * q.num) : α) (↑(p.den * q.den) : α) =
    HMul.hMul (α := α) (↑p.num : α) (↑q.num : α) / HMul.hMul (α := α) (↑p.den : α) (↑q.den : α)
have push_cast : HMul.hMul (α := α) (↑p.num : α) (↑q.num : α) / HMul.hMul (α := α) (↑p.den : α) (↑q.den : α) =
  HMul.hMul (α := α) (↑p.num : α) (↑q.num : α) / HMul.hMul (α := α) (↑p.den : α) (↑q.den : α)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
p q : ℚ
hp : Ne.{u_3 + 1} (α := α) (↑p.den : α) 0
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
⊢ Ne.{u_3 + 1} (α := α) (↑(p.den * q.den) : α) 0
have hb : HMul.hMul (α := α) (↑p.den : α) (↑q.den : α) ≠ 0
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
q : ℚ
hq : Ne.{u_3 + 1} (α := α) (↑q.num : α) 0
⊢ Eq.{u_3 + 1} (α := α) (↑q⁻¹ : α) (↑q : α)⁻¹
have rw : Eq.{u_3 + 1} (α := α) (↑((↑q.den : ℤ) /. q.num) : α) (↑q : α)⁻¹
Tactic: rw [inv_def, cast_divInt_of_ne_zero _ hq, cast_def, inv_div, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
q : ℚ
hq : Ne.{u_3 + 1} (α := α) (↑q.num : α) 0
rw : Eq.{u_3 + 1} (α := α) (↑((↑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_divInt_of_ne_zero _ hq, cast_def, inv_div, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
q : ℚ
hq : Ne.{u_3 + 1} (α := α) (↑q.num : α) 0
rw : Eq.{u_3 + 1} (α := α) (↑((↑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_divInt_of_ne_zero _ hq, cast_def, inv_div, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
q : ℚ
hq : Ne.{u_3 + 1} (α := α) (↑q.num : α) 0
rw : Eq.{u_3 + 1} (α := α) (↑((↑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_divInt_of_ne_zero _ hq, cast_def, inv_div, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
q : ℚ
hq : Ne.{u_3 + 1} (α := α) (↑q.num : α) 0
rw : Eq.{u_3 + 1} (α := α) (↑((↑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 : α))⁻¹
rw₃ : HDiv.hDiv (α := α) (↑(↑q.den : ℤ) : α) (↑q.num : α) = HDiv.hDiv (α := α) (↑q.den : α) (↑q.num : α)
⊢ 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_divInt_of_ne_zero _ hq, cast_def, inv_div, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
p q : ℚ
hp : Ne.{u_3 + 1} (α := α) (↑p.den : α) 0
hq : Ne.{u_3 + 1} (α := α) (↑q.num : α) 0
⊢ (↑(p / q) : α) = HDiv.hDiv (α := α) (↑p : α) (↑q : α)
have rw : HDiv.hDiv (α := α) (↑(p.num * (↑q.den : ℤ)) : α) (↑((↑p.den : ℤ) * q.num) : α) =
  HMul.hMul (α := α) (↑p.num : α) (↑q.den : α) / HMul.hMul (α := α) (↑p.den : α) (↑q.num : α)
Tactic: rw [div_def', cast_divInt_of_ne_zero, cast_def, cast_def, div_eq_mul_inv (_ / _), inv_div,
    (Int.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 : DivisionRing α
p q : ℚ
hp : Ne.{u_3 + 1} (α := α) (↑p.den : α) 0
hq : Ne.{u_3 + 1} (α := α) (↑q.num : α) 0
rw :
  HDiv.hDiv (α := α) (↑(p.num * (↑q.den : ℤ)) : α) (↑((↑p.den : ℤ) * q.num) : α) =
    HMul.hMul (α := α) (↑p.num : α) (↑q.den : α) / HMul.hMul (α := α) (↑p.den : α) (↑q.num : α)
⊢ (↑(p / q) : α) = HDiv.hDiv (α := α) (↑p : α) (↑q : α)
have b0 : Ne.{u_3 + 1} (α := α) (↑((↑p.den : ℤ) * q.num) : α) 0
Tactic: rw [div_def', cast_divInt_of_ne_zero, cast_def, cast_def, div_eq_mul_inv (_ / _), inv_div,
    (Int.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 : DivisionRing α
p q : ℚ
hp : Ne.{u_3 + 1} (α := α) (↑p.den : α) 0
hq : Ne.{u_3 + 1} (α := α) (↑q.num : α) 0
⊢ HDiv.hDiv (α := α) (↑(p.num * (↑q.den : ℤ)) : α) (↑((↑p.den : ℤ) * q.num) : α) =
    HMul.hMul (α := α) (↑p.num : α) (↑q.den : α) / HMul.hMul (α := α) (↑p.den : α) (↑q.num : α)
have push_cast : HMul.hMul (α := α) (↑p.num : α) (↑q.den : α) / HMul.hMul (α := α) (↑p.den : α) (↑q.num : α) =
  HMul.hMul (α := α) (↑p.num : α) (↑q.den : α) / HMul.hMul (α := α) (↑p.den : α) (↑q.num : α)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionRing α
p q : ℚ
hp : Ne.{u_3 + 1} (α := α) (↑p.den : α) 0
hq : Ne.{u_3 + 1} (α := α) (↑q.num : α) 0
⊢ Ne.{u_3 + 1} (α := α) (↑((↑p.den : ℤ) * q.num) : α) 0
have b0 : HMul.hMul (α := α) (↑p.den : α) (↑q.num : α) ≠ 0
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
F : Type u_1
α : Type u_3
β : Type u_4
inst : FunLike F α β
inst_1 : DivisionSemiring α
inst_2 : DivisionSemiring β
inst_3 : RingHomClass F α β
f : F
q : ℚ≥0
⊢ Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (↑q : α) : β) ((↑q : β) : β)
have simp_rw : (f : (a : α) → β) (HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)) = HDiv.hDiv (α := β) (↑q.num : β) (↑q.den : β)
Tactic: simp_rw [NNRat.cast_def, map_div₀, map_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
F : Type u_1
α : Type u_3
β : Type u_4
inst : FunLike F α β
inst_1 : DivisionSemiring α
inst_2 : DivisionSemiring β
inst_3 : RingHomClass F α β
f : F
q : ℚ≥0
simp_rw :
  (f : (a : α) → β) (HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)) = HDiv.hDiv (α := β) (↑q.num : β) (↑q.den : β)
⊢ Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (↑q : α) : β) ((↑q : β) : β)
have simp_rw₁ : HDiv.hDiv (α := β) (β := β) ((f : (a : α) → β) (↑q.num : α) : β) ((f : (a : α) → β) (↑q.den : α) : β) =
  HDiv.hDiv (α := β) (↑q.num : β) (↑q.den : β)
Tactic: simp_rw [NNRat.cast_def, map_div₀, map_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
F : Type u_1
α : Type u_3
inst : DivisionSemiring α
inst_1 : FunLike F ℚ≥0 α
inst_2 : RingHomClass F ℚ≥0 α
f : F
q : ℚ≥0
⊢ Eq.{u_3 + 1} (α := α) ((f : (a : ℚ≥0) → α) q : α) ((↑q : α) : α)
have rw : Eq.{u_3 + 1} (α := α) ((f : (a : ℚ≥0) → α) q : α) ((f : (a : ℚ≥0) → α) (↑q : ℚ≥0) : α)
Tactic: rw [← map_nnratCast f, NNRat.cast_id]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
F : Type u_1
α : Type u_3
inst : DivisionSemiring α
inst_1 : FunLike F ℚ≥0 α
inst_2 : RingHomClass F ℚ≥0 α
f : F
q : ℚ≥0
rw : Eq.{u_3 + 1} (α := α) ((f : (a : ℚ≥0) → α) q : α) ((f : (a : ℚ≥0) → α) (↑q : ℚ≥0) : α)
⊢ Eq.{u_3 + 1} (α := α) ((f : (a : ℚ≥0) → α) q : α) ((↑q : α) : α)
have rw₁ : Eq.{u_3 + 1} (α := α) ((f : (a : ℚ≥0) → α) q : α) ((f : (a : ℚ≥0) → α) q : α)
Tactic: rw [← map_nnratCast f, NNRat.cast_id]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
F : Type u_1
α : Type u_3
β : Type u_4
inst : FunLike F α β
inst_1 : DivisionRing α
inst_2 : DivisionRing β
inst_3 : RingHomClass F α β
f : F
q : ℚ
⊢ Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (↑q : α) : β) ((↑q : β) : β)
have rw : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)) : β) ((↑q : β) : β)
Tactic: rw [cast_def, map_div₀, map_intCast, map_natCast, cast_def]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
F : Type u_1
α : Type u_3
β : Type u_4
inst : FunLike F α β
inst_1 : DivisionRing α
inst_2 : DivisionRing β
inst_3 : RingHomClass F α β
f : F
q : ℚ
rw : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)) : β) ((↑q : β) : β)
⊢ Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (↑q : α) : β) ((↑q : β) : β)
have rw₁ : HDiv.hDiv (α := β) (β := β) ((f : (a : α) → β) (↑q.num : α) : β) ((f : (a : α) → β) (↑q.den : α) : β) = (↑q : β)
Tactic: rw [cast_def, map_div₀, map_intCast, map_natCast, cast_def]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
F : Type u_1
α : Type u_3
β : Type u_4
inst : FunLike F α β
inst_1 : DivisionRing α
inst_2 : DivisionRing β
inst_3 : RingHomClass F α β
f : F
q : ℚ
rw : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)) : β) ((↑q : β) : β)
rw₁ : HDiv.hDiv (α := β) (β := β) ((f : (a : α) → β) (↑q.num : α) : β) ((f : (a : α) → β) (↑q.den : α) : β) = (↑q : β)
⊢ Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (↑q : α) : β) ((↑q : β) : β)
have rw₂ : HDiv.hDiv (α := β) (β := β) ((↑q.num : β) : β) ((f : (a : α) → β) (↑q.den : α) : β) = (↑q : β)
Tactic: rw [cast_def, map_div₀, map_intCast, map_natCast, cast_def]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
F : Type u_1
α : Type u_3
β : Type u_4
inst : FunLike F α β
inst_1 : DivisionRing α
inst_2 : DivisionRing β
inst_3 : RingHomClass F α β
f : F
q : ℚ
rw : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)) : β) ((↑q : β) : β)
rw₁ : HDiv.hDiv (α := β) (β := β) ((f : (a : α) → β) (↑q.num : α) : β) ((f : (a : α) → β) (↑q.den : α) : β) = (↑q : β)
rw₂ : HDiv.hDiv (α := β) (β := β) ((↑q.num : β) : β) ((f : (a : α) → β) (↑q.den : α) : β) = (↑q : β)
⊢ Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (↑q : α) : β) ((↑q : β) : β)
have rw₃ : HDiv.hDiv (α := β) (↑q.num : β) (↑q.den : β) = (↑q : β)
Tactic: rw [cast_def, map_div₀, map_intCast, map_natCast, cast_def]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
F : Type u_1
α : Type u_3
β : Type u_4
inst : FunLike F α β
inst_1 : DivisionRing α
inst_2 : DivisionRing β
inst_3 : RingHomClass F α β
f : F
q : ℚ
rw : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)) : β) ((↑q : β) : β)
rw₁ : HDiv.hDiv (α := β) (β := β) ((f : (a : α) → β) (↑q.num : α) : β) ((f : (a : α) → β) (↑q.den : α) : β) = (↑q : β)
rw₂ : HDiv.hDiv (α := β) (β := β) ((↑q.num : β) : β) ((f : (a : α) → β) (↑q.den : α) : β) = (↑q : β)
rw₃ : HDiv.hDiv (α := β) (↑q.num : β) (↑q.den : β) = (↑q : β)
⊢ Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (↑q : α) : β) ((↑q : β) : β)
have rw₄ : HDiv.hDiv (α := β) (↑q.num : β) (↑q.den : β) = HDiv.hDiv (α := β) (↑q.num : β) (↑q.den : β)
Tactic: rw [cast_def, map_div₀, map_intCast, map_natCast, cast_def]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
F : Type u_1
α : Type u_3
inst : DivisionRing α
inst_1 : FunLike F ℚ α
inst_2 : RingHomClass F ℚ α
f : F
q : ℚ
⊢ Eq.{u_3 + 1} (α := α) ((f : (a : ℚ) → α) q : α) ((↑q : α) : α)
have rw : Eq.{u_3 + 1} (α := α) ((f : (a : ℚ) → α) q : α) ((f : (a : ℚ) → α) (↑q : ℚ) : α)
Tactic: rw [← map_ratCast f, Rat.cast_id]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
F : Type u_1
α : Type u_3
inst : DivisionRing α
inst_1 : FunLike F ℚ α
inst_2 : RingHomClass F ℚ α
f : F
q : ℚ
rw : Eq.{u_3 + 1} (α := α) ((f : (a : ℚ) → α) q : α) ((f : (a : ℚ) → α) (↑q : ℚ) : α)
⊢ Eq.{u_3 + 1} (α := α) ((f : (a : ℚ) → α) q : α) ((↑q : α) : α)
have rw₁ : Eq.{u_3 + 1} (α := α) ((f : (a : ℚ) → α) q : α) ((f : (a : ℚ) → α) q : α)
Tactic: rw [← map_ratCast f, Rat.cast_id]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
F : Type u_1
M₀ : Type u_5
inst : MonoidWithZero M₀
inst_1 : FunLike F ℚ≥0 M₀
inst_2 : MonoidWithZeroHomClass F ℚ≥0 M₀
f g : F
h : ∀ (n : ℕ), Eq.{u_5 + 1} (α := M₀) ((f : (a : ℚ≥0) → M₀) (↑n : ℚ≥0) : M₀) ((g : (a : ℚ≥0) → M₀) (↑n : ℚ≥0) : M₀)
r : ℚ≥0
⊢ Eq.{u_5 + 1} (α := M₀) ((f : (a : ℚ≥0) → M₀) r : M₀) ((g : (a : ℚ≥0) → M₀) r : M₀)
have rw : Eq.{u_5 + 1} (α := M₀) ((f : (a : ℚ≥0) → M₀) (↑r.den : ℚ≥0) : M₀) ((g : (a : ℚ≥0) → M₀) (↑r.den : ℚ≥0) : M₀)
Tactic: rw [← r.num_div_den, div_eq_mul_inv, map_mul, map_mul, h, eq_on_inv₀ f g]