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_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
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
⊢ ∃ (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
-- 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 m' : ℕ
s : S
hs : HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) m' = g * s
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
⊢ ∃ (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

Premises used: Localization.awayMap_surjective_iff, Iff.mp, DFunLike.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 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
⊢ (f : (a : S) → T) (s ^ m * b) = HPow.hPow (α := T) ((f : (a : S) → T) (g * s) : T) m * x

Tactic:
simp [e, mul_pow, mul_assoc, mul_left_comm]

Premises used: mul_assoc, mul_left_comm, mul_pow
-- 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 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
⊢ (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]
-- 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 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
⊢ (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

Premises used: map_pow, pow_mul, 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_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

Tactic:
⟨s ^ m * b, (n + m' * m), 0, this ▸ ?_⟩

Premises used: HMul.hMul, Eq.rec, HPow.hPow, HAdd.hAdd, Exists.intro, OfNat.ofNat, Eq.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}))ᶜ
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
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
⊢ ∃ (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:
refine ⟨s ^ m * b, (n + m' * m), 0, this ▸ ?_⟩
-- 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 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
⊢ 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:
simp [pow_add, mul_assoc]

Premises used: mul_assoc, pow_add
-- 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)
⊢ 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))

Tactic:
have h₂ : Function.Surjective (IsLocalization.Away.map (Localization.Away (algebraMap R S r))
        (Localization.Away (algebraMap R T r)) f.toRingHom (algebraMap R S r)) := by
      intro x
      obtain ⟨x, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.exists_mk'_eq (.powers (algebraMap R T r)) x
      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))]
      have : PrimeSpectrum.basicOpen (algebraMap R S r) ≤ PrimeSpectrum.basicOpen g := by
        simpa [← SetLike.coe_subset_coe] using hrg
      simp only [PrimeSpectrum.basicOpen_le_basicOpen_iff, Ideal.mem_radical_iff,
        Ideal.mem_span_singleton] at this
      obtain ⟨m', s, hs⟩ := this
      obtain ⟨b, m, e : f b = f g ^ m * x⟩ := Localization.awayMap_surjective_iff.mp hg x
      have : f (s ^ m * b) = f (g * s) ^ m * x := by simp [e, mul_pow, mul_assoc, mul_left_comm]
      simp_rw [← hs, map_pow, AlgHom.commutes, ← pow_mul] at this
      refine ⟨s ^ m * b, (n + m' * m), 0, this ▸ ?_⟩
      simp [pow_add, mul_assoc]
-- 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))
⊢ RingHom.IsIntegral.{u, u_1} (R := Away r) (A := Away (M := T) ((algebraMap R T : (a : R) → T) r : T))
    (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:
h₁.trans _ _ (RingHom.IsIntegral.of_finite (.of_surjective _ h₂))

Premises used: RingHom.IsIntegral.of_finite, RingHom.Finite.of_surjective, RingHom.IsIntegral.trans
-- 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))
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))
⊢ 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))

Tactic:
convert! h₁.trans _ _ (RingHom.IsIntegral.of_finite (.of_surjective _ h₂)) using 1

Premises used: RingHom.IsIntegral.of_finite, RingHom.Finite.of_surjective, RingHom.IsIntegral.trans