awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ LE.le (α := Submonoid R[X]) (Submonoid.powers P.g)
    (Submonoid.comap (F := R[X] →ₐ[R] P.Ring) (aeval P.X) (IsUnit.submonoid P.Ring))

Tactic:
simpa [Submonoid.powers_le, IsUnit.mem_submonoid_iff] using P.hasMap_X.2

Premises used: StandardEtalePair.hasMap_X, IsUnit.mem_submonoid_iff, And.right, Submonoid.powers_le
-- 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
⊢ LE.le (α := 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)))
    (RingHom.ker (F := Localization.Away P.g →ₐ[R] P.Ring)
      (IsLocalization.liftAlgHom (R := R[X]) (M := Submonoid.powers P.g) (f := aeval P.X) ⋯))

Tactic:
simpa [Ideal.span_le] using P.hasMap_X.1

Premises used: Ideal.span_le, StandardEtalePair.hasMap_X, And.left
-- 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_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) ⋯) ⋯)
            (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)
              ⋯) :
          (a : P.Ring) → P.Ring)
        P.X :
      P.Ring)
    ((AlgHom.id R P.Ring : (a : P.Ring) → P.Ring) P.X : P.Ring)
⊢ 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)

Tactic:
ext
-- 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
⊢ 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) ⋯) ⋯)
            (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)
              ⋯) :
          (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 [IsScalarTower.algebraMap_apply R[X] (Localization.Away P.g) (_ ⧸ _),
      -Ideal.Quotient.mk_algebraMap]

Premises used: Localization.Away, Polynomial, HasQuotient.Quotient, StandardEtalePair.g, IsScalarTower.algebraMap_apply, Ideal.Quotient.mk_algebraMap
-- 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
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))))
⊢ 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})))

Tactic:
simp only [Ideal.map_span, Set.image_insert_eq, Set.image_singleton]

Premises used: Set.image_singleton, Ideal.map_span, Set.image_insert_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
⊢ 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:
rfl
-- Module: Mathlib.RingTheory.Etale.StandardEtale
Goal:
R : Type u_1
inst : CommRing R
P : StandardEtalePair R
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
⊢ (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

Tactic:
simp [equivMvPolynomialQuotient, StandardEtalePair.Ring]

Premises used: StandardEtalePair.Ring, StandardEtalePair.equivMvPolynomialQuotient
-- Module: Mathlib.RingTheory.Etale.StandardEtale
Goal:
R : Type u_1
inst : CommRing R
P : StandardEtalePair R
⊢ (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:
rfl
-- 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 : R →+* S
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
⊢ ∃ (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

Premises used: StandardEtalePair.cond
-- 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 : 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

Tactic:
⟨p₁.map f, p₂.map f, n, ?_⟩

Premises used: Exists.intro, Polynomial.map
-- 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 : 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
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
⊢ ∃ (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:
refine ⟨p₁.map f, p₂.map f, n, ?_⟩
-- 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 : 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
⊢ 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:
simp [← Polynomial.map_mul, ← Polynomial.map_add, e]

Premises used: Polynomial.map_mul, Polynomial.map_add
-- 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
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
x : T
H : P.HasMap x
⊢ HasMap (P.map (algebraMap R S)) x

Tactic:
simpa [HasMap]

Premises used: StandardEtalePair.HasMap
-- 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 : StandardEtalePresentation R S
⊢ (P.equivRing.symm : (a : P.Ring) → S) P.X = P.x

Tactic:
P.lift_X _ P.hasMap

Premises used: Quotient.liftOn', StandardEtalePresentation.hasMap, AddCon.liftOn, StandardEtalePresentation.P, StandardEtalePair.lift_X
-- 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 : StandardEtalePresentation R S
⊢ (P.equivRing : (a : S) → P.Ring) P.x = P.X

Tactic:
(P.equivRing.symm_apply_eq.mp P.equivRing_symm_X).symm

Premises used: AlgEquiv.symm_apply_eq, StandardEtalePresentation.equivRing, Iff.mp, Eq.symm, StandardEtalePresentation.equivRing_symm_X
-- 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_1 : StandardEtalePair R
P : StandardEtalePresentation R S
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := P.Ring) (β := S) (⇑(↑(P.lift P.x ⋯) : P.Ring →+* S) : (a : P.Ring) → S)

Tactic:
P.lift_bijective.injective

Premises used: Quotient.liftOn', Set.Mem, AddCon.liftOn, Function.Bijective.injective, StandardEtalePresentation.lift_bijective, StandardEtalePair.Ring, Submodule.quotientRel, AddAction.orbitRel, AddCon.Quotient
-- 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_1 : StandardEtalePair R
P : StandardEtalePresentation R S
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := P.Ring) (β := S) (⇑(↑(P.lift P.x ⋯) : P.Ring →+* S) : (a : P.Ring) → S)

Tactic:
exact P.lift_bijective.injective

Premises used: Function.Bijective.injective, StandardEtalePresentation.lift_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_1 : StandardEtalePair R
P : StandardEtalePresentation R S
⊢ Function.Injective (α :=
    HasQuotient.Quotient (MvPolynomial (Fin 2) R) (B := 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)))))
    (β := P.Ring)
    (⇑(↑(↑P.equivMvPolynomialQuotient.symm :
              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)} →ₐ[R]
                P.Ring) :
          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) :
      (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)

Tactic:
P.equivMvPolynomialQuotient.symm.injective

Premises used: AlgEquiv.symm, StandardEtalePresentation.P, AlgEquiv.injective, StandardEtalePair.equivMvPolynomialQuotient
-- 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_1 : StandardEtalePair R
P : StandardEtalePresentation R S
⊢ Function.Injective (α :=
    HasQuotient.Quotient (MvPolynomial (Fin 2) R) (B := 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)))))
    (β := P.Ring)
    (⇑(↑(↑P.equivMvPolynomialQuotient.symm :
              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)} →ₐ[R]
                P.Ring) :
          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) :
      (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)

Tactic:
exact P.equivMvPolynomialQuotient.symm.injective

Premises used: AlgEquiv.symm, StandardEtalePresentation.P, AlgEquiv.injective, StandardEtalePair.equivMvPolynomialQuotient
-- 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 : StandardEtalePresentation R S
p : R[X]
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)
⊢ 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)

Tactic:
change (((MvPolynomial.aeval _).comp (Bivariate.equivMvPolynomial R).toAlgHom).comp CAlgHom) _ = _

Premises used: MvPolynomial.aeval, AlgEquiv.toAlgHom, Polynomial.CAlgHom, Polynomial.Bivariate.equivMvPolynomial, AlgHom.comp, 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 : StandardEtalePresentation R S
p : R[X]
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)
⊢ 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:
congr 1