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₂ : ℤ)
⊢ n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
have rwa₁ : ∀ (h : HMul.hMul (α := α) (↑n₁ : α) (↑d₁ : α)⁻¹ * (↑d₂ : α) = (↑n₂ : α)), 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 : 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₂ : ℤ)
⊢ n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
have rwa₂ : ∀ (h : (↑n₁ : α) * HMul.hMul (α := α) (↑d₁ : α)⁻¹ (↑d₂ : α) = (↑n₂ : α)), 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 : 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₂ : ℤ)
⊢ n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
have rwa₃ : ∀ (h : (↑n₁ : α) * HMul.hMul (α := α) (↑d₂ : α) (↑d₁ : α)⁻¹ = (↑n₂ : α)), 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 : 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₂ : ℤ)
⊢ n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
have rwa₄ : ∀ (h : HMul.hMul (α := α) (↑n₁ : α) (↑d₂ : α) * (↑d₁ : α)⁻¹ = (↑n₂ : α)), 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 : 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₂ : ℤ)
⊢ n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
have rwa₅ : ∀ (h : HMul.hMul (α := α) (↑n₁ : α) (↑d₂ : α) / (↑d₁ : α) = (↑n₂ : α)), 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 : 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₂ : ℤ)
⊢ n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
have rwa₆ : ∀ (h : (↑n₂ : α) = HMul.hMul (α := α) (↑n₁ : α) (↑d₂ : α) / (↑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 : 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₂ : ℤ)
⊢ n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
have rwa₇ : ∀ (h : HMul.hMul (α := α) (↑n₂ : α) (↑d₁ : α) = HMul.hMul (α := α) (↑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 : 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₂ : ℤ)
⊢ n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
have rwa₈ : ∀ (h : HMul.hMul (α := α) (↑n₁ : α) (↑d₂ : α) = HMul.hMul (α := α) (↑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 : 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₂ : ℤ)
⊢ n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
have rwa₉ : ∀ (h : HMul.hMul (α := α) (↑n₁ : α) (↑d₂ : α) = HMul.hMul (α := α) (↑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 : 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₂ : ℤ)
⊢ n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
have rwa₁₀ : ∀ (h : HMul.hMul (α := α) (↑n₁ : α) (↑d₂ : α) = (↑(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 : 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₂ : ℤ)
⊢ n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
have rwa₁₁ : ∀ (h : HMul.hMul (α := α) (↑n₁ : α) (↑(↑d₂ : ℤ) : α) = (↑(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 : 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₂ : ℤ)
⊢ n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
have rwa₁₂ : ∀ (h : Eq.{u_3 + 1} (α := α) (↑(n₁ * (↑d₂ : ℤ)) : α) (↑(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 : 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₂ : ℤ)
⊢ n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
have rwa₁₃ : ∀ (h : n₁ * (↑d₂ : ℤ) = 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