awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
x : TotalSpace.{w₂, v, w₁} (B := B') F ((⇑f : (a : B') → B) *ᵖ E)
h : Membership.mem (α := B) e.baseSet ((f : (a : B') → B) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E)) : B)
⊢ TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E)
      (x.proj (E := (⇑f : (a : B') → B) *ᵖ E),
          ((↑e : TotalSpace F E → B × F) (Pullback.lift (E := E) (⇑f : (a : B') → B) x)).2).1
      (e.symm (E := E)
        ((f : (a : B') → B)
          (x.proj (E := (⇑f : (a : B') → B) *ᵖ E),
              ((↑e : TotalSpace F E → B × F) (Pullback.lift (E := E) (⇑f : (a : B') → B) x)).2).1)
        (x.proj (E := (⇑f : (a : B') → B) *ᵖ E),
            ((↑e : TotalSpace F E → B × F) (Pullback.lift (E := E) (⇑f : (a : B') → B) x)).2).2) =
    x
have simp_rw : TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E))
    (e.symm (E := E) ((f : (a : B') → B) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E)))
      ((↑e : TotalSpace F E → B × F) (Pullback.lift (E := E) (⇑f : (a : B') → B) x)).2) =
  x
Tactic: simp_rw [Pullback.lift, e.symm_apply_apply_mk h]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
x : TotalSpace.{w₂, v, w₁} (B := B') F ((⇑f : (a : B') → B) *ᵖ E)
h : Membership.mem (α := B) e.baseSet ((f : (a : B') → B) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E)) : B)
simp_rw simp_rw₁ :
  TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E))
      (e.symm (E := E) ((f : (a : B') → B) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E)))
        ((↑e : TotalSpace F E → B × F) (Pullback.lift (E := E) (⇑f : (a : B') → B) x)).2) =
    x
⊢ TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E)
      (x.proj (E := (⇑f : (a : B') → B) *ᵖ E),
          ((↑e : TotalSpace F E → B × F) (Pullback.lift (E := E) (⇑f : (a : B') → B) x)).2).1
      (e.symm (E := E)
        ((f : (a : B') → B)
          (x.proj (E := (⇑f : (a : B') → B) *ᵖ E),
              ((↑e : TotalSpace F E → B × F) (Pullback.lift (E := E) (⇑f : (a : B') → B) x)).2).1)
        (x.proj (E := (⇑f : (a : B') → B) *ᵖ E),
            ((↑e : TotalSpace F E → B × F) (Pullback.lift (E := E) (⇑f : (a : B') → B) x)).2).2) =
    x
have simp_rw₂ : TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E))
    (e.symm (E := E) ((f : (a : B') → B) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E)))
      ((↑e : TotalSpace F E → B × F)
          (TotalSpace.mk (E := E) ((f : (a : B') → B) (x.proj (E := (⇑f : (a : B') → B) *ᵖ E)))
            (x.snd (E := (⇑f : (a : B') → B) *ᵖ E)))).2) =
  x
Tactic: simp_rw [Pullback.lift, e.symm_apply_apply_mk h]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (hypothesis)
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
x : B' × F
h : x ∈ SProd.sprod (α := Set B') (β := Set F) ((⇑f : (a : B') → B) ⁻¹' e.baseSet) univ
⊢ (TotalSpace.proj.{w₂, v, w₁} (F := F) (E := (⇑f : (a : B') → B) *ᵖ E)
        (TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E) x.1 (e.symm (E := E) ((f : (a : B') → B) x.1) x.2)),
      ((↑e : TotalSpace F E → B × F)
          (Pullback.lift (E := E) (⇑f : (a : B') → B)
            (TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E) x.1 (e.symm (E := E) ((f : (a : B') → B) x.1) x.2)))).2) =
    x
have h₁ : Membership.mem (α := B) e.baseSet ((f : (a : B') → B) x.1 : B)
Tactic: simp_rw [mem_prod, mem_preimage, mem_univ, and_true] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
x : B' × F
h : Membership.mem (α := B) e.baseSet ((f : (a : B') → B) x.1 : B)
⊢ (TotalSpace.proj.{w₂, v, w₁} (F := F) (E := (⇑f : (a : B') → B) *ᵖ E)
        (TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E) x.1 (e.symm (E := E) ((f : (a : B') → B) x.1) x.2)),
      ((↑e : TotalSpace F E → B × F)
          (Pullback.lift (E := E) (⇑f : (a : B') → B)
            (TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E) x.1 (e.symm (E := E) ((f : (a : B') → B) x.1) x.2)))).2) =
    x
have simp_rw : (x.1,
    ((↑e : TotalSpace F E → B × F)
        (Pullback.lift (E := E) (⇑f : (a : B') → B)
          (TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E) x.1 (e.symm (E := E) ((f : (a : B') → B) x.1) x.2)))).2) =
  x
Tactic: simp_rw [Pullback.lift_mk, e.apply_mk_symm h]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
x : B' × F
h : Membership.mem (α := B) e.baseSet ((f : (a : B') → B) x.1 : B)
simp_rw simp_rw₁ :
  (x.1,
      ((↑e : TotalSpace F E → B × F)
          (Pullback.lift (E := E) (⇑f : (a : B') → B)
            (TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E) x.1 (e.symm (E := E) ((f : (a : B') → B) x.1) x.2)))).2) =
    x
⊢ (TotalSpace.proj.{w₂, v, w₁} (F := F) (E := (⇑f : (a : B') → B) *ᵖ E)
        (TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E) x.1 (e.symm (E := E) ((f : (a : B') → B) x.1) x.2)),
      ((↑e : TotalSpace F E → B × F)
          (Pullback.lift (E := E) (⇑f : (a : B') → B)
            (TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E) x.1 (e.symm (E := E) ((f : (a : B') → B) x.1) x.2)))).2) =
    x
have simp_rw₂ : (x.1,
    ((↑e : TotalSpace F E → B × F)
        (TotalSpace.mk (E := E) ((f : (a : B') → B) x.1) (e.symm (E := E) ((f : (a : B') → B) x.1) x.2))).2) =
  x
Tactic: simp_rw [Pullback.lift_mk, e.apply_mk_symm h]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
⊢ IsOpen[Pullback.TotalSpace.topologicalSpace F E (⇑f : (a : B') → B)]
    (Pullback.lift (E := E) (⇑f : (a : B') → B) ⁻¹' e.source)
have simp_rw : IsOpen[Pullback.TotalSpace.topologicalSpace F E (⇑f : (a : B') → B)]
  (TotalSpace.proj (E := E) ∘ Pullback.lift (E := E) (⇑f : (a : B') → B) ⁻¹' e.baseSet)
Tactic: simp_rw [e.source_eq, ← preimage_comp]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
⊢ ContinuousOn (Y := TotalSpace.{w₂, v, w₁} (B := B') F ((⇑f : (a : B') → B) *ᵖ E))
    (fun (y : B' × F) ↦
      TotalSpace.mk (E := (⇑f : (a : B') → B) *ᵖ E) y.1 (e.symm (E := E) ((f : (a : B') → B) y.1) y.2))
    (SProd.sprod (α := Set B') (β := Set F) ((⇑f : (a : B') → B) ⁻¹' e.baseSet) univ)
have simp_rw : ContinuousOn (Y := B' × TotalSpace F E)
  (fun (x : B' × F) ↦
    (x.1, TotalSpace.mk (E := E) ((f : (a : B') → B) x.1) (e.symm (E := E) ((f : (a : B') → B) x.1) x.2)))
  (SProd.sprod (α := Set B') (β := Set F) ((⇑f : (a : B') → B) ⁻¹' e.baseSet) univ)
Tactic: simp_rw [(inducing_pullbackTotalSpaceEmbedding F E f).continuousOn_iff, Function.comp_def,
      pullbackTotalSpaceEmbedding]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
Goal:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : TopologicalSpace F
inst_3 : TopologicalSpace B
inst_4 : (_b : B) → Zero (E _b)
K : Type U
inst_5 : FunLike K B' B
inst_6 : ContinuousMapClass K B' B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
f : K
⊢ Eq (α := Set (TotalSpace.{w₂, v, w₁} (B := B') F ((⇑f : (a : B') → B) *ᵖ E)))
    (Pullback.lift (E := E) (⇑f : (a : B') → B) ⁻¹' e.source)
    (TotalSpace.proj (E := (⇑f : (a : B') → B) *ᵖ E) ⁻¹' (⇑f : (a : B') → B) ⁻¹' e.baseSet)
have rw : Eq (α := Set (TotalSpace.{w₂, v, w₁} (B := B') F ((⇑f : (a : B') → B) *ᵖ E)))
  (Pullback.lift (E := E) (⇑f : (a : B') → B) ⁻¹' TotalSpace.proj (E := E) ⁻¹' e.baseSet)
  (TotalSpace.proj (E := (⇑f : (a : B') → B) *ᵖ E) ⁻¹' (⇑f : (a : B') → B) ⁻¹' e.baseSet)
Tactic: rw [e.source_eq]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle (goal)
Goal:
B : Type u_1
F : Type u_2
Z : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace Z
proj : Z → B
inst_3 : Nonempty F
h : IsHomeomorphicTrivialFiberBundle F proj
⊢ Function.Surjective proj
have obtain : ∀ (e : Z ≃ₜ B × F)
  (h :
    IsHomeomorphicTrivialFiberBundle.{u_1, u_2, u_3} (B := B) F (Z := Z)
      (Function.comp (β := B × F) Prod.fst (⇑e : (a : Z) → B × F))),
  Function.Surjective.{u_3 + 1, u_1 + 1} (α := Z) (β := B) (Function.comp (β := B × F) Prod.fst (⇑e : (a : Z) → B × F))
Tactic: obtain ⟨e, rfl⟩ := h.proj_eq
Cleared hypotheses: proj, h
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle (goal)
Goal:
B : Type u_1
F : Type u_2
Z : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace Z
proj : Z → B
h : IsHomeomorphicTrivialFiberBundle F proj
⊢ Continuous[inst_2, inst] proj
have obtain : ∀ (e : Z ≃ₜ B × F)
  (h :
    IsHomeomorphicTrivialFiberBundle.{u_1, u_2, u_3} (B := B) F (Z := Z)
      (Function.comp (β := B × F) Prod.fst (⇑e : (a : Z) → B × F))),
  Continuous[inst_2, inst] (Function.comp (β := B × F) Prod.fst (⇑e : (a : Z) → B × F))
Tactic: obtain ⟨e, rfl⟩ := h.proj_eq
Cleared hypotheses: proj, h
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle (goal)
Goal:
B : Type u_1
F : Type u_2
Z : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : TopologicalSpace Z
proj : Z → B
h : IsHomeomorphicTrivialFiberBundle F proj
⊢ IsOpenMap proj
have obtain : ∀ (e : Z ≃ₜ B × F)
  (h :
    IsHomeomorphicTrivialFiberBundle.{u_1, u_2, u_3} (B := B) F (Z := Z)
      (Function.comp (β := B × F) Prod.fst (⇑e : (a : Z) → B × F))),
  IsOpenMap.{u_3, u_1} (X := Z) (Y := B) (Function.comp (β := B × F) Prod.fst (⇑e : (a : Z) → B × F))
Tactic: obtain ⟨e, rfl⟩ := h.proj_eq
Cleared hypotheses: proj, 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 e' : Pretrivialization F proj
h₁ : e.toPartialEquiv = e'.toPartialEquiv
h₂ : e.baseSet = e'.baseSet
⊢ e = e'
have mk : ∀ (toPartialEquiv : PartialEquiv Z (B × F)) (open_target : IsOpen[instTopologicalSpaceProd] toPartialEquiv.target)
  (baseSet : Set B) (open_baseSet : IsOpen[inst] baseSet) (source_eq : toPartialEquiv.source = proj ⁻¹' baseSet)
  (target_eq : toPartialEquiv.target = SProd.sprod (β := Set F) baseSet univ)
  (proj_toFun : ∀ p ∈ toPartialEquiv.source, ((↑toPartialEquiv : Z → B × F) p).1 = proj p)
  (h₁ :
    { toPartialEquiv := toPartialEquiv, open_target := open_target, baseSet := baseSet, open_baseSet := open_baseSet,
          source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun :
          Pretrivialization F proj }.toPartialEquiv =
      e'.toPartialEquiv)
  (h₂ :
    { toPartialEquiv := toPartialEquiv, open_target := open_target, baseSet := baseSet, open_baseSet := open_baseSet,
          source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun :
          Pretrivialization F proj }.baseSet =
      e'.baseSet),
  { toPartialEquiv := toPartialEquiv, open_target := open_target, baseSet := baseSet, open_baseSet := open_baseSet,
      source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun : Pretrivialization F proj } =
    e'
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
e e' : Pretrivialization F proj
h₁ : ∀ (x : Z), (↑e : Z → B × F) x = (↑e' : Z → B × F) x
h₂ : ∀ (x : B × F), (↑e.symm : B × F → Z) x = (↑e'.symm : B × F → Z) x
h₃ : e.baseSet = e'.baseSet
⊢ e = e'
have h₄ : e.toPartialEquiv = e'.toPartialEquiv
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
e e' : Pretrivialization F proj
h₁ : ∀ (x : Z), (↑e : Z → B × F) x = (↑e' : Z → B × F) x
h₂ : ∀ (x : B × F), (↑e.symm : B × F → Z) x = (↑e'.symm : B × F → Z) x
h₃ : e.baseSet = e'.baseSet
⊢ e.toPartialEquiv = e'.toPartialEquiv
have h₄ : ∀ (x : Z), (↑e.toPartialEquiv : Z → B × F) x = (↑e'.toPartialEquiv : Z → B × F) x
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
e e' : Pretrivialization F proj
h₁ : ∀ (x : Z), (↑e : Z → B × F) x = (↑e' : Z → B × F) x
h₂ : ∀ (x : B × F), (↑e.symm : B × F → Z) x = (↑e'.symm : B × F → Z) x
h₃ : e.baseSet = e'.baseSet
h₄ : ∀ (x : Z), (↑e.toPartialEquiv : Z → B × F) x = (↑e'.toPartialEquiv : Z → B × F) x
h₅ : ∀ (x : B × F), (↑e.symm : B × F → Z) x = (↑e'.symm : B × F → Z) x
⊢ e.toPartialEquiv = e'.toPartialEquiv
have h₆ : e.source = e'.source
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
e e' : Pretrivialization F proj
h₁ : ∀ (x : Z), (↑e : Z → B × F) x = (↑e' : Z → B × F) x
h₂ : ∀ (x : B × F), (↑e.symm : B × F → Z) x = (↑e'.symm : B × F → Z) x
h₃ : e.baseSet = e'.baseSet
⊢ e = e'
have h₄ : ∀ (x : Z), (↑e.toPartialEquiv : Z → B × F) x = (↑e'.toPartialEquiv : Z → B × F) x
Tactic: ext1 <;> [ext1; exact 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 e' : Pretrivialization F proj
h₁ : ∀ (x : Z), (↑e : Z → B × F) x = (↑e' : Z → B × F) x
h₂ : ∀ (x : B × F), (↑e.symm : B × F → Z) x = (↑e'.symm : B × F → Z) x
h₃ : e.baseSet = e'.baseSet
h₄ : ∀ (x : Z), (↑e.toPartialEquiv : Z → B × F) x = (↑e'.toPartialEquiv : Z → B × F) x
h₅ : ∀ (x : B × F), (↑e.symm : B × F → Z) x = (↑e'.symm : B × F → Z) x
⊢ e = e'
have h₆ : e.source = e'.source
Tactic: ext1 <;> [ext1; exact 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 e' : Pretrivialization F proj
h₁ : ∀ (x : Z), (↑e : Z → B × F) x = (↑e' : Z → B × F) x
h₂ : ∀ (x : B × F), (↑e.symm : B × F → Z) x = (↑e'.symm : B × F → Z) x
h₃ : e.baseSet = e'.baseSet
⊢ e.source = e'.source
have h₄ : proj ⁻¹' e.baseSet = e'.source
Tactic: rw [e.source_eq, e'.source_eq, 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 e' : Pretrivialization F proj
h₁ : ∀ (x : Z), (↑e : Z → B × F) x = (↑e' : Z → B × F) x
h₂ : ∀ (x : B × F), (↑e.symm : B × F → Z) x = (↑e'.symm : B × F → Z) x
h₃ : e.baseSet = e'.baseSet
h₄ : proj ⁻¹' e.baseSet = e'.source
⊢ e.source = e'.source
have h₅ : proj ⁻¹' e.baseSet = proj ⁻¹' e'.baseSet
Tactic: rw [e.source_eq, e'.source_eq, 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 e' : Pretrivialization F proj
h₁ : ∀ (x : Z), (↑e : Z → B × F) x = (↑e' : Z → B × F) x
h₂ : ∀ (x : B × F), (↑e.symm : B × F → Z) x = (↑e'.symm : B × F → Z) x
h₃ : e.baseSet = e'.baseSet
h₄ : proj ⁻¹' e.baseSet = e'.source
h₅ : proj ⁻¹' e.baseSet = proj ⁻¹' e'.baseSet
⊢ e.source = e'.source
have h₆ : proj ⁻¹' e'.baseSet = proj ⁻¹' e'.baseSet
Tactic: rw [e.source_eq, e'.source_eq, 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 : Nonempty F
⊢ Injective (α := Pretrivialization F proj) toPartialEquiv
have refine : ∀ (e e' : Pretrivialization F proj) (h : e.toPartialEquiv = e'.toPartialEquiv), e.baseSet = e'.baseSet
Tactic: refine fun e e' h ↦ ext' _ _ 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 : Pretrivialization F proj
x : Z
⊢ x ∈ e.source ↔ proj x ∈ e.baseSet
have rw : x ∈ proj ⁻¹' e.baseSet ↔ proj x ∈ e.baseSet
Tactic: rw [e.source_eq, mem_preimage]
-- 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 : Z
rw : x ∈ proj ⁻¹' e.baseSet ↔ proj x ∈ e.baseSet
⊢ x ∈ e.source ↔ proj x ∈ e.baseSet
have rw₁ : proj x ∈ e.baseSet ↔ proj x ∈ e.baseSet
Tactic: rw [e.source_eq, mem_preimage]
-- 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
⊢ x ∈ e.target ↔ x.1 ∈ e.baseSet
have rw : x ∈ SProd.sprod (β := Set F) e.baseSet univ ↔ x.1 ∈ e.baseSet
Tactic: rw [e.target_eq, prod_univ, mem_preimage]
-- 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
rw : x ∈ SProd.sprod (β := Set F) e.baseSet univ ↔ x.1 ∈ e.baseSet
⊢ x ∈ e.target ↔ x.1 ∈ e.baseSet
have rw₁ : Membership.mem (γ := Set (B × F)) (Prod.fst ⁻¹' e.baseSet) x ↔ x.1 ∈ e.baseSet
Tactic: rw [e.target_eq, prod_univ, mem_preimage]
-- 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
rw : x ∈ SProd.sprod (β := Set F) e.baseSet univ ↔ x.1 ∈ e.baseSet
rw₁ : Membership.mem (γ := Set (B × F)) (Prod.fst ⁻¹' e.baseSet) x ↔ x.1 ∈ e.baseSet
⊢ x ∈ e.target ↔ x.1 ∈ e.baseSet
have rw₂ : x.1 ∈ e.baseSet ↔ x.1 ∈ e.baseSet
Tactic: rw [e.target_eq, prod_univ, mem_preimage]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Trivialization (hypothesis)
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
⊢ proj ((↑e.symm : B × F → Z) x) = x.1
have this : proj ((↑e.symm : B × F → Z) x) = ((↑e : Z → B × F) ((↑e.symm : B × F → Z) x)).1
Tactic: have := (e.coe_fst (e.map_target hx)).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 : Pretrivialization F proj
x : B × F
hx : x ∈ e.target
this : proj ((↑e.symm : B × F → Z) x) = ((↑e : Z → B × F) ((↑e.symm : B × F → Z) x)).1
⊢ proj ((↑e.symm : B × F → Z) x) = x.1
have rwa : ∀ (this : proj ((↑e.symm : B × F → Z) x) = ((↑e.toPartialEquiv : Z → B × F) ((↑e.symm : B × F → Z) x)).1),
  proj ((↑e.symm : B × F → Z) x) = x.1
Tactic: rwa [← e.coe_coe, e.right_inv hx] at this
Cleared hypotheses: this
-- 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
this : proj ((↑e.symm : B × F → Z) x) = ((↑e : Z → B × F) ((↑e.symm : B × F → Z) x)).1
rwa :
  ∀ (this : proj ((↑e.symm : B × F → Z) x) = ((↑e.toPartialEquiv : Z → B × F) ((↑e.symm : B × F → Z) x)).1),
    proj ((↑e.symm : B × F → Z) x) = x.1
⊢ proj ((↑e.symm : B × F → Z) x) = x.1
have rwa₁ : ∀ (this : proj ((↑e.symm : B × F → Z) x) = x.1), proj ((↑e.symm : B × F → Z) x) = x.1
Tactic: rwa [← e.coe_coe, e.right_inv hx] at this
Cleared hypotheses: this
-- 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 : Z
ex : x ∈ e.source
⊢ (↑e.symm : B × F → Z) (proj x, ((↑e : Z → B × F) x).2) = x
have rw : (↑e.symm : B × F → Z) (((↑e : Z → B × F) x).1, ((↑e : Z → B × F) x).2) = x
Tactic: rw [← e.coe_fst ex, ← e.coe_coe, e.left_inv ex]
-- 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 : Z
ex : x ∈ e.source
rw : (↑e.symm : B × F → Z) (((↑e : Z → B × F) x).1, ((↑e : Z → B × F) x).2) = x
⊢ (↑e.symm : B × F → Z) (proj x, ((↑e : Z → B × F) x).2) = x
have rw₁ : (↑e.symm : B × F → Z) (((↑e.toPartialEquiv : Z → B × F) x).1, ((↑e.toPartialEquiv : Z → B × F) x).2) = x
Tactic: rw [← e.coe_fst ex, ← e.coe_coe, e.left_inv ex]
-- 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 : Z
ex : x ∈ e.source
rw : (↑e.symm : B × F → Z) (((↑e : Z → B × F) x).1, ((↑e : Z → B × F) x).2) = x
rw₁ : (↑e.symm : B × F → Z) (((↑e.toPartialEquiv : Z → B × F) x).1, ((↑e.toPartialEquiv : Z → B × F) x).2) = x
⊢ (↑e.symm : B × F → Z) (proj x, ((↑e : Z → B × F) x).2) = x
have rw₂ : x = x
Tactic: rw [← e.coe_fst ex, ← e.coe_coe, e.left_inv ex]
-- 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
⊢ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' e.baseSet ∩ e.target = e.target
have refine : ∀ (x : B × F) (hx : x ∈ e.target), x ∈ (↑e.symm : B × F → Z) ⁻¹' proj ⁻¹' e.baseSet
Tactic: refine inter_eq_right.mpr fun x hx => ?_