-- Mathlib/RingTheory/Unramified/Basic.lean
theorem iff_comp_injective :
    FormallyUnramified R A ↔
      ∀ ⦃B : Type u⦄ [CommRing B],
        ∀ [Algebra R B] (I : Ideal B) (_ : I ^ 2 = ⊥),
          Function.Injective ((Ideal.Quotient.mkₐ R I).comp : (A →ₐ[R] B) → A →ₐ[R] B ⧸ I)

Proof state:
case mpr.subsingleton_kaehlerDifferential.mk.intro.intro.a.refine_2.H
R : Type v
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : Algebra R A
H :
  ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
h : Nontrivial (Ω[A⁄R])
f₁ f₂ : { f // (TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R A }
e : f₁ ≠ f₂
x : A
⊢ ((Ideal.Quotient.mkₐ R (RingHom.ker (TensorProduct.lmul' R).kerSquareLift.toRingHom)).comp ↑f₁) x =
    ((Ideal.Quotient.mkₐ R (RingHom.ker (TensorProduct.lmul' R).kerSquareLift.toRingHom)).comp ↑f₂) x

Tactic:
apply RingHom.kerLift_injective (TensorProduct.lmul' R (S := A)).kerSquareLift.toRingHom

Result:
case mpr.subsingleton_kaehlerDifferential.mk.intro.intro.a.refine_2.H.a
R : Type v
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : Algebra R A
H :
  ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
h : Nontrivial (Ω[A⁄R])
f₁ f₂ : { f // (TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R A }
e : f₁ ≠ f₂
x : A
⊢ (TensorProduct.lmul' R).kerSquareLift.kerLift
      (((Ideal.Quotient.mkₐ R (RingHom.ker (TensorProduct.lmul' R).kerSquareLift.toRingHom)).comp ↑f₁) x) =
    (TensorProduct.lmul' R).kerSquareLift.kerLift
      (((Ideal.Quotient.mkₐ R (RingHom.ker (TensorProduct.lmul' R).kerSquareLift.toRingHom)).comp ↑f₂) x)

Proof state:
case mpr.subsingleton_kaehlerDifferential
R : Type v
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : Algebra R A
H :
  ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
⊢ Subsingleton (Ω[A⁄R])

Tactic:
rw [← not_nontrivial_iff_subsingleton]

Result:
case mpr.subsingleton_kaehlerDifferential
R : Type v
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : Algebra R A
H :
  ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
⊢ ¬Nontrivial (Ω[A⁄R])

Proof state:
case mpr.subsingleton_kaehlerDifferential.mk.intro.intro
R : Type v
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : Algebra R A
H :
  ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
h : Nontrivial (Ω[A⁄R])
f₁ f₂ : { f // (TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R A }
e : f₁ ≠ f₂
⊢ False

Tactic:
apply e

Result:
case mpr.subsingleton_kaehlerDifferential.mk.intro.intro
R : Type v
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : Algebra R A
H :
  ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
h : Nontrivial (Ω[A⁄R])
f₁ f₂ : { f // (TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R A }
e : f₁ ≠ f₂
⊢ f₁ = f₂

Proof state:
case mpr.subsingleton_kaehlerDifferential.mk.intro.intro.a.refine_2.H.a
R : Type v
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : Algebra R A
H :
  ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
h : Nontrivial (Ω[A⁄R])
f₁ f₂ : { f // (TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R A }
e : f₁ ≠ f₂
x : A
⊢ (TensorProduct.lmul' R).kerSquareLift.kerLift
      (((Ideal.Quotient.mkₐ R (RingHom.ker (TensorProduct.lmul' R).kerSquareLift.toRingHom)).comp ↑f₁) x) =
    (TensorProduct.lmul' R).kerSquareLift.kerLift
      (((Ideal.Quotient.mkₐ R (RingHom.ker (TensorProduct.lmul' R).kerSquareLift.toRingHom)).comp ↑f₂) x)

Tactic:
simpa using DFunLike.congr_fun (f₁.2.trans f₂.2.symm) x

Result:
no goals

Proof state:
case mpr.subsingleton_kaehlerDifferential.mk.intro.intro.a.refine_1
R : Type v
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : Algebra R A
H :
  ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
h : Nontrivial (Ω[A⁄R])
f₁ f₂ : { f // (TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R A }
e : f₁ ≠ f₂
⊢ (RingHom.ker (TensorProduct.lmul' R).toRingHom).cotangentIdeal ^ 2 = ⊥

Tactic:
exact Ideal.cotangentIdeal_square _

Result:
no goals

Proof state:
case mpr.subsingleton_kaehlerDifferential
R : Type v
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : Algebra R A
H :
  ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
⊢ ¬Nontrivial (Ω[A⁄R])

Tactic:
intro h

Result:
case mpr.subsingleton_kaehlerDifferential
R : Type v
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : Algebra R A
H :
  ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
h : Nontrivial (Ω[A⁄R])
⊢ False

Proof state:
case mpr.subsingleton_kaehlerDifferential
R : Type v
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : Algebra R A
H :
  ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
h : Nontrivial (Ω[A⁄R])
⊢ False

Tactic:
obtain ⟨f₁, f₂, e⟩ := (KaehlerDifferential.endEquiv R A).injective.nontrivial

Result:
case mpr.subsingleton_kaehlerDifferential.mk.intro.intro
R : Type v
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : Algebra R A
H :
  ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
h : Nontrivial (Ω[A⁄R])
f₁ f₂ : { f // (TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R A }
e : f₁ ≠ f₂
⊢ False