awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x y z : M
h : z ∈ (extChartAt I x).source ∩ (extChartAt I y).source
rw : (↑(extChartAt I x) : M → E) z ∈ (↑(extChartAt I x) : M → E) '' ((extChartAt I x).source ∩ (extChartAt I y).source)
⊢ (↑(extChartAt I x) : M → E) z ∈ ((extChartAt I x).symm ≫ extChartAt I y).source

Tactic:
rw [PartialEquiv.trans_source'', PartialEquiv.symm_symm, PartialEquiv.symm_target]

Premises used: PartialEquiv.symm_symm, PartialEquiv.trans_source'', PartialEquiv.symm_target
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x y z : M
h : z ∈ (extChartAt I x).source ∩ (extChartAt I y).source
⊢ (↑(extChartAt I x) : M → E) z ∈ (↑(extChartAt I x) : M → E) '' ((extChartAt I x).source ∩ (extChartAt I y).source)

Tactic:
mem_image_of_mem _ h

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x y z : M
h : z ∈ (extChartAt I x).source ∩ (extChartAt I y).source
⊢ (↑(extChartAt I x) : M → E) z ∈ (↑(extChartAt I x) : M → E) '' ((extChartAt I x).source ∩ (extChartAt I y).source)

Tactic:
exact mem_image_of_mem _ h

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x y : M
⊢ ContinuousOn
    (VectorBundleCore.coordChange (ι := (↑(atlas H M) : Type (max u_4 u_6))) (tangentBundleCore I M) (achart H x)
      (achart H y))
    (VectorBundleCore.baseSet (ι := (↑(atlas H M) : Type (max u_4 u_6))) (tangentBundleCore I M) (achart H x) ∩
      VectorBundleCore.baseSet (ι := (↑(atlas H M) : Type (max u_4 u_6))) (tangentBundleCore I M) (achart H y))

Tactic:
(tangentBundleCore I M).continuousOn_coordChange (achart H x) (achart H y)

Premises used: achart, tangentBundleCore, VectorBundleCore.continuousOn_coordChange
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x y : M
h :
  (extChartAt I x).source =
    VectorBundleCore.baseSet (ι := (↑(atlas H M) : Type (max u_4 u_6))) (tangentBundleCore I M) (achart H x)
h₁ :
  (extChartAt I y).source =
    VectorBundleCore.baseSet (ι := (↑(atlas H M) : Type (max u_4 u_6))) (tangentBundleCore I M) (achart H y)
⊢ ContinuousOn (tangentCoordChange I x y) ((extChartAt I x).source ∩ (extChartAt I y).source)

Tactic:
convert! (tangentBundleCore I M).continuousOn_coordChange (achart H x) (achart H y)

Premises used: achart, tangentBundleCore, VectorBundleCore.continuousOn_coordChange
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x y : M
⊢ (extChartAt I x).source =
    VectorBundleCore.baseSet (ι := (↑(atlas H M) : Type (max u_4 u_6))) (tangentBundleCore I M) (achart H x)

Tactic:
simp only [tangentBundleCore_baseSet, coe_achart, ← extChartAt_source I]

Premises used: coe_achart, extChartAt_source, tangentBundleCore_baseSet
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x y : M
⊢ (extChartAt I y).source =
    VectorBundleCore.baseSet (ι := (↑(atlas H M) : Type (max u_4 u_6))) (tangentBundleCore I M) (achart H y)

Tactic:
simp only [tangentBundleCore_baseSet, coe_achart, ← extChartAt_source I]

Premises used: coe_achart, extChartAt_source, tangentBundleCore_baseSet
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H : Type u_4
inst_5 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
F : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
inst_13 : IsManifold I 1 M
inst_14 : IsManifold I' 1 M'
⊢ VectorBundle.{u_1, u_6, u_2, u_2} 𝕜 (B := M) E (TangentSpace I)

Tactic:
inferInstanceAs <| VectorBundle 𝕜 E (tangentBundleCore I M).Fiber

Premises used: _private.0.TangentSpace.vectorBundle._proof_1
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
p : TM
⊢ Eq (α := OpenPartialHomeomorph TM (ModelProd H E)) (chartAt (ModelProd H E) p)
    (Trivialization.toOpenPartialHomeomorph
        (FiberBundleCore.localTriv (VectorBundleCore.toFiberBundleCore (tangentBundleCore I M))
          (achart H (p.proj (E := TangentSpace I)))) ≫ₕ
      OpenPartialHomeomorph.prod (chartAt H (p.proj (E := TangentSpace I))) (OpenPartialHomeomorph.refl E))

Tactic:
rfl

Premises used: achart, FiberBundleCore.Fiber, instTopologicalSpaceModelProd._aux_1, TangentSpace, ModelProd, rfl
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
p : TM
⊢ toPartialEquiv (chartAt (ModelProd H E) p) =
    FiberBundleCore.localTrivAsPartialEquiv (VectorBundleCore.toFiberBundleCore (tangentBundleCore I M))
        (achart H (p.proj (E := TangentSpace I))) ≫
      (toPartialEquiv (chartAt H (p.proj (E := TangentSpace I)))).prod (PartialEquiv.refl E)

Tactic:
rfl

Premises used: Equiv.toPartialEquivOfImageEq, achart, PartialEquiv.prod, FiberBundleCore.Fiber, PartialEquiv.restr, PartialEquiv.trans, PartialEquiv.symm, OpenPartialHomeomorph.toFun', Equiv.toPartialEquiv, FiberBundleCore.localTrivAsPartialEquiv, TangentSpace, PartialEquiv.IsImage.restr, Equiv.refl, PartialEquiv.refl, ModelProd, PartialEquiv.trans', rfl
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x : M
⊢ Eq (α :=
    Trivialization (B := M) E (Z := TotalSpace.{u_6, u_2, u_2} (B := M) E (TangentSpace I))
      (TotalSpace.proj (E := TangentSpace I)))
    (trivializationAt E (TangentSpace I) x)
    (FiberBundleCore.localTriv (VectorBundleCore.toFiberBundleCore (tangentBundleCore I M)) (achart H x))

Tactic:
rfl

Premises used: achart, FiberBundleCore.localTriv, FiberBundleCore.localTrivAt, rfl
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x : M
⊢ Eq (α := Set (TotalSpace.{u_6, u_2, u_2} (B := M) E (TangentSpace I)))
    (PartialEquiv.source
      (toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt E (TangentSpace I) x))))
    (TotalSpace.proj (E := TangentSpace I) ⁻¹' (toPartialEquiv (chartAt H x)).source)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x : M
⊢ PartialEquiv.target (α := TotalSpace.{u_6, u_2, u_2} (B := M) E (TangentSpace I))
      (toPartialEquiv (Trivialization.toOpenPartialHomeomorph (trivializationAt E (TangentSpace I) x))) =
    SProd.sprod (β := Set E) (toPartialEquiv (chartAt H x)).source univ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x : M
⊢ Trivialization.baseSet (Z := TotalSpace.{u_6, u_2, u_2} (B := M) E (TangentSpace I))
      (trivializationAt E (TangentSpace I) x) =
    (toPartialEquiv (chartAt H x)).source

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x : M
z : TM
⊢ (↑(trivializationAt E (TangentSpace I) x) : TotalSpace E (TangentSpace I) → M × E) z =
    (z.proj (E := TangentSpace I),
      (fderivWithin 𝕜
            ((↑(extend (chartAt H x) I) : M → E) ∘
              (↑(extend (chartAt H (z.proj (E := TangentSpace I))) I).symm : E → M))
            (range (↑I : H → E))
            ((↑(extend (chartAt H (z.proj (E := TangentSpace I))) I) : M → E) (z.proj (E := TangentSpace I))) :
          (a : E) → E)
        (z.snd (E := TangentSpace I)))

Tactic:
rfl

Premises used: Bundle.Trivialization.toFun', rfl
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x : M
z : TM
⊢ ((↑(trivializationAt E (TangentSpace I) x) : TotalSpace E (TangentSpace I) → M × E) z).1 =
    z.proj (E := TangentSpace I)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
p q : TM
⊢ p ∈ PartialEquiv.source (β := ModelProd H E) (toPartialEquiv (chartAt (ModelProd H E) q)) ↔
    p.proj (E := TangentSpace I) ∈ (toPartialEquiv (chartAt H (q.proj (E := TangentSpace I)))).source

Tactic:
simp only [FiberBundle.chartedSpace_chartAt, mfld_simps]

Premises used: FiberBundle.chartedSpace_chartAt
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
p : H × E
q : TM
simp :
  p.1 ∈ (toPartialEquiv (chartAt H (q.proj (E := TangentSpace I)))).target ∧
      ((↑((toPartialEquiv (chartAt H (q.proj (E := TangentSpace I)))).prod (PartialEquiv.refl E)).symm :
              ModelProd H E → M × E)
            p).1 ∈
        (toPartialEquiv (chartAt H (q.proj (E := TangentSpace I)))).source ↔
    p.1 ∈ (toPartialEquiv (chartAt H (q.proj (E := TangentSpace I)))).target
⊢ Membership.mem (γ := Set (ModelProd H E)) (PartialEquiv.target (toPartialEquiv (chartAt (ModelProd H E) q))) p ↔
    p.1 ∈ (toPartialEquiv (chartAt H (q.proj (E := TangentSpace I)))).target

Tactic:
simp only [FiberBundle.chartedSpace_chartAt, mfld_simps]

Premises used: FiberBundle.chartedSpace_chartAt
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
p : H × E
q : TM
rw :
  p.1 ∈ (toPartialEquiv (chartAt H (q.proj (E := TangentSpace I)))).target ∧
      ((↑((toPartialEquiv (chartAt H (q.proj (E := TangentSpace I)))).symm.prod (PartialEquiv.refl E).symm) :
              ModelProd H E → M × E)
            p).1 ∈
        (toPartialEquiv (chartAt H (q.proj (E := TangentSpace I)))).source ↔
    p.1 ∈ (toPartialEquiv (chartAt H (q.proj (E := TangentSpace I)))).target
⊢ p.1 ∈ (toPartialEquiv (chartAt H (q.proj (E := TangentSpace I)))).target ∧
      ((↑((toPartialEquiv (chartAt H (q.proj (E := TangentSpace I)))).prod (PartialEquiv.refl E)).symm :
              ModelProd H E → M × E)
            p).1 ∈
        (toPartialEquiv (chartAt H (q.proj (E := TangentSpace I)))).source ↔
    p.1 ∈ (toPartialEquiv (chartAt H (q.proj (E := TangentSpace I)))).target

Tactic:
rw [PartialEquiv.prod_symm]

Premises used: PartialEquiv.prod_symm
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
p : H × E
q : TM
⊢ p.1 ∈ (toPartialEquiv (chartAt H (q.proj (E := TangentSpace I)))).target ∧
      ((↑((toPartialEquiv (chartAt H (q.proj (E := TangentSpace I)))).symm.prod (PartialEquiv.refl E).symm) :
              ModelProd H E → M × E)
            p).1 ∈
        (toPartialEquiv (chartAt H (q.proj (E := TangentSpace I)))).source ↔
    p.1 ∈ (toPartialEquiv (chartAt H (q.proj (E := TangentSpace I)))).target

Tactic:
simp +contextual only [and_iff_left_iff_imp, mfld_simps]

Premises used: and_iff_left_iff_imp
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
p q : TM
⊢ ((↑(chartAt (ModelProd H E) q) : TM → ModelProd H E) p).1 =
    (↑(chartAt H (q.proj (E := TangentSpace I))) : M → H) (p.proj (E := TangentSpace I))

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', rfl
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
p : H × E
q : TM
⊢ ((↑(OpenPartialHomeomorph.symm (chartAt (ModelProd H E) q)) : ModelProd H E → TM) p).proj (E := TangentSpace I) =
    (↑(OpenPartialHomeomorph.symm (chartAt H (q.proj (E := TangentSpace I)))) : H → M) p.1

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', rfl
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
b₀ b : M
hb : b ∈ (toPartialEquiv (chartAt H b₀)).source
⊢ Trivialization.continuousLinearMapAt 𝕜 (E := TangentSpace I) (trivializationAt E (TangentSpace I) b₀) b =
    VectorBundleCore.coordChange (ι := (↑(atlas H M) : Type (max u_4 u_6))) (tangentBundleCore I M) (achart H b)
      (achart H b₀) b

Tactic:
simp [hb]
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
b₀ b : M
hb : b ∈ (toPartialEquiv (chartAt H b₀)).source
⊢ Trivialization.symmL 𝕜 (E := TangentSpace I) (trivializationAt E (TangentSpace I) b₀) b =
    VectorBundleCore.coordChange (ι := (↑(atlas H M) : Type (max u_4 u_6))) (tangentBundleCore I M) (achart H b₀)
      (achart H b) b

Tactic:
simp [hb]
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_8
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
b b' x : F
⊢ Eq (α := F →L[𝕜] F)
    (VectorBundleCore.coordChange (ι := (↑(atlas F F) : Type u_8)) (tangentBundleCore 𝓘(𝕜, F) F) (achart F b)
      (achart F b') x)
    1

Tactic:
simpa only [tangentBundleCore_coordChange, mfld_simps] using
    fderivWithin_id uniqueDiffWithinAt_univ

Premises used: fderivWithin_id, tangentBundleCore_coordChange, uniqueDiffWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_8
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
b b' : F
rw : b' ∈ (toPartialEquiv (chartAt F b)).source
⊢ Eq (α := F →L[𝕜] TangentSpace 𝓘(𝕜, F) b')
    (Trivialization.symmL 𝕜 (E := TangentSpace 𝓘(𝕜, F)) (trivializationAt F (TangentSpace 𝓘(𝕜, F)) b) b') 1

Tactic:
rw [TangentBundle.symmL_trivializationAt_eq_core, coordChange_model_space]

Premises used: TangentBundle.symmL_trivializationAt_eq_core, TangentBundle.coordChange_model_space
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_8
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
b b' : F
⊢ b' ∈ (toPartialEquiv (chartAt F b)).source

Tactic:
apply mem_univ

Premises used: Set.mem_univ
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_8
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
b b' : F
rw : b' ∈ (toPartialEquiv (chartAt F b)).source
⊢ Eq (α := TangentSpace 𝓘(𝕜, F) b' →L[𝕜] F)
    (Trivialization.continuousLinearMapAt 𝕜 (E := TangentSpace 𝓘(𝕜, F)) (trivializationAt F (TangentSpace 𝓘(𝕜, F)) b)
      b')
    1

Tactic:
rw [TangentBundle.continuousLinearMapAt_trivializationAt_eq_core, coordChange_model_space]

Premises used: TangentBundle.continuousLinearMapAt_trivializationAt_eq_core, TangentBundle.coordChange_model_space
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
h : IsManifold I (n + 1) M
⊢ IsManifold I n M

Tactic:
have : IsManifold I n M := .of_le (n := n + 1) (le_self_add)
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
h : IsManifold I (n + 1) M
this : IsManifold I n M
⊢ VectorBundleCore.IsContMDiff (ι := (↑(atlas H M) : Type (max u_4 u_6))) (tangentBundleCore I M) I n

Tactic:
⟨fun i j => ?_⟩

Premises used: VectorBundleCore.IsContMDiff.mk
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
h : IsManifold I (n + 1) M
this : IsManifold I n M
refine :
  ∀ (i j : (↑(atlas H M) : Type (max u_4 u_6))),
    ContMDiffOn I (E' := E →L[𝕜] E) 𝓘(𝕜, E →L[𝕜] E) n (VectorBundleCore.coordChange (tangentBundleCore I M) i j)
      (VectorBundleCore.baseSet (tangentBundleCore I M) i ∩ VectorBundleCore.baseSet (tangentBundleCore I M) j)
⊢ VectorBundleCore.IsContMDiff (ι := (↑(atlas H M) : Type (max u_4 u_6))) (tangentBundleCore I M) I n

Tactic:
refine ⟨fun i j => ?_⟩
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
h : IsManifold I (n + 1) M
this : IsManifold I n M
i j : (↑(atlas H M) : Type (max u_4 u_6))
rw :
  ContDiffOn 𝕜 n
    (VectorBundleCore.coordChange (tangentBundleCore I M) i j ∘
      (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
    ((↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) ''
      (VectorBundleCore.baseSet (tangentBundleCore I M) i ∩ VectorBundleCore.baseSet (tangentBundleCore I M) j))
rw₁ :
  VectorBundleCore.baseSet (tangentBundleCore I M) i ∩ VectorBundleCore.baseSet (tangentBundleCore I M) j ⊆
    (↑i : OpenPartialHomeomorph M H).source
⊢ ContMDiffOn I (E' := E →L[𝕜] E) 𝓘(𝕜, E →L[𝕜] E) n (VectorBundleCore.coordChange (tangentBundleCore I M) i j)
    (VectorBundleCore.baseSet (tangentBundleCore I M) i ∩ VectorBundleCore.baseSet (tangentBundleCore I M) j)

Tactic:
rw [contMDiffOn_iff_source_of_mem_maximalAtlas (subset_maximalAtlas i.2),
    contMDiffOn_iff_contDiffOn]

Premises used: contMDiffOn_iff_contDiffOn, contMDiffOn_iff_source_of_mem_maximalAtlas, IsManifold.subset_maximalAtlas, Subtype.property
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
h : IsManifold I (n + 1) M
this : IsManifold I n M
i j : (↑(atlas H M) : Type (max u_4 u_6))
⊢ ContDiffOn 𝕜 n
    (VectorBundleCore.coordChange (tangentBundleCore I M) i j ∘
      (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
    ((↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) ''
      (VectorBundleCore.baseSet (tangentBundleCore I M) i ∩ VectorBundleCore.baseSet (tangentBundleCore I M) j))

Tactic:
((contDiffOn_fderiv_coord_change (I := I) i j).congr fun x hx => ?_).mono ?_

Premises used: ContDiffOn.congr, ContDiffOn.mono, contDiffOn_fderiv_coord_change