case intro.intro
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : List.length l₁ ≤ List.length l₂
⊢ BlankExtends l₁ l₂
Γ : 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, e⟩ h
case intro.intro
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : List.length l₁ ≤ List.length l₂
⊢ l₂ = l₁ ++ List.replicate (i - j) default
case intro.intro
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : List.length l₁ ≤ List.length l₂
⊢ BlankExtends l₁ l₂
use i - j
case intro.intro
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : List.length l₁ ≤ List.length l₂
⊢ l₁ ++ List.replicate i default = l₁ ++ List.replicate (i - j) default ++ List.replicate j default
case intro.intro
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : List.length l₁ ≤ List.length l₂
⊢ l₂ = l₁ ++ List.replicate (i - j) default
refine' List.append_right_cancel (e.symm.trans _)
case intro.intro
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : List.length l₁ ≤ List.length l₂
⊢ j ≤ i
case intro.intro
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : List.length l₁ ≤ List.length l₂
⊢ l₁ ++ List.replicate i default = l₁ ++ List.replicate (i - j) default ++ List.replicate j default
rw [List.append_assoc, ← List.replicate_add, tsub_add_cancel_of_le]
case intro.intro
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
h : List.length l₁ ≤ List.length l₂
e : List.length (l₁ ++ List.replicate i default) = List.length (l₂ ++ List.replicate j default)
⊢ j ≤ i
case intro.intro
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : List.length l₁ ≤ List.length l₂
⊢ j ≤ i
apply_fun List.length at e
case intro.intro
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
h : List.length l₁ ≤ List.length l₂
e : List.length l₁ + i = List.length l₂ + j
⊢ j ≤ i
case intro.intro
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
h : List.length l₁ ≤ List.length l₂
e : List.length (l₁ ++ List.replicate i default) = List.length (l₂ ++ List.replicate j default)
⊢ j ≤ i
simp only [List.length_append, List.length_replicate] at e
no goals
case intro.intro
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
h : List.length l₁ ≤ List.length l₂
e : List.length l₁ + i = List.length l₂ + j
⊢ j ≤ i
rwa [← add_le_add_iff_left, e, add_le_add_iff_right]