-- Mathlib/Data/Finsupp/Single.lean
theorem single_eq_single_iff (a₁ a₂ : α) (b₁ b₂ : M) :
    single a₁ b₁ = single a₂ b₂ ↔ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Proof state:
case mpr.inr.intro
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
⊢ single a₁ 0 = single a₂ 0

Tactic:
rw [single_zero, single_zero]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
⊢ single a₁ b₁ = single a₂ b₂ ↔ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Tactic:
constructor

Result:
case mp
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
⊢ single a₁ b₁ = single a₂ b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

case mpr
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0 → single a₁ b₁ = single a₂ b₂

Proof state:
case mpr
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0 → single a₁ b₁ = single a₂ b₂

Tactic:
rintro (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)

Result:
case mpr.inl.intro
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ : α
b₁ : M
⊢ single a₁ b₁ = single a₁ b₁

case mpr.inr.intro
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
⊢ single a₁ 0 = single a₂ 0

Proof state:
case neg
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : single a₁ b₁ = single a₂ b₂
h : ¬a₁ = a₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Tactic:
rw [DFunLike.ext_iff] at eq

Result:
case neg
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : ∀ (x : α), (single a₁ b₁) x = (single a₂ b₂) x
h : ¬a₁ = a₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Proof state:
case pos
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : single a₁ b₁ = single a₂ b₂
h : a₁ = a₂
⊢ b₁ = b₂

Tactic:
rwa [h, (single_injective a₂).eq_iff] at eq

Result:
no goals

Proof state:
case mpr.inl.intro
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ : α
b₁ : M
⊢ single a₁ b₁ = single a₁ b₁

Tactic:
rfl

Result:
no goals

Proof state:
case neg
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : ∀ (x : α), (single a₁ b₁) x = (single a₂ b₂) x
h : ¬a₁ = a₂
h₁ : (single a₁ b₁) a₁ = (single a₂ b₂) a₁
h₂ : (single a₁ b₁) a₂ = (single a₂ b₂) a₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Tactic:
simp only [single_eq_same, single_eq_of_ne h, single_eq_of_ne (Ne.symm h)] at h₁ h₂

Result:
case neg
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : ∀ (x : α), (single a₁ b₁) x = (single a₂ b₂) x
h : ¬a₁ = a₂
h₁ : b₁ = 0
h₂ : 0 = b₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Proof state:
case neg
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : ∀ (x : α), (single a₁ b₁) x = (single a₂ b₂) x
h : ¬a₁ = a₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Tactic:
have h₁ := eq a₁

Result:
case neg
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : ∀ (x : α), (single a₁ b₁) x = (single a₂ b₂) x
h : ¬a₁ = a₂
h₁ : (single a₁ b₁) a₁ = (single a₂ b₂) a₁
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Proof state:
case mp
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
⊢ single a₁ b₁ = single a₂ b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Tactic:
intro eq

Result:
case mp
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : single a₁ b₁ = single a₂ b₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Proof state:
case neg
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : ∀ (x : α), (single a₁ b₁) x = (single a₂ b₂) x
h : ¬a₁ = a₂
h₁ : (single a₁ b₁) a₁ = (single a₂ b₂) a₁
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Tactic:
have h₂ := eq a₂

Result:
case neg
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : ∀ (x : α), (single a₁ b₁) x = (single a₂ b₂) x
h : ¬a₁ = a₂
h₁ : (single a₁ b₁) a₁ = (single a₂ b₂) a₁
h₂ : (single a₁ b₁) a₂ = (single a₂ b₂) a₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Proof state:
case pos
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : single a₁ b₁ = single a₂ b₂
h : a₁ = a₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Tactic:
refine Or.inl ⟨h, ?_⟩

Result:
case pos
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : single a₁ b₁ = single a₂ b₂
h : a₁ = a₂
⊢ b₁ = b₂

Proof state:
case mp
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : single a₁ b₁ = single a₂ b₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Tactic:
by_cases h : a₁ = a₂

Result:
case pos
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : single a₁ b₁ = single a₂ b₂
h : a₁ = a₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

case neg
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : single a₁ b₁ = single a₂ b₂
h : ¬a₁ = a₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Proof state:
case neg
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : ∀ (x : α), (single a₁ b₁) x = (single a₂ b₂) x
h : ¬a₁ = a₂
h₁ : b₁ = 0
h₂ : 0 = b₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Tactic:
exact Or.inr ⟨h₁, h₂.symm⟩

Result:
no goals