awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
M' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
h : Nonempty H
e : OpenPartialHomeomorph (M ⊕ M') H
x : OpenPartialHomeomorph M H
hx : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) ChartedSpace.atlas x
hxe : (fun (e : OpenPartialHomeomorph M H) ↦ (e.lift_openEmbedding ⋯ : OpenPartialHomeomorph (M ⊕ M') H)) x = e
⊢ (∃ (f : OpenPartialHomeomorph M H),
      Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f ∧
        Eq (α := OpenPartialHomeomorph (M ⊕ M') H)
          ((fun (e : OpenPartialHomeomorph M H) ↦ (e.lift_openEmbedding ⋯ : OpenPartialHomeomorph (M ⊕ M') H)) x)
          (f.lift_openEmbedding ⋯)) ∨
    ∃ (f' : OpenPartialHomeomorph M' H),
      Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f' ∧
        Eq (α := OpenPartialHomeomorph (M ⊕ M') H)
          ((fun (e : OpenPartialHomeomorph M H) ↦ (e.lift_openEmbedding ⋯ : OpenPartialHomeomorph (M ⊕ M') H)) x)
          (f'.lift_openEmbedding ⋯)
have inl : ∃ (f : OpenPartialHomeomorph M H),
  Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f ∧
    Eq (α := OpenPartialHomeomorph (M ⊕ M') H)
      ((fun (e : OpenPartialHomeomorph M H) ↦ (e.lift_openEmbedding sorry : OpenPartialHomeomorph (M ⊕ M') H)) x)
      (f.lift_openEmbedding sorry)
Tactic: left
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
M' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
h : Nonempty H
e : OpenPartialHomeomorph (M ⊕ M') H
x : OpenPartialHomeomorph M H
hx : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) ChartedSpace.atlas x
hxe : (fun (e : OpenPartialHomeomorph M H) ↦ (e.lift_openEmbedding ⋯ : OpenPartialHomeomorph (M ⊕ M') H)) x = e
w : OpenPartialHomeomorph M H
⊢ ∃ (f : OpenPartialHomeomorph M H),
    Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f ∧
      Eq (α := OpenPartialHomeomorph (M ⊕ M') H)
        ((fun (e : OpenPartialHomeomorph M H) ↦ (e.lift_openEmbedding ⋯ : OpenPartialHomeomorph (M ⊕ M') H)) x)
        (f.lift_openEmbedding ⋯)
have h₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) x ∧
  Eq (α := OpenPartialHomeomorph (M ⊕ M') H)
    ((fun (e : OpenPartialHomeomorph M H) ↦ (e.lift_openEmbedding sorry : OpenPartialHomeomorph (M ⊕ M') H)) x)
    (x.lift_openEmbedding sorry)
Tactic: use x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
M' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
h : Nonempty H
e : OpenPartialHomeomorph (M ⊕ M') H
x : OpenPartialHomeomorph M' H
hx : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) ChartedSpace.atlas x
hxe : (fun (e : OpenPartialHomeomorph M' H) ↦ (e.lift_openEmbedding ⋯ : OpenPartialHomeomorph (M ⊕ M') H)) x = e
⊢ (∃ (f : OpenPartialHomeomorph M H),
      Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f ∧ e = f.lift_openEmbedding ⋯) ∨
    ∃ (f' : OpenPartialHomeomorph M' H),
      Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f' ∧ e = f'.lift_openEmbedding ⋯
have inr : (∃ (f : OpenPartialHomeomorph M H),
    Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f ∧
      Eq (α := OpenPartialHomeomorph (M ⊕ M') H)
        ((fun (e : OpenPartialHomeomorph M' H) ↦ (e.lift_openEmbedding sorry : OpenPartialHomeomorph (M ⊕ M') H)) x)
        (f.lift_openEmbedding sorry)) ∨
  ∃ (f' : OpenPartialHomeomorph M' H),
    Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f' ∧
      Eq (α := OpenPartialHomeomorph (M ⊕ M') H)
        ((fun (e : OpenPartialHomeomorph M' H) ↦ (e.lift_openEmbedding sorry : OpenPartialHomeomorph (M ⊕ M') H)) x)
        (f'.lift_openEmbedding sorry)
Tactic: rw [← hxe]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
M' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
h : Nonempty H
e : OpenPartialHomeomorph (M ⊕ M') H
x : OpenPartialHomeomorph M' H
hx : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) ChartedSpace.atlas x
hxe : (fun (e : OpenPartialHomeomorph M' H) ↦ (e.lift_openEmbedding ⋯ : OpenPartialHomeomorph (M ⊕ M') H)) x = e
⊢ (∃ (f : OpenPartialHomeomorph M H),
      Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f ∧
        Eq (α := OpenPartialHomeomorph (M ⊕ M') H)
          ((fun (e : OpenPartialHomeomorph M' H) ↦ (e.lift_openEmbedding ⋯ : OpenPartialHomeomorph (M ⊕ M') H)) x)
          (f.lift_openEmbedding ⋯)) ∨
    ∃ (f' : OpenPartialHomeomorph M' H),
      Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f' ∧
        Eq (α := OpenPartialHomeomorph (M ⊕ M') H)
          ((fun (e : OpenPartialHomeomorph M' H) ↦ (e.lift_openEmbedding ⋯ : OpenPartialHomeomorph (M ⊕ M') H)) x)
          (f'.lift_openEmbedding ⋯)
have inr : ∃ (f' : OpenPartialHomeomorph M' H),
  Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f' ∧
    Eq (α := OpenPartialHomeomorph (M ⊕ M') H)
      ((fun (e : OpenPartialHomeomorph M' H) ↦ (e.lift_openEmbedding sorry : OpenPartialHomeomorph (M ⊕ M') H)) x)
      (f'.lift_openEmbedding sorry)
Tactic: right
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
M' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
h : Nonempty H
e : OpenPartialHomeomorph (M ⊕ M') H
x : OpenPartialHomeomorph M' H
hx : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) ChartedSpace.atlas x
hxe : (fun (e : OpenPartialHomeomorph M' H) ↦ (e.lift_openEmbedding ⋯ : OpenPartialHomeomorph (M ⊕ M') H)) x = e
w : OpenPartialHomeomorph M' H
⊢ ∃ (f' : OpenPartialHomeomorph M' H),
    Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f' ∧
      Eq (α := OpenPartialHomeomorph (M ⊕ M') H)
        ((fun (e : OpenPartialHomeomorph M' H) ↦ (e.lift_openEmbedding ⋯ : OpenPartialHomeomorph (M ⊕ M') H)) x)
        (f'.lift_openEmbedding ⋯)
have h₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') x ∧
  Eq (α := OpenPartialHomeomorph (M ⊕ M') H)
    ((fun (e : OpenPartialHomeomorph M' H) ↦ (e.lift_openEmbedding sorry : OpenPartialHomeomorph (M ⊕ M') H)) x)
    (x.lift_openEmbedding sorry)
Tactic: use x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M'
inst_2 : TopologicalSpace H
inst_3 : ChartedSpace H M
f : M → M'
hf : IsLocalHomeomorph f
g : M' → M
hg : Function.RightInverse g f
q : M'
⊢ q ∈ (toPartialEquiv (hf.localInverseAt (g q) ≫ₕ chartAt H (g q))).source
have nth_rw : f (g q) ∈ (toPartialEquiv (hf.localInverseAt (g q) ≫ₕ chartAt H (g q))).source
Tactic: nth_rw 3 [← hg.eq q]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
he : e ∈ c.atlas
⊢ IsOpen[c.toTopologicalSpace] e.source
have a : Membership.mem (γ := Set (Set M))
  (⋃ e ∈ c.atlas, ⋃ (s : Set H), ⋃ (_ : IsOpen[inst] s), {(↑e : M → H) ⁻¹' s ∩ e.source}) e.source
Tactic: apply TopologicalSpace.GenerateOpen.basic
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
he : e ∈ c.atlas
⊢ Membership.mem (γ := Set (Set M))
    (⋃ e ∈ c.atlas, ⋃ (s : Set H), ⋃ (_ : IsOpen[inst] s), {(↑e : M → H) ⁻¹' s ∩ e.source}) e.source
have a : ∃ i ∈ c.atlas, ∃ (i_1 : Set H), IsOpen[inst] i_1 ∧ e.source = (↑i : M → H) ⁻¹' i_1 ∩ i.source
Tactic: simp only [exists_prop, mem_iUnion, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
he : e ∈ c.atlas
⊢ ∃ i ∈ c.atlas, ∃ (i_1 : Set H), IsOpen[inst] i_1 ∧ e.source = (↑i : M → H) ⁻¹' i_1 ∩ i.source
have a : e.source = (↑e : M → H) ⁻¹' univ ∩ e.source
Tactic: refine ⟨e, he, univ, isOpen_univ, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (hypothesis)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
he : e ∈ c.atlas
⊢ IsOpen[inst] e.target
have E : e.target ∩ (↑e.symm : H → M) ⁻¹' e.source = e.target
Tactic: have E : e.target ∩ e.symm ⁻¹' e.source = e.target :=
    Subset.antisymm inter_subset_left fun x hx ↦
      ⟨hx, PartialEquiv.target_subset_preimage_source _ hx⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
this : TopologicalSpace M := c.toTopologicalSpace
⊢ ContinuousOn (↑e : M → H) e.source
have rw : ∀ (t : Set H), IsOpen[inst] t → IsOpen[c.toTopologicalSpace] (e.source ∩ (↑e : M → H) ⁻¹' t)
Tactic: rw [continuousOn_open_iff (c.open_source' he)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
this : TopologicalSpace M := c.toTopologicalSpace
s : Set H
s_open : IsOpen[inst] s
⊢ IsOpen[c.toTopologicalSpace] (e.source ∩ (↑e : M → H) ⁻¹' s)
have rw : IsOpen[c.toTopologicalSpace] ((↑e : M → H) ⁻¹' s ∩ e.source)
Tactic: rw [inter_comm]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
this : TopologicalSpace M := c.toTopologicalSpace
s : Set H
s_open : IsOpen[inst] s
⊢ IsOpen[c.toTopologicalSpace] ((↑e : M → H) ⁻¹' s ∩ e.source)
have a : Membership.mem (γ := Set (Set M))
  (⋃ e ∈ c.atlas, ⋃ (s : Set H), ⋃ (_ : IsOpen[inst] s), {(↑e : M → H) ⁻¹' s ∩ e.source})
  ((↑e : M → H) ⁻¹' s ∩ e.source)
Tactic: apply TopologicalSpace.GenerateOpen.basic
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
this : TopologicalSpace M := c.toTopologicalSpace
s : Set H
s_open : IsOpen[inst] s
⊢ Membership.mem (γ := Set (Set M))
    (⋃ e ∈ c.atlas, ⋃ (s : Set H), ⋃ (_ : IsOpen[inst] s), {(↑e : M → H) ⁻¹' s ∩ e.source})
    ((↑e : M → H) ⁻¹' s ∩ e.source)
have a : ∃ i ∈ c.atlas, ∃ (i_1 : Set H), IsOpen[inst] i_1 ∧ (↑e : M → H) ⁻¹' s ∩ e.source = (↑i : M → H) ⁻¹' i_1 ∩ i.source
Tactic: simp only [exists_prop, mem_iUnion, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
this : TopologicalSpace M := c.toTopologicalSpace
⊢ ContinuousOn e.invFun e.target
have h : ∀ (t : Set M),
  Membership.mem (γ := Set (Set M))
      (⋃ e ∈ c.atlas, ⋃ (s : Set H), ⋃ (_ : IsOpen[inst] s), {(↑e : M → H) ⁻¹' s ∩ e.source}) t →
    IsOpen[inst] (e.target ∩ e.invFun ⁻¹' t)
Tactic: apply continuousOn_isOpen_of_generateFrom
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (hypothesis)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
this : TopologicalSpace M := c.toTopologicalSpace
t : Set M
ht :
  Membership.mem (γ := Set (Set M))
    (⋃ e ∈ c.atlas, ⋃ (s : Set H), ⋃ (_ : IsOpen[inst] s), {(↑e : M → H) ⁻¹' s ∩ e.source}) t
⊢ IsOpen[inst] (e.target ∩ e.invFun ⁻¹' t)
have ht₁ : ∃ i ∈ c.atlas, ∃ (i_1 : Set H), IsOpen[inst] i_1 ∧ t = (↑i : M → H) ⁻¹' i_1 ∩ i.source
Tactic: simp only [exists_prop, mem_iUnion, mem_singleton_iff] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
this : TopologicalSpace M := c.toTopologicalSpace
t : Set M
ht : ∃ i ∈ c.atlas, ∃ (i_1 : Set H), IsOpen[inst] i_1 ∧ t = (↑i : M → H) ⁻¹' i_1 ∩ i.source
⊢ IsOpen[inst] (e.target ∩ e.invFun ⁻¹' t)
have h : ∀ (e' : PartialEquiv M H) (e'_atlas : e' ∈ c.atlas) (s : Set H) (s_open : IsOpen[inst] s)
  (ts : t = (↑e' : M → H) ⁻¹' s ∩ e'.source), IsOpen[inst] (e.target ∩ e.invFun ⁻¹' t)
Tactic: rcases ht with ⟨e', e'_atlas, s, s_open, ts⟩
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
this : TopologicalSpace M := c.toTopologicalSpace
t : Set M
e' : PartialEquiv M H
e'_atlas : e' ∈ c.atlas
s : Set H
s_open : IsOpen[inst] s
ts : t = (↑e' : M → H) ⁻¹' s ∩ e'.source
⊢ IsOpen[inst] (e.target ∩ e.invFun ⁻¹' t)
have h : IsOpen[inst] (e.target ∩ e.invFun ⁻¹' ((↑e' : M → H) ⁻¹' s ∩ e'.source))
Tactic: rw [ts]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (hypothesis)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
this : TopologicalSpace M := c.toTopologicalSpace
t : Set M
e' : PartialEquiv M H
e'_atlas : e' ∈ c.atlas
s : Set H
s_open : IsOpen[inst] s
ts : t = (↑e' : M → H) ⁻¹' s ∩ e'.source
f : PartialEquiv H H := e.symm ≫ e'
⊢ IsOpen[inst] (e.target ∩ e.invFun ⁻¹' ((↑e' : M → H) ⁻¹' s ∩ e'.source))
have this₁ : IsOpen[inst] ((↑f : H → H) ⁻¹' s ∩ f.source)
Tactic: have : IsOpen (f ⁻¹' s ∩ f.source) := by
        simpa [f, inter_comm] using (continuousOn_open_iff (c.open_source e e' he e'_atlas)).1
          (c.continuousOn_toFun e e' he e'_atlas) s s_open
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
this_1 : TopologicalSpace M := c.toTopologicalSpace
t : Set M
e' : PartialEquiv M H
e'_atlas : e' ∈ c.atlas
s : Set H
s_open : IsOpen[inst] s
ts : t = (↑e' : M → H) ⁻¹' s ∩ e'.source
f : PartialEquiv H H := e.symm ≫ e'
this : IsOpen[inst] ((↑f : H → H) ⁻¹' s ∩ f.source)
⊢ (↑e' : M → H) ∘ (↑e.symm : H → M) ⁻¹' s ∩ (e.target ∩ (↑e.symm : H → M) ⁻¹' e'.source) =
    e.target ∩ ((↑e' : M → H) ∘ (↑e.symm : H → M) ⁻¹' s ∩ (↑e.symm : H → M) ⁻¹' e'.source)
have rw : (↑e' : M → H) ∘ (↑e.symm : H → M) ⁻¹' s ∩ e.target ∩ (↑e.symm : H → M) ⁻¹' e'.source =
  e.target ∩ (↑e' : M → H) ∘ (↑e.symm : H → M) ⁻¹' s ∩ (↑e.symm : H → M) ⁻¹' e'.source
Tactic: rw [← inter_assoc, ← inter_assoc]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
this_1 : TopologicalSpace M := c.toTopologicalSpace
t : Set M
e' : PartialEquiv M H
e'_atlas : e' ∈ c.atlas
s : Set H
s_open : IsOpen[inst] s
ts : t = (↑e' : M → H) ⁻¹' s ∩ e'.source
f : PartialEquiv H H := e.symm ≫ e'
this : IsOpen[inst] ((↑f : H → H) ⁻¹' s ∩ f.source)
⊢ (↑e' : M → H) ∘ (↑e.symm : H → M) ⁻¹' s ∩ e.target ∩ (↑e.symm : H → M) ⁻¹' e'.source =
    e.target ∩ (↑e' : M → H) ∘ (↑e.symm : H → M) ⁻¹' s ∩ (↑e.symm : H → M) ⁻¹' e'.source
have e_a : (↑e' : M → H) ∘ (↑e.symm : H → M) ⁻¹' s ∩ e.target = e.target ∩ (↑e' : M → H) ∘ (↑e.symm : H → M) ⁻¹' s
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (hypothesis)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
this_1 : TopologicalSpace M := c.toTopologicalSpace
t : Set M
e' : PartialEquiv M H
e'_atlas : e' ∈ c.atlas
s : Set H
s_open : IsOpen[inst] s
ts : t = (↑e' : M → H) ⁻¹' s ∩ e'.source
f : PartialEquiv H H := e.symm ≫ e'
this : IsOpen[inst] ((↑f : H → H) ⁻¹' s ∩ f.source)
⊢ IsOpen[inst] (e.target ∩ e.invFun ⁻¹' ((↑e' : M → H) ⁻¹' s ∩ e'.source))
have A : (↑e' : M → H) ∘ (↑e.symm : H → M) ⁻¹' s ∩ (e.target ∩ (↑e.symm : H → M) ⁻¹' e'.source) =
  e.target ∩ ((↑e' : M → H) ∘ (↑e.symm : H → M) ⁻¹' s ∩ (↑e.symm : H → M) ⁻¹' e'.source)
Tactic: have A : e' ∘ e.symm ⁻¹' s ∩ (e.target ∩ e.symm ⁻¹' e'.source) =
          e.target ∩ (e' ∘ e.symm ⁻¹' s ∩ e.symm ⁻¹' e'.source) := by
        rw [← inter_assoc, ← inter_assoc]
        congr 1
        exact inter_comm _ _
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
x : M
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph M H))
    (⋃ (e : PartialEquiv M H), ⋃ (he : e ∈ c.atlas), {c.openPartialHomeomorph e he})
    (c.openPartialHomeomorph (c.chartAt x) ⋯)
have simp : ∃ (i : PartialEquiv M H) (h : i ∈ c.atlas), c.openPartialHomeomorph (c.chartAt x) sorry = c.openPartialHomeomorph i sorry
Tactic: simp only [mem_iUnion, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
⊢ ∀ᶠ (y : M) in 𝓝 c, ‖f y‖ = ‖f c‖
have hI : range (↑I : H → E) = univ
Tactic: have hI : range I = univ := ModelWithCorners.Boundaryless.range_eq_univ
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
⊢ 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
have rw : 𝓝[univ] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
Tactic: rw [hI, nhdsWithin_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
rw : 𝓝[univ] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
⊢ 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
have rw₁ : 𝓝 ((↑e : M → E) c) = 𝓝 ((↑e : M → E) c)
Tactic: rw [hI, nhdsWithin_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
⊢ ∀ᶠ (y : M) in 𝓝 c, ‖f y‖ = ‖f c‖
have H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
Tactic: have H₁ : 𝓝[range I] (e c) = 𝓝 (e c) := by rw [hI, nhdsWithin_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
⊢ map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = 𝓝 c
have rw : map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) =
  map (↑(extChartAt I c).symm : E → M) (𝓝[range (↑I : H → E)] (↑(extChartAt I c) : M → E) c)
Tactic: rw [← map_extChartAt_symm_nhdsWithin_range (I := I) c, H₁]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
rw :
  map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) =
    map (↑(extChartAt I c).symm : E → M) (𝓝[range (↑I : H → E)] (↑(extChartAt I c) : M → E) c)
⊢ map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = 𝓝 c
have rw₁ : map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = map (↑(extChartAt I c).symm : E → M) (𝓝 ((↑e : M → E) c))
Tactic: rw [← map_extChartAt_symm_nhdsWithin_range (I := I) c, H₁]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
⊢ ∀ᶠ (y : M) in 𝓝 c, ‖f y‖ = ‖f c‖
have H₂ : map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = 𝓝 c
Tactic: have H₂ : map e.symm (𝓝 (e c)) = 𝓝 c := by
    rw [← map_extChartAt_symm_nhdsWithin_range (I := I) c, H₁]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Complex (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst_5 : I.Boundaryless
M : Type u_4
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range (↑I : H → E) = univ
H₁ : 𝓝[range (↑I : H → E)] (↑e : M → E) c = 𝓝 ((↑e : M → E) c)
H₂ : map (↑e.symm : E → M) (𝓝 ((↑e : M → E) c)) = 𝓝 c
⊢ ∀ᶠ (y : M) in 𝓝 c, ‖f y‖ = ‖f c‖
have rw : ∀ᶠ (a : E) in 𝓝 ((↑e : M → E) c), ‖f ((↑e.symm : E → M) a)‖ = ‖f c‖
Tactic: rw [← H₂, eventually_map]