α : Type u_1
R : Type ?u.1571585
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type ?u.1571612
inst✝ : CancelCommMonoidWithZero β
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → P x → P y → P (x * y)
this : DecidableEq α := Classical.decEq α
⊢ P a
α : Type u_1
R : Type ?u.1571585
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type ?u.1571612
inst✝ : CancelCommMonoidWithZero β
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → P x → P y → P (x * y)
⊢ P a
letI := Classical.decEq α
α : Type u_1
R : Type ?u.1571585
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type ?u.1571612
inst✝ : CancelCommMonoidWithZero β
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → P x → P y → P (x * y)
this : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, x ~ᵤ y → P x → P y
⊢ P a
α : Type u_1
R : Type ?u.1571585
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type ?u.1571612
inst✝ : CancelCommMonoidWithZero β
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → 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 := by
  rintro x y ⟨u, rfl⟩ hx
  exact hcp (fun p _ hpx => isUnit_of_dvd_unit hpx u.isUnit) hx (h1 u.isUnit)
case pos
α : Type u_1
R : Type ?u.1571585
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type ?u.1571612
inst✝ : CancelCommMonoidWithZero β
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → P x → P y → P (x * y)
this : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, x ~ᵤ y → P x → P y
ha0 : a = 0
⊢ P a

case neg
α : Type u_1
R : Type ?u.1571585
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type ?u.1571612
inst✝ : CancelCommMonoidWithZero β
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → P x → P y → P (x * y)
this : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, x ~ᵤ y → P x → P y
ha0 : ¬a = 0
⊢ P a
α : Type u_1
R : Type ?u.1571585
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type ?u.1571612
inst✝ : CancelCommMonoidWithZero β
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → P x → P y → P (x * y)
this : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, x ~ᵤ y → P x → P y
⊢ P a
by_cases ha0 : a = 0
case neg
α : Type u_1
R : Type ?u.1571585
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type ?u.1571612
inst✝ : CancelCommMonoidWithZero β
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → P x → P y → P (x * y)
this✝ : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, x ~ᵤ y → P x → P y
ha0 : ¬a = 0
this : Nontrivial α
⊢ P a
case neg
α : Type u_1
R : Type ?u.1571585
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type ?u.1571612
inst✝ : CancelCommMonoidWithZero β
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → P x → P y → P (x * y)
this : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, x ~ᵤ y → P x → P y
ha0 : ¬a = 0
⊢ P a
haveI : Nontrivial α := ⟨⟨_, _, ha0⟩⟩
case neg
α : Type u_1
R : Type ?u.1571585
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type ?u.1571612
inst✝ : CancelCommMonoidWithZero β
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → P x → P y → P (x * y)
this✝¹ : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, x ~ᵤ y → P x → P y
ha0 : ¬a = 0
this✝ : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ P a
case neg
α : Type u_1
R : Type ?u.1571585
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type ?u.1571612
inst✝ : CancelCommMonoidWithZero β
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → P x → P y → P (x * y)
this✝ : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, x ~ᵤ y → P x → P y
ha0 : ¬a = 0
this : Nontrivial α
⊢ P a
letI : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
case neg
α : Type u_1
R : Type ?u.1571585
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type ?u.1571612
inst✝ : CancelCommMonoidWithZero β
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → P x → P y → P (x * y)
this✝¹ : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, x ~ᵤ y → P x → P y
ha0 : ¬a = 0
this✝ : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ P (Multiset.prod (normalizedFactors a))
case neg
α : Type u_1
R : Type ?u.1571585
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type ?u.1571612
inst✝ : CancelCommMonoidWithZero β
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → P x → P y → P (x * y)
this✝¹ : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, x ~ᵤ y → P x → P y
ha0 : ¬a = 0
this✝ : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ P a
refine' P_of_associated (normalizedFactors_prod ha0) _
case neg
α : Type u_1
R : Type ?u.1571585
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type ?u.1571612
inst✝ : CancelCommMonoidWithZero β
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → P x → P y → P (x * y)
this✝¹ : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, x ~ᵤ y → P x → P y
ha0 : ¬a = 0
this✝ : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ P (∏ m in Multiset.toFinset (normalizedFactors a), id m ^ Multiset.count m (normalizedFactors a))
case neg
α : Type u_1
R : Type ?u.1571585
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type ?u.1571612
inst✝ : CancelCommMonoidWithZero β
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → P x → P y → P (x * y)
this✝¹ : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, x ~ᵤ y → P x → P y
ha0 : ¬a = 0
this✝ : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ P (Multiset.prod (normalizedFactors a))
rw [← (normalizedFactors a).map_id, Finset.prod_multiset_map_count]
case neg.refine'_1
α : Type u_1
R : Type ?u.1571585
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type ?u.1571612
inst✝ : CancelCommMonoidWithZero β
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → P x → P y → P (x * y)
this✝¹ : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, x ~ᵤ y → P x → P y
ha0 : ¬a = 0
this✝ : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ ∀ (p : α), p ∈ normalizedFactors a → Prime p

case neg.refine'_2
α : Type u_1
R : Type ?u.1571585
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type ?u.1571612
inst✝ : CancelCommMonoidWithZero β
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → P x → P y → P (x * y)
this✝¹ : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, x ~ᵤ y → P x → P y
ha0 : ¬a = 0
this✝ : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ ∀ (p : α), p ∈ normalizedFactors a → ∀ (q : α), q ∈ normalizedFactors a → p ∣ q → p = q
case neg
α : Type u_1
R : Type ?u.1571585
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type ?u.1571612
inst✝ : CancelCommMonoidWithZero β
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → P x → P y → P (x * y)
this✝¹ : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, x ~ᵤ y → P x → P y
ha0 : ¬a = 0
this✝ : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ P (∏ m in Multiset.toFinset (normalizedFactors a), id m ^ Multiset.count m (normalizedFactors a))
refine' induction_on_prime_power _ _ _ _ @h1 @hpr @hcp <;> simp only [Multiset.mem_toFinset]
case intro
α : Type u_1
R : Type ?u.1571585
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type ?u.1571612
inst✝ : CancelCommMonoidWithZero β
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → P x → P y → P (x * y)
this : DecidableEq α := Classical.decEq α
x : α
u : αˣ
hx : P x
⊢ P (x * ↑u)
α : Type u_1
R : Type ?u.1571585
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type ?u.1571612
inst✝ : CancelCommMonoidWithZero β
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → P x → P y → P (x * y)
this : DecidableEq α := Classical.decEq α
⊢ ∀ {x y : α}, x ~ᵤ y → P x → P y
rintro x y ⟨u, rfl⟩ hx
no goals
case intro
α : Type u_1
R : Type ?u.1571585
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type ?u.1571612
inst✝ : CancelCommMonoidWithZero β
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → P x → P y → P (x * y)
this : DecidableEq α := Classical.decEq α
x : α
u : αˣ
hx : P x
⊢ P (x * ↑u)
exact hcp (fun p _ hpx => isUnit_of_dvd_unit hpx u.isUnit) hx (h1 u.isUnit)
no goals
case pos
α : Type u_1
R : Type ?u.1571585
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type ?u.1571612
inst✝ : CancelCommMonoidWithZero β
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → P x → P y → P (x * y)
this : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, x ~ᵤ y → P x → P y
ha0 : a = 0
⊢ P a
rwa [ha0]
no goals
case neg.refine'_1
α : Type u_1
R : Type ?u.1571585
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type ?u.1571612
inst✝ : CancelCommMonoidWithZero β
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → P x → P y → P (x * y)
this✝¹ : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, x ~ᵤ y → P x → P y
ha0 : ¬a = 0
this✝ : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ ∀ (p : α), p ∈ normalizedFactors a → Prime p
apply prime_of_normalized_factor
no goals
case neg.refine'_2
α : Type u_1
R : Type ?u.1571585
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type ?u.1571612
inst✝ : CancelCommMonoidWithZero β
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → P x → P y → P (x * y)
this✝¹ : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, x ~ᵤ y → P x → P y
ha0 : ¬a = 0
this✝ : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ ∀ (p : α), p ∈ normalizedFactors a → ∀ (q : α), q ∈ normalizedFactors a → p ∣ q → p = q
apply normalizedFactors_eq_of_dvd