awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u_4
Rₘ : Type u_6
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
Q : Type (max u_4 u_6)
x_1 : CommRing Q
x_2 : Algebra R Q
I : Ideal Q
e : HPow.hPow (β := ℕ) I 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
x : ↥M
apply : IsUnit (M := Q ⧸ I) ((Ideal.Quotient.mk I : (a : Q) → Q ⧸ I) ((algebraMap R Q : (a : R) → Q) (↑x : R)) : Q ⧸ I)
⊢ IsUnit (M := Q) ((algebraMap R Q : (a : R) → Q) (↑x : R) : Q)

Tactic:
apply (IsNilpotent.isUnit_quotient_mk_iff ⟨2, e⟩).mp

Premises used: Exists.intro, Iff.mp, OfNat.ofNat, IsNilpotent.isUnit_quotient_mk_iff
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u_4
Rₘ : Type u_6
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
Q : Type (max u_4 u_6)
x_1 : CommRing Q
x_2 : Algebra R Q
I : Ideal Q
e : HPow.hPow (β := ℕ) I 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
x : ↥M
⊢ IsUnit (M := Q ⧸ I) ((f : (a : Rₘ) → Q ⧸ I) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑x : R)) : Q ⧸ I)

Tactic:
(IsLocalization.map_units Rₘ x).map f

Premises used: IsLocalization.map_units, IsUnit.map
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u_4
Rₘ : Type u_6
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
Q : Type (max u_4 u_6)
x_1 : CommRing Q
x_2 : Algebra R Q
I : Ideal Q
e : HPow.hPow (β := ℕ) I 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
x : ↥M
h :
  Eq (α := Q ⧸ I) ((Ideal.Quotient.mk I : (a : Q) → Q ⧸ I) ((algebraMap R Q : (a : R) → Q) (↑x : R)) : Q ⧸ I)
    ((f : (a : Rₘ) → Q ⧸ I) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑x : R)) : Q ⧸ I)
⊢ IsUnit (M := Q ⧸ I) ((Ideal.Quotient.mk I : (a : Q) → Q ⧸ I) ((algebraMap R Q : (a : R) → Q) (↑x : R)) : Q ⧸ I)

Tactic:
convert! (IsLocalization.map_units Rₘ x).map f

Premises used: IsLocalization.map_units, IsUnit.map
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u_4
Rₘ : Type u_6
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
Q : Type (max u_4 u_6)
x_1 : CommRing Q
x_2 : Algebra R Q
I : Ideal Q
e : HPow.hPow (β := ℕ) I 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
x : ↥M
⊢ Eq (α := Q ⧸ I) ((Ideal.Quotient.mk I : (a : Q) → Q ⧸ I) ((algebraMap R Q : (a : R) → Q) (↑x : R)) : Q ⧸ I)
    ((f : (a : Rₘ) → Q ⧸ I) ((algebraMap R Rₘ : (a : R) → Rₘ) (↑x : R)) : Q ⧸ I)

Tactic:
simp only [Ideal.Quotient.mk_algebraMap, AlgHom.commutes]

Premises used: AlgHom.commutes, Ideal.Quotient.mk_algebraMap
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u_4
Rₘ : Type u_6
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
Q : Type (max u_4 u_6)
x : CommRing Q
x_1 : Algebra R Q
I : Ideal Q
e : HPow.hPow (β := ℕ) I 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
⊢ ∀ (x_2 : ↥M), IsUnit (M := Q) ((algebraMap R Q : (a : R) → Q) (↑x_2 : R) : Q)

Tactic:
have : ∀ x : M, IsUnit (algebraMap R Q x) := by
    intro x
    apply (IsNilpotent.isUnit_quotient_mk_iff ⟨2, e⟩).mp
    convert! (IsLocalization.map_units Rₘ x).map f
    simp only [Ideal.Quotient.mk_algebraMap, AlgHom.commutes]
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u_4
Rₘ : Type u_6
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
Q : Type (max u_4 u_6)
x : CommRing Q
x_1 : Algebra R Q
I : Ideal Q
e : HPow.hPow (β := ℕ) I 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
this_1 : ∀ (x_2 : ↥M), IsUnit (M := Q) ((algebraMap R Q : (a : R) → Q) (↑x_2 : R) : Q)
this : Rₘ →ₐ[R] Q :=
  let __src : Rₘ →+* Q := IsLocalization.lift this_1;
  { toRingHom := __src, commutes' := ⋯ }
h : AlgHom.comp (Ideal.Quotient.mkₐ R I) this = f
⊢ ∃ (a : Rₘ →ₐ[R] Q), AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f

Tactic:
use this
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u_4
Rₘ : Type u_6
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
Q : Type (max u_4 u_6)
x : CommRing Q
x_1 : Algebra R Q
I : Ideal Q
e : HPow.hPow (β := ℕ) I 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
this_1 : ∀ (x_2 : ↥M), IsUnit (M := Q) ((algebraMap R Q : (a : R) → Q) (↑x_2 : R) : Q)
this : Rₘ →ₐ[R] Q :=
  let __src : Rₘ →+* Q := IsLocalization.lift this_1;
  { toRingHom := __src, commutes' := ⋯ }
h : Eq (α := Rₘ →+* Q ⧸ I) (↑(AlgHom.comp (Ideal.Quotient.mkₐ R I) this) : Rₘ →+* Q ⧸ I) (↑f : Rₘ →+* Q ⧸ I)
⊢ AlgHom.comp (Ideal.Quotient.mkₐ R I) this = f

Tactic:
apply AlgHom.coe_ringHom_injective

Premises used: AlgHom.coe_ringHom_injective
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u_4
Rₘ : Type u_6
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
Q : Type (max u_4 u_6)
x : CommRing Q
x_1 : Algebra R Q
I : Ideal Q
e : HPow.hPow (β := ℕ) I 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
this_1 : ∀ (x_2 : ↥M), IsUnit (M := Q) ((algebraMap R Q : (a : R) → Q) (↑x_2 : R) : Q)
this : Rₘ →ₐ[R] Q :=
  let __src : Rₘ →+* Q := IsLocalization.lift this_1;
  { toRingHom := __src, commutes' := ⋯ }
⊢ Eq (α := Rₘ →+* Q ⧸ I) (↑(AlgHom.comp (Ideal.Quotient.mkₐ R I) this) : Rₘ →+* Q ⧸ I) (↑f : Rₘ →+* Q ⧸ I)

Tactic:
IsLocalization.ringHom_ext M ?_

Premises used: IsLocalization.ringHom_ext
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u_4
Rₘ : Type u_6
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
Q : Type (max u_4 u_6)
x : CommRing Q
x_1 : Algebra R Q
I : Ideal Q
e : HPow.hPow (β := ℕ) I 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
this_1 : ∀ (x_2 : ↥M), IsUnit (M := Q) ((algebraMap R Q : (a : R) → Q) (↑x_2 : R) : Q)
this : Rₘ →ₐ[R] Q :=
  let __src : Rₘ →+* Q := IsLocalization.lift this_1;
  { toRingHom := __src, commutes' := ⋯ }
h :
  Eq (α := R →+* Q ⧸ I)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(AlgHom.comp (Ideal.Quotient.mkₐ R I) this) : Rₘ →+* Q ⧸ I)
      (algebraMap R Rₘ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : Rₘ →+* Q ⧸ I) (algebraMap R Rₘ))
⊢ Eq (α := Rₘ →+* Q ⧸ I) (↑(AlgHom.comp (Ideal.Quotient.mkₐ R I) this) : Rₘ →+* Q ⧸ I) (↑f : Rₘ →+* Q ⧸ I)

Tactic:
refine IsLocalization.ringHom_ext M ?_

Premises used: IsLocalization.ringHom_ext
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u_4
Rₘ : Type u_6
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
Q : Type (max u_4 u_6)
x : CommRing Q
x_1 : Algebra R Q
I : Ideal Q
e : HPow.hPow (β := ℕ) I 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
this_1 : ∀ (x_2 : ↥M), IsUnit (M := Q) ((algebraMap R Q : (a : R) → Q) (↑x_2 : R) : Q)
this : Rₘ →ₐ[R] Q :=
  let __src : Rₘ →+* Q := IsLocalization.lift this_1;
  { toRingHom := __src, commutes' := ⋯ }
h :
  ∀ (x_2 : R),
    Eq (α := Q ⧸ I)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              (↑(AlgHom.comp (Ideal.Quotient.mkₐ R I) this) : Rₘ →+* Q ⧸ I) (algebraMap R Rₘ) :
            (a : R) → Q ⧸ I)
          x_2 :
        Q ⧸ I)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : Rₘ →+* Q ⧸ I) (algebraMap R Rₘ) : (a : R) → Q ⧸ I)
          x_2 :
        Q ⧸ I)
⊢ Eq (α := R →+* Q ⧸ I)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(AlgHom.comp (Ideal.Quotient.mkₐ R I) this) : Rₘ →+* Q ⧸ I)
      (algebraMap R Rₘ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : Rₘ →+* Q ⧸ I) (algebraMap R Rₘ))

Tactic:
ext
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u_4
Rₘ : Type u_6
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
Q : Type (max u_4 u_6)
x : CommRing Q
x_1 : Algebra R Q
I : Ideal Q
e : HPow.hPow (β := ℕ) I 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
this_1 : ∀ (x_3 : ↥M), IsUnit (M := Q) ((algebraMap R Q : (a : R) → Q) (↑x_3 : R) : Q)
this : Rₘ →ₐ[R] Q :=
  let __src : Rₘ →+* Q := IsLocalization.lift this_1;
  { toRingHom := __src, commutes' := ⋯ }
x_2 : R
⊢ Eq (α := Q ⧸ I)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(AlgHom.comp (Ideal.Quotient.mkₐ R I) this) : Rₘ →+* Q ⧸ I)
            (algebraMap R Rₘ) :
          (a : R) → Q ⧸ I)
        x_2 :
      Q ⧸ I)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : Rₘ →+* Q ⧸ I) (algebraMap R Rₘ) : (a : R) → Q ⧸ I) x_2 :
      Q ⧸ I)

Tactic:
simp
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R_1 : Type u
A_1 : Type v
inst : CommRing R_1
inst_1 : CommRing A_1
inst_2 : Algebra R_1 A_1
B : Type u_1
P : Type u_2
C : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R_1 B
inst_5 : CommRing C
inst_6 : Algebra R_1 C
inst_7 : CommRing P
inst_8 : Algebra R_1 P
R : Type u_4
A : Type u_5
Rₘ : Type u_6
Sₘ : Type u_7
inst_9 : CommRing R
inst_10 : CommRing A
inst_11 : CommRing Rₘ
inst_12 : CommRing Sₘ
M_1 : Submonoid R
inst_13 : Algebra R A
inst_14 : Algebra R Sₘ
inst_15 : Algebra A Sₘ
inst_16 : Algebra R Rₘ
inst_17 : Algebra Rₘ Sₘ
inst_18 : IsScalarTower R Rₘ Sₘ
inst_19 : IsScalarTower R A Sₘ
inst_20 : IsLocalization M_1 Rₘ
inst_21 : IsLocalization (Submonoid.map (F := R →+* A) (algebraMap R A) M_1) Sₘ
inst_22 : FormallySmooth R A
M : Submonoid A
⊢ FormallySmooth.{u_4, u_5} R (Localization (M := A) M)

Tactic:
have : FormallySmooth A (Localization M) := of_isLocalization M
  .comp _ A _

Premises used: Algebra.FormallySmooth.of_isLocalization, Localization, Algebra.FormallySmooth.comp
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u_4
Rₘ : Type u_6
Sₘ : Type u_7
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 : IsLocalization M Rₘ
inst_8 : FormallySmooth R Sₘ
⊢ FormallySmooth Rₘ Sₘ

Tactic:
.of_comp_surjective fun Q _ _ I e f ↦ ?_

Premises used: Algebra.FormallySmooth.of_comp_surjective
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u_4
Rₘ : Type u_6
Sₘ : Type u_7
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 : IsLocalization M Rₘ
inst_8 : FormallySmooth R Sₘ
refine :
  ∀ (Q : Type (max u_6 u_7)) (x : CommRing Q) (x_1 : Algebra Rₘ Q) (I : Ideal Q) (e : HPow.hPow (β := ℕ) I 2 = ⊥)
    (f : Sₘ →ₐ[Rₘ] Q ⧸ I), ∃ (a : Sₘ →ₐ[Rₘ] Q), AlgHom.comp (Ideal.Quotient.mkₐ Rₘ I) a = f
⊢ FormallySmooth Rₘ Sₘ

Tactic:
refine .of_comp_surjective fun Q _ _ I e f ↦ ?_
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u_4
Rₘ : Type u_6
Sₘ : Type u_7
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 : IsLocalization M Rₘ
inst_8 : FormallySmooth R Sₘ
Q : Type (max u_6 u_7)
x : CommRing Q
x_1 : Algebra Rₘ Q
I : Ideal Q
e : HPow.hPow (β := ℕ) I 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
this_1 : Algebra R Q :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ Q) (algebraMap R Rₘ))
this : IsScalarTower R Rₘ Q := ⋯
refine :
  ∀ (r : Rₘ),
    (↑(↑(AlgHom.toRingHom (lift I ⋯ (AlgHom.restrictScalars R f))) : Sₘ →* Q) : OneHom Sₘ Q).toFun
        ((algebraMap Rₘ Sₘ : (a : Rₘ) → Sₘ) r) =
      (algebraMap Rₘ Q : (a : Rₘ) → Q) r
⊢ Sₘ →ₐ[Rₘ] Q

Tactic:
refine { FormallySmooth.lift I ⟨2, e⟩ (f.restrictScalars R) with commutes' := ?_ }

Premises used: AlgHom.restrictScalars, Algebra.FormallySmooth.lift, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u_4
Rₘ : Type u_6
Sₘ : Type u_7
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 : IsLocalization M Rₘ
inst_8 : FormallySmooth R Sₘ
Q : Type (max u_6 u_7)
x : CommRing Q
x_1 : Algebra Rₘ Q
I : Ideal Q
e : HPow.hPow (β := ℕ) I 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
this_1 : Algebra R Q :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ Q) (algebraMap R Rₘ))
this : IsScalarTower R Rₘ Q := ⋯
r : Rₘ
I₁ :
  Eq (α := Q)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(lift I ⋯ (AlgHom.restrictScalars R f)) : Sₘ →+* Q)
            (algebraMap Rₘ Sₘ) :
          (a : Rₘ) → Q)
        r :
      Q)
    ((algebraMap Rₘ Q : (a : Rₘ) → Q) r : Q)
⊢ (↑(↑(AlgHom.toRingHom (lift I ⋯ (AlgHom.restrictScalars R f))) : Sₘ →* Q) : OneHom Sₘ Q).toFun
      ((algebraMap Rₘ Sₘ : (a : Rₘ) → Sₘ) r) =
    (algebraMap Rₘ Q : (a : Rₘ) → Q) r

Tactic:
change
      (RingHom.comp (FormallySmooth.lift I ⟨2, e⟩ (f.restrictScalars R) : Sₘ →+* Q)
            (algebraMap _ _))
          r =
        algebraMap _ _ r

Premises used: Algebra.algebraMap, RingHom.comp, AlgHom.restrictScalars, Algebra.FormallySmooth.lift, RingHomClass.toRingHom, Exists.intro, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u_4
Rₘ : Type u_6
Sₘ : Type u_7
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 : IsLocalization M Rₘ
inst_8 : FormallySmooth R Sₘ
Q : Type (max u_6 u_7)
x : CommRing Q
x_1 : Algebra Rₘ Q
I : Ideal Q
e : HPow.hPow (β := ℕ) I 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
this_1 : Algebra R Q :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ Q) (algebraMap R Rₘ))
this : IsScalarTower R Rₘ Q := ⋯
r : Rₘ
e_a :
  Eq (α := Rₘ →+* Q)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(lift I ⋯ (AlgHom.restrictScalars R f)) : Sₘ →+* Q)
      (algebraMap Rₘ Sₘ))
    (algebraMap Rₘ Q)
⊢ Eq (α := Q)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(lift I ⋯ (AlgHom.restrictScalars R f)) : Sₘ →+* Q)
            (algebraMap Rₘ Sₘ) :
          (a : Rₘ) → Q)
        r :
      Q)
    ((algebraMap Rₘ Q : (a : Rₘ) → Q) r : Q)

Tactic:
congr 1
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u_4
Rₘ : Type u_6
Sₘ : Type u_7
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 : IsLocalization M Rₘ
inst_8 : FormallySmooth R Sₘ
Q : Type (max u_6 u_7)
x : CommRing Q
x_1 : Algebra Rₘ Q
I : Ideal Q
e : HPow.hPow (β := ℕ) I 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
this_1 : Algebra R Q :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ Q) (algebraMap R Rₘ))
this : IsScalarTower R Rₘ Q := ⋯
r : Rₘ
⊢ Eq (α := Rₘ →+* Q)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(lift I ⋯ (AlgHom.restrictScalars R f)) : Sₘ →+* Q)
      (algebraMap Rₘ Sₘ))
    (algebraMap Rₘ Q)

Tactic:
IsLocalization.ringHom_ext M ?_

Premises used: IsLocalization.ringHom_ext
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u_4
Rₘ : Type u_6
Sₘ : Type u_7
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 : IsLocalization M Rₘ
inst_8 : FormallySmooth R Sₘ
Q : Type (max u_6 u_7)
x : CommRing Q
x_1 : Algebra Rₘ Q
I : Ideal Q
e : HPow.hPow (β := ℕ) I 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
this_1 : Algebra R Q :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ Q) (algebraMap R Rₘ))
this : IsScalarTower R Rₘ Q := ⋯
r : Rₘ
e_a :
  Eq (α := R →+* Q)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(lift I ⋯ (AlgHom.restrictScalars R f)) : Sₘ →+* Q)
        (algebraMap Rₘ Sₘ))
      (algebraMap R Rₘ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ Q) (algebraMap R Rₘ))
⊢ Eq (α := Rₘ →+* Q)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(lift I ⋯ (AlgHom.restrictScalars R f)) : Sₘ →+* Q)
      (algebraMap Rₘ Sₘ))
    (algebraMap Rₘ Q)

Tactic:
refine IsLocalization.ringHom_ext M ?_

Premises used: IsLocalization.ringHom_ext
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u_4
Rₘ : Type u_6
Sₘ : Type u_7
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 : IsLocalization M Rₘ
inst_8 : FormallySmooth R Sₘ
Q : Type (max u_6 u_7)
x : CommRing Q
x_1 : Algebra Rₘ Q
I : Ideal Q
e : HPow.hPow (β := ℕ) I 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
this_1 : Algebra R Q :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ Q) (algebraMap R Rₘ))
this : IsScalarTower R Rₘ Q := ⋯
r : Rₘ
e_a :
  Eq (α := R →+* Q)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(lift I ⋯ (AlgHom.restrictScalars R f)) : Sₘ →+* Q)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ Sₘ) (algebraMap R Rₘ)))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ Q) (algebraMap R Rₘ))
e_a₁ :
  Eq (α := R →+* Q)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(lift I ⋯ (AlgHom.restrictScalars R f)) : Sₘ →+* Q)
      (algebraMap R Sₘ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ Q) (algebraMap R Rₘ))
e_a₂ :
  Eq (α := R →+* Q)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(lift I ⋯ (AlgHom.restrictScalars R f)) : Sₘ →+* Q)
      (algebraMap R Sₘ))
    (algebraMap R Q)
e_a₃ e_a₄ : Eq (α := R →+* Q) (algebraMap R Q) (algebraMap R Q)
⊢ Eq (α := R →+* Q)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(lift I ⋯ (AlgHom.restrictScalars R f)) : Sₘ →+* Q)
        (algebraMap Rₘ Sₘ))
      (algebraMap R Rₘ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ Q) (algebraMap R Rₘ))

Tactic:
rw [RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq,
      AlgHom.comp_algebraMap]

Premises used: AlgHom.comp_algebraMap, RingHom.comp_assoc, IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u_4
Rₘ : Type u_6
Sₘ : Type u_7
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 : IsLocalization M Rₘ
inst_8 : FormallySmooth R Sₘ
Q : Type (max u_6 u_7)
x : CommRing Q
x_1 : Algebra Rₘ Q
I : Ideal Q
e : HPow.hPow (β := ℕ) I 2 = ⊥
f_1 : Sₘ →ₐ[Rₘ] Q ⧸ I
this_1 : Algebra R Q :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ Q) (algebraMap R Rₘ))
this : IsScalarTower R Rₘ Q := ⋯
f : Sₘ →ₐ[Rₘ] Q :=
  let __src : Sₘ →ₐ[R] Q := lift I ⋯ (AlgHom.restrictScalars R f_1);
  { toRingHom := __src.toRingHom, commutes' := ⋯ }
h : AlgHom.comp (Ideal.Quotient.mkₐ Rₘ I) f = f_1
⊢ ∃ (a : Sₘ →ₐ[Rₘ] Q), AlgHom.comp (Ideal.Quotient.mkₐ Rₘ I) a = f_1

Tactic:
use f
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u_4
Rₘ : Type u_6
Sₘ : Type u_7
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 : IsLocalization M Rₘ
inst_8 : FormallySmooth R Sₘ
Q : Type (max u_6 u_7)
x : CommRing Q
x_1 : Algebra Rₘ Q
I : Ideal Q
e : HPow.hPow (β := ℕ) I 2 = ⊥
f_1 : Sₘ →ₐ[Rₘ] Q ⧸ I
this_1 : Algebra R Q :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ Q) (algebraMap R Rₘ))
this : IsScalarTower R Rₘ Q := ⋯
f : Sₘ →ₐ[Rₘ] Q :=
  let __src : Sₘ →ₐ[R] Q := lift I ⋯ (AlgHom.restrictScalars R f_1);
  { toRingHom := __src.toRingHom, commutes' := ⋯ }
h :
  ∀ (x_2 : Sₘ),
    Eq (α := Q ⧸ I) ((AlgHom.comp (Ideal.Quotient.mkₐ Rₘ I) f : (a : Sₘ) → Q ⧸ I) x_2 : Q ⧸ I)
      ((f_1 : (a : Sₘ) → Q ⧸ I) x_2 : Q ⧸ I)
⊢ AlgHom.comp (Ideal.Quotient.mkₐ Rₘ I) f = f_1

Tactic:
ext
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u_4
Rₘ : Type u_6
Sₘ : Type u_7
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 : IsLocalization M Rₘ
inst_8 : FormallySmooth R Sₘ
Q : Type (max u_6 u_7)
x : CommRing Q
x_1 : Algebra Rₘ Q
I : Ideal Q
e : HPow.hPow (β := ℕ) I 2 = ⊥
f_1 : Sₘ →ₐ[Rₘ] Q ⧸ I
this_1 : Algebra R Q :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ Q) (algebraMap R Rₘ))
this : IsScalarTower R Rₘ Q := ⋯
f : Sₘ →ₐ[Rₘ] Q :=
  let __src : Sₘ →ₐ[R] Q := lift I ⋯ (AlgHom.restrictScalars R f_1);
  { toRingHom := __src.toRingHom, commutes' := ⋯ }
x_2 : Sₘ
⊢ Eq (α := Q ⧸ I) ((AlgHom.comp (Ideal.Quotient.mkₐ Rₘ I) f : (a : Sₘ) → Q ⧸ I) x_2 : Q ⧸ I)
    ((f_1 : (a : Sₘ) → Q ⧸ I) x_2 : Q ⧸ I)

Tactic:
simp [f]
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u_4
A : Type u_5
Rₘ : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
M : Submonoid R
inst_4 : Algebra R A
inst_5 : Algebra R Sₘ
inst_6 : Algebra A Sₘ
inst_7 : Algebra R Rₘ
inst_8 : Algebra Rₘ Sₘ
inst_9 : IsScalarTower R Rₘ Sₘ
inst_10 : IsScalarTower R A Sₘ
inst_11 : IsLocalization M Rₘ
inst_12 : IsLocalization (Submonoid.map (F := R →+* A) (algebraMap R A) M) Sₘ
inst_13 : FormallySmooth R A
⊢ FormallySmooth A Sₘ

Tactic:
haveI : FormallySmooth A Sₘ := FormallySmooth.of_isLocalization (M.map (algebraMap R A))
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u_4
A : Type u_5
Rₘ : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
M : Submonoid R
inst_4 : Algebra R A
inst_5 : Algebra R Sₘ
inst_6 : Algebra A Sₘ
inst_7 : Algebra R Rₘ
inst_8 : Algebra Rₘ Sₘ
inst_9 : IsScalarTower R Rₘ Sₘ
inst_10 : IsScalarTower R A Sₘ
inst_11 : IsLocalization M Rₘ
inst_12 : IsLocalization (Submonoid.map (F := R →+* A) (algebraMap R A) M) Sₘ
inst_13 : FormallySmooth R A
this : FormallySmooth A Sₘ
⊢ FormallySmooth R Sₘ

Tactic:
haveI : FormallySmooth R Sₘ := FormallySmooth.comp R A Sₘ
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u_4
A : Type u_5
Rₘ : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
M : Submonoid R
inst_4 : Algebra R A
inst_5 : Algebra R Sₘ
inst_6 : Algebra A Sₘ
inst_7 : Algebra R Rₘ
inst_8 : Algebra Rₘ Sₘ
inst_9 : IsScalarTower R Rₘ Sₘ
inst_10 : IsScalarTower R A Sₘ
inst_11 : IsLocalization M Rₘ
inst_12 : IsLocalization (Submonoid.map (F := R →+* A) (algebraMap R A) M) Sₘ
inst_13 : FormallySmooth R A
this_1 : FormallySmooth A Sₘ
this : FormallySmooth R Sₘ
⊢ FormallySmooth Rₘ Sₘ

Tactic:
FormallySmooth.localization_base M

Premises used: Algebra.FormallySmooth.localization_base
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u_4
A : Type u_5
Rₘ : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
M : Submonoid R
inst_4 : Algebra R A
inst_5 : Algebra R Sₘ
inst_6 : Algebra A Sₘ
inst_7 : Algebra R Rₘ
inst_8 : Algebra Rₘ Sₘ
inst_9 : IsScalarTower R Rₘ Sₘ
inst_10 : IsScalarTower R A Sₘ
inst_11 : IsLocalization M Rₘ
inst_12 : IsLocalization (Submonoid.map (F := R →+* A) (algebraMap R A) M) Sₘ
inst_13 : FormallySmooth R A
this_1 : FormallySmooth A Sₘ
this : FormallySmooth R Sₘ
⊢ FormallySmooth Rₘ Sₘ

Tactic:
exact FormallySmooth.localization_base M

Premises used: Algebra.FormallySmooth.localization_base