no goals
α : Type u_1
β : Type u_3
γ : Type ?u.8780
δ : Type ?u.8783
inst✝³ : CommMonoidWithZero α
inst✝² : CommMonoidWithZero β
F : Type u_2
G : Type u_4
inst✝¹ : MonoidWithZeroHomClass F α β
inst✝ : MulHomClass G β α
f : F
g : G
p : α
hinv : ∀ (a : α), ↑g (↑f a) = a
hp : Prime (↑f p)
h : p = 0
⊢ ↑f p = 0
simp [h]
case h.e'_4
α : Type u_1
β : Type u_3
γ : Type ?u.8780
δ : Type ?u.8783
inst✝³ : CommMonoidWithZero α
inst✝² : CommMonoidWithZero β
F : Type u_2
G : Type u_4
inst✝¹ : MonoidWithZeroHomClass F α β
inst✝ : MulHomClass G β α
f : F
g : G
p : α
hinv : ∀ (a : α), ↑g (↑f a) = a
hp : Prime (↑f p)
a b : α
h : p ∣ a * b
⊢ ↑f a * ↑f b = ↑f (a * b)
α : Type u_1
β : Type u_3
γ : Type ?u.8780
δ : Type ?u.8783
inst✝³ : CommMonoidWithZero α
inst✝² : CommMonoidWithZero β
F : Type u_2
G : Type u_4
inst✝¹ : MonoidWithZeroHomClass F α β
inst✝ : MulHomClass G β α
f : F
g : G
p : α
hinv : ∀ (a : α), ↑g (↑f a) = a
hp : Prime (↑f p)
a b : α
h : p ∣ a * b
⊢ ↑f p ∣ ↑f a * ↑f b
convert map_dvd f h
no goals
case h.e'_4
α : Type u_1
β : Type u_3
γ : Type ?u.8780
δ : Type ?u.8783
inst✝³ : CommMonoidWithZero α
inst✝² : CommMonoidWithZero β
F : Type u_2
G : Type u_4
inst✝¹ : MonoidWithZeroHomClass F α β
inst✝ : MulHomClass G β α
f : F
g : G
p : α
hinv : ∀ (a : α), ↑g (↑f a) = a
hp : Prime (↑f p)
a b : α
h : p ∣ a * b
⊢ ↑f a * ↑f b = ↑f (a * b)
simp
case refine'_2
α : Type u_1
β : Type u_3
γ : Type ?u.8780
δ : Type ?u.8783
inst✝³ : CommMonoidWithZero α
inst✝² : CommMonoidWithZero β
F : Type u_2
G : Type u_4
inst✝¹ : MonoidWithZeroHomClass F α β
inst✝ : MulHomClass G β α
f : F
g : G
p : α
hinv : ∀ (a : α), ↑g (↑f a) = a
hp : Prime (↑f p)
a b : α
h✝ : p ∣ a * b
h : ↑f p ∣ ↑f b
⊢ p ∣ b
case refine'_2
α : Type u_1
β : Type u_3
γ : Type ?u.8780
δ : Type ?u.8783
inst✝³ : CommMonoidWithZero α
inst✝² : CommMonoidWithZero β
F : Type u_2
G : Type u_4
inst✝¹ : MonoidWithZeroHomClass F α β
inst✝ : MulHomClass G β α
f : F
g : G
p : α
hinv : ∀ (a : α), ↑g (↑f a) = a
hp : Prime (↑f p)
a b : α
h : p ∣ a * b
⊢ ↑f p ∣ ↑f b → p ∣ b
intro h
no goals
case refine'_2
α : Type u_1
β : Type u_3
γ : Type ?u.8780
δ : Type ?u.8783
inst✝³ : CommMonoidWithZero α
inst✝² : CommMonoidWithZero β
F : Type u_2
G : Type u_4
inst✝¹ : MonoidWithZeroHomClass F α β
inst✝ : MulHomClass G β α
f : F
g : G
p : α
hinv : ∀ (a : α), ↑g (↑f a) = a
hp : Prime (↑f p)
a b : α
h✝ : p ∣ a * b
h : ↑f p ∣ ↑f b
⊢ p ∣ b
convert ← map_dvd g h <;> apply hinv