awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
⊢ ContMDiffOn I I n (↑f : M → M') f.source ∧ ContMDiffOn I I n (↑f.symm : M' → M) f.target
have mp : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f.symm : M' → M) f.symm.source
Tactic: refine ⟨isLocalStructomorphOn_contDiffGroupoid_iff_aux h,
      isLocalStructomorphOn_contDiffGroupoid_iff_aux ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
X : M'
hX : X ∈ f.symm.source
x : M := (↑f.symm : M' → M) X
⊢ LiftPropWithinAt (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f.symm : M' → M) f.symm.source X
have hx : x ∈ f.source
Tactic: have hx : x ∈ f.source := f.symm.mapsTo hX
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
X : M'
hX : X ∈ f.symm.source
x : M := (↑f.symm : M' → M) X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H X
⊢ LiftPropWithinAt (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f.symm : M' → M) f.symm.source X
have hxf : (contDiffGroupoid n I).IsLocalStructomorphWithinAt
  ((↑(chartAt H ((↑f : M → M') x)) : M' → H) ∘ (↑f : M → M') ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
  ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source) ((↑(chartAt H x) : M → H) x)
Tactic: obtain ⟨-, hxf⟩ := h x hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
X : M'
hX : X ∈ f.symm.source
x : M := (↑f.symm : M' → M) X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H X
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt
    ((↑(chartAt H ((↑f : M → M') x)) : M' → H) ∘ (↑f : M → M') ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source) ((↑(chartAt H x) : M → H) x)
⊢ LiftPropWithinAt (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f.symm : M' → M) f.symm.source X
have mp : ∀ (h2x : (↑(chartAt H X) : M' → H) X ∈ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source),
  ∃ e ∈ contDiffGroupoid n I,
    EqOn
        ((↑(chartAt H ((↑f.symm : M' → M) X)) : M → H) ∘
          (↑f.symm : M' → M) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M'))
        (↑e.toPartialEquiv : H → H)
        ((↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source ∩ e.source) ∧
      (↑(chartAt H X) : M' → H) X ∈ e.source
Tactic: refine ⟨(f.symm.continuousAt hX).continuousWithinAt, fun h2x => ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
X : M'
hX : X ∈ f.symm.source
x : M := (↑f.symm : M' → M) X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H X
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt
    ((↑(chartAt H ((↑f : M → M') x)) : M' → H) ∘ (↑f : M → M') ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source) ((↑(chartAt H x) : M → H) x)
h2x : (↑(chartAt H X) : M' → H) X ∈ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source
⊢ ∃ e ∈ contDiffGroupoid n I,
    e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source ∧
      EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) e.source ∧ (↑c : M → H) x ∈ e.source
have h1 : c' = chartAt H ((↑f : M → M') x)
Tactic: have h1 : c' = chartAt H (f x) := by simp only [x, c', f.right_inv hX]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
X : M'
hX : X ∈ f.symm.source
x : M := (↑f.symm : M' → M) X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H X
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt
    ((↑(chartAt H ((↑f : M → M') x)) : M' → H) ∘ (↑f : M → M') ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source) ((↑(chartAt H x) : M → H) x)
h2x : (↑(chartAt H X) : M' → H) X ∈ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source
h1 : c' = chartAt H ((↑f : M → M') x)
⊢ ∃ e ∈ contDiffGroupoid n I,
    e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source ∧
      EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) e.source ∧ (↑c : M → H) x ∈ e.source
have h2 : (↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M) = (↑(c.symm ≫ₕ f ≫ₕ c') : H → H)
Tactic: have h2 : c' ∘ f ∘ c.symm = ⇑(c.symm ≫ₕ f ≫ₕ c') := rfl
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
X : M'
hX : X ∈ f.symm.source
x : M := (↑f.symm : M' → M) X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H X
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt
    ((↑(chartAt H ((↑f : M → M') x)) : M' → H) ∘ (↑f : M → M') ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source) ((↑(chartAt H x) : M → H) x)
h2x : (↑(chartAt H X) : M' → H) X ∈ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source
h1 : c' = chartAt H ((↑f : M → M') x)
h2 : (↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M) = (↑(c.symm ≫ₕ f ≫ₕ c') : H → H)
⊢ ∃ e ∈ contDiffGroupoid n I,
    e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source ∧
      EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) e.source ∧ (↑c : M → H) x ∈ e.source
have hcx : (↑c : M → H) x ∈ (↑c.symm : H → M) ⁻¹' f.source
Tactic: have hcx : c x ∈ c.symm ⁻¹' f.source := by simp only [c, hx, mfld_simps]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
X : M'
hX : X ∈ f.symm.source
x : M := (↑f.symm : M' → M) X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H X
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt
    ((↑(chartAt H ((↑f : M → M') x)) : M' → H) ∘ (↑f : M → M') ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source) ((↑(chartAt H x) : M → H) x)
h2x : (↑(chartAt H X) : M' → H) X ∈ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source
h1 : c' = chartAt H ((↑f : M → M') x)
h2 : (↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M) = (↑(c.symm ≫ₕ f ≫ₕ c') : H → H)
hcx : (↑c : M → H) x ∈ (↑c.symm : H → M) ⁻¹' f.source
⊢ ∃ e ∈ contDiffGroupoid n I,
    e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source ∧
      EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) e.source ∧ (↑c : M → H) x ∈ e.source
have rw : ∃ e ∈ contDiffGroupoid n I,
  e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source ∧
    EqOn (↑(c.symm ≫ₕ f ≫ₕ c') : H → H) (↑e : H → H) e.source ∧ (↑c : M → H) x ∈ e.source
Tactic: rw [h2]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
X : M'
hX : X ∈ f.symm.source
x : M := (↑f.symm : M' → M) X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H X
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt
    ((↑(chartAt H ((↑f : M → M') x)) : M' → H) ∘ (↑f : M → M') ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source) ((↑(chartAt H x) : M → H) x)
h2x : (↑(chartAt H X) : M' → H) X ∈ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source
h1 : c' = chartAt H ((↑f : M → M') x)
h2 : (↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M) = (↑(c.symm ≫ₕ f ≫ₕ c') : H → H)
hcx : (↑c : M → H) x ∈ (↑c.symm : H → M) ⁻¹' f.source
⊢ ∃ e ∈ contDiffGroupoid n I,
    e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source ∧
      EqOn (↑(c.symm ≫ₕ f ≫ₕ c') : H → H) (↑e : H → H) e.source ∧ (↑c : M → H) x ∈ e.source
have rw : ∀
  (hxf :
    (↑(chartAt H x) : M → H) x ∈ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source →
      ∃ e ∈ contDiffGroupoid n I,
        e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source ∧
          EqOn (↑(c.symm ≫ₕ f ≫ₕ c') : H → H) (↑e : H → H) e.source ∧ (↑(chartAt H x) : M → H) x ∈ e.source)
  (h2x : (↑(chartAt H X) : M' → H) X ∈ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source)
  (h1 : c' = chartAt H ((↑f : M → M') x))
  (h2 : (↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M) = (↑(c.symm ≫ₕ f ≫ₕ c') : H → H))
  (hcx : (↑c : M → H) x ∈ (↑c.symm : H → M) ⁻¹' f.source),
  ∃ e ∈ contDiffGroupoid n I,
    e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source ∧
      EqOn (↑(c.symm ≫ₕ f ≫ₕ c') : H → H) (↑e : H → H) e.source ∧ (↑c : M → H) x ∈ e.source
Tactic: rw [← h1, h2, OpenPartialHomeomorph.isLocalStructomorphWithinAt_iff'] at hxf
Cleared hypotheses: hxf, h2x, h1, h2, hcx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
X : M'
hX : X ∈ f.symm.source
x : M := (↑f.symm : M' → M) X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H X
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt
    ((↑(chartAt H ((↑f : M → M') x)) : M' → H) ∘ (↑f : M → M') ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source) ((↑(chartAt H x) : M → H) x)
h2x : (↑(chartAt H X) : M' → H) X ∈ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source
h1 : c' = chartAt H ((↑f : M → M') x)
h2 : (↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M) = (↑(c.symm ≫ₕ f ≫ₕ c') : H → H)
hcx : (↑c : M → H) x ∈ (↑c.symm : H → M) ⁻¹' f.source
rw :
  ∀
    (hxf :
      (↑(chartAt H x) : M → H) x ∈ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source →
        ∃ e ∈ contDiffGroupoid n I,
          e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source ∧
            EqOn (↑(c.symm ≫ₕ f ≫ₕ c') : H → H) (↑e : H → H) e.source ∧ (↑(chartAt H x) : M → H) x ∈ e.source)
    (h2x : (↑(chartAt H X) : M' → H) X ∈ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source)
    (h1 : c' = chartAt H ((↑f : M → M') x))
    (h2 : (↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M) = (↑(c.symm ≫ₕ f ≫ₕ c') : H → H))
    (hcx : (↑c : M → H) x ∈ (↑c.symm : H → M) ⁻¹' f.source),
    ∃ e ∈ contDiffGroupoid n I,
      e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source ∧
        EqOn (↑(c.symm ≫ₕ f ≫ₕ c') : H → H) (↑e : H → H) e.source ∧ (↑c : M → H) x ∈ e.source
⊢ ∃ e ∈ contDiffGroupoid n I,
    e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source ∧
      EqOn (↑(c.symm ≫ₕ f ≫ₕ c') : H → H) (↑e : H → H) e.source ∧ (↑c : M → H) x ∈ e.source
have hs : ∀
  (hxf :
    (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑(c.symm ≫ₕ f ≫ₕ c') : H → H)
      ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source) ((↑(chartAt H x) : M → H) x))
  (h2x : (↑(chartAt H X) : M' → H) X ∈ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source)
  (h1 : c' = chartAt H ((↑f : M → M') x))
  (h2 : (↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M) = (↑(c.symm ≫ₕ f ≫ₕ c') : H → H))
  (hcx : (↑c : M → H) x ∈ (↑c.symm : H → M) ⁻¹' f.source),
  (c.symm ≫ₕ f ≫ₕ c').source ⊆ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source
Tactic: rw [← h1, h2, OpenPartialHomeomorph.isLocalStructomorphWithinAt_iff'] at hxf
Cleared hypotheses: hxf, h2x, h1, h2, hcx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
X : M'
hX : X ∈ f.symm.source
x : M := (↑f.symm : M' → M) X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H X
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑(c.symm ≫ₕ f ≫ₕ c') : H → H)
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source) ((↑(chartAt H x) : M → H) x)
h2x : (↑(chartAt H X) : M' → H) X ∈ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source
h1 : c' = chartAt H ((↑f : M → M') x)
h2 : (↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M) = (↑(c.symm ≫ₕ f ≫ₕ c') : H → H)
hcx : (↑c : M → H) x ∈ (↑c.symm : H → M) ⁻¹' f.source
⊢ (c.symm ≫ₕ f ≫ₕ c').source ⊆ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source
have hs : (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f.symm : M' → M) X))).target ∩
    ((↑(OpenPartialHomeomorph.symm (chartAt H ((↑f.symm : M' → M) X))) : H → M) ⁻¹' f.source ∩
      (↑(OpenPartialHomeomorph.symm (chartAt H ((↑f.symm : M' → M) X))) : H → M) ⁻¹' (↑f : M → M') ⁻¹' c'.source) ⊆
  (↑(OpenPartialHomeomorph.symm (chartAt H ((↑f.symm : M' → M) X))) : H → M) ⁻¹' f.source
Tactic: dsimp [x, c]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
X : M'
hX : X ∈ f.symm.source
x : M := (↑f.symm : M' → M) X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H X
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑(c.symm ≫ₕ f ≫ₕ c') : H → H)
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source) ((↑(chartAt H x) : M → H) x)
h2x : (↑(chartAt H X) : M' → H) X ∈ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source
h1 : c' = chartAt H ((↑f : M → M') x)
h2 : (↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M) = (↑(c.symm ≫ₕ f ≫ₕ c') : H → H)
hcx : (↑c : M → H) x ∈ (↑c.symm : H → M) ⁻¹' f.source
⊢ (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f.symm : M' → M) X))).target ∩
      ((↑(OpenPartialHomeomorph.symm (chartAt H ((↑f.symm : M' → M) X))) : H → M) ⁻¹' f.source ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H ((↑f.symm : M' → M) X))) : H → M) ⁻¹' (↑f : M → M') ⁻¹' c'.source) ⊆
    (↑(OpenPartialHomeomorph.symm (chartAt H ((↑f.symm : M' → M) X))) : H → M) ⁻¹' f.source
have hs : ∀ ⦃my_y : H⦄,
  my_y ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f.symm : M' → M) X))).target ∩
        ((↑(OpenPartialHomeomorph.symm (chartAt H ((↑f.symm : M' → M) X))) : H → M) ⁻¹' f.source ∩
          (↑(OpenPartialHomeomorph.symm (chartAt H ((↑f.symm : M' → M) X))) : H → M) ⁻¹' (↑f : M → M') ⁻¹' c'.source) →
    my_y ∈ (↑(OpenPartialHomeomorph.symm (chartAt H ((↑f.symm : M' → M) X))) : H → M) ⁻¹' f.source
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
X : M'
hX : X ∈ f.symm.source
x : M := (↑f.symm : M' → M) X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H X
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑(c.symm ≫ₕ f ≫ₕ c') : H → H)
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source) ((↑(chartAt H x) : M → H) x)
h2x : (↑(chartAt H X) : M' → H) X ∈ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source
h1 : c' = chartAt H ((↑f : M → M') x)
h2 : (↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M) = (↑(c.symm ≫ₕ f ≫ₕ c') : H → H)
hcx : (↑c : M → H) x ∈ (↑c.symm : H → M) ⁻¹' f.source
hs hs₁ hs₂ :
  ∀ ⦃my_y : H⦄,
    my_y ∈
        (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f.symm : M' → M) X))).target ∩
          ((↑(OpenPartialHomeomorph.symm (chartAt H ((↑f.symm : M' → M) X))) : H → M) ⁻¹' f.source ∩
            (↑(OpenPartialHomeomorph.symm (chartAt H ((↑f.symm : M' → M) X))) : H → M) ⁻¹'
              (↑f : M → M') ⁻¹' c'.source) →
      my_y ∈ (↑(OpenPartialHomeomorph.symm (chartAt H ((↑f.symm : M' → M) X))) : H → M) ⁻¹' f.source
⊢ (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f.symm : M' → M) X))).target ∩
      ((↑(OpenPartialHomeomorph.symm (chartAt H ((↑f.symm : M' → M) X))) : H → M) ⁻¹' f.source ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H ((↑f.symm : M' → M) X))) : H → M) ⁻¹' (↑f : M → M') ⁻¹' c'.source) ⊆
    (↑(OpenPartialHomeomorph.symm (chartAt H ((↑f.symm : M' → M) X))) : H → M) ⁻¹' f.source
have hs₃ : ∀ ⦃my_y : H⦄,
  my_y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f.symm : M' → M) X))).target ∧
      (↑(OpenPartialHomeomorph.symm (chartAt H ((↑f.symm : M' → M) X))) : H → M) my_y ∈ f.source ∧
        (↑f : M → M') ((↑(OpenPartialHomeomorph.symm (chartAt H ((↑f.symm : M' → M) X))) : H → M) my_y) ∈
          (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f : M → M') x))).source →
    my_y ∈ (↑(OpenPartialHomeomorph.symm (chartAt H ((↑f.symm : M' → M) X))) : H → M) ⁻¹' f.source
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
X : M'
hX : X ∈ f.symm.source
x : M := (↑f.symm : M' → M) X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H X
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑(c.symm ≫ₕ f ≫ₕ c') : H → H)
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source) ((↑(chartAt H x) : M → H) x)
h2x : (↑(chartAt H X) : M' → H) X ∈ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source
h1 : c' = chartAt H ((↑f : M → M') x)
h2 : (↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M) = (↑(c.symm ≫ₕ f ≫ₕ c') : H → H)
hcx : (↑c : M → H) x ∈ (↑c.symm : H → M) ⁻¹' f.source
⊢ (↑(chartAt H x) : M → H) x ∈
    (c.symm ≫ₕ f ≫ₕ c').source ∪ ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source)ᶜ
have hx₁ : (↑(chartAt H x) : M → H) x ∈ (c.symm ≫ₕ f ≫ₕ c').source
Tactic: apply Or.inl