-- 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:
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
⊢ (Q.ofComp P).toAlgHom.comp (Q.toComp P).toAlgHom = IsScalarTower.toAlgHom R P.Ring Q.Ring

Tactic:
ext1

Result:
case hf
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
i✝ : P.vars
⊢ ((Q.ofComp P).toAlgHom.comp (Q.toComp P).toAlgHom) (X i✝) = (IsScalarTower.toAlgHom R P.Ring Q.Ring) (X i✝)

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
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) =
    ∑ i_1 ∈ Finset.filter (fun x => x.1 = i) (Finset.map e.toEmbedding (support x)),
      (monomial (e.symm (i, 0))) 1 * (Q.toComp P).toAlgHom.toRingHom ((monomial i_1.2) (coeff (e.symm i_1) x))

Tactic:
refine Finset.sum_congr rfl fun j hj ↦ ?_

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

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

Tactic:
obtain rfl := (Finset.mem_filter.mp hj).2

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

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

Tactic:
rintro x (h₂ : (Q.ofComp P).toAlgHom 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 : (Q.comp P).Ring
h₂ : (Q.ofComp P).toAlgHom x = 0
⊢ x ∈ Ideal.map (Q.toComp P).toAlgHom P.ker

Proof state:
case a.convert_4.a.h1.intro.isTrue
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 →₀ ℕ)
h✝ : a = 0
⊢ 0 = if v.1 = i then (aeval P.val) ((monomial v.2) a) else 0

Tactic:
simp only [zero_smul, coeff_zero, *, map_zero, ite_self]

Result:
no goals

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

Tactic:
apply le_antisymm

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

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