awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
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_1 : Type u_1
P : Type u_2
C_1 : Type u_3
inst_3 : CommRing B_1
inst_4 : Algebra R_1 B_1
inst_5 : CommRing C_1
inst_6 : Algebra R_1 C_1
inst_7 : CommRing P
inst_8 : Algebra R_1 P
R : Type u_4
inst_9 : CommRing R
A : Type u_5
inst_10 : CommRing A
inst_11 : Algebra R A
B : Type u_6
inst_12 : CommRing B
inst_13 : Algebra R B
inst_14 : FormallySmooth R A
C : Type (max u_5 u_6)
x : CommRing C
x_1 : Algebra B C
I : Ideal C
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : B ⊗[R] A →ₐ[B] C ⧸ I
this_1 : Algebra R C :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (algebraMap R B))
this : IsScalarTower R B C
b : B
a : A
refine_2 :
  HSMul.hSMul (β := C ⧸ I) b ((f : (a : B ⊗[R] A) → C ⧸ I) (1 ⊗ₜ[R] a) : C ⧸ I) =
    (f : (a : B ⊗[R] A) → C ⧸ I) (b ⊗ₜ[R] a)
refine_2₁ :
  Eq (α := C ⧸ I) ((f : (a : B ⊗[R] A) → C ⧸ I) (HSMul.hSMul (β := B ⊗[R] A) b (1 ⊗ₜ[R] a)) : C ⧸ I)
    ((f : (a : B ⊗[R] A) → C ⧸ I) (b ⊗ₜ[R] a) : C ⧸ I)
refine_2₂ :
  Eq (α := C ⧸ I) ((f : (a : B ⊗[R] A) → C ⧸ I) (HSMul.hSMul (β := B) b 1 ⊗ₜ[R] a) : C ⧸ I)
    ((f : (a : B ⊗[R] A) → C ⧸ I) (b ⊗ₜ[R] a) : C ⧸ I)
⊢ HMul.hMul (α := C ⧸ I) (β := C ⧸ I) ((algebraMap B (C ⧸ I) : (a : B) → C ⧸ I) b : C ⧸ I)
      ((f : (a : B ⊗[R] A) → C ⧸ I) (1 ⊗ₜ[R] a) : C ⧸ I) =
    (f : (a : B ⊗[R] A) → C ⧸ I) (b ⊗ₜ[R] a)
have refine_2₃ : Eq (α := C ⧸ I) ((f : (a : B ⊗[R] A) → C ⧸ I) ((b * 1) ⊗ₜ[R] a) : C ⧸ I)
  ((f : (a : B ⊗[R] A) → C ⧸ I) (b ⊗ₜ[R] a) : C ⧸ I)
Tactic: rw [← Algebra.smul_def, ← map_smul, TensorProduct.smul_tmul', smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
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_1 : Type u_1
P : Type u_2
C_1 : Type u_3
inst_3 : CommRing B_1
inst_4 : Algebra R_1 B_1
inst_5 : CommRing C_1
inst_6 : Algebra R_1 C_1
inst_7 : CommRing P
inst_8 : Algebra R_1 P
R : Type u_4
inst_9 : CommRing R
A : Type u_5
inst_10 : CommRing A
inst_11 : Algebra R A
B : Type u_6
inst_12 : CommRing B
inst_13 : Algebra R B
inst_14 : FormallySmooth R A
C : Type (max u_5 u_6)
x : CommRing C
x_1 : Algebra B C
I : Ideal C
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : B ⊗[R] A →ₐ[B] C ⧸ I
this_1 : Algebra R C :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (algebraMap R B))
this : IsScalarTower R B C
b : B
a : A
refine_2 :
  HSMul.hSMul (β := C ⧸ I) b ((f : (a : B ⊗[R] A) → C ⧸ I) (1 ⊗ₜ[R] a) : C ⧸ I) =
    (f : (a : B ⊗[R] A) → C ⧸ I) (b ⊗ₜ[R] a)
refine_2₁ :
  Eq (α := C ⧸ I) ((f : (a : B ⊗[R] A) → C ⧸ I) (HSMul.hSMul (β := B ⊗[R] A) b (1 ⊗ₜ[R] a)) : C ⧸ I)
    ((f : (a : B ⊗[R] A) → C ⧸ I) (b ⊗ₜ[R] a) : C ⧸ I)
refine_2₂ :
  Eq (α := C ⧸ I) ((f : (a : B ⊗[R] A) → C ⧸ I) (HSMul.hSMul (β := B) b 1 ⊗ₜ[R] a) : C ⧸ I)
    ((f : (a : B ⊗[R] A) → C ⧸ I) (b ⊗ₜ[R] a) : C ⧸ I)
refine_2₃ :
  Eq (α := C ⧸ I) ((f : (a : B ⊗[R] A) → C ⧸ I) ((b * 1) ⊗ₜ[R] a) : C ⧸ I)
    ((f : (a : B ⊗[R] A) → C ⧸ I) (b ⊗ₜ[R] a) : C ⧸ I)
⊢ HMul.hMul (α := C ⧸ I) (β := C ⧸ I) ((algebraMap B (C ⧸ I) : (a : B) → C ⧸ I) b : C ⧸ I)
      ((f : (a : B ⊗[R] A) → C ⧸ I) (1 ⊗ₜ[R] a) : C ⧸ I) =
    (f : (a : B ⊗[R] A) → C ⧸ I) (b ⊗ₜ[R] a)
have refine_2₄ : Eq (α := C ⧸ I) ((f : (a : B ⊗[R] A) → C ⧸ I) (b ⊗ₜ[R] a) : C ⧸ I) ((f : (a : B ⊗[R] A) → C ⧸ I) (b ⊗ₜ[R] a) : C ⧸ I)
Tactic: rw [← Algebra.smul_def, ← map_smul, TensorProduct.smul_tmul', smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
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ₘ
⊢ FormallySmooth R Rₘ
have refine : ∀ (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), ∃ (a : Rₘ →ₐ[R] Q), AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f
Tactic: refine .of_comp_surjective fun Q _ _ I e f ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
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) ((algebraMap R Q : (a : R) → Q) (↑x : R) : Q)
have apply : IsUnit (M := Q ⧸ I) ((Ideal.Quotient.mk I : (a : Q) → Q ⧸ I) ((algebraMap R Q : (a : R) → Q) (↑x : R)) : Q ⧸ I)
Tactic: apply (IsNilpotent.isUnit_quotient_mk_iff ⟨2, e⟩).mp
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
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) ((Ideal.Quotient.mk I : (a : Q) → Q ⧸ I) ((algebraMap R Q : (a : R) → Q) (↑x : R)) : Q ⧸ I)
have 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)
Tactic: convert! (IsLocalization.map_units Rₘ x).map f
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (hypothesis)
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
⊢ ∃ (a : Rₘ →ₐ[R] Q), AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f
have this : ∀ (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]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
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' := ⋯ }
⊢ ∃ (a : Rₘ →ₐ[R] Q), AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f
have h : AlgHom.comp (Ideal.Quotient.mkₐ R I) this = f
Tactic: use this
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
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' := ⋯ }
⊢ AlgHom.comp (Ideal.Quotient.mkₐ R I) this = f
have h : Eq (α := Rₘ →+* Q ⧸ I) (↑(AlgHom.comp (Ideal.Quotient.mkₐ R I) this) : Rₘ →+* Q ⧸ I) (↑f : Rₘ →+* Q ⧸ I)
Tactic: apply AlgHom.coe_ringHom_injective
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
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)
have 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ₘ))
Tactic: refine IsLocalization.ringHom_ext M ?_
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
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)
    (@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ₘ))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
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ₘ
have 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
Tactic: refine .of_comp_surjective fun Q _ _ I e f ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
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 := ⋯
⊢ Sₘ →ₐ[Rₘ] Q
have refine : ∀ (r : Rₘ),
  (↑(↑(AlgHom.toRingHom (lift I sorry (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: refine { FormallySmooth.lift I ⟨2, e⟩ (f.restrictScalars R) with commutes' := ?_ }
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
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ₘ
⊢ (↑(↑(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
have I₁ : Eq (α := Q)
  ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(lift I sorry (AlgHom.restrictScalars R f)) : Sₘ →+* Q)
          (algebraMap Rₘ Sₘ) :
        (a : Rₘ) → Q)
      r :
    Q)
  ((algebraMap Rₘ Q : (a : Rₘ) → Q) r : Q)
Tactic: change
      (RingHom.comp (FormallySmooth.lift I ⟨2, e⟩ (f.restrictScalars R) : Sₘ →+* Q)
            (algebraMap _ _))
          r =
        algebraMap _ _ r
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
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 (α := 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)
have e_a : Eq (α := Rₘ →+* Q)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(lift I sorry (AlgHom.restrictScalars R f)) : Sₘ →+* Q)
    (algebraMap Rₘ Sₘ))
  (algebraMap Rₘ Q)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
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)
have e_a : Eq (α := R →+* Q)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(lift I sorry (AlgHom.restrictScalars R f)) : Sₘ →+* Q)
      (algebraMap Rₘ Sₘ))
    (algebraMap R Rₘ))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ Q) (algebraMap R Rₘ))
Tactic: refine IsLocalization.ringHom_ext M ?_
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
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 _
      (@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ₘ))
have e_a : Eq (α := R →+* Q)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(lift I sorry (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ₘ))
Tactic: rw [RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq,
      AlgHom.comp_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
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ₘ))
⊢ 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ₘ))
have e_a₁ : Eq (α := R →+* Q)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(lift I sorry (AlgHom.restrictScalars R f)) : Sₘ →+* Q)
    (algebraMap R Sₘ))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ Q) (algebraMap R Rₘ))
Tactic: rw [RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq,
      AlgHom.comp_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
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ₘ))
⊢ 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ₘ))
have e_a₂ : Eq (α := R →+* Q)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(lift I sorry (AlgHom.restrictScalars R f)) : Sₘ →+* Q)
    (algebraMap R Sₘ))
  (algebraMap R Q)
Tactic: rw [RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq,
      AlgHom.comp_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
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)
⊢ 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ₘ))
have e_a₃ : Eq (α := R →+* Q) (algebraMap R Q) (algebraMap R Q)
Tactic: rw [RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq,
      AlgHom.comp_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
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' := ⋯ }
⊢ ∃ (a : Sₘ →ₐ[Rₘ] Q), AlgHom.comp (Ideal.Quotient.mkₐ Rₘ I) a = f_1
have h : AlgHom.comp (Ideal.Quotient.mkₐ Rₘ I) f = f_1
Tactic: use f
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
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' := ⋯ }
⊢ AlgHom.comp (Ideal.Quotient.mkₐ Rₘ I) f = f_1
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (hypothesis)
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 Rₘ Sₘ
have this : FormallySmooth A Sₘ
Tactic: haveI : FormallySmooth A Sₘ := FormallySmooth.of_isLocalization (M.map (algebraMap R A))