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

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

State before:
A : Type
R : BinRel A
h : equiv_rel R
x : A
⊢ x ∈ equivClass R x
Tactic:
define
State after:
A : Type
R : BinRel A
h : equiv_rel R
x : A
⊢ R x x

State before:
A : Type
R : BinRel A
h : equiv_rel R
x : A
⊢ R x x
Tactic:
define at h
State after:
A : Type
R : BinRel A
h : reflexive R ∧ symmetric R ∧ transitive R
x : A
⊢ R x x

State before:
A : Type
R : BinRel A
h : reflexive R ∧ symmetric R ∧ transitive R
x : A
⊢ R x x
Tactic:
have Rref : reflexive R := h.left
State after:
A : Type
R : BinRel A
h : reflexive R ∧ symmetric R ∧ transitive R
x : A
Rref : reflexive R
⊢ R x x

State before:
A : Type
R : BinRel A
h : reflexive R ∧ symmetric R ∧ transitive R
x : A
Rref : reflexive R
⊢ R x x
Tactic:
show R x x from Rref x
State after:
no goals