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'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') 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)
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
he' : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) ((↑c.symm : H → M) ⁻¹' f.source ∩ e.source)
hex : (↑c : M → H) x ∈ e.source
s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source
h : x ∈ s
⊢ ∃ (u : Set M), IsOpen u ∧ x ∈ u ∧ ContMDiffOn I I n (↑f : M → M') (f.source ∩ u)
have h₁ : ContMDiffOn I I n (↑f : M → M') (f.source ∩ s)
Tactic: refine ⟨s, (f.trans c').open_source.inter ((c.trans e).trans c'.symm).open_source, ?_, ?_⟩
-- 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'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') 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)
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
he' : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) ((↑c.symm : H → M) ⁻¹' f.source ∩ e.source)
hex : (↑c : M → H) x ∈ e.source
s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source
⊢ x ∈ s
have h : (x ∈ f.source ∧ (↑f : M → M') x ∈ c'.source) ∧
  (x ∈ c.source ∧ (↑c : M → H) x ∈ e.source) ∧ (↑e : H → H) ((↑c : M → H) x) ∈ c'.target
Tactic: simp only [s, 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'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') 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)
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
he' : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) ((↑c.symm : H → M) ⁻¹' f.source ∩ e.source)
hex : (↑c : M → H) x ∈ e.source
s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source
⊢ (x ∈ f.source ∧ (↑f : M → M') x ∈ c'.source) ∧
    (x ∈ c.source ∧ (↑c : M → H) x ∈ e.source) ∧ (↑e : H → H) ((↑c : M → H) x) ∈ c'.target
have h : (x ∈ f.source ∧ (↑f : M → M') x ∈ c'.source) ∧
  (x ∈ c.source ∧ (↑c : M → H) x ∈ e.source) ∧
    ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) ((↑c : M → H) x) ∈ c'.target
Tactic: rw [← he']
-- 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'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') 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)
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
he' : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) ((↑c.symm : H → M) ⁻¹' f.source ∩ e.source)
hex : (↑c : M → H) x ∈ e.source
s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source
h :
  (x ∈ f.source ∧ (↑f : M → M') x ∈ c'.source) ∧
    (x ∈ c.source ∧ (↑c : M → H) x ∈ e.source) ∧
      ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) ((↑c : M → H) x) ∈ c'.target
⊢ (x ∈ f.source ∧ (↑f : M → M') x ∈ c'.source) ∧
    (x ∈ c.source ∧ (↑c : M → H) x ∈ e.source) ∧ (↑e : H → H) ((↑c : M → H) x) ∈ c'.target
have h₁ : (↑c : M → H) x ∈ (↑c.symm : H → M) ⁻¹' f.source ∩ e.source
Tactic: rw [← he']
-- 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'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') 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)
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
he' : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) ((↑c.symm : H → M) ⁻¹' f.source ∩ e.source)
hex : (↑c : M → H) x ∈ e.source
s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source
⊢ ContMDiffOn I I n ((↑c'.symm : H → M') ∘ (↑e : H → H) ∘ (↑c : M → H)) s
have hc' : ContMDiffOn I I n (↑c'.symm : H → M') (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f : M → M') x))).target
Tactic: have hc' : ContMDiffOn I I n c'.symm _ := contMDiffOn_chart_symm
-- 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'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') 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)
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
he' : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) ((↑c.symm : H → M) ⁻¹' f.source ∩ e.source)
hex : (↑c : M → H) x ∈ e.source
s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source
hc' : ContMDiffOn I I n (↑c'.symm : H → M') (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f : M → M') x))).target
⊢ ContMDiffOn I I n ((↑c'.symm : H → M') ∘ (↑e : H → H) ∘ (↑c : M → H)) s
have he'' : ContMDiffOn I I n (↑e : H → H) e.source
Tactic: have he'' : ContMDiffOn I I n e _ := contMDiffOn_of_mem_contDiffGroupoid he
-- 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'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') 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)
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
he' : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) ((↑c.symm : H → M) ⁻¹' f.source ∩ e.source)
hex : (↑c : M → H) x ∈ e.source
s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source
hc' : ContMDiffOn I I n (↑c'.symm : H → M') (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f : M → M') x))).target
he'' : ContMDiffOn I I n (↑e : H → H) e.source
⊢ ContMDiffOn I I n ((↑c'.symm : H → M') ∘ (↑e : H → H) ∘ (↑c : M → H)) s
have hc : ContMDiffOn I I n (↑c : M → H) (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
Tactic: have hc : ContMDiffOn I I n c _ := contMDiffOn_chart
-- 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'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') 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)
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
he' : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) ((↑c.symm : H → M) ⁻¹' f.source ∩ e.source)
hex : (↑c : M → H) x ∈ e.source
s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source
hc' : ContMDiffOn I I n (↑c'.symm : H → M') (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f : M → M') x))).target
he'' : ContMDiffOn I I n (↑e : H → H) e.source
hc : ContMDiffOn I I n (↑c : M → H) (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
⊢ ContMDiffOn I I n ((↑c'.symm : H → M') ∘ (↑e : H → H) ∘ (↑c : M → H)) s
have refine : s ⊆
  (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∩ (↑c : M → H) ⁻¹' e.source ∩
    (↑e : H → H) ∘ (↑c : M → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f : M → M') x))).target
Tactic: refine (hc'.comp' (he''.comp' hc)).mono ?_
-- 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'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') 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)
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
he' : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) ((↑c.symm : H → M) ⁻¹' f.source ∩ e.source)
hex : (↑c : M → H) x ∈ e.source
s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source
hc' : ContMDiffOn I I n (↑c'.symm : H → M') (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f : M → M') x))).target
he'' : ContMDiffOn I I n (↑e : H → H) e.source
hc : ContMDiffOn I I n (↑c : M → H) (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
⊢ s ⊆
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∩ (↑c : M → H) ⁻¹' e.source ∩
      (↑e : H → H) ∘ (↑c : M → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f : M → M') x))).target
have dsimp : f.source ∩ (↑f : M → M') ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f : M → M') x))).source ∩
    ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' e.source ∩
      (↑e : H → H) ∘ (↑(chartAt H x) : M → H) ⁻¹'
        (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f : M → M') x))).target) ⊆
  (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' e.source ∩
    (↑e : H → H) ∘ (↑(chartAt H x) : M → H) ⁻¹'
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f : M → M') x))).target
Tactic: dsimp [s, c, 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'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') 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)
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
he' : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) ((↑c.symm : H → M) ⁻¹' f.source ∩ e.source)
hex : (↑c : M → H) x ∈ e.source
s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source
hc' : ContMDiffOn I I n (↑c'.symm : H → M') (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f : M → M') x))).target
he'' : ContMDiffOn I I n (↑e : H → H) e.source
hc : ContMDiffOn I I n (↑c : M → H) (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
⊢ f.source ∩ (↑f : M → M') ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f : M → M') x))).source ∩
      ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' e.source ∩
        (↑e : H → H) ∘ (↑(chartAt H x) : M → H) ⁻¹'
          (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f : M → M') x))).target) ⊆
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' e.source ∩
      (↑e : H → H) ∘ (↑(chartAt H x) : M → H) ⁻¹'
        (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f : M → M') x))).target
have mfld_set_tac : ∀ ⦃my_y : M⦄,
  my_y ∈
      f.source ∩ (↑f : M → M') ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f : M → M') x))).source ∩
        ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' e.source ∩
          (↑e : H → H) ∘ (↑(chartAt H x) : M → H) ⁻¹'
            (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f : M → M') x))).target) →
    my_y ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' e.source ∩
        (↑e : H → H) ∘ (↑(chartAt H x) : M → H) ⁻¹'
          (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f : M → M') x))).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'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') 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)
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
he' : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) ((↑c.symm : H → M) ⁻¹' f.source ∩ e.source)
hex : (↑c : M → H) x ∈ e.source
s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source
⊢ ContMDiffOn I I n (↑f : M → M') (f.source ∩ s)
have H₁ : ContMDiffOn I I n ((↑c'.symm : H → M') ∘ (↑e : H → H) ∘ (↑c : M → H)) s
Tactic: have H₁ : ContMDiffOn I I n (c'.symm ∘ e ∘ c) s := by
    have hc' : ContMDiffOn I I n c'.symm _ := contMDiffOn_chart_symm
    have he'' : ContMDiffOn I I n e _ := contMDiffOn_of_mem_contDiffGroupoid he
    have hc : ContMDiffOn I I n c _ := contMDiffOn_chart
    refine (hc'.comp' (he''.comp' hc)).mono ?_
    dsimp [s, c, c']
    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'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') 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)
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
he' : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) ((↑c.symm : H → M) ⁻¹' f.source ∩ e.source)
hex : (↑c : M → H) x ∈ e.source
s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source
H₁ : ContMDiffOn I I n ((↑c'.symm : H → M') ∘ (↑e : H → H) ∘ (↑c : M → H)) s
y : M
hy : y ∈ s
⊢ (↑f : M → M') y = ((↑c'.symm : H → M') ∘ (↑e : H → H) ∘ (↑c : M → H)) y
have hy₁ : (y ∈ f.source ∧ (↑f : M → M') y ∈ c'.source) ∧
  (y ∈ c.source ∧ (↑c : M → H) y ∈ e.source) ∧ (↑e : H → H) ((↑c : M → H) y) ∈ c'.target
Tactic: simp only [s, mfld_simps] at hy
Cleared hypotheses: hy
-- 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'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') 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)
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
he' : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) ((↑c.symm : H → M) ⁻¹' f.source ∩ e.source)
hex : (↑c : M → H) x ∈ e.source
s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source
H₁ : ContMDiffOn I I n ((↑c'.symm : H → M') ∘ (↑e : H → H) ∘ (↑c : M → H)) s
y : M
hy :
  (y ∈ f.source ∧ (↑f : M → M') y ∈ c'.source) ∧
    (y ∈ c.source ∧ (↑c : M → H) y ∈ e.source) ∧ (↑e : H → H) ((↑c : M → H) y) ∈ c'.target
⊢ (↑f : M → M') y = ((↑c'.symm : H → M') ∘ (↑e : H → H) ∘ (↑c : M → H)) y
have hy₁ : (↑f : M → M') y ∈ c'.source
Tactic: have hy₁ : f y ∈ c'.source := by simp only [hy, mfld_simps]