[GOAL]
X✝ : Type u
Y : Type v
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x₀ x₁ : X✝
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ Group (FundamentalGroup X x)
[PROOFSTEP]
dsimp only [FundamentalGroup]
[GOAL]
X✝ : Type u
Y : Type v
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x₀ x₁ : X✝
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ Group (Aut x)
[PROOFSTEP]
infer_instance
[GOAL]
X✝ : Type u
Y : Type v
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x₀ x₁ : X✝
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ Inhabited (FundamentalGroup X x)
[PROOFSTEP]
dsimp only [FundamentalGroup]
[GOAL]
X✝ : Type u
Y : Type v
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x₀ x₁ : X✝
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ Inhabited (Aut x)
[PROOFSTEP]
infer_instance
