internlm/Lean-Github huggingface dataset:
Theorem: List.Ascending.append
Proof state before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
⊢ List.forAllRel r (a :: as) bs → Ascending r (a :: as) → Ascending r bs → Ascending r (a :: as ++ bs)
Tactic:
dsimp [forAllRel_cons_left]
Proof state after:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
⊢ List.forAllRel r (a :: as) bs → Ascending r (a :: as) → Ascending r bs → Ascending r (a :: (as ++ bs))
Theorem: List.Ascending.append
Proof state before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
⊢ List.forAllRel r (a :: as) bs → Ascending r (a :: as) → Ascending r bs → Ascending r (a :: (as ++ bs))
Tactic:
rw [List.forAllRel_cons_left]
Proof state after:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
⊢ forAll (r a) bs ∧ List.forAllRel r as bs → Ascending r (a :: as) → Ascending r bs → Ascending r (a :: (as ++ bs))
Theorem: List.Ascending.append
Proof state before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
⊢ forAll (r a) bs ∧ List.forAllRel r as bs → Ascending r (a :: as) → Ascending r bs → Ascending r (a :: (as ++ bs))
Tactic:
intro h hass hbs
Proof state after:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
h : forAll (r a) bs ∧ List.forAllRel r as bs
hass : Ascending r (a :: as)
hbs : Ascending r bs
⊢ Ascending r (a :: (as ++ bs))
Theorem: List.Ascending.append
Proof state before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
h : forAll (r a) bs ∧ List.forAllRel r as bs
hass : Ascending r (a :: as)
hbs : Ascending r bs
⊢ Ascending r (a :: (as ++ bs))
Tactic:
have htail := h_ind h.right hass.tail hbs
Proof state after:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
h : forAll (r a) bs ∧ List.forAllRel r as bs
hass : Ascending r (a :: as)
hbs : Ascending r bs
htail : Ascending r (as ++ bs)
⊢ Ascending r (a :: (as ++ bs))
Theorem: List.Ascending.append
Proof state before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
h : forAll (r a) bs ∧ List.forAllRel r as bs
hass : Ascending r (a :: as)
hbs : Ascending r bs
htail : Ascending r (as ++ bs)
⊢ Ascending r (a :: (as ++ bs))
Tactic:
have hhead : bs.forAll (r a) := h.left
Proof state after:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
h : forAll (r a) bs ∧ List.forAllRel r as bs
hass : Ascending r (a :: as)
hbs : Ascending r bs
htail : Ascending r (as ++ bs)
hhead : forAll (r a) bs
⊢ Ascending r (a :: (as ++ bs))
Theorem: List.Ascending.append
Proof state before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
h : forAll (r a) bs ∧ List.forAllRel r as bs
hass : Ascending r (a :: as)
hbs : Ascending r bs
htail : Ascending r (as ++ bs)
hhead : forAll (r a) bs
⊢ Ascending r (a :: (as ++ bs))
Tactic:
apply cons_of_forAll _ htail
Proof state after:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
h : forAll (r a) bs ∧ List.forAllRel r as bs
hass : Ascending r (a :: as)
hbs : Ascending r bs
htail : Ascending r (as ++ bs)
hhead : forAll (r a) bs
⊢ forAll (r a) (as ++ bs)
Theorem: List.Ascending.append
Proof state before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
h : forAll (r a) bs ∧ List.forAllRel r as bs
hass : Ascending r (a :: as)
hbs : Ascending r bs
htail : Ascending r (as ++ bs)
hhead : forAll (r a) bs
⊢ forAll (r a) (as ++ bs)
Tactic:
rw [forAll_append]
Proof state after:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
h : forAll (r a) bs ∧ List.forAllRel r as bs
hass : Ascending r (a :: as)
hbs : Ascending r bs
htail : Ascending r (as ++ bs)
hhead : forAll (r a) bs
⊢ forAll (r a) as ∧ forAll (r a) bs
Theorem: List.Ascending.append
Proof state before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
h : forAll (r a) bs ∧ List.forAllRel r as bs
hass : Ascending r (a :: as)
hbs : Ascending r bs
htail : Ascending r (as ++ bs)
hhead : forAll (r a) bs
⊢ forAll (r a) as ∧ forAll (r a) bs
Tactic:
exact And.intro hass.forAll_of_tail hhead
Proof state after:
no goals
Theorem: List.Ascending.reverseAux_cons
Proof state before:
α : Type u
r : α → α → Prop
a : α
as bs : List α
⊢ Ascending (flip r) (a :: as) → Ascending r (a :: bs) → Ascending r (reverseAux (a :: as) bs)
Tactic:
revert a bs
Proof state after:
α : Type u
r : α → α → Prop
as : List α
⊢ ∀ {a : α} {bs : List α}, Ascending (flip r) (a :: as) → Ascending r (a :: bs) → Ascending r (reverseAux (a :: as) bs)
Theorem: List.Ascending.reverseAux_cons
Proof state before:
α : Type u
r : α → α → Prop
as : List α
⊢ ∀ {a : α} {bs : List α}, Ascending (flip r) (a :: as) → Ascending r (a :: bs) → Ascending r (reverseAux (a :: as) bs)
Tactic:
induction as <;> dsimp [reverseAux] <;> intro a bs
Proof state after:
case nil
α : Type u
r : α → α → Prop
a : α
bs : List α
⊢ Ascending (flip r) [a] → Ascending r (a :: bs) → Ascending r (a :: bs)

case cons
α : Type u
r : α → α → Prop
head✝ : α
tail✝ : List α
tail_ih✝ :
  ∀ {a : α} {bs : List α},
    Ascending (flip r) (a :: tail✝) → Ascending r (a :: bs) → Ascending r (reverseAux (a :: tail✝) bs)
a : α
bs : List α
⊢ Ascending (flip r) (a :: head✝ :: tail✝) → Ascending r (a :: bs) → Ascending r (reverseAux tail✝ (head✝ :: a :: bs))
Theorem: List.Ascending.reverseAux_cons
Proof state before:
α : Type u
r : α → α → Prop
a : α
bs : List α
⊢ Ascending (flip r) [a] → Ascending r (a :: bs) → Ascending r (a :: bs)
Tactic:
case nil => exact λ _ => id
Proof state after:
no goals
Theorem: List.Ascending.reverseAux_cons
Proof state before:
α : Type u
r : α → α → Prop
a' : α
as : List α
h_ind :
  ∀ {a : α} {bs : List α}, Ascending (flip r) (a :: as) → Ascending r (a :: bs) → Ascending r (reverseAux (a :: as) bs)
a : α
bs : List α
⊢ Ascending (flip r) (a :: a' :: as) → Ascending r (a :: bs) → Ascending r (reverseAux as (a' :: a :: bs))
Tactic:
case cons a' as h_ind =>
  intro haaas habs
  simp [reverseAux] at h_ind
  cases haaas with | cons haa haas =>
  apply h_ind haas (habs.cons haa)
Proof state after:
no goals
Theorem: List.Ascending.reverseAux_cons
Proof state before:
α : Type u
r : α → α → Prop
a : α
bs : List α
⊢ Ascending (flip r) [a] → Ascending r (a :: bs) → Ascending r (a :: bs)
Tactic:
exact λ _ => id
Proof state after:
no goals
Theorem: List.Ascending.reverseAux_cons
Proof state before:
α : Type u
r : α → α → Prop
a' : α
as : List α
h_ind :
  ∀ {a : α} {bs : List α}, Ascending (flip r) (a :: as) → Ascending r (a :: bs) → Ascending r (reverseAux (a :: as) bs)
a : α
bs : List α
⊢ Ascending (flip r) (a :: a' :: as) → Ascending r (a :: bs) → Ascending r (reverseAux as (a' :: a :: bs))
Tactic:
intro haaas habs
Proof state after:
α : Type u
r : α → α → Prop
a' : α
as : List α
h_ind :
  ∀ {a : α} {bs : List α}, Ascending (flip r) (a :: as) → Ascending r (a :: bs) → Ascending r (reverseAux (a :: as) bs)
a : α
bs : List α
haaas : Ascending (flip r) (a :: a' :: as)
habs : Ascending r (a :: bs)
⊢ Ascending r (reverseAux as (a' :: a :: bs))
Theorem: List.Ascending.reverseAux_cons
Proof state before:
α : Type u
r : α → α → Prop
a' : α
as : List α
h_ind :
  ∀ {a : α} {bs : List α}, Ascending (flip r) (a :: as) → Ascending r (a :: bs) → Ascending r (reverseAux (a :: as) bs)
a : α
bs : List α
haaas : Ascending (flip r) (a :: a' :: as)
habs : Ascending r (a :: bs)
⊢ Ascending r (reverseAux as (a' :: a :: bs))
Tactic:
simp [reverseAux] at h_ind
Proof state after:
α : Type u
r : α → α → Prop
a' : α
as : List α
h_ind :
  ∀ {a : α} {bs : List α}, Ascending (flip r) (a :: as) → Ascending r (a :: bs) → Ascending r (reverseAux as (a :: bs))
a : α
bs : List α
haaas : Ascending (flip r) (a :: a' :: as)
habs : Ascending r (a :: bs)
⊢ Ascending r (reverseAux as (a' :: a :: bs))
Theorem: List.Ascending.reverseAux_cons
Proof state before:
α : Type u
r : α → α → Prop
a' : α
as : List α
h_ind :
  ∀ {a : α} {bs : List α}, Ascending (flip r) (a :: as) → Ascending r (a :: bs) → Ascending r (reverseAux as (a :: bs))
a : α
bs : List α
haaas : Ascending (flip r) (a :: a' :: as)
habs : Ascending r (a :: bs)
⊢ Ascending r (reverseAux as (a' :: a :: bs))
Tactic:
cases haaas with | cons haa haas =>
apply h_ind haas (habs.cons haa)
Proof state after:
no goals
Theorem: List.Ascending.reverseAux_cons
Proof state before:
case cons
α : Type u
r : α → α → Prop
a' : α
as : List α
h_ind :
  ∀ {a : α} {bs : List α}, Ascending (flip r) (a :: as) → Ascending r (a :: bs) → Ascending r (reverseAux as (a :: bs))
a : α
bs : List α
habs : Ascending r (a :: bs)
haa : flip r a a'
haas : Ascending (flip r) (a' :: as)
⊢ Ascending r (reverseAux as (a' :: a :: bs))
Tactic:
apply h_ind haas (habs.cons haa)
Proof state after:
no goals
Theorem: List.Ascending.reverseAux
Proof state before:
α : Type u
r : α → α → Prop
as bs : List α
⊢ relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
Tactic:
revert bs
Proof state after:
α : Type u
r : α → α → Prop
as : List α
⊢ ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
Theorem: List.Ascending.reverseAux
Proof state before:
α : Type u
r : α → α → Prop
as : List α
⊢ ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
Tactic:
induction as <;> intro bs
Proof state after:
case nil
α : Type u
r : α → α → Prop
bs : List α
⊢ relHead r [] bs → Ascending (flip r) [] → Ascending r bs → Ascending r (List.reverseAux [] bs)

case cons
α : Type u
r : α → α → Prop
head✝ : α
tail✝ : List α
tail_ih✝ :
  ∀ {bs : List α},
    relHead r tail✝ bs → Ascending (flip r) tail✝ → Ascending r bs → Ascending r (List.reverseAux tail✝ bs)
bs : List α
⊢ relHead r (head✝ :: tail✝) bs →
    Ascending (flip r) (head✝ :: tail✝) → Ascending r bs → Ascending r (List.reverseAux (head✝ :: tail✝) bs)
Theorem: List.Ascending.reverseAux
Proof state before:
α : Type u
r : α → α → Prop
bs : List α
⊢ relHead r [] bs → Ascending (flip r) [] → Ascending r bs → Ascending r (List.reverseAux [] bs)
Tactic:
case nil => exact λ _ _ => id
Proof state after:
no goals
Theorem: List.Ascending.reverseAux
Proof state before:
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
⊢ relHead r (a :: as) bs → Ascending (flip r) (a :: as) → Ascending r bs → Ascending r (List.reverseAux (a :: as) bs)
Tactic:
case cons a as h_ind =>
  intro hhead has hbs
  unfold List.reverseAux
  apply h_ind
  . exact relHead_cons_right ▸ has.head
  . exact has.tail
  . exact hbs.cons_of_head_tail (relHead_cons_left ▸ hhead)
Proof state after:
no goals
Theorem: List.Ascending.reverseAux
Proof state before:
α : Type u
r : α → α → Prop
bs : List α
⊢ relHead r [] bs → Ascending (flip r) [] → Ascending r bs → Ascending r (List.reverseAux [] bs)
Tactic:
exact λ _ _ => id
Proof state after:
no goals
Theorem: List.Ascending.reverseAux
Proof state before:
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
⊢ relHead r (a :: as) bs → Ascending (flip r) (a :: as) → Ascending r bs → Ascending r (List.reverseAux (a :: as) bs)
Tactic:
intro hhead has hbs
Proof state after:
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending r (List.reverseAux (a :: as) bs)
Theorem: List.Ascending.reverseAux
Proof state before:
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending r (List.reverseAux (a :: as) bs)
Tactic:
unfold List.reverseAux
Proof state after:
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending r (List.reverseAux as (a :: bs))
Theorem: List.Ascending.reverseAux
Proof state before:
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending r (List.reverseAux as (a :: bs))
Tactic:
apply h_ind
Proof state after:
case a
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ relHead r as (a :: bs)

case a
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending (flip r) as

case a
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending r (a :: bs)
Theorem: List.Ascending.reverseAux
Proof state before:
case a
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ relHead r as (a :: bs)

case a
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending (flip r) as

case a
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending r (a :: bs)
Tactic:
. exact relHead_cons_right ▸ has.head
Proof state after:
case a
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending (flip r) as

case a
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending r (a :: bs)
Theorem: List.Ascending.reverseAux
Proof state before:
case a
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending (flip r) as

case a
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending r (a :: bs)
Tactic:
. exact has.tail
Proof state after:
case a
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending r (a :: bs)
Theorem: List.Ascending.reverseAux
Proof state before:
case a
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending r (a :: bs)
Tactic:
. exact hbs.cons_of_head_tail (relHead_cons_left ▸ hhead)
Proof state after:
no goals
Theorem: List.Ascending.reverseAux
Proof state before:
case a
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ relHead r as (a :: bs)
Tactic:
exact relHead_cons_right ▸ has.head
Proof state after:
no goals
Theorem: List.Ascending.reverseAux
Proof state before:
case a
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending (flip r) as
Tactic:
exact has.tail
Proof state after:
no goals
Theorem: List.Ascending.reverseAux
Proof state before:
case a
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending r (a :: bs)
Tactic:
exact hbs.cons_of_head_tail (relHead_cons_left ▸ hhead)
Proof state after:
no goals
Theorem: List.Ascending.reverse
Proof state before:
α : Type u
r : α → α → Prop
as : List α
hchain : Ascending r as
this : Ascending (flip (flip r)) as
⊢ relHead (flip r) as []
Tactic:
cases as <;> exact True.intro
Proof state after:
no goals
Theorem: List.Ascending.filterMap
Proof state before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
β : Type v
r' : β → β → Prop
f : α → Option β
rel_pres : ∀ (a₁ a₂ : α), r a₁ a₂ → ∀ (b₁ b₂ : β), f a₁ = some b₁ → f a₂ = some b₂ → r' b₁ b₂
⊢ ∀ {as : List α}, Ascending r as → Ascending r' (filterMap f as)
Tactic:
intro as
Proof state after:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
β : Type v
r' : β → β → Prop
f : α → Option β
rel_pres : ∀ (a₁ a₂ : α), r a₁ a₂ → ∀ (b₁ b₂ : β), f a₁ = some b₁ → f a₂ = some b₂ → r' b₁ b₂
as : List α
⊢ Ascending r as → Ascending r' (filterMap f as)
Theorem: List.Ascending.filterMap
Proof state before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
β : Type v
r' : β → β → Prop
f : α → Option β
rel_pres : ∀ (a₁ a₂ : α), r a₁ a₂ → ∀ (b₁ b₂ : β), f a₁ = some b₁ → f a₂ = some b₂ → r' b₁ b₂
as : List α
⊢ Ascending r as → Ascending r' (filterMap f as)
Tactic:
induction as
Proof state after:
case nil
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
β : Type v
r' : β → β → Prop
f : α → Option β
rel_pres : ∀ (a₁ a₂ : α), r a₁ a₂ → ∀ (b₁ b₂ : β), f a₁ = some b₁ → f a₂ = some b₂ → r' b₁ b₂
⊢ Ascending r [] → Ascending r' (filterMap f [])

case cons
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
β : Type v
r' : β → β → Prop
f : α → Option β
rel_pres : ∀ (a₁ a₂ : α), r a₁ a₂ → ∀ (b₁ b₂ : β), f a₁ = some b₁ → f a₂ = some b₂ → r' b₁ b₂
head✝ : α
tail✝ : List α
tail_ih✝ : Ascending r tail✝ → Ascending r' (filterMap f tail✝)
⊢ Ascending r (head✝ :: tail✝) → Ascending r' (filterMap f (head✝ :: tail✝))
Theorem: List.Ascending.filterMap
Proof state before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
β : Type v
r' : β → β → Prop
f : α → Option β
rel_pres : ∀ (a₁ a₂ : α), r a₁ a₂ → ∀ (b₁ b₂ : β), f a₁ = some b₁ → f a₂ = some b₂ → r' b₁ b₂
⊢ Ascending r [] → Ascending r' (filterMap f [])
Tactic:
case nil => exact λ _ => Ascending.nil
Proof state after:
no goals
Theorem: List.Ascending.filterMap
Proof state before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
β : Type v
r' : β → β → Prop
f : α → Option β
rel_pres : ∀ (a₁ a₂ : α), r a₁ a₂ → ∀ (b₁ b₂ : β), f a₁ = some b₁ → f a₂ = some b₂ → r' b₁ b₂
a : α
as : List α
h_ind : Ascending r as → Ascending r' (filterMap f as)
⊢ Ascending r (a :: as) → Ascending r' (filterMap f (a :: as))
Tactic:
case cons a as h_ind =>
  intro hchain
  unfold filterMap
  cases hfa : f a <;> dsimp
  case none => exact h_ind hchain.tail
  case some b =>
    apply cons_of_forAll
    . clear h_ind
      induction as <;> dsimp [filterMap]
      case a.nil => dsimp [List.forAll]
      case a.cons a₁ as h_ind₁ =>
        have hchainaas : Ascending r (a::as) := by
          apply hchain.tail.subst_head
          exact λ _ h => trans hchain.head h
        cases hfa₁ : f a₁ <;> dsimp
        case none => exact h_ind₁ hchainaas
        case some b₁ =>
          constructor
          . have := rel_pres a a₁ hchain.head
            rw [hfa, hfa₁] at this
            exact this b b₁ rfl rfl
          . exact h_ind₁ hchainaas
    . exact h_ind hchain.tail
Proof state after:
no goals
Theorem: List.Ascending.filterMap
Proof state before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
β : Type v
r' : β → β → Prop
f : α → Option β
rel_pres : ∀ (a₁ a₂ : α), r a₁ a₂ → ∀ (b₁ b₂ : β), f a₁ = some b₁ → f a₂ = some b₂ → r' b₁ b₂
⊢ Ascending r [] → Ascending r' (filterMap f [])
Tactic:
exact λ _ => Ascending.nil
Proof state after:
no goals
Theorem: List.Ascending.filterMap
Proof state before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
β : Type v
r' : β → β → Prop
f : α → Option β
rel_pres : ∀ (a₁ a₂ : α), r a₁ a₂ → ∀ (b₁ b₂ : β), f a₁ = some b₁ → f a₂ = some b₂ → r' b₁ b₂
a : α
as : List α
h_ind : Ascending r as → Ascending r' (filterMap f as)
⊢ Ascending r (a :: as) → Ascending r' (filterMap f (a :: as))
Tactic:
intro hchain
Proof state after:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
β : Type v
r' : β → β → Prop
f : α → Option β
rel_pres : ∀ (a₁ a₂ : α), r a₁ a₂ → ∀ (b₁ b₂ : β), f a₁ = some b₁ → f a₂ = some b₂ → r' b₁ b₂
a : α
as : List α
h_ind : Ascending r as → Ascending r' (filterMap f as)
hchain : Ascending r (a :: as)
⊢ Ascending r' (filterMap f (a :: as))