-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem coeff_single_smul_vadd [MulZeroClass R] [SMulWithZero R V] {r : R} {x : HahnModule Γ' R V}
    {a : Γ'} {b : Γ} :
    ((of R).symm (HahnSeries.single b r • x)).coeff (b +ᵥ a) = r • ((of R).symm x).coeff a

Proof state:
case h.mk
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : ((of R).symm x).coeff a = 0
a1 : Γ
a2 : Γ'
⊢ (a1, a2) ∈ VAddAntidiagonal ⋯ ⋯ (b +ᵥ a) ↔ (a1, a2) ∈ ∅

Tactic:
simp only [not_mem_empty, not_and, Set.mem_singleton_iff, Classical.not_not,
  mem_vaddAntidiagonal, Set.mem_setOf_eq, iff_false]

Result:
case h.mk
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : ((of R).symm x).coeff a = 0
a1 : Γ
a2 : Γ'
⊢ a1 = b → a2 ∈ ((of R).symm x).support → ¬a1 +ᵥ a2 = b +ᵥ a

Proof state:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : ¬((of R).symm x).coeff a = 0
⊢ ∑ x_1 ∈ VAddAntidiagonal ⋯ ⋯ (b +ᵥ a), ((HahnSeries.single b) r).coeff x_1.1 • ((of R).symm x).coeff x_1.2 =
    ∑ ij ∈ {(b, a)}, ((HahnSeries.single b) r).coeff ij.1 • ((of R).symm x).coeff ij.2

Tactic:
apply sum_congr _ fun _ _ => rfl

Result:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : ¬((of R).symm x).coeff a = 0
⊢ VAddAntidiagonal ⋯ ⋯ (b +ᵥ a) = {(b, a)}

Proof state:
case h.mk.mpr
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : ¬((of R).symm x).coeff a = 0
a1 : Γ
a2 : Γ'
⊢ a1 = b ∧ a2 = a → a1 = b ∧ a2 ∈ ((of R).symm x).support ∧ a1 +ᵥ a2 = b +ᵥ a

Tactic:
rintro ⟨rfl, rfl⟩

Result:
case h.mk.mpr.intro
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
hr : ¬r = 0
a1 : Γ
a2 : Γ'
hx : ¬((of R).symm x).coeff a2 = 0
⊢ a1 = a1 ∧ a2 ∈ ((of R).symm x).support ∧ a1 +ᵥ a2 = a1 +ᵥ a2

Proof state:
case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : ¬((of R).symm x).coeff a = 0
⊢ ∑ x_1 ∈ VAddAntidiagonal ⋯ ⋯ (b +ᵥ a), ((HahnSeries.single b) r).coeff x_1.1 • ((of R).symm x).coeff x_1.2 =
    r • ((of R).symm x).coeff a

Tactic:
trans ∑ ij ∈ {(b, a)},
  (HahnSeries.single b r).coeff ij.fst • ((of R).symm x).coeff ij.snd

Result:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : ¬((of R).symm x).coeff a = 0
⊢ ∑ x_1 ∈ VAddAntidiagonal ⋯ ⋯ (b +ᵥ a), ((HahnSeries.single b) r).coeff x_1.1 • ((of R).symm x).coeff x_1.2 =
    ∑ ij ∈ {(b, a)}, ((HahnSeries.single b) r).coeff ij.1 • ((of R).symm x).coeff ij.2

Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : ¬((of R).symm x).coeff a = 0
⊢ ∑ ij ∈ {(b, a)}, ((HahnSeries.single b) r).coeff ij.1 • ((of R).symm x).coeff ij.2 = r • ((of R).symm x).coeff a

Proof state:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
hr : ¬r = 0
a1 : Γ
a2 : Γ'
hx : ¬((of R).symm x).coeff a2 = 0
⊢ a2 ∈ ((of R).symm x).support

Tactic:
exact hx

Result:
no goals

Proof state:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : ¬((of R).symm x).coeff a = 0
⊢ VAddAntidiagonal ⋯ ⋯ (b +ᵥ a) = {(b, a)}

Tactic:
ext ⟨a1, a2⟩

Result:
case h.mk
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : ¬((of R).symm x).coeff a = 0
a1 : Γ
a2 : Γ'
⊢ (a1, a2) ∈ VAddAntidiagonal ⋯ ⋯ (b +ᵥ a) ↔ (a1, a2) ∈ {(b, a)}

Proof state:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : ¬((of R).symm x).coeff a = 0
⊢ ∑ ij ∈ {(b, a)}, ((HahnSeries.single b) r).coeff ij.1 • ((of R).symm x).coeff ij.2 = r • ((of R).symm x).coeff a

Tactic:
simp

Result:
no goals

Proof state:
case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : ((of R).symm x).coeff a = 0
⊢ ∑ x_1 ∈ VAddAntidiagonal ⋯ ⋯ (b +ᵥ a), ((HahnSeries.single b) r).coeff x_1.1 • ((of R).symm x).coeff x_1.2 =
    r • ((of R).symm x).coeff a

Tactic:
simp only [hx, smul_zero]

Result:
case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : ((of R).symm x).coeff a = 0
⊢ ∑ x_1 ∈ VAddAntidiagonal ⋯ ⋯ (b +ᵥ a), ((HahnSeries.single b) r).coeff x_1.1 • ((of R).symm x).coeff x_1.2 = 0