awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Riemannian (hypothesis)
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
⊢ (MDiffAt[s] fun (m : M) ↦ ⟪v m, w m⟫) x
have hb : MDiffAt[s] b x
Tactic: have hb : MDifferentiableWithinAt IM IB b s x := by
    simp only [mdifferentiableWithinAt_totalSpace] at hv
    exact hv.1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Riemannian (goal)
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) ↦ ⟪v m, w m⟫) x
have simp : (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: simp only [hg]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Riemannian (goal)
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
have hψ : MDiffAt[s] (T% g) x
Tactic: apply MDifferentiableWithinAt.clm_bundle_apply₂ (F₁ := F) (F₂ := F)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Riemannian (goal)
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
hψ : MDiffAt[s] (T% g) 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
have hv₁ : MDiffAt[s] (T% v) x
Tactic: apply MDifferentiableWithinAt.clm_bundle_apply₂ (F₁ := F) (F₂ := F)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Riemannian (goal)
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
hψ : MDiffAt[s] (T% g) x
hv₁ : MDiffAt[s] (T% v) 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
have hw₁ : MDiffAt[s] (T% w) x
Tactic: apply MDifferentiableWithinAt.clm_bundle_apply₂ (F₁ := F) (F₂ := F)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Riemannian (hypothesis)
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) ↦
      (((g (b m) : (a : E (b m)) → E (b m) →L[ℝ] ℝ) (v m) : E (b m) →L[ℝ] ℝ) : (a : E (b m)) → ℝ) (w m))
    x
have 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
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
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Riemannian (hypothesis)
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 (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
have 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
Tactic: simp only [mdifferentiableWithinAt_totalSpace] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tangent (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
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)
have refine : (↑I : H → E) '' ((↑i : OpenPartialHomeomorph M H).symm ≫ₕ (↑j : OpenPartialHomeomorph M H)).source ⊆ range (↑I : H → E)
Tactic: refine I.extendCoordChange_source.trans_subset ?_
-- 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
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))
⊢ ContDiffOn 𝕜 (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
have h : (((↑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
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tangent (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
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
have 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
Tactic: refine (ContDiffWithinAt.fderivWithin_right ?_ I.uniqueDiffOn le_rfl
    <| h hx).mono h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tangent (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
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
have 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
Tactic: refine (I.contDiffOn_extendCoordChange (subset_maximalAtlas i.2)
    (subset_maximalAtlas j.2) x hx).mono_of_mem_nhdsWithin ?_
-- 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 : (↑(atlas H M) : Type (max u_4 u_6))
x : M
hx : x ∈ (↑i : OpenPartialHomeomorph M H).source
v : E
⊢ (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
have rw : UniqueDiffWithinAt 𝕜 (range (↑I : H → E)) ((↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) x)
Tactic: rw [Filter.EventuallyEq.fderivWithin_eq, fderivWithin_fun_id, ContinuousLinearMap.id_apply]
-- 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 : (↑(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)
⊢ (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
have 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
Tactic: rw [Filter.EventuallyEq.fderivWithin_eq, fderivWithin_fun_id, ContinuousLinearMap.id_apply]
-- 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 : (↑(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
⊢ (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
have 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
Tactic: rw [Filter.EventuallyEq.fderivWithin_eq, fderivWithin_fun_id, ContinuousLinearMap.id_apply]
-- 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 : (↑(atlas H M) : Type (max u_4 u_6))
x : M
hx : x ∈ (↑i : OpenPartialHomeomorph M H).source
v : E
⊢ (↑((↑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
have 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
Tactic: filter_upwards [i.1.extend_target_mem_nhdsWithin hx] with y hy
-- 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 : (↑(atlas H M) : Type (max u_4 u_6))
⊢ 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 this : IsManifold I (HAdd.hAdd (α := ℕ∞ω) 0 1) M
Tactic: have : IsManifold I (0 + 1) M := by simpa