awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
⊢ IsOpen[Pullback.TotalSpace.topologicalSpace F E (⇑f : (a : B') → B)]
    (TotalSpace.proj (E := E) ∘ Pullback.lift (E := E) (⇑f : (a : B') → B) ⁻¹' e.baseSet)

Tactic:
e.open_baseSet.preimage ((map_continuous f).comp <| Pullback.continuous_proj F E f)

Premises used: Continuous.comp, Bundle.Trivialization.open_baseSet, Pullback.continuous_proj, ContinuousMapClass.map_continuous, IsOpen.preimage, DFunLike.coe
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
⊢ IsOpen[Pullback.TotalSpace.topologicalSpace F E (⇑f : (a : B') → B)]
    (TotalSpace.proj (E := E) ∘ Pullback.lift (E := E) (⇑f : (a : B') → B) ⁻¹' e.baseSet)

Tactic:
exact e.open_baseSet.preimage ((map_continuous f).comp <| Pullback.continuous_proj F E f)

Premises used: Continuous.comp, Bundle.Trivialization.open_baseSet, Pullback.continuous_proj, ContinuousMapClass.map_continuous, IsOpen.preimage, DFunLike.coe
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
simp_rw :
  ContinuousOn (Y := B' × TotalSpace F E)
    (fun (x : B' × F) ↦
      (x.1, TotalSpace.mk (E := E) ((f : (a : B') → B) x.1) (e.symm (E := E) ((f : (a : B') → B) x.1) x.2)))
    (SProd.sprod (α := Set B') (β := Set F) ((⇑f : (a : B') → B) ⁻¹' e.baseSet) univ)
⊢ ContinuousOn (Y := TotalSpace.{w₂, v, w₁} (B := B') F ((⇑f : (a : B') → B) *ᵖ E))
    (fun (y : B' × F) ↦
      TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E) y.1 (e.symm (E := E) ((f : (a : B') → B) y.1) y.2))
    (SProd.sprod (α := Set B') (β := Set F) ((⇑f : (a : B') → B) ⁻¹' e.baseSet) univ)

Tactic:
simp_rw [(inducing_pullbackTotalSpaceEmbedding F E f).continuousOn_iff, Function.comp_def,
      pullbackTotalSpaceEmbedding]

Premises used: Function.comp_def, inducing_pullbackTotalSpaceEmbedding, Bundle.pullbackTotalSpaceEmbedding, Topology.IsInducing.continuousOn_iff, DFunLike.coe
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
⊢ ContinuousOn (Y := B' × TotalSpace F E)
    (fun (x : B' × F) ↦
      (x.1, TotalSpace.mk (E := E) ((f : (a : B') → B) x.1) (e.symm (E := E) ((f : (a : B') → B) x.1) x.2)))
    (SProd.sprod (α := Set B') (β := Set F) ((⇑f : (a : B') → B) ⁻¹' e.baseSet) univ)

Tactic:
continuousOn_fst.prodMk
      (e.continuousOn_symm.comp ((map_continuous f).prodMap continuous_id).continuousOn Subset.rfl)

Premises used: Continuous.continuousOn, Continuous.prodMap, Bundle.Trivialization.continuousOn_symm, ContinuousOn.comp, continuousOn_fst, continuous_id, Set.Subset.rfl, ContinuousOn.prodMk, ContinuousMapClass.map_continuous
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
⊢ ContinuousOn (Y := B' × TotalSpace F E)
    (fun (x : B' × F) ↦
      (x.1, TotalSpace.mk (E := E) ((f : (a : B') → B) x.1) (e.symm (E := E) ((f : (a : B') → B) x.1) x.2)))
    (SProd.sprod (α := Set B') (β := Set F) ((⇑f : (a : B') → B) ⁻¹' e.baseSet) univ)

Tactic:
exact continuousOn_fst.prodMk
      (e.continuousOn_symm.comp ((map_continuous f).prodMap continuous_id).continuousOn Subset.rfl)

Premises used: Continuous.continuousOn, Continuous.prodMap, Bundle.Trivialization.continuousOn_symm, ContinuousOn.comp, continuousOn_fst, continuous_id, Set.Subset.rfl, ContinuousOn.prodMk, ContinuousMapClass.map_continuous
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
rw :
  Eq (α := Set (TotalSpace.{w₂, v, w₁} (B := B') F ((⇑f : (a : B') → B) *ᵖ E)))
    (Pullback.lift (E := E) (⇑f : (a : B') → B) ⁻¹' TotalSpace.proj (E := E) ⁻¹' e.baseSet)
    (TotalSpace.proj (E := (⇑f : (a : B') → B) *ᵖ E) ⁻¹' (⇑f : (a : B') → B) ⁻¹' e.baseSet)
⊢ Eq (α := Set (TotalSpace.{w₂, v, w₁} (B := B') F ((⇑f : (a : B') → B) *ᵖ E)))
    (Pullback.lift (E := E) (⇑f : (a : B') → B) ⁻¹' e.source)
    (TotalSpace.proj (E := (⇑f : (a : B') → B) *ᵖ E) ⁻¹' (⇑f : (a : B') → B) ⁻¹' e.baseSet)

Tactic:
rw [e.source_eq]

Premises used: Bundle.Trivialization.source_eq
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
⊢ Eq (α := Set (TotalSpace.{w₂, v, w₁} (B := B') F ((⇑f : (a : B') → B) *ᵖ E)))
    (Pullback.lift (E := E) (⇑f : (a : B') → B) ⁻¹' TotalSpace.proj (E := E) ⁻¹' e.baseSet)
    (TotalSpace.proj (E := (⇑f : (a : B') → B) *ᵖ E) ⁻¹' (⇑f : (a : B') → B) ⁻¹' e.baseSet)

Tactic:
rfl
-- Module: Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle
Goal:
B : Type u_1
F : Type u_2
Z : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace Z
proj : Z → B
h : IsHomeomorphicTrivialFiberBundle F proj
⊢ ∃ (e : Z ≃ₜ B × F), proj = Function.comp (β := B × F) Prod.fst (⇑e : (a : Z) → B × F)

Tactic:
⟨h.choose, (funext h.choose_spec).symm⟩

Premises used: Exists.choose_spec, funext, Exists.intro, Exists.choose, Eq.symm
-- Module: Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle
Goal:
B : Type u_1
F : Type u_2
Z : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace Z
proj : Z → B
inst_3 : Nonempty F
h : IsHomeomorphicTrivialFiberBundle F proj
obtain :
  ∀ (e : Z ≃ₜ B × F)
    (h :
      IsHomeomorphicTrivialFiberBundle.{u_1, u_2, u_3} (B := B) F (Z := Z)
        (Function.comp (β := B × F) Prod.fst (⇑e : (a : Z) → B × F))),
    Function.Surjective.{u_3 + 1, u_1 + 1} (α := Z) (β := B)
      (Function.comp (β := B × F) Prod.fst (⇑e : (a : Z) → B × F))
⊢ Function.Surjective proj

Tactic:
obtain ⟨e, rfl⟩ := h.proj_eq

Premises used: IsHomeomorphicTrivialFiberBundle.proj_eq, rfl
-- Module: Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle
Goal:
B : Type u_1
F : Type u_2
Z : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace Z
inst_3 : Nonempty F
e : Z ≃ₜ B × F
h :
  IsHomeomorphicTrivialFiberBundle.{u_1, u_2, u_3} (B := B) F (Z := Z)
    (Function.comp (β := B × F) Prod.fst (⇑e : (a : Z) → B × F))
⊢ Function.Surjective.{u_3 + 1, u_1 + 1} (α := Z) (β := B) (Function.comp (β := B × F) Prod.fst (⇑e : (a : Z) → B × F))

Tactic:
Prod.fst_surjective.comp e.surjective

Premises used: Prod.fst_surjective, Function.Surjective.comp, Homeomorph.surjective
-- Module: Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle
Goal:
B : Type u_1
F : Type u_2
Z : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace Z
inst_3 : Nonempty F
e : Z ≃ₜ B × F
h :
  IsHomeomorphicTrivialFiberBundle.{u_1, u_2, u_3} (B := B) F (Z := Z)
    (Function.comp (β := B × F) Prod.fst (⇑e : (a : Z) → B × F))
⊢ Function.Surjective.{u_3 + 1, u_1 + 1} (α := Z) (β := B) (Function.comp (β := B × F) Prod.fst (⇑e : (a : Z) → B × F))

Tactic:
exact Prod.fst_surjective.comp e.surjective

Premises used: Prod.fst_surjective, Function.Surjective.comp, Homeomorph.surjective
-- Module: Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle
Goal:
B : Type u_1
F : Type u_2
Z : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace Z
proj : Z → B
h : IsHomeomorphicTrivialFiberBundle F proj
obtain :
  ∀ (e : Z ≃ₜ B × F)
    (h :
      IsHomeomorphicTrivialFiberBundle.{u_1, u_2, u_3} (B := B) F (Z := Z)
        (Function.comp (β := B × F) Prod.fst (⇑e : (a : Z) → B × F))),
    Continuous[inst_2, inst] (Function.comp (β := B × F) Prod.fst (⇑e : (a : Z) → B × F))
⊢ Continuous[inst_2, inst] proj

Tactic:
obtain ⟨e, rfl⟩ := h.proj_eq

Premises used: IsHomeomorphicTrivialFiberBundle.proj_eq, rfl
-- Module: Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle
Goal:
B : Type u_1
F : Type u_2
Z : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace Z
e : Z ≃ₜ B × F
h :
  IsHomeomorphicTrivialFiberBundle.{u_1, u_2, u_3} (B := B) F (Z := Z)
    (Function.comp (β := B × F) Prod.fst (⇑e : (a : Z) → B × F))
⊢ Continuous[inst_2, inst] (Function.comp (β := B × F) Prod.fst (⇑e : (a : Z) → B × F))

Tactic:
continuous_fst.comp e.continuous

Premises used: Homeomorph.continuous, Continuous.comp, continuous_fst
-- Module: Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle
Goal:
B : Type u_1
F : Type u_2
Z : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace Z
e : Z ≃ₜ B × F
h :
  IsHomeomorphicTrivialFiberBundle.{u_1, u_2, u_3} (B := B) F (Z := Z)
    (Function.comp (β := B × F) Prod.fst (⇑e : (a : Z) → B × F))
⊢ Continuous[inst_2, inst] (Function.comp (β := B × F) Prod.fst (⇑e : (a : Z) → B × F))

Tactic:
exact continuous_fst.comp e.continuous

Premises used: Homeomorph.continuous, Continuous.comp, continuous_fst
-- Module: Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle
Goal:
B : Type u_1
F : Type u_2
Z : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace Z
proj : Z → B
h : IsHomeomorphicTrivialFiberBundle F proj
obtain :
  ∀ (e : Z ≃ₜ B × F)
    (h :
      IsHomeomorphicTrivialFiberBundle.{u_1, u_2, u_3} (B := B) F (Z := Z)
        (Function.comp (β := B × F) Prod.fst (⇑e : (a : Z) → B × F))),
    IsOpenMap.{u_3, u_1} (X := Z) (Y := B) (Function.comp (β := B × F) Prod.fst (⇑e : (a : Z) → B × F))
⊢ IsOpenMap proj

Tactic:
obtain ⟨e, rfl⟩ := h.proj_eq

Premises used: IsHomeomorphicTrivialFiberBundle.proj_eq, rfl
-- Module: Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle
Goal:
B : Type u_1
F : Type u_2
Z : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace Z
e : Z ≃ₜ B × F
h :
  IsHomeomorphicTrivialFiberBundle.{u_1, u_2, u_3} (B := B) F (Z := Z)
    (Function.comp (β := B × F) Prod.fst (⇑e : (a : Z) → B × F))
⊢ IsOpenMap.{u_3, u_1} (X := Z) (Y := B) (Function.comp (β := B × F) Prod.fst (⇑e : (a : Z) → B × F))

Tactic:
isOpenMap_fst.comp e.isOpenMap

Premises used: IsOpenMap.comp, isOpenMap_fst, Homeomorph.isOpenMap
-- Module: Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle
Goal:
B : Type u_1
F : Type u_2
Z : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace Z
e : Z ≃ₜ B × F
h :
  IsHomeomorphicTrivialFiberBundle.{u_1, u_2, u_3} (B := B) F (Z := Z)
    (Function.comp (β := B × F) Prod.fst (⇑e : (a : Z) → B × F))
⊢ IsOpenMap.{u_3, u_1} (X := Z) (Y := B) (Function.comp (β := B × F) Prod.fst (⇑e : (a : Z) → B × F))

Tactic:
exact isOpenMap_fst.comp e.isOpenMap

Premises used: IsOpenMap.comp, isOpenMap_fst, Homeomorph.isOpenMap
-- Module: Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle
Goal:
B : Type u_1
F : Type u_2
Z : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace Z
proj : Z → B
inst_3 : Nonempty F
h : IsHomeomorphicTrivialFiberBundle F proj
⊢ IsQuotientMap proj

Tactic:
h.isOpenMap_proj.isQuotientMap h.continuous_proj h.surjective_proj

Premises used: IsOpenMap.isQuotientMap, IsHomeomorphicTrivialFiberBundle.surjective_proj, IsHomeomorphicTrivialFiberBundle.continuous_proj, IsHomeomorphicTrivialFiberBundle.isOpenMap_proj
-- Module: Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle
Goal:
B : Type u_1
F : Type u_2
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
⊢ IsHomeomorphicTrivialFiberBundle (B := B) F (Z := B × F) Prod.fst

Tactic:
⟨Homeomorph.refl _, fun _x => rfl⟩

Premises used: IsHomeomorphicTrivialFiberBundle, Homeomorph.refl, Exists.intro, rfl
-- Module: Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle
Goal:
B : Type u_1
F : Type u_2
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
⊢ IsHomeomorphicTrivialFiberBundle (B := B) F (Z := F × B) Prod.snd

Tactic:
⟨Homeomorph.prodComm _ _, fun _x => rfl⟩

Premises used: Homeomorph.prodComm, IsHomeomorphicTrivialFiberBundle, Exists.intro, 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
e e' : Pretrivialization F proj
h₁ : e.toPartialEquiv = e'.toPartialEquiv
h₂ : e.baseSet = e'.baseSet
mk :
  ∀ (toPartialEquiv : PartialEquiv Z (B × F)) (open_target : IsOpen[instTopologicalSpaceProd] toPartialEquiv.target)
    (baseSet : Set B) (open_baseSet : IsOpen[inst] baseSet) (source_eq : toPartialEquiv.source = proj ⁻¹' baseSet)
    (target_eq : toPartialEquiv.target = SProd.sprod (β := Set F) baseSet univ)
    (proj_toFun : ∀ p ∈ toPartialEquiv.source, ((↑toPartialEquiv : Z → B × F) p).1 = proj p)
    (h₁ :
      { toPartialEquiv := toPartialEquiv, open_target := open_target, baseSet := baseSet, open_baseSet := open_baseSet,
            source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun :
            Pretrivialization F proj }.toPartialEquiv =
        e'.toPartialEquiv)
    (h₂ :
      { toPartialEquiv := toPartialEquiv, open_target := open_target, baseSet := baseSet, open_baseSet := open_baseSet,
            source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun :
            Pretrivialization F proj }.baseSet =
        e'.baseSet),
    { toPartialEquiv := toPartialEquiv, open_target := open_target, baseSet := baseSet, open_baseSet := open_baseSet,
        source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun : Pretrivialization F proj } =
      e'
⊢ e = e'

Tactic:
cases e
-- 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
toPartialEquiv : PartialEquiv Z (B × F)
open_target : IsOpen[instTopologicalSpaceProd] toPartialEquiv.target
baseSet : Set B
open_baseSet : IsOpen[inst] baseSet
source_eq : toPartialEquiv.source = proj ⁻¹' baseSet
target_eq : toPartialEquiv.target = SProd.sprod (β := Set F) baseSet univ
proj_toFun : ∀ p ∈ toPartialEquiv.source, ((↑toPartialEquiv : Z → B × F) p).1 = proj p
toPartialEquiv_1 : PartialEquiv Z (B × F)
open_target_1 : IsOpen[instTopologicalSpaceProd] toPartialEquiv_1.target
baseSet_1 : Set B
open_baseSet_1 : IsOpen[inst] baseSet_1
source_eq_1 : toPartialEquiv_1.source = proj ⁻¹' baseSet_1
target_eq_1 : toPartialEquiv_1.target = SProd.sprod (β := Set F) baseSet_1 univ
proj_toFun_1 : ∀ p ∈ toPartialEquiv_1.source, ((↑toPartialEquiv_1 : Z → B × F) p).1 = proj p
h₁ :
  { toPartialEquiv := toPartialEquiv, open_target := open_target, baseSet := baseSet, open_baseSet := open_baseSet,
        source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun :
        Pretrivialization F proj }.toPartialEquiv =
    { toPartialEquiv := toPartialEquiv_1, open_target := open_target_1, baseSet := baseSet_1,
        open_baseSet := open_baseSet_1, source_eq := source_eq_1, target_eq := target_eq_1, proj_toFun := proj_toFun_1 :
        Pretrivialization F proj }.toPartialEquiv
h₂ :
  { toPartialEquiv := toPartialEquiv, open_target := open_target, baseSet := baseSet, open_baseSet := open_baseSet,
        source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun : Pretrivialization F proj }.baseSet =
    { toPartialEquiv := toPartialEquiv_1, open_target := open_target_1, baseSet := baseSet_1,
        open_baseSet := open_baseSet_1, source_eq := source_eq_1, target_eq := target_eq_1, proj_toFun := proj_toFun_1 :
        Pretrivialization F proj }.baseSet
⊢ { toPartialEquiv := toPartialEquiv, open_target := open_target, baseSet := baseSet, open_baseSet := open_baseSet,
      source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun : Pretrivialization F proj } =
    { toPartialEquiv := toPartialEquiv_1, open_target := open_target_1, baseSet := baseSet_1,
      open_baseSet := open_baseSet_1, source_eq := source_eq_1, target_eq := target_eq_1, proj_toFun := proj_toFun_1 }

Tactic:
congr
-- 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
e e' : Pretrivialization F proj
h₁ : ∀ (x : Z), (↑e : Z → B × F) x = (↑e' : Z → B × F) x
h₂ : ∀ (x : B × F), (↑e.symm : B × F → Z) x = (↑e'.symm : B × F → Z) x
h₃ : e.baseSet = e'.baseSet
h₄ : e.toPartialEquiv = e'.toPartialEquiv
h₅ : e.baseSet = e'.baseSet
⊢ e = e'

Tactic:
ext1
-- 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
e e' : Pretrivialization F proj
h₁ : ∀ (x : Z), (↑e : Z → B × F) x = (↑e' : Z → B × F) x
h₂ : ∀ (x : B × F), (↑e.symm : B × F → Z) x = (↑e'.symm : B × F → Z) x
h₃ : e.baseSet = e'.baseSet
h₄ : ∀ (x : Z), (↑e.toPartialEquiv : Z → B × F) x = (↑e'.toPartialEquiv : Z → B × F) x
h₅ : ∀ (x : B × F), (↑e.symm : B × F → Z) x = (↑e'.symm : B × F → Z) x
h₆ : e.source = e'.source
⊢ e.toPartialEquiv = e'.toPartialEquiv

Tactic:
ext1
-- 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
e e' : Pretrivialization F proj
h₁ : ∀ (x : Z), (↑e : Z → B × F) x = (↑e' : Z → B × F) x
h₂ : ∀ (x : B × F), (↑e.symm : B × F → Z) x = (↑e'.symm : B × F → Z) x
h₃ : e.baseSet = e'.baseSet
⊢ e.baseSet = e'.baseSet

Tactic:
h₃
-- 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
e e' : Pretrivialization F proj
h₁ : ∀ (x : Z), (↑e : Z → B × F) x = (↑e' : Z → B × F) x
h₂ : ∀ (x : B × F), (↑e.symm : B × F → Z) x = (↑e'.symm : B × F → Z) x
h₃ : e.baseSet = e'.baseSet
⊢ e.baseSet = e'.baseSet

Tactic:
exact h₃
-- 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
e e' : Pretrivialization F proj
h₁ : ∀ (x : Z), (↑e : Z → B × F) x = (↑e' : Z → B × F) x
h₂ : ∀ (x : B × F), (↑e.symm : B × F → Z) x = (↑e'.symm : B × F → Z) x
h₃ : e.baseSet = e'.baseSet
h₄ : ∀ (x : Z), (↑e.toPartialEquiv : Z → B × F) x = (↑e'.toPartialEquiv : Z → B × F) x
h₅ : ∀ (x : B × F), (↑e.symm : B × F → Z) x = (↑e'.symm : B × F → Z) x
h₆ : e.source = e'.source
⊢ e = e'

Tactic:
ext1 <;> [ext1; exact h₃]
-- 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
e e' : Pretrivialization F proj
h₁ : ∀ (x : Z), (↑e : Z → B × F) x = (↑e' : Z → B × F) x
h₂ : ∀ (x : B × F), (↑e.symm : B × F → Z) x = (↑e'.symm : B × F → Z) x
h₃ : e.baseSet = e'.baseSet
x : Z
⊢ (↑e.toPartialEquiv : Z → B × F) x = (↑e'.toPartialEquiv : Z → B × F) x

Tactic:
apply h₁
-- 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
e e' : Pretrivialization F proj
h₁ : ∀ (x : Z), (↑e : Z → B × F) x = (↑e' : Z → B × F) x
h₂ : ∀ (x : B × F), (↑e.symm : B × F → Z) x = (↑e'.symm : B × F → Z) x
h₃ : e.baseSet = e'.baseSet
x : B × F
⊢ (↑e.symm : B × F → Z) x = (↑e'.symm : B × F → Z) x

Tactic:
apply h₂
-- 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
e e' : Pretrivialization F proj
h₁ : ∀ (x : Z), (↑e : Z → B × F) x = (↑e' : Z → B × F) x
h₂ : ∀ (x : B × F), (↑e.symm : B × F → Z) x = (↑e'.symm : B × F → Z) x
h₃ : e.baseSet = e'.baseSet
h₄ : proj ⁻¹' e.baseSet = e'.source
h₅ : proj ⁻¹' e.baseSet = proj ⁻¹' e'.baseSet
h₆ h₇ : proj ⁻¹' e'.baseSet = proj ⁻¹' e'.baseSet
⊢ e.source = e'.source

Tactic:
rw [e.source_eq, e'.source_eq, h₃]

Premises used: Bundle.Pretrivialization.source_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 : Nonempty F
⊢ Injective (α := Pretrivialization F proj) toPartialEquiv

Tactic:
fun e e' h ↦ ext' _ _ h ?_

Premises used: Bundle.Pretrivialization.ext', Function.Injective
-- 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 : Nonempty F
refine : ∀ (e e' : Pretrivialization F proj) (h : e.toPartialEquiv = e'.toPartialEquiv), e.baseSet = e'.baseSet
⊢ Injective (α := Pretrivialization F proj) toPartialEquiv

Tactic:
refine fun e e' h ↦ ext' _ _ h ?_

Premises used: Bundle.Pretrivialization.ext'
-- 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 : Nonempty F
e e' : Pretrivialization F proj
h : e.toPartialEquiv = e'.toPartialEquiv
⊢ e.baseSet = e'.baseSet

Tactic:
simpa only [fst_image_prod, univ_nonempty, target_eq]
    using congr_arg (Prod.fst '' PartialEquiv.target ·) h

Premises used: PartialEquiv.target, Set.univ_nonempty, Bundle.Pretrivialization.target_eq, Set.fst_image_prod, Prod.fst, congr_arg, Set.image
-- 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
e : Pretrivialization F proj
⊢ (↑e.toPartialEquiv : Z → B × F) = (↑e : Z → B × F)

Tactic:
rfl

Premises used: Bundle.Pretrivialization.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
e : Pretrivialization F proj
x : Z
ex : x ∈ e.source
⊢ ((↑e : Z → B × F) x).1 = proj x

Tactic:
e.proj_toFun x ex

Premises used: Bundle.Pretrivialization.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
e : Pretrivialization F proj
x : Z
rw : x ∈ proj ⁻¹' e.baseSet ↔ proj x ∈ e.baseSet
rw₁ rw₂ : proj x ∈ e.baseSet ↔ proj x ∈ e.baseSet
⊢ x ∈ e.source ↔ proj x ∈ e.baseSet

Tactic:
rw [e.source_eq, mem_preimage]

Premises used: Bundle.Pretrivialization.source_eq, Set.mem_preimage