internlm/Lean-Github huggingface dataset:
Theorem: PolynomialMap.Finsupp.sum_eq_one_iff
Proof state before:
case mp.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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
h1 : (d.sum fun x n => n) = 1
hd0 : d ≠ 0
a : α
ha : ¬d a = 0
⊢ ∃ a, Finsupp.single a 1 = d
Tactic:
rw [← Finsupp.add_sum_erase' _ a, Nat.add_eq_one_iff] at h1
Proof state after:
case mp.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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
h1 : d a = 0 ∧ ((Finsupp.erase a d).sum fun x n => n) = 1 ∨ d a = 1 ∧ ((Finsupp.erase a d).sum fun x n => n) = 0
ha : ¬d a = 0
⊢ ∃ a, Finsupp.single a 1 = d

case mp.intro.hg
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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
h1 : (d.sum fun x n => n) = 1
hd0 : d ≠ 0
a : α
ha : ¬d a = 0
⊢ α → 0 = 0
Theorem: PolynomialMap.Finsupp.sum_eq_one_iff
Proof state before:
case mp.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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
h1 : d a = 0 ∧ ((Finsupp.erase a d).sum fun x n => n) = 1 ∨ d a = 1 ∧ ((Finsupp.erase a d).sum fun x n => n) = 0
ha : ¬d a = 0
⊢ ∃ a, Finsupp.single a 1 = d

case mp.intro.hg
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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
h1 : (d.sum fun x n => n) = 1
hd0 : d ≠ 0
a : α
ha : ¬d a = 0
⊢ α → 0 = 0
Tactic:
rcases h1 with (⟨ha', _⟩ | ⟨ha, ha'⟩)
Proof state after:
case mp.intro.inl.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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha : ¬d a = 0
ha' : d a = 0
right✝ : ((Finsupp.erase a d).sum fun x n => n) = 1
⊢ ∃ a, Finsupp.single a 1 = d

case mp.intro.inr.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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ((Finsupp.erase a d).sum fun x n => n) = 0
⊢ ∃ a, Finsupp.single a 1 = d

case mp.intro.hg
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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
h1 : (d.sum fun x n => n) = 1
hd0 : d ≠ 0
a : α
ha : ¬d a = 0
⊢ α → 0 = 0
Theorem: PolynomialMap.Finsupp.sum_eq_one_iff
Proof state before:
case mp.intro.hg
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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
h1 : (d.sum fun x n => n) = 1
hd0 : d ≠ 0
a : α
ha : ¬d a = 0
⊢ α → 0 = 0
Tactic:
exact fun _ ↦ rfl
Proof state after:
no goals
Theorem: PolynomialMap.Finsupp.sum_eq_one_iff
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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
h1 : (d.sum fun x n => n) = 1
⊢ d ≠ 0
Tactic:
intro h
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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
h1 : (d.sum fun x n => n) = 1
h : d = 0
⊢ False
Theorem: PolynomialMap.Finsupp.sum_eq_one_iff
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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
h1 : (d.sum fun x n => n) = 1
h : d = 0
⊢ False
Tactic:
simp only [h, Finsupp.sum_zero_index, zero_ne_one] at h1
Proof state after:
no goals
Theorem: PolynomialMap.Finsupp.sum_eq_one_iff
Proof state before:
case mp.intro.inl.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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha : ¬d a = 0
ha' : d a = 0
right✝ : ((Finsupp.erase a d).sum fun x n => n) = 1
⊢ ∃ a, Finsupp.single a 1 = d
Tactic:
exfalso
Proof state after:
case mp.intro.inl.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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha : ¬d a = 0
ha' : d a = 0
right✝ : ((Finsupp.erase a d).sum fun x n => n) = 1
⊢ False
Theorem: PolynomialMap.Finsupp.sum_eq_one_iff
Proof state before:
case mp.intro.inl.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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha : ¬d a = 0
ha' : d a = 0
right✝ : ((Finsupp.erase a d).sum fun x n => n) = 1
⊢ False
Tactic:
exact ha ha'
Proof state after:
no goals
Theorem: PolynomialMap.Finsupp.sum_eq_one_iff
Proof state before:
case mp.intro.inr.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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ((Finsupp.erase a d).sum fun x n => n) = 0
⊢ ∃ a, Finsupp.single a 1 = d
Tactic:
use a
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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ((Finsupp.erase a d).sum fun x n => n) = 0
⊢ Finsupp.single a 1 = d
Theorem: PolynomialMap.Finsupp.sum_eq_one_iff
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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ((Finsupp.erase a d).sum fun x n => n) = 0
⊢ Finsupp.single a 1 = d
Tactic:
simp only [Finsupp.sum, Finsupp.support_erase, sum_eq_zero_iff, mem_erase] at ha'
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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ∀ (x : α), x ≠ a ∧ x ∈ d.support → (Finsupp.erase a d) x = 0
⊢ Finsupp.single a 1 = d
Theorem: PolynomialMap.Finsupp.sum_eq_one_iff
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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ∀ (x : α), x ≠ a ∧ x ∈ d.support → (Finsupp.erase a d) x = 0
⊢ Finsupp.single a 1 = d
Tactic:
ext b
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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ∀ (x : α), x ≠ a ∧ x ∈ d.support → (Finsupp.erase a d) x = 0
b : α
⊢ (Finsupp.single a 1) b = d b
Theorem: PolynomialMap.Finsupp.sum_eq_one_iff
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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ∀ (x : α), x ≠ a ∧ x ∈ d.support → (Finsupp.erase a d) x = 0
b : α
⊢ (Finsupp.single a 1) b = d b
Tactic:
by_cases hb : a = b
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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ∀ (x : α), x ≠ a ∧ x ∈ d.support → (Finsupp.erase a d) x = 0
b : α
hb : a = b
⊢ (Finsupp.single a 1) b = d b

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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ∀ (x : α), x ≠ a ∧ x ∈ d.support → (Finsupp.erase a d) x = 0
b : α
hb : ¬a = b
⊢ (Finsupp.single a 1) b = d b
Theorem: PolynomialMap.Finsupp.sum_eq_one_iff
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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ∀ (x : α), x ≠ a ∧ x ∈ d.support → (Finsupp.erase a d) x = 0
b : α
hb : a = b
⊢ (Finsupp.single a 1) b = d b
Tactic:
rw [← hb, Finsupp.single_eq_same, ha]
Proof state after:
no goals
Theorem: PolynomialMap.Finsupp.sum_eq_one_iff
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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ∀ (x : α), x ≠ a ∧ x ∈ d.support → (Finsupp.erase a d) x = 0
b : α
hb : ¬a = b
⊢ (Finsupp.single a 1) b = d b
Tactic:
rw [Finsupp.single_eq_of_ne hb]
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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ∀ (x : α), x ≠ a ∧ x ∈ d.support → (Finsupp.erase a d) x = 0
b : α
hb : ¬a = b
⊢ 0 = d b
Theorem: PolynomialMap.Finsupp.sum_eq_one_iff
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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ∀ (x : α), x ≠ a ∧ x ∈ d.support → (Finsupp.erase a d) x = 0
b : α
hb : ¬a = b
⊢ 0 = d b
Tactic:
apply symm
Proof state after:
case neg.a
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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ∀ (x : α), x ≠ a ∧ x ∈ d.support → (Finsupp.erase a d) x = 0
b : α
hb : ¬a = b
⊢ d b = 0
Theorem: PolynomialMap.Finsupp.sum_eq_one_iff
Proof state before:
case neg.a
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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
ha' : ∀ (x : α), x ≠ a ∧ x ∈ d.support → (Finsupp.erase a d) x = 0
b : α
hb : ¬a = b
⊢ d b = 0
Tactic:
simp only [ne_eq, Finsupp.mem_support_iff, and_imp] at ha'
Proof state after:
case neg.a
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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
b : α
hb : ¬a = b
ha' : ∀ (x : α), ¬x = a → ¬d x = 0 → (Finsupp.erase a d) x = 0
⊢ d b = 0
Theorem: PolynomialMap.Finsupp.sum_eq_one_iff
Proof state before:
case neg.a
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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
ha✝ : ¬d a = 0
ha : d a = 1
b : α
hb : ¬a = b
ha' : ∀ (x : α), ¬x = a → ¬d x = 0 → (Finsupp.erase a d) x = 0
⊢ d b = 0
Tactic:
simpa only [Finsupp.erase_ne (ne_comm.mp hb), _root_.not_imp_self] using ha' b (ne_comm.mp hb)
Proof state after:
no goals
Theorem: PolynomialMap.Finsupp.sum_eq_one_iff
Proof state before:
case mpr
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
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
⊢ (∃ a, Finsupp.single a 1 = d) → (d.sum fun x n => n) = 1
Tactic:
rintro ⟨a, rfl⟩
Proof state after:
case mpr.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
α : Type u_3
inst✝ : DecidableEq α
a : α
⊢ ((Finsupp.single a 1).sum fun x n => n) = 1
Theorem: PolynomialMap.Finsupp.sum_eq_one_iff
Proof state before:
case mpr.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
α : Type u_3
inst✝ : DecidableEq α
a : α
⊢ ((Finsupp.single a 1).sum fun x n => n) = 1
Tactic:
rw [Finsupp.sum_eq_single a, Finsupp.single_eq_same]
Proof state after:
case mpr.intro.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
α : Type u_3
inst✝ : DecidableEq α
a : α
⊢ ∀ (b : α), (Finsupp.single a 1) b ≠ 0 → b ≠ a → (Finsupp.single a 1) b = 0

case mpr.intro.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
α : Type u_3
inst✝ : DecidableEq α
a : α
⊢ (Finsupp.single a 1) a = 0 → 0 = 0
Theorem: PolynomialMap.Finsupp.sum_eq_one_iff
Proof state before:
case mpr.intro.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
α : Type u_3
inst✝ : DecidableEq α
a : α
⊢ ∀ (b : α), (Finsupp.single a 1) b ≠ 0 → b ≠ a → (Finsupp.single a 1) b = 0

case mpr.intro.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
α : Type u_3
inst✝ : DecidableEq α
a : α
⊢ (Finsupp.single a 1) a = 0 → 0 = 0
Tactic:
intro b hb hb'
Proof state after:
case mpr.intro.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
α : Type u_3
inst✝ : DecidableEq α
a b : α
hb : (Finsupp.single a 1) b ≠ 0
hb' : b ≠ a
⊢ (Finsupp.single a 1) b = 0

case mpr.intro.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
α : Type u_3
inst✝ : DecidableEq α
a : α
⊢ (Finsupp.single a 1) a = 0 → 0 = 0
Theorem: PolynomialMap.Finsupp.sum_eq_one_iff
Proof state before:
case mpr.intro.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
α : Type u_3
inst✝ : DecidableEq α
a b : α
hb : (Finsupp.single a 1) b ≠ 0
hb' : b ≠ a
⊢ (Finsupp.single a 1) b = 0

case mpr.intro.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
α : Type u_3
inst✝ : DecidableEq α
a : α
⊢ (Finsupp.single a 1) a = 0 → 0 = 0
Tactic:
exfalso
Proof state after:
case mpr.intro.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
α : Type u_3
inst✝ : DecidableEq α
a b : α
hb : (Finsupp.single a 1) b ≠ 0
hb' : b ≠ a
⊢ False

case mpr.intro.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
α : Type u_3
inst✝ : DecidableEq α
a : α
⊢ (Finsupp.single a 1) a = 0 → 0 = 0
Theorem: PolynomialMap.Finsupp.sum_eq_one_iff
Proof state before:
case mpr.intro.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
α : Type u_3
inst✝ : DecidableEq α
a b : α
hb : (Finsupp.single a 1) b ≠ 0
hb' : b ≠ a
⊢ False

case mpr.intro.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
α : Type u_3
inst✝ : DecidableEq α
a : α
⊢ (Finsupp.single a 1) a = 0 → 0 = 0
Tactic:
apply hb
Proof state after:
case mpr.intro.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
α : Type u_3
inst✝ : DecidableEq α
a b : α
hb : (Finsupp.single a 1) b ≠ 0
hb' : b ≠ a
⊢ (Finsupp.single a 1) b = 0

case mpr.intro.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
α : Type u_3
inst✝ : DecidableEq α
a : α
⊢ (Finsupp.single a 1) a = 0 → 0 = 0
Theorem: PolynomialMap.Finsupp.sum_eq_one_iff
Proof state before:
case mpr.intro.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
α : Type u_3
inst✝ : DecidableEq α
a b : α
hb : (Finsupp.single a 1) b ≠ 0
hb' : b ≠ a
⊢ (Finsupp.single a 1) b = 0

case mpr.intro.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
α : Type u_3
inst✝ : DecidableEq α
a : α
⊢ (Finsupp.single a 1) a = 0 → 0 = 0
Tactic:
rw [Finsupp.single_eq_of_ne hb'.symm]
Proof state after:
case mpr.intro.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
α : Type u_3
inst✝ : DecidableEq α
a : α
⊢ (Finsupp.single a 1) a = 0 → 0 = 0
Theorem: PolynomialMap.Finsupp.sum_eq_one_iff
Proof state before:
case mpr.intro.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
α : Type u_3
inst✝ : DecidableEq α
a : α
⊢ (Finsupp.single a 1) a = 0 → 0 = 0
Tactic:
exact fun _ ↦ rfl
Proof state after:
no goals
Theorem: PolynomialMap.isHomogeneousOfDegreeOne_coeff_support_le
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
⊢ 1 ≠ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: PolynomialMap.isHomogeneousOfDegreeOne_coeff_support_le
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
⊢ ((coeff m) f).support ⊆ Finset.map { toFun := fun i => Finsupp.single i 1, inj' := ⋯ } univ
Tactic:
intro d hd
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
d : ι →₀ ℕ
hd : d ∈ ((coeff m) f).support
⊢ d ∈ Finset.map { toFun := fun i => Finsupp.single i 1, inj' := ⋯ } univ
Theorem: PolynomialMap.isHomogeneousOfDegreeOne_coeff_support_le
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
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
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
d : ι →₀ ℕ
hd : ¬((coeff m) f) d = 0
⊢ d ∈ Finset.map { toFun := fun i => Finsupp.single i 1, inj' := ⋯ } univ
Theorem: PolynomialMap.isHomogeneousOfDegreeOne_coeff_support_le
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
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
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
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
Theorem: PolynomialMap.isHomogeneousOfDegreeOne_coeff_support_le
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
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'
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 : ι
⊢ ((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']
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 : ι
⊢ ((coeff m) f) (Finsupp.single i 1) = (TensorProduct.lid R N) (f.toFun R (1 ⊗ₜ[R] m i))