-- Mathlib/RingTheory/Generators.lean
lemma map_ofComp_ker (Q : Generators S T) (P : Generators R S) :
    Ideal.map (Q.ofComp P).toAlgHom (Q.comp P).ker = Q.ker

Proof state:
case h
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.Ring
⊢ (∃ x_1 ∈ (Q.comp P).ker, (Q.ofComp P).toAlgHom x_1 = x) ↔ x ∈ Q.ker

Tactic:
constructor

Result:
case h.mp
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.Ring
⊢ (∃ x_1 ∈ (Q.comp P).ker, (Q.ofComp P).toAlgHom x_1 = x) → x ∈ Q.ker

case h.mpr
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.Ring
⊢ x ∈ Q.ker → ∃ x_1 ∈ (Q.comp P).ker, (Q.ofComp P).toAlgHom x_1 = x

Proof state:
case h.mp.intro.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
x : (Q.comp P).Ring
hx : (aeval (Q.comp P).val) x = 0
⊢ (aeval Q.val) ((Q.ofComp P).toAlgHom x) = 0

Tactic:
rw [← hx, Hom.algebraMap_toAlgHom, id.map_eq_self]

Result:
no goals

Proof state:
case h.mpr
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.Ring
hx : x ∈ Q.ker
⊢ ∃ x_1 ∈ (Q.comp P).ker, (Q.ofComp P).toAlgHom x_1 = x

Tactic:
exact ⟨_, (kerCompPreimage Q P ⟨x, hx⟩).2, ofComp_kerCompPreimage Q P ⟨x, hx⟩⟩

Result:
no goals

Proof state:
case h.mp.intro.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
x : (Q.comp P).Ring
hx : x ∈ (Q.comp P).ker
⊢ (Q.ofComp P).toAlgHom x ∈ Q.ker

Tactic:
simp only [ker_eq_ker_aeval_val, Submodule.coe_restrictScalars, SetLike.mem_coe,
  RingHom.mem_ker, AlgHom.toLinearMap_apply, Submodule.restrictScalars_mem] at hx ⊢

Result:
case h.mp.intro.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
x : (Q.comp P).Ring
hx : (aeval (Q.comp P).val) x = 0
⊢ (aeval Q.val) ((Q.ofComp P).toAlgHom x) = 0

Proof state:
case h.mp
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.Ring
⊢ (∃ x_1 ∈ (Q.comp P).ker, (Q.ofComp P).toAlgHom x_1 = x) → x ∈ Q.ker

Tactic:
rintro ⟨x, hx, rfl⟩

Result:
case h.mp.intro.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
x : (Q.comp P).Ring
hx : x ∈ (Q.comp P).ker
⊢ (Q.ofComp P).toAlgHom x ∈ Q.ker

Proof state:
case h.mpr
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.Ring
⊢ x ∈ Q.ker → ∃ x_1 ∈ (Q.comp P).ker, (Q.ofComp P).toAlgHom x_1 = x

Tactic:
intro hx

Result:
case h.mpr
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.Ring
hx : x ∈ Q.ker
⊢ ∃ x_1 ∈ (Q.comp P).ker, (Q.ofComp P).toAlgHom x_1 = x

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

Tactic:
ext x

Result:
case h
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.Ring
⊢ x ∈ Ideal.map (Q.ofComp P).toAlgHom (Q.comp P).ker ↔ x ∈ Q.ker

Proof state:
case h
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.Ring
⊢ x ∈ Ideal.map (Q.ofComp P).toAlgHom (Q.comp P).ker ↔ x ∈ Q.ker

Tactic:
rw [Ideal.mem_map_iff_of_surjective _ (toAlgHom_ofComp_surjective Q P)]

Result:
case h
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.Ring
⊢ (∃ x_1 ∈ (Q.comp P).ker, (Q.ofComp P).toAlgHom x_1 = x) ↔ x ∈ Q.ker