awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
ι : Type u_7
inst_2 : Finite ι
x : R⟦Γ⟧
h : Nonempty ι
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (a : ι), x.support)

Tactic:
Eq.mpr (congrArg (fun s ↦ s.IsPWO) (Set.iUnion_const x.support)) x.isPWO_support

Premises used: Eq.mpr, HahnSeries.isPWO_support
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
ι : Type u_7
inst_2 : Finite ι
x : R⟦Γ⟧
h : Nonempty ι
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (a : ι), x.support)

Tactic:
exact Eq.mpr (congrArg (fun s ↦ s.IsPWO) (Set.iUnion_const x.support)) x.isPWO_support

Premises used: Eq.mpr
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
ι : Type u_7
inst_2 : Unique ι
x : SummableFamily Γ R ι
coeff : ∀ (g : Γ), x.hsum.coeff g = HahnSeries.coeff ((x : (a : ι) → R⟦Γ⟧) default) g
⊢ x.hsum = (x : (a : ι) → R⟦Γ⟧) default

Tactic:
ext g
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
ι : Type u_7
inst_2 : Unique ι
x : SummableFamily Γ R ι
g : Γ
⊢ x.hsum.coeff g = HahnSeries.coeff ((x : (a : ι) → R⟦Γ⟧) default) g

Tactic:
simp only [coeff_hsum, finsum_unique]

Premises used: finsum_unique, HahnSeries.SummableFamily.coeff_hsum
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
e : α ≃ β
s : SummableFamily Γ R α
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (a : β), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) ((e.symm : (a : β) → α) a)))

Tactic:
Set.IsPWO.mono s.isPWO_iUnion_support fun g => ?_

Premises used: HahnSeries.SummableFamily.isPWO_iUnion_support, Set.IsPWO.mono
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
e : α ≃ β
s : SummableFamily Γ R α
refine :
  ∀ (g : Γ),
    Membership.mem (γ := Set Γ)
        (⋃ (a : β), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) ((e.symm : (a : β) → α) a))) g →
      Membership.mem (γ := Set Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) g
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (a : β), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) ((e.symm : (a : β) → α) a)))

Tactic:
refine Set.IsPWO.mono s.isPWO_iUnion_support fun g => ?_

Premises used: HahnSeries.SummableFamily.isPWO_iUnion_support, Set.IsPWO.mono
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
e : α ≃ β
s : SummableFamily Γ R α
g : Γ
simp :
  ∀ (x : β) (h : ¬Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) ((e.symm : (a : β) → α) x)) g) 0),
    ∃ (i : α), ¬Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g) 0
⊢ Membership.mem (γ := Set Γ) (⋃ (a : β), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) ((e.symm : (a : β) → α) a)))
      g →
    Membership.mem (γ := Set Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) g

Tactic:
simp only [Set.mem_iUnion, mem_support, ne_eq, forall_exists_index]

Premises used: Set.mem_iUnion, forall_exists_index, ne_eq, HahnSeries.mem_support
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
e : α ≃ β
s : SummableFamily Γ R α
g : Γ
⊢ ∀ (x : β) (h : ¬Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) ((e.symm : (a : β) → α) x)) g) 0),
    ∃ (i : α), ¬Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g) 0

Tactic:
fun b hg => Exists.intro (e.symm b) hg

Premises used: Exists.intro, Equiv.symm, DFunLike.coe
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
e : α ≃ β
s : SummableFamily Γ R α
g : Γ
⊢ ∀ (x : β) (h : ¬Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) ((e.symm : (a : β) → α) x)) g) 0),
    ∃ (i : α), ¬Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g) 0

Tactic:
exact fun b hg => Exists.intro (e.symm b) hg

Premises used: Exists.intro, Equiv.symm, DFunLike.coe
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
e : α ≃ β
s : SummableFamily Γ R α
coeff : ∀ (g : Γ), (Equiv e s).hsum.coeff g = s.hsum.coeff g
⊢ (Equiv e s).hsum = s.hsum

Tactic:
ext g
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
e : α ≃ β
s : SummableFamily Γ R α
g : Γ
coeff :
  Eq.{u_3 + 1} (α := R) (∑ᶠ (i : β), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) ((e.symm : (a : β) → α) i)) g)
    (∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)
⊢ (Equiv e s).hsum.coeff g = s.hsum.coeff g

Tactic:
simp only [coeff_hsum, Equiv_toFun]

Premises used: HahnSeries.SummableFamily.Equiv_toFun, HahnSeries.SummableFamily.coeff_hsum
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
e : α ≃ β
s : SummableFamily Γ R α
g : Γ
⊢ Eq.{u_3 + 1} (α := R) (∑ᶠ (i : β), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) ((e.symm : (a : β) → α) i)) g)
    (∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)

Tactic:
finsum_eq_of_bijective e.symm (Equiv.bijective e.symm) fun x => rfl

Premises used: Equiv.bijective, finsum_eq_of_bijective, Equiv.symm, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
e : α ≃ β
s : SummableFamily Γ R α
g : Γ
⊢ Eq.{u_3 + 1} (α := R) (∑ᶠ (i : β), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) ((e.symm : (a : β) → α) i)) g)
    (∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)

Tactic:
exact finsum_eq_of_bijective e.symm (Equiv.bijective e.symm) fun x => rfl

Premises used: Equiv.bijective, finsum_eq_of_bijective, Equiv.symm, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
inst_2 : AddCommMonoid V
inst_3 : SMulWithZero R V
f : α → R
s : SummableFamily Γ V α
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (a : α), (HSMul.hSMul (β := V⟦Γ⟧) (f a) ((s : (a : α) → V⟦Γ⟧) a : V⟦Γ⟧)).support)

Tactic:
Set.IsPWO.mono s.isPWO_iUnion_support fun g hg => ?_

Premises used: HahnSeries.SummableFamily.isPWO_iUnion_support, Set.IsPWO.mono
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
inst_2 : AddCommMonoid V
inst_3 : SMulWithZero R V
f : α → R
s : SummableFamily Γ V α
refine :
  ∀ (g : Γ)
    (hg :
      Membership.mem (γ := Set Γ) (⋃ (a : α), (HSMul.hSMul (β := V⟦Γ⟧) (f a) ((s : (a : α) → V⟦Γ⟧) a : V⟦Γ⟧)).support)
        g),
    Membership.mem (γ := Set Γ) (⋃ (a : α), support.{u_1, u_4} (R := V) ((s : (a : α) → V⟦Γ⟧) a)) g
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (a : α), (HSMul.hSMul (β := V⟦Γ⟧) (f a) ((s : (a : α) → V⟦Γ⟧) a : V⟦Γ⟧)).support)

Tactic:
refine Set.IsPWO.mono s.isPWO_iUnion_support fun g hg => ?_

Premises used: HahnSeries.SummableFamily.isPWO_iUnion_support, Set.IsPWO.mono
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
inst_2 : AddCommMonoid V
inst_3 : SMulWithZero R V
f : α → R
s : SummableFamily Γ V α
g : Γ
hg : Membership.mem (γ := Set Γ) (⋃ (a : α), (HSMul.hSMul (β := V⟦Γ⟧) (f a) ((s : (a : α) → V⟦Γ⟧) a : V⟦Γ⟧)).support) g
simp_all :
  ∀ (hg : ∃ (i : α), ¬HSMul.hSMul (β := V) (f i) (HahnSeries.coeff ((s : (a : α) → V⟦Γ⟧) i) g) = 0),
    ∃ (i : α), ¬Eq.{u_4 + 1} (α := V) (HahnSeries.coeff ((s : (a : α) → V⟦Γ⟧) i) g) 0
⊢ Membership.mem (γ := Set Γ) (⋃ (a : α), support.{u_1, u_4} (R := V) ((s : (a : α) → V⟦Γ⟧) a)) g

Tactic:
simp_all only [Set.mem_iUnion, mem_support, coeff_smul, ne_eq]

Premises used: HahnSeries.coeff_smul, Set.mem_iUnion, ne_eq, HahnSeries.mem_support
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
inst_2 : AddCommMonoid V
inst_3 : SMulWithZero R V
f : α → R
s : SummableFamily Γ V α
g : Γ
hg : ∃ (i : α), ¬HSMul.hSMul (β := V) (f i) (HahnSeries.coeff ((s : (a : α) → V⟦Γ⟧) i) g) = 0
obtain :
  ∀ (i : α) (hi : ¬HSMul.hSMul (β := V) (f i) (HahnSeries.coeff ((s : (a : α) → V⟦Γ⟧) i) g) = 0),
    ∃ (i : α), ¬Eq.{u_4 + 1} (α := V) (HahnSeries.coeff ((s : (a : α) → V⟦Γ⟧) i) g) 0
⊢ ∃ (i : α), ¬Eq.{u_4 + 1} (α := V) (HahnSeries.coeff ((s : (a : α) → V⟦Γ⟧) i) g) 0

Tactic:
obtain ⟨i, hi⟩ := hg
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
inst_2 : AddCommMonoid V
inst_3 : SMulWithZero R V
f : α → R
s : SummableFamily Γ V α
g : Γ
i : α
hi : ¬HSMul.hSMul (β := V) (f i) (HahnSeries.coeff ((s : (a : α) → V⟦Γ⟧) i) g) = 0
⊢ ∃ (i : α), ¬Eq.{u_4 + 1} (α := V) (HahnSeries.coeff ((s : (a : α) → V⟦Γ⟧) i) g) 0

Tactic:
Exists.intro i <| right_ne_zero_of_smul hi

Premises used: right_ne_zero_of_smul, Exists.intro
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
inst_2 : AddCommMonoid V
inst_3 : SMulWithZero R V
f : α → R
s : SummableFamily Γ V α
g : Γ
i : α
hi : ¬HSMul.hSMul (β := V) (f i) (HahnSeries.coeff ((s : (a : α) → V⟦Γ⟧) i) g) = 0
⊢ ∃ (i : α), ¬Eq.{u_4 + 1} (α := V) (HahnSeries.coeff ((s : (a : α) → V⟦Γ⟧) i) g) 0

Tactic:
exact Exists.intro i <| right_ne_zero_of_smul hi

Premises used: right_ne_zero_of_smul, Exists.intro
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
inst_2 : AddCommMonoid V
inst_3 : SMulWithZero R V
f : α → R
s : SummableFamily Γ V α
g : Γ
⊢ Set.Finite.{u_5} (α := α) {a : α | (HSMul.hSMul (β := V⟦Γ⟧) (f a) ((s : (a : α) → V⟦Γ⟧) a : V⟦Γ⟧)).coeff g ≠ 0}

Tactic:
Set.Finite.subset (s.finite_co_support g) fun i hi => ?_

Premises used: Set.Finite.subset, HahnSeries.SummableFamily.finite_co_support
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
inst_2 : AddCommMonoid V
inst_3 : SMulWithZero R V
f : α → R
s : SummableFamily Γ V α
g : Γ
refine :
  ∀ (i : α)
    (hi :
      Membership.mem (γ := Set α) {a : α | (HSMul.hSMul (β := V⟦Γ⟧) (f a) ((s : (a : α) → V⟦Γ⟧) a : V⟦Γ⟧)).coeff g ≠ 0}
        i),
    Membership.mem (γ := Set α)
      (Function.support.{u_5, u_4} (M := V) fun (a : α) ↦ HahnSeries.coeff ((s : (a : α) → V⟦Γ⟧) a) g) i
⊢ Set.Finite.{u_5} (α := α) {a : α | (HSMul.hSMul (β := V⟦Γ⟧) (f a) ((s : (a : α) → V⟦Γ⟧) a : V⟦Γ⟧)).coeff g ≠ 0}

Tactic:
refine Set.Finite.subset (s.finite_co_support g) fun i hi => ?_

Premises used: Set.Finite.subset, HahnSeries.SummableFamily.finite_co_support
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
inst_2 : AddCommMonoid V
inst_3 : SMulWithZero R V
f : α → R
s : SummableFamily Γ V α
g : Γ
i : α
hi : Membership.mem (γ := Set α) {a : α | (HSMul.hSMul (β := V⟦Γ⟧) (f a) ((s : (a : α) → V⟦Γ⟧) a : V⟦Γ⟧)).coeff g ≠ 0} i
⊢ ¬HSMul.hSMul (β := V) (f i) (HahnSeries.coeff ((s : (a : α) → V⟦Γ⟧) i) g) = 0

Tactic:
simp_all only [coeff_smul, ne_eq, Set.mem_setOf_eq, Function.mem_support]

Premises used: HahnSeries.coeff_smul, Set.mem_setOf_eq, ne_eq, Function.mem_support
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
inst_2 : AddCommMonoid V
inst_3 : SMulWithZero R V
f : α → R
s : SummableFamily Γ V α
g : Γ
i : α
hi : ¬HSMul.hSMul (β := V) (f i) (HahnSeries.coeff ((s : (a : α) → V⟦Γ⟧) i) g) = 0
⊢ ¬Eq.{u_4 + 1} (α := V) (HahnSeries.coeff ((s : (a : α) → V⟦Γ⟧) i) g) 0

Tactic:
right_ne_zero_of_smul hi

Premises used: right_ne_zero_of_smul
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
inst_2 : AddCommMonoid V
inst_3 : SMulWithZero R V
f : α → R
s : SummableFamily Γ V α
g : Γ
i : α
hi : ¬HSMul.hSMul (β := V) (f i) (HahnSeries.coeff ((s : (a : α) → V⟦Γ⟧) i) g) = 0
⊢ ¬Eq.{u_4 + 1} (α := V) (HahnSeries.coeff ((s : (a : α) → V⟦Γ⟧) i) g) 0

Tactic:
exact right_ne_zero_of_smul hi

Premises used: right_ne_zero_of_smul
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_4
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
inst_2 : AddCommMonoid V
inst_3 : SMulWithZero R V
f : α → R
s : SummableFamily Γ V α
g : Γ
⊢ (smulFamily f s).hsum.coeff g = ∑ᶠ (i : α), HSMul.hSMul (β := V) (f i) (HahnSeries.coeff ((s : (a : α) → V⟦Γ⟧) i) g)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s : SummableFamily Γ R α
g g' : Γ
hg : ∀ (b : α) (g' : Γ), Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) b)) g' → g ≤ g'
hg' : g' ∈ s.hsum.support
⊢ Ne.{u_3 + 1} (α := R) (∑ i ∈ (s.coeff g').support, HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g') 0

Tactic:
rw [mem_support, coeff_hsum_eq_sum] at hg'

Premises used: HahnSeries.SummableFamily.coeff_hsum_eq_sum, HahnSeries.mem_support
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s : SummableFamily Γ R α
g g' : Γ
hg : ∀ (b : α) (g' : Γ), Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) b)) g' → g ≤ g'
hg' : Ne.{u_3 + 1} (α := R) (∑ i ∈ (s.coeff g').support, HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g') 0
obtain :
  ∀ i ∈ (s.coeff g').support, ∀ (hi : Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g') 0), g ≤ g'
⊢ g ≤ g'

Tactic:
obtain ⟨i, _, hi⟩ := Finset.exists_ne_zero_of_sum_ne_zero hg'

Premises used: Finset.exists_ne_zero_of_sum_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s : SummableFamily Γ R α
g g' : Γ
hg : ∀ (b : α) (g' : Γ), Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) b)) g' → g ≤ g'
hg' : Ne.{u_3 + 1} (α := R) (∑ i ∈ (s.coeff g').support, HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g') 0
i : α
left : i ∈ (s.coeff g').support
hi : Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g') 0
⊢ g ≤ g'

Tactic:
hg i g' hi
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s : SummableFamily Γ R α
g g' : Γ
hg : ∀ (b : α) (g' : Γ), Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) b)) g' → g ≤ g'
hg' : Ne.{u_3 + 1} (α := R) (∑ i ∈ (s.coeff g').support, HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g') 0
i : α
left : i ∈ (s.coeff g').support
hi : Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g') 0
⊢ g ≤ g'

Tactic:
exact hg i g' hi
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
a : α
ha : (↑g : WithTop Γ) = orderTop.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)
hg : ∀ (b : α) (g' : Γ), Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) b)) g' → g ≤ g'
hna : ∀ (b : α), b ≠ a → Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) b) g) 0
rw :
  Eq.{u_3 + 1} (α := R) (∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)
    (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g)
rw₁ rw₂ :
  Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g)
⊢ s.hsum.coeff g = HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g

Tactic:
rw [coeff_hsum, finsum_eq_single (fun i ↦ (s i).coeff g) a
    hna]

Premises used: HahnSeries.SummableFamily.coeff_hsum, HahnSeries.coeff, DFunLike.coe, finsum_eq_single
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
a : α
ha : (↑g : WithTop Γ) = orderTop.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)
hg : ∀ (b : α) (g' : Γ), Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) b)) g' → g ≤ g'
hna : ∀ (b : α), b ≠ a → Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) b) g) 0
⊢ s.hsum.orderTop = (↑g : WithTop Γ)

Tactic:
have := hsum_orderTop_of_le ha hg hna
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
a : α
ha : (↑g : WithTop Γ) = orderTop.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)
hg : ∀ (b : α) (g' : Γ), Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) b)) g' → g ≤ g'
hna : ∀ (b : α), b ≠ a → Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) b) g) 0
this : s.hsum.orderTop = (↑g : WithTop Γ)
⊢ (if h : s.hsum = 0 then ⊤ else (↑(⋯.min (s := s.hsum.support) ⋯) : WithTop Γ)) = (↑g : WithTop Γ)

Tactic:
rw [orderTop] at this

Premises used: HahnSeries.orderTop
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
a : α
ha : (↑g : WithTop Γ) = orderTop.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)
hg : ∀ (b : α) (g' : Γ), Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) b)) g' → g ≤ g'
hna : ∀ (b : α), b ≠ a → Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) b) g) 0
this : (if h : s.hsum = 0 then ⊤ else (↑(⋯.min (s := s.hsum.support) ⋯) : WithTop Γ)) = (↑g : WithTop Γ)
by_contra : ∀ (h : s.hsum = 0), False
⊢ s.hsum ≠ 0

Tactic:
by_contra h
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
a : α
ha : (↑g : WithTop Γ) = orderTop.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)
hg : ∀ (b : α) (g' : Γ), Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) b)) g' → g ≤ g'
hna : ∀ (b : α), b ≠ a → Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) b) g) 0
this : (if h : s.hsum = 0 then ⊤ else (↑(⋯.min (s := s.hsum.support) ⋯) : WithTop Γ)) = (↑g : WithTop Γ)
h : s.hsum = 0
⊢ False

Tactic:
simp [h] at this
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
a : α
ha : (↑g : WithTop Γ) = orderTop.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)
hg : ∀ (b : α) (g' : Γ), Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) b)) g' → g ≤ g'
hna : ∀ (b : α), b ≠ a → Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) b) g) 0
this : (if h : s.hsum = 0 then ⊤ else (↑(⋯.min (s := s.hsum.support) ⋯) : WithTop Γ)) = (↑g : WithTop Γ)
⊢ s.hsum ≠ 0

Tactic:
have hs : s.hsum ≠ 0 := by
    by_contra h
    simp [h] at this
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
a : α
ha : (↑g : WithTop Γ) = orderTop.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)
hg : ∀ (b : α) (g' : Γ), Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) b)) g' → g ≤ g'
hna : ∀ (b : α), b ≠ a → Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) b) g) 0
this : (if h : s.hsum = 0 then ⊤ else (↑(⋯.min (s := s.hsum.support) ⋯) : WithTop Γ)) = (↑g : WithTop Γ)
hs : s.hsum ≠ 0
⊢ ⋯.min (s := s.hsum.support) ⋯ = g

Tactic:
simp only [hs, ↓reduceDIte, WithTop.coe_eq_coe] at this

Premises used: reduceDIte, WithTop.coe_eq_coe
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
a : α
ha : (↑g : WithTop Γ) = orderTop.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)
hg : ∀ (b : α) (g' : Γ), Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) b)) g' → g ≤ g'
hna : ∀ (b : α), b ≠ a → Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) b) g) 0
hs : s.hsum ≠ 0
this : ⋯.min (s := s.hsum.support) ⋯ = g
simp :
  Eq.{u_3 + 1} (α := R) (∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)
    (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g)
⊢ s.hsum.leadingCoeff = HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g

Tactic:
simp only [leadingCoeff_of_ne_zero hs, coeff_hsum, untop_orderTop_of_ne_zero hs, this]

Premises used: HahnSeries.untop_orderTop_of_ne_zero, HahnSeries.SummableFamily.coeff_hsum, HahnSeries.leadingCoeff_of_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
a : α
ha : (↑g : WithTop Γ) = orderTop.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)
hg : ∀ (b : α) (g' : Γ), Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) b)) g' → g ≤ g'
hna : ∀ (b : α), b ≠ a → Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) b) g) 0
hs : s.hsum ≠ 0
this : ⋯.min (s := s.hsum.support) ⋯ = g
rw rw₁ :
  Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g)
⊢ Eq.{u_3 + 1} (α := R) (∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)
    (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g)

Tactic:
rw [finsum_eq_single (fun i ↦ (s i).coeff g) a hna]

Premises used: HahnSeries.coeff, DFunLike.coe, finsum_eq_single
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommGroup R
s_1 t : SummableFamily Γ R α
a : α
s : SummableFamily Γ R α
simp_rw : Set.IsPWO.{u_1} (α := Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a))
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) (-(s : (a : α) → R⟦Γ⟧) a))

Tactic:
simp_rw [support_neg]

Premises used: HahnSeries.support_neg
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommGroup R
s_1 t : SummableFamily Γ R α
a : α
s : SummableFamily Γ R α
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a))

Tactic:
s.isPWO_iUnion_support

Premises used: HahnSeries.SummableFamily.isPWO_iUnion_support
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommGroup R
s_1 t : SummableFamily Γ R α
a : α
s : SummableFamily Γ R α
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a))

Tactic:
exact s.isPWO_iUnion_support

Premises used: HahnSeries.SummableFamily.isPWO_iUnion_support