-- 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
ι' : 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
intro₁ : ∀ (val : Fintype σ') (val : Fintype σ), jacobian (Q.comp P) = P.jacobian • Q.jacobian
intro₂ :
  ∀ (val : Fintype σ') (val_1 : Fintype σ),
    (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
h :
  ∀ (val : Fintype σ') (val_1 : Fintype σ),
    (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)
⊢ jacobian (Q.comp P) = P.jacobian • Q.jacobian
have intro₃ : ∀ (val : Fintype σ') (val_1 : Fintype σ),
  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: classical
  cases nonempty_fintype σ'
  cases nonempty_fintype σ
  rw [jacobian_eq_jacobiMatrix_det, ← Matrix.fromBlocks_toBlocks ((Q.comp P).jacobiMatrix),
    jacobiMatrix_comp_₁₂]
  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
  · simp only [Generators.algebraMap_apply, ← map_mul]
    congr
    convert!
      Matrix.det_fromBlocks_zero₁₂ (Q.comp P).jacobiMatrix.toBlocks₁₁
        (Q.comp P).jacobiMatrix.toBlocks₂₁ (Q.comp P).jacobiMatrix.toBlocks₂₂
  · rw [jacobiMatrix_comp_₁₁_det, jacobiMatrix_comp_₂₂_det, mul_comm, Algebra.smul_def]