-- 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 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
j : (Q.vars →₀ ℕ) × (P.vars →₀ ℕ)
hi : j.1 ∈ Finset.image Prod.fst (Finset.map (↑e).toEmbedding (support x))
hj : j ∈ Finset.filter (fun x => x.1 = j.1) (Finset.map e.toEmbedding (support x))
⊢ (monomial (e.symm j)) (coeff (e.symm j) x) =
    (monomial (e.symm (j.1, 0))) 1 * (Q.toComp P).toAlgHom.toRingHom ((monomial j.2) (coeff (e.symm j) x))

Tactic:
obtain ⟨i, j⟩ := j

Result:
case h.e'_1.mk
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 →₀ ℕ
j : P.vars →₀ ℕ
hi : (i, j).1 ∈ Finset.image Prod.fst (Finset.map (↑e).toEmbedding (support x))
hj : (i, j) ∈ Finset.filter (fun x => x.1 = (i, j).1) (Finset.map e.toEmbedding (support x))
⊢ (monomial (e.symm (i, j))) (coeff (e.symm (i, j)) x) =
    (monomial (e.symm ((i, j).1, 0))) 1 *
      (Q.toComp P).toAlgHom.toRingHom ((monomial (i, j).2) (coeff (e.symm (i, j)) x))

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

Tactic:
simp only [Finset.mem_filter, Finset.mem_map_equiv, AddEquiv.coe_toEquiv_symm, comp_vars,
  mem_support_iff, coeff_monomial, ↓reduceIte, ne_eq, ite_and, ite_not]

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 a = 0 then 0 else if v.1 = i then (aeval P.val) ((monomial v.2) a) else 0) =
    if v.1 = i then (aeval P.val) ((monomial v.2) a) else 0

Proof state:
case a.convert_4.a.h2
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))
p q : MvPolynomial (Q.comp P).vars R
hp :
  (∑ᶠ (i_1 : (Q.vars →₀ ℕ) × (P.vars →₀ ℕ)),
      if i_1.1 = i then (aeval P.val) ((monomial i_1.2) (coeff (e.symm i_1) p)) else 0) =
    coeff i ((Q.ofComp P).toAlgHom p)
hq :
  (∑ᶠ (i_1 : (Q.vars →₀ ℕ) × (P.vars →₀ ℕ)),
      if i_1.1 = i then (aeval P.val) ((monomial i_1.2) (coeff (e.symm i_1) q)) else 0) =
    coeff i ((Q.ofComp P).toAlgHom q)
⊢ (∑ᶠ (i_1 : (Q.vars →₀ ℕ) × (P.vars →₀ ℕ)),
      if i_1.1 = i then (aeval P.val) ((monomial i_1.2) (coeff (e.symm i_1) (p + q))) else 0) =
    coeff i ((Q.ofComp P).toAlgHom (p + q))

Tactic:
simp only [coeff_add, map_add, ite_add_zero]

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

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
⊢ x ∈ Ideal.comap (Q.toComp P).toAlgHom (RingHom.ker (Q.ofComp P).toAlgHom)

Tactic:
have : (Q.ofComp P).toAlgHom.comp (Q.toComp P).toAlgHom = IsScalarTower.toAlgHom R _ _ := by
  ext1; simp

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
⊢ x ∈ Ideal.comap (Q.toComp P).toAlgHom (RingHom.ker (Q.ofComp P).toAlgHom)