awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H₁ : Type u_6
inst : TopologicalSpace H₁
H₂ : Type u_7
inst_1 : TopologicalSpace H₂
H₃ : Type u_8
inst_2 : TopologicalSpace H₃
inst_3 : ChartedSpace H₁ H₂
inst_4 : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst_5 : HasGroupoid H₂ G₁
inst_6 : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst_7 : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e : H₂ → H₂) e.source
x_1 : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e
f : OpenPartialHomeomorph H₂ H₁
hf : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f
e' : OpenPartialHomeomorph H₃ H₂
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e'
f' : OpenPartialHomeomorph H₂ H₁
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f'
x : H₁
hx :
  (x ∈ f.target ∧ (↑f.symm : H₁ → H₂) x ∈ e.target) ∧
    (↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x) ∈ e'.source ∧
      (↑e' : H₃ → H₂) ((↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x)) ∈ f'.source
hxs : x ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source
hxs' : x ∈ f.target ∩ (↑f.symm : H₁ → H₂) ⁻¹' ((e.symm ≫ₕ e').source ∩ (↑(e.symm ≫ₕ e') : H₂ → H₂) ⁻¹' f'.source)
φ : OpenPartialHomeomorph H₁ H₁
hφG₁ : φ ∈ G₁
hφ_dom : x ∈ φ.source
hφ :
  EqOn (↑(f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f') : H₁ → H₁) (↑φ.toPartialEquiv : H₁ → H₁)
    ((↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)
⊢ ∃ (s : Set H₁), IsOpen[inst] s ∧ x ∈ s ∧ ((e ≫ₕ f).symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁
have simp_rw : ∃ (s : Set H₁), IsOpen[inst] s ∧ x ∈ s ∧ (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁
Tactic: simp_rw [OpenPartialHomeomorph.trans_symm_eq_symm_trans_symm,
        OpenPartialHomeomorph.trans_assoc]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (hypothesis)
Goal:
H₁ : Type u_6
inst : TopologicalSpace H₁
H₂ : Type u_7
inst_1 : TopologicalSpace H₂
H₃ : Type u_8
inst_2 : TopologicalSpace H₃
inst_3 : ChartedSpace H₁ H₂
inst_4 : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst_5 : HasGroupoid H₂ G₁
inst_6 : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst_7 : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e : H₂ → H₂) e.source
x_1 : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e
f : OpenPartialHomeomorph H₂ H₁
hf : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f
e' : OpenPartialHomeomorph H₃ H₂
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e'
f' : OpenPartialHomeomorph H₂ H₁
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f'
x : H₁
hx :
  (x ∈ f.target ∧ (↑f.symm : H₁ → H₂) x ∈ e.target) ∧
    (↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x) ∈ e'.source ∧
      (↑e' : H₃ → H₂) ((↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x)) ∈ f'.source
hxs : x ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source
hxs' : x ∈ f.target ∩ (↑f.symm : H₁ → H₂) ⁻¹' ((e.symm ≫ₕ e').source ∩ (↑(e.symm ≫ₕ e') : H₂ → H₂) ⁻¹' f'.source)
φ : OpenPartialHomeomorph H₁ H₁
hφG₁ : φ ∈ G₁
hφ_dom : x ∈ φ.source
hφ :
  EqOn (↑(f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f') : H₁ → H₁) (↑φ.toPartialEquiv : H₁ → H₁)
    ((↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)
⊢ ∃ (s : Set H₁), IsOpen[inst] s ∧ x ∈ s ∧ (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁
have hs : IsOpen[inst] (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source
Tactic: have hs : IsOpen (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source :=
        (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').open_source
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H₁ : Type u_6
inst : TopologicalSpace H₁
H₂ : Type u_7
inst_1 : TopologicalSpace H₂
H₃ : Type u_8
inst_2 : TopologicalSpace H₃
inst_3 : ChartedSpace H₁ H₂
inst_4 : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst_5 : HasGroupoid H₂ G₁
inst_6 : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst_7 : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e : H₂ → H₂) e.source
x_1 : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e
f : OpenPartialHomeomorph H₂ H₁
hf : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f
e' : OpenPartialHomeomorph H₃ H₂
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e'
f' : OpenPartialHomeomorph H₂ H₁
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f'
x : H₁
hx :
  (x ∈ f.target ∧ (↑f.symm : H₁ → H₂) x ∈ e.target) ∧
    (↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x) ∈ e'.source ∧
      (↑e' : H₃ → H₂) ((↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x)) ∈ f'.source
hxs : x ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source
hxs' : x ∈ f.target ∩ (↑f.symm : H₁ → H₂) ⁻¹' ((e.symm ≫ₕ e').source ∩ (↑(e.symm ≫ₕ e') : H₂ → H₂) ⁻¹' f'.source)
φ : OpenPartialHomeomorph H₁ H₁
hφG₁ : φ ∈ G₁
hφ_dom : x ∈ φ.source
hφ :
  EqOn (↑(f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f') : H₁ → H₁) (↑φ.toPartialEquiv : H₁ → H₁)
    ((↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)
hs : IsOpen[inst] (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source
⊢ ∃ (s : Set H₁), IsOpen[inst] s ∧ x ∈ s ∧ (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁
have refine_1 : x ∈ (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source ∩ φ.source
Tactic: refine ⟨_, hs.inter φ.open_source, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H₁ : Type u_6
inst : TopologicalSpace H₁
H₂ : Type u_7
inst_1 : TopologicalSpace H₂
H₃ : Type u_8
inst_2 : TopologicalSpace H₃
inst_3 : ChartedSpace H₁ H₂
inst_4 : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst_5 : HasGroupoid H₂ G₁
inst_6 : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst_7 : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e : H₂ → H₂) e.source
x_1 : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e
f : OpenPartialHomeomorph H₂ H₁
hf : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f
e' : OpenPartialHomeomorph H₃ H₂
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e'
f' : OpenPartialHomeomorph H₂ H₁
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f'
x : H₁
hx :
  (x ∈ f.target ∧ (↑f.symm : H₁ → H₂) x ∈ e.target) ∧
    (↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x) ∈ e'.source ∧
      (↑e' : H₃ → H₂) ((↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x)) ∈ f'.source
hxs : x ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source
hxs' : x ∈ f.target ∩ (↑f.symm : H₁ → H₂) ⁻¹' ((e.symm ≫ₕ e').source ∩ (↑(e.symm ≫ₕ e') : H₂ → H₂) ⁻¹' f'.source)
φ : OpenPartialHomeomorph H₁ H₁
hφG₁ : φ ∈ G₁
hφ_dom : x ∈ φ.source
hφ :
  EqOn (↑(f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f') : H₁ → H₁) (↑φ.toPartialEquiv : H₁ → H₁)
    ((↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)
hs : IsOpen[inst] (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source
refine_1 : x ∈ (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source ∩ φ.source
⊢ ∃ (s : Set H₁), IsOpen[inst] s ∧ x ∈ s ∧ (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁
have refine_2 : (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').restr ((f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source ∩ φ.source) ∈ G₁
Tactic: refine ⟨_, hs.inter φ.open_source, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H₁ : Type u_6
inst : TopologicalSpace H₁
H₂ : Type u_7
inst_1 : TopologicalSpace H₂
H₃ : Type u_8
inst_2 : TopologicalSpace H₃
inst_3 : ChartedSpace H₁ H₂
inst_4 : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst_5 : HasGroupoid H₂ G₁
inst_6 : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst_7 : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e : H₂ → H₂) e.source
x_1 : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e
f : OpenPartialHomeomorph H₂ H₁
hf : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f
e' : OpenPartialHomeomorph H₃ H₂
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e'
f' : OpenPartialHomeomorph H₂ H₁
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f'
x : H₁
hx :
  (x ∈ f.target ∧ (↑f.symm : H₁ → H₂) x ∈ e.target) ∧
    (↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x) ∈ e'.source ∧
      (↑e' : H₃ → H₂) ((↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x)) ∈ f'.source
hxs : x ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source
hxs' : x ∈ f.target ∩ (↑f.symm : H₁ → H₂) ⁻¹' ((e.symm ≫ₕ e').source ∩ (↑(e.symm ≫ₕ e') : H₂ → H₂) ⁻¹' f'.source)
φ : OpenPartialHomeomorph H₁ H₁
hφG₁ : φ ∈ G₁
hφ_dom : x ∈ φ.source
hφ :
  EqOn (↑(f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f') : H₁ → H₁) (↑φ.toPartialEquiv : H₁ → H₁)
    ((↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)
hs : IsOpen[inst] (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source
⊢ (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').restr ((f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source ∩ φ.source) ∈ G₁
have refine_2 : (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').restr ((f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source ∩ φ.source) ≈
  φ.restr (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source
Tactic: refine G₁.mem_of_eqOnSource (closedUnderRestriction' hφG₁ hs) ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H₁ : Type u_6
inst : TopologicalSpace H₁
H₂ : Type u_7
inst_1 : TopologicalSpace H₂
H₃ : Type u_8
inst_2 : TopologicalSpace H₃
inst_3 : ChartedSpace H₁ H₂
inst_4 : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst_5 : HasGroupoid H₂ G₁
inst_6 : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst_7 : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e : H₂ → H₂) e.source
x_1 : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e
f : OpenPartialHomeomorph H₂ H₁
hf : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f
e' : OpenPartialHomeomorph H₃ H₂
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e'
f' : OpenPartialHomeomorph H₂ H₁
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f'
x : H₁
hx :
  (x ∈ f.target ∧ (↑f.symm : H₁ → H₂) x ∈ e.target) ∧
    (↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x) ∈ e'.source ∧
      (↑e' : H₃ → H₂) ((↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x)) ∈ f'.source
hxs : x ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source
hxs' : x ∈ f.target ∩ (↑f.symm : H₁ → H₂) ⁻¹' ((e.symm ≫ₕ e').source ∩ (↑(e.symm ≫ₕ e') : H₂ → H₂) ⁻¹' f'.source)
φ : OpenPartialHomeomorph H₁ H₁
hφG₁ : φ ∈ G₁
hφ_dom : x ∈ φ.source
hφ :
  EqOn (↑(f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f') : H₁ → H₁) (↑φ.toPartialEquiv : H₁ → H₁)
    ((↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)
hs : IsOpen[inst] (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source
⊢ (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').restr ((f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source ∩ φ.source) ≈
    φ.restr (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source
have refine_2 : (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').restr φ.source ≈ φ.restr (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source
Tactic: rw [OpenPartialHomeomorph.restr_source_inter]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H₁ : Type u_6
inst : TopologicalSpace H₁
H₂ : Type u_7
inst_1 : TopologicalSpace H₂
H₃ : Type u_8
inst_2 : TopologicalSpace H₃
inst_3 : ChartedSpace H₁ H₂
inst_4 : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst_5 : HasGroupoid H₂ G₁
inst_6 : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst_7 : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e : H₂ → H₂) e.source
x_1 : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e
f : OpenPartialHomeomorph H₂ H₁
hf : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f
e' : OpenPartialHomeomorph H₃ H₂
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e'
f' : OpenPartialHomeomorph H₂ H₁
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f'
x : H₁
hx :
  (x ∈ f.target ∧ (↑f.symm : H₁ → H₂) x ∈ e.target) ∧
    (↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x) ∈ e'.source ∧
      (↑e' : H₃ → H₂) ((↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x)) ∈ f'.source
hxs : x ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source
hxs' : x ∈ f.target ∩ (↑f.symm : H₁ → H₂) ⁻¹' ((e.symm ≫ₕ e').source ∩ (↑(e.symm ≫ₕ e') : H₂ → H₂) ⁻¹' f'.source)
φ : OpenPartialHomeomorph H₁ H₁
hφG₁ : φ ∈ G₁
hφ_dom : x ∈ φ.source
hφ :
  EqOn (↑(f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f') : H₁ → H₁) (↑φ.toPartialEquiv : H₁ → H₁)
    ((↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)
hs : IsOpen[inst] (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source
⊢ (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').restr φ.source ≈ φ.restr (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source
have refine_2 : (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source ∩ φ.source ⊆ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source
Tactic: refine OpenPartialHomeomorph.Set.EqOn.restr_eqOn_source (hφ.mono ?_)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H₁ : Type u_6
inst : TopologicalSpace H₁
H₂ : Type u_7
inst_1 : TopologicalSpace H₂
H₃ : Type u_8
inst_2 : TopologicalSpace H₃
inst_3 : ChartedSpace H₁ H₂
inst_4 : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst_5 : HasGroupoid H₂ G₁
inst_6 : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst_7 : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e : H₂ → H₂) e.source
x_1 : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e
f : OpenPartialHomeomorph H₂ H₁
hf : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f
e' : OpenPartialHomeomorph H₃ H₂
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e'
f' : OpenPartialHomeomorph H₂ H₁
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f'
x : H₁
hx :
  (x ∈ f.target ∧ (↑f.symm : H₁ → H₂) x ∈ e.target) ∧
    (↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x) ∈ e'.source ∧
      (↑e' : H₃ → H₂) ((↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x)) ∈ f'.source
hxs : x ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source
hxs' : x ∈ f.target ∩ (↑f.symm : H₁ → H₂) ⁻¹' ((e.symm ≫ₕ e').source ∩ (↑(e.symm ≫ₕ e') : H₂ → H₂) ⁻¹' f'.source)
φ : OpenPartialHomeomorph H₁ H₁
hφG₁ : φ ∈ G₁
hφ_dom : x ∈ φ.source
hφ :
  EqOn (↑(f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f') : H₁ → H₁) (↑φ.toPartialEquiv : H₁ → H₁)
    ((↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)
hs : IsOpen[inst] (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source
⊢ (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source ∩ φ.source ⊆ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source
have refine_2 : ∀ ⦃my_y : H₁⦄,
  my_y ∈ (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source ∩ φ.source →
    my_y ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H₁ : Type u_6
inst : TopologicalSpace H₁
H₂ : Type u_7
inst_1 : TopologicalSpace H₂
H₃ : Type u_8
inst_2 : TopologicalSpace H₃
inst_3 : ChartedSpace H₁ H₂
inst_4 : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst_5 : HasGroupoid H₂ G₁
inst_6 : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst_7 : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e : H₂ → H₂) e.source
x_1 : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e
f : OpenPartialHomeomorph H₂ H₁
hf : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f
e' : OpenPartialHomeomorph H₃ H₂
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e'
f' : OpenPartialHomeomorph H₂ H₁
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f'
x : H₁
hx :
  (x ∈ f.target ∧ (↑f.symm : H₁ → H₂) x ∈ e.target) ∧
    (↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x) ∈ e'.source ∧
      (↑e' : H₃ → H₂) ((↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x)) ∈ f'.source
hxs : x ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source
hxs' : x ∈ f.target ∩ (↑f.symm : H₁ → H₂) ⁻¹' ((e.symm ≫ₕ e').source ∩ (↑(e.symm ≫ₕ e') : H₂ → H₂) ⁻¹' f'.source)
φ : OpenPartialHomeomorph H₁ H₁
hφG₁ : φ ∈ G₁
hφ_dom : x ∈ φ.source
hφ :
  EqOn (↑(f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f') : H₁ → H₁) (↑φ.toPartialEquiv : H₁ → H₁)
    ((↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)
hs : IsOpen[inst] (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source
refine_2 refine_2₁ refine_2₂ :
  ∀ ⦃my_y : H₁⦄,
    my_y ∈ (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source ∩ φ.source →
      my_y ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source
⊢ (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source ∩ φ.source ⊆ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source
have refine_2₃ : ∀ ⦃my_y : H₁⦄,
  (my_y ∈ f.target ∧
        (↑f.symm : H₁ → H₂) my_y ∈ e.target ∧
          (↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) my_y) ∈ e'.source ∧
            (↑e' : H₃ → H₂) ((↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) my_y)) ∈ f'.source) ∧
      my_y ∈ φ.source →
    my_y ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalSourceTargetProperty (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_4
H : Type u_6
G : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : TopologicalSpace H
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_10
N : Type u_12
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
hf : ContinuousAt f x
hP : IsLocalSourceTargetProperty P
domChart : OpenPartialHomeomorph M H
codChart : OpenPartialHomeomorph N G
hx : x ∈ domChart.source
hfx : f x ∈ codChart.source
hdomChart : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (IsManifold.maximalAtlas I n M) domChart
hcodChart : Membership.mem (γ := Set (OpenPartialHomeomorph N G)) (IsManifold.maximalAtlas J n N) codChart
hfP : P f domChart codChart
⊢ LiftSourceTargetPropertyAt I J n f x P
have obtain : ∀ (s : Set M) (hs : s ⊆ f ⁻¹' codChart.source) (hsopen : IsOpen[inst_7] s) (hxs : x ∈ s),
  LiftSourceTargetPropertyAt I J n f x P
Tactic: obtain ⟨s, hs, hsopen, hxs⟩ := mem_nhds_iff.mp <|
    hf.preimage_mem_nhds (codChart.open_source.mem_nhds hfx)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalSourceTargetProperty (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_4
H : Type u_6
G : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : TopologicalSpace H
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_10
N : Type u_12
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
f g : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
hP : IsLocalSourceTargetProperty P
hf : LiftSourceTargetPropertyAt I J n f x P
h' : f =ᶠ[𝓝 x] g
⊢ LiftSourceTargetPropertyAt I J n g x P
have obtain : ∀ (s' : Set M) (hxs' : s' ∈ 𝓝 x) (hfg : EqOn f g s'), LiftSourceTargetPropertyAt I J n g x P
Tactic: obtain ⟨s', hxs', hfg⟩ := h'.exists_mem
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalSourceTargetProperty (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_4
H : Type u_6
G : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : TopologicalSpace H
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_10
N : Type u_12
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
f g : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
hP : IsLocalSourceTargetProperty P
hf : LiftSourceTargetPropertyAt I J n f x P
h' : f =ᶠ[𝓝 x] g
s' : Set M
hxs' : s' ∈ 𝓝 x
hfg : EqOn f g s'
⊢ LiftSourceTargetPropertyAt I J n g x P
have obtain : ∀ (s : Set M) (hss' : s ⊆ s') (hs : IsOpen[inst_7] s) (hxs : x ∈ s), LiftSourceTargetPropertyAt I J n g x P
Tactic: obtain ⟨s, hss', hs, hxs⟩ := mem_nhds_iff.mp hxs'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalSourceTargetProperty (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_4
H : Type u_6
G : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : TopologicalSpace H
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_10
N : Type u_12
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
f g : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
hP : IsLocalSourceTargetProperty P
hf : LiftSourceTargetPropertyAt I J n f x P
h' : f =ᶠ[𝓝 x] g
s' : Set M
hxs' : s' ∈ 𝓝 x
hfg : EqOn f g s'
s : Set M
hss' : s ⊆ s'
hs : IsOpen[inst_7] s
hxs : x ∈ s
⊢ LiftSourceTargetPropertyAt I J n g x P
have refine_1 : x ∈ (hf.domChart (P := P).restr s).source
Tactic: refine ⟨hf.domChart.restr s, hf.codChart, ?_, ?_, ?_, hf.codChart_mem_maximalAtlas, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalSourceTargetProperty (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_4
H : Type u_6
G : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : TopologicalSpace H
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_10
N : Type u_12
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
f g : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
hP : IsLocalSourceTargetProperty P
hf : LiftSourceTargetPropertyAt I J n f x P
h' : f =ᶠ[𝓝 x] g
s' : Set M
hxs' : s' ∈ 𝓝 x
hfg : EqOn f g s'
s : Set M
hss' : s ⊆ s'
hs : IsOpen[inst_7] s
hxs : x ∈ s
refine_1 : x ∈ (hf.domChart (P := P).restr s).source
⊢ LiftSourceTargetPropertyAt I J n g x P
have refine_2 : g x ∈ hf.codChart (P := P).source
Tactic: refine ⟨hf.domChart.restr s, hf.codChart, ?_, ?_, ?_, hf.codChart_mem_maximalAtlas, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalSourceTargetProperty (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_4
H : Type u_6
G : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : TopologicalSpace H
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_10
N : Type u_12
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
f g : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
hP : IsLocalSourceTargetProperty P
hf : LiftSourceTargetPropertyAt I J n f x P
h' : f =ᶠ[𝓝 x] g
s' : Set M
hxs' : s' ∈ 𝓝 x
hfg : EqOn f g s'
s : Set M
hss' : s ⊆ s'
hs : IsOpen[inst_7] s
hxs : x ∈ s
refine_1 : x ∈ (hf.domChart (P := P).restr s).source
refine_2 : g x ∈ hf.codChart (P := P).source
⊢ LiftSourceTargetPropertyAt I J n g x P
have refine_3 : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (IsManifold.maximalAtlas I n M) (hf.domChart (P := P).restr s)
Tactic: refine ⟨hf.domChart.restr s, hf.codChart, ?_, ?_, ?_, hf.codChart_mem_maximalAtlas, ?_, ?_⟩