case mp
α : Type u_1
β : Type ?u.55526
γ : Type ?u.55529
ι : Type ?u.55532
M : Type u_2
M' : Type ?u.55538
N : Type ?u.55541
P : Type ?u.55544
G : Type ?u.55547
H : Type ?u.55550
R : Type ?u.55553
S : Type ?u.55556
inst✝ : Zero M
a a' : α
b : 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
β : Type ?u.55526
γ : Type ?u.55529
ι : Type ?u.55532
M : Type u_2
M' : Type ?u.55538
N : Type ?u.55541
P : Type ?u.55544
G : Type ?u.55547
H : Type ?u.55550
R : Type ?u.55553
S : Type ?u.55556
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
b₁ b₂ : M
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0 → single a₁ b₁ = single a₂ b₂
α : Type u_1
β : Type ?u.55526
γ : Type ?u.55529
ι : Type ?u.55532
M : Type u_2
M' : Type ?u.55538
N : Type ?u.55541
P : Type ?u.55544
G : Type ?u.55547
H : Type ?u.55550
R : Type ?u.55553
S : Type ?u.55556
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
b₁ b₂ : M
⊢ single a₁ b₁ = single a₂ b₂ ↔ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
constructor
case mp
α : Type u_1
β : Type ?u.55526
γ : Type ?u.55529
ι : Type ?u.55532
M : Type u_2
M' : Type ?u.55538
N : Type ?u.55541
P : Type ?u.55544
G : Type ?u.55547
H : Type ?u.55550
R : Type ?u.55553
S : Type ?u.55556
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
b₁ b₂ : M
eq : single a₁ b₁ = single a₂ b₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
case mp
α : Type u_1
β : Type ?u.55526
γ : Type ?u.55529
ι : Type ?u.55532
M : Type u_2
M' : Type ?u.55538
N : Type ?u.55541
P : Type ?u.55544
G : Type ?u.55547
H : Type ?u.55550
R : Type ?u.55553
S : Type ?u.55556
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
b₁ b₂ : M
⊢ single a₁ b₁ = single a₂ b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
intro eq
case pos
α : Type u_1
β : Type ?u.55526
γ : Type ?u.55529
ι : Type ?u.55532
M : Type u_2
M' : Type ?u.55538
N : Type ?u.55541
P : Type ?u.55544
G : Type ?u.55547
H : Type ?u.55550
R : Type ?u.55553
S : Type ?u.55556
inst✝ : Zero M
a a' : α
b : 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
β : Type ?u.55526
γ : Type ?u.55529
ι : Type ?u.55532
M : Type u_2
M' : Type ?u.55538
N : Type ?u.55541
P : Type ?u.55544
G : Type ?u.55547
H : Type ?u.55550
R : Type ?u.55553
S : Type ?u.55556
inst✝ : Zero M
a a' : α
b : 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 mp
α : Type u_1
β : Type ?u.55526
γ : Type ?u.55529
ι : Type ?u.55532
M : Type u_2
M' : Type ?u.55538
N : Type ?u.55541
P : Type ?u.55544
G : Type ?u.55547
H : Type ?u.55550
R : Type ?u.55553
S : Type ?u.55556
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
b₁ b₂ : M
eq : single a₁ b₁ = single a₂ b₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
by_cases h : a₁ = a₂
case pos
α : Type u_1
β : Type ?u.55526
γ : Type ?u.55529
ι : Type ?u.55532
M : Type u_2
M' : Type ?u.55538
N : Type ?u.55541
P : Type ?u.55544
G : Type ?u.55547
H : Type ?u.55550
R : Type ?u.55553
S : Type ?u.55556
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
b₁ b₂ : M
eq : single a₁ b₁ = single a₂ b₂
h : a₁ = a₂
⊢ b₁ = b₂
case pos
α : Type u_1
β : Type ?u.55526
γ : Type ?u.55529
ι : Type ?u.55532
M : Type u_2
M' : Type ?u.55538
N : Type ?u.55541
P : Type ?u.55544
G : Type ?u.55547
H : Type ?u.55550
R : Type ?u.55553
S : Type ?u.55556
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
b₁ b₂ : M
eq : single a₁ b₁ = single a₂ b₂
h : a₁ = a₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
refine' Or.inl ⟨h, _⟩
no goals
case pos
α : Type u_1
β : Type ?u.55526
γ : Type ?u.55529
ι : Type ?u.55532
M : Type u_2
M' : Type ?u.55538
N : Type ?u.55541
P : Type ?u.55544
G : Type ?u.55547
H : Type ?u.55550
R : Type ?u.55553
S : Type ?u.55556
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
b₁ b₂ : M
eq : single a₁ b₁ = single a₂ b₂
h : a₁ = a₂
⊢ b₁ = b₂
rwa [h, (single_injective a₂).eq_iff] at eq
case neg
α : Type u_1
β : Type ?u.55526
γ : Type ?u.55529
ι : Type ?u.55532
M : Type u_2
M' : Type ?u.55538
N : Type ?u.55541
P : Type ?u.55544
G : Type ?u.55547
H : Type ?u.55550
R : Type ?u.55553
S : Type ?u.55556
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
b₁ b₂ : M
eq✝ : single a₁ b₁ = single a₂ b₂
eq : ∀ (x : α), ↑(single a₁ b₁) x = ↑(single a₂ b₂) x
h : ¬a₁ = a₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
case neg
α : Type u_1
β : Type ?u.55526
γ : Type ?u.55529
ι : Type ?u.55532
M : Type u_2
M' : Type ?u.55538
N : Type ?u.55541
P : Type ?u.55544
G : Type ?u.55547
H : Type ?u.55550
R : Type ?u.55553
S : Type ?u.55556
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
b₁ b₂ : M
eq : single a₁ b₁ = single a₂ b₂
h : ¬a₁ = a₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
rw [FunLike.ext_iff] at eq
case neg
α : Type u_1
β : Type ?u.55526
γ : Type ?u.55529
ι : Type ?u.55532
M : Type u_2
M' : Type ?u.55538
N : Type ?u.55541
P : Type ?u.55544
G : Type ?u.55547
H : Type ?u.55550
R : Type ?u.55553
S : Type ?u.55556
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
b₁ b₂ : M
eq✝ : single a₁ b₁ = single a₂ b₂
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
case neg
α : Type u_1
β : Type ?u.55526
γ : Type ?u.55529
ι : Type ?u.55532
M : Type u_2
M' : Type ?u.55538
N : Type ?u.55541
P : Type ?u.55544
G : Type ?u.55547
H : Type ?u.55550
R : Type ?u.55553
S : Type ?u.55556
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
b₁ b₂ : M
eq✝ : single a₁ b₁ = single a₂ b₂
eq : ∀ (x : α), ↑(single a₁ b₁) x = ↑(single a₂ b₂) x
h : ¬a₁ = a₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
have h₁ := eq a₁
case neg
α : Type u_1
β : Type ?u.55526
γ : Type ?u.55529
ι : Type ?u.55532
M : Type u_2
M' : Type ?u.55538
N : Type ?u.55541
P : Type ?u.55544
G : Type ?u.55547
H : Type ?u.55550
R : Type ?u.55553
S : Type ?u.55556
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
b₁ b₂ : M
eq✝ : single a₁ b₁ = single a₂ b₂
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
case neg
α : Type u_1
β : Type ?u.55526
γ : Type ?u.55529
ι : Type ?u.55532
M : Type u_2
M' : Type ?u.55538
N : Type ?u.55541
P : Type ?u.55544
G : Type ?u.55547
H : Type ?u.55550
R : Type ?u.55553
S : Type ?u.55556
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
b₁ b₂ : M
eq✝ : single a₁ b₁ = single a₂ b₂
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
have h₂ := eq a₂
case neg
α : Type u_1
β : Type ?u.55526
γ : Type ?u.55529
ι : Type ?u.55532
M : Type u_2
M' : Type ?u.55538
N : Type ?u.55541
P : Type ?u.55544
G : Type ?u.55547
H : Type ?u.55550
R : Type ?u.55553
S : Type ?u.55556
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
b₁ b₂ : M
eq✝ : single a₁ b₁ = single a₂ b₂
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
case neg
α : Type u_1
β : Type ?u.55526
γ : Type ?u.55529
ι : Type ?u.55532
M : Type u_2
M' : Type ?u.55538
N : Type ?u.55541
P : Type ?u.55544
G : Type ?u.55547
H : Type ?u.55550
R : Type ?u.55553
S : Type ?u.55556
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
b₁ b₂ : M
eq✝ : single a₁ b₁ = single a₂ b₂
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
simp only [single_eq_same, single_eq_of_ne h, single_eq_of_ne (Ne.symm h)] at h₁ h₂
no goals
case neg
α : Type u_1
β : Type ?u.55526
γ : Type ?u.55529
ι : Type ?u.55532
M : Type u_2
M' : Type ?u.55538
N : Type ?u.55541
P : Type ?u.55544
G : Type ?u.55547
H : Type ?u.55550
R : Type ?u.55553
S : Type ?u.55556
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
b₁ b₂ : M
eq✝ : single a₁ b₁ = single a₂ b₂
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
exact Or.inr ⟨h₁, h₂.symm⟩
case mpr.inl.intro
α : Type u_1
β : Type ?u.55526
γ : Type ?u.55529
ι : Type ?u.55532
M : Type u_2
M' : Type ?u.55538
N : Type ?u.55541
P : Type ?u.55544
G : Type ?u.55547
H : Type ?u.55550
R : Type ?u.55553
S : Type ?u.55556
inst✝ : Zero M
a a' : α
b : M
a₁ : α
b₁ : M
⊢ single a₁ b₁ = single a₁ b₁

case mpr.inr.intro
α : Type u_1
β : Type ?u.55526
γ : Type ?u.55529
ι : Type ?u.55532
M : Type u_2
M' : Type ?u.55538
N : Type ?u.55541
P : Type ?u.55544
G : Type ?u.55547
H : Type ?u.55550
R : Type ?u.55553
S : Type ?u.55556
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
⊢ single a₁ 0 = single a₂ 0
case mpr
α : Type u_1
β : Type ?u.55526
γ : Type ?u.55529
ι : Type ?u.55532
M : Type u_2
M' : Type ?u.55538
N : Type ?u.55541
P : Type ?u.55544
G : Type ?u.55547
H : Type ?u.55550
R : Type ?u.55553
S : Type ?u.55556
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
b₁ b₂ : M
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0 → single a₁ b₁ = single a₂ b₂
rintro (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)
no goals
case mpr.inl.intro
α : Type u_1
β : Type ?u.55526
γ : Type ?u.55529
ι : Type ?u.55532
M : Type u_2
M' : Type ?u.55538
N : Type ?u.55541
P : Type ?u.55544
G : Type ?u.55547
H : Type ?u.55550
R : Type ?u.55553
S : Type ?u.55556
inst✝ : Zero M
a a' : α
b : M
a₁ : α
b₁ : M
⊢ single a₁ b₁ = single a₁ b₁
rfl
no goals
case mpr.inr.intro
α : Type u_1
β : Type ?u.55526
γ : Type ?u.55529
ι : Type ?u.55532
M : Type u_2
M' : Type ?u.55538
N : Type ?u.55541
P : Type ?u.55544
G : Type ?u.55547
H : Type ?u.55550
R : Type ?u.55553
S : Type ?u.55556
inst✝ : Zero M
a a' : α
b : M
a₁ a₂ : α
⊢ single a₁ 0 = single a₂ 0
rw [single_zero, single_zero]