case a
α : Type u_1
β : Type ?u.118486
γ : Type ?u.118489
inst✝ : DecidableEq α
s : Finset α
z : Sym2 α
⊢ z ∈ filter (fun a => ¬IsDiag a) (image Quotient.mk'' (s ×ˢ s)) ↔ z ∈ image Quotient.mk'' (offDiag s)
α : Type u_1
β : Type ?u.118486
γ : Type ?u.118489
inst✝ : DecidableEq α
s : Finset α
⊢ filter (fun a => ¬IsDiag a) (image Quotient.mk'' (s ×ˢ s)) = image Quotient.mk'' (offDiag s)
ext z
case a.hf
α : Type u_1
β : Type ?u.118486
γ : Type ?u.118489
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ Quotient.mk (Rel.setoid α) (x✝, y✝) ∈ filter (fun a => ¬IsDiag a) (image Quotient.mk'' (s ×ˢ s)) ↔
    Quotient.mk (Rel.setoid α) (x✝, y✝) ∈ image Quotient.mk'' (offDiag s)
case a
α : Type u_1
β : Type ?u.118486
γ : Type ?u.118489
inst✝ : DecidableEq α
s : Finset α
z : Sym2 α
⊢ z ∈ filter (fun a => ¬IsDiag a) (image Quotient.mk'' (s ×ˢ s)) ↔ z ∈ image Quotient.mk'' (offDiag s)
induction z using Sym2.inductionOn
case a.hf
α : Type u_1
β : Type ?u.118486
γ : Type ?u.118489
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ (∃ a b, (a ∈ s ∧ b ∈ s) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) ∧
      ¬IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝)) ↔
    ∃ a b, (a ∈ s ∧ b ∈ s ∧ a ≠ b) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
case a.hf
α : Type u_1
β : Type ?u.118486
γ : Type ?u.118489
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ Quotient.mk (Rel.setoid α) (x✝, y✝) ∈ filter (fun a => ¬IsDiag a) (image Quotient.mk'' (s ×ˢ s)) ↔
    Quotient.mk (Rel.setoid α) (x✝, y✝) ∈ image Quotient.mk'' (offDiag s)
simp only [mem_image, mem_offDiag, mem_filter, Prod.exists, mem_product]
case a.hf.mp
α : Type u_1
β : Type ?u.118486
γ : Type ?u.118489
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ (∃ a b, (a ∈ s ∧ b ∈ s) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) ∧
      ¬IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝)) →
    ∃ a b, (a ∈ s ∧ b ∈ s ∧ a ≠ b) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)

case a.hf.mpr
α : Type u_1
β : Type ?u.118486
γ : Type ?u.118489
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ (∃ a b, (a ∈ s ∧ b ∈ s ∧ a ≠ b) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) →
    (∃ a b, (a ∈ s ∧ b ∈ s) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) ∧
      ¬IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝))
case a.hf
α : Type u_1
β : Type ?u.118486
γ : Type ?u.118489
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ (∃ a b, (a ∈ s ∧ b ∈ s) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) ∧
      ¬IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝)) ↔
    ∃ a b, (a ∈ s ∧ b ∈ s ∧ a ≠ b) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
constructor
case a.hf.mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.118486
γ : Type ?u.118489
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
hab : ¬IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝))
a b : α
h : Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
ha : a ∈ s
hb : b ∈ s
⊢ ∃ a b, (a ∈ s ∧ b ∈ s ∧ a ≠ b) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
case a.hf.mp
α : Type u_1
β : Type ?u.118486
γ : Type ?u.118489
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ (∃ a b, (a ∈ s ∧ b ∈ s) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) ∧
      ¬IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝)) →
    ∃ a b, (a ∈ s ∧ b ∈ s ∧ a ≠ b) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
rintro ⟨⟨a, b, ⟨ha, hb⟩, (h : Quotient.mk _ _ = _)⟩, hab⟩
case a.hf.mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.118486
γ : Type ?u.118489
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ a b : α
hab : ¬a = b
h : Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
ha : a ∈ s
hb : b ∈ s
⊢ ∃ a b, (a ∈ s ∧ b ∈ s ∧ a ≠ b) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
case a.hf.mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.118486
γ : Type ?u.118489
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
hab : ¬IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝))
a b : α
h : Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
ha : a ∈ s
hb : b ∈ s
⊢ ∃ a b, (a ∈ s ∧ b ∈ s ∧ a ≠ b) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
rw [← h, Sym2.mk''_isDiag_iff] at hab
no goals
case a.hf.mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.118486
γ : Type ?u.118489
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ a b : α
hab : ¬a = b
h : Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
ha : a ∈ s
hb : b ∈ s
⊢ ∃ a b, (a ∈ s ∧ b ∈ s ∧ a ≠ b) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
exact ⟨a, b, ⟨ha, hb, hab⟩, h⟩
case a.hf.mpr.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.118486
γ : Type ?u.118489
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ a b : α
h : Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
ha : a ∈ s
hb : b ∈ s
hab : a ≠ b
⊢ (∃ a b, (a ∈ s ∧ b ∈ s) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) ∧
    ¬IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝))
case a.hf.mpr
α : Type u_1
β : Type ?u.118486
γ : Type ?u.118489
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ (∃ a b, (a ∈ s ∧ b ∈ s ∧ a ≠ b) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) →
    (∃ a b, (a ∈ s ∧ b ∈ s) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) ∧
      ¬IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝))
rintro ⟨a, b, ⟨ha, hb, hab⟩, (h : Quotient.mk _ _ = _)⟩
case a.hf.mpr.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.118486
γ : Type ?u.118489
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ a b : α
h : Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
ha : a ∈ s
hb : b ∈ s
hab : ¬IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝))
⊢ (∃ a b, (a ∈ s ∧ b ∈ s) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) ∧
    ¬IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝))
case a.hf.mpr.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.118486
γ : Type ?u.118489
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ a b : α
h : Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
ha : a ∈ s
hb : b ∈ s
hab : a ≠ b
⊢ (∃ a b, (a ∈ s ∧ b ∈ s) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) ∧
    ¬IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝))
rw [Ne.def, ← Sym2.mk''_isDiag_iff, h] at hab
no goals
case a.hf.mpr.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.118486
γ : Type ?u.118489
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ a b : α
h : Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)
ha : a ∈ s
hb : b ∈ s
hab : ¬IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝))
⊢ (∃ a b, (a ∈ s ∧ b ∈ s) ∧ Quotient.mk'' (a, b) = Quotient.mk (Rel.setoid α) (x✝, y✝)) ∧
    ¬IsDiag (Quotient.mk (Rel.setoid α) (x✝, y✝))
exact ⟨⟨a, b, ⟨ha, hb⟩, h⟩, hab⟩