awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (hypothesis)
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
inst_5 : q.LiesOver p
inst_6 : FiniteType R S
inst_7 : QuasiFiniteAt R q
s₁ : S
hs₁q : s₁ ∉ q
hs₁ : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s₁ ∈ q'
s₂ : ↥(integralClosure R S)
hs₂q : (↑s₂ : S) ∉ q
hs₂ :
  Function.Bijective (α := Localization.Away s₂) (β :=
    Localization.Away (M := S)
      ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
    (⇑(Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (integralClosure R S))) s₂) :
      (a : Localization.Away s₂) →
        Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) s₂))
s₃ : ↥(integralClosure R S)
n : ℕ
hs₃ :
  Eq (α :=
    Localization.Away (M := S)
      ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
    ((Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (integralClosure R S))) s₂ :
          (a : Localization.Away s₂) →
            Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) s₂))
        (IsLocalization.mk' (Localization.Away s₂) s₃
          (Subtype.mk (p := fun (x : ↥(integralClosure R S)) ↦
            Membership.mem (γ := Submonoid ↥(integralClosure R S)) (Submonoid.powers s₂) x) ((fun (x : ℕ) ↦ s₂ ^ x) n)
            ⋯)) :
      Localization.Away (M := S)
        ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
    ((algebraMap S
            (Localization.Away (M := S)
              ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S)) :
          (a : S) → Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) s₂))
        s₁ :
      Localization.Away (M := S)
        ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
m : ℕ
hm : (↑s₂ : S) ^ m * (↑s₃ : S) = (↑s₂ : S) ^ m * (s₁ * (↑s₂ : S) ^ n)
hm0 : 0 < m
⊢ ∃ s ∉ q,
    ∃ (hs : IsIntegral R s),
      (∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q') ∧
        ∀ (q' : Ideal ↥(integralClosure R S)),
          q'.IsPrime →
            q' ≠ Ideal.under (↥(integralClosure R S)) q →
              q'.LiesOver p →
                Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hs ∈ q'
have hs₃q : (↑s₃ : S) ∉ q
Tactic: have hs₃q : s₃.1 ∉ q := fun h ↦ (show ↑s₂ ^ m * (s₁ * ↑s₂ ^ n) ∉ q from q.primeCompl.mul_mem
    (pow_mem hs₂q _) (mul_mem hs₁q (pow_mem hs₂q _))) (hm ▸ Ideal.mul_mem_left _ _ h)
-- 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₃ : ↥(integralClosure R S)
n : ℕ
hs₃ :
  Eq (α :=
    Localization.Away (M := S)
      ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
    ((Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (integralClosure R S))) s₂ :
          (a : Localization.Away s₂) →
            Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) s₂))
        (IsLocalization.mk' (Localization.Away s₂) s₃
          (Subtype.mk (p := fun (x : ↥(integralClosure R S)) ↦
            Membership.mem (γ := Submonoid ↥(integralClosure R S)) (Submonoid.powers s₂) x) ((fun (x : ℕ) ↦ s₂ ^ x) n)
            ⋯)) :
      Localization.Away (M := S)
        ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
    ((algebraMap S
            (Localization.Away (M := S)
              ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S)) :
          (a : S) → Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) s₂))
        s₁ :
      Localization.Away (M := S)
        ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
m : ℕ
hm : (↑s₂ : S) ^ m * (↑s₃ : S) = (↑s₂ : S) ^ m * (s₁ * (↑s₂ : S) ^ n)
hm0 : 0 < m
hs₃q : (↑s₃ : 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 refine : ∀ (q' : Ideal ↥(integralClosure R S)),
  q'.IsPrime →
    ∀ (hq'q : 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₂ : S) ^ m * (↑s₃ : S)) sorry ∈
          q'
Tactic: refine ⟨↑s₂ ^ m * ↑s₃, q.primeCompl.mul_mem (pow_mem hs₂q _) hs₃q, (s₂ ^ m * s₃).2,
    fun q' _ hq'q _ ↦ hm ▸ Ideal.mul_mem_left _ _ (Ideal.mul_mem_right _ _ (hs₁ q' ‹_› hq'q ‹_›)),
    fun q' _ hq'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₃ : ↥(integralClosure R S)
n : ℕ
hs₃ :
  Eq (α :=
    Localization.Away (M := S)
      ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
    ((Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (integralClosure R S))) s₂ :
          (a : Localization.Away s₂) →
            Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) s₂))
        (IsLocalization.mk' (Localization.Away s₂) s₃
          (Subtype.mk (p := fun (x : ↥(integralClosure R S)) ↦
            Membership.mem (γ := Submonoid ↥(integralClosure R S)) (Submonoid.powers s₂) x) ((fun (x : ℕ) ↦ s₂ ^ x) n)
            ⋯)) :
      Localization.Away (M := S)
        ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
    ((algebraMap S
            (Localization.Away (M := S)
              ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S)) :
          (a : S) → Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) s₂))
        s₁ :
      Localization.Away (M := S)
        ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
m : ℕ
hm : (↑s₂ : S) ^ m * (↑s₃ : S) = (↑s₂ : S) ^ m * (s₁ * (↑s₂ : S) ^ n)
hm0 : 0 < m
hs₃q : (↑s₃ : S) ∉ q
q' : Ideal ↥(integralClosure R S)
h : q'.IsPrime
hq'q : q' ≠ Ideal.under (↥(integralClosure R S)) q
h_1 : q'.LiesOver p
this : Algebra (↥(integralClosure R S)) (Localization.Away (↑s₂ : S)) := OreLocalization.instAlgebra
e : Localization.Away s₂ ≃ₐ[↥(integralClosure R S)] Localization.Away (↑s₂ : S) :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
q's : Ideal (Localization.Away s₂) :=
  Ideal.map (F := ↥(integralClosure R S) →+* Localization.Away s₂)
    (algebraMap (↥(integralClosure R S)) (Localization.Away s₂)) q'
⊢ Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x)
      ((↑s₂ : S) ^ m * (↑s₃ : S)) ⋯ ∈
    q'
have by_contra : ∀
  (H :
    ¬Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x)
          ((↑s₂ : S) ^ m * (↑s₃ : S)) sorry ∈
        q'),
  False
Tactic: by_contra H
-- 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₃ : ↥(integralClosure R S)
n : ℕ
hs₃ :
  Eq (α :=
    Localization.Away (M := S)
      ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
    ((Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (integralClosure R S))) s₂ :
          (a : Localization.Away s₂) →
            Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) s₂))
        (IsLocalization.mk' (Localization.Away s₂) s₃
          (Subtype.mk (p := fun (x : ↥(integralClosure R S)) ↦
            Membership.mem (γ := Submonoid ↥(integralClosure R S)) (Submonoid.powers s₂) x) ((fun (x : ℕ) ↦ s₂ ^ x) n)
            ⋯)) :
      Localization.Away (M := S)
        ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
    ((algebraMap S
            (Localization.Away (M := S)
              ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S)) :
          (a : S) → Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) s₂))
        s₁ :
      Localization.Away (M := S)
        ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
m : ℕ
hm : (↑s₂ : S) ^ m * (↑s₃ : S) = (↑s₂ : S) ^ m * (s₁ * (↑s₂ : S) ^ n)
hm0 : 0 < m
hs₃q : (↑s₃ : S) ∉ q
q' : Ideal ↥(integralClosure R S)
h : q'.IsPrime
hq'q : q' ≠ Ideal.under (↥(integralClosure R S)) q
h_1 : q'.LiesOver p
this : Algebra (↥(integralClosure R S)) (Localization.Away (↑s₂ : S)) := OreLocalization.instAlgebra
e : Localization.Away s₂ ≃ₐ[↥(integralClosure R S)] Localization.Away (↑s₂ : S) :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
q's : Ideal (Localization.Away s₂) :=
  Ideal.map (F := ↥(integralClosure R S) →+* Localization.Away s₂)
    (algebraMap (↥(integralClosure R S)) (Localization.Away s₂)) q'
H :
  ¬Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x)
        ((↑s₂ : S) ^ m * (↑s₃ : S)) ⋯ ∈
      q'
⊢ Disjoint (↑(Submonoid.powers s₂) : Set ↥(integralClosure R S)) (↑q' : Set ↥(integralClosure R S))
have rw : s₂ ∉ q'
Tactic: rw [Ideal.disjoint_powers_iff_notMem_of_isPrime]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (goal)
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'
f : R[X] := HMul.hMul (α := R[X]) X (minpoly R s)
⊢ ∃ (m : ℕ) (f : R[X]) (b : p.ResidueField[X]),
    f.Monic ∧
      b.Monic ∧
        IsCoprime (HPow.hPow (α := p.ResidueField[X]) X (m + 1)) b ∧
          Polynomial.map (algebraMap R p.ResidueField) f = HPow.hPow (α := p.ResidueField[X]) X (m + 1) * b ∧
            Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) f : S) (0 : S)
have obtain : ∀ (q : p.ResidueField[X])
  (hq :
    Polynomial.map (algebraMap R p.ResidueField) (minpoly R s) =
      HSub.hSub (α := p.ResidueField[X]) X ((C : (a : p.ResidueField) → p.ResidueField[X]) 0) ^
          rootMultiplicity (R := p.ResidueField) 0 (Polynomial.map (algebraMap R p.ResidueField) (minpoly R s)) *
        q)
  (hq' : ¬HSub.hSub (α := p.ResidueField[X]) X ((C : (a : p.ResidueField) → p.ResidueField[X]) 0) ∣ q),
  ∃ (m : ℕ) (f : R[X]) (b : p.ResidueField[X]),
    f.Monic ∧
      b.Monic ∧
        IsCoprime (HPow.hPow (α := p.ResidueField[X]) X (m + 1)) b ∧
          Polynomial.map (algebraMap R p.ResidueField) f = HPow.hPow (α := p.ResidueField[X]) X (m + 1) * b ∧
            Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) f : S) (0 : S)
Tactic: obtain ⟨q, hq, hq'⟩ := exists_eq_pow_rootMultiplicity_mul_and_not_dvd
      ((minpoly R s).map (algebraMap R p.ResidueField)) ((minpoly.monic hRs).map _).ne_zero 0
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (hypothesis)
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_1 : Ideal S
inst_5 : q_1.IsPrime
inst_6 : q_1.LiesOver p
inst_7 : QuasiFiniteAt R q_1
s : S
hsq : s ∉ q_1
hRs : IsIntegral R s
hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q_1 → q'.LiesOver p → s ∈ q'
hs₀ :
  ∀ (q' : Ideal ↥(integralClosure R S)),
    q'.IsPrime →
      q' ≠ Ideal.under (↥(integralClosure R S)) q_1 →
        q'.LiesOver p →
          Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hRs ∈ q'
f : R[X] := HMul.hMul (α := R[X]) X (minpoly R s)
q : p.ResidueField[X]
hq :
  Polynomial.map (algebraMap R p.ResidueField) (minpoly R s) =
    HSub.hSub (α := p.ResidueField[X]) X ((C : (a : p.ResidueField) → p.ResidueField[X]) 0) ^
        rootMultiplicity (R := p.ResidueField) 0 (Polynomial.map (algebraMap R p.ResidueField) (minpoly R s)) *
      q
hq' : ¬HSub.hSub (α := p.ResidueField[X]) X ((C : (a : p.ResidueField) → p.ResidueField[X]) 0) ∣ q
⊢ ∃ (m : ℕ) (f : R[X]) (b : p.ResidueField[X]),
    f.Monic ∧
      b.Monic ∧
        IsCoprime (HPow.hPow (α := p.ResidueField[X]) X (m + 1)) b ∧
          Polynomial.map (algebraMap R p.ResidueField) f = HPow.hPow (α := p.ResidueField[X]) X (m + 1) * b ∧
            Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) f : S) (0 : S)
have hqm : q.Monic
Tactic: have hqm : q.Monic := by
      simpa [((minpoly.monic hRs).map _).leadingCoeff] using congr(leadingCoeff $hq).symm
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (goal)
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_1 : Ideal S
inst_5 : q_1.IsPrime
inst_6 : q_1.LiesOver p
inst_7 : QuasiFiniteAt R q_1
s : S
hsq : s ∉ q_1
hRs : IsIntegral R s
hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q_1 → q'.LiesOver p → s ∈ q'
hs₀ :
  ∀ (q' : Ideal ↥(integralClosure R S)),
    q'.IsPrime →
      q' ≠ Ideal.under (↥(integralClosure R S)) q_1 →
        q'.LiesOver p →
          Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hRs ∈ q'
f : R[X] := HMul.hMul (α := R[X]) X (minpoly R s)
q : p.ResidueField[X]
hq' : ¬HSub.hSub (α := p.ResidueField[X]) X ((C : (a : p.ResidueField) → p.ResidueField[X]) 0) ∣ q
hqm : q.Monic
m' : ℕ := rootMultiplicity (R := p.ResidueField) 0 (Polynomial.map (algebraMap R p.ResidueField) (minpoly R s))
hq :
  Polynomial.map (algebraMap R p.ResidueField) (minpoly R s) =
    HSub.hSub (α := p.ResidueField[X]) X ((C : (a : p.ResidueField) → p.ResidueField[X]) 0) ^ m' * q
⊢ ∃ (m : ℕ) (f : R[X]) (b : p.ResidueField[X]),
    f.Monic ∧
      b.Monic ∧
        IsCoprime (HPow.hPow (α := p.ResidueField[X]) X (m + 1)) b ∧
          Polynomial.map (algebraMap R p.ResidueField) f = HPow.hPow (α := p.ResidueField[X]) X (m + 1) * b ∧
            Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) f : S) (0 : S)
have refine : IsCoprime (HPow.hPow (α := p.ResidueField[X]) X (m' + 1)) q
Tactic: refine ⟨m', f, q, monic_X.mul (minpoly.monic hRs), hqm, ?_,
      by simp [f, hq, pow_succ', mul_assoc], by simp [f]⟩
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (goal)
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
⊢ Eq.{v + 1} (α := ↥(integralClosure R S)) ((aeval s₀ : (a : R[X]) → ↥(integralClosure R S)) f : ↥(integralClosure R S))
    (0 : ↥(integralClosure R S))
have a : Eq.{v + 1} (α := S) (↑((aeval s₀ : (a : R[X]) → ↥(integralClosure R S)) f) : S) (↑0 : S)
Tactic: ext1
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (goal)
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
⊢ Eq.{v + 1} (α := S) (↑((aeval s₀ : (a : R[X]) → ↥(integralClosure R S)) f) : S) (↑0 : S)
have a : Eq (α := S)
  ((Subalgebra.val (integralClosure R S) : (a : ↥(integralClosure R S)) → S)
      ((aeval s₀ : (a : R[X]) → ↥(integralClosure R S)) f : ↥(integralClosure R S)) :
    S)
  (0 : S)
Tactic: change (integralClosure R S).val (aeval s₀ f) = 0
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (goal)
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
⊢ Eq (α := S)
    ((Subalgebra.val (integralClosure R S) : (a : ↥(integralClosure R S)) → S)
        ((aeval s₀ : (a : R[X]) → ↥(integralClosure R S)) f : ↥(integralClosure R S)) :
      S)
    (0 : S)
have a : Eq.{v + 1} (α := S)
  (((aeval ((Subalgebra.val (integralClosure R S) : (a : ↥(integralClosure R S)) → S) s₀) : R[X] →ₐ[R] S) :
        (a : R[X]) → S)
      f :
    S)
  (0 : S)
Tactic: rwa [← aeval_algHom_apply]