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₁ 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
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
⊢ 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

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₁ 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₂)
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₁)
⊢ 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:
rw [← Ideal.IsPrime.mul_mem_left_iff (x := algebraMap _ _ r), ← Algebra.smul_def, e] at hx ⊢

Premises used: Algebra.smul_def, Ideal.IsPrime.mul_mem_left_iff
-- 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)
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
⊢ s ∈ (↑q₁ : PrimeSpectrum S).asIdeal

Tactic:
simpa using hx
-- 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)
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
⊢ s ∈ (↑q₁ : PrimeSpectrum S).asIdeal

Tactic:
replace hx : s ∈ q₁.1.asIdeal := by simpa using hx
-- 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)
H : q₁ ≤ q₂
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
hx : s ∈ (↑q₁ : PrimeSpectrum S).asIdeal
⊢ 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:
simpa using H hx
-- 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)
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
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₂)
⊢ ((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

Premises used: Subtype.property
-- 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)
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 ∉ 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:
simpa [IsScalarTower.algebraMap_apply R S q₂.1.asIdeal.ResidueField]

Premises used: Ideal.ResidueField, Subtype.val, IsScalarTower.algebraMap_apply, PrimeSpectrum.asIdeal
-- 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)
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 ∉ 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₁)
⊢ ((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

Premises used: Subtype.property
-- 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)
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 ∉ 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:
simpa [IsScalarTower.algebraMap_apply R S q₁.1.asIdeal.ResidueField]

Premises used: Ideal.ResidueField, Subtype.val, IsScalarTower.algebraMap_apply, PrimeSpectrum.asIdeal
-- 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
⊢ 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))

Tactic:
(Topology.IsEmbedding.of_comp_iff .subtypeVal).mp ?_

Premises used: Iff.mp, Topology.IsEmbedding.of_comp_iff, Topology.IsEmbedding.subtypeVal
-- 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
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)))
⊢ 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))

Tactic:
refine (Topology.IsEmbedding.of_comp_iff .subtypeVal).mp ?_

Premises used: Iff.mp, Topology.IsEmbedding.of_comp_iff, Topology.IsEmbedding.subtypeVal
-- 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
⊢ 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)
-- 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
this :
  Topology.IsEmbedding (X := PrimeSpectrum (S ⊗[R] p.asIdeal.ResidueField)) (tensorProductTo R S p.asIdeal.ResidueField)
⊢ 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:
((Homeomorph.prodUnique _ _).isEmbedding.comp this).comp
      (homeomorphOfRingEquiv (Algebra.TensorProduct.comm _ _ _).toRingEquiv).isEmbedding

Premises used: Homeomorph.prodUnique, Homeomorph.isEmbedding, Quotient.liftOn', Set.Mem, AddCon.liftOn, setOf, List.foldl, Topology.IsEmbedding.comp, IsLocalRing.ResidueField, Quotient, Set.preimage, Ideal.comap, PrimeSpectrum.homeomorphOfRingEquiv, TensorProduct.tmul, PrimeSpectrum.comap, AddCon.toQuotient, FreeAddMonoid.sumAux
-- 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
this :
  Topology.IsEmbedding (X := PrimeSpectrum (S ⊗[R] p.asIdeal.ResidueField)) (tensorProductTo R S p.asIdeal.ResidueField)
⊢ 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:
exact ((Homeomorph.prodUnique _ _).isEmbedding.comp this).comp
      (homeomorphOfRingEquiv (Algebra.TensorProduct.comm _ _ _).toRingEquiv).isEmbedding

Premises used: Homeomorph.prodUnique, Homeomorph.isEmbedding, Topology.IsEmbedding.comp, PrimeSpectrum.homeomorphOfRingEquiv
-- 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)) :=
  ⋯
⊢ Continuous (X := (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_4)) (Y :=
    PrimeSpectrum (p.asIdeal.Fiber S))
    (⇑(H.toHomeomorphOfSurjective ⋯).symm :
      (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_4)) → PrimeSpectrum (p.asIdeal.Fiber S))

Tactic:
(H.toHomeomorphOfSurjective (preimageOrderIsoFiber R S p).symm.surjective).symm.continuous

Premises used: Homeomorph.continuous, OrderIso.surjective, OrderIso.symm, Homeomorph.symm, PrimeSpectrum.preimageOrderIsoFiber, Topology.IsEmbedding.toHomeomorphOfSurjective
-- 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)) :=
  ⋯
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 ⋯).symm :
      (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_4)) → PrimeSpectrum (p.asIdeal.Fiber S))
⊢ 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)))

Tactic:
convert!
        (H.toHomeomorphOfSurjective (preimageOrderIsoFiber R S p).symm.surjective).symm.continuous

Premises used: Homeomorph.continuous, OrderIso.surjective, OrderIso.symm, Homeomorph.symm, PrimeSpectrum.preimageOrderIsoFiber, Topology.IsEmbedding.toHomeomorphOfSurjective
-- 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)) :=
  ⋯
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 ⋯).symm :
          (a : (↑(comap (algebraMap R S) ⁻¹' {p}) : Type u_4)) → PrimeSpectrum (p.asIdeal.Fiber S))
        x
⊢ 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))

Tactic:
ext1 x
-- 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 : (↑(Set.preimage (β := PrimeSpectrum R) (comap (algebraMap R S)) {p}) : Type u_4)
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 ⋯ :
            (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))
⊢ 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

Tactic:
obtain ⟨x, rfl⟩ := (H.toHomeomorphOfSurjective
        (preimageOrderIsoFiber R S p).symm.surjective).surjective x

Premises used: OrderIso.surjective, OrderIso.symm, PrimeSpectrum.preimageOrderIsoFiber, Homeomorph.surjective, Topology.IsEmbedding.toHomeomorphOfSurjective, rfl