mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
p : Z.TotalSpace
x✝ : p ∈ (Z.localTrivAsPartialEquiv i).source
⊢ (↑{ toPartialEquiv := Z.localTrivAsPartialEquiv i, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯,
            open_source := ⋯, open_target := ⋯ }
        p).1 =
    Z.proj p

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
e✝ : Pretrivialization F proj
x : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
e : Pretrivialization F fun z ↦ proj ↑z
inst✝ : Nonempty (Z → F)
x✝ : Z
⊢ x✝ ∈ Subtype.val '' e.source →
    (if h : proj x✝ ∈ s then ↑e ⟨x✝, h⟩ else (proj x✝, Classical.arbitrary (Z → F) x✝)) ∈ e.target

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
e✝ : Pretrivialization F proj
x✝ : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
e : Pretrivialization F fun z ↦ proj ↑z
inst✝ : Nonempty (Z → F)
x : B × F
hx : x ∈ e.target
⊢ ↑(e.invFun x) ∈ Subtype.val '' e.source

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
e✝ : Pretrivialization F proj
x : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
e : Pretrivialization F fun z ↦ proj ↑z
inst✝ : Nonempty (Z → F)
x✝ : Z
⊢ x✝ ∈ Subtype.val '' e.source →
    ↑(e.invFun (if h : proj x✝ ∈ s then ↑e ⟨x✝, h⟩ else (proj x✝, Classical.arbitrary (Z → F) x✝))) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
e✝ : Pretrivialization F proj
x : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
e : Pretrivialization F fun z ↦ proj ↑z
inst✝ : Nonempty (Z → F)
⊢ Subtype.val '' e.source = proj ⁻¹' e.baseSet

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
⊢ Continuous[inst✝¹, _]
    (have this := fun x ↦ { proj := x, snd := v };
    this)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
e✝ : Pretrivialization F proj
x : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
e : Pretrivialization F fun z ↦ proj ↑z
inst✝ : Nonempty (Z → F)
⊢ e.target = e.baseSet ×ˢ univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
e✝ : Pretrivialization F proj
x : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
e : Pretrivialization F fun z ↦ proj ↑z
inst✝ : Nonempty (Z → F)
x✝ : Z
⊢ x✝ ∈ Subtype.val '' e.source →
    (if h : proj x✝ ∈ s then ↑e ⟨x✝, h⟩ else (proj x✝, Classical.arbitrary (Z → F) x✝)).1 = proj x✝

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
p : Z.TotalSpace
⊢ ↑(Z.localTrivAt p.proj) p = (p.proj, p.snd)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj✝ : Z → B
e✝ : Pretrivialization F proj✝
x✝ : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
hs : IsOpen[inst✝²] s
proj : Z → ↑s
e : Pretrivialization F proj
inst✝ : Nonempty (B → F → Z)
x : B × F
⊢ Z

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
b : B
⊢ b ∈ (Z.localTrivAt b).baseSet

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
b : B
a : F
⊢ { proj := b, snd := a } ∈ (Z.localTrivAt b).source

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj✝ : Z → B
e✝ : Pretrivialization F proj✝
x : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
hs : IsOpen[inst✝²] s
proj : Z → ↑s
e : Pretrivialization F proj
inst✝ : Nonempty (B → F → Z)
z : Z
hz : z ∈ e.source
⊢ (↑(↑e z).1, (↑e z).2) ∈ Prod.map Subtype.val id '' e.target

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj✝ : Z → B
e✝ : Pretrivialization F proj✝
x : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
hs : IsOpen[inst✝²] s
proj : Z → ↑s
e : Pretrivialization F proj
inst✝ : Nonempty (B → F → Z)
x✝ : B × F
⊢ x✝ ∈ Prod.map Subtype.val id '' e.target →
    (if h : x✝.1 ∈ s then e.invFun (⟨x✝.1, h⟩, x✝.2) else Classical.arbitrary (B → F → Z) x✝.1 x✝.2) ∈ e.source

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj✝ : Z → B
e✝ : Pretrivialization F proj✝
x : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
hs : IsOpen[inst✝²] s
proj : Z → ↑s
e : Pretrivialization F proj
inst✝ : Nonempty (B → F → Z)
z : Z
hz : z ∈ e.source
⊢ (if h : (↑(↑e z).1, (↑e z).2).1 ∈ s then e.invFun (⟨(↑(↑e z).1, (↑e z).2).1, h⟩, (↑(↑e z).1, (↑e z).2).2)
    else Classical.arbitrary (B → F → Z) (↑(↑e z).1, (↑e z).2).1 (↑(↑e z).1, (↑e z).2).2) =
    z

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b✝ : B
a : F
b : B
x : Z.Fiber b
⊢ 𝓝 x = comap (TotalSpace.mk b) (𝓝 { proj := b, snd := x })

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
⊢ ContinuousOn (↑e.symm) e.target

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
⊢ IsOpen[a.totalSpaceTopology] e.source

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj✝ : Z → B
e✝ : Pretrivialization F proj✝
x : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
hs : IsOpen[inst✝²] s
proj : Z → ↑s
e : Pretrivialization F proj
inst✝ : Nonempty (B → F → Z)
x✝ : B × F
⊢ x✝ ∈ Prod.map Subtype.val id '' e.target →
    (↑(↑e (if h : x✝.1 ∈ s then e.invFun (⟨x✝.1, h⟩, x✝.2) else Classical.arbitrary (B → F → Z) x✝.1 x✝.2)).1,
        (↑e (if h : x✝.1 ∈ s then e.invFun (⟨x✝.1, h⟩, x✝.2) else Classical.arbitrary (B → F → Z) x✝.1 x✝.2)).2) =
      x✝

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj✝ : Z → B
e✝ : Pretrivialization F proj✝
x : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
hs : IsOpen[inst✝²] s
proj : Z → ↑s
e : Pretrivialization F proj
inst✝ : Nonempty (B → F → Z)
⊢ e.source = Subtype.val ∘ proj ⁻¹' Subtype.val '' e.baseSet

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj✝ : Z → B
e✝ : Pretrivialization F proj✝
x : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
hs : IsOpen[inst✝²] s
proj : Z → ↑s
e : Pretrivialization F proj
inst✝ : Nonempty (B → F → Z)
⊢ Prod.map Subtype.val id '' e.target = (Subtype.val '' e.baseSet) ×ˢ univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj✝ : Z → B
e✝ : Pretrivialization F proj✝
x : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
hs : IsOpen[inst✝²] s
proj : Z → ↑s
e : Pretrivialization F proj
inst✝ : Nonempty (B → F → Z)
x✝ : Z
h : x✝ ∈ e.source
⊢ (↑(↑e x✝).1, (↑e x✝).2).1 = (Subtype.val ∘ proj) x✝

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e e' : Trivialization F proj
h₁ : e.toOpenPartialHomeomorph = e'.toOpenPartialHomeomorph
h₂ : e.baseSet = e'.baseSet
⊢ e = e'

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e e' : Trivialization F proj
h : (fun e ↦ e.toPretrivialization) e = (fun e ↦ e.toPretrivialization) e'
⊢ e = e'

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e : Trivialization F proj
x : Z
⊢ x ∈ e.source ↔ proj x ∈ e.baseSet

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e : Trivialization F proj
x : Z
⊢ x ∈ e.source ↔ proj x ∈ e.baseSet

Tactic:
by rw [e.source_eq, mem_preimage]

Goal state after:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
⊢ IsOpen[instTopologicalSpaceProd] (e'.target ∩ ↑e'.symm ⁻¹' e.source)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e : Trivialization F proj
x : Z
ex : x ∈ e.source
⊢ map proj (𝓝 x) = 𝓝 (proj x)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
x✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
s : Set (B × F)
hs : IsOpen[instTopologicalSpaceProd] s
⊢ ↑e.toPartialEquiv ⁻¹' s ∩ e.source = ↑e ⁻¹' s ∩ e.source ∩ e.source

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
x✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
s : Set (B × F)
hs : IsOpen[instTopologicalSpaceProd] s
e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
u : Set (B × F)
hu1 : IsOpen[instTopologicalSpaceProd] u
hu2 : ↑e ∘ ↑e'.symm ⁻¹' s ∩ (e'.target ∩ ↑e'.symm ⁻¹' e.source) = u ∩ (e'.target ∩ ↑e'.symm ⁻¹' e.source)
hu3 :
  (fun x ↦ ↑x) ⁻¹' ↑e ∘ ↑e'.symm ⁻¹' s ∩ (fun x ↦ ↑x) ⁻¹' ↑e'.symm ⁻¹' e.source =
    (fun x ↦ ↑x) ⁻¹' u ∩ (fun x ↦ ↑x) ⁻¹' ↑e'.symm ⁻¹' e.source
⊢ Subtype.val ⁻¹' (u ∩ e'.target ∩ ↑e'.symm ⁻¹' e.source) = e'.setSymm ⁻¹' (↑e ⁻¹' s ∩ e.source)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e : Trivialization F proj
α : Type u_5
l : Filter α
f : α → Z
z : Z
hz : z ∈ e.source
⊢ Tendsto f l (𝓝 z) ↔ Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun x ↦ (↑e (f x)).2) l (𝓝 (↑e z).2)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
x✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
⊢ ContinuousOn (↑e.toPartialEquiv) e.source

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e : Trivialization F proj
z : Z
hz : z ∈ e.source
⊢ 𝓝 z = comap proj (𝓝 (proj z)) ⊓ comap (Prod.snd ∘ ↑e) (𝓝 (↑e z).2)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
b : B
x : E b
⊢ { proj := b, snd := x } ∈ (a.pretrivializationAt b).source

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
b : B
hb : b ∈ e.baseSet
p : F
⊢ ↑e.symm (b, p) ∈ proj ⁻¹' {b}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e : Trivialization F proj
b : B
v : F
hb : b ∈ e.baseSet
⊢ ContinuousAt (fun x ↦ (x, v)) b

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
Z' : Type u_5
inst✝ : TopologicalSpace Z'
h : Z' ≃ₜ Z
⊢ (h.transOpenPartialHomeomorph e.toOpenPartialHomeomorph).source = proj ∘ ⇑h ⁻¹' e.baseSet

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
b : B
⊢ Continuous[inst✝ b, a.totalSpaceTopology] (TotalSpace.mk b)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
Z' : Type u_5
inst✝ : TopologicalSpace Z'
h : Z' ≃ₜ Z
⊢ (h.transOpenPartialHomeomorph e.toOpenPartialHomeomorph).target = e.baseSet ×ˢ univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
Z' : Type u_5
inst✝ : TopologicalSpace Z'
h : Z' ≃ₜ Z
p : Z'
hp : p ∈ (h.transOpenPartialHomeomorph e.toOpenPartialHomeomorph).source
⊢ h p ∈ e.source

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
Z' : Type u_5
inst✝ : TopologicalSpace Z'
h : Z' ≃ₜ Z
p : Z'
hp : p ∈ (h.transOpenPartialHomeomorph e.toOpenPartialHomeomorph).source
⊢ (↑(h.transOpenPartialHomeomorph e.toOpenPartialHomeomorph) p).1 = (proj ∘ ⇑h) p

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
b : B
h : IsInducing (↑(a.pretrivializationAt b) ∘ TotalSpace.mk b)
⊢ IsInducing (TotalSpace.mk b)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
B' : Type u_5
inst✝ : TopologicalSpace B'
h : B ≃ₜ B'
⊢ (e.transHomeomorph (h.prodCongr (Homeomorph.refl F))).source = ⇑h ∘ proj ⁻¹' ⇑h.symm ⁻¹' e.baseSet

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
⊢ Continuous[a.totalSpaceTopology, inst✝²] TotalSpace.proj

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
B' : Type u_5
inst✝ : TopologicalSpace B'
h : B ≃ₜ B'
⊢ (e.transHomeomorph (h.prodCongr (Homeomorph.refl F))).target = (⇑h.symm ⁻¹' e.baseSet) ×ˢ univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
B' : Type u_5
inst✝ : TopologicalSpace B'
h : B ≃ₜ B'
p : Z
hp : p ∈ (e.transHomeomorph (h.prodCongr (Homeomorph.refl F))).source
⊢ (↑(e.transHomeomorph (h.prodCongr (Homeomorph.refl F))) p).1 = (⇑h ∘ proj) p

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
X : Type u_5
inst✝ : TopologicalSpace X
f : Z → X
z : Z
e : Trivialization F proj
he : proj z ∈ e.baseSet
hf : ContinuousAt (f ∘ ↑e.symm) (↑e z)
⊢ z ∈ e.symm.target

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
X : Type u_5
inst✝ : TopologicalSpace X
f : Z → X
z : Z
e : Trivialization F proj
he : proj z ∈ e.baseSet
hf : ContinuousAt (f ∘ ↑e.symm) (↑e z)
⊢ ContinuousAt f z

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
X : Type u_5
inst✝ : TopologicalSpace X
f : X → Z
x : X
e : Trivialization F proj
hf_proj : ContinuousAt (proj ∘ f) x
he : proj (f x) ∈ e.baseSet
hf : ContinuousAt (↑e ∘ f) x
⊢ ContinuousAt f x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalSpace (TotalSpace F E)
inst✝ : ∀ (x : B), Nonempty (E x)
e : Trivialization F TotalSpace.proj
⊢ ∀ z ∈ e.baseSet ×ˢ univ, { proj := z.1, snd := e.symm z.1 z.2 } = ↑e.symm z

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalSpace (TotalSpace F E)
inst✝ : ∀ (x : B), Nonempty (E x)
e : Trivialization F TotalSpace.proj
⊢ ContinuousOn (fun z ↦ TotalSpace.mk' F z.1 (e.symm z.1 z.2)) (e.baseSet ×ˢ univ)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x : Z
e' : Trivialization F TotalSpace.proj
b : B
y : E b
F' : Type u_5
inst✝ : TopologicalSpace F'
e : Trivialization F proj
h : F ≃ₜ F'
⊢ (e.transHomeomorph ((Homeomorph.refl B).prodCongr h)).target = e.baseSet ×ˢ univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ (b, e₁.coordChange e₂ b x) = ↑e₂ (↑e₁.symm (b, x))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
X : Type u_6
inst✝ : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen[inst✝³] s
hf : ∀ b ∈ s, ContinuousOn (f ∘ ↑(a.pretrivializationAt b).symm) ((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ univ)
⊢ ContinuousOn f (TotalSpace.proj ⁻¹' s)

Tactic:
by

Goal state after: