awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tangent (goal)
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'
this : IsManifold I (HAdd.hAdd (α := ℕ∞ω) 0 1) M
i j k : (↑(atlas H M) : Type (max u_4 u_6))
x : M
hxk : x ∈ (↑k : OpenPartialHomeomorph M H).source
hxi : x ∈ (↑i : OpenPartialHomeomorph M H).source
hxj : x ∈ (↑j : OpenPartialHomeomorph M H).source
v : E
hy :
  (↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E)
      ((↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M)
        ((↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) x)) =
    (↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) x
⊢ ((↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) ∘ (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
      ((↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) x) =
    (↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) x
have hy₁ : (↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) x = (↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) x
Tactic: rw [Function.comp_apply, i.1.extend_left_inv hxi]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tangent (goal)
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 z : M
v : E
h : z ∈ (extChartAt I x).source
⊢ (tangentCoordChange I x x z : (a : E) → E) v = v
have a : z ∈ VectorBundleCore.baseSet (ι := (↑(atlas H M) : Type (max u_4 u_6))) (tangentBundleCore I M) (achart H x)
Tactic: apply (tangentBundleCore I M).coordChange_self
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tangent (goal)
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
w x y z : M
v : E
h : z ∈ (extChartAt I w).source ∩ (extChartAt I x).source ∩ (extChartAt I y).source
⊢ Eq (α := E) ((tangentCoordChange I x y z : (a : E) → E) ((tangentCoordChange I w x z : (a : E) → E) v : E) : E)
    ((tangentCoordChange I w y z : (a : E) → E) v : E)
have a : z ∈
  VectorBundleCore.baseSet (ι := (↑(atlas H M) : Type (max u_4 u_6))) (tangentBundleCore I M) (achart H w) ∩
      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: apply (tangentBundleCore I M).coordChange_comp
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tangent (goal)
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).symm ≫ extChartAt I y).source
have rw : (↑(extChartAt I x) : M → E) z ∈ (↑(extChartAt I x) : M → E) '' ((extChartAt I x).source ∩ (extChartAt I y).source)
Tactic: rw [PartialEquiv.trans_source'', PartialEquiv.symm_symm, PartialEquiv.symm_target]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tangent (goal)
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 (tangentCoordChange I x y) ((extChartAt I x).source ∩ (extChartAt I y).source)
have h : (extChartAt I x).source =
  VectorBundleCore.baseSet (ι := (↑(atlas H M) : Type (max u_4 u_6))) (tangentBundleCore I M) (achart H x)
Tactic: convert! (tangentBundleCore I M).continuousOn_coordChange (achart H x) (achart H y)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tangent (goal)
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)
⊢ ContinuousOn (tangentCoordChange I x y) ((extChartAt I x).source ∩ (extChartAt I y).source)
have h₁ : (extChartAt I y).source =
  VectorBundleCore.baseSet (ι := (↑(atlas H M) : Type (max u_4 u_6))) (tangentBundleCore I M) (achart H y)
Tactic: convert! (tangentBundleCore I M).continuousOn_coordChange (achart H x) (achart H y)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tangent (goal)
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
⊢ 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
have 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
Tactic: simp only [FiberBundle.chartedSpace_chartAt, mfld_simps]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tangent (goal)
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)))).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
have 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
Tactic: rw [PartialEquiv.prod_symm]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tangent (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_8
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
b b' : F
⊢ Eq (α := F →L[𝕜] TangentSpace 𝓘(𝕜, F) b')
    (Trivialization.symmL 𝕜 (E := TangentSpace 𝓘(𝕜, F)) (trivializationAt F (TangentSpace 𝓘(𝕜, F)) b) b') 1
have rw : b' ∈ (toPartialEquiv (chartAt F b)).source
Tactic: rw [TangentBundle.symmL_trivializationAt_eq_core, coordChange_model_space]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tangent (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_8
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
b b' : F
⊢ Eq (α := TangentSpace 𝓘(𝕜, F) b' →L[𝕜] F)
    (Trivialization.continuousLinearMapAt 𝕜 (E := TangentSpace 𝓘(𝕜, F)) (trivializationAt F (TangentSpace 𝓘(𝕜, F)) b)
      b')
    1
have rw : b' ∈ (toPartialEquiv (chartAt F b)).source
Tactic: rw [TangentBundle.continuousLinearMapAt_trivializationAt_eq_core, coordChange_model_space]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tangent (hypothesis)
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
⊢ VectorBundleCore.IsContMDiff (ι := (↑(atlas H M) : Type (max u_4 u_6))) (tangentBundleCore I M) I n
have this : IsManifold I n M
Tactic: have : IsManifold I n M := .of_le (n := n + 1) (le_self_add)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tangent (goal)
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
have 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)
Tactic: refine ⟨fun i j => ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tangent (goal)
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))
⊢ 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)
have 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))
Tactic: rw [contMDiffOn_iff_source_of_mem_maximalAtlas (subset_maximalAtlas i.2),
    contMDiffOn_iff_contDiffOn]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tangent (goal)
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))
⊢ 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)
have rw₁ : VectorBundleCore.baseSet (tangentBundleCore I M) i ∩ VectorBundleCore.baseSet (tangentBundleCore I M) j ⊆
  (↑i : OpenPartialHomeomorph M H).source
Tactic: rw [contMDiffOn_iff_source_of_mem_maximalAtlas (subset_maximalAtlas i.2),
    contMDiffOn_iff_contDiffOn]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tangent (goal)
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))
have 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
Tactic: refine ((contDiffOn_fderiv_coord_change (I := I) i j).congr fun x hx => ?_).mono ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tangent (goal)
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
⊢ 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))
have 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
Tactic: refine ((contDiffOn_fderiv_coord_change (I := I) i j).congr fun x hx => ?_).mono ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tangent (hypothesis)
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
⊢ (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
have 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)
Tactic: rw [PartialEquiv.trans_source'] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tangent (goal)
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)
⊢ (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
have 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
Tactic: simp_rw [Function.comp_apply, tangentBundleCore_coordChange, (i.1.extend I).right_inv hx.1]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tangent (goal)
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
⊢ (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
have 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)
Tactic: simp_rw [Function.comp_apply, tangentBundleCore_coordChange, (i.1.extend I).right_inv hx.1]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tangent (hypothesis)
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
⊢ ContMDiffVectorBundle.{u_1, u_6, u_2, u_2, u_2, u_4} n (B := M) E (TangentSpace I) I
have this : IsManifold I 1 M
Tactic: have : IsManifold I 1 M := .of_le (n := n + 1) le_add_self
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tangent (hypothesis)
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
⊢ ContMDiffVectorBundle.{u_1, u_6, u_2, u_2, u_2, u_4} n (B := M) E (TangentSpace I) I
have this₁ : 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
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tangent (hypothesis)
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
⊢ ContMDiffVectorBundle.{u_1, u_6, u_2, u_2, u_2, u_4} ∞ (B := M) E (TangentSpace I) I
have this : IsManifold I (HAdd.hAdd (α := ℕ∞ω) ∞ 1) M
Tactic: have : IsManifold I (∞ + 1) M := h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tangent (hypothesis)
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
⊢ ContMDiffVectorBundle.{u_1, u_6, u_2, u_2, u_2, u_4} 1 (B := M) E (TangentSpace I) I
have this : IsManifold I (HAdd.hAdd (α := ℕ∞ω) 1 1) M
Tactic: have : IsManifold I (1 + 1) M := h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tangent (goal)
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
⊢ (↑(trivializationAt E (TangentSpace I) x) : TotalSpace E (TangentSpace I) → H × E) p =
    (p.proj (E := TangentSpace I), p.snd (E := TangentSpace I))
have 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))
Tactic: simp only [TangentBundle.trivializationAt_apply]