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
e : H ≃ₗᵢ[𝕜] K
rw :
  comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) (↑(↑e : H ≃L[𝕜] K) : H →L[𝕜] K))
        (↑(↑e : H ≃L[𝕜] K) : H →L[𝕜] K) ∘SL
      (↑(↑e.symm : K ≃L[𝕜] H) : K →L[𝕜] H) =
    (↑(↑e.symm : K ≃L[𝕜] H) : K →L[𝕜] H)
rw₁ : comp (σ₂₃ := RingHom.id 𝕜) 1 (↑(↑e.symm : K ≃L[𝕜] H) : K →L[𝕜] H) = (↑(↑e.symm : K ≃L[𝕜] H) : K →L[𝕜] H)
rw₂ : ContinuousLinearMap.id 𝕜 H ∘SL (↑(↑e.symm : K ≃L[𝕜] H) : K →L[𝕜] H) = (↑(↑e.symm : K ≃L[𝕜] H) : K →L[𝕜] H)
rw₃ rw₄ : (↑(↑e.symm : K ≃L[𝕜] H) : K →L[𝕜] H) = (↑(↑e.symm : K ≃L[𝕜] H) : K →L[𝕜] H)
⊢ comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) (↑(↑e : H ≃L[𝕜] K) : H →L[𝕜] K))
      ((↑(↑e : H ≃L[𝕜] K) : H →L[𝕜] K) ∘SL (↑(↑e.symm : K ≃L[𝕜] H) : K →L[𝕜] H)) =
    (↑(↑e.symm : K ≃L[𝕜] H) : K →L[𝕜] H)

Tactic:
rw [← comp_assoc, norm_map_iff_adjoint_comp_self _ |>.mp e.norm_map, one_def, id_comp]

Premises used: ContinuousLinearMap.comp_assoc, Iff.mp, ContinuousLinearMap.id_comp, ContinuousLinearMap.norm_map_iff_adjoint_comp_self, ContinuousLinearMap.one_def
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_5
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
K : Type u_6
inst_3 : NormedAddCommGroup K
inst_4 : InnerProductSpace 𝕜 K
inst_5 : FiniteDimensional 𝕜 H
inst_6 : FiniteDimensional 𝕜 K
e : H ≃ₗᵢ[𝕜] K
⊢ (LinearMap.adjoint : (a : H →ₗ[𝕜] K) → K →ₗ[𝕜] H) (↑e.toLinearEquiv : H →ₗ[𝕜] K) = (↑e.symm.toLinearEquiv : K →ₗ[𝕜] H)

Tactic:
have := FiniteDimensional.complete 𝕜 H
  have := FiniteDimensional.complete 𝕜 K
  congr($e.adjoint_eq_symm)

Premises used: LinearIsometryEquiv.adjoint_eq_symm, congrArg, id, ContinuousLinearMap.toLinearMap, FiniteDimensional.complete
-- 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
⊢ star (↑(↑e : H ≃L[𝕜] H) : H →L[𝕜] H) = (↑(↑e.symm : H ≃L[𝕜] H) : H →L[𝕜] H)

Tactic:
e.adjoint_eq_symm

Premises used: LinearIsometryEquiv.adjoint_eq_symm
-- 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 →L[𝕜] H
hu : Membership.mem (γ := Submonoid (H →L[𝕜] H)) (unitary (H →L[𝕜] H)) u
x : H
⊢ norm (E := H) ((u : (a : H) → H) x : H) = ‖x‖

Tactic:
have := Unitary.star_mul_self_of_mem hu
  u.norm_map_iff_adjoint_comp_self.mpr this x

Premises used: Iff.mpr, Unitary.star_mul_self_of_mem, ContinuousLinearMap.norm_map_iff_adjoint_comp_self
-- 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 →L[𝕜] H
hu : Membership.mem (γ := Submonoid (H →L[𝕜] H)) (unitary (H →L[𝕜] H)) u
x y : H
⊢ inner 𝕜 (E := H) ((u : (a : H) → H) x : H) ((u : (a : H) → H) y : H) = ⟪x, y⟫_𝕜

Tactic:
have := Unitary.star_mul_self_of_mem hu
  u.inner_map_map_iff_adjoint_comp_self.mpr this x y

Premises used: Iff.mpr, Unitary.star_mul_self_of_mem, ContinuousLinearMap.inner_map_map_iff_adjoint_comp_self
-- 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
K : Type u_6
inst_10 : NormedAddCommGroup K
inst_11 : InnerProductSpace 𝕜 K
inst_12 : CompleteSpace K
e : H ≃ₗᵢ[𝕜] K
x : H →L[𝕜] H
⊢ Eq.{u_6 + 1} (α := K →L[𝕜] K)
    (((ContinuousAlgEquiv.toAlgEquiv (↑e : H ≃L[𝕜] K).conjContinuousAlgEquiv :
            AlgEquiv.{u_1, u_5, u_6} 𝕜 (H →L[𝕜] H) (K →L[𝕜] K)) :
          (a : H →L[𝕜] H) → K →L[𝕜] K)
        (star x) :
      K →L[𝕜] K)
    (star
        (((ContinuousAlgEquiv.toAlgEquiv (↑e : H ≃L[𝕜] K).conjContinuousAlgEquiv :
              AlgEquiv.{u_1, u_5, u_6} 𝕜 (H →L[𝕜] H) (K →L[𝕜] K)) :
            (a : H →L[𝕜] H) → K →L[𝕜] K)
          x) :
      K →L[𝕜] K)

Tactic:
simp [star_eq_adjoint, conjContinuousAlgEquiv_apply, ← toContinuousLinearEquiv_symm, comp_assoc]

Premises used: ContinuousLinearEquiv.conjContinuousAlgEquiv_apply, LinearIsometryEquiv.toContinuousLinearEquiv_symm, ContinuousLinearMap.comp_assoc, ContinuousLinearMap.star_eq_adjoint
-- 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
e : H ≃ₗᵢ[𝕜] K
x : H →L[𝕜] H
y : K
⊢ Eq (α := K)
    (((((e.conjStarAlgEquiv : StarAlgEquiv.{u_1, u_5, u_6} 𝕜 (H →L[𝕜] H) (K →L[𝕜] K)) : (a : H →L[𝕜] H) → K →L[𝕜] K) x :
            K →L[𝕜] K) :
          (a : K) → K)
        y :
      K)
    ((e : (a : H) → K) ((x : (a : H) → H) ((e.symm : (a : K) → H) y : H) : H) : K)

Tactic:
rfl

Premises used: 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
K : Type u_6
inst_4 : NormedAddCommGroup K
inst_5 : InnerProductSpace 𝕜 K
inst_6 : CompleteSpace K
e : H ≃ₗᵢ[𝕜] K
f : K →L[𝕜] K
x : H
⊢ Eq (α := H)
    (((((StarAlgEquiv.symm e.conjStarAlgEquiv : StarAlgEquiv.{u_1, u_6, u_5} 𝕜 (K →L[𝕜] K) (H →L[𝕜] H)) :
                (a : K →L[𝕜] K) → H →L[𝕜] H)
              f :
            H →L[𝕜] H) :
          (a : H) → H)
        x :
      H)
    ((e.symm : (a : K) → H) ((f : (a : K) → K) ((e : (a : H) → K) x : K) : K) : H)

Tactic:
rfl

Premises used: 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
K : Type u_6
inst_4 : NormedAddCommGroup K
inst_5 : InnerProductSpace 𝕜 K
inst_6 : CompleteSpace K
e : H ≃ₗᵢ[𝕜] K
x : H →L[𝕜] H
⊢ ((e.conjStarAlgEquiv : StarAlgEquiv.{u_1, u_5, u_6} 𝕜 (H →L[𝕜] H) (K →L[𝕜] K)) : (a : H →L[𝕜] H) → K →L[𝕜] K) x =
    (↑(↑e : H ≃L[𝕜] K) : H →L[𝕜] K) ∘SL x ∘SL (↑(↑e.symm : K ≃L[𝕜] H) : K →L[𝕜] H)

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, ContinuousLinearEquiv.symm, LinearEquiv.symm, LinearIsometryEquiv.toContinuousLinearEquiv, 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
K : Type u_6
inst_4 : NormedAddCommGroup K
inst_5 : InnerProductSpace 𝕜 K
inst_6 : CompleteSpace K
e : H ≃ₗᵢ[𝕜] K
⊢ Eq (α := StarAlgEquiv.{u_1, u_6, u_5} 𝕜 (K →L[𝕜] K) (H →L[𝕜] H)) (StarAlgEquiv.symm e.conjStarAlgEquiv)
    e.symm.conjStarAlgEquiv

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, ContinuousLinearEquiv.symm, LinearEquiv.symm, LinearIsometryEquiv.conjStarAlgEquiv, StarRingEquiv.symm, StarAlgEquiv.symm, StarAlgEquiv.ofAlgEquiv, LinearIsometryEquiv.toContinuousLinearEquiv, Equiv.symm, RingEquiv.symm, 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
⊢ Eq (α := (H →L[𝕜] H) ≃⋆ₐ[𝕜] H →L[𝕜] H) (conjStarAlgEquiv (refl 𝕜 H)) StarAlgEquiv.refl

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, RingEquiv.refl, StarAlgEquiv.refl, LinearIsometryEquiv.conjStarAlgEquiv, StarRingEquiv.refl, StarAlgEquiv.ofAlgEquiv, Equiv.refl, 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
K : Type u_6
inst_4 : NormedAddCommGroup K
inst_5 : InnerProductSpace 𝕜 K
inst_6 : CompleteSpace K
G : Type u_7
inst_7 : NormedAddCommGroup G
inst_8 : InnerProductSpace 𝕜 G
inst_9 : CompleteSpace G
e : H ≃ₗᵢ[𝕜] K
f : K ≃ₗᵢ[𝕜] G
⊢ Eq (α := StarAlgEquiv.{u_1, u_5, u_7} 𝕜 (H →L[𝕜] H) (G →L[𝕜] G)) (conjStarAlgEquiv (e.trans f))
    (StarAlgEquiv.trans e.conjStarAlgEquiv f.conjStarAlgEquiv)

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, LinearIsometryEquiv.toLinearIsometry, ContinuousLinearEquiv.symm, LinearEquiv.symm, LinearIsometryEquiv.trans, LinearIsometryEquiv.conjStarAlgEquiv, Equiv.trans, StarRingEquiv.trans, RingEquiv.trans, StarAlgEquiv.ofAlgEquiv, LinearIsometryEquiv.toContinuousLinearEquiv, StarAlgEquiv.trans, LinearEquiv.trans, 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
K : Type u_6
inst_4 : NormedAddCommGroup K
inst_5 : InnerProductSpace 𝕜 K
inst_6 : CompleteSpace K
f g : H ≃ₗᵢ[𝕜] K
rw : Eq (α := StarAlgEquiv.{u_1, u_5, u_6} 𝕜 (H →L[𝕜] H) (K →L[𝕜] K)) g.conjStarAlgEquiv f.conjStarAlgEquiv
| Eq (α := StarAlgEquiv.{u_1, u_5, u_6} 𝕜 (H →L[𝕜] H) (K →L[𝕜] K)) f.conjStarAlgEquiv g.conjStarAlgEquiv

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- 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
conv_lhs :
  Eq (α := StarAlgEquiv.{u_1, u_5, u_6} 𝕜 (H →L[𝕜] H) (K →L[𝕜] K)) g.conjStarAlgEquiv f.conjStarAlgEquiv ↔
    ∃ (α : ↥(unitary 𝕜)), f = α • g
⊢ Eq (α := StarAlgEquiv.{u_1, u_5, u_6} 𝕜 (H →L[𝕜] H) (K →L[𝕜] K)) f.conjStarAlgEquiv g.conjStarAlgEquiv ↔
    ∃ (α : ↥(unitary 𝕜)), f = α • g

Tactic:
conv_lhs => rw [eq_comm]

Premises used: eq_comm
-- 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
simp_rw :
  (∃ (y : 𝕜),
      HSMul.hSMul (β := H →L[𝕜] H) y 1 = (↑(↑g : H ≃L[𝕜] K).symm : K →L[𝕜] H) ∘SL (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)) ↔
    ∃ (α : ↥(unitary 𝕜)), ∀ (x : H), Eq.{u_6 + 1} (α := K) ((f : (a : H) → K) x : K) ((α • g : (a : H) → K) x : K)
⊢ Eq (α := StarAlgEquiv.{u_1, u_5, u_6} 𝕜 (H →L[𝕜] H) (K →L[𝕜] K)) g.conjStarAlgEquiv f.conjStarAlgEquiv ↔
    ∃ (α : ↥(unitary 𝕜)), f = α • g

Tactic:
simp_rw [StarAlgEquiv.ext_iff, LinearIsometryEquiv.ext_iff, conjStarAlgEquiv_apply,
    ← eq_toContinuousLinearMap_symm_comp, ← comp_assoc, toContinuousLinearEquiv_symm,
    eq_comp_toContinuousLinearMap_symm,
    comp_assoc, ← comp_assoc _ (f : H →L[𝕜] K), comp_coe, ← ContinuousLinearMap.mul_def,
    ← Subalgebra.mem_center_iff (R := 𝕜), Algebra.IsCentral.center_eq_bot, ← comp_coe,
    Algebra.mem_bot, Set.mem_range, Algebra.algebraMap_eq_smul_one]

Premises used: Set.mem_range, LinearIsometryEquiv.ext_iff, LinearIsometryEquiv.conjStarAlgEquiv_apply, Subalgebra.mem_center_iff, Algebra.mem_bot, ContinuousLinearEquiv.eq_toContinuousLinearMap_symm_comp, ContinuousLinearEquiv.comp_coe, LinearIsometryEquiv.toContinuousLinearEquiv_symm, ContinuousLinearEquiv.eq_comp_toContinuousLinearMap_symm, Algebra.algebraMap_eq_smul_one, ContinuousLinearMap.comp_assoc, StarAlgEquiv.ext_iff, Algebra.IsCentral.center_eq_bot, ContinuousLinearMap.mul_def, 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 : ∃ (α : ↥(unitary 𝕜)), ∀ (x : H), Eq.{u_6 + 1} (α := K) ((f : (a : H) → K) x : K) ((α • g : (a : H) → K) x : K)
y : ↥(unitary 𝕜)
h : ∀ (x : H), Eq.{u_6 + 1} (α := K) ((f : (a : H) → K) x : K) ((y • g : (a : H) → K) x : K)
h₁ :
  ∀ (x : H),
    Eq (α := H) ((HSMul.hSMul (β := H →L[𝕜] H) (↑y : 𝕜) 1 : (a : H) → H) x : H)
      (((↑(↑g : H ≃L[𝕜] K).symm : K →L[𝕜] H) ∘SL (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K) : (a : H) → H) x : H)
⊢ HSMul.hSMul (β := H →L[𝕜] H) (↑y : 𝕜) 1 = (↑(↑g : H ≃L[𝕜] K).symm : K →L[𝕜] H) ∘SL (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)

Tactic:
ext
-- 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 : ∃ (α : ↥(unitary 𝕜)), ∀ (x : H), Eq.{u_6 + 1} (α := K) ((f : (a : H) → K) x : K) ((α • g : (a : H) → K) x : K)
y : ↥(unitary 𝕜)
h : ∀ (x : H), Eq.{u_6 + 1} (α := K) ((f : (a : H) → K) x : K) ((y • g : (a : H) → K) x : K)
x : H
⊢ Eq (α := H) ((HSMul.hSMul (β := H →L[𝕜] H) (↑y : 𝕜) 1 : (a : H) → H) x : H)
    (((↑(↑g : H ≃L[𝕜] K).symm : K →L[𝕜] H) ∘SL (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K) : (a : H) → H) x : H)

Tactic:
simp [h]
-- 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
refine :
  (∃ (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)),
      ∃ (α : ↥(unitary 𝕜)), ∀ (x : H), Eq.{u_6 + 1} (α := K) ((f : (a : H) → K) x : K) ((α • g : (a : H) → K) x : K)
⊢ (∃ (y : 𝕜),
      HSMul.hSMul (β := H →L[𝕜] H) y 1 = (↑(↑g : H ≃L[𝕜] K).symm : K →L[𝕜] H) ∘SL (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)) ↔
    ∃ (α : ↥(unitary 𝕜)), ∀ (x : H), Eq.{u_6 + 1} (α := K) ((f : (a : H) → K) x : K) ((α • g : (a : H) → K) x : K)

Tactic:
refine ⟨fun ⟨y, h⟩ ↦ ?_, fun ⟨y, h⟩ ↦ ⟨(y : 𝕜), by ext; simp [h]⟩⟩
-- 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)
pos :
  ∀ (hy : y = 0),
    ∃ (α : ↥(unitary 𝕜)), ∀ (x : H), Eq.{u_6 + 1} (α := K) ((f : (a : H) → K) x : K) ((α • g : (a : H) → K) x : K)
neg :
  ∀ (hy : y ≠ 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:
by_cases! hy : y = 0
-- 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
x : H
⊢ x = 0

Tactic:
simpa [hy] using congr($h x).symm

Premises used: congrArg, id, Eq.symm, DFunLike.coe
-- 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
⊢ ∃ (α : ↥(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 [hy] using congr($h x).symm]⟩
-- 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
h₁ :
  ∀ (x : H),
    Eq.{u_6 + 1} (α := K) (((↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K) : (a : H) → K) x : K)
      ((y • (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K) : (a : H) → K) x : K)
⊢ (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K) = y • (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K)

Tactic:
ext
-- 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
x : H
⊢ Eq.{u_6 + 1} (α := K) (((↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K) : (a : H) → K) x : K)
    ((y • (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K) : (a : H) → K) x : K)

Tactic:
simpa using congr(g ($h _)).symm

Premises used: congrArg, id, Eq.symm, DFunLike.coe
-- 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
⊢ (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K) = y • (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K)

Tactic:
have hfg : (f : H →L[𝕜] K) = y • g := by ext; simpa using congr(g ($h _)).symm
-- 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)
h₁ :
  ∀ (x : H),
    Eq.{u_6 + 1} (α := K) (((↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K) : (a : H) → K) x : K)
      ((star y • (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K) : (a : H) → K) x : K)
⊢ (↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K) = star y • (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)

Tactic:
ext 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)
x : H
⊢ (f : (a : H) → K)
      ((((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K) : K →L[𝕜] H) : (a : K) → H)
          ((g : (a : H) → K) x : K) :
        H) =
    HSMul.hSMul (α := 𝕜) (β := K) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜) ((f : (a : H) → K) x : K)

Tactic:
simpa [map_smulₛₗ, ← ContinuousLinearEquiv.comp_coe, ← toContinuousLinearEquiv_symm,
      ← adjoint_eq_symm, ContinuousLinearMap.one_def] using congr(f (adjoint $h x)).symm

Premises used: LinearIsometryEquiv.adjoint_eq_symm, congrArg, id, ContinuousLinearEquiv.comp_coe, LinearIsometryEquiv.toContinuousLinearEquiv_symm, ContinuousLinearMap.adjoint, Eq.symm, DFunLike.coe, ContinuousLinearMap.one_def, LinearIsometryEquiv.map_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)
x : H
⊢ (f : (a : H) → K)
      ((((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K) : K →L[𝕜] H) : (a : K) → H)
          ((g : (a : H) → K) x : K) :
        H) =
    HSMul.hSMul (α := 𝕜) (β := K) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜) ((f : (a : H) → K) x : K)

Tactic:
have := by simpa [map_smulₛₗ, ← ContinuousLinearEquiv.comp_coe, ← toContinuousLinearEquiv_symm,
      ← adjoint_eq_symm, ContinuousLinearMap.one_def] using congr(f (adjoint $h x)).symm
-- 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)
x : H
this :
  (f : (a : H) → K)
      ((((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K) : K →L[𝕜] H) : (a : K) → H)
          ((g : (a : H) → K) x : K) :
        H) =
    HSMul.hSMul (α := 𝕜) (β := K) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜) ((f : (a : H) → K) x : K)
⊢ Eq.{u_6 + 1} (α := K) (((↑(↑g : H ≃L[𝕜] K) : H →L[𝕜] K) : (a : H) → K) x : K)
    ((star y • (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K) : (a : H) → K) x : K)

Tactic:
simpa