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
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'
i : (↑(atlas H M) : Type (max u_4 u_6))
x : M
hx : x ∈ (↑i : OpenPartialHomeomorph M H).source
v : E
⊢ UniqueDiffWithinAt 𝕜 (range (↑I : H → E)) ((↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) x)

Tactic:
exact I.uniqueDiffWithinAt_image

Premises used: ModelWithCorners.uniqueDiffWithinAt_image
-- 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'
i : (↑(atlas H M) : Type (max u_4 u_6))
x : M
hx : x ∈ (↑i : OpenPartialHomeomorph M H).source
v : E
h :
  ∀ (y : E) (hy : y ∈ ((↑i : OpenPartialHomeomorph M H).extend I).target),
    ((↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) ∘
          (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
        y =
      y
⊢ (↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) ∘
      (↑((↑i : OpenPartialHomeomorph M H).extend I).symm :
        E → M) =ᶠ[𝓝[range (↑I : H → E)] (↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) x]
    fun (x : E) ↦ x

Tactic:
filter_upwards [i.1.extend_target_mem_nhdsWithin hx] with y hy

Premises used: OpenPartialHomeomorph.extend_target_mem_nhdsWithin, Subtype.val
-- 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'
i : (↑(atlas H M) : Type (max u_4 u_6))
x : M
hx : x ∈ (↑i : OpenPartialHomeomorph M H).source
v y : E
hy : y ∈ ((↑i : OpenPartialHomeomorph M H).extend I).target
⊢ ((↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) ∘ (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
      y =
    y

Tactic:
(i.1.extend I).right_inv hy

Premises used: PartialEquiv.right_inv, Subtype.val, OpenPartialHomeomorph.extend
-- 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'
i : (↑(atlas H M) : Type (max u_4 u_6))
x : M
hx : x ∈ (↑i : OpenPartialHomeomorph M H).source
v y : E
hy : y ∈ ((↑i : OpenPartialHomeomorph M H).extend I).target
⊢ ((↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) ∘ (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
      y =
    y

Tactic:
exact (i.1.extend I).right_inv hy

Premises used: PartialEquiv.right_inv, Subtype.val, OpenPartialHomeomorph.extend
-- 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'
i j : (↑(atlas H M) : Type (max u_4 u_6))
⊢ IsManifold I (HAdd.hAdd (α := ℕ∞ω) 0 1) M

Tactic:
simpa
-- 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'
i j : (↑(atlas H M) : Type (max u_4 u_6))
⊢ IsManifold I (HAdd.hAdd (α := ℕ∞ω) 0 1) M

Tactic:
have : IsManifold I (0 + 1) M := by simpa
-- 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'
i j : (↑(atlas H M) : Type (max u_4 u_6))
this : IsManifold I (HAdd.hAdd (α := ℕ∞ω) 0 1) M
⊢ ContinuousOn.{u_6, u_2} (Y := E →L[𝕜] E)
    (fun (x : M) ↦
      fderivWithin 𝕜
        ((↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) ∘
          (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
        (range (↑I : H → E)) ((↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) x))
    ((↑i : OpenPartialHomeomorph M H).source ∩ (↑j : OpenPartialHomeomorph M H).source)

Tactic:
(contDiffOn_fderiv_coord_change (n := 0) i j).continuousOn.comp
      (i.1.continuousOn_extend.mono ?_) ?_

Premises used: contDiffOn_fderiv_coord_change, ContinuousOn.comp, ContDiffOn.continuousOn, ContinuousOn.mono, OpenPartialHomeomorph.continuousOn_extend, Subtype.val
-- 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'
i j : (↑(atlas H M) : Type (max u_4 u_6))
this : IsManifold I (HAdd.hAdd (α := ℕ∞ω) 0 1) M
refine_1 :
  (↑i : OpenPartialHomeomorph M H).source ∩ (↑j : OpenPartialHomeomorph M H).source ⊆
    ((↑i : OpenPartialHomeomorph M H).extend I).source
refine_2 :
  MapsTo (↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E)
    ((↑i : OpenPartialHomeomorph M H).source ∩ (↑j : OpenPartialHomeomorph M H).source)
    (((↑i : OpenPartialHomeomorph M H).extend I).symm ≫ (↑j : OpenPartialHomeomorph M H).extend I).source
⊢ ContinuousOn.{u_6, u_2} (Y := E →L[𝕜] E)
    (fun (x : M) ↦
      fderivWithin 𝕜
        ((↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) ∘
          (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
        (range (↑I : H → E)) ((↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) x))
    ((↑i : OpenPartialHomeomorph M H).source ∩ (↑j : OpenPartialHomeomorph M H).source)

Tactic:
refine (contDiffOn_fderiv_coord_change (n := 0) i j).continuousOn.comp
      (i.1.continuousOn_extend.mono ?_) ?_

Premises used: contDiffOn_fderiv_coord_change, ContinuousOn.comp, ContDiffOn.continuousOn, ContinuousOn.mono, OpenPartialHomeomorph.continuousOn_extend, Subtype.val
-- 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'
i j : (↑(atlas H M) : Type (max u_4 u_6))
this : IsManifold I (HAdd.hAdd (α := ℕ∞ω) 0 1) M
refine_1 :
  (↑i : OpenPartialHomeomorph M H).source ∩ (↑j : OpenPartialHomeomorph M H).source ⊆
    (↑i : OpenPartialHomeomorph M H).source
⊢ (↑i : OpenPartialHomeomorph M H).source ∩ (↑j : OpenPartialHomeomorph M H).source ⊆
    ((↑i : OpenPartialHomeomorph M H).extend I).source

Tactic:
rw [i.1.extend_source]

Premises used: OpenPartialHomeomorph.extend_source, Subtype.val
-- 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'
i j : (↑(atlas H M) : Type (max u_4 u_6))
this : IsManifold I (HAdd.hAdd (α := ℕ∞ω) 0 1) M
⊢ (↑i : OpenPartialHomeomorph M H).source ∩ (↑j : OpenPartialHomeomorph M H).source ⊆
    (↑i : OpenPartialHomeomorph M H).source

Tactic:
inter_subset_left

Premises used: Set.inter_subset_left
-- 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'
i j : (↑(atlas H M) : Type (max u_4 u_6))
this : IsManifold I (HAdd.hAdd (α := ℕ∞ω) 0 1) M
⊢ (↑i : OpenPartialHomeomorph M H).source ∩ (↑j : OpenPartialHomeomorph M H).source ⊆
    (↑i : OpenPartialHomeomorph M H).source

Tactic:
exact inter_subset_left

Premises used: Set.inter_subset_left
-- 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'
i j : (↑(atlas H M) : Type (max u_4 u_6))
this : IsManifold I (HAdd.hAdd (α := ℕ∞ω) 0 1) M
⊢ MapsTo (↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E)
    ((↑i : OpenPartialHomeomorph M H).source ∩ (↑j : OpenPartialHomeomorph M H).source)
    (((↑i : OpenPartialHomeomorph M H).extend I).symm ≫ (↑j : OpenPartialHomeomorph M H).extend I).source

Tactic:
mapsTo_iff_image_subset.2 (i.1.extend_image_source_inter j.1).subset

Premises used: Iff.mpr, Set.mapsTo_iff_image_subset, OpenPartialHomeomorph.extend_image_source_inter, Eq.subset, Subtype.val
-- 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'
i j : (↑(atlas H M) : Type (max u_4 u_6))
this : IsManifold I (HAdd.hAdd (α := ℕ∞ω) 0 1) M
⊢ MapsTo (↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E)
    ((↑i : OpenPartialHomeomorph M H).source ∩ (↑j : OpenPartialHomeomorph M H).source)
    (((↑i : OpenPartialHomeomorph M H).extend I).symm ≫ (↑j : OpenPartialHomeomorph M H).extend I).source

Tactic:
exact mapsTo_iff_image_subset.2 (i.1.extend_image_source_inter j.1).subset

Premises used: Iff.mpr, Set.mapsTo_iff_image_subset, OpenPartialHomeomorph.extend_image_source_inter, Eq.subset, Subtype.val
-- 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'
⊢ IsManifold I (HAdd.hAdd (α := ℕ∞ω) 0 1) M

Tactic:
simpa
-- 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'
⊢ IsManifold I (HAdd.hAdd (α := ℕ∞ω) 0 1) M

Tactic:
have : IsManifold I (0 + 1) M := by simpa
-- 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'
this : IsManifold I (HAdd.hAdd (α := ℕ∞ω) 0 1) M
i j k : (↑(atlas H M) : Type (max u_4 u_6))
x : M
hxk : x ∈ (↑k : OpenPartialHomeomorph M H).source
hxi : x ∈ (↑i : OpenPartialHomeomorph M H).source
hxj : x ∈ (↑j : OpenPartialHomeomorph M H).source
v : E
⊢ (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M) ⁻¹' ((↑j : OpenPartialHomeomorph M H).extend I).source ∈
    𝓝 ((↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) x)

Tactic:
have := i.1.extend_preimage_mem_nhds (I := I) hxi (j.1.extend_source_mem_nhds (I := I) hxj)
-- 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'
this_1 : IsManifold I (HAdd.hAdd (α := ℕ∞ω) 0 1) M
i j k : (↑(atlas H M) : Type (max u_4 u_6))
x : M
hxk : x ∈ (↑k : OpenPartialHomeomorph M H).source
hxi : x ∈ (↑i : OpenPartialHomeomorph M H).source
hxj : x ∈ (↑j : OpenPartialHomeomorph M H).source
v : E
this :
  (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M) ⁻¹' ((↑j : OpenPartialHomeomorph M H).extend I).source ∈
    𝓝 ((↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) x)
h :
  ∀ (y : E)
    (hy :
      y ∈
        (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M) ⁻¹'
          ((↑j : OpenPartialHomeomorph M H).extend I).source),
    (((↑((↑k : OpenPartialHomeomorph M H).extend I) : M → E) ∘
            (↑((↑j : OpenPartialHomeomorph M H).extend I).symm : E → M)) ∘
          (↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) ∘
            (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
        y =
      ((↑((↑k : OpenPartialHomeomorph M H).extend I) : M → E) ∘
          (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
        y
⊢ ((↑((↑k : OpenPartialHomeomorph M H).extend I) : M → E) ∘
        (↑((↑j : OpenPartialHomeomorph M H).extend I).symm : E → M)) ∘
      (↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) ∘
        (↑((↑i : OpenPartialHomeomorph M H).extend I).symm :
          E → M) =ᶠ[𝓝[range (↑I : H → E)] (↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) x]
    (↑((↑k : OpenPartialHomeomorph M H).extend I) : M → E) ∘ (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M)

Tactic:
filter_upwards [nhdsWithin_le_nhds this] with y hy

Premises used: nhdsWithin_le_nhds
-- 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'
this_1 : IsManifold I (HAdd.hAdd (α := ℕ∞ω) 0 1) M
i j k : (↑(atlas H M) : Type (max u_4 u_6))
x : M
hxk : x ∈ (↑k : OpenPartialHomeomorph M H).source
hxi : x ∈ (↑i : OpenPartialHomeomorph M H).source
hxj : x ∈ (↑j : OpenPartialHomeomorph M H).source
v : E
this :
  (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M) ⁻¹' ((↑j : OpenPartialHomeomorph M H).extend I).source ∈
    𝓝 ((↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) x)
y : E
hy :
  y ∈ (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M) ⁻¹' ((↑j : OpenPartialHomeomorph M H).extend I).source
h :
  (↑((↑k : OpenPartialHomeomorph M H).extend I) : M → E)
      ((↑((↑j : OpenPartialHomeomorph M H).extend I).symm : E → M)
        ((↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E)
          ((↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M) y))) =
    (↑((↑k : OpenPartialHomeomorph M H).extend I) : M → E)
      ((↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M) y)
⊢ (((↑((↑k : OpenPartialHomeomorph M H).extend I) : M → E) ∘
          (↑((↑j : OpenPartialHomeomorph M H).extend I).symm : E → M)) ∘
        (↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) ∘
          (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
      y =
    ((↑((↑k : OpenPartialHomeomorph M H).extend I) : M → E) ∘
        (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
      y

Tactic:
simp_rw [Function.comp_apply, (j.1.extend I).left_inv hy]

Premises used: Function.comp_apply, PartialEquiv.left_inv, Subtype.val, OpenPartialHomeomorph.extend