-- Mathlib/Computability/Tape.lean
theorem ListBlank.ext {Γ} [i : Inhabited Γ] {L₁ L₂ : ListBlank Γ} :
    (∀ i, L₁.nth i = L₂.nth i) → L₁ = L₂

Proof state:
case refine_1
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1
h : l₁.length ≤ l₂.length
⊢ l₂.length = (l₁ ++ List.replicate (l₂.length - l₁.length) default).length

Tactic:
simp only [Nat.add_sub_cancel' h, List.length_append, List.length_replicate]

Result:
no goals

Proof state:
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
⊢ (∀ (i_1 : ℕ), L₁.nth i_1 = L₂.nth i_1) → L₁ = L₂

Tactic:
refine ListBlank.induction_on L₁ fun l₁ ↦ ListBlank.induction_on L₂ fun l₂ H ↦ ?_

Result:
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1
⊢ mk l₁ = mk l₂

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

Tactic:
rw [H]

Result:
no goals

Proof state:
case refine_2.inl
Γ : Type u_1
i✝ : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i : ℕ), l₁.getI i = l₂.getI i
h✝ : l₁.length ≤ l₂.length
i : ℕ
h : i < l₂.length
h₂ : i < (l₁ ++ List.replicate (l₂.length - l₁.length) default).length
h' : i < l₁.length
⊢ (l₁ ++ List.replicate (l₂.length - l₁.length) default)[i] = l₂[i]

Tactic:
simp [h', List.getElem_append _ h₂, ← List.getI_eq_getElem _ h, ← List.getI_eq_getElem _ h', H]

Result:
no goals

Proof state:
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1
⊢ mk l₁ = mk l₂

Tactic:
wlog h : l₁.length ≤ l₂.length

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

Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1
h : l₁.length ≤ l₂.length
⊢ mk l₁ = mk l₂

Proof state:
case refine_2.inr
Γ : Type u_1
i✝ : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i : ℕ), l₁.getI i = l₂.getI i
h✝ : l₁.length ≤ l₂.length
i : ℕ
h : i < l₂.length
h₂ : i < (l₁ ++ List.replicate (l₂.length - l₁.length) default).length
h' : l₁.length ≤ i
⊢ (l₁ ++ List.replicate (l₂.length - l₁.length) default)[i] = l₂[i]

Tactic:
rw [List.getElem_append_right h', List.getElem_replicate,
  ← List.getI_eq_default _ h', H, List.getI_eq_getElem _ h]

Result:
no goals

Proof state:
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1
h : l₁.length ≤ l₂.length
⊢ mk l₁ = mk l₂

Tactic:
refine Quotient.sound' (Or.inl ⟨l₂.length - l₁.length, ?_⟩)

Result:
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1
h : l₁.length ≤ l₂.length
⊢ l₂ = l₁ ++ List.replicate (l₂.length - l₁.length) default

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

Tactic:
cases le_total l₁.length l₂.length <;> [skip; symm] <;> apply this <;> try assumption

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

Proof state:
case refine_2
Γ : Type u_1
i✝ : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i : ℕ), (mk l₁).nth i = (mk l₂).nth i
h✝ : l₁.length ≤ l₂.length
i : ℕ
h : i < l₂.length
h₂ : i < (l₁ ++ List.replicate (l₂.length - l₁.length) default).length
⊢ (l₁ ++ List.replicate (l₂.length - l₁.length) default)[i] = l₂[i]

Tactic:
simp only [ListBlank.nth_mk] at H

Result:
case refine_2
Γ : Type u_1
i✝ : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i : ℕ), l₁.getI i = l₂.getI i
h✝ : l₁.length ≤ l₂.length
i : ℕ
h : i < l₂.length
h₂ : i < (l₁ ++ List.replicate (l₂.length - l₁.length) default).length
⊢ (l₁ ++ List.replicate (l₂.length - l₁.length) default)[i] = l₂[i]

Proof state:
case refine_2
Γ : Type u_1
i✝ : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i : ℕ), l₁.getI i = l₂.getI i
h✝ : l₁.length ≤ l₂.length
i : ℕ
h : i < l₂.length
h₂ : i < (l₁ ++ List.replicate (l₂.length - l₁.length) default).length
⊢ (l₁ ++ List.replicate (l₂.length - l₁.length) default)[i] = l₂[i]

Tactic:
rcases lt_or_le i l₁.length with h' | h'

Result:
case refine_2.inl
Γ : Type u_1
i✝ : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i : ℕ), l₁.getI i = l₂.getI i
h✝ : l₁.length ≤ l₂.length
i : ℕ
h : i < l₂.length
h₂ : i < (l₁ ++ List.replicate (l₂.length - l₁.length) default).length
h' : i < l₁.length
⊢ (l₁ ++ List.replicate (l₂.length - l₁.length) default)[i] = l₂[i]

case refine_2.inr
Γ : Type u_1
i✝ : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i : ℕ), l₁.getI i = l₂.getI i
h✝ : l₁.length ≤ l₂.length
i : ℕ
h : i < l₂.length
h₂ : i < (l₁ ++ List.replicate (l₂.length - l₁.length) default).length
h' : l₁.length ≤ i
⊢ (l₁ ++ List.replicate (l₂.length - l₁.length) default)[i] = l₂[i]

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

Tactic:
assumption

Result:
no goals

Proof state:
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1
h : l₁.length ≤ l₂.length
⊢ l₂ = l₁ ++ List.replicate (l₂.length - l₁.length) default

Tactic:
refine List.ext_getElem ?_ fun i h h₂ ↦ Eq.symm ?_

Result:
case refine_1
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1
h : l₁.length ≤ l₂.length
⊢ l₂.length = (l₁ ++ List.replicate (l₂.length - l₁.length) default).length

case refine_2
Γ : Type u_1
i✝ : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i : ℕ), (mk l₁).nth i = (mk l₂).nth i
h✝ : l₁.length ≤ l₂.length
i : ℕ
h : i < l₂.length
h₂ : i < (l₁ ++ List.replicate (l₂.length - l₁.length) default).length
⊢ (l₁ ++ List.replicate (l₂.length - l₁.length) default)[i] = l₂[i]