awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (hypothesis)
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))
⊢ ∃ (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
have this₁ : ∃ (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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (goal)
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 : ∃ (n : ℕ), g ∣ HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n
⊢ ∃ (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
have obtain : ∀ (m' : ℕ) (s : S) (hs : HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) m' = g * s),
  ∃ (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
Tactic: obtain ⟨m', s, hs⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (goal)
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 m' : ℕ
s : S
hs : HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) m' = g * s
⊢ ∃ (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
have obtain : ∀ (b : S) (m : ℕ) (e : (f : (a : S) → T) b = HPow.hPow (α := T) ((f : (a : S) → T) g : T) m * x),
  ∃ (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
Tactic: obtain ⟨b, m, e : f b = f g ^ m * x⟩ := Localization.awayMap_surjective_iff.mp hg x
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (hypothesis)
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 m' : ℕ
s : S
hs : HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) m' = g * s
b : S
m : ℕ
e : (f : (a : S) → T) b = HPow.hPow (α := T) ((f : (a : S) → T) g : T) m * x
⊢ ∃ (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
have this₁ : (f : (a : S) → T) (s ^ m * b) = HPow.hPow (α := T) ((f : (a : S) → T) (g * s) : T) m * x
Tactic: have : f (s ^ m * b) = f (g * s) ^ m * x := by simp [e, mul_pow, mul_assoc, mul_left_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (hypothesis)
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 m' : ℕ
s : S
hs : HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) m' = g * s
b : S
m : ℕ
e : (f : (a : S) → T) b = HPow.hPow (α := T) ((f : (a : S) → T) g : T) m * x
this : (f : (a : S) → T) (s ^ m * b) = HPow.hPow (α := T) ((f : (a : S) → T) (g * s) : T) m * x
⊢ ∃ (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
have this₁ : (f : (a : S) → T) (s ^ m * b) = HPow.hPow (α := T) ((algebraMap R T : (a : R) → T) r : T) (m' * m) * x
Tactic: simp_rw [← hs, map_pow, AlgHom.commutes, ← pow_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (goal)
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 m' : ℕ
s : S
hs : HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) m' = g * s
b : S
m : ℕ
e : (f : (a : S) → T) b = HPow.hPow (α := T) ((f : (a : S) → T) g : T) m * x
this : (f : (a : S) → T) (s ^ m * b) = HPow.hPow (α := T) ((algebraMap R T : (a : R) → T) r : T) (m' * m) * x
⊢ ∃ (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
have refine : HPow.hPow (α := T) ((algebraMap R T : (a : R) → T) r : T) (0 + n) *
    (HPow.hPow (α := T) ((algebraMap R T : (a : R) → T) r : T) (m' * m) * x) =
  HPow.hPow (α := T) ((algebraMap R T : (a : R) → T) r : T) (0 + (n + m' * m)) * x
Tactic: refine ⟨s ^ m * b, (n + m' * m), 0, this ▸ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (goal)
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))
⊢ 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))
have h : Away (M := T) ((Algebra.ofId R T : (a : R) → T) r : T) = Away (M := T) ((algebraMap R T : (a : R) → T) r : T) →
  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: convert! h₁.trans _ _ (RingHom.IsIntegral.of_finite (.of_surjective _ h₂)) using 1
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (hypothesis)
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))
⊢ 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))
have this₁ : 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
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (goal)
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))
have refine_2 : Algebra.FiniteType.{u, u_1} (Away r) (Away (M := T) ((Algebra.ofId R T : (a : R) → T) r : T))
Tactic: refine RingHom.finiteType_algebraMap.mpr ?_
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (goal)
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 ∉ 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'
have 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'
Tactic: obtain ⟨s₁, hs₁q, hs₁⟩ := Ideal.exists_not_mem_forall_mem_of_ne_of_liesOver (R := R) p q
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (goal)
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 ∉ 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'
have 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'
Tactic: obtain ⟨s₂, hs₂q, hs₂⟩ := Algebra.ZariskisMainProperty.of_finiteType (R := R) q
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (goal)
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 ∉ 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'
have 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'
Tactic: obtain ⟨s₃, hs₃⟩ := hs₂.2 (algebraMap _ _ s₁)