Theorem: refl_trans_step_is_trans (Traat/chapter1.lean)

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

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x z y : A
red_x_z : R x z
red_z_y : refl_trans_clos R z y
⊢ trans_clos R x y
Tactic:
revert red_x_z x
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
z y : A
red_z_y : refl_trans_clos R z y
⊢ ∀ {x : A}, R x z → trans_clos R x y

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
z y : A
red_z_y : refl_trans_clos R z y
⊢ ∀ {x : A}, R x z → trans_clos R x y
Tactic:
induction red_z_y <;> aesop
State after:
no goals