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
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
P : Presentation R S ι σ
H :
  Eq (α := Ideal (T ⊗[R] P.Ring))
    (RingHom.ker (F := T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S)
      (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S) : T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S))
    (Ideal.map (F := P.Ring →ₐ[R] T ⊗[R] P.Ring) TensorProduct.includeRight
      (RingHom.ker (F := P.Ring →ₐ[R] S) (IsScalarTower.toAlgHom R P.Ring S)))
e : T ⊗[R] MvPolynomial ι R ≃ₐ[T] MvPolynomial ι T := algebraTensorAlgEquiv R T
p q : MvPolynomial ι T
hp :
  Eq (α := T ⊗[R] S)
    (((TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S) : T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S) :
          (a : T ⊗[R] MvPolynomial ι R) → T ⊗[R] S)
        ((e.symm : (a : MvPolynomial ι T) → T ⊗[R] MvPolynomial ι R) p) :
      T ⊗[R] S)
    (((aeval (R := T) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
            MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
          (a : MvPolynomial ι T) → T ⊗[R] S)
        p :
      T ⊗[R] S)
hq :
  Eq (α := T ⊗[R] S)
    (((TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S) : T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S) :
          (a : T ⊗[R] MvPolynomial ι R) → T ⊗[R] S)
        ((e.symm : (a : MvPolynomial ι T) → T ⊗[R] MvPolynomial ι R) q) :
      T ⊗[R] S)
    (((aeval (R := T) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
            MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
          (a : MvPolynomial ι T) → T ⊗[R] S)
        q :
      T ⊗[R] S)
⊢ Eq (α := T ⊗[R] S)
    (((TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S) : T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S) :
          (a : T ⊗[R] MvPolynomial ι R) → T ⊗[R] S)
        ((e.symm : (a : MvPolynomial ι T) → T ⊗[R] MvPolynomial ι R) (p + q)) :
      T ⊗[R] S)
    (((aeval (R := T) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
            MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
          (a : MvPolynomial ι T) → T ⊗[R] S)
        (p + q) :
      T ⊗[R] S)

Tactic:
simp only [map_add, hp, hq]

Premises used: map_add
-- 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_1
inst_3 : CommRing T
inst_4 : Algebra R T
P : Presentation R S ι σ
H :
  Eq (α := Ideal (T ⊗[R] P.Ring))
    (RingHom.ker (F := T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S)
      (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S) : T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S))
    (Ideal.map (F := P.Ring →ₐ[R] T ⊗[R] P.Ring) TensorProduct.includeRight
      (RingHom.ker (F := P.Ring →ₐ[R] S) (IsScalarTower.toAlgHom R P.Ring S)))
e : T ⊗[R] MvPolynomial ι R ≃ₐ[T] MvPolynomial ι T := algebraTensorAlgEquiv R T
p : MvPolynomial ι T
i : ι
hp :
  Eq (α := T ⊗[R] S)
    (((TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S) : T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S) :
          (a : T ⊗[R] MvPolynomial ι R) → T ⊗[R] S)
        ((e.symm : (a : MvPolynomial ι T) → T ⊗[R] MvPolynomial ι R) p) :
      T ⊗[R] S)
    (((aeval (R := T) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
            MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
          (a : MvPolynomial ι T) → T ⊗[R] S)
        p :
      T ⊗[R] S)
⊢ Eq (α := T ⊗[R] S)
    (((TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S) : T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S) :
          (a : T ⊗[R] MvPolynomial ι R) → T ⊗[R] S)
        ((e.symm : (a : MvPolynomial ι T) → T ⊗[R] MvPolynomial ι R) (p * X i)) :
      T ⊗[R] S)
    (((aeval (R := T) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
            MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
          (a : MvPolynomial ι T) → T ⊗[R] S)
        (p * X i) :
      T ⊗[R] S)

Tactic:
simp [hp, e]
-- 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_1
inst_3 : CommRing T
inst_4 : Algebra R T
P : Presentation R S ι σ
x : MvPolynomial ι T
hx :
  Eq (α := T ⊗[R] S)
    (((aeval (R := T) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
            MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
          (a : MvPolynomial ι T) → T ⊗[R] S)
        x :
      T ⊗[R] S)
    (0 : T ⊗[R] S)
H :
  Eq (α := Ideal (T ⊗[R] P.Ring))
    (RingHom.ker (F := T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S)
      (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S) : T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S))
    (Ideal.map (F := P.Ring →ₐ[R] T ⊗[R] P.Ring) TensorProduct.includeRight
      (RingHom.ker (F := P.Ring →ₐ[R] S) (IsScalarTower.toAlgHom R P.Ring S)))
e : T ⊗[R] MvPolynomial ι R ≃ₐ[T] MvPolynomial ι T := algebraTensorAlgEquiv R T
⊢ Membership.mem (α := T ⊗[R] MvPolynomial ι R) (γ := Ideal (T ⊗[R] P.Ring))
    (RingHom.ker (F := T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S)
      (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S) : T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S))
    ((e.symm : (a : MvPolynomial ι T) → T ⊗[R] MvPolynomial ι R) x : T ⊗[R] MvPolynomial ι R)

Tactic:
have H' : e.symm x ∈ RingHom.ker (TensorProduct.map (AlgHom.id R T)
        (IsScalarTower.toAlgHom R P.Ring S)) := by
      rw [RingHom.mem_ker, ← hx]
      clear hx
      induction x using MvPolynomial.induction_on with
      | C a =>
        simp only [algHom_C, TensorProduct.algebraMap_apply,
          algebraMap_self, RingHom.id_apply, e]
        rw [← MvPolynomial.algebraMap_eq, AlgEquiv.commutes]
        simp only [TensorProduct.algebraMap_apply, algebraMap_self, RingHom.id_apply,
          TensorProduct.map_tmul, AlgHom.coe_id, id_eq, map_one]
      | add p q hp hq => simp only [map_add, hp, hq]
      | mul_X p i hp => simp [hp, e]
-- 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_1
inst_3 : CommRing T
inst_4 : Algebra R T
P : Presentation R S ι σ
x : MvPolynomial ι T
hx :
  Eq (α := T ⊗[R] S)
    (((aeval (R := T) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
            MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
          (a : MvPolynomial ι T) → T ⊗[R] S)
        x :
      T ⊗[R] S)
    (0 : T ⊗[R] S)
H :
  Eq (α := Ideal (T ⊗[R] P.Ring))
    (RingHom.ker (F := T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S)
      (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S) : T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S))
    (Ideal.map (F := P.Ring →ₐ[R] T ⊗[R] P.Ring) TensorProduct.includeRight
      (RingHom.ker (F := P.Ring →ₐ[R] S) (IsScalarTower.toAlgHom R P.Ring S)))
e : T ⊗[R] MvPolynomial ι R ≃ₐ[T] MvPolynomial ι T := algebraTensorAlgEquiv R T
H' :
  Membership.mem (α := T ⊗[R] MvPolynomial ι R) (γ := Ideal (T ⊗[R] P.Ring))
    (RingHom.ker (F := T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S)
      (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S) : T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S))
    ((e.symm : (a : MvPolynomial ι T) → T ⊗[R] MvPolynomial ι R) x : T ⊗[R] MvPolynomial ι R)
⊢ Membership.mem (α := T ⊗[R] MvPolynomial ι R) (γ := Ideal (T ⊗[R] P.Ring))
    (Ideal.map (F := P.Ring →ₐ[R] T ⊗[R] P.Ring) TensorProduct.includeRight
      (RingHom.ker (F := P.Ring →ₐ[R] S) (IsScalarTower.toAlgHom R P.Ring S)))
    ((e.symm : (a : MvPolynomial ι T) → T ⊗[R] MvPolynomial ι R) x : T ⊗[R] MvPolynomial ι R)

Tactic:
rw [H] at H'
-- 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_1
inst_3 : CommRing T
inst_4 : Algebra R T
P : Presentation R S ι σ
x : MvPolynomial ι T
hx :
  Eq (α := T ⊗[R] S)
    (((aeval (R := T) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
            MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
          (a : MvPolynomial ι T) → T ⊗[R] S)
        x :
      T ⊗[R] S)
    (0 : T ⊗[R] S)
H :
  Eq (α := Ideal (T ⊗[R] P.Ring))
    (RingHom.ker (F := T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S)
      (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S) : T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S))
    (Ideal.map (F := P.Ring →ₐ[R] T ⊗[R] P.Ring) TensorProduct.includeRight
      (RingHom.ker (F := P.Ring →ₐ[R] S) (IsScalarTower.toAlgHom R P.Ring S)))
e : T ⊗[R] MvPolynomial ι R ≃ₐ[T] MvPolynomial ι T := algebraTensorAlgEquiv R T
H' :
  Membership.mem (α := T ⊗[R] MvPolynomial ι R) (γ := Ideal (T ⊗[R] P.Ring))
    (Ideal.map (F := P.Ring →ₐ[R] T ⊗[R] P.Ring) TensorProduct.includeRight
      (RingHom.ker (F := P.Ring →ₐ[R] S) (IsScalarTower.toAlgHom R P.Ring S)))
    ((e.symm : (a : MvPolynomial ι T) → T ⊗[R] MvPolynomial ι R) x : T ⊗[R] MvPolynomial ι R)
⊢ Membership.mem (α := T ⊗[R] MvPolynomial ι R) (γ := Ideal (T ⊗[R] P.Ring))
    (Ideal.map (F := P.Ring →ₐ[R] T ⊗[R] P.Ring) TensorProduct.includeRight P.ker)
    ((e.symm : (a : MvPolynomial ι T) → T ⊗[R] MvPolynomial ι R) x : T ⊗[R] MvPolynomial ι R)

Tactic:
replace H' : e.symm x ∈ Ideal.map TensorProduct.includeRight P.ker := H'
-- 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_1
inst_3 : CommRing T
inst_4 : Algebra R T
P : Presentation R S ι σ
x : MvPolynomial ι T
hx :
  Eq (α := T ⊗[R] S)
    (((aeval (R := T) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
            MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
          (a : MvPolynomial ι T) → T ⊗[R] S)
        x :
      T ⊗[R] S)
    (0 : T ⊗[R] S)
H :
  Eq (α := Ideal (T ⊗[R] P.Ring))
    (RingHom.ker (F := T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S)
      (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S) : T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S))
    (Ideal.map (F := P.Ring →ₐ[R] T ⊗[R] P.Ring) TensorProduct.includeRight
      (RingHom.ker (F := P.Ring →ₐ[R] S) (IsScalarTower.toAlgHom R P.Ring S)))
e : T ⊗[R] MvPolynomial ι R ≃ₐ[T] MvPolynomial ι T := algebraTensorAlgEquiv R T
H' :
  Membership.mem (α := T ⊗[R] MvPolynomial ι R) (γ := Ideal (T ⊗[R] P.Ring))
    (Ideal.map (F := P.Ring →ₐ[R] T ⊗[R] P.Ring) TensorProduct.includeRight P.ker)
    ((e.symm : (a : MvPolynomial ι T) → T ⊗[R] MvPolynomial ι R) x : T ⊗[R] MvPolynomial ι R)
⊢ Membership.mem (γ := Ideal (MvPolynomial ι T))
    (Ideal.span
      (Set.range
        (Function.comp (β := T ⊗[R] MvPolynomial ι R) (⇑e : (a : T ⊗[R] MvPolynomial ι R) → MvPolynomial ι T)
            (⇑(↑TensorProduct.includeRight : P.Ring →+* T ⊗[R] P.Ring) : (a : P.Ring) → T ⊗[R] MvPolynomial ι R) ∘
          P.relation)))
    x

Tactic:
rw [← P.span_range_relation_eq_ker, ← Ideal.mem_comap, ← Ideal.comap_coe,
      ← AlgEquiv.toRingEquiv_toRingHom, Ideal.comap_coe, AlgEquiv.symm_toRingEquiv,
      Ideal.comap_symm, ← Ideal.map_coe, ← Ideal.map_coe _ (Ideal.span _), Ideal.map_map,
      Ideal.map_span, ← Set.range_comp, AlgEquiv.toRingEquiv_toRingHom, RingHom.coe_comp,
      RingHom.coe_coe] at H'

Premises used: Set.range_comp, AlgEquiv.toRingEquiv_toRingHom, Ideal.comap_symm, RingHom.coe_coe, Ideal.map_span, Algebra.Presentation.span_range_relation_eq_ker, Ideal.map_map, RingHom.coe_comp, Ideal.span, Ideal.comap_coe, AlgEquiv.symm_toRingEquiv, Ideal.mem_comap, Ideal.map_coe
-- 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_1
inst_3 : CommRing T
inst_4 : Algebra R T
P : Presentation R S ι σ
x : MvPolynomial ι T
hx :
  Eq (α := T ⊗[R] S)
    (((aeval (R := T) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
            MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
          (a : MvPolynomial ι T) → T ⊗[R] S)
        x :
      T ⊗[R] S)
    (0 : T ⊗[R] S)
H :
  Eq (α := Ideal (T ⊗[R] P.Ring))
    (RingHom.ker (F := T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S)
      (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S) : T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S))
    (Ideal.map (F := P.Ring →ₐ[R] T ⊗[R] P.Ring) TensorProduct.includeRight
      (RingHom.ker (F := P.Ring →ₐ[R] S) (IsScalarTower.toAlgHom R P.Ring S)))
e : T ⊗[R] MvPolynomial ι R ≃ₐ[T] MvPolynomial ι T := algebraTensorAlgEquiv R T
H' :
  Membership.mem (γ := Ideal (MvPolynomial ι T))
    (Ideal.span
      (Set.range
        (Function.comp (β := T ⊗[R] MvPolynomial ι R) (⇑e : (a : T ⊗[R] MvPolynomial ι R) → MvPolynomial ι T)
            (⇑(↑TensorProduct.includeRight : P.Ring →+* T ⊗[R] P.Ring) : (a : P.Ring) → T ⊗[R] MvPolynomial ι R) ∘
          P.relation)))
    x
⊢ Membership.mem (γ := Ideal (MvPolynomial ι T))
    (Ideal.span
      (Set.range
        (Function.comp (β := T ⊗[R] MvPolynomial ι R) (⇑e : (a : T ⊗[R] MvPolynomial ι R) → MvPolynomial ι T)
            (⇑(↑TensorProduct.includeRight : P.Ring →+* T ⊗[R] P.Ring) : (a : P.Ring) → T ⊗[R] MvPolynomial ι R) ∘
          P.relation)))
    x

Tactic:
H'
-- 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_1
inst_3 : CommRing T
inst_4 : Algebra R T
P : Presentation R S ι σ
x : MvPolynomial ι T
hx :
  Eq (α := T ⊗[R] S)
    (((aeval (R := T) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
            MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
          (a : MvPolynomial ι T) → T ⊗[R] S)
        x :
      T ⊗[R] S)
    (0 : T ⊗[R] S)
H :
  Eq (α := Ideal (T ⊗[R] P.Ring))
    (RingHom.ker (F := T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S)
      (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S) : T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S))
    (Ideal.map (F := P.Ring →ₐ[R] T ⊗[R] P.Ring) TensorProduct.includeRight
      (RingHom.ker (F := P.Ring →ₐ[R] S) (IsScalarTower.toAlgHom R P.Ring S)))
e : T ⊗[R] MvPolynomial ι R ≃ₐ[T] MvPolynomial ι T := algebraTensorAlgEquiv R T
H' :
  Membership.mem (γ := Ideal (MvPolynomial ι T))
    (Ideal.span
      (Set.range
        (Function.comp (β := T ⊗[R] MvPolynomial ι R) (⇑e : (a : T ⊗[R] MvPolynomial ι R) → MvPolynomial ι T)
            (⇑(↑TensorProduct.includeRight : P.Ring →+* T ⊗[R] P.Ring) : (a : P.Ring) → T ⊗[R] MvPolynomial ι R) ∘
          P.relation)))
    x
h :
  ∀ (x : σ),
    Eq (α := MvPolynomial ι T)
      ((MvPolynomial.map (algebraMap R T) : (a : MvPolynomial ι R) → MvPolynomial ι T) (P.relation x) :
        MvPolynomial ι T)
      ((Function.comp (β := T ⊗[R] MvPolynomial ι R) (⇑e : (a : T ⊗[R] MvPolynomial ι R) → MvPolynomial ι T)
              (⇑(↑TensorProduct.includeRight : P.Ring →+* T ⊗[R] P.Ring) : (a : P.Ring) → T ⊗[R] MvPolynomial ι R) ∘
            P.relation)
          x :
        MvPolynomial ι T)
⊢ Membership.mem (γ := Submodule (MvPolynomial ι T) (MvPolynomial ι T))
    (Ideal.span
      (Set.range fun (i : σ) ↦
        (MvPolynomial.map (algebraMap R T) : (a : MvPolynomial ι R) → MvPolynomial ι T) (P.relation i)))
    x

Tactic:
convert! H'
-- 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_1
inst_3 : CommRing T
inst_4 : Algebra R T
P : Presentation R S ι σ
x : MvPolynomial ι T
hx :
  Eq (α := T ⊗[R] S)
    (((aeval (R := T) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
            MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
          (a : MvPolynomial ι T) → T ⊗[R] S)
        x :
      T ⊗[R] S)
    (0 : T ⊗[R] S)
H :
  Eq (α := Ideal (T ⊗[R] P.Ring))
    (RingHom.ker (F := T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S)
      (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S) : T ⊗[R] P.Ring →ₐ[R] T ⊗[R] S))
    (Ideal.map (F := P.Ring →ₐ[R] T ⊗[R] P.Ring) TensorProduct.includeRight
      (RingHom.ker (F := P.Ring →ₐ[R] S) (IsScalarTower.toAlgHom R P.Ring S)))
e : T ⊗[R] MvPolynomial ι R ≃ₐ[T] MvPolynomial ι T := algebraTensorAlgEquiv R T
H' :
  Membership.mem (γ := Ideal (MvPolynomial ι T))
    (Ideal.span
      (Set.range
        (Function.comp (β := T ⊗[R] MvPolynomial ι R) (⇑e : (a : T ⊗[R] MvPolynomial ι R) → MvPolynomial ι T)
            (⇑(↑TensorProduct.includeRight : P.Ring →+* T ⊗[R] P.Ring) : (a : P.Ring) → T ⊗[R] MvPolynomial ι R) ∘
          P.relation)))
    x
x_1 : σ
⊢ Eq (α := MvPolynomial ι T)
    ((MvPolynomial.map (algebraMap R T) : (a : MvPolynomial ι R) → MvPolynomial ι T) (P.relation x_1) :
      MvPolynomial ι T)
    ((Function.comp (β := T ⊗[R] MvPolynomial ι R) (⇑e : (a : T ⊗[R] MvPolynomial ι R) → MvPolynomial ι T)
            (⇑(↑TensorProduct.includeRight : P.Ring →+* T ⊗[R] P.Ring) : (a : P.Ring) → T ⊗[R] MvPolynomial ι R) ∘
          P.relation)
        x_1 :
      MvPolynomial ι T)

Tactic:
simp [e]
-- 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_1
inst_3 : CommRing T
inst_4 : Algebra R T
P : Presentation R S ι σ
⊢ Eq (α := Generators T (T ⊗[R] S) ι) (toGenerators (baseChange T P)) (Generators.baseChange T P.toGenerators)

Tactic:
rfl

Premises used: Algebra.Generators.ofSurjective, Algebra.Generators.baseChange, 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 ι σ
i : ι' ⊕ ι
⊢ Eq (α := MvPolynomial ι' S) ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) (X i) : MvPolynomial ι' S)
    (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) i : MvPolynomial ι' S)

Tactic:
aeval_X (Sum.elim X (C ∘ P.val)) i

Premises used: MvPolynomial.aeval_X, MvPolynomial.X, Function.comp, Algebra.Generators.val, MvPolynomial.C, DFunLike.coe, Algebra.Presentation.toGenerators, 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 ι σ
r : σ'
simp :
  (Finsupp.sum (Q.relation r) fun (a : ι' →₀ ℕ) (b : S) ↦
      (aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val)) :
          (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S)
        (HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
          ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.σ b) : MvPolynomial (ι' ⊕ ι) R)
          ((monomial (Finsupp.mapDomain Sum.inl a) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1 : MvPolynomial (ι' ⊕ ι) R))) =
    Q.relation r
⊢ (Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) (Q.compRelationAux P r) = Q.relation r

Tactic:
simp only [aux, compRelationAux, map_finsuppSum]

Premises used: _private.0.Algebra.Presentation.aux, map_finsuppSum, Algebra.Presentation.compRelationAux
-- 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 ι σ
r : σ'
simp :
  (Finsupp.sum (Q.relation r) fun (a : ι' →₀ ℕ) (b : S) ↦
      HMul.hMul (α := MvPolynomial ι' S)
        ((aeval ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) : (a : MvPolynomial ι R) → MvPolynomial ι' S) (P.σ b) :
          MvPolynomial ι' S)
        (HMul.hMul (α := MvPolynomial ι' S) ((algebraMap R (MvPolynomial ι' S) : (a : R) → MvPolynomial ι' S) 1)
          (Finsupp.prod (Finsupp.mapDomain Sum.inl a) fun (i : ι' ⊕ ι) (k : ℕ) ↦
            HPow.hPow (α := MvPolynomial ι' S) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) i) k))) =
    Q.relation r
⊢ (Finsupp.sum (Q.relation r) fun (a : ι' →₀ ℕ) (b : S) ↦
      (aeval (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val)) :
          (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S)
        (HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
          ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.σ b) : MvPolynomial (ι' ⊕ ι) R)
          ((monomial (Finsupp.mapDomain Sum.inl a) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1 : MvPolynomial (ι' ⊕ ι) R))) =
    Q.relation r

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

Premises used: Sum.elim_comp_inr, map_mul, MvPolynomial.aeval_rename, MvPolynomial.aeval_monomial
-- 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 ι σ
r : σ'
rw : Finsupp.sum (Q.relation r) Finsupp.single
| Q.relation r

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

Premises used: Algebra.Presentation.relation, Finsupp.sum_single
-- 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 ι σ
r : σ'
conv_rhs :
  Eq (α := MvPolynomial ι' S)
    (Finsupp.sum (Q.relation r) fun (a : ι' →₀ ℕ) (b : S) ↦
      HMul.hMul (α := MvPolynomial ι' S)
        ((aeval ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) : (a : MvPolynomial ι R) → MvPolynomial ι' S) (P.σ b) :
          MvPolynomial ι' S)
        (HMul.hMul (α := MvPolynomial ι' S) ((algebraMap R (MvPolynomial ι' S) : (a : R) → MvPolynomial ι' S) 1)
          (Finsupp.prod (Finsupp.mapDomain Sum.inl a) fun (i : ι' ⊕ ι) (k : ℕ) ↦
            HPow.hPow (α := MvPolynomial ι' S) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) i) k)))
    (Finsupp.sum (Q.relation r) Finsupp.single)
⊢ (Finsupp.sum (Q.relation r) fun (a : ι' →₀ ℕ) (b : S) ↦
      HMul.hMul (α := MvPolynomial ι' S)
        ((aeval ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) : (a : MvPolynomial ι R) → MvPolynomial ι' S) (P.σ b) :
          MvPolynomial ι' S)
        (HMul.hMul (α := MvPolynomial ι' S) ((algebraMap R (MvPolynomial ι' S) : (a : R) → MvPolynomial ι' S) 1)
          (Finsupp.prod (Finsupp.mapDomain Sum.inl a) fun (i : ι' ⊕ ι) (k : ℕ) ↦
            HPow.hPow (α := MvPolynomial ι' S) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) i) k))) =
    Q.relation r

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

Premises used: Algebra.Presentation.relation, Finsupp.sum_single