Theorem: HTPI.csb_match_not_cri (HTPILib/Chap8Part2.lean)

State before:
U V : Type
R S : Rel U V
X0 : Set U
x : U
y : V
h1 : csb_match R S X0 x y
h2 : x ∉ cum_rep_image R S X0
⊢ S x y
Tactic:
by_cases on h1
State after:
case Case_1
U V : Type
R S : Rel U V
X0 : Set U
x : U
y : V
h2 : x ∉ cum_rep_image R S X0
h1 : x ∈ cum_rep_image R S X0 ∧ R x y
⊢ S x y

case Case_2
U V : Type
R S : Rel U V
X0 : Set U
x : U
y : V
h2 : x ∉ cum_rep_image R S X0
h1 : x ∉ cum_rep_image R S X0 ∧ S x y
⊢ S x y

State before:
case Case_1
U V : Type
R S : Rel U V
X0 : Set U
x : U
y : V
h2 : x ∉ cum_rep_image R S X0
h1 : x ∈ cum_rep_image R S X0 ∧ R x y
⊢ S x y
Tactic:
show S x y from absurd h1.left h2
State after:
no goals

State before:
case Case_2
U V : Type
R S : Rel U V
X0 : Set U
x : U
y : V
h2 : x ∉ cum_rep_image R S X0
h1 : x ∉ cum_rep_image R S X0 ∧ S x y
⊢ S x y
Tactic:
show S x y from h1.right
State after:
no goals