-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem add_smul [AddCommMonoid R] [SMulWithZero R V] {x y : HahnSeries Γ R}
    {z : HahnModule Γ' R V} (h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u) :
    (x + y) • z = x • z + y • z

Proof state:
case h.h
Γ : 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✝¹ : AddCommMonoid R
inst✝ : SMulWithZero R V
x y : HahnSeries Γ R
z : HahnModule Γ' R V
h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u
a : Γ'
hwf : (x.support ∪ y.support).IsPWO
⊢ ∑ x_1 ∈ VAddAntidiagonal hwf ⋯ a,
      (x.coeff x_1.1 • ((of R).symm z).coeff x_1.2 + y.coeff x_1.1 • ((of R).symm z).coeff x_1.2) =
    ((of R).symm (x • z)).coeff a + ((of R).symm (y • z)).coeff a

Tactic:
rw [coeff_smul_left hwf Set.subset_union_right,
  coeff_smul_left hwf Set.subset_union_left]

Result:
case h.h
Γ : 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✝¹ : AddCommMonoid R
inst✝ : SMulWithZero R V
x y : HahnSeries Γ R
z : HahnModule Γ' R V
h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u
a : Γ'
hwf : (x.support ∪ y.support).IsPWO
⊢ ∑ x_1 ∈ VAddAntidiagonal hwf ⋯ a,
      (x.coeff x_1.1 • ((of R).symm z).coeff x_1.2 + y.coeff x_1.1 • ((of R).symm z).coeff x_1.2) =
    ∑ ij ∈ VAddAntidiagonal hwf ⋯ a, x.coeff ij.1 • ((of R).symm z).coeff ij.2 +
      ∑ ij ∈ VAddAntidiagonal hwf ⋯ a, y.coeff ij.1 • ((of R).symm z).coeff ij.2

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✝¹ : AddCommMonoid R
inst✝ : SMulWithZero R V
x y : HahnSeries Γ R
z : HahnModule Γ' R V
h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u
⊢ (x + y) • z = x • z + y • z

Tactic:
ext a

Result:
case h.h
Γ : 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✝¹ : AddCommMonoid R
inst✝ : SMulWithZero R V
x y : HahnSeries Γ R
z : HahnModule Γ' R V
h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u
a : Γ'
⊢ ((of R).symm ((x + y) • z)).coeff a = ((of R).symm (x • z + y • z)).coeff a

Proof state:
case h.h
Γ : 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✝¹ : AddCommMonoid R
inst✝ : SMulWithZero R V
x y : HahnSeries Γ R
z : HahnModule Γ' R V
h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u
a : Γ'
b : Γ
⊢ ¬x.coeff b + y.coeff b = 0 → ¬x.coeff b = 0 ∨ ¬y.coeff b = 0

Tactic:
contrapose!

Result:
case h.h
Γ : 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✝¹ : AddCommMonoid R
inst✝ : SMulWithZero R V
x y : HahnSeries Γ R
z : HahnModule Γ' R V
h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u
a : Γ'
b : Γ
⊢ x.coeff b = 0 ∧ y.coeff b = 0 → x.coeff b + y.coeff b = 0

Proof state:
case h.h
Γ : 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✝¹ : AddCommMonoid R
inst✝ : SMulWithZero R V
x y : HahnSeries Γ R
z : HahnModule Γ' R V
h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u
a : Γ'
hwf : (x.support ∪ y.support).IsPWO
b : Γ
⊢ b ∈ (x + y).support → b ∈ x.support ∪ y.support

Tactic:
simp_all only [Set.isPWO_union, HahnSeries.isPWO_support, and_self, HahnSeries.mem_support,
  HahnSeries.coeff_add, ne_eq, Set.mem_union, Set.mem_setOf_eq, mem_support]

Result:
case h.h
Γ : 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✝¹ : AddCommMonoid R
inst✝ : SMulWithZero R V
x y : HahnSeries Γ R
z : HahnModule Γ' R V
h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u
a : Γ'
b : Γ
⊢ ¬x.coeff b + y.coeff b = 0 → ¬x.coeff b = 0 ∨ ¬y.coeff b = 0

Proof state:
case h.h
Γ : 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✝¹ : AddCommMonoid R
inst✝ : SMulWithZero R V
x y : HahnSeries Γ R
z : HahnModule Γ' R V
h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u
a : Γ'
hwf : (x.support ∪ y.support).IsPWO
⊢ ∑ x_1 ∈ VAddAntidiagonal hwf ⋯ a,
      (x.coeff x_1.1 • ((of R).symm z).coeff x_1.2 + y.coeff x_1.1 • ((of R).symm z).coeff x_1.2) =
    ∑ ij ∈ VAddAntidiagonal hwf ⋯ a, x.coeff ij.1 • ((of R).symm z).coeff ij.2 +
      ∑ ij ∈ VAddAntidiagonal hwf ⋯ a, y.coeff ij.1 • ((of R).symm z).coeff ij.2

Tactic:
simp only [HahnSeries.coeff_add, h, sum_add_distrib]

Result:
no goals

Proof state:
case h.h
Γ : 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✝¹ : AddCommMonoid R
inst✝ : SMulWithZero R V
x y : HahnSeries Γ R
z : HahnModule Γ' R V
h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u
a : Γ'
⊢ ((of R).symm ((x + y) • z)).coeff a = ((of R).symm (x • z + y • z)).coeff a

Tactic:
have hwf := x.isPWO_support.union y.isPWO_support

Result:
case h.h
Γ : 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✝¹ : AddCommMonoid R
inst✝ : SMulWithZero R V
x y : HahnSeries Γ R
z : HahnModule Γ' R V
h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u
a : Γ'
hwf : (x.support ∪ y.support).IsPWO
⊢ ((of R).symm ((x + y) • z)).coeff a = ((of R).symm (x • z + y • z)).coeff a

Proof state:
case h.h
Γ : 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✝¹ : AddCommMonoid R
inst✝ : SMulWithZero R V
x y : HahnSeries Γ R
z : HahnModule Γ' R V
h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u
a : Γ'
hwf : (x.support ∪ y.support).IsPWO
⊢ ∑ ij ∈ VAddAntidiagonal hwf ⋯ a, (x.coeff + y.coeff) ij.1 • ((of R).symm z).coeff ij.2 =
    ((of R).symm (x • z) + (of R).symm (y • z)).coeff a

Tactic:
simp_all only [Pi.add_apply, HahnSeries.coeff_add']

Result:
case h.h
Γ : 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✝¹ : AddCommMonoid R
inst✝ : SMulWithZero R V
x y : HahnSeries Γ R
z : HahnModule Γ' R V
h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u
a : Γ'
hwf : (x.support ∪ y.support).IsPWO
⊢ ∑ x_1 ∈ VAddAntidiagonal hwf ⋯ a,
      (x.coeff x_1.1 • ((of R).symm z).coeff x_1.2 + y.coeff x_1.1 • ((of R).symm z).coeff x_1.2) =
    ((of R).symm (x • z)).coeff a + ((of R).symm (y • z)).coeff a