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⟦Γ⟧
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
⊢ (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

Tactic:
simp [this.2, this.1, h, hz, smul_smul, mul_comm]

Premises used: smul_smul, And.right, And.left, mul_comm
-- 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
⊢ 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 [h, hz] at 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
pos :
  ∀ (h : 0 < x.orderTop),
    (powerSeriesFamily x (a * b)).hsum = ((powerSeriesFamily x a).mul (powerSeriesFamily x b)).hsum
neg :
  ∀ (h : ¬0 < x.orderTop),
    (powerSeriesFamily x (a * b)).hsum = ((powerSeriesFamily x a).mul (powerSeriesFamily x b)).hsum
⊢ (powerSeriesFamily x (a * b)).hsum = ((powerSeriesFamily x a).mul (powerSeriesFamily x b)).hsum

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
h : 0 < x.orderTop
pos :
  ∀ (g : Γ),
    (powerSeriesFamily x (a * b)).hsum.coeff g = ((powerSeriesFamily x a).mul (powerSeriesFamily x b)).hsum.coeff g
⊢ (powerSeriesFamily x (a * b)).hsum = ((powerSeriesFamily x a).mul (powerSeriesFamily x b)).hsum

Tactic:
ext g
-- 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
h : 0 < x.orderTop
g : Γ
pos :
  Eq.{u_4 + 1} (α := V)
    (∑ x_1 ∈ ((powerSeriesFamily x (a * b)).coeff g).support,
      HSMul.hSMul (α := R) ((PowerSeries.coeff x_1 : (a : PowerSeries R) → R) (a * b) : R) ((x ^ x_1).coeff g))
    (∑ x_1 ∈ (((powerSeriesFamily x a).mul (powerSeriesFamily x b)).coeff g).support,
      HSMul.hSMul (α := R) ((PowerSeries.coeff x_1.2 : (a : PowerSeries R) → R) b : R)
        (HSMul.hSMul (α := R) ((PowerSeries.coeff x_1.1 : (a : PowerSeries R) → R) a : R)
          ((x ^ x_1.1 * x ^ x_1.2).coeff g)))
⊢ (powerSeriesFamily x (a * b)).hsum.coeff g = ((powerSeriesFamily x a).mul (powerSeriesFamily x b)).hsum.coeff g

Tactic:
simp only [coeff_hsum_eq_sum, smulFamily_toFun, h, powers_of_orderTop_pos,
      HahnSeries.coeff_smul, mul_toFun, Algebra.mul_smul_comm, Algebra.smul_mul_assoc]

Premises used: Algebra.mul_smul_comm, HahnSeries.SummableFamily.mul_toFun, HahnSeries.coeff_smul, HahnSeries.SummableFamily.smulFamily_toFun, Algebra.smul_mul_assoc, HahnSeries.SummableFamily.powers_of_orderTop_pos, HahnSeries.SummableFamily.coeff_hsum_eq_sum
-- 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
h : 0 < x.orderTop
g : Γ
i : ℕ
hi :
  Membership.mem (γ := Finset ℕ)
    (image (fun (i : ℕ × ℕ) ↦ i.1 + i.2) (((powerSeriesFamily x a).mul (powerSeriesFamily x b)).coeff g).support) i
his : i ∉ ((powerSeriesFamily x (a * b)).coeff g).support
⊢ HSMul.hSMul (α := R) ((PowerSeries.coeff i : (a : PowerSeries R) → R) (a * b) : R) ((x ^ i).coeff g) = 0

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

Premises used: Finset.sum_smul, PowerSeries.coeff_mul
-- 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
h : 0 < x.orderTop
g : Γ
pos :
  Eq.{u_4 + 1} (α := V)
    (∑
      x_1 ∈ image (fun (i : ℕ × ℕ) ↦ i.1 + i.2) (((powerSeriesFamily x a).mul (powerSeriesFamily x b)).coeff g).support,
      HSMul.hSMul (α := R) ((PowerSeries.coeff x_1 : (a : PowerSeries R) → R) (a * b) : R) ((x ^ x_1).coeff g))
    (∑ x_1 ∈ (((powerSeriesFamily x a).mul (powerSeriesFamily x b)).coeff g).support,
      HSMul.hSMul (α := R) ((PowerSeries.coeff x_1.2 : (a : PowerSeries R) → R) b : R)
        (HSMul.hSMul (α := R) ((PowerSeries.coeff x_1.1 : (a : PowerSeries R) → R) a : R)
          ((x ^ x_1.1 * x ^ x_1.2).coeff g)))
⊢ Eq.{u_4 + 1} (α := V)
    (∑ x_1 ∈ ((powerSeriesFamily x (a * b)).coeff g).support,
      HSMul.hSMul (α := R) ((PowerSeries.coeff x_1 : (a : PowerSeries R) → R) (a * b) : R) ((x ^ x_1).coeff g))
    (∑ x_1 ∈ (((powerSeriesFamily x a).mul (powerSeriesFamily x b)).coeff g).support,
      HSMul.hSMul (α := R) ((PowerSeries.coeff x_1.2 : (a : PowerSeries R) → R) b : R)
        (HSMul.hSMul (α := R) ((PowerSeries.coeff x_1.1 : (a : PowerSeries R) → R) a : R)
          ((x ^ x_1.1 * x ^ x_1.2).coeff g)))

Tactic:
rw [sum_subset (support_powerSeriesFamily_subset a b g)
      (fun i hi his ↦ by simpa [h, PowerSeries.coeff_mul, sum_smul] using his)]

Premises used: Finset.sum_subset, HahnSeries.SummableFamily.support_powerSeriesFamily_subset
-- 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
h : 0 < x.orderTop
g : Γ
pos :
  Eq.{u_4 + 1} (α := V)
    (∑
      x_1 ∈
        image (fun (i : ℕ × ℕ) ↦ i.1 + i.2)
          (Set.Finite.toFinset (s :=
            Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
              HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.2 : (a : PowerSeries R) → R) b : R)
                (HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.1 : (a : PowerSeries R) → R) a : R)
                  ((HMul.hMul (α := V⟦Γ⟧) (β := V⟦Γ⟧) ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.1 : V⟦Γ⟧)
                        ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.2 : V⟦Γ⟧)).coeff
                    g)))
            ⋯),
      ∑ i ∈ @antidiagonal _ Nat.instAddMonoid _ x_1,
        HMul.hMul (α := R) (β := R) ((PowerSeries.coeff i.1 : (a : PowerSeries R) → R) a : R)
            ((PowerSeries.coeff i.2 : (a : PowerSeries R) → R) b : R) •
          (x ^ x_1).coeff g)
    (∑
      x_1 ∈
        Set.Finite.toFinset (s :=
          Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
            HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.2 : (a : PowerSeries R) → R) b : R)
              (HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.1 : (a : PowerSeries R) → R) a : R)
                ((HMul.hMul (α := V⟦Γ⟧) (β := V⟦Γ⟧) ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.1 : V⟦Γ⟧)
                      ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.2 : V⟦Γ⟧)).coeff
                  g)))
          ⋯,
      HSMul.hSMul (α := R) ((PowerSeries.coeff x_1.2 : (a : PowerSeries R) → R) b : R)
        (HSMul.hSMul (α := R) ((PowerSeries.coeff x_1.1 : (a : PowerSeries R) → R) a : R)
          ((x ^ x_1.1 * x ^ x_1.2).coeff g)))
⊢ Eq.{u_4 + 1} (α := V)
    (∑
      x_1 ∈ image (fun (i : ℕ × ℕ) ↦ i.1 + i.2) (((powerSeriesFamily x a).mul (powerSeriesFamily x b)).coeff g).support,
      HSMul.hSMul (α := R) ((PowerSeries.coeff x_1 : (a : PowerSeries R) → R) (a * b) : R) ((x ^ x_1).coeff g))
    (∑ x_1 ∈ (((powerSeriesFamily x a).mul (powerSeriesFamily x b)).coeff g).support,
      HSMul.hSMul (α := R) ((PowerSeries.coeff x_1.2 : (a : PowerSeries R) → R) b : R)
        (HSMul.hSMul (α := R) ((PowerSeries.coeff x_1.1 : (a : PowerSeries R) → R) a : R)
          ((x ^ x_1.1 * x ^ x_1.2).coeff g)))

Tactic:
simp only [coeff_support, mul_toFun, smulFamily_toFun, Algebra.mul_smul_comm,
      Algebra.smul_mul_assoc, HahnSeries.coeff_smul, PowerSeries.coeff_mul, sum_smul]

Premises used: Finset.sum_smul, Algebra.mul_smul_comm, HahnSeries.SummableFamily.mul_toFun, HahnSeries.coeff_smul, HahnSeries.SummableFamily.coeff_support, PowerSeries.coeff_mul, HahnSeries.SummableFamily.smulFamily_toFun, Algebra.smul_mul_assoc
-- 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
h : 0 < x.orderTop
g : Γ
x_1 : ℕ × ℕ
h_1 :
  x_1 ∈
    (↑(Set.Finite.toFinset (s :=
          Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
            HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.2 : (a : PowerSeries R) → R) b : R)
              (HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.1 : (a : PowerSeries R) → R) a : R)
                ((HMul.hMul (α := V⟦Γ⟧) (β := V⟦Γ⟧) ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.1 : V⟦Γ⟧)
                      ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.2 : V⟦Γ⟧)).coeff
                  g)))
          ⋯) :
      Set (ℕ × ℕ))
x_2 : ℕ × ℕ
h_2 :
  x_2 ∈
    (↑(Set.Finite.toFinset (s :=
          Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
            HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.2 : (a : PowerSeries R) → R) b : R)
              (HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.1 : (a : PowerSeries R) → R) a : R)
                ((HMul.hMul (α := V⟦Γ⟧) (β := V⟦Γ⟧) ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.1 : V⟦Γ⟧)
                      ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.2 : V⟦Γ⟧)).coeff
                  g)))
          ⋯) :
      Set (ℕ × ℕ))
⊢ Eq (α := (_ : ℕ) × ℕ × ℕ)
      ((fun (x : ℕ × ℕ) ↦ (Sigma.mk (β := fun (i : ℕ) ↦ ℕ × ℕ) (x.1 + x.2) x : (_ : ℕ) × ℕ × ℕ)) x_1)
      ((fun (x : ℕ × ℕ) ↦ (Sigma.mk (β := fun (i : ℕ) ↦ ℕ × ℕ) (x.1 + x.2) x : (_ : ℕ) × ℕ × ℕ)) x_2) →
    x_1 = x_2

Tactic:
simp
-- 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
h : 0 < x.orderTop
g : Γ
x_1 : ℕ × ℕ
h_1 :
  x_1 ∈
    Set.Finite.toFinset (s :=
      Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
        HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.2 : (a : PowerSeries R) → R) b : R)
          (HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.1 : (a : PowerSeries R) → R) a : R)
            ((HMul.hMul (α := V⟦Γ⟧) (β := V⟦Γ⟧) ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.1 : V⟦Γ⟧)
                  ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.2 : V⟦Γ⟧)).coeff
              g)))
      ⋯
⊢ HSMul.hSMul (α := R) ((PowerSeries.coeff x_1.2 : (a : PowerSeries R) → R) b : R)
      (HSMul.hSMul (α := R) ((PowerSeries.coeff x_1.1 : (a : PowerSeries R) → R) a : R)
        ((x ^ x_1.1 * x ^ x_1.2).coeff g)) =
    HMul.hMul (α := R) (β := R)
        ((PowerSeries.coeff
                (Sigma.snd (β := fun (i : ℕ) ↦ ℕ × ℕ)
                    ((fun (x : ℕ × ℕ) ↦ (Sigma.mk (β := fun (i : ℕ) ↦ ℕ × ℕ) (x.1 + x.2) x : (_ : ℕ) × ℕ × ℕ)) x_1)).1 :
              (a : PowerSeries R) → R)
            a :
          R)
        ((PowerSeries.coeff
                (Sigma.snd (β := fun (i : ℕ) ↦ ℕ × ℕ)
                    ((fun (x : ℕ × ℕ) ↦ (Sigma.mk (β := fun (i : ℕ) ↦ ℕ × ℕ) (x.1 + x.2) x : (_ : ℕ) × ℕ × ℕ)) x_1)).2 :
              (a : PowerSeries R) → R)
            b :
          R) •
      (HPow.hPow (β := ℕ) x
            (Sigma.fst (β := fun (i : ℕ) ↦ ℕ × ℕ)
              ((fun (x : ℕ × ℕ) ↦ (Sigma.mk (β := fun (i : ℕ) ↦ ℕ × ℕ) (x.1 + x.2) x : (_ : ℕ) × ℕ × ℕ)) x_1))).coeff
        g

Tactic:
simp [smul_smul, mul_comm, pow_add]

Premises used: pow_add, smul_smul, mul_comm
-- 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
h : 0 < x.orderTop
g : Γ
ij : ℕ × ℕ
hij :
  ij ∈
    (↑(Set.Finite.toFinset (s :=
          Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
            HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.2 : (a : PowerSeries R) → R) b : R)
              (HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.1 : (a : PowerSeries R) → R) a : R)
                ((HMul.hMul (α := V⟦Γ⟧) (β := V⟦Γ⟧) ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.1 : V⟦Γ⟧)
                      ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.2 : V⟦Γ⟧)).coeff
                  g)))
          ⋯) :
      Set (ℕ × ℕ))
pos :
  ∃ (a_1 : ℕ) (b_1 : ℕ),
    (a_1, b_1) ∈
        Set.Finite.toFinset (s :=
          Function.support.{0, u_4} (M := V) fun (a_2 : ℕ × ℕ) ↦
            HSMul.hSMul (α := R) ((PowerSeries.coeff a_2.2 : (a : PowerSeries R) → R) b : R)
              (HSMul.hSMul (α := R) ((PowerSeries.coeff a_2.1 : (a : PowerSeries R) → R) a : R)
                ((HMul.hMul (α := V⟦Γ⟧) (β := V⟦Γ⟧) ((powers x : (a : ℕ) → V⟦Γ⟧) a_2.1 : V⟦Γ⟧)
                      ((powers x : (a : ℕ) → V⟦Γ⟧) a_2.2 : V⟦Γ⟧)).coeff
                  g)))
          ⋯ ∧
      a_1 + b_1 = ij.1 + ij.2
⊢ (fun (x : ℕ × ℕ) ↦ (Sigma.mk (β := fun (i : ℕ) ↦ ℕ × ℕ) (x.1 + x.2) x : (_ : ℕ) × ℕ × ℕ)) ij ∈
    (↑(Finset.sigma (α := fun (a : ℕ) ↦ ℕ × ℕ)
          (image (fun (i : ℕ × ℕ) ↦ i.1 + i.2)
            (Set.Finite.toFinset (s :=
              Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
                HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.2 : (a : PowerSeries R) → R) b : R)
                  (HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.1 : (a : PowerSeries R) → R) a : R)
                    ((HMul.hMul (α := V⟦Γ⟧) (β := V⟦Γ⟧) ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.1 : V⟦Γ⟧)
                          ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.2 : V⟦Γ⟧)).coeff
                      g)))
              ⋯))
          (@antidiagonal _ Nat.instAddMonoid _)) :
      Set ((_ : ℕ) × ℕ × ℕ))

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

Premises used: and_true, Set.mem_image, Set.mem_sigma_iff, Finset.coe_image, Finset.HasAntidiagonal.mem_antidiagonal, Prod.exists, Finset.mem_coe, Finset.coe_sigma
-- 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
h : 0 < x.orderTop
g : Γ
ij : ℕ × ℕ
hij :
  ij ∈
    (↑(Set.Finite.toFinset (s :=
          Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
            HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.2 : (a : PowerSeries R) → R) b : R)
              (HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.1 : (a : PowerSeries R) → R) a : R)
                ((HMul.hMul (α := V⟦Γ⟧) (β := V⟦Γ⟧) ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.1 : V⟦Γ⟧)
                      ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.2 : V⟦Γ⟧)).coeff
                  g)))
          ⋯) :
      Set (ℕ × ℕ))
h₁ :
  (ij.1, ij.2) ∈
      Set.Finite.toFinset (s :=
        Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
          HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.2 : (a : PowerSeries R) → R) b : R)
            (HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.1 : (a : PowerSeries R) → R) a : R)
              ((HMul.hMul (α := V⟦Γ⟧) (β := V⟦Γ⟧) ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.1 : V⟦Γ⟧)
                    ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.2 : V⟦Γ⟧)).coeff
                g)))
        ⋯ ∧
    ij.1 + ij.2 = ij.1 + ij.2
⊢ ∃ (a_1 : ℕ) (b_1 : ℕ),
    (a_1, b_1) ∈
        Set.Finite.toFinset (s :=
          Function.support.{0, u_4} (M := V) fun (a_2 : ℕ × ℕ) ↦
            HSMul.hSMul (α := R) ((PowerSeries.coeff a_2.2 : (a : PowerSeries R) → R) b : R)
              (HSMul.hSMul (α := R) ((PowerSeries.coeff a_2.1 : (a : PowerSeries R) → R) a : R)
                ((HMul.hMul (α := V⟦Γ⟧) (β := V⟦Γ⟧) ((powers x : (a : ℕ) → V⟦Γ⟧) a_2.1 : V⟦Γ⟧)
                      ((powers x : (a : ℕ) → V⟦Γ⟧) a_2.2 : V⟦Γ⟧)).coeff
                  g)))
          ⋯ ∧
      a_1 + b_1 = ij.1 + ij.2

Tactic:
use ij.1, ij.2

Premises used: Prod.fst, 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
h : 0 < x.orderTop
g : Γ
ij : ℕ × ℕ
hij :
  ij ∈
    (↑(Set.Finite.toFinset (s :=
          Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
            HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.2 : (a : PowerSeries R) → R) b : R)
              (HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.1 : (a : PowerSeries R) → R) a : R)
                ((HMul.hMul (α := V⟦Γ⟧) (β := V⟦Γ⟧) ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.1 : V⟦Γ⟧)
                      ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.2 : V⟦Γ⟧)).coeff
                  g)))
          ⋯) :
      Set (ℕ × ℕ))
⊢ (ij.1, ij.2) ∈
      Set.Finite.toFinset (s :=
        Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
          HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.2 : (a : PowerSeries R) → R) b : R)
            (HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.1 : (a : PowerSeries R) → R) a : R)
              ((HMul.hMul (α := V⟦Γ⟧) (β := V⟦Γ⟧) ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.1 : V⟦Γ⟧)
                    ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.2 : V⟦Γ⟧)).coeff
                g)))
        ⋯ ∧
    ij.1 + ij.2 = ij.1 + ij.2

Tactic:
simp_all
-- 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
h : 0 < x.orderTop
g : Γ
i : (_ : ℕ) × ℕ × ℕ
hi :
  Membership.mem (γ := Finset ((_ : ℕ) × ℕ × ℕ))
    (Finset.sigma (α := fun (a : ℕ) ↦ ℕ × ℕ)
      (image (fun (i : ℕ × ℕ) ↦ i.1 + i.2)
        (Set.Finite.toFinset (s :=
          Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
            HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.2 : (a : PowerSeries R) → R) b : R)
              (HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.1 : (a : PowerSeries R) → R) a : R)
                ((HMul.hMul (α := V⟦Γ⟧) (β := V⟦Γ⟧) ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.1 : V⟦Γ⟧)
                      ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.2 : V⟦Γ⟧)).coeff
                  g)))
          ⋯))
      (@antidiagonal _ Nat.instAddMonoid _))
    i
his :
  i ∉
    (fun (x : ℕ × ℕ) ↦ Sigma.mk (β := fun (i : ℕ) ↦ ℕ × ℕ) (x.1 + x.2) x) ''
      (↑(Set.Finite.toFinset (s :=
            Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
              HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.2 : (a : PowerSeries R) → R) b : R)
                (HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.1 : (a : PowerSeries R) → R) a : R)
                  ((HMul.hMul (α := V⟦Γ⟧) (β := V⟦Γ⟧) ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.1 : V⟦Γ⟧)
                        ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.2 : V⟦Γ⟧)).coeff
                    g)))
            ⋯) :
        Set (ℕ × ℕ))
m n : ℕ
contrapose! :
  HSMul.hSMul (α := R) ((PowerSeries.coeff n : (a : PowerSeries R) → R) b : R)
        (HSMul.hSMul (α := R) ((PowerSeries.coeff m : (a : PowerSeries R) → R) a : R) ((x ^ m * x ^ n).coeff g)) ≠
      0 →
    Sigma.mk (β := fun (i : ℕ) ↦ ℕ × ℕ) (m + n) (m, n) ≠ i
⊢ Sigma.mk (β := fun (i : ℕ) ↦ ℕ × ℕ) (m + n) (m, n) = i →
    HSMul.hSMul (α := R) ((PowerSeries.coeff n : (a : PowerSeries R) → R) b : R)
        (HSMul.hSMul (α := R) ((PowerSeries.coeff m : (a : PowerSeries R) → R) a : R) ((x ^ m * x ^ n).coeff g)) =
      0

Tactic:
contrapose!
-- 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
h : 0 < x.orderTop
g : Γ
i : (_ : ℕ) × ℕ × ℕ
hi :
  Membership.mem (γ := Finset ((_ : ℕ) × ℕ × ℕ))
    (Finset.sigma (α := fun (a : ℕ) ↦ ℕ × ℕ)
      (image (fun (i : ℕ × ℕ) ↦ i.1 + i.2)
        (Set.Finite.toFinset (s :=
          Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
            HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.2 : (a : PowerSeries R) → R) b : R)
              (HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.1 : (a : PowerSeries R) → R) a : R)
                ((HMul.hMul (α := V⟦Γ⟧) (β := V⟦Γ⟧) ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.1 : V⟦Γ⟧)
                      ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.2 : V⟦Γ⟧)).coeff
                  g)))
          ⋯))
      (@antidiagonal _ Nat.instAddMonoid _))
    i
his :
  i ∉
    (fun (x : ℕ × ℕ) ↦ Sigma.mk (β := fun (i : ℕ) ↦ ℕ × ℕ) (x.1 + x.2) x) ''
      (↑(Set.Finite.toFinset (s :=
            Function.support.{0, u_4} (M := V) fun (a_1 : ℕ × ℕ) ↦
              HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.2 : (a : PowerSeries R) → R) b : R)
                (HSMul.hSMul (α := R) ((PowerSeries.coeff a_1.1 : (a : PowerSeries R) → R) a : R)
                  ((HMul.hMul (α := V⟦Γ⟧) (β := V⟦Γ⟧) ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.1 : V⟦Γ⟧)
                        ((powers x : (a : ℕ) → V⟦Γ⟧) a_1.2 : V⟦Γ⟧)).coeff
                    g)))
            ⋯) :
        Set (ℕ × ℕ))
m n : ℕ
⊢ ∀ (x_1 x_2 : ℕ),
    ¬HSMul.hSMul (α := R) ((PowerSeries.coeff x_2 : (a : PowerSeries R) → R) b : R)
            (HSMul.hSMul (α := R) ((PowerSeries.coeff x_1 : (a : PowerSeries R) → R) a : R)
              ((x ^ x_1 * x ^ x_2).coeff g)) =
          0 →
      ¬Sigma.mk (β := fun (i : ℕ) ↦ ℕ × ℕ) (x_1 + x_2) (x_1, x_2) = i

Tactic:
simp only [powers_of_orderTop_pos h, Set.Finite.coe_toFinset, Set.mem_image,
          Function.mem_support, ne_eq, Prod.exists, not_exists, not_and] at his

Premises used: Set.mem_image, not_exists, Set.Finite.coe_toFinset, ne_eq, Function.mem_support, HahnSeries.SummableFamily.powers_of_orderTop_pos, Prod.exists, not_and