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
x : M
m n : ℕ∞ω
hf : LiftPropWithinAt (ContDiffWithinAtProp I I' n) f s x
le : m ≤ n
⊢ LiftPropWithinAt (ContDiffWithinAtProp I I' m) f s x

Tactic:
⟨hf.1, hf.2.of_le (mod_cast le)⟩

Premises used: ChartedSpace.LiftPropWithinAt.prop, ContDiffWithinAt.of_le, ChartedSpace.LiftPropWithinAt.continuousWithinAt, cast, LE.le, Eq.refl, 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'
s : Set M
x : M
m n : ℕ∞ω
hf : LiftPropWithinAt (ContDiffWithinAtProp I I' n) f s x
le : m ≤ n
⊢ LiftPropWithinAt (ContDiffWithinAtProp I I' m) f s x

Tactic:
exact ⟨hf.1, hf.2.of_le (mod_cast le)⟩
-- 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
m n : ℕ∞ω
hf : ContMDiffAt I I' n f x
le : m ≤ n
⊢ ContMDiffAt I I' m f x

Tactic:
ContMDiffWithinAt.of_le hf le

Premises used: ContMDiffWithinAt.of_le, 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
m n : ℕ∞ω
hf : ContMDiffOn I I' n f s
le : m ≤ n
⊢ ContMDiffOn I I' m f s

Tactic:
fun x hx => (hf x hx).of_le le

Premises used: ContMDiffWithinAt.of_le, 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'
m n : ℕ∞ω
hf : ContMDiff I I' n f
le : m ≤ n
⊢ ContMDiff I I' m f

Tactic:
fun x =>
  (hf x).of_le le

Premises used: ContMDiff, ContMDiffAt.of_le
-- 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 : ContMDiff I I' n f
⊢ ContMDiffAt I I' n f x

Tactic:
h x
-- 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 : ℕ∞ω
⊢ ContMDiffWithinAt I I' n f univ x ↔ ContMDiffAt I I' n f x

Tactic:
Iff.rfl

Premises used: Iff.rfl, 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'
n : ℕ∞ω
⊢ ContMDiffOn I I' n f ∅

Tactic:
fun _x hx ↦ hx.elim

Premises used: False.elim, 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 : ℕ∞ω
⊢ ContMDiffOn I I' n f univ ↔ ContMDiff I I' n f

Tactic:
simp only [ContMDiffOn, ContMDiff, contMDiffWithinAt_univ, forall_prop_of_true, mem_univ]

Premises used: ContMDiff, forall_prop_of_true, Set.mem_univ, contMDiffWithinAt_univ, 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'
s : Set M
x : M
n : ℕ∞ω
simp_rw :
  ContinuousWithinAt f s x ∧
      ContDiffWithinAtProp I I' n
        ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) 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)
⊢ ContMDiffWithinAt I I' n f s 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_rw [ContMDiffWithinAt, liftPropWithinAt_iff']

Premises used: ContMDiffWithinAt, ChartedSpace.liftPropWithinAt_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 : ℕ∞ω
⊢ ContinuousWithinAt f s x ∧
      ContDiffWithinAtProp I I' n
        ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) 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:
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'
s : Set M
x : M
n : ℕ∞ω
simp :
  ContinuousWithinAt f s x ∧
      ContDiffWithinAtProp I I' n
        ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x) ↔
    ContinuousWithinAt f s x ∧
      ContDiffWithinAt 𝕜 n ((↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source))
        ((↑(extChartAt I x) : M → E) x)
⊢ ContMDiffWithinAt I I' n f s x ↔
    ContinuousWithinAt f s x ∧
      ContDiffWithinAt 𝕜 n ((↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source))
        ((↑(extChartAt I x) : M → E) x)

Tactic:
simp only [ContMDiffWithinAt, liftPropWithinAt_iff']

Premises used: ContMDiffWithinAt, ChartedSpace.liftPropWithinAt_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 : ℕ∞ω
⊢ ContinuousWithinAt f s x ∧
      ContDiffWithinAtProp I I' n
        ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x) ↔
    ContinuousWithinAt f s x ∧
      ContDiffWithinAt 𝕜 n ((↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source))
        ((↑(extChartAt I x) : M → E) x)

Tactic:
and_congr_right fun hc => contDiffWithinAt_congr_set <|
    hc.extChartAt_symm_preimage_inter_range_eventuallyEq

Premises used: ContinuousWithinAt.extChartAt_symm_preimage_inter_range_eventuallyEq, contDiffWithinAt_congr_set, and_congr_right
-- 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 : ℕ∞ω
⊢ ContinuousWithinAt f s x ∧
      ContDiffWithinAtProp I I' n
        ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x) ↔
    ContinuousWithinAt f s x ∧
      ContDiffWithinAt 𝕜 n ((↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source))
        ((↑(extChartAt I x) : M → E) x)

Tactic:
exact and_congr_right fun hc => contDiffWithinAt_congr_set <|
    hc.extChartAt_symm_preimage_inter_range_eventuallyEq

Premises used: contDiffWithinAt_congr_set, and_congr_right
-- 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 : ℕ∞ω
simp_rw :
  ContinuousWithinAt f s x ∧
      ContDiffWithinAtProp I I' n
        ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x) ↔
    (ContinuousWithinAt f s x ∧ ContinuousWithinAt ((↑(extChartAt I' (f x)) : M' → E') ∘ f) s x) ∧
      ContDiffWithinAtProp I 𝓘(𝕜, E') n
        ((↑(chartAt E' (((↑(extChartAt I' (f x)) : M' → E') ∘ f) x)) : E' → E') ∘
          ((↑(extChartAt I' (f x)) : M' → E') ∘ f) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x)
⊢ ContMDiffWithinAt I I' n f s x ↔
    ContinuousWithinAt f s x ∧ ContMDiffWithinAt I 𝓘(𝕜, E') n ((↑(extChartAt I' (f x)) : M' → E') ∘ f) s x

Tactic:
simp_rw [ContMDiffWithinAt, liftPropWithinAt_iff', ← and_assoc]

Premises used: ContMDiffWithinAt, and_assoc, ChartedSpace.liftPropWithinAt_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 : ℕ∞ω
⊢ ContinuousWithinAt f s x ∧ ContinuousWithinAt ((↑(extChartAt I' (f x)) : M' → E') ∘ f) s x ↔ ContinuousWithinAt f s x

Tactic:
have cont :
    ContinuousWithinAt f s x ∧ ContinuousWithinAt (extChartAt I' (f x) ∘ f) s x ↔
        ContinuousWithinAt f s x :=
      and_iff_left_of_imp <| (continuousAt_extChartAt _).comp_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
x : M
n : ℕ∞ω
cont :
  ContinuousWithinAt f s x ∧ ContinuousWithinAt ((↑(extChartAt I' (f x)) : M' → E') ∘ f) s x ↔ ContinuousWithinAt f s x
simp_rw :
  ContinuousWithinAt f s x ∧
      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.symm (chartAt H x)) : H → M) ⁻¹' s ∩ range (↑I : H → E))
        ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) ↔
    ContinuousWithinAt f s x ∧
      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.symm (chartAt H x)) : H → M) ⁻¹' s ∩ range (↑I : H → E))
        ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
⊢ ContinuousWithinAt f s x ∧
      ContDiffWithinAtProp I I' n
        ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x) ↔
    (ContinuousWithinAt f s x ∧ ContinuousWithinAt ((↑(extChartAt I' (f x)) : M' → E') ∘ f) s x) ∧
      ContDiffWithinAtProp I 𝓘(𝕜, E') n
        ((↑(chartAt E' (((↑(extChartAt I' (f x)) : M' → E') ∘ f) x)) : E' → E') ∘
          ((↑(extChartAt I' (f x)) : M' → E') ∘ f) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x)

Tactic:
simp_rw [cont, ContDiffWithinAtProp, extChartAt, OpenPartialHomeomorph.extend,
    PartialEquiv.coe_trans, ModelWithCorners.toPartialEquiv_coe, OpenPartialHomeomorph.coe_coe,
    modelWithCornersSelf_coe, chartAt_self_eq, OpenPartialHomeomorph.refl_apply, id_comp]

Premises used: extChartAt, OpenPartialHomeomorph.coe_coe, OpenPartialHomeomorph.refl_apply, ModelWithCorners.toPartialEquiv_coe, PartialEquiv.coe_trans, modelWithCornersSelf_coe, ContDiffWithinAtProp, OpenPartialHomeomorph.extend, chartAt_self_eq, Function.id_comp
-- 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 : ℕ∞ω
cont :
  ContinuousWithinAt f s x ∧ ContinuousWithinAt ((↑(extChartAt I' (f x)) : M' → E') ∘ f) s x ↔ ContinuousWithinAt f s x
⊢ ContinuousWithinAt f s x ∧
      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.symm (chartAt H x)) : H → M) ⁻¹' s ∩ range (↑I : H → E))
        ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) ↔
    ContinuousWithinAt f s x ∧
      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.symm (chartAt H x)) : H → M) ⁻¹' s ∩ range (↑I : H → E))
        ((↑I : H → E) ((↑(chartAt H x) : M → H) x))

Tactic:
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'
n : ℕ∞ω
x : M
rw :
  ContMDiffWithinAt I I' n f univ x ↔
    ContinuousAt f x ∧ ContMDiffAt I 𝓘(𝕜, E') n ((↑(extChartAt I' (f x)) : M' → E') ∘ f) x
rw₁ :
  ContMDiffWithinAt I I' n f univ x ↔
    ContinuousAt f x ∧ ContMDiffWithinAt I 𝓘(𝕜, E') n ((↑(extChartAt I' (f x)) : M' → E') ∘ f) univ x
rw₂ :
  ContinuousWithinAt f univ x ∧ ContMDiffWithinAt I 𝓘(𝕜, E') n ((↑(extChartAt I' (f x)) : M' → E') ∘ f) univ x ↔
    ContinuousAt f x ∧ ContMDiffWithinAt I 𝓘(𝕜, E') n ((↑(extChartAt I' (f x)) : M' → E') ∘ f) univ x
rw₃ rw₄ :
  ContinuousAt f x ∧ ContMDiffWithinAt I 𝓘(𝕜, E') n ((↑(extChartAt I' (f x)) : M' → E') ∘ f) univ x ↔
    ContinuousAt f x ∧ ContMDiffWithinAt I 𝓘(𝕜, E') n ((↑(extChartAt I' (f x)) : M' → E') ∘ f) univ x
⊢ ContMDiffAt I I' n f x ↔ ContinuousAt f x ∧ ContMDiffAt I 𝓘(𝕜, E') n ((↑(extChartAt I' (f x)) : M' → E') ∘ f) x

Tactic:
rw [ContMDiffAt, ContMDiffAt, contMDiffWithinAt_iff_target, continuousWithinAt_univ]

Premises used: contMDiffWithinAt_iff_target, continuousWithinAt_univ, 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
x : M
n : ℕ∞ω
simp_rw :
  ContinuousWithinAt f s x ∧
      ContDiffWithinAtProp I I' n
        ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x) ↔
    ContinuousWithinAt (f ∘ (↑(extChartAt I x).symm : E → M))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x) ∧
      ContDiffWithinAtProp 𝓘(𝕜, E) I' n
        ((↑(chartAt H' ((f ∘ (↑(extChartAt I x).symm : E → M)) ((↑(extChartAt I x) : M → E) x))) : M' → H') ∘
          (f ∘ (↑(extChartAt I x).symm : E → M)) ∘
            (↑(OpenPartialHomeomorph.symm (chartAt E ((↑(extChartAt I x) : M → E) x))) : E → E))
        ((↑(OpenPartialHomeomorph.symm (chartAt E ((↑(extChartAt I x) : M → E) x))) : E → E) ⁻¹'
          ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)))
        ((↑(chartAt E ((↑(extChartAt I x) : M → E) x)) : E → E) ((↑(extChartAt I x) : M → E) x))
⊢ ContMDiffWithinAt I I' n f s x ↔
    ContMDiffWithinAt 𝓘(𝕜, E) I' n (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_rw [ContMDiffWithinAt, liftPropWithinAt_iff']

Premises used: ContMDiffWithinAt, ChartedSpace.liftPropWithinAt_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 : ℕ∞ω
⊢ ContinuousWithinAt f s x ↔
    ContinuousWithinAt (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:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro