awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.CountableSeparatingOn (goal)
Goal:
α : Type u_1
p : Set α → Prop
t : Set α
q : Set (↑t : Type u_1) → Prop
h_1 : HasCountableSeparatingOn (↑t : Type u_1) q univ
hpq : ∀ (U : Set (↑t : Type u_1)), q U → ∃ (V : Set α), p V ∧ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' V = U
S : Set (Set (↑t : Type u_1))
hSc : S.Countable
hSq : ∀ s ∈ S, q s
hS :
  ∀ (x : (↑t : Type u_1)),
    Membership.mem (γ := Set (↑t : Type u_1)) univ x →
      ∀ (y : (↑t : Type u_1)), Membership.mem (γ := Set (↑t : Type u_1)) univ y → (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
V : (s : Set (↑t : Type u_1)) → Set α
hpV : ∀ (s : Set (↑t : Type u_1)) (hs : s ∈ S), p (V s)
hV : ∀ (s : Set (↑t : Type u_1)) (hs : s ∈ S), Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' V s = s
x : α
hx : x ∈ t
y : α
hy : y ∈ t
h : ∀ s ∈ V '' S, x ∈ s ↔ y ∈ s
U : Set (↑t : Type u_1)
hU : U ∈ S
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ t) x hx ∈ U ↔ Subtype.mk (p := fun (x : α) ↦ x ∈ t) y hy ∈ U
have rw : Membership.mem (γ := Set (↑t : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' V U)
    (Subtype.mk (p := fun (x : α) ↦ x ∈ t) x hx) ↔
  Membership.mem (γ := Set (↑t : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' V U)
    (Subtype.mk (p := fun (x : α) ↦ x ∈ t) y hy)
Tactic: rw [← hV U hU]
-- Lean 4 proof step from Mathlib.Order.Filter.CountableSeparatingOn (goal)
Goal:
α : Type u_1
p : Set α → Prop
t : Set α
⊢ HasCountableSeparatingOn.{u_1} (↑t : Type u_1)
      (fun (u : Set (↑t : Type u_1)) ↦ ∃ (v : Set α), p v ∧ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' v = u) univ ↔
    HasCountableSeparatingOn α p t
have mp : HasCountableSeparatingOn.{u_1} (↑t : Type u_1)
    (fun (u : Set (↑t : Type u_1)) ↦ ∃ (v : Set α), p v ∧ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' v = u) univ →
  HasCountableSeparatingOn α p t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.CountableSeparatingOn (goal)
Goal:
α : Type u_1
p : Set α → Prop
t : Set α
mp :
  HasCountableSeparatingOn.{u_1} (↑t : Type u_1)
      (fun (u : Set (↑t : Type u_1)) ↦ ∃ (v : Set α), p v ∧ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' v = u) univ →
    HasCountableSeparatingOn α p t
⊢ HasCountableSeparatingOn.{u_1} (↑t : Type u_1)
      (fun (u : Set (↑t : Type u_1)) ↦ ∃ (v : Set α), p v ∧ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' v = u) univ ↔
    HasCountableSeparatingOn α p t
have mpr : HasCountableSeparatingOn α p t →
  HasCountableSeparatingOn.{u_1} (↑t : Type u_1)
    (fun (u : Set (↑t : Type u_1)) ↦ ∃ (v : Set α), p v ∧ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' v = u) univ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.CountableSeparatingOn (goal)
Goal:
α : Type u_1
p : Set α → Prop
t : Set α
h : HasCountableSeparatingOn α p t
⊢ HasCountableSeparatingOn.{u_1} (↑t : Type u_1)
    (fun (u : Set (↑t : Type u_1)) ↦ ∃ (v : Set α), p v ∧ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' v = u) univ
have mpr : ∀ (S : Set (Set α)) (Sct : S.Countable) (Sp : ∀ s ∈ S, p s) (hS : ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y),
  HasCountableSeparatingOn.{u_1} (↑t : Type u_1)
    (fun (u : Set (↑t : Type u_1)) ↦ ∃ (v : Set α), p v ∧ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' v = u) univ
Tactic: rcases h with ⟨S, Sct, Sp, hS⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.CountableSeparatingOn (goal)
Goal:
α : Type u_1
p : Set α → Prop
t : Set α
S : Set (Set α)
Sct : S.Countable
Sp : ∀ s ∈ S, p s
hS : ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ HasCountableSeparatingOn.{u_1} (↑t : Type u_1)
    (fun (u : Set (↑t : Type u_1)) ↦ ∃ (v : Set α), p v ∧ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' v = u) univ
have left : ∀ (s : Set (↑t : Type u_1)),
  Membership.mem (γ := Set (Set (↑t : Type u_1)))
      {x : Set (↑t : Type u_1) | ∃ s ∈ S, Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' s = x} s →
    ∃ (v : Set α), p v ∧ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' v = s
Tactic: use {Subtype.val ⁻¹' s | s ∈ S}, Sct.image _, ?_, ?_
-- Lean 4 proof step from Mathlib.Order.Filter.CountableSeparatingOn (goal)
Goal:
α : Type u_1
p : Set α → Prop
t : Set α
S : Set (Set α)
Sct : S.Countable
Sp : ∀ s ∈ S, p s
hS : ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
left :
  ∀ (s : Set (↑t : Type u_1)),
    Membership.mem (γ := Set (Set (↑t : Type u_1)))
        {x : Set (↑t : Type u_1) | ∃ s ∈ S, Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' s = x} s →
      ∃ (v : Set α), p v ∧ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' v = s
⊢ HasCountableSeparatingOn.{u_1} (↑t : Type u_1)
    (fun (u : Set (↑t : Type u_1)) ↦ ∃ (v : Set α), p v ∧ Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' v = u) univ
have right : ∀ (x : (↑t : Type u_1)),
  Membership.mem (γ := Set (↑t : Type u_1)) univ x →
    ∀ (y : (↑t : Type u_1)),
      Membership.mem (γ := Set (↑t : Type u_1)) univ y →
        (∀ (s : Set (↑t : Type u_1)),
            Membership.mem (γ := Set (Set (↑t : Type u_1)))
                {x : Set (↑t : Type u_1) | ∃ s ∈ S, Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' s = x} s →
              (x ∈ s ↔ y ∈ s)) →
          x = y
Tactic: use {Subtype.val ⁻¹' s | s ∈ S}, Sct.image _, ?_, ?_
-- Lean 4 proof step from Mathlib.Order.Filter.CountableSeparatingOn (goal)
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
⊢ ∃ t ⊆ s, t.Subsingleton ∧ t ∈ l
have rcases : ∀ (S : Set (Set α)) (hSc : S.Countable) (hSp : ∀ s ∈ S, p s) (hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y),
  ∃ t ⊆ s, t.Subsingleton ∧ t ∈ l
Tactic: rcases h.1 with ⟨S, hSc, hSp, hS⟩
-- Lean 4 proof step from Mathlib.Order.Filter.CountableSeparatingOn (goal)
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ ∃ t ⊆ s, t.Subsingleton ∧ t ∈ l
have refine_1 : s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ ⊆ s
Tactic: refine ⟨s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ (U ∈ S) (_ : Uᶜ ∈ l), Uᶜ, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.CountableSeparatingOn (goal)
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
refine_1 : s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ ⊆ s
⊢ ∃ t ⊆ s, t.Subsingleton ∧ t ∈ l
have refine_2 : (s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ).Subsingleton
Tactic: refine ⟨s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ (U ∈ S) (_ : Uᶜ ∈ l), Uᶜ, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.CountableSeparatingOn (goal)
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
refine_1 : s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ ⊆ s
refine_2 : (s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ).Subsingleton
⊢ ∃ t ⊆ s, t.Subsingleton ∧ t ∈ l
have refine_3 : s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ ∈ l
Tactic: refine ⟨s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ (U ∈ S) (_ : Uᶜ ∈ l), Uᶜ, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.CountableSeparatingOn (hypothesis)
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
x : α
hx : x ∈ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ
y : α
hy : y ∈ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ
⊢ x = y
have hx₁ : (x ∈ s ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → x ∈ t) ∧ ∀ (i : Set α) (i_1 : i ∈ S) (i_2 : iᶜ ∈ l), x ∉ i
Tactic: simp only [mem_sInter, mem_inter_iff, mem_iInter, mem_compl_iff] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Order.Filter.CountableSeparatingOn (hypothesis)
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
x : α
hx : x ∈ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ
y : α
hy : y ∈ s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ U ∈ S, ⋂ (_ : Uᶜ ∈ l), Uᶜ
hx₁ : (x ∈ s ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → x ∈ t) ∧ ∀ (i : Set α) (i_1 : i ∈ S) (i_2 : iᶜ ∈ l), x ∉ i
⊢ x = y
have hy₁ : (y ∈ s ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → y ∈ t) ∧ ∀ (i : Set α) (i_1 : i ∈ S) (i_2 : iᶜ ∈ l), y ∉ i
Tactic: simp only [mem_sInter, mem_inter_iff, mem_iInter, mem_compl_iff] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Order.Filter.CountableSeparatingOn (goal)
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
x y : α
hx : (x ∈ s ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → x ∈ t) ∧ ∀ (i : Set α) (i_1 : i ∈ S) (i_2 : iᶜ ∈ l), x ∉ i
hy : (y ∈ s ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → y ∈ t) ∧ ∀ (i : Set α) (i_1 : i ∈ S) (i_2 : iᶜ ∈ l), y ∉ i
⊢ x = y
have refine_2 : ∀ (s : Set α) (hsS : s ∈ S), x ∈ s ↔ y ∈ s
Tactic: refine hS x hx.1.1 y hy.1.1 (fun s hsS ↦ ?_)
-- Lean 4 proof step from Mathlib.Order.Filter.CountableSeparatingOn (hypothesis)
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
p : Set α → Prop
s_1 : Set α
h : HasCountableSeparatingOn α p s_1
hs : s_1 ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s_1, ∀ y ∈ s_1, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
x y : α
hx : (x ∈ s_1 ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → x ∈ t) ∧ ∀ (i : Set α) (i_1 : i ∈ S) (i_2 : iᶜ ∈ l), x ∉ i
hy : (y ∈ s_1 ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → y ∈ t) ∧ ∀ (i : Set α) (i_1 : i ∈ S) (i_2 : iᶜ ∈ l), y ∉ i
s : Set α
hsS : s ∈ S
⊢ x ∈ s ↔ y ∈ s
have x₁ : s ∈ l ∨ sᶜ ∈ l
Tactic: cases hl s (hSp s hsS) with
    | inl hsl => simp only [hx.1.2 s ⟨hsS, hsl⟩, hy.1.2 s ⟨hsS, hsl⟩]
    | inr hsl => simp only [hx.2 s hsS hsl, hy.2 s hsS hsl]
-- Lean 4 proof step from Mathlib.Order.Filter.CountableSeparatingOn (goal)
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
p : Set α → Prop
s : Set α
inst_1 : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : s.Nonempty
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
⊢ ∃ a ∈ s, {a} ∈ l
have rcases : ∀ (t : Set α) (hts : t ⊆ s) (ht : t.Subsingleton) (htl : t ∈ l), ∃ a ∈ s, {a} ∈ l
Tactic: rcases exists_subset_subsingleton_mem_of_forall_separating p hs hl with ⟨t, hts, ht, htl⟩
-- Lean 4 proof step from Mathlib.Order.Filter.CountableSeparatingOn (goal)
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
p : Set α → Prop
s : Set α
inst_1 : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : s.Nonempty
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
t : Set α
hts : t ⊆ s
ht : t.Subsingleton
htl : t ∈ l
⊢ ∃ a ∈ s, {a} ∈ l
have inl : ∀ (hts : ∅ ⊆ s) (ht : Set.Subsingleton.{u_1} (α := α) ∅) (htl : ∅ ∈ l), ∃ a ∈ s, {a} ∈ l
Tactic: rcases ht.eq_empty_or_singleton with rfl | ⟨x, rfl⟩
Cleared hypotheses: t, hts, ht, htl
-- Lean 4 proof step from Mathlib.Order.Filter.CountableSeparatingOn (goal)
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
p : Set α → Prop
s : Set α
inst_1 : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : s.Nonempty
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
t : Set α
hts : t ⊆ s
ht : t.Subsingleton
htl : t ∈ l
inl : ∀ (hts : ∅ ⊆ s) (ht : Set.Subsingleton.{u_1} (α := α) ∅) (htl : ∅ ∈ l), ∃ a ∈ s, {a} ∈ l
⊢ ∃ a ∈ s, {a} ∈ l
have inr : ∀ (x : α) (hts : {x} ⊆ s) (ht : Set.Subsingleton (α := α) {x}) (htl : {x} ∈ l), ∃ a ∈ s, {a} ∈ l
Tactic: rcases ht.eq_empty_or_singleton with rfl | ⟨x, rfl⟩
Cleared hypotheses: t, hts, ht, htl
-- Lean 4 proof step from Mathlib.Order.Filter.CountableSeparatingOn (goal)
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
inst_1 : Nonempty α
p : Set α → Prop
s : Set α
inst_2 : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
⊢ ∃ (a : α), {a} ∈ l
have inl : ∀ [HasCountableSeparatingOn α p ∅] (hs : ∅ ∈ l), ∃ (a : α), {a} ∈ l
Tactic: rcases s.eq_empty_or_nonempty with rfl | hne
Cleared hypotheses: s, inst_2, hs
-- Lean 4 proof step from Mathlib.Order.Filter.CountableSeparatingOn (goal)
Goal:
α : Type u_1
l : Filter α
inst : CountableInterFilter l
inst_1 : Nonempty α
p : Set α → Prop
s : Set α
inst_2 : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
inl : ∀ [HasCountableSeparatingOn α p ∅] (hs : ∅ ∈ l), ∃ (a : α), {a} ∈ l
⊢ ∃ (a : α), {a} ∈ l
have inr : ∀ (hne : s.Nonempty), ∃ (a : α), {a} ∈ l
Tactic: rcases s.eq_empty_or_nonempty with rfl | hne
-- Lean 4 proof step from Mathlib.Order.Filter.CountableSeparatingOn (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : CountableInterFilter l
f g : α → β
p : Set β → Prop
s : Set β
h' : HasCountableSeparatingOn β p s
hf : ∀ᶠ (x : α) in l, f x ∈ s
hg : ∀ᶠ (x : α) in l, g x ∈ s
h : ∀ (U : Set β), p U → ∀ᶠ (x : α) in l, f x ∈ U ↔ g x ∈ U
⊢ f =ᶠ[l] g
have rcases : ∀ (S : Set (Set β)) (hSc : S.Countable) (hSp : ∀ s ∈ S, p s) (hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y),
  f =ᶠ[l] g
Tactic: rcases h'.1 with ⟨S, hSc, hSp, hS⟩
-- Lean 4 proof step from Mathlib.Order.Filter.CountableSeparatingOn (hypothesis)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : CountableInterFilter l
f g : α → β
p : Set β → Prop
s : Set β
h' : HasCountableSeparatingOn β p s
hf : ∀ᶠ (x : α) in l, f x ∈ s
hg : ∀ᶠ (x : α) in l, g x ∈ s
h : ∀ (U : Set β), p U → ∀ᶠ (x : α) in l, f x ∈ U ↔ g x ∈ U
S : Set (Set β)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ f =ᶠ[l] g
have H : ∀ᶠ (x : α) in l, ∀ s ∈ S, f x ∈ s ↔ g x ∈ s
Tactic: have H : ∀ᶠ x in l, ∀ s ∈ S, f x ∈ s ↔ g x ∈ s :=
    (eventually_countable_ball hSc).2 fun s hs ↦ (h _ (hSp _ hs))
-- Lean 4 proof step from Mathlib.Order.Filter.CountableSeparatingOn (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : CountableInterFilter l
f g : α → β
p : Set β → Prop
s : Set β
h' : HasCountableSeparatingOn β p s
hf : ∀ᶠ (x : α) in l, f x ∈ s
hg : ∀ᶠ (x : α) in l, g x ∈ s
h : ∀ (U : Set β), p U → ∀ᶠ (x : α) in l, f x ∈ U ↔ g x ∈ U
S : Set (Set β)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
H : ∀ᶠ (x : α) in l, ∀ s ∈ S, f x ∈ s ↔ g x ∈ s
⊢ f =ᶠ[l] g
have h₁ : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ∀ s ∈ S, f x ∈ s ↔ g x ∈ s) x} x →
        Membership.mem (γ := Set α)
          {x : α |
            Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ∈ s) x} x →
              Membership.mem (γ := Set α)
                {x : α |
                  Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ g x ∈ s) x} x →
                    Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x = g x) x} x}
                x}
          x}
    a
Tactic: filter_upwards [H, hf, hg] with x hx hxf hxg using hS _ hxf _ hxg hx
-- Lean 4 proof step from Mathlib.Order.Filter.CountableSeparatingOn (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : CountableInterFilter l
f g : α → β
p : Set β → Prop
s : Set β
h' : HasCountableSeparatingOn β p s
hf : ∀ᶠ (x : α) in l, f x ∈ s
hg : ∀ᶠ (x : α) in l, g x ∈ s
h : ∀ (U : Set β), p U → ∀ᶠ (x : α) in l, f x ∈ U ↔ g x ∈ U
S : Set (Set β)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
H : ∀ᶠ (x : α) in l, ∀ s ∈ S, f x ∈ s ↔ g x ∈ s
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ∀ s ∈ S, f x ∈ s ↔ g x ∈ s) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ∈ s) x} x →
                Membership.mem (γ := Set α)
                  {x : α |
                    Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ g x ∈ s) x} x →
                      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x = g x) x} x}
                  x}
            x}
      a
⊢ f =ᶠ[l] g
have h₂ : ∀ (a : α), (∀ s ∈ S, f a ∈ s ↔ g a ∈ s) → f a ∈ s → g a ∈ s → f a = g a
Tactic: filter_upwards [H, hf, hg] with x hx hxf hxg using hS _ hxf _ hxg hx
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α : Type u_1
s : ℕ → Set α
⊢ ∃ (t : ℕ → Set α), Antitone t ∧ Eq.{u_1 + 1} (α := Filter α) (⨅ (i : ℕ), 𝓟 (s i)) (⨅ (i : ℕ), 𝓟 (t i))
have h : (Antitone.{0, u_1} (β := Set α) fun (n : ℕ) ↦ ⋂ (m : ℕ), ⋂ (_ : m ≤ n), s m) ∧
  Eq.{u_1 + 1} (α := Filter α) (⨅ (i : ℕ), 𝓟 (s i))
    (⨅ (i : ℕ), 𝓟 ((fun (n : ℕ) ↦ (⋂ (m : ℕ), ⋂ (_ : m ≤ n), s m : Set α)) i))
Tactic: use fun n => ⋂ m ≤ n, s m
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α : Type u_1
s : ℕ → Set α
⊢ (Antitone.{0, u_1} (β := Set α) fun (n : ℕ) ↦ ⋂ (m : ℕ), ⋂ (_ : m ≤ n), s m) ∧
    Eq.{u_1 + 1} (α := Filter α) (⨅ (i : ℕ), 𝓟 (s i))
      (⨅ (i : ℕ), 𝓟 ((fun (n : ℕ) ↦ (⋂ (m : ℕ), ⋂ (_ : m ≤ n), s m : Set α)) i))
have h : Antitone.{0, u_1} (β := Set α) fun (n : ℕ) ↦ ⋂ (m : ℕ), ⋂ (_ : m ≤ n), s m
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α : Type u_1
s : ℕ → Set α
h : Antitone.{0, u_1} (β := Set α) fun (n : ℕ) ↦ ⋂ (m : ℕ), ⋂ (_ : m ≤ n), s m
⊢ (Antitone.{0, u_1} (β := Set α) fun (n : ℕ) ↦ ⋂ (m : ℕ), ⋂ (_ : m ≤ n), s m) ∧
    Eq.{u_1 + 1} (α := Filter α) (⨅ (i : ℕ), 𝓟 (s i))
      (⨅ (i : ℕ), 𝓟 ((fun (n : ℕ) ↦ (⋂ (m : ℕ), ⋂ (_ : m ≤ n), s m : Set α)) i))
have h₁ : Eq.{u_1 + 1} (α := Filter α) (⨅ (i : ℕ), 𝓟 (s i)) (⨅ (i : ℕ), 𝓟 (⋂ (m : ℕ), ⋂ (_ : m ≤ i), s m))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α : Type u_1
s : ℕ → Set α
⊢ Eq.{u_1 + 1} (α := Filter α) (⨅ (i : ℕ), 𝓟 (s i)) (⨅ (i : ℕ), 𝓟 (⋂ (m : ℕ), ⋂ (_ : m ≤ i), s m))
have h : LE.le.{u_1} (α := Filter α) (⨅ (i : ℕ), 𝓟 (s i)) (⨅ (i : ℕ), 𝓟 (⋂ (m : ℕ), ⋂ (_ : m ≤ i), s m))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α : Type u_1
s : ℕ → Set α
h : LE.le.{u_1} (α := Filter α) (⨅ (i : ℕ), 𝓟 (s i)) (⨅ (i : ℕ), 𝓟 (⋂ (m : ℕ), ⋂ (_ : m ≤ i), s m))
⊢ Eq.{u_1 + 1} (α := Filter α) (⨅ (i : ℕ), 𝓟 (s i)) (⨅ (i : ℕ), 𝓟 (⋂ (m : ℕ), ⋂ (_ : m ≤ i), s m))
have h₁ : LE.le.{u_1} (α := Filter α) (⨅ (i : ℕ), 𝓟 (⋂ (m : ℕ), ⋂ (_ : m ≤ i), s m)) (⨅ (i : ℕ), 𝓟 (s i))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α : Type u_1
s : ℕ → Set α
⊢ LE.le.{u_1} (α := Filter α) (⨅ (i : ℕ), 𝓟 (s i)) (⨅ (i : ℕ), 𝓟 (⋂ (m : ℕ), ⋂ (_ : m ≤ i), s m))
have h : ∀ (i : ℕ), LE.le.{u_1} (α := Filter α) (⨅ (i : ℕ), 𝓟 (s i)) (𝓟 (⋂ (m : ℕ), ⋂ (_ : m ≤ i), s m))
Tactic: rw [le_iInf_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α : Type u_1
s : ℕ → Set α
⊢ LE.le.{u_1} (α := Filter α) (⨅ (i : ℕ), 𝓟 (⋂ (m : ℕ), ⋂ (_ : m ≤ i), s m)) (⨅ (i : ℕ), 𝓟 (s i))
have h : ∀ (i : ℕ), ⨅ (i : ℕ), 𝓟 (⋂ (m : ℕ), ⋂ (_ : m ≤ i), s m) ≤ 𝓟 (s i)
Tactic: rw [le_iInf_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α : Type u_1
s : ℕ → Set α
i : ℕ
⊢ LE.le.{u_1} (α := Filter α) (⨅ (i : ℕ), 𝓟 (s i)) (𝓟 (⋂ (m : ℕ), ⋂ (_ : m ≤ i), s m))
have h : Membership.mem (γ := Filter α) (⨅ (i : ℕ), 𝓟 (s i)) (⋂ (m : ℕ), ⋂ (_ : m ≤ i), s m)
Tactic: rw [le_principal_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α : Type u_1
s : ℕ → Set α
i : ℕ
⊢ Membership.mem (γ := Filter α) (⨅ (i : ℕ), 𝓟 (s i)) (⋂ (m : ℕ), ⋂ (_ : m ≤ i), s m)
have h : ∀ (j : ℕ), Membership.mem (γ := Set ℕ) {i_1 : ℕ | i_1 ≤ i} j → Membership.mem (γ := Filter α) (⨅ (i : ℕ), 𝓟 (s i)) (s j)
Tactic: refine (biInter_mem (finite_le_nat _)).2 fun j _ => ?_
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α : Type u_1
s : ℕ → Set α
i : ℕ
⊢ ⨅ (i : ℕ), 𝓟 (⋂ (m : ℕ), ⋂ (_ : m ≤ i), s m) ≤ 𝓟 (s i)
have h : i ≤ i
Tactic: refine iInf_le_of_le i (principal_mono.2 <| iInter₂_subset i ?_)
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α : Type u_1
ι : Type u_4
inst : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
⊢ ∃ (x : ℕ → ι), Eq.{u_1 + 1} (α := α) (⨅ t ∈ B, f t) (⨅ (i : ℕ), f (x i))
have inl : ∀ (hB : B = ∅), ∃ (x : ℕ → ι), Eq.{u_1 + 1} (α := α) (⨅ t ∈ B, f t) (⨅ (i : ℕ), f (x i))
Tactic: rcases B.eq_empty_or_nonempty with hB | Bnonempty
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α : Type u_1
ι : Type u_4
inst : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
inl : ∀ (hB : B = ∅), ∃ (x : ℕ → ι), Eq.{u_1 + 1} (α := α) (⨅ t ∈ B, f t) (⨅ (i : ℕ), f (x i))
⊢ ∃ (x : ℕ → ι), Eq.{u_1 + 1} (α := α) (⨅ t ∈ B, f t) (⨅ (i : ℕ), f (x i))
have inr : ∀ (Bnonempty : B.Nonempty), ∃ (x : ℕ → ι), Eq.{u_1 + 1} (α := α) (⨅ t ∈ B, f t) (⨅ (i : ℕ), f (x i))
Tactic: rcases B.eq_empty_or_nonempty with hB | Bnonempty
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α : Type u_1
ι : Type u_4
inst : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
hB : B = ∅
⊢ ∃ (x : ℕ → ι), Eq.{u_1 + 1} (α := α) (⨅ t ∈ B, f t) (⨅ (i : ℕ), f (x i))
have inl : ∃ (x : ℕ → ι), Eq.{u_1 + 1} (α := α) ⊤ (⨅ (i : ℕ), f (x i))
Tactic: rw [hB, iInf_emptyset]
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α : Type u_1
ι : Type u_4
inst : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
hB : B = ∅
⊢ ∃ (x : ℕ → ι), Eq.{u_1 + 1} (α := α) ⊤ (⨅ (i : ℕ), f (x i))
have h₁ : Eq.{u_1 + 1} (α := α) ⊤ (⨅ (i : ℕ), f ((fun (x : ℕ) ↦ i₀) i))
Tactic: use fun _ => i₀
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α : Type u_1
ι' : Sort u_5
f : Filter α
h : f.IsCountablyGenerated
p : ι' → Prop
s : ι' → Set α
hs : f.HasBasis p s
⊢ ∃ (x : ℕ → Set α), f = ⨅ (i : ℕ), 𝓟 (x i)
have rcases : ∀ (s_1 : Set (Set α)) (hsc : s_1.Countable) (hs : (generate s_1).HasBasis p s),
  ∃ (x : ℕ → Set α), generate s_1 = ⨅ (i : ℕ), 𝓟 (x i)
Tactic: rcases h with ⟨s, hsc, rfl⟩
Cleared hypotheses: f, h, hs
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α : Type u_1
ι' : Sort u_5
p : ι' → Prop
s_1 : ι' → Set α
s : Set (Set α)
hsc : s.Countable
hs : (generate s).HasBasis p s_1
⊢ ∃ (x : ℕ → Set α), generate s = ⨅ (i : ℕ), 𝓟 (x i)
have rw : ∃ (x : ℕ → Set α), Eq.{u_1 + 1} (α := Filter α) (⨅ s_2 ∈ s, 𝓟 s_2) (⨅ (i : ℕ), 𝓟 (x i))
Tactic: rw [generate_eq_biInf]
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α : Type u_1
ι' : Sort u_5
f : Filter α
h : f.IsCountablyGenerated
p : ι' → Prop
s : ι' → Set α
hs : f.HasBasis p s
⊢ ∃ (x : ℕ → ι'), (∀ (i : ℕ), p (x i)) ∧ f.HasAntitoneBasis fun (i : ℕ) ↦ s (x i)
have obtain : ∀ (x' : ℕ → Set α) (hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)),
  ∃ (x : ℕ → ι'), (∀ (i : ℕ), p (x i)) ∧ f.HasAntitoneBasis fun (i : ℕ) ↦ s (x i)
Tactic: obtain ⟨x', hx'⟩ : ∃ x : ℕ → Set α, f = ⨅ i, 𝓟 (x i) := by
    rcases h with ⟨s, hsc, rfl⟩
    rw [generate_eq_biInf]
    exact countable_biInf_principal_eq_seq_iInf hsc
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (hypothesis)
Goal:
α : Type u_1
ι' : Sort u_5
f : Filter α
h : f.IsCountablyGenerated
p : ι' → Prop
s : ι' → Set α
hs : f.HasBasis p s
x' : ℕ → Set α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
⊢ ∃ (x : ℕ → ι'), (∀ (i : ℕ), p (x i)) ∧ f.HasAntitoneBasis fun (i : ℕ) ↦ s (x i)
have this : ∀ (i : ℕ), x' i ∈ f
Tactic: have : ∀ i, x' i ∈ f := fun i => hx'.symm ▸ (iInf_le (fun i => 𝓟 (x' i)) i) (mem_principal_self _)