-- Mathlib/RingTheory/Generators.lean
lemma map_toComp_ker (Q : Generators S T) (P : Generators R S) :
    P.ker.map (Q.toComp P).toAlgHom = RingHom.ker (Q.ofComp P).toAlgHom

Proof state:
case a
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
this : DecidableEq (Q.vars →₀ ℕ) := Classical.decEq (Q.vars →₀ ℕ)
x : (Q.comp P).Ring
h₂ : (Q.ofComp P).toAlgHom x = 0
e : ((Q.comp P).vars →₀ ℕ) ≃+ (Q.vars →₀ ℕ) × (P.vars →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : Q.vars →₀ ℕ
hi : i ∈ Finset.image Prod.fst (Finset.map (↑e).toEmbedding (support x))
⊢ ∑ i ∈ Finset.filter (fun i_1 => i_1.1 = i) (Finset.map (↑e).toEmbedding (support x)),
      (monomial (e.symm i)) (coeff (e.symm i) x) ∈
    Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker

Tactic:
convert_to monomial (e.symm (i, 0)) 1 * (Q.toComp P).toAlgHom.toRingHom
  (∑ j ∈ ((support x).map e.toEmbedding).filter (fun x ↦ x.1 = i),
    monomial j.2 (coeff (e.symm j) x)) ∈ _

Result:
case h.e'_1
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
this : DecidableEq (Q.vars →₀ ℕ) := Classical.decEq (Q.vars →₀ ℕ)
x : (Q.comp P).Ring
h₂ : (Q.ofComp P).toAlgHom x = 0
e : ((Q.comp P).vars →₀ ℕ) ≃+ (Q.vars →₀ ℕ) × (P.vars →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : Q.vars →₀ ℕ
hi : i ∈ Finset.image Prod.fst (Finset.map (↑e).toEmbedding (support x))
⊢ ∑ i ∈ Finset.filter (fun i_1 => i_1.1 = i) (Finset.map (↑e).toEmbedding (support x)),
      (monomial (e.symm i)) (coeff (e.symm i) x) =
    (monomial (e.symm (i, 0))) 1 *
      (Q.toComp P).toAlgHom.toRingHom
        (∑ j ∈ Finset.filter (fun x => x.1 = i) (Finset.map e.toEmbedding (support x)),
          (monomial j.2) (coeff (e.symm j) x))

case a.convert_4
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
this : DecidableEq (Q.vars →₀ ℕ) := Classical.decEq (Q.vars →₀ ℕ)
x : (Q.comp P).Ring
h₂ : (Q.ofComp P).toAlgHom x = 0
e : ((Q.comp P).vars →₀ ℕ) ≃+ (Q.vars →₀ ℕ) × (P.vars →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : Q.vars →₀ ℕ
hi : i ∈ Finset.image Prod.fst (Finset.map (↑e).toEmbedding (support x))
⊢ (monomial (e.symm (i, 0))) 1 *
      (Q.toComp P).toAlgHom.toRingHom
        (∑ j ∈ Finset.filter (fun x => x.1 = i) (Finset.map e.toEmbedding (support x)),
          (monomial j.2) (coeff (e.symm j) x)) ∈
    Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
this : DecidableEq (Q.vars →₀ ℕ) := Classical.decEq (Q.vars →₀ ℕ)
x✝ : (Q.comp P).Ring
e : ((Q.comp P).vars →₀ ℕ) ≃+ (Q.vars →₀ ℕ) × (P.vars →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : Q.vars →₀ ℕ
x : (Q.comp P).Ring
⊢ (↑(Finset.map (↑e).toEmbedding (support x)))ᶜ ⊆
    (Function.support fun a => if a.1 = i then (aeval P.val) ((monomial a.2) (coeff (e.symm a) x)) else 0)ᶜ

Tactic:
intro j

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
this : DecidableEq (Q.vars →₀ ℕ) := Classical.decEq (Q.vars →₀ ℕ)
x✝ : (Q.comp P).Ring
e : ((Q.comp P).vars →₀ ℕ) ≃+ (Q.vars →₀ ℕ) × (P.vars →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : Q.vars →₀ ℕ
x : (Q.comp P).Ring
j : (Q.vars →₀ ℕ) × (P.vars →₀ ℕ)
⊢ j ∈ (↑(Finset.map (↑e).toEmbedding (support x)))ᶜ →
    j ∈ (Function.support fun a => if a.1 = i then (aeval P.val) ((monomial a.2) (coeff (e.symm a) x)) else 0)ᶜ

Proof state:
case a.convert_4.a.h1
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
this✝ : DecidableEq (Q.vars →₀ ℕ) := Classical.decEq (Q.vars →₀ ℕ)
e : ((Q.comp P).vars →₀ ℕ) ≃+ (Q.vars →₀ ℕ) × (P.vars →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : Q.vars →₀ ℕ
this :
  ∀ (x : (Q.comp P).Ring),
    (Function.support fun a => if a.1 = i then (aeval P.val) ((monomial a.2) (coeff (e.symm a) x)) else 0) ⊆
      ↑(Finset.map (↑e).toEmbedding (support x))
v : (Q.comp P).vars →₀ ℕ
a : R
⊢ ∑ a_1 ∈ Finset.filter (fun a => a.1 = i) (Finset.map (↑e).toEmbedding ((monomial v) a).support),
      (aeval P.val) ((monomial a_1.2) (coeff (e.symm a_1) ((monomial v) a))) =
    coeff i ((Q.ofComp P).toAlgHom ((monomial v) a))

Tactic:
obtain ⟨v, rfl⟩ := e.symm.surjective v

Result:
case a.convert_4.a.h1.intro
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
this✝ : DecidableEq (Q.vars →₀ ℕ) := Classical.decEq (Q.vars →₀ ℕ)
e : ((Q.comp P).vars →₀ ℕ) ≃+ (Q.vars →₀ ℕ) × (P.vars →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : Q.vars →₀ ℕ
this :
  ∀ (x : (Q.comp P).Ring),
    (Function.support fun a => if a.1 = i then (aeval P.val) ((monomial a.2) (coeff (e.symm a) x)) else 0) ⊆
      ↑(Finset.map (↑e).toEmbedding (support x))
a : R
v : (Q.vars →₀ ℕ) × (P.vars →₀ ℕ)
⊢ ∑ a_1 ∈ Finset.filter (fun a => a.1 = i) (Finset.map (↑e).toEmbedding ((monomial (e.symm v)) a).support),
      (aeval P.val) ((monomial a_1.2) (coeff (e.symm a_1) ((monomial (e.symm v)) a))) =
    coeff i ((Q.ofComp P).toAlgHom ((monomial (e.symm v)) a))

Proof state:
case a
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
this✝ : DecidableEq (Q.vars →₀ ℕ) := Classical.decEq (Q.vars →₀ ℕ)
x : P.Ring
hx : (algebraMap P.Ring S) x = 0
this : (Q.ofComp P).toAlgHom.comp (Q.toComp P).toAlgHom = IsScalarTower.toAlgHom R P.Ring Q.Ring
⊢ x ∈ Ideal.comap (Q.toComp P).toAlgHom (RingHom.ker (Q.ofComp P).toAlgHom)

Tactic:
simp only [comp_vars, AlgHom.toRingHom_eq_coe, Ideal.mem_comap, RingHom.coe_coe,
  RingHom.mem_ker, ← AlgHom.comp_apply, this, IsScalarTower.toAlgHom_apply]

Result:
case a
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
this✝ : DecidableEq (Q.vars →₀ ℕ) := Classical.decEq (Q.vars →₀ ℕ)
x : P.Ring
hx : (algebraMap P.Ring S) x = 0
this : (Q.ofComp P).toAlgHom.comp (Q.toComp P).toAlgHom = IsScalarTower.toAlgHom R P.Ring Q.Ring
⊢ (algebraMap P.Ring Q.Ring) x = 0