Theorem: HTPI.Theorem_4_5_4_part_3 (HTPILib/Chap4.lean)

State before:
A : Type
R : BinRel A
h : equiv_rel R
⊢ ∀ X ∈ mod A R, ¬empty X
Tactic:
fix X : Set A
State after:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
⊢ X ∈ mod A R → ¬empty X

State before:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
⊢ X ∈ mod A R → ¬empty X
Tactic:
assume h2 : X ∈ mod A R
State after:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : X ∈ mod A R
⊢ ¬empty X

State before:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : X ∈ mod A R
⊢ ¬empty X
Tactic:
define
State after:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : X ∈ mod A R
⊢ ¬¬∃ x, x ∈ X

State before:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : X ∈ mod A R
⊢ ¬¬∃ x, x ∈ X
Tactic:
double_neg
State after:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : X ∈ mod A R
⊢ ∃ x, x ∈ X

State before:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : X ∈ mod A R
⊢ ∃ x, x ∈ X
Tactic:
define at h2
State after:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
⊢ ∃ x, x ∈ X

State before:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
⊢ ∃ x, x ∈ X
Tactic:
obtain (x : A) (h3 : equivClass R x = X) from h2
State after:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
x : A
h3 : equivClass R x = X
⊢ ∃ x, x ∈ X

State before:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
x : A
h3 : equivClass R x = X
⊢ ∃ x, x ∈ X
Tactic:
rewrite [←h3]
State after:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
x : A
h3 : equivClass R x = X
⊢ ∃ x_1, x_1 ∈ equivClass R x

State before:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
x : A
h3 : equivClass R x = X
⊢ ∃ x_1, x_1 ∈ equivClass R x
Tactic:
show ∃ (x_1 : A), x_1 ∈ equivClass R x from
  Exists.intro x (Lemma_4_5_5_1 R h x)
State after:
no goals