awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 φ))
h'₁ :
  ∀ (i_1 : ι),
    Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
      (⨆ (μ : K), maxGenEigenspace (LinearMap.restrict (f i_1) ⋯) μ) ⊤
⊢ Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
    (⨆ (χ : ι → K), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤
have h_dim₁ : finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) = finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ)
Tactic: apply ih _ (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
hi :
  ∀ (j : ι) (φ : K),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace φ) : Set M) (↑((f i).maxGenEigenspace φ) : Set M)
⊢ Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
have ih₁ : ∀ (φ : K),
  Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
    (⨆ (χ : ι → K), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) sorry) (χ j)) ⊤
Tactic: replace ih (φ : K) :
        ⨆ χ : ι → K, ⨅ j, maxGenEigenspace ((f j).restrict (hi j φ)) (χ j) = ⊤ := by
      apply ih _ (hy φ)
      · intro j k μ
        exact mapsTo_restrict_maxGenEigenspace_restrict_of_mapsTo (f j) (f k) _ _ (h j k μ)
      · exact fun j ↦ Module.End.genEigenspace_restrict_eq_top _ (h' j)
      · rfl
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (hypothesis)
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
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)
ih :
  ∀ (φ : K),
    Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
      (⨆ (χ : ι → K), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤
φ : K
this :
  ∀ (χ : ι → K),
    χ i ≠ φ →
      Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
        (⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊥
⊢ Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
    (⨆ (χ : ι → K), ⨆ (_ : χ i = φ), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤
have ih₁ : Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
  (⨆ (χ : ι → K), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) sorry) (χ j)) ⊤
Tactic: specialize ih φ
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (hypothesis)
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
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
this :
  ∀ (χ : ι → K),
    χ i ≠ φ →
      Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
        (⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊥
ih :
  Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
    (⨆ (χ : ι → K), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤
⊢ Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
    (⨆ (χ : ι → K), ⨆ (_ : χ i = φ), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤
have ih₁ : Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
  ((⨆ (i_1 : ι → K), ⨆ (_ : i_1 i ≠ φ), ⊥) ⊔
    ⨆ (i_1 : ι → K), ⨆ (_ : ¬i_1 i ≠ φ), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) sorry) (i_1 j))
  ⊤
Tactic: rw [iSup_split, biSup_congr this] at ih
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
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)
ih :
  ∀ (φ : K),
    Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
      (⨆ (χ : ι → K), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤
φ : K
⊢ Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
    (⨆ (χ : ι → K), ⨆ (_ : χ i = φ), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤
have suffices : ∀ (χ : ι → K),
  χ i ≠ φ →
    Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
      (⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) sorry) (χ j)) ⊥
Tactic: suffices ∀ χ : ι → K, χ i ≠ φ → ⨅ j, maxGenEigenspace ((f j).restrict (hi j φ)) (χ j) = ⊥ by
        specialize ih φ; rw [iSup_split, biSup_congr this] at ih; simpa using ih
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
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)
ih :
  ∀ (φ : K),
    Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
      (⨆ (χ : ι → K), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤
φ : K
χ : ι → K
hχ : χ i ≠ φ
⊢ Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
    (⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊥
have rw : Disjoint ((f i).maxGenEigenspace φ) (⨅ (i : ι), (f i).maxGenEigenspace (χ i))
Tactic: rw [eq_bot_iff, ← ((f i).maxGenEigenspace φ).ker_subtype, LinearMap.ker,
        ← Submodule.map_le_iff_le_comap, ← Submodule.inf_iInf_maxGenEigenspace_of_forall_mapsTo,
        ← disjoint_iff_inf_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (hypothesis)
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
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)
ih :
  ∀ (φ : K),
    Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
      (⨆ (χ : ι → K), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤
⊢ Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
have ih₁ : ∀ (φ : K),
  Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
    (⨆ (χ : ι → K), ⨆ (_ : χ i = φ), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) sorry) (χ j)) ⊤
Tactic: replace ih (φ : K) :
        ⨆ (χ : ι → K) (_ : χ i = φ), ⨅ j, maxGenEigenspace ((f j).restrict (hi j φ)) (χ j) = ⊤ := by
      suffices ∀ χ : ι → K, χ i ≠ φ → ⨅ j, maxGenEigenspace ((f j).restrict (hi j φ)) (χ j) = ⊥ by
        specialize ih φ; rw [iSup_split, biSup_congr this] at ih; simpa using ih
      intro χ hχ
      rw [eq_bot_iff, ← ((f i).maxGenEigenspace φ).ker_subtype, LinearMap.ker,
        ← Submodule.map_le_iff_le_comap, ← Submodule.inf_iInf_maxGenEigenspace_of_forall_mapsTo,
        ← disjoint_iff_inf_le]
      exact ((f i).disjoint_genEigenspace hχ.symm _ _).mono_right (iInf_le _ i)
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
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)
ih :
  ∀ (φ : K),
    Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
      (⨆ (χ : ι → K), ⨆ (_ : χ i = φ), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤
φ : K
χ : ι → K
hχ : χ i = φ
⊢ ⨅ (j : ι), (f j).maxGenEigenspace (χ j) =
    Submodule.map ((f i).maxGenEigenspace φ).subtype (⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j))
have rw : ⨅ (j : ι), (f j).maxGenEigenspace (χ j) =
  Submodule.map ((f i).maxGenEigenspace (χ i)).subtype (⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) sorry) (χ j))
Tactic: rw [← hχ, iInf_maxGenEigenspace_restrict_map_subtype_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
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)
ih :
  ∀ (φ : K),
    Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
      (⨆ (χ : ι → K), ⨆ (_ : χ i = φ), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤
φ : K
χ : ι → K
hχ : χ i = φ
rw :
  ⨅ (j : ι), (f j).maxGenEigenspace (χ j) =
    Submodule.map ((f i).maxGenEigenspace (χ i)).subtype
      (⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j))
⊢ ⨅ (j : ι), (f j).maxGenEigenspace (χ j) =
    Submodule.map ((f i).maxGenEigenspace φ).subtype (⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j))
have rw₁ : Eq.{u_4 + 1} (α := Submodule K M) (⨅ (j : ι), (f j).maxGenEigenspace (χ j)) (⨅ (j : ι), (f j).maxGenEigenspace (χ j))
Tactic: rw [← hχ, iInf_maxGenEigenspace_restrict_map_subtype_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (hypothesis)
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
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)
ih :
  ∀ (φ : K),
    Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
      (⨆ (χ : ι → K), ⨆ (_ : χ i = φ), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤
φ : K
⊢ ⨆ (χ : ι → K), ⨆ (_ : χ i = φ), ⨅ (j : ι), (f j).maxGenEigenspace (χ j) = (f i).maxGenEigenspace φ
have this : ∀ (χ : ι → K) (hχ : χ i = φ),
  ⨅ (j : ι), (f j).maxGenEigenspace (χ j) =
    Submodule.map ((f i).maxGenEigenspace φ).subtype (⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) sorry) (χ j))
Tactic: have (χ : ι → K) (hχ : χ i = φ) : ⨅ j, maxGenEigenspace (f j) (χ j) =
          (⨅ j, maxGenEigenspace ((f j).restrict (hi j φ)) (χ j)).map
            ((f i).maxGenEigenspace φ).subtype := by
        rw [← hχ, iInf_maxGenEigenspace_restrict_map_subtype_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
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)
ih :
  ∀ (φ : K),
    Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
      (⨆ (χ : ι → K), ⨆ (_ : χ i = φ), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤
φ : K
this :
  ∀ (χ : ι → K) (hχ : χ i = φ),
    ⨅ (j : ι), (f j).maxGenEigenspace (χ j) =
      Submodule.map ((f i).maxGenEigenspace φ).subtype (⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j))
⊢ ⨆ (χ : ι → K), ⨆ (_ : χ i = φ), ⨅ (j : ι), (f j).maxGenEigenspace (χ j) = (f i).maxGenEigenspace φ
have simp_rw : ⨆ (i_1 : ι → K),
    ⨆ (_ : i_1 i = φ),
      Submodule.map ((f i).maxGenEigenspace φ).subtype
        (⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) sorry) (i_1 j)) =
  (f i).maxGenEigenspace φ
Tactic: simp_rw [biSup_congr this, ← Submodule.map_iSup, ih, Submodule.map_top,
        Submodule.range_subtype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
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)
ih :
  ∀ (φ : K),
    Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
      (⨆ (χ : ι → K), ⨆ (_ : χ i = φ), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤
φ : K
this :
  ∀ (χ : ι → K) (hχ : χ i = φ),
    ⨅ (j : ι), (f j).maxGenEigenspace (χ j) =
      Submodule.map ((f i).maxGenEigenspace φ).subtype (⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j))
simp_rw :
  ⨆ (i_1 : ι → K),
      ⨆ (_ : i_1 i = φ),
        Submodule.map ((f i).maxGenEigenspace φ).subtype
          (⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (i_1 j)) =
    (f i).maxGenEigenspace φ
⊢ ⨆ (χ : ι → K), ⨆ (_ : χ i = φ), ⨅ (j : ι), (f j).maxGenEigenspace (χ j) = (f i).maxGenEigenspace φ
have simp_rw₁ : Submodule.map ((f i).maxGenEigenspace φ).subtype
    (⨆ (i_1 : ι → K), ⨆ (_ : i_1 i = φ), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) sorry) (i_1 j)) =
  (f i).maxGenEigenspace φ
Tactic: simp_rw [biSup_congr this, ← Submodule.map_iSup, ih, Submodule.map_top,
        Submodule.range_subtype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
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)
ih :
  ∀ (φ : K),
    Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
      (⨆ (χ : ι → K), ⨆ (_ : χ i = φ), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤
φ : K
this :
  ∀ (χ : ι → K) (hχ : χ i = φ),
    ⨅ (j : ι), (f j).maxGenEigenspace (χ j) =
      Submodule.map ((f i).maxGenEigenspace φ).subtype (⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j))
simp_rw :
  ⨆ (i_1 : ι → K),
      ⨆ (_ : i_1 i = φ),
        Submodule.map ((f i).maxGenEigenspace φ).subtype
          (⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (i_1 j)) =
    (f i).maxGenEigenspace φ
simp_rw₁ :
  Submodule.map ((f i).maxGenEigenspace φ).subtype
      (⨆ (i_1 : ι → K), ⨆ (_ : i_1 i = φ), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (i_1 j)) =
    (f i).maxGenEigenspace φ
⊢ ⨆ (χ : ι → K), ⨆ (_ : χ i = φ), ⨅ (j : ι), (f j).maxGenEigenspace (χ j) = (f i).maxGenEigenspace φ
have simp_rw₂ : Submodule.map ((f i).maxGenEigenspace φ).subtype ⊤ = (f i).maxGenEigenspace φ
Tactic: simp_rw [biSup_congr this, ← Submodule.map_iSup, ih, Submodule.map_top,
        Submodule.range_subtype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
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)
ih :
  ∀ (φ : K),
    Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
      (⨆ (χ : ι → K), ⨆ (_ : χ i = φ), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤
φ : K
this :
  ∀ (χ : ι → K) (hχ : χ i = φ),
    ⨅ (j : ι), (f j).maxGenEigenspace (χ j) =
      Submodule.map ((f i).maxGenEigenspace φ).subtype (⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j))
simp_rw :
  ⨆ (i_1 : ι → K),
      ⨆ (_ : i_1 i = φ),
        Submodule.map ((f i).maxGenEigenspace φ).subtype
          (⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (i_1 j)) =
    (f i).maxGenEigenspace φ
simp_rw₁ :
  Submodule.map ((f i).maxGenEigenspace φ).subtype
      (⨆ (i_1 : ι → K), ⨆ (_ : i_1 i = φ), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (i_1 j)) =
    (f i).maxGenEigenspace φ
simp_rw₂ : Submodule.map ((f i).maxGenEigenspace φ).subtype ⊤ = (f i).maxGenEigenspace φ
⊢ ⨆ (χ : ι → K), ⨆ (_ : χ i = φ), ⨅ (j : ι), (f j).maxGenEigenspace (χ j) = (f i).maxGenEigenspace φ
have simp_rw₃ : ((f i).maxGenEigenspace φ).subtype.range = (f i).maxGenEigenspace φ
Tactic: simp_rw [biSup_congr this, ← Submodule.map_iSup, ih, Submodule.map_top,
        Submodule.range_subtype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (hypothesis)
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
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)
ih :
  ∀ (φ : K),
    Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
      (⨆ (χ : ι → K), ⨆ (_ : χ i = φ), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤
⊢ Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
have ih₁ : ∀ (φ : K), ⨆ (χ : ι → K), ⨆ (_ : χ i = φ), ⨅ (j : ι), (f j).maxGenEigenspace (χ j) = (f i).maxGenEigenspace φ
Tactic: replace ih (φ : K) :
        ⨆ (χ : ι → K) (_ : χ i = φ), ⨅ j, maxGenEigenspace (f j) (χ j) =
        maxGenEigenspace (f i) φ := by
      have (χ : ι → K) (hχ : χ i = φ) : ⨅ j, maxGenEigenspace (f j) (χ j) =
          (⨅ j, maxGenEigenspace ((f j).restrict (hi j φ)) (χ j)).map
            ((f i).maxGenEigenspace φ).subtype := by
        rw [← hχ, iInf_maxGenEigenspace_restrict_map_subtype_eq]
      simp_rw [biSup_congr this, ← Submodule.map_iSup, ih, Submodule.map_top,
        Submodule.range_subtype]
Cleared hypotheses: ih