awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
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
⊢ 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 ℕ)
have 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)
            sorry)) :
      Set ℕ)
Tactic: by_cases hz : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
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 ℕ)
⊢ 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 ℕ)
have 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)
            sorry)) :
      Set ℕ)
Tactic: by_cases hz : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (hypothesis)
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 ℕ)
have 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
Tactic: have : g = 0 ∧ (a.constantCoeff * b.constantCoeff) • (1 : V) ≠ 0 := by
        simpa [hz, h] using hn
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
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
⊢ 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 ℕ)
have 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)
          sorry) :
      Set (ℕ × ℕ)),
  x_1.1 + x_1.2 = n
Tactic: simp only [coe_image, Set.mem_image]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
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
⊢ ∃
    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
have 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)
          sorry) :
      Set (ℕ × ℕ)) ∧
  HAdd.hAdd (α := ℕ) (0, 0).1 (0, 0).2 = n
Tactic: use (0, 0)
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
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
⊢ (powerSeriesFamily x (a * b)).hsum = ((powerSeriesFamily x a).mul (powerSeriesFamily x b)).hsum
have pos : ∀ (h : 0 < x.orderTop), (powerSeriesFamily x (a * b)).hsum = ((powerSeriesFamily x a).mul (powerSeriesFamily x b)).hsum
Tactic: by_cases h : 0 < x.orderTop
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
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
⊢ (powerSeriesFamily x (a * b)).hsum = ((powerSeriesFamily x a).mul (powerSeriesFamily x b)).hsum
have neg : ∀ (h : ¬0 < x.orderTop), (powerSeriesFamily x (a * b)).hsum = ((powerSeriesFamily x a).mul (powerSeriesFamily x b)).hsum
Tactic: by_cases h : 0 < x.orderTop
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
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
⊢ (powerSeriesFamily x (a * b)).hsum = ((powerSeriesFamily x a).mul (powerSeriesFamily x b)).hsum
have pos : ∀ (g : Γ),
  (powerSeriesFamily x (a * b)).hsum.coeff g = ((powerSeriesFamily x a).mul (powerSeriesFamily x b)).hsum.coeff g
Tactic: ext g
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
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 : Γ
⊢ (powerSeriesFamily x (a * b)).hsum.coeff g = ((powerSeriesFamily x a).mul (powerSeriesFamily x b)).hsum.coeff g
have 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)))
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]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
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 : Γ
⊢ 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)))
have 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)))
Tactic: rw [sum_subset (support_powerSeriesFamily_subset a b g)
      (fun i hi his ↦ by simpa [h, PowerSeries.coeff_mul, sum_smul] using his)]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
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 : Γ
⊢ 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)))
have 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)))
          sorry),
    ∑ 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)))
        sorry,
    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]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
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 (ℕ × ℕ))
⊢ (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 ((_ : ℕ) × ℕ × ℕ))
have 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)))
        sorry ∧
    a_1 + b_1 = ij.1 + ij.2
Tactic: simp only [coe_sigma, coe_image, Set.mem_sigma_iff, Set.mem_image, Prod.exists, mem_coe,
        mem_antidiagonal, and_true]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
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 (ℕ × ℕ))
⊢ ∃ (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
have 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)))
      sorry ∧
  ij.1 + ij.2 = ij.1 + ij.2
Tactic: use ij.1, ij.2
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
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 : ℕ
⊢ 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
have 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
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (hypothesis)
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 : ℕ
⊢ 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
have his₁ : ∀ (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
Cleared hypotheses: his