awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.Cocardinal (goal)
Goal:
α : Type u
c : Cardinal.{u}
hreg_1 hreg : c.IsRegular
hUnion :
  ∀ (S : Set (Set α)),
    #(↑S : Type u) < c →
      (∀ s ∈ S, Membership.mem (γ := Set (Set α)) {s : Set α | #(↑s : Type u) < c} s) →
        Membership.mem (γ := Set (Set α)) {s : Set α | #(↑s : Type u) < c} (⋃₀ S)
⊢ Filter α
have hmono : ∀ (t : Set α),
  Membership.mem (γ := Set (Set α)) {s : Set α | #(↑s : Type u) < c} t →
    ∀ s ⊆ t, Membership.mem (γ := Set (Set α)) {s : Set α | #(↑s : Type u) < c} s
Tactic: apply ofCardinalUnion {s | Cardinal.mk s < c} (natCast_lt_aleph0.trans_le hreg.aleph0_le)
-- Lean 4 proof step from Mathlib.Order.Filter.Cocardinal (goal)
Goal:
α : Type u
c : Cardinal.{u}
hreg_1 hreg : c.IsRegular
⊢ ∀ (S : Set (Set α)),
    #(↑S : Type u) < c →
      (∀ s ∈ S, Membership.mem (γ := Set (Set α)) {s : Set α | #(↑s : Type u) < c} s) →
        Membership.mem (γ := Set (Set α)) {s : Set α | #(↑s : Type u) < c} (⋃₀ S)
have hUnion : ∀ (s : Set (Set α)) (hS : #(↑s : Type u) < c)
  (hSc : ∀ s_1 ∈ s, Membership.mem (γ := Set (Set α)) {s : Set α | #(↑s : Type u) < c} s_1),
  ⨆ (s_1 : (↑s : Type u)), #(↑(↑s_1 : Set α) : Type u) < c
Tactic: refine fun s hS hSc ↦ lt_of_le_of_lt (mk_sUnion_le _) <| mul_lt_of_lt hreg.aleph0_le hS ?_
-- Lean 4 proof step from Mathlib.Order.Filter.Cocardinal (goal)
Goal:
α : Type u
c : Cardinal.{u}
hreg_1 hreg : c.IsRegular
s : Set (Set α)
hS : #(↑s : Type u) < c
hSc : ∀ s_1 ∈ s, Membership.mem (γ := Set (Set α)) {s : Set α | #(↑s : Type u) < c} s_1
⊢ ⨆ (s_1 : (↑s : Type u)), #(↑(↑s_1 : Set α) : Type u) < c
have apply : #(↑s : Type u) < c.ord.cof
Tactic: apply iSup_lt_of_lt_cof_ord _ fun i ↦ hSc i.1 i.2
-- Lean 4 proof step from Mathlib.Order.Filter.Cocardinal (goal)
Goal:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
S : Set (Set α)
hS : #(↑S : Type u) < c
hSs : ∀ s ∈ S, s ∈ cocardinal α hreg
⊢ ⋂₀ S ∈ cocardinal α hreg
have grw : #(↑(compl '' S) : Type u) * ⨆ (s : (↑(compl '' S) : Type u)), #(↑(↑s : Set α) : Type u) < c
Tactic: grw [mem_cocardinal, Set.compl_sInter, mk_sUnion_le]
-- Lean 4 proof step from Mathlib.Order.Filter.Cocardinal (goal)
Goal:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
S : Set (Set α)
hS : #(↑S : Type u) < c
hSs : ∀ s ∈ S, s ∈ cocardinal α hreg
⊢ #(↑(compl '' S) : Type u) * ⨆ (s : (↑(compl '' S) : Type u)), #(↑(↑s : Set α) : Type u) < c
have apply : #(↑(compl '' S) : Type u) < c.ord.cof
Tactic: apply mul_lt_of_lt hreg.aleph0_le (mk_image_le.trans_lt hS) (iSup_lt_of_lt_cof_ord ..)
-- Lean 4 proof step from Mathlib.Order.Filter.Cocardinal (goal)
Goal:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
S : Set (Set α)
hS : #(↑S : Type u) < c
hSs : ∀ s ∈ S, s ∈ cocardinal α hreg
apply : #(↑(compl '' S) : Type u) < c.ord.cof
⊢ #(↑(compl '' S) : Type u) * ⨆ (s : (↑(compl '' S) : Type u)), #(↑(↑s : Set α) : Type u) < c
have apply₁ : ∀ (i : (↑(compl '' S) : Type u)), #(↑(↑i : Set α) : Type u) < c
Tactic: apply mul_lt_of_lt hreg.aleph0_le (mk_image_le.trans_lt hS) (iSup_lt_of_lt_cof_ord ..)
-- Lean 4 proof step from Mathlib.Order.Filter.Cocardinal (goal)
Goal:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
S : Set (Set α)
hS : #(↑S : Type u) < c
hSs : ∀ s ∈ S, s ∈ cocardinal α hreg
⊢ #(↑(compl '' S) : Type u) < c.ord.cof
have rw : #(↑(compl '' S) : Type u) < c
Tactic: rw [hreg.cof_ord]
-- Lean 4 proof step from Mathlib.Order.Filter.Cocardinal (goal)
Goal:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
s : Set α
h : ∃ (i : Set α), {s : Set α | #(↑s : Type u) < c} i ∧ iᶜ ⊆ s
_t : Set α
htf : {s : Set α | #(↑s : Type u) < c} _t
hts : _tᶜ ⊆ s
⊢ #(↑sᶜ : Type u) < c
have apply : #(↑sᶜ : Type u) ≤ #(↑_t : Type u)
Tactic: apply lt_of_le_of_lt _ htf
-- Lean 4 proof step from Mathlib.Order.Filter.Cocardinal (hypothesis)
Goal:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
s : Set α
h : ∃ (i : Set α), {s : Set α | #(↑s : Type u) < c} i ∧ iᶜ ⊆ s
_t : Set α
htf : {s : Set α | #(↑s : Type u) < c} _t
hts : _tᶜ ⊆ s
⊢ #(↑sᶜ : Type u) ≤ #(↑_t : Type u)
have hts₁ : sᶜ ⊆ _t
Tactic: rw [compl_subset_comm] at hts
Cleared hypotheses: hts
-- Lean 4 proof step from Mathlib.Order.Filter.Cocardinal (hypothesis)
Goal:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
s : Set α
h : ∃ (i : Set α), {s : Set α | #(↑s : Type u) < c} i ∧ iᶜ ⊆ s
_t : Set α
htf : {s : Set α | #(↑s : Type u) < c} _t
hts : _tᶜ ⊆ s
⊢ s ∈ cocardinal α hreg
have this : #(↑sᶜ : Type u) < c
Tactic: have : #↑sᶜ < c := by
        apply lt_of_le_of_lt _ htf
        rw [compl_subset_comm] at hts
        apply Cardinal.mk_le_mk_of_subset hts
-- Lean 4 proof step from Mathlib.Order.Filter.Cocardinal (goal)
Goal:
α : Type u
s : Set α
⊢ Membership.mem (γ := Filter α) cocountable s ↔ sᶜ.Countable
have rw : Membership.mem (γ := Filter α) cocountable s ↔ #(↑sᶜ : Type u) ≤ ℵ₀
Tactic: rw [← Cardinal.le_aleph0_iff_set_countable, mem_cocardinal, lt_aleph_one_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Cocardinal (goal)
Goal:
α : Type u
s : Set α
rw : Membership.mem (γ := Filter α) cocountable s ↔ #(↑sᶜ : Type u) ≤ ℵ₀
⊢ Membership.mem (γ := Filter α) cocountable s ↔ sᶜ.Countable
have rw₁ : #(↑sᶜ : Type u) < (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1 ↔ #(↑sᶜ : Type u) ≤ ℵ₀
Tactic: rw [← Cardinal.le_aleph0_iff_set_countable, mem_cocardinal, lt_aleph_one_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Cocardinal (goal)
Goal:
α : Type u
s : Set α
rw : Membership.mem (γ := Filter α) cocountable s ↔ #(↑sᶜ : Type u) ≤ ℵ₀
rw₁ : #(↑sᶜ : Type u) < (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1 ↔ #(↑sᶜ : Type u) ≤ ℵ₀
⊢ Membership.mem (γ := Filter α) cocountable s ↔ sᶜ.Countable
have rw₂ : #(↑sᶜ : Type u) ≤ ℵ₀ ↔ #(↑sᶜ : Type u) ≤ ℵ₀
Tactic: rw [← Cardinal.le_aleph0_iff_set_countable, mem_cocardinal, lt_aleph_one_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
α : Type u_2
l : Filter α
⊢ l ≤ cofinite ↔ ∀ (x : α), {x}ᶜ ∈ l
have refine : ∀ (h : ∀ (x : α), {x}ᶜ ∈ l) (s : Set α) (hs : sᶜ.Finite), s ∈ l
Tactic: refine ⟨fun h x => h (finite_singleton x).compl_mem_cofinite, fun h s (hs : sᶜ.Finite) => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
α : Type u_2
l : Filter α
h : ∀ (x : α), {x}ᶜ ∈ l
s : Set α
hs : sᶜ.Finite
⊢ s ∈ l
have rw : ∀ i ∈ sᶜ, {i}ᶜ ∈ l
Tactic: rw [← compl_compl s, ← biUnion_of_singleton sᶜ, compl_iUnion₂, Filter.biInter_mem hs]
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
α : Type u_2
l : Filter α
inst : l.IsCountablyGenerated
h : cofinite ≤ l
⊢ l.kerᶜ.Countable
have rcases : ∀ (s : ℕ → Set α) (hs : l.HasAntitoneBasis s), l.kerᶜ.Countable
Tactic: rcases exists_antitone_basis l with ⟨s, hs⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
α : Type u_2
l : Filter α
inst : l.IsCountablyGenerated
h : cofinite ≤ l
s : ℕ → Set α
hs : l.HasAntitoneBasis s
⊢ l.kerᶜ.Countable
have simp : Set.Countable.{u_2} (α := α) (⋃ (i : ℕ), (s i)ᶜ)
Tactic: simp only [hs.ker, iInter_true, compl_iInter]
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
α : Type u_2
β : Type u_3
f : α → β
l : Filter β
inst : l.IsCountablyGenerated
h : Tendsto f cofinite l
⊢ (f ⁻¹' l.ker)ᶜ.Countable
have rw : (comap f l).kerᶜ.Countable
Tactic: rw [← ker_comap]
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
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
⊢ Set.pi (α := α) univ s ∈ pi (α := α) l
have h₁ : ∀ (a : (i : ι) → α i) (ha : a ∈ Set.pi (α := α) {x : ι | s x = univ}ᶜ s) (i : ι),
  Membership.mem (γ := Set ι) univ i → a i ∈ s i
Tactic: filter_upwards [pi_mem_pi hfin fun i _ ↦ h i] with a ha i _
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
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
⊢ a i ∈ s i
have if : ∀ (hi : s i = univ), a i ∈ s i
Tactic: if hi : s i = univ then
    simp [hi]
  else
    exact ha i hi
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
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
⊢ a i ∈ s i
have if₁ : ∀ (hi : ¬s i = univ), a i ∈ s i
Tactic: if hi : s i = univ then
    simp [hi]
  else
    exact ha i hi
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
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)
have refine : (pi (α := β) fun (i : ι) ↦ map (f i) (l i)) ≤ map (Pi.map (α := α) (β := β) f) (pi (α := α) l)
Tactic: refine le_antisymm (tendsto_piMap_pi fun _ ↦ tendsto_map) ?_
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
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)
have 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))
Tactic: refine ((hasBasis_pi fun i ↦ (l i).basis_sets).map _).ge_iff.2 ?_
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
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))
    (Pi.map (α := α) (β := β) f '' (I, s).1.pi (α := α) fun (i : ι) ↦ id ((I, s).2 i))
have 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)
Tactic: rw [← univ_pi_piecewise_univ, piMap_image_univ_pi]
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
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)
have 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)
Tactic: refine univ_pi_mem_pi (fun i ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
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)
⊢ 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)
have 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
Tactic: refine univ_pi_mem_pi (fun i ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
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 : ι
⊢ 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)
have 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)
Tactic: by_cases hi : i ∈ I
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases hi : i ∈ I
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
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)
⊢ i ∈ Iᶜ → f i '' I.piecewise (β := fun (i : ι) ↦ Set (α i)) (fun (i : ι) ↦ id (s i)) (fun (x : ι) ↦ univ) i = univ
have h : ∀ (hiI : i ∉ I),
  f i '' I.piecewise (β := fun (i : ι) ↦ Set (α i)) (fun (i : ι) ↦ id (s i)) (fun (x : ι) ↦ univ) i = univ
Tactic: (hiI : i ∉ I)
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
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 : ι) in cofinite,
    f i '' (I, s).1.piecewise (β := fun (i : ι) ↦ Set (α i)) (fun (i : ι) ↦ id ((I, s).2 i)) (fun (x : ι) ↦ univ) i =
      univ
have 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
Tactic: filter_upwards [hf, hI.compl_mem_cofinite] with i hsurj (hiI : i ∉ I)
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
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))
    (Pi.map (α := α) (β := β) f '' (I, s).1.pi (α := α) fun (i : ι) ↦ id ((I, s).2 i))
have 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))
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]
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
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))
⊢ 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))
have 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)
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]
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
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)
⊢ 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))
have 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)
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]
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
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)
⊢ 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))
have 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
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]
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
α : Type u_2
s t : Set α
ht : t.Finite
⊢ cofinite ⊓ 𝓟 (s \ t) = cofinite ⊓ 𝓟 s
have rw : cofinite ⊓ 𝓟 (s ∩ tᶜ) = cofinite ⊓ 𝓟 s
Tactic: rw [diff_eq, ← inf_principal, ← inf_assoc, inf_right_comm, ht.cofinite_inf_principal_compl]
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
α : Type u_2
s t : Set α
ht : t.Finite
rw : cofinite ⊓ 𝓟 (s ∩ tᶜ) = cofinite ⊓ 𝓟 s
⊢ cofinite ⊓ 𝓟 (s \ t) = cofinite ⊓ 𝓟 s
have rw₁ : cofinite ⊓ (𝓟 s ⊓ 𝓟 tᶜ) = cofinite ⊓ 𝓟 s
Tactic: rw [diff_eq, ← inf_principal, ← inf_assoc, inf_right_comm, ht.cofinite_inf_principal_compl]
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
α : Type u_2
s t : Set α
ht : t.Finite
rw : cofinite ⊓ 𝓟 (s ∩ tᶜ) = cofinite ⊓ 𝓟 s
rw₁ : cofinite ⊓ (𝓟 s ⊓ 𝓟 tᶜ) = cofinite ⊓ 𝓟 s
⊢ cofinite ⊓ 𝓟 (s \ t) = cofinite ⊓ 𝓟 s
have rw₂ : cofinite ⊓ 𝓟 s ⊓ 𝓟 tᶜ = cofinite ⊓ 𝓟 s
Tactic: rw [diff_eq, ← inf_principal, ← inf_assoc, inf_right_comm, ht.cofinite_inf_principal_compl]
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
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
⊢ cofinite ⊓ 𝓟 (s \ t) = cofinite ⊓ 𝓟 s
have rw₃ : cofinite ⊓ 𝓟 tᶜ ⊓ 𝓟 s = cofinite ⊓ 𝓟 s
Tactic: rw [diff_eq, ← inf_principal, ← inf_assoc, inf_right_comm, ht.cofinite_inf_principal_compl]
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
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
⊢ cofinite ⊓ 𝓟 (s \ t) = cofinite ⊓ 𝓟 s
have rw₄ : cofinite ⊓ 𝓟 s = cofinite ⊓ 𝓟 s
Tactic: rw [diff_eq, ← inf_principal, ← inf_assoc, inf_right_comm, ht.cofinite_inf_principal_compl]
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
⊢ Eq (α := Filter ℕ) cofinite atTop
have refine : LE.le (α := Filter ℕ) cofinite atTop
Tactic: refine le_antisymm ?_ atTop_le_cofinite
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
⊢ LE.le (α := Filter ℕ) cofinite atTop
have refine : ∀ (N : ℕ), True → Membership.mem (γ := Filter ℕ) cofinite (Ici N)
Tactic: refine atTop_basis.ge_iff.2 fun N _ => ?_
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
p : ℕ → Prop
⊢ (∃ᶠ (n : ℕ) in atTop, p n) ↔ Set.Infinite (α := ℕ) {n : ℕ | p n}
have rw : (∃ᶠ (n : ℕ) in cofinite, p n) ↔ Set.Infinite (α := ℕ) {n : ℕ | p n}
Tactic: rw [← Nat.cofinite_eq_atTop, frequently_cofinite_iff_infinite]
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
p : ℕ → Prop
rw : (∃ᶠ (n : ℕ) in cofinite, p n) ↔ Set.Infinite (α := ℕ) {n : ℕ | p n}
⊢ (∃ᶠ (n : ℕ) in atTop, p n) ↔ Set.Infinite (α := ℕ) {n : ℕ | p n}
have rw₁ : Set.Infinite (α := ℕ) {x : ℕ | p x} ↔ Set.Infinite (α := ℕ) {n : ℕ | p n}
Tactic: rw [← Nat.cofinite_eq_atTop, frequently_cofinite_iff_infinite]
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
α : Type u_4
β : Type u_5
inst : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a
have pos : ∀ (all_top : ∃ y ∈ s, ∃ (x : β), f y < x), ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a
Tactic: by_cases! all_top : ∃ y ∈ s, ∃ x, f y < x
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
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
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a
have neg : ∀ (all_top : ∀ (y : α) (_ : y ∈ s) (x : β), x ≤ f y), ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a
Tactic: by_cases! all_top : ∃ y ∈ s, ∃ x, f y < x