awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (ℕ × ℕ))
⊢ 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
have 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
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
-- 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 (ℕ × ℕ))
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
⊢ 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
have 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)))
        sorry))
    (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
Cleared hypotheses: hi
-- 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 : (_ : ℕ) × ℕ × ℕ
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 : ℕ) ↦ ℕ × ℕ)
⊢ 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
have 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
Tactic: rw [mul_comm ((PowerSeries.coeff i.snd.1) a), ← hi.2, mul_smul, pow_add]
-- 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 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
Tactic: simp only [h, not_false_eq_true, powerSeriesFamily_of_not_orderTop_pos,
      powerSeriesFamily_hsum_zero, map_mul, hsum_mul]
-- 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
⊢ 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
have 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
Tactic: rw [smul_mul_smul_comm, mul_one]
-- 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
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
⊢ 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
have 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
Tactic: rw [smul_mul_smul_comm, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
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 1).hsum = 1
have 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' := sorry }
  1
Tactic: simp only [hsum, smulFamily_toFun, coeff_one, powers_toFun, ite_smul, one_smul, zero_smul]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
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⟦Γ⟧
⊢ 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
have 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' := sorry }
      g)
    (HahnSeries.coeff 1 g)
Tactic: ext g
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
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 : Γ
⊢ 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)
have 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
Tactic: rw [finsum_eq_single _ (0 : ℕ) (fun n hn => by simp [hn])]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
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
⊢ (powerSeriesFamily (R := R) x ((algebraMap R R⟦X⟧ : (a : R) → R⟦X⟧) r)).hsum = (algebraMap R R⟦Γ⟧ : (a : R) → R⟦Γ⟧) r
have simp : (powerSeriesFamily (R := R) x ((C : (a : R) → R⟦X⟧) r)).hsum = (algebraMap R R⟦Γ⟧ : (a : R) → R⟦Γ⟧) r
Tactic: simp only [algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
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
⊢ (powerSeriesFamily (R := R) x ((C : (a : R) → R⟦X⟧) r)).hsum = (algebraMap R R⟦Γ⟧ : (a : R) → R⟦Γ⟧) r
have 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
Tactic: ext g
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
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
g : Γ
⊢ (powerSeriesFamily (R := R) x ((C : (a : R) → R⟦X⟧) r)).hsum.coeff g =
    HahnSeries.coeff ((algebraMap R R⟦Γ⟧ : (a : R) → R⟦Γ⟧) r) g
have coeff : Eq.{u_3 + 1} (α := R) (∑ᶠ (i : ℕ), (if i = 0 then r • (if 0 < x.orderTop then x else 0) ^ i else 0).coeff g)
  (HahnSeries.coeff ((algebraMap R R⟦Γ⟧ : (a : R) → R⟦Γ⟧) r) g)
Tactic: simp only [coeff_hsum, smulFamily_toFun, coeff_C, powers_toFun, ite_smul, zero_smul]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
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
g : Γ
⊢ Eq.{u_3 + 1} (α := R) (∑ᶠ (i : ℕ), (if i = 0 then r • (if 0 < x.orderTop then x else 0) ^ i else 0).coeff g)
    (HahnSeries.coeff ((algebraMap R R⟦Γ⟧ : (a : R) → R⟦Γ⟧) r) g)
have coeff : (if Eq (α := ℕ) 0 0 then r • HPow.hPow (β := ℕ) (if 0 < x.orderTop then x else 0) 0 else 0).coeff g =
  HahnSeries.coeff ((algebraMap R R⟦Γ⟧ : (a : R) → R⟦Γ⟧) r) g
Tactic: rw [finsum_eq_single _ 0 fun n hn => by simp [hn]]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
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
g : Γ
⊢ (if Eq (α := ℕ) 0 0 then r • HPow.hPow (β := ℕ) (if 0 < x.orderTop then x else 0) 0 else 0).coeff g =
    HahnSeries.coeff ((algebraMap R R⟦Γ⟧ : (a : R) → R⟦Γ⟧) r) g
have pos : ∀ (hg : g = 0),
  (if Eq (α := ℕ) 0 0 then r • HPow.hPow (β := ℕ) (if 0 < x.orderTop then x else 0) 0 else 0).coeff g =
    HahnSeries.coeff ((algebraMap R R⟦Γ⟧ : (a : R) → R⟦Γ⟧) r) g
Tactic: by_cases hg : g = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
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
g : Γ
pos :
  ∀ (hg : g = 0),
    (if Eq (α := ℕ) 0 0 then r • HPow.hPow (β := ℕ) (if 0 < x.orderTop then x else 0) 0 else 0).coeff g =
      HahnSeries.coeff ((algebraMap R R⟦Γ⟧ : (a : R) → R⟦Γ⟧) r) g
⊢ (if Eq (α := ℕ) 0 0 then r • HPow.hPow (β := ℕ) (if 0 < x.orderTop then x else 0) 0 else 0).coeff g =
    HahnSeries.coeff ((algebraMap R R⟦Γ⟧ : (a : R) → R⟦Γ⟧) r) g
have neg : ∀ (hg : ¬g = 0),
  (if Eq (α := ℕ) 0 0 then r • HPow.hPow (β := ℕ) (if 0 < x.orderTop then x else 0) 0 else 0).coeff g =
    HahnSeries.coeff ((algebraMap R R⟦Γ⟧ : (a : R) → R⟦Γ⟧) r) g
Tactic: by_cases hg : g = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
r : R
⊢ (heval x : (a : R⟦X⟧) → R⟦Γ⟧) ((C : (a : R) → R⟦X⟧) r) = HSMul.hSMul (β := R⟦Γ⟧) r 1
have coeff : ∀ (g : Γ),
  HahnSeries.coeff ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) ((C : (a : R) → R⟦X⟧) r)) g = (HSMul.hSMul (β := R⟦Γ⟧) r 1).coeff g
Tactic: ext g
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
r : R
g : Γ
⊢ HahnSeries.coeff ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) ((C : (a : R) → R⟦X⟧) r)) g = (HSMul.hSMul (β := R⟦Γ⟧) r 1).coeff g
have coeff : ∑ᶠ (i : ℕ),
    HMul.hMul (α := R) ((coeff i : (a : R⟦X⟧) → R) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) : R)
      (((if 0 < x.orderTop then x else 0) ^ i).coeff g) =
  if g = 0 then r else 0
Tactic: simp only [heval_apply, coeff_hsum, smulFamily_toFun, powers_toFun, HahnSeries.coeff_smul,
    HahnSeries.coeff_one, smul_eq_mul, mul_ite, mul_one, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
r : R
g : Γ
⊢ ∑ᶠ (i : ℕ),
      HMul.hMul (α := R) ((coeff i : (a : R⟦X⟧) → R) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) : R)
        (((if 0 < x.orderTop then x else 0) ^ i).coeff g) =
    if g = 0 then r else 0
have coeff : HMul.hMul (α := R) ((coeff 0 : (a : R⟦X⟧) → R) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) : R)
    ((HPow.hPow (β := ℕ) (if 0 < x.orderTop then x else 0) 0).coeff g) =
  if g = 0 then r else 0
Tactic: rw [finsum_eq_single _ 0 (fun n hn ↦ by simp [coeff_C_of_ne_zero hn])]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
r : R
g : Γ
⊢ HMul.hMul (α := R) ((coeff 0 : (a : R⟦X⟧) → R) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) : R)
      ((HPow.hPow (β := ℕ) (if 0 < x.orderTop then x else 0) 0).coeff g) =
    if g = 0 then r else 0
have pos : ∀ (hg : g = 0),
  HMul.hMul (α := R) ((coeff 0 : (a : R⟦X⟧) → R) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) : R)
      ((HPow.hPow (β := ℕ) (if 0 < x.orderTop then x else 0) 0).coeff g) =
    if g = 0 then r else 0
Tactic: by_cases hg : g = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
r : R
g : Γ
pos :
  ∀ (hg : g = 0),
    HMul.hMul (α := R) ((coeff 0 : (a : R⟦X⟧) → R) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) : R)
        ((HPow.hPow (β := ℕ) (if 0 < x.orderTop then x else 0) 0).coeff g) =
      if g = 0 then r else 0
⊢ HMul.hMul (α := R) ((coeff 0 : (a : R⟦X⟧) → R) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) : R)
      ((HPow.hPow (β := ℕ) (if 0 < x.orderTop then x else 0) 0).coeff g) =
    if g = 0 then r else 0
have neg : ∀ (hg : ¬g = 0),
  HMul.hMul (α := R) ((coeff 0 : (a : R⟦X⟧) → R) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) : R)
      ((HPow.hPow (β := ℕ) (if 0 < x.orderTop then x else 0) 0).coeff g) =
    if g = 0 then r else 0
Tactic: by_cases hg : g = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
⊢ (heval x : (a : R⟦X⟧) → R⟦Γ⟧) X = x
have rw : {
      toFun := fun (a : ℕ) ↦
        HSMul.hSMul (α := R) (β := R⟦Γ⟧) ((coeff a : (a : R⟦X⟧) → R) (mk fun (m : ℕ) ↦ if m = 1 then 1 else 0) : R)
          ((powers x : (a : ℕ) → R⟦Γ⟧) a : R⟦Γ⟧),
      isPWO_iUnion_support' := sorry, finite_co_support' := sorry : SummableFamily Γ R ℕ }.hsum =
  x
Tactic: rw [X_eq, monomial_eq_mk, heval_apply, powerSeriesFamily, smulFamily]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
⊢ {
        toFun := fun (a : ℕ) ↦
          HSMul.hSMul (α := R) (β := R⟦Γ⟧) ((coeff a : (a : R⟦X⟧) → R) (mk fun (m : ℕ) ↦ if m = 1 then 1 else 0) : R)
            ((powers x : (a : ℕ) → R⟦Γ⟧) a : R⟦Γ⟧),
        isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ : SummableFamily Γ R ℕ }.hsum =
    x
have simp : hsum (α := ℕ)
    { toFun := fun (a : ℕ) ↦ if a = 1 then x ^ a else 0, isPWO_iUnion_support' := sorry, finite_co_support' := sorry } =
  x
Tactic: simp only [coeff_mk, powers_toFun, hx, ↓reduceIte, ite_smul, one_smul, zero_smul]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
⊢ hsum (α := ℕ)
      { toFun := fun (a : ℕ) ↦ if a = 1 then x ^ a else 0, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ } =
    x
have coeff : ∀ (g : Γ),
  HahnSeries.coeff
      (hsum (α := ℕ)
        { toFun := fun (a : ℕ) ↦ if a = 1 then x ^ a else 0, isPWO_iUnion_support' := sorry, finite_co_support' := sorry })
      g =
    x.coeff g
Tactic: ext g
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
⊢ HahnSeries.coeff
      (hsum (α := ℕ)
        { toFun := fun (a : ℕ) ↦ if a = 1 then x ^ a else 0, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ })
      g =
    x.coeff g
have coeff : HahnSeries.coeff
    (({ toFun := fun (a : ℕ) ↦ if a = 1 then x ^ a else 0, isPWO_iUnion_support' := sorry, finite_co_support' := sorry } :
        (a : ℕ) → R⟦Γ⟧)
      1)
    g =
  x.coeff g
Tactic: rw [coeff_hsum, finsum_eq_single _ 1 (fun n hn ↦ by simp [hn])]