-- Mathlib/Computability/Tape.lean
theorem BlankRel.trans {Γ} [Inhabited Γ] {l₁ l₂ l₃ : List Γ} :
    BlankRel l₁ l₂ → BlankRel l₂ l₃ → BlankRel l₁ l₃

Proof state:
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ l₃ : List Γ
⊢ BlankRel l₁ l₂ → BlankRel l₂ l₃ → BlankRel l₁ l₃

Tactic:
rintro (h₁ | h₁) (h₂ | h₂)

Result:
case inl.inl
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ l₃ : List Γ
h₁ : BlankExtends l₁ l₂
h₂ : BlankExtends l₂ l₃
⊢ BlankRel l₁ l₃

case inl.inr
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ l₃ : List Γ
h₁ : BlankExtends l₁ l₂
h₂ : BlankExtends l₃ l₂
⊢ BlankRel l₁ l₃

case inr.inl
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ l₃ : List Γ
h₁ : BlankExtends l₂ l₁
h₂ : BlankExtends l₂ l₃
⊢ BlankRel l₁ l₃

case inr.inr
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ l₃ : List Γ
h₁ : BlankExtends l₂ l₁
h₂ : BlankExtends l₃ l₂
⊢ BlankRel l₁ l₃

Proof state:
case inl.inr.inr
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ l₃ : List Γ
h₁ : BlankExtends l₁ l₂
h₂ : BlankExtends l₃ l₂
h : l₃.length ≤ l₁.length
⊢ BlankRel l₁ l₃

Tactic:
exact Or.inr (h₂.above_of_le h₁ h)

Result:
no goals

Proof state:
case inr.inl
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ l₃ : List Γ
h₁ : BlankExtends l₂ l₁
h₂ : BlankExtends l₂ l₃
⊢ BlankRel l₁ l₃

Tactic:
rcases le_total l₁.length l₃.length with h | h

Result:
case inr.inl.inl
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ l₃ : List Γ
h₁ : BlankExtends l₂ l₁
h₂ : BlankExtends l₂ l₃
h : l₁.length ≤ l₃.length
⊢ BlankRel l₁ l₃

case inr.inl.inr
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ l₃ : List Γ
h₁ : BlankExtends l₂ l₁
h₂ : BlankExtends l₂ l₃
h : l₃.length ≤ l₁.length
⊢ BlankRel l₁ l₃

Proof state:
case inl.inl
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ l₃ : List Γ
h₁ : BlankExtends l₁ l₂
h₂ : BlankExtends l₂ l₃
⊢ BlankRel l₁ l₃

Tactic:
exact Or.inl (h₁.trans h₂)

Result:
no goals

Proof state:
case inr.inr
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ l₃ : List Γ
h₁ : BlankExtends l₂ l₁
h₂ : BlankExtends l₃ l₂
⊢ BlankRel l₁ l₃

Tactic:
exact Or.inr (h₂.trans h₁)

Result:
no goals

Proof state:
case inl.inr.inl
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ l₃ : List Γ
h₁ : BlankExtends l₁ l₂
h₂ : BlankExtends l₃ l₂
h : l₁.length ≤ l₃.length
⊢ BlankRel l₁ l₃

Tactic:
exact Or.inl (h₁.above_of_le h₂ h)

Result:
no goals

Proof state:
case inl.inr
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ l₃ : List Γ
h₁ : BlankExtends l₁ l₂
h₂ : BlankExtends l₃ l₂
⊢ BlankRel l₁ l₃

Tactic:
rcases le_total l₁.length l₃.length with h | h

Result:
case inl.inr.inl
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ l₃ : List Γ
h₁ : BlankExtends l₁ l₂
h₂ : BlankExtends l₃ l₂
h : l₁.length ≤ l₃.length
⊢ BlankRel l₁ l₃

case inl.inr.inr
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ l₃ : List Γ
h₁ : BlankExtends l₁ l₂
h₂ : BlankExtends l₃ l₂
h : l₃.length ≤ l₁.length
⊢ BlankRel l₁ l₃

Proof state:
case inr.inl.inr
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ l₃ : List Γ
h₁ : BlankExtends l₂ l₁
h₂ : BlankExtends l₂ l₃
h : l₃.length ≤ l₁.length
⊢ BlankRel l₁ l₃

Tactic:
exact Or.inr (h₂.below_of_le h₁ h)

Result:
no goals

Proof state:
case inr.inl.inl
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ l₃ : List Γ
h₁ : BlankExtends l₂ l₁
h₂ : BlankExtends l₂ l₃
h : l₁.length ≤ l₃.length
⊢ BlankRel l₁ l₃

Tactic:
exact Or.inl (h₁.below_of_le h₂ h)

Result:
no goals