Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1
⊢ mk l₁ = mk l₂
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
⊢ (∀ (i_1 : ℕ), nth L₁ i_1 = nth L₂ i_1) → L₁ = L₂
refine' ListBlank.induction_on L₁ fun l₁ ↦ ListBlank.induction_on L₂ fun l₂ H ↦ _
case inr
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1
this :
  ∀ {Γ : Type u_1} [i : Inhabited Γ] {L₁ L₂ : ListBlank Γ} (l₁ l₂ : List Γ),
    (∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1) → List.length l₁ ≤ List.length l₂ → mk l₁ = mk l₂
h : ¬List.length l₁ ≤ List.length l₂
⊢ mk l₁ = mk l₂

Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1
h : List.length l₁ ≤ List.length l₂
⊢ mk l₁ = mk l₂
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1
⊢ mk l₁ = mk l₂
wlog h : l₁.length ≤ l₂.length
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1
h : List.length l₁ ≤ List.length l₂
⊢ l₂ = l₁ ++ List.replicate (List.length l₂ - List.length l₁) default
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1
h : List.length l₁ ≤ List.length l₂
⊢ mk l₁ = mk l₂
refine' Quotient.sound' (Or.inl ⟨l₂.length - l₁.length, _⟩)
case refine'_1
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1
h : List.length l₁ ≤ List.length l₂
⊢ List.length l₂ = List.length (l₁ ++ List.replicate (List.length l₂ - List.length l₁) default)

case refine'_2
Γ : Type u_1
i✝ : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i : ℕ), nth (mk l₁) i = nth (mk l₂) i
h✝ : List.length l₁ ≤ List.length l₂
i : ℕ
h : i < List.length l₂
h₂ : i < List.length (l₁ ++ List.replicate (List.length l₂ - List.length l₁) default)
⊢ List.get (l₁ ++ List.replicate (List.length l₂ - List.length l₁) default) { val := i, isLt := h₂ } =
    List.get l₂ { val := i, isLt := h }
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1
h : List.length l₁ ≤ List.length l₂
⊢ l₂ = l₁ ++ List.replicate (List.length l₂ - List.length l₁) default
refine' List.ext_get _ fun i h h₂ ↦ Eq.symm _
case refine'_2
Γ : Type u_1
i✝ : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i : ℕ), List.getI l₁ i = List.getI l₂ i
h✝ : List.length l₁ ≤ List.length l₂
i : ℕ
h : i < List.length l₂
h₂ : i < List.length (l₁ ++ List.replicate (List.length l₂ - List.length l₁) default)
⊢ List.get (l₁ ++ List.replicate (List.length l₂ - List.length l₁) default) { val := i, isLt := h₂ } =
    List.get l₂ { val := i, isLt := h }
case refine'_2
Γ : Type u_1
i✝ : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i : ℕ), nth (mk l₁) i = nth (mk l₂) i
h✝ : List.length l₁ ≤ List.length l₂
i : ℕ
h : i < List.length l₂
h₂ : i < List.length (l₁ ++ List.replicate (List.length l₂ - List.length l₁) default)
⊢ List.get (l₁ ++ List.replicate (List.length l₂ - List.length l₁) default) { val := i, isLt := h₂ } =
    List.get l₂ { val := i, isLt := h }
simp only [ListBlank.nth_mk] at H
case refine'_2.inl
Γ : Type u_1
i✝ : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i : ℕ), List.getI l₁ i = List.getI l₂ i
h✝ : List.length l₁ ≤ List.length l₂
i : ℕ
h : i < List.length l₂
h₂ : i < List.length (l₁ ++ List.replicate (List.length l₂ - List.length l₁) default)
h' : i < List.length l₁
⊢ List.get (l₁ ++ List.replicate (List.length l₂ - List.length l₁) default) { val := i, isLt := h₂ } =
    List.get l₂ { val := i, isLt := h }

case refine'_2.inr
Γ : Type u_1
i✝ : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i : ℕ), List.getI l₁ i = List.getI l₂ i
h✝ : List.length l₁ ≤ List.length l₂
i : ℕ
h : i < List.length l₂
h₂ : i < List.length (l₁ ++ List.replicate (List.length l₂ - List.length l₁) default)
h' : List.length l₁ ≤ i
⊢ List.get (l₁ ++ List.replicate (List.length l₂ - List.length l₁) default) { val := i, isLt := h₂ } =
    List.get l₂ { val := i, isLt := h }
case refine'_2
Γ : Type u_1
i✝ : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i : ℕ), List.getI l₁ i = List.getI l₂ i
h✝ : List.length l₁ ≤ List.length l₂
i : ℕ
h : i < List.length l₂
h₂ : i < List.length (l₁ ++ List.replicate (List.length l₂ - List.length l₁) default)
⊢ List.get (l₁ ++ List.replicate (List.length l₂ - List.length l₁) default) { val := i, isLt := h₂ } =
    List.get l₂ { val := i, isLt := h }
cases' lt_or_le i l₁.length with h' h'
case inr.inr.H
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1
this :
  ∀ {Γ : Type u_1} [i : Inhabited Γ] {L₁ L₂ : ListBlank Γ} (l₁ l₂ : List Γ),
    (∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1) → List.length l₁ ≤ List.length l₂ → mk l₁ = mk l₂
h : ¬List.length l₁ ≤ List.length l₂
h✝ : List.length l₂ ≤ List.length l₁
⊢ ∀ (i_1 : ℕ), nth (mk l₂) i_1 = nth (mk l₁) i_1
case inr
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1
this :
  ∀ {Γ : Type u_1} [i : Inhabited Γ] {L₁ L₂ : ListBlank Γ} (l₁ l₂ : List Γ),
    (∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1) → List.length l₁ ≤ List.length l₂ → mk l₁ = mk l₂
h : ¬List.length l₁ ≤ List.length l₂
⊢ mk l₁ = mk l₂
cases le_total l₁.length l₂.length <;> [skip; symm] <;> apply this <;> try assumption
case inr.inr.H
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1
this :
  ∀ {Γ : Type u_1} [i : Inhabited Γ] {L₁ L₂ : ListBlank Γ} (l₁ l₂ : List Γ),
    (∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1) → List.length l₁ ≤ List.length l₂ → mk l₁ = mk l₂
h : ¬List.length l₁ ≤ List.length l₂
h✝ : List.length l₂ ≤ List.length l₁
i✝ : ℕ
⊢ nth (mk l₂) i✝ = nth (mk l₁) i✝
case inr.inr.H
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1
this :
  ∀ {Γ : Type u_1} [i : Inhabited Γ] {L₁ L₂ : ListBlank Γ} (l₁ l₂ : List Γ),
    (∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1) → List.length l₁ ≤ List.length l₂ → mk l₁ = mk l₂
h : ¬List.length l₁ ≤ List.length l₂
h✝ : List.length l₂ ≤ List.length l₁
⊢ ∀ (i_1 : ℕ), nth (mk l₂) i_1 = nth (mk l₁) i_1
intro
no goals
case inr.inr.H
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1
this :
  ∀ {Γ : Type u_1} [i : Inhabited Γ] {L₁ L₂ : ListBlank Γ} (l₁ l₂ : List Γ),
    (∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1) → List.length l₁ ≤ List.length l₂ → mk l₁ = mk l₂
h : ¬List.length l₁ ≤ List.length l₂
h✝ : List.length l₂ ≤ List.length l₁
i✝ : ℕ
⊢ nth (mk l₂) i✝ = nth (mk l₁) i✝
rw [H]
no goals
case inr.inr.h
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1
this :
  ∀ {Γ : Type u_1} [i : Inhabited Γ] {L₁ L₂ : ListBlank Γ} (l₁ l₂ : List Γ),
    (∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1) → List.length l₁ ≤ List.length l₂ → mk l₁ = mk l₂
h : ¬List.length l₁ ≤ List.length l₂
h✝ : List.length l₂ ≤ List.length l₁
⊢ List.length l₂ ≤ List.length l₁
assumption
no goals
case refine'_1
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1
h : List.length l₁ ≤ List.length l₂
⊢ List.length l₂ = List.length (l₁ ++ List.replicate (List.length l₂ - List.length l₁) default)
simp only [add_tsub_cancel_of_le h, List.length_append, List.length_replicate]
no goals
case refine'_2.inl
Γ : Type u_1
i✝ : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i : ℕ), List.getI l₁ i = List.getI l₂ i
h✝ : List.length l₁ ≤ List.length l₂
i : ℕ
h : i < List.length l₂
h₂ : i < List.length (l₁ ++ List.replicate (List.length l₂ - List.length l₁) default)
h' : i < List.length l₁
⊢ List.get (l₁ ++ List.replicate (List.length l₂ - List.length l₁) default) { val := i, isLt := h₂ } =
    List.get l₂ { val := i, isLt := h }
simp only [List.get_append _ h', List.get?_eq_get h, List.get?_eq_get h',
  ← List.getI_eq_get _ h, ← List.getI_eq_get _ h', H]
no goals
case refine'_2.inr
Γ : Type u_1
i✝ : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i : ℕ), List.getI l₁ i = List.getI l₂ i
h✝ : List.length l₁ ≤ List.length l₂
i : ℕ
h : i < List.length l₂
h₂ : i < List.length (l₁ ++ List.replicate (List.length l₂ - List.length l₁) default)
h' : List.length l₁ ≤ i
⊢ List.get (l₁ ++ List.replicate (List.length l₂ - List.length l₁) default) { val := i, isLt := h₂ } =
    List.get l₂ { val := i, isLt := h }
simp only [List.get_append_right' h', List.get_replicate, List.get?_eq_get h,
  List.get?_len_le h', ← List.getI_eq_default _ h', H, List.getI_eq_get _ h]