awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (goal)
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)))
have 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
Tactic: refine Localization.awayMap_surjective_iff.mpr fun a ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (goal)
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₀)
⊢ ∃ (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
have 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
Tactic: use 0
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨b', m, e : _ = _⟩ := Localization.awayMap_surjective_iff.mp hg b
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (goal)
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_1 : 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_1
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
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
have H₁ : ((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₀ ^ m * a ⊗ₜ[R] 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 ⊗ₜ[R] b
Tactic: refine ⟨e₀ ^ m * a ⊗ₜ b', m, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (goal)
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₀)
⊢ IsUnit (M := P.Fiber (Localization.Away e₀))
    (1 ⊗ₜ[R'] (algebraMap (R' ⊗[R] R'') (Localization.Away e₀) : (a : R' ⊗[R] R'') → Localization.Away e₀) (1 ⊗ₜ[R] g))
have contrapose : ∀
  (hgq :
    ¬IsUnit (M := P.Fiber (Localization.Away e₀))
        (1 ⊗ₜ[R']
          (algebraMap (R' ⊗[R] R'') (Localization.Away e₀) : (a : R' ⊗[R] R'') → Localization.Away e₀) (1 ⊗ₜ[R] g))),
  Membership.mem (α := S) q ((algebraMap R'' S : (a : R'') → S) g : S)
Tactic: contrapose hgq
Cleared hypotheses: hgq
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (goal)
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''
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₀)
hgq :
  ¬IsUnit (M := P.Fiber (Localization.Away e₀))
      (1 ⊗ₜ[R']
        (algebraMap (R' ⊗[R] R'') (Localization.Away e₀) : (a : R' ⊗[R] R'') → Localization.Away e₀) (1 ⊗ₜ[R] g))
⊢ Membership.mem (α := S) q ((algebraMap R'' S : (a : R'') → S) g : S)
have obtain : ∀ (m : Ideal (P.Fiber (Localization.Away e₀))),
  m.IsMaximal →
    ∀
      (hm :
        Ideal.span
            {1 ⊗ₜ[R']
                (algebraMap (R' ⊗[R] R'') (Localization.Away e₀) : (a : R' ⊗[R] R'') → Localization.Away e₀)
                  (1 ⊗ₜ[R] g)} ≤
          m),
      Membership.mem (α := S) q ((algebraMap R'' S : (a : R'') → S) g : S)
Tactic: obtain ⟨m, _, hm⟩ := Ideal.exists_le_maximal _ (Ideal.span_singleton_eq_top.not.mpr hgq)
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (hypothesis)
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''
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₀)
hgq :
  ¬IsUnit (M := P.Fiber (Localization.Away e₀))
      (1 ⊗ₜ[R']
        (algebraMap (R' ⊗[R] R'') (Localization.Away e₀) : (a : R' ⊗[R] R'') → Localization.Away e₀) (1 ⊗ₜ[R] g))
m : Ideal (P.Fiber (Localization.Away e₀))
left : m.IsMaximal
hm :
  Ideal.span
      {1 ⊗ₜ[R']
          (algebraMap (R' ⊗[R] R'') (Localization.Away e₀) : (a : R' ⊗[R] R'') → Localization.Away e₀) (1 ⊗ₜ[R] g)} ≤
    m
⊢ Membership.mem (α := S) q ((algebraMap R'' S : (a : R'') → S) g : S)
have this₁ : Eq (α := Ideal (R' ⊗[R] R''))
  (Ideal.comap (F := R' ⊗[R] R'' →+* P.ResidueField ⊗[R'] Localization.Away e₀)
    (RingHom.comp (AlgHom.toRingHom TensorProduct.includeRight) (algebraMap (R' ⊗[R] R'') (Localization.Away e₀))) m)
  (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')
Tactic: have := H (m.comap (Algebra.TensorProduct.includeRight.toRingHom.comp (algebraMap _ _)))
      inferInstance (m.comap_liesOver P (Algebra.TensorProduct.includeRight.comp
        (IsScalarTower.toAlgHom _ _ _)))
        (Ideal.notMem_of_isUnit (m.comap Algebra.TensorProduct.includeRight)
        (IsLocalization.Away.algebraMap_isUnit _))
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (goal)
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''
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_1 : Algebra.IsIntegral R' (Localization.Away e₀)
hgq :
  ¬IsUnit (M := P.Fiber (Localization.Away e₀))
      (1 ⊗ₜ[R']
        (algebraMap (R' ⊗[R] R'') (Localization.Away e₀) : (a : R' ⊗[R] R'') → Localization.Away e₀) (1 ⊗ₜ[R] g))
m : Ideal (P.Fiber (Localization.Away e₀))
left : m.IsMaximal
hm :
  Ideal.span
      {1 ⊗ₜ[R']
          (algebraMap (R' ⊗[R] R'') (Localization.Away e₀) : (a : R' ⊗[R] R'') → Localization.Away e₀) (1 ⊗ₜ[R] g)} ≤
    m
this :
  Eq (α := Ideal (R' ⊗[R] R''))
    (Ideal.comap (F := R' ⊗[R] R'' →+* P.ResidueField ⊗[R'] Localization.Away e₀)
      (RingHom.comp (AlgHom.toRingHom TensorProduct.includeRight) (algebraMap (R' ⊗[R] R'') (Localization.Away e₀))) m)
    (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')
⊢ Membership.mem (α := S) q ((algebraMap R'' S : (a : R'') → S) g : S)
have rw : Membership.mem (α := S) (γ := Ideal S)
  (Ideal.comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) P')
  ((algebraMap R'' S : (a : R'') → S) g : S)
Tactic: rw [← hP'q]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (goal)
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₀)
f : R'
hfP : f ∉ P
hf :
  AlgHom.Finite (R := R') (A := Localization.Away f) (B :=
    Localization.Away (M := Localization.Away e)
      ((ofId R' (Localization.Away e) : (a : R') → Localization.Away e) f : Localization.Away e))
    (Localization.awayMapₐ (ofId R' (Localization.Away e)) f)
⊢ ∃ f ∉ P,
    Module.Finite (Localization.Away f)
      (Localization.Away (M := TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S)
        (((TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S) :
                R' ⊗[R] S →ₐ[R'] TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S) :
              (a : R' ⊗[R] S) → Localization.Away f ⊗[R] S)
            e :
          TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S))
have refine : Module.Finite (Localization.Away f)
  (Localization.Away (M := TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S)
    (((TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S) :
            R' ⊗[R] S →ₐ[R'] TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S) :
          (a : R' ⊗[R] S) → Localization.Away f ⊗[R] S)
        e :
      TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S))
Tactic: refine ⟨f, hfP, ?_⟩