Theorem: refl_trans_union_left (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 => refl_trans_clos R x x_1)
    (refl_trans_clos ((fun R S x y => R x y ∨ S x y) R S))
Tactic:
simp
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ ∀ (x y : A), refl_trans_clos R x y → refl_trans_clos (fun x y => R x y ∨ S x y) x y

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ ∀ (x y : A), refl_trans_clos R x y → refl_trans_clos (fun x y => R x y ∨ S x y) x y
Tactic:
intros x y red_x_y
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
x y : A
red_x_y : refl_trans_clos R x y
⊢ refl_trans_clos (fun x y => R x y ∨ S x y) x y

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
x y : A
red_x_y : refl_trans_clos R x y
⊢ refl_trans_clos (fun x y => R x y ∨ S x y) x y
Tactic:
induction red_x_y <;> aesop
State after:
no goals