Theorem: List.HookedAscending.of_implies (Algdata/Data/List/Ascending.lean)

State before:
α : Type u_1
r r₁ : α → α → Prop
⊢ (∀ (a b : α), r a b → r₁ a b) → ∀ {as bs : List α}, HookedAscending r as bs → HookedAscending r₁ as bs
Tactic:
intro himp as bs hhook
State after:
α : Type u_1
r r₁ : α → α → Prop
himp : ∀ (a b : α), r a b → r₁ a b
as bs : List α
hhook : HookedAscending r as bs
⊢ HookedAscending r₁ as bs

State before:
α : Type u_1
r r₁ : α → α → Prop
himp : ∀ (a b : α), r a b → r₁ a b
as bs : List α
hhook : HookedAscending r as bs
⊢ HookedAscending r₁ as bs
Tactic:
constructor
State after:
case fst_lt_snd
α : Type u_1
r r₁ : α → α → Prop
himp : ∀ (a b : α), r a b → r₁ a b
as bs : List α
hhook : HookedAscending r as bs
⊢ List.forAllRel r₁ as bs

case fst_revAscending
α : Type u_1
r r₁ : α → α → Prop
himp : ∀ (a b : α), r a b → r₁ a b
as bs : List α
hhook : HookedAscending r as bs
⊢ Ascending (flip r₁) as

case snd_Ascending
α : Type u_1
r r₁ : α → α → Prop
himp : ∀ (a b : α), r a b → r₁ a b
as bs : List α
hhook : HookedAscending r as bs
⊢ Ascending r₁ bs

State before:
α : Type u_1
r r₁ : α → α → Prop
himp : ∀ (a b : α), r a b → r₁ a b
as bs : List α
hhook : HookedAscending r as bs
⊢ List.forAllRel r₁ as bs
Tactic:
case fst_lt_snd =>
  exact List.forAllRel_of_forAllRel himp hhook.fst_lt_snd
State after:
no goals

State before:
α : Type u_1
r r₁ : α → α → Prop
himp : ∀ (a b : α), r a b → r₁ a b
as bs : List α
hhook : HookedAscending r as bs
⊢ Ascending (flip r₁) as
Tactic:
case fst_revAscending =>
  have : ∀ a b, flip r a b → flip r₁ a b := λ a b => himp b a
  exact hhook.fst_revAscending.of_implies this
State after:
no goals

State before:
α : Type u_1
r r₁ : α → α → Prop
himp : ∀ (a b : α), r a b → r₁ a b
as bs : List α
hhook : HookedAscending r as bs
⊢ Ascending r₁ bs
Tactic:
case snd_Ascending =>
  exact hhook.snd_Ascending.of_implies himp
State after:
no goals

State before:
α : Type u_1
r r₁ : α → α → Prop
himp : ∀ (a b : α), r a b → r₁ a b
as bs : List α
hhook : HookedAscending r as bs
⊢ List.forAllRel r₁ as bs
Tactic:
exact List.forAllRel_of_forAllRel himp hhook.fst_lt_snd
State after:
no goals

State before:
α : Type u_1
r r₁ : α → α → Prop
himp : ∀ (a b : α), r a b → r₁ a b
as bs : List α
hhook : HookedAscending r as bs
⊢ Ascending (flip r₁) as
Tactic:
have : ∀ a b, flip r a b → flip r₁ a b := λ a b => himp b a
State after:
α : Type u_1
r r₁ : α → α → Prop
himp : ∀ (a b : α), r a b → r₁ a b
as bs : List α
hhook : HookedAscending r as bs
this : ∀ (a b : α), flip r a b → flip r₁ a b
⊢ Ascending (flip r₁) as

State before:
α : Type u_1
r r₁ : α → α → Prop
himp : ∀ (a b : α), r a b → r₁ a b
as bs : List α
hhook : HookedAscending r as bs
this : ∀ (a b : α), flip r a b → flip r₁ a b
⊢ Ascending (flip r₁) as
Tactic:
exact hhook.fst_revAscending.of_implies this
State after:
no goals

State before:
α : Type u_1
r r₁ : α → α → Prop
himp : ∀ (a b : α), r a b → r₁ a b
as bs : List α
hhook : HookedAscending r as bs
⊢ Ascending r₁ bs
Tactic:
exact hhook.snd_Ascending.of_implies himp
State after:
no goals