awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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 σ'
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)))
⊢ 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_rw [← MvPolynomial.aeval_rename,
    ← AlgHom.mapMatrix_apply, ← Matrix.det_submatrix_equiv_self f, AlgHom.map_det,
    AlgHom.mapMatrix_apply, Matrix.map_map]

Premises used: AlgHom.map_det, AlgHom.mapMatrix_apply, Matrix.map_map, Matrix.det_submatrix_equiv_self, MvPolynomial.aeval_rename
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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)
    (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 [← AlgHom.coe_comp, rename_comp_rename, rename_id]

Premises used: AlgHom.coe_comp, MvPolynomial.rename_comp_rename, MvPolynomial.rename_id
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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)
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)))
⊢ (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]

Premises used: Algebra.PreSubmersivePresentation.jacobiMatrix_reindex, Algebra.Generators.algebraMap_apply, Matrix.reindex_apply, Equiv.symm_symm, AlgHom.map_det, AlgHom.mapMatrix_apply, AlgHom.coe_comp, nonempty_fintype, Algebra.Generators.reindex_val, Algebra.Presentation.reindex_toGenerators, Matrix.map_map, MvPolynomial.rename_comp_rename, MvPolynomial.aeval_rename, Algebra.PreSubmersivePresentation.reindex_toPresentation, Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det, MvPolynomial.rename_id
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
Goal:
R : Type u
ι : Type w
σ : Type t
inst : CommRing R
v : ι → MvPolynomial σ R
a : ι → σ
ha : Function.Injective a
s :
  HasQuotient.Quotient (MvPolynomial σ R) (B := Ideal (MvPolynomial σ R)) (Ideal.span (Set.range v)) → MvPolynomial σ R
hs :
  ∀ (x : HasQuotient.Quotient (MvPolynomial σ R) (B := Ideal (MvPolynomial σ R)) (Ideal.span (Set.range v))),
    (Ideal.Quotient.mk (Ideal.span (Set.range v)) :
          (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ Ideal.span (Set.range v))
        (s x) =
      x
inst_1 : Fintype ι
inst_2 : DecidableEq ι
i j : ι
⊢ (naive a ha s hs).jacobiMatrix i j = (pderiv (a i) : (a : MvPolynomial σ R) → MvPolynomial σ R) (v j)

Tactic:
jacobiMatrix_apply _ _ _

Premises used: Algebra.PreSubmersivePresentation.jacobiMatrix_apply
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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 ι σ
T : Type u_1
inst_4 : CommRing T
inst_5 : Algebra R T
e : S ≃ₐ[R] T
⊢ IsUnit (P.ofAlgEquiv e).jacobian

Tactic:
simp [P.jacobian_isUnit]

Premises used: Algebra.SubmersivePresentation.jacobian_isUnit
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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)
rw : IsUnit.{v} (M := S) 1
⊢ IsUnit (PreSubmersivePresentation.ofBijectiveAlgebraMap h).jacobian

Tactic:
rw [ofBijectiveAlgebraMap_jacobian]

Premises used: Algebra.PreSubmersivePresentation.ofBijectiveAlgebraMap_jacobian
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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.{v} (M := S) 1

Tactic:
isUnit_one

Premises used: isUnit_one
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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.{v} (M := S) 1

Tactic:
exact isUnit_one

Premises used: isUnit_one
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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 ι σ
rw : IsUnit.{u_1} (M := T) ((algebraMap S T : (a : S) → T) P.jacobian : T) ∧ IsUnit Q.jacobian
⊢ IsUnit (jacobian (Q.comp P.toPreSubmersivePresentation))

Tactic:
rw [comp_jacobian_eq_jacobian_smul_jacobian, Algebra.smul_def, IsUnit.mul_iff]

Premises used: IsUnit.mul_iff, Algebra.PreSubmersivePresentation.comp_jacobian_eq_jacobian_smul_jacobian, Algebra.smul_def
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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.{u_1} (M := T) ((algebraMap S T : (a : S) → T) P.jacobian : T) ∧ IsUnit Q.jacobian

Tactic:
⟨RingHom.isUnit_map _ <| P.jacobian_isUnit, Q.jacobian_isUnit⟩

Premises used: And.intro, RingHom.isUnit_map, Algebra.SubmersivePresentation.jacobian_isUnit
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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.{u_1} (M := T) ((algebraMap S T : (a : S) → T) P.jacobian : T) ∧ IsUnit Q.jacobian

Tactic:
exact ⟨RingHom.isUnit_map _ <| P.jacobian_isUnit, Q.jacobian_isUnit⟩
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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
rw : IsUnit.{v} (M := S) ((algebraMap R S : (a : R) → S) r : S)
⊢ IsUnit (jacobian (PreSubmersivePresentation.localizationAway S r))

Tactic:
rw [localizationAway_jacobian]

Premises used: Algebra.PreSubmersivePresentation.localizationAway_jacobian
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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
⊢ (fun (x : ℕ) ↦ r ^ x) 1 = r

Tactic:
simp
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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.{v} (M := S) ((algebraMap R S : (a : R) → S) r : S)

Tactic:
exact IsLocalization.map_units _ (⟨r, 1, by simp⟩ : Submonoid.powers r)

Premises used: Subtype.mk, Exists.intro, IsLocalization.map_units, OfNat.ofNat
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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 ι σ
ι' : Type u_1
σ' : Type u_2
inst_4 : Finite σ'
e : ι' ≃ ι
f : σ' ≃ σ
⊢ IsUnit (P.reindex e f).jacobian

Tactic:
simp [P.jacobian_isUnit]

Premises used: Algebra.SubmersivePresentation.jacobian_isUnit
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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 σ
inst_4 : Subsingleton S
⊢ Eq (α :=
    Ideal
      (Generators.Ring.{u_2, u, v}
        { val := fun (x : PUnit.{u_2 + 1}) ↦ 1, σ' := fun (x : S) ↦ 1, aeval_val_σ' := ⋯, algebraMap_eq := ⋯ }))
    (Ideal.span (Set.range fun (x : PUnit.{u_1 + 1}) ↦ 1))
    (Generators.ker
      { val := fun (x : PUnit.{u_2 + 1}) ↦ 1, σ' := fun (x : S) ↦ 1, aeval_val_σ' := ⋯, algebraMap_eq := ⋯ })

Tactic:
simp [Generators.ker, Extension.ker, RingHom.ker_eq_top_of_subsingleton]

Premises used: Algebra.Generators.ker, RingHom.ker_eq_top_of_subsingleton, Algebra.Extension.ker
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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 P.jacobian

Tactic:
P.jacobian_isUnit

Premises used: Algebra.SubmersivePresentation.jacobian_isUnit
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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 σ
h :
  Matrix.det.{v, t} (n := σ)
      ((LinearMap.toMatrix (Pi.basisFun S σ) (Pi.basisFun S σ) : (a : (σ → S) →ₗ[S] σ → S) → Matrix σ σ S)
        P.aevalDifferential) =
    P.jacobian
⊢ 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))

Tactic:
convert! P.jacobian_isUnit

Premises used: Algebra.SubmersivePresentation.jacobian_isUnit
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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 σ
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)
⊢ Matrix.det.{v, t} (n := σ)
      ((LinearMap.toMatrix (Pi.basisFun S σ) (Pi.basisFun S σ) : (a : (σ → S) →ₗ[S] σ → S) → Matrix σ σ S)
        P.aevalDifferential) =
    P.jacobian

Tactic:
rw [LinearMap.toMatrix_eq_toMatrix', jacobian_eq_jacobiMatrix_det,
      aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix, P.algebraMap_eq]

Premises used: Algebra.SubmersivePresentation.toPreSubmersivePresentation, Algebra.Generators.algebraMap_eq, Algebra.PreSubmersivePresentation.aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix, Algebra.PreSubmersivePresentation.toPresentation, LinearMap.toMatrix_eq_toMatrix', Algebra.Presentation.toGenerators, Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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 σ
⊢ 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:
simp [RingHom.map_det]

Premises used: RingHom.map_det
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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 ι σ
x : σ → S
⊢ Eq (α := σ → S) ((P.aevalDifferentialEquiv : (a : σ → S) → σ → S) x : σ → S)
    ((P.aevalDifferential : (a : σ → S) → σ → S) x : σ → S)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, Finset.sum, rfl
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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 ι σ
i j : σ
⊢ Eq.{v + 1} (α := S) ((P.basisDeriv : (a : σ) → σ → S) i j : S)
    ((aeval P.val : (a : MvPolynomial ι R) → S)
        ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation i) : MvPolynomial ι R) :
      S)

Tactic:
simp [basisDeriv]

Premises used: Algebra.SubmersivePresentation.basisDeriv
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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 ι σ
i j : σ
⊢ Eq.{v + 1} (α := S) ((P.basisDeriv : (a : σ) → σ → S) i j : S)
    ((aeval P.val : (a : MvPolynomial ι R) → S)
        ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation i) : MvPolynomial ι R) :
      S)

Tactic:
classical
  simp [basisDeriv]

Premises used: Algebra.SubmersivePresentation.basisDeriv
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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 ι σ
simp_rw : LinearIndependent S (M := (j : σ) → S) fun (i j : σ) ↦ (P.basisDeriv : (a : σ) → σ → S) i j
⊢ 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)

Tactic:
simp_rw [← SubmersivePresentation.basisDeriv_apply]

Premises used: Algebra.SubmersivePresentation.basisDeriv_apply
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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 : σ) ↦ (P.basisDeriv : (a : σ) → σ → S) i j

Tactic:
P.basisDeriv.linearIndependent

Premises used: Algebra.SubmersivePresentation.basisDeriv, Module.Basis.linearIndependent
-- Module: Mathlib.RingTheory.Extension.Presentation.Submersive
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 : σ) ↦ (P.basisDeriv : (a : σ) → σ → S) i j

Tactic:
exact P.basisDeriv.linearIndependent

Premises used: Algebra.SubmersivePresentation.basisDeriv, Module.Basis.linearIndependent
-- Module: Mathlib.RingTheory.FilteredAlgebra.Basic
Goal:
ι : Type u_1
σ : Type u_3
inst : Preorder ι
inst_1 : Preorder σ
F F_lt : ι → σ
i : ι
inst_2 : IsFiltration F F_lt
⊢ F_lt i ≤ F i

Tactic:
is_sup (F i) i (fun _ hi ↦ IsFiltration.mono (le_of_lt hi))

Premises used: IsFiltration.is_sup, IsFiltration.mono, le_of_lt
-- Module: Mathlib.RingTheory.FilteredAlgebra.Basic
Goal:
R : Type u_3
M : Type u_4
σ : Type u_5
σM : Type u_6
inst : Preorder σ
inst_1 : Semiring R
inst_2 : SetLike σ R
inst_3 : Preorder σM
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : SetLike σM M
F : ℤ → σ
mono : Monotone F
inst_7 : SetLike.GradedMonoid F
F' : ℤ → σM
mono' : Monotone F'
inst_8 : SetLike.GradedSMul F F'
⊢ IsModuleFiltration F (fun (n : ℤ) ↦ F (n - 1)) F' fun (n : ℤ) ↦ F' (n - 1)

Tactic:
letI := IsRingFiltration.mk_int F mono
  { IsFiltration.mk_int F' mono' with }

Premises used: IsFiltration.mk_int, IsModuleFiltration.mk
-- Module: Mathlib.RingTheory.Filtration
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 : ℕ
⊢ HPow.hPow (β := ℕ) I 0 • F.N j ≤ F.N (0 + j)

Tactic:
simp
-- Module: Mathlib.RingTheory.Filtration
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)
succ : I • I ^ n • F.N j ≤ F.N (n + j + 1)
⊢ I ^ (n + 1) • F.N j ≤ F.N (n + 1 + j)

Tactic:
rw [pow_succ', mul_smul, add_assoc, add_comm 1, ← add_assoc]

Premises used: add_assoc, add_comm, OfNat.ofNat, SemigroupAction.mul_smul, pow_succ'
-- Module: Mathlib.RingTheory.Filtration
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 • I ^ n • F.N j ≤ F.N (n + j + 1)

Tactic:
(smul_mono_right _ ih).trans (F.smul_le _)

Premises used: Ideal.Filtration.smul_le, Set.Mem, smul_mono_right, LE.le.trans
-- Module: Mathlib.RingTheory.Filtration
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 • I ^ n • F.N j ≤ F.N (n + j + 1)

Tactic:
exact (smul_mono_right _ ih).trans (F.smul_le _)

Premises used: Ideal.Filtration.smul_le, smul_mono_right, LE.le.trans
-- Module: Mathlib.RingTheory.Filtration
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)
succ : ∀ (n : ℕ) (ih : I ^ n • F.N j ≤ F.N (n + j)), I ^ (n + 1) • F.N j ≤ F.N (n + 1 + j)
⊢ I ^ i • F.N j ≤ F.N (i + 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 _)

Premises used: add_assoc, add_comm, OfNat.ofNat, SemigroupAction.mul_smul, pow_succ'
-- Module: Mathlib.RingTheory.Filtration
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 : ℕ
rw : I ^ k • I ^ i • F.N j ≤ I ^ k • F.N (i + j)
⊢ I ^ (i + k) • F.N j ≤ I ^ k • F.N (i + j)

Tactic:
rw [add_comm, pow_add, mul_smul]

Premises used: pow_add, add_comm, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Filtration
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 ^ k • I ^ i • F.N j ≤ I ^ k • F.N (i + j)

Tactic:
smul_mono_right _ (F.pow_smul_le i j)

Premises used: Set.Mem, smul_mono_right, Ideal.Filtration.pow_smul_le
-- Module: Mathlib.RingTheory.Filtration
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 ^ k • I ^ i • F.N j ≤ I ^ k • F.N (i + j)

Tactic:
exact smul_mono_right _ (F.pow_smul_le i j)

Premises used: smul_mono_right, Ideal.Filtration.pow_smul_le
-- Module: Mathlib.RingTheory.Filtration
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
⊢ Antitone F.N

Tactic:
antitone_nat_of_succ_le F.mono

Premises used: antitone_nat_of_succ_le, Ideal.Filtration.mono
-- Module: Mathlib.RingTheory.Filtration
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 : ℕ
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)
⊢ sSup (N '' S) (i + 1) ≤ sSup (N '' S) i

Tactic:
apply sSup_le_sSup_of_isCofinalFor _

Premises used: sSup_le_sSup_of_isCofinalFor
-- Module: Mathlib.RingTheory.Filtration
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_1 F' : I.Filtration M
S : Set (I.Filtration M)
i : ℕ
F : I.Filtration M
hF : F ∈ S
⊢ ∃ (b : Submodule R M),
    Membership.mem (γ := Set (Submodule R M))
        (Set.range fun (f : (↑(N '' S) : Type u_2)) ↦ (↑f : (i : ℕ) → (fun (a : ℕ) ↦ Submodule R M) i) i) b ∧
      (fun (f : (↑(N '' S) : Type u_2)) ↦ (↑f : (i : ℕ) → (fun (a : ℕ) ↦ Submodule R M) i) (i + 1))
          (Subtype.mk (p := fun (x : (i : ℕ) → (fun (a : ℕ) ↦ Submodule R M) i) ↦ x ∈ N '' S) F.N ⋯) ≤
        b

Tactic:
⟨_, ⟨⟨_, F, hF, rfl⟩, rfl⟩, F.mono i⟩

Premises used: Subtype.mk, And.intro, Ideal.Filtration.mono, Exists.intro, rfl