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

State before:
A : Type
R : BinRel A
h : equiv_rel R
⊢ ∀ (x y : A), y ∈ equivClass R x ↔ equivClass R y = equivClass R x
Tactic:
have Rsymm : symmetric R := h.right.left
State after:
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
⊢ ∀ (x y : A), y ∈ equivClass R x ↔ equivClass R y = equivClass R x

State before:
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
⊢ ∀ (x y : A), y ∈ equivClass R x ↔ equivClass R y = equivClass R x
Tactic:
have Rtrans : transitive R := h.right.right
State after:
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
⊢ ∀ (x y : A), y ∈ equivClass R x ↔ equivClass R y = equivClass R x

State before:
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
⊢ ∀ (x y : A), y ∈ equivClass R x ↔ equivClass R y = equivClass R x
Tactic:
fix x : A
State after:
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x : A
⊢ ∀ (y : A), y ∈ equivClass R x ↔ equivClass R y = equivClass R x

State before:
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x : A
⊢ ∀ (y : A), y ∈ equivClass R x ↔ equivClass R y = equivClass R x
Tactic:
fix y : A
State after:
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
⊢ y ∈ equivClass R x ↔ equivClass R y = equivClass R x

State before:
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
⊢ y ∈ equivClass R x ↔ equivClass R y = equivClass R x
Tactic:
apply Iff.intro
State after:
case mp
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
⊢ y ∈ equivClass R x → equivClass R y = equivClass R x

case mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
⊢ equivClass R y = equivClass R x → y ∈ equivClass R x

State before:
case mp
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
⊢ y ∈ equivClass R x → equivClass R y = equivClass R x
Tactic:
assume h2 :
  y ∈ equivClass R x
State after:
case mp
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : y ∈ equivClass R x
⊢ equivClass R y = equivClass R x

State before:
case mp
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : y ∈ equivClass R x
⊢ equivClass R y = equivClass R x
Tactic:
define at h2
State after:
case mp
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
⊢ equivClass R y = equivClass R x

State before:
case mp
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
⊢ equivClass R y = equivClass R x
Tactic:
apply Set.ext
State after:
case mp.h
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
⊢ ∀ (x_1 : A), x_1 ∈ equivClass R y ↔ x_1 ∈ equivClass R x

State before:
case mp.h
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
⊢ ∀ (x_1 : A), x_1 ∈ equivClass R y ↔ x_1 ∈ equivClass R x
Tactic:
fix z : A
State after:
case mp.h
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
⊢ z ∈ equivClass R y ↔ z ∈ equivClass R x

State before:
case mp.h
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
⊢ z ∈ equivClass R y ↔ z ∈ equivClass R x
Tactic:
apply Iff.intro
State after:
case mp.h.mp
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
⊢ z ∈ equivClass R y → z ∈ equivClass R x

case mp.h.mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
⊢ z ∈ equivClass R x → z ∈ equivClass R y

State before:
case mp.h.mp
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
⊢ z ∈ equivClass R y → z ∈ equivClass R x
Tactic:
assume h3 : z ∈ equivClass R y
State after:
case mp.h.mp
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
h3 : z ∈ equivClass R y
⊢ z ∈ equivClass R x

State before:
case mp.h.mp
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
h3 : z ∈ equivClass R y
⊢ z ∈ equivClass R x
Tactic:
define
State after:
case mp.h.mp
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
h3 : z ∈ equivClass R y
⊢ R z x

State before:
case mp.h.mp
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
h3 : z ∈ equivClass R y
⊢ R z x
Tactic:
define at h3
State after:
case mp.h.mp
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
h3 : R z y
⊢ R z x

State before:
case mp.h.mp
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
h3 : R z y
⊢ R z x
Tactic:
show R z x from Rtrans z y x h3 h2
State after:
no goals

State before:
case mp.h.mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
⊢ z ∈ equivClass R x → z ∈ equivClass R y
Tactic:
assume h3 : z ∈ equivClass R x
State after:
case mp.h.mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
h3 : z ∈ equivClass R x
⊢ z ∈ equivClass R y

State before:
case mp.h.mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
h3 : z ∈ equivClass R x
⊢ z ∈ equivClass R y
Tactic:
define
State after:
case mp.h.mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
h3 : z ∈ equivClass R x
⊢ R z y

State before:
case mp.h.mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
h3 : z ∈ equivClass R x
⊢ R z y
Tactic:
define at h3
State after:
case mp.h.mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
h3 : R z x
⊢ R z y

State before:
case mp.h.mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
h3 : R z x
⊢ R z y
Tactic:
have h4 : R x y := Rsymm y x h2
State after:
case mp.h.mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
h3 : R z x
h4 : R x y
⊢ R z y

State before:
case mp.h.mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : R y x
z : A
h3 : R z x
h4 : R x y
⊢ R z y
Tactic:
show R z y from Rtrans z x y h3 h4
State after:
no goals

State before:
case mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
⊢ equivClass R y = equivClass R x → y ∈ equivClass R x
Tactic:
assume h2 :
  equivClass R y = equivClass R x
State after:
case mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : equivClass R y = equivClass R x
⊢ y ∈ equivClass R x

State before:
case mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : equivClass R y = equivClass R x
⊢ y ∈ equivClass R x
Tactic:
rewrite [←h2]
State after:
case mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : equivClass R y = equivClass R x
⊢ y ∈ equivClass R y

State before:
case mpr
A : Type
R : BinRel A
h : equiv_rel R
Rsymm : symmetric R
Rtrans : transitive R
x y : A
h2 : equivClass R y = equivClass R x
⊢ y ∈ equivClass R y
Tactic:
show y ∈ equivClass R y from Lemma_4_5_5_1 R h y
State after:
no goals