-- Mathlib/RingTheory/Kaehler/Basic.lean
theorem KaehlerDifferential.End_equiv_aux (f : S →ₐ[R] S ⊗ S ⧸ KaehlerDifferential.ideal R S ^ 2) :
    (Ideal.Quotient.mkₐ R (KaehlerDifferential.ideal R S).cotangentIdeal).comp f =
        IsScalarTower.toAlgHom R S _ ↔
      (TensorProduct.lmul' R : S ⊗[R] S →ₐ[R] S).kerSquareLift.comp f = AlgHom.id R S

Proof state:
case h.mpr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ ideal R S ^ 2
x : S
e₁ :
  (TensorProduct.lmul' R).kerSquareLift (f x) =
    (quotientCotangentIdealRingEquiv R S) ((Ideal.Quotient.mk (ideal R S).cotangentIdeal) (f x))
e₂ :
  x =
    (quotientCotangentIdealRingEquiv R S)
      ((IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) x)
⊢ ((TensorProduct.lmul' R).kerSquareLift.comp f) x = (AlgHom.id R S) x →
    ((Ideal.Quotient.mkₐ R (ideal R S).cotangentIdeal).comp f) x =
      (IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) x

Tactic:
intro e

Result:
case h.mpr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ ideal R S ^ 2
x : S
e₁ :
  (TensorProduct.lmul' R).kerSquareLift (f x) =
    (quotientCotangentIdealRingEquiv R S) ((Ideal.Quotient.mk (ideal R S).cotangentIdeal) (f x))
e₂ :
  x =
    (quotientCotangentIdealRingEquiv R S)
      ((IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) x)
e : ((TensorProduct.lmul' R).kerSquareLift.comp f) x = (AlgHom.id R S) x
⊢ ((Ideal.Quotient.mkₐ R (ideal R S).cotangentIdeal).comp f) x =
    (IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) x

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ ideal R S ^ 2
⊢ (Ideal.Quotient.mkₐ R (ideal R S).cotangentIdeal).comp f =
      IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal) ↔
    (TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R S

Tactic:
rw [AlgHom.ext_iff, AlgHom.ext_iff]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ ideal R S ^ 2
⊢ (∀ (x : S),
      ((Ideal.Quotient.mkₐ R (ideal R S).cotangentIdeal).comp f) x =
        (IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) x) ↔
    ∀ (x : S), ((TensorProduct.lmul' R).kerSquareLift.comp f) x = (AlgHom.id R S) x

Proof state:
case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ ideal R S ^ 2
x : S
e₁ :
  (TensorProduct.lmul' R).kerSquareLift (f x) =
    (quotientCotangentIdealRingEquiv R S) ((Ideal.Quotient.mk (ideal R S).cotangentIdeal) (f x))
e₂ :
  x =
    (quotientCotangentIdealRingEquiv R S)
      ((IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) x)
⊢ ((Ideal.Quotient.mkₐ R (ideal R S).cotangentIdeal).comp f) x =
      (IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) x ↔
    ((TensorProduct.lmul' R).kerSquareLift.comp f) x = (AlgHom.id R S) x

Tactic:
constructor

Result:
case h.mp
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ ideal R S ^ 2
x : S
e₁ :
  (TensorProduct.lmul' R).kerSquareLift (f x) =
    (quotientCotangentIdealRingEquiv R S) ((Ideal.Quotient.mk (ideal R S).cotangentIdeal) (f x))
e₂ :
  x =
    (quotientCotangentIdealRingEquiv R S)
      ((IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) x)
⊢ ((Ideal.Quotient.mkₐ R (ideal R S).cotangentIdeal).comp f) x =
      (IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) x →
    ((TensorProduct.lmul' R).kerSquareLift.comp f) x = (AlgHom.id R S) x

case h.mpr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ ideal R S ^ 2
x : S
e₁ :
  (TensorProduct.lmul' R).kerSquareLift (f x) =
    (quotientCotangentIdealRingEquiv R S) ((Ideal.Quotient.mk (ideal R S).cotangentIdeal) (f x))
e₂ :
  x =
    (quotientCotangentIdealRingEquiv R S)
      ((IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) x)
⊢ ((TensorProduct.lmul' R).kerSquareLift.comp f) x = (AlgHom.id R S) x →
    ((Ideal.Quotient.mkₐ R (ideal R S).cotangentIdeal).comp f) x =
      (IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) x

Proof state:
case intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ ideal R S ^ 2
x : S
y : S ⊗[R] S
⊢ (TensorProduct.lmul' R).kerSquareLift ((Ideal.Quotient.mk (ideal R S ^ 2)) y) =
    (quotientCotangentIdealRingEquiv R S)
      ((Ideal.Quotient.mk (ideal R S).cotangentIdeal) ((Ideal.Quotient.mk (ideal R S ^ 2)) y))

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ ideal R S ^ 2
x : S
y : S ⊗[R] S ⧸ ideal R S ^ 2
⊢ (TensorProduct.lmul' R).kerSquareLift y =
    (quotientCotangentIdealRingEquiv R S) ((Ideal.Quotient.mk (ideal R S).cotangentIdeal) y)

Tactic:
obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective y

Result:
case intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ ideal R S ^ 2
x : S
y : S ⊗[R] S
⊢ (TensorProduct.lmul' R).kerSquareLift ((Ideal.Quotient.mk (ideal R S ^ 2)) y) =
    (quotientCotangentIdealRingEquiv R S)
      ((Ideal.Quotient.mk (ideal R S).cotangentIdeal) ((Ideal.Quotient.mk (ideal R S ^ 2)) y))

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ ideal R S ^ 2
⊢ (∀ (x : S),
      ((Ideal.Quotient.mkₐ R (ideal R S).cotangentIdeal).comp f) x =
        (IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) x) ↔
    ∀ (x : S), ((TensorProduct.lmul' R).kerSquareLift.comp f) x = (AlgHom.id R S) x

Tactic:
apply forall_congr'

Result:
case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ ideal R S ^ 2
⊢ ∀ (a : S),
    ((Ideal.Quotient.mkₐ R (ideal R S).cotangentIdeal).comp f) a =
        (IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) a ↔
      ((TensorProduct.lmul' R).kerSquareLift.comp f) a = (AlgHom.id R S) a