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
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
x : ModelProd H E
y : TangentBundle I H
⊢ ∀
    x_1 ∈
      (extChartAt (I.prod 𝓘(𝕜, E)) x).target ∩
        (↑(extChartAt (I.prod 𝓘(𝕜, E)) x).symm : E × E → ModelProd H E) ⁻¹'
          (⇑(tangentBundleModelSpaceHomeomorph I).symm : (a : ModelProd H E) → TangentBundle I H) ⁻¹'
            (extChartAt I.tangent y).source,
    ((↑(extChartAt I.tangent y) : TangentBundle I H → E × E) ∘
          (⇑(tangentBundleModelSpaceHomeomorph I).symm : (a : ModelProd H E) → TangentBundle I H) ∘
            (↑(extChartAt (I.prod 𝓘(𝕜, E)) x).symm : E × E → ModelProd H E))
        x_1 =
      id x_1
have simp : ∀ (a b : E) (x : H) (h : (↑I : H → E) x = a),
  (↑I : H → E)
        (({
                toFun := fun (x : TotalSpace E fun (x : H) ↦ E) ↦
                  (x.proj (E := fun (x : H) ↦ E), x.snd (E := fun (x : H) ↦ E)),
                invFun := fun (x : H × E) ↦ ⟨x.1, x.2⟩, left_inv := sorry, right_inv := sorry :
                (TotalSpace E fun (x : H) ↦ E) ≃ H × E } :
              (a : TangentBundle I H) → ModelProd H E)
            ⟨((↑(I.prod (PartialEquiv.refl E)).symm : E × E → ModelProd H E) (a, b)).1,
              ((↑(I.prod (PartialEquiv.refl E)).symm : E × E → ModelProd H E) (a, b)).2⟩).1 =
      a ∧
    (({ toFun := fun (x : TotalSpace E fun (x : H) ↦ E) ↦ (x.proj (E := fun (x : H) ↦ E), x.snd (E := fun (x : H) ↦ E)),
              invFun := fun (x : H × E) ↦ ⟨x.1, x.2⟩, left_inv := sorry, right_inv := sorry :
              (TotalSpace E fun (x : H) ↦ E) ≃ H × E } :
            (a : TangentBundle I H) → ModelProd H E)
          ⟨((↑(I.prod (PartialEquiv.refl E)).symm : E × E → ModelProd H E) (a, b)).1,
            ((↑(I.prod (PartialEquiv.refl E)).symm : E × E → ModelProd H E) (a, b)).2⟩).2 =
      b
Tactic: simp only [mfld_simps, mem_range, TotalSpace.toProd, Equiv.coe_fn_symm_mk, forall_exists_index,
    Prod.forall, Prod.mk.injEq]
-- 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
⊢ ContMDiff I.tangent 𝓘(𝕜, E) (M' := E) n fun (p : TangentBundle I H) ↦ p.snd (E := TangentSpace I)
have change : ContMDiff I.tangent (M := TangentBundle I H) 𝓘(𝕜, E) (M' := E) n
  (Function.comp (β := ModelProd H E) (id Prod.snd)
    (⇑(tangentBundleModelSpaceHomeomorph I) : (a : TangentBundle I H) → ModelProd H E))
Tactic: change ContMDiff I.tangent 𝓘(𝕜, E) n
    ((id Prod.snd : ModelProd H E → E) ∘ (tangentBundleModelSpaceHomeomorph I))
-- 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
⊢ ContMDiff I.tangent (M := TangentBundle I H) 𝓘(𝕜, E) (M' := E) n
    (Function.comp (β := ModelProd H E) (id Prod.snd)
      (⇑(tangentBundleModelSpaceHomeomorph I) : (a : TangentBundle I H) → ModelProd H E))
have hg : ContMDiff (I.prod 𝓘(𝕜, E)) (M := ModelProd H E) 𝓘(𝕜, E) n (id Prod.snd)
Tactic: apply ContMDiff.comp (I' := I.prod 𝓘(𝕜, E))
-- 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
hg : ContMDiff (I.prod 𝓘(𝕜, E)) (M := ModelProd H E) 𝓘(𝕜, E) n (id Prod.snd)
⊢ ContMDiff I.tangent (M := TangentBundle I H) 𝓘(𝕜, E) (M' := E) n
    (Function.comp (β := ModelProd H E) (id Prod.snd)
      (⇑(tangentBundleModelSpaceHomeomorph I) : (a : TangentBundle I H) → ModelProd H E))
have hf : ContMDiff I.tangent (M := TangentBundle I H) (I.prod 𝓘(𝕜, E)) (M' := ModelProd H E) n
  (⇑(tangentBundleModelSpaceHomeomorph I) : (a : TangentBundle I H) → ModelProd H E)
Tactic: apply ContMDiff.comp (I' := I.prod 𝓘(𝕜, E))
-- 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
⊢ ContMDiff (I.prod 𝓘(𝕜, E)) (M := ModelProd H E) 𝓘(𝕜, E) n (id Prod.snd)
have h : instTopologicalSpaceModelProd H E = instTopologicalSpaceProd →
  Eq (α := ChartedSpace (ModelProd H E) (ModelProd H E)) (chartedSpaceSelf (ModelProd H E)) (prodChartedSpace H H E E)
Tactic: convert! contMDiff_snd
-- 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
h :
  instTopologicalSpaceModelProd H E = instTopologicalSpaceProd →
    Eq (α := ChartedSpace (ModelProd H E) (ModelProd H E)) (chartedSpaceSelf (ModelProd H E)) (prodChartedSpace H H E E)
⊢ ContMDiff (I.prod 𝓘(𝕜, E)) (M := ModelProd H E) 𝓘(𝕜, E) n (id Prod.snd)
have hg : ChartedSpace H H
Tactic: convert! contMDiff_snd
-- 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
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
s : Set E
x : E
⊢ ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' := TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E)))
      n (fun (x : E) ↦ ⟨x, V x⟩) s x ↔
    ContDiffWithinAt 𝕜 n V s x
have refine_1 : ∀
  (h :
    ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' :=
      TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) n (fun (x : E) ↦ ⟨x, V x⟩) s x),
  ContDiffWithinAt 𝕜 n V s x
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- 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
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
s : Set E
x : E
refine_1 :
  ∀
    (h :
      ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' :=
        TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E))) n (fun (x : E) ↦ ⟨x, V x⟩) s x),
    ContDiffWithinAt 𝕜 n V s x
⊢ ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' := TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E)))
      n (fun (x : E) ↦ ⟨x, V x⟩) s x ↔
    ContDiffWithinAt 𝕜 n V s x
have refine_2 : ∀ (h : ContDiffWithinAt 𝕜 n V s x),
  ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' := TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E)))
    n (fun (x : E) ↦ ⟨x, V x⟩) s x
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- 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
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
s : Set E
x : E
h : ContDiffWithinAt 𝕜 n V s x
⊢ ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' := TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E)))
    n (fun (x : E) ↦ ⟨x, V x⟩) s x
have refine_2 : ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) (M' := E) n (fun (x : E) ↦ ⟨x, V x⟩.proj (E := TangentSpace 𝓘(𝕜, E))) s x ∧
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) (M' := E) n
    (fun (x_1 : E) ↦
      ((↑(trivializationAt E (TangentSpace 𝓘(𝕜, E)) (⟨x, V x⟩.proj (E := TangentSpace 𝓘(𝕜, E)))) :
            TotalSpace E (TangentSpace 𝓘(𝕜, E)) → E × E)
          ⟨x_1, V x_1⟩).2)
    s x
Tactic: apply Bundle.contMDiffWithinAt_totalSpace.2
-- 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
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
s : Set E
x : E
h : ContDiffWithinAt 𝕜 n V s x
⊢ ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) (M' := E) n (fun (x : E) ↦ ⟨x, V x⟩.proj (E := TangentSpace 𝓘(𝕜, E))) s x ∧
    ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) (M' := E) n
      (fun (x_1 : E) ↦
        ((↑(trivializationAt E (TangentSpace 𝓘(𝕜, E)) (⟨x, V x⟩.proj (E := TangentSpace 𝓘(𝕜, E)))) :
              TotalSpace E (TangentSpace 𝓘(𝕜, E)) → E × E)
            ⟨x_1, V x_1⟩).2)
      s x
have refine_2 : ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) (M' := E) n
  (fun (x_1 : E) ↦
    ((↑(trivializationAt E (TangentSpace 𝓘(𝕜, E)) (⟨x, V x⟩.proj (E := TangentSpace 𝓘(𝕜, E)))) :
          TotalSpace E (TangentSpace 𝓘(𝕜, E)) → E × E)
        ⟨x_1, V x_1⟩).2)
  s x
Tactic: refine ⟨contMDiffWithinAt_id, ?_⟩
-- 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
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
s : Set E
x : E
h : ContDiffWithinAt 𝕜 n V s x
⊢ ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) (M' := E) n
    (fun (x_1 : E) ↦
      ((↑(trivializationAt E (TangentSpace 𝓘(𝕜, E)) (⟨x, V x⟩.proj (E := TangentSpace 𝓘(𝕜, E)))) :
            TotalSpace E (TangentSpace 𝓘(𝕜, E)) → E × E)
          ⟨x_1, V x_1⟩).2)
    s x
have h₁ : ∀ (y : E),
  ((↑(trivializationAt E (TangentSpace 𝓘(𝕜, E)) (⟨x, V x⟩.proj (E := TangentSpace 𝓘(𝕜, E)))) :
          TotalSpace E (TangentSpace 𝓘(𝕜, E)) → E × E)
        ⟨y, V y⟩).2 =
    V y
Tactic: convert! h.contMDiffWithinAt with 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
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'
x₀ x : H
y₀ y : H'
ϕ : E →L[𝕜] E'
⊢ inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x y₀ y ϕ = ϕ
have erw : VectorBundleCore.coordChange (ι := (↑(atlas H' H') : Type u_5)) (tangentBundleCore I' H')
      (VectorBundleCore.indexAt (tangentBundleCore I' H') y) (VectorBundleCore.indexAt (tangentBundleCore I' H') y₀)
      y ∘SL
    ϕ ∘SL
      VectorBundleCore.coordChange (ι := (↑(atlas H H) : Type u_4)) (tangentBundleCore I H)
        (VectorBundleCore.indexAt (tangentBundleCore I H) x₀) (VectorBundleCore.indexAt (tangentBundleCore I H) x) x =
  ϕ
Tactic: erw [VectorBundleCore.inCoordinates_eq]
-- 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
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'
x₀ x : H
y₀ y : H'
ϕ : E →L[𝕜] E'
erw :
  VectorBundleCore.coordChange (ι := (↑(atlas H' H') : Type u_5)) (tangentBundleCore I' H')
        (VectorBundleCore.indexAt (tangentBundleCore I' H') y) (VectorBundleCore.indexAt (tangentBundleCore I' H') y₀)
        y ∘SL
      ϕ ∘SL
        VectorBundleCore.coordChange (ι := (↑(atlas H H) : Type u_4)) (tangentBundleCore I H)
          (VectorBundleCore.indexAt (tangentBundleCore I H) x₀) (VectorBundleCore.indexAt (tangentBundleCore I H) x) x =
    ϕ
⊢ inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x y₀ y ϕ = ϕ
have hx : x ∈
  VectorBundleCore.baseSet (ι := (↑(atlas H H) : Type u_4)) (tangentBundleCore I H)
    (VectorBundleCore.indexAt (tangentBundleCore I H) x₀)
Tactic: erw [VectorBundleCore.inCoordinates_eq]
-- 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
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'
x₀ x : H
y₀ y : H'
ϕ : E →L[𝕜] E'
erw :
  VectorBundleCore.coordChange (ι := (↑(atlas H' H') : Type u_5)) (tangentBundleCore I' H')
        (VectorBundleCore.indexAt (tangentBundleCore I' H') y) (VectorBundleCore.indexAt (tangentBundleCore I' H') y₀)
        y ∘SL
      ϕ ∘SL
        VectorBundleCore.coordChange (ι := (↑(atlas H H) : Type u_4)) (tangentBundleCore I H)
          (VectorBundleCore.indexAt (tangentBundleCore I H) x₀) (VectorBundleCore.indexAt (tangentBundleCore I H) x) x =
    ϕ
hx :
  x ∈
    VectorBundleCore.baseSet (ι := (↑(atlas H H) : Type u_4)) (tangentBundleCore I H)
      (VectorBundleCore.indexAt (tangentBundleCore I H) x₀)
⊢ inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x y₀ y ϕ = ϕ
have hy : y ∈
  VectorBundleCore.baseSet (ι := (↑(atlas H' H') : Type u_5)) (tangentBundleCore I' H')
    (VectorBundleCore.indexAt (tangentBundleCore I' H') y₀)
Tactic: erw [VectorBundleCore.inCoordinates_eq]
-- 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
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'
x₀ x : H
y₀ y : H'
ϕ : E →L[𝕜] E'
⊢ VectorBundleCore.coordChange (ι := (↑(atlas H' H') : Type u_5)) (tangentBundleCore I' H')
        (VectorBundleCore.indexAt (tangentBundleCore I' H') y) (VectorBundleCore.indexAt (tangentBundleCore I' H') y₀)
        y ∘SL
      ϕ ∘SL
        VectorBundleCore.coordChange (ι := (↑(atlas H H) : Type u_4)) (tangentBundleCore I H)
          (VectorBundleCore.indexAt (tangentBundleCore I H) x₀) (VectorBundleCore.indexAt (tangentBundleCore I H) x) x =
    ϕ
have simp_rw : VectorBundleCore.coordChange (ι := (↑(atlas H' H') : Type u_5)) (tangentBundleCore I' H') (achart H' y) (achart H' y₀)
      y ∘SL
    ϕ ∘SL
      VectorBundleCore.coordChange (ι := (↑(atlas H H) : Type u_4)) (tangentBundleCore I H) (achart H x₀) (achart H x)
        x =
  ϕ
Tactic: simp_rw [tangentBundleCore_indexAt, tangentBundleCore_coordChange_model_space,
    ContinuousLinearMap.id_comp, ContinuousLinearMap.comp_id]
-- 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
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'
x₀ x : H
y₀ y : H'
ϕ : E →L[𝕜] E'
simp_rw :
  VectorBundleCore.coordChange (ι := (↑(atlas H' H') : Type u_5)) (tangentBundleCore I' H') (achart H' y) (achart H' y₀)
        y ∘SL
      ϕ ∘SL
        VectorBundleCore.coordChange (ι := (↑(atlas H H) : Type u_4)) (tangentBundleCore I H) (achart H x₀) (achart H x)
          x =
    ϕ
⊢ VectorBundleCore.coordChange (ι := (↑(atlas H' H') : Type u_5)) (tangentBundleCore I' H')
        (VectorBundleCore.indexAt (tangentBundleCore I' H') y) (VectorBundleCore.indexAt (tangentBundleCore I' H') y₀)
        y ∘SL
      ϕ ∘SL
        VectorBundleCore.coordChange (ι := (↑(atlas H H) : Type u_4)) (tangentBundleCore I H)
          (VectorBundleCore.indexAt (tangentBundleCore I H) x₀) (VectorBundleCore.indexAt (tangentBundleCore I H) x) x =
    ϕ
have simp_rw₁ : ContinuousLinearMap.id 𝕜 E' ∘SL ϕ ∘SL ContinuousLinearMap.id 𝕜 E = ϕ
Tactic: simp_rw [tangentBundleCore_indexAt, tangentBundleCore_coordChange_model_space,
    ContinuousLinearMap.id_comp, ContinuousLinearMap.comp_id]
-- 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
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'
x₀ x : H
y₀ y : H'
ϕ : E →L[𝕜] E'
simp_rw :
  VectorBundleCore.coordChange (ι := (↑(atlas H' H') : Type u_5)) (tangentBundleCore I' H') (achart H' y) (achart H' y₀)
        y ∘SL
      ϕ ∘SL
        VectorBundleCore.coordChange (ι := (↑(atlas H H) : Type u_4)) (tangentBundleCore I H) (achart H x₀) (achart H x)
          x =
    ϕ
simp_rw₁ : ContinuousLinearMap.id 𝕜 E' ∘SL ϕ ∘SL ContinuousLinearMap.id 𝕜 E = ϕ
⊢ VectorBundleCore.coordChange (ι := (↑(atlas H' H') : Type u_5)) (tangentBundleCore I' H')
        (VectorBundleCore.indexAt (tangentBundleCore I' H') y) (VectorBundleCore.indexAt (tangentBundleCore I' H') y₀)
        y ∘SL
      ϕ ∘SL
        VectorBundleCore.coordChange (ι := (↑(atlas H H) : Type u_4)) (tangentBundleCore I H)
          (VectorBundleCore.indexAt (tangentBundleCore I H) x₀) (VectorBundleCore.indexAt (tangentBundleCore I H) x) x =
    ϕ
have simp_rw₂ : ϕ ∘SL ContinuousLinearMap.id 𝕜 E = ϕ
Tactic: simp_rw [tangentBundleCore_indexAt, tangentBundleCore_coordChange_model_space,
    ContinuousLinearMap.id_comp, ContinuousLinearMap.comp_id]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tensoriality (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
A : Type u_9
inst_13 : AddCommGroup A
inst_14 : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F (V := V) Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if σ x' = σ' x' then 1 else 0
⊢ Φ σ = Φ σ'
have hψx : ψ x = 1
Tactic: have hψx : ψ x = 1 := by simp [ψ, hσσ'.self_of_nhds]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tensoriality (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
A : Type u_9
inst_13 : AddCommGroup A
inst_14 : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F (V := V) Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if σ x' = σ' x' then 1 else 0
hψx : ψ x = 1
x' : M
⊢ (ψ • σ) x' = (ψ • σ') x'
have dsimp : HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) (if σ x' = σ' x' then 1 else 0) (σ x') =
  HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) (if σ x' = σ' x' then 1 else 0) (σ' x')
Tactic: dsimp [ψ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tensoriality (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
A : Type u_9
inst_13 : AddCommGroup A
inst_14 : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F (V := V) Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if σ x' = σ' x' then 1 else 0
hψx : ψ x = 1
x' : M
⊢ HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) (if σ x' = σ' x' then 1 else 0) (σ x') =
    HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) (if σ x' = σ' x' then 1 else 0) (σ' x')
have pos : ∀ (hx' : σ x' = σ' x'), HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) 1 (σ x') = HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) 1 (σ' x')
Tactic: split_ifs with hx'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tensoriality (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
A : Type u_9
inst_13 : AddCommGroup A
inst_14 : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F (V := V) Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if σ x' = σ' x' then 1 else 0
hψx : ψ x = 1
x' : M
pos :
  ∀ (hx' : σ x' = σ' x'), HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) 1 (σ x') = HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) 1 (σ' x')
⊢ HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) (if σ x' = σ' x' then 1 else 0) (σ x') =
    HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) (if σ x' = σ' x' then 1 else 0) (σ' x')
have neg : ∀ (hx' : ¬σ x' = σ' x'), HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) 0 (σ x') = HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) 0 (σ' x')
Tactic: split_ifs with hx'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tensoriality (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
A : Type u_9
inst_13 : AddCommGroup A
inst_14 : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F (V := V) Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if σ x' = σ' x' then 1 else 0
hψx : ψ x = 1
⊢ Φ σ = Φ σ'
have this : ∀ (x' : M), (ψ • σ) x' = (ψ • σ') x'
Tactic: have (x' : M) : (ψ • σ) x' = (ψ • σ') x' := by
    dsimp [ψ]
    split_ifs with hx' <;> simp [hx']