awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalSourceTargetProperty (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
F' : Type u_5
H : Type u_6
H' : Type u_7
G : Type u_8
G' : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜 F'
inst_9 : TopologicalSpace H
inst_10 : TopologicalSpace H'
inst_11 : TopologicalSpace G
inst_12 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F' G'
M : Type u_10
M' : Type u_11
N : Type u_12
N' : Type u_13
inst_13 : TopologicalSpace M
inst_14 : ChartedSpace H M
inst_15 : TopologicalSpace M'
inst_16 : ChartedSpace H' M'
inst_17 : TopologicalSpace N
inst_18 : ChartedSpace G N
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
n : ℕ∞ω
f : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
inst_21 : IsManifold I n M
inst_22 : IsManifold I' n M'
inst_23 : IsManifold J n N
inst_24 : IsManifold J' n N'
Q : (M' → N') → OpenPartialHomeomorph M' H' → OpenPartialHomeomorph N' G' → Prop
R : (M × M' → N × N') → OpenPartialHomeomorph (M × M') (H × H') → OpenPartialHomeomorph (N × N') (G × G') → Prop
hf : LiftSourceTargetPropertyAt I J n f x P
g : M' → N'
x' : M'
hg : LiftSourceTargetPropertyAt I' J' n g x' Q
h :
  ∀ {f : M → N} {φ₁ : OpenPartialHomeomorph M H} {ψ₁ : OpenPartialHomeomorph N G} {g : M' → N'}
    {φ₂ : OpenPartialHomeomorph M' H'} {ψ₂ : OpenPartialHomeomorph N' G'},
    P f φ₁ ψ₁ → Q g φ₂ ψ₂ → R (Prod.map f g) (φ₁.prod φ₂) (ψ₁.prod ψ₂)
⊢ (hf.domChart (P := P).prod (hg.domChart (P := Q))).source ⊆
    Prod.map f g ⁻¹' (hf.codChart (P := P).prod (hg.codChart (P := Q))).source
have source_subset_preimage_source : hf.domChart (P := P).source ×ˢ hg.domChart (P := Q).source ⊆
  (f ⁻¹' hf.codChart (P := P).source) ×ˢ (g ⁻¹' hg.codChart (P := Q).source)
Tactic: simp only [OpenPartialHomeomorph.prod_toPartialEquiv, PartialEquiv.prod_source,
      preimage_prod_map_prod]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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
inst_6 : IsManifold I 1 M
e : OpenPartialHomeomorph M H
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
x : M
hx : x ∈ e.source
⊢ MDiffAt (↑e : M → H) x
have rw : ContinuousAt (↑e : M → H) x ∧
  DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e : M → H)) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
Tactic: rw [mdifferentiableAt_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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
inst_6 : IsManifold I 1 M
e : OpenPartialHomeomorph M H
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
x : M
hx : x ∈ e.source
⊢ ContinuousAt (↑e : M → H) x ∧
    DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e : M → H)) (range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)
have refine : DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e : M → H)) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
Tactic: refine ⟨(e.continuousOn x hx).continuousAt (e.open_source.mem_nhds hx), ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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
inst_6 : IsManifold I 1 M
e : OpenPartialHomeomorph M H
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
x : M
hx : x ∈ e.source
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e : M → H)) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
have mem : (↑I : H → E) ((↑(chartAt H x) : M → H) x) ∈
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e)).source ∩
    range (↑I : H → E)
Tactic: have mem :
    I ((chartAt H x : M → H) x) ∈ I.symm ⁻¹' ((chartAt H x).symm ≫ₕ e).source ∩ range I := by
    simp only [hx, mfld_simps]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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
inst_6 : IsManifold I 1 M
e : OpenPartialHomeomorph M H
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
x : M
hx : x ∈ e.source
mem :
  (↑I : H → E) ((↑(chartAt H x) : M → H) x) ∈
    (↑I.symm : E → H) ⁻¹'
        (OpenPartialHomeomorph.toPartialEquiv (OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e)).source ∩
      range (↑I : H → E)
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e : M → H)) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
have this : OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e ∈ contDiffGroupoid 1 I
Tactic: have : (chartAt H x).symm.trans e ∈ contDiffGroupoid 1 I :=
    HasGroupoid.compatible (chart_mem_atlas H x) h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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
inst_6 : IsManifold I 1 M
e : OpenPartialHomeomorph M H
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
x : M
hx : x ∈ e.source
mem :
  (↑I : H → E) ((↑(chartAt H x) : M → H) x) ∈
    (↑I.symm : E → H) ⁻¹'
        (OpenPartialHomeomorph.toPartialEquiv (OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e)).source ∩
      range (↑I : H → E)
this : OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e ∈ contDiffGroupoid 1 I
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e : M → H)) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
have A : ContDiffOn 𝕜 1 ((↑I : H → E) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e) : H → H) ∘ (↑I.symm : E → H))
  ((↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e)).source ∩
    range (↑I : H → E))
Tactic: have A :
    ContDiffOn 𝕜 1 (I ∘ (chartAt H x).symm.trans e ∘ I.symm)
      (I.symm ⁻¹' ((chartAt H x).symm.trans e).source ∩ range I) :=
    this.1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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
inst_6 : IsManifold I 1 M
e : OpenPartialHomeomorph M H
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
x : M
hx : x ∈ e.source
mem :
  (↑I : H → E) ((↑(chartAt H x) : M → H) x) ∈
    (↑I.symm : E → H) ⁻¹'
        (OpenPartialHomeomorph.toPartialEquiv (OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e)).source ∩
      range (↑I : H → E)
this : OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e ∈ contDiffGroupoid 1 I
A :
  ContDiffOn 𝕜 1 ((↑I : H → E) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e) : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹'
        (OpenPartialHomeomorph.toPartialEquiv (OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e)).source ∩
      range (↑I : H → E))
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e : M → H)) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
have B : DifferentiableWithinAt 𝕜 ((↑I : H → E) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e) : H → H) ∘ (↑I.symm : E → H))
  ((↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e)).source ∩
    range (↑I : H → E))
  ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
Tactic: have B := A.differentiableOn one_ne_zero (I ((chartAt H x : M → H) x)) mem
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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
inst_6 : IsManifold I 1 M
e : OpenPartialHomeomorph M H
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
x : M
hx : x ∈ e.source
mem :
  (↑I : H → E) ((↑(chartAt H x) : M → H) x) ∈
    (↑I.symm : E → H) ⁻¹'
        (OpenPartialHomeomorph.toPartialEquiv (OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e)).source ∩
      range (↑I : H → E)
this : OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e ∈ contDiffGroupoid 1 I
A :
  ContDiffOn 𝕜 1 ((↑I : H → E) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e) : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹'
        (OpenPartialHomeomorph.toPartialEquiv (OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e)).source ∩
      range (↑I : H → E))
B :
  DifferentiableWithinAt 𝕜
    ((↑I : H → E) ∘ ((↑e : M → H) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
        (↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' e.source ∩
      range (↑I : H → E))
    ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e : M → H)) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
have rw : ∀
  (B :
    DifferentiableWithinAt 𝕜
      ((↑I : H → E) ∘ ((↑e : M → H) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) ∘ (↑I.symm : E → H))
      (range (↑I : H → E)) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))),
  DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e : M → H)) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
Tactic: rw [inter_comm, differentiableWithinAt_inter] at B
Cleared hypotheses: B
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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
inst_6 : IsManifold I 1 M
e : OpenPartialHomeomorph M H
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
x : M
hx : x ∈ e.source
mem :
  (↑I : H → E) ((↑(chartAt H x) : M → H) x) ∈
    (↑I.symm : E → H) ⁻¹'
        (OpenPartialHomeomorph.toPartialEquiv (OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e)).source ∩
      range (↑I : H → E)
this : OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e ∈ contDiffGroupoid 1 I
A :
  ContDiffOn 𝕜 1 ((↑I : H → E) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e) : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹'
        (OpenPartialHomeomorph.toPartialEquiv (OpenPartialHomeomorph.symm (chartAt H x) ≫ₕ e)).source ∩
      range (↑I : H → E))
B :
  DifferentiableWithinAt 𝕜
    ((↑I : H → E) ∘ ((↑e : M → H) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
        (↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' e.source ∩
      range (↑I : H → E))
    ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
rw :
  ∀
    (B :
      DifferentiableWithinAt 𝕜
        ((↑I : H → E) ∘ ((↑e : M → H) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) ∘ (↑I.symm : E → H))
        (range (↑I : H → E)) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))),
    DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e : M → H)) (range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e : M → H)) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
have rw₁ : ∀
  (B :
    DifferentiableWithinAt 𝕜
      ((↑I : H → E) ∘ ((↑e : M → H) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) ∘ (↑I.symm : E → H))
      (range (↑I : H → E) ∩
        ((↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
          (↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' e.source))
      ((↑I : H → E) ((↑(chartAt H x) : M → H) x))),
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
      (↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' e.source ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
Tactic: rw [inter_comm, differentiableWithinAt_inter] at B
Cleared hypotheses: B
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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
inst_6 : IsManifold I 1 M
e : OpenPartialHomeomorph M H
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
x : H
hx : x ∈ e.target
⊢ MDiffAt (↑e.symm : H → M) x
have rw : ContinuousAt (↑e.symm : H → M) x ∧
  DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e.symm : H → M)) (range (↑I : H → E))
    ((↑(extChartAt I x) : H → E) x)
Tactic: rw [mdifferentiableAt_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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
inst_6 : IsManifold I 1 M
e : OpenPartialHomeomorph M H
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
x : H
hx : x ∈ e.target
⊢ ContinuousAt (↑e.symm : H → M) x ∧
    DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e.symm : H → M)) (range (↑I : H → E))
      ((↑(extChartAt I x) : H → E) x)
have refine : DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e.symm : H → M)) (range (↑I : H → E))
  ((↑(extChartAt I x) : H → E) x)
Tactic: refine ⟨(e.continuousOn_symm x hx).continuousAt (e.open_target.mem_nhds hx), ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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
inst_6 : IsManifold I 1 M
e : OpenPartialHomeomorph M H
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
x : H
hx : x ∈ e.target
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e.symm : H → M)) (range (↑I : H → E))
    ((↑(extChartAt I x) : H → E) x)
have mem : (↑I : H → E) x ∈
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (e.symm ≫ₕ chartAt H ((↑e.symm : H → M) x))).source ∩
    range (↑I : H → E)
Tactic: have mem : I x ∈ I.symm ⁻¹' (e.symm ≫ₕ chartAt H (e.symm x)).source ∩ range I := by
    simp only [hx, mfld_simps]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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
inst_6 : IsManifold I 1 M
e : OpenPartialHomeomorph M H
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
x : H
hx : x ∈ e.target
mem :
  (↑I : H → E) x ∈
    (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (e.symm ≫ₕ chartAt H ((↑e.symm : H → M) x))).source ∩
      range (↑I : H → E)
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e.symm : H → M)) (range (↑I : H → E))
    ((↑(extChartAt I x) : H → E) x)
have this : e.symm ≫ₕ chartAt H ((↑e.symm : H → M) x) ∈ contDiffGroupoid 1 I
Tactic: have : e.symm.trans (chartAt H (e.symm x)) ∈ contDiffGroupoid 1 I :=
    HasGroupoid.compatible h (chart_mem_atlas H _)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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
inst_6 : IsManifold I 1 M
e : OpenPartialHomeomorph M H
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
x : H
hx : x ∈ e.target
mem :
  (↑I : H → E) x ∈
    (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (e.symm ≫ₕ chartAt H ((↑e.symm : H → M) x))).source ∩
      range (↑I : H → E)
this : e.symm ≫ₕ chartAt H ((↑e.symm : H → M) x) ∈ contDiffGroupoid 1 I
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e.symm : H → M)) (range (↑I : H → E))
    ((↑(extChartAt I x) : H → E) x)
have A : ContDiffOn 𝕜 1 ((↑I : H → E) ∘ (↑(e.symm ≫ₕ chartAt H ((↑e.symm : H → M) x)) : H → H) ∘ (↑I.symm : E → H))
  ((↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (e.symm ≫ₕ chartAt H ((↑e.symm : H → M) x))).source ∩
    range (↑I : H → E))
Tactic: have A :
    ContDiffOn 𝕜 1 (I ∘ e.symm.trans (chartAt H (e.symm x)) ∘ I.symm)
      (I.symm ⁻¹' (e.symm.trans (chartAt H (e.symm x))).source ∩ range I) :=
    this.1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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
inst_6 : IsManifold I 1 M
e : OpenPartialHomeomorph M H
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
x : H
hx : x ∈ e.target
mem :
  (↑I : H → E) x ∈
    (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (e.symm ≫ₕ chartAt H ((↑e.symm : H → M) x))).source ∩
      range (↑I : H → E)
this : e.symm ≫ₕ chartAt H ((↑e.symm : H → M) x) ∈ contDiffGroupoid 1 I
A :
  ContDiffOn 𝕜 1 ((↑I : H → E) ∘ (↑(e.symm ≫ₕ chartAt H ((↑e.symm : H → M) x)) : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (e.symm ≫ₕ chartAt H ((↑e.symm : H → M) x))).source ∩
      range (↑I : H → E))
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e.symm : H → M)) (range (↑I : H → E))
    ((↑(extChartAt I x) : H → E) x)
have B : DifferentiableWithinAt 𝕜 ((↑I : H → E) ∘ (↑(e.symm ≫ₕ chartAt H ((↑e.symm : H → M) x)) : H → H) ∘ (↑I.symm : E → H))
  ((↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (e.symm ≫ₕ chartAt H ((↑e.symm : H → M) x))).source ∩
    range (↑I : H → E))
  ((↑I : H → E) x)
Tactic: have B := A.differentiableOn one_ne_zero (I x) mem
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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
inst_6 : IsManifold I 1 M
e : OpenPartialHomeomorph M H
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
x : H
hx : x ∈ e.target
mem :
  (↑I : H → E) x ∈
    (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (e.symm ≫ₕ chartAt H ((↑e.symm : H → M) x))).source ∩
      range (↑I : H → E)
this : e.symm ≫ₕ chartAt H ((↑e.symm : H → M) x) ∈ contDiffGroupoid 1 I
A :
  ContDiffOn 𝕜 1 ((↑I : H → E) ∘ (↑(e.symm ≫ₕ chartAt H ((↑e.symm : H → M) x)) : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (e.symm ≫ₕ chartAt H ((↑e.symm : H → M) x))).source ∩
      range (↑I : H → E))
B :
  DifferentiableWithinAt 𝕜
    ((↑I : H → E) ∘ ((↑(chartAt H ((↑e.symm : H → M) x)) : M → H) ∘ (↑e.symm : H → M)) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' e.target ∩
        (↑I.symm : E → H) ⁻¹'
          (↑e.symm : H → M) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑e.symm : H → M) x))).source ∩
      range (↑I : H → E))
    ((↑I : H → E) x)
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e.symm : H → M)) (range (↑I : H → E))
    ((↑(extChartAt I x) : H → E) x)
have rw : ∀
  (B :
    DifferentiableWithinAt 𝕜
      ((↑I : H → E) ∘ ((↑(chartAt H ((↑e.symm : H → M) x)) : M → H) ∘ (↑e.symm : H → M)) ∘ (↑I.symm : E → H))
      (range (↑I : H → E)) ((↑I : H → E) x)),
  DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e.symm : H → M)) (range (↑I : H → E))
    ((↑(extChartAt I x) : H → E) x)
Tactic: rw [inter_comm, differentiableWithinAt_inter] at B
Cleared hypotheses: B
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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
inst_6 : IsManifold I 1 M
e : OpenPartialHomeomorph M H
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
x : H
hx : x ∈ e.target
mem :
  (↑I : H → E) x ∈
    (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (e.symm ≫ₕ chartAt H ((↑e.symm : H → M) x))).source ∩
      range (↑I : H → E)
this : e.symm ≫ₕ chartAt H ((↑e.symm : H → M) x) ∈ contDiffGroupoid 1 I
A :
  ContDiffOn 𝕜 1 ((↑I : H → E) ∘ (↑(e.symm ≫ₕ chartAt H ((↑e.symm : H → M) x)) : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (e.symm ≫ₕ chartAt H ((↑e.symm : H → M) x))).source ∩
      range (↑I : H → E))
B :
  DifferentiableWithinAt 𝕜
    ((↑I : H → E) ∘ ((↑(chartAt H ((↑e.symm : H → M) x)) : M → H) ∘ (↑e.symm : H → M)) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' e.target ∩
        (↑I.symm : E → H) ⁻¹'
          (↑e.symm : H → M) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑e.symm : H → M) x))).source ∩
      range (↑I : H → E))
    ((↑I : H → E) x)
rw :
  ∀
    (B :
      DifferentiableWithinAt 𝕜
        ((↑I : H → E) ∘ ((↑(chartAt H ((↑e.symm : H → M) x)) : M → H) ∘ (↑e.symm : H → M)) ∘ (↑I.symm : E → H))
        (range (↑I : H → E)) ((↑I : H → E) x)),
    DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e.symm : H → M)) (range (↑I : H → E))
      ((↑(extChartAt I x) : H → E) x)
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x (↑e.symm : H → M)) (range (↑I : H → E))
    ((↑(extChartAt I x) : H → E) x)
have rw₁ : ∀
  (B :
    DifferentiableWithinAt 𝕜
      ((↑I : H → E) ∘ ((↑(chartAt H ((↑e.symm : H → M) x)) : M → H) ∘ (↑e.symm : H → M)) ∘ (↑I.symm : E → H))
      (range (↑I : H → E) ∩
        ((↑I.symm : E → H) ⁻¹' e.target ∩
          (↑I.symm : E → H) ⁻¹'
            (↑e.symm : H → M) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑e.symm : H → M) x))).source))
      ((↑I : H → E) x)),
  (↑I.symm : E → H) ⁻¹' e.target ∩
      (↑I.symm : E → H) ⁻¹'
        (↑e.symm : H → M) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑e.symm : H → M) x))).source ∈
    𝓝 ((↑I : H → E) x)
Tactic: rw [inter_comm, differentiableWithinAt_inter] at B
Cleared hypotheses: B