awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Commute (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b c : M₀
ha : IsUnit a
k : ℕ
rw : (a ^ k)⁻¹ʳ * b = c ↔ b = a ^ k * c
⊢ a⁻¹ʳ ^ k * b = c ↔ b = a ^ k * c
have rw₁ : b = a ^ k * c ↔ b = a ^ k * c
Tactic: rw [Ring.inverse_pow, Ring.inverse_mul_eq_iff_eq_mul _ _ _ (IsUnit.pow _ ha)]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Commute (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
a b c : G₀
hac : Commute a c
hbc : Commute b c
⊢ Commute (a / b) c
have rw : Commute (a * b⁻¹) c
Tactic: rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Conj (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
⊢ IsConj a b ↔ ∃ (c : α), c ≠ 0 ∧ c * a * c⁻¹ = b
have rw : (∃ (x : α), x ≠ 0 ∧ SemiconjBy x a b) ↔ ∃ (c : α), c ≠ 0 ∧ c * a * c⁻¹ = b
Tactic: rw [IsConj, Units.exists_iff_ne_zero (p := (SemiconjBy · a b))]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Conj (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
⊢ (∃ (x : α), x ≠ 0 ∧ SemiconjBy x a b) ↔ ∃ (c : α), c ≠ 0 ∧ c * a * c⁻¹ = b
have a₁ : ∀ (c : α), c ≠ 0 ∧ SemiconjBy c a b ↔ c ≠ 0 ∧ c * a * c⁻¹ = b
Tactic: congr! 2 with c
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Defs (goal)
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
inst_1 : IsLeftCancelMulZero M₀
a b c : M₀
⊢ a * b = a * c ↔ b = c ∨ a = 0
have pos : ∀ (ha : a = 0), a * b = a * c ↔ b = c ∨ a = 0
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Defs (goal)
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
inst_1 : IsLeftCancelMulZero M₀
a b c : M₀
pos : ∀ (ha : a = 0), a * b = a * c ↔ b = c ∨ a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0
have neg : ∀ (ha : ¬a = 0), a * b = a * c ↔ b = c ∨ a = 0
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Defs (goal)
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
inst_1 : IsLeftCancelMulZero M₀
a b c : M₀
⊢ a * b = a * c ↔ b = c ∨ a = 0
have pos : ∀ (ha : a = 0), a * b = a * c ↔ b = c ∨ a = 0
Tactic: by_cases ha : a = 0 <;> [simp only [ha, zero_mul, or_true]; simp [mul_right_inj', ha]]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Defs (goal)
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
inst_1 : IsLeftCancelMulZero M₀
a b c : M₀
pos : ∀ (ha : a = 0), a * b = a * c ↔ b = c ∨ a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0
have neg : ∀ (ha : ¬a = 0), a * b = a * c ↔ b = c ∨ a = 0
Tactic: by_cases ha : a = 0 <;> [simp only [ha, zero_mul, or_true]; simp [mul_right_inj', ha]]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Defs (goal)
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
inst_1 : IsRightCancelMulZero M₀
a b c : M₀
⊢ a * c = b * c ↔ a = b ∨ c = 0
have pos : ∀ (hc : c = 0), a * c = b * c ↔ a = b ∨ c = 0
Tactic: by_cases hc : c = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Defs (goal)
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
inst_1 : IsRightCancelMulZero M₀
a b c : M₀
pos : ∀ (hc : c = 0), a * c = b * c ↔ a = b ∨ c = 0
⊢ a * c = b * c ↔ a = b ∨ c = 0
have neg : ∀ (hc : ¬c = 0), a * c = b * c ↔ a = b ∨ c = 0
Tactic: by_cases hc : c = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Defs (goal)
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
inst_1 : IsRightCancelMulZero M₀
a b c : M₀
⊢ a * c = b * c ↔ a = b ∨ c = 0
have pos : ∀ (hc : c = 0), a * c = b * c ↔ a = b ∨ c = 0
Tactic: by_cases hc : c = 0 <;> [simp only [hc, mul_zero, or_true]; simp [mul_left_inj', hc]]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Defs (goal)
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
inst_1 : IsRightCancelMulZero M₀
a b c : M₀
pos : ∀ (hc : c = 0), a * c = b * c ↔ a = b ∨ c = 0
⊢ a * c = b * c ↔ a = b ∨ c = 0
have neg : ∀ (hc : ¬c = 0), a * c = b * c ↔ a = b ∨ c = 0
Tactic: by_cases hc : c = 0 <;> [simp only [hc, mul_zero, or_true]; simp [mul_left_inj', hc]]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Defs (goal)
Goal:
M₀ : Type u_2
inst : Mul M₀
inst_1 : Zero M₀
⊢ IsCancelMulZero M₀ ↔ ∀ {a : M₀}, a ≠ 0 → IsRegular a
have simp : (∀ (x : M₀) (x_1 : x ≠ 0), IsLeftRegular x ∧ IsRightRegular x) ↔ ∀ {a : M₀}, a ≠ 0 → IsRegular a
Tactic: simp only [isCancelMulZero_iff, isLeftCancelMulZero_iff, isRightCancelMulZero_iff, ← forall_and]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Defs (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
M : Type u_2
inst_1 : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
y : M₀
⊢ f (HPow.hPow (β := ℕ) x 0 * y) = HPow.hPow (β := ℕ) (f x) 0 * f y
have zero : f (1 * y) = HPow.hPow (β := ℕ) (f x) 0 * f y
Tactic: rw [pow_zero, pow_zero, one_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Defs (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
M : Type u_2
inst_1 : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
y : M₀
zero : f (1 * y) = HPow.hPow (β := ℕ) (f x) 0 * f y
⊢ f (HPow.hPow (β := ℕ) x 0 * y) = HPow.hPow (β := ℕ) (f x) 0 * f y
have zero₁ : f (1 * y) = 1 * f y
Tactic: rw [pow_zero, pow_zero, one_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Defs (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
M : Type u_2
inst_1 : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
y : M₀
zero : f (1 * y) = HPow.hPow (β := ℕ) (f x) 0 * f y
zero₁ : f (1 * y) = 1 * f y
⊢ f (HPow.hPow (β := ℕ) x 0 * y) = HPow.hPow (β := ℕ) (f x) 0 * f y
have zero₂ : f y = 1 * f y
Tactic: rw [pow_zero, pow_zero, one_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Defs (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
M : Type u_2
inst_1 : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
y : M₀
zero : f (1 * y) = HPow.hPow (β := ℕ) (f x) 0 * f y
zero₁ : f (1 * y) = 1 * f y
zero₂ : f y = 1 * f y
⊢ f (HPow.hPow (β := ℕ) x 0 * y) = HPow.hPow (β := ℕ) (f x) 0 * f y
have zero₃ : f y = f y
Tactic: rw [pow_zero, pow_zero, one_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Defs (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
M : Type u_2
inst_1 : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
n : ℕ
hn : ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y
y : M₀
⊢ f (x ^ (n + 1) * y) = f x ^ (n + 1) * f y
have succ : f (x * x ^ n * y) = f x ^ (n + 1) * f y
Tactic: rw [pow_succ', pow_succ', mul_assoc, mul_assoc, hx, hn]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Defs (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
M : Type u_2
inst_1 : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
n : ℕ
hn : ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y
y : M₀
succ : f (x * x ^ n * y) = f x ^ (n + 1) * f y
⊢ f (x ^ (n + 1) * y) = f x ^ (n + 1) * f y
have succ₁ : f (x * x ^ n * y) = f x * f x ^ n * f y
Tactic: rw [pow_succ', pow_succ', mul_assoc, mul_assoc, hx, hn]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Defs (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
M : Type u_2
inst_1 : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
n : ℕ
hn : ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y
y : M₀
succ : f (x * x ^ n * y) = f x ^ (n + 1) * f y
succ₁ : f (x * x ^ n * y) = f x * f x ^ n * f y
⊢ f (x ^ (n + 1) * y) = f x ^ (n + 1) * f y
have succ₂ : f (x * (x ^ n * y)) = f x * f x ^ n * f y
Tactic: rw [pow_succ', pow_succ', mul_assoc, mul_assoc, hx, hn]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Defs (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
M : Type u_2
inst_1 : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
n : ℕ
hn : ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y
y : M₀
succ : f (x * x ^ n * y) = f x ^ (n + 1) * f y
succ₁ : f (x * x ^ n * y) = f x * f x ^ n * f y
succ₂ : f (x * (x ^ n * y)) = f x * f x ^ n * f y
⊢ f (x ^ (n + 1) * y) = f x ^ (n + 1) * f y
have succ₃ : f (x * (x ^ n * y)) = f x * (f x ^ n * f y)
Tactic: rw [pow_succ', pow_succ', mul_assoc, mul_assoc, hx, hn]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Defs (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
M : Type u_2
inst_1 : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
n : ℕ
hn : ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y
y : M₀
succ : f (x * x ^ n * y) = f x ^ (n + 1) * f y
succ₁ : f (x * x ^ n * y) = f x * f x ^ n * f y
succ₂ : f (x * (x ^ n * y)) = f x * f x ^ n * f y
succ₃ : f (x * (x ^ n * y)) = f x * (f x ^ n * f y)
⊢ f (x ^ (n + 1) * y) = f x ^ (n + 1) * f y
have succ₄ : f x * f (x ^ n * y) = f x * (f x ^ n * f y)
Tactic: rw [pow_succ', pow_succ', mul_assoc, mul_assoc, hx, hn]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Defs (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
M : Type u_2
inst_1 : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
n : ℕ
hn : ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y
y : M₀
succ : f (x * x ^ n * y) = f x ^ (n + 1) * f y
succ₁ : f (x * x ^ n * y) = f x * f x ^ n * f y
succ₂ : f (x * (x ^ n * y)) = f x * f x ^ n * f y
succ₃ : f (x * (x ^ n * y)) = f x * (f x ^ n * f y)
succ₄ : f x * f (x ^ n * y) = f x * (f x ^ n * f y)
⊢ f (x ^ (n + 1) * y) = f x ^ (n + 1) * f y
have succ₅ : f x * (f x ^ n * f y) = f x * (f x ^ n * f y)
Tactic: rw [pow_succ', pow_succ', mul_assoc, mul_assoc, hx, hn]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Defs (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
M : Type u_2
inst_1 : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
n : ℕ
⊢ ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y
have zero : ∀ (y : M₀), f (HPow.hPow (β := ℕ) x 0 * y) = HPow.hPow (β := ℕ) (f x) 0 * f y
Tactic: induction n with
  | zero => intro y; rw [pow_zero, pow_zero, one_mul, one_mul]
  | succ n hn => intro y; rw [pow_succ', pow_succ', mul_assoc, mul_assoc, hx, hn]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Defs (goal)
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
M : Type u_2
inst_1 : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
n : ℕ
zero : ∀ (y : M₀), f (HPow.hPow (β := ℕ) x 0 * y) = HPow.hPow (β := ℕ) (f x) 0 * f y
⊢ ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y
have succ : ∀ (n : ℕ) (hn : ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y) (y : M₀), f (x ^ (n + 1) * y) = f x ^ (n + 1) * f y
Tactic: induction n with
  | zero => intro y; rw [pow_zero, pow_zero, one_mul, one_mul]
  | succ n hn => intro y; rw [pow_succ', pow_succ', mul_assoc, mul_assoc, hx, hn]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Defs (goal)
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
inst_1 : Div M₀
inst_2 : MulDivCancelClass M₀
b a : M₀
ha : a ≠ 0
⊢ a * b / a = b
have rw : b * a / a = b
Tactic: rw [mul_comm, mul_div_cancel_right₀ _ ha]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Defs (goal)
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
inst_1 : Div M₀
inst_2 : MulDivCancelClass M₀
b a : M₀
ha : a ≠ 0
rw : b * a / a = b
⊢ a * b / a = b
have rw₁ : b = b
Tactic: rw [mul_comm, mul_div_cancel_right₀ _ ha]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Defs (goal)
Goal:
G₀ : Type u
M₀ : Type u_1
inst : GroupWithZero G₀
a_1 a b : G₀
hb : b ≠ 0
⊢ a * b / b = a
have rw : a * b * b⁻¹ = a
Tactic: rw [div_eq_mul_inv, mul_assoc, mul_inv_cancel₀ hb, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Defs (goal)
Goal:
G₀ : Type u
M₀ : Type u_1
inst : GroupWithZero G₀
a_1 a b : G₀
hb : b ≠ 0
rw : a * b * b⁻¹ = a
⊢ a * b / b = a
have rw₁ : a * (b * b⁻¹) = a
Tactic: rw [div_eq_mul_inv, mul_assoc, mul_inv_cancel₀ hb, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Defs (goal)
Goal:
G₀ : Type u
M₀ : Type u_1
inst : GroupWithZero G₀
a_1 a b : G₀
hb : b ≠ 0
rw : a * b * b⁻¹ = a
rw₁ : a * (b * b⁻¹) = a
⊢ a * b / b = a
have rw₂ : a * 1 = a
Tactic: rw [div_eq_mul_inv, mul_assoc, mul_inv_cancel₀ hb, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Defs (goal)
Goal:
G₀ : Type u
M₀ : Type u_1
inst : GroupWithZero G₀
a_1 a b : G₀
hb : b ≠ 0
rw : a * b * b⁻¹ = a
rw₁ : a * (b * b⁻¹) = a
rw₂ : a * 1 = a
⊢ a * b / b = a
have rw₃ : a = a
Tactic: rw [div_eq_mul_inv, mul_assoc, mul_inv_cancel₀ hb, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Defs (goal)
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
⊢ NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → ∀ (y : M₀), x * y = 0 → y = 0
have simp : (∀ {a b : M₀}, a * b = 0 → ¬a = 0 → b = 0) ↔ ∀ (x : M₀), x ≠ 0 → ∀ (y : M₀), x * y = 0 → y = 0
Tactic: simp only [noZeroDivisors_iff, or_iff_not_imp_left]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Defs (goal)
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
⊢ NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → ∀ (y : M₀), y * x = 0 → y = 0
have simp : (∀ {a b : M₀}, a * b = 0 → ¬b = 0 → a = 0) ↔ ∀ (x : M₀), x ≠ 0 → ∀ (y : M₀), y * x = 0 → y = 0
Tactic: simp only [noZeroDivisors_iff, or_iff_not_imp_right]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : SemigroupWithZero α
a : α
h : a = 0
⊢ 0 ∣ a
have rw : Dvd.dvd.{u_1} (α := α) 0 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : MonoidWithZero α
inst_1 : IsLeftCancelMulZero α
a b c : α
ha : a ≠ 0
d : α
⊢ a * c = a * b * d ↔ c = b * d
have rw : a * c = a * (b * d) ↔ c = b * d
Tactic: rw [mul_assoc, mul_right_inj' ha]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : MonoidWithZero α
inst_1 : IsLeftCancelMulZero α
a b c : α
ha : a ≠ 0
d : α
rw : a * c = a * (b * d) ↔ c = b * d
⊢ a * c = a * b * d ↔ c = b * d
have rw₁ : c = b * d ↔ c = b * d
Tactic: rw [mul_assoc, mul_right_inj' ha]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a b c : α
hc : c ≠ 0
d : α
⊢ b * c = a * c * d ↔ b = a * d
have rw : b * c = a * d * c ↔ b = a * d
Tactic: rw [mul_right_comm, mul_left_inj' hc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a b c : α
hc : c ≠ 0
d : α
rw : b * c = a * d * c ↔ b = a * d
⊢ b * c = a * c * d ↔ b = a * d
have rw₁ : b = a * d ↔ b = a * d
Tactic: rw [mul_right_comm, mul_left_inj' hc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ DvdNotUnit a b
have left : a ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
left : a ≠ 0
⊢ DvdNotUnit a b
have right : ∃ (x : α), ¬IsUnit x ∧ b = a * x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ ∃ (x : α), ¬IsUnit x ∧ b = a * x
have right : ∀ (c : α) (hnd : ¬a * c ∣ a), ∃ (x : α), ¬IsUnit x ∧ a * c = a * x
Tactic: rcases hd with ⟨c, rfl⟩
Cleared hypotheses: b, hd, hnd
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a c : α
hnd : ¬a * c ∣ a
⊢ ∃ (x : α), ¬IsUnit x ∧ a * c = a * x
have right : ¬IsUnit c
Tactic: refine ⟨c, ?_, rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : MonoidWithZero α
x y : α
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : α), ¬IsUnit z → z ≠ 0 → z ∣ x → ¬z ∣ y
⊢ IsRelPrime x y
have refine : ∀ (z : α) (hx : z ∣ x) (hy : z ∣ y) (h : ¬IsUnit z), z ≠ 0
Tactic: refine fun z hx hy ↦ by_contra fun h ↦ H z h ?_ hx hy
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
x y : α
h : x ∣ y ∧ ¬y ∣ x
d : α
hd : y = x * d
hyx : ¬y ∣ x
h_1 : d ∣ 1
e : α
he : 1 = d * e
⊢ x = y * e
have rw : x = x * d * e
Tactic: rw [hd, mul_assoc, ← he, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
x y : α
h : x ∣ y ∧ ¬y ∣ x
d : α
hd : y = x * d
hyx : ¬y ∣ x
h_1 : d ∣ 1
e : α
he : 1 = d * e
rw : x = x * d * e
⊢ x = y * e
have rw₁ : x = x * (d * e)
Tactic: rw [hd, mul_assoc, ← he, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
x y : α
h : x ∣ y ∧ ¬y ∣ x
d : α
hd : y = x * d
hyx : ¬y ∣ x
h_1 : d ∣ 1
e : α
he : 1 = d * e
rw : x = x * d * e
rw₁ : x = x * (d * e)
⊢ x = y * e
have rw₂ : x = x * 1
Tactic: rw [hd, mul_assoc, ← he, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
x y : α
h : x ∣ y ∧ ¬y ∣ x
d : α
hd : y = x * d
hyx : ¬y ∣ x
h_1 : d ∣ 1
e : α
he : 1 = d * e
rw : x = x * d * e
rw₁ : x = x * (d * e)
rw₂ : x = x * 1
⊢ x = y * e
have rw₃ : x = x
Tactic: rw [hd, mul_assoc, ← he, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
x y : α
h : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
h_1 : y ∣ x
e : α
he : x = y * e
| x * 1 = x * (d * e)
have lhs : x * 1
Tactic: lhs
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
x y : α
h : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
h_1 : y ∣ x
e : α
he : x = y * e
| x * 1
have rw : x * d * e * 1
Tactic: rw [he, hdx]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
x y : α
h : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
h_1 : y ∣ x
e : α
he : x = y * e
| x * d * e * 1
have simp : x * (d * e)
Tactic: simp [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
x y : α
h : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
h_1 : y ∣ x
e : α
he : x = y * e
| x * 1 = x * (d * e)
have rw : x * (d * e)
Tactic: lhs
            rw [he, hdx]
            simp [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
x y : α
h : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
h_1 : y ∣ x
e : α
he : x = y * e
⊢ x * 1 = x * (d * e)
have conv : x * 1 = x * (d * e)
Tactic: conv =>
            lhs
            rw [he, hdx]
            simp [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
x y : α
h : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
h_1 : y ∣ x
e : α
he : x = y * e
conv : x * 1 = x * (d * e)
⊢ x * 1 = x * (d * e)
have conv₁ : x * (d * e) = x * (d * e)
Tactic: conv =>
            lhs
            rw [he, hdx]
            simp [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : MonoidWithZero α
p q : α
h₁ : q ≠ 0
h₂ : p ∣ q
⊢ p ≠ 0
have rcases : ∀ (u : α) (h₁ : p * u ≠ 0), p ≠ 0
Tactic: rcases h₂ with ⟨u, rfl⟩
Cleared hypotheses: q, h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
m n : α
hm : IsPrimal m
hn : IsPrimal n
⊢ IsPrimal (m * n)
have inl : ∀ (hm : IsPrimal.{u_2} (α := α) 0), IsPrimal (0 * n)
Tactic: obtain rfl | h0 := eq_or_ne m 0
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
m n : α
hm : IsPrimal m
hn : IsPrimal n
inl : ∀ (hm : IsPrimal.{u_2} (α := α) 0), IsPrimal (0 * n)
⊢ IsPrimal (m * n)
have inr : ∀ (h0 : m ≠ 0), IsPrimal (m * n)
Tactic: obtain rfl | h0 := eq_or_ne m 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
m n : α
hm : IsPrimal m
hn : IsPrimal n
h0 : m ≠ 0
b c : α
h : m * n ∣ b * c
⊢ ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ b ∧ a₂ ∣ c ∧ m * n = a₁ * a₂
have inr : ∀ (a₁ a₂ b c : α) (hm : IsPrimal (a₁ * a₂)) (h0 : a₁ * a₂ ≠ 0) (h : a₁ * a₂ * n ∣ a₁ * b * (a₂ * c)),
  ∃ (a₁_1 : α), ∃ (a₂_1 : α), a₁_1 ∣ a₁ * b ∧ a₂_1 ∣ a₂ * c ∧ a₁ * a₂ * n = a₁_1 * a₂_1
Tactic: obtain ⟨a₁, a₂, ⟨b, rfl⟩, ⟨c, rfl⟩, rfl⟩ := hm (dvd_of_mul_right_dvd h)
Cleared hypotheses: m, hm, h0, b, c, h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (hypothesis)
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
n : α
hn : IsPrimal n
a₁ a₂ b c : α
hm : IsPrimal (a₁ * a₂)
h0 : a₁ * a₂ ≠ 0
h : a₁ * a₂ * n ∣ a₁ * b * (a₂ * c)
⊢ ∃ (a₁_1 : α), ∃ (a₂_1 : α), a₁_1 ∣ a₁ * b ∧ a₂_1 ∣ a₂ * c ∧ a₁ * a₂ * n = a₁_1 * a₂_1
have h₁ : n ∣ b * c
Tactic: rw [mul_mul_mul_comm, mul_dvd_mul_iff_left h0] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
n : α
hn : IsPrimal n
a₁ a₂ b c : α
hm : IsPrimal (a₁ * a₂)
h0 : a₁ * a₂ ≠ 0
h : n ∣ b * c
⊢ ∃ (a₁_1 : α), ∃ (a₂_1 : α), a₁_1 ∣ a₁ * b ∧ a₂_1 ∣ a₂ * c ∧ a₁ * a₂ * n = a₁_1 * a₂_1
have inr : ∀ (a₁' a₂' : α) (h₁ : a₁' ∣ b) (h₂ : a₂' ∣ c) (hn : IsPrimal (a₁' * a₂')) (h : a₁' * a₂' ∣ b * c),
  ∃ (a₁_1 : α), ∃ (a₂_1 : α), a₁_1 ∣ a₁ * b ∧ a₂_1 ∣ a₂ * c ∧ a₁ * a₂ * (a₁' * a₂') = a₁_1 * a₂_1
Tactic: obtain ⟨a₁', a₂', h₁, h₂, rfl⟩ := hn h
Cleared hypotheses: n, hn, h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
inst_2 : Subsingleton.{u_1 + 1} αˣ
c d : α
hcd : a = a * c * d
⊢ a = a * c
have hcd₁ : c = 1 ∧ d = 1 ∨ a = 0
Tactic: rw [mul_assoc, eq_comm, mul_right_eq_self₀, mul_eq_one] at hcd
Cleared hypotheses: hcd
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
inst_2 : Subsingleton.{u_1 + 1} αˣ
c d : α
hcd : c = 1 ∧ d = 1 ∨ a = 0
⊢ a = a * c
have inl : a = a * 1
Tactic: obtain ⟨rfl, -⟩ | rfl := hcd
Cleared hypotheses: c, hcd
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
inst_2 : Subsingleton.{u_1 + 1} αˣ
c d : α
hcd : c = 1 ∧ d = 1 ∨ a = 0
inl : a = a * 1
⊢ a = a * c
have inr : 0 = 0 * c
Tactic: obtain ⟨rfl, -⟩ | rfl := hcd
Cleared hypotheses: a, hcd
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
⊢ a ^ n ∣ a ^ m ↔ n ≤ m
have mp : a ^ n ∣ a ^ m → n ≤ m
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
mp : a ^ n ∣ a ^ m → n ≤ m
⊢ a ^ n ∣ a ^ m ↔ n ≤ m
have mpr : n ≤ m → a ^ n ∣ a ^ m
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
⊢ n ≤ m
have mp : ¬m < n
Tactic: rw [← not_lt]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
⊢ False
have mp : IsUnit a
Tactic: apply ha
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Divisibility (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
⊢ a ^ m * a ∣ a ^ m * 1
have rw : a ^ (m + 1) ∣ a ^ m
Tactic: rw [← pow_succ, mul_one]