awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
apply : ClusterPt a (Filter.map (fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i) atTop)
apply₁ apply₂ :
  ∀ (u : Set α) (hu : u ∈ 𝓝 a) (s : Finset ((b : β) × γ b)), ∃ (b : Finset ((b : β) × γ b)), s ⊆ b ∧ ∏ i ∈ b, f i ∈ u
apply₃ :
  ∀ (u : Set α) (hu : u ∈ 𝓝 a) (s : Finset ((b : β) × γ b)) (v : Set α) (vu : v ⊆ u)
    (v_open : IsOpen[inst_1.toTopologicalSpace] v) (hv : a ∈ v),
    ∃ (b : Finset ((b : β) × γ b)), s ⊆ b ∧ ∏ i ∈ b, f i ∈ u
apply₄ :
  ∀ (u : Set α) (hu : u ∈ 𝓝 a) (s : Finset ((b : β) × γ b)) (v : Set α) (vu : v ⊆ u)
    (v_open : IsOpen[inst_1.toTopologicalSpace] v) (hv : a ∈ v) (t0 : Finset β) (st0 : ∏ i ∈ t0, g i ∈ v)
    (ht0 : image (Sigma.fst (β := fun (b : β) ↦ γ b)) s ⊆ t0), ∃ (b : Finset ((b : β) × γ b)), s ⊆ b ∧ ∏ i ∈ b, f i ∈ u
⊢ HasProd f a
have apply₅ : ∀ (u : Set α) (hu : u ∈ 𝓝 a) (s : Finset ((b : β) × γ b)) (v : Set α) (vu : v ⊆ u)
  (v_open : IsOpen[inst_1.toTopologicalSpace] v) (hv : a ∈ v) (t0 : Finset β) (st0 : ∏ i ∈ t0, g i ∈ v)
  (ht0 : image (Sigma.fst (β := fun (b : β) ↦ γ b)) s ⊆ t0)
  (L :
    Tendsto (β := α) (fun (t : Finset ((b : β) × γ b)) ↦ ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ t0, f p) atTop
      (𝓝 (∏ b ∈ t0, g b))),
  ∃ (b : Finset ((b : β) × γ b)), s ⊆ b ∧ ∏ i ∈ b, f i ∈ u
Tactic: classical
  apply le_nhds_of_cauchy_adhp h
  simp only [← mapClusterPt_def, mapClusterPt_iff_frequently, frequently_atTop, ge_iff_le,
    le_eq_subset]
  intro u hu s
  rcases mem_nhds_iff.1 hu with ⟨v, vu, v_open, hv⟩
  obtain ⟨t0, st0, ht0⟩ : ∃ t0, ∏ i ∈ t0, g i ∈ v ∧ s.image Sigma.fst ⊆ t0 := by
    have A : ∀ᶠ t0 in (atTop : Filter (Finset β)), ∏ i ∈ t0, g i ∈ v := hg (v_open.mem_nhds hv)
    exact (A.and (Ici_mem_atTop _)).exists
  have L : Tendsto (fun t : Finset (Σ b, γ b) ↦ ∏ p ∈ t with p.1 ∈ t0, f p) atTop
      (𝓝 <| ∏ b ∈ t0, g b) := by
    simp only [← sigma_preimage_mk, prod_sigma]
    refine tendsto_finsetProd _ fun b _ ↦ ?_
    change
      Tendsto (fun t ↦ (fun t ↦ ∏ s ∈ t, f ⟨b, s⟩) (preimage t (Sigma.mk b) _)) atTop (𝓝 (g b))
    exact (hf b).comp (tendsto_finset_preimage_atTop_atTop (sigma_mk_injective))
  have : ∃ t, ∏ p ∈ t with p.1 ∈ t0, f p ∈ v ∧ s ⊆ t :=
    ((Tendsto.eventually_mem L (v_open.mem_nhds st0)).and (Ici_mem_atTop _)).exists
  obtain ⟨t, tv, st⟩ := this
  refine ⟨{p ∈ t | p.1 ∈ t0}, fun x hx ↦ ?_, vu tv⟩
  simpa only [mem_filter, st hx, true_and] using ht0 (mem_image_of_mem Sigma.fst hx)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
β : Type u_2
L : SummationFilter β
⊢ L.NeBot ∨ L.filter = ⊥
have pos : ∀ (h : L.filter = ⊥), L.NeBot ∨ L.filter = ⊥
Tactic: by_cases h : L.filter = ⊥
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
β : Type u_2
L : SummationFilter β
pos : ∀ (h : L.filter = ⊥), L.NeBot ∨ L.filter = ⊥
⊢ L.NeBot ∨ L.filter = ⊥
have neg : ∀ (h : ¬L.filter = ⊥), L.NeBot ∨ L.filter = ⊥
Tactic: by_cases h : L.filter = ⊥
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
β : Type u_2
L : SummationFilter β
⊢ L.support = (map SetLike.coe L.filter).limsInf
have refine : ∀ (c : Set β), L.support ≤ c ↔ (map SetLike.coe L.filter).limsInf ≤ c
Tactic: refine eq_of_forall_ge_iff fun c ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
β : Type u_2
L : SummationFilter β
⊢ L.support = univ ↔ L.filter ≤ atTop
have simp : (∀ (x : β), ∀ᶠ (s : Finset β) in L.filter, x ∈ s) ↔ L.filter ≤ atTop
Tactic: simp only [support, Set.eq_univ_iff_forall, Set.mem_setOf]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
β : Type u_2
L : SummationFilter β
⊢ (∀ (x : β), ∀ᶠ (s : Finset β) in L.filter, x ∈ s) ↔ L.filter ≤ atTop
have refine_1 : ∀ (h : ∀ (x : β), ∀ᶠ (s : Finset β) in L.filter, x ∈ s) (s : Set (Finset β))
  (hs : Membership.mem (γ := Filter (Finset β)) atTop s), s ∈ L.filter
Tactic: refine ⟨fun h s hs ↦ ?_, fun h b ↦ .filter_mono h ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
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
⊢ (∀ (x : β), ∀ᶠ (s : Finset β) in L.filter, x ∈ s) ↔ L.filter ≤ atTop
have refine_2 : ∀ (h : L.filter ≤ atTop) (b : β), ∀ᶠ (x : Finset β) in atTop, b ∈ x
Tactic: refine ⟨fun h s hs ↦ ?_, fun h b ↦ .filter_mono h ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
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
⊢ s ∈ L.filter
have refine_1 : ∀ (t : Finset β) (ht : ∀ b ≥ t, b ∈ s), s ∈ L.filter
Tactic: obtain ⟨t, ht⟩ := mem_atTop_sets.mp hs
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (hypothesis)
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
⊢ s ∈ L.filter
have this : ⋂ 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
β : Type u_2
L : SummationFilter β
h : L.filter ≤ atTop
b : β
⊢ ∀ᶠ (x : Finset β) in atTop, b ∈ x
have 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
Tactic: filter_upwards [eventually_ge_atTop {b}] using by simp
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
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
⊢ ∀ᶠ (x : Finset β) in atTop, b ∈ x
have h₂ : ∀ (a : Finset β), {b} ≤ a → b ∈ a
Tactic: filter_upwards [eventually_ge_atTop {b}] using by simp
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (hypothesis)
Goal:
β : Type u_2
L : SummationFilter β
hL : ¬L.NeBot
⊢ L.LeAtTop
have hLs : L.support = univ
Tactic: have hLs : L.support = Set.univ := by
    simp [SummationFilter.support, L.neBot_or_eq_bot.resolve_left hL]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
β : Type u_2
L : SummationFilter β
inst : L.HasSupport
b : β
⊢ (∀ᶠ (s : Finset β) in L.filter, b ∈ s) ∨ ∀ᶠ (s : Finset β) in L.filter, b ∉ s
have rw : (¬∀ᶠ (s : Finset β) in L.filter, b ∈ s) → ∀ᶠ (s : Finset β) in L.filter, b ∉ s
Tactic: rw [or_iff_not_imp_left]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
β : Type u_2
L : SummationFilter β
inst : L.HasSupport
b : β
hb : ¬∀ᶠ (s : Finset β) in L.filter, b ∈ s
⊢ ∀ᶠ (s : Finset β) in L.filter, b ∉ s
have 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
Tactic: filter_upwards [L.eventually_le_support] with a ha using notMem_subset ha hb
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
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
⊢ ∀ᶠ (s : Finset β) in L.filter, b ∉ s
have h₁ : ∀ (a : Finset β), (↑a : Set β) ⊆ L.support → b ∉ a
Tactic: filter_upwards [L.eventually_le_support] with a ha using notMem_subset ha hb
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : L.NeBot
f : β ↪ γ
⊢ (L.map f).support = (⇑f : (a : β) → γ) '' L.support
have h : ∀ (c : γ), c ∈ (L.map f).support ↔ Membership.mem (γ := Set γ) ((⇑f : (a : β) → γ) '' L.support) c
Tactic: ext c
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : L.NeBot
f : β ↪ γ
c : γ
⊢ c ∈ (L.map f).support ↔ Membership.mem (γ := Set γ) ((⇑f : (a : β) → γ) '' L.support) c
have 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 : γ)
Tactic: rcases em (c ∈ range f) with ⟨b, rfl⟩ | hc
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
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 : γ)
⊢ c ∈ (L.map f).support ↔ Membership.mem (γ := Set γ) ((⇑f : (a : β) → γ) '' L.support) c
have h₁ : ∀ (hc : c ∉ range.{u_3, u_2 + 1} (ι := β) (⇑f : (a : β) → γ)),
  c ∈ (L.map f).support ↔ Membership.mem (γ := Set γ) ((⇑f : (a : β) → γ) '' L.support) c
Tactic: rcases em (c ∈ range f) with ⟨b, rfl⟩ | hc
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : L.HasSupport
f : β ↪ γ
⊢ (L.map f).HasSupport
have eventually_le_support : ∀ᶠ (s : Finset γ) in (L.map f).filter, (↑s : Set γ) ⊆ (L.map f).support
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : L.HasSupport
f : β ↪ γ
⊢ ∀ᶠ (s : Finset γ) in (L.map f).filter, (↑s : Set γ) ⊆ (L.map f).support
have eventually_le_support : ∀ (h : L.NeBot), ∀ᶠ (s : Finset γ) in (L.map f).filter, (↑s : Set γ) ⊆ (L.map f).support
Tactic: obtain (h | h) := L.neBot_or_eq_bot
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
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
⊢ ∀ᶠ (s : Finset γ) in (L.map f).filter, (↑s : Set γ) ⊆ (L.map f).support
have eventually_le_support₁ : ∀ (h : L.filter = ⊥), ∀ᶠ (s : Finset γ) in (L.map f).filter, (↑s : Set γ) ⊆ (L.map f).support
Tactic: obtain (h | h) := L.neBot_or_eq_bot
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : L.HasSupport
f : β ↪ γ
h : L.NeBot
⊢ ∀ᶠ (s : Finset γ) in (L.map f).filter, (↑s : Set γ) ⊆ (L.map f).support
have eventually_le_support : ∀ᶠ (a : Finset β) in L.filter,
  (↑a : Set β) ⊆ preimage.{u_2, u_3} (β := γ) (⇑f : (a : β) → γ) ((⇑f : (a : β) → γ) '' L.support)
Tactic: simp only [map_filter, eventually_map, Finset.coe_map, image_subset_iff, support_map]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : L.HasSupport
f : β ↪ γ
h : L.NeBot
⊢ ∀ᶠ (a : Finset β) in L.filter,
    (↑a : Set β) ⊆ preimage.{u_2, u_3} (β := γ) (⇑f : (a : β) → γ) ((⇑f : (a : β) → γ) '' L.support)
have 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
Tactic: filter_upwards [L.eventually_le_support] with a using by grind
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
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
⊢ ∀ᶠ (a : Finset β) in L.filter,
    (↑a : Set β) ⊆ preimage.{u_2, u_3} (β := γ) (⇑f : (a : β) → γ) ((⇑f : (a : β) → γ) '' L.support)
have h₂ : ∀ (a : Finset β),
  (↑a : Set β) ⊆ L.support →
    (↑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
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : L.HasSupport
f : γ ↪ β
⊢ (L.comap f).HasSupport
have eventually_le_support : ∀ᶠ (s : Finset γ) in (L.comap f).filter, (↑s : Set γ) ⊆ (L.comap f).support
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : L.HasSupport
f : γ ↪ β
⊢ ∀ᶠ (s : Finset γ) in (L.comap f).filter, (↑s : Set γ) ⊆ (L.comap f).support
have eventually_le_support : ∀ᶠ (a : Finset β) in L.filter,
  Subset.{u_3} (α := Set γ) ((⇑f : (a : γ) → β) ⁻¹' (↑a : Set β)) ((⇑f : (a : γ) → β) ⁻¹' L.support)
Tactic: simp only [support_comap, comap_filter, eventually_map, Finset.coe_preimage]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : L.HasSupport
f : γ ↪ β
⊢ ∀ᶠ (a : Finset β) in L.filter,
    Subset.{u_3} (α := Set γ) ((⇑f : (a : γ) → β) ⁻¹' (↑a : Set β)) ((⇑f : (a : γ) → β) ⁻¹' L.support)
have 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
Tactic: filter_upwards [L.eventually_le_support] with a using Set.preimage_mono
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
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
⊢ ∀ᶠ (a : Finset β) in L.filter,
    Subset.{u_3} (α := Set γ) ((⇑f : (a : γ) → β) ⁻¹' (↑a : Set β)) ((⇑f : (a : γ) → β) ⁻¹' L.support)
have h₁ : ∀ (a : Finset β),
  (↑a : Set β) ⊆ L.support →
    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
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : L.LeAtTop
f : γ ↪ β
⊢ (L.comap f).filter ≤ atTop
have rw : (L.comap f).support = univ
Tactic: rw [← support_eq_univ_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
γ : Type u_3
β : Type u_4
f : γ ↪ β
⊢ Eq.{u_3 + 1} (α := SummationFilter γ)
    { filter := Filter.map (fun (s : Finset β) ↦ s.preimage (⇑f : (a : γ) → β) ⋯) atTop } { filter := atTop }
have e_filter : ∀ (s : Set (Finset γ)),
  Membership.mem (γ := Filter (Finset γ)) (Filter.map (fun (s : Finset β) ↦ s.preimage (⇑f : (a : γ) → β) sorry) atTop) s ↔
    Membership.mem (γ := Filter (Finset γ)) atTop s
Tactic: congr 1 with s
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
γ : Type u_3
β : Type u_4
f : γ ↪ β
s : Set (Finset γ)
⊢ Membership.mem (γ := Filter (Finset γ)) (Filter.map (fun (s : Finset β) ↦ s.preimage (⇑f : (a : γ) → β) ⋯) atTop) s ↔
    Membership.mem (γ := Filter (Finset γ)) atTop s
have e_filter : (∃ (a : Finset β), ∀ (b : Finset β), a ⊆ b → b.preimage (⇑f : (a : γ) → β) sorry ∈ s) ↔
  ∃ (a : Finset γ), ∀ (b : Finset γ), a ⊆ b → b ∈ s
Tactic: simp only [mem_map, mem_atTop_sets, ge_iff_le, Finset.le_eq_subset, mem_preimage]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
γ : Type u_3
β : Type u_4
f : γ ↪ β
s : Set (Finset γ)
⊢ (∃ (a : Finset β), ∀ (b : Finset β), a ⊆ b → b.preimage (⇑f : (a : γ) → β) ⋯ ∈ s) ↔
    ∃ (a : Finset γ), ∀ (b : Finset γ), a ⊆ b → b ∈ s
have e_filter : (∃ (a : Finset β), ∀ (b : Finset β), a ⊆ b → b.preimage (⇑f : (a : γ) → β) sorry ∈ s) →
  ∃ (a : Finset γ), ∀ (b : Finset γ), a ⊆ b → b ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
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
⊢ (∃ (a : Finset β), ∀ (b : Finset β), a ⊆ b → b.preimage (⇑f : (a : γ) → β) ⋯ ∈ s) ↔
    ∃ (a : Finset γ), ∀ (b : Finset γ), a ⊆ b → b ∈ s
have e_filter₁ : (∃ (a : Finset γ), ∀ (b : Finset γ), a ⊆ b → b ∈ s) →
  ∃ (a : Finset β), ∀ (b : Finset β), a ⊆ b → b.preimage (⇑f : (a : γ) → β) sorry ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
γ : Type u_3
β : Type u_4
f : γ ↪ β
s : Set (Finset γ)
t : Finset β
ht : ∀ (b : Finset β), t ⊆ b → b.preimage (⇑f : (a : γ) → β) ⋯ ∈ s
⊢ ∃ (a : Finset γ), ∀ (b : Finset γ), a ⊆ b → b ∈ s
have e_filter : ∀ (x : Finset γ) (hx : t.preimage (⇑f : (a : γ) → β) sorry ⊆ x), x ∈ s
Tactic: refine ⟨t.preimage f (by simp), fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
γ : Type u_3
β : Type u_4
f : γ ↪ β
⊢ (unconditional β).comap f = unconditional γ
have simp : Eq.{u_3 + 1} (α := SummationFilter γ)
  { filter := Filter.map (fun (s : Finset β) ↦ s.preimage (⇑f : (a : γ) → β) sorry) atTop } { filter := atTop }
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)⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
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 }
⊢ (unconditional β).comap f = unconditional γ
have e_filter : ∀ (s : Set (Finset γ)),
  Membership.mem (γ := Filter (Finset γ)) (Filter.map (fun (s : Finset β) ↦ s.preimage (⇑f : (a : γ) → β) sorry) atTop) s ↔
    Membership.mem (γ := Filter (Finset γ)) atTop s
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)⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
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
⊢ (unconditional β).comap f = unconditional γ
have e_filter₁ : ∀ (s : Set (Finset γ)),
  (∃ (a : Finset β), ∀ (b : Finset β), a ⊆ b → b.preimage (⇑f : (a : γ) → β) sorry ∈ s) ↔
    ∃ (a : Finset γ), ∀ (b : Finset γ), a ⊆ b → b ∈ s
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)⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
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
⊢ (unconditional β).comap f = unconditional γ
have e_filter₂ : ∀ (s : Set (Finset γ)) (t : Finset β) (ht : ∀ (b : Finset β), t ⊆ b → b.preimage (⇑f : (a : γ) → β) sorry ∈ s),
  ∃ (a : Finset γ), ∀ (b : Finset γ), a ⊆ b → b ∈ s
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)⟩