awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)
H : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
this_1 : FormallyUnramified.{u_2, u_1} (ResidueField R) (ResidueField S)
this : FormallyUnramified.{u_2, u_1} R (ResidueField S)
subsingleton_kaehlerDifferential : Subsingleton.{u_2 + 1} (TensorProduct S (ResidueField S) Ω[S⁄R])
⊢ Subsingleton.{u_2 + 1} Ω[S⁄R]

Tactic:
rw [← subsingleton_tensorProduct (R := S)]

Premises used: IsLocalRing.subsingleton_tensorProduct
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)
H : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
this_1 : FormallyUnramified.{u_2, u_1} (ResidueField R) (ResidueField S)
this : FormallyUnramified.{u_2, u_1} R (ResidueField S)
⊢ Subsingleton.{u_2 + 1} (TensorProduct S (ResidueField S) Ω[S⁄R])

Tactic:
subsingleton_of_forall_eq 0 fun x ↦ ?_

Premises used: subsingleton_of_forall_eq, OfNat.ofNat
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)
H : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
this_1 : FormallyUnramified.{u_2, u_1} (ResidueField R) (ResidueField S)
this : FormallyUnramified.{u_2, u_1} R (ResidueField S)
subsingleton_kaehlerDifferential : ∀ (x : TensorProduct S (ResidueField S) Ω[S⁄R]), x = 0
⊢ Subsingleton.{u_2 + 1} (TensorProduct S (ResidueField S) Ω[S⁄R])

Tactic:
refine subsingleton_of_forall_eq 0 fun x ↦ ?_

Premises used: subsingleton_of_forall_eq, OfNat.ofNat
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)
H : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
this_1 : FormallyUnramified.{u_2, u_1} (ResidueField R) (ResidueField S)
this : FormallyUnramified.{u_2, u_1} R (ResidueField S)
x : TensorProduct S (ResidueField S) Ω[S⁄R]
subsingleton_kaehlerDifferential :
  ∀ (x : Ideal.Cotangent (RingHom.ker (F := S →+* ResidueField S) (algebraMap S (ResidueField S)))),
    Eq (α := TensorProduct S (ResidueField S) Ω[S⁄R])
      ((KaehlerDifferential.kerCotangentToTensor R S (ResidueField S) :
            (a : (RingHom.ker (algebraMap S (ResidueField S))).Cotangent) → TensorProduct S (ResidueField S) Ω[S⁄R])
          x :
        TensorProduct S (ResidueField S) Ω[S⁄R])
      (0 : TensorProduct S (ResidueField S) Ω[S⁄R])
⊢ x = 0

Tactic:
obtain ⟨x, rfl⟩ := (KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange R S
    (ResidueField S) Ideal.Quotient.mk_surjective x).mp (Subsingleton.elim _ _)

Premises used: Ideal.Quotient.mk_surjective, KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange, IsLocalRing.ResidueField, Iff.mp, Subsingleton.elim, rfl
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)
H : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
this_1 : FormallyUnramified.{u_2, u_1} (ResidueField R) (ResidueField S)
this : FormallyUnramified.{u_2, u_1} R (ResidueField S)
x : Ideal.Cotangent (RingHom.ker (F := S →+* ResidueField S) (algebraMap S (ResidueField S)))
subsingleton_kaehlerDifferential :
  ∀ (x : S)
    (hx : Membership.mem (γ := Ideal S) (RingHom.ker (F := S →+* ResidueField S) (algebraMap S (ResidueField S))) x),
    Eq (α := TensorProduct S (ResidueField S) Ω[S⁄R])
      ((KaehlerDifferential.kerCotangentToTensor R S (ResidueField S) :
            (a : (RingHom.ker (algebraMap S (ResidueField S))).Cotangent) → TensorProduct S (ResidueField S) Ω[S⁄R])
          ((Ideal.toCotangent (RingHom.ker (F := S →+* ResidueField S) (algebraMap S (ResidueField S))) :
              (a : ↥(RingHom.ker (algebraMap S (ResidueField S)))) →
                (RingHom.ker (algebraMap S (ResidueField S))).Cotangent)
            (Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Ideal S) (RingHom.ker (F := S →+* ResidueField S) (algebraMap S (ResidueField S))) x)
              x hx)) :
        TensorProduct S (ResidueField S) Ω[S⁄R])
      (0 : TensorProduct S (ResidueField S) Ω[S⁄R])
⊢ Eq (α := TensorProduct S (ResidueField S) Ω[S⁄R])
    ((KaehlerDifferential.kerCotangentToTensor R S (ResidueField S) :
          (a : (RingHom.ker (algebraMap S (ResidueField S))).Cotangent) → TensorProduct S (ResidueField S) Ω[S⁄R])
        x :
      TensorProduct S (ResidueField S) Ω[S⁄R])
    (0 : TensorProduct S (ResidueField S) Ω[S⁄R])

Tactic:
obtain ⟨⟨x, hx⟩, rfl⟩ := Ideal.toCotangent_surjective _ x

Premises used: Ideal.toCotangent_surjective, rfl
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)
H : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
this_1 : FormallyUnramified.{u_2, u_1} (ResidueField R) (ResidueField S)
this : FormallyUnramified.{u_2, u_1} R (ResidueField S)
x : S
hx : Membership.mem (γ := Ideal S) (RingHom.ker (F := S →+* ResidueField S) (algebraMap S (ResidueField S))) x
subsingleton_kaehlerDifferential :
  Eq (α := TensorProduct S (ResidueField S) Ω[S⁄R])
    (1 ⊗ₜ[S] (KaehlerDifferential.D R S : (a : S) → Ω[S⁄R]) x : TensorProduct S (ResidueField S) Ω[S⁄R])
    (0 : TensorProduct S (ResidueField S) Ω[S⁄R])
⊢ Eq (α := TensorProduct S (ResidueField S) Ω[S⁄R])
    ((KaehlerDifferential.kerCotangentToTensor R S (ResidueField S) :
          (a : (RingHom.ker (algebraMap S (ResidueField S))).Cotangent) → TensorProduct S (ResidueField S) Ω[S⁄R])
        ((Ideal.toCotangent (RingHom.ker (F := S →+* ResidueField S) (algebraMap S (ResidueField S))) :
            (a : ↥(RingHom.ker (algebraMap S (ResidueField S)))) →
              (RingHom.ker (algebraMap S (ResidueField S))).Cotangent)
          (Subtype.mk (p := fun (x : S) ↦
            Membership.mem (γ := Ideal S) (RingHom.ker (F := S →+* ResidueField S) (algebraMap S (ResidueField S))) x) x
            hx)) :
      TensorProduct S (ResidueField S) Ω[S⁄R])
    (0 : TensorProduct S (ResidueField S) Ω[S⁄R])

Tactic:
simp only [KaehlerDifferential.kerCotangentToTensor_toCotangent]

Premises used: KaehlerDifferential.kerCotangentToTensor_toCotangent
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)
H : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
this_1 : FormallyUnramified.{u_2, u_1} (ResidueField R) (ResidueField S)
this : FormallyUnramified.{u_2, u_1} R (ResidueField S)
x : S
hx : Membership.mem (γ := Ideal S) (RingHom.ker (F := S →+* ResidueField S) (algebraMap S (ResidueField S))) x
⊢ Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) x

Tactic:
simpa [H] using hx
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)
H : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
this_1 : FormallyUnramified.{u_2, u_1} (ResidueField R) (ResidueField S)
this : FormallyUnramified.{u_2, u_1} R (ResidueField S)
x : S
hx : Membership.mem (γ := Ideal S) (RingHom.ker (F := S →+* ResidueField S) (algebraMap S (ResidueField S))) x
⊢ Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) x

Tactic:
replace hx : x ∈ Ideal.map (algebraMap R S) (maximalIdeal R) := by simpa [H] using hx
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)
H : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
this_1 : FormallyUnramified.{u_2, u_1} (ResidueField R) (ResidueField S)
this : FormallyUnramified.{u_2, u_1} R (ResidueField S)
x : S
⊢ Eq (α := TensorProduct S (ResidueField S) Ω[S⁄R]) (1 ⊗ₜ[S] (KaehlerDifferential.D R S : (a : S) → Ω[S⁄R]) 0) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)
H : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
this_1 : FormallyUnramified.{u_2, u_1} (ResidueField R) (ResidueField S)
this : FormallyUnramified.{u_2, u_1} R (ResidueField S)
x_1 x : S
h : Membership.mem (γ := Set S) ((⇑(algebraMap R S) : (a : R) → S) '' (↑(maximalIdeal R) : Set R)) x
subsingleton_kaehlerDifferential :
  ∀ (x : R) (hx : x ∈ (↑(maximalIdeal R) : Set R)),
    Eq (α := TensorProduct S (ResidueField S) Ω[S⁄R])
      (1 ⊗ₜ[S] (KaehlerDifferential.D R S : (a : S) → Ω[S⁄R]) ((algebraMap R S : (a : R) → S) x) :
        TensorProduct S (ResidueField S) Ω[S⁄R])
      (0 : TensorProduct S (ResidueField S) Ω[S⁄R])
⊢ Eq (α := TensorProduct S (ResidueField S) Ω[S⁄R])
    (1 ⊗ₜ[S] (KaehlerDifferential.D R S : (a : S) → Ω[S⁄R]) x : TensorProduct S (ResidueField S) Ω[S⁄R])
    (0 : TensorProduct S (ResidueField S) Ω[S⁄R])

Tactic:
obtain ⟨x, hx, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)
H : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
this_1 : FormallyUnramified.{u_2, u_1} (ResidueField R) (ResidueField S)
this : FormallyUnramified.{u_2, u_1} R (ResidueField S)
x_1 : S
x : R
hx : x ∈ (↑(maximalIdeal R) : Set R)
⊢ Eq (α := TensorProduct S (ResidueField S) Ω[S⁄R])
    (1 ⊗ₜ[S] (KaehlerDifferential.D R S : (a : S) → Ω[S⁄R]) ((algebraMap R S : (a : R) → S) x) :
      TensorProduct S (ResidueField S) Ω[S⁄R])
    (0 : TensorProduct S (ResidueField S) Ω[S⁄R])

Tactic:
simp
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)
H : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
this_1 : FormallyUnramified.{u_2, u_1} (ResidueField R) (ResidueField S)
this : FormallyUnramified.{u_2, u_1} R (ResidueField S)
x_1 x y : S
hx :
  Membership.mem (γ := Submodule S S)
    (Submodule.span S ((⇑(algebraMap R S) : (a : R) → S) '' (↑(maximalIdeal R) : Set R))) x
hy :
  Membership.mem (γ := Submodule S S)
    (Submodule.span S ((⇑(algebraMap R S) : (a : R) → S) '' (↑(maximalIdeal R) : Set R))) y
h :
  Eq (α := TensorProduct S (ResidueField S) Ω[S⁄R])
    (1 ⊗ₜ[S] (KaehlerDifferential.D R S : (a : S) → Ω[S⁄R]) x : TensorProduct S (ResidueField S) Ω[S⁄R])
    (0 : TensorProduct S (ResidueField S) Ω[S⁄R])
h_1 :
  Eq (α := TensorProduct S (ResidueField S) Ω[S⁄R])
    (1 ⊗ₜ[S] (KaehlerDifferential.D R S : (a : S) → Ω[S⁄R]) y : TensorProduct S (ResidueField S) Ω[S⁄R])
    (0 : TensorProduct S (ResidueField S) Ω[S⁄R])
⊢ Eq (α := TensorProduct S (ResidueField S) Ω[S⁄R])
    (1 ⊗ₜ[S] (KaehlerDifferential.D R S : (a : S) → Ω[S⁄R]) (x + y) : TensorProduct S (ResidueField S) Ω[S⁄R])
    (0 : TensorProduct S (ResidueField S) Ω[S⁄R])

Tactic:
simp [*, TensorProduct.tmul_add]

Premises used: TensorProduct.tmul_add
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)
H : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
this_1 : FormallyUnramified.{u_2, u_1} (ResidueField R) (ResidueField S)
this : FormallyUnramified.{u_2, u_1} R (ResidueField S)
x_1 a x : S
hx :
  Membership.mem (γ := Submodule S S)
    (Submodule.span S ((⇑(algebraMap R S) : (a : R) → S) '' (↑(maximalIdeal R) : Set R))) x
h :
  Eq (α := TensorProduct S (ResidueField S) Ω[S⁄R])
    (1 ⊗ₜ[S] (KaehlerDifferential.D R S : (a : S) → Ω[S⁄R]) x : TensorProduct S (ResidueField S) Ω[S⁄R])
    (0 : TensorProduct S (ResidueField S) Ω[S⁄R])
rwa : Membership.mem (γ := Ideal S) (maximalIdeal S) x
rwa₁ rwa₂ rwa₃ rwa₄ : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) x
⊢ Eq (α := ResidueField S) ((residue S : (a : S) → ResidueField S) x : ResidueField S) (0 : ResidueField S)

Tactic:
rwa [residue_eq_zero_iff, ← H]

Premises used: IsLocalRing.residue_eq_zero_iff
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)
H : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
this_1 : FormallyUnramified.{u_2, u_1} (ResidueField R) (ResidueField S)
this : FormallyUnramified.{u_2, u_1} R (ResidueField S)
x_1 a x : S
hx :
  Membership.mem (γ := Submodule S S)
    (Submodule.span S ((⇑(algebraMap R S) : (a : R) → S) '' (↑(maximalIdeal R) : Set R))) x
h :
  Eq (α := TensorProduct S (ResidueField S) Ω[S⁄R])
    (1 ⊗ₜ[S] (KaehlerDifferential.D R S : (a : S) → Ω[S⁄R]) x : TensorProduct S (ResidueField S) Ω[S⁄R])
    (0 : TensorProduct S (ResidueField S) Ω[S⁄R])
⊢ Eq (α := ResidueField S) ((residue S : (a : S) → ResidueField S) x : ResidueField S) (0 : ResidueField S)

Tactic:
have : residue S x = 0 := by rwa [residue_eq_zero_iff, ← H]
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)
H : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
this_1 : FormallyUnramified.{u_2, u_1} (ResidueField R) (ResidueField S)
this_2 : FormallyUnramified.{u_2, u_1} R (ResidueField S)
x_1 a x : S
hx :
  Membership.mem (γ := Submodule S S)
    (Submodule.span S ((⇑(algebraMap R S) : (a : R) → S) '' (↑(maximalIdeal R) : Set R))) x
h :
  Eq (α := TensorProduct S (ResidueField S) Ω[S⁄R])
    (1 ⊗ₜ[S] (KaehlerDifferential.D R S : (a : S) → Ω[S⁄R]) x : TensorProduct S (ResidueField S) Ω[S⁄R])
    (0 : TensorProduct S (ResidueField S) Ω[S⁄R])
this : Eq (α := ResidueField S) ((residue S : (a : S) → ResidueField S) x : ResidueField S) (0 : ResidueField S)
⊢ Eq (α := TensorProduct S (ResidueField S) Ω[S⁄R])
    (1 ⊗ₜ[S] (KaehlerDifferential.D R S : (a : S) → Ω[S⁄R]) (a • x) : TensorProduct S (ResidueField S) Ω[S⁄R])
    (0 : TensorProduct S (ResidueField S) Ω[S⁄R])

Tactic:
simp [*, TensorProduct.tmul_add, TensorProduct.smul_tmul', ← Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one, TensorProduct.smul_tmul', TensorProduct.tmul_add
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
⊢ FormallyUnramified R S ↔
    Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S) ∧
      Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)

Tactic:
⟨fun _ ↦ ⟨inferInstance, map_maximalIdeal⟩, fun ⟨_, e⟩ ↦ of_map_maximalIdeal e⟩

Premises used: Algebra.FormallyUnramified, _private.0.Algebra.FormallyUnramified.iff_map_maximalIdeal_eq.match_1, inferInstance, And.intro, Iff.intro, Algebra.FormallyUnramified.map_maximalIdeal, Algebra.FormallyUnramified.of_map_maximalIdeal
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_8 : Localization.AtPrime.IsLiesOverAlgebra p q
⊢ EssFiniteType.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)

Tactic:
have : EssFiniteType (Localization.AtPrime p) (Localization.AtPrime q) := .of_comp R _ _
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_8 : Localization.AtPrime.IsLiesOverAlgebra p q
this : EssFiniteType.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
trans : IsUnramifiedAt R q ↔ FormallyUnramified.{u_2, u_1} (Localization.AtPrime p) (Localization.AtPrime q)
trans₁ :
  FormallyUnramified.{u_2, u_1} (Localization.AtPrime p) (Localization.AtPrime q) ↔
    Algebra.IsSeparable.{u_1, u_2} p.ResidueField q.ResidueField ∧
      Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime q))
        (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
        (maximalIdeal (Localization.AtPrime q))
⊢ IsUnramifiedAt R q ↔
    Algebra.IsSeparable.{u_1, u_2} p.ResidueField q.ResidueField ∧
      Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime q))
        (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
        (maximalIdeal (Localization.AtPrime q))

Tactic:
trans Algebra.FormallyUnramified (Localization.AtPrime p) (Localization.AtPrime q)

Premises used: Localization.AtPrime, Algebra.FormallyUnramified
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_8 : Localization.AtPrime.IsLiesOverAlgebra p q
this : EssFiniteType.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
⊢ IsUnramifiedAt R q ↔ FormallyUnramified.{u_2, u_1} (Localization.AtPrime p) (Localization.AtPrime q)

Tactic:
⟨fun _ ↦ .of_restrictScalars R _ _,
      fun _ ↦ Algebra.FormallyUnramified.comp _ (Localization.AtPrime p) _⟩

Premises used: Localization.AtPrime, Algebra.FormallyUnramified.comp, Iff.intro, Algebra.FormallyUnramified.of_restrictScalars
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_8 : Localization.AtPrime.IsLiesOverAlgebra p q
this : EssFiniteType.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
⊢ IsUnramifiedAt R q ↔ FormallyUnramified.{u_2, u_1} (Localization.AtPrime p) (Localization.AtPrime q)

Tactic:
exact ⟨fun _ ↦ .of_restrictScalars R _ _,
      fun _ ↦ Algebra.FormallyUnramified.comp _ (Localization.AtPrime p) _⟩
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_8 : Localization.AtPrime.IsLiesOverAlgebra p q
this : EssFiniteType.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
rw :
  Algebra.IsSeparable.{u_1, u_2} (ResidueField (Localization.AtPrime p)) (ResidueField (Localization.AtPrime q)) ∧
      Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime q))
        (Ideal.map (R := Localization.AtPrime p) (F :=
          RingHom.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
          (algebraMap (Localization.AtPrime p) (Localization.AtPrime q)) (maximalIdeal (Localization.AtPrime p)))
        (maximalIdeal (Localization.AtPrime q)) ↔
    Algebra.IsSeparable.{u_1, u_2} p.ResidueField q.ResidueField ∧
      Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime q))
        (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
        (maximalIdeal (Localization.AtPrime q))
⊢ FormallyUnramified.{u_2, u_1} (Localization.AtPrime p) (Localization.AtPrime q) ↔
    Algebra.IsSeparable.{u_1, u_2} p.ResidueField q.ResidueField ∧
      Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime q))
        (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
        (maximalIdeal (Localization.AtPrime q))

Tactic:
rw [FormallyUnramified.iff_map_maximalIdeal_eq]

Premises used: Algebra.FormallyUnramified.iff_map_maximalIdeal_eq