-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem coeff_smul_order_add_order {Γ} [LinearOrderedCancelAddCommMonoid Γ] [Zero R]
    [SMulWithZero R V] (x : HahnSeries Γ R) (y : HahnModule Γ R V) :
    ((of R).symm (x • y)).coeff (x.order + ((of R).symm y).order) =
    x.leadingCoeff • ((of R).symm y).leadingCoeff

Proof state:
case neg
R : Type u_3
V : Type u_5
inst✝³ : AddCommMonoid V
Γ : Type u_6
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Zero R
inst✝ : SMulWithZero R V
x : HahnSeries Γ R
y : HahnModule Γ R V
hx : ¬x = 0
hy : ¬(of R).symm y = 0
⊢ ∑ ij ∈ VAddAntidiagonal ⋯ ⋯ (⋯.min ⋯ + ⋯.min ⋯), x.coeff ij.1 • ((of R).symm y).coeff ij.2 =
    x.coeff (⋯.min ⋯) • ((of R).symm y).coeff (⋯.min ⋯)

Tactic:
erw [Finset.vaddAntidiagonal_min_vadd_min, Finset.sum_singleton]

Result:
no goals

Proof state:
case neg
R : Type u_3
V : Type u_5
inst✝³ : AddCommMonoid V
Γ : Type u_6
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Zero R
inst✝ : SMulWithZero R V
x : HahnSeries Γ R
y : HahnModule Γ R V
hx : ¬x = 0
⊢ ((of R).symm (x • y)).coeff (x.order + ((of R).symm y).order) = x.leadingCoeff • ((of R).symm y).leadingCoeff

Tactic:
by_cases hy : (of R).symm y = 0

Result:
case pos
R : Type u_3
V : Type u_5
inst✝³ : AddCommMonoid V
Γ : Type u_6
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Zero R
inst✝ : SMulWithZero R V
x : HahnSeries Γ R
y : HahnModule Γ R V
hx : ¬x = 0
hy : (of R).symm y = 0
⊢ ((of R).symm (x • y)).coeff (x.order + ((of R).symm y).order) = x.leadingCoeff • ((of R).symm y).leadingCoeff

case neg
R : Type u_3
V : Type u_5
inst✝³ : AddCommMonoid V
Γ : Type u_6
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Zero R
inst✝ : SMulWithZero R V
x : HahnSeries Γ R
y : HahnModule Γ R V
hx : ¬x = 0
hy : ¬(of R).symm y = 0
⊢ ((of R).symm (x • y)).coeff (x.order + ((of R).symm y).order) = x.leadingCoeff • ((of R).symm y).leadingCoeff

Proof state:
case pos
R : Type u_3
V : Type u_5
inst✝³ : AddCommMonoid V
Γ : Type u_6
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Zero R
inst✝ : SMulWithZero R V
x : HahnSeries Γ R
y : HahnModule Γ R V
hx : ¬x = 0
hy : (of R).symm y = 0
⊢ ((of R).symm (x • y)).coeff (x.order + ((of R).symm y).order) = x.leadingCoeff • ((of R).symm y).leadingCoeff

Tactic:
simp [hy, coeff_smul]

Result:
no goals

Proof state:
case neg
R : Type u_3
V : Type u_5
inst✝³ : AddCommMonoid V
Γ : Type u_6
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Zero R
inst✝ : SMulWithZero R V
x : HahnSeries Γ R
y : HahnModule Γ R V
hx : ¬x = 0
hy : ¬(of R).symm y = 0
⊢ ((of R).symm (x • y)).coeff (x.order + ((of R).symm y).order) = x.leadingCoeff • ((of R).symm y).leadingCoeff

Tactic:
rw [HahnSeries.order_of_ne hx, HahnSeries.order_of_ne hy, coeff_smul,
  HahnSeries.leadingCoeff_of_ne hx, HahnSeries.leadingCoeff_of_ne hy]

Result:
case neg
R : Type u_3
V : Type u_5
inst✝³ : AddCommMonoid V
Γ : Type u_6
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Zero R
inst✝ : SMulWithZero R V
x : HahnSeries Γ R
y : HahnModule Γ R V
hx : ¬x = 0
hy : ¬(of R).symm y = 0
⊢ ∑ ij ∈ VAddAntidiagonal ⋯ ⋯ (⋯.min ⋯ + ⋯.min ⋯), x.coeff ij.1 • ((of R).symm y).coeff ij.2 =
    x.coeff (⋯.min ⋯) • ((of R).symm y).coeff (⋯.min ⋯)

Proof state:
case pos
R : Type u_3
V : Type u_5
inst✝³ : AddCommMonoid V
Γ : Type u_6
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Zero R
inst✝ : SMulWithZero R V
x : HahnSeries Γ R
y : HahnModule Γ R V
hx : x = 0
⊢ ((of R).symm (x • y)).coeff (x.order + ((of R).symm y).order) = x.leadingCoeff • ((of R).symm y).leadingCoeff

Tactic:
simp [HahnSeries.coeff_zero, hx]

Result:
no goals

Proof state:
R : Type u_3
V : Type u_5
inst✝³ : AddCommMonoid V
Γ : Type u_6
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Zero R
inst✝ : SMulWithZero R V
x : HahnSeries Γ R
y : HahnModule Γ R V
⊢ ((of R).symm (x • y)).coeff (x.order + ((of R).symm y).order) = x.leadingCoeff • ((of R).symm y).leadingCoeff

Tactic:
by_cases hx : x = (0 : HahnSeries Γ R)

Result:
case pos
R : Type u_3
V : Type u_5
inst✝³ : AddCommMonoid V
Γ : Type u_6
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Zero R
inst✝ : SMulWithZero R V
x : HahnSeries Γ R
y : HahnModule Γ R V
hx : x = 0
⊢ ((of R).symm (x • y)).coeff (x.order + ((of R).symm y).order) = x.leadingCoeff • ((of R).symm y).leadingCoeff

case neg
R : Type u_3
V : Type u_5
inst✝³ : AddCommMonoid V
Γ : Type u_6
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Zero R
inst✝ : SMulWithZero R V
x : HahnSeries Γ R
y : HahnModule Γ R V
hx : ¬x = 0
⊢ ((of R).symm (x • y)).coeff (x.order + ((of R).symm y).order) = x.leadingCoeff • ((of R).symm y).leadingCoeff