awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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
this :
  Eq (α := MvPolynomial Unit R →ₐ[R] S) (aeval (Generators.val (Generators.localizationAway S r)))
    (AlgHom.comp
      (↑(mvPolynomialQuotientEquiv S r) :
        MvPolynomial Unit R ⧸ Ideal.span {(C : (a : R) → MvPolynomial Unit R) r * X () - 1} →ₐ[R] S)
      (Ideal.Quotient.mkₐ R
        (Ideal.span
          {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
                ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
              1})))
⊢ Eq (α := Ideal (Generators.Ring (Generators.localizationAway S r))) (Generators.ker (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})
have rw : Eq (α := Ideal (Generators.Ring (Generators.localizationAway S r)))
  (Ideal.comap (F :=
    MvPolynomial Unit R →+*
      HasQuotient.Quotient (MvPolynomial Unit R) (B := Ideal (MvPolynomial Unit R))
        (Ideal.span
          {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
                ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
              1}))
    (↑(Ideal.Quotient.mkₐ R
          (Ideal.span
            {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
                  ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
                1})) :
      MvPolynomial Unit R →+* MvPolynomial Unit R ⧸ Ideal.span {(C : (a : R) → MvPolynomial Unit R) r * X () - 1})
    (RingHom.ker (F :=
      RingHom.{u, v}
        (HasQuotient.Quotient (MvPolynomial Unit R) (B := Ideal (MvPolynomial Unit R))
          (Ideal.span
            {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
                  ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
                1}))
        S)
      (↑(↑(mvPolynomialQuotientEquiv S r) :
            MvPolynomial Unit R ⧸ Ideal.span {(C : (a : R) → MvPolynomial Unit R) r * X () - 1} →ₐ[R] S) :
        MvPolynomial Unit R ⧸ Ideal.span {(C : (a : R) → MvPolynomial Unit R) r * X () - 1} →+* S)))
  (Ideal.span
    {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
          ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
        1})
Tactic: rw [Generators.ker_eq_ker_aeval_val, this, ← RingHom.ker_coe_toRingHom, AlgHom.comp_toRingHom,
    ← RingHom.comap_ker]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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
      (Set.range fun (x : Unit) ↦
        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))
have simp : 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: simp only [Set.range_const]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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 (α := 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))
have 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))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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))
⊢ 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))
have 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)))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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 ι σ
⊢ 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))
have 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))
Tactic: rw [Ideal.span_le]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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
⊢ 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))
have 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))
Tactic: ⟨y, hy⟩
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (hypothesis)
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
⊢ 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))
have Z : 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
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (hypothesis)
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)
⊢ 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))
have 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)
Tactic: apply_fun TensorProduct.includeRight (R := R) (A := T) at Z
Cleared hypotheses: Z
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (hypothesis)
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)
⊢ 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))
have 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)
Tactic: rw [map_zero] at Z
Cleared hypotheses: Z
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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)
⊢ 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))
have 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)
Tactic: simp only [SetLike.mem_coe, RingHom.mem_ker, ← Z, ← hy,
      TensorProduct.includeRight_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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 := 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)
have 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)
Tactic: rw [aeval_map_algebraMap T (P.baseChange T).val (P.relation y)]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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)
    (1 ⊗ₜ[R] (aeval P.val : (a : MvPolynomial ι R) → S) (P.relation y) : T ⊗[R] S)
have 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)
Tactic: change _ = TensorProduct.includeRight.toRingHom _
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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)
    ((AlgHom.toRingHom TensorProduct.includeRight : (a : S) → T ⊗[R] S)
        ((aeval P.val : (a : MvPolynomial ι R) → S) (P.relation y)) :
      T ⊗[R] S)
have 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)
Tactic: rw [map_aeval, AlgHom.toRingHom_eq_coe, RingHom.coe_coe,
      TensorProduct.includeRight.comp_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (hypothesis)
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
⊢ 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
have 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)
Tactic: rw [RingHom.mem_ker] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (hypothesis)
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)
⊢ 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
have 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)))
Tactic: have H := Algebra.TensorProduct.lTensor_ker (A := T) (IsScalarTower.toAlgHom R P.Ring S)
      P.algebraMap_surjective
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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)
have 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)
Tactic: rw [RingHom.mem_ker, ← hx]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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)
        ((e.symm : (a : MvPolynomial ι T) → T ⊗[R] MvPolynomial ι R) ((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)
        ((C : (a : T) → MvPolynomial ι T) a) :
      T ⊗[R] S)
have 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)
        ((C : (a : T) → MvPolynomial ι T) a)) :
    T ⊗[R] S)
  (a ⊗ₜ[R] 1 : T ⊗[R] S)
Tactic: simp only [algHom_C, TensorProduct.algebraMap_apply,
          algebraMap_self, RingHom.id_apply, e]