awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Ideal R
inst_3 : P.IsPrime
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : Q.LiesOver P
inst_6 : IsUnramifiedAt R Q
x : S
p : R[X]
inst_7 : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q)
inst_8 : Localization.AtPrime.IsLiesOverAlgebra P Q
hp₁ :
  Eq (α := Ideal P.ResidueField[X]) (Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p})
    (RingHom.ker (F := P.ResidueField[X] →+* P.ResidueField ⊗[R] S) (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x))))
hp₂ : Eq (α := Subalgebra R S) R[x] ⊤
Q' : Ideal (P.Fiber S) :=
  PrimeSpectrum.asIdeal
    ((PrimeSpectrum.primesOverOrderIsoFiber R S P : (a : (↑(P.primesOver S) : Type u_3)) → PrimeSpectrum (P.Fiber S))
      (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q ⋯))
this_1 : Q'.LiesOver Q
this_2 : Q'.LiesOver P
this_3 : Algebra (Localization.AtPrime Q) (Localization.AtPrime Q') :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this_4 : Algebra (Localization.AtPrime P) (Localization.AtPrime Q') :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this_5 : IsUnramifiedAt P.ResidueField (A := P.Fiber S) Q'
this :
  Function.Surjective (α := P.ResidueField[X]) (β := P.ResidueField ⊗[R] S)
    (⇑(aeval (1 ⊗ₜ[R] x)) : (a : P.ResidueField[X]) → P.ResidueField ⊗[R] S)
r : IsLocalRing.ResidueField (Localization.AtPrime P)
h :
  ∀ (x : R),
    Eq (α := IsLocalRing.ResidueField (Localization.AtPrime Q'))
      ((@RingHom.comp _ P.ResidueField _ _ Semiring.toNonAssocSemiring _
              (algebraMap (IsLocalRing.ResidueField (Localization.AtPrime P))
                (IsLocalRing.ResidueField (Localization.AtPrime Q')))
              (algebraMap R P.ResidueField) :
            (a : R) → IsLocalRing.ResidueField (Localization.AtPrime Q'))
          x :
        IsLocalRing.ResidueField (Localization.AtPrime Q'))
      ((@RingHom.comp _ P.ResidueField _ _ Semiring.toNonAssocSemiring _
              (algebraMap (IsLocalRing.ResidueField (Localization.AtPrime P))
                (IsLocalRing.ResidueField (Localization.AtPrime Q')))
              (algebraMap R P.ResidueField) :
            (a : R) → IsLocalRing.ResidueField (Localization.AtPrime Q'))
          x :
        IsLocalRing.ResidueField (Localization.AtPrime Q'))
⊢ Eq (α := IsLocalRing.ResidueField (Localization.AtPrime P) →+* IsLocalRing.ResidueField (Localization.AtPrime Q'))
    (algebraMap (IsLocalRing.ResidueField (Localization.AtPrime P))
      (IsLocalRing.ResidueField (Localization.AtPrime Q')))
    (algebraMap (IsLocalRing.ResidueField (Localization.AtPrime P))
      (IsLocalRing.ResidueField (Localization.AtPrime Q')))

Tactic:
ext x
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Ideal R
inst_3 : P.IsPrime
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : Q.LiesOver P
inst_6 : IsUnramifiedAt R Q
x_1 : S
p : R[X]
inst_7 : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q)
inst_8 : Localization.AtPrime.IsLiesOverAlgebra P Q
hp₁ :
  Eq (α := Ideal P.ResidueField[X]) (Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p})
    (RingHom.ker (F := P.ResidueField[X] →+* P.ResidueField ⊗[R] S) (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x_1))))
hp₂ : Eq (α := Subalgebra R S) R[x_1] ⊤
Q' : Ideal (P.Fiber S) :=
  PrimeSpectrum.asIdeal
    ((PrimeSpectrum.primesOverOrderIsoFiber R S P : (a : (↑(P.primesOver S) : Type u_3)) → PrimeSpectrum (P.Fiber S))
      (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q ⋯))
this_1 : Q'.LiesOver Q
this_2 : Q'.LiesOver P
this_3 : Algebra (Localization.AtPrime Q) (Localization.AtPrime Q') :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this_4 : Algebra (Localization.AtPrime P) (Localization.AtPrime Q') :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this_5 : IsUnramifiedAt P.ResidueField (A := P.Fiber S) Q'
this :
  Function.Surjective (α := P.ResidueField[X]) (β := P.ResidueField ⊗[R] S)
    (⇑(aeval (1 ⊗ₜ[R] x_1)) : (a : P.ResidueField[X]) → P.ResidueField ⊗[R] S)
r : IsLocalRing.ResidueField (Localization.AtPrime P)
x : R
⊢ Eq (α := IsLocalRing.ResidueField (Localization.AtPrime Q'))
    ((@RingHom.comp _ P.ResidueField _ _ Semiring.toNonAssocSemiring _
            (algebraMap (IsLocalRing.ResidueField (Localization.AtPrime P))
              (IsLocalRing.ResidueField (Localization.AtPrime Q')))
            (algebraMap R P.ResidueField) :
          (a : R) → IsLocalRing.ResidueField (Localization.AtPrime Q'))
        x :
      IsLocalRing.ResidueField (Localization.AtPrime Q'))
    ((@RingHom.comp _ P.ResidueField _ _ Semiring.toNonAssocSemiring _
            (algebraMap (IsLocalRing.ResidueField (Localization.AtPrime P))
              (IsLocalRing.ResidueField (Localization.AtPrime Q')))
            (algebraMap R P.ResidueField) :
          (a : R) → IsLocalRing.ResidueField (Localization.AtPrime Q'))
        x :
      IsLocalRing.ResidueField (Localization.AtPrime Q'))

Tactic:
simp [← IsScalarTower.algebraMap_apply]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Ideal R
inst_3 : P.IsPrime
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : Q.LiesOver P
inst_6 : IsUnramifiedAt R Q
x : S
p : R[X]
inst_7 : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q)
inst_8 : Localization.AtPrime.IsLiesOverAlgebra P Q
hp₁ :
  Eq (α := Ideal P.ResidueField[X]) (Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p})
    (RingHom.ker (F := P.ResidueField[X] →+* P.ResidueField ⊗[R] S) (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x))))
hp₂ : Eq (α := Subalgebra R S) R[x] ⊤
Q' : Ideal (P.Fiber S) :=
  PrimeSpectrum.asIdeal
    ((PrimeSpectrum.primesOverOrderIsoFiber R S P : (a : (↑(P.primesOver S) : Type u_3)) → PrimeSpectrum (P.Fiber S))
      (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q ⋯))
this_1 : Q'.LiesOver Q
this_2 : Q'.LiesOver P
this_3 : Algebra (Localization.AtPrime Q) (Localization.AtPrime Q') :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this_4 : Algebra (Localization.AtPrime P) (Localization.AtPrime Q') :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this_5 : IsUnramifiedAt P.ResidueField (A := P.Fiber S) Q'
this :
  Function.Surjective (α := P.ResidueField[X]) (β := P.ResidueField ⊗[R] S)
    (⇑(aeval (1 ⊗ₜ[R] x)) : (a : P.ResidueField[X]) → P.ResidueField ⊗[R] S)
⊢ Eq (α := Q'.ResidueField (R := P.Fiber S))
    ((IsScalarTower.toAlgHom P.ResidueField Q.ResidueField (Q'.ResidueField (R := P.Fiber S)) :
          (a : Q.ResidueField) → Q'.ResidueField)
        ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) x) :
      Q'.ResidueField (R := P.Fiber S))
    ((algebraMap (P.Fiber S) (Q'.ResidueField (R := P.Fiber S)) : (a : P.Fiber S) → Q'.ResidueField) (1 ⊗ₜ[R] x) :
      Q'.ResidueField (R := P.Fiber S))

Tactic:
simp [← TensorProduct.right_algebraMap_apply, ← IsScalarTower.algebraMap_apply]

Premises used: Algebra.TensorProduct.right_algebraMap_apply, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
H : ∃ (x : S), Eq (α := Subalgebra R S) R[x] ⊤
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
inl : Subsingleton S → ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
inr : Nontrivial S → ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

Tactic:
cases subsingleton_or_nontrivial S

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
H : ∃ (x : S), Eq (α := Subalgebra R S) R[x] ⊤
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Subsingleton S
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

Tactic:
cases Ideal.IsPrime.ne_top' (Subsingleton.elim Q ⊤)

Premises used: Subsingleton.elim, Top.top, Ideal.IsPrime.ne_top'
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
H : ∃ (x : S), Eq (α := Subalgebra R S) R[x] ⊤
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
⊢ Nontrivial R

Tactic:
have := (algebraMap R S).domain_nontrivial
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
H : ∃ (x : S), Eq (α := Subalgebra R S) R[x] ⊤
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
this_1 : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver P Q
inr : ∀ (x : S) (hx : Eq (α := Subalgebra R S) R[x] ⊤), ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

Tactic:
obtain ⟨x, hx⟩ := H
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
this_1 : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
⊢ IsIntegral R x

Tactic:
have hRx : IsIntegral R x := IsIntegral.isIntegral _
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
this_1 : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))
⊢ Function.Surjective.{u_1 + 1, u_3 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)

Tactic:
have hx' : Function.Surjective (aeval (R := R) x) :=
    (AlgHom.range_eq_top _).mp ((adjoin_singleton_eq_range_aeval R x).symm.trans hx)
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
this_1 : Nontrivial R
P : Ideal R := Ideal.under R Q
this_2 : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))
hx' : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
this :
  ∃ (q : R[X]),
    q.Monic ∧
      Eq.{u_3 + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S) ∧
        ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉ Q
obtain :
  ∀ (q : R[X]) (hq : q.Monic) (hqx : Eq.{u_3 + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S))
    (hq'x : ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉ Q),
    ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

Tactic:
obtain ⟨q, hq, hqx, hq'x⟩ := this
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
this_1 : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))
hx' : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
q : R[X]
hq : q.Monic
hqx : Eq.{u_3 + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S)
hq'x : ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉ Q
⊢ HMul.hMul (α := R[X]) (β := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X]) (1 : R[X]) + q * 0 =
    HPow.hPow (α := R[X]) (β := ℕ) ((derivative : (a : R[X]) → R[X]) q : R[X]) 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
this_1 : Nontrivial R
P_1 : Ideal R := Ideal.under R Q
this : Algebra.{u_1, u_3} (Localization.AtPrime P_1) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver P_1 Q
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))
hx' : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
q : R[X]
hq : q.Monic
hqx : Eq.{u_3 + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S)
hq'x : ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉ Q
P : StandardEtalePair R := { f := q, monic_f := hq, g := (derivative : (a : R[X]) → R[X]) q, cond := ⋯ }
⊢ Eq.{u_3 + 1} (α :=
    Localization.Away (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S))
    (((aeval
              ((algebraMap S
                    (Localization.Away (M := S)
                      ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S)) :
                  (a : S) → Localization.Away ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q)))
                x) :
            AlgHom.{u_1, u_1, u_3} R R[X]
              (Localization.Away (M := S)
                ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S))) :
          (a : R[X]) → Localization.Away ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q)))
        P.f :
      Localization.Away (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S))
    (0 : Localization.Away (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S))

Tactic:
simp_all [P]
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
this_1 : Nontrivial R
P_1 : Ideal R := Ideal.under R Q
this : Algebra.{u_1, u_3} (Localization.AtPrime P_1) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver P_1 Q
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))
hx' : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
q : R[X]
hq : q.Monic
hqx : Eq.{u_3 + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S)
hq'x : ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉ Q
P : StandardEtalePair R := { f := q, monic_f := hq, g := (derivative : (a : R[X]) → R[X]) q, cond := ⋯ }
⊢ IsUnit.{u_3} (M :=
    Localization.Away (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S))
    (((aeval
              ((algebraMap S
                    (Localization.Away (M := S)
                      ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S)) :
                  (a : S) → Localization.Away ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q)))
                x) :
            AlgHom.{u_1, u_1, u_3} R R[X]
              (Localization.Away (M := S)
                ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S))) :
          (a : R[X]) → Localization.Away ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q)))
        P.g :
      Localization.Away (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S))

Tactic:
simpa using IsLocalization.Away.algebraMap_isUnit _

Premises used: IsLocalization.Away.algebraMap_isUnit
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
this_1 : Nontrivial R
P_1 : Ideal R := Ideal.under R Q
this : Algebra.{u_1, u_3} (Localization.AtPrime P_1) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver P_1 Q
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))
hx' : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
q : R[X]
hq : q.Monic
hqx : Eq.{u_3 + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S)
hq'x : ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉ Q
P : StandardEtalePair R := { f := q, monic_f := hq, g := (derivative : (a : R[X]) → R[X]) q, cond := ⋯ }
⊢ P.HasMap (S :=
    Localization.Away (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S))
    ((algebraMap S
            (Localization.Away (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S)) :
          (a : S) → Localization.Away ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q)))
        x :
      Localization.Away (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S))

Tactic:
have hP : P.HasMap (algebraMap _ (Localization.Away (aeval x q.derivative)) x) :=
      ⟨by simp_all [P], by simpa using IsLocalization.Away.algebraMap_isUnit _⟩
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
this_1 : Nontrivial R
P_1 : Ideal R := Ideal.under R Q
this : Algebra.{u_1, u_3} (Localization.AtPrime P_1) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver P_1 Q
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))
hx' : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
q : R[X]
hq : q.Monic
hqx : Eq.{u_3 + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S)
hq'x : ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉ Q
P : StandardEtalePair R := { f := q, monic_f := hq, g := (derivative : (a : R[X]) → R[X]) q, cond := ⋯ }
hP :
  P.HasMap (S :=
    Localization.Away (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S))
    ((algebraMap S
            (Localization.Away (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S)) :
          (a : S) → Localization.Away ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q)))
        x :
      Localization.Away (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S))
f : AdjoinRoot P.f →ₐ[R] S := AdjoinRoot.liftAlgHom P.f (ofId R S) x hqx
simp :
  IsLocalization.Away.{u_3, u_3} (R := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S)
    (Localization.Away (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S))
⊢ IsLocalization.Away.{u_3, u_3} (R := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S)
    (Localization.Away (M := S)
      ((f : (a : AdjoinRoot P.f) → S) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f) : S))

Tactic:
simp only [AdjoinRoot.liftAlgHom_mk, toRingHom_ofId, f, ← aeval_def, P]

Premises used: Algebra.toRingHom_ofId, Polynomial.aeval_def, AdjoinRoot.liftAlgHom_mk
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
this_1 : Nontrivial R
P_1 : Ideal R := Ideal.under R Q
this : Algebra.{u_1, u_3} (Localization.AtPrime P_1) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver P_1 Q
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))
hx' : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
q : R[X]
hq : q.Monic
hqx : Eq.{u_3 + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S)
hq'x : ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉ Q
P : StandardEtalePair R := { f := q, monic_f := hq, g := (derivative : (a : R[X]) → R[X]) q, cond := ⋯ }
hP :
  P.HasMap (S :=
    Localization.Away (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S))
    ((algebraMap S
            (Localization.Away (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S)) :
          (a : S) → Localization.Away ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q)))
        x :
      Localization.Away (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S))
f : AdjoinRoot P.f →ₐ[R] S := AdjoinRoot.liftAlgHom P.f (ofId R S) x hqx
⊢ IsLocalization.Away.{u_3, u_3} (R := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S)
    (Localization.Away (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S))

Tactic:
infer_instance