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
inst_2 : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ (b, e₁.coordChange e₂ b x).1 = ((↑e₂ : Z → B × F) ((↑e₁.symm : B × F → Z) (b, x))).1
have rw : proj ((↑e₁.symm : B × F → Z) (b, x)) ∈ e₁.baseSet
Tactic: rw [e₂.coe_fst', ← e₁.coe_fst', e₁.apply_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
inst_2 : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
rw : proj ((↑e₁.symm : B × F → Z) (b, x)) ∈ e₁.baseSet
⊢ (b, e₁.coordChange e₂ b x).1 = ((↑e₂ : Z → B × F) ((↑e₁.symm : B × F → Z) (b, x))).1
have rw₁ : proj ((↑e₁.symm : B × F → Z) (b, x)) ∈ e₂.baseSet
Tactic: rw [e₂.coe_fst', ← e₁.coe_fst', e₁.apply_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
inst_2 : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
p : Z
h : proj p ∈ e₁.baseSet
⊢ e₁.coordChange e₂ (proj p) ((↑e₁ : Z → B × F) p).2 = ((↑e₂ : Z → B × F) p).2
have rw : ((↑e₂ : Z → B × F) ((↑e₁.symm : B × F → Z) (proj p, ((↑e₁ : Z → B × F) p).2))).2 = ((↑e₂ : Z → B × F) p).2
Tactic: rw [coordChange, e₁.symm_apply_mk_proj (e₁.mem_source.2 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
p : Z
h : proj p ∈ e₁.baseSet
rw : ((↑e₂ : Z → B × F) ((↑e₁.symm : B × F → Z) (proj p, ((↑e₁ : Z → B × F) p).2))).2 = ((↑e₂ : Z → B × F) p).2
⊢ e₁.coordChange e₂ (proj p) ((↑e₁ : Z → B × F) p).2 = ((↑e₂ : Z → B × F) p).2
have rw₁ : ((↑e₂ : Z → B × F) p).2 = ((↑e₂ : Z → B × F) p).2
Tactic: rw [coordChange, e₁.symm_apply_mk_proj (e₁.mem_source.2 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 : Trivialization F proj
b : B
h : b ∈ e.baseSet
x : F
⊢ e.coordChange e b x = x
have rw : ((↑e : Z → B × F) ((↑e.symm : B × F → Z) (b, x))).2 = x
Tactic: rw [coordChange, e.apply_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
inst_2 : TopologicalSpace Z
e : Trivialization F proj
b : B
h : b ∈ e.baseSet
x : F
rw : ((↑e : Z → B × F) ((↑e.symm : B × F → Z) (b, x))).2 = x
⊢ e.coordChange e b x = x
have rw₁ : (b, x).2 = x
Tactic: rw [coordChange, e.apply_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
inst_2 : TopologicalSpace Z
e₁ e₂ e₃ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ e₂.coordChange e₃ b (e₁.coordChange e₂ b x) = e₁.coordChange e₃ b x
have rw : (↑e₁.symm : B × F → Z) (b, x) ∈ e₂.source
Tactic: rw [coordChange, e₁.mk_coordChange _ h₁ h₂, ← e₂.coe_coe, e₂.left_inv, coordChange]
-- 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₂ e₃ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ (↑e₁.symm : B × F → Z) (b, x) ∈ e₂.source
have rwa : proj ((↑e₁.symm : B × F → Z) (b, x)) ∈ e₂.baseSet
Tactic: rwa [e₂.mem_source, 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
inst_2 : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
⊢ Continuous[inst_1, inst_1] (e₁.coordChange e₂ b)
have refine_1 : Continuous[inst_1, instTopologicalSpaceProd] (Prod.mk b)
Tactic: refine continuous_snd.comp (e₂.toOpenPartialHomeomorph.continuousOn.comp_continuous
    (e₁.toOpenPartialHomeomorph.continuousOn_symm.comp_continuous ?_ ?_) ?_)
-- 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
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
refine_1 : Continuous[inst_1, instTopologicalSpaceProd] (Prod.mk b)
⊢ Continuous[inst_1, inst_1] (e₁.coordChange e₂ b)
have refine_2 : ∀ (x : F), (b, x) ∈ e₁.target
Tactic: refine continuous_snd.comp (e₂.toOpenPartialHomeomorph.continuousOn.comp_continuous
    (e₁.toOpenPartialHomeomorph.continuousOn_symm.comp_continuous ?_ ?_) ?_)
-- 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
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
refine_1 : Continuous[inst_1, instTopologicalSpaceProd] (Prod.mk b)
refine_2 : ∀ (x : F), (b, x) ∈ e₁.target
⊢ Continuous[inst_1, inst_1] (e₁.coordChange e₂ b)
have refine_3 : ∀ (x : F), (↑e₁.symm : B × F → Z) (b, x) ∈ e₂.source
Tactic: refine continuous_snd.comp (e₂.toOpenPartialHomeomorph.continuousOn.comp_continuous
    (e₁.toOpenPartialHomeomorph.continuousOn_symm.comp_continuous ?_ ?_) ?_)
-- 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
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ (↑e₁.symm : B × F → Z) (b, x) ∈ e₂.source
have refine_3 : proj ((↑e₁.symm : B × F → Z) (b, x)) ∈ e₂.baseSet
Tactic: rwa [e₂.mem_source, e₁.proj_symm_apply' h₁]
-- 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
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e : Trivialization F proj
s : Set B
inst_4 : Nonempty ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
z : { x : Z // x ∈ proj ⁻¹' s }
hz : Membership.mem (γ := Set { x : Z // x ∈ proj ⁻¹' s }) (fun (x : { x : Z // x ∈ proj ⁻¹' s }) ↦ e.source (↑x : Z)) z
⊢ (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id ∘
        (↑(e.toPretrivialization.restrictPreimage' s).toPartialEquiv :
          (↑(proj ⁻¹' s) : Type u_4) → (↑s : Type u_1) × F))
      z =
    ((↑e.toPartialEquiv : Z → B × F) ∘ Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s)) z
have fst : ((Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id ∘
        (↑(e.toPretrivialization.restrictPreimage' s).toPartialEquiv :
          (↑(proj ⁻¹' s) : Type u_4) → (↑s : Type u_1) × F))
      z).1 =
  (((↑e.toPartialEquiv : Z → B × F) ∘ Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s)) z).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 : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e : Trivialization F proj
s : Set B
inst_4 : Nonempty ((↑s : Type u_1) → F → (↑(proj ⁻¹' s) : Type u_4))
z : { x : Z // x ∈ proj ⁻¹' s }
hz : Membership.mem (γ := Set { x : Z // x ∈ proj ⁻¹' s }) (fun (x : { x : Z // x ∈ proj ⁻¹' s }) ↦ e.source (↑x : Z)) z
fst :
  ((Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id ∘
          (↑(e.toPretrivialization.restrictPreimage' s).toPartialEquiv :
            (↑(proj ⁻¹' s) : Type u_4) → (↑s : Type u_1) × F))
        z).1 =
    (((↑e.toPartialEquiv : Z → B × F) ∘ Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s)) z).1
⊢ (Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id ∘
        (↑(e.toPretrivialization.restrictPreimage' s).toPartialEquiv :
          (↑(proj ⁻¹' s) : Type u_4) → (↑s : Type u_1) × F))
      z =
    ((↑e.toPartialEquiv : Z → B × F) ∘ Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s)) z
have snd : ((Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id ∘
        (↑(e.toPretrivialization.restrictPreimage' s).toPartialEquiv :
          (↑(proj ⁻¹' s) : Type u_4) → (↑s : Type u_1) × F))
      z).2 =
  (((↑e.toPartialEquiv : Z → B × F) ∘ Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s)) z).2
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 : Z → B
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
s : Set B
hps : IsOpen[inst_2] (proj ⁻¹' s)
e : Trivialization.{u_1, u_2, u_4} (B := B) F fun (z : (↑(proj ⁻¹' s) : Type u_4)) ↦ proj (↑z : Z)
inst_4 : Nonempty (Z → F)
⊢ ContinuousOn
    ((↑e.toPretrivialization.domExtend (s := s).toPartialEquiv : Z → B × F) ∘
      Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s))
    e.toPretrivialization.source
have h : (↑e.toPretrivialization.domExtend (s := s).toPartialEquiv : Z → B × F) ∘
    Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) =
  (↑e.toPartialEquiv : (↑(proj ⁻¹' s) : Type u_4) → B × F)
Tactic: convert! e.continuousOn_toFun
-- 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
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
s : Set B
hps : IsOpen[inst_2] (proj ⁻¹' s)
e : Trivialization.{u_1, u_2, u_4} (B := B) F fun (z : (↑(proj ⁻¹' s) : Type u_4)) ↦ proj (↑z : Z)
inst_4 : Nonempty (Z → F)
⊢ (↑e.toPretrivialization.domExtend (s := s).toPartialEquiv : Z → B × F) ∘
      Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) =
    (↑e.toPartialEquiv : (↑(proj ⁻¹' s) : Type u_4) → B × F)
have h : ∀ (x : Z) (hx : proj x ∈ s),
  comp (α := { x : Z // x ∈ proj ⁻¹' s }) (↑e.toPretrivialization.domExtend (s := s).toPartialEquiv : Z → B × F)
      (Subtype.val (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s)) (Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) x hx) =
    (↑e.toPartialEquiv : (↑(proj ⁻¹' s) : Type u_4) → B × F) (Subtype.mk (p := fun (x : Z) ↦ x ∈ proj ⁻¹' s) x hx)
Tactic: ext1 ⟨x, (hx : proj x ∈ s)⟩
-- 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
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj_1
x : Z
e' : Trivialization (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 : Trivialization F proj
inst_4 : Nonempty (B → F → Z)
⊢ ContinuousOn
    ((Pretrivialization.codExtend' (s := s) hs e.toPretrivialization).invFun ∘
      Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id)
    e.toPretrivialization.target
have h : (Pretrivialization.codExtend' (s := s) hs e.toPretrivialization).invFun ∘
    Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id =
  e.invFun
Tactic: convert! e.continuousOn_invFun
-- 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
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj_1
x : Z
e' : Trivialization (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 : Trivialization F proj
inst_4 : Nonempty (B → F → Z)
⊢ (Pretrivialization.codExtend' (s := s) hs e.toPretrivialization).invFun ∘
      Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id =
    e.invFun
have h : ∀ (x : Prod.{u_1, u_2} { x : B // x ∈ s } F),
  ((Pretrivialization.codExtend' (s := s) hs e.toPretrivialization).invFun ∘
        Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id)
      x =
    e.invFun x
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
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj_1
x : Z
e' : Trivialization (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 : Trivialization F proj
inst_4 : Nonempty (B → F → Z)
x_1 : Prod.{u_1, u_2} { x : B // x ∈ s } F
⊢ ((Pretrivialization.codExtend' (s := s) hs e.toPretrivialization).invFun ∘
        Prod.map (Subtype.val (p := fun (x : B) ↦ x ∈ s)) id)
      x_1 =
    e.invFun x_1
have h : (↑e.toPretrivialization.symm : (↑s : Type u_1) × F → Z) x_1 = (↑e.symm : (↑s : Type u_1) × F → Z) x_1
Tactic: simp [Pretrivialization.codExtend']
-- 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 : Trivialization F proj
s : Set B
⊢ e.source ∩ frontier (proj ⁻¹' s) = proj ⁻¹' (e.baseSet ∩ frontier s)
have rw : e.source ∩ (↑e.toOpenPartialHomeomorph : Z → B × F) ⁻¹' frontier (SProd.sprod (β := Set F) s univ) =
  proj ⁻¹' (e.baseSet ∩ frontier s)
Tactic: rw [← (e.isImage_preimage_prod s).frontier.preimage_eq, frontier_prod_univ_eq,
    (e.isImage_preimage_prod _).preimage_eq, e.source_eq, preimage_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
inst_2 : TopologicalSpace Z
e : Trivialization F proj
s : Set B
rw :
  e.source ∩ (↑e.toOpenPartialHomeomorph : Z → B × F) ⁻¹' frontier (SProd.sprod (β := Set F) s univ) =
    proj ⁻¹' (e.baseSet ∩ frontier s)
⊢ e.source ∩ frontier (proj ⁻¹' s) = proj ⁻¹' (e.baseSet ∩ frontier s)
have rw₁ : e.source ∩ (↑e.toOpenPartialHomeomorph : Z → B × F) ⁻¹' SProd.sprod (β := Set F) (frontier s) univ =
  proj ⁻¹' (e.baseSet ∩ frontier s)
Tactic: rw [← (e.isImage_preimage_prod s).frontier.preimage_eq, frontier_prod_univ_eq,
    (e.isImage_preimage_prod _).preimage_eq, e.source_eq, preimage_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
inst_2 : TopologicalSpace Z
e : Trivialization F proj
s : Set B
rw :
  e.source ∩ (↑e.toOpenPartialHomeomorph : Z → B × F) ⁻¹' frontier (SProd.sprod (β := Set F) s univ) =
    proj ⁻¹' (e.baseSet ∩ frontier s)
rw₁ :
  e.source ∩ (↑e.toOpenPartialHomeomorph : Z → B × F) ⁻¹' SProd.sprod (β := Set F) (frontier s) univ =
    proj ⁻¹' (e.baseSet ∩ frontier s)
⊢ e.source ∩ frontier (proj ⁻¹' s) = proj ⁻¹' (e.baseSet ∩ frontier s)
have rw₂ : e.source ∩ proj ⁻¹' frontier s = proj ⁻¹' (e.baseSet ∩ frontier s)
Tactic: rw [← (e.isImage_preimage_prod s).frontier.preimage_eq, frontier_prod_univ_eq,
    (e.isImage_preimage_prod _).preimage_eq, e.source_eq, preimage_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
inst_2 : TopologicalSpace Z
e : Trivialization F proj
s : Set B
rw :
  e.source ∩ (↑e.toOpenPartialHomeomorph : Z → B × F) ⁻¹' frontier (SProd.sprod (β := Set F) s univ) =
    proj ⁻¹' (e.baseSet ∩ frontier s)
rw₁ :
  e.source ∩ (↑e.toOpenPartialHomeomorph : Z → B × F) ⁻¹' SProd.sprod (β := Set F) (frontier s) univ =
    proj ⁻¹' (e.baseSet ∩ frontier s)
rw₂ : e.source ∩ proj ⁻¹' frontier s = proj ⁻¹' (e.baseSet ∩ frontier s)
⊢ e.source ∩ frontier (proj ⁻¹' s) = proj ⁻¹' (e.baseSet ∩ frontier s)
have rw₃ : proj ⁻¹' e.baseSet ∩ proj ⁻¹' frontier s = proj ⁻¹' (e.baseSet ∩ frontier s)
Tactic: rw [← (e.isImage_preimage_prod s).frontier.preimage_eq, frontier_prod_univ_eq,
    (e.isImage_preimage_prod _).preimage_eq, e.source_eq, preimage_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
inst_2 : TopologicalSpace Z
e : Trivialization F proj
s : Set B
rw :
  e.source ∩ (↑e.toOpenPartialHomeomorph : Z → B × F) ⁻¹' frontier (SProd.sprod (β := Set F) s univ) =
    proj ⁻¹' (e.baseSet ∩ frontier s)
rw₁ :
  e.source ∩ (↑e.toOpenPartialHomeomorph : Z → B × F) ⁻¹' SProd.sprod (β := Set F) (frontier s) univ =
    proj ⁻¹' (e.baseSet ∩ frontier s)
rw₂ : e.source ∩ proj ⁻¹' frontier s = proj ⁻¹' (e.baseSet ∩ frontier s)
rw₃ : proj ⁻¹' e.baseSet ∩ proj ⁻¹' frontier s = proj ⁻¹' (e.baseSet ∩ frontier s)
⊢ e.source ∩ frontier (proj ⁻¹' s) = proj ⁻¹' (e.baseSet ∩ frontier s)
have rw₄ : proj ⁻¹' e.baseSet ∩ proj ⁻¹' frontier s = proj ⁻¹' e.baseSet ∩ proj ⁻¹' frontier s
Tactic: rw [← (e.isImage_preimage_prod s).frontier.preimage_eq, frontier_prod_univ_eq,
    (e.isImage_preimage_prod _).preimage_eq, e.source_eq, preimage_inter]
-- 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
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e e' : Trivialization F proj
s : Set B
Hs : e.baseSet ∩ frontier s = e'.baseSet ∩ frontier s
Heq : EqOn (↑e : Z → B × F) (↑e' : Z → B × F) (proj ⁻¹' (e.baseSet ∩ frontier s))
⊢ e.source ∩ frontier (proj ⁻¹' s) = e'.source ∩ frontier (proj ⁻¹' s)
have rw : proj ⁻¹' (e.baseSet ∩ frontier s) = e'.source ∩ frontier (proj ⁻¹' s)
Tactic: rw [e.frontier_preimage, e'.frontier_preimage, Hs]
-- 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
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e e' : Trivialization F proj
s : Set B
Hs : e.baseSet ∩ frontier s = e'.baseSet ∩ frontier s
Heq : EqOn (↑e : Z → B × F) (↑e' : Z → B × F) (proj ⁻¹' (e.baseSet ∩ frontier s))
rw : proj ⁻¹' (e.baseSet ∩ frontier s) = e'.source ∩ frontier (proj ⁻¹' s)
⊢ e.source ∩ frontier (proj ⁻¹' s) = e'.source ∩ frontier (proj ⁻¹' s)
have rw₁ : proj ⁻¹' (e.baseSet ∩ frontier s) = proj ⁻¹' (e'.baseSet ∩ frontier s)
Tactic: rw [e.frontier_preimage, e'.frontier_preimage, Hs]
-- 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
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e e' : Trivialization F proj
s : Set B
Hs : e.baseSet ∩ frontier s = e'.baseSet ∩ frontier s
Heq : EqOn (↑e : Z → B × F) (↑e' : Z → B × F) (proj ⁻¹' (e.baseSet ∩ frontier s))
rw : proj ⁻¹' (e.baseSet ∩ frontier s) = e'.source ∩ frontier (proj ⁻¹' s)
rw₁ : proj ⁻¹' (e.baseSet ∩ frontier s) = proj ⁻¹' (e'.baseSet ∩ frontier s)
⊢ e.source ∩ frontier (proj ⁻¹' s) = e'.source ∩ frontier (proj ⁻¹' s)
have rw₂ : proj ⁻¹' (e'.baseSet ∩ frontier s) = proj ⁻¹' (e'.baseSet ∩ frontier s)
Tactic: rw [e.frontier_preimage, e'.frontier_preimage, Hs]
-- 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
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
e e' : Trivialization F proj
s : Set B
Hs : e.baseSet ∩ frontier s = e'.baseSet ∩ frontier s
Heq : EqOn (↑e : Z → B × F) (↑e' : Z → B × F) (proj ⁻¹' (e.baseSet ∩ frontier s))
⊢ EqOn (↑e.toOpenPartialHomeomorph : Z → B × F) (↑e'.toOpenPartialHomeomorph : Z → B × F)
    (e.source ∩ frontier (proj ⁻¹' s))
have rwa : EqOn (↑e.toOpenPartialHomeomorph : Z → B × F) (↑e'.toOpenPartialHomeomorph : Z → B × F)
  (proj ⁻¹' (e.baseSet ∩ frontier s))
Tactic: rwa [e.frontier_preimage]
-- 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
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x_1 : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
inst_4 : LinearOrder B
inst_5 : OrderTopology B
e e' : Trivialization F proj
a : B
He : a ∈ e.baseSet
He' : a ∈ e'.baseSet
Heq : ∀ (p : Z), proj p = a → (↑e : Z → B × F) p = (↑e' : Z → B × F) p
x : B
hx : x ∈ frontier (Iic a)
⊢ x ∈ e.baseSet ↔ x ∈ e'.baseSet
have He₁ : x ∈ e.baseSet
Tactic: obtain rfl : x = a := mem_singleton_iff.1 (frontier_Iic_subset _ hx)
Cleared hypotheses: a, He, He', Heq, hx
-- 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
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x_1 : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
inst_4 : LinearOrder B
inst_5 : OrderTopology B
e e' : Trivialization F proj
a : B
He : a ∈ e.baseSet
He' : a ∈ e'.baseSet
Heq : ∀ (p : Z), proj p = a → (↑e : Z → B × F) p = (↑e' : Z → B × F) p
x : B
hx : x ∈ frontier (Iic a)
He₁ : x ∈ e.baseSet
⊢ x ∈ e.baseSet ↔ x ∈ e'.baseSet
have He'₁ : x ∈ e'.baseSet
Tactic: obtain rfl : x = a := mem_singleton_iff.1 (frontier_Iic_subset _ hx)
Cleared hypotheses: a, He, He', Heq, hx
-- 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
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace (TotalSpace F E)
e_1 : Trivialization F proj
x_1 : Z
e'_1 : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
b : B
y : E b
inst_4 : LinearOrder B
inst_5 : OrderTopology B
e e' : Trivialization F proj
a : B
He : a ∈ e.baseSet
He' : a ∈ e'.baseSet
Heq : ∀ (p : Z), proj p = a → (↑e : Z → B × F) p = (↑e' : Z → B × F) p
x : B
hx : x ∈ frontier (Iic a)
He₁ : x ∈ e.baseSet
He'₁ : x ∈ e'.baseSet
⊢ x ∈ e.baseSet ↔ x ∈ e'.baseSet
have Heq₁ : ∀ (p : Z), proj p = x → (↑e : Z → B × F) p = (↑e' : Z → B × F) p
Tactic: obtain rfl : x = a := mem_singleton_iff.1 (frontier_Iic_subset _ hx)
Cleared hypotheses: a, He, He', Heq, hx