awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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 : Eq (α := TensorProduct S (ResidueField S) Ω[S⁄R]) (1 ⊗ₜ[S] (KaehlerDifferential.D R S : (a : S) → Ω[S⁄R]) 0) 0
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
-- 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
⊢ 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₁ : ∀ (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])
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
-- 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])
⊢ 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₂ : ∀ (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])
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
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (hypothesis)
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
⊢ 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))
have this : EssFiniteType.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
Tactic: have : EssFiniteType (Localization.AtPrime p) (Localization.AtPrime q) := .of_comp R _ _
-- 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 : 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 ↔
    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))
have trans : IsUnramifiedAt R q ↔ FormallyUnramified.{u_2, u_1} (Localization.AtPrime p) (Localization.AtPrime q)
Tactic: trans Algebra.FormallyUnramified (Localization.AtPrime p) (Localization.AtPrime q)
-- 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 : 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)
⊢ 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))
have 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))
Tactic: trans Algebra.FormallyUnramified (Localization.AtPrime p) (Localization.AtPrime q)
-- 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 : 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)
⊢ 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))
have 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))
Tactic: rw [FormallyUnramified.iff_map_maximalIdeal_eq]
-- 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 : 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)
⊢ 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))
have a : 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)))
  (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
Tactic: congr!
-- 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 : 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)
⊢ 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)))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
have a : 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))
    (Localization.localRingHom p q (algebraMap R S) sorry) (maximalIdeal (Localization.AtPrime p)))
  (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
Tactic: rw [Localization.AtPrime.IsLiesOverAlgebra.algebraMap_eq,
    ← Localization.AtPrime.map_eq_maximalIdeal, Ideal.map_map, Localization.localRingHom,
    IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]
-- 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 : 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)
a :
  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))
      (Localization.localRingHom p q (algebraMap R S) ⋯) (maximalIdeal (Localization.AtPrime p)))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
⊢ 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)))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
have a₁ : 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))
    (Localization.localRingHom p q (algebraMap R S) sorry)
    (Ideal.map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p))
  (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
Tactic: rw [Localization.AtPrime.IsLiesOverAlgebra.algebraMap_eq,
    ← Localization.AtPrime.map_eq_maximalIdeal, Ideal.map_map, Localization.localRingHom,
    IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]
-- 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 : 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)
a :
  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))
      (Localization.localRingHom p q (algebraMap R S) ⋯) (maximalIdeal (Localization.AtPrime p)))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
a₁ :
  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))
      (Localization.localRingHom p q (algebraMap R S) ⋯)
      (Ideal.map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
⊢ 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)))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
have a₂ : Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime q))
  (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q))
    (RingHom.comp (β := Localization.AtPrime p) (Localization.localRingHom p q (algebraMap R S) sorry)
      (algebraMap R (Localization.AtPrime p)))
    p)
  (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
Tactic: rw [Localization.AtPrime.IsLiesOverAlgebra.algebraMap_eq,
    ← Localization.AtPrime.map_eq_maximalIdeal, Ideal.map_map, Localization.localRingHom,
    IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]
-- 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 : 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)
a :
  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))
      (Localization.localRingHom p q (algebraMap R S) ⋯) (maximalIdeal (Localization.AtPrime p)))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
a₁ :
  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))
      (Localization.localRingHom p q (algebraMap R S) ⋯)
      (Ideal.map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
a₂ :
  Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime q))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q))
      (RingHom.comp (β := Localization.AtPrime p) (Localization.localRingHom p q (algebraMap R S) ⋯)
        (algebraMap R (Localization.AtPrime p)))
      p)
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
⊢ 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)))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
have a₃ : Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime q))
  (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q))
    (@RingHom.comp _ (Localization.AtPrime p) _ _ Semiring.toNonAssocSemiring _
      (IsLocalization.map (M := p.primeCompl) (T := q.primeCompl) (Localization.AtPrime q) (algebraMap R S) sorry)
      (algebraMap R (Localization.AtPrime p)))
    p)
  (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
Tactic: rw [Localization.AtPrime.IsLiesOverAlgebra.algebraMap_eq,
    ← Localization.AtPrime.map_eq_maximalIdeal, Ideal.map_map, Localization.localRingHom,
    IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]
-- 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 : 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)
a :
  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))
      (Localization.localRingHom p q (algebraMap R S) ⋯) (maximalIdeal (Localization.AtPrime p)))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
a₁ :
  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))
      (Localization.localRingHom p q (algebraMap R S) ⋯)
      (Ideal.map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
a₂ :
  Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime q))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q))
      (RingHom.comp (β := Localization.AtPrime p) (Localization.localRingHom p q (algebraMap R S) ⋯)
        (algebraMap R (Localization.AtPrime p)))
      p)
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
a₃ :
  Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime q))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q))
      (@RingHom.comp _ (Localization.AtPrime p) _ _ Semiring.toNonAssocSemiring _
        (IsLocalization.map (M := p.primeCompl) (T := q.primeCompl) (Localization.AtPrime q) (algebraMap R S) ⋯)
        (algebraMap R (Localization.AtPrime p)))
      p)
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
⊢ 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)))
    (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
have a₄ : Eq.{u_2 + 1} (α := Ideal (Localization.AtPrime q))
  (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (Localization.AtPrime q)) (algebraMap R S)) p)
  (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p)
Tactic: rw [Localization.AtPrime.IsLiesOverAlgebra.algebraMap_eq,
    ← Localization.AtPrime.map_eq_maximalIdeal, Ideal.map_map, Localization.localRingHom,
    IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]