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
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
T : Type w
inst_7 : CommSemiring T
inst_8 : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t
s' : Finset T := Finset.image (⇑h : (a : S) → T) s
h' : AlgHom.{u, v, w} R ↥(AlgHom.range (φ R s)) ↥(AlgHom.range (φ R s')) :=
  AlgHom.codRestrict (h.comp (Subalgebra.val (AlgHom.range (φ R s)))) (AlgHom.range (φ R s')) ⋯
j : Fin s.card → Fin s'.card :=
  Function.comp (β := ↥s') (⇑s'.equivFin : (a : ↥s') → Fin s'.card)
    ((fun (x : ↥s) ↦
        match (motive := ↥s → ↥s') x with
        | ⟨x, hx⟩ => Subtype.mk (p := fun (x : T) ↦ x ∈ s') ((h : (a : S) → T) x) ⋯) ∘
      (⇑s.equivFin.symm : (a : Fin s.card) → ↥s))
eq_h_comp : AlgHom.comp (φ R s') (rename j) = h.comp (φ R s)
p' : MvPolynomial (Fin s'.card) R ⊗[R] M :=
  (rTensor M (toLinearMap (rename j)) : (a : MvPolynomial (Fin s.card) R ⊗[R] M) → MvPolynomial (Fin s'.card) R ⊗[R] M)
    p
ha' :
  Eq (α := T ⊗[R] M) (π R M T (Sigma.mk (β := fun (s : Finset T) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
    ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t)
⊢ Eq (α := T ⊗[R] N) ((rTensor N h.toLinearMap : (a : S ⊗[R] N) → T ⊗[R] N) (toFun S f t) : T ⊗[R] N)
    (toFun T f ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t) : T ⊗[R] N)
have rw : Eq (α := T ⊗[R] N)
  ((rTensor N (h.comp (φ R s)).toLinearMap : (a : MvPolynomial (Fin s.card) R ⊗[R] N) → T ⊗[R] N)
      (f.toFun' (MvPolynomial (Fin s.card) R) p) :
    T ⊗[R] N)
  ((rTensor N (toLinearMap (φ R s')) : (a : MvPolynomial (Fin s'.card) R ⊗[R] N) → T ⊗[R] N)
      (f.toFun' (MvPolynomial (Fin s'.card) R) p') :
    T ⊗[R] N)
Tactic: rw [toFun_eq_rTensor_φ_toFun' f ha, toFun_eq_rTensor_φ_toFun' f ha', ← LinearMap.comp_apply,
    ← rTensor_comp, ← comp_toLinearMap]
-- 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
T : Type w
inst_7 : CommSemiring T
inst_8 : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t
s' : Finset T := Finset.image (⇑h : (a : S) → T) s
h' : AlgHom.{u, v, w} R ↥(AlgHom.range (φ R s)) ↥(AlgHom.range (φ R s')) :=
  AlgHom.codRestrict (h.comp (Subalgebra.val (AlgHom.range (φ R s)))) (AlgHom.range (φ R s')) ⋯
j : Fin s.card → Fin s'.card :=
  Function.comp (β := ↥s') (⇑s'.equivFin : (a : ↥s') → Fin s'.card)
    ((fun (x : ↥s) ↦
        match (motive := ↥s → ↥s') x with
        | ⟨x, hx⟩ => Subtype.mk (p := fun (x : T) ↦ x ∈ s') ((h : (a : S) → T) x) ⋯) ∘
      (⇑s.equivFin.symm : (a : Fin s.card) → ↥s))
eq_h_comp : AlgHom.comp (φ R s') (rename j) = h.comp (φ R s)
p' : MvPolynomial (Fin s'.card) R ⊗[R] M :=
  (rTensor M (toLinearMap (rename j)) : (a : MvPolynomial (Fin s.card) R ⊗[R] M) → MvPolynomial (Fin s'.card) R ⊗[R] M)
    p
ha' :
  Eq (α := T ⊗[R] M) (π R M T (Sigma.mk (β := fun (s : Finset T) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
    ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t)
⊢ Eq (α := T ⊗[R] N)
    ((rTensor N (h.comp (φ R s)).toLinearMap : (a : MvPolynomial (Fin s.card) R ⊗[R] N) → T ⊗[R] N)
        (f.toFun' (MvPolynomial (Fin s.card) R) p) :
      T ⊗[R] N)
    ((rTensor N (toLinearMap (φ R s')) : (a : MvPolynomial (Fin s'.card) R ⊗[R] N) → T ⊗[R] N)
        (f.toFun' (MvPolynomial (Fin s'.card) R) p') :
      T ⊗[R] N)
have hh' : AlgHom.comp (Subalgebra.val (AlgHom.range (φ R s'))) h' = h.comp (Subalgebra.val (AlgHom.range (φ R s)))
Tactic: apply toFun'_eq_of_diagram f p p' h h'
-- 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
T : Type w
inst_7 : CommSemiring T
inst_8 : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t
s' : Finset T := Finset.image (⇑h : (a : S) → T) s
h' : AlgHom.{u, v, w} R ↥(AlgHom.range (φ R s)) ↥(AlgHom.range (φ R s')) :=
  AlgHom.codRestrict (h.comp (Subalgebra.val (AlgHom.range (φ R s)))) (AlgHom.range (φ R s')) ⋯
j : Fin s.card → Fin s'.card :=
  Function.comp (β := ↥s') (⇑s'.equivFin : (a : ↥s') → Fin s'.card)
    ((fun (x : ↥s) ↦
        match (motive := ↥s → ↥s') x with
        | ⟨x, hx⟩ => Subtype.mk (p := fun (x : T) ↦ x ∈ s') ((h : (a : S) → T) x) ⋯) ∘
      (⇑s.equivFin.symm : (a : Fin s.card) → ↥s))
eq_h_comp : AlgHom.comp (φ R s') (rename j) = h.comp (φ R s)
p' : MvPolynomial (Fin s'.card) R ⊗[R] M :=
  (rTensor M (toLinearMap (rename j)) : (a : MvPolynomial (Fin s.card) R ⊗[R] M) → MvPolynomial (Fin s'.card) R ⊗[R] M)
    p
ha' :
  Eq (α := T ⊗[R] M) (π R M T (Sigma.mk (β := fun (s : Finset T) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
    ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t)
hh' : AlgHom.comp (Subalgebra.val (AlgHom.range (φ R s'))) h' = h.comp (Subalgebra.val (AlgHom.range (φ R s)))
⊢ Eq (α := T ⊗[R] N)
    ((rTensor N (h.comp (φ R s)).toLinearMap : (a : MvPolynomial (Fin s.card) R ⊗[R] N) → T ⊗[R] N)
        (f.toFun' (MvPolynomial (Fin s.card) R) p) :
      T ⊗[R] N)
    ((rTensor N (toLinearMap (φ R s')) : (a : MvPolynomial (Fin s'.card) R ⊗[R] N) → T ⊗[R] N)
        (f.toFun' (MvPolynomial (Fin s'.card) R) p') :
      T ⊗[R] N)
have hpq : Eq (α := TensorProduct.{u, w, u_1} R (↥(AlgHom.range (φ R s'))) M)
  ((rTensor M (h'.comp (AlgHom.rangeRestrict (φ R s))).toLinearMap :
        (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
      p :
    TensorProduct.{u, w, 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' :
    TensorProduct.{u, w, u_1} R (↥(AlgHom.range (φ R s'))) M)
Tactic: apply toFun'_eq_of_diagram f p p' h h'
-- 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
T : Type w
inst_7 : CommSemiring T
inst_8 : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t
s' : Finset T := Finset.image (⇑h : (a : S) → T) s
h' : AlgHom.{u, v, w} R ↥(AlgHom.range (φ R s)) ↥(AlgHom.range (φ R s')) :=
  AlgHom.codRestrict (h.comp (Subalgebra.val (AlgHom.range (φ R s)))) (AlgHom.range (φ R s')) ⋯
j : Fin s.card → Fin s'.card :=
  Function.comp (β := ↥s') (⇑s'.equivFin : (a : ↥s') → Fin s'.card)
    ((fun (x : ↥s) ↦
        match (motive := ↥s → ↥s') x with
        | ⟨x, hx⟩ => Subtype.mk (p := fun (x : T) ↦ x ∈ s') ((h : (a : S) → T) x) ⋯) ∘
      (⇑s.equivFin.symm : (a : Fin s.card) → ↥s))
eq_h_comp : AlgHom.comp (φ R s') (rename j) = h.comp (φ R s)
p' : MvPolynomial (Fin s'.card) R ⊗[R] M :=
  (rTensor M (toLinearMap (rename j)) : (a : MvPolynomial (Fin s.card) R ⊗[R] M) → MvPolynomial (Fin s'.card) R ⊗[R] M)
    p
ha' :
  Eq (α := T ⊗[R] M) (π R M T (Sigma.mk (β := fun (s : Finset T) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
    ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t)
⊢ Eq (α := TensorProduct.{u, w, u_1} R (↥(AlgHom.range (φ R s'))) M)
    ((rTensor M (h'.comp (AlgHom.rangeRestrict (φ R s))).toLinearMap :
          (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
        p :
      TensorProduct.{u, w, 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' :
      TensorProduct.{u, w, u_1} R (↥(AlgHom.range (φ R s'))) M)
have hpq : Eq (α := TensorProduct.{u, w, u_1} R (↥(AlgHom.range (φ R s'))) M)
  ((rTensor M (h'.comp (AlgHom.rangeRestrict (φ R s))).toLinearMap :
        (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
      p :
    TensorProduct.{u, w, u_1} R (↥(AlgHom.range (φ R s'))) M)
  ((rTensor M (toLinearMap (AlgHom.comp (AlgHom.rangeRestrict (φ R s')) (rename j))) :
        (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
      p :
    TensorProduct.{u, w, u_1} R (↥(AlgHom.range (φ R s'))) M)
Tactic: simp only [p', ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap]
-- 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
T : Type w
inst_7 : CommSemiring T
inst_8 : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t
s' : Finset T := Finset.image (⇑h : (a : S) → T) s
h' : AlgHom.{u, v, w} R ↥(AlgHom.range (φ R s)) ↥(AlgHom.range (φ R s')) :=
  AlgHom.codRestrict (h.comp (Subalgebra.val (AlgHom.range (φ R s)))) (AlgHom.range (φ R s')) ⋯
j : Fin s.card → Fin s'.card :=
  Function.comp (β := ↥s') (⇑s'.equivFin : (a : ↥s') → Fin s'.card)
    ((fun (x : ↥s) ↦
        match (motive := ↥s → ↥s') x with
        | ⟨x, hx⟩ => Subtype.mk (p := fun (x : T) ↦ x ∈ s') ((h : (a : S) → T) x) ⋯) ∘
      (⇑s.equivFin.symm : (a : Fin s.card) → ↥s))
eq_h_comp : AlgHom.comp (φ R s') (rename j) = h.comp (φ R s)
p' : MvPolynomial (Fin s'.card) R ⊗[R] M :=
  (rTensor M (toLinearMap (rename j)) : (a : MvPolynomial (Fin s.card) R ⊗[R] M) → MvPolynomial (Fin s'.card) R ⊗[R] M)
    p
ha' :
  Eq (α := T ⊗[R] M) (π R M T (Sigma.mk (β := fun (s : Finset T) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
    ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t)
⊢ Eq (α := TensorProduct.{u, w, u_1} R (↥(AlgHom.range (φ R s'))) M)
    ((rTensor M (h'.comp (AlgHom.rangeRestrict (φ R s))).toLinearMap :
          (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
        p :
      TensorProduct.{u, w, u_1} R (↥(AlgHom.range (φ R s'))) M)
    ((rTensor M (toLinearMap (AlgHom.comp (AlgHom.rangeRestrict (φ R s')) (rename j))) :
          (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
        p :
      TensorProduct.{u, w, u_1} R (↥(AlgHom.range (φ R s'))) M)
have hpq : h'.comp (AlgHom.rangeRestrict (φ R s)) = AlgHom.comp (AlgHom.rangeRestrict (φ R s')) (rename j)
Tactic: congr
-- 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
T : Type w
inst_7 : CommSemiring T
inst_8 : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t
s' : Finset T := Finset.image (⇑h : (a : S) → T) s
h' : AlgHom.{u, v, w} R ↥(AlgHom.range (φ R s)) ↥(AlgHom.range (φ R s')) :=
  AlgHom.codRestrict (h.comp (Subalgebra.val (AlgHom.range (φ R s)))) (AlgHom.range (φ R s')) ⋯
j : Fin s.card → Fin s'.card :=
  Function.comp (β := ↥s') (⇑s'.equivFin : (a : ↥s') → Fin s'.card)
    ((fun (x : ↥s) ↦
        match (motive := ↥s → ↥s') x with
        | ⟨x, hx⟩ => Subtype.mk (p := fun (x : T) ↦ x ∈ s') ((h : (a : S) → T) x) ⋯) ∘
      (⇑s.equivFin.symm : (a : Fin s.card) → ↥s))
eq_h_comp : AlgHom.comp (φ R s') (rename j) = h.comp (φ R s)
p' : MvPolynomial (Fin s'.card) R ⊗[R] M :=
  (rTensor M (toLinearMap (rename j)) : (a : MvPolynomial (Fin s.card) R ⊗[R] M) → MvPolynomial (Fin s'.card) R ⊗[R] M)
    p
ha' :
  Eq (α := T ⊗[R] M) (π R M T (Sigma.mk (β := fun (s : Finset T) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
    ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t)
⊢ h'.comp (AlgHom.rangeRestrict (φ R s)) = AlgHom.comp (AlgHom.rangeRestrict (φ R s')) (rename j)
have hpq : ∀ (n : Fin s.card),
  Eq.{w + 1} (α := T)
    (↑((h'.comp (AlgHom.rangeRestrict (φ R s)) : (a : MvPolynomial (Fin s.card) R) → ↥(φ R s').range) (X n)) : T)
    (↑(((AlgHom.comp (AlgHom.rangeRestrict (φ R s')) (rename j) :
              AlgHom.{u, u, w} R (MvPolynomial (Fin s.card) R) ↥(AlgHom.range (φ R s'))) :
            (a : MvPolynomial (Fin s.card) R) → ↥(φ R s').range)
          (X n)) :
      T)
Tactic: ext n
-- 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
T : Type w
inst_7 : CommSemiring T
inst_8 : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t
s' : Finset T := Finset.image (⇑h : (a : S) → T) s
h' : AlgHom.{u, v, w} R ↥(AlgHom.range (φ R s)) ↥(AlgHom.range (φ R s')) :=
  AlgHom.codRestrict (h.comp (Subalgebra.val (AlgHom.range (φ R s)))) (AlgHom.range (φ R s')) ⋯
j : Fin s.card → Fin s'.card :=
  Function.comp (β := ↥s') (⇑s'.equivFin : (a : ↥s') → Fin s'.card)
    ((fun (x : ↥s) ↦
        match (motive := ↥s → ↥s') x with
        | ⟨x, hx⟩ => Subtype.mk (p := fun (x : T) ↦ x ∈ s') ((h : (a : S) → T) x) ⋯) ∘
      (⇑s.equivFin.symm : (a : Fin s.card) → ↥s))
eq_h_comp : AlgHom.comp (φ R s') (rename j) = h.comp (φ R s)
p' : MvPolynomial (Fin s'.card) R ⊗[R] M :=
  (rTensor M (toLinearMap (rename j)) : (a : MvPolynomial (Fin s.card) R ⊗[R] M) → MvPolynomial (Fin s'.card) R ⊗[R] M)
    p
ha' :
  Eq (α := T ⊗[R] M) (π R M T (Sigma.mk (β := fun (s : Finset T) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
    ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t)
n : Fin s.card
⊢ Eq.{w + 1} (α := T)
    (↑((h'.comp (AlgHom.rangeRestrict (φ R s)) : (a : MvPolynomial (Fin s.card) R) → ↥(φ R s').range) (X n)) : T)
    (↑(((AlgHom.comp (AlgHom.rangeRestrict (φ R s')) (rename j) :
              AlgHom.{u, u, w} R (MvPolynomial (Fin s.card) R) ↥(AlgHom.range (φ R s'))) :
            (a : MvPolynomial (Fin s.card) R) → ↥(φ R s').range)
          (X n)) :
      T)
have hpq : Eq.{w + 1} (α := T) ((h : (a : S) → T) ((φ R s : (a : MvPolynomial (Fin s.card) R) → S) (X n) : S) : T)
  ((φ R s' : (a : MvPolynomial (Fin s'.card) R) → T)
      (X
          ((s'.equivFin : (a : ↥s') → Fin s'.card)
            (Subtype.mk (p := fun (x : T) ↦ x ∈ s')
              ((h : (a : S) → T) (↑((s.equivFin.symm : (a : Fin s.card) → ↥s) n) : S)) sorry)) :
        MvPolynomial (Fin s'.card) R) :
    T)
Tactic: simp only [AlgHom.coe_comp, Function.comp_apply, coe_codRestrict,
      Subalgebra.coe_val, rename_X, h', j]
-- 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
T : Type w
inst_7 : CommSemiring T
inst_8 : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
⊢ Eq (α := T ⊗[R] N) ((rTensor N h.toLinearMap : (a : S ⊗[R] N) → T ⊗[R] N) (toFun S f t) : T ⊗[R] N)
    (toFun T f ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t) : T ⊗[R] N)
have obtain : ∀ (s : Finset S) (p : MvPolynomial (Fin s.card) R ⊗[R] M)
  (ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t),
  Eq (α := T ⊗[R] N) ((rTensor N h.toLinearMap : (a : S ⊗[R] N) → T ⊗[R] N) (toFun S f t) : T ⊗[R] N)
    (toFun T f ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t) : T ⊗[R] N)
Tactic: classical
  obtain ⟨⟨s, p⟩, ha⟩ := π_surjective t
  let s' := s.image h
  let h' : (φ R s).range →ₐ[R] (φ R s').range :=
    (h.comp (Subalgebra.val _)).codRestrict (φ R s').range (by
    rintro ⟨x, hx⟩
    simp only [range_φ] at hx ⊢
    simp only [AlgHom.coe_comp, Subalgebra.coe_val, Function.comp_apply, Finset.coe_image,
      Algebra.adjoin_image, s']
    exact ⟨x, hx, rfl⟩)
  let j : Fin s.card → Fin s'.card :=
    (s'.equivFin) ∘ (fun ⟨x, hx⟩ ↦ ⟨h x, Finset.mem_image_of_mem h hx⟩) ∘ (s.equivFin).symm
  have eq_h_comp : (φ R s').comp (rename j) = h.comp (φ R s) := by
    ext p
    simp only [φ, AlgHom.comp_apply, aeval_rename, comp_aeval]
    congr
    ext n
    simp only [Function.comp_apply, Equiv.symm_apply_apply, j]
  let p' := rTensor M (rename j).toLinearMap p
  have ha' : π R M T (⟨s', p'⟩ : lifts R M T) = rTensor M h.toLinearMap t := by
    simp only [← ha, π, p', ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap, eq_h_comp]
  rw [toFun_eq_rTensor_φ_toFun' f ha, toFun_eq_rTensor_φ_toFun' f ha', ← LinearMap.comp_apply,
    ← rTensor_comp, ← comp_toLinearMap]
  apply toFun'_eq_of_diagram f p p' h h'
  · simp only [val_comp_codRestrict, h']
  · simp only [p', ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap]
    congr
    ext n
    simp only [AlgHom.coe_comp, Function.comp_apply, coe_codRestrict,
      Subalgebra.coe_val, rename_X, h', j]
    simp only [φ, aeval_X, Equiv.symm_apply_apply]
-- 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
T : Type w
inst_7 : CommSemiring T
inst_8 : Algebra R T
h : S →ₐ[R] T
⊢ Eq (α := S ⊗[R] M → T ⊗[R] N) ((⇑(rTensor N h.toLinearMap) : (a : S ⊗[R] N) → T ⊗[R] N) ∘ toFun S f)
    (toFun T f ∘ (⇑(rTensor M h.toLinearMap) : (a : S ⊗[R] M) → T ⊗[R] M))
have h₁ : ∀ (t : S ⊗[R] M),
  Eq (α := T ⊗[R] N) (((⇑(rTensor N h.toLinearMap) : (a : S ⊗[R] N) → T ⊗[R] N) ∘ toFun S f) t)
    ((toFun T f ∘ (⇑(rTensor M h.toLinearMap) : (a : S ⊗[R] M) → T ⊗[R] M)) t)
Tactic: ext t
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type u_5
inst_5 : CommSemiring S
inst_6 : Algebra R S
⊢ Eq (α := S ⊗[R] M → S ⊗[R] N) (toFun S 0) 0
have h : ∀ (t : S ⊗[R] M), Eq (α := S ⊗[R] N) (toFun S 0 t) (0 t)
Tactic: ext t
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type u_5
inst_5 : CommSemiring S
inst_6 : Algebra R S
t : S ⊗[R] M
⊢ Eq (α := S ⊗[R] N) (toFun S 0 t) (0 t)
have h : ∀ (s : Finset S) (p : MvPolynomial (Fin s.card) R ⊗[R] M)
  (ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t),
  Eq (α := S ⊗[R] N) (toFun S 0 t) (0 t)
Tactic: obtain ⟨⟨s, p⟩, ha⟩ := π_surjective t
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
f g : M →ₚₗ[R] N
S : Type u_5
inst_5 : CommSemiring S
inst_6 : Algebra R S
t : S ⊗[R] M
⊢ toFun S (f + g) t = toFun S f t + toFun S g t
have obtain : ∀ (s : Finset S) (p : MvPolynomial (Fin s.card) R ⊗[R] M)
  (ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t),
  toFun S (f + g) t = toFun S f t + toFun S g t
Tactic: obtain ⟨⟨s, p⟩, ha⟩ := π_surjective t
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
f g : M →ₚₗ[R] N
S : Type u_5
inst_5 : CommSemiring S
inst_6 : Algebra R S
⊢ toFun S (f + g) = HAdd.hAdd (α := S ⊗[R] M → S ⊗[R] N) (toFun S f) (toFun S g)
have h : ∀ (t : S ⊗[R] M),
  toFun S (f + g) t = HAdd.hAdd (α := S ⊗[R] M → S ⊗[R] N) (β := S ⊗[R] M → S ⊗[R] N) (toFun S f) (toFun S g) t
Tactic: ext t
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommRing R
M : Type u_6
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_7
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u_8
inst_5 : CommSemiring S
inst_6 : Algebra R S
⊢ toFun S (-f) = HSMul.hSMul (α := R) (β := S ⊗[R] M → S ⊗[R] N) (-1) (toFun S f)
have h : ∀ (t : S ⊗[R] M), toFun S (-f) t = HSMul.hSMul (α := R) (β := S ⊗[R] M → S ⊗[R] N) (-1) (toFun S f) t
Tactic: ext t
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommRing R
M : Type u_6
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_7
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u_8
inst_5 : CommSemiring S
inst_6 : Algebra R S
t : S ⊗[R] M
⊢ toFun S (-f) t = HSMul.hSMul (α := R) (β := S ⊗[R] M → S ⊗[R] N) (-1) (toFun S f) t
have h : ∀ (s : Finset S) (p : MvPolynomial (Fin s.card) R ⊗[R] M)
  (ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t),
  toFun S (-f) t = HSMul.hSMul (α := R) (β := S ⊗[R] M → S ⊗[R] N) (-1) (toFun S f) t
Tactic: obtain ⟨⟨s, p⟩, ha⟩ := π_surjective t
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
r : R
f : M →ₚₗ[R] N
S : Type u_5
inst_5 : CommSemiring S
inst_6 : Algebra R S
⊢ toFun S (r • f) = HSMul.hSMul (β := S ⊗[R] M → S ⊗[R] N) r (toFun S f)
have h : ∀ (t : S ⊗[R] M), toFun S (r • f) t = HSMul.hSMul (β := S ⊗[R] M → S ⊗[R] N) r (toFun S f) t
Tactic: ext t
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
r : R
f : M →ₚₗ[R] N
S : Type u_5
inst_5 : CommSemiring S
inst_6 : Algebra R S
t : S ⊗[R] M
⊢ toFun S (r • f) t = HSMul.hSMul (β := S ⊗[R] M → S ⊗[R] N) r (toFun S f) t
have h : ∀ (s : Finset S) (p : MvPolynomial (Fin s.card) R ⊗[R] M)
  (ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t),
  toFun S (r • f) t = HSMul.hSMul (β := S ⊗[R] M → S ⊗[R] N) r (toFun S f) t
Tactic: obtain ⟨⟨s, p⟩, ha⟩ := π_surjective t
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u_5
inst_5 : CommSemiring S
inst_6 : Algebra R S
x : M
⊢ Eq (α := S ⊗[R] N) (1 ⊗ₜ[R] f.ground x) (toFun S f (1 ⊗ₜ[R] x))
have simp : Eq (α := S ⊗[R] N)
  (1 ⊗ₜ[R]
    Function.comp (β := R ⊗[R] N) (⇑(TensorProduct.lid R N) : (a : R ⊗[R] N) → N)
      (toFun R f ∘ (⇑(LinearEquiv.symm (TensorProduct.lid R M)) : (a : M) → R ⊗[R] M)) x)
  (toFun S f (1 ⊗ₜ[R] x))
Tactic: simp only [ground, toFun'_eq_toFun]