Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: case hi
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := ⋯
⊢ ∀ a ∈ (Ici x).sigma fun y ↦ Ici y,
    (match a with
      | ⟨a, b⟩ => ⟨b, a⟩) ∈
      (Ici x).sigma fun z ↦ Icc x z

pp: case hj
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := ⋯
⊢ ∀ a ∈ (Ici x).sigma fun z ↦ Icc x z,
    (match a with
      | ⟨a, b⟩ => ⟨b, a⟩) ∈
      (Ici x).sigma fun y ↦ Ici y

pp: case left_neg
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := ⋯
⊢ ∀ a ∈ (Ici x).sigma fun y ↦ Ici y,
    (match
        match a with
        | ⟨a, b⟩ => ⟨b, a⟩ with
      | ⟨a, b⟩ => ⟨b, a⟩) =
      a

pp: case right_neg
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := ⋯
⊢ ∀ a ∈ (Ici x).sigma fun z ↦ Icc x z,
    (match
        match a with
        | ⟨a, b⟩ => ⟨b, a⟩ with
      | ⟨a, b⟩ => ⟨b, a⟩) =
      a

pp: case h
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := ⋯
⊢ ∀ a ∈ (Ici x).sigma fun y ↦ Ici y,
    (if a.fst ≤ a.snd then (mu 𝕜) x a.fst * f a.snd else 0) =
      if
          (match a with
              | ⟨a, b⟩ => ⟨b, a⟩).snd ≤
            (match a with
              | ⟨a, b⟩ => ⟨b, a⟩).fst then
        (mu 𝕜) x
            (match a with
              | ⟨a, b⟩ => ⟨b, a⟩).snd *
          f
            (match a with
              | ⟨a, b⟩ => ⟨b, a⟩).fst
      else 0

Tactic:
<;>

Goal state after:
case hi
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := ⋯
⊢ ∀ a ∈ (Ici x).sigma fun y ↦ Ici y,
    (match a with
      | ⟨a, b⟩ => ⟨b, a⟩) ∈
      (Ici x).sigma fun z ↦ Icc x z

case hj
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := ⋯
⊢ ∀ a ∈ (Ici x).sigma fun z ↦ Icc x z,
    (match a with
      | ⟨a, b⟩ => ⟨b, a⟩) ∈
      (Ici x).sigma fun y ↦ Ici y

case left_neg
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := ⋯
⊢ ∀ a ∈ (Ici x).sigma fun y ↦ Ici y,
    (match
        match a with
        | ⟨a, b⟩ => ⟨b, a⟩ with
      | ⟨a, b⟩ => ⟨b, a⟩) =
      a

case right_neg
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := ⋯
⊢ ∀ a ∈ (Ici x).sigma fun z ↦ Icc x z,
    (match
        match a with
        | ⟨a, b⟩ => ⟨b, a⟩ with
      | ⟨a, b⟩ => ⟨b, a⟩) =
      a

case h
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := ⋯
⊢ ∀ a ∈ (Ici x).sigma fun y ↦ Ici y,
    (if a.fst ≤ a.snd then (mu 𝕜) x a.fst * f a.snd else 0) =
      if
          (match a with
              | ⟨a, b⟩ => ⟨b, a⟩).snd ≤
            (match a with
              | ⟨a, b⟩ => ⟨b, a⟩).fst then
        (mu 𝕜) x
            (match a with
              | ⟨a, b⟩ => ⟨b, a⟩).snd *
          f
            (match a with
              | ⟨a, b⟩ => ⟨b, a⟩).fst
      else 0