awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target} e
ee' : e' ≈ e
A : e'.symm ≈ e.symm
⊢ PG.property (↑e.symm : H → H) e'.symm.source
have h : e'.symm.source = e.target
Tactic: convert! he.2 using 1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target} e
ee' : e' ≈ e
A : e'.symm ≈ e.symm
⊢ e'.symm.source = e.target
have h : e.symm.source = e.target
Tactic: rw [A.1, symm_toPartialEquiv, PartialEquiv.symm_source]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target} e
ee' : e' ≈ e
A : e'.symm ≈ e.symm
h : e.symm.source = e.target
⊢ e'.symm.source = e.target
have h₁ : e.symm.source = e.target
Tactic: rw [A.1, symm_toPartialEquiv, PartialEquiv.symm_source]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target} e
ee' : e' ≈ e
A : e'.symm ≈ e.symm
h : e.symm.source = e.target
h₁ : e.symm.source = e.target
⊢ e'.symm.source = e.target
have h₂ : e.target = e.target
Tactic: rw [A.1, symm_toPartialEquiv, PartialEquiv.symm_source]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
PG₁ PG₂ : Pregroupoid H
h : ∀ (f : H → H) (s : Set H), PG₁.property f s → PG₂.property f s
⊢ PG₁.groupoid ≤ PG₂.groupoid
have refine : ∀ (e : OpenPartialHomeomorph H H) (he : e ∈ PG₁.groupoid), e ∈ PG₂.groupoid
Tactic: refine StructureGroupoid.le_iff.2 fun e he ↦ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (hypothesis)
Goal:
H : Type u_1
inst : TopologicalSpace H
PG₁ PG₂ : Pregroupoid H
h : ∀ (f : H → H) (s : Set H), PG₁.property f s → PG₂.property f s
e : OpenPartialHomeomorph H H
he : e ∈ PG₁.groupoid
⊢ e ∈ PG₂.groupoid
have he₁ : PG₁.property (↑e : H → H) e.source ∧ PG₁.property (↑e.symm : H → H) e.target
Tactic: rw [mem_groupoid_of_pregroupoid] at he ⊢
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he' : e ≈ e'
he : PG.property (↑e : H → H) e.source
⊢ PG.property (↑e' : H → H) e'.source
have rw : PG.property (↑e' : H → H) e.source
Tactic: rw [← he'.1]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst] s
hse : e ≈ ofSet s hs
s' : Set H
hs' : IsOpen[inst] s'
hse' : e' ≈ ofSet s' hs'
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | ∃ (s : Set H) (h : IsOpen[inst] s), e ≈ ofSet s h} (e ≫ₕ e')
have refine : e ≫ₕ e' ≈ ofSet (s ∩ s') sorry
Tactic: refine ⟨s ∩ s', hs.inter hs', ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (hypothesis)
Goal:
H : Type u_1
inst : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst] s
hse : e ≈ ofSet s hs
s' : Set H
hs' : IsOpen[inst] s'
hse' : e' ≈ ofSet s' hs'
⊢ e ≫ₕ e' ≈ ofSet (s ∩ s') ⋯
have this : e ≫ₕ e' ≈ ofSet s hs ≫ₕ ofSet s' hs'
Tactic: have := OpenPartialHomeomorph.EqOnSource.trans' hse hse'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst] s
hse : e ≈ ofSet s hs
s' : Set H
hs' : IsOpen[inst] s'
hse' : e' ≈ ofSet s' hs'
this : e ≫ₕ e' ≈ ofSet s hs ≫ₕ ofSet s' hs'
⊢ e ≫ₕ e' ≈ ofSet (s ∩ s') ⋯
have rwa : ∀ (this : e ≫ₕ e' ≈ ofSet (s ∩ s') sorry), e ≫ₕ e' ≈ ofSet (s ∩ s') sorry
Tactic: rwa [OpenPartialHomeomorph.ofSet_trans_ofSet] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst] s
hse : e ≈ ofSet s hs
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | ∃ (s : Set H) (h : IsOpen[inst] s), e ≈ ofSet s h} e.symm
have refine : e.symm ≈ ofSet s hs
Tactic: refine ⟨s, hs, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst] s
hse : e ≈ ofSet s hs
⊢ e.symm ≈ ofSet s hs
have rw : e.symm ≈ (ofSet s hs).symm
Tactic: rw [← ofSet_symm]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
e : OpenPartialHomeomorph H H
h :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            {e : OpenPartialHomeomorph H H | ∃ (s : Set H) (h : IsOpen[inst] s), e ≈ ofSet s h} (e.restr s)
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | ∃ (s : Set H) (h : IsOpen[inst] s), e ≈ ofSet s h} e
have refine : EqOn (↑e : H → H) (↑(ofSet e.source sorry) : H → H) e.source
Tactic: refine ⟨e.source, e.open_source, by simp only [mfld_simps], ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
e : OpenPartialHomeomorph H H
h :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            {e : OpenPartialHomeomorph H H | ∃ (s : Set H) (h : IsOpen[inst] s), e ≈ ofSet s h} (e.restr s)
x : H
hx : x ∈ e.source
⊢ (↑e : H → H) x = (↑(ofSet e.source ⋯) : H → H) x
have rcases : ∀ (s : Set H) (hs : IsOpen[inst] s) (hxs : x ∈ s) (s' : Set H) (hs' : IsOpen[inst] s')
  (hes' : e.restr s ≈ ofSet s' hs'), (↑e : H → H) x = (↑(ofSet e.source sorry) : H → H) x
Tactic: rcases h x hx with ⟨s, hs, hxs, s', hs', hes'⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
e : OpenPartialHomeomorph H H
h :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            {e : OpenPartialHomeomorph H H | ∃ (s : Set H) (h : IsOpen[inst] s), e ≈ ofSet s h} (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
hs : IsOpen[inst] s
hxs : x ∈ s
s' : Set H
hs' : IsOpen[inst] s'
hes' : e.restr s ≈ ofSet s' hs'
⊢ x ∈ e.source ∩ interior s
have refine : x ∈ interior s
Tactic: refine ⟨hx, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (hypothesis)
Goal:
H : Type u_1
inst : TopologicalSpace H
e : OpenPartialHomeomorph H H
h :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            {e : OpenPartialHomeomorph H H | ∃ (s : Set H) (h : IsOpen[inst] s), e ≈ ofSet s h} (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
hs : IsOpen[inst] s
hxs : x ∈ s
s' : Set H
hs' : IsOpen[inst] s'
hes' : e.restr s ≈ ofSet s' hs'
⊢ (↑e : H → H) x = (↑(ofSet e.source ⋯) : H → H) x
have hes : x ∈ (e.restr s).source
Tactic: have hes : x ∈ (e.restr s).source := by
      rw [e.restr_source]
      refine ⟨hx, ?_⟩
      rw [hs.interior_eq]
      exact hxs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
e : OpenPartialHomeomorph H H
s' : Set H
hs' : IsOpen[inst] s'
he : e ≈ ofSet s' hs'
s : Set H
hs : IsOpen[inst] s
⊢ Membership.mem (γ := StructureGroupoid H) idRestrGroupoid (e.restr s)
have h : e.restr s ≈ ofSet (s' ∩ s) sorry
Tactic: use s' ∩ s, hs'.inter hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
e : OpenPartialHomeomorph H H
s' : Set H
hs' : IsOpen[inst] s'
he : e ≈ ofSet s' hs'
s : Set H
hs : IsOpen[inst] s
⊢ e.restr s ≈ ofSet (s' ∩ s) ⋯
have h : (ofSet s' hs').restr s ≈ ofSet (s' ∩ s) sorry
Tactic: refine Setoid.trans (OpenPartialHomeomorph.EqOnSource.restr he s) ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
⊢ ClosedUnderRestriction G ↔ idRestrGroupoid ≤ G
have mp : ClosedUnderRestriction G → idRestrGroupoid ≤ G
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
mp : ClosedUnderRestriction G → idRestrGroupoid ≤ G
⊢ ClosedUnderRestriction G ↔ idRestrGroupoid ≤ G
have mpr : idRestrGroupoid ≤ G → ClosedUnderRestriction G
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst] s
hes : e ≈ ofSet s hs
⊢ e ∈ G
have mp : ofSet s hs ∈ G
Tactic: refine G.mem_of_eqOnSource ?_ hes
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst] s
hes : e ≈ ofSet s hs
⊢ ofSet s hs ∈ G
have h : ofSet s hs = OpenPartialHomeomorph.restr (OpenPartialHomeomorph.refl H) s
Tactic: convert! closedUnderRestriction' G.id_mem hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst] s
hes : e ≈ ofSet s hs
⊢ ofSet s hs = OpenPartialHomeomorph.restr (OpenPartialHomeomorph.refl H) s
have h : ∀ (x : H), (↑(ofSet s hs) : H → H) x = (↑(OpenPartialHomeomorph.restr (OpenPartialHomeomorph.refl H) s) : H → H) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst] s
hes : e ≈ ofSet s hs
h : ∀ (x : H), (↑(ofSet s hs) : H → H) x = (↑(OpenPartialHomeomorph.restr (OpenPartialHomeomorph.refl H) s) : H → H) x
⊢ ofSet s hs = OpenPartialHomeomorph.restr (OpenPartialHomeomorph.refl H) s
have h₁ : ∀ (x : H),
  (↑(ofSet s hs).symm : H → H) x =
    (↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.restr (OpenPartialHomeomorph.refl H) s)) : H → H) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst] s
hes : e ≈ ofSet s hs
h : ∀ (x : H), (↑(ofSet s hs) : H → H) x = (↑(OpenPartialHomeomorph.restr (OpenPartialHomeomorph.refl H) s) : H → H) x
h₁ :
  ∀ (x : H),
    (↑(ofSet s hs).symm : H → H) x =
      (↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.restr (OpenPartialHomeomorph.refl H) s)) : H → H) x
⊢ ofSet s hs = OpenPartialHomeomorph.restr (OpenPartialHomeomorph.refl H) s
have h₂ : ∀ (x : H),
  x ∈ (ofSet s hs).source ↔ x ∈ (toPartialEquiv (OpenPartialHomeomorph.restr (OpenPartialHomeomorph.refl H) s)).source
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
⊢ ClosedUnderRestriction G
have mpr : ∀ {e : OpenPartialHomeomorph H H}, e ∈ G → ∀ (s : Set H), IsOpen[inst] s → e.restr s ∈ G
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
e : OpenPartialHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen[inst] s
⊢ e.restr s ∈ G
have mpr : ofSet s hs ≫ₕ e ∈ G
Tactic: rw [← ofSet_trans (e : OpenPartialHomeomorph H H) hs]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
e : OpenPartialHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen[inst] s
⊢ ofSet s hs ≫ₕ e ∈ G
have mpr : ofSet s hs ∈ G
Tactic: refine G.trans ?_ he
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
e : OpenPartialHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen[inst] s
⊢ ofSet s hs ∈ G
have mpr : Membership.mem (γ := StructureGroupoid H) idRestrGroupoid (ofSet s hs)
Tactic: apply StructureGroupoid.le_iff.mp h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace F
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
HB : Type u_7
inst_3 : TopologicalSpace HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : FiberBundle F E
x : TotalSpace F E
⊢ Eq (α := OpenPartialHomeomorph (TotalSpace F E) (ModelProd HB F)) (chartAt (ModelProd HB F) x)
    (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))) ≫ₕ
      OpenPartialHomeomorph.prod (chartAt HB (x.proj (E := E))) (OpenPartialHomeomorph.refl F))
have dsimp : Eq (α := OpenPartialHomeomorph (TotalSpace F E) (ModelProd HB F))
  (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))) ≫ₕ
    OpenPartialHomeomorph.prod
      (chartAt HB
        ((↑(Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E)))) : TotalSpace F E → B × F)
            x).1)
      (OpenPartialHomeomorph.refl F))
  (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))) ≫ₕ
    OpenPartialHomeomorph.prod (chartAt HB (x.proj (E := E))) (OpenPartialHomeomorph.refl F))
Tactic: dsimp only [chartAt_comp, prodChartedSpace_chartAt, FiberBundle.chartedSpace'_chartAt,
    chartAt_self_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace F
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
HB : Type u_7
inst_3 : TopologicalSpace HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : FiberBundle F E
x : TotalSpace F E
⊢ Eq (α := OpenPartialHomeomorph (TotalSpace F E) (ModelProd HB F))
    (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))) ≫ₕ
      OpenPartialHomeomorph.prod
        (chartAt HB
          ((↑(Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E)))) : TotalSpace F E → B × F)
              x).1)
        (OpenPartialHomeomorph.refl F))
    (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))) ≫ₕ
      OpenPartialHomeomorph.prod (chartAt HB (x.proj (E := E))) (OpenPartialHomeomorph.refl F))
have rw : Eq (α := OpenPartialHomeomorph (TotalSpace F E) (ModelProd HB F))
  (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))) ≫ₕ
    OpenPartialHomeomorph.prod (chartAt HB ((↑(trivializationAt F E (x.proj (E := E))) : TotalSpace F E → B × F) x).1)
      (OpenPartialHomeomorph.refl F))
  (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))) ≫ₕ
    OpenPartialHomeomorph.prod (chartAt HB (x.proj (E := E))) (OpenPartialHomeomorph.refl F))
Tactic: rw [Trivialization.coe_coe, Trivialization.coe_fst' _ (mem_baseSet_trivializationAt F E x.proj)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace F
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
HB : Type u_7
inst_3 : TopologicalSpace HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : FiberBundle F E
x : TotalSpace F E
rw :
  Eq (α := OpenPartialHomeomorph (TotalSpace F E) (ModelProd HB F))
    (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))) ≫ₕ
      OpenPartialHomeomorph.prod (chartAt HB ((↑(trivializationAt F E (x.proj (E := E))) : TotalSpace F E → B × F) x).1)
        (OpenPartialHomeomorph.refl F))
    (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))) ≫ₕ
      OpenPartialHomeomorph.prod (chartAt HB (x.proj (E := E))) (OpenPartialHomeomorph.refl F))
⊢ Eq (α := OpenPartialHomeomorph (TotalSpace F E) (ModelProd HB F))
    (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))) ≫ₕ
      OpenPartialHomeomorph.prod
        (chartAt HB
          ((↑(Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E)))) : TotalSpace F E → B × F)
              x).1)
        (OpenPartialHomeomorph.refl F))
    (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))) ≫ₕ
      OpenPartialHomeomorph.prod (chartAt HB (x.proj (E := E))) (OpenPartialHomeomorph.refl F))
have rw₁ : Eq (α := OpenPartialHomeomorph (TotalSpace F E) (ModelProd HB F))
  (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))) ≫ₕ
    OpenPartialHomeomorph.prod (chartAt HB (x.proj (E := E))) (OpenPartialHomeomorph.refl F))
  (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))) ≫ₕ
    OpenPartialHomeomorph.prod (chartAt HB (x.proj (E := E))) (OpenPartialHomeomorph.refl F))
Tactic: rw [Trivialization.coe_coe, Trivialization.coe_fst' _ (mem_baseSet_trivializationAt F E x.proj)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace F
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
HB : Type u_7
inst_3 : TopologicalSpace HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : FiberBundle F E
x : TotalSpace F E
y : ModelProd HB F
hy : Membership.mem (γ := Set (ModelProd HB F)) (PartialEquiv.target (toPartialEquiv (chartAt (ModelProd HB F) x))) y
⊢ ((↑(OpenPartialHomeomorph.symm (chartAt (ModelProd HB F) x)) : ModelProd HB F → TotalSpace F E) y).proj (E := E) =
    (↑(OpenPartialHomeomorph.symm (chartAt HB (x.proj (E := E)))) : HB → B) y.1
have simp : ∀
  (hy :
    y ∈
      SProd.sprod (β := Set F) (toPartialEquiv (chartAt HB (x.proj (E := E)))).target univ ∩
        (fun (p : HB × F) ↦ ((↑(OpenPartialHomeomorph.symm (chartAt HB (x.proj (E := E)))) : HB → B) p.1, p.2)) ⁻¹'
          (toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))))).target),
  ((↑(OpenPartialHomeomorph.symm
                (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))) ≫ₕ
                  OpenPartialHomeomorph.prod (chartAt HB (x.proj (E := E))) (OpenPartialHomeomorph.refl F))) :
            ModelProd HB F → TotalSpace F E)
          y).proj
      (E := E) =
    (↑(OpenPartialHomeomorph.symm (chartAt HB (x.proj (E := E)))) : HB → B) y.1
Tactic: simp only [FiberBundle.chartedSpace_chartAt, mfld_simps] at hy ⊢
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_8 : TopologicalSpace B
inst_9 : ChartedSpace HB B
inst_10 : FiberBundle F E
x : TotalSpace F E
⊢ extChartAt (IB.prod 𝓘(𝕜, F)) x =
    toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E)))) ≫
      (extChartAt IB (x.proj (E := E))).prod (PartialEquiv.refl F)
have simp_rw : toPartialEquiv
      (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))) ≫ₕ
        OpenPartialHomeomorph.prod (chartAt HB (x.proj (E := E))) (OpenPartialHomeomorph.refl F)) ≫
    ModelWithCorners.toPartialEquiv (IB.prod 𝓘(𝕜, F)) =
  toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E)))) ≫
    (toPartialEquiv (chartAt HB (x.proj (E := E))) ≫ IB.toPartialEquiv).prod (PartialEquiv.refl F)
Tactic: simp_rw [extChartAt, FiberBundle.chartedSpace_chartAt, OpenPartialHomeomorph.extend]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_8 : TopologicalSpace B
inst_9 : ChartedSpace HB B
inst_10 : FiberBundle F E
x : TotalSpace F E
⊢ toPartialEquiv
        (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E))) ≫ₕ
          OpenPartialHomeomorph.prod (chartAt HB (x.proj (E := E))) (OpenPartialHomeomorph.refl F)) ≫
      ModelWithCorners.toPartialEquiv (IB.prod 𝓘(𝕜, F)) =
    toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E)))) ≫
      (toPartialEquiv (chartAt HB (x.proj (E := E))) ≫ IB.toPartialEquiv).prod (PartialEquiv.refl F)
have simp : toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E)))) ≫
    (toPartialEquiv (chartAt HB (x.proj (E := E)))).prod (PartialEquiv.refl F) ≫ IB.prod (PartialEquiv.refl F) =
  toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E)))) ≫
    (toPartialEquiv (chartAt HB (x.proj (E := E))) ≫ IB.toPartialEquiv).prod (PartialEquiv.refl F)
Tactic: simp only [PartialEquiv.trans_assoc, mfld_simps]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_8 : TopologicalSpace B
inst_9 : ChartedSpace HB B
inst_10 : FiberBundle F E
x : TotalSpace F E
⊢ toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E)))) ≫
      (toPartialEquiv (chartAt HB (x.proj (E := E)))).prod (PartialEquiv.refl F) ≫ IB.prod (PartialEquiv.refl F) =
    toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E)))) ≫
      (toPartialEquiv (chartAt HB (x.proj (E := E))) ≫ IB.toPartialEquiv).prod (PartialEquiv.refl F)
have rw : toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E)))) ≫
    (toPartialEquiv (chartAt HB (x.proj (E := E))) ≫ IB.toPartialEquiv).prod
      (PartialEquiv.refl F ≫ PartialEquiv.refl F) =
  toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt F E (x.proj (E := E)))) ≫
    (toPartialEquiv (chartAt HB (x.proj (E := E))) ≫ IB.toPartialEquiv).prod (PartialEquiv.refl F)
Tactic: rw [PartialEquiv.prod_trans, PartialEquiv.refl_trans]