awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tangent (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
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)
have refine_1 : (↑i : OpenPartialHomeomorph M H).source ∩ (↑j : OpenPartialHomeomorph M H).source ⊆
  ((↑i : OpenPartialHomeomorph M H).extend I).source
Tactic: refine (contDiffOn_fderiv_coord_change (n := 0) i j).continuousOn.comp
      (i.1.continuousOn_extend.mono ?_) ?_
-- 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'
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
⊢ 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)
have 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
Tactic: refine (contDiffOn_fderiv_coord_change (n := 0) i j).continuousOn.comp
      (i.1.continuousOn_extend.mono ?_) ?_
-- 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'
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).extend I).source
have refine_1 : (↑i : OpenPartialHomeomorph M H).source ∩ (↑j : OpenPartialHomeomorph M H).source ⊆
  (↑i : OpenPartialHomeomorph M H).source
Tactic: rw [i.1.extend_source]
-- 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'
⊢ ∀ (i j k : (↑(atlas H M) : Type (max u_4 u_6))),
    ∀
      x ∈
        (↑i : OpenPartialHomeomorph M H).source ∩ (↑j : OpenPartialHomeomorph M H).source ∩
          (↑k : OpenPartialHomeomorph M H).source,
      ∀ (v : E),
        Eq (α := E)
          ((fderivWithin 𝕜
                  ((↑((↑k : OpenPartialHomeomorph M H).extend I) : M → E) ∘
                    (↑((↑j : OpenPartialHomeomorph M H).extend I).symm : E → M))
                  (range (↑I : H → E)) ((↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) x) :
                (a : E) → E)
              ((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) :
                    (a : E) → E)
                  v :
                E) :
            E)
          ((fderivWithin 𝕜
                  ((↑((↑k : 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) :
                (a : E) → E)
              v :
            E)
have this : IsManifold I (HAdd.hAdd (α := ℕ∞ω) 0 1) M
Tactic: have : IsManifold I (0 + 1) M := by simpa
-- 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'
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
⊢ Eq (α := E)
    ((fderivWithin 𝕜
            ((↑((↑k : OpenPartialHomeomorph M H).extend I) : M → E) ∘
              (↑((↑j : OpenPartialHomeomorph M H).extend I).symm : E → M))
            (range (↑I : H → E)) ((↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) x) :
          (a : E) → E)
        ((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) :
              (a : E) → E)
            v :
          E) :
      E)
    ((fderivWithin 𝕜
            ((↑((↑k : 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) :
          (a : E) → E)
        v :
      E)
have hs : ((↑((↑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: rw [fderivWithin_fderivWithin, Filter.EventuallyEq.fderivWithin_eq]
-- 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'
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
hs :
  ((↑((↑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)
⊢ Eq (α := E)
    ((fderivWithin 𝕜
            ((↑((↑k : OpenPartialHomeomorph M H).extend I) : M → E) ∘
              (↑((↑j : OpenPartialHomeomorph M H).extend I).symm : E → M))
            (range (↑I : H → E)) ((↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) x) :
          (a : E) → E)
        ((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) :
              (a : E) → E)
            v :
          E) :
      E)
    ((fderivWithin 𝕜
            ((↑((↑k : 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) :
          (a : E) → E)
        v :
      E)
have hx : (((↑((↑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))
    ((↑((↑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))
    ((↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) x)
Tactic: rw [fderivWithin_fderivWithin, Filter.EventuallyEq.fderivWithin_eq]
-- 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'
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
⊢ ((↑((↑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)
have 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)
Tactic: have := i.1.extend_preimage_mem_nhds (I := I) hxi (j.1.extend_source_mem_nhds (I := I) hxj)
-- 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'
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)
⊢ ((↑((↑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)
have 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
Tactic: filter_upwards [nhdsWithin_le_nhds this] with y hy
-- 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'
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
⊢ (((↑((↑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
have 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)
Tactic: simp_rw [Function.comp_apply, (j.1.extend I).left_inv hy]
-- 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'
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
⊢ (((↑((↑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))
      ((↑((↑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))
      ((↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) x)
have hx : (↑((↑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)
          ((↑((↑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)
      ((↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) x))
Tactic: simp_rw [Function.comp_apply, i.1.extend_left_inv hxi, j.1.extend_left_inv hxj]
-- 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'
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
hx :
  (↑((↑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)
            ((↑((↑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)
        ((↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) x))
⊢ (((↑((↑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))
      ((↑((↑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))
      ((↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) x)
have hx₁ : (↑((↑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) x)) =
  (↑((↑k : OpenPartialHomeomorph M H).extend I) : M → E) x
Tactic: simp_rw [Function.comp_apply, i.1.extend_left_inv hxi, j.1.extend_left_inv hxj]
-- 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'
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
⊢ ((↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) ∘ (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
      ((↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) x) =
    (↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) x
have hy : (↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E)
    ((↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M)
      ((↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) x)) =
  (↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) x
Tactic: rw [Function.comp_apply, i.1.extend_left_inv hxi]