awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nilpotent (goal)
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)
⊢ Eq (α := M) ((f ^ S.sup g : (a : M) → M) m : M) ((0 : (a : M) → M) m : M)
have 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)
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
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Matrix ι ι R
⊢ IsNilpotent Aᵀ ↔ IsNilpotent A
have simp_rw : (∃ (n : ℕ), Aᵀ ^ n = 0) ↔ ∃ (n : ℕ), A ^ n = 0
Tactic: simp_rw [IsNilpotent, ← transpose_pow, transpose_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nilpotent (goal)
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
⊢ IsNilpotent Aᵀ ↔ IsNilpotent A
have simp_rw₁ : (∃ (n : ℕ), (A ^ n)ᵀ = 0) ↔ ∃ (n : ℕ), A ^ n = 0
Tactic: simp_rw [IsNilpotent, ← transpose_pow, transpose_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Matrix ι ι R
⊢ IsNilpotent A ↔ ∀ (v : ι → R), ∃ (n : ℕ), A ^ n *ᵥ v = 0
have 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
Tactic: simp_rw [← isNilpotent_toLin'_iff, Module.End.isNilpotent_iff_of_finite, ← toLin'_pow,
    toLin'_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nilpotent (goal)
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
⊢ IsNilpotent A ↔ ∀ (v : ι → R), ∃ (n : ℕ), A ^ n *ᵥ v = 0
have 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
Tactic: simp_rw [← isNilpotent_toLin'_iff, Module.End.isNilpotent_iff_of_finite, ← toLin'_pow,
    toLin'_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nilpotent (goal)
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
⊢ IsNilpotent A ↔ ∀ (v : ι → R), ∃ (n : ℕ), A ^ n *ᵥ v = 0
have 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
Tactic: simp_rw [← isNilpotent_toLin'_iff, Module.End.isNilpotent_iff_of_finite, ← toLin'_pow,
    toLin'_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Matrix ι ι R
⊢ IsNilpotent A ↔ ∀ (i : ι), ∃ (n : ℕ), (A ^ n).row i = 0
have rw : (∀ (v : ι → R), ∃ (n : ℕ), Aᵀ ^ n *ᵥ v = 0) ↔ ∀ (i : ι), ∃ (n : ℕ), (A ^ n).row i = 0
Tactic: rw [← isNilpotent_transpose_iff, isNilpotent_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nilpotent (goal)
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
have refine_1 : ∀ (h : ∀ (v : ι → R), ∃ (n : ℕ), Aᵀ ^ n *ᵥ v = 0) (i : ι), ∃ (n : ℕ), (A ^ n).row i = 0
Tactic: refine ⟨fun h i ↦ ?_, fun h v ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nilpotent (goal)
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
⊢ (∀ (v : ι → R), ∃ (n : ℕ), Aᵀ ^ n *ᵥ v = 0) ↔ ∀ (i : ι), ∃ (n : ℕ), (A ^ n).row i = 0
have refine_2 : ∀ (h : ∀ (i : ι), ∃ (n : ℕ), (A ^ n).row i = 0) (v : ι → R), ∃ (n : ℕ), Aᵀ ^ n *ᵥ v = 0
Tactic: refine ⟨fun h i ↦ ?_, fun h v ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nilpotent (goal)
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 : ℕ), (A ^ n).row i = 0
have refine_1 : ∀ (n : ℕ) (hn : Aᵀ ^ n *ᵥ Pi.single (M := fun (a : ι) ↦ R) i 1 = 0), ∃ (n : ℕ), (A ^ n).row i = 0
Tactic: obtain ⟨n, hn⟩ := h (Pi.single i 1)
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nilpotent (goal)
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
⊢ ∃ (n : ℕ), Aᵀ ^ n *ᵥ v = 0
have refine_2 : ∀ (n : (i : ι) → ℕ) (hn : ∀ (i : ι), (A ^ n i).row i = 0), ∃ (n : ℕ), Aᵀ ^ n *ᵥ v = 0
Tactic: choose n hn using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nilpotent (goal)
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
⊢ ∃ (n : ℕ), Aᵀ ^ n *ᵥ v = 0
have refine_2 : ∀ (i : ι), HPow.hPow (β := ℕ) A (⨆ (j : ι), n j) i = 0
Tactic: suffices ∀ i, (A ^ ⨆ j, n j) i = 0 from ⟨⨆ j, n j, by simp [mulVec_eq_sum, this]⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Matrix ι ι R
⊢ IsNilpotent A ↔ ∀ (i : ι), ∃ (n : ℕ), (A ^ n).col i = 0
have rw : (∀ (i : ι), ∃ (n : ℕ), (Aᵀ ^ n).row i = 0) ↔ ∀ (i : ι), ∃ (n : ℕ), (A ^ n).col i = 0
Tactic: rw [← isNilpotent_transpose_iff, isNilpotent_iff_forall_row]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Matrix ι ι R
⊢ (∀ (i : ι), ∃ (n : ℕ), (Aᵀ ^ n).row i = 0) ↔ ∀ (i : ι), ∃ (n : ℕ), (A ^ n).col i = 0
have simp_rw : (∀ (i : ι), ∃ (n : ℕ), (A ^ n)ᵀ.row i = 0) ↔ ∀ (i : ι), ∃ (n : ℕ), (A ^ n).col i = 0
Tactic: simp_rw [← transpose_pow, row_transpose]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.NilpotentKer (hypothesis)
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 R S
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.NilpotentKer (goal)
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)
this : Module.Finite.{u_1, u_2} R (HasQuotient.Quotient S (B := Ideal S) (RingHom.ker f))
⊢ Module.Finite R S
have generalize : ∀ (I : Ideal S) (hI : RingHom.ker f = I) (hf₂ : I ≤ nilradical S) (hf₃ : I.FG)
  (this : Module.Finite.{u_1, u_2} R (S ⧸ I)), Module.Finite R S
Tactic: generalize hI : RingHom.ker f = I at *
Cleared hypotheses: hf₂, hf₃, this
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.NilpotentKer (goal)
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)
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this_1 : Module.Finite.{u_1, u_2} R (S ⧸ I)
this : ∀ (i : ℕ), Module.Finite.{u_1, u_2} R (S ⧸ I ^ i)
⊢ Module.Finite R S
have obtain : ∀ (n : ℕ) (hn : I ^ n = ⊥), Module.Finite R S
Tactic: obtain ⟨n, hn : _ = ⊥⟩ := hf₃.isNilpotent_iff_le_nilradical.mpr hf₂
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.NilpotentKer (goal)
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)
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this : Module.Finite.{u_1, u_2} R (S ⧸ I)
⊢ Module.Finite R S
have suffices : ∀ (i : ℕ), Module.Finite.{u_1, u_2} R (S ⧸ I ^ i)
Tactic: suffices ∀ i, Module.Finite R (S ⧸ I ^ i) by
    obtain ⟨n, hn : _ = ⊥⟩ := hf₃.isNilpotent_iff_le_nilradical.mpr hf₂
    let e : (S ⧸ I ^ n) ≃ₐ[R] S := hn ▸ (AlgEquiv.quotientBot R S)
    exact .of_surjective e.toLinearMap e.surjective
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.NilpotentKer (goal)
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)
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this : Module.Finite.{u_1, u_2} R (S ⧸ I)
⊢ Module.Finite.{u_1, u_2} R (S ⧸ HPow.hPow (β := ℕ) I 0)
have zero : Module.Finite.{u_1, u_2} R (HasQuotient.Quotient S (B := Ideal S) ⊤)
Tactic: rw [pow_zero, Ideal.one_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.NilpotentKer (hypothesis)
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)
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this : Module.Finite.{u_1, u_2} R (S ⧸ I)
n : ℕ
IH : Module.Finite.{u_1, u_2} R (S ⧸ I ^ n)
φ : S ⧸ I ^ (n + 1) →ₐ[S] S ⧸ I ^ n := Ideal.Quotient.factorₐ S ⋯
⊢ Module.Finite.{u_1, u_2} R (S ⧸ I ^ (n + 1))
have hφ : Function.Surjective (α := S ⧸ I ^ (n + 1)) (β := S ⧸ I ^ n) (⇑φ : (a : S ⧸ I ^ (n + 1)) → S ⧸ I ^ n)
Tactic: have hφ : Function.Surjective φ :=
      Ideal.Quotient.factor_surjective (Ideal.pow_le_pow_right n.le_succ)
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.NilpotentKer (hypothesis)
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)
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this : Module.Finite.{u_1, u_2} R (S ⧸ I)
n : ℕ
IH : Module.Finite.{u_1, u_2} R (S ⧸ I ^ n)
φ : S ⧸ I ^ (n + 1) →ₐ[S] S ⧸ I ^ n := Ideal.Quotient.factorₐ S ⋯
hφ : Function.Surjective (α := S ⧸ I ^ (n + 1)) (β := S ⧸ I ^ n) (⇑φ : (a : S ⧸ I ^ (n + 1)) → S ⧸ I ^ n)
⊢ Module.Finite.{u_1, u_2} R (S ⧸ I ^ (n + 1))
have hφ' : φ.toLinearMap ∘ₗ Submodule.mkQ (I ^ (n + 1)) = Submodule.mkQ (I ^ n)
Tactic: have hφ' : φ.toLinearMap ∘ₗ (I ^ (n + 1)).mkQ = (I ^ n).mkQ := rfl
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.NilpotentKer (goal)
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)
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this : Module.Finite.{u_1, u_2} R (S ⧸ I)
n : ℕ
IH : Module.Finite.{u_1, u_2} R (S ⧸ I ^ n)
φ : S ⧸ I ^ (n + 1) →ₐ[S] S ⧸ I ^ n := Ideal.Quotient.factorₐ S ⋯
hφ : Function.Surjective (α := S ⧸ I ^ (n + 1)) (β := S ⧸ I ^ n) (⇑φ : (a : S ⧸ I ^ (n + 1)) → S ⧸ I ^ n)
hφ' : φ.toLinearMap ∘ₗ Submodule.mkQ (I ^ (n + 1)) = Submodule.mkQ (I ^ n)
⊢ Module.Finite.{u_1, u_2} R (S ⧸ I ^ (n + 1))
have succ : Submodule.FG
  (Submodule.map
    ((↑R :
        {S M M₂ : Type u_2} →
          [inst : Semiring R] →
            [inst_6 : Semiring S] →
              [inst_7 : AddCommMonoid M] →
                [inst_8 : AddCommMonoid M₂] →
                  [inst_9 : Module R M] →
                    [inst_10 : Module R M₂] →
                      [inst_11 : Module S M] →
                        [inst_12 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      φ.toLinearMap)
    ⊤)
Tactic: refine ⟨Submodule.fg_of_fg_map_of_fg_inf_ker (φ.toLinearMap.restrictScalars R) ?_ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.NilpotentKer (goal)
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)
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this : Module.Finite.{u_1, u_2} R (S ⧸ I)
n : ℕ
IH : Module.Finite.{u_1, u_2} R (S ⧸ I ^ n)
φ : S ⧸ I ^ (n + 1) →ₐ[S] S ⧸ I ^ n := Ideal.Quotient.factorₐ S ⋯
hφ : Function.Surjective (α := S ⧸ I ^ (n + 1)) (β := S ⧸ I ^ n) (⇑φ : (a : S ⧸ I ^ (n + 1)) → S ⧸ I ^ n)
hφ' : φ.toLinearMap ∘ₗ Submodule.mkQ (I ^ (n + 1)) = Submodule.mkQ (I ^ n)
succ :
  Submodule.FG
    (Submodule.map
      ((↑R :
          {S M M₂ : Type u_2} →
            [inst : Semiring R] →
              [inst_6 : Semiring S] →
                [inst_7 : AddCommMonoid M] →
                  [inst_8 : AddCommMonoid M₂] →
                    [inst_9 : Module R M] →
                      [inst_10 : Module R M₂] →
                        [inst_11 : Module S M] →
                          [inst_12 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        φ.toLinearMap)
      ⊤)
⊢ Module.Finite.{u_1, u_2} R (S ⧸ I ^ (n + 1))
have succ₁ : Submodule.FG
  (⊤ ⊓
    LinearMap.ker
      ((↑R :
          {S M M₂ : Type u_2} →
            [inst : Semiring R] →
              [inst_6 : Semiring S] →
                [inst_7 : AddCommMonoid M] →
                  [inst_8 : AddCommMonoid M₂] →
                    [inst_9 : Module R M] →
                      [inst_10 : Module R M₂] →
                        [inst_11 : Module S M] →
                          [inst_12 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        φ.toLinearMap))
Tactic: refine ⟨Submodule.fg_of_fg_map_of_fg_inf_ker (φ.toLinearMap.restrictScalars R) ?_ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.NilpotentKer (hypothesis)
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)
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this : Module.Finite.{u_1, u_2} R (S ⧸ I)
n : ℕ
IH : Module.Finite.{u_1, u_2} R (S ⧸ I ^ n)
φ : S ⧸ I ^ (n + 1) →ₐ[S] S ⧸ I ^ n := Ideal.Quotient.factorₐ S ⋯
hφ : Function.Surjective (α := S ⧸ I ^ (n + 1)) (β := S ⧸ I ^ n) (⇑φ : (a : S ⧸ I ^ (n + 1)) → S ⧸ I ^ n)
hφ' : φ.toLinearMap ∘ₗ Submodule.mkQ (I ^ (n + 1)) = Submodule.mkQ (I ^ n)
⊢ Module.Finite.{u_1, u_2} R ((S ⧸ I) ⊗[S] ↥(I ^ n))
have this₁ : Module.Finite S ↥(I ^ n)
Tactic: have : Module.Finite S ↑(I ^ n) := .of_fg (.pow hf₃ _)
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.NilpotentKer (hypothesis)
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)
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this : Module.Finite.{u_1, u_2} R (S ⧸ I)
n : ℕ
IH : Module.Finite.{u_1, u_2} R (S ⧸ I ^ n)
φ : S ⧸ I ^ (n + 1) →ₐ[S] S ⧸ I ^ n := Ideal.Quotient.factorₐ S ⋯
hφ : Function.Surjective (α := S ⧸ I ^ (n + 1)) (β := S ⧸ I ^ n) (⇑φ : (a : S ⧸ I ^ (n + 1)) → S ⧸ I ^ n)
hφ' : φ.toLinearMap ∘ₗ Submodule.mkQ (I ^ (n + 1)) = Submodule.mkQ (I ^ n)
⊢ Submodule.FG
    (⊤ ⊓
      LinearMap.ker
        ((↑R :
            {S M M₂ : Type u_2} →
              [inst : Semiring R] →
                [inst_6 : Semiring S] →
                  [inst_7 : AddCommMonoid M] →
                    [inst_8 : AddCommMonoid M₂] →
                      [inst_9 : Module R M] →
                        [inst_10 : Module R M₂] →
                          [inst_11 : Module S M] →
                            [inst_12 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          φ.toLinearMap))
have this₁ : Module.Finite.{u_1, u_2} R ((S ⧸ I) ⊗[S] ↥(I ^ n))
Tactic: have : Module.Finite R ((S ⧸ I) ⊗[S] ↑(I ^ n)) := by
        have : Module.Finite S ↑(I ^ n) := .of_fg (.pow hf₃ _)
        exact .trans (S ⧸ I) _
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.NilpotentKer (goal)
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)
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this_1 : Module.Finite.{u_1, u_2} R (S ⧸ I)
n : ℕ
IH : Module.Finite.{u_1, u_2} R (S ⧸ I ^ n)
φ : S ⧸ I ^ (n + 1) →ₐ[S] S ⧸ I ^ n := Ideal.Quotient.factorₐ S ⋯
hφ : Function.Surjective (α := S ⧸ I ^ (n + 1)) (β := S ⧸ I ^ n) (⇑φ : (a : S ⧸ I ^ (n + 1)) → S ⧸ I ^ n)
hφ' : φ.toLinearMap ∘ₗ Submodule.mkQ (I ^ (n + 1)) = Submodule.mkQ (I ^ n)
this : Module.Finite.{u_1, u_2} R ((S ⧸ I) ⊗[S] ↥(I ^ n))
⊢ (S ⧸ I) ⊗[S] ↥(I ^ n) →ₗ[S] S ⧸ I ^ (n + 1)
have refine : ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule S ↥(I ^ n)) I ⊤ →ₗ[S] S ⧸ I ^ (n + 1)
Tactic: refine ?_ ∘ₗ (TensorProduct.quotTensorEquivQuotSMul _ I).toLinearMap
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.NilpotentKer (goal)
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)
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this_1 : Module.Finite.{u_1, u_2} R (S ⧸ I)
n : ℕ
IH : Module.Finite.{u_1, u_2} R (S ⧸ I ^ n)
φ : S ⧸ I ^ (n + 1) →ₐ[S] S ⧸ I ^ n := Ideal.Quotient.factorₐ S ⋯
hφ : Function.Surjective (α := S ⧸ I ^ (n + 1)) (β := S ⧸ I ^ n) (⇑φ : (a : S ⧸ I ^ (n + 1)) → S ⧸ I ^ n)
hφ' : φ.toLinearMap ∘ₗ Submodule.mkQ (I ^ (n + 1)) = Submodule.mkQ (I ^ n)
this : Module.Finite.{u_1, u_2} R ((S ⧸ I) ⊗[S] ↥(I ^ n))
⊢ ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule S ↥(I ^ n)) I ⊤ →ₗ[S] S ⧸ I ^ (n + 1)
have refine : HSMul.hSMul (β := Submodule S ↥(I ^ n)) I ⊤ ≤
  LinearMap.ker (M₂ := S ⧸ I ^ (n + 1)) (Submodule.mkQ (I ^ (n + 1)) ∘ₗ Submodule.subtype (I ^ n))
Tactic: refine Submodule.liftQ _ ((Submodule.mkQ _).comp (I ^ n).subtype) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.NilpotentKer (goal)
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)
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this_1 : Module.Finite.{u_1, u_2} R (S ⧸ I)
n : ℕ
IH : Module.Finite.{u_1, u_2} R (S ⧸ I ^ n)
φ : S ⧸ I ^ (n + 1) →ₐ[S] S ⧸ I ^ n := Ideal.Quotient.factorₐ S ⋯
hφ : Function.Surjective (α := S ⧸ I ^ (n + 1)) (β := S ⧸ I ^ n) (⇑φ : (a : S ⧸ I ^ (n + 1)) → S ⧸ I ^ n)
hφ' : φ.toLinearMap ∘ₗ Submodule.mkQ (I ^ (n + 1)) = Submodule.mkQ (I ^ n)
this : Module.Finite.{u_1, u_2} R ((S ⧸ I) ⊗[S] ↥(I ^ n))
⊢ HSMul.hSMul (β := Submodule S ↥(I ^ n)) I ⊤ ≤
    LinearMap.ker (M₂ := S ⧸ I ^ (n + 1)) (Submodule.mkQ (I ^ (n + 1)) ∘ₗ Submodule.subtype (I ^ n))
have rw : I • Submodule.map (Submodule.subtype (I ^ n)) ⊤ ≤
  (Submodule.subtype (I ^ n)).range ⊓
    LinearMap.ker (R₂ := S) (M₂ := S ⧸ I ^ (n + 1)) (τ₁₂ := RingHom.id S) (Submodule.mkQ (I ^ (n + 1)))
Tactic: rw [LinearMap.ker_comp, ← Submodule.map_le_map_iff_of_injective (I ^ n).subtype_injective,
          Submodule.map_smul'', Submodule.map_comap_eq]