-- Mathlib/RingTheory/Generators.lean
lemma toAlgHom_ofComp_surjective (Q : Generators S T) (P : Generators R S) :
    Function.Surjective (Q.ofComp P).toAlgHom

Proof state:
case h_X.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
i : Q.vars
p : MvPolynomial (Q.vars ⊕ P.vars) R
⊢ ∃ a, (Q.ofComp P).toAlgHom a = (Q.ofComp P).toAlgHom p * X i

Tactic:
use p * MvPolynomial.X (R := R) (Sum.inl i)

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
i : Q.vars
p : MvPolynomial (Q.vars ⊕ P.vars) R
⊢ (Q.ofComp P).toAlgHom (p * X (Sum.inl i)) = (Q.ofComp P).toAlgHom p * X i

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
i : Q.vars
p : MvPolynomial (Q.vars ⊕ P.vars) R
⊢ (Q.ofComp P).toAlgHom (p * X (Sum.inl i)) = (Q.ofComp P).toAlgHom p * X i

Tactic:
simp [Algebra.Generators.ofComp, Algebra.Generators.Hom.toAlgHom]

Result:
no goals

Proof state:
case h_add
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
p q : MvPolynomial Q.vars S
hp : ∃ a, (Q.ofComp P).toAlgHom a = p
hq : ∃ a, (Q.ofComp P).toAlgHom a = q
⊢ ∃ a, (Q.ofComp P).toAlgHom a = p + q

Tactic:
obtain ⟨p, rfl⟩ := hp

Result:
case h_add.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
q : MvPolynomial Q.vars S
hq : ∃ a, (Q.ofComp P).toAlgHom a = q
p : (Q.comp P).Ring
⊢ ∃ a, (Q.ofComp P).toAlgHom a = (Q.ofComp P).toAlgHom p + q

Proof state:
case h_add.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
p q : (Q.comp P).Ring
⊢ ∃ a, (Q.ofComp P).toAlgHom a = (Q.ofComp P).toAlgHom p + (Q.ofComp P).toAlgHom q

Tactic:
use p + q

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
p q : (Q.comp P).Ring
⊢ (Q.ofComp P).toAlgHom (p + q) = (Q.ofComp P).toAlgHom p + (Q.ofComp P).toAlgHom q

Proof state:
case h_C
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
a : S
⊢ ∃ a_1, (Q.ofComp P).toAlgHom a_1 = C a

Tactic:
use MvPolynomial.rename Sum.inr (P.σ a)

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
a : S
⊢ (Q.ofComp P).toAlgHom ((rename Sum.inr) (P.σ a)) = C a

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
a : S
⊢ (Q.ofComp P).toAlgHom ((rename Sum.inr) (P.σ a)) = C a

Tactic:
simp only [Hom.toAlgHom, ofComp, Generators.comp, MvPolynomial.aeval_rename,
  Sum.elim_comp_inr]

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
a : S
⊢ (aeval (⇑C ∘ P.val)) (P.σ a) = C a

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
a : S
⊢ (aeval (⇑C ∘ P.val)) (P.σ a) = C a

Tactic:
simp_rw [Function.comp_def, ← MvPolynomial.algebraMap_eq, ← IsScalarTower.toAlgHom_apply R,
  ← MvPolynomial.comp_aeval]

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
a : S
⊢ ((IsScalarTower.toAlgHom R S (MvPolynomial Q.vars S)).comp (aeval P.val)) (P.σ a) =
    (IsScalarTower.toAlgHom R S (MvPolynomial Q.vars S)) a

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
p : Q.Ring
⊢ ∃ a, (Q.ofComp P).toAlgHom a = p

Tactic:
induction p using MvPolynomial.induction_on with
| h_C a =>
    use MvPolynomial.rename Sum.inr (P.σ a)
    simp only [Hom.toAlgHom, ofComp, Generators.comp, MvPolynomial.aeval_rename,
      Sum.elim_comp_inr]
    simp_rw [Function.comp_def, ← MvPolynomial.algebraMap_eq, ← IsScalarTower.toAlgHom_apply R,
      ← MvPolynomial.comp_aeval]
    simp
| h_add p q hp hq =>
    obtain ⟨p, rfl⟩ := hp
    obtain ⟨q, rfl⟩ := hq
    use p + q
    simp
| h_X p i hp =>
    obtain ⟨(p : MvPolynomial (Q.vars ⊕ P.vars) R), rfl⟩ := hp
    use p * MvPolynomial.X (R := R) (Sum.inl i)
    simp [Algebra.Generators.ofComp, Algebra.Generators.Hom.toAlgHom]

Result:
no goals

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
a : S
⊢ ((IsScalarTower.toAlgHom R S (MvPolynomial Q.vars S)).comp (aeval P.val)) (P.σ a) =
    (IsScalarTower.toAlgHom R S (MvPolynomial Q.vars S)) a

Tactic:
simp

Result:
no goals

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
p q : (Q.comp P).Ring
⊢ (Q.ofComp P).toAlgHom (p + q) = (Q.ofComp P).toAlgHom p + (Q.ofComp P).toAlgHom q

Tactic:
simp

Result:
no goals

Proof state:
case h_X
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
p : MvPolynomial Q.vars S
i : Q.vars
hp : ∃ a, (Q.ofComp P).toAlgHom a = p
⊢ ∃ a, (Q.ofComp P).toAlgHom a = p * X i

Tactic:
obtain ⟨(p : MvPolynomial (Q.vars ⊕ P.vars) R), rfl⟩ := hp

Result:
case h_X.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
i : Q.vars
p : MvPolynomial (Q.vars ⊕ P.vars) R
⊢ ∃ a, (Q.ofComp P).toAlgHom a = (Q.ofComp P).toAlgHom p * X i