Theorem: wedge_inc_refl_sym_trans (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) (wedge R) fun x x_1 => refl_trans_sym_clos R x x_1
Tactic:
intros x y wedge
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
wedge : _root_.wedge R x y
⊢ refl_trans_sym_clos R x y

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
wedge : _root_.wedge R x y
⊢ refl_trans_sym_clos R x y
Tactic:
cases' wedge with w h
State after:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h : refl_trans_clos R w x ∧ refl_trans_clos R w y
⊢ refl_trans_sym_clos R x y

State before:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h : refl_trans_clos R w x ∧ refl_trans_clos R w y
⊢ refl_trans_sym_clos R x y
Tactic:
cases' h with h1 h2
State after:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_sym_clos R x y

State before:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_sym_clos R x y
Tactic:
apply (refl_trans_sym_clos.trans _ w)
State after:
case intro.intro.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_sym_clos R x w

case intro.intro.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_sym_clos R w y

State before:
case intro.intro.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_sym_clos R x w

case intro.intro.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_sym_clos R w y
Tactic:
. apply refl_trans_sym_clos.inv
  apply refl_trans_sym_refl_trans; trivial
State after:
case intro.intro.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_sym_clos R w y

State before:
case intro.intro.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_sym_clos R w y
Tactic:
. apply refl_trans_sym_refl_trans; trivial
State after:
no goals

State before:
case intro.intro.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_sym_clos R x w
Tactic:
apply refl_trans_sym_clos.inv
State after:
case intro.intro.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_sym_clos R w x

State before:
case intro.intro.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_sym_clos R w x
Tactic:
apply refl_trans_sym_refl_trans
State after:
case intro.intro.a.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_clos R w x

State before:
case intro.intro.a.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_clos R w x
Tactic:
trivial
State after:
no goals

State before:
case intro.intro.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_sym_clos R w y
Tactic:
apply refl_trans_sym_refl_trans
State after:
case intro.intro.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_clos R w y

State before:
case intro.intro.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_clos R w y
Tactic:
trivial
State after:
no goals