-- Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
theorem mem_normalizedFactors_iff [Subsingleton αˣ] {p x : α} (hx : x ≠ 0) :
    p ∈ normalizedFactors x ↔ Prime p ∧ p ∣ x

Proof state:
case mpr
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
p x : α
hx : x ≠ 0
⊢ Prime p ∧ p ∣ x → p ∈ normalizedFactors x

Tactic:
rintro ⟨hprime, hdvd⟩

Result:
case mpr.intro
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
p x : α
hx : x ≠ 0
hprime : Prime p
hdvd : p ∣ x
⊢ p ∈ normalizedFactors x

Proof state:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
p x : α
hx : x ≠ 0
⊢ p ∈ normalizedFactors x ↔ Prime p ∧ p ∣ x

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
p x : α
hx : x ≠ 0
⊢ p ∈ normalizedFactors x → Prime p ∧ p ∣ x

case mpr
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
p x : α
hx : x ≠ 0
⊢ Prime p ∧ p ∣ x → p ∈ normalizedFactors x

Proof state:
case mpr.intro
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
p x : α
hx : x ≠ 0
hprime : Prime p
hdvd : p ∣ x
⊢ p ∈ normalizedFactors x

Tactic:
obtain ⟨q, hqmem, hqeq⟩ := exists_mem_normalizedFactors_of_dvd hx hprime.irreducible hdvd

Result:
case mpr.intro.intro.intro
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
p x : α
hx : x ≠ 0
hprime : Prime p
hdvd : p ∣ x
q : α
hqmem : q ∈ normalizedFactors x
hqeq : p ~ᵤ q
⊢ p ∈ normalizedFactors x

Proof state:
case mpr.intro.intro.intro
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
p x : α
hx : x ≠ 0
hprime : Prime p
hdvd : p ∣ x
q : α
hqmem : q ∈ normalizedFactors x
hqeq : p ~ᵤ q
⊢ p ∈ normalizedFactors x

Tactic:
rw [associated_iff_eq] at hqeq

Result:
case mpr.intro.intro.intro
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
p x : α
hx : x ≠ 0
hprime : Prime p
hdvd : p ∣ x
q : α
hqmem : q ∈ normalizedFactors x
hqeq : p = q
⊢ p ∈ normalizedFactors x

Proof state:
case mp
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
p x : α
hx : x ≠ 0
h : p ∈ normalizedFactors x
⊢ Prime p ∧ p ∣ x

Tactic:
exact ⟨prime_of_normalized_factor p h, dvd_of_mem_normalizedFactors h⟩

Result:
no goals

Proof state:
case mpr.intro.intro.intro
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
p x : α
hx : x ≠ 0
hprime : Prime p
hdvd : p ∣ x
q : α
hqmem : q ∈ normalizedFactors x
hqeq : p = q
⊢ p ∈ normalizedFactors x

Tactic:
exact hqeq ▸ hqmem

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
p x : α
hx : x ≠ 0
⊢ p ∈ normalizedFactors x → Prime p ∧ p ∣ x

Tactic:
intro h

Result:
case mp
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
p x : α
hx : x ≠ 0
h : p ∈ normalizedFactors x
⊢ Prime p ∧ p ∣ x