Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case refine_2.inl.inl
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
b c : α
hbc : G.Adj b c
e : α
hde : G.Adj e e
hab : G.Adj e b
hac : G.Adj e c
⊢ s(e, e) = s(e, b) ∨ s(e, e) = s(e, c) ∨ s(e, e) = s(b, c)

pp: case refine_2.inl.inr.inl
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
c d e : α
hde : G.Adj d e
hac : G.Adj d c
hbc : G.Adj e c
hab : G.Adj d e
⊢ s(d, e) = s(d, e) ∨ s(d, e) = s(d, c) ∨ s(d, e) = s(e, c)

pp: case refine_2.inl.inr.inr
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
b d e : α
hde : G.Adj d e
hab : G.Adj d b
hbc : G.Adj b e
hac : G.Adj d e
⊢ s(d, e) = s(d, b) ∨ s(d, e) = s(d, e) ∨ s(d, e) = s(b, e)

pp: case refine_2.inr.inl.inl
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
c d e : α
hde : G.Adj d e
hbc : G.Adj d c
hac : G.Adj e c
hab : G.Adj e d
⊢ s(d, e) = s(e, d) ∨ s(d, e) = s(e, c) ∨ s(d, e) = s(d, c)

pp: case refine_2.inr.inl.inr.inl
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
a c : α
hac : G.Adj a c
e : α
hde : G.Adj e e
hab : G.Adj a e
hbc : G.Adj e c
⊢ s(e, e) = s(a, e) ∨ s(e, e) = s(a, c) ∨ s(e, e) = s(e, c)

pp: case refine_2.inr.inl.inr.inr
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
a d e : α
hde : G.Adj d e
hab : G.Adj a d
hac : G.Adj a e
hbc : G.Adj d e
⊢ s(d, e) = s(a, d) ∨ s(d, e) = s(a, e) ∨ s(d, e) = s(d, e)

pp: case refine_2.inr.inr.inl
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
b d e : α
hde : G.Adj d e
hbc : G.Adj b d
hab : G.Adj e b
hac : G.Adj e d
⊢ s(d, e) = s(e, b) ∨ s(d, e) = s(e, d) ∨ s(d, e) = s(b, d)

pp: case refine_2.inr.inr.inr.inl
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
a d e : α
hde : G.Adj d e
hac : G.Adj a d
hab : G.Adj a e
hbc : G.Adj e d
⊢ s(d, e) = s(a, e) ∨ s(d, e) = s(a, d) ∨ s(d, e) = s(e, d)

pp: case refine_2.inr.inr.inr.inr
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
a b : α
hab : G.Adj a b
e : α
hde : G.Adj e e
hac : G.Adj a e
hbc : G.Adj b e
⊢ s(e, e) = s(a, b) ∨ s(e, e) = s(a, e) ∨ s(e, e) = s(b, e)

Tactic:
<;>

Goal state after:
case refine_2.inl.inl
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
b c : α
hbc : G.Adj b c
e : α
hde : G.Adj e e
hab : G.Adj e b
hac : G.Adj e c
⊢ s(e, e) = s(e, b) ∨ s(e, e) = s(e, c) ∨ s(e, e) = s(b, c)

case refine_2.inl.inr.inl
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
c d e : α
hde : G.Adj d e
hac : G.Adj d c
hbc : G.Adj e c
hab : G.Adj d e
⊢ s(d, e) = s(d, e) ∨ s(d, e) = s(d, c) ∨ s(d, e) = s(e, c)

case refine_2.inl.inr.inr
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
b d e : α
hde : G.Adj d e
hab : G.Adj d b
hbc : G.Adj b e
hac : G.Adj d e
⊢ s(d, e) = s(d, b) ∨ s(d, e) = s(d, e) ∨ s(d, e) = s(b, e)

case refine_2.inr.inl.inl
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
c d e : α
hde : G.Adj d e
hbc : G.Adj d c
hac : G.Adj e c
hab : G.Adj e d
⊢ s(d, e) = s(e, d) ∨ s(d, e) = s(e, c) ∨ s(d, e) = s(d, c)

case refine_2.inr.inl.inr.inl
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
a c : α
hac : G.Adj a c
e : α
hde : G.Adj e e
hab : G.Adj a e
hbc : G.Adj e c
⊢ s(e, e) = s(a, e) ∨ s(e, e) = s(a, c) ∨ s(e, e) = s(e, c)

case refine_2.inr.inl.inr.inr
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
a d e : α
hde : G.Adj d e
hab : G.Adj a d
hac : G.Adj a e
hbc : G.Adj d e
⊢ s(d, e) = s(a, d) ∨ s(d, e) = s(a, e) ∨ s(d, e) = s(d, e)

case refine_2.inr.inr.inl
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
b d e : α
hde : G.Adj d e
hbc : G.Adj b d
hab : G.Adj e b
hac : G.Adj e d
⊢ s(d, e) = s(e, b) ∨ s(d, e) = s(e, d) ∨ s(d, e) = s(b, d)

case refine_2.inr.inr.inr.inl
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
a d e : α
hde : G.Adj d e
hac : G.Adj a d
hab : G.Adj a e
hbc : G.Adj e d
⊢ s(d, e) = s(a, e) ∨ s(d, e) = s(a, d) ∨ s(d, e) = s(e, d)

case refine_2.inr.inr.inr.inr
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
a b : α
hab : G.Adj a b
e : α
hde : G.Adj e e
hac : G.Adj a e
hbc : G.Adj b e
⊢ s(e, e) = s(a, b) ∨ s(e, e) = s(a, e) ∨ s(e, e) = s(b, e)