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
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:
exact 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
-- 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
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 + ε)
⊢ ∃! ε : 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)

Premises used: Polynomial.derivative, StandardEtalePair.f, 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
ε : 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 + ε
⊢ 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)
-- 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
ε : 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 + ε
this : HPow.hPow (α := S) (β := ℕ) ((aeval x : (a : R[X]) → S) P.f : S) 2 = 0
⊢ HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.f : S) ε = 0

Tactic:
have : aeval x P.f * ε = 0 := ((pow_two _).symm.trans hI).le (Ideal.mul_mem_mul hf hεI)
-- 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
ε : 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 + ε
this_1 : HPow.hPow (α := S) (β := ℕ) ((aeval x : (a : R[X]) → S) P.f : S) 2 = 0
this : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.f : S) ε = 0
⊢ ∃! ε : S, ε ∈ I ∧ P.HasMap (x + ε)

Tactic:
⟨aeval x P.f * -b, ⟨I.mul_mem_right _ hf, ?_, ?_⟩, ?_⟩

Premises used: HMul.hMul, StandardEtalePair.f, ExistsUnique, Ideal.mul_mem_right, And.intro, Exists.intro, Polynomial.aeval, DFunLike.coe, Neg.neg
-- 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
ε : 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 + ε
this_1 : HPow.hPow (α := S) (β := ℕ) ((aeval x : (a : R[X]) → S) P.f : S) 2 = 0
this : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.f : S) ε = 0
refine_1 :
  Eq.{u_2 + 1} (α := S)
    ((aeval (x + HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.f : S) (-b)) : (a : R[X]) → S) P.f : S) (0 : S)
refine_2 :
  IsUnit.{u_2} (M := S)
    ((aeval (x + HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.f : S) (-b)) : (a : R[X]) → S) P.g : S)
refine_3 :
  ∀ (y : S),
    (fun (ε : S) ↦ ε ∈ I ∧ P.HasMap (x + ε)) y → y = HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.f : S) (-b)
⊢ ∃! ε : S, ε ∈ I ∧ P.HasMap (x + ε)

Tactic:
refine ⟨aeval x P.f * -b, ⟨I.mul_mem_right _ hf, ?_, ?_⟩, ?_⟩
-- 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
ε : 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 + ε
this_1 : HPow.hPow (α := S) (β := ℕ) ((aeval x : (a : R[X]) → S) P.f : S) 2 = 0
this : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.f : S) ε = 0
⊢ HPow.hPow (β := ℕ) (HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.f : S) (-b)) 2 = 0

Tactic:
grind
-- 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
ε : 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 + ε
this_1 : HPow.hPow (α := S) (β := ℕ) ((aeval x : (a : R[X]) → S) P.f : S) 2 = 0
this : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.f : S) ε = 0
refine_1 :
  HAdd.hAdd (α := S) ((aeval x : (a : R[X]) → S) P.f : S)
      (HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P.f : R[X]) : S)
        (HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.f : S) (-b))) =
    0
⊢ Eq.{u_2 + 1} (α := S)
    ((aeval (x + HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.f : S) (-b)) : (a : R[X]) → S) P.f : S) (0 : S)

Tactic:
rw [Polynomial.aeval_add_of_sq_eq_zero _ _ _ (by grind)]

Premises used: Polynomial.aeval_add_of_sq_eq_zero
-- 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
ε : 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 + ε
this_1 : HPow.hPow (α := S) (β := ℕ) ((aeval x : (a : R[X]) → S) P.f : S) 2 = 0
this : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.f : S) ε = 0
⊢ HAdd.hAdd (α := S) ((aeval x : (a : R[X]) → S) P.f : S)
      (HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P.f : R[X]) : S)
        (HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.f : S) (-b))) =
    0

Tactic:
grind
-- 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
ε : 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 + ε
this_1 : HPow.hPow (α := S) (β := ℕ) ((aeval x : (a : R[X]) → S) P.f : S) 2 = 0
this : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.f : S) ε = 0
refine_2 :
  IsUnit.{u_2} (M := 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)
⊢ IsUnit.{u_2} (M := S)
    ((aeval (x + HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.f : S) (-b)) : (a : R[X]) → S) P.g : S)

Tactic:
rw [← IsNilpotent.isUnit_quotient_mk_iff (I := I) ⟨2, hI⟩, ← Ideal.Quotient.mkₐ_eq_mk R,
      ← aeval_algHom_apply, Ideal.Quotient.mkₐ_eq_mk, map_add,
      Ideal.Quotient.eq_zero_iff_mem.mpr (I.mul_mem_right _ hf), add_zero]

Premises used: Iff.mpr, map_add, Ideal.Quotient.eq_zero_iff_mem, Ideal.Quotient.mkₐ_eq_mk, Ideal.mul_mem_right, Exists.intro, add_zero, Polynomial.aeval_algHom_apply, OfNat.ofNat, IsNilpotent.isUnit_quotient_mk_iff
-- 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
ε : 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 + ε
this_1 : HPow.hPow (α := S) (β := ℕ) ((aeval x : (a : R[X]) → S) P.f : S) 2 = 0
this : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.f : S) ε = 0
⊢ IsUnit.{u_2} (M := 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)

Tactic:
hx.2

Premises used: And.right
-- 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
ε : 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 + ε
this_1 : HPow.hPow (α := S) (β := ℕ) ((aeval x : (a : R[X]) → S) P.f : S) 2 = 0
this : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.f : S) ε = 0
⊢ IsUnit.{u_2} (M := 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)

Tactic:
exact hx.2

Premises used: And.right
-- 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
ε : 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 + ε
this_1 : HPow.hPow (α := S) (β := ℕ) ((aeval x : (a : R[X]) → S) P.f : S) 2 = 0
this : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.f : S) ε = 0
ε' : S
hε'I : ε' ∈ I
hε' : Eq.{u_2 + 1} (α := S) ((aeval (x + ε') : (a : R[X]) → S) P.f : S) (0 : S)
hε'' : IsUnit.{u_2} (M := S) ((aeval (x + ε') : (a : R[X]) → S) P.g : S)
⊢ HAdd.hAdd (α := S) ((aeval x : (a : R[X]) → S) P.f : S)
      (HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P.f : R[X]) : S) ε') =
    0

Tactic:
rw [Polynomial.aeval_add_of_sq_eq_zero _ _ _ (hI.le (Ideal.pow_mem_pow hε'I 2))] at hε'

Premises used: Polynomial.aeval_add_of_sq_eq_zero, Eq.le, Ideal.pow_mem_pow, OfNat.ofNat
-- 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
ε : 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 + ε
this_1 : HPow.hPow (α := S) (β := ℕ) ((aeval x : (a : R[X]) → S) P.f : S) 2 = 0
this : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.f : S) ε = 0
ε' : S
hε'I : ε' ∈ I
hε' : Eq.{u_2 + 1} (α := S) ((aeval (x + ε') : (a : R[X]) → S) P.f : S) (0 : S)
hε'' : IsUnit.{u_2} (M := S) ((aeval (x + ε') : (a : R[X]) → S) P.g : S)
hε'₁ :
  HAdd.hAdd (α := S) ((aeval x : (a : R[X]) → S) P.f : S)
      (HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P.f : R[X]) : S) ε') =
    0
⊢ IsUnit.{u_2} (M := S) ((aeval (x + ε') : (a : R[X]) → S) P.g : S)

Tactic:
rw [Polynomial.aeval_add_of_sq_eq_zero _ _ _ (hI.le (Ideal.pow_mem_pow hε'I 2))] at hε'

Premises used: Polynomial.aeval_add_of_sq_eq_zero, Eq.le, Ideal.pow_mem_pow, OfNat.ofNat
-- 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
ε : 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 + ε
this_1 : HPow.hPow (α := S) (β := ℕ) ((aeval x : (a : R[X]) → S) P.f : S) 2 = 0
this : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.f : S) ε = 0
ε' : S
hε'I : ε' ∈ I
hε' :
  HAdd.hAdd (α := S) ((aeval x : (a : R[X]) → S) P.f : S)
      (HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P.f : R[X]) : S) ε') =
    0
hε'' : IsUnit.{u_2} (M := S) ((aeval (x + ε') : (a : R[X]) → S) P.g : S)
⊢ ε * ε' = 0

Tactic:
have : ε * ε' = 0 := ((pow_two _).symm.trans hI).le (Ideal.mul_mem_mul hεI hε'I)
-- 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
ε : 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 + ε
this_1 : HPow.hPow (α := S) (β := ℕ) ((aeval x : (a : R[X]) → S) P.f : S) 2 = 0
this_2 : HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.f : S) ε = 0
ε' : S
hε'I : ε' ∈ I
hε' :
  HAdd.hAdd (α := S) ((aeval x : (a : R[X]) → S) P.f : S)
      (HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P.f : R[X]) : S) ε') =
    0
hε'' : IsUnit.{u_2} (M := S) ((aeval (x + ε') : (a : R[X]) → S) P.g : S)
this : ε * ε' = 0
⊢ ε' = HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.f : S) (-b)

Tactic:
grind
-- 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
⊢ Algebra.FormallyEtale R P.Ring

Tactic:
Algebra.FormallyEtale.iff_comp_bijective.mpr fun S _ _ I hI ↦ ?_

Premises used: Iff.mpr, Algebra.FormallyEtale.iff_comp_bijective
-- 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
refine :
  ∀ (S : Type u_1) (x : CommRing S) (x_1 : Algebra R S) (I : Ideal S) (hI : HPow.hPow (β := ℕ) I 2 = ⊥),
    Function.Bijective (α := P.Ring →ₐ[R] S) (β := P.Ring →ₐ[R] S ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
⊢ Algebra.FormallyEtale R P.Ring

Tactic:
refine Algebra.FormallyEtale.iff_comp_bijective.mpr fun S _ _ I hI ↦ ?_

Premises used: Iff.mpr, Algebra.FormallyEtale.iff_comp_bijective