mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : ∀ (x : B), Nonempty (E x)
e : Pretrivialization F TotalSpace.proj
b : B
hb : b ∉ e.baseSet
x✝ : F
⊢ e.symm b x✝ = Classical.arbitrary (E b)

Tactic:
;

Goal state after:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : ∀ (x : B), Nonempty (E x)
e : Pretrivialization F TotalSpace.proj
b : B
hb : b ∉ e.baseSet
x✝ : F
⊢ e.symm b x✝ = Classical.arbitrary (E b)
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
e : Pretrivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
x : ↑s × F
hx : (↑x.1, x.2) ∈ e.target
⊢ ⟨e.invFun (↑x.1, x.2), ⋯⟩ ∈ Subtype.val ⁻¹' e.source

Tactic:
;

Goal state after:
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
e : Pretrivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
x : ↑s × F
hx : (↑x.1, x.2) ∈ e.target
⊢ ⟨e.invFun (↑x.1, x.2), ⋯⟩ ∈ Subtype.val ⁻¹' e.source
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
e : Pretrivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
z : ↑(proj ⁻¹' s)
hz : z ∈ Subtype.val ⁻¹' e.source
⊢ (if h : (proj ↑z, (↑e ↑z).2) ∈ e.target then ⟨e.invFun (proj ↑z, (↑e ↑z).2), ⋯⟩
    else Classical.arbitrary (↑s → F → ↑(proj ⁻¹' s)) ⟨proj ↑z, ⋯⟩ (↑e ↑z).2) =
    z

Tactic:
;

Goal state after:
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
e : Pretrivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
z : ↑(proj ⁻¹' s)
hz : z ∈ Subtype.val ⁻¹' e.source
⊢ (if h : (proj ↑z, (↑e ↑z).2) ∈ e.target then ⟨e.invFun (proj ↑z, (↑e ↑z).2), ⋯⟩
    else Classical.arbitrary (↑s → F → ↑(proj ⁻¹' s)) ⟨proj ↑z, ⋯⟩ (↑e ↑z).2) =
    z
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
e : Pretrivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
x : ↑s × F
hx : (↑x.1, x.2) ∈ e.target
⊢ (proj
        ↑(if h : (↑x.1, x.2) ∈ e.target then ⟨e.invFun (↑x.1, x.2), ⋯⟩
          else Classical.arbitrary (↑s → F → ↑(proj ⁻¹' s)) x.1 x.2),
      id
        (↑e
            ↑(if h : (↑x.1, x.2) ∈ e.target then ⟨e.invFun (↑x.1, x.2), ⋯⟩
              else Classical.arbitrary (↑s → F → ↑(proj ⁻¹' s)) x.1 x.2)).2) =
    Prod.map Subtype.val id x

Tactic:
;

Goal state after:
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
e : Pretrivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
x : ↑s × F
hx : (↑x.1, x.2) ∈ e.target
⊢ (proj
        ↑(if h : (↑x.1, x.2) ∈ e.target then ⟨e.invFun (↑x.1, x.2), ⋯⟩
          else Classical.arbitrary (↑s → F → ↑(proj ⁻¹' s)) x.1 x.2),
      id
        (↑e
            ↑(if h : (↑x.1, x.2) ∈ e.target then ⟨e.invFun (↑x.1, x.2), ⋯⟩
              else Classical.arbitrary (↑s → F → ↑(proj ⁻¹' s)) x.1 x.2)).2) =
    Prod.map Subtype.val id x
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: case e'_2.e'_3
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
e : Pretrivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
x : ↑s × F
hx : (↑x.1, x.2) ∈ e.target
⊢ (e.toPartialEquiv.1 (e.invFun (↑x.1, x.2))).1 = proj ↑⟨e.invFun (↑x.1, x.2), ⋯⟩

Tactic:
;

Goal state after:
case e'_2.e'_3
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
e : Pretrivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
x : ↑s × F
hx : (↑x.1, x.2) ∈ e.target
⊢ (e.toPartialEquiv.1 (e.invFun (↑x.1, x.2))).1 = proj ↑⟨e.invFun (↑x.1, x.2), ⋯⟩
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)
z : Z
hzp : proj z ∈ s
hze : ⟨z, hzp⟩ ∈ e.source
⊢ ↑(e.invFun
        (if h : proj ↑⟨z, hzp⟩ ∈ s then ↑e ⟨↑⟨z, hzp⟩, h⟩
        else (proj ↑⟨z, hzp⟩, Classical.arbitrary (Z → F) ↑⟨z, hzp⟩))) =
    ↑⟨z, hzp⟩

Tactic:
;

Goal state after:
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)
z : Z
hzp : proj z ∈ s
hze : ⟨z, hzp⟩ ∈ e.source
⊢ ↑(e.invFun
        (if h : proj ↑⟨z, hzp⟩ ∈ s then ↑e ⟨↑⟨z, hzp⟩, h⟩
        else (proj ↑⟨z, hzp⟩, Classical.arbitrary (Z → F) ↑⟨z, hzp⟩))) =
    ↑⟨z, hzp⟩
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)
z : Z
⊢ z ∈ Subtype.val '' e.source ↔ z ∈ proj ⁻¹' e.baseSet

Tactic:
;

Goal state after:
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)
z : Z
⊢ z ∈ Subtype.val '' e.source ↔ z ∈ proj ⁻¹' e.baseSet
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
⊢ x✝ ∈ e.target ↔ x✝ ∈ e.baseSet ×ˢ univ

Tactic:
;

Goal state after:
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
⊢ x✝ ∈ e.target ↔ x✝ ∈ e.baseSet ×ˢ univ
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)
z : Z
hzp : proj z ∈ s
hze : ⟨z, hzp⟩ ∈ e.source
⊢ (if h : proj ↑⟨z, hzp⟩ ∈ s then ↑e ⟨↑⟨z, hzp⟩, h⟩ else (proj ↑⟨z, hzp⟩, Classical.arbitrary (Z → F) ↑⟨z, hzp⟩)).1 =
    proj ↑⟨z, hzp⟩

Tactic:
;

Goal state after:
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)
z : Z
hzp : proj z ∈ s
hze : ⟨z, hzp⟩ ∈ e.source
⊢ (if h : proj ↑⟨z, hzp⟩ ∈ s then ↑e ⟨↑⟨z, hzp⟩, h⟩ else (proj ↑⟨z, hzp⟩, Classical.arbitrary (Z → F) ↑⟨z, hzp⟩)).1 =
    proj ↑⟨z, hzp⟩
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 : { x // x ∈ s } × F
hx : x ∈ e.target
⊢ (if h : (Prod.map Subtype.val id x).1 ∈ s then
      e.invFun (⟨(Prod.map Subtype.val id x).1, h⟩, (Prod.map Subtype.val id x).2)
    else Classical.arbitrary (B → F → Z) (Prod.map Subtype.val id x).1 (Prod.map Subtype.val id x).2) ∈
    e.source

Tactic:
;

Goal state after:
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 : { x // x ∈ s } × F
hx : x ∈ e.target
⊢ (if h : (Prod.map Subtype.val id x).1 ∈ s then
      e.invFun (⟨(Prod.map Subtype.val id x).1, h⟩, (Prod.map Subtype.val id x).2)
    else Classical.arbitrary (B → F → Z) (Prod.map Subtype.val id x).1 (Prod.map Subtype.val id x).2) ∈
    e.source
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 : { x // x ∈ s } × F
hx : x ∈ e.target
⊢ (↑(↑e
            (if h : (Prod.map Subtype.val id x).1 ∈ s then
              e.invFun (⟨(Prod.map Subtype.val id x).1, h⟩, (Prod.map Subtype.val id x).2)
            else Classical.arbitrary (B → F → Z) (Prod.map Subtype.val id x).1 (Prod.map Subtype.val id x).2)).1,
      (↑e
          (if h : (Prod.map Subtype.val id x).1 ∈ s then
            e.invFun (⟨(Prod.map Subtype.val id x).1, h⟩, (Prod.map Subtype.val id x).2)
          else Classical.arbitrary (B → F → Z) (Prod.map Subtype.val id x).1 (Prod.map Subtype.val id x).2)).2) =
    Prod.map Subtype.val id x

Tactic:
;

Goal state after:
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 : { x // x ∈ s } × F
hx : x ∈ e.target
⊢ (↑(↑e
            (if h : (Prod.map Subtype.val id x).1 ∈ s then
              e.invFun (⟨(Prod.map Subtype.val id x).1, h⟩, (Prod.map Subtype.val id x).2)
            else Classical.arbitrary (B → F → Z) (Prod.map Subtype.val id x).1 (Prod.map Subtype.val id x).2)).1,
      (↑e
          (if h : (Prod.map Subtype.val id x).1 ∈ s then
            e.invFun (⟨(Prod.map Subtype.val id x).1, h⟩, (Prod.map Subtype.val id x).2)
          else Classical.arbitrary (B → F → Z) (Prod.map Subtype.val id x).1 (Prod.map Subtype.val id x).2)).2) =
    Prod.map Subtype.val id x
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
⊢ x✝ ∈ e.source ↔ x✝ ∈ Subtype.val ∘ proj ⁻¹' Subtype.val '' e.baseSet

Tactic:
;

Goal state after:
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
⊢ x✝ ∈ e.source ↔ x✝ ∈ Subtype.val ∘ proj ⁻¹' Subtype.val '' e.baseSet
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: case mk
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
toOpenPartialHomeomorph✝ : OpenPartialHomeomorph Z (B × F)
baseSet✝ : Set B
open_baseSet✝ : IsOpen[inst✝²] baseSet✝
source_eq✝ : toOpenPartialHomeomorph✝.source = proj ⁻¹' baseSet✝
target_eq✝ : toOpenPartialHomeomorph✝.target = baseSet✝ ×ˢ univ
proj_toFun✝ : ∀ p ∈ toOpenPartialHomeomorph✝.source, (↑toOpenPartialHomeomorph✝ p).1 = proj p
h₁ :
  { toOpenPartialHomeomorph := toOpenPartialHomeomorph✝, baseSet := baseSet✝, open_baseSet := open_baseSet✝,
        source_eq := source_eq✝, target_eq := target_eq✝, proj_toFun := proj_toFun✝ }.toOpenPartialHomeomorph =
    e'.toOpenPartialHomeomorph
h₂ :
  { toOpenPartialHomeomorph := toOpenPartialHomeomorph✝, baseSet := baseSet✝, open_baseSet := open_baseSet✝,
        source_eq := source_eq✝, target_eq := target_eq✝, proj_toFun := proj_toFun✝ }.baseSet =
    e'.baseSet
⊢ { toOpenPartialHomeomorph := toOpenPartialHomeomorph✝, baseSet := baseSet✝, open_baseSet := open_baseSet✝,
      source_eq := source_eq✝, target_eq := target_eq✝, proj_toFun := proj_toFun✝ } =
    e'

Tactic:
;

Goal state after:
case mk
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
toOpenPartialHomeomorph✝ : OpenPartialHomeomorph Z (B × F)
baseSet✝ : Set B
open_baseSet✝ : IsOpen[inst✝²] baseSet✝
source_eq✝ : toOpenPartialHomeomorph✝.source = proj ⁻¹' baseSet✝
target_eq✝ : toOpenPartialHomeomorph✝.target = baseSet✝ ×ˢ univ
proj_toFun✝ : ∀ p ∈ toOpenPartialHomeomorph✝.source, (↑toOpenPartialHomeomorph✝ p).1 = proj p
h₁ :
  { toOpenPartialHomeomorph := toOpenPartialHomeomorph✝, baseSet := baseSet✝, open_baseSet := open_baseSet✝,
        source_eq := source_eq✝, target_eq := target_eq✝, proj_toFun := proj_toFun✝ }.toOpenPartialHomeomorph =
    e'.toOpenPartialHomeomorph
h₂ :
  { toOpenPartialHomeomorph := toOpenPartialHomeomorph✝, baseSet := baseSet✝, open_baseSet := open_baseSet✝,
        source_eq := source_eq✝, target_eq := target_eq✝, proj_toFun := proj_toFun✝ }.baseSet =
    e'.baseSet
⊢ { toOpenPartialHomeomorph := toOpenPartialHomeomorph✝, baseSet := baseSet✝, open_baseSet := open_baseSet✝,
      source_eq := source_eq✝, target_eq := target_eq✝, proj_toFun := proj_toFun✝ } =
    e'
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

Tactic:
;

Goal state after:
ι : 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
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
⊢ (fun x ↦ ↑x) ⁻¹' ↑e ∘ ↑e'.symm ⁻¹' s ∩ (fun x ↦ ↑x) ⁻¹' ↑e'.symm ⁻¹' e.source =
    e'.setSymm ⁻¹' ↑e ⁻¹' s ∩ e'.setSymm ⁻¹' e.source

Tactic:
;

Goal state after:
ι : 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
⊢ (fun x ↦ ↑x) ⁻¹' ↑e ∘ ↑e'.symm ⁻¹' s ∩ (fun x ↦ ↑x) ⁻¹' ↑e'.symm ⁻¹' e.source =
    e'.setSymm ⁻¹' ↑e ⁻¹' s ∩ e'.setSymm ⁻¹' e.source
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'
x✝ : Z
⊢ x✝ ∈ (e.transHomeomorph (h.prodCongr (Homeomorph.refl F))).source ↔ x✝ ∈ ⇑h ∘ proj ⁻¹' ⇑h.symm ⁻¹' e.baseSet

Tactic:
;

Goal state after:
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'
x✝ : Z
⊢ x✝ ∈ (e.transHomeomorph (h.prodCongr (Homeomorph.refl F))).source ↔ x✝ ∈ ⇑h ∘ proj ⁻¹' ⇑h.symm ⁻¹' e.baseSet
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'
x✝ : B' × F
⊢ x✝ ∈ (e.transHomeomorph (h.prodCongr (Homeomorph.refl F))).target ↔ x✝ ∈ (⇑h.symm ⁻¹' e.baseSet) ×ˢ univ

Tactic:
;

Goal state after:
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'
x✝ : B' × F
⊢ x✝ ∈ (e.transHomeomorph (h.prodCongr (Homeomorph.refl F))).target ↔ x✝ ∈ (⇑h.symm ⁻¹' e.baseSet) ×ˢ univ
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: case fst
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
e : Trivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
z : { x // x ∈ proj ⁻¹' s }
hz : z ∈ fun x ↦ e.source ↑x
⊢ ((Prod.map Subtype.val id ∘ ↑(e.toPretrivialization.restrictPreimage' s).toPartialEquiv) z).1 =
    ((↑e.toPartialEquiv ∘ Subtype.val) z).1

pp: case snd
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
e : Trivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
z : { x // x ∈ proj ⁻¹' s }
hz : z ∈ fun x ↦ e.source ↑x
⊢ ((Prod.map Subtype.val id ∘ ↑(e.toPretrivialization.restrictPreimage' s).toPartialEquiv) z).2 =
    ((↑e.toPartialEquiv ∘ Subtype.val) z).2

Tactic:
;

Goal state after:
case fst
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
e : Trivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
z : { x // x ∈ proj ⁻¹' s }
hz : z ∈ fun x ↦ e.source ↑x
⊢ ((Prod.map Subtype.val id ∘ ↑(e.toPretrivialization.restrictPreimage' s).toPartialEquiv) z).1 =
    ((↑e.toPartialEquiv ∘ Subtype.val) z).1

case snd
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
e : Trivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
z : { x // x ∈ proj ⁻¹' s }
hz : z ∈ fun x ↦ e.source ↑x
⊢ ((Prod.map Subtype.val id ∘ ↑(e.toPretrivialization.restrictPreimage' s).toPartialEquiv) z).2 =
    ((↑e.toPartialEquiv ∘ Subtype.val) z).2
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: case mp
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : IsLocallyInjective f
x : X
U : Set X
ho : IsOpen[inst✝] U
hm : x ∈ U
hi : Set.InjOn f U
⊢ ∃ U ∈ 𝓝 x, Set.InjOn f U

Tactic:
;

Goal state after:
case mp
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : IsLocallyInjective f
x : X
U : Set X
ho : IsOpen[inst✝] U
hm : x ∈ U
hi : Set.InjOn f U
⊢ ∃ U ∈ 𝓝 x, Set.InjOn f U
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
⊢ IsLocallyInjective f ↔ ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U

Tactic:
by
  constructor <;> intro h x
  · obtain ⟨U, ho, hm, hi⟩ := h x; exact ⟨U, ho.mem_nhds hm, hi⟩
  · obtain ⟨U, hn, hi⟩ := h x
    exact ⟨interior U, isOpen_interior, mem_interior_iff_mem_nhds.mpr hn, hi.mono interior_subset⟩

Goal state after: