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'
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))
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
⊢ (((↑((↑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]

Premises used: OpenPartialHomeomorph.extend_left_inv, Function.comp_apply, 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'
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
⊢ DifferentiableWithinAt 𝕜
    ((↑((↑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)

Tactic:
(I.contDiffWithinAt_extendCoordChange' (subset_maximalAtlas j.2)
        (subset_maximalAtlas k.2) hxj hxk).differentiableWithinAt one_ne_zero

Premises used: ModelWithCorners.contDiffWithinAt_extendCoordChange', one_ne_zero, IsManifold.subset_maximalAtlas, ContDiffWithinAt.differentiableWithinAt, Subtype.property
-- 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
⊢ DifferentiableWithinAt 𝕜
    ((↑((↑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)

Tactic:
exact (I.contDiffWithinAt_extendCoordChange' (subset_maximalAtlas j.2)
        (subset_maximalAtlas k.2) hxj hxk).differentiableWithinAt one_ne_zero

Premises used: ModelWithCorners.contDiffWithinAt_extendCoordChange', one_ne_zero, IsManifold.subset_maximalAtlas, ContDiffWithinAt.differentiableWithinAt, Subtype.property
-- 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
⊢ DifferentiableWithinAt 𝕜
    ((↑((↑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)

Tactic:
(I.contDiffWithinAt_extendCoordChange' (subset_maximalAtlas i.2)
        (subset_maximalAtlas j.2) hxi hxj).differentiableWithinAt one_ne_zero

Premises used: ModelWithCorners.contDiffWithinAt_extendCoordChange', one_ne_zero, IsManifold.subset_maximalAtlas, ContDiffWithinAt.differentiableWithinAt, Subtype.property
-- 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
⊢ DifferentiableWithinAt 𝕜
    ((↑((↑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)

Tactic:
exact (I.contDiffWithinAt_extendCoordChange' (subset_maximalAtlas i.2)
        (subset_maximalAtlas j.2) hxi hxj).differentiableWithinAt one_ne_zero

Premises used: ModelWithCorners.contDiffWithinAt_extendCoordChange', one_ne_zero, IsManifold.subset_maximalAtlas, ContDiffWithinAt.differentiableWithinAt, Subtype.property
-- 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_1 : M
hxk : x_1 ∈ (↑k : OpenPartialHomeomorph M H).source
hxi : x_1 ∈ (↑i : OpenPartialHomeomorph M H).source
hxj : x_1 ∈ (↑j : OpenPartialHomeomorph M H).source
v x : E
h :
  x ∈ range (↑I : H → E) →
    ((↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) ∘
          (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
        x ∈
      range (↑I : H → E)
⊢ x ∈ range (↑I : H → E) →
    ((↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) ∘
          (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
        x ∈
      range (↑I : H → E)

Tactic:
_
-- 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_1 : M
hxk : x_1 ∈ (↑k : OpenPartialHomeomorph M H).source
hxi : x_1 ∈ (↑i : OpenPartialHomeomorph M H).source
hxj : x_1 ∈ (↑j : OpenPartialHomeomorph M H).source
v x : E
h : x ∈ range (↑I : H → E)
⊢ ((↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) ∘ (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
      x ∈
    range (↑I : H → E)

Tactic:
mem_range_self _

Premises used: Set.mem_range_self, Set.Mem, ModelWithCorners.toFun'
-- 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_1 : M
hxk : x_1 ∈ (↑k : OpenPartialHomeomorph M H).source
hxi : x_1 ∈ (↑i : OpenPartialHomeomorph M H).source
hxj : x_1 ∈ (↑j : OpenPartialHomeomorph M H).source
v x : E
h : x ∈ range (↑I : H → E)
⊢ ((↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) ∘ (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
      x ∈
    range (↑I : H → E)

Tactic:
exact mem_range_self _

Premises used: Set.mem_range_self
-- 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
⊢ UniqueDiffWithinAt 𝕜 (range (↑I : H → E)) ((↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) x)

Tactic:
I.uniqueDiffWithinAt_image

Premises used: ModelWithCorners.toFun', 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'
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
⊢ 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'
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
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
hy₁ hy₂ :
  (↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) x = (↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) x
⊢ ((↑((↑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]

Premises used: OpenPartialHomeomorph.extend_left_inv, Function.comp_apply, Subtype.val
-- 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
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
i : (↑(atlas H M) : Type (max u_4 u_6))
⊢ VectorBundleCore.baseSet (tangentBundleCore I M) i = (↑i : OpenPartialHomeomorph M H).source

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
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
i : (↑(atlas H M) : Type (max u_4 u_6))
⊢ Trivialization.baseSet (Z :=
      TotalSpace E (VectorBundleCore.Fiber (ι := (↑(atlas H M) : Type (max u_4 u_6))) (tangentBundleCore I M)))
      (VectorBundleCore.localTriv (tangentBundleCore I M) i) =
    (↑i : OpenPartialHomeomorph M H).source

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
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x x' z : M
⊢ VectorBundleCore.coordChange (ι := (↑(atlas H M) : Type (max u_4 u_6))) (tangentBundleCore I M) (achart H x)
      (achart H x') z =
    fderivWithin 𝕜 ((↑(extChartAt I x') : M → E) ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) z)

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
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x y z : M
⊢ tangentCoordChange I x y z =
    fderivWithin 𝕜 ((↑(extChartAt I y) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) z)

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
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x z : M
v : E
h : z ∈ (extChartAt I x).source
a : z ∈ VectorBundleCore.baseSet (ι := (↑(atlas H M) : Type (max u_4 u_6))) (tangentBundleCore I M) (achart H x)
⊢ (tangentCoordChange I x x z : (a : E) → E) v = v

Tactic:
apply (tangentBundleCore I M).coordChange_self

Premises used: VectorBundleCore.coordChange_self, tangentBundleCore
-- 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
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x z : M
v : E
h a : z ∈ (extChartAt I x).source
⊢ z ∈ VectorBundleCore.baseSet (ι := (↑(atlas H M) : Type (max u_4 u_6))) (tangentBundleCore I M) (achart H x)

Tactic:
rw [tangentBundleCore_baseSet, coe_achart, ← extChartAt_source I]

Premises used: coe_achart, extChartAt_source, tangentBundleCore_baseSet
-- 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
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x z : M
v : E
h : z ∈ (extChartAt I x).source
⊢ z ∈ (extChartAt I x).source

Tactic:
h
-- 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
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
x z : M
v : E
h : z ∈ (extChartAt I x).source
⊢ z ∈ (extChartAt I x).source

Tactic:
exact h
-- 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
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
w x y z : M
v : E
h : z ∈ (extChartAt I w).source ∩ (extChartAt I x).source ∩ (extChartAt I y).source
a :
  z ∈
    VectorBundleCore.baseSet (ι := (↑(atlas H M) : Type (max u_4 u_6))) (tangentBundleCore I M) (achart H w) ∩
        VectorBundleCore.baseSet (ι := (↑(atlas H M) : Type (max u_4 u_6))) (tangentBundleCore I M) (achart H x) ∩
      VectorBundleCore.baseSet (ι := (↑(atlas H M) : Type (max u_4 u_6))) (tangentBundleCore I M) (achart H y)
⊢ Eq (α := E) ((tangentCoordChange I x y z : (a : E) → E) ((tangentCoordChange I w x z : (a : E) → E) v : E) : E)
    ((tangentCoordChange I w y z : (a : E) → E) v : E)

Tactic:
apply (tangentBundleCore I M).coordChange_comp

Premises used: tangentBundleCore, VectorBundleCore.coordChange_comp
-- 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
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
w x y z : M
v : E
h a : z ∈ (extChartAt I w).source ∩ (extChartAt I x).source ∩ (extChartAt I y).source
⊢ z ∈
    VectorBundleCore.baseSet (ι := (↑(atlas H M) : Type (max u_4 u_6))) (tangentBundleCore I M) (achart H w) ∩
        VectorBundleCore.baseSet (ι := (↑(atlas H M) : Type (max u_4 u_6))) (tangentBundleCore I M) (achart H x) ∩
      VectorBundleCore.baseSet (ι := (↑(atlas H M) : Type (max u_4 u_6))) (tangentBundleCore I M) (achart H y)

Tactic:
simp only [tangentBundleCore_baseSet, coe_achart, ← extChartAt_source I]

Premises used: coe_achart, extChartAt_source, tangentBundleCore_baseSet
-- 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
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
w x y z : M
v : E
h : z ∈ (extChartAt I w).source ∩ (extChartAt I x).source ∩ (extChartAt I y).source
⊢ z ∈ (extChartAt I w).source ∩ (extChartAt I x).source ∩ (extChartAt I y).source

Tactic:
h
-- 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
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
w x y z : M
v : E
h : z ∈ (extChartAt I w).source ∩ (extChartAt I x).source ∩ (extChartAt I y).source
⊢ z ∈ (extChartAt I w).source ∩ (extChartAt I x).source ∩ (extChartAt I y).source

Tactic:
exact h