Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁹ : Preorder α
inst✝⁸ : LocallyFiniteOrder α
inst✝⁷ : AddCommMonoid 𝕜
inst✝⁶ : Monoid 𝕜
inst✝⁵ : Semiring 𝕝
inst✝⁴ : AddCommMonoid 𝕞
inst✝³ : SMul 𝕜 𝕝
inst✝² : Module 𝕝 𝕞
inst✝¹ : DistribMulAction 𝕜 𝕞
inst✝ : IsScalarTower 𝕜 𝕝 𝕞
f : IncidenceAlgebra 𝕜 α
g : IncidenceAlgebra 𝕝 α
h : IncidenceAlgebra 𝕞 α
a b : α
a✝ : a ≤ b
⊢ ∑ x ∈ (Icc a b).sigma (Icc a), (f a x.snd • g x.snd x.fst) • h x.fst b =
    ∑ x ∈ (Icc a b).sigma fun a ↦ Icc a b, f a x.fst • g x.fst x.snd • h x.snd b

Tactic:
apply sum_nbij' (fun ⟨a, b⟩ ↦ ⟨b, a⟩) (fun ⟨a, b⟩ ↦ ⟨b, a⟩)

Goal state after:
case hi
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁹ : Preorder α
inst✝⁸ : LocallyFiniteOrder α
inst✝⁷ : AddCommMonoid 𝕜
inst✝⁶ : Monoid 𝕜
inst✝⁵ : Semiring 𝕝
inst✝⁴ : AddCommMonoid 𝕞
inst✝³ : SMul 𝕜 𝕝
inst✝² : Module 𝕝 𝕞
inst✝¹ : DistribMulAction 𝕜 𝕞
inst✝ : IsScalarTower 𝕜 𝕝 𝕞
f : IncidenceAlgebra 𝕜 α
g : IncidenceAlgebra 𝕝 α
h : IncidenceAlgebra 𝕞 α
a b : α
a✝ : a ≤ b
⊢ ∀ a_1 ∈ (Icc a b).sigma (Icc a),
    (match a_1 with
      | ⟨a, b⟩ => ⟨b, a⟩) ∈
      (Icc a b).sigma fun a ↦ Icc a b

case hj
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁹ : Preorder α
inst✝⁸ : LocallyFiniteOrder α
inst✝⁷ : AddCommMonoid 𝕜
inst✝⁶ : Monoid 𝕜
inst✝⁵ : Semiring 𝕝
inst✝⁴ : AddCommMonoid 𝕞
inst✝³ : SMul 𝕜 𝕝
inst✝² : Module 𝕝 𝕞
inst✝¹ : DistribMulAction 𝕜 𝕞
inst✝ : IsScalarTower 𝕜 𝕝 𝕞
f : IncidenceAlgebra 𝕜 α
g : IncidenceAlgebra 𝕝 α
h : IncidenceAlgebra 𝕞 α
a b : α
a✝ : a ≤ b
⊢ ∀ a_1 ∈ (Icc a b).sigma fun a ↦ Icc a b,
    (match a_1 with
      | ⟨a, b⟩ => ⟨b, a⟩) ∈
      (Icc a b).sigma (Icc a)

case left_neg
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁹ : Preorder α
inst✝⁸ : LocallyFiniteOrder α
inst✝⁷ : AddCommMonoid 𝕜
inst✝⁶ : Monoid 𝕜
inst✝⁵ : Semiring 𝕝
inst✝⁴ : AddCommMonoid 𝕞
inst✝³ : SMul 𝕜 𝕝
inst✝² : Module 𝕝 𝕞
inst✝¹ : DistribMulAction 𝕜 𝕞
inst✝ : IsScalarTower 𝕜 𝕝 𝕞
f : IncidenceAlgebra 𝕜 α
g : IncidenceAlgebra 𝕝 α
h : IncidenceAlgebra 𝕞 α
a b : α
a✝ : a ≤ b
⊢ ∀ a_1 ∈ (Icc a b).sigma (Icc a),
    (match
        match a_1 with
        | ⟨a, b⟩ => ⟨b, a⟩ with
      | ⟨a, b⟩ => ⟨b, a⟩) =
      a_1

case right_neg
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁹ : Preorder α
inst✝⁸ : LocallyFiniteOrder α
inst✝⁷ : AddCommMonoid 𝕜
inst✝⁶ : Monoid 𝕜
inst✝⁵ : Semiring 𝕝
inst✝⁴ : AddCommMonoid 𝕞
inst✝³ : SMul 𝕜 𝕝
inst✝² : Module 𝕝 𝕞
inst✝¹ : DistribMulAction 𝕜 𝕞
inst✝ : IsScalarTower 𝕜 𝕝 𝕞
f : IncidenceAlgebra 𝕜 α
g : IncidenceAlgebra 𝕝 α
h : IncidenceAlgebra 𝕞 α
a b : α
a✝ : a ≤ b
⊢ ∀ a_1 ∈ (Icc a b).sigma fun a ↦ Icc a b,
    (match
        match a_1 with
        | ⟨a, b⟩ => ⟨b, a⟩ with
      | ⟨a, b⟩ => ⟨b, a⟩) =
      a_1

case h
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁹ : Preorder α
inst✝⁸ : LocallyFiniteOrder α
inst✝⁷ : AddCommMonoid 𝕜
inst✝⁶ : Monoid 𝕜
inst✝⁵ : Semiring 𝕝
inst✝⁴ : AddCommMonoid 𝕞
inst✝³ : SMul 𝕜 𝕝
inst✝² : Module 𝕝 𝕞
inst✝¹ : DistribMulAction 𝕜 𝕞
inst✝ : IsScalarTower 𝕜 𝕝 𝕞
f : IncidenceAlgebra 𝕜 α
g : IncidenceAlgebra 𝕝 α
h : IncidenceAlgebra 𝕞 α
a b : α
a✝ : a ≤ b
⊢ ∀ a_1 ∈ (Icc a b).sigma (Icc a),
    (f a a_1.snd • g a_1.snd a_1.fst) • h a_1.fst b =
      f a
          (match a_1 with
            | ⟨a, b⟩ => ⟨b, a⟩).fst •
        g
            (match a_1 with
              | ⟨a, b⟩ => ⟨b, a⟩).fst
            (match a_1 with
              | ⟨a, b⟩ => ⟨b, a⟩).snd •
          h
            (match a_1 with
              | ⟨a, b⟩ => ⟨b, a⟩).snd
            b