awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
rw : gcd x y * (x * y / gcd x y) = x * y
⊢ gcd x y * lcm x y = x * y

Tactic:
rw [lcm]

Premises used: EuclideanDomain.lcm
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
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
neg : ∀ (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

Tactic:
by_cases h : gcd x y = 0

Premises used: EuclideanDomain.gcd
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
h : gcd x y = 0
pos : 0 = x * y
⊢ gcd x y * (x * y / gcd x y) = x * y

Tactic:
rw [h, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
h : gcd x y = 0
⊢ x = 0 ∧ y = 0

Tactic:
rw [EuclideanDomain.gcd_eq_zero_iff] at h

Premises used: EuclideanDomain.gcd_eq_zero_iff
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
h : x = 0 ∧ y = 0
pos : 0 = 0 * y
pos₁ pos₂ : Eq.{u + 1} (α := R) 0 0
⊢ 0 = x * y

Tactic:
rw [h.1, zero_mul]

Premises used: MulZeroClass.zero_mul, And.left
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
h : ¬gcd x y = 0
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
⊢ gcd x y * (x * y / gcd x y) = x * y

Tactic:
rcases gcd_dvd x y with ⟨⟨r, hr⟩, ⟨s, hs⟩⟩

Premises used: EuclideanDomain.gcd_dvd
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
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
neg : ∀ (g : R) (h : ¬g = 0) (hr : x = g * r), g * (x * y / g) = x * y
⊢ gcd x y * (x * y / gcd x y) = x * y

Tactic:
generalize gcd x y = g at h hr ⊢

Premises used: EuclideanDomain.gcd
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
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
neg : ∀ (hs : y = gcd (g * r) y * s), g * (g * r * y / g) = g * r * y
⊢ g * (x * y / g) = x * y

Tactic:
subst hr
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
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)
neg₁ neg₂ : g * (r * y) = g * (r * y)
⊢ g * (g * r * y / g) = g * r * y

Tactic:
rw [mul_assoc, mul_div_cancel_left₀ _ h]

Premises used: mul_assoc, mul_div_cancel_left₀
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
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
neg : ∀ (hc : ¬c = 0), a * b / (a * c) = b / c
⊢ a * b / (a * c) = b / c

Tactic:
by_cases hc : c = 0
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
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

Tactic:
simp [hc]
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
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

Tactic:
eq_div_of_mul_eq_right hc (mul_left_cancel₀ ha ?_)

Premises used: mul_left_cancel₀, EuclideanDomain.eq_div_of_mul_eq_right
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
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 * b / (a * c) = b / c

Tactic:
refine eq_div_of_mul_eq_right hc (mul_left_cancel₀ ha ?_)

Premises used: mul_left_cancel₀, EuclideanDomain.eq_div_of_mul_eq_right
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : ¬c = 0
⊢ a * c ∣ a * b

Tactic:
gcongr
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
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
neg₂ neg₃ : a * b = a * b
⊢ 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)]

Premises used: mul_assoc, mul_div_cancel_left₀, EuclideanDomain.mul_div_assoc, mul_ne_zero
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
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)
inr : ∀ (hc0 : c ≠ 0), a * b / (c * d) = a / c * (b / d)
⊢ a * b / (c * d) = a / c * (b / d)

Tactic:
rcases eq_or_ne c 0 with (rfl | hc0)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a b d : R
hbd : d ∣ b
hac : 0 ∣ a
⊢ a * b / (0 * d) = a / 0 * (b / d)

Tactic:
simp
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
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)
inr₁ : ∀ (hd0 : d ≠ 0), a * b / (c * d) = a / c * (b / d)
⊢ a * b / (c * d) = a / c * (b / d)

Tactic:
rcases eq_or_ne d 0 with (rfl | hd0)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a b c : R
hac : c ∣ a
hc0 : c ≠ 0
hbd : 0 ∣ b
⊢ a * b / (c * 0) = a / c * (b / 0)

Tactic:
simp
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
a b c d : R
hac : c ∣ a
hbd : d ∣ b
hc0 : c ≠ 0
hd0 : d ≠ 0
inr : ∀ (k1 : R), c * k1 * b / (c * d) = c * k1 / c * (b / d)
⊢ a * b / (c * d) = a / c * (b / d)

Tactic:
obtain ⟨k1, rfl⟩ := hac

Premises used: rfl
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
b c d : R
hbd : d ∣ b
hc0 : c ≠ 0
hd0 : d ≠ 0
k1 : R
inr : ∀ (k2 : R), c * k1 * (d * k2) / (c * d) = c * k1 / c * (d * k2 / d)
⊢ c * k1 * b / (c * d) = c * k1 / c * (b / d)

Tactic:
obtain ⟨k2, rfl⟩ := hbd

Premises used: rfl
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
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
inr₃ inr₄ : k1 * k2 = k1 * k2
⊢ c * k1 * (d * k2) / (c * d) = c * k1 / c * (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)]

Premises used: mul_mul_mul_comm, mul_div_cancel_left₀, mul_ne_zero
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
rw : x / y + z = (x + y * z) / y
⊢ (x + y * z) / y = x / y + z

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
apply : y * (x / y + z) = x + y * z
⊢ x / y + z = (x + y * z) / y

Tactic:
apply eq_div_of_mul_eq_right h1

Premises used: EuclideanDomain.eq_div_of_mul_eq_right
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
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
rw₁ rw₂ : x + y * z = x + y * z
⊢ y * (x / y + z) = x + y * z

Tactic:
rw [mul_add, EuclideanDomain.mul_div_cancel' h1 h2]

Premises used: mul_add, EuclideanDomain.mul_div_cancel'
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
rw : (x + y * z) / y = x / y + z
⊢ (x + z * y) / y = x / y + z

Tactic:
rw [mul_comm z y]

Premises used: mul_comm
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
⊢ (x + y * z) / y = x / y + z

Tactic:
add_mul_div_left _ _ _ h1 h2

Premises used: EuclideanDomain.add_mul_div_left
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
⊢ (x + y * z) / y = x / y + z

Tactic:
exact add_mul_div_left _ _ _ h1 h2

Premises used: EuclideanDomain.add_mul_div_left
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
rw : x / y - z = (x - y * z) / y
⊢ (x - y * z) / y = x / y - z

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
apply : y * (x / y - z) = x - y * z
⊢ x / y - z = (x - y * z) / y

Tactic:
apply eq_div_of_mul_eq_right h1

Premises used: EuclideanDomain.eq_div_of_mul_eq_right
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
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
rw₁ rw₂ : x - y * z = x - y * z
⊢ y * (x / y - z) = x - y * z

Tactic:
rw [mul_sub, EuclideanDomain.mul_div_cancel' h1 h2]

Premises used: mul_sub, EuclideanDomain.mul_div_cancel'
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
rw : (x - y * z) / y = x / y - z
⊢ (x - z * y) / y = x / y - z

Tactic:
rw [mul_comm z y]

Premises used: mul_comm
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
⊢ (x - y * z) / y = x / y - z

Tactic:
sub_mul_div_left _ _ _ h1 h2

Premises used: EuclideanDomain.sub_mul_div_left
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
⊢ (x - y * z) / y = x / y - z

Tactic:
exact sub_mul_div_left _ _ _ h1 h2

Premises used: EuclideanDomain.sub_mul_div_left
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
rw : x + y / z = (z * x + y) / z
⊢ (z * x + y) / z = x + y / z

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
apply : z * (x + y / z) = z * x + y
⊢ x + y / z = (z * x + y) / z

Tactic:
apply eq_div_of_mul_eq_right h1

Premises used: EuclideanDomain.eq_div_of_mul_eq_right
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
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
rw₁ rw₂ : z * x + y = z * x + y
⊢ z * (x + y / z) = z * x + y

Tactic:
rw [mul_add, EuclideanDomain.mul_div_cancel' h1 h2]

Premises used: mul_add, EuclideanDomain.mul_div_cancel'
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
rw : (z * x + y) / z = x + y / z
⊢ (x * z + y) / z = x + y / z

Tactic:
rw [mul_comm x z]

Premises used: mul_comm
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ (z * x + y) / z = x + y / z

Tactic:
mul_add_div_left _ _ _ h1 h2

Premises used: EuclideanDomain.mul_add_div_left
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ (z * x + y) / z = x + y / z

Tactic:
exact mul_add_div_left _ _ _ h1 h2

Premises used: EuclideanDomain.mul_add_div_left
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
rw : x - y / z = (z * x - y) / z
⊢ (z * x - y) / z = x - y / z

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
apply : z * (x - y / z) = z * x - y
⊢ x - y / z = (z * x - y) / z

Tactic:
apply eq_div_of_mul_eq_right h1

Premises used: EuclideanDomain.eq_div_of_mul_eq_right
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
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
rw₁ rw₂ : z * x - y = z * x - y
⊢ z * (x - y / z) = z * x - y

Tactic:
rw [mul_sub, EuclideanDomain.mul_div_cancel' h1 h2]

Premises used: mul_sub, EuclideanDomain.mul_div_cancel'
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
rw : (z * x - y) / z = x - y / z
⊢ (x * z - y) / z = x - y / z

Tactic:
rw [mul_comm x z]

Premises used: mul_comm
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ (z * x - y) / z = x - y / z

Tactic:
mul_sub_div_left _ _ _ h1 h2

Premises used: EuclideanDomain.mul_sub_div_left
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ (z * x - y) / z = x - y / z

Tactic:
exact mul_sub_div_left _ _ _ h1 h2

Premises used: EuclideanDomain.mul_sub_div_left
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
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
inr : ∀ (hz : z ≠ 0), x / (y * z) = x / y / z
⊢ x / (y * z) = x / y / z

Tactic:
rcases eq_or_ne z 0 with rfl | hz

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y : R
h1 : y ∣ x
h2 : y * 0 ∣ x
⊢ x / (y * 0) = x / y / 0

Tactic:
simp only [mul_zero, div_zero]

Premises used: EuclideanDomain.div_zero, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
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
⊢ x / (y * z) = x / y / z

Tactic:
apply eq_div_of_mul_eq_right hz

Premises used: EuclideanDomain.eq_div_of_mul_eq_right
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
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
inr₂ inr₃ : x / y = x / y
⊢ z * (x / (y * z)) = x / y

Tactic:
rw [← EuclideanDomain.mul_div_assoc z h2, mul_comm y z, mul_div_mul_cancel hz h1]

Premises used: EuclideanDomain.mul_div_mul_cancel, EuclideanDomain.mul_div_assoc, mul_comm
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
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)
inr : ∀ (hy : y ≠ 0), x / y / z = x / (y * z)
⊢ x / y / z = x / (y * z)

Tactic:
rcases eq_or_ne y 0 with rfl | hy

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x z : R
h1 : 0 ∣ x
h2 : z ∣ x / 0
⊢ x / 0 / z = x / (0 * z)

Tactic:
simp only [div_zero, zero_div, zero_mul]

Premises used: EuclideanDomain.zero_div, MulZeroClass.zero_mul, EuclideanDomain.div_zero
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ∣ x
h2 : z ∣ x / y
hy : y ≠ 0
⊢ y * z ∣ x

Tactic:
rw [← mul_dvd_mul_iff_left hy, EuclideanDomain.mul_div_cancel' hy h1] at h2

Premises used: mul_dvd_mul_iff_left, EuclideanDomain.mul_div_cancel'
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ∣ x
h2 : z ∣ x / y
hy : y ≠ 0
h2₁ : y * z ∣ x
⊢ y ≠ 0

Tactic:
rw [← mul_dvd_mul_iff_left hy, EuclideanDomain.mul_div_cancel' hy h1] at h2

Premises used: mul_dvd_mul_iff_left, EuclideanDomain.mul_div_cancel'
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ∣ x
h2 : y * z ∣ x
hy : y ≠ 0
⊢ x / y / z = x / (y * z)

Tactic:
(div_mul h1 h2).symm

Premises used: EuclideanDomain.div_mul, Eq.symm
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ∣ x
h2 : y * z ∣ x
hy : y ≠ 0
⊢ x / y / z = x / (y * z)

Tactic:
exact (div_mul h1 h2).symm

Premises used: EuclideanDomain.div_mul, Eq.symm
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
apply : t * y * (x / y + z / t) = t * x + y * z
⊢ x / y + z / t = (t * x + y * z) / (t * y)

Tactic:
apply eq_div_of_mul_eq_right (mul_ne_zero h2 h1)

Premises used: mul_ne_zero, EuclideanDomain.eq_div_of_mul_eq_right
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
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
rw₅ rw₆ : t * x + y * z = t * x + y * z
⊢ t * y * (x / 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]

Premises used: mul_assoc, mul_comm, mul_add, EuclideanDomain.mul_div_cancel'
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
apply : t * y * (x / y - z / t) = t * x - y * z
⊢ x / y - z / t = (t * x - y * z) / (t * y)

Tactic:
apply eq_div_of_mul_eq_right (mul_ne_zero h2 h1)

Premises used: mul_ne_zero, EuclideanDomain.eq_div_of_mul_eq_right
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
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
rw₅ rw₆ : t * x - y * z = t * x - y * z
⊢ t * y * (x / 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]

Premises used: mul_sub, mul_assoc, mul_comm, EuclideanDomain.mul_div_cancel'
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
obtain : ∀ (a : R) (ha : x = y * a), x / y = z ↔ x = y * z
⊢ x / y = z ↔ x = y * z

Tactic:
obtain ⟨a, ha⟩ := h2
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ≠ 0
a : R
ha : x = y * a
rw : a = z ↔ y * a = y * z
⊢ x / y = z ↔ x = y * z

Tactic:
rw [ha, mul_div_cancel_left₀ _ h1]

Premises used: mul_div_cancel_left₀
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ≠ 0
a : R
ha : x = y * a
⊢ a = z ↔ y * a = y * z

Tactic:
simp only [mul_eq_mul_left_iff, h1, or_false]

Premises used: mul_eq_mul_left_iff, or_false
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
rw : y / z = x ↔ z * x = y
rw₁ : y = z * x ↔ z * x = y
rw₂ rw₃ : z * x = y ↔ z * x = y
⊢ x = y / z ↔ z * x = y

Tactic:
rw [eq_comm, div_eq_iff_eq_mul_of_dvd _ _ _ h1 h2, eq_comm]

Premises used: EuclideanDomain.div_eq_iff_eq_mul_of_dvd, eq_comm
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
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 * z
⊢ x / y = z / t ↔ t * x = y * z

Tactic:
rw [div_eq_iff_eq_mul_of_dvd _ _ _ h1 h3, ← mul_div_assoc _ h4,
    eq_div_iff_mul_eq_of_dvd _ _ _ h2]

Premises used: EuclideanDomain.eq_div_iff_mul_eq_of_dvd, EuclideanDomain.div_eq_iff_eq_mul_of_dvd, EuclideanDomain.mul_div_assoc
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
obtain : ∀ (a : R) (ha : z = t * a), t ∣ y * z
⊢ t ∣ y * z

Tactic:
obtain ⟨a, ha⟩ := h4
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
a : R
ha : z = t * a
h : y * z = t * (y * a)
⊢ t ∣ y * z

Tactic:
use y * a
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
a : R
ha : z = t * a
h : y * (t * a) = t * (y * a)
h₁ : t * a * y = t * (y * a)
h₂ : t * (a * y) = t * (y * a)
h₃ h₄ : t * (a * y) = t * (a * y)
⊢ y * z = t * (y * a)

Tactic:
rw [ha, mul_comm, mul_assoc, mul_comm y a]

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
e : S ≃+* R
a : S
⊢ Eq.{u_2 + 1} (α := S)
    ((e.symm : (a : R) → S) (HDiv.hDiv (α := R) (β := R) ((e : (a : S) → R) a : R) ((e : (a : S) → R) 0 : R)) : S)
    (0 : S)

Tactic:
simp
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
e : S ≃+* R
a b : S
a₁ :
  Eq.{u_1 + 1} (α := R)
    ((e : (a : S) → R)
        (HAdd.hAdd (β := S)
          (HMul.hMul (β := S) b
            ((e.symm : (a : R) → S) (HDiv.hDiv (α := R) (β := R) ((e : (a : S) → R) a : R) ((e : (a : S) → R) b : R)) :
              S))
          ((e.symm : (a : R) → S) (HMod.hMod (α := R) (β := R) ((e : (a : S) → R) a : R) ((e : (a : S) → R) b : R)) :
            S)) :
      R)
    ((e : (a : S) → R) a : R)
⊢ HAdd.hAdd (β := S)
      (HMul.hMul (β := S) b
        ((e.symm : (a : R) → S) (HDiv.hDiv (α := R) (β := R) ((e : (a : S) → R) a : R) ((e : (a : S) → R) b : R)) : S))
      ((e.symm : (a : R) → S) (HMod.hMod (α := R) (β := R) ((e : (a : S) → R) a : R) ((e : (a : S) → R) b : R)) : S) =
    a

Tactic:
apply e.injective

Premises used: RingEquiv.injective
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
e : S ≃+* R
a b : S
⊢ Eq.{u_1 + 1} (α := R)
    ((e : (a : S) → R)
        (HAdd.hAdd (β := S)
          (HMul.hMul (β := S) b
            ((e.symm : (a : R) → S) (HDiv.hDiv (α := R) (β := R) ((e : (a : S) → R) a : R) ((e : (a : S) → R) b : R)) :
              S))
          ((e.symm : (a : R) → S) (HMod.hMod (α := R) (β := R) ((e : (a : S) → R) a : R) ((e : (a : S) → R) b : R)) :
            S)) :
      R)
    ((e : (a : S) → R) a : R)

Tactic:
simpa using EuclideanDomain.quotient_mul_add_remainder_eq (e a) (e b)

Premises used: EuclideanDomain.quotient_mul_add_remainder_eq, DFunLike.coe
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
e : S ≃+* R
a b : S
hb : b ≠ 0
⊢ Ne.{u_1 + 1} (α := R) ((e : (a : S) → R) b : R) (0 : R)

Tactic:
simpa using hb
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
e : S ≃+* R
a b : S
hb : b ≠ 0
⊢ Ne.{u_1 + 1} (α := R) ((e : (a : S) → R) b : R) (0 : R)

Tactic:
have hb' : e b ≠ 0 := by simpa using hb
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
e : S ≃+* R
a b : S
hb : b ≠ 0
hb' : Ne.{u_1 + 1} (α := R) ((e : (a : S) → R) b : R) (0 : R)
⊢ EuclideanDomain.r.{u_1} (R := R)
    ((e : (a : S) → R)
        ((e.symm : (a : R) → S) (HMod.hMod (α := R) (β := R) ((e : (a : S) → R) a : R) ((e : (a : S) → R) b : R)) : S) :
      R)
    ((e : (a : S) → R) b : R)

Tactic:
simpa using EuclideanDomain.remainder_lt (e a) hb'

Premises used: DFunLike.coe, EuclideanDomain.remainder_lt
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
e : S ≃+* R
a b : S
hb : b ≠ 0
hb' : Ne.{u_1 + 1} (α := R) ((e : (a : S) → R) b : R) (0 : R)
⊢ ¬EuclideanDomain.r.{u_1} (R := R) ((e : (a : S) → R) (a * b) : R) ((e : (a : S) → R) a : R)

Tactic:
simpa using EuclideanDomain.mul_left_not_lt (e a) hb'

Premises used: EuclideanDomain.mul_left_not_lt, DFunLike.coe