Theorem: inc_refl_trans_eq (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ ((fun R R' => ∀ (x y : A), R x y → R' x y) (fun x x_1 => R x x_1) fun x x_1 => S x x_1) →
    ((fun R R' => ∀ (x y : A), R x y → R' x y) (fun x x_1 => S x x_1) fun x x_1 => refl_trans_clos R x x_1) →
      (fun R R' => ∀ (x y : A), R x y ↔ R' x y) (fun x x_1 => refl_trans_clos S x x_1) fun x x_1 =>
        refl_trans_clos R x x_1
Tactic:
simp
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ (∀ (x y : A), R x y → S x y) →
    (∀ (x y : A), S x y → refl_trans_clos R x y) → ∀ (x y : A), refl_trans_clos S x y ↔ refl_trans_clos R x y

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ (∀ (x y : A), R x y → S x y) →
    (∀ (x y : A), S x y → refl_trans_clos R x y) → ∀ (x y : A), refl_trans_clos S x y ↔ refl_trans_clos R x y
Tactic:
intros r_sub_s s_sub_r_star x y
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y : A
⊢ refl_trans_clos S x y ↔ refl_trans_clos R x y

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y : A
⊢ refl_trans_clos S x y ↔ refl_trans_clos R x y
Tactic:
constructor <;> intros steps
State after:
case mp
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y : A
steps : refl_trans_clos S x y
⊢ refl_trans_clos R x y

case mpr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y : A
steps : refl_trans_clos R x y
⊢ refl_trans_clos S x y

State before:
case mp
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y : A
steps : refl_trans_clos S x y
⊢ refl_trans_clos R x y

case mpr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y : A
steps : refl_trans_clos R x y
⊢ refl_trans_clos S x y
Tactic:
. induction steps
  . constructor
  . apply refl_trans_clos_transitive
    . apply s_sub_r_star; trivial
    . trivial
State after:
case mpr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y : A
steps : refl_trans_clos R x y
⊢ refl_trans_clos S x y

State before:
case mpr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y : A
steps : refl_trans_clos R x y
⊢ refl_trans_clos S x y
Tactic:
. induction steps
  . constructor
  . aesop
State after:
no goals

State before:
case mp
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y : A
steps : refl_trans_clos S x y
⊢ refl_trans_clos R x y
Tactic:
induction steps
State after:
case mp.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝ : A
⊢ refl_trans_clos R a✝ a✝

case mp.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ refl_trans_clos R a✝² c✝

State before:
case mp.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝ : A
⊢ refl_trans_clos R a✝ a✝

case mp.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ refl_trans_clos R a✝² c✝
Tactic:
. constructor
State after:
case mp.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ refl_trans_clos R a✝² c✝

State before:
case mp.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ refl_trans_clos R a✝² c✝
Tactic:
. apply refl_trans_clos_transitive
  . apply s_sub_r_star; trivial
  . trivial
State after:
no goals

State before:
case mp.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝ : A
⊢ refl_trans_clos R a✝ a✝
Tactic:
constructor
State after:
no goals

State before:
case mp.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ refl_trans_clos R a✝² c✝
Tactic:
apply refl_trans_clos_transitive
State after:
case mp.step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ refl_trans_clos R a✝² ?mp.step.y

case mp.step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ refl_trans_clos R ?mp.step.y c✝

case mp.step.y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ A

State before:
case mp.step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ refl_trans_clos R a✝² ?mp.step.y

case mp.step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ refl_trans_clos R ?mp.step.y c✝

case mp.step.y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ A
Tactic:
. apply s_sub_r_star; trivial
State after:
case mp.step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ refl_trans_clos R b✝ c✝

State before:
case mp.step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ refl_trans_clos R b✝ c✝
Tactic:
. trivial
State after:
no goals

State before:
case mp.step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ refl_trans_clos R a✝² ?mp.step.y
Tactic:
apply s_sub_r_star
State after:
case mp.step.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ S a✝² ?mp.step.y

State before:
case mp.step.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ S a✝² ?mp.step.y
Tactic:
trivial
State after:
no goals

State before:
case mp.step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ refl_trans_clos R b✝ c✝
Tactic:
trivial
State after:
no goals

State before:
case mpr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y : A
steps : refl_trans_clos R x y
⊢ refl_trans_clos S x y
Tactic:
induction steps
State after:
case mpr.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝ : A
⊢ refl_trans_clos S a✝ a✝

case mpr.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
a_ih✝ : refl_trans_clos S b✝ c✝
⊢ refl_trans_clos S a✝² c✝

State before:
case mpr.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝ : A
⊢ refl_trans_clos S a✝ a✝

case mpr.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
a_ih✝ : refl_trans_clos S b✝ c✝
⊢ refl_trans_clos S a✝² c✝
Tactic:
. constructor
State after:
case mpr.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
a_ih✝ : refl_trans_clos S b✝ c✝
⊢ refl_trans_clos S a✝² c✝

State before:
case mpr.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
a_ih✝ : refl_trans_clos S b✝ c✝
⊢ refl_trans_clos S a✝² c✝
Tactic:
. aesop
State after:
no goals

State before:
case mpr.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝ : A
⊢ refl_trans_clos S a✝ a✝
Tactic:
constructor
State after:
no goals

State before:
case mpr.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
a_ih✝ : refl_trans_clos S b✝ c✝
⊢ refl_trans_clos S a✝² c✝
Tactic:
aesop
State after:
no goals