awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Fiber (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p_1 : Ideal R
inst_3 : p_1.IsPrime
p : PrimeSpectrum R
q₁ q₂ : (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_2)
⊢ LE.le (α := PrimeSpectrum (p.asIdeal.Fiber S))
      ((preimageEquivFiber R S p :
            (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
          q₁ :
        PrimeSpectrum (p.asIdeal.Fiber S))
      ((preimageEquivFiber R S p :
            (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
          q₂ :
        PrimeSpectrum (p.asIdeal.Fiber S)) ↔
    q₁ ≤ q₂
have mp : LE.le (α := PrimeSpectrum (p.asIdeal.Fiber S))
    ((preimageEquivFiber R S p :
          (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
        q₁ :
      PrimeSpectrum (p.asIdeal.Fiber S))
    ((preimageEquivFiber R S p :
          (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
        q₂ :
      PrimeSpectrum (p.asIdeal.Fiber S)) →
  q₁ ≤ q₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Fiber (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p_1 : Ideal R
inst_3 : p_1.IsPrime
p : PrimeSpectrum R
q₁ q₂ : (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_2)
mp :
  LE.le (α := PrimeSpectrum (p.asIdeal.Fiber S))
      ((preimageEquivFiber R S p :
            (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
          q₁ :
        PrimeSpectrum (p.asIdeal.Fiber S))
      ((preimageEquivFiber R S p :
            (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
          q₂ :
        PrimeSpectrum (p.asIdeal.Fiber S)) →
    q₁ ≤ q₂
⊢ LE.le (α := PrimeSpectrum (p.asIdeal.Fiber S))
      ((preimageEquivFiber R S p :
            (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
          q₁ :
        PrimeSpectrum (p.asIdeal.Fiber S))
      ((preimageEquivFiber R S p :
            (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
          q₂ :
        PrimeSpectrum (p.asIdeal.Fiber S)) ↔
    q₁ ≤ q₂
have mpr : q₁ ≤ q₂ →
  LE.le (α := PrimeSpectrum (p.asIdeal.Fiber S))
    ((preimageEquivFiber R S p :
          (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
        q₁ :
      PrimeSpectrum (p.asIdeal.Fiber S))
    ((preimageEquivFiber R S p :
          (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
        q₂ :
      PrimeSpectrum (p.asIdeal.Fiber S))
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Fiber (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p_1 : Ideal R
inst_3 : p_1.IsPrime
p : PrimeSpectrum R
q₁ q₂ : (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_2)
⊢ LE.le (α := PrimeSpectrum (p.asIdeal.Fiber S))
      ((preimageEquivFiber R S p :
            (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
          q₁ :
        PrimeSpectrum (p.asIdeal.Fiber S))
      ((preimageEquivFiber R S p :
            (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
          q₂ :
        PrimeSpectrum (p.asIdeal.Fiber S)) →
    q₁ ≤ q₂
have mp : ∀ (q₁ : PrimeSpectrum (p.asIdeal.Fiber S)),
  LE.le (α := PrimeSpectrum (p.asIdeal.Fiber S))
      ((preimageEquivFiber R S p :
            (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
          ((Equiv.symm (preimageEquivFiber R S p) :
              (a : PrimeSpectrum (p.asIdeal.Fiber S)) → (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2))
            q₁) :
        PrimeSpectrum (p.asIdeal.Fiber S))
      ((preimageEquivFiber R S p :
            (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
          q₂ :
        PrimeSpectrum (p.asIdeal.Fiber S)) →
    (Equiv.symm (preimageEquivFiber R S p) :
          (a : PrimeSpectrum (p.asIdeal.Fiber S)) → (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2))
        q₁ ≤
      q₂
Tactic: obtain ⟨q₁, rfl⟩ := (preimageEquivFiber R S p).symm.surjective q₁
Cleared hypotheses: q₁
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Fiber (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p_1 : Ideal R
inst_3 : p_1.IsPrime
p : PrimeSpectrum R
q₂ : (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_2)
q₁ : PrimeSpectrum (p.asIdeal.Fiber S)
⊢ LE.le (α := PrimeSpectrum (p.asIdeal.Fiber S))
      ((preimageEquivFiber R S p :
            (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
          ((Equiv.symm (preimageEquivFiber R S p) :
              (a : PrimeSpectrum (p.asIdeal.Fiber S)) → (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2))
            q₁) :
        PrimeSpectrum (p.asIdeal.Fiber S))
      ((preimageEquivFiber R S p :
            (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
          q₂ :
        PrimeSpectrum (p.asIdeal.Fiber S)) →
    (Equiv.symm (preimageEquivFiber R S p) :
          (a : PrimeSpectrum (p.asIdeal.Fiber S)) → (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2))
        q₁ ≤
      q₂
have mp : ∀ (q₂ : PrimeSpectrum (p.asIdeal.Fiber S)),
  LE.le (α := PrimeSpectrum (p.asIdeal.Fiber S))
      ((preimageEquivFiber R S p :
            (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
          ((Equiv.symm (preimageEquivFiber R S p) :
              (a : PrimeSpectrum (p.asIdeal.Fiber S)) → (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2))
            q₁) :
        PrimeSpectrum (p.asIdeal.Fiber S))
      ((preimageEquivFiber R S p :
            (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
          ((Equiv.symm (preimageEquivFiber R S p) :
              (a : PrimeSpectrum (p.asIdeal.Fiber S)) → (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2))
            q₂) :
        PrimeSpectrum (p.asIdeal.Fiber S)) →
    LE.le.{u_2} (α := (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_2))
      ((Equiv.symm (preimageEquivFiber R S p) :
            (a : PrimeSpectrum (p.asIdeal.Fiber S)) → (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2))
          q₁ :
        (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_2))
      ((Equiv.symm (preimageEquivFiber R S p) :
            (a : PrimeSpectrum (p.asIdeal.Fiber S)) → (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2))
          q₂ :
        (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_2))
Tactic: obtain ⟨q₂, rfl⟩ := (preimageEquivFiber R S p).symm.surjective q₂
Cleared hypotheses: q₂
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Fiber (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p_1 : Ideal R
inst_3 : p_1.IsPrime
p : PrimeSpectrum R
q₁ q₂ : (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_2)
H : q₁ ≤ q₂
x : p.asIdeal.Fiber S
hx :
  Membership.mem (γ := Submodule (p.asIdeal.Fiber S) (p.asIdeal.Fiber S))
    (asIdeal
      ((preimageEquivFiber R S p :
          (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
        q₁))
    x
⊢ Membership.mem (γ := Submodule (p.asIdeal.Fiber S) (p.asIdeal.Fiber S))
    (asIdeal
      ((preimageEquivFiber R S p :
          (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
        q₂))
    x
have mpr : ∀ (r : R) (hr : r ∉ p.asIdeal) (s : S) (e : r • x = 1 ⊗ₜ[R] s),
  Membership.mem (γ := Submodule (p.asIdeal.Fiber S) (p.asIdeal.Fiber S))
    (asIdeal
      ((preimageEquivFiber R S p :
          (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
        q₂))
    x
Tactic: obtain ⟨r, hr, s, e⟩ := Ideal.Fiber.exists_smul_eq_one_tmul _ x
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Fiber (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p_1 : Ideal R
inst_3 : p_1.IsPrime
p : PrimeSpectrum R
q₁ q₂ : (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_2)
H : q₁ ≤ q₂
x : p.asIdeal.Fiber S
hx :
  Membership.mem (γ := Submodule (p.asIdeal.Fiber S) (p.asIdeal.Fiber S))
    (asIdeal
      ((preimageEquivFiber R S p :
          (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
        q₁))
    x
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
⊢ Membership.mem (γ := Submodule (p.asIdeal.Fiber S) (p.asIdeal.Fiber S))
    (asIdeal
      ((preimageEquivFiber R S p :
          (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
        q₂))
    x
have mpr : ∀ (hr : r ∉ p.asIdeal) (s : S)
  (hx :
    Membership.mem (γ := Ideal (p.asIdeal.Fiber S))
      (asIdeal
        ((preimageEquivFiber R S p :
            (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
          q₁))
      (1 ⊗ₜ[R] s))
  (e : r • x = 1 ⊗ₜ[R] s),
  Membership.mem (γ := Ideal (p.asIdeal.Fiber S))
    (asIdeal
      ((preimageEquivFiber R S p :
          (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
        q₂))
    (1 ⊗ₜ[R] s)
Tactic: rw [← Ideal.IsPrime.mul_mem_left_iff (x := algebraMap _ _ r), ← Algebra.smul_def, e] at hx ⊢
Cleared hypotheses: hx, hr, s, e
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Fiber (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p_1 : Ideal R
inst_3 : p_1.IsPrime
p : PrimeSpectrum R
q₁ q₂ : (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_2)
H : q₁ ≤ q₂
x : p.asIdeal.Fiber S
hx :
  Membership.mem (γ := Submodule (p.asIdeal.Fiber S) (p.asIdeal.Fiber S))
    (asIdeal
      ((preimageEquivFiber R S p :
          (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
        q₁))
    x
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
mpr :
  ∀ (hr : r ∉ p.asIdeal) (s : S)
    (hx :
      Membership.mem (γ := Ideal (p.asIdeal.Fiber S))
        (asIdeal
          ((preimageEquivFiber R S p :
              (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
            q₁))
        (1 ⊗ₜ[R] s))
    (e : r • x = 1 ⊗ₜ[R] s),
    Membership.mem (γ := Ideal (p.asIdeal.Fiber S))
      (asIdeal
        ((preimageEquivFiber R S p :
            (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
          q₂))
      (1 ⊗ₜ[R] s)
⊢ Membership.mem (γ := Submodule (p.asIdeal.Fiber S) (p.asIdeal.Fiber S))
    (asIdeal
      ((preimageEquivFiber R S p :
          (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
        q₂))
    x
have mpr₁ : ∀
  (hx :
    Membership.mem (γ := Ideal (p.asIdeal.Fiber S))
      (asIdeal
        ((preimageEquivFiber R S p :
            (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
          q₁))
      (HMul.hMul (α := p.asIdeal.Fiber S)
        ((algebraMap R (p.asIdeal.Fiber S) : (a : R) → p.asIdeal.Fiber S) r : p.asIdeal.Fiber S) x))
  (hr : r ∉ p.asIdeal) (s : S) (e : r • x = 1 ⊗ₜ[R] s),
  ((algebraMap R (p.asIdeal.Fiber S) : (a : R) → p.asIdeal.Fiber S) r : p.asIdeal.Fiber S) ∉
    asIdeal
      ((preimageEquivFiber R S p :
          (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
        q₂)
Tactic: rw [← Ideal.IsPrime.mul_mem_left_iff (x := algebraMap _ _ r), ← Algebra.smul_def, e] at hx ⊢
Cleared hypotheses: hx, hr, s, e
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Fiber (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p_1 : Ideal R
inst_3 : p_1.IsPrime
p : PrimeSpectrum R
q₁ q₂ : (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_2)
H : q₁ ≤ q₂
x : p.asIdeal.Fiber S
hx :
  Membership.mem (γ := Submodule (p.asIdeal.Fiber S) (p.asIdeal.Fiber S))
    (asIdeal
      ((preimageEquivFiber R S p :
          (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
        q₁))
    x
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
mpr :
  ∀ (hr : r ∉ p.asIdeal) (s : S)
    (hx :
      Membership.mem (γ := Ideal (p.asIdeal.Fiber S))
        (asIdeal
          ((preimageEquivFiber R S p :
              (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
            q₁))
        (1 ⊗ₜ[R] s))
    (e : r • x = 1 ⊗ₜ[R] s),
    Membership.mem (γ := Ideal (p.asIdeal.Fiber S))
      (asIdeal
        ((preimageEquivFiber R S p :
            (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
          q₂))
      (1 ⊗ₜ[R] s)
mpr₁ :
  ∀
    (hx :
      Membership.mem (γ := Ideal (p.asIdeal.Fiber S))
        (asIdeal
          ((preimageEquivFiber R S p :
              (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
            q₁))
        (HMul.hMul (α := p.asIdeal.Fiber S)
          ((algebraMap R (p.asIdeal.Fiber S) : (a : R) → p.asIdeal.Fiber S) r : p.asIdeal.Fiber S) x))
    (hr : r ∉ p.asIdeal) (s : S) (e : r • x = 1 ⊗ₜ[R] s),
    ((algebraMap R (p.asIdeal.Fiber S) : (a : R) → p.asIdeal.Fiber S) r : p.asIdeal.Fiber S) ∉
      asIdeal
        ((preimageEquivFiber R S p :
            (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
          q₂)
⊢ Membership.mem (γ := Submodule (p.asIdeal.Fiber S) (p.asIdeal.Fiber S))
    (asIdeal
      ((preimageEquivFiber R S p :
          (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
        q₂))
    x
have mpr₂ : ((algebraMap R (p.asIdeal.Fiber S) : (a : R) → p.asIdeal.Fiber S) r : p.asIdeal.Fiber S) ∉
  asIdeal
    ((preimageEquivFiber R S p :
        (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
      q₁)
Tactic: rw [← Ideal.IsPrime.mul_mem_left_iff (x := algebraMap _ _ r), ← Algebra.smul_def, e] at hx ⊢
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Fiber (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p_1 : Ideal R
inst_3 : p_1.IsPrime
p : PrimeSpectrum R
q₁ q₂ : (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_2)
H : q₁ ≤ q₂
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
hx :
  Membership.mem (γ := Ideal (p.asIdeal.Fiber S))
    (asIdeal
      ((preimageEquivFiber R S p :
          (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
        q₁))
    (1 ⊗ₜ[R] s)
e : r • x = 1 ⊗ₜ[R] s
⊢ Membership.mem (γ := Ideal (p.asIdeal.Fiber S))
    (asIdeal
      ((preimageEquivFiber R S p :
          (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
        q₂))
    (1 ⊗ₜ[R] s)
have hx₁ : s ∈ (↑q₁ : PrimeSpectrum S).asIdeal
Tactic: replace hx : s ∈ q₁.1.asIdeal := by simpa using hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Fiber (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p_1 : Ideal R
inst_3 : p_1.IsPrime
p : PrimeSpectrum R
q₁ q₂ : (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_2)
H : q₁ ≤ q₂
x : p.asIdeal.Fiber S
r : R
hx :
  Membership.mem (γ := Ideal (p.asIdeal.Fiber S))
    (asIdeal
      ((preimageEquivFiber R S p :
          (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
        q₁))
    (HMul.hMul (α := p.asIdeal.Fiber S)
      ((algebraMap R (p.asIdeal.Fiber S) : (a : R) → p.asIdeal.Fiber S) r : p.asIdeal.Fiber S) x)
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
⊢ ((algebraMap R (p.asIdeal.Fiber S) : (a : R) → p.asIdeal.Fiber S) r : p.asIdeal.Fiber S) ∉
    asIdeal
      ((preimageEquivFiber R S p :
          (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
        q₂)
have mpr : ∀ (hr : r ∉ asIdeal (comap (algebraMap R S) (↑q₂ : PrimeSpectrum S))) (s : S) (e : r • x = 1 ⊗ₜ[R] s),
  ((algebraMap R (p.asIdeal.Fiber S) : (a : R) → p.asIdeal.Fiber S) r : p.asIdeal.Fiber S) ∉
    asIdeal
      ((preimageEquivFiber R S p :
          (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
        q₂)
Tactic: rw [← q₂.2] at hr
Cleared hypotheses: hr, s, e
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Fiber (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p_1 : Ideal R
inst_3 : p_1.IsPrime
p : PrimeSpectrum R
q₁ q₂ : (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_2)
H : q₁ ≤ q₂
x : p.asIdeal.Fiber S
hx :
  Membership.mem (γ := Submodule (p.asIdeal.Fiber S) (p.asIdeal.Fiber S))
    (asIdeal
      ((preimageEquivFiber R S p :
          (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
        q₁))
    x
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
⊢ ((algebraMap R (p.asIdeal.Fiber S) : (a : R) → p.asIdeal.Fiber S) r : p.asIdeal.Fiber S) ∉
    asIdeal
      ((preimageEquivFiber R S p :
          (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
        q₁)
have mpr : ∀ (hr : r ∉ asIdeal (comap (algebraMap R S) (↑q₁ : PrimeSpectrum S))) (s : S) (e : r • x = 1 ⊗ₜ[R] s),
  ((algebraMap R (p.asIdeal.Fiber S) : (a : R) → p.asIdeal.Fiber S) r : p.asIdeal.Fiber S) ∉
    asIdeal
      ((preimageEquivFiber R S p :
          (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
        q₁)
Tactic: rw [← q₁.2] at hr
Cleared hypotheses: hr, s, e
-- 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
⊢ 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))
have refine : Topology.IsEmbedding (X := PrimeSpectrum (p.asIdeal.Fiber S)) (Y := PrimeSpectrum S)
  (Function.comp (β :=
    { x : PrimeSpectrum S //
      Membership.mem (γ := Set (PrimeSpectrum S)) (Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p})
        x })
    (Subtype.val (p := fun (x : PrimeSpectrum S) ↦
      Membership.mem (γ := Set (PrimeSpectrum S)) (Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) x))
    (⇑(OrderIso.symm (preimageOrderIsoFiber R S p)) :
      (a : PrimeSpectrum (p.asIdeal.Fiber S)) → (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_4)))
Tactic: refine (Topology.IsEmbedding.of_comp_iff .subtypeVal).mp ?_
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Fiber (hypothesis)
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
⊢ Topology.IsEmbedding (X := PrimeSpectrum (p.asIdeal.Fiber S)) (Y := PrimeSpectrum S)
    (Function.comp (β :=
      { x : PrimeSpectrum S //
        Membership.mem (γ := Set (PrimeSpectrum S)) (Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p})
          x })
      (Subtype.val (p := fun (x : PrimeSpectrum S) ↦
        Membership.mem (γ := Set (PrimeSpectrum S)) (Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p})
          x))
      (⇑(OrderIso.symm (preimageOrderIsoFiber R S p)) :
        (a : PrimeSpectrum (p.asIdeal.Fiber S)) → (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_4)))
have this : Topology.IsEmbedding (X := PrimeSpectrum (S ⊗[R] p.asIdeal.ResidueField)) (tensorProductTo R S p.asIdeal.ResidueField)
Tactic: have := PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks _ S _
      (Ideal.surjectiveOnStalks_residueField p.asIdeal)
-- 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)) :=
  ⋯
⊢ Continuous (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)))
have h : 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 sorry).symm :
    (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_4)) → PrimeSpectrum (p.asIdeal.Fiber S))
Tactic: convert!
        (H.toHomeomorphOfSurjective (preimageOrderIsoFiber R S p).symm.surjective).symm.continuous