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 : 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,
    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 : ∀ (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),
  ∃ 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: obtain ⟨e, he, h2e, hef, hex⟩ :
      ∃ e : OpenPartialHomeomorph H H,
        e ∈ contDiffGroupoid n I ∧
          e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source ∧
            EqOn (c' ∘ f ∘ c.symm) e e.source ∧ c x ∈ e.source := by
      have h1 : c' = chartAt H (f x) := by simp only [x, c', f.right_inv hX]
      have h2 : c' ∘ f ∘ c.symm = ⇑(c.symm ≫ₕ f ≫ₕ c') := rfl
      have hcx : c x ∈ c.symm ⁻¹' f.source := by simp only [c, hx, mfld_simps]
      rw [h2]
      rw [← h1, h2, OpenPartialHomeomorph.isLocalStructomorphWithinAt_iff'] at hxf
      · exact hxf hcx
      · dsimp [x, c]; mfld_set_tac
      · apply Or.inl
        simp only [c, hx, h1, 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
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
⊢ (↑c' : M' → H) X = (↑e : H → H) ((↑c : M → H) ((↑f.symm : M' → M) X))
have rw : (↑c' : M' → H) X = ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) ((↑c : M → H) x)
Tactic: rw [← hef hex]
-- 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
⊢ (↑c' : M' → H) X = (↑c' : M' → H) ((↑f : M → M') ((↑c.symm : H → M) ((↑c : M → H) x)))
have hfX : (↑f.symm : M' → M) X ∈ c.source
Tactic: have hfX : f.symm X ∈ c.source := by simp only [c, x, 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
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
hfX : (↑f.symm : M' → M) X ∈ c.source
⊢ (↑c' : M' → H) X = (↑c' : M' → H) ((↑f : M → M') ((↑c.symm : H → M) ((↑c : M → H) x)))
have rw : (↑c' : M' → H) X = (↑c' : M' → H) ((↑f : M → M') ((↑f.symm : M' → M) X))
Tactic: rw [c.left_inv hfX, f.right_inv 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)
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
hfX : (↑f.symm : M' → M) X ∈ c.source
rw : (↑c' : M' → H) X = (↑c' : M' → H) ((↑f : M → M') ((↑f.symm : M' → M) X))
⊢ (↑c' : M' → H) X = (↑c' : M' → H) ((↑f : M → M') ((↑c.symm : H → M) ((↑c : M → H) x)))
have rw₁ : (↑c' : M' → H) X = (↑c' : M' → H) X
Tactic: rw [c.left_inv hfX, 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
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
⊢ ∃ 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 h2X : (↑c' : M' → H) X = (↑e : H → H) ((↑c : M → H) ((↑f.symm : M' → M) X))
Tactic: have h2X : c' X = e (c (f.symm X)) := by
      rw [← hef hex]
      dsimp only [Function.comp_def]
      have hfX : f.symm X ∈ c.source := by simp only [c, x, mfld_simps]
      rw [c.left_inv hfX, f.right_inv 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)
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))
⊢ EqOn (↑(c.symm ≫ₕ f ≫ₕ c').symm : H → H) (↑e.symm : H → H) (e.target ∩ e.target)
have h₁ : EqOn (↑e.symm : H → H) (↑(c.symm ≫ₕ f ≫ₕ c').symm : H → H) (e.target ∩ e.target)
Tactic: apply EqOn.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 : 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))
⊢ EqOn (↑e.symm : H → H) (↑(c.symm ≫ₕ f ≫ₕ c').symm : H → H) (e.target ∩ e.target)
have h₁ : e.source ∩ e.source = (c.symm ≫ₕ f ≫ₕ c').source ∩ e.source
Tactic: refine e.isImage_source_target.symm_eqOn_of_inter_eq_of_eqOn ?_ ?_
-- 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))
h₁ : e.source ∩ e.source = (c.symm ≫ₕ f ≫ₕ c').source ∩ e.source
⊢ EqOn (↑e.symm : H → H) (↑(c.symm ≫ₕ f ≫ₕ c').symm : H → H) (e.target ∩ e.target)
have h₂ : EqOn (↑e : H → H) (↑(c.symm ≫ₕ f ≫ₕ c') : H → H) (e.source ∩ e.source)
Tactic: refine e.isImage_source_target.symm_eqOn_of_inter_eq_of_eqOn ?_ ?_
-- 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))
⊢ e.source ∩ e.source = (c.symm ≫ₕ f ≫ₕ c').source ∩ e.source
have h₁ : e.source = (c.symm ≫ₕ f ≫ₕ c').source ∩ e.source
Tactic: rw [inter_self, inter_eq_right.mpr h2e]
-- 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))
h₁ : e.source = (c.symm ≫ₕ f ≫ₕ c').source ∩ e.source
⊢ e.source ∩ e.source = (c.symm ≫ₕ f ≫ₕ c').source ∩ e.source
have h₂ : e.source = e.source
Tactic: rw [inter_self, inter_eq_right.mpr h2e]
-- 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))
⊢ EqOn (↑e : H → H) (↑(c.symm ≫ₕ f ≫ₕ c') : H → H) (e.source ∩ e.source)
have h₁ : EqOn (↑e : H → H) (↑(c.symm ≫ₕ f ≫ₕ c') : H → H) e.source
Tactic: rw [inter_self]
-- 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))
⊢ 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 ∩ e.target)
Tactic: 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