awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ Continuous (X := E) (Y := E) (⇑T : (a : E) → E)

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

Premises used: LinearMap.continuous_of_seq_closed_graph
-- 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
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)
rw : ⟪HSub.hSub (β := E) y ((T : (a : E) → E) x : E), HSub.hSub (β := E) y ((T : (a : E) → E) x : E)⟫ = 0
⊢ y = (T : (a : E) → E) x

Tactic:
rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜]

Premises used: sub_eq_zero, inner_self_eq_zero
-- 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
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))⟫
rw₁ 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))⟫
⊢ ⟪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:
rw [← T.map_sub, hT]

Premises used: LinearMap.map_sub
-- 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
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))⟫

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]
-- 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
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

Tactic:
tendsto_nhds_unique ((hTu.sub_const _).inner tendsto_const_nhds) ?_

Premises used: tendsto_const_nhds, Filter.Tendsto.sub_const, Filter.Tendsto.inner, tendsto_nhds_unique
-- 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
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))⟫
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)
⊢ ⟪HSub.hSub (β := E) y ((T : (a : E) → E) x : E), HSub.hSub (β := E) y ((T : (a : E) → E) x : E)⟫ = 0

Tactic:
refine tendsto_nhds_unique ((hTu.sub_const _).inner tendsto_const_nhds) ?_

Premises used: tendsto_const_nhds, Filter.Tendsto.sub_const, Filter.Tendsto.inner, tendsto_nhds_unique
-- 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
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))⟫
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)
⊢ 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:
simp_rw [Function.comp_apply, hlhs]

Premises used: Function.comp_apply
-- 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
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))⟫
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)))
⊢ 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:
rw [← inner_zero_left (T (y - T x))]

Premises used: HSub.hSub, inner_zero_left, DFunLike.coe
-- 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
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)))

Tactic:
Filter.Tendsto.inner ?_ tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.inner
-- 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
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))⟫
refine : Filter.Tendsto.{0, u_2} (β := E) (fun (t : ℕ) ↦ u t - x) Filter.atTop (nhds 0)
⊢ 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:
refine Filter.Tendsto.inner ?_ tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.inner
-- 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
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))⟫
rw : Filter.Tendsto (fun (t : ℕ) ↦ u t - x) Filter.atTop (nhds (x - x))
⊢ Filter.Tendsto.{0, u_2} (β := E) (fun (t : ℕ) ↦ u t - x) Filter.atTop (nhds 0)

Tactic:
rw [← sub_self x]

Premises used: sub_self
-- 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
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) Filter.atTop (nhds (x - x))

Tactic:
hu.sub_const _

Premises used: Filter.Tendsto.sub_const
-- 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
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) Filter.atTop (nhds (x - x))

Tactic:
exact hu.sub_const _

Premises used: Filter.Tendsto.sub_const
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
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
simp_rw : (∀ (x : E), ⟪(T : (a : E) → E) x, x⟫ = 0) ↔ ∀ (x : E), Eq (α := E) ((T : (a : E) → E) x : E) (0 : E)
⊢ (∀ (x : E), ⟪(T : (a : E) → E) x, x⟫ = 0) ↔ T = 0

Tactic:
simp_rw [LinearMap.ext_iff, zero_apply]

Premises used: LinearMap.zero_apply, LinearMap.ext_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
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
simp_rw₁ : ∀ (x : E), True
⊢ ∀ (x : E), ⟪(T : (a : E) → E) x, x⟫ = 0

Tactic:
simp_rw [h, inner_zero_left, forall_const]

Premises used: inner_zero_left, forall_const
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
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
refine : ∀ (h : ∀ (x : E), ⟪(T : (a : E) → E) x, x⟫ = 0) (x : E), Eq (α := E) ((T : (a : E) → E) x : E) (0 : E)
⊢ (∀ (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]⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
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
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
⊢ Eq (α := E) ((T : (a : E) → E) x : E) (0 : E)

Tactic:
rw [← @inner_self_eq_zero 𝕜, hT.inner_map_polarization]

Premises used: LinearMap.IsSymmetric.inner_map_polarization, inner_self_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
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
simp_rw : (HSub.hSub (α := 𝕜) 0 0 - HMul.hMul (α := 𝕜) I 0 + HMul.hMul (α := 𝕜) I 0) / 4 = 0
⊢ (⟪(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:
simp_rw [h _]
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
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
⊢ (HSub.hSub (α := 𝕜) 0 0 - HMul.hMul (α := 𝕜) I 0 + HMul.hMul (α := 𝕜) I 0) / 4 = 0

Tactic:
ring
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
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
⊢ Eq (α := E) ((T : (a : E) → E) v : E) (0 : E)

Tactic:
rw [mem_ker] at hv ⊢

Premises used: LinearMap.mem_ker
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
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), Eq (α := E) ((T : (a : E) → E) y : E) ((S : (a : E) → E) ((S : (a : E) → E) v : E) : E)

Tactic:
simpa using @h (S (S v))
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
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)
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)
⊢ 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))

Premises used: DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
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
rw₅ rw₆ : Eq.{u_1 + 1} (α := 𝕜) 0 0
⊢ Eq (α := E) ((S : (a : E) → E) v : E) (0 : E)

Tactic:
rw [← inner_self_eq_zero (𝕜 := 𝕜), ← hS, ← hy, hT, hv, inner_zero_right]

Premises used: inner_zero_right, inner_self_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
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

Tactic:
⟨fun h u hu v hv => ?_, 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 : 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
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⟫
⊢ (U.subtype ∘ₗ U.projectionOnto V hUV).IsSymmetric ↔ U ⟂ V

Tactic:
refine ⟨fun h u hu v hv => ?_, fun h x y => ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
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
refine_1 : ⟪v, (↑(Subtype.mk (p := Membership.mem U) u hu) : E)⟫ = 0
refine_1₁ : ⟪(↑(Subtype.mk (p := Membership.mem V) v hv) : E), (↑(Subtype.mk (p := Membership.mem U) u hu) : E)⟫ = 0
refine_1₂ :
  ⟪(↑(Subtype.mk (p := Membership.mem V) v hv) : E),
      (↑((U.projectionOnto V hUV : (a : E) → ↥U) (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ U) u hu) : E)) : E)⟫ =
    0
refine_1₃ :
  ⟪(↑(Subtype.mk (p := Membership.mem V) v hv) : E),
      (U.subtype : (a : ↥U) → E)
        ((U.projectionOnto V hUV : (a : E) → ↥U) (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ U) u hu) : E) : ↥U)⟫ =
    0
refine_1₄ :
  ⟪(↑(Subtype.mk (p := Membership.mem V) v hv) : E),
      (U.subtype ∘ₗ U.projectionOnto V hUV : (a : E) → E) (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ U) u hu) : E)⟫ =
    0
refine_1₅ :
  ⟪(U.subtype ∘ₗ U.projectionOnto V hUV : (a : E) → E) (↑(Subtype.mk (p := Membership.mem V) v hv) : E),
      (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ U) u hu) : E)⟫ =
    0
refine_1₆ :
  ⟪(U.subtype : (a : ↥U) → E)
        ((U.projectionOnto V hUV : (a : E) → ↥U) (↑(Subtype.mk (p := Membership.mem V) v hv) : E) : ↥U),
      (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ U) u hu) : E)⟫ =
    0
refine_1₇ : ⟪(U.subtype : (a : ↥U) → E) 0, (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ U) u hu) : E)⟫ = 0
refine_1₈ : ⟪0, (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ U) u hu) : E)⟫ = 0
refine_1₉ refine_1₁₀ : Eq.{u_1 + 1} (α := 𝕜) 0 0
⊢ ⟪v, u⟫ = 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]

Premises used: Subtype.coe_mk, Submodule.subtype_apply, LinearMap.comp_apply, map_zero, inner_zero_left, Subtype.mk, Submodule.projectionOnto_apply_left, Submodule.projectionOnto_apply_right
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
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 ⟂ V
x y : E
refine_2 :
  ⟪(U.subtype ∘ₗ U.projectionOnto V hUV : (a : E) → E) x, y⟫ =
    ⟪HAdd.hAdd (α := E) (β := E) ((U.projection V hUV : (a : E) → E) x : E) ((V.projection U ⋯ : (a : E) → E) x : E),
      (U.subtype ∘ₗ U.projectionOnto V hUV : (a : E) → E) y⟫
⊢ ⟪(U.subtype ∘ₗ U.projectionOnto V hUV : (a : E) → E) x, y⟫ =
    ⟪x, (U.subtype ∘ₗ U.projectionOnto V hUV : (a : E) → E) y⟫

Tactic:
nth_rw 2 [← projection_add_projection_eq_self hUV x]

Premises used: Submodule.projection_add_projection_eq_self
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
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 ⟂ V
x y : E
refine_2 :
  ⟪(U.subtype ∘ₗ U.projectionOnto V hUV : (a : E) → E) x,
      HAdd.hAdd (α := E) (β := E) ((U.projection V hUV : (a : E) → E) y : E) ((V.projection U ⋯ : (a : E) → E) y : E)⟫ =
    ⟪HAdd.hAdd (α := E) (β := E) ((U.projection V hUV : (a : E) → E) x : E) ((V.projection U ⋯ : (a : E) → E) x : E),
      (U.subtype ∘ₗ U.projectionOnto V hUV : (a : E) → E) y⟫
⊢ ⟪(U.subtype ∘ₗ U.projectionOnto V hUV : (a : E) → E) x, y⟫ =
    ⟪HAdd.hAdd (α := E) (β := E) ((U.projection V hUV : (a : E) → E) x : E) ((V.projection U ⋯ : (a : E) → E) x : E),
      (U.subtype ∘ₗ U.projectionOnto V hUV : (a : E) → E) y⟫

Tactic:
nth_rw 1 [← projection_add_projection_eq_self hUV y]

Premises used: Submodule.projection_add_projection_eq_self
-- Module: Mathlib.Analysis.InnerProductSpace.Symmetric
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 ⟂ V
x y : E
refine_2 :
  ∀ (h : ∀ u ∈ U, ∀ v ∈ V, ⟪u, v⟫ = 0) (x y : E),
    ⟪(U.subtype ∘ₗ U.projectionOnto V hUV : (a : E) → E) x,
        HAdd.hAdd (α := E) (β := E) ((U.projection V hUV : (a : E) → E) y : E)
          ((V.projection U ⋯ : (a : E) → E) y : E)⟫ =
      ⟪HAdd.hAdd (α := E) (β := E) ((U.projection V hUV : (a : E) → E) x : E) ((V.projection U ⋯ : (a : E) → E) x : E),
        (U.subtype ∘ₗ U.projectionOnto V hUV : (a : E) → E) y⟫
⊢ ⟪(U.subtype ∘ₗ U.projectionOnto V hUV : (a : E) → E) x,
      HAdd.hAdd (α := E) (β := E) ((U.projection V hUV : (a : E) → E) y : E) ((V.projection U ⋯ : (a : E) → E) y : E)⟫ =
    ⟪HAdd.hAdd (α := E) (β := E) ((U.projection V hUV : (a : E) → E) x : E) ((V.projection U ⋯ : (a : E) → E) x : E),
      (U.subtype ∘ₗ U.projectionOnto V hUV : (a : E) → E) y⟫

Tactic:
rw [isOrtho_iff_inner_eq] at h

Premises used: Submodule.isOrtho_iff_inner_eq