awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 + ε
this : HPow.hPow (α := S) (β := ℕ) ((aeval x : (a : R[X]) → S) P.f : S) 2 = 0
⊢ ∃! ε : S, ε ∈ I ∧ P.HasMap (x + ε)
have this₁ : 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)
-- 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
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 + ε)
have 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)
Tactic: refine ⟨aeval x P.f * -b, ⟨I.mul_mem_right _ hf, ?_, ?_⟩, ?_⟩
-- 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
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)
⊢ ∃! ε : S, ε ∈ I ∧ P.HasMap (x + ε)
have 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)
Tactic: refine ⟨aeval x P.f * -b, ⟨I.mul_mem_right _ hf, ?_, ?_⟩, ?_⟩
-- 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
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)
⊢ ∃! ε : S, ε ∈ I ∧ P.HasMap (x + ε)
have 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)
Tactic: refine ⟨aeval x P.f * -b, ⟨I.mul_mem_right _ hf, ?_, ?_⟩, ?_⟩
-- 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
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
⊢ 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)
have 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
Tactic: rw [Polynomial.aeval_add_of_sq_eq_zero _ _ _ (by grind)]
-- 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
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)
    ((aeval (x + HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.f : S) (-b)) : (a : R[X]) → S) P.g : S)
have 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)
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]
-- 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 + ε
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)
⊢ ε' = HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.f : S) (-b)
have 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
Tactic: rw [Polynomial.aeval_add_of_sq_eq_zero _ _ _ (hI.le (Ideal.pow_mem_pow hε'I 2))] at hε'
Cleared hypotheses: hε', hε''
-- 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 + ε
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)
⊢ ε' = HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) P.f : S) (-b)
have this₁ : ε * ε' = 0
Tactic: have : ε * ε' = 0 := ((pow_two _).symm.trans hI).le (Ideal.mul_mem_mul hεI hε'I)
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
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
have 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))
Tactic: refine Algebra.FormallyEtale.iff_comp_bijective.mpr fun S _ _ I hI ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
S_1 : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S_1
inst_2 : CommRing T
inst_3 : Algebra R S_1
inst_4 : Algebra R T
P : StandardEtalePair R
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))
have rw : Function.Bijective (α := { x_2 : S // P.HasMap x_2 }) (β := { x_2 : S ⧸ I // P.HasMap x_2 })
  (Function.comp (β := P.Ring →ₐ[R] S ⧸ I) (⇑P.homEquiv : (a : P.Ring →ₐ[R] S ⧸ I) → { x_2 : S ⧸ I // P.HasMap x_2 })
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) ∘
      (⇑(Equiv.symm P.homEquiv) : (a : { x_2 : S // P.HasMap x_2 }) → P.Ring →ₐ[R] S)))
Tactic: rw [← P.homEquiv.symm.bijective.of_comp_iff, ← P.homEquiv.bijective.of_comp_iff']
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
S_1 : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S_1
inst_2 : CommRing T
inst_3 : Algebra R S_1
inst_4 : Algebra R T
P : StandardEtalePair R
S : Type u_1
x : CommRing S
x_1 : Algebra R S
I : Ideal S
hI : HPow.hPow (β := ℕ) I 2 = ⊥
⊢ Function.Bijective (α := { x_2 : S // P.HasMap x_2 }) (β := { x_2 : S ⧸ I // P.HasMap x_2 })
    (Function.comp (β := P.Ring →ₐ[R] S ⧸ I) (⇑P.homEquiv : (a : P.Ring →ₐ[R] S ⧸ I) → { x_2 : S ⧸ I // P.HasMap x_2 })
      (AlgHom.comp (Ideal.Quotient.mkₐ R I) ∘
        (⇑(Equiv.symm P.homEquiv) : (a : { x_2 : S // P.HasMap x_2 }) → P.Ring →ₐ[R] S)))
have suffices : ∀ (x_2 : S),
  P.HasMap (S := S ⧸ I) ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) x_2 : S ⧸ I) →
    ∃! a : { x_3 : S // P.HasMap x_3 }, (↑a : S) - x_2 ∈ I
Tactic: suffices ∀ x, P.HasMap (Ideal.Quotient.mk I x) → ∃! a : { x : S // P.HasMap x }, a - x ∈ I by
    simpa [Function.bijective_iff_existsUnique, Ideal.Quotient.mk_surjective.forall,
      Subtype.ext_iff, Ideal.Quotient.mk_eq_mk_iff_sub_mem]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
S_1 : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S_1
inst_2 : CommRing T
inst_3 : Algebra R S_1
inst_4 : Algebra R T
P : StandardEtalePair R
S : Type u_1
x_1 : CommRing S
x_2 : Algebra R S
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)
⊢ ∃! a : { x : S // P.HasMap x }, (↑a : S) - x ∈ I
have obtain : ∀ (ε : S) (H : ∀ (y : S), (fun (ε : S) ↦ ε ∈ I ∧ P.HasMap (x + ε)) y → y = ε) (hεI : ε ∈ I) (hε : P.HasMap (x + ε)),
  ∃! a : { x : S // P.HasMap x }, (↑a : S) - x ∈ I
Tactic: obtain ⟨ε, ⟨hεI, hε⟩, H⟩ := P.existsUnique_hasMap_of_hasMap_quotient_of_sq_eq_bot I hI _ hx
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
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
⊢ P.Ring ≃ₐ[R]
    Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)
have refine_1 : Eq (α :=
  Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
  (((aeval
            ((algebraMap (AdjoinRoot P.f)
                  (Localization.Away (M := AdjoinRoot P.f)
                    ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)) :
                (a : AdjoinRoot P.f) → Localization.Away ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g))
              (AdjoinRoot.root P.f)) :
          R[X] →ₐ[R]
            Localization.Away (M := AdjoinRoot P.f)
              ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)) :
        (a : R[X]) → Localization.Away ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g))
      P.f :
    Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
  (0 : Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
Tactic: refine .ofAlgHom (P.lift (algebraMap (AdjoinRoot P.f) _ (.root P.f)) ⟨?_, ?_⟩)
    (IsLocalization.liftAlgHom (M := .powers <| AdjoinRoot.mk P.f P.g)
      (f := AdjoinRoot.liftAlgHom _ _ P.X P.hasMap_X.1) <| Subtype.forall.mpr ?_) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
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_1 :
  Eq (α :=
    Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
    (((aeval
              ((algebraMap (AdjoinRoot P.f)
                    (Localization.Away (M := AdjoinRoot P.f)
                      ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)) :
                  (a : AdjoinRoot P.f) → Localization.Away ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g))
                (AdjoinRoot.root P.f)) :
            R[X] →ₐ[R]
              Localization.Away (M := AdjoinRoot P.f)
                ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)) :
          (a : R[X]) → Localization.Away ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g))
        P.f :
      Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
    (0 :
      Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
⊢ P.Ring ≃ₐ[R]
    Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)
have refine_2 : IsUnit (M :=
  Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
  (((aeval
            ((algebraMap (AdjoinRoot P.f)
                  (Localization.Away (M := AdjoinRoot P.f)
                    ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)) :
                (a : AdjoinRoot P.f) → Localization.Away ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g))
              (AdjoinRoot.root P.f)) :
          R[X] →ₐ[R]
            Localization.Away (M := AdjoinRoot P.f)
              ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)) :
        (a : R[X]) → Localization.Away ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g))
      P.g :
    Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
Tactic: refine .ofAlgHom (P.lift (algebraMap (AdjoinRoot P.f) _ (.root P.f)) ⟨?_, ?_⟩)
    (IsLocalization.liftAlgHom (M := .powers <| AdjoinRoot.mk P.f P.g)
      (f := AdjoinRoot.liftAlgHom _ _ P.X P.hasMap_X.1) <| Subtype.forall.mpr ?_) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
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
⊢ Eq (α :=
    Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
    (((aeval
              ((algebraMap (AdjoinRoot P.f)
                    (Localization.Away (M := AdjoinRoot P.f)
                      ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)) :
                  (a : AdjoinRoot P.f) → Localization.Away ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g))
                (AdjoinRoot.root P.f)) :
            R[X] →ₐ[R]
              Localization.Away (M := AdjoinRoot P.f)
                ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)) :
          (a : R[X]) → Localization.Away ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g))
        P.f :
      Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
    (0 :
      Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
have refine_1 : Eq (α :=
  Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
  ((algebraMap (AdjoinRoot P.f)
        (Localization.Away (M := AdjoinRoot P.f)
          ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)) :
      (a : AdjoinRoot P.f) → Localization.Away ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g))
    ((aeval (AdjoinRoot.root P.f) : (a : R[X]) → AdjoinRoot P.f) P.f))
  0
Tactic: rw [aeval_algebraMap_apply, AdjoinRoot.aeval_eq, AdjoinRoot.mk_self, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
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_1 :
  Eq (α :=
    Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
    ((algebraMap (AdjoinRoot P.f)
          (Localization.Away (M := AdjoinRoot P.f)
            ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)) :
        (a : AdjoinRoot P.f) → Localization.Away ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g))
      ((aeval (AdjoinRoot.root P.f) : (a : R[X]) → AdjoinRoot P.f) P.f))
    0
⊢ Eq (α :=
    Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
    (((aeval
              ((algebraMap (AdjoinRoot P.f)
                    (Localization.Away (M := AdjoinRoot P.f)
                      ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)) :
                  (a : AdjoinRoot P.f) → Localization.Away ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g))
                (AdjoinRoot.root P.f)) :
            R[X] →ₐ[R]
              Localization.Away (M := AdjoinRoot P.f)
                ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)) :
          (a : R[X]) → Localization.Away ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g))
        P.f :
      Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
    (0 :
      Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
have refine_1₁ : Eq (α :=
  Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
  ((algebraMap (AdjoinRoot P.f)
        (Localization.Away (M := AdjoinRoot P.f)
          ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)) :
      (a : AdjoinRoot P.f) → Localization.Away ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g))
    ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.f))
  0
Tactic: rw [aeval_algebraMap_apply, AdjoinRoot.aeval_eq, AdjoinRoot.mk_self, map_zero]