-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem liftPropAt_symm_of_mem_maximalAtlas [HasGroupoid M G] {x : H}
    (hG : G.LocalInvariantProp G Q) (hQ : ∀ y, Q id univ y) (he : e ∈ maximalAtlas M G)
    (hx : x ∈ e.target) : LiftPropAt Q e.symm x

Proof state:
H : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst✝ : HasGroupoid M G
x : H
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
hx : x ∈ e.target
h : Q (↑e ∘ ↑e.symm) univ x
this : ↑e.symm x ∈ e.source
⊢ LiftPropAt Q (↑e.symm) x

Tactic:
rw [LiftPropAt, hG.liftPropWithinAt_indep_chart G.id_mem_maximalAtlas (mem_univ _) he this]

Result:
H : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst✝ : HasGroupoid M G
x : H
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
hx : x ∈ e.target
h : Q (↑e ∘ ↑e.symm) univ x
this : ↑e.symm x ∈ e.source
⊢ ContinuousWithinAt (↑e.symm) univ x ∧
    Q (↑e ∘ ↑e.symm ∘ ↑(PartialHomeomorph.refl H).symm) (↑(PartialHomeomorph.refl H).symm ⁻¹' univ)
      (↑(PartialHomeomorph.refl H) x)

Proof state:
H : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst✝ : HasGroupoid M G
x : H
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
hx : x ∈ e.target
h : Q (↑e ∘ ↑e.symm) univ x
this : ↑e.symm x ∈ e.source
⊢ ContinuousWithinAt (↑e.symm) univ x ∧
    Q (↑e ∘ ↑e.symm ∘ ↑(PartialHomeomorph.refl H).symm) (↑(PartialHomeomorph.refl H).symm ⁻¹' univ)
      (↑(PartialHomeomorph.refl H) x)

Tactic:
refine ⟨(e.symm.continuousAt hx).continuousWithinAt, ?_⟩

Result:
H : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst✝ : HasGroupoid M G
x : H
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
hx : x ∈ e.target
h : Q (↑e ∘ ↑e.symm) univ x
this : ↑e.symm x ∈ e.source
⊢ Q (↑e ∘ ↑e.symm ∘ ↑(PartialHomeomorph.refl H).symm) (↑(PartialHomeomorph.refl H).symm ⁻¹' univ)
    (↑(PartialHomeomorph.refl H) x)

Proof state:
H : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst✝ : HasGroupoid M G
x : H
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
hx : x ∈ e.target
h : Q (↑e ∘ ↑e.symm) univ x
⊢ ↑e.symm x ∈ e.source

Tactic:
simp only [hx, mfld_simps]

Result:
no goals

Proof state:
H : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst✝ : HasGroupoid M G
x : H
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
hx : x ∈ e.target
⊢ Q (↑e ∘ ↑e.symm) univ x

Tactic:
exact hG.congr' (e.eventually_right_inverse hx) (hQ x)

Result:
no goals

Proof state:
H : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst✝ : HasGroupoid M G
x : H
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
hx : x ∈ e.target
h : Q (↑e ∘ ↑e.symm) univ x
⊢ LiftPropAt Q (↑e.symm) x

Tactic:
have : e.symm x ∈ e.source := by simp only [hx, mfld_simps]

Result:
H : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst✝ : HasGroupoid M G
x : H
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
hx : x ∈ e.target
h : Q (↑e ∘ ↑e.symm) univ x
this : ↑e.symm x ∈ e.source
⊢ LiftPropAt Q (↑e.symm) x

Proof state:
H : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst✝ : HasGroupoid M G
x : H
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
hx : x ∈ e.target
h : Q (↑e ∘ ↑e.symm) univ x
this : ↑e.symm x ∈ e.source
⊢ Q (↑e ∘ ↑e.symm ∘ ↑(PartialHomeomorph.refl H).symm) (↑(PartialHomeomorph.refl H).symm ⁻¹' univ)
    (↑(PartialHomeomorph.refl H) x)

Tactic:
simp only [h, mfld_simps]

Result:
no goals

Proof state:
H : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst✝ : HasGroupoid M G
x : H
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
hx : x ∈ e.target
⊢ LiftPropAt Q (↑e.symm) x

Tactic:
suffices h : Q (e ∘ e.symm) univ x by
  have : e.symm x ∈ e.source := by simp only [hx, mfld_simps]
  rw [LiftPropAt, hG.liftPropWithinAt_indep_chart G.id_mem_maximalAtlas (mem_univ _) he this]
  refine ⟨(e.symm.continuousAt hx).continuousWithinAt, ?_⟩
  simp only [h, mfld_simps]

Result:
H : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
inst✝ : HasGroupoid M G
x : H
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
hx : x ∈ e.target
⊢ Q (↑e ∘ ↑e.symm) univ x