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
ι : 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
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
⊢ 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)
have C : ∀ (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)
Tactic: 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]
Cleared hypotheses: x
-- 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)
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 (γ := 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' : 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]
-- 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)
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 (γ := 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'₁ : 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'
Cleared hypotheses: H'
-- 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)
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 (γ := 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'₁ : 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'
Cleared hypotheses: H'
-- 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)
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 (γ := 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'₁ : 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'
Cleared hypotheses: H'
-- 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
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 (γ := 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 : ∀ (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)
Tactic: convert! H'
-- 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
ι' : 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 : σ'
⊢ (Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) (Q.compRelationAux P r) = Q.relation r
have 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
Tactic: simp only [aux, compRelationAux, map_finsuppSum]
-- 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
ι' : 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 : σ'
⊢ (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
have 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
Tactic: simp only [map_mul, aeval_rename, aeval_monomial, Sum.elim_comp_inr]
-- 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
ι' : 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 : σ'
| Q.relation r
have rw : Finsupp.sum (Q.relation r) Finsupp.single
Tactic: rw [← Finsupp.sum_single (Q.relation r)]
-- 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
ι' : 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 : σ'
⊢ (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
have 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)
Tactic: conv_rhs => rw [← Finsupp.sum_single (Q.relation r)]
-- 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
ι' : 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 : σ'
⊢ 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)
have e_g : Eq (α := (ι' →₀ ℕ) → S → MvPolynomial ι' S)
  (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.single
Tactic: congr
-- 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
ι' : 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 : σ'
⊢ Eq (α := (ι' →₀ ℕ) → S → MvPolynomial ι' S)
    (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.single
have e_g : ∀ (u : ι' →₀ ℕ) (s : S) (m : ι' →₀ ℕ),
  coeff m
      (HMul.hMul (α := MvPolynomial ι' S)
        ((aeval ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) : (a : MvPolynomial ι R) → MvPolynomial ι' S) (P.σ s) :
          MvPolynomial ι' S)
        (HMul.hMul (α := MvPolynomial ι' S) ((algebraMap R (MvPolynomial ι' S) : (a : R) → MvPolynomial ι' S) 1)
          (Finsupp.prod (Finsupp.mapDomain Sum.inl u) fun (i : ι' ⊕ ι) (k : ℕ) ↦
            HPow.hPow (α := MvPolynomial ι' S) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) i) k))) =
    coeff m (Finsupp.single u s)
Tactic: ext u s m
-- 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
ι' : 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 : σ'
u : ι' →₀ ℕ
s : S
m : ι' →₀ ℕ
⊢ coeff m
      (HMul.hMul (α := MvPolynomial ι' S)
        ((aeval ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) : (a : MvPolynomial ι R) → MvPolynomial ι' S) (P.σ s) :
          MvPolynomial ι' S)
        (HMul.hMul (α := MvPolynomial ι' S) ((algebraMap R (MvPolynomial ι' S) : (a : R) → MvPolynomial ι' S) 1)
          (Finsupp.prod (Finsupp.mapDomain Sum.inl u) fun (i : ι' ⊕ ι) (k : ℕ) ↦
            HPow.hPow (α := MvPolynomial ι' S) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) i) k))) =
    coeff m (Finsupp.single u s)
have e_g : coeff m
    (eval₂ (algebraMap R (MvPolynomial ι' S)) ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) (P.σ s) *
      HMul.hMul (α := MvPolynomial ι' S) ((algebraMap R (MvPolynomial ι' S) : (a : R) → MvPolynomial ι' S) 1)
        (Finsupp.prod (Finsupp.mapDomain Sum.inl u) fun (i : ι' ⊕ ι) (k : ℕ) ↦
          HPow.hPow (α := MvPolynomial ι' S) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) i) k)) =
  coeff m ((monomial u : (a : S) → MvPolynomial ι' S) s)
Tactic: simp only [MvPolynomial.single_eq_monomial, aeval, AlgHom.coe_mk, coe_eval₂Hom]
-- 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
ι' : 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 : σ'
u : ι' →₀ ℕ
s : S
m : ι' →₀ ℕ
⊢ coeff m
      (eval₂ (algebraMap R (MvPolynomial ι' S)) ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) (P.σ s) *
        HMul.hMul (α := MvPolynomial ι' S) ((algebraMap R (MvPolynomial ι' S) : (a : R) → MvPolynomial ι' S) 1)
          (Finsupp.prod (Finsupp.mapDomain Sum.inl u) fun (i : ι' ⊕ ι) (k : ℕ) ↦
            HPow.hPow (α := MvPolynomial ι' S) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) i) k)) =
    coeff m ((monomial u : (a : S) → MvPolynomial ι' S) s)
have e_g : coeff m
    (HMul.hMul (α := MvPolynomial ι' S)
      ((C : (a : S) → MvPolynomial ι' S) ((aeval P.val : (a : MvPolynomial ι R) → S) (P.σ s)) : MvPolynomial ι' S)
      (HMul.hMul (α := MvPolynomial ι' S) ((RingHom.comp C (algebraMap R S) : (a : R) → MvPolynomial ι' S) 1)
        (Finsupp.prod (Finsupp.mapDomain Sum.inl u) fun (i : ι' ⊕ ι) (k : ℕ) ↦
          HPow.hPow (α := MvPolynomial ι' S) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) i) k))) =
  coeff m
    (HMul.hMul (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
      ((C : (a : S) → MvPolynomial ι' S) s : MvPolynomial ι' S)
      (u.prod fun (n : ι') (e : ℕ) ↦ HPow.hPow (α := MvPolynomial ι' S) (X n) e : MvPolynomial ι' S))
Tactic: rw [monomial_eq, IsScalarTower.algebraMap_eq R S, algebraMap_eq, ← eval₂_comp_left, ← aeval_def]
-- 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
ι' : 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 ι σ
a : S
⊢ ∃ (a_1 : MvPolynomial (ι' ⊕ ι) R),
    Eq (α := MvPolynomial ι' S) ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S) a_1 : MvPolynomial ι' S)
      ((C : (a : S) → MvPolynomial ι' S) a : MvPolynomial ι' S)
have h : Eq (α := MvPolynomial ι' S)
  ((Q.aux P : (a : MvPolynomial (ι' ⊕ ι) R) → MvPolynomial ι' S)
      ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.σ a)) :
    MvPolynomial ι' S)
  ((C : (a : S) → MvPolynomial ι' S) a : MvPolynomial ι' S)
Tactic: use rename Sum.inr <| P.σ a