awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (hypothesis)
Goal:
R : Type u_4
B : Type u_5
inst : CommRing R
inst_1 : NonUnitalNonAssocRing B
inst_2 : Module R B
inst_3 : SMulCommClass R B B
inst_4 : IsScalarTower R B B
inst_5 : Module ℚ B
D : B →ₗ[R] B
h_der :
  ∀ (x y : B),
    (D : (a : B) → B) (x * y) =
      HMul.hMul (β := B) x ((D : (a : B) → B) y : B) + HMul.hMul (α := B) ((D : (a : B) → B) x : B) y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
h_nilL : IsNilpotent DL
h_nilR : IsNilpotent DR
h_comm : Commute DL DR
m : B ⊗[R] B →ₗ[R] B := LinearMap.mul' R B
hm : m = LinearMap.mul' R B
⊢ (exp D : (a : B) → B) (x * y) =
    HMul.hMul (α := B) (β := B) ((exp D : (a : B) → B) x : B) ((exp D : (a : B) → B) y : B)
have h₁ : Eq (α := B) ((exp D : (a : B) → B) (x * y) : B)
  ((m : (a : B ⊗[R] B) → B) ((exp (DL + DR) : (a : B ⊗[R] B) → B ⊗[R] B) (x ⊗ₜ[R] y) : B ⊗[R] B) : B)
Tactic: have h₁ : exp D (x * y) = m (exp (DL + DR) (x ⊗ₜ[R] y)) := by
    suffices exp D ∘ₗ m = m ∘ₗ exp (DL + DR) by simpa using LinearMap.congr_fun this (x ⊗ₜ[R] y)
    apply commute_exp_left_of_commute (h_comm.isNilpotent_add h_nilL h_nilR) h_nil
    ext
    simp [DL, DR, hm, h_der]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (hypothesis)
Goal:
R : Type u_4
B : Type u_5
inst : CommRing R
inst_1 : NonUnitalNonAssocRing B
inst_2 : Module R B
inst_3 : SMulCommClass R B B
inst_4 : IsScalarTower R B B
inst_5 : Module ℚ B
D : B →ₗ[R] B
h_der :
  ∀ (x y : B),
    (D : (a : B) → B) (x * y) =
      HMul.hMul (β := B) x ((D : (a : B) → B) y : B) + HMul.hMul (α := B) ((D : (a : B) → B) x : B) y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
h_nilL : IsNilpotent DL
h_nilR : IsNilpotent DR
h_comm : Commute DL DR
m : B ⊗[R] B →ₗ[R] B := LinearMap.mul' R B
hm : m = LinearMap.mul' R B
h₁ :
  Eq (α := B) ((exp D : (a : B) → B) (x * y) : B)
    ((m : (a : B ⊗[R] B) → B) ((exp (DL + DR) : (a : B ⊗[R] B) → B ⊗[R] B) (x ⊗ₜ[R] y) : B ⊗[R] B) : B)
⊢ (exp D : (a : B) → B) (x * y) =
    HMul.hMul (α := B) (β := B) ((exp D : (a : B) → B) x : B) ((exp D : (a : B) → B) y : B)
have h₂ : exp DL = LinearMap.lTensor B (exp D)
Tactic: have h₂ : exp DL = (exp D).lTensor B := (h_nil.map_exp (lTensorAlgHom R B B)).symm
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (hypothesis)
Goal:
R : Type u_4
B : Type u_5
inst : CommRing R
inst_1 : NonUnitalNonAssocRing B
inst_2 : Module R B
inst_3 : SMulCommClass R B B
inst_4 : IsScalarTower R B B
inst_5 : Module ℚ B
D : B →ₗ[R] B
h_der :
  ∀ (x y : B),
    (D : (a : B) → B) (x * y) =
      HMul.hMul (β := B) x ((D : (a : B) → B) y : B) + HMul.hMul (α := B) ((D : (a : B) → B) x : B) y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
h_nilL : IsNilpotent DL
h_nilR : IsNilpotent DR
h_comm : Commute DL DR
m : B ⊗[R] B →ₗ[R] B := LinearMap.mul' R B
hm : m = LinearMap.mul' R B
h₁ :
  Eq (α := B) ((exp D : (a : B) → B) (x * y) : B)
    ((m : (a : B ⊗[R] B) → B) ((exp (DL + DR) : (a : B ⊗[R] B) → B ⊗[R] B) (x ⊗ₜ[R] y) : B ⊗[R] B) : B)
h₂ : exp DL = LinearMap.lTensor B (exp D)
⊢ (exp D : (a : B) → B) (x * y) =
    HMul.hMul (α := B) (β := B) ((exp D : (a : B) → B) x : B) ((exp D : (a : B) → B) y : B)
have h₃ : exp DR = LinearMap.rTensor B (exp D)
Tactic: have h₃ : exp DR = (exp D).rTensor B := (h_nil.map_exp (rTensorAlgHom R B B)).symm
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.GeometricallyReduced (goal)
Goal:
k : Type u_3
A : Type u_4
inst : Field k
inst_1 : Ring A
inst_2 : Algebra k A
e : (p : Ideal k) → [inst_3 : p.IsPrime] → AlgebraicClosure k ≃ₐ[k] AlgebraicClosure p.ResidueField :=
  fun (p : Ideal k) [p.IsPrime] ↦
    have this : Algebra.IsAlgebraic k p.ResidueField := ⋯;
    IsAlgClosure.equiv k (AlgebraicClosure k) (AlgebraicClosure p.ResidueField)
⊢ IsGeometricallyReduced k A ↔ IsReduced (AlgebraicClosure k ⊗[k] A)
have refine_1 : IsGeometricallyReduced k A →
  ∀ (h : ∀ (p : Ideal k) [inst_3 : p.IsPrime], IsReduced (AlgebraicClosure p.ResidueField ⊗[k] A)),
    IsReduced (AlgebraicClosure k ⊗[k] A)
Tactic: refine ⟨fun ⟨h⟩ ↦ ?_, fun h ↦ ⟨fun p hp ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.GeometricallyReduced (goal)
Goal:
k : Type u_3
A : Type u_4
inst : Field k
inst_1 : Ring A
inst_2 : Algebra k A
e : (p : Ideal k) → [inst_3 : p.IsPrime] → AlgebraicClosure k ≃ₐ[k] AlgebraicClosure p.ResidueField :=
  fun (p : Ideal k) [p.IsPrime] ↦
    have this : Algebra.IsAlgebraic k p.ResidueField := ⋯;
    IsAlgClosure.equiv k (AlgebraicClosure k) (AlgebraicClosure p.ResidueField)
refine_1 :
  IsGeometricallyReduced k A →
    ∀ (h : ∀ (p : Ideal k) [inst_3 : p.IsPrime], IsReduced (AlgebraicClosure p.ResidueField ⊗[k] A)),
      IsReduced (AlgebraicClosure k ⊗[k] A)
⊢ IsGeometricallyReduced k A ↔ IsReduced (AlgebraicClosure k ⊗[k] A)
have refine_2 : ∀ (h : IsReduced (AlgebraicClosure k ⊗[k] A)) (p : Ideal k) (hp : p.IsPrime),
  IsReduced (AlgebraicClosure p.ResidueField ⊗[k] A)
Tactic: refine ⟨fun ⟨h⟩ ↦ ?_, fun h ↦ ⟨fun p hp ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.GeometricallyReduced (hypothesis)
Goal:
k_1 : Type u_1
A_1 : Type u_2
inst : Field k_1
inst_1 : Ring A_1
inst_2 : Algebra k_1 A_1
k : Type u_3
A : Type u_4
K : Type u_5
inst_3 : Field k
inst_4 : Ring A
inst_5 : Algebra k A
inst_6 : Field K
inst_7 : Algebra k K
inst_8 : Algebra.IsAlgebraic k K
inst_9 : IsGeometricallyReduced k A
⊢ IsReduced (K ⊗[k] A)
have this : IsReduced (AlgebraicClosure k ⊗[k] A)
Tactic: have := (isGeometricallyReduced_field_iff k A).mp ‹_›
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.GeometricallyReduced (goal)
Goal:
k : Type u_1
A : Type u_2
inst : Field k
inst_1 : Ring A
inst_2 : Algebra k A
B : Type u_3
inst_3 : Ring B
inst_4 : Algebra k B
f : A →ₐ[k] B
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
inst_5 : IsGeometricallyReduced k B
⊢ IsGeometricallyReduced k A
have rw : IsReduced (AlgebraicClosure k ⊗[k] A)
Tactic: rw [isGeometricallyReduced_field_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.GeometricallyReduced (goal)
Goal:
k : Type u_1
A : Type u_2
inst : Field k
inst_1 : Ring A
inst_2 : Algebra k A
h : ∀ (B : Subalgebra k A), B.FG → IsGeometricallyReduced.{u_1, u_2} k ↥B
⊢ IsGeometricallyReduced k A
have simp_rw : ∀ (h : ∀ (B : Subalgebra k A), B.FG → IsReduced (TensorProduct.{u_1, u_1, u_2} k (AlgebraicClosure k) ↥B)),
  IsReduced (AlgebraicClosure k ⊗[k] A)
Tactic: simp_rw [isGeometricallyReduced_field_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (goal)
Goal:
R : Type u_1
S : Type u_3
F : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
inst_3 : RingHomClass F R S
f : F
hf : Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ Ideal.IsRadical (ker f) ↔ IsReduced S
have simp_rw : Ideal.IsRadical (ker f) ↔
  ∀ (x : R), (∃ (n : ℕ), Membership.mem (γ := Ideal R) (ker f) (x ^ n)) → Membership.mem (γ := Ideal R) (ker f) x
Tactic: simp_rw [isReduced_iff, hf.forall, IsNilpotent, ← map_pow, ← RingHom.mem_ker]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (goal)
Goal:
R : Type u_1
y : R
inst : CommSemiring R
⊢ IsRadical y ↔ Ideal.IsRadical (R := R) (Ideal.span {y})
have simp_rw : (∀ (n : ℕ) (x : R),
    Membership.mem (γ := Ideal R) (Ideal.span {y}) (x ^ n) → Membership.mem (γ := Ideal R) (Ideal.span {y}) x) ↔
  Ideal.IsRadical (R := R) (Ideal.span {y})
Tactic: simp_rw [IsRadical, ← Ideal.mem_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (goal)
Goal:
R : Type u_1
inst : CommSemiring R
x : R
⊢ IsNilpotent x ↔ ∀ (J : Ideal R), J.IsPrime → x ∈ J
have rw : (∀ (p : Submodule R R), Membership.mem (γ := Set (Submodule R R)) {J : Ideal R | J.IsPrime} p → x ∈ p) ↔
  ∀ (J : Ideal R), J.IsPrime → x ∈ J
Tactic: rw [← mem_nilradical, nilradical_eq_sInf, Submodule.mem_sInf]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (goal)
Goal:
R : Type u_3
inst : CommSemiring R
⊢ Eq (α := Ideal R) (nilradical R) ⊥ ↔ IsReduced R
have simp_rw : LE.le (α := Ideal R) (nilradical R) ⊥ ↔ IsReduced R
Tactic: simp_rw [eq_bot_iff, SetLike.le_def, Submodule.mem_bot, mem_nilradical, isReduced_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (goal)
Goal:
R : Type u_3
inst : CommSemiring R
simp_rw : LE.le (α := Ideal R) (nilradical R) ⊥ ↔ IsReduced R
⊢ Eq (α := Ideal R) (nilradical R) ⊥ ↔ IsReduced R
have simp_rw₁ : (∀ ⦃x : R⦄, Membership.mem (γ := Ideal R) (nilradical R) x → Membership.mem (γ := Ideal R) ⊥ x) ↔ IsReduced R
Tactic: simp_rw [eq_bot_iff, SetLike.le_def, Submodule.mem_bot, mem_nilradical, isReduced_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (goal)
Goal:
R : Type u_3
inst : CommSemiring R
simp_rw : LE.le (α := Ideal R) (nilradical R) ⊥ ↔ IsReduced R
simp_rw₁ : (∀ ⦃x : R⦄, Membership.mem (γ := Ideal R) (nilradical R) x → Membership.mem (γ := Ideal R) ⊥ x) ↔ IsReduced R
⊢ Eq (α := Ideal R) (nilradical R) ⊥ ↔ IsReduced R
have simp_rw₂ : (∀ ⦃x : R⦄, Membership.mem (γ := Ideal R) (nilradical R) x → x = 0) ↔ IsReduced R
Tactic: simp_rw [eq_bot_iff, SetLike.le_def, Submodule.mem_bot, mem_nilradical, isReduced_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (goal)
Goal:
R : Type u_3
inst : CommSemiring R
simp_rw : LE.le (α := Ideal R) (nilradical R) ⊥ ↔ IsReduced R
simp_rw₁ : (∀ ⦃x : R⦄, Membership.mem (γ := Ideal R) (nilradical R) x → Membership.mem (γ := Ideal R) ⊥ x) ↔ IsReduced R
simp_rw₂ : (∀ ⦃x : R⦄, Membership.mem (γ := Ideal R) (nilradical R) x → x = 0) ↔ IsReduced R
⊢ Eq (α := Ideal R) (nilradical R) ⊥ ↔ IsReduced R
have simp_rw₃ : (∀ ⦃x : R⦄, IsNilpotent x → x = 0) ↔ IsReduced R
Tactic: simp_rw [eq_bot_iff, SetLike.le_def, Submodule.mem_bot, mem_nilradical, isReduced_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (goal)
Goal:
R : Type u_1
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a : A
⊢ IsNilpotent (R := A →ₗ[R] A) (mulLeft R a) ↔ IsNilpotent a
have mp : IsNilpotent (R := A →ₗ[R] A) (mulLeft R a) → IsNilpotent a
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (goal)
Goal:
R : Type u_1
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a : A
mp : IsNilpotent (R := A →ₗ[R] A) (mulLeft R a) → IsNilpotent a
⊢ IsNilpotent (R := A →ₗ[R] A) (mulLeft R a) ↔ IsNilpotent a
have mpr : IsNilpotent a → IsNilpotent (R := A →ₗ[R] A) (mulLeft R a)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (goal)
Goal:
R : Type u_1
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a : A
n : ℕ
hn : HPow.hPow (α := A →ₗ[R] A) (mulLeft R a) n = 0
⊢ IsNilpotent a
have h : a ^ n = 0
Tactic: use n
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (goal)
Goal:
R : Type u_1
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ IsNilpotent (R := A →ₗ[R] A) (mulLeft R a)
have h : HPow.hPow (α := A →ₗ[R] A) (mulLeft R a) n = 0
Tactic: use n
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (goal)
Goal:
R : Type u_1
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a : A
⊢ IsNilpotent (R := A →ₗ[R] A) (mulRight R a) ↔ IsNilpotent a
have mp : IsNilpotent (R := A →ₗ[R] A) (mulRight R a) → IsNilpotent a
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (goal)
Goal:
R : Type u_1
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a : A
mp : IsNilpotent (R := A →ₗ[R] A) (mulRight R a) → IsNilpotent a
⊢ IsNilpotent (R := A →ₗ[R] A) (mulRight R a) ↔ IsNilpotent a
have mpr : IsNilpotent a → IsNilpotent (R := A →ₗ[R] A) (mulRight R a)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (goal)
Goal:
R : Type u_1
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a : A
n : ℕ
hn : HPow.hPow (α := A →ₗ[R] A) (mulRight R a) n = 0
⊢ IsNilpotent a
have h : a ^ n = 0
Tactic: use n
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (goal)
Goal:
R : Type u_1
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ IsNilpotent (R := A →ₗ[R] A) (mulRight R a)
have h : HPow.hPow (α := A →ₗ[R] A) (mulRight R a) n = 0
Tactic: use n
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (goal)
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_3
M : Type u_4
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommMonoid M
inst_4 : Module R M
b : Basis ι R M
f : M →ₗ[R] M
⊢ IsNilpotent (R := Matrix ι ι R) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) f : Matrix ι ι R) ↔ IsNilpotent f
have refine : ∀ (k : ℕ),
  HPow.hPow (α := Matrix ι ι R) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) f : Matrix ι ι R) k = 0 ↔ f ^ k = 0
Tactic: refine exists_congr fun k ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (goal)
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_3
M : Type u_4
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommMonoid M
inst_4 : Module R M
b : Basis ι R M
f : M →ₗ[R] M
k : ℕ
⊢ HPow.hPow (α := Matrix ι ι R) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) f : Matrix ι ι R) k = 0 ↔ f ^ k = 0
have rw : Eq (α := Matrix ι ι R) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) (f ^ k) : Matrix ι ι R) (0 : Matrix ι ι R) ↔
  f ^ k = 0
Tactic: rw [toMatrix_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (hypothesis)
Goal:
R : Type u_1
ι : Type u_3
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : CommSemiring R
A : Matrix ι ι R
⊢ IsNilpotent (R := (ι → R) →ₗ[R] ι → R) ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A : (ι → R) →ₗ[R] ι → R) ↔
    IsNilpotent A
have this : (LinearMap.toMatrix (Pi.basisFun R ι) (Pi.basisFun R ι) : (a : (ι → R) →ₗ[R] ι → R) → Matrix ι ι R)
    ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A) =
  A
Tactic: have : A.toLin'.toMatrix (Pi.basisFun R ι) (Pi.basisFun R ι) = A := LinearMap.toMatrix'_toLin' A
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (goal)
Goal:
R : Type u_1
ι : Type u_3
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : CommSemiring R
A : Matrix ι ι R
this :
  (LinearMap.toMatrix (Pi.basisFun R ι) (Pi.basisFun R ι) : (a : (ι → R) →ₗ[R] ι → R) → Matrix ι ι R)
      ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A) =
    A
| IsNilpotent A
have rw : IsNilpotent (R := Matrix ι ι R)
  ((LinearMap.toMatrix (Pi.basisFun R ι) (Pi.basisFun R ι) : (a : (ι → R) →ₗ[R] ι → R) → Matrix ι ι R)
      ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A) :
    Matrix ι ι R)
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (goal)
Goal:
R : Type u_1
ι : Type u_3
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : CommSemiring R
A : Matrix ι ι R
this :
  (LinearMap.toMatrix (Pi.basisFun R ι) (Pi.basisFun R ι) : (a : (ι → R) →ₗ[R] ι → R) → Matrix ι ι R)
      ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A) =
    A
⊢ IsNilpotent (R := (ι → R) →ₗ[R] ι → R) ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A : (ι → R) →ₗ[R] ι → R) ↔
    IsNilpotent A
have conv_rhs : IsNilpotent (R := (ι → R) →ₗ[R] ι → R) ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A : (ι → R) →ₗ[R] ι → R) ↔
  IsNilpotent (R := Matrix ι ι R)
    ((LinearMap.toMatrix (Pi.basisFun R ι) (Pi.basisFun R ι) : (a : (ι → R) →ₗ[R] ι → R) → Matrix ι ι R)
        ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A) :
      Matrix ι ι R)
Tactic: conv_rhs => rw [← this]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (goal)
Goal:
R : Type u_1
ι : Type u_3
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : CommSemiring R
A : Matrix ι ι R
this :
  (LinearMap.toMatrix (Pi.basisFun R ι) (Pi.basisFun R ι) : (a : (ι → R) →ₗ[R] ι → R) → Matrix ι ι R)
      ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A) =
    A
⊢ IsNilpotent (R := (ι → R) →ₗ[R] ι → R) ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A : (ι → R) →ₗ[R] ι → R) ↔
    IsNilpotent (R := Matrix ι ι R)
      ((LinearMap.toMatrix (Pi.basisFun R ι) (Pi.basisFun R ι) : (a : (ι → R) →ₗ[R] ι → R) → Matrix ι ι R)
          ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A) :
        Matrix ι ι R)
have rw : IsNilpotent (R := (ι → R) →ₗ[R] ι → R) ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A : (ι → R) →ₗ[R] ι → R) ↔
  IsNilpotent (R := (ι → R) →ₗ[R] ι → R) ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A : (ι → R) →ₗ[R] ι → R)
Tactic: rw [LinearMap.isNilpotent_toMatrix_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
hq : MapsTo (⇑f : (a : M) → M) (↑q : Set M) (↑q : Set M)
h : p ≤ q
hf : IsNilpotent (LinearMap.restrict f hq)
⊢ IsNilpotent (LinearMap.restrict f hp)
have obtain : ∀ (n : ℕ) (hn : LinearMap.restrict f hq ^ n = 0), IsNilpotent (LinearMap.restrict f hp)
Tactic: obtain ⟨n, hn⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
hq : MapsTo (⇑f : (a : M) → M) (↑q : Set M) (↑q : Set M)
h : p ≤ q
n : ℕ
hn : LinearMap.restrict f hq ^ n = 0
⊢ IsNilpotent (LinearMap.restrict f hp)
have h₁ : LinearMap.restrict f hp ^ n = 0
Tactic: use n
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
hq : MapsTo (⇑f : (a : M) → M) (↑q : Set M) (↑q : Set M)
h : p ≤ q
n : ℕ
hn : LinearMap.restrict f hq ^ n = 0
⊢ LinearMap.restrict f hp ^ n = 0
have h₁ : ∀ (x : M) (hx : x ∈ p),
  Eq.{u_3 + 1} (α := M)
    (↑((LinearMap.restrict f hp ^ n : (a : ↥p) → ↥p) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx)) : M)
    (↑((0 : (a : ↥p) → ↥p) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx)) : M)
Tactic: ext ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (hypothesis)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
hq : MapsTo (⇑f : (a : M) → M) (↑q : Set M) (↑q : Set M)
h : p ≤ q
n : ℕ
hn : LinearMap.restrict f hq ^ n = 0
x : M
hx : x ∈ p
⊢ Eq.{u_3 + 1} (α := M)
    (↑((LinearMap.restrict f hp ^ n : (a : ↥p) → ↥p) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx)) : M)
    (↑((0 : (a : ↥p) → ↥p) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx)) : M)
have hn₁ : Eq (α := ↥q) ((LinearMap.restrict f hq ^ n : (a : ↥q) → ↥q) (Subtype.mk (p := fun (x : M) ↦ x ∈ q) x sorry) : ↥q)
  ((0 : (a : ↥q) → ↥q) (Subtype.mk (p := fun (x : M) ↦ x ∈ q) x sorry) : ↥q)
Tactic: replace hn := DFunLike.congr_fun hn ⟨x, h hx⟩
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
hq : MapsTo (⇑f : (a : M) → M) (↑q : Set M) (↑q : Set M)
h : p ≤ q
n : ℕ
x : M
hx : x ∈ p
hn :
  Eq (α := ↥q) ((LinearMap.restrict f hq ^ n : (a : ↥q) → ↥q) (Subtype.mk (p := fun (x : M) ↦ x ∈ q) x ⋯) : ↥q)
    ((0 : (a : ↥q) → ↥q) (Subtype.mk (p := fun (x : M) ↦ x ∈ q) x ⋯) : ↥q)
⊢ Eq.{u_3 + 1} (α := M)
    (↑((LinearMap.restrict f hp ^ n : (a : ↥p) → ↥p) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx)) : M)
    (↑((0 : (a : ↥p) → ↥p) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx)) : M)
have h₁ : Eq (α := ↥p) ((LinearMap.restrict f hp ^ n : (a : ↥p) → ↥p) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx) : ↥p) (0 : ↥p)
Tactic: simp_rw [LinearMap.zero_apply, ZeroMemClass.coe_zero, ZeroMemClass.coe_eq_zero] at hn ⊢
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
hq : MapsTo (⇑f : (a : M) → M) (↑q : Set M) (↑q : Set M)
h : p ≤ q
n : ℕ
x : M
hx : x ∈ p
hn :
  Eq (α := ↥q) ((LinearMap.restrict f hq ^ n : (a : ↥q) → ↥q) (Subtype.mk (p := fun (x : M) ↦ x ∈ q) x ⋯) : ↥q) (0 : ↥q)
⊢ Eq (α := ↥p) ((LinearMap.restrict f hp ^ n : (a : ↥p) → ↥p) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx) : ↥p)
    (0 : ↥p)
have h₁ : ∀
  (hn :
    Eq (α := ↥q)
      (Subtype.mk (p := fun (x : M) ↦ x ∈ q) ((f ^ n : (a : M) → M) (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ q) x sorry) : M))
          sorry :
        ↥q)
      (0 : ↥q)),
  Eq (α := ↥p)
    (Subtype.mk (p := fun (x : M) ↦ x ∈ p) ((f ^ n : (a : M) → M) (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx) : M))
        sorry :
      ↥p)
    (0 : ↥p)
Tactic: rw [Module.End.pow_restrict, LinearMap.restrict_apply] at hn ⊢
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
hq : MapsTo (⇑f : (a : M) → M) (↑q : Set M) (↑q : Set M)
h : p ≤ q
n : ℕ
x : M
hx : x ∈ p
hn :
  Eq (α := ↥q)
    (Subtype.mk (p := fun (x : M) ↦ x ∈ q) ((f ^ n : (a : M) → M) (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ q) x ⋯) : M))
        ⋯ :
      ↥q)
    (0 : ↥q)
⊢ Eq (α := ↥p)
    (Subtype.mk (p := fun (x : M) ↦ x ∈ p) ((f ^ n : (a : M) → M) (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx) : M))
        ⋯ :
      ↥p)
    (0 : ↥p)
have h₁ : Eq (α := M)
  ((↑(Subtype.mk (p := fun (x : M) ↦ x ∈ p) ((f ^ n : (a : M) → M) (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx) : M))
          sorry) :
      M) :
    M)
  ((↑0 : M) : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : M →ₗ[R] M
p : Submodule R M
hf : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
hnil : IsNilpotent f
⊢ IsNilpotent (f.restrict hf)
have obtain : ∀ (n : ℕ) (hn : f ^ n = 0), IsNilpotent (f.restrict hf)
Tactic: obtain ⟨n, hn⟩ := hnil
Cleared hypotheses: hnil
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : M →ₗ[R] M
p : Submodule R M
hf : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
n : ℕ
hn : f ^ n = 0
m : ↥p
⊢ Eq (α := ↥p) ((f.restrict hf ^ n : (a : ↥p) → ↥p) m : ↥p) ((0 : (a : ↥p) → ↥p) m : ↥p)
have simp : Eq (α := ↥p) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) 0 sorry : ↥p) (0 : ↥p)
Tactic: simp only [Module.End.pow_restrict n, hn,
    LinearMap.restrict_apply, LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (goal)
Goal:
R : Type u_1
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
p : Submodule R M
hp : p ≤ Submodule.comap f p
hnp : IsNilpotent f
⊢ IsNilpotent (p.mapQ p f hp)
have obtain : ∀ (k : ℕ) (hk : f ^ k = 0), IsNilpotent (p.mapQ p f hp)
Tactic: obtain ⟨k, hk⟩ := hnp
Cleared hypotheses: hnp
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Lemmas (goal)
Goal:
R : Type u_1
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
p : Submodule R M
hp : p ≤ Submodule.comap f p
k : ℕ
hk : f ^ k = 0
⊢ IsNilpotent (p.mapQ p f hp)
have h : p.mapQ p f hp ^ k = 0
Tactic: use k