awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallyUnramified R A
f : A →ₐ[R] B
H : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
Q : Type u_3
inst_6 : CommRing Q
inst_7 : Algebra R Q
I : Ideal Q
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : B →ₐ[R] Q
e : Eq (α := B →ₐ[R] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂)
x : A
H₁ :
  ∀ (x : A),
    Eq.{u_3 + 1} (α := Q ⧸ I)
      (((AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₁.comp f) : AlgHom.{u_1, u_2, u_3} R A (Q ⧸ I)) : (a : A) → Q ⧸ I) x :
        Q ⧸ I)
      (((AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₂.comp f) : AlgHom.{u_1, u_2, u_3} R A (Q ⧸ I)) : (a : A) → Q ⧸ I) x :
        Q ⧸ I)
⊢ Eq (α := AlgHom.{u_1, u_2, u_3} R A (Q ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₁.comp f))
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₂.comp f))

Tactic:
ext x
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallyUnramified R A
f : A →ₐ[R] B
H : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
Q : Type u_3
inst_6 : CommRing Q
inst_7 : Algebra R Q
I : Ideal Q
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : B →ₐ[R] Q
e : Eq (α := B →ₐ[R] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂)
x_1 x : A
⊢ Eq.{u_3 + 1} (α := Q ⧸ I)
    (((AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₁.comp f) : AlgHom.{u_1, u_2, u_3} R A (Q ⧸ I)) : (a : A) → Q ⧸ I) x :
      Q ⧸ I)
    (((AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₂.comp f) : AlgHom.{u_1, u_2, u_3} R A (Q ⧸ I)) : (a : A) → Q ⧸ I) x :
      Q ⧸ I)

Tactic:
DFunLike.congr_fun e (f x)

Premises used: DFunLike.congr_fun, DFunLike.coe
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallyUnramified R A
f : A →ₐ[R] B
H : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
Q : Type u_3
inst_6 : CommRing Q
inst_7 : Algebra R Q
I : Ideal Q
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : B →ₐ[R] Q
e : Eq (α := B →ₐ[R] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂)
x_1 x : A
⊢ Eq.{u_3 + 1} (α := Q ⧸ I)
    (((AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₁.comp f) : AlgHom.{u_1, u_2, u_3} R A (Q ⧸ I)) : (a : A) → Q ⧸ I) x :
      Q ⧸ I)
    (((AlgHom.comp (Ideal.Quotient.mkₐ R I) (f₂.comp f) : AlgHom.{u_1, u_2, u_3} R A (Q ⧸ I)) : (a : A) → Q ⧸ I) x :
      Q ⧸ I)

Tactic:
exact DFunLike.congr_fun e (f x)

Premises used: DFunLike.congr_fun, DFunLike.coe
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u_1
inst : CommRing R
A_1 : Type u_2
B : Type u_3
inst_1 : CommRing A_1
inst_2 : Algebra R A_1
inst_3 : CommRing B
inst_4 : Algebra R B
A : Type u_4
inst_5 : CommRing A
inst_6 : Algebra R A
inst_7 : FormallyUnramified R A
I : Ideal A
⊢ FormallyUnramified.{u_4, u_1} R (A ⧸ I)

Tactic:
FormallyUnramified.of_surjective (IsScalarTower.toAlgHom R A (A ⧸ I)) Ideal.Quotient.mk_surjective

Premises used: Algebra.FormallyUnramified.of_surjective, IsScalarTower.toAlgHom, Ideal.Quotient.mk_surjective, HasQuotient.Quotient
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
e : A ≃ₐ[R] B
⊢ FormallyUnramified R A ↔ FormallyUnramified R B

Tactic:
⟨fun _ ↦ of_equiv e, fun _ ↦ of_equiv e.symm⟩

Premises used: AlgEquiv.symm, Iff.intro, Algebra.FormallyUnramified.of_equiv
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallyUnramified R A
rw :
  ∀ ⦃B_1 : Type (max u_2 u_3)⦄ [inst_6 : CommRing B_1] [inst_7 : Algebra B B_1] (I : Ideal B_1),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Injective (α := B ⊗[R] A →ₐ[B] B_1) (β := B ⊗[R] A →ₐ[B] B_1 ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ B I))
⊢ FormallyUnramified B (B ⊗[R] A)

Tactic:
rw [iff_comp_injective]

Premises used: Algebra.FormallyUnramified.iff_comp_injective
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallyUnramified R A
C : Type (max u_2 u_3)
_ :
  ∀ [inst_6 : CommRing C] [inst_7 : Algebra B C] (I : Ideal C),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Injective (α := B ⊗[R] A →ₐ[B] C) (β := B ⊗[R] A →ₐ[B] C ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ B I))
⊢ ∀ [inst_6 : CommRing C] [inst_7 : Algebra B C] (I : Ideal C),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Injective (α := B ⊗[R] A →ₐ[B] C) (β := B ⊗[R] A →ₐ[B] C ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ B I))

Tactic:
_
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallyUnramified R A
C : Type (max u_2 u_3)
inst_6 : CommRing C
_ :
  ∀ [inst_7 : Algebra B C] (I : Ideal C),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Injective (α := B ⊗[R] A →ₐ[B] C) (β := B ⊗[R] A →ₐ[B] C ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ B I))
⊢ ∀ [inst_7 : Algebra B C] (I : Ideal C),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Injective (α := B ⊗[R] A →ₐ[B] C) (β := B ⊗[R] A →ₐ[B] C ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ B I))

Tactic:
_
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallyUnramified R A
C : Type (max u_2 u_3)
inst_6 : CommRing C
inst_7 : Algebra B C
I : Ideal C
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : B ⊗[R] A →ₐ[B] C
e : Eq (α := B ⊗[R] A →ₐ[B] C ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ B I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ B I) f₂)
this : Algebra R C :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (algebraMap R B))
⊢ IsScalarTower R B C

Tactic:
haveI : IsScalarTower R B C := IsScalarTower.of_algebraMap_eq' rfl
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallyUnramified R A
C : Type (max u_2 u_3)
inst_6 : CommRing C
inst_7 : Algebra B C
I : Ideal C
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : B ⊗[R] A →ₐ[B] C
e : Eq (α := B ⊗[R] A →ₐ[B] C ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ B I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ B I) f₂)
this_1 : Algebra R C :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (algebraMap R B))
this : IsScalarTower R B C
h :
  Eq (α := A →ₐ[R] C) (AlgHom.comp (AlgHom.restrictScalars R f₁) TensorProduct.includeRight)
    (AlgHom.comp (AlgHom.restrictScalars R f₂) TensorProduct.includeRight)
⊢ f₁ = f₂

Tactic:
ext : 1
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallyUnramified R A
C : Type (max u_2 u_3)
inst_6 : CommRing C
inst_7 : Algebra B C
I : Ideal C
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : B ⊗[R] A →ₐ[B] C
e : Eq (α := B ⊗[R] A →ₐ[B] C ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ B I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ B I) f₂)
this_1 : Algebra R C :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (algebraMap R B))
this : IsScalarTower R B C
⊢ Eq (α := A →ₐ[R] C) (AlgHom.comp (AlgHom.restrictScalars R f₁) TensorProduct.includeRight)
    (AlgHom.comp (AlgHom.restrictScalars R f₂) TensorProduct.includeRight)

Tactic:
FormallyUnramified.ext I ⟨2, hI⟩ fun x => AlgHom.congr_fun e (1 ⊗ₜ x)

Premises used: Algebra.FormallyUnramified.ext, Exists.intro, AlgHom.congr_fun, TensorProduct.tmul, OfNat.ofNat
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallyUnramified R A
C : Type (max u_2 u_3)
inst_6 : CommRing C
inst_7 : Algebra B C
I : Ideal C
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : B ⊗[R] A →ₐ[B] C
e : Eq (α := B ⊗[R] A →ₐ[B] C ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ B I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ B I) f₂)
this_1 : Algebra R C :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (algebraMap R B))
this : IsScalarTower R B C
⊢ Eq (α := A →ₐ[R] C) (AlgHom.comp (AlgHom.restrictScalars R f₁) TensorProduct.includeRight)
    (AlgHom.comp (AlgHom.restrictScalars R f₂) TensorProduct.includeRight)

Tactic:
exact FormallyUnramified.ext I ⟨2, hI⟩ fun x => AlgHom.congr_fun e (1 ⊗ₜ x)

Premises used: Algebra.FormallyUnramified.ext, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallyUnramified R B
p : Ideal R
⊢ FormallyUnramified.{u_3, u_1} (R ⧸ p)
    (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := R →+* B) (algebraMap R B) p))

Tactic:
.of_equiv (Algebra.TensorProduct.quotIdealMapEquivQuotTensor B p).symm

Premises used: AlgEquiv.symm, Algebra.TensorProduct.quotIdealMapEquivQuotTensor, Algebra.FormallyUnramified.of_equiv
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u_1
Rₘ : Type u_3
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
rw :
  ∀ ⦃B : Type u_3⦄ [inst_4 : CommRing B] [inst_5 : Algebra R B] (I : Ideal B),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Injective (α := Rₘ →ₐ[R] B) (β := Rₘ →ₐ[R] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
⊢ FormallyUnramified R Rₘ

Tactic:
rw [iff_comp_injective]

Premises used: Algebra.FormallyUnramified.iff_comp_injective
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u_1
Rₘ : Type u_3
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
Q : Type u_3
_ :
  ∀ [inst_4 : CommRing Q] [inst_5 : Algebra R Q] (I : Ideal Q),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Injective (α := Rₘ →ₐ[R] Q) (β := Rₘ →ₐ[R] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
⊢ ∀ [inst_4 : CommRing Q] [inst_5 : Algebra R Q] (I : Ideal Q),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Injective (α := Rₘ →ₐ[R] Q) (β := Rₘ →ₐ[R] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))

Tactic:
_
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u_1
Rₘ : Type u_3
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
Q : Type u_3
inst_4 : CommRing Q
_ :
  ∀ [inst_5 : Algebra R Q] (I : Ideal Q),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Injective (α := Rₘ →ₐ[R] Q) (β := Rₘ →ₐ[R] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
⊢ ∀ [inst_5 : Algebra R Q] (I : Ideal Q),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Injective (α := Rₘ →ₐ[R] Q) (β := Rₘ →ₐ[R] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))

Tactic:
_
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u_1
Rₘ : Type u_3
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
Q : Type u_3
inst_4 : CommRing Q
inst_5 : Algebra R Q
I : Ideal Q
_ :
  HPow.hPow (β := ℕ) I 2 = ⊥ →
    Function.Injective (α := Rₘ →ₐ[R] Q) (β := Rₘ →ₐ[R] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
⊢ HPow.hPow (β := ℕ) I 2 = ⊥ →
    Function.Injective (α := Rₘ →ₐ[R] Q) (β := Rₘ →ₐ[R] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))

Tactic:
_
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u_1
Rₘ : Type u_3
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
Q : Type u_3
inst_4 : CommRing Q
inst_5 : Algebra R Q
I : Ideal Q
h : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : Rₘ →ₐ[R] Q
_ :
  Eq (α := Rₘ →ₐ[R] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂) → f₁ = f₂
⊢ Eq (α := Rₘ →ₐ[R] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂) → f₁ = f₂

Tactic:
_
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u_1
Rₘ : Type u_3
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
Q : Type u_3
inst_4 : CommRing Q
inst_5 : Algebra R Q
I : Ideal Q
h : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : Rₘ →ₐ[R] Q
h_1 : Eq (α := Rₘ →ₐ[R] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂)
a : Eq (α := Rₘ →+* Q) (↑f₁ : Rₘ →+* Q) (↑f₂ : Rₘ →+* Q)
⊢ f₁ = f₂

Tactic:
apply AlgHom.coe_ringHom_injective

Premises used: AlgHom.coe_ringHom_injective
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u_1
Rₘ : Type u_3
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
Q : Type u_3
inst_4 : CommRing Q
inst_5 : Algebra R Q
I : Ideal Q
h : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : Rₘ →ₐ[R] Q
h_1 : Eq (α := Rₘ →ₐ[R] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂)
⊢ Eq (α := Rₘ →+* Q) (↑f₁ : Rₘ →+* Q) (↑f₂ : Rₘ →+* Q)

Tactic:
IsLocalization.ringHom_ext M ?_

Premises used: IsLocalization.ringHom_ext
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u_1
Rₘ : Type u_3
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
Q : Type u_3
inst_4 : CommRing Q
inst_5 : Algebra R Q
I : Ideal Q
h : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : Rₘ →ₐ[R] Q
h_1 : Eq (α := Rₘ →ₐ[R] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂)
a :
  Eq (α := R →+* Q) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f₁ : Rₘ →+* Q) (algebraMap R Rₘ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f₂ : Rₘ →+* Q) (algebraMap R Rₘ))
⊢ Eq (α := Rₘ →+* Q) (↑f₁ : Rₘ →+* Q) (↑f₂ : Rₘ →+* Q)

Tactic:
refine IsLocalization.ringHom_ext M ?_

Premises used: IsLocalization.ringHom_ext
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u_1
Rₘ : Type u_3
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
Q : Type u_3
inst_4 : CommRing Q
inst_5 : Algebra R Q
I : Ideal Q
h : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : Rₘ →ₐ[R] Q
h_1 : Eq (α := Rₘ →ₐ[R] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂)
a :
  ∀ (x : R),
    Eq.{u_3 + 1} (α := Q)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f₁ : Rₘ →+* Q) (algebraMap R Rₘ) : (a : R) → Q) x : Q)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f₂ : Rₘ →+* Q) (algebraMap R Rₘ) : (a : R) → Q) x : Q)
⊢ Eq (α := R →+* Q) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f₁ : Rₘ →+* Q) (algebraMap R Rₘ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f₂ : Rₘ →+* Q) (algebraMap R Rₘ))

Tactic:
ext
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u_1
Rₘ : Type u_3
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
Q : Type u_3
inst_4 : CommRing Q
inst_5 : Algebra R Q
I : Ideal Q
h : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : Rₘ →ₐ[R] Q
h_1 : Eq (α := Rₘ →ₐ[R] Q ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂)
x : R
⊢ Eq.{u_3 + 1} (α := Q)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f₁ : Rₘ →+* Q) (algebraMap R Rₘ) : (a : R) → Q) x : Q)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f₂ : Rₘ →+* Q) (algebraMap R Rₘ) : (a : R) → Q) x : Q)

Tactic:
simp
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u_1
S : Type u_2
Rₘ : Type u_3
Sₘ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
M_1 : Submonoid R
inst_4 : Algebra R S
inst_5 : Algebra R Sₘ
inst_6 : Algebra S Sₘ
inst_7 : Algebra R Rₘ
inst_8 : Algebra Rₘ Sₘ
inst_9 : IsScalarTower R Rₘ Sₘ
inst_10 : IsScalarTower R S Sₘ
inst_11 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M_1) Sₘ
inst_12 : FormallyUnramified R S
M : Submonoid S
⊢ FormallyUnramified.{u_2, u_1} R (Localization (M := S) M)

Tactic:
have := of_isLocalization (Rₘ := Localization M) M
  .comp _ S _

Premises used: Algebra.FormallyUnramified.comp, Localization, Algebra.FormallyUnramified.of_isLocalization
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u_1
Rₘ : Type u_3
Sₘ : Type u_4
inst : CommRing R
inst_1 : CommRing Rₘ
inst_2 : CommRing Sₘ
M : Submonoid R
inst_3 : Algebra R Sₘ
inst_4 : Algebra R Rₘ
inst_5 : Algebra Rₘ Sₘ
inst_6 : IsScalarTower R Rₘ Sₘ
inst_7 : FormallyUnramified R Sₘ
⊢ FormallyUnramified Rₘ Sₘ

Tactic:
FormallyUnramified.of_restrictScalars R Rₘ Sₘ

Premises used: Algebra.FormallyUnramified.of_restrictScalars
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u_1
S : Type u_2
Rₘ : Type u_3
Sₘ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
M : Submonoid R
inst_4 : Algebra R S
inst_5 : Algebra R Sₘ
inst_6 : Algebra S Sₘ
inst_7 : Algebra R Rₘ
inst_8 : Algebra Rₘ Sₘ
inst_9 : IsScalarTower R Rₘ Sₘ
inst_10 : IsScalarTower R S Sₘ
inst_11 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) Sₘ
inst_12 : FormallyUnramified R S
⊢ FormallyUnramified S Sₘ

Tactic:
haveI : FormallyUnramified S Sₘ :=
    FormallyUnramified.of_isLocalization (M.map (algebraMap R S))
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u_1
S : Type u_2
Rₘ : Type u_3
Sₘ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
M : Submonoid R
inst_4 : Algebra R S
inst_5 : Algebra R Sₘ
inst_6 : Algebra S Sₘ
inst_7 : Algebra R Rₘ
inst_8 : Algebra Rₘ Sₘ
inst_9 : IsScalarTower R Rₘ Sₘ
inst_10 : IsScalarTower R S Sₘ
inst_11 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) Sₘ
inst_12 : FormallyUnramified R S
this : FormallyUnramified S Sₘ
⊢ FormallyUnramified R Sₘ

Tactic:
haveI : FormallyUnramified R Sₘ := FormallyUnramified.comp R S Sₘ
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u_1
S : Type u_2
Rₘ : Type u_3
Sₘ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
M : Submonoid R
inst_4 : Algebra R S
inst_5 : Algebra R Sₘ
inst_6 : Algebra S Sₘ
inst_7 : Algebra R Rₘ
inst_8 : Algebra Rₘ Sₘ
inst_9 : IsScalarTower R Rₘ Sₘ
inst_10 : IsScalarTower R S Sₘ
inst_11 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) Sₘ
inst_12 : FormallyUnramified R S
this_1 : FormallyUnramified S Sₘ
this : FormallyUnramified R Sₘ
⊢ FormallyUnramified Rₘ Sₘ

Tactic:
FormallyUnramified.localization_base M

Premises used: Algebra.FormallyUnramified.localization_base
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type u_1
S : Type u_2
Rₘ : Type u_3
Sₘ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
M : Submonoid R
inst_4 : Algebra R S
inst_5 : Algebra R Sₘ
inst_6 : Algebra S Sₘ
inst_7 : Algebra R Rₘ
inst_8 : Algebra Rₘ Sₘ
inst_9 : IsScalarTower R Rₘ Sₘ
inst_10 : IsScalarTower R S Sₘ
inst_11 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) Sₘ
inst_12 : FormallyUnramified R S
this_1 : FormallyUnramified S Sₘ
this : FormallyUnramified R Sₘ
⊢ FormallyUnramified Rₘ Sₘ

Tactic:
exact FormallyUnramified.localization_base M

Premises used: Algebra.FormallyUnramified.localization_base
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
inst_4 : FormallyUnramified R S
⊢ ∃ (e : S ⊗[R] S), IsIdempotentElem e ∧ Eq (α := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (S ⊗[R] S ∙ e)

Tactic:
(Ideal.isIdempotentElem_iff_of_fg _ (KaehlerDifferential.ideal_fg R S)).mp <|
      (Ideal.cotangent_subsingleton_iff _).mp <| inferInstanceAs <| Subsingleton Ω[S⁄R]

Premises used: KaehlerDifferential.ideal_fg, Ideal.isIdempotentElem_iff_of_fg, _private.0.Algebra.FormallyUnramified.exists_algEquiv_prod._proof_1, Iff.mp, Ideal.cotangent_subsingleton_iff
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
inst_4 : FormallyUnramified R S
obtain :
  ∀ (e : S ⊗[R] S) (he : IsIdempotentElem e)
    (hsp : Eq (α := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (S ⊗[R] S ∙ e)),
    ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra S T), Nonempty.{u + 1} (S ⊗[R] S ≃ₐ[S] S × T)
⊢ ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra S T), Nonempty.{u + 1} (S ⊗[R] S ≃ₐ[S] S × T)

Tactic:
obtain ⟨e, he, hsp⟩ : ∃ e, IsIdempotentElem e ∧ KaehlerDifferential.ideal R S = S ⊗[R] S ∙ e :=
    (Ideal.isIdempotentElem_iff_of_fg _ (KaehlerDifferential.ideal_fg R S)).mp <|
      (Ideal.cotangent_subsingleton_iff _).mp <| inferInstanceAs <| Subsingleton Ω[S⁄R]

Premises used: KaehlerDifferential.ideal_fg, Ideal.isIdempotentElem_iff_of_fg, KaehlerDifferential.ideal, Iff.mp, Ideal.cotangent_subsingleton_iff
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
inst_4 : FormallyUnramified R S
e : S ⊗[R] S
he : IsIdempotentElem e
hsp : Eq (α := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (S ⊗[R] S ∙ e)
⊢ e + (1 - e) = 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
inst_4 : FormallyUnramified R S
e : S ⊗[R] S
he : IsIdempotentElem e
hsp : Eq (α := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (S ⊗[R] S ∙ e)
⊢ e * (1 - e) = 0

Tactic:
simp [he]
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
inst_4 : FormallyUnramified R S
e : S ⊗[R] S
he : IsIdempotentElem e
hsp : Eq (α := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (S ⊗[R] S ∙ e)
e₁ : S ⊗[R] S ≃ₐ[S]
  HasQuotient.Quotient (S ⊗[R] S) (B := Ideal (S ⊗[R] S)) (Ideal.span {e}) ×
    HasQuotient.Quotient (S ⊗[R] S) (B := Ideal (S ⊗[R] S)) (Ideal.span {1 - e}) :=
  AlgEquiv.prodQuotientOfIsIdempotentElem S he ⋯ ⋯ ⋯
e₂ : HasQuotient.Quotient (S ⊗[R] S) (B := Ideal (S ⊗[R] S)) (Ideal.span {e}) ≃ₐ[S] S :=
  AlgEquiv.trans (Ideal.quotientEquivAlgOfEq S ⋯) (Ideal.quotientKerAlgEquivOfSurjective ⋯)
⊢ ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra S T), Nonempty.{u + 1} (S ⊗[R] S ≃ₐ[S] S × T)

Tactic:
⟨(S ⊗[R] S) ⧸ Ideal.span {1 - e}, inferInstance, inferInstance,
    ⟨e₁.trans (.prodCongr e₂ .refl)⟩⟩

Premises used: AlgEquiv.prodCongr, HSub.hSub, inferInstance, Nonempty.intro, HasQuotient.Quotient, AlgEquiv.trans, Exists.intro, TensorProduct, Ideal.span, AlgEquiv.refl, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
inst_4 : FormallyUnramified R S
e : S ⊗[R] S
he : IsIdempotentElem e
hsp : Eq (α := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (S ⊗[R] S ∙ e)
e₁ : S ⊗[R] S ≃ₐ[S]
  HasQuotient.Quotient (S ⊗[R] S) (B := Ideal (S ⊗[R] S)) (Ideal.span {e}) ×
    HasQuotient.Quotient (S ⊗[R] S) (B := Ideal (S ⊗[R] S)) (Ideal.span {1 - e}) :=
  AlgEquiv.prodQuotientOfIsIdempotentElem S he ⋯ ⋯ ⋯
e₂ : HasQuotient.Quotient (S ⊗[R] S) (B := Ideal (S ⊗[R] S)) (Ideal.span {e}) ≃ₐ[S] S :=
  AlgEquiv.trans (Ideal.quotientEquivAlgOfEq S ⋯) (Ideal.quotientKerAlgEquivOfSurjective ⋯)
⊢ ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra S T), Nonempty.{u + 1} (S ⊗[R] S ≃ₐ[S] S × T)

Tactic:
exact ⟨(S ⊗[R] S) ⧸ Ideal.span {1 - e}, inferInstance, inferInstance,
    ⟨e₁.trans (.prodCongr e₂ .refl)⟩⟩