awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
hp : Prime p
a b c : M
hc : p * b = a * c
inl : ∀ (h : p ∣ a), p ∣ a ∨ a ∣ b
⊢ p ∣ a ∨ a ∣ b
have inr : ∀ (x : M) (hc : p * b = a * (p * x)), p ∣ a ∨ a ∣ b
Tactic: rcases hp.2.2 a c (hc ▸ dvd_mul_right _ _) with (h | ⟨x, rfl⟩)
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (hypothesis)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
hp : Prime p
a b x : M
hc : p * b = a * (p * x)
⊢ p ∣ a ∨ a ∣ b
have hc₁ : b = a * x
Tactic: rw [mul_left_comm, mul_right_inj' hp.ne_zero] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a b : M
hp : Prime p
h : ¬p ∣ a
h' : HPow.hPow (β := ℕ) p 0 ∣ a * b
⊢ HPow.hPow (β := ℕ) p 0 ∣ b
have zero : 1 ∣ b
Tactic: rw [pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a b : M
hp : Prime p
h : ¬p ∣ a
n : ℕ
ih : ∀ (h' : p ^ n ∣ a * b), p ^ n ∣ b
h' : p ^ (n + 1) ∣ a * b
⊢ p ^ (n + 1) ∣ b
have succ : ∀ (c : M) (ih : ∀ (h' : p ^ n ∣ a * (p ^ n * c)), p ^ n ∣ p ^ n * c) (h' : p ^ (n + 1) ∣ a * (p ^ n * c)),
  p ^ (n + 1) ∣ p ^ n * c
Tactic: obtain ⟨c, rfl⟩ := ih (dvd_trans (pow_dvd_pow p n.le_succ) h')
Cleared hypotheses: b, ih, h'
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a : M
hp : Prime p
h : ¬p ∣ a
n : ℕ
c : M
ih : ∀ (h' : p ^ n ∣ a * (p ^ n * c)), p ^ n ∣ p ^ n * c
h' : p ^ (n + 1) ∣ a * (p ^ n * c)
⊢ p ^ (n + 1) ∣ p ^ n * c
have succ : p ^ n * p ∣ p ^ n * c
Tactic: rw [pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a : M
hp : Prime p
h : ¬p ∣ a
n : ℕ
c : M
ih : ∀ (h' : p ^ n ∣ a * (p ^ n * c)), p ^ n ∣ p ^ n * c
h' : p ^ (n + 1) ∣ a * (p ^ n * c)
⊢ p ^ n * p ∣ p ^ n * c
have apply : p ∣ a * c
Tactic: apply mul_dvd_mul_left _ ((hp.dvd_or_dvd _).resolve_left h)
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a : M
hp : Prime p
h : ¬p ∣ a
n : ℕ
c : M
ih : ∀ (h' : p ^ n ∣ a * (p ^ n * c)), p ^ n ∣ p ^ n * c
h' : p ^ (n + 1) ∣ a * (p ^ n * c)
⊢ p ∣ a * c
have rwa : p ^ n * p ∣ p ^ n * (a * c)
Tactic: rwa [← mul_dvd_mul_iff_left (pow_ne_zero n hp.ne_zero), ← pow_succ, mul_left_comm]
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a : M
hp : Prime p
h : ¬p ∣ a
n : ℕ
c : M
ih : ∀ (h' : p ^ n ∣ a * (p ^ n * c)), p ^ n ∣ p ^ n * c
h' : p ^ (n + 1) ∣ a * (p ^ n * c)
rwa : p ^ n * p ∣ p ^ n * (a * c)
⊢ p ∣ a * c
have rwa₁ : p ^ (n + 1) ∣ p ^ n * (a * c)
Tactic: rwa [← mul_dvd_mul_iff_left (pow_ne_zero n hp.ne_zero), ← pow_succ, mul_left_comm]
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a b : M
hp : Prime p
n : ℕ
h : ¬p ∣ a
h' : p ^ n ∣ a * b
⊢ p ^ n ∣ b
have zero : ∀ (h' : HPow.hPow (β := ℕ) p 0 ∣ a * b), HPow.hPow (β := ℕ) p 0 ∣ b
Tactic: induction n with
  | zero =>
    rw [pow_zero]
    exact one_dvd b
  | succ n ih =>
    obtain ⟨c, rfl⟩ := ih (dvd_trans (pow_dvd_pow p n.le_succ) h')
    rw [pow_succ]
    apply mul_dvd_mul_left _ ((hp.dvd_or_dvd _).resolve_left h)
    rwa [← mul_dvd_mul_iff_left (pow_ne_zero n hp.ne_zero), ← pow_succ, mul_left_comm]
Cleared hypotheses: n, h'
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a b : M
hp : Prime p
n : ℕ
h : ¬p ∣ a
h' : p ^ n ∣ a * b
zero : ∀ (h' : HPow.hPow (β := ℕ) p 0 ∣ a * b), HPow.hPow (β := ℕ) p 0 ∣ b
⊢ p ^ n ∣ b
have succ : ∀ (n : ℕ) (ih : ∀ (h' : p ^ n ∣ a * b), p ^ n ∣ b) (h' : p ^ (n + 1) ∣ a * b), p ^ (n + 1) ∣ b
Tactic: induction n with
  | zero =>
    rw [pow_zero]
    exact one_dvd b
  | succ n ih =>
    obtain ⟨c, rfl⟩ := ih (dvd_trans (pow_dvd_pow p n.le_succ) h')
    rw [pow_succ]
    apply mul_dvd_mul_left _ ((hp.dvd_or_dvd _).resolve_left h)
    rwa [← mul_dvd_mul_iff_left (pow_ne_zero n hp.ne_zero), ← pow_succ, mul_left_comm]
Cleared hypotheses: n, h'
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (hypothesis)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a b : M
hp : Prime p
n : ℕ
h : ¬p ∣ b
h' : p ^ n ∣ a * b
⊢ p ^ n ∣ a
have h'₁ : p ^ n ∣ b * a
Tactic: rw [mul_comm] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a b : M
n : ℕ
hp : Prime p
hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n
hb : ¬HPow.hPow (β := ℕ) p 2 ∣ b
⊢ p ∣ a
have inl : ∀ (H : p ∣ a ^ n.succ), p ∣ a
Tactic: rcases hp.dvd_or_dvd ((dvd_pow_self p (Nat.succ_ne_zero n)).trans hpow) with H | hbdiv
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a b : M
n : ℕ
hp : Prime p
hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n
hb : ¬HPow.hPow (β := ℕ) p 2 ∣ b
inl : ∀ (H : p ∣ a ^ n.succ), p ∣ a
⊢ p ∣ a
have inr : ∀ (hbdiv : p ∣ b ^ n), p ∣ a
Tactic: rcases hp.dvd_or_dvd ((dvd_pow_self p (Nat.succ_ne_zero n)).trans hpow) with H | hbdiv
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a b : M
n : ℕ
hp : Prime p
hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n
hb : ¬HPow.hPow (β := ℕ) p 2 ∣ b
hbdiv : p ∣ b ^ n
⊢ p ∣ a
have inr : ∀ (x : M) (hpow : p ^ n.succ ∣ a ^ n.succ * (p * x) ^ n) (hb : ¬HPow.hPow (β := ℕ) p 2 ∣ p * x)
  (hbdiv : p ∣ (p * x) ^ n), p ∣ a
Tactic: obtain ⟨x, rfl⟩ := hp.dvd_of_dvd_pow hbdiv
Cleared hypotheses: b, hpow, hb, hbdiv
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
x : M
hpow : p ^ n.succ ∣ a ^ n.succ * (p * x) ^ n
hb : ¬HPow.hPow (β := ℕ) p 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
⊢ p ∣ a
have inr : ∀ (y : M) (hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y), p ∣ a
Tactic: obtain ⟨y, hy⟩ := hpow
Cleared hypotheses: hpow
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬HPow.hPow (β := ℕ) p 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
⊢ a ^ n.succ * x ^ n = p * y
have refine : p ^ n * (a ^ n.succ * x ^ n) = p ^ n * (p * y)
Tactic: refine mul_left_cancel₀ (pow_ne_zero n hp.ne_zero) ?_
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬HPow.hPow (β := ℕ) p 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
⊢ p ^ n * (a ^ n.succ * x ^ n) = p ^ n * (p * y)
have rw : p ^ n * (a ^ n.succ * x ^ n) = p ^ n * p * y
Tactic: rw [← mul_assoc _ p, ← pow_succ, ← hy, mul_pow, ← mul_assoc (a ^ n.succ), mul_comm _ (p ^ n),
      mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬HPow.hPow (β := ℕ) p 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
rw : p ^ n * (a ^ n.succ * x ^ n) = p ^ n * p * y
⊢ p ^ n * (a ^ n.succ * x ^ n) = p ^ n * (p * y)
have rw₁ : p ^ n * (a ^ n.succ * x ^ n) = p ^ (n + 1) * y
Tactic: rw [← mul_assoc _ p, ← pow_succ, ← hy, mul_pow, ← mul_assoc (a ^ n.succ), mul_comm _ (p ^ n),
      mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬HPow.hPow (β := ℕ) p 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
rw : p ^ n * (a ^ n.succ * x ^ n) = p ^ n * p * y
rw₁ : p ^ n * (a ^ n.succ * x ^ n) = p ^ (n + 1) * y
⊢ p ^ n * (a ^ n.succ * x ^ n) = p ^ n * (p * y)
have rw₂ : p ^ n * (a ^ n.succ * x ^ n) = a ^ n.succ * (p * x) ^ n
Tactic: rw [← mul_assoc _ p, ← pow_succ, ← hy, mul_pow, ← mul_assoc (a ^ n.succ), mul_comm _ (p ^ n),
      mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬HPow.hPow (β := ℕ) p 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
rw : p ^ n * (a ^ n.succ * x ^ n) = p ^ n * p * y
rw₁ : p ^ n * (a ^ n.succ * x ^ n) = p ^ (n + 1) * y
rw₂ : p ^ n * (a ^ n.succ * x ^ n) = a ^ n.succ * (p * x) ^ n
⊢ p ^ n * (a ^ n.succ * x ^ n) = p ^ n * (p * y)
have rw₃ : p ^ n * (a ^ n.succ * x ^ n) = a ^ n.succ * (p ^ n * x ^ n)
Tactic: rw [← mul_assoc _ p, ← pow_succ, ← hy, mul_pow, ← mul_assoc (a ^ n.succ), mul_comm _ (p ^ n),
      mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬HPow.hPow (β := ℕ) p 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
rw : p ^ n * (a ^ n.succ * x ^ n) = p ^ n * p * y
rw₁ : p ^ n * (a ^ n.succ * x ^ n) = p ^ (n + 1) * y
rw₂ : p ^ n * (a ^ n.succ * x ^ n) = a ^ n.succ * (p * x) ^ n
rw₃ : p ^ n * (a ^ n.succ * x ^ n) = a ^ n.succ * (p ^ n * x ^ n)
⊢ p ^ n * (a ^ n.succ * x ^ n) = p ^ n * (p * y)
have rw₄ : p ^ n * (a ^ n.succ * x ^ n) = a ^ n.succ * p ^ n * x ^ n
Tactic: rw [← mul_assoc _ p, ← pow_succ, ← hy, mul_pow, ← mul_assoc (a ^ n.succ), mul_comm _ (p ^ n),
      mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬HPow.hPow (β := ℕ) p 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
rw : p ^ n * (a ^ n.succ * x ^ n) = p ^ n * p * y
rw₁ : p ^ n * (a ^ n.succ * x ^ n) = p ^ (n + 1) * y
rw₂ : p ^ n * (a ^ n.succ * x ^ n) = a ^ n.succ * (p * x) ^ n
rw₃ : p ^ n * (a ^ n.succ * x ^ n) = a ^ n.succ * (p ^ n * x ^ n)
rw₄ : p ^ n * (a ^ n.succ * x ^ n) = a ^ n.succ * p ^ n * x ^ n
⊢ p ^ n * (a ^ n.succ * x ^ n) = p ^ n * (p * y)
have rw₅ : p ^ n * (a ^ n.succ * x ^ n) = p ^ n * a ^ n.succ * x ^ n
Tactic: rw [← mul_assoc _ p, ← pow_succ, ← hy, mul_pow, ← mul_assoc (a ^ n.succ), mul_comm _ (p ^ n),
      mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬HPow.hPow (β := ℕ) p 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
rw : p ^ n * (a ^ n.succ * x ^ n) = p ^ n * p * y
rw₁ : p ^ n * (a ^ n.succ * x ^ n) = p ^ (n + 1) * y
rw₂ : p ^ n * (a ^ n.succ * x ^ n) = a ^ n.succ * (p * x) ^ n
rw₃ : p ^ n * (a ^ n.succ * x ^ n) = a ^ n.succ * (p ^ n * x ^ n)
rw₄ : p ^ n * (a ^ n.succ * x ^ n) = a ^ n.succ * p ^ n * x ^ n
rw₅ : p ^ n * (a ^ n.succ * x ^ n) = p ^ n * a ^ n.succ * x ^ n
⊢ p ^ n * (a ^ n.succ * x ^ n) = p ^ n * (p * y)
have rw₆ : p ^ n * (a ^ n.succ * x ^ n) = p ^ n * (a ^ n.succ * x ^ n)
Tactic: rw [← mul_assoc _ p, ← pow_succ, ← hy, mul_pow, ← mul_assoc (a ^ n.succ), mul_comm _ (p ^ n),
      mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (hypothesis)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬HPow.hPow (β := ℕ) p 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
⊢ p ∣ a
have this : a ^ n.succ * x ^ n = p * y
Tactic: have : a ^ n.succ * x ^ n = p * y := by
    refine mul_left_cancel₀ (pow_ne_zero n hp.ne_zero) ?_
    rw [← mul_assoc _ p, ← pow_succ, ← hy, mul_pow, ← mul_assoc (a ^ n.succ), mul_comm _ (p ^ n),
      mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬HPow.hPow (β := ℕ) p 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
this : a ^ n.succ * x ^ n = p * y
⊢ p ∣ a
have inr : ∀ (hdvdx : p ∣ x ^ n), HPow.hPow (β := ℕ) p 2 ∣ p * x
Tactic: refine hp.dvd_of_dvd_pow ((hp.dvd_or_dvd ⟨_, this⟩).resolve_right fun hdvdx => hb ?_)
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬HPow.hPow (β := ℕ) p 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
this : a ^ n.succ * x ^ n = p * y
hdvdx : p ∣ x ^ n
⊢ HPow.hPow (β := ℕ) p 2 ∣ p * x
have inr : ∀ (z : M) (hb : ¬HPow.hPow (β := ℕ) p 2 ∣ p * (p * z)) (hbdiv : p ∣ (p * (p * z)) ^ n)
  (hy : a ^ n.succ * (p * (p * z)) ^ n = p ^ n.succ * y) (this : a ^ n.succ * (p * z) ^ n = p * y)
  (hdvdx : p ∣ (p * z) ^ n), HPow.hPow (β := ℕ) p 2 ∣ p * (p * z)
Tactic: obtain ⟨z, rfl⟩ := hp.dvd_of_dvd_pow hdvdx
Cleared hypotheses: x, hb, hbdiv, hy, this, hdvdx
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
y z : M
hb : ¬HPow.hPow (β := ℕ) p 2 ∣ p * (p * z)
hbdiv : p ∣ (p * (p * z)) ^ n
hy : a ^ n.succ * (p * (p * z)) ^ n = p ^ n.succ * y
this : a ^ n.succ * (p * z) ^ n = p * y
hdvdx : p ∣ (p * z) ^ n
⊢ HPow.hPow (β := ℕ) p 2 ∣ p * (p * z)
have inr : p * p ∣ p * p * z
Tactic: rw [pow_two, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p x y : M
h : Prime p
i : ℕ
hxy : p ^ (i + 1) ∣ x * y
⊢ p ^ (i + 1) ∣ x ∨ p ∣ y
have rw : ¬p ∣ y → p ^ (i + 1) ∣ x
Tactic: rw [or_iff_not_imp_right]
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
hp : Prime p
a b : M
k l : ℕ
h_1 : p ^ k ∣ a
h_2 : p ^ l ∣ b
h_3 : p ^ (k + l + 1) ∣ a * b
x : M
hx : a = p ^ k * x
y : M
hy : b = p ^ l * y
z : M
hz : a * b = p ^ (k + l + 1) * z
h : p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z)
hp0 : p ^ (k + l) ≠ 0
⊢ x * y = p * z
have rwa : ∀ (h : x * y = p * z) (hp0 : p ^ (k + l) ≠ 0), x * y = p * z
Tactic: rwa [mul_right_inj' hp0] at h
Cleared hypotheses: h, hp0
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p q : M
h : DvdNotUnit p q
hq : Irreducible q
⊢ IsUnit p
have obtain : p ≠ 0 → ∀ (x : M) (hx : ¬IsUnit x) (hx' : q = p * x), IsUnit p
Tactic: obtain ⟨_, x, hx, hx'⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p q : M
hp : DvdNotUnit p q
⊢ ¬IsUnit q
have obtain : ∀ (x : M) (hx : ¬IsUnit x), ¬IsUnit (p * x)
Tactic: obtain ⟨-, x, hx, rfl⟩ := hp
Cleared hypotheses: q, hp
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p q : M
h : DvdNotUnit p q
hcontra : p = q
⊢ False
have obtain : ∀ (hp : p ≠ 0) (x : M) (hx' : ¬IsUnit x) (hx'' : q = p * x), False
Tactic: obtain ⟨hp, x, hx', hx''⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
q : M
hq : ¬IsUnit q
hq' : q ≠ 0
⊢ Function.Injective.{1, u_1 + 1} (β := M) fun (n : ℕ) ↦ q ^ n
have refine_1 : ∀ (n m : ℕ) (h : n < m), ¬IsUnit (q ^ (m - n))
Tactic: refine .of_lt_imp_ne fun n m h => DvdNotUnit.ne ⟨pow_ne_zero n hq', q ^ (m - n), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Prime.Lemmas (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
q : M
hq : ¬IsUnit q
hq' : q ≠ 0
refine_1 : ∀ (n m : ℕ) (h : n < m), ¬IsUnit (q ^ (m - n))
⊢ Function.Injective.{1, u_1 + 1} (β := M) fun (n : ℕ) ↦ q ^ n
have refine_2 : ∀ (n m : ℕ) (h : n < m), q ^ m = q ^ n * q ^ (m - n)
Tactic: refine .of_lt_imp_ne fun n m h => DvdNotUnit.ne ⟨pow_ne_zero n hq', q ^ (m - n), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommSemiring R
⊢ HMul.hMul (α := QuadraticAlgebra R a b) ω ω = { re := a, im := b }
have re : (HMul.hMul (α := QuadraticAlgebra R a b) ω ω).re = re (a := a) (b := b) { re := a, im := b }
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommSemiring R
re : (HMul.hMul (α := QuadraticAlgebra R a b) ω ω).re = QuadraticAlgebra.re (a := a) (b := b) { re := a, im := b }
⊢ HMul.hMul (α := QuadraticAlgebra R a b) ω ω = { re := a, im := b }
have im : (HMul.hMul (α := QuadraticAlgebra R a b) ω ω).im = im (a := a) (b := b) { re := a, im := b }
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommSemiring R
⊢ HMul.hMul (α := QuadraticAlgebra R a b) ω ω =
    HSMul.hSMul (β := QuadraticAlgebra R a b) a 1 + HSMul.hSMul (β := QuadraticAlgebra R a b) b ω
have re : (HMul.hMul (α := QuadraticAlgebra R a b) ω ω).re =
  (HSMul.hSMul (β := QuadraticAlgebra R a b) a 1 + HSMul.hSMul (β := QuadraticAlgebra R a b) b ω).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommSemiring R
re :
  (HMul.hMul (α := QuadraticAlgebra R a b) ω ω).re =
    (HSMul.hSMul (β := QuadraticAlgebra R a b) a 1 + HSMul.hSMul (β := QuadraticAlgebra R a b) b ω).re
⊢ HMul.hMul (α := QuadraticAlgebra R a b) ω ω =
    HSMul.hSMul (β := QuadraticAlgebra R a b) a 1 + HSMul.hSMul (β := QuadraticAlgebra R a b) b ω
have im : (HMul.hMul (α := QuadraticAlgebra R a b) ω ω).im =
  (HSMul.hSMul (β := QuadraticAlgebra R a b) a 1 + HSMul.hSMul (β := QuadraticAlgebra R a b) b ω).im
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommSemiring R
x y : R
⊢ HMul.hMul (α := QuadraticAlgebra R a b) ω { re := x, im := y : QuadraticAlgebra R a b } =
    { re := a * y, im := x + b * y }
have re : (HMul.hMul (α := QuadraticAlgebra R a b) ω { re := x, im := y : QuadraticAlgebra R a b }).re =
  re (a := a) (b := b) { re := a * y, im := x + b * y }
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommSemiring R
x y : R
re :
  (HMul.hMul (α := QuadraticAlgebra R a b) ω { re := x, im := y : QuadraticAlgebra R a b }).re =
    QuadraticAlgebra.re (a := a) (b := b) { re := a * y, im := x + b * y }
⊢ HMul.hMul (α := QuadraticAlgebra R a b) ω { re := x, im := y : QuadraticAlgebra R a b } =
    { re := a * y, im := x + b * y }
have im : (HMul.hMul (α := QuadraticAlgebra R a b) ω { re := x, im := y : QuadraticAlgebra R a b }).im =
  im (a := a) (b := b) { re := a * y, im := x + b * y }
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommSemiring R
n x y : R
⊢ HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b) (ω : QuadraticAlgebra R a b)
        ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) n : QuadraticAlgebra R a b) *
      { re := x, im := y : QuadraticAlgebra R a b } =
    { re := a * n * y, im := n * x + n * b * y }
have re : (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b) (ω : QuadraticAlgebra R a b)
        ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) n : QuadraticAlgebra R a b) *
      { re := x, im := y : QuadraticAlgebra R a b }).re =
  re (a := a) (b := b) { re := a * n * y, im := n * x + n * b * y }
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommSemiring R
n x y : R
re :
  (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b) (ω : QuadraticAlgebra R a b)
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) n : QuadraticAlgebra R a b) *
        { re := x, im := y : QuadraticAlgebra R a b }).re =
    QuadraticAlgebra.re (a := a) (b := b) { re := a * n * y, im := n * x + n * b * y }
⊢ HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b) (ω : QuadraticAlgebra R a b)
        ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) n : QuadraticAlgebra R a b) *
      { re := x, im := y : QuadraticAlgebra R a b } =
    { re := a * n * y, im := n * x + n * b * y }
have im : (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b) (ω : QuadraticAlgebra R a b)
        ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) n : QuadraticAlgebra R a b) *
      { re := x, im := y : QuadraticAlgebra R a b }).im =
  im (a := a) (b := b) { re := a * n * y, im := n * x + n * b * y }
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommSemiring R
n x y : R
⊢ (HMul.hMul (α := QuadraticAlgebra R a b) (β := QuadraticAlgebra R a b) (ω : QuadraticAlgebra R a b)
          ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) n : QuadraticAlgebra R a b) *
        { re := x, im := y : QuadraticAlgebra R a b }).im =
    im (a := a) (b := b) { re := a * n * y, im := n * x + n * b * y }
have im : n * x + b * n * y = n * x + n * b * y
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommSemiring R
x y : R
⊢ { re := x, im := y } =
    HAdd.hAdd (α := QuadraticAlgebra R a b)
      ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b)
      (HSMul.hSMul (β := QuadraticAlgebra R a b) y ω)
have re : re (a := a) (b := b) { re := x, im := y : QuadraticAlgebra R a b } =
  (HAdd.hAdd (α := QuadraticAlgebra R a b)
      ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b)
      (HSMul.hSMul (β := QuadraticAlgebra R a b) y ω)).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommSemiring R
x y : R
re :
  QuadraticAlgebra.re (a := a) (b := b) { re := x, im := y : QuadraticAlgebra R a b } =
    (HAdd.hAdd (α := QuadraticAlgebra R a b)
        ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b)
        (HSMul.hSMul (β := QuadraticAlgebra R a b) y ω)).re
⊢ { re := x, im := y } =
    HAdd.hAdd (α := QuadraticAlgebra R a b)
      ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b)
      (HSMul.hSMul (β := QuadraticAlgebra R a b) y ω)
have im : im (a := a) (b := b) { re := x, im := y : QuadraticAlgebra R a b } =
  (HAdd.hAdd (α := QuadraticAlgebra R a b)
      ((algebraMap R (QuadraticAlgebra R a b) : (a_1 : R) → QuadraticAlgebra R a b) x : QuadraticAlgebra R a b)
      (HSMul.hSMul (β := QuadraticAlgebra R a b) y ω)).im
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.Basic (goal)
Goal:
R : Type u_2
a b : R
inst : CommSemiring R
A : Type u_3
inst_1 : Ring A
inst_2 : Algebra R A
f g : QuadraticAlgebra R a b →ₐ[R] A
h : Eq.{u_3 + 1} (α := A) ((f : (a : QuadraticAlgebra R a b) → A) ω : A) ((g : (a : QuadraticAlgebra R a b) → A) ω : A)
⊢ f = g
have H : ∀ (x y : R),
  Eq.{u_3 + 1} (α := A) ((f : (a : QuadraticAlgebra R a b) → A) { re := x, im := y } : A)
    ((g : (a : QuadraticAlgebra R a b) → A) { re := x, im := y } : A)
Tactic: ext ⟨x, y⟩