-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
@[simp]
lemma _root_.LinearIsometryEquiv.adjoint_eq_symm (e : H ≃ₗᵢ[𝕜] K) :
    adjoint (e : H →L[𝕜] K) = e.symm :=
  let e' := (e : H →L[𝕜] K)
  calc
    adjoint e' = adjoint e' ∘L (e' ∘L e.symm)

Proof state:
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
e : H ≃ₗᵢ[𝕜] K
e' : H →L[𝕜] K := ↑{ toLinearEquiv := e.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ (adjoint e').comp
      (e'.comp ↑{ toLinearEquiv := e.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }) =
    ↑{ toLinearEquiv := e.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Tactic:
rw [← comp_assoc, norm_map_iff_adjoint_comp_self e' |>.mp e.norm_map]

Result:
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
e : H ≃ₗᵢ[𝕜] K
e' : H →L[𝕜] K := ↑{ toLinearEquiv := e.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ comp 1 ↑{ toLinearEquiv := e.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ } =
    ↑{ toLinearEquiv := e.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Proof state:
case h.e'_3.h.e'_24.h
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
e : H ≃ₗᵢ[𝕜] K
e' : H →L[𝕜] K := ↑{ toLinearEquiv := e.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
x✝ : K
⊢ (e'.comp ↑{ toLinearEquiv := e.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }) x✝ = (id 𝕜 K) x✝

Tactic:
simp [e']

Result:
no goals

Proof state:
case h.e'_3.h.e'_24
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
e : H ≃ₗᵢ[𝕜] K
e' : H →L[𝕜] K := ↑{ toLinearEquiv := e.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ e'.comp ↑{ toLinearEquiv := e.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ } = id 𝕜 K

Tactic:
ext

Result:
case h.e'_3.h.e'_24.h
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
e : H ≃ₗᵢ[𝕜] K
e' : H →L[𝕜] K := ↑{ toLinearEquiv := e.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
x✝ : K
⊢ (e'.comp ↑{ toLinearEquiv := e.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }) x✝ = (id 𝕜 K) x✝

Proof state:
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
e : H ≃ₗᵢ[𝕜] K
e' : H →L[𝕜] K := ↑{ toLinearEquiv := e.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ adjoint e' =
    (adjoint e').comp
      (e'.comp ↑{ toLinearEquiv := e.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })

Tactic:
convert (adjoint e').comp_id.symm

Result:
case h.e'_3.h.e'_24
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
e : H ≃ₗᵢ[𝕜] K
e' : H →L[𝕜] K := ↑{ toLinearEquiv := e.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ e'.comp ↑{ toLinearEquiv := e.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ } = id 𝕜 K

Proof state:
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
e : H ≃ₗᵢ[𝕜] K
e' : H →L[𝕜] K := ↑{ toLinearEquiv := e.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ comp 1 ↑{ toLinearEquiv := e.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ } =
    ↑{ toLinearEquiv := e.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Tactic:
exact (e.symm : K →L[𝕜] H).id_comp

Result:
no goals