-- 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.h2.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 →₀ ℕ)
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) p)) else 0).Finite

Tactic:
refine (((support p).map e).finite_toSet.subset ?_)

Result:
case a.convert_4.a.h2.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 →₀ ℕ)
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) p)) else 0) ⊆
    ↑(Finset.map (↑e).toEmbedding p.support)

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

Tactic:
congr

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 →₀ ℕ)
x✝ : (Q.comp P).Ring
e : ((Q.comp P).vars →₀ ℕ) ≃+ (Q.vars →₀ ℕ) × (P.vars →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : Q.vars →₀ ℕ
x : (Q.comp P).Ring
j : (Q.vars →₀ ℕ) × (P.vars →₀ ℕ)
⊢ j ∈ (↑(Finset.map (↑e).toEmbedding (support x)))ᶜ →
    j ∈ (Function.support fun a => if a.1 = i then (aeval P.val) ((monomial a.2) (coeff (e.symm a) x)) else 0)ᶜ

Tactic:
obtain ⟨j, rfl⟩ := e.surjective j

Result:
case 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
this : DecidableEq (Q.vars →₀ ℕ) := Classical.decEq (Q.vars →₀ ℕ)
x✝ : (Q.comp P).Ring
e : ((Q.comp P).vars →₀ ℕ) ≃+ (Q.vars →₀ ℕ) × (P.vars →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : Q.vars →₀ ℕ
x : (Q.comp P).Ring
j : (Q.comp P).vars →₀ ℕ
⊢ e j ∈ (↑(Finset.map (↑e).toEmbedding (support x)))ᶜ →
    e j ∈ (Function.support fun a => if a.1 = i then (aeval P.val) ((monomial a.2) (coeff (e.symm a) x)) else 0)ᶜ

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

Tactic:
let e : ((Q.comp P).vars →₀ ℕ) ≃+ (Q.vars →₀ ℕ) × (P.vars →₀ ℕ) :=
  Finsupp.sumFinsuppAddEquivProdFinsupp

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
e : ((Q.comp P).vars →₀ ℕ) ≃+ (Q.vars →₀ ℕ) × (P.vars →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
⊢ x ∈ Ideal.map (Q.toComp P).toAlgHom P.ker

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

Tactic:
rw [Ideal.map_le_iff_le_comap]

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