-- Mathlib/RingTheory/Presentation.lean
/-- The pre-images constructed in `comp_relation_aux` are indeed pre-images under `aux`. -/
private lemma comp_relation_aux_map (r : Q.rels) :
    (Q.aux P) (Q.comp_relation_aux P r) = Q.relation r

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
r : Q.rels
⊢ (Finsupp.sum (Q.relation r) fun a b =>
      (aeval (⇑C ∘ P.val)) (P.σ b) *
        ((algebraMap R (MvPolynomial Q.vars S)) 1 *
          (Finsupp.mapDomain Sum.inl a).prod fun i k => Sum.elim X (⇑C ∘ P.val) i ^ k)) =
    Finsupp.sum (Q.relation r) Finsupp.single

Tactic:
congr

Result:
case e_g
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
r : Q.rels
⊢ (fun a b =>
      (aeval (⇑C ∘ P.val)) (P.σ b) *
        ((algebraMap R (MvPolynomial Q.vars S)) 1 *
          (Finsupp.mapDomain Sum.inl a).prod fun i k => Sum.elim X (⇑C ∘ P.val) i ^ k)) =
    Finsupp.single

Proof state:
case e_g.h.h.a
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
r : Q.rels
u : Q.vars →₀ ℕ
s : S
m : Q.vars →₀ ℕ
⊢ coeff m
      (C ((aeval P.val) (P.σ s)) *
        ((C.comp (algebraMap R S)) 1 * (Finsupp.mapDomain Sum.inl u).prod fun i k => Sum.elim X (⇑C ∘ P.val) i ^ k)) =
    coeff m (C s * u.prod fun n e => X n ^ e)

Tactic:
simp [Finsupp.prod_mapDomain_index_inj (Sum.inl_injective)]

Result:
no goals

Proof state:
case e_g.h.h.a
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
r : Q.rels
u : Q.vars →₀ ℕ
s : S
m : Q.vars →₀ ℕ
⊢ coeff m
      (eval₂ (algebraMap R (MvPolynomial Q.vars S)) (⇑C ∘ P.val) (P.σ s) *
        ((algebraMap R (MvPolynomial Q.vars S)) 1 *
          (Finsupp.mapDomain Sum.inl u).prod fun i k => Sum.elim X (⇑C ∘ P.val) i ^ k)) =
    coeff m ((monomial u) s)

Tactic:
rw [monomial_eq, IsScalarTower.algebraMap_eq R S, algebraMap_eq, ← eval₂_comp_left, ← aeval_def]

Result:
case e_g.h.h.a
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
r : Q.rels
u : Q.vars →₀ ℕ
s : S
m : Q.vars →₀ ℕ
⊢ coeff m
      (C ((aeval P.val) (P.σ s)) *
        ((C.comp (algebraMap R S)) 1 * (Finsupp.mapDomain Sum.inl u).prod fun i k => Sum.elim X (⇑C ∘ P.val) i ^ k)) =
    coeff m (C s * u.prod fun n e => X n ^ e)

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
r : Q.rels
⊢ (Finsupp.sum (Q.relation r) fun a b =>
      (aeval (⇑C ∘ P.val)) (P.σ b) *
        ((algebraMap R (MvPolynomial Q.vars S)) 1 *
          (Finsupp.mapDomain Sum.inl a).prod fun i k => Sum.elim X (⇑C ∘ P.val) i ^ k)) =
    Q.relation r

Tactic:
conv_rhs => rw [← Finsupp.sum_single (Q.relation r)]

Result:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
r : Q.rels
⊢ (Finsupp.sum (Q.relation r) fun a b =>
      (aeval (⇑C ∘ P.val)) (P.σ b) *
        ((algebraMap R (MvPolynomial Q.vars S)) 1 *
          (Finsupp.mapDomain Sum.inl a).prod fun i k => Sum.elim X (⇑C ∘ P.val) i ^ k)) =
    Finsupp.sum (Q.relation r) Finsupp.single

Proof state:
case e_g
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
r : Q.rels
⊢ (fun a b =>
      (aeval (⇑C ∘ P.val)) (P.σ b) *
        ((algebraMap R (MvPolynomial Q.vars S)) 1 *
          (Finsupp.mapDomain Sum.inl a).prod fun i k => Sum.elim X (⇑C ∘ P.val) i ^ k)) =
    Finsupp.single

Tactic:
ext u s m

Result:
case e_g.h.h.a
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
r : Q.rels
u : Q.vars →₀ ℕ
s : S
m : Q.vars →₀ ℕ
⊢ coeff m
      ((aeval (⇑C ∘ P.val)) (P.σ s) *
        ((algebraMap R (MvPolynomial Q.vars S)) 1 *
          (Finsupp.mapDomain Sum.inl u).prod fun i k => Sum.elim X (⇑C ∘ P.val) i ^ k)) =
    coeff m (Finsupp.single u s)

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
r : Q.rels
⊢ (Algebra.Presentation.aux Q P) (Algebra.Presentation.comp_relation_aux Q P r) = Q.relation r

Tactic:
simp only [aux, comp_relation_aux, Generators.comp_vars, Sum.elim_inl, map_finsupp_sum]

Result:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
r : Q.rels
⊢ (Finsupp.sum (Q.relation r) fun a b =>
      (aeval (Sum.elim X (⇑C ∘ P.val))) ((rename Sum.inr) (P.σ b) * (monomial (Finsupp.mapDomain Sum.inl a)) 1)) =
    Q.relation r

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
r : Q.rels
⊢ (Finsupp.sum (Q.relation r) fun a b =>
      (aeval (Sum.elim X (⇑C ∘ P.val))) ((rename Sum.inr) (P.σ b) * (monomial (Finsupp.mapDomain Sum.inl a)) 1)) =
    Q.relation r

Tactic:
simp only [_root_.map_mul, aeval_rename, aeval_monomial, Sum.elim_comp_inr]

Result:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
r : Q.rels
⊢ (Finsupp.sum (Q.relation r) fun a b =>
      (aeval (⇑C ∘ P.val)) (P.σ b) *
        ((algebraMap R (MvPolynomial Q.vars S)) 1 *
          (Finsupp.mapDomain Sum.inl a).prod fun i k => Sum.elim X (⇑C ∘ P.val) i ^ k)) =
    Q.relation r

Proof state:
case e_g.h.h.a
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
r : Q.rels
u : Q.vars →₀ ℕ
s : S
m : Q.vars →₀ ℕ
⊢ coeff m
      ((aeval (⇑C ∘ P.val)) (P.σ s) *
        ((algebraMap R (MvPolynomial Q.vars S)) 1 *
          (Finsupp.mapDomain Sum.inl u).prod fun i k => Sum.elim X (⇑C ∘ P.val) i ^ k)) =
    coeff m (Finsupp.single u s)

Tactic:
simp only [MvPolynomial.single_eq_monomial, aeval, AlgHom.coe_mk, coe_eval₂Hom]

Result:
case e_g.h.h.a
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
r : Q.rels
u : Q.vars →₀ ℕ
s : S
m : Q.vars →₀ ℕ
⊢ coeff m
      (eval₂ (algebraMap R (MvPolynomial Q.vars S)) (⇑C ∘ P.val) (P.σ s) *
        ((algebraMap R (MvPolynomial Q.vars S)) 1 *
          (Finsupp.mapDomain Sum.inl u).prod fun i k => Sum.elim X (⇑C ∘ P.val) i ^ k)) =
    coeff m ((monomial u) s)