awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
⊢ (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
have 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)) sorry
  else
    Classical.arbitrary ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
      (Subtype.mk (p := fun (x : B) ↦ x ∈ s) (proj (↑z : Z)) sorry) ((↑e : Z → B × F) (↑z : Z)).2) =
  z
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
⊢ (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
have rw : Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) (e.invFun (proj (↑z : Z), ((↑e : Z → B × F) (↑z : Z)).2)) sorry = z
Tactic: rw [dif_pos]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
⊢ (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
have hc : (proj (↑z : Z), ((↑e : Z → B × F) (↑z : Z)).2) ∈ e.target
Tactic: rw [dif_pos]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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 (proj (↑z : Z), ((↑e : Z → B × F) (↑z : Z)).2)) ⋯ = z
have 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)) sorry =
  z
Tactic: simp_rw [← e.proj_toFun _ hz]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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 (proj (↑z : Z), ((↑e : Z → B × F) (↑z : Z)).2)) ⋯ = z
have 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)) sorry =
  z
Tactic: all_goals simp_rw [← e.proj_toFun _ hz]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
⊢ (proj (↑z : Z), ((↑e : Z → B × F) (↑z : Z)).2) ∈ e.target
have hc : (((↑e.toPartialEquiv : Z → B × F) (↑z : Z)).1, ((↑e : Z → B × F) (↑z : Z)).2) ∈ e.target
Tactic: simp_rw [← e.proj_toFun _ hz]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
⊢ (proj (↑z : Z), ((↑e : Z → B × F) (↑z : Z)).2) ∈ e.target
have hc : (((↑e.toPartialEquiv : Z → B × F) (↑z : Z)).1, ((↑e : Z → B × F) (↑z : Z)).2) ∈ e.target
Tactic: all_goals simp_rw [← e.proj_toFun _ hz]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (hypothesis)
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
⊢ 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
have hx₁ : ((↑x.1 : B), x.2) ∈ e.target
Tactic: simp only [mem_preimage, (Prod.map_apply), id_eq] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
⊢ 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
have 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)) sorry
          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)) sorry
              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]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
⊢ (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
have rw : (proj (↑(Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) (e.invFun ((↑x.1 : B), x.2)) sorry) : Z),
    id ((↑e : Z → B × F) (↑(Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) (e.invFun ((↑x.1 : B), x.2)) sorry) : Z)).2) =
  Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x
Tactic: rw [dif_pos hx]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
⊢ (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
have 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)) sorry) : Z)
Tactic: convert! ← e.right_inv' hx
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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)
⊢ Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) '' e.source = proj ⁻¹' e.baseSet
have h : ∀ (z : Z), z ∈ Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) '' e.source ↔ z ∈ proj ⁻¹' e.baseSet
Tactic: ext z
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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)
⊢ e.target = SProd.sprod (β := Set F) e.baseSet univ
have h : ∀ (x : B × F), x ∈ e.target ↔ x ∈ SProd.sprod (β := Set F) e.baseSet univ
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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) =
    Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id x
have fst : ((↑((↑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: ext
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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)
⊢ e.source = Subtype.val (p := fun (x : B) ↦ x ∈ s) ∘ proj ⁻¹' Subtype.val (p := fun (x : B) ↦ x ∈ s) '' e.baseSet
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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)
⊢ 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
have 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
Tactic: rw [e.target_eq, prodMap_image_prod, image_id]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
⊢ 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
have 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
Tactic: rw [e.target_eq, prodMap_image_prod, image_id]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
⊢ 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
have 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
Tactic: rw [e.target_eq, prodMap_image_prod, image_id]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
⊢ e = e'
have 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'
Tactic: cases e
Cleared hypotheses: e, h₁, h₂
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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 = e'
have h₁ : e.toOpenPartialHomeomorph = e'.toOpenPartialHomeomorph
Tactic: ext1
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
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
⊢ e = e'
have h₂ : e.baseSet = e'.baseSet
Tactic: ext1