Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case hi
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : R⟦Γ⟧
b : Γ
⊢ ∀ a ∈ (antidiagonal ⋯ ⋯ b).sigma fun a ↦ antidiagonal ⋯ ⋯ a.1,
    (match a with
      | ⟨(_i, j), (k, l)⟩ => ⟨(k, l + j), (l, j)⟩) ∈
      (antidiagonal ⋯ ⋯ b).sigma fun a ↦ antidiagonal ⋯ ⋯ a.2

pp: case hj
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : R⟦Γ⟧
b : Γ
⊢ ∀ a ∈ (antidiagonal ⋯ ⋯ b).sigma fun a ↦ antidiagonal ⋯ ⋯ a.2,
    (match a with
      | ⟨(i, _j), (k, l)⟩ => ⟨(i + k, l), (i, k)⟩) ∈
      (antidiagonal ⋯ ⋯ b).sigma fun a ↦ antidiagonal ⋯ ⋯ a.1

pp: case left_neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : R⟦Γ⟧
b : Γ
⊢ ∀ a ∈ (antidiagonal ⋯ ⋯ 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

pp: case right_neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : R⟦Γ⟧
b : Γ
⊢ ∀ a ∈ (antidiagonal ⋯ ⋯ b).sigma fun a ↦ antidiagonal ⋯ ⋯ 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

pp: case h
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : R⟦Γ⟧
b : Γ
⊢ ∀ a ∈ (antidiagonal ⋯ ⋯ b).sigma fun a ↦ antidiagonal ⋯ ⋯ a.1,
    x.coeff a.snd.1 * y.coeff a.snd.2 * 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 *
          z.coeff
            (match a with
                | ⟨(_i, j), (k, l)⟩ => ⟨(k, l + j), (l, j)⟩).snd.2)

Tactic:
<;>

Goal state after:
case hi
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : R⟦Γ⟧
b : Γ
⊢ ∀ a ∈ (antidiagonal ⋯ ⋯ b).sigma fun a ↦ antidiagonal ⋯ ⋯ a.1,
    (match a with
      | ⟨(_i, j), (k, l)⟩ => ⟨(k, l + j), (l, j)⟩) ∈
      (antidiagonal ⋯ ⋯ b).sigma fun a ↦ antidiagonal ⋯ ⋯ a.2

case hj
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : R⟦Γ⟧
b : Γ
⊢ ∀ a ∈ (antidiagonal ⋯ ⋯ b).sigma fun a ↦ antidiagonal ⋯ ⋯ a.2,
    (match a with
      | ⟨(i, _j), (k, l)⟩ => ⟨(i + k, l), (i, k)⟩) ∈
      (antidiagonal ⋯ ⋯ b).sigma fun a ↦ antidiagonal ⋯ ⋯ a.1

case left_neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : R⟦Γ⟧
b : Γ
⊢ ∀ a ∈ (antidiagonal ⋯ ⋯ 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
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : R⟦Γ⟧
b : Γ
⊢ ∀ a ∈ (antidiagonal ⋯ ⋯ b).sigma fun a ↦ antidiagonal ⋯ ⋯ 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
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : R⟦Γ⟧
b : Γ
⊢ ∀ a ∈ (antidiagonal ⋯ ⋯ b).sigma fun a ↦ antidiagonal ⋯ ⋯ a.1,
    x.coeff a.snd.1 * y.coeff a.snd.2 * 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 *
          z.coeff
            (match a with
                | ⟨(_i, j), (k, l)⟩ => ⟨(k, l + j), (l, j)⟩).snd.2)