awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
L : SummationFilter β
c : Set β
⊢ L.support ≤ c ↔ (map SetLike.coe L.filter).limsInf ≤ c

Tactic:
simpa [support, limsInf, setOf_subset] using
    ⟨fun hL b hb x hx ↦ hL x <| hb.mp <| .of_forall fun c hc ↦ hc hx,
      fun hL x hx ↦ singleton_subset_iff.mp <| hL _ <| by simpa using hx⟩

Premises used: Filter.limsInf, Set.setOf_subset, SummationFilter.support
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
L : SummationFilter β
simp : (∀ (x : β), ∀ᶠ (s : Finset β) in L.filter, x ∈ s) ↔ L.filter ≤ atTop
⊢ L.support = univ ↔ L.filter ≤ atTop

Tactic:
simp only [support, Set.eq_univ_iff_forall, Set.mem_setOf]

Premises used: Set.eq_univ_iff_forall, Set.mem_setOf, SummationFilter.support
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
L : SummationFilter β
⊢ (∀ (x : β), ∀ᶠ (s : Finset β) in L.filter, x ∈ s) ↔ L.filter ≤ atTop

Tactic:
⟨fun h s hs ↦ ?_, fun h b ↦ .filter_mono h ?_⟩

Premises used: Filter.Eventually.filter_mono, Iff.intro
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
L : SummationFilter β
refine_1 :
  ∀ (h : ∀ (x : β), ∀ᶠ (s : Finset β) in L.filter, x ∈ s) (s : Set (Finset β))
    (hs : Membership.mem (γ := Filter (Finset β)) atTop s), s ∈ L.filter
refine_2 : ∀ (h : L.filter ≤ atTop) (b : β), ∀ᶠ (x : Finset β) in atTop, b ∈ x
⊢ (∀ (x : β), ∀ᶠ (s : Finset β) in L.filter, x ∈ s) ↔ L.filter ≤ atTop

Tactic:
refine ⟨fun h s hs ↦ ?_, fun h b ↦ .filter_mono h ?_⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
L : SummationFilter β
h : ∀ (x : β), ∀ᶠ (s : Finset β) in L.filter, x ∈ s
s : Set (Finset β)
hs : Membership.mem (γ := Filter (Finset β)) atTop s
refine_1 : ∀ (t : Finset β) (ht : ∀ b ≥ t, b ∈ s), s ∈ L.filter
⊢ s ∈ L.filter

Tactic:
obtain ⟨t, ht⟩ := mem_atTop_sets.mp hs

Premises used: Filter.mem_atTop_sets, Iff.mp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
L : SummationFilter β
h : ∀ (x : β), ∀ᶠ (s : Finset β) in L.filter, x ∈ s
s : Set (Finset β)
hs : Membership.mem (γ := Filter (Finset β)) atTop s
t : Finset β
ht : ∀ b ≥ t, b ∈ s
⊢ ⋂ i ∈ t, {x : Finset β | (fun (s : Finset β) ↦ i ∈ s) x} ∈ L.filter

Tactic:
have := (Filter.biInter_finset_mem t).mpr fun b hb ↦ h b
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
L : SummationFilter β
h : ∀ (x : β), ∀ᶠ (s : Finset β) in L.filter, x ∈ s
s : Set (Finset β)
hs : Membership.mem (γ := Filter (Finset β)) atTop s
t : Finset β
ht : ∀ b ≥ t, b ∈ s
this : ⋂ i ∈ t, {x : Finset β | (fun (s : Finset β) ↦ i ∈ s) x} ∈ L.filter
r : Finset β
hr : Membership.mem (γ := Set (Finset β)) (⋂ i ∈ t, {x : Finset β | (fun (s : Finset β) ↦ i ∈ s) x}) r
⊢ r ≥ t

Tactic:
simpa using hr
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
L : SummationFilter β
h : ∀ (x : β), ∀ᶠ (s : Finset β) in L.filter, x ∈ s
s : Set (Finset β)
hs : Membership.mem (γ := Filter (Finset β)) atTop s
t : Finset β
ht : ∀ b ≥ t, b ∈ s
this : ⋂ i ∈ t, {x : Finset β | (fun (s : Finset β) ↦ i ∈ s) x} ∈ L.filter
⊢ s ∈ L.filter

Tactic:
exact Filter.mem_of_superset this fun r hr ↦ ht r (by simpa using hr)

Premises used: Filter.mem_of_superset
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
L : SummationFilter β
h : L.filter ≤ atTop
b : β
⊢ ∀ (a : Finset β), {b} ≤ a → b ∈ a

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
L : SummationFilter β
h : L.filter ≤ atTop
b : β
h₁ :
  ∀ (a : Finset β),
    Membership.mem (γ := Set (Finset β))
      {x : Finset β |
        Membership.mem (γ := Set (Finset β)) {x : Finset β | (fun (x : Finset β) ↦ {b} ≤ x) x} x →
          Membership.mem (γ := Set (Finset β)) {x : Finset β | (fun (x : Finset β) ↦ b ∈ x) x} x}
      a
h₂ : ∀ (a : Finset β), {b} ≤ a → b ∈ a
⊢ ∀ᶠ (x : Finset β) in atTop, b ∈ x

Tactic:
filter_upwards [eventually_ge_atTop {b}] using by simp

Premises used: Filter.eventually_ge_atTop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
L : SummationFilter β
inst : L.LeAtTop
⊢ L.support = univ

Tactic:
support_eq_univ_iff.mpr L.le_atTop

Premises used: Iff.mpr, SummationFilter.support_eq_univ_iff, SummationFilter.LeAtTop.le_atTop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : IsEmpty β
L : SummationFilter β
⊢ L.LeAtTop

Tactic:
⟨support_eq_univ_iff.mp <| Subsingleton.elim ..⟩

Premises used: SummationFilter.LeAtTop.mk, SummationFilter.support_eq_univ_iff, Iff.mp, Subsingleton.elim
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
L : SummationFilter β
hL : ¬L.NeBot
⊢ L.support = univ

Tactic:
simp [SummationFilter.support, L.neBot_or_eq_bot.resolve_left hL]

Premises used: SummationFilter.neBot_or_eq_bot, Or.resolve_left, SummationFilter.support
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
L : SummationFilter β
hL : ¬L.NeBot
⊢ L.support = univ

Tactic:
have hLs : L.support = Set.univ := by
    simp [SummationFilter.support, L.neBot_or_eq_bot.resolve_left hL]
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
L : SummationFilter β
hL : ¬L.NeBot
hLs : L.support = univ
⊢ L.LeAtTop

Tactic:
⟨L.support_eq_univ_iff.mp hLs⟩

Premises used: SummationFilter.LeAtTop.mk, SummationFilter.support_eq_univ_iff, Iff.mp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
L : SummationFilter β
hL : ¬L.NeBot
hLs : L.support = univ
⊢ L.LeAtTop

Tactic:
exact ⟨L.support_eq_univ_iff.mp hLs⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : L.LeAtTop
b : β
⊢ (fun (x : β) ↦ x ∈ L.support) b

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : L.LeAtTop
⊢ ∀ᶠ (s : Finset β) in L.filter, (↑s : Set β) ⊆ L.support

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
L : SummationFilter β
inst : L.HasSupport
b : β
rw : (¬∀ᶠ (s : Finset β) in L.filter, b ∈ s) → ∀ᶠ (s : Finset β) in L.filter, b ∉ s
⊢ (∀ᶠ (s : Finset β) in L.filter, b ∈ s) ∨ ∀ᶠ (s : Finset β) in L.filter, b ∉ s

Tactic:
rw [or_iff_not_imp_left]

Premises used: Classical.or_iff_not_imp_left
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
L : SummationFilter β
inst : L.HasSupport
b : β
hb : ¬∀ᶠ (s : Finset β) in L.filter, b ∈ s
a : Finset β
ha : (↑a : Set β) ⊆ L.support
⊢ b ∉ a

Tactic:
notMem_subset ha hb

Premises used: Set.notMem_subset
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
L : SummationFilter β
inst : L.HasSupport
b : β
hb : ¬∀ᶠ (s : Finset β) in L.filter, b ∈ s
h :
  ∀ (a : Finset β),
    Membership.mem (γ := Set (Finset β))
      {x : Finset β |
        Membership.mem (γ := Set (Finset β)) {x : Finset β | (fun (s : Finset β) ↦ (↑s : Set β) ⊆ L.support) x} x →
          Membership.mem (γ := Set (Finset β)) {x : Finset β | (fun (s : Finset β) ↦ b ∉ s) x} x}
      a
h₁ h₂ : ∀ (a : Finset β) (ha : (↑a : Set β) ⊆ L.support), b ∉ a
⊢ ∀ᶠ (s : Finset β) in L.filter, b ∉ s

Tactic:
filter_upwards [L.eventually_le_support] with a ha using notMem_subset ha hb

Premises used: SummationFilter.HasSupport.eventually_le_support
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : L.NeBot
f : β ↪ γ
h : ∀ (c : γ), c ∈ (L.map f).support ↔ Membership.mem (γ := Set γ) ((⇑f : (a : β) → γ) '' L.support) c
⊢ (L.map f).support = (⇑f : (a : β) → γ) '' L.support

Tactic:
ext c
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : L.NeBot
f : β ↪ γ
c : γ
h :
  ∀ (b : β),
    Membership.mem (α := γ) (L.map f).support ((f : (a : β) → γ) b : γ) ↔
      Membership.mem.{u_3, u_3} (α := γ) (γ := Set γ) ((⇑f : (a : β) → γ) '' L.support) ((f : (a : β) → γ) b : γ)
h₁ :
  ∀ (hc : c ∉ range.{u_3, u_2 + 1} (ι := β) (⇑f : (a : β) → γ)),
    c ∈ (L.map f).support ↔ Membership.mem (γ := Set γ) ((⇑f : (a : β) → γ) '' L.support) c
⊢ c ∈ (L.map f).support ↔ Membership.mem (γ := Set γ) ((⇑f : (a : β) → γ) '' L.support) c

Tactic:
rcases em (c ∈ range f) with ⟨b, rfl⟩ | hc

Premises used: Membership.mem, em, Set.range, DFunLike.coe, rfl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : L.NeBot
f : β ↪ γ
b : β
⊢ Membership.mem (α := γ) (L.map f).support ((f : (a : β) → γ) b : γ) ↔
    Membership.mem.{u_3, u_3} (α := γ) (γ := Set γ) ((⇑f : (a : β) → γ) '' L.support) ((f : (a : β) → γ) b : γ)

Tactic:
simp [support]

Premises used: SummationFilter.support
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : L.NeBot
f : β ↪ γ
c : γ
hc : c ∉ range.{u_3, u_2 + 1} (ι := β) (⇑f : (a : β) → γ)
hc' : c ∈ (L.map f).support
this :
  ∃ (x : Finset β),
    Membership.mem (γ := Set (Finset γ)) {x : Finset γ | (fun (s : Finset γ) ↦ c ∈ s) x} (Finset.map f x)
⊢ Membership.mem (γ := Set γ) ((⇑f : (a : β) → γ) '' L.support) c

Tactic:
grind
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : L.NeBot
f : β ↪ γ
c : γ
hc : c ∉ range.{u_3, u_2 + 1} (ι := β) (⇑f : (a : β) → γ)
⊢ Membership.mem (γ := Set γ) ((⇑f : (a : β) → γ) '' L.support) c → c ∈ (L.map f).support

Tactic:
grind
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : L.NeBot
f : β ↪ γ
c : γ
hc : c ∉ range.{u_3, u_2 + 1} (ι := β) (⇑f : (a : β) → γ)
⊢ c ∈ (L.map f).support ↔ Membership.mem (γ := Set γ) ((⇑f : (a : β) → γ) '' L.support) c

Tactic:
exact ⟨fun hc' ↦ have := hc'.exists; by grind, by grind⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : L.HasSupport
f : β ↪ γ
eventually_le_support : ∀ᶠ (s : Finset γ) in (L.map f).filter, (↑s : Set γ) ⊆ (L.map f).support
⊢ (L.map f).HasSupport

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : L.HasSupport
f : β ↪ γ
eventually_le_support : ∀ (h : L.NeBot), ∀ᶠ (s : Finset γ) in (L.map f).filter, (↑s : Set γ) ⊆ (L.map f).support
eventually_le_support₁ : ∀ (h : L.filter = ⊥), ∀ᶠ (s : Finset γ) in (L.map f).filter, (↑s : Set γ) ⊆ (L.map f).support
⊢ ∀ᶠ (s : Finset γ) in (L.map f).filter, (↑s : Set γ) ⊆ (L.map f).support

Tactic:
obtain (h | h) := L.neBot_or_eq_bot

Premises used: SummationFilter.neBot_or_eq_bot
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : L.HasSupport
f : β ↪ γ
h : L.NeBot
eventually_le_support :
  ∀ᶠ (a : Finset β) in L.filter,
    (↑a : Set β) ⊆ preimage.{u_2, u_3} (β := γ) (⇑f : (a : β) → γ) ((⇑f : (a : β) → γ) '' L.support)
⊢ ∀ᶠ (s : Finset γ) in (L.map f).filter, (↑s : Set γ) ⊆ (L.map f).support

Tactic:
simp only [map_filter, eventually_map, Finset.coe_map, image_subset_iff, support_map]

Premises used: SummationFilter.support_map, Filter.eventually_map, Set.image_subset_iff, SummationFilter.map_filter, Finset.coe_map
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : L.HasSupport
f : β ↪ γ
h : L.NeBot
a : Finset β
⊢ (↑a : Set β) ⊆ L.support →
    (↑a : Set β) ⊆ preimage.{u_2, u_3} (β := γ) (⇑f : (a : β) → γ) ((⇑f : (a : β) → γ) '' L.support)

Tactic:
grind
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : L.HasSupport
f : β ↪ γ
h : L.NeBot
h₁ :
  ∀ (a : Finset β),
    Membership.mem (γ := Set (Finset β))
      {x : Finset β |
        Membership.mem (γ := Set (Finset β)) {x : Finset β | (fun (s : Finset β) ↦ (↑s : Set β) ⊆ L.support) x} x →
          Membership.mem (γ := Set (Finset β))
            {x : Finset β |
              (fun (a : Finset β) ↦
                  (↑a : Set β) ⊆ preimage.{u_2, u_3} (β := γ) (⇑f : (a : β) → γ) ((⇑f : (a : β) → γ) '' L.support))
                x}
            x}
      a
h₂ h₃ :
  ∀ (a : Finset β),
    (↑a : Set β) ⊆ L.support →
      (↑a : Set β) ⊆ preimage.{u_2, u_3} (β := γ) (⇑f : (a : β) → γ) ((⇑f : (a : β) → γ) '' L.support)
⊢ ∀ᶠ (a : Finset β) in L.filter,
    (↑a : Set β) ⊆ preimage.{u_2, u_3} (β := γ) (⇑f : (a : β) → γ) ((⇑f : (a : β) → γ) '' L.support)

Tactic:
filter_upwards [L.eventually_le_support] with a using by grind

Premises used: SummationFilter.HasSupport.eventually_le_support
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : L.HasSupport
f : β ↪ γ
h : L.filter = ⊥
⊢ ∀ᶠ (s : Finset γ) in (L.map f).filter, (↑s : Set γ) ⊆ (L.map f).support

Tactic:
simp [h]
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_2
γ : Type u_3
L : SummationFilter β
f : γ ↪ β
⊢ (L.comap f).support = (⇑f : (a : γ) → β) ⁻¹' L.support

Tactic:
simp [support]

Premises used: SummationFilter.support
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : L.HasSupport
f : γ ↪ β
eventually_le_support : ∀ᶠ (s : Finset γ) in (L.comap f).filter, (↑s : Set γ) ⊆ (L.comap f).support
⊢ (L.comap f).HasSupport

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : L.HasSupport
f : γ ↪ β
eventually_le_support :
  ∀ᶠ (a : Finset β) in L.filter,
    Subset.{u_3} (α := Set γ) ((⇑f : (a : γ) → β) ⁻¹' (↑a : Set β)) ((⇑f : (a : γ) → β) ⁻¹' L.support)
⊢ ∀ᶠ (s : Finset γ) in (L.comap f).filter, (↑s : Set γ) ⊆ (L.comap f).support

Tactic:
simp only [support_comap, comap_filter, eventually_map, Finset.coe_preimage]

Premises used: SummationFilter.comap_filter, Filter.eventually_map, Finset.coe_preimage, SummationFilter.support_comap
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : L.HasSupport
f : γ ↪ β
a : Finset β
⊢ (↑a : Set β) ⊆ L.support →
    Subset.{u_3} (α := Set γ) ((⇑f : (a : γ) → β) ⁻¹' (↑a : Set β)) ((⇑f : (a : γ) → β) ⁻¹' L.support)

Tactic:
Set.preimage_mono

Premises used: Set.preimage_mono
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : L.HasSupport
f : γ ↪ β
h :
  ∀ (a : Finset β),
    Membership.mem (γ := Set (Finset β))
      {x : Finset β |
        Membership.mem (γ := Set (Finset β)) {x : Finset β | (fun (s : Finset β) ↦ (↑s : Set β) ⊆ L.support) x} x →
          Membership.mem (γ := Set (Finset β))
            {x : Finset β |
              (fun (a : Finset β) ↦
                  Subset.{u_3} (α := Set γ) ((⇑f : (a : γ) → β) ⁻¹' (↑a : Set β)) ((⇑f : (a : γ) → β) ⁻¹' L.support))
                x}
            x}
      a
h₁ h₂ :
  ∀ (a : Finset β),
    (↑a : Set β) ⊆ L.support →
      Subset.{u_3} (α := Set γ) ((⇑f : (a : γ) → β) ⁻¹' (↑a : Set β)) ((⇑f : (a : γ) → β) ⁻¹' L.support)
⊢ ∀ᶠ (a : Finset β) in L.filter,
    Subset.{u_3} (α := Set γ) ((⇑f : (a : γ) → β) ⁻¹' (↑a : Set β)) ((⇑f : (a : γ) → β) ⁻¹' L.support)

Tactic:
filter_upwards [L.eventually_le_support] with a using Set.preimage_mono

Premises used: SummationFilter.HasSupport.eventually_le_support, Set.preimage_mono
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : L.LeAtTop
f : γ ↪ β
rw : (L.comap f).support = univ
⊢ (L.comap f).filter ≤ atTop

Tactic:
rw [← support_eq_univ_iff]

Premises used: SummationFilter.support_eq_univ_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : L.LeAtTop
f : γ ↪ β
⊢ (L.comap f).support = univ

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ (unconditional β).LeAtTop

Tactic:
⟨le_rfl⟩

Premises used: le_rfl, SummationFilter.LeAtTop.mk
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ (unconditional β).NeBot

Tactic:
⟨atTop_neBot⟩

Premises used: Filter.atTop_neBot, SummationFilter.NeBot.mk
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Countable β
⊢ (unconditional β).filter.IsCountablyGenerated

Tactic:
atTop.isCountablyGenerated

Premises used: iInf, Filter.atTop, Filter.atTop.isCountablyGenerated
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
γ : Type u_3
β : Type u_4
f : γ ↪ β
e_filter :
  ∀ (s : Set (Finset γ)),
    Membership.mem (γ := Filter (Finset γ)) (Filter.map (fun (s : Finset β) ↦ s.preimage (⇑f : (a : γ) → β) ⋯) atTop)
        s ↔
      Membership.mem (γ := Filter (Finset γ)) atTop s
⊢ Eq.{u_3 + 1} (α := SummationFilter γ)
    { filter := Filter.map (fun (s : Finset β) ↦ s.preimage (⇑f : (a : γ) → β) ⋯) atTop } { filter := atTop }

Tactic:
congr 1 with s
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
γ : Type u_3
β : Type u_4
f : γ ↪ β
s : Set (Finset γ)
e_filter :
  (∃ (a : Finset β), ∀ (b : Finset β), a ⊆ b → b.preimage (⇑f : (a : γ) → β) ⋯ ∈ s) ↔
    ∃ (a : Finset γ), ∀ (b : Finset γ), a ⊆ b → b ∈ s
⊢ Membership.mem (γ := Filter (Finset γ)) (Filter.map (fun (s : Finset β) ↦ s.preimage (⇑f : (a : γ) → β) ⋯) atTop) s ↔
    Membership.mem (γ := Filter (Finset γ)) atTop s

Tactic:
simp only [mem_map, mem_atTop_sets, ge_iff_le, Finset.le_eq_subset, mem_preimage]

Premises used: ge_iff_le, Filter.mem_atTop_sets, Finset.le_eq_subset, Filter.mem_map, Set.mem_preimage
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
γ : Type u_3
β : Type u_4
f : γ ↪ β
s : Set (Finset γ)
e_filter :
  (∃ (a : Finset β), ∀ (b : Finset β), a ⊆ b → b.preimage (⇑f : (a : γ) → β) ⋯ ∈ s) →
    ∃ (a : Finset γ), ∀ (b : Finset γ), a ⊆ b → b ∈ s
e_filter₁ :
  (∃ (a : Finset γ), ∀ (b : Finset γ), a ⊆ b → b ∈ s) →
    ∃ (a : Finset β), ∀ (b : Finset β), a ⊆ b → b.preimage (⇑f : (a : γ) → β) ⋯ ∈ s
⊢ (∃ (a : Finset β), ∀ (b : Finset β), a ⊆ b → b.preimage (⇑f : (a : γ) → β) ⋯ ∈ s) ↔
    ∃ (a : Finset γ), ∀ (b : Finset γ), a ⊆ b → b ∈ s

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
γ : Type u_3
β : Type u_4
f : γ ↪ β
s : Set (Finset γ)
t : Finset β
ht : ∀ (b : Finset β), t ⊆ b → b.preimage (⇑f : (a : γ) → β) ⋯ ∈ s
⊢ InjOn.{u_3, u_4} (α := γ) (β := β) (⇑f : (a : γ) → β) ((⇑f : (a : γ) → β) ⁻¹' (↑t : Set β))

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
γ : Type u_3
β : Type u_4
f : γ ↪ β
s : Set (Finset γ)
t : Finset β
ht : ∀ (b : Finset β), t ⊆ b → b.preimage (⇑f : (a : γ) → β) ⋯ ∈ s
e_filter : ∀ (x : Finset γ) (hx : t.preimage (⇑f : (a : γ) → β) ⋯ ⊆ x), x ∈ s
⊢ ∃ (a : Finset γ), ∀ (b : Finset γ), a ⊆ b → b ∈ s

Tactic:
refine ⟨t.preimage f (by simp), fun x hx ↦ ?_⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
γ : Type u_3
β : Type u_4
f : γ ↪ β
s : Set (Finset γ)
t : Finset β
ht : ∀ (b : Finset β), t ⊆ b → b.preimage (⇑f : (a : γ) → β) ⋯ ∈ s
x : Finset γ
hx : t.preimage (⇑f : (a : γ) → β) ⋯ ⊆ x
⊢ x ∈ s

Tactic:
simpa [Finset.union_eq_right.mpr hx] using ht (t ∪ x.map f) t.subset_union_left

Premises used: Iff.mpr, Finset.map, Finset.subset_union_left, Finset.union_eq_right, Union.union
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
γ : Type u_3
β : Type u_4
f : γ ↪ β
s : Set (Finset γ)
t : Finset γ
ht : ∀ (b : Finset γ), t ⊆ b → b ∈ s
⊢ ∃ (a : Finset β), ∀ (b : Finset β), a ⊆ b → b.preimage (⇑f : (a : γ) → β) ⋯ ∈ s

Tactic:
⟨_, fun b hb ↦ ht _ (Finset.map_subset_iff_subset_preimage.mp hb)⟩

Premises used: SummationFilter.comap._proof_1, Finset.preimage, Exists.intro, Iff.mp, Finset.map_subset_iff_subset_preimage, DFunLike.coe
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
γ : Type u_3
β : Type u_4
f : γ ↪ β
s : Set (Finset γ)
t : Finset γ
ht : ∀ (b : Finset γ), t ⊆ b → b ∈ s
⊢ ∃ (a : Finset β), ∀ (b : Finset β), a ⊆ b → b.preimage (⇑f : (a : γ) → β) ⋯ ∈ s

Tactic:
exact ⟨_, fun b hb ↦ ht _ (Finset.map_subset_iff_subset_preimage.mp hb)⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
γ : Type u_3
β : Type u_4
f : γ ↪ β
simp :
  Eq.{u_3 + 1} (α := SummationFilter γ)
    { filter := Filter.map (fun (s : Finset β) ↦ s.preimage (⇑f : (a : γ) → β) ⋯) atTop } { filter := atTop }
e_filter :
  ∀ (s : Set (Finset γ)),
    Membership.mem (γ := Filter (Finset γ)) (Filter.map (fun (s : Finset β) ↦ s.preimage (⇑f : (a : γ) → β) ⋯) atTop)
        s ↔
      Membership.mem (γ := Filter (Finset γ)) atTop s
e_filter₁ :
  ∀ (s : Set (Finset γ)),
    (∃ (a : Finset β), ∀ (b : Finset β), a ⊆ b → b.preimage (⇑f : (a : γ) → β) ⋯ ∈ s) ↔
      ∃ (a : Finset γ), ∀ (b : Finset γ), a ⊆ b → b ∈ s
e_filter₂ :
  ∀ (s : Set (Finset γ)) (t : Finset β) (ht : ∀ (b : Finset β), t ⊆ b → b.preimage (⇑f : (a : γ) → β) ⋯ ∈ s),
    ∃ (a : Finset γ), ∀ (b : Finset γ), a ⊆ b → b ∈ s
e_filter₃ e_filter₄ :
  ∀ (s : Set (Finset γ)) (t : Finset γ) (ht : ∀ (b : Finset γ), t ⊆ b → b ∈ s),
    ∃ (a : Finset β), ∀ (b : Finset β), a ⊆ b → b.preimage (⇑f : (a : γ) → β) ⋯ ∈ s
⊢ (unconditional β).comap f = unconditional γ

Tactic:
classical
  simp only [unconditional, comap]
  congr 1 with s
  simp only [mem_map, mem_atTop_sets, ge_iff_le, Finset.le_eq_subset, mem_preimage]
  constructor <;> rintro ⟨t, ht⟩
  · refine ⟨t.preimage f (by simp), fun x hx ↦ ?_⟩
    simpa [Finset.union_eq_right.mpr hx] using ht (t ∪ x.map f) t.subset_union_left
  · exact ⟨_, fun b hb ↦ ht _ (Finset.map_subset_iff_subset_preimage.mp hb)⟩

Premises used: ge_iff_le, Filter.mem_atTop_sets, Finset.le_eq_subset, SummationFilter.comap, Filter.mem_map, Set.mem_preimage, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_4
inst : Finite β
L : SummationFilter β
inst_1 : L.LeAtTop
inst_2 : L.NeBot
haveI : ∀ (this : Fintype β), L = unconditional β
⊢ L = unconditional β

Tactic:
haveI := Fintype.ofFinite β
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_4
inst : Finite β
L : SummationFilter β
inst_1 : L.LeAtTop
inst_2 : L.NeBot
this : Fintype β
rw : Eq.{u_4 + 1} (α := Filter (Finset β)) (𝓟 (Ici Finset.univ)) (pure Finset.univ)
rw₁ : Eq.{u_4 + 1} (α := Filter (Finset β)) (𝓟 (Ici ⊤)) (pure ⊤)
rw₂ : Eq (α := Filter (Finset β)) (𝓟 {⊤}) (pure ⊤)
rw₃ rw₄ : Eq.{u_4 + 1} (α := Filter (Finset β)) (pure ⊤) (pure ⊤)
⊢ Eq.{u_4 + 1} (α := Filter (Finset β)) atTop (pure Finset.univ)

Tactic:
rw [(isTop_iff_eq_top.mpr rfl).atTop_eq (a := Finset.univ), ← Finset.top_eq_univ,
      Ici_top, principal_singleton]

Premises used: Finset.top_eq_univ, IsTop.atTop_eq, Set.Ici_top, Filter.principal_singleton
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_4
inst : Finite β
L : SummationFilter β
inst_1 : L.LeAtTop
inst_2 : L.NeBot
this : Fintype β
⊢ Eq.{u_4 + 1} (α := Filter (Finset β)) atTop (pure Finset.univ)

Tactic:
have hAtTop : (atTop : Filter (Finset β)) = pure Finset.univ := by
    rw [(isTop_iff_eq_top.mpr rfl).atTop_eq (a := Finset.univ), ← Finset.top_eq_univ,
      Ici_top, principal_singleton]
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_4
inst : Finite β
L : SummationFilter β
inst_1 : L.LeAtTop
inst_2 : L.NeBot
this : Fintype β
hAtTop : Eq.{u_4 + 1} (α := Filter (Finset β)) atTop (pure Finset.univ)
⊢ L.filter ≤ atTop

Tactic:
have hL := L.le_atTop