awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ι
H : ∀ᶠ (i : ι) in F, ∃ (b : α i), P i b
⊢ ∃ (b : (i : ι) → α i), ∀ᶠ (i : ι) in F, P i (b i)
have refine : ∀ᶠ (i : ι) in F, P i ((fun (i : ι) ↦ (if h : ∃ (b : α i), P i b then h.choose (p := P i) else Nonempty.some sorry : α i)) i)
Tactic: refine ⟨fun i ↦ if h : ∃ b, P i b then h.choose else Nonempty.some inferInstance, ?_⟩
-- 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 ι
H : ∀ᶠ (i : ι) in F, ∃ (b : α i), P i b
⊢ ∀ᶠ (i : ι) in F,
    P i ((fun (i : ι) ↦ (if h : ∃ (b : α i), P i b then h.choose (p := P i) else Nonempty.some ⋯ : α i)) i)
have h : ∀ (i : ι) (hi : ∃ (b : α i), P i b), P i (if h : ∃ (b : α i), P i b then h.choose (p := P i) else Nonempty.some sorry)
Tactic: filter_upwards [H] with i hi
-- 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: classical
  refine ⟨fun H ↦ ?_, fun ⟨b, hb⟩ ↦ hb.mp (.of_forall fun x a ↦ ⟨_, a⟩)⟩
  refine ⟨fun i ↦ if h : ∃ b, P i b then h.choose else Nonempty.some inferInstance, ?_⟩
  filter_upwards [H] with i hi
  exact dif_pos hi ▸ hi.choose_spec
-- 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 ι
refine : ∀ (H : ∀ᶠ (i : ι) in F, ∃ (b : α i), P i b), ∃ (b : (i : ι) → α i), ∀ᶠ (i : ι) in F, P i (b i)
⊢ (∀ᶠ (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),
  ∀ᶠ (i : ι) in F,
    P i ((fun (i : ι) ↦ (if h : ∃ (b : α i), P i b then h.choose (p := P i) else Nonempty.some sorry : α i)) i)
Tactic: classical
  refine ⟨fun H ↦ ?_, fun ⟨b, hb⟩ ↦ hb.mp (.of_forall fun x a ↦ ⟨_, a⟩)⟩
  refine ⟨fun i ↦ if h : ∃ b, P i b then h.choose else Nonempty.some inferInstance, ?_⟩
  filter_upwards [H] with i hi
  exact dif_pos hi ▸ hi.choose_spec
-- 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 ι
refine : ∀ (H : ∀ᶠ (i : ι) in F, ∃ (b : α i), P i b), ∃ (b : (i : ι) → α i), ∀ᶠ (i : ι) in F, P i (b i)
refine₁ :
  ∀ (H : ∀ᶠ (i : ι) in F, ∃ (b : α i), P i b),
    ∀ᶠ (i : ι) in F,
      P i ((fun (i : ι) ↦ (if h : ∃ (b : α i), P i b then h.choose (p := P i) else Nonempty.some ⋯ : α i)) i)
⊢ (∀ᶠ (i : ι) in F, ∃ (b : α i), P i b) ↔ ∃ (b : (i : ι) → α i), ∀ᶠ (i : ι) in F, P i (b i)
have h : ∀ (H : ∀ᶠ (i : ι) in F, ∃ (b : α i), P i b) (i : ι) (hi : ∃ (b : α i), P i b),
  P i (if h : ∃ (b : α i), P i b then h.choose (p := P i) else Nonempty.some sorry)
Tactic: classical
  refine ⟨fun H ↦ ?_, fun ⟨b, hb⟩ ↦ hb.mp (.of_forall fun x a ↦ ⟨_, a⟩)⟩
  refine ⟨fun i ↦ if h : ∃ b, P i b then h.choose else Nonempty.some inferInstance, ?_⟩
  filter_upwards [H] with i hi
  exact dif_pos hi ▸ hi.choose_spec
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
s t : Set α
l : Filter α
⊢ s ∩ t =ᶠ[l] t ↔ ∀ᶠ (x : α) in l, x ∈ t → x ∈ s
have rw : t ∩ s =ᶠ[l] t ↔ ∀ᶠ (x : α) in l, x ∈ t → x ∈ s
Tactic: rw [inter_comm, inter_eventuallyEq_left]
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
s t : Set α
l : Filter α
rw : t ∩ s =ᶠ[l] t ↔ ∀ᶠ (x : α) in l, x ∈ t → x ∈ s
⊢ s ∩ t =ᶠ[l] t ↔ ∀ᶠ (x : α) in l, x ∈ t → x ∈ s
have rw₁ : (∀ᶠ (x : α) in l, x ∈ t → x ∈ s) ↔ ∀ᶠ (x : α) in l, x ∈ t → x ∈ s
Tactic: rw [inter_comm, inter_eventuallyEq_left]
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
β : Type v
inst : LE β
l : Filter α
f f' g g' : α → β
H_1 : f ≤ᶠ[l] g
hf_1 : f =ᶠ[l] f'
hg_1 : g =ᶠ[l] g'
x : α
hf : f x = f' x
hg : g x = g' x
H : f x ≤ g x
⊢ f' x ≤ g' x
have rwa : ∀ (H : f' x ≤ g x), f' x ≤ g' x
Tactic: rwa [hf, hg] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
β : Type v
inst : LE β
l : Filter α
f f' g g' : α → β
H_1 : f ≤ᶠ[l] g
hf_1 : f =ᶠ[l] f'
hg_1 : g =ᶠ[l] g'
x : α
hf : f x = f' x
hg : g x = g' x
H : f x ≤ g x
rwa : ∀ (H : f' x ≤ g x), f' x ≤ g' x
⊢ f' x ≤ g' x
have rwa₁ : ∀ (H : f' x ≤ g' x), f' x ≤ g' x
Tactic: rwa [hf, hg] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
β : Type v
inst : SemilatticeSup β
l : Filter α
f₁ f₂ g₁ g₂ : α → β
hf : f₁ ≤ᶠ[l] f₂
hg : g₁ ≤ᶠ[l] g₂
⊢ f₁ ⊔ g₁ ≤ᶠ[l] f₂ ⊔ g₂
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f₁ x ≤ f₂ x) x} x →
        Membership.mem (γ := Set α)
          {x : α |
            Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ g₁ x ≤ g₂ x) x} x →
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ (f₁ ⊔ g₁) x ≤ (f₂ ⊔ g₂) x) x} x}
          x}
    a
Tactic: filter_upwards [hf, hg] with x hfx hgx using sup_le_sup hfx hgx
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
β : Type v
inst : SemilatticeSup β
l : Filter α
f₁ f₂ g₁ g₂ : α → β
hf : f₁ ≤ᶠ[l] f₂
hg : g₁ ≤ᶠ[l] g₂
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f₁ x ≤ f₂ x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ g₁ x ≤ g₂ x) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ (f₁ ⊔ g₁) x ≤ (f₂ ⊔ g₂) x) x} x}
            x}
      a
⊢ f₁ ⊔ g₁ ≤ᶠ[l] f₂ ⊔ g₂
have h₁ : ∀ (a : α), f₁ a ≤ f₂ a → g₁ a ≤ g₂ a → (f₁ ⊔ g₁) a ≤ (f₂ ⊔ g₂) a
Tactic: filter_upwards [hf, hg] with x hfx hgx using sup_le_sup hfx hgx
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
β : Type v
inst : SemilatticeSup β
l : Filter α
f g h : α → β
hf : f ≤ᶠ[l] h
hg : g ≤ᶠ[l] h
⊢ f ⊔ g ≤ᶠ[l] h
have h₁ : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ h x) x} x →
        Membership.mem (γ := Set α)
          {x : α |
            Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ g x ≤ h x) x} x →
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ (f ⊔ g) x ≤ h x) x} x}
          x}
    a
Tactic: filter_upwards [hf, hg] with x hfx hgx using _root_.sup_le hfx hgx
-- Lean 4 proof step from Mathlib.Order.Filter.Basic (goal)
Goal:
α : Type u
β : Type v
inst : SemilatticeSup β
l : Filter α
f g h : α → β
hf : f ≤ᶠ[l] h
hg : g ≤ᶠ[l] h
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ h x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ g x ≤ h x) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ (f ⊔ g) x ≤ h x) x} x}
            x}
      a
⊢ f ⊔ g ≤ᶠ[l] h
have h₂ : ∀ (a : α), f a ≤ h a → g a ≤ h a → (f ⊔ g) a ≤ h a
Tactic: filter_upwards [hf, hg] with x hfx hgx using _root_.sup_le hfx hgx
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 l : Filter α
inst : CountableInterFilter l
S : Set (Set α)
hS : #(↑S : Type u) < (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1
a : ∀ s ∈ S, s ∈ l
⊢ ⋂₀ S ∈ l
have apply : S.Countable
Tactic: apply CountableInterFilter.countable_sInter_mem S _ a
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 l : Filter α
inst : CountableInterFilter l
S : Set (Set α)
hS : #(↑S : Type u) < (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1
a : ∀ s ∈ S, s ∈ l
⊢ S.Countable
have rwa : #(↑S : Type u) ≤ ℵ₀
Tactic: rwa [← le_aleph0_iff_set_countable, ← lt_aleph_one_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
α : Type u
l : Filter α
h : CardinalInterFilter l ((ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1)
⊢ CountableInterFilter l
have refine : ∀ (S : Set (Set α)) (h : S.Countable) (a : ∀ s ∈ S, s ∈ l), #(↑S : Type u) < (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1
Tactic: refine ⟨fun S h a ↦ CardinalInterFilter.cardinal_sInter_mem (c := ℵ₁) S ?_ a⟩
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
α : Type u
l : Filter α
h_1 : CardinalInterFilter l ((ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1)
S : Set (Set α)
h : S.Countable
a : ∀ s ∈ S, s ∈ l
⊢ #(↑S : Type u) < (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1
have rwa : #(↑S : Type u) ≤ ℵ₀
Tactic: rwa [lt_aleph_one_iff, le_aleph0_iff_set_countable]
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
s : ι → Set α
hic : #ι < c
⊢ ⋂ (i : ι), s i ∈ l ↔ ∀ (i : ι), s i ∈ l
have rw : ⋂₀ range s ∈ l ↔ ∀ (i : ι), s i ∈ l
Tactic: rw [← sInter_range _]
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
s : ι → Set α
hic : #ι < c
⊢ ⋂₀ range s ∈ l ↔ ∀ (i : ι), s i ∈ l
have apply : (∀ s_1 ∈ range s, s_1 ∈ l) ↔ ∀ (i : ι), s i ∈ l
Tactic: apply (cardinal_sInter_mem (lt_of_le_of_lt Cardinal.mk_range_le hic)).trans
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
S : Set ι
hS : #(↑S : Type u) < c
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)), 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.CardinalInter (goal)
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
p : α → ι → Prop
hic : #ι < c
⊢ (∀ᶠ (x : α) in l, ∀ (i : ι), p x i) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p x i
have simp : ⋂ (i : ι), {x : α | p x i} ∈ l ↔ ∀ (i : ι), {x : α | p x i} ∈ l
Tactic: simp only [Filter.Eventually, setOf_forall]
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
S : Set ι
hS : #(↑S : Type u) < c
p : α → (i : ι) → i ∈ S → Prop
⊢ (∀ᶠ (x : α) in l, ∀ (i : ι) (hi : i ∈ S), p x i hi) ↔ ∀ (i : ι) (hi : i ∈ S), ∀ᶠ (x : α) in l, p x i hi
have simp : ⋂ (i : ι), ⋂ (i_1 : i ∈ S), {x : α | p x i i_1} ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), {x : α | p x i hi} ∈ l
Tactic: simp only [Filter.Eventually, setOf_forall]
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
S : Set ι
hS : #(↑S : Type u) < c
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)), s (↑x : ι) sorry ≤ᶠ[l] ⋃ (x : (↑S : Type u)), t (↑x : ι) sorry
Tactic: simp only [biUnion_eq_iUnion]
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
S : Set ι
hS : #(↑S : Type u) < c
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)), s (↑x : ι) sorry ≤ᶠ[l] ⋂ (x : (↑S : Type u)), t (↑x : ι) sorry
Tactic: simp only [biInter_eq_iInter]
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Set (Set α)
hc : 2 < c
hl : ∀ (S : Set (Set α)), #(↑S : Type u) < c → S ⊆ l → ⋂₀ S ∈ l
h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l
s t : Set α
hs : s ∈ l
ht : t ∈ l
⊢ ⋂₀ {s, t} ∈ l
have apply : #(↑{s, t} : Type u) < c
Tactic: apply hl _ (?_) (insert_subset_iff.2 ⟨hs, singleton_subset_iff.2 ht⟩)
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Set (Set α)
hc : 2 < c
hl : ∀ (S : Set (Set α)), #(↑S : Type u) < c → S ⊆ l → ⋂₀ S ∈ l
h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l
s t : Set α
hs : s ∈ l
ht : t ∈ l
⊢ #(↑{s, t} : Type u) ≤ 2
have _ : #(↑{t} : Type u) + 1 = 2
Tactic: calc
      _ ≤ #({t} : Set (Set α)) + 1 := Cardinal.mk_insert_le
      _ = 2 := by norm_num
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (hypothesis)
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Set (Set α)
hc : 2 < c
hl : ∀ (S : Set (Set α)), #(↑S : Type u) < c → S ⊆ l → ⋂₀ S ∈ l
h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l
s t : Set α
hs : s ∈ l
ht : t ∈ l
⊢ #(↑{s, t} : Type u) < c
have this : #(↑{s, t} : Type u) ≤ 2
Tactic: have : #({s, t} : Set (Set α)) ≤ 2 := by
      calc
      _ ≤ #({t} : Set (Set α)) + 1 := Cardinal.mk_insert_le
      _ = 2 := by norm_num
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Set (Set α)
hc : 2 < c
hUnion : ∀ (S : Set (Set α)), #(↑S : Type u) < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
⊢ Filter α
have refine_1 : ∀ (S : Set (Set α)) (hSc : #(↑S : Type u) < c) (hSp : S ⊆ {s : Set α | sᶜ ∈ l}),
  Membership.mem (γ := Set (Set α)) {s : Set α | sᶜ ∈ l} (⋂₀ S)
Tactic: refine .ofCardinalInter {s | sᶜ ∈ l} hc (fun S hSc hSp ↦ ?_) fun s t ht hsub ↦ ?_
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Set (Set α)
hc : 2 < c
hUnion : ∀ (S : Set (Set α)), #(↑S : Type u) < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
refine_1 :
  ∀ (S : Set (Set α)) (hSc : #(↑S : Type u) < c) (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 .ofCardinalInter {s | sᶜ ∈ l} hc (fun S hSc hSp ↦ ?_) fun s t ht hsub ↦ ?_
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Set (Set α)
hc : 2 < c
hUnion : ∀ (S : Set (Set α)), #(↑S : Type u) < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : #(↑S : Type u) < c
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.CardinalInter (goal)
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Set (Set α)
hc : 2 < c
hUnion : ∀ (S : Set (Set α)), #(↑S : Type u) < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : #(↑S : Type u) < c
hSp : S ⊆ {s : Set α | sᶜ ∈ l}
⊢ ⋃₀ (compl '' S) ∈ l
have refine_1 : ∀ s ∈ compl '' S, s ∈ l
Tactic: apply hUnion (compl '' S) (lt_of_le_of_lt mk_image_le hSc)
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (hypothesis)
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Set (Set α)
hc : 2 < c
hUnion : ∀ (S : Set (Set α)), #(↑S : Type u) < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : #(↑S : Type u) < c
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.CardinalInter (goal)
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Set (Set α)
hc : 2 < c
hUnion : ∀ (S : Set (Set α)), #(↑S : Type u) < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : #(↑S : Type u) < c
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.CardinalInter (goal)
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Set (Set α)
hc : 2 < c
hUnion : ∀ (S : Set (Set α)), #(↑S : Type u) < c → (∀ 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.CardinalInter (hypothesis)
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Set (Set α)
hc : 2 < c
hUnion : ∀ (S : Set (Set α)), #(↑S : Type u) < c → (∀ 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.CardinalInter (goal)
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
⊢ CardinalInterFilter (α := α) ⊥ c
have rw : CardinalInterFilter (α := α) (𝓟 ∅) c
Tactic: rw [← principal_empty]
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
⊢ CardinalInterFilter (α := α) ⊤ c
have rw : CardinalInterFilter (α := α) (𝓟 Set.univ) c
Tactic: rw [← principal_univ]
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Filter β
inst_1 : CardinalInterFilter l c
f : α → β
⊢ CardinalInterFilter (comap f l) c
have refine : ∀ (S : Set (Set α)) (hSc : #(↑S : Type u) < c) (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.CardinalInter (goal)
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Filter β
inst_1 : CardinalInterFilter l c
f : α → β
S : Set (Set α)
hSc : #(↑S : Type u) < c
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.CardinalInter (goal)
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Filter β
inst_1 : CardinalInterFilter l c
f : α → β
S : Set (Set α)
hSc : #(↑S : Type u) < c
t : (s : Set α) → Set β
htl : ∀ s ∈ S, t s ∈ l
ht : ∀ s ∈ S, f ⁻¹' t s ⊆ s
⊢ ⋂₀ S ∈ comap f l
have refine : f ⁻¹' ⋂ i ∈ S, t i ⊆ ⋂₀ S
Tactic: refine ⟨_, (cardinal_bInter_mem hSc).2 htl, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Filter α
inst_1 : CardinalInterFilter l c
f : α → β
⊢ CardinalInterFilter (map f l) c
have refine : ∀ (S : Set (Set β)) (hSc : #(↑S : Type u) < c) (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.CardinalInter (goal)
Goal:
ι α β : Type u
c : Cardinal.{u}
l_1 : Filter α
inst : CardinalInterFilter l_1 c
l : Filter α
inst_1 : CardinalInterFilter l c
f : α → β
S : Set (Set β)
hSc : #(↑S : Type u) < c
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.CardinalInter (goal)
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
inst_1 : CardinalInterFilter l₁ c
inst_2 : CardinalInterFilter l₂ c
⊢ CardinalInterFilter (l₁ ⊓ l₂) c
have refine : ∀ (S : Set (Set α)) (hSc : #(↑S : Type u) < c) (hS : ∀ s ∈ S, s ∈ l₁ ⊓ l₂), ⋂₀ S ∈ l₁ ⊓ l₂
Tactic: refine ⟨fun S hSc hS => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
inst_1 : CardinalInterFilter l₁ c
inst_2 : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #(↑S : Type u) < c
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.CardinalInter (hypothesis)
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
inst_1 : CardinalInterFilter l₁ c
inst_2 : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #(↑S : Type u) < c
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₁ := (cardinal_bInter_mem hSc).2 hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (hypothesis)
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
inst_1 : CardinalInterFilter l₁ c
inst_2 : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #(↑S : Type u) < c
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₂ := (cardinal_bInter_mem hSc).2 ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
inst_1 : CardinalInterFilter l₁ c
inst_2 : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #(↑S : Type u) < c
s t : (s : Set α) → s ∈ S → Set α
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₁
ht : ⋂ (i : Set α), ⋂ (h : i ∈ S), t i h ∈ l₂
⊢ ⋂₀ S ∈ l₁ ⊓ l₂
have refine : ∀ (i : Set α) (hi : i ∈ S), (⋂ (i : Set α), ⋂ (h : i ∈ S), s i h) ∩ ⋂ (i : Set α), ⋂ (h : i ∈ S), t i h ⊆ i
Tactic: refine mem_of_superset (inter_mem_inf hs ht) (subset_sInter fun i hi => ?_)
-- Lean 4 proof step from Mathlib.Order.Filter.CardinalInter (goal)
Goal:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst : CardinalInterFilter l c
l₁ l₂ : Filter α
inst_1 : CardinalInterFilter l₁ c
inst_2 : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #(↑S : Type u) < c
s t : (s : Set α) → s ∈ S → Set α
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₁
ht : ⋂ (i : Set α), ⋂ (h : i ∈ S), t i h ∈ l₂
i : Set α
hi : i ∈ S
⊢ (⋂ (i : Set α), ⋂ (h : i ∈ S), s i h) ∩ ⋂ (i : Set α), ⋂ (h : i ∈ S), t i h ⊆ i
have rw : (⋂ (i : Set α), ⋂ (h : i ∈ S), s i h) ∩ ⋂ (i : Set α), ⋂ (h : i ∈ S), t i h ⊆ s i hi ∩ t i hi
Tactic: rw [hst i hi]