awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommRing R
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommGroup N
inst_4 : Module R N
f_1 f : M →ₚₗ[R] N
S : Type u
x : CommSemiring S
x_1 : Algebra R S
m : S ⊗[R] M
toFun' : HSMul.hSMul (α := R) (-1) (f.toFun' S m) + HSMul.hSMul (α := R) 1 (f.toFun' S m) = 0
⊢ HSMul.hSMul (α := R) (-1) (f.toFun' S m) + f.toFun' S m = 0

Tactic:
nth_rewrite 2 [← _root_.one_smul (M := R) (b := f.toFun' S m)]

Premises used: one_smul, PolynomialLaw.toFun'
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommRing R
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommGroup N
inst_4 : Module R N
f_1 f : M →ₚₗ[R] N
S : Type u
x : CommSemiring S
x_1 : Algebra R S
m : S ⊗[R] M
toFun' : HAdd.hAdd (α := R) (-1) 1 • f.toFun' S m = 0
⊢ HSMul.hSMul (α := R) (-1) (f.toFun' S m) + HSMul.hSMul (α := R) 1 (f.toFun' S m) = 0

Tactic:
rw [← _root_.add_smul]

Premises used: add_smul
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommRing R
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommGroup N
inst_4 : Module R N
f_1 f : M →ₚₗ[R] N
S : Type u
x : CommSemiring S
x_1 : Algebra R S
m : S ⊗[R] M
⊢ HAdd.hAdd (α := R) (-1) 1 • f.toFun' S m = 0

Tactic:
simp only [neg_add_cancel, _root_.zero_smul]

Premises used: zero_smul, neg_add_cancel
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommRing R
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommGroup N
inst_4 : Module R N
f_1 f g : M →ₚₗ[R] N
toFun' :
  ∀ (x : Type u) (x_1 : CommSemiring x) (x_2 : Algebra R x) (x_3 : x ⊗[R] M),
    (f + g).toFun' x x_3 = (g + f).toFun' x x_3
⊢ f + g = g + f

Tactic:
ext
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommRing R
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommGroup N
inst_4 : Module R N
f_1 f g : M →ₚₗ[R] N
x : Type u
x_1 : CommSemiring x
x_2 : Algebra R x
x_3 : x ⊗[R] M
⊢ (f + g).toFun' x x_3 = (g + f).toFun' x x_3

Tactic:
simp only [add_def, add_comm]

Premises used: add_comm, PolynomialLaw.add_def
-- 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
f : M →ₚₗ[R] N
m : M
⊢ f.ground m = (TensorProduct.lid R N : (a : R ⊗[R] N) → N) (f.toFun' R (1 ⊗ₜ[R] m))

Tactic:
rfl

Premises used: PolynomialLaw.ground, TensorProduct.tmul, AddCon.toQuotient, rfl
-- 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
f : M →ₚₗ[R] N
S : Type u
inst_5 : CommSemiring S
inst_6 : Algebra R S
x : M
rw :
  Eq (α := S ⊗[R] N) (1 ⊗ₜ[R] (TensorProduct.lid R N : (a : R ⊗[R] N) → N) (f.toFun' R (1 ⊗ₜ[R] x)) : S ⊗[R] N)
    (f.toFun' S (1 ⊗ₜ[R] x) : S ⊗[R] N)
⊢ Eq (α := S ⊗[R] N) (1 ⊗ₜ[R] f.ground x) (f.toFun' S (1 ⊗ₜ[R] x))

Tactic:
rw [ground_apply]

Premises used: PolynomialLaw.ground_apply
-- 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
f : M →ₚₗ[R] N
S : Type u
inst_5 : CommSemiring S
inst_6 : Algebra R S
x : M
⊢ Eq (α := S ⊗[R] N)
    ((rTensor N (toLinearMap (Algebra.algHom R R S)) : (a : R ⊗[R] N) → S ⊗[R] N) (f.toFun' R (1 ⊗ₜ[R] x)) : S ⊗[R] N)
    (f.toFun' S ((rTensor M (toLinearMap (Algebra.algHom R R S)) : (a : R ⊗[R] M) → S ⊗[R] M) (1 ⊗ₜ[R] x)) : S ⊗[R] N)

Tactic:
f.isCompat_apply' (Algebra.algHom R R S) (1 ⊗ₜ[R] x)

Premises used: Algebra.algHom, PolynomialLaw.isCompat_apply', TensorProduct.tmul, OfNat.ofNat
-- 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
f : M →ₚₗ[R] N
S : Type u
inst_5 : CommSemiring S
inst_6 : Algebra R S
x : M
h :
  Eq (α := S ⊗[R] N) (1 ⊗ₜ[R] (TensorProduct.lid R N : (a : R ⊗[R] N) → N) (f.toFun' R (1 ⊗ₜ[R] x)) : S ⊗[R] N)
    ((rTensor N (toLinearMap (Algebra.algHom R R S)) : (a : R ⊗[R] N) → S ⊗[R] N) (f.toFun' R (1 ⊗ₜ[R] x)) : S ⊗[R] N)
h₁ :
  Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] x)
    ((rTensor M (toLinearMap (Algebra.algHom R R S)) : (a : R ⊗[R] M) → S ⊗[R] M) (1 ⊗ₜ[R] x))
⊢ Eq (α := S ⊗[R] N) (1 ⊗ₜ[R] (TensorProduct.lid R N : (a : R ⊗[R] N) → N) (f.toFun' R (1 ⊗ₜ[R] x)) : S ⊗[R] N)
    (f.toFun' S (1 ⊗ₜ[R] x) : S ⊗[R] N)

Tactic:
convert! f.isCompat_apply' (Algebra.algHom R R S) (1 ⊗ₜ[R] x)

Premises used: Algebra.algHom, PolynomialLaw.isCompat_apply', TensorProduct.tmul, OfNat.ofNat
-- 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
f : M →ₚₗ[R] N
S : Type u
inst_5 : CommSemiring S
inst_6 : Algebra R S
x : M
⊢ Eq (α := S ⊗[R] N) (1 ⊗ₜ[R] (TensorProduct.lid R N : (a : R ⊗[R] N) → N) (f.toFun' R (1 ⊗ₜ[R] x)) : S ⊗[R] N)
    ((rTensor N (toLinearMap (Algebra.algHom R R S)) : (a : R ⊗[R] N) → S ⊗[R] N) (f.toFun' R (1 ⊗ₜ[R] x)) : S ⊗[R] N)

Tactic:
simp only [includeRight_lid]

Premises used: TensorProduct.includeRight_lid
-- 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
f : M →ₚₗ[R] N
S : Type u
inst_5 : CommSemiring S
inst_6 : Algebra R S
x : M
h : Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] x : S ⊗[R] M) ((toLinearMap (Algebra.algHom R R S) : (a : R) → S) 1 ⊗ₜ[R] x : S ⊗[R] M)
h₁ : Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] x : S ⊗[R] M) ((Algebra.algHom R R S : (a : R) → S) 1 ⊗ₜ[R] x : S ⊗[R] M)
h₂ h₃ : Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] x) (1 ⊗ₜ[R] x)
⊢ Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] x)
    ((rTensor M (toLinearMap (Algebra.algHom R R S)) : (a : R ⊗[R] M) → S ⊗[R] M) (1 ⊗ₜ[R] x))

Tactic:
rw [rTensor_tmul, toLinearMap_apply, map_one]

Premises used: LinearMap.rTensor_tmul, AlgHom.toLinearMap_apply, map_one
-- 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
f x y : M →ₚₗ[R] N
h : ∀ (m : M), (x + y).ground m = (x.ground + y.ground) m
⊢ (x + y).ground = x.ground + y.ground

Tactic:
ext m
-- 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
f x y : M →ₚₗ[R] N
m : M
⊢ (x + y).ground m = (x.ground + y.ground) m

Tactic:
simp [ground]

Premises used: PolynomialLaw.ground
-- 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
f : M →ₚₗ[R] N
r : R
x : M →ₚₗ[R] N
h : ∀ (m : M), (r • x).ground m = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) x.ground m
⊢ (r • x).ground = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) x.ground

Tactic:
ext m
-- 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
f : M →ₚₗ[R] N
r : R
x : M →ₚₗ[R] N
m : M
⊢ (r • x).ground m = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) x.ground m

Tactic:
simp [ground]

Premises used: PolynomialLaw.ground
-- 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
h : ∀ (x : M), ground.{u, u_1, u_1} (R := R) id x = _root_.id x
⊢ Eq.{u_1 + 1} (α := M → M) (ground.{u, u_1, u_1} (R := R) id) _root_.id

Tactic:
ext
-- 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
x : M
⊢ ground.{u, u_1, u_1} (R := R) id x = _root_.id x

Tactic:
simp [ground_apply, id_apply']

Premises used: PolynomialLaw.id_apply', PolynomialLaw.ground_apply
-- 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
m : M
rw : _root_.id m = m
rw₁ rw₂ : m = m
⊢ ground.{u, u_1, u_1} (R := R) id m = m

Tactic:
rw [ground_id, id_eq]

Premises used: PolynomialLaw.ground_id, id_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
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'
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)
⊢ 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))

Tactic:
ext
-- 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
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'
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:
simp only [Function.comp_apply, isCompat_apply']

Premises used: PolynomialLaw.isCompat_apply', Function.comp_apply
-- 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
P : Type u_3
inst_5 : AddCommMonoid P
inst_6 : Module R P
f : M →ₚₗ[R] N
g : N →ₚₗ[R] P
S : Type u
inst_7 : CommSemiring S
inst_8 : Algebra R S
⊢ Eq (α := S ⊗[R] M → S ⊗[R] P) ((g.comp f).toFun' S) (g.toFun' S ∘ f.toFun' S)

Tactic:
rfl

Premises used: rfl
-- 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
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 : M →ₚₗ[R] N
g : N →ₚₗ[R] P
h : P →ₚₗ[R] Q
⊢ h.comp (g.comp f) = (h.comp g).comp f

Tactic:
rfl

Premises used: PolynomialLaw.comp, rfl
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
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
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
⊢ g.comp id = g

Tactic:
ext
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
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
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:
rfl
-- 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
f : M →ₚₗ[R] N
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
⊢ comp id f = f

Tactic:
ext
-- 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
f : M →ₚₗ[R] N
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:
rfl
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
inst_2 : Algebra R S
s : Finset S
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))
⊢ 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))

Tactic:
rw [← Algebra.adjoin_range_eq_range_aeval]

Premises used: Algebra.adjoin_range_eq_range_aeval
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
inst_2 : Algebra R S
s : Finset S
e_s : (Set.range fun (n : Fin s.card) ↦ (↑((s.equivFin.symm : (a : Fin s.card) → ↥s) n) : S)) = (↑s : Set 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))

Tactic:
congr
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
inst_2 : Algebra R S
s : Finset S
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)
⊢ (Set.range fun (n : Fin s.card) ↦ (↑((s.equivFin.symm : (a : Fin s.card) → ↥s) n) : S)) = (↑s : Set S)

Tactic:
rw [← Function.comp_def, Set.range_comp]

Premises used: Set.range_comp, Function.comp_def
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
inst_2 : Algebra R S
s : Finset 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:
simp only [Equiv.range_eq_univ, Set.image_univ, Subtype.range_coe_subtype, Finset.setOf_mem]

Premises used: Set.image_univ, Finset.setOf_mem, Subtype.range_coe_subtype, Equiv.range_eq_univ
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
inst_2 : Algebra R S
B : Subalgebra R S
hB : B.FG
⊢ AlgHom.range (φ R (Exists.choose (p := fun (t : Finset S) ↦ Algebra.adjoin R (↑t : Set S) = B) hB)) = B

Tactic:
simp only [range_φ, hB.choose_spec]

Premises used: Exists.choose_spec, 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
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))
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)
⊢ (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:
simp only [θ, ← AlgHom.comp_assoc, ← hh']

Premises used: AlgHom.comp_assoc
-- 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
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))
⊢ (ψ.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 [AlgHom.comp_assoc]

Premises used: AlgHom.comp_assoc
-- 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
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 θ)

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]
-- 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
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 θ)
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)
⊢ 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)

Tactic:
rw [← φ.val_comp_rangeRestrict, ← quotientKerEquivRangeₐ_comp_mkₐ φ,
    ← ψ.val_comp_rangeRestrict, ← quotientKerEquivRangeₐ_comp_mkₐ ψ,
    ← AlgHom.comp_assoc, ← AlgHom.comp_assoc _, ht]

Premises used: RingCon.quotientKerEquivRangeₐ_comp_mkₐ, AlgHom.comp_assoc, AlgHom.val_comp_rangeRestrict