awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
x : E
r : ℝ
hd : HarmonicOnNhd f (ball x r)
hc : ContinuousOn f (closedBall x r)
⊢ HarmonicContOnCl f (ball x r)

Tactic:
⟨hd, hc.mono <| closure_ball_subset_closedBall⟩

Premises used: InnerProductSpace.HarmonicContOnCl.mk, Metric.closure_ball_subset_closedBall, ContinuousOn.mono
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
x : E
s : Set E
h : HarmonicContOnCl f s
hx : x ∈ s
⊢ ContDiffAt ℝ 2 f x

Tactic:
(h.1 x hx).1

Premises used: InnerProductSpace.HarmonicContOnCl.harmonicOnNhd, And.left
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
x : E
s : Set E
h : HarmonicContOnCl f s
hx : x ∈ s
⊢ DifferentiableAt ℝ f x

Tactic:
(h.contDiffAt hx).differentiableAt two_ne_zero

Premises used: ContDiffAt.differentiableAt, two_ne_zero, InnerProductSpace.HarmonicContOnCl.contDiffAt
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
s t : Set E
h : HarmonicContOnCl f s
ht : t ⊆ s
⊢ HarmonicContOnCl f t

Tactic:
⟨h.harmonicOnNhd.mono ht, h.continuousOn.mono (closure_mono ht)⟩

Premises used: InnerProductSpace.HarmonicContOnCl.mk, closure_mono, InnerProductSpace.HarmonicContOnCl.harmonicOnNhd, ContinuousOn.mono, InnerProductSpace.HarmonicOnNhd.mono, InnerProductSpace.HarmonicContOnCl.continuousOn
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f₁ f₂ : E → F
s : Set E
hf₁ : HarmonicContOnCl f₁ s
hf₂ : HarmonicContOnCl f₂ s
⊢ HarmonicContOnCl (f₁ + f₂) s

Tactic:
⟨hf₁.1.add hf₂.1, hf₁.2.add hf₂.2⟩

Premises used: InnerProductSpace.HarmonicOnNhd.add, InnerProductSpace.HarmonicContOnCl.mk, InnerProductSpace.HarmonicContOnCl.harmonicOnNhd, ContinuousOn.add, InnerProductSpace.HarmonicContOnCl.continuousOn
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
s : Set E
hf : HarmonicContOnCl f s
c : F
⊢ HarmonicContOnCl (f + fun (x : E) ↦ c) s

Tactic:
hf.add harmonicContOnCl_const

Premises used: InnerProductSpace.HarmonicContOnCl.add, InnerProductSpace.harmonicContOnCl_const
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
s : Set E
hf : HarmonicContOnCl f s
c : F
⊢ HarmonicContOnCl ((fun (x : E) ↦ c) + f) s

Tactic:
harmonicContOnCl_const.add hf

Premises used: InnerProductSpace.HarmonicContOnCl.add, InnerProductSpace.harmonicContOnCl_const
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
s : Set E
hf : HarmonicContOnCl f s
⊢ HarmonicContOnCl (-f) s

Tactic:
⟨hf.1.neg, hf.2.neg⟩

Premises used: ContinuousOn.neg, InnerProductSpace.HarmonicOnNhd.neg, InnerProductSpace.HarmonicContOnCl.mk, InnerProductSpace.HarmonicContOnCl.harmonicOnNhd, InnerProductSpace.HarmonicContOnCl.continuousOn
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f₁ f₂ : E → F
s : Set E
hf₁ : HarmonicContOnCl f₁ s
hf₂ : HarmonicContOnCl f₂ s
⊢ HarmonicContOnCl (f₁ - f₂) s

Tactic:
⟨hf₁.1.sub hf₂.1, hf₁.2.sub hf₂.2⟩

Premises used: ContinuousOn.sub, InnerProductSpace.HarmonicContOnCl.mk, InnerProductSpace.HarmonicOnNhd.sub, InnerProductSpace.HarmonicContOnCl.harmonicOnNhd, InnerProductSpace.HarmonicContOnCl.continuousOn
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
s : Set E
hf : HarmonicContOnCl f s
c : F
⊢ HarmonicContOnCl (f - fun (x : E) ↦ c) s

Tactic:
hf.sub harmonicContOnCl_const

Premises used: InnerProductSpace.harmonicContOnCl_const, InnerProductSpace.HarmonicContOnCl.sub
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
s : Set E
hf : HarmonicContOnCl f s
c : F
⊢ HarmonicContOnCl ((fun (x : E) ↦ c) - f) s

Tactic:
harmonicContOnCl_const.sub hf

Premises used: InnerProductSpace.harmonicContOnCl_const, InnerProductSpace.HarmonicContOnCl.sub
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
s : Set E
hf : HarmonicContOnCl f s
c : ℝ
⊢ HarmonicContOnCl (c • f) s

Tactic:
⟨hf.1.const_smul, hf.2.const_smul c⟩

Premises used: InnerProductSpace.HarmonicContOnCl.mk, InnerProductSpace.HarmonicOnNhd.const_smul, InnerProductSpace.HarmonicContOnCl.harmonicOnNhd, ContinuousOn.const_smul, InnerProductSpace.HarmonicContOnCl.continuousOn
-- Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace
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)
rwa :
  ∀ (hij : ¬i = j),
    ∀ 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)), i.1 ≠ j.1 ∨ i.2 ≠ j.2
rwa₁ :
  ∀ (hij : ¬(i.1 = j.1 ∧ i.2 = j.2)),
    ∀ 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)), i.1 ≠ j.1 ∨ i.2 ≠ j.2
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀ (hij : ¬i.1 = j.1 ∨ ¬i.2 = j.2),
    ∀ 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)), i.1 ≠ j.1 ∨ i.2 ≠ j.2
⊢ i.1 ≠ j.1 ∨ i.2 ≠ j.2

Tactic:
rwa [Ne.eq_def, Prod.ext_iff, not_and_or] at hij

Premises used: Prod.ext_iff, Ne.eq_def, not_and_or
-- Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace
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)
inl : ∀ (h₁ : i.1 ≠ j.1), v ∈ (eigenspace A j.2 ⊓ eigenspace B j.1)ᗮ
inr : ∀ (h₂ : i.2 ≠ j.2), v ∈ (eigenspace A j.2 ⊓ eigenspace B j.1)ᗮ
⊢ v ∈ (eigenspace A j.2 ⊓ eigenspace B j.1)ᗮ

Tactic:
obtain (h₁ | h₂) : i.1 ≠ j.1 ∨ i.2 ≠ j.2 := by rwa [Ne.eq_def, Prod.ext_iff, not_and_or] at hij

Premises used: Prod.fst, Prod.snd
-- Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace
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
inl : ∀ (hw1 : w ∈ (↑(eigenspace A j.2) : Set E)) (hw2 : w ∈ (↑(eigenspace B j.1) : Set E)), inner 𝕜 w v = 0
⊢ w ∈ eigenspace A j.2 ⊓ eigenspace B j.1 → inner 𝕜 w v = 0

Tactic:
⟨hw1, hw2⟩
-- Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace
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
inr : ∀ (hw1 : w ∈ (↑(eigenspace A j.2) : Set E)) (hw2 : w ∈ (↑(eigenspace B j.1) : Set E)), inner 𝕜 w v = 0
⊢ w ∈ eigenspace A j.2 ⊓ eigenspace B j.1 → inner 𝕜 w v = 0

Tactic:
⟨hw1, hw2⟩
-- Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace
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
hw1 : w ∈ (↑(eigenspace A j.2) : Set E)
hw2 : w ∈ (↑(eigenspace B j.1) : Set E)
⊢ inner 𝕜 w v = 0

Tactic:
hB.orthogonalFamily_eigenspaces.pairwise h₁ hv2 w hw2

Premises used: LinearMap.IsSymmetric.orthogonalFamily_eigenspaces, OrthogonalFamily.pairwise
-- Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace
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
hw1 : w ∈ (↑(eigenspace A j.2) : Set E)
hw2 : w ∈ (↑(eigenspace B j.1) : Set E)
⊢ inner 𝕜 w v = 0

Tactic:
exact hB.orthogonalFamily_eigenspaces.pairwise h₁ hv2 w hw2

Premises used: LinearMap.IsSymmetric.orthogonalFamily_eigenspaces, OrthogonalFamily.pairwise
-- Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace
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
hw1 : w ∈ (↑(eigenspace A j.2) : Set E)
hw2 : w ∈ (↑(eigenspace B j.1) : Set E)
⊢ inner 𝕜 w v = 0

Tactic:
hA.orthogonalFamily_eigenspaces.pairwise h₂ hv1 w hw1

Premises used: LinearMap.IsSymmetric.orthogonalFamily_eigenspaces, OrthogonalFamily.pairwise
-- Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace
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
hw1 : w ∈ (↑(eigenspace A j.2) : Set E)
hw2 : w ∈ (↑(eigenspace B j.1) : Set E)
⊢ inner 𝕜 w v = 0

Tactic:
exact hA.orthogonalFamily_eigenspaces.pairwise h₂ hv1 w hw1

Premises used: LinearMap.IsSymmetric.orthogonalFamily_eigenspaces, OrthogonalFamily.pairwise
-- Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace
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))
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
⊢ 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

Premises used: Function.ne_iff, Iff.mp
-- Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace
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
⊢ (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
-- Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace
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)
⊢ ∀ (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

Premises used: Subtype.forall, Submodule.coe_subtypeₗᵢ, Submodule.coe_subtype
-- Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace
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)
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)
⊢ 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:
apply H
-- Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace
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
⊢ 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:
(Submodule.mem_iInf <| fun _ ↦ eigenspace (T _) (f _)).mp Ef.2 _

Premises used: Submodule.mem_iInf, Set.Mem, Module.End.eigenspace, Iff.mp, Subtype.property
-- Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace
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
⊢ 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:
exact (Submodule.mem_iInf <| fun _ ↦ eigenspace (T _) (f _)).mp Ef.2 _

Premises used: Submodule.mem_iInf, Module.End.eigenspace, Iff.mp, Subtype.property
-- Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace
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
⊢ 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:
(Submodule.mem_iInf <| fun _ ↦ eigenspace (T _) (g _)).mp Eg.2 _

Premises used: Submodule.mem_iInf, Set.Mem, Module.End.eigenspace, Iff.mp, Subtype.property
-- Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace
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
⊢ 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:
exact (Submodule.mem_iInf <| fun _ ↦ eigenspace (T _) (g _)).mp Eg.2 _

Premises used: Submodule.mem_iInf, Module.End.eigenspace, Iff.mp, Subtype.property
-- Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace
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
rw : map (eigenspace A α).subtype ⊤
| eigenspace A α

Tactic:
rw [← (eigenspace A α).map_subtype_top]

Premises used: Module.End.eigenspace, Submodule.map_subtype_top
-- Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace
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
conv_rhs : ⨆ (γ : 𝕜), eigenspace A α ⊓ eigenspace B γ = map (eigenspace A α).subtype ⊤
⊢ ⨆ (γ : 𝕜), eigenspace A α ⊓ eigenspace B γ = eigenspace A α

Tactic:
conv_rhs => rw [← (eigenspace A α).map_subtype_top]

Premises used: Module.End.eigenspace, Submodule.map_subtype_top
-- Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace
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
simp :
  map (eigenspace A α).subtype
      (⨆ (i : 𝕜), (genEigenspace (B.restrict ⋯) i : (a : ℕ∞) → Submodule 𝕜 ↥(eigenspace A α)) 1) =
    map (eigenspace A α).subtype ⊤
⊢ ⨆ (γ : 𝕜), eigenspace A α ⊓ eigenspace B γ = map (eigenspace A α).subtype ⊤

Tactic:
simp only [← Submodule.map_iSup,
    (eigenspace A α).inf_genEigenspace _ (mapsTo_genEigenspace_of_comm hAB α 1)]

Premises used: Submodule.map_iSup, Module.End.mapsTo_genEigenspace_of_comm, Module.End.eigenspace, Submodule.inf_genEigenspace, OfNat.ofNat
-- Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace
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
e_p :
  Eq.{u_2 + 1} (α := Submodule 𝕜 ↥(eigenspace A α))
    (⨆ (i : 𝕜), (genEigenspace (B.restrict ⋯) i : (a : ℕ∞) → Submodule 𝕜 ↥(eigenspace A α)) 1) ⊤
⊢ map (eigenspace A α).subtype
      (⨆ (i : 𝕜), (genEigenspace (B.restrict ⋯) i : (a : ℕ∞) → Submodule 𝕜 ↥(eigenspace A α)) 1) =
    map (eigenspace A α).subtype ⊤

Tactic:
congr 1