awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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 = ⊥
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)))
⊢ Function.Bijective (α := P.Ring →ₐ[R] S) (β := P.Ring →ₐ[R] S ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))

Tactic:
rw [← P.homEquiv.symm.bijective.of_comp_iff, ← P.homEquiv.bijective.of_comp_iff']

Premises used: Equiv.bijective, StandardEtalePair.homEquiv, Function.Bijective.of_comp_iff, Function.Bijective.of_comp_iff', Equiv.symm
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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 = ⊥
this :
  ∀ (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
⊢ 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:
simpa [Function.bijective_iff_existsUnique, Ideal.Quotient.mk_surjective.forall,
      Subtype.ext_iff, Ideal.Quotient.mk_eq_mk_iff_sub_mem]

Premises used: Function.Surjective.forall, Subtype.ext_iff, Ideal.Quotient.mk_surjective, Ideal.Quotient.mk_eq_mk_iff_sub_mem, Function.bijective_iff_existsUnique
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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 = ⊥
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
⊢ 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:
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]
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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)
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
⊢ ∃! 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

Premises used: StandardEtalePair.existsUnique_hasMap_of_hasMap_quotient_of_sq_eq_bot
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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)
ε : S
H : ∀ (y : S), (fun (ε : S) ↦ ε ∈ I ∧ P.HasMap (x + ε)) y → y = ε
hεI : ε ∈ I
hε : P.HasMap (x + ε)
⊢ (fun (a : { x : S // P.HasMap x }) ↦ (↑a : S) - x ∈ I) (Subtype.mk (p := fun (x : S) ↦ P.HasMap x) (x + ε) hε)

Tactic:
simpa
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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)
ε : S
H : ∀ (y : S), (fun (ε : S) ↦ ε ∈ I ∧ P.HasMap (x + ε)) y → y = ε
hεI : ε ∈ I
hε : P.HasMap (x + ε)
y : { x : S // P.HasMap x }
hy : (fun (a : { x : S // P.HasMap x }) ↦ (↑a : S) - x ∈ I) y
⊢ P.HasMap (x + ((↑y : S) - x))

Tactic:
simpa using y.2

Premises used: Subtype.property
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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)
ε : 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:
exact ⟨⟨x + ε, hε⟩, by simpa, fun y hy ↦
    Subtype.ext (sub_eq_iff_eq_add'.mp (H _ ⟨hy, by simpa using y.2⟩))⟩
-- 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
⊢ Set.Finite (α := R[X][Y])
    (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
-- 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_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
refine_1₃ 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
⊢ 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:
rw [aeval_algebraMap_apply, AdjoinRoot.aeval_eq, AdjoinRoot.mk_self, map_zero]

Premises used: map_zero, AdjoinRoot.aeval_eq, AdjoinRoot.mk_self, Polynomial.aeval_algebraMap_apply
-- 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_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))
⊢ 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:
rw [aeval_algebraMap_apply, AdjoinRoot.aeval_eq]

Premises used: AdjoinRoot.aeval_eq, Polynomial.aeval_algebraMap_apply
-- 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
⊢ 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:
IsLocalization.Away.algebraMap_isUnit ..

Premises used: IsLocalization.Away.algebraMap_isUnit
-- 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
⊢ 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:
exact IsLocalization.Away.algebraMap_isUnit ..

Premises used: IsLocalization.Away.algebraMap_isUnit
-- 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 (AdjoinRoot P.f))
    (Submonoid.powers ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g) : Submonoid (AdjoinRoot P.f))
    (Submonoid.comap (AdjoinRoot.liftAlgHom P.f (Algebra.ofId R P.Ring) P.X ⋯) (IsUnit.submonoid P.Ring) :
      Submonoid (AdjoinRoot P.f))

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
⊢ Eq (α :=
    Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
    (((AlgHom.comp (B :=
              Localization (M := AdjoinRoot P.f)
                (Submonoid.powers ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g) : Submonoid (AdjoinRoot P.f)))
              (AlgHom.comp (B := 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))
                  ⋯)
                (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 ⋯) ⋯))
              (Algebra.algHom R (AdjoinRoot P.f)
                (Localization (M := AdjoinRoot P.f)
                  (Submonoid.powers ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g) :
                    Submonoid (AdjoinRoot P.f)))) :
            AdjoinRoot P.f →ₐ[R]
              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) :
      Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
    ((AlgHom.comp
            (AlgHom.id R
              (Localization.Away (M := AdjoinRoot P.f)
                ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)))
            (Algebra.algHom R (AdjoinRoot P.f)
              (Localization (M := AdjoinRoot P.f)
                (Submonoid.powers ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g) :
                  Submonoid (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) :
      Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))

Tactic:
simp [Algebra.algHom]

Premises used: Algebra.algHom
-- 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_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 ⋯) ⋯ :
              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)) :
          (a : P.Ring) → P.Ring)
        P.X :
      P.Ring)
    ((AlgHom.id R P.Ring : (a : P.Ring) → P.Ring) P.X : 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 ⋯) ⋯ :
        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

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 :=
            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)) :
          (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
-- 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
⊢ IsUnit (M :=
    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))))
    ((algebraMap (Localization.Away P.g)
            (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 : Localization.Away P.g) →
            Localization.Away P.g ⧸
              Ideal.span {(algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f})
        ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.g) :
      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:
(IsLocalization.Away.algebraMap_isUnit ..).map _

Premises used: IsUnit.map, IsLocalization.Away.algebraMap_isUnit
-- 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
⊢ IsUnit (M :=
    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))))
    ((algebraMap (Localization.Away P.g)
            (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 : Localization.Away P.g) →
            Localization.Away P.g ⧸
              Ideal.span {(algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f})
        ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.g) :
      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:
exact (IsLocalization.Away.algebraMap_isUnit ..).map _

Premises used: IsUnit.map, IsLocalization.Away.algebraMap_isUnit