awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
⊢ Eq (α := Multiset α) (Multiset.map (⇑normalize : (a : α) → α) (factors a))
    (Multiset.map (⇑normalize : (a : α) → α) (factors b))
have h' : Eq.{u_1 + 1} (α := (a : α) → α) (⇑normalize : (a : α) → α)
  (Function.comp (β := Associates α) Associates.out Associates.mk)
Tactic: have h' : ⇑(normalize (α := α)) = Associates.out ∘ Associates.mk := funext Associates.out_mk
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
h' :
  Eq.{u_1 + 1} (α := (a : α) → α) (⇑normalize : (a : α) → α)
    (Function.comp (β := Associates α) Associates.out Associates.mk)
⊢ Eq (α := Multiset α) (Multiset.map (⇑normalize : (a : α) → α) (factors a))
    (Multiset.map (⇑normalize : (a : α) → α) (factors b))
have rw : Multiset.map (Function.comp (β := Associates α) Associates.out Associates.mk) (factors a) =
  Multiset.map (Function.comp (β := Associates α) Associates.out Associates.mk) (factors b)
Tactic: rw [h', ← Multiset.map_map, ← Multiset.map_map,
    Associates.rel_associated_iff_map_eq_map.mp (factors_rel_of_associated h)]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
h' :
  Eq.{u_1 + 1} (α := (a : α) → α) (⇑normalize : (a : α) → α)
    (Function.comp (β := Associates α) Associates.out Associates.mk)
rw :
  Multiset.map (Function.comp (β := Associates α) Associates.out Associates.mk) (factors a) =
    Multiset.map (Function.comp (β := Associates α) Associates.out Associates.mk) (factors b)
⊢ Eq (α := Multiset α) (Multiset.map (⇑normalize : (a : α) → α) (factors a))
    (Multiset.map (⇑normalize : (a : α) → α) (factors b))
have rw₁ : Multiset.map (α := Associates α) Associates.out (Multiset.map Associates.mk (factors a)) =
  Multiset.map (Function.comp (β := Associates α) Associates.out Associates.mk) (factors b)
Tactic: rw [h', ← Multiset.map_map, ← Multiset.map_map,
    Associates.rel_associated_iff_map_eq_map.mp (factors_rel_of_associated h)]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
h' :
  Eq.{u_1 + 1} (α := (a : α) → α) (⇑normalize : (a : α) → α)
    (Function.comp (β := Associates α) Associates.out Associates.mk)
rw :
  Multiset.map (Function.comp (β := Associates α) Associates.out Associates.mk) (factors a) =
    Multiset.map (Function.comp (β := Associates α) Associates.out Associates.mk) (factors b)
rw₁ :
  Multiset.map (α := Associates α) Associates.out (Multiset.map Associates.mk (factors a)) =
    Multiset.map (Function.comp (β := Associates α) Associates.out Associates.mk) (factors b)
⊢ Eq (α := Multiset α) (Multiset.map (⇑normalize : (a : α) → α) (factors a))
    (Multiset.map (⇑normalize : (a : α) → α) (factors b))
have rw₂ : Multiset.map (α := Associates α) Associates.out (Multiset.map Associates.mk (factors a)) =
  Multiset.map (α := Associates α) Associates.out (Multiset.map Associates.mk (factors b))
Tactic: rw [h', ← Multiset.map_map, ← Multiset.map_map,
    Associates.rel_associated_iff_map_eq_map.mp (factors_rel_of_associated h)]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
h' :
  Eq.{u_1 + 1} (α := (a : α) → α) (⇑normalize : (a : α) → α)
    (Function.comp (β := Associates α) Associates.out Associates.mk)
rw :
  Multiset.map (Function.comp (β := Associates α) Associates.out Associates.mk) (factors a) =
    Multiset.map (Function.comp (β := Associates α) Associates.out Associates.mk) (factors b)
rw₁ :
  Multiset.map (α := Associates α) Associates.out (Multiset.map Associates.mk (factors a)) =
    Multiset.map (Function.comp (β := Associates α) Associates.out Associates.mk) (factors b)
rw₂ :
  Multiset.map (α := Associates α) Associates.out (Multiset.map Associates.mk (factors a)) =
    Multiset.map (α := Associates α) Associates.out (Multiset.map Associates.mk (factors b))
⊢ Eq (α := Multiset α) (Multiset.map (⇑normalize : (a : α) → α) (factors a))
    (Multiset.map (⇑normalize : (a : α) → α) (factors b))
have rw₃ : Multiset.map (α := Associates α) Associates.out (Multiset.map Associates.mk (factors b)) =
  Multiset.map (α := Associates α) Associates.out (Multiset.map Associates.mk (factors b))
Tactic: rw [h', ← Multiset.map_map, ← Multiset.map_map,
    Associates.rel_associated_iff_map_eq_map.mp (factors_rel_of_associated h)]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalizedFactors x = normalizedFactors y
⊢ (normalizedFactors x).prod ~ᵤ (normalizedFactors y).prod
have rw : (normalizedFactors y).prod ~ᵤ (normalizedFactors y).prod
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
p : α
hp : Irreducible p
k : ℕ
⊢ normalizedFactors (p ^ k) = Multiset.replicate k ((normalize : (a : α) → α) p)
have rw : k • normalizedFactors p = Multiset.replicate k ((normalize : (a : α) → α) p)
Tactic: rw [normalizedFactors_pow, normalizedFactors_irreducible hp, Multiset.nsmul_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
p : α
hp : Irreducible p
k : ℕ
rw : k • normalizedFactors p = Multiset.replicate k ((normalize : (a : α) → α) p)
⊢ normalizedFactors (p ^ k) = Multiset.replicate k ((normalize : (a : α) → α) p)
have rw₁ : HSMul.hSMul (β := Multiset α) k (singleton (α := α) ((normalize : (a : α) → α) p : α)) =
  Multiset.replicate k ((normalize : (a : α) → α) p)
Tactic: rw [normalizedFactors_pow, normalizedFactors_irreducible hp, Multiset.nsmul_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
p : α
hp : Irreducible p
k : ℕ
rw : k • normalizedFactors p = Multiset.replicate k ((normalize : (a : α) → α) p)
rw₁ :
  HSMul.hSMul (β := Multiset α) k (singleton (α := α) ((normalize : (a : α) → α) p : α)) =
    Multiset.replicate k ((normalize : (a : α) → α) p)
⊢ normalizedFactors (p ^ k) = Multiset.replicate k ((normalize : (a : α) → α) p)
have rw₂ : Eq (α := Multiset α) (Multiset.replicate k ((normalize : (a : α) → α) p) : Multiset α)
  (Multiset.replicate k ((normalize : (a : α) → α) p) : Multiset α)
Tactic: rw [normalizedFactors_pow, normalizedFactors_irreducible hp, Multiset.nsmul_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a p : α
H : p ∈ normalizedFactors a
⊢ p ∣ a
have pos : ∀ (hcases : a = 0), p ∣ a
Tactic: by_cases hcases : a = 0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a p : α
H : p ∈ normalizedFactors a
pos : ∀ (hcases : a = 0), p ∣ a
⊢ p ∣ a
have neg : ∀ (hcases : ¬a = 0), p ∣ a
Tactic: by_cases hcases : a = 0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a p : α
H : p ∈ normalizedFactors a
hcases : a = 0
⊢ p ∣ a
have pos : p ∣ 0
Tactic: rw [hcases]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
inst_3 : Subsingleton.{u_1 + 1} αˣ
p x : α
hx : x ≠ 0
⊢ p ∈ normalizedFactors x ↔ Prime p ∧ p ∣ x
have mp : p ∈ normalizedFactors x → Prime p ∧ p ∣ x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
inst_3 : Subsingleton.{u_1 + 1} αˣ
p x : α
hx : x ≠ 0
mp : p ∈ normalizedFactors x → Prime p ∧ p ∣ x
⊢ p ∈ normalizedFactors x ↔ Prime p ∧ p ∣ x
have mpr : Prime p ∧ p ∣ x → p ∈ normalizedFactors x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
inst_3 : Subsingleton.{u_1 + 1} αˣ
p x : α
hx : x ≠ 0
hprime : Prime p
hdvd : p ∣ x
⊢ p ∈ normalizedFactors x
have mpr : ∀ (q : α) (hqmem : q ∈ normalizedFactors x) (hqeq : p ~ᵤ q), p ∈ normalizedFactors x
Tactic: obtain ⟨q, hqmem, hqeq⟩ := exists_mem_normalizedFactors_of_dvd hx hprime.irreducible hdvd
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
inst_3 : Subsingleton.{u_1 + 1} αˣ
p x : α
hx : x ≠ 0
hprime : Prime p
hdvd : p ∣ x
q : α
hqmem : q ∈ normalizedFactors x
hqeq : p ~ᵤ q
⊢ p ∈ normalizedFactors x
have hqeq₁ : p = q
Tactic: rw [associated_iff_eq] at hqeq
Cleared hypotheses: hqeq
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
p x : α
h : x ≠ 0
⊢ p ∈ normalizedFactors x ↔ Irreducible p ∧ (normalize : (a : α) → α) p = p ∧ p ∣ x
have refine : Irreducible p ∧ (normalize : (a : α) → α) p = p ∧ p ∣ x →
  ∀ (h₁ : Irreducible p) (h₂ : (normalize : (a : α) → α) p = p) (h₃ : p ∣ x), p ∈ normalizedFactors x
Tactic: refine ⟨fun h ↦ ⟨irreducible_of_normalized_factor p h, normalize_normalized_factor p h,
    dvd_of_mem_normalizedFactors h⟩, fun ⟨h₁, h₂, h₃⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
p x : α
h : x ≠ 0
h_1 : Irreducible p ∧ (normalize : (a : α) → α) p = p ∧ p ∣ x
h₁ : Irreducible p
h₂ : (normalize : (a : α) → α) p = p
h₃ : p ∣ x
⊢ p ∈ normalizedFactors x
have obtain : ∀ (y : α) (hy₁ : y ∈ factors x) (hy₂ : p ~ᵤ y), p ∈ normalizedFactors x
Tactic: obtain ⟨y, hy₁, hy₂⟩ := exists_mem_factors_of_dvd h h₁ h₃
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
p x : α
h : x ≠ 0
h_1 : Irreducible p ∧ (normalize : (a : α) → α) p = p ∧ p ∣ x
h₁ : Irreducible p
h₂ : (normalize : (a : α) → α) p = p
h₃ : p ∣ x
y : α
hy₁ : y ∈ factors x
hy₂ : p ~ᵤ y
⊢ (normalize : (a : α) → α) y = p
have rwa : Eq (α := α) ((normalize : (a : α) → α) y : α) ((normalize : (a : α) → α) p : α)
Tactic: rwa [← h₂, normalize_eq_normalize_iff_associated, Associated.comm]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
p x : α
h : x ≠ 0
h_1 : Irreducible p ∧ (normalize : (a : α) → α) p = p ∧ p ∣ x
h₁ : Irreducible p
h₂ : (normalize : (a : α) → α) p = p
h₃ : p ∣ x
y : α
hy₁ : y ∈ factors x
hy₂ : p ~ᵤ y
rwa : Eq (α := α) ((normalize : (a : α) → α) y : α) ((normalize : (a : α) → α) p : α)
⊢ (normalize : (a : α) → α) y = p
have rwa₁ : y ~ᵤ p
Tactic: rwa [← h₂, normalize_eq_normalize_iff_associated, Associated.comm]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a b : α
hc : IsRelPrime a b
⊢ Disjoint (normalizedFactors a) (normalizedFactors b)
have rw : ∀ {a_1 : α}, a_1 ∈ normalizedFactors a → a_1 ∉ normalizedFactors b
Tactic: rw [Multiset.disjoint_left]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a b : α
hc : IsRelPrime a b
x : α
hxa : x ∈ normalizedFactors a
hxb : x ∈ normalizedFactors b
⊢ False
have x_dvd_a : x ∣ a
Tactic: have x_dvd_a := dvd_of_mem_normalizedFactors hxa
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a b : α
hc : IsRelPrime a b
x : α
hxa : x ∈ normalizedFactors a
hxb : x ∈ normalizedFactors b
x_dvd_a : x ∣ a
⊢ False
have x_dvd_b : x ∣ b
Tactic: have x_dvd_b := dvd_of_mem_normalizedFactors hxb
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
p r : α
h : ∀ {m : α}, m ∈ normalizedFactors r → m = p
hr : r ≠ 0
⊢ ∃ (i : ℕ), p ^ i ~ᵤ r
have h₁ : p ^ (normalizedFactors r).card ~ᵤ r
Tactic: use (normalizedFactors r).card
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
p r : α
h : ∀ {m : α}, m ∈ normalizedFactors r → m = p
hr : r ≠ 0
⊢ p ^ (normalizedFactors r).card ~ᵤ r
have this : (normalizedFactors r).prod ~ᵤ r
Tactic: have := UniqueFactorizationMonoid.prod_normalizedFactors hr
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
p r : α
h : ∀ {m : α}, m ∈ normalizedFactors r → m = p
hr : r ≠ 0
this : (normalizedFactors r).prod ~ᵤ r
⊢ p ^ (normalizedFactors r).card ~ᵤ r
have h₁ : ∀ (this : (Multiset.replicate (normalizedFactors r).card p).prod ~ᵤ r), p ^ (normalizedFactors r).card ~ᵤ r
Tactic: rwa [Multiset.eq_replicate_of_mem fun b => h, Multiset.prod_replicate] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
p r : α
h : ∀ {m : α}, m ∈ normalizedFactors r → m = p
hr : r ≠ 0
this : (normalizedFactors r).prod ~ᵤ r
h₁ : ∀ (this : (Multiset.replicate (normalizedFactors r).card p).prod ~ᵤ r), p ^ (normalizedFactors r).card ~ᵤ r
⊢ p ^ (normalizedFactors r).card ~ᵤ r
have h₂ : ∀ (this : p ^ (normalizedFactors r).card ~ᵤ r), p ^ (normalizedFactors r).card ~ᵤ r
Tactic: rwa [Multiset.eq_replicate_of_mem fun b => h, Multiset.prod_replicate] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
inst_3 : Subsingleton.{u_1 + 1} αˣ
m : Multiset α
h : ∀ p ∈ m, Prime p
⊢ normalizedFactors m.prod = m
have inl : Subsingleton α → normalizedFactors m.prod = m
Tactic: cases subsingleton_or_nontrivial α
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
inst_3 : Subsingleton.{u_1 + 1} αˣ
m : Multiset α
h : ∀ p ∈ m, Prime p
inl : Subsingleton α → normalizedFactors m.prod = m
⊢ normalizedFactors m.prod = m
have inr : Nontrivial α → normalizedFactors m.prod = m
Tactic: cases subsingleton_or_nontrivial α
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
inst_3 : Subsingleton.{u_1 + 1} αˣ
m : Multiset α
h : ∀ p ∈ m, Prime p
h_1 : Subsingleton α
⊢ m = 0
have refine : ∀ (x : α) (hx : x ∈ m), False
Tactic: refine Multiset.eq_zero_of_forall_notMem fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
inst_3 : Subsingleton.{u_1 + 1} αˣ
m : Multiset α
h : ∀ p ∈ m, Prime p
h_1 : Subsingleton α
⊢ normalizedFactors m.prod = m
have inl : ∀ (h : ∀ (p : α), Membership.mem (γ := Multiset α) 0 p → Prime p),
  Eq.{u_1 + 1} (α := Multiset α) (normalizedFactors (Multiset.prod 0)) 0
Tactic: obtain rfl : m = 0 := by
      refine Multiset.eq_zero_of_forall_notMem fun x hx ↦ ?_
      simpa [Subsingleton.elim x 0] using h x hx
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a b c : α
ha : a ∈ normalizedFactors c
hb : b ∈ normalizedFactors c
h : a ~ᵤ b
⊢ a = b
have rw : a ∣ b ∧ b ∣ a
Tactic: rw [← normalize_normalized_factor a ha, ← normalize_normalized_factor b hb,
    normalize_eq_normalize_iff]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
⊢ 0 < normalizedFactors x ↔ ¬IsUnit x
have mp : 0 < normalizedFactors x → ¬IsUnit x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
mp : 0 < normalizedFactors x → ¬IsUnit x
⊢ 0 < normalizedFactors x ↔ ¬IsUnit x
have mpr : ¬IsUnit x → 0 < normalizedFactors x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x : α
hx_1 : x ≠ 0
h : 0 < normalizedFactors x
hx : IsUnit x
⊢ False
have mp : ∀ (p : α) (hp : p ∈ normalizedFactors x), False
Tactic: obtain ⟨p, hp⟩ := Multiset.exists_mem_of_ne_zero h.ne'
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
⊢ 0 < normalizedFactors x
have mpr : ∀ (p : α) (hp : p ∈ normalizedFactors x), 0 < normalizedFactors x
Tactic: obtain ⟨p, hp⟩ := exists_mem_normalizedFactors hx h
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
⊢ normalizedFactors x = 0 ↔ IsUnit x
have rw : ¬normalizedFactors x = 0 ↔ ¬IsUnit x
Tactic: rw [← not_iff_not, ← normalizedFactors_pos _ hx, pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
rw : ¬normalizedFactors x = 0 ↔ ¬IsUnit x
⊢ normalizedFactors x = 0 ↔ IsUnit x
have rw₁ : ¬normalizedFactors x = 0 ↔ 0 < normalizedFactors x
Tactic: rw [← not_iff_not, ← normalizedFactors_pos _ hx, pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
rw : ¬normalizedFactors x = 0 ↔ ¬IsUnit x
rw₁ : ¬normalizedFactors x = 0 ↔ 0 < normalizedFactors x
⊢ normalizedFactors x = 0 ↔ IsUnit x
have rw₂ : ¬normalizedFactors x = 0 ↔ normalizedFactors x ≠ 0
Tactic: rw [← not_iff_not, ← normalizedFactors_pos _ hx, pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x : α
hx : IsUnit x
⊢ normalizedFactors x = 0
have inl : ∀ (hx : IsUnit.{u_1} (M := α) 0), Eq.{u_1 + 1} (α := Multiset α) (normalizedFactors 0) 0
Tactic: obtain rfl | hx₀ := eq_or_ne x 0
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x : α
hx : IsUnit x
inl : ∀ (hx : IsUnit.{u_1} (M := α) 0), Eq.{u_1 + 1} (α := Multiset α) (normalizedFactors 0) 0
⊢ normalizedFactors x = 0
have inr : ∀ (hx₀ : x ≠ 0), normalizedFactors x = 0
Tactic: obtain rfl | hx₀ := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ DvdNotUnit x y ↔ normalizedFactors x < normalizedFactors y
have mp : DvdNotUnit x y → normalizedFactors x < normalizedFactors y
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
mp : DvdNotUnit x y → normalizedFactors x < normalizedFactors y
⊢ DvdNotUnit x y ↔ normalizedFactors x < normalizedFactors y
have mpr : normalizedFactors x < normalizedFactors y → DvdNotUnit x y
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
s : Multiset α
hs : 0 ∉ s
⊢ normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum
have inl : Subsingleton α → normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum
Tactic: cases subsingleton_or_nontrivial α
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
s : Multiset α
hs : 0 ∉ s
inl : Subsingleton α → normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum
⊢ normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum
have inr : Nontrivial α → normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum
Tactic: cases subsingleton_or_nontrivial α
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
s : Multiset α
hs : 0 ∉ s
h : Subsingleton α
⊢ s = 0
have a : ∀ (x : α), x ∉ s
Tactic: apply Multiset.eq_zero_of_forall_notMem