awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
f : Filter α
β : Sort v
s : β → Set α
inst : Subsingleton β
rw : ⋂₀ range s ∈ f ↔ ∀ (i : β), s i ∈ f
rw₁ : ⋂ i ∈ range s, i ∈ f ↔ ∀ (i : β), s i ∈ f
⊢ ⋂ (i : β), s i ∈ f ↔ ∀ (i : β), s i ∈ f
have rw₂ : (∀ i ∈ range s, i ∈ f) ↔ ∀ (i : β), s i ∈ f
Tactic: rw [← sInter_range, sInter_eq_biInter, biInter_mem' (subsingleton_range s), forall_mem_range]
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
f : Filter α
β : Sort v
s : β → Set α
inst : Subsingleton β
rw : ⋂₀ range s ∈ f ↔ ∀ (i : β), s i ∈ f
rw₁ : ⋂ i ∈ range s, i ∈ f ↔ ∀ (i : β), s i ∈ f
rw₂ : (∀ i ∈ range s, i ∈ f) ↔ ∀ (i : β), s i ∈ f
⊢ ⋂ (i : β), s i ∈ f ↔ ∀ (i : β), s i ∈ f
have rw₃ : (∀ (i : β), s i ∈ f) ↔ ∀ (i : β), s i ∈ f
Tactic: rw [← sInter_range, sInter_eq_biInter, biInter_mem' (subsingleton_range s), forall_mem_range]
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
f : Filter α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
⊢ ((∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u) ↔ ∃ u ∈ f, P u ∧ Q u
have mp : ((∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u) → ∃ u ∈ f, P u ∧ Q u
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
f : Filter α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
mp : ((∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u) → ∃ u ∈ f, P u ∧ Q u
⊢ ((∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u) ↔ ∃ u ∈ f, P u ∧ Q u
have mpr : (∃ u ∈ f, P u ∧ Q u) → (∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
f g : Filter α
⊢ ¬f ≤ g ↔ ∃ s ∈ g, s ∉ f
have simp_rw : (¬∀ x ∈ g, x ∈ f) ↔ ∃ s ∈ g, s ∉ f
Tactic: simp_rw [le_def, not_forall, exists_prop]
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
f g : Filter α
simp_rw : (¬∀ x ∈ g, x ∈ f) ↔ ∃ s ∈ g, s ∉ f
⊢ ¬f ≤ g ↔ ∃ s ∈ g, s ∉ f
have simp_rw₁ : (∃ (x : Set α) (_ : x ∈ g), x ∉ f) ↔ ∃ s ∈ g, s ∉ f
Tactic: simp_rw [le_def, not_forall, exists_prop]
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
f : Filter α
⊢ ¬Disjoint f f ↔ f.NeBot
have rw : ¬f = ⊥ ↔ f.NeBot
Tactic: rw [disjoint_self, neBot_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
f : Filter α
rw : ¬f = ⊥ ↔ f.NeBot
⊢ ¬Disjoint f f ↔ f.NeBot
have rw₁ : ¬f = ⊥ ↔ f ≠ ⊥
Tactic: rw [disjoint_self, neBot_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
hs : s ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
⊢ p s
have have : ∀ (p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s), p s
Tactic: have p_of_f : ∀ i, ∀ s ∈ f i, p s := fun i s hs ↦ by simpa using ins hs uni
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (hypothesis)
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
hs : s ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun (t : Set α) ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
⊢ p s
have q_mono : Monotone q
Tactic: have q_mono : Monotone q := fun a b hab ha ↦
    ⟨mem_of_superset ha.1 hab, fun t hbt ↦ ha.2 _ (hab.trans hbt)⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s_1 : Set α
hs_1 : s_1 ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun (t : Set α) ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
i : ι
s : Set α
hs : s ∈ f i
t : Set α
ht : q t
⊢ q (s ∩ t)
have right : ∀ (t' : Set α), s ∩ t ⊆ t' → p t'
Tactic: use inter_mem (mem_iInf_of_mem _ hs) ht.1
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s_1 : Set α
hs_1 : s_1 ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun (t : Set α) ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
i : ι
s : Set α
hs : s ∈ f i
t : Set α
ht : q t
u : Set α
hu : s ∩ t ⊆ u
⊢ u = (u ∪ s) ∩ (u ∪ t)
have rwa : ∀ (hu : u ∪ s ∩ t = u), u = (u ∪ s) ∩ (u ∪ t)
Tactic: rwa [← union_eq_left, union_inter_distrib_left, eq_comm] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s_1 : Set α
hs_1 : s_1 ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun (t : Set α) ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
i : ι
s : Set α
hs : s ∈ f i
t : Set α
ht : q t
u : Set α
hu : s ∩ t ⊆ u
rwa : ∀ (hu : u ∪ s ∩ t = u), u = (u ∪ s) ∩ (u ∪ t)
⊢ u = (u ∪ s) ∩ (u ∪ t)
have rwa₁ : ∀ (hu : (u ∪ s) ∩ (u ∪ t) = u), u = (u ∪ s) ∩ (u ∪ t)
Tactic: rwa [← union_eq_left, union_inter_distrib_left, eq_comm] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s_1 : Set α
hs_1 : s_1 ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun (t : Set α) ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
i : ι
s : Set α
hs : s ∈ f i
t : Set α
ht : q t
u : Set α
hu : s ∩ t ⊆ u
rwa : ∀ (hu : u ∪ s ∩ t = u), u = (u ∪ s) ∩ (u ∪ t)
rwa₁ : ∀ (hu : (u ∪ s) ∩ (u ∪ t) = u), u = (u ∪ s) ∩ (u ∪ t)
⊢ u = (u ∪ s) ∩ (u ∪ t)
have rwa₂ : ∀ (hu : u = (u ∪ s) ∩ (u ∪ t)), u = (u ∪ s) ∩ (u ∪ t)
Tactic: rwa [← union_eq_left, union_inter_distrib_left, eq_comm] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s_1 : Set α
hs_1 : s_1 ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun (t : Set α) ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
i : ι
s : Set α
hs : s ∈ f i
t : Set α
ht : q t
u : Set α
hu : s ∩ t ⊆ u
⊢ p u
have right : ∀ (this : u = (u ∪ s) ∩ (u ∪ t)), p u
Tactic: have : u = (u ∪ s) ∩ (u ∪ t) := by
      rwa [← union_eq_left, union_inter_distrib_left, eq_comm] at hu
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s_1 : Set α
hs_1 : s_1 ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun (t : Set α) ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
i : ι
s : Set α
hs : s ∈ f i
t : Set α
ht : q t
u : Set α
hu : s ∩ t ⊆ u
this : u = (u ∪ s) ∩ (u ∪ t)
⊢ p u
have right : p ((u ∪ s) ∩ (u ∪ t))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (hypothesis)
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
hs : s ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun (t : Set α) ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
⊢ p s
have A : ∀ (i : ι), ∀ s ∈ f i, ∀ (t : Set α), q t → q (s ∩ t)
Tactic: have A : ∀ i, ∀ s ∈ f i, ∀ t, q t → q (s ∩ t) := fun i s hs t ht ↦ by
    use inter_mem (mem_iInf_of_mem _ hs) ht.1
    intro u hu
    have : u = (u ∪ s) ∩ (u ∪ t) := by
      rwa [← union_eq_left, union_inter_distrib_left, eq_comm] at hu
    rw [this]
    exact ins (mem_of_superset hs subset_union_right) (ht.2 _ subset_union_right)
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (hypothesis)
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
hs : s ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun (t : Set α) ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
A : ∀ (i : ι), ∀ s ∈ f i, ∀ (t : Set α), q t → q (s ∩ t)
⊢ p s
have B : ∀ (s t : Set α), q s → q t → q (s ∩ t)
Tactic: have B : ∀ s t, q s → q t → q (s ∩ t) := fun s t hqs hqt ↦ by
    let 𝓕 : Filter α :=
    { sets := {s | ∀ t, q t → q (s ∩ t)}
      univ_sets := by simp
      sets_of_superset ha hab t ht := q_mono (inter_subset_inter_left _ hab) (ha t ht)
      inter_sets ha hb t ht := by simpa [inter_assoc] using ha _ (hb _ ht) }
    exact (le_iInf_iff.mpr A : 𝓕 ≤ iInf f) hqs.1 _ hqt
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (hypothesis)
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
hs : s ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun (t : Set α) ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
A : ∀ (i : ι), ∀ s ∈ f i, ∀ (t : Set α), q t → q (s ∩ t)
B : ∀ (s t : Set α), q s → q t → q (s ∩ t)
⊢ p s
have C : ∀ (i : ι), ∀ s ∈ f i, q s
Tactic: have C : ∀ i, ∀ s ∈ f i, q s := fun i s hs ↦
    ⟨mem_iInf_of_mem _ hs, fun t hst ↦ p_of_f _ _ (mem_of_superset hs hst)⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (hypothesis)
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
hs : s ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun (t : Set α) ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
A : ∀ (i : ι), ∀ s ∈ f i, ∀ (t : Set α), q t → q (s ∩ t)
B : ∀ (s t : Set α), q s → q t → q (s ∩ t)
C : ∀ (i : ι), ∀ s ∈ f i, q s
𝓖 : Filter α := { sets := {t : Set α | q t}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
⊢ p s
have this : 𝓖 ≤ iInf f
Tactic: have : 𝓖 ≤ iInf f := le_iInf_iff.mpr C
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
s t : Set α
⊢ 𝓟 s = 𝓟 t ↔ s = t
have simp : s ⊆ t ∧ t ⊆ s ↔ s ≤ t ∧ t ≤ s
Tactic: simp only [le_antisymm_iff, le_principal_iff, mem_principal]
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
inst : Subsingleton α
l : Filter α
inst_1 : l.NeBot
⊢ l = ⊤
have refine : ∀ (s : Set α) (hs : s ∈ l), Membership.mem (γ := Filter α) ⊤ s
Tactic: refine top_unique fun s hs => ?_
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
inst : Subsingleton α
l : Filter α
inst_1 : l.NeBot
s : Set α
hs : s ∈ l
⊢ Membership.mem (γ := Filter α) ⊤ s
have obtain : ∀ (hs : univ ∈ l), Membership.mem (γ := Filter α) ⊤ univ
Tactic: obtain rfl : s = univ := Subsingleton.eq_univ_of_nonempty (nonempty_of_mem hs)
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
ι : Sort x
f g : Filter α
s_1 t : Set α
inst : Nonempty α
s : Set α
hs : Membership.mem (γ := Filter α) ⊤ s
⊢ s.Nonempty
have rwa : Set.Nonempty.{u} (α := α) univ
Tactic: rwa [mem_top.1 hs, ← nonempty_iff_univ_nonempty]
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
p : ι → Prop
l : Filter α
h : ∀ {s : Set α}, s ∈ l ↔ ∃ (i : ι), p i ∧ s ∈ f i
⊢ l = ⨅ (i : ι), ⨅ (_ : p i), f i
have rw : l = ⨅ (x : Subtype p), f (↑x : ι)
Tactic: rw [iInf_subtype']
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) f
ne : Nonempty ι
i : ι
⊢ ∀ {x y : Set α},
    Membership.mem (γ := Set (Set α)) (⋃ (i : ι), (f i).sets) x →
      x ⊆ y → Membership.mem (γ := Set (Set α)) (⋃ (i : ι), (f i).sets) y
have simp : ∀ {x y : Set α} (x_1 : ι), x ∈ (f x_1).sets → x ⊆ y → ∃ (i : ι), y ∈ (f i).sets
Tactic: simp only [mem_iUnion, exists_imp]
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) f
ne : Nonempty ι
i : ι
⊢ ∀ {x y : Set α},
    Membership.mem (γ := Set (Set α)) (⋃ (i : ι), (f i).sets) x →
      Membership.mem (γ := Set (Set α)) (⋃ (i : ι), (f i).sets) y →
        Membership.mem (γ := Set (Set α)) (⋃ (i : ι), (f i).sets) (x ∩ y)
have simp : ∀ {x y : Set α} (x_1 : ι), x ∈ (f x_1).sets → ∀ (x_2 : ι), y ∈ (f x_2).sets → ∃ (i : ι), x ∩ y ∈ (f i).sets
Tactic: simp only [mem_iUnion, exists_imp]
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) f
ne : Nonempty ι
i : ι
x y : Set α
a : ι
hx : x ∈ (f a).sets
b : ι
hy : y ∈ (f b).sets
⊢ ∃ (i : ι), x ∩ y ∈ (f i).sets
have rcases : ∀ (c : ι) (ha : f a ≥ f c) (hb : f b ≥ f c), ∃ (i : ι), x ∩ y ∈ (f i).sets
Tactic: rcases h a b with ⟨c, ha, hb⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (hypothesis)
Goal:
α : Type u
β : Type v
f : β → Filter α
s : Set β
h : DirectedOn (f ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) s
ne : s.Nonempty
t : Set α
⊢ Membership.mem (γ := Filter α) (⨅ i ∈ s, f i) t ↔ ∃ i ∈ s, t ∈ f i
have this : Nonempty.{v + 1} (↑s : Type v)
Tactic: haveI := ne.to_subtype
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
β : Type v
f : β → Filter α
s : Set β
h : DirectedOn (f ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) s
ne : s.Nonempty
t : Set α
this : Nonempty.{v + 1} (↑s : Type v)
⊢ Membership.mem (γ := Filter α) (⨅ i ∈ s, f i) t ↔ ∃ i ∈ s, t ∈ f i
have simp_rw : Membership.mem (γ := Filter α) (⨅ (x : Subtype (Membership.mem s)), f (↑x : β)) t ↔ ∃ i ∈ s, t ∈ f i
Tactic: simp_rw [iInf_subtype', mem_iInf_of_directed h.directed_val, Subtype.exists, exists_prop]
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
β : Type v
f : β → Filter α
s : Set β
h : DirectedOn (f ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) s
ne : s.Nonempty
t : Set α
this : Nonempty.{v + 1} (↑s : Type v)
simp_rw : Membership.mem (γ := Filter α) (⨅ (x : Subtype (Membership.mem s)), f (↑x : β)) t ↔ ∃ i ∈ s, t ∈ f i
⊢ Membership.mem (γ := Filter α) (⨅ i ∈ s, f i) t ↔ ∃ i ∈ s, t ∈ f i
have simp_rw₁ : (∃ (i : { x : β // x ∈ s }), t ∈ f (↑i : β)) ↔ ∃ i ∈ s, t ∈ f i
Tactic: simp_rw [iInf_subtype', mem_iInf_of_directed h.directed_val, Subtype.exists, exists_prop]
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
β : Type v
f : β → Filter α
s : Set β
h : DirectedOn (f ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) s
ne : s.Nonempty
t : Set α
this : Nonempty.{v + 1} (↑s : Type v)
simp_rw : Membership.mem (γ := Filter α) (⨅ (x : Subtype (Membership.mem s)), f (↑x : β)) t ↔ ∃ i ∈ s, t ∈ f i
simp_rw₁ : (∃ (i : { x : β // x ∈ s }), t ∈ f (↑i : β)) ↔ ∃ i ∈ s, t ∈ f i
⊢ Membership.mem (γ := Filter α) (⨅ i ∈ s, f i) t ↔ ∃ i ∈ s, t ∈ f i
have simp_rw₂ : (∃ (a : β) (_ : a ∈ s), t ∈ f a) ↔ ∃ i ∈ s, t ∈ f i
Tactic: simp_rw [iInf_subtype', mem_iInf_of_directed h.directed_val, Subtype.exists, exists_prop]
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
ι : Sort x
f_1 g : Filter α
s t : Set α
f : Filter α
⊢ ⊤ \ f = ￢f
have h : ∀ (s : Set α), s ∈ ⊤ \ f ↔ s ∈ ￢f
Tactic: ext s
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
ι : Sort x
f_1 g : Filter α
s_1 t : Set α
f : Filter α
s : Set α
⊢ s ∈ ⊤ \ f ↔ s ∈ ￢f
have h : (∀ t ∈ f, ∀ (x : α), x ∈ s ∨ x ∈ t) ↔ ∀ (x : α), (∀ t ∈ f, x ∈ t) ∨ x ∈ s
Tactic: simp only [mem_sdiff_iff_union, Filter.hnot_def, mem_principal, compl_subset_iff_union,
      mem_top_iff_forall, eq_univ_iff_forall, ker, mem_union, mem_sInter, Filter.mem_sets]
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) f
hb : ∀ (i : ι), (f i).NeBot
⊢ (iInf f).NeBot
have inl : IsEmpty ι → (iInf f).NeBot
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) f
hb : ∀ (i : ι), (f i).NeBot
inl : IsEmpty ι → (iInf f).NeBot
⊢ (iInf f).NeBot
have inr : Nonempty ι → (iInf f).NeBot
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) f
hb : ∀ (i : ι), (f i).NeBot
h : IsEmpty ι
⊢ (iInf f).NeBot
have inl : iInf f ≠ ⊥
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
s t : Set α
⊢ 𝓟 s ⊓ 𝓟 t ≤ 𝓟 (s ∩ t)
have simp : ∃ t₁ ∈ 𝓟 s, ∃ t₂ ∈ 𝓟 t, s ∩ t = t₁ ∩ t₂
Tactic: simp only [le_principal_iff, mem_inf_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
s : Set α
⊢ 𝓟 s ⊓ 𝓟 sᶜ = ⊥
have rw : 𝓟 (s ∩ sᶜ) = ⊥
Tactic: rw [inf_principal, inter_compl_self, principal_empty]
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
s : Set α
rw : 𝓟 (s ∩ sᶜ) = ⊥
⊢ 𝓟 s ⊓ 𝓟 sᶜ = ⊥
have rw₁ : Eq.{u + 1} (α := Filter α) (𝓟 ∅) ⊥
Tactic: rw [inf_principal, inter_compl_self, principal_empty]
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
s : Set α
rw : 𝓟 (s ∩ sᶜ) = ⊥
rw₁ : Eq.{u + 1} (α := Filter α) (𝓟 ∅) ⊥
⊢ 𝓟 s ⊓ 𝓟 sᶜ = ⊥
have rw₂ : Eq.{u + 1} (α := Filter α) ⊥ ⊥
Tactic: rw [inf_principal, inter_compl_self, principal_empty]
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
s : Set α
⊢ 𝓟 s ⊔ 𝓟 sᶜ = ⊤
have rw : 𝓟 (s ∪ sᶜ) = ⊤
Tactic: rw [sup_principal, union_compl_self, principal_univ]
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
s : Set α
rw : 𝓟 (s ∪ sᶜ) = ⊤
⊢ 𝓟 s ⊔ 𝓟 sᶜ = ⊤
have rw₁ : Eq.{u + 1} (α := Filter α) (𝓟 univ) ⊤
Tactic: rw [sup_principal, union_compl_self, principal_univ]
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
s : Set α
rw : 𝓟 (s ∪ sᶜ) = ⊤
rw₁ : Eq.{u + 1} (α := Filter α) (𝓟 univ) ⊤
⊢ 𝓟 s ⊔ 𝓟 sᶜ = ⊤
have rw₂ : Eq.{u + 1} (α := Filter α) ⊤ ⊤
Tactic: rw [sup_principal, union_compl_self, principal_univ]
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
⊢ ⨆ (i : ι), f i ⊓ 𝓟 s = (⨆ (i : ι), f i) ⊓ 𝓟 s
have h : ∀ (s_1 : Set α), Membership.mem (γ := Filter α) (⨆ (i : ι), f i ⊓ 𝓟 s) s_1 ↔ s_1 ∈ (⨆ (i : ι), f i) ⊓ 𝓟 s
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
f : Filter α
s : Set α
⊢ f ⊓ 𝓟 s = ⊥ ↔ sᶜ ∈ f
have rw : {x : α | x ∈ s → Membership.mem (γ := Set α) ∅ x} ∈ f ↔ sᶜ ∈ f
Tactic: rw [← empty_mem_iff_bot, mem_inf_principal]
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
f : Filter α
s : Set α
h : f ⊓ 𝓟 sᶜ = ⊥
⊢ s ∈ f
have rwa : ∀ (h : sᶜᶜ ∈ f), s ∈ f
Tactic: rwa [inf_principal_eq_bot, compl_compl] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
f : Filter α
s : Set α
h : f ⊓ 𝓟 sᶜ = ⊥
rwa : ∀ (h : sᶜᶜ ∈ f), s ∈ f
⊢ s ∈ f
have rwa₁ : ∀ (h : s ∈ f), s ∈ f
Tactic: rwa [inf_principal_eq_bot, compl_compl] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
f : Filter α
t : f.NeBot
p : Prop
⊢ (∀ᶠ (x : α) in f, p) ↔ p
have pos : ∀ (h : p), (∀ᶠ (x : α) in f, p) ↔ p
Tactic: by_cases h : p
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
f : Filter α
t : f.NeBot
p : Prop
pos : ∀ (h : p), (∀ᶠ (x : α) in f, p) ↔ p
⊢ (∀ᶠ (x : α) in f, p) ↔ p
have neg : ∀ (h : ¬p), (∀ᶠ (x : α) in f, p) ↔ p
Tactic: by_cases h : p
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
f : Filter α
p : α → Prop
h : ∀ᶠ (x : α) in f, p x
x : Set α
⊢ ∀ᶠ (x_1 : α) in f, x_1 ∈ x → p x_1
have h₁ : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x_1 : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ p x) x} x_1 →
        Membership.mem (γ := Set α) {x_2 : α | (fun (x_3 : α) ↦ x_3 ∈ x → p x_3) x_2} x_1}
    a
Tactic: filter_upwards [h] with _ pa _ using pa
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
f : Filter α
p : α → Prop
h : ∀ᶠ (x : α) in f, p x
x : Set α
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x_1 : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ p x) x} x_1 →
          Membership.mem (γ := Set α) {x_2 : α | (fun (x_3 : α) ↦ x_3 ∈ x → p x_3) x_2} x_1}
      a
⊢ ∀ᶠ (x_1 : α) in f, x_1 ∈ x → p x_1
have h₂ : ∀ (a : α), p a → a ∈ x → p a
Tactic: filter_upwards [h] with _ pa _ using pa
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
f : Filter α
p : α → Prop
h : ∀ (s : Set α), ∀ᶠ (x : α) in f, x ∈ s → p x
⊢ ∀ᶠ (x : α) in f, p x
have h₁ : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Membership.mem (γ := Set α) univ x → p x) x} x →
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ p x) x} x}
    a
Tactic: filter_upwards [h univ] with _ pa using pa (by simp)
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
f : Filter α
p : α → Prop
h : ∀ (s : Set α), ∀ᶠ (x : α) in f, x ∈ s → p x
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Membership.mem (γ := Set α) univ x → p x) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ p x) x} x}
      a
⊢ ∀ᶠ (x : α) in f, p x
have h₂ : ∀ (a : α), (Membership.mem (γ := Set α) univ a → p a) → p a
Tactic: filter_upwards [h univ] with _ pa using pa (by simp)
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
p q : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
hq : ∀ᶠ (x : α) in f, q x
⊢ ∃ᶠ (x : α) in f, p x ∧ q x
have refine : ∀ (h : ∀ᶠ (x : α) in f, ¬(fun (x : α) ↦ p x ∧ q x) x) (x : α),
  ¬(fun (x : α) ↦ p x ∧ q x) x → q x → ¬(fun (x : α) ↦ p x) x
Tactic: refine mt (fun h => hq.mp <| h.mono ?_) hp
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
p : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
⊢ ∃ (x : α), p x
have by_contra : ∀ (H : ¬∃ (x : α), p x), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (hypothesis)
Goal:
α : Type u
p : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
H : ¬∃ (x : α), p x
⊢ False
have H₁ : ∀ᶠ (x : α) in f, ¬p x
Tactic: replace H : ∀ᶠ x in f, ¬p x := Eventually.of_forall (not_exists.1 H)
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
l : Filter α
p : α → Prop
⊢ (∃ᶠ (x : α) in l, p x) ↔ (l ⊓ 𝓟 {x : α | p x}).NeBot
have rw : (∃ᶠ (x : α) in l, p x) ↔ {x : α | p x}ᶜ ∉ l
Tactic: rw [neBot_iff, Ne, inf_principal_eq_bot]
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
f : Filter α
inst : f.NeBot
p : Prop
⊢ (∃ᶠ (x : α) in f, p) ↔ p
have pos : p → ((∃ᶠ (x : α) in f, p) ↔ p)
Tactic: by_cases p
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
f : Filter α
inst : f.NeBot
p : Prop
pos : p → ((∃ᶠ (x : α) in f, p) ↔ p)
⊢ (∃ᶠ (x : α) in f, p) ↔ p
have neg : ¬p → ((∃ᶠ (x : α) in f, p) ↔ p)
Tactic: by_cases p
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (hypothesis)
Goal:
α : Type u
β : Type v
r : α → β → Prop
l : Filter α
inst : l.NeBot
h : ∀ᶠ (x : α) in l, ∃ (y : β), r x y
⊢ ∃ (f : α → β), ∀ᶠ (x : α) in l, r x (f x)
have this : Nonempty β
Tactic: haveI : Nonempty β := let ⟨_, hx⟩ := h.exists; hx.nonempty
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
β : Type v
r : α → β → Prop
l : Filter α
inst : l.NeBot
h : ∀ᶠ (x : α) in l, ∃ (y : β), r x y
this : Nonempty β
⊢ ∃ (f : α → β), ∀ᶠ (x : α) in l, r x (f x)
have choose! : ∀ (f : (x : α) → β) (hf : ∀ (x : α) (hx : ∃ (y : β), r x y), r x (f x)), ∃ (f : α → β), ∀ᶠ (x : α) in l, r x (f x)
Tactic: choose! f hf using fun x (hx : ∃ y, r x y) => hx
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
ι : Type u_2
α : ι → Type u_3
inst : ∀ (i : ι), Nonempty.{u_3 + 1} (α i)
P : (i : ι) → α i → Prop
F : Filter ι
⊢ (∀ᶠ (i : ι) in F, ∃ (b : α i), P i b) ↔ ∃ (b : (i : ι) → α i), ∀ᶠ (i : ι) in F, P i (b i)
have refine : ∀ (H : ∀ᶠ (i : ι) in F, ∃ (b : α i), P i b), ∃ (b : (i : ι) → α i), ∀ᶠ (i : ι) in F, P i (b i)
Tactic: refine ⟨fun H ↦ ?_, fun ⟨b, hb⟩ ↦ hb.mp (.of_forall fun x a ↦ ⟨_, a⟩)⟩