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
ι' : 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
⊢ 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
have 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)
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]
Cleared hypotheses: p
-- 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 : 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)
⊢ 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
have 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)
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]
Cleared hypotheses: p
-- 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 : 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)
⊢ 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
have 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)
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]
Cleared hypotheses: p
-- 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 σ'
⊢ jacobian (Q.comp P) = P.jacobian • Q.jacobian
have intro : ∀ (val : Fintype σ'), jacobian (Q.comp P) = P.jacobian • Q.jacobian
Tactic: cases nonempty_fintype σ'
-- 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 σ'
val : Fintype σ'
⊢ jacobian (Q.comp P) = P.jacobian • Q.jacobian
have intro : ∀ (val : Fintype σ), jacobian (Q.comp P) = P.jacobian • Q.jacobian
Tactic: cases nonempty_fintype σ
-- 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 σ'
val : Fintype σ'
val_1 : Fintype σ
⊢ jacobian (Q.comp P) = P.jacobian • Q.jacobian
have 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
Tactic: rw [jacobian_eq_jacobiMatrix_det, ← Matrix.fromBlocks_toBlocks ((Q.comp P).jacobiMatrix),
    jacobiMatrix_comp_₁₂]
-- 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 σ'
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
have 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)
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
-- 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 σ'
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)
⊢ (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
have 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
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
-- 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 σ'
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)
have 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)
Tactic: simp only [Generators.algebraMap_apply, ← map_mul]
-- 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 σ'
val : Fintype σ'
val_1 : Fintype σ
⊢ 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)
have 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))))
Tactic: congr
-- 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 σ'
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
have 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
Tactic: rw [jacobiMatrix_comp_₁₁_det, jacobiMatrix_comp_₂₂_det, mul_comm, Algebra.smul_def]
-- 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 σ'
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
⊢ 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
have intro₁ : HMul.hMul (β := T) Q.jacobian ((algebraMap S T : (a : S) → T) P.jacobian : T) = P.jacobian • Q.jacobian
Tactic: rw [jacobiMatrix_comp_₁₁_det, jacobiMatrix_comp_₂₂_det, mul_comm, Algebra.smul_def]
-- 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 σ'
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
⊢ 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
have intro₂ : HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) P.jacobian : T) Q.jacobian = P.jacobian • Q.jacobian
Tactic: rw [jacobiMatrix_comp_₁₁_det, jacobiMatrix_comp_₂₂_det, mul_comm, Algebra.smul_def]