case intro.intro
Γ : Type u_1
inst✝ : Inhabited Γ
l : List Γ
i j : ℕ
h : List.length (l ++ List.replicate i default) ≤ List.length (l ++ List.replicate j default)
⊢ BlankExtends (l ++ List.replicate i default) (l ++ List.replicate j default)
Γ : Type u_1
inst✝ : Inhabited Γ
l l₁ l₂ : List Γ
⊢ BlankExtends l l₁ → BlankExtends l l₂ → List.length l₁ ≤ List.length l₂ → BlankExtends l₁ l₂
rintro ⟨i, rfl⟩ ⟨j, rfl⟩ h
case intro.intro
Γ : Type u_1
inst✝ : Inhabited Γ
l : List Γ
i j : ℕ
h : List.length (l ++ List.replicate i default) ≤ List.length (l ++ List.replicate j default)
⊢ l ++ List.replicate j default = l ++ List.replicate i default ++ List.replicate (j - i) default
case intro.intro
Γ : Type u_1
inst✝ : Inhabited Γ
l : List Γ
i j : ℕ
h : List.length (l ++ List.replicate i default) ≤ List.length (l ++ List.replicate j default)
⊢ BlankExtends (l ++ List.replicate i default) (l ++ List.replicate j default)
use j - i
case intro.intro
Γ : Type u_1
inst✝ : Inhabited Γ
l : List Γ
i j : ℕ
h : i ≤ j
⊢ l ++ List.replicate j default = l ++ List.replicate i default ++ List.replicate (j - i) default
case intro.intro
Γ : Type u_1
inst✝ : Inhabited Γ
l : List Γ
i j : ℕ
h : List.length (l ++ List.replicate i default) ≤ List.length (l ++ List.replicate j default)
⊢ l ++ List.replicate j default = l ++ List.replicate i default ++ List.replicate (j - i) default
simp only [List.length_append, add_le_add_iff_left, List.length_replicate] at h
no goals
case intro.intro
Γ : Type u_1
inst✝ : Inhabited Γ
l : List Γ
i j : ℕ
h : i ≤ j
⊢ l ++ List.replicate j default = l ++ List.replicate i default ++ List.replicate (j - i) default
simp only [← List.replicate_add, add_tsub_cancel_of_le h, List.append_assoc]