Theorem: trans_clos_idempotent (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ ∀ (R : A → A → Prop),
    (fun R R' => ∀ (x y : A), R x y ↔ R' x y) (refl_trans_clos (refl_trans_clos R)) (refl_trans_clos R)
Tactic:
simp
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ ∀ (R : A → A → Prop) (x y : A), refl_trans_clos (refl_trans_clos R) x y ↔ refl_trans_clos R x y

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ ∀ (R : A → A → Prop) (x y : A), refl_trans_clos (refl_trans_clos R) x y ↔ refl_trans_clos R x y
Tactic:
intros R x y
State after:
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y : A
⊢ refl_trans_clos (refl_trans_clos R) x y ↔ refl_trans_clos R x y

State before:
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y : A
⊢ refl_trans_clos (refl_trans_clos R) x y ↔ refl_trans_clos R x y
Tactic:
constructor <;> intros steps <;> induction' steps with z a b c red_a_c _red_b_c ih
State after:
case mp.refl
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y z : A
⊢ refl_trans_clos R z z

case mp.step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : refl_trans_clos R a b
_red_b_c : refl_trans_clos (refl_trans_clos R) b c
ih : refl_trans_clos R b c
⊢ refl_trans_clos R a c

case mpr.refl
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y z : A
⊢ refl_trans_clos (refl_trans_clos R) z z

case mpr.step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos (refl_trans_clos R) a c

State before:
case mp.refl
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y z : A
⊢ refl_trans_clos R z z

case mp.step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : refl_trans_clos R a b
_red_b_c : refl_trans_clos (refl_trans_clos R) b c
ih : refl_trans_clos R b c
⊢ refl_trans_clos R a c

case mpr.refl
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y z : A
⊢ refl_trans_clos (refl_trans_clos R) z z

case mpr.step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos (refl_trans_clos R) a c
Tactic:
. constructor
State after:
case mp.step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : refl_trans_clos R a b
_red_b_c : refl_trans_clos (refl_trans_clos R) b c
ih : refl_trans_clos R b c
⊢ refl_trans_clos R a c

case mpr.refl
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y z : A
⊢ refl_trans_clos (refl_trans_clos R) z z

case mpr.step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos (refl_trans_clos R) a c

State before:
case mp.step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : refl_trans_clos R a b
_red_b_c : refl_trans_clos (refl_trans_clos R) b c
ih : refl_trans_clos R b c
⊢ refl_trans_clos R a c

case mpr.refl
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y z : A
⊢ refl_trans_clos (refl_trans_clos R) z z

case mpr.step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos (refl_trans_clos R) a c
Tactic:
. apply refl_trans_clos_transitive <;> trivial
State after:
case mpr.refl
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y z : A
⊢ refl_trans_clos (refl_trans_clos R) z z

case mpr.step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos (refl_trans_clos R) a c

State before:
case mpr.refl
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y z : A
⊢ refl_trans_clos (refl_trans_clos R) z z

case mpr.step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos (refl_trans_clos R) a c
Tactic:
. constructor
State after:
case mpr.step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos (refl_trans_clos R) a c

State before:
case mpr.step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos (refl_trans_clos R) a c
Tactic:
. apply refl_trans_clos.step
  . apply refl_trans_clos.step; trivial
    constructor
  . trivial
State after:
no goals

State before:
case mp.refl
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y z : A
⊢ refl_trans_clos R z z
Tactic:
constructor
State after:
no goals

State before:
case mp.step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : refl_trans_clos R a b
_red_b_c : refl_trans_clos (refl_trans_clos R) b c
ih : refl_trans_clos R b c
⊢ refl_trans_clos R a c
Tactic:
apply refl_trans_clos_transitive <;> trivial
State after:
no goals

State before:
case mpr.refl
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y z : A
⊢ refl_trans_clos (refl_trans_clos R) z z
Tactic:
constructor
State after:
no goals

State before:
case mpr.step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos (refl_trans_clos R) a c
Tactic:
apply refl_trans_clos.step
State after:
case mpr.step.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos R a ?mpr.step.b

case mpr.step.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos (refl_trans_clos R) ?mpr.step.b c

case mpr.step.b
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ A

State before:
case mpr.step.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos R a ?mpr.step.b

case mpr.step.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos (refl_trans_clos R) ?mpr.step.b c

case mpr.step.b
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ A
Tactic:
. apply refl_trans_clos.step; trivial
  constructor
State after:
case mpr.step.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos (refl_trans_clos R) b c

State before:
case mpr.step.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos (refl_trans_clos R) b c
Tactic:
. trivial
State after:
no goals

State before:
case mpr.step.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos R a ?mpr.step.b
Tactic:
apply refl_trans_clos.step
State after:
case mpr.step.a.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ R a ?mpr.step.a.b

case mpr.step.a.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos R ?mpr.step.a.b ?mpr.step.b

case mpr.step.a.b
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ A

State before:
case mpr.step.a.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ R a ?mpr.step.a.b

case mpr.step.a.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos R ?mpr.step.a.b ?mpr.step.b

case mpr.step.a.b
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ A
Tactic:
trivial
State after:
case mpr.step.a.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos R b ?mpr.step.b

State before:
case mpr.step.a.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos R b ?mpr.step.b
Tactic:
constructor
State after:
no goals

State before:
case mpr.step.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos (refl_trans_clos R) b c
Tactic:
trivial
State after:
no goals