Theorem: refl_trans_sym_refl_trans (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ∀ (R : A → A → Prop), (fun R R' => ∀ (x y : A), R x y → R' x y) (refl_trans_clos R) (refl_trans_sym_clos R)
Tactic:
intros R x y red
State after:
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
R : A → A → Prop
x y : A
red : refl_trans_clos R x y
⊢ refl_trans_sym_clos R x y

State before:
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
R : A → A → Prop
x y : A
red : refl_trans_clos R x y
⊢ refl_trans_sym_clos R x y
Tactic:
induction red
State after:
case refl
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
R : A → A → Prop
x y a✝ : A
⊢ refl_trans_sym_clos R a✝ a✝

case step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
R : A → A → Prop
x y a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
a_ih✝ : refl_trans_sym_clos R b✝ c✝
⊢ refl_trans_sym_clos R a✝² c✝

State before:
case refl
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
R : A → A → Prop
x y a✝ : A
⊢ refl_trans_sym_clos R a✝ a✝

case step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
R : A → A → Prop
x y a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
a_ih✝ : refl_trans_sym_clos R b✝ c✝
⊢ refl_trans_sym_clos R a✝² c✝
Tactic:
constructor
State after:
case step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
R : A → A → Prop
x y a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
a_ih✝ : refl_trans_sym_clos R b✝ c✝
⊢ refl_trans_sym_clos R a✝² c✝

State before:
case step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
R : A → A → Prop
x y a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
a_ih✝ : refl_trans_sym_clos R b✝ c✝
⊢ refl_trans_sym_clos R a✝² c✝
Tactic:
apply refl_trans_sym_clos.trans <;> try trivial
State after:
case step.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
R : A → A → Prop
x y a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
a_ih✝ : refl_trans_sym_clos R b✝ c✝
⊢ refl_trans_sym_clos R a✝² b✝

State before:
case step.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
R : A → A → Prop
x y a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
a_ih✝ : refl_trans_sym_clos R b✝ c✝
⊢ refl_trans_sym_clos R a✝² b✝
Tactic:
aesop
State after:
no goals

State before:
case step.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
R : A → A → Prop
x y a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
a_ih✝ : refl_trans_sym_clos R b✝ c✝
⊢ refl_trans_sym_clos R ?step.b c✝
Tactic:
trivial
State after:
no goals