awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : StandardEtalePair R
f g : P.Ring →ₐ[R] S
H_1 : Eq.{u_2 + 1} (α := S) ((f : (a : P.Ring) → S) P.X : S) ((g : (a : P.Ring) → S) P.X : S)
H :
  (f.comp
          (Ideal.Quotient.mkₐ R
            (Ideal.span
              (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
                {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1})))).comp
      CAlgHom =
    (g.comp
          (Ideal.Quotient.mkₐ R
            (Ideal.span
              (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
                {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1})))).comp
      CAlgHom
⊢ Eq (α := R[X] →ₐ[R] P.Ring) (aeval P.X)
    (AlgHom.comp
      (Ideal.Quotient.mkₐ R
        (Ideal.span
          (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
            {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1})))
      CAlgHom)
have hX : Eq (α := P.Ring) ((aeval P.X : (a : R[X]) → P.Ring) X : P.Ring)
  ((AlgHom.comp
          (Ideal.Quotient.mkₐ R
            (Ideal.span
              (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
                {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1})))
          CAlgHom :
        (a : R[X]) → P.Ring)
      X :
    P.Ring)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : StandardEtalePair R
f g : P.Ring →ₐ[R] S
H_1 : Eq.{u_2 + 1} (α := S) ((f : (a : P.Ring) → S) P.X : S) ((g : (a : P.Ring) → S) P.X : S)
H :
  (f.comp
          (Ideal.Quotient.mkₐ R
            (Ideal.span
              (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
                {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1})))).comp
      CAlgHom =
    (g.comp
          (Ideal.Quotient.mkₐ R
            (Ideal.span
              (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
                {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1})))).comp
      CAlgHom
⊢ f = g
have H' : Eq (α := R[X] →ₐ[R] P.Ring) (aeval P.X)
  (AlgHom.comp
    (Ideal.Quotient.mkₐ R
      (Ideal.span
        (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
          {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1})))
    CAlgHom)
Tactic: have H' : aeval (R := R) P.X = (Ideal.Quotient.mkₐ _ _).comp Polynomial.CAlgHom := by
    ext; simp [StandardEtalePair.Ring, StandardEtalePair.X]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : StandardEtalePair R
f g : P.Ring →ₐ[R] S
H_1 : Eq.{u_2 + 1} (α := S) ((f : (a : P.Ring) → S) P.X : S) ((g : (a : P.Ring) → S) P.X : S)
H :
  (f.comp
          (Ideal.Quotient.mkₐ R
            (Ideal.span
              (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
                {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1})))).comp
      CAlgHom =
    (g.comp
          (Ideal.Quotient.mkₐ R
            (Ideal.span
              (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
                {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1})))).comp
      CAlgHom
H' :
  Eq (α := R[X] →ₐ[R] P.Ring) (aeval P.X)
    (AlgHom.comp
      (Ideal.Quotient.mkₐ R
        (Ideal.span
          (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
            {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1})))
      CAlgHom)
⊢ f = g
have refine : Eq.{u_2 + 1} (α := S)
  ((f.comp
          (Ideal.Quotient.mkₐ R
            (Ideal.span
              (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
                {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1}))) :
        (a : R[X][Y]) → S)
      Y :
    S)
  ((g.comp
          (Ideal.Quotient.mkₐ R
            (Ideal.span
              (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
                {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1}))) :
        (a : R[X][Y]) → S)
      Y :
    S)
Tactic: refine Ideal.Quotient.algHom_ext _ (Polynomial.algHom_ext' H ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : StandardEtalePair R
f g : P.Ring →ₐ[R] S
H_1 : Eq.{u_2 + 1} (α := S) ((f : (a : P.Ring) → S) P.X : S) ((g : (a : P.Ring) → S) P.X : S)
H :
  (f.comp
          (Ideal.Quotient.mkₐ R
            (Ideal.span
              (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
                {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1})))).comp
      CAlgHom =
    (g.comp
          (Ideal.Quotient.mkₐ R
            (Ideal.span
              (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
                {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1})))).comp
      CAlgHom
H' :
  Eq (α := R[X] →ₐ[R] P.Ring) (aeval P.X)
    (AlgHom.comp
      (Ideal.Quotient.mkₐ R
        (Ideal.span
          (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
            {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1})))
      CAlgHom)
⊢ Eq.{u_2 + 1} (α := S)
    (((↑f.toRingHom : P.Ring →* S) : (a : P.Ring) → S)
        ((Ideal.Quotient.mk
                (Ideal.span
                  (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
                    {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1})) :
              (a : R[X][Y]) →
                R[X][Y] ⧸ Ideal.span {(C : (a : R[X]) → R[X][Y]) P.f, Y * (C : (a : R[X]) → R[X][Y]) P.g - 1})
            Y :
          HasQuotient.Quotient R[X][Y] (B := Ideal R[X][Y])
            (Ideal.span
              (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
                {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1}))) :
      S)
    (((↑g.toRingHom : P.Ring →* S) : (a : P.Ring) → S)
        ((Ideal.Quotient.mk
                (Ideal.span
                  (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
                    {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1})) :
              (a : R[X][Y]) →
                R[X][Y] ⧸ Ideal.span {(C : (a : R[X]) → R[X][Y]) P.f, Y * (C : (a : R[X]) → R[X][Y]) P.g - 1})
            Y :
          HasQuotient.Quotient R[X][Y] (B := Ideal R[X][Y])
            (Ideal.span
              (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
                {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1}))) :
      S)
have rw : Eq.{u_2 + 1} (α := S) (↑((Units.map (↑f.toRingHom : P.Ring →* S) : (a : P.Ringˣ) → Sˣ) (IsUnit.unit sorry))⁻¹ : S)
  (↑((Units.map (↑g.toRingHom : P.Ring →* S) : (a : P.Ringˣ) → Sˣ) (IsUnit.unit sorry))⁻¹ : S)
Tactic: rw [← show (↑P.hasMap_X.2.unit⁻¹ : P.Ring) = Ideal.Quotient.mk _ .X from
    Units.mul_eq_one_iff_inv_eq.mp P.aeval_X_g_mul_mk_X, ← Units.coe_map_inv, ← Units.coe_map_inv]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : StandardEtalePair R
f g : P.Ring →ₐ[R] S
H_1 : Eq.{u_2 + 1} (α := S) ((f : (a : P.Ring) → S) P.X : S) ((g : (a : P.Ring) → S) P.X : S)
H :
  (f.comp
          (Ideal.Quotient.mkₐ R
            (Ideal.span
              (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
                {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1})))).comp
      CAlgHom =
    (g.comp
          (Ideal.Quotient.mkₐ R
            (Ideal.span
              (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
                {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1})))).comp
      CAlgHom
H' :
  Eq (α := R[X] →ₐ[R] P.Ring) (aeval P.X)
    (AlgHom.comp
      (Ideal.Quotient.mkₐ R
        (Ideal.span
          (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
            {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1})))
      CAlgHom)
⊢ Eq.{u_2 + 1} (α := S) (↑((Units.map (↑f.toRingHom : P.Ring →* S) : (a : P.Ringˣ) → Sˣ) (IsUnit.unit ⋯))⁻¹ : S)
    (↑((Units.map (↑g.toRingHom : P.Ring →* S) : (a : P.Ringˣ) → Sˣ) (IsUnit.unit ⋯))⁻¹ : S)
have e_self : Eq.{u_2 + 1} (α := Sˣ) ((Units.map (↑f.toRingHom : P.Ring →* S) : (a : P.Ringˣ) → Sˣ) (IsUnit.unit sorry) : Sˣ)
  ((Units.map (↑g.toRingHom : P.Ring →* S) : (a : P.Ringˣ) → Sˣ) (IsUnit.unit sorry) : Sˣ)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : StandardEtalePair R
f g : P.Ring →ₐ[R] S
H_1 : Eq.{u_2 + 1} (α := S) ((f : (a : P.Ring) → S) P.X : S) ((g : (a : P.Ring) → S) P.X : S)
H :
  (f.comp
          (Ideal.Quotient.mkₐ R
            (Ideal.span
              (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
                {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1})))).comp
      CAlgHom =
    (g.comp
          (Ideal.Quotient.mkₐ R
            (Ideal.span
              (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
                {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1})))).comp
      CAlgHom
H' :
  Eq (α := R[X] →ₐ[R] P.Ring) (aeval P.X)
    (AlgHom.comp
      (Ideal.Quotient.mkₐ R
        (Ideal.span
          (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
            {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1})))
      CAlgHom)
⊢ Eq.{u_2 + 1} (α := Sˣ) ((Units.map (↑f.toRingHom : P.Ring →* S) : (a : P.Ringˣ) → Sˣ) (IsUnit.unit ⋯) : Sˣ)
    ((Units.map (↑g.toRingHom : P.Ring →* S) : (a : P.Ringˣ) → Sˣ) (IsUnit.unit ⋯) : Sˣ)
have e_self : Eq.{u_2 + 1} (α := S) (↑((Units.map (↑f.toRingHom : P.Ring →* S) : (a : P.Ringˣ) → Sˣ) (IsUnit.unit sorry)) : S)
  (↑((Units.map (↑g.toRingHom : P.Ring →* S) : (a : P.Ringˣ) → Sˣ) (IsUnit.unit sorry)) : S)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : HPow.hPow (β := ℕ) I 2 = ⊥
x : S
hx : P.HasMap (S := S ⧸ I) ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) x : S ⧸ I)
⊢ ∃! ε : S, ε ∈ I ∧ P.HasMap (x + ε)
have hf : Membership.mem (α := S) I ((aeval x : (a : R[X]) → S) P.f : S)
Tactic: have hf := Ideal.Quotient.eq_zero_iff_mem.mp
    ((aeval_algHom_apply (Ideal.Quotient.mkₐ R I) _ _).symm.trans hx.1)
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : HPow.hPow (β := ℕ) I 2 = ⊥
x : S
hx : P.HasMap (S := S ⧸ I) ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) x : S ⧸ I)
hf : Membership.mem (α := S) I ((aeval x : (a : R[X]) → S) P.f : S)
⊢ ∃! ε : S, ε ∈ I ∧ P.HasMap (x + ε)
have obtain : ∀ (a : S ⧸ I)
  (ha :
    HMul.hMul (α := S ⧸ I)
        (((aeval ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) x) : AlgHom.{u_1, u_1, u_2} R R[X] (S ⧸ I)) :
              (a : R[X]) → S ⧸ I)
            P.g :
          S ⧸ I)
        a =
      1),
  ∃! ε : S, ε ∈ I ∧ P.HasMap (x + ε)
Tactic: obtain ⟨⟨_, a, ha, -⟩, rfl⟩ := hx.2
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : HPow.hPow (β := ℕ) I 2 = ⊥
x : S
hx : P.HasMap (S := S ⧸ I) ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) x : S ⧸ I)
hf : Membership.mem (α := S) I ((aeval x : (a : R[X]) → S) P.f : S)
a : S ⧸ I
ha :
  HMul.hMul (α := S ⧸ I)
      (((aeval ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) x) : AlgHom.{u_1, u_1, u_2} R R[X] (S ⧸ I)) :
            (a : R[X]) → S ⧸ I)
          P.g :
        S ⧸ I)
      a =
    1
⊢ ∃! ε : S, ε ∈ I ∧ P.HasMap (x + ε)
have obtain : ∀ (a : S)
  (ha :
    HMul.hMul (α := S ⧸ I) (β := S ⧸ I)
        (((aeval ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) x) : AlgHom.{u_1, u_1, u_2} R R[X] (S ⧸ I)) :
              (a : R[X]) → S ⧸ I)
            P.g :
          S ⧸ I)
        ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) a : S ⧸ I) =
      1),
  ∃! ε : S, ε ∈ I ∧ P.HasMap (x + ε)
Tactic: obtain ⟨a, rfl⟩ := Ideal.Quotient.mk_surjective a
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : HPow.hPow (β := ℕ) I 2 = ⊥
x : S
hx : P.HasMap (S := S ⧸ I) ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) x : S ⧸ I)
hf : Membership.mem (α := S) I ((aeval x : (a : R[X]) → S) P.f : S)
a : S
ha :
  HMul.hMul (α := S ⧸ I) (β := S ⧸ I)
      (((aeval ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) x) : AlgHom.{u_1, u_1, u_2} R R[X] (S ⧸ I)) :
            (a : R[X]) → S ⧸ I)
          P.g :
        S ⧸ I)
      ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) a : S ⧸ I) =
    1
⊢ ∃! ε : S, ε ∈ I ∧ P.HasMap (x + ε)
have ha₁ : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.g : S) a - 1 ∈ I
Tactic: simp_rw [← Ideal.Quotient.mkₐ_eq_mk R, aeval_algHom_apply, ← map_mul, ← map_one
    (Ideal.Quotient.mkₐ R I), Ideal.Quotient.mkₐ_eq_mk, Ideal.Quotient.mk_eq_mk_iff_sub_mem] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : HPow.hPow (β := ℕ) I 2 = ⊥
x : S
hx : P.HasMap (S := S ⧸ I) ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) x : S ⧸ I)
hf : Membership.mem (α := S) I ((aeval x : (a : R[X]) → S) P.f : S)
a : S
ha : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.g : S) a - 1 ∈ I
⊢ ∃! ε : S, ε ∈ I ∧ P.HasMap (x + ε)
have obtain : ∀ (p₁ p₂ : R[X]) (n : ℕ)
  (e : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) P.f : R[X]) p₁ + P.f * p₂ = P.g ^ n),
  ∃! ε : S, ε ∈ I ∧ P.HasMap (x + ε)
Tactic: obtain ⟨p₁, p₂, n, e⟩ := P.cond
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : HPow.hPow (β := ℕ) I 2 = ⊥
x : S
hx : P.HasMap (S := S ⧸ I) ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) x : S ⧸ I)
hf : Membership.mem (α := S) I ((aeval x : (a : R[X]) → S) P.f : S)
a : S
ha : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.g : S) a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) P.f : R[X]) p₁ + P.f * p₂ = P.g ^ n
⊢ ∃! ε : S, ε ∈ I ∧ P.HasMap (x + ε)
have e₁ : Eq.{u_2 + 1} (α := S)
  ((aeval x : (a : R[X]) → S) (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) P.f : R[X]) p₁ + P.f * p₂) : S)
  ((aeval x : (a : R[X]) → S) (P.g ^ n) : S)
Tactic: apply_fun aeval x at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : HPow.hPow (β := ℕ) I 2 = ⊥
x : S
hx : P.HasMap (S := S ⧸ I) ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) x : S ⧸ I)
hf : Membership.mem (α := S) I ((aeval x : (a : R[X]) → S) P.f : S)
a : S
ha : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.g : S) a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e :
  Eq.{u_2 + 1} (α := S)
    ((aeval x : (a : R[X]) → S) (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) P.f : R[X]) p₁ + P.f * p₂) : S)
    ((aeval x : (a : R[X]) → S) (P.g ^ n) : S)
⊢ ∃! ε : S, ε ∈ I ∧ P.HasMap (x + ε)
have e₁ : HMul.hMul (α := S) (β := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P.f : R[X]) : S)
      ((aeval x : (a : R[X]) → S) p₁ : S) +
    HMul.hMul (α := S) (β := S) ((aeval x : (a : R[X]) → S) P.f : S) ((aeval x : (a : R[X]) → S) p₂ : S) =
  HPow.hPow (α := S) ((aeval x : (a : R[X]) → S) P.g : S) n
Tactic: simp only [map_add, map_mul, map_pow] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : HPow.hPow (β := ℕ) I 2 = ⊥
x : S
hx : P.HasMap (S := S ⧸ I) ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) x : S ⧸ I)
hf : Membership.mem (α := S) I ((aeval x : (a : R[X]) → S) P.f : S)
a : S
ha : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.g : S) a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e :
  HMul.hMul (α := S) (β := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P.f : R[X]) : S)
        ((aeval x : (a : R[X]) → S) p₁ : S) +
      HMul.hMul (α := S) (β := S) ((aeval x : (a : R[X]) → S) P.f : S) ((aeval x : (a : R[X]) → S) p₂ : S) =
    HPow.hPow (α := S) ((aeval x : (a : R[X]) → S) P.g : S) n
⊢ ∃ ε ∈ I,
    ∃ (b : S),
      HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P.f : R[X]) : S) b = 1 + ε
have refine : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P.f : R[X]) : S)
      (HMul.hMul (β := S) (a ^ n) ((aeval x : (a : R[X]) → S) p₁ : S)) -
    1 ∈
  I
Tactic: refine ⟨_, ?_, (a ^ n * aeval x p₁), sub_eq_iff_eq_add'.mp rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : HPow.hPow (β := ℕ) I 2 = ⊥
x : S
hx : P.HasMap (S := S ⧸ I) ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) x : S ⧸ I)
hf : Membership.mem (α := S) I ((aeval x : (a : R[X]) → S) P.f : S)
a : S
ha : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.g : S) a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e :
  HMul.hMul (α := S) (β := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P.f : R[X]) : S)
        ((aeval x : (a : R[X]) → S) p₁ : S) +
      HMul.hMul (α := S) (β := S) ((aeval x : (a : R[X]) → S) P.f : S) ((aeval x : (a : R[X]) → S) p₂ : S) =
    HPow.hPow (α := S) ((aeval x : (a : R[X]) → S) P.g : S) n
⊢ HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P.f : R[X]) : S)
        (HMul.hMul (β := S) (a ^ n) ((aeval x : (a : R[X]) → S) p₁ : S)) -
      1 ∈
    I
have h : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P.f : R[X]) : S)
      (HMul.hMul (β := S) (a ^ n) ((aeval x : (a : R[X]) → S) p₁ : S)) -
    1 =
  HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.g : S) a ^ n - 1 -
    HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.f : S)
      (HMul.hMul (β := S) (a ^ n) ((aeval x : (a : R[X]) → S) p₂ : S))
Tactic: convert_to (aeval x P.g * a) ^ n - 1 - aeval x P.f * (a ^ n * aeval x p₂) ∈ I
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : HPow.hPow (β := ℕ) I 2 = ⊥
x : S
hx : P.HasMap (S := S ⧸ I) ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) x : S ⧸ I)
hf : Membership.mem (α := S) I ((aeval x : (a : R[X]) → S) P.f : S)
a : S
ha : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.g : S) a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e :
  HMul.hMul (α := S) (β := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P.f : R[X]) : S)
        ((aeval x : (a : R[X]) → S) p₁ : S) +
      HMul.hMul (α := S) (β := S) ((aeval x : (a : R[X]) → S) P.f : S) ((aeval x : (a : R[X]) → S) p₂ : S) =
    HPow.hPow (α := S) ((aeval x : (a : R[X]) → S) P.g : S) n
h :
  HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P.f : R[X]) : S)
        (HMul.hMul (β := S) (a ^ n) ((aeval x : (a : R[X]) → S) p₁ : S)) -
      1 =
    HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.g : S) a ^ n - 1 -
      HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.f : S)
        (HMul.hMul (β := S) (a ^ n) ((aeval x : (a : R[X]) → S) p₂ : S))
⊢ HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P.f : R[X]) : S)
        (HMul.hMul (β := S) (a ^ n) ((aeval x : (a : R[X]) → S) p₁ : S)) -
      1 ∈
    I
have convert_to : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.g : S) a ^ n - 1 -
    HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.f : S)
      (HMul.hMul (β := S) (a ^ n) ((aeval x : (a : R[X]) → S) p₂ : S)) ∈
  I
Tactic: convert_to (aeval x P.g * a) ^ n - 1 - aeval x P.f * (a ^ n * aeval x p₂) ∈ I
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : HPow.hPow (β := ℕ) I 2 = ⊥
x : S
hx : P.HasMap (S := S ⧸ I) ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) x : S ⧸ I)
hf : Membership.mem (α := S) I ((aeval x : (a : R[X]) → S) P.f : S)
a : S
ha : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.g : S) a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e :
  HMul.hMul (α := S) (β := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P.f : R[X]) : S)
        ((aeval x : (a : R[X]) → S) p₁ : S) +
      HMul.hMul (α := S) (β := S) ((aeval x : (a : R[X]) → S) P.f : S) ((aeval x : (a : R[X]) → S) p₂ : S) =
    HPow.hPow (α := S) ((aeval x : (a : R[X]) → S) P.g : S) n
⊢ ∃! ε : S, ε ∈ I ∧ P.HasMap (x + ε)
have obtain : ∀ (ε : S) (hεI : ε ∈ I) (b : S)
  (hb : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P.f : R[X]) : S) b = 1 + ε),
  ∃! ε : S, ε ∈ I ∧ P.HasMap (x + ε)
Tactic: obtain ⟨ε, hεI, b, hb⟩ : ∃ ε ∈ I, ∃ b, aeval x (derivative P.f) * b = 1 + ε := by
    refine ⟨_, ?_, (a ^ n * aeval x p₁), sub_eq_iff_eq_add'.mp rfl⟩
    convert_to (aeval x P.g * a) ^ n - 1 - aeval x P.f * (a ^ n * aeval x p₂) ∈ I
    · linear_combination a ^ n * e
    · exact sub_mem (Ideal.mem_of_dvd _ (sub_one_dvd_pow_sub_one _ _) ha) (I.mul_mem_right _ hf)
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : HPow.hPow (β := ℕ) I 2 = ⊥
x : S
hx : P.HasMap (S := S ⧸ I) ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) x : S ⧸ I)
hf : Membership.mem (α := S) I ((aeval x : (a : R[X]) → S) P.f : S)
a : S
ha : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.g : S) a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e :
  HMul.hMul (α := S) (β := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P.f : R[X]) : S)
        ((aeval x : (a : R[X]) → S) p₁ : S) +
      HMul.hMul (α := S) (β := S) ((aeval x : (a : R[X]) → S) P.f : S) ((aeval x : (a : R[X]) → S) p₂ : S) =
    HPow.hPow (α := S) ((aeval x : (a : R[X]) → S) P.g : S) n
ε : S
hεI : ε ∈ I
b : S
hb : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P.f : R[X]) : S) b = 1 + ε
⊢ ∃! ε : S, ε ∈ I ∧ P.HasMap (x + ε)
have this : HPow.hPow (α := S) (β := ℕ) ((aeval x : (a : R[X]) → S) P.f : S) 2 = 0
Tactic: have : aeval x P.f ^ 2 = 0 := hI.le (Ideal.pow_mem_pow hf 2)