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

Tactic:
contrapose!

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

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
⊢ (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)

Tactic:
simp only [coe_sigma, coe_image, Set.mem_sigma_iff, Set.mem_image, Prod.exists, mem_coe,
  mem_antidiagonal, and_true]

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
⊢ ∃ 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

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
x✝¹ : ℕ × ℕ
x✝ : x✝¹ ∈ ↑(((powerSeriesFamily hx a).mul (powerSeriesFamily hx b)).coeff g).support
⊢ (fun x => ⟨x.1 + x.2, x⟩) x✝³ = (fun x => ⟨x.1 + x.2, x⟩) x✝¹ → x✝³ = x✝¹

Tactic:
simp_all

Result:
no goals

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

Tactic:
have 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 := by
  intro m n
  contrapose!
  simp only [coeff_support, mul_toFun, smulFamily_toFun, Algebra.mul_smul_comm,
    Algebra.smul_mul_assoc, Set.Finite.coe_toFinset, Set.mem_image,
    Prod.exists, not_exists, not_and] at his
  exact his m n

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

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

Tactic:
intro i hi his

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

Tactic:
simp only [coeff_support, mul_toFun, smulFamily_toFun, Algebra.mul_smul_comm,
  Algebra.smul_mul_assoc, Set.Finite.coe_toFinset, Set.mem_image,
  Prod.exists, not_exists, not_and] at his

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