awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
xy : ∀ (x_1 : Γ'), (embDomain f x).coeff x_1 = (embDomain f y).coeff x_1
g : Γ
⊢ (embDomain f x).coeff ((f : (a : Γ) → Γ') g) = (embDomain f y).coeff ((f : (a : Γ) → Γ') g)

Tactic:
have xyg := xy (f g)
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
xy : ∀ (x_1 : Γ'), (embDomain f x).coeff x_1 = (embDomain f y).coeff x_1
g : Γ
xyg : (embDomain f x).coeff ((f : (a : Γ) → Γ') g) = (embDomain f y).coeff ((f : (a : Γ) → Γ') g)
coeff : ∀ (xyg : x.coeff g = (embDomain f y).coeff ((f : (a : Γ) → Γ') g)), x.coeff g = y.coeff g
coeff₁ coeff₂ coeff₃ coeff₄ : ∀ (xyg : x.coeff g = y.coeff g), x.coeff g = y.coeff g
⊢ x.coeff g = y.coeff g

Tactic:
rwa [embDomain_coeff, embDomain_coeff] at xyg

Premises used: HahnSeries.embDomain_coeff
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ' : Type u_2
R : Type u_3
inst : Zero R
inst_1 : PartialOrder Γ'
Γ : Type u_5
inst_2 : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
inl :
  orderTop.{u_2, u_3} (R := R) (embDomain f 0) =
    WithTop.map.{u_5, u_2} (α := Γ) (⇑f : (a : Γ) → Γ') (orderTop.{u_5, u_3} (R := R) 0)
inr : ∀ (hx : x ≠ 0), (embDomain f x).orderTop = WithTop.map (⇑f : (a : Γ) → Γ') x.orderTop
⊢ (embDomain f x).orderTop = WithTop.map (⇑f : (a : Γ) → Γ') x.orderTop

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ' : Type u_2
R : Type u_3
inst : Zero R
inst_1 : PartialOrder Γ'
Γ : Type u_5
inst_2 : LinearOrder Γ
f : Γ ↪o Γ'
⊢ orderTop.{u_2, u_3} (R := R) (embDomain f 0) =
    WithTop.map.{u_5, u_2} (α := Γ) (⇑f : (a : Γ) → Γ') (orderTop.{u_5, u_3} (R := R) 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ' : Type u_2
R : Type u_3
inst : Zero R
inst_1 : PartialOrder Γ'
Γ : Type u_5
inst_2 : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
⊢ x.orderTop ≠ ⊤

Tactic:
simpa using hx
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ' : Type u_2
R : Type u_3
inst : Zero R
inst_1 : PartialOrder Γ'
Γ : Type u_5
inst_2 : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
inr : (embDomain f x).orderTop = (↑((f : (a : Γ) → Γ') (x.orderTop.untop ⋯)) : WithTop Γ')
⊢ (embDomain f x).orderTop = WithTop.map (⇑f : (a : Γ) → Γ') x.orderTop

Tactic:
rw [← WithTop.coe_untop x.orderTop (by simpa using hx), WithTop.map_coe]

Premises used: WithTop.coe_untop, HahnSeries.orderTop, WithTop.map_coe
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ' : Type u_2
R : Type u_3
inst : Zero R
inst_1 : PartialOrder Γ'
Γ : Type u_5
inst_2 : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
inr : Membership.mem (α := Γ') (embDomain f x).support ((f : (a : Γ) → Γ') (x.orderTop.untop ⋯) : Γ')
inr₁ : ∀ g' ∈ (embDomain f x).support, (f : (a : Γ) → Γ') (x.orderTop.untop ⋯) ≤ g'
⊢ (embDomain f x).orderTop = (↑((f : (a : Γ) → Γ') (x.orderTop.untop ⋯)) : WithTop Γ')

Tactic:
apply orderTop_eq_of_le

Premises used: HahnSeries.orderTop_eq_of_le
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ' : Type u_2
R : Type u_3
inst : Zero R
inst_1 : PartialOrder Γ'
Γ : Type u_5
inst_2 : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
⊢ x.orderTop = (↑(x.orderTop.untop ⋯) : WithTop Γ)

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ' : Type u_2
R : Type u_3
inst : Zero R
inst_1 : PartialOrder Γ'
Γ : Type u_5
inst_2 : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
⊢ Membership.mem (α := Γ') (embDomain f x).support ((f : (a : Γ) → Γ') (x.orderTop.untop ⋯) : Γ')

Tactic:
simpa using coeff_orderTop_ne (by simp)

Premises used: HahnSeries.coeff_orderTop_ne
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ' : Type u_2
R : Type u_3
inst : Zero R
inst_1 : PartialOrder Γ'
Γ : Type u_5
inst_2 : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
y : Γ'
hy : y ∈ (embDomain f x).support
inr :
  ∀ (z : Γ) (hz : z ∈ x.support) (hy : Membership.mem (α := Γ') (embDomain f x).support ((f : (a : Γ) → Γ') z : Γ')),
    LE.le.{u_2} (α := Γ') ((f : (a : Γ) → Γ') (x.orderTop.untop ⋯) : Γ') ((f : (a : Γ) → Γ') z : Γ')
⊢ (f : (a : Γ) → Γ') (x.orderTop.untop ⋯) ≤ y

Tactic:
obtain ⟨z, hz, rfl⟩ :=
    (Set.mem_image _ _ _).mp <| Set.mem_of_subset_of_mem support_embDomain_subset hy

Premises used: Set.mem_of_subset_of_mem, Set.mem_image, Iff.mp, HahnSeries.support_embDomain_subset, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ' : Type u_2
R : Type u_3
inst : Zero R
inst_1 : PartialOrder Γ'
Γ : Type u_5
inst_2 : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
z : Γ
hz : z ∈ x.support
hy : Membership.mem (α := Γ') (embDomain f x).support ((f : (a : Γ) → Γ') z : Γ')
inr : x.orderTop ≤ (↑z : WithTop Γ)
⊢ LE.le.{u_2} (α := Γ') ((f : (a : Γ) → Γ') (x.orderTop.untop ⋯) : Γ') ((f : (a : Γ) → Γ') z : Γ')

Tactic:
rw [OrderEmbedding.le_iff_le, WithTop.untop_le_iff]

Premises used: WithTop.untop_le_iff, OrderEmbedding.le_iff_le
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ' : Type u_2
R : Type u_3
inst : Zero R
inst_1 : PartialOrder Γ'
Γ : Type u_5
inst_2 : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
z : Γ
hz : z ∈ x.support
hy : Membership.mem (α := Γ') (embDomain f x).support ((f : (a : Γ) → Γ') z : Γ')
inr : x.coeff z ≠ 0
⊢ x.orderTop ≤ (↑z : WithTop Γ)

Tactic:
apply orderTop_le_of_coeff_ne_zero

Premises used: HahnSeries.orderTop_le_of_coeff_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ' : Type u_2
R : Type u_3
inst : Zero R
inst_1 : PartialOrder Γ'
Γ : Type u_5
inst_2 : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
z : Γ
hz : z ∈ x.support
hy : Membership.mem (α := Γ') (embDomain f x).support ((f : (a : Γ) → Γ') z : Γ')
⊢ x.coeff z ≠ 0

Tactic:
simpa using hz
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
f : Γ → R
n : Γ
hn : ∀ m < n, f m = 0
⊢ BddBelow (Function.support f)

Tactic:
⟨n, fun _ ↦ ?_⟩

Premises used: Set.Nonempty, BddBelow, Exists.intro
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
f : Γ → R
n : Γ
hn : ∀ m < n, f m = 0
refine : ∀ x ∈ Function.support f, n ≤ x
⊢ BddBelow (Function.support f)

Tactic:
refine ⟨n, fun _ ↦ ?_⟩
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
f : Γ → R
n : Γ
hn : ∀ m < n, f m = 0
x : Γ
contrapose : ¬n ≤ x → x ∉ Function.support f
⊢ x ∈ Function.support f → n ≤ x

Tactic:
contrapose
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
f : Γ → R
n : Γ
hn : ∀ m < n, f m = 0
x : Γ
⊢ ¬n ≤ x → x ∉ Function.support f

Tactic:
simp_all
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
inst_2 : Nonempty Γ
⊢ BddBelow.{u_1} (α := Γ) (Function.support.{u_1, u_3} (M := R) 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
x : R⟦Γ⟧
i : WithTop Γ
H : ∀ (j : Γ), (↑j : WithTop Γ) < i → x.coeff j = 0
inl : ∀ (H : ∀ (j : Γ), (↑j : WithTop Γ) < i → Eq.{u_3 + 1} (α := R) (coeff 0 j) 0), i ≤ orderTop.{u_1, u_3} (R := R) 0
inr : ∀ (h : x ≠ 0), i ≤ x.orderTop
⊢ i ≤ x.orderTop

Tactic:
obtain rfl | h := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
i : WithTop Γ
H : ∀ (j : Γ), (↑j : WithTop Γ) < i → Eq.{u_3 + 1} (α := R) (coeff 0 j) 0
⊢ i ≤ orderTop.{u_1, u_3} (R := R) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
x : R⟦Γ⟧
i : WithTop Γ
H : ∀ (j : Γ), (↑j : WithTop Γ) < i → x.coeff j = 0
h : x ≠ 0
inr : ∀ (hi : x.orderTop < i), False
⊢ i ≤ x.orderTop

Tactic:
by_contra! hi
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
x : R⟦Γ⟧
i : WithTop Γ
H : ∀ (j : Γ), (↑j : WithTop Γ) < i → x.coeff j = 0
h : x ≠ 0
hi : x.orderTop < i
⊢ False

Tactic:
x.isWF_support.min_mem (support_nonempty_iff.2 h) (H _ (orderTop_of_ne_zero h ▸ hi))

Premises used: Iff.mpr, Set.IsWF.min_mem, Eq.rec, HahnSeries.support_nonempty_iff, HahnSeries.orderTop_of_ne_zero, HahnSeries.isWF_support
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
x : R⟦Γ⟧
i : WithTop Γ
H : ∀ (j : Γ), (↑j : WithTop Γ) < i → x.coeff j = 0
h : x ≠ 0
hi : x.orderTop < i
⊢ False

Tactic:
exact x.isWF_support.min_mem (support_nonempty_iff.2 h) (H _ (orderTop_of_ne_zero h ▸ hi))

Premises used: Iff.mpr, Set.IsWF.min_mem, Eq.rec, HahnSeries.support_nonempty_iff, HahnSeries.orderTop_of_ne_zero, HahnSeries.isWF_support
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
x : R⟦Γ⟧
i : WithTop Γ
rw : (¬∀ (j : Γ), (↑j : WithTop Γ) < i → x.coeff j = 0) ↔ ∃ (j : Γ), (↑j : WithTop Γ) < i ∧ x.coeff j ≠ 0
⊢ x.orderTop < i ↔ ∃ (j : Γ), (↑j : WithTop Γ) < i ∧ x.coeff j ≠ 0

Tactic:
rw [← not_le, le_orderTop_iff_forall]

Premises used: not_le, HahnSeries.le_orderTop_iff_forall
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
x : R⟦Γ⟧
i : WithTop Γ
⊢ (¬∀ (j : Γ), (↑j : WithTop Γ) < i → x.coeff j = 0) ↔ ∃ (j : Γ), (↑j : WithTop Γ) < i ∧ x.coeff j ≠ 0

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
inst_2 : Zero Γ
x : R⟦Γ⟧
i : Γ
h : x ≠ 0
H : ∀ j < i, x.coeff j = 0
contrapose! : ∀ (h : x.order < i), x = 0
⊢ i ≤ x.order

Tactic:
contrapose! h
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
inst_2 : Zero Γ
x : R⟦Γ⟧
i : Γ
H : ∀ j < i, x.coeff j = 0
h : x.order < i
⊢ x.coeff x.order = 0

Tactic:
have := H _ h
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
inst_2 : Zero Γ
x : R⟦Γ⟧
i : Γ
H : ∀ j < i, x.coeff j = 0
h : x.order < i
this : x.coeff x.order = 0
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : x = 0), x = 0
⊢ x = 0

Tactic:
rwa [coeff_order_eq_zero] at this

Premises used: HahnSeries.coeff_order_eq_zero
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
inst_2 : Zero Γ
x : R⟦Γ⟧
i : Γ
h : x ≠ 0
rw : (¬∀ j < i, x.coeff j = 0) ↔ ∃ j < i, x.coeff j ≠ 0
⊢ x.order < i ↔ ∃ j < i, x.coeff j ≠ 0

Tactic:
rw [← not_le, le_order_iff_forall h]

Premises used: not_le, HahnSeries.le_order_iff_forall
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
inst_2 : Zero Γ
x : R⟦Γ⟧
i : Γ
h : x ≠ 0
⊢ (¬∀ j < i, x.coeff j = 0) ↔ ∃ j < i, x.coeff j ≠ 0

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
inst_2 : LocallyFiniteOrder Γ
f : Γ → R
hf : BddBelow (Function.support f)
⊢ (Function.support f).IsPWO

Tactic:
hf.isWF.isPWO

Premises used: Set.IsWF.isPWO, BddBelow.isWF
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : Zero R
inst_1 : LinearOrder Γ
inst_2 : LocallyFiniteOrder Γ
inst_3 : Nonempty Γ
⊢ BddBelow.{u_1} (α := Γ) (Function.support.{u_1, u_3} (M := R) 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
inst_2 : LocallyFiniteOrder Γ
inst_3 : Nonempty Γ
⊢ Eq (α := R⟦Γ⟧) (ofSuppBddBelow 0 ⋯) 0

Tactic:
rfl

Premises used: HahnSeries.ofSuppBddBelow, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
inst_2 : LocallyFiniteOrder Γ
f : Γ → R
hf : BddBelow (Function.support f)
⊢ ofSuppBddBelow f hf = 0 ↔ f = 0

Tactic:
HahnSeries.ext_iff

Premises used: HahnSeries.ext_iff
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
inst_2 : LocallyFiniteOrder Γ
f : Γ → R
hf : BddBelow (Function.support f)
⊢ (ofSuppBddBelow f hf).coeff = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
inst_2 : LocallyFiniteOrder Γ
inst_3 : Zero Γ
f : Γ → R
hf : f ≠ 0
n : Γ
hn : ∀ m < n, f m = 0
rw : ∀ j < n, (ofSuppBddBelow f ⋯).coeff j = 0
rw₁ : ofSuppBddBelow f ⋯ ≠ 0
⊢ n ≤ (ofSuppBddBelow f ⋯).order

Tactic:
rw [le_order_iff_forall]

Premises used: HahnSeries.le_order_iff_forall
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
inst_2 : LocallyFiniteOrder Γ
inst_3 : Zero Γ
f : Γ → R
hf : f ≠ 0
n : Γ
hn : ∀ m < n, f m = 0
⊢ ∀ j < n, (ofSuppBddBelow f ⋯).coeff j = 0

Tactic:
hn
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
inst_2 : LocallyFiniteOrder Γ
inst_3 : Zero Γ
f : Γ → R
hf : f ≠ 0
n : Γ
hn : ∀ m < n, f m = 0
⊢ ∀ j < n, (ofSuppBddBelow f ⋯).coeff j = 0

Tactic:
exact hn
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
inst_2 : LocallyFiniteOrder Γ
inst_3 : Zero Γ
f : Γ → R
hf : f ≠ 0
n : Γ
hn : ∀ m < n, f m = 0
⊢ ofSuppBddBelow f ⋯ ≠ 0

Tactic:
simpa
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : Zero R
inst_1 : PartialOrder Γ
inst_2 : DecidableLT Γ
c : Γ
x : R⟦Γ⟧
⊢ (Function.support.{u_1, u_3} (M := R) fun (i : Γ) ↦ if i < c then x.coeff i else 0) ⊆ x.support

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : Zero R
inst_1 : PartialOrder Γ
inst_2 : DecidableLT Γ
c : Γ
coeff :
  ∀ (x : Γ),
    Eq.{u_3 + 1} (α := R)
      (HahnSeries.coeff { coeff := fun (i : Γ) ↦ if i < c then HahnSeries.coeff 0 i else 0, isPWO_support' := ⋯ } x)
      (HahnSeries.coeff 0 x)
⊢ Eq (α := R⟦Γ⟧) { coeff := fun (i : Γ) ↦ if i < c then HahnSeries.coeff 0 i else 0, isPWO_support' := ⋯ } 0

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : Zero R
inst_1 : PartialOrder Γ
inst_2 : DecidableLT Γ
c x : Γ
⊢ Eq.{u_3 + 1} (α := R) (coeff { coeff := fun (i : Γ) ↦ if i < c then coeff 0 i else 0, isPWO_support' := ⋯ } x)
    (coeff 0 x)

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : PartialOrder Γ
inst_2 : DecidableLT Γ
c : Γ
x : R⟦Γ⟧
⊢ Eq.{u_1 + 1} (α := Set Γ) (support.{u_1, u_3} (R := R) ((truncLT c : (a : R⟦Γ⟧) → R⟦Γ⟧) x))
    {y : Γ | y ∈ x.support ∧ y < c}

Tactic:
simp [truncLT, Function.support, and_comm]

Premises used: and_comm, HahnSeries.truncLT, Function.support
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : PartialOrder Γ
inst_2 : DecidableLT Γ
c : Γ
x : R⟦Γ⟧
rw : {y : Γ | y ∈ x.support ∧ y < c} ⊆ x.support
⊢ support.{u_1, u_3} (R := R) ((truncLT c : (a : R⟦Γ⟧) → R⟦Γ⟧) x) ⊆ x.support

Tactic:
rw [support_truncLT]

Premises used: HahnSeries.support_truncLT
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : PartialOrder Γ
inst_2 : DecidableLT Γ
c : Γ
x : R⟦Γ⟧
⊢ {y : Γ | y ∈ x.support ∧ y < c} ⊆ x.support

Tactic:
Set.sep_subset ..

Premises used: Set.sep_subset
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : PartialOrder Γ
inst_2 : DecidableLT Γ
c : Γ
x : R⟦Γ⟧
⊢ {y : Γ | y ∈ x.support ∧ y < c} ⊆ x.support

Tactic:
exact Set.sep_subset ..

Premises used: Set.sep_subset
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : PartialOrder Γ
inst_2 : DecidableLT Γ
c : Γ
x : R⟦Γ⟧
i : Γ
⊢ coeff ((truncLT c : (a : R⟦Γ⟧) → R⟦Γ⟧) x) i = if i < c then x.coeff i else 0

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : PartialOrder Γ
inst_2 : DecidableLT Γ
c i : Γ
h : i < c
x : R⟦Γ⟧
⊢ coeff ((truncLT c : (a : R⟦Γ⟧) → R⟦Γ⟧) x) i = x.coeff i

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
c i : Γ
h : c ≤ i
x : R⟦Γ⟧
⊢ Eq.{u_3 + 1} (α := R) (coeff ((truncLT c : (a : R⟦Γ⟧) → R⟦Γ⟧) x) i) 0

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
Goal:
Γ : Type u_1
R : Type u_2
A : Type u_3
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
inst_5 : CommRing A
inst_6 : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
n : ℕ
⊢ (binomialFamily x r : (a : ℕ) → A⟦Γ⟧) n = Ring.choose r n • (x - 1) ^ n

Tactic:
simp [hx, binomialFamily]

Premises used: HahnSeries.SummableFamily.binomialFamily
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
Goal:
Γ : Type u_1
R : Type u_2
A : Type u_3
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
inst_5 : CommRing A
inst_6 : Algebra R A
x : A⟦Γ⟧
hx : ¬0 < (x - 1).orderTop
r : R
n : ℕ
rw : (powerSeriesFamily 0 (PowerSeries.binomialSeries A r) : (a : ℕ) → A⟦Γ⟧) n = HPow.hPow (α := A⟦Γ⟧) 0 n
⊢ (binomialFamily x r : (a : ℕ) → A⟦Γ⟧) n = HPow.hPow (α := A⟦Γ⟧) 0 n

Tactic:
rw [binomialFamily, powerSeriesFamily_of_not_orderTop_pos hx]

Premises used: HahnSeries.SummableFamily.powerSeriesFamily_of_not_orderTop_pos, HahnSeries.SummableFamily.binomialFamily
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
Goal:
Γ : Type u_1
R : Type u_2
A : Type u_3
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
inst_5 : CommRing A
inst_6 : Algebra R A
x : A⟦Γ⟧
hx : ¬0 < (x - 1).orderTop
r : R
n : ℕ
pos :
  ∀ (hn : n = 0), (powerSeriesFamily 0 (PowerSeries.binomialSeries A r) : (a : ℕ) → A⟦Γ⟧) n = HPow.hPow (α := A⟦Γ⟧) 0 n
neg :
  ∀ (hn : ¬n = 0), (powerSeriesFamily 0 (PowerSeries.binomialSeries A r) : (a : ℕ) → A⟦Γ⟧) n = HPow.hPow (α := A⟦Γ⟧) 0 n
⊢ (powerSeriesFamily 0 (PowerSeries.binomialSeries A r) : (a : ℕ) → A⟦Γ⟧) n = HPow.hPow (α := A⟦Γ⟧) 0 n

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
Goal:
Γ : Type u_1
R : Type u_2
A : Type u_3
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
inst_5 : CommRing A
inst_6 : Algebra R A
x : A⟦Γ⟧
hx : ¬0 < (x - 1).orderTop
r : R
n : ℕ
hn : n = 0
⊢ (powerSeriesFamily 0 (PowerSeries.binomialSeries A r) : (a : ℕ) → A⟦Γ⟧) n = HPow.hPow (α := A⟦Γ⟧) 0 n

Tactic:
simp [hn]
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
Goal:
Γ : Type u_1
R : Type u_2
A : Type u_3
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
inst_5 : CommRing A
inst_6 : Algebra R A
x : A⟦Γ⟧
hx : ¬0 < (x - 1).orderTop
r : R
n : ℕ
hn : ¬n = 0
⊢ (powerSeriesFamily 0 (PowerSeries.binomialSeries A r) : (a : ℕ) → A⟦Γ⟧) n = HPow.hPow (α := A⟦Γ⟧) 0 n

Tactic:
simp [hn]
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
Goal:
Γ : Type u_1
R : Type u_2
A : Type u_3
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
inst_5 : CommRing A
inst_6 : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
n : ℕ
hn : 0 < n
simp : 0 < (Ring.choose r n • (x - 1) ^ n).orderTop
⊢ LT.lt.{u_1} (α := WithTop Γ) 0 (orderTop.{u_1, u_3} (R := A) ((binomialFamily x r : (a : ℕ) → A⟦Γ⟧) n))

Tactic:
simp only [binomialFamily, smulFamily_toFun, PowerSeries.binomialSeries_coeff, powers_toFun, hx,
    ↓reduceIte, smul_assoc, one_smul]

Premises used: smul_assoc, PowerSeries.binomialSeries_coeff, one_smul, HahnSeries.SummableFamily.smulFamily_toFun, HahnSeries.SummableFamily.powers_toFun, HahnSeries.SummableFamily.binomialFamily, reduceIte
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
Goal:
Γ : Type u_1
R : Type u_2
A : Type u_3
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
inst_5 : CommRing A
inst_6 : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
n : ℕ
hn : 0 < n
⊢ n ≠ 0

Tactic:
Nat.ne_zero_of_lt hn

Premises used: Nat.ne_zero_of_lt
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
Goal:
Γ : Type u_1
R : Type u_2
A : Type u_3
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
inst_5 : CommRing A
inst_6 : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
n : ℕ
hn : 0 < n
⊢ n ≠ 0

Tactic:
exact Nat.ne_zero_of_lt hn

Premises used: Nat.ne_zero_of_lt
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
Goal:
Γ : Type u_1
R : Type u_2
A : Type u_3
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
inst_5 : CommRing A
inst_6 : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
n : ℕ
hn : 0 < n
⊢ n ≠ 0

Tactic:
have : n ≠ 0 := by exact Nat.ne_zero_of_lt hn
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
Goal:
Γ : Type u_1
R : Type u_2
A : Type u_3
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
inst_5 : CommRing A
inst_6 : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
n : ℕ
hn : 0 < n
this : n ≠ 0
⊢ 0 < n • (x - 1).orderTop

Tactic:
(nsmul_pos_iff (Nat.ne_zero_of_lt hn)).mpr hx

Premises used: Iff.mpr, Nat.ne_zero_of_lt, nsmul_pos_iff
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
Goal:
Γ : Type u_1
R : Type u_2
A : Type u_3
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
inst_5 : CommRing A
inst_6 : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
n : ℕ
hn : 0 < n
this : n ≠ 0
⊢ n • (x - 1).orderTop ≤ ((x - 1) ^ n).orderTop

Tactic:
orderTop_nsmul_le_orderTop_pow

Premises used: HahnSeries.orderTop_nsmul_le_orderTop_pow
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
Goal:
Γ : Type u_1
R : Type u_2
A : Type u_3
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
inst_5 : CommRing A
inst_6 : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
n : ℕ
hn : 0 < n
this : n ≠ 0
⊢ ((x - 1) ^ n).orderTop ≤ (Ring.choose r n • (x - 1) ^ n).orderTop

Tactic:
orderTop_le_orderTop_smul (Ring.choose r n) ((x - 1) ^ n)

Premises used: HSub.hSub, Ring.choose, HPow.hPow, HahnSeries.orderTop_le_orderTop_smul, OfNat.ofNat
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
Goal:
Γ : Type u_1
R : Type u_2
A : Type u_3
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
inst_5 : CommRing A
inst_6 : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
n : ℕ
hn : 0 < n
this : n ≠ 0
⊢ 0 < (Ring.choose r n • (x - 1) ^ n).orderTop

Tactic:
calc
    0 < n • (x - 1).orderTop := (nsmul_pos_iff (Nat.ne_zero_of_lt hn)).mpr hx
    _ ≤ ((x - 1) ^ n).orderTop := orderTop_nsmul_le_orderTop_pow
    _ ≤ ((Ring.choose r n) • ((x - 1) ^ n)).orderTop :=
      orderTop_le_orderTop_smul (Ring.choose r n) ((x - 1) ^ n)

Premises used: Iff.mpr, HahnSeries.orderTop, HSub.hSub, HahnSeries.orderTop_nsmul_le_orderTop_pow, Ring.choose, HPow.hPow, HahnSeries.orderTop_le_orderTop_smul, HSMul.hSMul, Nat.ne_zero_of_lt, OfNat.ofNat, nsmul_pos_iff