Theorem: refl_trans_clos_transitive (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
⊢ refl_trans_clos R x y → refl_trans_clos R y z → refl_trans_clos R x z
Tactic:
intros tr_x_y
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
tr_x_y : refl_trans_clos R x y
⊢ refl_trans_clos R y z → refl_trans_clos R x z

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
tr_x_y : refl_trans_clos R x y
⊢ refl_trans_clos R y z → refl_trans_clos R x z
Tactic:
induction tr_x_y <;> aesop
State after:
no goals