awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
rw :
  Function.Injective (α := E) (β := E) (⇑((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A ∘ₗ A) : (a : E) → E) ↔
    Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑A : (a : E) → F)
rw₁ :
  ker (M₂ := E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A ∘ₗ A) = ⊥ ↔
    Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑A : (a : E) → F)
rw₂ : ker (M₂ := E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A ∘ₗ A) = ⊥ ↔ A.ker = ⊥
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := E) (β := E)
      (Function.comp.{u_2 + 1, u_3 + 1, u_2 + 1} (β := F)
        (⇑((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A : F →ₗ[𝕜] E) : (a : F) → E) (⇑A : (a : E) → F)) ↔
    Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑A : (a : E) → F)
have rw₃ : A.ker = ⊥ ↔ A.ker = ⊥
Tactic: rw [← coe_comp, ← ker_eq_bot, ← ker_eq_bot, ker_adjoint_comp_self]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
⊢ (ker (M₂ := E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A ∘ₗ A))ᗮ =
    range.{u_1, u_1, u_3, u_2} (R := 𝕜) (M := F) (τ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A)
have rw : A.kerᗮ = range.{u_1, u_1, u_3, u_2} (R := 𝕜) (M := F) (τ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A)
Tactic: rw [ker_adjoint_comp_self, orthogonal_ker]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
rw :
  A.kerᗮ =
    range.{u_1, u_1, u_3, u_2} (R := 𝕜) (M := F) (τ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A)
⊢ (ker (M₂ := E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A ∘ₗ A))ᗮ =
    range.{u_1, u_1, u_3, u_2} (R := 𝕜) (M := F) (τ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A)
have rw₁ : Eq.{u_2 + 1} (α := Submodule 𝕜 E)
  (range.{u_1, u_1, u_3, u_2} (R := 𝕜) (M := F) (τ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A))
  (range.{u_1, u_1, u_3, u_2} (R := 𝕜) (M := F) (τ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A))
Tactic: rw [ker_adjoint_comp_self, orthogonal_ker]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
⊢ finrank 𝕜 F -
      finrank.{u_1, u_3} 𝕜
        ↥(ker.{u_1, u_1, u_3, u_2} (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
            ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A)) =
    finrank.{u_1, u_3} 𝕜 ↥A.range
have rw : finrank.{u_1, u_3} 𝕜
        ↥(ker.{u_1, u_1, u_3, u_2} (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
            ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A)) +
      finrank.{u_1, u_3} 𝕜 ↥A.range -
    finrank.{u_1, u_3} 𝕜
      ↥(ker.{u_1, u_1, u_3, u_2} (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
          ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A)) =
  finrank.{u_1, u_3} 𝕜 ↥A.range
Tactic: rw [← A.adjoint.ker.finrank_add_finrank_orthogonal,
    orthogonal_ker, adjoint_adjoint]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
ι₁ : Type u_5
ι₂ : Type u_6
b₁ : Basis ι₁ 𝕜 E
b₂ : Basis ι₂ 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : A = (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B
x : ι₁
y : ι₂
⊢ inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) ((b₁ : (a : ι₁) → E) x : E) : F) ((b₂ : (a : ι₂) → F) y : F) =
    inner.{u_1, u_2} 𝕜 (E := E) ((b₁ : (a : ι₁) → E) x : E) ((B : (a : F) → E) ((b₂ : (a : ι₂) → F) y : F) : E)
have rw : inner.{u_1, u_3} 𝕜 (E := F)
    ((((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B : E →ₗ[𝕜] F) : (a : E) → F) ((b₁ : (a : ι₁) → E) x : E) : F)
    ((b₂ : (a : ι₂) → F) y : F) =
  inner.{u_1, u_2} 𝕜 (E := E) ((b₁ : (a : ι₁) → E) x : E) ((B : (a : F) → E) ((b₂ : (a : ι₂) → F) y : F) : E)
Tactic: rw [h, adjoint_inner_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
ι₁ : Type u_5
ι₂ : Type u_6
b₁ : Basis ι₁ 𝕜 E
b₂ : Basis ι₂ 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : A = (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B
x : ι₁
y : ι₂
rw :
  inner.{u_1, u_3} 𝕜 (E := F)
      ((((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B : E →ₗ[𝕜] F) : (a : E) → F) ((b₁ : (a : ι₁) → E) x : E) : F)
      ((b₂ : (a : ι₂) → F) y : F) =
    inner.{u_1, u_2} 𝕜 (E := E) ((b₁ : (a : ι₁) → E) x : E) ((B : (a : F) → E) ((b₂ : (a : ι₂) → F) y : F) : E)
⊢ inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) ((b₁ : (a : ι₁) → E) x : E) : F) ((b₂ : (a : ι₂) → F) y : F) =
    inner.{u_1, u_2} 𝕜 (E := E) ((b₁ : (a : ι₁) → E) x : E) ((B : (a : F) → E) ((b₂ : (a : ι₂) → F) y : F) : E)
have rw₁ : inner.{u_1, u_2} 𝕜 (E := E) ((b₁ : (a : ι₁) → E) x : E) ((B : (a : F) → E) ((b₂ : (a : ι₂) → F) y : F) : E) =
  inner.{u_1, u_2} 𝕜 (E := E) ((b₁ : (a : ι₁) → E) x : E) ((B : (a : F) → E) ((b₂ : (a : ι₂) → F) y : F) : E)
Tactic: rw [h, adjoint_inner_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
ι₁ : Type u_5
ι₂ : Type u_6
b₁ : Basis ι₁ 𝕜 E
b₂ : Basis ι₂ 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
⊢ A = (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B ↔
    ∀ (i₁ : ι₁) (i₂ : ι₂),
      inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) ((b₁ : (a : ι₁) → E) i₁ : E) : F) ((b₂ : (a : ι₂) → F) i₂ : F) =
        inner.{u_1, u_2} 𝕜 (E := E) ((b₁ : (a : ι₁) → E) i₁ : E) ((B : (a : F) → E) ((b₂ : (a : ι₂) → F) i₂ : F) : E)
have refine : ∀
  (h :
    ∀ (i₁ : ι₁) (i₂ : ι₂),
      inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) ((b₁ : (a : ι₁) → E) i₁ : E) : F) ((b₂ : (a : ι₂) → F) i₂ : F) =
        inner.{u_1, u_2} 𝕜 (E := E) ((b₁ : (a : ι₁) → E) i₁ : E) ((B : (a : F) → E) ((b₂ : (a : ι₂) → F) i₂ : F) : E)),
  A = (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B
Tactic: refine ⟨fun h x y => by rw [h, adjoint_inner_left], fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
ι₁ : Type u_5
ι₂ : Type u_6
b₁ : Basis ι₁ 𝕜 E
b₂ : Basis ι₂ 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h :
  ∀ (i₁ : ι₁) (i₂ : ι₂),
    inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) ((b₁ : (a : ι₁) → E) i₁ : E) : F) ((b₂ : (a : ι₂) → F) i₂ : F) =
      inner.{u_1, u_2} 𝕜 (E := E) ((b₁ : (a : ι₁) → E) i₁ : E) ((B : (a : F) → E) ((b₂ : (a : ι₂) → F) i₂ : F) : E)
⊢ A = (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B
have refine : ∀ (i₁ : ι₁),
  Eq.{u_3 + 1} (α := F) ((A : (a : E) → F) ((b₁ : (a : ι₁) → E) i₁ : E) : F)
    ((((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B : E →ₗ[𝕜] F) : (a : E) → F) ((b₁ : (a : ι₁) → E) i₁ : E) : F)
Tactic: refine Basis.ext b₁ fun i₁ => ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
ι : Type u_5
b : Basis ι 𝕜 E
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : A = (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B
x : ι
y : F
⊢ ⟪(A : (a : E) → F) ((b : (a : ι) → E) x : E), y⟫_𝕜 =
    inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) x : E) ((B : (a : F) → E) y : E)
have rw : ⟪(((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B : E →ₗ[𝕜] F) : (a : E) → F) ((b : (a : ι) → E) x : E), y⟫_𝕜 =
  inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) x : E) ((B : (a : F) → E) y : E)
Tactic: rw [h, adjoint_inner_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
ι : Type u_5
b : Basis ι 𝕜 E
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : A = (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B
x : ι
y : F
rw :
  ⟪(((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B : E →ₗ[𝕜] F) : (a : E) → F) ((b : (a : ι) → E) x : E), y⟫_𝕜 =
    inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) x : E) ((B : (a : F) → E) y : E)
⊢ ⟪(A : (a : E) → F) ((b : (a : ι) → E) x : E), y⟫_𝕜 =
    inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) x : E) ((B : (a : F) → E) y : E)
have rw₁ : inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) x : E) ((B : (a : F) → E) y : E) =
  inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) x : E) ((B : (a : F) → E) y : E)
Tactic: rw [h, adjoint_inner_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
ι : Type u_5
b : Basis ι 𝕜 E
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
⊢ A = (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B ↔
    ∀ (i : ι) (y : F),
      ⟪(A : (a : E) → F) ((b : (a : ι) → E) i : E), y⟫_𝕜 =
        inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((B : (a : F) → E) y : E)
have refine : ∀
  (h :
    ∀ (i : ι) (y : F),
      ⟪(A : (a : E) → F) ((b : (a : ι) → E) i : E), y⟫_𝕜 =
        inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((B : (a : F) → E) y : E))
  (i : ι),
  Eq.{u_3 + 1} (α := F) ((A : (a : E) → F) ((b : (a : ι) → E) i : E) : F)
    ((((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B : E →ₗ[𝕜] F) : (a : E) → F) ((b : (a : ι) → E) i : E) : F)
Tactic: refine ⟨fun h x y => by rw [h, adjoint_inner_left], fun h => Basis.ext b fun i => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
ι : Type u_5
b : Basis ι 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : A = (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B
x : ι
y : E
⊢ inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) y : F) ((b : (a : ι) → F) x : F) =
    ⟪y, (B : (a : F) → E) ((b : (a : ι) → F) x : F)⟫_𝕜
have rw : inner.{u_1, u_3} 𝕜 (E := F) ((((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B : E →ₗ[𝕜] F) : (a : E) → F) y : F)
    ((b : (a : ι) → F) x : F) =
  ⟪y, (B : (a : F) → E) ((b : (a : ι) → F) x : F)⟫_𝕜
Tactic: rw [h, adjoint_inner_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
ι : Type u_5
b : Basis ι 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : A = (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B
x : ι
y : E
rw :
  inner.{u_1, u_3} 𝕜 (E := F) ((((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B : E →ₗ[𝕜] F) : (a : E) → F) y : F)
      ((b : (a : ι) → F) x : F) =
    ⟪y, (B : (a : F) → E) ((b : (a : ι) → F) x : F)⟫_𝕜
⊢ inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) y : F) ((b : (a : ι) → F) x : F) =
    ⟪y, (B : (a : F) → E) ((b : (a : ι) → F) x : F)⟫_𝕜
have rw₁ : ⟪y, (B : (a : F) → E) ((b : (a : ι) → F) x : F)⟫_𝕜 = ⟪y, (B : (a : F) → E) ((b : (a : ι) → F) x : F)⟫_𝕜
Tactic: rw [h, adjoint_inner_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
ι : Type u_5
b : Basis ι 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
⊢ A = (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B ↔
    ∀ (i : ι) (x : E),
      inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((b : (a : ι) → F) i : F) =
        ⟪x, (B : (a : F) → E) ((b : (a : ι) → F) i : F)⟫_𝕜
have refine : ∀
  (h :
    ∀ (i : ι) (x : E),
      inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((b : (a : ι) → F) i : F) =
        ⟪x, (B : (a : F) → E) ((b : (a : ι) → F) i : F)⟫_𝕜),
  A = (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B
Tactic: refine ⟨fun h x y => by rw [h, adjoint_inner_left], fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
ι : Type u_5
b : Basis ι 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h :
  ∀ (i : ι) (x : E),
    inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((b : (a : ι) → F) i : F) =
      ⟪x, (B : (a : F) → E) ((b : (a : ι) → F) i : F)⟫_𝕜
⊢ A = (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B
have h₁ : ∀ (x : E),
  Eq.{u_3 + 1} (α := F) ((A : (a : E) → F) x : F)
    ((((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B : E →ₗ[𝕜] F) : (a : E) → F) x : F)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
A : E →ₗ[𝕜] E
⊢ IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) A ↔ IsSelfAdjoint A
have rw : A = (adjoint : (a : E →ₗ[𝕜] E) → E →ₗ[𝕜] E) A ↔ (adjoint : (a : E →ₗ[𝕜] E) → E →ₗ[𝕜] E) A = A
Tactic: rw [isSelfAdjoint_iff', IsSymmetric, ← LinearMap.eq_adjoint_iff]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
x : E
⊢ LE.le (α := ℝ) (0 : ℝ)
    ((re : (a : 𝕜) → ℝ)
        ⟪x, (HMul.hMul (α := E →ₗ[𝕜] E) ((adjoint : (a : E →ₗ[𝕜] E) → E →ₗ[𝕜] E) T : E →ₗ[𝕜] E) T : (a : E) → E) x⟫_𝕜 :
      ℝ)
have simp : LE.le (α := ℝ) (0 : ℝ)
  ((re : (a : 𝕜) → ℝ) (HPow.hPow (α := 𝕜) (β := ℕ) (↑(norm (E := E) ((T : (a : E) → E) x : E)) : 𝕜) 2) : ℝ)
Tactic: simp only [Module.End.mul_apply, adjoint_inner_right, inner_self_eq_norm_sq_to_K]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
x : E
⊢ LE.le (α := ℝ) (0 : ℝ)
    ((re : (a : 𝕜) → ℝ) (HPow.hPow (α := 𝕜) (β := ℕ) (↑(norm (E := E) ((T : (a : E) → E) x : E)) : 𝕜) 2) : ℝ)
have norm_cast : 0 ≤ HPow.hPow (β := ℕ) (norm (E := E) ((T : (a : E) → E) x : E)) 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
x : E
⊢ Eq (α := ℝ)
    ((im : (a : 𝕜) → ℝ)
        ⟪x, (((adjoint : (a : E →ₗ[𝕜] E) → E →ₗ[𝕜] E) T : E →ₗ[𝕜] E) : (a : E) → E) ((T : (a : E) → E) x : E)⟫_𝕜 :
      ℝ)
    (0 : ℝ)
have simp : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) (HPow.hPow (α := 𝕜) (β := ℕ) (↑(norm (E := E) ((T : (a : E) → E) x : E)) : 𝕜) 2) : ℝ)
  (0 : ℝ)
Tactic: simp only [adjoint_inner_right, inner_self_eq_norm_sq_to_K]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
x : E
⊢ Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) (HPow.hPow (α := 𝕜) (β := ℕ) (↑(norm (E := E) ((T : (a : E) → E) x : E)) : 𝕜) 2) : ℝ)
    (0 : ℝ)
have norm_cast : Eq (α := ℝ) 0 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T : E →L[𝕜] E
⊢ have this : CompleteSpace E := ⋯;
  IsSelfAdjoint (↑T : E →ₗ[𝕜] E) ↔ IsSelfAdjoint T
have simp : Eq (α := E →L[𝕜] E)
    ((LinearIsometryEquiv.toLinearEquiv.{u_1, u_1, u_2, u_2} (E := E →L[𝕜] E) ContinuousLinearMap.adjoint :
          (a : E →L[𝕜] E) → E →L[𝕜] E)
        (((toContinuousLinearMap : (E →ₗ[𝕜] E) ≃ₗ[𝕜] E →L[𝕜] E) : (a : E →ₗ[𝕜] E) → E →L[𝕜] E) (↑T : E →ₗ[𝕜] E) :
          E →L[𝕜] E) :
      E →L[𝕜] E)
    (((toContinuousLinearMap : (E →ₗ[𝕜] E) ≃ₗ[𝕜] E →L[𝕜] E) : (a : E →ₗ[𝕜] E) → E →L[𝕜] E) (↑T : E →ₗ[𝕜] E) :
      E →L[𝕜] E) ↔
  (ContinuousLinearMap.adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T = T
Tactic: simp only [IsSelfAdjoint, star, adjoint, LinearEquiv.trans_apply,
    coe_toContinuousLinearMap_symm,
    ContinuousLinearMap.toLinearMap_eq_iff_eq_toContinuousLinearMap]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
S T : E →ₗ[𝕜] E
hS : IsStarProjection S
hT : IsStarProjection T
⊢ S = T ↔ S.range = T.range
have this : CompleteSpace E
Tactic: have := FiniteDimensional.complete 𝕜 E
-- 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
⊢ (∀ (x y : H), inner.{u_1, u_6} 𝕜 (E := K) ((u : (a : H) → K) x : K) ((u : (a : H) → K) y : K) = ⟪x, y⟫_𝕜) ↔
    Eq (α := H →L[𝕜] H) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) u) u) 1
have refine_1 : ∀ (h : ∀ (x y : H), inner.{u_1, u_6} 𝕜 (E := K) ((u : (a : H) → K) x : K) ((u : (a : H) → K) y : K) = ⟪x, y⟫_𝕜) (x : H),
  Eq (α := H) ((comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) u) u : (a : H) → H) x : H)
    ((1 : (a : H) → H) x : H)
Tactic: refine ⟨fun h ↦ ext fun x ↦ ?_, fun 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
u : H →L[𝕜] K
refine_1 :
  ∀ (h : ∀ (x y : H), inner.{u_1, u_6} 𝕜 (E := K) ((u : (a : H) → K) x : K) ((u : (a : H) → K) y : K) = ⟪x, y⟫_𝕜)
    (x : H),
    Eq (α := H) ((comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) u) u : (a : H) → H) x : H)
      ((1 : (a : H) → H) x : H)
⊢ (∀ (x y : H), inner.{u_1, u_6} 𝕜 (E := K) ((u : (a : H) → K) x : K) ((u : (a : H) → K) y : K) = ⟪x, y⟫_𝕜) ↔
    Eq (α := H →L[𝕜] H) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) u) u) 1
have refine_2 : ∀ (h : Eq (α := H →L[𝕜] H) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) u) u) 1) (x y : H),
  inner.{u_1, u_6} 𝕜 (E := K) ((u : (a : H) → K) x : K) ((u : (a : H) → K) y : K) = ⟪x, y⟫_𝕜
Tactic: refine ⟨fun h ↦ ext fun x ↦ ?_, fun 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
u : H →L[𝕜] K
h : ∀ (x y : H), inner.{u_1, u_6} 𝕜 (E := K) ((u : (a : H) → K) x : K) ((u : (a : H) → K) y : K) = ⟪x, y⟫_𝕜
x : H
⊢ Eq (α := H) ((comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) u) u : (a : H) → H) x : H)
    ((1 : (a : H) → H) x : H)
have refine_1 : ∀ (y : H),
  ⟪(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) u) u : (a : H) → H) x, y⟫_𝕜 =
    ⟪(1 : (a : H) → H) x, y⟫_𝕜
Tactic: refine ext_inner_right 𝕜 fun y ↦ ?_
-- 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
⊢ (∀ (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
have rw : (∀ (x y : H), inner.{u_1, u_6} 𝕜 (E := K) ((u : (a : H) → K) x : K) ((u : (a : H) → K) y : K) = ⟪x, y⟫_𝕜) ↔
  Eq (α := H →L[𝕜] H) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) u) u) 1
Tactic: rw [LinearMap.norm_map_iff_inner_map_map u, u.inner_map_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
u : H →L[𝕜] K
rw :
  (∀ (x y : H), inner.{u_1, u_6} 𝕜 (E := K) ((u : (a : H) → K) x : K) ((u : (a : H) → K) y : K) = ⟪x, y⟫_𝕜) ↔
    Eq (α := H →L[𝕜] H) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : H →L[𝕜] K) → K →L[𝕜] H) u) u) 1
⊢ (∀ (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
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 [LinearMap.norm_map_iff_inner_map_map u, u.inner_map_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
u : H →L[𝕜] K
⊢ 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 : (∀ (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
Tactic: rw [AddMonoidHomClass.isometry_iff_norm, norm_map_iff_adjoint_comp_self]