awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
all_top : ∃ y ∈ s, ∃ (x : β), f y < x
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a
have pos : ∀ (y : α) (hys : y ∈ s) (x : β) (hx : f y < x), ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a
Tactic: rcases all_top with ⟨y, hys, x, hx⟩
Cleared hypotheses: all_top
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (hypothesis)
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
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a
have this : Set.Finite.{u_4} (α := α) {y : α | ¬x ≤ f y}
Tactic: have : { y | ¬x ≤ f y }.Finite := Filter.eventually_cofinite.mp (tendsto_atTop.1 hf x)
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (hypothesis)
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}
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a
have this₁ : Set.Finite.{u_4} (α := α) {y : α | f y < x}
Tactic: simp only [not_le] at this
Cleared hypotheses: this
-- 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
y : α
hys : y ∈ s
x : β
hx : f y < x
this : Set.Finite.{u_4} (α := α) {y : α | f y < x}
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a
have 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
Tactic: obtain ⟨a₀, ⟨ha₀ : f a₀ < x, ha₀s⟩, others_bigger⟩ :=
      exists_min_image _ f (this.inter_of_left s) ⟨y, hx, hys⟩
-- 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
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
have pos : ∀ (a : α) (has : a ∈ s), f a < x → f a₀ ≤ f a
Tactic: refine ⟨a₀, ha₀s, fun a has => (lt_or_ge (f a) x).elim ?_ (le_trans ha₀.le)⟩
-- 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
all_top : ∀ (y : α) (_ : y ∈ s) (x : β), x ≤ f y
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a
have neg : ∀ (a₀ : α) (ha₀s : a₀ ∈ s), ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a
Tactic: obtain ⟨a₀, ha₀s⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
f : α → β
a : α
b : β
⊢ update (β := fun (a : α) ↦ β) f a b =ᶠ[𝓟 {a}ᶜ] f
have h : ∀ (a_1 : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {a}ᶜ x →
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ update (β := fun (a : α) ↦ β) f a b x = f x) x} x}
    a_1
Tactic: filter_upwards [mem_principal_self _] with u hu using Function.update_of_ne hu _ _
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
f : α → β
a : α
b : β
h :
  ∀ (a_1 : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {a}ᶜ x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ update (β := fun (a : α) ↦ β) f a b x = f x) x} x}
      a_1
⊢ update (β := fun (a : α) ↦ β) f a b =ᶠ[𝓟 {a}ᶜ] f
have h₁ : ∀ (a_1 : α), Membership.mem (γ := Set α) {a}ᶜ a_1 → update (β := fun (a : α) ↦ β) f a b a_1 = f a_1
Tactic: filter_upwards [mem_principal_self _] with u hu using Function.update_of_ne hu _ _
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
α : Type u_2
f : Filter α
⊢ f ≤ cofinite ↔ f.ker = ∅
have rw : (∀ (x : α), {x}ᶜ ∈ f) ↔ ∀ (a : α), ∃ (i : Set α) (_ : i ∈ f), a ∉ i
Tactic: rw [le_cofinite_iff_compl_singleton_mem, ker_def, iInter₂_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
α : Type u_2
f : Filter α
⊢ f ≤ cofinite ↔ Coheyting.boundary f = f
have rw : f.ker = ∅ ↔ f.kerᶜ ∈ f
Tactic: rw [← Coheyting.inf_hnot_self, inf_eq_left, le_cofinite_iff_ker,
    Filter.hnot_def, le_principal_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
α : Type u_2
f : Filter α
⊢ f.ker = ∅ ↔ f.kerᶜ ∈ f
have mp : f.ker = ∅ → f.kerᶜ ∈ f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
α : Type u_2
f : Filter α
mp : f.ker = ∅ → f.kerᶜ ∈ f
⊢ f.ker = ∅ ↔ f.kerᶜ ∈ f
have mpr : f.kerᶜ ∈ f → f.ker = ∅
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
α : Type u_2
f : Filter α
h : f.kerᶜ ∈ f
⊢ f.ker = ∅
have mpr : ∀ (x : α), x ∉ f.ker
Tactic: rw [eq_empty_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
α : Type u_2
f : Filter α
⊢ ∃! p : Set α × Filter α, p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2
have refine_1 : (f.ker, Coheyting.boundary f).2 ≤ cofinite
Tactic: refine ⟨(f.ker, Coheyting.boundary f), ⟨?_, ?_, ?_⟩, fun q hq => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
α : Type u_2
f : Filter α
refine_1 : (f.ker, Coheyting.boundary f).2 ≤ cofinite
⊢ ∃! p : Set α × Filter α, p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2
have refine_2 : Disjoint (𝓟 (f.ker, Coheyting.boundary f).1) (f.ker, Coheyting.boundary f).2
Tactic: refine ⟨(f.ker, Coheyting.boundary f), ⟨?_, ?_, ?_⟩, fun q hq => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
α : Type u_2
f : Filter α
refine_1 : (f.ker, Coheyting.boundary f).2 ≤ cofinite
refine_2 : Disjoint (𝓟 (f.ker, Coheyting.boundary f).1) (f.ker, Coheyting.boundary f).2
⊢ ∃! p : Set α × Filter α, p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2
have refine_3 : f = 𝓟 (f.ker, Coheyting.boundary f).1 ⊔ (f.ker, Coheyting.boundary f).2
Tactic: refine ⟨(f.ker, Coheyting.boundary f), ⟨?_, ?_, ?_⟩, fun q hq => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
α : Type u_2
f : Filter α
refine_1 : (f.ker, Coheyting.boundary f).2 ≤ cofinite
refine_2 : Disjoint (𝓟 (f.ker, Coheyting.boundary f).1) (f.ker, Coheyting.boundary f).2
refine_3 : f = 𝓟 (f.ker, Coheyting.boundary f).1 ⊔ (f.ker, Coheyting.boundary f).2
⊢ ∃! p : Set α × Filter α, p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2
have refine_4 : ∀ (q : Set α × Filter α)
  (hq : (fun (p : Set α × Filter α) ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q),
  q = (f.ker, Coheyting.boundary f)
Tactic: refine ⟨(f.ker, Coheyting.boundary f), ⟨?_, ?_, ?_⟩, fun q hq => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
α : Type u_2
f : Filter α
⊢ Disjoint (𝓟 (f.ker, Coheyting.boundary f).1) (f.ker, Coheyting.boundary f).2
have refine_2 : (f.ker, Coheyting.boundary f).1ᶜ ∈ (f.ker, Coheyting.boundary f).2
Tactic: rw [disjoint_principal_left]
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
α : Type u_2
f : Filter α
⊢ f = 𝓟 (f.ker, Coheyting.boundary f).1 ⊔ (f.ker, Coheyting.boundary f).2
have refine_3 : f = 𝓟 (f.kerᶜᶜ, Coheyting.boundary f).1 ⊔ (f.kerᶜᶜ, Coheyting.boundary f).2
Tactic: rw [← compl_compl f.ker, ← hnot_principal, ← Filter.hnot_def,
      Coheyting.hnot_hnot_sup_boundary]
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
α : Type u_2
f : Filter α
refine_3 : f = 𝓟 (f.kerᶜᶜ, Coheyting.boundary f).1 ⊔ (f.kerᶜᶜ, Coheyting.boundary f).2
⊢ f = 𝓟 (f.ker, Coheyting.boundary f).1 ⊔ (f.ker, Coheyting.boundary f).2
have refine_3₁ : f = ￢𝓟 f.kerᶜ ⊔ (f.kerᶜᶜ, Coheyting.boundary f).2
Tactic: rw [← compl_compl f.ker, ← hnot_principal, ← Filter.hnot_def,
      Coheyting.hnot_hnot_sup_boundary]
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
α : Type u_2
f : Filter α
refine_3 : f = 𝓟 (f.kerᶜᶜ, Coheyting.boundary f).1 ⊔ (f.kerᶜᶜ, Coheyting.boundary f).2
refine_3₁ : f = ￢𝓟 f.kerᶜ ⊔ (f.kerᶜᶜ, Coheyting.boundary f).2
⊢ f = 𝓟 (f.ker, Coheyting.boundary f).1 ⊔ (f.ker, Coheyting.boundary f).2
have refine_3₂ : f = ￢￢f ⊔ (f.kerᶜᶜ, Coheyting.boundary f).2
Tactic: rw [← compl_compl f.ker, ← hnot_principal, ← Filter.hnot_def,
      Coheyting.hnot_hnot_sup_boundary]
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
α : Type u_2
f : Filter α
refine_3 : f = 𝓟 (f.kerᶜᶜ, Coheyting.boundary f).1 ⊔ (f.kerᶜᶜ, Coheyting.boundary f).2
refine_3₁ : f = ￢𝓟 f.kerᶜ ⊔ (f.kerᶜᶜ, Coheyting.boundary f).2
refine_3₂ : f = ￢￢f ⊔ (f.kerᶜᶜ, Coheyting.boundary f).2
⊢ f = 𝓟 (f.ker, Coheyting.boundary f).1 ⊔ (f.ker, Coheyting.boundary f).2
have refine_3₃ : f = f
Tactic: rw [← compl_compl f.ker, ← hnot_principal, ← Filter.hnot_def,
      Coheyting.hnot_hnot_sup_boundary]
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (hypothesis)
Goal:
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun (p : Set α × Filter α) ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
⊢ q = (f.ker, Coheyting.boundary f)
have hqk : f.ker = (𝓟 q.1 ⊔ q.2).ker
Tactic: have hqk := congrArg Filter.ker hq.2.2
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (hypothesis)
Goal:
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun (p : Set α × Filter α) ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = (𝓟 q.1 ⊔ q.2).ker
⊢ q = (f.ker, Coheyting.boundary f)
have hqk₁ : f.ker = q.1
Tactic: rw [ker_sup, ker_principal, le_cofinite_iff_ker.mp hq.1, union_empty] at hqk
Cleared hypotheses: hqk
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun (p : Set α × Filter α) ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
⊢ q = (f.ker, Coheyting.boundary f)
have refine_4 : q.2 ≤ f
Tactic: refine congrArg₂ Prod.mk hqk.symm (le_antisymm (le_inf ?_ ?_) ?_)
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun (p : Set α × Filter α) ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
refine_4 : q.2 ≤ f
⊢ q = (f.ker, Coheyting.boundary f)
have refine_4₁ : q.2 ≤ ￢f
Tactic: refine congrArg₂ Prod.mk hqk.symm (le_antisymm (le_inf ?_ ?_) ?_)
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun (p : Set α × Filter α) ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
refine_4 : q.2 ≤ f
refine_4₁ : q.2 ≤ ￢f
⊢ q = (f.ker, Coheyting.boundary f)
have refine_4₂ : Coheyting.boundary f ≤ q.2
Tactic: refine congrArg₂ Prod.mk hqk.symm (le_antisymm (le_inf ?_ ?_) ?_)
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun (p : Set α × Filter α) ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
⊢ q.2 ≤ f
have refine_4 : q.2 ≤ 𝓟 q.1 ⊔ q.2
Tactic: rw [hq.2.2]
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun (p : Set α × Filter α) ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
⊢ q.2 ≤ ￢f
have refine_4 : Disjoint (𝓟 q.1) q.2
Tactic: rw [Filter.hnot_def, le_principal_iff, ← disjoint_principal_left, hqk]
-- Lean 4 proof step from Mathlib.Order.Filter.Cofinite (goal)
Goal:
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun (p : Set α × Filter α) ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
⊢ Coheyting.boundary f ≤ q.2
have refine_4 : Coheyting.boundary q.2 ≤ q.2
Tactic: grw [hq.2.2, Coheyting.boundary_sup_le, boundary_principal, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
Goal:
α : Type u_2
l : Filter α
inst : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s : (i : ι) → i ∈ S → Set α
⊢ ⋂ (i : ι), ⋂ (hi : i ∈ S), s i hi ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
have rw : ⋂ (x : (↑S : Type u_4)), s (↑x : ι) sorry ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
Tactic: rw [biInter_eq_iInter]
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
Goal:
α : Type u_2
l : Filter α
inst : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s : (i : ι) → i ∈ S → Set α
⊢ ⋂ (x : (↑S : Type u_4)), s (↑x : ι) ⋯ ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
have haveI : ∀ (this : Encodable (↑S : Type u_4)), ⋂ (x : (↑S : Type u_4)), s (↑x : ι) sorry ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
Tactic: haveI := hS.toEncodable
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
Goal:
α : Type u_2
l : Filter α
inst : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋃ (i : ι), ⋃ (h : i ∈ S), s i h ≤ᶠ[l] ⋃ (i : ι), ⋃ (h : i ∈ S), t i h
have simp : ⋃ (x : (↑S : Type u_4)), s (↑x : ι) sorry ≤ᶠ[l] ⋃ (x : (↑S : Type u_4)), t (↑x : ι) sorry
Tactic: simp only [biUnion_eq_iUnion]
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
Goal:
α : Type u_2
l : Filter α
inst : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋃ (x : (↑S : Type u_4)), s (↑x : ι) ⋯ ≤ᶠ[l] ⋃ (x : (↑S : Type u_4)), t (↑x : ι) ⋯
have haveI : ∀ (this : Encodable (↑S : Type u_4)), ⋃ (x : (↑S : Type u_4)), s (↑x : ι) sorry ≤ᶠ[l] ⋃ (x : (↑S : Type u_4)), t (↑x : ι) sorry
Tactic: haveI := hS.toEncodable
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
Goal:
α : Type u_2
l : Filter α
inst : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋂ (i : ι), ⋂ (h : i ∈ S), s i h ≤ᶠ[l] ⋂ (i : ι), ⋂ (h : i ∈ S), t i h
have simp : ⋂ (x : (↑S : Type u_4)), s (↑x : ι) sorry ≤ᶠ[l] ⋂ (x : (↑S : Type u_4)), t (↑x : ι) sorry
Tactic: simp only [biInter_eq_iInter]
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
Goal:
α : Type u_2
l : Filter α
inst : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋂ (x : (↑S : Type u_4)), s (↑x : ι) ⋯ ≤ᶠ[l] ⋂ (x : (↑S : Type u_4)), t (↑x : ι) ⋯
have haveI : ∀ (this : Encodable (↑S : Type u_4)), ⋂ (x : (↑S : Type u_4)), s (↑x : ι) sorry ≤ᶠ[l] ⋂ (x : (↑S : Type u_4)), t (↑x : ι) sorry
Tactic: haveI := hS.toEncodable
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
⊢ Filter α
have refine_1 : ∀ (S : Set (Set α)) (hSc : S.Countable) (hSp : S ⊆ {s : Set α | sᶜ ∈ l}),
  Membership.mem (γ := Set (Set α)) {s : Set α | sᶜ ∈ l} (⋂₀ S)
Tactic: refine .ofCountableInter {s | sᶜ ∈ l} (fun S hSc hSp ↦ ?_) fun s t ht hsub ↦ ?_
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
refine_1 :
  ∀ (S : Set (Set α)) (hSc : S.Countable) (hSp : S ⊆ {s : Set α | sᶜ ∈ l}),
    Membership.mem (γ := Set (Set α)) {s : Set α | sᶜ ∈ l} (⋂₀ S)
⊢ Filter α
have refine_2 : ∀ (s t : Set α) (ht : Membership.mem (γ := Set (Set α)) {s : Set α | sᶜ ∈ l} s) (hsub : s ⊆ t),
  Membership.mem (γ := Set (Set α)) {s : Set α | sᶜ ∈ l} t
Tactic: refine .ofCountableInter {s | sᶜ ∈ l} (fun S hSc hSp ↦ ?_) fun s t ht hsub ↦ ?_
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : S ⊆ {s : Set α | sᶜ ∈ l}
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | sᶜ ∈ l} (⋂₀ S)
have refine_1 : ⋃₀ (compl '' S) ∈ l
Tactic: rw [mem_setOf_eq, compl_sInter]
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : S ⊆ {s : Set α | sᶜ ∈ l}
⊢ ⋃₀ (compl '' S) ∈ l
have refine_1 : ∀ s ∈ compl '' S, s ∈ l
Tactic: apply hUnion (compl '' S) (hSc.image _)
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (hypothesis)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : S ⊆ {s : Set α | sᶜ ∈ l}
s : Set α
hs : s ∈ compl '' S
⊢ s ∈ l
have hs₁ : ∃ x ∈ S, xᶜ = s
Tactic: rw [mem_image] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : S ⊆ {s : Set α | sᶜ ∈ l}
s : Set α
hs : ∃ x ∈ S, xᶜ = s
⊢ s ∈ l
have refine_1 : ∀ (t : Set α) (ht : t ∈ S), tᶜ ∈ l
Tactic: rcases hs with ⟨t, ht, rfl⟩
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
s t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | sᶜ ∈ l} s
hsub : s ⊆ t
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | sᶜ ∈ l} t
have refine_2 : tᶜ ∈ l
Tactic: rw [mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (hypothesis)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
s t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | sᶜ ∈ l} s
hsub : s ⊆ t
⊢ tᶜ ∈ l
have hsub₁ : tᶜ ⊆ sᶜ
Tactic: rw [← compl_subset_compl] at hsub
Cleared hypotheses: hsub
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst : CountableInterFilter l
⊢ CountableInterFilter.{u_2} (α := α) ⊥
have rw : CountableInterFilter.{u_2} (α := α) (𝓟 ∅)
Tactic: rw [← principal_empty]
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst : CountableInterFilter l
⊢ CountableInterFilter.{u_2} (α := α) ⊤
have rw : CountableInterFilter.{u_2} (α := α) (𝓟 univ)
Tactic: rw [← principal_univ]
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Filter β
inst_1 : CountableInterFilter l
f : α → β
⊢ CountableInterFilter (comap f l)
have refine : ∀ (S : Set (Set α)) (hSc : S.Countable) (hS : ∀ s ∈ S, s ∈ comap f l), ⋂₀ S ∈ comap f l
Tactic: refine ⟨fun S hSc hS => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Filter β
inst_1 : CountableInterFilter l
f : α → β
S : Set (Set α)
hSc : S.Countable
hS : ∀ s ∈ S, s ∈ comap f l
⊢ ⋂₀ S ∈ comap f l
have choose! : ∀ (t : (s : Set α) → Set β) (htl : ∀ s ∈ S, t s ∈ l) (ht : ∀ s ∈ S, f ⁻¹' t s ⊆ s), ⋂₀ S ∈ comap f l
Tactic: choose! t htl ht using hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (hypothesis)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Filter β
inst_1 : CountableInterFilter l
f : α → β
S : Set (Set α)
hSc : S.Countable
t : (s : Set α) → Set β
htl : ∀ s ∈ S, t s ∈ l
ht : ∀ s ∈ S, f ⁻¹' t s ⊆ s
⊢ ⋂₀ S ∈ comap f l
have this : ⋂ s ∈ S, t s ∈ l
Tactic: have : (⋂ s ∈ S, t s) ∈ l := (countable_bInter_mem hSc).2 htl
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Filter β
inst_1 : CountableInterFilter l
f : α → β
S : Set (Set α)
hSc : S.Countable
t : (s : Set α) → Set β
htl : ∀ s ∈ S, t s ∈ l
ht : ∀ s ∈ S, f ⁻¹' t s ⊆ s
this : ⋂ s ∈ S, t s ∈ l
⊢ ⋂₀ S ∈ comap f l
have refine : f ⁻¹' ⋂ s ∈ S, t s ⊆ ⋂₀ S
Tactic: refine ⟨_, this, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Filter α
inst_1 : CountableInterFilter l
f : α → β
⊢ CountableInterFilter (map f l)
have refine : ∀ (S : Set (Set β)) (hSc : S.Countable) (hS : ∀ s ∈ S, s ∈ map f l), ⋂₀ S ∈ map f l
Tactic: refine ⟨fun S hSc hS => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l_1 : Filter α
inst : CountableInterFilter l_1
l : Filter α
inst_1 : CountableInterFilter l
f : α → β
S : Set (Set β)
hSc : S.Countable
hS : ∀ s ∈ S, s ∈ map f l
⊢ ⋂₀ S ∈ map f l
have simp : ∀ (hS : ∀ s ∈ S, f ⁻¹' s ∈ l), ⋂ i ∈ S, f ⁻¹' i ∈ l
Tactic: simp only [mem_map, sInter_eq_biInter, preimage_iInter₂] at hS ⊢
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst : CountableInterFilter l
l₁ l₂ : Filter α
inst_1 : CountableInterFilter l₁
inst_2 : CountableInterFilter l₂
⊢ CountableInterFilter (l₁ ⊓ l₂)
have refine : ∀ (S : Set (Set α)) (hSc : S.Countable) (hS : ∀ s ∈ S, s ∈ l₁ ⊓ l₂), ⋂₀ S ∈ l₁ ⊓ l₂
Tactic: refine ⟨fun S hSc hS => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst : CountableInterFilter l
l₁ l₂ : Filter α
inst_1 : CountableInterFilter l₁
inst_2 : CountableInterFilter l₂
S : Set (Set α)
hSc : S.Countable
hS : ∀ s ∈ S, s ∈ l₁ ⊓ l₂
⊢ ⋂₀ S ∈ l₁ ⊓ l₂
have choose : ∀ (s : (s : Set α) → s ∈ S → Set α) (hs : ∀ (s_1 : Set α) (a : s_1 ∈ S), s s_1 a ∈ l₁) (t : (s : Set α) → s ∈ S → Set α)
  (ht : ∀ (s : Set α) (a : s ∈ S), t s a ∈ l₂) (hst : ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a),
  ⋂₀ S ∈ l₁ ⊓ l₂
Tactic: choose s hs t ht hst using hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (hypothesis)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst : CountableInterFilter l
l₁ l₂ : Filter α
inst_1 : CountableInterFilter l₁
inst_2 : CountableInterFilter l₂
S : Set (Set α)
hSc : S.Countable
s : (s : Set α) → s ∈ S → Set α
hs : ∀ (s_1 : Set α) (a : s_1 ∈ S), s s_1 a ∈ l₁
t : (s : Set α) → s ∈ S → Set α
ht : ∀ (s : Set α) (a : s ∈ S), t s a ∈ l₂
hst : ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a
⊢ ⋂₀ S ∈ l₁ ⊓ l₂
have hs₁ : ⋂ (i : Set α), ⋂ (h : i ∈ S), s i h ∈ l₁
Tactic: replace hs : (⋂ i ∈ S, s i ‹_›) ∈ l₁ := (countable_bInter_mem hSc).2 hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.Filter.CountableInter (hypothesis)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst : CountableInterFilter l
l₁ l₂ : Filter α
inst_1 : CountableInterFilter l₁
inst_2 : CountableInterFilter l₂
S : Set (Set α)
hSc : S.Countable
s t : (s : Set α) → s ∈ S → Set α
ht : ∀ (s : Set α) (a : s ∈ S), t s a ∈ l₂
hst : ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a
hs : ⋂ (i : Set α), ⋂ (h : i ∈ S), s i h ∈ l₁
⊢ ⋂₀ S ∈ l₁ ⊓ l₂
have ht₁ : ⋂ (i : Set α), ⋂ (h : i ∈ S), t i h ∈ l₂
Tactic: replace ht : (⋂ i ∈ S, t i ‹_›) ∈ l₂ := (countable_bInter_mem hSc).2 ht
Cleared hypotheses: ht