-- Mathlib/LinearAlgebra/Eigenspace/Pi.lean
lemma independent_iInf_maxGenEigenspace_of_forall_mapsTo
    (h : ∀ i j φ, MapsTo (f i) ((f j).maxGenEigenspace φ) ((f j).maxGenEigenspace φ)) :
    iSupIndep fun χ : ι → R ↦ ⨅ i, (f i).maxGenEigenspace (χ i)

Proof state:
case insert.intro.intro.intro.intro.intro.intro
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
f : ι → End R M
inst✝ : NoZeroSMulDivisors R M
h : ∀ (l : ι) (χ : ι → R), MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
ih : Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ => ⨅ i, (f i).maxGenEigenspace (χ i))
y : M
hy : y ∈ ⨅ i, (f i).maxGenEigenspace (χ₂ i)
z : M
hz : z ∈ s.sup fun χ => ⨅ i, (f i).maxGenEigenspace (χ i)
hx : y + z ∈ ⨅ i, (f i).maxGenEigenspace (χ₁ i)
hx' : y + z ∈ (⨅ i, (f i).maxGenEigenspace (χ₂ i)) ⊔ s.sup fun χ => ⨅ i, (f i).maxGenEigenspace (χ i)
⊢ y + z ∈ ⨅ i, (f i).maxGenEigenspace (χ₂ i)

Tactic:
clear hx'

Result:
case insert.intro.intro.intro.intro.intro.intro
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
f : ι → End R M
inst✝ : NoZeroSMulDivisors R M
h : ∀ (l : ι) (χ : ι → R), MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
ih : Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ => ⨅ i, (f i).maxGenEigenspace (χ i))
y : M
hy : y ∈ ⨅ i, (f i).maxGenEigenspace (χ₂ i)
z : M
hz : z ∈ s.sup fun χ => ⨅ i, (f i).maxGenEigenspace (χ i)
hx : y + z ∈ ⨅ i, (f i).maxGenEigenspace (χ₁ i)
⊢ y + z ∈ ⨅ i, (f i).maxGenEigenspace (χ₂ i)

Proof state:
case insert.intro
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
f : ι → End R M
inst✝ : NoZeroSMulDivisors R M
h : ∀ (l : ι) (χ : ι → R), MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
ih : Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ => ⨅ i, (f i).maxGenEigenspace (χ i))
⊢ ∀
    x ∈
      (⨅ i, (f i).maxGenEigenspace (χ₁ i)) ⊓
        ((⨅ i, (f i).maxGenEigenspace (χ₂ i)) ⊔ s.sup fun χ => ⨅ i, (f i).maxGenEigenspace (χ i)),
    x = 0

Tactic:
rintro x ⟨hx, hx'⟩

Result:
case insert.intro.intro
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
f : ι → End R M
inst✝ : NoZeroSMulDivisors R M
h : ∀ (l : ι) (χ : ι → R), MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
ih : Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ => ⨅ i, (f i).maxGenEigenspace (χ i))
x : M
hx : x ∈ ↑(⨅ i, (f i).maxGenEigenspace (χ₁ i))
hx' : x ∈ ↑((⨅ i, (f i).maxGenEigenspace (χ₂ i)) ⊔ s.sup fun χ => ⨅ i, (f i).maxGenEigenspace (χ i))
⊢ x = 0

Proof state:
case insert.intro.intro
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
f : ι → End R M
inst✝ : NoZeroSMulDivisors R M
h : ∀ (l : ι) (χ : ι → R), MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
ih : Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ => ⨅ i, (f i).maxGenEigenspace (χ i))
x : M
hx : x ∈ ↑(⨅ i, (f i).maxGenEigenspace (χ₁ i))
hx' : x ∈ ↑((⨅ i, (f i).maxGenEigenspace (χ₂ i)) ⊔ s.sup fun χ => ⨅ i, (f i).maxGenEigenspace (χ i))
⊢ x = 0

Tactic:
simp only [SetLike.mem_coe] at hx hx'

Result:
case insert.intro.intro
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
f : ι → End R M
inst✝ : NoZeroSMulDivisors R M
h : ∀ (l : ι) (χ : ι → R), MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
ih : Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ => ⨅ i, (f i).maxGenEigenspace (χ i))
x : M
hx : x ∈ ⨅ i, (f i).maxGenEigenspace (χ₁ i)
hx' : x ∈ (⨅ i, (f i).maxGenEigenspace (χ₂ i)) ⊔ s.sup fun χ => ⨅ i, (f i).maxGenEigenspace (χ i)
⊢ x = 0

Proof state:
case insert
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
f : ι → End R M
inst✝ : NoZeroSMulDivisors R M
h : ∀ (l : ι) (χ : ι → R), MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
ih : χ₁ ∉ s → Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ => ⨅ i, (f i).maxGenEigenspace (χ i))
hχ₁₂ : χ₁ ∉ insert χ₂ s
⊢ Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) ((insert χ₂ s).sup fun χ => ⨅ i, (f i).maxGenEigenspace (χ i))

Tactic:
obtain ⟨hχ₁₂ : χ₁ ≠ χ₂, hχ₁ : χ₁ ∉ s⟩ := by rwa [Finset.mem_insert, not_or] at hχ₁₂

Result:
case insert.intro
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
f : ι → End R M
inst✝ : NoZeroSMulDivisors R M
h : ∀ (l : ι) (χ : ι → R), MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
ih : χ₁ ∉ s → Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ => ⨅ i, (f i).maxGenEigenspace (χ i))
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
⊢ Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) ((insert χ₂ s).sup fun χ => ⨅ i, (f i).maxGenEigenspace (χ i))

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
f : ι → End R M
inst✝ : NoZeroSMulDivisors R M
h : ∀ (i j : ι) (φ : R), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)
l : ι
χ : ι → R
⊢ MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))

Tactic:
intro x hx

Result:
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
f : ι → End R M
inst✝ : NoZeroSMulDivisors R M
h : ∀ (i j : ι) (φ : R), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)
l : ι
χ : ι → R
x : M
hx : x ∈ ⨅ i, ↑((f i).maxGenEigenspace (χ i))
⊢ (f l) x ∈ ⨅ i, ↑((f i).maxGenEigenspace (χ i))