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 : 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
⊢ ⟪v, u⟫ = 0
have refine_1₁ : ⟪(↑(Subtype.mk (p := Membership.mem V) v hv) : E), (↑(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]
-- 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
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
⊢ ⟪v, u⟫ = 0
have 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
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]
-- 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
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
⊢ ⟪v, u⟫ = 0
have 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
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]
-- 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
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
⊢ ⟪v, u⟫ = 0
have 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
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]
-- 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
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
⊢ ⟪v, u⟫ = 0
have 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
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]
-- 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
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
⊢ ⟪v, u⟫ = 0
have 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
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]
-- 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
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
⊢ ⟪v, u⟫ = 0
have refine_1₇ : ⟪(U.subtype : (a : ↥U) → E) 0, (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ 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]
-- 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
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
⊢ ⟪v, u⟫ = 0
have refine_1₈ : ⟪0, (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ 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]
-- 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
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
⊢ ⟪v, u⟫ = 0
have refine_1₉ : Eq.{u_1 + 1} (α := 𝕜) 0 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]
-- 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 ⟂ 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⟫
have 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 sorry : (a : E) → E) x : E),
    (U.subtype ∘ₗ U.projectionOnto V hUV : (a : E) → E) y⟫
Tactic: nth_rw 2 [← projection_add_projection_eq_self hUV 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
U V : Submodule 𝕜 E
hUV : IsCompl U V
h : U ⟂ V
x y : E
⊢ ⟪(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⟫
have 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 sorry : (a : E) → E) y : E)⟫ =
  ⟪HAdd.hAdd (α := E) (β := E) ((U.projection V hUV : (a : E) → E) x : E) ((V.projection U sorry : (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]
-- 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 ⟂ V
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⟫
have 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 sorry : (a : E) → E) y : E)⟫ =
    ⟪HAdd.hAdd (α := E) (β := E) ((U.projection V hUV : (a : E) → E) x : E) ((V.projection U sorry : (a : E) → E) x : E),
      (U.subtype ∘ₗ U.projectionOnto V hUV : (a : E) → E) y⟫
Tactic: rw [isOrtho_iff_inner_eq] at h
Cleared hypotheses: 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
T : E →ₗ[𝕜] E
hT : IsIdempotentElem T
⊢ IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T ↔ T.range ⟂ T.ker
have rw : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T ↔ (T.range.projection T.ker sorry).IsSymmetric
Tactic: rw [← isSymmetric_projection_iff hT.isProj_range.isCompl, ← hT.eq_projection]
-- 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 : IsIdempotentElem T
rw : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T ↔ (T.range.projection T.ker ⋯).IsSymmetric
⊢ IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T ↔ T.range ⟂ T.ker
have rw₁ : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T ↔ IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
Tactic: rw [← isSymmetric_projection_iff hT.isProj_range.isCompl, ← hT.eq_projection]
-- 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
⊢ T.rangeᗮ = T.ker
have h : ∀ (x : E), x ∈ T.rangeᗮ ↔ x ∈ T.ker
Tactic: ext 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
⊢ x ∈ T.rangeᗮ ↔ x ∈ T.ker
have h : x ∈ T.rangeᗮ → x ∈ T.ker
Tactic: constructor
-- 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
h : x ∈ T.rangeᗮ → x ∈ T.ker
⊢ x ∈ T.rangeᗮ ↔ x ∈ T.ker
have h₁ : x ∈ T.ker → x ∈ T.rangeᗮ
Tactic: constructor
-- 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 : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) S
hT : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
⊢ S = T ↔ S.range = T.range
have refine : ∀ (h : S.range = T.range), S = T
Tactic: refine ⟨fun h => h ▸ rfl, fun h => ?_⟩
-- 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 : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) S
hT : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
h : S.range = T.range
⊢ S = T
have rw : S.range = T.range ∧ S.rangeᗮ = T.rangeᗮ
Tactic: rw [hS.isIdempotentElem.ext_iff hT.isIdempotentElem,
    ← hT.isIdempotentElem.isSymmetric_iff_orthogonal_range.mp hT.isSymmetric,
    ← hS.isIdempotentElem.isSymmetric_iff_orthogonal_range.mp hS.isSymmetric]
-- 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
p q : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
hq : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) q
hqp : p.range ≤ q.range
⊢ IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (q - p)
have hqp₁ : q ∘ₗ p = p
Tactic: rw [← hq.isIdempotentElem.comp_eq_right_iff] at hqp
Cleared hypotheses: hqp
-- 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
p q : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
hq : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) q
hqp : q ∘ₗ p = p
⊢ IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (q - p)
have refine : ∀ (x y : E), ⟪y, (p * q : (a : E) → E) x⟫ = ⟪y, (p : (a : E) → E) x⟫
Tactic: refine ⟨hp.isIdempotentElem.sub hq.isIdempotentElem (LinearMap.ext fun x => ext_inner_left 𝕜
    fun y => ?_) hqp, hq.isSymmetric.sub hp.isSymmetric⟩
-- 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
p q : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
hq : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) q
hqp : q ∘ₗ p = p
x y : E
⊢ ⟪y, (p * q : (a : E) → E) x⟫ = ⟪y, (p : (a : E) → E) x⟫
have simp_rw : ⟪y, (p : (a : E) → E) ((q : (a : E) → E) x : E)⟫ = ⟪y, (p : (a : E) → E) x⟫
Tactic: simp_rw [Module.End.mul_apply, ← hp.isSymmetric _, ← hq.isSymmetric _, ← comp_apply, hqp]
-- 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
p q : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
hq : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) q
hqp : q ∘ₗ p = p
x y : E
simp_rw : ⟪y, (p : (a : E) → E) ((q : (a : E) → E) x : E)⟫ = ⟪y, (p : (a : E) → E) x⟫
⊢ ⟪y, (p * q : (a : E) → E) x⟫ = ⟪y, (p : (a : E) → E) x⟫
have simp_rw₁ : inner 𝕜 (E := E) ((p : (a : E) → E) y : E) ((q : (a : E) → E) x : E) = ⟪(p : (a : E) → E) y, x⟫
Tactic: simp_rw [Module.End.mul_apply, ← hp.isSymmetric _, ← hq.isSymmetric _, ← comp_apply, hqp]
-- 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
p q : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
hq : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) q
hqp : q ∘ₗ p = p
x y : E
simp_rw : ⟪y, (p : (a : E) → E) ((q : (a : E) → E) x : E)⟫ = ⟪y, (p : (a : E) → E) x⟫
simp_rw₁ : inner 𝕜 (E := E) ((p : (a : E) → E) y : E) ((q : (a : E) → E) x : E) = ⟪(p : (a : E) → E) y, x⟫
⊢ ⟪y, (p * q : (a : E) → E) x⟫ = ⟪y, (p : (a : E) → E) x⟫
have simp_rw₂ : ⟪(q : (a : E) → E) ((p : (a : E) → E) y : E), x⟫ = ⟪(p : (a : E) → E) y, x⟫
Tactic: simp_rw [Module.End.mul_apply, ← hp.isSymmetric _, ← hq.isSymmetric _, ← comp_apply, hqp]
-- 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
p q : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
hq : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) q
hqp : q ∘ₗ p = p
x y : E
simp_rw : ⟪y, (p : (a : E) → E) ((q : (a : E) → E) x : E)⟫ = ⟪y, (p : (a : E) → E) x⟫
simp_rw₁ : inner 𝕜 (E := E) ((p : (a : E) → E) y : E) ((q : (a : E) → E) x : E) = ⟪(p : (a : E) → E) y, x⟫
simp_rw₂ : ⟪(q : (a : E) → E) ((p : (a : E) → E) y : E), x⟫ = ⟪(p : (a : E) → E) y, x⟫
⊢ ⟪y, (p * q : (a : E) → E) x⟫ = ⟪y, (p : (a : E) → E) x⟫
have simp_rw₃ : ⟪(q ∘ₗ p : (a : E) → E) y, x⟫ = ⟪(p : (a : E) → E) y, x⟫
Tactic: simp_rw [Module.End.mul_apply, ← hp.isSymmetric _, ← hq.isSymmetric _, ← comp_apply, hqp]
-- 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
f : E →ₗ[𝕜] E
hf : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) f
hf' : f ≠ 0
α : 𝕜
⊢ IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (α • f) ↔ IsSelfAdjoint α
have refine : ∀ (h : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (α • f)), IsSelfAdjoint α
Tactic: refine ⟨fun h ↦ ?_, hf.smul⟩
-- 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
f : E →ₗ[𝕜] E
hf : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) f
hf' : f ≠ 0
α : 𝕜
h : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (α • f)
⊢ IsSelfAdjoint α
have hf'₁ : ¬∀ (x v : E), ⟪v, (f : (a : E) → E) x⟫ = 0
Tactic: simp only [ne_eq, LinearMap.ext_iff, zero_apply, ext_iff_inner_left 𝕜 (E := E),
    inner_zero_right] at hf'
Cleared hypotheses: hf'