awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
s_1 : Set M
i : M
s : Set M
h : i ∉ s
hs_1 : s.Finite
ih :
  ∀
    (H :
      ∃ (r : R),
        r - 1 ∈ I ∧
          N ≤
              comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)
                (HSMul.hSMul (β := Submodule R M) I (span R s)) ∧
            s ⊆ (↑N : Set M)),
    ∃ (r : R), r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ (↑N : Set M) ∧ s ⊆ (↑N : Set M)
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
n : M
hn : n ∈ N
y : M
hy : y ∈ HSMul.hSMul (β := Submodule R M) I (R ∙ i)
z : M
hz : z ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
hyz : y + z = r • n
insert :
  ∀ (hy : ∃ y_1 ∈ I, y_1 • i = y) (z : M) (hz : z ∈ HSMul.hSMul (β := Submodule R M) I (span R s))
    (hyz : y + z = r • n),
    Membership.mem (γ := Submodule R M)
      (comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) (c * r))
        (HSMul.hSMul (β := Submodule R M) I (span R s)))
      n
⊢ Membership.mem (γ := Submodule R M)
    (comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) (c * r))
      (HSMul.hSMul (β := Submodule R M) I (span R s)))
    n

Tactic:
rw [mem_smul_span_singleton] at hy

Premises used: Submodule.mem_smul_span_singleton
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
s_1 : Set M
i : M
s : Set M
h : i ∉ s
hs_1 : s.Finite
ih :
  ∀
    (H :
      ∃ (r : R),
        r - 1 ∈ I ∧
          N ≤
              comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)
                (HSMul.hSMul (β := Submodule R M) I (span R s)) ∧
            s ⊆ (↑N : Set M)),
    ∃ (r : R), r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ (↑N : Set M) ∧ s ⊆ (↑N : Set M)
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
n : M
hn : n ∈ N
y : M
hy : ∃ y_1 ∈ I, y_1 • i = y
z : M
hz : z ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
hyz : y + z = r • n
insert :
  ∀ d ∈ I,
    ∀ (hyz : d • i + z = r • n),
      Membership.mem (γ := Submodule R M)
        (comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) (c * r))
          (HSMul.hSMul (β := Submodule R M) I (span R s)))
        n
⊢ Membership.mem (γ := Submodule R M)
    (comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) (c * r))
      (HSMul.hSMul (β := Submodule R M) I (span R s)))
    n

Tactic:
rcases hy with ⟨d, _, rfl⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
s_1 : Set M
i : M
s : Set M
h : i ∉ s
hs_1 : s.Finite
ih :
  ∀
    (H :
      ∃ (r : R),
        r - 1 ∈ I ∧
          N ≤
              comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)
                (HSMul.hSMul (β := Submodule R M) I (span R s)) ∧
            s ⊆ (↑N : Set M)),
    ∃ (r : R), r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ (↑N : Set M) ∧ s ⊆ (↑N : Set M)
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
n : M
hn : n ∈ N
z : M
hz : z ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
d : R
left : d ∈ I
hyz : d • i + z = r • n
insert : (c * r) • n ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
⊢ Membership.mem (γ := Submodule R M)
    (comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) (c * r))
      (HSMul.hSMul (β := Submodule R M) I (span R s)))
    n

Tactic:
simp only [mem_comap, LinearMap.lsmul_apply]

Premises used: Submodule.mem_comap, LinearMap.lsmul_apply
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
s_1 : Set M
i : M
s : Set M
h : i ∉ s
hs_1 : s.Finite
ih :
  ∀
    (H :
      ∃ (r : R),
        r - 1 ∈ I ∧
          N ≤
              comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)
                (HSMul.hSMul (β := Submodule R M) I (span R s)) ∧
            s ⊆ (↑N : Set M)),
    ∃ (r : R), r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ (↑N : Set M) ∧ s ⊆ (↑N : Set M)
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
n : M
hn : n ∈ N
z : M
hz : z ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
d : R
left : d ∈ I
hyz : d • i + z = r • n
insert : d • c • i + c • z ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
⊢ (c * r) • n ∈ HSMul.hSMul (β := Submodule R M) I (span R s)

Tactic:
rw [mul_smul, ← hyz, smul_add, smul_smul, mul_comm, mul_smul]

Premises used: smul_smul, mul_comm, SemigroupAction.mul_smul, smul_add
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
s_1 : Set M
i : M
s : Set M
h : i ∉ s
hs_1 : s.Finite
ih :
  ∀
    (H :
      ∃ (r : R),
        r - 1 ∈ I ∧
          N ≤
              comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)
                (HSMul.hSMul (β := Submodule R M) I (span R s)) ∧
            s ⊆ (↑N : Set M)),
    ∃ (r : R), r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ (↑N : Set M) ∧ s ⊆ (↑N : Set M)
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
n : M
hn : n ∈ N
z : M
hz : z ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
d : R
left : d ∈ I
hyz : d • i + z = r • n
⊢ d • c • i + c • z ∈ HSMul.hSMul (β := Submodule R M) I (span R s)

Tactic:
add_mem (smul_mem _ _ hci) (smul_mem _ _ hz)

Premises used: AddMemClass.add_mem, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
s_1 : Set M
i : M
s : Set M
h : i ∉ s
hs_1 : s.Finite
ih :
  ∀
    (H :
      ∃ (r : R),
        r - 1 ∈ I ∧
          N ≤
              comap (σ₁₂ := RingHom.id R) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r)
                (HSMul.hSMul (β := Submodule R M) I (span R s)) ∧
            s ⊆ (↑N : Set M)),
    ∃ (r : R), r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ (↑N : Set M) ∧ s ⊆ (↑N : Set M)
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
n : M
hn : n ∈ N
z : M
hz : z ∈ HSMul.hSMul (β := Submodule R M) I (span R s)
d : R
left : d ∈ I
hyz : d • i + z = r • n
⊢ d • c • i + c • z ∈ HSMul.hSMul (β := Submodule R M) I (span R s)

Tactic:
exact add_mem (smul_mem _ _ hci) (smul_mem _ _ hz)

Premises used: AddMemClass.add_mem, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
hn : N.FG
hin : N ≤ I • N
obtain : ∀ (r : R) (hr : r - 1 ∈ I) (hr' : ∀ n ∈ N, r • n = 0), ∃ r ∈ I, ∀ n ∈ N, r • n = n
⊢ ∃ r ∈ I, ∀ n ∈ N, r • n = n

Tactic:
obtain ⟨r, hr, hr'⟩ := exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul I N hn hin

Premises used: Submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
hn_1 : N.FG
hin : N ≤ I • N
r : R
hr : r - 1 ∈ I
hr' : ∀ n ∈ N, r • n = 0
n : M
hn : n ∈ N
⊢ -(r - 1) • n = n

Tactic:
simpa [sub_smul] using hr' n hn

Premises used: sub_smul
-- Module: Mathlib.RingTheory.Finiteness.Nakayama
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
hn : N.FG
hin : N ≤ I • N
r : R
hr : r - 1 ∈ I
hr' : ∀ n ∈ N, r • n = 0
⊢ ∃ r ∈ I, ∀ n ∈ N, r • n = n

Tactic:
exact ⟨-(r - 1), I.neg_mem hr, fun n hn => by simpa [sub_smul] using hr' n hn⟩
-- Module: Mathlib.RingTheory.Finiteness.Nilpotent
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Finite R M
f : End R M
h : IsNilpotent f
m : M
n : ℕ
hn : f ^ n = 0
⊢ Eq (α := M) ((f ^ n : (a : M) → M) m : M) (0 : M)

Tactic:
simp [hn]
-- Module: Mathlib.RingTheory.Finiteness.Nilpotent
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Finite R M
f : End R M
refine : ∀ (h : ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((f ^ n : (a : M) → M) m : M) (0 : M)), IsNilpotent f
⊢ IsNilpotent f ↔ ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((f ^ n : (a : M) → M) m : M) (0 : M)

Tactic:
refine ⟨fun ⟨n, hn⟩ m ↦ ⟨n, by simp [hn]⟩, fun h ↦ ?_⟩
-- Module: Mathlib.RingTheory.Finiteness.Nilpotent
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Finite R M
f : End R M
h : ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((f ^ n : (a : M) → M) m : M) (0 : M)
rcases : ∀ (S : Finset M) (hS : Eq (α := Submodule R M) (Submodule.span R (↑S : Set M)) ⊤), IsNilpotent f
⊢ IsNilpotent f

Tactic:
rcases Module.Finite.fg_top (R := R) (M := M) with ⟨S, hS⟩

Premises used: Module.Finite.fg_top
-- Module: Mathlib.RingTheory.Finiteness.Nilpotent
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Finite R M
f : End R M
h : ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((f ^ n : (a : M) → M) m : M) (0 : M)
S : Finset M
hS : Eq (α := Submodule R M) (Submodule.span R (↑S : Set M)) ⊤
choose : ∀ (g : (m : M) → ℕ) (hg : ∀ (m : M), Eq (α := M) ((f ^ g m : (a : M) → M) m : M) (0 : M)), IsNilpotent f
⊢ IsNilpotent f

Tactic:
choose g hg using h
-- Module: Mathlib.RingTheory.Finiteness.Nilpotent
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Finite R M
f : End R M
S : Finset M
hS : Eq (α := Submodule R M) (Submodule.span R (↑S : Set M)) ⊤
g : (m : M) → ℕ
hg : ∀ (m : M), Eq (α := M) ((f ^ g m : (a : M) → M) m : M) (0 : M)
h : f ^ S.sup g = 0
⊢ IsNilpotent f

Tactic:
use Finset.sup S g

Premises used: Finset.sup
-- Module: Mathlib.RingTheory.Finiteness.Nilpotent
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Finite R M
f : End R M
S : Finset M
hS : Eq (α := Submodule R M) (Submodule.span R (↑S : Set M)) ⊤
g : (m : M) → ℕ
hg : ∀ (m : M), Eq (α := M) ((f ^ g m : (a : M) → M) m : M) (0 : M)
h : ∀ (m : M), Eq (α := M) ((f ^ S.sup g : (a : M) → M) m : M) ((0 : (a : M) → M) m : M)
⊢ f ^ S.sup g = 0

Tactic:
ext m
-- Module: Mathlib.RingTheory.Finiteness.Nilpotent
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Finite R M
f : End R M
S : Finset M
hS : Eq (α := Submodule R M) (Submodule.span R (↑S : Set M)) ⊤
g : (m : M) → ℕ
hg : ∀ (m : M), Eq (α := M) ((f ^ g m : (a : M) → M) m : M) (0 : M)
m : M
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R (↑S : Set M)) m

Tactic:
simp [hS]
-- Module: Mathlib.RingTheory.Finiteness.Nilpotent
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Finite R M
f : End R M
S : Finset M
hS : Eq (α := Submodule R M) (Submodule.span R (↑S : Set M)) ⊤
g : (m : M) → ℕ
hg : ∀ (m : M), Eq (α := M) ((f ^ g m : (a : M) → M) m : M) (0 : M)
m : M
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R (↑S : Set M)) m

Tactic:
have hm : m ∈ Submodule.span R S := by simp [hS]
-- Module: Mathlib.RingTheory.Finiteness.Nilpotent
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Finite R M
f : End R M
S : Finset M
hS : Eq (α := Submodule R M) (Submodule.span R (↑S : Set M)) ⊤
g : (m : M) → ℕ
hg : ∀ (m : M), Eq (α := M) ((f ^ g m : (a : M) → M) m : M) (0 : M)
m x : M
hx : x ∈ (↑S : Set M)
⊢ Eq (α := M) ((f ^ S.sup g : (a : M) → M) x : M) ((0 : (a : M) → M) x : M)

Tactic:
pow_map_zero_of_le (Finset.le_sup hx) (hg x)

Premises used: Module.End.pow_map_zero_of_le, Finset.le_sup
-- Module: Mathlib.RingTheory.Finiteness.Nilpotent
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Finite R M
f : End R M
S : Finset M
hS : Eq (α := Submodule R M) (Submodule.span R (↑S : Set M)) ⊤
g : (m : M) → ℕ
hg : ∀ (m : M), Eq (α := M) ((f ^ g m : (a : M) → M) m : M) (0 : M)
m x : M
hx : x ∈ (↑S : Set M)
⊢ Eq (α := M) ((f ^ S.sup g : (a : M) → M) x : M) ((0 : (a : M) → M) x : M)

Tactic:
exact pow_map_zero_of_le (Finset.le_sup hx) (hg x)

Premises used: Module.End.pow_map_zero_of_le, Finset.le_sup
-- Module: Mathlib.RingTheory.Finiteness.Nilpotent
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Finite R M
f : End R M
S : Finset M
hS : Eq (α := Submodule R M) (Submodule.span R (↑S : Set M)) ⊤
g : (m : M) → ℕ
hg : ∀ (m : M), Eq (α := M) ((f ^ g m : (a : M) → M) m : M) (0 : M)
m : M
⊢ Eq (α := M) ((f ^ S.sup g : (a : M) → M) 0 : M) ((0 : (a : M) → M) 0 : M)

Tactic:
simp
-- Module: Mathlib.RingTheory.Finiteness.Nilpotent
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Finite R M
f : End R M
S : Finset M
hS : Eq (α := Submodule R M) (Submodule.span R (↑S : Set M)) ⊤
g : (m : M) → ℕ
hg : ∀ (m : M), Eq (α := M) ((f ^ g m : (a : M) → M) m : M) (0 : M)
m x y : M
hx : Membership.mem (γ := Submodule R M) (Submodule.span R (↑S : Set M)) x
hy : Membership.mem (γ := Submodule R M) (Submodule.span R (↑S : Set M)) y
h : Eq (α := M) ((f ^ S.sup g : (a : M) → M) x : M) ((0 : (a : M) → M) x : M)
h_1 : Eq (α := M) ((f ^ S.sup g : (a : M) → M) y : M) ((0 : (a : M) → M) y : M)
⊢ Eq (α := M) ((f ^ S.sup g : (a : M) → M) (x + y) : M) ((0 : (a : M) → M) (x + y) : M)

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Finiteness.Nilpotent
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Finite R M
f : End R M
S : Finset M
hS : Eq (α := Submodule R M) (Submodule.span R (↑S : Set M)) ⊤
g : (m : M) → ℕ
hg : ∀ (m : M), Eq (α := M) ((f ^ g m : (a : M) → M) m : M) (0 : M)
m : M
a : R
x : M
hx : Membership.mem (γ := Submodule R M) (Submodule.span R (↑S : Set M)) x
h : Eq (α := M) ((f ^ S.sup g : (a : M) → M) x : M) ((0 : (a : M) → M) x : M)
⊢ Eq (α := M) ((f ^ S.sup g : (a : M) → M) (a • x) : M) ((0 : (a : M) → M) (a • x) : M)

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Finiteness.Nilpotent
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Finite R M
f : End R M
S : Finset M
hS : Eq (α := Submodule R M) (Submodule.span R (↑S : Set M)) ⊤
g : (m : M) → ℕ
hg : ∀ (m : M), Eq (α := M) ((f ^ g m : (a : M) → M) m : M) (0 : M)
m : M
hm : Membership.mem (γ := Submodule R M) (Submodule.span R (↑S : Set M)) m
h : ∀ (x : M) (hx : x ∈ (↑S : Set M)), Eq (α := M) ((f ^ S.sup g : (a : M) → M) x : M) ((0 : (a : M) → M) x : M)
h₁ : Eq (α := M) ((f ^ S.sup g : (a : M) → M) 0 : M) ((0 : (a : M) → M) 0 : M)
h₂ :
  ∀ (x y : M),
    Membership.mem (γ := Submodule R M) (Submodule.span R (↑S : Set M)) x →
      Membership.mem (γ := Submodule R M) (Submodule.span R (↑S : Set M)) y →
        Eq (α := M) ((f ^ S.sup g : (a : M) → M) x : M) ((0 : (a : M) → M) x : M) →
          Eq (α := M) ((f ^ S.sup g : (a : M) → M) y : M) ((0 : (a : M) → M) y : M) →
            Eq (α := M) ((f ^ S.sup g : (a : M) → M) (x + y) : M) ((0 : (a : M) → M) (x + y) : M)
h₃ :
  ∀ (a : R) (x : M),
    Membership.mem (γ := Submodule R M) (Submodule.span R (↑S : Set M)) x →
      Eq (α := M) ((f ^ S.sup g : (a : M) → M) x : M) ((0 : (a : M) → M) x : M) →
        Eq (α := M) ((f ^ S.sup g : (a : M) → M) (a • x) : M) ((0 : (a : M) → M) (a • x) : M)
⊢ Eq (α := M) ((f ^ S.sup g : (a : M) → M) m : M) ((0 : (a : M) → M) m : M)

Tactic:
induction hm using Submodule.span_induction with
  | mem x hx => exact pow_map_zero_of_le (Finset.le_sup hx) (hg x)
  | zero => simp
  | add => simp_all
  | smul => simp_all
-- Module: Mathlib.RingTheory.Finiteness.Nilpotent
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Matrix ι ι R
simp_rw : (∃ (n : ℕ), Aᵀ ^ n = 0) ↔ ∃ (n : ℕ), A ^ n = 0
simp_rw₁ : (∃ (n : ℕ), (A ^ n)ᵀ = 0) ↔ ∃ (n : ℕ), A ^ n = 0
⊢ IsNilpotent Aᵀ ↔ IsNilpotent A

Tactic:
simp_rw [IsNilpotent, ← transpose_pow, transpose_eq_zero]

Premises used: Matrix.transpose_pow, Matrix.transpose_eq_zero, IsNilpotent
-- Module: Mathlib.RingTheory.Finiteness.Nilpotent
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Matrix ι ι R
simp_rw :
  IsNilpotent (R := (ι → R) →ₗ[R] ι → R) ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A : (ι → R) →ₗ[R] ι → R) ↔
    ∀ (v : ι → R), ∃ (n : ℕ), A ^ n *ᵥ v = 0
simp_rw₁ :
  (∀ (m : ι → R),
      ∃ (n : ℕ),
        Eq (α := ι → R)
          ((HPow.hPow (α := Module.End R (ι → R))
                  ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A : (ι → R) →ₗ[R] ι → R) n :
                (a : ι → R) → ι → R)
              m :
            ι → R)
          (0 : ι → R)) ↔
    ∀ (v : ι → R), ∃ (n : ℕ), A ^ n *ᵥ v = 0
simp_rw₂ :
  (∀ (m : ι → R),
      ∃ (n : ℕ),
        Eq (α := ι → R)
          ((((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) (A ^ n) : (ι → R) →ₗ[R] ι → R) : (a : ι → R) → ι → R)
              m :
            ι → R)
          (0 : ι → R)) ↔
    ∀ (v : ι → R), ∃ (n : ℕ), A ^ n *ᵥ v = 0
⊢ IsNilpotent A ↔ ∀ (v : ι → R), ∃ (n : ℕ), A ^ n *ᵥ v = 0

Tactic:
simp_rw [← isNilpotent_toLin'_iff, Module.End.isNilpotent_iff_of_finite, ← toLin'_pow,
    toLin'_apply]

Premises used: Matrix.isNilpotent_toLin'_iff, Module.End.isNilpotent_iff_of_finite, Matrix.toLin'_pow, Matrix.toLin'_apply
-- Module: Mathlib.RingTheory.Finiteness.Nilpotent
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Matrix ι ι R
rw : (∀ (v : ι → R), ∃ (n : ℕ), Aᵀ ^ n *ᵥ v = 0) ↔ ∀ (i : ι), ∃ (n : ℕ), (A ^ n).row i = 0
⊢ IsNilpotent A ↔ ∀ (i : ι), ∃ (n : ℕ), (A ^ n).row i = 0

Tactic:
rw [← isNilpotent_transpose_iff, isNilpotent_iff]

Premises used: Matrix.isNilpotent_transpose_iff, Matrix.isNilpotent_iff
-- Module: Mathlib.RingTheory.Finiteness.Nilpotent
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Matrix ι ι R
⊢ (∀ (v : ι → R), ∃ (n : ℕ), Aᵀ ^ n *ᵥ v = 0) ↔ ∀ (i : ι), ∃ (n : ℕ), (A ^ n).row i = 0

Tactic:
⟨fun h i ↦ ?_, fun h v ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.Finiteness.Nilpotent
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Matrix ι ι R
refine_1 : ∀ (h : ∀ (v : ι → R), ∃ (n : ℕ), Aᵀ ^ n *ᵥ v = 0) (i : ι), ∃ (n : ℕ), (A ^ n).row i = 0
refine_2 : ∀ (h : ∀ (i : ι), ∃ (n : ℕ), (A ^ n).row i = 0) (v : ι → R), ∃ (n : ℕ), Aᵀ ^ n *ᵥ v = 0
⊢ (∀ (v : ι → R), ∃ (n : ℕ), Aᵀ ^ n *ᵥ v = 0) ↔ ∀ (i : ι), ∃ (n : ℕ), (A ^ n).row i = 0

Tactic:
refine ⟨fun h i ↦ ?_, fun h v ↦ ?_⟩
-- Module: Mathlib.RingTheory.Finiteness.Nilpotent
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Matrix ι ι R
h : ∀ (v : ι → R), ∃ (n : ℕ), Aᵀ ^ n *ᵥ v = 0
i : ι
refine_1 : ∀ (n : ℕ) (hn : Aᵀ ^ n *ᵥ Pi.single (M := fun (a : ι) ↦ R) i 1 = 0), ∃ (n : ℕ), (A ^ n).row i = 0
⊢ ∃ (n : ℕ), (A ^ n).row i = 0

Tactic:
obtain ⟨n, hn⟩ := h (Pi.single i 1)

Premises used: Pi.single, OfNat.ofNat
-- Module: Mathlib.RingTheory.Finiteness.Nilpotent
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Matrix ι ι R
h : ∀ (v : ι → R), ∃ (n : ℕ), Aᵀ ^ n *ᵥ v = 0
i : ι
n : ℕ
hn : Aᵀ ^ n *ᵥ Pi.single (M := fun (a : ι) ↦ R) i 1 = 0
⊢ (A ^ n).row i = 0

Tactic:
simpa [← transpose_pow] using hn

Premises used: Matrix.transpose_pow
-- Module: Mathlib.RingTheory.Finiteness.Nilpotent
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Matrix ι ι R
h : ∀ (v : ι → R), ∃ (n : ℕ), Aᵀ ^ n *ᵥ v = 0
i : ι
n : ℕ
hn : Aᵀ ^ n *ᵥ Pi.single (M := fun (a : ι) ↦ R) i 1 = 0
⊢ ∃ (n : ℕ), (A ^ n).row i = 0

Tactic:
exact ⟨n, by simpa [← transpose_pow] using hn⟩
-- Module: Mathlib.RingTheory.Finiteness.Nilpotent
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Matrix ι ι R
h : ∀ (i : ι), ∃ (n : ℕ), (A ^ n).row i = 0
v : ι → R
refine_2 : ∀ (n : (i : ι) → ℕ) (hn : ∀ (i : ι), (A ^ n i).row i = 0), ∃ (n : ℕ), Aᵀ ^ n *ᵥ v = 0
⊢ ∃ (n : ℕ), Aᵀ ^ n *ᵥ v = 0

Tactic:
choose n hn using h
-- Module: Mathlib.RingTheory.Finiteness.Nilpotent
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Matrix ι ι R
v : ι → R
n : (i : ι) → ℕ
hn : ∀ (i : ι), (A ^ n i).row i = 0
this : ∀ (i : ι), HPow.hPow (β := ℕ) A (⨆ (j : ι), n j) i = 0
⊢ HPow.hPow (β := ℕ) Aᵀ (⨆ (j : ι), n j) *ᵥ v = 0

Tactic:
simp [mulVec_eq_sum, this]

Premises used: Matrix.mulVec_eq_sum
-- Module: Mathlib.RingTheory.Finiteness.Nilpotent
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Matrix ι ι R
v : ι → R
n : (i : ι) → ℕ
hn : ∀ (i : ι), (A ^ n i).row i = 0
refine_2 : ∀ (i : ι), HPow.hPow (β := ℕ) A (⨆ (j : ι), n j) i = 0
⊢ ∃ (n : ℕ), Aᵀ ^ n *ᵥ v = 0

Tactic:
suffices ∀ i, (A ^ ⨆ j, n j) i = 0 from ⟨⨆ j, n j, by simp [mulVec_eq_sum, this]⟩
-- Module: Mathlib.RingTheory.Finiteness.Nilpotent
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Matrix ι ι R
v : ι → R
n : (i : ι) → ℕ
hn : ∀ (i : ι), (A ^ n i).row i = 0
⊢ ∀ (i : ι), HPow.hPow (β := ℕ) A (⨆ (j : ι), n j) i = 0

Tactic:
fun i ↦ pow_row_eq_zero_of_le (hn i) (Finite.le_ciSup n i)

Premises used: Finite.le_ciSup, Matrix.pow_row_eq_zero_of_le, Matrix.row
-- Module: Mathlib.RingTheory.Finiteness.Nilpotent
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Matrix ι ι R
v : ι → R
n : (i : ι) → ℕ
hn : ∀ (i : ι), (A ^ n i).row i = 0
⊢ ∀ (i : ι), HPow.hPow (β := ℕ) A (⨆ (j : ι), n j) i = 0

Tactic:
exact fun i ↦ pow_row_eq_zero_of_le (hn i) (Finite.le_ciSup n i)

Premises used: Finite.le_ciSup, Matrix.pow_row_eq_zero_of_le
-- Module: Mathlib.RingTheory.Finiteness.Nilpotent
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Matrix ι ι R
rw : (∀ (i : ι), ∃ (n : ℕ), (Aᵀ ^ n).row i = 0) ↔ ∀ (i : ι), ∃ (n : ℕ), (A ^ n).col i = 0
⊢ IsNilpotent A ↔ ∀ (i : ι), ∃ (n : ℕ), (A ^ n).col i = 0

Tactic:
rw [← isNilpotent_transpose_iff, isNilpotent_iff_forall_row]

Premises used: Matrix.isNilpotent_transpose_iff, Matrix.isNilpotent_iff_forall_row
-- Module: Mathlib.RingTheory.Finiteness.Nilpotent
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Matrix ι ι R
simp_rw : (∀ (i : ι), ∃ (n : ℕ), (A ^ n)ᵀ.row i = 0) ↔ ∀ (i : ι), ∃ (n : ℕ), (A ^ n).col i = 0
⊢ (∀ (i : ι), ∃ (n : ℕ), (Aᵀ ^ n).row i = 0) ↔ ∀ (i : ι), ∃ (n : ℕ), (A ^ n).col i = 0

Tactic:
simp_rw [← transpose_pow, row_transpose]

Premises used: Matrix.row_transpose, Matrix.transpose_pow
-- Module: Mathlib.RingTheory.Finiteness.NilpotentKer
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Module.Finite R T
f : S →ₐ[R] T
hf₁ : Function.Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
hf₂ : LE.le (α := Ideal S) (RingHom.ker f) (nilradical S)
hf₃ : Ideal.FG (RingHom.ker f)
⊢ Module.Finite.{u_1, u_2} R (HasQuotient.Quotient S (B := Ideal S) (RingHom.ker f))

Tactic:
have : Module.Finite R (S ⧸ RingHom.ker f) :=
    let e := Ideal.quotientKerAlgEquivOfSurjective hf₁
    .of_surjective e.symm.toLinearMap e.symm.surjective