awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst : PartialOrder Γ
inst_1 : Semiring R
inst_2 : AddCommMonoid V
inst_3 : Module R V
a : Γ
r : R
s : V
b : Γ
h : b = a
⊢ coeff (ZeroHom.toFun (↑(addMonoidHom a) : ZeroHom V V⟦Γ⟧) (r • s)) b =
    (HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((RingHom.id R : (a : R) → R) r : R)
          (ZeroHom.toFun (↑(addMonoidHom a) : ZeroHom V V⟦Γ⟧) s)).coeff
      b

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst : PartialOrder Γ
inst_1 : Semiring R
inst_2 : AddCommMonoid V
inst_3 : Module R V
a : Γ
r : R
s : V
b : Γ
h : ¬b = a
⊢ coeff (ZeroHom.toFun (↑(addMonoidHom a) : ZeroHom V V⟦Γ⟧) (r • s)) b =
    (HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((RingHom.id R : (a : R) → R) r : R)
          (ZeroHom.toFun (↑(addMonoidHom a) : ZeroHom V V⟦Γ⟧) s)).coeff
      b

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
U : Type u_5
V : Type u_6
inst : PartialOrder Γ
inst_1 : Semiring R
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : AddCommMonoid U
inst_5 : Module R U
f : U →ₗ[R] V
r : R
x : U⟦Γ⟧
coeff : ∀ (x_1 : Γ), HahnSeries.coeff ((r • x).map f) x_1 = (HSMul.hSMul (β := V⟦Γ⟧) r (x.map f)).coeff x_1
⊢ (r • x).map f = HSMul.hSMul (β := V⟦Γ⟧) r (x.map f)

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
U : Type u_5
V : Type u_6
inst : PartialOrder Γ
inst_1 : Semiring R
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : AddCommMonoid U
inst_5 : Module R U
f : U →ₗ[R] V
r : R
x : U⟦Γ⟧
x_1 : Γ
⊢ coeff ((r • x).map f) x_1 = (HSMul.hSMul (β := V⟦Γ⟧) r (x.map f)).coeff x_1

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst : PartialOrder Γ
inst_1 : Semiring R
inst_2 : AddCommMonoid V
inst_3 : Module R V
x x_1 : Γ →₀ V
coeff :
  ∀ (x_2 : Γ),
    HahnSeries.coeff ((ofFinsupp : (a : Γ →₀ V) → V⟦Γ⟧) (x + x_1)) x_2 =
      (HAdd.hAdd (α := V⟦Γ⟧) (β := V⟦Γ⟧) ((ofFinsupp : (a : Γ →₀ V) → V⟦Γ⟧) x : V⟦Γ⟧)
            ((ofFinsupp : (a : Γ →₀ V) → V⟦Γ⟧) x_1 : V⟦Γ⟧)).coeff
        x_2
⊢ (ofFinsupp : (a : Γ →₀ V) → V⟦Γ⟧) (x + x_1) =
    HAdd.hAdd (α := V⟦Γ⟧) (β := V⟦Γ⟧) ((ofFinsupp : (a : Γ →₀ V) → V⟦Γ⟧) x : V⟦Γ⟧)
      ((ofFinsupp : (a : Γ →₀ V) → V⟦Γ⟧) x_1 : V⟦Γ⟧)

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst : PartialOrder Γ
inst_1 : Semiring R
inst_2 : AddCommMonoid V
inst_3 : Module R V
x x_1 : Γ →₀ V
x_2 : Γ
⊢ coeff ((ofFinsupp : (a : Γ →₀ V) → V⟦Γ⟧) (x + x_1)) x_2 =
    (HAdd.hAdd (α := V⟦Γ⟧) (β := V⟦Γ⟧) ((ofFinsupp : (a : Γ →₀ V) → V⟦Γ⟧) x : V⟦Γ⟧)
          ((ofFinsupp : (a : Γ →₀ V) → V⟦Γ⟧) x_1 : V⟦Γ⟧)).coeff
      x_2

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst : PartialOrder Γ
inst_1 : Semiring R
inst_2 : AddCommMonoid V
inst_3 : Module R V
x : R
x_1 : Γ →₀ V
coeff :
  ∀ (x_2 : Γ),
    HahnSeries.coeff ((ofFinsupp : (a : Γ →₀ V) → V⟦Γ⟧) (x • x_1)) x_2 =
      (HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((RingHom.id R : (a : R) → R) x : R)
            ((ofFinsupp : (a : Γ →₀ V) → V⟦Γ⟧) x_1 : V⟦Γ⟧)).coeff
        x_2
⊢ (ofFinsupp : (a : Γ →₀ V) → V⟦Γ⟧) (x • x_1) =
    HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((RingHom.id R : (a : R) → R) x : R) ((ofFinsupp : (a : Γ →₀ V) → V⟦Γ⟧) x_1 : V⟦Γ⟧)

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst : PartialOrder Γ
inst_1 : Semiring R
inst_2 : AddCommMonoid V
inst_3 : Module R V
x : R
x_1 : Γ →₀ V
x_2 : Γ
⊢ coeff ((ofFinsupp : (a : Γ →₀ V) → V⟦Γ⟧) (x • x_1)) x_2 =
    (HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((RingHom.id R : (a : R) → R) x : R)
          ((ofFinsupp : (a : Γ →₀ V) → V⟦Γ⟧) x_1 : V⟦Γ⟧)).coeff
      x_2

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_6
inst : PartialOrder Γ
inst_1 : Semiring R
inst_2 : AddCommMonoid V
inst_3 : Module R V
f : Γ →₀ V
a : Γ
⊢ Eq.{u_6 + 1} (α := V) (coeff ((ofFinsuppLinearMap R : (a : Γ →₀ V) → V⟦Γ⟧) f) a : V) ((f : (a : Γ) → V) a : V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Semiring R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
r : R
x : R⟦Γ⟧
coeff : ∀ (g : Γ'), (embDomain f (r • x)).coeff g = (r • embDomain f x).coeff g
⊢ embDomain f (r • x) = r • embDomain f x

Tactic:
ext g
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Semiring R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
r : R
x : R⟦Γ⟧
g : Γ'
pos :
  ∀ (hg : Membership.mem (γ := Set Γ') (Set.range.{u_2, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')) g),
    (embDomain f (r • x)).coeff g = (r • embDomain f x).coeff g
neg :
  ∀ (hg : g ∉ Set.range.{u_2, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')),
    (embDomain f (r • x)).coeff g = (r • embDomain f x).coeff g
⊢ (embDomain f (r • x)).coeff g = (r • embDomain f x).coeff g

Tactic:
by_cases hg : g ∈ Set.range f

Premises used: Set.range, DFunLike.coe
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Semiring R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
r : R
x : R⟦Γ⟧
g : Γ'
hg : Membership.mem (γ := Set Γ') (Set.range.{u_2, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')) g
pos : ∀ (a : Γ), (embDomain f (r • x)).coeff ((f : (a : Γ) → Γ') a) = (r • embDomain f x).coeff ((f : (a : Γ) → Γ') a)
⊢ (embDomain f (r • x)).coeff g = (r • embDomain f x).coeff g

Tactic:
obtain ⟨a, rfl⟩ := hg

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Semiring R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
r : R
x : R⟦Γ⟧
a : Γ
⊢ (embDomain f (r • x)).coeff ((f : (a : Γ) → Γ') a) = (r • embDomain f x).coeff ((f : (a : Γ) → Γ') a)

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Semiring R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
r : R
x : R⟦Γ⟧
g : Γ'
hg : g ∉ Set.range.{u_2, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')
⊢ (embDomain f (r • x)).coeff g = (r • embDomain f x).coeff g

Tactic:
simp [embDomain_notin_range hg]

Premises used: HahnSeries.embDomain_notin_range
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_6
inst : PartialOrder Γ
inst_1 : Semiring R
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : DecidableLT Γ
c : Γ
⊢ Eq (α := (a : V⟦Γ⟧) → V⟦Γ⟧) (⇑(truncLTLinearMap R c) : (a : V⟦Γ⟧) → V⟦Γ⟧) (⇑(truncLT c) : (a : V⟦Γ⟧) → V⟦Γ⟧)

Tactic:
rfl
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
⊢ Injective (α := R⟦Γ⟧) coeff

Tactic:
fun _ _ => HahnSeries.ext

Premises used: HahnSeries.ext, Function.Injective
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x y : R⟦Γ⟧
⊢ x.coeff = y.coeff ↔ x = y

Tactic:
coeff_injective.eq_iff

Premises used: Function.Injective.eq_iff, HahnSeries.coeff_injective
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
f : Γ → R
h : (Function.support f).IsPWO
⊢ { coeff := f, isPWO_support' := h : R⟦Γ⟧ }.support = Function.support f

Tactic:
rfl

Premises used: HahnSeries.support, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
⊢ x.support.IsPWO

Tactic:
x.isPWO_support'

Premises used: HahnSeries.support, HahnSeries.isPWO_support'
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
⊢ x.support.IsWF

Tactic:
x.isPWO_support.isWF

Premises used: HahnSeries.isPWO_support, Set.IsPWO.isWF
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
a : Γ
⊢ a ∈ x.support ↔ x.coeff a ≠ 0

Tactic:
.rfl

Premises used: HahnSeries.support, Set.Mem, Iff.rfl, setOf, Function.support, Not
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
⊢ Set.IsPWO.{u_1} (α := Γ) (Function.support.{u_1, u_3} (M := R) 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Subsingleton R
x x_1 : R⟦Γ⟧
⊢ x.coeff = x_1.coeff

Tactic:
subsingleton
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
⊢ Eq (α := Γ → R) (coeff 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
⊢ Eq.{u_3 + 1} (α := R) (coeff 0 a) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
⊢ x.coeff = 0 ↔ x = 0

Tactic:
coeff_injective.eq_iff' rfl

Premises used: HahnSeries.coeff_injective, Function.Injective.eq_iff', rfl
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
g : Γ
h : x.coeff g ≠ 0
⊢ x ≠ 0

Tactic:
mt (fun x0 => (x0.symm ▸ coeff_zero : x.coeff g = 0)) h

Premises used: mt, Eq.rec, HahnSeries.coeff_zero, Eq.symm
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
⊢ Eq.{u_1 + 1} (α := Set Γ) (support.{u_1, u_3} (R := R) 0) ∅

Tactic:
Function.support_zero

Premises used: HahnSeries.support, Function.support_zero
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
rw : (Function.support x.coeff).Nonempty ↔ x ≠ 0
rw₁ : x.coeff ≠ 0 ↔ x ≠ 0
rw₂ : ¬x.coeff = 0 ↔ x ≠ 0
rw₃ rw₄ : ¬x = 0 ↔ x ≠ 0
⊢ x.support.Nonempty ↔ x ≠ 0

Tactic:
rw [support, support_nonempty_iff, Ne, coeff_fun_eq_zero_iff]

Premises used: HahnSeries.support, HahnSeries.coeff_fun_eq_zero_iff, Ne, HahnSeries.support_nonempty_iff
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
⊢ x.support = ∅ ↔ x = 0

Tactic:
Function.support_eq_empty_iff.trans coeff_fun_eq_zero_iff

Premises used: HahnSeries.support, HahnSeries.coeff_fun_eq_zero_iff, Function.support_eq_empty_iff, Iff.trans
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero S
f : ZeroHom R S
coeff : ∀ (x : Γ), HahnSeries.coeff (map 0 f) x = HahnSeries.coeff 0 x
⊢ Eq (α := S⟦Γ⟧) (map 0 f) 0

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero S
f : ZeroHom R S
x : Γ
⊢ coeff (map 0 f) x = coeff 0 x

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero S
x : R⟦Γ⟧
f : ZeroHom R S
⊢ support (x.map f) ⊆ x.support

Tactic:
Function.support_comp_subset (ZeroHomClass.map_zero f) _

Premises used: HahnSeries.support, Function.support_comp_subset, ZeroHomClass.map_zero
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
x : R⟦Γ'⟧⟦Γ⟧
⊢ Set.IsPWO (α := Lex (Γ × Γ')) (Function.support (M := R) fun (g : Lex (Γ × Γ')) ↦ (x.coeff g.1).coeff g.2)

Tactic:
Set.PartiallyWellOrderedOn.subsetProdLex ?_ ?_

Premises used: Set.PartiallyWellOrderedOn.subsetProdLex
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
x : R⟦Γ'⟧⟦Γ⟧
refine_1 :
  Set.IsPWO.{u_1} (α := Γ)
    ((fun (x : Lex (Γ × Γ')) ↦ ((ofLex : (a : Lex (Γ × Γ')) → Γ × Γ') x).1) ''
      Function.support (M := R) fun (g : Lex (Γ × Γ')) ↦ (x.coeff g.1).coeff g.2)
refine_2 :
  ∀ (a : Γ),
    Set.IsPWO.{u_2} (α := Γ')
      {y : Γ' |
        Membership.mem (α := Lex (Γ × Γ')) (γ := Set (Lex (Γ × Γ')))
          (Function.support (M := R) fun (g : Lex (Γ × Γ')) ↦ (x.coeff g.1).coeff g.2)
          ((toLex : (a : Γ × Γ') → Lex (Γ × Γ')) (a, y) : Lex (Γ × Γ'))}
⊢ Set.IsPWO (α := Lex (Γ × Γ')) (Function.support (M := R) fun (g : Lex (Γ × Γ')) ↦ (x.coeff g.1).coeff g.2)

Tactic:
refine Set.PartiallyWellOrderedOn.subsetProdLex ?_ ?_

Premises used: Set.PartiallyWellOrderedOn.subsetProdLex
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
x : R⟦Γ'⟧⟦Γ⟧
⊢ Set.IsPWO.{u_1} (α := Γ)
    ((fun (x : Lex (Γ × Γ')) ↦ ((ofLex : (a : Lex (Γ × Γ')) → Γ × Γ') x).1) ''
      Function.support (M := R) fun (g : Lex (Γ × Γ')) ↦ (x.coeff g.1).coeff g.2)

Tactic:
Set.IsPWO.mono x.isPWO_support' ?_

Premises used: HahnSeries.isPWO_support', Set.IsPWO.mono
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
x : R⟦Γ'⟧⟦Γ⟧
refine_1 :
  ((fun (x : Lex (Γ × Γ')) ↦ ((ofLex : (a : Lex (Γ × Γ')) → Γ × Γ') x).1) ''
      Function.support (M := R) fun (g : Lex (Γ × Γ')) ↦ (x.coeff g.1).coeff g.2) ⊆
    Function.support x.coeff
⊢ Set.IsPWO.{u_1} (α := Γ)
    ((fun (x : Lex (Γ × Γ')) ↦ ((ofLex : (a : Lex (Γ × Γ')) → Γ × Γ') x).1) ''
      Function.support (M := R) fun (g : Lex (Γ × Γ')) ↦ (x.coeff g.1).coeff g.2)

Tactic:
refine Set.IsPWO.mono x.isPWO_support' ?_

Premises used: HahnSeries.isPWO_support', Set.IsPWO.mono
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
x : R⟦Γ'⟧⟦Γ⟧
refine_1 :
  ∀ (x_1 : Lex (Γ × Γ')), (x.coeff x_1.1).coeff x_1.2 ≠ 0 → x.coeff ((ofLex : (a : Lex (Γ × Γ')) → Γ × Γ') x_1).1 ≠ 0
⊢ ((fun (x : Lex (Γ × Γ')) ↦ ((ofLex : (a : Lex (Γ × Γ')) → Γ × Γ') x).1) ''
      Function.support (M := R) fun (g : Lex (Γ × Γ')) ↦ (x.coeff g.1).coeff g.2) ⊆
    Function.support x.coeff

Tactic:
simp_rw [Set.image_subset_iff, support_subset_iff, Set.mem_preimage, Function.mem_support]

Premises used: Function.support_subset_iff, Function.mem_support, Set.image_subset_iff, Set.mem_preimage
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
x : R⟦Γ'⟧⟦Γ⟧
⊢ ∀ (x_1 : Lex (Γ × Γ')), (x.coeff x_1.1).coeff x_1.2 ≠ 0 → x.coeff ((ofLex : (a : Lex (Γ × Γ')) → Γ × Γ') x_1).1 ≠ 0

Tactic:
fun _ ↦ ne_zero_of_coeff_ne_zero

Premises used: HahnSeries.ne_zero_of_coeff_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
x : R⟦Γ'⟧⟦Γ⟧
⊢ ∀ (x_1 : Lex (Γ × Γ')), (x.coeff x_1.1).coeff x_1.2 ≠ 0 → x.coeff ((ofLex : (a : Lex (Γ × Γ')) → Γ × Γ') x_1).1 ≠ 0

Tactic:
exact fun _ ↦ ne_zero_of_coeff_ne_zero

Premises used: HahnSeries.ne_zero_of_coeff_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
x : R⟦Γ'⟧⟦Γ⟧
a : Γ
⊢ Set.IsPWO.{u_2} (α := Γ')
    {y : Γ' |
      Membership.mem (α := Lex (Γ × Γ')) (γ := Set (Lex (Γ × Γ')))
        (Function.support (M := R) fun (g : Lex (Γ × Γ')) ↦ (x.coeff g.1).coeff g.2)
        ((toLex : (a : Γ × Γ') → Lex (Γ × Γ')) (a, y) : Lex (Γ × Γ'))}

Tactic:
simpa [Function.mem_support, ne_eq] using (x.coeff a).isPWO_support'

Premises used: HahnSeries.isPWO_support', ne_eq, Function.mem_support, HahnSeries.coeff
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
x : R⟦Γ'⟧⟦Γ⟧
⊢ ∀ (a : Γ),
    Set.IsPWO.{u_2} (α := Γ')
      {y : Γ' |
        Membership.mem (α := Lex (Γ × Γ')) (γ := Set (Lex (Γ × Γ')))
          (Function.support (M := R) fun (g : Lex (Γ × Γ')) ↦ (x.coeff g.1).coeff g.2)
          ((toLex : (a : Γ × Γ') → Lex (Γ × Γ')) (a, y) : Lex (Γ × Γ'))}

Tactic:
exact fun a => by simpa [Function.mem_support, ne_eq] using (x.coeff a).isPWO_support'
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
f : Γ → R
h : (Function.support f).IsPWO
simp_rw : f = coeff 0 ↔ f = 0
simp_rw₁ : (∀ (x : Γ), f x = coeff 0 x) ↔ ∀ (x : Γ), f x = 0 x
simp_rw₂ : (∀ (x : Γ), f x = 0) ↔ ∀ (x : Γ), f x = 0 x
⊢ { coeff := f, isPWO_support' := h : R⟦Γ⟧ } = 0 ↔ f = 0

Tactic:
simp_rw [HahnSeries.ext_iff, funext_iff, coeff_zero, Pi.zero_apply]

Premises used: funext_iff, Pi.zero_apply, HahnSeries.ext_iff, HahnSeries.coeff_zero
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
x : R⟦Lex (Γ × Γ')⟧
⊢ Eq.{u_1 + 1} (α := Set Γ)
    (Function.support (M := R⟦Γ'⟧) fun (g : Γ) ↦ { coeff := fun (g' : Γ') ↦ x.coeff (g, g'), isPWO_support' := ⋯ })
    (Function.support (M := (g' : Γ') → R) fun (g : Γ) (g' : Γ') ↦ x.coeff (g, g'))

Tactic:
simp only [Function.support, ne_eq, mk_eq_zero]

Premises used: ne_eq, Function.support, HahnSeries.mk_eq_zero
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
x : R⟦Lex (Γ × Γ')⟧
⊢ Eq.{u_1 + 1} (α := Set Γ)
    (Function.support (M := R⟦Γ'⟧) fun (g : Γ) ↦ { coeff := fun (g' : Γ') ↦ x.coeff (g, g'), isPWO_support' := ⋯ })
    (Function.support (M := (g' : Γ') → R) fun (g : Γ) (g' : Γ') ↦ x.coeff (g, g'))

Tactic:
have h₁ : (Function.support fun g => HahnSeries.mk (fun g' => x.coeff (g, g'))
        (Set.PartiallyWellOrderedOn.fiberProdLex x.isPWO_support' g)) = Function.support
        fun g => fun g' => x.coeff (g, g') := by
      simp only [Function.support, ne_eq, mk_eq_zero]
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
x : R⟦Lex (Γ × Γ')⟧
h₁ :
  Eq.{u_1 + 1} (α := Set Γ)
    (Function.support (M := R⟦Γ'⟧) fun (g : Γ) ↦ { coeff := fun (g' : Γ') ↦ x.coeff (g, g'), isPWO_support' := ⋯ })
    (Function.support (M := (g' : Γ') → R) fun (g : Γ) (g' : Γ') ↦ x.coeff (g, g'))
rw : (Prod.fst '' Function.support x.coeff).IsPWO
⊢ Set.IsPWO.{u_1} (α := Γ)
    (Function.support (M := R⟦Γ'⟧) fun (g : Γ) ↦ { coeff := fun (g' : Γ') ↦ x.coeff (g, g'), isPWO_support' := ⋯ })

Tactic:
rw [h₁, Function.support_fun_curry x.coeff]

Premises used: Function.support_fun_curry, HahnSeries.coeff
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
x : R⟦Lex (Γ × Γ')⟧
h₁ :
  Eq.{u_1 + 1} (α := Set Γ)
    (Function.support (M := R⟦Γ'⟧) fun (g : Γ) ↦ { coeff := fun (g' : Γ') ↦ x.coeff (g, g'), isPWO_support' := ⋯ })
    (Function.support (M := (g' : Γ') → R) fun (g : Γ) (g' : Γ') ↦ x.coeff (g, g'))
⊢ (Prod.fst '' Function.support x.coeff).IsPWO

Tactic:
Set.PartiallyWellOrderedOn.imageProdLex x.isPWO_support'

Premises used: Lex, Set.PartiallyWellOrderedOn.imageProdLex, HahnSeries.isPWO_support'
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
x : R⟦Lex (Γ × Γ')⟧
h₁ :
  Eq.{u_1 + 1} (α := Set Γ)
    (Function.support (M := R⟦Γ'⟧) fun (g : Γ) ↦ { coeff := fun (g' : Γ') ↦ x.coeff (g, g'), isPWO_support' := ⋯ })
    (Function.support (M := (g' : Γ') → R) fun (g : Γ) (g' : Γ') ↦ x.coeff (g, g'))
⊢ (Prod.fst '' Function.support x.coeff).IsPWO

Tactic:
exact Set.PartiallyWellOrderedOn.imageProdLex x.isPWO_support'

Premises used: Set.PartiallyWellOrderedOn.imageProdLex, HahnSeries.isPWO_support'
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
r : R
⊢ coeff ((single a : (a : R) → R⟦Γ⟧) r) a = r

Tactic:
Pi.single_eq_same (M := fun _ => R) a r

Premises used: Function.update, Pi.single, dite, Pi.single_eq_same
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
r : R
⊢ coeff ((single a : (a : R) → R⟦Γ⟧) r) a = r

Tactic:
exact Pi.single_eq_same (M := fun _ => R) a r

Premises used: Pi.single_eq_same
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
r : R
⊢ coeff ((single a : (a : R) → R⟦Γ⟧) r) a = r

Tactic:
classical exact Pi.single_eq_same (M := fun _ => R) a r
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a b : Γ
r : R
h : b ≠ a
⊢ Eq.{u_3 + 1} (α := R) (coeff ((single a : (a : R) → R⟦Γ⟧) r) b) 0

Tactic:
Pi.single_eq_of_ne (M := fun _ => R) h r

Premises used: Function.update, Pi.single_eq_of_ne, Pi.single, dite
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a b : Γ
r : R
h : b ≠ a
⊢ Eq.{u_3 + 1} (α := R) (coeff ((single a : (a : R) → R⟦Γ⟧) r) b) 0

Tactic:
exact Pi.single_eq_of_ne (M := fun _ => R) h r

Premises used: Pi.single_eq_of_ne
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a b : Γ
r : R
h : b ≠ a
⊢ Eq.{u_3 + 1} (α := R) (coeff ((single a : (a : R) → R⟦Γ⟧) r) b) 0

Tactic:
classical exact Pi.single_eq_of_ne (M := fun _ => R) h r
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a b : Γ
r : R
pos : ∀ (h : b = a), coeff ((single a : (a : R) → R⟦Γ⟧) r) b = r
neg : ∀ (h : ¬b = a), Eq.{u_3 + 1} (α := R) (coeff ((single a : (a : R) → R⟦Γ⟧) r) b) 0
⊢ coeff ((single a : (a : R) → R⟦Γ⟧) r) b = if b = a then r else 0

Tactic:
split_ifs with h
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a b : Γ
r : R
h : b = a
⊢ coeff ((single a : (a : R) → R⟦Γ⟧) r) b = r

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a b : Γ
r : R
h : ¬b = a
⊢ Eq.{u_3 + 1} (α := R) (coeff ((single a : (a : R) → R⟦Γ⟧) r) b) 0

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
r : R
h : r ≠ 0
⊢ Eq (α := Set Γ) (support.{u_1, u_3} (R := R) ((single a : (a : R) → R⟦Γ⟧) r)) {a}

Tactic:
Pi.support_single_of_ne h

Premises used: HahnSeries.support, Function.update, Pi.support_single_of_ne, Pi.single, dite
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
r : R
h : r ≠ 0
⊢ Eq (α := Set Γ) (support.{u_1, u_3} (R := R) ((single a : (a : R) → R⟦Γ⟧) r)) {a}

Tactic:
exact Pi.support_single_of_ne h

Premises used: Pi.support_single_of_ne
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
r : R
h : r ≠ 0
⊢ Eq (α := Set Γ) (support.{u_1, u_3} (R := R) ((single a : (a : R) → R⟦Γ⟧) r)) {a}

Tactic:
classical exact Pi.support_single_of_ne h

Premises used: Pi.support_single_of_ne