awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.JointEigenspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
A B : E →ₗ[𝕜] E
hA : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) A
hB : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) B
i j : 𝕜 × 𝕜
hij : i ≠ j
v : E
h : v ∈ eigenspace A i.2 ⊓ eigenspace B i.1
hv1 : v ∈ (↑(eigenspace A i.2) : Set E)
hv2 : v ∈ (↑(eigenspace B i.1) : Set E)
h₁ : i.1 ≠ j.1
w : E
⊢ w ∈ eigenspace A j.2 ⊓ eigenspace B j.1 → inner 𝕜 w v = 0
have inl : ∀ (hw1 : w ∈ (↑(eigenspace A j.2) : Set E)) (hw2 : w ∈ (↑(eigenspace B j.1) : Set E)), inner 𝕜 w v = 0
Tactic: ⟨hw1, hw2⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.JointEigenspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
A B : E →ₗ[𝕜] E
hA : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) A
hB : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) B
i j : 𝕜 × 𝕜
hij : i ≠ j
v : E
h : v ∈ eigenspace A i.2 ⊓ eigenspace B i.1
hv1 : v ∈ (↑(eigenspace A i.2) : Set E)
hv2 : v ∈ (↑(eigenspace B i.1) : Set E)
h₂ : i.2 ≠ j.2
w : E
⊢ w ∈ eigenspace A j.2 ⊓ eigenspace B j.1 → inner 𝕜 w v = 0
have inr : ∀ (hw1 : w ∈ (↑(eigenspace A j.2) : Set E)) (hw2 : w ∈ (↑(eigenspace B j.1) : Set E)), inner 𝕜 w v = 0
Tactic: ⟨hw1, hw2⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.JointEigenspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
hT : ∀ (i : n), IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (T i)
f g : n → 𝕜
hfg : f ≠ g
Ef : ↥(⨅ (j : n), (T j).eigenspace (f j))
Eg : ↥(⨅ (j : n), (T j).eigenspace (g j))
⊢ inner 𝕜 (E := E)
      (((fun (γ : n → 𝕜) ↦
                (subtypeₗᵢ (⨅ (j : n), (T j).eigenspace (γ j)) : ↥(⨅ (j : n), (T j).eigenspace (γ j)) →ₗᵢ[𝕜] E))
              f :
            (a : (fun (γ : n → 𝕜) ↦ ↥(⨅ (j : n), (T j).eigenspace (γ j))) f) → E)
          Ef :
        E)
      (((fun (γ : n → 𝕜) ↦
                (subtypeₗᵢ (⨅ (j : n), (T j).eigenspace (γ j)) : ↥(⨅ (j : n), (T j).eigenspace (γ j)) →ₗᵢ[𝕜] E))
              g :
            (a : (fun (γ : n → 𝕜) ↦ ↥(⨅ (j : n), (T j).eigenspace (γ j))) g) → E)
          Eg :
        E) =
    0
have obtain : ∀ (a : n) (ha : f a ≠ g a),
  inner 𝕜 (E := E)
      (((fun (γ : n → 𝕜) ↦
                (subtypeₗᵢ (⨅ (j : n), (T j).eigenspace (γ j)) : ↥(⨅ (j : n), (T j).eigenspace (γ j)) →ₗᵢ[𝕜] E))
              f :
            (a : (fun (γ : n → 𝕜) ↦ ↥(⨅ (j : n), (T j).eigenspace (γ j))) f) → E)
          Ef :
        E)
      (((fun (γ : n → 𝕜) ↦
                (subtypeₗᵢ (⨅ (j : n), (T j).eigenspace (γ j)) : ↥(⨅ (j : n), (T j).eigenspace (γ j)) →ₗᵢ[𝕜] E))
              g :
            (a : (fun (γ : n → 𝕜) ↦ ↥(⨅ (j : n), (T j).eigenspace (γ j))) g) → E)
          Eg :
        E) =
    0
Tactic: obtain ⟨a, ha⟩ := Function.ne_iff.mp hfg
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.JointEigenspace (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
hT : ∀ (i : n), IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (T i)
f g : n → 𝕜
hfg : f ≠ g
Ef : ↥(⨅ (j : n), (T j).eigenspace (f j))
Eg : ↥(⨅ (j : n), (T j).eigenspace (g j))
a : n
ha : f a ≠ g a
⊢ inner 𝕜 (E := E)
      (((fun (γ : n → 𝕜) ↦
                (subtypeₗᵢ (⨅ (j : n), (T j).eigenspace (γ j)) : ↥(⨅ (j : n), (T j).eigenspace (γ j)) →ₗᵢ[𝕜] E))
              f :
            (a : (fun (γ : n → 𝕜) ↦ ↥(⨅ (j : n), (T j).eigenspace (γ j))) f) → E)
          Ef :
        E)
      (((fun (γ : n → 𝕜) ↦
                (subtypeₗᵢ (⨅ (j : n), (T j).eigenspace (γ j)) : ↥(⨅ (j : n), (T j).eigenspace (γ j)) →ₗᵢ[𝕜] E))
              g :
            (a : (fun (γ : n → 𝕜) ↦ ↥(⨅ (j : n), (T j).eigenspace (γ j))) g) → E)
          Eg :
        E) =
    0
have H : (fun (i j : 𝕜) ↦
    ∀ (v : (fun (μ : 𝕜) ↦ ↥((T a).eigenspace μ)) i) (w : (fun (μ : 𝕜) ↦ ↥((T a).eigenspace μ)) j),
      inner 𝕜 (E := E)
          (((fun (μ : 𝕜) ↦ ((T a).eigenspace μ).subtypeₗᵢ) i : (a : (fun (μ : 𝕜) ↦ ↥((T a).eigenspace μ)) i) → E) v : E)
          (((fun (μ : 𝕜) ↦ ((T a).eigenspace μ).subtypeₗᵢ) j : (a : (fun (μ : 𝕜) ↦ ↥((T a).eigenspace μ)) j) → E) w :
            E) =
        0)
  (f a) (g a)
Tactic: have H := orthogonalFamily_eigenspaces (hT a) ha
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.JointEigenspace (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
hT : ∀ (i : n), IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (T i)
f g : n → 𝕜
hfg : f ≠ g
Ef : ↥(⨅ (j : n), (T j).eigenspace (f j))
Eg : ↥(⨅ (j : n), (T j).eigenspace (g j))
a : n
ha : f a ≠ g a
H :
  (fun (i j : 𝕜) ↦
      ∀ (v : (fun (μ : 𝕜) ↦ ↥((T a).eigenspace μ)) i) (w : (fun (μ : 𝕜) ↦ ↥((T a).eigenspace μ)) j),
        inner 𝕜 (E := E)
            (((fun (μ : 𝕜) ↦ ((T a).eigenspace μ).subtypeₗᵢ) i : (a : (fun (μ : 𝕜) ↦ ↥((T a).eigenspace μ)) i) → E) v :
              E)
            (((fun (μ : 𝕜) ↦ ((T a).eigenspace μ).subtypeₗᵢ) j : (a : (fun (μ : 𝕜) ↦ ↥((T a).eigenspace μ)) j) → E) w :
              E) =
          0)
    (f a) (g a)
⊢ inner 𝕜 (E := E)
      (((fun (γ : n → 𝕜) ↦
                (subtypeₗᵢ (⨅ (j : n), (T j).eigenspace (γ j)) : ↥(⨅ (j : n), (T j).eigenspace (γ j)) →ₗᵢ[𝕜] E))
              f :
            (a : (fun (γ : n → 𝕜) ↦ ↥(⨅ (j : n), (T j).eigenspace (γ j))) f) → E)
          Ef :
        E)
      (((fun (γ : n → 𝕜) ↦
                (subtypeₗᵢ (⨅ (j : n), (T j).eigenspace (γ j)) : ↥(⨅ (j : n), (T j).eigenspace (γ j)) →ₗᵢ[𝕜] E))
              g :
            (a : (fun (γ : n → 𝕜) ↦ ↥(⨅ (j : n), (T j).eigenspace (γ j))) g) → E)
          Eg :
        E) =
    0
have H₁ : ∀ (a_1 : E) (b : a_1 ∈ (T a).eigenspace (f a)) (a_2 : E) (b : a_2 ∈ (T a).eigenspace (g a)), inner 𝕜 a_1 a_2 = 0
Tactic: simp only [Submodule.coe_subtypeₗᵢ, Submodule.coe_subtype, Subtype.forall] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.JointEigenspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
hT : ∀ (i : n), IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (T i)
f g : n → 𝕜
hfg : f ≠ g
Ef : ↥(⨅ (j : n), (T j).eigenspace (f j))
Eg : ↥(⨅ (j : n), (T j).eigenspace (g j))
a : n
ha : f a ≠ g a
H : ∀ (a_1 : E) (b : a_1 ∈ (T a).eigenspace (f a)) (a_2 : E) (b : a_2 ∈ (T a).eigenspace (g a)), inner 𝕜 a_1 a_2 = 0
⊢ inner 𝕜 (E := E)
      (((fun (γ : n → 𝕜) ↦
                (subtypeₗᵢ (⨅ (j : n), (T j).eigenspace (γ j)) : ↥(⨅ (j : n), (T j).eigenspace (γ j)) →ₗᵢ[𝕜] E))
              f :
            (a : (fun (γ : n → 𝕜) ↦ ↥(⨅ (j : n), (T j).eigenspace (γ j))) f) → E)
          Ef :
        E)
      (((fun (γ : n → 𝕜) ↦
                (subtypeₗᵢ (⨅ (j : n), (T j).eigenspace (γ j)) : ↥(⨅ (j : n), (T j).eigenspace (γ j)) →ₗᵢ[𝕜] E))
              g :
            (a : (fun (γ : n → 𝕜) ↦ ↥(⨅ (j : n), (T j).eigenspace (γ j))) g) → E)
          Eg :
        E) =
    0
have b : Membership.mem (α := E) ((T a).eigenspace (f a))
  (((fun (γ : n → 𝕜) ↦ (subtypeₗᵢ (⨅ (j : n), (T j).eigenspace (γ j)) : ↥(⨅ (j : n), (T j).eigenspace (γ j)) →ₗᵢ[𝕜] E))
          f :
        (a : (fun (γ : n → 𝕜) ↦ ↥(⨅ (j : n), (T j).eigenspace (γ j))) f) → E)
      Ef :
    E)
Tactic: apply H
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.JointEigenspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
hT : ∀ (i : n), IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (T i)
f g : n → 𝕜
hfg : f ≠ g
Ef : ↥(⨅ (j : n), (T j).eigenspace (f j))
Eg : ↥(⨅ (j : n), (T j).eigenspace (g j))
a : n
ha : f a ≠ g a
H : ∀ (a_1 : E) (b : a_1 ∈ (T a).eigenspace (f a)) (a_2 : E) (b : a_2 ∈ (T a).eigenspace (g a)), inner 𝕜 a_1 a_2 = 0
b :
  Membership.mem (α := E) ((T a).eigenspace (f a))
    (((fun (γ : n → 𝕜) ↦
              (subtypeₗᵢ (⨅ (j : n), (T j).eigenspace (γ j)) : ↥(⨅ (j : n), (T j).eigenspace (γ j)) →ₗᵢ[𝕜] E))
            f :
          (a : (fun (γ : n → 𝕜) ↦ ↥(⨅ (j : n), (T j).eigenspace (γ j))) f) → E)
        Ef :
      E)
⊢ inner 𝕜 (E := E)
      (((fun (γ : n → 𝕜) ↦
                (subtypeₗᵢ (⨅ (j : n), (T j).eigenspace (γ j)) : ↥(⨅ (j : n), (T j).eigenspace (γ j)) →ₗᵢ[𝕜] E))
              f :
            (a : (fun (γ : n → 𝕜) ↦ ↥(⨅ (j : n), (T j).eigenspace (γ j))) f) → E)
          Ef :
        E)
      (((fun (γ : n → 𝕜) ↦
                (subtypeₗᵢ (⨅ (j : n), (T j).eigenspace (γ j)) : ↥(⨅ (j : n), (T j).eigenspace (γ j)) →ₗᵢ[𝕜] E))
              g :
            (a : (fun (γ : n → 𝕜) ↦ ↥(⨅ (j : n), (T j).eigenspace (γ j))) g) → E)
          Eg :
        E) =
    0
have b₁ : Membership.mem (α := E) ((T a).eigenspace (g a))
  (((fun (γ : n → 𝕜) ↦ (subtypeₗᵢ (⨅ (j : n), (T j).eigenspace (γ j)) : ↥(⨅ (j : n), (T j).eigenspace (γ j)) →ₗᵢ[𝕜] E))
          g :
        (a : (fun (γ : n → 𝕜) ↦ ↥(⨅ (j : n), (T j).eigenspace (γ j))) g) → E)
      Eg :
    E)
Tactic: apply H
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.JointEigenspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
α : 𝕜
A B : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
hB : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) B
hAB : Commute A B
| eigenspace A α
have rw : map (eigenspace A α).subtype ⊤
Tactic: rw [← (eigenspace A α).map_subtype_top]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.JointEigenspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
α : 𝕜
A B : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
hB : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) B
hAB : Commute A B
⊢ ⨆ (γ : 𝕜), eigenspace A α ⊓ eigenspace B γ = eigenspace A α
have conv_rhs : ⨆ (γ : 𝕜), eigenspace A α ⊓ eigenspace B γ = map (eigenspace A α).subtype ⊤
Tactic: conv_rhs => rw [← (eigenspace A α).map_subtype_top]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.JointEigenspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
α : 𝕜
A B : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
hB : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) B
hAB : Commute A B
⊢ ⨆ (γ : 𝕜), eigenspace A α ⊓ eigenspace B γ = map (eigenspace A α).subtype ⊤
have simp : map (eigenspace A α).subtype
    (⨆ (i : 𝕜), (genEigenspace (B.restrict sorry) i : (a : ℕ∞) → Submodule 𝕜 ↥(eigenspace A α)) 1) =
  map (eigenspace A α).subtype ⊤
Tactic: simp only [← Submodule.map_iSup,
    (eigenspace A α).inf_genEigenspace _ (mapsTo_genEigenspace_of_comm hAB α 1)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.JointEigenspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
α : 𝕜
A B : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
hB : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) B
hAB : Commute A B
⊢ map (eigenspace A α).subtype
      (⨆ (i : 𝕜), (genEigenspace (B.restrict ⋯) i : (a : ℕ∞) → Submodule 𝕜 ↥(eigenspace A α)) 1) =
    map (eigenspace A α).subtype ⊤
have e_p : Eq.{u_2 + 1} (α := Submodule 𝕜 ↥(eigenspace A α))
  (⨆ (i : 𝕜), (genEigenspace (B.restrict sorry) i : (a : ℕ∞) → Submodule 𝕜 ↥(eigenspace A α)) 1) ⊤
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.JointEigenspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
A B : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
hA : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) A
hB : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) B
hAB : Commute A B
⊢ DirectSum.IsInternal (S := Submodule 𝕜 E) fun (i : 𝕜 × 𝕜) ↦ eigenspace A i.2 ⊓ eigenspace B i.1
have apply : Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (i : 𝕜 × 𝕜), eigenspace A i.2 ⊓ eigenspace B i.1)ᗮ ⊥
Tactic: apply (orthogonalFamily_eigenspace_inf_eigenspace hA hB).isInternal_iff.mpr
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.JointEigenspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
A B : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
hA : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) A
hB : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) B
hAB : Commute A B
⊢ Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (i : 𝕜 × 𝕜), eigenspace A i.2 ⊓ eigenspace B i.1)ᗮ ⊥
have rw : Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (j : 𝕜), ⨆ (i : 𝕜), eigenspace A (i, j).2 ⊓ eigenspace B (i, j).1) ⊤
Tactic: rw [Submodule.orthogonal_eq_bot_iff, iSup_prod, iSup_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.JointEigenspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
ι : Type u_5
T : ι → E →ₗ[𝕜] E
hT : ∀ (i : ι), IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (T i)
h : Pairwise (Commute on T)
x : ι
⊢ Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (μ : 𝕜), maxGenEigenspace (T x) μ) ⊤
have rw : Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (μ : 𝕜), maxGenEigenspace (T x) μ)ᗮ ⊥
Tactic: rw [← orthogonal_eq_bot_iff,
      congr(⨆ μ, $(maxGenEigenspace_eq_eigenspace (isFinitelySemisimple <| hT _) μ)),
      (hT _).orthogonalComplement_iSup_eigenspaces_eq_bot]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.JointEigenspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
ι : Type u_5
T : ι → E →ₗ[𝕜] E
hT : ∀ (i : ι), IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (T i)
h : Pairwise (Commute on T)
x : ι
rw : Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (μ : 𝕜), maxGenEigenspace (T x) μ)ᗮ ⊥
⊢ Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (μ : 𝕜), maxGenEigenspace (T x) μ) ⊤
have rw₁ : Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (μ : 𝕜), eigenspace (T x) μ)ᗮ ⊥
Tactic: rw [← orthogonal_eq_bot_iff,
      congr(⨆ μ, $(maxGenEigenspace_eq_eigenspace (isFinitelySemisimple <| hT _) μ)),
      (hT _).orthogonalComplement_iSup_eigenspaces_eq_bot]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.JointEigenspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
ι : Type u_5
T : ι → E →ₗ[𝕜] E
hT : ∀ (i : ι), IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (T i)
h : Pairwise (Commute on T)
x : ι
rw : Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (μ : 𝕜), maxGenEigenspace (T x) μ)ᗮ ⊥
rw₁ : Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (μ : 𝕜), eigenspace (T x) μ)ᗮ ⊥
⊢ Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (μ : 𝕜), maxGenEigenspace (T x) μ) ⊤
have rw₂ : Eq.{u_2 + 1} (α := Submodule 𝕜 E) ⊥ ⊥
Tactic: rw [← orthogonal_eq_bot_iff,
      congr(⨆ μ, $(maxGenEigenspace_eq_eigenspace (isFinitelySemisimple <| hT _) μ)),
      (hT _).orthogonalComplement_iSup_eigenspaces_eq_bot]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.JointEigenspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : DecidableEq (n → 𝕜)
hT : ∀ (i : n), IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (T i)
hC : Pairwise (Commute on T)
⊢ DirectSum.IsInternal (S := Submodule 𝕜 E) fun (α : n → 𝕜) ↦ ⨅ (j : n), (T j).eigenspace (α j)
have rw : Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (α : n → 𝕜), ⨅ (j : n), (T j).eigenspace (α j))ᗮ ⊥
Tactic: rw [OrthogonalFamily.isInternal_iff]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.JointEigenspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : DecidableEq (n → 𝕜)
hT : ∀ (i : n), IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (T i)
hC : Pairwise (Commute on T)
rw : Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (α : n → 𝕜), ⨅ (j : n), (T j).eigenspace (α j))ᗮ ⊥
⊢ DirectSum.IsInternal (S := Submodule 𝕜 E) fun (α : n → 𝕜) ↦ ⨅ (j : n), (T j).eigenspace (α j)
have rw₁ : OrthogonalFamily 𝕜 (E := E) (fun (i : n → 𝕜) ↦ ↥(⨅ (j : n), (T j).eigenspace (i j))) fun (i : n → 𝕜) ↦
  subtypeₗᵢ (⨅ (j : n), (T j).eigenspace (i j))
Tactic: rw [OrthogonalFamily.isInternal_iff]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.JointEigenspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : DecidableEq (n → 𝕜)
hT : ∀ (i : n), IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (T i)
hC : Pairwise (Commute on T)
⊢ Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (α : n → 𝕜), ⨅ (j : n), (T j).eigenspace (α j))ᗮ ⊥
have rw : Eq.{u_2 + 1} (α := Submodule 𝕜 E) ⊤ᗮ ⊥
Tactic: rw [iSup_iInf_eq_top_of_commute hT hC, top_orthogonal_eq_bot]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.JointEigenspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : DecidableEq (n → 𝕜)
hT : ∀ (i : n), IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (T i)
hC : Pairwise (Commute on T)
rw : Eq.{u_2 + 1} (α := Submodule 𝕜 E) ⊤ᗮ ⊥
⊢ Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (α : n → 𝕜), ⨅ (j : n), (T j).eigenspace (α j))ᗮ ⊥
have rw₁ : Eq.{u_2 + 1} (α := Submodule 𝕜 E) ⊥ ⊥
Tactic: rw [iSup_iInf_eq_top_of_commute hT hC, top_orthogonal_eq_bot]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
e : E
s : Set E
f : E → F
hs : UniqueDiffOn 𝕜 s
he : e ∈ s
e₁ e₂ : E
⊢ Eq.{u_3 + 1} (α := F) ((tensorIteratedFDerivWithinTwo 𝕜 f s e : (a : E ⊗[𝕜] E) → F) (e₁ ⊗ₜ[𝕜] e₂) : F)
    ((iteratedFDerivWithin 𝕜 2 f s e : (a : (i : Fin 2) → E) → F) ![e₁, e₂] : F)
have rw : Eq.{u_3 + 1} (α := F) ((tensorIteratedFDerivWithinTwo 𝕜 f s e : (a : E ⊗[𝕜] E) → F) (e₁ ⊗ₜ[𝕜] e₂) : F)
  ((((bilinearIteratedFDerivWithinTwo 𝕜 f s e : (a : E) → E →ₗ[𝕜] F) e₁ : E →ₗ[𝕜] F) : (a : E) → F) e₂ : F)
Tactic: rw [← bilinearIteratedFDerivWithinTwo_eq_iteratedFDeriv f hs he, tensorIteratedFDerivWithinTwo,
    lift.tmul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
e : E
s : Set E
f : E → F
hs : UniqueDiffOn 𝕜 s
he : e ∈ s
e₁ e₂ : E
rw :
  Eq.{u_3 + 1} (α := F) ((tensorIteratedFDerivWithinTwo 𝕜 f s e : (a : E ⊗[𝕜] E) → F) (e₁ ⊗ₜ[𝕜] e₂) : F)
    ((((bilinearIteratedFDerivWithinTwo 𝕜 f s e : (a : E) → E →ₗ[𝕜] F) e₁ : E →ₗ[𝕜] F) : (a : E) → F) e₂ : F)
⊢ Eq.{u_3 + 1} (α := F) ((tensorIteratedFDerivWithinTwo 𝕜 f s e : (a : E ⊗[𝕜] E) → F) (e₁ ⊗ₜ[𝕜] e₂) : F)
    ((iteratedFDerivWithin 𝕜 2 f s e : (a : (i : Fin 2) → E) → F) ![e₁, e₂] : F)
have rw₁ : Eq.{u_3 + 1} (α := F) ((lift (bilinearIteratedFDerivWithinTwo 𝕜 f s e) : (a : E ⊗[𝕜] E) → F) (e₁ ⊗ₜ[𝕜] e₂) : F)
  ((((bilinearIteratedFDerivWithinTwo 𝕜 f s e : (a : E) → E →ₗ[𝕜] F) e₁ : E →ₗ[𝕜] F) : (a : E) → F) e₂ : F)
Tactic: rw [← bilinearIteratedFDerivWithinTwo_eq_iteratedFDeriv f hs he, tensorIteratedFDerivWithinTwo,
    lift.tmul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
e : E
s : Set E
f : E → F
hs : UniqueDiffOn 𝕜 s
he : e ∈ s
e₁ e₂ : E
rw :
  Eq.{u_3 + 1} (α := F) ((tensorIteratedFDerivWithinTwo 𝕜 f s e : (a : E ⊗[𝕜] E) → F) (e₁ ⊗ₜ[𝕜] e₂) : F)
    ((((bilinearIteratedFDerivWithinTwo 𝕜 f s e : (a : E) → E →ₗ[𝕜] F) e₁ : E →ₗ[𝕜] F) : (a : E) → F) e₂ : F)
rw₁ :
  Eq.{u_3 + 1} (α := F) ((lift (bilinearIteratedFDerivWithinTwo 𝕜 f s e) : (a : E ⊗[𝕜] E) → F) (e₁ ⊗ₜ[𝕜] e₂) : F)
    ((((bilinearIteratedFDerivWithinTwo 𝕜 f s e : (a : E) → E →ₗ[𝕜] F) e₁ : E →ₗ[𝕜] F) : (a : E) → F) e₂ : F)
⊢ Eq.{u_3 + 1} (α := F) ((tensorIteratedFDerivWithinTwo 𝕜 f s e : (a : E ⊗[𝕜] E) → F) (e₁ ⊗ₜ[𝕜] e₂) : F)
    ((iteratedFDerivWithin 𝕜 2 f s e : (a : (i : Fin 2) → E) → F) ![e₁, e₂] : F)
have rw₂ : Eq.{u_3 + 1} (α := F)
  ((((bilinearIteratedFDerivWithinTwo 𝕜 f s e : (a : E) → E →ₗ[𝕜] F) e₁ : E →ₗ[𝕜] F) : (a : E) → F) e₂ : F)
  ((((bilinearIteratedFDerivWithinTwo 𝕜 f s e : (a : E) → E →ₗ[𝕜] F) e₁ : E →ₗ[𝕜] F) : (a : E) → F) e₂ : F)
Tactic: rw [← bilinearIteratedFDerivWithinTwo_eq_iteratedFDeriv f hs he, tensorIteratedFDerivWithinTwo,
    lift.tmul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
e e₁ e₂ : E
⊢ Eq.{u_3 + 1} (α := F) ((tensorIteratedFDerivTwo 𝕜 f e : (a : E ⊗[𝕜] E) → F) (e₁ ⊗ₜ[𝕜] e₂) : F)
    ((iteratedFDeriv 𝕜 2 f e : (a : (i : Fin 2) → E) → F) ![e₁, e₂] : F)
have rw : Eq.{u_3 + 1} (α := F) ((tensorIteratedFDerivTwo 𝕜 f e : (a : E ⊗[𝕜] E) → F) (e₁ ⊗ₜ[𝕜] e₂) : F)
  ((((bilinearIteratedFDerivTwo 𝕜 f e : (a : E) → E →ₗ[𝕜] F) e₁ : E →ₗ[𝕜] F) : (a : E) → F) e₂ : F)
Tactic: rw [← bilinearIteratedFDerivTwo_eq_iteratedFDeriv, tensorIteratedFDerivTwo, lift.tmul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
e e₁ e₂ : E
rw :
  Eq.{u_3 + 1} (α := F) ((tensorIteratedFDerivTwo 𝕜 f e : (a : E ⊗[𝕜] E) → F) (e₁ ⊗ₜ[𝕜] e₂) : F)
    ((((bilinearIteratedFDerivTwo 𝕜 f e : (a : E) → E →ₗ[𝕜] F) e₁ : E →ₗ[𝕜] F) : (a : E) → F) e₂ : F)
⊢ Eq.{u_3 + 1} (α := F) ((tensorIteratedFDerivTwo 𝕜 f e : (a : E ⊗[𝕜] E) → F) (e₁ ⊗ₜ[𝕜] e₂) : F)
    ((iteratedFDeriv 𝕜 2 f e : (a : (i : Fin 2) → E) → F) ![e₁, e₂] : F)
have rw₁ : Eq.{u_3 + 1} (α := F) ((lift (bilinearIteratedFDerivTwo 𝕜 f e) : (a : E ⊗[𝕜] E) → F) (e₁ ⊗ₜ[𝕜] e₂) : F)
  ((((bilinearIteratedFDerivTwo 𝕜 f e : (a : E) → E →ₗ[𝕜] F) e₁ : E →ₗ[𝕜] F) : (a : E) → F) e₂ : F)
Tactic: rw [← bilinearIteratedFDerivTwo_eq_iteratedFDeriv, tensorIteratedFDerivTwo, lift.tmul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
e e₁ e₂ : E
rw :
  Eq.{u_3 + 1} (α := F) ((tensorIteratedFDerivTwo 𝕜 f e : (a : E ⊗[𝕜] E) → F) (e₁ ⊗ₜ[𝕜] e₂) : F)
    ((((bilinearIteratedFDerivTwo 𝕜 f e : (a : E) → E →ₗ[𝕜] F) e₁ : E →ₗ[𝕜] F) : (a : E) → F) e₂ : F)
rw₁ :
  Eq.{u_3 + 1} (α := F) ((lift (bilinearIteratedFDerivTwo 𝕜 f e) : (a : E ⊗[𝕜] E) → F) (e₁ ⊗ₜ[𝕜] e₂) : F)
    ((((bilinearIteratedFDerivTwo 𝕜 f e : (a : E) → E →ₗ[𝕜] F) e₁ : E →ₗ[𝕜] F) : (a : E) → F) e₂ : F)
⊢ Eq.{u_3 + 1} (α := F) ((tensorIteratedFDerivTwo 𝕜 f e : (a : E ⊗[𝕜] E) → F) (e₁ ⊗ₜ[𝕜] e₂) : F)
    ((iteratedFDeriv 𝕜 2 f e : (a : (i : Fin 2) → E) → F) ![e₁, e₂] : F)
have rw₂ : Eq.{u_3 + 1} (α := F) ((((bilinearIteratedFDerivTwo 𝕜 f e : (a : E) → E →ₗ[𝕜] F) e₁ : E →ₗ[𝕜] F) : (a : E) → F) e₂ : F)
  ((((bilinearIteratedFDerivTwo 𝕜 f e : (a : E) → E →ₗ[𝕜] F) e₁ : E →ₗ[𝕜] F) : (a : E) → F) e₂ : F)
Tactic: rw [← bilinearIteratedFDerivTwo_eq_iteratedFDeriv, tensorIteratedFDerivTwo, lift.tmul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
⊢ Δ[Set.univ] f = Δ f
have h : ∀ (x : E), (Δ[Set.univ] f) x = Δ f x
Tactic: ext x