awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
p : TangentBundle I H
x : ModelProd H E
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).snd (E :=
      TangentSpace I) ≍
    ((↑(TotalSpace.toProd H E).toPartialEquiv.symm : ModelProd H E → TangentBundle I H) x).snd (E := TangentSpace I)

Tactic:
apply heq_of_eq

Premises used: heq_of_eq
-- 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).snd (E :=
      TangentSpace I) =
    ((↑(TotalSpace.toProd H E).toPartialEquiv.symm : ModelProd H E → TangentBundle I H) x).snd (E := TangentSpace I)

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, Prod.fst, mem_achart_source, tangentBundleCore, TangentSpace, Prod.snd, ModelProd
-- 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).snd (E :=
      TangentSpace I) =
    ((↑(TotalSpace.toProd H E).toPartialEquiv.symm : ModelProd H E → TangentBundle I H) x).snd (E := TangentSpace I)

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, Prod.fst, mem_achart_source, tangentBundleCore, Prod.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
⊢ PartialEquiv.source
      (toPartialEquiv
        ({
            toFun :=
              fun
                (p_1 :
                  FiberBundleCore.TotalSpace (ι := (↑(atlas H H) : Type u_4))
                    (VectorBundleCore.toFiberBundleCore (tangentBundleCore I H))) ↦
              (p_1.proj (E :=
                  FiberBundleCore.Fiber (ι := (↑(atlas H H) : Type u_4))
                    (VectorBundleCore.toFiberBundleCore (tangentBundleCore I H))),
                FiberBundleCore.coordChange (ι := (↑(atlas H H) : Type u_4))
                  (VectorBundleCore.toFiberBundleCore (tangentBundleCore I H))
                  (FiberBundleCore.indexAt (VectorBundleCore.toFiberBundleCore (tangentBundleCore I H))
                    (p_1.proj (E :=
                      FiberBundleCore.Fiber (ι := (↑(atlas H H) : Type u_4))
                        (VectorBundleCore.toFiberBundleCore (tangentBundleCore I H)))))
                  (achart H (p.proj (E := TangentSpace I)))
                  (p_1.proj (E :=
                    FiberBundleCore.Fiber (ι := (↑(atlas H H) : Type u_4))
                      (VectorBundleCore.toFiberBundleCore (tangentBundleCore I H))))
                  (p_1.snd (E :=
                    FiberBundleCore.Fiber (ι := (↑(atlas H H) : Type u_4))
                      (VectorBundleCore.toFiberBundleCore (tangentBundleCore I H))))),
            invFun := fun (p_1 : H × E) ↦
              ⟨p_1.1,
                FiberBundleCore.coordChange (ι := (↑(atlas H H) : Type u_4))
                  (VectorBundleCore.toFiberBundleCore (tangentBundleCore I H)) (achart H (p.proj (E := TangentSpace I)))
                  (FiberBundleCore.indexAt (VectorBundleCore.toFiberBundleCore (tangentBundleCore I H)) p_1.1) p_1.1
                  p_1.2⟩,
            source :=
              FiberBundleCore.proj (VectorBundleCore.toFiberBundleCore (tangentBundleCore I H)) ⁻¹'
                (toPartialEquiv (↑(achart H (p.proj (E := TangentSpace I))) : OpenPartialHomeomorph H H)).source,
            target :=
              SProd.sprod (β := Set E)
                (toPartialEquiv (↑(achart H (p.proj (E := TangentSpace I))) : OpenPartialHomeomorph H H)).source univ,
            map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯, open_source := ⋯, open_target := ⋯,
            continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ :
            OpenPartialHomeomorph
              (FiberBundleCore.TotalSpace (ι := (↑(atlas H H) : Type u_4))
                (VectorBundleCore.toFiberBundleCore (tangentBundleCore I H)))
              (H × E) } ≫ₕ
          OpenPartialHomeomorph.prod (chartAt H (p.proj (E := TangentSpace I))) (OpenPartialHomeomorph.refl E))) =
    (TotalSpace.toProd H E).toPartialEquiv.source

Tactic:
simp only [mfld_simps]
-- 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
rw :
  (↑(TotalSpace.toProd H E).toPartialEquiv : TangentBundle I H → ModelProd H E) =
    (⇑(TotalSpace.toProd H E) : (a : TotalSpace E fun (x : H) ↦ E) → H × E)
⊢ Eq (α := TangentBundle I H → ModelProd H E) (↑(chartAt (ModelProd H E) p) : TangentBundle I H → ModelProd H E)
    (⇑(TotalSpace.toProd H E) : (a : TotalSpace E fun (x : H) ↦ E) → H × E)

Tactic:
rw [← OpenPartialHomeomorph.coe_coe, tangentBundle_model_space_chartAt]

Premises used: OpenPartialHomeomorph.coe_coe, tangentBundle_model_space_chartAt
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
p : TangentBundle I H
⊢ (↑(TotalSpace.toProd H E).toPartialEquiv : TangentBundle I H → ModelProd H E) =
    (⇑(TotalSpace.toProd H E) : (a : TotalSpace E fun (x : H) ↦ E) → H × E)

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 : TangentBundle I H
rw :
  (↑(TotalSpace.toProd H E).toPartialEquiv.symm : ModelProd H E → TangentBundle I H) =
    (⇑(TotalSpace.toProd H E).symm : (a : H × E) → TotalSpace E fun (x : H) ↦ E)
⊢ Eq (α := ModelProd H E → TangentBundle I H)
    (↑(OpenPartialHomeomorph.symm (chartAt (ModelProd H E) p)) : ModelProd H E → TangentBundle I H)
    (⇑(TotalSpace.toProd H E).symm : (a : H × E) → TotalSpace E fun (x : H) ↦ E)

Tactic:
rw [← OpenPartialHomeomorph.coe_coe, OpenPartialHomeomorph.symm_toPartialEquiv,
    tangentBundle_model_space_chartAt]

Premises used: OpenPartialHomeomorph.symm_toPartialEquiv, OpenPartialHomeomorph.coe_coe, tangentBundle_model_space_chartAt
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
p : TangentBundle I H
⊢ (↑(TotalSpace.toProd H E).toPartialEquiv.symm : ModelProd H E → TangentBundle I H) =
    (⇑(TotalSpace.toProd H E).symm : (a : H × E) → TotalSpace E fun (x : H) ↦ E)

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
x x' z : H
h :
  ∀ (v : E),
    Eq (α := E)
      ((VectorBundleCore.coordChange (ι := (↑(atlas H H) : Type u_4)) (tangentBundleCore I H) (achart H x) (achart H x')
              z :
            (a : E) → E)
          v :
        E)
      ((ContinuousLinearMap.id 𝕜 E : (a : E) → E) v : E)
⊢ VectorBundleCore.coordChange (ι := (↑(atlas H H) : Type u_4)) (tangentBundleCore I H) (achart H x) (achart H x') z =
    ContinuousLinearMap.id 𝕜 E

Tactic:
ext v
-- 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
x x' z : H
v : E
⊢ Eq (α := E)
    ((VectorBundleCore.coordChange (ι := (↑(atlas H H) : Type u_4)) (tangentBundleCore I H) (achart H x) (achart H x')
            z :
          (a : E) → E)
        v :
      E)
    ((ContinuousLinearMap.id 𝕜 E : (a : E) → E) v : E)

Tactic:
(tangentBundleCore I H).coordChange_self (achart _ z) z (mem_univ _) v

Premises used: VectorBundleCore.coordChange_self, achart, tangentBundleCore, Set.mem_univ
-- 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
x x' z : H
v : E
⊢ Eq (α := E)
    ((VectorBundleCore.coordChange (ι := (↑(atlas H H) : Type u_4)) (tangentBundleCore I H) (achart H x) (achart H x')
            z :
          (a : E) → E)
        v :
      E)
    ((ContinuousLinearMap.id 𝕜 E : (a : E) → E) v : E)

Tactic:
exact (tangentBundleCore I H).coordChange_self (achart _ z) z (mem_univ _) v

Premises used: VectorBundleCore.coordChange_self, achart, tangentBundleCore, Set.mem_univ
-- 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'
p : TangentBundle I H := ⟨(↑I.symm : E → H) 0, 0⟩
rw : ContinuousOn (Y := ModelProd H E) (↑(chartAt (ModelProd H E) p) : TangentBundle I H → ModelProd H E) univ
⊢ Continuous[_, instTopologicalSpaceModelProd H E] (↑(chartAt (ModelProd H E) p) : TangentBundle I H → ModelProd H E)

Tactic:
rw [← continuousOn_univ]

Premises used: continuousOn_univ
-- 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'
p : TangentBundle I H := ⟨(↑I.symm : E → H) 0, 0⟩
⊢ ContinuousOn (Y := ModelProd H E) (↑(chartAt (ModelProd H E) p) : TangentBundle I H → ModelProd H E)
    (PartialEquiv.source (β := ModelProd H E) (toPartialEquiv (chartAt (ModelProd H E) p)))

Tactic:
(chartAt (ModelProd H E) p).continuousOn

Premises used: chartAt, OpenPartialHomeomorph.continuousOn, ModelProd
-- 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'
p : TangentBundle I H := ⟨(↑I.symm : E → H) 0, 0⟩
h : univ = PartialEquiv.source (β := ModelProd H E) (toPartialEquiv (chartAt (ModelProd H E) p))
⊢ ContinuousOn (Y := ModelProd H E) (↑(chartAt (ModelProd H E) p) : TangentBundle I H → ModelProd H E) univ

Tactic:
convert! (chartAt (ModelProd H E) p).continuousOn

Premises used: chartAt, OpenPartialHomeomorph.continuousOn, ModelProd
-- 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'
p : TangentBundle I H := ⟨(↑I.symm : E → H) 0, 0⟩
⊢ univ = PartialEquiv.source (β := ModelProd H E) (toPartialEquiv (chartAt (ModelProd H E) p))

Tactic:
simp only [mfld_simps]
-- 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'
p : TangentBundle I H := ⟨(↑I.symm : E → H) 0, 0⟩
⊢ Continuous[_, instTopologicalSpaceModelProd H E] (↑(chartAt (ModelProd H E) p) : TangentBundle I H → ModelProd H E)

Tactic:
have : Continuous (chartAt (ModelProd H E) p) := by
        rw [← continuousOn_univ]
        convert! (chartAt (ModelProd H E) p).continuousOn
        simp only [mfld_simps]
-- 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'
p : TangentBundle I H := ⟨(↑I.symm : E → H) 0, 0⟩
this :
  Continuous[_, instTopologicalSpaceModelProd H E] (↑(chartAt (ModelProd H E) p) : TangentBundle I H → ModelProd H E)
⊢ Continuous[_, instTopologicalSpaceModelProd H E] (TotalSpace.toProd H E).toFun

Tactic:
simpa only [mfld_simps] using this
-- 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'
p : TangentBundle I H := ⟨(↑I.symm : E → H) 0, 0⟩
rw :
  ContinuousOn (X := ModelProd H E)
    (↑(OpenPartialHomeomorph.symm (chartAt (ModelProd H E) p)) : ModelProd H E → TangentBundle I H) univ
⊢ Continuous[instTopologicalSpaceModelProd H E, _]
    (↑(OpenPartialHomeomorph.symm (chartAt (ModelProd H E) p)) : ModelProd H E → TangentBundle I H)

Tactic:
rw [← continuousOn_univ]

Premises used: continuousOn_univ
-- 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'
p : TangentBundle I H := ⟨(↑I.symm : E → H) 0, 0⟩
⊢ ContinuousOn (X := ModelProd H E)
    (↑(OpenPartialHomeomorph.symm (chartAt (ModelProd H E) p)) : ModelProd H E → TangentBundle I H)
    (PartialEquiv.source (toPartialEquiv (OpenPartialHomeomorph.symm (chartAt (ModelProd H E) p))))

Tactic:
(chartAt (ModelProd H E) p).symm.continuousOn

Premises used: chartAt, OpenPartialHomeomorph.continuousOn, ModelProd, OpenPartialHomeomorph.symm
-- 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'
p : TangentBundle I H := ⟨(↑I.symm : E → H) 0, 0⟩
h :
  Eq (α := Set (ModelProd H E)) univ
    (PartialEquiv.source (toPartialEquiv (OpenPartialHomeomorph.symm (chartAt (ModelProd H E) p))))
⊢ ContinuousOn (X := ModelProd H E)
    (↑(OpenPartialHomeomorph.symm (chartAt (ModelProd H E) p)) : ModelProd H E → TangentBundle I H) univ

Tactic:
convert! (chartAt (ModelProd H E) p).symm.continuousOn

Premises used: chartAt, OpenPartialHomeomorph.continuousOn, ModelProd, OpenPartialHomeomorph.symm
-- 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'
p : TangentBundle I H := ⟨(↑I.symm : E → H) 0, 0⟩
⊢ Eq (α := Set (ModelProd H E)) univ
    (PartialEquiv.source (toPartialEquiv (OpenPartialHomeomorph.symm (chartAt (ModelProd H E) p))))

Tactic:
simp only [mfld_simps]
-- 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'
p : TangentBundle I H := ⟨(↑I.symm : E → H) 0, 0⟩
⊢ Continuous[instTopologicalSpaceModelProd H E, _]
    (↑(OpenPartialHomeomorph.symm (chartAt (ModelProd H E) p)) : ModelProd H E → TangentBundle I H)

Tactic:
have : Continuous (chartAt (ModelProd H E) p).symm := by
        rw [← continuousOn_univ]
        convert! (chartAt (ModelProd H E) p).symm.continuousOn
        simp only [mfld_simps]
-- 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'
p : TangentBundle I H := ⟨(↑I.symm : E → H) 0, 0⟩
this :
  Continuous[instTopologicalSpaceModelProd H E, _]
    (↑(OpenPartialHomeomorph.symm (chartAt (ModelProd H E) p)) : ModelProd H E → TangentBundle I H)
⊢ Continuous[instTopologicalSpaceModelProd H E, _] (TotalSpace.toProd H E).invFun

Tactic:
simpa only [mfld_simps] using this
-- 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
⊢ Eq (α := (a : TangentBundle I H) → ModelProd H E)
    (⇑(tangentBundleModelSpaceHomeomorph I) : (a : TangentBundle I H) → ModelProd H E)
    (⇑(TotalSpace.toProd H E) : (a : TotalSpace E fun (x : H) ↦ E) → H × E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
⊢ Eq (α := (a : ModelProd H E) → TangentBundle I H)
    (⇑(tangentBundleModelSpaceHomeomorph I).symm : (a : ModelProd H E) → TangentBundle I H)
    (⇑(TotalSpace.toProd H E).symm : (a : H × E) → TotalSpace E fun (x : H) ↦ E)

Tactic:
rfl

Premises used: Bundle.TotalSpace.toProd, TangentSpace, ModelProd, rfl