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
apply :
  ∀ (x : TangentBundle I H) (y : ModelProd H E),
    ContDiffOn 𝕜 n
      ((↑(extChartAt (I.prod 𝓘(𝕜, E)) y) : ModelProd H E → E × E) ∘
        (⇑(tangentBundleModelSpaceHomeomorph I) : (a : TangentBundle I H) → ModelProd H E) ∘
          (↑(extChartAt I.tangent x).symm : E × E → TangentBundle I H))
      ((extChartAt I.tangent x).target ∩
        (↑(extChartAt I.tangent x).symm : E × E → TangentBundle I H) ⁻¹'
          (⇑(tangentBundleModelSpaceHomeomorph I) : (a : TangentBundle I H) → ModelProd H E) ⁻¹'
            (extChartAt (I.prod 𝓘(𝕜, E)) y).source)
⊢ 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_iff.2 ⟨Homeomorph.continuous _, fun x y ↦ ?_⟩

Premises used: Iff.mpr, Homeomorph.continuous, contMDiff_iff, And.intro
-- 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
x : TangentBundle I H
y : ModelProd H E
apply :
  ∀
    x_1 ∈
      (extChartAt I.tangent x).target ∩
        (↑(extChartAt I.tangent x).symm : E × E → TangentBundle I H) ⁻¹'
          (⇑(tangentBundleModelSpaceHomeomorph I) : (a : TangentBundle I H) → ModelProd H E) ⁻¹'
            (extChartAt (I.prod 𝓘(𝕜, E)) y).source,
    ((↑(extChartAt (I.prod 𝓘(𝕜, E)) y) : ModelProd H E → E × E) ∘
          (⇑(tangentBundleModelSpaceHomeomorph I) : (a : TangentBundle I H) → ModelProd H E) ∘
            (↑(extChartAt I.tangent x).symm : E × E → TangentBundle I H))
        x_1 =
      id x_1
⊢ ContDiffOn 𝕜 n
    ((↑(extChartAt (I.prod 𝓘(𝕜, E)) y) : ModelProd H E → E × E) ∘
      (⇑(tangentBundleModelSpaceHomeomorph I) : (a : TangentBundle I H) → ModelProd H E) ∘
        (↑(extChartAt I.tangent x).symm : E × E → TangentBundle I H))
    ((extChartAt I.tangent x).target ∩
      (↑(extChartAt I.tangent x).symm : E × E → TangentBundle I H) ⁻¹'
        (⇑(tangentBundleModelSpaceHomeomorph I) : (a : TangentBundle I H) → ModelProd H E) ⁻¹'
          (extChartAt (I.prod 𝓘(𝕜, E)) y).source)

Tactic:
apply contDiffOn_id.congr

Premises used: ContDiffOn.congr, contDiffOn_id
-- 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
x : TangentBundle I H
y : ModelProd H E
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 := ⋯, right_inv := ⋯ :
                  (TotalSpace E fun (x : H) ↦ E) ≃ H × E } :
                (a : TotalSpace E fun (x : H) ↦ E) → 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 := ⋯, right_inv := ⋯ :
                (TotalSpace E fun (x : H) ↦ E) ≃ H × E } :
              (a : TotalSpace E fun (x : H) ↦ E) → 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
⊢ ∀
    x_1 ∈
      (extChartAt I.tangent x).target ∩
        (↑(extChartAt I.tangent x).symm : E × E → TangentBundle I H) ⁻¹'
          (⇑(tangentBundleModelSpaceHomeomorph I) : (a : TangentBundle I H) → ModelProd H E) ⁻¹'
            (extChartAt (I.prod 𝓘(𝕜, E)) y).source,
    ((↑(extChartAt (I.prod 𝓘(𝕜, E)) y) : ModelProd H E → E × E) ∘
          (⇑(tangentBundleModelSpaceHomeomorph I) : (a : TangentBundle I H) → ModelProd H E) ∘
            (↑(extChartAt I.tangent x).symm : E × E → TangentBundle I H))
        x_1 =
      id x_1

Tactic:
simp only [mfld_simps, mem_range, TotalSpace.toProd, Equiv.coe_fn_symm_mk, forall_exists_index,
    Prod.forall, Prod.mk.injEq]

Premises used: Set.mem_range, Equiv.coe_fn_symm_mk, Bundle.TotalSpace.toProd, forall_exists_index, Prod.mk.injEq, Prod.forall
-- 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
x_1 : TangentBundle I H
y : ModelProd H E
b : E
x : H
⊢ (↑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 := ⋯, right_inv := ⋯ :
                (TotalSpace E fun (x : H) ↦ E) ≃ H × E } :
              (a : TotalSpace E fun (x : H) ↦ E) → H × E)
            ⟨((↑(I.prod (PartialEquiv.refl E)).symm : E × E → ModelProd H E) ((↑I : H → E) x, b)).1,
              ((↑(I.prod (PartialEquiv.refl E)).symm : E × E → ModelProd H E) ((↑I : H → E) x, b)).2⟩).1 =
      (↑I : H → E) x ∧
    (({ 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 := ⋯, right_inv := ⋯ :
              (TotalSpace E fun (x : H) ↦ E) ≃ H × E } :
            (a : TotalSpace E fun (x : H) ↦ E) → H × E)
          ⟨((↑(I.prod (PartialEquiv.refl E)).symm : E × E → ModelProd H E) ((↑I : H → E) x, b)).1,
            ((↑(I.prod (PartialEquiv.refl E)).symm : E × E → ModelProd H E) ((↑I : H → E) x, b)).2⟩).2 =
      b

Tactic:
simp [PartialEquiv.prod]

Premises used: PartialEquiv.prod
-- 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
apply :
  ∀ (x : ModelProd H E) (y : TangentBundle I H),
    ContDiffOn 𝕜 n
      ((↑(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))
      ((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)
⊢ ContMDiff (I.prod 𝓘(𝕜, E)) (M := ModelProd H E) I.tangent (M' := TangentBundle I H) n
    (⇑(tangentBundleModelSpaceHomeomorph I).symm : (a : ModelProd H E) → TangentBundle I H)

Tactic:
apply contMDiff_iff.2 ⟨Homeomorph.continuous _, fun x y ↦ ?_⟩

Premises used: Iff.mpr, Homeomorph.continuous, contMDiff_iff, And.intro
-- 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
x : ModelProd H E
y : TangentBundle I H
apply :
  ∀
    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
⊢ ContDiffOn 𝕜 n
    ((↑(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))
    ((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)

Tactic:
apply contDiffOn_id.congr

Premises used: ContDiffOn.congr, contDiffOn_id
-- 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
x : ModelProd H E
y : TangentBundle I H
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 := ⋯, right_inv := ⋯ :
                  (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 := ⋯, right_inv := ⋯ :
                (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
⊢ ∀
    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

Tactic:
simp only [mfld_simps, mem_range, TotalSpace.toProd, Equiv.coe_fn_symm_mk, forall_exists_index,
    Prod.forall, Prod.mk.injEq]

Premises used: Set.mem_range, Equiv.coe_fn_symm_mk, Bundle.TotalSpace.toProd, forall_exists_index, Prod.mk.injEq, Prod.forall
-- 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
x_1 : ModelProd H E
y : TangentBundle I H
b : E
x : H
⊢ (↑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 := ⋯, right_inv := ⋯ :
                (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) ((↑I : H → E) x, b)).1,
              ((↑(I.prod (PartialEquiv.refl E)).symm : E × E → ModelProd H E) ((↑I : H → E) x, b)).2⟩).1 =
      (↑I : H → E) x ∧
    (({ 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 := ⋯, right_inv := ⋯ :
              (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) ((↑I : H → E) x, b)).1,
            ((↑(I.prod (PartialEquiv.refl E)).symm : E × E → ModelProd H E) ((↑I : H → E) x, b)).2⟩).2 =
      b

Tactic:
simpa [PartialEquiv.prod] using ⟨rfl, rfl⟩

Premises used: PartialEquiv.prod
-- 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
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))
⊢ ContMDiff I.tangent 𝓘(𝕜, E) (M' := E) n fun (p : TangentBundle I H) ↦ p.snd (E := TangentSpace I)

Tactic:
change ContMDiff I.tangent 𝓘(𝕜, E) n
    ((id Prod.snd : ModelProd H E → E) ∘ (tangentBundleModelSpaceHomeomorph I))

Premises used: ContMDiff, Function.comp, id, ModelWithCorners.tangent, modelWithCornersSelf, Prod.snd, DFunLike.coe, tangentBundleModelSpaceHomeomorph
-- 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
hg : ContMDiff (I.prod 𝓘(𝕜, E)) (M := ModelProd H E) 𝓘(𝕜, E) n (id Prod.snd)
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)
⊢ 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:
apply ContMDiff.comp (I' := I.prod 𝓘(𝕜, E))

Premises used: ContMDiff.comp
-- 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
⊢ ContMDiff (I.prod 𝓘(𝕜, E)) (M := H × E) 𝓘(𝕜, E) n Prod.snd

Tactic:
contMDiff_snd

Premises used: contMDiff_snd
-- 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
h :
  instTopologicalSpaceModelProd H E = instTopologicalSpaceProd →
    Eq (α := ChartedSpace (ModelProd H E) (ModelProd H E)) (chartedSpaceSelf (ModelProd H E)) (prodChartedSpace H H E E)
hg : ChartedSpace H H
⊢ ContMDiff (I.prod 𝓘(𝕜, E)) (M := ModelProd H E) 𝓘(𝕜, E) n (id Prod.snd)

Tactic:
convert! contMDiff_snd

Premises used: contMDiff_snd
-- 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
e_10 : instTopologicalSpaceModelProd H E = instTopologicalSpaceProd
⊢ Eq (α := ChartedSpace (ModelProd H E) (ModelProd H E)) (chartedSpaceSelf (ModelProd H E)) (chartedSpaceSelf (H × E))

Tactic:
rfl
-- 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
⊢ 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:
contMDiff_tangentBundleModelSpaceHomeomorph

Premises used: contMDiff_tangentBundleModelSpaceHomeomorph
-- 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
⊢ 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:
exact contMDiff_tangentBundleModelSpaceHomeomorph

Premises used: contMDiff_tangentBundleModelSpaceHomeomorph
-- 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
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

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- 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
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
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
⊢ 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 ↦ ?_⟩
-- 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
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
s : Set E
x : E
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:
ContMDiffWithinAt.contDiffWithinAt <|
      (contMDiff_snd_tangentBundle_modelSpace E 𝓘(𝕜, E)).contMDiffAt.comp_contMDiffWithinAt _ h

Premises used: ContMDiffWithinAt.contDiffWithinAt, modelWithCornersSelf, ContMDiff.contMDiffAt, ContMDiffAt.comp_contMDiffWithinAt, contMDiff_snd_tangentBundle_modelSpace
-- 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
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
s : Set E
x : E
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:
exact ContMDiffWithinAt.contDiffWithinAt <|
      (contMDiff_snd_tangentBundle_modelSpace E 𝓘(𝕜, E)).contMDiffAt.comp_contMDiffWithinAt _ h

Premises used: ContMDiffWithinAt.contDiffWithinAt, modelWithCornersSelf, ContMDiff.contMDiffAt, ContMDiffAt.comp_contMDiffWithinAt, contMDiff_snd_tangentBundle_modelSpace
-- 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
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
s : Set E
x : E
h : ContDiffWithinAt 𝕜 n V s x
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
⊢ ContMDiffWithinAt 𝓘(𝕜, E) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) (M' := TotalSpace (B := E) E (TangentSpace 𝓘(𝕜, E)))
    n (fun (x : E) ↦ ⟨x, V x⟩) s x

Tactic:
apply Bundle.contMDiffWithinAt_totalSpace.2

Premises used: Iff.mpr, Bundle.contMDiffWithinAt_totalSpace
-- 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
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

Tactic:
⟨contMDiffWithinAt_id, ?_⟩

Premises used: contMDiffWithinAt_id, And.intro
-- 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
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
s : Set E
x : E
h : ContDiffWithinAt 𝕜 n V s x
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
⊢ 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:
refine ⟨contMDiffWithinAt_id, ?_⟩
-- 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
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
s : Set E
x : E
h : ContDiffWithinAt 𝕜 n V s x
⊢ ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) n V s x

Tactic:
h.contMDiffWithinAt

Premises used: ContDiffWithinAt.contMDiffWithinAt
-- 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
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
s : Set E
x : E
h : ContDiffWithinAt 𝕜 n V s x
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
⊢ 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:
convert! h.contMDiffWithinAt with y

Premises used: ContDiffWithinAt.contMDiffWithinAt
-- 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
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
s : Set E
x : E
h : ContDiffWithinAt 𝕜 n V s x
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:
simp