case refine'_1
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a b c : α
h : IsNClique G 3 s
⊢ ∃ a b c, Adj G a b ∧ Adj G a c ∧ Adj G b c ∧ s = {a, b, c}

case refine'_2
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a b c : α
⊢ (∃ a b c, Adj G a b ∧ Adj G a c ∧ Adj G b c ∧ s = {a, b, c}) → IsNClique G 3 s
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a b c : α
⊢ IsNClique G 3 s ↔ ∃ a b c, Adj G a b ∧ Adj G a c ∧ Adj G b c ∧ s = {a, b, c}
refine' ⟨fun h ↦ _, _⟩
case refine'_1.intro.intro.intro.intro.intro.intro
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a✝ b✝ c✝ : α
h : IsNClique G 3 s
a b c : α
hs : s = {a, b, c}
⊢ ∃ a b c, Adj G a b ∧ Adj G a c ∧ Adj G b c ∧ s = {a, b, c}
case refine'_1
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a b c : α
h : IsNClique G 3 s
⊢ ∃ a b c, Adj G a b ∧ Adj G a c ∧ Adj G b c ∧ s = {a, b, c}
obtain ⟨a, b, c, -, -, -, hs⟩ := card_eq_three.1 h.card_eq
case refine'_1.intro.intro.intro.intro.intro.intro
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a✝ b✝ c✝ : α
h : IsNClique G 3 s
a b c : α
hs : s = {a, b, c}
⊢ Adj G a b ∧ Adj G a c ∧ Adj G b c ∧ s = {a, b, c}
case refine'_1.intro.intro.intro.intro.intro.intro
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a✝ b✝ c✝ : α
h : IsNClique G 3 s
a b c : α
hs : s = {a, b, c}
⊢ ∃ a b c, Adj G a b ∧ Adj G a c ∧ Adj G b c ∧ s = {a, b, c}
refine' ⟨a, b, c, _⟩
no goals
case refine'_1.intro.intro.intro.intro.intro.intro
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a✝ b✝ c✝ : α
h : IsNClique G 3 s
a b c : α
hs : s = {a, b, c}
⊢ Adj G a b ∧ Adj G a c ∧ Adj G b c ∧ s = {a, b, c}
rwa [hs, eq_self_iff_true, and_true, is3Clique_triple_iff.symm, ← hs]
case refine'_2.intro.intro.intro.intro.intro.intro
α : Type u_1
G H : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
a✝ b✝ c✝ a b c : α
hab : Adj G a b
hbc : Adj G a c
hca : Adj G b c
⊢ IsNClique G 3 {a, b, c}
case refine'_2
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a b c : α
⊢ (∃ a b c, Adj G a b ∧ Adj G a c ∧ Adj G b c ∧ s = {a, b, c}) → IsNClique G 3 s
rintro ⟨a, b, c, hab, hbc, hca, rfl⟩
no goals
case refine'_2.intro.intro.intro.intro.intro.intro
α : Type u_1
G H : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
a✝ b✝ c✝ a b c : α
hab : Adj G a b
hbc : Adj G a c
hca : Adj G b c
⊢ IsNClique G 3 {a, b, c}
exact is3Clique_triple_iff.2 ⟨hab, hbc, hca⟩