awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
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)
empty :
  χ₁ ∉ ∅ →
    Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
      (Finset.sup ∅ fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
⊢ χ₁ ∉ s →
    Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
      (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
have insert : ∀ (χ₂ : ι → 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))),
  χ₁ ∉ insert χ₂ s →
    Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
      ((insert χ₂ s).sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert χ₂ s _n ih =>
  intro hχ₁₂
  obtain ⟨hχ₁₂ : χ₁ ≠ χ₂, hχ₁ : χ₁ ∉ s⟩ := by rwa [Finset.mem_insert, not_or] at hχ₁₂
  specialize ih hχ₁
  rw [Finset.sup_insert, disjoint_iff, Submodule.eq_bot_iff]
  rintro x ⟨hx, hx'⟩
  simp only [SetLike.mem_coe] at hx hx'
  suffices x ∈ ⨅ i, (f i).maxGenEigenspace (χ₂ i) by
    rw [← Submodule.mem_bot (R := R), ← (disjoint_iInf_maxGenEigenspace f hχ₁₂).eq_bot]
    exact ⟨hx, this⟩
  obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.mem_sup.mp hx'; clear hx'
  suffices ∀ l, ∃ (k : ℕ),
      ((f l - algebraMap R (Module.End R M) (χ₂ l)) ^ k) (y + z) ∈
      (⨅ i, (f i).maxGenEigenspace (χ₁ i)) ⊓
        Finset.sup s fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i) by
    simpa [ih.eq_bot, Submodule.mem_bot] using this
  intro l
  let g : Module.End R M := f l - algebraMap R (Module.End R M) (χ₂ l)
  obtain ⟨k, hk : (g ^ k) y = 0⟩ := (mem_iInf_maxGenEigenspace_iff _ _ _).mp hy l
  have aux (f : End R M) (φ : R) (k : ℕ) (p : Submodule R M) (hp : MapsTo f p p) :
      MapsTo ((f - algebraMap R (Module.End R M) φ) ^ k) p p := by
    rw [Module.End.coe_pow]
    exact MapsTo.iterate (fun m hm ↦ p.sub_mem (hp hm) (p.smul_mem _ hm)) k
  refine ⟨k, Submodule.mem_inf.mp ⟨?_, ?_⟩⟩
  · refine aux (f l) (χ₂ l) k (⨅ i, (f i).maxGenEigenspace (χ₁ i)) ?_ hx
    simp only [Submodule.coe_iInf]
    exact h l χ₁
  · rw [map_add, hk, zero_add]
    suffices (s.sup fun χ ↦ (⨅ i, (f i).maxGenEigenspace (χ i))).map (g ^ k) ≤
        s.sup fun χ ↦ (⨅ i, (f i).maxGenEigenspace (χ i)) from
      this (Submodule.mem_map_of_mem hz)
    simp_rw [Finset.sup_eq_iSup, Submodule.map_iSup (ι := ι → R), Submodule.map_iSup (ι := _ ∈ s)]
    refine iSup₂_mono fun χ _ ↦ ?_
    rintro - ⟨u, hu, rfl⟩
    refine aux (f l) (χ₂ l) k (⨅ i, (f i).maxGenEigenspace (χ i)) ?_ hu
    simp only [Submodule.coe_iInf]
    exact h l χ
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
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))
⊢ iSupIndep (α := Submodule R M) fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)
have 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))
Tactic: classical
  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 χ)
  intro χ₁ s
  induction s using Finset.induction_on with
  | empty => simp
  | insert χ₂ s _n ih =>
  intro hχ₁₂
  obtain ⟨hχ₁₂ : χ₁ ≠ χ₂, hχ₁ : χ₁ ∉ s⟩ := by rwa [Finset.mem_insert, not_or] at hχ₁₂
  specialize ih hχ₁
  rw [Finset.sup_insert, disjoint_iff, Submodule.eq_bot_iff]
  rintro x ⟨hx, hx'⟩
  simp only [SetLike.mem_coe] at hx hx'
  suffices x ∈ ⨅ i, (f i).maxGenEigenspace (χ₂ i) by
    rw [← Submodule.mem_bot (R := R), ← (disjoint_iInf_maxGenEigenspace f hχ₁₂).eq_bot]
    exact ⟨hx, this⟩
  obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.mem_sup.mp hx'; clear hx'
  suffices ∀ l, ∃ (k : ℕ),
      ((f l - algebraMap R (Module.End R M) (χ₂ l)) ^ k) (y + z) ∈
      (⨅ i, (f i).maxGenEigenspace (χ₁ i)) ⊓
        Finset.sup s fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i) by
    simpa [ih.eq_bot, Submodule.mem_bot] using this
  intro l
  let g : Module.End R M := f l - algebraMap R (Module.End R M) (χ₂ l)
  obtain ⟨k, hk : (g ^ k) y = 0⟩ := (mem_iInf_maxGenEigenspace_iff _ _ _).mp hy l
  have aux (f : End R M) (φ : R) (k : ℕ) (p : Submodule R M) (hp : MapsTo f p p) :
      MapsTo ((f - algebraMap R (Module.End R M) φ) ^ k) p p := by
    rw [Module.End.coe_pow]
    exact MapsTo.iterate (fun m hm ↦ p.sub_mem (hp hm) (p.smul_mem _ hm)) k
  refine ⟨k, Submodule.mem_inf.mp ⟨?_, ?_⟩⟩
  · refine aux (f l) (χ₂ l) k (⨅ i, (f i).maxGenEigenspace (χ₁ i)) ?_ hx
    simp only [Submodule.coe_iInf]
    exact h l χ₁
  · rw [map_add, hk, zero_add]
    suffices (s.sup fun χ ↦ (⨅ i, (f i).maxGenEigenspace (χ i))).map (g ^ k) ≤
        s.sup fun χ ↦ (⨅ i, (f i).maxGenEigenspace (χ i)) from
      this (Submodule.mem_map_of_mem hz)
    simp_rw [Finset.sup_eq_iSup, Submodule.map_iSup (ι := ι → R), Submodule.map_iSup (ι := _ ∈ s)]
    refine iSup₂_mono fun χ _ ↦ ?_
    rintro - ⟨u, hu, rfl⟩
    refine aux (f l) (χ₂ l) k (⨅ i, (f i).maxGenEigenspace (χ i)) ?_ hu
    simp only [Submodule.coe_iInf]
    exact h l χ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
Goal:
ι : Type u_1
K : Type u_3
M : Type u_4
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
⊢ Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
have generalize : ∀ (n : ℕ) (h_dim : finrank K M = n),
  Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
Tactic: generalize h_dim : finrank K M = n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
Goal:
ι : Type u_1
K : Type u_3
M : Type u_4
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
n : ℕ
h_dim : finrank K M = n
⊢ Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
have ind : ∀ (n : ℕ)
  (ih :
    ∀ m < n,
      ∀ {M : Type u_4} [inst_4 : AddCommGroup M] [inst_5 : Module K M] [FiniteDimensional K M] (f : ι → End K M)
        (h :
          ∀ (i j : ι) (φ : K),
            MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M))
        (h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤)
        (h_dim : finrank K M = m),
        Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤)
  {M : Type u_4} [inst_4 : AddCommGroup M] [inst_5 : Module K M] [FiniteDimensional K M] (f : ι → End K M)
  (h :
    ∀ (i j : ι) (φ : K),
      MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M))
  (h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤) (h_dim : finrank K M = n),
  Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
Tactic: induction n using Nat.strongRecOn generalizing M with | ind n ih => ?_
Cleared hypotheses: M, inst_1, inst_2, inst_3, f, h, h', n, h_dim
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst_4 : AddCommGroup M] [inst_5 : Module K M] [FiniteDimensional K M] (f : ι → End K M)
      (h :
        ∀ (i j : ι) (φ : K),
          MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M))
      (h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤)
      (h_dim : finrank K M = m),
      Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
⊢ Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
have ind : ∀ (this : ∀ (a : ι), ∃ (φ : K), (f a).maxGenEigenspace φ = ⊤),
  Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
Tactic: obtain this | ⟨i : ι, hy : ¬ ∃ φ, (f i).maxGenEigenspace φ = ⊤⟩ :=
    forall_or_exists_not (fun j : ι ↦ ∃ φ : K, (f j).maxGenEigenspace φ = ⊤)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst_4 : AddCommGroup M] [inst_5 : Module K M] [FiniteDimensional K M] (f : ι → End K M)
      (h :
        ∀ (i j : ι) (φ : K),
          MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M))
      (h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤)
      (h_dim : finrank K M = m),
      Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
ind :
  ∀ (this : ∀ (a : ι), ∃ (φ : K), (f a).maxGenEigenspace φ = ⊤),
    Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
⊢ Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
have ind₁ : ∀ (i : ι) (hy : ¬∃ (φ : K), (f i).maxGenEigenspace φ = ⊤),
  Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
Tactic: obtain this | ⟨i : ι, hy : ¬ ∃ φ, (f i).maxGenEigenspace φ = ⊤⟩ :=
    forall_or_exists_not (fun j : ι ↦ ∃ φ : K, (f j).maxGenEigenspace φ = ⊤)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst_4 : AddCommGroup M] [inst_5 : Module K M] [FiniteDimensional K M] (f : ι → End K M)
      (h :
        ∀ (i j : ι) (φ : K),
          MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M))
      (h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤)
      (h_dim : finrank K M = m),
      Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
this : ∀ (a : ι), ∃ (φ : K), (f a).maxGenEigenspace φ = ⊤
⊢ Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
have ind : ∀ (χ : (a : ι) → K) (hχ : ∀ (a : ι), (f a).maxGenEigenspace (χ a) = ⊤),
  Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
Tactic: choose χ hχ using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (hypothesis)
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst_4 : AddCommGroup M] [inst_5 : Module K M] [FiniteDimensional K M] (f : ι → End K M)
      (h :
        ∀ (i j : ι) (φ : K),
          MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M))
      (h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤)
      (h_dim : finrank K M = m),
      Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
χ : (a : ι) → K
hχ : ∀ (a : ι), (f a).maxGenEigenspace (χ a) = ⊤
⊢ Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
have hχ₁ : Eq.{u_4 + 1} (α := Submodule K M) (⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
Tactic: replace hχ : ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤ := by simpa
Cleared hypotheses: hχ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst_4 : AddCommGroup M] [inst_5 : Module K M] [FiniteDimensional K M] (f : ι → End K M)
      (h :
        ∀ (i j : ι) (φ : K),
          MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M))
      (h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤)
      (h_dim : finrank K M = m),
      Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
χ : (a : ι) → K
hχ : Eq.{u_4 + 1} (α := Submodule K M) (⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
⊢ Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
have ind : ∀ (hχ : LE.le.{u_4} (α := Submodule K M) ⊤ (⨅ (i : ι), (f i).maxGenEigenspace (χ i))),
  LE.le.{u_4} (α := Submodule K M) ⊤ (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
Tactic: simp_rw [eq_top_iff] at hχ ⊢
Cleared hypotheses: hχ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (hypothesis)
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst_4 : AddCommGroup M] [inst_5 : Module K M] [FiniteDimensional K M] (f : ι → End K M)
      (h :
        ∀ (i j : ι) (φ : K),
          MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M))
      (h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤)
      (h_dim : finrank K M = m),
      Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
i : ι
hy : ¬∃ (φ : K), (f i).maxGenEigenspace φ = ⊤
φ : K
⊢ finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) < n
have hy₁ : ∀ (x : K), (f i).maxGenEigenspace x < ⊤
Tactic: simp_rw [not_exists, ← lt_top_iff_ne_top] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (hypothesis)
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst_4 : AddCommGroup M] [inst_5 : Module K M] [FiniteDimensional K M] (f : ι → End K M)
      (h :
        ∀ (i j : ι) (φ : K),
          MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M))
      (h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤)
      (h_dim : finrank K M = m),
      Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
i : ι
hy : ¬∃ (φ : K), (f i).maxGenEigenspace φ = ⊤
⊢ Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
have hy₁ : ∀ (φ : K), finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) < n
Tactic: replace hy : ∀ φ, finrank K ((f i).maxGenEigenspace φ) < n := fun φ ↦ by
      simp_rw [not_exists, ← lt_top_iff_ne_top] at hy; exact h_dim ▸ Submodule.finrank_lt (hy φ).ne
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (hypothesis)
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst_4 : AddCommGroup M] [inst_5 : Module K M] [FiniteDimensional K M] (f : ι → End K M)
      (h :
        ∀ (i j : ι) (φ : K),
          MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M))
      (h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤)
      (h_dim : finrank K M = m),
      Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) < n
⊢ Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
have hi : ∀ (j : ι) (φ : K),
  MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace φ) : Set M) (↑((f i).maxGenEigenspace φ) : Set M)
Tactic: have hi (j : ι) (φ : K) :
        MapsTo (f j) ((f i).maxGenEigenspace φ) ((f i).maxGenEigenspace φ) := by
      exact h j i φ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst_4 : AddCommGroup M] [inst_5 : Module K M] [FiniteDimensional K M] (f : ι → End K M)
      (h :
        ∀ (i j : ι) (φ : K),
          MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M))
      (h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤)
      (h_dim : finrank K M = m),
      Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) < n
hi :
  ∀ (j : ι) (φ : K),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace φ) : Set M) (↑((f i).maxGenEigenspace φ) : Set M)
φ : K
⊢ Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
    (⨆ (χ : ι → K), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤
have h₁ : ∀ (i_1 j : ι) (φ_1 : K),
  MapsTo (⇑(LinearMap.restrict (f i_1) sorry) : (a : ↥((f i).maxGenEigenspace φ)) → ↥((f i).maxGenEigenspace φ))
    (↑(maxGenEigenspace (LinearMap.restrict (f j) sorry) φ_1) : Set ↥((f i).maxGenEigenspace φ))
    (↑(maxGenEigenspace (LinearMap.restrict (f j) sorry) φ_1) : Set ↥((f i).maxGenEigenspace φ))
Tactic: apply ih _ (hy φ)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst_4 : AddCommGroup M] [inst_5 : Module K M] [FiniteDimensional K M] (f : ι → End K M)
      (h :
        ∀ (i j : ι) (φ : K),
          MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M))
      (h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤)
      (h_dim : finrank K M = m),
      Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) < n
hi :
  ∀ (j : ι) (φ : K),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace φ) : Set M) (↑((f i).maxGenEigenspace φ) : Set M)
φ : K
h₁ :
  ∀ (i_1 j : ι) (φ_1 : K),
    MapsTo (⇑(LinearMap.restrict (f i_1) ⋯) : (a : ↥((f i).maxGenEigenspace φ)) → ↥((f i).maxGenEigenspace φ))
      (↑(maxGenEigenspace (LinearMap.restrict (f j) ⋯) φ_1) : Set ↥((f i).maxGenEigenspace φ))
      (↑(maxGenEigenspace (LinearMap.restrict (f j) ⋯) φ_1) : Set ↥((f i).maxGenEigenspace φ))
⊢ Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
    (⨆ (χ : ι → K), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤
have h'₁ : ∀ (i_1 : ι),
  Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
    (⨆ (μ : K), maxGenEigenspace (LinearMap.restrict (f i_1) sorry) μ) ⊤
Tactic: apply ih _ (hy φ)