awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Nilpotent.GeometricallyReduced
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)
refine_2 :
  ∀ (h : IsReduced (AlgebraicClosure k ⊗[k] A)) (p : Ideal k) (hp : p.IsPrime),
    IsReduced (AlgebraicClosure p.ResidueField ⊗[k] A)
⊢ IsGeometricallyReduced k A ↔ IsReduced (AlgebraicClosure k ⊗[k] A)

Tactic:
refine ⟨fun ⟨h⟩ ↦ ?_, fun h ↦ ⟨fun p hp ↦ ?_⟩⟩
-- Module: Mathlib.RingTheory.Nilpotent.GeometricallyReduced
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)
h_1 : IsGeometricallyReduced k A
h : ∀ (p : Ideal k) [inst_3 : p.IsPrime], IsReduced (AlgebraicClosure p.ResidueField ⊗[k] A)
⊢ IsReduced (AlgebraicClosure k ⊗[k] A)

Tactic:
isReduced_of_injective _ (Algebra.TensorProduct.congr (e ⊥) AlgEquiv.refl).injective

Premises used: isReduced_of_injective, Bot.bot, AlgEquiv.injective, Algebra.TensorProduct.congr, AlgEquiv.refl
-- Module: Mathlib.RingTheory.Nilpotent.GeometricallyReduced
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)
h_1 : IsGeometricallyReduced k A
h : ∀ (p : Ideal k) [inst_3 : p.IsPrime], IsReduced (AlgebraicClosure p.ResidueField ⊗[k] A)
⊢ IsReduced (AlgebraicClosure k ⊗[k] A)

Tactic:
exact isReduced_of_injective _ (Algebra.TensorProduct.congr (e ⊥) AlgEquiv.refl).injective

Premises used: isReduced_of_injective, Bot.bot, AlgEquiv.injective, Algebra.TensorProduct.congr, AlgEquiv.refl
-- Module: Mathlib.RingTheory.Nilpotent.GeometricallyReduced
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)
h : IsReduced (AlgebraicClosure k ⊗[k] A)
p : Ideal k
hp : p.IsPrime
⊢ IsReduced (AlgebraicClosure p.ResidueField ⊗[k] A)

Tactic:
isReduced_of_injective _ (Algebra.TensorProduct.congr (e p).symm AlgEquiv.refl).injective

Premises used: isReduced_of_injective, AlgEquiv.symm, AlgEquiv.injective, Algebra.TensorProduct.congr, AlgEquiv.refl
-- Module: Mathlib.RingTheory.Nilpotent.GeometricallyReduced
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)
h : IsReduced (AlgebraicClosure k ⊗[k] A)
p : Ideal k
hp : p.IsPrime
⊢ IsReduced (AlgebraicClosure p.ResidueField ⊗[k] A)

Tactic:
exact isReduced_of_injective _ (Algebra.TensorProduct.congr (e p).symm AlgEquiv.refl).injective

Premises used: isReduced_of_injective, AlgEquiv.symm, AlgEquiv.injective, Algebra.TensorProduct.congr, AlgEquiv.refl
-- Module: Mathlib.RingTheory.Nilpotent.GeometricallyReduced
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 (AlgebraicClosure k ⊗[k] A)

Tactic:
have := (isGeometricallyReduced_field_iff k A).mp ‹_›
-- Module: Mathlib.RingTheory.Nilpotent.GeometricallyReduced
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
this : IsReduced (AlgebraicClosure k ⊗[k] A)
⊢ IsReduced (K ⊗[k] A)

Tactic:
isReduced_of_injective
    (Algebra.TensorProduct.map ((IsAlgClosed.lift : K →ₐ[k] AlgebraicClosure k)) 1)
    (Module.Flat.rTensor_preserves_injective_linearMap _ (RingHom.injective _))

Premises used: isReduced_of_injective, Algebra.TensorProduct.map, RingHom.injective, IsAlgClosed.lift, OfNat.ofNat, Module.Flat.rTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.Nilpotent.GeometricallyReduced
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
this : IsReduced (AlgebraicClosure k ⊗[k] A)
⊢ IsReduced (K ⊗[k] A)

Tactic:
exact isReduced_of_injective
    (Algebra.TensorProduct.map ((IsAlgClosed.lift : K →ₐ[k] AlgebraicClosure k)) 1)
    (Module.Flat.rTensor_preserves_injective_linearMap _ (RingHom.injective _))

Premises used: isReduced_of_injective, Algebra.TensorProduct.map, RingHom.injective, IsAlgClosed.lift, OfNat.ofNat, Module.Flat.rTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.Nilpotent.GeometricallyReduced
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
rw : IsReduced (AlgebraicClosure k ⊗[k] A)
⊢ IsGeometricallyReduced k A

Tactic:
rw [isGeometricallyReduced_field_iff]

Premises used: Algebra.isGeometricallyReduced_field_iff
-- Module: Mathlib.RingTheory.Nilpotent.GeometricallyReduced
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
⊢ IsReduced (AlgebraicClosure k ⊗[k] A)

Tactic:
isReduced_of_injective (Algebra.TensorProduct.map 1 f)
    (Module.Flat.lTensor_preserves_injective_linearMap _ hf)

Premises used: isReduced_of_injective, Module.Flat.lTensor_preserves_injective_linearMap, Algebra.TensorProduct.map, OfNat.ofNat
-- Module: Mathlib.RingTheory.Nilpotent.GeometricallyReduced
Goal:
k : Type u_1
A : Type u_2
inst : Field k
inst_1 : Ring A
inst_2 : Algebra k A
inst_3 : IsGeometricallyReduced k A
⊢ IsReduced A

Tactic:
isReduced_of_injective
    (Algebra.TensorProduct.includeRight : A →ₐ[k] (AlgebraicClosure k) ⊗[k] A)
    (Algebra.TensorProduct.includeRight_injective (RingHom.injective _))

Premises used: isReduced_of_injective, Algebra.TensorProduct.includeRight_injective, RingHom.injective, Algebra.TensorProduct.includeRight
-- Module: Mathlib.RingTheory.Nilpotent.GeometricallyReduced
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
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)
⊢ IsGeometricallyReduced k A

Tactic:
simp_rw [isGeometricallyReduced_field_iff] at h ⊢

Premises used: Algebra.isGeometricallyReduced_field_iff
-- Module: Mathlib.RingTheory.Nilpotent.GeometricallyReduced
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 → IsReduced (TensorProduct.{u_1, u_1, u_2} k (AlgebraicClosure k) ↥B)
⊢ IsReduced (AlgebraicClosure k ⊗[k] A)

Tactic:
IsReduced.tensorProduct_of_flat_of_forall_fg h

Premises used: IsReduced.tensorProduct_of_flat_of_forall_fg
-- Module: Mathlib.RingTheory.Nilpotent.GeometricallyReduced
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 → IsReduced (TensorProduct.{u_1, u_1, u_2} k (AlgebraicClosure k) ↥B)
⊢ IsReduced (AlgebraicClosure k ⊗[k] A)

Tactic:
exact IsReduced.tensorProduct_of_flat_of_forall_fg h

Premises used: IsReduced.tensorProduct_of_flat_of_forall_fg
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
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)
simp_rw :
  Ideal.IsRadical (ker f) ↔
    ∀ (x : R), (∃ (n : ℕ), Membership.mem (γ := Ideal R) (ker f) (x ^ n)) → Membership.mem (γ := Ideal R) (ker f) x
⊢ Ideal.IsRadical (ker f) ↔ IsReduced S

Tactic:
simp_rw [isReduced_iff, hf.forall, IsNilpotent, ← map_pow, ← RingHom.mem_ker]

Premises used: Function.Surjective.forall, isReduced_iff, RingHom.mem_ker, map_pow, IsNilpotent
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
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) ↔
    ∀ (x : R), (∃ (n : ℕ), Membership.mem (γ := Ideal R) (ker f) (x ^ n)) → Membership.mem (γ := Ideal R) (ker f) x

Tactic:
rfl
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
Goal:
R : Type u_1
y : R
inst : CommSemiring R
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})
⊢ IsRadical y ↔ Ideal.IsRadical (R := R) (Ideal.span {y})

Tactic:
simp_rw [IsRadical, ← Ideal.mem_span_singleton]

Premises used: IsRadical, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
Goal:
R : Type u_1
y : R
inst : CommSemiring R
⊢ (∀ (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:
forall_comm.trans (forall_congr' fun r => exists_imp.symm)

Premises used: forall_comm, forall_congr', Iff.trans, exists_imp, Iff.symm
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
Goal:
R : Type u_1
y : R
inst : CommSemiring R
⊢ (∀ (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:
exact forall_comm.trans (forall_congr' fun r => exists_imp.symm)

Premises used: forall_comm, forall_congr', Iff.trans, exists_imp, Iff.symm
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
Goal:
R : Type u_1
inst : Monoid R
inst_1 : Zero R
x : R
⊢ IsNilpotent x ↔ Membership.mem (γ := Submonoid R) (Submonoid.powers x) 0

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.range, IsNilpotent
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
Goal:
R : Type u_1
inst : CommSemiring R
x : R
⊢ Membership.mem (γ := Ideal R) (nilradical R) x ↔ IsNilpotent x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.singleton, IsNilpotent
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
Goal:
R : Type u_3
inst : CommSemiring R
⊢ Eq.{u_3 + 1} (α := Ideal R) (sInf {J : Ideal R | ⊥ ≤ J ∧ J.IsPrime}) (sInf {J : Ideal R | J.IsPrime})

Tactic:
simp_rw [and_iff_right bot_le]

Premises used: and_iff_right, bot_le
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
Goal:
R : Type u_1
inst : CommSemiring R
x : R
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
⊢ IsNilpotent x ↔ ∀ (J : Ideal R), J.IsPrime → x ∈ J

Tactic:
rw [← mem_nilradical, nilradical_eq_sInf, Submodule.mem_sInf]

Premises used: Submodule.mem_sInf, nilradical_eq_sInf, mem_nilradical
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
Goal:
R : Type u_1
inst : CommSemiring R
x : R
⊢ (∀ (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:
rfl
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
Goal:
R : Type u_1
inst : CommSemiring R
J : Ideal R
H : J.IsPrime
⊢ nilradical R ≤ J

Tactic:
(nilradical_eq_sInf R).symm ▸ sInf_le H

Premises used: Eq.rec, sInf_le, nilradical_eq_sInf, Eq.symm
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
Goal:
R : Type u_3
inst : CommSemiring R
inst_1 : IsReduced R
⊢ Eq (α := Ideal R) (nilradical R) 0

Tactic:
Ideal.ext fun _ => isNilpotent_iff_eq_zero

Premises used: isNilpotent_iff_eq_zero, Ideal.ext
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
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
simp_rw₃ : (∀ ⦃x : R⦄, IsNilpotent x → x = 0) ↔ IsReduced R
⊢ Eq (α := Ideal R) (nilradical R) ⊥ ↔ IsReduced R

Tactic:
simp_rw [eq_bot_iff, SetLike.le_def, Submodule.mem_bot, mem_nilradical, isReduced_iff]

Premises used: Submodule.mem_bot, isReduced_iff, SetLike.le_def, eq_bot_iff, mem_nilradical
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
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
mpr : IsNilpotent a → IsNilpotent (R := A →ₗ[R] A) (mulLeft R a)
⊢ IsNilpotent (R := A →ₗ[R] A) (mulLeft R a) ↔ IsNilpotent a

Tactic:
constructor
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
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
h : a ^ n = 0
⊢ IsNilpotent a

Tactic:
use n
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
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
h : HPow.hPow (α := A →ₗ[R] A) (mulLeft R a) n = 0
⊢ IsNilpotent (R := A →ₗ[R] A) (mulLeft R a)

Tactic:
use n
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
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
⊢ a ^ n = 0

Tactic:
simp only [mulLeft_eq_zero_iff, pow_mulLeft] at hn ⊢

Premises used: LinearMap.mulLeft_eq_zero_iff, LinearMap.pow_mulLeft
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
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
h : a ^ n = 0
⊢ HPow.hPow (α := A →ₗ[R] A) (mulLeft R a) n = 0

Tactic:
simp only [mulLeft_eq_zero_iff, pow_mulLeft] at hn ⊢

Premises used: LinearMap.mulLeft_eq_zero_iff, LinearMap.pow_mulLeft
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
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
⊢ a ^ n = 0

Tactic:
hn
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
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
⊢ a ^ n = 0

Tactic:
exact hn
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
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
mpr : IsNilpotent a → IsNilpotent (R := A →ₗ[R] A) (mulRight R a)
⊢ IsNilpotent (R := A →ₗ[R] A) (mulRight R a) ↔ IsNilpotent a

Tactic:
constructor
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
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
h : a ^ n = 0
⊢ IsNilpotent a

Tactic:
use n
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
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
h : HPow.hPow (α := A →ₗ[R] A) (mulRight R a) n = 0
⊢ IsNilpotent (R := A →ₗ[R] A) (mulRight R a)

Tactic:
use n
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
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
⊢ a ^ n = 0

Tactic:
simp only [mulRight_eq_zero_iff, pow_mulRight] at hn ⊢

Premises used: LinearMap.pow_mulRight, LinearMap.mulRight_eq_zero_iff
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
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
h : a ^ n = 0
⊢ HPow.hPow (α := A →ₗ[R] A) (mulRight R a) n = 0

Tactic:
simp only [mulRight_eq_zero_iff, pow_mulRight] at hn ⊢

Premises used: LinearMap.pow_mulRight, LinearMap.mulRight_eq_zero_iff
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
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

Tactic:
exists_congr fun k ↦ ?_

Premises used: exists_congr, IsNilpotent
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
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
refine :
  ∀ (k : ℕ),
    HPow.hPow (α := Matrix ι ι R) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) f : Matrix ι ι R) k = 0 ↔ f ^ k = 0
⊢ IsNilpotent (R := Matrix ι ι R) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) f : Matrix ι ι R) ↔ IsNilpotent f

Tactic:
refine exists_congr fun k ↦ ?_

Premises used: exists_congr
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
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 : ℕ
rw :
  Eq (α := Matrix ι ι R) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) (f ^ k) : Matrix ι ι R) (0 : Matrix ι ι R) ↔
    f ^ k = 0
⊢ HPow.hPow (α := Matrix ι ι R) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) f : Matrix ι ι R) k = 0 ↔ f ^ k = 0

Tactic:
rw [toMatrix_pow]

Premises used: LinearMap.toMatrix_pow
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
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 : ℕ
⊢ Eq (α := Matrix ι ι R) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) (f ^ k) : Matrix ι ι R) (0 : Matrix ι ι R) ↔
    f ^ k = 0

Tactic:
(toMatrix b b).map_eq_zero_iff

Premises used: LinearEquiv.map_eq_zero_iff, LinearMap.toMatrix
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
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 : ℕ
⊢ Eq (α := Matrix ι ι R) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) (f ^ k) : Matrix ι ι R) (0 : Matrix ι ι R) ↔
    f ^ k = 0

Tactic:
exact (toMatrix b b).map_eq_zero_iff

Premises used: LinearEquiv.map_eq_zero_iff, LinearMap.toMatrix
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
Goal:
R : Type u_1
ι : Type u_3
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : CommSemiring R
A : Matrix ι ι R
⊢ (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
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
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
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)
| IsNilpotent A

Tactic:
rw [← this]
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
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
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)
⊢ IsNilpotent (R := (ι → R) →ₗ[R] ι → R) ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A : (ι → R) →ₗ[R] ι → R) ↔
    IsNilpotent A

Tactic:
conv_rhs => rw [← this]
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
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
rw 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)
⊢ 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:
rw [LinearMap.isNilpotent_toMatrix_iff]

Premises used: LinearMap.isNilpotent_toMatrix_iff
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
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)
obtain : ∀ (n : ℕ) (hn : LinearMap.restrict f hq ^ n = 0), IsNilpotent (LinearMap.restrict f hp)
⊢ IsNilpotent (LinearMap.restrict f hp)

Tactic:
obtain ⟨n, hn⟩ := hf
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
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
h₁ : LinearMap.restrict f hp ^ n = 0
⊢ IsNilpotent (LinearMap.restrict f hp)

Tactic:
use n