awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p_1 : Ideal R
inst_3 : p_1.IsPrime
p : PrimeSpectrum R
q : (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_2)
a :
  ∀ (x : S),
    Membership.mem (γ := Ideal S)
        (asIdeal
          (↑((fun (q : PrimeSpectrum (p.asIdeal.Fiber S)) ↦
                  Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
                    Membership.mem (γ := Set (PrimeSpectrum S))
                      (Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) x)
                    (comap (AlgHom.toRingHom includeRight) q) ⋯)
                ((fun (q : (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_2)) ↦
                    {
                      asIdeal :=
                        RingHom.ker (F := p.asIdeal.ResidueField ⊗[R] S →+* (↑q : PrimeSpectrum S).asIdeal.ResidueField)
                          (AlgHom.toRingHom
                            (Algebra.TensorProduct.lift
                                (Ideal.ResidueField.mapₐ p.asIdeal (↑q : PrimeSpectrum S).asIdeal (ofId R S) ⋯)
                                (IsScalarTower.toAlgHom R S (↑q : PrimeSpectrum S).asIdeal.ResidueField) ⋯ :
                              p.asIdeal.ResidueField ⊗[R] S →ₐ[R] (↑q : PrimeSpectrum S).asIdeal.ResidueField)),
                      isPrime := ⋯ : PrimeSpectrum (p.asIdeal.Fiber S) })
                  q)) :
            PrimeSpectrum S))
        x ↔
      x ∈ (↑q : PrimeSpectrum S).asIdeal
⊢ (fun (q : PrimeSpectrum (p.asIdeal.Fiber S)) ↦
        Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
          Membership.mem (γ := Set (PrimeSpectrum S)) (Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p})
            x)
          (comap (AlgHom.toRingHom includeRight) q) ⋯)
      ((fun (q : (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_2)) ↦
          {
            asIdeal :=
              RingHom.ker (F := p.asIdeal.ResidueField ⊗[R] S →+* (↑q : PrimeSpectrum S).asIdeal.ResidueField)
                (AlgHom.toRingHom
                  (Algebra.TensorProduct.lift
                      (Ideal.ResidueField.mapₐ p.asIdeal (↑q : PrimeSpectrum S).asIdeal (ofId R S) ⋯)
                      (IsScalarTower.toAlgHom R S (↑q : PrimeSpectrum S).asIdeal.ResidueField) ⋯ :
                    p.asIdeal.ResidueField ⊗[R] S →ₐ[R] (↑q : PrimeSpectrum S).asIdeal.ResidueField)),
            isPrime := ⋯ : PrimeSpectrum (p.asIdeal.Fiber S) })
        q) =
    q

Tactic:
ext x
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p_1 : Ideal R
inst_3 : p_1.IsPrime
p : PrimeSpectrum R
q : (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_2)
x : S
⊢ Membership.mem (γ := Ideal S)
      (asIdeal
        (↑((fun (q : PrimeSpectrum (p.asIdeal.Fiber S)) ↦
                Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
                  Membership.mem (γ := Set (PrimeSpectrum S))
                    (Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) x)
                  (comap (AlgHom.toRingHom includeRight) q) ⋯)
              ((fun (q : (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_2)) ↦
                  {
                    asIdeal :=
                      RingHom.ker (F := p.asIdeal.ResidueField ⊗[R] S →+* (↑q : PrimeSpectrum S).asIdeal.ResidueField)
                        (AlgHom.toRingHom
                          (Algebra.TensorProduct.lift
                              (Ideal.ResidueField.mapₐ p.asIdeal (↑q : PrimeSpectrum S).asIdeal (ofId R S) ⋯)
                              (IsScalarTower.toAlgHom R S (↑q : PrimeSpectrum S).asIdeal.ResidueField) ⋯ :
                            p.asIdeal.ResidueField ⊗[R] S →ₐ[R] (↑q : PrimeSpectrum S).asIdeal.ResidueField)),
                    isPrime := ⋯ : PrimeSpectrum (p.asIdeal.Fiber S) })
                q)) :
          PrimeSpectrum S))
      x ↔
    x ∈ (↑q : PrimeSpectrum S).asIdeal

Tactic:
simp
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p_1 : Ideal R
inst_3 : p_1.IsPrime
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
asIdeal :
  ∀ (x : p.asIdeal.Fiber S),
    Membership.mem (γ := Ideal (p.asIdeal.Fiber S))
        (PrimeSpectrum.asIdeal
          ((fun (q : (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_2)) ↦
              {
                asIdeal :=
                  RingHom.ker (F := p.asIdeal.ResidueField ⊗[R] S →+* (↑q : PrimeSpectrum S).asIdeal.ResidueField)
                    (AlgHom.toRingHom
                      (Algebra.TensorProduct.lift
                          (Ideal.ResidueField.mapₐ p.asIdeal (↑q : PrimeSpectrum S).asIdeal (ofId R S) ⋯)
                          (IsScalarTower.toAlgHom R S (↑q : PrimeSpectrum S).asIdeal.ResidueField) ⋯ :
                        p.asIdeal.ResidueField ⊗[R] S →ₐ[R] (↑q : PrimeSpectrum S).asIdeal.ResidueField)),
                isPrime := ⋯ : PrimeSpectrum (p.asIdeal.Fiber S) })
            ((fun (q : PrimeSpectrum (p.asIdeal.Fiber S)) ↦
                Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
                  Membership.mem (γ := Set (PrimeSpectrum S))
                    (Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) x)
                  (comap (AlgHom.toRingHom includeRight) q) ⋯)
              q)))
        x ↔
      x ∈ q.asIdeal
⊢ (fun (q : (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_2)) ↦
        {
          asIdeal :=
            RingHom.ker (F := p.asIdeal.ResidueField ⊗[R] S →+* (↑q : PrimeSpectrum S).asIdeal.ResidueField)
              (AlgHom.toRingHom
                (Algebra.TensorProduct.lift
                    (Ideal.ResidueField.mapₐ p.asIdeal (↑q : PrimeSpectrum S).asIdeal (ofId R S) ⋯)
                    (IsScalarTower.toAlgHom R S (↑q : PrimeSpectrum S).asIdeal.ResidueField) ⋯ :
                  p.asIdeal.ResidueField ⊗[R] S →ₐ[R] (↑q : PrimeSpectrum S).asIdeal.ResidueField)),
          isPrime := ⋯ : PrimeSpectrum (p.asIdeal.Fiber S) })
      ((fun (q : PrimeSpectrum (p.asIdeal.Fiber S)) ↦
          Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
            Membership.mem (γ := Set (PrimeSpectrum S))
              (Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) x)
            (comap (AlgHom.toRingHom includeRight) q) ⋯)
        q) =
    q

Tactic:
ext x
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p_1 : Ideal R
inst_3 : p_1.IsPrime
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
x : p.asIdeal.Fiber S
asIdeal :
  ∀ (r : R) (hr : r ∉ p.asIdeal) (s : S) (e : r • x = 1 ⊗ₜ[R] s),
    Membership.mem (γ := Ideal (p.asIdeal.Fiber S))
        (PrimeSpectrum.asIdeal
          ((fun (q : (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_2)) ↦
              {
                asIdeal :=
                  RingHom.ker (F := p.asIdeal.ResidueField ⊗[R] S →+* (↑q : PrimeSpectrum S).asIdeal.ResidueField)
                    (AlgHom.toRingHom
                      (Algebra.TensorProduct.lift
                          (Ideal.ResidueField.mapₐ p.asIdeal (↑q : PrimeSpectrum S).asIdeal (ofId R S) ⋯)
                          (IsScalarTower.toAlgHom R S (↑q : PrimeSpectrum S).asIdeal.ResidueField) ⋯ :
                        p.asIdeal.ResidueField ⊗[R] S →ₐ[R] (↑q : PrimeSpectrum S).asIdeal.ResidueField)),
                isPrime := ⋯ : PrimeSpectrum (p.asIdeal.Fiber S) })
            ((fun (q : PrimeSpectrum (p.asIdeal.Fiber S)) ↦
                Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
                  Membership.mem (γ := Set (PrimeSpectrum S))
                    (Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) x)
                  (comap (AlgHom.toRingHom includeRight) q) ⋯)
              q)))
        x ↔
      x ∈ q.asIdeal
⊢ Membership.mem (γ := Ideal (p.asIdeal.Fiber S))
      (PrimeSpectrum.asIdeal
        ((fun (q : (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_2)) ↦
            {
              asIdeal :=
                RingHom.ker (F := p.asIdeal.ResidueField ⊗[R] S →+* (↑q : PrimeSpectrum S).asIdeal.ResidueField)
                  (AlgHom.toRingHom
                    (Algebra.TensorProduct.lift
                        (Ideal.ResidueField.mapₐ p.asIdeal (↑q : PrimeSpectrum S).asIdeal (ofId R S) ⋯)
                        (IsScalarTower.toAlgHom R S (↑q : PrimeSpectrum S).asIdeal.ResidueField) ⋯ :
                      p.asIdeal.ResidueField ⊗[R] S →ₐ[R] (↑q : PrimeSpectrum S).asIdeal.ResidueField)),
              isPrime := ⋯ : PrimeSpectrum (p.asIdeal.Fiber S) })
          ((fun (q : PrimeSpectrum (p.asIdeal.Fiber S)) ↦
              Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
                Membership.mem (γ := Set (PrimeSpectrum S))
                  (Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) x)
                (comap (AlgHom.toRingHom includeRight) q) ⋯)
            q)))
      x ↔
    x ∈ q.asIdeal

Tactic:
obtain ⟨r, hr, s, e⟩ := Ideal.Fiber.exists_smul_eq_one_tmul _ x

Premises used: Ideal.Fiber.exists_smul_eq_one_tmul
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p_1 : Ideal R
inst_3 : p_1.IsPrime
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
⊢ ∀ {R : Type (max u_1 u_2)} [inst : CommSemiring R] (self : PrimeSpectrum R), self.asIdeal.IsPrime

Tactic:
have := @PrimeSpectrum.isPrime
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p_1 : Ideal R
inst_3 : p_1.IsPrime
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
this : ∀ {R : Type (max u_1 u_2)} [inst : CommSemiring R] (self : PrimeSpectrum R), self.asIdeal.IsPrime
⊢ 1 ⊗ₜ[R] s ∈ q.asIdeal ↔
    Membership.mem (γ := Ideal (p.asIdeal.Fiber S))
      (asIdeal
        ((fun (q : (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_2)) ↦
            {
              asIdeal :=
                RingHom.ker (F := p.asIdeal.ResidueField ⊗[R] S →+* (↑q : PrimeSpectrum S).asIdeal.ResidueField)
                  (AlgHom.toRingHom
                    (Algebra.TensorProduct.lift
                        (Ideal.ResidueField.mapₐ p.asIdeal (↑q : PrimeSpectrum S).asIdeal (ofId R S) ⋯)
                        (IsScalarTower.toAlgHom R S (↑q : PrimeSpectrum S).asIdeal.ResidueField) ⋯ :
                      p.asIdeal.ResidueField ⊗[R] S →ₐ[R] (↑q : PrimeSpectrum S).asIdeal.ResidueField)),
              isPrime := ⋯ : PrimeSpectrum (p.asIdeal.Fiber S) })
          ((fun (q : PrimeSpectrum (p.asIdeal.Fiber S)) ↦
              Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
                Membership.mem (γ := Set (PrimeSpectrum S))
                  (Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) x)
                (comap (AlgHom.toRingHom includeRight) q) ⋯)
            q)))
      (1 ⊗ₜ[R] s)

Tactic:
simp
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p_1 : Ideal R
inst_3 : p_1.IsPrime
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
this : ∀ {R : Type (max u_1 u_2)} [inst : CommSemiring R] (self : PrimeSpectrum R), self.asIdeal.IsPrime
asIdeal : r ∉ PrimeSpectrum.asIdeal (comap (algebraMap R (p.asIdeal.Fiber S)) q)
⊢ ((algebraMap R (p.asIdeal.Fiber S) : (a : R) → p.asIdeal.Fiber S) r : p.asIdeal.Fiber S) ∉ q.asIdeal

Tactic:
rw [← Ideal.mem_comap, ← PrimeSpectrum.comap_asIdeal]

Premises used: PrimeSpectrum.comap_asIdeal, Ideal.mem_comap
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p_1 : Ideal R
inst_3 : p_1.IsPrime
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
this : ∀ {R : Type (max u_1 u_2)} [inst : CommSemiring R] (self : PrimeSpectrum R), self.asIdeal.IsPrime
⊢ r ∉ p.asIdeal

Tactic:
hr
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p_1 : Ideal R
inst_3 : p_1.IsPrime
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
this : ∀ {R : Type (max u_1 u_2)} [inst : CommSemiring R] (self : PrimeSpectrum R), self.asIdeal.IsPrime
h : comap (algebraMap R (p.asIdeal.Fiber S)) q = p
⊢ r ∉ asIdeal (comap (algebraMap R (p.asIdeal.Fiber S)) q)

Tactic:
convert! hr
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p_1 : Ideal R
inst_3 : p_1.IsPrime
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
this : ∀ {R : Type (max u_1 u_2)} [inst : CommSemiring R] (self : PrimeSpectrum R), self.asIdeal.IsPrime
⊢ comap (algebraMap R (p.asIdeal.Fiber S)) q = p

Tactic:
(residueField_comap _).le ⟨q.comap (algebraMap _ _), rfl⟩

Premises used: Algebra.algebraMap, Set.Mem, setOf, Eq.le, PrimeSpectrum.residueField_comap, Set.singleton, Exists.intro, PrimeSpectrum.comap, rfl
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p_1 : Ideal R
inst_3 : p_1.IsPrime
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
this : ∀ {R : Type (max u_1 u_2)} [inst : CommSemiring R] (self : PrimeSpectrum R), self.asIdeal.IsPrime
⊢ comap (algebraMap R (p.asIdeal.Fiber S)) q = p

Tactic:
exact (residueField_comap _).le ⟨q.comap (algebraMap _ _), rfl⟩

Premises used: Algebra.algebraMap, Eq.le, PrimeSpectrum.residueField_comap, Exists.intro, PrimeSpectrum.comap, rfl
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p_1 : Ideal R
inst_3 : p_1.IsPrime
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
this : ∀ {R : Type (max u_1 u_2)} [inst : CommSemiring R] (self : PrimeSpectrum R), self.asIdeal.IsPrime
⊢ ((algebraMap R (p.asIdeal.Fiber S) : (a : R) → p.asIdeal.Fiber S) r : p.asIdeal.Fiber S) ∉
    asIdeal
      ((fun (q : (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_2)) ↦
          {
            asIdeal :=
              RingHom.ker (F := p.asIdeal.ResidueField ⊗[R] S →+* (↑q : PrimeSpectrum S).asIdeal.ResidueField)
                (AlgHom.toRingHom
                  (Algebra.TensorProduct.lift
                      (Ideal.ResidueField.mapₐ p.asIdeal (↑q : PrimeSpectrum S).asIdeal (ofId R S) ⋯)
                      (IsScalarTower.toAlgHom R S (↑q : PrimeSpectrum S).asIdeal.ResidueField) ⋯ :
                    p.asIdeal.ResidueField ⊗[R] S →ₐ[R] (↑q : PrimeSpectrum S).asIdeal.ResidueField)),
            isPrime := ⋯ : PrimeSpectrum (p.asIdeal.Fiber S) })
        ((fun (q : PrimeSpectrum (p.asIdeal.Fiber S)) ↦
            Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
              Membership.mem (γ := Set (PrimeSpectrum S))
                (Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) x)
              (comap (AlgHom.toRingHom includeRight) q) ⋯)
          q))

Tactic:
simpa [-Algebra.algebraMap_self, -AlgHom.commutes, -AlgHom.map_algebraMap,
        -Ideal.ResidueField.map_algebraMap]

Premises used: Algebra.algebraMap_self, Ideal.ResidueField.map_algebraMap, AlgHom.commutes, AlgHom.map_algebraMap
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p_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₂
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))
⊢ 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
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p_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 :
  ∀ (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₂
⊢ 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:
obtain ⟨q₁, rfl⟩ := (preimageEquivFiber R S p).symm.surjective q₁

Premises used: PrimeSpectrum.preimageEquivFiber, Equiv.surjective, Equiv.symm, rfl
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p_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)
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))
⊢ 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₂

Premises used: PrimeSpectrum.preimageEquivFiber, Equiv.surjective, Equiv.symm, rfl
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p_1 : Ideal R
inst_3 : p_1.IsPrime
p : PrimeSpectrum R
q₁ 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:
simpa using Ideal.comap_mono

Premises used: Ideal.comap_mono