Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁸ : AddCommMonoid Γ
inst✝⁷ : PartialOrder Γ
inst✝⁶ : IsOrderedCancelAddMonoid Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddAction Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Semiring R
inst✝ : Module R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
b : Γ'
⊢ ∑ x_1 ∈ (VAddAntidiagonal b ⋯).sigma fun a ↦ antidiagonal ⋯ ⋯ a.1,
      (x.coeff x_1.snd.1 * y.coeff x_1.snd.2) • ((of R).symm z).coeff x_1.fst.2 =
    ∑ x_1 ∈ (VAddAntidiagonal b ⋯).sigma fun a ↦ VAddAntidiagonal a.2 ⋯,
      x.coeff x_1.fst.1 • y.coeff x_1.snd.1 • ((of R).symm z).coeff x_1.snd.2

Tactic:
apply Finset.sum_nbij' (fun ⟨⟨_i, j⟩, ⟨k, l⟩⟩ ↦ ⟨(k, l +ᵥ j), (l, j)⟩)
    (fun ⟨⟨i, _j⟩, ⟨k, l⟩⟩ ↦ ⟨(i + k, l), (i, k)⟩)

Goal state after:
case hi
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁸ : AddCommMonoid Γ
inst✝⁷ : PartialOrder Γ
inst✝⁶ : IsOrderedCancelAddMonoid Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddAction Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Semiring R
inst✝ : Module R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
b : Γ'
⊢ ∀ a ∈ (VAddAntidiagonal b ⋯).sigma fun a ↦ antidiagonal ⋯ ⋯ a.1,
    (match a with
      | ⟨(_i, j), (k, l)⟩ => ⟨(k, l +ᵥ j), (l, j)⟩) ∈
      (VAddAntidiagonal b ⋯).sigma fun a ↦ VAddAntidiagonal a.2 ⋯

case hj
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁸ : AddCommMonoid Γ
inst✝⁷ : PartialOrder Γ
inst✝⁶ : IsOrderedCancelAddMonoid Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddAction Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Semiring R
inst✝ : Module R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
b : Γ'
⊢ ∀ a ∈ (VAddAntidiagonal b ⋯).sigma fun a ↦ VAddAntidiagonal a.2 ⋯,
    (match a with
      | ⟨(i, _j), (k, l)⟩ => ⟨(i + k, l), (i, k)⟩) ∈
      (VAddAntidiagonal b ⋯).sigma fun a ↦ antidiagonal ⋯ ⋯ a.1

case left_neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁸ : AddCommMonoid Γ
inst✝⁷ : PartialOrder Γ
inst✝⁶ : IsOrderedCancelAddMonoid Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddAction Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Semiring R
inst✝ : Module R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
b : Γ'
⊢ ∀ a ∈ (VAddAntidiagonal b ⋯).sigma fun a ↦ antidiagonal ⋯ ⋯ a.1,
    (match
        match a with
        | ⟨(_i, j), (k, l)⟩ => ⟨(k, l +ᵥ j), (l, j)⟩ with
      | ⟨(i, _j), (k, l)⟩ => ⟨(i + k, l), (i, k)⟩) =
      a

case right_neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁸ : AddCommMonoid Γ
inst✝⁷ : PartialOrder Γ
inst✝⁶ : IsOrderedCancelAddMonoid Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddAction Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Semiring R
inst✝ : Module R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
b : Γ'
⊢ ∀ a ∈ (VAddAntidiagonal b ⋯).sigma fun a ↦ VAddAntidiagonal a.2 ⋯,
    (match
        match a with
        | ⟨(i, _j), (k, l)⟩ => ⟨(i + k, l), (i, k)⟩ with
      | ⟨(_i, j), (k, l)⟩ => ⟨(k, l +ᵥ j), (l, j)⟩) =
      a

case h
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁸ : AddCommMonoid Γ
inst✝⁷ : PartialOrder Γ
inst✝⁶ : IsOrderedCancelAddMonoid Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddAction Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Semiring R
inst✝ : Module R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
b : Γ'
⊢ ∀ a ∈ (VAddAntidiagonal b ⋯).sigma fun a ↦ antidiagonal ⋯ ⋯ a.1,
    (x.coeff a.snd.1 * y.coeff a.snd.2) • ((of R).symm z).coeff a.fst.2 =
      x.coeff
          (match a with
              | ⟨(_i, j), (k, l)⟩ => ⟨(k, l +ᵥ j), (l, j)⟩).fst.1 •
        y.coeff
            (match a with
                | ⟨(_i, j), (k, l)⟩ => ⟨(k, l +ᵥ j), (l, j)⟩).snd.1 •
          ((of R).symm z).coeff
            (match a with
                | ⟨(_i, j), (k, l)⟩ => ⟨(k, l +ᵥ j), (l, j)⟩).snd.2