awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq.{u_1 + 1} (α := M → M) (ground.{u, u_1, u_1} (R := R) id) _root_.id
have h : ∀ (x : M), ground.{u, u_1, u_1} (R := R) id x = _root_.id x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
⊢ ground.{u, u_1, u_1} (R := R) id m = m
have rw : _root_.id m = m
Tactic: rw [ground_id, id_eq]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
rw : _root_.id m = m
⊢ ground.{u, u_1, u_1} (R := R) id m = m
have rw₁ : m = m
Tactic: rw [ground_id, id_eq]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_3
inst_5 : AddCommMonoid P
inst_6 : Module R P
Q : Type u_4
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
f_1 : M →ₚₗ[R] N
g_1 : N →ₚₗ[R] P
h : P →ₚₗ[R] Q
g : N →ₚₗ[R] P
f : M →ₚₗ[R] N
S : Type u
inst_9 : CommSemiring S
inst_10 : Algebra R S
S' : Type u
inst_11 : CommSemiring S'
inst_12 : Algebra R S'
φ : S →ₐ[R] S'
⊢ Eq (α := S ⊗[R] M → S' ⊗[R] P) ((⇑(rTensor P φ.toLinearMap) : (a : S ⊗[R] P) → S' ⊗[R] P) ∘ g.toFun' S ∘ f.toFun' S)
    ((g.toFun' S' ∘ f.toFun' S') ∘ (⇑(rTensor M φ.toLinearMap) : (a : S ⊗[R] M) → S' ⊗[R] M))
have h₁ : ∀ (x : S ⊗[R] M),
  Eq (α := S' ⊗[R] P) (((⇑(rTensor P φ.toLinearMap) : (a : S ⊗[R] P) → S' ⊗[R] P) ∘ g.toFun' S ∘ f.toFun' S) x)
    (((g.toFun' S' ∘ f.toFun' S') ∘ (⇑(rTensor M φ.toLinearMap) : (a : S ⊗[R] M) → S' ⊗[R] M)) x)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
N : Type u_2
inst_1 : AddCommMonoid N
inst_2 : Module R N
P : Type u_3
inst_3 : AddCommMonoid P
inst_4 : Module R P
g : N →ₚₗ[R] P
⊢ g.comp id = g
have toFun' : ∀ (x : Type u) (x_1 : CommSemiring x) (x_2 : Algebra R x) (x_3 : x ⊗[R] N), (g.comp id).toFun' x x_3 = g.toFun' x x_3
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
⊢ comp id f = f
have toFun' : ∀ (x : Type u) (x_1 : CommSemiring x) (x_2 : Algebra R x) (x_3 : x ⊗[R] M), (comp id f).toFun' x x_3 = f.toFun' x x_3
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
inst_2 : Algebra R S
s : Finset S
⊢ Eq (α := Subalgebra R S)
    (AlgHom.range (A := MvPolynomial (Fin s.card) R)
      (aeval fun (n : Fin s.card) ↦ (↑((s.equivFin.symm : (a : Fin s.card) → ↥s) n) : S)))
    (Algebra.adjoin R (↑s : Set S))
have rw : Eq (α := Subalgebra R S)
  (Algebra.adjoin R (Set.range fun (n : Fin s.card) ↦ (↑((s.equivFin.symm : (a : Fin s.card) → ↥s) n) : S)))
  (Algebra.adjoin R (↑s : Set S))
Tactic: rw [← Algebra.adjoin_range_eq_range_aeval]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
inst_2 : Algebra R S
s : Finset S
⊢ Eq (α := Subalgebra R S)
    (Algebra.adjoin R (Set.range fun (n : Fin s.card) ↦ (↑((s.equivFin.symm : (a : Fin s.card) → ↥s) n) : S)))
    (Algebra.adjoin R (↑s : Set S))
have e_s : (Set.range fun (n : Fin s.card) ↦ (↑((s.equivFin.symm : (a : Fin s.card) → ↥s) n) : S)) = (↑s : Set S)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
inst_2 : Algebra R S
s : Finset S
⊢ (Set.range fun (n : Fin s.card) ↦ (↑((s.equivFin.symm : (a : Fin s.card) → ↥s) n) : S)) = (↑s : Set S)
have e_s : Set.image (α := ↥s) (Subtype.val (p := fun (x : S) ↦ x ∈ s))
    (Set.range (ι := Fin s.card) (⇑s.equivFin.symm : (a : Fin s.card) → ↥s)) =
  (↑s : Set S)
Tactic: rw [← Function.comp_def, Set.range_comp]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type v
inst_5 : CommSemiring S
inst_6 : Algebra R S
f : M →ₚₗ[R] N
A : Type u
inst_7 : CommSemiring A
inst_8 : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst_9 : CommSemiring T
inst_10 : Algebra R T
B : Type u
inst_11 : CommSemiring B
inst_12 : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : AlgHom.{u, v, w} R ↥φ.range ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  Eq (α := TensorProduct.{u, w, u_1} R (↥ψ.range) M)
    ((rTensor M (h'.comp φ.rangeRestrict).toLinearMap : (a : A ⊗[R] M) → ↥ψ.range ⊗[R] M) p :
      TensorProduct.{u, w, u_1} R (↥ψ.range) M)
    ((rTensor M ψ.rangeRestrict.toLinearMap : (a : B ⊗[R] M) → ↥ψ.range ⊗[R] M) q :
      TensorProduct.{u, w, u_1} R (↥ψ.range) M)
θ : RingCon.Quotient (RingCon.ker (↑φ : A →+* S)) →ₐ[R] RingCon.Quotient (RingCon.ker (↑ψ : B →+* T)) :=
  (↑(quotientKerEquivRangeₐ ψ).symm : ↥ψ.range →ₐ[R] (RingCon.ker (↑ψ : B →+* T)).Quotient).comp
    (h'.comp (↑(quotientKerEquivRangeₐ φ) : (RingCon.ker (↑φ : A →+* S)).Quotient →ₐ[R] ↥φ.range))
⊢ (h.comp φ.range.val).comp (↑(quotientKerEquivRangeₐ φ) : (RingCon.ker (↑φ : A →+* S)).Quotient →ₐ[R] ↥φ.range) =
    ψ.range.val.comp ((↑(quotientKerEquivRangeₐ ψ) : (RingCon.ker (↑ψ : B →+* T)).Quotient →ₐ[R] ↥ψ.range).comp θ)
have simp : (ψ.range.val.comp h').comp (↑(quotientKerEquivRangeₐ φ) : (RingCon.ker (↑φ : A →+* S)).Quotient →ₐ[R] ↥φ.range) =
  (((ψ.range.val.comp (↑(quotientKerEquivRangeₐ ψ) : (RingCon.ker (↑ψ : B →+* T)).Quotient →ₐ[R] ↥ψ.range)).comp
            (↑(quotientKerEquivRangeₐ ψ).symm : ↥ψ.range →ₐ[R] (RingCon.ker (↑ψ : B →+* T)).Quotient)).comp
        h').comp
    (↑(quotientKerEquivRangeₐ φ) : (RingCon.ker (↑φ : A →+* S)).Quotient →ₐ[R] ↥φ.range)
Tactic: simp only [θ, ← AlgHom.comp_assoc, ← hh']
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type v
inst_5 : CommSemiring S
inst_6 : Algebra R S
f : M →ₚₗ[R] N
A : Type u
inst_7 : CommSemiring A
inst_8 : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst_9 : CommSemiring T
inst_10 : Algebra R T
B : Type u
inst_11 : CommSemiring B
inst_12 : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : AlgHom.{u, v, w} R ↥φ.range ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  Eq (α := TensorProduct.{u, w, u_1} R (↥ψ.range) M)
    ((rTensor M (h'.comp φ.rangeRestrict).toLinearMap : (a : A ⊗[R] M) → ↥ψ.range ⊗[R] M) p :
      TensorProduct.{u, w, u_1} R (↥ψ.range) M)
    ((rTensor M ψ.rangeRestrict.toLinearMap : (a : B ⊗[R] M) → ↥ψ.range ⊗[R] M) q :
      TensorProduct.{u, w, u_1} R (↥ψ.range) M)
θ : RingCon.Quotient (RingCon.ker (↑φ : A →+* S)) →ₐ[R] RingCon.Quotient (RingCon.ker (↑ψ : B →+* T)) :=
  (↑(quotientKerEquivRangeₐ ψ).symm : ↥ψ.range →ₐ[R] (RingCon.ker (↑ψ : B →+* T)).Quotient).comp
    (h'.comp (↑(quotientKerEquivRangeₐ φ) : (RingCon.ker (↑φ : A →+* S)).Quotient →ₐ[R] ↥φ.range))
⊢ Eq (α := T ⊗[R] N) ((rTensor N (h.comp φ).toLinearMap : (a : A ⊗[R] N) → T ⊗[R] N) (f.toFun' A p) : T ⊗[R] N)
    ((rTensor N ψ.toLinearMap : (a : B ⊗[R] N) → T ⊗[R] N) (f.toFun' B q) : T ⊗[R] N)
have ht : (h.comp φ.range.val).comp (↑(quotientKerEquivRangeₐ φ) : (RingCon.ker (↑φ : A →+* S)).Quotient →ₐ[R] ↥φ.range) =
  ψ.range.val.comp ((↑(quotientKerEquivRangeₐ ψ) : (RingCon.ker (↑ψ : B →+* T)).Quotient →ₐ[R] ↥ψ.range).comp θ)
Tactic: have ht : (h.comp φ.range.val).comp (quotientKerEquivRangeₐ φ).toAlgHom =
      ψ.range.val.comp ((quotientKerEquivRangeₐ ψ).toAlgHom.comp θ) := by
    simp only [θ, ← AlgHom.comp_assoc, ← hh']
    simp [AlgHom.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type v
inst_5 : CommSemiring S
inst_6 : Algebra R S
f : M →ₚₗ[R] N
A : Type u
inst_7 : CommSemiring A
inst_8 : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst_9 : CommSemiring T
inst_10 : Algebra R T
B : Type u
inst_11 : CommSemiring B
inst_12 : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : AlgHom.{u, v, w} R ↥φ.range ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  Eq (α := TensorProduct.{u, w, u_1} R (↥ψ.range) M)
    ((rTensor M (h'.comp φ.rangeRestrict).toLinearMap : (a : A ⊗[R] M) → ↥ψ.range ⊗[R] M) p :
      TensorProduct.{u, w, u_1} R (↥ψ.range) M)
    ((rTensor M ψ.rangeRestrict.toLinearMap : (a : B ⊗[R] M) → ↥ψ.range ⊗[R] M) q :
      TensorProduct.{u, w, u_1} R (↥ψ.range) M)
θ : RingCon.Quotient (RingCon.ker (↑φ : A →+* S)) →ₐ[R] RingCon.Quotient (RingCon.ker (↑ψ : B →+* T)) :=
  (↑(quotientKerEquivRangeₐ ψ).symm : ↥ψ.range →ₐ[R] (RingCon.ker (↑ψ : B →+* T)).Quotient).comp
    (h'.comp (↑(quotientKerEquivRangeₐ φ) : (RingCon.ker (↑φ : A →+* S)).Quotient →ₐ[R] ↥φ.range))
ht :
  (h.comp φ.range.val).comp (↑(quotientKerEquivRangeₐ φ) : (RingCon.ker (↑φ : A →+* S)).Quotient →ₐ[R] ↥φ.range) =
    ψ.range.val.comp ((↑(quotientKerEquivRangeₐ ψ) : (RingCon.ker (↑ψ : B →+* T)).Quotient →ₐ[R] ↥ψ.range).comp θ)
⊢ Eq (α := T ⊗[R] N) ((rTensor N (h.comp φ).toLinearMap : (a : A ⊗[R] N) → T ⊗[R] N) (f.toFun' A p) : T ⊗[R] N)
    ((rTensor N ψ.toLinearMap : (a : B ⊗[R] N) → T ⊗[R] N) (f.toFun' B q) : T ⊗[R] N)
have rw : Eq (α := T ⊗[R] N)
  ((rTensor N
          ((ψ.range.val.comp
                  ((↑(quotientKerEquivRangeₐ ψ) : (RingCon.ker (↑ψ : B →+* T)).Quotient →ₐ[R] ↥ψ.range).comp θ)).comp
              (mkₐ R (RingCon.ker (↑φ : A →+* S)))).toLinearMap :
        (a : A ⊗[R] N) → T ⊗[R] N)
      (f.toFun' A p) :
    T ⊗[R] N)
  ((rTensor N
          (ψ.range.val.comp
              ((↑(quotientKerEquivRangeₐ ψ) : (RingCon.ker (↑ψ : B →+* T)).Quotient →ₐ[R] ↥ψ.range).comp
                (mkₐ R (RingCon.ker (↑ψ : B →+* T))))).toLinearMap :
        (a : B ⊗[R] N) → T ⊗[R] N)
      (f.toFun' B q) :
    T ⊗[R] N)
Tactic: rw [← φ.val_comp_rangeRestrict, ← quotientKerEquivRangeₐ_comp_mkₐ φ,
    ← ψ.val_comp_rangeRestrict, ← quotientKerEquivRangeₐ_comp_mkₐ ψ,
    ← AlgHom.comp_assoc, ← AlgHom.comp_assoc _, ht]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type v
inst_5 : CommSemiring S
inst_6 : Algebra R S
f : M →ₚₗ[R] N
A : Type u
inst_7 : CommSemiring A
inst_8 : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst_9 : CommSemiring T
inst_10 : Algebra R T
B : Type u
inst_11 : CommSemiring B
inst_12 : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : AlgHom.{u, v, w} R ↥φ.range ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  Eq (α := TensorProduct.{u, w, u_1} R (↥ψ.range) M)
    ((rTensor M (h'.comp φ.rangeRestrict).toLinearMap : (a : A ⊗[R] M) → ↥ψ.range ⊗[R] M) p :
      TensorProduct.{u, w, u_1} R (↥ψ.range) M)
    ((rTensor M ψ.rangeRestrict.toLinearMap : (a : B ⊗[R] M) → ↥ψ.range ⊗[R] M) q :
      TensorProduct.{u, w, u_1} R (↥ψ.range) M)
θ : RingCon.Quotient (RingCon.ker (↑φ : A →+* S)) →ₐ[R] RingCon.Quotient (RingCon.ker (↑ψ : B →+* T)) :=
  (↑(quotientKerEquivRangeₐ ψ).symm : ↥ψ.range →ₐ[R] (RingCon.ker (↑ψ : B →+* T)).Quotient).comp
    (h'.comp (↑(quotientKerEquivRangeₐ φ) : (RingCon.ker (↑φ : A →+* S)).Quotient →ₐ[R] ↥φ.range))
ht :
  (h.comp φ.range.val).comp (↑(quotientKerEquivRangeₐ φ) : (RingCon.ker (↑φ : A →+* S)).Quotient →ₐ[R] ↥φ.range) =
    ψ.range.val.comp ((↑(quotientKerEquivRangeₐ ψ) : (RingCon.ker (↑ψ : B →+* T)).Quotient →ₐ[R] ↥ψ.range).comp θ)
⊢ Eq (α := RingCon.Quotient (RingCon.ker (↑ψ : B →+* T)) ⊗[R] N)
    (f.toFun' (RingCon.Quotient (RingCon.ker (↑ψ : B →+* T)))
      ((rTensor M
            ((↑(quotientKerEquivRangeₐ ψ).symm : ↥ψ.range →ₐ[R] (RingCon.ker (↑ψ : B →+* T)).Quotient).comp
                (h'.comp
                  ((↑(quotientKerEquivRangeₐ φ) : (RingCon.ker (↑φ : A →+* S)).Quotient →ₐ[R] ↥φ.range).comp
                    (mkₐ R (RingCon.ker (↑φ : A →+* S)))))).toLinearMap :
          (a : A ⊗[R] M) → (RingCon.ker (↑ψ : B →+* T)).Quotient ⊗[R] M)
        p))
    (f.toFun' (RingCon.Quotient (RingCon.ker (↑ψ : B →+* T)))
      ((rTensor M (toLinearMap (mkₐ R (RingCon.ker (↑ψ : B →+* T)))) :
          (a : B ⊗[R] M) → (RingCon.ker (↑ψ : B →+* T)).Quotient ⊗[R] M)
        q))
have h₁ : Eq (α := RingCon.Quotient (RingCon.ker (↑ψ : B →+* T)) ⊗[R] N)
  (f.toFun' (RingCon.Quotient (RingCon.ker (↑ψ : B →+* T)))
    ((rTensor M
          (((↑(quotientKerEquivRangeₐ ψ).symm : ↥ψ.range →ₐ[R] (RingCon.ker (↑ψ : B →+* T)).Quotient).comp
                  (↑(quotientKerEquivRangeₐ ψ) : (RingCon.ker (↑ψ : B →+* T)).Quotient →ₐ[R] ↥ψ.range)).comp
              (mkₐ R (RingCon.ker (↑ψ : B →+* T)))).toLinearMap :
        (a : B ⊗[R] M) → (RingCon.ker (↑ψ : B →+* T)).Quotient ⊗[R] M)
      q))
  (f.toFun' (RingCon.Quotient (RingCon.ker (↑ψ : B →+* T)))
    ((rTensor M (toLinearMap (mkₐ R (RingCon.ker (↑ψ : B →+* T)))) :
        (a : B ⊗[R] M) → (RingCon.ker (↑ψ : B →+* T)).Quotient ⊗[R] M)
      q))
Tactic: rw [quotientKerEquivRangeₐ_comp_mkₐ, comp_toLinearMap,
    rTensor_comp_apply, hpq, ← rTensor_comp_apply, ← comp_toLinearMap,
    ← quotientKerEquivRangeₐ_comp_mkₐ, ← AlgHom.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type v
inst_5 : CommSemiring S
inst_6 : Algebra R S
f : M →ₚₗ[R] N
A : Type u
inst_7 : CommSemiring A
inst_8 : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
B : Type u
inst_9 : CommSemiring B
inst_10 : Algebra R B
q : B ⊗[R] M
ψ : B →ₐ[R] S
h : φ.range ≤ ψ.range
hpq :
  Eq (α := TensorProduct.{u, v, u_1} R (↥ψ.range) M)
    ((rTensor M ((Subalgebra.inclusion h).comp φ.rangeRestrict).toLinearMap : (a : A ⊗[R] M) → ↥ψ.range ⊗[R] M) p :
      TensorProduct.{u, v, u_1} R (↥ψ.range) M)
    ((rTensor M ψ.rangeRestrict.toLinearMap : (a : B ⊗[R] M) → ↥ψ.range ⊗[R] M) q :
      TensorProduct.{u, v, u_1} R (↥ψ.range) M)
⊢ ψ.range.val.comp (Subalgebra.inclusion h) = AlgHom.comp (AlgHom.id R S) φ.range.val
have H : ∀ (x : ↥φ.range),
  Eq (α := S) ((ψ.range.val.comp (Subalgebra.inclusion h) : (a : ↥φ.range) → S) x : S)
    ((AlgHom.comp (AlgHom.id R S) φ.range.val : (a : ↥φ.range) → S) x : S)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type v
inst_5 : CommSemiring S
inst_6 : Algebra R S
f : M →ₚₗ[R] N
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h :
  Eq (α := S ⊗[R] M) (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p))
    (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
⊢ Eq (α := S ⊗[R] N)
    ((rTensor N (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] N) → S ⊗[R] N)
        (f.toFun' (MvPolynomial (Fin s.card) R) p) :
      S ⊗[R] N)
    ((rTensor N (toLinearMap (φ R s')) : (a : MvPolynomial (Fin s'.card) R ⊗[R] N) → S ⊗[R] N)
        (f.toFun' (MvPolynomial (Fin s'.card) R) p') :
      S ⊗[R] N)
have hu : let u : TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R s))) M :=
  (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
      (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
    p;
u =
  (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
      (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
    p
Tactic: set u := rTensor M (φ R s).rangeRestrict.toLinearMap p with hu
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type v
inst_5 : CommSemiring S
inst_6 : Algebra R S
f : M →ₚₗ[R] N
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h :
  Eq (α := S ⊗[R] M) (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p))
    (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
u : TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R s))) M :=
  (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
      (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
    p
hu :
  u =
    (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
        (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
      p
⊢ Subalgebra.FG (AlgHom.range (φ R s))
have rw : Subalgebra.FG (Subalgebra.map (φ R s) ⊤)
Tactic: rw [← Algebra.map_top]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type v
inst_5 : CommSemiring S
inst_6 : Algebra R S
f : M →ₚₗ[R] N
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h :
  Eq (α := S ⊗[R] M) (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p))
    (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
u : TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R s))) M :=
  (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
      (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
    p
hu :
  u =
    (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
        (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
      p
⊢ Eq (α := S ⊗[R] N)
    ((rTensor N (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] N) → S ⊗[R] N)
        (f.toFun' (MvPolynomial (Fin s.card) R) p) :
      S ⊗[R] N)
    ((rTensor N (toLinearMap (φ R s')) : (a : MvPolynomial (Fin s'.card) R ⊗[R] N) → S ⊗[R] N)
        (f.toFun' (MvPolynomial (Fin s'.card) R) p') :
      S ⊗[R] N)
have uFG : Subalgebra.FG (AlgHom.range (φ R s))
Tactic: have uFG : Subalgebra.FG (R := R) (φ R s).range := by
    rw [← Algebra.map_top]
    exact Subalgebra.FG.map _ Algebra.FiniteType.out
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type v
inst_5 : CommSemiring S
inst_6 : Algebra R S
f : M →ₚₗ[R] N
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h :
  Eq (α := S ⊗[R] M) (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p))
    (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
u : TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R s))) M :=
  (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
      (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
    p
hu :
  u =
    (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
        (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
      p
uFG : Subalgebra.FG (AlgHom.range (φ R s))
⊢ Eq (α := S ⊗[R] N)
    ((rTensor N (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] N) → S ⊗[R] N)
        (f.toFun' (MvPolynomial (Fin s.card) R) p) :
      S ⊗[R] N)
    ((rTensor N (toLinearMap (φ R s')) : (a : MvPolynomial (Fin s'.card) R ⊗[R] N) → S ⊗[R] N)
        (f.toFun' (MvPolynomial (Fin s'.card) R) p') :
      S ⊗[R] N)
have hu' : let u' : TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R s'))) M :=
  (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s'))) :
      (a : MvPolynomial (Fin s'.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
    p';
u' =
  (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s'))) :
      (a : MvPolynomial (Fin s'.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
    p'
Tactic: set u' := rTensor M (φ R s').rangeRestrict.toLinearMap p' with hu'
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type v
inst_5 : CommSemiring S
inst_6 : Algebra R S
f : M →ₚₗ[R] N
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h :
  Eq (α := S ⊗[R] M) (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p))
    (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
u : TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R s))) M :=
  (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
      (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
    p
hu :
  u =
    (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
        (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
      p
uFG : Subalgebra.FG (AlgHom.range (φ R s))
u' : TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R s'))) M :=
  (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s'))) :
      (a : MvPolynomial (Fin s'.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
    p'
hu' :
  u' =
    (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s'))) :
        (a : MvPolynomial (Fin s'.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
      p'
⊢ Subalgebra.FG (AlgHom.range (φ R s'))
have rw : Subalgebra.FG (Subalgebra.map (φ R s') ⊤)
Tactic: rw [← Algebra.map_top]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type v
inst_5 : CommSemiring S
inst_6 : Algebra R S
f : M →ₚₗ[R] N
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h :
  Eq (α := S ⊗[R] M) (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p))
    (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
u : TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R s))) M :=
  (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
      (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
    p
hu :
  u =
    (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
        (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
      p
uFG : Subalgebra.FG (AlgHom.range (φ R s))
u' : TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R s'))) M :=
  (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s'))) :
      (a : MvPolynomial (Fin s'.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
    p'
hu' :
  u' =
    (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s'))) :
        (a : MvPolynomial (Fin s'.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
      p'
⊢ Eq (α := S ⊗[R] N)
    ((rTensor N (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] N) → S ⊗[R] N)
        (f.toFun' (MvPolynomial (Fin s.card) R) p) :
      S ⊗[R] N)
    ((rTensor N (toLinearMap (φ R s')) : (a : MvPolynomial (Fin s'.card) R ⊗[R] N) → S ⊗[R] N)
        (f.toFun' (MvPolynomial (Fin s'.card) R) p') :
      S ⊗[R] N)
have u'FG : Subalgebra.FG (AlgHom.range (φ R s'))
Tactic: have u'FG : Subalgebra.FG (R := R) (φ R s').range := by
    rw [← Algebra.map_top]
    exact Subalgebra.FG.map _ Algebra.FiniteType.out