Theorem: refl_trans_is_trans_or_eq (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
⊢ refl_trans_clos R x y → x = y ∨ trans_clos R x y
Tactic:
intros red
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
red : refl_trans_clos R x y
⊢ x = y ∨ trans_clos R x y

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
red : refl_trans_clos R x y
⊢ x = y ∨ trans_clos R x y
Tactic:
induction red <;> aesop
State after:
no goals