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
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
m n : ℕ
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
⊢ 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:
his m 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⟦Γ⟧
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
m n : ℕ
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
⊢ 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:
exact his m 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⟦Γ⟧
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 (ℕ × ℕ))
⊢ ∀ (j k : ℕ),
    Sigma.mk (β := fun (i : ℕ) ↦ ℕ × ℕ) (j + k) (j, k) = i →
      HSMul.hSMul (α := R) ((PowerSeries.coeff k : (a : PowerSeries R) → R) b : R)
          (HSMul.hSMul (α := R) ((PowerSeries.coeff j : (a : PowerSeries R) → R) a : R) ((x ^ j * x ^ k).coeff g)) =
        0

Tactic:
have hisc : ∀ j k : ℕ, ⟨j + k, (j, k)⟩ = i → (PowerSeries.coeff k) b •
          (PowerSeries.coeff j a • (x ^ j * x ^ k).coeff g) = 0 := by
        intro m n
        contrapose!
        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
        exact his m 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⟦Γ⟧
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 (ℕ × ℕ))
hisc :
  ∀ (j k : ℕ),
    Sigma.mk (β := fun (i : ℕ) ↦ ℕ × ℕ) (j + k) (j, k) = i →
      HSMul.hSMul (α := R) ((PowerSeries.coeff k : (a : PowerSeries R) → R) b : R)
          (HSMul.hSMul (α := R) ((PowerSeries.coeff j : (a : PowerSeries R) → R) a : R) ((x ^ j * x ^ k).coeff g)) =
        0
⊢ Membership.mem (γ := Finset ℕ)
      (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.fst (β := fun (i : ℕ) ↦ ℕ × ℕ)) ∧
    i.snd (β := fun (i : ℕ) ↦ ℕ × ℕ).1 + i.snd (β := fun (i : ℕ) ↦ ℕ × ℕ).2 = i.fst (β := fun (i : ℕ) ↦ ℕ × ℕ)

Tactic:
simp only [mem_sigma, mem_antidiagonal] at hi

Premises used: Finset.mem_sigma, Finset.HasAntidiagonal.mem_antidiagonal
-- 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 : (_ : ℕ) × ℕ × ℕ
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 (ℕ × ℕ))
hisc :
  ∀ (j k : ℕ),
    Sigma.mk (β := fun (i : ℕ) ↦ ℕ × ℕ) (j + k) (j, k) = i →
      HSMul.hSMul (α := R) ((PowerSeries.coeff k : (a : PowerSeries R) → R) b : R)
          (HSMul.hSMul (α := R) ((PowerSeries.coeff j : (a : PowerSeries R) → R) a : R) ((x ^ j * x ^ k).coeff g)) =
        0
hi :
  Membership.mem (γ := Finset ℕ)
      (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.fst (β := fun (i : ℕ) ↦ ℕ × ℕ)) ∧
    i.snd (β := fun (i : ℕ) ↦ ℕ × ℕ).1 + i.snd (β := fun (i : ℕ) ↦ ℕ × ℕ).2 = i.fst (β := fun (i : ℕ) ↦ ℕ × ℕ)
pos :
  HSMul.hSMul (α := R) ((PowerSeries.coeff i.snd (β := fun (i : ℕ) ↦ ℕ × ℕ).2 : (a : PowerSeries R) → R) b : R)
      (HSMul.hSMul (α := R) ((PowerSeries.coeff i.snd (β := fun (i : ℕ) ↦ ℕ × ℕ).1 : (a : PowerSeries R) → R) a : R)
        ((x ^ i.snd (β := fun (i : ℕ) ↦ ℕ × ℕ).1 * x ^ i.snd (β := fun (i : ℕ) ↦ ℕ × ℕ).2).coeff g)) =
    0
⊢ HMul.hMul (α := R) (β := R) ((PowerSeries.coeff i.snd (β := fun (i : ℕ) ↦ ℕ × ℕ).1 : (a : PowerSeries R) → R) a : R)
        ((PowerSeries.coeff i.snd (β := fun (i : ℕ) ↦ ℕ × ℕ).2 : (a : PowerSeries R) → R) b : R) •
      (x ^ i.fst (β := fun (i : ℕ) ↦ ℕ × ℕ)).coeff g =
    0

Tactic:
rw [mul_comm ((PowerSeries.coeff i.snd.1) a), ← hi.2, mul_smul, pow_add]

Premises used: pow_add, PowerSeries.coeff, Prod.fst, And.right, mul_comm, Sigma.snd, DFunLike.coe, 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
h : 0 < x.orderTop
g : Γ
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 (ℕ × ℕ))
hisc :
  ∀ (j k : ℕ),
    Sigma.mk (β := fun (i : ℕ) ↦ ℕ × ℕ) (j + k) (j, k) = i →
      HSMul.hSMul (α := R) ((PowerSeries.coeff k : (a : PowerSeries R) → R) b : R)
          (HSMul.hSMul (α := R) ((PowerSeries.coeff j : (a : PowerSeries R) → R) a : R) ((x ^ j * x ^ k).coeff g)) =
        0
hi :
  Membership.mem (γ := Finset ℕ)
      (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.fst (β := fun (i : ℕ) ↦ ℕ × ℕ)) ∧
    i.snd (β := fun (i : ℕ) ↦ ℕ × ℕ).1 + i.snd (β := fun (i : ℕ) ↦ ℕ × ℕ).2 = i.fst (β := fun (i : ℕ) ↦ ℕ × ℕ)
⊢ Eq.recOn (motive :=
      fun (x : ℕ)
        (x_1 :
          Sigma.fst (β := fun (a : ℕ) ↦ ℕ × ℕ)
              (Sigma.mk (β := fun (i : ℕ) ↦ ℕ × ℕ)
                (i.snd (β := fun (i : ℕ) ↦ ℕ × ℕ).1 + i.snd (β := fun (i : ℕ) ↦ ℕ × ℕ).2)
                (i.snd (β := fun (i : ℕ) ↦ ℕ × ℕ).1, i.snd (β := fun (i : ℕ) ↦ ℕ × ℕ).2)) =
            x) ↦
      ℕ × ℕ) ⋯
      (Sigma.snd (β := fun (a : ℕ) ↦ ℕ × ℕ)
        (Sigma.mk (β := fun (i : ℕ) ↦ ℕ × ℕ) (i.snd (β := fun (i : ℕ) ↦ ℕ × ℕ).1 + i.snd (β := fun (i : ℕ) ↦ ℕ × ℕ).2)
          (i.snd (β := fun (i : ℕ) ↦ ℕ × ℕ).1, i.snd (β := fun (i : ℕ) ↦ ℕ × ℕ).2))) =
    i.snd (β := fun (a : ℕ) ↦ ℕ × ℕ)

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 : Γ
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 (ℕ × ℕ))
hisc :
  ∀ (j k : ℕ),
    Sigma.mk (β := fun (i : ℕ) ↦ ℕ × ℕ) (j + k) (j, k) = i →
      HSMul.hSMul (α := R) ((PowerSeries.coeff k : (a : PowerSeries R) → R) b : R)
          (HSMul.hSMul (α := R) ((PowerSeries.coeff j : (a : PowerSeries R) → R) a : R) ((x ^ j * x ^ k).coeff g)) =
        0
hi :
  Membership.mem (γ := Finset ℕ)
      (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.fst (β := fun (i : ℕ) ↦ ℕ × ℕ)) ∧
    i.snd (β := fun (i : ℕ) ↦ ℕ × ℕ).1 + i.snd (β := fun (i : ℕ) ↦ ℕ × ℕ).2 = i.fst (β := fun (i : ℕ) ↦ ℕ × ℕ)
⊢ HSMul.hSMul (α := R) ((PowerSeries.coeff i.snd (β := fun (i : ℕ) ↦ ℕ × ℕ).2 : (a : PowerSeries R) → R) b : R)
      (HSMul.hSMul (α := R) ((PowerSeries.coeff i.snd (β := fun (i : ℕ) ↦ ℕ × ℕ).1 : (a : PowerSeries R) → R) a : R)
        ((x ^ i.snd (β := fun (i : ℕ) ↦ ℕ × ℕ).1 * x ^ i.snd (β := fun (i : ℕ) ↦ ℕ × ℕ).2).coeff g)) =
    0

Tactic:
exact hisc i.snd.1 i.snd.2 <| Sigma.eq hi.2 (by simp)

Premises used: Sigma.eq, Prod.fst, Sigma.snd, 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
neg :
  HSMul.hSMul (β := V⟦Γ⟧)
      (HMul.hMul (α := R) (β := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) a : R)
        ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) b : R))
      1 =
    HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) a : R) 1 *
      HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) b : R) 1
⊢ (powerSeriesFamily x (a * b)).hsum = ((powerSeriesFamily x a).mul (powerSeriesFamily x b)).hsum

Tactic:
simp only [h, not_false_eq_true, powerSeriesFamily_of_not_orderTop_pos,
      powerSeriesFamily_hsum_zero, map_mul, hsum_mul]

Premises used: HahnSeries.SummableFamily.powerSeriesFamily_of_not_orderTop_pos, HahnSeries.SummableFamily.powerSeriesFamily_hsum_zero, map_mul, HahnSeries.SummableFamily.hsum_mul, not_false_eq_true
-- 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
neg :
  HSMul.hSMul (β := V⟦Γ⟧)
      (HMul.hMul (α := R) (β := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) a : R)
        ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) b : R))
      1 =
    HMul.hMul (α := R) (β := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) a : R)
        ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) b : R) •
      HMul.hMul (α := V⟦Γ⟧) 1 1
neg₁ neg₂ :
  HSMul.hSMul (β := V⟦Γ⟧)
      (HMul.hMul (α := R) (β := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) a : R)
        ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) b : R))
      1 =
    HSMul.hSMul (β := V⟦Γ⟧)
      (HMul.hMul (α := R) (β := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) a : R)
        ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) b : R))
      1
⊢ HSMul.hSMul (β := V⟦Γ⟧)
      (HMul.hMul (α := R) (β := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) a : R)
        ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) b : R))
      1 =
    HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) a : R) 1 *
      HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) b : R) 1

Tactic:
rw [smul_mul_smul_comm, mul_one]

Premises used: smul_mul_smul_comm, mul_one
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
simp :
  Eq (α := R⟦Γ⟧)
    { coeff := fun (g : Γ) ↦ ∑ᶠ (i : ℕ), (if i = 0 then (if 0 < x.orderTop then x else 0) ^ i else 0).coeff g,
      isPWO_support' := ⋯ }
    1
⊢ (powerSeriesFamily (R := R) x 1).hsum = 1

Tactic:
simp only [hsum, smulFamily_toFun, coeff_one, powers_toFun, ite_smul, one_smul, zero_smul]

Premises used: one_smul, zero_smul, HahnSeries.SummableFamily.smulFamily_toFun, PowerSeries.coeff_one, HahnSeries.SummableFamily.powers_toFun, ite_smul, HahnSeries.SummableFamily.hsum
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
coeff :
  ∀ (g : Γ),
    Eq.{u_3 + 1} (α := R)
      (HahnSeries.coeff
        { coeff := fun (g : Γ) ↦ ∑ᶠ (i : ℕ), (if i = 0 then (if 0 < x.orderTop then x else 0) ^ i else 0).coeff g,
          isPWO_support' := ⋯ }
        g)
      (HahnSeries.coeff 1 g)
⊢ Eq (α := R⟦Γ⟧)
    { coeff := fun (g : Γ) ↦ ∑ᶠ (i : ℕ), (if i = 0 then (if 0 < x.orderTop then x else 0) ^ i else 0).coeff g,
      isPWO_support' := ⋯ }
    1

Tactic:
ext g
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
g : Γ
n : ℕ
hn : n ≠ 0
⊢ (if n = 0 then (if 0 < x.orderTop then x else 0) ^ n else 0).coeff g = 0

Tactic:
simp [hn]
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
g : Γ
coeff :
  (if Eq (α := ℕ) 0 0 then HPow.hPow (β := ℕ) (if 0 < x.orderTop then x else 0) 0 else 0).coeff g = HahnSeries.coeff 1 g
⊢ Eq.{u_3 + 1} (α := R) (∑ᶠ (i : ℕ), (if i = 0 then (if 0 < x.orderTop then x else 0) ^ i else 0).coeff g)
    (HahnSeries.coeff 1 g)

Tactic:
rw [finsum_eq_single _ (0 : ℕ) (fun n hn => by simp [hn])]

Premises used: OfNat.ofNat, finsum_eq_single
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
g : Γ
⊢ (if Eq (α := ℕ) 0 0 then HPow.hPow (β := ℕ) (if 0 < x.orderTop then x else 0) 0 else 0).coeff g = HahnSeries.coeff 1 g

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
a b : R⟦X⟧
⊢ (powerSeriesFamily x (a * b)).hsum = (powerSeriesFamily x a).hsum * (powerSeriesFamily x b).hsum

Tactic:
simp only [← hsum_mul, hsum_powerSeriesFamily_mul]

Premises used: HahnSeries.SummableFamily.hsum_powerSeriesFamily_mul, HahnSeries.SummableFamily.hsum_mul
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
⊢ (powerSeriesFamily (R := R) x 0).hsum = 0

Tactic:
simp only [hsum, smulFamily_toFun, map_zero, zero_smul,
      coeff_zero, finsum_zero, mk_eq_zero, Pi.zero_def]

Premises used: finsum_zero, map_zero, Pi.zero_def, zero_smul, HahnSeries.SummableFamily.smulFamily_toFun, HahnSeries.mk_eq_zero, HahnSeries.coeff_zero, HahnSeries.SummableFamily.hsum
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
a b : R⟦X⟧
⊢ (powerSeriesFamily x (a + b)).hsum = (powerSeriesFamily x a).hsum + (powerSeriesFamily x b).hsum

Tactic:
simp only [powerSeriesFamily_add, hsum_add]

Premises used: HahnSeries.SummableFamily.powerSeriesFamily_add, HahnSeries.SummableFamily.hsum_add
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
r : R
simp : (powerSeriesFamily (R := R) x ((C : (a : R) → R⟦X⟧) r)).hsum = (algebraMap R R⟦Γ⟧ : (a : R) → R⟦Γ⟧) r
⊢ (powerSeriesFamily (R := R) x ((algebraMap R R⟦X⟧ : (a : R) → R⟦X⟧) r)).hsum = (algebraMap R R⟦Γ⟧ : (a : R) → R⟦Γ⟧) r

Tactic:
simp only [algebraMap_eq]

Premises used: PowerSeries.algebraMap_eq
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
r : R
coeff :
  ∀ (g : Γ),
    (powerSeriesFamily (R := R) x ((C : (a : R) → R⟦X⟧) r)).hsum.coeff g =
      HahnSeries.coeff ((algebraMap R R⟦Γ⟧ : (a : R) → R⟦Γ⟧) r) g
⊢ (powerSeriesFamily (R := R) x ((C : (a : R) → R⟦X⟧) r)).hsum = (algebraMap R R⟦Γ⟧ : (a : R) → R⟦Γ⟧) r

Tactic:
ext g