-- Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
theorem tangentMapWithin_id {p : TangentBundle I M} (hs : UniqueMDiffWithinAt I s p.proj) :
    tangentMapWithin I I (id : M → M) s p = p

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
p : TangentBundle I M
hs : UniqueMDiffWithinAt I s p.proj
⊢ { proj := p.proj, snd := (ContinuousLinearMap.id 𝕜 (TangentSpace I p.proj)) p.snd } = p

Tactic:
rcases p with ⟨⟩

Result:
case mk
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
proj✝ : M
snd✝ : TangentSpace I proj✝
hs : UniqueMDiffWithinAt I s { proj := proj✝, snd := snd✝ }.proj
⊢ { proj := { proj := proj✝, snd := snd✝ }.proj,
      snd :=
        (ContinuousLinearMap.id 𝕜 (TangentSpace I { proj := proj✝, snd := snd✝ }.proj))
          { proj := proj✝, snd := snd✝ }.snd } =
    { proj := proj✝, snd := snd✝ }

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
p : TangentBundle I M
hs : UniqueMDiffWithinAt I s p.proj
⊢ UniqueMDiffWithinAt I s p.proj

Tactic:
exact hs

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
p : TangentBundle I M
hs : UniqueMDiffWithinAt I s p.proj
⊢ { proj := p.proj, snd := (mfderivWithin I I id s p.proj) p.snd } = p

Tactic:
rw [mfderivWithin_id]

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
p : TangentBundle I M
hs : UniqueMDiffWithinAt I s p.proj
⊢ { proj := p.proj, snd := (ContinuousLinearMap.id 𝕜 (TangentSpace I p.proj)) p.snd } = p

𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
p : TangentBundle I M
hs : UniqueMDiffWithinAt I s p.proj
⊢ UniqueMDiffWithinAt I s p.proj

Proof state:
case mk
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
proj✝ : M
snd✝ : TangentSpace I proj✝
hs : UniqueMDiffWithinAt I s { proj := proj✝, snd := snd✝ }.proj
⊢ { proj := { proj := proj✝, snd := snd✝ }.proj,
      snd :=
        (ContinuousLinearMap.id 𝕜 (TangentSpace I { proj := proj✝, snd := snd✝ }.proj))
          { proj := proj✝, snd := snd✝ }.snd } =
    { proj := proj✝, snd := snd✝ }

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
p : TangentBundle I M
hs : UniqueMDiffWithinAt I s p.proj
⊢ tangentMapWithin I I id s p = p

Tactic:
simp only [tangentMapWithin, id]

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
p : TangentBundle I M
hs : UniqueMDiffWithinAt I s p.proj
⊢ { proj := p.proj, snd := (mfderivWithin I I id s p.proj) p.snd } = p