Theorem: unused_extendedChart_leftInverse' (Sard/ManifoldAux.lean)

State before:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
e : PartialHomeomorph M H
t : Set E
ht : t ⊆ ↑(e.extend I) '' e.source
⊢ ↑(e.extend I) ∘ ↑(e.extend I).symm '' t = t
Tactic:
sorry
State after:
no goals