-- 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
⊢ ∑ y ∈ Ici x, (mu 𝕜) x y * ∑ z ∈ Ici y, f z = ∑ y ∈ Ici x, (mu 𝕜) x y * ∑ z ∈ Ici y, (zeta 𝕜) y z * f z

Tactic:
congr with y

Result:
case e_f.h
𝕜 : 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 : α
⊢ (mu 𝕜) x y * ∑ z ∈ Ici y, f z = (mu 𝕜) x y * ∑ z ∈ Ici y, (zeta 𝕜) y z * f z

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, (mu 𝕜) x y * g y = ∑ y ∈ Ici x, (mu 𝕜) x y * ∑ z ∈ Ici y, f z

Tactic:
simp_rw [h]

Result:
no goals

Proof state:
case e_f.h
𝕜 : 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 : α
⊢ (mu 𝕜) x y * ∑ z ∈ Ici y, f z = (mu 𝕜) x y * ∑ z ∈ Ici y, (zeta 𝕜) y z * f z

Tactic:
rw [sum_congr rfl fun z hz ↦ ?_]

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
y z : α
hz : z ∈ Ici y
⊢ f z = (zeta 𝕜) y z * f z

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 ∈ Ioi x, if x_1 ≤ x then f x else 0) = 0

Tactic:
exact sum_eq_zero fun y hy ↦ if_neg (mem_Ioi.mp hy).not_le

Result:
no goals

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, (mu 𝕜) x y * ∑ z ∈ Ici y, (zeta 𝕜) y z * f z = ∑ y ∈ Ici x, ∑ z ∈ Ici y, (mu 𝕜) x y * (zeta 𝕜) y z * f z

Tactic:
simp [mul_sum]

Result:
no goals

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, 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

Tactic:
apply sum_nbij' (fun ⟨a, b⟩ ↦ ⟨b, a⟩) (fun ⟨a, b⟩ ↦ ⟨b, a⟩) <;>
  aesop (add simp mul_assoc) (add unsafe le_trans)

Result:
no goals

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, (mu 𝕜) x y * g y = f x

Tactic:
calc
  ∑ y ∈ Ici x, mu 𝕜 x y * g y = ∑ y ∈ Ici x, mu 𝕜 x y * ∑ z ∈ Ici y, f z := by simp_rw [h]
  _ = ∑ y ∈ Ici x, mu 𝕜 x y * ∑ z ∈ Ici y, zeta 𝕜 y z * f z := by
    congr with y
    rw [sum_congr rfl fun z hz ↦ ?_]
    rw [zeta_apply, if_pos (mem_Ici.mp ‹_›), one_mul]
  _ = ∑ y ∈ Ici x, ∑ z ∈ Ici y, mu 𝕜 x y * zeta 𝕜 y z * f z := by simp [mul_sum]
  _ = ∑ z ∈ Ici x, ∑ y ∈ Icc x z, mu 𝕜 x y * zeta 𝕜 y z * f z := by
    rw [sum_sigma' (Ici x) fun y ↦ Ici y]
    rw [sum_sigma' (Ici x) fun z ↦ Icc x z]
    simp only [mul_boole, MulZeroClass.zero_mul, ite_mul, zeta_apply]
    apply sum_nbij' (fun ⟨a, b⟩ ↦ ⟨b, a⟩) (fun ⟨a, b⟩ ↦ ⟨b, a⟩) <;>
      aesop (add simp mul_assoc) (add unsafe le_trans)
  _ = ∑ z ∈ Ici x, (mu 𝕜 * zeta 𝕜 : IncidenceAlgebra 𝕜 α) x z * f z := by
    simp_rw [mul_apply, sum_mul]
  _ = ∑ y ∈ Ici x, ∑ z ∈ Ici y, (1 : IncidenceAlgebra 𝕜 α) x z * f z := by
    simp [mu_mul_zeta 𝕜, ← add_sum_Ioi_eq_sum_Ici]
    exact sum_eq_zero fun y hy ↦ if_neg (mem_Ioi.mp hy).not_le
  _ = f x := by
    simp [one_apply, ← add_sum_Ioi_eq_sum_Ici]
    exact sum_eq_zero fun y hy ↦ if_neg (mem_Ioi.mp hy).not_le

Result:
no goals

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, ∑ y ∈ Icc x z, (mu 𝕜) x y * (zeta 𝕜) y z * f z = ∑ z ∈ Ici x, (mu 𝕜 * zeta 𝕜) x z * f z

Tactic:
simp_rw [mul_apply, sum_mul]

Result:
no goals

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, (mu 𝕜) x y * (zeta 𝕜) y z * f z =
    ∑ z ∈ Ici x, ∑ y ∈ Icc x z, (mu 𝕜) x y * (zeta 𝕜) y z * f z

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

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 =
    ∑ z ∈ Ici x, ∑ y ∈ Icc x z, (mu 𝕜) x y * (zeta 𝕜) y z * f z

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
⊢ f x = ∑ y ∈ Ici x, (mu 𝕜) x y * g y

Tactic:
symm

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
⊢ ∑ y ∈ Ici x, (mu 𝕜) x y * g y = f x