awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.CharZero (goal)
Goal:
α : Type u_3
inst : DivisionRing α
inst_1 : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
d₁a : Ne.{u_3 + 1} (α := α) (↑d₁ : α) 0
d₂a : Ne.{u_3 + 1} (α := α) (↑d₂ : α) 0
h : HDiv.hDiv (α := α) (↑n₁ : α) (↑d₁ : α) = HDiv.hDiv (α := α) (↑n₂ : α) (↑d₂ : α)
rwa : ∀ (h : HDiv.hDiv (α := α) (↑n₁ : α) (↑d₁ : α) * (↑d₂ : α) = (↑n₂ : α)), n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
rwa₁ : ∀ (h : HMul.hMul (α := α) (↑n₁ : α) (↑d₁ : α)⁻¹ * (↑d₂ : α) = (↑n₂ : α)), n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
rwa₂ : ∀ (h : (↑n₁ : α) * HMul.hMul (α := α) (↑d₁ : α)⁻¹ (↑d₂ : α) = (↑n₂ : α)), n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
rwa₃ : ∀ (h : (↑n₁ : α) * HMul.hMul (α := α) (↑d₂ : α) (↑d₁ : α)⁻¹ = (↑n₂ : α)), n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
rwa₄ : ∀ (h : HMul.hMul (α := α) (↑n₁ : α) (↑d₂ : α) * (↑d₁ : α)⁻¹ = (↑n₂ : α)), n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
rwa₅ : ∀ (h : HMul.hMul (α := α) (↑n₁ : α) (↑d₂ : α) / (↑d₁ : α) = (↑n₂ : α)), n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
rwa₆ : ∀ (h : (↑n₂ : α) = HMul.hMul (α := α) (↑n₁ : α) (↑d₂ : α) / (↑d₁ : α)), n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
rwa₇ :
  ∀ (h : HMul.hMul (α := α) (↑n₂ : α) (↑d₁ : α) = HMul.hMul (α := α) (↑n₁ : α) (↑d₂ : α)),
    n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
rwa₈ :
  ∀ (h : HMul.hMul (α := α) (↑n₁ : α) (↑d₂ : α) = HMul.hMul (α := α) (↑n₂ : α) (↑d₁ : α)),
    n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
rwa₉ :
  ∀ (h : HMul.hMul (α := α) (↑n₁ : α) (↑d₂ : α) = HMul.hMul (α := α) (↑n₂ : α) (↑(↑d₁ : ℤ) : α)),
    n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
rwa₁₀ : ∀ (h : HMul.hMul (α := α) (↑n₁ : α) (↑d₂ : α) = (↑(n₂ * (↑d₁ : ℤ)) : α)), n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
rwa₁₁ :
  ∀ (h : HMul.hMul (α := α) (↑n₁ : α) (↑(↑d₂ : ℤ) : α) = (↑(n₂ * (↑d₁ : ℤ)) : α)), n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
rwa₁₂ : ∀ (h : Eq.{u_3 + 1} (α := α) (↑(n₁ * (↑d₂ : ℤ)) : α) (↑(n₂ * (↑d₁ : ℤ)) : α)), n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
rwa₁₃ : ∀ (h : n₁ * (↑d₂ : ℤ) = n₂ * (↑d₁ : ℤ)), n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
⊢ n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
have rwa₁₄ : ∀ (h : mkRat n₁ d₁ = mkRat n₂ d₂), n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
Tactic: rwa [eq_div_iff_mul_eq d₂a, division_def, mul_assoc, (d₁.cast_commute (d₂ : α)).inv_left₀.eq,
      ← mul_assoc, ← division_def, eq_comm, eq_div_iff_mul_eq d₁a, eq_comm, ← Int.cast_natCast d₁,
      ← Int.cast_mul, ← Int.cast_natCast d₂, ← Int.cast_mul, Int.cast_inj, ← mkRat_eq_iff d₁0 d₂0]
      at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.CharZero (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
hpq : Eq.{u_3 + 1} (α := α) (↑p : α) (↑q : α)
⊢ p = q
have rw : ∀ (hpq : HMul.hMul (α := α) (↑p.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.num : α) (↑p.den : α)), p = q
Tactic: rw [NNRat.cast_def, NNRat.cast_def, Commute.div_eq_div_iff] at hpq
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.CharZero (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
hpq : Eq.{u_3 + 1} (α := α) (↑p : α) (↑q : α)
rw : ∀ (hpq : HMul.hMul (α := α) (↑p.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.num : α) (↑p.den : α)), p = q
⊢ p = q
have hbd : ∀ (hpq : HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) = HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)),
  Commute.{u_3} (S := α) (↑p.den : α) (↑q.den : α)
Tactic: rw [NNRat.cast_def, NNRat.cast_def, Commute.div_eq_div_iff] at hpq
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.CharZero (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
hpq : Eq.{u_3 + 1} (α := α) (↑p : α) (↑q : α)
rw : ∀ (hpq : HMul.hMul (α := α) (↑p.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.num : α) (↑p.den : α)), p = q
hbd :
  ∀ (hpq : HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) = HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)),
    Commute.{u_3} (S := α) (↑p.den : α) (↑q.den : α)
⊢ p = q
have hb : ∀ (hpq : HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) = HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)),
  Ne.{u_3 + 1} (α := α) (↑p.den : α) 0
Tactic: rw [NNRat.cast_def, NNRat.cast_def, Commute.div_eq_div_iff] at hpq
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.CharZero (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
hpq : Eq.{u_3 + 1} (α := α) (↑p : α) (↑q : α)
rw : ∀ (hpq : HMul.hMul (α := α) (↑p.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.num : α) (↑p.den : α)), p = q
hbd :
  ∀ (hpq : HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) = HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)),
    Commute.{u_3} (S := α) (↑p.den : α) (↑q.den : α)
hb :
  ∀ (hpq : HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) = HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)),
    Ne.{u_3 + 1} (α := α) (↑p.den : α) 0
⊢ p = q
have hd : ∀ (hpq : HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) = HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)),
  Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
Tactic: rw [NNRat.cast_def, NNRat.cast_def, Commute.div_eq_div_iff] at hpq
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.CharZero (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
hpq : HMul.hMul (α := α) (↑p.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.num : α) (↑p.den : α)
⊢ p = q
have rw : HMul.hMul (α := ℚ≥0) (↑p.num : ℚ≥0) (↑q.den : ℚ≥0) = HMul.hMul (α := ℚ≥0) (↑q.num : ℚ≥0) (↑p.den : ℚ≥0)
Tactic: rw [← p.num_div_den, ← q.num_div_den, div_eq_div_iff]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.CharZero (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
hpq : HMul.hMul (α := α) (↑p.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.num : α) (↑p.den : α)
rw : HMul.hMul (α := ℚ≥0) (↑p.num : ℚ≥0) (↑q.den : ℚ≥0) = HMul.hMul (α := ℚ≥0) (↑q.num : ℚ≥0) (↑p.den : ℚ≥0)
⊢ p = q
have hb : Ne (α := ℚ≥0) (↑p.den : ℚ≥0) 0
Tactic: rw [← p.num_div_den, ← q.num_div_den, div_eq_div_iff]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.CharZero (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
hpq : HMul.hMul (α := α) (↑p.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.num : α) (↑p.den : α)
rw : HMul.hMul (α := ℚ≥0) (↑p.num : ℚ≥0) (↑q.den : ℚ≥0) = HMul.hMul (α := ℚ≥0) (↑q.num : ℚ≥0) (↑p.den : ℚ≥0)
hb : Ne (α := ℚ≥0) (↑p.den : ℚ≥0) 0
⊢ p = q
have hd : Ne (α := ℚ≥0) (↑q.den : ℚ≥0) 0
Tactic: rw [← p.num_div_den, ← q.num_div_den, div_eq_div_iff]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.CharZero (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
hpq : HMul.hMul (α := α) (↑p.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.num : α) (↑p.den : α)
⊢ p = q
have on_goal : HMul.hMul (α := ℚ≥0) (↑p.num : ℚ≥0) (↑q.den : ℚ≥0) = HMul.hMul (α := ℚ≥0) (↑q.num : ℚ≥0) (↑p.den : ℚ≥0)
Tactic: on_goal 1 => rw [← p.num_div_den, ← q.num_div_den, div_eq_div_iff]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.CharZero (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
hpq : HMul.hMul (α := α) (↑p.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.num : α) (↑p.den : α)
on_goal : HMul.hMul (α := ℚ≥0) (↑p.num : ℚ≥0) (↑q.den : ℚ≥0) = HMul.hMul (α := ℚ≥0) (↑q.num : ℚ≥0) (↑p.den : ℚ≥0)
⊢ p = q
have hb : Ne (α := ℚ≥0) (↑p.den : ℚ≥0) 0
Tactic: on_goal 1 => rw [← p.num_div_den, ← q.num_div_den, div_eq_div_iff]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.CharZero (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
hpq : HMul.hMul (α := α) (↑p.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.num : α) (↑p.den : α)
on_goal : HMul.hMul (α := ℚ≥0) (↑p.num : ℚ≥0) (↑q.den : ℚ≥0) = HMul.hMul (α := ℚ≥0) (↑q.num : ℚ≥0) (↑p.den : ℚ≥0)
hb : Ne (α := ℚ≥0) (↑p.den : ℚ≥0) 0
⊢ p = q
have hd : Ne (α := ℚ≥0) (↑q.den : ℚ≥0) 0
Tactic: on_goal 1 => rw [← p.num_div_den, ← q.num_div_den, div_eq_div_iff]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.CharZero (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
hpq : HMul.hMul (α := α) (↑p.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.num : α) (↑p.den : α)
⊢ HMul.hMul (α := ℚ≥0) (↑p.num : ℚ≥0) (↑q.den : ℚ≥0) = HMul.hMul (α := ℚ≥0) (↑q.num : ℚ≥0) (↑p.den : ℚ≥0)
have norm_cast : ∀ (hpq : p.num * q.den = q.num * p.den), p.num * q.den = q.num * p.den
Tactic: norm_cast at hpq ⊢
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.CharZero (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
hpq : HMul.hMul (α := α) (↑p.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.num : α) (↑p.den : α)
⊢ Ne (α := ℚ≥0) (↑p.den : ℚ≥0) 0
have hb : ¬p.den = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.CharZero (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
hpq : HMul.hMul (α := α) (↑p.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.num : α) (↑p.den : α)
⊢ Ne (α := ℚ≥0) (↑q.den : ℚ≥0) 0
have hd : ¬q.den = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.CharZero (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
hpq : HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) = HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)
⊢ Ne.{u_3 + 1} (α := α) (↑p.den : α) 0
have hb : ¬p.den = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.CharZero (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
hpq : HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) = HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)
⊢ Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
have hd : ¬q.den = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.CharZero (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
q : ℚ≥0
⊢ Eq.{u_3 + 1} (α := α) (↑q : α) 0 ↔ q = 0
have rw : Eq.{u_3 + 1} (α := α) (↑q : α) (↑0 : α) ↔ q = 0
Tactic: rw [← cast_zero, cast_inj]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.CharZero (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
q : ℚ≥0
rw : Eq.{u_3 + 1} (α := α) (↑q : α) (↑0 : α) ↔ q = 0
⊢ Eq.{u_3 + 1} (α := α) (↑q : α) 0 ↔ q = 0
have rw₁ : q = 0 ↔ q = 0
Tactic: rw [← cast_zero, cast_inj]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.CharZero (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
a b : ℕ
⊢ (↑(divNat a b) : α) = HDiv.hDiv (α := α) (↑a : α) (↑b : α)
have rw : Eq.{u_3 + 1} (α := α) (↑(divNat a b) : α) (↑(HDiv.hDiv (α := ℚ≥0) (↑a : ℚ≥0) (↑b : ℚ≥0)) : α)
Tactic: rw [← cast_natCast, ← cast_natCast b, ← cast_div]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.CharZero (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
a b : ℕ
⊢ Eq.{u_3 + 1} (α := α) (↑(divNat a b) : α) (↑(HDiv.hDiv (α := ℚ≥0) (↑a : ℚ≥0) (↑b : ℚ≥0)) : α)
have e_a : divNat a b = HDiv.hDiv (α := ℚ≥0) (↑a : ℚ≥0) (↑b : ℚ≥0)
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.CharZero (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
a b : ℕ
⊢ divNat a b = HDiv.hDiv (α := ℚ≥0) (↑a : ℚ≥0) (↑b : ℚ≥0)
have e_a : Eq (α := ℚ) (↑(divNat a b) : ℚ) (↑(HDiv.hDiv (α := ℚ≥0) (↑a : ℚ≥0) (↑b : ℚ≥0)) : ℚ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
⊢ (↑(divNat a b) : α) = HDiv.hDiv (α := α) (↑a : α) (↑b : α)
have rcases : ∀ (n : ℤ) (d : ℕ) (h : d ≠ 0) (c : n.natAbs.Coprime d) (hn : 0 ≤ { num := n, den := d, den_nz := h, reduced := c : ℚ })
  (e : divNat a b = Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := n, den := d, den_nz := h, reduced := c } hn),
  (↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := n, den := d, den_nz := h, reduced := c } hn) : α) =
    HDiv.hDiv (α := α) (↑a : α) (↑b : α)
Tactic: rcases e : divNat a b with ⟨⟨n, d, h, c⟩, hn⟩
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (hypothesis)
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
hn : 0 ≤ { num := n, den := d, den_nz := h, reduced := c : ℚ }
e : divNat a b = Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := n, den := d, den_nz := h, reduced := c } hn
⊢ (↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := n, den := d, den_nz := h, reduced := c } hn) : α) =
    HDiv.hDiv (α := α) (↑a : α) (↑b : α)
have hn₁ : 0 ≤ { num := n, den := d, den_nz := h, reduced := c : ℚ }.num
Tactic: rw [← Rat.num_nonneg] at hn
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
hn_1 : 0 ≤ { num := n, den := d, den_nz := h, reduced := c : ℚ }
hn : 0 ≤ { num := n, den := d, den_nz := h, reduced := c : ℚ }.num
e : divNat a b = Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := n, den := d, den_nz := h, reduced := c } hn_1
⊢ (↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := n, den := d, den_nz := h, reduced := c } hn_1) : α) =
    HDiv.hDiv (α := α) (↑a : α) (↑b : α)
have lift : ∀ (n : ℕ) (c : (Int.natAbs (↑n : ℤ)).Coprime d) (hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ })
  (e : divNat a b = Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn),
  (↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn) : α) =
    HDiv.hDiv (α := α) (↑a : α) (↑b : α)
Tactic: lift n to ℕ using hn
Cleared hypotheses: n, c, hn_1, hn, e
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (Int.natAbs (↑n : ℤ)).Coprime d
hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ }
e : divNat a b = Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn
⊢ Ne.{u_3 + 1} (α := α) (↑d : α) 0
have refine : ∀ (hd : Eq.{u_3 + 1} (α := α) (↑d : α) 0), Eq.{u_3 + 1} (α := α) (↑b : α) 0
Tactic: refine fun hd ↦ hb ?_
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (hypothesis)
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (Int.natAbs (↑n : ℤ)).Coprime d
hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ }
e : divNat a b = Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn
hd : Eq.{u_3 + 1} (α := α) (↑d : α) 0
⊢ Eq.{u_3 + 1} (α := α) (↑b : α) 0
have this : Rat.divInt (↑a : ℤ) (↑b : ℤ) =
  (↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn) : ℚ)
Tactic: have : Rat.divInt a b = _ := congr_arg NNRat.cast e
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (Int.natAbs (↑n : ℤ)).Coprime d
hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ }
e : divNat a b = Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn
hd : Eq.{u_3 + 1} (α := α) (↑d : α) 0
this :
  Rat.divInt (↑a : ℤ) (↑b : ℤ) =
    (↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn) : ℚ)
⊢ Eq.{u_3 + 1} (α := α) (↑b : α) 0
have obtain : ∀ (k : ℕ) (hb : Ne.{u_3 + 1} (α := α) (↑(d * k) : α) 0)
  (e :
    divNat a (d * k) =
      Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn)
  (this :
    Rat.divInt (↑a : ℤ) (↑(d * k) : ℤ) =
      (↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn) : ℚ)),
  Eq.{u_3 + 1} (α := α) (↑(d * k) : α) 0
Tactic: obtain ⟨k, rfl⟩ : d ∣ b := by simpa [Int.natCast_dvd_natCast, this] using Rat.den_dvd a b
Cleared hypotheses: b, hb, e, this
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (hypothesis)
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (Int.natAbs (↑n : ℤ)).Coprime d
hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ }
e : divNat a b = Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn
⊢ (↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn) : α) =
    HDiv.hDiv (α := α) (↑a : α) (↑b : α)
have hd : Ne.{u_3 + 1} (α := α) (↑d : α) 0
Tactic: have hd : (d : α) ≠ 0 := by
    refine fun hd ↦ hb ?_
    have : Rat.divInt a b = _ := congr_arg NNRat.cast e
    obtain ⟨k, rfl⟩ : d ∣ b := by simpa [Int.natCast_dvd_natCast, this] using Rat.den_dvd a b
    simp [*]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (hypothesis)
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (Int.natAbs (↑n : ℤ)).Coprime d
hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ }
e : divNat a b = Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn
hd : Ne.{u_3 + 1} (α := α) (↑d : α) 0
⊢ (↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn) : α) =
    HDiv.hDiv (α := α) (↑a : α) (↑b : α)
have hb' : b ≠ 0
Tactic: have hb' : b ≠ 0 := by rintro rfl; exact hb Nat.cast_zero
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (hypothesis)
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (Int.natAbs (↑n : ℤ)).Coprime d
hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ }
e : divNat a b = Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn
hd : Ne.{u_3 + 1} (α := α) (↑d : α) 0
hb' : b ≠ 0
⊢ (↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn) : α) =
    HDiv.hDiv (α := α) (↑a : α) (↑b : α)
have e₁ : a * d = n * b
Tactic: simp_rw [Rat.mk_eq_divInt, mk_divInt, divNat_inj hb' h] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (Int.natAbs (↑n : ℤ)).Coprime d
hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ }
hd : Ne.{u_3 + 1} (α := α) (↑d : α) 0
hb' : b ≠ 0
e : a * d = n * b
⊢ (↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn) : α) =
    HDiv.hDiv (α := α) (↑a : α) (↑b : α)
have rw : HDiv.hDiv (α := α)
    (↑(num (Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ } hn)) : α)
    (↑(den (Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ } hn)) :
      α) =
  HDiv.hDiv (α := α) (↑a : α) (↑b : α)
Tactic: rw [cast_def]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (Int.natAbs (↑n : ℤ)).Coprime d
hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ }
hd : Ne.{u_3 + 1} (α := α) (↑d : α) 0
hb' : b ≠ 0
e : a * d = n * b
⊢ HDiv.hDiv (α := α)
      (↑(num (Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ } hn)) :
        α)
      (↑(den (Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ } hn)) :
        α) =
    HDiv.hDiv (α := α) (↑a : α) (↑b : α)
have dsimp : HDiv.hDiv (α := α) (↑n : α) (↑d : α) = HDiv.hDiv (α := α) (↑a : α) (↑b : α)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (Int.natAbs (↑n : ℤ)).Coprime d
hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ }
hd : Ne.{u_3 + 1} (α := α) (↑d : α) 0
hb' : b ≠ 0
e : a * d = n * b
⊢ HDiv.hDiv (α := α) (↑n : α) (↑d : α) = HDiv.hDiv (α := α) (↑a : α) (↑b : α)
have rw : HMul.hMul (α := α) (↑n : α) (↑b : α) = HMul.hMul (α := α) (↑a : α) (↑d : α)
Tactic: rw [Commute.div_eq_div_iff _ hd hb]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (Int.natAbs (↑n : ℤ)).Coprime d
hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ }
hd : Ne.{u_3 + 1} (α := α) (↑d : α) 0
hb' : b ≠ 0
e : a * d = n * b
rw : HMul.hMul (α := α) (↑n : α) (↑b : α) = HMul.hMul (α := α) (↑a : α) (↑d : α)
⊢ HDiv.hDiv (α := α) (↑n : α) (↑d : α) = HDiv.hDiv (α := α) (↑a : α) (↑b : α)
have rw₁ : Commute.{u_3} (S := α) (↑d : α) (↑b : α)
Tactic: rw [Commute.div_eq_div_iff _ hd hb]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (Int.natAbs (↑n : ℤ)).Coprime d
hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ }
hd : Ne.{u_3 + 1} (α := α) (↑d : α) 0
hb' : b ≠ 0
e : a * d = n * b
⊢ HMul.hMul (α := α) (↑n : α) (↑b : α) = HMul.hMul (α := α) (↑a : α) (↑d : α)
have norm_cast : Eq.{u_3 + 1} (α := α) (↑(n * b) : α) (↑(a * d) : α)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (Int.natAbs (↑n : ℤ)).Coprime d
hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ }
hd : Ne.{u_3 + 1} (α := α) (↑d : α) 0
hb' : b ≠ 0
e : a * d = n * b
⊢ Eq.{u_3 + 1} (α := α) (↑(n * b) : α) (↑(a * d) : α)
have rw : Eq.{u_3 + 1} (α := α) (↑(n * b) : α) (↑(n * b) : α)
Tactic: rw [e]
-- 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) : α) = 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_divNat_of_ne_zero, cast_def, cast_def, mul_comm _ q.den,
    (Nat.commute_cast _ _).div_add_div (Nat.commute_cast _ _) hq hr]
-- 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.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_divNat_of_ne_zero, cast_def, cast_def, mul_comm _ q.den,
    (Nat.commute_cast _ _).div_add_div (Nat.commute_cast _ _) hq hr]
-- 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.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 : DivisionSemiring α
q r : ℚ≥0
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