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 : Fintype σ
inst_8 : Fintype σ'
rw :
  Eq.{u_3 + 1} (α := T)
    (Matrix.det.{u_3, t} (n := σ)
      ((AlgHom.mapMatrix (aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))) :
          (a : Matrix σ σ (MvPolynomial (ι' ⊕ ι) R)) → Matrix σ σ T)
        (Matrix.toBlocks₂₂ (jacobiMatrix (Q.comp P)))))
    (Matrix.det.{u_3, t} (n := σ)
      ((RingHom.mapMatrix (algebraMap S T) : (a : Matrix σ σ S) → Matrix σ σ T)
        ((RingHom.mapMatrix (algebraMap P.Ring S) : (a : Matrix σ σ P.Ring) → Matrix σ σ S) P.jacobiMatrix)))
⊢ Eq.{u_3 + 1} (α := 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)
    ((algebraMap S T : (a : S) → T) ((algebraMap P.Ring S : (a : P.Ring) → S) P.jacobiMatrix.det : S) : T)

Tactic:
rw [AlgHom.map_det (aeval (Q.comp P).val), RingHom.map_det, RingHom.map_det]

Premises used: MvPolynomial.aeval, Algebra.PreSubmersivePresentation.toPresentation, AlgHom.map_det, RingHom.map_det, Algebra.PreSubmersivePresentation.comp, Algebra.Generators.val, 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
ι' : 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 : Fintype σ
inst_8 : Fintype σ'
e_M :
  Eq (α := Matrix σ σ T)
    ((AlgHom.mapMatrix (aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))) :
          (a : Matrix σ σ (MvPolynomial (ι' ⊕ ι) R)) → Matrix σ σ T)
        (Matrix.toBlocks₂₂ (jacobiMatrix (Q.comp P))) :
      Matrix σ σ T)
    ((RingHom.mapMatrix (algebraMap S T) : (a : Matrix σ σ S) → Matrix σ σ T)
        ((RingHom.mapMatrix (algebraMap P.Ring S) : (a : Matrix σ σ P.Ring) → Matrix σ σ S) P.jacobiMatrix) :
      Matrix σ σ T)
⊢ Eq.{u_3 + 1} (α := T)
    (Matrix.det.{u_3, t} (n := σ)
      ((AlgHom.mapMatrix (aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))) :
          (a : Matrix σ σ (MvPolynomial (ι' ⊕ ι) R)) → Matrix σ σ T)
        (Matrix.toBlocks₂₂ (jacobiMatrix (Q.comp P)))))
    (Matrix.det.{u_3, t} (n := σ)
      ((RingHom.mapMatrix (algebraMap S T) : (a : Matrix σ σ S) → Matrix σ σ T)
        ((RingHom.mapMatrix (algebraMap P.Ring S) : (a : Matrix σ σ P.Ring) → Matrix σ σ S) P.jacobiMatrix)))

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 : Fintype σ
inst_8 : Fintype σ'
e_M :
  ∀ (i j : σ),
    Eq.{u_3 + 1} (α := T)
      ((AlgHom.mapMatrix (aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))) :
            (a : Matrix σ σ (MvPolynomial (ι' ⊕ ι) R)) → Matrix σ σ T)
          (Matrix.toBlocks₂₂ (jacobiMatrix (Q.comp P))) i j :
        T)
      ((RingHom.mapMatrix (algebraMap S T) : (a : Matrix σ σ S) → Matrix σ σ T)
          ((RingHom.mapMatrix (algebraMap P.Ring S) : (a : Matrix σ σ P.Ring) → Matrix σ σ S) P.jacobiMatrix) i j :
        T)
⊢ Eq (α := Matrix σ σ T)
    ((AlgHom.mapMatrix (aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))) :
          (a : Matrix σ σ (MvPolynomial (ι' ⊕ ι) R)) → Matrix σ σ T)
        (Matrix.toBlocks₂₂ (jacobiMatrix (Q.comp P))) :
      Matrix σ σ T)
    ((RingHom.mapMatrix (algebraMap S T) : (a : Matrix σ σ S) → Matrix σ σ T)
        ((RingHom.mapMatrix (algebraMap P.Ring S) : (a : Matrix σ σ P.Ring) → Matrix σ σ S) P.jacobiMatrix) :
      Matrix σ σ T)

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
ι' : 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 : Fintype σ
inst_8 : Fintype σ'
i j : σ
e_M :
  (aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P)))) : (a : MvPolynomial (ι' ⊕ ι) R) → T)
      (jacobiMatrix (Q.comp P) (Sum.inr i) (Sum.inr j) :
        Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P)))) =
    eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap R S))
      (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) (P.jacobiMatrix i j)
⊢ Eq.{u_3 + 1} (α := T)
    ((AlgHom.mapMatrix (aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))) :
          (a : Matrix σ σ (MvPolynomial (ι' ⊕ ι) R)) → Matrix σ σ T)
        (Matrix.toBlocks₂₂ (jacobiMatrix (Q.comp P))) i j :
      T)
    ((RingHom.mapMatrix (algebraMap S T) : (a : Matrix σ σ S) → Matrix σ σ T)
        ((RingHom.mapMatrix (algebraMap P.Ring S) : (a : Matrix σ σ P.Ring) → Matrix σ σ S) P.jacobiMatrix) i j :
      T)

Tactic:
simp only [Matrix.toBlocks₂₂, AlgHom.mapMatrix_apply, Matrix.map_apply, Matrix.of_apply,
    RingHom.mapMatrix_apply, Generators.algebraMap_apply, map_aeval, coe_eval₂Hom]

Premises used: RingHom.mapMatrix_apply, MvPolynomial.map_aeval, Algebra.Generators.algebraMap_apply, Matrix.map_apply, AlgHom.mapMatrix_apply, Matrix.of_apply, MvPolynomial.coe_eval₂Hom, Matrix.toBlocks₂₂
-- 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 : Fintype σ
inst_8 : Fintype σ'
i j : σ
e_M :
  (aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P)))) : (a : MvPolynomial (ι' ⊕ ι) R) → T)
      ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.jacobiMatrix i j) :
        MvPolynomial (ι' ⊕ ι) R) =
    eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) (P.jacobiMatrix i j)
⊢ (aeval (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P)))) : (a : MvPolynomial (ι' ⊕ ι) R) → T)
      (jacobiMatrix (Q.comp P) (Sum.inr i) (Sum.inr j) :
        Generators.Ring (Presentation.toGenerators (toPresentation (Q.comp P)))) =
    eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap R S))
      (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) (P.jacobiMatrix i j)

Tactic:
rw [jacobiMatrix_comp_inr_inr, ← IsScalarTower.algebraMap_eq]

Premises used: IsScalarTower.algebraMap_eq, _private.0.Algebra.PreSubmersivePresentation.jacobiMatrix_comp_inr_inr
-- 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 : Fintype σ
inst_8 : Fintype σ'
i j : σ
e_M :
  ∀ (p : P.Ring),
    eval₂ (algebraMap R T) (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) p) =
      eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) p
⊢ eval₂ (algebraMap R T) (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))
      ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.jacobiMatrix i j)) =
    eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) (P.jacobiMatrix i j)

Tactic:
generalize P.jacobiMatrix i j = p

Premises used: 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 : Fintype σ
inst_8 : Fintype σ'
i j : σ
a : R
⊢ eval₂ (algebraMap R T) (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))
      ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) ((C : (a : R) → MvPolynomial ι R) a)) =
    eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) ((C : (a : R) → MvPolynomial ι R) a)

Tactic:
simp only [algHom_C, algebraMap_eq, eval₂_C]

Premises used: MvPolynomial.eval₂_C, MvPolynomial.algHom_C, MvPolynomial.algebraMap_eq
-- 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 : Fintype σ
inst_8 : Fintype σ'
i j : σ
p q : MvPolynomial ι R
hp :
  eval₂ (algebraMap R T) (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))
      ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) p) =
    eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) p
hq :
  eval₂ (algebraMap R T) (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))
      ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) q) =
    eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) q
⊢ eval₂ (algebraMap R T) (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))
      ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (p + q)) =
    eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) (p + q)

Tactic:
simp [hp, hq]
-- 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 : Fintype σ
inst_8 : Fintype σ'
i_1 j : σ
p : MvPolynomial ι R
i : ι
hp :
  eval₂ (algebraMap R T) (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))
      ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) p) =
    eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) p
e_M :
  eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) p *
      eval₂ (algebraMap R T) (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (X i)) =
    eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) p *
      eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) (X i)
⊢ eval₂ (algebraMap R T) (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))
      ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (p * X i)) =
    eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) (p * X i)

Tactic:
simp only [map_mul, eval₂_mul, hp]

Premises used: map_mul, MvPolynomial.eval₂_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 : Fintype σ
inst_8 : Fintype σ'
i_1 j : σ
p : MvPolynomial ι R
i : ι
hp :
  eval₂ (algebraMap R T) (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))
      ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) p) =
    eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) p
⊢ eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) p *
      eval₂ (algebraMap R T) (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (X i)) =
    eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) p *
      eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) (X i)

Tactic:
simp [Presentation.toGenerators_comp, toPresentation_comp]

Premises used: Algebra.Presentation.toGenerators_comp, Algebra.PreSubmersivePresentation.toPresentation_comp
-- 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 : Fintype σ
inst_8 : Fintype σ'
i j : σ
p : P.Ring
e_M :
  ∀ (a : R),
    eval₂ (algebraMap R T) (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) ((C : (a : R) → MvPolynomial ι R) a)) =
      eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i))
        ((C : (a : R) → MvPolynomial ι R) a)
e_M₁ :
  ∀ (p q : MvPolynomial ι R)
    (hp :
      eval₂ (algebraMap R T) (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))
          ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) p) =
        eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) p)
    (hq :
      eval₂ (algebraMap R T) (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))
          ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) q) =
        eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) q),
    eval₂ (algebraMap R T) (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (p + q)) =
      eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) (p + q)
e_M₂ :
  ∀ (p : MvPolynomial ι R) (i : ι)
    (hp :
      eval₂ (algebraMap R T) (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))
          ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) p) =
        eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) p),
    eval₂ (algebraMap R T) (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (p * X i)) =
      eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) (p * X i)
⊢ eval₂ (algebraMap R T) (Generators.val (Presentation.toGenerators (toPresentation (Q.comp P))))
      ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) p) =
    eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) p

Tactic:
induction p using MvPolynomial.induction_on with
  | C a =>
    simp only [algHom_C, algebraMap_eq, eval₂_C]
  | add p q hp hq => simp [hp, hq]
  | mul_X p i hp =>
    simp only [map_mul, eval₂_mul, hp]
    simp [Presentation.toGenerators_comp, toPresentation_comp]

Premises used: MvPolynomial.eval₂_C, Algebra.Presentation.toGenerators_comp, MvPolynomial.induction_on, MvPolynomial.algHom_C, map_mul, MvPolynomial.eval₂_mul, MvPolynomial.algebraMap_eq, Algebra.PreSubmersivePresentation.toPresentation_comp, MvPolynomial.C
-- 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 σ'
intro : ∀ (val : Fintype σ'), jacobian (Q.comp P) = P.jacobian • Q.jacobian
⊢ jacobian (Q.comp P) = P.jacobian • Q.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
ι' : 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 σ'
intro : ∀ (val : Fintype σ), jacobian (Q.comp P) = P.jacobian • Q.jacobian
⊢ jacobian (Q.comp P) = P.jacobian • Q.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
ι' : 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 :
  (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))))) =
    P.jacobian • Q.jacobian
⊢ jacobian (Q.comp P) = P.jacobian • Q.jacobian

Tactic:
rw [jacobian_eq_jacobiMatrix_det, ← Matrix.fromBlocks_toBlocks ((Q.comp P).jacobiMatrix),
    jacobiMatrix_comp_₁₂]

Premises used: Matrix.fromBlocks_toBlocks, _private.0.Algebra.PreSubmersivePresentation.jacobiMatrix_comp_₁₂, Algebra.PreSubmersivePresentation.comp, Algebra.PreSubmersivePresentation.jacobiMatrix, 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
ι' : 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 :
  (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)
intro :
  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
⊢ (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))))) =
    P.jacobian • Q.jacobian

Tactic:
convert_to
    (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₁₁.det *
    (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₂₂.det = P.jacobian • Q.jacobian

Premises used: MvPolynomial.aeval, Algebra.PreSubmersivePresentation.toPresentation, Algebra.PreSubmersivePresentation.jacobian, Matrix.toBlocks₁₁, Algebra.PreSubmersivePresentation.comp, Matrix.toBlocks₂₂, Algebra.Generators.val, Algebra.PreSubmersivePresentation.jacobiMatrix, DFunLike.coe, Algebra.Presentation.toGenerators, Matrix.det