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_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
hsQ' :
  Ne.{u_3 + 1} (α := Q.ResidueField) ((algebraMap R Q.ResidueField : (a : R) → Q.ResidueField) s : Q.ResidueField)
    (0 : Q.ResidueField)
hrQ' :
  Eq.{u_3 + 1} (α := Q.ResidueField) ((φ : (a : p.Fiber S) → Q.ResidueField) r : Q.ResidueField) (1 : Q.ResidueField)
e' :
  HMul.hMul (α := Q.ResidueField) (β := Q.ResidueField)
      ((algebraMap R Q.ResidueField : (a : R) → Q.ResidueField) s : Q.ResidueField)
      ((φ : (a : p.Fiber S) → Q.ResidueField) x : Q.ResidueField) =
    (algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t
Q' : Ideal S
left : Q'.IsPrime
right : Q'.LiesOver (Ideal.under R Q)
H_1 : Q' ≠ Q
this : Algebra.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime Q') :=
  Localization.AtPrime.algebraOfLiesOver p Q'
hsQ'' :
  Ne.{u_3 + 1} (α := Q'.ResidueField) ((algebraMap R Q'.ResidueField : (a : R) → Q'.ResidueField) s : Q'.ResidueField)
    (0 : Q'.ResidueField)
φ' : p.Fiber S →ₐ[p.ResidueField] Q'.ResidueField :=
  TensorProduct.lift (ofId p.ResidueField Q'.ResidueField) (IsScalarTower.toAlgHom R S Q'.ResidueField) ⋯
H :
  Eq.{u_3 + 1} (α := Q'.ResidueField) ((φ' : (a : p.Fiber S) → Q'.ResidueField) r : Q'.ResidueField)
    (0 : Q'.ResidueField)
refine_2 :
  Eq (α := Q'.ResidueField) ((algebraMap S Q'.ResidueField : (a : S) → Q'.ResidueField) t : Q'.ResidueField)
    (0 : Q'.ResidueField)
⊢ t ∈ Q'

Tactic:
rw [← Ideal.algebraMap_residueField_eq_zero]

Premises used: Ideal.algebraMap_residueField_eq_zero
-- 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
hsQ' :
  Ne.{u_3 + 1} (α := Q.ResidueField) ((algebraMap R Q.ResidueField : (a : R) → Q.ResidueField) s : Q.ResidueField)
    (0 : Q.ResidueField)
hrQ' :
  Eq.{u_3 + 1} (α := Q.ResidueField) ((φ : (a : p.Fiber S) → Q.ResidueField) r : Q.ResidueField) (1 : Q.ResidueField)
e' :
  HMul.hMul (α := Q.ResidueField) (β := Q.ResidueField)
      ((algebraMap R Q.ResidueField : (a : R) → Q.ResidueField) s : Q.ResidueField)
      ((φ : (a : p.Fiber S) → Q.ResidueField) x : Q.ResidueField) =
    (algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t
Q' : Ideal S
left : Q'.IsPrime
right : Q'.LiesOver (Ideal.under R Q)
H_1 : Q' ≠ Q
this : Algebra.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime Q') :=
  Localization.AtPrime.algebraOfLiesOver p Q'
hsQ'' :
  Ne.{u_3 + 1} (α := Q'.ResidueField) ((algebraMap R Q'.ResidueField : (a : R) → Q'.ResidueField) s : Q'.ResidueField)
    (0 : Q'.ResidueField)
φ' : p.Fiber S →ₐ[p.ResidueField] Q'.ResidueField :=
  TensorProduct.lift (ofId p.ResidueField Q'.ResidueField) (IsScalarTower.toAlgHom R S Q'.ResidueField) ⋯
H :
  Eq.{u_3 + 1} (α := Q'.ResidueField) ((φ' : (a : p.Fiber S) → Q'.ResidueField) r : Q'.ResidueField)
    (0 : Q'.ResidueField)
⊢ Eq (α := Q'.ResidueField) ((algebraMap S Q'.ResidueField : (a : S) → Q'.ResidueField) t : Q'.ResidueField)
    ((φ' : (a : p.Fiber S) → Q'.ResidueField) (1 ⊗ₜ[R] t) : Q'.ResidueField)

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
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
hsQ' :
  Ne.{u_3 + 1} (α := Q.ResidueField) ((algebraMap R Q.ResidueField : (a : R) → Q.ResidueField) s : Q.ResidueField)
    (0 : Q.ResidueField)
hrQ' :
  Eq.{u_3 + 1} (α := Q.ResidueField) ((φ : (a : p.Fiber S) → Q.ResidueField) r : Q.ResidueField) (1 : Q.ResidueField)
e' :
  HMul.hMul (α := Q.ResidueField) (β := Q.ResidueField)
      ((algebraMap R Q.ResidueField : (a : R) → Q.ResidueField) s : Q.ResidueField)
      ((φ : (a : p.Fiber S) → Q.ResidueField) x : Q.ResidueField) =
    (algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t
Q' : Ideal S
left : Q'.IsPrime
right : Q'.LiesOver (Ideal.under R Q)
H_1 : Q' ≠ Q
this : Algebra.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime Q') :=
  Localization.AtPrime.algebraOfLiesOver p Q'
hsQ'' :
  Ne.{u_3 + 1} (α := Q'.ResidueField) ((algebraMap R Q'.ResidueField : (a : R) → Q'.ResidueField) s : Q'.ResidueField)
    (0 : Q'.ResidueField)
φ' : p.Fiber S →ₐ[p.ResidueField] Q'.ResidueField :=
  TensorProduct.lift (ofId p.ResidueField Q'.ResidueField) (IsScalarTower.toAlgHom R S Q'.ResidueField) ⋯
H :
  Eq.{u_3 + 1} (α := Q'.ResidueField) ((φ' : (a : p.Fiber S) → Q'.ResidueField) r : Q'.ResidueField)
    (0 : Q'.ResidueField)
⊢ Eq.{u_3 + 1} (α := Q'.ResidueField) ((φ' : (a : p.Fiber S) → Q'.ResidueField) (1 ⊗ₜ[R] t) : Q'.ResidueField)
    (0 : Q'.ResidueField)

Tactic:
simpa [smul_def, H] using congr(φ' $e).symm

Premises used: congrArg, id, Algebra.smul_def, Eq.symm, DFunLike.coe
-- 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
hsQ' :
  Ne.{u_3 + 1} (α := Q.ResidueField) ((algebraMap R Q.ResidueField : (a : R) → Q.ResidueField) s : Q.ResidueField)
    (0 : Q.ResidueField)
hrQ' :
  Eq.{u_3 + 1} (α := Q.ResidueField) ((φ : (a : p.Fiber S) → Q.ResidueField) r : Q.ResidueField) (1 : Q.ResidueField)
e' :
  HMul.hMul (α := Q.ResidueField) (β := Q.ResidueField)
      ((algebraMap R Q.ResidueField : (a : R) → Q.ResidueField) s : Q.ResidueField)
      ((φ : (a : p.Fiber S) → Q.ResidueField) x : Q.ResidueField) =
    (algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t
⊢ (φ : (a : p.Fiber S) → Q.ResidueField) x =
    HSMul.hSMul (α := p.ResidueField) (β := Q.ResidueField)
      (((algebraMap R p.ResidueField : (a : R) → p.ResidueField) s)⁻¹ : p.ResidueField)
      ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)

Tactic:
simpa [smul_def, ← IsScalarTower.algebraMap_apply, eq_inv_mul_iff_mul_eq₀ hsQ']

Premises used: eq_inv_mul_iff_mul_eq₀, Algebra.smul_def, 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
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
hsQ' :
  Ne.{u_3 + 1} (α := Q.ResidueField) ((algebraMap R Q.ResidueField : (a : R) → Q.ResidueField) s : Q.ResidueField)
    (0 : Q.ResidueField)
hrQ' :
  Eq.{u_3 + 1} (α := Q.ResidueField) ((φ : (a : p.Fiber S) → Q.ResidueField) r : Q.ResidueField) (1 : Q.ResidueField)
e' :
  HMul.hMul (α := Q.ResidueField) (β := Q.ResidueField)
      ((algebraMap R Q.ResidueField : (a : R) → Q.ResidueField) s : Q.ResidueField)
      ((φ : (a : p.Fiber S) → Q.ResidueField) x : Q.ResidueField) =
    (algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t
⊢ (φ : (a : p.Fiber S) → Q.ResidueField) x =
    HSMul.hSMul (α := p.ResidueField) (β := Q.ResidueField)
      (((algebraMap R p.ResidueField : (a : R) → p.ResidueField) s)⁻¹ : p.ResidueField)
      ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)

Tactic:
have : φ x = (algebraMap _ p.ResidueField s)⁻¹ • algebraMap _ _ t := by
      simpa [smul_def, ← IsScalarTower.algebraMap_apply, eq_inv_mul_iff_mul_eq₀ hsQ']
-- 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
hsQ' :
  Ne.{u_3 + 1} (α := Q.ResidueField) ((algebraMap R Q.ResidueField : (a : R) → Q.ResidueField) s : Q.ResidueField)
    (0 : Q.ResidueField)
hrQ' :
  Eq.{u_3 + 1} (α := Q.ResidueField) ((φ : (a : p.Fiber S) → Q.ResidueField) r : Q.ResidueField) (1 : Q.ResidueField)
e' :
  HMul.hMul (α := Q.ResidueField) (β := Q.ResidueField)
      ((algebraMap R Q.ResidueField : (a : R) → Q.ResidueField) s : Q.ResidueField)
      ((φ : (a : p.Fiber S) → Q.ResidueField) x : Q.ResidueField) =
    (algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t
this :
  (φ : (a : p.Fiber S) → Q.ResidueField) x =
    HSMul.hSMul (α := p.ResidueField) (β := Q.ResidueField)
      (((algebraMap R p.ResidueField : (a : R) → p.ResidueField) s)⁻¹ : p.ResidueField)
      ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)
⊢ LE.le (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
    p.ResidueField[HSMul.hSMul (α := p.ResidueField) (β := Q.ResidueField)
        (((algebraMap R p.ResidueField : (a : R) → p.ResidueField) s)⁻¹ : p.ResidueField)
        ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
    (Ideal.ResidueField
        (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]

Tactic:
adjoin_singleton_le ?_

Premises used: Set.Mem, Algebra.adjoin_singleton_le
-- 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
hsQ' :
  Ne.{u_3 + 1} (α := Q.ResidueField) ((algebraMap R Q.ResidueField : (a : R) → Q.ResidueField) s : Q.ResidueField)
    (0 : Q.ResidueField)
hrQ' :
  Eq.{u_3 + 1} (α := Q.ResidueField) ((φ : (a : p.Fiber S) → Q.ResidueField) r : Q.ResidueField) (1 : Q.ResidueField)
e' :
  HMul.hMul (α := Q.ResidueField) (β := Q.ResidueField)
      ((algebraMap R Q.ResidueField : (a : R) → Q.ResidueField) s : Q.ResidueField)
      ((φ : (a : p.Fiber S) → Q.ResidueField) x : Q.ResidueField) =
    (algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t
this :
  (φ : (a : p.Fiber S) → Q.ResidueField) x =
    HSMul.hSMul (α := p.ResidueField) (β := Q.ResidueField)
      (((algebraMap R p.ResidueField : (a : R) → p.ResidueField) s)⁻¹ : p.ResidueField)
      ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)
⊢ Membership.mem (γ := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField)
    (Ideal.ResidueField
        (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
    (HSMul.hSMul (α := p.ResidueField) (β := Q.ResidueField)
      (((algebraMap R p.ResidueField : (a : R) → p.ResidueField) s)⁻¹ : p.ResidueField)
      ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField))

Tactic:
Subalgebra.smul_mem _ (self_mem_adjoin_singleton _ _) _

Premises used: Set.Mem, Subalgebra.smul_mem, Algebra.self_mem_adjoin_singleton
-- 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
hsQ' :
  Ne.{u_3 + 1} (α := Q.ResidueField) ((algebraMap R Q.ResidueField : (a : R) → Q.ResidueField) s : Q.ResidueField)
    (0 : Q.ResidueField)
hrQ' :
  Eq.{u_3 + 1} (α := Q.ResidueField) ((φ : (a : p.Fiber S) → Q.ResidueField) r : Q.ResidueField) (1 : Q.ResidueField)
e' :
  HMul.hMul (α := Q.ResidueField) (β := Q.ResidueField)
      ((algebraMap R Q.ResidueField : (a : R) → Q.ResidueField) s : Q.ResidueField)
      ((φ : (a : p.Fiber S) → Q.ResidueField) x : Q.ResidueField) =
    (algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t
this :
  (φ : (a : p.Fiber S) → Q.ResidueField) x =
    HSMul.hSMul (α := p.ResidueField) (β := Q.ResidueField)
      (((algebraMap R p.ResidueField : (a : R) → p.ResidueField) s)⁻¹ : p.ResidueField)
      ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)
⊢ Membership.mem (γ := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField)
    (Ideal.ResidueField
        (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
    (HSMul.hSMul (α := p.ResidueField) (β := Q.ResidueField)
      (((algebraMap R p.ResidueField : (a : R) → p.ResidueField) s)⁻¹ : p.ResidueField)
      ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField))

Tactic:
exact Subalgebra.smul_mem _ (self_mem_adjoin_singleton _ _) _

Premises used: Subalgebra.smul_mem, Algebra.self_mem_adjoin_singleton