-- Mathlib/RingTheory/FinitePresentation.lean
/-- Induction principle for finitely presented ring homomorphisms.

For a property to hold for all finitely presented ring homs, it suffices for it to hold for
`Polynomial.C : R → R[X]`, surjective ring homs with finitely generated kernels, and to be closed
under composition.

Note that to state this conveniently for ring homs between rings of different universes, we carry
around two predicates `P` and `Q`, which should be "the same" apart from universes:
* `P`, for ring homs `(R : Type u) → (S : Type u)`.
* `Q`, for ring homs `(R : Type u) → (S : Type v)`.
-/
lemma polynomial_induction
    (P : ∀ (R : Type u) [CommRing R] (S : Type u) [CommRing S], (R →+* S) → Prop)
    (Q : ∀ (R : Type u) [CommRing R] (S : Type v) [CommRing S], (R →+* S) → Prop)
    (polynomial : ∀ (R) [CommRing R], P R R[X] C)
    (fg_ker : ∀ (R : Type u) [CommRing R] (S : Type v) [CommRing S] (f : R →+* S),
      Surjective f → (ker f).FG → Q R S f)
    (comp : ∀ (R) [CommRing R] (S) [CommRing S] (T) [CommRing T] (f : R →+* S) (g : S →+* T),
      P R S f → Q S T g → Q R T (g.comp f))
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) (hf : f.FinitePresentation) :
    Q R S f

Proof state:
case h.e'_3
P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f → (ker f).FG → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
n : ℕ
IH :
  ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] (g' : MvPolynomial (Fin n) R →+* S),
    Surjective ⇑g' →
      (ker g').FG →
        let this := (g'.comp MvPolynomial.C).toAlgebra;
        Q R S (g'.comp MvPolynomial.C)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
g' : MvPolynomial (Fin (n + 1)) R →+* S
hg : Surjective ⇑g'
hg' : (ker g').FG
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] MvPolynomial (Fin n) R[X] :=
  (MvPolynomial.renameEquiv R (finSuccEquiv n)).trans (MvPolynomial.optionEquivRight R (Fin n))
⊢ Ideal.comap (↑e.symm) (ker g') = Ideal.map (↑e).toRingHom (ker g')

Tactic:
exact Ideal.comap_symm e.toRingEquiv

Result:
no goals

Proof state:
case h.e'_5
P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f → (ker f).FG → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
n : ℕ
IH :
  ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] (g' : MvPolynomial (Fin n) R →+* S),
    Surjective ⇑g' →
      (ker g').FG →
        let this := (g'.comp MvPolynomial.C).toAlgebra;
        Q R S (g'.comp MvPolynomial.C)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
g' : MvPolynomial (Fin (n + 1)) R →+* S
hg : Surjective ⇑g'
hg' : (ker g').FG
this✝ : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] MvPolynomial (Fin n) R[X] :=
  (MvPolynomial.renameEquiv R (finSuccEquiv n)).trans (MvPolynomial.optionEquivRight R (Fin n))
he : (ker (g'.comp ↑e.symm)).FG
this : Q R[X] S ((g'.comp ↑e.symm).comp MvPolynomial.C)
⊢ g'.comp MvPolynomial.C = ((g'.comp ↑e.symm).comp MvPolynomial.C).comp C

Tactic:
rw [comp_assoc, comp_assoc]

Result:
case h.e'_5
P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f → (ker f).FG → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
n : ℕ
IH :
  ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] (g' : MvPolynomial (Fin n) R →+* S),
    Surjective ⇑g' →
      (ker g').FG →
        let this := (g'.comp MvPolynomial.C).toAlgebra;
        Q R S (g'.comp MvPolynomial.C)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
g' : MvPolynomial (Fin (n + 1)) R →+* S
hg : Surjective ⇑g'
hg' : (ker g').FG
this✝ : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] MvPolynomial (Fin n) R[X] :=
  (MvPolynomial.renameEquiv R (finSuccEquiv n)).trans (MvPolynomial.optionEquivRight R (Fin n))
he : (ker (g'.comp ↑e.symm)).FG
this : Q R[X] S ((g'.comp ↑e.symm).comp MvPolynomial.C)
⊢ g'.comp MvPolynomial.C = g'.comp ((↑e.symm).comp (MvPolynomial.C.comp C))