awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : ChartedSpace H'' M''
f : M → M'
s : Set M
n : ℕ∞ω
t : Set M'
g : M' → M''
x : M
st : MapsTo f s t
e : PartialEquiv M E := extChartAt I x
e' : PartialEquiv M' E' := extChartAt I' (f x)
hg :
  ContinuousWithinAt g t (f x) ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M'))
      ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) (writtenInExtChartAt I I' x f ((↑e : M → E) x))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑e' : M' → E') ∘ f ∘ (↑e.symm : E → M)) ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑e : M → E) x)
this : (↑e' : M' → E') (f x) = writtenInExtChartAt I I' x f ((↑e : M → E) x)
⊢ ∀ᶠ (y : E) in 𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x,
    f ((↑e.symm : E → M) y) ∈ t ∧ f ((↑e.symm : E → M) y) ∈ e'.source
have simp : ∀ᶠ (a : M) in 𝓝[s] x,
  f ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) a)) ∈ t ∧
    f ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) a)) ∈ e'.source
Tactic: simp only [e, ← map_extChartAt_nhdsWithin, eventually_map]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : ChartedSpace H'' M''
f : M → M'
s : Set M
n : ℕ∞ω
t : Set M'
g : M' → M''
x : M
st : MapsTo f s t
e : PartialEquiv M E := extChartAt I x
e' : PartialEquiv M' E' := extChartAt I' (f x)
hg :
  ContinuousWithinAt g t (f x) ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M'))
      ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) (writtenInExtChartAt I I' x f ((↑e : M → E) x))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑e' : M' → E') ∘ f ∘ (↑e.symm : E → M)) ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑e : M → E) x)
this : (↑e' : M' → E') (f x) = writtenInExtChartAt I I' x f ((↑e : M → E) x)
⊢ ∀ᶠ (a : M) in 𝓝[s] x,
    f ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) a)) ∈ t ∧
      f ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) a)) ∈ e'.source
have h : ∀ a ∈ f ⁻¹' (extChartAt I' (f x)).source,
  a ∈ s ∩ (extChartAt I x).source →
    f ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) a)) ∈ t ∧
      f ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) a)) ∈ e'.source
Tactic: filter_upwards [hf.1.tendsto (extChartAt_source_mem_nhds (I := I') (f x)),
      inter_mem_nhdsWithin s (extChartAt_source_mem_nhds (I := I) x)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : ChartedSpace H'' M''
f : M → M'
s : Set M
n : ℕ∞ω
t : Set M'
g : M' → M''
x : M
st : MapsTo f s t
e : PartialEquiv M E := extChartAt I x
e' : PartialEquiv M' E' := extChartAt I' (f x)
hg :
  ContinuousWithinAt g t (f x) ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M'))
      ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) (writtenInExtChartAt I I' x f ((↑e : M → E) x))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑e' : M' → E') ∘ f ∘ (↑e.symm : E → M)) ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑e : M → E) x)
this : (↑e' : M' → E') (f x) = writtenInExtChartAt I I' x f ((↑e : M → E) x)
⊢ ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' ((g ∘ f) x)) : M'' → E'') ∘ (g ∘ f) ∘ (↑e.symm : E → M))
    ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑e : M → E) x)
have A : ∀ᶠ (y : E) in 𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x,
  f ((↑e.symm : E → M) y) ∈ t ∧ f ((↑e.symm : E → M) y) ∈ e'.source
Tactic: have A : ∀ᶠ y in 𝓝[e.symm ⁻¹' s ∩ range I] e x, f (e.symm y) ∈ t ∧ f (e.symm y) ∈ e'.source := by
    simp only [e, ← map_extChartAt_nhdsWithin, eventually_map]
    filter_upwards [hf.1.tendsto (extChartAt_source_mem_nhds (I := I') (f x)),
      inter_mem_nhdsWithin s (extChartAt_source_mem_nhds (I := I) x)]
    rintro x' (hfx' : f x' ∈ e'.source) ⟨hx's, hx'⟩
    simp only [e, true_and, e.left_inv hx', st hx's, *]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : ChartedSpace H'' M''
f : M → M'
s : Set M
n : ℕ∞ω
t : Set M'
g : M' → M''
x : M
st : MapsTo f s t
e : PartialEquiv M E := extChartAt I x
e' : PartialEquiv M' E' := extChartAt I' (f x)
hg :
  ContinuousWithinAt g t (f x) ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M'))
      ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) (writtenInExtChartAt I I' x f ((↑e : M → E) x))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑e' : M' → E') ∘ f ∘ (↑e.symm : E → M)) ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑e : M → E) x)
this : (↑e' : M' → E') (f x) = writtenInExtChartAt I I' x f ((↑e : M → E) x)
A :
  ∀ᶠ (y : E) in 𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x,
    f ((↑e.symm : E → M) y) ∈ t ∧ f ((↑e.symm : E → M) y) ∈ e'.source
⊢ ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' ((g ∘ f) x)) : M'' → E'') ∘ (g ∘ f) ∘ (↑e.symm : E → M))
    ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑e : M → E) x)
have refine_1 : writtenInExtChartAt I I' x f ⁻¹' ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) ∈
  𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x
Tactic: refine ((hg.2.comp _ (hf.2.mono inter_subset_right)
      ((mapsTo_preimage _ _).mono_left inter_subset_left)).mono_of_mem_nhdsWithin
      (inter_mem ?_ self_mem_nhdsWithin)).congr_of_eventuallyEq ?_ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : ChartedSpace H'' M''
f : M → M'
s : Set M
n : ℕ∞ω
t : Set M'
g : M' → M''
x : M
st : MapsTo f s t
e : PartialEquiv M E := extChartAt I x
e' : PartialEquiv M' E' := extChartAt I' (f x)
hg :
  ContinuousWithinAt g t (f x) ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M'))
      ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) (writtenInExtChartAt I I' x f ((↑e : M → E) x))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑e' : M' → E') ∘ f ∘ (↑e.symm : E → M)) ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑e : M → E) x)
this : (↑e' : M' → E') (f x) = writtenInExtChartAt I I' x f ((↑e : M → E) x)
A :
  ∀ᶠ (y : E) in 𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x,
    f ((↑e.symm : E → M) y) ∈ t ∧ f ((↑e.symm : E → M) y) ∈ e'.source
refine_1 :
  writtenInExtChartAt I I' x f ⁻¹' ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) ∈
    𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x
⊢ ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' ((g ∘ f) x)) : M'' → E'') ∘ (g ∘ f) ∘ (↑e.symm : E → M))
    ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑e : M → E) x)
have refine_2 : (↑(extChartAt I'' ((g ∘ f) x)) : M'' → E'') ∘
    (g ∘ f) ∘ (↑e.symm : E → M) =ᶠ[𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x]
  ((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M')) ∘ writtenInExtChartAt I I' x f
Tactic: refine ((hg.2.comp _ (hf.2.mono inter_subset_right)
      ((mapsTo_preimage _ _).mono_left inter_subset_left)).mono_of_mem_nhdsWithin
      (inter_mem ?_ self_mem_nhdsWithin)).congr_of_eventuallyEq ?_ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : ChartedSpace H'' M''
f : M → M'
s : Set M
n : ℕ∞ω
t : Set M'
g : M' → M''
x : M
st : MapsTo f s t
e : PartialEquiv M E := extChartAt I x
e' : PartialEquiv M' E' := extChartAt I' (f x)
hg :
  ContinuousWithinAt g t (f x) ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M'))
      ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) (writtenInExtChartAt I I' x f ((↑e : M → E) x))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑e' : M' → E') ∘ f ∘ (↑e.symm : E → M)) ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑e : M → E) x)
this : (↑e' : M' → E') (f x) = writtenInExtChartAt I I' x f ((↑e : M → E) x)
A :
  ∀ᶠ (y : E) in 𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x,
    f ((↑e.symm : E → M) y) ∈ t ∧ f ((↑e.symm : E → M) y) ∈ e'.source
refine_1 :
  writtenInExtChartAt I I' x f ⁻¹' ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) ∈
    𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x
refine_2 :
  (↑(extChartAt I'' ((g ∘ f) x)) : M'' → E'') ∘
      (g ∘ f) ∘ (↑e.symm : E → M) =ᶠ[𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x]
    ((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M')) ∘ writtenInExtChartAt I I' x f
⊢ ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' ((g ∘ f) x)) : M'' → E'') ∘ (g ∘ f) ∘ (↑e.symm : E → M))
    ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑e : M → E) x)
have refine_3 : ((↑(extChartAt I'' ((g ∘ f) x)) : M'' → E'') ∘ (g ∘ f) ∘ (↑e.symm : E → M)) ((↑e : M → E) x) =
  (((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M')) ∘ writtenInExtChartAt I I' x f)
    ((↑e : M → E) x)
Tactic: refine ((hg.2.comp _ (hf.2.mono inter_subset_right)
      ((mapsTo_preimage _ _).mono_left inter_subset_left)).mono_of_mem_nhdsWithin
      (inter_mem ?_ self_mem_nhdsWithin)).congr_of_eventuallyEq ?_ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : ChartedSpace H'' M''
f : M → M'
s : Set M
n : ℕ∞ω
t : Set M'
g : M' → M''
x : M
st : MapsTo f s t
e : PartialEquiv M E := extChartAt I x
e' : PartialEquiv M' E' := extChartAt I' (f x)
hg :
  ContinuousWithinAt g t (f x) ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M'))
      ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) (writtenInExtChartAt I I' x f ((↑e : M → E) x))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑e' : M' → E') ∘ f ∘ (↑e.symm : E → M)) ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑e : M → E) x)
this : (↑e' : M' → E') (f x) = writtenInExtChartAt I I' x f ((↑e : M → E) x)
A :
  ∀ᶠ (y : E) in 𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x,
    f ((↑e.symm : E → M) y) ∈ t ∧ f ((↑e.symm : E → M) y) ∈ e'.source
⊢ writtenInExtChartAt I I' x f ⁻¹' ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) ∈
    𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x
have h : ∀ (a : E),
  f ((↑e.symm : E → M) a) ∈ t ∧ f ((↑e.symm : E → M) a) ∈ e'.source →
    a ∈ writtenInExtChartAt I I' x f ⁻¹' ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E'))
Tactic: filter_upwards [A]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : ChartedSpace H'' M''
f : M → M'
s : Set M
n : ℕ∞ω
t : Set M'
g : M' → M''
x : M
st : MapsTo f s t
e : PartialEquiv M E := extChartAt I x
e' : PartialEquiv M' E' := extChartAt I' (f x)
hg :
  ContinuousWithinAt g t (f x) ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M'))
      ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) (writtenInExtChartAt I I' x f ((↑e : M → E) x))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑e' : M' → E') ∘ f ∘ (↑e.symm : E → M)) ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑e : M → E) x)
this : (↑e' : M' → E') (f x) = writtenInExtChartAt I I' x f ((↑e : M → E) x)
A :
  ∀ᶠ (y : E) in 𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x,
    f ((↑e.symm : E → M) y) ∈ t ∧ f ((↑e.symm : E → M) y) ∈ e'.source
x' : E
ht : f ((↑e.symm : E → M) x') ∈ t
hfx' : f ((↑e.symm : E → M) x') ∈ e'.source
⊢ x' ∈ writtenInExtChartAt I I' x f ⁻¹' ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E'))
have h : (↑(extChartAt I' (f x)) : M' → E') (f ((↑(extChartAt I x).symm : E → M) x')) ∈ range (↑I' : H' → E')
Tactic: simp only [*, e, e', mem_preimage, writtenInExtChartAt, (· ∘ ·), mem_inter_iff, e'.left_inv,
      true_and]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : ChartedSpace H'' M''
f : M → M'
s : Set M
n : ℕ∞ω
t : Set M'
g : M' → M''
x : M
st : MapsTo f s t
e : PartialEquiv M E := extChartAt I x
e' : PartialEquiv M' E' := extChartAt I' (f x)
hg :
  ContinuousWithinAt g t (f x) ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M'))
      ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) (writtenInExtChartAt I I' x f ((↑e : M → E) x))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑e' : M' → E') ∘ f ∘ (↑e.symm : E → M)) ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑e : M → E) x)
this : (↑e' : M' → E') (f x) = writtenInExtChartAt I I' x f ((↑e : M → E) x)
A :
  ∀ᶠ (y : E) in 𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x,
    f ((↑e.symm : E → M) y) ∈ t ∧ f ((↑e.symm : E → M) y) ∈ e'.source
⊢ (↑(extChartAt I'' ((g ∘ f) x)) : M'' → E'') ∘
      (g ∘ f) ∘ (↑e.symm : E → M) =ᶠ[𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x]
    ((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M')) ∘ writtenInExtChartAt I I' x f
have h : ∀ (a : E),
  f ((↑e.symm : E → M) a) ∈ t ∧ f ((↑e.symm : E → M) a) ∈ e'.source →
    ((↑(extChartAt I'' ((g ∘ f) x)) : M'' → E'') ∘ (g ∘ f) ∘ (↑e.symm : E → M)) a =
      (((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M')) ∘ writtenInExtChartAt I I' x f) a
Tactic: filter_upwards [A]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : ChartedSpace H'' M''
f : M → M'
s : Set M
n : ℕ∞ω
t : Set M'
g : M' → M''
x : M
y : M'
hg : ContMDiffWithinAt I' I'' n g t y
hf : ContMDiffWithinAt I I' n f s x
st : MapsTo f s t
hx : f x = y
⊢ ContMDiffWithinAt I I'' n (g ∘ f) s x
have hg₁ : ContMDiffWithinAt I' I'' n g t (f x)
Tactic: subst hx
Cleared hypotheses: y, hg, hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : ChartedSpace H'' M''
f : M → M'
n : ℕ∞ω
g : M' → M''
hg : ContMDiff I' I'' n g
hf : ContMDiff I I' n f
⊢ ContMDiff I I'' n (g ∘ f)
have rw : ∀ (hg : ContMDiffOn I' I'' n g univ) (hf : ContMDiffOn I I' n f univ), ContMDiffOn I I'' n (g ∘ f) univ
Tactic: rw [← contMDiffOn_univ] at hf hg ⊢
Cleared hypotheses: hg, hf
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : ChartedSpace H'' M''
f : M → M'
s : Set M
n : ℕ∞ω
g : M' → M''
x : M
y : M'
hg : ContMDiffAt I' I'' n g y
hf : ContMDiffWithinAt I I' n f s x
hx : f x = y
⊢ ContMDiffWithinAt I I'' n (g ∘ f) s x
have hg₁ : ContMDiffAt I' I'' n g (f x)
Tactic: subst hx
Cleared hypotheses: y, hg, hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : ChartedSpace H'' M''
f : M → M'
n : ℕ∞ω
g : M' → M''
x : M
y : M'
hg : ContMDiffAt I' I'' n g y
hf : ContMDiffAt I I' n f x
hx : f x = y
⊢ ContMDiffAt I I'' n (g ∘ f) x
have hg₁ : ContMDiffAt I' I'' n g (f x)
Tactic: subst hx
Cleared hypotheses: y, hg, hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Basic (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
s : Set M
n : ℕ∞ω
f : M → M
hf : ContMDiffOn I I n f s
hmaps : MapsTo f s s
k : ℕ
⊢ ContMDiffOn I I n f^[k] s
have zero : ContMDiffOn I I n f^[0] s
Tactic: induction k with
  | zero => simpa using contMDiffOn_id
  | succ k h => simpa using h.comp hf hmaps
Cleared hypotheses: k