-- Mathlib/RingTheory/Smooth/Basic.lean
theorem of_isLocalization : FormallySmooth R Rₘ

Proof state:
case h
R Rₘ : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
this✝ : ∀ (x : ↥M), IsUnit ((algebraMap R Q) ↑x)
this : Rₘ →ₐ[R] Q :=
  let __src := IsLocalization.lift this✝;
  { toRingHom := __src, commutes' := ⋯ }
⊢ (Ideal.Quotient.mkₐ R I).comp this = f

Tactic:
apply AlgHom.coe_ringHom_injective

Result:
case h.a
R Rₘ : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
this✝ : ∀ (x : ↥M), IsUnit ((algebraMap R Q) ↑x)
this : Rₘ →ₐ[R] Q :=
  let __src := IsLocalization.lift this✝;
  { toRingHom := __src, commutes' := ⋯ }
⊢ ↑((Ideal.Quotient.mkₐ R I).comp this) = ↑f

Proof state:
case comp_surjective
R Rₘ : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
this✝ : ∀ (x : ↥M), IsUnit ((algebraMap R Q) ↑x)
this : Rₘ →ₐ[R] Q :=
  let __src := IsLocalization.lift this✝;
  { toRingHom := __src, commutes' := ⋯ }
⊢ ∃ a, (Ideal.Quotient.mkₐ R I).comp a = f

Tactic:
use this

Result:
case h
R Rₘ : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
this✝ : ∀ (x : ↥M), IsUnit ((algebraMap R Q) ↑x)
this : Rₘ →ₐ[R] Q :=
  let __src := IsLocalization.lift this✝;
  { toRingHom := __src, commutes' := ⋯ }
⊢ (Ideal.Quotient.mkₐ R I).comp this = f

Proof state:
R Rₘ : Type u
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
⊢ FormallySmooth R Rₘ

Tactic:
constructor

Result:
case comp_surjective
R Rₘ : Type u
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
⊢ ∀ ⦃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 h.a.a
R Rₘ : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
this✝ : ∀ (x : ↥M), IsUnit ((algebraMap R Q) ↑x)
this : Rₘ →ₐ[R] Q :=
  let __src := IsLocalization.lift this✝;
  { toRingHom := __src, commutes' := ⋯ }
x✝ : R
⊢ ((↑((Ideal.Quotient.mkₐ R I).comp this)).comp (algebraMap R Rₘ)) x✝ = ((↑f).comp (algebraMap R Rₘ)) x✝

Tactic:
simp

Result:
no goals

Proof state:
R Rₘ : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
x : ↥M
⊢ IsUnit ((algebraMap R Q) ↑x)

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

Result:
R Rₘ : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
x : ↥M
⊢ IsUnit ((Ideal.Quotient.mk I) ((algebraMap R Q) ↑x))

Proof state:
case comp_surjective
R Rₘ : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
this : ∀ (x : ↥M), IsUnit ((algebraMap R Q) ↑x)
⊢ ∃ a, (Ideal.Quotient.mkₐ R I).comp a = f

Tactic:
let this : Rₘ →ₐ[R] Q :=
  { IsLocalization.lift this with commutes' := IsLocalization.lift_eq this }

Result:
case comp_surjective
R Rₘ : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
this✝ : ∀ (x : ↥M), IsUnit ((algebraMap R Q) ↑x)
this : Rₘ →ₐ[R] Q :=
  let __src := IsLocalization.lift this✝;
  { toRingHom := __src, commutes' := ⋯ }
⊢ ∃ a, (Ideal.Quotient.mkₐ R I).comp a = f

Proof state:
case comp_surjective
R Rₘ : Type u
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
⊢ ∀ ⦃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ₘ : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
⊢ ∃ a, (Ideal.Quotient.mkₐ R I).comp a = f

Proof state:
case h.a
R Rₘ : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
this✝ : ∀ (x : ↥M), IsUnit ((algebraMap R Q) ↑x)
this : Rₘ →ₐ[R] Q :=
  let __src := IsLocalization.lift this✝;
  { toRingHom := __src, commutes' := ⋯ }
⊢ (↑((Ideal.Quotient.mkₐ R I).comp this)).comp (algebraMap R Rₘ) = (↑f).comp (algebraMap R Rₘ)

Tactic:
ext

Result:
case h.a.a
R Rₘ : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
this✝ : ∀ (x : ↥M), IsUnit ((algebraMap R Q) ↑x)
this : Rₘ →ₐ[R] Q :=
  let __src := IsLocalization.lift this✝;
  { toRingHom := __src, commutes' := ⋯ }
x✝ : R
⊢ ((↑((Ideal.Quotient.mkₐ R I).comp this)).comp (algebraMap R Rₘ)) x✝ = ((↑f).comp (algebraMap R Rₘ)) x✝

Proof state:
case h.a
R Rₘ : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
this✝ : ∀ (x : ↥M), IsUnit ((algebraMap R Q) ↑x)
this : Rₘ →ₐ[R] Q :=
  let __src := IsLocalization.lift this✝;
  { toRingHom := __src, commutes' := ⋯ }
⊢ ↑((Ideal.Quotient.mkₐ R I).comp this) = ↑f

Tactic:
refine IsLocalization.ringHom_ext M ?_

Result:
case h.a
R Rₘ : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
this✝ : ∀ (x : ↥M), IsUnit ((algebraMap R Q) ↑x)
this : Rₘ →ₐ[R] Q :=
  let __src := IsLocalization.lift this✝;
  { toRingHom := __src, commutes' := ⋯ }
⊢ (↑((Ideal.Quotient.mkₐ R I).comp this)).comp (algebraMap R Rₘ) = (↑f).comp (algebraMap R Rₘ)

Proof state:
case h.e'_3
R Rₘ : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
x : ↥M
⊢ (Ideal.Quotient.mk I) ((algebraMap R Q) ↑x) = f ((algebraMap R Rₘ) ↑x)

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

Result:
no goals

Proof state:
R Rₘ : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
⊢ ∀ (x : ↥M), IsUnit ((algebraMap R Q) ↑x)

Tactic:
intro x

Result:
R Rₘ : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
x : ↥M
⊢ IsUnit ((algebraMap R Q) ↑x)