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

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
as : List α
b : β
cs : List γ
⊢ predHead (fun a => r₁ a b) as → predHead (r₂ b) cs → relHead r as cs
Tactic:
cases as <;> cases cs <;> intros <;> try {intros; exact True.intro}
State after:
case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
head✝¹ : α
tail✝¹ : List α
head✝ : γ
tail✝ : List γ
a✝¹ : predHead (fun a => r₁ a b) (head✝¹ :: tail✝¹)
a✝ : predHead (r₂ b) (head✝ :: tail✝)
⊢ relHead r (head✝¹ :: tail✝¹) (head✝ :: tail✝)

State before:
case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
head✝¹ : α
tail✝¹ : List α
head✝ : γ
tail✝ : List γ
a✝¹ : predHead (fun a => r₁ a b) (head✝¹ :: tail✝¹)
a✝ : predHead (r₂ b) (head✝ :: tail✝)
⊢ relHead r (head✝¹ :: tail✝¹) (head✝ :: tail✝)
Tactic:
dsimp [relHead]
State after:
case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
head✝¹ : α
tail✝¹ : List α
head✝ : γ
tail✝ : List γ
a✝¹ : predHead (fun a => r₁ a b) (head✝¹ :: tail✝¹)
a✝ : predHead (r₂ b) (head✝ :: tail✝)
⊢ r head✝¹ head✝

State before:
case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
head✝¹ : α
tail✝¹ : List α
head✝ : γ
tail✝ : List γ
a✝¹ : predHead (fun a => r₁ a b) (head✝¹ :: tail✝¹)
a✝ : predHead (r₂ b) (head✝ :: tail✝)
⊢ r head✝¹ head✝
Tactic:
dsimp [predHead] at *
State after:
case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
head✝¹ : α
tail✝¹ : List α
head✝ : γ
tail✝ : List γ
a✝¹ : r₁ head✝¹ b
a✝ : r₂ b head✝
⊢ r head✝¹ head✝

State before:
case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
head✝¹ : α
tail✝¹ : List α
head✝ : γ
tail✝ : List γ
a✝¹ : r₁ head✝¹ b
a✝ : r₂ b head✝
⊢ r head✝¹ head✝
Tactic:
exact trans ‹r₁ _ b› ‹r₂ b _›
State after:
no goals

State before:
case cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
head✝ : α
tail✝ : List α
a✝¹ : predHead (fun a => r₁ a b) (head✝ :: tail✝)
a✝ : predHead (r₂ b) []
⊢ relHead r (head✝ :: tail✝) []
Tactic:
exact True.intro
State after:
no goals