Lean4
/-- A version of `WithTop.map` for `MonoidWithZeroHom`s. -/
@[simps -fullyApplied]
protected def _root_.MonoidWithZeroHom.withTopMap {R S : Type*} [MulZeroOneClass R] [DecidableEq R] [Nontrivial R]
[MulZeroOneClass S] [DecidableEq S] [Nontrivial S] (f : R →*₀ S) (hf : Function.Injective f) :
WithTop R →*₀ WithTop S :=
{ f.toZeroHom.withTopMap,
f.toMonoidHom.toOneHom.withTopMap with
toFun := WithTop.map f
map_mul' := fun x y =>
by
have : ∀ z, map f z = 0 ↔ z = 0 := fun z => (Option.map_injective hf).eq_iff' f.toZeroHom.withTopMap.map_zero
rcases Decidable.eq_or_ne x 0 with (rfl | hx)
· simp
rcases Decidable.eq_or_ne y 0 with (rfl | hy)
· simp
cases x with
| top => simp [hy, this]
| coe x => ?_
cases y with
| top =>
have : (f x : WithTop S) ≠ 0 := by simpa [hf.eq_iff' (map_zero f)] using hx
simp [mul_top hx, mul_top this]
| coe y => simp [← coe_mul] }
