awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_4
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : CommRing V
inst_5 : Algebra R V
x : V⟦Γ⟧
f g : PowerSeries R
n : ℕ
pos :
  ∀ (hx : 0 < x.orderTop),
    Eq (α := V⟦Γ⟧) ((powerSeriesFamily x (f + g) : (a : ℕ) → V⟦Γ⟧) n : V⟦Γ⟧)
      ((powerSeriesFamily x f + powerSeriesFamily x g : (a : ℕ) → V⟦Γ⟧) n : V⟦Γ⟧)
neg :
  ∀ (hx : ¬0 < x.orderTop),
    Eq (α := V⟦Γ⟧) ((powerSeriesFamily x (f + g) : (a : ℕ) → V⟦Γ⟧) n : V⟦Γ⟧)
      ((powerSeriesFamily x f + powerSeriesFamily x g : (a : ℕ) → V⟦Γ⟧) n : V⟦Γ⟧)
⊢ Eq (α := V⟦Γ⟧) ((powerSeriesFamily x (f + g) : (a : ℕ) → V⟦Γ⟧) n : V⟦Γ⟧)
    ((powerSeriesFamily x f + powerSeriesFamily x g : (a : ℕ) → V⟦Γ⟧) n : V⟦Γ⟧)

Tactic:
by_cases hx : 0 < x.orderTop

Premises used: HahnSeries.orderTop
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_4
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : CommRing V
inst_5 : Algebra R V
x : V⟦Γ⟧
f g : PowerSeries R
n : ℕ
hx : 0 < x.orderTop
⊢ Eq (α := V⟦Γ⟧) ((powerSeriesFamily x (f + g) : (a : ℕ) → V⟦Γ⟧) n : V⟦Γ⟧)
    ((powerSeriesFamily x f + powerSeriesFamily x g : (a : ℕ) → V⟦Γ⟧) n : V⟦Γ⟧)

Tactic:
simp [hx, add_smul]

Premises used: add_smul
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_4
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : CommRing V
inst_5 : Algebra R V
x : V⟦Γ⟧
f g : PowerSeries R
n : ℕ
hx : ¬0 < x.orderTop
⊢ Eq (α := V⟦Γ⟧) ((powerSeriesFamily x (f + g) : (a : ℕ) → V⟦Γ⟧) n : V⟦Γ⟧)
    ((powerSeriesFamily x f + powerSeriesFamily x g : (a : ℕ) → V⟦Γ⟧) n : V⟦Γ⟧)

Tactic:
simp [hx, add_smul]

Premises used: add_smul
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_4
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : CommRing V
inst_5 : Algebra R V
x : V⟦Γ⟧
f : PowerSeries R
r : R
h :
  ∀ (n : ℕ),
    Eq (α := V⟦Γ⟧) ((powerSeriesFamily x (r • f) : (a : ℕ) → V⟦Γ⟧) n : V⟦Γ⟧)
      ((HSMul.hSMul (α := R⟦Γ⟧) ((HahnSeries.single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) (powerSeriesFamily x f) :
            (a : ℕ) → V⟦Γ⟧)
          n :
        V⟦Γ⟧)
⊢ powerSeriesFamily x (r • f) =
    HSMul.hSMul (α := R⟦Γ⟧) ((HahnSeries.single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) (powerSeriesFamily x f)

Tactic:
ext1 n
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_4
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : CommRing V
inst_5 : Algebra R V
x : V⟦Γ⟧
f : PowerSeries R
r : R
n : ℕ
⊢ Eq (α := V⟦Γ⟧) ((powerSeriesFamily x (r • f) : (a : ℕ) → V⟦Γ⟧) n : V⟦Γ⟧)
    ((HSMul.hSMul (α := R⟦Γ⟧) ((HahnSeries.single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) (powerSeriesFamily x f) :
          (a : ℕ) → V⟦Γ⟧)
        n :
      V⟦Γ⟧)

Tactic:
simp [mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_4
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : CommRing V
inst_5 : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
pos :
  ∀ (h : 0 < x.orderTop),
    ((powerSeriesFamily x (a * b)).coeff g).support ⊆
      image (fun (i : ℕ × ℕ) ↦ i.1 + i.2) (((powerSeriesFamily x a).mul (powerSeriesFamily x b)).coeff g).support
neg :
  ∀ (h : ¬0 < x.orderTop),
    ((powerSeriesFamily x (a * b)).coeff g).support ⊆
      image (fun (i : ℕ × ℕ) ↦ i.1 + i.2) (((powerSeriesFamily x a).mul (powerSeriesFamily x b)).coeff g).support
⊢ ((powerSeriesFamily x (a * b)).coeff g).support ⊆
    image (fun (i : ℕ × ℕ) ↦ i.1 + i.2) (((powerSeriesFamily x a).mul (powerSeriesFamily x b)).coeff g).support

Tactic:
by_cases h : 0 < x.orderTop

Premises used: HahnSeries.orderTop
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_4
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : CommRing V
inst_5 : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : 0 < x.orderTop
pos :
  ∀ (x_1 : ℕ),
    Ne.{u_4 + 1} (α := V) (HahnSeries.coeff ((powerSeriesFamily x (a * b) : (a : ℕ) → V⟦Γ⟧) x_1) g) 0 →
      x_1 ∈
        (↑(image (fun (i : ℕ × ℕ) ↦ i.1 + i.2)
              (Set.Finite.toFinset (s :=
                Function.support.{0, u_4} (M := V) fun (a_2 : ℕ × ℕ) ↦
                  HahnSeries.coeff (((powerSeriesFamily x a).mul (powerSeriesFamily x b) : (a : ℕ × ℕ) → V⟦Γ⟧) a_2) g)
                ⋯)) :
          Set ℕ)
⊢ ((powerSeriesFamily x (a * b)).coeff g).support ⊆
    image (fun (i : ℕ × ℕ) ↦ i.1 + i.2) (((powerSeriesFamily x a).mul (powerSeriesFamily x b)).coeff g).support

Tactic:
simp only [coeff_support, Set.Finite.toFinset_subset, support_subset_iff]

Premises used: Set.Finite.toFinset_subset, HahnSeries.SummableFamily.coeff_support, Function.support_subset_iff
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_4
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : CommRing V
inst_5 : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : 0 < x.orderTop
n : ℕ
hn : Ne.{u_4 + 1} (α := V) (HahnSeries.coeff ((powerSeriesFamily x (a * b) : (a : ℕ) → V⟦Γ⟧) n) g) 0
⊢ ∃ c ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    HSMul.hSMul (α := R) ((PowerSeries.coeff c.1 : (a : PowerSeries R) → R) a : R)
        (HSMul.hSMul (α := R) (β := V) ((PowerSeries.coeff c.2 : (a : PowerSeries R) → R) b : R)
          (HahnSeries.coeff ((powers x : (a : ℕ) → V⟦Γ⟧) n) g)) ≠
      0

Tactic:
exists_ne_zero_of_sum_ne_zero ?_

Premises used: Finset.exists_ne_zero_of_sum_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_4
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : CommRing V
inst_5 : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : 0 < x.orderTop
n : ℕ
hn : Ne.{u_4 + 1} (α := V) (HahnSeries.coeff ((powerSeriesFamily x (a * b) : (a : ℕ) → V⟦Γ⟧) n) g) 0
refine :
  Ne.{u_4 + 1} (α := V)
    (∑ x_1 ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      HSMul.hSMul (α := R) ((PowerSeries.coeff x_1.1 : (a : PowerSeries R) → R) a : R)
        (HSMul.hSMul (α := R) (β := V) ((PowerSeries.coeff x_1.2 : (a : PowerSeries R) → R) b : R)
          (HahnSeries.coeff ((powers x : (a : ℕ) → V⟦Γ⟧) n) g)))
    0
⊢ ∃ c ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    HSMul.hSMul (α := R) ((PowerSeries.coeff c.1 : (a : PowerSeries R) → R) a : R)
        (HSMul.hSMul (α := R) (β := V) ((PowerSeries.coeff c.2 : (a : PowerSeries R) → R) b : R)
          (HahnSeries.coeff ((powers x : (a : ℕ) → V⟦Γ⟧) n) g)) ≠
      0

Tactic:
refine exists_ne_zero_of_sum_ne_zero ?_

Premises used: Finset.exists_ne_zero_of_sum_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_4
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : CommRing V
inst_5 : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : 0 < x.orderTop
n : ℕ
hn : Ne.{u_4 + 1} (α := V) (HahnSeries.coeff ((powerSeriesFamily x (a * b) : (a : ℕ) → V⟦Γ⟧) n) g) 0
⊢ Ne.{u_4 + 1} (α := V)
    (∑ x_1 ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      HSMul.hSMul (α := R) ((PowerSeries.coeff x_1.1 : (a : PowerSeries R) → R) a : R)
        (HSMul.hSMul (α := R) (β := V) ((PowerSeries.coeff x_1.2 : (a : PowerSeries R) → R) b : R)
          (HahnSeries.coeff ((powers x : (a : ℕ) → V⟦Γ⟧) n) g)))
    0

Tactic:
simpa [PowerSeries.coeff_mul, sum_smul, mul_smul, h] using hn

Premises used: Finset.sum_smul, PowerSeries.coeff_mul, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_4
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : CommRing V
inst_5 : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : 0 < x.orderTop
n : ℕ
hn : Ne.{u_4 + 1} (α := V) (HahnSeries.coeff ((powerSeriesFamily x (a * b) : (a : ℕ) → V⟦Γ⟧) n) g) 0
⊢ ∃ c ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    HSMul.hSMul (α := R) ((PowerSeries.coeff c.1 : (a : PowerSeries R) → R) a : R)
        (HSMul.hSMul (α := R) (β := V) ((PowerSeries.coeff c.2 : (a : PowerSeries R) → R) b : R)
          (HahnSeries.coeff ((powers x : (a : ℕ) → V⟦Γ⟧) n) g)) ≠
      0

Tactic:
have he : ∃ c ∈ antidiagonal n, (PowerSeries.coeff c.1) a • (PowerSeries.coeff c.2) b •
        ((powers x) n).coeff g ≠ 0 := by
      refine exists_ne_zero_of_sum_ne_zero ?_
      simpa [PowerSeries.coeff_mul, sum_smul, mul_smul, h] using hn
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_4
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : CommRing V
inst_5 : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : 0 < x.orderTop
n : ℕ
hn : Ne.{u_4 + 1} (α := V) (HahnSeries.coeff ((powerSeriesFamily x (a * b) : (a : ℕ) → V⟦Γ⟧) n) g) 0
he :
  ∃ c ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    HSMul.hSMul (α := R) ((PowerSeries.coeff c.1 : (a : PowerSeries R) → R) a : R)
        (HSMul.hSMul (α := R) (β := V) ((PowerSeries.coeff c.2 : (a : PowerSeries R) → R) b : R)
          (HahnSeries.coeff ((powers x : (a : ℕ) → V⟦Γ⟧) n) g)) ≠
      0
⊢ ∃ (c : ℕ × ℕ),
    c.1 + c.2 = n ∧
      HSMul.hSMul (α := R) ((PowerSeries.coeff c.1 : (a : PowerSeries R) → R) a : R)
          (HSMul.hSMul (α := R) ((PowerSeries.coeff c.2 : (a : PowerSeries R) → R) b : R) ((x ^ n).coeff g)) ≠
        0

Tactic:
simp only [powers_of_orderTop_pos h, mem_antidiagonal] at he

Premises used: Finset.HasAntidiagonal.mem_antidiagonal, HahnSeries.SummableFamily.powers_of_orderTop_pos
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_4
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : CommRing V
inst_5 : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : 0 < x.orderTop
n : ℕ
hn : Ne.{u_4 + 1} (α := V) (HahnSeries.coeff ((powerSeriesFamily x (a * b) : (a : ℕ) → V⟦Γ⟧) n) g) 0
he :
  ∃ (c : ℕ × ℕ),
    c.1 + c.2 = n ∧
      HSMul.hSMul (α := R) ((PowerSeries.coeff c.1 : (a : PowerSeries R) → R) a : R)
          (HSMul.hSMul (α := R) ((PowerSeries.coeff c.2 : (a : PowerSeries R) → R) b : R) ((x ^ n).coeff g)) ≠
        0
pos :
  ∀ (c : ℕ × ℕ) (hcn : c.1 + c.2 = n)
    (hc :
      HSMul.hSMul (α := R) ((PowerSeries.coeff c.1 : (a : PowerSeries R) → R) a : R)
          (HSMul.hSMul (α := R) ((PowerSeries.coeff c.2 : (a : PowerSeries R) → R) b : R) ((x ^ n).coeff g)) ≠
        0),
    n ∈
      (↑(image (fun (i : ℕ × ℕ) ↦ i.1 + i.2)
            (Set.Finite.toFinset (s :=
              Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
                HahnSeries.coeff (((powerSeriesFamily x a).mul (powerSeriesFamily x b) : (a : ℕ × ℕ) → V⟦Γ⟧) a_1) g)
              ⋯)) :
        Set ℕ)
⊢ n ∈
    (↑(image (fun (i : ℕ × ℕ) ↦ i.1 + i.2)
          (Set.Finite.toFinset (s :=
            Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
              HahnSeries.coeff (((powerSeriesFamily x a).mul (powerSeriesFamily x b) : (a : ℕ × ℕ) → V⟦Γ⟧) a_1) g)
            ⋯)) :
      Set ℕ)

Tactic:
obtain ⟨c, hcn, hc⟩ := he
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_4
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : CommRing V
inst_5 : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : 0 < x.orderTop
n : ℕ
hn : Ne.{u_4 + 1} (α := V) (HahnSeries.coeff ((powerSeriesFamily x (a * b) : (a : ℕ) → V⟦Γ⟧) n) g) 0
c : ℕ × ℕ
hcn : c.1 + c.2 = n
hc :
  HSMul.hSMul (α := R) ((PowerSeries.coeff c.1 : (a : PowerSeries R) → R) a : R)
      (HSMul.hSMul (α := R) ((PowerSeries.coeff c.2 : (a : PowerSeries R) → R) b : R) ((x ^ n).coeff g)) ≠
    0
pos :
  ∃ (x_1 : ℕ × ℕ),
    Membership.mem (γ := Set (ℕ × ℕ))
        (Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
          HahnSeries.coeff (((powerSeriesFamily x a).mul (powerSeriesFamily x b) : (a : ℕ × ℕ) → V⟦Γ⟧) a_1) g)
        x_1 ∧
      x_1.1 + x_1.2 = n
⊢ n ∈
    (↑(image (fun (i : ℕ × ℕ) ↦ i.1 + i.2)
          (Set.Finite.toFinset (s :=
            Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
              HahnSeries.coeff (((powerSeriesFamily x a).mul (powerSeriesFamily x b) : (a : ℕ × ℕ) → V⟦Γ⟧) a_1) g)
            ⋯)) :
      Set ℕ)

Tactic:
simp only [coe_image, Set.Finite.coe_toFinset, Set.mem_image]

Premises used: Set.mem_image, Finset.coe_image, Set.Finite.coe_toFinset
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_4
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : CommRing V
inst_5 : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : 0 < x.orderTop
n : ℕ
hn : Ne.{u_4 + 1} (α := V) (HahnSeries.coeff ((powerSeriesFamily x (a * b) : (a : ℕ) → V⟦Γ⟧) n) g) 0
c : ℕ × ℕ
hcn : c.1 + c.2 = n
hc :
  HSMul.hSMul (α := R) ((PowerSeries.coeff c.1 : (a : PowerSeries R) → R) a : R)
      (HSMul.hSMul (α := R) ((PowerSeries.coeff c.2 : (a : PowerSeries R) → R) b : R) ((x ^ n).coeff g)) ≠
    0
h₁ :
  Membership.mem (γ := Set (ℕ × ℕ))
      (Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
        HahnSeries.coeff (((powerSeriesFamily x a).mul (powerSeriesFamily x b) : (a : ℕ × ℕ) → V⟦Γ⟧) a_1) g)
      c ∧
    c.1 + c.2 = n
⊢ ∃ (x_1 : ℕ × ℕ),
    Membership.mem (γ := Set (ℕ × ℕ))
        (Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
          HahnSeries.coeff (((powerSeriesFamily x a).mul (powerSeriesFamily x b) : (a : ℕ × ℕ) → V⟦Γ⟧) a_1) g)
        x_1 ∧
      x_1.1 + x_1.2 = n

Tactic:
use c
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_4
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : CommRing V
inst_5 : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : 0 < x.orderTop
n : ℕ
hn : Ne.{u_4 + 1} (α := V) (HahnSeries.coeff ((powerSeriesFamily x (a * b) : (a : ℕ) → V⟦Γ⟧) n) g) 0
c : ℕ × ℕ
hcn : c.1 + c.2 = n
hc :
  HSMul.hSMul (α := R) ((PowerSeries.coeff c.1 : (a : PowerSeries R) → R) a : R)
      (HSMul.hSMul (α := R) ((PowerSeries.coeff c.2 : (a : PowerSeries R) → R) b : R) ((x ^ n).coeff g)) ≠
    0
h₁ :
  (HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((PowerSeries.coeff c.1 : (a : PowerSeries R) → R) a : R)
            ((powers x : (a : ℕ) → V⟦Γ⟧) c.1 : V⟦Γ⟧) *
          HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((PowerSeries.coeff c.2 : (a : PowerSeries R) → R) b : R)
            ((powers x : (a : ℕ) → V⟦Γ⟧) c.2 : V⟦Γ⟧)).coeff
      g ≠
    0
⊢ Membership.mem (γ := Set (ℕ × ℕ))
      (Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
        HahnSeries.coeff (((powerSeriesFamily x a).mul (powerSeriesFamily x b) : (a : ℕ × ℕ) → V⟦Γ⟧) a_1) g)
      c ∧
    c.1 + c.2 = n

Tactic:
simp only [mul_toFun, smulFamily_toFun, Function.mem_support, hcn,
      and_true]

Premises used: HahnSeries.SummableFamily.mul_toFun, and_true, HahnSeries.SummableFamily.smulFamily_toFun, Function.mem_support
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_4
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : CommRing V
inst_5 : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : 0 < x.orderTop
n : ℕ
hn : Ne.{u_4 + 1} (α := V) (HahnSeries.coeff ((powerSeriesFamily x (a * b) : (a : ℕ) → V⟦Γ⟧) n) g) 0
c : ℕ × ℕ
hcn : c.1 + c.2 = n
hc :
  HSMul.hSMul (α := R) ((PowerSeries.coeff c.1 : (a : PowerSeries R) → R) a : R)
      (HSMul.hSMul (α := R) ((PowerSeries.coeff c.2 : (a : PowerSeries R) → R) b : R) ((x ^ n).coeff g)) ≠
    0
h₁ :
  (HSMul.hSMul (α := R) ((PowerSeries.coeff c.1 : (a : PowerSeries R) → R) a : R)
          (HSMul.hSMul (α := R) ((PowerSeries.coeff c.2 : (a : PowerSeries R) → R) b : R) (x ^ n))).coeff
      g ≠
    0
⊢ (HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((PowerSeries.coeff c.1 : (a : PowerSeries R) → R) a : R)
            ((powers x : (a : ℕ) → V⟦Γ⟧) c.1 : V⟦Γ⟧) *
          HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((PowerSeries.coeff c.2 : (a : PowerSeries R) → R) b : R)
            ((powers x : (a : ℕ) → V⟦Γ⟧) c.2 : V⟦Γ⟧)).coeff
      g ≠
    0

Tactic:
rw [powers_of_orderTop_pos h c.1, powers_of_orderTop_pos h c.2, Algebra.smul_mul_assoc,
      Algebra.mul_smul_comm, ← pow_add, hcn]

Premises used: Algebra.mul_smul_comm, pow_add, Prod.fst, Algebra.smul_mul_assoc, HahnSeries.SummableFamily.powers_of_orderTop_pos, Prod.snd
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_4
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : CommRing V
inst_5 : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : 0 < x.orderTop
n : ℕ
hn : Ne.{u_4 + 1} (α := V) (HahnSeries.coeff ((powerSeriesFamily x (a * b) : (a : ℕ) → V⟦Γ⟧) n) g) 0
c : ℕ × ℕ
hcn : c.1 + c.2 = n
hc :
  HSMul.hSMul (α := R) ((PowerSeries.coeff c.1 : (a : PowerSeries R) → R) a : R)
      (HSMul.hSMul (α := R) ((PowerSeries.coeff c.2 : (a : PowerSeries R) → R) b : R) ((x ^ n).coeff g)) ≠
    0
⊢ (HSMul.hSMul (α := R) ((PowerSeries.coeff c.1 : (a : PowerSeries R) → R) a : R)
          (HSMul.hSMul (α := R) ((PowerSeries.coeff c.2 : (a : PowerSeries R) → R) b : R) (x ^ n))).coeff
      g ≠
    0

Tactic:
simp [hc]
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_4
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : CommRing V
inst_5 : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : ¬0 < x.orderTop
neg :
  ∀ (x_1 : ℕ),
    Ne.{u_4 + 1} (α := V) (HahnSeries.coeff ((powerSeriesFamily x (a * b) : (a : ℕ) → V⟦Γ⟧) x_1) g) 0 →
      x_1 ∈
        (↑(image (fun (i : ℕ × ℕ) ↦ i.1 + i.2)
              (Set.Finite.toFinset (s :=
                Function.support.{0, u_4} (M := V) fun (a_2 : ℕ × ℕ) ↦
                  HahnSeries.coeff (((powerSeriesFamily x a).mul (powerSeriesFamily x b) : (a : ℕ × ℕ) → V⟦Γ⟧) a_2) g)
                ⋯)) :
          Set ℕ)
⊢ ((powerSeriesFamily x (a * b)).coeff g).support ⊆
    image (fun (i : ℕ × ℕ) ↦ i.1 + i.2) (((powerSeriesFamily x a).mul (powerSeriesFamily x b)).coeff g).support

Tactic:
simp only [coeff_support, Set.Finite.toFinset_subset, support_subset_iff]

Premises used: Set.Finite.toFinset_subset, HahnSeries.SummableFamily.coeff_support, Function.support_subset_iff
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_4
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : CommRing V
inst_5 : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : ¬0 < x.orderTop
n : ℕ
hn : Ne.{u_4 + 1} (α := V) (HahnSeries.coeff ((powerSeriesFamily x (a * b) : (a : ℕ) → V⟦Γ⟧) n) g) 0
pos :
  ∀ (hz : n = 0),
    n ∈
      (↑(image (fun (i : ℕ × ℕ) ↦ i.1 + i.2)
            (Set.Finite.toFinset (s :=
              Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
                HahnSeries.coeff (((powerSeriesFamily x a).mul (powerSeriesFamily x b) : (a : ℕ × ℕ) → V⟦Γ⟧) a_1) g)
              ⋯)) :
        Set ℕ)
neg :
  ∀ (hz : ¬n = 0),
    n ∈
      (↑(image (fun (i : ℕ × ℕ) ↦ i.1 + i.2)
            (Set.Finite.toFinset (s :=
              Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
                HahnSeries.coeff (((powerSeriesFamily x a).mul (powerSeriesFamily x b) : (a : ℕ × ℕ) → V⟦Γ⟧) a_1) g)
              ⋯)) :
        Set ℕ)
⊢ n ∈
    (↑(image (fun (i : ℕ × ℕ) ↦ i.1 + i.2)
          (Set.Finite.toFinset (s :=
            Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
              HahnSeries.coeff (((powerSeriesFamily x a).mul (powerSeriesFamily x b) : (a : ℕ × ℕ) → V⟦Γ⟧) a_1) g)
            ⋯)) :
      Set ℕ)

Tactic:
by_cases hz : n = 0
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_4
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : CommRing V
inst_5 : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : ¬0 < x.orderTop
n : ℕ
hn : Ne.{u_4 + 1} (α := V) (HahnSeries.coeff ((powerSeriesFamily x (a * b) : (a : ℕ) → V⟦Γ⟧) n) g) 0
hz : n = 0
⊢ g = 0 ∧
    HSMul.hSMul (β := V)
        (HMul.hMul (α := R) (β := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) a : R)
          ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) b : R))
        1 ≠
      0

Tactic:
simpa [hz, h] using hn
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_4
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : CommRing V
inst_5 : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : ¬0 < x.orderTop
n : ℕ
hn : Ne.{u_4 + 1} (α := V) (HahnSeries.coeff ((powerSeriesFamily x (a * b) : (a : ℕ) → V⟦Γ⟧) n) g) 0
hz : n = 0
⊢ g = 0 ∧
    HSMul.hSMul (β := V)
        (HMul.hMul (α := R) (β := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) a : R)
          ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) b : R))
        1 ≠
      0

Tactic:
have : g = 0 ∧ (a.constantCoeff * b.constantCoeff) • (1 : V) ≠ 0 := by
        simpa [hz, h] using hn
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_4
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : CommRing V
inst_5 : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : ¬0 < x.orderTop
n : ℕ
hn : Ne.{u_4 + 1} (α := V) (HahnSeries.coeff ((powerSeriesFamily x (a * b) : (a : ℕ) → V⟦Γ⟧) n) g) 0
hz : n = 0
this :
  g = 0 ∧
    HSMul.hSMul (β := V)
        (HMul.hMul (α := R) (β := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) a : R)
          ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) b : R))
        1 ≠
      0
pos :
  ∃
    x_1 ∈
      (↑(Set.Finite.toFinset (s :=
            Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
              HahnSeries.coeff (((powerSeriesFamily x a).mul (powerSeriesFamily x b) : (a : ℕ × ℕ) → V⟦Γ⟧) a_1) g)
            ⋯) :
        Set (ℕ × ℕ)),
    x_1.1 + x_1.2 = n
⊢ n ∈
    (↑(image (fun (i : ℕ × ℕ) ↦ i.1 + i.2)
          (Set.Finite.toFinset (s :=
            Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
              HahnSeries.coeff (((powerSeriesFamily x a).mul (powerSeriesFamily x b) : (a : ℕ × ℕ) → V⟦Γ⟧) a_1) g)
            ⋯)) :
      Set ℕ)

Tactic:
simp only [coe_image, Set.mem_image]

Premises used: Set.mem_image, Finset.coe_image
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_4
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : CommRing V
inst_5 : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : ¬0 < x.orderTop
n : ℕ
hn : Ne.{u_4 + 1} (α := V) (HahnSeries.coeff ((powerSeriesFamily x (a * b) : (a : ℕ) → V⟦Γ⟧) n) g) 0
hz : n = 0
this :
  g = 0 ∧
    HSMul.hSMul (β := V)
        (HMul.hMul (α := R) (β := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) a : R)
          ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) b : R))
        1 ≠
      0
h₁ :
  (0, 0) ∈
      (↑(Set.Finite.toFinset (s :=
            Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
              HahnSeries.coeff (((powerSeriesFamily x a).mul (powerSeriesFamily x b) : (a : ℕ × ℕ) → V⟦Γ⟧) a_1) g)
            ⋯) :
        Set (ℕ × ℕ)) ∧
    HAdd.hAdd (α := ℕ) (0, 0).1 (0, 0).2 = n
⊢ ∃
    x_1 ∈
      (↑(Set.Finite.toFinset (s :=
            Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
              HahnSeries.coeff (((powerSeriesFamily x a).mul (powerSeriesFamily x b) : (a : ℕ × ℕ) → V⟦Γ⟧) a_1) g)
            ⋯) :
        Set (ℕ × ℕ)),
    x_1.1 + x_1.2 = n

Tactic:
use (0, 0)

Premises used: Prod.mk, OfNat.ofNat