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
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst_3 : CompleteSpace E
hT : IsIdempotentElem T
h : IsStarNormal T
⊢ T = star T * T
have rw : ∀ (x : E), Eq (α := E) ((T - star T * T : (a : E) → E) x : E) ((0 : (a : E) → E) x : E)
Tactic: rw [← sub_eq_zero, ContinuousLinearMap.ext_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
T : E →L[𝕜] E
inst_3 : CompleteSpace E
hT : IsIdempotentElem T
h : IsStarNormal T
⊢ ∀ (x : E), Eq (α := E) ((T - star T * T : (a : E) → E) x : E) ((0 : (a : E) → E) x : E)
have simp_rw : ∀ (x : E), norm (E := E) ((T - star T * T : (a : E) → E) x : E) = 0
Tactic: simp_rw [zero_apply, ← norm_eq_zero (E := E)]
-- 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
T : E →L[𝕜] E
inst_3 : CompleteSpace E
hT : IsIdempotentElem T
h : IsStarNormal T
⊢ ∀ (x : E), norm (E := E) ((T - star T * T : (a : E) → E) x : E) = 0
have this : (∀ (x : E), norm (E := E) ((T - star T * T : (a : E) → E) x : E) = 0) ↔ IsIdempotentElem T
Tactic: have :=
    calc (∀ x : E, ‖(T - star T * T) x‖ = 0) ↔ ∀ x, ‖(adjoint (1 - T)) (T x)‖ = 0 := by
          simp [star_eq_adjoint, one_def]
      _ ↔ ∀ x, ‖(1 - T) (T x)‖ = 0 := by
          simp only [isStarNormal_iff_norm_eq_adjoint.mp h.one_sub]
      _ ↔ ∀ x, ‖(T - T * T) x‖ = 0 := by simp
      _ ↔ T - T * T = 0 := by simp only [norm_eq_zero, ContinuousLinearMap.ext_iff, zero_apply]
      _ ↔ IsIdempotentElem T := by simp only [sub_eq_zero, IsIdempotentElem, eq_comm]
-- 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
T : E →L[𝕜] E
inst_3 : CompleteSpace E
⊢ IsStarProjection T ↔ IsIdempotentElem T ∧ IsStarNormal T
have rw : IsIdempotentElem T → (IsSelfAdjoint T ↔ IsStarNormal T)
Tactic: rw [isStarProjection_iff, and_congr_right_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 : CompleteSpace E
T : E →L[𝕜] E
U : Submodule 𝕜 E
h :
  Membership.mem (γ := Sublattice (Submodule 𝕜 E))
    (invtSubmodule (↑((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T) : E →ₗ[𝕜] E)) U
⊢ Uᗮ ∈ invtSubmodule (↑T : E →ₗ[𝕜] E)
have simp : ∀
  (h :
    ∀ x ∈ U, Membership.mem (α := E) U ((((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) T : E →L[𝕜] E) : (a : E) → E) x : E))
  (x : E), (∀ u ∈ U, ⟪u, x⟫_𝕜 = 0) → ∀ u ∈ U, ⟪u, (T : (a : E) → E) x⟫_𝕜 = 0
Tactic: simp only [mem_invtSubmodule_iff_forall_mem_of_mem, coe_coe, mem_orthogonal] at h ⊢
Cleared hypotheses: h
-- 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 : CompleteSpace E
p : E →L[𝕜] E
⊢ IsStarProjection p ↔ ∃ (x : (↑p : E →ₗ[𝕜] E).range.HasOrthogonalProjection), p = (↑p : E →ₗ[𝕜] E).range.starProjection
have simp_rw : LinearMap.IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑p : E →ₗ[𝕜] E) ↔
  ∃ (x : (↑p : E →ₗ[𝕜] E).range.HasOrthogonalProjection), p = (↑p : E →ₗ[𝕜] E).range.starProjection
Tactic: simp_rw [p.isStarProjection_iff_isSymmetricProjection.eq,
    LinearMap.isSymmetricProjection_iff_eq_coe_starProjection_range, coe_inj]
-- 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 : CompleteSpace E
p : E →L[𝕜] E
simp_rw :
  LinearMap.IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑p : E →ₗ[𝕜] E) ↔
    ∃ (x : (↑p : E →ₗ[𝕜] E).range.HasOrthogonalProjection), p = (↑p : E →ₗ[𝕜] E).range.starProjection
⊢ IsStarProjection p ↔ ∃ (x : (↑p : E →ₗ[𝕜] E).range.HasOrthogonalProjection), p = (↑p : E →ₗ[𝕜] E).range.starProjection
have simp_rw₁ : (∃ (x : (↑p : E →ₗ[𝕜] E).range.HasOrthogonalProjection),
    (↑p : E →ₗ[𝕜] E) = (↑(↑p : E →ₗ[𝕜] E).range.starProjection : E →ₗ[𝕜] E)) ↔
  ∃ (x : (↑p : E →ₗ[𝕜] E).range.HasOrthogonalProjection), p = (↑p : E →ₗ[𝕜] E).range.starProjection
Tactic: simp_rw [p.isStarProjection_iff_isSymmetricProjection.eq,
    LinearMap.isSymmetricProjection_iff_eq_coe_starProjection_range, coe_inj]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (hypothesis)
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
x : E
y : F
⊢ ⟪(((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A : F →ₗ[𝕜] E) : (a : F) → E) y, x⟫_𝕜 = ⟪y, (A : (a : E) → F) x⟫_𝕜
have this : CompleteSpace E
Tactic: have := FiniteDimensional.complete 𝕜 E
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (hypothesis)
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
x : E
y : F
this : CompleteSpace E
⊢ ⟪(((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A : F →ₗ[𝕜] E) : (a : F) → E) y, x⟫_𝕜 = ⟪y, (A : (a : E) → F) x⟫_𝕜
have this₁ : CompleteSpace F
Tactic: have := FiniteDimensional.complete 𝕜 F
-- 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
x : E
y : F
this_1 : CompleteSpace E
this : CompleteSpace F
⊢ ⟪(((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A : F →ₗ[𝕜] E) : (a : F) → E) y, x⟫_𝕜 = ⟪y, (A : (a : E) → F) x⟫_𝕜
have rw : ⟪((↑((ContinuousLinearMap.adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E)
              (((toContinuousLinearMap : (E →ₗ[𝕜] F) ≃ₗ[𝕜] E →L[𝕜] F) : (a : E →ₗ[𝕜] F) → E →L[𝕜] F)
                (↑(((toContinuousLinearMap : (E →ₗ[𝕜] F) ≃ₗ[𝕜] E →L[𝕜] F) : (a : E →ₗ[𝕜] F) → E →L[𝕜] F) A) :
                  E →ₗ[𝕜] F))) :
          F →ₗ[𝕜] E) :
        (a : F) → E)
      y,
    x⟫_𝕜 =
  ⟪y,
    ((↑(((toContinuousLinearMap : (E →ₗ[𝕜] F) ≃ₗ[𝕜] E →L[𝕜] F) : (a : E →ₗ[𝕜] F) → E →L[𝕜] F) A) : E →ₗ[𝕜] F) :
        (a : E) → F)
      x⟫_𝕜
Tactic: rw [← coe_toContinuousLinearMap A, adjoint_eq_toCLM_adjoint]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (hypothesis)
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
x : E
y : F
⊢ ⟪x, (((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A : F →ₗ[𝕜] E) : (a : F) → E) y⟫_𝕜 = ⟪(A : (a : E) → F) x, y⟫_𝕜
have this : CompleteSpace E
Tactic: have := FiniteDimensional.complete 𝕜 E
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (hypothesis)
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
x : E
y : F
this : CompleteSpace E
⊢ ⟪x, (((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A : F →ₗ[𝕜] E) : (a : F) → E) y⟫_𝕜 = ⟪(A : (a : E) → F) x, y⟫_𝕜
have this₁ : CompleteSpace F
Tactic: have := FiniteDimensional.complete 𝕜 F
-- 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
x : E
y : F
this_1 : CompleteSpace E
this : CompleteSpace F
⊢ ⟪x, (((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A : F →ₗ[𝕜] E) : (a : F) → E) y⟫_𝕜 = ⟪(A : (a : E) → F) x, y⟫_𝕜
have rw : ⟪x,
    ((↑((ContinuousLinearMap.adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E)
              (((toContinuousLinearMap : (E →ₗ[𝕜] F) ≃ₗ[𝕜] E →L[𝕜] F) : (a : E →ₗ[𝕜] F) → E →L[𝕜] F)
                (↑(((toContinuousLinearMap : (E →ₗ[𝕜] F) ≃ₗ[𝕜] E →L[𝕜] F) : (a : E →ₗ[𝕜] F) → E →L[𝕜] F) A) :
                  E →ₗ[𝕜] F))) :
          F →ₗ[𝕜] E) :
        (a : F) → E)
      y⟫_𝕜 =
  ⟪((↑(((toContinuousLinearMap : (E →ₗ[𝕜] F) ≃ₗ[𝕜] E →L[𝕜] F) : (a : E →ₗ[𝕜] F) → E →L[𝕜] F) A) : E →ₗ[𝕜] F) :
        (a : E) → F)
      x,
    y⟫_𝕜
Tactic: rw [← coe_toContinuousLinearMap A, adjoint_eq_toCLM_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
A : E →ₗ[𝕜] F
⊢ (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A) = A
have h : ∀ (v : E),
  Eq.{u_3 + 1} (α := F)
    ((((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A) : E →ₗ[𝕜] F) : (a : E) → F)
        v :
      F)
    ((A : (a : E) → F) v : F)
Tactic: ext v
-- 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
v : E
⊢ Eq.{u_3 + 1} (α := F)
    ((((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A) : E →ₗ[𝕜] F) : (a : E) → F)
        v :
      F)
    ((A : (a : E) → F) v : F)
have h : ∀ (w : F),
  ⟪w,
      (((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A) : E →ₗ[𝕜] F) : (a : E) → F)
        v⟫_𝕜 =
    ⟪w, (A : (a : E) → F) v⟫_𝕜
Tactic: refine ext_inner_left 𝕜 fun w => ?_
-- 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
v : E
w : F
⊢ ⟪w,
      (((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A) : E →ₗ[𝕜] F) : (a : E) → F)
        v⟫_𝕜 =
    ⟪w, (A : (a : E) → F) v⟫_𝕜
have h : ⟪(((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A : F →ₗ[𝕜] E) : (a : F) → E) w, v⟫_𝕜 = ⟪w, (A : (a : E) → F) v⟫_𝕜
Tactic: rw [adjoint_inner_right, 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
A : E →ₗ[𝕜] F
v : E
w : F
h : ⟪(((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A : F →ₗ[𝕜] E) : (a : F) → E) w, v⟫_𝕜 = ⟪w, (A : (a : E) → F) v⟫_𝕜
⊢ ⟪w,
      (((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A) : E →ₗ[𝕜] F) : (a : E) → F)
        v⟫_𝕜 =
    ⟪w, (A : (a : E) → F) v⟫_𝕜
have h₁ : ⟪w, (A : (a : E) → F) v⟫_𝕜 = ⟪w, (A : (a : E) → F) v⟫_𝕜
Tactic: rw [adjoint_inner_right, 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
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
inst_7 : FiniteDimensional 𝕜 E
inst_8 : FiniteDimensional 𝕜 F
inst_9 : FiniteDimensional 𝕜 G
A : F →ₗ[𝕜] G
B : E →ₗ[𝕜] F
⊢ Eq (α := G →ₗ[𝕜] E) ((adjoint : (a : E →ₗ[𝕜] G) → G →ₗ[𝕜] E) (A ∘ₗ B) : G →ₗ[𝕜] E)
    ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) B ∘ₗ (adjoint : (a : F →ₗ[𝕜] G) → G →ₗ[𝕜] F) A : G →ₗ[𝕜] E)
have h : ∀ (v : G),
  Eq.{u_2 + 1} (α := E) ((((adjoint : (a : E →ₗ[𝕜] G) → G →ₗ[𝕜] E) (A ∘ₗ B) : G →ₗ[𝕜] E) : (a : G) → E) v : E)
    (((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) B ∘ₗ (adjoint : (a : F →ₗ[𝕜] G) → G →ₗ[𝕜] F) A : (a : G) → E) v : E)
Tactic: ext v
-- 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
inst_7 : FiniteDimensional 𝕜 E
inst_8 : FiniteDimensional 𝕜 F
inst_9 : FiniteDimensional 𝕜 G
A : F →ₗ[𝕜] G
B : E →ₗ[𝕜] F
v : G
⊢ Eq.{u_2 + 1} (α := E) ((((adjoint : (a : E →ₗ[𝕜] G) → G →ₗ[𝕜] E) (A ∘ₗ B) : G →ₗ[𝕜] E) : (a : G) → E) v : E)
    (((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) B ∘ₗ (adjoint : (a : F →ₗ[𝕜] G) → G →ₗ[𝕜] F) A : (a : G) → E) v : E)
have h : ∀ (w : E),
  ⟪w, (((adjoint : (a : E →ₗ[𝕜] G) → G →ₗ[𝕜] E) (A ∘ₗ B) : G →ₗ[𝕜] E) : (a : G) → E) v⟫_𝕜 =
    ⟪w, ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) B ∘ₗ (adjoint : (a : F →ₗ[𝕜] G) → G →ₗ[𝕜] F) A : (a : G) → E) v⟫_𝕜
Tactic: refine ext_inner_left 𝕜 fun w => ?_
-- 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
B : F →ₗ[𝕜] E
h : A = (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B
x : E
y : F
⊢ ⟪(A : (a : E) → F) x, y⟫_𝕜 = ⟪x, (B : (a : F) → E) y⟫_𝕜
have rw : ⟪(((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B : E →ₗ[𝕜] F) : (a : E) → F) x, y⟫_𝕜 = ⟪x, (B : (a : F) → E) y⟫_𝕜
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
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : A = (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B
x : E
y : F
rw : ⟪(((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B : E →ₗ[𝕜] F) : (a : E) → F) x, y⟫_𝕜 = ⟪x, (B : (a : F) → E) y⟫_𝕜
⊢ ⟪(A : (a : E) → F) x, y⟫_𝕜 = ⟪x, (B : (a : F) → E) y⟫_𝕜
have rw₁ : ⟪x, (B : (a : F) → E) y⟫_𝕜 = ⟪x, (B : (a : F) → E) y⟫_𝕜
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
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
⊢ A = (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B ↔
    ∀ (x : E) (y : F), ⟪(A : (a : E) → F) x, y⟫_𝕜 = ⟪x, (B : (a : F) → E) y⟫_𝕜
have refine : ∀ (h : ∀ (x : E) (y : F), ⟪(A : (a : E) → F) x, y⟫_𝕜 = ⟪x, (B : (a : F) → E) y⟫_𝕜),
  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
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : ∀ (x : E) (y : F), ⟪(A : (a : E) → F) x, y⟫_𝕜 = ⟪x, (B : (a : F) → E) y⟫_𝕜
⊢ 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
hA : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) A
⊢ (adjoint : (a : E →ₗ[𝕜] E) → E →ₗ[𝕜] E) A = A
have rwa : A = (adjoint : (a : E →ₗ[𝕜] E) → E →ₗ[𝕜] E) A
Tactic: rwa [eq_comm, eq_adjoint_iff A A]
-- 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
hA : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) A
rwa : A = (adjoint : (a : E →ₗ[𝕜] E) → E →ₗ[𝕜] E) A
⊢ (adjoint : (a : E →ₗ[𝕜] E) → E →ₗ[𝕜] E) A = A
have rwa₁ : ∀ (x y : E), ⟪(A : (a : E) → E) x, y⟫_𝕜 = ⟪x, (A : (a : E) → E) y⟫_𝕜
Tactic: rwa [eq_comm, eq_adjoint_iff A A]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (hypothesis)
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
⊢ A.kerᗮ =
    range.{u_1, u_1, u_3, u_2} (R := 𝕜) (M := F) (τ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A)
have this : CompleteSpace E
Tactic: haveI := FiniteDimensional.complete 𝕜 E
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (hypothesis)
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
this : CompleteSpace E
⊢ A.kerᗮ =
    range.{u_1, u_1, u_3, u_2} (R := 𝕜) (M := F) (τ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A)
have this₁ : CompleteSpace F
Tactic: haveI := FiniteDimensional.complete 𝕜 F
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (hypothesis)
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
⊢ A.rangeᗮ =
    ker.{u_1, u_1, u_3, u_2} (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A)
have this : CompleteSpace E
Tactic: haveI := FiniteDimensional.complete 𝕜 E
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (hypothesis)
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
this : CompleteSpace E
⊢ A.rangeᗮ =
    ker.{u_1, u_1, u_3, u_2} (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A)
have this₁ : CompleteSpace F
Tactic: haveI := FiniteDimensional.complete 𝕜 F
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (hypothesis)
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) = A.ker
have this : CompleteSpace E
Tactic: haveI := FiniteDimensional.complete 𝕜 E
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (hypothesis)
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
this : CompleteSpace E
⊢ ker (M₂ := E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A ∘ₗ A) = A.ker
have this₁ : CompleteSpace F
Tactic: haveI := FiniteDimensional.complete 𝕜 F
-- 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
⊢ 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 : 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)
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
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)
⊢ 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₁ : 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)
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
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)
⊢ 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₂ : ker (M₂ := E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A ∘ₗ A) = ⊥ ↔ A.ker = ⊥
Tactic: rw [← coe_comp, ← ker_eq_bot, ← ker_eq_bot, ker_adjoint_comp_self]