-- Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
/-- A general form of Möbius inversion. Based on lemma 2.1.2 of Incidence Algebras by Spiegel and
O'Donnell. -/
lemma moebius_inversion_top (f g : α → 𝕜) (h : ∀ x, g x = ∑ y ∈ Ici x, f y) (x : α) :
    f x = ∑ y ∈ Ici x, mu 𝕜 x y * g y

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
⊢ ∑ x_1 ∈ (Ici x).sigma fun y => Ici y, (mu 𝕜) x x_1.fst * (zeta 𝕜) x_1.fst x_1.snd * f x_1.snd =
    ∑ x_1 ∈ (Ici x).sigma fun z => Icc x z, (mu 𝕜) x x_1.snd * (zeta 𝕜) x_1.snd x_1.fst * f x_1.fst

Tactic:
simp only [mul_boole, MulZeroClass.zero_mul, ite_mul, zeta_apply]

Result:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
⊢ (∑ x_1 ∈ (Ici x).sigma fun y => Ici y, if x_1.fst ≤ x_1.snd then (mu 𝕜) x x_1.fst * f x_1.snd else 0) =
    ∑ x_1 ∈ (Ici x).sigma fun z => Icc x z, if x_1.snd ≤ x_1.fst then (mu 𝕜) x x_1.snd * f x_1.fst else 0

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
⊢ ∑ x_1 ∈ (Ici x).sigma fun y => Ici y, (mu 𝕜) x x_1.fst * (zeta 𝕜) x_1.fst x_1.snd * f x_1.snd =
    ∑ z ∈ Ici x, ∑ y ∈ Icc x z, (mu 𝕜) x y * (zeta 𝕜) y z * f z

Tactic:
rw [sum_sigma' (Ici x) fun z ↦ Icc x z]

Result:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
⊢ ∑ x_1 ∈ (Ici x).sigma fun y => Ici y, (mu 𝕜) x x_1.fst * (zeta 𝕜) x_1.fst x_1.snd * f x_1.snd =
    ∑ x_1 ∈ (Ici x).sigma fun z => Icc x z, (mu 𝕜) x x_1.snd * (zeta 𝕜) x_1.snd x_1.fst * f x_1.fst

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
⊢ ∑ y ∈ Ici x, ∑ z ∈ Ici y, 1 x z * f z = f x

Tactic:
simp [one_apply, ← add_sum_Ioi_eq_sum_Ici]

Result:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
⊢ (∑ x_1 ∈ Ioi x, if x_1 ≤ x then f x else 0) = 0

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
⊢ ∑ z ∈ Ici x, (mu 𝕜 * zeta 𝕜) x z * f z = ∑ y ∈ Ici x, ∑ z ∈ Ici y, 1 x z * f z

Tactic:
simp [mu_mul_zeta 𝕜, ← add_sum_Ioi_eq_sum_Ici]

Result:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
⊢ (∑ x_1 ∈ Ioi x, if x_1 ≤ x then f x else 0) = 0

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
y z : α
hz : z ∈ Ici y
⊢ f z = (zeta 𝕜) y z * f z

Tactic:
rw [zeta_apply, if_pos (mem_Ici.mp ‹_›), one_mul]

Result:
no goals