Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case hi
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∀ a ∈ (antidiagonal n).sigma fun a ↦ antidiagonal a.1,
    (match a with
      | ⟨(_i, j), (k, l)⟩ => ⟨(k, l + j), (l, j)⟩) ∈
      (antidiagonal n).sigma fun a ↦ antidiagonal a.2

pp: case hj
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∀ a ∈ (antidiagonal n).sigma fun a ↦ antidiagonal a.2,
    (match a with
      | ⟨(i, _j), (k, l)⟩ => ⟨(i + k, l), (i, k)⟩) ∈
      (antidiagonal n).sigma fun a ↦ antidiagonal a.1

pp: case left_neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∀ a ∈ (antidiagonal n).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_2
inst✝ : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∀ a ∈ (antidiagonal n).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_2
inst✝ : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∀ a ∈ (antidiagonal n).sigma fun a ↦ antidiagonal a.1,
    (coeff a.snd.1) φ₁ * (coeff a.snd.2) φ₂ * (coeff a.fst.2) φ₃ =
      (coeff
            (match a with
                | ⟨(_i, j), (k, l)⟩ => ⟨(k, l + j), (l, j)⟩).fst.1)
          φ₁ *
        ((coeff
              (match a with
                  | ⟨(_i, j), (k, l)⟩ => ⟨(k, l + j), (l, j)⟩).snd.1)
            φ₂ *
          (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_2
inst✝ : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∀ a ∈ (antidiagonal n).sigma fun a ↦ antidiagonal a.1,
    (match a with
      | ⟨(_i, j), (k, l)⟩ => ⟨(k, l + j), (l, j)⟩) ∈
      (antidiagonal n).sigma fun a ↦ antidiagonal a.2

case hj
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∀ a ∈ (antidiagonal n).sigma fun a ↦ antidiagonal a.2,
    (match a with
      | ⟨(i, _j), (k, l)⟩ => ⟨(i + k, l), (i, k)⟩) ∈
      (antidiagonal n).sigma fun a ↦ antidiagonal a.1

case left_neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∀ a ∈ (antidiagonal n).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_2
inst✝ : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∀ a ∈ (antidiagonal n).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_2
inst✝ : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∀ a ∈ (antidiagonal n).sigma fun a ↦ antidiagonal a.1,
    (coeff a.snd.1) φ₁ * (coeff a.snd.2) φ₂ * (coeff a.fst.2) φ₃ =
      (coeff
            (match a with
                | ⟨(_i, j), (k, l)⟩ => ⟨(k, l + j), (l, j)⟩).fst.1)
          φ₁ *
        ((coeff
              (match a with
                  | ⟨(_i, j), (k, l)⟩ => ⟨(k, l + j), (l, j)⟩).snd.1)
            φ₂ *
          (coeff
              (match a with
                  | ⟨(_i, j), (k, l)⟩ => ⟨(k, l + j), (l, j)⟩).snd.2)
            φ₃)