-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem coeff_smul_right [SMulZeroClass R V] {x : HahnSeries Γ R} {y : HahnModule Γ' R V} {a : Γ'}
    {s : Set Γ'} (hs : s.IsPWO) (hys : ((of R).symm y).support ⊆ s) :
    ((of R).symm <| x • y).coeff a =
      ∑ ij ∈ VAddAntidiagonal x.isPWO_support hs a,
        x.coeff ij.fst • ((of R).symm y).coeff ij.snd

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✝¹ : Zero R
inst✝ : SMulZeroClass R V
x : HahnSeries Γ R
y : HahnModule Γ' R V
a : Γ'
s : Set Γ'
hs : s.IsPWO
hys : ((of R).symm y).support ⊆ s
⊢ ((of R).symm (x • y)).coeff a = ∑ ij ∈ VAddAntidiagonal ⋯ hs a, x.coeff ij.1 • ((of R).symm y).coeff ij.2

Tactic:
classical
rw [coeff_smul]
apply sum_subset_zero_on_sdiff (vaddAntidiagonal_mono_right hys) _ fun _ _ => rfl
intro b hb
simp only [not_and, mem_sdiff, mem_vaddAntidiagonal, HahnSeries.mem_support, not_imp_not] at hb
rw [hb.2 hb.1.1 hb.1.2.2, smul_zero]

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✝¹ : Zero R
inst✝ : SMulZeroClass R V
x : HahnSeries Γ R
y : HahnModule Γ' R V
a : Γ'
s : Set Γ'
hs : s.IsPWO
hys : ((of R).symm y).support ⊆ s
b : Γ × Γ'
hb : (x.coeff b.1 ≠ 0 ∧ b.2 ∈ s ∧ b.1 +ᵥ b.2 = a) ∧ (x.coeff b.1 ≠ 0 → b.1 +ᵥ b.2 = a → ((of R).symm y).coeff b.2 = 0)
⊢ x.coeff b.1 • ((of R).symm y).coeff b.2 = 0

Tactic:
rw [hb.2 hb.1.1 hb.1.2.2, smul_zero]

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✝¹ : Zero R
inst✝ : SMulZeroClass R V
x : HahnSeries Γ R
y : HahnModule Γ' R V
a : Γ'
s : Set Γ'
hs : s.IsPWO
hys : ((of R).symm y).support ⊆ s
b : Γ × Γ'
hb : b ∈ VAddAntidiagonal ⋯ hs a \ VAddAntidiagonal ⋯ ⋯ a
⊢ x.coeff b.1 • ((of R).symm y).coeff b.2 = 0

Tactic:
simp only [not_and, mem_sdiff, mem_vaddAntidiagonal, HahnSeries.mem_support, not_imp_not] at hb

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✝¹ : Zero R
inst✝ : SMulZeroClass R V
x : HahnSeries Γ R
y : HahnModule Γ' R V
a : Γ'
s : Set Γ'
hs : s.IsPWO
hys : ((of R).symm y).support ⊆ s
b : Γ × Γ'
hb : (x.coeff b.1 ≠ 0 ∧ b.2 ∈ s ∧ b.1 +ᵥ b.2 = a) ∧ (x.coeff b.1 ≠ 0 → b.1 +ᵥ b.2 = a → ((of R).symm y).coeff b.2 = 0)
⊢ x.coeff b.1 • ((of R).symm y).coeff b.2 = 0

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✝¹ : Zero R
inst✝ : SMulZeroClass R V
x : HahnSeries Γ R
y : HahnModule Γ' R V
a : Γ'
s : Set Γ'
hs : s.IsPWO
hys : ((of R).symm y).support ⊆ s
⊢ ∀ x_1 ∈ VAddAntidiagonal ⋯ hs a \ VAddAntidiagonal ⋯ ⋯ a, x.coeff x_1.1 • ((of R).symm y).coeff x_1.2 = 0

Tactic:
intro b hb

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✝¹ : Zero R
inst✝ : SMulZeroClass R V
x : HahnSeries Γ R
y : HahnModule Γ' R V
a : Γ'
s : Set Γ'
hs : s.IsPWO
hys : ((of R).symm y).support ⊆ s
b : Γ × Γ'
hb : b ∈ VAddAntidiagonal ⋯ hs a \ VAddAntidiagonal ⋯ ⋯ a
⊢ x.coeff b.1 • ((of R).symm y).coeff b.2 = 0

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✝¹ : Zero R
inst✝ : SMulZeroClass R V
x : HahnSeries Γ R
y : HahnModule Γ' R V
a : Γ'
s : Set Γ'
hs : s.IsPWO
hys : ((of R).symm y).support ⊆ s
⊢ ∑ ij ∈ VAddAntidiagonal ⋯ ⋯ a, x.coeff ij.1 • ((of R).symm y).coeff ij.2 =
    ∑ ij ∈ VAddAntidiagonal ⋯ hs a, x.coeff ij.1 • ((of R).symm y).coeff ij.2

Tactic:
apply sum_subset_zero_on_sdiff (vaddAntidiagonal_mono_right hys) _ 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✝¹ : Zero R
inst✝ : SMulZeroClass R V
x : HahnSeries Γ R
y : HahnModule Γ' R V
a : Γ'
s : Set Γ'
hs : s.IsPWO
hys : ((of R).symm y).support ⊆ s
⊢ ∀ x_1 ∈ VAddAntidiagonal ⋯ hs a \ VAddAntidiagonal ⋯ ⋯ a, x.coeff x_1.1 • ((of R).symm y).coeff x_1.2 = 0

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✝¹ : Zero R
inst✝ : SMulZeroClass R V
x : HahnSeries Γ R
y : HahnModule Γ' R V
a : Γ'
s : Set Γ'
hs : s.IsPWO
hys : ((of R).symm y).support ⊆ s
⊢ ((of R).symm (x • y)).coeff a = ∑ ij ∈ VAddAntidiagonal ⋯ hs a, x.coeff ij.1 • ((of R).symm y).coeff ij.2

Tactic:
rw [coeff_smul]

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✝¹ : Zero R
inst✝ : SMulZeroClass R V
x : HahnSeries Γ R
y : HahnModule Γ' R V
a : Γ'
s : Set Γ'
hs : s.IsPWO
hys : ((of R).symm y).support ⊆ s
⊢ ∑ ij ∈ VAddAntidiagonal ⋯ ⋯ a, x.coeff ij.1 • ((of R).symm y).coeff ij.2 =
    ∑ ij ∈ VAddAntidiagonal ⋯ hs a, x.coeff ij.1 • ((of R).symm y).coeff ij.2