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
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
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
⊢ 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.{u_1 + 1} (α :=
  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))
    0)
  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
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
refine_1₂ :
  Eq.{u_1 + 1} (α :=
    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))
      0)
    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.{u_1 + 1} (α :=
  Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)) 0 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
⊢ 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))
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))
  ((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.g) :
    Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
Tactic: rw [aeval_algebraMap_apply, AdjoinRoot.aeval_eq]
-- 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
⊢ AlgHom.comp (B :=
      Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
      (IsLocalization.liftAlgHom (R := AdjoinRoot P.f) (M :=
          Submonoid.powers ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g)) (f :=
          AdjoinRoot.liftAlgHom P.f (Algebra.ofId R P.Ring) P.X ⋯) ⋯ :
        Localization.Away (M := AdjoinRoot P.f)
            ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f) →ₐ[R]
          P.Ring)
      (P.lift
          ((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))
          ⋯ :
        P.Ring →ₐ[R]
          Localization.Away (M := AdjoinRoot P.f)
            ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)) =
    AlgHom.id R P.Ring
have refine_5 : Eq (α := P.Ring)
  ((AlgHom.comp (B :=
          Localization.Away (M := AdjoinRoot P.f)
            ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
          (IsLocalization.liftAlgHom (R := AdjoinRoot P.f) (M :=
              Submonoid.powers ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g)) (f :=
              AdjoinRoot.liftAlgHom P.f (Algebra.ofId R P.Ring) P.X sorry) sorry :
            Localization.Away (M := AdjoinRoot P.f)
                ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f) →ₐ[R]
              P.Ring)
          (P.lift
              ((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))
              sorry :
            P.Ring →ₐ[R]
              Localization.Away (M := AdjoinRoot P.f)
                ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)) :
        (a : P.Ring) → P.Ring)
      P.X :
    P.Ring)
  ((AlgHom.id R P.Ring : (a : P.Ring) → P.Ring) P.X : P.Ring)
Tactic: ext
-- 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]
    HasQuotient.Quotient (Localization.Away P.g) (B := Ideal (Localization.Away P.g))
      (Ideal.span
        (singleton (α := Localization.Away P.g)
          ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f : Localization.Away P.g)))
have refine_1 : Eq (α :=
  HasQuotient.Quotient (Localization.Away P.g) (B := Ideal (Localization.Away P.g))
    (Ideal.span
      (singleton (α := Localization.Away P.g)
        ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f : Localization.Away P.g))))
  (((aeval
            ((algebraMap R[X]
                  (HasQuotient.Quotient (Localization.Away P.g) (B := Ideal (Localization.Away P.g))
                    (Ideal.span
                      (singleton (α := Localization.Away P.g)
                        ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
                          Localization.Away P.g)))) :
                (a : R[X]) →
                  Localization.Away P.g ⧸
                    Ideal.span {(algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f})
              X) :
          R[X] →ₐ[R]
            HasQuotient.Quotient (Localization.Away P.g) (B := Ideal (Localization.Away P.g))
              (Ideal.span
                (singleton (α := Localization.Away P.g)
                  ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
                    Localization.Away P.g)))) :
        (a : R[X]) →
          Localization.Away P.g ⧸
            Ideal.span {(algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f})
      P.f :
    HasQuotient.Quotient (Localization.Away P.g) (B := Ideal (Localization.Away P.g))
      (Ideal.span
        (singleton (α := Localization.Away P.g)
          ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
            Localization.Away P.g))))
  (0 :
    HasQuotient.Quotient (Localization.Away P.g) (B := Ideal (Localization.Away P.g))
      (Ideal.span
        (singleton (α := Localization.Away P.g)
          ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
            Localization.Away P.g))))
Tactic: refine .ofAlgHom (P.lift (algebraMap R[X] _ .X) ⟨?_, ?_⟩)
    (Ideal.Quotient.liftₐ _ (IsLocalization.liftAlgHom (M := .powers <| P.g)
      (f := aeval P.X) <| 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 (α := P.Ring →ₐ[R] P.Ring)
    (AlgHom.comp (B :=
      HasQuotient.Quotient (Localization.Away P.g) (B := Ideal (Localization.Away P.g))
        (Ideal.span
          (singleton (α := Localization.Away P.g)
            ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
              Localization.Away P.g))))
      (Ideal.Quotient.liftₐ
        (Ideal.span
          (singleton (α := Localization.Away P.g)
            ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
              Localization.Away P.g)))
        (IsLocalization.liftAlgHom (R := R[X]) (M := Submonoid.powers P.g) (f := aeval P.X) ⋯) ⋯)
      (P.lift
        ((algebraMap R[X]
              (HasQuotient.Quotient (Localization.Away P.g) (B := Ideal (Localization.Away P.g))
                (Ideal.span
                  (singleton (α := Localization.Away P.g)
                    ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
                      Localization.Away P.g)))) :
            (a : R[X]) →
              Localization.Away P.g ⧸
                Ideal.span {(algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f})
          X)
        ⋯))
    (AlgHom.id R P.Ring)
have refine_6 : Eq (α := P.Ring)
  ((AlgHom.comp (B :=
          HasQuotient.Quotient (Localization.Away P.g) (B := Ideal (Localization.Away P.g))
            (Ideal.span
              (singleton (α := Localization.Away P.g)
                ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
                  Localization.Away P.g))))
          (Ideal.Quotient.liftₐ
            (Ideal.span
              (singleton (α := Localization.Away P.g)
                ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
                  Localization.Away P.g)))
            (IsLocalization.liftAlgHom (R := R[X]) (M := Submonoid.powers P.g) (f := aeval P.X) sorry) sorry)
          (P.lift
            ((algebraMap R[X]
                  (HasQuotient.Quotient (Localization.Away P.g) (B := Ideal (Localization.Away P.g))
                    (Ideal.span
                      (singleton (α := Localization.Away P.g)
                        ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
                          Localization.Away P.g)))) :
                (a : R[X]) →
                  Localization.Away P.g ⧸
                    Ideal.span {(algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f})
              X)
            sorry) :
        (a : P.Ring) → P.Ring)
      P.X :
    P.Ring)
  ((AlgHom.id R P.Ring : (a : P.Ring) → P.Ring) P.X : P.Ring)
Tactic: ext
-- 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 (α := Ideal (MvPolynomial (Fin 2) R))
    (Ideal.span
      (insert (α := MvPolynomial (Fin 2) R)
        ((Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R) ((C : (a : R[X]) → R[X][Y]) P.f) :
          MvPolynomial (Fin 2) R)
        (singleton (α := MvPolynomial (Fin 2) R)
          ((Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
              (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1) :
            MvPolynomial (Fin 2) R))))
    (Ideal.map (R := R[X][Y]) (F := R[X][Y] →+* MvPolynomial (Fin 2) R)
      (↑(Bivariate.equivMvPolynomial R) : R[X][Y] →+* MvPolynomial (Fin 2) 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})))
have simp : Eq (α := Ideal (MvPolynomial (Fin 2) R))
  (Ideal.span
    (insert (α := MvPolynomial (Fin 2) R)
      ((Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R) ((C : (a : R[X]) → R[X][Y]) P.f) :
        MvPolynomial (Fin 2) R)
      (singleton (α := MvPolynomial (Fin 2) R)
        ((Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1) :
          MvPolynomial (Fin 2) R))))
  (Ideal.span
    (insert (α := MvPolynomial (Fin 2) R)
      (((↑(Bivariate.equivMvPolynomial R) : R[X][Y] →+* MvPolynomial (Fin 2) R) :
            (a : R[X][Y]) → MvPolynomial (Fin 2) R)
          ((C : (a : R[X]) → R[X][Y]) P.f) :
        MvPolynomial (Fin 2) R)
      (singleton (α := MvPolynomial (Fin 2) R)
        (((↑(Bivariate.equivMvPolynomial R) : R[X][Y] →+* MvPolynomial (Fin 2) R) :
              (a : R[X][Y]) → MvPolynomial (Fin 2) R)
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1) :
          MvPolynomial (Fin 2) R))))
Tactic: simp only [Ideal.map_span, Set.image_insert_eq, Set.image_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
inst : CommRing R
P : StandardEtalePair R
⊢ (P.equivMvPolynomialQuotient.symm :
        (a :
            MvPolynomial (Fin 2) R ⧸
              Ideal.span
                {(Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
                    ((C : (a : R[X]) → R[X][Y]) P.f),
                  (Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
                    (Y * (C : (a : R[X]) → R[X][Y]) P.g - 1)}) →
          P.Ring)
      ((Ideal.Quotient.mk
            (Ideal.span
              (insert (α := MvPolynomial (Fin 2) R)
                ((Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
                    ((C : (a : R[X]) → R[X][Y]) P.f) :
                  MvPolynomial (Fin 2) R)
                (singleton (α := MvPolynomial (Fin 2) R)
                  ((Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
                      (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1) :
                    MvPolynomial (Fin 2) R)))) :
          (a : MvPolynomial (Fin 2) R) →
            MvPolynomial (Fin 2) R ⧸
              Ideal.span
                {(Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
                    ((C : (a : R[X]) → R[X][Y]) P.f),
                  (Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
                    (Y * (C : (a : R[X]) → R[X][Y]) P.g - 1)})
        (MvPolynomial.X 0)) =
    P.X
have simp : (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})
    ((C : (a : R[X]) → R[X][Y]) X) =
  P.X
Tactic: simp [equivMvPolynomialQuotient, StandardEtalePair.Ring]
-- 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
f : R →+* S
⊢ ∃ (p₁ : S[X]) (p₂ : S[X]) (n : ℕ),
    HMul.hMul (α := S[X]) ((derivative : (a : S[X]) → S[X]) (map f P.f) : S[X]) p₁ + map f P.f * p₂ = map f P.g ^ n
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),
  ∃ (p₁ : S[X]) (p₂ : S[X]) (n : ℕ),
    HMul.hMul (α := S[X]) ((derivative : (a : S[X]) → S[X]) (map f P.f) : S[X]) p₁ + map f P.f * p₂ = map f P.g ^ n
Tactic: obtain ⟨p₁, p₂, n, e⟩ := P.cond
-- 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
f : R →+* S
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
⊢ ∃ (p₁ : S[X]) (p₂ : S[X]) (n : ℕ),
    HMul.hMul (α := S[X]) ((derivative : (a : S[X]) → S[X]) (map f P.f) : S[X]) p₁ + map f P.f * p₂ = map f P.g ^ n
have refine : HMul.hMul (α := S[X]) ((derivative : (a : S[X]) → S[X]) (map f P.f) : S[X]) (map f p₁) + map f P.f * map f p₂ =
  map f P.g ^ n
Tactic: refine ⟨p₁.map f, p₂.map f, n, ?_⟩
-- 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 : StandardEtalePresentation R S
p : R[X]
⊢ Eq.{u_2 + 1} (α := S)
    ((MvPolynomial.aeval P.toPresentation.val : (a : MvPolynomial (Fin 2) R) → S)
        ((Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R) ((C : (a : R[X]) → R[X][Y]) p) :
          MvPolynomial (Fin 2) R) :
      S)
    ((aeval P.x : (a : R[X]) → S) p : S)
have change : Eq.{u_2 + 1} (α := S)
  ((AlgHom.comp
          (AlgHom.comp (MvPolynomial.aeval P.toPresentation.val)
            (↑(Bivariate.equivMvPolynomial R) : R[X][Y] →ₐ[R] MvPolynomial (Fin 2) R))
          CAlgHom :
        (a : R[X]) → S)
      p :
    S)
  ((aeval P.x : (a : R[X]) → S) p : S)
Tactic: change (((MvPolynomial.aeval _).comp (Bivariate.equivMvPolynomial R).toAlgHom).comp CAlgHom) _ = _
-- 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 : StandardEtalePresentation R S
p : R[X]
⊢ Eq.{u_2 + 1} (α := S)
    ((AlgHom.comp
            (AlgHom.comp (MvPolynomial.aeval P.toPresentation.val)
              (↑(Bivariate.equivMvPolynomial R) : R[X][Y] →ₐ[R] MvPolynomial (Fin 2) R))
            CAlgHom :
          (a : R[X]) → S)
        p :
      S)
    ((aeval P.x : (a : R[X]) → S) p : S)
have e_a : Eq (α := R[X] →ₐ[R] S)
  (AlgHom.comp
    (AlgHom.comp (MvPolynomial.aeval P.toPresentation.val)
      (↑(Bivariate.equivMvPolynomial R) : R[X][Y] →ₐ[R] MvPolynomial (Fin 2) R))
    CAlgHom)
  (aeval P.x)
Tactic: congr 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 : StandardEtalePresentation R S
p : R[X]
⊢ Eq (α := R[X] →ₐ[R] S)
    (AlgHom.comp
      (AlgHom.comp (MvPolynomial.aeval P.toPresentation.val)
        (↑(Bivariate.equivMvPolynomial R) : R[X][Y] →ₐ[R] MvPolynomial (Fin 2) R))
      CAlgHom)
    (aeval P.x)
have e_a : Eq.{u_2 + 1} (α := S)
  ((AlgHom.comp
          (AlgHom.comp (MvPolynomial.aeval P.toPresentation.val)
            (↑(Bivariate.equivMvPolynomial R) : R[X][Y] →ₐ[R] MvPolynomial (Fin 2) R))
          CAlgHom :
        (a : R[X]) → S)
      X :
    S)
  ((aeval P.x : (a : R[X]) → S) X : S)
Tactic: ext