α : Type u_1
β : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : CancelCommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
⊢ ∀ (a : β), a ≠ 0 → ∃ f, (∀ (b : β), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
α : Type u_1
β : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : CancelCommMonoidWithZero β
e : α ≃* β
hα : UniqueFactorizationMonoid α
⊢ UniqueFactorizationMonoid β
rw [UniqueFactorizationMonoid.iff_exists_prime_factors] at hα⊢
α : Type u_1
β : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : CancelCommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
a : β
ha : a ≠ 0
⊢ ∃ f, (∀ (b : β), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
α : Type u_1
β : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : CancelCommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
⊢ ∀ (a : β), a ≠ 0 → ∃ f, (∀ (b : β), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
intro a ha
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : CancelCommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
a : β
ha : a ≠ 0
w : Multiset α
hp : ∀ (b : α), b ∈ w → Prime b
u : αˣ
h : Multiset.prod w * ↑u = ↑(symm e) a
⊢ ∃ f, (∀ (b : β), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
α : Type u_1
β : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : CancelCommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
a : β
ha : a ≠ 0
⊢ ∃ f, (∀ (b : β), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
obtain ⟨w, hp, u, h⟩ :=
  hα (e.symm a) fun h =>
    ha <| by
      convert← map_zero e
      simp [← h]
no goals
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : CancelCommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
a : β
ha : a ≠ 0
w : Multiset α
hp : ∀ (b : α), b ∈ w → Prime b
u : αˣ
h : Multiset.prod w * ↑u = ↑(symm e) a
⊢ ∃ f, (∀ (b : β), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
exact
  ⟨w.map e, fun b hb =>
      let ⟨c, hc, he⟩ := Multiset.mem_map.1 hb
      he ▸ e.prime_iff.1 (hp c hc),
      Units.map e.toMonoidHom u,
    by
      erw [Multiset.prod_hom, ← e.map_mul, h]
      simp⟩
case h.e'_2
α : Type u_1
β : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : CancelCommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
a : β
ha : a ≠ 0
h : ↑(symm e) a = 0
⊢ ↑e 0 = a
α : Type u_1
β : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : CancelCommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
a : β
ha : a ≠ 0
h : ↑(symm e) a = 0
⊢ a = 0
convert← map_zero e
no goals
case h.e'_2
α : Type u_1
β : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : CancelCommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
a : β
ha : a ≠ 0
h : ↑(symm e) a = 0
⊢ ↑e 0 = a
simp [← h]
α : Type u_1
β : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : CancelCommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
a : β
ha : a ≠ 0
w : Multiset α
hp : ∀ (b : α), b ∈ w → Prime b
u : αˣ
h : Multiset.prod w * ↑u = ↑(symm e) a
⊢ ↑e (↑(symm e) a) = a
α : Type u_1
β : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : CancelCommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
a : β
ha : a ≠ 0
w : Multiset α
hp : ∀ (b : α), b ∈ w → Prime b
u : αˣ
h : Multiset.prod w * ↑u = ↑(symm e) a
⊢ Multiset.prod (Multiset.map (↑e) w) * ↑(↑(Units.map (toMonoidHom e)) u) = a
erw [Multiset.prod_hom, ← e.map_mul, h]
no goals
α : Type u_1
β : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : CancelCommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
a : β
ha : a ≠ 0
w : Multiset α
hp : ∀ (b : α), b ∈ w → Prime b
u : αˣ
h : Multiset.prod w * ↑u = ↑(symm e) a
⊢ ↑e (↑(symm e) a) = a
simp