Theorem: PolynomialMap.isHomogeneousOfDegreeOne_coeff_single (DividedPowers/PolynomialMap/Homogeneous.lean)

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) = f.ground (m i)
Tactic:
simp only [ground, Function.comp_apply, TensorProduct.lid_symm_apply, ← toFun_eq_toFun']
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 : ι
⊢ ((coeff m) f) (Finsupp.single i 1) = (TensorProduct.lid R N) (f.toFun R (1 ⊗ₜ[R] m i))

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

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]
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

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]
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

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]
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

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
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

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]
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

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 _
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

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]
State after:
no goals

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]
State after:
no goals

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]
State after:
no goals