awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hn : n ≠ ∞
⊢ ContMDiffWithinAt I I' n f s x → ∀ᶠ (x' : M) in 𝓝[insert x s] x, ContMDiffWithinAt I I' n f s x'
have rw : (∃ u ∈ 𝓝[insert x s] x, ContMDiffOn I I' n f u) → ∀ᶠ (x' : M) in 𝓝[insert x s] x, ContMDiffWithinAt I I' n f s x'
Tactic: rw [contMDiffWithinAt_iff_contMDiffOn_nhds hn]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hn : n ≠ ∞
u : Set M
hu : u ∈ 𝓝[insert x s] x
h : ContMDiffOn I I' n f u
⊢ ∀ᶠ (x' : M) in 𝓝[insert x s] x, ContMDiffWithinAt I I' n f s x'
have h₁ : ∀ (x' : M) (h'x' : x' ∈ u) (hx' : u ∈ 𝓝[insert x s] x'), ContMDiffWithinAt I I' n f s x'
Tactic: filter_upwards [hu, eventually_mem_nhdsWithin_iff.mpr hu] with x' h'x' hx'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hn : n ≠ ∞
u : Set M
hu : u ∈ 𝓝[insert x s] x
h : ContMDiffOn I I' n f u
x' : M
h'x' : x' ∈ u
hx' : u ∈ 𝓝[insert x s] x'
⊢ ContMDiffWithinAt I I' n f s x'
have h₁ : u ∈ 𝓝[s] x'
Tactic: apply (h x' h'x').mono_of_mem_nhdsWithin
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f f₁ : M → M'
n : ℕ∞ω
h : ContMDiff I I' n f
h₁ : ∀ (y : M), f₁ y = f y
⊢ ContMDiff I I' n f₁
have rw : ∀ (h : ContMDiffOn I I' n f univ) (h₁ : ∀ (y : M), f₁ y = f y), ContMDiffOn I I' n f₁ univ
Tactic: rw [← contMDiffOn_univ] at h ⊢
Cleared hypotheses: h, h₁
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f f₁ : M → M'
n : ℕ∞ω
h₁ : ∀ (y : M), f₁ y = f y
⊢ ContMDiff I I' n f₁ ↔ ContMDiff I I' n f
have simp_rw : ContMDiffOn I I' n f₁ univ ↔ ContMDiffOn I I' n f univ
Tactic: simp_rw [← contMDiffOn_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.NormedSpace (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
n : WithTop ℕ∞
f : E → E'
s : Set E
x : E
⊢ ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') n f s x ↔ ContDiffWithinAt 𝕜 n f s x
have simp : ContDiffWithinAt 𝕜 n f s x → ContinuousWithinAt f s x
Tactic: simp +contextual only [ContMDiffWithinAt, liftPropWithinAt_iff',
    ContDiffWithinAtProp, iff_def, mfld_simps]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.NormedSpace (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
n : WithTop ℕ∞
f : E → E'
x : E
⊢ ContMDiffAt 𝓘(𝕜, E) 𝓘(𝕜, E') n f x ↔ ContDiffAt 𝕜 n f x
have rw : ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') n f univ x ↔ ContDiffAt 𝕜 n f x
Tactic: rw [← contMDiffWithinAt_univ, contMDiffWithinAt_iff_contDiffWithinAt, contDiffWithinAt_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.NormedSpace (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
n : WithTop ℕ∞
f : E → E'
x : E
rw : ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') n f univ x ↔ ContDiffAt 𝕜 n f x
⊢ ContMDiffAt 𝓘(𝕜, E) 𝓘(𝕜, E') n f x ↔ ContDiffAt 𝕜 n f x
have rw₁ : ContDiffWithinAt 𝕜 n f univ x ↔ ContDiffAt 𝕜 n f x
Tactic: rw [← contMDiffWithinAt_univ, contMDiffWithinAt_iff_contDiffWithinAt, contDiffWithinAt_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.NormedSpace (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
n : WithTop ℕ∞
f : E → E'
x : E
rw : ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') n f univ x ↔ ContDiffAt 𝕜 n f x
rw₁ : ContDiffWithinAt 𝕜 n f univ x ↔ ContDiffAt 𝕜 n f x
⊢ ContMDiffAt 𝓘(𝕜, E) 𝓘(𝕜, E') n f x ↔ ContDiffAt 𝕜 n f x
have rw₂ : ContDiffAt 𝕜 n f x ↔ ContDiffAt 𝕜 n f x
Tactic: rw [← contMDiffWithinAt_univ, contMDiffWithinAt_iff_contDiffWithinAt, contDiffWithinAt_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.NormedSpace (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
n : WithTop ℕ∞
f : E → E'
⊢ ContMDiff 𝓘(𝕜, E) 𝓘(𝕜, E') n f ↔ ContDiff 𝕜 n f
have rw : ContMDiff 𝓘(𝕜, E) 𝓘(𝕜, E') n f ↔ ContDiffOn 𝕜 n f univ
Tactic: rw [← contDiffOn_univ, ← contMDiffOn_univ, contMDiffOn_iff_contDiffOn]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.NormedSpace (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
n : WithTop ℕ∞
f : E → E'
rw : ContMDiff 𝓘(𝕜, E) 𝓘(𝕜, E') n f ↔ ContDiffOn 𝕜 n f univ
⊢ ContMDiff 𝓘(𝕜, E) 𝓘(𝕜, E') n f ↔ ContDiff 𝕜 n f
have rw₁ : ContMDiffOn 𝓘(𝕜, E) 𝓘(𝕜, E') n f univ ↔ ContDiffOn 𝕜 n f univ
Tactic: rw [← contDiffOn_univ, ← contMDiffOn_univ, contMDiffOn_iff_contDiffOn]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.NormedSpace (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
n : WithTop ℕ∞
f : E → E'
rw : ContMDiff 𝓘(𝕜, E) 𝓘(𝕜, E') n f ↔ ContDiffOn 𝕜 n f univ
rw₁ : ContMDiffOn 𝓘(𝕜, E) 𝓘(𝕜, E') n f univ ↔ ContDiffOn 𝕜 n f univ
⊢ ContMDiff 𝓘(𝕜, E) 𝓘(𝕜, E') n f ↔ ContDiff 𝕜 n f
have rw₂ : ContDiffOn 𝕜 n f univ ↔ ContDiffOn 𝕜 n f univ
Tactic: rw [← contDiffOn_univ, ← contMDiffOn_univ, contMDiffOn_iff_contDiffOn]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.NormedSpace (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_8
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_9
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
n : WithTop ℕ∞
g : M → F₁ →L[𝕜] F₂
f : M → F₁
s : Set M
x : M
hg : ContMDiffWithinAt I (E' := F₁ →L[𝕜] F₂) 𝓘(𝕜, F₁ →L[𝕜] F₂) n g s x
hf : ContMDiffWithinAt I 𝓘(𝕜, F₁) n f s x
⊢ ContDiffWithinAt 𝕜 (F := F₂) n (fun (x : (F₁ →L[𝕜] F₂) × F₁) ↦ (x.1 : (a : F₁) → F₂) x.2) univ (g x, f x)
have h : ContDiff 𝕜 (F := F₂) n fun (x : (F₁ →L[𝕜] F₂) × F₁) ↦ (x.1 : (a : F₁) → F₂) x.2
Tactic: apply ContDiff.contDiffAt
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
s : Set M
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
x₀ : M
f : M → M'
hf : ContMDiffWithinAt I I' n f s x₀
hmn : m + 1 ≤ n
hx : x₀ ∈ s
hs : UniqueMDiffOn I s
⊢ ContMDiffWithinAt I (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') m (inTangentCoordinates I I' id f (mfderivWithin I I' f s) x₀)
    s x₀
have this : ContMDiffWithinAt.{u_1, u_2, u_3, u_4, u_5, u_6, u_7} (I.prod I) I' (M' := M') n (fun (x : M × M) ↦ f x.2) (s ×ˢ s)
  (x₀, x₀)
Tactic: have : CMDiffAt[s ×ˢ s] n (fun x : M × M ↦ f x.2) (x₀, x₀) :=
    hf.comp (x₀, x₀) contMDiffWithinAt_snd mapsTo_snd_prod
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
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
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
Js : IsManifold J 1 N
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
x₀ : N
f : N → M → M'
g : N → M
hf : ContMDiffAt (J.prod I) I' n (uncurry f) (x₀, g x₀)
hg : ContMDiffAt J I m g x₀
hmn : m + 1 ≤ n
⊢ ContMDiffAt J (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') m
    (inTangentCoordinates.{u_1, u_2, u_5, u_3, u_6, u_4, u_7, u_10} I I' (M' := M') g (fun (x : N) ↦ f x (g x))
      (fun (x : N) ↦ mfderiv% (f x) (g x)) x₀)
    x₀
have hf₁ : ContMDiffWithinAt (J.prod I) I' n (uncurry f) univ (x₀, g x₀)
Tactic: rw [← contMDiffWithinAt_univ] at hf hg ⊢
Cleared hypotheses: hf, hg, hmn
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
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
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
Js : IsManifold J 1 N
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
x₀ : N
f : N → M → M'
g : N → M
hf : ContMDiffAt (J.prod I) I' n (uncurry f) (x₀, g x₀)
hg : ContMDiffAt J I m g x₀
hmn : m + 1 ≤ n
hf₁ : ContMDiffWithinAt (J.prod I) I' n (uncurry f) univ (x₀, g x₀)
⊢ ContMDiffAt J (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') m
    (inTangentCoordinates.{u_1, u_2, u_5, u_3, u_6, u_4, u_7, u_10} I I' (M' := M') g (fun (x : N) ↦ f x (g x))
      (fun (x : N) ↦ mfderiv% (f x) (g x)) x₀)
    x₀
have hg₁ : ContMDiffWithinAt J I m g univ x₀
Tactic: rw [← contMDiffWithinAt_univ] at hf hg ⊢
Cleared hypotheses: hf, hg, hmn
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
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
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
Js : IsManifold J 1 N
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
x₀ : N
f : N → M → M'
g : N → M
hf : ContMDiffWithinAt (J.prod I) I' n (uncurry f) univ (x₀, g x₀)
hg : ContMDiffWithinAt J I m g univ x₀
hmn : m + 1 ≤ n
⊢ ContMDiffWithinAt J (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') m
    (inTangentCoordinates.{u_1, u_2, u_5, u_3, u_6, u_4, u_7, u_10} I I' (M' := M') g (fun (x : N) ↦ f x (g x))
      (fun (x : N) ↦ mfderiv% (f x) (g x)) x₀)
    univ x₀
have hf₁ : ContMDiffWithinAt (J.prod I) I' n (uncurry f) (SProd.sprod (α := Set N) (β := Set M) univ univ) (x₀, g x₀)
Tactic: rw [← univ_prod_univ] at hf
Cleared hypotheses: hf, hg, hmn
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
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
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
Js : IsManifold J 1 N
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
x₀ : N
f : N → M → M'
g : N → M
hf : ContMDiffWithinAt (J.prod I) I' n (uncurry f) (SProd.sprod (α := Set N) (β := Set M) univ univ) (x₀, g x₀)
hg : ContMDiffWithinAt J I m g univ x₀
hmn : m + 1 ≤ n
⊢ ContMDiffWithinAt J (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') m
    (inTangentCoordinates.{u_1, u_2, u_5, u_3, u_6, u_4, u_7, u_10} I I' (M' := M') g (fun (x : N) ↦ f x (g x))
      (fun (x : N) ↦ mfderiv% (f x) (g x)) x₀)
    univ x₀
have simp_rw : ContMDiffWithinAt J (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') m
  (inTangentCoordinates.{u_1, u_2, u_5, u_3, u_6, u_4, u_7, u_10} I I' (M' := M') g (fun (x : N) ↦ f x (g x))
    (fun (x : N) ↦ mfderivWithin I I' (f x) univ (g x)) x₀)
  univ x₀
Tactic: simp_rw [← mfderivWithin_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f s
hmn : m + 1 ≤ n
hs : UniqueMDiffOn I s
x₀ : TangentBundle I M
hx₀ : Membership.mem (γ := Set (TangentBundle I M)) (TotalSpace.proj (E := TangentSpace I) ⁻¹' s) x₀
s' : Set (TangentBundle I M) := TotalSpace.proj (E := TangentSpace I) ⁻¹' s
b₁ : TangentBundle I M → M := fun (p : TangentBundle I M) ↦ p.proj (E := TangentSpace I)
v : (y : TangentBundle I M) → TangentSpace I (b₁ y) := fun (y : TangentBundle I M) ↦ y.snd (E := TangentSpace I)
⊢ ContMDiffWithinAt I.tangent I'.tangent (M' := TangentBundle I' M') m (tangentMapWithin I I' f s)
    (TotalSpace.proj (E := TangentSpace I) ⁻¹' s) x₀
have hv : ContMDiffWithinAt I.tangent I.tangent (M' := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) m
  (fun (y : TangentBundle I M) ↦ ⟨b₁ y, v y⟩) s' x₀
Tactic: have hv : ContMDiffWithinAt I.tangent I.tangent m (fun y ↦ (v y : TangentBundle I M)) s' x₀ :=
    contMDiffWithinAt_id
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f s
hmn : m + 1 ≤ n
hs : UniqueMDiffOn I s
x₀ : TangentBundle I M
hx₀ : Membership.mem (γ := Set (TangentBundle I M)) (TotalSpace.proj (E := TangentSpace I) ⁻¹' s) x₀
s' : Set (TangentBundle I M) := TotalSpace.proj (E := TangentSpace I) ⁻¹' s
b₁ : TangentBundle I M → M := fun (p : TangentBundle I M) ↦ p.proj (E := TangentSpace I)
v : (y : TangentBundle I M) → TangentSpace I (b₁ y) := fun (y : TangentBundle I M) ↦ y.snd (E := TangentSpace I)
hv :
  ContMDiffWithinAt I.tangent I.tangent (M' := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) m
    (fun (y : TangentBundle I M) ↦ ⟨b₁ y, v y⟩) s' x₀
b₂ : TangentBundle I M → M' := f ∘ b₁
⊢ ContMDiffWithinAt I.tangent I'.tangent (M' := TangentBundle I' M') m (tangentMapWithin I I' f s)
    (TotalSpace.proj (E := TangentSpace I) ⁻¹' s) x₀
have hb₂ : ContMDiffWithinAt I.tangent I' m b₂ s' x₀
Tactic: have hb₂ : CMDiffAt[s'] m b₂ x₀ :=
    ((hf (b₁ x₀) hx₀).of_le (le_self_add.trans hmn)).comp _
      (contMDiffWithinAt_proj (TangentSpace I)) (fun x h ↦ h)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f s
hmn : m + 1 ≤ n
hs : UniqueMDiffOn I s
x₀ : TangentBundle I M
hx₀ : Membership.mem (γ := Set (TangentBundle I M)) (TotalSpace.proj (E := TangentSpace I) ⁻¹' s) x₀
s' : Set (TangentBundle I M) := TotalSpace.proj (E := TangentSpace I) ⁻¹' s
b₁ : TangentBundle I M → M := fun (p : TangentBundle I M) ↦ p.proj (E := TangentSpace I)
v : (y : TangentBundle I M) → TangentSpace I (b₁ y) := fun (y : TangentBundle I M) ↦ y.snd (E := TangentSpace I)
hv :
  ContMDiffWithinAt I.tangent I.tangent (M' := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) m
    (fun (y : TangentBundle I M) ↦ ⟨b₁ y, v y⟩) s' x₀
b₂ : TangentBundle I M → M' := f ∘ b₁
hb₂ : ContMDiffWithinAt I.tangent I' m b₂ s' x₀
ϕ : (y : TangentBundle I M) →
  ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (b₁ y)) (TangentSpace I' (b₂ y)) :=
  fun (y : TangentBundle I M) ↦ mfderivWithin I I' f s (b₁ y)
⊢ ContMDiffWithinAt I.tangent (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') (M' := E →L[𝕜] E') m
    (fun (y : TangentBundle I M) ↦
      ContinuousLinearMap.inCoordinates E (TangentSpace I) E' (TangentSpace I') (b₁ x₀) (b₁ y) (b₂ x₀) (b₂ y) (ϕ y))
    s' x₀
have A : ContMDiffWithinAt I (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') (M' := E →L[𝕜] E') m
  (fun (y : M) ↦
    ContinuousLinearMap.inCoordinates E (TangentSpace I) E' (TangentSpace I') (b₁ x₀) y (b₂ x₀) (f y)
      (mfderivWithin I I' f s y))
  s (b₁ x₀)
Tactic: have A : CMDiffAt[s] m (fun y ↦ ContinuousLinearMap.inCoordinates E (TangentSpace I (M := M)) E'
        (TangentSpace I' (M := M')) (b₁ x₀) y (b₂ x₀) (f y) (mfderiv[s] f y)) (b₁ x₀) :=
      .mfderivWithin_const (hf _ hx₀) hmn hx₀ hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiffMFDeriv (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f s
hmn : m + 1 ≤ n
hs : UniqueMDiffOn I s
x₀ : TangentBundle I M
hx₀ : Membership.mem (γ := Set (TangentBundle I M)) (TotalSpace.proj (E := TangentSpace I) ⁻¹' s) x₀
s' : Set (TangentBundle I M) := TotalSpace.proj (E := TangentSpace I) ⁻¹' s
b₁ : TangentBundle I M → M := fun (p : TangentBundle I M) ↦ p.proj (E := TangentSpace I)
v : (y : TangentBundle I M) → TangentSpace I (b₁ y) := fun (y : TangentBundle I M) ↦ y.snd (E := TangentSpace I)
hv :
  ContMDiffWithinAt I.tangent I.tangent (M' := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) m
    (fun (y : TangentBundle I M) ↦ ⟨b₁ y, v y⟩) s' x₀
b₂ : TangentBundle I M → M' := f ∘ b₁
hb₂ : ContMDiffWithinAt I.tangent I' m b₂ s' x₀
ϕ : (y : TangentBundle I M) →
  ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (b₁ y)) (TangentSpace I' (b₂ y)) :=
  fun (y : TangentBundle I M) ↦ mfderivWithin I I' f s (b₁ y)
⊢ ContMDiffWithinAt I.tangent I'.tangent (M' := TangentBundle I' M') m (tangentMapWithin I I' f s)
    (TotalSpace.proj (E := TangentSpace I) ⁻¹' s) x₀
have hϕ : ContMDiffWithinAt I.tangent (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') (M' := E →L[𝕜] E') m
  (fun (y : TangentBundle I M) ↦
    ContinuousLinearMap.inCoordinates E (TangentSpace I) E' (TangentSpace I') (b₁ x₀) (b₁ y) (b₂ x₀) (b₂ y) (ϕ y))
  s' x₀
Tactic: have hϕ : CMDiffAt[s'] m (fun y ↦ ContinuousLinearMap.inCoordinates E (TangentSpace I (M := M)) E'
      (TangentSpace I' (M := M')) (b₁ x₀) (b₁ y) (b₂ x₀) (b₂ y) (ϕ y)) x₀ := by
    have A : CMDiffAt[s] m (fun y ↦ ContinuousLinearMap.inCoordinates E (TangentSpace I (M := M)) E'
        (TangentSpace I' (M := M')) (b₁ x₀) y (b₂ x₀) (f y) (mfderiv[s] f y)) (b₁ x₀) :=
      .mfderivWithin_const (hf _ hx₀) hmn hx₀ hs
    exact A.comp _ (contMDiffWithinAt_proj (TangentSpace I)) (fun x h ↦ h)