-- 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'_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:
congr 1 with r

Result:
case h.e'_5.e_f.a.a
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)
r : R
m✝ : Fin (n + 1) →₀ ℕ
⊢ MvPolynomial.coeff m✝ (MvPolynomial.C r) = MvPolynomial.coeff m✝ (((↑e.symm).comp (MvPolynomial.C.comp C)) r)

Proof state:
case mk.intro.intro.intro
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)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
g' : MvPolynomial (Fin n) R →+* S
hg : Surjective ⇑g'
hg' : (ker g').FG
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
⊢ Q R S (g'.comp MvPolynomial.C)

Tactic:
induction n generalizing R S with
| zero =>
  refine fg_ker _ _ _ (hg.comp (MvPolynomial.C_surjective (Fin 0))) ?_
  rw [← comap_ker]
  convert hg'.map (MvPolynomial.isEmptyRingEquiv R (Fin 0)).toRingHom using 1
  simp only [RingEquiv.toRingHom_eq_coe]
  exact Ideal.comap_symm (MvPolynomial.isEmptyRingEquiv R (Fin 0))
| succ n IH =>
  let e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] MvPolynomial (Fin n) R[X] :=
    (MvPolynomial.renameEquiv R (finSuccEquiv n)).trans (MvPolynomial.optionEquivRight R (Fin n))
  have he : (ker (g'.comp <| RingHomClass.toRingHom e.symm)).FG := by
    rw [← RingHom.comap_ker]
    convert hg'.map e.toAlgHom.toRingHom using 1
    exact Ideal.comap_symm e.toRingEquiv
  have := IH (R := R[X]) (S := S) (g'.comp e.symm) (hg.comp e.symm.surjective) he
  convert comp _ _ _ _ _ (polynomial _) this using 1
  rw [comp_assoc, comp_assoc]
  congr 1 with r
  simp [e]

Result:
no goals