awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Algebra R A
inst_5 : Algebra R B
I : Ideal R
inst_6 : I.IsPrime
x y : R ⧸ I
e :
  Eq (α := I.ResidueField) ((algebraMap (R ⧸ I) I.ResidueField : (a : R ⧸ I) → I.ResidueField) x : I.ResidueField)
    ((algebraMap (R ⧸ I) I.ResidueField : (a : R ⧸ I) → I.ResidueField) y : I.ResidueField)
obtain :
  ∀ (x : R)
    (e :
      Eq (α := I.ResidueField)
        ((algebraMap (R ⧸ I) I.ResidueField : (a : R ⧸ I) → I.ResidueField)
            ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x) :
          I.ResidueField)
        ((algebraMap (R ⧸ I) I.ResidueField : (a : R ⧸ I) → I.ResidueField) y : I.ResidueField)),
    ∃ (c : ↥(R ⧸ I)⁰),
      HMul.hMul (β := R ⧸ I) (↑c : R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I) = (↑c : R ⧸ I) * y
⊢ ∃ (c : ↥(R ⧸ I)⁰), (↑c : R ⧸ I) * x = (↑c : R ⧸ I) * y

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Algebra R A
inst_5 : Algebra R B
I : Ideal R
inst_6 : I.IsPrime
y : R ⧸ I
x : R
e :
  Eq (α := I.ResidueField)
    ((algebraMap (R ⧸ I) I.ResidueField : (a : R ⧸ I) → I.ResidueField) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x) :
      I.ResidueField)
    ((algebraMap (R ⧸ I) I.ResidueField : (a : R ⧸ I) → I.ResidueField) y : I.ResidueField)
obtain :
  ∀ (y : R)
    (e :
      Eq (α := I.ResidueField)
        ((algebraMap (R ⧸ I) I.ResidueField : (a : R ⧸ I) → I.ResidueField)
            ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x) :
          I.ResidueField)
        ((algebraMap (R ⧸ I) I.ResidueField : (a : R ⧸ I) → I.ResidueField)
            ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y) :
          I.ResidueField)),
    ∃ (c : ↥(R ⧸ I)⁰),
      HMul.hMul (β := R ⧸ I) (↑c : R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I) =
        HMul.hMul (β := R ⧸ I) (↑c : R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
⊢ ∃ (c : ↥(R ⧸ I)⁰),
    HMul.hMul (β := R ⧸ I) (↑c : R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I) = (↑c : R ⧸ I) * y

Tactic:
obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective y

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Algebra R A
inst_5 : Algebra R B
I : Ideal R
inst_6 : I.IsPrime
x y : R
e :
  Eq (α := I.ResidueField)
    ((algebraMap (R ⧸ I) I.ResidueField : (a : R ⧸ I) → I.ResidueField) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x) :
      I.ResidueField)
    ((algebraMap (R ⧸ I) I.ResidueField : (a : R ⧸ I) → I.ResidueField) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y) :
      I.ResidueField)
⊢ Eq (α := I.ResidueField)
    ((algebraMap (R ⧸ I) I.ResidueField : (a : R ⧸ I) → I.ResidueField)
        ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (x - y)) :
      I.ResidueField)
    (0 : I.ResidueField)

Tactic:
rw [← sub_eq_zero, ← map_sub, ← map_sub] at e

Premises used: map_sub, sub_eq_zero
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Algebra R A
inst_5 : Algebra R B
I : Ideal R
inst_6 : I.IsPrime
x y : R
e :
  Eq (α := I.ResidueField)
    ((algebraMap (R ⧸ I) I.ResidueField : (a : R ⧸ I) → I.ResidueField)
        ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (x - y)) :
      I.ResidueField)
    (0 : I.ResidueField)
⊢ Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)

Tactic:
simp only [IsLocalRing.ResidueField.algebraMap_eq, IsLocalRing.residue_eq_zero_iff,
      IsScalarTower.algebraMap_apply R (Localization.AtPrime I) I.ResidueField,
      Ideal.algebraMap_quotient_residueField_mk, IsLocalization.AtPrime.to_map_mem_maximal_iff _ I,
      ← Ideal.Quotient.mk_eq_mk_iff_sub_mem] at e

Premises used: Ideal.algebraMap_quotient_residueField_mk, IsLocalRing.residue_eq_zero_iff, Localization.AtPrime, Ideal.ResidueField, IsLocalization.AtPrime.to_map_mem_maximal_iff, IsLocalRing.ResidueField.algebraMap_eq, IsLocalization.AtPrime.isLocalRing, Ideal.Quotient.mk_eq_mk_iff_sub_mem, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Algebra R A
inst_5 : Algebra R B
I : Ideal R
inst_6 : I.IsPrime
x y : R
e :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
h :
  HMul.hMul (α := R ⧸ I) (β := R ⧸ I) ((↑1 : R ⧸ I) : R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I) =
    HMul.hMul (α := R ⧸ I) (β := R ⧸ I) ((↑1 : R ⧸ I) : R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
⊢ ∃ (c : ↥(R ⧸ I)⁰),
    HMul.hMul (β := R ⧸ I) (↑c : R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I) =
      HMul.hMul (β := R ⧸ I) (↑c : R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)

Tactic:
use 1
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Algebra R A
inst_5 : Algebra R B
I : Ideal R
inst_6 : I.IsPrime
x y : R
e :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
⊢ HMul.hMul (α := R ⧸ I) (β := R ⧸ I) ((↑1 : R ⧸ I) : R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I) =
    HMul.hMul (α := R ⧸ I) (β := R ⧸ I) ((↑1 : R ⧸ I) : R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)

Tactic:
simp [e]
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsMaximal
⊢ Function.Bijective.{u_1 + 1, u_1 + 1} (α := R ⧸ I) (β := I.ResidueField)
    (⇑(algebraMap (R ⧸ I) I.ResidueField) : (a : R ⧸ I) → I.ResidueField)

Tactic:
⟨I.injective_algebraMap_quotient_residueField, IsFractionRing.surjective_iff_isField.mpr
    ((Quotient.maximal_ideal_iff_isField_quotient I).mp inferInstance)⟩

Premises used: Iff.mpr, IsFractionRing.surjective_iff_isField, inferInstance, And.intro, Ideal.injective_algebraMap_quotient_residueField, Iff.mp, Function.Bijective, Ideal.Quotient.maximal_ideal_iff_isField_quotient
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsMaximal
rw :
  Function.Surjective (α := R) (β := I.ResidueField)
    (⇑(@RingHom.comp _ (R ⧸ I) _ _ Semiring.toNonAssocSemiring _ (algebraMap (R ⧸ I) I.ResidueField)
          (algebraMap R (R ⧸ I))) :
      (a : R) → I.ResidueField)
⊢ Function.Surjective (α := R) (β := I.ResidueField) (⇑(algebraMap R I.ResidueField) : (a : R) → I.ResidueField)

Tactic:
rw [IsScalarTower.algebraMap_eq R (R ⧸ I) _]

Premises used: HasQuotient.Quotient, IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsMaximal
⊢ Function.Surjective (α := R) (β := I.ResidueField)
    (⇑(@RingHom.comp _ (R ⧸ I) _ _ Semiring.toNonAssocSemiring _ (algebraMap (R ⧸ I) I.ResidueField)
          (algebraMap R (R ⧸ I))) :
      (a : R) → I.ResidueField)

Tactic:
I.bijective_algebraMap_quotient_residueField.surjective.comp Ideal.Quotient.mk_surjective

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, Ideal.Quotient.mk_surjective, Function.Bijective.surjective, Function.Surjective.comp, Ideal.bijective_algebraMap_quotient_residueField
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsMaximal
⊢ Function.Surjective (α := R) (β := I.ResidueField)
    (⇑(@RingHom.comp _ (R ⧸ I) _ _ Semiring.toNonAssocSemiring _ (algebraMap (R ⧸ I) I.ResidueField)
          (algebraMap R (R ⧸ I))) :
      (a : R) → I.ResidueField)

Tactic:
exact I.bijective_algebraMap_quotient_residueField.surjective.comp Ideal.Quotient.mk_surjective

Premises used: Ideal.Quotient.mk_surjective, Function.Bijective.surjective, Function.Surjective.comp, Ideal.bijective_algebraMap_quotient_residueField
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Algebra R A
inst_5 : Algebra R B
I_1 : Ideal R
inst_6 : I_1.IsPrime
I : Ideal R
inst_7 : I.IsMaximal
⊢ Module.Finite R I.ResidueField

Tactic:
.of_surjective (Algebra.linearMap _ _) I.algebraMap_residueField_surjective

Premises used: Module.Finite.of_surjective, Ideal.algebraMap_residueField_surjective, Algebra.linearMap
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Algebra R A
inst_5 : Algebra R B
I : Ideal R
inst_6 : I.IsPrime
k : Type u_5
inst_7 : Field k
p : Ideal k
inst_8 : p.IsPrime
⊢ p.IsMaximal

Tactic:
simpa [p.eq_bot_of_prime] using Ideal.bot_isMaximal

Premises used: Ideal.eq_bot_of_prime, Ideal.bot_isMaximal
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
k : Type u_5
inst : Field k
p : Ideal k
inst_1 : p.IsPrime
x : k
⊢ Eq (α := p.ResidueField) ((p.algEquivResidueFieldOfField : (a : k) → p.ResidueField) x : p.ResidueField)
    ((algebraMap k p.ResidueField : (a : k) → p.ResidueField) x : p.ResidueField)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
⊢ RingHom.SurjectiveOnStalks (S := I.ResidueField) (algebraMap R I.ResidueField)

Tactic:
(RingHom.surjectiveOnStalks_of_surjective Ideal.Quotient.mk_surjective).comp
    (RingHom.surjectiveOnStalks_of_isLocalization I.primeCompl _)

Premises used: RingHom.surjectiveOnStalks_of_surjective, Ideal.Quotient.mk_surjective, IsLocalRing.ResidueField, Ideal.primeCompl, RingHom.SurjectiveOnStalks.comp, RingHom.surjectiveOnStalks_of_isLocalization
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Algebra R A
inst_5 : Algebra R B
I : Ideal R
inst_6 : I.IsPrime
p : Ideal R
inst_7 : p.IsPrime
q : Ideal A
inst_8 : q.IsPrime
inst_9 : q.LiesOver p
inst_10 : Algebra.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime q)
inst_11 : Localization.AtPrime.IsLiesOverAlgebra p q
rw :
  IsLocalHom (R := Localization.AtPrime p) (S := Localization.AtPrime q) (F :=
    RingHom.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime q))
    (Localization.localRingHom p q (algebraMap R A) ⋯)
⊢ IsLocalHom (R := Localization.AtPrime p) (S := Localization.AtPrime q) (F :=
    RingHom.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime q))
    (algebraMap (Localization.AtPrime p) (Localization.AtPrime q))

Tactic:
rw [Localization.AtPrime.IsLiesOverAlgebra.algebraMap_eq]

Premises used: Localization.AtPrime.IsLiesOverAlgebra.algebraMap_eq
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Algebra R A
inst_5 : Algebra R B
I : Ideal R
inst_6 : I.IsPrime
p : Ideal R
inst_7 : p.IsPrime
q : Ideal A
inst_8 : q.IsPrime
inst_9 : q.LiesOver p
inst_10 : Algebra.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime q)
inst_11 : Localization.AtPrime.IsLiesOverAlgebra p q
⊢ IsLocalHom (R := Localization.AtPrime p) (S := Localization.AtPrime q) (F :=
    RingHom.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime q))
    (Localization.localRingHom p q (algebraMap R A) ⋯)

Tactic:
Localization.isLocalHom_localRingHom _ _ _ (Ideal.over_def _ _)

Premises used: Ideal.over_def, Localization.isLocalHom_localRingHom
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Algebra R A
inst_5 : Algebra R B
I : Ideal R
inst_6 : I.IsPrime
p : Ideal R
inst_7 : p.IsPrime
q : Ideal A
inst_8 : q.IsPrime
inst_9 : q.LiesOver p
inst_10 : Algebra.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime q)
inst_11 : Localization.AtPrime.IsLiesOverAlgebra p q
⊢ IsLocalHom (R := Localization.AtPrime p) (S := Localization.AtPrime q) (F :=
    RingHom.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime q))
    (Localization.localRingHom p q (algebraMap R A) ⋯)

Tactic:
exact Localization.isLocalHom_localRingHom _ _ _ (Ideal.over_def _ _)

Premises used: Ideal.over_def, Localization.isLocalHom_localRingHom
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Algebra R A
inst_5 : Algebra R B
I : Ideal R
inst_6 : I.IsPrime
p : Ideal R
inst_7 : p.IsPrime
⊢ Algebra.EssFiniteType R p.ResidueField

Tactic:
.comp _ (Localization.AtPrime p) _

Premises used: Localization.AtPrime, Algebra.EssFiniteType.comp
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Algebra R A
inst_5 : Algebra R B
I : Ideal R
inst_6 : I.IsPrime
inst_7 : Algebra.EssFiniteType R A
p : Ideal R
inst_8 : p.IsPrime
q : Ideal A
inst_9 : q.IsPrime
inst_10 : q.LiesOver p
inst_11 : Algebra.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime q)
inst_12 : Localization.AtPrime.IsLiesOverAlgebra p q
⊢ Algebra.EssFiniteType.{u_1, u_3} R q.ResidueField

Tactic:
have : Algebra.EssFiniteType R q.ResidueField := .comp _ A _
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Algebra R A
inst_5 : Algebra R B
I : Ideal R
inst_6 : I.IsPrime
inst_7 : Algebra.EssFiniteType R A
p : Ideal R
inst_8 : p.IsPrime
q : Ideal A
inst_9 : q.IsPrime
inst_10 : q.LiesOver p
inst_11 : Algebra.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime q)
inst_12 : Localization.AtPrime.IsLiesOverAlgebra p q
this : Algebra.EssFiniteType.{u_1, u_3} R q.ResidueField
⊢ Algebra.EssFiniteType.{u_1, u_3} p.ResidueField q.ResidueField

Tactic:
.of_comp R _ _

Premises used: Algebra.EssFiniteType.of_comp
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Algebra R A
inst_5 : Algebra R B
I : Ideal R
inst_6 : I.IsPrime
inst_7 : Algebra.EssFiniteType R A
p : Ideal R
inst_8 : p.IsPrime
q : Ideal A
inst_9 : q.IsPrime
inst_10 : q.LiesOver p
inst_11 : Algebra.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime q)
inst_12 : Localization.AtPrime.IsLiesOverAlgebra p q
this : Algebra.EssFiniteType.{u_1, u_3} R q.ResidueField
⊢ Algebra.EssFiniteType.{u_1, u_3} p.ResidueField q.ResidueField

Tactic:
refine .of_comp R _ _
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Algebra R A
inst_5 : Algebra R B
I : Ideal R
inst_6 : I.IsPrime
f : R →+* S
hf₁ : I ≤ RingHom.ker f
hf₂ : I.primeCompl ≤ Submonoid.comap f (IsUnit.submonoid S)
⊢ ∀ (y : ↥(R ⧸ I)⁰), IsUnit.{u_2} (M := S) ((Quotient.lift I f hf₁ : (a : R ⧸ I) → S) (↑y : R ⧸ I) : S)

Tactic:
simpa [Ideal.Quotient.mk_surjective.forall, Ideal.Quotient.eq_zero_iff_mem]

Premises used: Function.Surjective.forall, Ideal.Quotient.eq_zero_iff_mem, Ideal.Quotient.mk_surjective
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
inst_2 : I.IsPrime
f : R →+* S
hf₁ : I ≤ RingHom.ker f
hf₂ : I.primeCompl ≤ Submonoid.comap f (IsUnit.submonoid S)
r : R
rw :
  Eq.{u_2 + 1} (α := S)
    ((Quotient.lift I f hf₁ : (a : R ⧸ I) → S) ((algebraMap R (R ⧸ I) : (a : R) → R ⧸ I) r : R ⧸ I) : S)
    ((f : (a : R) → S) r : S)
⊢ Eq.{u_2 + 1} (α := S)
    ((lift I f hf₁ hf₂ : (a : I.ResidueField) → S)
        ((algebraMap R I.ResidueField : (a : R) → I.ResidueField) r : I.ResidueField) :
      S)
    ((f : (a : R) → S) r : S)

Tactic:
rw [lift, IsScalarTower.algebraMap_apply R (R ⧸ I) I.ResidueField, IsLocalization.lift_eq]

Premises used: IsLocalization.lift_eq, Ideal.ResidueField, HasQuotient.Quotient, Ideal.ResidueField.lift, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
inst_2 : I.IsPrime
f : R →+* S
hf₁ : I ≤ RingHom.ker f
hf₂ : I.primeCompl ≤ Submonoid.comap f (IsUnit.submonoid S)
r : R
⊢ Eq.{u_2 + 1} (α := S)
    ((Quotient.lift I f hf₁ : (a : R ⧸ I) → S) ((algebraMap R (R ⧸ I) : (a : R) → R ⧸ I) r : R ⧸ I) : S)
    ((f : (a : R) → S) r : S)

Tactic:
simp
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Algebra R A
inst_5 : Algebra R B
I_1 : Ideal R
inst_6 : I_1.IsPrime
I : Ideal A
inst_7 : I.IsPrime
f : A →ₐ[R] B
hf₁ : I ≤ RingHom.ker f
hf₂ : I.primeCompl ≤ Submonoid.comap f (IsUnit.submonoid B)
r : R
⊢ (↑(↑(lift I f.toRingHom hf₁ hf₂) : I.ResidueField →* B) : OneHom I.ResidueField B).toFun
      ((algebraMap R I.ResidueField : (a : R) → I.ResidueField) r) =
    (algebraMap R B : (a : R) → B) r

Tactic:
simp [IsScalarTower.algebraMap_apply R A I.ResidueField]

Premises used: Ideal.ResidueField, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal A
inst_5 : I.IsPrime
f : A →ₐ[R] B
hf₁ : I ≤ RingHom.ker f
hf₂ : I.primeCompl ≤ Submonoid.comap f (IsUnit.submonoid B)
r : A
⊢ Eq.{u_4 + 1} (α := B)
    ((liftₐ I f hf₁ hf₂ : (a : I.ResidueField) → B)
        ((algebraMap A I.ResidueField : (a : A) → I.ResidueField) r : I.ResidueField) :
      B)
    ((f : (a : A) → B) r : B)

Tactic:
lift_algebraMap _ _ _ hf₂ _

Premises used: Ideal.ResidueField.lift_algebraMap
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal A
inst_5 : I.IsPrime
f : A →ₐ[R] B
hf₁ : I ≤ RingHom.ker f
hf₂ : I.primeCompl ≤ Submonoid.comap f (IsUnit.submonoid B)
⊢ (liftₐ I f hf₁ hf₂).comp (IsScalarTower.toAlgHom R A I.ResidueField) = f

Tactic:
AlgHom.ext fun _ ↦ liftₐ_algebraMap _ _ _ hf₂ _

Premises used: AlgHom.ext, Ideal.ResidueField.liftₐ_algebraMap
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
inst_2 : I.IsPrime
f g : RingHom.{u_1, u_2} I.ResidueField S
H : Eq (α := R →+* S) (f.comp (algebraMap R I.ResidueField)) (g.comp (algebraMap R I.ResidueField))
⊢ f = g

Tactic:
IsLocalization.ringHom_ext (R ⧸ I)⁰ (Ideal.Quotient.ringHom_ext H)

Premises used: Ideal.Quotient.ringHom_ext, nonZeroDivisors, HasQuotient.Quotient, IsLocalization.ringHom_ext
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal A
inst_5 : I.IsPrime
f g : AlgHom.{u_1, u_3, u_4} R I.ResidueField B
H :
  Eq (α := A →ₐ[R] B) (f.comp (IsScalarTower.toAlgHom R A I.ResidueField))
    (g.comp (IsScalarTower.toAlgHom R A I.ResidueField))
⊢ f = g

Tactic:
AlgHom.coe_ringHom_injective (ringHom_ext congr($H))

Premises used: AlgHom.coe_ringHom_injective, congrArg, id, RingHomClass.toRingHom, Ideal.ResidueField.ringHom_ext
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
p : Ideal A
q : Ideal B
inst_7 : q.LiesOver p
inst_8 : p.IsMaximal
inst_9 : q.IsMaximal
inst_10 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime q)
inst_11 : Localization.AtPrime.IsLiesOverAlgebra p q
inst_12 : Algebra.IsSeparable.{u_2, u_3} (A ⧸ p) (B ⧸ q)
⊢ Algebra.IsSeparable.{u_2, u_3} p.ResidueField q.ResidueField

Tactic:
Algebra.IsSeparable.of_equiv_equiv
    (.ofBijective _ p.bijective_algebraMap_quotient_residueField)
    (.ofBijective _ q.bijective_algebraMap_quotient_residueField) ?_

Premises used: Algebra.IsSeparable.of_equiv_equiv, RingEquiv.ofBijective, Ideal.bijective_algebraMap_quotient_residueField
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
p : Ideal A
q : Ideal B
inst_7 : q.LiesOver p
inst_8 : p.IsMaximal
inst_9 : q.IsMaximal
inst_10 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime q)
inst_11 : Localization.AtPrime.IsLiesOverAlgebra p q
inst_12 : Algebra.IsSeparable.{u_2, u_3} (A ⧸ p) (B ⧸ q)
refine :
  Eq (α := RingHom.{u_2, u_3} (A ⧸ p) q.ResidueField)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap p.ResidueField q.ResidueField)
      (↑(RingEquiv.ofBijective (F := A ⧸ p →+* p.ResidueField)
            (algebraMap (A ⧸ p) p.ResidueField : A ⧸ p →+* p.ResidueField) ⋯) :
        A ⧸ p →+* p.ResidueField))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(RingEquiv.ofBijective (F := B ⧸ q →+* q.ResidueField)
            (algebraMap (B ⧸ q) q.ResidueField : B ⧸ q →+* q.ResidueField) ⋯) :
        B ⧸ q →+* q.ResidueField)
      (algebraMap (A ⧸ p) (B ⧸ q)))
⊢ Algebra.IsSeparable.{u_2, u_3} p.ResidueField q.ResidueField

Tactic:
refine Algebra.IsSeparable.of_equiv_equiv
    (.ofBijective _ p.bijective_algebraMap_quotient_residueField)
    (.ofBijective _ q.bijective_algebraMap_quotient_residueField) ?_

Premises used: Algebra.IsSeparable.of_equiv_equiv, RingEquiv.ofBijective, Ideal.bijective_algebraMap_quotient_residueField