-- Mathlib/RingTheory/Unramified/Basic.lean
theorem of_isLocalization [IsLocalization M Rₘ] : FormallyUnramified R Rₘ

Proof state:
R : Type u_1
Rₘ : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
⊢ FormallyUnramified R Rₘ

Tactic:
rw [iff_comp_injective]

Result:
R : Type u_1
Rₘ : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
⊢ ∀ ⦃B : Type u_3⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp

Proof state:
case a
R : Type u_1
Rₘ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
x✝ : I ^ 2 = ⊥
f₁ f₂ : Rₘ →ₐ[R] Q
a✝ : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
⊢ ↑f₁ = ↑f₂

Tactic:
refine IsLocalization.ringHom_ext M ?_

Result:
case a
R : Type u_1
Rₘ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
x✝ : I ^ 2 = ⊥
f₁ f₂ : Rₘ →ₐ[R] Q
a✝ : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
⊢ (↑f₁).comp (algebraMap R Rₘ) = (↑f₂).comp (algebraMap R Rₘ)

Proof state:
case a.a
R : Type u_1
Rₘ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
x✝¹ : I ^ 2 = ⊥
f₁ f₂ : Rₘ →ₐ[R] Q
a✝ : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
x✝ : R
⊢ ((↑f₁).comp (algebraMap R Rₘ)) x✝ = ((↑f₂).comp (algebraMap R Rₘ)) x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
Rₘ : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
⊢ ∀ ⦃B : Type u_3⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
intro Q _ _ I _ f₁ f₂ _

Result:
R : Type u_1
Rₘ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
x✝ : I ^ 2 = ⊥
f₁ f₂ : Rₘ →ₐ[R] Q
a✝ : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
⊢ f₁ = f₂

Proof state:
case a
R : Type u_1
Rₘ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
x✝ : I ^ 2 = ⊥
f₁ f₂ : Rₘ →ₐ[R] Q
a✝ : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
⊢ (↑f₁).comp (algebraMap R Rₘ) = (↑f₂).comp (algebraMap R Rₘ)

Tactic:
ext

Result:
case a.a
R : Type u_1
Rₘ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
x✝¹ : I ^ 2 = ⊥
f₁ f₂ : Rₘ →ₐ[R] Q
a✝ : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
x✝ : R
⊢ ((↑f₁).comp (algebraMap R Rₘ)) x✝ = ((↑f₂).comp (algebraMap R Rₘ)) x✝

Proof state:
R : Type u_1
Rₘ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
x✝ : I ^ 2 = ⊥
f₁ f₂ : Rₘ →ₐ[R] Q
a✝ : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
⊢ f₁ = f₂

Tactic:
apply AlgHom.coe_ringHom_injective

Result:
case a
R : Type u_1
Rₘ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
x✝ : I ^ 2 = ⊥
f₁ f₂ : Rₘ →ₐ[R] Q
a✝ : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
⊢ ↑f₁ = ↑f₂