awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
g : Γ
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)
⊢ (powerSeriesFamily (R := R) x ((C : (a : R) → R⟦X⟧) r)).hsum.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]

Premises used: zero_smul, HahnSeries.SummableFamily.smulFamily_toFun, PowerSeries.coeff_C, HahnSeries.SummableFamily.coeff_hsum, HahnSeries.SummableFamily.powers_toFun, ite_smul
-- 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
g : Γ
n : ℕ
hn : n ≠ 0
⊢ (if n = 0 then r • (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⟦Γ⟧
r : R
g : Γ
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
⊢ 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:
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⟦Γ⟧
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
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
⊢ (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
-- 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
g : Γ
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:
simp [hg, Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_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⟦Γ⟧
r : R
g : Γ
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:
simp [hg, Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
a b : R⟦X⟧
⊢ (heval x : (a : R⟦X⟧) → R⟦Γ⟧) (a * b) =
    HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) a : R⟦Γ⟧) ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) b : R⟦Γ⟧)

Tactic:
map_mul (heval x) a b

Premises used: map_mul, PowerSeries.heval
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
r : R
coeff :
  ∀ (g : Γ),
    HahnSeries.coeff ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) ((C : (a : R) → R⟦X⟧) r)) g = (HSMul.hSMul (β := R⟦Γ⟧) r 1).coeff g
⊢ (heval x : (a : R⟦X⟧) → R⟦Γ⟧) ((C : (a : R) → R⟦X⟧) r) = HSMul.hSMul (β := R⟦Γ⟧) r 1

Tactic:
ext g
-- Module: Mathlib.RingTheory.HahnSeries.HEval
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 : Γ
coeff :
  ∑ᶠ (i : ℕ),
      HMul.hMul (α := R) ((PowerSeries.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
⊢ HahnSeries.coeff ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) ((C : (a : R) → R⟦X⟧) r)) g = (HSMul.hSMul (β := R⟦Γ⟧) r 1).coeff g

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]

Premises used: HahnSeries.coeff_smul, PowerSeries.heval_apply, mul_ite, MulZeroClass.mul_zero, HahnSeries.coeff_one, HahnSeries.SummableFamily.smulFamily_toFun, HahnSeries.SummableFamily.coeff_hsum, HahnSeries.SummableFamily.powers_toFun, smul_eq_mul, mul_one
-- Module: Mathlib.RingTheory.HahnSeries.HEval
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 : Γ
n : ℕ
hn : n ≠ 0
⊢ HMul.hMul (α := R) ((coeff n : (a : R⟦X⟧) → R) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) : R)
      (((if 0 < x.orderTop then x else 0) ^ n).coeff g) =
    0

Tactic:
simp [coeff_C_of_ne_zero hn]

Premises used: PowerSeries.coeff_C_of_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.HEval
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 : Γ
coeff :
  HMul.hMul (α := R) ((PowerSeries.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
⊢ ∑ᶠ (i : ℕ),
      HMul.hMul (α := R) ((PowerSeries.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:
rw [finsum_eq_single _ 0 (fun n hn ↦ by simp [coeff_C_of_ne_zero hn])]

Premises used: OfNat.ofNat, finsum_eq_single
-- Module: Mathlib.RingTheory.HahnSeries.HEval
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
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
⊢ 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
-- Module: Mathlib.RingTheory.HahnSeries.HEval
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 : Γ
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:
simp
-- Module: Mathlib.RingTheory.HahnSeries.HEval
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 : Γ
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:
simp
-- Module: Mathlib.RingTheory.HahnSeries.HEval
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
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' := ⋯, finite_co_support' := ⋯ : SummableFamily Γ R ℕ }.hsum =
    x
⊢ (heval x : (a : R⟦X⟧) → R⟦Γ⟧) X = x

Tactic:
rw [X_eq, monomial_eq_mk, heval_apply, powerSeriesFamily, smulFamily]

Premises used: PowerSeries.heval_apply, HahnSeries.SummableFamily.powerSeriesFamily, PowerSeries.monomial_eq_mk, PowerSeries.X_eq, HahnSeries.SummableFamily.smulFamily
-- Module: Mathlib.RingTheory.HahnSeries.HEval
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
simp :
  hsum (α := ℕ)
      { toFun := fun (a : ℕ) ↦ if a = 1 then x ^ a else 0, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ } =
    x
⊢ {
        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

Tactic:
simp only [coeff_mk, powers_toFun, hx, ↓reduceIte, ite_smul, one_smul, zero_smul]

Premises used: PowerSeries.coeff_mk, one_smul, zero_smul, HahnSeries.SummableFamily.powers_toFun, reduceIte, ite_smul
-- Module: Mathlib.RingTheory.HahnSeries.HEval
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
coeff :
  ∀ (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
⊢ hsum (α := ℕ)
      { toFun := fun (a : ℕ) ↦ if a = 1 then x ^ a else 0, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ } =
    x

Tactic:
ext g
-- Module: Mathlib.RingTheory.HahnSeries.HEval
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 : Γ
n : ℕ
hn : n ≠ 1
⊢ Eq.{u_3 + 1} (α := R)
    (HahnSeries.coeff
      (({ toFun := fun (a : ℕ) ↦ if a = 1 then x ^ a else 0, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ } :
          (a : ℕ) → R⟦Γ⟧)
        n)
      g)
    0

Tactic:
simp [hn]
-- Module: Mathlib.RingTheory.HahnSeries.HEval
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 : Γ
coeff :
  HahnSeries.coeff
      (({ toFun := fun (a : ℕ) ↦ if a = 1 then x ^ a else 0, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ } :
          (a : ℕ) → R⟦Γ⟧)
        1)
      g =
    x.coeff 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

Tactic:
rw [coeff_hsum, finsum_eq_single _ 1 (fun n hn ↦ by simp [hn])]

Premises used: HahnSeries.SummableFamily.coeff_hsum, OfNat.ofNat, finsum_eq_single
-- Module: Mathlib.RingTheory.HahnSeries.HEval
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
      (({ toFun := fun (a : ℕ) ↦ if a = 1 then x ^ a else 0, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ } :
          (a : ℕ) → R⟦Γ⟧)
        1)
      g =
    x.coeff g

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
u : R⟦X⟧ˣ
⊢ IsUnit (M := R⟦Γ⟧) ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) (↑u : R⟦X⟧) : R⟦Γ⟧)

Tactic:
isUnit_iff_exists_inv.mpr ?_

Premises used: Iff.mpr, isUnit_iff_exists_inv
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
u : R⟦X⟧ˣ
refine : ∃ (b : R⟦Γ⟧), HMul.hMul (α := R⟦Γ⟧) ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) (↑u : R⟦X⟧) : R⟦Γ⟧) b = 1
⊢ IsUnit (M := R⟦Γ⟧) ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) (↑u : R⟦X⟧) : R⟦Γ⟧)

Tactic:
refine isUnit_iff_exists_inv.mpr ?_

Premises used: Iff.mpr, isUnit_iff_exists_inv
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
u : R⟦X⟧ˣ
h :
  HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) (↑u : R⟦X⟧) : R⟦Γ⟧)
      ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) u.inv : R⟦Γ⟧) =
    1
⊢ ∃ (b : R⟦Γ⟧), HMul.hMul (α := R⟦Γ⟧) ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) (↑u : R⟦X⟧) : R⟦Γ⟧) b = 1

Tactic:
use heval x u.inv

Premises used: PowerSeries.heval, Units.inv, DFunLike.coe
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
u : R⟦X⟧ˣ
h : Eq (α := R⟦Γ⟧) ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) ((↑u : R⟦X⟧) * u.inv) : R⟦Γ⟧) (1 : R⟦Γ⟧)
h₁ : Eq (α := R⟦Γ⟧) ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) 1) 1
h₂ h₃ : Eq (α := R⟦Γ⟧) 1 1
⊢ HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) (↑u : R⟦X⟧) : R⟦Γ⟧)
      ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) u.inv : R⟦Γ⟧) =
    1

Tactic:
rw [← heval_mul, Units.val_inv, map_one]

Premises used: map_one, Units.val_inv, PowerSeries.heval_mul
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
g : Γ
⊢ Eq.{u_3 + 1} (α := R) (∑ᶠ (i : ℕ), HahnSeries.coeff ((powerSeriesFamily x f : (a : ℕ) → R⟦Γ⟧) i) g)
    (∑ᶠ (n : ℕ), ((powerSeriesFamily x f).coeff g : (a : ℕ) → R) n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
g : Γ
⊢ Eq.{u_3 + 1} (α := R) (∑ᶠ (i : ℕ), HahnSeries.coeff ((powerSeriesFamily x f : (a : ℕ) → R⟦Γ⟧) i) g)
    (∑ᶠ (n : ℕ), ((powerSeriesFamily x f).coeff g : (a : ℕ) → R) n)

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
rw : Eq (α := R) (((powerSeriesFamily x f).coeff 0 : (a : ℕ) → R) 0 : R) ((coeff 0 : (a : R⟦X⟧) → R) f : R)
rw₁ : ∀ (x_1 : ℕ), x_1 ≠ 0 → Eq (α := R) (((powerSeriesFamily x f).coeff 0 : (a : ℕ) → R) x_1 : R) (0 : R)
⊢ Eq (α := R) (HahnSeries.coeff.{u_1, u_3} (Γ := Γ) ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) f) 0 : R)
    ((constantCoeff : (a : R⟦X⟧) → R) f : R)

Tactic:
rw [coeff_heval, finsum_eq_single (fun n => ((powerSeriesFamily x f).coeff 0) n) 0,
    ← PowerSeries.coeff_zero_eq_constantCoeff_apply]

Premises used: PowerSeries.coeff_heval, HahnSeries.SummableFamily.powerSeriesFamily, HahnSeries.SummableFamily.coeff, PowerSeries.coeff_zero_eq_constantCoeff_apply, OfNat.ofNat, DFunLike.coe, finsum_eq_single
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
⊢ Eq (α := R) (((powerSeriesFamily x f).coeff 0 : (a : ℕ) → R) 0 : R) ((coeff 0 : (a : R⟦X⟧) → R) f : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
n : ℕ
hn : n ≠ 0
simp :
  HMul.hMul (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) f : R)
      (HahnSeries.coeff.{u_1, u_3} (Γ := Γ) ((powers x : (a : ℕ) → R⟦Γ⟧) n) 0 : R) =
    0
⊢ Eq (α := R) (((powerSeriesFamily x f).coeff 0 : (a : ℕ) → R) n : R) (0 : R)

Tactic:
simp only [coeff_apply, smulFamily_toFun, HahnSeries.coeff_smul, smul_eq_mul]

Premises used: HahnSeries.coeff_smul, HahnSeries.SummableFamily.smulFamily_toFun, HahnSeries.SummableFamily.coeff_apply, smul_eq_mul
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
n : ℕ
hn : n ≠ 0
⊢ HMul.hMul (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) f : R)
      (HahnSeries.coeff.{u_1, u_3} (Γ := Γ) ((powers x : (a : ℕ) → R⟦Γ⟧) n) 0 : R) =
    0

Tactic:
mul_eq_zero_of_right (coeff n f) (coeff_eq_zero_of_lt_orderTop ?_)

Premises used: mul_eq_zero_of_right, PowerSeries.coeff, DFunLike.coe, HahnSeries.coeff_eq_zero_of_lt_orderTop
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
n : ℕ
hn : n ≠ 0
refine : LT.lt.{u_1} (α := WithTop Γ) (↑0 : WithTop Γ) (orderTop.{u_1, u_3} (R := R) ((powers x : (a : ℕ) → R⟦Γ⟧) n))
⊢ HMul.hMul (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) f : R)
      (HahnSeries.coeff.{u_1, u_3} (Γ := Γ) ((powers x : (a : ℕ) → R⟦Γ⟧) n) 0 : R) =
    0

Tactic:
refine mul_eq_zero_of_right (coeff n f) (coeff_eq_zero_of_lt_orderTop ?_)

Premises used: mul_eq_zero_of_right, PowerSeries.coeff, DFunLike.coe, HahnSeries.coeff_eq_zero_of_lt_orderTop
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
n : ℕ
hn : n ≠ 0
pos :
  ∀ (h : 0 < x.orderTop),
    LT.lt.{u_1} (α := WithTop Γ) (↑0 : WithTop Γ) (orderTop.{u_1, u_3} (R := R) ((powers x : (a : ℕ) → R⟦Γ⟧) n))
neg :
  ∀ (h : ¬0 < x.orderTop),
    LT.lt.{u_1} (α := WithTop Γ) (↑0 : WithTop Γ) (orderTop.{u_1, u_3} (R := R) ((powers x : (a : ℕ) → R⟦Γ⟧) n))
⊢ LT.lt.{u_1} (α := WithTop Γ) (↑0 : WithTop Γ) (orderTop.{u_1, u_3} (R := R) ((powers x : (a : ℕ) → R⟦Γ⟧) n))

Tactic:
by_cases h : 0 < x.orderTop

Premises used: HahnSeries.orderTop
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
n : ℕ
hn : n ≠ 0
h : 0 < x.orderTop
⊢ LT.lt.{u_1} (α := WithTop Γ) (↑0 : WithTop Γ) (orderTop.{u_1, u_3} (R := R) ((powers x : (a : ℕ) → R⟦Γ⟧) n))

Tactic:
(lt_of_lt_of_le ((nsmul_pos_iff hn).mpr h) ?_)

Premises used: Iff.mpr, nsmul_pos_iff, lt_of_lt_of_le
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
n : ℕ
hn : n ≠ 0
h : 0 < x.orderTop
pos : n • x.orderTop ≤ orderTop.{u_1, u_3} (R := R) ((powers x : (a : ℕ) → R⟦Γ⟧) n)
⊢ LT.lt.{u_1} (α := WithTop Γ) (↑0 : WithTop Γ) (orderTop.{u_1, u_3} (R := R) ((powers x : (a : ℕ) → R⟦Γ⟧) n))

Tactic:
refine (lt_of_lt_of_le ((nsmul_pos_iff hn).mpr h) ?_)

Premises used: Iff.mpr, nsmul_pos_iff, lt_of_lt_of_le
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
n : ℕ
hn : n ≠ 0
h : 0 < x.orderTop
⊢ n • x.orderTop ≤ orderTop.{u_1, u_3} (R := R) ((powers x : (a : ℕ) → R⟦Γ⟧) n)

Tactic:
simp [h, orderTop_nsmul_le_orderTop_pow]

Premises used: HahnSeries.orderTop_nsmul_le_orderTop_pow
-- Module: Mathlib.RingTheory.HahnSeries.HEval
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
n : ℕ
hn : n ≠ 0
h : ¬0 < x.orderTop
⊢ LT.lt.{u_1} (α := WithTop Γ) (↑0 : WithTop Γ) (orderTop.{u_1, u_3} (R := R) ((powers x : (a : ℕ) → R⟦Γ⟧) n))

Tactic:
simp [h, hn]
-- Module: Mathlib.RingTheory.HahnSeries.HahnEmbedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : Module ℚ M
inst_4 : IsOrderedModule ℚ M
⊢ Nonempty.{u_1 + 1} (HahnEmbedding.ArchimedeanStrata ℚ M)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.HahnSeries.HahnEmbedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : Module ℚ M
inst_4 : IsOrderedModule ℚ M
obtain : ∀ (strata : HahnEmbedding.ArchimedeanStrata ℚ M), Nonempty.{max 1 (u_1 + 1)} (HahnEmbedding.Seed ℚ M ℝ)
⊢ Nonempty.{max 1 (u_1 + 1)} (HahnEmbedding.Seed ℚ M ℝ)

Tactic:
obtain ⟨strata⟩ : Nonempty (HahnEmbedding.ArchimedeanStrata ℚ M) := inferInstance

Premises used: Rat, HahnEmbedding.ArchimedeanStrata, Nonempty
-- Module: Mathlib.RingTheory.HahnSeries.HahnEmbedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : Module ℚ M
inst_4 : IsOrderedModule ℚ M
strata : HahnEmbedding.ArchimedeanStrata ℚ M
choose :
  ∀ (f : (c : FiniteArchimedeanClass M) → ↥(strata.stratum c) →+o ℝ)
    (hf :
      ∀ (c : FiniteArchimedeanClass M),
        Function.Injective (α := ↥(strata.stratum c)) (β := ℝ) (⇑(f c) : (a : ↥(strata.stratum c)) → ℝ)),
    Nonempty.{max 1 (u_1 + 1)} (HahnEmbedding.Seed ℚ M ℝ)
⊢ Nonempty.{max 1 (u_1 + 1)} (HahnEmbedding.Seed ℚ M ℝ)

Tactic:
choose f hf using fun c ↦ Archimedean.exists_orderAddMonoidHom_real_injective (strata.stratum c)

Premises used: Membership.mem, Subtype, HahnEmbedding.ArchimedeanStrata.stratum, Archimedean.exists_orderAddMonoidHom_real_injective
-- Module: Mathlib.RingTheory.HahnSeries.HahnEmbedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : Module ℚ M
inst_4 : IsOrderedModule ℚ M
strata : HahnEmbedding.ArchimedeanStrata ℚ M
f : (c : FiniteArchimedeanClass M) → ↥(strata.stratum c) →+o ℝ
hf :
  ∀ (c : FiniteArchimedeanClass M),
    Function.Injective (α := ↥(strata.stratum c)) (β := ℝ) (⇑(f c) : (a : ↥(strata.stratum c)) → ℝ)
⊢ Nonempty.{max 1 (u_1 + 1)} (HahnEmbedding.Seed ℚ M ℝ)

Tactic:
⟨strata, fun c ↦ (f c).toRatLinearMap, fun c ↦ ?_⟩

Premises used: Nonempty.intro, HahnEmbedding.Seed.mk, AddMonoidHom.toRatLinearMap, OrderAddMonoidHom.toAddMonoidHom
-- Module: Mathlib.RingTheory.HahnSeries.HahnEmbedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : Module ℚ M
inst_4 : IsOrderedModule ℚ M
strata : HahnEmbedding.ArchimedeanStrata ℚ M
f : (c : FiniteArchimedeanClass M) → ↥(strata.stratum c) →+o ℝ
hf :
  ∀ (c : FiniteArchimedeanClass M),
    Function.Injective (α := ↥(strata.stratum c)) (β := ℝ) (⇑(f c) : (a : ↥(strata.stratum c)) → ℝ)
refine :
  ∀ (c : FiniteArchimedeanClass M),
    StrictMono.{u_1, 0} (α := ↥(strata.stratum c)) (β := ℝ)
      (⇑((fun (c : FiniteArchimedeanClass M) ↦ ((f c).toRatLinearMap : ↥(strata.stratum c) →ₗ[ℚ] ℝ)) c) :
        (a : ↥(strata.stratum c)) → ℝ)
⊢ Nonempty.{max 1 (u_1 + 1)} (HahnEmbedding.Seed ℚ M ℝ)

Tactic:
refine ⟨strata, fun c ↦ (f c).toRatLinearMap, fun c ↦ ?_⟩