awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
this : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i : ι' // p i } :=
  fun (n : ℕ) ↦
    Nat.recOn.{max 1 u_5} (motive := fun (x : ℕ) ↦ { i : ι' // p i }) n (hs.index (p := p) (s := s) (x' 0) ⋯)
      fun (n : ℕ) (xn : { i : ι' // p i }) ↦ hs.index (p := p) (s := s) (x' (n + 1) ∩ s (↑xn : ι')) ⋯
⊢ ∃ (x : ℕ → ι'), (∀ (i : ℕ), p (x i)) ∧ f.HasAntitoneBasis fun (i : ℕ) ↦ s (x i)
have x_anti : Antitone.{0, u_1} (β := Set α) fun (i : ℕ) ↦ s (↑(x i) : ι')
Tactic: have x_anti : Antitone fun i => s (x i).1 :=
    antitone_nat_of_succ_le fun i => (hs.set_index_subset _).trans inter_subset_right
-- 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)
this : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i : ι' // p i } :=
  fun (n : ℕ) ↦
    Nat.recOn.{max 1 u_5} (motive := fun (x : ℕ) ↦ { i : ι' // p i }) n (hs.index (p := p) (s := s) (x' 0) ⋯)
      fun (n : ℕ) (xn : { i : ι' // p i }) ↦ hs.index (p := p) (s := s) (x' (n + 1) ∩ s (↑xn : ι')) ⋯
x_anti : Antitone.{0, u_1} (β := Set α) fun (i : ℕ) ↦ s (↑(x i) : ι')
⊢ ∃ (x : ℕ → ι'), (∀ (i : ℕ), p (x i)) ∧ f.HasAntitoneBasis fun (i : ℕ) ↦ s (x i)
have x_subset : ∀ (i : ℕ), s (↑(x i) : ι') ⊆ x' i
Tactic: have x_subset : ∀ i, s (x i).1 ⊆ x' i := by
    rintro (_ | i)
    exacts [hs.set_index_subset _, (hs.set_index_subset _).trans inter_subset_left]
-- 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 α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
this : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i : ι' // p i } :=
  fun (n : ℕ) ↦
    Nat.recOn.{max 1 u_5} (motive := fun (x : ℕ) ↦ { i : ι' // p i }) n (hs.index (p := p) (s := s) (x' 0) ⋯)
      fun (n : ℕ) (xn : { i : ι' // p i }) ↦ hs.index (p := p) (s := s) (x' (n + 1) ∩ s (↑xn : ι')) ⋯
x_anti : Antitone.{0, u_1} (β := Set α) fun (i : ℕ) ↦ s (↑(x i) : ι')
x_subset : ∀ (i : ℕ), s (↑(x i) : ι') ⊆ x' i
⊢ ∃ (x : ℕ → ι'), (∀ (i : ℕ), p (x i)) ∧ f.HasAntitoneBasis fun (i : ℕ) ↦ s (x i)
have refine : f.HasAntitoneBasis fun (i : ℕ) ↦ s ((fun (i : ℕ) ↦ (↑(x i) : ι')) i)
Tactic: refine ⟨fun i => (x i).1, fun i => (x i).2, ?_⟩
-- 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)
this : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i : ι' // p i } :=
  fun (n : ℕ) ↦
    Nat.recOn.{max 1 u_5} (motive := fun (x : ℕ) ↦ { i : ι' // p i }) n (hs.index (p := p) (s := s) (x' 0) ⋯)
      fun (n : ℕ) (xn : { i : ι' // p i }) ↦ hs.index (p := p) (s := s) (x' (n + 1) ∩ s (↑xn : ι')) ⋯
x_anti : Antitone.{0, u_1} (β := Set α) fun (i : ℕ) ↦ s (↑(x i) : ι')
x_subset : ∀ (i : ℕ), s (↑(x i) : ι') ⊆ x' i
⊢ f.HasAntitoneBasis fun (i : ℕ) ↦ s ((fun (i : ℕ) ↦ (↑(x i) : ι')) i)
have this₁ : HasAntitoneBasis.{u_1, 0} (α := α) (⨅ (i : ℕ), 𝓟 (s (↑(x i) : ι'))) fun (i : ℕ) ↦ s (↑(x i) : ι')
Tactic: have : (⨅ i, 𝓟 (s (x i).1)).HasAntitoneBasis fun i => s (x i).1 := .iInf_principal x_anti
-- 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 α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
this_1 : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i : ι' // p i } :=
  fun (n : ℕ) ↦
    Nat.recOn.{max 1 u_5} (motive := fun (x : ℕ) ↦ { i : ι' // p i }) n (hs.index (p := p) (s := s) (x' 0) ⋯)
      fun (n : ℕ) (xn : { i : ι' // p i }) ↦ hs.index (p := p) (s := s) (x' (n + 1) ∩ s (↑xn : ι')) ⋯
x_anti : Antitone.{0, u_1} (β := Set α) fun (i : ℕ) ↦ s (↑(x i) : ι')
x_subset : ∀ (i : ℕ), s (↑(x i) : ι') ⊆ x' i
this : HasAntitoneBasis.{u_1, 0} (α := α) (⨅ (i : ℕ), 𝓟 (s (↑(x i) : ι'))) fun (i : ℕ) ↦ s (↑(x i) : ι')
⊢ f.HasAntitoneBasis fun (i : ℕ) ↦ s ((fun (i : ℕ) ↦ (↑(x i) : ι')) i)
have h₁ : f = ⨅ (i : ℕ), 𝓟 (s (↑(x i) : ι'))
Tactic: convert! this
-- 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 α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
this_1 : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i : ι' // p i } :=
  fun (n : ℕ) ↦
    Nat.recOn.{max 1 u_5} (motive := fun (x : ℕ) ↦ { i : ι' // p i }) n (hs.index (p := p) (s := s) (x' 0) ⋯)
      fun (n : ℕ) (xn : { i : ι' // p i }) ↦ hs.index (p := p) (s := s) (x' (n + 1) ∩ s (↑xn : ι')) ⋯
x_anti : Antitone.{0, u_1} (β := Set α) fun (i : ℕ) ↦ s (↑(x i) : ι')
x_subset : ∀ (i : ℕ), s (↑(x i) : ι') ⊆ x' i
this : HasAntitoneBasis.{u_1, 0} (α := α) (⨅ (i : ℕ), 𝓟 (s (↑(x i) : ι'))) fun (i : ℕ) ↦ s (↑(x i) : ι')
i : ℕ
⊢ s (↑(x i) : ι') ∈ f
have zero : s (↑(x 0) : ι') ∈ f
Tactic: cases i
Cleared hypotheses: 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 α
hx' : f = ⨅ (i : ℕ), 𝓟 (x' i)
this_1 : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i : ι' // p i } :=
  fun (n : ℕ) ↦
    Nat.recOn.{max 1 u_5} (motive := fun (x : ℕ) ↦ { i : ι' // p i }) n (hs.index (p := p) (s := s) (x' 0) ⋯)
      fun (n : ℕ) (xn : { i : ι' // p i }) ↦ hs.index (p := p) (s := s) (x' (n + 1) ∩ s (↑xn : ι')) ⋯
x_anti : Antitone.{0, u_1} (β := Set α) fun (i : ℕ) ↦ s (↑(x i) : ι')
x_subset : ∀ (i : ℕ), s (↑(x i) : ι') ⊆ x' i
this : HasAntitoneBasis.{u_1, 0} (α := α) (⨅ (i : ℕ), 𝓟 (s (↑(x i) : ι'))) fun (i : ℕ) ↦ s (↑(x i) : ι')
i : ℕ
zero : s (↑(x 0) : ι') ∈ f
⊢ s (↑(x i) : ι') ∈ f
have succ : ∀ (n : ℕ), s (↑(x (n + 1)) : ι') ∈ f
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Sort u_5
f g : Filter α
inst : f.IsCountablyGenerated
inst_1 : g.IsCountablyGenerated
⊢ (f ⊓ g).IsCountablyGenerated
have rcases : ∀ (s : ℕ → Set α) (hs : f.HasAntitoneBasis s), (f ⊓ g).IsCountablyGenerated
Tactic: rcases f.exists_antitone_basis with ⟨s, hs⟩
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Sort u_5
f g : Filter α
inst : f.IsCountablyGenerated
inst_1 : g.IsCountablyGenerated
s : ℕ → Set α
hs : f.HasAntitoneBasis s
⊢ (f ⊓ g).IsCountablyGenerated
have rcases : ∀ (t : ℕ → Set α) (ht : g.HasAntitoneBasis t), (f ⊓ g).IsCountablyGenerated
Tactic: rcases g.exists_antitone_basis with ⟨t, ht⟩
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Sort u_5
f g : Filter α
inst : f.IsCountablyGenerated
inst_1 : g.IsCountablyGenerated
⊢ (f ⊔ g).IsCountablyGenerated
have rcases : ∀ (s : ℕ → Set α) (hs : f.HasAntitoneBasis s), (f ⊔ g).IsCountablyGenerated
Tactic: rcases f.exists_antitone_basis with ⟨s, hs⟩
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Sort u_5
f g : Filter α
inst : f.IsCountablyGenerated
inst_1 : g.IsCountablyGenerated
s : ℕ → Set α
hs : f.HasAntitoneBasis s
⊢ (f ⊔ g).IsCountablyGenerated
have rcases : ∀ (t : ℕ → Set α) (ht : g.HasAntitoneBasis t), (f ⊔ g).IsCountablyGenerated
Tactic: rcases g.exists_antitone_basis with ⟨t, ht⟩
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α : Type u_1
ι' : Sort u_5
inst : Countable ι'
x : ι' → Set α
⊢ IsCountablyGenerated.{u_1} (α := α) (⨅ (i : ι'), 𝓟 (x i))
have right : ⨅ (i : ι'), 𝓟 (x i) = generate (range x)
Tactic: use range x, countable_range x
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α : Type u_1
ι' : Sort u_5
inst : Countable ι'
x : ι' → Set α
⊢ ⨅ (i : ι'), 𝓟 (x i) = generate (range x)
have right : Eq.{u_1 + 1} (α := Filter α) (⨅ (i : ι'), 𝓟 (x i)) (⨅ s ∈ range x, 𝓟 s)
Tactic: rw [generate_eq_biInf, iInf_range]
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α : Type u_1
ι' : Sort u_5
inst : Countable ι'
x : ι' → Set α
right : Eq.{u_1 + 1} (α := Filter α) (⨅ (i : ι'), 𝓟 (x i)) (⨅ s ∈ range x, 𝓟 s)
⊢ ⨅ (i : ι'), 𝓟 (x i) = generate (range x)
have right₁ : Eq.{u_1 + 1} (α := Filter α) (⨅ (i : ι'), 𝓟 (x i)) (⨅ (i : ι'), 𝓟 (x i))
Tactic: rw [generate_eq_biInf, iInf_range]
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α : Type u_1
f : Filter α
h : ∃ (x : ℕ → Set α), f = ⨅ (i : ℕ), 𝓟 (x i)
⊢ f.IsCountablyGenerated
have rcases : ∀ (x : ℕ → Set α), IsCountablyGenerated.{u_1} (α := α) (⨅ (i : ℕ), 𝓟 (x i))
Tactic: rcases h with ⟨x, rfl⟩
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α : Type u_1
f : Filter α
⊢ f.IsCountablyGenerated ↔ ∃ (x : ℕ → Set α), f.HasAntitoneBasis x
have mp : f.IsCountablyGenerated → ∃ (x : ℕ → Set α), f.HasAntitoneBasis x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α : Type u_1
f : Filter α
mp : f.IsCountablyGenerated → ∃ (x : ℕ → Set α), f.HasAntitoneBasis x
⊢ f.IsCountablyGenerated ↔ ∃ (x : ℕ → Set α), f.HasAntitoneBasis x
have mpr : (∃ (x : ℕ → Set α), f.HasAntitoneBasis x) → f.IsCountablyGenerated
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α : Type u_1
f : Filter α
x : ℕ → Set α
h : f.HasAntitoneBasis x
⊢ f.IsCountablyGenerated
have mpr : IsCountablyGenerated.{u_1} (α := α) (⨅ (i : ℕ), 𝓟 (x i))
Tactic: rw [h.1.eq_iInf]
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α : Type u_1
a : α
⊢ IsCountablyGenerated (pure a)
have rw : IsCountablyGenerated (α := α) (𝓟 {a})
Tactic: rw [← principal_singleton]
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι_1 : Type u_4
ι' : Sort u_5
ι : Sort u_6
α : Type u_7
inst : Countable ι
f : ι → Filter α
inst_1 : ∀ (i : ι), (f i).IsCountablyGenerated
⊢ IsCountablyGenerated.{u_7} (α := α) (⨅ (i : ι), f i)
have choose : ∀ (s : (i : ι) → ℕ → Set α) (hs : ∀ (i : ι), (f i).HasAntitoneBasis (s i)),
  IsCountablyGenerated.{u_7} (α := α) (⨅ (i : ι), f i)
Tactic: choose s hs using fun i => exists_antitone_basis (f i)
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι_1 : Type u_4
ι' : Sort u_5
ι : Sort u_6
α : Type u_7
inst : Countable ι
f : ι → Filter α
inst_1 : ∀ (i : ι), (f i).IsCountablyGenerated
s : (i : ι) → ℕ → Set α
hs : ∀ (i : ι), (f i).HasAntitoneBasis (s i)
⊢ IsCountablyGenerated.{u_7} (α := α) (⨅ (i : ι), f i)
have rw : IsCountablyGenerated.{u_7} (α := α) (⨅ (x : PLift ι), f x.down)
Tactic: rw [← PLift.down_surjective.iInf_comp]
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι_1 : Type u_4
ι' : Sort u_5
ι : Sort u_6
α : Type u_7
inst : Countable ι
f : ι → Filter α
inst_1 : ∀ (i : ι), (f i).IsCountablyGenerated
s : (i : ι) → ℕ → Set α
hs : ∀ (i : ι), (f i).HasAntitoneBasis (s i)
⊢ IsCountablyGenerated.{u_7} (α := α) (⨅ (x : PLift ι), f x.down)
have refine : Set.Countable.{u_6} (α := (I : Set (PLift ι)) × ((i : (↑I : Type u_6)) → ℕ))
  {If : (I : Set (PLift ι)) × ((i : (↑I : Type u_6)) → ℕ) |
    If.fst (β := fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ).Finite ∧
      ∀ (i : (↑(If.fst (β := fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ)) : Type u_6)), True}
Tactic: refine HasCountableBasis.isCountablyGenerated ⟨.iInf fun n => (hs _).1, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι_1 : Type u_4
ι' : Sort u_5
ι : Sort u_6
α : Type u_7
inst : Countable ι
f : ι → Filter α
inst_1 : ∀ (i : ι), (f i).IsCountablyGenerated
s : (i : ι) → ℕ → Set α
hs : ∀ (i : ι), (f i).HasAntitoneBasis (s i)
⊢ Set.Countable.{u_6} (α := (I : Set (PLift ι)) × ((i : (↑I : Type u_6)) → ℕ))
    {If : (I : Set (PLift ι)) × ((i : (↑I : Type u_6)) → ℕ) |
      If.fst (β := fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ).Finite ∧
        ∀ (i : (↑(If.fst (β := fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ)) : Type u_6)), True}
have refine : Subset (α := Set ((I : Set (PLift ι)) × ((i : (↑I : Type u_6)) → ℕ)))
  {If : (I : Set (PLift ι)) × ((i : (↑I : Type u_6)) → ℕ) |
    If.fst (β := fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ).Finite ∧
      ∀ (i : (↑(If.fst (β := fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ)) : Type u_6)), True}
  (range (ι := (x : Finset (PLift ι)) × ((i : (↑(↑x : Set (PLift ι)) : Type u_6)) → ℕ))
    (Sigma.map (β₁ := fun (x : Finset (PLift ι)) ↦ (i : (↑(↑x : Set (PLift ι)) : Type u_6)) → ℕ) (β₂ :=
      fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ) SetLike.coe fun (x : Finset (PLift ι)) ↦ id))
Tactic: refine (countable_range <| Sigma.map ((↑) : Finset (PLift ι) → Set (PLift ι)) fun _ => id).mono ?_
-- Lean 4 proof step from Mathlib.Order.Filter.CountablyGenerated (goal)
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι_1 : Type u_4
ι' : Sort u_5
ι : Sort u_6
α : Type u_7
inst : Countable ι
f_1 : ι → Filter α
inst_1 : ∀ (i : ι), (f_1 i).IsCountablyGenerated
s : (i : ι) → ℕ → Set α
hs : ∀ (i : ι), (f_1 i).HasAntitoneBasis (s i)
I : Set (PLift ι)
f : (i : (↑I : Type u_6)) → ℕ
hI :
  (Sigma.fst (β := fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ)
      (Sigma.mk (β := fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ) I f)).Finite
⊢ Membership.mem (γ := Set ((I : Set (PLift ι)) × ((i : (↑I : Type u_6)) → ℕ)))
    (range (ι := (x : Finset (PLift ι)) × ((i : (↑(↑x : Set (PLift ι)) : Type u_6)) → ℕ))
      (Sigma.map (β₁ := fun (x : Finset (PLift ι)) ↦ (i : (↑(↑x : Set (PLift ι)) : Type u_6)) → ℕ) (β₂ :=
        fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ) SetLike.coe fun (x : Finset (PLift ι)) ↦ id))
    (Sigma.mk (β := fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ) I f)
have lift : ∀ (I : Finset (PLift ι)) (f : (i : (↑(↑I : Set (PLift ι)) : Type u_6)) → ℕ),
  Membership.mem (γ := Set ((I : Set (PLift ι)) × ((i : (↑I : Type u_6)) → ℕ)))
    (range (ι := (x : Finset (PLift ι)) × ((i : (↑(↑x : Set (PLift ι)) : Type u_6)) → ℕ))
      (Sigma.map (β₁ := fun (x : Finset (PLift ι)) ↦ (i : (↑(↑x : Set (PLift ι)) : Type u_6)) → ℕ) (β₂ :=
        fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ) SetLike.coe fun (x : Finset (PLift ι)) ↦ id))
    (Sigma.mk (β := fun (I : Set (PLift ι)) ↦ (i : (↑I : Type u_6)) → ℕ) (↑I : Set (PLift ι)) f)
Tactic: lift I to Finset (PLift ι) using hI
Cleared hypotheses: I, f, hI
-- Lean 4 proof step from Mathlib.Order.Filter.Curry (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
m : Filter β
p : α × β → Prop
⊢ (∃ᶠ (x : α × β) in l.curry m, p x) ↔ ∃ᶠ (x : α) in l, ∃ᶠ (y : β) in m, p (x, y)
have simp_rw : (¬∀ᶠ (x : α × β) in l.curry m, ¬p x) ↔ ¬∀ᶠ (x : α) in l, ¬¬∀ᶠ (x_1 : β) in m, ¬p (x, x_1)
Tactic: simp_rw [Filter.Frequently, not_iff_not, not_not, eventually_curry_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Curry (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
m : Filter β
p : α × β → Prop
simp_rw : (¬∀ᶠ (x : α × β) in l.curry m, ¬p x) ↔ ¬∀ᶠ (x : α) in l, ¬¬∀ᶠ (x_1 : β) in m, ¬p (x, x_1)
⊢ (∃ᶠ (x : α × β) in l.curry m, p x) ↔ ∃ᶠ (x : α) in l, ∃ᶠ (y : β) in m, p (x, y)
have simp_rw₁ : (∀ᶠ (x : α × β) in l.curry m, ¬p x) ↔ ∀ᶠ (x : α) in l, ¬¬∀ᶠ (x_1 : β) in m, ¬p (x, x_1)
Tactic: simp_rw [Filter.Frequently, not_iff_not, not_not, eventually_curry_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Curry (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
m : Filter β
p : α × β → Prop
simp_rw : (¬∀ᶠ (x : α × β) in l.curry m, ¬p x) ↔ ¬∀ᶠ (x : α) in l, ¬¬∀ᶠ (x_1 : β) in m, ¬p (x, x_1)
simp_rw₁ : (∀ᶠ (x : α × β) in l.curry m, ¬p x) ↔ ∀ᶠ (x : α) in l, ¬¬∀ᶠ (x_1 : β) in m, ¬p (x, x_1)
⊢ (∃ᶠ (x : α × β) in l.curry m, p x) ↔ ∃ᶠ (x : α) in l, ∃ᶠ (y : β) in m, p (x, y)
have simp_rw₂ : (∀ᶠ (x : α × β) in l.curry m, ¬p x) ↔ ∀ᶠ (x : α) in l, ∀ᶠ (x_1 : β) in m, ¬p (x, x_1)
Tactic: simp_rw [Filter.Frequently, not_iff_not, not_not, eventually_curry_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Defs (goal)
Goal:
α : Type u_1
s : Set α
⊢ Membership.mem (γ := Filter α) ⊤ s ↔ s = univ
have rw : (∀ (x : α), x ∈ s) ↔ s = univ
Tactic: rw [mem_top_iff_forall, eq_univ_iff_forall]
-- Lean 4 proof step from Mathlib.Order.Filter.Defs (goal)
Goal:
α : Type u_1
s : Set α
rw : (∀ (x : α), x ∈ s) ↔ s = univ
⊢ Membership.mem (γ := Filter α) ⊤ s ↔ s = univ
have rw₁ : (∀ (x : α), x ∈ s) ↔ ∀ (x : α), x ∈ s
Tactic: rw [mem_top_iff_forall, eq_univ_iff_forall]
-- Lean 4 proof step from Mathlib.Order.Filter.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
f_1 g_1 : Filter α
s t : Set α
f g : Filter α
y a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ g
xy : a ∩ b ⊆ y
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : Set α), a ∈ f ∧ ∃ (b : Set α), b ∈ g ∧ s = a ∩ b} y
have refine : y = (a ∪ y) ∩ (b ∪ y)
Tactic: refine ⟨a ∪ y, mem_of_superset ha subset_union_left, b ∪ y,
          mem_of_superset hb subset_union_left, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
f_1 g_1 : Filter α
s t : Set α
f g : Filter α
y a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ g
xy : a ∩ b ⊆ y
⊢ y = (a ∪ y) ∩ (b ∪ y)
have rw : y = a ∩ b ∪ y
Tactic: rw [← inter_union_distrib_right, union_eq_self_of_subset_left xy]
-- Lean 4 proof step from Mathlib.Order.Filter.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
f_1 g_1 : Filter α
s t : Set α
f g : Filter α
y a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ g
xy : a ∩ b ⊆ y
rw : y = a ∩ b ∪ y
⊢ y = (a ∪ y) ∩ (b ∪ y)
have rw₁ : y = y
Tactic: rw [← inter_union_distrib_right, union_eq_self_of_subset_left xy]
-- Lean 4 proof step from Mathlib.Order.Filter.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
f_1 g_1 : Filter α
s t : Set α
f g : Filter α
a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ g
c : Set α
hc : c ∈ f
d : Set α
hd : d ∈ g
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : Set α), a ∈ f ∧ ∃ (b : Set α), b ∈ g ∧ s = a ∩ b}
    (a ∩ b ∩ (c ∩ d))
have refine : a ∩ b ∩ (c ∩ d) = a ∩ c ∩ (b ∩ d)
Tactic: refine ⟨a ∩ c, inter_mem ha hc, b ∩ d, inter_mem hb hd, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
f_1 g_1 : Filter α
s t_1 : Set α
f g : Filter α
x y : Set α
hx : Membership.mem (γ := Set (Set α)) {s : Set α | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f} x
hy : Membership.mem (γ := Set (Set α)) {s : Set α | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f} y
t : Set α
htg : t ∈ g
ht : x ∩ y ⊆ t
⊢ t ∈ f
have rw : (x ∪ t) ∩ (y ∪ t) ∈ f
Tactic: rw [← union_eq_right.2 ht, inter_union_distrib_right]
-- Lean 4 proof step from Mathlib.Order.Filter.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
f_1 g_1 : Filter α
s t_1 : Set α
f g : Filter α
x y : Set α
hx : Membership.mem (γ := Set (Set α)) {s : Set α | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f} x
hy : Membership.mem (γ := Set (Set α)) {s : Set α | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f} y
t : Set α
htg : t ∈ g
ht : x ∩ y ⊆ t
⊢ (x ∪ t) ∩ (y ∪ t) ∈ f
have hs : x ∪ t ∈ f
Tactic: apply inter_mem
-- Lean 4 proof step from Mathlib.Order.Filter.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
f_1 g_1 : Filter α
s t_1 : Set α
f g : Filter α
x y : Set α
hx : Membership.mem (γ := Set (Set α)) {s : Set α | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f} x
hy : Membership.mem (γ := Set (Set α)) {s : Set α | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f} y
t : Set α
htg : t ∈ g
ht : x ∩ y ⊆ t
hs : x ∪ t ∈ f
⊢ (x ∪ t) ∩ (y ∪ t) ∈ f
have ht₁ : y ∪ t ∈ f
Tactic: apply inter_mem
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
f : Filter ℝ
hf : ¬IsCobounded (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f
⊢ f.limsSup = 0
have rwa : Eq (α := ℝ) (sInf {a : ℝ | ∀ᶠ (n : ℝ) in f, n ≤ a}) 0
Tactic: rwa [limsSup, sInf_of_not_bddBelow]
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
f : Filter ℝ
hf : ¬IsCobounded (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f
rwa : Eq (α := ℝ) (sInf {a : ℝ | ∀ᶠ (n : ℝ) in f, n ≤ a}) 0
⊢ f.limsSup = 0
have rwa₁ : Eq (α := ℝ) 0 0
Tactic: rwa [limsSup, sInf_of_not_bddBelow]
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
f : Filter ℝ
hf : ¬IsCobounded (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f
rwa : Eq (α := ℝ) (sInf {a : ℝ | ∀ᶠ (n : ℝ) in f, n ≤ a}) 0
rwa₁ : Eq (α := ℝ) 0 0
⊢ f.limsSup = 0
have rwa₂ : ¬BddBelow (α := ℝ) {a : ℝ | ∀ᶠ (n : ℝ) in f, n ≤ a}
Tactic: rwa [limsSup, sInf_of_not_bddBelow]
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
f : Filter ℝ
hf : ¬IsBounded (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f
⊢ Eq (α := ℝ) (sInf {a : ℝ | ∀ᶠ (n : ℝ) in f, n ≤ a}) 0
have h : Eq (α := Set ℝ) {a : ℝ | ∀ᶠ (n : ℝ) in f, n ≤ a} ∅
Tactic: convert! sInf_empty
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
f : Filter ℝ
hf : ¬IsCobounded (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f
⊢ f.limsInf = 0
have rwa : Eq (α := ℝ) (sSup {a : ℝ | ∀ᶠ (n : ℝ) in f, a ≤ n}) 0
Tactic: rwa [limsInf, sSup_of_not_bddAbove]
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
f : Filter ℝ
hf : ¬IsCobounded (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f
rwa : Eq (α := ℝ) (sSup {a : ℝ | ∀ᶠ (n : ℝ) in f, a ≤ n}) 0
⊢ f.limsInf = 0
have rwa₁ : Eq (α := ℝ) 0 0
Tactic: rwa [limsInf, sSup_of_not_bddAbove]
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
f : Filter ℝ
hf : ¬IsCobounded (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f
rwa : Eq (α := ℝ) (sSup {a : ℝ | ∀ᶠ (n : ℝ) in f, a ≤ n}) 0
rwa₁ : Eq (α := ℝ) 0 0
⊢ f.limsInf = 0
have rwa₂ : ¬BddAbove (α := ℝ) {a : ℝ | ∀ᶠ (n : ℝ) in f, a ≤ n}
Tactic: rwa [limsInf, sSup_of_not_bddAbove]
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
f : Filter ℝ
hf : ¬IsBounded (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f
⊢ Eq (α := ℝ) (sSup {a : ℝ | ∀ᶠ (n : ℝ) in f, a ≤ n}) 0
have h : Eq (α := Set ℝ) {a : ℝ | ∀ᶠ (n : ℝ) in f, a ≤ n} ∅
Tactic: convert! sSup_empty
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
⊢ (IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (i : ι) ↦ (↑(u i) : ℝ)) ↔
    IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
have simp : (∃ (b : ℝ), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ b) ↔ ∃ (x : ℝ) (_ : 0 ≤ x), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ x
Tactic: simp only [IsBoundedUnder, IsBounded, eventually_map, ← coe_le_coe, NNReal.exists, coe_mk]
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
⊢ (∃ (b : ℝ), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ b) ↔ ∃ (x : ℝ) (_ : 0 ≤ x), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ x
have mp : (∃ (b : ℝ), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ b) → ∃ (x : ℝ) (_ : 0 ≤ x), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
mp : (∃ (b : ℝ), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ b) → ∃ (x : ℝ) (_ : 0 ≤ x), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ x
⊢ (∃ (b : ℝ), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ b) ↔ ∃ (x : ℝ) (_ : 0 ≤ x), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ x
have mpr : (∃ (x : ℝ) (_ : 0 ≤ x), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ x) → ∃ (b : ℝ), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb : ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ b
⊢ ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ (↑b.toNNReal : ℝ)
have h : ∀ (a : ι), (↑(u a) : ℝ) ≤ b → (↑(u a) : ℝ) ≤ (↑b.toNNReal : ℝ)
Tactic: filter_upwards [hb]
-- Lean 4 proof step from Mathlib.Order.Filter.ENNReal (goal)
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
⊢ (IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f fun (i : ι) ↦ (↑(u i) : ℝ)) ↔
    IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f u
have simp : (∃ (b : ℝ), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≥ b) ↔ ∃ (x : ℝ) (_ : 0 ≤ x), ∀ᶠ (a : ι) in f, x ≤ (↑(u a) : ℝ)
Tactic: simp only [IsBoundedUnder, IsBounded, eventually_map, ← coe_le_coe, NNReal.exists, coe_mk]