awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
s : SummableFamily Γ R α
t : SummableFamily Γ R β
g : Γ
simp_rw :
  (s.smul t).hsum.coeff g =
    ∑
      x ∈
        addAntidiagonal (s := ⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
          ⋃ (a : β), support.{u_1, u_3} (R := R) ((t : (a : β) → R⟦Γ⟧) a)) ⋯ ⋯ g,
      s.hsum.coeff x.1 • t.hsum.coeff x.2
⊢ (s.mul t).hsum.coeff g =
    ∑
      gh ∈
        addAntidiagonal (s := ⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
          ⋃ (a : β), support.{u_1, u_3} (R := R) ((t : (a : β) → R⟦Γ⟧) a)) ⋯ ⋯ g,
      s.hsum.coeff gh.1 * t.hsum.coeff gh.2

Tactic:
simp_rw [← smul_eq_mul, mul_eq_smul]

Premises used: smul_eq_mul, HahnSeries.SummableFamily.mul_eq_smul
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
s : SummableFamily Γ R α
t : SummableFamily Γ R β
g : Γ
⊢ (s.smul t).hsum.coeff g =
    ∑
      x ∈
        addAntidiagonal (s := ⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
          ⋃ (a : β), support.{u_1, u_3} (R := R) ((t : (a : β) → R⟦Γ⟧) a)) ⋯ ⋯ g,
      s.hsum.coeff x.1 • t.hsum.coeff x.2

Tactic:
coeff_smul s t g

Premises used: Set.addAntidiagonal, setOf, HahnSeries.SummableFamily.coeff_smul, Finset.addAntidiagonal
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
s : SummableFamily Γ R α
t : SummableFamily Γ R β
g : Γ
⊢ (s.smul t).hsum.coeff g =
    ∑
      x ∈
        addAntidiagonal (s := ⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
          ⋃ (a : β), support.{u_1, u_3} (R := R) ((t : (a : β) → R⟦Γ⟧) a)) ⋯ ⋯ g,
      s.hsum.coeff x.1 • t.hsum.coeff x.2

Tactic:
exact coeff_smul s t g

Premises used: HahnSeries.SummableFamily.coeff_smul
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
s : SummableFamily Γ R α
t : SummableFamily Γ R β
rw : (s.smul t).hsum = s.hsum • t.hsum
⊢ (s.mul t).hsum = s.hsum * t.hsum

Tactic:
rw [← smul_eq_mul, mul_eq_smul]

Premises used: smul_eq_mul, HahnSeries.SummableFamily.mul_eq_smul
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
s : SummableFamily Γ R α
t : SummableFamily Γ R β
⊢ (s.smul t).hsum = s.hsum • t.hsum

Tactic:
smul_hsum s t

Premises used: HahnSeries.SummableFamily.smul_hsum
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
s : SummableFamily Γ R α
t : SummableFamily Γ R β
⊢ (s.smul t).hsum = s.hsum • t.hsum

Tactic:
exact smul_hsum s t

Premises used: HahnSeries.SummableFamily.smul_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
f : α →₀ R⟦Γ⟧
apply :
  Subset.{u_1} (α := Set Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((f : (a : α) → R⟦Γ⟧) a))
    (⋃ i ∈ f.support, support.{u_1, u_3} (R := R) ((f : (a : α) → R⟦Γ⟧) i))
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((f : (a : α) → R⟦Γ⟧) a))

Tactic:
apply (f.support.isPWO_bUnion.2 fun a _ => (f a).isPWO_support).mono

Premises used: Iff.mpr, HahnSeries.isPWO_support, Finsupp.support, Finset.isPWO_bUnion, Set.IsPWO.mono, 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
f : α →₀ R⟦Γ⟧
⊢ Subset.{u_1} (α := Set Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((f : (a : α) → R⟦Γ⟧) a))
    (⋃ i ∈ f.support, support.{u_1, u_3} (R := R) ((f : (a : α) → R⟦Γ⟧) i))

Tactic:
Set.iUnion_subset_iff.2 fun a g hg => ?_

Premises used: Iff.mpr, Set.iUnion_subset_iff
-- 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
f : α →₀ R⟦Γ⟧
refine :
  ∀ (a : α) (g : Γ) (hg : Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((f : (a : α) → R⟦Γ⟧) a)) g),
    Membership.mem (γ := Set Γ) (⋃ i ∈ f.support, support.{u_1, u_3} (R := R) ((f : (a : α) → R⟦Γ⟧) i)) g
⊢ Subset.{u_1} (α := Set Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((f : (a : α) → R⟦Γ⟧) a))
    (⋃ i ∈ f.support, support.{u_1, u_3} (R := R) ((f : (a : α) → R⟦Γ⟧) i))

Tactic:
refine Set.iUnion_subset_iff.2 fun a g hg => ?_

Premises used: Iff.mpr, Set.iUnion_subset_iff
-- 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
f : α →₀ R⟦Γ⟧
a : α
g : Γ
hg : Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((f : (a : α) → R⟦Γ⟧) a)) g
rw : Set.Nonempty.{u_1} (α := Γ) (support.{u_1, u_3} (R := R) ((f : (a : α) → R⟦Γ⟧) a))
⊢ a ∈ f.support

Tactic:
rw [Finsupp.mem_support_iff, ← support_nonempty_iff]

Premises used: Finsupp.mem_support_iff, HahnSeries.support_nonempty_iff
-- 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
f : α →₀ R⟦Γ⟧
a : α
g : Γ
hg : Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((f : (a : α) → R⟦Γ⟧) a)) g
⊢ Set.Nonempty.{u_1} (α := Γ) (support.{u_1, u_3} (R := R) ((f : (a : α) → R⟦Γ⟧) a))

Tactic:
⟨g, hg⟩

Premises used: Set.Nonempty, 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
f : α →₀ R⟦Γ⟧
a : α
g : Γ
hg : Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((f : (a : α) → R⟦Γ⟧) a)) g
⊢ Set.Nonempty.{u_1} (α := Γ) (support.{u_1, u_3} (R := R) ((f : (a : α) → R⟦Γ⟧) a))

Tactic:
exact ⟨g, 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
f : α →₀ R⟦Γ⟧
a : α
g : Γ
hg : Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((f : (a : α) → R⟦Γ⟧) a)) g
⊢ a ∈ f.support

Tactic:
have haf : a ∈ f.support := by
      rw [Finsupp.mem_support_iff, ← support_nonempty_iff]
      exact ⟨g, 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
f : α →₀ R⟦Γ⟧
a : α
g : Γ
hg : Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((f : (a : α) → R⟦Γ⟧) a)) g
haf : a ∈ f.support
⊢ Membership.mem (γ := Set Γ) (⋃ i ∈ f.support, support.{u_1, u_3} (R := R) ((f : (a : α) → R⟦Γ⟧) i)) g

Tactic:
Set.mem_biUnion haf hg

Premises used: Set.Mem, Set.mem_biUnion
-- 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
f : α →₀ R⟦Γ⟧
a : α
g : Γ
hg : Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((f : (a : α) → R⟦Γ⟧) a)) g
haf : a ∈ f.support
⊢ Membership.mem (γ := Set Γ) (⋃ i ∈ f.support, support.{u_1, u_3} (R := R) ((f : (a : α) → R⟦Γ⟧) i)) g

Tactic:
exact Set.mem_biUnion haf hg

Premises used: Set.mem_biUnion
-- 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
f : α →₀ R⟦Γ⟧
g : Γ
⊢ Set.Finite.{u_5} (α := α) {a : α | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((f : (a : α) → R⟦Γ⟧) a) g) 0}

Tactic:
f.support.finite_toSet.subset fun a ha => ?_

Premises used: Finsupp.support, Set.Finite.subset, Finset.finite_toSet
-- 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
f : α →₀ R⟦Γ⟧
g : Γ
refine :
  ∀ (a : α)
    (ha :
      Membership.mem (γ := Set α) {a : α | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((f : (a : α) → R⟦Γ⟧) a) g) 0} a),
    a ∈ (↑f.support : Set α)
⊢ Set.Finite.{u_5} (α := α) {a : α | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((f : (a : α) → R⟦Γ⟧) a) g) 0}

Tactic:
refine f.support.finite_toSet.subset fun a ha => ?_

Premises used: Finsupp.support, Set.Finite.subset, Finset.finite_toSet
-- 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
f : α →₀ R⟦Γ⟧
g : Γ
a : α
ha : Membership.mem (γ := Set α) {a : α | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((f : (a : α) → R⟦Γ⟧) a) g) 0} a
simp : ¬Eq (α := R⟦Γ⟧) ((f : (a : α) → R⟦Γ⟧) a : R⟦Γ⟧) (0 : R⟦Γ⟧)
⊢ a ∈ (↑f.support : Set α)

Tactic:
simp only [mem_coe, Finsupp.mem_support_iff, Ne]

Premises used: Finsupp.mem_support_iff, Ne, Finset.mem_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
f : α →₀ R⟦Γ⟧
g : Γ
a : α
ha : Membership.mem (γ := Set α) {a : α | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((f : (a : α) → R⟦Γ⟧) a) g) 0} a
contrapose :
  ∀ (ha : Eq (α := R⟦Γ⟧) ((f : (a : α) → R⟦Γ⟧) a : R⟦Γ⟧) (0 : R⟦Γ⟧)),
    a ∉ {a : α | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((f : (a : α) → R⟦Γ⟧) a) g) 0}
⊢ ¬Eq (α := R⟦Γ⟧) ((f : (a : α) → R⟦Γ⟧) a : R⟦Γ⟧) (0 : R⟦Γ⟧)

Tactic:
contrapose 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
f : α →₀ R⟦Γ⟧
g : Γ
a : α
ha : Eq (α := R⟦Γ⟧) ((f : (a : α) → R⟦Γ⟧) a : R⟦Γ⟧) (0 : R⟦Γ⟧)
⊢ a ∉ {a : α | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((f : (a : α) → R⟦Γ⟧) a) g) 0}

Tactic:
simp [ha]
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
f : α →₀ R⟦Γ⟧
⊢ Eq (α := (a : α) → R⟦Γ⟧) (⇑(ofFinsupp f) : (a : α) → R⟦Γ⟧) (⇑f : (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
f : α →₀ R⟦Γ⟧
coeff : ∀ (g : Γ), (ofFinsupp f).hsum.coeff g = HahnSeries.coeff (f.sum fun (x : α) ↦ id) g
⊢ (ofFinsupp f).hsum = f.sum fun (x : α) ↦ id

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
f : α →₀ R⟦Γ⟧
g : Γ
coeff :
  Eq.{u_3 + 1} (α := R) (∑ᶠ (i : α), HahnSeries.coeff ((f : (a : α) → R⟦Γ⟧) i) g)
    (HahnSeries.coeff (∑ x ∈ f.support, id ((f : (a : α) → R⟦Γ⟧) x)) g)
⊢ (ofFinsupp f).hsum.coeff g = HahnSeries.coeff (f.sum fun (x : α) ↦ id) g

Tactic:
simp only [coeff_hsum, coe_ofFinsupp, Finsupp.sum]

Premises used: Finsupp.sum, HahnSeries.SummableFamily.coeff_hsum, HahnSeries.SummableFamily.coe_ofFinsupp
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
f : α →₀ R⟦Γ⟧
g : Γ
coeff :
  Eq.{u_3 + 1} (α := R)
    (∑ᶠ (i : α), (HahnSeries.coeff.addMonoidHom g : (a : R⟦Γ⟧) → R) ((f : (a : α) → R⟦Γ⟧) i : R⟦Γ⟧) : R)
    ((HahnSeries.coeff.addMonoidHom g : (a : R⟦Γ⟧) → R) (∑ x ∈ f.support, (f : (a : α) → R⟦Γ⟧) x) : R)
⊢ Eq.{u_3 + 1} (α := R) (∑ᶠ (i : α), HahnSeries.coeff ((f : (a : α) → R⟦Γ⟧) i) g)
    (HahnSeries.coeff (∑ x ∈ f.support, id ((f : (a : α) → R⟦Γ⟧) x)) g)

Tactic:
simp_rw [← coeff.addMonoidHom_apply, id]

Premises used: id, HahnSeries.coeff.addMonoidHom_apply
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
f : α →₀ R⟦Γ⟧
g : Γ
coeff :
  (Function.support.{u_5, u_3} (M := R) fun (i : α) ↦
      (HahnSeries.coeff.addMonoidHom g : (a : R⟦Γ⟧) → R) ((f : (a : α) → R⟦Γ⟧) i : R⟦Γ⟧)) ⊆
    (↑f.support : Set α)
⊢ Eq.{u_3 + 1} (α := R)
    (∑ᶠ (i : α), (HahnSeries.coeff.addMonoidHom g : (a : R⟦Γ⟧) → R) ((f : (a : α) → R⟦Γ⟧) i : R⟦Γ⟧) : R)
    ((HahnSeries.coeff.addMonoidHom g : (a : R⟦Γ⟧) → R) (∑ x ∈ f.support, (f : (a : α) → R⟦Γ⟧) x) : R)

Tactic:
rw [map_sum, finsum_eq_sum_of_support_subset]

Premises used: map_sum, finsum_eq_sum_of_support_subset
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
f : α →₀ R⟦Γ⟧
g : Γ
x : α
h :
  Membership.mem (γ := Set α)
    (Function.support.{u_5, u_3} (M := R) fun (i : α) ↦
      (HahnSeries.coeff.addMonoidHom g : (a : R⟦Γ⟧) → R) ((f : (a : α) → R⟦Γ⟧) i : R⟦Γ⟧))
    x
coeff : ¬Eq (α := R⟦Γ⟧) ((f : (a : α) → R⟦Γ⟧) x : R⟦Γ⟧) (0 : R⟦Γ⟧)
⊢ x ∈ (↑f.support : Set α)

Tactic:
simp only [mem_coe, Finsupp.mem_support_iff, Ne]

Premises used: Finsupp.mem_support_iff, Ne, Finset.mem_coe
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
f : α →₀ R⟦Γ⟧
g : Γ
x : α
h :
  Membership.mem (γ := Set α)
    (Function.support.{u_5, u_3} (M := R) fun (i : α) ↦
      (HahnSeries.coeff.addMonoidHom g : (a : R⟦Γ⟧) → R) ((f : (a : α) → R⟦Γ⟧) i : R⟦Γ⟧))
    x
coeff :
  ∀ (h : Eq (α := R⟦Γ⟧) ((f : (a : α) → R⟦Γ⟧) x : R⟦Γ⟧) (0 : R⟦Γ⟧)),
    x ∉
      Function.support.{u_5, u_3} (M := R) fun (i : α) ↦
        (HahnSeries.coeff.addMonoidHom g : (a : R⟦Γ⟧) → R) ((f : (a : α) → R⟦Γ⟧) i : R⟦Γ⟧)
⊢ ¬Eq (α := R⟦Γ⟧) ((f : (a : α) → R⟦Γ⟧) x : R⟦Γ⟧) (0 : R⟦Γ⟧)

Tactic:
contrapose h
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
f : α →₀ R⟦Γ⟧
g : Γ
x : α
h : Eq (α := R⟦Γ⟧) ((f : (a : α) → R⟦Γ⟧) x : R⟦Γ⟧) (0 : R⟦Γ⟧)
⊢ x ∉
    Function.support.{u_5, u_3} (M := R) fun (i : α) ↦
      (coeff.addMonoidHom g : (a : R⟦Γ⟧) → R) ((f : (a : α) → R⟦Γ⟧) i : R⟦Γ⟧)

Tactic:
simp [h]
-- 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 : α ↪ β
⊢ Set.IsPWO.{u_1} (α := Γ)
    (⋃ (a : β),
      support.{u_1, u_3} (R := R)
        (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))

Tactic:
s.isPWO_iUnion_support.mono (Set.iUnion_subset fun b g h => ?_)

Premises used: Set.iUnion_subset, 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
s : SummableFamily Γ R α
f : α ↪ β
refine :
  ∀ (b : β) (g : Γ)
    (h :
      Membership.mem (γ := Set Γ)
        (support.{u_1, u_3} (R := 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))
        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)
        (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))

Tactic:
refine s.isPWO_iUnion_support.mono (Set.iUnion_subset fun b g h => ?_)

Premises used: Set.iUnion_subset, 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
s : SummableFamily Γ R α
f : α ↪ β
b : β
g : Γ
h :
  Membership.mem (γ := Set Γ)
    (support.{u_1, u_3} (R := 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))
    g
pos :
  ∀ (hb : Membership.mem (γ := Set β) (Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)) b),
    Membership.mem (γ := Set Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) g
neg :
  ∀ (hb : b ∉ Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)),
    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:
by_cases hb : b ∈ Set.range f

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

Tactic:
rw [dif_pos hb] at h

Premises used: dif_pos
-- 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 : α ↪ β
b : β
g : Γ
hb : Membership.mem (γ := Set β) (Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)) b
h :
  Membership.mem (γ := Set Γ)
    (support.{u_1, u_3} (R := R)
      ((s : (a : α) → R⟦Γ⟧) (Classical.choose (p := fun (x : α) ↦ (f : (a : α) → β) x = b) hb)))
    g
⊢ Membership.mem (γ := Set Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) g

Tactic:
Set.mem_iUnion.2 ⟨Classical.choose hb, h⟩

Premises used: Iff.mpr, Set.mem_iUnion, Exists.intro, Classical.choose
-- 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 : α ↪ β
b : β
g : Γ
hb : Membership.mem (γ := Set β) (Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)) b
h :
  Membership.mem (γ := Set Γ)
    (support.{u_1, u_3} (R := R)
      ((s : (a : α) → R⟦Γ⟧) (Classical.choose (p := fun (x : α) ↦ (f : (a : α) → β) x = b) hb)))
    g
⊢ Membership.mem (γ := Set Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) g

Tactic:
exact Set.mem_iUnion.2 ⟨Classical.choose hb, h⟩

Premises used: Iff.mpr, Set.mem_iUnion, Exists.intro, Classical.choose
-- 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 : α ↪ β
b : β
g : Γ
h :
  Membership.mem (γ := Set Γ)
    (support.{u_1, u_3} (R := 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))
    g
hb : b ∉ Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)
⊢ Membership.mem (γ := Set Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) g

Tactic:
simp [-Set.mem_range, dif_neg hb] at h

Premises used: Set.mem_range, dif_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 : 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
pos :
  ∀ (hb : Membership.mem (γ := Set β) (Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)) b),
    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
neg :
  ∀ (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
⊢ 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:
by_cases hb : b ∈ Set.range f

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

Tactic:
simp only [Ne, Set.mem_setOf_eq, dif_pos hb] at h

Premises used: dif_pos, Ne, Set.mem_setOf_eq
-- 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:
⟨Classical.choose hb, h, Classical.choose_spec hb⟩

Premises used: Set.Mem, setOf, Classical.choose_spec, And.intro, Exists.intro, Classical.choose, Set.image