awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
⊢ Eq (α := (a : α) → R⟦Γ⟧) (⇑0 : (a : α) → R⟦Γ⟧) 0

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
a : α
⊢ Eq (α := R⟦Γ⟧) ((0 : (a : α) → R⟦Γ⟧) a : R⟦Γ⟧) (0 : R⟦Γ⟧)

Tactic:
rfl

Premises used: 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
M : Type u_7
inst_2 : SMulZeroClass M R
r : M
t : SummableFamily Γ R β
g : Γ
⊢ Set.Finite.{u_6} (α := β) {a : β | (HSMul.hSMul (β := (a : β) → R⟦Γ⟧) r (⇑t : (a : β) → R⟦Γ⟧) a).coeff g ≠ 0}

Tactic:
(t.finite_co_support g).subset ?_

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
M : Type u_7
inst_2 : SMulZeroClass M R
r : M
t : SummableFamily Γ R β
g : Γ
refine :
  Subset.{u_6} (α := Set β) {a : β | (HSMul.hSMul (β := (a : β) → R⟦Γ⟧) r (⇑t : (a : β) → R⟦Γ⟧) a).coeff g ≠ 0}
    (Function.support.{u_6, u_3} (M := R) fun (a : β) ↦ coeff ((t : (a : β) → R⟦Γ⟧) a) g)
⊢ Set.Finite.{u_6} (α := β) {a : β | (HSMul.hSMul (β := (a : β) → R⟦Γ⟧) r (⇑t : (a : β) → R⟦Γ⟧) a).coeff g ≠ 0}

Tactic:
refine (t.finite_co_support g).subset ?_

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
M : Type u_7
inst_2 : SMulZeroClass M R
r : M
t : SummableFamily Γ R β
g : Γ
i : β
hi : ¬HSMul.hSMul (β := R) r (coeff ((t : (a : β) → R⟦Γ⟧) i) g) = 0
⊢ ¬Eq.{u_3 + 1} (α := R) (coeff ((t : (a : β) → R⟦Γ⟧) 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
M : Type u_7
inst_2 : SMulZeroClass M R
r : M
t : SummableFamily Γ R β
g : Γ
i : β
hi : ¬HSMul.hSMul (β := R) r (coeff ((t : (a : β) → R⟦Γ⟧) i) g) = 0
⊢ ¬Eq.{u_3 + 1} (α := R) (coeff ((t : (a : β) → R⟦Γ⟧) 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
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
M : Type u_7
inst_2 : SMulZeroClass M R
m : M
s : SummableFamily Γ R α
⊢ (⇑(m • s) : (a : α) → R⟦Γ⟧) = HSMul.hSMul (β := (a : α) → R⟦Γ⟧) m (⇑s : (a : α) → R⟦Γ⟧)

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
M : Type u_7
inst_2 : SMulZeroClass M R
m : M
s : SummableFamily Γ R α
a : α
⊢ (m • s : (a : α) → R⟦Γ⟧) a = HSMul.hSMul (β := R⟦Γ⟧) m ((s : (a : α) → R⟦Γ⟧) a : R⟦Γ⟧)

Tactic:
rfl

Premises used: 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
s : SummableFamily Γ R α
g : Γ
a : α
⊢ a ∈
      Set.Finite.toFinset (s :=
        Function.support.{u_5, u_3} (M := R) fun (a : α) ↦ HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) ⋯ ↔
    Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) 0

Tactic:
simp
-- 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 α
a : α
g : Γ
⊢ Eq.{u_3 + 1} (α := R) ((s.coeff g : (a : α) → R) a : R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g : R)

Tactic:
rfl

Premises used: 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
s : SummableFamily Γ R α
g : Γ
contrapose :
  g ∉ ⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a) →
    g ∉ Function.support.{u_1, u_3} (M := R) fun (g : Γ) ↦ ∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g
⊢ Membership.mem (γ := Set Γ)
      (Function.support.{u_1, u_3} (M := R) fun (g : Γ) ↦ ∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g) g →
    Membership.mem (γ := Set Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) g

Tactic:
contrapose
-- 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
s : SummableFamily Γ R α
g : Γ
rw :
  (∀ (x : α), g ∉ support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) x)) →
    Eq.{u_3 + 1} (α := R) (∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g) 0
⊢ g ∉ ⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a) →
    g ∉ Function.support.{u_1, u_3} (M := R) fun (g : Γ) ↦ ∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g

Tactic:
rw [Set.mem_iUnion, not_exists, Function.mem_support, Classical.not_not]

Premises used: Classical.not_not, Set.mem_iUnion, not_exists, 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
s : SummableFamily Γ R α
g : Γ
simp_rw :
  (∀ (x : α), Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) x) g) 0) →
    Eq.{u_3 + 1} (α := R) (∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g) 0
⊢ (∀ (x : α), g ∉ support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) x)) →
    Eq.{u_3 + 1} (α := R) (∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g) 0

Tactic:
simp_rw [mem_support, Classical.not_not]

Premises used: Classical.not_not, 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
s : SummableFamily Γ R α
g : Γ
h : ∀ (x : α), Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) x) g) 0
rw : Eq.{u_3 + 1} (α := R) (∑ᶠ (x : α), 0) 0
rw₁ rw₂ : Eq.{u_3 + 1} (α := R) 0 0
⊢ Eq.{u_3 + 1} (α := R) (∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g) 0

Tactic:
rw [finsum_congr h, finsum_zero]

Premises used: finsum_zero, finsum_congr
-- 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 : Γ
⊢ s.hsum.coeff g = ∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) 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
coeff : ∀ (x : Γ), Eq.{u_3 + 1} (α := R) (HahnSeries.coeff (hsum.{u_1, u_3, u_5} (α := α) 0) x) (HahnSeries.coeff 0 x)
⊢ Eq (α := R⟦Γ⟧) (hsum.{u_1, u_3, u_5} (α := α) 0) 0

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
x : Γ
⊢ Eq.{u_3 + 1} (α := R) (HahnSeries.coeff (hsum.{u_1, u_3, u_5} (α := α) 0) x) (HahnSeries.coeff 0 x)

Tactic:
simp
-- 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 : Γ
hg : g ∈ s.hsum.support
⊢ Ne.{u_3 + 1} (α := R)
    (∑
      i ∈
        Set.Finite.toFinset (s :=
          Function.support.{u_5, u_3} (M := R) fun (a : α) ↦ HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) ⋯,
      HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)
    0

Tactic:
rw [mem_support, coeff_hsum, finsum_eq_sum _ (s.finite_co_support _)] at hg

Premises used: finsum_eq_sum, HahnSeries.SummableFamily.coeff_hsum, HahnSeries.mem_support, HahnSeries.SummableFamily.finite_co_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 : Γ
hg :
  Ne.{u_3 + 1} (α := R)
    (∑
      i ∈
        Set.Finite.toFinset (s :=
          Function.support.{u_5, u_3} (M := R) fun (a : α) ↦ HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) ⋯,
      HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)
    0
obtain :
  ∀
    a ∈
      Set.Finite.toFinset (s :=
        Function.support.{u_5, u_3} (M := R) fun (a : α) ↦ HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) ⋯,
    ∀ (h2 : Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) 0),
      Membership.mem (γ := Set Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) g
⊢ Membership.mem (γ := Set Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) g

Tactic:
obtain ⟨a, _, h2⟩ := 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 : Γ
hg :
  Ne.{u_3 + 1} (α := R)
    (∑
      i ∈
        Set.Finite.toFinset (s :=
          Function.support.{u_5, u_3} (M := R) fun (a : α) ↦ HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) ⋯,
      HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)
    0
a : α
left :
  a ∈
    Set.Finite.toFinset (s :=
      Function.support.{u_5, u_3} (M := R) fun (a : α) ↦ HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) ⋯
h2 : Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) 0
rw : ∃ (i : α), Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) i)) g
⊢ Membership.mem (γ := Set Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) g

Tactic:
rw [Set.mem_iUnion]

Premises used: Set.mem_iUnion
-- 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 : Γ
hg :
  Ne.{u_3 + 1} (α := R)
    (∑
      i ∈
        Set.Finite.toFinset (s :=
          Function.support.{u_5, u_3} (M := R) fun (a : α) ↦ HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) ⋯,
      HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)
    0
a : α
left :
  a ∈
    Set.Finite.toFinset (s :=
      Function.support.{u_5, u_3} (M := R) fun (a : α) ↦ HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) ⋯
h2 : Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) 0
⊢ ∃ (i : α), Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) i)) g

Tactic:
⟨a, h2⟩

Premises used: Exists.intro
-- 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 : Γ
hg :
  Ne.{u_3 + 1} (α := R)
    (∑
      i ∈
        Set.Finite.toFinset (s :=
          Function.support.{u_5, u_3} (M := R) fun (a : α) ↦ HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) ⋯,
      HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)
    0
a : α
left :
  a ∈
    Set.Finite.toFinset (s :=
      Function.support.{u_5, u_3} (M := R) fun (a : α) ↦ HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) ⋯
h2 : Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) 0
⊢ ∃ (i : α), Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) i)) g

Tactic:
exact ⟨a, h2⟩
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s t : SummableFamily Γ R α
coeff : ∀ (g : Γ), (s + t).hsum.coeff g = (s.hsum + t.hsum).coeff g
⊢ (s + t).hsum = s.hsum + t.hsum

Tactic:
ext g
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s t : SummableFamily Γ R α
g : Γ
coeff :
  ∑ᶠ (i : α),
      HAdd.hAdd (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g) (HahnSeries.coeff ((t : (a : α) → R⟦Γ⟧) i) g) =
    HAdd.hAdd (α := R) (∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)
      (∑ᶠ (i : α), HahnSeries.coeff ((t : (a : α) → R⟦Γ⟧) i) g)
⊢ (s + t).hsum.coeff g = (s.hsum + t.hsum).coeff g

Tactic:
simp only [coeff_hsum, coeff_add, add_apply]

Premises used: HahnSeries.SummableFamily.add_apply, HahnSeries.coeff_add, HahnSeries.SummableFamily.coeff_hsum
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s t : SummableFamily Γ R α
g : Γ
⊢ ∑ᶠ (i : α),
      HAdd.hAdd (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g) (HahnSeries.coeff ((t : (a : α) → R⟦Γ⟧) i) g) =
    HAdd.hAdd (α := R) (∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)
      (∑ᶠ (i : α), HahnSeries.coeff ((t : (a : α) → R⟦Γ⟧) i) g)

Tactic:
finsum_add_distrib (s.finite_co_support _) (t.finite_co_support _)

Premises used: finsum_add_distrib, HahnSeries.SummableFamily.finite_co_support
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s t : SummableFamily Γ R α
g : Γ
⊢ ∑ᶠ (i : α),
      HAdd.hAdd (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g) (HahnSeries.coeff ((t : (a : α) → R⟦Γ⟧) i) g) =
    HAdd.hAdd (α := R) (∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)
      (∑ᶠ (i : α), HahnSeries.coeff ((t : (a : α) → R⟦Γ⟧) i) g)

Tactic:
exact finsum_add_distrib (s.finite_co_support _) (t.finite_co_support _)

Premises used: finsum_add_distrib, HahnSeries.SummableFamily.finite_co_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 : Γ
t : Finset α
h : {a : α | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) 0} ⊆ (↑t : Set α)
simp :
  Eq.{u_3 + 1} (α := R)
    (∑
      i ∈
        Set.Finite.toFinset (s :=
          Function.support.{u_5, u_3} (M := R) fun (a : α) ↦ HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) ⋯,
      HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)
    (∑ i ∈ t, HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)
⊢ s.hsum.coeff g = ∑ i ∈ t, HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g

Tactic:
simp only [coeff_hsum, finsum_eq_sum _ (s.finite_co_support _)]

Premises used: finsum_eq_sum, HahnSeries.SummableFamily.coeff_hsum, HahnSeries.SummableFamily.finite_co_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 : Γ
t : Finset α
h : {a : α | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) 0} ⊆ (↑t : Set α)
⊢ ∀ x ∈ t,
    x ∉
        Set.Finite.toFinset (s :=
          Function.support.{u_5, u_3} (M := R) fun (a : α) ↦ HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) ⋯ →
      Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) x) g) 0

Tactic:
simp
-- 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 : Γ
t : Finset α
h : {a : α | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) 0} ⊆ (↑t : Set α)
⊢ Eq.{u_3 + 1} (α := R)
    (∑
      i ∈
        Set.Finite.toFinset (s :=
          Function.support.{u_5, u_3} (M := R) fun (a : α) ↦ HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) ⋯,
      HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)
    (∑ i ∈ t, HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)

Tactic:
exact sum_subset (Set.Finite.toFinset_subset.mpr h) (by simp)

Premises used: Iff.mpr, Set.Finite.toFinset_subset, Finset.sum_subset
-- 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 : Γ
⊢ s.hsum.coeff g = ∑ i ∈ (s.coeff g).support, HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g

Tactic:
simp only [coeff_hsum, finsum_eq_sum _ (s.finite_co_support _), coeff_support]

Premises used: finsum_eq_sum, HahnSeries.SummableFamily.coeff_support, HahnSeries.SummableFamily.coeff_hsum, 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
ι : Type u_7
inst_2 : DecidableEq ι
i : ι
x : R⟦Γ⟧
⊢ Set.IsPWO.{u_1} (α := Γ) (support.{u_1, u_3} (R := R) (Pi.single (M := fun (x : ι) ↦ R⟦Γ⟧) i x i))

Tactic:
simp
-- 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 : DecidableEq ι
i : ι
x : R⟦Γ⟧
⊢ Set.IsPWO.{u_1} (α := Γ) (support.{u_1, u_3} (R := R) (Pi.single (M := fun (x : ι) ↦ R⟦Γ⟧) i x i))

Tactic:
have : (Pi.single (M := fun _ ↦ R⟦Γ⟧) i x i).support.IsPWO := by simp
-- 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 : DecidableEq ι
i : ι
x : R⟦Γ⟧
this : Set.IsPWO.{u_1} (α := Γ) (support.{u_1, u_3} (R := R) (Pi.single (M := fun (x : ι) ↦ R⟦Γ⟧) i x i))
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (a : ι), support.{u_1, u_3} (R := R) (Pi.single (M := fun (a : ι) ↦ R⟦Γ⟧) i x a))

Tactic:
this.mono <| Set.iUnion_subset fun a => ?_

Premises used: Set.iUnion_subset, 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
ι : Type u_7
inst_2 : DecidableEq ι
i : ι
x : R⟦Γ⟧
this : Set.IsPWO.{u_1} (α := Γ) (support.{u_1, u_3} (R := R) (Pi.single (M := fun (x : ι) ↦ R⟦Γ⟧) i x i))
refine :
  ∀ (a : ι),
    Subset.{u_1} (α := Set Γ) (support.{u_1, u_3} (R := R) (Pi.single (M := fun (a : ι) ↦ R⟦Γ⟧) i x a))
      (support.{u_1, u_3} (R := R) (Pi.single (M := fun (x : ι) ↦ R⟦Γ⟧) i x i))
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (a : ι), support.{u_1, u_3} (R := R) (Pi.single (M := fun (a : ι) ↦ R⟦Γ⟧) i x a))

Tactic:
refine this.mono <| Set.iUnion_subset fun a => ?_

Premises used: Set.iUnion_subset, 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
ι : Type u_7
inst_2 : DecidableEq ι
i : ι
x : R⟦Γ⟧
this : Set.IsPWO.{u_1} (α := Γ) (support.{u_1, u_3} (R := R) (Pi.single (M := fun (x : ι) ↦ R⟦Γ⟧) i x i))
a : ι
inl :
  ∀ (this : Set.IsPWO.{u_1} (α := Γ) (support.{u_1, u_3} (R := R) (Pi.single (M := fun (x : ι) ↦ R⟦Γ⟧) a x a))),
    Subset.{u_1} (α := Set Γ) (support.{u_1, u_3} (R := R) (Pi.single (M := fun (a : ι) ↦ R⟦Γ⟧) a x a))
      (support.{u_1, u_3} (R := R) (Pi.single (M := fun (a : ι) ↦ R⟦Γ⟧) a x a))
inr :
  ∀ (ha : a ≠ i),
    Subset.{u_1} (α := Set Γ) (support.{u_1, u_3} (R := R) (Pi.single (M := fun (a : ι) ↦ R⟦Γ⟧) i x a))
      (support.{u_1, u_3} (R := R) (Pi.single (M := fun (x : ι) ↦ R⟦Γ⟧) i x i))
⊢ Subset.{u_1} (α := Set Γ) (support.{u_1, u_3} (R := R) (Pi.single (M := fun (a : ι) ↦ R⟦Γ⟧) i x a))
    (support.{u_1, u_3} (R := R) (Pi.single (M := fun (x : ι) ↦ R⟦Γ⟧) i x i))

Tactic:
obtain rfl | ha := eq_or_ne a i

Premises used: eq_or_ne, 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
ι : Type u_7
inst_2 : DecidableEq ι
x : R⟦Γ⟧
a : ι
this : Set.IsPWO.{u_1} (α := Γ) (support.{u_1, u_3} (R := R) (Pi.single (M := fun (x : ι) ↦ R⟦Γ⟧) a x a))
⊢ Subset.{u_1} (α := Set Γ) (support.{u_1, u_3} (R := R) (Pi.single (M := fun (a : ι) ↦ R⟦Γ⟧) a x a))
    (support.{u_1, u_3} (R := R) (Pi.single (M := fun (a : ι) ↦ R⟦Γ⟧) a x a))

Tactic:
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
ι : Type u_7
inst_2 : DecidableEq ι
i : ι
x : R⟦Γ⟧
this : Set.IsPWO.{u_1} (α := Γ) (support.{u_1, u_3} (R := R) (Pi.single (M := fun (x : ι) ↦ R⟦Γ⟧) i x i))
a : ι
ha : a ≠ i
⊢ Subset.{u_1} (α := Set Γ) (support.{u_1, u_3} (R := R) (Pi.single (M := fun (a : ι) ↦ R⟦Γ⟧) i x a))
    (support.{u_1, u_3} (R := R) (Pi.single (M := fun (x : ι) ↦ R⟦Γ⟧) i x i))

Tactic:
simp [ha]
-- 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 : DecidableEq ι
i : ι
x : R⟦Γ⟧
g : Γ
j : ι
inl :
  Membership.mem (γ := Set ι)
      {a : ι | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff (Pi.single (M := fun (a : ι) ↦ R⟦Γ⟧) j x a) g) 0} j →
    Membership.mem (γ := Set ι) {j} j
inr :
  ∀ (ha : j ≠ i),
    Membership.mem (γ := Set ι)
        {a : ι | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff (Pi.single (M := fun (a : ι) ↦ R⟦Γ⟧) i x a) g) 0} j →
      Membership.mem (γ := Set ι) {i} j
⊢ Membership.mem (γ := Set ι)
      {a : ι | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff (Pi.single (M := fun (a : ι) ↦ R⟦Γ⟧) i x a) g) 0} j →
    Membership.mem (γ := Set ι) {i} j

Tactic:
obtain rfl | ha := eq_or_ne j i

Premises used: eq_or_ne, 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
ι : Type u_7
inst_2 : DecidableEq ι
x : R⟦Γ⟧
g : Γ
j : ι
⊢ Membership.mem (γ := Set ι)
      {a : ι | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff (Pi.single (M := fun (a : ι) ↦ R⟦Γ⟧) j x a) g) 0} j →
    Membership.mem (γ := Set ι) {j} j

Tactic:
simp [*]
-- 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 : DecidableEq ι
i : ι
x : R⟦Γ⟧
g : Γ
j : ι
ha : j ≠ i
⊢ Membership.mem (γ := Set ι)
      {a : ι | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff (Pi.single (M := fun (a : ι) ↦ R⟦Γ⟧) i x a) g) 0} j →
    Membership.mem (γ := Set ι) {i} j

Tactic:
simp [*]
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
ι : Type u_7
inst_2 : DecidableEq ι
i : ι
x : R⟦Γ⟧
coeff : ∀ (g : Γ), (single i x).hsum.coeff g = x.coeff g
⊢ (single i x).hsum = x

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 : DecidableEq ι
i : ι
x : R⟦Γ⟧
g : Γ
coeff : ∀ (x_1 : ι), x_1 ≠ i → Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((single i x : (a : ι) → R⟦Γ⟧) x_1) g) 0
⊢ (single i x).hsum.coeff g = x.coeff g

Tactic:
rw [coeff_hsum, finsum_eq_single _ i, single_toFun, Pi.single_eq_same]

Premises used: HahnSeries.SummableFamily.single_toFun, HahnSeries.SummableFamily.coeff_hsum, Pi.single_eq_same, finsum_eq_single
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
ι : Type u_7
inst_2 : DecidableEq ι
i : ι
x : R⟦Γ⟧
g : Γ
⊢ ∀ (x_1 : ι), x_1 ≠ i → Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((single i x : (a : ι) → R⟦Γ⟧) x_1) g) 0

Tactic:
simp +contextual
-- 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⟦Γ⟧
inl : IsEmpty ι → Set.IsPWO.{u_1} (α := Γ) (⋃ (a : ι), x.support)
inr : Nonempty ι → Set.IsPWO.{u_1} (α := Γ) (⋃ (a : ι), x.support)
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (a : ι), x.support)

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- 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 : IsEmpty ι
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (a : ι), x.support)

Tactic:
simp