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
h : ContinuousOn f s
x : M
y : M'
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))
⊢ 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 h₁ : MapsTo (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' y).source
Tactic: apply (continuousOn_extChartAt _).comp
-- 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 (f ∘ (↑(extChartAt I x).symm : E → M))
    ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
have apply : ∀ (z : E)
  (hz : z ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)),
  (↑(extChartAt I x).symm : E → M) z ∈ s
Tactic: apply h.comp ((continuousOn_extChartAt_symm _).mono inter_subset_left) (fun 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
h : ContinuousOn 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)
⊢ (↑(extChartAt I x).symm : E → M) z ∈ s
have hz₁ : z ∈ (extChartAt I x).target ∧
  (↑(extChartAt I x).symm : E → M) z ∈ s ∧ f ((↑(extChartAt I x).symm : E → M) z) ∈ (extChartAt I' y).source
Tactic: simp only [preimage_inter, mem_inter_iff, mem_preimage] 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
h : ContinuousOn 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)
⊢ (f ∘ (↑(extChartAt I x).symm : E → M)) z ∈ (extChartAt I' y).source
have hz₁ : z ∈ (extChartAt I x).target ∧
  (↑(extChartAt I x).symm : E → M) z ∈ s ∧ f ((↑(extChartAt I x).symm : E → M) z) ∈ (extChartAt I' y).source
Tactic: simp only [preimage_inter, mem_inter_iff, mem_preimage] at hz
Cleared hypotheses: hz
-- 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 ∧
      ∀ (y : M'), ContMDiffOn I 𝓘(𝕜, E') n ((↑(extChartAt I' y) : M' → E') ∘ f) (s ∩ f ⁻¹' (extChartAt I' y).source)
have simp : ContinuousOn f s →
  ((∀ (x : M) (y : M'),
      ContDiffOn 𝕜 n
        ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘
          f ∘ (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M))
        ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).target ∩
          (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M) ⁻¹'
            (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source))) ↔
    ∀ (y : M'),
      ContinuousOn ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘ f)
          (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source) ∧
        ∀ (x : M) (y_1 : E'),
          ContDiffOn 𝕜 n
            ((↑(ModelWithCorners.toPartialEquiv 𝓘(𝕜, E')) : E' → E') ∘
              ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘ f) ∘
                (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M))
            ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).target ∩
              (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M) ⁻¹'
                (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source)))
Tactic: simp only [contMDiffOn_iff, ModelWithCorners.source_eq, chartAt_self_eq,
    OpenPartialHomeomorph.refl_partialEquiv, PartialEquiv.refl_trans, extChartAt,
    OpenPartialHomeomorph.extend, Set.preimage_univ, Set.inter_univ, 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
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
h : ContinuousOn f s
⊢ (∀ (x : M) (y : M'),
      ContDiffOn 𝕜 n
        ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘
          f ∘ (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M))
        ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).target ∩
          (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M) ⁻¹'
            (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source))) →
    ∀ (y : M'),
      ContinuousOn ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘ f)
          (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source) ∧
        ∀ (x : M) (y_1 : E'),
          ContDiffOn 𝕜 n
            ((↑(ModelWithCorners.toPartialEquiv 𝓘(𝕜, E')) : E' → E') ∘
              ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘ f) ∘
                (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M))
            ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).target ∩
              (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M) ⁻¹'
                (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source))
have mp : ∀
  (h' :
    ∀ (x : M) (y : M'),
      ContDiffOn 𝕜 n
        ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘
          f ∘ (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M))
        ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).target ∩
          (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M) ⁻¹'
            (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source)))
  (y : M'),
  ContinuousOn ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘ f)
    (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source)
Tactic: refine fun h' y => ⟨?_, fun x _ => h' x y⟩
-- 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 : ContinuousOn f s
h' :
  ∀ (x : M) (y : M'),
    ContDiffOn 𝕜 n
      ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘
        f ∘ (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M))
      ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).target ∩
        (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M) ⁻¹'
          (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source))
y : M'
⊢ ContinuousOn ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘ f)
    (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source)
have h'' : ContinuousOn (↑I' : H' → E') univ
Tactic: have h'' : ContinuousOn _ univ := (ModelWithCorners.continuous I').continuousOn
-- 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 : ContinuousOn f s
h' :
  ∀ (x : M) (y : M'),
    ContDiffOn 𝕜 n
      ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘
        f ∘ (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M))
      ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).target ∩
        (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M) ⁻¹'
          (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source))
y : M'
h'' : ContinuousOn (↑I' : H' → E') univ
⊢ ContinuousOn ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘ f)
    (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source)
have h₁ : (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source =
  (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source ∩
    (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)) : M' → H') ⁻¹' univ
Tactic: convert! (h''.comp_inter (chartAt H' y).continuousOn_toFun).comp_inter 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'
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
⊢ ContMDiff I I' n f ↔
    Continuous[inst_4, inst_9] f ∧
      ∀ (y : M'), ContMDiffOn I 𝓘(𝕜, E') n ((↑(extChartAt I' y) : M' → E') ∘ f) (f ⁻¹' (extChartAt I' y).source)
have rw : (ContinuousOn f univ ∧
    ∀ (y : M'), ContMDiffOn I 𝓘(𝕜, E') n ((↑(extChartAt I' y) : M' → E') ∘ f) (univ ∩ f ⁻¹' (extChartAt I' y).source)) ↔
  Continuous[inst_4, inst_9] f ∧
    ∀ (y : M'), ContMDiffOn I 𝓘(𝕜, E') n ((↑(extChartAt I' y) : M' → E') ∘ f) (f ⁻¹' (extChartAt I' y).source)
Tactic: rw [← contMDiffOn_univ, contMDiffOn_iff_target]
-- 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'
⊢ ContMDiff I I' 0 f ↔ Continuous[inst_4, inst_9] f
have rw : ContMDiffOn I I' 0 f univ ↔ Continuous[inst_4, inst_9] f
Tactic: rw [← contMDiffOn_univ, ← continuousOn_univ, contMDiffOn_zero_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'
rw : ContMDiffOn I I' 0 f univ ↔ Continuous[inst_4, inst_9] f
⊢ ContMDiff I I' 0 f ↔ Continuous[inst_4, inst_9] f
have rw₁ : ContMDiffOn I I' 0 f univ ↔ ContinuousOn f univ
Tactic: rw [← contMDiffOn_univ, ← continuousOn_univ, contMDiffOn_zero_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'
rw : ContMDiffOn I I' 0 f univ ↔ Continuous[inst_4, inst_9] f
rw₁ : ContMDiffOn I I' 0 f univ ↔ ContinuousOn f univ
⊢ ContMDiff I I' 0 f ↔ Continuous[inst_4, inst_9] f
have rw₂ : ContinuousOn f univ ↔ ContinuousOn f univ
Tactic: rw [← contMDiffOn_univ, ← continuousOn_univ, contMDiffOn_zero_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 : ℕ∞
⊢ ContMDiffWithinAt I I' (↑n : ℕ∞ω) f s x ↔ ∀ (m : ℕ), (↑m : ℕ∞) ≤ n → ContMDiffWithinAt I I' (↑m : ℕ∞ω) f s x
have refine : ∀ (h : ∀ (m : ℕ), (↑m : ℕ∞) ≤ n → ContMDiffWithinAt I I' (↑m : ℕ∞ω) f s x), ContMDiffWithinAt I I' (↑n : ℕ∞ω) f s x
Tactic: refine ⟨fun h m hm => h.of_le (mod_cast hm), fun 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
x : M
n : ℕ∞
h : ∀ (m : ℕ), (↑m : ℕ∞) ≤ n → ContMDiffWithinAt I I' (↑m : ℕ∞ω) f s x
⊢ ContMDiffWithinAt I I' (↑n : ℕ∞ω) f s x
have none : ∀ (h : ∀ (m : ℕ), LE.le (α := ℕ∞) (↑m : ℕ∞) none → ContMDiffWithinAt I I' (↑m : ℕ∞ω) f s x),
  ContMDiffWithinAt I I' (↑none : ℕ∞ω) f s x
Tactic: obtain - | n := n
Cleared hypotheses: n, 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
x : M
n : ℕ∞
h : ∀ (m : ℕ), (↑m : ℕ∞) ≤ n → ContMDiffWithinAt I I' (↑m : ℕ∞ω) f s x
none :
  ∀ (h : ∀ (m : ℕ), LE.le (α := ℕ∞) (↑m : ℕ∞) Option.none → ContMDiffWithinAt I I' (↑m : ℕ∞ω) f s x),
    ContMDiffWithinAt I I' (↑Option.none : ℕ∞ω) f s x
⊢ ContMDiffWithinAt I I' (↑n : ℕ∞ω) f s x
have some : ∀ (n : ℕ) (h : ∀ (m : ℕ), (↑m : ℕ∞) ≤ some n → ContMDiffWithinAt I I' (↑m : ℕ∞ω) f s x),
  ContMDiffWithinAt I I' (↑(some n) : ℕ∞ω) f s x
Tactic: obtain - | n := n
Cleared hypotheses: n, 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
x : M
n : ℕ∞ω
⊢ ContMDiffWithinAt I I' n f s x ↔ ∀ m ≤ n, m ≠ ∞ → ContMDiffWithinAt I I' m f s x
have refine : ∀ (h : ∀ m ≤ n, m ≠ ∞ → ContMDiffWithinAt I I' m f s x), ContMDiffWithinAt I I' n f s x
Tactic: refine ⟨fun h m hm h'm ↦ h.of_le hm, fun 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
x : M
n : ℕ∞ω
h : ∀ m ≤ n, m ≠ ∞ → ContMDiffWithinAt I I' m f s x
⊢ ContMDiffWithinAt I I' n f s x
have top : ∀ (h : ∀ m ≤ ω, m ≠ ∞ → ContMDiffWithinAt I I' m f s x), ContMDiffWithinAt I I' ω f s x
Tactic: cases n with
  | top =>
    exact h _ le_rfl (by simp)
  | coe n =>
    exact contMDiffWithinAt_iff_nat.2 (fun m hm ↦ h _ (mod_cast hm) (by simp))
Cleared hypotheses: n, 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
x : M
n : ℕ∞ω
h : ∀ m ≤ n, m ≠ ∞ → ContMDiffWithinAt I I' m f s x
top : ∀ (h : ∀ m ≤ ω, m ≠ ∞ → ContMDiffWithinAt I I' m f s x), ContMDiffWithinAt I I' ω f s x
⊢ ContMDiffWithinAt I I' n f s x
have coe : ∀ (n : ℕ∞) (h : ∀ m ≤ (↑n : ℕ∞ω), m ≠ ∞ → ContMDiffWithinAt I I' m f s x), ContMDiffWithinAt I I' (↑n : ℕ∞ω) f s x
Tactic: cases n with
  | top =>
    exact h _ le_rfl (by simp)
  | coe n =>
    exact contMDiffWithinAt_iff_nat.2 (fun m hm ↦ h _ (mod_cast hm) (by simp))
Cleared hypotheses: n, 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'
x : M
n : ℕ∞ω
⊢ ContMDiffWithinAt I I' n f univ x ↔ ∀ m ≤ n, m ≠ ∞ → ContMDiffWithinAt I I' m f univ x
have rw : (∀ m ≤ n, m ≠ ∞ → ContMDiffWithinAt I I' m f univ x) ↔ ∀ m ≤ n, m ≠ ∞ → ContMDiffWithinAt I I' m f univ x
Tactic: rw [contMDiffWithinAt_iff_le_ne_infty]
-- 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 : ℕ∞ω
⊢ ContMDiffWithinAt I I' n f (insert x s) x ↔ ContMDiffWithinAt I I' n f s x
have simp : ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' insert x s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x) ↔
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I' (f x)) : 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)
Tactic: simp only [contMDiffWithinAt_iff, continuousWithinAt_insert_self]