-- Mathlib/RingTheory/Presentation.lean
private lemma span_range_relation_eq_ker_comp : Ideal.span
    (Set.range (Sum.elim (Algebra.Presentation.comp_relation_aux Q P)
      fun rp ↦ (rename Sum.inr) (P.relation rp))) = (Q.comp P.toGenerators).ker

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
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
⊢ Ideal.span (Set.range (Algebra.Presentation.comp_relation_aux Q P)) ⊔
      Ideal.span (Set.range fun rp => (rename Sum.inr) (P.relation rp)) =
    Ideal.span (Set.range (Algebra.Presentation.comp_relation_aux Q P)) ⊔
      Ideal.span (⇑(rename Sum.inr) '' Set.range P.relation)

Tactic:
congr

Result:
case e_a.e_s
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
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
⊢ (Set.range fun rp => (rename Sum.inr) (P.relation rp)) = ⇑(rename Sum.inr) '' Set.range P.relation

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
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
⊢ Ideal.span
      (Set.range (Sum.elim (Algebra.Presentation.comp_relation_aux Q P) fun rp => (rename Sum.inr) (P.relation rp))) =
    (Q.comp P.toGenerators).ker

Tactic:
rw [Generators.ker_eq_ker_aeval_val, Q.aeval_comp_val_eq, ← AlgHom.comap_ker]

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
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
⊢ Ideal.span
      (Set.range (Sum.elim (Algebra.Presentation.comp_relation_aux Q P) fun rp => (rename Sum.inr) (P.relation rp))) =
    Ideal.comap (Algebra.Presentation.aux Q P) (RingHom.ker (aevalTower (IsScalarTower.toAlgHom R S T) Q.val))

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
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
⊢ Ideal.span
      (Set.range (Sum.elim (Algebra.Presentation.comp_relation_aux Q P) fun rp => (rename Sum.inr) (P.relation rp))) =
    Ideal.span (Set.range (Algebra.Presentation.comp_relation_aux Q P)) ⊔ RingHom.ker (Algebra.Presentation.aux Q P)

Tactic:
rw [Set.Sum.elim_range, Ideal.span_union, Q.aux_ker, ← P.ker_eq_ker_aeval_val,
  ← P.span_range_relation_eq_ker, Ideal.map_span]

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
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
⊢ Ideal.span (Set.range (Algebra.Presentation.comp_relation_aux Q P)) ⊔
      Ideal.span (Set.range fun rp => (rename Sum.inr) (P.relation rp)) =
    Ideal.span (Set.range (Algebra.Presentation.comp_relation_aux Q P)) ⊔
      Ideal.span (⇑(rename Sum.inr) '' Set.range P.relation)

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
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
⊢ Ideal.span
      (Set.range (Sum.elim (Algebra.Presentation.comp_relation_aux Q P) fun rp => (rename Sum.inr) (P.relation rp))) =
    Ideal.comap (Algebra.Presentation.aux Q P) (RingHom.ker (aevalTower (IsScalarTower.toAlgHom R S T) Q.val))

Tactic:
show _ = Ideal.comap _ (RingHom.ker (aeval Q.val))

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
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
⊢ Ideal.span
      (Set.range (Sum.elim (Algebra.Presentation.comp_relation_aux Q P) fun rp => (rename Sum.inr) (P.relation rp))) =
    Ideal.comap (Algebra.Presentation.aux Q P) (RingHom.ker (aeval Q.val))

Proof state:
case e_a.e_s
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
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
⊢ (Set.range fun rp => (rename Sum.inr) (P.relation rp)) = ⇑(rename Sum.inr) '' Set.range P.relation

Tactic:
ext

Result:
case e_a.e_s.h
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
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
x✝ : MvPolynomial (Q.vars ⊕ P.vars) R
⊢ (x✝ ∈ Set.range fun rp => (rename Sum.inr) (P.relation rp)) ↔ x✝ ∈ ⇑(rename Sum.inr) '' Set.range P.relation

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
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
⊢ Ideal.span
      (Set.range (Sum.elim (Algebra.Presentation.comp_relation_aux Q P) fun rp => (rename Sum.inr) (P.relation rp))) =
    Ideal.comap (Algebra.Presentation.aux Q P) (RingHom.ker (aeval Q.val))

Tactic:
rw [← Q.ker_eq_ker_aeval_val, ← Q.span_range_relation_eq_ker, ← Q.aux_image_relation P,
  ← Ideal.map_span, Ideal.comap_map_of_surjective' _ (Q.aux_surjective P)]

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
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
⊢ Ideal.span
      (Set.range (Sum.elim (Algebra.Presentation.comp_relation_aux Q P) fun rp => (rename Sum.inr) (P.relation rp))) =
    Ideal.span (Set.range (Algebra.Presentation.comp_relation_aux Q P)) ⊔ RingHom.ker (Algebra.Presentation.aux Q P)

Proof state:
case e_a.e_s.h
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
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
x✝ : MvPolynomial (Q.vars ⊕ P.vars) R
⊢ (x✝ ∈ Set.range fun rp => (rename Sum.inr) (P.relation rp)) ↔ x✝ ∈ ⇑(rename Sum.inr) '' Set.range P.relation

Tactic:
simp

Result:
no goals