awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
inst_2 : Nonempty X
s : Set X
hs : IsGδ s
hd : Dense s
h : IsMeagre s
t : Set X
hts : t ⊆ sᶜ
htG : IsGδ t
hd' : Dense t
x : X
hx₁ : x ∈ s
hx₂ : x ∈ t
⊢ False

Tactic:
hts hx₂ hx₁
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
inst_2 : Nonempty X
s : Set X
hs : IsGδ s
hd : Dense s
h : IsMeagre s
t : Set X
hts : t ⊆ sᶜ
htG : IsGδ t
hd' : Dense t
x : X
hx₁ : x ∈ s
hx₂ : x ∈ t
⊢ False

Tactic:
exact hts hx₂ hx₁
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
inst_2 : Nonempty X
s : Set X
hs : s ∈ residual X
rcases : ∀ (t : Set X) (ht_sub : t ⊆ s) (htGδ : IsGδ t) (ht_dense : Dense t), ¬IsMeagre s
⊢ ¬IsMeagre s

Tactic:
rcases (mem_residual (X := X)).1 hs with ⟨t, ht_sub, htGδ, ht_dense⟩

Premises used: mem_residual, Iff.mp
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
inst_2 : Nonempty X
s : Set X
hs : s ∈ residual X
t : Set X
ht_sub : t ⊆ s
htGδ : IsGδ t
ht_dense : Dense t
hs_meagre : IsMeagre s
⊢ False

Tactic:
not_isMeagre_of_isGδ_of_dense (X := X) htGδ ht_dense (hs_meagre.mono ht_sub)

Premises used: IsMeagre.mono, not_isMeagre_of_isGδ_of_dense
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
inst_2 : Nonempty X
s : Set X
hs : s ∈ residual X
t : Set X
ht_sub : t ⊆ s
htGδ : IsGδ t
ht_dense : Dense t
hs_meagre : IsMeagre s
⊢ False

Tactic:
exact not_isMeagre_of_isGδ_of_dense (X := X) htGδ ht_dense (hs_meagre.mono ht_sub)

Premises used: IsMeagre.mono, not_isMeagre_of_isGδ_of_dense
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
baire_property :
  ∀ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen (f n)) → (∀ (n : ℕ), Dense (f n)) → Dense.{u_1} (X := X) (⋂ (n : ℕ), f n)
⊢ BaireSpace X

Tactic:
constructor
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
baire_property : ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ ⋂ (n : ℕ), f n).Nonempty
⊢ Dense.{u_1} (X := X) (⋂ (n : ℕ), f n)

Tactic:
rw [dense_iff_inter_open]

Premises used: dense_iff_inter_open
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set X
U_open : IsOpen U
U_nonempty : U.Nonempty
rcases :
  ∀ (K₀ : PositiveCompacts X) (hK₀ : closure (↑K₀ : Set X) ⊆ U),
    ∃ (K : ℕ → PositiveCompacts X),
      (∀ (n : ℕ), K (n + 1) ≤ K n) ∧ (∀ (n : ℕ), closure (↑(K (n + 1)) : Set X) ⊆ f n) ∧ closure (↑(K 0) : Set X) ⊆ U
⊢ ∃ (K : ℕ → PositiveCompacts X),
    (∀ (n : ℕ), K (n + 1) ≤ K n) ∧ (∀ (n : ℕ), closure (↑(K (n + 1)) : Set X) ⊆ f n) ∧ closure (↑(K 0) : Set X) ⊆ U

Tactic:
rcases U_open.exists_positiveCompacts_closure_subset U_nonempty with ⟨K₀, hK₀⟩

Premises used: IsOpen.exists_positiveCompacts_closure_subset
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set X
U_open : IsOpen U
U_nonempty : U.Nonempty
K₀ : PositiveCompacts X
hK₀ : closure (↑K₀ : Set X) ⊆ U
⊢ ∀ (n : ℕ) (K : PositiveCompacts X), ∃ (K' : PositiveCompacts X), closure (↑K' : Set X) ⊆ f n ∩ interior (↑K : Set X)

Tactic:
fun n K ↦ ((ho n).inter isOpen_interior).exists_positiveCompacts_closure_subset ?_

Premises used: isOpen_interior, IsOpen.inter, IsOpen.exists_positiveCompacts_closure_subset
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set X
U_open : IsOpen U
U_nonempty : U.Nonempty
K₀ : PositiveCompacts X
hK₀ : closure (↑K₀ : Set X) ⊆ U
refine : ∀ (n : ℕ) (K : PositiveCompacts X), (f n ∩ interior (↑K : Set X)).Nonempty
⊢ ∀ (n : ℕ) (K : PositiveCompacts X), ∃ (K' : PositiveCompacts X), closure (↑K' : Set X) ⊆ f n ∩ interior (↑K : Set X)

Tactic:
refine fun n K ↦ ((ho n).inter isOpen_interior).exists_positiveCompacts_closure_subset ?_

Premises used: isOpen_interior, IsOpen.inter, IsOpen.exists_positiveCompacts_closure_subset
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set X
U_open : IsOpen U
U_nonempty : U.Nonempty
K₀ : PositiveCompacts X
hK₀ : closure (↑K₀ : Set X) ⊆ U
n : ℕ
K : PositiveCompacts X
rw : (interior (↑K : Set X) ∩ f n).Nonempty
⊢ (f n ∩ interior (↑K : Set X)).Nonempty

Tactic:
rw [inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set X
U_open : IsOpen U
U_nonempty : U.Nonempty
K₀ : PositiveCompacts X
hK₀ : closure (↑K₀ : Set X) ⊆ U
n : ℕ
K : PositiveCompacts X
⊢ (interior (↑K : Set X) ∩ f n).Nonempty

Tactic:
(hd n).inter_open_nonempty _ isOpen_interior K.interior_nonempty

Premises used: isOpen_interior, TopologicalSpace.PositiveCompacts.interior_nonempty, Dense.inter_open_nonempty
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set X
U_open : IsOpen U
U_nonempty : U.Nonempty
K₀ : PositiveCompacts X
hK₀ : closure (↑K₀ : Set X) ⊆ U
n : ℕ
K : PositiveCompacts X
⊢ (interior (↑K : Set X) ∩ f n).Nonempty

Tactic:
exact (hd n).inter_open_nonempty _ isOpen_interior K.interior_nonempty

Premises used: isOpen_interior, TopologicalSpace.PositiveCompacts.interior_nonempty, Dense.inter_open_nonempty
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set X
U_open : IsOpen U
U_nonempty : U.Nonempty
K₀ : PositiveCompacts X
hK₀ : closure (↑K₀ : Set X) ⊆ U
⊢ ∀ (n : ℕ) (K : PositiveCompacts X), ∃ (K' : PositiveCompacts X), closure (↑K' : Set X) ⊆ f n ∩ interior (↑K : Set X)

Tactic:
have : ∀ (n) (K : PositiveCompacts X),
        ∃ K' : PositiveCompacts X, closure ↑K' ⊆ f n ∩ interior K := by
      refine fun n K ↦ ((ho n).inter isOpen_interior).exists_positiveCompacts_closure_subset ?_
      rw [inter_comm]
      exact (hd n).inter_open_nonempty _ isOpen_interior K.interior_nonempty
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set X
U_open : IsOpen U
U_nonempty : U.Nonempty
K₀ : PositiveCompacts X
hK₀ : closure (↑K₀ : Set X) ⊆ U
this :
  ∀ (n : ℕ) (K : PositiveCompacts X), ∃ (K' : PositiveCompacts X), closure (↑K' : Set X) ⊆ f n ∩ interior (↑K : Set X)
choose :
  ∀ (K_next : (n : ℕ) → (K : PositiveCompacts X) → PositiveCompacts X)
    (hK_next : ∀ (n : ℕ) (K : PositiveCompacts X), closure (↑(K_next n K) : Set X) ⊆ f n ∩ interior (↑K : Set X)),
    ∃ (K : ℕ → PositiveCompacts X),
      (∀ (n : ℕ), K (n + 1) ≤ K n) ∧ (∀ (n : ℕ), closure (↑(K (n + 1)) : Set X) ⊆ f n) ∧ closure (↑(K 0) : Set X) ⊆ U
⊢ ∃ (K : ℕ → PositiveCompacts X),
    (∀ (n : ℕ), K (n + 1) ≤ K n) ∧ (∀ (n : ℕ), closure (↑(K (n + 1)) : Set X) ⊆ f n) ∧ closure (↑(K 0) : Set X) ⊆ U

Tactic:
choose K_next hK_next using this
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set X
U_open : IsOpen U
U_nonempty : U.Nonempty
K₀ : PositiveCompacts X
hK₀ : closure (↑K₀ : Set X) ⊆ U
K_next : (n : ℕ) → (K : PositiveCompacts X) → PositiveCompacts X
hK_next : ∀ (n : ℕ) (K : PositiveCompacts X), closure (↑(K_next n K) : Set X) ⊆ f n ∩ interior (↑K : Set X)
h :
  (∀ (n : ℕ),
      LE.le.{u_1} (α := PositiveCompacts X)
        ((fun (t : ℕ) ↦ Nat.rec (motive := fun (x : ℕ) ↦ PositiveCompacts X) K₀ K_next t) (n + 1))
        ((fun (t : ℕ) ↦ Nat.rec (motive := fun (x : ℕ) ↦ PositiveCompacts X) K₀ K_next t) n)) ∧
    (∀ (n : ℕ),
        closure (↑((fun (t : ℕ) ↦ Nat.rec (motive := fun (x : ℕ) ↦ PositiveCompacts X) K₀ K_next t) (n + 1)) : Set X) ⊆
          f n) ∧
      closure (↑((fun (t : ℕ) ↦ Nat.rec (motive := fun (x : ℕ) ↦ PositiveCompacts X) K₀ K_next t) 0) : Set X) ⊆ U
⊢ ∃ (K : ℕ → PositiveCompacts X),
    (∀ (n : ℕ), K (n + 1) ≤ K n) ∧ (∀ (n : ℕ), closure (↑(K (n + 1)) : Set X) ⊆ f n) ∧ closure (↑(K 0) : Set X) ⊆ U

Tactic:
use Nat.rec K₀ K_next
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set X
U_open : IsOpen U
U_nonempty : U.Nonempty
K₀ : PositiveCompacts X
hK₀ : closure (↑K₀ : Set X) ⊆ U
K_next : (n : ℕ) → (K : PositiveCompacts X) → PositiveCompacts X
hK_next : ∀ (n : ℕ) (K : PositiveCompacts X), closure (↑(K_next n K) : Set X) ⊆ f n ∩ interior (↑K : Set X)
⊢ (∀ (n : ℕ),
      LE.le.{u_1} (α := PositiveCompacts X)
        ((fun (t : ℕ) ↦ Nat.rec (motive := fun (x : ℕ) ↦ PositiveCompacts X) K₀ K_next t) (n + 1))
        ((fun (t : ℕ) ↦ Nat.rec (motive := fun (x : ℕ) ↦ PositiveCompacts X) K₀ K_next t) n)) ∧
    (∀ (n : ℕ),
        closure (↑((fun (t : ℕ) ↦ Nat.rec (motive := fun (x : ℕ) ↦ PositiveCompacts X) K₀ K_next t) (n + 1)) : Set X) ⊆
          f n) ∧
      closure (↑((fun (t : ℕ) ↦ Nat.rec (motive := fun (x : ℕ) ↦ PositiveCompacts X) K₀ K_next t) 0) : Set X) ⊆ U

Tactic:
⟨fun n ↦ ?_, fun n ↦ (hK_next n _).trans inter_subset_left, hK₀⟩

Premises used: Nat.rec, HasSubset.Subset.trans, Set.inter_subset_left, And.intro
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set X
U_open : IsOpen U
U_nonempty : U.Nonempty
K₀ : PositiveCompacts X
hK₀ : closure (↑K₀ : Set X) ⊆ U
K_next : (n : ℕ) → (K : PositiveCompacts X) → PositiveCompacts X
hK_next : ∀ (n : ℕ) (K : PositiveCompacts X), closure (↑(K_next n K) : Set X) ⊆ f n ∩ interior (↑K : Set X)
h :
  ∀ (n : ℕ),
    LE.le.{u_1} (α := PositiveCompacts X)
      ((fun (t : ℕ) ↦ Nat.rec (motive := fun (x : ℕ) ↦ PositiveCompacts X) K₀ K_next t) (n + 1))
      ((fun (t : ℕ) ↦ Nat.rec (motive := fun (x : ℕ) ↦ PositiveCompacts X) K₀ K_next t) n)
⊢ (∀ (n : ℕ),
      LE.le.{u_1} (α := PositiveCompacts X)
        ((fun (t : ℕ) ↦ Nat.rec (motive := fun (x : ℕ) ↦ PositiveCompacts X) K₀ K_next t) (n + 1))
        ((fun (t : ℕ) ↦ Nat.rec (motive := fun (x : ℕ) ↦ PositiveCompacts X) K₀ K_next t) n)) ∧
    (∀ (n : ℕ),
        closure (↑((fun (t : ℕ) ↦ Nat.rec (motive := fun (x : ℕ) ↦ PositiveCompacts X) K₀ K_next t) (n + 1)) : Set X) ⊆
          f n) ∧
      closure (↑((fun (t : ℕ) ↦ Nat.rec (motive := fun (x : ℕ) ↦ PositiveCompacts X) K₀ K_next t) 0) : Set X) ⊆ U

Tactic:
refine ⟨fun n ↦ ?_, fun n ↦ (hK_next n _).trans inter_subset_left, hK₀⟩
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set X
U_open : IsOpen U
U_nonempty : U.Nonempty
K₀ : PositiveCompacts X
hK₀ : closure (↑K₀ : Set X) ⊆ U
K_next : (n : ℕ) → (K : PositiveCompacts X) → PositiveCompacts X
hK_next : ∀ (n : ℕ) (K : PositiveCompacts X), closure (↑(K_next n K) : Set X) ⊆ f n ∩ interior (↑K : Set X)
n : ℕ
⊢ LE.le.{u_1} (α := PositiveCompacts X)
    ((fun (t : ℕ) ↦ Nat.rec (motive := fun (x : ℕ) ↦ PositiveCompacts X) K₀ K_next t) (n + 1))
    ((fun (t : ℕ) ↦ Nat.rec (motive := fun (x : ℕ) ↦ PositiveCompacts X) K₀ K_next t) n)

Tactic:
subset_closure.trans <| (hK_next _ _).trans <|
      inter_subset_right.trans interior_subset

Premises used: interior_subset, subset_closure, HasSubset.Subset.trans, Set.Subset, Set.inter_subset_right
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set X
U_open : IsOpen U
U_nonempty : U.Nonempty
K₀ : PositiveCompacts X
hK₀ : closure (↑K₀ : Set X) ⊆ U
K_next : (n : ℕ) → (K : PositiveCompacts X) → PositiveCompacts X
hK_next : ∀ (n : ℕ) (K : PositiveCompacts X), closure (↑(K_next n K) : Set X) ⊆ f n ∩ interior (↑K : Set X)
n : ℕ
⊢ LE.le.{u_1} (α := PositiveCompacts X)
    ((fun (t : ℕ) ↦ Nat.rec (motive := fun (x : ℕ) ↦ PositiveCompacts X) K₀ K_next t) (n + 1))
    ((fun (t : ℕ) ↦ Nat.rec (motive := fun (x : ℕ) ↦ PositiveCompacts X) K₀ K_next t) n)

Tactic:
exact subset_closure.trans <| (hK_next _ _).trans <|
      inter_subset_right.trans interior_subset

Premises used: interior_subset, subset_closure, HasSubset.Subset.trans, Set.inter_subset_right
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set X
U_open : IsOpen U
U_nonempty : U.Nonempty
baire_property :
  ∀ (K : ℕ → PositiveCompacts X) (hK_anti : ∀ (n : ℕ), K (n + 1) ≤ K n)
    (hKf : ∀ (n : ℕ), closure (↑(K (n + 1)) : Set X) ⊆ f n) (hKU : closure (↑(K 0) : Set X) ⊆ U),
    (U ∩ ⋂ (n : ℕ), f n).Nonempty
⊢ (U ∩ ⋂ (n : ℕ), f n).Nonempty

Tactic:
obtain ⟨K, hK_anti, hKf, hKU⟩ : ∃ K : ℕ → PositiveCompacts X,
      (∀ n, K (n + 1) ≤ K n) ∧ (∀ n, closure ↑(K (n + 1)) ⊆ f n) ∧ closure ↑(K 0) ⊆ U := by
    rcases U_open.exists_positiveCompacts_closure_subset U_nonempty with ⟨K₀, hK₀⟩
    have : ∀ (n) (K : PositiveCompacts X),
        ∃ K' : PositiveCompacts X, closure ↑K' ⊆ f n ∩ interior K := by
      refine fun n K ↦ ((ho n).inter isOpen_interior).exists_positiveCompacts_closure_subset ?_
      rw [inter_comm]
      exact (hd n).inter_open_nonempty _ isOpen_interior K.interior_nonempty
    choose K_next hK_next using this
    -- The next two lines are faster than a single `refine`.
    use Nat.rec K₀ K_next
    refine ⟨fun n ↦ ?_, fun n ↦ (hK_next n _).trans inter_subset_left, hK₀⟩
    exact subset_closure.trans <| (hK_next _ _).trans <|
      inter_subset_right.trans interior_subset
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set X
U_open : IsOpen U
U_nonempty : U.Nonempty
K : ℕ → PositiveCompacts X
hK_anti : ∀ (n : ℕ), K (n + 1) ≤ K n
hKf : ∀ (n : ℕ), closure (↑(K (n + 1)) : Set X) ⊆ f n
hKU : closure (↑(K 0) : Set X) ⊆ U
x : X
hx : Membership.mem (γ := Set X) (⋂ (n : ℕ), closure (↑(K n) : Set X)) x
simp : ∀ (hx : ∀ (i : ℕ), x ∈ closure (↑(K i) : Set X)), x ∈ U ∧ ∀ (i : ℕ), x ∈ f i
⊢ x ∈ U ∩ ⋂ (n : ℕ), f n

Tactic:
simp only [mem_iInter, mem_inter_iff] at hx ⊢

Premises used: Set.mem_inter_iff, Set.mem_iInter
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set X
U_open : IsOpen U
U_nonempty : U.Nonempty
K : ℕ → PositiveCompacts X
hK_anti : ∀ (n : ℕ), K (n + 1) ≤ K n
hKf : ∀ (n : ℕ), closure (↑(K (n + 1)) : Set X) ⊆ f n
hKU : closure (↑(K 0) : Set X) ⊆ U
x : X
hx : ∀ (i : ℕ), x ∈ closure (↑(K i) : Set X)
⊢ x ∈ U ∧ ∀ (i : ℕ), x ∈ f i

Tactic:
⟨hKU <| hx 0, fun n ↦ hKf n <| hx (n + 1)⟩

Premises used: HAdd.hAdd, And.intro, OfNat.ofNat
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set X
U_open : IsOpen U
U_nonempty : U.Nonempty
K : ℕ → PositiveCompacts X
hK_anti : ∀ (n : ℕ), K (n + 1) ≤ K n
hKf : ∀ (n : ℕ), closure (↑(K (n + 1)) : Set X) ⊆ f n
hKU : closure (↑(K 0) : Set X) ⊆ U
x : X
hx : ∀ (i : ℕ), x ∈ closure (↑(K i) : Set X)
⊢ x ∈ U ∧ ∀ (i : ℕ), x ∈ f i

Tactic:
exact ⟨hKU <| hx 0, fun n ↦ hKf n <| hx (n + 1)⟩
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set X
U_open : IsOpen U
U_nonempty : U.Nonempty
K : ℕ → PositiveCompacts X
hK_anti : ∀ (n : ℕ), K (n + 1) ≤ K n
hKf : ∀ (n : ℕ), closure (↑(K (n + 1)) : Set X) ⊆ f n
hKU : closure (↑(K 0) : Set X) ⊆ U
⊢ ⋂ (n : ℕ), closure (↑(K n) : Set X) ⊆ U ∩ ⋂ (n : ℕ), f n

Tactic:
have hK_subset : (⋂ n, closure (K n) : Set X) ⊆ U ∩ ⋂ n, f n := fun x hx ↦ by
    simp only [mem_iInter, mem_inter_iff] at hx ⊢
    exact ⟨hKU <| hx 0, fun n ↦ hKf n <| hx (n + 1)⟩
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set X
U_open : IsOpen U
U_nonempty : U.Nonempty
K : ℕ → PositiveCompacts X
hK_anti : ∀ (n : ℕ), K (n + 1) ≤ K n
hKf : ∀ (n : ℕ), closure (↑(K (n + 1)) : Set X) ⊆ f n
hKU : closure (↑(K 0) : Set X) ⊆ U
hK_subset : ⋂ (n : ℕ), closure (↑(K n) : Set X) ⊆ U ∩ ⋂ (n : ℕ), f n
⊢ Set.Nonempty.{u_1} (α := X) (⋂ (n : ℕ), closure (↑(K n) : Set X))

Tactic:
have hK_nonempty : (⋂ n, closure (K n) : Set X).Nonempty :=
    IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed _
      (fun n => closure_mono <| hK_anti n) (fun n => (K n).nonempty.closure)
      (K 0).isCompact.closure fun n => isClosed_closure
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set X
U_open : IsOpen U
U_nonempty : U.Nonempty
K : ℕ → PositiveCompacts X
hK_anti : ∀ (n : ℕ), K (n + 1) ≤ K n
hKf : ∀ (n : ℕ), closure (↑(K (n + 1)) : Set X) ⊆ f n
hKU : closure (↑(K 0) : Set X) ⊆ U
hK_subset : ⋂ (n : ℕ), closure (↑(K n) : Set X) ⊆ U ∩ ⋂ (n : ℕ), f n
hK_nonempty : Set.Nonempty.{u_1} (α := X) (⋂ (n : ℕ), closure (↑(K n) : Set X))
⊢ (U ∩ ⋂ (n : ℕ), f n).Nonempty

Tactic:
hK_nonempty.mono hK_subset

Premises used: Set.Nonempty.mono
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set X
U_open : IsOpen U
U_nonempty : U.Nonempty
K : ℕ → PositiveCompacts X
hK_anti : ∀ (n : ℕ), K (n + 1) ≤ K n
hKf : ∀ (n : ℕ), closure (↑(K (n + 1)) : Set X) ⊆ f n
hKU : closure (↑(K 0) : Set X) ⊆ U
hK_subset : ⋂ (n : ℕ), closure (↑(K n) : Set X) ⊆ U ∩ ⋂ (n : ℕ), f n
hK_nonempty : Set.Nonempty.{u_1} (α := X) (⋂ (n : ℕ), closure (↑(K n) : Set X))
⊢ (U ∩ ⋂ (n : ℕ), f n).Nonempty

Tactic:
exact hK_nonempty.mono hK_subset

Premises used: Set.Nonempty.mono
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
hG : IsGδ s
⊢ BaireSpace.{u_1} (↑(closure s) : Type u_1)

Tactic:
BaireSpace.of_t2Space_locallyCompactSpace

Premises used: BaireSpace.of_t2Space_locallyCompactSpace
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
hG : IsGδ s
convert_3 : R1Space.{u_1} (↑(closure s) : Type u_1)
convert_4 : LocallyCompactSpace.{u_1} (↑(closure s) : Type u_1)
⊢ BaireSpace.{u_1} (↑(closure s) : Type u_1)

Tactic:
convert! BaireSpace.of_t2Space_locallyCompactSpace using 1

Premises used: BaireSpace.of_t2Space_locallyCompactSpace
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
hG : IsGδ s
⊢ R1Space.{u_1} (↑(closure s) : Type u_1)

Tactic:
infer_instance
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
hG : IsGδ s
⊢ LocallyCompactSpace.{u_1} (↑(closure s) : Type u_1)

Tactic:
isClosed_closure.locallyCompactSpace

Premises used: IsClosed.locallyCompactSpace, isClosed_closure
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
hG : IsGδ s
⊢ LocallyCompactSpace.{u_1} (↑(closure s) : Type u_1)

Tactic:
exact isClosed_closure.locallyCompactSpace

Premises used: IsClosed.locallyCompactSpace, isClosed_closure
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
hG : IsGδ s
⊢ BaireSpace.{u_1} (↑(closure s) : Type u_1)

Tactic:
have : BaireSpace (closure s) := by
    convert! BaireSpace.of_t2Space_locallyCompactSpace using 1
    · infer_instance
    · exact isClosed_closure.locallyCompactSpace
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
hG : IsGδ s
this : BaireSpace.{u_1} (↑(closure s) : Type u_1)
⊢ Dense (X := { x : X // x ∈ closure s }) (Subtype.val (p := fun (x : X) ↦ x ∈ closure s) ⁻¹' s)

Tactic:
simp [Subtype.dense_iff, inter_eq_right.mpr subset_closure]

Premises used: Iff.mpr, Subtype.dense_iff, subset_closure, Set.inter_eq_right
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
hG : IsGδ s
this : BaireSpace.{u_1} (↑(closure s) : Type u_1)
⊢ BaireSpace.{u_1} (↑(Subtype.val (p := fun (x : X) ↦ x ∈ closure s) ⁻¹' s) : Type u_1)

Tactic:
have : BaireSpace ((↑) ⁻¹' s : Set (closure s)) :=
    (isGδ_induced continuous_subtype_val hG).baireSpace_of_dense
    (by simp [Subtype.dense_iff, inter_eq_right.mpr subset_closure])
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
hG : IsGδ s
this_1 : BaireSpace.{u_1} (↑(closure s) : Type u_1)
this : BaireSpace.{u_1} (↑(Subtype.val (p := fun (x : X) ↦ x ∈ closure s) ⁻¹' s) : Type u_1)
⊢ Function.LeftInverse
    (fun (x : (↑s : Type u_1)) ↦
      Subtype.mk (p := fun (x : (↑(closure s) : Type u_1)) ↦
        Membership.mem (γ := Set (↑(closure s) : Type u_1)) (Subtype.val (p := fun (x : X) ↦ x ∈ closure s) ⁻¹' s) x)
        (Subtype.mk (p := fun (x : X) ↦ x ∈ closure s) (↑x : X) ⋯) ⋯)
    fun (x : (↑(Subtype.val (p := fun (x : X) ↦ x ∈ closure s) ⁻¹' s) : Type u_1)) ↦
    Subtype.mk (p := fun (x : X) ↦ x ∈ s) (↑(↑x : (↑(closure s) : Type u_1)) : X) ⋯

Tactic:
grind