α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
hf : Function.Surjective ↑f
b : ConjClasses β
⊢ ∃ a, map f a = b
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
hf : Function.Surjective ↑f
⊢ Function.Surjective (map f)
intro b
case intro
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
hf : Function.Surjective ↑f
b : β
⊢ ∃ a, map f a = ConjClasses.mk b
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
hf : Function.Surjective ↑f
b : ConjClasses β
⊢ ∃ a, map f a = b
obtain ⟨b, rfl⟩ := ConjClasses.mk_surjective b
case intro.intro
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
hf : Function.Surjective ↑f
a : α
⊢ ∃ a_1, map f a_1 = ConjClasses.mk (↑f a)
case intro
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
hf : Function.Surjective ↑f
b : β
⊢ ∃ a, map f a = ConjClasses.mk b
obtain ⟨a, rfl⟩ := hf b
no goals
case intro.intro
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
hf : Function.Surjective ↑f
a : α
⊢ ∃ a_1, map f a_1 = ConjClasses.mk (↑f a)
exact ⟨ConjClasses.mk a, rfl⟩