-- Mathlib/RingTheory/Generators.lean
lemma ker_comp_eq_sup (Q : Generators S T) (P : Generators R S) :
    (Q.comp P).ker =
      Ideal.map (Q.toComp P).toAlgHom P.ker ⊔ Ideal.comap (Q.ofComp P).toAlgHom Q.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
⊢ RingHom.ker (Q.ofComp P).toAlgHom ⊔ (Q.comp P).ker ⊔ RingHom.ker (Q.ofComp P).toAlgHom ≤ (Q.comp P).ker

Tactic:
simp only [le_sup_left, sup_of_le_left, sup_le_iff, le_refl, and_true]

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
⊢ RingHom.ker (Q.ofComp P).toAlgHom ≤ (Q.comp 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
x : (Q.comp P).Ring
hx : x ∈ RingHom.ker (Q.ofComp P).toAlgHom
⊢ x ∈ (Q.comp P).ker

Tactic:
simp only [RingHom.mem_ker] at hx

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
x : (Q.comp P).Ring
hx : (Q.ofComp P).toAlgHom x = 0
⊢ x ∈ (Q.comp 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
x : (Q.comp P).Ring
hx : (Q.ofComp P).toAlgHom x = 0
⊢ (algebraMap T T) ((aeval (Q.comp P).val) x) = 0

Tactic:
rw [← Generators.Hom.algebraMap_toAlgHom (Q.ofComp P), hx, map_zero]

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
⊢ (Q.comp P).ker = RingHom.ker (Q.ofComp P).toAlgHom ⊔ (Q.comp P).ker ⊔ RingHom.ker (Q.ofComp P).toAlgHom

Tactic:
apply le_antisymm (le_trans le_sup_right le_sup_left)

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
⊢ RingHom.ker (Q.ofComp P).toAlgHom ⊔ (Q.comp P).ker ⊔ RingHom.ker (Q.ofComp P).toAlgHom ≤ (Q.comp 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
x : (Q.comp P).Ring
hx : (Q.ofComp P).toAlgHom x = 0
⊢ x ∈ (Q.comp P).ker

Tactic:
rw [Generators.ker_eq_ker_aeval_val, RingHom.mem_ker, ← id.map_eq_self (MvPolynomial.aeval _ x)]

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
x : (Q.comp P).Ring
hx : (Q.ofComp P).toAlgHom x = 0
⊢ (algebraMap T T) ((aeval (Q.comp P).val) 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
⊢ (Q.comp P).ker = Ideal.map (Q.toComp P).toAlgHom P.ker ⊔ Ideal.comap (Q.ofComp P).toAlgHom Q.ker

Tactic:
rw [← map_ofComp_ker Q P,
  Ideal.comap_map_of_surjective _ (toAlgHom_ofComp_surjective Q P)]

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
⊢ (Q.comp P).ker = Ideal.map (Q.toComp P).toAlgHom P.ker ⊔ ((Q.comp P).ker ⊔ Ideal.comap (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
⊢ (Q.comp P).ker = Ideal.map (Q.toComp P).toAlgHom P.ker ⊔ ((Q.comp P).ker ⊔ Ideal.comap (Q.ofComp P).toAlgHom ⊥)

Tactic:
rw [← sup_assoc, Algebra.Generators.map_toComp_ker, ← RingHom.ker_eq_comap_bot]

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
⊢ (Q.comp P).ker = RingHom.ker (Q.ofComp P).toAlgHom ⊔ (Q.comp P).ker ⊔ 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
⊢ RingHom.ker (Q.ofComp P).toAlgHom ≤ (Q.comp P).ker

Tactic:
intro x hx

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
x : (Q.comp P).Ring
hx : x ∈ RingHom.ker (Q.ofComp P).toAlgHom
⊢ x ∈ (Q.comp P).ker