awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) (x + y), x + y⟫_ℂ - ⟪(T : (a : V) → V) (x - y), x - y⟫_ℂ +
            Complex.I * ⟪(T : (a : V) → V) (x + Complex.I • y), x + Complex.I • y⟫_ℂ -
          Complex.I * ⟪(T : (a : V) → V) (x - Complex.I • y), x - Complex.I • y⟫_ℂ) /
        4)
⊢ ⟪(T : (a : V) → V) x, y⟫_ℂ = (starRingEnd ℂ : (a : ℂ) → ℂ) ⟪(T : (a : V) → V) y, x⟫_ℂ

Tactic:
rw [inner_map_polarization T x y]

Premises used: inner_map_polarization
-- 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⟫_ℂ =
    (star ⟪(T : (a : V) → V) (x + y), x + y⟫_ℂ - star ⟪(T : (a : V) → V) (x - y), x - y⟫_ℂ +
          star ⟪(T : (a : V) → V) (x + Complex.I • y), x + Complex.I • y⟫_ℂ * star Complex.I -
        star ⟪(T : (a : V) → V) (x - Complex.I • y), x - Complex.I • y⟫_ℂ * star Complex.I) /
      star 4
⊢ ⟪(T : (a : V) → V) x, y⟫_ℂ =
    (starRingEnd ℂ : (a : ℂ) → ℂ)
      ((⟪(T : (a : V) → V) (x + y), x + y⟫_ℂ - ⟪(T : (a : V) → V) (x - y), x - y⟫_ℂ +
            Complex.I * ⟪(T : (a : V) → V) (x + Complex.I • y), x + Complex.I • y⟫_ℂ -
          Complex.I * ⟪(T : (a : V) → V) (x - Complex.I • y), x - Complex.I • y⟫_ℂ) /
        4)

Tactic:
simp only [starRingEnd_apply, star_div₀, star_sub, star_add, star_mul]

Premises used: StarAddMonoid.star_add, starRingEnd_apply, StarMul.star_mul, star_sub, star_div₀
-- 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⟫_ℂ =
    HDiv.hDiv (β := ℂ)
      (⟪(T : (a : V) → V) (x + y), x + y⟫_ℂ - ⟪(T : (a : V) → V) (x - y), x - y⟫_ℂ +
          HMul.hMul (β := ℂ) ⟪(T : (a : V) → V) (x + Complex.I • y), x + Complex.I • y⟫_ℂ
            ((starRingEnd ℂ : (a : ℂ) → ℂ) Complex.I : ℂ) -
        HMul.hMul (β := ℂ) ⟪(T : (a : V) → V) (x - Complex.I • y), x - Complex.I • y⟫_ℂ
          ((starRingEnd ℂ : (a : ℂ) → ℂ) Complex.I : ℂ))
      ((starRingEnd ℂ : (a : ℂ) → ℂ) 4 : ℂ)
⊢ ⟪(T : (a : V) → V) x, y⟫_ℂ =
    HDiv.hDiv (β := ℂ)
      (HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ⟪(T : (a : V) → V) (x + y), x + y⟫_ℂ : ℂ)
            ((starRingEnd ℂ : (a : ℂ) → ℂ) ⟪(T : (a : V) → V) (x - y), x - y⟫_ℂ : ℂ) +
          HMul.hMul (α := ℂ) (β := ℂ)
            ((starRingEnd ℂ : (a : ℂ) → ℂ) ⟪(T : (a : V) → V) (x + Complex.I • y), x + Complex.I • y⟫_ℂ : ℂ)
            ((starRingEnd ℂ : (a : ℂ) → ℂ) Complex.I : ℂ) -
        HMul.hMul (α := ℂ) (β := ℂ)
          ((starRingEnd ℂ : (a : ℂ) → ℂ) ⟪(T : (a : V) → V) (x - Complex.I • y), x - Complex.I • y⟫_ℂ : ℂ)
          ((starRingEnd ℂ : (a : ℂ) → ℂ) Complex.I : ℂ))
      ((starRingEnd ℂ : (a : ℂ) → ℂ) 4 : ℂ)

Tactic:
rw [h (x + y), h (x - y), h (x + Complex.I • y), h (x - Complex.I • y)]

Premises used: HSub.hSub, HAdd.hAdd, HSMul.hSMul, Complex.I
-- 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⟫_ℂ =
    HDiv.hDiv (β := ℂ)
      (⟪(T : (a : V) → V) (x + y), x + y⟫_ℂ - ⟪(T : (a : V) → V) (x - y), x - y⟫_ℂ +
          ⟪(T : (a : V) → V) (x + Complex.I • y), x + Complex.I • y⟫_ℂ * -Complex.I -
        ⟪(T : (a : V) → V) (x - Complex.I • y), x - Complex.I • y⟫_ℂ * -Complex.I)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) 4 : ℂ)
⊢ ⟪(T : (a : V) → V) x, y⟫_ℂ =
    HDiv.hDiv (β := ℂ)
      (⟪(T : (a : V) → V) (x + y), x + y⟫_ℂ - ⟪(T : (a : V) → V) (x - y), x - y⟫_ℂ +
          HMul.hMul (β := ℂ) ⟪(T : (a : V) → V) (x + Complex.I • y), x + Complex.I • y⟫_ℂ
            ((starRingEnd ℂ : (a : ℂ) → ℂ) Complex.I : ℂ) -
        HMul.hMul (β := ℂ) ⟪(T : (a : V) → V) (x - Complex.I • y), x - Complex.I • y⟫_ℂ
          ((starRingEnd ℂ : (a : ℂ) → ℂ) Complex.I : ℂ))
      ((starRingEnd ℂ : (a : ℂ) → ℂ) 4 : ℂ)

Tactic:
simp only [Complex.conj_I]

Premises used: Complex.conj_I
-- 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), x + y⟫_ℂ - ⟪(T : (a : V) → V) (x - y), x - y⟫_ℂ -
          Complex.I * ⟪(T : (a : V) → V) (x + Complex.I • y), x + Complex.I • y⟫_ℂ +
        Complex.I * ⟪(T : (a : V) → V) (x - Complex.I • y), x - Complex.I • y⟫_ℂ) /
      4 =
    HDiv.hDiv (β := ℂ)
      (⟪(T : (a : V) → V) (x + y), x + y⟫_ℂ - ⟪(T : (a : V) → V) (x - y), x - y⟫_ℂ +
          ⟪(T : (a : V) → V) (x + Complex.I • y), x + Complex.I • y⟫_ℂ * -Complex.I -
        ⟪(T : (a : V) → V) (x - Complex.I • y), x - Complex.I • y⟫_ℂ * -Complex.I)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) 4 : ℂ)
⊢ ⟪(T : (a : V) → V) x, y⟫_ℂ =
    HDiv.hDiv (β := ℂ)
      (⟪(T : (a : V) → V) (x + y), x + y⟫_ℂ - ⟪(T : (a : V) → V) (x - y), x - y⟫_ℂ +
          ⟪(T : (a : V) → V) (x + Complex.I • y), x + Complex.I • y⟫_ℂ * -Complex.I -
        ⟪(T : (a : V) → V) (x - Complex.I • y), x - Complex.I • y⟫_ℂ * -Complex.I)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) 4 : ℂ)

Tactic:
rw [inner_map_polarization']

Premises used: inner_map_polarization'
-- 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 :
  ⟪HAdd.hAdd (α := V) (β := V) ((T : (a : V) → V) x : V) ((T : (a : V) → V) y : V), x + y⟫_ℂ -
          ⟪HSub.hSub (α := V) (β := V) ((T : (a : V) → V) x : V) ((T : (a : V) → V) y : V), x - y⟫_ℂ -
        Complex.I *
          ⟪HAdd.hAdd (α := V) ((T : (a : V) → V) x : V) (HSMul.hSMul (β := V) Complex.I ((T : (a : V) → V) y : V)),
            x + Complex.I • y⟫_ℂ +
      Complex.I *
        ⟪HSub.hSub (α := V) ((T : (a : V) → V) x : V) (HSMul.hSMul (β := V) Complex.I ((T : (a : V) → V) y : V)),
          x - Complex.I • y⟫_ℂ =
    ⟪HAdd.hAdd (α := V) (β := V) ((T : (a : V) → V) x : V) ((T : (a : V) → V) y : V), x + y⟫_ℂ -
          ⟪HSub.hSub (α := V) (β := V) ((T : (a : V) → V) x : V) ((T : (a : V) → V) y : V), x - y⟫_ℂ +
        -(⟪HAdd.hAdd (α := V) ((T : (a : V) → V) x : V) (HSMul.hSMul (β := V) Complex.I ((T : (a : V) → V) y : V)),
              x + Complex.I • y⟫_ℂ *
            Complex.I) +
      ⟪HSub.hSub (α := V) ((T : (a : V) → V) x : V) (HSMul.hSMul (β := V) Complex.I ((T : (a : V) → V) y : V)),
          x - Complex.I • y⟫_ℂ *
        Complex.I
⊢ (⟪(T : (a : V) → V) (x + y), x + y⟫_ℂ - ⟪(T : (a : V) → V) (x - y), x - y⟫_ℂ -
          Complex.I * ⟪(T : (a : V) → V) (x + Complex.I • y), x + Complex.I • y⟫_ℂ +
        Complex.I * ⟪(T : (a : V) → V) (x - Complex.I • y), x - Complex.I • y⟫_ℂ) /
      4 =
    HDiv.hDiv (β := ℂ)
      (⟪(T : (a : V) → V) (x + y), x + y⟫_ℂ - ⟪(T : (a : V) → V) (x - y), x - y⟫_ℂ +
          ⟪(T : (a : V) → V) (x + Complex.I • y), x + Complex.I • y⟫_ℂ * -Complex.I -
        ⟪(T : (a : V) → V) (x - Complex.I • y), x - Complex.I • y⟫_ℂ * -Complex.I)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) 4 : ℂ)

Tactic:
norm_num
-- 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
⊢ ⟪HAdd.hAdd (α := V) (β := V) ((T : (a : V) → V) x : V) ((T : (a : V) → V) y : V), x + y⟫_ℂ -
          ⟪HSub.hSub (α := V) (β := V) ((T : (a : V) → V) x : V) ((T : (a : V) → V) y : V), x - y⟫_ℂ -
        Complex.I *
          ⟪HAdd.hAdd (α := V) ((T : (a : V) → V) x : V) (HSMul.hSMul (β := V) Complex.I ((T : (a : V) → V) y : V)),
            x + Complex.I • y⟫_ℂ +
      Complex.I *
        ⟪HSub.hSub (α := V) ((T : (a : V) → V) x : V) (HSMul.hSMul (β := V) Complex.I ((T : (a : V) → V) y : V)),
          x - Complex.I • y⟫_ℂ =
    ⟪HAdd.hAdd (α := V) (β := V) ((T : (a : V) → V) x : V) ((T : (a : V) → V) y : V), x + y⟫_ℂ -
          ⟪HSub.hSub (α := V) (β := V) ((T : (a : V) → V) x : V) ((T : (a : V) → V) y : V), x - y⟫_ℂ +
        -(⟪HAdd.hAdd (α := V) ((T : (a : V) → V) x : V) (HSMul.hSMul (β := V) Complex.I ((T : (a : V) → V) y : V)),
              x + Complex.I • y⟫_ℂ *
            Complex.I) +
      ⟪HSub.hSub (α := V) ((T : (a : V) → V) x : V) (HSMul.hSMul (β := V) Complex.I ((T : (a : V) → V) y : V)),
          x - Complex.I • y⟫_ℂ *
        Complex.I

Tactic:
ring
-- 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
inl :
  ∀ (h : Eq.{u_1 + 1} (α := 𝕜) I 0),
    ⟪(T : (a : E) → E) x, y⟫ =
      (⟪(T : (a : E) → E) (x + y), x + y⟫ - ⟪(T : (a : E) → E) (x - y), x - y⟫ -
            I *
              ⟪(T : (a : E) → E) (x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y),
                x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y⟫ +
          I *
            ⟪(T : (a : E) → E) (x - HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y),
              x - HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y⟫) /
        4
inr :
  ∀ (h : HMul.hMul (α := 𝕜) I I = -1),
    ⟪(T : (a : E) → E) x, y⟫ =
      (⟪(T : (a : E) → E) (x + y), x + y⟫ - ⟪(T : (a : E) → E) (x - y), x - y⟫ -
            I *
              ⟪(T : (a : E) → E) (x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y),
                x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y⟫ +
          I *
            ⟪(T : (a : E) → E) (x - HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y),
              x - HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y⟫) /
        4
⊢ ⟪(T : (a : E) → E) x, y⟫ =
    (⟪(T : (a : E) → E) (x + y), x + y⟫ - ⟪(T : (a : E) → E) (x - y), x - y⟫ -
          I *
            ⟪(T : (a : E) → E) (x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y),
              x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y⟫ +
        I *
          ⟪(T : (a : E) → E) (x - HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y),
            x - HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y⟫) /
      4

Tactic:
rcases @I_mul_I_ax 𝕜 _ with (h | h)

Premises used: RCLike.I_mul_I_ax
-- 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
h : Eq.{u_1 + 1} (α := 𝕜) I 0
inl :
  (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(T : (a : E) → E) y, x⟫ =
    (HAdd.hAdd (β := 𝕜) ⟪x, (T : (a : E) → E) x⟫ ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(T : (a : E) → E) y, x⟫ : 𝕜) +
          (⟪(T : (a : E) → E) y, x⟫ + ⟪(T : (a : E) → E) y, y⟫) -
        (HSub.hSub (β := 𝕜) ⟪x, (T : (a : E) → E) x⟫ ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(T : (a : E) → E) y, x⟫ : 𝕜) -
          (⟪(T : (a : E) → E) y, x⟫ - ⟪(T : (a : E) → E) y, y⟫))) /
      4
⊢ ⟪(T : (a : E) → E) x, y⟫ =
    (⟪(T : (a : E) → E) (x + y), x + y⟫ - ⟪(T : (a : E) → E) (x - y), x - y⟫ -
          I *
            ⟪(T : (a : E) → E) (x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y),
              x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y⟫ +
        I *
          ⟪(T : (a : E) → E) (x - HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y),
            x - HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y⟫) /
      4

Tactic:
simp_rw [h, zero_mul, sub_zero, add_zero, map_add, map_sub, inner_add_left,
      inner_add_right, inner_sub_left, inner_sub_right, hT x, ← inner_conj_symm x (T y)]

Premises used: map_sub, sub_zero, MulZeroClass.zero_mul, map_add, inner_add_left, inner_add_right, inner_sub_left, inner_sub_right, add_zero, DFunLike.coe, 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 →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
h : Eq.{u_1 + 1} (α := 𝕜) I 0
this : (↑((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) y, x⟫) : 𝕜) = ⟪(T : (a : E) → E) y, x⟫
rw :
  ⟪(T : (a : E) → E) y, x⟫ =
    (⟪x, (T : (a : E) → E) x⟫ + ⟪(T : (a : E) → E) y, x⟫ + (⟪(T : (a : E) → E) y, x⟫ + ⟪(T : (a : E) → E) y, y⟫) -
        (⟪x, (T : (a : E) → E) x⟫ - ⟪(T : (a : E) → E) y, x⟫ - (⟪(T : (a : E) → E) y, x⟫ - ⟪(T : (a : E) → E) y, y⟫))) /
      4
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(T : (a : E) → E) y, x⟫ =
    (HAdd.hAdd (β := 𝕜) ⟪x, (T : (a : E) → E) x⟫ ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(T : (a : E) → E) y, x⟫ : 𝕜) +
          (⟪(T : (a : E) → E) y, x⟫ + ⟪(T : (a : E) → E) y, y⟫) -
        (HSub.hSub (β := 𝕜) ⟪x, (T : (a : E) → E) x⟫ ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(T : (a : E) → E) y, x⟫ : 𝕜) -
          (⟪(T : (a : E) → E) y, x⟫ - ⟪(T : (a : E) → E) y, y⟫))) /
      4

Tactic:
rw [conj_eq_iff_re.mpr this]

Premises used: Iff.mpr, RCLike.conj_eq_iff_re
-- 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
h : Eq.{u_1 + 1} (α := 𝕜) I 0
this : (↑((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) y, x⟫) : 𝕜) = ⟪(T : (a : E) → E) y, x⟫
⊢ ⟪(T : (a : E) → E) y, x⟫ =
    (⟪x, (T : (a : E) → E) x⟫ + ⟪(T : (a : E) → E) y, x⟫ + (⟪(T : (a : E) → E) y, x⟫ + ⟪(T : (a : E) → E) y, y⟫) -
        (⟪x, (T : (a : E) → E) x⟫ - ⟪(T : (a : E) → E) y, x⟫ - (⟪(T : (a : E) → E) y, x⟫ - ⟪(T : (a : E) → E) y, y⟫))) /
      4

Tactic:
ring
-- 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
h : Eq.{u_1 + 1} (α := 𝕜) I 0
inl : (↑((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) y, x⟫) : 𝕜) = ⟪(T : (a : E) → E) y, x⟫
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(T : (a : E) → E) y, x⟫ =
    (HAdd.hAdd (β := 𝕜) ⟪x, (T : (a : E) → E) x⟫ ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(T : (a : E) → E) y, x⟫ : 𝕜) +
          (⟪(T : (a : E) → E) y, x⟫ + ⟪(T : (a : E) → E) y, y⟫) -
        (HSub.hSub (β := 𝕜) ⟪x, (T : (a : E) → E) x⟫ ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(T : (a : E) → E) y, x⟫ : 𝕜) -
          (⟪(T : (a : E) → E) y, x⟫ - ⟪(T : (a : E) → E) y, y⟫))) /
      4

Tactic:
suffices (re ⟪T y, x⟫ : 𝕜) = ⟪T y, x⟫ by
      rw [conj_eq_iff_re.mpr this]
      ring
-- 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
h : Eq.{u_1 + 1} (α := 𝕜) I 0
inl :
  (↑((re : (a : 𝕜) → ℝ)
          ((↑((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) y, x⟫) : 𝕜) +
            HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) y, x⟫) : 𝕜) I)) :
      𝕜) =
    (↑((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) y, x⟫) : 𝕜) +
      HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) y, x⟫) : 𝕜) I
⊢ (↑((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) y, x⟫) : 𝕜) = ⟪(T : (a : E) → E) y, x⟫

Tactic:
rw [← re_add_im ⟪T y, x⟫]
-- 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
h : Eq.{u_1 + 1} (α := 𝕜) I 0
inl :
  Eq.{u_1 + 1} (α := 𝕜) (↑((re : (a : 𝕜) → ℝ) (↑((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) y, x⟫) : 𝕜)) : 𝕜)
    (↑((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) y, x⟫) : 𝕜)
⊢ (↑((re : (a : 𝕜) → ℝ)
          ((↑((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) y, x⟫) : 𝕜) +
            HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) y, x⟫) : 𝕜) I)) :
      𝕜) =
    (↑((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) y, x⟫) : 𝕜) +
      HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) y, x⟫) : 𝕜) I

Tactic:
simp_rw [h, mul_zero, add_zero]

Premises used: MulZeroClass.mul_zero, add_zero
-- 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
h : Eq.{u_1 + 1} (α := 𝕜) I 0
inl inl₁ inl₂ inl₃ :
  Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) y, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) y, x⟫ : ℝ)
⊢ Eq.{u_1 + 1} (α := 𝕜) (↑((re : (a : 𝕜) → ℝ) (↑((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) y, x⟫) : 𝕜)) : 𝕜)
    (↑((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) y, x⟫) : 𝕜)

Tactic:
norm_cast
-- 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
h : HMul.hMul (α := 𝕜) I I = -1
inr :
  ⟪(T : (a : E) → E) x, y⟫ =
    (⟪(T : (a : E) → E) x, x⟫ + ⟪(T : (a : E) → E) x, y⟫ + (⟪(T : (a : E) → E) y, x⟫ + ⟪(T : (a : E) → E) y, y⟫) -
          (⟪(T : (a : E) → E) x, x⟫ -
              (⟪(T : (a : E) → E) x, y⟫ + (⟪(T : (a : E) → E) y, x⟫ - ⟪(T : (a : E) → E) y, y⟫)) +
            (I * ⟪(T : (a : E) → E) x, x⟫ + -⟪(T : (a : E) → E) x, y⟫ +
              (⟪(T : (a : E) → E) y, x⟫ + I * ⟪(T : (a : E) → E) y, y⟫))) +
        (I * ⟪(T : (a : E) → E) x, x⟫ -
          (-⟪(T : (a : E) → E) x, y⟫ + (⟪(T : (a : E) → E) y, x⟫ - I * ⟪(T : (a : E) → E) y, y⟫)))) /
      4
⊢ ⟪(T : (a : E) → E) x, y⟫ =
    (⟪(T : (a : E) → E) (x + y), x + y⟫ - ⟪(T : (a : E) → E) (x - y), x - y⟫ -
          I *
            ⟪(T : (a : E) → E) (x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y),
              x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y⟫ +
        I *
          ⟪(T : (a : E) → E) (x - HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y),
            x - HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y⟫) /
      4

Tactic:
simp_rw [map_add, map_sub, inner_add_left, inner_add_right, inner_sub_left, inner_sub_right,
      map_smul, inner_smul_left, inner_smul_right, RCLike.conj_I, mul_add, mul_sub, sub_sub,
      ← mul_assoc, mul_neg, h, neg_neg, one_mul, neg_one_mul]

Premises used: map_sub, mul_sub, mul_assoc, neg_one_mul, map_add, neg_neg, inner_add_left, inner_add_right, inner_sub_left, sub_sub, inner_smul_right, RCLike.conj_I, inner_sub_right, mul_add, one_mul, mul_neg, map_smul, 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
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
h : HMul.hMul (α := 𝕜) I I = -1
⊢ ⟪(T : (a : E) → E) x, y⟫ =
    (⟪(T : (a : E) → E) x, x⟫ + ⟪(T : (a : E) → E) x, y⟫ + (⟪(T : (a : E) → E) y, x⟫ + ⟪(T : (a : E) → E) y, y⟫) -
          (⟪(T : (a : E) → E) x, x⟫ -
              (⟪(T : (a : E) → E) x, y⟫ + (⟪(T : (a : E) → E) y, x⟫ - ⟪(T : (a : E) → E) y, y⟫)) +
            (I * ⟪(T : (a : E) → E) x, x⟫ + -⟪(T : (a : E) → E) x, y⟫ +
              (⟪(T : (a : E) → E) y, x⟫ + I * ⟪(T : (a : E) → E) y, y⟫))) +
        (I * ⟪(T : (a : E) → E) x, x⟫ -
          (-⟪(T : (a : E) → E) x, y⟫ + (⟪(T : (a : E) → E) y, x⟫ - I * ⟪(T : (a : E) → E) y, y⟫)))) /
      4

Tactic:
ring
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ[𝕜] E
f : E ≃ₗᵢ[𝕜] F
⊢ ((↑f.toLinearEquiv : E →ₗ[𝕜] F) ∘ₗ T ∘ₗ (↑f.symm.toLinearEquiv : F →ₗ[𝕜] E)).IsSymmetric ↔ T.IsSymmetric

Tactic:
⟨fun h x y => ?_, fun h x y => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ[𝕜] E
f : E ≃ₗᵢ[𝕜] F
refine_1 :
  ∀ (h : ((↑f.toLinearEquiv : E →ₗ[𝕜] F) ∘ₗ T ∘ₗ (↑f.symm.toLinearEquiv : F →ₗ[𝕜] E)).IsSymmetric) (x y : E),
    ⟪(T : (a : E) → E) x, y⟫ = ⟪x, (T : (a : E) → E) y⟫
refine_2 :
  ∀ (h : T.IsSymmetric) (x y : F),
    ⟪((↑f.toLinearEquiv : E →ₗ[𝕜] F) ∘ₗ T ∘ₗ (↑f.symm.toLinearEquiv : F →ₗ[𝕜] E) : (a : F) → F) x, y⟫ =
      ⟪x, ((↑f.toLinearEquiv : E →ₗ[𝕜] F) ∘ₗ T ∘ₗ (↑f.symm.toLinearEquiv : F →ₗ[𝕜] E) : (a : F) → F) y⟫
⊢ ((↑f.toLinearEquiv : E →ₗ[𝕜] F) ∘ₗ T ∘ₗ (↑f.symm.toLinearEquiv : F →ₗ[𝕜] E)).IsSymmetric ↔ T.IsSymmetric

Tactic:
refine ⟨fun h x y => ?_, fun h 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
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ[𝕜] E
f : E ≃ₗᵢ[𝕜] F
h : ((↑f.toLinearEquiv : E →ₗ[𝕜] F) ∘ₗ T ∘ₗ (↑f.symm.toLinearEquiv : F →ₗ[𝕜] E)).IsSymmetric
x y : E
⊢ ⟪(T : (a : E) → E) x, y⟫ = ⟪x, (T : (a : E) → E) y⟫

Tactic:
simpa [LinearIsometryEquiv.inner_map_eq_flip] using h (f x) (f y)

Premises used: LinearIsometryEquiv.inner_map_eq_flip, 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
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ[𝕜] E
f : E ≃ₗᵢ[𝕜] F
h : T.IsSymmetric
x y : F
⊢ ⟪((↑f.toLinearEquiv : E →ₗ[𝕜] F) ∘ₗ T ∘ₗ (↑f.symm.toLinearEquiv : F →ₗ[𝕜] E) : (a : F) → F) x, y⟫ =
    ⟪x, ((↑f.toLinearEquiv : E →ₗ[𝕜] F) ∘ₗ T ∘ₗ (↑f.symm.toLinearEquiv : F →ₗ[𝕜] E) : (a : F) → F) y⟫

Tactic:
simp [LinearIsometryEquiv.inner_map_eq_flip, h _ (f.symm y)]

Premises used: LinearIsometryEquiv.symm, LinearIsometryEquiv.inner_map_eq_flip, 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
x x_1 x_2 : E
⊢ ⟪((↑((((rankOne 𝕜 : (a : E) → E →L⋆[𝕜] E →L[𝕜] E) x : E →L⋆[𝕜] E →L[𝕜] E) : (a : E) → E →L[𝕜] E) x) : E →ₗ[𝕜] E) :
          (a : E) → E)
        x_1,
      x_2⟫_𝕜 =
    ⟪x_1,
      ((↑((((rankOne 𝕜 : (a : E) → E →L⋆[𝕜] E →L[𝕜] E) x : E →L⋆[𝕜] E →L[𝕜] E) : (a : E) → E →L[𝕜] E) x) : E →ₗ[𝕜] E) :
          (a : E) → E)
        x_2⟫_𝕜

Tactic:
simp [inner_smul_left, inner_smul_right, mul_comm]

Premises used: inner_smul_right, mul_comm, 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
T : E ≃ₗ[𝕜] E
hT : (↑T : E →ₗ[𝕜] E).IsSymmetric
x y : E
⊢ ⟪((↑T.symm : E →ₗ[𝕜] E) : (a : E) → E) x, y⟫ = ⟪x, ((↑T.symm : E →ₗ[𝕜] E) : (a : E) → E) y⟫

Tactic:
simpa using hT (T.symm x) (T.symm y) |>.symm

Premises used: LinearEquiv.symm, Eq.symm, 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 ≃ₗ[𝕜] E
⊢ (↑T.symm : E →ₗ[𝕜] E).IsSymmetric ↔ (↑T : E →ₗ[𝕜] E).IsSymmetric

Tactic:
⟨.toLinearMap_symm, .toLinearMap_symm⟩

Premises used: LinearMap.IsSymmetric.toLinearMap_symm, Iff.intro
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
⊢ Continuous (X := E) (Y := E) (⇑T : (a : E) → E)

Tactic:
T.continuous_of_seq_closed_graph fun u x y hu hTu => ?_

Premises used: LinearMap.continuous_of_seq_closed_graph