awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hy₁ : (↑f : M → M') y ∈ c'.source
⊢ (↑f : M → M') y = ((↑c'.symm : H → M') ∘ (↑e : H → H) ∘ (↑c : M → H)) y
have hy₂ : y ∈ c.source
Tactic: have hy₂ : y ∈ c.source := by simp only [hy, mfld_simps]
-- 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
hy₁ : (↑f : M → M') y ∈ c'.source
hy₂ : y ∈ c.source
⊢ (↑f : M → M') y = ((↑c'.symm : H → M') ∘ (↑e : H → H) ∘ (↑c : M → H)) y
have hy₃ : (↑c : M → H) y ∈ (↑c.symm : H → M) ⁻¹' f.source ∩ e.source
Tactic: have hy₃ : c y ∈ c.symm ⁻¹' f.source ∩ e.source := by simp only [hy, 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
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
hy₁ : (↑f : M → M') y ∈ c'.source
hy₂ : y ∈ c.source
hy₃ : (↑c : M → H) y ∈ (↑c.symm : H → M) ⁻¹' f.source ∩ e.source
⊢ (↑f : M → M') y = (↑c'.symm : H → M') ((↑c' : M' → H) ((↑f : M → M') y))
have rw : (↑f : M → M') y = (↑f : M → M') y
Tactic: rw [c'.left_inv hy₁]
-- 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₁ : 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
hy₁ : (↑f : M → M') y ∈ c'.source
hy₂ : y ∈ c.source
hy₃ : (↑c : M → H) y ∈ (↑c.symm : H → M) ⁻¹' f.source ∩ e.source
⊢ (↑c'.symm : H → M') ((↑c' : M' → H) ((↑f : M → M') y)) =
    (↑c'.symm : H → M') ((↑c' : M' → H) ((↑f : M → M') ((↑c.symm : H → M) ((↑c : M → H) y))))
have rw : (↑c'.symm : H → M') ((↑c' : M' → H) ((↑f : M → M') y)) = (↑c'.symm : H → M') ((↑c' : M' → H) ((↑f : M → M') y))
Tactic: rw [c.left_inv hy₂]
-- 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₁ : 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
hy₁ : (↑f : M → M') y ∈ c'.source
hy₂ : y ∈ c.source
hy₃ : (↑c : M → H) y ∈ (↑c.symm : H → M) ⁻¹' f.source ∩ e.source
⊢ (↑c'.symm : H → M') ((↑c' : M' → H) ((↑f : M → M') ((↑c.symm : H → M) ((↑c : M → H) y)))) =
    (↑c'.symm : H → M') ((↑e : H → H) ((↑c : M → H) y))
have rw : (↑c'.symm : H → M') ((↑c' : M' → H) ((↑f : M → M') ((↑c.symm : H → M) ((↑c : M → H) y)))) =
  (↑c'.symm : H → M') (((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) ((↑c : M → H) y))
Tactic: rw [← he' hy₃]
-- 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₁ : 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
hy₁ : (↑f : M → M') y ∈ c'.source
hy₂ : y ∈ c.source
hy₃ : (↑c : M → H) y ∈ (↑c.symm : H → M) ⁻¹' f.source ∩ e.source
⊢ (↑f : M → M') y = ((↑c'.symm : H → M') ∘ (↑e : H → H) ∘ (↑c : M → H)) y
have f₁ : (↑f : M → M') y = (↑c'.symm : H → M') ((↑c' : M' → H) ((↑f : M → M') y))
Tactic: calc
      f y = c'.symm (c' (f y)) := by rw [c'.left_inv hy₁]
      _ = c'.symm (c' (f (c.symm (c y)))) := by rw [c.left_inv hy₂]
      _ = c'.symm (e (c y)) := by rw [← he' hy₃]; rfl
-- 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₁ : 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
hy₁ : (↑f : M → M') y ∈ c'.source
hy₂ : y ∈ c.source
hy₃ : (↑c : M → H) y ∈ (↑c.symm : H → M) ⁻¹' f.source ∩ e.source
f₁ : (↑f : M → M') y = (↑c'.symm : H → M') ((↑c' : M' → H) ((↑f : M → M') y))
⊢ (↑f : M → M') y = ((↑c'.symm : H → M') ∘ (↑e : H → H) ∘ (↑c : M → H)) y
have f₂ : (↑c'.symm : H → M') ((↑c' : M' → H) ((↑f : M → M') y)) =
  (↑c'.symm : H → M') ((↑c' : M' → H) ((↑f : M → M') ((↑c.symm : H → M) ((↑c : M → H) y))))
Tactic: calc
      f y = c'.symm (c' (f y)) := by rw [c'.left_inv hy₁]
      _ = c'.symm (c' (f (c.symm (c y)))) := by rw [c.left_inv hy₂]
      _ = c'.symm (e (c y)) := by rw [← he' hy₃]; rfl
-- 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₁ : 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
hy₁ : (↑f : M → M') y ∈ c'.source
hy₂ : y ∈ c.source
hy₃ : (↑c : M → H) y ∈ (↑c.symm : H → M) ⁻¹' f.source ∩ e.source
f₁ : (↑f : M → M') y = (↑c'.symm : H → M') ((↑c' : M' → H) ((↑f : M → M') y))
f₂ :
  (↑c'.symm : H → M') ((↑c' : M' → H) ((↑f : M → M') y)) =
    (↑c'.symm : H → M') ((↑c' : M' → H) ((↑f : M → M') ((↑c.symm : H → M) ((↑c : M → H) y))))
⊢ (↑f : M → M') y = ((↑c'.symm : H → M') ∘ (↑e : H → H) ∘ (↑c : M → H)) y
have f₃ : (↑c'.symm : H → M') ((↑c' : M' → H) ((↑f : M → M') ((↑c.symm : H → M) ((↑c : M → H) y)))) =
  (↑c'.symm : H → M') ((↑e : H → H) ((↑c : M → H) y))
Tactic: calc
      f y = c'.symm (c' (f y)) := by rw [c'.left_inv hy₁]
      _ = c'.symm (c' (f (c.symm (c y)))) := by rw [c.left_inv hy₂]
      _ = c'.symm (e (c y)) := by rw [← he' hy₃]; 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'
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
⊢ ContMDiffOn I I n (↑f : M → M') (f.source ∩ s)
have H₂ : EqOn (↑f : M → M') ((↑c'.symm : H → M') ∘ (↑e : H → H) ∘ (↑c : M → H)) s
Tactic: have H₂ : EqOn f (c'.symm ∘ e ∘ c) s := by
    intro y hy
    simp only [s, mfld_simps] at hy
    have hy₁ : f y ∈ c'.source := by simp only [hy, mfld_simps]
    have hy₂ : y ∈ c.source := by simp only [hy, mfld_simps]
    have hy₃ : c y ∈ c.symm ⁻¹' f.source ∩ e.source := by simp only [hy, mfld_simps]
    calc
      f y = c'.symm (c' (f y)) := by rw [c'.left_inv hy₁]
      _ = c'.symm (c' (f (c.symm (c y)))) := by rw [c.left_inv hy₂]
      _ = c'.symm (e (c y)) := by rw [← he' hy₃]; rfl
-- 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₁ : ContMDiffOn I I n ((↑c'.symm : H → M') ∘ (↑e : H → H) ∘ (↑c : M → H)) s
H₂ : EqOn (↑f : M → M') ((↑c'.symm : H → M') ∘ (↑e : H → H) ∘ (↑c : M → H)) s
⊢ ContMDiffOn I I n (↑f : M → M') (f.source ∩ s)
have h : f.source ∩ s ⊆ s
Tactic: refine (H₁.congr H₂).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
H₁ : ContMDiffOn I I n ((↑c'.symm : H → M') ∘ (↑e : H → H) ∘ (↑c : M → H)) s
H₂ : EqOn (↑f : M → M') ((↑c'.symm : H → M') ∘ (↑e : H → H) ∘ (↑c : M → H)) s
⊢ f.source ∩ s ⊆ s
have h : ∀ ⦃my_y : M⦄, my_y ∈ f.source ∩ s → my_y ∈ s
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'
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
H₂ : EqOn (↑f : M → M') ((↑c'.symm : H → M') ∘ (↑e : H → H) ∘ (↑c : M → H)) s
h h₁ h₂ : ∀ ⦃my_y : M⦄, my_y ∈ f.source ∩ s → my_y ∈ s
⊢ f.source ∩ s ⊆ s
have h₃ : ∀ ⦃my_y : M⦄, my_y ∈ f.source ∧ my_y ∈ s → my_y ∈ s
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'
⊢ 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 : M → M') f.source →
  ContMDiffOn I I n (↑f : M → M') f.source ∧ ContMDiffOn I I n (↑f.symm : M' → M) f.target
Tactic: constructor
-- 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'
mp :
  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
⊢ 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 mpr : ContMDiffOn I I n (↑f : M → M') f.source ∧ ContMDiffOn I I n (↑f.symm : M' → M) f.target →
  LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
Tactic: constructor