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 : 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 + 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 : ⟪(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: 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]
-- 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
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
have 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⟫
Tactic: refine ⟨fun h x y => ?_, fun h x 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
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⟫
⊢ ((↑f.toLinearEquiv : E →ₗ[𝕜] F) ∘ₗ T ∘ₗ (↑f.symm.toLinearEquiv : F →ₗ[𝕜] E)).IsSymmetric ↔ T.IsSymmetric
have 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⟫
Tactic: refine ⟨fun h x y => ?_, fun h x y => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (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 →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
⊢ Continuous (X := E) (Y := E) (⇑T : (a : E) → E)
have refine : ∀ (u : ℕ → E) (x y : E) (hu : Filter.Tendsto u Filter.atTop (nhds x))
  (hTu : Filter.Tendsto ((⇑T : (a : E) → E) ∘ u) Filter.atTop (nhds y)), y = (T : (a : E) → E) x
Tactic: refine T.continuous_of_seq_closed_graph fun u x y hu hTu => ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (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 →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto ((⇑T : (a : E) → E) ∘ u) Filter.atTop (nhds y)
⊢ y = (T : (a : E) → E) x
have rw : ⟪HSub.hSub (β := E) y ((T : (a : E) → E) x : E), HSub.hSub (β := E) y ((T : (a : E) → E) x : E)⟫ = 0
Tactic: rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (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 →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto ((⇑T : (a : E) → E) ∘ u) Filter.atTop (nhds y)
k : ℕ
⊢ ⟪HSub.hSub (α := E) (β := E) ((T : (a : E) → E) (u k) : E) ((T : (a : E) → E) x : E),
      HSub.hSub (β := E) y ((T : (a : E) → E) x : E)⟫ =
    ⟪u k - x, (T : (a : E) → E) (HSub.hSub (β := E) y ((T : (a : E) → E) x : E))⟫
have rw : ⟪(T : (a : E) → E) (u k - x), HSub.hSub (β := E) y ((T : (a : E) → E) x : E)⟫ =
  ⟪u k - x, (T : (a : E) → E) (HSub.hSub (β := E) y ((T : (a : E) → E) x : E))⟫
Tactic: rw [← T.map_sub, hT]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (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 →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto ((⇑T : (a : E) → E) ∘ u) Filter.atTop (nhds y)
k : ℕ
rw :
  ⟪(T : (a : E) → E) (u k - x), HSub.hSub (β := E) y ((T : (a : E) → E) x : E)⟫ =
    ⟪u k - x, (T : (a : E) → E) (HSub.hSub (β := E) y ((T : (a : E) → E) x : E))⟫
⊢ ⟪HSub.hSub (α := E) (β := E) ((T : (a : E) → E) (u k) : E) ((T : (a : E) → E) x : E),
      HSub.hSub (β := E) y ((T : (a : E) → E) x : E)⟫ =
    ⟪u k - x, (T : (a : E) → E) (HSub.hSub (β := E) y ((T : (a : E) → E) x : E))⟫
have rw₁ : ⟪u k - x, (T : (a : E) → E) (HSub.hSub (β := E) y ((T : (a : E) → E) x : E))⟫ =
  ⟪u k - x, (T : (a : E) → E) (HSub.hSub (β := E) y ((T : (a : E) → E) x : E))⟫
Tactic: rw [← T.map_sub, hT]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (hypothesis)
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
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto ((⇑T : (a : E) → E) ∘ u) Filter.atTop (nhds y)
⊢ ⟪HSub.hSub (β := E) y ((T : (a : E) → E) x : E), HSub.hSub (β := E) y ((T : (a : E) → E) x : E)⟫ = 0
have hlhs : ∀ (k : ℕ),
  ⟪HSub.hSub (α := E) (β := E) ((T : (a : E) → E) (u k) : E) ((T : (a : E) → E) x : E),
      HSub.hSub (β := E) y ((T : (a : E) → E) x : E)⟫ =
    ⟪u k - x, (T : (a : E) → E) (HSub.hSub (β := E) y ((T : (a : E) → E) x : E))⟫
Tactic: have hlhs : ∀ k : ℕ, ⟪T (u k) - T x, y - T x⟫ = ⟪u k - x, T (y - T x)⟫ := by
    intro k
    rw [← T.map_sub, hT]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (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 →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto ((⇑T : (a : E) → E) ∘ u) Filter.atTop (nhds y)
hlhs :
  ∀ (k : ℕ),
    ⟪HSub.hSub (α := E) (β := E) ((T : (a : E) → E) (u k) : E) ((T : (a : E) → E) x : E),
        HSub.hSub (β := E) y ((T : (a : E) → E) x : E)⟫ =
      ⟪u k - x, (T : (a : E) → E) (HSub.hSub (β := E) y ((T : (a : E) → E) x : E))⟫
⊢ ⟪HSub.hSub (β := E) y ((T : (a : E) → E) x : E), HSub.hSub (β := E) y ((T : (a : E) → E) x : E)⟫ = 0
have refine : Filter.Tendsto.{0, u_1} (β := 𝕜)
  (fun (t : ℕ) ↦
    ⟪HSub.hSub (α := E) (β := E) (((⇑T : (a : E) → E) ∘ u) t : E) ((T : (a : E) → E) x : E),
      HSub.hSub (β := E) y ((T : (a : E) → E) x : E)⟫)
  Filter.atTop (nhds 0)
Tactic: refine tendsto_nhds_unique ((hTu.sub_const _).inner tendsto_const_nhds) ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (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 →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto ((⇑T : (a : E) → E) ∘ u) Filter.atTop (nhds y)
hlhs :
  ∀ (k : ℕ),
    ⟪HSub.hSub (α := E) (β := E) ((T : (a : E) → E) (u k) : E) ((T : (a : E) → E) x : E),
        HSub.hSub (β := E) y ((T : (a : E) → E) x : E)⟫ =
      ⟪u k - x, (T : (a : E) → E) (HSub.hSub (β := E) y ((T : (a : E) → E) x : E))⟫
⊢ Filter.Tendsto.{0, u_1} (β := 𝕜)
    (fun (t : ℕ) ↦
      ⟪HSub.hSub (α := E) (β := E) (((⇑T : (a : E) → E) ∘ u) t : E) ((T : (a : E) → E) x : E),
        HSub.hSub (β := E) y ((T : (a : E) → E) x : E)⟫)
    Filter.atTop (nhds 0)
have simp_rw : Filter.Tendsto.{0, u_1} (β := 𝕜)
  (fun (t : ℕ) ↦ ⟪u t - x, (T : (a : E) → E) (HSub.hSub (β := E) y ((T : (a : E) → E) x : E))⟫) Filter.atTop (nhds 0)
Tactic: simp_rw [Function.comp_apply, hlhs]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (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 →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto ((⇑T : (a : E) → E) ∘ u) Filter.atTop (nhds y)
hlhs :
  ∀ (k : ℕ),
    ⟪HSub.hSub (α := E) (β := E) ((T : (a : E) → E) (u k) : E) ((T : (a : E) → E) x : E),
        HSub.hSub (β := E) y ((T : (a : E) → E) x : E)⟫ =
      ⟪u k - x, (T : (a : E) → E) (HSub.hSub (β := E) y ((T : (a : E) → E) x : E))⟫
⊢ Filter.Tendsto.{0, u_1} (β := 𝕜)
    (fun (t : ℕ) ↦ ⟪u t - x, (T : (a : E) → E) (HSub.hSub (β := E) y ((T : (a : E) → E) x : E))⟫) Filter.atTop (nhds 0)
have rw : Filter.Tendsto (fun (t : ℕ) ↦ ⟪u t - x, (T : (a : E) → E) (HSub.hSub (β := E) y ((T : (a : E) → E) x : E))⟫)
  Filter.atTop
  (nhds (inner 𝕜 (E := E) (0 : E) ((T : (a : E) → E) (HSub.hSub (β := E) y ((T : (a : E) → E) x : E)) : E)))
Tactic: rw [← inner_zero_left (T (y - T x))]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (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 →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto ((⇑T : (a : E) → E) ∘ u) Filter.atTop (nhds y)
hlhs :
  ∀ (k : ℕ),
    ⟪HSub.hSub (α := E) (β := E) ((T : (a : E) → E) (u k) : E) ((T : (a : E) → E) x : E),
        HSub.hSub (β := E) y ((T : (a : E) → E) x : E)⟫ =
      ⟪u k - x, (T : (a : E) → E) (HSub.hSub (β := E) y ((T : (a : E) → E) x : E))⟫
⊢ Filter.Tendsto (fun (t : ℕ) ↦ ⟪u t - x, (T : (a : E) → E) (HSub.hSub (β := E) y ((T : (a : E) → E) x : E))⟫)
    Filter.atTop
    (nhds (inner 𝕜 (E := E) (0 : E) ((T : (a : E) → E) (HSub.hSub (β := E) y ((T : (a : E) → E) x : E)) : E)))
have refine : Filter.Tendsto.{0, u_2} (β := E) (fun (t : ℕ) ↦ u t - x) Filter.atTop (nhds 0)
Tactic: refine Filter.Tendsto.inner ?_ tendsto_const_nhds
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (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 →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto ((⇑T : (a : E) → E) ∘ u) Filter.atTop (nhds y)
hlhs :
  ∀ (k : ℕ),
    ⟪HSub.hSub (α := E) (β := E) ((T : (a : E) → E) (u k) : E) ((T : (a : E) → E) x : E),
        HSub.hSub (β := E) y ((T : (a : E) → E) x : E)⟫ =
      ⟪u k - x, (T : (a : E) → E) (HSub.hSub (β := E) y ((T : (a : E) → E) x : E))⟫
⊢ Filter.Tendsto.{0, u_2} (β := E) (fun (t : ℕ) ↦ u t - x) Filter.atTop (nhds 0)
have rw : Filter.Tendsto (fun (t : ℕ) ↦ u t - x) Filter.atTop (nhds (x - x))
Tactic: rw [← sub_self x]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
⊢ (∀ (x : E), ⟪(T : (a : E) → E) x, x⟫ = 0) ↔ T = 0
have simp_rw : (∀ (x : E), ⟪(T : (a : E) → E) x, x⟫ = 0) ↔ ∀ (x : E), Eq (α := E) ((T : (a : E) → E) x : E) (0 : E)
Tactic: simp_rw [LinearMap.ext_iff, zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
h : ∀ (x : E), Eq (α := E) ((T : (a : E) → E) x : E) (0 : E)
⊢ ∀ (x : E), ⟪(T : (a : E) → E) x, x⟫ = 0
have simp_rw : ∀ (x : E), ⟪0, x⟫ = 0
Tactic: simp_rw [h, inner_zero_left, forall_const]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
h : ∀ (x : E), Eq (α := E) ((T : (a : E) → E) x : E) (0 : E)
simp_rw : ∀ (x : E), ⟪0, x⟫ = 0
⊢ ∀ (x : E), ⟪(T : (a : E) → E) x, x⟫ = 0
have simp_rw₁ : ∀ (x : E), True
Tactic: simp_rw [h, inner_zero_left, forall_const]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
⊢ (∀ (x : E), ⟪(T : (a : E) → E) x, x⟫ = 0) ↔ ∀ (x : E), Eq (α := E) ((T : (a : E) → E) x : E) (0 : E)
have refine : ∀ (h : ∀ (x : E), ⟪(T : (a : E) → E) x, x⟫ = 0) (x : E), Eq (α := E) ((T : (a : E) → E) x : E) (0 : E)
Tactic: refine ⟨fun h x => ?_, fun h => by simp_rw [h, inner_zero_left, forall_const]⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
h : ∀ (x : E), ⟪(T : (a : E) → E) x, x⟫ = 0
x : E
⊢ Eq (α := E) ((T : (a : E) → E) x : E) (0 : E)
have rw : (⟪(T : (a : E) → E) (HAdd.hAdd (β := E) x ((T : (a : E) → E) x : E)), HAdd.hAdd (β := E) x ((T : (a : E) → E) x : E)⟫ -
          ⟪(T : (a : E) → E) (HSub.hSub (β := E) x ((T : (a : E) → E) x : E)),
            HSub.hSub (β := E) x ((T : (a : E) → E) x : E)⟫ -
        I *
          ⟪(T : (a : E) → E) (x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) I ((T : (a : E) → E) x : E)),
            x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) I ((T : (a : E) → E) x : E)⟫ +
      I *
        ⟪(T : (a : E) → E) (x - HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) I ((T : (a : E) → E) x : E)),
          x - HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) I ((T : (a : E) → E) x : E)⟫) /
    4 =
  0
Tactic: rw [← @inner_self_eq_zero 𝕜, hT.inner_map_polarization]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
h : ∀ (x : E), ⟪(T : (a : E) → E) x, x⟫ = 0
x : E
⊢ (⟪(T : (a : E) → E) (HAdd.hAdd (β := E) x ((T : (a : E) → E) x : E)),
              HAdd.hAdd (β := E) x ((T : (a : E) → E) x : E)⟫ -
            ⟪(T : (a : E) → E) (HSub.hSub (β := E) x ((T : (a : E) → E) x : E)),
              HSub.hSub (β := E) x ((T : (a : E) → E) x : E)⟫ -
          I *
            ⟪(T : (a : E) → E) (x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) I ((T : (a : E) → E) x : E)),
              x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) I ((T : (a : E) → E) x : E)⟫ +
        I *
          ⟪(T : (a : E) → E) (x - HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) I ((T : (a : E) → E) x : E)),
            x - HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) I ((T : (a : E) → E) x : E)⟫) /
      4 =
    0
have simp_rw : (HSub.hSub (α := 𝕜) 0 0 - HMul.hMul (α := 𝕜) I 0 + HMul.hMul (α := 𝕜) I 0) / 4 = 0
Tactic: simp_rw [h _]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
S T : E →ₗ[𝕜] E
hS : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) S
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
h : S.range ≤ T.range
v : E
hv : v ∈ T.ker
⊢ v ∈ S.ker
have hv₁ : Eq (α := E) ((T : (a : E) → E) v : E) (0 : E)
Tactic: rw [mem_ker] at hv ⊢
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
S T : E →ₗ[𝕜] E
hS : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) S
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
h : S.range ≤ T.range
v : E
hv : Eq (α := E) ((T : (a : E) → E) v : E) (0 : E)
⊢ Eq (α := E) ((S : (a : E) → E) v : E) (0 : E)
have obtain : ∀ (y : E) (hy : Eq (α := E) ((T : (a : E) → E) y : E) ((S : (a : E) → E) ((S : (a : E) → E) v : E) : E)),
  Eq (α := E) ((S : (a : E) → E) v : E) (0 : E)
Tactic: obtain ⟨y, hy⟩ : ∃ y, T y = S (S v) := by simpa using @h (S (S v))
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
S T : E →ₗ[𝕜] E
hS : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) S
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
h : S.range ≤ T.range
v : E
hv : Eq (α := E) ((T : (a : E) → E) v : E) (0 : E)
y : E
hy : Eq (α := E) ((T : (a : E) → E) y : E) ((S : (a : E) → E) ((S : (a : E) → E) v : E) : E)
⊢ Eq (α := E) ((S : (a : E) → E) v : E) (0 : E)
have rw : inner 𝕜 (E := E) ((S : (a : E) → E) v : E) ((S : (a : E) → E) v : E) = 0
Tactic: rw [← inner_self_eq_zero (𝕜 := 𝕜), ← hS, ← hy, hT, hv, inner_zero_right]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
S T : E →ₗ[𝕜] E
hS : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) S
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
h : S.range ≤ T.range
v : E
hv : Eq (α := E) ((T : (a : E) → E) v : E) (0 : E)
y : E
hy : Eq (α := E) ((T : (a : E) → E) y : E) ((S : (a : E) → E) ((S : (a : E) → E) v : E) : E)
rw : inner 𝕜 (E := E) ((S : (a : E) → E) v : E) ((S : (a : E) → E) v : E) = 0
⊢ Eq (α := E) ((S : (a : E) → E) v : E) (0 : E)
have rw₁ : ⟪(S : (a : E) → E) ((S : (a : E) → E) v : E), v⟫ = 0
Tactic: rw [← inner_self_eq_zero (𝕜 := 𝕜), ← hS, ← hy, hT, hv, inner_zero_right]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
S T : E →ₗ[𝕜] E
hS : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) S
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
h : S.range ≤ T.range
v : E
hv : Eq (α := E) ((T : (a : E) → E) v : E) (0 : E)
y : E
hy : Eq (α := E) ((T : (a : E) → E) y : E) ((S : (a : E) → E) ((S : (a : E) → E) v : E) : E)
rw : inner 𝕜 (E := E) ((S : (a : E) → E) v : E) ((S : (a : E) → E) v : E) = 0
rw₁ : ⟪(S : (a : E) → E) ((S : (a : E) → E) v : E), v⟫ = 0
⊢ Eq (α := E) ((S : (a : E) → E) v : E) (0 : E)
have rw₂ : ⟪(T : (a : E) → E) y, v⟫ = 0
Tactic: rw [← inner_self_eq_zero (𝕜 := 𝕜), ← hS, ← hy, hT, hv, inner_zero_right]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
S T : E →ₗ[𝕜] E
hS : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) S
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
h : S.range ≤ T.range
v : E
hv : Eq (α := E) ((T : (a : E) → E) v : E) (0 : E)
y : E
hy : Eq (α := E) ((T : (a : E) → E) y : E) ((S : (a : E) → E) ((S : (a : E) → E) v : E) : E)
rw : inner 𝕜 (E := E) ((S : (a : E) → E) v : E) ((S : (a : E) → E) v : E) = 0
rw₁ : ⟪(S : (a : E) → E) ((S : (a : E) → E) v : E), v⟫ = 0
rw₂ : ⟪(T : (a : E) → E) y, v⟫ = 0
⊢ Eq (α := E) ((S : (a : E) → E) v : E) (0 : E)
have rw₃ : ⟪y, (T : (a : E) → E) v⟫ = 0
Tactic: rw [← inner_self_eq_zero (𝕜 := 𝕜), ← hS, ← hy, hT, hv, inner_zero_right]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
S T : E →ₗ[𝕜] E
hS : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) S
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
h : S.range ≤ T.range
v : E
hv : Eq (α := E) ((T : (a : E) → E) v : E) (0 : E)
y : E
hy : Eq (α := E) ((T : (a : E) → E) y : E) ((S : (a : E) → E) ((S : (a : E) → E) v : E) : E)
rw : inner 𝕜 (E := E) ((S : (a : E) → E) v : E) ((S : (a : E) → E) v : E) = 0
rw₁ : ⟪(S : (a : E) → E) ((S : (a : E) → E) v : E), v⟫ = 0
rw₂ : ⟪(T : (a : E) → E) y, v⟫ = 0
rw₃ : ⟪y, (T : (a : E) → E) v⟫ = 0
⊢ Eq (α := E) ((S : (a : E) → E) v : E) (0 : E)
have rw₄ : ⟪y, 0⟫ = 0
Tactic: rw [← inner_self_eq_zero (𝕜 := 𝕜), ← hS, ← hy, hT, hv, inner_zero_right]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
S T : E →ₗ[𝕜] E
hS : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) S
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
h : S.range ≤ T.range
v : E
hv : Eq (α := E) ((T : (a : E) → E) v : E) (0 : E)
y : E
hy : Eq (α := E) ((T : (a : E) → E) y : E) ((S : (a : E) → E) ((S : (a : E) → E) v : E) : E)
rw : inner 𝕜 (E := E) ((S : (a : E) → E) v : E) ((S : (a : E) → E) v : E) = 0
rw₁ : ⟪(S : (a : E) → E) ((S : (a : E) → E) v : E), v⟫ = 0
rw₂ : ⟪(T : (a : E) → E) y, v⟫ = 0
rw₃ : ⟪y, (T : (a : E) → E) v⟫ = 0
rw₄ : ⟪y, 0⟫ = 0
⊢ Eq (α := E) ((S : (a : E) → E) v : E) (0 : E)
have rw₅ : Eq.{u_1 + 1} (α := 𝕜) 0 0
Tactic: rw [← inner_self_eq_zero (𝕜 := 𝕜), ← hS, ← hy, hT, hv, inner_zero_right]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
hUV : IsCompl U V
⊢ (U.subtype ∘ₗ U.projectionOnto V hUV).IsSymmetric ↔ U ⟂ V
have refine_1 : ∀ (h : (U.subtype ∘ₗ U.projectionOnto V hUV).IsSymmetric) (u : E) (hu : u ∈ U) (v : E) (hv : v ∈ V), ⟪v, u⟫ = 0
Tactic: refine ⟨fun h u hu v hv => ?_, fun h x y => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
hUV : IsCompl U V
refine_1 :
  ∀ (h : (U.subtype ∘ₗ U.projectionOnto V hUV).IsSymmetric) (u : E) (hu : u ∈ U) (v : E) (hv : v ∈ V), ⟪v, u⟫ = 0
⊢ (U.subtype ∘ₗ U.projectionOnto V hUV).IsSymmetric ↔ U ⟂ V
have refine_2 : ∀ (h : U ⟂ V) (x y : E),
  ⟪(U.subtype ∘ₗ U.projectionOnto V hUV : (a : E) → E) x, y⟫ =
    ⟪x, (U.subtype ∘ₗ U.projectionOnto V hUV : (a : E) → E) y⟫
Tactic: refine ⟨fun h u hu v hv => ?_, fun h x y => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Symmetric (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
hUV : IsCompl U V
h : (U.subtype ∘ₗ U.projectionOnto V hUV).IsSymmetric
u : E
hu : u ∈ U
v : E
hv : v ∈ V
⊢ ⟪v, u⟫ = 0
have refine_1 : ⟪v, (↑(Subtype.mk (p := Membership.mem U) u hu) : E)⟫ = 0
Tactic: rw [← Subtype.coe_mk u hu, ← Subtype.coe_mk v hv,
      ← Submodule.projectionOnto_apply_left hUV ⟨u, hu⟩, ← U.subtype_apply, ← comp_apply,
      ← h, comp_apply, Submodule.projectionOnto_apply_right hUV ⟨v, hv⟩,
      map_zero, inner_zero_left]