-- Mathlib/Data/DFinsupp/Defs.lean
theorem single_eq_single_iff (i j : ι) (xi : β i) (xj : β j) :
    DFinsupp.single i xi = DFinsupp.single j xj ↔ i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0

Proof state:
case pos
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i : ι
xi xj : β i
h : single i xi = single i xj
⊢ i = i ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0

Tactic:
exact Or.inl ⟨rfl, heq_of_eq (DFinsupp.single_injective h)⟩

Result:
no goals

Proof state:
case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
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

Tactic:
exact Or.inr ⟨hci, hcj.symm⟩

Result:
no goals

Proof state:
case mp
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
⊢ single i xi = single j xj → i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0

Tactic:
intro h

Result:
case mp
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
⊢ i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0

Proof state:
case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
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

Tactic:
have hcj := congr_fun h_coe j

Result:
case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
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

Proof state:
case pos
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
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

Tactic:
subst hij

Result:
case pos
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i : ι
xi xj : β i
h : single i xi = single i xj
⊢ i = i ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0

Proof state:
case mpr
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
⊢ i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0 → single i xi = single j xj

Tactic:
rintro (⟨rfl, hxi⟩ | ⟨hi, hj⟩)

Result:
case mpr.inl.intro
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i : ι
xi xj : β i
hxi : HEq xi xj
⊢ single i xi = single i xj

case mpr.inr.intro
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
hi : xi = 0
hj : xj = 0
⊢ single i xi = single j xj

Proof state:
case mpr.inl.intro
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i : ι
xi xj : β i
hxi : HEq xi xj
⊢ single i xi = single i xj

Tactic:
rw [eq_of_heq hxi]

Result:
no goals

Proof state:
case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
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

Tactic:
rw [DFinsupp.single_eq_of_ne (Ne.symm hij)] at hci

Result:
case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
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

Proof state:
case mp
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
⊢ i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0

Tactic:
by_cases hij : i = j

Result:
case pos
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
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 v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
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

Proof state:
case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
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

Tactic:
rw [DFinsupp.single_eq_of_ne hij] at hcj

Result:
case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
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

Proof state:
case mpr.inr.intro
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
hi : xi = 0
hj : xj = 0
⊢ single i xi = single j xj

Tactic:
rw [hi, hj, DFinsupp.single_zero, DFinsupp.single_zero]

Result:
no goals

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
⊢ single i xi = single j xj ↔ i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0

Tactic:
constructor

Result:
case mp
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
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 v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
⊢ i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0 → single i xi = single j xj

Proof state:
case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
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

Tactic:
have hci := congr_fun h_coe i

Result:
case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
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

Proof state:
case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
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

Tactic:
rw [DFinsupp.single_eq_same] at hci hcj

Result:
case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
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

Proof state:
case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
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

Tactic:
have h_coe : ⇑(DFinsupp.single i xi) = DFinsupp.single j xj := congr_arg (⇑) h

Result:
case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
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