-- Mathlib/RingTheory/HahnSeries/HEval.lean
theorem support_powerSeriesFamily_subset (hx : 0 < x.orderTop) (a b : PowerSeries R) (g : Γ) :
    ((powerSeriesFamily hx (a * b)).coeff g).support ⊆
    (((powerSeriesFamily hx a).mul (powerSeriesFamily hx b)).coeff g).support.image
      fun i => i.1 + i.2

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 : Γ
n : ℕ
hn :
  ∑ x_1 ∈ antidiagonal n, (PowerSeries.coeff R x_1.1) a • (PowerSeries.coeff R x_1.2) b • ((powers x hx) n).coeff g ≠ 0
he : ∃ a_1, a_1.1 + a_1.2 = n ∧ (PowerSeries.coeff R a_1.1) a • (PowerSeries.coeff R a_1.2) b • (x ^ n).coeff g ≠ 0
⊢ ¬(PowerSeries.coeff R he.choose.1) a • (PowerSeries.coeff R he.choose.2) b • (x ^ n).coeff g = 0

Tactic:
exact he.choose_spec.2

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 : Γ
n : ℕ
hn : (PowerSeries.coeff R n) (a * b) • ((powers x hx) n).coeff g ≠ 0
⊢ ∃ a_1 b_1, (a_1, b_1) ∈ ↑⋯.toFinset ∧ a_1 + b_1 = n

Tactic:
simp_rw [PowerSeries.coeff_mul, sum_smul, mul_smul] at hn

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 : Γ
n : ℕ
hn :
  ∑ x_1 ∈ antidiagonal n, (PowerSeries.coeff R x_1.1) a • (PowerSeries.coeff R x_1.2) b • ((powers x hx) n).coeff g ≠ 0
⊢ ∃ a_1 b_1, (a_1, b_1) ∈ ↑⋯.toFinset ∧ a_1 + b_1 = n

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 : Γ
n : ℕ
hn :
  ∑ x_1 ∈ antidiagonal n, (PowerSeries.coeff R x_1.1) a • (PowerSeries.coeff R x_1.2) b • ((powers x hx) n).coeff g ≠ 0
he :
  ∃ a_1 ∈ antidiagonal n, (PowerSeries.coeff R a_1.1) a • (PowerSeries.coeff R a_1.2) b • ((powers x hx) n).coeff g ≠ 0
⊢ ∃ a_1 b_1, (a_1, b_1) ∈ ↑⋯.toFinset ∧ a_1 + b_1 = n

Tactic:
simp only [powers_toFun, mem_antidiagonal] at he

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 : Γ
n : ℕ
hn :
  ∑ x_1 ∈ antidiagonal n, (PowerSeries.coeff R x_1.1) a • (PowerSeries.coeff R x_1.2) b • ((powers x hx) n).coeff g ≠ 0
he : ∃ a_1, a_1.1 + a_1.2 = n ∧ (PowerSeries.coeff R a_1.1) a • (PowerSeries.coeff R a_1.2) b • (x ^ n).coeff g ≠ 0
⊢ ∃ a_1 b_1, (a_1, b_1) ∈ ↑⋯.toFinset ∧ a_1 + b_1 = n

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 : Γ
⊢ ((powerSeriesFamily hx (a * b)).coeff g).support ⊆
    image (fun i => i.1 + i.2) (((powerSeriesFamily hx a).mul (powerSeriesFamily hx b)).coeff g).support

Tactic:
simp only [coeff_support, smulFamily_toFun, HahnSeries.coeff_smul, Set.Finite.toFinset_subset,
  coe_image, support_subset_iff, Set.mem_image, Prod.exists]

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 : Γ
⊢ ∀ (x_1 : ℕ),
    (PowerSeries.coeff R x_1) (a * b) • ((powers x hx) x_1).coeff g ≠ 0 →
      ∃ a_2 b_1, (a_2, b_1) ∈ ↑⋯.toFinset ∧ a_2 + b_1 = x_1

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 : Γ
n : ℕ
hn :
  ∑ x_1 ∈ antidiagonal n, (PowerSeries.coeff R x_1.1) a • (PowerSeries.coeff R x_1.2) b • ((powers x hx) n).coeff g ≠ 0
he : ∃ a_1, a_1.1 + a_1.2 = n ∧ (PowerSeries.coeff R a_1.1) a • (PowerSeries.coeff R a_1.2) b • (x ^ n).coeff g ≠ 0
⊢ (he.choose.1, he.choose.2) ∈ ↑⋯.toFinset ∧ he.choose.1 + he.choose.2 = n

Tactic:
refine ⟨?_, he.choose_spec.1⟩

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 : Γ
n : ℕ
hn :
  ∑ x_1 ∈ antidiagonal n, (PowerSeries.coeff R x_1.1) a • (PowerSeries.coeff R x_1.2) b • ((powers x hx) n).coeff g ≠ 0
he : ∃ a_1, a_1.1 + a_1.2 = n ∧ (PowerSeries.coeff R a_1.1) a • (PowerSeries.coeff R a_1.2) b • (x ^ n).coeff g ≠ 0
⊢ (he.choose.1, he.choose.2) ∈ ↑⋯.toFinset

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_1 : ℕ),
    (PowerSeries.coeff R x_1) (a * b) • ((powers x hx) x_1).coeff g ≠ 0 →
      ∃ a_2 b_1, (a_2, b_1) ∈ ↑⋯.toFinset ∧ a_2 + b_1 = x_1

Tactic:
intro n hn

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 : Γ
n : ℕ
hn : (PowerSeries.coeff R n) (a * b) • ((powers x hx) n).coeff g ≠ 0
⊢ ∃ a_1 b_1, (a_1, b_1) ∈ ↑⋯.toFinset ∧ a_1 + b_1 = n

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 : Γ
n : ℕ
hn :
  ∑ x_1 ∈ antidiagonal n, (PowerSeries.coeff R x_1.1) a • (PowerSeries.coeff R x_1.2) b • ((powers x hx) n).coeff g ≠ 0
⊢ ∃ a_1 b_1, (a_1, b_1) ∈ ↑⋯.toFinset ∧ a_1 + b_1 = n

Tactic:
have he := exists_ne_zero_of_sum_ne_zero hn

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 : Γ
n : ℕ
hn :
  ∑ x_1 ∈ antidiagonal n, (PowerSeries.coeff R x_1.1) a • (PowerSeries.coeff R x_1.2) b • ((powers x hx) n).coeff g ≠ 0
he :
  ∃ a_1 ∈ antidiagonal n, (PowerSeries.coeff R a_1.1) a • (PowerSeries.coeff R a_1.2) b • ((powers x hx) n).coeff g ≠ 0
⊢ ∃ a_1 b_1, (a_1, b_1) ∈ ↑⋯.toFinset ∧ a_1 + b_1 = n

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 : Γ
n : ℕ
hn :
  ∑ x_1 ∈ antidiagonal n, (PowerSeries.coeff R x_1.1) a • (PowerSeries.coeff R x_1.2) b • ((powers x hx) n).coeff g ≠ 0
he : ∃ a_1, a_1.1 + a_1.2 = n ∧ (PowerSeries.coeff R a_1.1) a • (PowerSeries.coeff R a_1.2) b • (x ^ n).coeff g ≠ 0
⊢ ¬(PowerSeries.coeff R he.choose.2) b •
        (PowerSeries.coeff R he.choose.1) a • (x ^ he.choose.1 * x ^ he.choose.2).coeff g =
      0

Tactic:
rw [← pow_add, smul_comm, he.choose_spec.1]

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 : Γ
n : ℕ
hn :
  ∑ x_1 ∈ antidiagonal n, (PowerSeries.coeff R x_1.1) a • (PowerSeries.coeff R x_1.2) b • ((powers x hx) n).coeff g ≠ 0
he : ∃ a_1, a_1.1 + a_1.2 = n ∧ (PowerSeries.coeff R a_1.1) a • (PowerSeries.coeff R a_1.2) b • (x ^ n).coeff g ≠ 0
⊢ ¬(PowerSeries.coeff R he.choose.1) a • (PowerSeries.coeff R he.choose.2) b • (x ^ n).coeff g = 0