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

State before:
A : Type
R : BinRel A
h : equiv_rel R
⊢ ∀ (x : A), x ∈ ⋃₀ mod A R
Tactic:
fix x : A
State after:
A : Type
R : BinRel A
h : equiv_rel R
x : A
⊢ x ∈ ⋃₀ mod A R

State before:
A : Type
R : BinRel A
h : equiv_rel R
x : A
⊢ x ∈ ⋃₀ mod A R
Tactic:
define
State after:
A : Type
R : BinRel A
h : equiv_rel R
x : A
⊢ ∃ t ∈ mod A R, x ∈ t

State before:
A : Type
R : BinRel A
h : equiv_rel R
x : A
⊢ ∃ t ∈ mod A R, x ∈ t
Tactic:
apply Exists.intro (equivClass R x)
State after:
A : Type
R : BinRel A
h : equiv_rel R
x : A
⊢ equivClass R x ∈ mod A R ∧ x ∈ equivClass R x

State before:
A : Type
R : BinRel A
h : equiv_rel R
x : A
⊢ equivClass R x ∈ mod A R ∧ x ∈ equivClass R x
Tactic:
apply And.intro _ (Lemma_4_5_5_1 R h x)
State after:
A : Type
R : BinRel A
h : equiv_rel R
x : A
⊢ equivClass R x ∈ mod A R

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

State before:
A : Type
R : BinRel A
h : equiv_rel R
x : A
⊢ ∃ x_1, equivClass R x_1 = equivClass R x
Tactic:
apply Exists.intro x
State after:
A : Type
R : BinRel A
h : equiv_rel R
x : A
⊢ equivClass R x = equivClass R x

State before:
A : Type
R : BinRel A
h : equiv_rel R
x : A
⊢ equivClass R x = equivClass R x
Tactic:
rfl
State after:
no goals