awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Moebius (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
rw : HPow.hPow (α := ℤ) (-1) (factors a).card = -1
rw₁ : HPow.hPow (α := ℤ) (β := ℕ) (-1) 1 = -1
⊢ moebius a = -1
have rw₂ : Eq (α := ℤ) (-1) (-1)
Tactic: rw [ha.squarefree.moebius_eq, card_factors_of_irreducible ha, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Moebius (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
⊢ moebius (a * b) = moebius a * moebius b
have inl : Subsingleton α → moebius (a * b) = moebius a * moebius b
Tactic: rcases subsingleton_or_nontrivial α
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Moebius (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
inl : Subsingleton α → moebius (a * b) = moebius a * moebius b
⊢ moebius (a * b) = moebius a * moebius b
have inr : Nontrivial α → moebius (a * b) = moebius a * moebius b
Tactic: rcases subsingleton_or_nontrivial α
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Moebius (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h_1 : Subsingleton α
⊢ moebius (a * b) = moebius a * moebius b
have inl : moebius (1 * b) = moebius.{u_1} (α := α) 1 * moebius b
Tactic: rw [Subsingleton.elim a 1, moebius_one, one_mul, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Moebius (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h_1 : Subsingleton α
inl : moebius (1 * b) = moebius.{u_1} (α := α) 1 * moebius b
⊢ moebius (a * b) = moebius a * moebius b
have inl₁ : moebius (1 * b) = 1 * moebius b
Tactic: rw [Subsingleton.elim a 1, moebius_one, one_mul, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Moebius (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h_1 : Subsingleton α
inl : moebius (1 * b) = moebius.{u_1} (α := α) 1 * moebius b
inl₁ : moebius (1 * b) = 1 * moebius b
⊢ moebius (a * b) = moebius a * moebius b
have inl₂ : moebius b = 1 * moebius b
Tactic: rw [Subsingleton.elim a 1, moebius_one, one_mul, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Moebius (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h_1 : Subsingleton α
inl : moebius (1 * b) = moebius.{u_1} (α := α) 1 * moebius b
inl₁ : moebius (1 * b) = 1 * moebius b
inl₂ : moebius b = 1 * moebius b
⊢ moebius (a * b) = moebius a * moebius b
have inl₃ : moebius b = moebius b
Tactic: rw [Subsingleton.elim a 1, moebius_one, one_mul, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Moebius (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h_1 : Nontrivial α
⊢ moebius (a * b) = moebius a * moebius b
have pos : ∀ (ha : Squarefree a), moebius (a * b) = moebius a * moebius b
Tactic: by_cases ha : Squarefree a
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Moebius (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h_1 : Nontrivial α
pos : ∀ (ha : Squarefree a), moebius (a * b) = moebius a * moebius b
⊢ moebius (a * b) = moebius a * moebius b
have neg : ∀ (ha : ¬Squarefree a), moebius (a * b) = moebius a * moebius b
Tactic: by_cases ha : Squarefree a
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Moebius (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h_1 : Nontrivial α
ha : Squarefree a
⊢ moebius (a * b) = moebius a * moebius b
have pos : ∀ (hb : Squarefree b), moebius (a * b) = moebius a * moebius b
Tactic: by_cases hb : Squarefree b
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Moebius (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h_1 : Nontrivial α
ha : Squarefree a
pos : ∀ (hb : Squarefree b), moebius (a * b) = moebius a * moebius b
⊢ moebius (a * b) = moebius a * moebius b
have neg : ∀ (hb : ¬Squarefree b), moebius (a * b) = moebius a * moebius b
Tactic: by_cases hb : Squarefree b
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Moebius (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h_1 : Nontrivial α
ha : Squarefree a
hb : Squarefree b
⊢ moebius (a * b) = moebius a * moebius b
have hab : Squarefree (a * b)
Tactic: have hab : Squarefree (a * b) := squarefree_mul_iff.mpr ⟨h, ha, hb⟩
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Moebius (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h_1 : Nontrivial α
ha : Squarefree a
hb : Squarefree b
hab : Squarefree (a * b)
⊢ moebius (a * b) = moebius a * moebius b
have pos : HPow.hPow (α := ℤ) (-1) (factors (a * b)).card = moebius a * moebius b
Tactic: rw [hab.moebius_eq, Multiset.card_eq_card_of_rel (factors_mul ha.ne_zero hb.ne_zero),
    Multiset.card_add, pow_add, ha.moebius_eq, hb.moebius_eq]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Moebius (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h_1 : Nontrivial α
ha : Squarefree a
hb : Squarefree b
hab : Squarefree (a * b)
pos : HPow.hPow (α := ℤ) (-1) (factors (a * b)).card = moebius a * moebius b
⊢ moebius (a * b) = moebius a * moebius b
have pos₁ : HPow.hPow (α := ℤ) (-1) (factors a + factors b).card = moebius a * moebius b
Tactic: rw [hab.moebius_eq, Multiset.card_eq_card_of_rel (factors_mul ha.ne_zero hb.ne_zero),
    Multiset.card_add, pow_add, ha.moebius_eq, hb.moebius_eq]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Moebius (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h_1 : Nontrivial α
ha : Squarefree a
hb : Squarefree b
hab : Squarefree (a * b)
pos : HPow.hPow (α := ℤ) (-1) (factors (a * b)).card = moebius a * moebius b
pos₁ : HPow.hPow (α := ℤ) (-1) (factors a + factors b).card = moebius a * moebius b
⊢ moebius (a * b) = moebius a * moebius b
have pos₂ : HPow.hPow (α := ℤ) (-1) ((factors a).card + (factors b).card) = moebius a * moebius b
Tactic: rw [hab.moebius_eq, Multiset.card_eq_card_of_rel (factors_mul ha.ne_zero hb.ne_zero),
    Multiset.card_add, pow_add, ha.moebius_eq, hb.moebius_eq]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Moebius (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h_1 : Nontrivial α
ha : Squarefree a
hb : Squarefree b
hab : Squarefree (a * b)
pos : HPow.hPow (α := ℤ) (-1) (factors (a * b)).card = moebius a * moebius b
pos₁ : HPow.hPow (α := ℤ) (-1) (factors a + factors b).card = moebius a * moebius b
pos₂ : HPow.hPow (α := ℤ) (-1) ((factors a).card + (factors b).card) = moebius a * moebius b
⊢ moebius (a * b) = moebius a * moebius b
have pos₃ : HPow.hPow (α := ℤ) (-1) (factors a).card * HPow.hPow (α := ℤ) (-1) (factors b).card = moebius a * moebius b
Tactic: rw [hab.moebius_eq, Multiset.card_eq_card_of_rel (factors_mul ha.ne_zero hb.ne_zero),
    Multiset.card_add, pow_add, ha.moebius_eq, hb.moebius_eq]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Moebius (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h_1 : Nontrivial α
ha : Squarefree a
hb : Squarefree b
hab : Squarefree (a * b)
pos : HPow.hPow (α := ℤ) (-1) (factors (a * b)).card = moebius a * moebius b
pos₁ : HPow.hPow (α := ℤ) (-1) (factors a + factors b).card = moebius a * moebius b
pos₂ : HPow.hPow (α := ℤ) (-1) ((factors a).card + (factors b).card) = moebius a * moebius b
pos₃ : HPow.hPow (α := ℤ) (-1) (factors a).card * HPow.hPow (α := ℤ) (-1) (factors b).card = moebius a * moebius b
⊢ moebius (a * b) = moebius a * moebius b
have pos₄ : HPow.hPow (α := ℤ) (-1) (factors a).card * HPow.hPow (α := ℤ) (-1) (factors b).card =
  HPow.hPow (α := ℤ) (-1) (factors a).card * moebius b
Tactic: rw [hab.moebius_eq, Multiset.card_eq_card_of_rel (factors_mul ha.ne_zero hb.ne_zero),
    Multiset.card_add, pow_add, ha.moebius_eq, hb.moebius_eq]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Moebius (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h_1 : Nontrivial α
ha : Squarefree a
hb : Squarefree b
hab : Squarefree (a * b)
pos : HPow.hPow (α := ℤ) (-1) (factors (a * b)).card = moebius a * moebius b
pos₁ : HPow.hPow (α := ℤ) (-1) (factors a + factors b).card = moebius a * moebius b
pos₂ : HPow.hPow (α := ℤ) (-1) ((factors a).card + (factors b).card) = moebius a * moebius b
pos₃ : HPow.hPow (α := ℤ) (-1) (factors a).card * HPow.hPow (α := ℤ) (-1) (factors b).card = moebius a * moebius b
pos₄ :
  HPow.hPow (α := ℤ) (-1) (factors a).card * HPow.hPow (α := ℤ) (-1) (factors b).card =
    HPow.hPow (α := ℤ) (-1) (factors a).card * moebius b
⊢ moebius (a * b) = moebius a * moebius b
have pos₅ : HPow.hPow (α := ℤ) (-1) (factors a).card * HPow.hPow (α := ℤ) (-1) (factors b).card =
  HPow.hPow (α := ℤ) (-1) (factors a).card * HPow.hPow (α := ℤ) (-1) (factors b).card
Tactic: rw [hab.moebius_eq, Multiset.card_eq_card_of_rel (factors_mul ha.ne_zero hb.ne_zero),
    Multiset.card_add, pow_add, ha.moebius_eq, hb.moebius_eq]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq α
s : Finset α
i : α → ℕ
p : α
hps : p ∉ s
is_prime : ∀ q ∈ insert p s, Prime q
is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q'
⊢ IsRelPrime (p ^ i p) (∏ p' ∈ s, p' ^ i p')
have hp : Prime p
Tactic: have hp := is_prime _ (Finset.mem_insert_self _ _)
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq α
s : Finset α
i : α → ℕ
p : α
hps : p ∉ s
is_prime : ∀ q ∈ insert p s, Prime q
is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q'
hp : Prime p
⊢ IsRelPrime (p ^ i p) (∏ p' ∈ s, p' ^ i p')
have refine : ∀ ⦃d : α⦄, d ∣ p ^ i p → d ∣ ∏ p' ∈ s, p' ^ i p' → ¬Prime d
Tactic: refine (isRelPrime_iff_no_prime_factors <| pow_ne_zero _ hp.ne_zero).mpr ?_
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq α
s : Finset α
i : α → ℕ
p : α
hps : p ∉ s
is_prime : ∀ q ∈ insert p s, Prime q
is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q'
hp : Prime p
d : α
hdp : d ∣ p ^ i p
hdprod : d ∣ ∏ p' ∈ s, p' ^ i p'
hd : Prime d
⊢ False
have apply : p ∈ s
Tactic: apply hps
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq α
s : Finset α
i : α → ℕ
p : α
hps : p ∉ s
is_prime : ∀ q ∈ insert p s, Prime q
is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q'
hp : Prime p
d : α
hdp : d ∣ p ^ i p
hdprod : d ∣ ∏ p' ∈ s, p' ^ i p'
hd : Prime d
⊢ p ∈ s
have hdp₁ : d ∣ p
Tactic: replace hdp := hd.dvd_of_dvd_pow hdp
Cleared hypotheses: hdp
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq α
s : Finset α
i : α → ℕ
p : α
hps : p ∉ s
is_prime : ∀ q ∈ insert p s, Prime q
is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q'
hp : Prime p
d : α
hdprod : d ∣ ∏ p' ∈ s, p' ^ i p'
hd : Prime d
hdp : d ∣ p
⊢ p ∈ s
have obtain : ∀ (q : α) (q_mem' : Membership.mem (γ := Multiset α) (Multiset.map (fun (p' : α) ↦ p' ^ i p') s.val) q) (hdq : d ∣ q),
  p ∈ s
Tactic: obtain ⟨q, q_mem', hdq⟩ := hd.exists_mem_multiset_dvd hdprod
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq α
s : Finset α
i : α → ℕ
p : α
hps : p ∉ s
is_prime : ∀ q ∈ insert p s, Prime q
is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q'
hp : Prime p
d : α
hdprod : d ∣ ∏ p' ∈ s, p' ^ i p'
hd : Prime d
hdp : d ∣ p
q : α
q_mem' : Membership.mem (γ := Multiset α) (Multiset.map (fun (p' : α) ↦ p' ^ i p') s.val) q
hdq : d ∣ q
⊢ p ∈ s
have obtain : ∀ (q : α) (q_mem : q ∈ s.val)
  (q_mem' : Membership.mem (γ := Multiset α) (Multiset.map (fun (p' : α) ↦ p' ^ i p') s.val) (q ^ i q))
  (hdq : d ∣ q ^ i q), p ∈ s
Tactic: obtain ⟨q, q_mem, rfl⟩ := Multiset.mem_map.mp q_mem'
Cleared hypotheses: q, q_mem', hdq
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq α
s : Finset α
i : α → ℕ
p : α
hps : p ∉ s
is_prime : ∀ q ∈ insert p s, Prime q
is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q'
hp : Prime p
d : α
hdprod : d ∣ ∏ p' ∈ s, p' ^ i p'
hd : Prime d
hdp : d ∣ p
q : α
q_mem : q ∈ s.val
q_mem' : Membership.mem (γ := Multiset α) (Multiset.map (fun (p' : α) ↦ p' ^ i p') s.val) (q ^ i q)
hdq : d ∣ q ^ i q
⊢ p ∈ s
have hdq₁ : d ∣ q
Tactic: replace hdq := hd.dvd_of_dvd_pow hdq
Cleared hypotheses: hdq
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq α
s : Finset α
i : α → ℕ
p : α
hps : p ∉ s
is_prime : ∀ q ∈ insert p s, Prime q
is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q'
hp : Prime p
d : α
hdprod : d ∣ ∏ p' ∈ s, p' ^ i p'
hd : Prime d
hdp : d ∣ p
q : α
q_mem : q ∈ s.val
q_mem' : Membership.mem (γ := Multiset α) (Multiset.map (fun (p' : α) ↦ p' ^ i p') s.val) (q ^ i q)
hdq : d ∣ q
⊢ p ∈ s
have this : p ∣ q
Tactic: have : p ∣ q := dvd_trans (hd.irreducible.dvd_symm hp.irreducible hdp) hdq
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq α
s : Finset α
i : α → ℕ
p : α
hps : p ∉ s
is_prime : ∀ q ∈ insert p s, Prime q
is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q'
hp : Prime p
d : α
hdprod : d ∣ ∏ p' ∈ s, p' ^ i p'
hd : Prime d
hdp : d ∣ p
q : α
q_mem : q ∈ s.val
q_mem' : Membership.mem (γ := Multiset α) (Multiset.map (fun (p' : α) ↦ p' ^ i p') s.val) (q ^ i q)
hdq : d ∣ q
this : p ∣ q
⊢ p ∈ s
have a : p ∈ s ↔ q ∈ s.val
Tactic: convert! q_mem using 0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq α
s : Finset α
i : α → ℕ
p : α
hps : p ∉ s
is_prime : ∀ q ∈ insert p s, Prime q
is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q'
hp : Prime p
d : α
hdprod : d ∣ ∏ p' ∈ s, p' ^ i p'
hd : Prime d
hdp : d ∣ p
q : α
q_mem : q ∈ s.val
q_mem' : Membership.mem (γ := Multiset α) (Multiset.map (fun (p' : α) ↦ p' ^ i p') s.val) (q ^ i q)
hdq : d ∣ q
this : p ∣ q
⊢ p ∈ s ↔ q ∈ s.val
have a : p ∈ s ↔ q ∈ s
Tactic: rw [Finset.mem_val,
    is_coprime _ (Finset.mem_insert_self p s) _ (Finset.mem_insert_of_mem q_mem) this]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq α
s : Finset α
i : α → ℕ
p : α
hps : p ∉ s
is_prime : ∀ q ∈ insert p s, Prime q
is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q'
hp : Prime p
d : α
hdprod : d ∣ ∏ p' ∈ s, p' ^ i p'
hd : Prime d
hdp : d ∣ p
q : α
q_mem : q ∈ s.val
q_mem' : Membership.mem (γ := Multiset α) (Multiset.map (fun (p' : α) ↦ p' ^ i p') s.val) (q ^ i q)
hdq : d ∣ q
this : p ∣ q
a : p ∈ s ↔ q ∈ s
⊢ p ∈ s ↔ q ∈ s.val
have a₁ : q ∈ s ↔ q ∈ s
Tactic: rw [Finset.mem_val,
    is_coprime _ (Finset.mem_insert_self p s) _ (Finset.mem_insert_of_mem q_mem) this]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
P : α → Prop
i : α → ℕ
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this : DecidableEq α := Classical.decEq α
p : α
f' : Finset α
hpf' : p ∉ f'
ih : ∀ (is_prime : ∀ p ∈ f', Prime p) (is_coprime : ∀ p ∈ f', ∀ q ∈ f', p ∣ q → p = q), P (∏ p ∈ f', p ^ i p)
is_prime : ∀ p_1 ∈ insert p f', Prime p_1
is_coprime : ∀ p_1 ∈ insert p f', ∀ q ∈ insert p f', p_1 ∣ q → p_1 = q
⊢ P (∏ p ∈ insert p f', p ^ i p)
have insert : P (p ^ i p * ∏ x ∈ f', x ^ i x)
Tactic: rw [Finset.prod_insert hpf']
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
P : α → Prop
s : Finset α
i : α → ℕ
is_prime : ∀ p ∈ s, Prime p
is_coprime : ∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this : DecidableEq α := Classical.decEq α
⊢ P (∏ p ∈ s, p ^ i p)
have empty : ∀ (is_prime : ∀ (p : α), Membership.mem (γ := Finset α) ∅ p → Prime p)
  (is_coprime :
    ∀ (p : α), Membership.mem (γ := Finset α) ∅ p → ∀ (q : α), Membership.mem (γ := Finset α) ∅ q → p ∣ q → p = q),
  P (∏ p ∈ ∅, p ^ i p)
Tactic: induction s using Finset.induction_on with
  | empty => simpa using h1 isUnit_one
  | insert p f' hpf' ih =>
    rw [Finset.prod_insert hpf']
    exact
      hcp (prime_pow_coprime_prod_of_coprime_insert i p hpf' is_prime is_coprime)
        (hpr (i p) (is_prime _ (Finset.mem_insert_self _ _)))
        (ih (fun q hq => is_prime _ (Finset.mem_insert_of_mem hq)) fun q hq q' hq' =>
          is_coprime _ (Finset.mem_insert_of_mem hq) _ (Finset.mem_insert_of_mem hq'))
Cleared hypotheses: s, is_prime, is_coprime
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
P : α → Prop
s : Finset α
i : α → ℕ
is_prime : ∀ p ∈ s, Prime p
is_coprime : ∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this : DecidableEq α := Classical.decEq α
empty :
  ∀ (is_prime : ∀ (p : α), Membership.mem (γ := Finset α) ∅ p → Prime p)
    (is_coprime :
      ∀ (p : α), Membership.mem (γ := Finset α) ∅ p → ∀ (q : α), Membership.mem (γ := Finset α) ∅ q → p ∣ q → p = q),
    P (∏ p ∈ ∅, p ^ i p)
⊢ P (∏ p ∈ s, p ^ i p)
have insert : ∀ (p : α) (f' : Finset α) (hpf' : p ∉ f')
  (ih : ∀ (is_prime : ∀ p ∈ f', Prime p) (is_coprime : ∀ p ∈ f', ∀ q ∈ f', p ∣ q → p = q), P (∏ p ∈ f', p ^ i p))
  (is_prime : ∀ p_1 ∈ insert p f', Prime p_1) (is_coprime : ∀ p_1 ∈ insert p f', ∀ q ∈ insert p f', p_1 ∣ q → p_1 = q),
  P (∏ p ∈ insert p f', p ^ i p)
Tactic: induction s using Finset.induction_on with
  | empty => simpa using h1 isUnit_one
  | insert p f' hpf' ih =>
    rw [Finset.prod_insert hpf']
    exact
      hcp (prime_pow_coprime_prod_of_coprime_insert i p hpf' is_prime is_coprime)
        (hpr (i p) (is_prime _ (Finset.mem_insert_self _ _)))
        (ih (fun q hq => is_prime _ (Finset.mem_insert_of_mem hq)) fun q hq q' hq' =>
          is_coprime _ (Finset.mem_insert_of_mem hq) _ (Finset.mem_insert_of_mem hq'))
Cleared hypotheses: s, is_prime, is_coprime
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this : DecidableEq α := Classical.decEq α
⊢ P a
have P_of_associated : ∀ {x y : α}, Associated x y → P x → P y
Tactic: have P_of_associated : ∀ {x y}, Associated x y → P x → P y := by
    rintro x y ⟨u, rfl⟩ hx
    exact hcp (fun p _ hpx => isUnit_of_dvd_unit hpx u.isUnit) hx (h1 u.isUnit)
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, Associated x y → P x → P y
⊢ P a
have pos : ∀ (ha0 : a = 0), P a
Tactic: by_cases ha0 : a = 0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, Associated x y → P x → P y
pos : ∀ (ha0 : a = 0), P a
⊢ P a
have neg : ∀ (ha0 : ¬a = 0), P a
Tactic: by_cases ha0 : a = 0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, Associated x y → P x → P y
ha0 : ¬a = 0
⊢ P a
have this₁ : Nontrivial α
Tactic: haveI : Nontrivial α := ⟨⟨_, _, ha0⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this_1 : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, Associated x y → P x → P y
ha0 : ¬a = 0
this_2 : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ P a
have neg : P (normalizedFactors a).prod
Tactic: refine P_of_associated (prod_normalizedFactors ha0) ?_
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this_1 : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, Associated x y → P x → P y
ha0 : ¬a = 0
this_2 : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ P (normalizedFactors a).prod
have neg : P (∏ m ∈ (normalizedFactors a).toFinset, id m ^ Multiset.count m (normalizedFactors a))
Tactic: rw [← (normalizedFactors a).map_id, Finset.prod_multiset_map_count]