-- 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
this✝ : Algebra R Q := ((algebraMap Rₘ Q).comp (algebraMap R Rₘ)).toAlgebra
this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
f : Sₘ →ₐ[Rₘ] Q :=
  let __src := lift I ⋯ (AlgHom.restrictScalars R f✝);
  { toRingHom := __src.toRingHom, commutes' := ⋯ }
⊢ ∃ a, (Ideal.Quotient.mkₐ Rₘ I).comp a = f✝

Tactic:
use f

Result:
case h
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
f : Sₘ →ₐ[Rₘ] Q :=
  let __src := lift I ⋯ (AlgHom.restrictScalars R f✝);
  { toRingHom := __src.toRingHom, commutes' := ⋯ }
⊢ (Ideal.Quotient.mkₐ Rₘ I).comp f = f✝

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
this : Algebra R Q := ((algebraMap Rₘ Q).comp (algebraMap R Rₘ)).toAlgebra
⊢ ∃ a, (Ideal.Quotient.mkₐ Rₘ I).comp a = f

Tactic:
letI : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl

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
this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
⊢ ∃ a, (Ideal.Quotient.mkₐ Rₘ I).comp a = f

Proof state:
case h.H
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
f : Sₘ →ₐ[Rₘ] Q :=
  let __src := lift I ⋯ (AlgHom.restrictScalars R f✝);
  { toRingHom := __src.toRingHom, commutes' := ⋯ }
x✝ : Sₘ
⊢ ((Ideal.Quotient.mkₐ Rₘ I).comp f) x✝ = f✝ x✝

Tactic:
simp [f]

Result:
no goals

Proof state:
case h
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
f : Sₘ →ₐ[Rₘ] Q :=
  let __src := lift I ⋯ (AlgHom.restrictScalars R f✝);
  { toRingHom := __src.toRingHom, commutes' := ⋯ }
⊢ (Ideal.Quotient.mkₐ Rₘ I).comp f = f✝

Tactic:
ext

Result:
case h.H
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
f : Sₘ →ₐ[Rₘ] Q :=
  let __src := lift I ⋯ (AlgHom.restrictScalars R f✝);
  { toRingHom := __src.toRingHom, commutes' := ⋯ }
x✝ : Sₘ
⊢ ((Ideal.Quotient.mkₐ Rₘ I).comp f) x✝ = f✝ x✝

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ₘ
⊢ ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra Rₘ B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Surjective (Ideal.Quotient.mkₐ Rₘ I).comp

Tactic:
intro Q _ _ I e f

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
⊢ ∃ a, (Ideal.Quotient.mkₐ Rₘ I).comp a = f

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ₘ)).comp (algebraMap R Rₘ) =
    (algebraMap Rₘ Q).comp (algebraMap R Rₘ)

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

Result:
no goals

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
⊢ Sₘ →ₐ[Rₘ] Q

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

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