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 : StandardEtalePresentation R S
p : R[X]
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)
⊢ 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:
ext
-- Module: Mathlib.RingTheory.Etale.StandardEtale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : 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)
        X :
      S)
    ((aeval P.x : (a : R[X]) → S) X : S)

Tactic:
simp
-- Module: Mathlib.RingTheory.Etale.StandardEtale
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
P_1 : StandardEtalePair R
P : StandardEtalePresentation R S
⊢ IsUnit
    { toPresentation := P.toPresentation, map := id, map_inj := ⋯ :
        Algebra.PreSubmersivePresentation R S (Fin 2) (Fin 2) }.jacobian

Tactic:
simp [P.hasMap.2, P.hasMap.isUnit_derivative_f]

Premises used: StandardEtalePresentation.hasMap, And.right, StandardEtalePair.HasMap.isUnit_derivative_f
-- 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.toSubmersivePresentation.jacobian =
    HMul.hMul (α := S) (β := S) ((aeval P.x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P.f : R[X]) : S)
      ((aeval P.x : (a : R[X]) → S) P.g : S)

Tactic:
simp [StandardEtalePresentation.toSubmersivePresentation]

Premises used: StandardEtalePresentation.toSubmersivePresentation
-- 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
x : S
obtain :
  ∀
    (x :
      Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)),
    ∃ (p : R[X]) (n : ℕ),
      HMul.hMul (α := S)
          (((P.equivRing.trans P.equivAwayAdjoinRoot).symm :
                (a : Localization.Away ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g)) → S)
              x :
            S)
          (HPow.hPow (α := S) ((aeval P.x : (a : R[X]) → S) P.g : S) n) =
        (aeval P.x : (a : R[X]) → S) p
⊢ ∃ (p : R[X]) (n : ℕ), x * HPow.hPow (α := S) ((aeval P.x : (a : R[X]) → S) P.g : S) n = (aeval P.x : (a : R[X]) → S) p

Tactic:
obtain ⟨x, rfl⟩ := (P.equivRing.trans P.P.equivAwayAdjoinRoot).symm.surjective x

Premises used: AlgEquiv.symm, StandardEtalePresentation.P, StandardEtalePair.equivAwayAdjoinRoot, StandardEtalePresentation.equivRing, AlgEquiv.trans, AlgEquiv.surjective, rfl
-- Module: Mathlib.RingTheory.Etale.StandardEtale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : StandardEtalePresentation R S
x : Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)
n : ℕ
p : R[X]
e :
  HMul.hMul (β :=
      Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
      x
      ((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,
                    Subtype.mk (p := fun (x : AdjoinRoot P.f) ↦
                      Membership.mem (γ := Submonoid (AdjoinRoot P.f))
                        (Submonoid.powers ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g) :
                          Submonoid (AdjoinRoot P.f))
                        x)
                      ((fun (x : ℕ) ↦
                          HPow.hPow (α := AdjoinRoot P.f)
                            ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f) x)
                        n)
                      ⋯) :
                  AdjoinRoot P.f ×
                    ↥(Submonoid.powers ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g) :
                        Submonoid (AdjoinRoot P.f))).2 :
            AdjoinRoot P.f) :
        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,
          Subtype.mk (p := fun (x : AdjoinRoot P.f) ↦
            Membership.mem (γ := Submonoid (AdjoinRoot P.f))
              (Submonoid.powers ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g) : Submonoid (AdjoinRoot P.f)) x)
            ((fun (x : ℕ) ↦
                HPow.hPow (α := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)
                  x)
              n)
            ⋯).1
⊢ ∃ (p : R[X]) (n : ℕ),
    HMul.hMul (α := S)
        (((P.equivRing.trans P.equivAwayAdjoinRoot).symm :
              (a : Localization.Away ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g)) → S)
            x :
          S)
        (HPow.hPow (α := S) ((aeval P.x : (a : R[X]) → S) P.g : S) n) =
      (aeval P.x : (a : R[X]) → S) p

Tactic:
⟨p, n, P.equivRing.injective ?_⟩

Premises used: StandardEtalePresentation.equivRing, Exists.intro, AlgEquiv.injective
-- 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
e : S ≃ₐ[R] T
⊢ Eq.{u_3 + 1} (α := T) (((P.lift ((e : (a : S) → T) P.x) ⋯ : P.Ring →ₐ[R] T) : (a : P.Ring) → T) P.X : T)
    (((↑e : S →ₐ[R] T).comp (P.lift P.x ⋯) : (a : P.Ring) → T) P.X : T)

Tactic:
simp
-- Module: Mathlib.RingTheory.Etale.StandardEtale
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
P : StandardEtalePresentation R S
f₁ f₂ : S →ₐ[R] T
h : Eq.{u_3 + 1} (α := T) ((f₁ : (a : S) → T) P.x : T) ((f₂ : (a : S) → T) P.x : T)
⊢ Eq.{u_3 + 1} (α := T) ((f₁.comp (↑P.equivRing.symm : P.Ring →ₐ[R] S) : (a : P.Ring) → T) P.X : T)
    ((f₂.comp (↑P.equivRing.symm : P.Ring →ₐ[R] S) : (a : P.Ring) → T) P.X : T)

Tactic:
simpa
-- 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 : StandardEtalePresentation R S
f₁ f₂ : S →ₐ[R] T
h : Eq.{u_3 + 1} (α := T) ((f₁ : (a : S) → T) P.x : T) ((f₂ : (a : S) → T) P.x : T)
⊢ f₁.comp (↑P.equivRing.symm : P.Ring →ₐ[R] S) = f₂.comp (↑P.equivRing.symm : P.Ring →ₐ[R] S)

Tactic:
have : f₁.comp P.equivRing.symm.toAlgHom = f₂.comp P.equivRing.symm.toAlgHom :=
    P.P.hom_ext (by simpa)
-- 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 : StandardEtalePresentation R S
f₁ f₂ : S →ₐ[R] T
h : Eq.{u_3 + 1} (α := T) ((f₁ : (a : S) → T) P.x : T) ((f₂ : (a : S) → T) P.x : T)
this : f₁.comp (↑P.equivRing.symm : P.Ring →ₐ[R] S) = f₂.comp (↑P.equivRing.symm : P.Ring →ₐ[R] S)
H : ∀ (x : S), Eq.{u_3 + 1} (α := T) ((f₁ : (a : S) → T) x : T) ((f₂ : (a : S) → T) x : T)
⊢ f₁ = f₂

Tactic:
ext x

Premises used: StandardEtalePresentation.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 : StandardEtalePresentation R S
f₁ f₂ : S →ₐ[R] T
h : Eq.{u_3 + 1} (α := T) ((f₁ : (a : S) → T) P.x : T) ((f₂ : (a : S) → T) P.x : T)
this : f₁.comp (↑P.equivRing.symm : P.Ring →ₐ[R] S) = f₂.comp (↑P.equivRing.symm : P.Ring →ₐ[R] S)
x : S
H :
  ∀ (x : P.Ring),
    Eq.{u_3 + 1} (α := T) ((f₁ : (a : S) → T) ((P.equivRing.symm : (a : P.Ring) → S) x : S) : T)
      ((f₂ : (a : S) → T) ((P.equivRing.symm : (a : P.Ring) → S) x : S) : T)
⊢ Eq.{u_3 + 1} (α := T) ((f₁ : (a : S) → T) x : T) ((f₂ : (a : S) → T) x : T)

Tactic:
obtain ⟨x, rfl⟩ := P.equivRing.symm.surjective x

Premises used: AlgEquiv.symm, StandardEtalePresentation.equivRing, AlgEquiv.surjective, 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 : StandardEtalePresentation R S
f₁ f₂ : S →ₐ[R] T
h : Eq.{u_3 + 1} (α := T) ((f₁ : (a : S) → T) P.x : T) ((f₂ : (a : S) → T) P.x : T)
this : f₁.comp (↑P.equivRing.symm : P.Ring →ₐ[R] S) = f₂.comp (↑P.equivRing.symm : P.Ring →ₐ[R] S)
x : P.Ring
⊢ Eq.{u_3 + 1} (α := T) ((f₁ : (a : S) → T) ((P.equivRing.symm : (a : P.Ring) → S) x : S) : T)
    ((f₂ : (a : S) → T) ((P.equivRing.symm : (a : P.Ring) → S) x : S) : T)

Tactic:
congr($this x)

Premises used: congrArg, id, DFunLike.coe
-- 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 : StandardEtalePresentation R S
f₁ f₂ : S →ₐ[R] T
h : Eq.{u_3 + 1} (α := T) ((f₁ : (a : S) → T) P.x : T) ((f₂ : (a : S) → T) P.x : T)
this : f₁.comp (↑P.equivRing.symm : P.Ring →ₐ[R] S) = f₂.comp (↑P.equivRing.symm : P.Ring →ₐ[R] S)
x : P.Ring
⊢ Eq.{u_3 + 1} (α := T) ((f₁ : (a : S) → T) ((P.equivRing.symm : (a : P.Ring) → S) x : S) : T)
    ((f₂ : (a : S) → T) ((P.equivRing.symm : (a : P.Ring) → S) x : S) : T)

Tactic:
exact congr($this 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
algInst : Algebra.{u_1, u_3} R (StandardEtalePair.Ring (P.map (algebraMap R T))) :=
  RingHom.toAlgebra
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap T (StandardEtalePair.Ring (P.map (algebraMap R T)))) (algebraMap R T))
scalarTowerInst : IsScalarTower R T (StandardEtalePair.Ring (P.map (algebraMap R T))) := ⋯
⊢ P.HasMap (S := StandardEtalePair.Ring (P.map (algebraMap R T))) (StandardEtalePair.X (P.map (algebraMap R T)))

Tactic:
simpa [StandardEtalePair.HasMap] using (P.map (algebraMap R T)).hasMap_X

Premises used: StandardEtalePair.hasMap_X, StandardEtalePair.HasMap
-- 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
algInst : Algebra.{u_1, u_3} R (StandardEtalePair.Ring (P.map (algebraMap R T))) :=
  RingHom.toAlgebra
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap T (StandardEtalePair.Ring (P.map (algebraMap R T)))) (algebraMap R T))
scalarTowerInst : IsScalarTower R T (StandardEtalePair.Ring (P.map (algebraMap R T))) := ⋯
H : P.HasMap (S := StandardEtalePair.Ring (P.map (algebraMap R T))) (StandardEtalePair.X (P.map (algebraMap R T)))
f : T ⊗[R] S →ₐ[T] StandardEtalePair.Ring (P.map (algebraMap R T)) :=
  Algebra.TensorProduct.lift (Algebra.ofId T (StandardEtalePair.Ring (P.map (algebraMap R T))))
    ((P.lift (StandardEtalePair.X (P.map (algebraMap R T))) H).comp (↑P.equivRing : S →ₐ[R] P.Ring)) ⋯
H₁ :
  Eq (α := StandardEtalePair.Ring (P.map (algebraMap R T)))
    ((f.comp (StandardEtalePair.lift (S := T ⊗[R] S) (P.map (algebraMap R T)) (1 ⊗ₜ[R] P.x) ⋯) :
          (a : (P.map (algebraMap R T)).Ring) → (P.map (algebraMap R T)).Ring)
        (StandardEtalePair.X (P.map (algebraMap R T))) :
      StandardEtalePair.Ring (P.map (algebraMap R T)))
    ((AlgHom.id T (StandardEtalePair.Ring (P.map (algebraMap R T))) :
          (a : (P.map (algebraMap R T)).Ring) → (P.map (algebraMap R T)).Ring)
        (StandardEtalePair.X (P.map (algebraMap R T))) :
      StandardEtalePair.Ring (P.map (algebraMap R T)))
⊢ f.comp (StandardEtalePair.lift (S := T ⊗[R] S) (P.map (algebraMap R T)) (1 ⊗ₜ[R] P.x) ⋯) =
    AlgHom.id T (StandardEtalePair.Ring (P.map (algebraMap R T)))

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_1 : StandardEtalePair R
P : StandardEtalePresentation R S
algInst : Algebra.{u_1, u_3} R (StandardEtalePair.Ring (P.map (algebraMap R T))) :=
  RingHom.toAlgebra
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap T (StandardEtalePair.Ring (P.map (algebraMap R T)))) (algebraMap R T))
scalarTowerInst : IsScalarTower R T (StandardEtalePair.Ring (P.map (algebraMap R T))) := ⋯
H : P.HasMap (S := StandardEtalePair.Ring (P.map (algebraMap R T))) (StandardEtalePair.X (P.map (algebraMap R T)))
f : T ⊗[R] S →ₐ[T] StandardEtalePair.Ring (P.map (algebraMap R T)) :=
  Algebra.TensorProduct.lift (Algebra.ofId T (StandardEtalePair.Ring (P.map (algebraMap R T))))
    ((P.lift (StandardEtalePair.X (P.map (algebraMap R T))) H).comp (↑P.equivRing : S →ₐ[R] P.Ring)) ⋯
⊢ Eq (α := StandardEtalePair.Ring (P.map (algebraMap R T)))
    ((f.comp (StandardEtalePair.lift (S := T ⊗[R] S) (P.map (algebraMap R T)) (1 ⊗ₜ[R] P.x) ⋯) :
          (a : (P.map (algebraMap R T)).Ring) → (P.map (algebraMap R T)).Ring)
        (StandardEtalePair.X (P.map (algebraMap R T))) :
      StandardEtalePair.Ring (P.map (algebraMap R T)))
    ((AlgHom.id T (StandardEtalePair.Ring (P.map (algebraMap R T))) :
          (a : (P.map (algebraMap R T)).Ring) → (P.map (algebraMap R T)).Ring)
        (StandardEtalePair.X (P.map (algebraMap R T))) :
      StandardEtalePair.Ring (P.map (algebraMap R T)))

Tactic:
simp [f]
-- 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
algInst : Algebra.{u_1, u_3} R (StandardEtalePair.Ring (P.map (algebraMap R T))) :=
  RingHom.toAlgebra
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap T (StandardEtalePair.Ring (P.map (algebraMap R T)))) (algebraMap R T))
scalarTowerInst : IsScalarTower R T (StandardEtalePair.Ring (P.map (algebraMap R T))) := ⋯
H : P.HasMap (S := StandardEtalePair.Ring (P.map (algebraMap R T))) (StandardEtalePair.X (P.map (algebraMap R T)))
f : T ⊗[R] S →ₐ[T] StandardEtalePair.Ring (P.map (algebraMap R T)) :=
  Algebra.TensorProduct.lift (Algebra.ofId T (StandardEtalePair.Ring (P.map (algebraMap R T))))
    ((P.lift (StandardEtalePair.X (P.map (algebraMap R T))) H).comp (↑P.equivRing : S →ₐ[R] P.Ring)) ⋯
h :
  Eq (α := S →ₐ[R] T ⊗[R] S)
    (AlgHom.comp (B := T ⊗[R] S)
        (AlgHom.restrictScalars R (S := T)
          (AlgHom.comp (StandardEtalePair.lift (S := T ⊗[R] S) (P.map (algebraMap R T)) (1 ⊗ₜ[R] P.x) ⋯) f))
        Algebra.TensorProduct.includeRight :
      S →ₐ[R] T ⊗[R] S)
    (AlgHom.comp (AlgHom.restrictScalars R (AlgHom.id T (T ⊗[R] S))) Algebra.TensorProduct.includeRight :
      S →ₐ[R] T ⊗[R] S)
⊢ Eq (α := T ⊗[R] S →ₐ[T] T ⊗[R] S)
    (AlgHom.comp (StandardEtalePair.lift (S := T ⊗[R] S) (P.map (algebraMap R T)) (1 ⊗ₜ[R] P.x) ⋯) f :
      T ⊗[R] S →ₐ[T] T ⊗[R] S)
    (AlgHom.id T (T ⊗[R] S) : T ⊗[R] S →ₐ[T] T ⊗[R] S)

Tactic:
ext1
-- 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
algInst : Algebra.{u_1, u_3} R (StandardEtalePair.Ring (P.map (algebraMap R T))) :=
  RingHom.toAlgebra
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap T (StandardEtalePair.Ring (P.map (algebraMap R T)))) (algebraMap R T))
scalarTowerInst : IsScalarTower R T (StandardEtalePair.Ring (P.map (algebraMap R T))) := ⋯
H : P.HasMap (S := StandardEtalePair.Ring (P.map (algebraMap R T))) (StandardEtalePair.X (P.map (algebraMap R T)))
f : T ⊗[R] S →ₐ[T] StandardEtalePair.Ring (P.map (algebraMap R T)) :=
  Algebra.TensorProduct.lift (Algebra.ofId T (StandardEtalePair.Ring (P.map (algebraMap R T))))
    ((P.lift (StandardEtalePair.X (P.map (algebraMap R T))) H).comp (↑P.equivRing : S →ₐ[R] P.Ring)) ⋯
h :
  Eq (α := T ⊗[R] S)
    (((AlgHom.comp (B := T ⊗[R] S)
              (AlgHom.restrictScalars R (S := T)
                (AlgHom.comp (StandardEtalePair.lift (S := T ⊗[R] S) (P.map (algebraMap R T)) (1 ⊗ₜ[R] P.x) ⋯) f))
              Algebra.TensorProduct.includeRight :
            S →ₐ[R] T ⊗[R] S) :
          (a : S) → T ⊗[R] S)
        P.x :
      T ⊗[R] S)
    ((AlgHom.comp (AlgHom.restrictScalars R (AlgHom.id T (T ⊗[R] S))) Algebra.TensorProduct.includeRight :
          (a : S) → T ⊗[R] S)
        P.x :
      T ⊗[R] S)
⊢ Eq (α := S →ₐ[R] T ⊗[R] S)
    (AlgHom.comp (B := T ⊗[R] S)
        (AlgHom.restrictScalars R (S := T)
          (AlgHom.comp (StandardEtalePair.lift (S := T ⊗[R] S) (P.map (algebraMap R T)) (1 ⊗ₜ[R] P.x) ⋯) f))
        Algebra.TensorProduct.includeRight :
      S →ₐ[R] T ⊗[R] S)
    (AlgHom.comp (AlgHom.restrictScalars R (AlgHom.id T (T ⊗[R] S))) Algebra.TensorProduct.includeRight :
      S →ₐ[R] T ⊗[R] S)

Tactic:
apply P.hom_ext

Premises used: StandardEtalePresentation.hom_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_1 : StandardEtalePair R
P : StandardEtalePresentation R S
algInst : Algebra.{u_1, u_3} R (StandardEtalePair.Ring (P.map (algebraMap R T))) :=
  RingHom.toAlgebra
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap T (StandardEtalePair.Ring (P.map (algebraMap R T)))) (algebraMap R T))
scalarTowerInst : IsScalarTower R T (StandardEtalePair.Ring (P.map (algebraMap R T))) := ⋯
H : P.HasMap (S := StandardEtalePair.Ring (P.map (algebraMap R T))) (StandardEtalePair.X (P.map (algebraMap R T)))
f : T ⊗[R] S →ₐ[T] StandardEtalePair.Ring (P.map (algebraMap R T)) :=
  Algebra.TensorProduct.lift (Algebra.ofId T (StandardEtalePair.Ring (P.map (algebraMap R T))))
    ((P.lift (StandardEtalePair.X (P.map (algebraMap R T))) H).comp (↑P.equivRing : S →ₐ[R] P.Ring)) ⋯
⊢ Eq (α := T ⊗[R] S)
    (((AlgHom.comp (B := T ⊗[R] S)
              (AlgHom.restrictScalars R (S := T)
                (AlgHom.comp (StandardEtalePair.lift (S := T ⊗[R] S) (P.map (algebraMap R T)) (1 ⊗ₜ[R] P.x) ⋯) f))
              Algebra.TensorProduct.includeRight :
            S →ₐ[R] T ⊗[R] S) :
          (a : S) → T ⊗[R] S)
        P.x :
      T ⊗[R] S)
    ((AlgHom.comp (AlgHom.restrictScalars R (AlgHom.id T (T ⊗[R] S))) Algebra.TensorProduct.includeRight :
          (a : S) → T ⊗[R] S)
        P.x :
      T ⊗[R] S)

Tactic:
simp [f]
-- 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
algInst : Algebra.{u_1, u_3} R (StandardEtalePair.Ring (P.map (algebraMap R T))) :=
  RingHom.toAlgebra
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap T (StandardEtalePair.Ring (P.map (algebraMap R T)))) (algebraMap R T))
scalarTowerInst : IsScalarTower R T (StandardEtalePair.Ring (P.map (algebraMap R T))) := ⋯
H : P.HasMap (S := StandardEtalePair.Ring (P.map (algebraMap R T))) (StandardEtalePair.X (P.map (algebraMap R T)))
f : T ⊗[R] S →ₐ[T] StandardEtalePair.Ring (P.map (algebraMap R T)) :=
  Algebra.TensorProduct.lift (Algebra.ofId T (StandardEtalePair.Ring (P.map (algebraMap R T))))
    ((P.lift (StandardEtalePair.X (P.map (algebraMap R T))) H).comp (↑P.equivRing : S →ₐ[R] P.Ring)) ⋯
α : T ⊗[R] S ≃ₐ[T] StandardEtalePair.Ring (P.map (algebraMap R T)) :=
  AlgEquiv.ofAlgHom f (StandardEtalePair.lift (S := T ⊗[R] S) (P.map (algebraMap R T)) (1 ⊗ₜ[R] P.x) ⋯) ⋯ ⋯
⊢ Function.Bijective (α := StandardEtalePair.Ring (P.map (algebraMap R T))) (β := T ⊗[R] S)
    (⇑(StandardEtalePair.lift (S := T ⊗[R] S) (P.map (algebraMap R T)) (1 ⊗ₜ[R] P.x) ⋯ :
          StandardEtalePair.Ring (P.map (algebraMap R T)) →ₐ[T] T ⊗[R] S) :
      (a : (P.map (algebraMap R T)).Ring) → T ⊗[R] S)

Tactic:
α.symm.bijective

Premises used: AlgEquiv.symm, Quotient.liftOn', Set.Mem, AddCon.liftOn, StandardEtalePair.Ring, Submodule.quotientRel, AddAction.orbitRel, AddCon.Quotient, AlgEquiv.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
algInst : Algebra.{u_1, u_3} R (StandardEtalePair.Ring (P.map (algebraMap R T))) :=
  RingHom.toAlgebra
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap T (StandardEtalePair.Ring (P.map (algebraMap R T)))) (algebraMap R T))
scalarTowerInst : IsScalarTower R T (StandardEtalePair.Ring (P.map (algebraMap R T))) := ⋯
H : P.HasMap (S := StandardEtalePair.Ring (P.map (algebraMap R T))) (StandardEtalePair.X (P.map (algebraMap R T)))
f : T ⊗[R] S →ₐ[T] StandardEtalePair.Ring (P.map (algebraMap R T)) :=
  Algebra.TensorProduct.lift (Algebra.ofId T (StandardEtalePair.Ring (P.map (algebraMap R T))))
    ((P.lift (StandardEtalePair.X (P.map (algebraMap R T))) H).comp (↑P.equivRing : S →ₐ[R] P.Ring)) ⋯
α : T ⊗[R] S ≃ₐ[T] StandardEtalePair.Ring (P.map (algebraMap R T)) :=
  AlgEquiv.ofAlgHom f (StandardEtalePair.lift (S := T ⊗[R] S) (P.map (algebraMap R T)) (1 ⊗ₜ[R] P.x) ⋯) ⋯ ⋯
⊢ Function.Bijective (α := StandardEtalePair.Ring (P.map (algebraMap R T))) (β := T ⊗[R] S)
    (⇑(StandardEtalePair.lift (S := T ⊗[R] S) (P.map (algebraMap R T)) (1 ⊗ₜ[R] P.x) ⋯ :
          StandardEtalePair.Ring (P.map (algebraMap R T)) →ₐ[T] T ⊗[R] S) :
      (a : (P.map (algebraMap R T)).Ring) → T ⊗[R] S)

Tactic:
exact α.symm.bijective

Premises used: AlgEquiv.symm, AlgEquiv.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_2 : StandardEtalePresentation R S
P : StandardEtalePair R
⊢ Function.Bijective (α := P.Ring) (β := P.Ring) (⇑(P.lift P.X ⋯) : (a : P.Ring) → P.Ring)

Tactic:
simpa [StandardEtalePair.lift_X_left] using Function.bijective_id

Premises used: Function.bijective_id, StandardEtalePair.lift_X_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_1 : StandardEtalePair R
P : StandardEtalePresentation R S
inst_5 : IsStandardEtale R S
⊢ Etale R S

Tactic:
.of_equiv IsStandardEtale.nonempty_standardEtalePresentation.some.equivRing.symm

Premises used: AlgEquiv.symm, Algebra.Etale.of_equiv, Nonempty.some, StandardEtalePresentation.equivRing, Algebra.IsStandardEtale.nonempty_standardEtalePresentation