awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : PreSubmersivePresentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
inst_3 : Finite σ
inst_4 : Finite σ'
val : Fintype σ
val_1 : Fintype σ'
⊢ (P.reindex e f).jacobian = P.jacobian
have intro : Eq.{v + 1} (α := S)
  ((algebraMap (P.reindex e f).Ring S : (a : (P.reindex e f).Ring) → S) (P.reindex e f).jacobiMatrix.det : S)
  ((algebraMap P.Ring S : (a : P.Ring) → S) P.jacobiMatrix.det : S)
Tactic: simp_rw [PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : PreSubmersivePresentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
inst_3 : Finite σ
inst_4 : Finite σ'
val : Fintype σ
val_1 : Fintype σ'
⊢ Eq.{v + 1} (α := S)
    ((algebraMap (P.reindex e f).Ring S : (a : (P.reindex e f).Ring) → S) (P.reindex e f).jacobiMatrix.det : S)
    ((algebraMap P.Ring S : (a : P.Ring) → S) P.jacobiMatrix.det : S)
have intro : Eq.{v + 1} (α := S)
  ((aeval (P.val ∘ (⇑e : (a : ι') → ι)) : (a : MvPolynomial ι' R) → S)
      (Matrix.det (n := σ')
        (Matrix.map (P.jacobiMatrix.submatrix (⇑f : (a : σ') → σ) (⇑f : (a : σ') → σ))
          (⇑(rename (⇑e.symm : (a : ι) → ι')) : (a : MvPolynomial ι R) → MvPolynomial ι' R))) :
    S)
  ((aeval P.val : (a : MvPolynomial ι R) → S) P.jacobiMatrix.det : S)
Tactic: simp only [reindex_toPresentation, Presentation.reindex_toGenerators, jacobiMatrix_reindex,
    Matrix.reindex_apply, Equiv.symm_symm, Generators.algebraMap_apply, Generators.reindex_val]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : PreSubmersivePresentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
inst_3 : Finite σ
inst_4 : Finite σ'
val : Fintype σ
val_1 : Fintype σ'
⊢ Eq.{v + 1} (α := S)
    ((aeval (P.val ∘ (⇑e : (a : ι') → ι)) : (a : MvPolynomial ι' R) → S)
        (Matrix.det (n := σ')
          (Matrix.map (P.jacobiMatrix.submatrix (⇑f : (a : σ') → σ) (⇑f : (a : σ') → σ))
            (⇑(rename (⇑e.symm : (a : ι) → ι')) : (a : MvPolynomial ι R) → MvPolynomial ι' R))) :
      S)
    ((aeval P.val : (a : MvPolynomial ι R) → S) P.jacobiMatrix.det : S)
have intro : Eq.{v + 1} (α := S)
  (Matrix.det.{v, u_2} (n := σ')
    (Matrix.map (P.jacobiMatrix.submatrix (⇑f : (a : σ') → σ) (⇑f : (a : σ') → σ))
      (Function.comp (β := MvPolynomial ι R) (⇑(aeval P.val) : (a : MvPolynomial ι R) → S)
        (Function.comp (β := MvPolynomial ι' R)
          (⇑(rename (⇑e : (a : ι') → ι)) : (a : MvPolynomial ι' R) → MvPolynomial ι R)
          (⇑(rename (⇑e.symm : (a : ι) → ι')) : (a : P.Ring) → MvPolynomial ι' R)))))
  (Matrix.det.{v, u_2} (n := σ')
    (Matrix.map (P.jacobiMatrix.submatrix (⇑f : (a : σ') → σ) (⇑f : (a : σ') → σ))
      (⇑(aeval P.val) : (a : MvPolynomial ι R) → S)))
Tactic: simp_rw [← MvPolynomial.aeval_rename,
    ← AlgHom.mapMatrix_apply, ← Matrix.det_submatrix_equiv_self f, AlgHom.map_det,
    AlgHom.mapMatrix_apply, Matrix.map_map]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : PreSubmersivePresentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
inst_3 : Finite σ
inst_4 : Finite σ'
⊢ (P.reindex e f).jacobian = P.jacobian
have intro : ∀ (val : Fintype σ), (P.reindex e f).jacobian = P.jacobian
Tactic: classical
  cases nonempty_fintype σ
  cases nonempty_fintype σ'
  simp_rw [PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det]
  simp only [reindex_toPresentation, Presentation.reindex_toGenerators, jacobiMatrix_reindex,
    Matrix.reindex_apply, Equiv.symm_symm, Generators.algebraMap_apply, Generators.reindex_val]
  simp_rw [← MvPolynomial.aeval_rename,
    ← AlgHom.mapMatrix_apply, ← Matrix.det_submatrix_equiv_self f, AlgHom.map_det,
    AlgHom.mapMatrix_apply, Matrix.map_map]
  simp [← AlgHom.coe_comp, rename_comp_rename, rename_id]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : PreSubmersivePresentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
inst_3 : Finite σ
inst_4 : Finite σ'
intro : ∀ (val : Fintype σ), (P.reindex e f).jacobian = P.jacobian
⊢ (P.reindex e f).jacobian = P.jacobian
have intro₁ : ∀ (val : Fintype σ) (val : Fintype σ'), (P.reindex e f).jacobian = P.jacobian
Tactic: classical
  cases nonempty_fintype σ
  cases nonempty_fintype σ'
  simp_rw [PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det]
  simp only [reindex_toPresentation, Presentation.reindex_toGenerators, jacobiMatrix_reindex,
    Matrix.reindex_apply, Equiv.symm_symm, Generators.algebraMap_apply, Generators.reindex_val]
  simp_rw [← MvPolynomial.aeval_rename,
    ← AlgHom.mapMatrix_apply, ← Matrix.det_submatrix_equiv_self f, AlgHom.map_det,
    AlgHom.mapMatrix_apply, Matrix.map_map]
  simp [← AlgHom.coe_comp, rename_comp_rename, rename_id]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : PreSubmersivePresentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
inst_3 : Finite σ
inst_4 : Finite σ'
intro : ∀ (val : Fintype σ), (P.reindex e f).jacobian = P.jacobian
intro₁ : ∀ (val : Fintype σ) (val : Fintype σ'), (P.reindex e f).jacobian = P.jacobian
⊢ (P.reindex e f).jacobian = P.jacobian
have intro₂ : ∀ (val : Fintype σ) (val_1 : Fintype σ'),
  Eq.{v + 1} (α := S)
    ((algebraMap (P.reindex e f).Ring S : (a : (P.reindex e f).Ring) → S) (P.reindex e f).jacobiMatrix.det : S)
    ((algebraMap P.Ring S : (a : P.Ring) → S) P.jacobiMatrix.det : S)
Tactic: classical
  cases nonempty_fintype σ
  cases nonempty_fintype σ'
  simp_rw [PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det]
  simp only [reindex_toPresentation, Presentation.reindex_toGenerators, jacobiMatrix_reindex,
    Matrix.reindex_apply, Equiv.symm_symm, Generators.algebraMap_apply, Generators.reindex_val]
  simp_rw [← MvPolynomial.aeval_rename,
    ← AlgHom.mapMatrix_apply, ← Matrix.det_submatrix_equiv_self f, AlgHom.map_det,
    AlgHom.mapMatrix_apply, Matrix.map_map]
  simp [← AlgHom.coe_comp, rename_comp_rename, rename_id]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : PreSubmersivePresentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
inst_3 : Finite σ
inst_4 : Finite σ'
intro : ∀ (val : Fintype σ), (P.reindex e f).jacobian = P.jacobian
intro₁ : ∀ (val : Fintype σ) (val : Fintype σ'), (P.reindex e f).jacobian = P.jacobian
intro₂ :
  ∀ (val : Fintype σ) (val_1 : Fintype σ'),
    Eq.{v + 1} (α := S)
      ((algebraMap (P.reindex e f).Ring S : (a : (P.reindex e f).Ring) → S) (P.reindex e f).jacobiMatrix.det : S)
      ((algebraMap P.Ring S : (a : P.Ring) → S) P.jacobiMatrix.det : S)
⊢ (P.reindex e f).jacobian = P.jacobian
have intro₃ : ∀ (val : Fintype σ) (val_1 : Fintype σ'),
  Eq.{v + 1} (α := S)
    ((aeval (P.val ∘ (⇑e : (a : ι') → ι)) : (a : MvPolynomial ι' R) → S)
        (Matrix.det (n := σ')
          (Matrix.map (P.jacobiMatrix.submatrix (⇑f : (a : σ') → σ) (⇑f : (a : σ') → σ))
            (⇑(rename (⇑e.symm : (a : ι) → ι')) : (a : MvPolynomial ι R) → MvPolynomial ι' R))) :
      S)
    ((aeval P.val : (a : MvPolynomial ι R) → S) P.jacobiMatrix.det : S)
Tactic: classical
  cases nonempty_fintype σ
  cases nonempty_fintype σ'
  simp_rw [PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det]
  simp only [reindex_toPresentation, Presentation.reindex_toGenerators, jacobiMatrix_reindex,
    Matrix.reindex_apply, Equiv.symm_symm, Generators.algebraMap_apply, Generators.reindex_val]
  simp_rw [← MvPolynomial.aeval_rename,
    ← AlgHom.mapMatrix_apply, ← Matrix.det_submatrix_equiv_self f, AlgHom.map_det,
    AlgHom.mapMatrix_apply, Matrix.map_map]
  simp [← AlgHom.coe_comp, rename_comp_rename, rename_id]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : PreSubmersivePresentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
inst_3 : Finite σ
inst_4 : Finite σ'
intro : ∀ (val : Fintype σ), (P.reindex e f).jacobian = P.jacobian
intro₁ : ∀ (val : Fintype σ) (val : Fintype σ'), (P.reindex e f).jacobian = P.jacobian
intro₂ :
  ∀ (val : Fintype σ) (val_1 : Fintype σ'),
    Eq.{v + 1} (α := S)
      ((algebraMap (P.reindex e f).Ring S : (a : (P.reindex e f).Ring) → S) (P.reindex e f).jacobiMatrix.det : S)
      ((algebraMap P.Ring S : (a : P.Ring) → S) P.jacobiMatrix.det : S)
intro₃ :
  ∀ (val : Fintype σ) (val_1 : Fintype σ'),
    Eq.{v + 1} (α := S)
      ((aeval (P.val ∘ (⇑e : (a : ι') → ι)) : (a : MvPolynomial ι' R) → S)
          (Matrix.det (n := σ')
            (Matrix.map (P.jacobiMatrix.submatrix (⇑f : (a : σ') → σ) (⇑f : (a : σ') → σ))
              (⇑(rename (⇑e.symm : (a : ι) → ι')) : (a : MvPolynomial ι R) → MvPolynomial ι' R))) :
        S)
      ((aeval P.val : (a : MvPolynomial ι R) → S) P.jacobiMatrix.det : S)
⊢ (P.reindex e f).jacobian = P.jacobian
have intro₄ : ∀ (val : Fintype σ) (val_1 : Fintype σ'),
  Eq.{v + 1} (α := S)
    (Matrix.det.{v, u_2} (n := σ')
      (Matrix.map (P.jacobiMatrix.submatrix (⇑f : (a : σ') → σ) (⇑f : (a : σ') → σ))
        (Function.comp (β := MvPolynomial ι R) (⇑(aeval P.val) : (a : MvPolynomial ι R) → S)
          (Function.comp (β := MvPolynomial ι' R)
            (⇑(rename (⇑e : (a : ι') → ι)) : (a : MvPolynomial ι' R) → MvPolynomial ι R)
            (⇑(rename (⇑e.symm : (a : ι) → ι')) : (a : P.Ring) → MvPolynomial ι' R)))))
    (Matrix.det.{v, u_2} (n := σ')
      (Matrix.map (P.jacobiMatrix.submatrix (⇑f : (a : σ') → σ) (⇑f : (a : σ') → σ))
        (⇑(aeval P.val) : (a : MvPolynomial ι R) → S)))
Tactic: classical
  cases nonempty_fintype σ
  cases nonempty_fintype σ'
  simp_rw [PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det]
  simp only [reindex_toPresentation, Presentation.reindex_toGenerators, jacobiMatrix_reindex,
    Matrix.reindex_apply, Equiv.symm_symm, Generators.algebraMap_apply, Generators.reindex_val]
  simp_rw [← MvPolynomial.aeval_rename,
    ← AlgHom.mapMatrix_apply, ← Matrix.det_submatrix_equiv_self f, AlgHom.map_det,
    AlgHom.mapMatrix_apply, Matrix.map_map]
  simp [← AlgHom.coe_comp, rename_comp_rename, rename_id]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
h : Function.Bijective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ IsUnit (PreSubmersivePresentation.ofBijectiveAlgebraMap h).jacobian
have rw : IsUnit.{v} (M := S) 1
Tactic: rw [ofBijectiveAlgebraMap_jacobian]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
T : Type u_1
ι' : Type u_2
σ' : Type u_3
inst_4 : CommRing T
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : Finite σ'
Q : SubmersivePresentation S T ι' σ'
P : SubmersivePresentation R S ι σ
⊢ IsUnit (jacobian (Q.comp P.toPreSubmersivePresentation))
have rw : IsUnit.{u_1} (M := T) ((algebraMap S T : (a : S) → T) P.jacobian : T) ∧ IsUnit Q.jacobian
Tactic: rw [comp_jacobian_eq_jacobian_smul_jacobian, Algebra.smul_def, IsUnit.mul_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
r : R
inst_4 : IsLocalization.Away r S
⊢ IsUnit (jacobian (PreSubmersivePresentation.localizationAway S r))
have rw : IsUnit.{v} (M := S) ((algebraMap R S : (a : R) → S) r : S)
Tactic: rw [localizationAway_jacobian]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
this : Fintype σ
⊢ IsUnit.{v} (M := S)
    (Matrix.det.{v, t} (n := σ)
      ((LinearMap.toMatrix (Pi.basisFun S σ) (Pi.basisFun S σ) : (a : (σ → S) →ₗ[S] σ → S) → Matrix σ σ S)
        P.aevalDifferential))
have h : Matrix.det.{v, t} (n := σ)
    ((LinearMap.toMatrix (Pi.basisFun S σ) (Pi.basisFun S σ) : (a : (σ → S) →ₗ[S] σ → S) → Matrix σ σ S)
      P.aevalDifferential) =
  P.jacobian
Tactic: convert! P.jacobian_isUnit
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
this : Fintype σ
⊢ Matrix.det.{v, t} (n := σ)
      ((LinearMap.toMatrix (Pi.basisFun S σ) (Pi.basisFun S σ) : (a : (σ → S) →ₗ[S] σ → S) → Matrix σ σ S)
        P.aevalDifferential) =
    P.jacobian
have h : Eq.{v + 1} (α := S)
  (Matrix.det.{v, t} (n := σ)
      ((AlgHom.mapMatrix (aeval P.val) : (a : Matrix σ σ (MvPolynomial ι R)) → Matrix σ σ S) P.jacobiMatrix) :
    S)
  (((↑(aeval P.val) : MvPolynomial ι R →+* S) : (a : P.Ring) → S) P.jacobiMatrix.det : S)
Tactic: rw [LinearMap.toMatrix_eq_toMatrix', jacobian_eq_jacobiMatrix_det,
      aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix, P.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Submersive (goal)
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
⊢ LinearIndependent S (M := (j : σ) → S) fun (i j : σ) ↦
    (aeval P.val : (a : MvPolynomial ι R) → S)
      ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation i) : MvPolynomial ι R)
have simp_rw : LinearIndependent S (M := (j : σ) → S) fun (i j : σ) ↦ (P.basisDeriv : (a : σ) → σ → S) i j
Tactic: simp_rw [← SubmersivePresentation.basisDeriv_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
j n : ℕ
ih : I ^ n • F.N j ≤ F.N (n + j)
⊢ I ^ (n + 1) • F.N j ≤ F.N (n + 1 + j)
have succ : I • I ^ n • F.N j ≤ F.N (n + j + 1)
Tactic: rw [pow_succ', mul_smul, add_assoc, add_comm 1, ← add_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
i j : ℕ
⊢ I ^ i • F.N j ≤ F.N (i + j)
have zero : HPow.hPow (β := ℕ) I 0 • F.N j ≤ F.N (0 + j)
Tactic: induction i with
  | zero => simp
  | succ _ ih =>
    rw [pow_succ', mul_smul, add_assoc, add_comm 1, ← add_assoc]
    exact (smul_mono_right _ ih).trans (F.smul_le _)
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
i j : ℕ
zero : HPow.hPow (β := ℕ) I 0 • F.N j ≤ F.N (0 + j)
⊢ I ^ i • F.N j ≤ F.N (i + j)
have succ : ∀ (n : ℕ) (ih : I ^ n • F.N j ≤ F.N (n + j)), I ^ (n + 1) • F.N j ≤ F.N (n + 1 + j)
Tactic: induction i with
  | zero => simp
  | succ _ ih =>
    rw [pow_succ', mul_smul, add_assoc, add_comm 1, ← add_assoc]
    exact (smul_mono_right _ ih).trans (F.smul_le _)
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
i j k : ℕ
⊢ I ^ (i + k) • F.N j ≤ I ^ k • F.N (i + j)
have rw : I ^ k • I ^ i • F.N j ≤ I ^ k • F.N (i + j)
Tactic: rw [add_comm, pow_add, mul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F F' : I.Filtration M
S : Set (I.Filtration M)
i : ℕ
⊢ sSup (N '' S) (i + 1) ≤ sSup (N '' S) i
have apply : IsCofinalFor.{u_2} (α := Submodule R M)
  (Set.range fun (f : (↑(N '' S) : Type u_2)) ↦ (↑f : (i : ℕ) → (fun (a : ℕ) ↦ Submodule R M) i) (i + 1))
  (Set.range fun (f : (↑(N '' S) : Type u_2)) ↦ (↑f : (i : ℕ) → (fun (a : ℕ) ↦ Submodule R M) i) i)
Tactic: apply sSup_le_sSup_of_isCofinalFor _
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F F' : I.Filtration M
S : Set (I.Filtration M)
i : ℕ
⊢ I • sSup (N '' S) i ≤ sSup (N '' S) (i + 1)
have rw : LE.le.{u_2} (α := Submodule R M) (⨆ (i_1 : (↑(N '' S) : Type u_2)), I • (↑i_1 : ℕ → Submodule R M) i)
  (⨆ (i_1 : (↑(N '' S) : Type u_2)), (↑i_1 : ℕ → Submodule R M) (i + 1))
Tactic: rw [sSup_eq_iSup', iSup_apply, Submodule.smul_iSup, iSup_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F F' : I.Filtration M
S : Set (I.Filtration M)
i : ℕ
⊢ LE.le.{u_2} (α := Submodule R M) (⨆ (i_1 : (↑(N '' S) : Type u_2)), I • (↑i_1 : ℕ → Submodule R M) i)
    (⨆ (i_1 : (↑(N '' S) : Type u_2)), (↑i_1 : ℕ → Submodule R M) (i + 1))
have apply : ∀ (i_1 : (↑(N '' S) : Type u_2)), I • (↑i_1 : ℕ → Submodule R M) i ≤ (↑i_1 : ℕ → Submodule R M) (i + 1)
Tactic: apply iSup_mono _
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F F' : I.Filtration M
S : Set (I.Filtration M)
i : ℕ
⊢ sInf (N '' S) (i + 1) ≤ sInf (N '' S) i
have apply : IsCoinitialFor.{u_2} (α := Submodule R M)
  (Set.range fun (f : (↑(N '' S) : Type u_2)) ↦ (↑f : (i : ℕ) → (fun (a : ℕ) ↦ Submodule R M) i) i)
  (Set.range fun (f : (↑(N '' S) : Type u_2)) ↦ (↑f : (i : ℕ) → (fun (a : ℕ) ↦ Submodule R M) i) (i + 1))
Tactic: apply sInf_le_sInf_of_isCoinitialFor _
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F F' : I.Filtration M
S : Set (I.Filtration M)
i : ℕ
⊢ HSMul.hSMul (β := Submodule R M) I (⨅ (i_1 : (↑(N '' S) : Type u_2)), (↑i_1 : ℕ → Submodule R M) i) ≤
    ⨅ (i_1 : (↑(N '' S) : Type u_2)), (↑i_1 : ℕ → Submodule R M) (i + 1)
have refine : LE.le.{u_2} (α := Submodule R M) (⨅ (i_1 : (↑(N '' S) : Type u_2)), I • (↑i_1 : ℕ → Submodule R M) i)
  (⨅ (i_1 : (↑(N '' S) : Type u_2)), (↑i_1 : ℕ → Submodule R M) (i + 1))
Tactic: refine smul_iInf_le.trans ?_
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F F' : I.Filtration M
S : Set (I.Filtration M)
i : ℕ
⊢ LE.le.{u_2} (α := Submodule R M) (⨅ (i_1 : (↑(N '' S) : Type u_2)), I • (↑i_1 : ℕ → Submodule R M) i)
    (⨅ (i_1 : (↑(N '' S) : Type u_2)), (↑i_1 : ℕ → Submodule R M) (i + 1))
have apply : ∀ (i_1 : (↑(N '' S) : Type u_2)), I • (↑i_1 : ℕ → Submodule R M) i ≤ (↑i_1 : ℕ → Submodule R M) (i + 1)
Tactic: apply iInf_mono _
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I_1 : Ideal R
F F' : I_1.Filtration M
I : Ideal R
N : Submodule R M
i : ℕ
⊢ I ^ (i + 1) • N ≤ I ^ i • N
have rw : HPow.hPow (β := ℕ) I 1 • I ^ i • N ≤ I ^ i • N
Tactic: rw [add_comm, pow_add, mul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I_1 : Ideal R
F F' : I_1.Filtration M
I : Ideal R
N : Submodule R M
i : ℕ
⊢ I • I ^ i • N ≤ I ^ (i + 1) • N
have rw : I • I ^ i • N ≤ I ^ (1 + i) • N
Tactic: rw [add_comm, pow_add, mul_smul, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I_1 : Ideal R
F F' : I_1.Filtration M
I : Ideal R
N : Submodule R M
i : ℕ
rw : I • I ^ i • N ≤ I ^ (1 + i) • N
⊢ I • I ^ i • N ≤ I ^ (i + 1) • N
have rw₁ : I • I ^ i • N ≤ (HPow.hPow (β := ℕ) I 1 * I ^ i) • N
Tactic: rw [add_comm, pow_add, mul_smul, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I_1 : Ideal R
F F' : I_1.Filtration M
I : Ideal R
N : Submodule R M
i : ℕ
rw : I • I ^ i • N ≤ I ^ (1 + i) • N
rw₁ : I • I ^ i • N ≤ (HPow.hPow (β := ℕ) I 1 * I ^ i) • N
⊢ I • I ^ i • N ≤ I ^ (i + 1) • N
have rw₂ : I • I ^ i • N ≤ HPow.hPow (β := ℕ) I 1 • I ^ i • N
Tactic: rw [add_comm, pow_add, mul_smul, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I_1 : Ideal R
F F' : I_1.Filtration M
I : Ideal R
N : Submodule R M
i : ℕ
rw : I • I ^ i • N ≤ I ^ (1 + i) • N
rw₁ : I • I ^ i • N ≤ (HPow.hPow (β := ℕ) I 1 * I ^ i) • N
rw₂ : I • I ^ i • N ≤ HPow.hPow (β := ℕ) I 1 • I ^ i • N
⊢ I • I ^ i • N ≤ I ^ (i + 1) • N
have rw₃ : I • I ^ i • N ≤ I • I ^ i • N
Tactic: rw [add_comm, pow_add, mul_smul, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
⊢ (I.stableFiltration N).Stable
have h : ∀ n ≥ 0, I • (I.stableFiltration N).N n = (I.stableFiltration N).N (n + 1)
Tactic: use 0
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
n : ℕ
h : n ≥ 0
⊢ I • I ^ n • N = I ^ (n + 1) • N
have h : I • I ^ n • N = I ^ (1 + n) • N
Tactic: rw [add_comm, pow_add, mul_smul, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
n : ℕ
h_1 : n ≥ 0
h : I • I ^ n • N = I ^ (1 + n) • N
⊢ I • I ^ n • N = I ^ (n + 1) • N
have h₁ : I • I ^ n • N = (HPow.hPow (β := ℕ) I 1 * I ^ n) • N
Tactic: rw [add_comm, pow_add, mul_smul, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
n : ℕ
h_1 : n ≥ 0
h : I • I ^ n • N = I ^ (1 + n) • N
h₁ : I • I ^ n • N = (HPow.hPow (β := ℕ) I 1 * I ^ n) • N
⊢ I • I ^ n • N = I ^ (n + 1) • N
have h₂ : I • I ^ n • N = HPow.hPow (β := ℕ) I 1 • I ^ n • N
Tactic: rw [add_comm, pow_add, mul_smul, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
n : ℕ
h_1 : n ≥ 0
h : I • I ^ n • N = I ^ (1 + n) • N
h₁ : I • I ^ n • N = (HPow.hPow (β := ℕ) I 1 * I ^ n) • N
h₂ : I • I ^ n • N = HPow.hPow (β := ℕ) I 1 • I ^ n • N
⊢ I • I ^ n • N = I ^ (n + 1) • N
have h₃ : I • I ^ n • N = I • I ^ n • N
Tactic: rw [add_comm, pow_add, mul_smul, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
h : F.Stable
⊢ ∃ (n₀ : ℕ), ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
have obtain : ∀ (n₀ : ℕ) (hn : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)), ∃ (n₀ : ℕ), ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
Tactic: obtain ⟨n₀, hn⟩ := h
Cleared hypotheses: h