case pos
Γ✝ : Type ?u.1226138
R : Type u_2
inst✝² : OrderedCancelAddCommMonoid Γ✝
Γ : Type u_1
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
hx : x = 0
⊢ coeff (x * y) (order x + order y) = coeff x (order x) * coeff y (order y)

case neg
Γ✝ : Type ?u.1226138
R : Type u_2
inst✝² : OrderedCancelAddCommMonoid Γ✝
Γ : Type u_1
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
hx : ¬x = 0
⊢ coeff (x * y) (order x + order y) = coeff x (order x) * coeff y (order y)
Γ✝ : Type ?u.1226138
R : Type u_2
inst✝² : OrderedCancelAddCommMonoid Γ✝
Γ : Type u_1
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
⊢ coeff (x * y) (order x + order y) = coeff x (order x) * coeff y (order y)
by_cases hx : x = 0
case pos
Γ✝ : Type ?u.1226138
R : Type u_2
inst✝² : OrderedCancelAddCommMonoid Γ✝
Γ : Type u_1
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
hx : ¬x = 0
hy : y = 0
⊢ coeff (x * y) (order x + order y) = coeff x (order x) * coeff y (order y)

case neg
Γ✝ : Type ?u.1226138
R : Type u_2
inst✝² : OrderedCancelAddCommMonoid Γ✝
Γ : Type u_1
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
hx : ¬x = 0
hy : ¬y = 0
⊢ coeff (x * y) (order x + order y) = coeff x (order x) * coeff y (order y)
case neg
Γ✝ : Type ?u.1226138
R : Type u_2
inst✝² : OrderedCancelAddCommMonoid Γ✝
Γ : Type u_1
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
hx : ¬x = 0
⊢ coeff (x * y) (order x + order y) = coeff x (order x) * coeff y (order y)
by_cases hy : y = 0
no goals
case neg
Γ✝ : Type ?u.1226138
R : Type u_2
inst✝² : OrderedCancelAddCommMonoid Γ✝
Γ : Type u_1
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
hx : ¬x = 0
hy : ¬y = 0
⊢ coeff (x * y) (order x + order y) = coeff x (order x) * coeff y (order y)
rw [order_of_ne hx, order_of_ne hy, mul_coeff, Finset.addAntidiagonal_min_add_min,
  Finset.sum_singleton]
no goals
case pos
Γ✝ : Type ?u.1226138
R : Type u_2
inst✝² : OrderedCancelAddCommMonoid Γ✝
Γ : Type u_1
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
hx : x = 0
⊢ coeff (x * y) (order x + order y) = coeff x (order x) * coeff y (order y)
simp [hx, mul_coeff]
no goals
case pos
Γ✝ : Type ?u.1226138
R : Type u_2
inst✝² : OrderedCancelAddCommMonoid Γ✝
Γ : Type u_1
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
hx : ¬x = 0
hy : y = 0
⊢ coeff (x * y) (order x + order y) = coeff x (order x) * coeff y (order y)
simp [hy, mul_coeff]