awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tangent (hypothesis)
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
⊢ (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))
have this : Eq (α := E →L[𝕜] E)
  (fderivWithin 𝕜 ((↑I : H → E) ∘ (↑I.symm : E → H)) (range (↑I : H → E)) ((↑I : H → E) (p.proj (E := TangentSpace I))))
  (fderivWithin 𝕜 id (range (↑I : H → E)) ((↑I : H → E) (p.proj (E := TangentSpace I))))
Tactic: have : fderivWithin 𝕜 (↑I ∘ ↑I.symm) (range I) (I p.proj) =
      fderivWithin 𝕜 id (range I) (I p.proj) :=
    fderivWithin_congr' (fun y hy ↦ by simp [hy]) (mem_range_self p.proj)
-- 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
⊢ toPartialEquiv (chartAt (ModelProd H E) p) = (TotalSpace.toProd H E).toPartialEquiv
have h : ∀ (x : TangentBundle I H),
  (↑(toPartialEquiv (chartAt (ModelProd H E) p)) : TangentBundle I H → ModelProd H E) x =
    (↑(TotalSpace.toProd H E).toPartialEquiv : TangentBundle I H → ModelProd H E) x
Tactic: ext x : 1
-- 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
h :
  ∀ (x : TangentBundle I H),
    (↑(toPartialEquiv (chartAt (ModelProd H E) p)) : TangentBundle I H → ModelProd H E) x =
      (↑(TotalSpace.toProd H E).toPartialEquiv : TangentBundle I H → ModelProd H E) x
⊢ toPartialEquiv (chartAt (ModelProd H E) p) = (TotalSpace.toProd H E).toPartialEquiv
have hsymm : ∀ (x : ModelProd H E),
  (↑(PartialEquiv.symm (toPartialEquiv (chartAt (ModelProd H E) p))) : ModelProd H E → TangentBundle I H) x =
    (↑(TotalSpace.toProd H E).toPartialEquiv.symm : ModelProd H E → TangentBundle I H) x
Tactic: ext x : 1
-- 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
h :
  ∀ (x : TangentBundle I H),
    (↑(toPartialEquiv (chartAt (ModelProd H E) p)) : TangentBundle I H → ModelProd H E) x =
      (↑(TotalSpace.toProd H E).toPartialEquiv : TangentBundle I H → ModelProd H E) x
hsymm :
  ∀ (x : ModelProd H E),
    (↑(PartialEquiv.symm (toPartialEquiv (chartAt (ModelProd H E) p))) : ModelProd H E → TangentBundle I H) x =
      (↑(TotalSpace.toProd H E).toPartialEquiv.symm : ModelProd H E → TangentBundle I H) x
⊢ toPartialEquiv (chartAt (ModelProd H E) p) = (TotalSpace.toProd H E).toPartialEquiv
have hs : PartialEquiv.source (β := ModelProd H E) (toPartialEquiv (chartAt (ModelProd H E) p)) =
  (TotalSpace.toProd H E).toPartialEquiv.source
Tactic: ext x : 1
-- 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 x : TangentBundle I H
⊢ (↑(toPartialEquiv (chartAt (ModelProd H E) p)) : TangentBundle I H → ModelProd H E) x =
    (↑(TotalSpace.toProd H E).toPartialEquiv : TangentBundle I H → ModelProd H E) x
have h : ((↑(toPartialEquiv (chartAt (ModelProd H E) p)) : TangentBundle I H → ModelProd H E) x).1 =
  ((↑(TotalSpace.toProd H E).toPartialEquiv : TangentBundle I H → ModelProd H E) x).1
Tactic: ext
-- 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 x : TangentBundle I H
h :
  ((↑(toPartialEquiv (chartAt (ModelProd H E) p)) : TangentBundle I H → ModelProd H E) x).1 =
    ((↑(TotalSpace.toProd H E).toPartialEquiv : TangentBundle I H → ModelProd H E) x).1
⊢ (↑(toPartialEquiv (chartAt (ModelProd H E) p)) : TangentBundle I H → ModelProd H E) x =
    (↑(TotalSpace.toProd H E).toPartialEquiv : TangentBundle I H → ModelProd H E) x
have h₁ : ((↑(toPartialEquiv (chartAt (ModelProd H E) p)) : TangentBundle I H → ModelProd H E) x).2 =
  ((↑(TotalSpace.toProd H E).toPartialEquiv : TangentBundle I H → ModelProd H E) x).2
Tactic: ext
-- 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 : ModelProd H E
⊢ (↑(PartialEquiv.symm (toPartialEquiv (chartAt (ModelProd H E) p))) : ModelProd H E → TangentBundle I H) x =
    (↑(TotalSpace.toProd H E).toPartialEquiv.symm : ModelProd H E → TangentBundle I H) x
have hsymm : ((↑(PartialEquiv.symm (toPartialEquiv (chartAt (ModelProd H E) p))) : ModelProd H E → TangentBundle I H) x).proj (E :=
    TangentSpace I) =
  ((↑(TotalSpace.toProd H E).toPartialEquiv.symm : ModelProd H E → TangentBundle I H) x).proj (E := TangentSpace I)
Tactic: ext
-- 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 : ModelProd H E
hsymm :
  ((↑(PartialEquiv.symm (toPartialEquiv (chartAt (ModelProd H E) p))) : ModelProd H E → TangentBundle I H) x).proj (E :=
      TangentSpace I) =
    ((↑(TotalSpace.toProd H E).toPartialEquiv.symm : ModelProd H E → TangentBundle I H) x).proj (E := TangentSpace I)
⊢ (↑(PartialEquiv.symm (toPartialEquiv (chartAt (ModelProd H E) p))) : ModelProd H E → TangentBundle I H) x =
    (↑(TotalSpace.toProd H E).toPartialEquiv.symm : ModelProd H E → TangentBundle I H) x
have 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)
Tactic: ext
-- 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 : 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)
have 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)
Tactic: apply heq_of_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
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
p : TangentBundle I H
⊢ 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)
have 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)
Tactic: rw [← OpenPartialHomeomorph.coe_coe, tangentBundle_model_space_chartAt]
-- 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
⊢ 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)
have 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)
Tactic: rw [← OpenPartialHomeomorph.coe_coe, OpenPartialHomeomorph.symm_toPartialEquiv,
    tangentBundle_model_space_chartAt]
-- 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
x x' z : H
⊢ VectorBundleCore.coordChange (ι := (↑(atlas H H) : Type u_4)) (tangentBundleCore I H) (achart H x) (achart H x') z =
    ContinuousLinearMap.id 𝕜 E
have 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: ext v
-- 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'
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)
have rw : ContinuousOn (Y := ModelProd H E) (↑(chartAt (ModelProd H E) p) : TangentBundle I H → ModelProd H E) univ
Tactic: rw [← continuousOn_univ]
-- 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'
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) univ
have h : univ = PartialEquiv.source (β := ModelProd H E) (toPartialEquiv (chartAt (ModelProd H E) p))
Tactic: convert! (chartAt (ModelProd H E) p).continuousOn
-- 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'
p : TangentBundle I H := ⟨(↑I.symm : E → H) 0, 0⟩
⊢ Continuous[_, instTopologicalSpaceModelProd H E] (TotalSpace.toProd H E).toFun
have this : 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]
-- 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'
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)
have rw : ContinuousOn (X := ModelProd H E)
  (↑(OpenPartialHomeomorph.symm (chartAt (ModelProd H E) p)) : ModelProd H E → TangentBundle I H) univ
Tactic: rw [← continuousOn_univ]
-- 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'
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) univ
have h : Eq (α := Set (ModelProd H E)) univ
  (PartialEquiv.source (toPartialEquiv (OpenPartialHomeomorph.symm (chartAt (ModelProd H E) p))))
Tactic: convert! (chartAt (ModelProd H E) p).symm.continuousOn
-- 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'
p : TangentBundle I H := ⟨(↑I.symm : E → H) 0, 0⟩
⊢ Continuous[instTopologicalSpaceModelProd H E, _] (TotalSpace.toProd H E).invFun
have this : 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]
-- 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) (I.prod 𝓘(𝕜, E)) (M' := ModelProd H E) n
    (⇑(tangentBundleModelSpaceHomeomorph I) : (a : TangentBundle I H) → ModelProd H E)
have 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)
Tactic: apply contMDiff_iff.2 ⟨Homeomorph.continuous _, fun x y ↦ ?_⟩
-- 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 : 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)
have 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
Tactic: apply contDiffOn_id.congr
-- 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 : TangentBundle I H
y : ModelProd H E
⊢ ∀
    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
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 : 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 := sorry, right_inv := sorry :
              (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
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.prod 𝓘(𝕜, E)) (M := ModelProd H E) I.tangent (M' := TangentBundle I H) n
    (⇑(tangentBundleModelSpaceHomeomorph I).symm : (a : ModelProd H E) → TangentBundle I H)
have 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)
Tactic: apply contMDiff_iff.2 ⟨Homeomorph.continuous _, fun x y ↦ ?_⟩
-- 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
⊢ 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)
have 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
Tactic: apply contDiffOn_id.congr