-- Mathlib/RingTheory/Unramified/Basic.lean
theorem comp [FormallyUnramified R A] [FormallyUnramified A B] :
    FormallyUnramified R 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 A
inst✝² : FormallyUnramified A B
C : Type u_3
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
e' : f₁.comp (IsScalarTower.toAlgHom R A B) = f₂.comp (IsScalarTower.toAlgHom R A B)
this : Algebra A C := (AlgHom.restrictDomain A f₁).toAlgebra
⊢ f₁ = f₂

Tactic:
let F₁ : B →ₐ[A] C := { f₁ with commutes' := fun r => 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 A
inst✝² : FormallyUnramified A B
C : Type u_3
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
e' : f₁.comp (IsScalarTower.toAlgHom R A B) = f₂.comp (IsScalarTower.toAlgHom R A B)
this : Algebra A C := (AlgHom.restrictDomain A f₁).toAlgebra
F₁ : B →ₐ[A] C := { toRingHom := f₁.toRingHom, commutes' := ⋯ }
⊢ 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 A
inst✝² : FormallyUnramified A B
C : Type u_3
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
e' : f₁.comp (IsScalarTower.toAlgHom R A B) = f₂.comp (IsScalarTower.toAlgHom R A B)
⊢ f₁ = f₂

Tactic:
letI := (f₁.restrictDomain 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 A
inst✝² : FormallyUnramified A B
C : Type u_3
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
e' : f₁.comp (IsScalarTower.toAlgHom R A B) = f₂.comp (IsScalarTower.toAlgHom R A B)
this : Algebra A C := (AlgHom.restrictDomain A f₁).toAlgebra
⊢ f₁ = f₂

Proof state:
case H.e_a
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 A
inst✝² : FormallyUnramified A B
C : Type u_3
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
e' : f₁.comp (IsScalarTower.toAlgHom R A B) = f₂.comp (IsScalarTower.toAlgHom R A B)
this : Algebra A C := (AlgHom.restrictDomain A f₁).toAlgebra
F₁ : B →ₐ[A] C := { toRingHom := f₁.toRingHom, commutes' := ⋯ }
F₂ : B →ₐ[A] C := { toRingHom := f₂.toRingHom, commutes' := ⋯ }
x : B
⊢ F₁ = F₂

Tactic:
exact FormallyUnramified.ext I ⟨2, hI⟩ (AlgHom.congr_fun e)

Result:
no goals

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 A
inst✝² : FormallyUnramified A B
C : Type u_3
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
e' : f₁.comp (IsScalarTower.toAlgHom R A B) = f₂.comp (IsScalarTower.toAlgHom R A B)
this : Algebra A C := (AlgHom.restrictDomain A f₁).toAlgebra
F₁ : B →ₐ[A] C := { toRingHom := f₁.toRingHom, commutes' := ⋯ }
F₂ : B →ₐ[A] C := { toRingHom := f₂.toRingHom, commutes' := ⋯ }
⊢ f₁ = f₂

Tactic:
ext1 x

Result:
case H
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 A
inst✝² : FormallyUnramified A B
C : Type u_3
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
e' : f₁.comp (IsScalarTower.toAlgHom R A B) = f₂.comp (IsScalarTower.toAlgHom R A B)
this : Algebra A C := (AlgHom.restrictDomain A f₁).toAlgebra
F₁ : B →ₐ[A] C := { toRingHom := f₁.toRingHom, commutes' := ⋯ }
F₂ : B →ₐ[A] C := { toRingHom := f₂.toRingHom, commutes' := ⋯ }
x : B
⊢ f₁ x = 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 A
inst✝² : FormallyUnramified A B
C : Type u_3
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
⊢ f₁ = f₂

Tactic:
have e' :=
  FormallyUnramified.lift_unique I ⟨2, hI⟩ (f₁.comp <| IsScalarTower.toAlgHom R A B)
    (f₂.comp <| IsScalarTower.toAlgHom R A B) (by rw [← AlgHom.comp_assoc, e, AlgHom.comp_assoc])

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 A
inst✝² : FormallyUnramified A B
C : Type u_3
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
e' : f₁.comp (IsScalarTower.toAlgHom R A B) = f₂.comp (IsScalarTower.toAlgHom R A B)
⊢ 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 A
inst✝ : FormallyUnramified A B
⊢ ∀ ⦃B_1 : Type u_3⦄ [inst : CommRing B_1] [inst_1 : Algebra R B_1] (I : Ideal B_1),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
intro C _ _ I hI 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 A
inst✝² : FormallyUnramified A B
C : Type u_3
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
⊢ f₁ = f₂