-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem smul_add [Zero R] [DistribSMul R V] (x : HahnSeries Γ R) (y z : HahnModule Γ' R V) :
    x • (y + z) = x • y + x • 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✝¹ : Zero R
inst✝ : DistribSMul R V
x : HahnSeries Γ R
y z : HahnModule Γ' R V
k : Γ'
hwf : (((of R).symm y).support ∪ ((of R).symm z).support).IsPWO
⊢ ((of R).symm (y + z)).support ⊆ ((of R).symm y).support ∪ ((of R).symm z).support

Tactic:
intro b

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✝¹ : Zero R
inst✝ : DistribSMul R V
x : HahnSeries Γ R
y z : HahnModule Γ' R V
k : Γ'
hwf : (((of R).symm y).support ∪ ((of R).symm z).support).IsPWO
b : Γ'
⊢ b ∈ ((of R).symm (y + z)).support → b ∈ ((of R).symm y).support ∪ ((of R).symm z).support

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✝¹ : Zero R
inst✝ : DistribSMul R V
x : HahnSeries Γ R
y z : HahnModule Γ' R V
k b : Γ'
⊢ ¬((of R).symm y).coeff b + ((of R).symm z).coeff b = 0 → ¬((of R).symm y).coeff b = 0 ∨ ¬((of R).symm z).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✝¹ : Zero R
inst✝ : DistribSMul R V
x : HahnSeries Γ R
y z : HahnModule Γ' R V
k b : Γ'
⊢ ((of R).symm y).coeff b = 0 ∧ ((of R).symm z).coeff b = 0 → ((of R).symm y).coeff b + ((of R).symm z).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✝¹ : Zero R
inst✝ : DistribSMul R V
x : HahnSeries Γ R
y z : HahnModule Γ' R V
k b : Γ'
⊢ ((of R).symm y).coeff b = 0 ∧ ((of R).symm z).coeff b = 0 → ((of R).symm y).coeff b + ((of R).symm z).coeff b = 0

Tactic:
intro h

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✝¹ : Zero R
inst✝ : DistribSMul R V
x : HahnSeries Γ R
y z : HahnModule Γ' R V
k b : Γ'
h : ((of R).symm y).coeff b = 0 ∧ ((of R).symm z).coeff b = 0
⊢ ((of R).symm y).coeff b + ((of R).symm z).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✝¹ : Zero R
inst✝ : DistribSMul R V
x : HahnSeries Γ R
y z : HahnModule Γ' R V
k : Γ'
hwf : (((of R).symm y).support ∪ ((of R).symm z).support).IsPWO
⊢ ∑ ij ∈ VAddAntidiagonal ⋯ hwf k, x.coeff ij.1 • ((of R).symm y + (of R).symm z).coeff ij.2 =
    ((of R).symm (x • y + x • z)).coeff k

Tactic:
simp_all only [HahnSeries.coeff_add', Pi.add_apply, smul_add, of_symm_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✝¹ : Zero R
inst✝ : DistribSMul R V
x : HahnSeries Γ R
y z : HahnModule Γ' R V
k : Γ'
hwf : (((of R).symm y).support ∪ ((of R).symm z).support).IsPWO
⊢ ∑ x_1 ∈ VAddAntidiagonal ⋯ hwf k, x.coeff x_1.1 • (((of R).symm y).coeff x_1.2 + ((of R).symm z).coeff x_1.2) =
    ((of R).symm (x • y)).coeff k + ((of R).symm (x • z)).coeff k

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✝¹ : Zero R
inst✝ : DistribSMul R V
x : HahnSeries Γ R
y z : HahnModule Γ' R V
k : Γ'
hwf : (((of R).symm y).support ∪ ((of R).symm z).support).IsPWO
b : Γ'
⊢ b ∈ ((of R).symm (y + z)).support → b ∈ ((of R).symm y).support ∪ ((of R).symm z).support

Tactic:
simp_all only [Set.isPWO_union, HahnSeries.isPWO_support, and_self, of_symm_add,
  HahnSeries.coeff_add', Pi.add_apply, ne_eq, Set.mem_union, HahnSeries.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✝¹ : Zero R
inst✝ : DistribSMul R V
x : HahnSeries Γ R
y z : HahnModule Γ' R V
k b : Γ'
⊢ ¬((of R).symm y).coeff b + ((of R).symm z).coeff b = 0 → ¬((of R).symm y).coeff b = 0 ∨ ¬((of R).symm z).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✝¹ : Zero R
inst✝ : DistribSMul R V
x : HahnSeries Γ R
y z : HahnModule Γ' R V
k : Γ'
⊢ ((of R).symm (x • (y + z))).coeff k = ((of R).symm (x • y + x • z)).coeff k

Tactic:
have hwf := ((of R).symm y).isPWO_support.union ((of R).symm z).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✝¹ : Zero R
inst✝ : DistribSMul R V
x : HahnSeries Γ R
y z : HahnModule Γ' R V
k : Γ'
hwf : (((of R).symm y).support ∪ ((of R).symm z).support).IsPWO
⊢ ((of R).symm (x • (y + z))).coeff k = ((of R).symm (x • y + x • z)).coeff k

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✝¹ : Zero R
inst✝ : DistribSMul R V
x : HahnSeries Γ R
y z : HahnModule Γ' R V
k : Γ'
hwf : (((of R).symm y).support ∪ ((of R).symm z).support).IsPWO
⊢ ((of R).symm (x • (y + z))).coeff k = ((of R).symm (x • y + x • z)).coeff k

Tactic:
rw [coeff_smul_right hwf, of_symm_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✝¹ : Zero R
inst✝ : DistribSMul R V
x : HahnSeries Γ R
y z : HahnModule Γ' R V
k : Γ'
hwf : (((of R).symm y).support ∪ ((of R).symm z).support).IsPWO
⊢ ∑ ij ∈ VAddAntidiagonal ⋯ hwf k, x.coeff ij.1 • ((of R).symm y + (of R).symm z).coeff ij.2 =
    ((of R).symm (x • y + x • z)).coeff k

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✝¹ : Zero R
inst✝ : DistribSMul R V
x : HahnSeries Γ R
y z : HahnModule Γ' R V
k : Γ'
hwf : (((of R).symm y).support ∪ ((of R).symm z).support).IsPWO
⊢ ((of R).symm (y + z)).support ⊆ ((of R).symm y).support ∪ ((of R).symm z).support

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✝ : DistribSMul R V
x : HahnSeries Γ R
y z : HahnModule Γ' R V
⊢ x • (y + z) = x • y + x • z

Tactic:
ext k

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✝¹ : Zero R
inst✝ : DistribSMul R V
x : HahnSeries Γ R
y z : HahnModule Γ' R V
k : Γ'
⊢ ((of R).symm (x • (y + z))).coeff k = ((of R).symm (x • y + x • z)).coeff k