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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ contDiffGroupoid n I'
hs : s ⊆ f ⁻¹' e'.source
hx : f x ∈ e'.source
h :
  ContDiffWithinAt 𝕜 m ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I : H → E) x)
A :
  ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x) ∈
    (↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E')
this :
  ContDiffWithinAt 𝕜 n ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H'))
    ((↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E'))
    (((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) ((↑I : H → E) x))
y : E
hy : y ∈ (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)
⊢ ((↑I' : H' → E') ∘ f ∘ (↑I.symm : E → H)) y ∈ (↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E')
have hy₁ : (↑I.symm : E → H) y ∈ s ∧ y ∈ range (↑I : H → E)
Tactic: simp only [mfld_simps] at hy
Cleared hypotheses: hy
-- 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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n : ℕ∞ω
s : Set H
x : H
t : Set H
f : H → H'
hts : s ∈ 𝓝[t] x
h : ContDiffWithinAtProp I I' n f s x
⊢ ContDiffWithinAtProp I I' n f t x
have refine : (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∈ 𝓝[(↑I.symm : E → H) ⁻¹' t ∩ range (↑I : H → E)] (↑I : H → E) x
Tactic: refine h.mono_of_mem_nhdsWithin ?_
-- 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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n : ℕ∞ω
s : Set H
x : H
t : Set H
f : H → H'
hts : s ∈ 𝓝[t] x
h : ContDiffWithinAtProp I I' n f s x
⊢ (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E) ∈ 𝓝[(↑I.symm : E → H) ⁻¹' t ∩ range (↑I : H → E)] (↑I : H → E) x
have refine : (↑I.symm : E → H) ⁻¹' s ∈ 𝓝[(↑I.symm : E → H) ⁻¹' t ∩ range (↑I : H → E)] (↑I : H → E) x
Tactic: refine inter_mem ?_ (mem_of_superset self_mem_nhdsWithin inter_subset_right)
-- 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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n : ℕ∞ω
s : Set H
x : H
t : Set H
f : H → H'
hts : s ∈ 𝓝[t] x
h : ContDiffWithinAtProp I I' n f s x
⊢ (↑I.symm : E → H) ⁻¹' s ∈ 𝓝[(↑I.symm : E → H) ⁻¹' t ∩ range (↑I : H → E)] (↑I : H → E) x
have rwa : s ∈ map (↑I.symm : E → H) (𝓝[(↑I.symm : E → H) ⁻¹' t ∩ range (↑I : H → E)] (↑I : H → E) x)
Tactic: rwa [← Filter.mem_map, ← I.image_eq, I.symm_map_nhdsWithin_image]
-- 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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type u_6
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n : ℕ∞ω
s : Set H
x : H
t : Set H
f : H → H'
hts : s ∈ 𝓝[t] x
h : ContDiffWithinAtProp I I' n f s x
rwa : s ∈ map (↑I.symm : E → H) (𝓝[(↑I.symm : E → H) ⁻¹' t ∩ range (↑I : H → E)] (↑I : H → E) x)
⊢ (↑I.symm : E → H) ⁻¹' s ∈ 𝓝[(↑I.symm : E → H) ⁻¹' t ∩ range (↑I : H → E)] (↑I : H → E) x
have rwa₁ : s ∈ map (↑I.symm : E → H) (𝓝[(↑I : H → E) '' t] (↑I : H → E) x)
Tactic: rwa [← Filter.mem_map, ← I.image_eq, I.symm_map_nhdsWithin_image]
-- 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
n : ℕ∞ω
x : H
⊢ ContDiffWithinAtProp I I n id univ x
have simp : ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑I.symm : E → H)) (range (↑I : H → E)) ((↑I : H → E) x)
Tactic: simp only [ContDiffWithinAtProp, id_comp, preimage_univ, univ_inter]
-- 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
n : ℕ∞ω
x : H
⊢ ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑I.symm : E → H)) (range (↑I : H → E)) ((↑I : H → E) x)
have this : ContDiffWithinAt 𝕜 n id (range (↑I : H → E)) ((↑I : H → E) x)
Tactic: have : ContDiffWithinAt 𝕜 n id (range I) (I x) := contDiff_id.contDiffAt.contDiffWithinAt
-- 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
n : ℕ∞ω
x : H
this : ContDiffWithinAt 𝕜 n id (range (↑I : H → E)) ((↑I : H → E) x)
⊢ ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑I.symm : E → H)) (range (↑I : H → E)) ((↑I : H → E) x)
have refine_1 : ∀ (y : E) (hy : y ∈ range (↑I : H → E)), ((↑I : H → E) ∘ (↑I.symm : E → H)) y = id y
Tactic: refine this.congr (fun y hy => ?_) ?_
-- 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
n : ℕ∞ω
x : H
this : ContDiffWithinAt 𝕜 n id (range (↑I : H → E)) ((↑I : H → E) x)
refine_1 : ∀ (y : E) (hy : y ∈ range (↑I : H → E)), ((↑I : H → E) ∘ (↑I.symm : E → H)) y = id y
⊢ ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑I.symm : E → H)) (range (↑I : H → E)) ((↑I : H → E) x)
have refine_2 : ((↑I : H → E) ∘ (↑I.symm : E → H)) ((↑I : H → E) x) = id ((↑I : H → E) x)
Tactic: refine this.congr (fun y hy => ?_) ?_
-- 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'
n : ℕ∞ω
f : M → M'
x : M
⊢ ContinuousAt f x ∧
      ContDiffWithinAtProp I I' n
        ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) univ
        ((↑(chartAt H x) : M → H) x) ↔
    ContinuousAt f x ∧
      ContDiffWithinAt 𝕜 n ((↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
have rw : ContinuousAt f x ∧
    ContDiffWithinAt 𝕜 n
      ((↑I' : H' → E') ∘
        ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) ∘
          (↑I.symm : E → H))
      (range (↑I : H → E)) ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) ↔
  ContinuousAt f x ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
Tactic: rw [ContDiffWithinAtProp, preimage_univ, univ_inter]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
x : M
n : ℕ∞ω
⊢ 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)
have 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)
Tactic: simp_rw [ContMDiffWithinAt, liftPropWithinAt_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 ↔
    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)
have 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)
Tactic: simp only [ContMDiffWithinAt, liftPropWithinAt_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 ↔
    ContinuousWithinAt f s x ∧ ContMDiffWithinAt I 𝓘(𝕜, E') n ((↑(extChartAt I' (f x)) : M' → E') ∘ f) s x
have 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)
Tactic: simp_rw [ContMDiffWithinAt, liftPropWithinAt_iff', ← and_assoc]
-- 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
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 ∧ 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)
have cont : 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
-- 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 : ℕ∞ω
cont :
  ContinuousWithinAt f s x ∧ ContinuousWithinAt ((↑(extChartAt I' (f x)) : M' → E') ∘ f) s x ↔ ContinuousWithinAt f s 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)
have 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))
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]
-- 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 : ℕ∞ω
x : M
⊢ ContMDiffAt I I' n f x ↔ ContinuousAt f x ∧ ContMDiffAt I 𝓘(𝕜, E') n ((↑(extChartAt I' (f x)) : M' → E') ∘ f) x
have rw : ContMDiffWithinAt I I' n f univ 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]
-- 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 : ℕ∞ω
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
⊢ ContMDiffAt I I' n f x ↔ ContinuousAt f x ∧ ContMDiffAt I 𝓘(𝕜, E') n ((↑(extChartAt I' (f x)) : M' → E') ∘ f) x
have rw₁ : ContMDiffWithinAt I I' n f univ x ↔
  ContinuousAt f x ∧ ContMDiffWithinAt I 𝓘(𝕜, E') n ((↑(extChartAt I' (f x)) : M' → E') ∘ f) univ x
Tactic: rw [ContMDiffAt, ContMDiffAt, contMDiffWithinAt_iff_target, continuousWithinAt_univ]
-- 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 : ℕ∞ω
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
⊢ ContMDiffAt I I' n f x ↔ ContinuousAt f x ∧ ContMDiffAt I 𝓘(𝕜, E') n ((↑(extChartAt I' (f x)) : M' → E') ∘ f) x
have 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
Tactic: rw [ContMDiffAt, ContMDiffAt, contMDiffWithinAt_iff_target, continuousWithinAt_univ]
-- 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 : ℕ∞ω
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
⊢ ContMDiffAt I I' n f x ↔ ContinuousAt f x ∧ ContMDiffAt I 𝓘(𝕜, E') n ((↑(extChartAt I' (f x)) : M' → E') ∘ f) x
have 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
Tactic: rw [ContMDiffAt, ContMDiffAt, contMDiffWithinAt_iff_target, continuousWithinAt_univ]
-- 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 ↔
    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)
have 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))
Tactic: simp_rw [ContMDiffWithinAt, liftPropWithinAt_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 : ℕ∞ω
⊢ 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)
have refine_1 : ∀ (h : 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: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩