awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
D_comp : CompactSpace.{u} (↑D : Type u)
X₁ : (↑D : Type u) → A := Prod.fst ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set (↑D : Type u)
left : CompactSpace.{u} (↑E : Type u)
E_onto : X₁ '' E = univ
E_min :
  ∀ (E₀ : Set (↑E : Type u)), E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁ '' E₀ ≠ univ
ρ : (↑E : Type u) → A := E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
ρ' : (↑E : Type u) ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
X₂ : (↑D : Type u) → B := Prod.snd ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₂_cont : Continuous X₂
x : (↑E : Type u)
⊢ (f ∘ E.restrict (π := fun (a : (↑D : Type u)) ↦ B) X₂) x = (φ ∘ (⇑ρ' : (a : (↑E : Type u)) → A)) x

Tactic:
x.val.mem.symm

Premises used: Subtype.mem, Set.restrict, Eq.symm, Subtype.val
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
D_comp : CompactSpace.{u} (↑D : Type u)
X₁ : (↑D : Type u) → A := Prod.fst ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set (↑D : Type u)
left : CompactSpace.{u} (↑E : Type u)
E_onto : X₁ '' E = univ
E_min :
  ∀ (E₀ : Set (↑E : Type u)), E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁ '' E₀ ≠ univ
ρ : (↑E : Type u) → A := E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
ρ' : (↑E : Type u) ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
X₂ : (↑D : Type u) → B := Prod.snd ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₂_cont : Continuous X₂
x : (↑E : Type u)
⊢ (f ∘ E.restrict (π := fun (a : (↑D : Type u)) ↦ B) X₂) x = (φ ∘ (⇑ρ' : (a : (↑E : Type u)) → A)) x

Tactic:
exact x.val.mem.symm

Premises used: Subtype.mem, Eq.symm, Subtype.val
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : CompactSpace A
inst_2 : T2Space A
⊢ Projective A ↔ ExtremallyDisconnected A

Tactic:
⟨Projective.extremallyDisconnected, fun _ => ExtremallyDisconnected.projective⟩

Premises used: CompactT2.Projective.extremallyDisconnected, CompactT2.ExtremallyDisconnected.projective, Iff.intro
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
ι : Type u_1
X : ι → Type u_2
inst_1 : (i : ι) → TopologicalSpace (X i)
h₀ : ∀ (i : ι), ExtremallyDisconnected.{u_2} (X i)
open_closure : ∀ (U : Set ((i : ι) × X i)), IsOpen U → IsOpen (closure U)
⊢ ExtremallyDisconnected ((i : ι) × X i)

Tactic:
constructor
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
ι : Type u_1
X : ι → Type u_2
inst_1 : (i : ι) → TopologicalSpace (X i)
h₀ : ∀ (i : ι), ExtremallyDisconnected.{u_2} (X i)
s : Set ((i : ι) × X i)
hs : IsOpen s
open_closure :
  ∀ (hs : ∀ (i : ι), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)) (i : ι),
    IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' closure s)
⊢ IsOpen (closure s)

Tactic:
rw [isOpen_sigma_iff] at hs ⊢

Premises used: isOpen_sigma_iff
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
ι : Type u_1
X : ι → Type u_2
inst_1 : (i : ι) → TopologicalSpace (X i)
h₀ : ∀ (i : ι), ExtremallyDisconnected.{u_2} (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
i : ι
⊢ ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)

Tactic:
rcases h₀ i with ⟨h₀⟩
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
ι : Type u_1
X : ι → Type u_2
inst_1 : (i : ι) → TopologicalSpace (X i)
h₀_1 : ∀ (i : ι), ExtremallyDisconnected.{u_2} (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
h : Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' closure s = closure (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
rw : IsOpen (closure (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s))
⊢ IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' closure s)

Tactic:
rw [h]
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
ι : Type u_1
X : ι → Type u_2
inst_1 : (i : ι) → TopologicalSpace (X i)
h₀_1 : ∀ (i : ι), ExtremallyDisconnected.{u_2} (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
h : Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' closure s = closure (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
⊢ IsOpen (closure (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s))

Tactic:
h₀ _ (hs i)
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
ι : Type u_1
X : ι → Type u_2
inst_1 : (i : ι) → TopologicalSpace (X i)
h₀_1 : ∀ (i : ι), ExtremallyDisconnected.{u_2} (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
h : Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' closure s = closure (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
⊢ IsOpen (closure (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s))

Tactic:
exact h₀ _ (hs i)
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
ι : Type u_1
X : ι → Type u_2
inst_1 : (i : ι) → TopologicalSpace (X i)
h₀_1 : ∀ (i : ι), ExtremallyDisconnected.{u_2} (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
open_closure : Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' closure s = closure (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
⊢ IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' closure s)

Tactic:
suffices h : Sigma.mk i ⁻¹' closure s = closure (Sigma.mk i ⁻¹' s) by
    rw [h]
    exact h₀ _ (hs i)
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
ι : Type u_1
X : ι → Type u_2
inst_1 : (i : ι) → TopologicalSpace (X i)
h₀_1 : ∀ (i : ι), ExtremallyDisconnected.{u_2} (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
open_closure : IsOpenMap (X := X i) (Sigma.mk (β := fun (i : ι) ↦ X i) i)
open_closure₁ : Continuous (X := X i) (Sigma.mk (β := fun (i : ι) ↦ X i) i)
⊢ Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' closure s = closure (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)

Tactic:
apply IsOpenMap.preimage_closure_eq_closure_preimage

Premises used: IsOpenMap.preimage_closure_eq_closure_preimage
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
ι : Type u_1
X : ι → Type u_2
inst_1 : (i : ι) → TopologicalSpace (X i)
h₀_1 : ∀ (i : ι), ExtremallyDisconnected.{u_2} (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
U : Set (X i)
open_closure : IsOpen U → IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i '' U)
⊢ IsOpen U → IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i '' U)

Tactic:
_
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
ι : Type u_1
X : ι → Type u_2
inst_1 : (i : ι) → TopologicalSpace (X i)
h₀_1 : ∀ (i : ι), ExtremallyDisconnected.{u_2} (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
U : Set (X i)
h : IsOpen U
open_closure : ∀ (i_1 : ι), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i_1 ⁻¹' Sigma.mk (β := fun (i : ι) ↦ X i) i '' U)
⊢ IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i '' U)

Tactic:
rw [isOpen_sigma_iff]

Premises used: isOpen_sigma_iff
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
ι : Type u_1
X : ι → Type u_2
inst_1 : (i : ι) → TopologicalSpace (X i)
h₀_1 : ∀ (i : ι), ExtremallyDisconnected.{u_2} (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
U : Set (X i)
h : IsOpen U
j : ι
pos : ∀ (ij : i = j), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) j ⁻¹' Sigma.mk (β := fun (i : ι) ↦ X i) i '' U)
neg : ∀ (ij : ¬i = j), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) j ⁻¹' Sigma.mk (β := fun (i : ι) ↦ X i) i '' U)
⊢ IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) j ⁻¹' Sigma.mk (β := fun (i : ι) ↦ X i) i '' U)

Tactic:
by_cases ij : i = j
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
ι : Type u_1
X : ι → Type u_2
inst_1 : (i : ι) → TopologicalSpace (X i)
h₀_1 : ∀ (i : ι), ExtremallyDisconnected.{u_2} (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
U : Set (X i)
h : IsOpen U
j : ι
ij : i = j
pos : IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' Sigma.mk (β := fun (i : ι) ↦ X i) i '' U)
pos₁ pos₂ pos₃ pos₄ : IsOpen U
⊢ IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) j ⁻¹' Sigma.mk (β := fun (i : ι) ↦ X i) i '' U)

Tactic:
rwa [← ij, sigma_mk_preimage_image_eq_self]

Premises used: sigma_mk_preimage_image_eq_self
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
ι : Type u_1
X : ι → Type u_2
inst_1 : (i : ι) → TopologicalSpace (X i)
h₀_1 : ∀ (i : ι), ExtremallyDisconnected.{u_2} (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
U : Set (X i)
h : IsOpen U
j : ι
ij : ¬i = j
neg : IsOpen.{u_2} (X := X j) ∅
⊢ IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) j ⁻¹' Sigma.mk (β := fun (i : ι) ↦ X i) i '' U)

Tactic:
rw [sigma_mk_preimage_image' ij]

Premises used: sigma_mk_preimage_image'
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
ι : Type u_1
X : ι → Type u_2
inst_1 : (i : ι) → TopologicalSpace (X i)
h₀_1 : ∀ (i : ι), ExtremallyDisconnected.{u_2} (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
U : Set (X i)
h : IsOpen U
j : ι
ij : ¬i = j
⊢ IsOpen.{u_2} (X := X j) ∅

Tactic:
isOpen_empty

Premises used: isOpen_empty
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
ι : Type u_1
X : ι → Type u_2
inst_1 : (i : ι) → TopologicalSpace (X i)
h₀_1 : ∀ (i : ι), ExtremallyDisconnected.{u_2} (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
U : Set (X i)
h : IsOpen U
j : ι
ij : ¬i = j
⊢ IsOpen.{u_2} (X := X j) ∅

Tactic:
exact isOpen_empty

Premises used: isOpen_empty
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
ι : Type u_1
X : ι → Type u_2
inst_1 : (i : ι) → TopologicalSpace (X i)
h₀_1 : ∀ (i : ι), ExtremallyDisconnected.{u_2} (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
⊢ Continuous (X := X i) (Sigma.mk (β := fun (i : ι) ↦ X i) i)

Tactic:
fun_prop
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
h : PreirreducibleSpace X
U : Set X
hU : IsOpen U
pos : ∀ (Un : U = ∅), IsOpen (closure U)
neg : ∀ (Un : U.Nonempty), IsOpen (closure U)
⊢ IsOpen (closure U)

Tactic:
by_cases! Un : U = ∅
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
h : PreirreducibleSpace X
U : Set X
hU : IsOpen U
Un : U = ∅
⊢ IsOpen (closure U)

Tactic:
simp_all
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
h : PreirreducibleSpace X
U : Set X
hU : IsOpen U
Un : U.Nonempty
⊢ IsOpen (closure U)

Tactic:
((preirreducibleSpace_iff_open_dense X).mp h hU Un).closure_eq ▸ isOpen_univ

Premises used: preirreducibleSpace_iff_open_dense, Eq.rec, Dense.closure_eq, isOpen_univ, Iff.mp, Eq.symm
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
h : PreirreducibleSpace X
U : Set X
hU : IsOpen U
Un : U.Nonempty
⊢ IsOpen (closure U)

Tactic:
exact ((preirreducibleSpace_iff_open_dense X).mp h hU Un).closure_eq ▸ isOpen_univ
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
h : ExtremallyDisconnected X
h' : PreconnectedSpace X
apply : ∀ (s : Set X) (hs : IsOpen s) (sn : s.Nonempty), Dense s
⊢ PreirreducibleSpace X

Tactic:
apply (preirreducibleSpace_iff_open_dense X).mpr (fun s hs sn ↦ ?_)

Premises used: Iff.mpr, preirreducibleSpace_iff_open_dense
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
h : ExtremallyDisconnected X
h' : PreconnectedSpace X
s : Set X
hs : IsOpen s
sn : s.Nonempty
apply : closure s = univ
⊢ Dense s

Tactic:
apply dense_iff_closure_eq.mpr

Premises used: Iff.mpr, dense_iff_closure_eq
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
h : ExtremallyDisconnected X
h' : PreconnectedSpace X
s : Set X
hs : IsOpen s
sn : s.Nonempty
inl : closure s = ∅ → closure s = univ
inr : closure s = univ → closure s = univ
⊢ closure s = univ

Tactic:
cases preconnectedSpace_iff_clopen.mp h' (closure s) ⟨isClosed_closure, h.open_closure s hs⟩

Premises used: ExtremallyDisconnected.open_closure, closure, And.intro, Iff.mp, isClosed_closure, preconnectedSpace_iff_clopen
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
h : ExtremallyDisconnected X
h' : PreconnectedSpace X
s : Set X
hs : IsOpen s
sn : s.Nonempty
h_1 : closure s = ∅
⊢ closure s = univ

Tactic:
simp_all
-- Module: Mathlib.Topology.ExtremallyDisconnected
Goal:
X : Type u
inst : TopologicalSpace X
h : ExtremallyDisconnected X
h' : PreconnectedSpace X
s : Set X
hs : IsOpen s
sn : s.Nonempty
h_1 : closure s = univ
⊢ closure s = univ

Tactic:
assumption
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : FiberBundle F E
b : B
⊢ IsInducing (X := E b) (Y := TotalSpace F E) (TotalSpace.mk (E := E) b)

Tactic:
totalSpaceMk_isInducing' b

Premises used: FiberBundle.totalSpaceMk_isInducing'
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : FiberBundle F E
b : B
⊢ b ∈ Trivialization.baseSet (trivializationAt F E b)

Tactic:
mem_baseSet_trivializationAt' b

Premises used: FiberBundle.mem_baseSet_trivializationAt', Set.Mem
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : FiberBundle F E
b : B
⊢ Membership.mem (γ := Set (Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))))
    (trivializationAtlas F E) (trivializationAt F E b)

Tactic:
trivialization_mem_atlas' b

Premises used: FiberBundle.trivialization_mem_atlas', Set.Mem
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : FiberBundle F E
x : TotalSpace F E
⊢ map (TotalSpace.proj (E := E)) (𝓝 x) = 𝓝 (x.proj (E := E))

Tactic:
(trivializationAt F E x.proj).map_proj_nhds <|
    (trivializationAt F E x.proj).mem_source.2 <| mem_baseSet_trivializationAt F E x.proj

Premises used: Iff.mpr, Bundle.TotalSpace.proj, FiberBundle.trivializationAt, Bundle.Trivialization.mem_source, FiberBundle.mem_baseSet_trivializationAt, Bundle.Trivialization.map_proj_nhds
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : FiberBundle F E
⊢ Continuous[inst_2, inst] (TotalSpace.proj (E := E))

Tactic:
continuous_iff_continuousAt.2 fun x => (map_proj_nhds F x).le

Premises used: Iff.mpr, Eq.le, FiberBundle.map_proj_nhds, continuous_iff_continuousAt
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : FiberBundle F E
⊢ IsOpenMap (X := TotalSpace F E) (TotalSpace.proj (E := E))

Tactic:
IsOpenMap.of_nhds_le fun x => (map_proj_nhds F x).ge

Premises used: Eq.ge, FiberBundle.map_proj_nhds, IsOpenMap.of_nhds_le
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : FiberBundle F E
inst_5 : Nonempty F
⊢ Function.Surjective (α := TotalSpace F E) (TotalSpace.proj (E := E))

Tactic:
fun b =>
  let ⟨p, _, hpb⟩ :=
    (trivializationAt F E b).proj_surjOn_baseSet (mem_baseSet_trivializationAt F E b)
  ⟨p, hpb⟩

Premises used: _private.0.FiberBundle.surjective_proj.match_1, Exists, Bundle.TotalSpace.proj, FiberBundle.trivializationAt, Exists.intro, Bundle.Trivialization.proj_surjOn_baseSet, FiberBundle.mem_baseSet_trivializationAt, Eq, Function.Surjective
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : FiberBundle F E
inst_5 : Nonempty F
⊢ IsQuotientMap (X := TotalSpace F E) (TotalSpace.proj (E := E))

Tactic:
(isOpenMap_proj F E).isQuotientMap (continuous_proj F E) (surjective_proj F E)

Premises used: IsOpenMap.isQuotientMap, FiberBundle.isOpenMap_proj, FiberBundle.continuous_proj, FiberBundle.surjective_proj
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : FiberBundle F E
x : B
⊢ Continuous[inst_3 x, inst_2] (TotalSpace.mk (E := E) x)

Tactic:
(totalSpaceMk_isInducing F E x).continuous

Premises used: FiberBundle.totalSpaceMk_isInducing, Topology.IsInducing.continuous
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : FiberBundle F E
x : B
⊢ IsEmbedding (X := E x) (Y := TotalSpace F E) (TotalSpace.mk (E := E) x)

Tactic:
⟨totalSpaceMk_isInducing F E x, TotalSpace.mk_injective x⟩

Premises used: Bundle.TotalSpace.mk_injective, FiberBundle.totalSpaceMk_isInducing, Topology.IsEmbedding.mk
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : FiberBundle F E
inst_5 : T1Space B
x : B
rw : IsClosed[inst_2] (TotalSpace.proj (E := E) ⁻¹' {x})
⊢ IsClosed[inst_2] (range (TotalSpace.mk (E := E) x))

Tactic:
rw [TotalSpace.range_mk]

Premises used: Bundle.TotalSpace.range_mk
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : FiberBundle F E
inst_5 : T1Space B
x : B
⊢ IsClosed[inst_2] (TotalSpace.proj (E := E) ⁻¹' {x})

Tactic:
isClosed_singleton.preimage <| continuous_proj F E

Premises used: FiberBundle.continuous_proj, IsClosed.preimage, isClosed_singleton
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : FiberBundle F E
inst_5 : T1Space B
x : B
⊢ IsClosed[inst_2] (TotalSpace.proj (E := E) ⁻¹' {x})

Tactic:
exact isClosed_singleton.preimage <| continuous_proj F E

Premises used: FiberBundle.continuous_proj, IsClosed.preimage, isClosed_singleton
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : FiberBundle F E
inst_5 : T0Space F
b : B
⊢ T0Space.{u_5} (E b)

Tactic:
FiberBundle.homeomorphAt F E b |>.symm.t0Space

Premises used: Homeomorph.t0Space, FiberBundle.homeomorphAt, Homeomorph.symm
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : FiberBundle F E
inst_5 : T1Space F
b : B
⊢ T1Space.{u_5} (E b)

Tactic:
FiberBundle.homeomorphAt F E b |>.symm.t1Space

Premises used: FiberBundle.homeomorphAt, Homeomorph.symm, Homeomorph.t1Space
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : FiberBundle F E
inst_5 : T2Space F
b : B
⊢ T2Space.{u_5} (E b)

Tactic:
FiberBundle.homeomorphAt F E b |>.symm.t2Space

Premises used: FiberBundle.homeomorphAt, Homeomorph.symm, Homeomorph.t2Space
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : FiberBundle F E
inst_5 : T3Space F
b : B
⊢ T3Space.{u_5} (E b)

Tactic:
FiberBundle.homeomorphAt F E b |>.symm.t3Space

Premises used: FiberBundle.homeomorphAt, Homeomorph.symm, Homeomorph.t3Space
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : FiberBundle F E
x : TotalSpace F E
⊢ x ∈
    (OpenPartialHomeomorph.toPartialEquiv
        (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))))).source

Tactic:
(Trivialization.mem_source _).mpr <| mem_baseSet_trivializationAt F E x.proj

Premises used: Iff.mpr, Bundle.TotalSpace.proj, Bundle.Trivialization.mem_source, FiberBundle.mem_baseSet_trivializationAt