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
s : SummableFamily Γ R α
f : α ↪ β
g : Γ
b : β
hb : Membership.mem (γ := Set β) (Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)) b
h :
  ¬Eq.{u_3 + 1} (α := R)
      (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) (Classical.choose (p := fun (x : α) ↦ (f : (a : α) → β) x = b) hb)) g) 0
⊢ Membership.mem (γ := Set β)
    (Set.image.{u_5, u_6} (α := α) (⇑f : (a : α) → β)
      (Function.support.{u_5, u_3} (M := R) fun (a : α) ↦ HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g))
    b

Tactic:
exact ⟨Classical.choose hb, h, Classical.choose_spec hb⟩
-- 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 α
f : α ↪ β
g : Γ
b : β
h :
  Membership.mem (γ := Set β)
    {a : β |
      Ne.{u_3 + 1} (α := R)
        (HahnSeries.coeff
          (if h : Membership.mem (γ := Set β) (Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)) a then
            (s : (a : α) → R⟦Γ⟧) (Classical.choose (p := fun (x : α) ↦ (f : (a : α) → β) x = a) h)
          else 0)
          g)
        0}
    b
hb : b ∉ Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)
⊢ Membership.mem (γ := Set β)
    (Set.image.{u_5, u_6} (α := α) (⇑f : (a : α) → β)
      (Function.support.{u_5, u_3} (M := R) fun (a : α) ↦ HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g))
    b

Tactic:
simp only [Ne, Set.mem_setOf_eq, dif_neg hb, coeff_zero, not_true_eq_false] at h

Premises used: not_true_eq_false, Ne, Set.mem_setOf_eq, dif_neg, HahnSeries.coeff_zero
-- 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
s : SummableFamily Γ R α
f : α ↪ β
b : β
⊢ Eq (α := R⟦Γ⟧) ((s.embDomain f : (a : β) → R⟦Γ⟧) b : R⟦Γ⟧)
    (if h : Membership.mem (γ := Set β) (Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)) b then
        (s : (a : α) → R⟦Γ⟧) (Classical.choose (p := fun (x : α) ↦ (f : (a : α) → β) x = b) h)
      else 0 :
      R⟦Γ⟧)

Tactic:
rfl

Premises used: dite, 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
s : SummableFamily Γ R α
f : α ↪ β
a : α
rw :
  Eq (α := R⟦Γ⟧)
    ((s : (a : α) → R⟦Γ⟧)
        (Classical.choose (p := fun (x : α) ↦ Eq.{u_6 + 1} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) a : β))
          ⋯) :
      R⟦Γ⟧)
    ((s : (a : α) → R⟦Γ⟧) a : R⟦Γ⟧)
⊢ Eq (α := R⟦Γ⟧) ((s.embDomain f : (a : β) → R⟦Γ⟧) ((f : (a : α) → β) a) : R⟦Γ⟧) ((s : (a : α) → R⟦Γ⟧) a : R⟦Γ⟧)

Tactic:
rw [embDomain_apply, dif_pos (Set.mem_range_self a)]

Premises used: Set.mem_range_self, HahnSeries.SummableFamily.embDomain_apply, dif_pos
-- 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
s : SummableFamily Γ R α
f : α ↪ β
a : α
⊢ Eq (α := R⟦Γ⟧)
    ((s : (a : α) → R⟦Γ⟧)
        (Classical.choose (p := fun (x : α) ↦ Eq.{u_6 + 1} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) a : β))
          ⋯) :
      R⟦Γ⟧)
    ((s : (a : α) → R⟦Γ⟧) a : R⟦Γ⟧)

Tactic:
congr rfl (f.injective (Classical.choose_spec (Set.mem_range_self a)))

Premises used: Set.mem_range_self, Classical.choose_spec, congr, Function.Embedding.injective, 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
s : SummableFamily Γ R α
f : α ↪ β
a : α
⊢ Eq (α := R⟦Γ⟧)
    ((s : (a : α) → R⟦Γ⟧)
        (Classical.choose (p := fun (x : α) ↦ Eq.{u_6 + 1} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) a : β))
          ⋯) :
      R⟦Γ⟧)
    ((s : (a : α) → R⟦Γ⟧) a : R⟦Γ⟧)

Tactic:
exact congr rfl (f.injective (Classical.choose_spec (Set.mem_range_self a)))

Premises used: Set.mem_range_self, Classical.choose_spec, congr, Function.Embedding.injective, 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
s : SummableFamily Γ R α
f : α ↪ β
b : β
h : b ∉ Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)
rw :
  Eq (α := R⟦Γ⟧)
    (if h : Membership.mem (γ := Set β) (Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)) b then
      (s : (a : α) → R⟦Γ⟧) (Classical.choose (p := fun (x : α) ↦ (f : (a : α) → β) x = b) h)
    else 0)
    0
rw₁ rw₂ : Eq (α := R⟦Γ⟧) 0 0
⊢ Eq (α := R⟦Γ⟧) ((s.embDomain f : (a : β) → R⟦Γ⟧) b : R⟦Γ⟧) (0 : R⟦Γ⟧)

Tactic:
rw [embDomain_apply, dif_neg h]

Premises used: HahnSeries.SummableFamily.embDomain_apply, dif_neg
-- 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
s : SummableFamily Γ R α
f : α ↪ β
coeff : ∀ (g : Γ), (s.embDomain f).hsum.coeff g = s.hsum.coeff g
⊢ (s.embDomain f).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
s : SummableFamily Γ R α
f : α ↪ β
g : Γ
coeff :
  Eq.{u_3 + 1} (α := R)
    (∑ᶠ (i : β),
      if h : Membership.mem (γ := Set β) (Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)) i then
        HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) (Classical.choose (p := fun (x : α) ↦ (f : (a : α) → β) x = i) ⋯)) g
      else 0)
    (∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)
⊢ (s.embDomain f).hsum.coeff g = s.hsum.coeff g

Tactic:
simp only [coeff_hsum, embDomain_apply, apply_dite HahnSeries.coeff, dite_apply, coeff_zero]

Premises used: HahnSeries.SummableFamily.embDomain_apply, apply_dite, HahnSeries.SummableFamily.coeff_hsum, HahnSeries.coeff, HahnSeries.coeff_zero, dite_apply
-- 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
s : SummableFamily Γ R α
f : α ↪ β
g : Γ
⊢ Eq.{u_3 + 1} (α := R)
    (∑ᶠ (i : β),
      if h : Membership.mem (γ := Set β) (Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)) i then
        HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) (Classical.choose (p := fun (x : α) ↦ (f : (a : α) → β) x = i) ⋯)) g
      else 0)
    (∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)

Tactic:
finsum_emb_domain f fun a => (s a).coeff g

Premises used: finsum_emb_domain, HahnSeries.coeff, 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
s : SummableFamily Γ R α
f : α ↪ β
g : Γ
⊢ Eq.{u_3 + 1} (α := R)
    (∑ᶠ (i : β),
      if h : Membership.mem (γ := Set β) (Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)) i then
        HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) (Classical.choose (p := fun (x : α) ↦ (f : (a : α) → β) x = i) ⋯)) g
      else 0)
    (∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)

Tactic:
exact finsum_emb_domain f fun a => (s a).coeff g

Premises used: finsum_emb_domain, HahnSeries.coeff, 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
s : SummableFamily Γ R α
f : α ↪ β
coeff : ∀ (g : Γ), (s.embDomain f).hsum.coeff g = s.hsum.coeff g
coeff₁ :
  ∀ (g : Γ),
    Eq.{u_3 + 1} (α := R)
      (∑ᶠ (i : β),
        if h : Membership.mem (γ := Set β) (Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)) i then
          HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) (Classical.choose (p := fun (x : α) ↦ (f : (a : α) → β) x = i) ⋯)) g
        else 0)
      (∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)
⊢ (s.embDomain f).hsum = s.hsum

Tactic:
classical
  ext g
  simp only [coeff_hsum, embDomain_apply, apply_dite HahnSeries.coeff, dite_apply, coeff_zero]
  exact finsum_emb_domain f fun a => (s a).coeff g

Premises used: HahnSeries.SummableFamily.embDomain_apply, apply_dite, HahnSeries.SummableFamily.coeff_hsum, HahnSeries.coeff, HahnSeries.coeff_zero, dite_apply
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
g : Γ
hn : g ∈ (HPow.hPow (β := ℕ) x 0).support
⊢ g = 0 ∧ ¬Eq.{u_3 + 1} (α := R) 1 0

Tactic:
simp only [pow_zero, mem_support, coeff_one, ne_eq, ite_eq_right_iff, Classical.not_imp] at hn

Premises used: ne_eq, pow_zero, HahnSeries.coeff_one, ite_eq_right_iff, Classical.not_imp, HahnSeries.mem_support
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
g : Γ
hn : g = 0 ∧ ¬Eq.{u_3 + 1} (α := R) 1 0
zero : Membership.mem (γ := AddSubmonoid Γ) (AddSubmonoid.closure x.support) 0
⊢ g ∈ (↑(AddSubmonoid.closure x.support) : Set Γ)

Tactic:
simp only [hn, SetLike.mem_coe]

Premises used: SetLike.mem_coe
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
g : Γ
hn : g = 0 ∧ ¬Eq.{u_3 + 1} (α := R) 1 0
⊢ Membership.mem (γ := AddSubmonoid Γ) (AddSubmonoid.closure x.support) 0

Tactic:
AddSubmonoid.zero_mem _

Premises used: AddSubmonoid.zero_mem
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
g : Γ
hn : g = 0 ∧ ¬Eq.{u_3 + 1} (α := R) 1 0
⊢ Membership.mem (γ := AddSubmonoid Γ) (AddSubmonoid.closure x.support) 0

Tactic:
exact AddSubmonoid.zero_mem _

Premises used: AddSubmonoid.zero_mem
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
n : ℕ
ih : ∀ ⦃g : Γ⦄ (hn : g ∈ (x ^ n).support), g ∈ (↑(AddSubmonoid.closure x.support) : Set Γ)
g : Γ
hn : g ∈ (x ^ (n + 1)).support
succ :
  ∀ (i : Γ) (hi : i ∈ (npowRec n x).support) (j : Γ) (hj : j ∈ x.support)
    (hn : (fun (x1 x2 : Γ) ↦ x1 + x2) i j ∈ (x ^ (n + 1)).support),
    (fun (x1 x2 : Γ) ↦ x1 + x2) i j ∈ (↑(AddSubmonoid.closure x.support) : Set Γ)
⊢ g ∈ (↑(AddSubmonoid.closure x.support) : Set Γ)

Tactic:
obtain ⟨i, hi, j, hj, rfl⟩ := support_mul_subset hn

Premises used: HahnSeries.support_mul_subset, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
n : ℕ
ih : ∀ ⦃g : Γ⦄ (hn : g ∈ (x ^ n).support), g ∈ (↑(AddSubmonoid.closure x.support) : Set Γ)
i : Γ
hi : i ∈ (npowRec n x).support
j : Γ
hj : j ∈ x.support
hn : (fun (x1 x2 : Γ) ↦ x1 + x2) i j ∈ (x ^ (n + 1)).support
⊢ (fun (x1 x2 : Γ) ↦ x1 + x2) i j ∈ (↑(AddSubmonoid.closure x.support) : Set Γ)

Tactic:
SetLike.mem_coe.2 (AddSubmonoid.add_mem _ (ih hi) (AddSubmonoid.subset_closure hj))

Premises used: AddSubmonoid.add_mem, Iff.mpr, AddSubmonoid.subset_closure, SetLike.mem_coe
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
n : ℕ
ih : ∀ ⦃g : Γ⦄ (hn : g ∈ (x ^ n).support), g ∈ (↑(AddSubmonoid.closure x.support) : Set Γ)
i : Γ
hi : i ∈ (npowRec n x).support
j : Γ
hj : j ∈ x.support
hn : (fun (x1 x2 : Γ) ↦ x1 + x2) i j ∈ (x ^ (n + 1)).support
⊢ (fun (x1 x2 : Γ) ↦ x1 + x2) i j ∈ (↑(AddSubmonoid.closure x.support) : Set Γ)

Tactic:
exact SetLike.mem_coe.2 (AddSubmonoid.add_mem _ (ih hi) (AddSubmonoid.subset_closure hj))

Premises used: AddSubmonoid.add_mem, Iff.mpr, AddSubmonoid.subset_closure, SetLike.mem_coe
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
n : ℕ
g : Γ
hn : g ∈ (x ^ n).support
zero : ∀ ⦃g : Γ⦄ (hn : g ∈ (HPow.hPow (β := ℕ) x 0).support), g ∈ (↑(AddSubmonoid.closure x.support) : Set Γ)
succ :
  ∀ (n : ℕ) (ih : ∀ ⦃g : Γ⦄ (hn : g ∈ (x ^ n).support), g ∈ (↑(AddSubmonoid.closure x.support) : Set Γ)) ⦃g : Γ⦄
    (hn : g ∈ (x ^ (n + 1)).support), g ∈ (↑(AddSubmonoid.closure x.support) : Set Γ)
⊢ g ∈ (↑(AddSubmonoid.closure x.support) : Set Γ)

Tactic:
induction n generalizing g with
  | zero =>
    simp only [pow_zero, mem_support, coeff_one, ne_eq, ite_eq_right_iff, Classical.not_imp] at hn
    simp only [hn, SetLike.mem_coe]
    exact AddSubmonoid.zero_mem _
  | succ n ih =>
    obtain ⟨i, hi, j, hj, rfl⟩ := support_mul_subset hn
    exact SetLike.mem_coe.2 (AddSubmonoid.add_mem _ (ih hi) (AddSubmonoid.subset_closure hj))

Premises used: AddSubmonoid.zero_mem, ne_eq, pow_zero, HahnSeries.coeff_one, ite_eq_right_iff, Classical.not_imp, SetLike.mem_coe, HahnSeries.support_mul_subset, rfl, HahnSeries.mem_support
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
hx : 0 ≤ x.order
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (n : ℕ), (x ^ n).support)

Tactic:
(x.isPWO_support'.addSubmonoid_closure
    fun _ hg => le_trans hx (order_le_of_coeff_ne_zero (Function.mem_support.mp hg))).mono
    (Set.iUnion_subset fun n => support_pow_subset_closure x n)

Premises used: Set.IsPWO.addSubmonoid_closure, Set.iUnion_subset, HahnSeries.SummableFamily.support_pow_subset_closure, HahnSeries.isPWO_support', HahnSeries.order_le_of_coeff_ne_zero, Iff.mp, Function.mem_support, Set.IsPWO.mono, le_trans
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
g : Γ
n : ℕ
hn : ¬(HPow.hPow (α := R⟦Γ⟧) 0 n).coeff g = 0
by_contra : ∀ (h' : ¬n = 0), False
⊢ n = 0

Tactic:
by_contra h'
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
g : Γ
n : ℕ
hn : ¬(HPow.hPow (α := R⟦Γ⟧) 0 n).coeff g = 0
h' : ¬n = 0
⊢ False

Tactic:
simp_all only [ne_eq, not_false_eq_true, zero_pow, coeff_zero, not_true_eq_false]

Premises used: not_true_eq_false, ne_eq, HahnSeries.coeff_zero, not_false_eq_true, zero_pow
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (n : ℕ), (x ^ n).support)

Tactic:
have hpwo : Set.IsPWO (⋃ n, support (x ^ n)) :=
    isPWO_iUnion_support_powers (zero_le_orderTop_iff.mp <| le_of_lt hx)
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : Set.IsPWO.{u_1} (α := Γ) (⋃ (n : ℕ), (x ^ n).support)
pos :
  ∀ (h0 : x = 0), Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) g) 0}
neg :
  ∀ (h0 : ¬x = 0), Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) g) 0}
⊢ Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) g) 0}

Tactic:
by_cases h0 : x = 0
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : Set.IsPWO.{u_1} (α := Γ) (⋃ (n : ℕ), (x ^ n).support)
h0 : x = 0
⊢ Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) g) 0}

Tactic:
h0 ▸ Set.Finite.subset (Set.finite_singleton 0) (co_support_zero g)

Premises used: HahnSeries.SummableFamily.co_support_zero, Eq.rec, Set.Finite.subset, OfNat.ofNat, Eq.symm, Set.finite_singleton
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : Set.IsPWO.{u_1} (α := Γ) (⋃ (n : ℕ), (x ^ n).support)
h0 : x = 0
⊢ Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) g) 0}

Tactic:
exact h0 ▸ Set.Finite.subset (Set.finite_singleton 0) (co_support_zero g)
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : Set.IsPWO.{u_1} (α := Γ) (⋃ (n : ℕ), (x ^ n).support)
h0 : ¬x = 0
pos :
  ∀ (hg : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), {g : Γ | (x ^ n).coeff g ≠ 0}) g),
    Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) g) 0}
neg :
  ∀ (hg : g ∉ ⋃ (n : ℕ), {g : Γ | (x ^ n).coeff g ≠ 0}),
    Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) g) 0}
⊢ Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) g) 0}

Tactic:
by_cases hg : g ∈ ⋃ n : ℕ, { g | (x ^ n).coeff g ≠ 0 }
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : Set.IsPWO.{u_1} (α := Γ) (⋃ (n : ℕ), (x ^ n).support)
h0 : ¬x = 0
hg : g ∉ ⋃ (n : ℕ), {g : Γ | (x ^ n).coeff g ≠ 0}
⊢ Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) g) 0}

Tactic:
Set.finite_empty.subset fun n hn => hg (Set.mem_iUnion.2 ⟨n, hn⟩)

Premises used: Iff.mpr, Set.finite_empty, Set.mem_iUnion, Set.Finite.subset, Exists.intro
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : Set.IsPWO.{u_1} (α := Γ) (⋃ (n : ℕ), (x ^ n).support)
h0 : ¬x = 0
hg : g ∉ ⋃ (n : ℕ), {g : Γ | (x ^ n).coeff g ≠ 0}
⊢ Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) g) 0}

Tactic:
exact Set.finite_empty.subset fun n hn => hg (Set.mem_iUnion.2 ⟨n, hn⟩)

Premises used: Iff.mpr, Set.finite_empty, Set.mem_iUnion, Set.Finite.subset, Exists.intro
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : Set.IsPWO.{u_1} (α := Γ) (⋃ (n : ℕ), (x ^ n).support)
h0 : ¬x = 0
hg : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), {g : Γ | (x ^ n).coeff g ≠ 0}) g
pos :
  ∀ (y : Γ),
    Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) y →
      (∀ (z : Γ),
          Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) z →
            z < y →
              Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) z) 0}) →
        Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) y) 0}
⊢ Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) g) 0}

Tactic:
apply hpwo.isWF.induction hg

Premises used: Set.IsPWO.isWF, Set.WellFoundedOn.induction
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : Set.IsPWO.{u_1} (α := Γ) (⋃ (n : ℕ), (x ^ n).support)
h0 : ¬x = 0
hg : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), {g : Γ | (x ^ n).coeff g ≠ 0}) g
y : Γ
ys : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) y
hy :
  ∀ (z : Γ),
    Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) z →
      z < y → Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) z) 0}
⊢ Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) y) 0}

Tactic:
((((addAntidiagonal x.isPWO_support hpwo y).finite_toSet.biUnion
    fun ij hij => hy ij.snd (mem_addAntidiagonal.1 (mem_coe.1 hij)).2.1 ?_).image Nat.succ).union
      (Set.finite_singleton 0)).subset ?_

Premises used: Set.Finite.union, HahnSeries.isPWO_support, Set.Finite.subset, Set.Finite.image, And.right, And.left, Iff.mp, Finset.addAntidiagonal, Finset.finite_toSet, Set.Finite.biUnion, OfNat.ofNat, Nat.succ, Prod.snd, Set.finite_singleton, Finset.mem_coe, Finset.mem_addAntidiagonal
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : Set.IsPWO.{u_1} (α := Γ) (⋃ (n : ℕ), (x ^ n).support)
h0 : ¬x = 0
hg : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), {g : Γ | (x ^ n).coeff g ≠ 0}) g
y : Γ
ys : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) y
hy :
  ∀ (z : Γ),
    Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) z →
      z < y → Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) z) 0}
pos :
  ∀ (ij : Γ × Γ)
    (hij : ij ∈ (↑(addAntidiagonal (s := x.support) (t := ⋃ (n : ℕ), (x ^ n).support) ⋯ hpwo y) : Set (Γ × Γ))),
    ij.2 < y
pos₁ :
  {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) y) 0} ⊆
    (Nat.succ ''
        ⋃ i ∈ (↑(addAntidiagonal (s := x.support) (t := ⋃ (n : ℕ), (x ^ n).support) ⋯ hpwo y) : Set (Γ × Γ)),
          {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) i.2) 0}) ∪
      {0}
⊢ Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) y) 0}

Tactic:
refine ((((addAntidiagonal x.isPWO_support hpwo y).finite_toSet.biUnion
    fun ij hij => hy ij.snd (mem_addAntidiagonal.1 (mem_coe.1 hij)).2.1 ?_).image Nat.succ).union
      (Set.finite_singleton 0)).subset ?_

Premises used: Set.Finite.union, HahnSeries.isPWO_support, Set.Finite.subset, Set.Finite.image, And.right, And.left, Iff.mp, Finset.addAntidiagonal, Finset.finite_toSet, Set.Finite.biUnion, OfNat.ofNat, Nat.succ, Prod.snd, Set.finite_singleton, Finset.mem_coe, Finset.mem_addAntidiagonal
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : Set.IsPWO.{u_1} (α := Γ) (⋃ (n : ℕ), (x ^ n).support)
h0 : ¬x = 0
hg : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), {g : Γ | (x ^ n).coeff g ≠ 0}) g
y : Γ
ys : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) y
hy :
  ∀ (z : Γ),
    Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) z →
      z < y → Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) z) 0}
ij : Γ × Γ
hij : ij ∈ (↑(addAntidiagonal (s := x.support) (t := ⋃ (n : ℕ), (x ^ n).support) ⋯ hpwo y) : Set (Γ × Γ))
pos :
  ∀ (hi : ij.1 ∈ x.support),
    Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) ij.2 →
      ∀ (ys : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) (ij.1 + ij.2))
        (hy :
          ∀ (z : Γ),
            Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) z →
              z < ij.1 + ij.2 →
                Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) z) 0})
        (hij :
          ij ∈
            (↑(addAntidiagonal (s := x.support) (t := ⋃ (n : ℕ), (x ^ n).support) ⋯ hpwo (ij.1 + ij.2)) : Set (Γ × Γ))),
        ij.2 < ij.1 + ij.2
⊢ ij.2 < y

Tactic:
obtain ⟨hi, _, rfl⟩ := mem_addAntidiagonal.1 (mem_coe.1 hij)

Premises used: Iff.mp, Finset.mem_coe, rfl, Finset.mem_addAntidiagonal