awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s t : Set M
x : M
h : x ∈ f.source
ht : t ∈ 𝓝[s] x
rwa :
  ∀
    (ht :
      t ∈
        map (↑(f.extend I).symm : E → M)
          (𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) x)),
    (↑(f.extend I).symm : E → M) ⁻¹' t ∈
      𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) x
⊢ (↑(f.extend I).symm : E → M) ⁻¹' t ∈
    𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) x
have rwa₁ : ∀
  (ht :
    (↑(f.extend I).symm : E → M) ⁻¹' t ∈
      𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) x),
  (↑(f.extend I).symm : E → M) ⁻¹' t ∈
    𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) x
Tactic: rwa [← map_extend_symm_nhdsWithin f (I := I) h, mem_map] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
t : Set M
x : M
h : x ∈ f.source
ht : t ∈ 𝓝 x
⊢ (↑(f.extend I).symm : E → M) ⁻¹' t ∈ 𝓝 ((↑(f.extend I) : M → E) x)
have apply : t ∈ 𝓝 ((↑(f.extend I).symm : E → M) ((↑(f.extend I) : M → E) x))
Tactic: apply (continuousAt_extend_symm f h).preimage_mem_nhds
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
t : Set M
x : M
h : x ∈ f.source
ht : t ∈ 𝓝 x
⊢ t ∈ 𝓝 ((↑(f.extend I).symm : E → M) ((↑(f.extend I) : M → E) x))
have rwa : x ∈ (f.extend I).source
Tactic: rwa [(f.extend I).left_inv]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s t : Set M
⊢ (↑(f.extend I).symm : E → M) ⁻¹' (s ∩ t) ∩ range (↑I : H → E) =
    (↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑(f.extend I).symm : E → M) ⁻¹' t
have h : ∀ (x : E),
  x ∈ (↑(f.extend I).symm : E → M) ⁻¹' (s ∩ t) ∩ range (↑I : H → E) ↔
    x ∈ (↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑(f.extend I).symm : E → M) ⁻¹' t
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
x : M
hs : s ⊆ f.source
hx : x ∈ f.source
⊢ (↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) =ᶠ[𝓝 ((↑(f.extend I) : M → E) x)] (↑(f.extend I) : M → E) '' s
have rw : 𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) x =
  𝓝[(↑(f.extend I) : M → E) '' s] (↑(f.extend I) : M → E) x
Tactic: rw [← nhdsWithin_eq_iff_eventuallyEq, ← map_extend_nhdsWithin _ hx,
    map_extend_nhdsWithin_eq_image_of_subset _ hx hs]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
x : M
hs : s ⊆ f.source
hx : x ∈ f.source
rw :
  𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) x =
    𝓝[(↑(f.extend I) : M → E) '' s] (↑(f.extend I) : M → E) x
⊢ (↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) =ᶠ[𝓝 ((↑(f.extend I) : M → E) x)] (↑(f.extend I) : M → E) '' s
have rw₁ : map (↑(f.extend I) : M → E) (𝓝[s] x) = 𝓝[(↑(f.extend I) : M → E) '' s] (↑(f.extend I) : M → E) x
Tactic: rw [← nhdsWithin_eq_iff_eventuallyEq, ← map_extend_nhdsWithin _ hx,
    map_extend_nhdsWithin_eq_image_of_subset _ hx hs]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
x : M
hs : s ⊆ f.source
hx : x ∈ f.source
rw :
  𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) x =
    𝓝[(↑(f.extend I) : M → E) '' s] (↑(f.extend I) : M → E) x
rw₁ : map (↑(f.extend I) : M → E) (𝓝[s] x) = 𝓝[(↑(f.extend I) : M → E) '' s] (↑(f.extend I) : M → E) x
⊢ (↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) =ᶠ[𝓝 ((↑(f.extend I) : M → E) x)] (↑(f.extend I) : M → E) '' s
have rw₂ : 𝓝[(↑(f.extend I) : M → E) '' s] (↑(f.extend I) : M → E) x = 𝓝[(↑(f.extend I) : M → E) '' s] (↑(f.extend I) : M → E) x
Tactic: rw [← nhdsWithin_eq_iff_eventuallyEq, ← map_extend_nhdsWithin _ hx,
    map_extend_nhdsWithin_eq_image_of_subset _ hx hs]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
⊢ PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e') =
    (↑I : H → E) '' (e.symm ≫ₕ e').source
have simp_rw : (↑I.symm : E → H) ⁻¹' e.target ∩ (↑(e.extend I).symm : E → M) ⁻¹' e'.source ∩ range (↑I : H → E) =
  (↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E)
Tactic: simp_rw [extendCoordChange, PartialEquiv.trans_source, I.image_eq, e'.extend_source,
    PartialEquiv.symm_source, e.extend_target, inter_right_comm _ (range I)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f f' : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ (↑(f.extend I) : M → E) '' (f.source ∩ f'.source) =
    PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) f f')
have simp_rw : (↑(f.extend I) : M → E) '' (f.source ∩ f'.source) = (↑I : H → E) '' (f.symm ≫ₕ f').source
Tactic: simp_rw [I.extendCoordChange_source, f.extend_coe, image_comp I f,
    OpenPartialHomeomorph.trans_source'', OpenPartialHomeomorph.symm_symm,
    OpenPartialHomeomorph.symm_target]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f f' : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
simp_rw : (↑(f.extend I) : M → E) '' (f.source ∩ f'.source) = (↑I : H → E) '' (f.symm ≫ₕ f').source
⊢ (↑(f.extend I) : M → E) '' (f.source ∩ f'.source) =
    PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) f f')
have simp_rw₁ : (fun (a : M) ↦ ((↑I : H → E) ∘ (↑f : M → H)) a) '' (f.source ∩ f'.source) = (↑I : H → E) '' (f.symm ≫ₕ f').source
Tactic: simp_rw [I.extendCoordChange_source, f.extend_coe, image_comp I f,
    OpenPartialHomeomorph.trans_source'', OpenPartialHomeomorph.symm_symm,
    OpenPartialHomeomorph.symm_target]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f f' : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
simp_rw : (↑(f.extend I) : M → E) '' (f.source ∩ f'.source) = (↑I : H → E) '' (f.symm ≫ₕ f').source
simp_rw₁ :
  (fun (a : M) ↦ ((↑I : H → E) ∘ (↑f : M → H)) a) '' (f.source ∩ f'.source) = (↑I : H → E) '' (f.symm ≫ₕ f').source
⊢ (↑(f.extend I) : M → E) '' (f.source ∩ f'.source) =
    PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) f f')
have simp_rw₂ : (↑I : H → E) '' (↑f : M → H) '' (f.source ∩ f'.source) = (↑I : H → E) '' (f.symm ≫ₕ f').source
Tactic: simp_rw [I.extendCoordChange_source, f.extend_coe, image_comp I f,
    OpenPartialHomeomorph.trans_source'', OpenPartialHomeomorph.symm_symm,
    OpenPartialHomeomorph.symm_target]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f f' : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
simp_rw : (↑(f.extend I) : M → E) '' (f.source ∩ f'.source) = (↑I : H → E) '' (f.symm ≫ₕ f').source
simp_rw₁ :
  (fun (a : M) ↦ ((↑I : H → E) ∘ (↑f : M → H)) a) '' (f.source ∩ f'.source) = (↑I : H → E) '' (f.symm ≫ₕ f').source
simp_rw₂ : (↑I : H → E) '' (↑f : M → H) '' (f.source ∩ f'.source) = (↑I : H → E) '' (f.symm ≫ₕ f').source
⊢ (↑(f.extend I) : M → E) '' (f.source ∩ f'.source) =
    PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) f f')
have simp_rw₃ : (↑I : H → E) '' (↑f : M → H) '' (f.source ∩ f'.source) =
  (↑I : H → E) '' (↑f.symm.symm : M → H) '' (f.symm.target ∩ f'.source)
Tactic: simp_rw [I.extendCoordChange_source, f.extend_coe, image_comp I f,
    OpenPartialHomeomorph.trans_source'', OpenPartialHomeomorph.symm_symm,
    OpenPartialHomeomorph.symm_target]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f f' : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
simp_rw : (↑(f.extend I) : M → E) '' (f.source ∩ f'.source) = (↑I : H → E) '' (f.symm ≫ₕ f').source
simp_rw₁ :
  (fun (a : M) ↦ ((↑I : H → E) ∘ (↑f : M → H)) a) '' (f.source ∩ f'.source) = (↑I : H → E) '' (f.symm ≫ₕ f').source
simp_rw₂ : (↑I : H → E) '' (↑f : M → H) '' (f.source ∩ f'.source) = (↑I : H → E) '' (f.symm ≫ₕ f').source
simp_rw₃ :
  (↑I : H → E) '' (↑f : M → H) '' (f.source ∩ f'.source) =
    (↑I : H → E) '' (↑f.symm.symm : M → H) '' (f.symm.target ∩ f'.source)
⊢ (↑(f.extend I) : M → E) '' (f.source ∩ f'.source) =
    PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) f f')
have simp_rw₄ : (↑I : H → E) '' (↑f : M → H) '' (f.source ∩ f'.source) =
  (↑I : H → E) '' (fun (a : M) ↦ (↑f : M → H) a) '' (f.symm.target ∩ f'.source)
Tactic: simp_rw [I.extendCoordChange_source, f.extend_coe, image_comp I f,
    OpenPartialHomeomorph.trans_source'', OpenPartialHomeomorph.symm_symm,
    OpenPartialHomeomorph.symm_target]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
x : E
hx : Membership.mem (γ := Set E) (PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e')) x
⊢ PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e') ∈ 𝓝[range (↑I : H → E)] x
have rw : ∀ (hx : x ∈ (↑I : H → E) '' (e.symm ≫ₕ e').source), (↑I : H → E) '' (e.symm ≫ₕ e').source ∈ 𝓝[range (↑I : H → E)] x
Tactic: rw [I.extendCoordChange_source] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
x : E
hx : x ∈ (↑I : H → E) '' (e.symm ≫ₕ e').source
⊢ (↑I : H → E) '' (e.symm ≫ₕ e').source ∈ 𝓝[range (↑I : H → E)] x
have obtain : ∀ (x : H) (hx : x ∈ (e.symm ≫ₕ e').source), (↑I : H → E) '' (e.symm ≫ₕ e').source ∈ 𝓝[range (↑I : H → E)] (↑I : H → E) x
Tactic: obtain ⟨x, hx, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
x : H
hx : x ∈ (e.symm ≫ₕ e').source
⊢ (↑I : H → E) '' (e.symm ≫ₕ e').source ∈ 𝓝[range (↑I : H → E)] (↑I : H → E) x
have refine : (e.symm ≫ₕ e').source ∈ 𝓝 x
Tactic: refine I.image_mem_nhdsWithin ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
x : M
hxe : x ∈ e.source
hxe' : x ∈ e'.source
⊢ PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e') ∈
    𝓝[range (↑I : H → E)] (↑(e.extend I) : M → E) x
have hx : Membership.mem (γ := Set E) (PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'))
  ((↑(e.extend I) : M → E) x)
Tactic: apply extendCoordChange_source_mem_nhdsWithin
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
x : M
hxe : x ∈ e.source
hxe' : x ∈ e'.source
⊢ Membership.mem (γ := Set E) (PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'))
    ((↑(e.extend I) : M → E) x)
have hx : (↑(e.extend I) : M → E) x ∈ (↑(e.extend I) : M → E) '' (e.source ∩ e'.source)
Tactic: rw [← OpenPartialHomeomorph.extend_image_source_inter]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
⊢ UniqueDiffOn.{u_1, u_2} 𝕜 (E := E)
    (PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'))
have rw : UniqueDiffOn 𝕜 ((↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E))
Tactic: rw [extendCoordChange_source, I.image_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
⊢ UniqueDiffOn.{u_1, u_2} 𝕜 (E := E)
    (PartialEquiv.target (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'))
have rw : UniqueDiffOn.{u_1, u_2} 𝕜 (E := E) (PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e' e))
Tactic: rw [← extendCoordChange_symm, PartialEquiv.symm_target]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
⊢ ContDiffOn.{u_1, u_2, u_2} 𝕜 (E := E) n (↑(extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e') : E → E)
    (PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'))
have rw : ContDiffOn 𝕜 n (↑(extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e') : E → E)
  ((↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E))
Tactic: rw [I.extendCoordChange_source, I.image_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
x : E
hx : Membership.mem (γ := Set E) (PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e')) x
⊢ ContDiffWithinAt 𝕜 n (↑(extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e') : E → E) (range (↑I : H → E)) x
have apply : PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e') ∈ 𝓝[range (↑I : H → E)] x
Tactic: apply (I.contDiffOn_extendCoordChange he he' x hx).mono_of_mem_nhdsWithin
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
x : E
hx : Membership.mem (γ := Set E) (PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e')) x
⊢ PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e') ∈ 𝓝[range (↑I : H → E)] x
have rw : ∀ (hx : x ∈ (↑I : H → E) '' (e.symm ≫ₕ e').source), (↑I : H → E) '' (e.symm ≫ₕ e').source ∈ 𝓝[range (↑I : H → E)] x
Tactic: rw [I.extendCoordChange_source] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
x : E
hx : x ∈ (↑I : H → E) '' (e.symm ≫ₕ e').source
⊢ (↑I : H → E) '' (e.symm ≫ₕ e').source ∈ 𝓝[range (↑I : H → E)] x
have obtain : ∀ (z : H) (hz : z ∈ (e.symm ≫ₕ e').source), (↑I : H → E) '' (e.symm ≫ₕ e').source ∈ 𝓝[range (↑I : H → E)] (↑I : H → E) z
Tactic: obtain ⟨z, hz, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
x : M
hxe : x ∈ e.source
hxe' : x ∈ e'.source
⊢ ContDiffWithinAt 𝕜 n (↑(extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e') : E → E) (range (↑I : H → E))
    ((↑(e.extend I) : M → E) x)
have refine : Membership.mem (γ := Set E) (PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'))
  ((↑(e.extend I) : M → E) x)
Tactic: refine I.contDiffWithinAt_extendCoordChange he he' ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
x : M
hxe : x ∈ e.source
hxe' : x ∈ e'.source
⊢ Membership.mem (γ := Set E) (PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'))
    ((↑(e.extend I) : M → E) x)
have rw : (↑(e.extend I) : M → E) x ∈ (↑(e.extend I) : M → E) '' (e.source ∩ e'.source)
Tactic: rw [← OpenPartialHomeomorph.extend_image_source_inter]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
x : E
hx : Membership.mem (γ := Set E) (PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e')) x
⊢ ContinuousLinearMap.IsInvertible
    (fderivWithin 𝕜 (↑(extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e') : E → E)
      (PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e')) x)
have set : let φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e';
∀ (hx : x ∈ φ.source), ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 (↑φ : E → E) φ.source x)
Tactic: set φ := I.extendCoordChange e e'
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
x : E
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'
hx : x ∈ φ.source
⊢ ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 (↑φ : E → E) φ.source x)
have hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
Tactic: have hφ : ContDiffOn 𝕜 n φ φ.source := I.contDiffOn_extendCoordChange he he'