awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
⊢ (∀ (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))) →
    ∀ (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))

Tactic:
fun h' x y => (h' y).2 x 0

Premises used: And.right, OfNat.ofNat
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
⊢ (∀ (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))) →
    ∀ (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))

Tactic:
exact fun h' x y => (h' y).2 x 0
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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 ∧
      ∀ (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) ⁻¹' f ⁻¹' (extChartAt I' y).source)

Tactic:
simp [← contMDiffOn_univ, contMDiffOn_iff, continuousOn_univ]

Premises used: contMDiffOn_iff, contMDiffOn_univ, continuousOn_univ
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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'
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)
⊢ 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)

Tactic:
rw [← contMDiffOn_univ, contMDiffOn_iff_target]

Premises used: contMDiffOn_univ, contMDiffOn_iff_target
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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'
⊢ (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:
simp [continuousOn_univ]

Premises used: continuousOn_univ
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
rw₂ rw₃ : ContinuousOn f univ ↔ ContinuousOn f univ
⊢ ContMDiff I I' 0 f ↔ Continuous[inst_4, inst_9] f

Tactic:
rw [← contMDiffOn_univ, ← continuousOn_univ, contMDiffOn_zero_iff]

Premises used: contMDiffOn_univ, continuousOn_univ, contMDiffOn_zero_iff
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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 : ContMDiffWithinAt I I' (n + 1) f s x
⊢ ContMDiffWithinAt I I' n f s x

Tactic:
h.of_le le_self_add

Premises used: ContMDiffWithinAt.of_le, le_self_add
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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 : ℕ∞ω
h : ContMDiffAt I I' (n + 1) f x
⊢ ContMDiffAt I I' n f x

Tactic:
ContMDiffWithinAt.of_succ h

Premises used: ContMDiffWithinAt.of_succ, ContMDiffAt
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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 : ℕ∞ω
h : ContMDiffOn I I' (n + 1) f s
⊢ ContMDiffOn I I' n f s

Tactic:
fun x hx => (h x hx).of_succ

Premises used: ContMDiffWithinAt.of_succ, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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 : ℕ∞ω
h : ContMDiff I I' (n + 1) f
⊢ ContMDiff I I' n f

Tactic:
fun x =>
  (h x).of_succ

Premises used: ContMDiff, ContMDiffAt.of_succ
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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 : ℕ∞ω
hf : ContMDiffWithinAt I I' n f s x
⊢ ContinuousWithinAt f s x

Tactic:
hf.1

Premises used: ChartedSpace.LiftPropWithinAt.continuousWithinAt
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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 : ℕ∞ω
hf : ContMDiffAt I I' n f x
⊢ ContinuousAt f x

Tactic:
(continuousWithinAt_univ _ _).1 <| ContMDiffWithinAt.continuousWithinAt hf

Premises used: continuousWithinAt_univ, Iff.mp, ContMDiffWithinAt.continuousWithinAt
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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 : ℕ∞ω
hf : ContMDiffOn I I' n f s
⊢ ContinuousOn f s

Tactic:
fun x hx =>
  (hf x hx).continuousWithinAt

Premises used: ContinuousOn, ContMDiffWithinAt.continuousWithinAt
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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 : ℕ∞ω
hf : ContMDiff I I' n f
⊢ Continuous[inst_4, inst_9] f

Tactic:
continuous_iff_continuousAt.2 fun x => (hf x).continuousAt

Premises used: Iff.mpr, ContMDiffAt.continuousAt, continuous_iff_continuousAt
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
⊢ ContMDiffWithinAt I I' ∞ f s x ↔ ∀ (n : ℕ), ContMDiffWithinAt I I' (↑n : ℕ∞ω) f s x

Tactic:
⟨fun h n => ⟨h.1, contDiffWithinAt_infty.1 h.2 n⟩, fun H =>
    ⟨(H 0).1, contDiffWithinAt_infty.2 fun n => (H n).2⟩⟩

Premises used: Iff.mpr, ChartedSpace.LiftPropWithinAt.prop, ChartedSpace.LiftPropWithinAt.continuousWithinAt, contDiffWithinAt_infty, Iff.intro, Iff.mp, OfNat.ofNat, ChartedSpace.LiftPropWithinAt.mk
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
⊢ ContMDiffAt I I' ∞ f x ↔ ∀ (n : ℕ), ContMDiffAt I I' (↑n : ℕ∞ω) f x

Tactic:
contMDiffWithinAt_infty

Premises used: ContMDiffAt, contMDiffWithinAt_infty
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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' ∞ f s ↔ ∀ (n : ℕ), ContMDiffOn I I' (↑n : ℕ∞ω) f s

Tactic:
⟨fun h _ => h.of_le (mod_cast le_top),
    fun h x hx => contMDiffWithinAt_infty.2 fun n => h n x hx⟩

Premises used: Iff.mpr, WithTop.coe_le_coe._simp_1, ContMDiffOn.of_le, cast, le_top, Iff.intro, contMDiffWithinAt_infty, Eq.symm
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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' ∞ f ↔ ∀ (n : ℕ), ContMDiff I I' (↑n : ℕ∞ω) f

Tactic:
⟨fun h _ => h.of_le (mod_cast le_top), fun h x => contMDiffWithinAt_infty.2 fun n => h n x⟩

Premises used: Iff.mpr, WithTop.coe_le_coe._simp_1, cast, le_top, Iff.intro, contMDiffWithinAt_infty, ContMDiff.of_le, Eq.symm
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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

Tactic:
⟨fun h m hm => h.of_le (mod_cast hm), fun h => ?_⟩

Premises used: WithTop.coe_le_coe._simp_1, cast, ContMDiffWithinAt.of_le, Iff.intro, Eq.symm
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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 : ℕ∞
refine :
  ∀ (h : ∀ (m : ℕ), (↑m : ℕ∞) ≤ n → ContMDiffWithinAt I I' (↑m : ℕ∞ω) f s x), ContMDiffWithinAt I I' (↑n : ℕ∞ω) f s x
⊢ ContMDiffWithinAt I I' (↑n : ℕ∞ω) f s x ↔ ∀ (m : ℕ), (↑m : ℕ∞) ≤ n → ContMDiffWithinAt I I' (↑m : ℕ∞ω) f s x

Tactic:
refine ⟨fun h m hm => h.of_le (mod_cast hm), fun h => ?_⟩
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
some :
  ∀ (n : ℕ) (h : ∀ (m : ℕ), (↑m : ℕ∞) ≤ Option.some n → ContMDiffWithinAt I I' (↑m : ℕ∞ω) f s x),
    ContMDiffWithinAt I I' (↑(Option.some n) : ℕ∞ω) f s x
⊢ ContMDiffWithinAt I I' (↑n : ℕ∞ω) f s x

Tactic:
obtain - | n := n
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
h : ∀ (m : ℕ), LE.le (α := ℕ∞) (↑m : ℕ∞) none → ContMDiffWithinAt I I' (↑m : ℕ∞ω) f s x
⊢ ContMDiffWithinAt I I' (↑none : ℕ∞ω) f s x

Tactic:
contMDiffWithinAt_infty.2 fun n => h n le_top

Premises used: Iff.mpr, le_top, contMDiffWithinAt_infty
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
h : ∀ (m : ℕ), LE.le (α := ℕ∞) (↑m : ℕ∞) none → ContMDiffWithinAt I I' (↑m : ℕ∞ω) f s x
⊢ ContMDiffWithinAt I I' (↑none : ℕ∞ω) f s x

Tactic:
exact contMDiffWithinAt_infty.2 fun n => h n le_top

Premises used: Iff.mpr, le_top, contMDiffWithinAt_infty
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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 : ℕ∞) ≤ some n → ContMDiffWithinAt I I' (↑m : ℕ∞ω) f s x
⊢ ContMDiffWithinAt I I' (↑(some n) : ℕ∞ω) f s x

Tactic:
h n le_rfl

Premises used: le_rfl, WithTop.some
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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 : ℕ∞) ≤ some n → ContMDiffWithinAt I I' (↑m : ℕ∞ω) f s x
⊢ ContMDiffWithinAt I I' (↑(some n) : ℕ∞ω) f s x

Tactic:
exact h n le_rfl

Premises used: le_rfl
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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 : ℕ∞
⊢ ContMDiffAt I I' (↑n : ℕ∞ω) f x ↔ ∀ (m : ℕ), (↑m : ℕ∞) ≤ n → ContMDiffAt I I' (↑m : ℕ∞ω) f x

Tactic:
simp [← contMDiffWithinAt_univ, contMDiffWithinAt_iff_nat]

Premises used: contMDiffWithinAt_univ, contMDiffWithinAt_iff_nat