-- Mathlib/RingTheory/CotangentLocalizationAway.lean
/--
Let `R → S → T` be algebras such that `T` is the localization of `S` away from one
element, where `S` is generated over `R` by `P` with kernel `I` and `Q` is the
canonical `S`-presentation of `T`. Denote by `J` the kernel of the composition
`R[X,Y] → T`. Then `T ⊗[S] (I/I²) → J/J²` is injective.
-/
@[stacks 08JZ "part of (1)"]
lemma liftBaseChange_injective_of_isLocalizationAway :
    Function.Injective (LinearMap.liftBaseChange T
      (Extension.Cotangent.map
        ((Generators.localizationAway g (S := T)).toComp P).toExtensionHom))

Proof state:
case h
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S
Q : Generators S T := localizationAway g
algInst✝ : Algebra P.Ring ((localizationAway g).comp P).Ring := ((localizationAway g).toComp P).toAlgHom.toAlgebra
f : P.Ring ⧸ P.ker ^ 2 := (Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)
π : ((localizationAway g).comp P).Ring →ₐ[R] Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) :=
  compLocalizationAwayAlgHom T g P
x : ↥P.toExtension.ker
hx :
  (lift
        (↑S
          (↑(LinearMap.ringLmapEquivSelf T T (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)).symm
            (Extension.Cotangent.map (Q.toComp P).toExtensionHom))))
      (((TensorProduct.mk S T P.toExtension.Cotangent) 1) (Extension.Cotangent.mk x)) =
    0
n : ℕ
hm : (Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g) ^ n * (Ideal.Quotient.mk (P.ker ^ 2)) ↑x = 0
⊢ ⟨g ^ n, ⋯⟩ • Extension.Cotangent.mk x = 0

Tactic:
rw [← map_pow, ← map_mul, Ideal.Quotient.eq_zero_iff_mem] at hm

Result:
case h
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S
Q : Generators S T := localizationAway g
algInst✝ : Algebra P.Ring ((localizationAway g).comp P).Ring := ((localizationAway g).toComp P).toAlgHom.toAlgebra
f : P.Ring ⧸ P.ker ^ 2 := (Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)
π : ((localizationAway g).comp P).Ring →ₐ[R] Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) :=
  compLocalizationAwayAlgHom T g P
x : ↥P.toExtension.ker
hx :
  (lift
        (↑S
          (↑(LinearMap.ringLmapEquivSelf T T (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)).symm
            (Extension.Cotangent.map (Q.toComp P).toExtensionHom))))
      (((TensorProduct.mk S T P.toExtension.Cotangent) 1) (Extension.Cotangent.mk x)) =
    0
n : ℕ
hm : P.σ g ^ n * ↑x ∈ P.ker ^ 2
⊢ ⟨g ^ n, ⋯⟩ • Extension.Cotangent.mk x = 0

Proof state:
case intro.a
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S
Q : Generators S T := localizationAway g
algInst✝ : Algebra P.Ring ((localizationAway g).comp P).Ring := ((localizationAway g).toComp P).toAlgHom.toAlgebra
f : P.Ring ⧸ P.ker ^ 2 := (Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)
π : ((localizationAway g).comp P).Ring →ₐ[R] Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) :=
  compLocalizationAwayAlgHom T g P
x : ↥P.toExtension.ker
hx :
  (lift
        (↑S
          (↑(LinearMap.ringLmapEquivSelf T T (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)).symm
            (Extension.Cotangent.map (Q.toComp P).toExtensionHom))))
      (((TensorProduct.mk S T P.toExtension.Cotangent) 1) (Extension.Cotangent.mk x)) =
    0
⊢ ((localizationAway g).toComp P).toAlgHom ↑x ∈ ((localizationAway g).comp P).ker ^ 2

Tactic:
simpa only [LinearEquiv.coe_coe, LinearMap.ringLmapEquivSelf_symm_apply,
  mk_apply, lift.tmul, LinearMap.coe_restrictScalars, LinearMap.coe_smulRight,
  LinearMap.one_apply, LinearMap.smul_apply, one_smul, Algebra.Extension.Cotangent.map_mk,
  Extension.Cotangent.mk_eq_zero_iff] using hx

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S
Q : Generators S T := localizationAway g
algInst✝ : Algebra P.Ring ((localizationAway g).comp P).Ring := ((localizationAway g).toComp P).toAlgHom.toAlgebra
f : P.Ring ⧸ P.ker ^ 2 := (Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)
π : ((localizationAway g).comp P).Ring →ₐ[R] Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) :=
  compLocalizationAwayAlgHom T g P
x : P.toExtension.Cotangent
hx :
  (lift
        (↑S
          (↑(LinearMap.ringLmapEquivSelf T T (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)).symm
            (Extension.Cotangent.map (Q.toComp P).toExtensionHom))))
      (((TensorProduct.mk S T P.toExtension.Cotangent) 1) x) =
    0
⊢ ((TensorProduct.mk S T P.toExtension.Cotangent) 1) x = 0

Tactic:
obtain ⟨x, rfl⟩ := Algebra.Extension.Cotangent.mk_surjective x

Result:
case intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S
Q : Generators S T := localizationAway g
algInst✝ : Algebra P.Ring ((localizationAway g).comp P).Ring := ((localizationAway g).toComp P).toAlgHom.toAlgebra
f : P.Ring ⧸ P.ker ^ 2 := (Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)
π : ((localizationAway g).comp P).Ring →ₐ[R] Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) :=
  compLocalizationAwayAlgHom T g P
x : ↥P.toExtension.ker
hx :
  (lift
        (↑S
          (↑(LinearMap.ringLmapEquivSelf T T (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)).symm
            (Extension.Cotangent.map (Q.toComp P).toExtensionHom))))
      (((TensorProduct.mk S T P.toExtension.Cotangent) 1) (Extension.Cotangent.mk x)) =
    0
⊢ ((TensorProduct.mk S T P.toExtension.Cotangent) 1) (Extension.Cotangent.mk x) = 0

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S
⊢ Function.Injective
    ⇑(LinearMap.liftBaseChange T (Extension.Cotangent.map ((localizationAway g).toComp P).toExtensionHom))

Tactic:
set Q := Generators.localizationAway g (S := T)

Result:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S
Q : Generators S T := localizationAway g
⊢ Function.Injective ⇑(LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))