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
P : Presentation R S ι σ
r : R
inst_3 : IsLocalization.Away r S
⊢ Eq (α := Ideal (Generators.Ring (Generators.localizationAway S r)))
    (Ideal.span
      {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
            ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
          1})
    (Generators.ker (Generators.localizationAway S r))

Tactic:
exact (Generators.ker_localizationAway r).symm

Premises used: Algebra.Generators.ker_localizationAway, Eq.symm
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
⊢ dimension (localizationAway S r) = 0

Tactic:
simp [Presentation.dimension]

Premises used: Algebra.Presentation.dimension
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
⊢ Membership.mem (γ := Ideal (Generators.Ring (Generators.localizationAway S r)))
    (Generators.ker (Generators.localizationAway S r))
    (HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
        ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
      1)

Tactic:
(Presentation.localizationAway S r).relation_mem_ker ()

Premises used: Unit.unit, Set.Mem, Algebra.Presentation.relation_mem_ker, Algebra.Presentation.localizationAway, Algebra.Generators.localizationAway
-- 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 ι σ
a :
  LE.le (α := Ideal (MvPolynomial ι T))
    (Ideal.span
      (Set.range fun (i : σ) ↦
        (MvPolynomial.map (algebraMap R T) : (a : MvPolynomial ι R) → MvPolynomial ι T) (P.relation i)))
    (RingHom.ker (F := MvPolynomial ι T →ₐ[T] T ⊗[R] S)
      (aeval (R := T) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
        MvPolynomial ι T →ₐ[T] T ⊗[R] S))
a₁ :
  LE.le (α := Ideal (MvPolynomial ι T))
    (RingHom.ker (F := MvPolynomial ι T →ₐ[T] T ⊗[R] S)
      (aeval (R := T) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
        MvPolynomial ι T →ₐ[T] T ⊗[R] S))
    (Ideal.span
      (Set.range fun (i : σ) ↦
        (MvPolynomial.map (algebraMap R T) : (a : MvPolynomial ι R) → MvPolynomial ι T) (P.relation i)))
⊢ Eq (α := Ideal (MvPolynomial ι T))
    (Ideal.span
      (Set.range fun (i : σ) ↦
        (MvPolynomial.map (algebraMap R T) : (a : MvPolynomial ι R) → MvPolynomial ι T) (P.relation i)))
    (RingHom.ker (F := MvPolynomial ι T →ₐ[T] T ⊗[R] S)
      (aeval (R := T) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
        MvPolynomial ι T →ₐ[T] T ⊗[R] S))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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 ι σ
a :
  (Set.range fun (i : σ) ↦
      (MvPolynomial.map (algebraMap R T) : (a : MvPolynomial ι R) → MvPolynomial ι T) (P.relation i)) ⊆
    (↑(RingHom.ker (F := MvPolynomial ι T →ₐ[T] T ⊗[R] S)
          (aeval (R := T) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
            MvPolynomial ι T →ₐ[T] T ⊗[R] S)) :
      Set (MvPolynomial ι T))
⊢ LE.le (α := Ideal (MvPolynomial ι T))
    (Ideal.span
      (Set.range fun (i : σ) ↦
        (MvPolynomial.map (algebraMap R T) : (a : MvPolynomial ι R) → MvPolynomial ι T) (P.relation i)))
    (RingHom.ker (F := MvPolynomial ι T →ₐ[T] T ⊗[R] S)
      (aeval (R := T) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
        MvPolynomial ι T →ₐ[T] T ⊗[R] S))

Tactic:
rw [Ideal.span_le]

Premises used: Ideal.span_le
-- 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
a :
  ∀ (y : σ)
    (hy :
      (fun (i : σ) ↦
            ((MvPolynomial.map (algebraMap R T) : (a : MvPolynomial ι R) → MvPolynomial ι T) (P.relation i) :
              MvPolynomial ι T))
          y =
        x),
    x ∈
      (↑(RingHom.ker (F := MvPolynomial ι T →ₐ[T] T ⊗[R] S)
            (aeval (R := T) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
              MvPolynomial ι T →ₐ[T] T ⊗[R] S)) :
        Set (MvPolynomial ι T))
⊢ Membership.mem (γ := Set (MvPolynomial ι T))
      (Set.range fun (i : σ) ↦
        (MvPolynomial.map (algebraMap R T) : (a : MvPolynomial ι R) → MvPolynomial ι T) (P.relation i))
      x →
    x ∈
      (↑(RingHom.ker (F := MvPolynomial ι T →ₐ[T] T ⊗[R] S)
            (aeval (R := T) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
              MvPolynomial ι T →ₐ[T] T ⊗[R] S)) :
        Set (MvPolynomial ι T))

Tactic:
⟨y, hy⟩
-- 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
y : σ
hy :
  (fun (i : σ) ↦
        ((MvPolynomial.map (algebraMap R T) : (a : MvPolynomial ι R) → MvPolynomial ι T) (P.relation i) :
          MvPolynomial ι T))
      y =
    x
⊢ Eq.{v + 1} (α := S) ((aeval P.val : (a : MvPolynomial ι R) → S) (P.relation y) : S) (0 : S)

Tactic:
have Z := aeval_val_relation P y
-- 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
y : σ
hy :
  (fun (i : σ) ↦
        ((MvPolynomial.map (algebraMap R T) : (a : MvPolynomial ι R) → MvPolynomial ι T) (P.relation i) :
          MvPolynomial ι T))
      y =
    x
Z : Eq.{v + 1} (α := S) ((aeval P.val : (a : MvPolynomial ι R) → S) (P.relation y) : S) (0 : S)
⊢ Eq (α := T ⊗[R] S)
    ((TensorProduct.includeRight : (a : S) → T ⊗[R] S) ((aeval P.val : (a : MvPolynomial ι R) → S) (P.relation y)) :
      T ⊗[R] S)
    ((TensorProduct.includeRight : (a : S) → T ⊗[R] S) 0 : T ⊗[R] S)

Tactic:
apply_fun TensorProduct.includeRight (R := R) (A := T) at Z

Premises used: Algebra.TensorProduct.includeRight
-- 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
y : σ
hy :
  (fun (i : σ) ↦
        ((MvPolynomial.map (algebraMap R T) : (a : MvPolynomial ι R) → MvPolynomial ι T) (P.relation i) :
          MvPolynomial ι T))
      y =
    x
Z :
  Eq (α := T ⊗[R] S)
    ((TensorProduct.includeRight : (a : S) → T ⊗[R] S) ((aeval P.val : (a : MvPolynomial ι R) → S) (P.relation y)) :
      T ⊗[R] S)
    ((TensorProduct.includeRight : (a : S) → T ⊗[R] S) 0 : T ⊗[R] S)
⊢ Eq (α := T ⊗[R] S)
    ((TensorProduct.includeRight : (a : S) → T ⊗[R] S) ((aeval P.val : (a : MvPolynomial ι R) → S) (P.relation y)) :
      T ⊗[R] S)
    (0 : T ⊗[R] S)

Tactic:
rw [map_zero] at Z

Premises used: map_zero
-- 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
y : σ
hy :
  (fun (i : σ) ↦
        ((MvPolynomial.map (algebraMap R T) : (a : MvPolynomial ι R) → MvPolynomial ι T) (P.relation i) :
          MvPolynomial ι T))
      y =
    x
Z :
  Eq (α := T ⊗[R] S)
    ((TensorProduct.includeRight : (a : S) → T ⊗[R] S) ((aeval P.val : (a : MvPolynomial ι R) → S) (P.relation y)) :
      T ⊗[R] S)
    (0 : T ⊗[R] S)
a :
  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)
        ((MvPolynomial.map (algebraMap R T) : (a : MvPolynomial ι R) → MvPolynomial ι T) (P.relation y)) :
      T ⊗[R] S)
    (1 ⊗ₜ[R] (aeval P.val : (a : MvPolynomial ι R) → S) (P.relation y) : T ⊗[R] S)
⊢ x ∈
    (↑(RingHom.ker (F := MvPolynomial ι T →ₐ[T] T ⊗[R] S)
          (aeval (R := T) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
            MvPolynomial ι T →ₐ[T] T ⊗[R] S)) :
      Set (MvPolynomial ι T))

Tactic:
simp only [SetLike.mem_coe, RingHom.mem_ker, ← Z, ← hy,
      TensorProduct.includeRight_apply]

Premises used: Algebra.TensorProduct.includeRight_apply, RingHom.mem_ker, SetLike.mem_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
y : σ
hy :
  (fun (i : σ) ↦
        ((MvPolynomial.map (algebraMap R T) : (a : MvPolynomial ι R) → MvPolynomial ι T) (P.relation i) :
          MvPolynomial ι T))
      y =
    x
Z :
  Eq (α := T ⊗[R] S)
    ((TensorProduct.includeRight : (a : S) → T ⊗[R] S) ((aeval P.val : (a : MvPolynomial ι R) → S) (P.relation y)) :
      T ⊗[R] S)
    (0 : T ⊗[R] S)
a :
  Eq (α := T ⊗[R] S)
    (((aeval (R := R) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
            MvPolynomial ι R →ₐ[R] T ⊗[R] S) :
          (a : MvPolynomial ι R) → T ⊗[R] S)
        (P.relation y) :
      T ⊗[R] S)
    (1 ⊗ₜ[R] (aeval P.val : (a : MvPolynomial ι R) → S) (P.relation y) : T ⊗[R] S)
⊢ 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)
        ((MvPolynomial.map (algebraMap R T) : (a : MvPolynomial ι R) → MvPolynomial ι T) (P.relation y)) :
      T ⊗[R] S)
    (1 ⊗ₜ[R] (aeval P.val : (a : MvPolynomial ι R) → S) (P.relation y) : T ⊗[R] S)

Tactic:
rw [aeval_map_algebraMap T (P.baseChange T).val (P.relation y)]

Premises used: Algebra.Generators.baseChange, Algebra.Presentation.relation, MvPolynomial.aeval_map_algebraMap, Algebra.Generators.val, 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
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
P : Presentation R S ι σ
x : MvPolynomial ι T
y : σ
hy :
  (fun (i : σ) ↦
        ((MvPolynomial.map (algebraMap R T) : (a : MvPolynomial ι R) → MvPolynomial ι T) (P.relation i) :
          MvPolynomial ι T))
      y =
    x
Z :
  Eq (α := T ⊗[R] S)
    ((TensorProduct.includeRight : (a : S) → T ⊗[R] S) ((aeval P.val : (a : MvPolynomial ι R) → S) (P.relation y)) :
      T ⊗[R] S)
    (0 : T ⊗[R] S)
a :
  Eq (α := T ⊗[R] S)
    (((aeval (R := R) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
            MvPolynomial ι R →ₐ[R] T ⊗[R] S) :
          (a : MvPolynomial ι R) → T ⊗[R] S)
        (P.relation y) :
      T ⊗[R] S)
    ((AlgHom.toRingHom TensorProduct.includeRight : (a : S) → T ⊗[R] S)
        ((aeval P.val : (a : MvPolynomial ι R) → S) (P.relation y)) :
      T ⊗[R] S)
⊢ Eq (α := T ⊗[R] S)
    (((aeval (R := R) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
            MvPolynomial ι R →ₐ[R] T ⊗[R] S) :
          (a : MvPolynomial ι R) → T ⊗[R] S)
        (P.relation y) :
      T ⊗[R] S)
    (1 ⊗ₜ[R] (aeval P.val : (a : MvPolynomial ι R) → S) (P.relation y) : T ⊗[R] S)

Tactic:
change _ = TensorProduct.includeRight.toRingHom _

Premises used: AlgHom.toRingHom, DFunLike.coe, Algebra.TensorProduct.includeRight
-- 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
y : σ
hy :
  (fun (i : σ) ↦
        ((MvPolynomial.map (algebraMap R T) : (a : MvPolynomial ι R) → MvPolynomial ι T) (P.relation i) :
          MvPolynomial ι T))
      y =
    x
Z :
  Eq (α := T ⊗[R] S)
    ((TensorProduct.includeRight : (a : S) → T ⊗[R] S) ((aeval P.val : (a : MvPolynomial ι R) → S) (P.relation y)) :
      T ⊗[R] S)
    (0 : T ⊗[R] S)
a :
  Eq (α := T ⊗[R] S)
    (((aeval (R := R) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
            MvPolynomial ι R →ₐ[R] T ⊗[R] S) :
          (a : MvPolynomial ι R) → T ⊗[R] S)
        (P.relation y) :
      T ⊗[R] S)
    ((eval₂Hom (algebraMap R (T ⊗[R] S)) fun (i : ι) ↦ (TensorProduct.includeRight : (a : S) → T ⊗[R] S) (P.val i) :
          (a : MvPolynomial ι R) → T ⊗[R] S)
        (P.relation y) :
      T ⊗[R] S)
⊢ Eq (α := T ⊗[R] S)
    (((aeval (R := R) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
            MvPolynomial ι R →ₐ[R] T ⊗[R] S) :
          (a : MvPolynomial ι R) → T ⊗[R] S)
        (P.relation y) :
      T ⊗[R] S)
    ((AlgHom.toRingHom TensorProduct.includeRight : (a : S) → T ⊗[R] S)
        ((aeval P.val : (a : MvPolynomial ι R) → S) (P.relation y)) :
      T ⊗[R] S)

Tactic:
rw [map_aeval, AlgHom.toRingHom_eq_coe, RingHom.coe_coe,
      TensorProduct.includeRight.comp_algebraMap]

Premises used: AlgHom.comp_algebraMap, MvPolynomial.map_aeval, RingHom.coe_coe, AlgHom.toRingHom_eq_coe, Algebra.TensorProduct.includeRight
-- 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
y : σ
hy :
  (fun (i : σ) ↦
        ((MvPolynomial.map (algebraMap R T) : (a : MvPolynomial ι R) → MvPolynomial ι T) (P.relation i) :
          MvPolynomial ι T))
      y =
    x
Z :
  Eq (α := T ⊗[R] S)
    ((TensorProduct.includeRight : (a : S) → T ⊗[R] S) ((aeval P.val : (a : MvPolynomial ι R) → S) (P.relation y)) :
      T ⊗[R] S)
    (0 : T ⊗[R] S)
⊢ Eq (α := T ⊗[R] S)
    (((aeval (R := R) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
            MvPolynomial ι R →ₐ[R] T ⊗[R] S) :
          (a : MvPolynomial ι R) → T ⊗[R] S)
        (P.relation y) :
      T ⊗[R] S)
    ((eval₂Hom (algebraMap R (T ⊗[R] S)) fun (i : ι) ↦ (TensorProduct.includeRight : (a : S) → T ⊗[R] S) (P.val i) :
          (a : MvPolynomial ι R) → T ⊗[R] S)
        (P.relation y) :
      T ⊗[R] S)

Tactic:
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
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
P : Presentation R S ι σ
x : MvPolynomial ι T
hx :
  Membership.mem (γ := Submodule (MvPolynomial ι T) (MvPolynomial ι T))
    (RingHom.ker (F := MvPolynomial ι T →ₐ[T] T ⊗[R] S)
      (aeval (R := T) (S₁ := T ⊗[R] S) (Generators.val (Generators.baseChange T P.toGenerators)) :
        MvPolynomial ι T →ₐ[T] T ⊗[R] S))
    x
⊢ 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)

Tactic:
rw [RingHom.mem_ker] at hx

Premises used: RingHom.mem_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
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)
⊢ 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)))

Tactic:
have H := Algebra.TensorProduct.lTensor_ker (A := T) (IsScalarTower.toAlgHom R P.Ring S)
      P.algebraMap_surjective
-- 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
rw :
  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) x) :
      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)
⊢ 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:
rw [RingHom.mem_ker, ← hx]

Premises used: RingHom.mem_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
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
a : T
C :
  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)
        ((AlgEquiv.symm (algebraTensorAlgEquiv R T) : (a : MvPolynomial ι T) → T ⊗[R] MvPolynomial ι R)
          ((MvPolynomial.C : (a : T) → MvPolynomial ι T) a)) :
      T ⊗[R] S)
    (a ⊗ₜ[R] 1 : 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)
          ((MvPolynomial.C : (a : T) → MvPolynomial ι T) a)) :
      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)
        ((MvPolynomial.C : (a : T) → MvPolynomial ι T) a) :
      T ⊗[R] S)

Tactic:
simp only [algHom_C, TensorProduct.algebraMap_apply,
          algebraMap_self, RingHom.id_apply, e]

Premises used: Algebra.TensorProduct.algebraMap_apply, RingHom.id_apply, Algebra.algebraMap_self, MvPolynomial.algHom_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_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
a : T
⊢ 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)
        ((algebraMap T (T ⊗[R] MvPolynomial ι R) : (a : T) → T ⊗[R] MvPolynomial ι R) a) :
      T ⊗[R] S)
    (a ⊗ₜ[R] 1 : T ⊗[R] S)

Tactic:
simp only [TensorProduct.algebraMap_apply, algebraMap_self, RingHom.id_apply,
          TensorProduct.map_tmul, AlgHom.coe_id, id_eq, map_one]

Premises used: Algebra.TensorProduct.algebraMap_apply, RingHom.id_apply, Algebra.algebraMap_self, AlgHom.coe_id, Algebra.TensorProduct.map_tmul, map_one, id_eq