awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
s : Set H
x : H
f g : H → H
hfgs : ∀ y ∈ s, f y = g y
h_1 : f x = g x
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hex : x ∈ e.source
⊢ ∃ e ∈ G, EqOn g (↑e.toPartialEquiv : H → H) (s ∩ e.source) ∧ x ∈ e.source
have refine : EqOn g (↑e.toPartialEquiv : H → H) (s ∩ e.source)
Tactic: refine ⟨e, heG, ?_, hex⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
s : Set H
x : H
f g : H → H
hfgs : ∀ y ∈ s, f y = g y
h_1 : f x = g x
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hex : x ∈ e.source
y : H
hy : y ∈ s ∩ e.source
⊢ g y = (↑e.toPartialEquiv : H → H) y
have rw : g y = f y
Tactic: rw [← hef hy, hfgs y hy.1]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
s : Set H
x : H
f g : H → H
hfgs : ∀ y ∈ s, f y = g y
h_1 : f x = g x
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hex : x ∈ e.source
y : H
hy : y ∈ s ∩ e.source
rw : g y = f y
⊢ g y = (↑e.toPartialEquiv : H → H) y
have rw₁ : g y = g y
Tactic: rw [← hef hy, hfgs y hy.1]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
s : Set H
x : H
f : H → H
e' : OpenPartialHomeomorph H H
he'G : e' ∈ G
h_1 : s ⊆ f ⁻¹' e'.source
hfx : f x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s
⊢ ∃ e ∈ G, EqOn ((↑e' : H → H) ∘ f) (↑e.toPartialEquiv : H → H) (s ∩ e.source) ∧ x ∈ e.source
have rcases : ∀ (e : OpenPartialHomeomorph H H) (heG : e ∈ G) (hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source))
  (hex : x ∈ e.source), ∃ e ∈ G, EqOn ((↑e' : H → H) ∘ f) (↑e.toPartialEquiv : H → H) (s ∩ e.source) ∧ x ∈ e.source
Tactic: rcases h hx with ⟨e, heG, hef, hex⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
s : Set H
x : H
f : H → H
e' : OpenPartialHomeomorph H H
he'G : e' ∈ G
h_1 : s ⊆ f ⁻¹' e'.source
hfx : f x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hex : x ∈ e.source
⊢ ∃ e ∈ G, EqOn ((↑e' : H → H) ∘ f) (↑e.toPartialEquiv : H → H) (s ∩ e.source) ∧ x ∈ e.source
have refine_1 : EqOn ((↑e' : H → H) ∘ f) (↑(e ≫ₕ e').toPartialEquiv : H → H) (s ∩ (e ≫ₕ e').source)
Tactic: refine ⟨e.trans e', G.trans heG he'G, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
s : Set H
x : H
f : H → H
e' : OpenPartialHomeomorph H H
he'G : e' ∈ G
h_1 : s ⊆ f ⁻¹' e'.source
hfx : f x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hex : x ∈ e.source
refine_1 : EqOn ((↑e' : H → H) ∘ f) (↑(e ≫ₕ e').toPartialEquiv : H → H) (s ∩ (e ≫ₕ e').source)
⊢ ∃ e ∈ G, EqOn ((↑e' : H → H) ∘ f) (↑e.toPartialEquiv : H → H) (s ∩ e.source) ∧ x ∈ e.source
have refine_2 : x ∈ (e ≫ₕ e').source
Tactic: refine ⟨e.trans e', G.trans heG he'G, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (hypothesis)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
s : Set H
x : H
f : H → H
e' : OpenPartialHomeomorph H H
he'G : e' ∈ G
h_1 : s ⊆ f ⁻¹' e'.source
hfx : f x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hex : x ∈ e.source
y : H
hy : y ∈ s ∩ (e ≫ₕ e').source
⊢ ((↑e' : H → H) ∘ f) y = (↑(e ≫ₕ e').toPartialEquiv : H → H) y
have hy₁ : y ∈ s ∧ y ∈ e.source ∧ (↑e : H → H) y ∈ e'.source
Tactic: simp only [mfld_simps] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
⊢ G.IsLocalStructomorphWithinAt (↑f : H → H) s x ↔
    x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source
have mp : G.IsLocalStructomorphWithinAt (↑f : H → H) s x →
  x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
mp :
  G.IsLocalStructomorphWithinAt (↑f : H → H) s x →
    x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source
⊢ G.IsLocalStructomorphWithinAt (↑f : H → H) s x ↔
    x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source
have mpr : (x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source) →
  G.IsLocalStructomorphWithinAt (↑f : H → H) s x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
hf : G.IsLocalStructomorphWithinAt (↑f : H → H) s x
h2x : x ∈ s
⊢ ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source
have mp : ∀ (e : OpenPartialHomeomorph H H) (he : e ∈ G) (hfe : EqOn (↑f : H → H) (↑e.toPartialEquiv : H → H) (s ∩ e.source))
  (hxe : x ∈ e.source), ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source
Tactic: obtain ⟨e, he, hfe, hxe⟩ := hf h2x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
hf : G.IsLocalStructomorphWithinAt (↑f : H → H) s x
h2x : x ∈ s
e : OpenPartialHomeomorph H H
he : e ∈ G
hfe : EqOn (↑f : H → H) (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hxe : x ∈ e.source
⊢ ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source
have mp : (e.restr f.source).source ⊆ f.source
Tactic: refine ⟨e.restr f.source, closedUnderRestriction' he f.open_source, ?_, ?_, hxe, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
hf : G.IsLocalStructomorphWithinAt (↑f : H → H) s x
h2x : x ∈ s
e : OpenPartialHomeomorph H H
he : e ∈ G
hfe : EqOn (↑f : H → H) (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hxe : x ∈ e.source
mp : (e.restr f.source).source ⊆ f.source
⊢ ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source
have mp₁ : EqOn (↑f : H → H) (↑(e.restr f.source) : H → H) (s ∩ (e.restr f.source).source)
Tactic: refine ⟨e.restr f.source, closedUnderRestriction' he f.open_source, ?_, ?_, hxe, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
hf : G.IsLocalStructomorphWithinAt (↑f : H → H) s x
h2x : x ∈ s
e : OpenPartialHomeomorph H H
he : e ∈ G
hfe : EqOn (↑f : H → H) (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hxe : x ∈ e.source
mp : (e.restr f.source).source ⊆ f.source
mp₁ : EqOn (↑f : H → H) (↑(e.restr f.source) : H → H) (s ∩ (e.restr f.source).source)
⊢ ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source
have mp₂ : x ∈ interior f.source
Tactic: refine ⟨e.restr f.source, closedUnderRestriction' he f.open_source, ?_, ?_, hxe, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
hf : G.IsLocalStructomorphWithinAt (↑f : H → H) s x
h2x : x ∈ s
e : OpenPartialHomeomorph H H
he : e ∈ G
hfe : EqOn (↑f : H → H) (↑e.toPartialEquiv : H → H) (s ∩ e.source)
hxe : x ∈ e.source
⊢ x ∈ interior f.source
have mp : x ∈ f.source
Tactic: rw [f.open_source.interior_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx_1 : x ∈ f.source ∪ sᶜ
hf : x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source
hx : x ∈ s
⊢ ∃ e ∈ G, EqOn (↑f : H → H) (↑e.toPartialEquiv : H → H) (s ∩ e.source) ∧ x ∈ e.source
have mpr : ∀ (e : OpenPartialHomeomorph H H) (he : e ∈ G),
  e.source ⊆ f.source →
    ∀ (hfe : EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source)) (hxe : x ∈ e.source),
      ∃ e ∈ G, EqOn (↑f : H → H) (↑e.toPartialEquiv : H → H) (s ∩ e.source) ∧ x ∈ e.source
Tactic: obtain ⟨e, he, _, hfe, hxe⟩ := hf hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hs : f.source ⊆ s
hx : x ∈ f.source ∪ sᶜ
⊢ G.IsLocalStructomorphWithinAt (↑f : H → H) s x ↔
    x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) e.source ∧ x ∈ e.source
have rw : (x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source) ↔
  x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) e.source ∧ x ∈ e.source
Tactic: rw [f.isLocalStructomorphWithinAt_iff hx]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hs : f.source ⊆ s
hx : x ∈ f.source ∪ sᶜ
⊢ (x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source) ↔
    x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) e.source ∧ x ∈ e.source
have refine : x ∈ s →
  ∀ e ∈ G,
    e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source ↔
      e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) e.source ∧ x ∈ e.source
Tactic: refine imp_congr_right fun _ ↦ exists_congr fun e ↦ and_congr_right fun _ ↦ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hs : f.source ⊆ s
hx : x ∈ f.source ∪ sᶜ
h : x ∈ s
e : OpenPartialHomeomorph H H
h_1 : e ∈ G
⊢ e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source ↔
    e.source ⊆ f.source ∧ EqOn (↑f : H → H) (↑e : H → H) e.source ∧ x ∈ e.source
have refine : ∀ (h2e : e.source ⊆ f.source),
  EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source ↔ EqOn (↑f : H → H) (↑e : H → H) e.source ∧ x ∈ e.source
Tactic: refine and_congr_right fun h2e ↦ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hs : f.source ⊆ s
hx : x ∈ f.source ∪ sᶜ
h : x ∈ s
e : OpenPartialHomeomorph H H
h_1 : e ∈ G
h2e : e.source ⊆ f.source
⊢ EqOn (↑f : H → H) (↑e : H → H) (s ∩ e.source) ∧ x ∈ e.source ↔ EqOn (↑f : H → H) (↑e : H → H) e.source ∧ x ∈ e.source
have rw : EqOn (↑f : H → H) (↑e : H → H) e.source ∧ x ∈ e.source ↔ EqOn (↑f : H → H) (↑e : H → H) e.source ∧ x ∈ e.source
Tactic: rw [inter_eq_right.mpr (h2e.trans hs)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G : StructureGroupoid H
inst_1 : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
x : H
⊢ x ∈ f.source ∪ f.sourceᶜ
have simp_rw : Membership.mem (γ := Set H) univ x
Tactic: simp_rw [union_compl_self, mem_univ]
-- 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 : 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'
⊢ (e ≫ₕ f).symm ≫ₕ e' ≫ₕ f' ∈ G₁
have apply : ∀ x ∈ ((e ≫ₕ f).symm ≫ₕ e' ≫ₕ f').source,
  ∃ (s : Set H₁), IsOpen[inst] s ∧ x ∈ s ∧ ((e ≫ₕ f).symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁
Tactic: apply G₁.locality
-- 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 ∈ ((e ≫ₕ f).symm ≫ₕ e' ≫ₕ f').source
⊢ ∃ (s : Set H₁), IsOpen[inst] s ∧ x ∈ s ∧ ((e ≫ₕ f).symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁
have 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
Tactic: simp only [mfld_simps] at hx
Cleared hypotheses: hx
-- 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
⊢ ∃ (s : Set H₁), IsOpen[inst] s ∧ x ∈ s ∧ ((e ≫ₕ f).symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁
have hxs : x ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source
Tactic: have hxs : x ∈ f.symm ⁻¹' (e.symm ≫ₕ e').source := by simp only [hx, mfld_simps]
-- 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
⊢ ∃ (s : Set H₁), IsOpen[inst] s ∧ x ∈ s ∧ ((e ≫ₕ f).symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁
have hxs' : x ∈ f.target ∩ (↑f.symm : H₁ → H₂) ⁻¹' ((e.symm ≫ₕ e').source ∩ (↑(e.symm ≫ₕ e') : H₂ → H₂) ⁻¹' f'.source)
Tactic: have hxs' : x ∈ f.target ∩
          f.symm ⁻¹' ((e.symm ≫ₕ e').source ∩ e.symm ≫ₕ e' ⁻¹' f'.source) := by
        simp only [hx, mfld_simps]
-- 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)
⊢ ∃ (s : Set H₁), IsOpen[inst] s ∧ x ∈ s ∧ ((e ≫ₕ f).symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁
have obtain : ∀ (φ : OpenPartialHomeomorph H₁ H₁) (hφG₁ : φ ∈ G₁)
  (hφ :
    EqOn ((↑f' : H₂ → H₁) ∘ (↑(e.symm ≫ₕ e') : H₂ → H₂) ∘ (↑f.symm : H₁ → H₂)) (↑φ.toPartialEquiv : H₁ → H₁)
      ((↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source))
  (hφ_dom : x ∈ φ.source), ∃ (s : Set H₁), IsOpen[inst] s ∧ x ∈ s ∧ ((e ≫ₕ f).symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁
Tactic: obtain ⟨φ, hφG₁, hφ, hφ_dom⟩ := LocalInvariantProp.liftPropOn_indep_chart
        (isLocalStructomorphWithinAt_localInvariantProp G₁) (G₁.subset_maximalAtlas hf)
        (G₁.subset_maximalAtlas hf') (H _ (G₂.compatible he he')) hxs' hxs
-- 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φ :
  EqOn ((↑f' : H₂ → H₁) ∘ (↑(e.symm ≫ₕ e') : H₂ → H₂) ∘ (↑f.symm : H₁ → H₂)) (↑φ.toPartialEquiv : H₁ → H₁)
    ((↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)
hφ_dom : x ∈ φ.source
⊢ ∃ (s : Set H₁), IsOpen[inst] s ∧ x ∈ s ∧ ((e ≫ₕ f).symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁
have hφ₁ : EqOn (↑(f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f') : H₁ → H₁) (↑φ.toPartialEquiv : H₁ → H₁)
  ((↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)
Tactic: simp_rw [← OpenPartialHomeomorph.coe_trans, OpenPartialHomeomorph.trans_assoc] at hφ
Cleared hypotheses: hφ