awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : QuasiFiniteAt R q
s : S
hsq : s ∉ q
hRs : IsIntegral R s
hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
hs₀ :
  ∀ (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 hRs ∈ q'
m : ℕ
f : R[X]
b : p.ResidueField[X]
hfm : f.Monic
hbm : b.Monic
hab : IsCoprime (HPow.hPow (α := p.ResidueField[X]) X (m + 1)) b
hfab : Polynomial.map (algebraMap R p.ResidueField) f = HPow.hPow (α := p.ResidueField[X]) X (m + 1) * b
hf : Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) f : S) (0 : S)
R' : Type u
w : CommRing R'
w_1 : Algebra R R'
w_2 : Etale R R'
P : Ideal R'
w_3 : P.IsPrime
w_4 : P.LiesOver p
a' b' : R'[X]
hP :
  Function.Bijective (α := p.ResidueField) (β := P.ResidueField)
    (⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) : (a : p.ResidueField) → P.ResidueField)
ha'm : a'.Monic
hb'm : b'.Monic
hfab' : Polynomial.map (algebraMap R R') f = a' * b'
c d : R'[X]
hcd : c * a' + d * b' = 1
ha' :
  Eq (α := P.ResidueField[X])
    (Polynomial.map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯))
      (HPow.hPow (α := p.ResidueField[X]) X (m + 1)))
    (Polynomial.map (algebraMap R' P.ResidueField) a')
hb' :
  Eq (α := P.ResidueField[X]) (Polynomial.map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)) b)
    (Polynomial.map (algebraMap R' P.ResidueField) b')
s₀ : ↥(integralClosure R S) :=
  Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hRs
hfs₀ :
  Eq.{v + 1} (α := ↥(integralClosure R S)) ((aeval s₀ : (a : R[X]) → ↥(integralClosure R S)) f : ↥(integralClosure R S))
    (0 : ↥(integralClosure R S))
s' : R' ⊗[R] S := 1 ⊗ₜ[R] s
hs'f : Eq (α := R' ⊗[R] S) ((aeval s' : (a : R[X]) → R' ⊗[R] S) f : R' ⊗[R] S) (0 : R' ⊗[R] S)
hs₀'f :
  Eq (α := TensorProduct.{u, u, v} R R' ↥(integralClosure R S))
    ((aeval (1 ⊗ₜ[R] s₀) : (a : R[X]) → R' ⊗[R] ↥(integralClosure R S)) f :
      TensorProduct.{u, u, v} R R' ↥(integralClosure R S))
    (0 : TensorProduct.{u, u, v} R R' ↥(integralClosure R S))
e₀ : TensorProduct.{u, u, v} R R' ↥(integralClosure R S) :=
  (aeval (1 ⊗ₜ[R] s₀) : (a : R'[X]) → R' ⊗[R] ↥(integralClosure R S)) (c * a')
he₀ : IsIdempotentElem e₀
e : R' ⊗[R] S := (aeval s' : (a : R'[X]) → R' ⊗[R] S) (c * a')
φ : TensorProduct.{u, u, v} R R' ↥(integralClosure R S) →ₐ[R'] R' ⊗[R] S :=
  TensorProduct.map (AlgHom.id R' R') (Subalgebra.val (integralClosure R S))
⊢ ((aeval ((φ : (a : R' ⊗[R] ↥(integralClosure R S)) → R' ⊗[R] S) (1 ⊗ₜ[R] s₀)) : R'[X] →ₐ[R'] R' ⊗[R] S) :
        (a : R'[X]) → R' ⊗[R] S)
      (c * a') =
    e

Tactic:
rfl
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : QuasiFiniteAt R q
s : S
hsq : s ∉ q
hRs : IsIntegral R s
hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
hs₀ :
  ∀ (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 hRs ∈ q'
m : ℕ
f : R[X]
b : p.ResidueField[X]
hfm : f.Monic
hbm : b.Monic
hab : IsCoprime (HPow.hPow (α := p.ResidueField[X]) X (m + 1)) b
hfab : Polynomial.map (algebraMap R p.ResidueField) f = HPow.hPow (α := p.ResidueField[X]) X (m + 1) * b
hf : Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) f : S) (0 : S)
R' : Type u
w : CommRing R'
w_1 : Algebra R R'
w_2 : Etale R R'
P : Ideal R'
w_3 : P.IsPrime
w_4 : P.LiesOver p
a' b' : R'[X]
hP :
  Function.Bijective (α := p.ResidueField) (β := P.ResidueField)
    (⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) : (a : p.ResidueField) → P.ResidueField)
ha'm : a'.Monic
hb'm : b'.Monic
hfab' : Polynomial.map (algebraMap R R') f = a' * b'
c d : R'[X]
hcd : c * a' + d * b' = 1
ha' :
  Eq (α := P.ResidueField[X])
    (Polynomial.map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯))
      (HPow.hPow (α := p.ResidueField[X]) X (m + 1)))
    (Polynomial.map (algebraMap R' P.ResidueField) a')
hb' :
  Eq (α := P.ResidueField[X]) (Polynomial.map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)) b)
    (Polynomial.map (algebraMap R' P.ResidueField) b')
s₀ : ↥(integralClosure R S) :=
  Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hRs
hfs₀ :
  Eq.{v + 1} (α := ↥(integralClosure R S)) ((aeval s₀ : (a : R[X]) → ↥(integralClosure R S)) f : ↥(integralClosure R S))
    (0 : ↥(integralClosure R S))
s' : R' ⊗[R] S := 1 ⊗ₜ[R] s
hs'f : Eq (α := R' ⊗[R] S) ((aeval s' : (a : R[X]) → R' ⊗[R] S) f : R' ⊗[R] S) (0 : R' ⊗[R] S)
hs₀'f :
  Eq (α := TensorProduct.{u, u, v} R R' ↥(integralClosure R S))
    ((aeval (1 ⊗ₜ[R] s₀) : (a : R[X]) → R' ⊗[R] ↥(integralClosure R S)) f :
      TensorProduct.{u, u, v} R R' ↥(integralClosure R S))
    (0 : TensorProduct.{u, u, v} R R' ↥(integralClosure R S))
e₀ : TensorProduct.{u, u, v} R R' ↥(integralClosure R S) :=
  (aeval (1 ⊗ₜ[R] s₀) : (a : R'[X]) → R' ⊗[R] ↥(integralClosure R S)) (c * a')
he₀ : IsIdempotentElem e₀
e : R' ⊗[R] S := (aeval s' : (a : R'[X]) → R' ⊗[R] S) (c * a')
φ : TensorProduct.{u, u, v} R R' ↥(integralClosure R S) →ₐ[R'] R' ⊗[R] S :=
  TensorProduct.map (AlgHom.id R' R') (Subalgebra.val (integralClosure R S))
⊢ (φ : (a : R' ⊗[R] ↥(integralClosure R S)) → R' ⊗[R] S) e₀ = e

Tactic:
have he₀e : φ e₀ = e := by
    simp only [e₀, ← aeval_algHom_apply]; rfl
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : QuasiFiniteAt R q
s : S
hsq : s ∉ q
hRs : IsIntegral R s
hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
hs₀ :
  ∀ (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 hRs ∈ q'
m : ℕ
f : R[X]
b : p.ResidueField[X]
hfm : f.Monic
hbm : b.Monic
hab : IsCoprime (HPow.hPow (α := p.ResidueField[X]) X (m + 1)) b
hfab : Polynomial.map (algebraMap R p.ResidueField) f = HPow.hPow (α := p.ResidueField[X]) X (m + 1) * b
hf : Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) f : S) (0 : S)
R' : Type u
w : CommRing R'
w_1 : Algebra R R'
w_2 : Etale R R'
P : Ideal R'
w_3 : P.IsPrime
w_4 : P.LiesOver p
a' b' : R'[X]
hP :
  Function.Bijective (α := p.ResidueField) (β := P.ResidueField)
    (⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) : (a : p.ResidueField) → P.ResidueField)
ha'm : a'.Monic
hb'm : b'.Monic
hfab' : Polynomial.map (algebraMap R R') f = a' * b'
c d : R'[X]
hcd : c * a' + d * b' = 1
ha' :
  Eq (α := P.ResidueField[X])
    (Polynomial.map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯))
      (HPow.hPow (α := p.ResidueField[X]) X (m + 1)))
    (Polynomial.map (algebraMap R' P.ResidueField) a')
hb' :
  Eq (α := P.ResidueField[X]) (Polynomial.map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)) b)
    (Polynomial.map (algebraMap R' P.ResidueField) b')
s₀ : ↥(integralClosure R S) :=
  Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hRs
hfs₀ :
  Eq.{v + 1} (α := ↥(integralClosure R S)) ((aeval s₀ : (a : R[X]) → ↥(integralClosure R S)) f : ↥(integralClosure R S))
    (0 : ↥(integralClosure R S))
s' : R' ⊗[R] S := 1 ⊗ₜ[R] s
hs'f : Eq (α := R' ⊗[R] S) ((aeval s' : (a : R[X]) → R' ⊗[R] S) f : R' ⊗[R] S) (0 : R' ⊗[R] S)
hs₀'f :
  Eq (α := TensorProduct.{u, u, v} R R' ↥(integralClosure R S))
    ((aeval (1 ⊗ₜ[R] s₀) : (a : R[X]) → R' ⊗[R] ↥(integralClosure R S)) f :
      TensorProduct.{u, u, v} R R' ↥(integralClosure R S))
    (0 : TensorProduct.{u, u, v} R R' ↥(integralClosure R S))
e₀ : TensorProduct.{u, u, v} R R' ↥(integralClosure R S) :=
  (aeval (1 ⊗ₜ[R] s₀) : (a : R'[X]) → R' ⊗[R] ↥(integralClosure R S)) (c * a')
he₀ : IsIdempotentElem e₀
e : R' ⊗[R] S := (aeval s' : (a : R'[X]) → R' ⊗[R] S) (c * a')
φ : TensorProduct.{u, u, v} R R' ↥(integralClosure R S) →ₐ[R'] R' ⊗[R] S :=
  TensorProduct.map (AlgHom.id R' R') (Subalgebra.val (integralClosure R S))
he₀e : (φ : (a : R' ⊗[R] ↥(integralClosure R S)) → R' ⊗[R] S) e₀ = e
⊢ IsIdempotentElem e

Tactic:
have he : IsIdempotentElem e := he₀e ▸ he₀.map _
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
inst_4 : CommRing R'
inst_5 : Algebra R R'
inst_6 : CommRing R''
inst_7 : Algebra R R''
inst_8 : Algebra R'' S
inst_9 : Algebra.IsIntegral R R''
inst_10 : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst_11 : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e :
  ((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
        (a : R' ⊗[R] R'') → R' ⊗[R] S)
      e₀ =
    e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' →
          P'' =
            Ideal.comap (F := R' ⊗[R] R'' →+* R' ⊗[R] S)
              (AlgHom.toRingHom
                (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S))
              P'
g : R''
hgq : ((algebraMap R'' S : (a : R'') → S) g : S) ∉ q
hg :
  Function.Surjective.{u_5 + 1, u_3 + 1} (α := Localization.Away g) (β :=
    Localization.Away (M := S) ((algebraMap R'' S : (a : R'') → S) g : S))
    (⇑(Localization.awayMap (algebraMap R'' S) g) :
      (a : Localization.Away g) → Localization.Away ((algebraMap R'' S : (a : R'') → S) g))
⊢ Algebra.IsIntegral R' (Localization.Away e₀)

Tactic:
have : Algebra.IsIntegral R' (Localization.Away e₀) :=
    .of_surjective (IsScalarTower.toAlgHom R' (R' ⊗[R] (R'')) _)
      (IsLocalization.Away.algebraMap_surjective_of_isIdempotentElem e₀ he₀)
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
inst_4 : CommRing R'
inst_5 : Algebra R R'
inst_6 : CommRing R''
inst_7 : Algebra R R''
inst_8 : Algebra R'' S
inst_9 : Algebra.IsIntegral R R''
inst_10 : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst_11 : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e :
  ((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
        (a : R' ⊗[R] R'') → R' ⊗[R] S)
      e₀ =
    e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' →
          P'' =
            Ideal.comap (F := R' ⊗[R] R'' →+* R' ⊗[R] S)
              (AlgHom.toRingHom
                (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S))
              P'
g : R''
hgq : ((algebraMap R'' S : (a : R'') → S) g : S) ∉ q
hg :
  Function.Surjective.{u_5 + 1, u_3 + 1} (α := Localization.Away g) (β :=
    Localization.Away (M := S) ((algebraMap R'' S : (a : R'') → S) g : S))
    (⇑(Localization.awayMap (algebraMap R'' S) g) :
      (a : Localization.Away g) → Localization.Away ((algebraMap R'' S : (a : R'') → S) g))
this : Algebra.IsIntegral R' (Localization.Away e₀)
⊢ Function.Surjective (α := Localization.Away (e₀ * 1 ⊗ₜ[R] g)) (β :=
    Localization.Away (M := R' ⊗[R] S)
      (((AlgHom.toRingHom
                (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
              R' ⊗[R] R'' →+* R' ⊗[R] S) :
            (a : R' ⊗[R] R'') → R' ⊗[R] S)
          (e₀ * 1 ⊗ₜ[R] g) :
        R' ⊗[R] S))
    (⇑(Localization.awayMap
          (AlgHom.toRingHom
            (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S))
          (e₀ * 1 ⊗ₜ[R] g)) :
      (a : Localization.Away (e₀ * 1 ⊗ₜ[R] g)) →
        Localization.Away
          (((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom :
              (a : R' ⊗[R] R'') → R' ⊗[R] S)
            (e₀ * 1 ⊗ₜ[R] g)))

Tactic:
Localization.awayMap_surjective_iff.mpr fun a ↦ ?_

Premises used: Iff.mpr, Localization.awayMap_surjective_iff
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
inst_4 : CommRing R'
inst_5 : Algebra R R'
inst_6 : CommRing R''
inst_7 : Algebra R R''
inst_8 : Algebra R'' S
inst_9 : Algebra.IsIntegral R R''
inst_10 : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst_11 : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e :
  ((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
        (a : R' ⊗[R] R'') → R' ⊗[R] S)
      e₀ =
    e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' →
          P'' =
            Ideal.comap (F := R' ⊗[R] R'' →+* R' ⊗[R] S)
              (AlgHom.toRingHom
                (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S))
              P'
g : R''
hgq : ((algebraMap R'' S : (a : R'') → S) g : S) ∉ q
hg :
  Function.Surjective.{u_5 + 1, u_3 + 1} (α := Localization.Away g) (β :=
    Localization.Away (M := S) ((algebraMap R'' S : (a : R'') → S) g : S))
    (⇑(Localization.awayMap (algebraMap R'' S) g) :
      (a : Localization.Away g) → Localization.Away ((algebraMap R'' S : (a : R'') → S) g))
this : Algebra.IsIntegral R' (Localization.Away e₀)
H₁ :
  ∀ (a : R' ⊗[R] S),
    ∃ (b : R' ⊗[R] R'') (m : ℕ),
      ((AlgHom.toRingHom
                (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
              R' ⊗[R] R'' →+* R' ⊗[R] S) :
            (a : R' ⊗[R] R'') → R' ⊗[R] S)
          b =
        HPow.hPow (α := R' ⊗[R] S)
            (((AlgHom.toRingHom
                      (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) :
                        R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
                    R' ⊗[R] R'' →+* R' ⊗[R] S) :
                  (a : R' ⊗[R] R'') → R' ⊗[R] S)
                (e₀ * 1 ⊗ₜ[R] g) :
              R' ⊗[R] S)
            m *
          a
⊢ Function.Surjective (α := Localization.Away (e₀ * 1 ⊗ₜ[R] g)) (β :=
    Localization.Away (M := R' ⊗[R] S)
      (((AlgHom.toRingHom
                (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
              R' ⊗[R] R'' →+* R' ⊗[R] S) :
            (a : R' ⊗[R] R'') → R' ⊗[R] S)
          (e₀ * 1 ⊗ₜ[R] g) :
        R' ⊗[R] S))
    (⇑(Localization.awayMap
          (AlgHom.toRingHom
            (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S))
          (e₀ * 1 ⊗ₜ[R] g)) :
      (a : Localization.Away (e₀ * 1 ⊗ₜ[R] g)) →
        Localization.Away
          (((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom :
              (a : R' ⊗[R] R'') → R' ⊗[R] S)
            (e₀ * 1 ⊗ₜ[R] g)))

Tactic:
refine Localization.awayMap_surjective_iff.mpr fun a ↦ ?_

Premises used: Iff.mpr, Localization.awayMap_surjective_iff
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
inst_4 : CommRing R'
inst_5 : Algebra R R'
inst_6 : CommRing R''
inst_7 : Algebra R R''
inst_8 : Algebra R'' S
inst_9 : Algebra.IsIntegral R R''
inst_10 : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst_11 : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e :
  ((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
        (a : R' ⊗[R] R'') → R' ⊗[R] S)
      e₀ =
    e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' →
          P'' =
            Ideal.comap (F := R' ⊗[R] R'' →+* R' ⊗[R] S)
              (AlgHom.toRingHom
                (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S))
              P'
g : R''
hgq : ((algebraMap R'' S : (a : R'') → S) g : S) ∉ q
hg :
  Function.Surjective.{u_5 + 1, u_3 + 1} (α := Localization.Away g) (β :=
    Localization.Away (M := S) ((algebraMap R'' S : (a : R'') → S) g : S))
    (⇑(Localization.awayMap (algebraMap R'' S) g) :
      (a : Localization.Away g) → Localization.Away ((algebraMap R'' S : (a : R'') → S) g))
this : Algebra.IsIntegral R' (Localization.Away e₀)
h :
  ∃ (m : ℕ),
    ((AlgHom.toRingHom
              (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
            R' ⊗[R] R'' →+* R' ⊗[R] S) :
          (a : R' ⊗[R] R'') → R' ⊗[R] S)
        0 =
      HPow.hPow (α := R' ⊗[R] S)
          (((AlgHom.toRingHom
                    (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) :
                      R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
                  R' ⊗[R] R'' →+* R' ⊗[R] S) :
                (a : R' ⊗[R] R'') → R' ⊗[R] S)
              (e₀ * 1 ⊗ₜ[R] g) :
            R' ⊗[R] S)
          m *
        0
⊢ ∃ (b : R' ⊗[R] R'') (m : ℕ),
    ((AlgHom.toRingHom
              (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
            R' ⊗[R] R'' →+* R' ⊗[R] S) :
          (a : R' ⊗[R] R'') → R' ⊗[R] S)
        b =
      HPow.hPow (α := R' ⊗[R] S)
          (((AlgHom.toRingHom
                    (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) :
                      R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
                  R' ⊗[R] R'' →+* R' ⊗[R] S) :
                (a : R' ⊗[R] R'') → R' ⊗[R] S)
              (e₀ * 1 ⊗ₜ[R] g) :
            R' ⊗[R] S)
          m *
        0

Tactic:
use 0
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
inst_4 : CommRing R'
inst_5 : Algebra R R'
inst_6 : CommRing R''
inst_7 : Algebra R R''
inst_8 : Algebra R'' S
inst_9 : Algebra.IsIntegral R R''
inst_10 : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst_11 : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e :
  ((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
        (a : R' ⊗[R] R'') → R' ⊗[R] S)
      e₀ =
    e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' →
          P'' =
            Ideal.comap (F := R' ⊗[R] R'' →+* R' ⊗[R] S)
              (AlgHom.toRingHom
                (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S))
              P'
g : R''
hgq : ((algebraMap R'' S : (a : R'') → S) g : S) ∉ q
hg :
  Function.Surjective.{u_5 + 1, u_3 + 1} (α := Localization.Away g) (β :=
    Localization.Away (M := S) ((algebraMap R'' S : (a : R'') → S) g : S))
    (⇑(Localization.awayMap (algebraMap R'' S) g) :
      (a : Localization.Away g) → Localization.Away ((algebraMap R'' S : (a : R'') → S) g))
this : Algebra.IsIntegral R' (Localization.Away e₀)
⊢ ∃ (m : ℕ),
    ((AlgHom.toRingHom
              (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
            R' ⊗[R] R'' →+* R' ⊗[R] S) :
          (a : R' ⊗[R] R'') → R' ⊗[R] S)
        0 =
      HPow.hPow (α := R' ⊗[R] S)
          (((AlgHom.toRingHom
                    (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) :
                      R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
                  R' ⊗[R] R'' →+* R' ⊗[R] S) :
                (a : R' ⊗[R] R'') → R' ⊗[R] S)
              (e₀ * 1 ⊗ₜ[R] g) :
            R' ⊗[R] S)
          m *
        0

Tactic:
simp
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
inst_4 : CommRing R'
inst_5 : Algebra R R'
inst_6 : CommRing R''
inst_7 : Algebra R R''
inst_8 : Algebra R'' S
inst_9 : Algebra.IsIntegral R R''
inst_10 : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst_11 : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e :
  ((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
        (a : R' ⊗[R] R'') → R' ⊗[R] S)
      e₀ =
    e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' →
          P'' =
            Ideal.comap (F := R' ⊗[R] R'' →+* R' ⊗[R] S)
              (AlgHom.toRingHom
                (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S))
              P'
g : R''
hgq : ((algebraMap R'' S : (a : R'') → S) g : S) ∉ q
hg :
  Function.Surjective.{u_5 + 1, u_3 + 1} (α := Localization.Away g) (β :=
    Localization.Away (M := S) ((algebraMap R'' S : (a : R'') → S) g : S))
    (⇑(Localization.awayMap (algebraMap R'' S) g) :
      (a : Localization.Away g) → Localization.Away ((algebraMap R'' S : (a : R'') → S) g))
this : Algebra.IsIntegral R' (Localization.Away e₀)
a : R'
b : S
H₁ :
  ∀ (b' : R'') (m : ℕ)
    (e : (algebraMap R'' S : (a : R'') → S) b' = HPow.hPow (α := S) ((algebraMap R'' S : (a : R'') → S) g : S) m * b),
    ∃ (b_1 : R' ⊗[R] R'') (m : ℕ),
      ((AlgHom.toRingHom
                (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
              R' ⊗[R] R'' →+* R' ⊗[R] S) :
            (a : R' ⊗[R] R'') → R' ⊗[R] S)
          b_1 =
        HPow.hPow (α := R' ⊗[R] S)
            (((AlgHom.toRingHom
                      (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) :
                        R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
                    R' ⊗[R] R'' →+* R' ⊗[R] S) :
                  (a : R' ⊗[R] R'') → R' ⊗[R] S)
                (e₀ * 1 ⊗ₜ[R] g) :
              R' ⊗[R] S)
            m *
          a ⊗ₜ[R] b
⊢ ∃ (b_1 : R' ⊗[R] R'') (m : ℕ),
    ((AlgHom.toRingHom
              (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
            R' ⊗[R] R'' →+* R' ⊗[R] S) :
          (a : R' ⊗[R] R'') → R' ⊗[R] S)
        b_1 =
      HPow.hPow (α := R' ⊗[R] S)
          (((AlgHom.toRingHom
                    (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) :
                      R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
                  R' ⊗[R] R'' →+* R' ⊗[R] S) :
                (a : R' ⊗[R] R'') → R' ⊗[R] S)
              (e₀ * 1 ⊗ₜ[R] g) :
            R' ⊗[R] S)
          m *
        a ⊗ₜ[R] b

Tactic:
obtain ⟨b', m, e : _ = _⟩ := Localization.awayMap_surjective_iff.mp hg b

Premises used: Localization.awayMap_surjective_iff, Iff.mp