Theorem: IncidenceAlgebra.mu_apply_of_ne' (LeanCamCombi/Incidence.lean)

State before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
⊢ (mu 𝕜) a b = -∑ x ∈ Ioc a b, (mu 𝕜) x b
Tactic:
rw [mu_eq_mu']
State after:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
⊢ (IncidenceAlgebra.mu' 𝕜) a b = -∑ x ∈ Ioc a b, (IncidenceAlgebra.mu' 𝕜) x b

State before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
⊢ (IncidenceAlgebra.mu' 𝕜) a b = -∑ x ∈ Ioc a b, (IncidenceAlgebra.mu' 𝕜) x b
Tactic:
exact mu'_apply_of_ne h
State after:
no goals