Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case mp.refine_1
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG : G.EdgeDisjointTriangles
a b : α
hab✝ : ¬a = b
hab : G.Adj (a, b).1 (a, b).2
c : α
hac : G.Adj (a, b).1 c
hbc : G.Adj (a, b).2 c
d : α
had : G.Adj (a, b).1 d
hbd : G.Adj (a, b).2 d
⊢ {(a, b).1, (a, b).2, c} ∈ G.cliqueSet 3

pp: case mp.refine_2
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG : G.EdgeDisjointTriangles
a b : α
hab✝ : ¬a = b
hab : G.Adj (a, b).1 (a, b).2
c : α
hac : G.Adj (a, b).1 c
hbc : G.Adj (a, b).2 c
d : α
had : G.Adj (a, b).1 d
hbd : G.Adj (a, b).2 d
⊢ {(a, b).1, (a, b).2, d} ∈ G.cliqueSet 3

pp: case mp.refine_3
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG : G.EdgeDisjointTriangles
a b : α
hab✝ : ¬a = b
hab : G.Adj (a, b).1 (a, b).2
c : α
hac : G.Adj (a, b).1 c
hbc : G.Adj (a, b).2 c
d : α
had : G.Adj (a, b).1 d
hbd : G.Adj (a, b).2 d
⊢ a ∈ ↑{(a, b).1, (a, b).2, c} ∩ ↑{(a, b).1, (a, b).2, d}

pp: case mp.refine_4
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG : G.EdgeDisjointTriangles
a b : α
hab✝ : ¬a = b
hab : G.Adj (a, b).1 (a, b).2
c : α
hac : G.Adj (a, b).1 c
hbc : G.Adj (a, b).2 c
d : α
had : G.Adj (a, b).1 d
hbd : G.Adj (a, b).2 d
⊢ b ∈ ↑{(a, b).1, (a, b).2, c} ∩ ↑{(a, b).1, (a, b).2, d}

Tactic:
<;>

Goal state after:
case mp.refine_1
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG : G.EdgeDisjointTriangles
a b : α
hab✝ : ¬a = b
hab : G.Adj (a, b).1 (a, b).2
c : α
hac : G.Adj (a, b).1 c
hbc : G.Adj (a, b).2 c
d : α
had : G.Adj (a, b).1 d
hbd : G.Adj (a, b).2 d
⊢ {(a, b).1, (a, b).2, c} ∈ G.cliqueSet 3

case mp.refine_2
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG : G.EdgeDisjointTriangles
a b : α
hab✝ : ¬a = b
hab : G.Adj (a, b).1 (a, b).2
c : α
hac : G.Adj (a, b).1 c
hbc : G.Adj (a, b).2 c
d : α
had : G.Adj (a, b).1 d
hbd : G.Adj (a, b).2 d
⊢ {(a, b).1, (a, b).2, d} ∈ G.cliqueSet 3

case mp.refine_3
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG : G.EdgeDisjointTriangles
a b : α
hab✝ : ¬a = b
hab : G.Adj (a, b).1 (a, b).2
c : α
hac : G.Adj (a, b).1 c
hbc : G.Adj (a, b).2 c
d : α
had : G.Adj (a, b).1 d
hbd : G.Adj (a, b).2 d
⊢ a ∈ ↑{(a, b).1, (a, b).2, c} ∩ ↑{(a, b).1, (a, b).2, d}

case mp.refine_4
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG : G.EdgeDisjointTriangles
a b : α
hab✝ : ¬a = b
hab : G.Adj (a, b).1 (a, b).2
c : α
hac : G.Adj (a, b).1 c
hbc : G.Adj (a, b).2 c
d : α
had : G.Adj (a, b).1 d
hbd : G.Adj (a, b).2 d
⊢ b ∈ ↑{(a, b).1, (a, b).2, c} ∩ ↑{(a, b).1, (a, b).2, d}