awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
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'
u'FG : Subalgebra.FG (AlgHom.range (φ R s'))
huu' :
  Eq (α := S ⊗[R] M)
    ((rTensor M (toLinearMap (Subalgebra.val (AlgHom.range (φ R s)))) : (a : ↥(φ R s).range ⊗[R] M) → S ⊗[R] M) u :
      S ⊗[R] M)
    ((rTensor M (toLinearMap (Subalgebra.val (AlgHom.range (φ R s')))) : (a : ↥(φ R s').range ⊗[R] M) → S ⊗[R] M) u' :
      S ⊗[R] M)
obtain :
  ∀ (B : Subalgebra R S) (hAB : AlgHom.range (φ R s) ≤ B) (hA'B : AlgHom.range (φ R s') ≤ B)
    (h :
      Eq (α := TensorProduct.{u, v, u_1} R (↥B) M)
        ((rTensor M (Subalgebra.inclusion hAB).toLinearMap : (a : ↥(φ R s).range ⊗[R] M) → ↥B ⊗[R] M) u :
          TensorProduct.{u, v, u_1} R (↥B) M)
        ((rTensor M (Subalgebra.inclusion hA'B).toLinearMap : (a : ↥(φ R s').range ⊗[R] M) → ↥B ⊗[R] M) u' :
          TensorProduct.{u, v, u_1} R (↥B) M))
    (t : Finset S) (hB : Algebra.adjoin R (↑t : Set S) = B),
    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)
⊢ 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)

Tactic:
obtain ⟨B, hAB, hA'B, ⟨t, hB⟩, h⟩ :=
    TensorProduct.Algebra.eq_of_fg_of_subtype_eq' (R := R) uFG u'FG huu'

Premises used: TensorProduct.Algebra.eq_of_fg_of_subtype_eq'
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
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_1 :
  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'
u'FG : Subalgebra.FG (AlgHom.range (φ R s'))
huu' :
  Eq (α := S ⊗[R] M)
    ((rTensor M (toLinearMap (Subalgebra.val (AlgHom.range (φ R s)))) : (a : ↥(φ R s).range ⊗[R] M) → S ⊗[R] M) u :
      S ⊗[R] M)
    ((rTensor M (toLinearMap (Subalgebra.val (AlgHom.range (φ R s')))) : (a : ↥(φ R s').range ⊗[R] M) → S ⊗[R] M) u' :
      S ⊗[R] M)
B : Subalgebra R S
hAB : AlgHom.range (φ R s) ≤ B
hA'B : AlgHom.range (φ R s') ≤ B
h :
  Eq (α := TensorProduct.{u, v, u_1} R (↥B) M)
    ((rTensor M (Subalgebra.inclusion hAB).toLinearMap : (a : ↥(φ R s).range ⊗[R] M) → ↥B ⊗[R] M) u :
      TensorProduct.{u, v, u_1} R (↥B) M)
    ((rTensor M (Subalgebra.inclusion hA'B).toLinearMap : (a : ↥(φ R s').range ⊗[R] M) → ↥B ⊗[R] M) u' :
      TensorProduct.{u, v, u_1} R (↥B) M)
t : Finset S
hB : Algebra.adjoin R (↑t : Set S) = B
⊢ B = AlgHom.range (φ R t)

Tactic:
rw [← range_φ R t, eq_comm] at hB

Premises used: eq_comm, PolynomialLaw.range_φ
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
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_1 :
  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'
u'FG : Subalgebra.FG (AlgHom.range (φ R s'))
huu' :
  Eq (α := S ⊗[R] M)
    ((rTensor M (toLinearMap (Subalgebra.val (AlgHom.range (φ R s)))) : (a : ↥(φ R s).range ⊗[R] M) → S ⊗[R] M) u :
      S ⊗[R] M)
    ((rTensor M (toLinearMap (Subalgebra.val (AlgHom.range (φ R s')))) : (a : ↥(φ R s').range ⊗[R] M) → S ⊗[R] M) u' :
      S ⊗[R] M)
B : Subalgebra R S
hAB : AlgHom.range (φ R s) ≤ B
hA'B : AlgHom.range (φ R s') ≤ B
h :
  Eq (α := TensorProduct.{u, v, u_1} R (↥B) M)
    ((rTensor M (Subalgebra.inclusion hAB).toLinearMap : (a : ↥(φ R s).range ⊗[R] M) → ↥B ⊗[R] M) u :
      TensorProduct.{u, v, u_1} R (↥B) M)
    ((rTensor M (Subalgebra.inclusion hA'B).toLinearMap : (a : ↥(φ R s').range ⊗[R] M) → ↥B ⊗[R] M) u' :
      TensorProduct.{u, v, u_1} R (↥B) M)
t : Finset S
hB : B = AlgHom.range (φ R t)
⊢ LE.le (α := Subalgebra R S) (AlgHom.range (φ R s)) (AlgHom.range (φ R t))

Tactic:
have hAB' : (φ R s).range ≤ (φ R t).range := le_trans hAB (le_of_eq hB)
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
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_1 :
  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'
u'FG : Subalgebra.FG (AlgHom.range (φ R s'))
huu' :
  Eq (α := S ⊗[R] M)
    ((rTensor M (toLinearMap (Subalgebra.val (AlgHom.range (φ R s)))) : (a : ↥(φ R s).range ⊗[R] M) → S ⊗[R] M) u :
      S ⊗[R] M)
    ((rTensor M (toLinearMap (Subalgebra.val (AlgHom.range (φ R s')))) : (a : ↥(φ R s').range ⊗[R] M) → S ⊗[R] M) u' :
      S ⊗[R] M)
B : Subalgebra R S
hAB : AlgHom.range (φ R s) ≤ B
hA'B : AlgHom.range (φ R s') ≤ B
h :
  Eq (α := TensorProduct.{u, v, u_1} R (↥B) M)
    ((rTensor M (Subalgebra.inclusion hAB).toLinearMap : (a : ↥(φ R s).range ⊗[R] M) → ↥B ⊗[R] M) u :
      TensorProduct.{u, v, u_1} R (↥B) M)
    ((rTensor M (Subalgebra.inclusion hA'B).toLinearMap : (a : ↥(φ R s').range ⊗[R] M) → ↥B ⊗[R] M) u' :
      TensorProduct.{u, v, u_1} R (↥B) M)
t : Finset S
hB : B = AlgHom.range (φ R t)
hAB' : LE.le (α := Subalgebra R S) (AlgHom.range (φ R s)) (AlgHom.range (φ R t))
⊢ LE.le (α := Subalgebra R S) (AlgHom.range (φ R s')) (AlgHom.range (φ R t))

Tactic:
have hA'B' : (φ R s').range ≤ (φ R t).range := le_trans hA'B (le_of_eq hB)
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
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_1 :
  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'
u'FG : Subalgebra.FG (AlgHom.range (φ R s'))
huu' :
  Eq (α := S ⊗[R] M)
    ((rTensor M (toLinearMap (Subalgebra.val (AlgHom.range (φ R s)))) : (a : ↥(φ R s).range ⊗[R] M) → S ⊗[R] M) u :
      S ⊗[R] M)
    ((rTensor M (toLinearMap (Subalgebra.val (AlgHom.range (φ R s')))) : (a : ↥(φ R s').range ⊗[R] M) → S ⊗[R] M) u' :
      S ⊗[R] M)
B : Subalgebra R S
hAB : AlgHom.range (φ R s) ≤ B
hA'B : AlgHom.range (φ R s') ≤ B
h :
  Eq (α := TensorProduct.{u, v, u_1} R (↥B) M)
    ((rTensor M (Subalgebra.inclusion hAB).toLinearMap : (a : ↥(φ R s).range ⊗[R] M) → ↥B ⊗[R] M) u :
      TensorProduct.{u, v, u_1} R (↥B) M)
    ((rTensor M (Subalgebra.inclusion hA'B).toLinearMap : (a : ↥(φ R s').range ⊗[R] M) → ↥B ⊗[R] M) u' :
      TensorProduct.{u, v, u_1} R (↥B) M)
t : Finset S
hB : B = AlgHom.range (φ R t)
hAB' : LE.le (α := Subalgebra R S) (AlgHom.range (φ R s)) (AlgHom.range (φ R t))
hA'B' : LE.le (α := Subalgebra R S) (AlgHom.range (φ R s')) (AlgHom.range (φ R t))
⊢ ∃ (q : MvPolynomial (Fin t.card) R ⊗[R] M),
    Eq (α := TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R t))) M)
      ((rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R t))) :
            (a : MvPolynomial (Fin t.card) R ⊗[R] M) → ↥(φ R t).range ⊗[R] M)
          q :
        TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R t))) M)
      ((rTensor M ((Subalgebra.inclusion ⋯).comp (Subalgebra.inclusion hAB)).toLinearMap :
            (a : ↥(φ R s).range ⊗[R] M) → ↥(φ R t).range ⊗[R] M)
          u :
        TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R t))) M)

Tactic:
have : ∃ q : MvPolynomial (Fin t.card) R ⊗[R] M, rTensor M (toLinearMap (φ R t).rangeRestrict) q =
      rTensor M ((Subalgebra.inclusion (le_of_eq hB)).comp
        (Subalgebra.inclusion hAB)).toLinearMap u :=
    rTensor_surjective _ (rangeRestrict_surjective _) _
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
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 : 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
rw :
  Eq (α := S ⊗[R] N) (Function.extend (π R M S) (toFunLifted S f) (fun (x : S ⊗[R] M) ↦ 0) t)
    ((rTensor N (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] N) → S ⊗[R] N)
      (f.toFun' (MvPolynomial (Fin s.card) R) p))
rw₁ :
  Eq (α := S ⊗[R] N)
    (Function.extend (π R M S) (toFunLifted S f) (fun (x : S ⊗[R] M) ↦ 0)
      (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p)))
    ((rTensor N (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] N) → S ⊗[R] N)
      (f.toFun' (MvPolynomial (Fin s.card) R) p))
rw₂ :
  Eq (α := S ⊗[R] N) (toFunLifted S f (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p))
    ((rTensor N (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] N) → S ⊗[R] N)
      (f.toFun' (MvPolynomial (Fin s.card) R) p))
rw₃ rw₄ :
  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)
⊢ toFun S f t =
    (rTensor N (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] N) → S ⊗[R] N)
      (f.toFun' (MvPolynomial (Fin s.card) R) p)

Tactic:
rw [PolynomialLaw.toFun, ← ha, (factorsThrough_toFunLifted_π f).extend_apply, toFunLifted]

Premises used: PolynomialLaw.factorsThrough_toFunLifted_π, Function.FactorsThrough.extend_apply, PolynomialLaw.toFun, PolynomialLaw.toFunLifted
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
T : Type u_3
inst_5 : CommSemiring T
inst_6 : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
ht : Membership.mem (γ := Submodule R (T ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t
obtain :
  ∀ (u : TensorProduct.{u, u_3, u_1} R (↥A) M) (hu : (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → T ⊗[R] M) u = t),
    ∃ (s : S ⊗[R] M), (rTensor M φ.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) s = t
⊢ ∃ (s : S ⊗[R] M), (rTensor M φ.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) s = t

Tactic:
obtain ⟨u, hu⟩ := ht
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
T : Type u_3
inst_5 : CommSemiring T
inst_6 : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
u : TensorProduct.{u, u_3, u_1} R (↥A) M
hu : (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → T ⊗[R] M) u = t
h_surj :
  Function.Surjective (α := S ⊗[R] M) (β := TensorProduct.{u, u_3, u_1} R (↥φ.range) M)
    (⇑(rTensor M φ.rangeRestrict.toLinearMap) : (a : S ⊗[R] M) → ↥φ.range ⊗[R] M)
obtain :
  ∀ (p : S ⊗[R] M)
    (hp :
      Eq (α := TensorProduct.{u, u_3, u_1} R (↥φ.range) M)
        ((rTensor M φ.rangeRestrict.toLinearMap : (a : S ⊗[R] M) → ↥φ.range ⊗[R] M) p :
          TensorProduct.{u, u_3, u_1} R (↥φ.range) M)
        ((rTensor M (Subalgebra.inclusion hφ).toLinearMap : (a : ↥A ⊗[R] M) → ↥φ.range ⊗[R] M) u :
          TensorProduct.{u, u_3, u_1} R (↥φ.range) M)),
    ∃ (s : S ⊗[R] M), (rTensor M φ.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) s = t
⊢ ∃ (s : S ⊗[R] M), (rTensor M φ.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) s = t

Tactic:
obtain ⟨p, hp⟩ := h_surj ((Subalgebra.inclusion hφ).toLinearMap.rTensor M u)

Premises used: AlgHom.toLinearMap, Subalgebra.inclusion, DFunLike.coe, LinearMap.rTensor
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
T : Type u_3
inst_5 : CommSemiring T
inst_6 : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
u : TensorProduct.{u, u_3, u_1} R (↥A) M
hu : (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → T ⊗[R] M) u = t
h_surj :
  Function.Surjective (α := S ⊗[R] M) (β := TensorProduct.{u, u_3, u_1} R (↥φ.range) M)
    (⇑(rTensor M φ.rangeRestrict.toLinearMap) : (a : S ⊗[R] M) → ↥φ.range ⊗[R] M)
p : S ⊗[R] M
hp :
  Eq (α := TensorProduct.{u, u_3, u_1} R (↥φ.range) M)
    ((rTensor M φ.rangeRestrict.toLinearMap : (a : S ⊗[R] M) → ↥φ.range ⊗[R] M) p :
      TensorProduct.{u, u_3, u_1} R (↥φ.range) M)
    ((rTensor M (Subalgebra.inclusion hφ).toLinearMap : (a : ↥A ⊗[R] M) → ↥φ.range ⊗[R] M) u :
      TensorProduct.{u, u_3, u_1} R (↥φ.range) M)
h : (rTensor M φ.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) p = t
⊢ ∃ (s : S ⊗[R] M), (rTensor M φ.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) s = t

Tactic:
use p
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
T : Type u_3
inst_5 : CommSemiring T
inst_6 : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
u : TensorProduct.{u, u_3, u_1} R (↥A) M
hu : (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → T ⊗[R] M) u = t
h_surj :
  Function.Surjective (α := S ⊗[R] M) (β := TensorProduct.{u, u_3, u_1} R (↥φ.range) M)
    (⇑(rTensor M φ.rangeRestrict.toLinearMap) : (a : S ⊗[R] M) → ↥φ.range ⊗[R] M)
p : S ⊗[R] M
hp :
  Eq (α := TensorProduct.{u, u_3, u_1} R (↥φ.range) M)
    ((rTensor M φ.rangeRestrict.toLinearMap : (a : S ⊗[R] M) → ↥φ.range ⊗[R] M) p :
      TensorProduct.{u, u_3, u_1} R (↥φ.range) M)
    ((rTensor M (Subalgebra.inclusion hφ).toLinearMap : (a : ↥A ⊗[R] M) → ↥φ.range ⊗[R] M) u :
      TensorProduct.{u, u_3, u_1} R (↥φ.range) M)
h :
  Eq (α := T ⊗[R] M) ((rTensor M φ.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) p : T ⊗[R] M)
    ((rTensor M (φ.range.val.comp φ.rangeRestrict).toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) p : T ⊗[R] M)
⊢ (rTensor M φ.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) p = t

Tactic:
rw [← hu, ← Subalgebra.val_comp_inclusion hφ, comp_toLinearMap, rTensor_comp,
      LinearMap.comp_apply, ← hp, ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap]

Premises used: AlgHom.comp_toLinearMap, LinearMap.comp_apply, LinearMap.rTensor_comp, Subalgebra.val_comp_inclusion
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
T : Type u_3
inst_5 : CommSemiring T
inst_6 : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
u : TensorProduct.{u, u_3, u_1} R (↥A) M
hu : (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → T ⊗[R] M) u = t
h_surj :
  Function.Surjective (α := S ⊗[R] M) (β := TensorProduct.{u, u_3, u_1} R (↥φ.range) M)
    (⇑(rTensor M φ.rangeRestrict.toLinearMap) : (a : S ⊗[R] M) → ↥φ.range ⊗[R] M)
p : S ⊗[R] M
hp :
  Eq (α := TensorProduct.{u, u_3, u_1} R (↥φ.range) M)
    ((rTensor M φ.rangeRestrict.toLinearMap : (a : S ⊗[R] M) → ↥φ.range ⊗[R] M) p :
      TensorProduct.{u, u_3, u_1} R (↥φ.range) M)
    ((rTensor M (Subalgebra.inclusion hφ).toLinearMap : (a : ↥A ⊗[R] M) → ↥φ.range ⊗[R] M) u :
      TensorProduct.{u, u_3, u_1} R (↥φ.range) M)
⊢ Eq (α := T ⊗[R] M) ((rTensor M φ.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) p : T ⊗[R] M)
    ((rTensor M (φ.range.val.comp φ.rangeRestrict).toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) p : T ⊗[R] M)

Tactic:
simp
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
T : Type u_3
inst_5 : CommSemiring T
inst_6 : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
u : TensorProduct.{u, u_3, u_1} R (↥A) M
hu : (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → T ⊗[R] M) u = t
suffices :
  Function.Surjective (α := S ⊗[R] M) (β := TensorProduct.{u, u_3, u_1} R (↥φ.range) M)
    (⇑(rTensor M φ.rangeRestrict.toLinearMap) : (a : S ⊗[R] M) → ↥φ.range ⊗[R] M)
⊢ ∃ (s : S ⊗[R] M), (rTensor M φ.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) s = t

Tactic:
suffices h_surj : Function.Surjective ((φ.rangeRestrict.toLinearMap).rTensor M) by
    obtain ⟨p, hp⟩ := h_surj ((Subalgebra.inclusion hφ).toLinearMap.rTensor M u)
    use p
    rw [← hu, ← Subalgebra.val_comp_inclusion hφ, comp_toLinearMap, rTensor_comp,
      LinearMap.comp_apply, ← hp, ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap]
    simp
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
T : Type u_3
inst_5 : CommSemiring T
inst_6 : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
u : TensorProduct.{u, u_3, u_1} R (↥A) M
hu : (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → T ⊗[R] M) u = t
⊢ Function.Surjective (α := S ⊗[R] M) (β := TensorProduct.{u, u_3, u_1} R (↥φ.range) M)
    (⇑(rTensor M φ.rangeRestrict.toLinearMap) : (a : S ⊗[R] M) → ↥φ.range ⊗[R] M)

Tactic:
rTensor_surjective M (rangeRestrict_surjective φ)

Premises used: AlgHom.rangeRestrict_surjective, LinearMap.rTensor_surjective
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
T : Type u_3
inst_5 : CommSemiring T
inst_6 : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
u : TensorProduct.{u, u_3, u_1} R (↥A) M
hu : (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → T ⊗[R] M) u = t
⊢ Function.Surjective (α := S ⊗[R] M) (β := TensorProduct.{u, u_3, u_1} R (↥φ.range) M)
    (⇑(rTensor M φ.rangeRestrict.toLinearMap) : (a : S ⊗[R] M) → ↥φ.range ⊗[R] M)

Tactic:
exact rTensor_surjective M (rangeRestrict_surjective φ)

Premises used: LinearMap.rTensor_surjective
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
t : S ⊗[R] M
obtain :
  ∀ (B : Subalgebra R S) (hB : B.FG)
    (ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M B.val.toLinearMap)) t),
    ∃ (a : lifts R M S), π R M S a = t
⊢ ∃ (a : lifts R M S), π R M S a = t

Tactic:
obtain ⟨B : Subalgebra R S, hB : B.FG, ht : t ∈ range _⟩ := TensorProduct.Algebra.exists_of_fg t

Premises used: TensorProduct.Algebra.exists_of_fg, LinearMap.range, Subalgebra