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
e : Pretrivialization F proj
s : Set B
inst_2 : Nonempty ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
z : (↑(proj ⁻¹' s) : Type u_4)
hz :
  Membership.mem (γ := Set (↑(proj ⁻¹' s) : Type u_4)) (Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) ⁻¹' e.source) z
⊢ Membership.mem (γ := Set (Prod.{u_1, u_2} (↑s : Type u_1) F))
    (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id ⁻¹' e.target)
    (Subtype.mk (p := fun (x : B) ↦ x ∈ s) (proj (↑z : Z)) ⋯, ((↑e : Z → B × F) (↑z : Z)).2)

Tactic:
simpa only [Prod.map_apply, ← e.proj_toFun _ hz] using e.map_source' hz

Premises used: PartialEquiv.map_source', Bundle.Pretrivialization.toPartialEquiv, Prod.map_apply, Bundle.Pretrivialization.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
e_1 : Pretrivialization F proj
x_1 : Z
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e : Pretrivialization F proj
s : Set B
inst_2 : Nonempty ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
x : Prod.{u_1, u_2} (↑s : Type u_1) F
hx :
  Membership.mem (γ := Set (Prod.{u_1, u_2} (↑s : Type u_1) F))
    (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id ⁻¹' e.target) x
⊢ ((↑x.1 : B), x.2) ∈ e.target

Tactic:
simp only [mem_preimage, (Prod.map_apply), id_eq] at hx

Premises used: Prod.map_apply, Set.mem_preimage, id_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_1 : Z
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e : Pretrivialization F proj
s : Set B
inst_2 : Nonempty ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
x : Prod.{u_1, u_2} (↑s : Type u_1) F
hx : ((↑x.1 : B), x.2) ∈ e.target
rw :
  Membership.mem (γ := Set (↑(proj ⁻¹' s) : Type u_4)) (Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) ⁻¹' e.source)
    (Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) (e.invFun ((↑x.1 : B), x.2)) ⋯)
⊢ Membership.mem (γ := Set (↑(proj ⁻¹' s) : Type u_4)) (Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) ⁻¹' e.source)
    (if h : ((↑x.1 : B), x.2) ∈ e.target then
      Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) (e.invFun ((↑x.1 : B), x.2)) ⋯
    else Classical.arbitrary ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4)) x.1 x.2)

Tactic:
rw [dif_pos hx]

Premises used: dif_pos
-- 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_1 : Z
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e : Pretrivialization F proj
s : Set B
inst_2 : Nonempty ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
x : Prod.{u_1, u_2} (↑s : Type u_1) F
hx : ((↑x.1 : B), x.2) ∈ e.target
⊢ Membership.mem (γ := Set (↑(proj ⁻¹' s) : Type u_4)) (Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) ⁻¹' e.source)
    (Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) (e.invFun ((↑x.1 : B), x.2)) ⋯)

Tactic:
e.map_target' hx

Premises used: Set.Mem, setOf, Set.preimage, Bundle.Pretrivialization.toPartialEquiv, PartialEquiv.map_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
e_1 : Pretrivialization F proj
x_1 : Z
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e : Pretrivialization F proj
s : Set B
inst_2 : Nonempty ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
x : Prod.{u_1, u_2} (↑s : Type u_1) F
hx : ((↑x.1 : B), x.2) ∈ e.target
⊢ Membership.mem (γ := Set (↑(proj ⁻¹' s) : Type u_4)) (Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) ⁻¹' e.source)
    (Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) (e.invFun ((↑x.1 : B), x.2)) ⋯)

Tactic:
exact e.map_target' hx

Premises used: Bundle.Pretrivialization.toPartialEquiv, PartialEquiv.map_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
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
e : Pretrivialization F proj
s : Set B
inst_2 : Nonempty ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
z : (↑(proj ⁻¹' s) : Type u_4)
hz :
  Membership.mem (γ := Set (↑(proj ⁻¹' s) : Type u_4)) (Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) ⁻¹' e.source) z
dsimp :
  (if h : (proj (↑z : Z), ((↑e : Z → B × F) (↑z : Z)).2) ∈ e.target then
      Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) (e.invFun (proj (↑z : Z), ((↑e : Z → B × F) (↑z : Z)).2)) ⋯
    else
      Classical.arbitrary ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
        (Subtype.mk (p := fun (x : B) ↦ x ∈ s) (proj (↑z : Z)) ⋯) ((↑e : Z → B × F) (↑z : Z)).2) =
    z
⊢ (if h :
        ((↑(Subtype.mk (p := fun (x : B) ↦ x ∈ s) (proj (↑z : Z)) ⋯, ((↑e : Z → B × F) (↑z : Z)).2).1 : B),
            (Subtype.mk (p := fun (x : B) ↦ x ∈ s) (proj (↑z : Z)) ⋯, ((↑e : Z → B × F) (↑z : Z)).2).2) ∈
          e.target then
      Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s)
        (e.invFun
          ((↑(Subtype.mk (p := fun (x : B) ↦ x ∈ s) (proj (↑z : Z)) ⋯, ((↑e : Z → B × F) (↑z : Z)).2).1 : B),
            (Subtype.mk (p := fun (x : B) ↦ x ∈ s) (proj (↑z : Z)) ⋯, ((↑e : Z → B × F) (↑z : Z)).2).2))
        ⋯
    else
      Classical.arbitrary ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
        (Subtype.mk (p := fun (x : B) ↦ x ∈ s) (proj (↑z : Z)) ⋯, ((↑e : Z → B × F) (↑z : Z)).2).1
        (Subtype.mk (p := fun (x : B) ↦ x ∈ s) (proj (↑z : Z)) ⋯, ((↑e : Z → B × F) (↑z : Z)).2).2) =
    z

Tactic:
dsimp only
-- 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
e : Pretrivialization F proj
s : Set B
inst_2 : Nonempty ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
z : (↑(proj ⁻¹' s) : Type u_4)
hz :
  Membership.mem (γ := Set (↑(proj ⁻¹' s) : Type u_4)) (Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) ⁻¹' e.source) z
rw : Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) (e.invFun (proj (↑z : Z), ((↑e : Z → B × F) (↑z : Z)).2)) ⋯ = z
hc : (proj (↑z : Z), ((↑e : Z → B × F) (↑z : Z)).2) ∈ e.target
⊢ (if h : (proj (↑z : Z), ((↑e : Z → B × F) (↑z : Z)).2) ∈ e.target then
      Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) (e.invFun (proj (↑z : Z), ((↑e : Z → B × F) (↑z : Z)).2)) ⋯
    else
      Classical.arbitrary ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
        (Subtype.mk (p := fun (x : B) ↦ x ∈ s) (proj (↑z : Z)) ⋯) ((↑e : Z → B × F) (↑z : Z)).2) =
    z

Tactic:
rw [dif_pos]

Premises used: dif_pos
-- 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
e : Pretrivialization F proj
s : Set B
inst_2 : Nonempty ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
z : (↑(proj ⁻¹' s) : Type u_4)
hz :
  Membership.mem (γ := Set (↑(proj ⁻¹' s) : Type u_4)) (Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) ⁻¹' e.source) z
simp_rw :
  Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s)
      (e.invFun (((↑e.toPartialEquiv : Z → B × F) (↑z : Z)).1, ((↑e : Z → B × F) (↑z : Z)).2)) ⋯ =
    z
⊢ Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) (e.invFun (proj (↑z : Z), ((↑e : Z → B × F) (↑z : Z)).2)) ⋯ = z

Tactic:
simp_rw [← e.proj_toFun _ hz]

Premises used: Bundle.Pretrivialization.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
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
e : Pretrivialization F proj
s : Set B
inst_2 : Nonempty ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
z : (↑(proj ⁻¹' s) : Type u_4)
hz :
  Membership.mem (γ := Set (↑(proj ⁻¹' s) : Type u_4)) (Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) ⁻¹' e.source) z
all_goals :
  Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s)
      (e.invFun (((↑e.toPartialEquiv : Z → B × F) (↑z : Z)).1, ((↑e : Z → B × F) (↑z : Z)).2)) ⋯ =
    z
⊢ Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) (e.invFun (proj (↑z : Z), ((↑e : Z → B × F) (↑z : Z)).2)) ⋯ = z

Tactic:
all_goals simp_rw [← e.proj_toFun _ hz]

Premises used: Bundle.Pretrivialization.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
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
e : Pretrivialization F proj
s : Set B
inst_2 : Nonempty ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
z : (↑(proj ⁻¹' s) : Type u_4)
hz :
  Membership.mem (γ := Set (↑(proj ⁻¹' s) : Type u_4)) (Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) ⁻¹' e.source) z
hc : (((↑e.toPartialEquiv : Z → B × F) (↑z : Z)).1, ((↑e : Z → B × F) (↑z : Z)).2) ∈ e.target
⊢ (proj (↑z : Z), ((↑e : Z → B × F) (↑z : Z)).2) ∈ e.target

Tactic:
simp_rw [← e.proj_toFun _ hz]

Premises used: Bundle.Pretrivialization.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
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
e : Pretrivialization F proj
s : Set B
inst_2 : Nonempty ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
z : (↑(proj ⁻¹' s) : Type u_4)
hz :
  Membership.mem (γ := Set (↑(proj ⁻¹' s) : Type u_4)) (Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) ⁻¹' e.source) z
hc : (((↑e.toPartialEquiv : Z → B × F) (↑z : Z)).1, ((↑e : Z → B × F) (↑z : Z)).2) ∈ e.target
⊢ (proj (↑z : Z), ((↑e : Z → B × F) (↑z : Z)).2) ∈ e.target

Tactic:
all_goals simp_rw [← e.proj_toFun _ hz]

Premises used: Bundle.Pretrivialization.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
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
e : Pretrivialization F proj
s : Set B
inst_2 : Nonempty ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
z : (↑(proj ⁻¹' s) : Type u_4)
hz :
  Membership.mem (γ := Set (↑(proj ⁻¹' s) : Type u_4)) (Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) ⁻¹' e.source) z
⊢ Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s)
      (e.invFun (((↑e.toPartialEquiv : Z → B × F) (↑z : Z)).1, ((↑e : Z → B × F) (↑z : Z)).2)) ⋯ =
    z

Tactic:
Subtype.ext (e.left_inv' hz)

Premises used: PartialEquiv.left_inv', Bundle.Pretrivialization.toPartialEquiv, Subtype.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
e : Pretrivialization F proj
s : Set B
inst_2 : Nonempty ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
z : (↑(proj ⁻¹' s) : Type u_4)
hz :
  Membership.mem (γ := Set (↑(proj ⁻¹' s) : Type u_4)) (Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) ⁻¹' e.source) z
⊢ (((↑e.toPartialEquiv : Z → B × F) (↑z : Z)).1, ((↑e : Z → B × F) (↑z : Z)).2) ∈ e.target

Tactic:
e.map_source' hz

Premises used: PartialEquiv.map_source', Set.Mem, 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 : 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
e : Pretrivialization F proj
s : Set B
inst_2 : Nonempty ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
z : (↑(proj ⁻¹' s) : Type u_4)
hz :
  Membership.mem (γ := Set (↑(proj ⁻¹' s) : Type u_4)) (Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) ⁻¹' e.source) z
⊢ Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s)
      (e.invFun (((↑e.toPartialEquiv : Z → B × F) (↑z : Z)).1, ((↑e : Z → B × F) (↑z : Z)).2)) ⋯ =
    z

Tactic:
exacts [Subtype.ext (e.left_inv' hz), e.map_source' hz]

Premises used: PartialEquiv.map_source', Bundle.Pretrivialization.toPartialEquiv, Subtype.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_1 : Z
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e : Pretrivialization F proj
s : Set B
inst_2 : Nonempty ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
x : Prod.{u_1, u_2} (↑s : Type u_1) F
hx : ((↑x.1 : B), x.2) ∈ e.target
simp_rw :
  (proj
        (↑(if h : ((↑x.1 : B), x.2) ∈ e.target then
              Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) (e.invFun ((↑x.1 : B), x.2)) ⋯
            else Classical.arbitrary ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4)) x.1 x.2) :
          Z),
      id
        ((↑e : Z → B × F)
            (↑(if h : ((↑x.1 : B), x.2) ∈ e.target then
                  Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) (e.invFun ((↑x.1 : B), x.2)) ⋯
                else Classical.arbitrary ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4)) x.1 x.2) :
              Z)).2) =
    Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x
⊢ Prod.map (α₁ := { x : B // x ∈ s }) (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id
      (Subtype.mk (p := fun (x : B) ↦ x ∈ s)
          (proj
            (↑(if h : ((↑x.1 : B), x.2) ∈ e.target then
                  Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) (e.invFun ((↑x.1 : B), x.2)) ⋯
                else Classical.arbitrary ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4)) x.1 x.2) :
              Z))
          ⋯,
        ((↑e : Z → B × F)
            (↑(if h : ((↑x.1 : B), x.2) ∈ e.target then
                  Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) (e.invFun ((↑x.1 : B), x.2)) ⋯
                else Classical.arbitrary ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4)) x.1 x.2) :
              Z)).2) =
    Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x

Tactic:
simp_rw [Prod.map_apply]

Premises used: Prod.map_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_1 : Z
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e : Pretrivialization F proj
s : Set B
inst_2 : Nonempty ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
x : Prod.{u_1, u_2} (↑s : Type u_1) F
hx : ((↑x.1 : B), x.2) ∈ e.target
rw :
  (proj (↑(Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) (e.invFun ((↑x.1 : B), x.2)) ⋯) : Z),
      id ((↑e : Z → B × F) (↑(Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) (e.invFun ((↑x.1 : B), x.2)) ⋯) : Z)).2) =
    Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x
⊢ (proj
        (↑(if h : ((↑x.1 : B), x.2) ∈ e.target then
              Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) (e.invFun ((↑x.1 : B), x.2)) ⋯
            else Classical.arbitrary ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4)) x.1 x.2) :
          Z),
      id
        ((↑e : Z → B × F)
            (↑(if h : ((↑x.1 : B), x.2) ∈ e.target then
                  Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) (e.invFun ((↑x.1 : B), x.2)) ⋯
                else Classical.arbitrary ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4)) x.1 x.2) :
              Z)).2) =
    Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x

Tactic:
rw [dif_pos hx]

Premises used: dif_pos
-- 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_1 : Z
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e : Pretrivialization F proj
s : Set B
inst_2 : Nonempty ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
x : Prod.{u_1, u_2} (↑s : Type u_1) F
hx : ((↑x.1 : B), x.2) ∈ e.target
⊢ (↑e.toPartialEquiv : Z → B × F) (e.invFun ((↑x.1 : B), x.2)) = ((↑x.1 : B), x.2)

Tactic:
e.right_inv' hx

Premises used: PartialEquiv.right_inv', 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 : Z → B
e_1 : Pretrivialization F proj
x_1 : Z
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e : Pretrivialization F proj
s : Set B
inst_2 : Nonempty ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
x : Prod.{u_1, u_2} (↑s : Type u_1) F
hx : ((↑x.1 : B), x.2) ∈ e.target
h :
  (e.toPartialEquiv.1 (e.invFun ((↑x.1 : B), x.2))).1 =
    proj (↑(Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) (e.invFun ((↑x.1 : B), x.2)) ⋯) : Z)
⊢ (proj (↑(Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) (e.invFun ((↑x.1 : B), x.2)) ⋯) : Z),
      id ((↑e : Z → B × F) (↑(Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) (e.invFun ((↑x.1 : B), x.2)) ⋯) : Z)).2) =
    Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x

Tactic:
convert! ← e.right_inv' hx

Premises used: PartialEquiv.right_inv', 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 : Z → B
e_1 : Pretrivialization F proj
x_1 : Z
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e : Pretrivialization F proj
s : Set B
inst_2 : Nonempty ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
x : Prod.{u_1, u_2} (↑s : Type u_1) F
hx : ((↑x.1 : B), x.2) ∈ e.target
⊢ (e.toPartialEquiv.1 (e.invFun ((↑x.1 : B), x.2))).1 =
    proj (↑(Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) (e.invFun ((↑x.1 : B), x.2)) ⋯) : Z)

Tactic:
e.proj_toFun _ (e.map_target' hx)

Premises used: Bundle.Pretrivialization.toPartialEquiv, Bundle.Pretrivialization.proj_toFun, PartialEquiv.map_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
e_1 : Pretrivialization F proj
x_1 : Z
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e : Pretrivialization F proj
s : Set B
inst_2 : Nonempty ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
x : Prod.{u_1, u_2} (↑s : Type u_1) F
hx : ((↑x.1 : B), x.2) ∈ e.target
⊢ (e.toPartialEquiv.1 (e.invFun ((↑x.1 : B), x.2))).1 =
    proj (↑(Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) (e.invFun ((↑x.1 : B), x.2)) ⋯) : Z)

Tactic:
exact e.proj_toFun _ (e.map_target' hx)

Premises used: Bundle.Pretrivialization.toPartialEquiv, Bundle.Pretrivialization.proj_toFun, PartialEquiv.map_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
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
e : Pretrivialization F proj
s : Set B
inst_2 : Nonempty ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id)

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
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
⊢ B × F

Tactic:
exact if h : proj z ∈ s then e ⟨z, h⟩
    else (proj z, Classical.arbitrary (Z → F) z)

Premises used: Prod.mk, Classical.arbitrary
-- 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
⊢ B × F

Tactic:
classical exact if h : proj z ∈ s then e ⟨z, h⟩
    else (proj z, Classical.arbitrary (Z → F) z)

Premises used: Prod.mk, Classical.arbitrary
-- 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))) ∈
    e.target

Tactic:
simpa [hzp, e.coe_fst hze] using e.map_source hze

Premises used: PartialEquiv.map_source, Bundle.Pretrivialization.toPartialEquiv, 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 : Z → B
e_1 : Pretrivialization F proj
x_1 : 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 : B × F
hx : x ∈ e.target
⊢ (↑(e.invFun x) : Z) ∈ Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) '' e.source

Tactic:
simpa using ⟨(e.invFun x).2, e.map_target hx⟩