-- 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_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 : Γ
⊢ Set.MapsTo (fun x => ⟨x.1 + x.2, x⟩) ↑(((powerSeriesFamily hx a).mul (powerSeriesFamily hx b)).coeff g).support
    ↑((image (fun i => i.1 + i.2) (((powerSeriesFamily hx a).mul (powerSeriesFamily hx b)).coeff g).support).sigma
        antidiagonal)

Tactic:
intro ij hij

Result:
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
⊢ (fun x => ⟨x.1 + x.2, x⟩) ij ∈
    ↑((image (fun i => i.1 + i.2) (((powerSeriesFamily hx a).mul (powerSeriesFamily hx b)).coeff g).support).sigma
        antidiagonal)

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 : (_ : ℕ) × ℕ × ℕ
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

Tactic:
rw [mul_comm ((PowerSeries.coeff R i.snd.1) a), ← hi.2, mul_smul, pow_add]

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.2) b • (PowerSeries.coeff R i.snd.1) a • (x ^ i.snd.1 * x ^ i.snd.2)).coeff g = 0

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 ∈ ((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 =
    ∑ x_1 ∈ (((powerSeriesFamily hx a).mul (powerSeriesFamily hx b)).coeff g).support,
      ((PowerSeries.coeff R x_1.1) a • x ^ x_1.1 * (PowerSeries.coeff R x_1.2) b • x ^ x_1.2).coeff g

Tactic:
rw [sum_subset (support_powerSeriesFamily_subset hx a b g)]

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 : Γ
⊢ ∑ x_1 ∈ image (fun i => i.1 + i.2) (((powerSeriesFamily hx a).mul (powerSeriesFamily hx 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 =
    ∑ x_1 ∈ (((powerSeriesFamily hx a).mul (powerSeriesFamily hx b)).coeff g).support,
      ((PowerSeries.coeff R x_1.1) a • x ^ x_1.1 * (PowerSeries.coeff R x_1.2) b • x ^ x_1.2).coeff g

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

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,
      (∑ i ∈ antidiagonal x_1, ((PowerSeries.coeff R i.1) a * (PowerSeries.coeff R i.2) b) • x ^ x_1).coeff g =
    ∑ x_1 ∈ (((powerSeriesFamily hx a).mul (powerSeriesFamily hx b)).coeff g).support,
      ((PowerSeries.coeff R x_1.1) a • x ^ x_1.1 * (PowerSeries.coeff R x_1.2) b • x ^ x_1.2).coeff g

Tactic:
rw [← coeff_sum, sum_sigma', coeff_sum]

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 ∈
        (image (fun i => i.1 + i.2) (((powerSeriesFamily hx a).mul (powerSeriesFamily hx b)).coeff g).support).sigma
          antidiagonal,
      (((PowerSeries.coeff R i.snd.1) a * (PowerSeries.coeff R i.snd.2) b) • x ^ i.fst).coeff g =
    ∑ x_1 ∈ (((powerSeriesFamily hx a).mul (powerSeriesFamily hx b)).coeff g).support,
      ((PowerSeries.coeff R x_1.1) a • x ^ x_1.1 * (PowerSeries.coeff R x_1.2) b • x ^ x_1.2).coeff g

Proof state:
Γ : 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
⊢ ∀ (j k : ℕ), ⟨j + k, (j, k)⟩ = i → (PowerSeries.coeff R k) b • (PowerSeries.coeff R j) a • (x ^ j * x ^ k).coeff g = 0

Tactic:
intro m n

Result:
Γ : 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
m n : ℕ
⊢ ⟨m + n, (m, n)⟩ = i → (PowerSeries.coeff R n) b • (PowerSeries.coeff R m) a • (x ^ m * x ^ n).coeff g = 0

Proof state:
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

Tactic:
simp_all

Result:
no goals