case h
α : Type u_1
β : Type ?u.40966
γ : Type ?u.40969
x y : α
⊢ IsDiag (Quotient.mk (Rel.setoid α) (x, y)) → Quotient.mk (Rel.setoid α) (x, y) ∈ Set.range diag
α : Type u_1
β : Type ?u.40966
γ : Type ?u.40969
z : Sym2 α
⊢ IsDiag z → z ∈ Set.range diag
induction' z using Sym2.ind with x y
case h
α : Type u_1
β : Type ?u.40966
γ : Type ?u.40969
x : α
⊢ Quotient.mk (Rel.setoid α) (x, x) ∈ Set.range diag
case h
α : Type u_1
β : Type ?u.40966
γ : Type ?u.40969
x y : α
⊢ IsDiag (Quotient.mk (Rel.setoid α) (x, y)) → Quotient.mk (Rel.setoid α) (x, y) ∈ Set.range diag
rintro (rfl : x = y)
no goals
case h
α : Type u_1
β : Type ?u.40966
γ : Type ?u.40969
x : α
⊢ Quotient.mk (Rel.setoid α) (x, x) ∈ Set.range diag
exact ⟨_, rfl⟩