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
X : M'
hX : X ∈ f.symm.source
x_1 : M := (↑f.symm : M' → M) X
hx_1 : x_1 ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x_1
c' : OpenPartialHomeomorph M' H := chartAt H X
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt
    ((↑(chartAt H ((↑f : M → M') x_1)) : M' → H) ∘
      (↑f : M → M') ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x_1)) : H → M))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x_1)) : H → M) ⁻¹' f.source) ((↑(chartAt H x_1) : M → H) x_1)
h2x : (↑(chartAt H X) : M' → H) X ∈ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
h2e : e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source
hef : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) e.source
hex : (↑c : M → H) x_1 ∈ e.source
h2X : (↑c' : M' → H) X = (↑e : H → H) ((↑c : M → H) ((↑f.symm : M' → M) X))
h1 : EqOn (↑(c.symm ≫ₕ f ≫ₕ c').symm : H → H) (↑e.symm : H → H) (e.target ∩ e.target)
x : H
hx : x ∈ e.target
⊢ x ∈ (c.symm ≫ₕ f ≫ₕ c').target
have rw : ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) ((↑e.symm : H → H) x) ∈ (c.symm ≫ₕ f ≫ₕ c').target
Tactic: rw [← e.right_inv hx, ← hef (e.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
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 : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
h2e : e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source
hef : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) e.source
hex : (↑c : M → H) x ∈ e.source
h2X : (↑c' : M' → H) X = (↑e : H → H) ((↑c : M → H) ((↑f.symm : M' → M) X))
h1 : EqOn (↑(c.symm ≫ₕ f ≫ₕ c').symm : H → H) (↑e.symm : H → H) (e.target ∩ e.target)
⊢ EqOn ((↑c : M → H) ∘ (↑f.symm : M' → M) ∘ (↑c'.symm : H → M')) (↑e.symm : H → H)
    ((↑c'.symm : H → M') ⁻¹' f.target ∩ e.target)
have h2 : e.target ⊆ (c.symm ≫ₕ f ≫ₕ c').target
Tactic: have h2 : e.target ⊆ (c.symm ≫ₕ f ≫ₕ c').target := by
        intro x hx; rw [← e.right_inv hx, ← hef (e.symm.mapsTo hx)]
        exact OpenPartialHomeomorph.mapsTo _ (h2e <| e.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
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 : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
h2e : e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source
hef : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) e.source
hex : (↑c : M → H) x ∈ e.source
h2X : (↑c' : M' → H) X = (↑e : H → H) ((↑c : M → H) ((↑f.symm : M' → M) X))
h1 : EqOn (↑(c.symm ≫ₕ f ≫ₕ c').symm : H → H) (↑e.symm : H → H) (e.target ∩ e.target)
h2 : e.target ⊆ (c.symm ≫ₕ f ≫ₕ c').target
⊢ EqOn ((↑c : M → H) ∘ (↑f.symm : M' → M) ∘ (↑c'.symm : H → M')) (↑e.symm : H → H)
    ((↑c'.symm : H → M') ⁻¹' f.target ∩ e.target)
have h1₁ : EqOn (↑(c.symm ≫ₕ f ≫ₕ c').symm : H → H) (↑e.symm : H → H) e.target
Tactic: rw [inter_self] at h1
Cleared hypotheses: h1, 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
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
h2e : e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source
hef : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) e.source
hex : (↑c : M → H) x ∈ e.source
h2X : (↑c' : M' → H) X = (↑e : H → H) ((↑c : M → H) ((↑f.symm : M' → M) X))
h1 : EqOn (↑(c.symm ≫ₕ f ≫ₕ c').symm : H → H) (↑e.symm : H → H) e.target
h2 : e.target ⊆ (c.symm ≫ₕ f ≫ₕ c').target
⊢ EqOn ((↑c : M → H) ∘ (↑f.symm : M' → M) ∘ (↑c'.symm : H → M')) (↑e.symm : H → H)
    ((↑c'.symm : H → M') ⁻¹' f.target ∩ e.target)
have rwa : e.target ⊆ (↑c'.symm : H → M') ⁻¹' f.target
Tactic: rwa [inter_eq_right.mpr]
-- 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
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
h2e : e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source
hef : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) e.source
hex : (↑c : M → H) x ∈ e.source
h2X : (↑c' : M' → H) X = (↑e : H → H) ((↑c : M → H) ((↑f.symm : M' → M) X))
h1 : EqOn (↑(c.symm ≫ₕ f ≫ₕ c').symm : H → H) (↑e.symm : H → H) e.target
h2 : e.target ⊆ (c.symm ≫ₕ f ≫ₕ c').target
⊢ e.target ⊆ (↑c'.symm : H → M') ⁻¹' f.target
have refine : (c.symm ≫ₕ f ≫ₕ c').target ⊆ (↑c'.symm : H → M') ⁻¹' f.target
Tactic: refine h2.trans ?_
-- 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
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
h2e : e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source
hef : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) e.source
hex : (↑c : M → H) x ∈ e.source
h2X : (↑c' : M' → H) X = (↑e : H → H) ((↑c : M → H) ((↑f.symm : M' → M) X))
h1 : EqOn (↑(c.symm ≫ₕ f ≫ₕ c').symm : H → H) (↑e.symm : H → H) e.target
h2 : e.target ⊆ (c.symm ≫ₕ f ≫ₕ c').target
⊢ (c.symm ≫ₕ f ≫ₕ c').target ⊆ (↑c'.symm : H → M') ⁻¹' f.target
have mfld_set_tac : ∀ ⦃my_y : H⦄, my_y ∈ (c.symm ≫ₕ f ≫ₕ c').target → my_y ∈ (↑c'.symm : H → M') ⁻¹' f.target
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
    ((↑(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 : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
h2e : e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source
hef : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) e.source
hex : (↑c : M → H) x ∈ e.source
h2X : (↑c' : M' → H) X = (↑e : H → H) ((↑c : M → H) ((↑f.symm : M' → M) X))
h1 : EqOn (↑(c.symm ≫ₕ f ≫ₕ c').symm : H → H) (↑e.symm : H → H) e.target
h2 : e.target ⊆ (c.symm ≫ₕ f ≫ₕ c').target
mfld_set_tac mfld_set_tac₁ mfld_set_tac₂ :
  ∀ ⦃my_y : H⦄, my_y ∈ (c.symm ≫ₕ f ≫ₕ c').target → my_y ∈ (↑c'.symm : H → M') ⁻¹' f.target
⊢ (c.symm ≫ₕ f ≫ₕ c').target ⊆ (↑c'.symm : H → M') ⁻¹' f.target
have mfld_set_tac₃ : ∀ ⦃my_y : H⦄,
  (my_y ∈ c'.target ∧ (↑c'.symm : H → M') my_y ∈ f.target) ∧ (↑f.symm : M' → M) ((↑c'.symm : H → M') my_y) ∈ c.source →
    my_y ∈ (↑c'.symm : H → M') ⁻¹' f.target
Tactic: mfld_set_tac
-- 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 : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
h2e : e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source
hef : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) e.source
hex : (↑c : M → H) x ∈ e.source
h2X : (↑c' : M' → H) X = (↑e : H → H) ((↑c : M → H) ((↑f.symm : M' → M) X))
⊢ ∃ 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
have h3e : EqOn ((↑c : M → H) ∘ (↑f.symm : M' → M) ∘ (↑c'.symm : H → M')) (↑e.symm : H → H)
  ((↑c'.symm : H → M') ⁻¹' f.target ∩ e.target)
Tactic: have h3e : EqOn (c ∘ f.symm ∘ c'.symm) e.symm (c'.symm ⁻¹' f.target ∩ e.target) := by
      have h1 : EqOn (c.symm ≫ₕ f ≫ₕ c').symm e.symm (e.target ∩ e.target) := by
        apply EqOn.symm
        refine e.isImage_source_target.symm_eqOn_of_inter_eq_of_eqOn ?_ ?_
        · rw [inter_self, inter_eq_right.mpr h2e]
        · rw [inter_self]; exact hef.symm
      have h2 : e.target ⊆ (c.symm ≫ₕ f ≫ₕ c').target := by
        intro x hx; rw [← e.right_inv hx, ← hef (e.symm.mapsTo hx)]
        exact OpenPartialHomeomorph.mapsTo _ (h2e <| e.symm.mapsTo hx)
      rw [inter_self] at h1
      rwa [inter_eq_right.mpr]
      refine h2.trans ?_
      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
    ((↑(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 : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
h2e : e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source
hef : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) e.source
hex : (↑c : M → H) x ∈ e.source
h2X : (↑c' : M' → H) X = (↑e : H → H) ((↑c : M → H) ((↑f.symm : M' → M) X))
h3e :
  EqOn ((↑c : M → H) ∘ (↑f.symm : M' → M) ∘ (↑c'.symm : H → M')) (↑e.symm : H → H)
    ((↑c'.symm : H → M') ⁻¹' f.target ∩ e.target)
⊢ ∃ 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
have mp : (↑(chartAt H X) : M' → H) X ∈ e.symm.source
Tactic: refine ⟨e.symm, StructureGroupoid.symm _ he, h3e, ?_⟩
-- 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
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
h2e : e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source
hef : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) e.source
hex : (↑c : M → H) x ∈ e.source
h2X : (↑c' : M' → H) X = (↑e : H → H) ((↑c : M → H) ((↑f.symm : M' → M) X))
h3e :
  EqOn ((↑c : M → H) ∘ (↑f.symm : M' → M) ∘ (↑c'.symm : H → M')) (↑e.symm : H → H)
    ((↑c'.symm : H → M') ⁻¹' f.target ∩ e.target)
⊢ (↑(chartAt H X) : M' → H) X ∈ e.symm.source
have mp : (↑e : H → H) ((↑c : M → H) ((↑f.symm : M' → M) X)) ∈ e.symm.source
Tactic: rw [h2X]
-- 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₁ : ContMDiffOn I I n (↑f : M → M') f.source
h₂ : ContMDiffOn I I n (↑f.symm : M' → M) f.target
x : M
hx : x ∈ f.source
⊢ LiftPropWithinAt (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source x
have mpr : (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: refine ⟨(h₁ x hx).continuousWithinAt, ?_⟩
-- 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₁ : ContMDiffOn I I n (↑f : M → M') f.source
h₂ : ContMDiffOn I I n (↑f.symm : M' → M) f.target
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') x)
hx' : (↑c : M → H) x ∈ (↑c.symm : H → M) ⁻¹' f.source
⊢ ∃ e ∈ contDiffGroupoid n I,
    EqOn
        ((↑(chartAt H ((↑f : M → M') x)) : M' → H) ∘
          (↑f : M → M') ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        (↑e.toPartialEquiv : H → H) ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source ∩ e.source) ∧
      (↑(chartAt H x) : M → H) x ∈ e.source
have mpr : (contDiffPregroupoid n I).property (↑((c.symm ≫ₕ f) ≫ₕ c') : H → H) ((c.symm ≫ₕ f) ≫ₕ c').source
Tactic: refine ⟨(c.symm.trans f).trans c', ⟨?_, ?_⟩, (?_ : EqOn (c' ∘ f ∘ c.symm) _ _), ?_⟩
-- 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₁ : ContMDiffOn I I n (↑f : M → M') f.source
h₂ : ContMDiffOn I I n (↑f.symm : M' → M) f.target
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') x)
hx' : (↑c : M → H) x ∈ (↑c.symm : H → M) ⁻¹' f.source
mpr : (contDiffPregroupoid n I).property (↑((c.symm ≫ₕ f) ≫ₕ c') : H → H) ((c.symm ≫ₕ f) ≫ₕ c').source
⊢ ∃ e ∈ contDiffGroupoid n I,
    EqOn
        ((↑(chartAt H ((↑f : M → M') x)) : M' → H) ∘
          (↑f : M → M') ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        (↑e.toPartialEquiv : H → H) ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source ∩ e.source) ∧
      (↑(chartAt H x) : M → H) x ∈ e.source
have mpr₁ : (contDiffPregroupoid n I).property (↑((c.symm ≫ₕ f) ≫ₕ c').symm : H → H) ((c.symm ≫ₕ f) ≫ₕ c').target
Tactic: refine ⟨(c.symm.trans f).trans c', ⟨?_, ?_⟩, (?_ : EqOn (c' ∘ f ∘ c.symm) _ _), ?_⟩