instSemigroupWithZero — Mathlib

Lean4
instance instSemigroupWithZero [SemigroupWithZero α] [NoZeroDivisors α] : SemigroupWithZero (WithTop α)
    where
  __ := instMulZeroClass
  mul_assoc a b
    c := by
    rcases eq_or_ne a 0 with (rfl | ha); · simp only [zero_mul]
    rcases eq_or_ne b 0 with (rfl | hb); · simp only [zero_mul, mul_zero]
    rcases eq_or_ne c 0 with (rfl | hc); · simp only [mul_zero]
    cases a with
    | top => simp [hb, hc]
    | coe a => ?_
    cases b with
    | top => simp [mul_top ha, top_mul hc]
    | coe b => ?_
    cases c with
    | top =>
      rw [mul_top hb, mul_top ha]
      rw [← coe_zero, ne_eq, coe_eq_coe] at ha hb
      simp [ha, hb]
    | coe c => simp only [← coe_mul, mul_assoc]
Похожие утверждения