awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
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⟫
⊢ ⟪(T - S : (a : E) → E) x, y⟫ = ⟪x, (T - S : (a : E) → E) y⟫
have 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)⟫
Tactic: rw [sub_apply, inner_sub_left, hT x y, hS x y, ← inner_sub_right, sub_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
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
⊢ ⟪(S * T : (a : E) → E) x, x_1⟫ = ⟪x, (S * T : (a : E) → E) x_1⟫
have rw : ⟪(S : (a : E) → E) ((T : (a : E) → E) x : E), x_1⟫ = ⟪x, (S * T : (a : E) → E) x_1⟫
Tactic: rw [Module.End.mul_apply, hS, hT, hST, Module.End.mul_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
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⟫
⊢ ⟪(S * T : (a : E) → E) x, x_1⟫ = ⟪x, (S * T : (a : E) → E) x_1⟫
have 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⟫
Tactic: rw [Module.End.mul_apply, hS, hT, hST, Module.End.mul_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
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⟫
⊢ ⟪(S * T : (a : E) → E) x, x_1⟫ = ⟪x, (S * T : (a : E) → E) x_1⟫
have rw₂ : ⟪x, (T : (a : E) → E) ((S : (a : E) → E) x_1 : E)⟫ = ⟪x, (S * T : (a : E) → E) x_1⟫
Tactic: rw [Module.End.mul_apply, hS, hT, hST, Module.End.mul_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
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⟫
⊢ ⟪(S * T : (a : E) → E) x, x_1⟫ = ⟪x, (S * T : (a : E) → E) x_1⟫
have rw₃ : ⟪x, (T : (a : E) → E) ((S : (a : E) → E) x_1 : E)⟫ = ⟪x, (T * S : (a : E) → E) x_1⟫
Tactic: rw [Module.End.mul_apply, hS, hT, hST, Module.End.mul_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
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⟫
⊢ ⟪(S * T : (a : E) → E) x, x_1⟫ = ⟪x, (S * T : (a : E) → E) x_1⟫
have 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)⟫
Tactic: rw [Module.End.mul_apply, hS, hT, hST, Module.End.mul_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
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 : ℕ
⊢ (T ^ n).IsSymmetric
have refine : ∀ (k : ℕ), 0 ≤ k → ∀ (ih : (T ^ k).IsSymmetric), (T ^ (k + 1)).IsSymmetric
Tactic: refine Nat.le_induction (by simp [Module.End.one_eq_id]) (fun k _ ih ↦ ?_) n n.zero_le
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
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
⊢ (T ^ (k + 1)).IsSymmetric
have rw : IsSymmetric (T ^ k * T)
Tactic: rw [Module.End.iterate_succ, ← Module.End.mul_eq_comp]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
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
⊢ (↑(T.reApplyInnerSelf x) : 𝕜) = ⟪(T : (a : E) → E) x, x⟫
have rsuffices : ∀ (r : ℝ) (hr : ⟪(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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
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⟫
⊢ (↑(T.reApplyInnerSelf x) : 𝕜) = ⟪(T : (a : E) → E) x, x⟫
have rsuffices₁ : ∃ (r : ℝ), ⟪(T : (a : E) → E) x, x⟫ = (↑r : 𝕜)
Tactic: rsuffices ⟨r, hr⟩ : ∃ r : ℝ, ⟪T x, x⟫ = r
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
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 : ℝ), ⟪(T : (a : E) → E) x, x⟫ = (↑r : 𝕜)
have rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(T : (a : E) → E) x, x⟫ = ⟪(T : (a : E) → E) x, x⟫
Tactic: rw [← conj_eq_iff_real]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
Goal:
V : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
⊢ T.IsSymmetric ↔ ∀ (v : V), (starRingEnd ℂ : (a : ℂ) → ℂ) ⟪(T : (a : V) → V) v, v⟫_ℂ = ⟪(T : (a : V) → V) v, v⟫_ℂ
have mp : T.IsSymmetric → ∀ (v : V), (starRingEnd ℂ : (a : ℂ) → ℂ) ⟪(T : (a : V) → V) v, v⟫_ℂ = ⟪(T : (a : V) → V) v, v⟫_ℂ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
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⟫_ℂ
⊢ T.IsSymmetric ↔ ∀ (v : V), (starRingEnd ℂ : (a : ℂ) → ℂ) ⟪(T : (a : V) → V) v, v⟫_ℂ = ⟪(T : (a : V) → V) v, v⟫_ℂ
have mpr : (∀ (v : V), (starRingEnd ℂ : (a : ℂ) → ℂ) ⟪(T : (a : V) → V) v, v⟫_ℂ = ⟪(T : (a : V) → V) v, v⟫_ℂ) → T.IsSymmetric
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
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
⊢ ⟪(T : (a : V) → V) x, y⟫_ℂ = ⟪x, (T : (a : V) → V) y⟫_ℂ
have mpr : ⟪(T : (a : V) → V) x, y⟫_ℂ = (starRingEnd ℂ : (a : ℂ) → ℂ) ⟪(T : (a : V) → V) y, x⟫_ℂ
Tactic: rw [← inner_conj_symm x (T y)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
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
⊢ ⟪(T : (a : V) → V) x, y⟫_ℂ = (starRingEnd ℂ : (a : ℂ) → ℂ) ⟪(T : (a : V) → V) y, x⟫_ℂ
have 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)
Tactic: rw [inner_map_polarization T x y]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
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
⊢ ⟪(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)
have 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
Tactic: simp only [starRingEnd_apply, star_div₀, star_sub, star_add, star_mul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
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
⊢ ⟪(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 : ℂ)
have 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 : ℂ)
Tactic: rw [h (x + y), h (x - y), h (x + Complex.I • y), h (x - Complex.I • y)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
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
⊢ ⟪(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 : ℂ)
have 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 : ℂ)
Tactic: simp only [Complex.conj_I]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
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
⊢ ⟪(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 : ℂ)
have 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 : ℂ)
Tactic: rw [inner_map_polarization']
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
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
⊢ (⟪(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 : ℂ)
have 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
Tactic: norm_num
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
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
⊢ ⟪(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
have 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
Tactic: rcases @I_mul_I_ax 𝕜 _ with (h | h)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
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
⊢ ⟪(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
have 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
Tactic: rcases @I_mul_I_ax 𝕜 _ with (h | h)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
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
⊢ ⟪(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
have 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
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)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
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⟫
⊢ (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
have 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
Tactic: rw [conj_eq_iff_re.mpr this]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
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
⊢ (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
have inl : (↑((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) y, x⟫) : 𝕜) = ⟪(T : (a : E) → E) y, x⟫
Tactic: suffices (re ⟪T y, x⟫ : 𝕜) = ⟪T y, x⟫ by
      rw [conj_eq_iff_re.mpr this]
      ring
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
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
⊢ (↑((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) y, x⟫) : 𝕜) = ⟪(T : (a : E) → E) y, x⟫
have 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
Tactic: rw [← re_add_im ⟪T y, x⟫]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
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
⊢ (↑((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
have inl : Eq.{u_1 + 1} (α := 𝕜) (↑((re : (a : 𝕜) → ℝ) (↑((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) y, x⟫) : 𝕜)) : 𝕜)
  (↑((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) y, x⟫) : 𝕜)
Tactic: simp_rw [h, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
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
⊢ Eq.{u_1 + 1} (α := 𝕜) (↑((re : (a : 𝕜) → ℝ) (↑((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) y, x⟫) : 𝕜)) : 𝕜)
    (↑((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) y, x⟫) : 𝕜)
have inl : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) y, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) y, x⟫ : ℝ)
Tactic: norm_cast