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
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
e_1 : Pretrivialization F proj
x : Z
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
s : Set B
e : Pretrivialization.{u_1, u_2, u_4} (B := B) F fun (z : (↑(proj ⁻¹' s) : Type u_4)) ↦ proj (↑z : Z)
inst_2 : Nonempty (Z → F)
z : Z
hzp : proj z ∈ s
hze : Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) z hzp ∈ e.source
⊢ (↑(e.invFun
          (if h : proj (↑(Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) z hzp) : Z) ∈ s then
            (↑e : (↑(proj ⁻¹' s) : Type u_4) → B × F)
              (Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s)
                (↑(Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) z hzp) : Z) h)
          else
            (proj (↑(Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) z hzp) : Z),
              Classical.arbitrary (Z → F) (↑(Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) z hzp) : Z)))) :
      Z) =
    (↑(Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) z hzp) : Z)

Tactic:
simp [hzp, e.symm_apply_apply hze]

Premises used: Bundle.Pretrivialization.symm_apply_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
e_1 : Pretrivialization F proj
x : Z
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
s : Set B
e : Pretrivialization.{u_1, u_2, u_4} (B := B) F fun (z : (↑(proj ⁻¹' s) : Type u_4)) ↦ proj (↑z : Z)
inst_2 : Nonempty (Z → F)
h : ∀ (z : Z), z ∈ Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) '' e.source ↔ z ∈ proj ⁻¹' e.baseSet
⊢ Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) '' e.source = proj ⁻¹' e.baseSet

Tactic:
ext z
-- 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
e_1 : Pretrivialization F proj
x : Z
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
s : Set B
e : Pretrivialization.{u_1, u_2, u_4} (B := B) F fun (z : (↑(proj ⁻¹' s) : Type u_4)) ↦ proj (↑z : Z)
inst_2 : Nonempty (Z → F)
z : Z
⊢ z ∈ Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) '' e.source ↔ z ∈ proj ⁻¹' e.baseSet

Tactic:
simpa [e.source_eq] using
    (e.proj_symm_apply' · ▸ (e.invFun (proj z, Classical.arbitrary (Z → F) z)).2)

Premises used: Bundle.Pretrivialization.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
e_1 : Pretrivialization F proj
x : Z
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
s : Set B
e : Pretrivialization.{u_1, u_2, u_4} (B := B) F fun (z : (↑(proj ⁻¹' s) : Type u_4)) ↦ proj (↑z : Z)
inst_2 : Nonempty (Z → F)
h : ∀ (x : B × F), x ∈ e.target ↔ x ∈ SProd.sprod (β := Set F) e.baseSet univ
⊢ e.target = SProd.sprod (β := Set F) 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
e_1 : Pretrivialization F proj
x : Z
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
s : Set B
e : Pretrivialization.{u_1, u_2, u_4} (B := B) F fun (z : (↑(proj ⁻¹' s) : Type u_4)) ↦ proj (↑z : Z)
inst_2 : Nonempty (Z → F)
x_1 : B × F
⊢ x_1 ∈ e.target ↔ x_1 ∈ SProd.sprod (β := Set F) e.baseSet univ

Tactic:
simp [e.target_eq]

Premises used: Bundle.Pretrivialization.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
e_1 : Pretrivialization F proj
x : Z
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
s : Set B
e : Pretrivialization.{u_1, u_2, u_4} (B := B) F fun (z : (↑(proj ⁻¹' s) : Type u_4)) ↦ proj (↑z : Z)
inst_2 : Nonempty (Z → F)
z : Z
hzp : proj z ∈ s
hze : Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) z hzp ∈ e.source
⊢ (if h : proj (↑(Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) z hzp) : Z) ∈ s then
        (↑e : (↑(proj ⁻¹' s) : Type u_4) → B × F)
          (Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) (↑(Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) z hzp) : Z)
            h)
      else
        (proj (↑(Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) z hzp) : Z),
          Classical.arbitrary (Z → F) (↑(Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) z hzp) : Z))).1 =
    proj (↑(Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) z hzp) : Z)

Tactic:
simp [hzp, e.coe_fst hze]

Premises used: Bundle.Pretrivialization.coe_fst
-- 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_1 : Z → B
e_1 : Pretrivialization F proj_1
x_1 : Z
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
s : Set B
hs : IsOpen[inst] s
proj : Z → (↑s : Type u_1)
e : Pretrivialization F proj
inst_2 : Nonempty (B → F → Z)
x : B × F
⊢ Z

Tactic:
exact if h : x.1 ∈ s then e.invFun (⟨x.1, h⟩, x.2)
    else Classical.arbitrary (B → F → Z) x.1 x.2

Premises used: Prod.fst, Classical.arbitrary, Prod.snd
-- 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_1 : Z → B
e_1 : Pretrivialization F proj_1
x_1 : Z
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
s : Set B
hs : IsOpen[inst] s
proj : Z → (↑s : Type u_1)
e : Pretrivialization F proj
inst_2 : Nonempty (B → F → Z)
x : B × F
⊢ Z

Tactic:
classical exact if h : x.1 ∈ s then e.invFun (⟨x.1, h⟩, x.2)
    else Classical.arbitrary (B → F → Z) x.1 x.2

Premises used: Prod.fst, Classical.arbitrary, Prod.snd
-- 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_1 : Z → B
e_1 : Pretrivialization F proj_1
x : Z
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
s : Set B
hs : IsOpen[inst] s
proj : Z → (↑s : Type u_1)
e : Pretrivialization F proj
inst_2 : Nonempty (B → F → Z)
z : Z
hz : z ∈ e.source
⊢ ((↑((↑e : Z → (↑s : Type u_1) × F) z).1 : B), ((↑e : Z → (↑s : Type u_1) × F) z).2) ∈
    Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id '' e.target

Tactic:
simpa using e.map_source hz

Premises used: PartialEquiv.map_source, Bundle.Pretrivialization.toPartialEquiv
-- 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_1 : Z → B
e_1 : Pretrivialization F proj_1
x_1 : Z
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
s : Set B
hs : IsOpen[inst] s
proj : Z → (↑s : Type u_1)
e : Pretrivialization F proj
inst_2 : Nonempty (B → F → Z)
x : Prod.{u_1, u_2} { x : B // x ∈ s } F
hx : x ∈ e.target
⊢ (if h : (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1 ∈ s then
      e.invFun
        (Subtype.mk (p := fun (x : B) ↦ x ∈ s) (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1 h,
          (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).2)
    else
      Classical.arbitrary (B → F → Z) (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1
        (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).2) ∈
    e.source

Tactic:
simpa using e.map_target hx

Premises used: PartialEquiv.map_target, Bundle.Pretrivialization.toPartialEquiv
-- 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_1 : Z → B
e_1 : Pretrivialization F proj_1
x : Z
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
s : Set B
hs : IsOpen[inst] s
proj : Z → (↑s : Type u_1)
e : Pretrivialization F proj
inst_2 : Nonempty (B → F → Z)
z : Z
hz : z ∈ e.source
⊢ (if h : ((↑((↑e : Z → (↑s : Type u_1) × F) z).1 : B), ((↑e : Z → (↑s : Type u_1) × F) z).2).1 ∈ s then
      e.invFun
        (Subtype.mk (p := fun (x : B) ↦ x ∈ s)
            ((↑((↑e : Z → (↑s : Type u_1) × F) z).1 : B), ((↑e : Z → (↑s : Type u_1) × F) z).2).1 h,
          ((↑((↑e : Z → (↑s : Type u_1) × F) z).1 : B), ((↑e : Z → (↑s : Type u_1) × F) z).2).2)
    else
      Classical.arbitrary (B → F → Z)
        ((↑((↑e : Z → (↑s : Type u_1) × F) z).1 : B), ((↑e : Z → (↑s : Type u_1) × F) z).2).1
        ((↑((↑e : Z → (↑s : Type u_1) × F) z).1 : B), ((↑e : Z → (↑s : Type u_1) × F) z).2).2) =
    z

Tactic:
simpa using e.left_inv hz

Premises used: Bundle.Pretrivialization.toPartialEquiv, PartialEquiv.left_inv
-- 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_1 : Z → B
e_1 : Pretrivialization F proj_1
x_1 : Z
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
s : Set B
hs : IsOpen[inst] s
proj : Z → (↑s : Type u_1)
e : Pretrivialization F proj
inst_2 : Nonempty (B → F → Z)
x : Prod.{u_1, u_2} { x : B // x ∈ s } F
hx : x ∈ e.target
⊢ ((↑((↑e : Z → (↑s : Type u_1) × F)
                (if h : (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1 ∈ s then
                  e.invFun
                    (Subtype.mk (p := fun (x : B) ↦ x ∈ s) (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1 h,
                      (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).2)
                else
                  Classical.arbitrary (B → F → Z) (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1
                    (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).2)).1 :
          B),
        ((↑e : Z → (↑s : Type u_1) × F)
            (if h : (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1 ∈ s then
              e.invFun
                (Subtype.mk (p := fun (x : B) ↦ x ∈ s) (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1 h,
                  (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).2)
            else
              Classical.arbitrary (B → F → Z) (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1
                (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).2)).2).1 =
    (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1

Tactic:
simp [e.apply_symm_apply hx]

Premises used: Bundle.Pretrivialization.apply_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_1 : Z → B
e_1 : Pretrivialization F proj_1
x_1 : Z
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
s : Set B
hs : IsOpen[inst] s
proj : Z → (↑s : Type u_1)
e : Pretrivialization F proj
inst_2 : Nonempty (B → F → Z)
x : Prod.{u_1, u_2} { x : B // x ∈ s } F
hx : x ∈ e.target
⊢ ((↑((↑e : Z → (↑s : Type u_1) × F)
                (if h : (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1 ∈ s then
                  e.invFun
                    (Subtype.mk (p := fun (x : B) ↦ x ∈ s) (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1 h,
                      (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).2)
                else
                  Classical.arbitrary (B → F → Z) (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1
                    (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).2)).1 :
          B),
        ((↑e : Z → (↑s : Type u_1) × F)
            (if h : (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1 ∈ s then
              e.invFun
                (Subtype.mk (p := fun (x : B) ↦ x ∈ s) (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1 h,
                  (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).2)
            else
              Classical.arbitrary (B → F → Z) (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).1
                (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).2)).2).2 =
    (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x).2

Tactic:
simp [e.apply_symm_apply hx]

Premises used: Bundle.Pretrivialization.apply_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_1 : Z → B
e_1 : Pretrivialization F proj_1
x : Z
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
s : Set B
hs : IsOpen[inst] s
proj : Z → (↑s : Type u_1)
e : Pretrivialization F proj
inst_2 : Nonempty (B → F → Z)
h :
  ∀ (x : Z),
    x ∈ e.source ↔
      x ∈ Subtype.val (p := fun (x : B) ↦ x ∈ s) ∘ proj ⁻¹' Subtype.val (p := fun (x : B) ↦ x ∈ s) '' e.baseSet
⊢ e.source = Subtype.val (p := fun (x : B) ↦ x ∈ s) ∘ proj ⁻¹' Subtype.val (p := fun (x : B) ↦ x ∈ s) '' 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_1 : Z → B
e_1 : Pretrivialization F proj_1
x : Z
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
s : Set B
hs : IsOpen[inst] s
proj : Z → (↑s : Type u_1)
e : Pretrivialization F proj
inst_2 : Nonempty (B → F → Z)
x_1 : Z
⊢ x_1 ∈ e.source ↔
    x_1 ∈ Subtype.val (p := fun (x : B) ↦ x ∈ s) ∘ proj ⁻¹' Subtype.val (p := fun (x : B) ↦ x ∈ s) '' e.baseSet

Tactic:
simp [e.source_eq]

Premises used: Bundle.Pretrivialization.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_1 : Z → B
e_1 : Pretrivialization F proj_1
x : Z
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
s : Set B
hs : IsOpen[inst] s
proj : Z → (↑s : Type u_1)
e : Pretrivialization F proj
inst_2 : Nonempty (B → F → Z)
rw :
  Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id '' SProd.sprod (β := Set F) e.baseSet univ =
    SProd.sprod (β := Set F) (Subtype.val (p := fun (x : B) ↦ x ∈ s) '' e.baseSet) univ
rw₁ :
  SProd.sprod (β := Set F) (Subtype.val (p := fun (x : B) ↦ x ∈ s) '' e.baseSet) (id '' univ) =
    SProd.sprod (β := Set F) (Subtype.val (p := fun (x : B) ↦ x ∈ s) '' e.baseSet) univ
rw₂ rw₃ :
  SProd.sprod (β := Set F) (Subtype.val (p := fun (x : B) ↦ x ∈ s) '' e.baseSet) univ =
    SProd.sprod (β := Set F) (Subtype.val (p := fun (x : B) ↦ x ∈ s) '' e.baseSet) univ
⊢ Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id '' e.target =
    SProd.sprod (β := Set F) (Subtype.val (p := fun (x : B) ↦ x ∈ s) '' e.baseSet) univ

Tactic:
rw [e.target_eq, prodMap_image_prod, image_id]

Premises used: Set.prodMap_image_prod, Bundle.Pretrivialization.target_eq, Set.image_id
-- 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_1 : Z → B
e_1 : Pretrivialization F proj_1
x : Z
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
s : Set B
hs : IsOpen[inst] s
proj : Z → (↑s : Type u_1)
e : Pretrivialization F proj
inst_2 : Nonempty (B → F → Z)
x_1 : Z
h : x_1 ∈ e.source
⊢ ((↑((↑e : Z → (↑s : Type u_1) × F) x_1).1 : B), ((↑e : Z → (↑s : Type u_1) × F) x_1).2).1 =
    (Subtype.val (p := fun (x : B) ↦ x ∈ s) ∘ proj) x_1

Tactic:
simp [e.coe_fst h]

Premises used: Bundle.Pretrivialization.coe_fst
-- 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
h₁ : e.toOpenPartialHomeomorph = e'.toOpenPartialHomeomorph
h₂ : e.baseSet = e'.baseSet
mk :
  ∀ (toOpenPartialHomeomorph : OpenPartialHomeomorph Z (B × F)) (baseSet : Set B) (open_baseSet : IsOpen[inst] baseSet)
    (source_eq : toOpenPartialHomeomorph.source = proj ⁻¹' baseSet)
    (target_eq : toOpenPartialHomeomorph.target = SProd.sprod (β := Set F) baseSet univ)
    (proj_toFun : ∀ p ∈ toOpenPartialHomeomorph.source, ((↑toOpenPartialHomeomorph : Z → B × F) 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 :
            Trivialization F proj }.toOpenPartialHomeomorph =
        e'.toOpenPartialHomeomorph)
    (h₂ :
      { toOpenPartialHomeomorph := toOpenPartialHomeomorph, baseSet := baseSet, open_baseSet := open_baseSet,
            source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun : Trivialization F proj }.baseSet =
        e'.baseSet),
    { toOpenPartialHomeomorph := toOpenPartialHomeomorph, baseSet := baseSet, open_baseSet := open_baseSet,
        source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun : Trivialization 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
inst_2 : TopologicalSpace Z
toOpenPartialHomeomorph : OpenPartialHomeomorph Z (B × F)
baseSet : Set B
open_baseSet : IsOpen[inst] baseSet
source_eq : toOpenPartialHomeomorph.source = proj ⁻¹' baseSet
target_eq : toOpenPartialHomeomorph.target = SProd.sprod (β := Set F) baseSet univ
proj_toFun : ∀ p ∈ toOpenPartialHomeomorph.source, ((↑toOpenPartialHomeomorph : Z → B × F) p).1 = proj p
toOpenPartialHomeomorph_1 : OpenPartialHomeomorph Z (B × F)
baseSet_1 : Set B
open_baseSet_1 : IsOpen[inst] baseSet_1
source_eq_1 : toOpenPartialHomeomorph_1.source = proj ⁻¹' baseSet_1
target_eq_1 : toOpenPartialHomeomorph_1.target = SProd.sprod (β := Set F) baseSet_1 univ
proj_toFun_1 : ∀ p ∈ toOpenPartialHomeomorph_1.source, ((↑toOpenPartialHomeomorph_1 : Z → B × F) 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 :
        Trivialization F proj }.toOpenPartialHomeomorph =
    { toOpenPartialHomeomorph := toOpenPartialHomeomorph_1, baseSet := baseSet_1, open_baseSet := open_baseSet_1,
        source_eq := source_eq_1, target_eq := target_eq_1, proj_toFun := proj_toFun_1 :
        Trivialization F proj }.toOpenPartialHomeomorph
h₂ :
  { toOpenPartialHomeomorph := toOpenPartialHomeomorph, baseSet := baseSet, open_baseSet := open_baseSet,
        source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun : Trivialization F proj }.baseSet =
    { toOpenPartialHomeomorph := toOpenPartialHomeomorph_1, baseSet := baseSet_1, open_baseSet := open_baseSet_1,
        source_eq := source_eq_1, target_eq := target_eq_1, proj_toFun := proj_toFun_1 : Trivialization F proj }.baseSet
⊢ { toOpenPartialHomeomorph := toOpenPartialHomeomorph, baseSet := baseSet, open_baseSet := open_baseSet,
      source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun : Trivialization F proj } =
    { toOpenPartialHomeomorph := toOpenPartialHomeomorph_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
inst_2 : TopologicalSpace Z
e e' : Trivialization F proj
h :
  Eq (α := Pretrivialization F proj) ((fun (e : Trivialization F proj) ↦ e.toPretrivialization) e)
    ((fun (e : Trivialization F proj) ↦ e.toPretrivialization) e')
h₁ : e.toOpenPartialHomeomorph = e'.toOpenPartialHomeomorph
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
inst_2 : TopologicalSpace Z
e e' : Trivialization F proj
h :
  Eq (α := Pretrivialization F proj) ((fun (e : Trivialization F proj) ↦ e.toPretrivialization) e)
    ((fun (e : Trivialization F proj) ↦ e.toPretrivialization) e')
⊢ e.toOpenPartialHomeomorph = e'.toOpenPartialHomeomorph

Tactic:
OpenPartialHomeomorph.toPartialEquiv_injective
    (congr_arg Pretrivialization.toPartialEquiv h)

Premises used: OpenPartialHomeomorph.toPartialEquiv_injective, congr_arg, Bundle.Pretrivialization.toPartialEquiv
-- 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
h :
  Eq (α := Pretrivialization F proj) ((fun (e : Trivialization F proj) ↦ e.toPretrivialization) e)
    ((fun (e : Trivialization F proj) ↦ e.toPretrivialization) e')
⊢ e.baseSet = e'.baseSet

Tactic:
congr_arg Pretrivialization.baseSet h

Premises used: congr_arg, Bundle.Pretrivialization.baseSet
-- 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
h :
  Eq (α := Pretrivialization F proj) ((fun (e : Trivialization F proj) ↦ e.toPretrivialization) e)
    ((fun (e : Trivialization F proj) ↦ e.toPretrivialization) e')
⊢ e.toOpenPartialHomeomorph = e'.toOpenPartialHomeomorph

Tactic:
exacts [OpenPartialHomeomorph.toPartialEquiv_injective
    (congr_arg Pretrivialization.toPartialEquiv h), congr_arg Pretrivialization.baseSet h]

Premises used: OpenPartialHomeomorph.toPartialEquiv_injective, congr_arg, Bundle.Pretrivialization.toPartialEquiv, Bundle.Pretrivialization.baseSet
-- 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
⊢ (↑e.toOpenPartialHomeomorph : Z → B × F) = (↑e : Z → B × F)

Tactic:
rfl

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

Tactic:
e.proj_toFun x ex

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
e : Trivialization F proj
⊢ EqOn (Prod.fst ∘ (↑e : Z → B × F)) proj e.source

Tactic:
fun _x hx => e.coe_fst hx

Premises used: Bundle.Trivialization.coe_fst, Set.EqOn
-- 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
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.Trivialization.source_eq, Set.mem_preimage