-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
lemma map_smul_of_iInf_genEigenspace_ne_bot [NoZeroSMulDivisors R M]
    {L F : Type*} [SMul R L] [FunLike F L (End R M)] [MulActionHomClass F R L (End R M)] (f : F)
    (μ : L → R) (k : ℕ∞) (h_ne : ⨅ x, (f x).genEigenspace (μ x) k ≠ ⊥)
    (t : R) (x : L) :
    μ (t • x) = t • μ x

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✝² : SMul R L
inst✝¹ : FunLike F L (End R M)
inst✝ : MulActionHomClass F R L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
t : R
x : L
⊢ μ (t • x) = t • μ x

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✝² : SMul R L
inst✝¹ : FunLike F L (End R M)
inst✝ : MulActionHomClass F R L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
t : R
x : L
contra : ¬μ (t • x) = t • μ x
⊢ 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✝² : SMul R L
inst✝¹ : FunLike F L (End R M)
inst✝ : MulActionHomClass F R L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
t : R
x : L
contra : ¬μ (t • x) = t • μ x
g : L → Submodule R M := fun x => ((f x).genEigenspace (μ x)) k
this : ⨅ x, g x ≤ g x ⊓ g (t • x)
⊢ Disjoint (g x) (g (t • x))

Tactic:
apply Disjoint.mono_left (genEigenspace_le_smul (f x) (μ x) t 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✝² : SMul R L
inst✝¹ : FunLike F L (End R M)
inst✝ : MulActionHomClass F R L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
t : R
x : L
contra : ¬μ (t • x) = t • μ x
g : L → Submodule R M := fun x => ((f x).genEigenspace (μ x)) k
this : ⨅ x, g x ≤ g x ⊓ g (t • x)
⊢ Disjoint (((t • f x).genEigenspace (t * μ x)) k) (g (t • x))

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✝² : SMul R L
inst✝¹ : FunLike F L (End R M)
inst✝ : MulActionHomClass F R L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
t : R
x : L
contra : ¬μ (t • x) = t • μ x
g : L → Submodule R M := fun x => ((f x).genEigenspace (μ x)) k
⊢ False

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

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✝² : SMul R L
inst✝¹ : FunLike F L (End R M)
inst✝ : MulActionHomClass F R L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
t : R
x : L
contra : ¬μ (t • x) = t • μ x
g : L → Submodule R M := fun x => ((f x).genEigenspace (μ x)) k
this : ⨅ x, g x ≤ g x ⊓ g (t • x)
⊢ 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✝² : SMul R L
inst✝¹ : FunLike F L (End R M)
inst✝ : MulActionHomClass F R L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
t : R
x : L
contra : ¬μ (t • x) = t • μ x
g : L → Submodule R M := fun x => ((f x).genEigenspace (μ x)) k
this : ⨅ x, g x ≤ g x ⊓ g (t • x)
⊢ Disjoint (((t • f x).genEigenspace (t * μ x)) k) (g (t • x))

Tactic:
simp only [g, map_smul]

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✝² : SMul R L
inst✝¹ : FunLike F L (End R M)
inst✝ : MulActionHomClass F R L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
t : R
x : L
contra : ¬μ (t • x) = t • μ x
g : L → Submodule R M := fun x => ((f x).genEigenspace (μ x)) k
this : ⨅ x, g x ≤ g x ⊓ g (t • x)
⊢ Disjoint (((t • f x).genEigenspace (t * μ x)) k) (((t • f x).genEigenspace (μ (t • x))) 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✝² : SMul R L
inst✝¹ : FunLike F L (End R M)
inst✝ : MulActionHomClass F R L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
t : R
x : L
contra : ¬μ (t • x) = t • μ x
⊢ 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✝² : SMul R L
inst✝¹ : FunLike F L (End R M)
inst✝ : MulActionHomClass F R L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
t : R
x : L
contra : ¬μ (t • x) = t • μ x
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✝² : SMul R L
inst✝¹ : FunLike F L (End R M)
inst✝ : MulActionHomClass F R L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
t : R
x : L
contra : ¬μ (t • x) = t • μ x
g : L → Submodule R M := fun x => ((f x).genEigenspace (μ x)) k
this : ⨅ x, g x ≤ g x ⊓ g (t • x)
⊢ 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✝² : SMul R L
inst✝¹ : FunLike F L (End R M)
inst✝ : MulActionHomClass F R L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
t : R
x : L
contra : ¬μ (t • x) = t • μ x
g : L → Submodule R M := fun x => ((f x).genEigenspace (μ x)) k
this : ⨅ x, g x ≤ g x ⊓ g (t • x)
⊢ Disjoint (g x) (g (t • x))

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✝² : SMul R L
inst✝¹ : FunLike F L (End R M)
inst✝ : MulActionHomClass F R L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
t : R
x : L
contra : ¬μ (t • x) = t • μ x
g : L → Submodule R M := fun x => ((f x).genEigenspace (μ x)) k
this : ⨅ x, g x ≤ g x ⊓ g (t • x)
⊢ Disjoint (((t • f x).genEigenspace (t * μ x)) k) (((t • f x).genEigenspace (μ (t • x))) k)

Tactic:
exact disjoint_genEigenspace (t • f x) (Ne.symm contra) k k

Result:
no goals