awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
refine_1 :
  ∀ (x : E)
    (hx : x ∈ (((↑i : OpenPartialHomeomorph M H).extend I).symm ≫ (↑j : OpenPartialHomeomorph M H).extend I).source),
    (VectorBundleCore.coordChange (tangentBundleCore I M) i j ∘
          (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
        x =
      fderivWithin 𝕜
        ((↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) ∘
          (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
        (range (↑I : H → E)) x
refine_2 :
  (↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) ''
      (VectorBundleCore.baseSet (tangentBundleCore I M) i ∩ VectorBundleCore.baseSet (tangentBundleCore I M) j) ⊆
    (((↑i : OpenPartialHomeomorph M H).extend I).symm ≫ (↑j : OpenPartialHomeomorph M H).extend I).source
⊢ 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:
refine ((contDiffOn_fderiv_coord_change (I := I) i j).congr fun x hx => ?_).mono ?_

Premises used: ContDiffOn.congr, ContDiffOn.mono, contDiffOn_fderiv_coord_change
-- 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))
x : E
hx : x ∈ (((↑i : OpenPartialHomeomorph M H).extend I).symm ≫ (↑j : OpenPartialHomeomorph M H).extend I).source
⊢ x ∈
    ((↑i : OpenPartialHomeomorph M H).extend I).symm.source ∩
      (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M) ⁻¹'
        (((↑i : OpenPartialHomeomorph M H).extend I).symm.target ∩ ((↑j : OpenPartialHomeomorph M H).extend I).source)

Tactic:
rw [PartialEquiv.trans_source'] at hx

Premises used: PartialEquiv.trans_source'
-- 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))
x : E
hx :
  x ∈
    ((↑i : OpenPartialHomeomorph M H).extend I).symm.source ∩
      (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M) ⁻¹'
        (((↑i : OpenPartialHomeomorph M H).extend I).symm.target ∩ ((↑j : OpenPartialHomeomorph M H).extend I).source)
refine_1 :
  VectorBundleCore.coordChange (tangentBundleCore I M) i j
      ((↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M) x) =
    fderivWithin 𝕜
      ((↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) ∘
        (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
      (range (↑I : H → E)) x
refine_1₁ :
  Eq (α := E →L[𝕜] E)
    (fderivWithin 𝕜
      ((↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) ∘
        (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
      (range (↑I : H → E))
      ((↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E)
        ((↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M) x)))
    (fderivWithin 𝕜
      ((↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) ∘
        (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
      (range (↑I : H → E)) x)
⊢ (VectorBundleCore.coordChange (tangentBundleCore I M) i j ∘
        (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
      x =
    fderivWithin 𝕜
      ((↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) ∘
        (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
      (range (↑I : H → E)) x

Tactic:
simp_rw [Function.comp_apply, tangentBundleCore_coordChange, (i.1.extend I).right_inv hx.1]

Premises used: PartialEquiv.right_inv, tangentBundleCore_coordChange, And.left, Function.comp_apply, Subtype.val, OpenPartialHomeomorph.extend
-- 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))
⊢ (↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) ''
      (VectorBundleCore.baseSet (tangentBundleCore I M) i ∩ VectorBundleCore.baseSet (tangentBundleCore I M) j) ⊆
    (((↑i : OpenPartialHomeomorph M H).extend I).symm ≫ (↑j : OpenPartialHomeomorph M H).extend I).source

Tactic:
(i.1.extend_image_source_inter j.1).subset

Premises used: OpenPartialHomeomorph.extend_image_source_inter, Eq.subset, Subtype.val
-- 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))
⊢ (↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) ''
      (VectorBundleCore.baseSet (tangentBundleCore I M) i ∩ VectorBundleCore.baseSet (tangentBundleCore I M) j) ⊆
    (((↑i : OpenPartialHomeomorph M H).extend I).symm ≫ (↑j : OpenPartialHomeomorph M H).extend I).source

Tactic:
exact (i.1.extend_image_source_inter j.1).subset

Premises used: OpenPartialHomeomorph.extend_image_source_inter, Eq.subset, Subtype.val
-- 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))
⊢ VectorBundleCore.baseSet (tangentBundleCore I M) i ∩ VectorBundleCore.baseSet (tangentBundleCore I M) j ⊆
    (↑i : OpenPartialHomeomorph M H).source

Tactic:
apply inter_subset_left

Premises used: Set.inter_subset_left
-- 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 1 M

Tactic:
have : IsManifold I 1 M := .of_le (n := n + 1) le_add_self
-- 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 1 M
⊢ VectorBundleCore.IsContMDiff (ι := (↑(atlas H M) : Type (max u_4 u_6))) (tangentBundleCore I M) I n

Tactic:
have : (tangentBundleCore I M).IsContMDiff I n := tangentBundleCore.isContMDiff
-- 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_1 : IsManifold I 1 M
this : VectorBundleCore.IsContMDiff (ι := (↑(atlas H M) : Type (max u_4 u_6))) (tangentBundleCore I M) I n
⊢ ContMDiffVectorBundle.{u_1, u_6, u_2, u_2, u_2, u_4} n (B := M) E (TangentSpace I) I

Tactic:
(tangentBundleCore I M).instContMDiffVectorBundle

Premises used: VectorBundleCore.Fiber, FiberBundleCore.Fiber, VectorBundleCore.instContMDiffVectorBundle, VectorBundleCore.moduleFiber._aux_1, VectorBundleCore.topologicalSpaceFiber._aux_1, tangentBundleCore, VectorBundleCore.addCommGroupFiber._aux_4, TangentSpace, instTopologicalSpaceTangentSpace._aux_1, VectorBundleCore.addCommGroupFiber._aux_1, instAddCommGroupTangentSpace._aux_1, instAddCommGroupTangentSpace._aux_4
-- 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_1 : IsManifold I 1 M
this : VectorBundleCore.IsContMDiff (ι := (↑(atlas H M) : Type (max u_4 u_6))) (tangentBundleCore I M) I n
⊢ ContMDiffVectorBundle.{u_1, u_6, u_2, u_2, u_2, u_4} n (B := M) E (TangentSpace I) I

Tactic:
exact (tangentBundleCore I M).instContMDiffVectorBundle

Premises used: VectorBundleCore.instContMDiffVectorBundle, tangentBundleCore
-- 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'
h : IsManifold I ∞ M
⊢ IsManifold I (HAdd.hAdd (α := ℕ∞ω) ∞ 1) M

Tactic:
have : IsManifold I (∞ + 1) M := h
-- 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'
h : IsManifold I ∞ M
this : IsManifold I (HAdd.hAdd (α := ℕ∞ω) ∞ 1) M
⊢ ContMDiffVectorBundle.{u_1, u_6, u_2, u_2, u_2, u_4} ∞ (B := M) E (TangentSpace I) I

Tactic:
TangentBundle.contMDiffVectorBundle

Premises used: TangentBundle.contMDiffVectorBundle
-- 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'
h : IsManifold I ∞ M
this : IsManifold I (HAdd.hAdd (α := ℕ∞ω) ∞ 1) M
⊢ ContMDiffVectorBundle.{u_1, u_6, u_2, u_2, u_2, u_4} ∞ (B := M) E (TangentSpace I) I

Tactic:
exact TangentBundle.contMDiffVectorBundle

Premises used: TangentBundle.contMDiffVectorBundle
-- 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'
inst_15 : IsManifold I ω M
⊢ ContMDiffVectorBundle.{u_1, u_6, u_2, u_2, u_2, u_4} ω (B := M) E (TangentSpace I) I

Tactic:
TangentBundle.contMDiffVectorBundle

Premises used: TangentBundle.contMDiffVectorBundle
-- 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'
h : IsManifold I 2 M
⊢ IsManifold I (HAdd.hAdd (α := ℕ∞ω) 1 1) M

Tactic:
have : IsManifold I (1 + 1) M := h
-- 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'
h : IsManifold I 2 M
this : IsManifold I (HAdd.hAdd (α := ℕ∞ω) 1 1) M
⊢ ContMDiffVectorBundle.{u_1, u_6, u_2, u_2, u_2, u_4} 1 (B := M) E (TangentSpace I) I

Tactic:
TangentBundle.contMDiffVectorBundle

Premises used: TangentBundle.contMDiffVectorBundle
-- 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'
h : IsManifold I 2 M
this : IsManifold I (HAdd.hAdd (α := ℕ∞ω) 1 1) M
⊢ ContMDiffVectorBundle.{u_1, u_6, u_2, u_2, u_2, u_4} 1 (B := M) E (TangentSpace I) I

Tactic:
exact TangentBundle.contMDiffVectorBundle

Premises used: TangentBundle.contMDiffVectorBundle
-- 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
p : TangentBundle I H
x : H
simp :
  (p.proj (E := TangentSpace I),
      (fderivWithin 𝕜
            ((↑(extend (chartAt H x) I) : H → E) ∘
              (↑(extend (chartAt H (p.proj (E := TangentSpace I))) I).symm : E → H))
            (range (↑I : H → E))
            ((↑(extend (chartAt H (p.proj (E := TangentSpace I))) I) : H → E) (p.proj (E := TangentSpace I))) :
          (a : E) → E)
        (p.snd (E := TangentSpace I))) =
    (p.proj (E := TangentSpace I), p.snd (E := TangentSpace I))
⊢ (↑(trivializationAt E (TangentSpace I) x) : TotalSpace E (TangentSpace I) → H × E) p =
    (p.proj (E := TangentSpace I), p.snd (E := TangentSpace I))

Tactic:
simp only [TangentBundle.trivializationAt_apply]

Premises used: TangentBundle.trivializationAt_apply
-- 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
p : TangentBundle I H
x : H
y : E
hy : y ∈ range (↑I : H → E)
⊢ ((↑I : H → E) ∘ (↑I.symm : E → H)) y = id y

Tactic:
simp [hy]
-- 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
p : TangentBundle I H
x : H
⊢ Eq (α := E →L[𝕜] E)
    (fderivWithin 𝕜 ((↑I : H → E) ∘ (↑I.symm : E → H)) (range (↑I : H → E))
      ((↑I : H → E) (p.proj (E := TangentSpace I))))
    (fderivWithin 𝕜 id (range (↑I : H → E)) ((↑I : H → E) (p.proj (E := TangentSpace I))))

Tactic:
have : fderivWithin 𝕜 (↑I ∘ ↑I.symm) (range I) (I p.proj) =
      fderivWithin 𝕜 id (range I) (I p.proj) :=
    fderivWithin_congr' (fun y hy ↦ by simp [hy]) (mem_range_self p.proj)
-- 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
p : TangentBundle I H
x : H
this :
  Eq (α := E →L[𝕜] E)
    (fderivWithin 𝕜 ((↑I : H → E) ∘ (↑I.symm : E → H)) (range (↑I : H → E))
      ((↑I : H → E) (p.proj (E := TangentSpace I))))
    (fderivWithin 𝕜 id (range (↑I : H → E)) ((↑I : H → E) (p.proj (E := TangentSpace I))))
⊢ (p.proj (E := TangentSpace I),
      (fderivWithin 𝕜
            ((↑(extend (chartAt H x) I) : H → E) ∘
              (↑(extend (chartAt H (p.proj (E := TangentSpace I))) I).symm : E → H))
            (range (↑I : H → E))
            ((↑(extend (chartAt H (p.proj (E := TangentSpace I))) I) : H → E) (p.proj (E := TangentSpace I))) :
          (a : E) → E)
        (p.snd (E := TangentSpace I))) =
    (p.proj (E := TangentSpace I), p.snd (E := TangentSpace I))

Tactic:
simp [this, fderivWithin_id (ModelWithCorners.uniqueDiffWithinAt_image I)]

Premises used: fderivWithin_id, ModelWithCorners.uniqueDiffWithinAt_image
-- 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
p : TangentBundle I H
h :
  ∀ (x : TangentBundle I H),
    (↑(toPartialEquiv (chartAt (ModelProd H E) p)) : TangentBundle I H → ModelProd H E) x =
      (↑(TotalSpace.toProd H E).toPartialEquiv : TangentBundle I H → ModelProd H E) x
hsymm :
  ∀ (x : ModelProd H E),
    (↑(PartialEquiv.symm (toPartialEquiv (chartAt (ModelProd H E) p))) : ModelProd H E → TangentBundle I H) x =
      (↑(TotalSpace.toProd H E).toPartialEquiv.symm : ModelProd H E → TangentBundle I H) x
hs :
  PartialEquiv.source (β := ModelProd H E) (toPartialEquiv (chartAt (ModelProd H E) p)) =
    (TotalSpace.toProd H E).toPartialEquiv.source
⊢ toPartialEquiv (chartAt (ModelProd H E) p) = (TotalSpace.toProd H E).toPartialEquiv

Tactic:
ext x : 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
p x : TangentBundle I H
h :
  ((↑(toPartialEquiv (chartAt (ModelProd H E) p)) : TangentBundle I H → ModelProd H E) x).1 =
    ((↑(TotalSpace.toProd H E).toPartialEquiv : TangentBundle I H → ModelProd H E) x).1
h₁ :
  ((↑(toPartialEquiv (chartAt (ModelProd H E) p)) : TangentBundle I H → ModelProd H E) x).2 =
    ((↑(TotalSpace.toProd H E).toPartialEquiv : TangentBundle I H → ModelProd H E) x).2
⊢ (↑(toPartialEquiv (chartAt (ModelProd H E) p)) : TangentBundle I H → ModelProd H E) x =
    (↑(TotalSpace.toProd H E).toPartialEquiv : TangentBundle I H → ModelProd H E) x

Tactic:
ext
-- 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
p x : TangentBundle I H
⊢ ((↑(toPartialEquiv (chartAt (ModelProd H E) p)) : TangentBundle I H → ModelProd H E) x).1 =
    ((↑(TotalSpace.toProd H E).toPartialEquiv : TangentBundle I H → ModelProd H E) x).1

Tactic:
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
p x : TangentBundle I H
⊢ ((↑(toPartialEquiv (chartAt (ModelProd H E) p)) : TangentBundle I H → ModelProd H E) x).2 =
    ((↑(TotalSpace.toProd H E).toPartialEquiv : TangentBundle I H → ModelProd H E) x).2

Tactic:
(tangentBundleCore I H).coordChange_self (achart _ x.1) x.1 (mem_achart_source H x.1) x.2

Premises used: VectorBundleCore.coordChange_self, achart, mem_achart_source, Bundle.TotalSpace.proj, tangentBundleCore, Bundle.TotalSpace.snd
-- 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
p x : TangentBundle I H
⊢ ((↑(toPartialEquiv (chartAt (ModelProd H E) p)) : TangentBundle I H → ModelProd H E) x).2 =
    ((↑(TotalSpace.toProd H E).toPartialEquiv : TangentBundle I H → ModelProd H E) x).2

Tactic:
exact (tangentBundleCore I H).coordChange_self (achart _ x.1) x.1 (mem_achart_source H x.1) x.2

Premises used: VectorBundleCore.coordChange_self, achart, mem_achart_source, Bundle.TotalSpace.proj, tangentBundleCore, Bundle.TotalSpace.snd
-- 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
p : TangentBundle I H
x : ModelProd H E
hsymm :
  ((↑(PartialEquiv.symm (toPartialEquiv (chartAt (ModelProd H E) p))) : ModelProd H E → TangentBundle I H) x).proj (E :=
      TangentSpace I) =
    ((↑(TotalSpace.toProd H E).toPartialEquiv.symm : ModelProd H E → TangentBundle I H) x).proj (E := TangentSpace I)
hsymm₁ :
  ((↑(PartialEquiv.symm (toPartialEquiv (chartAt (ModelProd H E) p))) : ModelProd H E → TangentBundle I H) x).snd (E :=
      TangentSpace I) ≍
    ((↑(TotalSpace.toProd H E).toPartialEquiv.symm : ModelProd H E → TangentBundle I H) x).snd (E := TangentSpace I)
⊢ (↑(PartialEquiv.symm (toPartialEquiv (chartAt (ModelProd H E) p))) : ModelProd H E → TangentBundle I H) x =
    (↑(TotalSpace.toProd H E).toPartialEquiv.symm : ModelProd H E → TangentBundle I H) x

Tactic:
ext
-- 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
p : TangentBundle I H
x : ModelProd H E
⊢ ((↑(PartialEquiv.symm (toPartialEquiv (chartAt (ModelProd H E) p))) : ModelProd H E → TangentBundle I H) x).proj (E :=
      TangentSpace I) =
    ((↑(TotalSpace.toProd H E).toPartialEquiv.symm : ModelProd H E → TangentBundle I H) x).proj (E := TangentSpace I)

Tactic:
rfl