Theorem: IncidenceAlgebra.moebius_inversion_bot (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✝² : OrderBot α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Iic x, f y
x : α
⊢ f x = ∑ y ∈ Iic x, (mu 𝕜) y x * g y
Tactic:
convert moebius_inversion_top (α := αᵒᵈ) f g h x using 3
State after:
case h.e'_3.a.h.e'_5
𝕄 : 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✝² : OrderBot α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Iic x, f y
x x✝ : α
a✝ : x✝ ∈ Ici x
⊢ (mu 𝕜) x✝ x = (mu 𝕜) x x✝

State before:
case h.e'_3.a.h.e'_5
𝕄 : 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✝² : OrderBot α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Iic x, f y
x x✝ : α
a✝ : x✝ ∈ Ici x
⊢ (mu 𝕜) x✝ x = (mu 𝕜) x x✝
Tactic:
erw [mu_toDual]
State after:
no goals