awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
p : (↑e.source : Type u_4)
⊢ (e.sourceHomeomorphBaseSetProd : (a : (↑e.source : Type u_4)) → (↑e.baseSet : Type u_1) × F) p =
    (Subtype.mk (p := fun (x : B) ↦ x ∈ e.baseSet) (proj (↑p : Z)) ⋯, ((↑e : Z → B × F) (↑p : Z)).2)

Tactic:
e.preimageHomeomorph_apply subset_rfl ⟨p, e.mem_source.mp p.2⟩

Premises used: Bundle.Trivialization.preimageHomeomorph_apply, Prod.map, Subtype.mk, Bundle.Trivialization.mem_source, Iff.mp, Subtype.val, subset_rfl, Subtype.property
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
p : Prod.{u_1, u_2} (↑e.baseSet : Type u_1) F
⊢ Eq.{u_4 + 1} (α := (↑e.source : Type u_4))
    ((e.sourceHomeomorphBaseSetProd.symm : (a : (↑e.baseSet : Type u_1) × F) → (↑e.source : Type u_4)) p :
      (↑e.source : Type u_4))
    (Subtype.mk (p := fun (x : Z) ↦ x ∈ e.source) ((↑e.symm : B × F → Z) ((↑p.1 : B), p.2)) ⋯ :
      { x : Z // x ∈ e.source })

Tactic:
rfl

Premises used: Set.Mem, OpenPartialHomeomorph.toFun', rfl
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
b : B
hb : b ∈ e.baseSet
p : (↑(proj ⁻¹' {b}) : Type u_4)
⊢ (e.preimageSingletonHomeomorph hb : (a : (↑(proj ⁻¹' {b}) : Type u_4)) → F) p = ((↑e : Z → B × F) (↑p : Z)).2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
b : B
hb : b ∈ e.baseSet
p : F
rw : Membership.mem (γ := Set B) {b} (proj ((↑e.symm : B × F → Z) (b, p)))
rw₁ : Membership.mem (γ := Set B) {b} b
rw₂ rw₃ : b = b
⊢ (↑e.symm : B × F → Z) (b, p) ∈ proj ⁻¹' {b}

Tactic:
rw [mem_preimage, e.proj_symm_apply' hb, mem_singleton_iff]

Premises used: Set.mem_singleton_iff, Bundle.Trivialization.proj_symm_apply', Set.mem_preimage
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
b : B
hb : b ∈ e.baseSet
p : F
⊢ ((e.preimageSingletonHomeomorph hb).symm : (a : F) → (↑(proj ⁻¹' {b}) : Type u_4)) p =
    Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' {b}) ((↑e.symm : B × F → Z) (b, p)) ⋯

Tactic:
rfl

Premises used: Subtype.map, Set.MapsTo.restrict, rfl
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
x : Z
ex : x ∈ e.source
⊢ ContinuousAt proj x

Tactic:
(e.map_proj_nhds ex).le

Premises used: ContinuousAt, Eq.le, Filter.Tendsto, Bundle.Trivialization.map_proj_nhds
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
⊢ ContinuousOn proj e.source

Tactic:
continuousOn_of_forall_continuousAt fun _ ↦ e.continuousAt_proj

Premises used: continuousOn_of_forall_continuousAt, Bundle.Trivialization.continuousAt_proj
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
b : B
v : F
hb : b ∈ e.baseSet
⊢ ContinuousAt (Y := B × F) (fun (x : B) ↦ (x, v)) b

Tactic:
fun_prop
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e : Trivialization F proj
v : F
⊢ ContinuousOn.{u_1, u_4} (Y := Z) (fun (x : B) ↦ (↑e.symm : B × F → Z) (x, v)) e.baseSet

Tactic:
fun _ hb ↦ (e.continuousAt_symm_prodMk_left hb).continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, Bundle.Trivialization.continuousAt_symm_prodMk_left, ContinuousOn
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
Z' : Type u_5
inst_4 : TopologicalSpace Z'
h : Z' ≃ₜ Z
⊢ (h.transOpenPartialHomeomorph e.toOpenPartialHomeomorph).source = proj ∘ (⇑h : (a : Z') → Z) ⁻¹' e.baseSet

Tactic:
simp [source_eq, preimage_preimage, Function.comp_def]

Premises used: Bundle.Trivialization.source_eq, Set.preimage_preimage, Function.comp_def
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
Z' : Type u_5
inst_4 : TopologicalSpace Z'
h : Z' ≃ₜ Z
⊢ (h.transOpenPartialHomeomorph e.toOpenPartialHomeomorph).target = SProd.sprod (β := Set F) e.baseSet univ

Tactic:
simp [target_eq]

Premises used: Bundle.Trivialization.target_eq
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
Z' : Type u_5
inst_4 : TopologicalSpace Z'
h : Z' ≃ₜ Z
p : Z'
hp : p ∈ (h.transOpenPartialHomeomorph e.toOpenPartialHomeomorph).source
⊢ Membership.mem (α := Z) e.source ((h : (a : Z') → Z) p : Z)

Tactic:
simpa using hp
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
Z' : Type u_5
inst_4 : TopologicalSpace Z'
h : Z' ≃ₜ Z
p : Z'
hp : p ∈ (h.transOpenPartialHomeomorph e.toOpenPartialHomeomorph).source
⊢ Membership.mem (α := Z) e.source ((h : (a : Z') → Z) p : Z)

Tactic:
have hp : h p ∈ e.source := by simpa using hp
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
Z' : Type u_5
inst_4 : TopologicalSpace Z'
h : Z' ≃ₜ Z
p : Z'
hp_1 : p ∈ (h.transOpenPartialHomeomorph e.toOpenPartialHomeomorph).source
hp : Membership.mem (α := Z) e.source ((h : (a : Z') → Z) p : Z)
⊢ ((↑(h.transOpenPartialHomeomorph e.toOpenPartialHomeomorph) : Z' → B × F) p).1 = (proj ∘ (⇑h : (a : Z') → Z)) p

Tactic:
simp [hp]
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
B' : Type u_5
inst_4 : TopologicalSpace B'
h : B ≃ₜ B'
h₁ :
  ∀ (x : Z),
    x ∈ (e.transHomeomorph (h.prodCongr (Homeomorph.refl F))).source ↔
      x ∈ preimage.{u_4, u_5} (β := B') ((⇑h : (a : B) → B') ∘ proj) ((⇑h.symm : (a : B') → B) ⁻¹' e.baseSet)
⊢ (e.transHomeomorph (h.prodCongr (Homeomorph.refl F))).source =
    preimage.{u_4, u_5} (β := B') ((⇑h : (a : B) → B') ∘ proj) ((⇑h.symm : (a : B') → B) ⁻¹' e.baseSet)

Tactic:
ext
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
B' : Type u_5
inst_4 : TopologicalSpace B'
h : B ≃ₜ B'
x_1 : Z
⊢ x_1 ∈ (e.transHomeomorph (h.prodCongr (Homeomorph.refl F))).source ↔
    x_1 ∈ preimage.{u_4, u_5} (β := B') ((⇑h : (a : B) → B') ∘ proj) ((⇑h.symm : (a : B') → B) ⁻¹' e.baseSet)

Tactic:
simp [e.mem_source]

Premises used: Bundle.Trivialization.mem_source
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
B' : Type u_5
inst_4 : TopologicalSpace B'
h : B ≃ₜ B'
h₁ :
  ∀ (x : B' × F),
    x ∈ (e.transHomeomorph (h.prodCongr (Homeomorph.refl F))).target ↔
      x ∈ SProd.sprod (α := Set B') (β := Set F) ((⇑h.symm : (a : B') → B) ⁻¹' e.baseSet) univ
⊢ (e.transHomeomorph (h.prodCongr (Homeomorph.refl F))).target =
    SProd.sprod (α := Set B') (β := Set F) ((⇑h.symm : (a : B') → B) ⁻¹' e.baseSet) univ

Tactic:
ext
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
B' : Type u_5
inst_4 : TopologicalSpace B'
h : B ≃ₜ B'
x_1 : B' × F
⊢ x_1 ∈ (e.transHomeomorph (h.prodCongr (Homeomorph.refl F))).target ↔
    x_1 ∈ SProd.sprod (α := Set B') (β := Set F) ((⇑h.symm : (a : B') → B) ⁻¹' e.baseSet) univ

Tactic:
simp [Prod.map, e.mem_target]

Premises used: Prod.map, Bundle.Trivialization.mem_target
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
B' : Type u_5
inst_4 : TopologicalSpace B'
h : B ≃ₜ B'
p : Z
hp : p ∈ (e.transHomeomorph (h.prodCongr (Homeomorph.refl F))).source
⊢ ((↑(e.transHomeomorph (h.prodCongr (Homeomorph.refl F))) : Z → B' × F) p).1 = ((⇑h : (a : B) → B') ∘ proj) p

Tactic:
simpa using e.proj_toFun p hp

Premises used: Bundle.Trivialization.proj_toFun
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
X : Type u_5
inst_3 : TopologicalSpace X
f : Z → X
z : Z
e : Trivialization F proj
he : proj z ∈ e.baseSet
hf : ContinuousAt (f ∘ (↑e.symm : B × F → Z)) ((↑e : Z → B × F) z)
rw : proj z ∈ e.baseSet
⊢ z ∈ e.symm.target

Tactic:
rw [PartialEquiv.symm_target, e.mem_source]

Premises used: PartialEquiv.symm_target, Bundle.Trivialization.mem_source
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
X : Type u_5
inst_3 : TopologicalSpace X
f : Z → X
z : Z
e : Trivialization F proj
he : proj z ∈ e.baseSet
hf : ContinuousAt (f ∘ (↑e.symm : B × F → Z)) ((↑e : Z → B × F) z)
⊢ proj z ∈ e.baseSet

Tactic:
he
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
X : Type u_5
inst_3 : TopologicalSpace X
f : Z → X
z : Z
e : Trivialization F proj
he : proj z ∈ e.baseSet
hf : ContinuousAt (f ∘ (↑e.symm : B × F → Z)) ((↑e : Z → B × F) z)
⊢ proj z ∈ e.baseSet

Tactic:
exact he
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
X : Type u_5
inst_3 : TopologicalSpace X
f : Z → X
z : Z
e : Trivialization F proj
he : proj z ∈ e.baseSet
hf : ContinuousAt (f ∘ (↑e.symm : B × F → Z)) ((↑e : Z → B × F) z)
⊢ z ∈ e.symm.target

Tactic:
have hez : z ∈ e.toPartialEquiv.symm.target := by
    rw [PartialEquiv.symm_target, e.mem_source]
    exact he
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
X : Type u_5
inst_3 : TopologicalSpace X
f : Z → X
z : Z
e : Trivialization F proj
he : proj z ∈ e.baseSet
hf : ContinuousAt (f ∘ (↑e.symm : B × F → Z)) ((↑e : Z → B × F) z)
hez : z ∈ e.symm.target
rwa : ContinuousAt (f ∘ (↑e.symm : B × F → Z)) ((↑e.symm.symm : Z → B × F) z)
rwa₁ rwa₂ rwa₃ rwa₄ : ContinuousAt (f ∘ (↑e.symm : B × F → Z)) ((↑e.toOpenPartialHomeomorph : Z → B × F) z)
⊢ ContinuousAt f z

Tactic:
rwa [e.toOpenPartialHomeomorph.symm.continuousAt_iff_continuousAt_comp_right hez,
    OpenPartialHomeomorph.symm_symm]

Premises used: OpenPartialHomeomorph.continuousAt_iff_continuousAt_comp_right, OpenPartialHomeomorph.symm_symm, Bundle.Trivialization.toOpenPartialHomeomorph, OpenPartialHomeomorph.symm
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
X : Type u_5
inst_3 : 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 : Z → B × F) ∘ f) x
rw : ContinuousAt ((↑e.toOpenPartialHomeomorph : Z → B × F) ∘ f) x
rw₁ : f ⁻¹' e.source ∈ 𝓝 x
⊢ ContinuousAt f x

Tactic:
rw [e.continuousAt_iff_continuousAt_comp_left]

Premises used: OpenPartialHomeomorph.continuousAt_iff_continuousAt_comp_left, Bundle.Trivialization.toOpenPartialHomeomorph
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
X : Type u_5
inst_3 : 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 : Z → B × F) ∘ f) x
⊢ ContinuousAt ((↑e.toOpenPartialHomeomorph : Z → B × F) ∘ f) x

Tactic:
hf

Premises used: Bundle.Trivialization.toFun', OpenPartialHomeomorph.toFun'
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
X : Type u_5
inst_3 : 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 : Z → B × F) ∘ f) x
⊢ ContinuousAt ((↑e.toOpenPartialHomeomorph : Z → B × F) ∘ f) x

Tactic:
exact hf
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
X : Type u_5
inst_3 : 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 : Z → B × F) ∘ f) x
rw : proj ∘ f ⁻¹' e.baseSet ∈ 𝓝 x
⊢ f ⁻¹' e.source ∈ 𝓝 x

Tactic:
rw [e.source_eq, ← preimage_comp]

Premises used: Bundle.Trivialization.source_eq, Set.preimage_comp
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
X : Type u_5
inst_3 : 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 : Z → B × F) ∘ f) x
⊢ proj ∘ f ⁻¹' e.baseSet ∈ 𝓝 x

Tactic:
hf_proj.preimage_mem_nhds (e.open_baseSet.mem_nhds he)

Premises used: ContinuousAt.preimage_mem_nhds, Bundle.Trivialization.open_baseSet, IsOpen.mem_nhds
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
X : Type u_5
inst_3 : 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 : Z → B × F) ∘ f) x
⊢ proj ∘ f ⁻¹' e.baseSet ∈ 𝓝 x

Tactic:
exact hf_proj.preimage_mem_nhds (e.open_baseSet.mem_nhds he)

Premises used: ContinuousAt.preimage_mem_nhds, Bundle.Trivialization.open_baseSet, IsOpen.mem_nhds
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace (TotalSpace F E)
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
⊢ ContinuousOn (↑e' : TotalSpace F E → B × F) e'.source

Tactic:
e'.continuousOn_toFun

Premises used: Bundle.Trivialization.toFun', OpenPartialHomeomorph.continuousOn_toFun, Bundle.Trivialization.toOpenPartialHomeomorph
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace (TotalSpace F E)
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
⊢ TotalSpace.mk (E := E) b y ∈ e'.source ↔ b ∈ e'.baseSet

Tactic:
e'.mem_source

Premises used: Set.Mem, Bundle.Trivialization.mem_source
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace (TotalSpace F E)
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
hb : b ∈ e'.baseSet
⊢ ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b y)).1 = b

Tactic:
e'.coe_fst (e'.mem_source.2 hb)

Premises used: Iff.mpr, Bundle.Trivialization.coe_fst, Bundle.Trivialization.mem_source
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace (TotalSpace F E)
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : F
⊢ (b, y) ∈ e'.target ↔ b ∈ e'.baseSet

Tactic:
e'.toPretrivialization.mem_target

Premises used: Bundle.Pretrivialization.mem_target, Set.Mem, Bundle.Trivialization.toPretrivialization
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace (TotalSpace F E)
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
x : TotalSpace F E
hx : x ∈ e'.source
⊢ (↑e'.symm : B × F → TotalSpace F E) ((↑e' : TotalSpace F E → B × F) x) = x

Tactic:
e'.toPartialEquiv.left_inv hx

Premises used: Bundle.Trivialization.toFun', OpenPartialHomeomorph.toFun', PartialEquiv.left_inv, OpenPartialHomeomorph.toPartialEquiv, Bundle.Trivialization.toOpenPartialHomeomorph
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace (TotalSpace F E)
x : B
y : F
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
h : x ∈ e.baseSet
⊢ ((↑e.symm : B × F → TotalSpace F E) (x, y)).proj (E := E) = x

Tactic:
e.proj_symm_apply' h

Premises used: Bundle.Trivialization.proj_symm_apply'
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (x : B) → Zero (E x)
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
hb : b ∈ e.baseSet
y : F
⊢ e.symm (E := E) b y = cast ⋯ (((↑e.symm : B × F → TotalSpace F E) (b, y)).snd (E := E))

Tactic:
dif_pos hb

Premises used: Bundle.Trivialization.symm, Set.Mem, dif_pos, Bundle.Pretrivialization.symm
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (x : B) → Zero (E x)
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
hb : b ∉ e.baseSet
y : F
⊢ e.symm (E := E) b y = 0

Tactic:
dif_neg hb

Premises used: Bundle.Trivialization.symm, Set.Mem, dif_neg, Bundle.Pretrivialization.symm
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (x : B) → Zero (E x)
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
hb : b ∈ e.baseSet
y : F
⊢ TotalSpace.mk (E := E) b (e.symm (E := E) b y) = (↑e.symm : B × F → TotalSpace F E) (b, y)

Tactic:
e.toPretrivialization.mk_symm hb y

Premises used: Bundle.Trivialization.symm, OpenPartialHomeomorph.toFun', Bundle.Trivialization.toPretrivialization, Bundle.Pretrivialization.mk_symm
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (x : B) → Zero (E x)
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
z : TotalSpace F E
hz : z.proj (E := E) ∈ e.baseSet
⊢ e.symm (E := E) (z.proj (E := E)) ((↑e : TotalSpace F E → B × F) z).2 = z.snd (E := E)

Tactic:
e.toPretrivialization.symm_proj_apply z hz

Premises used: Bundle.Pretrivialization.symm_proj_apply, Bundle.Trivialization.symm, Bundle.Trivialization.toPretrivialization
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (x : B) → Zero (E x)
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
hb : b ∈ e.baseSet
y : E b
⊢ e.symm (E := E) b ((↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b y)).2 = y

Tactic:
e.symm_proj_apply ⟨b, y⟩ hb

Premises used: Bundle.Trivialization.symm_proj_apply, Bundle.TotalSpace.mk
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (x : B) → Zero (E x)
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
hb : b ∈ e.baseSet
y : F
⊢ (↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b y)) = (b, y)

Tactic:
e.toPretrivialization.apply_mk_symm hb y

Premises used: Bundle.Trivialization.symm, Bundle.Trivialization.toFun', Bundle.Pretrivialization.apply_mk_symm, Bundle.Pretrivialization.toFun', Bundle.Trivialization.toPretrivialization
-- Module: Mathlib.Topology.FiberBundle.Trivialization
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (x : B) → Zero (E x)
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
x : B × F
hx : x.1 ∈ e.baseSet
right : Membership.mem (γ := Set F) univ x.2
rw rw₁ : (↑e.symm : B × F → TotalSpace F E) (x.1, x.2) = (↑e.symm : B × F → TotalSpace F E) x
⊢ TotalSpace.mk (E := E) x.1 (e.symm (E := E) x.1 x.2) = (↑e.symm : B × F → TotalSpace F E) x

Tactic:
rw [e.mk_symm hx]

Premises used: Bundle.Trivialization.mk_symm