-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
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) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) x
subsingleton_kaehlerDifferential :
  Eq (α := TensorProduct S (ResidueField S) Ω[S⁄R]) (1 ⊗ₜ[S] (KaehlerDifferential.D R S : (a : S) → Ω[S⁄R]) 0) 0
subsingleton_kaehlerDifferential₁ :
  ∀ (x : S) (h : Membership.mem (γ := Set S) ((⇑(algebraMap R S) : (a : R) → S) '' (↑(maximalIdeal R) : Set R)) x),
    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])
subsingleton_kaehlerDifferential₂ :
  ∀ (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),
    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])
          (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])
⊢ 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])
have subsingleton_kaehlerDifferential₃ : ∀ (a x : S)
  (hx :
    Membership.mem (γ := Submodule S S)
      (Submodule.span S ((⇑(algebraMap R S) : (a : R) → S) '' (↑(maximalIdeal R) : Set R))) x),
  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])
      (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: induction hx using Submodule.span_induction with
  | zero => simp
  | mem x h => obtain ⟨x, hx, rfl⟩ := h; simp
  | add x y hx hy _ _ => simp [*, TensorProduct.tmul_add]
  | smul a x hx _ =>
    have : residue S x = 0 := by rwa [residue_eq_zero_iff, ← H]
    simp [*, TensorProduct.tmul_add, TensorProduct.smul_tmul', ← Algebra.algebraMap_eq_smul_one]
Cleared hypotheses: hx