awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_4
S : Type u_5
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : Field S
f : R →+* S
inst_3 : IsLocalHom (R := R) (S := S) f
x : R
⊢ Eq.{u_5 + 1} (α := S)
    ((lift f : (a : ResidueField R) → S) ((residue R : (a : R) → ResidueField R) x : ResidueField R) : S)
    ((f : (a : R) → S) x : S)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : CommRing S
inst_3 : IsLocalRing S
inst_4 : CommRing T
inst_5 : IsLocalRing T
f : R →+* S
inst_6 : IsLocalHom (R := R) (S := S) f
a : R
ha : Membership.mem (γ := Ideal R) (maximalIdeal R : Ideal R) a
rw : Membership.mem (α := S) (γ := Ideal S) (maximalIdeal S : Ideal S) ((f : (a : R) → S) a : S)
⊢ Eq.{u_2 + 1} (α := HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S))
    (((RingHom.comp (Ideal.Quotient.mk (maximalIdeal S)) f :
            RingHom.{u_1, u_2} R (HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S))) :
          (a : R) → S ⧸ maximalIdeal S)
        a :
      HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S))
    (0 : HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S))

Tactic:
rw [RingHom.comp_apply, Ideal.Quotient.eq_zero_iff_mem]

Premises used: Ideal.Quotient.eq_zero_iff_mem, RingHom.comp_apply
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : CommRing S
inst_3 : IsLocalRing S
inst_4 : CommRing T
inst_5 : IsLocalRing T
f : R →+* S
inst_6 : IsLocalHom (R := R) (S := S) f
a : R
ha : Membership.mem (γ := Ideal R) (maximalIdeal R : Ideal R) a
⊢ Membership.mem (α := S) (γ := Ideal S) (maximalIdeal S : Ideal S) ((f : (a : R) → S) a : S)

Tactic:
map_nonunit f a ha

Premises used: Set.Mem, map_nonunit
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : CommRing S
inst_3 : IsLocalRing S
inst_4 : CommRing T
inst_5 : IsLocalRing T
f : R →+* S
inst_6 : IsLocalHom (R := R) (S := S) f
a : R
ha : Membership.mem (γ := Ideal R) (maximalIdeal R : Ideal R) a
⊢ Membership.mem (α := S) (γ := Ideal S) (maximalIdeal S : Ideal S) ((f : (a : R) → S) a : S)

Tactic:
exact map_nonunit f a ha

Premises used: map_nonunit
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
⊢ Eq (α := ResidueField R →+* ResidueField R) (map (RingHom.id R)) (RingHom.id (ResidueField R))

Tactic:
Ideal.Quotient.ringHom_ext <| RingHom.ext fun _ => rfl

Premises used: Ideal.Quotient.ringHom_ext, RingHom.ext, IsLocalRing.ResidueField, rfl
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : CommRing S
inst_3 : IsLocalRing S
inst_4 : CommRing T
inst_5 : IsLocalRing T
f : T →+* R
g : R →+* S
inst_6 : IsLocalHom (R := T) (S := R) f
inst_7 : IsLocalHom (R := R) (S := S) g
⊢ Eq (α := RingHom.{u_3, u_2} (ResidueField T) (ResidueField S)) (map (g.comp f))
    (RingHom.comp (β := ResidueField R) (map g) (map f))

Tactic:
Ideal.Quotient.ringHom_ext <| RingHom.ext fun _ => rfl

Premises used: Ideal.Quotient.ringHom_ext, RingHom.ext, IsLocalRing.ResidueField, rfl
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : CommRing S
inst_3 : IsLocalRing S
f : R →+* S
inst_4 : IsLocalHom (R := R) (S := S) f
⊢ Eq (α := RingHom.{u_1, u_2} R (ResidueField S)) (RingHom.comp (β := ResidueField R) (map f) (residue R))
    (RingHom.comp (residue S) f)

Tactic:
rfl

Premises used: IsLocalRing.ResidueField.map, Quotient.liftOn', Ideal.Quotient.mk, AddCon.liftOn, Submodule.Quotient.mk, IsLocalRing.residue, Quotient, rfl
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : CommRing S
inst_3 : IsLocalRing S
f : R →+* S
inst_4 : IsLocalHom (R := R) (S := S) f
r : R
⊢ Eq.{u_2 + 1} (α := ResidueField S)
    (((map f : RingHom.{u_1, u_2} (ResidueField R) (ResidueField S)) : (a : ResidueField R) → ResidueField S)
        ((residue R : (a : R) → ResidueField R) r) :
      ResidueField S)
    ((residue S : (a : S) → ResidueField S) ((f : (a : R) → S) r) : ResidueField S)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
x : ResidueField R
⊢ (map (RingHom.id R) : (a : ResidueField R) → ResidueField R) x = x

Tactic:
DFunLike.congr_fun map_id x

Premises used: DFunLike.congr_fun, IsLocalRing.ResidueField.map_id
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : CommRing S
inst_3 : IsLocalRing S
inst_4 : CommRing T
inst_5 : IsLocalRing T
f : R →+* S
g : S →+* T
x : ResidueField R
inst_6 : IsLocalHom (R := R) (S := S) f
inst_7 : IsLocalHom (R := S) (S := T) g
⊢ Eq.{u_3 + 1} (α := ResidueField T)
    (((map g : RingHom.{u_2, u_3} (ResidueField S) (ResidueField T)) : (a : ResidueField S) → ResidueField T)
        (((map f : RingHom.{u_1, u_2} (ResidueField R) (ResidueField S)) : (a : ResidueField R) → ResidueField S) x) :
      ResidueField T)
    (((map (g.comp f) : RingHom.{u_1, u_3} (ResidueField R) (ResidueField T)) : (a : ResidueField R) → ResidueField T)
        x :
      ResidueField T)

Tactic:
DFunLike.congr_fun (map_comp f g).symm x

Premises used: DFunLike.congr_fun, IsLocalRing.ResidueField.map_comp, Quotient.liftOn', AddCon.liftOn, Eq.symm
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : CommRing S
inst_3 : IsLocalRing S
inst_4 : CommRing T
inst_5 : IsLocalRing T
f : R ≃+* S
x : ResidueField R
⊢ ((map (↑f.symm : S →+* R) : RingHom.{u_2, u_1} (ResidueField S) (ResidueField R)) :
        (a : ResidueField S) → ResidueField R)
      (((map (↑f : R →+* S) : RingHom.{u_1, u_2} (ResidueField R) (ResidueField S)) :
          (a : ResidueField R) → ResidueField S)
        x) =
    x

Tactic:
simp only [map_map, RingEquiv.symm_comp, map_id, RingHom.id_apply]

Premises used: RingHom.id_apply, IsLocalRing.ResidueField.map_map, IsLocalRing.ResidueField.map_id, RingEquiv.symm_comp
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : CommRing S
inst_3 : IsLocalRing S
inst_4 : CommRing T
inst_5 : IsLocalRing T
f : R ≃+* S
x : ResidueField S
⊢ ((map (↑f : R →+* S) : RingHom.{u_1, u_2} (ResidueField R) (ResidueField S)) : (a : ResidueField R) → ResidueField S)
      (((map (↑f.symm : S →+* R) : RingHom.{u_2, u_1} (ResidueField S) (ResidueField R)) :
          (a : ResidueField S) → ResidueField R)
        x) =
    x

Tactic:
simp only [map_map, RingEquiv.comp_symm, map_id, RingHom.id_apply]

Premises used: RingHom.id_apply, IsLocalRing.ResidueField.map_map, IsLocalRing.ResidueField.map_id, RingEquiv.comp_symm
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : CommRing S
inst_3 : IsLocalRing S
f : R ≃+* S
⊢ Eq (α := RingEquiv.{u_2, u_1} (ResidueField S) (ResidueField R)) (RingEquiv.symm (mapEquiv f)) (mapEquiv f.symm)

Tactic:
rfl

Premises used: IsLocalRing.ResidueField.mapEquiv, Equiv.symm, RingEquiv.symm, rfl
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : CommRing S
inst_3 : IsLocalRing S
inst_4 : CommRing T
inst_5 : IsLocalRing T
e₁ : R ≃+* S
e₂ : S ≃+* T
⊢ Eq (α := RingEquiv.{u_1, u_3} (ResidueField R) (ResidueField T)) (mapEquiv (e₁.trans e₂))
    (RingEquiv.trans (S := ResidueField S) (mapEquiv e₁) (mapEquiv e₂))

Tactic:
RingEquiv.toRingHom_injective <| map_comp (e₁ : R →+* S) (e₂ : S →+* T)

Premises used: IsLocalRing.ResidueField.map_comp, RingHomClass.toRingHom, RingEquiv.toRingHom_injective
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
⊢ Eq (α := ResidueField R ≃+* ResidueField R) (mapEquiv (RingEquiv.refl R)) (RingEquiv.refl (ResidueField R))

Tactic:
RingEquiv.toRingHom_injective map_id

Premises used: IsLocalRing.ResidueField.map_id, RingEquiv.toRingHom_injective
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
G : Type u_4
inst_2 : Group G
inst_3 : MulSemiringAction G R
g : G
r : R
⊢ (residue R : (a : R) → ResidueField R) (g • r) =
    HSMul.hSMul (β := ResidueField R) g ((residue R : (a : R) → ResidueField R) r : ResidueField R)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, SMul.comp.smul, rfl
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : CommRing S
inst_3 : IsLocalRing S
inst_4 : CommRing T
inst_5 : IsLocalRing T
inst_6 : Algebra R S
inst_7 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
⊢ Ideal.LiesOver (maximalIdeal S) (maximalIdeal R)

Tactic:
⟨(((local_hom_TFAE (algebraMap R S)).out 0 4 rfl rfl).mp inferInstance).symm⟩

Premises used: Algebra.algebraMap, inferInstance, Ideal.LiesOver.mk, List.TFAE.out, Iff.mp, OfNat.ofNat, Eq.symm, IsLocalRing.local_hom_TFAE, rfl
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : CommRing S
inst_3 : IsLocalRing S
inst_4 : Algebra R S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
x : R
⊢ Eq.{u_2 + 1} (α := ResidueField S)
    ((algebraMap (ResidueField R) (ResidueField S) : (a : ResidueField R) → ResidueField S)
        ((residue R : (a : R) → ResidueField R) x) :
      ResidueField S)
    ((residue S : (a : S) → ResidueField S) ((algebraMap R S : (a : R) → S) x) : ResidueField S)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : CommRing S
inst_3 : IsLocalRing S
inst_4 : CommRing T
inst_5 : IsLocalRing T
inst_6 : Algebra R S
inst_7 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
R₀ : Type u_4
inst_8 : CommRing R₀
inst_9 : Algebra R₀ R
inst_10 : Algebra R₀ S
inst_11 : IsScalarTower R₀ R S
⊢ IsScalarTower.{u_4, u_1, u_2} R₀ (ResidueField R) (ResidueField S)

Tactic:
Ideal.Quotient.isScalarTower_of_liesOver ..

Premises used: Ideal.Quotient.isScalarTower_of_liesOver, IsLocalRing.ResidueField
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : CommRing S
inst_3 : IsLocalRing S
inst_4 : CommRing T
inst_5 : IsLocalRing T
inst_6 : Algebra R S
inst_7 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
R₀ : Type u_4
inst_8 : CommRing R₀
inst_9 : Algebra R₀ R
inst_10 : Algebra R₀ S
inst_11 : IsScalarTower R₀ R S
inst_12 : IsLocalRing R₀
inst_13 : IsLocalHom (R := R₀) (S := R) (F := R₀ →+* R) (algebraMap R₀ R)
inst_14 : IsLocalHom (R := R₀) (S := S) (F := R₀ →+* S) (algebraMap R₀ S)
⊢ IsScalarTower.{u_4, u_1, u_2} (ResidueField R₀) (ResidueField R) (ResidueField S)

Tactic:
.of_algebraMap_eq fun x ↦ ?_

Premises used: IsScalarTower.of_algebraMap_eq
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : CommRing S
inst_3 : IsLocalRing S
inst_4 : CommRing T
inst_5 : IsLocalRing T
inst_6 : Algebra R S
inst_7 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
R₀ : Type u_4
inst_8 : CommRing R₀
inst_9 : Algebra R₀ R
inst_10 : Algebra R₀ S
inst_11 : IsScalarTower R₀ R S
inst_12 : IsLocalRing R₀
inst_13 : IsLocalHom (R := R₀) (S := R) (F := R₀ →+* R) (algebraMap R₀ R)
inst_14 : IsLocalHom (R := R₀) (S := S) (F := R₀ →+* S) (algebraMap R₀ S)
refine :
  ∀ (x : ResidueField R₀),
    Eq.{u_2 + 1} (α := ResidueField S)
      ((algebraMap (ResidueField R₀) (ResidueField S) : (a : ResidueField R₀) → ResidueField S) x : ResidueField S)
      ((algebraMap (ResidueField R) (ResidueField S) : (a : ResidueField R) → ResidueField S)
          ((algebraMap (ResidueField R₀) (ResidueField R) : (a : ResidueField R₀) → ResidueField R) x) :
        ResidueField S)
⊢ IsScalarTower.{u_4, u_1, u_2} (ResidueField R₀) (ResidueField R) (ResidueField S)

Tactic:
refine .of_algebraMap_eq fun x ↦ ?_
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : CommRing S
inst_3 : IsLocalRing S
inst_4 : CommRing T
inst_5 : IsLocalRing T
inst_6 : Algebra R S
inst_7 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
R₀ : Type u_4
inst_8 : CommRing R₀
inst_9 : Algebra R₀ R
inst_10 : Algebra R₀ S
inst_11 : IsScalarTower R₀ R S
inst_12 : IsLocalRing R₀
inst_13 : IsLocalHom (R := R₀) (S := R) (F := R₀ →+* R) (algebraMap R₀ R)
inst_14 : IsLocalHom (R := R₀) (S := S) (F := R₀ →+* S) (algebraMap R₀ S)
x : ResidueField R₀
obtain :
  ∀ (x : R₀),
    Eq.{u_2 + 1} (α := ResidueField S)
      ((algebraMap (ResidueField R₀) (ResidueField S) : (a : ResidueField R₀) → ResidueField S)
          ((residue R₀ : (a : R₀) → ResidueField R₀) x) :
        ResidueField S)
      ((algebraMap (ResidueField R) (ResidueField S) : (a : ResidueField R) → ResidueField S)
          ((algebraMap (ResidueField R₀) (ResidueField R) : (a : ResidueField R₀) → ResidueField R)
            ((residue R₀ : (a : R₀) → ResidueField R₀) x)) :
        ResidueField S)
⊢ Eq.{u_2 + 1} (α := ResidueField S)
    ((algebraMap (ResidueField R₀) (ResidueField S) : (a : ResidueField R₀) → ResidueField S) x : ResidueField S)
    ((algebraMap (ResidueField R) (ResidueField S) : (a : ResidueField R) → ResidueField S)
        ((algebraMap (ResidueField R₀) (ResidueField R) : (a : ResidueField R₀) → ResidueField R) x) :
      ResidueField S)

Tactic:
obtain ⟨x, rfl⟩ := residue_surjective x

Premises used: rfl, IsLocalRing.residue_surjective
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : CommRing S
inst_3 : IsLocalRing S
inst_4 : CommRing T
inst_5 : IsLocalRing T
inst_6 : Algebra R S
inst_7 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
R₀ : Type u_4
inst_8 : CommRing R₀
inst_9 : Algebra R₀ R
inst_10 : Algebra R₀ S
inst_11 : IsScalarTower R₀ R S
inst_12 : IsLocalRing R₀
inst_13 : IsLocalHom (R := R₀) (S := R) (F := R₀ →+* R) (algebraMap R₀ R)
inst_14 : IsLocalHom (R := R₀) (S := S) (F := R₀ →+* S) (algebraMap R₀ S)
x : R₀
⊢ Eq.{u_2 + 1} (α := ResidueField S)
    ((algebraMap (ResidueField R₀) (ResidueField S) : (a : ResidueField R₀) → ResidueField S)
        ((residue R₀ : (a : R₀) → ResidueField R₀) x) :
      ResidueField S)
    ((algebraMap (ResidueField R) (ResidueField S) : (a : ResidueField R) → ResidueField S)
        ((algebraMap (ResidueField R₀) (ResidueField R) : (a : ResidueField R₀) → ResidueField R)
          ((residue R₀ : (a : R₀) → ResidueField R₀) x)) :
      ResidueField S)

Tactic:
simp [← IsScalarTower.algebraMap_apply]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : CommRing S
inst_3 : IsLocalRing S
inst_4 : CommRing T
inst_5 : IsLocalRing T
inst_6 : Algebra R S
inst_7 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_8 : Module.Finite R S
⊢ Module.Finite.{u_1, u_2} (ResidueField R) (ResidueField S)

Tactic:
.of_restrictScalars_finite R _ _

Premises used: Module.Finite.of_restrictScalars_finite
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : CommRing S
inst_3 : IsLocalRing S
inst_4 : Algebra R S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : Module.Finite R S
hfin : Finite.{u_1 + 1} (ResidueField R)
⊢ Finite.{u_2 + 1} (ResidueField S)

Tactic:
Module.finite_of_finite (ResidueField R)

Premises used: IsLocalRing.ResidueField, Module.finite_of_finite
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
inst_4 : IsLocalRing R
inst_5 : IsLocalRing S
inst_6 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
eSp : ResidueField R ⊗[R] S ≃ₐ[R]
  HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) :=
  AlgEquiv.trans (Algebra.TensorProduct.comm R (ResidueField R) S)
    (AlgEquiv.restrictScalars R (AlgEquiv.symm (quotIdealMapEquivTensorQuot S (maximalIdeal R))))
rw : Ne.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) ⊤
⊢ Nontrivial (ResidueField R ⊗[R] S)

Tactic:
rw [eSp.nontrivial_congr, Ideal.Quotient.nontrivial_iff]

Premises used: Equiv.nontrivial_congr, Ideal.Quotient.nontrivial_iff, AlgEquiv.toEquiv
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
inst_4 : IsLocalRing R
inst_5 : IsLocalRing S
inst_6 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
eSp : ResidueField R ⊗[R] S ≃ₐ[R]
  HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) :=
  AlgEquiv.trans (Algebra.TensorProduct.comm R (ResidueField R) S)
    (AlgEquiv.restrictScalars R (AlgEquiv.symm (quotIdealMapEquivTensorQuot S (maximalIdeal R))))
⊢ Ne.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) ⊤

Tactic:
((((local_hom_TFAE (algebraMap R S)).out 0 2 rfl rfl).mp inferInstance).trans_lt
      (inferInstance : (maximalIdeal S).IsMaximal).lt_top).ne

Premises used: Algebra.algebraMap, inferInstance, List.TFAE.out, Iff.mp, Ideal.IsMaximal.lt_top, OfNat.ofNat, LE.le.trans_lt, IsLocalRing.local_hom_TFAE, rfl, LT.lt.ne
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
inst_4 : IsLocalRing R
inst_5 : IsLocalRing S
inst_6 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
eSp : ResidueField R ⊗[R] S ≃ₐ[R]
  HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) :=
  AlgEquiv.trans (Algebra.TensorProduct.comm R (ResidueField R) S)
    (AlgEquiv.restrictScalars R (AlgEquiv.symm (quotIdealMapEquivTensorQuot S (maximalIdeal R))))
⊢ Ne.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) ⊤

Tactic:
exact ((((local_hom_TFAE (algebraMap R S)).out 0 2 rfl rfl).mp inferInstance).trans_lt
      (inferInstance : (maximalIdeal S).IsMaximal).lt_top).ne

Premises used: Algebra.algebraMap, inferInstance, List.TFAE.out, Iff.mp, Ideal.IsMaximal.lt_top, OfNat.ofNat, LE.le.trans_lt, IsLocalRing.local_hom_TFAE, rfl, LT.lt.ne
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
x : S ⊗[R] p.ResidueField
obtain :
  ∀ (t : p.ResidueField) (r : R) (a : S) (hrt : r • t ∉ ⊥) (e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t),
    ∃ r ∉ p, ∃ (s : S), r • x = s ⊗ₜ[R] 1
⊢ ∃ r ∉ p, ∃ (s : S), r • x = s ⊗ₜ[R] 1

Tactic:
obtain ⟨t, r, a, hrt, e⟩ := RingHom.SurjectiveOnStalks.exists_mul_eq_tmul
    p.surjectiveOnStalks_residueField x ⊥ isPrime_bot

Premises used: RingHom.SurjectiveOnStalks.exists_mul_eq_tmul, Ideal.surjectiveOnStalks_residueField, Bot.bot, Ideal.isPrime_bot
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
x : S ⊗[R] p.ResidueField
t : p.ResidueField
r : R
a : S
hrt : r • t ∉ ⊥
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
obtain :
  ∀ (t : Localization.AtPrime p)
    (hrt :
      HSMul.hSMul (β := p.ResidueField) r
          ((IsLocalRing.residue (Localization.AtPrime p) :
                (a : Localization.AtPrime p) → IsLocalRing.ResidueField (Localization.AtPrime p))
              t :
            IsLocalRing.ResidueField (Localization.AtPrime p)) ∉
        ⊥)
    (e :
      1 ⊗ₜ[R]
            HSMul.hSMul (β := p.ResidueField) r
              ((IsLocalRing.residue (Localization.AtPrime p) :
                    (a : Localization.AtPrime p) → IsLocalRing.ResidueField (Localization.AtPrime p))
                  t :
                IsLocalRing.ResidueField (Localization.AtPrime p)) *
          x =
        a ⊗ₜ[R]
          (IsLocalRing.residue (Localization.AtPrime p) :
              (a : Localization.AtPrime p) → IsLocalRing.ResidueField (Localization.AtPrime p))
            t),
    ∃ r ∉ p, ∃ (s : S), r • x = s ⊗ₜ[R] 1
⊢ ∃ r ∉ p, ∃ (s : S), r • x = s ⊗ₜ[R] 1

Tactic:
obtain ⟨t, rfl⟩ := IsLocalRing.residue_surjective t

Premises used: rfl, IsLocalRing.residue_surjective