α : Type u_1
β : Type ?u.41545
γ : Type ?u.41548
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
⊢ IsDiag z
α : Type u_1
β : Type ?u.41545
γ : Type ?u.41548
a : α
z : Sym2 α
hd : ¬IsDiag z
h : a ∈ z
⊢ Mem.other h ≠ a
contrapose! hd
α : Type u_1
β : Type ?u.41545
γ : Type ?u.41548
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
h' : Quotient.mk (Rel.setoid α) (a, Mem.other h) = z
⊢ IsDiag z
α : Type u_1
β : Type ?u.41545
γ : Type ?u.41548
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
⊢ IsDiag z
have h' := Sym2.other_spec h
α : Type u_1
β : Type ?u.41545
γ : Type ?u.41548
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
h' : Quotient.mk (Rel.setoid α) (a, a) = z
⊢ IsDiag z
α : Type u_1
β : Type ?u.41545
γ : Type ?u.41548
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
h' : Quotient.mk (Rel.setoid α) (a, Mem.other h) = z
⊢ IsDiag z
rw [hd] at h'
α : Type u_1
β : Type ?u.41545
γ : Type ?u.41548
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
h' : Quotient.mk (Rel.setoid α) (a, a) = z
⊢ IsDiag (Quotient.mk (Rel.setoid α) (a, a))
α : Type u_1
β : Type ?u.41545
γ : Type ?u.41548
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
h' : Quotient.mk (Rel.setoid α) (a, a) = z
⊢ IsDiag z
rw [← h']
no goals
α : Type u_1
β : Type ?u.41545
γ : Type ?u.41548
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
h' : Quotient.mk (Rel.setoid α) (a, a) = z
⊢ IsDiag (Quotient.mk (Rel.setoid α) (a, a))
simp