awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
hG : IsGδ s
hd : Dense s
f : ℕ → Set (↑s : Type u_1)
hof : ∀ (n : ℕ), IsOpen[instTopologicalSpaceSubtype] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
V : ℕ → Set X
hV : (∀ (n : ℕ), IsOpen[inst] (V n)) ∧ s = ⋂ (n : ℕ), V n
⊢ Dense.{u_1} (X := (↑s : Type u_1)) (⋂ (n : ℕ), f n)
have baire_property : ∀ (g : (n : ℕ) → Set X) (hg1 : ∀ (n : ℕ), IsOpen[inst] (g n)) (hg2 : ∀ (n : ℕ), Dense (g n))
  (hg3 : ∀ (n : ℕ), Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' g n = f n),
  Dense.{u_1} (X := (↑s : Type u_1)) (⋂ (n : ℕ), f n)
Tactic: choose g hg1 hg2 hg3 using fun n => exists_open_dense_of_open_dense_subtype hd (hof n) (hdf n)
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
hG : IsGδ s
hd : Dense s
f : ℕ → Set (↑s : Type u_1)
hof : ∀ (n : ℕ), IsOpen[instTopologicalSpaceSubtype] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
V : ℕ → Set X
hV : (∀ (n : ℕ), IsOpen[inst] (V n)) ∧ s = ⋂ (n : ℕ), V n
g : (n : ℕ) → Set X
hg1 : ∀ (n : ℕ), IsOpen[inst] (g n)
hg2 : ∀ (n : ℕ), Dense (g n)
hg3 : ∀ (n : ℕ), Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' g n = f n
⊢ Dense.{u_1} (X := (↑s : Type u_1)) (⋂ (n : ℕ), f n)
have h_inter_dense : Dense.{u_1} (X := X) (⋂ (n : ℕ), g n ∩ V n)
Tactic: have h_inter_dense : Dense (⋂ n, g n ∩ V n) := BaireSpace.baire_property (fun n ↦ g n ∩ V n)
    (fun n => (hg1 n).inter (hV.1 n))
    (fun n => (hg2 n).inter_of_isOpen_left (hd.mono (by simp [hV.2, iInter_subset])) (hg1 n))
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
hG : IsGδ s
hd : Dense s
f : ℕ → Set (↑s : Type u_1)
hof : ∀ (n : ℕ), IsOpen[instTopologicalSpaceSubtype] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
V : ℕ → Set X
hV : (∀ (n : ℕ), IsOpen[inst] (V n)) ∧ s = ⋂ (n : ℕ), V n
g : (n : ℕ) → Set X
hg1 : ∀ (n : ℕ), IsOpen[inst] (g n)
hg2 : ∀ (n : ℕ), Dense (g n)
hg3 : ∀ (n : ℕ), Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' g n = f n
h_inter_dense : Dense.{u_1} (X := X) (⋂ (n : ℕ), g n ∩ V n)
⊢ Eq.{u_1 + 1} (α := Set X) (⋂ (n : ℕ), g n ∩ V n)
    (image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (⋂ (n : ℕ), f n))
have h : ∀ (x : X),
  Membership.mem (γ := Set X) (⋂ (n : ℕ), g n ∩ V n) x ↔
    Membership.mem (γ := Set X)
      (image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (⋂ (n : ℕ), f n)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
hG : IsGδ s
hd : Dense s
f : ℕ → Set (↑s : Type u_1)
hof : ∀ (n : ℕ), IsOpen[instTopologicalSpaceSubtype] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
V : ℕ → Set X
hV : (∀ (n : ℕ), IsOpen[inst] (V n)) ∧ s = ⋂ (n : ℕ), V n
g : (n : ℕ) → Set X
hg1 : ∀ (n : ℕ), IsOpen[inst] (g n)
hg2 : ∀ (n : ℕ), Dense (g n)
hg3 : ∀ (n : ℕ), Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' g n = f n
h_inter_dense : Dense.{u_1} (X := X) (⋂ (n : ℕ), g n ∩ V n)
x : X
⊢ Membership.mem (γ := Set X) (⋂ (n : ℕ), g n ∩ V n) x ↔
    Membership.mem (γ := Set X)
      (image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (⋂ (n : ℕ), f n)) x
have h : ∀ (hG : IsGδ.{u_1} (X := X) (⋂ (n : ℕ), V n)) (hd : Dense.{u_1} (X := X) (⋂ (n : ℕ), V n))
  (hof : ∀ (n : ℕ), IsOpen[instTopologicalSpaceSubtype] (f n)) (hdf : ∀ (n : ℕ), Dense (f n))
  (hV_1 : (∀ (n : ℕ), IsOpen[inst] (V n)) ∧ s = ⋂ (n : ℕ), V n) (hg1 : ∀ (n : ℕ), IsOpen[inst] (g n))
  (hg2 : ∀ (n : ℕ), Dense (g n)) (hg3 : ∀ (n : ℕ), Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' g n = f n)
  (h_inter_dense : Dense.{u_1} (X := X) (⋂ (n : ℕ), g n ∩ V n)),
  (∀ (i : ℕ), x ∈ g i ∧ x ∈ V i) ↔
    ∃ (x_1 : ∀ (i : ℕ), x ∈ V i), ∀ (i : ℕ), Subtype.mk (p := fun (a : X) ↦ a ∈ s) x sorry ∈ f i
Tactic: simp_all
Cleared hypotheses: hG, hd, hof, hdf, hg1, hg2, hg3, h_inter_dense
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
hG : IsGδ s
hd : Dense s
f : ℕ → Set (↑s : Type u_1)
hof : ∀ (n : ℕ), IsOpen[instTopologicalSpaceSubtype] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
V : ℕ → Set X
hV : (∀ (n : ℕ), IsOpen[inst] (V n)) ∧ s = ⋂ (n : ℕ), V n
g : (n : ℕ) → Set X
hg1 : ∀ (n : ℕ), IsOpen[inst] (g n)
hg2 : ∀ (n : ℕ), Dense (g n)
hg3 : ∀ (n : ℕ), Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' g n = f n
h_inter_dense : Dense.{u_1} (X := X) (⋂ (n : ℕ), g n ∩ V n)
⊢ Dense.{u_1} (X := (↑s : Type u_1)) (⋂ (n : ℕ), f n)
have h_inter_eq : Eq.{u_1 + 1} (α := Set X) (⋂ (n : ℕ), g n ∩ V n)
  (image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (⋂ (n : ℕ), f n))
Tactic: have h_inter_eq : ⋂ n, g n ∩ V n = ⋂ n, f n := by ext; simp_all; grind
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
⊢ BaireSpace Y
have baire_property : ∀ (f : ℕ → Set Y), (∀ (n : ℕ), IsOpen[inst_2] (f n)) → (∀ (n : ℕ), Dense (f n)) → Dense.{u_4} (X := Y) (⋂ (n : ℕ), f n)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst_2] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : (n : ℕ) → Set X := fun (n : ℕ) ↦ p '' f n ∪ (closure[inst] s)ᶜ
⊢ Dense.{u_4} (X := Y) (⋂ (n : ℕ), f n)
have c_open : ∀ (n : ℕ), IsOpen[inst] (c n)
Tactic: have c_open (n : ℕ) : IsOpen (c n) := IsOpen.union (hp.isOpenMap (f n) (hof n))
    isClosed_closure.isOpen_compl
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst_2] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : (n : ℕ) → Set X := fun (n : ℕ) ↦ p '' f n ∪ (closure[inst] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst] (c n)
n : ℕ
⊢ Dense (c n)
have rw : closure[inst] (c n) ⊆ univ ∧ univ ⊆ closure[inst] (c n)
Tactic: rw [dense_iff_closure_eq, subset_antisymm_iff]
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst_2] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : (n : ℕ) → Set X := fun (n : ℕ) ↦ p '' f n ∪ (closure[inst] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst] (c n)
n : ℕ
⊢ interior (closure[inst] s) ∪ (interior (closure[inst] s))ᶜ ⊆ closure[inst] s ∪ (interior (closure[inst] s))ᶜ
have h₁ : interior (closure[inst] s) ⊆ closure[inst] s
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst_2] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : (n : ℕ) → Set X := fun (n : ℕ) ↦ p '' f n ∪ (closure[inst] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst] (c n)
n : ℕ
⊢ closure[inst] (c n) ⊆ univ ∧ univ ⊆ closure[inst] (c n)
have this : univ ⊆ closure[inst] (c n)
Tactic: have : univ ⊆ closure (c n) := calc
      _ ⊆ (interior (closure s)) ∪ (interior (closure s))ᶜ := by grind
      _ ⊆ closure s ∪ (interior (closure s))ᶜ := by gcongr; exact interior_subset
      _ ⊆ closure (p '' f n) ∪ (interior (closure s))ᶜ := union_subset_union
          (closure_minimal (hp.continuous.range_subset_closure_image_dense (hdf n))
          isClosed_closure) (subset_refl (interior (closure s))ᶜ)
      _ ⊆ closure (p '' f n) ∪ closure ((closure s)ᶜ) := union_subset_union (by simp) (by simp)
      _ = closure (c n) := closure_union.symm
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst_2] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : (n : ℕ) → Set X := fun (n : ℕ) ↦ p '' f n ∪ (closure[inst] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst] (c n)
⊢ Dense.{u_4} (X := Y) (⋂ (n : ℕ), f n)
have c_dense : ∀ (n : ℕ), Dense (c n)
Tactic: have c_dense (n : ℕ) : Dense (c n) := by
    rw [dense_iff_closure_eq, subset_antisymm_iff]
    have : univ ⊆ closure (c n) := calc
      _ ⊆ (interior (closure s)) ∪ (interior (closure s))ᶜ := by grind
      _ ⊆ closure s ∪ (interior (closure s))ᶜ := by gcongr; exact interior_subset
      _ ⊆ closure (p '' f n) ∪ (interior (closure s))ᶜ := union_subset_union
          (closure_minimal (hp.continuous.range_subset_closure_image_dense (hdf n))
          isClosed_closure) (subset_refl (interior (closure s))ᶜ)
      _ ⊆ closure (p '' f n) ∪ closure ((closure s)ᶜ) := union_subset_union (by simp) (by simp)
      _ = closure (c n) := closure_union.symm
    grind
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst_2] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : (n : ℕ) → Set X := fun (n : ℕ) ↦ p '' f n ∪ (closure[inst] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst] (c n)
c_dense : ∀ (n : ℕ), Dense (c n)
⊢ Dense.{u_4} (X := Y) (⋂ (n : ℕ), f n)
have c_inter_dense : Dense.{u_1} (X := X) (⋂ (n : ℕ), c n)
Tactic: have c_inter_dense : Dense (⋂ n, c n) := dense_iInter_of_isOpen_nat c_open c_dense
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst_2] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : (n : ℕ) → Set X := fun (n : ℕ) ↦ p '' f n ∪ (closure[inst] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst] (c n)
c_dense : ∀ (n : ℕ), Dense (c n)
c_inter_dense : Dense.{u_1} (X := X) (⋂ (n : ℕ), c n)
⊢ ⋂ (n : ℕ), f n = p ⁻¹' ⋂ (n : ℕ), c n
have h : ∀ (x : Y), Membership.mem (γ := Set Y) (⋂ (n : ℕ), f n) x ↔ x ∈ p ⁻¹' ⋂ (n : ℕ), c n
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst_2] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : (n : ℕ) → Set X := fun (n : ℕ) ↦ p '' f n ∪ (closure[inst] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst] (c n)
c_dense : ∀ (n : ℕ), Dense (c n)
c_inter_dense : Dense.{u_1} (X := X) (⋂ (n : ℕ), c n)
x : Y
⊢ Membership.mem (γ := Set Y) (⋂ (n : ℕ), f n) x ↔ x ∈ p ⁻¹' ⋂ (n : ℕ), c n
have h : (∀ (i : ℕ), x ∈ f i) ↔ ∀ (i : ℕ), p x ∈ p '' f i ∨ p x ∉ closure[inst] s
Tactic: simp only [mem_iInter, mem_preimage, mem_union, mem_compl_iff, c]
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst_2] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : (n : ℕ) → Set X := fun (n : ℕ) ↦ p '' f n ∪ (closure[inst] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst] (c n)
c_dense : ∀ (n : ℕ), Dense (c n)
c_inter_dense : Dense.{u_1} (X := X) (⋂ (n : ℕ), c n)
x : Y
⊢ (∀ (i : ℕ), x ∈ f i) ↔ ∀ (i : ℕ), p x ∈ p '' f i ∨ p x ∉ closure[inst] s
have h : ∀ (h : ∀ (i : ℕ), p x ∈ p '' f i ∨ p x ∉ closure[inst] s) (i : ℕ), x ∈ f i
Tactic: refine ⟨fun h i => by grind, fun h i => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst_2] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : (n : ℕ) → Set X := fun (n : ℕ) ↦ p '' f n ∪ (closure[inst] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst] (c n)
c_dense : ∀ (n : ℕ), Dense (c n)
c_inter_dense : Dense.{u_1} (X := X) (⋂ (n : ℕ), c n)
⊢ Dense.{u_4} (X := Y) (⋂ (n : ℕ), f n)
have c_inter_eq : ⋂ (n : ℕ), f n = p ⁻¹' ⋂ (n : ℕ), c n
Tactic: have c_inter_eq : ⋂ n, f n = p ⁻¹' (⋂ n, c n) := by
    ext x
    simp only [mem_iInter, mem_preimage, mem_union, mem_compl_iff, c]
    refine ⟨fun h i => by grind, fun h i => ?_⟩
    exact hp.injective.mem_set_image.mp (imp_iff_or_not.mpr (h i)
      (subset_closure (mem_range_self x)))
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
S : Set (Set X)
ho : ∀ s ∈ S, IsOpen[inst] s
hS : S.Countable
hd : ∀ s ∈ S, Dense s
⊢ Dense (⋂₀ S)
have inl : ∀ (h : S = ∅), Dense (⋂₀ S)
Tactic: rcases S.eq_empty_or_nonempty with h | h
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
S : Set (Set X)
ho : ∀ s ∈ S, IsOpen[inst] s
hS : S.Countable
hd : ∀ s ∈ S, Dense s
inl : ∀ (h : S = ∅), Dense (⋂₀ S)
⊢ Dense (⋂₀ S)
have inr : ∀ (h : S.Nonempty), Dense (⋂₀ S)
Tactic: rcases S.eq_empty_or_nonempty with h | h
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
S : Set (Set X)
ho : ∀ s ∈ S, IsOpen[inst] s
hS : S.Countable
hd : ∀ s ∈ S, Dense s
h : S.Nonempty
⊢ Dense (⋂₀ S)
have inr : ∀ (f : ℕ → Set X) (ho : ∀ s ∈ range f, IsOpen[inst] s) (hS : (range f).Countable) (hd : ∀ s ∈ range f, Dense s)
  (h : (range f).Nonempty), Dense (⋂₀ range f)
Tactic: rcases hS.exists_eq_range h with ⟨f, rfl⟩
Cleared hypotheses: S, ho, hS, hd, h
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
α : Type u_2
inst : TopologicalSpace X
inst_1 : BaireSpace X
S : Set α
f : α → Set X
ho : ∀ s ∈ S, IsOpen[inst] (f s)
hS : S.Countable
hd : ∀ s ∈ S, Dense (f s)
⊢ Dense.{u_1} (X := X) (⋂ s ∈ S, f s)
have rw : Dense (⋂₀ (f '' S))
Tactic: rw [← sInter_image]
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
α : Type u_2
inst : TopologicalSpace X
inst_1 : BaireSpace X
S : Set α
f : α → Set X
ho : ∀ s ∈ S, IsOpen[inst] (f s)
hS : S.Countable
hd : ∀ s ∈ S, Dense (f s)
⊢ Dense (⋂₀ (f '' S))
have refine_1 : ∀ s ∈ f '' S, IsOpen[inst] s
Tactic: refine dense_sInter_of_isOpen ?_ (hS.image _) ?_
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
α : Type u_2
inst : TopologicalSpace X
inst_1 : BaireSpace X
S : Set α
f : α → Set X
ho : ∀ s ∈ S, IsOpen[inst] (f s)
hS : S.Countable
hd : ∀ s ∈ S, Dense (f s)
refine_1 : ∀ s ∈ f '' S, IsOpen[inst] s
⊢ Dense (⋂₀ (f '' S))
have refine_2 : ∀ s ∈ f '' S, Dense s
Tactic: refine dense_sInter_of_isOpen ?_ (hS.image _) ?_
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
⊢ s ∈ residual X ↔ ∃ t ⊆ s, IsGδ t ∧ Dense t
have mp : s ∈ residual X → ∃ t ⊆ s, IsGδ t ∧ Dense t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
mp : s ∈ residual X → ∃ t ⊆ s, IsGδ t ∧ Dense t
⊢ s ∈ residual X ↔ ∃ t ⊆ s, IsGδ t ∧ Dense t
have mpr : (∃ t ⊆ s, IsGδ t ∧ Dense t) → s ∈ residual X
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
⊢ s ∈ residual X → ∃ t ⊆ s, IsGδ t ∧ Dense t
have mp : (∃ (S : Set (Set X)), (∀ t ∈ S, IsOpen[inst] t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ⋂₀ S ⊆ s) →
  ∃ t ⊆ s, IsGδ t ∧ Dense t
Tactic: rw [mem_residual_iff]
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
S : Set (Set X)
hSo : ∀ t ∈ S, IsOpen[inst] t
hSd : ∀ t ∈ S, Dense t
Sct : S.Countable
Ss : ⋂₀ S ⊆ s
⊢ ∃ t ⊆ s, IsGδ t ∧ Dense t
have mp : Dense (⋂₀ S)
Tactic: refine ⟨_, Ss, ⟨_, fun t ht => hSo _ ht, Sct, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
p : X → Prop
⊢ (∀ᶠ (x : X) in residual X, p x) ↔ ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
have simp : (∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t) ↔ ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
Tactic: simp only [Filter.Eventually, mem_residual, subset_def, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
p : X → Prop
⊢ (∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t) ↔ ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
have mp : (∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t) → ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
p : X → Prop
mp : (∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t) → ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
⊢ (∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t) ↔ ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
have mpr : (∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x) → ∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
p : X → Prop
mp : (∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t) → ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
mpr : (∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x) → ∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t
⊢ (∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t) ↔ ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
have mp₁ : ∀ (w : Set X), (∀ x ∈ w, p x) → IsGδ w → Dense w → ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
p : X → Prop
mp : (∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t) → ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
mpr : (∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x) → ∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t
mp₁ mp₂ mp₃ : ∀ (w : Set X), (∀ x ∈ w, p x) → IsGδ w → Dense w → ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
⊢ (∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t) ↔ ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
have mpr₁ : ∀ (w : Set X), IsGδ w → Dense w → (∀ x ∈ w, p x) → ∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
p : X → Prop
mp : (∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t) → ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
mpr : (∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x) → ∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t
mp₁ mp₂ mp₃ : ∀ (w : Set X), (∀ x ∈ w, p x) → IsGδ w → Dense w → ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
mpr₁ mpr₂ mpr₃ : ∀ (w : Set X), IsGδ w → Dense w → (∀ x ∈ w, p x) → ∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t
mp₄ mp₅ mp₆ : ∀ (w : Set X), (∀ x ∈ w, p x) → IsGδ w → Dense w → ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
mpr₄ mpr₅ mpr₆ : ∀ (w : Set X), IsGδ w → Dense w → (∀ x ∈ w, p x) → ∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t
mp₇ mp₈ : ∀ (w : Set X), (∀ x ∈ w, p x) → IsGδ w → Dense w → ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
⊢ (∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t) ↔ ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
have mp₉ : ∀ (w : Set X), (∀ x ∈ w, p x) → IsGδ w → Dense w → IsGδ w ∧ Dense w ∧ ∀ x ∈ w, p x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
p : X → Prop
mp : (∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t) → ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
mpr : (∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x) → ∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t
mp₁ mp₂ mp₃ : ∀ (w : Set X), (∀ x ∈ w, p x) → IsGδ w → Dense w → ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
mpr₁ mpr₂ mpr₃ : ∀ (w : Set X), IsGδ w → Dense w → (∀ x ∈ w, p x) → ∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t
mp₄ mp₅ mp₆ : ∀ (w : Set X), (∀ x ∈ w, p x) → IsGδ w → Dense w → ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
mpr₄ mpr₅ mpr₆ : ∀ (w : Set X), IsGδ w → Dense w → (∀ x ∈ w, p x) → ∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t
mp₇ mp₈ : ∀ (w : Set X), (∀ x ∈ w, p x) → IsGδ w → Dense w → ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
mp₉ : ∀ (w : Set X), (∀ x ∈ w, p x) → IsGδ w → Dense w → IsGδ w ∧ Dense w ∧ ∀ x ∈ w, p x
⊢ (∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t) ↔ ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
have mp₁₀ : (w : Set X) → (∀ x ∈ w, p x) → IsGδ w → Dense w → Set X
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
p : X → Prop
mp : (∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t) → ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
mpr : (∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x) → ∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t
mp₁ mp₂ mp₃ : ∀ (w : Set X), (∀ x ∈ w, p x) → IsGδ w → Dense w → ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
mpr₁ mpr₂ mpr₃ : ∀ (w : Set X), IsGδ w → Dense w → (∀ x ∈ w, p x) → ∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t
mp₄ mp₅ mp₆ : ∀ (w : Set X), (∀ x ∈ w, p x) → IsGδ w → Dense w → ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
mpr₄ mpr₅ mpr₆ : ∀ (w : Set X), IsGδ w → Dense w → (∀ x ∈ w, p x) → ∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t
mp₇ mp₈ : ∀ (w : Set X), (∀ x ∈ w, p x) → IsGδ w → Dense w → ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
mp₉ : ∀ (w : Set X), (∀ x ∈ w, p x) → IsGδ w → Dense w → IsGδ w ∧ Dense w ∧ ∀ x ∈ w, p x
mp₁₀ : (w : Set X) → (∀ x ∈ w, p x) → IsGδ w → Dense w → Set X
mp₁₁ : ∀ (w : Set X), (∀ x ∈ w, p x) → IsGδ w → Dense w → IsGδ w ∧ Dense w ∧ ∀ x ∈ w, p x
mp₁₂ : (w : Set X) → (∀ x ∈ w, p x) → IsGδ w → Dense w → Set X
mpr₇ mpr₈ : ∀ (w : Set X), IsGδ w → Dense w → (∀ x ∈ w, p x) → ∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t
⊢ (∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t) ↔ ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
have mpr₉ : ∀ (w : Set X), IsGδ w → Dense w → (∀ x ∈ w, p x) → (∀ x ∈ w, p x) ∧ IsGδ w ∧ Dense w
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
p : X → Prop
mp : (∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t) → ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
mpr : (∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x) → ∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t
mp₁ mp₂ mp₃ : ∀ (w : Set X), (∀ x ∈ w, p x) → IsGδ w → Dense w → ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
mpr₁ mpr₂ mpr₃ : ∀ (w : Set X), IsGδ w → Dense w → (∀ x ∈ w, p x) → ∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t
mp₄ mp₅ mp₆ : ∀ (w : Set X), (∀ x ∈ w, p x) → IsGδ w → Dense w → ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
mpr₄ mpr₅ mpr₆ : ∀ (w : Set X), IsGδ w → Dense w → (∀ x ∈ w, p x) → ∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t
mp₇ mp₈ : ∀ (w : Set X), (∀ x ∈ w, p x) → IsGδ w → Dense w → ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
mp₉ : ∀ (w : Set X), (∀ x ∈ w, p x) → IsGδ w → Dense w → IsGδ w ∧ Dense w ∧ ∀ x ∈ w, p x
mp₁₀ : (w : Set X) → (∀ x ∈ w, p x) → IsGδ w → Dense w → Set X
mp₁₁ : ∀ (w : Set X), (∀ x ∈ w, p x) → IsGδ w → Dense w → IsGδ w ∧ Dense w ∧ ∀ x ∈ w, p x
mp₁₂ : (w : Set X) → (∀ x ∈ w, p x) → IsGδ w → Dense w → Set X
mpr₇ mpr₈ : ∀ (w : Set X), IsGδ w → Dense w → (∀ x ∈ w, p x) → ∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t
mpr₉ : ∀ (w : Set X), IsGδ w → Dense w → (∀ x ∈ w, p x) → (∀ x ∈ w, p x) ∧ IsGδ w ∧ Dense w
⊢ (∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t) ↔ ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
have mpr₁₀ : (w : Set X) → IsGδ w → Dense w → (∀ x ∈ w, p x) → Set X
Tactic: tauto