-- 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
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))
⊢ (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

Tactic:
refine Ideal.mem_map_of_mem _ ?_

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
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))
⊢ ∑ j ∈ Finset.filter (fun x => x.1 = i) (Finset.map e.toEmbedding (support x)), (monomial j.2) (coeff (e.symm j) x) ∈
    P.ker

Proof state:
case a.convert_4.a.h2.hg
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)
⊢ (Function.support fun i_1 => if i_1.1 = i then (aeval P.val) ((monomial i_1.2) (coeff (e.symm i_1) q)) else 0) ⊆
    ↑(Finset.map (↑e).toEmbedding q.support)

Tactic:
convert this q

Result:
no goals

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))
⊢ ∑ j ∈ Finset.filter (fun x => x.1 = i) (Finset.map e.toEmbedding (support x)), (monomial j.2) (coeff (e.symm j) x) ∈
    P.ker

Tactic:
simp only [ker_eq_ker_aeval_val, AddEquiv.toEquiv_eq_coe, RingHom.mem_ker, map_sum]

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
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)) =
    0

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
h₂ : (Q.ofComp P).toAlgHom x = 0
e : ((Q.comp P).vars →₀ ℕ) ≃+ (Q.vars →₀ ℕ) × (P.vars →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
this :
  ∑ v ∈ Finset.map (↑e).toEmbedding (support x), (monomial (e.symm v)) (coeff (e.symm v) x) ∈
    Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
⊢ x ∈ Ideal.map (Q.toComp P).toAlgHom P.ker

Tactic:
simpa only [AlgHom.toRingHom_eq_coe, Finset.sum_map, Equiv.coe_toEmbedding,
  EquivLike.coe_coe, AddEquiv.symm_apply_apply, support_sum_monomial_coeff] using this

Result:
no goals

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 →₀ ℕ)
⊢ P.ker ≤ Ideal.comap (Q.toComp P).toAlgHom (RingHom.ker (Q.ofComp P).toAlgHom)

Tactic:
rintro x (hx : algebraMap P.Ring S x = 0)

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