awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
v : Π₀ (i : ι), ↥(V i)
hv :
  Eq.{u_2 + 1} (α := E)
    (((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
            fun (i : ι) ↦ (V i).subtype :
          (a : Π₀ (i : ι), ↥(V i)) → E)
        v :
      E)
    (0 : E)
i : ι
⊢ ⟪(↑((v : (a : ι) → ↥(V a)) i) : E), (↑((v : (a : ι) → ↥(V a)) i) : E)⟫ = 0
have i₁ : ⟪(↑((v : (a : ι) → ↥(V a)) i) : E), (↑((v : (a : ι) → ↥(V a)) i) : E)⟫ =
  ⟪(↑((v : (a : ι) → ↥(V a)) i) : E),
    ((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
          fun (i : ι) ↦ (V i).subtype :
        (a : Π₀ (i : ι), ↥(V i)) → E)
      v⟫
Tactic: calc
    ⟪(v i : E), v i⟫ = ⟪(v i : E), DFinsupp.lsum ℕ (fun i => (V i).subtype) v⟫ := by
      simpa only [DFinsupp.sumAddHom_apply, DFinsupp.lsum_apply_apply] using
        (hV.inner_right_dfinsupp v i (v i)).symm
    _ = 0 := by simp only [hv, inner_zero_right]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
v : Π₀ (i : ι), ↥(V i)
hv :
  Eq.{u_2 + 1} (α := E)
    (((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
            fun (i : ι) ↦ (V i).subtype :
          (a : Π₀ (i : ι), ↥(V i)) → E)
        v :
      E)
    (0 : E)
i : ι
i₁ :
  ⟪(↑((v : (a : ι) → ↥(V a)) i) : E), (↑((v : (a : ι) → ↥(V a)) i) : E)⟫ =
    ⟪(↑((v : (a : ι) → ↥(V a)) i) : E),
      ((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
            fun (i : ι) ↦ (V i).subtype :
          (a : Π₀ (i : ι), ↥(V i)) → E)
        v⟫
⊢ ⟪(↑((v : (a : ι) → ↥(V a)) i) : E), (↑((v : (a : ι) → ↥(V a)) i) : E)⟫ = 0
have i₂ : ⟪(↑((v : (a : ι) → ↥(V a)) i) : E),
    ((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
          fun (i : ι) ↦ (V i).subtype :
        (a : Π₀ (i : ι), ↥(V i)) → E)
      v⟫ =
  0
Tactic: calc
    ⟪(v i : E), v i⟫ = ⟪(v i : E), DFinsupp.lsum ℕ (fun i => (V i).subtype) v⟫ := by
      simpa only [DFinsupp.sumAddHom_apply, DFinsupp.lsum_apply_apply] using
        (hV.inner_right_dfinsupp v i (v i)).symm
    _ = 0 := by simp only [hv, inner_zero_right]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
⊢ iSupIndep V
have h : Function.Injective (α := Π₀ (i : ι), ↥(V i)) (β := E)
  (⇑((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
        fun (i : ι) ↦ (V i).subtype) :
    (a : Π₀ (i : ι), ↥(V i)) → E)
Tactic: classical
  apply iSupIndep_of_dfinsupp_lsum_injective
  refine LinearMap.ker_eq_bot.mp ?_
  rw [Submodule.eq_bot_iff]
  intro v hv
  rw [LinearMap.mem_ker] at hv
  ext i
  suffices ⟪(v i : E), v i⟫ = 0 by simpa only [inner_self_eq_zero] using this
  calc
    ⟪(v i : E), v i⟫ = ⟪(v i : E), DFinsupp.lsum ℕ (fun i => (V i).subtype) v⟫ := by
      simpa only [DFinsupp.sumAddHom_apply, DFinsupp.lsum_apply_apply] using
        (hV.inner_right_dfinsupp v i (v i)).symm
    _ = 0 := by simp only [hv, inner_zero_right]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
h :
  Function.Injective (α := Π₀ (i : ι), ↥(V i)) (β := E)
    (⇑((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
          fun (i : ι) ↦ (V i).subtype) :
      (a : Π₀ (i : ι), ↥(V i)) → E)
⊢ iSupIndep V
have h₁ : Eq (α := Submodule 𝕜 (Π₀ (i : ι), ↥(V i)))
  (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
    ((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
      fun (i : ι) ↦ (V i).subtype))
  ⊥
Tactic: classical
  apply iSupIndep_of_dfinsupp_lsum_injective
  refine LinearMap.ker_eq_bot.mp ?_
  rw [Submodule.eq_bot_iff]
  intro v hv
  rw [LinearMap.mem_ker] at hv
  ext i
  suffices ⟪(v i : E), v i⟫ = 0 by simpa only [inner_self_eq_zero] using this
  calc
    ⟪(v i : E), v i⟫ = ⟪(v i : E), DFinsupp.lsum ℕ (fun i => (V i).subtype) v⟫ := by
      simpa only [DFinsupp.sumAddHom_apply, DFinsupp.lsum_apply_apply] using
        (hV.inner_right_dfinsupp v i (v i)).symm
    _ = 0 := by simp only [hv, inner_zero_right]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
h :
  Function.Injective (α := Π₀ (i : ι), ↥(V i)) (β := E)
    (⇑((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
          fun (i : ι) ↦ (V i).subtype) :
      (a : Π₀ (i : ι), ↥(V i)) → E)
h₁ :
  Eq (α := Submodule 𝕜 (Π₀ (i : ι), ↥(V i)))
    (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
      ((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
        fun (i : ι) ↦ (V i).subtype))
    ⊥
⊢ iSupIndep V
have h₂ : ∀ (x : Π₀ (i : ι), ↥(V i)),
  Membership.mem (γ := Submodule 𝕜 (Π₀ (i : ι), ↥(V i)))
      (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
        ((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
          fun (i : ι) ↦ (V i).subtype))
      x →
    x = 0
Tactic: classical
  apply iSupIndep_of_dfinsupp_lsum_injective
  refine LinearMap.ker_eq_bot.mp ?_
  rw [Submodule.eq_bot_iff]
  intro v hv
  rw [LinearMap.mem_ker] at hv
  ext i
  suffices ⟪(v i : E), v i⟫ = 0 by simpa only [inner_self_eq_zero] using this
  calc
    ⟪(v i : E), v i⟫ = ⟪(v i : E), DFinsupp.lsum ℕ (fun i => (V i).subtype) v⟫ := by
      simpa only [DFinsupp.sumAddHom_apply, DFinsupp.lsum_apply_apply] using
        (hV.inner_right_dfinsupp v i (v i)).symm
    _ = 0 := by simp only [hv, inner_zero_right]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
h :
  Function.Injective (α := Π₀ (i : ι), ↥(V i)) (β := E)
    (⇑((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
          fun (i : ι) ↦ (V i).subtype) :
      (a : Π₀ (i : ι), ↥(V i)) → E)
h₁ :
  Eq (α := Submodule 𝕜 (Π₀ (i : ι), ↥(V i)))
    (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
      ((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
        fun (i : ι) ↦ (V i).subtype))
    ⊥
h₂ h₃ :
  ∀ (v : Π₀ (i : ι), ↥(V i))
    (hv :
      Membership.mem (γ := Submodule 𝕜 (Π₀ (i : ι), ↥(V i)))
        (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
          ((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
            fun (i : ι) ↦ (V i).subtype))
        v),
    v = 0
⊢ iSupIndep V
have h₄ : ∀ (v : Π₀ (i : ι), ↥(V i))
  (hv :
    Eq.{u_2 + 1} (α := E)
      (((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
              fun (i : ι) ↦ (V i).subtype :
            (a : Π₀ (i : ι), ↥(V i)) → E)
          v :
        E)
      (0 : E)),
  v = 0
Tactic: classical
  apply iSupIndep_of_dfinsupp_lsum_injective
  refine LinearMap.ker_eq_bot.mp ?_
  rw [Submodule.eq_bot_iff]
  intro v hv
  rw [LinearMap.mem_ker] at hv
  ext i
  suffices ⟪(v i : E), v i⟫ = 0 by simpa only [inner_self_eq_zero] using this
  calc
    ⟪(v i : E), v i⟫ = ⟪(v i : E), DFinsupp.lsum ℕ (fun i => (V i).subtype) v⟫ := by
      simpa only [DFinsupp.sumAddHom_apply, DFinsupp.lsum_apply_apply] using
        (hV.inner_right_dfinsupp v i (v i)).symm
    _ = 0 := by simp only [hv, inner_zero_right]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
h :
  Function.Injective (α := Π₀ (i : ι), ↥(V i)) (β := E)
    (⇑((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
          fun (i : ι) ↦ (V i).subtype) :
      (a : Π₀ (i : ι), ↥(V i)) → E)
h₁ :
  Eq (α := Submodule 𝕜 (Π₀ (i : ι), ↥(V i)))
    (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
      ((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
        fun (i : ι) ↦ (V i).subtype))
    ⊥
h₂ h₃ :
  ∀ (v : Π₀ (i : ι), ↥(V i))
    (hv :
      Membership.mem (γ := Submodule 𝕜 (Π₀ (i : ι), ↥(V i)))
        (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
          ((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
            fun (i : ι) ↦ (V i).subtype))
        v),
    v = 0
h₄ :
  ∀ (v : Π₀ (i : ι), ↥(V i))
    (hv :
      Eq.{u_2 + 1} (α := E)
        (((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
                fun (i : ι) ↦ (V i).subtype :
              (a : Π₀ (i : ι), ↥(V i)) → E)
            v :
          E)
        (0 : E)),
    v = 0
⊢ iSupIndep V
have h₅ : ∀ (v : Π₀ (i : ι), ↥(V i))
  (hv :
    Eq.{u_2 + 1} (α := E)
      (((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
              fun (i : ι) ↦ (V i).subtype :
            (a : Π₀ (i : ι), ↥(V i)) → E)
          v :
        E)
      (0 : E))
  (i : ι), (↑((v : (a : ι) → ↥(V a)) i) : E) = (↑(((0 : Π₀ (i : ι), ↥(V i)) : (a : ι) → ↥(V a)) i) : E)
Tactic: classical
  apply iSupIndep_of_dfinsupp_lsum_injective
  refine LinearMap.ker_eq_bot.mp ?_
  rw [Submodule.eq_bot_iff]
  intro v hv
  rw [LinearMap.mem_ker] at hv
  ext i
  suffices ⟪(v i : E), v i⟫ = 0 by simpa only [inner_self_eq_zero] using this
  calc
    ⟪(v i : E), v i⟫ = ⟪(v i : E), DFinsupp.lsum ℕ (fun i => (V i).subtype) v⟫ := by
      simpa only [DFinsupp.sumAddHom_apply, DFinsupp.lsum_apply_apply] using
        (hV.inner_right_dfinsupp v i (v i)).symm
    _ = 0 := by simp only [hv, inner_zero_right]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
h :
  Function.Injective (α := Π₀ (i : ι), ↥(V i)) (β := E)
    (⇑((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
          fun (i : ι) ↦ (V i).subtype) :
      (a : Π₀ (i : ι), ↥(V i)) → E)
h₁ :
  Eq (α := Submodule 𝕜 (Π₀ (i : ι), ↥(V i)))
    (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
      ((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
        fun (i : ι) ↦ (V i).subtype))
    ⊥
h₂ h₃ :
  ∀ (v : Π₀ (i : ι), ↥(V i))
    (hv :
      Membership.mem (γ := Submodule 𝕜 (Π₀ (i : ι), ↥(V i)))
        (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
          ((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
            fun (i : ι) ↦ (V i).subtype))
        v),
    v = 0
h₄ :
  ∀ (v : Π₀ (i : ι), ↥(V i))
    (hv :
      Eq.{u_2 + 1} (α := E)
        (((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
                fun (i : ι) ↦ (V i).subtype :
              (a : Π₀ (i : ι), ↥(V i)) → E)
            v :
          E)
        (0 : E)),
    v = 0
h₅ :
  ∀ (v : Π₀ (i : ι), ↥(V i))
    (hv :
      Eq.{u_2 + 1} (α := E)
        (((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
                fun (i : ι) ↦ (V i).subtype :
              (a : Π₀ (i : ι), ↥(V i)) → E)
            v :
          E)
        (0 : E))
    (i : ι), (↑((v : (a : ι) → ↥(V a)) i) : E) = (↑(((0 : Π₀ (i : ι), ↥(V i)) : (a : ι) → ↥(V a)) i) : E)
⊢ iSupIndep V
have h₆ : ∀ (v : Π₀ (i : ι), ↥(V i))
  (hv :
    Eq.{u_2 + 1} (α := E)
      (((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(V i)) : (a : (i : ι) → ↥(V i) →ₗ[𝕜] E) → (Π₀ (i : ι), ↥(V i)) →ₗ[𝕜] E)
              fun (i : ι) ↦ (V i).subtype :
            (a : Π₀ (i : ι), ↥(V i)) → E)
          v :
        E)
      (0 : E))
  (i : ι), ⟪(↑((v : (a : ι) → ↥(V a)) i) : E), (↑((v : (a : ι) → ↥(V a)) i) : E)⟫ = 0
Tactic: classical
  apply iSupIndep_of_dfinsupp_lsum_injective
  refine LinearMap.ker_eq_bot.mp ?_
  rw [Submodule.eq_bot_iff]
  intro v hv
  rw [LinearMap.mem_ker] at hv
  ext i
  suffices ⟪(v i : E), v i⟫ = 0 by simpa only [inner_self_eq_zero] using this
  calc
    ⟪(v i : E), v i⟫ = ⟪(v i : E), DFinsupp.lsum ℕ (fun i => (V i).subtype) v⟫ := by
      simpa only [DFinsupp.sumAddHom_apply, DFinsupp.lsum_apply_apply] using
        (hV.inner_right_dfinsupp v i (v i)).symm
    _ = 0 := by simp only [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 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(T : (a : E) → E) x, y⟫ = ⟪(T : (a : E) → E) y, x⟫
have rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x, (T : (a : E) → E) y⟫ = ⟪(T : (a : E) → E) y, x⟫
Tactic: rw [hT x y, inner_conj_symm]
-- 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
rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x, (T : (a : E) → E) y⟫ = ⟪(T : (a : E) → E) y, x⟫
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(T : (a : E) → E) x, y⟫ = ⟪(T : (a : E) → E) y, x⟫
have rw₁ : ⟪(T : (a : E) → E) y, x⟫ = ⟪(T : (a : E) → E) y, x⟫
Tactic: rw [hT x y, inner_conj_symm]
-- 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
⊢ ⟪(T + S : (a : E) → E) x, y⟫ = ⟪x, (T + S : (a : E) → E) y⟫
have rw : ⟪HAdd.hAdd (α := E) (β := E) ((T : (a : E) → E) x : E) ((S : (a : E) → E) x : E), y⟫ = ⟪x, (T + S : (a : E) → E) y⟫
Tactic: rw [add_apply, inner_add_left, hT x y, hS x y, ← inner_add_right, add_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 S : E →ₗ[𝕜] E
hT : T.IsSymmetric
hS : S.IsSymmetric
x y : E
rw : ⟪HAdd.hAdd (α := E) (β := E) ((T : (a : E) → E) x : E) ((S : (a : E) → E) x : E), y⟫ = ⟪x, (T + S : (a : E) → E) y⟫
⊢ ⟪(T + S : (a : E) → E) x, y⟫ = ⟪x, (T + S : (a : E) → E) y⟫
have rw₁ : ⟪(T : (a : E) → E) x, y⟫ + ⟪(S : (a : E) → E) x, y⟫ = ⟪x, (T + S : (a : E) → E) y⟫
Tactic: rw [add_apply, inner_add_left, hT x y, hS x y, ← inner_add_right, add_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 S : E →ₗ[𝕜] E
hT : T.IsSymmetric
hS : S.IsSymmetric
x y : E
rw : ⟪HAdd.hAdd (α := 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⟫
⊢ ⟪(T + S : (a : E) → E) x, y⟫ = ⟪x, (T + S : (a : E) → E) y⟫
have rw₂ : ⟪x, (T : (a : E) → E) y⟫ + ⟪(S : (a : E) → E) x, y⟫ = ⟪x, (T + S : (a : E) → E) y⟫
Tactic: rw [add_apply, inner_add_left, hT x y, hS x y, ← inner_add_right, add_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 S : E →ₗ[𝕜] E
hT : T.IsSymmetric
hS : S.IsSymmetric
x y : E
rw : ⟪HAdd.hAdd (α := 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⟫
⊢ ⟪(T + S : (a : E) → E) x, y⟫ = ⟪x, (T + S : (a : E) → E) y⟫
have rw₃ : ⟪x, (T : (a : E) → E) y⟫ + ⟪x, (S : (a : E) → E) y⟫ = ⟪x, (T + S : (a : E) → E) y⟫
Tactic: rw [add_apply, inner_add_left, hT x y, hS x y, ← inner_add_right, add_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 S : E →ₗ[𝕜] E
hT : T.IsSymmetric
hS : S.IsSymmetric
x y : E
rw : ⟪HAdd.hAdd (α := 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⟫
⊢ ⟪(T + S : (a : E) → E) x, y⟫ = ⟪x, (T + S : (a : E) → E) y⟫
have rw₄ : ⟪x, HAdd.hAdd (α := E) (β := E) ((T : (a : E) → E) y : E) ((S : (a : E) → E) y : E)⟫ = ⟪x, (T + S : (a : E) → E) y⟫
Tactic: rw [add_apply, inner_add_left, hT x y, hS x y, ← inner_add_right, add_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 S : E →ₗ[𝕜] E
hT : T.IsSymmetric
hS : S.IsSymmetric
x y : E
rw : ⟪HAdd.hAdd (α := 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, HAdd.hAdd (α := 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, HAdd.hAdd (α := E) (β := E) ((T : (a : E) → E) y : E) ((S : (a : E) → E) y : E)⟫ =
  ⟪x, HAdd.hAdd (α := E) (β := E) ((T : (a : E) → E) y : E) ((S : (a : E) → E) y : E)⟫
Tactic: rw [add_apply, inner_add_left, hT x y, hS x y, ← inner_add_right, add_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 S : E →ₗ[𝕜] E
hT : T.IsSymmetric
hS : S.IsSymmetric
x y : E
⊢ ⟪(T - S : (a : E) → E) x, y⟫ = ⟪x, (T - S : (a : E) → E) y⟫
have 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⟫
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
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⟫
⊢ ⟪(T - S : (a : E) → E) x, y⟫ = ⟪x, (T - S : (a : E) → E) y⟫
have rw₁ : ⟪(T : (a : E) → E) x, y⟫ - ⟪(S : (a : E) → E) x, y⟫ = ⟪x, (T - S : (a : E) → E) y⟫
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
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⟫
⊢ ⟪(T - S : (a : E) → E) x, y⟫ = ⟪x, (T - S : (a : E) → E) y⟫
have rw₂ : ⟪x, (T : (a : E) → E) y⟫ - ⟪(S : (a : E) → E) x, y⟫ = ⟪x, (T - S : (a : E) → E) y⟫
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
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⟫
⊢ ⟪(T - S : (a : E) → E) x, y⟫ = ⟪x, (T - S : (a : E) → E) y⟫
have rw₃ : ⟪x, (T : (a : E) → E) y⟫ - ⟪x, (S : (a : E) → E) y⟫ = ⟪x, (T - S : (a : E) → E) y⟫
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
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⟫
⊢ ⟪(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, (T - S : (a : E) → E) y⟫
Tactic: rw [sub_apply, inner_sub_left, hT x y, hS x y, ← inner_sub_right, sub_apply]