awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra.FiniteType R T
inst_6 : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg :
  Function.Surjective.{v + 1, u_1 + 1} (α := Away g) (β := Away (M := T) ((f : (a : S) → T) g : T))
    (⇑(awayMapₐ f g) : (a : Away g) → Away ((f : (a : S) → T) g))
p : Ideal R
inst_7 : p.IsPrime
hgp : IsUnit (M := p.Fiber S) (1 ⊗ₜ[R] g)
this :
  IsClosed (X := PrimeSpectrum R)
    (Set.image (α := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.zeroLocus {g}))
q : PrimeSpectrum S
hq : Membership.mem (γ := Set (PrimeSpectrum S)) (PrimeSpectrum.zeroLocus {g}) q
e : PrimeSpectrum.comap (algebraMap R S) q = { asIdeal := p, isPrime := inst_7 : PrimeSpectrum R }
⊢ q.asIdeal.LiesOver p

Tactic:
have : q.asIdeal.LiesOver p := ⟨congr(($e).1).symm⟩
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra.FiniteType R T
inst_6 : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg :
  Function.Surjective.{v + 1, u_1 + 1} (α := Away g) (β := Away (M := T) ((f : (a : S) → T) g : T))
    (⇑(awayMapₐ f g) : (a : Away g) → Away ((f : (a : S) → T) g))
p : Ideal R
inst_7 : p.IsPrime
hgp : IsUnit (M := p.Fiber S) (1 ⊗ₜ[R] g)
this_1 :
  IsClosed (X := PrimeSpectrum R)
    (Set.image (α := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.zeroLocus {g}))
q : PrimeSpectrum S
hq : Membership.mem (γ := Set (PrimeSpectrum S)) (PrimeSpectrum.zeroLocus {g}) q
e : PrimeSpectrum.comap (algebraMap R S) q = { asIdeal := p, isPrime := inst_7 : PrimeSpectrum R }
this : q.asIdeal.LiesOver p
⊢ 1 ⊗ₜ[R] g ∉
    PrimeSpectrum.asIdeal
      ((PrimeSpectrum.preimageEquivFiber R S { asIdeal := p, isPrime := inst_7 } :
          (a : (↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {{ asIdeal := p, isPrime := inst_7 }}) : Type v)) →
            PrimeSpectrum ({ asIdeal := p, isPrime := inst_7 }.asIdeal.Fiber S))
        (Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
          Membership.mem (γ := Set (PrimeSpectrum S))
            (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
              {{ asIdeal := p, isPrime := inst_7 : PrimeSpectrum R }})
            x)
          q e))

Tactic:
have : 1 ⊗ₜ g ∉ (PrimeSpectrum.preimageEquivFiber R S ⟨p, ‹_›⟩ ⟨q, e⟩).asIdeal :=
      fun h ↦ Ideal.IsPrime.ne_top' (Ideal.eq_top_of_isUnit_mem _ h hgp)
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra.FiniteType R T
inst_6 : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg :
  Function.Surjective.{v + 1, u_1 + 1} (α := Away g) (β := Away (M := T) ((f : (a : S) → T) g : T))
    (⇑(awayMapₐ f g) : (a : Away g) → Away ((f : (a : S) → T) g))
p : Ideal R
inst_7 : p.IsPrime
hgp : IsUnit (M := p.Fiber S) (1 ⊗ₜ[R] g)
this_1 :
  IsClosed (X := PrimeSpectrum R)
    (Set.image (α := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.zeroLocus {g}))
q : PrimeSpectrum S
hq : Membership.mem (γ := Set (PrimeSpectrum S)) (PrimeSpectrum.zeroLocus {g}) q
e : PrimeSpectrum.comap (algebraMap R S) q = { asIdeal := p, isPrime := inst_7 : PrimeSpectrum R }
this_2 : q.asIdeal.LiesOver p
this :
  1 ⊗ₜ[R] g ∉
    RingHom.ker (F :=
      { asIdeal := p, isPrime := inst_7 : PrimeSpectrum R }.asIdeal.ResidueField ⊗[R] S →+*
        (↑(Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
                  Membership.mem (γ := Set (PrimeSpectrum S))
                    (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
                      {{ asIdeal := p, isPrime := inst_7 : PrimeSpectrum R }})
                    x)
                  q e) :
              PrimeSpectrum S).asIdeal.ResidueField)
      (AlgHom.toRingHom
        (Algebra.TensorProduct.lift
            (Ideal.ResidueField.mapₐ { asIdeal := p, isPrime := inst_7 }.asIdeal
              (↑(Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
                      Membership.mem (γ := Set (PrimeSpectrum S))
                        (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
                          {{ asIdeal := p, isPrime := inst_7 : PrimeSpectrum R }})
                        x)
                      q e) :
                  PrimeSpectrum S).asIdeal
              (Algebra.ofId R S) ⋯)
            (IsScalarTower.toAlgHom R S
              (↑(Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
                        Membership.mem (γ := Set (PrimeSpectrum S))
                          (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
                            {{ asIdeal := p, isPrime := inst_7 : PrimeSpectrum R }})
                          x)
                        q e) :
                    PrimeSpectrum S).asIdeal.ResidueField)
            ⋯ :
          { asIdeal := p, isPrime := inst_7 : PrimeSpectrum R }.asIdeal.ResidueField ⊗[R] S →ₐ[R]
            (↑(Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
                      Membership.mem (γ := Set (PrimeSpectrum S))
                        (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
                          {{ asIdeal := p, isPrime := inst_7 : PrimeSpectrum R }})
                        x)
                      q e) :
                  PrimeSpectrum S).asIdeal.ResidueField))
⊢ False

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra.FiniteType R T
inst_6 : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg :
  Function.Surjective.{v + 1, u_1 + 1} (α := Away g) (β := Away (M := T) ((f : (a : S) → T) g : T))
    (⇑(awayMapₐ f g) : (a : Away g) → Away ((f : (a : S) → T) g))
p : Ideal R
inst_7 : p.IsPrime
hgp : IsUnit (M := p.Fiber S) (1 ⊗ₜ[R] g)
this :
  IsClosed (X := PrimeSpectrum R)
    (Set.image (α := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.zeroLocus {g}))
obtain :
  ∀ (r : R)
    (hpr :
      { asIdeal := p, isPrime := inst_7 : PrimeSpectrum R } ∈ (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum R)))
    (hrg :
      (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum R)) ⊆
        (Set.image (α := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.zeroLocus {g}))ᶜ),
    ∃ r ∉ p,
      AlgHom.Finite.{u, u, u_1} (R := R) (A := Away r) (B := Away (M := T) ((Algebra.ofId R T : (a : R) → T) r : T))
        (awayMapₐ (Algebra.ofId R T) r)
⊢ ∃ r ∉ p,
    AlgHom.Finite.{u, u, u_1} (R := R) (A := Away r) (B := Away (M := T) ((Algebra.ofId R T : (a : R) → T) r : T))
      (awayMapₐ (Algebra.ofId R T) r)

Tactic:
obtain ⟨_, ⟨_, ⟨r, rfl⟩, rfl⟩, hpr, hrg⟩ := PrimeSpectrum.isBasis_basic_opens
    |>.exists_subset_of_mem_open (a := ⟨p, ‹_›⟩) (ou := this.isOpen_compl) <| by
    rintro ⟨q, hq, e⟩
    have : q.asIdeal.LiesOver p := ⟨congr(($e).1).symm⟩
    have : 1 ⊗ₜ g ∉ (PrimeSpectrum.preimageEquivFiber R S ⟨p, ‹_›⟩ ⟨q, e⟩).asIdeal :=
      fun h ↦ Ideal.IsPrime.ne_top' (Ideal.eq_top_of_isUnit_mem _ h hgp)
    rw [PrimeSpectrum.preimageEquivFiber_apply_asIdeal] at this
    simp_all

Premises used: IsClosed.isOpen_compl, Localization.r, PrimeSpectrum.isBasis_basic_opens, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra.FiniteType R T
inst_6 : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg :
  Function.Surjective.{v + 1, u_1 + 1} (α := Away g) (β := Away (M := T) ((f : (a : S) → T) g : T))
    (⇑(awayMapₐ f g) : (a : Away g) → Away ((f : (a : S) → T) g))
p : Ideal R
inst_7 : p.IsPrime
hgp : IsUnit (M := p.Fiber S) (1 ⊗ₜ[R] g)
this :
  IsClosed (X := PrimeSpectrum R)
    (Set.image (α := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.zeroLocus {g}))
r : R
hpr : { asIdeal := p, isPrime := inst_7 : PrimeSpectrum R } ∈ (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum R))
hrg :
  (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum R)) ⊆
    (Set.image (α := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.zeroLocus {g}))ᶜ
⊢ ∃ r ∉ p,
    AlgHom.Finite.{u, u, u_1} (R := R) (A := Away r) (B := Away (M := T) ((Algebra.ofId R T : (a : R) → T) r : T))
      (awayMapₐ (Algebra.ofId R T) r)

Tactic:
⟨r, hpr, RingHom.finite_iff_isIntegral_and_finiteType.mpr ⟨?_, ?_⟩⟩

Premises used: Iff.mpr, And.intro, Exists.intro, RingHom.finite_iff_isIntegral_and_finiteType
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra.FiniteType R T
inst_6 : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg :
  Function.Surjective.{v + 1, u_1 + 1} (α := Away g) (β := Away (M := T) ((f : (a : S) → T) g : T))
    (⇑(awayMapₐ f g) : (a : Away g) → Away ((f : (a : S) → T) g))
p : Ideal R
inst_7 : p.IsPrime
hgp : IsUnit (M := p.Fiber S) (1 ⊗ₜ[R] g)
this :
  IsClosed (X := PrimeSpectrum R)
    (Set.image (α := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.zeroLocus {g}))
r : R
hpr : { asIdeal := p, isPrime := inst_7 : PrimeSpectrum R } ∈ (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum R))
hrg :
  (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum R)) ⊆
    (Set.image (α := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.zeroLocus {g}))ᶜ
refine_1 :
  RingHom.IsIntegral.{u, u_1} (R := Away r) (A := Away (M := T) ((Algebra.ofId R T : (a : R) → T) r : T))
    (AlgHom.toRingHom (awayMapₐ (Algebra.ofId R T) r))
refine_2 :
  RingHom.FiniteType.{u, u_1} (A := Away r) (B := Away (M := T) ((Algebra.ofId R T : (a : R) → T) r : T))
    (AlgHom.toRingHom (awayMapₐ (Algebra.ofId R T) r))
⊢ ∃ r ∉ p,
    AlgHom.Finite.{u, u, u_1} (R := R) (A := Away r) (B := Away (M := T) ((Algebra.ofId R T : (a : R) → T) r : T))
      (awayMapₐ (Algebra.ofId R T) r)

Tactic:
refine ⟨r, hpr, RingHom.finite_iff_isIntegral_and_finiteType.mpr ⟨?_, ?_⟩⟩
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra.FiniteType R T
inst_6 : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg :
  Function.Surjective.{v + 1, u_1 + 1} (α := Away g) (β := Away (M := T) ((f : (a : S) → T) g : T))
    (⇑(awayMapₐ f g) : (a : Away g) → Away ((f : (a : S) → T) g))
p : Ideal R
inst_7 : p.IsPrime
hgp : IsUnit (M := p.Fiber S) (1 ⊗ₜ[R] g)
this :
  IsClosed (X := PrimeSpectrum R)
    (Set.image (α := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.zeroLocus {g}))
r : R
hpr : { asIdeal := p, isPrime := inst_7 : PrimeSpectrum R } ∈ (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum R))
hrg :
  (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum R)) ⊆
    (Set.image (α := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.zeroLocus {g}))ᶜ
simp :
  IsLocalization.Away.{u_1, u_1} (R := T) ((algebraMap R T : (a : R) → T) r : T)
    (Away (M := T) ((algebraMap R T : (a : R) → T) r : T))
⊢ IsLocalization.Away.{u_1, u_1} (R := T) ((f.toRingHom : (a : S) → T) ((algebraMap R S : (a : R) → S) r : S) : T)
    (Away (M := T) ((algebraMap R T : (a : R) → T) r : T))

Tactic:
simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, AlgHom.commutes]

Premises used: RingHom.coe_coe, AlgHom.toRingHom_eq_coe, AlgHom.commutes
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra.FiniteType R T
inst_6 : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg :
  Function.Surjective.{v + 1, u_1 + 1} (α := Away g) (β := Away (M := T) ((f : (a : S) → T) g : T))
    (⇑(awayMapₐ f g) : (a : Away g) → Away ((f : (a : S) → T) g))
p : Ideal R
inst_7 : p.IsPrime
hgp : IsUnit (M := p.Fiber S) (1 ⊗ₜ[R] g)
this :
  IsClosed (X := PrimeSpectrum R)
    (Set.image (α := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.zeroLocus {g}))
r : R
hpr : { asIdeal := p, isPrime := inst_7 : PrimeSpectrum R } ∈ (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum R))
hrg :
  (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum R)) ⊆
    (Set.image (α := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.zeroLocus {g}))ᶜ
⊢ IsLocalization.Away.{u_1, u_1} (R := T) ((algebraMap R T : (a : R) → T) r : T)
    (Away (M := T) ((algebraMap R T : (a : R) → T) r : T))

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra.FiniteType R T
inst_6 : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg :
  Function.Surjective.{v + 1, u_1 + 1} (α := Away g) (β := Away (M := T) ((f : (a : S) → T) g : T))
    (⇑(awayMapₐ f g) : (a : Away g) → Away ((f : (a : S) → T) g))
p : Ideal R
inst_7 : p.IsPrime
hgp : IsUnit (M := p.Fiber S) (1 ⊗ₜ[R] g)
this :
  IsClosed (X := PrimeSpectrum R)
    (Set.image (α := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.zeroLocus {g}))
r : R
hpr : { asIdeal := p, isPrime := inst_7 : PrimeSpectrum R } ∈ (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum R))
hrg :
  (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum R)) ⊆
    (Set.image (α := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.zeroLocus {g}))ᶜ
⊢ IsLocalization.Away.{u_1, u_1} (R := T) ((f.toRingHom : (a : S) → T) ((algebraMap R S : (a : R) → S) r : S) : T)
    (Away (M := T) ((algebraMap R T : (a : R) → T) r : T))

Tactic:
have : IsLocalization.Away (f.toRingHom (algebraMap R S r))
        (Localization.Away (algebraMap R T r)) := by
      simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, AlgHom.commutes]; infer_instance
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra.FiniteType R T
inst_6 : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg :
  Function.Surjective.{v + 1, u_1 + 1} (α := Away g) (β := Away (M := T) ((f : (a : S) → T) g : T))
    (⇑(awayMapₐ f g) : (a : Away g) → Away ((f : (a : S) → T) g))
p : Ideal R
inst_7 : p.IsPrime
hgp : IsUnit (M := p.Fiber S) (1 ⊗ₜ[R] g)
this_1 :
  IsClosed (X := PrimeSpectrum R)
    (Set.image (α := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.zeroLocus {g}))
r : R
hpr : { asIdeal := p, isPrime := inst_7 : PrimeSpectrum R } ∈ (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum R))
hrg :
  (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum R)) ⊆
    (Set.image (α := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.zeroLocus {g}))ᶜ
this :
  IsLocalization.Away.{u_1, u_1} (R := T) ((f.toRingHom : (a : S) → T) ((algebraMap R S : (a : R) → S) r : S) : T)
    (Away (M := T) ((algebraMap R T : (a : R) → T) r : T))
⊢ RingHom.IsIntegral.{u, v} (R := Away r) (A := Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
    (awayMap (algebraMap R S) r)

Tactic:
have h₁ : (Localization.awayMap (algebraMap R S) r).IsIntegral := isIntegral_localization
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra.FiniteType R T
inst_6 : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg :
  Function.Surjective.{v + 1, u_1 + 1} (α := Away g) (β := Away (M := T) ((f : (a : S) → T) g : T))
    (⇑(awayMapₐ f g) : (a : Away g) → Away ((f : (a : S) → T) g))
p : Ideal R
inst_7 : p.IsPrime
hgp : IsUnit (M := p.Fiber S) (1 ⊗ₜ[R] g)
this_1 :
  IsClosed (X := PrimeSpectrum R)
    (Set.image (α := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.zeroLocus {g}))
r : R
hpr : { asIdeal := p, isPrime := inst_7 : PrimeSpectrum R } ∈ (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum R))
hrg :
  (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum R)) ⊆
    (Set.image (α := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.zeroLocus {g}))ᶜ
this :
  IsLocalization.Away.{u_1, u_1} (R := T) ((f.toRingHom : (a : S) → T) ((algebraMap R S : (a : R) → S) r : S) : T)
    (Away (M := T) ((algebraMap R T : (a : R) → T) r : T))
h₁ :
  RingHom.IsIntegral.{u, v} (R := Away r) (A := Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
    (awayMap (algebraMap R S) r)
x : T
n : ℕ
suffices :
  ∃ (a : S) (k : ℕ) (l : ℕ),
    HMul.hMul (β := T) (HPow.hPow (α := T) ((algebraMap R T : (a : R) → T) r : T) (l + n)) ((f : (a : S) → T) a : T) =
      HPow.hPow (α := T) ((algebraMap R T : (a : R) → T) r : T) (l + k) * x
⊢ ∃ (a : Away (M := S) ((algebraMap R S : (a : R) → S) r : S)),
    Eq (α := Away (M := T) ((algebraMap R T : (a : R) → T) r : T))
      (((IsLocalization.Away.map (Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
                (Away (M := T) ((algebraMap R T : (a : R) → T) r : T)) f.toRingHom ((algebraMap R S : (a : R) → S) r) :
              RingHom.{v, u_1} (Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
                (Away (M := T) ((algebraMap R T : (a : R) → T) r : T))) :
            (a : Away ((algebraMap R S : (a : R) → S) r)) → Away ((algebraMap R T : (a : R) → T) r))
          a :
        Away (M := T) ((algebraMap R T : (a : R) → T) r : T))
      (IsLocalization.mk' (Away (M := T) ((algebraMap R T : (a : R) → T) r : T)) x
          (Subtype.mk (p := fun (x : T) ↦
            Membership.mem (γ := Submonoid T) (Submonoid.powers ((algebraMap R T : (a : R) → T) r) : Submonoid T) x)
            ((fun (x : ℕ) ↦ HPow.hPow (α := T) ((algebraMap R T : (a : R) → T) r : T) x) n) ⋯) :
        Away (M := T) ((algebraMap R T : (a : R) → T) r : T))

Tactic:
suffices ∃ a k l, algebraMap R T r ^ (l + n) * f a =
          algebraMap R T r ^ (l + k) * x by
        simpa [(IsLocalization.mk'_surjective (.powers (algebraMap R S r))).exists,
          IsLocalization.Away.map, IsLocalization.map_mk', IsLocalization.mk'_eq_iff_eq,
          ← map_pow, Submonoid.mem_powers_iff, IsLocalization.Away.map, IsLocalization.map_mk',
          IsLocalization.mk'_eq_iff_eq, ← map_mul, ← mul_assoc, ← pow_add,
          IsLocalization.eq_iff_exists (.powers (algebraMap R T r))]
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra.FiniteType R T
inst_6 : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg :
  Function.Surjective.{v + 1, u_1 + 1} (α := Away g) (β := Away (M := T) ((f : (a : S) → T) g : T))
    (⇑(awayMapₐ f g) : (a : Away g) → Away ((f : (a : S) → T) g))
p : Ideal R
inst_7 : p.IsPrime
hgp : IsUnit (M := p.Fiber S) (1 ⊗ₜ[R] g)
this_1 :
  IsClosed (X := PrimeSpectrum R)
    (Set.image (α := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.zeroLocus {g}))
r : R
hpr : { asIdeal := p, isPrime := inst_7 : PrimeSpectrum R } ∈ (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum R))
hrg :
  (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum R)) ⊆
    (Set.image (α := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.zeroLocus {g}))ᶜ
this :
  IsLocalization.Away.{u_1, u_1} (R := T) ((f.toRingHom : (a : S) → T) ((algebraMap R S : (a : R) → S) r : S) : T)
    (Away (M := T) ((algebraMap R T : (a : R) → T) r : T))
h₁ :
  RingHom.IsIntegral.{u, v} (R := Away r) (A := Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
    (awayMap (algebraMap R S) r)
x : T
n : ℕ
⊢ LE.le.{v} (α := TopologicalSpace.Opens (PrimeSpectrum S))
    (PrimeSpectrum.basicOpen ((algebraMap R S : (a : R) → S) r) : TopologicalSpace.Opens (PrimeSpectrum S))
    (PrimeSpectrum.basicOpen g : TopologicalSpace.Opens (PrimeSpectrum S))

Tactic:
simpa [← SetLike.coe_subset_coe] using hrg

Premises used: SetLike.coe_subset_coe
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra.FiniteType R T
inst_6 : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg :
  Function.Surjective.{v + 1, u_1 + 1} (α := Away g) (β := Away (M := T) ((f : (a : S) → T) g : T))
    (⇑(awayMapₐ f g) : (a : Away g) → Away ((f : (a : S) → T) g))
p : Ideal R
inst_7 : p.IsPrime
hgp : IsUnit (M := p.Fiber S) (1 ⊗ₜ[R] g)
this_1 :
  IsClosed (X := PrimeSpectrum R)
    (Set.image (α := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.zeroLocus {g}))
r : R
hpr : { asIdeal := p, isPrime := inst_7 : PrimeSpectrum R } ∈ (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum R))
hrg :
  (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum R)) ⊆
    (Set.image (α := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.zeroLocus {g}))ᶜ
this :
  IsLocalization.Away.{u_1, u_1} (R := T) ((f.toRingHom : (a : S) → T) ((algebraMap R S : (a : R) → S) r : S) : T)
    (Away (M := T) ((algebraMap R T : (a : R) → T) r : T))
h₁ :
  RingHom.IsIntegral.{u, v} (R := Away r) (A := Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
    (awayMap (algebraMap R S) r)
x : T
n : ℕ
⊢ LE.le.{v} (α := TopologicalSpace.Opens (PrimeSpectrum S))
    (PrimeSpectrum.basicOpen ((algebraMap R S : (a : R) → S) r) : TopologicalSpace.Opens (PrimeSpectrum S))
    (PrimeSpectrum.basicOpen g : TopologicalSpace.Opens (PrimeSpectrum S))

Tactic:
have : PrimeSpectrum.basicOpen (algebraMap R S r) ≤ PrimeSpectrum.basicOpen g := by
        simpa [← SetLike.coe_subset_coe] using hrg
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra.FiniteType R T
inst_6 : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg :
  Function.Surjective.{v + 1, u_1 + 1} (α := Away g) (β := Away (M := T) ((f : (a : S) → T) g : T))
    (⇑(awayMapₐ f g) : (a : Away g) → Away ((f : (a : S) → T) g))
p : Ideal R
inst_7 : p.IsPrime
hgp : IsUnit (M := p.Fiber S) (1 ⊗ₜ[R] g)
this_1 :
  IsClosed (X := PrimeSpectrum R)
    (Set.image (α := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.zeroLocus {g}))
r : R
hpr : { asIdeal := p, isPrime := inst_7 : PrimeSpectrum R } ∈ (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum R))
hrg :
  (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum R)) ⊆
    (Set.image (α := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.zeroLocus {g}))ᶜ
this_2 :
  IsLocalization.Away.{u_1, u_1} (R := T) ((f.toRingHom : (a : S) → T) ((algebraMap R S : (a : R) → S) r : S) : T)
    (Away (M := T) ((algebraMap R T : (a : R) → T) r : T))
h₁ :
  RingHom.IsIntegral.{u, v} (R := Away r) (A := Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
    (awayMap (algebraMap R S) r)
x : T
n : ℕ
this :
  LE.le.{v} (α := TopologicalSpace.Opens (PrimeSpectrum S))
    (PrimeSpectrum.basicOpen ((algebraMap R S : (a : R) → S) r) : TopologicalSpace.Opens (PrimeSpectrum S))
    (PrimeSpectrum.basicOpen g : TopologicalSpace.Opens (PrimeSpectrum S))
⊢ ∃ (n : ℕ), g ∣ HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n

Tactic:
simp only [PrimeSpectrum.basicOpen_le_basicOpen_iff, Ideal.mem_radical_iff,
        Ideal.mem_span_singleton] at this

Premises used: PrimeSpectrum.basicOpen_le_basicOpen_iff, Ideal.mem_radical_iff, Ideal.mem_span_singleton