awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Minpoly (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
μ : R
h : f.HasEigenvalue μ
w : M
H : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) 1 : Submodule R M) w
ne0 : w ≠ 0
⊢ IsRoot (minpoly R f) μ
have refine : eval μ (minpoly R f) • w = 0
Tactic: refine Or.resolve_right (smul_eq_zero.1 ?_) ne0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Minpoly (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
μ : R
h : f.HasEigenvalue μ
w : M
H : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) 1 : Submodule R M) w
ne0 : w ≠ 0
⊢ eval μ (minpoly R f) • w = 0
have rw : Eq (α := M) ((((aeval f : (a : R[X]) → End R M) (minpoly R f) : End R M) : (a : M) → M) w : M) (0 : M)
Tactic: rw [← aeval_apply_of_hasEigenvector ⟨H, ne0⟩]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Minpoly (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
inst_3 : IsDomain R
inst_4 : Module.Finite R M
h : IsRoot (minpoly R f) μ
⊢ f.HasEigenvalue μ
have obtain : ∀ (q : R[X]) (hq : minpoly R f = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]) * q),
  f.HasEigenvalue μ
Tactic: obtain ⟨q, hq⟩ := dvd_iff_isRoot.mpr h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Minpoly (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
inst_3 : IsDomain R
inst_4 : Module.Finite R M
h : IsRoot (minpoly R f) μ
q : R[X]
hq : minpoly R f = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]) * q
⊢ ∃ (v : M), Ne (α := M) ((((aeval f : (a : R[X]) → End R M) q : End R M) : (a : M) → M) v : M) (0 : M)
have by_contra! : ∀ (h_contra : ∀ (v : M), Eq (α := M) ((((aeval f : (a : R[X]) → End R M) q : End R M) : (a : M) → M) v : M) (0 : M)),
  False
Tactic: by_contra! h_contra
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Minpoly (hypothesis)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
inst_3 : IsDomain R
inst_4 : Module.Finite R M
h : IsRoot (minpoly R f) μ
q : R[X]
hq : minpoly R f = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]) * q
h_contra : ∀ (v : M), Eq (α := M) ((((aeval f : (a : R[X]) → End R M) q : End R M) : (a : M) → M) v : M) (0 : M)
⊢ False
have this : degree (minpoly R f) ≤ q.degree
Tactic: have := minpoly.min R f
      ((monic_X_sub_C μ).of_mul_monic_left (hq ▸ minpoly.monic (Algebra.IsIntegral.isIntegral f)))
      (LinearMap.ext h_contra)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Minpoly (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
inst_3 : IsDomain R
inst_4 : Module.Finite R M
h : IsRoot (minpoly R f) μ
q : R[X]
hq : minpoly R f = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]) * q
h_contra : ∀ (v : M), Eq (α := M) ((((aeval f : (a : R[X]) → End R M) q : End R M) : (a : M) → M) v : M) (0 : M)
this : degree (minpoly R f) ≤ q.degree
⊢ False
have rw : ∀ (this : HAdd.hAdd (α := WithBot ℕ) 1 (↑q.natDegree : WithBot ℕ) ≤ (↑q.natDegree : WithBot ℕ)), False
Tactic: rw [hq, degree_mul, degree_X_sub_C, degree_eq_natDegree] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Minpoly (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
inst_3 : IsDomain R
inst_4 : Module.Finite R M
h : IsRoot (minpoly R f) μ
q : R[X]
hq : minpoly R f = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]) * q
h_contra : ∀ (v : M), Eq (α := M) ((((aeval f : (a : R[X]) → End R M) q : End R M) : (a : M) → M) v : M) (0 : M)
this : degree (minpoly R f) ≤ q.degree
rw : ∀ (this : HAdd.hAdd (α := WithBot ℕ) 1 (↑q.natDegree : WithBot ℕ) ≤ (↑q.natDegree : WithBot ℕ)), False
⊢ False
have rw₁ : ∀ (this : 1 + q.degree ≤ q.degree), q ≠ 0
Tactic: rw [hq, degree_mul, degree_X_sub_C, degree_eq_natDegree] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Minpoly (hypothesis)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
inst_3 : IsDomain R
inst_4 : Module.Finite R M
h : IsRoot (minpoly R f) μ
q : R[X]
hq : minpoly R f = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]) * q
h_contra : ∀ (v : M), Eq (α := M) ((((aeval f : (a : R[X]) → End R M) q : End R M) : (a : M) → M) v : M) (0 : M)
this : HAdd.hAdd (α := WithBot ℕ) 1 (↑q.natDegree : WithBot ℕ) ≤ (↑q.natDegree : WithBot ℕ)
⊢ False
have this₁ : 1 + q.natDegree ≤ q.natDegree
Tactic: norm_cast at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Minpoly (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
inst_3 : IsDomain R
inst_4 : Module.Finite R M
h : IsRoot (minpoly R f) μ
q : R[X]
hq : minpoly R f = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]) * q
⊢ f.HasEigenvalue μ
have obtain : ∀ (v : M) (hv : Ne (α := M) ((((aeval f : (a : R[X]) → End R M) q : End R M) : (a : M) → M) v : M) (0 : M)),
  f.HasEigenvalue μ
Tactic: obtain ⟨v, hv⟩ : ∃ v : M, q.aeval f v ≠ 0 := by
    by_contra! h_contra
    have := minpoly.min R f
      ((monic_X_sub_C μ).of_mul_monic_left (hq ▸ minpoly.monic (Algebra.IsIntegral.isIntegral f)))
      (LinearMap.ext h_contra)
    rw [hq, degree_mul, degree_X_sub_C, degree_eq_natDegree] at this
    · norm_cast at this; grind
    · rintro rfl
      exact minpoly.ne_zero (Algebra.IsIntegral.isIntegral f) (mul_zero (X - C μ) ▸ hq)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Minpoly (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
inst_3 : IsDomain R
inst_4 : Module.Finite R M
h : IsRoot (minpoly R f) μ
q : R[X]
hq : minpoly R f = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]) * q
v : M
hv : Ne (α := M) ((((aeval f : (a : R[X]) → End R M) q : End R M) : (a : M) → M) v : M) (0 : M)
⊢ f.HasEigenvalue μ
have refine : Membership.mem (α := M) (f.eigenspace μ) ((((aeval f : (a : R[X]) → End R M) q : End R M) : (a : M) → M) v : M)
Tactic: refine Module.End.hasEigenvalue_of_hasEigenvector (hasEigenvector_iff.mpr ⟨?_, hv⟩)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Minpoly (hypothesis)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
inst_3 : IsDomain R
inst_4 : Module.Finite R M
inst_5 : IsTorsionFree R M
⊢ Set.Finite f.HasEigenvalue
have h : Ne (α := R[X]) (minpoly R f) 0
Tactic: have h : minpoly R f ≠ 0 := minpoly.ne_zero (Algebra.IsIntegral.isIntegral (R := R) f)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Minpoly (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
inst_3 : IsDomain R
inst_4 : Module.Finite R M
inst_5 : IsTorsionFree R M
h : Ne (α := R[X]) (minpoly R f) 0
⊢ Set.Finite f.HasEigenvalue
have h₁ : f.HasEigenvalue = rootSet (minpoly R f) R
Tactic: convert! (minpoly R f).rootSet_finite R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Minpoly (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
inst_3 : IsDomain R
inst_4 : Module.Finite R M
inst_5 : IsTorsionFree R M
h : Ne (α := R[X]) (minpoly R f) 0
⊢ f.HasEigenvalue = rootSet (minpoly R f) R
have h₁ : ∀ (μ : R), μ ∈ f.HasEigenvalue ↔ μ ∈ rootSet (minpoly R f) R
Tactic: ext μ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Minpoly (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
inst_3 : IsDomain R
inst_4 : Module.Finite R M
inst_5 : IsTorsionFree R M
h : Ne (α := R[X]) (minpoly R f) 0
μ : R
⊢ f.HasEigenvalue μ ↔ μ ∈ rootSet (minpoly R f) R
have h₁ : IsRoot (minpoly R f) μ ↔ μ ∈ rootSet (minpoly R f) R
Tactic: rw [hasEigenvalue_iff_isRoot, mem_rootSet_of_ne h, IsRoot, coe_aeval_eq_eval]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Minpoly (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
inst_3 : IsDomain R
inst_4 : Module.Finite R M
inst_5 : IsTorsionFree R M
h : Ne (α := R[X]) (minpoly R f) 0
μ : R
h₁ : IsRoot (minpoly R f) μ ↔ μ ∈ rootSet (minpoly R f) R
⊢ f.HasEigenvalue μ ↔ μ ∈ rootSet (minpoly R f) R
have h₂ : IsRoot (minpoly R f) μ ↔ Eq (α := R) ((aeval μ : (a : R[X]) → R) (minpoly R f) : R) (0 : R)
Tactic: rw [hasEigenvalue_iff_isRoot, mem_rootSet_of_ne h, IsRoot, coe_aeval_eq_eval]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Minpoly (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
inst_3 : IsDomain R
inst_4 : Module.Finite R M
inst_5 : IsTorsionFree R M
h : Ne (α := R[X]) (minpoly R f) 0
μ : R
h₁ : IsRoot (minpoly R f) μ ↔ μ ∈ rootSet (minpoly R f) R
h₂ : IsRoot (minpoly R f) μ ↔ Eq (α := R) ((aeval μ : (a : R[X]) → R) (minpoly R f) : R) (0 : R)
⊢ f.HasEigenvalue μ ↔ μ ∈ rootSet (minpoly R f) R
have h₃ : eval μ (minpoly R f) = 0 ↔ Eq (α := R) ((aeval μ : (a : R[X]) → R) (minpoly R f) : R) (0 : R)
Tactic: rw [hasEigenvalue_iff_isRoot, mem_rootSet_of_ne h, IsRoot, coe_aeval_eq_eval]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Minpoly (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
inst_3 : IsDomain R
inst_4 : Module.Finite R M
inst_5 : IsTorsionFree R M
h : Ne (α := R[X]) (minpoly R f) 0
μ : R
h₁ : IsRoot (minpoly R f) μ ↔ μ ∈ rootSet (minpoly R f) R
h₂ : IsRoot (minpoly R f) μ ↔ Eq (α := R) ((aeval μ : (a : R[X]) → R) (minpoly R f) : R) (0 : R)
h₃ : eval μ (minpoly R f) = 0 ↔ Eq (α := R) ((aeval μ : (a : R[X]) → R) (minpoly R f) : R) (0 : R)
⊢ f.HasEigenvalue μ ↔ μ ∈ rootSet (minpoly R f) R
have h₄ : eval μ (minpoly R f) = 0 ↔ eval μ (minpoly R f) = 0
Tactic: rw [hasEigenvalue_iff_isRoot, mem_rootSet_of_ne h, IsRoot, coe_aeval_eq_eval]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Minpoly (goal)
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
⊢ f.eigenspace (-q.coeff 0 / q.leadingCoeff) =
    LinearMap.ker
      (HSub.hSub (β := End K V) (q.leadingCoeff • f)
        ((algebraMap K (End K V) : (a : K) → End K V) (-q.coeff 0) : End K V))
have hb : q.leadingCoeff ≠ 0
Tactic: apply eigenspace_div
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Minpoly (goal)
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
⊢ q.leadingCoeff ≠ 0
have hb : ¬Eq (α := WithBot ℕ) 1 ⊥
Tactic: rw [Ne, leadingCoeff_eq_zero_iff_deg_eq_bot, hq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Minpoly (goal)
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
⊢ LinearMap.ker
      (HSub.hSub (β := End K V) (q.leadingCoeff • f)
        ((algebraMap K (End K V) : (a : K) → End K V) (-q.coeff 0) : End K V)) =
    LinearMap.ker (R₂ := K) (M₂ := V) (τ₁₂ := RingHom.id K)
      ((aeval f : (a : K[X]) → End K V)
        (HAdd.hAdd (β := K[X]) (HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) q.leadingCoeff : K[X]) X)
          ((C : (a : K) → K[X]) (q.coeff 0) : K[X])))
have rw : LinearMap.ker
    (HSub.hSub (β := End K V) (q.leadingCoeff • f)
      ((algebraMap K (End K V) : (a : K) → End K V) (-q.coeff 0) : End K V)) =
  LinearMap.ker
    (eval₂ (algebraMap K (End K V)) f
      (HAdd.hAdd (β := K[X]) (HSMul.hSMul (β := K[X]) q.leadingCoeff X) ((C : (a : K) → K[X]) (q.coeff 0) : K[X])))
Tactic: rw [C_mul', aeval_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Minpoly (goal)
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
⊢ Eq.{w + 1} (α := Submodule K V)
    (LinearMap.ker (R₂ := K) (M₂ := V) (τ₁₂ := RingHom.id K)
      ((aeval f : (a : K[X]) → End K V)
        (HAdd.hAdd (β := K[X]) (HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) q.leadingCoeff : K[X]) X)
          ((C : (a : K) → K[X]) (q.coeff 0) : K[X]))))
    (LinearMap.ker (R₂ := K) (M₂ := V) (τ₁₂ := RingHom.id K) ((aeval f : (a : K[X]) → End K V) q))
have rwa : Eq.{w + 1} (α := Submodule K V)
  (LinearMap.ker (R₂ := K) (M₂ := V) (τ₁₂ := RingHom.id K) ((aeval f : (a : K[X]) → End K V) q))
  (LinearMap.ker (R₂ := K) (M₂ := V) (τ₁₂ := RingHom.id K) ((aeval f : (a : K[X]) → End K V) q))
Tactic: rwa [← eq_X_add_C_of_degree_eq_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Minpoly (goal)
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
⊢ (spectrum K f).Finite
have h : Eq (α := (a : End K V) → Set K) (spectrum K) HasEigenvalue
Tactic: convert! f.finite_hasEigenvalue
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Minpoly (goal)
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
⊢ Eq (α := (a : End K V) → Set K) (spectrum K) HasEigenvalue
have h : ∀ (f : End K V) (x : K), x ∈ spectrum K f ↔ x ∈ f.HasEigenvalue
Tactic: ext f x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Minpoly (goal)
Goal:
n : Type u_1
R : Type u_2
inst : Field R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n R
⊢ (spectrum R A).Finite
have rw : (spectrum R (A := (n → R) →ₗ[R] n → R)
    ((toLinAlgEquiv (Pi.basisFun R n) : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) A : (n → R) →ₗ[R] n → R)).Finite
Tactic: rw [← AlgEquiv.spectrum_eq (Matrix.toLinAlgEquiv <| Pi.basisFun R n) A]
-- 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
μ : ι → R
p : Submodule R M
hfp : ∀ (i : ι), MapsTo (⇑(f i) : (a : M) → M) (↑p : Set M) (↑p : Set M)
⊢ p ⊓ ⨅ (i : ι), (f i).maxGenEigenspace (μ i) =
    Submodule.map p.subtype (⨅ (i : ι), maxGenEigenspace (LinearMap.restrict (f i) ⋯) (μ i))
have inl : IsEmpty ι →
  p ⊓ ⨅ (i : ι), (f i).maxGenEigenspace (μ i) =
    Submodule.map p.subtype (⨅ (i : ι), maxGenEigenspace (LinearMap.restrict (f i) sorry) (μ i))
Tactic: cases isEmpty_or_nonempty ι
-- 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
μ : ι → R
p : Submodule R M
hfp : ∀ (i : ι), MapsTo (⇑(f i) : (a : M) → M) (↑p : Set M) (↑p : Set M)
inl :
  IsEmpty ι →
    p ⊓ ⨅ (i : ι), (f i).maxGenEigenspace (μ i) =
      Submodule.map p.subtype (⨅ (i : ι), maxGenEigenspace (LinearMap.restrict (f i) ⋯) (μ i))
⊢ p ⊓ ⨅ (i : ι), (f i).maxGenEigenspace (μ i) =
    Submodule.map p.subtype (⨅ (i : ι), maxGenEigenspace (LinearMap.restrict (f i) ⋯) (μ i))
have inr : Nonempty ι →
  p ⊓ ⨅ (i : ι), (f i).maxGenEigenspace (μ i) =
    Submodule.map p.subtype (⨅ (i : ι), maxGenEigenspace (LinearMap.restrict (f i) sorry) (μ i))
Tactic: cases isEmpty_or_nonempty ι
-- 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
μ : ι → R
p : Submodule R M
hfp : ∀ (i : ι), MapsTo (⇑(f i) : (a : M) → M) (↑p : Set M) (↑p : Set M)
h : Nonempty ι
⊢ p ⊓ ⨅ (i : ι), (f i).maxGenEigenspace (μ i) =
    Submodule.map p.subtype (⨅ (i : ι), maxGenEigenspace (LinearMap.restrict (f i) ⋯) (μ i))
have inr : ⨅ (x : ι), p ⊓ (f x).maxGenEigenspace (μ x) =
  Submodule.map p.subtype (⨅ (i : ι), maxGenEigenspace (LinearMap.restrict (f i) sorry) (μ i))
Tactic: simp_rw [inf_iInf, p.inf_genEigenspace _ (hfp _), Submodule.map_iInf _ p.injective_subtype]
-- 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
μ : ι → R
p : Submodule R M
hfp : ∀ (i : ι), MapsTo (⇑(f i) : (a : M) → M) (↑p : Set M) (↑p : Set M)
h : Nonempty ι
inr :
  ⨅ (x : ι), p ⊓ (f x).maxGenEigenspace (μ x) =
    Submodule.map p.subtype (⨅ (i : ι), maxGenEigenspace (LinearMap.restrict (f i) ⋯) (μ i))
⊢ p ⊓ ⨅ (i : ι), (f i).maxGenEigenspace (μ i) =
    Submodule.map p.subtype (⨅ (i : ι), maxGenEigenspace (LinearMap.restrict (f i) ⋯) (μ i))
have inr₁ : ⨅ (x : ι), Submodule.map p.subtype ((genEigenspace (LinearMap.restrict (f x) sorry) (μ x) : (a : ℕ∞) → Submodule R ↥p) ⊤) =
  Submodule.map p.subtype (⨅ (i : ι), maxGenEigenspace (LinearMap.restrict (f i) sorry) (μ i))
Tactic: simp_rw [inf_iInf, p.inf_genEigenspace _ (hfp _), Submodule.map_iInf _ p.injective_subtype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (hypothesis)
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)
⊢ Submodule.map ((f i).maxGenEigenspace (μ i)).subtype
      (⨅ (j : ι), (fun (j : ι) ↦ maxGenEigenspace (LinearMap.restrict (f j) ⋯) (μ j)) j) =
    ⨅ (j : ι), (f j).maxGenEigenspace (μ j)
have this : Nonempty ι
Tactic: have : Nonempty ι := ⟨i⟩
-- 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
μ : ι → 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)
have refine : ⨅ (j : ι), (f j).maxGenEigenspace (μ j) ≤ p ⊓ ⨅ (j : ι), (f j).maxGenEigenspace (μ j)
Tactic: refine le_antisymm ?_ inf_le_right
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (hypothesis)
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)
⊢ Submodule.map ((f i).maxGenEigenspace (μ i)).subtype
      (⨅ (j : ι), (fun (j : ι) ↦ maxGenEigenspace (LinearMap.restrict (f j) ⋯) (μ j)) j) =
    ⨅ (j : ι), (f j).maxGenEigenspace (μ j)
have this₁ : ⨅ (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 _ _
-- 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
μ : ι → 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)
⊢ Submodule.map ((f i).maxGenEigenspace (μ i)).subtype
      (⨅ (j : ι), (fun (j : ι) ↦ maxGenEigenspace (LinearMap.restrict (f j) ⋯) (μ j)) j) =
    ⨅ (j : ι), (f j).maxGenEigenspace (μ j)
have rw : Eq.{u_4 + 1} (α := Submodule R M)
  (⨅ (i_1 : ι), Submodule.map p.subtype (maxGenEigenspace (LinearMap.restrict (f i_1) sorry) (μ i_1)))
  (⨅ (i : ι), p ⊓ (f i).maxGenEigenspace (μ i))
Tactic: rw [Submodule.map_iInf _ p.injective_subtype, this, Submodule.inf_iInf]
-- 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
μ : ι → 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)
| ⨅ (i : ι), p ⊓ (f i).maxGenEigenspace (μ i)
have enter : fun (i : ι) ↦ p ⊓ (f i).maxGenEigenspace (μ i)
Tactic: enter [1]
-- 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
μ : ι → 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)
| fun (i : ι) ↦ p ⊓ (f i).maxGenEigenspace (μ i)
have h₁ : ∀ (x : ι), p ⊓ (f x).maxGenEigenspace (μ x)
Tactic: ext
-- 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
μ : ι → 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 : ι
| p ⊓ (f x).maxGenEigenspace (μ x)
have h₁ : Submodule.map p.subtype ((genEigenspace (LinearMap.restrict (f x) sorry) (μ x) : (a : ℕ∞) → Submodule R ↥p) ⊤)
Tactic: rw [p.inf_genEigenspace (f _) (h _)]
-- 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
μ : ι → 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)
| ⨅ (i : ι), p ⊓ (f i).maxGenEigenspace (μ i)
have h₁ : ∀ (x : ι), Submodule.map p.subtype ((genEigenspace (LinearMap.restrict (f x) sorry) (μ x) : (a : ℕ∞) → Submodule R ↥p) ⊤)
Tactic: enter [1]
    ext
    rw [p.inf_genEigenspace (f _) (h _)]