-- 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.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 ((monomial v.1) ((aeval P.val) ((monomial v.2) a)))

Tactic:
simp only [comp_vars, coeff_monomial, ← e.injective.eq_iff,
  map_zero, AddEquiv.apply_symm_apply, apply_ite]

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 →₀ ℕ)
⊢ if v.1 = i then
    (∑ x ∈ Finset.filter (fun a => a.1 = i) (Finset.map (↑e).toEmbedding ((monomial (e.symm v)) a).support),
        if v = x then (aeval P.val) ((monomial x.2) a) else 0) =
      (aeval P.val) ((monomial v.2) a)
  else
    (∑ x ∈ Finset.filter (fun a => a.1 = i) (Finset.map (↑e).toEmbedding ((monomial (e.symm v)) a).support),
        if v = x then (aeval P.val) ((monomial x.2) a) else 0) =
      0

Proof state:
case a.convert_4.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))
⊢ ∑ x_1 ∈ Finset.filter (fun x => x.1 = i) (Finset.map (↑e).toEmbedding (support x)),
      (aeval P.val) ((monomial x_1.2) (coeff (e.symm x_1) x)) =
    coeff i ((Q.ofComp P).toAlgHom x)

Tactic:
clear h₂ hi

Result:
case a.convert_4.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
e : ((Q.comp P).vars →₀ ℕ) ≃+ (Q.vars →₀ ℕ) × (P.vars →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : Q.vars →₀ ℕ
⊢ ∑ x_1 ∈ Finset.filter (fun x => x.1 = i) (Finset.map (↑e).toEmbedding (support x)),
      (aeval P.val) ((monomial x_1.2) (coeff (e.symm x_1) x)) =
    coeff i ((Q.ofComp P).toAlgHom x)

Proof state:
case a.convert_4.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
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))
⊢ ∑ x_1 ∈ Finset.filter (fun x => x.1 = i) (Finset.map (↑e).toEmbedding (support x)),
      (aeval P.val) ((monomial x_1.2) (coeff (e.symm x_1) x)) =
    coeff i ((Q.ofComp P).toAlgHom x)

Tactic:
rw [Finset.sum_filter, ← finsum_eq_sum_of_support_subset _ (this x)]

Result:
case a.convert_4.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
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))
⊢ (∑ᶠ (i_1 : (Q.vars →₀ ℕ) × (P.vars →₀ ℕ)),
      if i_1.1 = i then (aeval P.val) ((monomial i_1.2) (coeff (e.symm i_1) x)) else 0) =
    coeff i ((Q.ofComp P).toAlgHom x)