awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
B : Type u_3
inst_3 : TopologicalSpace B
inst_4 : ChartedSpace HB B
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
E : B → Type u_5
inst_7 : TopologicalSpace (TotalSpace F E)
inst_8 : (x : B) → NormedAddCommGroup (E x)
inst_9 : (x : B) → InnerProductSpace ℝ (E x)
inst_10 : FiberBundle F E
inst_11 : VectorBundle ℝ F E
EM : Type u_6
inst_12 : NormedAddCommGroup EM
inst_13 : NormedSpace ℝ EM
HM : Type u_7
inst_14 : TopologicalSpace HM
IM : ModelWithCorners ℝ EM HM
M : Type u_8
inst_15 : TopologicalSpace M
inst_16 : ChartedSpace HM M
h : IsContMDiffRiemannianBundle IB 1 F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hv : (MDiffAt[s] fun (m : M) ↦ ⟨b m, v m⟩) x
hw : (MDiffAt[s] fun (m : M) ↦ ⟨b m, w m⟩) x
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_smooth :
  ContMDiff IB (E' := Prod.{u_1, u_4} EB (F →L[ℝ] F →L[ℝ] ℝ)) (IB.prod 𝓘(ℝ, F →L[ℝ] F →L[ℝ] ℝ)) (M' :=
    TotalSpace.{u_3, u_4, u_5} (F →L[ℝ] F →L[ℝ] ℝ) fun (b : B) ↦ E b →L[ℝ] E b →L[ℝ] ℝ) 1 fun (b : B) ↦ ⟨b, g b⟩
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = (((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) w
hb : MDiffAt[s] b x
⊢ (MDiffAt[s] fun (m : M) ↦
      ⟨b m, (((g (b m) : (a : E (b m)) → E (b m) →L[ℝ] ℝ) (v m) : E (b m) →L[ℝ] ℝ) : (a : E (b m)) → ℝ) (w m)⟩)
    x

Tactic:
have : MDifferentiableWithinAt IM (IB.prod 𝓘(ℝ))
      (fun m ↦ TotalSpace.mk' ℝ (E := Bundle.Trivial B ℝ) (b m) (g (b m) (v m) (w m))) s x := by
    apply MDifferentiableWithinAt.clm_bundle_apply₂ (F₁ := F) (F₂ := F)
    · exact MDifferentiableAt.comp_mdifferentiableWithinAt x
        (g_smooth.mdifferentiableAt one_ne_zero) hb
    · exact hv
    · exact hw
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
B : Type u_3
inst_3 : TopologicalSpace B
inst_4 : ChartedSpace HB B
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
E : B → Type u_5
inst_7 : TopologicalSpace (TotalSpace F E)
inst_8 : (x : B) → NormedAddCommGroup (E x)
inst_9 : (x : B) → InnerProductSpace ℝ (E x)
inst_10 : FiberBundle F E
inst_11 : VectorBundle ℝ F E
EM : Type u_6
inst_12 : NormedAddCommGroup EM
inst_13 : NormedSpace ℝ EM
HM : Type u_7
inst_14 : TopologicalSpace HM
IM : ModelWithCorners ℝ EM HM
M : Type u_8
inst_15 : TopologicalSpace M
inst_16 : ChartedSpace HM M
h : IsContMDiffRiemannianBundle IB 1 F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hv : (MDiffAt[s] fun (m : M) ↦ ⟨b m, v m⟩) x
hw : (MDiffAt[s] fun (m : M) ↦ ⟨b m, w m⟩) x
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_smooth :
  ContMDiff IB (E' := Prod.{u_1, u_4} EB (F →L[ℝ] F →L[ℝ] ℝ)) (IB.prod 𝓘(ℝ, F →L[ℝ] F →L[ℝ] ℝ)) (M' :=
    TotalSpace.{u_3, u_4, u_5} (F →L[ℝ] F →L[ℝ] ℝ) fun (b : B) ↦ E b →L[ℝ] E b →L[ℝ] ℝ) 1 fun (b : B) ↦ ⟨b, g b⟩
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = (((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) w
hb : MDiffAt[s] b x
this :
  (MDiffAt[s] fun (m : M) ↦
      ⟨b m, (((g (b m) : (a : E (b m)) → E (b m) →L[ℝ] ℝ) (v m) : E (b m) →L[ℝ] ℝ) : (a : E (b m)) → ℝ) (w m)⟩)
    x
⊢ (MDiffAt[s] fun (x : M) ↦ b x) x ∧
    (MDiffAt[s] fun (x_1 : M) ↦
        ((↑(trivializationAt ℝ (Trivial B ℝ) (b x)) : TotalSpace ℝ (Trivial B ℝ) → B × ℝ)
            ⟨b x_1,
              (((g (b x_1) : (a : E (b x_1)) → E (b x_1) →L[ℝ] ℝ) (v x_1) : E (b x_1) →L[ℝ] ℝ) : (a : E (b x_1)) → ℝ)
                (w x_1)⟩).2)
      x

Tactic:
simp only [mdifferentiableWithinAt_totalSpace] at this

Premises used: mdifferentiableWithinAt_totalSpace
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
B : Type u_3
inst_3 : TopologicalSpace B
inst_4 : ChartedSpace HB B
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
E : B → Type u_5
inst_7 : TopologicalSpace (TotalSpace F E)
inst_8 : (x : B) → NormedAddCommGroup (E x)
inst_9 : (x : B) → InnerProductSpace ℝ (E x)
inst_10 : FiberBundle F E
inst_11 : VectorBundle ℝ F E
EM : Type u_6
inst_12 : NormedAddCommGroup EM
inst_13 : NormedSpace ℝ EM
HM : Type u_7
inst_14 : TopologicalSpace HM
IM : ModelWithCorners ℝ EM HM
M : Type u_8
inst_15 : TopologicalSpace M
inst_16 : ChartedSpace HM M
h : IsContMDiffRiemannianBundle IB 1 F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hv : (MDiffAt[s] fun (m : M) ↦ ⟨b m, v m⟩) x
hw : (MDiffAt[s] fun (m : M) ↦ ⟨b m, w m⟩) x
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_smooth :
  ContMDiff IB (E' := Prod.{u_1, u_4} EB (F →L[ℝ] F →L[ℝ] ℝ)) (IB.prod 𝓘(ℝ, F →L[ℝ] F →L[ℝ] ℝ)) (M' :=
    TotalSpace.{u_3, u_4, u_5} (F →L[ℝ] F →L[ℝ] ℝ) fun (b : B) ↦ E b →L[ℝ] E b →L[ℝ] ℝ) 1 fun (b : B) ↦ ⟨b, g b⟩
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = (((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) w
hb : MDiffAt[s] b x
this :
  (MDiffAt[s] fun (x : M) ↦ b x) x ∧
    (MDiffAt[s] fun (x_1 : M) ↦
        ((↑(trivializationAt ℝ (Trivial B ℝ) (b x)) : TotalSpace ℝ (Trivial B ℝ) → B × ℝ)
            ⟨b x_1,
              (((g (b x_1) : (a : E (b x_1)) → E (b x_1) →L[ℝ] ℝ) (v x_1) : E (b x_1) →L[ℝ] ℝ) : (a : E (b x_1)) → ℝ)
                (w x_1)⟩).2)
      x
⊢ (MDiffAt[s] fun (m : M) ↦
      (((g (b m) : (a : E (b m)) → E (b m) →L[ℝ] ℝ) (v m) : E (b m) →L[ℝ] ℝ) : (a : E (b m)) → ℝ) (w m))
    x

Tactic:
this.2

Premises used: And.right
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
B : Type u_3
inst_3 : TopologicalSpace B
inst_4 : ChartedSpace HB B
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
E : B → Type u_5
inst_7 : TopologicalSpace (TotalSpace F E)
inst_8 : (x : B) → NormedAddCommGroup (E x)
inst_9 : (x : B) → InnerProductSpace ℝ (E x)
inst_10 : FiberBundle F E
inst_11 : VectorBundle ℝ F E
EM : Type u_6
inst_12 : NormedAddCommGroup EM
inst_13 : NormedSpace ℝ EM
HM : Type u_7
inst_14 : TopologicalSpace HM
IM : ModelWithCorners ℝ EM HM
M : Type u_8
inst_15 : TopologicalSpace M
inst_16 : ChartedSpace HM M
h : IsContMDiffRiemannianBundle IB 1 F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hv : (MDiffAt[s] fun (m : M) ↦ ⟨b m, v m⟩) x
hw : (MDiffAt[s] fun (m : M) ↦ ⟨b m, w m⟩) x
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_smooth :
  ContMDiff IB (E' := Prod.{u_1, u_4} EB (F →L[ℝ] F →L[ℝ] ℝ)) (IB.prod 𝓘(ℝ, F →L[ℝ] F →L[ℝ] ℝ)) (M' :=
    TotalSpace.{u_3, u_4, u_5} (F →L[ℝ] F →L[ℝ] ℝ) fun (b : B) ↦ E b →L[ℝ] E b →L[ℝ] ℝ) 1 fun (b : B) ↦ ⟨b, g b⟩
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = (((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) w
hb : MDiffAt[s] b x
this :
  (MDiffAt[s] fun (x : M) ↦ b x) x ∧
    (MDiffAt[s] fun (x_1 : M) ↦
        ((↑(trivializationAt ℝ (Trivial B ℝ) (b x)) : TotalSpace ℝ (Trivial B ℝ) → B × ℝ)
            ⟨b x_1,
              (((g (b x_1) : (a : E (b x_1)) → E (b x_1) →L[ℝ] ℝ) (v x_1) : E (b x_1) →L[ℝ] ℝ) : (a : E (b x_1)) → ℝ)
                (w x_1)⟩).2)
      x
⊢ (MDiffAt[s] fun (m : M) ↦
      (((g (b m) : (a : E (b m)) → E (b m) →L[ℝ] ℝ) (v m) : E (b m) →L[ℝ] ℝ) : (a : E (b m)) → ℝ) (w m))
    x

Tactic:
exact this.2

Premises used: And.right
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
B : Type u_3
inst_3 : TopologicalSpace B
inst_4 : ChartedSpace HB B
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
E : B → Type u_5
inst_7 : TopologicalSpace (TotalSpace F E)
inst_8 : (x : B) → NormedAddCommGroup (E x)
inst_9 : (x : B) → InnerProductSpace ℝ (E x)
inst_10 : FiberBundle F E
inst_11 : VectorBundle ℝ F E
EM : Type u_6
inst_12 : NormedAddCommGroup EM
inst_13 : NormedSpace ℝ EM
HM : Type u_7
inst_14 : TopologicalSpace HM
IM : ModelWithCorners ℝ EM HM
M : Type u_8
inst_15 : TopologicalSpace M
inst_16 : ChartedSpace HM M
h : IsContMDiffRiemannianBundle IB 1 F E
b : M → B
v w : (x : M) → E (b x)
x : M
hv : (MDiffAt fun (m : M) ↦ ⟨b m, v m⟩) x
hw : (MDiffAt fun (m : M) ↦ ⟨b m, w m⟩) x
⊢ (MDiffAt fun (b_1 : M) ↦ ⟪v b_1, w b_1⟫) x

Tactic:
MDifferentiableWithinAt.inner_bundle hv hw

Premises used: MDifferentiableAt, MDifferentiableWithinAt.inner_bundle, ChartedSpace.LiftPropAt
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
B : Type u_3
inst_3 : TopologicalSpace B
inst_4 : ChartedSpace HB B
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
E : B → Type u_5
inst_7 : TopologicalSpace (TotalSpace F E)
inst_8 : (x : B) → NormedAddCommGroup (E x)
inst_9 : (x : B) → InnerProductSpace ℝ (E x)
inst_10 : FiberBundle F E
inst_11 : VectorBundle ℝ F E
EM : Type u_6
inst_12 : NormedAddCommGroup EM
inst_13 : NormedSpace ℝ EM
HM : Type u_7
inst_14 : TopologicalSpace HM
IM : ModelWithCorners ℝ EM HM
M : Type u_8
inst_15 : TopologicalSpace M
inst_16 : ChartedSpace HM M
h : IsContMDiffRiemannianBundle IB 1 F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
hv : MDiff[s] fun (m : M) ↦ ⟨b m, v m⟩
hw : MDiff[s] fun (m : M) ↦ ⟨b m, w m⟩
⊢ MDiff[s] fun (b_1 : M) ↦ ⟪v b_1, w b_1⟫

Tactic:
fun x hx ↦ (hv x hx).inner_bundle (hw x hx)

Premises used: MDifferentiableOn, MDifferentiableWithinAt.inner_bundle
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
B : Type u_3
inst_3 : TopologicalSpace B
inst_4 : ChartedSpace HB B
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
E : B → Type u_5
inst_7 : TopologicalSpace (TotalSpace F E)
inst_8 : (x : B) → NormedAddCommGroup (E x)
inst_9 : (x : B) → InnerProductSpace ℝ (E x)
inst_10 : FiberBundle F E
inst_11 : VectorBundle ℝ F E
EM : Type u_6
inst_12 : NormedAddCommGroup EM
inst_13 : NormedSpace ℝ EM
HM : Type u_7
inst_14 : TopologicalSpace HM
IM : ModelWithCorners ℝ EM HM
M : Type u_8
inst_15 : TopologicalSpace M
inst_16 : ChartedSpace HM M
h : IsContMDiffRiemannianBundle IB 1 F E
b : M → B
v w : (x : M) → E (b x)
hv : MDiff fun (m : M) ↦ ⟨b m, v m⟩
hw : MDiff fun (m : M) ↦ ⟨b m, w m⟩
⊢ MDiff fun (b_1 : M) ↦ ⟪v b_1, w b_1⟫

Tactic:
fun x ↦ (hv x).inner_bundle (hw x)

Premises used: MDifferentiable, MDifferentiableAt.inner_bundle
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Goal:
EB : Type u_1
inst : NormedAddCommGroup EB
inst_1 : NormedSpace ℝ EB
HB : Type u_2
inst_2 : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
n n' : ℕ∞ω
B : Type u_3
inst_3 : TopologicalSpace B
inst_4 : ChartedSpace HB B
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
E : B → Type u_5
inst_7 : TopologicalSpace (TotalSpace F E)
inst_8 : (b : B) → TopologicalSpace (E b)
inst_9 : (b : B) → AddCommGroup (E b)
inst_10 : (b : B) → Module ℝ (E b)
inst_11 : ∀ (b : B), IsTopologicalAddGroup.{u_5} (E b)
inst_12 : ∀ (b : B), ContinuousConstSMul.{0, u_5} ℝ (E b)
inst_13 : FiberBundle F E
inst_14 : VectorBundle ℝ F E
g : ContMDiffRiemannianMetric IB n F E
⊢ IsContMDiffRiemannianBundle IB n F E

Tactic:
letI : RiemannianBundle E := ⟨g.toRiemannianMetric⟩
  ⟨g.inner, g.contMDiff, fun _ _ _ ↦ rfl⟩

Premises used: Bundle.ContMDiffRiemannianMetric.contMDiff, Bundle.ContMDiffRiemannianMetric.inner, And.intro, Exists.intro, IsContMDiffRiemannianBundle.mk, rfl
-- 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
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 (n + 1) M
i j : (↑(atlas H M) : Type (max u_4 u_6))
⊢ (((↑i : OpenPartialHomeomorph M H).extend I).symm ≫ (↑j : OpenPartialHomeomorph M H).extend I).source ⊆
    range (↑I : H → E)

Tactic:
I.extendCoordChange_source.trans_subset ?_

Premises used: ModelWithCorners.extendCoordChange_source, Eq.trans_subset
-- 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
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 (n + 1) M
i j : (↑(atlas H M) : Type (max u_4 u_6))
refine :
  (↑I : H → E) '' ((↑i : OpenPartialHomeomorph M H).symm ≫ₕ (↑j : OpenPartialHomeomorph M H)).source ⊆
    range (↑I : H → E)
⊢ (((↑i : OpenPartialHomeomorph M H).extend I).symm ≫ (↑j : OpenPartialHomeomorph M H).extend I).source ⊆
    range (↑I : H → E)

Tactic:
refine I.extendCoordChange_source.trans_subset ?_

Premises used: ModelWithCorners.extendCoordChange_source, Eq.trans_subset
-- 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
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 (n + 1) M
i j : (↑(atlas H M) : Type (max u_4 u_6))
⊢ (↑I : H → E) '' ((↑i : OpenPartialHomeomorph M H).symm ≫ₕ (↑j : OpenPartialHomeomorph M H)).source ⊆
    range (↑I : H → E)

Tactic:
apply image_subset_range

Premises used: Set.image_subset_range
-- 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
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 (n + 1) M
i j : (↑(atlas H M) : Type (max u_4 u_6))
⊢ (((↑i : OpenPartialHomeomorph M H).extend I).symm ≫ (↑j : OpenPartialHomeomorph M H).extend I).source ⊆
    range (↑I : H → E)

Tactic:
have h : ((i.1.extend I).symm ≫ j.1.extend I).source ⊆ range I := by
    refine I.extendCoordChange_source.trans_subset ?_; apply image_subset_range
-- 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
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 (n + 1) M
i j : (↑(atlas H M) : Type (max u_4 u_6))
h :
  (((↑i : OpenPartialHomeomorph M H).extend I).symm ≫ (↑j : OpenPartialHomeomorph M H).extend I).source ⊆
    range (↑I : H → E)
x : E
hx : x ∈ (((↑i : OpenPartialHomeomorph M H).extend I).symm ≫ (↑j : OpenPartialHomeomorph M H).extend I).source
⊢ ContDiffWithinAt 𝕜 (F := E →L[𝕜] E) n
    (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).symm ≫ (↑j : OpenPartialHomeomorph M H).extend I).source x

Tactic:
(ContDiffWithinAt.fderivWithin_right ?_ I.uniqueDiffOn le_rfl
    <| h hx).mono h

Premises used: le_rfl, ModelWithCorners.uniqueDiffOn, ContDiffWithinAt.fderivWithin_right, ContDiffWithinAt.mono
-- 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
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 (n + 1) M
i j : (↑(atlas H M) : Type (max u_4 u_6))
h :
  (((↑i : OpenPartialHomeomorph M H).extend I).symm ≫ (↑j : OpenPartialHomeomorph M H).extend I).source ⊆
    range (↑I : H → E)
x : E
hx : x ∈ (((↑i : OpenPartialHomeomorph M H).extend I).symm ≫ (↑j : OpenPartialHomeomorph M H).extend I).source
refine :
  ContDiffWithinAt 𝕜 (n + 1)
    ((↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) ∘
      (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
    (range (↑I : H → E)) x
⊢ ContDiffWithinAt 𝕜 (F := E →L[𝕜] E) n
    (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).symm ≫ (↑j : OpenPartialHomeomorph M H).extend I).source x

Tactic:
refine (ContDiffWithinAt.fderivWithin_right ?_ I.uniqueDiffOn le_rfl
    <| h hx).mono h

Premises used: le_rfl, ModelWithCorners.uniqueDiffOn, ContDiffWithinAt.fderivWithin_right, ContDiffWithinAt.mono
-- 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
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 (n + 1) M
i j : (↑(atlas H M) : Type (max u_4 u_6))
h :
  (((↑i : OpenPartialHomeomorph M H).extend I).symm ≫ (↑j : OpenPartialHomeomorph M H).extend I).source ⊆
    range (↑I : H → E)
x : E
hx : x ∈ (((↑i : OpenPartialHomeomorph M H).extend I).symm ≫ (↑j : OpenPartialHomeomorph M H).extend I).source
⊢ ContDiffWithinAt 𝕜 (n + 1)
    ((↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) ∘
      (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
    (range (↑I : H → E)) x

Tactic:
(I.contDiffOn_extendCoordChange (subset_maximalAtlas i.2)
    (subset_maximalAtlas j.2) x hx).mono_of_mem_nhdsWithin ?_

Premises used: ContDiffWithinAt.mono_of_mem_nhdsWithin, IsManifold.subset_maximalAtlas, ModelWithCorners.contDiffOn_extendCoordChange, 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
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 (n + 1) M
i j : (↑(atlas H M) : Type (max u_4 u_6))
h :
  (((↑i : OpenPartialHomeomorph M H).extend I).symm ≫ (↑j : OpenPartialHomeomorph M H).extend I).source ⊆
    range (↑I : H → E)
x : E
hx : x ∈ (((↑i : OpenPartialHomeomorph M H).extend I).symm ≫ (↑j : OpenPartialHomeomorph M H).extend I).source
refine :
  PartialEquiv.source
      (ModelWithCorners.extendCoordChange.{u_1, u_2, u_6, u_4} (𝕜 := 𝕜) (I := I) (↑i : OpenPartialHomeomorph M H)
        (↑j : OpenPartialHomeomorph M H)) ∈
    𝓝[range (↑I : H → E)] x
⊢ ContDiffWithinAt 𝕜 (n + 1)
    ((↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) ∘
      (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
    (range (↑I : H → E)) x

Tactic:
refine (I.contDiffOn_extendCoordChange (subset_maximalAtlas i.2)
    (subset_maximalAtlas j.2) x hx).mono_of_mem_nhdsWithin ?_

Premises used: ContDiffWithinAt.mono_of_mem_nhdsWithin, IsManifold.subset_maximalAtlas, ModelWithCorners.contDiffOn_extendCoordChange, 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
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 (n + 1) M
i j : (↑(atlas H M) : Type (max u_4 u_6))
h :
  (((↑i : OpenPartialHomeomorph M H).extend I).symm ≫ (↑j : OpenPartialHomeomorph M H).extend I).source ⊆
    range (↑I : H → E)
x : E
hx : x ∈ (((↑i : OpenPartialHomeomorph M H).extend I).symm ≫ (↑j : OpenPartialHomeomorph M H).extend I).source
⊢ PartialEquiv.source
      (ModelWithCorners.extendCoordChange.{u_1, u_2, u_6, u_4} (𝕜 := 𝕜) (I := I) (↑i : OpenPartialHomeomorph M H)
        (↑j : OpenPartialHomeomorph M H)) ∈
    𝓝[range (↑I : H → E)] x

Tactic:
I.extendCoordChange_source_mem_nhdsWithin hx

Premises used: ModelWithCorners.extendCoordChange_source_mem_nhdsWithin
-- 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
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 (n + 1) M
i j : (↑(atlas H M) : Type (max u_4 u_6))
h :
  (((↑i : OpenPartialHomeomorph M H).extend I).symm ≫ (↑j : OpenPartialHomeomorph M H).extend I).source ⊆
    range (↑I : H → E)
x : E
hx : x ∈ (((↑i : OpenPartialHomeomorph M H).extend I).symm ≫ (↑j : OpenPartialHomeomorph M H).extend I).source
⊢ PartialEquiv.source
      (ModelWithCorners.extendCoordChange.{u_1, u_2, u_6, u_4} (𝕜 := 𝕜) (I := I) (↑i : OpenPartialHomeomorph M H)
        (↑j : OpenPartialHomeomorph M H)) ∈
    𝓝[range (↑I : H → E)] x

Tactic:
exact I.extendCoordChange_source_mem_nhdsWithin hx

Premises used: ModelWithCorners.extendCoordChange_source_mem_nhdsWithin
-- 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
rw : UniqueDiffWithinAt 𝕜 (range (↑I : H → E)) ((↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) x)
hs :
  (↑((↑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
hx₁ :
  ((↑((↑i : 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) =
    (↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) x
⊢ (fderivWithin 𝕜
          ((↑((↑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) :
        (a : E) → E)
      v =
    v

Tactic:
rw [Filter.EventuallyEq.fderivWithin_eq, fderivWithin_fun_id, ContinuousLinearMap.id_apply]

Premises used: ContinuousLinearMap.id_apply, Filter.EventuallyEq.fderivWithin_eq, fderivWithin_fun_id
-- 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:
I.uniqueDiffWithinAt_image

Premises used: ModelWithCorners.toFun', ModelWithCorners.uniqueDiffWithinAt_image