rw [if_pos (mem_Icc.mp ‹_›).1]
case h.e'_2.a
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b : α
a✝¹ : a ≤ b
he : ¬a = b
x✝ : α
a✝ : x✝ ∈ Icc a b
⊢ (if a ≤ x✝ then (IncidenceAlgebra.mu' 𝕜) x✝ b else 0 * (IncidenceAlgebra.mu' 𝕜) x✝ b) = (IncidenceAlgebra.mu' 𝕜) x✝ b

case neg.convert_3
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b : α
a✝ : a ≤ b
he : ¬a = b
⊢ One 𝕜
no goals