Theorem: List.Ascending.filterMap (Algdata/Data/List/Ascending.lean)

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
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)

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
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✝))

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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))

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
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)

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
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)

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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)

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
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)

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
State after:
no goals

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
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)

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]
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✝)

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]
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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
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)

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
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)

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
State after:
no goals

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
State after:
no goals

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
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

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
State after:
no goals

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
State after:
no goals

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
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)

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
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)

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
State after:
no goals

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
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₁

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
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₁

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals