-- Mathlib/RingTheory/Smooth/Basic.lean
theorem comp [FormallySmooth R A] [FormallySmooth A B] : FormallySmooth R B

Proof state:
R : Type u
inst✝⁸ : CommSemiring R
A : Type u
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
B : Type u
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FormallySmooth R A
inst✝ : FormallySmooth A B
⊢ FormallySmooth R B

Tactic:
constructor

Result:
case comp_surjective
R : Type u
inst✝⁸ : CommSemiring R
A : Type u
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
B : Type u
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FormallySmooth R A
inst✝ : FormallySmooth A B
⊢ ∀ ⦃B_1 : Type u⦄ [inst : CommRing B_1] [inst_1 : Algebra R B_1] (I : Ideal B_1),
    I ^ 2 = ⊥ → Function.Surjective (Ideal.Quotient.mkₐ R I).comp

Proof state:
case comp_surjective.intro
R : Type u
inst✝¹⁰ : CommSemiring R
A : Type u
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
B : Type u
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallySmooth R A
inst✝² : FormallySmooth A B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f : B →ₐ[R] C ⧸ I
f' : A →ₐ[R] C
e : (Ideal.Quotient.mkₐ R I).comp f' = f.comp (IsScalarTower.toAlgHom R A B)
this : Algebra A C := f'.toAlgebra
⊢ ∃ a, (Ideal.Quotient.mkₐ R I).comp a = f

Tactic:
obtain ⟨f'', e'⟩ :=
  FormallySmooth.comp_surjective I hI { f.toRingHom with commutes' := AlgHom.congr_fun e.symm }

Result:
case comp_surjective.intro.intro
R : Type u
inst✝¹⁰ : CommSemiring R
A : Type u
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
B : Type u
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallySmooth R A
inst✝² : FormallySmooth A B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f : B →ₐ[R] C ⧸ I
f' : A →ₐ[R] C
e : (Ideal.Quotient.mkₐ R I).comp f' = f.comp (IsScalarTower.toAlgHom R A B)
this : Algebra A C := f'.toAlgebra
f'' : B →ₐ[A] C
e' :
  (Ideal.Quotient.mkₐ A I).comp f'' =
    let __src := f.toRingHom;
    { toRingHom := __src, commutes' := ⋯ }
⊢ ∃ a, (Ideal.Quotient.mkₐ R I).comp a = f

Proof state:
case comp_surjective.intro.intro
R : Type u
inst✝¹⁰ : CommSemiring R
A : Type u
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
B : Type u
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallySmooth R A
inst✝² : FormallySmooth A B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f : B →ₐ[R] C ⧸ I
f' : A →ₐ[R] C
e : (Ideal.Quotient.mkₐ R I).comp f' = f.comp (IsScalarTower.toAlgHom R A B)
this : Algebra A C := f'.toAlgebra
f'' : B →ₐ[A] C
e' :
  AlgHom.restrictScalars R ((Ideal.Quotient.mkₐ A I).comp f'') =
    AlgHom.restrictScalars R
      (let __src := f.toRingHom;
      { toRingHom := __src, commutes' := ⋯ })
⊢ ∃ a, (Ideal.Quotient.mkₐ R I).comp a = f

Tactic:
exact ⟨f''.restrictScalars _, e'.trans (AlgHom.ext fun _ => rfl)⟩

Result:
no goals

Proof state:
case comp_surjective
R : Type u
inst✝⁸ : CommSemiring R
A : Type u
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
B : Type u
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FormallySmooth R A
inst✝ : FormallySmooth A B
⊢ ∀ ⦃B_1 : Type u⦄ [inst : CommRing B_1] [inst_1 : Algebra R B_1] (I : Ideal B_1),
    I ^ 2 = ⊥ → Function.Surjective (Ideal.Quotient.mkₐ R I).comp

Tactic:
intro C _ _ I hI f

Result:
case comp_surjective
R : Type u
inst✝¹⁰ : CommSemiring R
A : Type u
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
B : Type u
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallySmooth R A
inst✝² : FormallySmooth A B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f : B →ₐ[R] C ⧸ I
⊢ ∃ a, (Ideal.Quotient.mkₐ R I).comp a = f

Proof state:
case comp_surjective.intro
R : Type u
inst✝¹⁰ : CommSemiring R
A : Type u
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
B : Type u
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallySmooth R A
inst✝² : FormallySmooth A B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f : B →ₐ[R] C ⧸ I
f' : A →ₐ[R] C
e : (Ideal.Quotient.mkₐ R I).comp f' = f.comp (IsScalarTower.toAlgHom R A B)
⊢ ∃ a, (Ideal.Quotient.mkₐ R I).comp a = f

Tactic:
letI := f'.toRingHom.toAlgebra

Result:
case comp_surjective.intro
R : Type u
inst✝¹⁰ : CommSemiring R
A : Type u
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
B : Type u
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallySmooth R A
inst✝² : FormallySmooth A B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f : B →ₐ[R] C ⧸ I
f' : A →ₐ[R] C
e : (Ideal.Quotient.mkₐ R I).comp f' = f.comp (IsScalarTower.toAlgHom R A B)
this : Algebra A C := f'.toAlgebra
⊢ ∃ a, (Ideal.Quotient.mkₐ R I).comp a = f

Proof state:
case comp_surjective.intro.intro
R : Type u
inst✝¹⁰ : CommSemiring R
A : Type u
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
B : Type u
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallySmooth R A
inst✝² : FormallySmooth A B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f : B →ₐ[R] C ⧸ I
f' : A →ₐ[R] C
e : (Ideal.Quotient.mkₐ R I).comp f' = f.comp (IsScalarTower.toAlgHom R A B)
this : Algebra A C := f'.toAlgebra
f'' : B →ₐ[A] C
e' :
  (Ideal.Quotient.mkₐ A I).comp f'' =
    let __src := f.toRingHom;
    { toRingHom := __src, commutes' := ⋯ }
⊢ ∃ a, (Ideal.Quotient.mkₐ R I).comp a = f

Tactic:
apply_fun AlgHom.restrictScalars R at e'

Result:
case comp_surjective.intro.intro
R : Type u
inst✝¹⁰ : CommSemiring R
A : Type u
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
B : Type u
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallySmooth R A
inst✝² : FormallySmooth A B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f : B →ₐ[R] C ⧸ I
f' : A →ₐ[R] C
e : (Ideal.Quotient.mkₐ R I).comp f' = f.comp (IsScalarTower.toAlgHom R A B)
this : Algebra A C := f'.toAlgebra
f'' : B →ₐ[A] C
e' :
  AlgHom.restrictScalars R ((Ideal.Quotient.mkₐ A I).comp f'') =
    AlgHom.restrictScalars R
      (let __src := f.toRingHom;
      { toRingHom := __src, commutes' := ⋯ })
⊢ ∃ a, (Ideal.Quotient.mkₐ R I).comp a = f

Proof state:
case comp_surjective
R : Type u
inst✝¹⁰ : CommSemiring R
A : Type u
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
B : Type u
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallySmooth R A
inst✝² : FormallySmooth A B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f : B →ₐ[R] C ⧸ I
⊢ ∃ a, (Ideal.Quotient.mkₐ R I).comp a = f

Tactic:
obtain ⟨f', e⟩ := FormallySmooth.comp_surjective I hI (f.comp (IsScalarTower.toAlgHom R A B))

Result:
case comp_surjective.intro
R : Type u
inst✝¹⁰ : CommSemiring R
A : Type u
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
B : Type u
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallySmooth R A
inst✝² : FormallySmooth A B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f : B →ₐ[R] C ⧸ I
f' : A →ₐ[R] C
e : (Ideal.Quotient.mkₐ R I).comp f' = f.comp (IsScalarTower.toAlgHom R A B)
⊢ ∃ a, (Ideal.Quotient.mkₐ R I).comp a = f