Theorem: List.Subperm.exists_intermediate (LeanCamCombi/Mathlib/Data/List/DropRight.lean)

State before:
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
hl : l₀ <+~ l₂
h₀ : l₀.length ≤ n
h₂ : n ≤ l₂.length
⊢ ∃ l₁, l₀ <+~ l₁ ∧ l₁ <+~ l₂ ∧ l₁.length = n
Tactic:
obtain ⟨l₀', hl₀, hl'⟩ := hl
State after:
case intro.intro
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
h₀ : l₀.length ≤ n
h₂ : n ≤ l₂.length
l₀' : List α
hl₀ : l₀' ~ l₀
hl' : l₀' <+ l₂
⊢ ∃ l₁, l₀ <+~ l₁ ∧ l₁ <+~ l₂ ∧ l₁.length = n

State before:
case intro.intro
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
h₀ : l₀.length ≤ n
h₂ : n ≤ l₂.length
l₀' : List α
hl₀ : l₀' ~ l₀
hl' : l₀' <+ l₂
⊢ ∃ l₁, l₀ <+~ l₁ ∧ l₁ <+~ l₂ ∧ l₁.length = n
Tactic:
obtain ⟨l₁, h₀₁, h₁₂, hn⟩ := hl'.exists_intermediate (hl₀.length_eq.trans_le h₀) h₂
State after:
case intro.intro.intro.intro.intro
α : Type u_1
l l' l₀ l₁✝ l₂ : List α
a b : α
m n : ℕ
h₀ : l₀.length ≤ n
h₂ : n ≤ l₂.length
l₀' : List α
hl₀ : l₀' ~ l₀
hl' : l₀' <+ l₂
l₁ : List α
h₀₁ : l₀' <+ l₁
h₁₂ : l₁ <+ l₂
hn : l₁.length = n
⊢ ∃ l₁, l₀ <+~ l₁ ∧ l₁ <+~ l₂ ∧ l₁.length = n

State before:
case intro.intro.intro.intro.intro
α : Type u_1
l l' l₀ l₁✝ l₂ : List α
a b : α
m n : ℕ
h₀ : l₀.length ≤ n
h₂ : n ≤ l₂.length
l₀' : List α
hl₀ : l₀' ~ l₀
hl' : l₀' <+ l₂
l₁ : List α
h₀₁ : l₀' <+ l₁
h₁₂ : l₁ <+ l₂
hn : l₁.length = n
⊢ ∃ l₁, l₀ <+~ l₁ ∧ l₁ <+~ l₂ ∧ l₁.length = n
Tactic:
exact ⟨l₁, ⟨_, hl₀, h₀₁⟩, h₁₂.subperm, hn⟩
State after:
no goals