-- Mathlib/RingTheory/Kaehler/JacobiZariski.lean
lemma δAux_toAlgHom {Q : Generators.{u₁} S T}
    {Q' : Generators.{u₃} S T} (f : Hom Q Q') (x) :
    δAux R Q' (f.toAlgHom x) = δAux R Q x + Finsupp.linearCombination _ (δAux R Q' ∘ f.val)
      (Q.cotangentSpaceBasis.repr ((1 : T) ⊗ₜ[Q.Ring] D S Q.Ring x :))

Proof state:
case h_add
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
Q' : Generators S T
f : Q.Hom Q'
this✝ : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower Q.Ring Q.Ring T
x₁ x₂ : MvPolynomial Q.vars S
hx₁ :
  (δAux R Q') (f.toAlgHom x₁) =
    (δAux R Q) x₁ +
      (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val)) (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₁))
hx₂ :
  (δAux R Q') (f.toAlgHom x₂) =
    (δAux R Q) x₂ +
      (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val)) (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₂))
⊢ (δAux R Q) x₁ +
        (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val))
          (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₁)) +
      ((δAux R Q) x₂ +
        (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val))
          (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₂))) =
    (δAux R Q) x₁ + (δAux R Q) x₂ +
      ((Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val))
          (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₁)) +
        (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val))
          (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₂)))

Tactic:
rw [add_add_add_comm]

Result:
no goals

Proof state:
case h_add
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
Q' : Generators S T
f : Q.Hom Q'
this✝ : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower Q.Ring Q.Ring T
x₁ x₂ : MvPolynomial Q.vars S
hx₁ :
  (δAux R Q') (f.toAlgHom x₁) =
    (δAux R Q) x₁ +
      (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val)) (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₁))
hx₂ :
  (δAux R Q') (f.toAlgHom x₂) =
    (δAux R Q) x₂ +
      (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val)) (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₂))
⊢ (δAux R Q') (f.toAlgHom (x₁ + x₂)) =
    (δAux R Q) (x₁ + x₂) +
      (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val))
        (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) (x₁ + x₂)))

Tactic:
simp only [map_add, hx₁, hx₂, tmul_add]

Result:
case h_add
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
Q' : Generators S T
f : Q.Hom Q'
this✝ : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower Q.Ring Q.Ring T
x₁ x₂ : MvPolynomial Q.vars S
hx₁ :
  (δAux R Q') (f.toAlgHom x₁) =
    (δAux R Q) x₁ +
      (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val)) (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₁))
hx₂ :
  (δAux R Q') (f.toAlgHom x₂) =
    (δAux R Q) x₂ +
      (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val)) (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₂))
⊢ (δAux R Q) x₁ +
        (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val))
          (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₁)) +
      ((δAux R Q) x₂ +
        (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val))
          (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₂))) =
    (δAux R Q) x₁ + (δAux R Q) x₂ +
      ((Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val))
          (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₁)) +
        (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val))
          (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₂)))

Proof state:
case h_C
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
Q' : Generators S T
f : Q.Hom Q'
this✝ : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower Q.Ring Q.Ring T
s : S
⊢ (δAux R Q') (f.toAlgHom (C s)) =
    (δAux R Q) (C s) +
      (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val))
        (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) (C s)))

Tactic:
simp [MvPolynomial.algebraMap_eq, δAux_C]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
Q' : Generators S T
f : Q.Hom Q'
x : Q.Ring
this : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
⊢ (δAux R Q') (f.toAlgHom x) =
    (δAux R Q) x +
      (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val)) (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x))

Tactic:
have : IsScalarTower Q.Ring Q.Ring T := IsScalarTower.left _

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
Q' : Generators S T
f : Q.Hom Q'
x : Q.Ring
this✝ : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower Q.Ring Q.Ring T
⊢ (δAux R Q') (f.toAlgHom x) =
    (δAux R Q) x +
      (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val)) (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x))

Proof state:
case h_X
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
Q' : Generators S T
f : Q.Hom Q'
this✝ : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower Q.Ring Q.Ring T
p : MvPolynomial Q.vars S
n : Q.vars
IH :
  (δAux R Q') (f.toAlgHom p) =
    (δAux R Q) p +
      (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val)) (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) p))
⊢ Q.val n • (δAux R Q) p +
      (eval₂ (algebraMap S T) (fun i => Q.val i) p • (δAux R Q') (f.val n) +
        Q.val n •
          (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val))
            (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) p))) =
    Q.val n • (δAux R Q) p +
      ((aeval Q.val) p • (δAux R Q') (f.val n) +
        Q.val n •
          (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val))
            (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) p)))

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
Q' : Generators S T
f : Q.Hom Q'
x : Q.Ring
⊢ (δAux R Q') (f.toAlgHom x) =
    (δAux R Q) x +
      (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val)) (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x))

Tactic:
letI : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
Q' : Generators S T
f : Q.Hom Q'
x : Q.Ring
this : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
⊢ (δAux R Q') (f.toAlgHom x) =
    (δAux R Q) x +
      (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val)) (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x))