awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
pos : ∀ (h : gcd x y = 0), gcd x y * (x * y / gcd x y) = x * y
⊢ gcd x y * (x * y / gcd x y) = x * y
have neg : ∀ (h : ¬gcd x y = 0), gcd x y * (x * y / gcd x y) = x * y
Tactic: by_cases h : gcd x y = 0
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
h : gcd x y = 0
⊢ gcd x y * (x * y / gcd x y) = x * y
have pos : 0 = x * y
Tactic: rw [h, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (hypothesis)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
h : gcd x y = 0
⊢ 0 = x * y
have h₁ : x = 0 ∧ y = 0
Tactic: rw [EuclideanDomain.gcd_eq_zero_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
h : x = 0 ∧ y = 0
⊢ 0 = x * y
have pos : 0 = 0 * y
Tactic: rw [h.1, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
h : x = 0 ∧ y = 0
pos : 0 = 0 * y
⊢ 0 = x * y
have pos₁ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [h.1, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
h : ¬gcd x y = 0
⊢ gcd x y * (x * y / gcd x y) = x * y
have neg : ∀ (r : R) (hr : x = gcd x y * r) (s : R) (hs : y = gcd x y * s), gcd x y * (x * y / gcd x y) = x * y
Tactic: rcases gcd_dvd x y with ⟨⟨r, hr⟩, ⟨s, hs⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
h : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ gcd x y * (x * y / gcd x y) = x * y
have neg : ∀ (g : R) (h : ¬g = 0) (hr : x = g * r), g * (x * y / g) = x * y
Tactic: generalize gcd x y = g at h hr ⊢
Cleared hypotheses: h, hr
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y r s : R
hs : y = gcd x y * s
g : R
h : ¬g = 0
hr : x = g * r
⊢ g * (x * y / g) = x * y
have neg : ∀ (hs : y = gcd (g * r) y * s), g * (g * r * y / g) = g * r * y
Tactic: subst hr
Cleared hypotheses: x, hs, hr
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
y r s g : R
h : ¬g = 0
hs : y = gcd (g * r) y * s
⊢ g * (g * r * y / g) = g * r * y
have neg : g * (g * (r * y) / g) = g * (r * y)
Tactic: rw [mul_assoc, mul_div_cancel_left₀ _ h]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
y r s g : R
h : ¬g = 0
hs : y = gcd (g * r) y * s
neg : g * (g * (r * y) / g) = g * (r * y)
⊢ g * (g * r * y / g) = g * r * y
have neg₁ : g * (r * y) = g * (r * y)
Tactic: rw [mul_assoc, mul_div_cancel_left₀ _ h]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
⊢ a * b / (a * c) = b / c
have pos : ∀ (hc : c = 0), a * b / (a * c) = b / c
Tactic: by_cases hc : c = 0
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
pos : ∀ (hc : c = 0), a * b / (a * c) = b / c
⊢ a * b / (a * c) = b / c
have neg : ∀ (hc : ¬c = 0), a * b / (a * c) = b / c
Tactic: by_cases hc : c = 0
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : ¬c = 0
⊢ a * b / (a * c) = b / c
have neg : a * (c * (a * b / (a * c))) = a * b
Tactic: refine eq_div_of_mul_eq_right hc (mul_left_cancel₀ ha ?_)
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : ¬c = 0
⊢ a * (c * (a * b / (a * c))) = a * b
have neg : a * c * (a * b / (a * c)) = a * b
Tactic: rw [← mul_assoc, ← mul_div_assoc _ (by gcongr), mul_div_cancel_left₀ _ (mul_ne_zero ha hc)]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : ¬c = 0
neg : a * c * (a * b / (a * c)) = a * b
⊢ a * (c * (a * b / (a * c))) = a * b
have neg₁ : a * c * (a * b) / (a * c) = a * b
Tactic: rw [← mul_assoc, ← mul_div_assoc _ (by gcongr), mul_div_cancel_left₀ _ (mul_ne_zero ha hc)]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : ¬c = 0
neg : a * c * (a * b / (a * c)) = a * b
neg₁ : a * c * (a * b) / (a * c) = a * b
⊢ a * (c * (a * b / (a * c))) = a * b
have neg₂ : a * b = a * b
Tactic: rw [← mul_assoc, ← mul_div_assoc _ (by gcongr), mul_div_cancel_left₀ _ (mul_ne_zero ha hc)]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b c d : R
hac : c ∣ a
hbd : d ∣ b
⊢ a * b / (c * d) = a / c * (b / d)
have inl : ∀ (hac : 0 ∣ a), a * b / (0 * d) = a / 0 * (b / d)
Tactic: rcases eq_or_ne c 0 with (rfl | hc0)
Cleared hypotheses: c, hac
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b c d : R
hac : c ∣ a
hbd : d ∣ b
inl : ∀ (hac : 0 ∣ a), a * b / (0 * d) = a / 0 * (b / d)
⊢ a * b / (c * d) = a / c * (b / d)
have inr : ∀ (hc0 : c ≠ 0), a * b / (c * d) = a / c * (b / d)
Tactic: rcases eq_or_ne c 0 with (rfl | hc0)
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b c d : R
hac : c ∣ a
hbd : d ∣ b
hc0 : c ≠ 0
⊢ a * b / (c * d) = a / c * (b / d)
have inr : ∀ (hbd : 0 ∣ b), a * b / (c * 0) = a / c * (b / 0)
Tactic: rcases eq_or_ne d 0 with (rfl | hd0)
Cleared hypotheses: d, hbd
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b c d : R
hac : c ∣ a
hbd : d ∣ b
hc0 : c ≠ 0
inr : ∀ (hbd : 0 ∣ b), a * b / (c * 0) = a / c * (b / 0)
⊢ a * b / (c * d) = a / c * (b / d)
have inr₁ : ∀ (hd0 : d ≠ 0), a * b / (c * d) = a / c * (b / d)
Tactic: rcases eq_or_ne d 0 with (rfl | hd0)
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b c d : R
hac : c ∣ a
hbd : d ∣ b
hc0 : c ≠ 0
hd0 : d ≠ 0
⊢ a * b / (c * d) = a / c * (b / d)
have inr : ∀ (k1 : R), c * k1 * b / (c * d) = c * k1 / c * (b / d)
Tactic: obtain ⟨k1, rfl⟩ := hac
Cleared hypotheses: a, hac
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
b c d : R
hbd : d ∣ b
hc0 : c ≠ 0
hd0 : d ≠ 0
k1 : R
⊢ c * k1 * b / (c * d) = c * k1 / c * (b / d)
have inr : ∀ (k2 : R), c * k1 * (d * k2) / (c * d) = c * k1 / c * (d * k2 / d)
Tactic: obtain ⟨k2, rfl⟩ := hbd
Cleared hypotheses: b, hbd
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
c d : R
hc0 : c ≠ 0
hd0 : d ≠ 0
k1 k2 : R
⊢ c * k1 * (d * k2) / (c * d) = c * k1 / c * (d * k2 / d)
have inr : c * k1 * (d * k2) / (c * d) = k1 * (d * k2 / d)
Tactic: rw [mul_div_cancel_left₀ _ hc0, mul_div_cancel_left₀ _ hd0, mul_mul_mul_comm,
    mul_div_cancel_left₀ _ (mul_ne_zero hc0 hd0)]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
c d : R
hc0 : c ≠ 0
hd0 : d ≠ 0
k1 k2 : R
inr : c * k1 * (d * k2) / (c * d) = k1 * (d * k2 / d)
⊢ c * k1 * (d * k2) / (c * d) = c * k1 / c * (d * k2 / d)
have inr₁ : c * k1 * (d * k2) / (c * d) = k1 * k2
Tactic: rw [mul_div_cancel_left₀ _ hc0, mul_div_cancel_left₀ _ hd0, mul_mul_mul_comm,
    mul_div_cancel_left₀ _ (mul_ne_zero hc0 hd0)]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
c d : R
hc0 : c ≠ 0
hd0 : d ≠ 0
k1 k2 : R
inr : c * k1 * (d * k2) / (c * d) = k1 * (d * k2 / d)
inr₁ : c * k1 * (d * k2) / (c * d) = k1 * k2
⊢ c * k1 * (d * k2) / (c * d) = c * k1 / c * (d * k2 / d)
have inr₂ : c * d * (k1 * k2) / (c * d) = k1 * k2
Tactic: rw [mul_div_cancel_left₀ _ hc0, mul_div_cancel_left₀ _ hd0, mul_mul_mul_comm,
    mul_div_cancel_left₀ _ (mul_ne_zero hc0 hd0)]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
c d : R
hc0 : c ≠ 0
hd0 : d ≠ 0
k1 k2 : R
inr : c * k1 * (d * k2) / (c * d) = k1 * (d * k2 / d)
inr₁ : c * k1 * (d * k2) / (c * d) = k1 * k2
inr₂ : c * d * (k1 * k2) / (c * d) = k1 * k2
⊢ c * k1 * (d * k2) / (c * d) = c * k1 / c * (d * k2 / d)
have inr₃ : k1 * k2 = k1 * k2
Tactic: rw [mul_div_cancel_left₀ _ hc0, mul_div_cancel_left₀ _ hd0, mul_mul_mul_comm,
    mul_div_cancel_left₀ _ (mul_ne_zero hc0 hd0)]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
⊢ (x + y * z) / y = x / y + z
have rw : x / y + z = (x + y * z) / y
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
⊢ x / y + z = (x + y * z) / y
have apply : y * (x / y + z) = x + y * z
Tactic: apply eq_div_of_mul_eq_right h1
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
⊢ y * (x / y + z) = x + y * z
have rw : y * (x / y) + y * z = x + y * z
Tactic: rw [mul_add, EuclideanDomain.mul_div_cancel' h1 h2]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
rw : y * (x / y) + y * z = x + y * z
⊢ y * (x / y + z) = x + y * z
have rw₁ : x + y * z = x + y * z
Tactic: rw [mul_add, EuclideanDomain.mul_div_cancel' h1 h2]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
⊢ (x + z * y) / y = x / y + z
have rw : (x + y * z) / y = x / y + z
Tactic: rw [mul_comm z y]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
⊢ (x - y * z) / y = x / y - z
have rw : x / y - z = (x - y * z) / y
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
⊢ x / y - z = (x - y * z) / y
have apply : y * (x / y - z) = x - y * z
Tactic: apply eq_div_of_mul_eq_right h1
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
⊢ y * (x / y - z) = x - y * z
have rw : y * (x / y) - y * z = x - y * z
Tactic: rw [mul_sub, EuclideanDomain.mul_div_cancel' h1 h2]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
rw : y * (x / y) - y * z = x - y * z
⊢ y * (x / y - z) = x - y * z
have rw₁ : x - y * z = x - y * z
Tactic: rw [mul_sub, EuclideanDomain.mul_div_cancel' h1 h2]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
⊢ (x - z * y) / y = x / y - z
have rw : (x - y * z) / y = x / y - z
Tactic: rw [mul_comm z y]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ (z * x + y) / z = x + y / z
have rw : x + y / z = (z * x + y) / z
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ x + y / z = (z * x + y) / z
have apply : z * (x + y / z) = z * x + y
Tactic: apply eq_div_of_mul_eq_right h1
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ z * (x + y / z) = z * x + y
have rw : z * x + z * (y / z) = z * x + y
Tactic: rw [mul_add, EuclideanDomain.mul_div_cancel' h1 h2]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
rw : z * x + z * (y / z) = z * x + y
⊢ z * (x + y / z) = z * x + y
have rw₁ : z * x + y = z * x + y
Tactic: rw [mul_add, EuclideanDomain.mul_div_cancel' h1 h2]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ (x * z + y) / z = x + y / z
have rw : (z * x + y) / z = x + y / z
Tactic: rw [mul_comm x z]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ (z * x - y) / z = x - y / z
have rw : x - y / z = (z * x - y) / z
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ x - y / z = (z * x - y) / z
have apply : z * (x - y / z) = z * x - y
Tactic: apply eq_div_of_mul_eq_right h1
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ z * (x - y / z) = z * x - y
have rw : z * x - z * (y / z) = z * x - y
Tactic: rw [mul_sub, EuclideanDomain.mul_div_cancel' h1 h2]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
rw : z * x - z * (y / z) = z * x - y
⊢ z * (x - y / z) = z * x - y
have rw₁ : z * x - y = z * x - y
Tactic: rw [mul_sub, EuclideanDomain.mul_div_cancel' h1 h2]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ (x * z - y) / z = x - y / z
have rw : (z * x - y) / z = x - y / z
Tactic: rw [mul_comm x z]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ∣ x
h2 : y * z ∣ x
⊢ x / (y * z) = x / y / z
have inl : ∀ (h2 : y * 0 ∣ x), x / (y * 0) = x / y / 0
Tactic: rcases eq_or_ne z 0 with rfl | hz
Cleared hypotheses: z, h2
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ∣ x
h2 : y * z ∣ x
inl : ∀ (h2 : y * 0 ∣ x), x / (y * 0) = x / y / 0
⊢ x / (y * z) = x / y / z
have inr : ∀ (hz : z ≠ 0), x / (y * z) = x / y / z
Tactic: rcases eq_or_ne z 0 with rfl | hz
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ∣ x
h2 : y * z ∣ x
hz : z ≠ 0
⊢ x / (y * z) = x / y / z
have inr : z * (x / (y * z)) = x / y
Tactic: apply eq_div_of_mul_eq_right hz
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ∣ x
h2 : y * z ∣ x
hz : z ≠ 0
⊢ z * (x / (y * z)) = x / y
have inr : z * x / (y * z) = x / y
Tactic: rw [← EuclideanDomain.mul_div_assoc z h2, mul_comm y z, mul_div_mul_cancel hz h1]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ∣ x
h2 : y * z ∣ x
hz : z ≠ 0
inr : z * x / (y * z) = x / y
⊢ z * (x / (y * z)) = x / y
have inr₁ : z * x / (z * y) = x / y
Tactic: rw [← EuclideanDomain.mul_div_assoc z h2, mul_comm y z, mul_div_mul_cancel hz h1]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ∣ x
h2 : y * z ∣ x
hz : z ≠ 0
inr : z * x / (y * z) = x / y
inr₁ : z * x / (z * y) = x / y
⊢ z * (x / (y * z)) = x / y
have inr₂ : x / y = x / y
Tactic: rw [← EuclideanDomain.mul_div_assoc z h2, mul_comm y z, mul_div_mul_cancel hz h1]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ∣ x
h2 : z ∣ x / y
⊢ x / y / z = x / (y * z)
have inl : ∀ (h1 : 0 ∣ x) (h2 : z ∣ x / 0), x / 0 / z = x / (0 * z)
Tactic: rcases eq_or_ne y 0 with rfl | hy
Cleared hypotheses: y, h1, h2
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ∣ x
h2 : z ∣ x / y
inl : ∀ (h1 : 0 ∣ x) (h2 : z ∣ x / 0), x / 0 / z = x / (0 * z)
⊢ x / y / z = x / (y * z)
have inr : ∀ (hy : y ≠ 0), x / y / z = x / (y * z)
Tactic: rcases eq_or_ne y 0 with rfl | hy
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (hypothesis)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ∣ x
h2 : z ∣ x / y
hy : y ≠ 0
⊢ x / y / z = x / (y * z)
have h2₁ : y * z ∣ x
Tactic: rw [← mul_dvd_mul_iff_left hy, EuclideanDomain.mul_div_cancel' hy h1] at h2
Cleared hypotheses: h2, hy
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
⊢ x / y + z / t = (t * x + y * z) / (t * y)
have apply : t * y * (x / y + z / t) = t * x + y * z
Tactic: apply eq_div_of_mul_eq_right (mul_ne_zero h2 h1)
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
⊢ t * y * (x / y + z / t) = t * x + y * z
have rw : t * y * (x / y) + t * y * (z / t) = t * x + y * z
Tactic: rw [mul_add, mul_assoc, EuclideanDomain.mul_div_cancel' h1 h3, mul_comm t y,
    mul_assoc, EuclideanDomain.mul_div_cancel' h2 h4]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
rw : t * y * (x / y) + t * y * (z / t) = t * x + y * z
⊢ t * y * (x / y + z / t) = t * x + y * z
have rw₁ : t * (y * (x / y)) + t * y * (z / t) = t * x + y * z
Tactic: rw [mul_add, mul_assoc, EuclideanDomain.mul_div_cancel' h1 h3, mul_comm t y,
    mul_assoc, EuclideanDomain.mul_div_cancel' h2 h4]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
rw : t * y * (x / y) + t * y * (z / t) = t * x + y * z
rw₁ : t * (y * (x / y)) + t * y * (z / t) = t * x + y * z
⊢ t * y * (x / y + z / t) = t * x + y * z
have rw₂ : t * x + t * y * (z / t) = t * x + y * z
Tactic: rw [mul_add, mul_assoc, EuclideanDomain.mul_div_cancel' h1 h3, mul_comm t y,
    mul_assoc, EuclideanDomain.mul_div_cancel' h2 h4]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
rw : t * y * (x / y) + t * y * (z / t) = t * x + y * z
rw₁ : t * (y * (x / y)) + t * y * (z / t) = t * x + y * z
rw₂ : t * x + t * y * (z / t) = t * x + y * z
⊢ t * y * (x / y + z / t) = t * x + y * z
have rw₃ : t * x + y * t * (z / t) = t * x + y * z
Tactic: rw [mul_add, mul_assoc, EuclideanDomain.mul_div_cancel' h1 h3, mul_comm t y,
    mul_assoc, EuclideanDomain.mul_div_cancel' h2 h4]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
rw : t * y * (x / y) + t * y * (z / t) = t * x + y * z
rw₁ : t * (y * (x / y)) + t * y * (z / t) = t * x + y * z
rw₂ : t * x + t * y * (z / t) = t * x + y * z
rw₃ : t * x + y * t * (z / t) = t * x + y * z
⊢ t * y * (x / y + z / t) = t * x + y * z
have rw₄ : t * x + y * (t * (z / t)) = t * x + y * z
Tactic: rw [mul_add, mul_assoc, EuclideanDomain.mul_div_cancel' h1 h3, mul_comm t y,
    mul_assoc, EuclideanDomain.mul_div_cancel' h2 h4]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
rw : t * y * (x / y) + t * y * (z / t) = t * x + y * z
rw₁ : t * (y * (x / y)) + t * y * (z / t) = t * x + y * z
rw₂ : t * x + t * y * (z / t) = t * x + y * z
rw₃ : t * x + y * t * (z / t) = t * x + y * z
rw₄ : t * x + y * (t * (z / t)) = t * x + y * z
⊢ t * y * (x / y + z / t) = t * x + y * z
have rw₅ : t * x + y * z = t * x + y * z
Tactic: rw [mul_add, mul_assoc, EuclideanDomain.mul_div_cancel' h1 h3, mul_comm t y,
    mul_assoc, EuclideanDomain.mul_div_cancel' h2 h4]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
⊢ x / y - z / t = (t * x - y * z) / (t * y)
have apply : t * y * (x / y - z / t) = t * x - y * z
Tactic: apply eq_div_of_mul_eq_right (mul_ne_zero h2 h1)
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
⊢ t * y * (x / y - z / t) = t * x - y * z
have rw : t * y * (x / y) - t * y * (z / t) = t * x - y * z
Tactic: rw [mul_sub, mul_assoc, EuclideanDomain.mul_div_cancel' h1 h3, mul_comm t y,
    mul_assoc, EuclideanDomain.mul_div_cancel' h2 h4]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
rw : t * y * (x / y) - t * y * (z / t) = t * x - y * z
⊢ t * y * (x / y - z / t) = t * x - y * z
have rw₁ : t * (y * (x / y)) - t * y * (z / t) = t * x - y * z
Tactic: rw [mul_sub, mul_assoc, EuclideanDomain.mul_div_cancel' h1 h3, mul_comm t y,
    mul_assoc, EuclideanDomain.mul_div_cancel' h2 h4]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
rw : t * y * (x / y) - t * y * (z / t) = t * x - y * z
rw₁ : t * (y * (x / y)) - t * y * (z / t) = t * x - y * z
⊢ t * y * (x / y - z / t) = t * x - y * z
have rw₂ : t * x - t * y * (z / t) = t * x - y * z
Tactic: rw [mul_sub, mul_assoc, EuclideanDomain.mul_div_cancel' h1 h3, mul_comm t y,
    mul_assoc, EuclideanDomain.mul_div_cancel' h2 h4]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
rw : t * y * (x / y) - t * y * (z / t) = t * x - y * z
rw₁ : t * (y * (x / y)) - t * y * (z / t) = t * x - y * z
rw₂ : t * x - t * y * (z / t) = t * x - y * z
⊢ t * y * (x / y - z / t) = t * x - y * z
have rw₃ : t * x - y * t * (z / t) = t * x - y * z
Tactic: rw [mul_sub, mul_assoc, EuclideanDomain.mul_div_cancel' h1 h3, mul_comm t y,
    mul_assoc, EuclideanDomain.mul_div_cancel' h2 h4]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
rw : t * y * (x / y) - t * y * (z / t) = t * x - y * z
rw₁ : t * (y * (x / y)) - t * y * (z / t) = t * x - y * z
rw₂ : t * x - t * y * (z / t) = t * x - y * z
rw₃ : t * x - y * t * (z / t) = t * x - y * z
⊢ t * y * (x / y - z / t) = t * x - y * z
have rw₄ : t * x - y * (t * (z / t)) = t * x - y * z
Tactic: rw [mul_sub, mul_assoc, EuclideanDomain.mul_div_cancel' h1 h3, mul_comm t y,
    mul_assoc, EuclideanDomain.mul_div_cancel' h2 h4]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
rw : t * y * (x / y) - t * y * (z / t) = t * x - y * z
rw₁ : t * (y * (x / y)) - t * y * (z / t) = t * x - y * z
rw₂ : t * x - t * y * (z / t) = t * x - y * z
rw₃ : t * x - y * t * (z / t) = t * x - y * z
rw₄ : t * x - y * (t * (z / t)) = t * x - y * z
⊢ t * y * (x / y - z / t) = t * x - y * z
have rw₅ : t * x - y * z = t * x - y * z
Tactic: rw [mul_sub, mul_assoc, EuclideanDomain.mul_div_cancel' h1 h3, mul_comm t y,
    mul_assoc, EuclideanDomain.mul_div_cancel' h2 h4]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
⊢ x / y = z ↔ x = y * z
have obtain : ∀ (a : R) (ha : x = y * a), x / y = z ↔ x = y * z
Tactic: obtain ⟨a, ha⟩ := h2
Cleared hypotheses: h2