internlm/Lean-Github huggingface dataset:
Theorem: List.HookedAscending.of_implies
Proof 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
Proof 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
Theorem: List.HookedAscending.of_implies
Proof 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
Proof 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
Theorem: List.HookedAscending.of_implies
Proof 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
Proof state after:
no goals
Theorem: List.HookedAscending.of_implies
Proof 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
Proof state after:
no goals
Theorem: List.HookedAscending.of_implies
Proof 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
Proof state after:
no goals
Theorem: List.HookedAscending.of_implies
Proof 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
Proof state after:
no goals
Theorem: List.HookedAscending.of_implies
Proof 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
Proof 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
Theorem: List.HookedAscending.of_implies
Proof 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
Proof state after:
no goals
Theorem: List.HookedAscending.of_implies
Proof 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
Proof state after:
no goals
Theorem: List.HookedAscending.unhook
Proof state before:
α : Type u_1
r : α → α → Prop
as bs : List α
⊢ HookedAscending r as bs → Ascending r (reverseAux as bs)
Tactic:
cases as <;> simp
Proof state after:
case nil
α : Type u_1
r : α → α → Prop
bs : List α
⊢ HookedAscending r [] bs → Ascending r bs

case cons
α : Type u_1
r : α → α → Prop
bs : List α
head✝ : α
tail✝ : List α
⊢ HookedAscending r (head✝ :: tail✝) bs → Ascending r (reverseAux tail✝ (head✝ :: bs))
Theorem: List.HookedAscending.unhook
Proof state before:
α : Type u_1
r : α → α → Prop
bs : List α
⊢ HookedAscending r [] bs → Ascending r bs
Tactic:
case nil => exact HookedAscending.snd_Ascending
Proof state after:
no goals
Theorem: List.HookedAscending.unhook
Proof state before:
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
⊢ HookedAscending r (a :: as) bs → Ascending r (reverseAux as (a :: bs))
Tactic:
case cons a as =>
  intro hhook
  apply Ascending.reverseAux_cons
  . exact hhook.fst_revAscending
  . apply Ascending.cons_of_forAll _ hhook.snd_Ascending
    have := hhook.fst_lt_snd
    rw [List.forAllRel_cons_left] at this
    exact this.left
Proof state after:
no goals
Theorem: List.HookedAscending.unhook
Proof state before:
α : Type u_1
r : α → α → Prop
bs : List α
⊢ HookedAscending r [] bs → Ascending r bs
Tactic:
exact HookedAscending.snd_Ascending
Proof state after:
no goals
Theorem: List.HookedAscending.unhook
Proof state before:
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
⊢ HookedAscending r (a :: as) bs → Ascending r (reverseAux as (a :: bs))
Tactic:
intro hhook
Proof state after:
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending r (reverseAux as (a :: bs))
Theorem: List.HookedAscending.unhook
Proof state before:
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending r (reverseAux as (a :: bs))
Tactic:
apply Ascending.reverseAux_cons
Proof state after:
case a
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending (flip r) (a :: as)

case a
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending r (a :: bs)
Theorem: List.HookedAscending.unhook
Proof state before:
case a
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending (flip r) (a :: as)

case a
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending r (a :: bs)
Tactic:
. exact hhook.fst_revAscending
Proof state after:
case a
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending r (a :: bs)
Theorem: List.HookedAscending.unhook
Proof state before:
case a
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending r (a :: bs)
Tactic:
. apply Ascending.cons_of_forAll _ hhook.snd_Ascending
  have := hhook.fst_lt_snd
  rw [List.forAllRel_cons_left] at this
  exact this.left
Proof state after:
no goals
Theorem: List.HookedAscending.unhook
Proof state before:
case a
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending (flip r) (a :: as)
Tactic:
exact hhook.fst_revAscending
Proof state after:
no goals
Theorem: List.HookedAscending.unhook
Proof state before:
case a
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
hhook : HookedAscending r (a :: as) bs
⊢ Ascending r (a :: bs)
Tactic:
apply Ascending.cons_of_forAll _ hhook.snd_Ascending
Proof state after:
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
hhook : HookedAscending r (a :: as) bs
⊢ forAll (r a) bs
Theorem: List.HookedAscending.unhook
Proof state before:
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
hhook : HookedAscending r (a :: as) bs
⊢ forAll (r a) bs
Tactic:
have := hhook.fst_lt_snd
Proof state after:
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
hhook : HookedAscending r (a :: as) bs
this : List.forAllRel r (a :: as) bs
⊢ forAll (r a) bs
Theorem: List.HookedAscending.unhook
Proof state before:
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
hhook : HookedAscending r (a :: as) bs
this : List.forAllRel r (a :: as) bs
⊢ forAll (r a) bs
Tactic:
rw [List.forAllRel_cons_left] at this
Proof state after:
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
hhook : HookedAscending r (a :: as) bs
this : forAll (r a) bs ∧ List.forAllRel r as bs
⊢ forAll (r a) bs
Theorem: List.HookedAscending.unhook
Proof state before:
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
hhook : HookedAscending r (a :: as) bs
this : forAll (r a) bs ∧ List.forAllRel r as bs
⊢ forAll (r a) bs
Tactic:
exact this.left
Proof state after:
no goals
Theorem: List.HookedAscending.flip
Proof state before:
α : Type u_1
r : α → α → Prop
as bs : List α
hhook : HookedAscending r as bs
⊢ List.forAllRel (flip r) bs as
Tactic:
simp
Proof state after:
α : Type u_1
r : α → α → Prop
as bs : List α
hhook : HookedAscending r as bs
⊢ List.forAllRel r as bs
Theorem: List.HookedAscending.flip
Proof state before:
α : Type u_1
r : α → α → Prop
as bs : List α
hhook : HookedAscending r as bs
⊢ List.forAllRel r as bs
Tactic:
exact hhook.fst_lt_snd
Proof state after:
no goals
Theorem: List.HookedAscending.flip
Proof state before:
α : Type u_1
r : α → α → Prop
as bs : List α
hhook : HookedAscending r as bs
⊢ Ascending (flip (flip r)) bs
Tactic:
have : ∀ a b, r a b → flip (flip r) a b := λ _ _ => id
Proof state after:
α : Type u_1
r : α → α → Prop
as bs : List α
hhook : HookedAscending r as bs
this : ∀ (a b : α), r a b → flip (flip r) a b
⊢ Ascending (flip (flip r)) bs
Theorem: List.HookedAscending.flip
Proof state before:
α : Type u_1
r : α → α → Prop
as bs : List α
hhook : HookedAscending r as bs
this : ∀ (a b : α), r a b → flip (flip r) a b
⊢ Ascending (flip (flip r)) bs
Tactic:
apply Ascending.of_implies this
Proof state after:
α : Type u_1
r : α → α → Prop
as bs : List α
hhook : HookedAscending r as bs
this : ∀ (a b : α), r a b → flip (flip r) a b
⊢ Ascending (fun a b => r a b) bs
Theorem: List.HookedAscending.flip
Proof state before:
α : Type u_1
r : α → α → Prop
as bs : List α
hhook : HookedAscending r as bs
this : ∀ (a b : α), r a b → flip (flip r) a b
⊢ Ascending (fun a b => r a b) bs
Tactic:
exact hhook.snd_Ascending
Proof state after:
no goals
Theorem: List.HookedAscending.reelL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
⊢ HookedAscending r as (b :: bs) → HookedAscending r (b :: as) bs
Tactic:
intro hhook
Proof state after:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
⊢ HookedAscending r (b :: as) bs
Theorem: List.HookedAscending.reelL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
⊢ HookedAscending r (b :: as) bs
Tactic:
have hlt := hhook.fst_lt_snd
Proof state after:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
hlt : List.forAllRel r as (b :: bs)
⊢ HookedAscending r (b :: as) bs
Theorem: List.HookedAscending.reelL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
hlt : List.forAllRel r as (b :: bs)
⊢ HookedAscending r (b :: as) bs
Tactic:
rw [List.forAllRel_cons_right] at hlt
Proof state after:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ HookedAscending r (b :: as) bs
Theorem: List.HookedAscending.reelL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ HookedAscending r (b :: as) bs
Tactic:
constructor
Proof state after:
case fst_lt_snd
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ List.forAllRel r (b :: as) bs

case fst_revAscending
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ Ascending (flip r) (b :: as)

case snd_Ascending
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ Ascending r bs
Theorem: List.HookedAscending.reelL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ List.forAllRel r (b :: as) bs
Tactic:
case fst_lt_snd =>
  constructor
  case left => exact hhook.snd_Ascending.forAll_of_tail
  case right => exact hlt.right
Proof state after:
no goals
Theorem: List.HookedAscending.reelL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ Ascending (flip r) (b :: as)
Tactic:
case fst_revAscending =>
  exact List.Ascending.cons_of_forAll hlt.left hhook.fst_revAscending
Proof state after:
no goals
Theorem: List.HookedAscending.reelL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ Ascending r bs
Tactic:
case snd_Ascending => exact hhook.snd_Ascending.tail
Proof state after:
no goals
Theorem: List.HookedAscending.reelL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ List.forAllRel r (b :: as) bs
Tactic:
constructor
Proof state after:
case left
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ (fun a => forAll (r a) bs) b

case right
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ forAll (fun a => forAll (r a) bs) as
Theorem: List.HookedAscending.reelL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ (fun a => forAll (r a) bs) b
Tactic:
case left => exact hhook.snd_Ascending.forAll_of_tail
Proof state after:
no goals
Theorem: List.HookedAscending.reelL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ forAll (fun a => forAll (r a) bs) as
Tactic:
case right => exact hlt.right
Proof state after:
no goals
Theorem: List.HookedAscending.reelL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ (fun a => forAll (r a) bs) b
Tactic:
exact hhook.snd_Ascending.forAll_of_tail
Proof state after:
no goals
Theorem: List.HookedAscending.reelL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ forAll (fun a => forAll (r a) bs) as
Tactic:
exact hlt.right
Proof state after:
no goals
Theorem: List.HookedAscending.reelL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ Ascending (flip r) (b :: as)
Tactic:
exact List.Ascending.cons_of_forAll hlt.left hhook.fst_revAscending
Proof state after:
no goals
Theorem: List.HookedAscending.reelL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ Ascending r bs
Tactic:
exact hhook.snd_Ascending.tail
Proof state after:
no goals
Theorem: List.HookedAscending.reelR
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
⊢ ∀ {a b c : α}, flip r a b → flip r b c → flip r a c
Tactic:
simp [flip]
Proof state after:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
⊢ ∀ {a b c : α}, r b a → r c b → r c a
Theorem: List.HookedAscending.reelR
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
a : α
as bs : List α
hhook : HookedAscending r (a :: as) bs
⊢ ∀ {a b c : α}, r b a → r c b → r c a
Tactic:
exact flip trans
Proof state after:
no goals
Theorem: List.HookedAscending.substToL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
⊢ eqv a b → eqv b a → HookedAscending r as (b :: bs) → HookedAscending r (a :: as) bs
Tactic:
intro hab hba hhook
Proof state after:
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
⊢ HookedAscending r (a :: as) bs
Theorem: List.HookedAscending.substToL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
⊢ HookedAscending r (a :: as) bs
Tactic:
have hlt := hhook.fst_lt_snd
Proof state after:
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
hlt : List.forAllRel r as (b :: bs)
⊢ HookedAscending r (a :: as) bs
Theorem: List.HookedAscending.substToL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
hlt : List.forAllRel r as (b :: bs)
⊢ HookedAscending r (a :: as) bs
Tactic:
rw [List.forAllRel_cons_right] at hlt
Proof state after:
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ HookedAscending r (a :: as) bs
Theorem: List.HookedAscending.substToL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ HookedAscending r (a :: as) bs
Tactic:
constructor
Proof state after:
case fst_lt_snd
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ List.forAllRel r (a :: as) bs

case fst_revAscending
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ Ascending (flip r) (a :: as)

case snd_Ascending
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ Ascending r bs
Theorem: List.HookedAscending.substToL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ List.forAllRel r (a :: as) bs
Tactic:
case fst_lt_snd =>
  constructor
  case left =>
    apply List.forAll_of_forAll (λ x (h : r b x) => trans hab h)
    exact hhook.snd_Ascending.forAll_of_tail
  case right => exact hlt.right
Proof state after:
no goals
Theorem: List.HookedAscending.substToL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ Ascending (flip r) (a :: as)
Tactic:
case fst_revAscending =>
  apply List.Ascending.cons_of_forAll _ hhook.fst_revAscending
  apply List.forAll_of_forAll (λ x (h : r x b) => trans h hba)
  exact hlt.left
Proof state after:
no goals
Theorem: List.HookedAscending.substToL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ Ascending r bs
Tactic:
case snd_Ascending => exact hhook.snd_Ascending.tail
Proof state after:
no goals
Theorem: List.HookedAscending.substToL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ List.forAllRel r (a :: as) bs
Tactic:
constructor
Proof state after:
case left
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ (fun a => forAll (r a) bs) a

case right
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ forAll (fun a => forAll (r a) bs) as
Theorem: List.HookedAscending.substToL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ (fun a => forAll (r a) bs) a
Tactic:
case left =>
  apply List.forAll_of_forAll (λ x (h : r b x) => trans hab h)
  exact hhook.snd_Ascending.forAll_of_tail
Proof state after:
no goals
Theorem: List.HookedAscending.substToL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ forAll (fun a => forAll (r a) bs) as
Tactic:
case right => exact hlt.right
Proof state after:
no goals
Theorem: List.HookedAscending.substToL
Proof state before:
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ (fun a => forAll (r a) bs) a
Tactic:
apply List.forAll_of_forAll (λ x (h : r b x) => trans hab h)
Proof state after:
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ forAll (fun x => r b x) bs