awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (hypothesis)
Goal:
R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
inst_4 : CommRing R'
inst_5 : Algebra R R'
inst_6 : CommRing R''
inst_7 : Algebra R R''
inst_8 : Algebra R'' S
inst_9 : Algebra.IsIntegral R R''
inst_10 : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst_11 : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e :
  ((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
        (a : R' ⊗[R] R'') → R' ⊗[R] S)
      e₀ =
    e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' →
          P'' =
            Ideal.comap (F := R' ⊗[R] R'' →+* R' ⊗[R] S)
              (AlgHom.toRingHom
                (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S))
              P'
g : R''
hgq : ((algebraMap R'' S : (a : R'') → S) g : S) ∉ q
hg :
  Function.Surjective.{u_5 + 1, u_3 + 1} (α := Localization.Away g) (β :=
    Localization.Away (M := S) ((algebraMap R'' S : (a : R'') → S) g : S))
    (⇑(Localization.awayMap (algebraMap R'' S) g) :
      (a : Localization.Away g) → Localization.Away ((algebraMap R'' S : (a : R'') → S) g))
this : Algebra.IsIntegral R' (Localization.Away e₀)
f : R'
hfP : f ∉ P
hf :
  AlgHom.Finite (R := R') (A := Localization.Away f) (B :=
    Localization.Away (M := Localization.Away e)
      ((ofId R' (Localization.Away e) : (a : R') → Localization.Away e) f : Localization.Away e))
    (Localization.awayMapₐ (ofId R' (Localization.Away e)) f)
φ : R' ⊗[R] S →ₐ[R'] TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S :=
  TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)
algInst : Algebra (R' ⊗[R] S) (TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S) := φ.toAlgebra
⊢ IsLocalization.Away (R := R' ⊗[R] S) (f ⊗ₜ[R] 1) (TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S)
have this₁ : Eq (α := Submonoid (R' ⊗[R] S)) (Submonoid.powers (f ⊗ₜ[R] 1)) (algebraMapSubmonoid (R' ⊗[R] S) (Submonoid.powers f))
Tactic: have : .powers (f ⊗ₜ[R] 1) = Algebra.algebraMapSubmonoid (R' ⊗[R] S) (.powers f) := by simp
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (goal)
Goal:
R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
inst_4 : CommRing R'
inst_5 : Algebra R R'
inst_6 : CommRing R''
inst_7 : Algebra R R''
inst_8 : Algebra R'' S
inst_9 : Algebra.IsIntegral R R''
inst_10 : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst_11 : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e :
  ((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
        (a : R' ⊗[R] R'') → R' ⊗[R] S)
      e₀ =
    e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' →
          P'' =
            Ideal.comap (F := R' ⊗[R] R'' →+* R' ⊗[R] S)
              (AlgHom.toRingHom
                (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S))
              P'
g : R''
hgq : ((algebraMap R'' S : (a : R'') → S) g : S) ∉ q
hg :
  Function.Surjective.{u_5 + 1, u_3 + 1} (α := Localization.Away g) (β :=
    Localization.Away (M := S) ((algebraMap R'' S : (a : R'') → S) g : S))
    (⇑(Localization.awayMap (algebraMap R'' S) g) :
      (a : Localization.Away g) → Localization.Away ((algebraMap R'' S : (a : R'') → S) g))
this_1 : Algebra.IsIntegral R' (Localization.Away e₀)
f : R'
hfP : f ∉ P
hf :
  AlgHom.Finite (R := R') (A := Localization.Away f) (B :=
    Localization.Away (M := Localization.Away e)
      ((ofId R' (Localization.Away e) : (a : R') → Localization.Away e) f : Localization.Away e))
    (Localization.awayMapₐ (ofId R' (Localization.Away e)) f)
φ : R' ⊗[R] S →ₐ[R'] TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S :=
  TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)
algInst : Algebra (R' ⊗[R] S) (TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S) := φ.toAlgebra
this :
  Eq (α := Submonoid (R' ⊗[R] S)) (Submonoid.powers (f ⊗ₜ[R] 1)) (algebraMapSubmonoid (R' ⊗[R] S) (Submonoid.powers f))
⊢ IsLocalization.Away (R := R' ⊗[R] S) (f ⊗ₜ[R] 1) (TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S)
have rw : IsLocalization (R := R' ⊗[R] S) (algebraMapSubmonoid (R' ⊗[R] S) (Submonoid.powers f))
  (TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S)
Tactic: rw [IsLocalization.Away, this]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (goal)
Goal:
R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
inst_4 : CommRing R'
inst_5 : Algebra R R'
inst_6 : CommRing R''
inst_7 : Algebra R R''
inst_8 : Algebra R'' S
inst_9 : Algebra.IsIntegral R R''
inst_10 : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst_11 : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e :
  ((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
        (a : R' ⊗[R] R'') → R' ⊗[R] S)
      e₀ =
    e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' →
          P'' =
            Ideal.comap (F := R' ⊗[R] R'' →+* R' ⊗[R] S)
              (AlgHom.toRingHom
                (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S))
              P'
g : R''
hgq : ((algebraMap R'' S : (a : R'') → S) g : S) ∉ q
hg :
  Function.Surjective.{u_5 + 1, u_3 + 1} (α := Localization.Away g) (β :=
    Localization.Away (M := S) ((algebraMap R'' S : (a : R'') → S) g : S))
    (⇑(Localization.awayMap (algebraMap R'' S) g) :
      (a : Localization.Away g) → Localization.Away ((algebraMap R'' S : (a : R'') → S) g))
this_1 : Algebra.IsIntegral R' (Localization.Away e₀)
f : R'
hfP : f ∉ P
hf :
  AlgHom.Finite (R := R') (A := Localization.Away f) (B :=
    Localization.Away (M := Localization.Away e)
      ((ofId R' (Localization.Away e) : (a : R') → Localization.Away e) f : Localization.Away e))
    (Localization.awayMapₐ (ofId R' (Localization.Away e)) f)
φ : R' ⊗[R] S →ₐ[R'] TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S :=
  TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)
algInst : Algebra (R' ⊗[R] S) (TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S) := φ.toAlgebra
this :
  Eq (α := Submonoid (R' ⊗[R] S)) (Submonoid.powers (f ⊗ₜ[R] 1)) (algebraMapSubmonoid (R' ⊗[R] S) (Submonoid.powers f))
⊢ IsLocalization (R := R' ⊗[R] S) (algebraMapSubmonoid (R' ⊗[R] S) (Submonoid.powers f))
    (TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S)
have refine : Eq (α := S →+* TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S)
  (@RingHom.comp _ (R' ⊗[R] S) _ _ Semiring.toNonAssocSemiring _
    (algebraMap (R' ⊗[R] S) (TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S))
    (AlgHom.toRingHom TensorProduct.includeRight))
  (AlgHom.toRingHom TensorProduct.includeRight)
Tactic: refine IsLocalization.tensorProduct_tensorProduct _ _ _ _ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (goal)
Goal:
R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
inst_4 : CommRing R'
inst_5 : Algebra R R'
inst_6 : CommRing R''
inst_7 : Algebra R R''
inst_8 : Algebra R'' S
inst_9 : Algebra.IsIntegral R R''
inst_10 : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst_11 : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e :
  ((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
        (a : R' ⊗[R] R'') → R' ⊗[R] S)
      e₀ =
    e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' →
          P'' =
            Ideal.comap (F := R' ⊗[R] R'' →+* R' ⊗[R] S)
              (AlgHom.toRingHom
                (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S))
              P'
g : R''
hgq : ((algebraMap R'' S : (a : R'') → S) g : S) ∉ q
hg :
  Function.Surjective.{u_5 + 1, u_3 + 1} (α := Localization.Away g) (β :=
    Localization.Away (M := S) ((algebraMap R'' S : (a : R'') → S) g : S))
    (⇑(Localization.awayMap (algebraMap R'' S) g) :
      (a : Localization.Away g) → Localization.Away ((algebraMap R'' S : (a : R'') → S) g))
this_1 : Algebra.IsIntegral R' (Localization.Away e₀)
f : R'
hfP : f ∉ P
hf :
  AlgHom.Finite (R := R') (A := Localization.Away f) (B :=
    Localization.Away (M := Localization.Away e)
      ((ofId R' (Localization.Away e) : (a : R') → Localization.Away e) f : Localization.Away e))
    (Localization.awayMapₐ (ofId R' (Localization.Away e)) f)
φ : R' ⊗[R] S →ₐ[R'] TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S :=
  TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)
algInst : Algebra (R' ⊗[R] S) (TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S) := φ.toAlgebra
this :
  Eq (α := Submonoid (R' ⊗[R] S)) (Submonoid.powers (f ⊗ₜ[R] 1)) (algebraMapSubmonoid (R' ⊗[R] S) (Submonoid.powers f))
⊢ Eq (α := S →+* TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S)
    (@RingHom.comp _ (R' ⊗[R] S) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (R' ⊗[R] S) (TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S))
      (AlgHom.toRingHom TensorProduct.includeRight))
    (AlgHom.toRingHom TensorProduct.includeRight)
have a : ∀ (x : S),
  Eq (α := TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S)
    ((@RingHom.comp _ (R' ⊗[R] S) _ _ Semiring.toNonAssocSemiring _
            (algebraMap (R' ⊗[R] S) (TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S))
            (AlgHom.toRingHom TensorProduct.includeRight) :
          (a : S) → Localization.Away f ⊗[R] S)
        x :
      TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S)
    ((AlgHom.toRingHom TensorProduct.includeRight : (a : S) → Localization.Away f ⊗[R] S) x :
      TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (hypothesis)
Goal:
R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
inst_4 : CommRing R'
inst_5 : Algebra R R'
inst_6 : CommRing R''
inst_7 : Algebra R R''
inst_8 : Algebra R'' S
inst_9 : Algebra.IsIntegral R R''
inst_10 : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst_11 : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e :
  ((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
        (a : R' ⊗[R] R'') → R' ⊗[R] S)
      e₀ =
    e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' →
          P'' =
            Ideal.comap (F := R' ⊗[R] R'' →+* R' ⊗[R] S)
              (AlgHom.toRingHom
                (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S))
              P'
g : R''
hgq : ((algebraMap R'' S : (a : R'') → S) g : S) ∉ q
hg :
  Function.Surjective.{u_5 + 1, u_3 + 1} (α := Localization.Away g) (β :=
    Localization.Away (M := S) ((algebraMap R'' S : (a : R'') → S) g : S))
    (⇑(Localization.awayMap (algebraMap R'' S) g) :
      (a : Localization.Away g) → Localization.Away ((algebraMap R'' S : (a : R'') → S) g))
this : Algebra.IsIntegral R' (Localization.Away e₀)
f : R'
hfP : f ∉ P
hf :
  AlgHom.Finite (R := R') (A := Localization.Away f) (B :=
    Localization.Away (M := Localization.Away e)
      ((ofId R' (Localization.Away e) : (a : R') → Localization.Away e) f : Localization.Away e))
    (Localization.awayMapₐ (ofId R' (Localization.Away e)) f)
φ : R' ⊗[R] S →ₐ[R'] TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S :=
  TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)
algInst : Algebra (R' ⊗[R] S) (TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S) := φ.toAlgebra
⊢ Module.Finite (Localization.Away f)
    (Localization.Away (M := TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S)
      (((TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S) :
              R' ⊗[R] S →ₐ[R'] TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S) :
            (a : R' ⊗[R] S) → Localization.Away f ⊗[R] S)
          e :
        TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S))
have this₁ : IsLocalization.Away (R := R' ⊗[R] S) (f ⊗ₜ[R] 1) (TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S)
Tactic: have : IsLocalization.Away (f ⊗ₜ 1 : R' ⊗[R] S) (Localization.Away f ⊗[R] S) := by
    have : .powers (f ⊗ₜ[R] 1) = Algebra.algebraMapSubmonoid (R' ⊗[R] S) (.powers f) := by simp
    rw [IsLocalization.Away, this]
    refine IsLocalization.tensorProduct_tensorProduct _ _ _ _ ?_
    ext; simp [RingHom.algebraMap_toAlgebra, φ]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (hypothesis)
Goal:
R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
inst_4 : CommRing R'
inst_5 : Algebra R R'
inst_6 : CommRing R''
inst_7 : Algebra R R''
inst_8 : Algebra R'' S
inst_9 : Algebra.IsIntegral R R''
inst_10 : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst_11 : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e :
  ((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
        (a : R' ⊗[R] R'') → R' ⊗[R] S)
      e₀ =
    e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' →
          P'' =
            Ideal.comap (F := R' ⊗[R] R'' →+* R' ⊗[R] S)
              (AlgHom.toRingHom
                (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S))
              P'
g : R''
hgq : ((algebraMap R'' S : (a : R'') → S) g : S) ∉ q
hg :
  Function.Surjective.{u_5 + 1, u_3 + 1} (α := Localization.Away g) (β :=
    Localization.Away (M := S) ((algebraMap R'' S : (a : R'') → S) g : S))
    (⇑(Localization.awayMap (algebraMap R'' S) g) :
      (a : Localization.Away g) → Localization.Away ((algebraMap R'' S : (a : R'') → S) g))
this_1 : Algebra.IsIntegral R' (Localization.Away e₀)
f : R'
hfP : f ∉ P
hf :
  AlgHom.Finite (R := R') (A := Localization.Away f) (B :=
    Localization.Away (M := Localization.Away e)
      ((ofId R' (Localization.Away e) : (a : R') → Localization.Away e) f : Localization.Away e))
    (Localization.awayMapₐ (ofId R' (Localization.Away e)) f)
φ : R' ⊗[R] S →ₐ[R'] TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S :=
  TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)
algInst : Algebra (R' ⊗[R] S) (TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S) := φ.toAlgebra
this : IsLocalization.Away (R := R' ⊗[R] S) (f ⊗ₜ[R] 1) (TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S)
⊢ Module.Finite (Localization.Away f)
    (Localization.Away (M := TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S)
      (((TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S) :
              R' ⊗[R] S →ₐ[R'] TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S) :
            (a : R' ⊗[R] S) → Localization.Away f ⊗[R] S)
          e :
        TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S))
have this₁ : IsLocalization.Away (e * f ⊗ₜ[R] 1)
  (Localization.Away (M := TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S)
    ((φ : (a : R' ⊗[R] S) → Localization.Away f ⊗[R] S) e : TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S))
Tactic: have : IsLocalization.Away (e * (f ⊗ₜ 1)) (Localization.Away (φ e)) :=
    .mul (Localization.Away f ⊗[R] S) (Localization.Away (algebraMap _ _ e)) _ _
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : StandardEtalePair R
x : S
h : P.HasMap x
⊢ IsUnit.{u_2} (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P.f : R[X]) : S)
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),
  IsUnit.{u_2} (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P.f : R[X]) : S)
Tactic: obtain ⟨p₁, p₂, n, e⟩ := P.cond
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : StandardEtalePair R
x : S
h : P.HasMap x
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
⊢ IsUnit.{u_2} (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P.f : R[X]) : S)
have this : (aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P.f : R[X]) ∣
  HPow.hPow (α := S) ((aeval x : (a : R[X]) → S) P.g : S) n
Tactic: have : aeval x P.f.derivative ∣ aeval x P.g ^ n :=
    ⟨_, by simpa [h.1] using congr(aeval x $e.symm)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
inst : CommRing R
P : StandardEtalePair R
⊢ Eq (α := R[X] →ₐ[R] P.Ring) (aeval P.X)
    (AlgHom.comp
      (Ideal.Quotient.mkₐ 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})))
      CAlgHom)
have hX : Eq (α := P.Ring) ((aeval P.X : (a : R[X]) → P.Ring) X : P.Ring)
  ((AlgHom.comp
          (Ideal.Quotient.mkₐ 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})))
          CAlgHom :
        (a : R[X]) → P.Ring)
      X :
    P.Ring)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : StandardEtalePair R
⊢ HMul.hMul (α := P.Ring) (β :=
      HasQuotient.Quotient R[X][Y] (B := Ideal R[X][Y])
        (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})))
      ((aeval P.X : (a : R[X]) → P.Ring) P.g : P.Ring)
      ((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})
          Y :
        HasQuotient.Quotient R[X][Y] (B := Ideal R[X][Y])
          (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}))) =
    1
have this : Eq (α := R[X] →ₐ[R] P.Ring) (aeval P.X)
  (AlgHom.comp
    (Ideal.Quotient.mkₐ 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})))
    CAlgHom)
Tactic: have : aeval (R := R) P.X = (Ideal.Quotient.mkₐ _ _).comp Polynomial.CAlgHom := by
    ext; simp [StandardEtalePair.Ring, StandardEtalePair.X]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
inst : CommRing R
P : StandardEtalePair R
this :
  Eq (α := R[X] →ₐ[R] P.Ring) (aeval P.X)
    (AlgHom.comp
      (Ideal.Quotient.mkₐ 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})))
      CAlgHom)
⊢ HMul.hMul (α := P.Ring) (β :=
      HasQuotient.Quotient R[X][Y] (B := Ideal R[X][Y])
        (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})))
      ((aeval P.X : (a : R[X]) → P.Ring) P.g : P.Ring)
      ((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})
          Y :
        HasQuotient.Quotient R[X][Y] (B := Ideal R[X][Y])
          (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}))) =
    1
have rw : HMul.hMul (α := P.Ring) (β :=
    HasQuotient.Quotient R[X][Y] (B := Ideal R[X][Y])
      (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})))
    ((AlgHom.comp
            (Ideal.Quotient.mkₐ 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})))
            CAlgHom :
          (a : R[X]) → P.Ring)
        P.g :
      P.Ring)
    ((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})
        Y :
      HasQuotient.Quotient R[X][Y] (B := Ideal R[X][Y])
        (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}))) =
  1
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : StandardEtalePair R
f g : P.Ring →ₐ[R] S
H : Eq.{u_2 + 1} (α := S) ((f : (a : P.Ring) → S) P.X : S) ((g : (a : P.Ring) → S) P.X : S)
⊢ f = g
have H₁ : (f.comp
        (Ideal.Quotient.mkₐ 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})))).comp
    CAlgHom =
  (g.comp
        (Ideal.Quotient.mkₐ 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})))).comp
    CAlgHom
Tactic: have H : (f.comp (Ideal.Quotient.mkₐ R _)).comp CAlgHom =
    (g.comp (Ideal.Quotient.mkₐ R _)).comp CAlgHom := Polynomial.algHom_ext (by simpa)