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

State before:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : x1 ∈ cum_rep_image R S X0
⊢ x2 ∈ cum_rep_image R S X0
Tactic:
have h4 : R x1 y := csb_match_cri h1 h3
State after:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : x1 ∈ cum_rep_image R S X0
h4 : R x1 y
⊢ x2 ∈ cum_rep_image R S X0

State before:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : x1 ∈ cum_rep_image R S X0
h4 : R x1 y
⊢ x2 ∈ cum_rep_image R S X0
Tactic:
by_contra h5
State after:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : x1 ∈ cum_rep_image R S X0
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
⊢ False

State before:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : x1 ∈ cum_rep_image R S X0
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
⊢ False
Tactic:
have h6 : S x2 y := csb_match_not_cri h2 h5
State after:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : x1 ∈ cum_rep_image R S X0
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
⊢ False

State before:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : x1 ∈ cum_rep_image R S X0
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
⊢ False
Tactic:
contradict h5
State after:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : x1 ∈ cum_rep_image R S X0
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
⊢ x2 ∈ cum_rep_image R S X0

State before:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : x1 ∈ cum_rep_image R S X0
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
⊢ x2 ∈ cum_rep_image R S X0
Tactic:
define at h3
State after:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : ∃ n, x1 ∈ rep_common_image R S X0 n
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
⊢ x2 ∈ cum_rep_image R S X0

State before:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : ∃ n, x1 ∈ rep_common_image R S X0 n
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
⊢ x2 ∈ cum_rep_image R S X0
Tactic:
define
State after:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : ∃ n, x1 ∈ rep_common_image R S X0 n
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
⊢ ∃ n, x2 ∈ rep_common_image R S X0 n

State before:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : ∃ n, x1 ∈ rep_common_image R S X0 n
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
⊢ ∃ n, x2 ∈ rep_common_image R S X0 n
Tactic:
obtain (n : Nat) (h7 : x1 ∈ rep_common_image R S X0 n) from h3
State after:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : ∃ n, x1 ∈ rep_common_image R S X0 n
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
n : ℕ
h7 : x1 ∈ rep_common_image R S X0 n
⊢ ∃ n, x2 ∈ rep_common_image R S X0 n

State before:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : ∃ n, x1 ∈ rep_common_image R S X0 n
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
n : ℕ
h7 : x1 ∈ rep_common_image R S X0 n
⊢ ∃ n, x2 ∈ rep_common_image R S X0 n
Tactic:
apply Exists.intro (n + 1)
State after:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : ∃ n, x1 ∈ rep_common_image R S X0 n
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
n : ℕ
h7 : x1 ∈ rep_common_image R S X0 n
⊢ x2 ∈ rep_common_image R S X0 (n + 1)

State before:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : ∃ n, x1 ∈ rep_common_image R S X0 n
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
n : ℕ
h7 : x1 ∈ rep_common_image R S X0 n
⊢ x2 ∈ rep_common_image R S X0 (n + 1)
Tactic:
rewrite [rep_common_image_step]
State after:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : ∃ n, x1 ∈ rep_common_image R S X0 n
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
n : ℕ
h7 : x1 ∈ rep_common_image R S X0 n
⊢ ∃ x ∈ rep_common_image R S X0 n, ∃ y, R x y ∧ S x2 y

State before:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : ∃ n, x1 ∈ rep_common_image R S X0 n
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
n : ℕ
h7 : x1 ∈ rep_common_image R S X0 n
⊢ ∃ x ∈ rep_common_image R S X0 n, ∃ y, R x y ∧ S x2 y
Tactic:
apply Exists.intro x1
State after:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : ∃ n, x1 ∈ rep_common_image R S X0 n
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
n : ℕ
h7 : x1 ∈ rep_common_image R S X0 n
⊢ x1 ∈ rep_common_image R S X0 n ∧ ∃ y, R x1 y ∧ S x2 y

State before:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : ∃ n, x1 ∈ rep_common_image R S X0 n
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
n : ℕ
h7 : x1 ∈ rep_common_image R S X0 n
⊢ x1 ∈ rep_common_image R S X0 n ∧ ∃ y, R x1 y ∧ S x2 y
Tactic:
apply And.intro h7
State after:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : ∃ n, x1 ∈ rep_common_image R S X0 n
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
n : ℕ
h7 : x1 ∈ rep_common_image R S X0 n
⊢ ∃ y, R x1 y ∧ S x2 y

State before:
U V : Type
R S : Rel U V
X0 : Set U
x1 x2 : U
y : V
h1 : csb_match R S X0 x1 y
h2 : csb_match R S X0 x2 y
h3 : ∃ n, x1 ∈ rep_common_image R S X0 n
h4 : R x1 y
h5 : ¬x2 ∈ cum_rep_image R S X0
h6 : S x2 y
n : ℕ
h7 : x1 ∈ rep_common_image R S X0 n
⊢ ∃ y, R x1 y ∧ S x2 y
Tactic:
show ∃ (y : V), R x1 y ∧ S x2 y from Exists.intro y (And.intro h4 h6)
State after:
no goals