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

State before:
A : Type
R : BinRel A
⊢ symmetric R ↔ extension R = inv (extension R)
Tactic:
apply Iff.intro
State after:
case mp
A : Type
R : BinRel A
⊢ symmetric R → extension R = inv (extension R)

case mpr
A : Type
R : BinRel A
⊢ extension R = inv (extension R) → symmetric R

State before:
case mp
A : Type
R : BinRel A
⊢ symmetric R → extension R = inv (extension R)
Tactic:
assume h1 : symmetric R
State after:
case mp
A : Type
R : BinRel A
h1 : symmetric R
⊢ extension R = inv (extension R)

State before:
case mp
A : Type
R : BinRel A
h1 : symmetric R
⊢ extension R = inv (extension R)
Tactic:
define at h1
State after:
case mp
A : Type
R : BinRel A
h1 : ∀ (x y : A), R x y → R y x
⊢ extension R = inv (extension R)

State before:
case mp
A : Type
R : BinRel A
h1 : ∀ (x y : A), R x y → R y x
⊢ extension R = inv (extension R)
Tactic:
apply Set.ext
State after:
case mp.h
A : Type
R : BinRel A
h1 : ∀ (x y : A), R x y → R y x
⊢ ∀ (x : A × A), x ∈ extension R ↔ x ∈ inv (extension R)

State before:
case mp.h
A : Type
R : BinRel A
h1 : ∀ (x y : A), R x y → R y x
⊢ ∀ (x : A × A), x ∈ extension R ↔ x ∈ inv (extension R)
Tactic:
fix (a, b) : A × A
State after:
case mp.h
A : Type
R : BinRel A
h1 : ∀ (x y : A), R x y → R y x
a b : A
⊢ (a, b) ∈ extension R ↔ (a, b) ∈ inv (extension R)

State before:
case mp.h
A : Type
R : BinRel A
h1 : ∀ (x y : A), R x y → R y x
a b : A
⊢ (a, b) ∈ extension R ↔ (a, b) ∈ inv (extension R)
Tactic:
show (a, b) ∈ extension R ↔ (a, b) ∈ inv (extension R) from
  calc (a, b) ∈ extension R
    _ ↔ R a b := by rfl
    _ ↔ R b a := Iff.intro (h1 a b) (h1 b a)
    _ ↔ (a, b) ∈ inv (extension R) := by rfl
State after:
no goals

State before:
A : Type
R : BinRel A
h1 : ∀ (x y : A), R x y → R y x
a b : A
⊢ (a, b) ∈ extension R ↔ R a b
Tactic:
rfl
State after:
no goals

State before:
A : Type
R : BinRel A
h1 : ∀ (x y : A), R x y → R y x
a b : A
⊢ R b a ↔ (a, b) ∈ inv (extension R)
Tactic:
rfl
State after:
no goals

State before:
case mpr
A : Type
R : BinRel A
⊢ extension R = inv (extension R) → symmetric R
Tactic:
assume h1 : extension R = inv (extension R)
State after:
case mpr
A : Type
R : BinRel A
h1 : extension R = inv (extension R)
⊢ symmetric R

State before:
case mpr
A : Type
R : BinRel A
h1 : extension R = inv (extension R)
⊢ symmetric R
Tactic:
define
State after:
case mpr
A : Type
R : BinRel A
h1 : extension R = inv (extension R)
⊢ ∀ (x y : A), R x y → R y x

State before:
case mpr
A : Type
R : BinRel A
h1 : extension R = inv (extension R)
⊢ ∀ (x y : A), R x y → R y x
Tactic:
fix a : A
State after:
case mpr
A : Type
R : BinRel A
h1 : extension R = inv (extension R)
a : A
⊢ ∀ (y : A), R a y → R y a

State before:
case mpr
A : Type
R : BinRel A
h1 : extension R = inv (extension R)
a : A
⊢ ∀ (y : A), R a y → R y a
Tactic:
fix b : A
State after:
case mpr
A : Type
R : BinRel A
h1 : extension R = inv (extension R)
a b : A
⊢ R a b → R b a

State before:
case mpr
A : Type
R : BinRel A
h1 : extension R = inv (extension R)
a b : A
⊢ R a b → R b a
Tactic:
assume h2 : R a b
State after:
case mpr
A : Type
R : BinRel A
h1 : extension R = inv (extension R)
a b : A
h2 : R a b
⊢ R b a

State before:
case mpr
A : Type
R : BinRel A
h1 : extension R = inv (extension R)
a b : A
h2 : R a b
⊢ R b a
Tactic:
rewrite [←ext_def R, h1, inv_def, ext_def] at h2
State after:
case mpr
A : Type
R : BinRel A
h1 : extension R = inv (extension R)
a b : A
h2 : R b a
⊢ R b a

State before:
case mpr
A : Type
R : BinRel A
h1 : extension R = inv (extension R)
a b : A
h2 : R b a
⊢ R b a
Tactic:
show R b a from h2
State after:
no goals