awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
μ : ι → R
i : ι
h :
  ∀ (j : ι),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace (μ i)) : Set M) (↑((f i).maxGenEigenspace (μ i)) : Set M)
this : Nonempty ι
⊢ let p := (f i).maxGenEigenspace (μ i);
  ∀ (j : ι), MapsTo (⇑(f j) : (a : M) → M) (↑p : Set M) (↑p : Set M)

Tactic:
set p := (f i).maxGenEigenspace (μ i)

Premises used: Module.End.maxGenEigenspace
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
μ : ι → R
i : ι
h_1 :
  ∀ (j : ι),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace (μ i)) : Set M) (↑((f i).maxGenEigenspace (μ i)) : Set M)
this : Nonempty ι
p : Submodule R M := (f i).maxGenEigenspace (μ i)
h : ∀ (j : ι), MapsTo (⇑(f j) : (a : M) → M) (↑p : Set M) (↑p : Set M)
⊢ ⨅ (j : ι), (f j).maxGenEigenspace (μ j) = p ⊓ ⨅ (j : ι), (f j).maxGenEigenspace (μ j)

Tactic:
le_antisymm ?_ inf_le_right

Premises used: inf_le_right, le_antisymm
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
μ : ι → R
i : ι
h_1 :
  ∀ (j : ι),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace (μ i)) : Set M) (↑((f i).maxGenEigenspace (μ i)) : Set M)
this : Nonempty ι
p : Submodule R M := (f i).maxGenEigenspace (μ i)
h : ∀ (j : ι), MapsTo (⇑(f j) : (a : M) → M) (↑p : Set M) (↑p : Set M)
refine : ⨅ (j : ι), (f j).maxGenEigenspace (μ j) ≤ p ⊓ ⨅ (j : ι), (f j).maxGenEigenspace (μ j)
⊢ ⨅ (j : ι), (f j).maxGenEigenspace (μ j) = p ⊓ ⨅ (j : ι), (f j).maxGenEigenspace (μ j)

Tactic:
refine le_antisymm ?_ inf_le_right

Premises used: inf_le_right, le_antisymm
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
μ : ι → R
i : ι
h_1 :
  ∀ (j : ι),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace (μ i)) : Set M) (↑((f i).maxGenEigenspace (μ i)) : Set M)
this : Nonempty ι
p : Submodule R M := (f i).maxGenEigenspace (μ i)
h : ∀ (j : ι), MapsTo (⇑(f j) : (a : M) → M) (↑p : Set M) (↑p : Set M)
⊢ ⨅ (j : ι), (f j).maxGenEigenspace (μ j) ≤ p ⊓ ⨅ (j : ι), (f j).maxGenEigenspace (μ j)

Tactic:
simpa only [le_inf_iff, le_refl, and_true] using iInf_le _ _

Premises used: le_refl, and_true, le_inf_iff, iInf_le
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
μ : ι → R
i : ι
h_1 :
  ∀ (j : ι),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace (μ i)) : Set M) (↑((f i).maxGenEigenspace (μ i)) : Set M)
this : Nonempty ι
p : Submodule R M := (f i).maxGenEigenspace (μ i)
h : ∀ (j : ι), MapsTo (⇑(f j) : (a : M) → M) (↑p : Set M) (↑p : Set M)
⊢ ⨅ (j : ι), (f j).maxGenEigenspace (μ j) = p ⊓ ⨅ (j : ι), (f j).maxGenEigenspace (μ j)

Tactic:
have : ⨅ j, (f j).maxGenEigenspace (μ j) = p ⊓ ⨅ j, (f j).maxGenEigenspace (μ j) := by
    refine le_antisymm ?_ inf_le_right
    simpa only [le_inf_iff, le_refl, and_true] using iInf_le _ _
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
μ : ι → R
i : ι
h_1 :
  ∀ (j : ι),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace (μ i)) : Set M) (↑((f i).maxGenEigenspace (μ i)) : Set M)
this_1 : Nonempty ι
p : Submodule R M := (f i).maxGenEigenspace (μ i)
h : ∀ (j : ι), MapsTo (⇑(f j) : (a : M) → M) (↑p : Set M) (↑p : Set M)
this : ⨅ (j : ι), (f j).maxGenEigenspace (μ j) = p ⊓ ⨅ (j : ι), (f j).maxGenEigenspace (μ j)
rw :
  Eq.{u_4 + 1} (α := Submodule R M)
    (⨅ (i_1 : ι), Submodule.map p.subtype (maxGenEigenspace (LinearMap.restrict (f i_1) ⋯) (μ i_1)))
    (⨅ (i : ι), p ⊓ (f i).maxGenEigenspace (μ i))
⊢ Submodule.map ((f i).maxGenEigenspace (μ i)).subtype
      (⨅ (j : ι), (fun (j : ι) ↦ maxGenEigenspace (LinearMap.restrict (f j) ⋯) (μ j)) j) =
    ⨅ (j : ι), (f j).maxGenEigenspace (μ j)

Tactic:
rw [Submodule.map_iInf _ p.injective_subtype, this, Submodule.inf_iInf]

Premises used: Submodule.inf_iInf, Submodule.map_iInf, Submodule.injective_subtype
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
μ : ι → R
i : ι
h_1 :
  ∀ (j : ι),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace (μ i)) : Set M) (↑((f i).maxGenEigenspace (μ i)) : Set M)
this_1 : Nonempty ι
p : Submodule R M := (f i).maxGenEigenspace (μ i)
h : ∀ (j : ι), MapsTo (⇑(f j) : (a : M) → M) (↑p : Set M) (↑p : Set M)
this : ⨅ (j : ι), (f j).maxGenEigenspace (μ j) = p ⊓ ⨅ (j : ι), (f j).maxGenEigenspace (μ j)
enter : fun (i : ι) ↦ p ⊓ (f i).maxGenEigenspace (μ i)
| ⨅ (i : ι), p ⊓ (f i).maxGenEigenspace (μ i)

Tactic:
enter [1]
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
μ : ι → R
i : ι
h_1 :
  ∀ (j : ι),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace (μ i)) : Set M) (↑((f i).maxGenEigenspace (μ i)) : Set M)
this_1 : Nonempty ι
p : Submodule R M := (f i).maxGenEigenspace (μ i)
h : ∀ (j : ι), MapsTo (⇑(f j) : (a : M) → M) (↑p : Set M) (↑p : Set M)
this : ⨅ (j : ι), (f j).maxGenEigenspace (μ j) = p ⊓ ⨅ (j : ι), (f j).maxGenEigenspace (μ j)
h₁ : ∀ (x : ι), p ⊓ (f x).maxGenEigenspace (μ x)
| fun (i : ι) ↦ p ⊓ (f i).maxGenEigenspace (μ i)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
μ : ι → R
i : ι
h_1 :
  ∀ (j : ι),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace (μ i)) : Set M) (↑((f i).maxGenEigenspace (μ i)) : Set M)
this_1 : Nonempty ι
p : Submodule R M := (f i).maxGenEigenspace (μ i)
h : ∀ (j : ι), MapsTo (⇑(f j) : (a : M) → M) (↑p : Set M) (↑p : Set M)
this : ⨅ (j : ι), (f j).maxGenEigenspace (μ j) = p ⊓ ⨅ (j : ι), (f j).maxGenEigenspace (μ j)
x : ι
h₁ : Submodule.map p.subtype ((genEigenspace (LinearMap.restrict (f x) ⋯) (μ x) : (a : ℕ∞) → Submodule R ↥p) ⊤)
| p ⊓ (f x).maxGenEigenspace (μ x)

Tactic:
rw [p.inf_genEigenspace (f _) (h _)]

Premises used: Submodule.inf_genEigenspace
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
μ : ι → R
i : ι
h_1 :
  ∀ (j : ι),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace (μ i)) : Set M) (↑((f i).maxGenEigenspace (μ i)) : Set M)
this_1 : Nonempty ι
p : Submodule R M := (f i).maxGenEigenspace (μ i)
h : ∀ (j : ι), MapsTo (⇑(f j) : (a : M) → M) (↑p : Set M) (↑p : Set M)
this : ⨅ (j : ι), (f j).maxGenEigenspace (μ j) = p ⊓ ⨅ (j : ι), (f j).maxGenEigenspace (μ j)
h₁ :
  ∀ (x : ι), Submodule.map p.subtype ((genEigenspace (LinearMap.restrict (f x) ⋯) (μ x) : (a : ℕ∞) → Submodule R ↥p) ⊤)
| ⨅ (i : ι), p ⊓ (f i).maxGenEigenspace (μ i)

Tactic:
enter [1]
    ext
    rw [p.inf_genEigenspace (f _) (h _)]

Premises used: Submodule.inf_genEigenspace
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
μ : ι → R
i : ι
h_1 :
  ∀ (j : ι),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace (μ i)) : Set M) (↑((f i).maxGenEigenspace (μ i)) : Set M)
this_1 : Nonempty ι
p : Submodule R M := (f i).maxGenEigenspace (μ i)
h : ∀ (j : ι), MapsTo (⇑(f j) : (a : M) → M) (↑p : Set M) (↑p : Set M)
this : ⨅ (j : ι), (f j).maxGenEigenspace (μ j) = p ⊓ ⨅ (j : ι), (f j).maxGenEigenspace (μ j)
conv_rhs :
  Eq.{u_4 + 1} (α := Submodule R M)
    (⨅ (i_1 : ι), Submodule.map p.subtype (maxGenEigenspace (LinearMap.restrict (f i_1) ⋯) (μ i_1)))
    (⨅ (i : ι), p ⊓ (f i).maxGenEigenspace (μ i))
conv_rhs₁ :
  Eq.{u_4 + 1} (α := Submodule R M)
    (⨅ (i_1 : ι), Submodule.map p.subtype (maxGenEigenspace (LinearMap.restrict (f i_1) ⋯) (μ i_1)))
    (⨅ (x : ι),
      Submodule.map p.subtype ((genEigenspace (LinearMap.restrict (f x) ⋯) (μ x) : (a : ℕ∞) → Submodule R ↥p) ⊤))
⊢ Eq.{u_4 + 1} (α := Submodule R M)
    (⨅ (i_1 : ι), Submodule.map p.subtype (maxGenEigenspace (LinearMap.restrict (f i_1) ⋯) (μ i_1)))
    (⨅ (i : ι), p ⊓ (f i).maxGenEigenspace (μ i))

Tactic:
conv_rhs =>
    enter [1]
    ext
    rw [p.inf_genEigenspace (f _) (h _)]

Premises used: Submodule.inf_genEigenspace
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
χ₁ χ₂ : ι → R
h : χ₁ ≠ χ₂
⊢ ∃ (j : ι), χ₁ j ≠ χ₂ j

Tactic:
Function.ne_iff.mp h

Premises used: Function.ne_iff, Iff.mp
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
χ₁ χ₂ : ι → R
h : χ₁ ≠ χ₂
obtain :
  ∀ (j : ι) (hj : χ₁ j ≠ χ₂ j),
    Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
      (⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i))
⊢ Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
    (⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i))

Tactic:
obtain ⟨j, hj⟩ : ∃ j, χ₁ j ≠ χ₂ j := Function.ne_iff.mp h

Premises used: Function.ne_iff, Iff.mp
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
χ₁ χ₂ : ι → R
h : χ₁ ≠ χ₂
j : ι
hj : χ₁ j ≠ χ₂ j
⊢ Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
    (⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i))

Tactic:
(End.disjoint_genEigenspace (f j) hj ⊤ ⊤).mono (iInf_le _ j) (iInf_le _ j)

Premises used: Module.End.disjoint_genEigenspace, Disjoint.mono, Top.top, iInf_le
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
χ₁ χ₂ : ι → R
h : χ₁ ≠ χ₂
j : ι
hj : χ₁ j ≠ χ₂ j
⊢ Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
    (⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i))

Tactic:
exact (End.disjoint_genEigenspace (f j) hj ⊤ ⊤).mono (iInf_le _ j) (iInf_le _ j)

Premises used: Disjoint.mono, iInf_le
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
χ₁ : ι → R
h :
  Membership.mem (γ := Set (ι → R))
    {χ : ι → R | Ne.{u_4 + 1} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊥} χ₁
χ₂ : ι → R
hχ₂ :
  Membership.mem (γ := Set (ι → R))
    {χ : ι → R | Ne.{u_4 + 1} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊥} χ₂
hχ₁₂ :
  Eq.{u_4 + 1} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
    (⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i))
contrapose! :
  ∀ (hχ₂ : χ₁ ≠ χ₂), χ₂ ∉ {χ : ι → R | Ne.{u_4 + 1} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊥}
⊢ χ₁ = χ₂

Tactic:
contrapose! hχ₂
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
χ₁ : ι → R
h :
  Membership.mem (γ := Set (ι → R))
    {χ : ι → R | Ne.{u_4 + 1} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊥} χ₁
χ₂ : ι → R
hχ₁₂ :
  Eq.{u_4 + 1} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
    (⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i))
hχ₂ : χ₁ ≠ χ₂
⊢ χ₂ ∉ {χ : ι → R | Ne.{u_4 + 1} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊥}

Tactic:
simpa [hχ₁₂] using disjoint_iInf_maxGenEigenspace f hχ₂

Premises used: Module.End.disjoint_iInf_maxGenEigenspace
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
h :
  ∀ (i j : ι) (φ : R),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
l : ι
χ : ι → R
x : M
hx : Membership.mem (γ := Set M) (⨅ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M)) x
simp :
  ∀ (hx : ∀ (i : ι), x ∈ (f i).maxGenEigenspace (χ i)) (i : ι),
    Membership.mem (α := M) ((f i).maxGenEigenspace (χ i)) ((f l : (a : M) → M) x : M)
⊢ Membership.mem (α := M) (γ := Set M) (⨅ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M))
    ((f l : (a : M) → M) x : M)

Tactic:
simp only [iInf_eq_iInter, mem_iInter, SetLike.mem_coe] at hx ⊢

Premises used: Set.iInf_eq_iInter, Set.mem_iInter, SetLike.mem_coe
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
h :
  ∀ (i j : ι) (φ : R),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
l : ι
χ : ι → R
x : M
hx : ∀ (i : ι), x ∈ (f i).maxGenEigenspace (χ i)
⊢ ∀ (i : ι), Membership.mem (α := M) ((f i).maxGenEigenspace (χ i)) ((f l : (a : M) → M) x : M)

Tactic:
fun i ↦ h l i (χ i) (hx i)
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
h :
  ∀ (i j : ι) (φ : R),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
l : ι
χ : ι → R
x : M
hx : ∀ (i : ι), x ∈ (f i).maxGenEigenspace (χ i)
⊢ ∀ (i : ι), Membership.mem (α := M) ((f i).maxGenEigenspace (χ i)) ((f l : (a : M) → M) x : M)

Tactic:
exact fun i ↦ h l i (χ i) (hx i)
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
h :
  ∀ (i j : ι) (φ : R),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
⊢ ∀ (l : ι) (χ : ι → R),
    MapsTo (α := M) (β := M) (⇑(f l) : (a : M) → M) (⨅ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M))
      (⨅ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M))

Tactic:
replace h (l : ι) (χ : ι → R) :
      MapsTo (f l) (⨅ i, (f i).maxGenEigenspace (χ i)) (⨅ i, (f i).maxGenEigenspace (χ i)) := by
    intro x hx
    simp only [iInf_eq_iInter, mem_iInter, SetLike.mem_coe] at hx ⊢
    exact fun i ↦ h l i (χ i) (hx i)
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
h :
  ∀ (l : ι) (χ : ι → R),
    MapsTo (α := M) (β := M) (⇑(f l) : (a : M) → M) (⨅ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M))
      (⨅ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M))
this :
  ∀ (χ : ι → R) (s : Finset (ι → R)),
    χ ∉ s →
      Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ i))
        (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
⊢ iSupIndep (α := Submodule R M) fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)

Tactic:
simpa only [iSupIndep_iff_supIndep,
      Finset.supIndep_iff_disjoint_erase] using fun s χ _ ↦ this _ _ (s.notMem_erase χ)

Premises used: Finset.supIndep_iff_disjoint_erase, iSupIndep_iff_supIndep
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
h :
  ∀ (l : ι) (χ : ι → R),
    MapsTo (α := M) (β := M) (⇑(f l) : (a : M) → M) (⨅ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M))
      (⨅ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M))
suffices :
  ∀ (χ : ι → R) (s : Finset (ι → R)),
    χ ∉ s →
      Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ i))
        (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
⊢ iSupIndep (α := Submodule R M) fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)

Tactic:
suffices ∀ χ (s : Finset (ι → R)) (_ : χ ∉ s),
      Disjoint (⨅ i, (f i).maxGenEigenspace (χ i))
        (s.sup fun (χ : ι → R) ↦ ⨅ i, (f i).maxGenEigenspace (χ i)) by
    simpa only [iSupIndep_iff_supIndep,
      Finset.supIndep_iff_disjoint_erase] using fun s χ _ ↦ this _ _ (s.notMem_erase χ)
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
h :
  ∀ (l : ι) (χ : ι → R),
    MapsTo (α := M) (β := M) (⇑(f l) : (a : M) → M) (⨅ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M))
      (⨅ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M))
χ₁ : ι → R
⊢ χ₁ ∉ ∅ →
    Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
      (Finset.sup ∅ fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
h :
  ∀ (l : ι) (χ : ι → R),
    MapsTo (α := M) (β := M) (⇑(f l) : (a : M) → M) (⨅ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M))
      (⨅ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
ih :
  χ₁ ∉ s →
    Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
      (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
hχ₁₂ : χ₁ ∉ insert χ₂ s
rwa : ∀ (hχ₁₂ : ¬(χ₁ = χ₂ ∨ χ₁ ∈ s)), ¬χ₁ = χ₂ ∧ χ₁ ∉ s
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hχ₁₂ : ¬χ₁ = χ₂ ∧ χ₁ ∉ s), ¬χ₁ = χ₂ ∧ χ₁ ∉ s
⊢ ¬χ₁ = χ₂ ∧ χ₁ ∉ s

Tactic:
rwa [Finset.mem_insert, not_or] at hχ₁₂

Premises used: Finset.mem_insert, not_or
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
h :
  ∀ (l : ι) (χ : ι → R),
    MapsTo (α := M) (β := M) (⇑(f l) : (a : M) → M) (⨅ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M))
      (⨅ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
ih :
  χ₁ ∉ s →
    Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
      (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
hχ₁₂ : χ₁ ∉ insert χ₂ s
⊢ χ₁ ≠ χ₂

Tactic:
obtain ⟨hχ₁₂ : χ₁ ≠ χ₂, hχ₁ : χ₁ ∉ s⟩ := by rwa [Finset.mem_insert, not_or] at hχ₁₂
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
h :
  ∀ (l : ι) (χ : ι → R),
    MapsTo (α := M) (β := M) (⇑(f l) : (a : M) → M) (⨅ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M))
      (⨅ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
ih :
  χ₁ ∉ s →
    Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
      (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
hχ₁₂ : χ₁ ∉ insert χ₂ s
hχ₁₃ : χ₁ ≠ χ₂
⊢ χ₁ ∉ s

Tactic:
obtain ⟨hχ₁₂ : χ₁ ≠ χ₂, hχ₁ : χ₁ ∉ s⟩ := by rwa [Finset.mem_insert, not_or] at hχ₁₂
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
h :
  ∀ (l : ι) (χ : ι → R),
    MapsTo (α := M) (β := M) (⇑(f l) : (a : M) → M) (⨅ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M))
      (⨅ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
ih :
  χ₁ ∉ s →
    Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
      (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
hχ₁₂_1 : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
⊢ Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
    (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))

Tactic:
specialize ih hχ₁
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
h :
  ∀ (l : ι) (χ : ι → R),
    MapsTo (α := M) (β := M) (⇑(f l) : (a : M) → M) (⨅ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M))
      (⨅ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
hχ₁₂_1 : χ₁ ∉ Insert.insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
ih :
  Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
    (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
insert :
  ∀ (x : M),
    Membership.mem (γ := Submodule R M)
        ((⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i)) ⊓
          ((⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i)) ⊔
            s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)))
        x →
      x = 0
⊢ Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
    ((Insert.insert χ₂ s).sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))

Tactic:
rw [Finset.sup_insert, disjoint_iff, Submodule.eq_bot_iff]

Premises used: Finset.sup_insert, disjoint_iff, Submodule.eq_bot_iff
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
h :
  ∀ (l : ι) (χ : ι → R),
    MapsTo (α := M) (β := M) (⇑(f l) : (a : M) → M) (⨅ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M))
      (⨅ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
hχ₁₂_1 : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
ih :
  Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
    (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
x : M
hx : x ∈ (↑(⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i)) : Set M)
hx' :
  x ∈
    (↑((⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i)) ⊔ s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) :
      Set M)
⊢ Membership.mem (γ := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i)) x

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

Premises used: SetLike.mem_coe