-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
lemma map_add_of_iInf_genEigenspace_ne_bot_of_commute [NoZeroSMulDivisors R M]
    {L F : Type*} [Add L] [FunLike F L (End R M)] [AddHomClass F L (End R M)] (f : F)
    (μ : L → R) (k : ℕ∞) (h_ne : ⨅ x, (f x).genEigenspace (μ x) k ≠ ⊥)
    (h : ∀ x y, Commute (f x) (f y)) (x y : L) :
    μ (x + y) = μ x + μ y

Proof state:
R : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : NoZeroSMulDivisors R M
L : Type u_1
F : Type u_2
inst✝² : Add L
inst✝¹ : FunLike F L (End R M)
inst✝ : AddHomClass F L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
h : ∀ (x y : L), Commute (f x) (f y)
x y : L
contra : ¬μ (x + y) = μ x + μ y
g : L → Submodule R M := fun x => ((f x).genEigenspace (μ x)) k
this : ⨅ x, g x ≤ g x ⊓ g y ⊓ g (x + y)
⊢ Disjoint (((f x + f y).genEigenspace (μ x + μ y)) (k + k)) (((f x + f y).genEigenspace (μ (x + y))) k)

Tactic:
exact disjoint_genEigenspace (f x + f y) (Ne.symm contra) _ k

Result:
no goals

Proof state:
R : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : NoZeroSMulDivisors R M
L : Type u_1
F : Type u_2
inst✝² : Add L
inst✝¹ : FunLike F L (End R M)
inst✝ : AddHomClass F L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
h : ∀ (x y : L), Commute (f x) (f y)
x y : L
contra : ¬μ (x + y) = μ x + μ y
g : L → Submodule R M := fun x => ((f x).genEigenspace (μ x)) k
⊢ False

Tactic:
have : ⨅ x, g x ≤ (g x ⊓ g y) ⊓ g (x + y) :=
  le_inf_iff.mpr ⟨le_inf_iff.mpr ⟨iInf_le g x, iInf_le g y⟩, iInf_le g (x + y)⟩

Result:
R : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : NoZeroSMulDivisors R M
L : Type u_1
F : Type u_2
inst✝² : Add L
inst✝¹ : FunLike F L (End R M)
inst✝ : AddHomClass F L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
h : ∀ (x y : L), Commute (f x) (f y)
x y : L
contra : ¬μ (x + y) = μ x + μ y
g : L → Submodule R M := fun x => ((f x).genEigenspace (μ x)) k
this : ⨅ x, g x ≤ g x ⊓ g y ⊓ g (x + y)
⊢ False

Proof state:
R : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : NoZeroSMulDivisors R M
L : Type u_1
F : Type u_2
inst✝² : Add L
inst✝¹ : FunLike F L (End R M)
inst✝ : AddHomClass F L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
h : ∀ (x y : L), Commute (f x) (f y)
x y : L
⊢ μ (x + y) = μ x + μ y

Tactic:
by_contra contra

Result:
R : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : NoZeroSMulDivisors R M
L : Type u_1
F : Type u_2
inst✝² : Add L
inst✝¹ : FunLike F L (End R M)
inst✝ : AddHomClass F L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
h : ∀ (x y : L), Commute (f x) (f y)
x y : L
contra : ¬μ (x + y) = μ x + μ y
⊢ False

Proof state:
R : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : NoZeroSMulDivisors R M
L : Type u_1
F : Type u_2
inst✝² : Add L
inst✝¹ : FunLike F L (End R M)
inst✝ : AddHomClass F L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
h : ∀ (x y : L), Commute (f x) (f y)
x y : L
contra : ¬μ (x + y) = μ x + μ y
g : L → Submodule R M := fun x => ((f x).genEigenspace (μ x)) k
this : ⨅ x, g x ≤ g x ⊓ g y ⊓ g (x + y)
⊢ Disjoint (g x ⊓ g y) (g (x + y))

Tactic:
apply Disjoint.mono_left (genEigenspace_inf_le_add (f x) (f y) (μ x) (μ y) k k (h x y))

Result:
R : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : NoZeroSMulDivisors R M
L : Type u_1
F : Type u_2
inst✝² : Add L
inst✝¹ : FunLike F L (End R M)
inst✝ : AddHomClass F L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
h : ∀ (x y : L), Commute (f x) (f y)
x y : L
contra : ¬μ (x + y) = μ x + μ y
g : L → Submodule R M := fun x => ((f x).genEigenspace (μ x)) k
this : ⨅ x, g x ≤ g x ⊓ g y ⊓ g (x + y)
⊢ Disjoint (((f x + f y).genEigenspace (μ x + μ y)) (k + k)) (g (x + y))

Proof state:
R : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : NoZeroSMulDivisors R M
L : Type u_1
F : Type u_2
inst✝² : Add L
inst✝¹ : FunLike F L (End R M)
inst✝ : AddHomClass F L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
h : ∀ (x y : L), Commute (f x) (f y)
x y : L
contra : ¬μ (x + y) = μ x + μ y
g : L → Submodule R M := fun x => ((f x).genEigenspace (μ x)) k
this : ⨅ x, g x ≤ g x ⊓ g y ⊓ g (x + y)
⊢ Disjoint (((f x + f y).genEigenspace (μ x + μ y)) (k + k)) (g (x + y))

Tactic:
simp only [g, map_add]

Result:
R : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : NoZeroSMulDivisors R M
L : Type u_1
F : Type u_2
inst✝² : Add L
inst✝¹ : FunLike F L (End R M)
inst✝ : AddHomClass F L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
h : ∀ (x y : L), Commute (f x) (f y)
x y : L
contra : ¬μ (x + y) = μ x + μ y
g : L → Submodule R M := fun x => ((f x).genEigenspace (μ x)) k
this : ⨅ x, g x ≤ g x ⊓ g y ⊓ g (x + y)
⊢ Disjoint (((f x + f y).genEigenspace (μ x + μ y)) (k + k)) (((f x + f y).genEigenspace (μ (x + y))) k)

Proof state:
R : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : NoZeroSMulDivisors R M
L : Type u_1
F : Type u_2
inst✝² : Add L
inst✝¹ : FunLike F L (End R M)
inst✝ : AddHomClass F L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
h : ∀ (x y : L), Commute (f x) (f y)
x y : L
contra : ¬μ (x + y) = μ x + μ y
⊢ False

Tactic:
let g : L → Submodule R M := fun x ↦ (f x).genEigenspace (μ x) k

Result:
R : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : NoZeroSMulDivisors R M
L : Type u_1
F : Type u_2
inst✝² : Add L
inst✝¹ : FunLike F L (End R M)
inst✝ : AddHomClass F L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
h : ∀ (x y : L), Commute (f x) (f y)
x y : L
contra : ¬μ (x + y) = μ x + μ y
g : L → Submodule R M := fun x => ((f x).genEigenspace (μ x)) k
⊢ False

Proof state:
R : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : NoZeroSMulDivisors R M
L : Type u_1
F : Type u_2
inst✝² : Add L
inst✝¹ : FunLike F L (End R M)
inst✝ : AddHomClass F L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
h : ∀ (x y : L), Commute (f x) (f y)
x y : L
contra : ¬μ (x + y) = μ x + μ y
g : L → Submodule R M := fun x => ((f x).genEigenspace (μ x)) k
this : ⨅ x, g x ≤ g x ⊓ g y ⊓ g (x + y)
⊢ False

Tactic:
refine h_ne <| eq_bot_iff.mpr (le_trans this (disjoint_iff_inf_le.mp ?_))

Result:
R : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : NoZeroSMulDivisors R M
L : Type u_1
F : Type u_2
inst✝² : Add L
inst✝¹ : FunLike F L (End R M)
inst✝ : AddHomClass F L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
h : ∀ (x y : L), Commute (f x) (f y)
x y : L
contra : ¬μ (x + y) = μ x + μ y
g : L → Submodule R M := fun x => ((f x).genEigenspace (μ x)) k
this : ⨅ x, g x ≤ g x ⊓ g y ⊓ g (x + y)
⊢ Disjoint (g x ⊓ g y) (g (x + y))