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
a b r r' s t s' t' : R
p : P a b (r, s, t)
p' : P a b (r', s', t')
⊢ P a b (xgcdAux r s t r' s' t')
have 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')
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]
Cleared hypotheses: r, r', s, t, s', t', p, p'
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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')
⊢ P a b (xgcdAux r s t r' s' t')
have 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')
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]
Cleared hypotheses: r, r', s, t, s', t', p, p'
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
⊢ a = a * 1 + b * 0
have rw : a = a + b * 0
Tactic: rw [mul_one, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
rw : a = a + b * 0
⊢ a = a * 1 + b * 0
have rw₁ : a = a + 0
Tactic: rw [mul_one, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
rw : a = a + b * 0
rw₁ : a = a + 0
⊢ a = a * 1 + b * 0
have rw₂ : a = a
Tactic: rw [mul_one, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
⊢ b = a * 0 + b * 1
have rw : b = a * 0 + b
Tactic: rw [mul_one, mul_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
rw : b = a * 0 + b
⊢ b = a * 0 + b * 1
have rw₁ : b = 0 + b
Tactic: rw [mul_one, mul_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
rw : b = a * 0 + b
rw₁ : b = 0 + b
⊢ b = a * 0 + b * 1
have rw₂ : b = b
Tactic: rw [mul_one, mul_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (hypothesis)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
⊢ gcd a b = a * gcdA a b + b * gcdB a b
have this : 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])
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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)
⊢ gcd a b = a * gcdA a b + b * gcdB a b
have rwa : ∀ (this : P a b (gcd a b, xgcd a b)), gcd a b = a * gcdA a b + b * gcdB a b
Tactic: rwa [xgcdAux_val, xgcd_val] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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
⊢ gcd a b = a * gcdA a b + b * gcdB a b
have 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
Tactic: rwa [xgcdAux_val, xgcd_val] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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
⊢ a = 0
have rw : a * b / b = 0
Tactic: rw [← mul_div_cancel_right₀ a h0.2, h, zero_div]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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
⊢ a = 0
have rw₁ : 0 / b = 0
Tactic: rw [← mul_div_cancel_right₀ a h0.2, h, zero_div]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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
⊢ a = 0
have rw₂ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [← mul_div_cancel_right₀ a h0.2, h, zero_div]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u_1
inst : EuclideanDomain R
a b : R
n : ℕ
hab : b ∣ a
⊢ (a / b) ^ n = a ^ n / b ^ n
have obtain : ∀ (c : R), (b * c / b) ^ n = (b * c) ^ n / b ^ n
Tactic: obtain ⟨c, rfl⟩ := hab
Cleared hypotheses: a, hab
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u_1
inst : EuclideanDomain R
b : R
n : ℕ
c : R
⊢ (b * c / b) ^ n = (b * c) ^ n / b ^ n
have inl : (0 * c / 0) ^ n = (0 * c) ^ n / HPow.hPow (α := R) 0 n
Tactic: obtain rfl | hb := eq_or_ne b 0
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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
⊢ (b * c / b) ^ n = (b * c) ^ n / b ^ n
have inr : ∀ (hb : b ≠ 0), (b * c / b) ^ n = (b * c) ^ n / b ^ n
Tactic: obtain rfl | hb := eq_or_ne b 0
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u_1
inst : EuclideanDomain R
n : ℕ
c : R
⊢ (0 * c / 0) ^ n = (0 * c) ^ n / HPow.hPow (α := R) 0 n
have inl : HPow.hPow (β := ℕ) (0 * c / 0) 0 = HPow.hPow (β := ℕ) (0 * c) 0 / HPow.hPow (α := R) (β := ℕ) 0 0
Tactic: obtain rfl | hn := eq_or_ne n 0
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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
⊢ (0 * c / 0) ^ n = (0 * c) ^ n / HPow.hPow (α := R) 0 n
have inl₁ : ∀ (hn : n ≠ 0), (0 * c / 0) ^ n = (0 * c) ^ n / HPow.hPow (α := R) 0 n
Tactic: obtain rfl | hn := eq_or_ne n 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
hxy : gcd x y = 0
⊢ x ∣ lcm x y
have rw : x ∣ 0
Tactic: rw [lcm, hxy, div_zero]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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
⊢ x * z * gcd x y = x * y
have rw : x * gcd x y * z = x * y
Tactic: rw [mul_right_comm, mul_assoc, ← hz]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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
⊢ x * z * gcd x y = x * y
have rw₁ : x * (gcd x y * z) = x * y
Tactic: rw [mul_right_comm, mul_assoc, ← hz]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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
⊢ x * z * gcd x y = x * y
have rw₂ : x * y = x * y
Tactic: rw [mul_right_comm, mul_assoc, ← hz]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
hxy : gcd x y = 0
⊢ y ∣ lcm x y
have rw : y ∣ 0
Tactic: rw [lcm, hxy, div_zero]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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
⊢ gcd x y * (y * z) = x * y
have rw : gcd x y * y * z = x * y
Tactic: rw [← mul_assoc, mul_right_comm, ← hz]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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
⊢ gcd x y * (y * z) = x * y
have rw₁ : gcd x y * z * y = x * y
Tactic: rw [← mul_assoc, mul_right_comm, ← hz]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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
⊢ gcd x y * (y * z) = x * y
have rw₂ : x * y = x * y
Tactic: rw [← mul_assoc, mul_right_comm, ← hz]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
⊢ lcm x y ∣ z
have rw : x * y / gcd x y ∣ z
Tactic: rw [lcm]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
⊢ x * y / gcd x y ∣ z
have pos : ∀ (hxy : gcd x y = 0), x * y / gcd x y ∣ z
Tactic: by_cases hxy : 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 z : R
hxz : x ∣ z
hyz : y ∣ z
pos : ∀ (hxy : gcd x y = 0), x * y / gcd x y ∣ z
⊢ x * y / gcd x y ∣ z
have neg : ∀ (hxy : ¬gcd x y = 0), x * y / gcd x y ∣ z
Tactic: by_cases hxy : 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 z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : gcd x y = 0
⊢ x * y / gcd x y ∣ z
have pos : 0 ∣ z
Tactic: rw [hxy, div_zero]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (hypothesis)
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
⊢ 0 ∣ z
have hxy₁ : x = 0 ∧ y = 0
Tactic: rw [EuclideanDomain.gcd_eq_zero_iff] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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
⊢ 0 ∣ z
have pos : ∀ (hxz : 0 ∣ z) (hyz : y ∣ z) (hxy : x = 0 ∧ y = 0), 0 ∣ z
Tactic: rwa [hxy.1] at hxz
Cleared hypotheses: hxz, hyz, hxy
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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 * y / gcd x y ∣ z
have neg : ∀ (r : R) (hr : x = gcd x y * r) (s : R) (hs : y = gcd x y * s), x * y / gcd x y ∣ z
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 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
⊢ x * y / gcd x y ∣ z
have obtain : ∀ (p : R) (hp : z * gcd x y = x * y * p), x * y / gcd x y ∣ z
Tactic: obtain ⟨p, hp⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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
⊢ x * y / gcd x y ∣ z
have h : z = x * y / gcd x y * p
Tactic: use p
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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
⊢ z = x * y / gcd x y * p
have h : ∀ (g : R) (hxy : ¬g = 0) (hs : y = g * s) (hp : z * g = x * y * p), z = x * y / g * p
Tactic: generalize gcd x y = g at hxy hs hp ⊢
Cleared hypotheses: hxy, hs, hp
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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
⊢ z = x * y / g * p
have 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
Tactic: subst hs
Cleared hypotheses: y, hyz, hr, hs, hp
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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
⊢ z = x * (g * s) / g * p
have h : x * (g * s) * p = x * s * p * g
Tactic: rw [mul_left_comm, mul_div_cancel_left₀ _ hxy, ← mul_left_inj' hxy, hp]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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
have h : x * g * s * p = x * s * p * g
Tactic: rw [← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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 * y / gcd x y ∣ z
have neg : x * y ∣ z * gcd x y
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]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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 * y ∣ z * gcd x y
have neg : x * y ∣ z * (x * gcdA x y) + z * (y * gcdB x y)
Tactic: rw [gcd_eq_gcd_ab, mul_add]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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 * y ∣ z * (x * gcdA x y) + z * (y * gcdB x y)
have neg : x * y ∣ z * (x * gcdA x y)
Tactic: apply dvd_add
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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)
⊢ x * y ∣ z * (x * gcdA x y) + z * (y * gcdB x y)
have neg₁ : x * y ∣ z * (y * gcdB x y)
Tactic: apply dvd_add
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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 * y ∣ z * (x * gcdA x y)
have neg : x * y ∣ x * (z * gcdA x y)
Tactic: rw [mul_left_comm]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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 * y ∣ x * (z * gcdA x y)
have neg : y ∣ z * gcdA x y
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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 * y ∣ z * (y * gcdB x y)
have neg : y * x ∣ y * (z * gcdB x y)
Tactic: rw [mul_left_comm, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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 * x ∣ y * (z * gcdB x y)
have neg : x ∣ z * gcdB x y
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x : R
⊢ lcm 0 x = 0
have rw : 0 * x / gcd 0 x = 0
Tactic: rw [lcm, zero_mul, zero_div]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x : R
rw : 0 * x / gcd 0 x = 0
⊢ lcm 0 x = 0
have rw₁ : 0 / gcd 0 x = 0
Tactic: rw [lcm, zero_mul, zero_div]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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
⊢ lcm 0 x = 0
have rw₂ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [lcm, zero_mul, zero_div]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x : R
⊢ lcm x 0 = 0
have rw : x * 0 / gcd x 0 = 0
Tactic: rw [lcm, mul_zero, zero_div]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x : R
rw : x * 0 / gcd x 0 = 0
⊢ lcm x 0 = 0
have rw₁ : 0 / gcd x 0 = 0
Tactic: rw [lcm, mul_zero, zero_div]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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
⊢ lcm x 0 = 0
have rw₂ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [lcm, mul_zero, zero_div]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
⊢ lcm x y = 0 ↔ x = 0 ∨ y = 0
have mp : lcm x y = 0 → x = 0 ∨ y = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
mp : lcm x y = 0 → x = 0 ∨ y = 0
⊢ lcm x y = 0 ↔ x = 0 ∨ y = 0
have mpr : x = 0 ∨ y = 0 → lcm x y = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (hypothesis)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
hxy : lcm x y = 0
⊢ x = 0 ∨ y = 0
have hxy₁ : x = 0 ∨ y / gcd x y = 0
Tactic: rw [lcm, mul_div_assoc _ (gcd_dvd_right _ _), mul_eq_zero] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
⊢ x = 0 ∨ y = 0
have apply : y / gcd x y = 0 → y = 0
Tactic: apply Or.imp_right _ hxy
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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
⊢ y = 0
have pos : ∀ (hgxy : gcd x y = 0), y = 0
Tactic: by_cases hgxy : 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
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
pos : ∀ (hgxy : gcd x y = 0), y = 0
⊢ y = 0
have neg : ∀ (hgxy : ¬gcd x y = 0), y = 0
Tactic: by_cases hgxy : gcd x y = 0
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (hypothesis)
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
⊢ y = 0
have hgxy₁ : x = 0 ∧ y = 0
Tactic: rw [EuclideanDomain.gcd_eq_zero_iff] at hgxy
Cleared hypotheses: hgxy
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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
⊢ y = 0
have neg : ∀ (r : R) (hr : x = gcd x y * r) (s : R) (hs : y = gcd x y * s), y = 0
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
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
⊢ y = 0
have neg : ∀ (g : R) (hr : x = g * r) (hs : y = g * s) (hy : y / g = 0) (hgxy : ¬g = 0), y = 0
Tactic: generalize gcd x y = g at hr hs hy hgxy ⊢
Cleared hypotheses: hy, hgxy, hr, 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
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
⊢ y = 0
have neg : ∀ (hxy : x = 0 ∨ g * s / gcd x (g * s) = 0) (hy : g * s / g = 0), g * s = 0
Tactic: subst hs
Cleared hypotheses: y, hxy, hs, hy
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (hypothesis)
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
⊢ g * s = 0
have hy₁ : s = 0
Tactic: rw [mul_div_cancel_left₀ _ hgxy] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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
⊢ g * s = 0
have neg : g * 0 = 0
Tactic: rw [hy, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
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
⊢ g * s = 0
have neg₁ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [hy, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
hx : x = 0
⊢ lcm x y = 0
have mpr : lcm 0 y = 0
Tactic: rw [hx, lcm_zero_left]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
hx : x = 0
mpr : lcm 0 y = 0
⊢ lcm x y = 0
have mpr₁ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [hx, lcm_zero_left]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
hy : y = 0
⊢ lcm x y = 0
have mpr : lcm x 0 = 0
Tactic: rw [hy, lcm_zero_right]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
hy : y = 0
mpr : lcm x 0 = 0
⊢ lcm x y = 0
have mpr₁ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [hy, lcm_zero_right]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
⊢ gcd x y * lcm x y = x * y
have rw : gcd x y * (x * y / gcd x y) = x * y
Tactic: rw [lcm]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
⊢ gcd x y * (x * y / gcd x y) = x * y
have pos : ∀ (h : gcd x y = 0), gcd x y * (x * y / gcd x y) = x * y
Tactic: by_cases h : gcd x y = 0