awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
p_1 : Ideal R_1
inst_3 : p_1.IsPrime
R : Type u_3
S : Type u_4
inst_4 : CommRing R
inst_5 : CommRing S
inst_6 : Algebra R S
p : PrimeSpectrum R
H : Topology.IsEmbedding (X := PrimeSpectrum (p.asIdeal.Fiber S)) (Y :=
  (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_4))
  (⇑(OrderIso.symm (preimageOrderIsoFiber R S p)) :
    (a : PrimeSpectrum (p.asIdeal.Fiber S)) → (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_4)) :=
  ⋯
x : PrimeSpectrum (p.asIdeal.Fiber S)
h :
  (preimageOrderIsoFiber R S p :
        (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_4)) → PrimeSpectrum (p.asIdeal.Fiber S))
      ((H.toHomeomorphOfSurjective ⋯ :
          (a : PrimeSpectrum (p.asIdeal.Fiber S)) → (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_4))
        x) =
    x
⊢ Eq (α := PrimeSpectrum (p.asIdeal.Fiber S))
    (Equiv.toFun
      (RelIso.toEquiv (r :=
        fun (x1 x2 : (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_4)) ↦ x1 ≤ x2) (s :=
        fun (x1 x2 : PrimeSpectrum (p.asIdeal.Fiber S)) ↦ x1 ≤ x2) (preimageOrderIsoFiber R S p))
      ((H.toHomeomorphOfSurjective ⋯ :
          (a : PrimeSpectrum (p.asIdeal.Fiber S)) → (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_4))
        x))
    (((H.toHomeomorphOfSurjective ⋯).symm :
        (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_4)) → PrimeSpectrum (p.asIdeal.Fiber S))
      ((H.toHomeomorphOfSurjective ⋯ :
          (a : PrimeSpectrum (p.asIdeal.Fiber S)) → (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_4))
        x))

Tactic:
simp only [Equiv.toFun_as_coe, RelIso.coe_fn_toEquiv, Homeomorph.symm_apply_apply]

Premises used: Equiv.toFun_as_coe, Homeomorph.symm_apply_apply, RelIso.coe_fn_toEquiv
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
p_1 : Ideal R_1
inst_3 : p_1.IsPrime
R : Type u_3
S : Type u_4
inst_4 : CommRing R
inst_5 : CommRing S
inst_6 : Algebra R S
p : PrimeSpectrum R
H : Topology.IsEmbedding (X := PrimeSpectrum (p.asIdeal.Fiber S)) (Y :=
  (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_4))
  (⇑(OrderIso.symm (preimageOrderIsoFiber R S p)) :
    (a : PrimeSpectrum (p.asIdeal.Fiber S)) → (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_4)) :=
  ⋯
x : PrimeSpectrum (p.asIdeal.Fiber S)
⊢ (preimageOrderIsoFiber R S p :
        (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_4)) → PrimeSpectrum (p.asIdeal.Fiber S))
      ((H.toHomeomorphOfSurjective ⋯ :
          (a : PrimeSpectrum (p.asIdeal.Fiber S)) → (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_4))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
p_1 : Ideal R_1
inst_3 : p_1.IsPrime
R : Type u_3
S : Type u_4
inst_4 : CommRing R
inst_5 : CommRing S
inst_6 : Algebra R S
p : PrimeSpectrum R
H : Topology.IsEmbedding (X := PrimeSpectrum (p.asIdeal.Fiber S)) (Y :=
  (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_4))
  (⇑(OrderIso.symm (preimageOrderIsoFiber R S p)) :
    (a : PrimeSpectrum (p.asIdeal.Fiber S)) → (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_4)) :=
  ⋯
⊢ (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_4) ≃ₜ PrimeSpectrum (p.asIdeal.Fiber S)

Tactic:
exact
  { __ := preimageOrderIsoFiber R S p
    continuous_toFun := by
      convert!
        (H.toHomeomorphOfSurjective (preimageOrderIsoFiber R S p).symm.surjective).symm.continuous
      ext1 x
      obtain ⟨x, rfl⟩ := (H.toHomeomorphOfSurjective
        (preimageOrderIsoFiber R S p).symm.surjective).surjective x
      simp only [Equiv.toFun_as_coe, RelIso.coe_fn_toEquiv, Homeomorph.symm_apply_apply]
      simp
    continuous_invFun := H.continuous }

Premises used: PrimeSpectrum.preimageOrderIsoFiber
-- 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
J : Ideal S
inst_3 : J.IsPrime
f : R →+* S
hf : I = comap f J
r : R
simp :
  Eq (α := J.ResidueField)
    ((IsLocalRing.residue (Localization.AtPrime J) :
          (a : Localization.AtPrime J) → IsLocalRing.ResidueField (Localization.AtPrime J))
        ((algebraMap S (Localization.AtPrime J) : (a : S) → Localization.AtPrime J) ((f : (a : R) → S) r)) :
      IsLocalRing.ResidueField (Localization.AtPrime J))
    ((algebraMap S J.ResidueField : (a : S) → J.ResidueField) ((f : (a : R) → S) r) : J.ResidueField)
⊢ Eq.{u_2 + 1} (α := J.ResidueField)
    (((map I J f hf : RingHom.{u_1, u_2} I.ResidueField J.ResidueField) : (a : I.ResidueField) → J.ResidueField)
        ((algebraMap (Localization.AtPrime I) I.ResidueField : (a : Localization.AtPrime I) → I.ResidueField)
          ((algebraMap R (Localization.AtPrime I) : (a : R) → Localization.AtPrime I) r)) :
      J.ResidueField)
    ((algebraMap S J.ResidueField : (a : S) → J.ResidueField) ((f : (a : R) → S) r) : J.ResidueField)

Tactic:
simp [IsLocalRing.ResidueField.map_residue, Localization.localRingHom_to_map]

Premises used: Localization.localRingHom_to_map, IsLocalRing.ResidueField.map_residue
-- 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
J : Ideal S
inst_3 : J.IsPrime
f : R →+* S
hf : I = comap f J
r : R
⊢ Eq (α := J.ResidueField)
    ((IsLocalRing.residue (Localization.AtPrime J) :
          (a : Localization.AtPrime J) → IsLocalRing.ResidueField (Localization.AtPrime J))
        ((algebraMap S (Localization.AtPrime J) : (a : S) → Localization.AtPrime J) ((f : (a : R) → S) r)) :
      IsLocalRing.ResidueField (Localization.AtPrime J))
    ((algebraMap S J.ResidueField : (a : S) → J.ResidueField) ((f : (a : R) → S) r) : J.ResidueField)

Tactic:
rfl
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
H : f.SurjectiveOnStalks
J : Ideal S
inst_2 : J.IsPrime
inst_3 : Ideal.IsPrime (Ideal.comap f J)
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := Ideal.ResidueField (Ideal.comap f J)) (β := J.ResidueField)
    (⇑(Ideal.ResidueField.map (Ideal.comap f J) J f ⋯) : (a : (Ideal.comap f J).ResidueField) → J.ResidueField)

Tactic:
⟨RingHom.injective _, Ideal.Quotient.lift_surjective_of_surjective _ _
    (Ideal.Quotient.mk_surjective.comp (H J ‹_›))⟩

Premises used: Ideal.Quotient.lift_surjective_of_surjective, RingHom.injective, Ideal.Quotient.mk_surjective, And.intro, Function.Surjective.comp, Function.Bijective
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
H : f.SurjectiveOnStalks
J : Ideal S
inst_2 : J.IsPrime
inst_3 : Ideal.IsPrime (Ideal.comap f J)
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := Ideal.ResidueField (Ideal.comap f J)) (β := J.ResidueField)
    (⇑(Ideal.ResidueField.map (Ideal.comap f J) J f ⋯) : (a : (Ideal.comap f J).ResidueField) → J.ResidueField)

Tactic:
exact ⟨RingHom.injective _, Ideal.Quotient.lift_surjective_of_surjective _ _
    (Ideal.Quotient.mk_surjective.comp (H J ‹_›))⟩
-- 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
J : Ideal B
inst_8 : J.IsPrime
f : A →ₐ[R] B
hf : I = comap f.toRingHom J
r : R
⊢ Eq (α := J.ResidueField)
    (OneHom.toFun (M := I.ResidueField)
      (↑(↑(map I J (↑f : A →+* B) hf) : I.ResidueField →* J.ResidueField) : OneHom I.ResidueField J.ResidueField)
      ((algebraMap R I.ResidueField : (a : R) → I.ResidueField) r))
    ((algebraMap R J.ResidueField : (a : R) → J.ResidueField) r)

Tactic:
simp [IsScalarTower.algebraMap_apply R A I.ResidueField,
      IsScalarTower.algebraMap_apply R B J.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
J : Ideal B
inst_6 : J.IsPrime
f : A →ₐ[R] B
hf : I = comap f.toRingHom J
x : I.ResidueField
⊢ Eq.{u_4 + 1} (α := J.ResidueField)
    (((mapₐ I J f hf : AlgHom.{u_1, u_3, u_4} R I.ResidueField J.ResidueField) : (a : I.ResidueField) → J.ResidueField)
        x :
      J.ResidueField)
    (((map I J f.toRingHom hf : RingHom.{u_3, u_4} I.ResidueField J.ResidueField) :
          (a : I.ResidueField) → J.ResidueField)
        x :
      J.ResidueField)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
x : R
rw :
  Membership.mem (α := Localization.AtPrime I) (γ := Ideal (Localization.AtPrime I))
      (IsLocalRing.maximalIdeal (Localization.AtPrime I))
      ((algebraMap R (Localization.AtPrime I) : (a : R) → Localization.AtPrime I) x : Localization.AtPrime I) ↔
    x ∈ I
⊢ Eq (α := I.ResidueField) ((algebraMap R I.ResidueField : (a : R) → I.ResidueField) x : I.ResidueField)
      (0 : I.ResidueField) ↔
    x ∈ I

Tactic:
rw [IsScalarTower.algebraMap_apply R (Localization.AtPrime I),
    IsLocalRing.ResidueField.algebraMap_eq, IsLocalRing.residue_eq_zero_iff]

Premises used: IsLocalRing.residue_eq_zero_iff, Localization.AtPrime, IsLocalRing.ResidueField.algebraMap_eq, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
x : R
⊢ Membership.mem (α := Localization.AtPrime I) (γ := Ideal (Localization.AtPrime I))
      (IsLocalRing.maximalIdeal (Localization.AtPrime I))
      ((algebraMap R (Localization.AtPrime I) : (a : R) → Localization.AtPrime I) x : Localization.AtPrime I) ↔
    x ∈ I

Tactic:
IsLocalization.AtPrime.to_map_mem_maximal_iff _ _ _

Premises used: Set.Mem, IsLocalization.AtPrime.to_map_mem_maximal_iff, IsLocalization.AtPrime.isLocalRing
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
x : R
⊢ Membership.mem (α := Localization.AtPrime I) (γ := Ideal (Localization.AtPrime I))
      (IsLocalRing.maximalIdeal (Localization.AtPrime I))
      ((algebraMap R (Localization.AtPrime I) : (a : R) → Localization.AtPrime I) x : Localization.AtPrime I) ↔
    x ∈ I

Tactic:
exact IsLocalization.AtPrime.to_map_mem_maximal_iff _ _ _

Premises used: IsLocalization.AtPrime.to_map_mem_maximal_iff, IsLocalization.AtPrime.isLocalRing
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
⊢ RingHom.ker (F := R →+* I.ResidueField) (algebraMap R I.ResidueField) = I

Tactic:
Ideal.ext fun _ ↦ Ideal.algebraMap_residueField_eq_zero

Premises used: Ideal.ext, Ideal.algebraMap_residueField_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_1 : Ideal R
inst_6 : I_1.IsPrime
I : Ideal A
inst_7 : I.IsPrime
⊢ IsScalarTower.{u_1, u_3, u_3} R (A ⧸ I) I.ResidueField

Tactic:
.of_algebraMap_eq' rfl

Premises used: IsScalarTower.of_algebraMap_eq', 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_1 : Ideal R
inst_6 : I_1.IsPrime
I : Ideal R
inst_7 : I.IsPrime
⊢ Ideal.LiesOver (B := I.ResidueField) ⊥ I

Tactic:
⟨I.ker_algebraMap_residueField.symm⟩

Premises used: Ideal.ker_algebraMap_residueField, Ideal.LiesOver.mk, Eq.symm
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
x : R
⊢ Eq (α := I.ResidueField)
    ((algebraMap (R ⧸ I) I.ResidueField : (a : R ⧸ I) → I.ResidueField) ((Quotient.mk I : (a : R) → R ⧸ I) x) :
      I.ResidueField)
    ((algebraMap R I.ResidueField : (a : R) → I.ResidueField) x : I.ResidueField)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, 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
rw : Eq (α := Ideal (R ⧸ I)) (RingHom.ker (F := R ⧸ I →+* I.ResidueField) (algebraMap (R ⧸ I) I.ResidueField)) ⊥
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := R ⧸ I) (β := I.ResidueField)
    (⇑(algebraMap (R ⧸ I) I.ResidueField) : (a : R ⧸ I) → I.ResidueField)

Tactic:
rw [RingHom.injective_iff_ker_eq_bot]

Premises used: RingHom.injective_iff_ker_eq_bot
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
⊢ Eq (α := Ideal (R ⧸ I)) (RingHom.ker (F := R ⧸ I →+* I.ResidueField) (algebraMap (R ⧸ I) I.ResidueField)) ⊥

Tactic:
(Ideal.ker_quotient_lift _ _).trans ?_

Premises used: Ideal.ker_quotient_lift, Ideal.Quotient.lift, Eq.trans
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
refine :
  Eq (α := Ideal (R ⧸ I))
    (map (F := R →+* R ⧸ I) (Quotient.mk I)
      (RingHom.ker (F := R →+* I.ResidueField) (↑(Algebra.ofId R I.ResidueField) : R →+* I.ResidueField)))
    ⊥
⊢ Eq (α := Ideal (R ⧸ I)) (RingHom.ker (F := R ⧸ I →+* I.ResidueField) (algebraMap (R ⧸ I) I.ResidueField)) ⊥

Tactic:
refine (Ideal.ker_quotient_lift _ _).trans ?_

Premises used: Ideal.ker_quotient_lift, Eq.trans
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
change :
  Eq (α := Ideal (R ⧸ I))
    (map (F := R →+* R ⧸ I) (Quotient.mk I) (RingHom.ker (F := R →+* I.ResidueField) (algebraMap R I.ResidueField))) ⊥
⊢ Eq (α := Ideal (R ⧸ I))
    (map (F := R →+* R ⧸ I) (Quotient.mk I)
      (RingHom.ker (F := R →+* I.ResidueField) (↑(Algebra.ofId R I.ResidueField) : R →+* I.ResidueField)))
    ⊥

Tactic:
change map (Quotient.mk I) (RingHom.ker (algebraMap R I.ResidueField)) = ⊥

Premises used: Algebra.algebraMap, Ideal.Quotient.mk, Ideal.ResidueField, Ideal.map, RingHom.ker
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
rw : Eq (α := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) I) ⊥
rw₁ rw₂ : Eq.{u_1 + 1} (α := Ideal (R ⧸ I)) ⊥ ⊥
⊢ Eq (α := Ideal (R ⧸ I))
    (map (F := R →+* R ⧸ I) (Quotient.mk I) (RingHom.ker (F := R →+* I.ResidueField) (algebraMap R I.ResidueField))) ⊥

Tactic:
rw [Ideal.ker_algebraMap_residueField, map_quotient_self]

Premises used: Ideal.ker_algebraMap_residueField, Ideal.map_quotient_self
-- 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 : I.ResidueField
obtain :
  ∀ (x : Localization.AtPrime I),
    ∃ (x_1 : (R ⧸ I) × ↥(R ⧸ I)⁰),
      HMul.hMul (α := I.ResidueField) (β := I.ResidueField)
          ((IsLocalRing.residue (Localization.AtPrime I) :
                (a : Localization.AtPrime I) → IsLocalRing.ResidueField (Localization.AtPrime I))
              x :
            IsLocalRing.ResidueField (Localization.AtPrime I))
          ((algebraMap (R ⧸ I) I.ResidueField : (a : R ⧸ I) → I.ResidueField) (↑x_1.2 : R ⧸ I) : I.ResidueField) =
        (algebraMap (R ⧸ I) I.ResidueField : (a : R ⧸ I) → I.ResidueField) x_1.1
⊢ ∃ (x_1 : (R ⧸ I) × ↥(R ⧸ I)⁰),
    HMul.hMul (β := I.ResidueField) x
        ((algebraMap (R ⧸ I) I.ResidueField : (a : R ⧸ I) → I.ResidueField) (↑x_1.2 : R ⧸ I) : I.ResidueField) =
      (algebraMap (R ⧸ I) I.ResidueField : (a : R ⧸ I) → I.ResidueField) x_1.1

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

Premises used: rfl, IsLocalRing.residue_surjective
-- 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 : Localization.AtPrime I
obtain :
  ∀ (x s : R) (hs : s ∈ I.primeCompl),
    ∃ (x_1 : (R ⧸ I) × ↥(R ⧸ I)⁰),
      HMul.hMul (α := I.ResidueField) (β := I.ResidueField)
          ((IsLocalRing.residue (Localization.AtPrime I) :
                (a : Localization.AtPrime I) → IsLocalRing.ResidueField (Localization.AtPrime I))
              (IsLocalization.mk' (Localization.AtPrime I) x (Subtype.mk (p := fun (x : R) ↦ x ∈ I.primeCompl) s hs)) :
            IsLocalRing.ResidueField (Localization.AtPrime I))
          ((algebraMap (R ⧸ I) I.ResidueField : (a : R ⧸ I) → I.ResidueField) (↑x_1.2 : R ⧸ I) : I.ResidueField) =
        (algebraMap (R ⧸ I) I.ResidueField : (a : R ⧸ I) → I.ResidueField) x_1.1
⊢ ∃ (x_1 : (R ⧸ I) × ↥(R ⧸ I)⁰),
    HMul.hMul (α := I.ResidueField) (β := I.ResidueField)
        ((IsLocalRing.residue (Localization.AtPrime I) :
              (a : Localization.AtPrime I) → IsLocalRing.ResidueField (Localization.AtPrime I))
            x :
          IsLocalRing.ResidueField (Localization.AtPrime I))
        ((algebraMap (R ⧸ I) I.ResidueField : (a : R ⧸ I) → I.ResidueField) (↑x_1.2 : R ⧸ I) : I.ResidueField) =
      (algebraMap (R ⧸ I) I.ResidueField : (a : R ⧸ I) → I.ResidueField) x_1.1

Tactic:
obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq I.primeCompl x

Premises used: Ideal.primeCompl, rfl, IsLocalization.exists_mk'_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
x s : R
hs : s ∈ I.primeCompl
⊢ ∃ (x_1 : (R ⧸ I) × ↥(R ⧸ I)⁰),
    HMul.hMul (α := I.ResidueField) (β := I.ResidueField)
        ((IsLocalRing.residue (Localization.AtPrime I) :
              (a : Localization.AtPrime I) → IsLocalRing.ResidueField (Localization.AtPrime I))
            (IsLocalization.mk' (Localization.AtPrime I) x (Subtype.mk (p := fun (x : R) ↦ x ∈ I.primeCompl) s hs)) :
          IsLocalRing.ResidueField (Localization.AtPrime I))
        ((algebraMap (R ⧸ I) I.ResidueField : (a : R ⧸ I) → I.ResidueField) (↑x_1.2 : R ⧸ I) : I.ResidueField) =
      (algebraMap (R ⧸ I) I.ResidueField : (a : R ⧸ I) → I.ResidueField) x_1.1

Tactic:
⟨⟨Ideal.Quotient.mk _ x, ⟨Ideal.Quotient.mk _ s, ?_⟩⟩, ?_⟩

Premises used: Ideal.Quotient.mk, Prod.mk, Subtype.mk, Exists.intro, DFunLike.coe
-- 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 s : R
hs : s ∈ I.primeCompl
refine_1 :
  Membership.mem (α := R ⧸ I) (γ := Submonoid (R ⧸ I)) (R ⧸ I)⁰ ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) s : R ⧸ I)
refine_2 :
  HMul.hMul (α := I.ResidueField) (β := I.ResidueField)
      ((IsLocalRing.residue (Localization.AtPrime I) :
            (a : Localization.AtPrime I) → IsLocalRing.ResidueField (Localization.AtPrime I))
          (IsLocalization.mk' (Localization.AtPrime I) x (Subtype.mk (p := fun (x : R) ↦ x ∈ I.primeCompl) s hs)) :
        IsLocalRing.ResidueField (Localization.AtPrime I))
      ((algebraMap (R ⧸ I) I.ResidueField : (a : R ⧸ I) → I.ResidueField)
          (↑((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x,
                  Subtype.mk (p := fun (x : R ⧸ I) ↦ Membership.mem (γ := Submonoid (R ⧸ I)) (R ⧸ I)⁰ x)
                    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) s) ⋯).2 :
            R ⧸ I) :
        I.ResidueField) =
    (algebraMap (R ⧸ I) I.ResidueField : (a : R ⧸ I) → I.ResidueField)
      ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x,
          Subtype.mk (p := fun (x : R ⧸ I) ↦ Membership.mem (γ := Submonoid (R ⧸ I)) (R ⧸ I)⁰ x)
            ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) s) ⋯).1
⊢ ∃ (x_1 : (R ⧸ I) × ↥(R ⧸ I)⁰),
    HMul.hMul (α := I.ResidueField) (β := I.ResidueField)
        ((IsLocalRing.residue (Localization.AtPrime I) :
              (a : Localization.AtPrime I) → IsLocalRing.ResidueField (Localization.AtPrime I))
            (IsLocalization.mk' (Localization.AtPrime I) x (Subtype.mk (p := fun (x : R) ↦ x ∈ I.primeCompl) s hs)) :
          IsLocalRing.ResidueField (Localization.AtPrime I))
        ((algebraMap (R ⧸ I) I.ResidueField : (a : R ⧸ I) → I.ResidueField) (↑x_1.2 : R ⧸ I) : I.ResidueField) =
      (algebraMap (R ⧸ I) I.ResidueField : (a : R ⧸ I) → I.ResidueField) x_1.1

Tactic:
refine ⟨⟨Ideal.Quotient.mk _ x, ⟨Ideal.Quotient.mk _ s, ?_⟩⟩, ?_⟩
-- 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 s : R
hs : s ∈ I.primeCompl
refine_1 : Ne (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) s : R ⧸ I) (0 : R ⧸ I)
refine_1₁ : ¬Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) s : R ⧸ I) (0 : R ⧸ I)
refine_1₂ refine_1₃ refine_1₄ refine_1₅ : s ∉ I
⊢ Membership.mem (α := R ⧸ I) (γ := Submonoid (R ⧸ I)) (R ⧸ I)⁰ ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) s : R ⧸ I)

Tactic:
rwa [mem_nonZeroDivisors_iff_ne_zero, ne_eq, Ideal.Quotient.eq_zero_iff_mem]

Premises used: ne_eq, Ideal.Quotient.eq_zero_iff_mem, mem_nonZeroDivisors_iff_ne_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 s : R
hs : s ∈ I.primeCompl
⊢ HMul.hMul (α := I.ResidueField) (β := I.ResidueField)
      ((IsLocalRing.residue (Localization.AtPrime I) :
            (a : Localization.AtPrime I) → IsLocalRing.ResidueField (Localization.AtPrime I))
          (IsLocalization.mk' (Localization.AtPrime I) x (Subtype.mk (p := fun (x : R) ↦ x ∈ I.primeCompl) s hs)) :
        IsLocalRing.ResidueField (Localization.AtPrime I))
      ((algebraMap (R ⧸ I) I.ResidueField : (a : R ⧸ I) → I.ResidueField)
          (↑((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x,
                  Subtype.mk (p := fun (x : R ⧸ I) ↦ Membership.mem (γ := Submonoid (R ⧸ I)) (R ⧸ I)⁰ x)
                    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) s) ⋯).2 :
            R ⧸ I) :
        I.ResidueField) =
    (algebraMap (R ⧸ I) I.ResidueField : (a : R ⧸ I) → I.ResidueField)
      ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x,
          Subtype.mk (p := fun (x : R ⧸ I) ↦ Membership.mem (γ := Submonoid (R ⧸ I)) (R ⧸ I)⁰ x)
            ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) s) ⋯).1

Tactic:
simp [IsScalarTower.algebraMap_eq R (Localization.AtPrime I) I.ResidueField, ← map_mul]

Premises used: Localization.AtPrime, Ideal.ResidueField, map_mul, IsScalarTower.algebraMap_eq