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
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst_7 : Finite σ
inst_8 : Finite σ'
val : Fintype σ'
val_1 : Fintype σ
h :
  Eq.{u_3 + 1} (α := T)
    ((aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P)))) :
          (a : MvPolynomial (ι' ⊕ ι) R) → T)
        (Matrix.det
            (Matrix.fromBlocks (Matrix.toBlocks₁₁ (jacobiMatrix (Q.comp P))) 0
              (Matrix.toBlocks₂₁ (jacobiMatrix (Q.comp P))) (Matrix.toBlocks₂₂ (jacobiMatrix (Q.comp P)))) :
          Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P)))) :
      T)
    ((aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P)))) :
          (a : MvPolynomial (ι' ⊕ ι) R) → T)
        (HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
          (Matrix.det (Matrix.toBlocks₁₁ (jacobiMatrix (Q.comp P))) :
            Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P))))
          (Matrix.det (Matrix.toBlocks₂₂ (jacobiMatrix (Q.comp P))))) :
      T)
⊢ (algebraMap (Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P)))) T : (a : (Q.comp P).Ring) → T)
      (Matrix.det
        (Matrix.fromBlocks (Matrix.toBlocks₁₁ (jacobiMatrix (Q.comp P))) 0 (Matrix.toBlocks₂₁ (jacobiMatrix (Q.comp P)))
          (Matrix.toBlocks₂₂ (jacobiMatrix (Q.comp P))))) =
    HMul.hMul (α := T) (β := T)
      ((aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P)))) :
            (a : MvPolynomial (ι' ⊕ ι) R) → T)
          (Matrix.det (Matrix.toBlocks₁₁ (jacobiMatrix (Q.comp P))) :
            Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P)))) :
        T)
      ((aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P)))) :
            (a : MvPolynomial (ι' ⊕ ι) R) → T)
          (Matrix.det (Matrix.toBlocks₂₂ (jacobiMatrix (Q.comp P))) :
            Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P)))) :
        T)

Tactic:
simp only [Generators.algebraMap_apply, ← map_mul]

Premises used: Algebra.Generators.algebraMap_apply, map_mul
-- 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
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst_7 : Finite σ
inst_8 : Finite σ'
val : Fintype σ'
val_1 : Fintype σ
h :
  Matrix.det
      (Matrix.fromBlocks (Matrix.toBlocks₁₁ (jacobiMatrix (Q.comp P))) 0 (Matrix.toBlocks₂₁ (jacobiMatrix (Q.comp P)))
        (Matrix.toBlocks₂₂ (jacobiMatrix (Q.comp P)))) =
    HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
      (Matrix.det (Matrix.toBlocks₁₁ (jacobiMatrix (Q.comp P))) :
        Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P))))
      (Matrix.det (Matrix.toBlocks₂₂ (jacobiMatrix (Q.comp P))))
⊢ Eq.{u_3 + 1} (α := T)
    ((aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P)))) :
          (a : MvPolynomial (ι' ⊕ ι) R) → T)
        (Matrix.det
            (Matrix.fromBlocks (Matrix.toBlocks₁₁ (jacobiMatrix (Q.comp P))) 0
              (Matrix.toBlocks₂₁ (jacobiMatrix (Q.comp P))) (Matrix.toBlocks₂₂ (jacobiMatrix (Q.comp P)))) :
          Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P)))) :
      T)
    ((aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P)))) :
          (a : MvPolynomial (ι' ⊕ ι) R) → T)
        (HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
          (Matrix.det (Matrix.toBlocks₁₁ (jacobiMatrix (Q.comp P))) :
            Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P))))
          (Matrix.det (Matrix.toBlocks₂₂ (jacobiMatrix (Q.comp P))))) :
      T)

Tactic:
congr
-- 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
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst_7 : Finite σ
inst_8 : Finite σ'
val : Fintype σ'
val_1 : Fintype σ
⊢ Matrix.det
      (Matrix.fromBlocks (Matrix.toBlocks₁₁ (jacobiMatrix (Q.comp P))) 0 (Matrix.toBlocks₂₁ (jacobiMatrix (Q.comp P)))
        (Matrix.toBlocks₂₂ (jacobiMatrix (Q.comp P)))) =
    HMul.hMul (α := Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P))))
      (Matrix.det (Matrix.toBlocks₁₁ (jacobiMatrix (Q.comp P))))
      (Matrix.det (Matrix.toBlocks₂₂ (jacobiMatrix (Q.comp P))))

Tactic:
Matrix.det_fromBlocks_zero₁₂ (Q.comp P).jacobiMatrix.toBlocks₁₁
        (Q.comp P).jacobiMatrix.toBlocks₂₁ (Q.comp P).jacobiMatrix.toBlocks₂₂

Premises used: Matrix.toBlocks₂₁, Matrix.toBlocks₁₁, Matrix.det_fromBlocks_zero₁₂, Algebra.PreSubmersivePresentation.comp, Matrix.toBlocks₂₂, Algebra.PreSubmersivePresentation.jacobiMatrix
-- 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
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst_7 : Finite σ
inst_8 : Finite σ'
val : Fintype σ'
val_1 : Fintype σ
⊢ Matrix.det
      (Matrix.fromBlocks (Matrix.toBlocks₁₁ (jacobiMatrix (Q.comp P))) 0 (Matrix.toBlocks₂₁ (jacobiMatrix (Q.comp P)))
        (Matrix.toBlocks₂₂ (jacobiMatrix (Q.comp P)))) =
    HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
      (Matrix.det (Matrix.toBlocks₁₁ (jacobiMatrix (Q.comp P))) :
        Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P))))
      (Matrix.det (Matrix.toBlocks₂₂ (jacobiMatrix (Q.comp P))))

Tactic:
convert!
      Matrix.det_fromBlocks_zero₁₂ (Q.comp P).jacobiMatrix.toBlocks₁₁
        (Q.comp P).jacobiMatrix.toBlocks₂₁ (Q.comp P).jacobiMatrix.toBlocks₂₂

Premises used: Matrix.toBlocks₂₁, Matrix.toBlocks₁₁, Matrix.det_fromBlocks_zero₁₂, Algebra.PreSubmersivePresentation.comp, Matrix.toBlocks₂₂, Algebra.PreSubmersivePresentation.jacobiMatrix
-- 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
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst_7 : Finite σ
inst_8 : Finite σ'
val : Fintype σ'
val_1 : Fintype σ
intro :
  HMul.hMul (β := T) Q.jacobian
      ((aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P)))) :
            (a : MvPolynomial (ι' ⊕ ι) R) → T)
          (Matrix.det (Matrix.toBlocks₂₂ (jacobiMatrix (Q.comp P))) :
            Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P)))) :
        T) =
    P.jacobian • Q.jacobian
intro₁ : HMul.hMul (β := T) Q.jacobian ((algebraMap S T : (a : S) → T) P.jacobian : T) = P.jacobian • Q.jacobian
intro₂ : HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) P.jacobian : T) Q.jacobian = P.jacobian • Q.jacobian
intro₃ intro₄ :
  HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) P.jacobian : T) Q.jacobian =
    HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) P.jacobian : T) Q.jacobian
⊢ HMul.hMul (α := T) (β := T)
      ((aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P)))) :
            (a : MvPolynomial (ι' ⊕ ι) R) → T)
          (Matrix.det (Matrix.toBlocks₁₁ (jacobiMatrix (Q.comp P))) :
            Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P)))) :
        T)
      ((aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P)))) :
            (a : MvPolynomial (ι' ⊕ ι) R) → T)
          (Matrix.det (Matrix.toBlocks₂₂ (jacobiMatrix (Q.comp P))) :
            Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P)))) :
        T) =
    P.jacobian • Q.jacobian

Tactic:
rw [jacobiMatrix_comp_₁₁_det, jacobiMatrix_comp_₂₂_det, mul_comm, Algebra.smul_def]

Premises used: _private.0.Algebra.PreSubmersivePresentation.jacobiMatrix_comp_₂₂_det, _private.0.Algebra.PreSubmersivePresentation.jacobiMatrix_comp_₁₁_det, mul_comm, 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
P : PreSubmersivePresentation R S ι σ
⊢ Eq (α := Presentation R (R ⊗[R] S) ι σ) (toPresentation (baseChange R P)) (Presentation.baseChange R P.toPresentation)

Tactic:
rfl

Premises used: Algebra.Presentation.baseChange, 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
P : PreSubmersivePresentation R S ι σ
⊢ Generators.Ring (S := R ⊗[R] S) (Presentation.toGenerators (toPresentation (baseChange R P))) = P.Ring

Tactic:
rfl

Premises used: 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
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
P : PreSubmersivePresentation R S ι σ
inst_5 : Finite σ
intro : ∀ (val : Fintype σ), Eq (α := T ⊗[R] S) (jacobian (baseChange T P)) (1 ⊗ₜ[R] P.jacobian)
⊢ Eq (α := T ⊗[R] S) (jacobian (baseChange T P)) (1 ⊗ₜ[R] P.jacobian)

Tactic:
cases nonempty_fintype σ

Premises used: nonempty_fintype
-- 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
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
P : PreSubmersivePresentation R S ι σ
inst_5 : Finite σ
val : Fintype σ
intro :
  Eq (α := T ⊗[R] S)
    ((algebraMap (Generators.Ring (S := T ⊗[R] S) (Presentation.toGenerators (toPresentation (baseChange T P))))
            (T ⊗[R] S) :
          (a : (baseChange T P).Ring) → T ⊗[R] S)
        (Matrix.det (jacobiMatrix (baseChange T P))) :
      T ⊗[R] S)
    (1 ⊗ₜ[R] (algebraMap P.Ring S : (a : P.Ring) → S) P.jacobiMatrix.det : T ⊗[R] S)
⊢ Eq (α := T ⊗[R] S) (jacobian (baseChange T P)) (1 ⊗ₜ[R] P.jacobian)

Tactic:
simp_rw [jacobian_eq_jacobiMatrix_det]

Premises used: 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
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
P : PreSubmersivePresentation R S ι σ
inst_5 : Finite σ
val : Fintype σ
a :
  ∀ (i j : σ),
    Eq (α := Generators.Ring (S := T ⊗[R] S) (Presentation.toGenerators (toPresentation (baseChange T P))))
      (jacobiMatrix (baseChange T P) i j)
      ((RingHom.mapMatrix (MvPolynomial.map (algebraMap R T)) :
          (a : Matrix σ σ (MvPolynomial ι R)) → Matrix σ σ (MvPolynomial ι T))
        P.jacobiMatrix i j)
⊢ Eq (α := Matrix σ σ (Generators.Ring (S := T ⊗[R] S) (Presentation.toGenerators (toPresentation (baseChange T P)))))
    (jacobiMatrix (baseChange T P))
    ((RingHom.mapMatrix (MvPolynomial.map (algebraMap R T)) :
        (a : Matrix σ σ (MvPolynomial ι R)) → Matrix σ σ (MvPolynomial ι T))
      P.jacobiMatrix)

Tactic:
ext i j : 1
-- 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
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
P : PreSubmersivePresentation R S ι σ
inst_5 : Finite σ
val : Fintype σ
i j : σ
⊢ Eq (α := Generators.Ring (S := T ⊗[R] S) (Presentation.toGenerators (toPresentation (baseChange T P))))
    (jacobiMatrix (baseChange T P) i j)
    ((RingHom.mapMatrix (MvPolynomial.map (algebraMap R T)) :
        (a : Matrix σ σ (MvPolynomial ι R)) → Matrix σ σ (MvPolynomial ι T))
      P.jacobiMatrix i j)

Tactic:
simp only [baseChange, jacobiMatrix_apply, Presentation.baseChange_relation,
      RingHom.mapMatrix_apply, Matrix.map_apply,
      Presentation.baseChange_toGenerators, MvPolynomial.pderiv_map]

Premises used: RingHom.mapMatrix_apply, Algebra.PreSubmersivePresentation.jacobiMatrix_apply, Matrix.map_apply, MvPolynomial.pderiv_map, Algebra.Presentation.baseChange_relation, Algebra.PreSubmersivePresentation.baseChange, Algebra.Presentation.baseChange_toGenerators
-- 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
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
P : PreSubmersivePresentation R S ι σ
inst_5 : Finite σ
val : Fintype σ
⊢ Eq (α := Matrix σ σ (Generators.Ring (S := T ⊗[R] S) (Presentation.toGenerators (toPresentation (baseChange T P)))))
    (jacobiMatrix (baseChange T P))
    ((RingHom.mapMatrix (MvPolynomial.map (algebraMap R T)) :
        (a : Matrix σ σ (MvPolynomial ι R)) → Matrix σ σ (MvPolynomial ι T))
      P.jacobiMatrix)

Tactic:
have h : (baseChange T P).jacobiMatrix =
      (MvPolynomial.map (algebraMap R T)).mapMatrix P.jacobiMatrix := by
    ext i j : 1
    simp only [baseChange, jacobiMatrix_apply, Presentation.baseChange_relation,
      RingHom.mapMatrix_apply, Matrix.map_apply,
      Presentation.baseChange_toGenerators, MvPolynomial.pderiv_map]
-- 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
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
P : PreSubmersivePresentation R S ι σ
inst_5 : Finite σ
val : Fintype σ
h :
  Eq (α := Matrix σ σ (Generators.Ring (S := T ⊗[R] S) (Presentation.toGenerators (toPresentation (baseChange T P)))))
    (jacobiMatrix (baseChange T P))
    ((RingHom.mapMatrix (MvPolynomial.map (algebraMap R T)) :
        (a : Matrix σ σ (MvPolynomial ι R)) → Matrix σ σ (MvPolynomial ι T))
      P.jacobiMatrix)
intro :
  Eq (α := T ⊗[R] S)
    (((aeval (R := R) (S₁ := T ⊗[R] S) (Generators.val (Presentation.toGenerators (toPresentation (baseChange T P)))) :
            MvPolynomial ι R →ₐ[R] T ⊗[R] S) :
          (a : MvPolynomial ι R) → T ⊗[R] S)
        P.jacobiMatrix.det :
      T ⊗[R] S)
    (1 ⊗ₜ[R] (aeval P.val : (a : MvPolynomial ι R) → S) P.jacobiMatrix.det : T ⊗[R] S)
⊢ Eq (α := T ⊗[R] S)
    ((algebraMap (Generators.Ring (S := T ⊗[R] S) (Presentation.toGenerators (toPresentation (baseChange T P))))
            (T ⊗[R] S) :
          (a : (baseChange T P).Ring) → T ⊗[R] S)
        (Matrix.det (jacobiMatrix (baseChange T P))) :
      T ⊗[R] S)
    (1 ⊗ₜ[R] (algebraMap P.Ring S : (a : P.Ring) → S) P.jacobiMatrix.det : T ⊗[R] S)

Tactic:
rw [h, ← RingHom.map_det, Generators.algebraMap_apply, aeval_map_algebraMap, P.algebraMap_apply]

Premises used: Algebra.Generators.algebraMap_apply, Algebra.PreSubmersivePresentation.toPresentation, MvPolynomial.aeval_map_algebraMap, RingHom.map_det, Algebra.Presentation.toGenerators
-- 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
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
P : PreSubmersivePresentation R S ι σ
inst_5 : Finite σ
val : Fintype σ
h :
  Eq (α := Matrix σ σ (Generators.Ring (S := T ⊗[R] S) (Presentation.toGenerators (toPresentation (baseChange T P)))))
    (jacobiMatrix (baseChange T P))
    ((RingHom.mapMatrix (MvPolynomial.map (algebraMap R T)) :
        (a : Matrix σ σ (MvPolynomial ι R)) → Matrix σ σ (MvPolynomial ι T))
      P.jacobiMatrix)
⊢ Eq (α := T ⊗[R] S)
    (((aeval (R := R) (S₁ := T ⊗[R] S) (Generators.val (Presentation.toGenerators (toPresentation (baseChange T P)))) :
            MvPolynomial ι R →ₐ[R] T ⊗[R] S) :
          (a : MvPolynomial ι R) → T ⊗[R] S)
        P.jacobiMatrix.det :
      T ⊗[R] S)
    (1 ⊗ₜ[R] (aeval P.val : (a : MvPolynomial ι R) → S) P.jacobiMatrix.det : T ⊗[R] S)

Tactic:
apply aeval_one_tmul

Premises used: MvPolynomial.aeval_one_tmul
-- 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_1 P : PreSubmersivePresentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
rw : Function.Injective.{u_2 + 1, t + 1} (α := σ') (β := σ) (⇑f : (a : σ') → σ)
⊢ Function.Injective.{u_2 + 1, u_1 + 1} (α := σ') (β := ι') ((⇑e.symm : (a : ι) → ι') ∘ P.map ∘ (⇑f : (a : σ') → σ))

Tactic:
rw [Function.Injective.of_comp_iff e.symm.injective, Function.Injective.of_comp_iff P.map_inj]

Premises used: Algebra.PreSubmersivePresentation.map_inj, Equiv.injective, Equiv.symm, Function.Injective.of_comp_iff
-- 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_1 P : PreSubmersivePresentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
⊢ Function.Injective.{u_2 + 1, t + 1} (α := σ') (β := σ) (⇑f : (a : σ') → σ)

Tactic:
f.injective

Premises used: Equiv.injective
-- 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_1 P : PreSubmersivePresentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
⊢ Function.Injective.{u_2 + 1, t + 1} (α := σ') (β := σ) (⇑f : (a : σ') → σ)

Tactic:
exact f.injective

Premises used: Equiv.injective
-- 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 : Fintype σ'
inst_4 : DecidableEq σ'
inst_5 : Fintype σ
inst_6 : DecidableEq σ
a :
  ∀ (i j : σ'),
    (P.reindex e f).jacobiMatrix i j =
      Matrix.map (α := P.Ring)
        ((Matrix.reindex f.symm f.symm : (a : Matrix σ σ P.Ring) → Matrix σ' σ' P.Ring) P.jacobiMatrix)
        (⇑(rename (⇑e.symm : (a : ι) → ι')) : (a : MvPolynomial ι R) → MvPolynomial ι' R) i j
⊢ (P.reindex e f).jacobiMatrix =
    Matrix.map (α := P.Ring)
      ((Matrix.reindex f.symm f.symm : (a : Matrix σ σ P.Ring) → Matrix σ' σ' P.Ring) P.jacobiMatrix)
      (⇑(rename (⇑e.symm : (a : ι) → ι')) : (a : MvPolynomial ι R) → MvPolynomial ι' R)

Tactic:
ext i j : 1
-- 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 : Fintype σ'
inst_4 : DecidableEq σ'
inst_5 : Fintype σ
inst_6 : DecidableEq σ
i j : σ'
⊢ (P.reindex e f).jacobiMatrix i j =
    Matrix.map (α := P.Ring)
      ((Matrix.reindex f.symm f.symm : (a : Matrix σ σ P.Ring) → Matrix σ' σ' P.Ring) P.jacobiMatrix)
      (⇑(rename (⇑e.symm : (a : ι) → ι')) : (a : MvPolynomial ι R) → MvPolynomial ι' R) i j

Tactic:
simp [jacobiMatrix_apply,
    MvPolynomial.pderiv_rename e.symm.injective, reindex, Presentation.reindex]

Premises used: Algebra.Presentation.reindex, MvPolynomial.pderiv_rename, Algebra.PreSubmersivePresentation.jacobiMatrix_apply, Equiv.injective, Equiv.symm, Algebra.PreSubmersivePresentation.reindex
-- 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
⊢ (P.reindex e f).jacobian = P.jacobian

Tactic:
cases nonempty_fintype σ

Premises used: nonempty_fintype
-- 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 σ
intro : ∀ (val : Fintype σ'), (P.reindex e f).jacobian = P.jacobian
⊢ (P.reindex e f).jacobian = P.jacobian

Tactic:
cases nonempty_fintype σ'

Premises used: nonempty_fintype
-- 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)
    ((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

Tactic:
simp_rw [PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det]

Premises used: 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
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)
    ((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)
⊢ 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 only [reindex_toPresentation, Presentation.reindex_toGenerators, jacobiMatrix_reindex,
    Matrix.reindex_apply, Equiv.symm_symm, Generators.algebraMap_apply, Generators.reindex_val]

Premises used: Algebra.PreSubmersivePresentation.jacobiMatrix_reindex, Algebra.Generators.algebraMap_apply, Matrix.reindex_apply, Equiv.symm_symm, Algebra.Generators.reindex_val, Algebra.Presentation.reindex_toGenerators, Algebra.PreSubmersivePresentation.reindex_toPresentation