case mp
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i j : ι
xi : β i
xj : β j
⊢ single i xi = single j xj → i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0

case mpr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i j : ι
xi : β i
xj : β j
⊢ i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0 → single i xi = single j xj
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i j : ι
xi : β i
xj : β j
⊢ single i xi = single j xj ↔ i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0
constructor
case mp
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
⊢ i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0
case mp
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i j : ι
xi : β i
xj : β j
⊢ single i xi = single j xj → i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0
intro h
case pos
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : i = j
⊢ i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0

case neg
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
⊢ i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0
case mp
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
⊢ i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0
by_cases hij : i = j
case pos
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i : ι
xi xj : β i
h : single i xi = single i xj
⊢ i = i ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0
case pos
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : i = j
⊢ i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0
subst hij
no goals
case pos
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i : ι
xi xj : β i
h : single i xi = single i xj
⊢ i = i ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0
exact Or.inl ⟨rfl, heq_of_eq (Dfinsupp.single_injective h)⟩
case neg
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
h_coe : ↑(single i xi) = ↑(single j xj)
⊢ i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0
case neg
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
⊢ i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0
have h_coe : ⇑(Dfinsupp.single i xi) = Dfinsupp.single j xj := congr_arg (⇑) h
case neg
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
h_coe : ↑(single i xi) = ↑(single j xj)
hci : ↑(single i xi) i = ↑(single j xj) i
⊢ i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0
case neg
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
h_coe : ↑(single i xi) = ↑(single j xj)
⊢ i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0
have hci := congr_fun h_coe i
case neg
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
h_coe : ↑(single i xi) = ↑(single j xj)
hci : ↑(single i xi) i = ↑(single j xj) i
hcj : ↑(single i xi) j = ↑(single j xj) j
⊢ i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0
case neg
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
h_coe : ↑(single i xi) = ↑(single j xj)
hci : ↑(single i xi) i = ↑(single j xj) i
⊢ i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0
have hcj := congr_fun h_coe j
case neg
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
h_coe : ↑(single i xi) = ↑(single j xj)
hci : xi = ↑(single j xj) i
hcj : ↑(single i xi) j = xj
⊢ i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0
case neg
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
h_coe : ↑(single i xi) = ↑(single j xj)
hci : ↑(single i xi) i = ↑(single j xj) i
hcj : ↑(single i xi) j = ↑(single j xj) j
⊢ i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0
rw [Dfinsupp.single_eq_same] at hci hcj
case neg
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
h_coe : ↑(single i xi) = ↑(single j xj)
hci : xi = 0
hcj : ↑(single i xi) j = xj
⊢ i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0
case neg
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
h_coe : ↑(single i xi) = ↑(single j xj)
hci : xi = ↑(single j xj) i
hcj : ↑(single i xi) j = xj
⊢ i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0
rw [Dfinsupp.single_eq_of_ne (Ne.symm hij)] at hci
case neg
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
h_coe : ↑(single i xi) = ↑(single j xj)
hci : xi = 0
hcj : 0 = xj
⊢ i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0
case neg
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
h_coe : ↑(single i xi) = ↑(single j xj)
hci : xi = 0
hcj : ↑(single i xi) j = xj
⊢ i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0
rw [Dfinsupp.single_eq_of_ne hij] at hcj
no goals
case neg
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
h_coe : ↑(single i xi) = ↑(single j xj)
hci : xi = 0
hcj : 0 = xj
⊢ i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0
exact Or.inr ⟨hci, hcj.symm⟩
case mpr.inl.intro
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i : ι
xi xj : β i
hxi : HEq xi xj
⊢ single i xi = single i xj

case mpr.inr.intro
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i j : ι
xi : β i
xj : β j
hi : xi = 0
hj : xj = 0
⊢ single i xi = single j xj
case mpr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i j : ι
xi : β i
xj : β j
⊢ i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0 → single i xi = single j xj
rintro (⟨rfl, hxi⟩ | ⟨hi, hj⟩)
no goals
case mpr.inl.intro
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i : ι
xi xj : β i
hxi : HEq xi xj
⊢ single i xi = single i xj
rw [eq_of_heq hxi]
no goals
case mpr.inr.intro
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i j : ι
xi : β i
xj : β j
hi : xi = 0
hj : xj = 0
⊢ single i xi = single j xj
rw [hi, hj, Dfinsupp.single_zero, Dfinsupp.single_zero]