-- 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
Γ : 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

Tactic:
refine (Finset.sum_of_injOn (fun x => ⟨x.1 + x.2, x⟩) (fun _ _ _ _ => by simp_all) ?_ ?_
  (fun _ _ => by simp only [smul_mul_smul_comm, pow_add])).symm

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 : Γ
⊢ 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)

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

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
⊢ (powerSeriesFamily hx (a * b)).hsum = ((powerSeriesFamily hx a).mul (powerSeriesFamily hx b)).hsum

Tactic:
ext 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 : Γ
⊢ (powerSeriesFamily hx (a * b)).hsum.coeff g = ((powerSeriesFamily hx a).mul (powerSeriesFamily hx b)).hsum.coeff g

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

Tactic:
exact hisc i.snd.1 i.snd.2 <| Sigma.eq hi.2 (by simp)

Result:
no goals

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 : (_ : ℕ) × ℕ × ℕ
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
⊢ Eq.recOn ⋯ ⟨i.snd.1 + i.snd.2, (i.snd.1, i.snd.2)⟩.snd = i.snd

Tactic:
simp

Result:
no goals

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 : Γ
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

Tactic:
simpa [PowerSeries.coeff_mul, sum_smul] using his

Result:
no goals

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 : Γ
⊢ (powerSeriesFamily hx (a * b)).hsum.coeff g = ((powerSeriesFamily hx a).mul (powerSeriesFamily hx b)).hsum.coeff g

Tactic:
simp only [powerSeriesFamily_apply, PowerSeries.coeff_mul, Finset.sum_smul, ← Finset.sum_product,
  coeff_hsum_eq_sum, mul_toFun]

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 ∈ ((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

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
m n : ℕ
his :
  ∀ (x_1 x_2 : ℕ),
    ((x_1, x_2) ∈
        Function.support fun a_1 =>
          ((PowerSeries.coeff R a_1.2) b •
                (PowerSeries.coeff R a_1.1) a • ((powers x hx) a_1.1 * (powers x hx) a_1.2)).coeff
            g) →
      ¬⟨x_1 + x_2, (x_1, x_2)⟩ = i
⊢ (PowerSeries.coeff R n) b • (PowerSeries.coeff R m) a • (x ^ m * x ^ n).coeff g ≠ 0 → ⟨m + n, (m, n)⟩ ≠ i

Tactic:
exact his m n

Result:
no goals

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 : Γ
x✝¹ : ℕ × ℕ
x✝ : x✝¹ ∈ (((powerSeriesFamily hx a).mul (powerSeriesFamily hx b)).coeff g).support
⊢ ((PowerSeries.coeff R x✝¹.1) a • x ^ x✝¹.1 * (PowerSeries.coeff R x✝¹.2) b • x ^ x✝¹.2).coeff g =
    (((PowerSeries.coeff R ((fun x => ⟨x.1 + x.2, x⟩) x✝¹).snd.1) a *
            (PowerSeries.coeff R ((fun x => ⟨x.1 + x.2, x⟩) x✝¹).snd.2) b) •
          x ^ ((fun x => ⟨x.1 + x.2, x⟩) x✝¹).fst).coeff
      g

Tactic:
simp only [smul_mul_smul_comm, pow_add]

Result:
no goals