Theorem: HTPI.csb_match_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
⊢ R 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
⊢ R 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
⊢ R 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
⊢ R x y
Tactic:
show R x y from h1.right
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
⊢ R x y
Tactic:
show R x y from absurd h2 h1.left
State after:
no goals