Theorem: IncidenceAlgebra.moebius_inversion_top (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✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ f x = ∑ y ∈ Ici x, (mu 𝕜) x y * g y
Tactic:
symm
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✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ ∑ y ∈ Ici x, (mu 𝕜) x y * g y = f x

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✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ ∑ y ∈ Ici x, (mu 𝕜) x y * g y = f x
Tactic:
calc
  ∑ y in Ici x, mu 𝕜 x y * g y = ∑ y in Ici x, mu 𝕜 x y * ∑ z in Ici y, f z := by simp_rw [h]
  _ = ∑ y in Ici x, mu 𝕜 x y * ∑ z in 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 in Ici x, ∑ z in Ici y, mu 𝕜 x y * zeta 𝕜 y z * f z := by simp [mul_sum]
  _ = ∑ z in Ici x, ∑ y in Icc x z, mu 𝕜 x y * zeta 𝕜 y z * f z := by
    erw [sum_sigma' (Ici x) fun y ↦ Ici y]
    erw [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 in Ici x, (mu 𝕜 * zeta 𝕜 : IncidenceAlgebra 𝕜 α) x z * f z := by
    simp_rw [mul_apply, sum_mul]
  _ = ∑ y in Ici x, ∑ z in Ici y, (1 : IncidenceAlgebra 𝕜 α) x z * f z := by
    simp [mu_mul_zeta 𝕜, ← add_sum_Ioi]
    exact sum_eq_zero fun y hy ↦ if_neg (mem_Ioi.mp hy).not_le
  _ = f x := by
    simp [one_apply, ← add_sum_Ioi]
    exact sum_eq_zero fun y hy ↦ if_neg (mem_Ioi.mp hy).not_le
State after:
no goals

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✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ ∑ y ∈ Ici x, (mu 𝕜) x y * g y = ∑ y ∈ Ici x, (mu 𝕜) x y * ∑ z ∈ Ici y, f z
Tactic:
simp_rw [h]
State after:
no goals

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✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ ∑ 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
State after:
case e_f.h
𝕄 : 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✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
y : α
⊢ (mu 𝕜) x y * ∑ z ∈ Ici y, f z = (mu 𝕜) x y * ∑ z ∈ Ici y, (zeta 𝕜) y z * f z

State before:
case e_f.h
𝕄 : 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✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
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 ↦ ?_]
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✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
y z : α
hz : z ∈ Ici y
⊢ f z = (zeta 𝕜) y z * f z

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✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
y z : α
hz : z ∈ Ici y
⊢ f z = (zeta 𝕜) y z * f z
Tactic:
rw [zeta_apply, if_pos (mem_Ici.mp ‹_›), one_mul]
State after:
no goals

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✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ ∑ 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]
State after:
no goals

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✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ ∑ 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:
erw [sum_sigma' (Ici x) fun y ↦ Ici y]
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✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ ∑ 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

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✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ ∑ 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:
erw [sum_sigma' (Ici x) fun z ↦ Icc x z]
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✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ ∑ 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

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✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ ∑ 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]
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✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ (∑ 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

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✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ (∑ 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)
State after:
no goals

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✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ ∑ 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]
State after:
no goals

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✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ ∑ 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]
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✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ (∑ x_1 ∈ Ioi x, if x_1 ≤ x then f x else 0) = 0

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✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ (∑ 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
State after:
no goals

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✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ ∑ y ∈ Ici x, ∑ z ∈ Ici y, 1 x z * f z = f x
Tactic:
simp [one_apply, ← add_sum_Ioi]
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✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ (∑ x_1 ∈ Ioi x, if x_1 ≤ x then f x else 0) = 0