awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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)
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)
⊢ f = g

Tactic:
refine Ideal.Quotient.algHom_ext _ (Polynomial.algHom_ext' H ?_)

Premises used: Polynomial.algHom_ext', Ideal.Quotient.algHom_ext
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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)
rw :
  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)
⊢ 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)

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]

Premises used: Units.coe_map_inv, Iff.mp, StandardEtalePair.aeval_X_g_mul_mk_X, Units.mul_eq_one_iff_inv_eq
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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)
e_self :
  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ˣ)
⊢ 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)

Tactic:
congr 2
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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)
e_self :
  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)
⊢ 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ˣ)

Tactic:
ext
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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)

Tactic:
simpa [H'] using congr($H _)
-- Module: Mathlib.RingTheory.Etale.StandardEtale
Goal:
R : Type u_1
inst : CommRing R
P : StandardEtalePair R
⊢ Eq (α := P.Ring) ((P.lift P.X ⋯ : (a : P.Ring) → P.Ring) P.X : P.Ring)
    ((AlgHom.id R P.Ring : (a : P.Ring) → P.Ring) P.X : P.Ring)

Tactic:
simp
-- Module: Mathlib.RingTheory.Etale.StandardEtale
Goal:
R : Type u_1
inst : CommRing R
P : StandardEtalePair R
⊢ Eq.{u_1 + 1} (α := P.Ring) (↑(IsUnit.unit ⋯)⁻¹ : P.Ring)
    ((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)

Tactic:
Units.mul_eq_one_iff_inv_eq.mp P.aeval_X_g_mul_mk_X

Premises used: Iff.mp, StandardEtalePair.aeval_X_g_mul_mk_X, Units.mul_eq_one_iff_inv_eq
-- Module: Mathlib.RingTheory.Etale.StandardEtale
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
P : StandardEtalePair R
f : P.Ring →ₐ[R] S
⊢ Eq.{u_2 + 1} (α := S)
    (((fun (x : { x : S // P.HasMap x }) ↦ P.lift (↑x : S) ⋯)
            ((fun (f : P.Ring →ₐ[R] S) ↦
                (Subtype.mk (p := fun (x : S) ↦ P.HasMap x) ((f : (a : P.Ring) → S) P.X) ⋯ : { x : S // P.HasMap x }))
              f) :
          (a : P.Ring) → S)
        P.X :
      S)
    ((f : (a : P.Ring) → S) P.X : S)

Tactic:
simp
-- Module: Mathlib.RingTheory.Etale.StandardEtale
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
P : StandardEtalePair R
x : { x : S // P.HasMap x }
⊢ (fun (f : P.Ring →ₐ[R] S) ↦
        (Subtype.mk (p := fun (x : S) ↦ P.HasMap x) ((f : (a : P.Ring) → S) P.X) ⋯ : { x : S // P.HasMap x }))
      ((fun (x : { x : S // P.HasMap x }) ↦ P.lift (↑x : S) ⋯) x) =
    x

Tactic:
simp
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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)
⊢ 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)
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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)
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 + ε)
⊢ ∃! ε : S, ε ∈ I ∧ P.HasMap (x + ε)

Tactic:
obtain ⟨⟨_, a, ha, -⟩, rfl⟩ := hx.2

Premises used: And.right, rfl
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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
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 + ε)
⊢ ∃! ε : S, ε ∈ I ∧ P.HasMap (x + ε)

Tactic:
obtain ⟨a, rfl⟩ := Ideal.Quotient.mk_surjective a

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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
⊢ 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

Premises used: map_mul, map_one, Ideal.Quotient.mkₐ_eq_mk, Ideal.Quotient.mk_eq_mk_iff_sub_mem, Polynomial.aeval_algHom_apply, Ideal.Quotient.mkₐ
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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
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 + ε)
⊢ ∃! ε : S, ε ∈ I ∧ P.HasMap (x + ε)

Tactic:
obtain ⟨p₁, p₂, n, e⟩ := P.cond

Premises used: StandardEtalePair.cond
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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
⊢ 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

Premises used: Polynomial.aeval
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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)
⊢ 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

Premises used: map_add, map_pow, map_mul
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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 + ε

Tactic:
⟨_, ?_, (a ^ n * aeval x p₁), sub_eq_iff_eq_add'.mp rfl⟩

Premises used: HMul.hMul, HPow.hPow, And.intro, Exists.intro, Iff.mp, Polynomial.aeval, DFunLike.coe, sub_eq_iff_eq_add', rfl
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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
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
⊢ ∃ ε ∈ 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 + ε

Tactic:
refine ⟨_, ?_, (a ^ n * aeval x p₁), sub_eq_iff_eq_add'.mp rfl⟩
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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))
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
⊢ 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:
convert_to (aeval x P.g * a) ^ n - 1 - aeval x P.f * (a ^ n * aeval x p₂) ∈ I

Premises used: HMul.hMul, StandardEtalePair.f, HPow.hPow, StandardEtalePair.g, Polynomial.aeval, DFunLike.coe
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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 =
    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:
linear_combination a ^ n * e
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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) 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:
sub_mem (Ideal.mem_of_dvd _ (sub_one_dvd_pow_sub_one _ _) ha) (I.mul_mem_right _ hf)

Premises used: Ideal.mem_of_dvd, sub_mem, Ideal.mul_mem_right, sub_one_dvd_pow_sub_one