awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
val : ι
⊢ Eq (α := MvPolynomial ι' S)
    ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) (X (Sum.inr val)) : MvPolynomial ι' S)
    ((AlgHom.comp (mapAlgHom (aeval P.val))
            (↑(sumAlgEquiv R ι' ι) : MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R)) :
          (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S)
        (X (Sum.inr val)) :
      MvPolynomial ι' S)

Tactic:
simp
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
rw :
  Eq (α := Ideal (MvPolynomial (ι' ⊕ ι) R))
    (Ideal.comap (F := MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R))
      (↑(sumAlgEquiv R ι' ι) : MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R))
      (Ideal.map (F := MvPolynomial ι R →+* MvPolynomial ι' (MvPolynomial ι R)) C
        (RingHom.ker (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val))))
    (Ideal.map (F := MvPolynomial ι R →ₐ[R] MvPolynomial (ι' ⊕ ι) R) (rename Sum.inr)
      (RingHom.ker (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val)))
⊢ Eq (α := Ideal (MvPolynomial (ι' ⊕ ι) R)) (RingHom.ker (Q.aux P))
    (Ideal.map (F := MvPolynomial ι R →ₐ[R] MvPolynomial (ι' ⊕ ι) R) (rename Sum.inr)
      (RingHom.ker (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val)))

Tactic:
rw [aux_eq_comp, ← AlgHom.comap_ker, MvPolynomial.ker_mapAlgHom]

Premises used: AlgHom.comap_ker, _private.0.Algebra.Presentation.aux_eq_comp, MvPolynomial.ker_mapAlgHom
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
change :
  Eq (α := Ideal (MvPolynomial (ι' ⊕ ι) R))
    (Ideal.comap (F := MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R))
      (↑(sumAlgEquiv R ι' ι) : MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R))
      (Ideal.map (F := MvPolynomial ι R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R))
        (IsScalarTower.toAlgHom R (MvPolynomial ι R) (MvPolynomial ι' (MvPolynomial ι R)))
        (RingHom.ker (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val))))
    (Ideal.map (F := MvPolynomial ι R →ₐ[R] MvPolynomial (ι' ⊕ ι) R) (rename Sum.inr)
      (RingHom.ker (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val)))
⊢ Eq (α := Ideal (MvPolynomial (ι' ⊕ ι) R))
    (Ideal.comap (F := MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R))
      (↑(sumAlgEquiv R ι' ι) : MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R))
      (Ideal.map (F := MvPolynomial ι R →+* MvPolynomial ι' (MvPolynomial ι R)) C
        (RingHom.ker (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val))))
    (Ideal.map (F := MvPolynomial ι R →ₐ[R] MvPolynomial (ι' ⊕ ι) R) (rename Sum.inr)
      (RingHom.ker (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val)))

Tactic:
change Ideal.comap _ (Ideal.map (IsScalarTower.toAlgHom R (MvPolynomial ι R) _) _) = _

Premises used: IsScalarTower.toAlgHom, Ideal.map, MvPolynomial, Ideal.comap
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
hf :
  Function.Bijective (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial ι' (MvPolynomial ι R))
    (⇑(↑(sumAlgEquiv R ι' ι) : MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R)) :
      (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' (MvPolynomial ι R))
⊢ Eq (α := Ideal (MvPolynomial (ι' ⊕ ι) R))
    (Ideal.comap (F := MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R))
      (↑(sumAlgEquiv R ι' ι) : MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R))
      (Ideal.map (F := MvPolynomial ι R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R))
        (IsScalarTower.toAlgHom R (MvPolynomial ι R) (MvPolynomial ι' (MvPolynomial ι R)))
        (RingHom.ker (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val))))
    (Ideal.map (F := MvPolynomial ι R →ₐ[R] MvPolynomial (ι' ⊕ ι) R) (rename Sum.inr)
      (RingHom.ker (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val)))

Tactic:
rw [← sumAlgEquiv_comp_rename_inr, ← Ideal.map_mapₐ, Ideal.comap_map_of_bijective]

Premises used: MvPolynomial.sumAlgEquiv_comp_rename_inr, Ideal.comap_map_of_bijective, Ideal.map_mapₐ
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
⊢ Function.Bijective (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial ι' (MvPolynomial ι R))
    (⇑(↑(sumAlgEquiv R ι' ι) : MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' (MvPolynomial ι R)) :
      (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' (MvPolynomial ι R))

Tactic:
simpa using AlgEquiv.bijective (sumAlgEquiv R ι' ι)

Premises used: MvPolynomial.sumAlgEquiv, AlgEquiv.bijective
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
hf :
  ∀ (i : ι' ⊕ ι),
    Eq.{u_3 + 1} (α := T)
      ((aeval (Generators.val (Q.comp P.toGenerators)) : (a : MvPolynomial (ι' ⊕ ι) R) → T) (X i) : T)
      ((AlgHom.comp (aevalTower (IsScalarTower.toAlgHom R S T) Q.val) (Q.aux P) : (a : MvPolynomial (ι' ⊕ ι) R) → T)
          (X i) :
        T)
⊢ Eq (α := MvPolynomial (ι' ⊕ ι) R →ₐ[R] T) (aeval (Generators.val (Q.comp P.toGenerators)))
    (AlgHom.comp (aevalTower (IsScalarTower.toAlgHom R S T) Q.val) (Q.aux P))

Tactic:
ext i
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
i : ι' ⊕ ι
hf :
  Eq.{u_3 + 1} (α := T) ((aeval (Generators.val (Q.comp P.toGenerators)) : (a : MvPolynomial (ι' ⊕ ι) R) → T) (X i) : T)
    ((aevalTower (IsScalarTower.toAlgHom R S T) Q.val : (a : MvPolynomial ι' S) → T)
        ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) (X i) : MvPolynomial ι' S) :
      T)
⊢ Eq.{u_3 + 1} (α := T) ((aeval (Generators.val (Q.comp P.toGenerators)) : (a : MvPolynomial (ι' ⊕ ι) R) → T) (X i) : T)
    ((AlgHom.comp (aevalTower (IsScalarTower.toAlgHom R S T) Q.val) (Q.aux P) : (a : MvPolynomial (ι' ⊕ ι) R) → T)
        (X i) :
      T)

Tactic:
simp only [AlgHom.coe_comp, Function.comp_apply]

Premises used: AlgHom.coe_comp, Function.comp_apply
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
i : ι' ⊕ ι
hf :
  ∀ (val : ι'),
    Eq.{u_3 + 1} (α := T)
      ((aeval (Generators.val (Q.comp P.toGenerators)) : (a : MvPolynomial (ι' ⊕ ι) R) → T) (X (Sum.inl val)) : T)
      ((aevalTower (IsScalarTower.toAlgHom R S T) Q.val : (a : MvPolynomial ι' S) → T)
          ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) (X (Sum.inl val)) : MvPolynomial ι' S) :
        T)
hf₁ :
  ∀ (val : ι),
    Eq.{u_3 + 1} (α := T)
      ((aeval (Generators.val (Q.comp P.toGenerators)) : (a : MvPolynomial (ι' ⊕ ι) R) → T) (X (Sum.inr val)) : T)
      ((aevalTower (IsScalarTower.toAlgHom R S T) Q.val : (a : MvPolynomial ι' S) → T)
          ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) (X (Sum.inr val)) : MvPolynomial ι' S) :
        T)
⊢ Eq.{u_3 + 1} (α := T) ((aeval (Generators.val (Q.comp P.toGenerators)) : (a : MvPolynomial (ι' ⊕ ι) R) → T) (X i) : T)
    ((aevalTower (IsScalarTower.toAlgHom R S T) Q.val : (a : MvPolynomial ι' S) → T)
        ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) (X i) : MvPolynomial ι' S) :
      T)

Tactic:
cases i
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
val : ι'
⊢ Eq.{u_3 + 1} (α := T)
    ((aeval (Generators.val (Q.comp P.toGenerators)) : (a : MvPolynomial (ι' ⊕ ι) R) → T) (X (Sum.inl val)) : T)
    ((aevalTower (IsScalarTower.toAlgHom R S T) Q.val : (a : MvPolynomial ι' S) → T)
        ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) (X (Sum.inl val)) : MvPolynomial ι' S) :
      T)

Tactic:
simp
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
val : ι
⊢ Eq.{u_3 + 1} (α := T)
    ((aeval (Generators.val (Q.comp P.toGenerators)) : (a : MvPolynomial (ι' ⊕ ι) R) → T) (X (Sum.inr val)) : T)
    ((aevalTower (IsScalarTower.toAlgHom R S T) Q.val : (a : MvPolynomial ι' S) → T)
        ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) (X (Sum.inr val)) : MvPolynomial ι' S) :
      T)

Tactic:
simp
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
rw :
  Eq (α := Ideal (MvPolynomial (ι' ⊕ ι) R))
    (Ideal.span
      (Set.range (ι := σ' ⊕ σ)
        (Sum.elim (Q.compRelationAux P) fun (rp : σ) ↦
          (rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.relation rp))))
    (Ideal.comap (Q.aux P)
      (RingHom.ker (F := MvPolynomial ι' S →ₐ[R] T) (aevalTower (IsScalarTower.toAlgHom R S T) Q.val)))
⊢ Ideal.span
      (Set.range (ι := σ' ⊕ σ)
        (Sum.elim (Q.compRelationAux P) fun (rp : σ) ↦
          (rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.relation rp))) =
    Generators.ker (Q.comp P.toGenerators)

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

Premises used: _private.0.Algebra.Presentation.aeval_comp_val_eq, AlgHom.comap_ker, Algebra.Generators.ker_eq_ker_aeval_val
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
change :
  Eq (α := Ideal (MvPolynomial (ι' ⊕ ι) R))
    (Ideal.span
      (Set.range (ι := σ' ⊕ σ)
        (Sum.elim (Q.compRelationAux P) fun (rp : σ) ↦
          (rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.relation rp))))
    (Ideal.comap (Q.aux P) (RingHom.ker (F := MvPolynomial ι' S →ₐ[S] T) (aeval Q.val)))
⊢ Eq (α := Ideal (MvPolynomial (ι' ⊕ ι) R))
    (Ideal.span
      (Set.range (ι := σ' ⊕ σ)
        (Sum.elim (Q.compRelationAux P) fun (rp : σ) ↦
          (rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.relation rp))))
    (Ideal.comap (Q.aux P)
      (RingHom.ker (F := MvPolynomial ι' S →ₐ[R] T) (aevalTower (IsScalarTower.toAlgHom R S T) Q.val)))

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

Premises used: MvPolynomial.aeval, Ideal.comap, Algebra.Generators.val, Algebra.Presentation.toGenerators, RingHom.ker
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
rw :
  Eq (α := Ideal (MvPolynomial (ι' ⊕ ι) R))
    (Ideal.span
      (Set.range (ι := σ' ⊕ σ)
        (Sum.elim (Q.compRelationAux P) fun (rp : σ) ↦
          (rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.relation rp))))
    (Ideal.span (Set.range (Q.compRelationAux P)) ⊔ RingHom.ker (Q.aux P))
⊢ Eq (α := Ideal (MvPolynomial (ι' ⊕ ι) R))
    (Ideal.span
      (Set.range (ι := σ' ⊕ σ)
        (Sum.elim (Q.compRelationAux P) fun (rp : σ) ↦
          (rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.relation rp))))
    (Ideal.comap (Q.aux P) (RingHom.ker (F := MvPolynomial ι' S →ₐ[S] T) (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)]

Premises used: Ideal.map_span, Algebra.Presentation.span_range_relation_eq_ker, _private.0.Algebra.Presentation.aux_surjective, Algebra.Generators.ker_eq_ker_aeval_val, Ideal.comap_map_of_surjective', Algebra.Presentation.toGenerators, _private.0.Algebra.Presentation.aux_image_relation
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
rw :
  Eq (α := Ideal (MvPolynomial (ι' ⊕ ι) R))
    (Ideal.span (Set.range (Q.compRelationAux P)) ⊔
      Ideal.span
        (Set.range fun (rp : σ) ↦ (rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.relation rp)))
    (Ideal.span (Set.range (Q.compRelationAux P)) ⊔
      Ideal.span ((⇑(rename Sum.inr) : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) '' Set.range P.relation))
⊢ Eq (α := Ideal (MvPolynomial (ι' ⊕ ι) R))
    (Ideal.span
      (Set.range (ι := σ' ⊕ σ)
        (Sum.elim (Q.compRelationAux P) fun (rp : σ) ↦
          (rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.relation rp))))
    (Ideal.span (Set.range (Q.compRelationAux P)) ⊔ RingHom.ker (Q.aux 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]

Premises used: _private.0.Algebra.Presentation.aux_ker, Set.Sum.elim_range, Ideal.map_span, Algebra.Presentation.span_range_relation_eq_ker, Algebra.Generators.ker_eq_ker_aeval_val, Ideal.span_union, Algebra.Presentation.toGenerators
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
e_a :
  Eq (α := Set (MvPolynomial (ι' ⊕ ι) R))
    (Set.range fun (rp : σ) ↦ (rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.relation rp))
    ((⇑(rename Sum.inr) : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) '' Set.range P.relation)
⊢ Eq (α := Ideal (MvPolynomial (ι' ⊕ ι) R))
    (Ideal.span (Set.range (Q.compRelationAux P)) ⊔
      Ideal.span
        (Set.range fun (rp : σ) ↦ (rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.relation rp)))
    (Ideal.span (Set.range (Q.compRelationAux P)) ⊔
      Ideal.span ((⇑(rename Sum.inr) : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) '' Set.range P.relation))

Tactic:
congr
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
e_a :
  ∀ (x : MvPolynomial (ι' ⊕ ι) R),
    Membership.mem (γ := Set (MvPolynomial (ι' ⊕ ι) R))
        (Set.range fun (rp : σ) ↦ (rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.relation rp))
        x ↔
      Membership.mem (γ := Set (MvPolynomial (ι' ⊕ ι) R))
        ((⇑(rename Sum.inr) : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) '' Set.range P.relation) x
⊢ Eq (α := Set (MvPolynomial (ι' ⊕ ι) R))
    (Set.range fun (rp : σ) ↦ (rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.relation rp))
    ((⇑(rename Sum.inr) : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) '' Set.range P.relation)

Tactic:
ext
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
x : MvPolynomial (ι' ⊕ ι) R
⊢ Membership.mem (γ := Set (MvPolynomial (ι' ⊕ ι) R))
      (Set.range fun (rp : σ) ↦ (rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.relation rp)) x ↔
    Membership.mem (γ := Set (MvPolynomial (ι' ⊕ ι) R))
      ((⇑(rename Sum.inr) : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) '' Set.range P.relation) x

Tactic:
simp
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
⊢ Eq (α := Generators R T (ι' ⊕ ι)) (toGenerators (Q.comp P)) (Q.comp P.toGenerators)

Tactic:
rfl

Premises used: Algebra.Generators.comp, rfl
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
r : σ
⊢ Eq (α := Generators.Ring (toGenerators (Q.comp P))) (relation (Q.comp P) (Sum.inr r))
    ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.relation r))

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
r : σ'
⊢ (Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) (relation (Q.comp P) (Sum.inl r)) = Q.relation r

Tactic:
simp [comp_relation, compRelationAux_map]

Premises used: _private.0.Algebra.Presentation.compRelationAux_map, Algebra.Presentation.comp_relation
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
g : S
inst_7 : IsLocalization.Away g T
P : Presentation R S ι σ
h1 : P.σ (-1) = -1
h0 : P.σ 0 = 0
r : Unit
simp :
  (Finsupp.sum
      (HAdd.hAdd (α := MvPolynomial Unit S) (β := MvPolynomial Unit S)
        ((monomial (Finsupp.single () 1) : (a : S) → MvPolynomial Unit S) g : MvPolynomial Unit S)
        ((C : (a : S) → MvPolynomial Unit S) (-1) : MvPolynomial Unit S))
      fun (x : Unit →₀ ℕ) (j : S) ↦
      HMul.hMul (α := MvPolynomial.{w, u} (Unit ⊕ ι) R) (β := MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ j) :
          MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((monomial (Finsupp.mapDomain Sum.inl x) : (a : R) → MvPolynomial (Unit ⊕ ι) R) 1 :
          MvPolynomial.{w, u} (Unit ⊕ ι) R)) =
    HMul.hMul (α := MvPolynomial.{w, u} (Unit ⊕ ι) R) (β := MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ g) :
          MvPolynomial.{w, u} (Unit ⊕ ι) R)
        (X (Sum.inl ())) +
      (C : (a : R) → MvPolynomial (Unit ⊕ ι) R) (-1)
⊢ relation (comp (localizationAway T g) P) (Sum.inl r) =
    HMul.hMul (α := MvPolynomial.{w, u} (Unit ⊕ ι) R) (β := MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ g) :
          MvPolynomial.{w, u} (Unit ⊕ ι) R)
        (X (Sum.inl ())) -
      1

Tactic:
simp only [Presentation.comp, Sum.elim_inl, Presentation.compRelationAux,
    Presentation.localizationAway_relation, sub_eq_add_neg, C_mul_X_eq_monomial,
    ← map_one C, ← map_neg C]

Premises used: Algebra.Presentation.localizationAway_relation, sub_eq_add_neg, MvPolynomial.C_mul_X_eq_monomial, Algebra.Presentation.comp, map_neg, map_one, Sum.elim_inl, Algebra.Presentation.compRelationAux, MvPolynomial.C
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
g : S
inst_7 : IsLocalization.Away g T
P : Presentation R S ι σ
h1 : P.σ (-1) = -1
h0 : P.σ 0 = 0
r : Unit
⊢ (Finsupp.sum
      (HAdd.hAdd (α := MvPolynomial Unit S) (β := MvPolynomial Unit S)
        ((monomial (Finsupp.single () 1) : (a : S) → MvPolynomial Unit S) g : MvPolynomial Unit S)
        ((C : (a : S) → MvPolynomial Unit S) (-1) : MvPolynomial Unit S))
      fun (x : Unit →₀ ℕ) (j : S) ↦
      HMul.hMul (α := MvPolynomial.{w, u} (Unit ⊕ ι) R) (β := MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ j) :
          MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((monomial (Finsupp.mapDomain Sum.inl x) : (a : R) → MvPolynomial (Unit ⊕ ι) R) 1 :
          MvPolynomial.{w, u} (Unit ⊕ ι) R)) =
    HMul.hMul (α := MvPolynomial.{w, u} (Unit ⊕ ι) R) (β := MvPolynomial.{w, u} (Unit ⊕ ι) R)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ g) :
          MvPolynomial.{w, u} (Unit ⊕ ι) R)
        (X (Sum.inl ())) +
      (C : (a : R) → MvPolynomial (Unit ⊕ ι) R) (-1)

Tactic:
(Finsupp.sum_single_add_single (Finsupp.single () 1) 0 g (-1 : S) _ ?_ ?_).trans ?_

Premises used: Unit.unit, Finsupp.sum_single_add_single, OfNat.ofNat, Neg.neg, Eq.trans, Finsupp.single