awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s t : SummableFamily Γ R α
g : Γ
⊢ (s + t).hsum.coeff g = (s.hsum + t.hsum).coeff g
have 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)
Tactic: simp only [coeff_hsum, coeff_add, add_apply]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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 α)
⊢ s.hsum.coeff g = ∑ i ∈ t, HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g
have 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) sorry,
    HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)
  (∑ i ∈ t, HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)
Tactic: simp only [coeff_hsum, finsum_eq_sum _ (s.finite_co_support _)]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (hypothesis)
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} (α := Γ) (⋃ (a : ι), support.{u_1, u_3} (R := R) (Pi.single (M := fun (a : ι) ↦ R⟦Γ⟧) i x a))
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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))
have 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))
Tactic: refine this.mono <| Set.iUnion_subset fun a => ?_
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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 : ι
⊢ 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))
have 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))
Tactic: obtain rfl | ha := eq_or_ne a i
Cleared hypotheses: i, this
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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))
⊢ 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))
have 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))
Tactic: obtain rfl | ha := eq_or_ne a i
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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 : ι
⊢ 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
have 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
Tactic: obtain rfl | ha := eq_or_ne j i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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
⊢ 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
have 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
Tactic: obtain rfl | ha := eq_or_ne j i
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
ι : Type u_7
inst_2 : DecidableEq ι
i : ι
x : R⟦Γ⟧
⊢ (single i x).hsum = x
have coeff : ∀ (g : Γ), (single i x).hsum.coeff g = x.coeff g
Tactic: ext g
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
ι : Type u_7
inst_2 : DecidableEq ι
i : ι
x : R⟦Γ⟧
g : Γ
⊢ (single i x).hsum.coeff g = x.coeff g
have coeff : ∀ (x_1 : ι), x_1 ≠ i → Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((single i x : (a : ι) → R⟦Γ⟧) x_1) g) 0
Tactic: rw [coeff_hsum, finsum_eq_single _ i, single_toFun, Pi.single_eq_same]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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⟦Γ⟧
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (a : ι), x.support)
have inl : IsEmpty ι → Set.IsPWO.{u_1} (α := Γ) (⋃ (a : ι), x.support)
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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)
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (a : ι), x.support)
have inr : Nonempty ι → Set.IsPWO.{u_1} (α := Γ) (⋃ (a : ι), x.support)
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
ι : Type u_7
inst_2 : Unique ι
x : SummableFamily Γ R ι
⊢ x.hsum = (x : (a : ι) → R⟦Γ⟧) default
have coeff : ∀ (g : Γ), x.hsum.coeff g = HahnSeries.coeff ((x : (a : ι) → R⟦Γ⟧) default) g
Tactic: ext g
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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)))
have 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
Tactic: refine Set.IsPWO.mono s.isPWO_iUnion_support fun g => ?_
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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 : Γ
⊢ 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
have 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
Tactic: simp only [Set.mem_iUnion, mem_support, ne_eq, forall_exists_index]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
e : α ≃ β
s : SummableFamily Γ R α
⊢ (Equiv e s).hsum = s.hsum
have coeff : ∀ (g : Γ), (Equiv e s).hsum.coeff g = s.hsum.coeff g
Tactic: ext g
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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 : Γ
⊢ (Equiv e s).hsum.coeff g = s.hsum.coeff g
have 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)
Tactic: simp only [coeff_hsum, Equiv_toFun]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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)
have 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
Tactic: refine Set.IsPWO.mono s.isPWO_iUnion_support fun g hg => ?_
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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
⊢ Membership.mem (γ := Set Γ) (⋃ (a : α), support.{u_1, u_4} (R := V) ((s : (a : α) → V⟦Γ⟧) a)) g
have 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
Tactic: simp_all only [Set.mem_iUnion, mem_support, coeff_smul, ne_eq]
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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
⊢ ∃ (i : α), ¬Eq.{u_4 + 1} (α := V) (HahnSeries.coeff ((s : (a : α) → V⟦Γ⟧) i) g) 0
have 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
Tactic: obtain ⟨i, hi⟩ := hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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}
have 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
Tactic: refine Set.Finite.subset (s.finite_co_support g) fun i hi => ?_
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (hypothesis)
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
⊢ Membership.mem (γ := Set α)
    (Function.support.{u_5, u_4} (M := V) fun (a : α) ↦ HahnSeries.coeff ((s : (a : α) → V⟦Γ⟧) a) g) i
have hi₁ : ¬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]
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (hypothesis)
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
⊢ g ≤ g'
have hg'₁ : 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'
Cleared hypotheses: hg'
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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
⊢ g ≤ g'
have obtain : ∀ i ∈ (s.coeff g').support, ∀ (hi : Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g') 0), g ≤ g'
Tactic: obtain ⟨i, _, hi⟩ := Finset.exists_ne_zero_of_sum_ne_zero hg'
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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.coeff g = HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g
have rw : Eq.{u_3 + 1} (α := R) (∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)
  (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g)
Tactic: rw [coeff_hsum, finsum_eq_single (fun i ↦ (s i).coeff g) a
    hna]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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)
⊢ s.hsum.coeff g = HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g
have rw₁ : Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g)
Tactic: rw [coeff_hsum, finsum_eq_single (fun i ↦ (s i).coeff g) a
    hna]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (hypothesis)
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.leadingCoeff = HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g
have this : s.hsum.orderTop = (↑g : WithTop Γ)
Tactic: have := hsum_orderTop_of_le ha hg hna
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (hypothesis)
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 Γ)
⊢ s.hsum.leadingCoeff = HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g
have this₁ : (if h : s.hsum = 0 then ⊤ else (↑(sorry.min (s := s.hsum.support) sorry) : WithTop Γ)) = (↑g : WithTop Γ)
Tactic: rw [orderTop] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (hypothesis)
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.leadingCoeff = HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g
have hs : s.hsum ≠ 0
Tactic: have hs : s.hsum ≠ 0 := by
    by_contra h
    simp [h] at this
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (hypothesis)
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
⊢ s.hsum.leadingCoeff = HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g
have this₁ : sorry.min (s := s.hsum.support) sorry = g
Tactic: simp only [hs, ↓reduceDIte, WithTop.coe_eq_coe] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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
⊢ s.hsum.leadingCoeff = HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g
have simp : Eq.{u_3 + 1} (α := R) (∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)
  (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g)
Tactic: simp only [leadingCoeff_of_ne_zero hs, coeff_hsum, untop_orderTop_of_ne_zero hs, this]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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
⊢ Eq.{u_3 + 1} (α := R) (∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)
    (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g)
have rw : Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g)
Tactic: rw [finsum_eq_single (fun i ↦ (s i).coeff g) a hna]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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))
have simp_rw : Set.IsPWO.{u_1} (α := Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a))
Tactic: simp_rw [support_neg]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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 α
g : Γ
⊢ Set.Finite.{u_5} (α := α) {a : α | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff (-(s : (a : α) → R⟦Γ⟧) a) g) 0}
have simp : Set.Finite.{u_5} (α := α) {a : α | ¬Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) 0}
Tactic: simp only [coeff_neg', Pi.neg_apply, Ne, neg_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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 s' : SummableFamily Γ R α
⊢ Set.IsPWO.{u_1} (α := Γ)
    (⋃ (a : α),
      (HSub.hSub (α := (a : α) → R⟦Γ⟧) (β := (a : α) → R⟦Γ⟧) (⇑s : (a : α) → R⟦Γ⟧) (⇑s' : (a : α) → R⟦Γ⟧) a).support)
have simp_rw : Set.IsPWO.{u_1} (α := Γ)
  (⋃ (a : α),
    (HAdd.hAdd (α := (a : α) → R⟦Γ⟧) (β := (a : α) → R⟦Γ⟧) (⇑s : (a : α) → R⟦Γ⟧) (-(⇑s' : (a : α) → R⟦Γ⟧)) a).support)
Tactic: simp_rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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 s' : SummableFamily Γ R α
g : Γ
⊢ Set.Finite.{u_5} (α := α)
    {a : α |
      (HSub.hSub (α := (a : α) → R⟦Γ⟧) (β := (a : α) → R⟦Γ⟧) (⇑s : (a : α) → R⟦Γ⟧) (⇑s' : (a : α) → R⟦Γ⟧) a).coeff g ≠
        0}
have simp_rw : Set.Finite.{u_5} (α := α)
  {a : α |
    (HAdd.hAdd (α := (a : α) → R⟦Γ⟧) (β := (a : α) → R⟦Γ⟧) (⇑s : (a : α) → R⟦Γ⟧) (-(⇑s' : (a : α) → R⟦Γ⟧)) a).coeff g ≠
      0}
Tactic: simp_rw [sub_eq_add_neg]