awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_5
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
K : Type u_6
inst_4 : NormedAddCommGroup K
inst_5 : InnerProductSpace 𝕜 K
inst_6 : CompleteSpace K
f g : H ≃ₗᵢ[𝕜] K
h_1 :
  ∃ (y : 𝕜), HSMul.hSMul (β := H →L[𝕜] H) y 1 = (↑(↑g : H ≃L[𝕜] K).symm : K →L[𝕜] H) ∘SL (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)
y : 𝕜
h : HSMul.hSMul (β := H →L[𝕜] H) y 1 = (↑(↑g : H ≃L[𝕜] K).symm : K →L[𝕜] H) ∘SL (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)
hy : y ≠ 0
hfg : (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K) = y • (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K)
⊢ (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K) = star y • (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)

Tactic:
have hgf : (g : H →L[𝕜] K) = star y • f := by
    ext x
    have := by simpa [map_smulₛₗ, ← ContinuousLinearEquiv.comp_coe, ← toContinuousLinearEquiv_symm,
      ← adjoint_eq_symm, ContinuousLinearMap.one_def] using congr(f (adjoint $h x)).symm
    simpa
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_5
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
K : Type u_6
inst_4 : NormedAddCommGroup K
inst_5 : InnerProductSpace 𝕜 K
inst_6 : CompleteSpace K
f g : H ≃ₗᵢ[𝕜] K
h_1 :
  ∃ (y : 𝕜), HSMul.hSMul (β := H →L[𝕜] H) y 1 = (↑(↑g : H ≃L[𝕜] K).symm : K →L[𝕜] H) ∘SL (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)
y : 𝕜
h : HSMul.hSMul (β := H →L[𝕜] H) y 1 = (↑(↑g : H ≃L[𝕜] K).symm : K →L[𝕜] H) ∘SL (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)
hy : y ≠ 0
hfg : (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K) = y • (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K)
hgf : (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K) = star y • (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)
⊢ (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K) =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜) y • (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K)

Tactic:
simp [← smul_smul, ← hfg, ← star_def, ← hgf]

Premises used: RCLike.star_def, smul_smul
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_5
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
K : Type u_6
inst_4 : NormedAddCommGroup K
inst_5 : InnerProductSpace 𝕜 K
inst_6 : CompleteSpace K
f g : H ≃ₗᵢ[𝕜] K
h_1 :
  ∃ (y : 𝕜), HSMul.hSMul (β := H →L[𝕜] H) y 1 = (↑(↑g : H ≃L[𝕜] K).symm : K →L[𝕜] H) ∘SL (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)
y : 𝕜
h : HSMul.hSMul (β := H →L[𝕜] H) y 1 = (↑(↑g : H ≃L[𝕜] K).symm : K →L[𝕜] H) ∘SL (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)
hy : y ≠ 0
hfg : (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K) = y • (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K)
hgf : (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K) = star y • (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)
⊢ (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K) =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜) y • (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K)

Tactic:
have : (g : H →L[𝕜] K) = (starRingEnd 𝕜 y * y) • g := by
    simp [← smul_smul, ← hfg, ← star_def, ← hgf]
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_5
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
K : Type u_6
inst_4 : NormedAddCommGroup K
inst_5 : InnerProductSpace 𝕜 K
inst_6 : CompleteSpace K
f g : H ≃ₗᵢ[𝕜] K
h_1 :
  ∃ (y : 𝕜), HSMul.hSMul (β := H →L[𝕜] H) y 1 = (↑(↑g : H ≃L[𝕜] K).symm : K →L[𝕜] H) ∘SL (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)
y : 𝕜
h : HSMul.hSMul (β := H →L[𝕜] H) y 1 = (↑(↑g : H ≃L[𝕜] K).symm : K →L[𝕜] H) ∘SL (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)
hy : y ≠ 0
hfg : (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K) = y • (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K)
hgf : (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K) = star y • (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)
this :
  (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K) =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜) y • (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K)
⊢ HSMul.hSMul (α := 𝕜) 1 (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K) =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜) y • (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K)

Tactic:
nth_rw 1 [← one_smul 𝕜 (g : H →L[𝕜] K)] at this

Premises used: one_smul, LinearIsometryEquiv.toContinuousLinearEquiv, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_5
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
K : Type u_6
inst_4 : NormedAddCommGroup K
inst_5 : InnerProductSpace 𝕜 K
inst_6 : CompleteSpace K
f g : H ≃ₗᵢ[𝕜] K
h_1 :
  ∃ (y : 𝕜), HSMul.hSMul (β := H →L[𝕜] H) y 1 = (↑(↑g : H ≃L[𝕜] K).symm : K →L[𝕜] H) ∘SL (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)
y : 𝕜
h : HSMul.hSMul (β := H →L[𝕜] H) y 1 = (↑(↑g : H ≃L[𝕜] K).symm : K →L[𝕜] H) ∘SL (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)
hy : y ≠ 0
hfg : (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K) = y • (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K)
hgf : (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K) = star y • (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)
this :
  HSMul.hSMul (α := 𝕜) 1 (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K) =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜) y • (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K)
⊢ HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜) y = 1 ∨ (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K) = 0

Tactic:
rw [← sub_eq_zero, ← sub_smul, smul_eq_zero, sub_eq_zero, eq_comm] at this

Premises used: sub_eq_zero, sub_smul, eq_comm, smul_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_5
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
K : Type u_6
inst_4 : NormedAddCommGroup K
inst_5 : InnerProductSpace 𝕜 K
inst_6 : CompleteSpace K
f g : H ≃ₗᵢ[𝕜] K
h_1 :
  ∃ (y : 𝕜), HSMul.hSMul (β := H →L[𝕜] H) y 1 = (↑(↑g : H ≃L[𝕜] K).symm : K →L[𝕜] H) ∘SL (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)
y : 𝕜
h : HSMul.hSMul (β := H →L[𝕜] H) y 1 = (↑(↑g : H ≃L[𝕜] K).symm : K →L[𝕜] H) ∘SL (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)
hy : y ≠ 0
hfg : (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K) = y • (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K)
hgf : (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K) = star y • (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)
this : HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜) y = 1 ∨ (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K) = 0
neg :
  ∀ (this : HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜) y = 1),
    ∃ (α : ↥(unitary 𝕜)), ∀ (x : H), Eq.{u_6 + 1} (α := K) ((f : (a : H) → K) x : K) ((α • g : (a : H) → K) x : K)
neg₁ :
  ∀ (this : (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K) = 0),
    ∃ (α : ↥(unitary 𝕜)), ∀ (x : H), Eq.{u_6 + 1} (α := K) ((f : (a : H) → K) x : K) ((α • g : (a : H) → K) x : K)
⊢ ∃ (α : ↥(unitary 𝕜)), ∀ (x : H), Eq.{u_6 + 1} (α := K) ((f : (a : H) → K) x : K) ((α • g : (a : H) → K) x : K)

Tactic:
obtain (this | this) := this
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_5
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
K : Type u_6
inst_4 : NormedAddCommGroup K
inst_5 : InnerProductSpace 𝕜 K
inst_6 : CompleteSpace K
f g : H ≃ₗᵢ[𝕜] K
h_1 :
  ∃ (y : 𝕜), HSMul.hSMul (β := H →L[𝕜] H) y 1 = (↑(↑g : H ≃L[𝕜] K).symm : K →L[𝕜] H) ∘SL (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)
y : 𝕜
h : HSMul.hSMul (β := H →L[𝕜] H) y 1 = (↑(↑g : H ≃L[𝕜] K).symm : K →L[𝕜] H) ∘SL (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)
hy : y ≠ 0
hfg : (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K) = y • (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K)
hgf : (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K) = star y • (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)
this : HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜) y = 1
⊢ Membership.mem (γ := Submonoid 𝕜) (unitary 𝕜) y

Tactic:
simp [Unitary.mem_iff, this, mul_comm y]

Premises used: mul_comm, Unitary.mem_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_5
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
K : Type u_6
inst_4 : NormedAddCommGroup K
inst_5 : InnerProductSpace 𝕜 K
inst_6 : CompleteSpace K
f g : H ≃ₗᵢ[𝕜] K
h_1 :
  ∃ (y : 𝕜), HSMul.hSMul (β := H →L[𝕜] H) y 1 = (↑(↑g : H ≃L[𝕜] K).symm : K →L[𝕜] H) ∘SL (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)
y : 𝕜
h : HSMul.hSMul (β := H →L[𝕜] H) y 1 = (↑(↑g : H ≃L[𝕜] K).symm : K →L[𝕜] H) ∘SL (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)
hy : y ≠ 0
hfg : (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K) = y • (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K)
hgf : (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K) = star y • (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)
this : HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜) y = 1
⊢ ∃ (α : ↥(unitary 𝕜)), ∀ (x : H), Eq.{u_6 + 1} (α := K) ((f : (a : H) → K) x : K) ((α • g : (a : H) → K) x : K)

Tactic:
exact ⟨⟨y, by simp [Unitary.mem_iff, this, mul_comm y]⟩, fun x ↦ congr($hfg x)⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_5
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
K : Type u_6
inst_4 : NormedAddCommGroup K
inst_5 : InnerProductSpace 𝕜 K
inst_6 : CompleteSpace K
f g : H ≃ₗᵢ[𝕜] K
h_1 :
  ∃ (y : 𝕜), HSMul.hSMul (β := H →L[𝕜] H) y 1 = (↑(↑g : H ≃L[𝕜] K).symm : K →L[𝕜] H) ∘SL (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)
y : 𝕜
h : HSMul.hSMul (β := H →L[𝕜] H) y 1 = (↑(↑g : H ≃L[𝕜] K).symm : K →L[𝕜] H) ∘SL (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)
hy : y ≠ 0
hfg : (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K) = y • (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K)
hgf : (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K) = star y • (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)
this : (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K) = 0
x : H
⊢ x = 0

Tactic:
simpa using congr($this x)
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_5
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
K : Type u_6
inst_4 : NormedAddCommGroup K
inst_5 : InnerProductSpace 𝕜 K
inst_6 : CompleteSpace K
f g : H ≃ₗᵢ[𝕜] K
h_1 :
  ∃ (y : 𝕜), HSMul.hSMul (β := H →L[𝕜] H) y 1 = (↑(↑g : H ≃L[𝕜] K).symm : K →L[𝕜] H) ∘SL (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)
y : 𝕜
h : HSMul.hSMul (β := H →L[𝕜] H) y 1 = (↑(↑g : H ≃L[𝕜] K).symm : K →L[𝕜] H) ∘SL (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)
hy : y ≠ 0
hfg : (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K) = y • (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K)
hgf : (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K) = star y • (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)
this : (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K) = 0
⊢ ∃ (α : ↥(unitary 𝕜)), ∀ (x : H), Eq.{u_6 + 1} (α := K) ((f : (a : H) → K) x : K) ((α • g : (a : H) → K) x : K)

Tactic:
exact ⟨1, fun x ↦ by simp [by simpa using congr($this x)]⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_5
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
u : ↥(unitary (H →L[𝕜] H))
x : H
⊢ norm (E := H) (((↑u : H →L[𝕜] H) : (a : H) → H) x : H) = ‖x‖

Tactic:
u.val.norm_map_of_mem_unitary u.property x

Premises used: ContinuousLinearMap.norm_map_of_mem_unitary, Subtype.property
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_5
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
u : ↥(unitary (H →L[𝕜] H))
x y : H
⊢ inner 𝕜 (E := H) (((↑u : H →L[𝕜] H) : (a : H) → H) x : H) (((↑u : H →L[𝕜] H) : (a : H) → H) y : H) = ⟪x, y⟫_𝕜

Tactic:
u.val.inner_map_map_of_mem_unitary u.property x y

Premises used: ContinuousLinearMap.inner_map_map_of_mem_unitary, Subtype.property
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedAddCommGroup G
inst_4 : InnerProductSpace 𝕜 E
inst_5 : InnerProductSpace 𝕜 F
inst_6 : InnerProductSpace 𝕜 G
H : Type u_5
inst_7 : NormedAddCommGroup H
inst_8 : InnerProductSpace 𝕜 H
inst_9 : CompleteSpace H
e : H ≃ₗᵢ[𝕜] H
h :
  ∀ (x : H),
    Eq (α := H) (((↑(↑e : H ≃L[𝕜] H) : H →L[𝕜] H) * (↑(↑e.symm : H ≃L[𝕜] H) : H →L[𝕜] H) : (a : H) → H) x : H)
      ((1 : (a : H) → H) x : H)
⊢ (↑(↑e : H ≃L[𝕜] H) : H →L[𝕜] H) * (↑(↑e.symm : H ≃L[𝕜] H) : H →L[𝕜] H) = 1

Tactic:
ext
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedAddCommGroup G
inst_4 : InnerProductSpace 𝕜 E
inst_5 : InnerProductSpace 𝕜 F
inst_6 : InnerProductSpace 𝕜 G
H : Type u_5
inst_7 : NormedAddCommGroup H
inst_8 : InnerProductSpace 𝕜 H
inst_9 : CompleteSpace H
e : H ≃ₗᵢ[𝕜] H
x : H
⊢ Eq (α := H) (((↑(↑e : H ≃L[𝕜] H) : H →L[𝕜] H) * (↑(↑e.symm : H ≃L[𝕜] H) : H →L[𝕜] H) : (a : H) → H) x : H)
    ((1 : (a : H) → H) x : H)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedAddCommGroup G
inst_4 : InnerProductSpace 𝕜 E
inst_5 : InnerProductSpace 𝕜 F
inst_6 : InnerProductSpace 𝕜 G
H : Type u_5
inst_7 : NormedAddCommGroup H
inst_8 : InnerProductSpace 𝕜 H
inst_9 : CompleteSpace H
e : H ≃ₗᵢ[𝕜] H
h :
  ∀ (x : H),
    Eq (α := H) (((↑(↑e.symm : H ≃L[𝕜] H) : H →L[𝕜] H) * (↑(↑e : H ≃L[𝕜] H) : H →L[𝕜] H) : (a : H) → H) x : H)
      ((1 : (a : H) → H) x : H)
⊢ (↑(↑e.symm : H ≃L[𝕜] H) : H →L[𝕜] H) * (↑(↑e : H ≃L[𝕜] H) : H →L[𝕜] H) = 1

Tactic:
ext
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedAddCommGroup G
inst_4 : InnerProductSpace 𝕜 E
inst_5 : InnerProductSpace 𝕜 F
inst_6 : InnerProductSpace 𝕜 G
H : Type u_5
inst_7 : NormedAddCommGroup H
inst_8 : InnerProductSpace 𝕜 H
inst_9 : CompleteSpace H
e : H ≃ₗᵢ[𝕜] H
x : H
⊢ Eq (α := H) (((↑(↑e.symm : H ≃L[𝕜] H) : H →L[𝕜] H) * (↑(↑e : H ≃L[𝕜] H) : H →L[𝕜] H) : (a : H) → H) x : H)
    ((1 : (a : H) → H) x : H)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedAddCommGroup G
inst_4 : InnerProductSpace 𝕜 E
inst_5 : InnerProductSpace 𝕜 F
inst_6 : InnerProductSpace 𝕜 G
H : Type u_5
inst_7 : NormedAddCommGroup H
inst_8 : InnerProductSpace 𝕜 H
inst_9 : CompleteSpace H
e : H ≃ₗᵢ[𝕜] H
e' : (H →L[𝕜] H)ˣ :=
  { val := (↑(↑e : H ≃L[𝕜] H) : H →L[𝕜] H), inv := (↑(↑e.symm : H ≃L[𝕜] H) : H →L[𝕜] H), val_inv := ⋯, inv_val := ⋯ }
⊢ Membership.mem (γ := Submonoid (H →L[𝕜] H)) (unitary (H →L[𝕜] H)) (↑(↑e : H ≃L[𝕜] H) : H →L[𝕜] H)

Tactic:
IsUnit.mem_unitary_of_star_mul_self ⟨e', rfl⟩ <|
          (e : H →L[𝕜] H).norm_map_iff_adjoint_comp_self.mp e.norm_map

Premises used: LinearIsometryEquiv.norm_map, IsUnit.mem_unitary_of_star_mul_self, Exists.intro, Iff.mp, LinearIsometryEquiv.toContinuousLinearEquiv, ContinuousLinearMap.norm_map_iff_adjoint_comp_self, rfl, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedAddCommGroup G
inst_4 : InnerProductSpace 𝕜 E
inst_5 : InnerProductSpace 𝕜 F
inst_6 : InnerProductSpace 𝕜 G
H : Type u_5
inst_7 : NormedAddCommGroup H
inst_8 : InnerProductSpace 𝕜 H
inst_9 : CompleteSpace H
e : H ≃ₗᵢ[𝕜] H
e' : (H →L[𝕜] H)ˣ :=
  { val := (↑(↑e : H ≃L[𝕜] H) : H →L[𝕜] H), inv := (↑(↑e.symm : H ≃L[𝕜] H) : H →L[𝕜] H), val_inv := ⋯, inv_val := ⋯ }
⊢ Membership.mem (γ := Submonoid (H →L[𝕜] H)) (unitary (H →L[𝕜] H)) (↑(↑e : H ≃L[𝕜] H) : H →L[𝕜] H)

Tactic:
exact IsUnit.mem_unitary_of_star_mul_self ⟨e', rfl⟩ <|
          (e : H →L[𝕜] H).norm_map_iff_adjoint_comp_self.mp e.norm_map

Premises used: LinearIsometryEquiv.norm_map, IsUnit.mem_unitary_of_star_mul_self, Exists.intro, Iff.mp, LinearIsometryEquiv.toContinuousLinearEquiv, ContinuousLinearMap.norm_map_iff_adjoint_comp_self, rfl, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedAddCommGroup G
inst_4 : InnerProductSpace 𝕜 E
inst_5 : InnerProductSpace 𝕜 F
inst_6 : InnerProductSpace 𝕜 G
H : Type u_5
inst_7 : NormedAddCommGroup H
inst_8 : InnerProductSpace 𝕜 H
inst_9 : CompleteSpace H
u v : ↥(unitary (H →L[𝕜] H))
h :
  ∀ (x : H),
    Eq (α := H)
      ((let __src := (↑(u * v) : H →L[𝕜] H);
            { toLinearMap := (↑__src : H →ₗ[𝕜] H),
              invFun := (⇑(↑(↑(star (u * v)) : H →L[𝕜] H) : H →ₜ+ H) : (a : H) → H), left_inv := ⋯, right_inv := ⋯,
              norm_map' := ⋯ } :
            (a : H) → H)
          x :
        H)
      ((HMul.hMul (α := H ≃ₗᵢ[𝕜] H)
              (let __src := (↑u : H →L[𝕜] H);
              { toLinearMap := (↑__src : H →ₗ[𝕜] H), invFun := (⇑(↑(↑(star u) : H →L[𝕜] H) : H →ₜ+ H) : (a : H) → H),
                left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ : H ≃ₗᵢ[𝕜] H })
              (let __src := (↑v : H →L[𝕜] H);
              { toLinearMap := (↑__src : H →ₗ[𝕜] H), invFun := (⇑(↑(↑(star v) : H →L[𝕜] H) : H →ₜ+ H) : (a : H) → H),
                left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ : H ≃ₗᵢ[𝕜] H }) :
            (a : H) → H)
          x :
        H)
⊢ (let __src := (↑(u * v) : H →L[𝕜] H);
    { toLinearMap := (↑__src : H →ₗ[𝕜] H), invFun := (⇑(↑(↑(star (u * v)) : H →L[𝕜] H) : H →ₜ+ H) : (a : H) → H),
      left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ }) =
    HMul.hMul (α := H ≃ₗᵢ[𝕜] H)
      (let __src := (↑u : H →L[𝕜] H);
      { toLinearMap := (↑__src : H →ₗ[𝕜] H), invFun := (⇑(↑(↑(star u) : H →L[𝕜] H) : H →ₜ+ H) : (a : H) → H),
        left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ : H ≃ₗᵢ[𝕜] H })
      (let __src := (↑v : H →L[𝕜] H);
      { toLinearMap := (↑__src : H →ₗ[𝕜] H), invFun := (⇑(↑(↑(star v) : H →L[𝕜] H) : H →ₜ+ H) : (a : H) → H),
        left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ : H ≃ₗᵢ[𝕜] H })

Tactic:
ext
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedAddCommGroup G
inst_4 : InnerProductSpace 𝕜 E
inst_5 : InnerProductSpace 𝕜 F
inst_6 : InnerProductSpace 𝕜 G
H : Type u_5
inst_7 : NormedAddCommGroup H
inst_8 : InnerProductSpace 𝕜 H
inst_9 : CompleteSpace H
u v : ↥(unitary (H →L[𝕜] H))
x : H
⊢ Eq (α := H)
    ((let __src := (↑(u * v) : H →L[𝕜] H);
          { toLinearMap := (↑__src : H →ₗ[𝕜] H), invFun := (⇑(↑(↑(star (u * v)) : H →L[𝕜] H) : H →ₜ+ H) : (a : H) → H),
            left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ } :
          (a : H) → H)
        x :
      H)
    ((HMul.hMul (α := H ≃ₗᵢ[𝕜] H)
            (let __src := (↑u : H →L[𝕜] H);
            { toLinearMap := (↑__src : H →ₗ[𝕜] H), invFun := (⇑(↑(↑(star u) : H →L[𝕜] H) : H →ₜ+ H) : (a : H) → H),
              left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ : H ≃ₗᵢ[𝕜] H })
            (let __src := (↑v : H →L[𝕜] H);
            { toLinearMap := (↑__src : H →ₗ[𝕜] H), invFun := (⇑(↑(↑(star v) : H →L[𝕜] H) : H →ₜ+ H) : (a : H) → H),
              left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ : H ≃ₗᵢ[𝕜] H }) :
          (a : H) → H)
        x :
      H)

Tactic:
rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_5
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
u : ↥(unitary (H →L[𝕜] H))
⊢ (↑(↑((linearIsometryEquiv : (a : ↥(unitary (H →L[𝕜] H))) → H ≃ₗᵢ[𝕜] H) u) : H ≃L[𝕜] H) : H →L[𝕜] H) = (↑u : H →L[𝕜] H)

Tactic:
rfl

Premises used: rfl, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_5
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
e : H ≃ₗᵢ[𝕜] H
⊢ (↑((MulEquiv.symm linearIsometryEquiv : (a : H ≃ₗᵢ[𝕜] H) → ↥(unitary (H →L[𝕜] H))) e) : H →L[𝕜] H) =
    (↑(↑e : H ≃L[𝕜] H) : H →L[𝕜] H)

Tactic:
rfl

Premises used: rfl, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_5
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
u : ↥(unitary (H →L[𝕜] H))
⊢ Eq.{u_5 + 1} (α := (H →L[𝕜] H) ≃⋆ₐ[𝕜] H →L[𝕜] H)
    (LinearIsometryEquiv.conjStarAlgEquiv ((linearIsometryEquiv : (a : ↥(unitary (H →L[𝕜] H))) → H ≃ₗᵢ[𝕜] H) u))
    ((conjStarAlgAut 𝕜 (H →L[𝕜] H) : (a : ↥(unitary (H →L[𝕜] H))) → (H →L[𝕜] H) ≃⋆ₐ[𝕜] H →L[𝕜] H) u)

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, LinearIsometryEquiv.conjStarAlgEquiv, LinearMap.mkContinuousOfExistsBound, Classical.choose, MulSemiringAction.toRingEquiv, StarAlgEquiv.ofAlgEquiv, rfl, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_5
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
u : H ≃ₗᵢ[𝕜] H
⊢ Eq (α := (H →L[𝕜] H) ≃⋆ₐ[𝕜] H →L[𝕜] H)
    ((conjStarAlgAut 𝕜 (H →L[𝕜] H) : (a : ↥(unitary (H →L[𝕜] H))) → (H →L[𝕜] H) ≃⋆ₐ[𝕜] H →L[𝕜] H)
        ((MulEquiv.symm linearIsometryEquiv : (a : H ≃ₗᵢ[𝕜] H) → ↥(unitary (H →L[𝕜] H))) u) :
      (H →L[𝕜] H) ≃⋆ₐ[𝕜] H →L[𝕜] H)
    (u.conjStarAlgEquiv : (H →L[𝕜] H) ≃⋆ₐ[𝕜] H →L[𝕜] H)

Tactic:
simp [← conjStarAlgEquiv_unitaryLinearIsometryEquiv]

Premises used: Unitary.conjStarAlgEquiv_unitaryLinearIsometryEquiv
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
m : Type u_5
n : Type u_6
inst_5 : Fintype m
inst_6 : DecidableEq m
inst_7 : Fintype n
inst_8 : DecidableEq n
inst_9 : FiniteDimensional 𝕜 E
inst_10 : FiniteDimensional 𝕜 F
v₁ : OrthonormalBasis n 𝕜 E
v₂ : OrthonormalBasis m 𝕜 F
A : Matrix m n 𝕜
⊢ Eq (α := F →ₗ[𝕜] E) ((toLin v₂.toBasis v₁.toBasis : (a : Matrix n m 𝕜) → F →ₗ[𝕜] E) Aᴴ : F →ₗ[𝕜] E)
    ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) ((toLin v₁.toBasis v₂.toBasis : (a : Matrix m n 𝕜) → E →ₗ[𝕜] F) A) :
      F →ₗ[𝕜] E)

Tactic:
eq_adjoint_iff_basis v₂.toBasis v₁.toBasis _ _ |>.mpr fun i j ↦ ?_

Premises used: Iff.mpr, LinearMap.eq_adjoint_iff_basis, OrthonormalBasis.toBasis
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
m : Type u_5
n : Type u_6
inst_5 : Fintype m
inst_6 : DecidableEq m
inst_7 : Fintype n
inst_8 : DecidableEq n
inst_9 : FiniteDimensional 𝕜 E
inst_10 : FiniteDimensional 𝕜 F
v₁ : OrthonormalBasis n 𝕜 E
v₂ : OrthonormalBasis m 𝕜 F
A : Matrix m n 𝕜
refine :
  ∀ (i : m) (j : n),
    inner.{u_1, u_2} 𝕜 (E := E)
        ((((toLin v₂.toBasis v₁.toBasis : (a : Matrix n m 𝕜) → F →ₗ[𝕜] E) Aᴴ : F →ₗ[𝕜] E) : (a : F) → E)
            ((v₂.toBasis : (a : m) → F) i : F) :
          E)
        ((v₁.toBasis : (a : n) → E) j : E) =
      inner.{u_1, u_3} 𝕜 (E := F) ((v₂.toBasis : (a : m) → F) i : F)
        ((((toLin v₁.toBasis v₂.toBasis : (a : Matrix m n 𝕜) → E →ₗ[𝕜] F) A : E →ₗ[𝕜] F) : (a : E) → F)
            ((v₁.toBasis : (a : n) → E) j : E) :
          F)
⊢ Eq (α := F →ₗ[𝕜] E) ((toLin v₂.toBasis v₁.toBasis : (a : Matrix n m 𝕜) → F →ₗ[𝕜] E) Aᴴ : F →ₗ[𝕜] E)
    ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) ((toLin v₁.toBasis v₂.toBasis : (a : Matrix m n 𝕜) → E →ₗ[𝕜] F) A) :
      F →ₗ[𝕜] E)

Tactic:
refine eq_adjoint_iff_basis v₂.toBasis v₁.toBasis _ _ |>.mpr fun i j ↦ ?_

Premises used: Iff.mpr, LinearMap.eq_adjoint_iff_basis, OrthonormalBasis.toBasis