-- Mathlib/RingTheory/HahnSeries/HEval.lean
theorem hsum_powerSeriesFamily_mul (hx : 0 < x.orderTop) (a b : PowerSeries R) :
    (powerSeriesFamily hx (a * b)).hsum =
    ((powerSeriesFamily hx a).mul (powerSeriesFamily hx b)).hsum

Proof state:
case coeff.h.refine_2
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝³ : LinearOrderedCancelAddCommMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : HahnSeries Γ V
hx : 0 < x.orderTop
a b : PowerSeries R
g : Γ
i : (_ : ℕ) × ℕ × ℕ
hi :
  i ∈
    (image (fun i => i.1 + i.2) (((powerSeriesFamily hx a).mul (powerSeriesFamily hx b)).coeff g).support).sigma
      antidiagonal
his : i ∉ (fun x => ⟨x.1 + x.2, x⟩) '' ↑(((powerSeriesFamily hx a).mul (powerSeriesFamily hx b)).coeff g).support
hisc :
  ∀ (j k : ℕ), ⟨j + k, (j, k)⟩ = i → (PowerSeries.coeff R k) b • (PowerSeries.coeff R j) a • (x ^ j * x ^ k).coeff g = 0
⊢ (((PowerSeries.coeff R i.snd.1) a * (PowerSeries.coeff R i.snd.2) b) • x ^ i.fst).coeff g = 0

Tactic:
simp only [mem_sigma, mem_antidiagonal] at hi

Result:
case coeff.h.refine_2
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝³ : LinearOrderedCancelAddCommMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : HahnSeries Γ V
hx : 0 < x.orderTop
a b : PowerSeries R
g : Γ
i : (_ : ℕ) × ℕ × ℕ
his : i ∉ (fun x => ⟨x.1 + x.2, x⟩) '' ↑(((powerSeriesFamily hx a).mul (powerSeriesFamily hx b)).coeff g).support
hisc :
  ∀ (j k : ℕ), ⟨j + k, (j, k)⟩ = i → (PowerSeries.coeff R k) b • (PowerSeries.coeff R j) a • (x ^ j * x ^ k).coeff g = 0
hi :
  i.fst ∈ image (fun i => i.1 + i.2) (((powerSeriesFamily hx a).mul (powerSeriesFamily hx b)).coeff g).support ∧
    i.snd.1 + i.snd.2 = i.fst
⊢ (((PowerSeries.coeff R i.snd.1) a * (PowerSeries.coeff R i.snd.2) b) • x ^ i.fst).coeff g = 0

Proof state:
case coeff.h.refine_1
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝³ : LinearOrderedCancelAddCommMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : HahnSeries Γ V
hx : 0 < x.orderTop
a b : PowerSeries R
g : Γ
ij : ℕ × ℕ
hij : ij ∈ ↑(((powerSeriesFamily hx a).mul (powerSeriesFamily hx b)).coeff g).support
⊢ ∃ a_1 b_1,
    (a_1, b_1) ∈ (((powerSeriesFamily hx a).mul (powerSeriesFamily hx b)).coeff g).support ∧ a_1 + b_1 = ij.1 + ij.2

Tactic:
use ij.1, ij.2

Result:
case h
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝³ : LinearOrderedCancelAddCommMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : HahnSeries Γ V
hx : 0 < x.orderTop
a b : PowerSeries R
g : Γ
ij : ℕ × ℕ
hij : ij ∈ ↑(((powerSeriesFamily hx a).mul (powerSeriesFamily hx b)).coeff g).support
⊢ (ij.1, ij.2) ∈ (((powerSeriesFamily hx a).mul (powerSeriesFamily hx b)).coeff g).support ∧ ij.1 + ij.2 = ij.1 + ij.2

Proof state:
case coeff.h
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝³ : LinearOrderedCancelAddCommMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : HahnSeries Γ V
hx : 0 < x.orderTop
a b : PowerSeries R
g : Γ
⊢ ∀ x_1 ∈ image (fun i => i.1 + i.2) (((powerSeriesFamily hx a).mul (powerSeriesFamily hx b)).coeff g).support,
    x_1 ∉ ((powerSeriesFamily hx (a * b)).coeff g).support →
      (∑ i ∈ antidiagonal x_1, ((PowerSeries.coeff R i.1) a * (PowerSeries.coeff R i.2) b) • x ^ x_1).coeff g = 0

Tactic:
intro i hi his

Result:
case coeff.h
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝³ : LinearOrderedCancelAddCommMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : HahnSeries Γ V
hx : 0 < x.orderTop
a b : PowerSeries R
g : Γ
i : ℕ
hi : i ∈ image (fun i => i.1 + i.2) (((powerSeriesFamily hx a).mul (powerSeriesFamily hx b)).coeff g).support
his : i ∉ ((powerSeriesFamily hx (a * b)).coeff g).support
⊢ (∑ i_1 ∈ antidiagonal i, ((PowerSeries.coeff R i_1.1) a * (PowerSeries.coeff R i_1.2) b) • x ^ i).coeff g = 0