awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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'
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
h : ContMDiffWithinAt I I' n f s w
⊢ 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 w1 : w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
Tactic: have w1 : w ∈ (chartAt H x).source := 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'
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
h : ContMDiffWithinAt I I' n f s w
w1 : w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).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 w2 : f w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
Tactic: have w2 : f w ∈ (chartAt H' y).source := by simp only [w, hz, mfld_simps]
-- 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'
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
h : ContMDiffWithinAt I I' n f s w
w1 : w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
w2 : f w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' 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 h₁ : z = (↑(extChartAt I x) : M → E) w
Tactic: convert! ((contMDiffWithinAt_iff_of_mem_source w1 w2).mp h).2.mono _
-- 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'
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
h : ContMDiffWithinAt I I' n f s w
w1 : w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
w2 : f w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
h₁ : z = (↑(extChartAt I x) : M → E) w
⊢ 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 mp : (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source) ⊆
  (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
Tactic: convert! ((contMDiffWithinAt_iff_of_mem_source w1 w2).mp h).2.mono _
-- 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'
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
h : ContMDiffWithinAt I I' n f s w
w1 : w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
w2 : f w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
⊢ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source) ⊆
    (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
have mp : ∀ ⦃my_y : E⦄,
  my_y ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source) →
    my_y ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
Tactic: mfld_set_tac
-- 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'
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
h : ContMDiffWithinAt I I' n f s w
w1 : w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
w2 : f w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
mp mp₁ mp₂ :
  ∀ ⦃my_y : E⦄,
    my_y ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source) →
      my_y ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
⊢ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source) ⊆
    (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
have mp₃ : ∀ ⦃my_y : E⦄,
  (my_y ∈ range (↑I : H → E) ∧ (↑I.symm : E → H) my_y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target) ∧
      (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) my_y) ∈ s ∧
        f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) my_y)) ∈
          (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source →
    my_y ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
Tactic: mfld_set_tac
-- 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'
hcont : ContinuousOn f s
hdiff :
  ∀ (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))
x : M
hx : x ∈ s
⊢ ContMDiffWithinAt I I' n f s x
have mpr : ContinuousWithinAt f s x ∧
  ContDiffWithinAtProp I I' n
    ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
    ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
      (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
        (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source))
    ((↑(chartAt H x) : M → H) x)
Tactic: refine (contDiffWithinAt_localInvariantProp n).liftPropWithinAt_iff.mpr ?_
-- 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'
hcont : ContinuousOn f s
hdiff :
  ∀ (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))
x : M
hx : x ∈ s
⊢ ContinuousWithinAt f s x ∧
    ContDiffWithinAtProp I I' n
      ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
      ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
          (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source))
      ((↑(chartAt H x) : M → H) x)
have mpr : ContDiffWithinAtProp I I' n
  ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
  ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
    (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
      (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source))
  ((↑(chartAt H x) : M → H) x)
Tactic: refine ⟨hcont 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
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hcont : ContinuousOn f s
hdiff :
  ∀ (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))
x : M
hx : x ∈ s
⊢ ContDiffWithinAtProp I I' n
    ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
    ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
      (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
        (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source))
    ((↑(chartAt H x) : M → H) x)
have mpr : ContDiffWithinAt 𝕜 n
  ((↑I' : H' → E') ∘
    ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) ∘ (↑I.symm : E → H))
  ((↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
      ((↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s ∩
        (↑I.symm : E → H) ⁻¹'
          (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
            f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source) ∩
    range (↑I : H → E))
  ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
Tactic: dsimp [ContDiffWithinAtProp]
-- 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'
hcont : ContinuousOn f s
hdiff :
  ∀ (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))
x : M
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 n
    ((↑I' : H' → E') ∘
      ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
        ((↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s ∩
          (↑I.symm : E → H) ⁻¹'
            (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
              f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source) ∩
      range (↑I : H → E))
    ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
have h : (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
      ((↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s ∩
        (↑I.symm : E → H) ⁻¹'
          (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
            f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source) ∩
    range (↑I : H → E) =
  (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)
Tactic: convert! hdiff x (f x) (extChartAt I x x) (by simp only [hx, mfld_simps]) using 1
-- 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'
hcont : ContinuousOn f s
hdiff :
  ∀ (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))
x : M
hx : x ∈ s
⊢ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
        ((↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s ∩
          (↑I.symm : E → H) ⁻¹'
            (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
              f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source) ∩
      range (↑I : H → E) =
    (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)
have h : ∀ (x_1 : E),
  x_1 ∈
      (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
          ((↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s ∩
            (↑I.symm : E → H) ⁻¹'
              (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
                f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source) ∩
        range (↑I : H → E) ↔
    x_1 ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)
Tactic: mfld_set_tac
-- 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
⊢ ContMDiffOn I I' 0 f s ↔ ContinuousOn f s
have rw : (ContinuousOn f s ∧
    ∀ (x : M) (y : M'),
      ContDiffOn 𝕜 0 ((↑(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))) ↔
  ContinuousOn f s
Tactic: rw [contMDiffOn_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
⊢ (ContinuousOn f s ∧
      ∀ (x : M) (y : M'),
        ContDiffOn 𝕜 0 ((↑(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))) ↔
    ContinuousOn f s
have refine : ∀ (h : ContinuousOn f s) (x : M) (y : M'),
  ContDiffOn 𝕜 0 ((↑(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: refine ⟨fun h ↦ h.1, fun 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 : M → M'
s : Set M
h : ContinuousOn f s
x : M
y : M'
⊢ ContDiffOn 𝕜 0 ((↑(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 rw : ContinuousOn ((↑(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: rw [contDiffOn_zero]
-- 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
h : ContinuousOn f s
x : M
y : M'
⊢ ContinuousOn ((↑(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 hf : ContinuousOn (f ∘ (↑(extChartAt I x).symm : E → M))
  ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
Tactic: apply (continuousOn_extChartAt _).comp