awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
tX : TopologicalSpace X
u : Set X
⊢ (∀ (n : ℕ) (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)) ↔
    ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)

Tactic:
forall_congr' fun n ↦ ?_

Premises used: forall_congr'
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
tX : TopologicalSpace X
u : Set X
a :
  ∀ (n : ℕ),
    (∀ (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)) ↔
      ∀ (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)
⊢ (∀ (n : ℕ) (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)) ↔
    ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)

Tactic:
refine forall_congr' fun n ↦ ?_

Premises used: forall_congr'
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
tX : TopologicalSpace X
u : Set X
n : ℕ
⊢ (∀ (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)) ↔
    ∀ (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)

Tactic:
⟨fun h p ↦ h <| @ContinuousMap.mk _ _ _ (_) p ?_, fun h p ↦ h ⟨p, ?_⟩⟩

Premises used: ContinuousMap.mk, Iff.intro, DFunLike.coe
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
tX : TopologicalSpace X
u : Set X
n : ℕ
a :
  ∀ (h : ∀ (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)) (p : C(Fin n → ℝ, X)),
    Continuous[_, deltaGenerated X] (⇑p : (a : Fin n → ℝ) → X)
a₁ :
  ∀ (h : ∀ (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)) (p : C(Fin n → ℝ, X)),
    Continuous[_, tX] (⇑p : (a : Fin n → ℝ) → X)
⊢ (∀ (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)) ↔
    ∀ (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)

Tactic:
refine ⟨fun h p ↦ h <| @ContinuousMap.mk _ _ _ (_) p ?_, fun h p ↦ h ⟨p, ?_⟩⟩
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
tX : TopologicalSpace X
u : Set X
n : ℕ
h : ∀ (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)
p : C(Fin n → ℝ, X)
⊢ Continuous[_, deltaGenerated X] (⇑p : (a : Fin n → ℝ) → X)

Tactic:
continuous_euclidean_to_deltaGenerated.mpr p.2

Premises used: Iff.mpr, _private.0.continuous_euclidean_to_deltaGenerated, ContinuousMap.continuous_toFun
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
tX : TopologicalSpace X
u : Set X
n : ℕ
h : ∀ (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)
p : C(Fin n → ℝ, X)
⊢ Continuous[_, deltaGenerated X] (⇑p : (a : Fin n → ℝ) → X)

Tactic:
exact continuous_euclidean_to_deltaGenerated.mpr p.2

Premises used: Iff.mpr, _private.0.continuous_euclidean_to_deltaGenerated, ContinuousMap.continuous_toFun
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
tX : TopologicalSpace X
u : Set X
n : ℕ
h : ∀ (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)
p : C(Fin n → ℝ, X)
⊢ Continuous[_, tX] (⇑p : (a : Fin n → ℝ) → X)

Tactic:
continuous_euclidean_to_deltaGenerated.mp <| @ContinuousMap.continuous_toFun _ _ _ (_) p

Premises used: _private.0.continuous_euclidean_to_deltaGenerated, ContinuousMap.continuous_toFun, Iff.mp
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
tX : TopologicalSpace X
u : Set X
n : ℕ
h : ∀ (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)
p : C(Fin n → ℝ, X)
⊢ Continuous[_, tX] (⇑p : (a : Fin n → ℝ) → X)

Tactic:
exact continuous_euclidean_to_deltaGenerated.mp <| @ContinuousMap.continuous_toFun _ _ _ (_) p

Premises used: _private.0.continuous_euclidean_to_deltaGenerated, ContinuousMap.continuous_toFun, Iff.mp
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
tX : TopologicalSpace X
inst : DeltaGeneratedSpace X
⊢ tX = deltaGenerated X

Tactic:
eq_of_le_of_ge DeltaGeneratedSpace.le_deltaGenerated deltaGenerated_le

Premises used: deltaGenerated_le, DeltaGeneratedSpace.le_deltaGenerated, eq_of_le_of_ge
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
tX : TopologicalSpace X
inst : DeltaGeneratedSpace X
u : Set X
nth_rewrite :
  IsOpen[deltaGenerated X] u ↔
    ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)
⊢ IsOpen[tX] u ↔ ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)

Tactic:
nth_rewrite 1 [eq_deltaGenerated (X := X)]

Premises used: eq_deltaGenerated
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
tX : TopologicalSpace X
inst : DeltaGeneratedSpace X
u : Set X
⊢ IsOpen[deltaGenerated X] u ↔
    ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)

Tactic:
isOpen_deltaGenerated_iff

Premises used: isOpen_deltaGenerated_iff
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
tX : TopologicalSpace X
inst : DeltaGeneratedSpace X
u : Set X
⊢ IsOpen[deltaGenerated X] u ↔
    ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), IsOpen (X := Fin n → ℝ) ((⇑p : (a : Fin n → ℝ) → X) ⁻¹' u)

Tactic:
exact isOpen_deltaGenerated_iff

Premises used: isOpen_deltaGenerated_iff
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : DeltaGeneratedSpace X
f : X → Y
simp_rw :
  coinduced f tX ≤ tY ↔
    ∀ (n : ℕ) (p : C(Fin n → ℝ, X)),
      coinduced (X := Fin n → ℝ) (f ∘ (⇑p : (a : Fin n → ℝ) → X)) (Pi.topologicalSpace (Y := fun (a : Fin n) ↦ ℝ)) ≤ tY
⊢ Continuous[tX, tY] f ↔ ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), Continuous[_, tY] (f ∘ (⇑p : (a : Fin n → ℝ) → X))

Tactic:
simp_rw [continuous_iff_coinduced_le]

Premises used: continuous_iff_coinduced_le
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : DeltaGeneratedSpace X
f : X → Y
nth_rewrite :
  coinduced f
        (⨆ (f : (n : ℕ) × C(Fin n → ℝ, X)),
          coinduced (X := Fin (f.fst (β := fun (n : ℕ) ↦ C(Fin n → ℝ, X))) → ℝ)
            (⇑(f.snd (β := fun (n : ℕ) ↦ C(Fin n → ℝ, X))) : (a : Fin f.fst → ℝ) → X) inferInstance) ≤
      tY ↔
    ∀ (n : ℕ) (p : C(Fin n → ℝ, X)),
      coinduced (X := Fin n → ℝ) (f ∘ (⇑p : (a : Fin n → ℝ) → X)) (Pi.topologicalSpace (Y := fun (a : Fin n) ↦ ℝ)) ≤ tY
⊢ coinduced f tX ≤ tY ↔
    ∀ (n : ℕ) (p : C(Fin n → ℝ, X)),
      coinduced (X := Fin n → ℝ) (f ∘ (⇑p : (a : Fin n → ℝ) → X)) (Pi.topologicalSpace (Y := fun (a : Fin n) ↦ ℝ)) ≤ tY

Tactic:
nth_rewrite 1 [eq_deltaGenerated (X := X), deltaGenerated]

Premises used: TopologicalSpace.deltaGenerated, eq_deltaGenerated
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : DeltaGeneratedSpace X
f : X → Y
⊢ coinduced f
        (⨆ (f : (n : ℕ) × C(Fin n → ℝ, X)),
          coinduced (X := Fin (f.fst (β := fun (n : ℕ) ↦ C(Fin n → ℝ, X))) → ℝ)
            (⇑(f.snd (β := fun (n : ℕ) ↦ C(Fin n → ℝ, X))) : (a : Fin f.fst → ℝ) → X) inferInstance) ≤
      tY ↔
    ∀ (n : ℕ) (p : C(Fin n → ℝ, X)),
      coinduced (X := Fin n → ℝ) (f ∘ (⇑p : (a : Fin n → ℝ) → X)) (Pi.topologicalSpace (Y := fun (a : Fin n) ↦ ℝ)) ≤ tY

Tactic:
simp [coinduced_compose, Sigma.forall]

Premises used: Sigma.forall, coinduced_compose
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : DeltaGeneratedSpace X
f : X → Y
simp_rw :
  (∀ (n : ℕ) (p : C(Fin n → ℝ, X)), Continuous[_, deltaGenerated Y] (f ∘ (⇑p : (a : Fin n → ℝ) → X))) ↔
    ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), Continuous[_, tY] (f ∘ (⇑p : (a : Fin n → ℝ) → X))
⊢ Continuous[tX, deltaGenerated Y] f ↔ Continuous[tX, tY] f

Tactic:
simp_rw [DeltaGeneratedSpace.continuous_iff, continuous_euclidean_to_deltaGenerated]

Premises used: _private.0.continuous_euclidean_to_deltaGenerated, DeltaGeneratedSpace.continuous_iff
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_3
t : TopologicalSpace X
x : TopologicalSpace X := deltaGenerated X
le_deltaGenerated : deltaGenerated X ≤ deltaGenerated X
⊢ DeltaGeneratedSpace X

Tactic:
constructor
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_3
t : TopologicalSpace X
x : TopologicalSpace X := deltaGenerated X
le_deltaGenerated le_deltaGenerated₁ : deltaGenerated X ≤ deltaGenerated X
⊢ deltaGenerated X ≤ deltaGenerated X

Tactic:
rw [@deltaGenerated_deltaGenerated_eq X t]

Premises used: deltaGenerated_deltaGenerated_eq
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_3
t₁ t₂ : TopologicalSpace X
h : t₁ ≤ t₂
rw : Continuous[deltaGenerated X, t₂] id
⊢ deltaGenerated X ≤ deltaGenerated X

Tactic:
rw [← continuous_id_iff_le, @continuous_to_deltaGenerated _ _
    (@deltaGenerated X t₁) t₂ deltaGeneratedSpace_deltaGenerated id]

Premises used: continuous_to_deltaGenerated, continuous_id_iff_le
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_3
t₁ t₂ : TopologicalSpace X
h : t₁ ≤ t₂
⊢ Continuous[deltaGenerated X, t₂] id

Tactic:
continuous_id_iff_le.2 <| (@deltaGenerated_le X t₁).trans h

Premises used: Iff.mpr, deltaGenerated_le, continuous_id_iff_le, LE.le.trans
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_3
t₁ t₂ : TopologicalSpace X
h : t₁ ≤ t₂
⊢ Continuous[deltaGenerated X, t₂] id

Tactic:
exact continuous_id_iff_le.2 <| (@deltaGenerated_le X t₁).trans h

Premises used: Iff.mpr, deltaGenerated_le, continuous_id_iff_le, LE.le.trans
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
⊢ DeltaGeneratedSpace.{u_1} (of X)

Tactic:
deltaGeneratedSpace_deltaGenerated

Premises used: deltaGeneratedSpace_deltaGenerated, DeltaGeneratedSpace.of
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
tX : TopologicalSpace X
rw : coinduced counit instTopologicalSpaceOf ≤ tX
⊢ Continuous[instTopologicalSpaceOf, tX] counit

Tactic:
rw [continuous_iff_coinduced_le]

Premises used: continuous_iff_coinduced_le
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
tX : TopologicalSpace X
⊢ coinduced counit instTopologicalSpaceOf ≤ tX

Tactic:
deltaGenerated_le

Premises used: deltaGenerated_le, DeltaGeneratedSpace.counit, Set.Mem, iSup, setOf, Set.preimage, IsOpen, DeltaGeneratedSpace.of
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
tX : TopologicalSpace X
⊢ coinduced counit instTopologicalSpaceOf ≤ tX

Tactic:
exact deltaGenerated_le

Premises used: deltaGenerated_le
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : DeltaGeneratedSpace X
rw : LocPathConnectedSpace X
⊢ LocPathConnectedSpace X

Tactic:
rw [eq_deltaGenerated (X := X), deltaGenerated_eq_coinduced]

Premises used: deltaGenerated_eq_coinduced, eq_deltaGenerated
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : DeltaGeneratedSpace X
⊢ LocPathConnectedSpace X

Tactic:
LocPathConnectedSpace.coinduced _

Premises used: LocPathConnectedSpace.coinduced
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : DeltaGeneratedSpace X
⊢ LocPathConnectedSpace X

Tactic:
exact LocPathConnectedSpace.coinduced _

Premises used: LocPathConnectedSpace.coinduced
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : DeltaGeneratedSpace X
rw : SequentialSpace X
⊢ SequentialSpace X

Tactic:
rw [eq_deltaGenerated (X := X)]

Premises used: eq_deltaGenerated
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : DeltaGeneratedSpace X
⊢ SequentialSpace X

Tactic:
SequentialSpace.iSup fun p ↦ SequentialSpace.coinduced p.2

Premises used: SequentialSpace.iSup, Sigma.snd, DFunLike.coe, SequentialSpace.coinduced
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : DeltaGeneratedSpace X
⊢ SequentialSpace X

Tactic:
exact SequentialSpace.iSup fun p ↦ SequentialSpace.coinduced p.2

Premises used: SequentialSpace.iSup
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
inst : DeltaGeneratedSpace X
f : X → Y
⊢ DeltaGeneratedSpace Y

Tactic:
let _ := tX.coinduced f
  ⟨(continuous_to_deltaGenerated.2 continuous_coinduced_rng).coinduced_le⟩

Premises used: Iff.mpr, continuous_to_deltaGenerated, TopologicalSpace.coinduced, DeltaGeneratedSpace.mk, continuous_coinduced_rng, Continuous.coinduced_le
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_3
ι : Sort u_4
t : ι → TopologicalSpace X
h : ∀ (i : ι), DeltaGeneratedSpace X
⊢ DeltaGeneratedSpace X

Tactic:
let _ := ⨆ i, t i
  ⟨iSup_le_iff.2 fun i ↦ (h i).le_deltaGenerated.trans <| deltaGenerated_mono <| le_iSup t i⟩

Premises used: Iff.mpr, iSup, le_iSup, DeltaGeneratedSpace.le_deltaGenerated, DeltaGeneratedSpace.mk, deltaGenerated_mono, iSup_le_iff, LE.le.trans
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : DeltaGeneratedSpace X
h₂ : DeltaGeneratedSpace X
rw : DeltaGeneratedSpace X
⊢ DeltaGeneratedSpace X

Tactic:
rw [sup_eq_iSup]

Premises used: sup_eq_iSup
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : DeltaGeneratedSpace X
h₂ : DeltaGeneratedSpace X
⊢ DeltaGeneratedSpace X

Tactic:
.iSup <| Bool.forall_bool.2 ⟨h₂, h₁⟩

Premises used: Iff.mpr, Bool.forall_bool, And.intro, DeltaGeneratedSpace.iSup
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : DeltaGeneratedSpace X
h₂ : DeltaGeneratedSpace X
⊢ DeltaGeneratedSpace X

Tactic:
exact .iSup <| Bool.forall_bool.2 ⟨h₂, h₁⟩

Premises used: Iff.mpr, Bool.forall_bool, And.intro
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : DeltaGeneratedSpace X
f : X → Y
h : IsQuotientMap f
⊢ DeltaGeneratedSpace Y

Tactic:
h.isCoinducing.eq_coinduced ▸ DeltaGeneratedSpace.coinduced f

Premises used: Eq.rec, Topology.IsCoinducing.eq_coinduced, DeltaGeneratedSpace.coinduced, Topology.IsQuotientMap.isCoinducing, Eq.symm
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : DeltaGeneratedSpace X
r : X → X → Prop
⊢ DeltaGeneratedSpace.{u_1} (Quot r)

Tactic:
isQuotientMap_quot_mk.deltaGeneratedSpace

Premises used: Topology.IsQuotientMap.deltaGeneratedSpace, isQuotientMap_quot_mk
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : DeltaGeneratedSpace X
s : Setoid X
⊢ DeltaGeneratedSpace.{u_1} (Quotient s)

Tactic:
isQuotientMap_quotient_mk'.deltaGeneratedSpace

Premises used: isQuotientMap_quotient_mk', Topology.IsQuotientMap.deltaGeneratedSpace
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : DeltaGeneratedSpace X
inst_1 : DeltaGeneratedSpace Y
⊢ DeltaGeneratedSpace (X ⊕ Y)

Tactic:
DeltaGeneratedSpace.sup (.coinduced Sum.inl) (.coinduced Sum.inr)

Premises used: setOf, Sum.inl, DeltaGeneratedSpace.sup, DeltaGeneratedSpace.coinduced, Sum.inr
-- Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace
Goal:
X_1 : Type u_1
Y : Type u_2
tX : TopologicalSpace X_1
tY : TopologicalSpace Y
ι : Type u_3
X : ι → Type u_4
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), DeltaGeneratedSpace.{u_4} (X i)
⊢ DeltaGeneratedSpace ((i : ι) × X i)

Tactic:
.iSup fun _ ↦ .coinduced _

Premises used: DeltaGeneratedSpace.coinduced, Sigma.mk, DeltaGeneratedSpace.iSup
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
f : Filter X
inst_1 : CountableInterFilter f
hf : ∀ x ∈ s, sᶜ ∈ 𝓝 x ⊓ f
contrapose! : ∀ (hf : sᶜ ∉ f), ∃ x ∈ s, sᶜ ∉ 𝓝 x ⊓ f
⊢ sᶜ ∈ f

Tactic:
contrapose! hf
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
f : Filter X
inst_1 : CountableInterFilter f
hf : sᶜ ∉ f
simp : ∀ (hf : (f ⊓ 𝓟 s).NeBot), ∃ x ∈ s, (𝓝 x ⊓ (f ⊓ 𝓟 s)).NeBot
⊢ ∃ x ∈ s, sᶜ ∉ 𝓝 x ⊓ f

Tactic:
simp only [notMem_iff_inf_principal_compl, compl_compl, inf_assoc] at hf ⊢

Premises used: compl_compl, Filter.notMem_iff_inf_principal_compl, inf_assoc
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
f : Filter X
inst_1 : CountableInterFilter f
hf : (f ⊓ 𝓟 s).NeBot
⊢ ∃ x ∈ s, (𝓝 x ⊓ (f ⊓ 𝓟 s)).NeBot

Tactic:
hs inf_le_right

Premises used: inf_le_right, ClusterPt
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
f : Filter X
inst_1 : CountableInterFilter f
hf : (f ⊓ 𝓟 s).NeBot
⊢ ∃ x ∈ s, (𝓝 x ⊓ (f ⊓ 𝓟 s)).NeBot

Tactic:
exact hs inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
f : Filter X
inst_1 : CountableInterFilter f
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
⊢ sᶜ ∈ f

Tactic:
hs.compl_mem_sets fun x hx ↦ ?_

Premises used: IsLindelof.compl_mem_sets
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
f : Filter X
inst_1 : CountableInterFilter f
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
refine : ∀ (x : X) (hx : x ∈ s), sᶜ ∈ 𝓝 x ⊓ f
⊢ sᶜ ∈ f

Tactic:
refine hs.compl_mem_sets fun x hx ↦ ?_

Premises used: IsLindelof.compl_mem_sets
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
f : Filter X
inst_1 : CountableInterFilter f
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x : X
hx : x ∈ s
rw : ∃ i ∈ 𝓝 x ⊓ 𝓟 s, (id i)ᶜ ∈ f
⊢ sᶜ ∈ 𝓝 x ⊓ f

Tactic:
rw [← disjoint_principal_right, disjoint_right_comm, (basis_sets _).disjoint_iff_left]

Premises used: disjoint_right_comm, Filter.basis_sets, Filter.HasBasis.disjoint_iff_left, Filter.disjoint_principal_right
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
f : Filter X
inst_1 : CountableInterFilter f
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x : X
hx : x ∈ s
⊢ ∃ i ∈ 𝓝 x ⊓ 𝓟 s, (id i)ᶜ ∈ f

Tactic:
hf x hx

Premises used: Set.Mem, setOf
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
f : Filter X
inst_1 : CountableInterFilter f
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x : X
hx : x ∈ s
⊢ ∃ i ∈ 𝓝 x ⊓ 𝓟 s, (id i)ᶜ ∈ f

Tactic:
exact hf x hx
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
p : Set X → Prop
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hcountable_union : ∀ (S : Set (Set X)), S.Countable → (∀ s ∈ S, p s) → p (⋃₀ S)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
let : p s
⊢ p s

Tactic:
let f : Filter X := ofCountableUnion {t | p t} hcountable_union (fun t ht _ hsub ↦ hmono hsub ht)
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
p : Set X → Prop
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hcountable_union : ∀ (S : Set (Set X)), S.Countable → (∀ s ∈ S, p s) → p (⋃₀ S)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
f : Filter X := ofCountableUnion {t : Set X | p t} hcountable_union ⋯
⊢ ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f

Tactic:
simpa [f] using hnhds
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
p : Set X → Prop
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hcountable_union : ∀ (S : Set (Set X)), S.Countable → (∀ s ∈ S, p s) → p (⋃₀ S)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
f : Filter X := ofCountableUnion {t : Set X | p t} hcountable_union ⋯
⊢ sᶜ ∈ f

Tactic:
have : sᶜ ∈ f := hs.compl_mem_sets_of_nhdsWithin (by simpa [f] using hnhds)
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsLindelof s
p : Set X → Prop
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hcountable_union : ∀ (S : Set (Set X)), S.Countable → (∀ s ∈ S, p s) → p (⋃₀ S)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
f : Filter X := ofCountableUnion {t : Set X | p t} hcountable_union ⋯
this : sᶜ ∈ f
rwa rwa₁ rwa₂ rwa₃ : p sᶜᶜ
⊢ p s

Tactic:
rwa [← compl_compl s]

Premises used: compl_compl
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsClosed[inst] t
f : Filter X
hnf : f.NeBot
_ : ∀ [CountableInterFilter f], f ≤ 𝓟 (s ∩ t) → ∃ x ∈ s ∩ t, ClusterPt x f
⊢ ∀ [CountableInterFilter f], f ≤ 𝓟 (s ∩ t) → ∃ x ∈ s ∩ t, ClusterPt x f

Tactic:
_
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsClosed[inst] t
f : Filter X
hnf : f.NeBot
inst_1 : CountableInterFilter f
hstf : f ≤ 𝓟 (s ∩ t)
⊢ f ≤ 𝓟 s ∧ f ≤ 𝓟 t

Tactic:
rw [← inf_principal, le_inf_iff] at hstf

Premises used: Filter.inf_principal, le_inf_iff
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsClosed[inst] t
f : Filter X
hnf : f.NeBot
inst_1 : CountableInterFilter f
hstf : f ≤ 𝓟 s ∧ f ≤ 𝓟 t
⊢ ∃ x ∈ s, ClusterPt x f

Tactic:
hs hstf.1

Premises used: And.left
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsClosed[inst] t
f : Filter X
hnf : f.NeBot
inst_1 : CountableInterFilter f
hstf : f ≤ 𝓟 s ∧ f ≤ 𝓟 t
obtain : ∀ (x : X) (hsx : x ∈ s) (hx : ClusterPt x f), ∃ x ∈ s ∩ t, ClusterPt x f
⊢ ∃ x ∈ s ∩ t, ClusterPt x f

Tactic:
obtain ⟨x, hsx, hx⟩ : ∃ x ∈ s, ClusterPt x f := hs hstf.1

Premises used: And.left
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsClosed[inst] t
f : Filter X
hnf : f.NeBot
inst_1 : CountableInterFilter f
hstf : f ≤ 𝓟 s ∧ f ≤ 𝓟 t
x : X
hsx : x ∈ s
hx : ClusterPt x f
⊢ x ∈ t

Tactic:
have hxt : x ∈ t := ht.mem_of_nhdsWithin_neBot <| hx.mono hstf.2
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsClosed[inst] t
f : Filter X
hnf : f.NeBot
inst_1 : CountableInterFilter f
hstf : f ≤ 𝓟 s ∧ f ≤ 𝓟 t
x : X
hsx : x ∈ s
hx : ClusterPt x f
hxt : x ∈ t
⊢ ∃ x ∈ s ∩ t, ClusterPt x f

Tactic:
⟨x, ⟨hsx, hxt⟩, hx⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsClosed[inst] t
f : Filter X
hnf : f.NeBot
inst_1 : CountableInterFilter f
hstf : f ≤ 𝓟 s ∧ f ≤ 𝓟 t
x : X
hsx : x ∈ s
hx : ClusterPt x f
hxt : x ∈ t
⊢ ∃ x ∈ s ∩ t, ClusterPt x f

Tactic:
exact ⟨x, ⟨hsx, hxt⟩, hx⟩
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
ht : IsLindelof t
hs : IsClosed[inst] s
⊢ IsLindelof (s ∩ t)

Tactic:
inter_comm t s ▸ ht.inter_right hs

Premises used: Eq.rec, Set.inter_comm, IsLindelof.inter_right
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsOpen[inst] t
⊢ IsLindelof (s \ t)

Tactic:
hs.inter_right (isClosed_compl_iff.mpr ht)

Premises used: Iff.mpr, Set.Mem, Set.diff, setOf, IsLindelof.inter_right, Not, isClosed_compl_iff