internlm/Lean-Github huggingface dataset:
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)
hchain : Ascending r (a :: as)
⊢ Ascending r' (filterMap f (a :: as))
Tactic:
unfold filterMap
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'
    (match f a with
    | none => filterMap f as
    | some b => b :: 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₂
a : α
as : List α
h_ind : Ascending r as → Ascending r' (filterMap f as)
hchain : Ascending r (a :: as)
⊢ Ascending r'
    (match f a with
    | none => filterMap f as
    | some b => b :: filterMap f as)
Tactic:
cases hfa : f a <;> dsimp
Proof state after:
case none
α : 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)
hfa : f a = none
⊢ Ascending r' (filterMap f as)

case some
α : 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)
val✝ : β
hfa : f a = some val✝
⊢ Ascending r' (val✝ :: 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₂
a : α
as : List α
h_ind : Ascending r as → Ascending r' (filterMap f as)
hchain : Ascending r (a :: as)
hfa : f a = none
⊢ Ascending r' (filterMap f as)
Tactic:
case none => 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₂
a : α
as : List α
h_ind : Ascending r as → Ascending r' (filterMap f as)
hchain : Ascending r (a :: as)
b : β
hfa : f a = some b
⊢ Ascending r' (b :: filterMap f as)
Tactic:
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₂
a : α
as : List α
h_ind : Ascending r as → Ascending r' (filterMap f as)
hchain : Ascending r (a :: as)
hfa : f a = none
⊢ Ascending r' (filterMap f as)
Tactic:
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₂
a : α
as : List α
h_ind : Ascending r as → Ascending r' (filterMap f as)
hchain : Ascending r (a :: as)
b : β
hfa : f a = some b
⊢ Ascending r' (b :: filterMap f as)
Tactic:
apply cons_of_forAll
Proof state after:
case a
α : 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)
b : β
hfa : f a = some b
⊢ forAll (r' b) (filterMap f as)

case a
α : 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)
b : β
hfa : f a = some b
⊢ Ascending r' (filterMap f as)
Theorem: List.Ascending.filterMap
Proof state before:
case a
α : 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)
b : β
hfa : f a = some b
⊢ forAll (r' b) (filterMap f as)

case a
α : 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)
b : β
hfa : f a = some b
⊢ Ascending r' (filterMap f as)
Tactic:
. 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
Proof state after:
case a
α : 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)
b : β
hfa : f a = some b
⊢ Ascending r' (filterMap f as)
Theorem: List.Ascending.filterMap
Proof state before:
case a
α : 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)
b : β
hfa : f a = some b
⊢ Ascending r' (filterMap f as)
Tactic:
. exact h_ind hchain.tail
Proof state after:
no goals
Theorem: List.Ascending.filterMap
Proof state before:
case a
α : 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)
b : β
hfa : f a = some b
⊢ forAll (r' b) (filterMap f as)
Tactic:
clear h_ind
Proof state after:
case a
α : 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 α
hchain : Ascending r (a :: as)
b : β
hfa : f a = some b
⊢ forAll (r' b) (filterMap f as)
Theorem: List.Ascending.filterMap
Proof state before:
case a
α : 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 α
hchain : Ascending r (a :: as)
b : β
hfa : f a = some b
⊢ forAll (r' b) (filterMap f as)
Tactic:
induction as <;> dsimp [filterMap]
Proof state after:
case a.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₂
a : α
b : β
hfa : f a = some b
hchain : Ascending r [a]
⊢ forAll (r' b) []

case a.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₂
a : α
b : β
hfa : f a = some b
head✝ : α
tail✝ : List α
tail_ih✝ : Ascending r (a :: tail✝) → forAll (r' b) (filterMap f tail✝)
hchain : Ascending r (a :: head✝ :: tail✝)
⊢ forAll (r' b)
    (match f head✝ with
    | none => filterMap f tail✝
    | some b => b :: filterMap f 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₂
a : α
b : β
hfa : f a = some b
hchain : Ascending r [a]
⊢ forAll (r' b) []
Tactic:
case a.nil => dsimp [List.forAll]
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 : α
b : β
hfa : f a = some b
a₁ : α
as : List α
h_ind₁ : Ascending r (a :: as) → forAll (r' b) (filterMap f as)
hchain : Ascending r (a :: a₁ :: as)
⊢ forAll (r' b)
    (match f a₁ with
    | none => filterMap f as
    | some b => b :: filterMap f as)
Tactic:
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
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 : α
b : β
hfa : f a = some b
hchain : Ascending r [a]
⊢ forAll (r' b) []
Tactic:
dsimp [List.forAll]
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 : α
b : β
hfa : f a = some b
a₁ : α
as : List α
h_ind₁ : Ascending r (a :: as) → forAll (r' b) (filterMap f as)
hchain : Ascending r (a :: a₁ :: as)
⊢ forAll (r' b)
    (match f a₁ with
    | none => filterMap f as
    | some b => b :: filterMap f as)
Tactic:
have hchainaas : Ascending r (a::as) := by
  apply hchain.tail.subst_head
  exact λ _ h => trans hchain.head h
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 : α
b : β
hfa : f a = some b
a₁ : α
as : List α
h_ind₁ : Ascending r (a :: as) → forAll (r' b) (filterMap f as)
hchain : Ascending r (a :: a₁ :: as)
hchainaas : Ascending r (a :: as)
⊢ forAll (r' b)
    (match f a₁ with
    | none => filterMap f as
    | some b => b :: 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₂
a : α
b : β
hfa : f a = some b
a₁ : α
as : List α
h_ind₁ : Ascending r (a :: as) → forAll (r' b) (filterMap f as)
hchain : Ascending r (a :: a₁ :: as)
hchainaas : Ascending r (a :: as)
⊢ forAll (r' b)
    (match f a₁ with
    | none => filterMap f as
    | some b => b :: filterMap f as)
Tactic:
cases hfa₁ : f a₁ <;> dsimp
Proof state after:
case none
α : 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 : α
b : β
hfa : f a = some b
a₁ : α
as : List α
h_ind₁ : Ascending r (a :: as) → forAll (r' b) (filterMap f as)
hchain : Ascending r (a :: a₁ :: as)
hchainaas : Ascending r (a :: as)
hfa₁ : f a₁ = none
⊢ forAll (r' b) (filterMap f as)

case some
α : 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 : α
b : β
hfa : f a = some b
a₁ : α
as : List α
h_ind₁ : Ascending r (a :: as) → forAll (r' b) (filterMap f as)
hchain : Ascending r (a :: a₁ :: as)
hchainaas : Ascending r (a :: as)
val✝ : β
hfa₁ : f a₁ = some val✝
⊢ forAll (r' b) (val✝ :: 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₂
a : α
b : β
hfa : f a = some b
a₁ : α
as : List α
h_ind₁ : Ascending r (a :: as) → forAll (r' b) (filterMap f as)
hchain : Ascending r (a :: a₁ :: as)
hchainaas : Ascending r (a :: as)
hfa₁ : f a₁ = none
⊢ forAll (r' b) (filterMap f as)
Tactic:
case none => exact h_ind₁ hchainaas
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 : α
b : β
hfa : f a = some b
a₁ : α
as : List α
h_ind₁ : Ascending r (a :: as) → forAll (r' b) (filterMap f as)
hchain : Ascending r (a :: a₁ :: as)
hchainaas : Ascending r (a :: as)
b₁ : β
hfa₁ : f a₁ = some b₁
⊢ forAll (r' b) (b₁ :: filterMap f as)
Tactic:
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
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 : α
b : β
hfa : f a = some b
a₁ : α
as : List α
h_ind₁ : Ascending r (a :: as) → forAll (r' b) (filterMap f as)
hchain : Ascending r (a :: a₁ :: as)
⊢ Ascending r (a :: as)
Tactic:
apply hchain.tail.subst_head
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 : α
b : β
hfa : f a = some b
a₁ : α
as : List α
h_ind₁ : Ascending r (a :: as) → forAll (r' b) (filterMap f as)
hchain : Ascending r (a :: a₁ :: as)
⊢ ∀ (c : α), r a₁ c → r a c
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 : α
b : β
hfa : f a = some b
a₁ : α
as : List α
h_ind₁ : Ascending r (a :: as) → forAll (r' b) (filterMap f as)
hchain : Ascending r (a :: a₁ :: as)
⊢ ∀ (c : α), r a₁ c → r a c
Tactic:
exact λ _ h => trans hchain.head h
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 : α
b : β
hfa : f a = some b
a₁ : α
as : List α
h_ind₁ : Ascending r (a :: as) → forAll (r' b) (filterMap f as)
hchain : Ascending r (a :: a₁ :: as)
hchainaas : Ascending r (a :: as)
hfa₁ : f a₁ = none
⊢ forAll (r' b) (filterMap f as)
Tactic:
exact h_ind₁ hchainaas
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 : α
b : β
hfa : f a = some b
a₁ : α
as : List α
h_ind₁ : Ascending r (a :: as) → forAll (r' b) (filterMap f as)
hchain : Ascending r (a :: a₁ :: as)
hchainaas : Ascending r (a :: as)
b₁ : β
hfa₁ : f a₁ = some b₁
⊢ forAll (r' b) (b₁ :: filterMap f as)
Tactic:
constructor
Proof state after:
case left
α : 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 : α
b : β
hfa : f a = some b
a₁ : α
as : List α
h_ind₁ : Ascending r (a :: as) → forAll (r' b) (filterMap f as)
hchain : Ascending r (a :: a₁ :: as)
hchainaas : Ascending r (a :: as)
b₁ : β
hfa₁ : f a₁ = some b₁
⊢ r' b b₁

case right
α : 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 : α
b : β
hfa : f a = some b
a₁ : α
as : List α
h_ind₁ : Ascending r (a :: as) → forAll (r' b) (filterMap f as)
hchain : Ascending r (a :: a₁ :: as)
hchainaas : Ascending r (a :: as)
b₁ : β
hfa₁ : f a₁ = some b₁
⊢ forAll (r' b) (filterMap f as)
Theorem: List.Ascending.filterMap
Proof state before:
case left
α : 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 : α
b : β
hfa : f a = some b
a₁ : α
as : List α
h_ind₁ : Ascending r (a :: as) → forAll (r' b) (filterMap f as)
hchain : Ascending r (a :: a₁ :: as)
hchainaas : Ascending r (a :: as)
b₁ : β
hfa₁ : f a₁ = some b₁
⊢ r' b b₁

case right
α : 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 : α
b : β
hfa : f a = some b
a₁ : α
as : List α
h_ind₁ : Ascending r (a :: as) → forAll (r' b) (filterMap f as)
hchain : Ascending r (a :: a₁ :: as)
hchainaas : Ascending r (a :: as)
b₁ : β
hfa₁ : f a₁ = some b₁
⊢ forAll (r' b) (filterMap f as)
Tactic:
. have := rel_pres a a₁ hchain.head
  rw [hfa, hfa₁] at this
  exact this b b₁ rfl rfl
Proof state after:
case right
α : 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 : α
b : β
hfa : f a = some b
a₁ : α
as : List α
h_ind₁ : Ascending r (a :: as) → forAll (r' b) (filterMap f as)
hchain : Ascending r (a :: a₁ :: as)
hchainaas : Ascending r (a :: as)
b₁ : β
hfa₁ : f a₁ = some b₁
⊢ forAll (r' b) (filterMap f as)
Theorem: List.Ascending.filterMap
Proof state before:
case right
α : 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 : α
b : β
hfa : f a = some b
a₁ : α
as : List α
h_ind₁ : Ascending r (a :: as) → forAll (r' b) (filterMap f as)
hchain : Ascending r (a :: a₁ :: as)
hchainaas : Ascending r (a :: as)
b₁ : β
hfa₁ : f a₁ = some b₁
⊢ forAll (r' b) (filterMap f as)
Tactic:
. exact h_ind₁ hchainaas
Proof state after:
no goals
Theorem: List.Ascending.filterMap
Proof state before:
case left
α : 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 : α
b : β
hfa : f a = some b
a₁ : α
as : List α
h_ind₁ : Ascending r (a :: as) → forAll (r' b) (filterMap f as)
hchain : Ascending r (a :: a₁ :: as)
hchainaas : Ascending r (a :: as)
b₁ : β
hfa₁ : f a₁ = some b₁
⊢ r' b b₁
Tactic:
have := rel_pres a a₁ hchain.head
Proof state after:
case left
α : 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 : α
b : β
hfa : f a = some b
a₁ : α
as : List α
h_ind₁ : Ascending r (a :: as) → forAll (r' b) (filterMap f as)
hchain : Ascending r (a :: a₁ :: as)
hchainaas : Ascending r (a :: as)
b₁ : β
hfa₁ : f a₁ = some b₁
this : ∀ (b₁ b₂ : β), f a = some b₁ → f a₁ = some b₂ → r' b₁ b₂
⊢ r' b b₁
Theorem: List.Ascending.filterMap
Proof state before:
case left
α : 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 : α
b : β
hfa : f a = some b
a₁ : α
as : List α
h_ind₁ : Ascending r (a :: as) → forAll (r' b) (filterMap f as)
hchain : Ascending r (a :: a₁ :: as)
hchainaas : Ascending r (a :: as)
b₁ : β
hfa₁ : f a₁ = some b₁
this : ∀ (b₁ b₂ : β), f a = some b₁ → f a₁ = some b₂ → r' b₁ b₂
⊢ r' b b₁
Tactic:
rw [hfa, hfa₁] at this
Proof state after:
case left
α : 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 : α
b : β
hfa : f a = some b
a₁ : α
as : List α
h_ind₁ : Ascending r (a :: as) → forAll (r' b) (filterMap f as)
hchain : Ascending r (a :: a₁ :: as)
hchainaas : Ascending r (a :: as)
b₁ : β
hfa₁ : f a₁ = some b₁
this : ∀ (b₁_1 b₂ : β), some b = some b₁_1 → some b₁ = some b₂ → r' b₁_1 b₂
⊢ r' b b₁
Theorem: List.Ascending.filterMap
Proof state before:
case left
α : 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 : α
b : β
hfa : f a = some b
a₁ : α
as : List α
h_ind₁ : Ascending r (a :: as) → forAll (r' b) (filterMap f as)
hchain : Ascending r (a :: a₁ :: as)
hchainaas : Ascending r (a :: as)
b₁ : β
hfa₁ : f a₁ = some b₁
this : ∀ (b₁_1 b₂ : β), some b = some b₁_1 → some b₁ = some b₂ → r' b₁_1 b₂
⊢ r' b b₁
Tactic:
exact this b b₁ rfl rfl
Proof state after:
no goals
Theorem: List.Ascending.filterMap
Proof state before:
case right
α : 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 : α
b : β
hfa : f a = some b
a₁ : α
as : List α
h_ind₁ : Ascending r (a :: as) → forAll (r' b) (filterMap f as)
hchain : Ascending r (a :: a₁ :: as)
hchainaas : Ascending r (a :: as)
b₁ : β
hfa₁ : f a₁ = some b₁
⊢ forAll (r' b) (filterMap f as)
Tactic:
exact h_ind₁ hchainaas
Proof state after:
no goals
Theorem: List.Ascending.filterMap
Proof state before:
case a
α : 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)
b : β
hfa : f a = some b
⊢ Ascending r' (filterMap f as)
Tactic:
exact h_ind hchain.tail
Proof state after:
no goals
Theorem: List.HookedAscending.inl
Proof state before:
α : Type u_1
r : α → α → Prop
as : List α
has : Ascending (flip r) as
⊢ List.forAllRel r as []
Tactic:
simp
Proof state after:
no goals
Theorem: List.HookedAscending.inr
Proof state before:
α : Type u_1
r : α → α → Prop
bs : List α
hbs : Ascending r bs
⊢ List.forAllRel r [] bs
Tactic:
simp
Proof state after:
no goals