Theorem: sym_clos_monotone (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) R R' → (fun R R' => ∀ (x y : A), R x y → R' x y) (sym_clos R) (sym_clos R')
Tactic:
intros le x y sym
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
R' : A → A → Prop
le : ∀ (x y : A), R x y → R' x y
x y : A
sym : sym_clos R x y
⊢ sym_clos R' x y

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
R' : A → A → Prop
le : ∀ (x y : A), R x y → R' x y
x y : A
sym : sym_clos R x y
⊢ sym_clos R' x y
Tactic:
induction sym <;> aesop
State after:
no goals