awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
u : H →L[𝕜] K
rw :
  (∀ (x : H), norm.{u_6} (E := K) ((u : (a : H) → K) x : K) = ‖x‖) ↔
    Eq (α := H →L[𝕜] H) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) u) u) 1
⊢ Isometry.{u_5, u_6} (α := H) (β := K) (⇑u : (a : H) → K) ↔
    Eq (α := H →L[𝕜] H) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) u) u) 1
have rw₁ : Eq (α := H →L[𝕜] H) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) u) u) 1 ↔
  Eq (α := H →L[𝕜] H) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) u) u) 1
Tactic: rw [AddMonoidHomClass.isometry_iff_norm, norm_map_iff_adjoint_comp_self]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
⊢ 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)
have 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)
Tactic: rw [← comp_assoc, norm_map_iff_adjoint_comp_self _ |>.mp e.norm_map, one_def, id_comp]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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)
⊢ 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)
have rw₁ : comp (σ₂₃ := RingHom.id 𝕜) 1 (↑(↑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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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)
⊢ 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)
have rw₂ : ContinuousLinearMap.id 𝕜 H ∘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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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)
⊢ 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)
have rw₃ : (↑(↑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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
| Eq (α := StarAlgEquiv.{u_1, u_5, u_6} 𝕜 (H →L[𝕜] H) (K →L[𝕜] K)) f.conjStarAlgEquiv g.conjStarAlgEquiv
have rw : Eq (α := StarAlgEquiv.{u_1, u_5, u_6} 𝕜 (H →L[𝕜] H) (K →L[𝕜] K)) g.conjStarAlgEquiv f.conjStarAlgEquiv
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
⊢ Eq (α := StarAlgEquiv.{u_1, u_5, u_6} 𝕜 (H →L[𝕜] H) (K →L[𝕜] K)) f.conjStarAlgEquiv g.conjStarAlgEquiv ↔
    ∃ (α : ↥(unitary 𝕜)), f = α • g
have conv_lhs : Eq (α := StarAlgEquiv.{u_1, u_5, u_6} 𝕜 (H →L[𝕜] H) (K →L[𝕜] K)) g.conjStarAlgEquiv f.conjStarAlgEquiv ↔
  ∃ (α : ↥(unitary 𝕜)), f = α • g
Tactic: conv_lhs => rw [eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
⊢ Eq (α := StarAlgEquiv.{u_1, u_5, u_6} 𝕜 (H →L[𝕜] H) (K →L[𝕜] K)) g.conjStarAlgEquiv f.conjStarAlgEquiv ↔
    ∃ (α : ↥(unitary 𝕜)), f = α • g
have 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)
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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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)
⊢ HSMul.hSMul (β := H →L[𝕜] H) (↑y : 𝕜) 1 = (↑(↑g : H ≃L[𝕜] K).symm : K →L[𝕜] H) ∘SL (↑(↑f : H ≃L[𝕜] K) : H →L[𝕜] K)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
⊢ (∃ (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)
have 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)
Tactic: refine ⟨fun ⟨y, h⟩ ↦ ?_, fun ⟨y, h⟩ ↦ ⟨(y : 𝕜), by ext; simp [h]⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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)
⊢ ∃ (α : ↥(unitary 𝕜)), ∀ (x : H), Eq.{u_6 + 1} (α := K) ((f : (a : H) → K) x : K) ((α • g : (a : H) → K) x : K)
have pos : ∀ (hy : y = 0),
  ∃ (α : ↥(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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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)
⊢ ∃ (α : ↥(unitary 𝕜)), ∀ (x : H), Eq.{u_6 + 1} (α := K) ((f : (a : H) → K) x : K) ((α • g : (a : H) → K) x : K)
have neg : ∀ (hy : y ≠ 0),
  ∃ (α : ↥(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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (hypothesis)
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)
have hfg : (↑(↑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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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)
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (hypothesis)
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
⊢ 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)
have 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)
Tactic: have := by simpa [map_smulₛₗ, ← ContinuousLinearEquiv.comp_coe, ← toContinuousLinearEquiv_symm,
      ← adjoint_eq_symm, ContinuousLinearMap.one_def] using congr(f (adjoint $h x)).symm
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (hypothesis)
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)
⊢ ∃ (α : ↥(unitary 𝕜)), ∀ (x : H), Eq.{u_6 + 1} (α := K) ((f : (a : H) → K) x : K) ((α • g : (a : H) → K) x : K)
have hgf : (↑(↑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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (hypothesis)
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)
⊢ ∃ (α : ↥(unitary 𝕜)), ∀ (x : H), Eq.{u_6 + 1} (α := K) ((f : (a : H) → K) x : K) ((α • g : (a : H) → K) x : K)
have this : (↑(↑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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (hypothesis)
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)
⊢ ∃ (α : ↥(unitary 𝕜)), ∀ (x : H), Eq.{u_6 + 1} (α := K) ((f : (a : H) → K) x : K) ((α • g : (a : H) → K) x : K)
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (hypothesis)
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)
⊢ ∃ (α : ↥(unitary 𝕜)), ∀ (x : H), Eq.{u_6 + 1} (α := K) ((f : (a : H) → K) x : K) ((α • g : (a : H) → K) x : K)
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
⊢ ∃ (α : ↥(unitary 𝕜)), ∀ (x : H), Eq.{u_6 + 1} (α := K) ((f : (a : H) → K) x : K) ((α • g : (a : H) → K) x : K)
have 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)
Tactic: obtain (this | this) := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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)
⊢ ∃ (α : ↥(unitary 𝕜)), ∀ (x : H), Eq.{u_6 + 1} (α := K) ((f : (a : H) → K) x : K) ((α • g : (a : H) → K) x : K)
have 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)
Tactic: obtain (this | this) := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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) : H →L[𝕜] H) * (↑(↑e.symm : H ≃L[𝕜] H) : H →L[𝕜] H) = 1
have 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: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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.symm : H ≃L[𝕜] H) : H →L[𝕜] H) * (↑(↑e : H ≃L[𝕜] H) : H →L[𝕜] H) = 1
have 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: ext