awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
l : Filter α
refine : ∀ (h : ∀ (x : α), {x}ᶜ ∈ l) (s : Set α) (hs : sᶜ.Finite), s ∈ l
⊢ l ≤ cofinite ↔ ∀ (x : α), {x}ᶜ ∈ l

Tactic:
refine ⟨fun h x => h (finite_singleton x).compl_mem_cofinite, fun h s (hs : sᶜ.Finite) => ?_⟩
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
l : Filter α
h : ∀ (x : α), {x}ᶜ ∈ l
s : Set α
hs : sᶜ.Finite
rw : ∀ i ∈ sᶜ, {i}ᶜ ∈ l
⊢ s ∈ l

Tactic:
rw [← compl_compl s, ← biUnion_of_singleton sᶜ, compl_iUnion₂, Filter.biInter_mem hs]

Premises used: compl_compl, Compl.compl, Set.biUnion_of_singleton, Set.compl_iUnion₂, Filter.biInter_mem
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
l : Filter α
h : ∀ (x : α), {x}ᶜ ∈ l
s : Set α
hs : sᶜ.Finite
⊢ ∀ i ∈ sᶜ, {i}ᶜ ∈ l

Tactic:
fun x _ => h x
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
l : Filter α
h : ∀ (x : α), {x}ᶜ ∈ l
s : Set α
hs : sᶜ.Finite
⊢ ∀ i ∈ sᶜ, {i}ᶜ ∈ l

Tactic:
exact fun x _ => h x
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
l : Filter α
⊢ l ≤ cofinite ↔ ∀ (x : α), ∀ᶠ (y : α) in l, y ≠ x

Tactic:
le_cofinite_iff_compl_singleton_mem

Premises used: Filter.le_cofinite_iff_compl_singleton_mem, Set.Mem, Filter.Eventually, setOf, Set.singleton
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
inst : Preorder α
inst_1 : NoTopOrder α
⊢ LE.le.{u_2} (α := Filter α) atTop cofinite

Tactic:
le_cofinite_iff_eventually_ne.mpr eventually_ne_atTop

Premises used: Iff.mpr, Filter.le_cofinite_iff_eventually_ne, Filter.eventually_ne_atTop
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
inst : Preorder α
inst_1 : NoBotOrder α
⊢ LE.le.{u_2} (α := Filter α) atBot cofinite

Tactic:
le_cofinite_iff_eventually_ne.mpr eventually_ne_atBot

Premises used: Filter.eventually_ne_atBot, Iff.mpr, Filter.le_cofinite_iff_eventually_ne
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
β : Type u_3
f : α → β
⊢ comap f cofinite ≤ cofinite

Tactic:
le_cofinite_iff_eventually_ne.mpr fun x =>
    mem_comap.2 ⟨{f x}ᶜ, (finite_singleton _).compl_mem_cofinite, fun _ => ne_of_apply_ne f⟩

Premises used: Iff.mpr, Compl.compl, Filter.le_cofinite_iff_eventually_ne, ne_of_apply_ne, Filter.mem_comap, Set.Finite.compl_mem_cofinite, And.intro, Exists.intro, Singleton.singleton, Set.finite_singleton
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
β : Type u_3
s : Set (α × β)
⊢ Membership.mem (γ := Filter (α × β)) (Filter.coprod cofinite cofinite) sᶜ ↔
    Membership.mem (γ := Filter (α × β)) cofinite sᶜ

Tactic:
simp only [compl_mem_coprod, mem_cofinite, compl_compl, finite_image_fst_and_snd_iff]

Premises used: Filter.mem_cofinite, compl_compl, Set.finite_image_fst_and_snd_iff, Filter.compl_mem_coprod
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
ι : Type u_1
α : ι → Type u_4
inst : Finite ι
s : Set ((i : ι) → α i)
⊢ Membership.mem (γ := Filter ((i : ι) → α i)) (Filter.coprodᵢ (α := α) fun (i : ι) ↦ cofinite) sᶜ ↔
    Membership.mem (γ := Filter ((i : ι) → α i)) cofinite sᶜ

Tactic:
simp only [compl_mem_coprodᵢ, mem_cofinite, compl_compl, forall_finite_image_eval_iff]

Premises used: Filter.mem_cofinite, compl_compl, Set.forall_finite_image_eval_iff, Filter.compl_mem_coprodᵢ
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
l : Filter α
⊢ Disjoint cofinite l ↔ ∃ s ∈ l, s.Finite

Tactic:
simp [l.basis_sets.disjoint_iff_right]

Premises used: Filter.HasBasis.disjoint_iff_right, Filter.basis_sets
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
l : Filter α
⊢ Disjoint l cofinite ↔ ∃ s ∈ l, s.Finite

Tactic:
disjoint_comm.trans disjoint_cofinite_left

Premises used: disjoint_comm, Filter.disjoint_cofinite_left, Iff.trans
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
l : Filter α
inst : l.IsCountablyGenerated
h : cofinite ≤ l
rcases : ∀ (s : ℕ → Set α) (hs : l.HasAntitoneBasis s), l.kerᶜ.Countable
⊢ l.kerᶜ.Countable

Tactic:
rcases exists_antitone_basis l with ⟨s, hs⟩

Premises used: Filter.exists_antitone_basis
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
l : Filter α
inst : l.IsCountablyGenerated
h : cofinite ≤ l
s : ℕ → Set α
hs : l.HasAntitoneBasis s
simp : Set.Countable.{u_2} (α := α) (⋃ (i : ℕ), (s i)ᶜ)
⊢ l.kerᶜ.Countable

Tactic:
simp only [hs.ker, iInter_true, compl_iInter]

Premises used: Set.compl_iInter, Filter.HasAntitoneBasis.toHasBasis, Filter.HasBasis.ker, Set.iInter_true
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
l : Filter α
inst : l.IsCountablyGenerated
h : cofinite ≤ l
s : ℕ → Set α
hs : l.HasAntitoneBasis s
⊢ Set.Countable.{u_2} (α := α) (⋃ (i : ℕ), (s i)ᶜ)

Tactic:
countable_iUnion fun n ↦ Set.Finite.countable <| h <| hs.mem _

Premises used: Filter.HasAntitoneBasis.mem, Set.countable_iUnion, Set.Finite.countable
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
l : Filter α
inst : l.IsCountablyGenerated
h : cofinite ≤ l
s : ℕ → Set α
hs : l.HasAntitoneBasis s
⊢ Set.Countable.{u_2} (α := α) (⋃ (i : ℕ), (s i)ᶜ)

Tactic:
exact countable_iUnion fun n ↦ Set.Finite.countable <| h <| hs.mem _

Premises used: Filter.HasAntitoneBasis.mem, Set.countable_iUnion, Set.Finite.countable
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
β : Type u_3
f : α → β
l : Filter β
inst : l.IsCountablyGenerated
h : Tendsto f cofinite l
rw : (comap f l).kerᶜ.Countable
⊢ (f ⁻¹' l.ker)ᶜ.Countable

Tactic:
rw [← ker_comap]

Premises used: Filter.ker_comap
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
β : Type u_3
f : α → β
l : Filter β
inst : l.IsCountablyGenerated
h : Tendsto f cofinite l
⊢ (comap f l).kerᶜ.Countable

Tactic:
countable_compl_ker h.le_comap

Premises used: Filter.Tendsto.le_comap, Filter.countable_compl_ker
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
β : Type u_3
f : α → β
l : Filter β
inst : l.IsCountablyGenerated
h : Tendsto f cofinite l
⊢ (comap f l).kerᶜ.Countable

Tactic:
exact countable_compl_ker h.le_comap

Premises used: Filter.Tendsto.le_comap, Filter.countable_compl_ker
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
ι : Type u_1
α : ι → Type u_4
s : (i : ι) → Set (α i)
l : (i : ι) → Filter (α i)
h : ∀ (i : ι), s i ∈ l i
hfin : ∀ᶠ (i : ι) in cofinite, s i = univ
a : (i : ι) → α i
ha : a ∈ Set.pi (α := α) {x : ι | s x = univ}ᶜ s
i : ι
h₁ : Membership.mem (γ := Set ι) univ i → a i ∈ s i
⊢ Membership.mem (γ := Set ι) univ i → a i ∈ s i

Tactic:
_
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
ι : Type u_1
α : ι → Type u_4
s : (i : ι) → Set (α i)
l : (i : ι) → Filter (α i)
h : ∀ (i : ι), s i ∈ l i
hfin : ∀ᶠ (i : ι) in cofinite, s i = univ
h₁ :
  ∀ (a : (i : ι) → α i) (ha : a ∈ Set.pi (α := α) {x : ι | s x = univ}ᶜ s) (i : ι),
    Membership.mem (γ := Set ι) univ i → a i ∈ s i
⊢ Set.pi (α := α) univ s ∈ pi (α := α) l

Tactic:
filter_upwards [pi_mem_pi hfin fun i _ ↦ h i] with a ha i _

Premises used: Filter.pi_mem_pi
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
ι : Type u_1
α : ι → Type u_4
s : (i : ι) → Set (α i)
l : (i : ι) → Filter (α i)
h : ∀ (i : ι), s i ∈ l i
hfin : ∀ᶠ (i : ι) in cofinite, s i = univ
a : (i : ι) → α i
ha : a ∈ Set.pi (α := α) {x : ι | s x = univ}ᶜ s
i : ι
h_1 : Membership.mem (γ := Set ι) univ i
hi : s i = univ
⊢ a i ∈ s i

Tactic:
simp [hi]
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
ι : Type u_1
α : ι → Type u_4
s : (i : ι) → Set (α i)
l : (i : ι) → Filter (α i)
h : ∀ (i : ι), s i ∈ l i
hfin : ∀ᶠ (i : ι) in cofinite, s i = univ
a : (i : ι) → α i
ha : a ∈ Set.pi (α := α) {x : ι | s x = univ}ᶜ s
i : ι
h_1 : Membership.mem (γ := Set ι) univ i
hi : ¬s i = univ
⊢ a i ∈ s i

Tactic:
ha i hi
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
ι : Type u_1
α : ι → Type u_4
s : (i : ι) → Set (α i)
l : (i : ι) → Filter (α i)
h : ∀ (i : ι), s i ∈ l i
hfin : ∀ᶠ (i : ι) in cofinite, s i = univ
a : (i : ι) → α i
ha : a ∈ Set.pi (α := α) {x : ι | s x = univ}ᶜ s
i : ι
h_1 : Membership.mem (γ := Set ι) univ i
hi : ¬s i = univ
⊢ a i ∈ s i

Tactic:
exact ha i hi
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
ι : Type u_1
α : ι → Type u_4
s : (i : ι) → Set (α i)
l : (i : ι) → Filter (α i)
h : ∀ (i : ι), s i ∈ l i
hfin : ∀ᶠ (i : ι) in cofinite, s i = univ
a : (i : ι) → α i
ha : a ∈ Set.pi (α := α) {x : ι | s x = univ}ᶜ s
i : ι
h_1 : Membership.mem (γ := Set ι) univ i
if : ∀ (hi : s i = univ), a i ∈ s i
if₁ : ∀ (hi : ¬s i = univ), a i ∈ s i
if₂ : ∀ (hi : s i = univ), a i ∈ s i
if₃ if₄ : ∀ (hi : ¬s i = univ), a i ∈ s i
⊢ a i ∈ s i

Tactic:
if hi : s i = univ then
    simp [hi]
  else
    exact ha i hi

Premises used: Set.univ
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
⊢ map (Pi.map (α := α) (β := β) f) (pi (α := α) l) = pi (α := β) fun (i : ι) ↦ map (f i) (l i)

Tactic:
le_antisymm (tendsto_piMap_pi fun _ ↦ tendsto_map) ?_

Premises used: Filter.tendsto_map, le_antisymm, Filter.tendsto_piMap_pi
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
refine : (pi (α := β) fun (i : ι) ↦ map (f i) (l i)) ≤ map (Pi.map (α := α) (β := β) f) (pi (α := α) l)
⊢ map (Pi.map (α := α) (β := β) f) (pi (α := α) l) = pi (α := β) fun (i : ι) ↦ map (f i) (l i)

Tactic:
refine le_antisymm (tendsto_piMap_pi fun _ ↦ tendsto_map) ?_

Premises used: Filter.tendsto_map, le_antisymm, Filter.tendsto_piMap_pi
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
⊢ (pi (α := β) fun (i : ι) ↦ map (f i) (l i)) ≤ map (Pi.map (α := α) (β := β) f) (pi (α := α) l)

Tactic:
((hasBasis_pi fun i ↦ (l i).basis_sets).map _).ge_iff.2 ?_

Premises used: Iff.mpr, Filter.HasBasis.map, Filter.HasBasis.ge_iff, Filter.basis_sets, Filter.hasBasis_pi
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
refine :
  ∀ (i' : Set ι × ((i : ι) → Set (α i))),
    (i'.1.Finite ∧ ∀ i ∈ i'.1, i'.2 i ∈ l i) →
      Membership.mem (γ := Filter ((i : ι) → β i)) (pi (α := β) fun (i : ι) ↦ map (f i) (l i))
        (Pi.map (α := α) (β := β) f '' i'.1.pi (α := α) fun (i : ι) ↦ id (i'.2 i))
⊢ (pi (α := β) fun (i : ι) ↦ map (f i) (l i)) ≤ map (Pi.map (α := α) (β := β) f) (pi (α := α) l)

Tactic:
refine ((hasBasis_pi fun i ↦ (l i).basis_sets).map _).ge_iff.2 ?_

Premises used: Iff.mpr, Filter.HasBasis.map, Filter.HasBasis.ge_iff, Filter.basis_sets, Filter.hasBasis_pi
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
rw :
  Membership.mem (γ := Filter ((i : ι) → β i)) (pi (α := β) fun (i : ι) ↦ map (f i) (l i))
    (Set.pi (α := β) univ fun (i : ι) ↦
      f i '' (I, s).1.piecewise (β := fun (i : ι) ↦ Set (α i)) (fun (i : ι) ↦ id ((I, s).2 i)) (fun (x : ι) ↦ univ) i)
⊢ Membership.mem (γ := Filter ((i : ι) → β i)) (pi (α := β) fun (i : ι) ↦ map (f i) (l i))
    (Pi.map (α := α) (β := β) f '' (I, s).1.pi (α := α) fun (i : ι) ↦ id ((I, s).2 i))

Tactic:
rw [← univ_pi_piecewise_univ, piMap_image_univ_pi]

Premises used: Set.univ_pi_piecewise_univ, Set.piMap_image_univ_pi
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
⊢ Membership.mem (γ := Filter ((i : ι) → β i)) (pi (α := β) fun (i : ι) ↦ map (f i) (l i))
    (Set.pi (α := β) univ fun (i : ι) ↦
      f i '' (I, s).1.piecewise (β := fun (i : ι) ↦ Set (α i)) (fun (i : ι) ↦ id ((I, s).2 i)) (fun (x : ι) ↦ univ) i)

Tactic:
univ_pi_mem_pi (fun i ↦ ?_) ?_

Premises used: Filter.univ_pi_mem_pi
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
refine_1 :
  ∀ (i : ι),
    f i '' (I, s).1.piecewise (β := fun (i : ι) ↦ Set (α i)) (fun (i : ι) ↦ id ((I, s).2 i)) (fun (x : ι) ↦ univ) i ∈
      map (f i) (l i)
refine_2 :
  ∀ᶠ (i : ι) in cofinite,
    f i '' (I, s).1.piecewise (β := fun (i : ι) ↦ Set (α i)) (fun (i : ι) ↦ id ((I, s).2 i)) (fun (x : ι) ↦ univ) i =
      univ
⊢ Membership.mem (γ := Filter ((i : ι) → β i)) (pi (α := β) fun (i : ι) ↦ map (f i) (l i))
    (Set.pi (α := β) univ fun (i : ι) ↦
      f i '' (I, s).1.piecewise (β := fun (i : ι) ↦ Set (α i)) (fun (i : ι) ↦ id ((I, s).2 i)) (fun (x : ι) ↦ univ) i)

Tactic:
refine univ_pi_mem_pi (fun i ↦ ?_) ?_

Premises used: Filter.univ_pi_mem_pi
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
i : ι
pos :
  ∀ (hi : i ∈ I),
    f i '' (I, s).1.piecewise (β := fun (i : ι) ↦ Set (α i)) (fun (i : ι) ↦ id ((I, s).2 i)) (fun (x : ι) ↦ univ) i ∈
      map (f i) (l i)
neg :
  ∀ (hi : i ∉ I),
    f i '' (I, s).1.piecewise (β := fun (i : ι) ↦ Set (α i)) (fun (i : ι) ↦ id ((I, s).2 i)) (fun (x : ι) ↦ univ) i ∈
      map (f i) (l i)
⊢ f i '' (I, s).1.piecewise (β := fun (i : ι) ↦ Set (α i)) (fun (i : ι) ↦ id ((I, s).2 i)) (fun (x : ι) ↦ univ) i ∈
    map (f i) (l i)

Tactic:
by_cases hi : i ∈ I
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
i : ι
hi : i ∈ I
⊢ f i '' (I, s).1.piecewise (β := fun (i : ι) ↦ Set (α i)) (fun (i : ι) ↦ id ((I, s).2 i)) (fun (x : ι) ↦ univ) i ∈
    map (f i) (l i)

Tactic:
simpa [hi] using image_mem_map (hs i hi)

Premises used: Filter.image_mem_map
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
i : ι
hi : i ∉ I
⊢ f i '' (I, s).1.piecewise (β := fun (i : ι) ↦ Set (α i)) (fun (i : ι) ↦ id ((I, s).2 i)) (fun (x : ι) ↦ univ) i ∈
    map (f i) (l i)

Tactic:
simp [hi]
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
i : ι
hsurj : Surjective (f i)
h :
  ∀ (hiI : i ∉ I),
    f i '' I.piecewise (β := fun (i : ι) ↦ Set (α i)) (fun (i : ι) ↦ id (s i)) (fun (x : ι) ↦ univ) i = univ
⊢ i ∈ Iᶜ → f i '' I.piecewise (β := fun (i : ι) ↦ Set (α i)) (fun (i : ι) ↦ id (s i)) (fun (x : ι) ↦ univ) i = univ

Tactic:
(hiI : i ∉ I)
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
h :
  ∀ (i : ι) (hsurj : Surjective (f i)) (hiI : i ∉ I),
    f i '' I.piecewise (β := fun (i : ι) ↦ Set (α i)) (fun (i : ι) ↦ id (s i)) (fun (x : ι) ↦ univ) i = univ
⊢ ∀ᶠ (i : ι) in cofinite,
    f i '' (I, s).1.piecewise (β := fun (i : ι) ↦ Set (α i)) (fun (i : ι) ↦ id ((I, s).2 i)) (fun (x : ι) ↦ univ) i =
      univ

Tactic:
filter_upwards [hf, hI.compl_mem_cofinite] with i hsurj (hiI : i ∉ I)

Premises used: Set.Finite.compl_mem_cofinite
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
i : ι
hsurj : Surjective (f i)
hiI : i ∉ I
⊢ f i '' I.piecewise (β := fun (i : ι) ↦ Set (α i)) (fun (i : ι) ↦ id (s i)) (fun (x : ι) ↦ univ) i = univ

Tactic:
simp [hiI, hsurj.range_eq]

Premises used: Function.Surjective.range_eq
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
rw :
  Membership.mem (γ := Filter ((i : ι) → β i)) (pi (α := β) fun (i : ι) ↦ map (f i) (l i))
    (Pi.map (α := α) (β := β) f ''
      Set.pi (α := α) univ
        ((I, s).1.piecewise (β := fun (i : ι) ↦ Set (α i)) (fun (i : ι) ↦ id ((I, s).2 i)) fun (x : ι) ↦ univ))
rw₁ rw₂ rw₃ :
  Membership.mem (γ := Filter ((i : ι) → β i)) (pi (α := β) fun (i : ι) ↦ map (f i) (l i))
    (Set.pi (α := β) univ fun (i : ι) ↦
      f i '' (I, s).1.piecewise (β := fun (i : ι) ↦ Set (α i)) (fun (i : ι) ↦ id ((I, s).2 i)) (fun (x : ι) ↦ univ) i)
refine_1 :
  ∀ (i : ι),
    f i '' (I, s).1.piecewise (β := fun (i : ι) ↦ Set (α i)) (fun (i : ι) ↦ id ((I, s).2 i)) (fun (x : ι) ↦ univ) i ∈
      map (f i) (l i)
refine_2 refine_2₁ :
  ∀ᶠ (i : ι) in cofinite,
    f i '' (I, s).1.piecewise (β := fun (i : ι) ↦ Set (α i)) (fun (i : ι) ↦ id ((I, s).2 i)) (fun (x : ι) ↦ univ) i =
      univ
⊢ Membership.mem (γ := Filter ((i : ι) → β i)) (pi (α := β) fun (i : ι) ↦ map (f i) (l i))
    (Pi.map (α := α) (β := β) f '' (I, s).1.pi (α := α) fun (i : ι) ↦ id ((I, s).2 i))

Tactic:
classical
  rw [← univ_pi_piecewise_univ, piMap_image_univ_pi]
  refine univ_pi_mem_pi (fun i ↦ ?_) ?_
  · by_cases hi : i ∈ I
    · simpa [hi] using image_mem_map (hs i hi)
    · simp [hi]
  · filter_upwards [hf, hI.compl_mem_cofinite] with i hsurj (hiI : i ∉ I)
    simp [hiI, hsurj.range_eq]

Premises used: Set.univ_pi_piecewise_univ, Set.piMap_image_univ_pi, Filter.univ_pi_mem_pi, Set.Finite.compl_mem_cofinite
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
inst : Finite ι
f : (i : ι) → α i → β i
l : (i : ι) → Filter (α i)
⊢ ∀ᶠ (i : ι) in cofinite, Surjective (f i)

Tactic:
simp
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
s : Set α
hs : s.Finite
⊢ cofinite ⊓ 𝓟 sᶜ = cofinite

Tactic:
simpa using hs.compl_mem_cofinite

Premises used: Set.Finite.compl_mem_cofinite
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_2
s t : Set α
ht : t.Finite
rw : cofinite ⊓ 𝓟 (s ∩ tᶜ) = cofinite ⊓ 𝓟 s
rw₁ : cofinite ⊓ (𝓟 s ⊓ 𝓟 tᶜ) = cofinite ⊓ 𝓟 s
rw₂ : cofinite ⊓ 𝓟 s ⊓ 𝓟 tᶜ = cofinite ⊓ 𝓟 s
rw₃ : cofinite ⊓ 𝓟 tᶜ ⊓ 𝓟 s = cofinite ⊓ 𝓟 s
rw₄ rw₅ : cofinite ⊓ 𝓟 s = cofinite ⊓ 𝓟 s
⊢ cofinite ⊓ 𝓟 (s \ t) = cofinite ⊓ 𝓟 s

Tactic:
rw [diff_eq, ← inf_principal, ← inf_assoc, inf_right_comm, ht.cofinite_inf_principal_compl]

Premises used: Filter.inf_principal, Set.diff_eq, inf_right_comm, inf_assoc, Set.Finite.cofinite_inf_principal_compl
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
⊢ Eq (α := Filter ℕ) cofinite atTop

Tactic:
le_antisymm ?_ atTop_le_cofinite

Premises used: le_antisymm, Filter.atTop_le_cofinite
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
refine : LE.le (α := Filter ℕ) cofinite atTop
⊢ Eq (α := Filter ℕ) cofinite atTop

Tactic:
refine le_antisymm ?_ atTop_le_cofinite

Premises used: le_antisymm, Filter.atTop_le_cofinite
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
⊢ LE.le (α := Filter ℕ) cofinite atTop

Tactic:
atTop_basis.ge_iff.2 fun N _ => ?_

Premises used: Iff.mpr, Filter.atTop_basis, Filter.HasBasis.ge_iff
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
refine : ∀ (N : ℕ), True → Membership.mem (γ := Filter ℕ) cofinite (Ici N)
⊢ LE.le (α := Filter ℕ) cofinite atTop

Tactic:
refine atTop_basis.ge_iff.2 fun N _ => ?_

Premises used: Iff.mpr, Filter.atTop_basis, Filter.HasBasis.ge_iff
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
N : ℕ
h : True
⊢ Membership.mem (γ := Filter ℕ) cofinite (Ici N)

Tactic:
simpa only [mem_cofinite, compl_Ici] using finite_lt_nat N

Premises used: Filter.mem_cofinite, Set.compl_Ici, Set.finite_lt_nat
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
p : ℕ → Prop
rw : (∃ᶠ (n : ℕ) in cofinite, p n) ↔ Set.Infinite (α := ℕ) {n : ℕ | p n}
rw₁ rw₂ : Set.Infinite (α := ℕ) {x : ℕ | p x} ↔ Set.Infinite (α := ℕ) {n : ℕ | p n}
⊢ (∃ᶠ (n : ℕ) in atTop, p n) ↔ Set.Infinite (α := ℕ) {n : ℕ | p n}

Tactic:
rw [← Nat.cofinite_eq_atTop, frequently_cofinite_iff_infinite]

Premises used: Filter.frequently_cofinite_iff_infinite, Nat.cofinite_eq_atTop
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
⊢ ∀ᶠ (k : ℕ) in atTop, 0 < k

Tactic:
Filter.eventually_of_mem (Filter.mem_atTop_sets.mpr ⟨1, fun _ hx ↦ hx⟩) (fun _ hx ↦ hx)

Premises used: Iff.mpr, Filter.mem_atTop_sets, Filter.eventually_of_mem, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_4
β : Type u_5
inst : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
pos : ∀ (all_top : ∃ y ∈ s, ∃ (x : β), f y < x), ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a
neg : ∀ (all_top : ∀ (y : α) (_ : y ∈ s) (x : β), x ≤ f y), ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Tactic:
by_cases! all_top : ∃ y ∈ s, ∃ x, f y < x
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_4
β : Type u_5
inst : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
all_top : ∃ y ∈ s, ∃ (x : β), f y < x
pos : ∀ (y : α) (hys : y ∈ s) (x : β) (hx : f y < x), ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Tactic:
rcases all_top with ⟨y, hys, x, hx⟩
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_4
β : Type u_5
inst : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
⊢ Set.Finite.{u_4} (α := α) {y : α | ¬x ≤ f y}

Tactic:
have : { y | ¬x ≤ f y }.Finite := Filter.eventually_cofinite.mp (tendsto_atTop.1 hf x)
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_4
β : Type u_5
inst : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
this : Set.Finite.{u_4} (α := α) {y : α | ¬x ≤ f y}
⊢ Set.Finite.{u_4} (α := α) {y : α | f y < x}

Tactic:
simp only [not_le] at this

Premises used: not_le
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_4
β : Type u_5
inst : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
this : Set.Finite.{u_4} (α := α) {y : α | f y < x}
pos :
  ∀ (a₀ : α) (others_bigger : ∀ b ∈ {y : α | f y < x} ∩ s, f a₀ ≤ f b) (ha₀ : f a₀ < x) (ha₀s : a₀ ∈ s),
    ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Tactic:
obtain ⟨a₀, ⟨ha₀ : f a₀ < x, ha₀s⟩, others_bigger⟩ :=
      exists_min_image _ f (this.inter_of_left s) ⟨y, hx, hys⟩

Premises used: Set.Finite.inter_of_left, Set.exists_min_image, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_4
β : Type u_5
inst : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
this : Set.Finite.{u_4} (α := α) {y : α | f y < x}
a₀ : α
others_bigger : ∀ b ∈ {y : α | f y < x} ∩ s, f a₀ ≤ f b
ha₀ : f a₀ < x
ha₀s : a₀ ∈ s
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Tactic:
⟨a₀, ha₀s, fun a has => (lt_or_ge (f a) x).elim ?_ (le_trans ha₀.le)⟩

Premises used: LT.lt.le, And.intro, Exists.intro, lt_or_ge, Or.elim, le_trans
-- Module: Mathlib.Order.Filter.Cofinite
Goal:
α : Type u_4
β : Type u_5
inst : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
this : Set.Finite.{u_4} (α := α) {y : α | f y < x}
a₀ : α
others_bigger : ∀ b ∈ {y : α | f y < x} ∩ s, f a₀ ≤ f b
ha₀ : f a₀ < x
ha₀s : a₀ ∈ s
pos : ∀ (a : α) (has : a ∈ s), f a < x → f a₀ ≤ f a
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Tactic:
refine ⟨a₀, ha₀s, fun a has => (lt_or_ge (f a) x).elim ?_ (le_trans ha₀.le)⟩