internlm/Lean-Github huggingface dataset:
Theorem: PolynomialMap.isHomogeneousOfDegreeOne_coeff_single
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
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree 1 f
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : ι → M
i : ι
⊢ ((coeff m) f) (Finsupp.single i 1) = (TensorProduct.lid R N) (f.toFun R (1 ⊗ₜ[R] m i))
Tactic:
have : Finset.sum Finset.univ (fun (j : ι) => (Pi.single i (1 : R) j) ⊗ₜ[R] m j) =
    1 ⊗ₜ[R] m i := by
  rw [Finset.sum_eq_single i (fun b _ hb => by rw [Pi.single_eq_of_ne hb, zero_tmul])
    (fun hi => by simp only [Finset.mem_univ, not_true_eq_false] at hi), Pi.single_eq_same]
Proof state after:
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
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree 1 f
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : ι → M
i : ι
this : ∑ j : ι, Pi.single i 1 j ⊗ₜ[R] m j = 1 ⊗ₜ[R] m i
⊢ ((coeff m) f) (Finsupp.single i 1) = (TensorProduct.lid R N) (f.toFun R (1 ⊗ₜ[R] m i))
Theorem: PolynomialMap.isHomogeneousOfDegreeOne_coeff_single
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
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree 1 f
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : ι → M
i : ι
this : ∑ j : ι, Pi.single i 1 j ⊗ₜ[R] m j = 1 ⊗ₜ[R] m i
⊢ ((coeff m) f) (Finsupp.single i 1) = (TensorProduct.lid R N) (f.toFun R (1 ⊗ₜ[R] m i))
Tactic:
simp only [← this, image_eq_coeff_sum, map_finsupp_sum, TensorProduct.lid_tmul]
Proof state after:
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
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree 1 f
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : ι → M
i : ι
this : ∑ j : ι, Pi.single i 1 j ⊗ₜ[R] m j = 1 ⊗ₜ[R] m i
⊢ ((coeff m) f) (Finsupp.single i 1) =
    ((coeff fun i => m i) f).sum fun a b => (∏ i_1 : ι, Pi.single i 1 i_1 ^ a i_1) • b
Theorem: PolynomialMap.isHomogeneousOfDegreeOne_coeff_single
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
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree 1 f
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : ι → M
i : ι
this : ∑ j : ι, Pi.single i 1 j ⊗ₜ[R] m j = 1 ⊗ₜ[R] m i
⊢ ((coeff m) f) (Finsupp.single i 1) =
    ((coeff fun i => m i) f).sum fun a b => (∏ i_1 : ι, Pi.single i 1 i_1 ^ a i_1) • b
Tactic:
rw [Finsupp.sum_of_support_subset _ (isHomogeneousOfDegreeOne_coeff_support_le hf m),
  sum_map, Function.Embedding.coeFn_mk, sum_eq_single i]
Proof state after:
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
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree 1 f
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : ι → M
i : ι
this : ∑ j : ι, Pi.single i 1 j ⊗ₜ[R] m j = 1 ⊗ₜ[R] m i
⊢ ((coeff m) f) (Finsupp.single i 1) =
    (∏ i_1 : ι, Pi.single i 1 i_1 ^ (Finsupp.single i 1) i_1) • ((coeff m) f) (Finsupp.single i 1)

case h₀
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
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree 1 f
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : ι → M
i : ι
this : ∑ j : ι, Pi.single i 1 j ⊗ₜ[R] m j = 1 ⊗ₜ[R] m i
⊢ ∀ b ∈ univ, b ≠ i → (∏ i_1 : ι, Pi.single i 1 i_1 ^ (Finsupp.single b 1) i_1) • ((coeff m) f) (Finsupp.single b 1) = 0

case h₁
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
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree 1 f
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : ι → M
i : ι
this : ∑ j : ι, Pi.single i 1 j ⊗ₜ[R] m j = 1 ⊗ₜ[R] m i
⊢ i ∉ univ → (∏ i_1 : ι, Pi.single i 1 i_1 ^ (Finsupp.single i 1) i_1) • ((coeff m) f) (Finsupp.single i 1) = 0

case h
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
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree 1 f
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : ι → M
i : ι
this : ∑ j : ι, Pi.single i 1 j ⊗ₜ[R] m j = 1 ⊗ₜ[R] m i
⊢ ∀ i_1 ∈ Finset.map { toFun := fun i => Finsupp.single i 1, inj' := ⋯ } univ,
    (∏ i_2 : ι, Pi.single i 1 i_2 ^ i_1 i_2) • 0 = 0
Theorem: PolynomialMap.isHomogeneousOfDegreeOne_coeff_single
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
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree 1 f
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : ι → M
i : ι
⊢ ∑ j : ι, Pi.single i 1 j ⊗ₜ[R] m j = 1 ⊗ₜ[R] m i
Tactic:
rw [Finset.sum_eq_single i (fun b _ hb => by rw [Pi.single_eq_of_ne hb, zero_tmul])
  (fun hi => by simp only [Finset.mem_univ, not_true_eq_false] at hi), Pi.single_eq_same]
Proof state after:
no goals
Theorem: PolynomialMap.isHomogeneousOfDegreeOne_coeff_single
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
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree 1 f
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : ι → M
i b : ι
x✝ : b ∈ univ
hb : b ≠ i
⊢ Pi.single i 1 b ⊗ₜ[R] m b = 0
Tactic:
rw [Pi.single_eq_of_ne hb, zero_tmul]
Proof state after:
no goals
Theorem: PolynomialMap.isHomogeneousOfDegreeOne_coeff_single
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
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree 1 f
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : ι → M
i : ι
hi : i ∉ univ
⊢ Pi.single i 1 i ⊗ₜ[R] m i = 0
Tactic:
simp only [Finset.mem_univ, not_true_eq_false] at hi
Proof state after:
no goals
Theorem: PolynomialMap.isHomogeneousOfDegreeOne_coeff_single
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
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree 1 f
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : ι → M
i : ι
this : ∑ j : ι, Pi.single i 1 j ⊗ₜ[R] m j = 1 ⊗ₜ[R] m i
⊢ ((coeff m) f) (Finsupp.single i 1) =
    (∏ i_1 : ι, Pi.single i 1 i_1 ^ (Finsupp.single i 1) i_1) • ((coeff m) f) (Finsupp.single i 1)
Tactic:
rw [Finset.prod_eq_single i (fun j _ hj => by rw [Finsupp.single_eq_of_ne hj.symm, pow_zero])
  (fun hi => by simp only [Finset.mem_univ, not_true_eq_false] at hi), Pi.single_eq_same,
  one_pow, _root_.one_smul]
Proof state after:
no goals
Theorem: PolynomialMap.isHomogeneousOfDegreeOne_coeff_single
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
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree 1 f
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : ι → M
i : ι
this : ∑ j : ι, Pi.single i 1 j ⊗ₜ[R] m j = 1 ⊗ₜ[R] m i
j : ι
x✝ : j ∈ univ
hj : j ≠ i
⊢ Pi.single i 1 j ^ (Finsupp.single i 1) j = 1
Tactic:
rw [Finsupp.single_eq_of_ne hj.symm, pow_zero]
Proof state after:
no goals
Theorem: PolynomialMap.isHomogeneousOfDegreeOne_coeff_single
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
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree 1 f
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : ι → M
i : ι
this : ∑ j : ι, Pi.single i 1 j ⊗ₜ[R] m j = 1 ⊗ₜ[R] m i
hi : i ∉ univ
⊢ Pi.single i 1 i ^ (Finsupp.single i 1) i = 1
Tactic:
simp only [Finset.mem_univ, not_true_eq_false] at hi
Proof state after:
no goals
Theorem: PolynomialMap.isHomogeneousOfDegreeOne_coeff_single
Proof state before:
case h₀
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
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree 1 f
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : ι → M
i : ι
this : ∑ j : ι, Pi.single i 1 j ⊗ₜ[R] m j = 1 ⊗ₜ[R] m i
⊢ ∀ b ∈ univ, b ≠ i → (∏ i_1 : ι, Pi.single i 1 i_1 ^ (Finsupp.single b 1) i_1) • ((coeff m) f) (Finsupp.single b 1) = 0
Tactic:
intro j _ hj
Proof state after:
case h₀
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
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree 1 f
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : ι → M
i : ι
this : ∑ j : ι, Pi.single i 1 j ⊗ₜ[R] m j = 1 ⊗ₜ[R] m i
j : ι
a✝ : j ∈ univ
hj : j ≠ i
⊢ (∏ i_1 : ι, Pi.single i 1 i_1 ^ (Finsupp.single j 1) i_1) • ((coeff m) f) (Finsupp.single j 1) = 0
Theorem: PolynomialMap.isHomogeneousOfDegreeOne_coeff_single
Proof state before:
case h₀
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
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree 1 f
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : ι → M
i : ι
this : ∑ j : ι, Pi.single i 1 j ⊗ₜ[R] m j = 1 ⊗ₜ[R] m i
j : ι
a✝ : j ∈ univ
hj : j ≠ i
⊢ (∏ i_1 : ι, Pi.single i 1 i_1 ^ (Finsupp.single j 1) i_1) • ((coeff m) f) (Finsupp.single j 1) = 0
Tactic:
rw [Finset.prod_eq_zero (i := j), _root_.zero_smul]
Proof state after:
case h₀.hi
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
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree 1 f
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : ι → M
i : ι
this : ∑ j : ι, Pi.single i 1 j ⊗ₜ[R] m j = 1 ⊗ₜ[R] m i
j : ι
a✝ : j ∈ univ
hj : j ≠ i
⊢ j ∈ univ

case h₀.h
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
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree 1 f
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : ι → M
i : ι
this : ∑ j : ι, Pi.single i 1 j ⊗ₜ[R] m j = 1 ⊗ₜ[R] m i
j : ι
a✝ : j ∈ univ
hj : j ≠ i
⊢ Pi.single i 1 j ^ (Finsupp.single j 1) j = 0
Theorem: PolynomialMap.isHomogeneousOfDegreeOne_coeff_single
Proof state before:
case h₀.hi
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
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree 1 f
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : ι → M
i : ι
this : ∑ j : ι, Pi.single i 1 j ⊗ₜ[R] m j = 1 ⊗ₜ[R] m i
j : ι
a✝ : j ∈ univ
hj : j ≠ i
⊢ j ∈ univ

case h₀.h
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
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree 1 f
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : ι → M
i : ι
this : ∑ j : ι, Pi.single i 1 j ⊗ₜ[R] m j = 1 ⊗ₜ[R] m i
j : ι
a✝ : j ∈ univ
hj : j ≠ i
⊢ Pi.single i 1 j ^ (Finsupp.single j 1) j = 0
Tactic:
exact Finset.mem_univ _
Proof state after:
case h₀.h
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
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree 1 f
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : ι → M
i : ι
this : ∑ j : ι, Pi.single i 1 j ⊗ₜ[R] m j = 1 ⊗ₜ[R] m i
j : ι
a✝ : j ∈ univ
hj : j ≠ i
⊢ Pi.single i 1 j ^ (Finsupp.single j 1) j = 0
Theorem: PolynomialMap.isHomogeneousOfDegreeOne_coeff_single
Proof state before:
case h₀.h
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
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree 1 f
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : ι → M
i : ι
this : ∑ j : ι, Pi.single i 1 j ⊗ₜ[R] m j = 1 ⊗ₜ[R] m i
j : ι
a✝ : j ∈ univ
hj : j ≠ i
⊢ Pi.single i 1 j ^ (Finsupp.single j 1) j = 0
Tactic:
rw [Finsupp.single_eq_same, Pi.single_eq_of_ne hj, pow_one]
Proof state after:
no goals
Theorem: PolynomialMap.isHomogeneousOfDegreeOne_coeff_single
Proof state before:
case h₁
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
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree 1 f
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : ι → M
i : ι
this : ∑ j : ι, Pi.single i 1 j ⊗ₜ[R] m j = 1 ⊗ₜ[R] m i
⊢ i ∉ univ → (∏ i_1 : ι, Pi.single i 1 i_1 ^ (Finsupp.single i 1) i_1) • ((coeff m) f) (Finsupp.single i 1) = 0
Tactic:
simp only [mem_univ, not_true_eq_false, IsEmpty.forall_iff]
Proof state after:
no goals
Theorem: PolynomialMap.isHomogeneousOfDegreeOne_coeff_single
Proof state before:
case h
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
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree 1 f
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : ι → M
i : ι
this : ∑ j : ι, Pi.single i 1 j ⊗ₜ[R] m j = 1 ⊗ₜ[R] m i
⊢ ∀ i_1 ∈ Finset.map { toFun := fun i => Finsupp.single i 1, inj' := ⋯ } univ,
    (∏ i_2 : ι, Pi.single i 1 i_2 ^ i_1 i_2) • 0 = 0
Tactic:
simp only [mem_map, mem_univ, Function.Embedding.coeFn_mk, true_and, smul_zero,
forall_exists_index, implies_true, forall_const]
Proof state after:
no goals
Theorem: PolynomialMap.ofLinearMap_mem_grade_one
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
v : M →ₗ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
m : S ⊗[R] M
⊢ (ofLinearMap v).toFun' S (r • m) = r ^ 1 • (ofLinearMap v).toFun' S m
Tactic:
simp only [ofLinearMap, LinearMapClass.map_smul, pow_one]
Proof state after:
no goals
Theorem: PolynomialMap.ofLinearMap_toFun
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
u : M →ₗ[R] N
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (ofLinearMap u).toFun S = ⇑(baseChange S u)
Tactic:
ext sm
Proof state after:
case h
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
u : M →ₗ[R] N
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
sm : S ⊗[R] M
⊢ (ofLinearMap u).toFun S sm = (baseChange S u) sm
Theorem: PolynomialMap.ofLinearMap_toFun
Proof state before:
case h
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
u : M →ₗ[R] N
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
sm : S ⊗[R] M
⊢ (ofLinearMap u).toFun S sm = (baseChange S u) sm
Tactic:
obtain ⟨n, φ, p, rfl⟩ := exists_lift sm
Proof state after:
case h.intro.intro.intro
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
u : M →ₗ[R] N
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
φ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
⊢ (ofLinearMap u).toFun S ((rTensor M φ.toLinearMap) p) = (baseChange S u) ((rTensor M φ.toLinearMap) p)
Theorem: PolynomialMap.ofLinearMap_toFun
Proof state before:
case h.intro.intro.intro
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
u : M →ₗ[R] N
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
φ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
⊢ (ofLinearMap u).toFun S ((rTensor M φ.toLinearMap) p) = (baseChange S u) ((rTensor M φ.toLinearMap) p)
Tactic:
simp only [← isCompat_apply, toFun_eq_toFun', ofLinearMap_toFun', baseChange_eq_ltensor,
  ← LinearMap.comp_apply, rTensor_comp_lTensor, lTensor_comp_rTensor]
Proof state after:
no goals
Theorem: PolynomialMap.ofLinearMap_coeff_single
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
u : M →ₗ[R] N
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
i : ι
⊢ ((coeff m) (ofLinearMap u)) (Finsupp.single i 1) = u (m i)
Tactic:
rw [coeff, generize, coe_comp, LinearEquiv.coe_coe, coe_mk, AddHom.coe_mk, Function.comp_apply]
Proof state after:
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
u : M →ₗ[R] N
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
i : ι
⊢ (scalarRTensor ((ofLinearMap u).toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i))) (Finsupp.single i 1) = u (m i)
Theorem: PolynomialMap.ofLinearMap_coeff_single
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
u : M →ₗ[R] N
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
i : ι
⊢ (scalarRTensor ((ofLinearMap u).toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i))) (Finsupp.single i 1) = u (m i)
Tactic:
simp only [ofLinearMap_toFun, map_sum, LinearMap.baseChange_tmul]
Proof state after:
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
u : M →ₗ[R] N
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
i : ι
⊢ (∑ x : ι, scalarRTensor (X x ⊗ₜ[R] u (m x))) (Finsupp.single i 1) = u (m i)
Theorem: PolynomialMap.ofLinearMap_coeff_single
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
u : M →ₗ[R] N
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
i : ι
⊢ (∑ x : ι, scalarRTensor (X x ⊗ₜ[R] u (m x))) (Finsupp.single i 1) = u (m i)
Tactic:
rw [Finsupp.coe_finset_sum, Finset.sum_apply, Finset.sum_eq_single i _ (fun hi => by
  simp only [mem_univ, not_true_eq_false] at hi), scalarRTensor_apply_tmul_apply,
    coeff_X, _root_.one_smul]
Proof state after:
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
u : M →ₗ[R] N
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
i : ι
⊢ ∀ b ∈ univ, b ≠ i → (scalarRTensor (X b ⊗ₜ[R] u (m b))) (Finsupp.single i 1) = 0
Theorem: PolynomialMap.ofLinearMap_coeff_single
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
u : M →ₗ[R] N
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
i : ι
hi : i ∉ univ
⊢ (scalarRTensor (X i ⊗ₜ[R] u (m i))) (Finsupp.single i 1) = 0
Tactic:
simp only [mem_univ, not_true_eq_false] at hi
Proof state after:
no goals
Theorem: PolynomialMap.ofLinearMap_coeff_single
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
u : M →ₗ[R] N
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
i : ι
⊢ ∀ b ∈ univ, b ≠ i → (scalarRTensor (X b ⊗ₜ[R] u (m b))) (Finsupp.single i 1) = 0
Tactic:
intro b _ hb
Proof state after:
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
u : M →ₗ[R] N
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
i b : ι
a✝ : b ∈ univ
hb : b ≠ i
⊢ (scalarRTensor (X b ⊗ₜ[R] u (m b))) (Finsupp.single i 1) = 0
Theorem: PolynomialMap.ofLinearMap_coeff_single
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
u : M →ₗ[R] N
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
i b : ι
a✝ : b ∈ univ
hb : b ≠ i
⊢ (scalarRTensor (X b ⊗ₜ[R] u (m b))) (Finsupp.single i 1) = 0
Tactic:
have hb' : ¬ Finsupp.single b 1 = Finsupp.single i 1 := by
  rwa [Finsupp.single_left_inj]; norm_num
Proof state after:
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
u : M →ₗ[R] N
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
i b : ι
a✝ : b ∈ univ
hb : b ≠ i
hb' : ¬Finsupp.single b 1 = Finsupp.single i 1
⊢ (scalarRTensor (X b ⊗ₜ[R] u (m b))) (Finsupp.single i 1) = 0
Theorem: PolynomialMap.ofLinearMap_coeff_single
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
u : M →ₗ[R] N
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
i b : ι
a✝ : b ∈ univ
hb : b ≠ i
hb' : ¬Finsupp.single b 1 = Finsupp.single i 1
⊢ (scalarRTensor (X b ⊗ₜ[R] u (m b))) (Finsupp.single i 1) = 0
Tactic:
rw [scalarRTensor_apply_tmul_apply, coeff_X', if_neg hb', _root_.zero_smul]
Proof state after:
no goals
Theorem: PolynomialMap.ofLinearMap_coeff_single
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
u : M →ₗ[R] N
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
i b : ι
a✝ : b ∈ univ
hb : b ≠ i
⊢ ¬Finsupp.single b 1 = Finsupp.single i 1
Tactic:
rwa [Finsupp.single_left_inj]
Proof state after:
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
u : M →ₗ[R] N
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
i b : ι
a✝ : b ∈ univ
hb : b ≠ i
⊢ 1 ≠ 0
Theorem: PolynomialMap.ofLinearMap_coeff_single
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
u : M →ₗ[R] N
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
i b : ι
a✝ : b ∈ univ
hb : b ≠ i
⊢ 1 ≠ 0
Tactic:
norm_num
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
⊢ 0 ^ a + 0 ^ b = 1
Tactic:
suffices (a = 1 ∧ b = 0) ∨ (a = 0 ∧ b = 1) by
  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:
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