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_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)
h₂ :
  Function.Surjective.{v + 1, u_1 + 1} (α := Away (M := S) ((algebraMap R S : (a : R) → S) r : S)) (β :=
    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)) :
      (a : Away ((algebraMap R S : (a : R) → S) r)) → Away ((algebraMap R T : (a : R) → T) r))
e_2 : Away (M := T) ((Algebra.ofId R T : (a : R) → T) r : T) = Away (M := T) ((algebraMap R T : (a : R) → T) r : T)
e_4 :
  HEq.{u_1 + 1} (α := Ring (Away (M := T) ((Algebra.ofId R T : (a : R) → T) r : T))) CommRing.toRing (β :=
    Ring (Away (M := T) ((algebraMap R T : (a : R) → T) r : T))) CommRing.toRing
⊢ Eq (α := RingHom.{u, u_1} (Away r) (Away (M := T) ((Algebra.ofId R T : (a : R) → T) r : T)))
    (AlgHom.toRingHom (awayMapₐ (Algebra.ofId R T) r))
    (RingHom.comp (β := Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
      (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))
      (awayMap (algebraMap R S) r))

Tactic:
IsLocalization.ringHom_ext (.powers r) (RingHom.ext fun x ↦ ?_)

Premises used: RingHom.ext, Submonoid.powers, IsLocalization.ringHom_ext
-- 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}))ᶜ
algInst : Algebra.{u, u_1} (Away r) (Away (M := T) ((Algebra.ofId R T : (a : R) → T) r : T)) :=
  RingHom.toAlgebra (AlgHom.toRingHom (awayMapₐ (Algebra.ofId R T) r))
⊢ IsScalarTower.{u, u, u_1} R (Away r) (Away (M := T) ((Algebra.ofId R T : (a : R) → T) r : T))

Tactic:
have := IsScalarTower.of_algebraMap_eq'
      (Localization.awayMapₐ (Algebra.ofId R T) r).comp_algebraMap.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}))
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}))ᶜ
algInst : Algebra.{u, u_1} (Away r) (Away (M := T) ((Algebra.ofId R T : (a : R) → T) r : T)) :=
  RingHom.toAlgebra (AlgHom.toRingHom (awayMapₐ (Algebra.ofId R T) r))
this : IsScalarTower.{u, u, u_1} R (Away r) (Away (M := T) ((Algebra.ofId R T : (a : R) → T) r : T))
⊢ 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))

Tactic:
RingHom.finiteType_algebraMap.mpr ?_

Premises used: Iff.mpr, RingHom.finiteType_algebraMap
-- 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}))ᶜ
algInst : Algebra.{u, u_1} (Away r) (Away (M := T) ((Algebra.ofId R T : (a : R) → T) r : T)) :=
  RingHom.toAlgebra (AlgHom.toRingHom (awayMapₐ (Algebra.ofId R T) r))
this : IsScalarTower.{u, u, u_1} R (Away r) (Away (M := T) ((Algebra.ofId R T : (a : R) → T) r : T))
refine_2 : Algebra.FiniteType.{u, u_1} (Away r) (Away (M := T) ((Algebra.ofId R T : (a : R) → T) r : T))
⊢ 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))

Tactic:
refine RingHom.finiteType_algebraMap.mpr ?_

Premises used: Iff.mpr, RingHom.finiteType_algebraMap
-- 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}))ᶜ
algInst : Algebra.{u, u_1} (Away r) (Away (M := T) ((Algebra.ofId R T : (a : R) → T) r : T)) :=
  RingHom.toAlgebra (AlgHom.toRingHom (awayMapₐ (Algebra.ofId R T) r))
this : IsScalarTower.{u, u, u_1} R (Away r) (Away (M := T) ((Algebra.ofId R T : (a : R) → T) r : T))
⊢ Algebra.FiniteType.{u, u_1} (Away r) (Away (M := T) ((Algebra.ofId R T : (a : R) → T) r : T))

Tactic:
.of_restrictScalars_finiteType R _ _

Premises used: Algebra.FiniteType.of_restrictScalars_finiteType
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
inst_5 : q.LiesOver p
inst_6 : FiniteType R S
inst_7 : QuasiFiniteAt R q
obtain :
  ∀ (s₁ : S) (hs₁q : s₁ ∉ q) (hs₁ : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s₁ ∈ q'),
    ∃ s ∉ q,
      ∃ (hs : IsIntegral R s),
        (∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q') ∧
          ∀ (q' : Ideal ↥(integralClosure R S)),
            q'.IsPrime →
              q' ≠ Ideal.under (↥(integralClosure R S)) q →
                q'.LiesOver p →
                  Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hs ∈ q'
⊢ ∃ s ∉ q,
    ∃ (hs : IsIntegral R s),
      (∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q') ∧
        ∀ (q' : Ideal ↥(integralClosure R S)),
          q'.IsPrime →
            q' ≠ Ideal.under (↥(integralClosure R S)) q →
              q'.LiesOver p →
                Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hs ∈ q'

Tactic:
obtain ⟨s₁, hs₁q, hs₁⟩ := Ideal.exists_not_mem_forall_mem_of_ne_of_liesOver (R := R) p q

Premises used: Ideal.exists_not_mem_forall_mem_of_ne_of_liesOver
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
inst_5 : q.LiesOver p
inst_6 : FiniteType R S
inst_7 : QuasiFiniteAt R q
s₁ : S
hs₁q : s₁ ∉ q
hs₁ : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s₁ ∈ q'
obtain :
  ∀ (s₂ : ↥(integralClosure R S)) (hs₂q : (↑s₂ : S) ∉ q)
    (hs₂ :
      Function.Bijective (α := Localization.Away s₂) (β :=
        Localization.Away (M := S)
          ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
        (⇑(Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (integralClosure R S))) s₂) :
          (a : Localization.Away s₂) →
            Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) s₂))),
    ∃ s ∉ q,
      ∃ (hs : IsIntegral R s),
        (∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q') ∧
          ∀ (q' : Ideal ↥(integralClosure R S)),
            q'.IsPrime →
              q' ≠ Ideal.under (↥(integralClosure R S)) q →
                q'.LiesOver p →
                  Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hs ∈ q'
⊢ ∃ s ∉ q,
    ∃ (hs : IsIntegral R s),
      (∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q') ∧
        ∀ (q' : Ideal ↥(integralClosure R S)),
          q'.IsPrime →
            q' ≠ Ideal.under (↥(integralClosure R S)) q →
              q'.LiesOver p →
                Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hs ∈ q'

Tactic:
obtain ⟨s₂, hs₂q, hs₂⟩ := Algebra.ZariskisMainProperty.of_finiteType (R := R) q

Premises used: Algebra.ZariskisMainProperty.of_finiteType
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
inst_5 : q.LiesOver p
inst_6 : FiniteType R S
inst_7 : QuasiFiniteAt R q
s₁ : S
hs₁q : s₁ ∉ q
hs₁ : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s₁ ∈ q'
s₂ : ↥(integralClosure R S)
hs₂q : (↑s₂ : S) ∉ q
hs₂ :
  Function.Bijective (α := Localization.Away s₂) (β :=
    Localization.Away (M := S)
      ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
    (⇑(Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (integralClosure R S))) s₂) :
      (a : Localization.Away s₂) →
        Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) s₂))
obtain :
  ∀ (s₃ : Localization.Away s₂)
    (hs₃ :
      Eq (α :=
        Localization.Away (M := S)
          ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
        ((Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (integralClosure R S))) s₂ :
              (a : Localization.Away s₂) →
                Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) s₂))
            s₃ :
          Localization.Away (M := S)
            ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
        ((algebraMap S
                (Localization.Away (M := S)
                  ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ :
                    S)) :
              (a : S) → Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) s₂))
            s₁ :
          Localization.Away (M := S)
            ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))),
    ∃ s ∉ q,
      ∃ (hs : IsIntegral R s),
        (∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q') ∧
          ∀ (q' : Ideal ↥(integralClosure R S)),
            q'.IsPrime →
              q' ≠ Ideal.under (↥(integralClosure R S)) q →
                q'.LiesOver p →
                  Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hs ∈ q'
⊢ ∃ s ∉ q,
    ∃ (hs : IsIntegral R s),
      (∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q') ∧
        ∀ (q' : Ideal ↥(integralClosure R S)),
          q'.IsPrime →
            q' ≠ Ideal.under (↥(integralClosure R S)) q →
              q'.LiesOver p →
                Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hs ∈ q'

Tactic:
obtain ⟨s₃, hs₃⟩ := hs₂.2 (algebraMap _ _ s₁)

Premises used: Algebra.algebraMap, And.right, DFunLike.coe
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
inst_5 : q.LiesOver p
inst_6 : FiniteType R S
inst_7 : QuasiFiniteAt R q
s₁ : S
hs₁q : s₁ ∉ q
hs₁ : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s₁ ∈ q'
s₂ : ↥(integralClosure R S)
hs₂q : (↑s₂ : S) ∉ q
hs₂ :
  Function.Bijective (α := Localization.Away s₂) (β :=
    Localization.Away (M := S)
      ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
    (⇑(Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (integralClosure R S))) s₂) :
      (a : Localization.Away s₂) →
        Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) s₂))
s₃ : ↥(integralClosure R S)
n : ℕ
hs₃ :
  Eq (α :=
    Localization.Away (M := S)
      ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
    ((Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (integralClosure R S))) s₂ :
          (a : Localization.Away s₂) →
            Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) s₂))
        (IsLocalization.mk' (Localization.Away s₂) s₃
          (Subtype.mk (p := fun (x : ↥(integralClosure R S)) ↦
            Membership.mem (γ := Submonoid ↥(integralClosure R S)) (Submonoid.powers s₂) x) ((fun (x : ℕ) ↦ s₂ ^ x) n)
            ⋯)) :
      Localization.Away (M := S)
        ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
    ((algebraMap S
            (Localization.Away (M := S)
              ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S)) :
          (a : S) → Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) s₂))
        s₁ :
      Localization.Away (M := S)
        ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
⊢ ∃ (m : ℕ), (↑s₂ : S) ^ m * (↑s₃ : S) = (↑s₂ : S) ^ m * (s₁ * (↑s₂ : S) ^ n)

Tactic:
simpa [IsLocalization.Away.map, IsLocalization.map_mk', IsLocalization.mk'_eq_iff_eq_mul,
      ← map_mul, ← map_pow, IsLocalization.eq_iff_exists (.powers s₂.1),
      Submonoid.mem_powers_iff] using hs₃

Premises used: IsLocalization.map_mk', map_pow, IsLocalization.mk'_eq_iff_eq_mul, map_mul, IsLocalization.Away.map, Submonoid.powers, Submonoid.mem_powers_iff, Subtype.val, IsLocalization.eq_iff_exists
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
inst_5 : q.LiesOver p
inst_6 : FiniteType R S
inst_7 : QuasiFiniteAt R q
s₁ : S
hs₁q : s₁ ∉ q
hs₁ : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s₁ ∈ q'
s₂ : ↥(integralClosure R S)
hs₂q : (↑s₂ : S) ∉ q
hs₂ :
  Function.Bijective (α := Localization.Away s₂) (β :=
    Localization.Away (M := S)
      ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
    (⇑(Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (integralClosure R S))) s₂) :
      (a : Localization.Away s₂) →
        Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) s₂))
s₃ : ↥(integralClosure R S)
n : ℕ
hs₃ :
  Eq (α :=
    Localization.Away (M := S)
      ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
    ((Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (integralClosure R S))) s₂ :
          (a : Localization.Away s₂) →
            Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) s₂))
        (IsLocalization.mk' (Localization.Away s₂) s₃
          (Subtype.mk (p := fun (x : ↥(integralClosure R S)) ↦
            Membership.mem (γ := Submonoid ↥(integralClosure R S)) (Submonoid.powers s₂) x) ((fun (x : ℕ) ↦ s₂ ^ x) n)
            ⋯)) :
      Localization.Away (M := S)
        ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
    ((algebraMap S
            (Localization.Away (M := S)
              ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S)) :
          (a : S) → Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) s₂))
        s₁ :
      Localization.Away (M := S)
        ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
m : ℕ
hm : (↑s₂ : S) ^ m * (↑s₃ : S) = (↑s₂ : S) ^ m * (s₁ * (↑s₂ : S) ^ n)
this :
  ∀ (m : ℕ) (hm : (↑s₂ : S) ^ m * (↑s₃ : S) = (↑s₂ : S) ^ m * (s₁ * (↑s₂ : S) ^ n)) (hm0 : 0 < m),
    ∃ s ∉ q,
      ∃ (hs : IsIntegral R s),
        (∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q') ∧
          ∀ (q' : Ideal ↥(integralClosure R S)),
            q'.IsPrime →
              q' ≠ Ideal.under (↥(integralClosure R S)) q →
                q'.LiesOver p →
                  Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hs ∈ q'
hm0 : ¬0 < m
⊢ (↑s₂ : S) ^ (m + 1) * (↑s₃ : S) = (↑s₂ : S) ^ (m + 1) * (s₁ * (↑s₂ : S) ^ n)

Tactic:
grind
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
inst_5 : q.LiesOver p
inst_6 : FiniteType R S
inst_7 : QuasiFiniteAt R q
s₁ : S
hs₁q : s₁ ∉ q
hs₁ : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s₁ ∈ q'
s₂ : ↥(integralClosure R S)
hs₂q : (↑s₂ : S) ∉ q
hs₂ :
  Function.Bijective (α := Localization.Away s₂) (β :=
    Localization.Away (M := S)
      ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
    (⇑(Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (integralClosure R S))) s₂) :
      (a : Localization.Away s₂) →
        Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) s₂))
s₃ : ↥(integralClosure R S)
n : ℕ
hs₃ :
  Eq (α :=
    Localization.Away (M := S)
      ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
    ((Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (integralClosure R S))) s₂ :
          (a : Localization.Away s₂) →
            Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) s₂))
        (IsLocalization.mk' (Localization.Away s₂) s₃
          (Subtype.mk (p := fun (x : ↥(integralClosure R S)) ↦
            Membership.mem (γ := Submonoid ↥(integralClosure R S)) (Submonoid.powers s₂) x) ((fun (x : ℕ) ↦ s₂ ^ x) n)
            ⋯)) :
      Localization.Away (M := S)
        ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
    ((algebraMap S
            (Localization.Away (M := S)
              ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S)) :
          (a : S) → Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) s₂))
        s₁ :
      Localization.Away (M := S)
        ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
m : ℕ
hm : (↑s₂ : S) ^ m * (↑s₃ : S) = (↑s₂ : S) ^ m * (s₁ * (↑s₂ : S) ^ n)
this :
  ∀ (m : ℕ) (hm : (↑s₂ : S) ^ m * (↑s₃ : S) = (↑s₂ : S) ^ m * (s₁ * (↑s₂ : S) ^ n)) (hm0 : 0 < m),
    ∃ s ∉ q,
      ∃ (hs : IsIntegral R s),
        (∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q') ∧
          ∀ (q' : Ideal ↥(integralClosure R S)),
            q'.IsPrime →
              q' ≠ Ideal.under (↥(integralClosure R S)) q →
                q'.LiesOver p →
                  Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hs ∈ q'
hm0 : ¬0 < m
⊢ 0 < m + 1

Tactic:
simp