-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem coeff_smul_left [SMulWithZero R V] {x : HahnSeries Γ R}
    {y : HahnModule Γ' R V} {a : Γ'} {s : Set Γ}
    (hs : s.IsPWO) (hxs : x.support ⊆ s) :
    ((of R).symm <| x • y).coeff a =
      ∑ ij ∈ VAddAntidiagonal hs ((of R).symm y).isPWO_support 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✝ : SMulWithZero R V
x : HahnSeries Γ R
y : HahnModule Γ' R V
a : Γ'
s : Set Γ
hs : s.IsPWO
hxs : x.support ⊆ s
b : Γ × Γ'
hb :
  (b.1 ∈ s ∧ ((of R).symm y).coeff b.2 ≠ 0 ∧ b.1 +ᵥ b.2 = a) ∧
    (((of R).symm y).coeff b.2 ≠ 0 ∧ b.1 +ᵥ b.2 = a → x.coeff b.1 = 0)
⊢ x.coeff b.1 • ((of R).symm y).coeff b.2 = 0

Tactic:
rw [hb.2 ⟨hb.1.2.1, hb.1.2.2⟩, zero_smul]

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✝ : SMulWithZero R V
x : HahnSeries Γ R
y : HahnModule Γ' R V
a : Γ'
s : Set Γ
hs : s.IsPWO
hxs : x.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_left hxs) _ fun _ _ => rfl
intro b hb
simp only [not_and', mem_sdiff, mem_vaddAntidiagonal, HahnSeries.mem_support, not_ne_iff] at hb
rw [hb.2 ⟨hb.1.2.1, hb.1.2.2⟩, zero_smul]

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✝ : SMulWithZero R V
x : HahnSeries Γ R
y : HahnModule Γ' R V
a : Γ'
s : Set Γ
hs : s.IsPWO
hxs : x.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✝ : SMulWithZero R V
x : HahnSeries Γ R
y : HahnModule Γ' R V
a : Γ'
s : Set Γ
hs : s.IsPWO
hxs : x.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✝ : SMulWithZero R V
x : HahnSeries Γ R
y : HahnModule Γ' R V
a : Γ'
s : Set Γ
hs : s.IsPWO
hxs : x.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_left hxs) _ 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✝ : SMulWithZero R V
x : HahnSeries Γ R
y : HahnModule Γ' R V
a : Γ'
s : Set Γ
hs : s.IsPWO
hxs : x.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✝ : SMulWithZero R V
x : HahnSeries Γ R
y : HahnModule Γ' R V
a : Γ'
s : Set Γ
hs : s.IsPWO
hxs : x.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_ne_iff] 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✝ : SMulWithZero R V
x : HahnSeries Γ R
y : HahnModule Γ' R V
a : Γ'
s : Set Γ
hs : s.IsPWO
hxs : x.support ⊆ s
b : Γ × Γ'
hb :
  (b.1 ∈ s ∧ ((of R).symm y).coeff b.2 ≠ 0 ∧ b.1 +ᵥ b.2 = a) ∧
    (((of R).symm y).coeff b.2 ≠ 0 ∧ b.1 +ᵥ b.2 = a → x.coeff b.1 = 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✝ : SMulWithZero R V
x : HahnSeries Γ R
y : HahnModule Γ' R V
a : Γ'
s : Set Γ
hs : s.IsPWO
hxs : x.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✝ : SMulWithZero R V
x : HahnSeries Γ R
y : HahnModule Γ' R V
a : Γ'
s : Set Γ
hs : s.IsPWO
hxs : x.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