awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Fiber (goal)
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)) :=
  ⋯
⊢ Eq (α :=
    (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_4) →
      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 ⋯).symm :
      (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_4)) → PrimeSpectrum (p.asIdeal.Fiber S))
have h : ∀ (x : (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_4)),
  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))
      x =
    ((H.toHomeomorphOfSurjective sorry).symm :
        (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_4)) → PrimeSpectrum (p.asIdeal.Fiber S))
      x
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Fiber (goal)
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 : (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_4)
⊢ 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))
      x =
    ((H.toHomeomorphOfSurjective ⋯).symm :
        (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_4)) → PrimeSpectrum (p.asIdeal.Fiber S))
      x
have h : ∀ (x : PrimeSpectrum (p.asIdeal.Fiber S)),
  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 sorry :
          (a : PrimeSpectrum (p.asIdeal.Fiber S)) → (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_4))
        x))
    (((H.toHomeomorphOfSurjective sorry).symm :
        (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_4)) → PrimeSpectrum (p.asIdeal.Fiber S))
      ((H.toHomeomorphOfSurjective sorry :
          (a : PrimeSpectrum (p.asIdeal.Fiber S)) → (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_4))
        x))
Tactic: obtain ⟨x, rfl⟩ := (H.toHomeomorphOfSurjective
        (preimageOrderIsoFiber R S p).symm.surjective).surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Fiber (goal)
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)
⊢ 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))
have h : (preimageOrderIsoFiber R S p : (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_4)) → PrimeSpectrum (p.asIdeal.Fiber S))
    ((H.toHomeomorphOfSurjective sorry :
        (a : PrimeSpectrum (p.asIdeal.Fiber S)) → (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_4))
      x) =
  x
Tactic: simp only [Equiv.toFun_as_coe, RelIso.coe_fn_toEquiv, Homeomorph.symm_apply_apply]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Ideal (goal)
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.{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)
have 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)
Tactic: simp [IsLocalRing.ResidueField.map_residue, Localization.localRingHom_to_map]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
x : R
⊢ Eq (α := I.ResidueField) ((algebraMap R I.ResidueField : (a : R) → I.ResidueField) x : I.ResidueField)
      (0 : I.ResidueField) ↔
    x ∈ I
have 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
Tactic: rw [IsScalarTower.algebraMap_apply R (Localization.AtPrime I),
    IsLocalRing.ResidueField.algebraMap_eq, IsLocalRing.residue_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := R ⧸ I) (β := I.ResidueField)
    (⇑(algebraMap (R ⧸ I) I.ResidueField) : (a : R ⧸ I) → I.ResidueField)
have rw : Eq (α := Ideal (R ⧸ I)) (RingHom.ker (F := R ⧸ I →+* I.ResidueField) (algebraMap (R ⧸ I) I.ResidueField)) ⊥
Tactic: rw [RingHom.injective_iff_ker_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Ideal (goal)
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)) ⊥
have 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)))
  ⊥
Tactic: refine (Ideal.ker_quotient_lift _ _).trans ?_
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
⊢ 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)))
    ⊥
have change : Eq (α := Ideal (R ⧸ I))
  (map (F := R →+* R ⧸ I) (Quotient.mk I) (RingHom.ker (F := R →+* I.ResidueField) (algebraMap R I.ResidueField))) ⊥
Tactic: change map (Quotient.mk I) (RingHom.ker (algebraMap R I.ResidueField)) = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
⊢ Eq (α := Ideal (R ⧸ I))
    (map (F := R →+* R ⧸ I) (Quotient.mk I) (RingHom.ker (F := R →+* I.ResidueField) (algebraMap R I.ResidueField))) ⊥
have rw : Eq (α := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) I) ⊥
Tactic: rw [Ideal.ker_algebraMap_residueField, map_quotient_self]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Ideal (goal)
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) ⊥
⊢ Eq (α := Ideal (R ⧸ I))
    (map (F := R →+* R ⧸ I) (Quotient.mk I) (RingHom.ker (F := R →+* I.ResidueField) (algebraMap R I.ResidueField))) ⊥
have rw₁ : Eq.{u_1 + 1} (α := Ideal (R ⧸ I)) ⊥ ⊥
Tactic: rw [Ideal.ker_algebraMap_residueField, map_quotient_self]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Ideal (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨x, rfl⟩ := IsLocalRing.residue_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Ideal (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq I.primeCompl x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Ideal (goal)
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
have refine_1 : Membership.mem (α := R ⧸ I) (γ := Submonoid (R ⧸ I)) (R ⧸ I)⁰ ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) s : R ⧸ I)
Tactic: refine ⟨⟨Ideal.Quotient.mk _ x, ⟨Ideal.Quotient.mk _ s, ?_⟩⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Ideal (goal)
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)
⊢ ∃ (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
have 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) sorry).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) sorry).1
Tactic: refine ⟨⟨Ideal.Quotient.mk _ x, ⟨Ideal.Quotient.mk _ s, ?_⟩⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Ideal (goal)
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
⊢ Membership.mem (α := R ⧸ I) (γ := Submonoid (R ⧸ I)) (R ⧸ I)⁰ ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) s : R ⧸ I)
have refine_1 : Ne (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) s : R ⧸ I) (0 : R ⧸ I)
Tactic: rwa [mem_nonZeroDivisors_iff_ne_zero, ne_eq, Ideal.Quotient.eq_zero_iff_mem]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Ideal (goal)
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)
⊢ Membership.mem (α := R ⧸ I) (γ := Submonoid (R ⧸ I)) (R ⧸ I)⁰ ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) s : R ⧸ I)
have refine_1₁ : ¬Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) s : R ⧸ I) (0 : R ⧸ I)
Tactic: rwa [mem_nonZeroDivisors_iff_ne_zero, ne_eq, Ideal.Quotient.eq_zero_iff_mem]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Ideal (goal)
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)
⊢ Membership.mem (α := R ⧸ I) (γ := Submonoid (R ⧸ I)) (R ⧸ I)⁰ ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) s : R ⧸ I)
have refine_1₂ : s ∉ I
Tactic: rwa [mem_nonZeroDivisors_iff_ne_zero, ne_eq, Ideal.Quotient.eq_zero_iff_mem]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Ideal (goal)
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)
⊢ ∃ (c : ↥(R ⧸ I)⁰), (↑c : R ⧸ I) * x = (↑c : R ⧸ I) * y
have 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
Tactic: obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
Cleared hypotheses: x, e
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Ideal (goal)
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)
⊢ ∃ (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
have 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)
Tactic: obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective y
Cleared hypotheses: y, e
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Ideal (hypothesis)
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)
⊢ ∃ (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)
have 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)
Tactic: rw [← sub_eq_zero, ← map_sub, ← map_sub] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Ideal (hypothesis)
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)
⊢ ∃ (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)
have 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)
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
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Ideal (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: use 1
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsMaximal
⊢ Function.Surjective (α := R) (β := I.ResidueField) (⇑(algebraMap R I.ResidueField) : (a : R) → I.ResidueField)
have 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)
Tactic: rw [IsScalarTower.algebraMap_eq R (R ⧸ I) _]