-- Mathlib/RingTheory/Unramified/Basic.lean
theorem of_comp [FormallyUnramified R B] : FormallyUnramified A B

Proof state:
R : Type u_1
inst✝⁹ : CommRing R
A : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
B : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : FormallyUnramified R B
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra A Q
I : Ideal Q
e : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[A] Q
e' : (Ideal.Quotient.mkₐ A I).comp f₁ = (Ideal.Quotient.mkₐ A I).comp f₂
⊢ f₁ = f₂

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

Result:
R : Type u_1
inst✝⁹ : CommRing R
A : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
B : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : FormallyUnramified R B
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra A Q
I : Ideal Q
e : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[A] Q
e' : (Ideal.Quotient.mkₐ A I).comp f₁ = (Ideal.Quotient.mkₐ A I).comp f₂
this : Algebra R Q := ((algebraMap A Q).comp (algebraMap R A)).toAlgebra
⊢ f₁ = f₂

Proof state:
R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
B : Type u_3
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R A B
inst✝ : FormallyUnramified R B
⊢ ∀ ⦃B_1 : Type u_3⦄ [inst : CommRing B_1] [inst_1 : Algebra A B_1] (I : Ideal B_1),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ A I).comp

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

Result:
R : Type u_1
inst✝⁹ : CommRing R
A : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
B : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : FormallyUnramified R B
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra A Q
I : Ideal Q
e : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[A] Q
e' : (Ideal.Quotient.mkₐ A I).comp f₁ = (Ideal.Quotient.mkₐ A I).comp f₂
⊢ f₁ = f₂

Proof state:
R : Type u_1
inst✝⁹ : CommRing R
A : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
B : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : FormallyUnramified R B
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra A Q
I : Ideal Q
e : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[A] Q
e' : (Ideal.Quotient.mkₐ A I).comp f₁ = (Ideal.Quotient.mkₐ A I).comp f₂
this✝ : Algebra R Q := ((algebraMap A Q).comp (algebraMap R A)).toAlgebra
this : IsScalarTower R A Q := IsScalarTower.of_algebraMap_eq' rfl
⊢ AlgHom.restrictScalars R f₁ = AlgHom.restrictScalars R f₂

Tactic:
refine FormallyUnramified.ext I ⟨2, e⟩ ?_

Result:
R : Type u_1
inst✝⁹ : CommRing R
A : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
B : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : FormallyUnramified R B
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra A Q
I : Ideal Q
e : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[A] Q
e' : (Ideal.Quotient.mkₐ A I).comp f₁ = (Ideal.Quotient.mkₐ A I).comp f₂
this✝ : Algebra R Q := ((algebraMap A Q).comp (algebraMap R A)).toAlgebra
this : IsScalarTower R A Q := IsScalarTower.of_algebraMap_eq' rfl
⊢ ∀ (x : B),
    (Ideal.Quotient.mk I) ((AlgHom.restrictScalars R f₁) x) = (Ideal.Quotient.mk I) ((AlgHom.restrictScalars R f₂) x)

Proof state:
R : Type u_1
inst✝⁹ : CommRing R
A : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
B : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : FormallyUnramified R B
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra A Q
I : Ideal Q
e : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[A] Q
e' : (Ideal.Quotient.mkₐ A I).comp f₁ = (Ideal.Quotient.mkₐ A I).comp f₂
this : Algebra R Q := ((algebraMap A Q).comp (algebraMap R A)).toAlgebra
⊢ f₁ = f₂

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

Result:
R : Type u_1
inst✝⁹ : CommRing R
A : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
B : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : FormallyUnramified R B
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra A Q
I : Ideal Q
e : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[A] Q
e' : (Ideal.Quotient.mkₐ A I).comp f₁ = (Ideal.Quotient.mkₐ A I).comp f₂
this✝ : Algebra R Q := ((algebraMap A Q).comp (algebraMap R A)).toAlgebra
this : IsScalarTower R A Q := IsScalarTower.of_algebraMap_eq' rfl
⊢ f₁ = f₂

Proof state:
R : Type u_1
inst✝⁹ : CommRing R
A : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
B : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : FormallyUnramified R B
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra A Q
I : Ideal Q
e : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[A] Q
e' : (Ideal.Quotient.mkₐ A I).comp f₁ = (Ideal.Quotient.mkₐ A I).comp f₂
this✝ : Algebra R Q := ((algebraMap A Q).comp (algebraMap R A)).toAlgebra
this : IsScalarTower R A Q := IsScalarTower.of_algebraMap_eq' rfl
⊢ f₁ = f₂

Tactic:
refine AlgHom.restrictScalars_injective R ?_

Result:
R : Type u_1
inst✝⁹ : CommRing R
A : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
B : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : FormallyUnramified R B
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra A Q
I : Ideal Q
e : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[A] Q
e' : (Ideal.Quotient.mkₐ A I).comp f₁ = (Ideal.Quotient.mkₐ A I).comp f₂
this✝ : Algebra R Q := ((algebraMap A Q).comp (algebraMap R A)).toAlgebra
this : IsScalarTower R A Q := IsScalarTower.of_algebraMap_eq' rfl
⊢ AlgHom.restrictScalars R f₁ = AlgHom.restrictScalars R f₂

Proof state:
R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
B : Type u_3
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R A B
inst✝ : FormallyUnramified R B
⊢ FormallyUnramified A B

Tactic:
rw [iff_comp_injective]

Result:
R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
B : Type u_3
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R A B
inst✝ : FormallyUnramified R B
⊢ ∀ ⦃B_1 : Type u_3⦄ [inst : CommRing B_1] [inst_1 : Algebra A B_1] (I : Ideal B_1),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ A I).comp

Proof state:
R : Type u_1
inst✝⁹ : CommRing R
A : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
B : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : FormallyUnramified R B
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra A Q
I : Ideal Q
e : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[A] Q
e' : (Ideal.Quotient.mkₐ A I).comp f₁ = (Ideal.Quotient.mkₐ A I).comp f₂
this✝ : Algebra R Q := ((algebraMap A Q).comp (algebraMap R A)).toAlgebra
this : IsScalarTower R A Q := IsScalarTower.of_algebraMap_eq' rfl
⊢ ∀ (x : B),
    (Ideal.Quotient.mk I) ((AlgHom.restrictScalars R f₁) x) = (Ideal.Quotient.mk I) ((AlgHom.restrictScalars R f₂) x)

Tactic:
intro x

Result:
R : Type u_1
inst✝⁹ : CommRing R
A : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
B : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : FormallyUnramified R B
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra A Q
I : Ideal Q
e : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[A] Q
e' : (Ideal.Quotient.mkₐ A I).comp f₁ = (Ideal.Quotient.mkₐ A I).comp f₂
this✝ : Algebra R Q := ((algebraMap A Q).comp (algebraMap R A)).toAlgebra
this : IsScalarTower R A Q := IsScalarTower.of_algebraMap_eq' rfl
x : B
⊢ (Ideal.Quotient.mk I) ((AlgHom.restrictScalars R f₁) x) = (Ideal.Quotient.mk I) ((AlgHom.restrictScalars R f₂) x)