α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this : DecidableEq α := Classical.decEq α
⊢ f (a * b) = f a * f b
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
⊢ f (a * b) = f a * f b
letI := Classical.decEq α
case pos
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this : DecidableEq α := Classical.decEq α
ha0 : a = 0
⊢ f (a * b) = f a * f b

case neg
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
⊢ f (a * b) = f a * f b
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this : DecidableEq α := Classical.decEq α
⊢ f (a * b) = f a * f b
by_cases ha0 : a = 0
case pos
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : b = 0
⊢ f (a * b) = f a * f b

case neg
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
⊢ f (a * b) = f a * f b
case neg
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
⊢ f (a * b) = f a * f b
by_cases hb0 : b = 0
case pos
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : f 1 = 0
⊢ f (a * b) = f a * f b

case neg
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
⊢ f (a * b) = f a * f b
case neg
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
⊢ f (a * b) = f a * f b
by_cases hf1 : f 1 = 0
case neg
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this : Nontrivial α
⊢ f (a * b) = f a * f b
case neg
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
⊢ f (a * b) = f a * f b
haveI : Nontrivial α := ⟨⟨_, _, ha0⟩⟩
case neg
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ f (a * b) = f a * f b
case neg
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this : Nontrivial α
⊢ f (a * b) = f a * f b
letI : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
case neg.refine'_1
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ ∀ (p : α), p ∈ Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b) → Prime p

case neg.refine'_2
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ ∀ (p : α),
    p ∈ Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b) →
      ∀ (q : α), q ∈ Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b) → p ∣ q → p = q
case neg
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ f
      (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors b))
refine' multiplicative_prime_power _ _ _ _ _ @h1 @hpr @hcp
case neg.refine'_1
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ ∀ (p : α), p ∈ normalizedFactors a ∨ p ∈ normalizedFactors b → Prime p

case neg.refine'_2
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ ∀ (p : α),
    p ∈ normalizedFactors a ∨ p ∈ normalizedFactors b →
      ∀ (q : α), q ∈ normalizedFactors a ∨ q ∈ normalizedFactors b → p ∣ q → p = q
case neg.refine'_1
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ ∀ (p : α), p ∈ Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b) → Prime p

case neg.refine'_2
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ ∀ (p : α),
    p ∈ Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b) →
      ∀ (q : α), q ∈ Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b) → p ∣ q → p = q
all_goals simp only [Multiset.mem_toFinset, Finset.mem_union]
no goals
case pos
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this : DecidableEq α := Classical.decEq α
ha0 : a = 0
⊢ f (a * b) = f a * f b
rw [ha0, MulZeroClass.zero_mul, h0, MulZeroClass.zero_mul]
no goals
case pos
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : b = 0
⊢ f (a * b) = f a * f b
rw [hb0, MulZeroClass.mul_zero, h0, MulZeroClass.mul_zero]
no goals
case pos
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : f 1 = 0
⊢ f (a * b) = f a * f b
calc
  f (a * b) = f (a * b * 1) := by rw [mul_one]
  _ = 0 := by simp only [h1 isUnit_one, hf1, MulZeroClass.mul_zero]
  _ = f a * f (b * 1) := by simp only [h1 isUnit_one, hf1, MulZeroClass.mul_zero]
  _ = f a * f b := by rw [mul_one]
no goals
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : f 1 = 0
⊢ f (a * b) = f (a * b * 1)
rw [mul_one]
no goals
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : f 1 = 0
⊢ f (a * b * 1) = 0
simp only [h1 isUnit_one, hf1, MulZeroClass.mul_zero]
no goals
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : f 1 = 0
⊢ 0 = f a * f (b * 1)
simp only [h1 isUnit_one, hf1, MulZeroClass.mul_zero]
no goals
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : f 1 = 0
⊢ f a * f (b * 1) = f a * f b
rw [mul_one]
case intro
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : Multiset.prod (normalizedFactors a) * ↑ua = a
⊢ f (a * b) = f a * f b
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors b))
⊢ f (a * b) = f a * f b
obtain ⟨ua, a_eq⟩ := normalizedFactors_prod ha0
case intro.intro
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : Multiset.prod (normalizedFactors a) * ↑ua = a
ub : αˣ
b_eq : Multiset.prod (normalizedFactors b) * ↑ub = b
⊢ f (a * b) = f a * f b
case intro
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : Multiset.prod (normalizedFactors a) * ↑ua = a
⊢ f (a * b) = f a * f b
obtain ⟨ub, b_eq⟩ := normalizedFactors_prod hb0
case intro.intro
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : Multiset.prod (normalizedFactors a) * ↑ua = a
ub : αˣ
b_eq : Multiset.prod (normalizedFactors b) * ↑ub = b
⊢ f (Multiset.prod (normalizedFactors a) * Multiset.prod (normalizedFactors b)) * f ↑ub * f ↑ua =
    f (Multiset.prod (normalizedFactors a)) * f (Multiset.prod (normalizedFactors b)) * f ↑ub * f ↑ua
case intro.intro
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : Multiset.prod (normalizedFactors a) * ↑ua = a
ub : αˣ
b_eq : Multiset.prod (normalizedFactors b) * ↑ub = b
⊢ f (a * b) = f a * f b
rw [← a_eq, ← b_eq, mul_right_comm (Multiset.prod (normalizedFactors a)) ua
    (Multiset.prod (normalizedFactors b) * ub), h1 ua.isUnit, h1 ub.isUnit, h1 ua.isUnit, ←
  mul_assoc, h1 ub.isUnit, mul_right_comm _ (f ua), ← mul_assoc]
case intro.intro.e_a.e_a
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : Multiset.prod (normalizedFactors a) * ↑ua = a
ub : αˣ
b_eq : Multiset.prod (normalizedFactors b) * ↑ub = b
⊢ f (Multiset.prod (normalizedFactors a) * Multiset.prod (normalizedFactors b)) =
    f (Multiset.prod (normalizedFactors a)) * f (Multiset.prod (normalizedFactors b))
case intro.intro
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : Multiset.prod (normalizedFactors a) * ↑ua = a
ub : αˣ
b_eq : Multiset.prod (normalizedFactors b) * ↑ub = b
⊢ f (Multiset.prod (normalizedFactors a) * Multiset.prod (normalizedFactors b)) * f ↑ub * f ↑ua =
    f (Multiset.prod (normalizedFactors a)) * f (Multiset.prod (normalizedFactors b)) * f ↑ub * f ↑ua
congr
case intro.intro.e_a.e_a
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : Multiset.prod (normalizedFactors a) * ↑ua = a
ub : αˣ
b_eq : Multiset.prod (normalizedFactors b) * ↑ub = b
⊢ f
      (∏ x in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        id x ^ Multiset.count x (normalizedFactors a) * id x ^ Multiset.count x (normalizedFactors b)) =
    f
        (∏ x in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          id x ^ Multiset.count x (normalizedFactors a)) *
      f
        (∏ x in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          id x ^ Multiset.count x (normalizedFactors b))

case intro.intro.e_a.e_a
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : Multiset.prod (normalizedFactors a) * ↑ua = a
ub : αˣ
b_eq : Multiset.prod (normalizedFactors b) * ↑ub = b
⊢ ∀ (x : α),
    x ∈ Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b) →
      ¬x ∈ Multiset.toFinset (normalizedFactors b) → id x ^ Multiset.count x (normalizedFactors b) = 1

case intro.intro.e_a.e_a
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : Multiset.prod (normalizedFactors a) * ↑ua = a
ub : αˣ
b_eq : Multiset.prod (normalizedFactors b) * ↑ub = b
⊢ ∀ (x : α),
    x ∈ Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b) →
      ¬x ∈ Multiset.toFinset (normalizedFactors a) → id x ^ Multiset.count x (normalizedFactors a) = 1
case intro.intro.e_a.e_a
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : Multiset.prod (normalizedFactors a) * ↑ua = a
ub : αˣ
b_eq : Multiset.prod (normalizedFactors b) * ↑ub = b
⊢ f (Multiset.prod (normalizedFactors a) * Multiset.prod (normalizedFactors b)) =
    f (Multiset.prod (normalizedFactors a)) * f (Multiset.prod (normalizedFactors b))
rw [← (normalizedFactors a).map_id, ← (normalizedFactors b).map_id,
  Finset.prod_multiset_map_count, Finset.prod_multiset_map_count,
  Finset.prod_subset (Finset.subset_union_left _ (normalizedFactors b).toFinset),
  Finset.prod_subset (Finset.subset_union_right _ (normalizedFactors b).toFinset), ←
  Finset.prod_mul_distrib]
case intro.intro.e_a.e_a
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : Multiset.prod (normalizedFactors a) * ↑ua = a
ub : αˣ
b_eq : Multiset.prod (normalizedFactors b) * ↑ub = b
⊢ ∀ (x : α),
    x ∈ Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b) →
      ¬x ∈ Multiset.toFinset (normalizedFactors b) → id x ^ Multiset.count x (normalizedFactors b) = 1

case intro.intro.e_a.e_a
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : Multiset.prod (normalizedFactors a) * ↑ua = a
ub : αˣ
b_eq : Multiset.prod (normalizedFactors b) * ↑ub = b
⊢ ∀ (x : α),
    x ∈ Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b) →
      ¬x ∈ Multiset.toFinset (normalizedFactors a) → id x ^ Multiset.count x (normalizedFactors a) = 1
case intro.intro.e_a.e_a
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : Multiset.prod (normalizedFactors a) * ↑ua = a
ub : αˣ
b_eq : Multiset.prod (normalizedFactors b) * ↑ub = b
⊢ f
      (∏ x in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        id x ^ Multiset.count x (normalizedFactors a) * id x ^ Multiset.count x (normalizedFactors b)) =
    f
        (∏ x in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          id x ^ Multiset.count x (normalizedFactors a)) *
      f
        (∏ x in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          id x ^ Multiset.count x (normalizedFactors b))

case intro.intro.e_a.e_a
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : Multiset.prod (normalizedFactors a) * ↑ua = a
ub : αˣ
b_eq : Multiset.prod (normalizedFactors b) * ↑ub = b
⊢ ∀ (x : α),
    x ∈ Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b) →
      ¬x ∈ Multiset.toFinset (normalizedFactors b) → id x ^ Multiset.count x (normalizedFactors b) = 1

case intro.intro.e_a.e_a
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : Multiset.prod (normalizedFactors a) * ↑ua = a
ub : αˣ
b_eq : Multiset.prod (normalizedFactors b) * ↑ub = b
⊢ ∀ (x : α),
    x ∈ Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b) →
      ¬x ∈ Multiset.toFinset (normalizedFactors a) → id x ^ Multiset.count x (normalizedFactors a) = 1
simp_rw [id.def, ← pow_add, this]
case intro.intro.e_a.e_a
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : Multiset.prod (normalizedFactors a) * ↑ua = a
ub : αˣ
b_eq : Multiset.prod (normalizedFactors b) * ↑ub = b
⊢ ∀ (x : α),
    x ∈ Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b) →
      ¬x ∈ normalizedFactors b → id x ^ Multiset.count x (normalizedFactors b) = 1

case intro.intro.e_a.e_a
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : Multiset.prod (normalizedFactors a) * ↑ua = a
ub : αˣ
b_eq : Multiset.prod (normalizedFactors b) * ↑ub = b
⊢ ∀ (x : α),
    x ∈ Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b) →
      ¬x ∈ normalizedFactors a → id x ^ Multiset.count x (normalizedFactors a) = 1
case intro.intro.e_a.e_a
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : Multiset.prod (normalizedFactors a) * ↑ua = a
ub : αˣ
b_eq : Multiset.prod (normalizedFactors b) * ↑ub = b
⊢ ∀ (x : α),
    x ∈ Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b) →
      ¬x ∈ Multiset.toFinset (normalizedFactors b) → id x ^ Multiset.count x (normalizedFactors b) = 1

case intro.intro.e_a.e_a
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : Multiset.prod (normalizedFactors a) * ↑ua = a
ub : αˣ
b_eq : Multiset.prod (normalizedFactors b) * ↑ub = b
⊢ ∀ (x : α),
    x ∈ Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b) →
      ¬x ∈ Multiset.toFinset (normalizedFactors a) → id x ^ Multiset.count x (normalizedFactors a) = 1
all_goals simp only [Multiset.mem_toFinset]
case intro.intro.e_a.e_a
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : Multiset.prod (normalizedFactors a) * ↑ua = a
ub : αˣ
b_eq : Multiset.prod (normalizedFactors b) * ↑ub = b
⊢ ∀ (x : α),
    x ∈ Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b) →
      ¬x ∈ normalizedFactors a → id x ^ Multiset.count x (normalizedFactors a) = 1
case intro.intro.e_a.e_a
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : Multiset.prod (normalizedFactors a) * ↑ua = a
ub : αˣ
b_eq : Multiset.prod (normalizedFactors b) * ↑ub = b
⊢ ∀ (x : α),
    x ∈ Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b) →
      ¬x ∈ Multiset.toFinset (normalizedFactors a) → id x ^ Multiset.count x (normalizedFactors a) = 1
simp only [Multiset.mem_toFinset]
case intro.intro.e_a.e_a
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : Multiset.prod (normalizedFactors a) * ↑ua = a
ub : αˣ
b_eq : Multiset.prod (normalizedFactors b) * ↑ub = b
p : α
a✝ : p ∈ Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b)
hpb : ¬p ∈ normalizedFactors b
⊢ id p ^ Multiset.count p (normalizedFactors b) = 1
case intro.intro.e_a.e_a
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : Multiset.prod (normalizedFactors a) * ↑ua = a
ub : αˣ
b_eq : Multiset.prod (normalizedFactors b) * ↑ub = b
⊢ ∀ (x : α),
    x ∈ Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b) →
      ¬x ∈ normalizedFactors b → id x ^ Multiset.count x (normalizedFactors b) = 1
intro p _ hpb
no goals
case intro.intro.e_a.e_a
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : Multiset.prod (normalizedFactors a) * ↑ua = a
ub : αˣ
b_eq : Multiset.prod (normalizedFactors b) * ↑ub = b
p : α
a✝ : p ∈ Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b)
hpb : ¬p ∈ normalizedFactors b
⊢ id p ^ Multiset.count p (normalizedFactors b) = 1
simp [hpb]
case intro.intro.e_a.e_a
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : Multiset.prod (normalizedFactors a) * ↑ua = a
ub : αˣ
b_eq : Multiset.prod (normalizedFactors b) * ↑ub = b
p : α
a✝ : p ∈ Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b)
hpa : ¬p ∈ normalizedFactors a
⊢ id p ^ Multiset.count p (normalizedFactors a) = 1
case intro.intro.e_a.e_a
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : Multiset.prod (normalizedFactors a) * ↑ua = a
ub : αˣ
b_eq : Multiset.prod (normalizedFactors b) * ↑ub = b
⊢ ∀ (x : α),
    x ∈ Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b) →
      ¬x ∈ normalizedFactors a → id x ^ Multiset.count x (normalizedFactors a) = 1
intro p _ hpa
no goals
case intro.intro.e_a.e_a
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p in Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b),
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : Multiset.prod (normalizedFactors a) * ↑ua = a
ub : αˣ
b_eq : Multiset.prod (normalizedFactors b) * ↑ub = b
p : α
a✝ : p ∈ Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b)
hpa : ¬p ∈ normalizedFactors a
⊢ id p ^ Multiset.count p (normalizedFactors a) = 1
simp [hpa]
case neg.refine'_2
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ ∀ (p : α),
    p ∈ normalizedFactors a ∨ p ∈ normalizedFactors b →
      ∀ (q : α), q ∈ normalizedFactors a ∨ q ∈ normalizedFactors b → p ∣ q → p = q
case neg.refine'_2
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ ∀ (p : α),
    p ∈ Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b) →
      ∀ (q : α), q ∈ Multiset.toFinset (normalizedFactors a) ∪ Multiset.toFinset (normalizedFactors b) → p ∣ q → p = q
simp only [Multiset.mem_toFinset, Finset.mem_union]
no goals
case neg.refine'_1
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ ∀ (p : α), p ∈ normalizedFactors a ∨ p ∈ normalizedFactors b → Prime p
rintro p (hpa | hpb) <;> apply prime_of_normalized_factor <;> assumption
no goals
case neg.refine'_2
α : Type u_2
R : Type ?u.1916855
inst✝⁴ : CancelCommMonoidWithZero R
inst✝³ : UniqueFactorizationMonoid R
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_1
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ ∀ (p : α),
    p ∈ normalizedFactors a ∨ p ∈ normalizedFactors b →
      ∀ (q : α), q ∈ normalizedFactors a ∨ q ∈ normalizedFactors b → p ∣ q → p = q
rintro p (hp | hp) q (hq | hq) hdvd <;>
  rw [← normalize_normalized_factor _ hp, ← normalize_normalized_factor _ hq] <;>
  exact
    normalize_eq_normalize hdvd
      ((prime_of_normalized_factor _ hp).irreducible.dvd_symm
        (prime_of_normalized_factor _ hq).irreducible hdvd)