Theorem: refl_trans_is_trans_refl (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) (refl_clos (trans_clos R)) (trans_clos (refl_clos R))
Tactic:
apply both_inclusions <;> intros x y hyp
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
hyp : refl_clos (trans_clos R) x y
⊢ trans_clos (refl_clos R) x y

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
hyp : trans_clos (refl_clos R) x y
⊢ refl_clos (trans_clos R) x y

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
hyp : refl_clos (trans_clos R) x y
⊢ trans_clos (refl_clos R) x y

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
hyp : trans_clos (refl_clos R) x y
⊢ refl_clos (trans_clos R) x y
Tactic:
. cases hyp
  . aesop
  . apply trans_clos_monotone R <;> aesop
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
hyp : trans_clos (refl_clos R) x y
⊢ refl_clos (trans_clos R) x y

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
hyp : trans_clos (refl_clos R) x y
⊢ refl_clos (trans_clos R) x y
Tactic:
. induction' hyp with _ _ rc _ _ _ rc step ih
  . cases rc <;> aesop
  . cases rc; trivial
    apply refl_clos.base; aesop
State after:
no goals

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
hyp : refl_clos (trans_clos R) x y
⊢ trans_clos (refl_clos R) x y
Tactic:
cases hyp
State after:
case a.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
⊢ trans_clos (refl_clos R) x x

case a.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
a✝ : trans_clos R x y
⊢ trans_clos (refl_clos R) x y

State before:
case a.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
⊢ trans_clos (refl_clos R) x x

case a.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
a✝ : trans_clos R x y
⊢ trans_clos (refl_clos R) x y
Tactic:
. aesop
State after:
case a.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
a✝ : trans_clos R x y
⊢ trans_clos (refl_clos R) x y

State before:
case a.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
a✝ : trans_clos R x y
⊢ trans_clos (refl_clos R) x y
Tactic:
. apply trans_clos_monotone R <;> aesop
State after:
no goals

State before:
case a.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
⊢ trans_clos (refl_clos R) x x
Tactic:
aesop
State after:
no goals

State before:
case a.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
a✝ : trans_clos R x y
⊢ trans_clos (refl_clos R) x y
Tactic:
apply trans_clos_monotone R <;> aesop
State after:
no goals

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
hyp : trans_clos (refl_clos R) x y
⊢ refl_clos (trans_clos R) x y
Tactic:
induction' hyp with _ _ rc _ _ _ rc step ih
State after:
case a.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝ b✝ : A
rc : refl_clos R a✝ b✝
⊢ refl_clos (trans_clos R) a✝ b✝

case a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝ b✝ c✝ : A
rc : refl_clos R a✝ b✝
step : trans_clos (refl_clos R) b✝ c✝
ih : refl_clos (trans_clos R) b✝ c✝
⊢ refl_clos (trans_clos R) a✝ c✝

State before:
case a.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝ b✝ : A
rc : refl_clos R a✝ b✝
⊢ refl_clos (trans_clos R) a✝ b✝

case a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝ b✝ c✝ : A
rc : refl_clos R a✝ b✝
step : trans_clos (refl_clos R) b✝ c✝
ih : refl_clos (trans_clos R) b✝ c✝
⊢ refl_clos (trans_clos R) a✝ c✝
Tactic:
. cases rc <;> aesop
State after:
case a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝ b✝ c✝ : A
rc : refl_clos R a✝ b✝
step : trans_clos (refl_clos R) b✝ c✝
ih : refl_clos (trans_clos R) b✝ c✝
⊢ refl_clos (trans_clos R) a✝ c✝

State before:
case a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝ b✝ c✝ : A
rc : refl_clos R a✝ b✝
step : trans_clos (refl_clos R) b✝ c✝
ih : refl_clos (trans_clos R) b✝ c✝
⊢ refl_clos (trans_clos R) a✝ c✝
Tactic:
. cases rc; trivial
  apply refl_clos.base; aesop
State after:
no goals

State before:
case a.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝ b✝ : A
rc : refl_clos R a✝ b✝
⊢ refl_clos (trans_clos R) a✝ b✝
Tactic:
cases rc <;> aesop
State after:
no goals

State before:
case a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝ b✝ c✝ : A
rc : refl_clos R a✝ b✝
step : trans_clos (refl_clos R) b✝ c✝
ih : refl_clos (trans_clos R) b✝ c✝
⊢ refl_clos (trans_clos R) a✝ c✝
Tactic:
cases rc
State after:
case a.step.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝ c✝ : A
step : trans_clos (refl_clos R) a✝ c✝
ih : refl_clos (trans_clos R) a✝ c✝
⊢ refl_clos (trans_clos R) a✝ c✝

case a.step.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝¹ b✝ c✝ : A
step : trans_clos (refl_clos R) b✝ c✝
ih : refl_clos (trans_clos R) b✝ c✝
a✝ : R a✝¹ b✝
⊢ refl_clos (trans_clos R) a✝¹ c✝

State before:
case a.step.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝ c✝ : A
step : trans_clos (refl_clos R) a✝ c✝
ih : refl_clos (trans_clos R) a✝ c✝
⊢ refl_clos (trans_clos R) a✝ c✝

case a.step.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝¹ b✝ c✝ : A
step : trans_clos (refl_clos R) b✝ c✝
ih : refl_clos (trans_clos R) b✝ c✝
a✝ : R a✝¹ b✝
⊢ refl_clos (trans_clos R) a✝¹ c✝
Tactic:
trivial
State after:
case a.step.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝¹ b✝ c✝ : A
step : trans_clos (refl_clos R) b✝ c✝
ih : refl_clos (trans_clos R) b✝ c✝
a✝ : R a✝¹ b✝
⊢ refl_clos (trans_clos R) a✝¹ c✝

State before:
case a.step.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝¹ b✝ c✝ : A
step : trans_clos (refl_clos R) b✝ c✝
ih : refl_clos (trans_clos R) b✝ c✝
a✝ : R a✝¹ b✝
⊢ refl_clos (trans_clos R) a✝¹ c✝
Tactic:
apply refl_clos.base
State after:
case a.step.base.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝¹ b✝ c✝ : A
step : trans_clos (refl_clos R) b✝ c✝
ih : refl_clos (trans_clos R) b✝ c✝
a✝ : R a✝¹ b✝
⊢ trans_clos R a✝¹ c✝

State before:
case a.step.base.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝¹ b✝ c✝ : A
step : trans_clos (refl_clos R) b✝ c✝
ih : refl_clos (trans_clos R) b✝ c✝
a✝ : R a✝¹ b✝
⊢ trans_clos R a✝¹ c✝
Tactic:
aesop
State after:
no goals