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'
x' : M
y : M'
hx : x' ∈ (extChartAt I x).source
hy : f x' ∈ (extChartAt I' y).source
⊢ ContinuousWithinAt f s x' ∧
      ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x') ↔
    ContinuousWithinAt f s x' ∧
      ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
        ((↑(extChartAt I x) : M → E) x')
have rw : ContinuousWithinAt f s x' →
  (ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x') ↔
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
      ((↑(extChartAt I x) : M → E) x'))
Tactic: rw [and_congr_right_iff]
-- 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'
x' : M
y : M'
hx : x' ∈ (extChartAt I x).source
hy : f x' ∈ (extChartAt I' y).source
⊢ ContinuousWithinAt f s x' →
    (ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x') ↔
      ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
        ((↑(extChartAt I x) : M → E) x'))
have set : let e := extChartAt I x;
∀ (hx : x' ∈ e.source),
  ContinuousWithinAt f s x' →
    (ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑e.symm : E → M))
        ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑e : M → E) x') ↔
      ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑e.symm : E → M))
        (e.target ∩ (↑e.symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)) ((↑e : M → E) x'))
Tactic: set e := extChartAt I x
Cleared hypotheses: 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'
x' : M
y : M'
hy : f x' ∈ (extChartAt I' y).source
e : PartialEquiv M E := extChartAt I x
hx : x' ∈ e.source
e' : PartialEquiv M' E' := extChartAt I' (f x)
⊢ ContinuousWithinAt f s x' →
    (ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑e.symm : E → M))
        ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑e : M → E) x') ↔
      ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑e.symm : E → M))
        (e.target ∩ (↑e.symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)) ((↑e : M → E) x'))
have refine : ∀ (hc : ContinuousWithinAt f s x'),
  (↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E) =ᶠ[𝓝 ((↑e : M → E) x')]
    e.target ∩ (↑e.symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)
Tactic: refine fun hc => contDiffWithinAt_congr_set ?_
-- 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'
x' : M
y : M'
hy : f x' ∈ (extChartAt I' y).source
e : PartialEquiv M E := extChartAt I x
hx : x' ∈ e.source
e' : PartialEquiv M' E' := extChartAt I' (f x)
hc : ContinuousWithinAt f s x'
⊢ (↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E) =ᶠ[𝓝 ((↑e : M → E) x')]
    e.target ∩ (↑e.symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)
have rw : f ⁻¹' (extChartAt I' y).source ∈ 𝓝[s] x'
Tactic: rw [← nhdsWithin_eq_iff_eventuallyEq, ← e.image_source_inter_eq',
    ← map_extChartAt_nhdsWithin_eq_image' hx,
    ← map_extChartAt_nhdsWithin' hx, inter_comm, nhdsWithin_inter_of_mem]
-- 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'
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
x' : M
y : M'
hx : x' ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
hy : f x' ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
⊢ ContinuousWithinAt f univ x' ∧
      ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' univ ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x') ↔
    ContinuousAt f x' ∧
      ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
        ((↑(extChartAt I x) : M → E) x')
have rw : ContinuousAt f x' ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' univ ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x') ↔
  ContinuousAt f x' ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x')
Tactic: rw [continuousWithinAt_univ, preimage_univ, univ_inter]
-- 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'
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
x' : M
y : M'
hx : x' ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
hy : f x' ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
rw :
  ContinuousAt f x' ∧
      ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' univ ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x') ↔
    ContinuousAt f x' ∧
      ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
        ((↑(extChartAt I x) : M → E) x')
⊢ ContinuousWithinAt f univ x' ∧
      ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' univ ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x') ↔
    ContinuousAt f x' ∧
      ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
        ((↑(extChartAt I x) : M → E) x')
have rw₁ : ContinuousAt f x' ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      (univ ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x') ↔
  ContinuousAt f x' ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x')
Tactic: rw [continuousWithinAt_univ, preimage_univ, univ_inter]
-- 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'
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
x' : M
y : M'
hx : x' ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
hy : f x' ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
rw :
  ContinuousAt f x' ∧
      ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' univ ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x') ↔
    ContinuousAt f x' ∧
      ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
        ((↑(extChartAt I x) : M → E) x')
rw₁ :
  ContinuousAt f x' ∧
      ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        (univ ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x') ↔
    ContinuousAt f x' ∧
      ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
        ((↑(extChartAt I x) : M → E) x')
⊢ ContinuousWithinAt f univ x' ∧
      ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' univ ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x') ↔
    ContinuousAt f x' ∧
      ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
        ((↑(extChartAt I x) : M → E) x')
have rw₂ : ContinuousAt f x' ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x') ↔
  ContinuousAt f x' ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x')
Tactic: rw [continuousWithinAt_univ, preimage_univ, univ_inter]
-- 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'
e : OpenPartialHomeomorph M H
e' : OpenPartialHomeomorph M' H'
f : M → M'
s : Set M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas I' n M') e'
hs : s ⊆ e.source
h2s : MapsTo f s e'.source
⊢ ContMDiffOn I I' n f s ↔
    ContinuousOn f s ∧
      ContDiffOn 𝕜 n ((↑(e'.extend I') : M' → E') ∘ f ∘ (↑(e.extend I).symm : E → M)) ((↑(e.extend I) : M → E) '' s)
have simp_rw : (∀ x ∈ s, ContMDiffWithinAt I I' n f s x) ↔
  ∀ (x : M) (x_1 : x ∈ s),
    ContinuousWithinAt f s x ∧
      ContDiffWithinAt 𝕜 n ((↑(e'.extend I') : M' → E') ∘ f ∘ (↑(e.extend I).symm : E → M))
        ((↑(e.extend I) : M → E) '' s) ((↑(e.extend I) : M → E) x)
Tactic: simp_rw [ContinuousOn, ContDiffOn, Set.forall_mem_image, ← forall_and, ContMDiffOn]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (hypothesis)
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
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
x : M
y : M'
hs : s ⊆ (extChartAt I x).source
h2s : MapsTo f s (extChartAt I' y).source
⊢ ContMDiffOn I I' n f s ↔
    ContDiffOn 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x) : M → E) '' s)
have hs₁ : s ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
Tactic: rw [extChartAt_source] at hs h2s
Cleared hypotheses: hs, h2s
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (hypothesis)
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
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
x : M
y : M'
hs : s ⊆ (extChartAt I x).source
h2s : MapsTo f s (extChartAt I' y).source
hs₁ : s ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
⊢ ContMDiffOn I I' n f s ↔
    ContDiffOn 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x) : M → E) '' s)
have h2s₁ : MapsTo f s (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
Tactic: rw [extChartAt_source] at hs h2s
Cleared hypotheses: hs, h2s
-- 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
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
⊢ ContMDiffOn I I' n f s ↔
    ContinuousOn f s ∧
      ∀ (x : M) (y : M'),
        ContDiffOn 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
          ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
have mp : ContMDiffOn I I' n f s →
  ContinuousOn f s ∧
    ∀ (x : M) (y : M'),
      ContDiffOn 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
Tactic: constructor
-- 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
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
mp :
  ContMDiffOn I I' n f s →
    ContinuousOn f s ∧
      ∀ (x : M) (y : M'),
        ContDiffOn 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
          ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
⊢ ContMDiffOn I I' n f s ↔
    ContinuousOn f s ∧
      ∀ (x : M) (y : M'),
        ContDiffOn 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
          ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
have mpr : (ContinuousOn f s ∧
    ∀ (x : M) (y : M'),
      ContDiffOn 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))) →
  ContMDiffOn I I' n f s
Tactic: constructor
-- 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
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
h : ContMDiffOn I I' n f s
⊢ ContinuousOn f s ∧
    ∀ (x : M) (y : M'),
      ContDiffOn 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
have mp : ∀ (x : M) (y : M') (z : E)
  (hz : z ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)),
  ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
    ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)) z
Tactic: refine ⟨fun x hx => (h x hx).1, fun x y z hz => ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (hypothesis)
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
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
h : ContMDiffOn I I' n f s
x : M
y : M'
z : E
hz : z ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)
⊢ ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
    ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)) z
have hz₁ : (z ∈ range (↑I : H → E) ∧ (↑I.symm : E → H) z ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target) ∧
  (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧
    f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z)) ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
Tactic: simp only [mfld_simps] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (hypothesis)
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
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
h : ContMDiffOn I I' n f s
x : M
y : M'
z : E
hz :
  (z ∈ range (↑I : H → E) ∧ (↑I.symm : E → H) z ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target) ∧
    (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧
      f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z)) ∈
        (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
w : M := (↑(extChartAt I x).symm : E → M) z
⊢ ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
    ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)) z
have this : w ∈ s
Tactic: have : w ∈ s := by simp only [w, hz, mfld_simps]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (hypothesis)
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
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
h : ContMDiffOn I I' n f s
x : M
y : M'
z : E
hz :
  (z ∈ range (↑I : H → E) ∧ (↑I.symm : E → H) z ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target) ∧
    (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧
      f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z)) ∈
        (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
w : M := (↑(extChartAt I x).symm : E → M) z
this : w ∈ s
⊢ ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
    ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)) z
have h₁ : ContMDiffWithinAt I I' n f s w
Tactic: specialize h w this
Cleared hypotheses: h