Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case h.add
R : Type u₁
S : Type u₂
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
T : Type u₃
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
inst✝ : Flat S T
x y : T ⊗[S] P.toExtension.H1Cotangent
hx :
  ∀
    (x_in :
      (liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)) ((lTensor T Extension.h1Cotangentι) x) ∈
        (Q.comp P).toExtension.cotangentComplex.ker),
    (liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)) x =
      ⟨(liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)) ((lTensor T Extension.h1Cotangentι) x),
        x_in⟩
hy :
  ∀
    (x_in :
      (liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)) ((lTensor T Extension.h1Cotangentι) y) ∈
        (Q.comp P).toExtension.cotangentComplex.ker),
    (liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)) y =
      ⟨(liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)) ((lTensor T Extension.h1Cotangentι) y),
        x_in⟩
x_in :
  (liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))
      ((lTensor T Extension.h1Cotangentι) (x + y)) ∈
    (Q.comp P).toExtension.cotangentComplex.ker
⊢ (↑((liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)) (x + y))).val =
    (↑⟨(liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))
            ((lTensor T Extension.h1Cotangentι) (x + y)),
          x_in⟩).val

Tactic:
;

Goal state after:
case h.add
R : Type u₁
S : Type u₂
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
T : Type u₃
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
inst✝ : Flat S T
x y : T ⊗[S] P.toExtension.H1Cotangent
hx :
  ∀
    (x_in :
      (liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)) ((lTensor T Extension.h1Cotangentι) x) ∈
        (Q.comp P).toExtension.cotangentComplex.ker),
    (liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)) x =
      ⟨(liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)) ((lTensor T Extension.h1Cotangentι) x),
        x_in⟩
hy :
  ∀
    (x_in :
      (liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)) ((lTensor T Extension.h1Cotangentι) y) ∈
        (Q.comp P).toExtension.cotangentComplex.ker),
    (liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)) y =
      ⟨(liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)) ((lTensor T Extension.h1Cotangentι) y),
        x_in⟩
x_in :
  (liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))
      ((lTensor T Extension.h1Cotangentι) (x + y)) ∈
    (Q.comp P).toExtension.cotangentComplex.ker
⊢ (↑((liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)) (x + y))).val =
    (↑⟨(liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))
            ((lTensor T Extension.h1Cotangentι) (x + y)),
          x_in⟩).val