awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ∈ SProd.sprod (β := Set F) e.baseSet univ,
    TotalSpace.mk (E := E) z.1 (e.symm (E := E) z.1 z.2) = (↑e.symm : B × F → TotalSpace F E) z

Tactic:
have : ∀ z ∈ e.baseSet ×ˢ (univ : Set F),
      TotalSpace.mk z.1 (e.symm z.1 z.2) = e.toOpenPartialHomeomorph.symm z := by
    rintro x ⟨hx : x.1 ∈ e.baseSet, _⟩
    rw [e.mk_symm hx]
-- 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))
this :
  ∀ z ∈ SProd.sprod (β := Set F) e.baseSet univ,
    TotalSpace.mk (E := E) z.1 (e.symm (E := E) z.1 z.2) = (↑e.symm : B × F → TotalSpace F E) z
⊢ ContinuousOn (Y := TotalSpace F E) (fun (z : B × F) ↦ TotalSpace.mk' (E := E) F z.1 (e.symm (E := E) z.1 z.2))
    (SProd.sprod (β := Set F) e.baseSet univ)

Tactic:
ContinuousOn.congr ?_ this

Premises used: ContinuousOn.congr
-- 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))
this :
  ∀ z ∈ SProd.sprod (β := Set F) e.baseSet univ,
    TotalSpace.mk (E := E) z.1 (e.symm (E := E) z.1 z.2) = (↑e.symm : B × F → TotalSpace F E) z
refine : ContinuousOn (↑e.symm : B × F → TotalSpace F E) (SProd.sprod (β := Set F) e.baseSet univ)
⊢ ContinuousOn (Y := TotalSpace F E) (fun (z : B × F) ↦ TotalSpace.mk' (E := E) F z.1 (e.symm (E := E) z.1 z.2))
    (SProd.sprod (β := Set F) e.baseSet univ)

Tactic:
refine ContinuousOn.congr ?_ this

Premises used: ContinuousOn.congr
-- 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))
this :
  ∀ z ∈ SProd.sprod (β := Set F) e.baseSet univ,
    TotalSpace.mk (E := E) z.1 (e.symm (E := E) z.1 z.2) = (↑e.symm : B × F → TotalSpace F E) z
rw : ContinuousOn (↑e.symm : B × F → TotalSpace F E) e.target
⊢ ContinuousOn (↑e.symm : B × F → TotalSpace F E) (SProd.sprod (β := Set F) e.baseSet univ)

Tactic:
rw [← e.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
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))
this :
  ∀ z ∈ SProd.sprod (β := Set F) e.baseSet univ,
    TotalSpace.mk (E := E) z.1 (e.symm (E := E) z.1 z.2) = (↑e.symm : B × F → TotalSpace F E) z
⊢ ContinuousOn (↑e.symm : B × F → TotalSpace F E) e.target

Tactic:
e.toOpenPartialHomeomorph.continuousOn_symm

Premises used: OpenPartialHomeomorph.continuousOn_symm, 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)
inst_3 : (x : B) → Zero (E x)
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
this :
  ∀ z ∈ SProd.sprod (β := Set F) e.baseSet univ,
    TotalSpace.mk (E := E) z.1 (e.symm (E := E) z.1 z.2) = (↑e.symm : B × F → TotalSpace F E) z
⊢ ContinuousOn (↑e.symm : B × F → TotalSpace F E) e.target

Tactic:
exact e.toOpenPartialHomeomorph.continuousOn_symm

Premises used: OpenPartialHomeomorph.continuousOn_symm, Bundle.Trivialization.toOpenPartialHomeomorph
-- 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_1 : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
F' : Type u_5
inst_4 : TopologicalSpace F'
e : Trivialization F proj
h : F ≃ₜ F'
⊢ (e.transHomeomorph (Homeomorph.prodCongr (Homeomorph.refl B) h)).target = SProd.sprod (β := Set F') e.baseSet univ

Tactic:
simp [target_eq, prod_univ, preimage_preimage]

Premises used: Set.preimage_preimage, Set.prod_univ, Bundle.Trivialization.target_eq
-- 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
F' : Type u_5
inst_3 : TopologicalSpace F'
e : Trivialization F proj
h : F ≃ₜ F'
x : Z
⊢ (↑(e.transFiberHomeomorph h) : Z → B × F') x = (((↑e : Z → B × F) x).1, (h : (a : F) → F') ((↑e : Z → B × F) x).2)

Tactic:
rfl

Premises used: Bundle.Trivialization.toFun', Prod.map, 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₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ (b, e₁.coordChange e₂ b x) = (↑e₂ : Z → B × F) ((↑e₁.symm : B × F → Z) (b, x))

Tactic:
Prod.ext ?_ rfl

Premises used: Prod.ext, 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₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
refine : (b, e₁.coordChange e₂ b x).1 = ((↑e₂ : Z → B × F) ((↑e₁.symm : B × F → Z) (b, x))).1
⊢ (b, e₁.coordChange e₂ b x) = (↑e₂ : Z → B × F) ((↑e₁.symm : B × F → Z) (b, x))

Tactic:
refine Prod.ext ?_ rfl

Premises used: Prod.ext, 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₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
rw : proj ((↑e₁.symm : B × F → Z) (b, x)) ∈ e₁.baseSet
rw₁ : proj ((↑e₁.symm : B × F → Z) (b, x)) ∈ e₂.baseSet
⊢ (b, e₁.coordChange e₂ b x).1 = ((↑e₂ : Z → B × F) ((↑e₁.symm : B × F → Z) (b, x))).1

Tactic:
rw [e₂.coe_fst', ← e₁.coe_fst', e₁.apply_symm_apply' h₁]

Premises used: Bundle.Trivialization.coe_fst', Bundle.Trivialization.apply_symm_apply'
-- 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₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
rwa rwa₁ rwa₂ rwa₃ : b ∈ e₁.baseSet
⊢ proj ((↑e₁.symm : B × F → Z) (b, x)) ∈ e₁.baseSet

Tactic:
rwa [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
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
rwa rwa₁ rwa₂ rwa₃ : b ∈ e₂.baseSet
⊢ proj ((↑e₁.symm : B × F → Z) (b, x)) ∈ e₂.baseSet

Tactic:
rwa [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
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
inst_2 : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
p : Z
h : proj p ∈ e₁.baseSet
rw : ((↑e₂ : Z → B × F) ((↑e₁.symm : B × F → Z) (proj p, ((↑e₁ : Z → B × F) p).2))).2 = ((↑e₂ : Z → B × F) p).2
rw₁ rw₂ : ((↑e₂ : Z → B × F) p).2 = ((↑e₂ : Z → B × F) p).2
⊢ e₁.coordChange e₂ (proj p) ((↑e₁ : Z → B × F) p).2 = ((↑e₂ : Z → B × F) p).2

Tactic:
rw [coordChange, e₁.symm_apply_mk_proj (e₁.mem_source.2 h)]

Premises used: Iff.mpr, Bundle.Trivialization.coordChange, Bundle.Trivialization.mem_source, Bundle.Trivialization.symm_apply_mk_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
h : b ∈ e.baseSet
x : F
rw : ((↑e : Z → B × F) ((↑e.symm : B × F → Z) (b, x))).2 = x
rw₁ rw₂ : (b, x).2 = x
⊢ e.coordChange e b x = x

Tactic:
rw [coordChange, e.apply_symm_apply' h]

Premises used: Bundle.Trivialization.coordChange, Bundle.Trivialization.apply_symm_apply'
-- 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
h : b ∈ e.baseSet
⊢ e.coordChange e b = id

Tactic:
funext <| e.coordChange_same_apply h

Premises used: funext, Bundle.Trivialization.coordChange_same_apply
-- 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₁ e₂ e₃ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
rw : (↑e₁.symm : B × F → Z) (b, x) ∈ e₂.source
⊢ e₂.coordChange e₃ b (e₁.coordChange e₂ b x) = e₁.coordChange e₃ b x

Tactic:
rw [coordChange, e₁.mk_coordChange _ h₁ h₂, ← e₂.coe_coe, e₂.left_inv, coordChange]

Premises used: OpenPartialHomeomorph.left_inv, Bundle.Trivialization.coordChange, Bundle.Trivialization.coe_coe, Bundle.Trivialization.mk_coordChange, 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
e₁ e₂ e₃ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
rwa : proj ((↑e₁.symm : B × F → Z) (b, x)) ∈ e₂.baseSet
rwa₁ rwa₂ rwa₃ rwa₄ : b ∈ e₂.baseSet
⊢ (↑e₁.symm : B × F → Z) (b, x) ∈ e₂.source

Tactic:
rwa [e₂.mem_source, e₁.proj_symm_apply' h₁]

Premises used: Bundle.Trivialization.mem_source, Bundle.Trivialization.proj_symm_apply'
-- 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₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
⊢ Continuous[inst_1, inst_1] (e₁.coordChange e₂ b)

Tactic:
continuous_snd.comp (e₂.toOpenPartialHomeomorph.continuousOn.comp_continuous
    (e₁.toOpenPartialHomeomorph.continuousOn_symm.comp_continuous ?_ ?_) ?_)

Premises used: ContinuousOn.comp_continuous, Continuous.comp, continuous_snd, Bundle.Trivialization.coordChange, OpenPartialHomeomorph.continuousOn, OpenPartialHomeomorph.continuousOn_symm, 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
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
refine_1 : Continuous[inst_1, instTopologicalSpaceProd] (Prod.mk b)
refine_2 : ∀ (x : F), (b, x) ∈ e₁.target
refine_3 : ∀ (x : F), (↑e₁.symm : B × F → Z) (b, x) ∈ e₂.source
⊢ Continuous[inst_1, inst_1] (e₁.coordChange e₂ b)

Tactic:
refine continuous_snd.comp (e₂.toOpenPartialHomeomorph.continuousOn.comp_continuous
    (e₁.toOpenPartialHomeomorph.continuousOn_symm.comp_continuous ?_ ?_) ?_)

Premises used: ContinuousOn.comp_continuous, Continuous.comp, continuous_snd, OpenPartialHomeomorph.continuousOn, OpenPartialHomeomorph.continuousOn_symm, 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
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
⊢ Continuous[inst_1, instTopologicalSpaceProd] (Prod.mk 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₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
⊢ ∀ (x : F), (b, x) ∈ e₁.target

Tactic:
fun x => e₁.mem_target.2 h₁

Premises used: Iff.mpr, Bundle.Trivialization.mem_target
-- 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₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
⊢ ∀ (x : F), (b, x) ∈ e₁.target

Tactic:
exact fun x => e₁.mem_target.2 h₁

Premises used: Iff.mpr, Bundle.Trivialization.mem_target
-- 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₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
refine_3 : proj ((↑e₁.symm : B × F → Z) (b, x)) ∈ e₂.baseSet
refine_3₁ refine_3₂ refine_3₃ refine_3₄ : b ∈ e₂.baseSet
⊢ (↑e₁.symm : B × F → Z) (b, x) ∈ e₂.source

Tactic:
rwa [e₂.mem_source, e₁.proj_symm_apply' h₁]

Premises used: Bundle.Trivialization.mem_source, Bundle.Trivialization.proj_symm_apply'
-- 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_1 : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b_1 : B
y : E b_1
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ e₂.coordChange e₁ b (e₁.coordChange e₂ b x) = x

Tactic:
simp only [*, coordChange_coordChange, coordChange_same_apply]

Premises used: Bundle.Trivialization.coordChange_same_apply, Bundle.Trivialization.coordChange_coordChange
-- 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_1 : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b_1 : B
y : E b_1
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ e₁.coordChange e₂ b (e₂.coordChange e₁ b x) = x

Tactic:
simp only [*, coordChange_coordChange, coordChange_same_apply]

Premises used: Bundle.Trivialization.coordChange_same_apply, Bundle.Trivialization.coordChange_coordChange
-- 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₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
⊢ (⇑(e₁.coordChangeHomeomorph e₂ h₁ h₂) : (a : F) → F) = e₁.coordChange e₂ b

Tactic:
rfl

Premises used: Bundle.Trivialization.coordChange, 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
s : Set B
x : Z
hx : x ∈ e.source
⊢ (↑e.toOpenPartialHomeomorph : Z → B × F) x ∈ SProd.sprod (β := Set F) s univ ↔ x ∈ proj ⁻¹' s

Tactic:
simp [hx]
-- 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_1 : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e : Trivialization F proj
s : Set B
hs : IsOpen[inst] s
⊢ (⋯.restr (s := SProd.sprod (β := Set F) s univ) (t := proj ⁻¹' s) ⋯).symm.source = proj ⁻¹' (e.baseSet ∩ s)

Tactic:
simp [source_eq]

Premises used: Bundle.Trivialization.source_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_1 : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e : Trivialization F proj
s : Set B
hs : IsOpen[inst] s
⊢ (⋯.restr (s := SProd.sprod (β := Set F) s univ) (t := proj ⁻¹' s) ⋯).symm.target =
    SProd.sprod (β := Set F) (e.baseSet ∩ s) univ

Tactic:
simp [target_eq, prod_univ]

Premises used: Set.prod_univ, 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_1 : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e : Trivialization F proj
s : Set B
inst_4 : Nonempty ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
⊢ Continuous[instTopologicalSpaceSubtype, inst_2] (Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s))

Tactic:
fun_prop
-- 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_1 : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e : Trivialization F proj
s : Set B
inst_4 : Nonempty ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
z : { x : Z // x ∈ proj ⁻¹' s }
hz : Membership.mem (γ := Set { x : Z // x ∈ proj ⁻¹' s }) (fun (x : { x : Z // x ∈ proj ⁻¹' s }) ↦ e.source (↑x : Z)) z
fst :
  ((Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id ∘
          (↑(e.toPretrivialization.restrictPreimage' s).toPartialEquiv :
            (↑(proj ⁻¹' s) : Type u_4) → (↑s : Type u_1) × F))
        z).1 =
    (((↑e.toPartialEquiv : Z → B × F) ∘ Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s)) z).1
snd :
  ((Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id ∘
          (↑(e.toPretrivialization.restrictPreimage' s).toPartialEquiv :
            (↑(proj ⁻¹' s) : Type u_4) → (↑s : Type u_1) × F))
        z).2 =
    (((↑e.toPartialEquiv : Z → B × F) ∘ Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s)) z).2
⊢ (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id ∘
        (↑(e.toPretrivialization.restrictPreimage' s).toPartialEquiv :
          (↑(proj ⁻¹' s) : Type u_4) → (↑s : Type u_1) × F))
      z =
    ((↑e.toPartialEquiv : Z → B × F) ∘ Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s)) z

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_1 : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e : Trivialization F proj
s : Set B
inst_4 : Nonempty ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
z : { x : Z // x ∈ proj ⁻¹' s }
hz : Membership.mem (γ := Set { x : Z // x ∈ proj ⁻¹' s }) (fun (x : { x : Z // x ∈ proj ⁻¹' s }) ↦ e.source (↑x : Z)) z
⊢ ((Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id ∘
          (↑(e.toPretrivialization.restrictPreimage' s).toPartialEquiv :
            (↑(proj ⁻¹' s) : Type u_4) → (↑s : Type u_1) × F))
        z).1 =
    (((↑e.toPartialEquiv : Z → B × F) ∘ Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s)) z).1

Tactic:
(e.proj_toFun _ hz).symm

Premises used: Eq.symm, Bundle.Trivialization.proj_toFun
-- 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_1 : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e : Trivialization F proj
s : Set B
inst_4 : Nonempty ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
z : { x : Z // x ∈ proj ⁻¹' s }
hz : Membership.mem (γ := Set { x : Z // x ∈ proj ⁻¹' s }) (fun (x : { x : Z // x ∈ proj ⁻¹' s }) ↦ e.source (↑x : Z)) z
⊢ ((Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id ∘
          (↑(e.toPretrivialization.restrictPreimage' s).toPartialEquiv :
            (↑(proj ⁻¹' s) : Type u_4) → (↑s : Type u_1) × F))
        z).2 =
    (((↑e.toPartialEquiv : Z → B × F) ∘ Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s)) 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_1 : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e : Trivialization F proj
s : Set B
inst_4 : Nonempty ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
z : { x : Z // x ∈ proj ⁻¹' s }
hz : Membership.mem (γ := Set { x : Z // x ∈ proj ⁻¹' s }) (fun (x : { x : Z // x ∈ proj ⁻¹' s }) ↦ e.source (↑x : Z)) z
⊢ ((Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id ∘
          (↑(e.toPretrivialization.restrictPreimage' s).toPartialEquiv :
            (↑(proj ⁻¹' s) : Type u_4) → (↑s : Type u_1) × F))
        z).1 =
    (((↑e.toPartialEquiv : Z → B × F) ∘ Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s)) z).1

Tactic:
exacts [(e.proj_toFun _ hz).symm, rfl]

Premises used: Eq.symm, rfl, Bundle.Trivialization.proj_toFun
-- 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_1 : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
s : Set B
hps : IsOpen[inst_2] (proj ⁻¹' s)
e : Trivialization.{u_1, u_2, u_4} (B := B) F fun (z : (↑(proj ⁻¹' s) : Type u_4)) ↦ proj (↑z : Z)
inst_4 : Nonempty (Z → F)
⊢ ContinuousOn (↑e.toPartialEquiv : (↑(proj ⁻¹' s) : Type u_4) → B × F) e.source

Tactic:
e.continuousOn_toFun

Premises used: OpenPartialHomeomorph.continuousOn_toFun, Bundle.Trivialization.toOpenPartialHomeomorph