-- Mathlib/RingTheory/Smooth/Basic.lean
theorem localization_base [FormallySmooth R Sₘ] : FormallySmooth Rₘ Sₘ

Proof state:
case comp_surjective
R Rₘ Sₘ : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₘ
inst✝⁸ : CommRing Sₘ
M : Submonoid R
inst✝⁷ : Algebra R Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : FormallySmooth R Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra Rₘ Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
⊢ ∃ a, (Ideal.Quotient.mkₐ Rₘ I).comp a = f

Tactic:
letI := ((algebraMap Rₘ Q).comp (algebraMap R Rₘ)).toAlgebra

Result:
case comp_surjective
R Rₘ Sₘ : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₘ
inst✝⁸ : CommRing Sₘ
M : Submonoid R
inst✝⁷ : Algebra R Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : FormallySmooth R Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra Rₘ Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
this : Algebra R Q := ((algebraMap Rₘ Q).comp (algebraMap R Rₘ)).toAlgebra
⊢ ∃ a, (Ideal.Quotient.mkₐ Rₘ I).comp a = f

Proof state:
R Rₘ Sₘ : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₘ
inst✝⁸ : CommRing Sₘ
M : Submonoid R
inst✝⁷ : Algebra R Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : FormallySmooth R Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra Rₘ Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
this✝ : Algebra R Q := ((algebraMap Rₘ Q).comp (algebraMap R Rₘ)).toAlgebra
this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
⊢ ∀ (r : Rₘ), (↑↑__src✝.toRingHom).toFun ((algebraMap Rₘ Sₘ) r) = (algebraMap Rₘ Q) r

Tactic:
intro r

Result:
R Rₘ Sₘ : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₘ
inst✝⁸ : CommRing Sₘ
M : Submonoid R
inst✝⁷ : Algebra R Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : FormallySmooth R Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra Rₘ Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
this✝ : Algebra R Q := ((algebraMap Rₘ Q).comp (algebraMap R Rₘ)).toAlgebra
this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
r : Rₘ
⊢ (↑↑__src✝.toRingHom).toFun ((algebraMap Rₘ Sₘ) r) = (algebraMap Rₘ Q) r

Proof state:
R Rₘ Sₘ : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₘ
inst✝⁸ : CommRing Sₘ
M : Submonoid R
inst✝⁷ : Algebra R Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : FormallySmooth R Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra Rₘ Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
this✝ : Algebra R Q := ((algebraMap Rₘ Q).comp (algebraMap R Rₘ)).toAlgebra
this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
r : Rₘ
⊢ ((↑(lift I ⋯ (AlgHom.restrictScalars R f))).comp (algebraMap Rₘ Sₘ)) r = (algebraMap Rₘ Q) r

Tactic:
congr 1

Result:
case e_a
R Rₘ Sₘ : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₘ
inst✝⁸ : CommRing Sₘ
M : Submonoid R
inst✝⁷ : Algebra R Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : FormallySmooth R Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra Rₘ Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
this✝ : Algebra R Q := ((algebraMap Rₘ Q).comp (algebraMap R Rₘ)).toAlgebra
this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
r : Rₘ
⊢ (↑(lift I ⋯ (AlgHom.restrictScalars R f))).comp (algebraMap Rₘ Sₘ) = algebraMap Rₘ Q

Proof state:
R Rₘ Sₘ : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₘ
inst✝⁸ : CommRing Sₘ
M : Submonoid R
inst✝⁷ : Algebra R Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : FormallySmooth R Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra Rₘ Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
this✝ : Algebra R Q := ((algebraMap Rₘ Q).comp (algebraMap R Rₘ)).toAlgebra
this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
r : Rₘ
⊢ (↑↑__src✝.toRingHom).toFun ((algebraMap Rₘ Sₘ) r) = (algebraMap Rₘ Q) r

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

Result:
R Rₘ Sₘ : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₘ
inst✝⁸ : CommRing Sₘ
M : Submonoid R
inst✝⁷ : Algebra R Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : FormallySmooth R Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra Rₘ Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
this✝ : Algebra R Q := ((algebraMap Rₘ Q).comp (algebraMap R Rₘ)).toAlgebra
this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
r : Rₘ
⊢ ((↑(lift I ⋯ (AlgHom.restrictScalars R f))).comp (algebraMap Rₘ Sₘ)) r = (algebraMap Rₘ Q) r

Proof state:
R Rₘ Sₘ : Type u
inst✝⁸ : CommRing R
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
M : Submonoid R
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : Algebra R Rₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : IsScalarTower R Rₘ Sₘ
inst✝¹ : IsLocalization M Rₘ
inst✝ : FormallySmooth R Sₘ
⊢ FormallySmooth Rₘ Sₘ

Tactic:
constructor

Result:
case comp_surjective
R Rₘ Sₘ : Type u
inst✝⁸ : CommRing R
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
M : Submonoid R
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : Algebra R Rₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : IsScalarTower R Rₘ Sₘ
inst✝¹ : IsLocalization M Rₘ
inst✝ : FormallySmooth R Sₘ
⊢ ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra Rₘ B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Surjective (Ideal.Quotient.mkₐ Rₘ I).comp

Proof state:
case e_a
R Rₘ Sₘ : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₘ
inst✝⁸ : CommRing Sₘ
M : Submonoid R
inst✝⁷ : Algebra R Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : FormallySmooth R Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra Rₘ Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
this✝ : Algebra R Q := ((algebraMap Rₘ Q).comp (algebraMap R Rₘ)).toAlgebra
this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
r : Rₘ
⊢ (↑(lift I ⋯ (AlgHom.restrictScalars R f))).comp (algebraMap Rₘ Sₘ) = algebraMap Rₘ Q

Tactic:
refine IsLocalization.ringHom_ext M ?_

Result:
case e_a
R Rₘ Sₘ : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₘ
inst✝⁸ : CommRing Sₘ
M : Submonoid R
inst✝⁷ : Algebra R Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : FormallySmooth R Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra Rₘ Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
this✝ : Algebra R Q := ((algebraMap Rₘ Q).comp (algebraMap R Rₘ)).toAlgebra
this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
r : Rₘ
⊢ ((↑(lift I ⋯ (AlgHom.restrictScalars R f))).comp (algebraMap Rₘ Sₘ)).comp (algebraMap R Rₘ) =
    (algebraMap Rₘ Q).comp (algebraMap R Rₘ)