internlm/Lean-Github huggingface dataset:
Theorem: PolynomialMap.zero_pow_add_zero_pow
Proof state before:
R✝ : Type u
inst✝⁹ : CommRing R✝
M✝ : Type u_1
N✝ : Type u_2
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup N✝
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ N✝
R : Type u
inst✝⁴ : CommRing R
M : Type ?u.366545
N : Type ?u.366548
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
a b : ℕ
h : a + b = 1
⊢ a = 1 ∧ b = 0 ∨ a = 0 ∧ b = 1
Tactic:
by_cases ha : a = 0
Proof state after:
case pos
R✝ : Type u
inst✝⁹ : CommRing R✝
M✝ : Type u_1
N✝ : Type u_2
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup N✝
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ N✝
R : Type u
inst✝⁴ : CommRing R
M : Type ?u.366545
N : Type ?u.366548
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
a b : ℕ
h : a + b = 1
ha : a = 0
⊢ a = 1 ∧ b = 0 ∨ a = 0 ∧ b = 1

case neg
R✝ : Type u
inst✝⁹ : CommRing R✝
M✝ : Type u_1
N✝ : Type u_2
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup N✝
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ N✝
R : Type u
inst✝⁴ : CommRing R
M : Type ?u.366545
N : Type ?u.366548
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
a b : ℕ
h : a + b = 1
ha : ¬a = 0
⊢ a = 1 ∧ b = 0 ∨ a = 0 ∧ b = 1
Theorem: PolynomialMap.zero_pow_add_zero_pow
Proof state before:
R✝ : Type u
inst✝⁹ : CommRing R✝
M✝ : Type u_1
N✝ : Type u_2
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup N✝
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ N✝
R : Type u
inst✝⁴ : CommRing R
M : Type ?u.366545
N : Type ?u.366548
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
a b : ℕ
h : a + b = 1
this : a = 1 ∧ b = 0 ∨ a = 0 ∧ b = 1
⊢ 0 ^ a + 0 ^ b = 1
Tactic:
cases this with
| inl h => rw [h.1, h.2, pow_one, pow_zero, zero_add]
| inr h => rw [h.1, h.2, pow_one, pow_zero, add_zero]
Proof state after:
no goals
Theorem: PolynomialMap.zero_pow_add_zero_pow
Proof state before:
case inl
R✝ : Type u
inst✝⁹ : CommRing R✝
M✝ : Type u_1
N✝ : Type u_2
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup N✝
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ N✝
R : Type u
inst✝⁴ : CommRing R
M : Type ?u.366545
N : Type ?u.366548
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
a b : ℕ
h✝ : a + b = 1
h : a = 1 ∧ b = 0
⊢ 0 ^ a + 0 ^ b = 1
Tactic:
rw [h.1, h.2, pow_one, pow_zero, zero_add]
Proof state after:
no goals
Theorem: PolynomialMap.zero_pow_add_zero_pow
Proof state before:
case inr
R✝ : Type u
inst✝⁹ : CommRing R✝
M✝ : Type u_1
N✝ : Type u_2
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup N✝
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ N✝
R : Type u
inst✝⁴ : CommRing R
M : Type ?u.366545
N : Type ?u.366548
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
a b : ℕ
h✝ : a + b = 1
h : a = 0 ∧ b = 1
⊢ 0 ^ a + 0 ^ b = 1
Tactic:
rw [h.1, h.2, pow_one, pow_zero, add_zero]
Proof state after:
no goals
Theorem: PolynomialMap.zero_pow_add_zero_pow
Proof state before:
case pos
R✝ : Type u
inst✝⁹ : CommRing R✝
M✝ : Type u_1
N✝ : Type u_2
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup N✝
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ N✝
R : Type u
inst✝⁴ : CommRing R
M : Type ?u.366545
N : Type ?u.366548
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
a b : ℕ
h : a + b = 1
ha : a = 0
⊢ a = 1 ∧ b = 0 ∨ a = 0 ∧ b = 1
Tactic:
exact Or.inr ⟨ha, by simpa [ha, zero_add] using h⟩
Proof state after:
no goals
Theorem: PolynomialMap.zero_pow_add_zero_pow
Proof state before:
R✝ : Type u
inst✝⁹ : CommRing R✝
M✝ : Type u_1
N✝ : Type u_2
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup N✝
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ N✝
R : Type u
inst✝⁴ : CommRing R
M : Type ?u.366545
N : Type ?u.366548
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
a b : ℕ
h : a + b = 1
ha : a = 0
⊢ b = 1
Tactic:
simpa [ha, zero_add] using h
Proof state after:
no goals
Theorem: PolynomialMap.zero_pow_add_zero_pow
Proof state before:
case neg
R✝ : Type u
inst✝⁹ : CommRing R✝
M✝ : Type u_1
N✝ : Type u_2
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup N✝
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ N✝
R : Type u
inst✝⁴ : CommRing R
M : Type ?u.366545
N : Type ?u.366548
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
a b : ℕ
h : a + b = 1
ha : ¬a = 0
⊢ a = 1 ∧ b = 0 ∨ a = 0 ∧ b = 1
Tactic:
have ha : a = 1 := le_antisymm (h ▸  Nat.le_add_right a b) (Nat.pos_of_ne_zero ha)
Proof state after:
case neg
R✝ : Type u
inst✝⁹ : CommRing R✝
M✝ : Type u_1
N✝ : Type u_2
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup N✝
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ N✝
R : Type u
inst✝⁴ : CommRing R
M : Type ?u.366545
N : Type ?u.366548
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
a b : ℕ
h : a + b = 1
ha✝ : ¬a = 0
ha : a = 1
⊢ a = 1 ∧ b = 0 ∨ a = 0 ∧ b = 1
Theorem: PolynomialMap.zero_pow_add_zero_pow
Proof state before:
case neg
R✝ : Type u
inst✝⁹ : CommRing R✝
M✝ : Type u_1
N✝ : Type u_2
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup N✝
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ N✝
R : Type u
inst✝⁴ : CommRing R
M : Type ?u.366545
N : Type ?u.366548
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
a b : ℕ
h : a + b = 1
ha✝ : ¬a = 0
ha : a = 1
⊢ a = 1 ∧ b = 0 ∨ a = 0 ∧ b = 1
Tactic:
exact Or.inl ⟨ha, by simpa [ha, add_right_eq_self] using h⟩
Proof state after:
no goals
Theorem: PolynomialMap.zero_pow_add_zero_pow
Proof state before:
R✝ : Type u
inst✝⁹ : CommRing R✝
M✝ : Type u_1
N✝ : Type u_2
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup N✝
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ N✝
R : Type u
inst✝⁴ : CommRing R
M : Type ?u.366545
N : Type ?u.366548
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
a b : ℕ
h : a + b = 1
ha✝ : ¬a = 0
ha : a = 1
⊢ b = 0
Tactic:
simpa [ha, add_right_eq_self] using h
Proof state after:
no goals
Theorem: PolynomialMap.component_toFun
Proof state before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (component p f).toFun S = fun m =>
    ((Polynomial.rTensor R N S) (f.toFun S[X] ((LinearMap.rTensor M (↑R (monomial 1))) m))) p
Tactic:
sorry
Proof state after:
no goals
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
⊢ IsHomogeneousOfDegree p (component p f)
Tactic:
intro S _ _ s sm
Proof state after:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
⊢ (component p f).toFun' S (s • sm) = s ^ p • (component p f).toFun' S sm
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
⊢ (component p f).toFun' S (s • sm) = s ^ p • (component p f).toFun' S sm
Tactic:
dsimp [component]
Proof state after:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
⊢ ((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) (s • sm)))) p =
    s ^ p • ((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))) p
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
⊢ ((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) (s • sm)))) p =
    s ^ p • ((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))) p
Tactic:
let ψ := ((aeval (R := S) (monomial 1 s : S[X])).restrictScalars R)
Proof state after:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
⊢ ((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) (s • sm)))) p =
    s ^ p • ((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))) p
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
⊢ ((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) (s • sm)))) p =
    s ^ p • ((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))) p
Tactic:
suffices  (rTensor M ((monomial 1).restrictScalars R)) (s • sm)
    = (rTensor M ψ.toLinearMap) (rTensor M ((monomial 1).restrictScalars R) sm) by
  rw [this, ← f.isCompat_apply' ψ]
  generalize toFun' f S[X] (rTensor M ((monomial 1).restrictScalars R) sm) = t
  rw [rTensor_apply, rTensor_apply, ← rTensor_comp_apply]
  conv_rhs =>
    rw [← (IsLinearMap.isLinearMap_smul (s ^ p)).mk'_apply, ← coe_restrictScalars R,
      ← LinearMap.comp_apply]
  apply LinearMap.congr_fun
  apply symm
  dsimp only [LinearMap.rTensor, TensorProduct.map]
  apply TensorProduct.lift.unique
  intro f n
  simp only [compl₂_id, coe_comp, coe_restrictScalars, Function.comp_apply, lift.tmul,
    lcoeff_apply, mk_apply, IsLinearMap.mk'_apply, AlgHom.toLinearMap_apply,
    AlgHom.coe_restrictScalars', TensorProduct.smul_tmul']
  apply congr_arg₂ _ _ rfl
  induction f using Polynomial.induction_on' with
  | h_add f g hf hg => rw [coeff_add, smul_add, hf, hg, ← coeff_add, map_add]
  | h_monomial n a =>
      simp only [ψ, aeval_monomial, ← smul_eq_mul, algebraMap_smul, coeff_smul, monomial_pow,
        one_mul, coeff_monomial]
      split_ifs with h
      . rw [smul_eq_mul, mul_comm, h, AlgHom.coe_restrictScalars', aeval_monomial, monomial_pow,
          one_mul, ← C_eq_algebraMap]
        simp only [C_mul_monomial, coeff_monomial, if_pos]
      . simp only [smul_zero, AlgHom.coe_restrictScalars', aeval_monomial, ← C_eq_algebraMap,
          monomial_pow, one_mul, C_mul_monomial, coeff_monomial, if_neg h]
Proof state after:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
⊢ (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
⊢ (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
Tactic:
.  suffices ∀ (sm : S ⊗[R] M), s • sm =
      rTensor M (((IsLinearMap.isLinearMap_smul s).mk').restrictScalars R) sm by
    simp only [this, ← rTensor_comp_apply]
    apply LinearMap.congr_fun
    apply congr_arg
    rw [LinearMap.ext_iff]
    intro r
    simp only [compl₂_id, smul_eq_mul, lift.tmul, coe_comp, coe_restrictScalars,
      Function.comp_apply, IsLinearMap.mk'_apply, mk_apply, AlgHom.toLinearMap_apply,
      AlgHom.coe_restrictScalars', aeval_monomial, pow_one]
    rw [mul_comm]
    simp only [AlgHom.coe_restrictScalars', aeval_monomial, pow_one, ψ, ← smul_eq_mul,
      algebraMap_smul, Polynomial.smul_monomial]
  intro sm
  rw [← (IsLinearMap.isLinearMap_smul s).mk'_apply, ← LinearMap.coe_restrictScalars R]
  apply LinearMap.congr_fun
  dsimp only [LinearMap.rTensor, TensorProduct.map, smul_eq_mul]
  apply lift.unique
  intro r m
  simp only [coe_restrictScalars, IsLinearMap.mk'_apply, compl₂_id, coe_comp, Function.comp_apply,
    mk_apply, smul_tmul', smul_eq_mul]
Proof state after:
no goals
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
⊢ ((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) (s • sm)))) p =
    s ^ p • ((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))) p
Tactic:
rw [this, ← f.isCompat_apply' ψ]
Proof state after:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
⊢ ((Polynomial.rTensor R N S)
        ((LinearMap.rTensor N ψ.toLinearMap) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))))
      p =
    s ^ p • ((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))) p
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
⊢ ((Polynomial.rTensor R N S)
        ((LinearMap.rTensor N ψ.toLinearMap) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))))
      p =
    s ^ p • ((Polynomial.rTensor R N S) (f.toFun' S[X] ((LinearMap.rTensor M (↑R (monomial 1))) sm))) p
Tactic:
generalize toFun' f S[X] (rTensor M ((monomial 1).restrictScalars R) sm) = t
Proof state after:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
⊢ ((Polynomial.rTensor R N S) ((LinearMap.rTensor N ψ.toLinearMap) t)) p = s ^ p • ((Polynomial.rTensor R N S) t) p
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
⊢ ((Polynomial.rTensor R N S) ((LinearMap.rTensor N ψ.toLinearMap) t)) p = s ^ p • ((Polynomial.rTensor R N S) t) p
Tactic:
rw [rTensor_apply, rTensor_apply, ← rTensor_comp_apply]
Proof state after:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
⊢ (LinearMap.rTensor N (↑R (lcoeff S p) ∘ₗ ψ.toLinearMap)) t = s ^ p • (LinearMap.rTensor N (↑R (lcoeff S p))) t
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
⊢ (LinearMap.rTensor N (↑R (lcoeff S p) ∘ₗ ψ.toLinearMap)) t = s ^ p • (LinearMap.rTensor N (↑R (lcoeff S p))) t
Tactic:
conv_rhs =>
  rw [← (IsLinearMap.isLinearMap_smul (s ^ p)).mk'_apply, ← coe_restrictScalars R,
    ← LinearMap.comp_apply]
Proof state after:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
⊢ (LinearMap.rTensor N (↑R (lcoeff S p) ∘ₗ ψ.toLinearMap)) t =
    (↑R (IsLinearMap.mk' (fun z => s ^ p • z) ⋯) ∘ₗ LinearMap.rTensor N (↑R (lcoeff S p))) t
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
⊢ (LinearMap.rTensor N (↑R (lcoeff S p) ∘ₗ ψ.toLinearMap)) t =
    (↑R (IsLinearMap.mk' (fun z => s ^ p • z) ⋯) ∘ₗ LinearMap.rTensor N (↑R (lcoeff S p))) t
Tactic:
apply LinearMap.congr_fun
Proof state after:
case h
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
⊢ LinearMap.rTensor N (↑R (lcoeff S p) ∘ₗ ψ.toLinearMap) =
    ↑R (IsLinearMap.mk' (fun z => s ^ p • z) ⋯) ∘ₗ LinearMap.rTensor N (↑R (lcoeff S p))
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
case h
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
⊢ LinearMap.rTensor N (↑R (lcoeff S p) ∘ₗ ψ.toLinearMap) =
    ↑R (IsLinearMap.mk' (fun z => s ^ p • z) ⋯) ∘ₗ LinearMap.rTensor N (↑R (lcoeff S p))
Tactic:
apply symm
Proof state after:
case h.a
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
⊢ ↑R (IsLinearMap.mk' (fun z => s ^ p • z) ⋯) ∘ₗ LinearMap.rTensor N (↑R (lcoeff S p)) =
    LinearMap.rTensor N (↑R (lcoeff S p) ∘ₗ ψ.toLinearMap)
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
case h.a
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
⊢ ↑R (IsLinearMap.mk' (fun z => s ^ p • z) ⋯) ∘ₗ LinearMap.rTensor N (↑R (lcoeff S p)) =
    LinearMap.rTensor N (↑R (lcoeff S p) ∘ₗ ψ.toLinearMap)
Tactic:
dsimp only [LinearMap.rTensor, TensorProduct.map]
Proof state after:
case h.a
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
⊢ ↑R (IsLinearMap.mk' (fun z => s ^ p • z) ⋯) ∘ₗ
      lift ((TensorProduct.mk R S N).compl₂ LinearMap.id ∘ₗ ↑R (lcoeff S p)) =
    lift ((TensorProduct.mk R S N).compl₂ LinearMap.id ∘ₗ ↑R (lcoeff S p) ∘ₗ ψ.toLinearMap)