Theorem: PolynomialMap.isHomogeneousOfDegreeOne_coeff_support_le (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
⊢ 1 ≠ 0
Tactic:
norm_num
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
⊢ ((coeff m) f).support ⊆ Finset.map { toFun := fun i => Finsupp.single i 1, inj' := ⋯ } univ
Tactic:
intro d hd
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
d : ι →₀ ℕ
hd : d ∈ ((coeff m) f).support
⊢ d ∈ Finset.map { toFun := fun i => Finsupp.single i 1, inj' := ⋯ } univ

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
d : ι →₀ ℕ
hd : d ∈ ((coeff m) f).support
⊢ d ∈ Finset.map { toFun := fun i => Finsupp.single i 1, inj' := ⋯ } univ
Tactic:
simp only [Finsupp.mem_support_iff, ne_eq] at hd
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
d : ι →₀ ℕ
hd : ¬((coeff m) f) d = 0
⊢ d ∈ Finset.map { toFun := fun i => Finsupp.single i 1, inj' := ⋯ } univ

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
d : ι →₀ ℕ
hd : ¬((coeff m) f) d = 0
⊢ d ∈ Finset.map { toFun := fun i => Finsupp.single i 1, inj' := ⋯ } univ
Tactic:
let hd' := (not_imp_comm.mp (isHomogeneousOfDegreeOne_coeff hf m)) hd
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
d : ι →₀ ℕ
hd : ¬((coeff m) f) d = 0
hd' : (d.sum fun x n => n) = 1 := not_imp_comm.mp (isHomogeneousOfDegreeOne_coeff hf m) hd
⊢ d ∈ Finset.map { toFun := fun i => Finsupp.single i 1, inj' := ⋯ } univ

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
d : ι →₀ ℕ
hd : ¬((coeff m) f) d = 0
hd' : (d.sum fun x n => n) = 1 := not_imp_comm.mp (isHomogeneousOfDegreeOne_coeff hf m) hd
⊢ d ∈ Finset.map { toFun := fun i => Finsupp.single i 1, inj' := ⋯ } univ
Tactic:
simpa only [Finset.mem_map, Finset.mem_univ, Function.Embedding.coeFn_mk,
  true_and, Finsupp.sum_eq_one_iff] using hd'
State after:
no goals