awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x_1 y_1 x y : R
h : x ≠ 0
IH : ∀ (s t s' t' : R), (xgcdAux (y % x) s t x s' t').1 = gcd (y % x) x
s t s' t' : R
simp : gcd (y % x) x = gcd x y
⊢ (xgcdAux x s t y s' t').1 = gcd x y

Tactic:
simp only [xgcdAux_rec h, IH]

Premises used: EuclideanDomain.xgcdAux_rec
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x_1 y_1 x y : R
h : x ≠ 0
IH : ∀ (s t s' t' : R), (xgcdAux (y % x) s t x s' t').1 = gcd (y % x) x
s t s' t' : R
rw rw₁ : gcd x y = gcd x y
⊢ gcd (y % x) x = gcd x y

Tactic:
rw [← gcd_val]

Premises used: EuclideanDomain.gcd_val
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
rw : xgcdAux x 1 0 y 0 1 = (gcd x y, (xgcdAux x 1 0 y 0 1).2)
rw₁ rw₂ : xgcdAux x 1 0 y 0 1 = ((xgcdAux x 1 0 y 0 1).1, (xgcdAux x 1 0 y 0 1).2)
⊢ xgcdAux x 1 0 y 0 1 = (gcd x y, xgcd x y)

Tactic:
rw [xgcd, ← xgcdAux_fst x y 1 0 0 1]

Premises used: EuclideanDomain.xgcdAux_fst, EuclideanDomain.xgcd, OfNat.ofNat
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b n s t s' t' : R
p : P a b (0, s, t)
p' : P a b (n, s', t')
⊢ P a b (xgcdAux 0 s t n s' t')

Tactic:
simpa only [xgcd_zero_left]

Premises used: EuclideanDomain.xgcd_zero_left
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b a_1 b_1 : R
h : a_1 ≠ 0
IH :
  ∀ {s t s' t' : R} (p : P a b (b_1 % a_1, s, t)) (p' : P a b (a_1, s', t')), P a b (xgcdAux (b_1 % a_1) s t a_1 s' t')
s t s' t' : R
p : P a b (a_1, s, t)
p' : P a b (b_1, s', t')
H1 : P a b (xgcdAux (b_1 % a_1) (s' - b_1 / a_1 * s) (t' - b_1 / a_1 * t) a_1 s t)
⊢ P a b (xgcdAux a_1 s t b_1 s' t')

Tactic:
rw [xgcdAux_rec h]

Premises used: EuclideanDomain.xgcdAux_rec
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b a_1 b_1 : R
h : a_1 ≠ 0
IH :
  ∀ {s t s' t' : R} (p : P a b (b_1 % a_1, s, t)) (p' : P a b (a_1, s', t')), P a b (xgcdAux (b_1 % a_1) s t a_1 s' t')
s t s' t' : R
p : P a b (a_1, s, t)
p' : P a b (b_1, s', t')
⊢ P a b (xgcdAux (b_1 % a_1) (s' - b_1 / a_1 * s) (t' - b_1 / a_1 * t) a_1 s t)

Tactic:
IH ?_ p
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b a_1 b_1 : R
h : a_1 ≠ 0
IH :
  ∀ {s t s' t' : R} (p : P a b (b_1 % a_1, s, t)) (p' : P a b (a_1, s', t')), P a b (xgcdAux (b_1 % a_1) s t a_1 s' t')
s t s' t' : R
p : P a b (a_1, s, t)
p' : P a b (b_1, s', t')
H1 : P a b (b_1 % a_1, s' - b_1 / a_1 * s, t' - b_1 / a_1 * t)
⊢ P a b (xgcdAux (b_1 % a_1) (s' - b_1 / a_1 * s) (t' - b_1 / a_1 * t) a_1 s t)

Tactic:
refine IH ?_ p
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b a_1 b_1 : R
h : a_1 ≠ 0
IH :
  ∀ {s t s' t' : R} (p : P a b (b_1 % a_1, s, t)) (p' : P a b (a_1, s', t')), P a b (xgcdAux (b_1 % a_1) s t a_1 s' t')
s t s' t' : R
p :
  match (motive := R × R × R → Prop) (a_1, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (motive := R × R × R → Prop) (b_1, s', t') with
  | (r, s, t) => r = a * s + b * t
H1 : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + b * (t' - b_1 / a_1 * t)
H1₁ : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + (b * t' - b * (b_1 / a_1 * t))
H1₂ : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + b * t' - b * (b_1 / a_1 * t)
H1₃ : b_1 % a_1 = a * s' + b * t' - a * (b_1 / a_1 * s) - b * (b_1 / a_1 * t)
H1₄ : b_1 % a_1 = b_1 - a * (b_1 / a_1 * s) - b * (b_1 / a_1 * t)
H1₅ : b_1 % a_1 = b_1 - (a * (b_1 / a_1 * s) + b * (b_1 / a_1 * t))
H1₆ : b_1 % a_1 = b_1 - (a * (s * (b_1 / a_1)) + b * (b_1 / a_1 * t))
H1₇ : b_1 % a_1 = b_1 - (a * s * (b_1 / a_1) + b * (b_1 / a_1 * t))
H1₈ : b_1 % a_1 = b_1 - (a * s * (b_1 / a_1) + b * (t * (b_1 / a_1)))
H1₉ : b_1 % a_1 = b_1 - (a * s * (b_1 / a_1) + b * t * (b_1 / a_1))
H1₁₀ : b_1 % a_1 = b_1 - (a * s + b * t) * (b_1 / a_1)
H1₁₁ : b_1 % a_1 = b_1 - a_1 * (b_1 / a_1)
H1₁₂ H1₁₃ : b_1 - a_1 * (b_1 / a_1) = b_1 - a_1 * (b_1 / a_1)
⊢ b_1 % a_1 = a * (s' - b_1 / a_1 * s) + b * (t' - b_1 / a_1 * t)

Tactic:
rw [mul_sub, mul_sub, add_sub, sub_add_eq_add_sub, ← p', sub_sub, mul_comm _ s, ← mul_assoc,
      mul_comm _ t, ← mul_assoc, ← add_mul, ← p, mod_eq_sub_mul_div]

Premises used: add_mul, mul_sub, add_sub, mul_assoc, EuclideanDomain.mod_eq_sub_mul_div, sub_sub, mul_comm, sub_add_eq_add_sub
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b r r' s t s' t' : R
p : P a b (r, s, t)
p' : P a b (r', s', t')
H0 : ∀ (n : R) {s t s' t' : R} (p : P a b (0, s, t)) (p' : P a b (n, s', t')), P a b (xgcdAux 0 s t n s' t')
H1 :
  ∀ (a_1 b_1 : R) (h : a_1 ≠ 0)
    (IH :
      ∀ {s t s' t' : R} (p : P a b (b_1 % a_1, s, t)) (p' : P a b (a_1, s', t')),
        P a b (xgcdAux (b_1 % a_1) s t a_1 s' t'))
    {s t s' t' : R} (p : P a b (a_1, s, t)) (p' : P a b (b_1, s', t')), P a b (xgcdAux a_1 s t b_1 s' t')
⊢ P a b (xgcdAux r s t r' s' t')

Tactic:
induction r, r' using GCD.induction generalizing s t s' t' with
  | H0 n => simpa only [xgcd_zero_left]
  | H1 _ _ h IH =>
    rw [xgcdAux_rec h]
    refine IH ?_ p
    unfold P at p p' ⊢
    dsimp
    rw [mul_sub, mul_sub, add_sub, sub_add_eq_add_sub, ← p', sub_sub, mul_comm _ s, ← mul_assoc,
      mul_comm _ t, ← mul_assoc, ← add_mul, ← p, mod_eq_sub_mul_div]

Premises used: add_mul, mul_sub, add_sub, mul_assoc, EuclideanDomain.mod_eq_sub_mul_div, _private.0.EuclideanDomain.P, sub_sub, EuclideanDomain.xgcd_zero_left, mul_comm, sub_add_eq_add_sub
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
rw : a = a + b * 0
rw₁ : a = a + 0
rw₂ rw₃ : a = a
⊢ a = a * 1 + b * 0

Tactic:
rw [mul_one, mul_zero, add_zero]

Premises used: MulZeroClass.mul_zero, mul_one, add_zero
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
rw : b = a * 0 + b
rw₁ : b = 0 + b
rw₂ rw₃ : b = b
⊢ b = a * 0 + b * 1

Tactic:
rw [mul_one, mul_zero, zero_add]

Premises used: zero_add, MulZeroClass.mul_zero, mul_one
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
⊢ P a b (xgcdAux a 1 0 b 0 1)

Tactic:
have :=
    @xgcdAux_P _ _ _ a b a b 1 0 0 1 (by dsimp [P]; rw [mul_one, mul_zero, add_zero])
      (by dsimp [P]; rw [mul_one, mul_zero, zero_add])
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
this : P a b (xgcdAux a 1 0 b 0 1)
rwa : ∀ (this : P a b (gcd a b, xgcd a b)), gcd a b = a * gcdA a b + b * gcdB a b
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : P a b (gcd a b, gcdA a b, gcdB a b)), gcd a b = a * gcdA a b + b * gcdB a b
⊢ gcd a b = a * gcdA a b + b * gcdB a b

Tactic:
rwa [xgcdAux_val, xgcd_val] at this

Premises used: EuclideanDomain.xgcdAux_val, EuclideanDomain.xgcd_val
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R_1 : Type u
inst : EuclideanDomain R_1
inst_1 : DecidableEq R_1
R : Type u_1
e : EuclideanDomain R
this : DecidableEq R
a b : R
h : a * b = 0
h0 : ¬a = 0 ∧ ¬b = 0
rw : a * b / b = 0
rw₁ : 0 / b = 0
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 0 0
⊢ a = 0

Tactic:
rw [← mul_div_cancel_right₀ a h0.2, h, zero_div]

Premises used: EuclideanDomain.zero_div, mul_div_cancel_right₀, And.right
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u_1
inst : EuclideanDomain R
a b : R
n : ℕ
hab : b ∣ a
obtain : ∀ (c : R), (b * c / b) ^ n = (b * c) ^ n / b ^ n
⊢ (a / b) ^ n = a ^ n / b ^ n

Tactic:
obtain ⟨c, rfl⟩ := hab

Premises used: rfl
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u_1
inst : EuclideanDomain R
b : R
n : ℕ
c : R
inl : (0 * c / 0) ^ n = (0 * c) ^ n / HPow.hPow (α := R) 0 n
inr : ∀ (hb : b ≠ 0), (b * c / b) ^ n = (b * c) ^ n / b ^ n
⊢ (b * c / b) ^ n = (b * c) ^ n / b ^ n

Tactic:
obtain rfl | hb := eq_or_ne b 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u_1
inst : EuclideanDomain R
n : ℕ
c : R
inl : HPow.hPow (β := ℕ) (0 * c / 0) 0 = HPow.hPow (β := ℕ) (0 * c) 0 / HPow.hPow (α := R) (β := ℕ) 0 0
inl₁ : ∀ (hn : n ≠ 0), (0 * c / 0) ^ n = (0 * c) ^ n / HPow.hPow (α := R) 0 n
⊢ (0 * c / 0) ^ n = (0 * c) ^ n / HPow.hPow (α := R) 0 n

Tactic:
obtain rfl | hn := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u_1
inst : EuclideanDomain R
c : R
⊢ HPow.hPow (β := ℕ) (0 * c / 0) 0 = HPow.hPow (β := ℕ) (0 * c) 0 / HPow.hPow (α := R) (β := ℕ) 0 0

Tactic:
simp [*]
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u_1
inst : EuclideanDomain R
n : ℕ
c : R
hn : n ≠ 0
⊢ (0 * c / 0) ^ n = (0 * c) ^ n / HPow.hPow (α := R) 0 n

Tactic:
simp [*]
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u_1
inst : EuclideanDomain R
b : R
n : ℕ
c : R
hb : b ≠ 0
⊢ (b * c / b) ^ n = (b * c) ^ n / b ^ n

Tactic:
simp [hb, mul_pow]

Premises used: mul_pow
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
hxy : gcd x y = 0
rw : x ∣ 0
⊢ x ∣ lcm x y

Tactic:
rw [lcm, hxy, div_zero]

Premises used: EuclideanDomain.div_zero, EuclideanDomain.lcm
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
hxy : gcd x y = 0
⊢ x ∣ 0

Tactic:
dvd_zero _

Premises used: dvd_zero
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
hxy : gcd x y = 0
⊢ x ∣ 0

Tactic:
exact dvd_zero _

Premises used: dvd_zero
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
hxy : ¬gcd x y = 0
z : R
hz : y = gcd x y * z
rw : x * gcd x y * z = x * y
rw₁ : x * (gcd x y * z) = x * y
rw₂ rw₃ : x * y = x * y
⊢ x * z * gcd x y = x * y

Tactic:
rw [mul_right_comm, mul_assoc, ← hz]

Premises used: mul_assoc, mul_right_comm
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
hxy : gcd x y = 0
rw : y ∣ 0
⊢ y ∣ lcm x y

Tactic:
rw [lcm, hxy, div_zero]

Premises used: EuclideanDomain.div_zero, EuclideanDomain.lcm
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
hxy : gcd x y = 0
⊢ y ∣ 0

Tactic:
dvd_zero _

Premises used: dvd_zero
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
hxy : gcd x y = 0
⊢ y ∣ 0

Tactic:
exact dvd_zero _

Premises used: dvd_zero
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
hxy : ¬gcd x y = 0
z : R
hz : x = gcd x y * z
rw : gcd x y * y * z = x * y
rw₁ : gcd x y * z * y = x * y
rw₂ rw₃ : x * y = x * y
⊢ gcd x y * (y * z) = x * y

Tactic:
rw [← mul_assoc, mul_right_comm, ← hz]

Premises used: mul_assoc, mul_right_comm
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
rw : x * y / gcd x y ∣ z
⊢ lcm x y ∣ z

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 z : R
hxz : x ∣ z
hyz : y ∣ z
pos : ∀ (hxy : gcd x y = 0), x * y / gcd x y ∣ z
neg : ∀ (hxy : ¬gcd x y = 0), x * y / gcd x y ∣ z
⊢ x * y / gcd x y ∣ z

Tactic:
by_cases hxy : 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 z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : gcd x y = 0
pos : 0 ∣ z
⊢ x * y / gcd x y ∣ z

Tactic:
rw [hxy, div_zero]

Premises used: EuclideanDomain.div_zero
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : gcd x y = 0
⊢ x = 0 ∧ y = 0

Tactic:
rw [EuclideanDomain.gcd_eq_zero_iff] at hxy

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 z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : x = 0 ∧ y = 0
pos pos₁ pos₂ pos₃ : ∀ (hxz : 0 ∣ z) (hyz : y ∣ z) (hxy : x = 0 ∧ y = 0), 0 ∣ z
⊢ 0 ∣ z

Tactic:
rwa [hxy.1] at hxz

Premises used: And.left
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
neg : ∀ (r : R) (hr : x = gcd x y * r) (s : R) (hs : y = gcd x y * s), x * y / gcd x y ∣ z
⊢ x * y / gcd x y ∣ z

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 z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
this : x * y ∣ z * gcd x y
obtain : ∀ (p : R) (hp : z * gcd x y = x * y * p), x * y / gcd x y ∣ z
⊢ x * y / gcd x y ∣ z

Tactic:
obtain ⟨p, hp⟩ := this
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
p : R
hp : z * gcd x y = x * y * p
h : z = x * y / gcd x y * p
⊢ x * y / gcd x y ∣ z

Tactic:
use p
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
p : R
hp : z * gcd x y = x * y * p
h : ∀ (g : R) (hxy : ¬g = 0) (hs : y = g * s) (hp : z * g = x * y * p), z = x * y / g * p
⊢ z = x * y / gcd x y * p

Tactic:
generalize gcd x y = g at hxy hs hp ⊢

Premises used: EuclideanDomain.gcd
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
r : R
hr : x = gcd x y * r
s p g : R
hxy : ¬g = 0
hs : y = g * s
hp : z * g = x * y * p
h : ∀ (hyz : g * s ∣ z) (hr : x = gcd x (g * s) * r) (hp : z * g = x * (g * s) * p), z = x * (g * s) / g * p
⊢ z = x * y / g * p

Tactic:
subst hs
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x z : R
hxz : x ∣ z
r s p g : R
hxy : ¬g = 0
hyz : g * s ∣ z
hr : x = gcd x (g * s) * r
hp : z * g = x * (g * s) * p
h : x * (g * s) * p = x * s * p * g
⊢ z = x * (g * s) / g * p

Tactic:
rw [mul_left_comm, mul_div_cancel_left₀ _ hxy, ← mul_left_inj' hxy, hp]

Premises used: mul_div_cancel_left₀, mul_left_comm, mul_left_inj'
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x z : R
hxz : x ∣ z
r s p g : R
hxy : ¬g = 0
hyz : g * s ∣ z
hr : x = gcd x (g * s) * r
hp : z * g = x * (g * s) * p
h : x * g * s * p = x * s * p * g
⊢ x * (g * s) * p = x * s * p * g

Tactic:
rw [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x z : R
hxz : x ∣ z
r s p g : R
hxy : ¬g = 0
hyz : g * s ∣ z
hr : x = gcd x (g * s) * r
hp : z * g = x * (g * s) * p
⊢ x * g * s * p = x * s * p * g

Tactic:
simp only [mul_right_comm]

Premises used: mul_right_comm
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
neg : x * y ∣ z * gcd x y
⊢ x * y / gcd x y ∣ z

Tactic:
suffices x * y ∣ z * gcd x y by
    obtain ⟨p, hp⟩ := this
    use p
    generalize gcd x y = g at hxy hs hp ⊢
    subst hs
    rw [mul_left_comm, mul_div_cancel_left₀ _ hxy, ← mul_left_inj' hxy, hp]
    rw [← mul_assoc]
    simp only [mul_right_comm]
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
neg : x * y ∣ z * (x * gcdA x y) + z * (y * gcdB x y)
⊢ x * y ∣ z * gcd x y

Tactic:
rw [gcd_eq_gcd_ab, mul_add]

Premises used: EuclideanDomain.gcd_eq_gcd_ab, mul_add
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
neg : x * y ∣ z * (x * gcdA x y)
neg₁ : x * y ∣ z * (y * gcdB x y)
⊢ x * y ∣ z * (x * gcdA x y) + z * (y * gcdB x y)

Tactic:
apply dvd_add

Premises used: dvd_add
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
neg : x * y ∣ x * (z * gcdA x y)
⊢ x * y ∣ z * (x * gcdA x y)

Tactic:
rw [mul_left_comm]

Premises used: mul_left_comm
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
neg : y ∣ z * gcdA x y
⊢ x * y ∣ x * (z * gcdA x y)

Tactic:
gcongr
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ y ∣ z * gcdA x y

Tactic:
apply hyz.mul_right

Premises used: Dvd.dvd.mul_right
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
neg : y * x ∣ y * (z * gcdB x y)
⊢ x * y ∣ z * (y * gcdB x y)

Tactic:
rw [mul_left_comm, mul_comm]

Premises used: mul_left_comm, mul_comm
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
neg : x ∣ z * gcdB x y
⊢ y * x ∣ y * (z * gcdB x y)

Tactic:
gcongr
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ x ∣ z * gcdB x y

Tactic:
apply hxz.mul_right

Premises used: Dvd.dvd.mul_right
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y z : R
⊢ lcm x y ∣ z ↔ x ∣ z ∧ y ∣ z

Tactic:
⟨fun hz => ⟨(dvd_lcm_left _ _).trans hz, (dvd_lcm_right _ _).trans hz⟩, fun ⟨hxz, hyz⟩ =>
    lcm_dvd hxz hyz⟩

Premises used: EuclideanDomain.lcm_dvd, Dvd.dvd, EuclideanDomain.dvd_lcm_right, And.intro, Iff.intro, EuclideanDomain.dvd_lcm_left, EuclideanDomain.lcm, _private.0.EuclideanDomain.lcm_dvd_iff.match_1, Dvd.dvd.trans
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x : R
rw : 0 * x / gcd 0 x = 0
rw₁ : 0 / gcd 0 x = 0
rw₂ rw₃ : Eq.{u + 1} (α := R) 0 0
⊢ lcm 0 x = 0

Tactic:
rw [lcm, zero_mul, zero_div]

Premises used: EuclideanDomain.zero_div, MulZeroClass.zero_mul, EuclideanDomain.lcm
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x : R
rw : x * 0 / gcd x 0 = 0
rw₁ : 0 / gcd x 0 = 0
rw₂ rw₃ : Eq.{u + 1} (α := R) 0 0
⊢ lcm x 0 = 0

Tactic:
rw [lcm, mul_zero, zero_div]

Premises used: EuclideanDomain.zero_div, MulZeroClass.mul_zero, EuclideanDomain.lcm
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
mp : lcm x y = 0 → x = 0 ∨ y = 0
mpr : x = 0 ∨ y = 0 → lcm x y = 0
⊢ lcm x y = 0 ↔ x = 0 ∨ y = 0

Tactic:
constructor
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
hxy : lcm x y = 0
⊢ x = 0 ∨ y / gcd x y = 0

Tactic:
rw [lcm, mul_div_assoc _ (gcd_dvd_right _ _), mul_eq_zero] at hxy

Premises used: mul_eq_zero, EuclideanDomain.mul_div_assoc, EuclideanDomain.gcd_dvd_right, EuclideanDomain.lcm
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
apply : y / gcd x y = 0 → y = 0
⊢ x = 0 ∨ y = 0

Tactic:
apply Or.imp_right _ hxy

Premises used: Or.imp_right
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
pos : ∀ (hgxy : gcd x y = 0), y = 0
neg : ∀ (hgxy : ¬gcd x y = 0), y = 0
⊢ y = 0

Tactic:
by_cases hgxy : 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
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
hgxy : gcd x y = 0
⊢ x = 0 ∧ y = 0

Tactic:
rw [EuclideanDomain.gcd_eq_zero_iff] at hgxy

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
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
hgxy : x = 0 ∧ y = 0
⊢ y = 0

Tactic:
hgxy.2

Premises used: And.right
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
hgxy : x = 0 ∧ y = 0
⊢ y = 0

Tactic:
exact hgxy.2

Premises used: And.right
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
hgxy : ¬gcd x y = 0
neg : ∀ (r : R) (hr : x = gcd x y * r) (s : R) (hs : y = gcd x y * s), y = 0
⊢ y = 0

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
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
hgxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
neg : ∀ (g : R) (hr : x = g * r) (hs : y = g * s) (hy : y / g = 0) (hgxy : ¬g = 0), y = 0
⊢ y = 0

Tactic:
generalize gcd x y = g at hr hs hy hgxy ⊢

Premises used: EuclideanDomain.gcd
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
r s g : R
hr : x = g * r
hs : y = g * s
hy : y / g = 0
hgxy : ¬g = 0
neg : ∀ (hxy : x = 0 ∨ g * s / gcd x (g * s) = 0) (hy : g * s / g = 0), g * s = 0
⊢ y = 0

Tactic:
subst hs
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x r s g : R
hr : x = g * r
hgxy : ¬g = 0
hxy : x = 0 ∨ g * s / gcd x (g * s) = 0
hy : g * s / g = 0
⊢ s = 0

Tactic:
rw [mul_div_cancel_left₀ _ hgxy] at hy

Premises used: mul_div_cancel_left₀
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x r s g : R
hr : x = g * r
hgxy : ¬g = 0
hxy : x = 0 ∨ g * s / gcd x (g * s) = 0
hy : s = 0
neg : g * 0 = 0
neg₁ neg₂ : Eq.{u + 1} (α := R) 0 0
⊢ g * s = 0

Tactic:
rw [hy, mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
hx : x = 0
mpr : lcm 0 y = 0
mpr₁ mpr₂ : Eq.{u + 1} (α := R) 0 0
⊢ lcm x y = 0

Tactic:
rw [hx, lcm_zero_left]

Premises used: EuclideanDomain.lcm_zero_left
-- Module: Mathlib.Algebra.EuclideanDomain.Basic
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
hy : y = 0
mpr : lcm x 0 = 0
mpr₁ mpr₂ : Eq.{u + 1} (α := R) 0 0
⊢ lcm x y = 0

Tactic:
rw [hy, lcm_zero_right]

Premises used: EuclideanDomain.lcm_zero_right