Theorem: refl_trans_sym_is_trans_sym_refl (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ (fun R R' => ∀ (x y : A), R x y ↔ R' x y) (refl_clos (trans_clos (sym_clos R))) (trans_clos (sym_clos (refl_clos R)))
Tactic:
apply both_inclusions <;> intros
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ trans_clos (sym_clos (refl_clos R)) x✝ y✝

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ refl_clos (trans_clos (sym_clos R)) x✝ y✝

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ trans_clos (sym_clos (refl_clos R)) x✝ y✝

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ refl_clos (trans_clos (sym_clos R)) x✝ y✝
Tactic:
. apply trans_clos_monotone
  . intros
    apply (refl_sym_is_sym_refl _ _ _).1
    trivial
  . apply (refl_trans_is_trans_refl _ _ _).1
    trivial
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ refl_clos (trans_clos (sym_clos R)) x✝ y✝

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ refl_clos (trans_clos (sym_clos R)) x✝ y✝
Tactic:
. apply (refl_trans_is_trans_refl _ _ _).2
  apply trans_clos_monotone
  . intros x y red
    apply  (refl_sym_is_sym_refl _ _ _).2
    trivial
  . trivial
State after:
no goals

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ trans_clos (sym_clos (refl_clos R)) x✝ y✝
Tactic:
apply trans_clos_monotone
State after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ ∀ (x y : A), ?a.R✝ x y → sym_clos (refl_clos R) x y

case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ trans_clos ?a.R✝ x✝ y✝

case a.R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ A → A → Prop

State before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ ∀ (x y : A), ?a.R✝ x y → sym_clos (refl_clos R) x y

case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ trans_clos ?a.R✝ x✝ y✝

case a.R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ A → A → Prop
Tactic:
. intros
  apply (refl_sym_is_sym_refl _ _ _).1
  trivial
State after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ trans_clos (fun x y => refl_clos (sym_clos R) x y) x✝ y✝

State before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ trans_clos (fun x y => refl_clos (sym_clos R) x y) x✝ y✝
Tactic:
. apply (refl_trans_is_trans_refl _ _ _).1
  trivial
State after:
no goals

State before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ ∀ (x y : A), ?a.R✝ x y → sym_clos (refl_clos R) x y
Tactic:
intros
State after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝¹ y✝¹ : A
a✝¹ : refl_clos (trans_clos (sym_clos R)) x✝¹ y✝¹
x✝ y✝ : A
a✝ : ?a.R✝ x✝ y✝
⊢ sym_clos (refl_clos R) x✝ y✝

State before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝¹ y✝¹ : A
a✝¹ : refl_clos (trans_clos (sym_clos R)) x✝¹ y✝¹
x✝ y✝ : A
a✝ : ?a.R✝ x✝ y✝
⊢ sym_clos (refl_clos R) x✝ y✝
Tactic:
apply (refl_sym_is_sym_refl _ _ _).1
State after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝¹ y✝¹ : A
a✝¹ : refl_clos (trans_clos (sym_clos R)) x✝¹ y✝¹
x✝ y✝ : A
a✝ : ?a.R✝ x✝ y✝
⊢ refl_clos (sym_clos R) x✝ y✝

State before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝¹ y✝¹ : A
a✝¹ : refl_clos (trans_clos (sym_clos R)) x✝¹ y✝¹
x✝ y✝ : A
a✝ : ?a.R✝ x✝ y✝
⊢ refl_clos (sym_clos R) x✝ y✝
Tactic:
trivial
State after:
no goals

State before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ trans_clos (fun x y => refl_clos (sym_clos R) x y) x✝ y✝
Tactic:
apply (refl_trans_is_trans_refl _ _ _).1
State after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ refl_clos (trans_clos (sym_clos R)) x✝ y✝

State before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ refl_clos (trans_clos (sym_clos R)) x✝ y✝
Tactic:
trivial
State after:
no goals

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ refl_clos (trans_clos (sym_clos R)) x✝ y✝
Tactic:
apply (refl_trans_is_trans_refl _ _ _).2
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ trans_clos (refl_clos (sym_clos R)) x✝ y✝

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ trans_clos (refl_clos (sym_clos R)) x✝ y✝
Tactic:
apply trans_clos_monotone
State after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ ∀ (x y : A), ?a.R✝ x y → refl_clos (sym_clos R) x y

case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ trans_clos ?a.R✝ x✝ y✝

case a.R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ A → A → Prop

State before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ ∀ (x y : A), ?a.R✝ x y → refl_clos (sym_clos R) x y

case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ trans_clos ?a.R✝ x✝ y✝

case a.R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ A → A → Prop
Tactic:
. intros x y red
  apply  (refl_sym_is_sym_refl _ _ _).2
  trivial
State after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ trans_clos (fun x y => sym_clos (refl_clos R) x y) x✝ y✝

State before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ trans_clos (fun x y => sym_clos (refl_clos R) x y) x✝ y✝
Tactic:
. trivial
State after:
no goals

State before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ ∀ (x y : A), ?a.R✝ x y → refl_clos (sym_clos R) x y
Tactic:
intros x y red
State after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
x y : A
red : ?a.R✝ x y
⊢ refl_clos (sym_clos R) x y

State before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
x y : A
red : ?a.R✝ x y
⊢ refl_clos (sym_clos R) x y
Tactic:
apply  (refl_sym_is_sym_refl _ _ _).2
State after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
x y : A
red : ?a.R✝ x y
⊢ sym_clos (refl_clos R) x y

State before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
x y : A
red : ?a.R✝ x y
⊢ sym_clos (refl_clos R) x y
Tactic:
trivial
State after:
no goals

State before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ trans_clos (fun x y => sym_clos (refl_clos R) x y) x✝ y✝
Tactic:
trivial
State after:
no goals