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
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : Module.Finite R S
inst_5 : IsUnramifiedAt R Q
inst_6 : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
this_1 : p.IsPrime
this : IsArtinianRing (p.Fiber S)
α : (↑(p.primesOver S) : Type u_3) ≃o PrimeSpectrum (p.Fiber S) := PrimeSpectrum.primesOverOrderIsoFiber R S p
x : Q.ResidueField
hx : Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField) p.ResidueField[x] ⊤
hx0 : ¬x = 0
⊢ ∃ (x : Q.ResidueField), x ≠ 0 ∧ Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField) p.ResidueField[x] ⊤

Tactic:
exact ⟨x, hx0, 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
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : Module.Finite R S
inst_5 : IsUnramifiedAt R Q
inst_6 : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
this_1 : p.IsPrime
this : IsArtinianRing (p.Fiber S)
α : (↑(p.primesOver S) : Type u_3) ≃o PrimeSpectrum (p.Fiber S) := PrimeSpectrum.primesOverOrderIsoFiber R S p
obtain :
  ∀ (x : Q.ResidueField) (hx0 : x ≠ 0)
    (hx : Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField) p.ResidueField[x] ⊤),
    ∃ t ∉ Q,
      (∀ (Q' : Ideal S),
          Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q') ∧
        Eq (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
          (Ideal.ResidueField
              (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
          ⊤
⊢ ∃ t ∉ Q,
    (∀ (Q' : Ideal S),
        Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q') ∧
      Eq (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
        (Ideal.ResidueField
            (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
        ⊤

Tactic:
obtain ⟨x, hx0, hx⟩ : ∃ x : Q.ResidueField, x ≠ 0 ∧ p.ResidueField[x] = ⊤ := by
    obtain ⟨x, hx⟩ := Field.exists_primitive_element p.ResidueField Q.ResidueField
    rw [IntermediateField.adjoin_eq_top_iff] at hx
    by_cases hx0 : x = 0
    · exact ⟨1, by simp, by simpa [p, hx0] using hx⟩
    · exact ⟨x, hx0, hx⟩

Premises used: Ideal.ResidueField
-- 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
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : Module.Finite R S
inst_5 : IsUnramifiedAt R Q
inst_6 : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
this_1 : p.IsPrime
this : IsArtinianRing (p.Fiber S)
α : (↑(p.primesOver S) : Type u_3) ≃o PrimeSpectrum (p.Fiber S) := PrimeSpectrum.primesOverOrderIsoFiber R S p
x : Q.ResidueField
hx0 : x ≠ 0
hx : Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField) p.ResidueField[x] ⊤
obtain :
  ∀ (x : p.ResidueField ⊗[R] S)
    (hx0 :
      Ne.{u_3 + 1} (α := Q.ResidueField)
        (((TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯ :
                p.ResidueField ⊗[R] S →ₐ[p.ResidueField] Q.ResidueField) :
              (a : p.ResidueField ⊗[R] S) → Q.ResidueField)
            x :
          Q.ResidueField)
        (0 : Q.ResidueField))
    (hx :
      Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField)
        p.ResidueField[(((TensorProduct.lift (ofId p.ResidueField Q.ResidueField)
                    (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯ :
                  p.ResidueField ⊗[R] S →ₐ[p.ResidueField] Q.ResidueField) :
                (a : p.ResidueField ⊗[R] S) → Q.ResidueField)
              x :
            Q.ResidueField)]
        ⊤),
    ∃ t ∉ Q,
      (∀ (Q' : Ideal S),
          Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q') ∧
        Eq (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
          (Ideal.ResidueField
              (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
          ⊤
⊢ ∃ t ∉ Q,
    (∀ (Q' : Ideal S),
        Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q') ∧
      Eq (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
        (Ideal.ResidueField
            (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
        ⊤

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Fiber.lift_residueField_surjective p _ x

Premises used: Ideal.Fiber.lift_residueField_surjective, rfl
-- 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
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : Module.Finite R S
inst_5 : IsUnramifiedAt R Q
inst_6 : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
this_1 : p.IsPrime
this : IsArtinianRing (p.Fiber S)
α : (↑(p.primesOver S) : Type u_3) ≃o PrimeSpectrum (p.Fiber S) := PrimeSpectrum.primesOverOrderIsoFiber R S p
x : p.ResidueField ⊗[R] S
hx0 :
  Ne.{u_3 + 1} (α := Q.ResidueField)
    (((TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯ :
            p.ResidueField ⊗[R] S →ₐ[p.ResidueField] Q.ResidueField) :
          (a : p.ResidueField ⊗[R] S) → Q.ResidueField)
        x :
      Q.ResidueField)
    (0 : Q.ResidueField)
hx :
  Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField)
    p.ResidueField[(((TensorProduct.lift (ofId p.ResidueField Q.ResidueField)
                (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯ :
              p.ResidueField ⊗[R] S →ₐ[p.ResidueField] Q.ResidueField) :
            (a : p.ResidueField ⊗[R] S) → Q.ResidueField)
          x :
        Q.ResidueField)]
    ⊤
⊢ let φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField :=
    TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯;
  Ne.{u_3 + 1} (α := Q.ResidueField) ((φ : (a : p.ResidueField ⊗[R] S) → Q.ResidueField) x : Q.ResidueField)
    (0 : Q.ResidueField)

Tactic:
set φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField := TensorProduct.lift
      (Algebra.ofId _ _) (IsScalarTower.toAlgHom _ _ _) fun _ _ ↦ .all _ _

Premises used: IsScalarTower.toAlgHom, Algebra.TensorProduct.lift, Ideal.ResidueField, Algebra.ofId, Ideal.Fiber
-- 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
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : Module.Finite R S
inst_5 : IsUnramifiedAt R Q
inst_6 : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
this_1 : p.IsPrime
this : IsArtinianRing (p.Fiber S)
α : (↑(p.primesOver S) : Type u_3) ≃o PrimeSpectrum (p.Fiber S) := PrimeSpectrum.primesOverOrderIsoFiber R S p
x : p.ResidueField ⊗[R] S
hx0 :
  Ne.{u_3 + 1} (α := Q.ResidueField)
    (((TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯ :
            p.ResidueField ⊗[R] S →ₐ[p.ResidueField] Q.ResidueField) :
          (a : p.ResidueField ⊗[R] S) → Q.ResidueField)
        x :
      Q.ResidueField)
    (0 : Q.ResidueField)
hx :
  Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField)
    p.ResidueField[(((TensorProduct.lift (ofId p.ResidueField Q.ResidueField)
                (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯ :
              p.ResidueField ⊗[R] S →ₐ[p.ResidueField] Q.ResidueField) :
            (a : p.ResidueField ⊗[R] S) → Q.ResidueField)
          x :
        Q.ResidueField)]
    ⊤
hx0₁ :
  let φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField :=
    TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯;
  Ne.{u_3 + 1} (α := Q.ResidueField) ((φ : (a : p.ResidueField ⊗[R] S) → Q.ResidueField) x : Q.ResidueField)
    (0 : Q.ResidueField)
⊢ let φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField :=
    TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯;
  Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField)
    p.ResidueField[((φ : (a : p.ResidueField ⊗[R] S) → Q.ResidueField) x : Q.ResidueField)] ⊤

Tactic:
set φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField := TensorProduct.lift
      (Algebra.ofId _ _) (IsScalarTower.toAlgHom _ _ _) fun _ _ ↦ .all _ _

Premises used: IsScalarTower.toAlgHom, Algebra.TensorProduct.lift, Ideal.ResidueField, Algebra.ofId, Ideal.Fiber
-- 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
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : Module.Finite R S
inst_5 : IsUnramifiedAt R Q
inst_6 : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
this_1 : p.IsPrime
this : IsArtinianRing (p.Fiber S)
α : (↑(p.primesOver S) : Type u_3) ≃o PrimeSpectrum (p.Fiber S) := PrimeSpectrum.primesOverOrderIsoFiber R S p
x : p.ResidueField ⊗[R] S
φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField :=
  TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯
hx0 :
  Ne.{u_3 + 1} (α := Q.ResidueField) ((φ : (a : p.ResidueField ⊗[R] S) → Q.ResidueField) x : Q.ResidueField)
    (0 : Q.ResidueField)
hx :
  Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField)
    p.ResidueField[((φ : (a : p.ResidueField ⊗[R] S) → Q.ResidueField) x : Q.ResidueField)] ⊤
obtain :
  ∀ (r : p.Fiber S)
    (hrQ :
      r ∉
        PrimeSpectrum.asIdeal
          ((α : (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 ⋯)))
    (hrid : IsIdempotentElem r)
    (hr :
      ∀ (q : Ideal (p.Fiber S)),
        q.IsPrime →
          q ≠
              PrimeSpectrum.asIdeal
                ((α : (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 ⋯)) →
            r ∈ q),
    ∃ t ∉ Q,
      (∀ (Q' : Ideal S),
          Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q') ∧
        Eq (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
          (Ideal.ResidueField
              (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
          ⊤
⊢ ∃ t ∉ Q,
    (∀ (Q' : Ideal S),
        Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q') ∧
      Eq (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
        (Ideal.ResidueField
            (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
        ⊤

Tactic:
obtain ⟨r, hrQ, hrid, hr⟩ :=
    IsArtinianRing.exists_not_mem_forall_mem_of_ne (α ⟨Q, ‹_›, ⟨rfl⟩⟩).asIdeal

Premises used: Ideal.LiesOver.mk, Subtype.mk, And.intro, IsArtinianRing.exists_not_mem_forall_mem_of_ne, DFunLike.coe, PrimeSpectrum.asIdeal, rfl
-- 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
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : Module.Finite R S
inst_5 : IsUnramifiedAt R Q
inst_6 : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
this_1 : p.IsPrime
this : IsArtinianRing (p.Fiber S)
α : (↑(p.primesOver S) : Type u_3) ≃o PrimeSpectrum (p.Fiber S) := PrimeSpectrum.primesOverOrderIsoFiber R S p
x : p.ResidueField ⊗[R] S
φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField :=
  TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯
hx0 :
  Ne.{u_3 + 1} (α := Q.ResidueField) ((φ : (a : p.ResidueField ⊗[R] S) → Q.ResidueField) x : Q.ResidueField)
    (0 : Q.ResidueField)
hx :
  Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField)
    p.ResidueField[((φ : (a : p.ResidueField ⊗[R] S) → Q.ResidueField) x : Q.ResidueField)] ⊤
r : p.Fiber S
hrQ :
  r ∉
    PrimeSpectrum.asIdeal
      ((α : (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 ⋯))
hrid : IsIdempotentElem r
hr :
  ∀ (q : Ideal (p.Fiber S)),
    q.IsPrime →
      q ≠
          PrimeSpectrum.asIdeal
            ((α : (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 ⋯)) →
        r ∈ q
obtain :
  ∀ (s : R) (hsQ : s ∉ p) (t : S) (e : s • (r * x) = 1 ⊗ₜ[R] t),
    ∃ t ∉ Q,
      (∀ (Q' : Ideal S),
          Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q') ∧
        Eq (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
          (Ideal.ResidueField
              (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
          ⊤
⊢ ∃ t ∉ Q,
    (∀ (Q' : Ideal S),
        Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q') ∧
      Eq (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
        (Ideal.ResidueField
            (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
        ⊤

Tactic:
obtain ⟨s, hsQ, t, e⟩ := Ideal.Fiber.exists_smul_eq_one_tmul _ (r * x)

Premises used: HMul.hMul, Ideal.Fiber.exists_smul_eq_one_tmul
-- 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
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : Module.Finite R S
inst_5 : IsUnramifiedAt R Q
inst_6 : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
this_1 : p.IsPrime
this : IsArtinianRing (p.Fiber S)
α : (↑(p.primesOver S) : Type u_3) ≃o PrimeSpectrum (p.Fiber S) := PrimeSpectrum.primesOverOrderIsoFiber R S p
x : p.ResidueField ⊗[R] S
φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField :=
  TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯
hx0 :
  Ne.{u_3 + 1} (α := Q.ResidueField) ((φ : (a : p.ResidueField ⊗[R] S) → Q.ResidueField) x : Q.ResidueField)
    (0 : Q.ResidueField)
hx :
  Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField)
    p.ResidueField[((φ : (a : p.ResidueField ⊗[R] S) → Q.ResidueField) x : Q.ResidueField)] ⊤
r : p.Fiber S
hrQ :
  r ∉
    PrimeSpectrum.asIdeal
      ((α : (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 ⋯))
hrid : IsIdempotentElem r
hr :
  ∀ (q : Ideal (p.Fiber S)),
    q.IsPrime →
      q ≠
          PrimeSpectrum.asIdeal
            ((α : (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 ⋯)) →
        r ∈ q
s : R
hsQ : s ∉ p
t : S
e : s • (r * x) = 1 ⊗ₜ[R] t
⊢ Eq (α := AlgHom.{u_1, u_1, u_3} R p.ResidueField Q.ResidueField) (Ideal.ResidueField.mapₐ p Q (ofId R S) ⋯)
    (AlgHom.restrictScalars R (ofId p.ResidueField Q.ResidueField))

Tactic:
ext
-- 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
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : Module.Finite R S
inst_5 : IsUnramifiedAt R Q
inst_6 : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
this_1 : p.IsPrime
this : IsArtinianRing (p.Fiber S)
α : (↑(p.primesOver S) : Type u_3) ≃o PrimeSpectrum (p.Fiber S) := PrimeSpectrum.primesOverOrderIsoFiber R S p
x : p.ResidueField ⊗[R] S
φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField :=
  TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯
hx0 :
  Ne.{u_3 + 1} (α := Q.ResidueField) ((φ : (a : p.ResidueField ⊗[R] S) → Q.ResidueField) x : Q.ResidueField)
    (0 : Q.ResidueField)
hx :
  Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField)
    p.ResidueField[((φ : (a : p.ResidueField ⊗[R] S) → Q.ResidueField) x : Q.ResidueField)] ⊤
r : p.Fiber S
hrQ :
  r ∉
    PrimeSpectrum.asIdeal
      ((α : (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 ⋯))
hrid : IsIdempotentElem r
hr :
  ∀ (q : Ideal (p.Fiber S)),
    q.IsPrime →
      q ≠
          PrimeSpectrum.asIdeal
            ((α : (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 ⋯)) →
        r ∈ q
s : R
hsQ : s ∉ p
t : S
e : s • (r * x) = 1 ⊗ₜ[R] t
⊢ Eq (α := AlgHom.{u_1, u_1, u_3} R p.ResidueField Q.ResidueField) (Ideal.ResidueField.mapₐ p Q (ofId R S) ⋯)
    (AlgHom.restrictScalars R (ofId p.ResidueField Q.ResidueField))

Tactic:
have : Ideal.ResidueField.mapₐ p Q (ofId R S) (Ideal.over_def Q p) =
      AlgHom.restrictScalars R (ofId p.ResidueField Q.ResidueField) := by ext
-- 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
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : Module.Finite R S
inst_5 : IsUnramifiedAt R Q
inst_6 : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
this_1 : p.IsPrime
this_2 : IsArtinianRing (p.Fiber S)
α : (↑(p.primesOver S) : Type u_3) ≃o PrimeSpectrum (p.Fiber S) := PrimeSpectrum.primesOverOrderIsoFiber R S p
x : p.ResidueField ⊗[R] S
φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField :=
  TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯
hx0 :
  Ne.{u_3 + 1} (α := Q.ResidueField) ((φ : (a : p.ResidueField ⊗[R] S) → Q.ResidueField) x : Q.ResidueField)
    (0 : Q.ResidueField)
hx :
  Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField)
    p.ResidueField[((φ : (a : p.ResidueField ⊗[R] S) → Q.ResidueField) x : Q.ResidueField)] ⊤
r : p.Fiber S
hrQ :
  r ∉
    PrimeSpectrum.asIdeal
      ((α : (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 ⋯))
hrid : IsIdempotentElem r
hr :
  ∀ (q : Ideal (p.Fiber S)),
    q.IsPrime →
      q ≠
          PrimeSpectrum.asIdeal
            ((α : (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 ⋯)) →
        r ∈ q
s : R
hsQ : s ∉ p
t : S
e : s • (r * x) = 1 ⊗ₜ[R] t
this :
  Eq (α := AlgHom.{u_1, u_1, u_3} R p.ResidueField Q.ResidueField) (Ideal.ResidueField.mapₐ p Q (ofId R S) ⋯)
    (AlgHom.restrictScalars R (ofId p.ResidueField Q.ResidueField))
rw :
  Ne.{u_3 + 1} (α := Q.ResidueField)
    (((TensorProduct.lift (AlgHom.restrictScalars R (ofId p.ResidueField Q.ResidueField))
              (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯ :
            p.ResidueField ⊗[R] S →ₐ[R] Q.ResidueField) :
          (a : p.Fiber S) → Q.ResidueField)
        r :
      Q.ResidueField)
    (0 : Q.ResidueField)
⊢ Ne.{u_3 + 1} (α := Q.ResidueField) ((φ : (a : p.Fiber S) → Q.ResidueField) r : Q.ResidueField) (0 : Q.ResidueField)

Tactic:
rw [← AlgHom.restrictScalars_apply R, Algebra.TensorProduct.restrictScalars_lift]

Premises used: AlgHom.restrictScalars_apply, Algebra.TensorProduct.restrictScalars_lift
-- 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
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : Module.Finite R S
inst_5 : IsUnramifiedAt R Q
inst_6 : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
this_1 : p.IsPrime
this_2 : IsArtinianRing (p.Fiber S)
α : (↑(p.primesOver S) : Type u_3) ≃o PrimeSpectrum (p.Fiber S) := PrimeSpectrum.primesOverOrderIsoFiber R S p
x : p.ResidueField ⊗[R] S
φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField :=
  TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯
hx0 :
  Ne.{u_3 + 1} (α := Q.ResidueField) ((φ : (a : p.ResidueField ⊗[R] S) → Q.ResidueField) x : Q.ResidueField)
    (0 : Q.ResidueField)
hx :
  Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField)
    p.ResidueField[((φ : (a : p.ResidueField ⊗[R] S) → Q.ResidueField) x : Q.ResidueField)] ⊤
r : p.Fiber S
hrQ :
  r ∉
    PrimeSpectrum.asIdeal
      ((α : (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 ⋯))
hrid : IsIdempotentElem r
hr :
  ∀ (q : Ideal (p.Fiber S)),
    q.IsPrime →
      q ≠
          PrimeSpectrum.asIdeal
            ((α : (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 ⋯)) →
        r ∈ q
s : R
hsQ : s ∉ p
t : S
e : s • (r * x) = 1 ⊗ₜ[R] t
this :
  Eq (α := AlgHom.{u_1, u_1, u_3} R p.ResidueField Q.ResidueField) (Ideal.ResidueField.mapₐ p Q (ofId R S) ⋯)
    (AlgHom.restrictScalars R (ofId p.ResidueField Q.ResidueField))
⊢ r ∉
    PrimeSpectrum.asIdeal
      ((α : (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 ⋯))

Tactic:
hrQ