awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
v : Π₀ (i : ι), ↥(V i)
hv :
  Eq.{u_2 + 1} (α := E)
    (((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
            fun (i : ι) ↦ (V i).subtype :
          (a : Π₀ (i : ι), ↥(V i)) → E)
        v :
      E)
    (0 : E)
i : ι
⊢ ⟪(↑((v : (a : ι) → ↥(V a)) i) : E), (↑((v : (a : ι) → ↥(V a)) i) : E)⟫ =
    ⟪(↑((v : (a : ι) → ↥(V a)) i) : E),
      ((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
            fun (i : ι) ↦ (V i).subtype :
          (a : Π₀ (i : ι), ↥(V i)) → E)
        v⟫

Tactic:
simpa only [DFinsupp.sumAddHom_apply, DFinsupp.lsum_apply_apply] using
        (hV.inner_right_dfinsupp v i (v i)).symm

Premises used: DFinsupp.sumAddHom_apply, Eq.symm, DFinsupp.lsum_apply_apply, DFunLike.coe, OrthogonalFamily.inner_right_dfinsupp
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
v : Π₀ (i : ι), ↥(V i)
hv :
  Eq.{u_2 + 1} (α := E)
    (((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
            fun (i : ι) ↦ (V i).subtype :
          (a : Π₀ (i : ι), ↥(V i)) → E)
        v :
      E)
    (0 : E)
i : ι
⊢ ⟪(↑((v : (a : ι) → ↥(V a)) i) : E),
      ((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
            fun (i : ι) ↦ (V i).subtype :
          (a : Π₀ (i : ι), ↥(V i)) → E)
        v⟫ =
    0

Tactic:
simp only [hv, inner_zero_right]

Premises used: inner_zero_right
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
v : Π₀ (i : ι), ↥(V i)
hv :
  Eq.{u_2 + 1} (α := E)
    (((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
            fun (i : ι) ↦ (V i).subtype :
          (a : Π₀ (i : ι), ↥(V i)) → E)
        v :
      E)
    (0 : E)
i : ι
i₁ :
  ⟪(↑((v : (a : ι) → ↥(V a)) i) : E), (↑((v : (a : ι) → ↥(V a)) i) : E)⟫ =
    ⟪(↑((v : (a : ι) → ↥(V a)) i) : E),
      ((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
            fun (i : ι) ↦ (V i).subtype :
          (a : Π₀ (i : ι), ↥(V i)) → E)
        v⟫
i₂ :
  ⟪(↑((v : (a : ι) → ↥(V a)) i) : E),
      ((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
            fun (i : ι) ↦ (V i).subtype :
          (a : Π₀ (i : ι), ↥(V i)) → E)
        v⟫ =
    0
⊢ ⟪(↑((v : (a : ι) → ↥(V a)) i) : E), (↑((v : (a : ι) → ↥(V a)) i) : E)⟫ = 0

Tactic:
calc
    ⟪(v i : E), v i⟫ = ⟪(v i : E), DFinsupp.lsum ℕ (fun i => (V i).subtype) v⟫ := by
      simpa only [DFinsupp.sumAddHom_apply, DFinsupp.lsum_apply_apply] using
        (hV.inner_right_dfinsupp v i (v i)).symm
    _ = 0 := by simp only [hv, inner_zero_right]

Premises used: DFinsupp.lsum, Nat, Submodule.subtype, Subtype.val, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
h :
  Function.Injective (α := Π₀ (i : ι), ↥(V i)) (β := E)
    (⇑((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
          fun (i : ι) ↦ (V i).subtype) :
      (a : Π₀ (i : ι), ↥(V i)) → E)
h₁ :
  Eq (α := Submodule 𝕜 (Π₀ (i : ι), ↥(V i)))
    (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
      ((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
        fun (i : ι) ↦ (V i).subtype))
    ⊥
h₂ h₃ :
  ∀ (v : Π₀ (i : ι), ↥(V i))
    (hv :
      Membership.mem (γ := Submodule 𝕜 (Π₀ (i : ι), ↥(V i)))
        (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
          ((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
            fun (i : ι) ↦ (V i).subtype))
        v),
    v = 0
h₄ :
  ∀ (v : Π₀ (i : ι), ↥(V i))
    (hv :
      Eq.{u_2 + 1} (α := E)
        (((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
                fun (i : ι) ↦ (V i).subtype :
              (a : Π₀ (i : ι), ↥(V i)) → E)
            v :
          E)
        (0 : E)),
    v = 0
h₅ :
  ∀ (v : Π₀ (i : ι), ↥(V i))
    (hv :
      Eq.{u_2 + 1} (α := E)
        (((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
                fun (i : ι) ↦ (V i).subtype :
              (a : Π₀ (i : ι), ↥(V i)) → E)
            v :
          E)
        (0 : E))
    (i : ι), (↑((v : (a : ι) → ↥(V a)) i) : E) = (↑(((0 : Π₀ (i : ι), ↥(V i)) : (a : ι) → ↥(V a)) i) : E)
h₆ :
  ∀ (v : Π₀ (i : ι), ↥(V i))
    (hv :
      Eq.{u_2 + 1} (α := E)
        (((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
                fun (i : ι) ↦ (V i).subtype :
              (a : Π₀ (i : ι), ↥(V i)) → E)
            v :
          E)
        (0 : E))
    (i : ι), ⟪(↑((v : (a : ι) → ↥(V a)) i) : E), (↑((v : (a : ι) → ↥(V a)) i) : E)⟫ = 0
⊢ iSupIndep V

Tactic:
classical
  apply iSupIndep_of_dfinsupp_lsum_injective
  refine LinearMap.ker_eq_bot.mp ?_
  rw [Submodule.eq_bot_iff]
  intro v hv
  rw [LinearMap.mem_ker] at hv
  ext i
  suffices ⟪(v i : E), v i⟫ = 0 by simpa only [inner_self_eq_zero] using this
  calc
    ⟪(v i : E), v i⟫ = ⟪(v i : E), DFinsupp.lsum ℕ (fun i => (V i).subtype) v⟫ := by
      simpa only [DFinsupp.sumAddHom_apply, DFinsupp.lsum_apply_apply] using
        (hV.inner_right_dfinsupp v i (v i)).symm
    _ = 0 := by simp only [hv, inner_zero_right]

Premises used: LinearMap.ker_eq_bot, LinearMap.mem_ker, Iff.mp, iSupIndep_of_dfinsupp_lsum_injective, Submodule.eq_bot_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
hV_sum : IsInternal (S := Submodule 𝕜 E) fun (i : ι) ↦ V i
α : ι → Type u_6
v_family : (i : ι) → Basis.{u_6, u_1, u_2} (α i) 𝕜 ↥(V i)
hv_family : ∀ (i : ι), Orthonormal.{u_1, u_2, u_6} 𝕜 (E := ↥(V i)) (ι := α i) (⇑(v_family i) : (a : α i) → ↥(V i))
⊢ Orthonormal 𝕜 (E := E) (ι := (i : ι) × α i) (⇑(hV_sum.collectedBasis (α := α) v_family) : (a : (i : ι) × α i) → E)

Tactic:
simpa only [hV_sum.collectedBasis_coe] using hV.orthonormal_sigma_orthonormal hv_family

Premises used: OrthogonalFamily.orthonormal_sigma_orthonormal, DirectSum.IsInternal.collectedBasis_coe
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
⊢ T.IsSymmetric ↔ LinearMap.IsSelfAdjoint (M := E) (flip (innerₛₗ 𝕜)) (⇑T : (a : E) → E)

Tactic:
⟨fun h x y => (h y x).symm, fun h x y => (h y x).symm⟩

Premises used: Iff.intro, Eq.symm
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x, (T : (a : E) → E) y⟫ = ⟪(T : (a : E) → E) y, x⟫
rw₁ rw₂ : ⟪(T : (a : E) → E) y, x⟫ = ⟪(T : (a : E) → E) y, x⟫
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(T : (a : E) → E) x, y⟫ = ⟪(T : (a : E) → E) y, x⟫

Tactic:
rw [hT x y, inner_conj_symm]

Premises used: inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T : E →ₗ[𝕜] E).IsSymmetric
x y : E
⊢ ⟪(T : (a : E) → E) x, y⟫ = ⟪x, (T : (a : E) → E) y⟫

Tactic:
hT x y
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
⊢ IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) 0

Tactic:
fun x y =>
  (inner_zero_right x : ⟪x, 0⟫ = 0).symm ▸ (inner_zero_left y : ⟪0, y⟫ = 0)

Premises used: Eq.rec, inner_zero_left, inner_zero_right, LinearMap.IsSymmetric, Eq.symm
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
⊢ IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) id

Tactic:
fun _ _ ↦ rfl

Premises used: LinearMap.IsSymmetric, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
⊢ IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) 1

Tactic:
fun _ _ ↦ rfl

Premises used: LinearMap.IsSymmetric, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T S : E →ₗ[𝕜] E
hT : T.IsSymmetric
hS : S.IsSymmetric
x y : E
rw : ⟪HAdd.hAdd (α := E) (β := E) ((T : (a : E) → E) x : E) ((S : (a : E) → E) x : E), y⟫ = ⟪x, (T + S : (a : E) → E) y⟫
rw₁ : ⟪(T : (a : E) → E) x, y⟫ + ⟪(S : (a : E) → E) x, y⟫ = ⟪x, (T + S : (a : E) → E) y⟫
rw₂ : ⟪x, (T : (a : E) → E) y⟫ + ⟪(S : (a : E) → E) x, y⟫ = ⟪x, (T + S : (a : E) → E) y⟫
rw₃ : ⟪x, (T : (a : E) → E) y⟫ + ⟪x, (S : (a : E) → E) y⟫ = ⟪x, (T + S : (a : E) → E) y⟫
rw₄ :
  ⟪x, HAdd.hAdd (α := E) (β := E) ((T : (a : E) → E) y : E) ((S : (a : E) → E) y : E)⟫ = ⟪x, (T + S : (a : E) → E) y⟫
rw₅ rw₆ :
  ⟪x, HAdd.hAdd (α := E) (β := E) ((T : (a : E) → E) y : E) ((S : (a : E) → E) y : E)⟫ =
    ⟪x, HAdd.hAdd (α := E) (β := E) ((T : (a : E) → E) y : E) ((S : (a : E) → E) y : E)⟫
⊢ ⟪(T + S : (a : E) → E) x, y⟫ = ⟪x, (T + S : (a : E) → E) y⟫

Tactic:
rw [add_apply, inner_add_left, hT x y, hS x y, ← inner_add_right, add_apply]

Premises used: LinearMap.add_apply, inner_add_left, inner_add_right
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
T : ι → E →ₗ[𝕜] E
s : Finset ι
hT : ∀ i ∈ s, (T i).IsSymmetric
x x_1 : E
⊢ ⟪(∑ i ∈ s, T i : (a : E) → E) x, x_1⟫ = ⟪x, (∑ i ∈ s, T i : (a : E) → E) x_1⟫

Tactic:
simpa [sum_inner, inner_sum] using Finset.sum_congr rfl fun _ hi ↦ hT _ hi _ _

Premises used: inner_sum, sum_inner, Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T S : E →ₗ[𝕜] E
hT : T.IsSymmetric
hS : S.IsSymmetric
x y : E
rw : ⟪HSub.hSub (α := E) (β := E) ((T : (a : E) → E) x : E) ((S : (a : E) → E) x : E), y⟫ = ⟪x, (T - S : (a : E) → E) y⟫
rw₁ : ⟪(T : (a : E) → E) x, y⟫ - ⟪(S : (a : E) → E) x, y⟫ = ⟪x, (T - S : (a : E) → E) y⟫
rw₂ : ⟪x, (T : (a : E) → E) y⟫ - ⟪(S : (a : E) → E) x, y⟫ = ⟪x, (T - S : (a : E) → E) y⟫
rw₃ : ⟪x, (T : (a : E) → E) y⟫ - ⟪x, (S : (a : E) → E) y⟫ = ⟪x, (T - S : (a : E) → E) y⟫
rw₄ :
  ⟪x, HSub.hSub (α := E) (β := E) ((T : (a : E) → E) y : E) ((S : (a : E) → E) y : E)⟫ = ⟪x, (T - S : (a : E) → E) y⟫
rw₅ rw₆ :
  ⟪x, HSub.hSub (α := E) (β := E) ((T : (a : E) → E) y : E) ((S : (a : E) → E) y : E)⟫ =
    ⟪x, HSub.hSub (α := E) (β := E) ((T : (a : E) → E) y : E) ((S : (a : E) → E) y : E)⟫
⊢ ⟪(T - S : (a : E) → E) x, y⟫ = ⟪x, (T - S : (a : E) → E) y⟫

Tactic:
rw [sub_apply, inner_sub_left, hT x y, hS x y, ← inner_sub_right, sub_apply]

Premises used: inner_sub_left, inner_sub_right, LinearMap.sub_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
c : 𝕜
hc : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) c = c
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
⊢ ⟪(c • T : (a : E) → E) x, y⟫ = ⟪x, (c • T : (a : E) → E) y⟫

Tactic:
simp only [smul_apply, inner_smul_left, hc, hT x y, inner_smul_right]

Premises used: LinearMap.smul_apply, inner_smul_right, inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
n : ℕ
x y : E
⊢ ⟪((↑n : E →ₗ[𝕜] E) : (a : E) → E) x, y⟫ = ⟪x, ((↑n : E →ₗ[𝕜] E) : (a : E) → E) y⟫

Tactic:
simp [← Nat.cast_smul_eq_nsmul 𝕜, inner_smul_left, inner_smul_right]

Premises used: inner_smul_right, Nat.cast_smul_eq_nsmul, inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
n : ℤ
x y : E
⊢ ⟪((↑n : E →ₗ[𝕜] E) : (a : E) → E) x, y⟫ = ⟪x, ((↑n : E →ₗ[𝕜] E) : (a : E) → E) y⟫

Tactic:
simp [← Int.cast_smul_eq_zsmul 𝕜, inner_smul_left, inner_smul_right]

Premises used: inner_smul_right, Int.cast_smul_eq_zsmul, inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
S T : E →ₗ[𝕜] E
hS : S.IsSymmetric
hT : T.IsSymmetric
hST : Commute S T
x x_1 : E
rw : ⟪(S : (a : E) → E) ((T : (a : E) → E) x : E), x_1⟫ = ⟪x, (S * T : (a : E) → E) x_1⟫
rw₁ : inner 𝕜 (E := E) ((T : (a : E) → E) x : E) ((S : (a : E) → E) x_1 : E) = ⟪x, (S * T : (a : E) → E) x_1⟫
rw₂ : ⟪x, (T : (a : E) → E) ((S : (a : E) → E) x_1 : E)⟫ = ⟪x, (S * T : (a : E) → E) x_1⟫
rw₃ : ⟪x, (T : (a : E) → E) ((S : (a : E) → E) x_1 : E)⟫ = ⟪x, (T * S : (a : E) → E) x_1⟫
rw₄ rw₅ : ⟪x, (T : (a : E) → E) ((S : (a : E) → E) x_1 : E)⟫ = ⟪x, (T : (a : E) → E) ((S : (a : E) → E) x_1 : E)⟫
⊢ ⟪(S * T : (a : E) → E) x, x_1⟫ = ⟪x, (S * T : (a : E) → E) x_1⟫

Tactic:
rw [Module.End.mul_apply, hS, hT, hST, Module.End.mul_apply]

Premises used: Module.End.mul_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
n : ℕ
⊢ (HPow.hPow (β := ℕ) T 0).IsSymmetric

Tactic:
simp [Module.End.one_eq_id]

Premises used: Module.End.one_eq_id
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
n : ℕ
refine : ∀ (k : ℕ), 0 ≤ k → ∀ (ih : (T ^ k).IsSymmetric), (T ^ (k + 1)).IsSymmetric
⊢ (T ^ n).IsSymmetric

Tactic:
refine Nat.le_induction (by simp [Module.End.one_eq_id]) (fun k _ ih ↦ ?_) n n.zero_le
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
n k : ℕ
h : 0 ≤ k
ih : (T ^ k).IsSymmetric
rw : IsSymmetric (T ^ k * T)
⊢ (T ^ (k + 1)).IsSymmetric

Tactic:
rw [Module.End.iterate_succ, ← Module.End.mul_eq_comp]

Premises used: Module.End.mul_eq_comp, Module.End.iterate_succ
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
n k : ℕ
h : 0 ≤ k
ih : (T ^ k).IsSymmetric
⊢ IsSymmetric (T ^ k * T)

Tactic:
ih.mul_of_commute hT <| .pow_left rfl k

Premises used: Commute.pow_left, rfl, LinearMap.IsSymmetric.mul_of_commute
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
n k : ℕ
h : 0 ≤ k
ih : (T ^ k).IsSymmetric
⊢ IsSymmetric (T ^ k * T)

Tactic:
exact ih.mul_of_commute hT <| .pow_left rfl k

Premises used: LinearMap.IsSymmetric.mul_of_commute
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T : E →ₗ[𝕜] E).IsSymmetric
x : E
rsuffices :
  ∀ (r : ℝ) (hr : ⟪(T : (a : E) → E) x, x⟫ = (↑r : 𝕜)), (↑(T.reApplyInnerSelf x) : 𝕜) = ⟪(T : (a : E) → E) x, x⟫
rsuffices₁ : ∃ (r : ℝ), ⟪(T : (a : E) → E) x, x⟫ = (↑r : 𝕜)
⊢ (↑(T.reApplyInnerSelf x) : 𝕜) = ⟪(T : (a : E) → E) x, x⟫

Tactic:
rsuffices ⟨r, hr⟩ : ∃ r : ℝ, ⟪T x, x⟫ = r

Premises used: DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T : E →ₗ[𝕜] E).IsSymmetric
x : E
r : ℝ
hr : ⟪(T : (a : E) → E) x, x⟫ = (↑r : 𝕜)
⊢ (↑(T.reApplyInnerSelf x) : 𝕜) = ⟪(T : (a : E) → E) x, x⟫

Tactic:
simp [hr, T.reApplyInnerSelf_apply]

Premises used: ContinuousLinearMap.reApplyInnerSelf_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T : E →ₗ[𝕜] E).IsSymmetric
x : E
rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(T : (a : E) → E) x, x⟫ = ⟪(T : (a : E) → E) x, x⟫
⊢ ∃ (r : ℝ), ⟪(T : (a : E) → E) x, x⟫ = (↑r : 𝕜)

Tactic:
rw [← conj_eq_iff_real]

Premises used: RCLike.conj_eq_iff_real
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T : E →ₗ[𝕜] E).IsSymmetric
x : E
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(T : (a : E) → E) x, x⟫ = ⟪(T : (a : E) → E) x, x⟫

Tactic:
hT.conj_inner_sym x x

Premises used: LinearMap.IsSymmetric.conj_inner_sym
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T : E →ₗ[𝕜] E).IsSymmetric
x : E
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(T : (a : E) → E) x, x⟫ = ⟪(T : (a : E) → E) x, x⟫

Tactic:
exact hT.conj_inner_sym x x

Premises used: LinearMap.IsSymmetric.conj_inner_sym
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
V : Submodule 𝕜 E
hV : ∀ v ∈ V, Membership.mem (α := E) V ((T : (a : E) → E) v : E)
⊢ (T.restrict hV).IsSymmetric

Tactic:
fun v w => hT v w

Premises used: LinearMap.IsSymmetric, Subtype.val
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
⊢ inner ℝ
      (((↑ℝ :
              {S : Type u_1} →
                {M M₂ : Type u_2} →
                  [inst : Semiring ℝ] →
                    [inst_3 : Semiring S] →
                      [inst_4 : AddCommMonoid M] →
                        [inst_5 : AddCommMonoid M₂] →
                          [inst_6 : Module ℝ M] →
                            [inst_7 : Module ℝ M₂] →
                              [inst_8 : Module S M] →
                                [inst_9 : Module S M₂] → [CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
            T :
          (a : E) → E)
        x)
      y =
    inner ℝ x
      (((↑ℝ :
              {S : Type u_1} →
                {M M₂ : Type u_2} →
                  [inst : Semiring ℝ] →
                    [inst_3 : Semiring S] →
                      [inst_4 : AddCommMonoid M] →
                        [inst_5 : AddCommMonoid M₂] →
                          [inst_6 : Module ℝ M] →
                            [inst_7 : Module ℝ M₂] →
                              [inst_8 : Module S M] →
                                [inst_9 : Module S M₂] → [CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
            T :
          (a : E) → E)
        y)

Tactic:
simp [hT x y, real_inner_eq_re_inner, LinearMap.coe_restrictScalars ℝ]

Premises used: Real, LinearMap.coe_restrictScalars, real_inner_eq_re_inner
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x : E
⊢ Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫ : ℝ) (0 : ℝ)

Tactic:
conj_eq_iff_im.mp <| hT.conj_inner_sym x x

Premises used: RCLike.conj_eq_iff_im, Iff.mp, LinearMap.IsSymmetric.conj_inner_sym
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x : E
⊢ Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) ⟪x, (T : (a : E) → E) x⟫ : ℝ) (0 : ℝ)

Tactic:
simp [← hT x x, hT]
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x : E
⊢ (↑((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫) : 𝕜) = ⟪(T : (a : E) → E) x, x⟫

Tactic:
conj_eq_iff_re.mp <| hT.conj_inner_sym x x

Premises used: RCLike.conj_eq_iff_re, Iff.mp, LinearMap.IsSymmetric.conj_inner_sym
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x : E
⊢ (↑((re : (a : 𝕜) → ℝ) ⟪x, (T : (a : E) → E) x⟫) : 𝕜) = ⟪x, (T : (a : E) → E) x⟫

Tactic:
simp [← hT x x, hT]
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
V : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
mp : T.IsSymmetric → ∀ (v : V), (starRingEnd ℂ : (a : ℂ) → ℂ) ⟪(T : (a : V) → V) v, v⟫_ℂ = ⟪(T : (a : V) → V) v, v⟫_ℂ
mpr : (∀ (v : V), (starRingEnd ℂ : (a : ℂ) → ℂ) ⟪(T : (a : V) → V) v, v⟫_ℂ = ⟪(T : (a : V) → V) v, v⟫_ℂ) → T.IsSymmetric
⊢ T.IsSymmetric ↔ ∀ (v : V), (starRingEnd ℂ : (a : ℂ) → ℂ) ⟪(T : (a : V) → V) v, v⟫_ℂ = ⟪(T : (a : V) → V) v, v⟫_ℂ

Tactic:
constructor
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
V : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
hT : T.IsSymmetric
v : V
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) ⟪(T : (a : V) → V) v, v⟫_ℂ = ⟪(T : (a : V) → V) v, v⟫_ℂ

Tactic:
apply IsSymmetric.conj_inner_sym hT

Premises used: LinearMap.IsSymmetric.conj_inner_sym
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
V : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), (starRingEnd ℂ : (a : ℂ) → ℂ) ⟪(T : (a : V) → V) v, v⟫_ℂ = ⟪(T : (a : V) → V) v, v⟫_ℂ
x y : V
mpr : ⟪(T : (a : V) → V) x, y⟫_ℂ = (starRingEnd ℂ : (a : ℂ) → ℂ) ⟪(T : (a : V) → V) y, x⟫_ℂ
⊢ ⟪(T : (a : V) → V) x, y⟫_ℂ = ⟪x, (T : (a : V) → V) y⟫_ℂ

Tactic:
rw [← inner_conj_symm x (T y)]

Premises used: DFunLike.coe, inner_conj_symm