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
Z : Type u_4
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x : B × F
hx : x ∈ e.target
⊢ x ∈ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' e.baseSet
have simp : x.1 ∈ e.baseSet
Tactic: simp only [mem_preimage, e.proj_symm_apply hx]
-- 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
e : Pretrivialization F proj
s : Set B
⊢ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' s ∩ SProd.sprod (β := Set F) e.baseSet univ =
    SProd.sprod (β := Set F) (s ∩ e.baseSet) univ
have h : ∀ (x : B) (y : F),
  (x, y) ∈ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' s ∩ SProd.sprod (β := Set F) e.baseSet univ ↔
    (x, y) ∈ SProd.sprod (β := Set F) (s ∩ e.baseSet) univ
Tactic: ext ⟨x, y⟩
-- 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
e : Pretrivialization F proj
s : Set B
x : B
y : F
⊢ (x, y) ∈ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' s ∩ SProd.sprod (β := Set F) e.baseSet univ ↔
    (x, y) ∈ SProd.sprod (β := Set F) (s ∩ e.baseSet) univ
have h : x ∈ e.baseSet → (proj ((↑e.symm : B × F → Z) (x, y)) ∈ s ↔ x ∈ s)
Tactic: suffices x ∈ e.baseSet → (proj (e.toPartialEquiv.symm (x, y)) ∈ s ↔ x ∈ s) by
    simpa only [prodMk_mem_set_prod_eq, mem_inter_iff, and_true, mem_univ, and_congr_left_iff]
-- 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
e : Pretrivialization F proj
s : Set B
x : B
y : F
h : x ∈ e.baseSet
⊢ proj ((↑e.symm : B × F → Z) (x, y)) ∈ s ↔ x ∈ s
have h₁ : x ∈ s ↔ x ∈ s
Tactic: rw [e.proj_symm_apply' 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
e f : Pretrivialization F proj
⊢ f.target ∩ (↑f.symm : B × F → Z) ⁻¹' e.source = SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ
have rw : (↑f.symm : B × F → Z) ⁻¹' e.source ∩ f.target = SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ
Tactic: rw [inter_comm, f.target_eq, e.source_eq, f.preimage_symm_proj_inter]
-- 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
e f : Pretrivialization F proj
rw : (↑f.symm : B × F → Z) ⁻¹' e.source ∩ f.target = SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ
⊢ f.target ∩ (↑f.symm : B × F → Z) ⁻¹' e.source = SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ
have rw₁ : (↑f.symm : B × F → Z) ⁻¹' e.source ∩ SProd.sprod (β := Set F) f.baseSet univ =
  SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ
Tactic: rw [inter_comm, f.target_eq, e.source_eq, f.preimage_symm_proj_inter]
-- 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
e f : Pretrivialization F proj
rw : (↑f.symm : B × F → Z) ⁻¹' e.source ∩ f.target = SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ
rw₁ :
  (↑f.symm : B × F → Z) ⁻¹' e.source ∩ SProd.sprod (β := Set F) f.baseSet univ =
    SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ
⊢ f.target ∩ (↑f.symm : B × F → Z) ⁻¹' e.source = SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ
have rw₂ : (↑f.symm : B × F → Z) ⁻¹' proj ⁻¹' e.baseSet ∩ SProd.sprod (β := Set F) f.baseSet univ =
  SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ
Tactic: rw [inter_comm, f.target_eq, e.source_eq, f.preimage_symm_proj_inter]
-- 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
e f : Pretrivialization F proj
rw : (↑f.symm : B × F → Z) ⁻¹' e.source ∩ f.target = SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ
rw₁ :
  (↑f.symm : B × F → Z) ⁻¹' e.source ∩ SProd.sprod (β := Set F) f.baseSet univ =
    SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ
rw₂ :
  (↑f.symm : B × F → Z) ⁻¹' proj ⁻¹' e.baseSet ∩ SProd.sprod (β := Set F) f.baseSet univ =
    SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ
⊢ f.target ∩ (↑f.symm : B × F → Z) ⁻¹' e.source = SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ
have rw₃ : SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ = SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ
Tactic: rw [inter_comm, f.target_eq, e.source_eq, f.preimage_symm_proj_inter]
-- 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
e f : Pretrivialization F proj
⊢ (f.symm.trans e.toPartialEquiv).source = SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ
have rw : f.symm.source ∩ (↑f.symm : B × F → Z) ⁻¹' e.source = SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ
Tactic: rw [PartialEquiv.trans_source, PartialEquiv.symm_source, e.target_inter_preimage_symm_source_eq]
-- 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
e f : Pretrivialization F proj
rw : f.symm.source ∩ (↑f.symm : B × F → Z) ⁻¹' e.source = SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ
⊢ (f.symm.trans e.toPartialEquiv).source = SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ
have rw₁ : f.target ∩ (↑f.symm : B × F → Z) ⁻¹' e.source = SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ
Tactic: rw [PartialEquiv.trans_source, PartialEquiv.symm_source, e.target_inter_preimage_symm_source_eq]
-- 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
e f : Pretrivialization F proj
rw : f.symm.source ∩ (↑f.symm : B × F → Z) ⁻¹' e.source = SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ
rw₁ : f.target ∩ (↑f.symm : B × F → Z) ⁻¹' e.source = SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ
⊢ (f.symm.trans e.toPartialEquiv).source = SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ
have rw₂ : SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ = SProd.sprod (β := Set F) (e.baseSet ∩ f.baseSet) univ
Tactic: rw [PartialEquiv.trans_source, PartialEquiv.symm_source, e.target_inter_preimage_symm_source_eq]
-- 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
e e' : Pretrivialization F proj
⊢ (e.symm.trans e'.toPartialEquiv).symm = e'.symm.trans e.toPartialEquiv
have rw : e'.symm.trans e.symm.symm = e'.symm.trans e.toPartialEquiv
Tactic: rw [PartialEquiv.trans_symm_eq_symm_trans_symm, PartialEquiv.symm_symm]
-- 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
e e' : Pretrivialization F proj
rw : e'.symm.trans e.symm.symm = e'.symm.trans e.toPartialEquiv
⊢ (e.symm.trans e'.toPartialEquiv).symm = e'.symm.trans e.toPartialEquiv
have rw₁ : e'.symm.trans e.toPartialEquiv = e'.symm.trans e.toPartialEquiv
Tactic: rw [PartialEquiv.trans_symm_eq_symm_trans_symm, PartialEquiv.symm_symm]
-- 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
e e' : Pretrivialization F proj
⊢ (e.symm.trans e'.toPartialEquiv).source = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
have rw : e.symm.source ∩ (↑e.symm : B × F → Z) ⁻¹' e'.source = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
Tactic: rw [PartialEquiv.trans_source, e'.source_eq, PartialEquiv.symm_source, e.target_eq, inter_comm,
    e.preimage_symm_proj_inter, inter_comm]
-- 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
e e' : Pretrivialization F proj
rw : e.symm.source ∩ (↑e.symm : B × F → Z) ⁻¹' e'.source = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
⊢ (e.symm.trans e'.toPartialEquiv).source = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
have rw₁ : e.symm.source ∩ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' e'.baseSet = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
Tactic: rw [PartialEquiv.trans_source, e'.source_eq, PartialEquiv.symm_source, e.target_eq, inter_comm,
    e.preimage_symm_proj_inter, inter_comm]
-- 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
e e' : Pretrivialization F proj
rw : e.symm.source ∩ (↑e.symm : B × F → Z) ⁻¹' e'.source = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
rw₁ :
  e.symm.source ∩ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' e'.baseSet = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
⊢ (e.symm.trans e'.toPartialEquiv).source = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
have rw₂ : e.target ∩ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' e'.baseSet = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
Tactic: rw [PartialEquiv.trans_source, e'.source_eq, PartialEquiv.symm_source, e.target_eq, inter_comm,
    e.preimage_symm_proj_inter, inter_comm]
-- 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
e e' : Pretrivialization F proj
rw : e.symm.source ∩ (↑e.symm : B × F → Z) ⁻¹' e'.source = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
rw₁ :
  e.symm.source ∩ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' e'.baseSet = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
rw₂ : e.target ∩ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' e'.baseSet = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
⊢ (e.symm.trans e'.toPartialEquiv).source = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
have rw₃ : SProd.sprod (β := Set F) e.baseSet univ ∩ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' e'.baseSet =
  SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
Tactic: rw [PartialEquiv.trans_source, e'.source_eq, PartialEquiv.symm_source, e.target_eq, inter_comm,
    e.preimage_symm_proj_inter, inter_comm]
-- 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
e e' : Pretrivialization F proj
rw : e.symm.source ∩ (↑e.symm : B × F → Z) ⁻¹' e'.source = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
rw₁ :
  e.symm.source ∩ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' e'.baseSet = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
rw₂ : e.target ∩ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' e'.baseSet = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
rw₃ :
  SProd.sprod (β := Set F) e.baseSet univ ∩ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' e'.baseSet =
    SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
⊢ (e.symm.trans e'.toPartialEquiv).source = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
have rw₄ : (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' e'.baseSet ∩ SProd.sprod (β := Set F) e.baseSet univ =
  SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
Tactic: rw [PartialEquiv.trans_source, e'.source_eq, PartialEquiv.symm_source, e.target_eq, inter_comm,
    e.preimage_symm_proj_inter, inter_comm]
-- 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
e e' : Pretrivialization F proj
rw : e.symm.source ∩ (↑e.symm : B × F → Z) ⁻¹' e'.source = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
rw₁ :
  e.symm.source ∩ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' e'.baseSet = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
rw₂ : e.target ∩ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' e'.baseSet = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
rw₃ :
  SProd.sprod (β := Set F) e.baseSet univ ∩ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' e'.baseSet =
    SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
rw₄ :
  (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' e'.baseSet ∩ SProd.sprod (β := Set F) e.baseSet univ =
    SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
⊢ (e.symm.trans e'.toPartialEquiv).source = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
have rw₅ : SProd.sprod (β := Set F) (e'.baseSet ∩ e.baseSet) univ = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
Tactic: rw [PartialEquiv.trans_source, e'.source_eq, PartialEquiv.symm_source, e.target_eq, inter_comm,
    e.preimage_symm_proj_inter, inter_comm]
-- 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
e e' : Pretrivialization F proj
rw : e.symm.source ∩ (↑e.symm : B × F → Z) ⁻¹' e'.source = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
rw₁ :
  e.symm.source ∩ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' e'.baseSet = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
rw₂ : e.target ∩ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' e'.baseSet = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
rw₃ :
  SProd.sprod (β := Set F) e.baseSet univ ∩ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' e'.baseSet =
    SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
rw₄ :
  (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' e'.baseSet ∩ SProd.sprod (β := Set F) e.baseSet univ =
    SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
rw₅ : SProd.sprod (β := Set F) (e'.baseSet ∩ e.baseSet) univ = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
⊢ (e.symm.trans e'.toPartialEquiv).source = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
have rw₆ : SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
Tactic: rw [PartialEquiv.trans_source, e'.source_eq, PartialEquiv.symm_source, e.target_eq, inter_comm,
    e.preimage_symm_proj_inter, inter_comm]
-- 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
e e' : Pretrivialization F proj
⊢ (e.symm.trans e'.toPartialEquiv).target = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
have rw : (e.symm.trans e'.toPartialEquiv).symm.source = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
Tactic: rw [← PartialEquiv.symm_source, symm_trans_symm, symm_trans_source_eq, inter_comm]
-- 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
e e' : Pretrivialization F proj
rw : (e.symm.trans e'.toPartialEquiv).symm.source = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
⊢ (e.symm.trans e'.toPartialEquiv).target = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
have rw₁ : (e'.symm.trans e.toPartialEquiv).source = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
Tactic: rw [← PartialEquiv.symm_source, symm_trans_symm, symm_trans_source_eq, inter_comm]
-- 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
e e' : Pretrivialization F proj
rw : (e.symm.trans e'.toPartialEquiv).symm.source = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
rw₁ : (e'.symm.trans e.toPartialEquiv).source = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
⊢ (e.symm.trans e'.toPartialEquiv).target = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
have rw₂ : SProd.sprod (β := Set F) (e'.baseSet ∩ e.baseSet) univ = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
Tactic: rw [← PartialEquiv.symm_source, symm_trans_symm, symm_trans_source_eq, inter_comm]
-- 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
e e' : Pretrivialization F proj
rw : (e.symm.trans e'.toPartialEquiv).symm.source = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
rw₁ : (e'.symm.trans e.toPartialEquiv).source = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
rw₂ : SProd.sprod (β := Set F) (e'.baseSet ∩ e.baseSet) univ = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
⊢ (e.symm.trans e'.toPartialEquiv).target = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
have rw₃ : SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ = SProd.sprod (β := Set F) (e.baseSet ∩ e'.baseSet) univ
Tactic: rw [← PartialEquiv.symm_source, symm_trans_symm, symm_trans_source_eq, inter_comm]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : (x : B) → Zero (E x)
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
z : TotalSpace F E
hz : z.proj (E := E) ∈ e.baseSet
⊢ e.symm (E := E) (z.proj (E := E)) ((↑e : TotalSpace F E → B × F) z).2 = z.snd (E := E)
have rw : cast sorry (((↑e.symm : B × F → TotalSpace F E) (z.proj (E := E), ((↑e : TotalSpace F E → B × F) z).2)).snd (E := E)) =
  z.snd (E := E)
Tactic: rw [e.symm_apply hz, cast_eq_iff_heq, e.mk_proj_snd' hz, e.symm_apply_apply (e.mem_source.mpr 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
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : (x : B) → Zero (E x)
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
z : TotalSpace F E
hz : z.proj (E := E) ∈ e.baseSet
rw :
  cast ⋯ (((↑e.symm : B × F → TotalSpace F E) (z.proj (E := E), ((↑e : TotalSpace F E → B × F) z).2)).snd (E := E)) =
    z.snd (E := E)
⊢ e.symm (E := E) (z.proj (E := E)) ((↑e : TotalSpace F E → B × F) z).2 = z.snd (E := E)
have rw₁ : ((↑e.symm : B × F → TotalSpace F E) (z.proj (E := E), ((↑e : TotalSpace F E → B × F) z).2)).snd (E := E) ≍
  z.snd (E := E)
Tactic: rw [e.symm_apply hz, cast_eq_iff_heq, e.mk_proj_snd' hz, e.symm_apply_apply (e.mem_source.mpr 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
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : (x : B) → Zero (E x)
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
z : TotalSpace F E
hz : z.proj (E := E) ∈ e.baseSet
rw :
  cast ⋯ (((↑e.symm : B × F → TotalSpace F E) (z.proj (E := E), ((↑e : TotalSpace F E → B × F) z).2)).snd (E := E)) =
    z.snd (E := E)
rw₁ :
  ((↑e.symm : B × F → TotalSpace F E) (z.proj (E := E), ((↑e : TotalSpace F E → B × F) z).2)).snd (E := E) ≍
    z.snd (E := E)
⊢ e.symm (E := E) (z.proj (E := E)) ((↑e : TotalSpace F E → B × F) z).2 = z.snd (E := E)
have rw₂ : ((↑e.symm : B × F → TotalSpace F E) ((↑e : TotalSpace F E → B × F) z)).snd (E := E) ≍ z.snd (E := E)
Tactic: rw [e.symm_apply hz, cast_eq_iff_heq, e.mk_proj_snd' hz, e.symm_apply_apply (e.mem_source.mpr 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
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : (x : B) → Zero (E x)
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
z : TotalSpace F E
hz : z.proj (E := E) ∈ e.baseSet
rw :
  cast ⋯ (((↑e.symm : B × F → TotalSpace F E) (z.proj (E := E), ((↑e : TotalSpace F E → B × F) z).2)).snd (E := E)) =
    z.snd (E := E)
rw₁ :
  ((↑e.symm : B × F → TotalSpace F E) (z.proj (E := E), ((↑e : TotalSpace F E → B × F) z).2)).snd (E := E) ≍
    z.snd (E := E)
rw₂ : ((↑e.symm : B × F → TotalSpace F E) ((↑e : TotalSpace F E → B × F) z)).snd (E := E) ≍ z.snd (E := E)
⊢ e.symm (E := E) (z.proj (E := E)) ((↑e : TotalSpace F E → B × F) z).2 = z.snd (E := E)
have rw₃ : z.snd (E := E) ≍ z.snd (E := E)
Tactic: rw [e.symm_apply hz, cast_eq_iff_heq, e.mk_proj_snd' hz, e.symm_apply_apply (e.mem_source.mpr 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
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : (x : B) → Zero (E x)
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
hb : b ∈ e.baseSet
y : F
⊢ (↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b y)) = (b, y)
have rw : (↑e : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) (b, y)) = (b, y)
Tactic: rw [e.mk_symm hb, e.apply_symm_apply (e.mk_mem_target.mpr hb)]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (goal)
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : (x : B) → Zero (E x)
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
hb : b ∈ e.baseSet
y : F
rw : (↑e : TotalSpace F E → B × F) ((↑e.symm : B × F → TotalSpace F E) (b, y)) = (b, y)
⊢ (↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b y)) = (b, y)
have rw₁ : (b, y) = (b, y)
Tactic: rw [e.mk_symm hb, e.apply_symm_apply (e.mk_mem_target.mpr hb)]
-- 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
⊢ 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)
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
⊢ 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)
have 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)) sorry)
Tactic: rw [dif_pos hx]