internlm/Lean-Github huggingface dataset:
Theorem: List.Ascending.head
Proof state before:
α : Type u
r : α → α → Prop
a b✝ : α
bs✝ : List α
a✝¹ : Ascending r (b✝ :: bs✝)
a✝ : r a b✝
⊢ predHead (r a) (b✝ :: bs✝)
Tactic:
case cons => exact ‹r a _›
Proof state after:
no goals
Theorem: List.Ascending.head
Proof state before:
α : Type u
r : α → α → Prop
a : α
⊢ predHead (r a) []
Tactic:
exact True.intro
Proof state after:
no goals
Theorem: List.Ascending.head
Proof state before:
α : Type u
r : α → α → Prop
a b✝ : α
bs✝ : List α
a✝¹ : Ascending r (b✝ :: bs✝)
a✝ : r a b✝
⊢ predHead (r a) (b✝ :: bs✝)
Tactic:
exact ‹r a _›
Proof state after:
no goals
Theorem: List.Ascending.of_append_left
Proof state before:
α : Type u
r : α → α → Prop
as bs : List α
⊢ Ascending r (as ++ bs) → Ascending r as
Tactic:
induction as
Proof state after:
case nil
α : Type u
r : α → α → Prop
bs : List α
⊢ Ascending r ([] ++ bs) → Ascending r []

case cons
α : Type u
r : α → α → Prop
bs : List α
head✝ : α
tail✝ : List α
tail_ih✝ : Ascending r (tail✝ ++ bs) → Ascending r tail✝
⊢ Ascending r (head✝ :: tail✝ ++ bs) → Ascending r (head✝ :: tail✝)
Theorem: List.Ascending.of_append_left
Proof state before:
α : Type u
r : α → α → Prop
bs : List α
⊢ Ascending r ([] ++ bs) → Ascending r []
Tactic:
case nil => exact λ _ => Ascending.nil
Proof state after:
no goals
Theorem: List.Ascending.of_append_left
Proof state before:
α : Type u
r : α → α → Prop
bs : List α
a : α
as : List α
h_ind : Ascending r (as ++ bs) → Ascending r as
⊢ Ascending r (a :: as ++ bs) → Ascending r (a :: as)
Tactic:
case cons a as h_ind =>
  cases as
  case nil => exact λ _ => Ascending.singleton a
  case cons a₁ as =>
    simp [List.cons_append] at *
    intro has; cases has with | cons ha htail =>
    exact Ascending.cons ha (h_ind htail)
Proof state after:
no goals
Theorem: List.Ascending.of_append_left
Proof state before:
α : Type u
r : α → α → Prop
bs : List α
⊢ Ascending r ([] ++ bs) → Ascending r []
Tactic:
exact λ _ => Ascending.nil
Proof state after:
no goals
Theorem: List.Ascending.of_append_left
Proof state before:
α : Type u
r : α → α → Prop
bs : List α
a : α
as : List α
h_ind : Ascending r (as ++ bs) → Ascending r as
⊢ Ascending r (a :: as ++ bs) → Ascending r (a :: as)
Tactic:
cases as
Proof state after:
case nil
α : Type u
r : α → α → Prop
bs : List α
a : α
h_ind : Ascending r ([] ++ bs) → Ascending r []
⊢ Ascending r ([a] ++ bs) → Ascending r [a]

case cons
α : Type u
r : α → α → Prop
bs : List α
a head✝ : α
tail✝ : List α
h_ind : Ascending r (head✝ :: tail✝ ++ bs) → Ascending r (head✝ :: tail✝)
⊢ Ascending r (a :: head✝ :: tail✝ ++ bs) → Ascending r (a :: head✝ :: tail✝)
Theorem: List.Ascending.of_append_left
Proof state before:
α : Type u
r : α → α → Prop
bs : List α
a : α
h_ind : Ascending r ([] ++ bs) → Ascending r []
⊢ Ascending r ([a] ++ bs) → Ascending r [a]
Tactic:
case nil => exact λ _ => Ascending.singleton a
Proof state after:
no goals
Theorem: List.Ascending.of_append_left
Proof state before:
α : Type u
r : α → α → Prop
bs : List α
a a₁ : α
as : List α
h_ind : Ascending r (a₁ :: as ++ bs) → Ascending r (a₁ :: as)
⊢ Ascending r (a :: a₁ :: as ++ bs) → Ascending r (a :: a₁ :: as)
Tactic:
case cons a₁ as =>
  simp [List.cons_append] at *
  intro has; cases has with | cons ha htail =>
  exact Ascending.cons ha (h_ind htail)
Proof state after:
no goals
Theorem: List.Ascending.of_append_left
Proof state before:
α : Type u
r : α → α → Prop
bs : List α
a : α
h_ind : Ascending r ([] ++ bs) → Ascending r []
⊢ Ascending r ([a] ++ bs) → Ascending r [a]
Tactic:
exact λ _ => Ascending.singleton a
Proof state after:
no goals
Theorem: List.Ascending.of_append_left
Proof state before:
α : Type u
r : α → α → Prop
bs : List α
a a₁ : α
as : List α
h_ind : Ascending r (a₁ :: as ++ bs) → Ascending r (a₁ :: as)
⊢ Ascending r (a :: a₁ :: as ++ bs) → Ascending r (a :: a₁ :: as)
Tactic:
simp [List.cons_append] at *
Proof state after:
α : Type u
r : α → α → Prop
bs : List α
a a₁ : α
as : List α
h_ind : Ascending r (a₁ :: (as ++ bs)) → Ascending r (a₁ :: as)
⊢ Ascending r (a :: a₁ :: (as ++ bs)) → Ascending r (a :: a₁ :: as)
Theorem: List.Ascending.of_append_left
Proof state before:
α : Type u
r : α → α → Prop
bs : List α
a a₁ : α
as : List α
h_ind : Ascending r (a₁ :: (as ++ bs)) → Ascending r (a₁ :: as)
⊢ Ascending r (a :: a₁ :: (as ++ bs)) → Ascending r (a :: a₁ :: as)
Tactic:
intro has
Proof state after:
α : Type u
r : α → α → Prop
bs : List α
a a₁ : α
as : List α
h_ind : Ascending r (a₁ :: (as ++ bs)) → Ascending r (a₁ :: as)
has : Ascending r (a :: a₁ :: (as ++ bs))
⊢ Ascending r (a :: a₁ :: as)
Theorem: List.Ascending.of_append_left
Proof state before:
α : Type u
r : α → α → Prop
bs : List α
a a₁ : α
as : List α
h_ind : Ascending r (a₁ :: (as ++ bs)) → Ascending r (a₁ :: as)
has : Ascending r (a :: a₁ :: (as ++ bs))
⊢ Ascending r (a :: a₁ :: as)
Tactic:
cases has with | cons ha htail =>
exact Ascending.cons ha (h_ind htail)
Proof state after:
no goals
Theorem: List.Ascending.of_append_left
Proof state before:
case cons
α : Type u
r : α → α → Prop
bs : List α
a a₁ : α
as : List α
h_ind : Ascending r (a₁ :: (as ++ bs)) → Ascending r (a₁ :: as)
ha : r a a₁
htail : Ascending r (a₁ :: (as ++ bs))
⊢ Ascending r (a :: a₁ :: as)
Tactic:
exact Ascending.cons ha (h_ind htail)
Proof state after:
no goals
Theorem: List.Ascending.of_append_right
Proof state before:
α : Type u
r : α → α → Prop
as bs : List α
⊢ Ascending r (as ++ bs) → Ascending r bs
Tactic:
induction as
Proof state after:
case nil
α : Type u
r : α → α → Prop
bs : List α
⊢ Ascending r ([] ++ bs) → Ascending r bs

case cons
α : Type u
r : α → α → Prop
bs : List α
head✝ : α
tail✝ : List α
tail_ih✝ : Ascending r (tail✝ ++ bs) → Ascending r bs
⊢ Ascending r (head✝ :: tail✝ ++ bs) → Ascending r bs
Theorem: List.Ascending.of_append_right
Proof state before:
α : Type u
r : α → α → Prop
bs : List α
⊢ Ascending r ([] ++ bs) → Ascending r bs
Tactic:
case nil => exact id
Proof state after:
no goals
Theorem: List.Ascending.of_append_right
Proof state before:
α : Type u
r : α → α → Prop
bs : List α
head✝ : α
tail✝ : List α
h_ind : Ascending r (tail✝ ++ bs) → Ascending r bs
⊢ Ascending r (head✝ :: tail✝ ++ bs) → Ascending r bs
Tactic:
case cons _ _ h_ind => exact h_ind ∘ Ascending.tail
Proof state after:
no goals
Theorem: List.Ascending.of_append_right
Proof state before:
α : Type u
r : α → α → Prop
bs : List α
⊢ Ascending r ([] ++ bs) → Ascending r bs
Tactic:
exact id
Proof state after:
no goals
Theorem: List.Ascending.of_append_right
Proof state before:
α : Type u
r : α → α → Prop
bs : List α
head✝ : α
tail✝ : List α
h_ind : Ascending r (tail✝ ++ bs) → Ascending r bs
⊢ Ascending r (head✝ :: tail✝ ++ bs) → Ascending r bs
Tactic:
exact h_ind ∘ Ascending.tail
Proof state after:
no goals
Theorem: List.Ascending.predHead_tail
Proof state before:
α : Type u
r : α → α → Prop
a : α
as : List α
p : α → Prop
⊢ (∀ (a b : α), p a → r a b → p b) → Ascending r (a :: as) → predHead p (a :: as) → predHead p as
Tactic:
intro hup hchain hpa
Proof state after:
α : Type u
r : α → α → Prop
a : α
as : List α
p : α → Prop
hup : ∀ (a b : α), p a → r a b → p b
hchain : Ascending r (a :: as)
hpa : predHead p (a :: as)
⊢ predHead p as
Theorem: List.Ascending.predHead_tail
Proof state before:
α : Type u
r : α → α → Prop
a : α
as : List α
p : α → Prop
hup : ∀ (a b : α), p a → r a b → p b
hchain : Ascending r (a :: as)
hpa : predHead p (a :: as)
⊢ predHead p as
Tactic:
cases as
Proof state after:
case nil
α : Type u
r : α → α → Prop
a : α
p : α → Prop
hup : ∀ (a b : α), p a → r a b → p b
hchain : Ascending r [a]
hpa : predHead p [a]
⊢ predHead p []

case cons
α : Type u
r : α → α → Prop
a : α
p : α → Prop
hup : ∀ (a b : α), p a → r a b → p b
head✝ : α
tail✝ : List α
hchain : Ascending r (a :: head✝ :: tail✝)
hpa : predHead p (a :: head✝ :: tail✝)
⊢ predHead p (head✝ :: tail✝)
Theorem: List.Ascending.predHead_tail
Proof state before:
α : Type u
r : α → α → Prop
a : α
p : α → Prop
hup : ∀ (a b : α), p a → r a b → p b
hchain : Ascending r [a]
hpa : predHead p [a]
⊢ predHead p []
Tactic:
case nil => exact True.intro
Proof state after:
no goals
Theorem: List.Ascending.predHead_tail
Proof state before:
α : Type u
r : α → α → Prop
a : α
p : α → Prop
hup : ∀ (a b : α), p a → r a b → p b
a₁ : α
as : List α
hchain : Ascending r (a :: a₁ :: as)
hpa : predHead p (a :: a₁ :: as)
⊢ predHead p (a₁ :: as)
Tactic:
case cons a₁ as => exact hup a a₁ hpa hchain.head
Proof state after:
no goals
Theorem: List.Ascending.predHead_tail
Proof state before:
α : Type u
r : α → α → Prop
a : α
p : α → Prop
hup : ∀ (a b : α), p a → r a b → p b
hchain : Ascending r [a]
hpa : predHead p [a]
⊢ predHead p []
Tactic:
exact True.intro
Proof state after:
no goals
Theorem: List.Ascending.predHead_tail
Proof state before:
α : Type u
r : α → α → Prop
a : α
p : α → Prop
hup : ∀ (a b : α), p a → r a b → p b
a₁ : α
as : List α
hchain : Ascending r (a :: a₁ :: as)
hpa : predHead p (a :: a₁ :: as)
⊢ predHead p (a₁ :: as)
Tactic:
exact hup a a₁ hpa hchain.head
Proof state after:
no goals
Theorem: List.Ascending.forAll_of_tail
Proof state before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
a : α
as : List α
⊢ Ascending r (a :: as) → forAll (r a) as
Tactic:
revert a
Proof state after:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
as : List α
⊢ ∀ {a : α}, Ascending r (a :: as) → forAll (r a) as
Theorem: List.Ascending.forAll_of_tail
Proof state before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
as : List α
⊢ ∀ {a : α}, Ascending r (a :: as) → forAll (r a) as
Tactic:
induction as <;> intro a h
Proof state after:
case nil
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
a : α
h : Ascending r [a]
⊢ forAll (r a) []

case cons
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {a : α}, Ascending r (a :: tail✝) → forAll (r a) tail✝
a : α
h : Ascending r (a :: head✝ :: tail✝)
⊢ forAll (r a) (head✝ :: tail✝)
Theorem: List.Ascending.forAll_of_tail
Proof state before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
a : α
h : Ascending r [a]
⊢ forAll (r a) []
Tactic:
case nil => exact True.intro
Proof state after:
no goals
Theorem: List.Ascending.forAll_of_tail
Proof state before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
a₁ : α
as : List α
h_ind : ∀ {a : α}, Ascending r (a :: as) → forAll (r a) as
a : α
h : Ascending r (a :: a₁ :: as)
⊢ forAll (r a) (a₁ :: as)
Tactic:
case cons a₁ as h_ind =>
  cases h with | cons ha htail =>
  have : as.forAll (r a) :=
    forAll_of_forAll (λ x => trans ha) $ h_ind htail
  exact And.intro ha this
Proof state after:
no goals
Theorem: List.Ascending.forAll_of_tail
Proof state before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
a : α
h : Ascending r [a]
⊢ forAll (r a) []
Tactic:
exact True.intro
Proof state after:
no goals
Theorem: List.Ascending.forAll_of_tail
Proof state before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
a₁ : α
as : List α
h_ind : ∀ {a : α}, Ascending r (a :: as) → forAll (r a) as
a : α
h : Ascending r (a :: a₁ :: as)
⊢ forAll (r a) (a₁ :: as)
Tactic:
cases h with | cons ha htail =>
have : as.forAll (r a) :=
  forAll_of_forAll (λ x => trans ha) $ h_ind htail
exact And.intro ha this
Proof state after:
no goals
Theorem: List.Ascending.forAll_of_tail
Proof state before:
case cons
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
a₁ : α
as : List α
h_ind : ∀ {a : α}, Ascending r (a :: as) → forAll (r a) as
a : α
ha : r a a₁
htail : Ascending r (a₁ :: as)
⊢ forAll (r a) (a₁ :: as)
Tactic:
have : as.forAll (r a) :=
  forAll_of_forAll (λ x => trans ha) $ h_ind htail
Proof state after:
case cons
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
a₁ : α
as : List α
h_ind : ∀ {a : α}, Ascending r (a :: as) → forAll (r a) as
a : α
ha : r a a₁
htail : Ascending r (a₁ :: as)
this : forAll (r a) as
⊢ forAll (r a) (a₁ :: as)
Theorem: List.Ascending.forAll_of_tail
Proof state before:
case cons
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
a₁ : α
as : List α
h_ind : ∀ {a : α}, Ascending r (a :: as) → forAll (r a) as
a : α
ha : r a a₁
htail : Ascending r (a₁ :: as)
this : forAll (r a) as
⊢ forAll (r a) (a₁ :: as)
Tactic:
exact And.intro ha this
Proof state after:
no goals
Theorem: List.Ascending.forAll_of_predHead
Proof state before:
α : Type u
r : α → α → Prop
p : α → Prop
as : List α
⊢ (∀ (a b : α), p a → r a b → p b) → predHead p as → Ascending r as → forAll p as
Tactic:
induction as
Proof state after:
case nil
α : Type u
r : α → α → Prop
p : α → Prop
⊢ (∀ (a b : α), p a → r a b → p b) → predHead p [] → Ascending r [] → forAll p []

case cons
α : Type u
r : α → α → Prop
p : α → Prop
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ (a b : α), p a → r a b → p b) → predHead p tail✝ → Ascending r tail✝ → forAll p tail✝
⊢ (∀ (a b : α), p a → r a b → p b) →
    predHead p (head✝ :: tail✝) → Ascending r (head✝ :: tail✝) → forAll p (head✝ :: tail✝)
Theorem: List.Ascending.forAll_of_predHead
Proof state before:
α : Type u
r : α → α → Prop
p : α → Prop
⊢ (∀ (a b : α), p a → r a b → p b) → predHead p [] → Ascending r [] → forAll p []
Tactic:
case nil => intros; exact True.intro
Proof state after:
no goals
Theorem: List.Ascending.forAll_of_predHead
Proof state before:
α : Type u
r : α → α → Prop
p : α → Prop
a : α
as : List α
h_ind : (∀ (a b : α), p a → r a b → p b) → predHead p as → Ascending r as → forAll p as
⊢ (∀ (a b : α), p a → r a b → p b) → predHead p (a :: as) → Ascending r (a :: as) → forAll p (a :: as)
Tactic:
case cons a as h_ind =>
  intro hup hpa hchain
  exact ⟨hpa, h_ind hup (hchain.predHead_tail hup hpa) hchain.tail⟩
Proof state after:
no goals
Theorem: List.Ascending.forAll_of_predHead
Proof state before:
α : Type u
r : α → α → Prop
p : α → Prop
⊢ (∀ (a b : α), p a → r a b → p b) → predHead p [] → Ascending r [] → forAll p []
Tactic:
intros
Proof state after:
α : Type u
r : α → α → Prop
p : α → Prop
a✝² : ∀ (a b : α), p a → r a b → p b
a✝¹ : predHead p []
a✝ : Ascending r []
⊢ forAll p []
Theorem: List.Ascending.forAll_of_predHead
Proof state before:
α : Type u
r : α → α → Prop
p : α → Prop
a✝² : ∀ (a b : α), p a → r a b → p b
a✝¹ : predHead p []
a✝ : Ascending r []
⊢ forAll p []
Tactic:
exact True.intro
Proof state after:
no goals
Theorem: List.Ascending.forAll_of_predHead
Proof state before:
α : Type u
r : α → α → Prop
p : α → Prop
a : α
as : List α
h_ind : (∀ (a b : α), p a → r a b → p b) → predHead p as → Ascending r as → forAll p as
⊢ (∀ (a b : α), p a → r a b → p b) → predHead p (a :: as) → Ascending r (a :: as) → forAll p (a :: as)
Tactic:
intro hup hpa hchain
Proof state after:
α : Type u
r : α → α → Prop
p : α → Prop
a : α
as : List α
h_ind : (∀ (a b : α), p a → r a b → p b) → predHead p as → Ascending r as → forAll p as
hup : ∀ (a b : α), p a → r a b → p b
hpa : predHead p (a :: as)
hchain : Ascending r (a :: as)
⊢ forAll p (a :: as)
Theorem: List.Ascending.forAll_of_predHead
Proof state before:
α : Type u
r : α → α → Prop
p : α → Prop
a : α
as : List α
h_ind : (∀ (a b : α), p a → r a b → p b) → predHead p as → Ascending r as → forAll p as
hup : ∀ (a b : α), p a → r a b → p b
hpa : predHead p (a :: as)
hchain : Ascending r (a :: as)
⊢ forAll p (a :: as)
Tactic:
exact ⟨hpa, h_ind hup (hchain.predHead_tail hup hpa) hchain.tail⟩
Proof state after:
no goals
Theorem: List.Ascending.forAllRel_of_append
Proof state before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
as bs : List α
⊢ Ascending r (as ++ bs) → List.forAllRel r as bs
Tactic:
induction as <;> simp
Proof state after:
case cons
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
head✝ : α
tail✝ : List α
tail_ih✝ : Ascending r (tail✝ ++ bs) → List.forAllRel r tail✝ bs
⊢ Ascending r (head✝ :: (tail✝ ++ bs)) → forAll (r head✝) bs ∧ List.forAllRel r tail✝ bs
Theorem: List.Ascending.forAllRel_of_append
Proof state before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : Ascending r (as ++ bs) → List.forAllRel r as bs
⊢ Ascending r (a :: (as ++ bs)) → forAll (r a) bs ∧ List.forAllRel r as bs
Tactic:
case cons a as h_ind =>
  intro hass
  have := hass.forAll_of_tail; simp at this
  exact And.intro this.right (h_ind hass.tail)
Proof state after:
no goals
Theorem: List.Ascending.forAllRel_of_append
Proof state before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : Ascending r (as ++ bs) → List.forAllRel r as bs
⊢ Ascending r (a :: (as ++ bs)) → forAll (r a) bs ∧ List.forAllRel r as bs
Tactic:
intro hass
Proof state after:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : Ascending r (as ++ bs) → List.forAllRel r as bs
hass : Ascending r (a :: (as ++ bs))
⊢ forAll (r a) bs ∧ List.forAllRel r as bs
Theorem: List.Ascending.forAllRel_of_append
Proof state before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : Ascending r (as ++ bs) → List.forAllRel r as bs
hass : Ascending r (a :: (as ++ bs))
⊢ forAll (r a) bs ∧ List.forAllRel r as bs
Tactic:
have := hass.forAll_of_tail
Proof state after:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : Ascending r (as ++ bs) → List.forAllRel r as bs
hass : Ascending r (a :: (as ++ bs))
this : forAll (r a) (as ++ bs)
⊢ forAll (r a) bs ∧ List.forAllRel r as bs
Theorem: List.Ascending.forAllRel_of_append
Proof state before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : Ascending r (as ++ bs) → List.forAllRel r as bs
hass : Ascending r (a :: (as ++ bs))
this : forAll (r a) (as ++ bs)
⊢ forAll (r a) bs ∧ List.forAllRel r as bs
Tactic:
simp at this
Proof state after:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : Ascending r (as ++ bs) → List.forAllRel r as bs
hass : Ascending r (a :: (as ++ bs))
this : forAll (r a) as ∧ forAll (r a) bs
⊢ forAll (r a) bs ∧ List.forAllRel r as bs
Theorem: List.Ascending.forAllRel_of_append
Proof state before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : Ascending r (as ++ bs) → List.forAllRel r as bs
hass : Ascending r (a :: (as ++ bs))
this : forAll (r a) as ∧ forAll (r a) bs
⊢ forAll (r a) bs ∧ List.forAllRel r as bs
Tactic:
exact And.intro this.right (h_ind hass.tail)
Proof state after:
no goals
Theorem: List.Ascending.cons_of_head_tail
Proof state before:
α : Type u
r : α → α → Prop
a : α
as : List α
⊢ predHead (r a) as → Ascending r as → Ascending r (a :: as)
Tactic:
cases as
Proof state after:
case nil
α : Type u
r : α → α → Prop
a : α
⊢ predHead (r a) [] → Ascending r [] → Ascending r [a]

case cons
α : Type u
r : α → α → Prop
a head✝ : α
tail✝ : List α
⊢ predHead (r a) (head✝ :: tail✝) → Ascending r (head✝ :: tail✝) → Ascending r (a :: head✝ :: tail✝)
Theorem: List.Ascending.cons_of_head_tail
Proof state before:
α : Type u
r : α → α → Prop
a : α
⊢ predHead (r a) [] → Ascending r [] → Ascending r [a]
Tactic:
case nil => exact λ _ _ => Ascending.singleton _
Proof state after:
no goals
Theorem: List.Ascending.cons_of_head_tail
Proof state before:
α : Type u
r : α → α → Prop
a head✝ : α
tail✝ : List α
⊢ predHead (r a) (head✝ :: tail✝) → Ascending r (head✝ :: tail✝) → Ascending r (a :: head✝ :: tail✝)
Tactic:
case cons => exact Ascending.cons
Proof state after:
no goals
Theorem: List.Ascending.cons_of_head_tail
Proof state before:
α : Type u
r : α → α → Prop
a : α
⊢ predHead (r a) [] → Ascending r [] → Ascending r [a]
Tactic:
exact λ _ _ => Ascending.singleton _
Proof state after:
no goals
Theorem: List.Ascending.cons_of_head_tail
Proof state before:
α : Type u
r : α → α → Prop
a head✝ : α
tail✝ : List α
⊢ predHead (r a) (head✝ :: tail✝) → Ascending r (head✝ :: tail✝) → Ascending r (a :: head✝ :: tail✝)
Tactic:
exact Ascending.cons
Proof state after:
no goals
Theorem: List.Ascending.cons_of_forAll
Proof state before:
α : Type u
r : α → α → Prop
a : α
as : List α
⊢ forAll (r a) as → Ascending r as → Ascending r (a :: as)
Tactic:
cases as
Proof state after:
case nil
α : Type u
r : α → α → Prop
a : α
⊢ forAll (r a) [] → Ascending r [] → Ascending r [a]

case cons
α : Type u
r : α → α → Prop
a head✝ : α
tail✝ : List α
⊢ forAll (r a) (head✝ :: tail✝) → Ascending r (head✝ :: tail✝) → Ascending r (a :: head✝ :: tail✝)
Theorem: List.Ascending.cons_of_forAll
Proof state before:
α : Type u
r : α → α → Prop
a : α
⊢ forAll (r a) [] → Ascending r [] → Ascending r [a]
Tactic:
case nil => intros; exact Ascending.singleton a
Proof state after:
no goals
Theorem: List.Ascending.cons_of_forAll
Proof state before:
α : Type u
r : α → α → Prop
a a₁ : α
as : List α
⊢ forAll (r a) (a₁ :: as) → Ascending r (a₁ :: as) → Ascending r (a :: a₁ :: as)
Tactic:
case cons a₁ as =>
  intro h
  exact Ascending.cons h.left
Proof state after:
no goals
Theorem: List.Ascending.cons_of_forAll
Proof state before:
α : Type u
r : α → α → Prop
a : α
⊢ forAll (r a) [] → Ascending r [] → Ascending r [a]
Tactic:
intros
Proof state after:
α : Type u
r : α → α → Prop
a : α
a✝¹ : forAll (r a) []
a✝ : Ascending r []
⊢ Ascending r [a]
Theorem: List.Ascending.cons_of_forAll
Proof state before:
α : Type u
r : α → α → Prop
a : α
a✝¹ : forAll (r a) []
a✝ : Ascending r []
⊢ Ascending r [a]
Tactic:
exact Ascending.singleton a
Proof state after:
no goals
Theorem: List.Ascending.cons_of_forAll
Proof state before:
α : Type u
r : α → α → Prop
a a₁ : α
as : List α
⊢ forAll (r a) (a₁ :: as) → Ascending r (a₁ :: as) → Ascending r (a :: a₁ :: as)
Tactic:
intro h
Proof state after:
α : Type u
r : α → α → Prop
a a₁ : α
as : List α
h : forAll (r a) (a₁ :: as)
⊢ Ascending r (a₁ :: as) → Ascending r (a :: a₁ :: as)
Theorem: List.Ascending.cons_of_forAll
Proof state before:
α : Type u
r : α → α → Prop
a a₁ : α
as : List α
h : forAll (r a) (a₁ :: as)
⊢ Ascending r (a₁ :: as) → Ascending r (a :: a₁ :: as)
Tactic:
exact Ascending.cons h.left
Proof state after:
no goals
Theorem: List.Ascending.append
Proof state before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
as bs : List α
⊢ List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
Tactic:
induction as
Proof state after:
case nil
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
⊢ List.forAllRel r [] bs → Ascending r [] → Ascending r bs → Ascending r ([] ++ bs)

case cons
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
head✝ : α
tail✝ : List α
tail_ih✝ : List.forAllRel r tail✝ bs → Ascending r tail✝ → Ascending r bs → Ascending r (tail✝ ++ bs)
⊢ List.forAllRel r (head✝ :: tail✝) bs →
    Ascending r (head✝ :: tail✝) → Ascending r bs → Ascending r (head✝ :: tail✝ ++ bs)
Theorem: List.Ascending.append
Proof state before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
⊢ List.forAllRel r [] bs → Ascending r [] → Ascending r bs → Ascending r ([] ++ bs)
Tactic:
case nil => dsimp; exact λ _ _ => id
Proof state after:
no goals
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:
case cons a as h_ind =>
  dsimp [forAllRel_cons_left]
  rw [List.forAllRel_cons_left]
  intro h hass hbs
  have htail := h_ind h.right hass.tail hbs
  have hhead : bs.forAll (r a) := h.left
  apply cons_of_forAll _ htail
  rw [forAll_append]
  exact And.intro hass.forAll_of_tail hhead
Proof state after:
no goals
Theorem: List.Ascending.append
Proof state before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
⊢ List.forAllRel r [] bs → Ascending r [] → Ascending r bs → Ascending r ([] ++ bs)
Tactic:
dsimp
Proof state after:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
⊢ True → Ascending r [] → Ascending r bs → Ascending r bs
Theorem: List.Ascending.append
Proof state before:
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
⊢ True → Ascending r [] → Ascending r bs → Ascending r bs
Tactic:
exact λ _ _ => id
Proof state after:
no goals