Theorem: List.forAllRel_trans (Algdata/Data/List/Prop.lean)

State before:
α✝ : Type ?u.8039
β✝ : Type ?u.8042
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
as : List α
bs : List β
cs : List γ
⊢ bs ≠ [] → List.forAllRel r₁ as bs → List.forAllRel r₂ bs cs → List.forAllRel r as cs
Tactic:
intro hbs hab hbc
State after:
α✝ : Type ?u.8039
β✝ : Type ?u.8042
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
as : List α
bs : List β
cs : List γ
hbs : bs ≠ []
hab : List.forAllRel r₁ as bs
hbc : List.forAllRel r₂ bs cs
⊢ List.forAllRel r as cs

State before:
α✝ : Type ?u.8039
β✝ : Type ?u.8042
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
as : List α
bs : List β
cs : List γ
hbs : bs ≠ []
hab : List.forAllRel r₁ as bs
hbc : List.forAllRel r₂ bs cs
⊢ List.forAllRel r as cs
Tactic:
cases bs
State after:
case nil
α✝ : Type ?u.8039
β✝ : Type ?u.8042
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
as : List α
cs : List γ
hbs : [] ≠ []
hab : List.forAllRel r₁ as []
hbc : List.forAllRel r₂ [] cs
⊢ List.forAllRel r as cs

case cons
α✝ : Type ?u.8039
β✝ : Type ?u.8042
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
as : List α
cs : List γ
head✝ : β
tail✝ : List β
hbs : head✝ :: tail✝ ≠ []
hab : List.forAllRel r₁ as (head✝ :: tail✝)
hbc : List.forAllRel r₂ (head✝ :: tail✝) cs
⊢ List.forAllRel r as cs

State before:
α✝ : Type ?u.8039
β✝ : Type ?u.8042
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
as : List α
cs : List γ
hbs : [] ≠ []
hab : List.forAllRel r₁ as []
hbc : List.forAllRel r₂ [] cs
⊢ List.forAllRel r as cs
Tactic:
case nil => exact absurd rfl hbs
State after:
no goals

State before:
α✝ : Type ?u.8039
β✝ : Type ?u.8042
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
as : List α
cs : List γ
b : β
bs : List β
hbs : b :: bs ≠ []
hab : List.forAllRel r₁ as (b :: bs)
hbc : List.forAllRel r₂ (b :: bs) cs
⊢ List.forAllRel r as cs
Tactic:
case cons b bs =>
  simp at hab hbc
  exact forAllRel_of_trans_forAll_forAll hab.left hbc.left
State after:
no goals

State before:
α✝ : Type ?u.8039
β✝ : Type ?u.8042
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
as : List α
cs : List γ
hbs : [] ≠ []
hab : List.forAllRel r₁ as []
hbc : List.forAllRel r₂ [] cs
⊢ List.forAllRel r as cs
Tactic:
exact absurd rfl hbs
State after:
no goals

State before:
α✝ : Type ?u.8039
β✝ : Type ?u.8042
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
as : List α
cs : List γ
b : β
bs : List β
hbs : b :: bs ≠ []
hab : List.forAllRel r₁ as (b :: bs)
hbc : List.forAllRel r₂ (b :: bs) cs
⊢ List.forAllRel r as cs
Tactic:
simp at hab hbc
State after:
α✝ : Type ?u.8039
β✝ : Type ?u.8042
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
as : List α
cs : List γ
b : β
bs : List β
hbs : b :: bs ≠ []
hab : forAll (fun x => r₁ x b) as ∧ List.forAllRel r₁ as bs
hbc : forAll (r₂ b) cs ∧ List.forAllRel r₂ bs cs
⊢ List.forAllRel r as cs

State before:
α✝ : Type ?u.8039
β✝ : Type ?u.8042
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
as : List α
cs : List γ
b : β
bs : List β
hbs : b :: bs ≠ []
hab : forAll (fun x => r₁ x b) as ∧ List.forAllRel r₁ as bs
hbc : forAll (r₂ b) cs ∧ List.forAllRel r₂ bs cs
⊢ List.forAllRel r as cs
Tactic:
exact forAllRel_of_trans_forAll_forAll hab.left hbc.left
State after:
no goals