awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l_1 : ListBlank Γ
n : ℕ
l : List Γ
i : ℕ
h : l.length ≤ n
inr : default = (l ++ List.replicate i default).getI n
⊢ l.getI n = (l ++ List.replicate i default).getI n

Tactic:
rw [List.getI_eq_default _ h]

Premises used: List.getI_eq_default
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l_1 : ListBlank Γ
n : ℕ
l : List Γ
i : ℕ
h : l.length ≤ n
inr : ∀ (h₂ : (l ++ List.replicate i default).length ≤ n), default = (l ++ List.replicate i default).getI n
inr₁ : ∀ (h₂ : n < (l ++ List.replicate i default).length), default = (l ++ List.replicate i default).getI n
⊢ default = (l ++ List.replicate i default).getI n

Tactic:
rcases le_or_gt _ n with h₂ | h₂

Premises used: le_or_gt
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l_1 : ListBlank Γ
n : ℕ
l : List Γ
i : ℕ
h : l.length ≤ n
h₂ : (l ++ List.replicate i default).length ≤ n
inr inr₁ : Eq.{u_1 + 1} (α := Γ) default default
⊢ default = (l ++ List.replicate i default).getI n

Tactic:
rw [List.getI_eq_default _ h₂]

Premises used: List.getI_eq_default
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l_1 : ListBlank Γ
n : ℕ
l : List Γ
i : ℕ
h : l.length ≤ n
h₂ : n < (l ++ List.replicate i default).length
inr : default = getElem (valid := fun (as : List Γ) (i : ℕ) ↦ i < as.length) (l ++ List.replicate i default) n h₂
inr₁ :
  default = getElem (valid := fun (as : List Γ) (i : ℕ) ↦ i < as.length) (List.replicate i default) (n - l.length) ⋯
inr₂ inr₃ : Eq.{u_1 + 1} (α := Γ) default default
⊢ default = (l ++ List.replicate i default).getI n

Tactic:
rw [List.getI_eq_getElem _ h₂, List.getElem_append_right h, List.getElem_replicate]

Premises used: List.getElem_replicate, List.getI_eq_getElem, List.getElem_append_right
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : List Γ
n : ℕ
⊢ nth (mk l) n = l.getI n

Tactic:
rfl

Premises used: Quotient.liftOn', List.getD, Turing.ListBlank.nth, List.getI, rfl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
rw : (cons l.head l.tail).nth 0 = (cons l.head l.tail).head
⊢ l.nth 0 = l.head

Tactic:
rw [← ListBlank.cons_head_tail l]

Premises used: Turing.ListBlank.cons_head_tail
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
h : ∀ (a : List Γ), nth (cons l.head (Quotient.mk'' a)) 0 = head (cons l.head (Quotient.mk'' a))
⊢ (cons l.head l.tail).nth 0 = (cons l.head l.tail).head

Tactic:
induction l.tail using Quotient.inductionOn'

Premises used: Turing.ListBlank.tail
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
a : List Γ
⊢ nth (cons l.head (Quotient.mk'' a)) 0 = head (cons l.head (Quotient.mk'' a))

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
n : ℕ
rw : (cons l.head l.tail).nth (n + 1) = (cons l.head l.tail).tail.nth n
⊢ l.nth (n + 1) = l.tail.nth n

Tactic:
rw [← ListBlank.cons_head_tail l]

Premises used: Turing.ListBlank.cons_head_tail
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
n : ℕ
h : ∀ (a : List Γ), nth (cons l.head (Quotient.mk'' a)) (n + 1) = nth (tail (cons l.head (Quotient.mk'' a))) n
⊢ (cons l.head l.tail).nth (n + 1) = (cons l.head l.tail).tail.nth n

Tactic:
induction l.tail using Quotient.inductionOn'

Premises used: Turing.ListBlank.tail
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
n : ℕ
a : List Γ
⊢ nth (cons l.head (Quotient.mk'' a)) (n + 1) = nth (tail (cons l.head (Quotient.mk'' a))) n

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
⊢ (∀ (i_1 : ℕ), L₁.nth i_1 = L₂.nth i_1) → L₁ = L₂

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

Premises used: Turing.ListBlank.induction_on
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
refine : ∀ (l₁ l₂ : List Γ) (H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1), Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
⊢ (∀ (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 ↦ ?_
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1
inr :
  ∀
    (this :
      ∀ {Γ : 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 : l₁.length ≤ l₂.length),
        Eq (α := ListBlank Γ) (mk l₁) (mk l₂))
    (h : ¬l₁.length ≤ l₂.length), Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
wlog :
  ∀ {Γ : 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 : l₁.length ≤ l₂.length),
    Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
⊢ Eq (α := ListBlank Γ) (mk l₁) (mk l₂)

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

Premises used: List.length
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : 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 Γ)
    (H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1) (h : l₁.length ≤ l₂.length),
    Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
h : ¬l₁.length ≤ l₂.length
inr : l₁.length ≤ l₂.length → Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
inr₁ : l₂.length ≤ l₁.length → Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
⊢ Eq (α := ListBlank Γ) (mk l₁) (mk l₂)

Tactic:
cases le_total l₁.length l₂.length

Premises used: le_total, List.length
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : 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 Γ)
    (H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1) (h : l₁.length ≤ l₂.length),
    Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
h : ¬l₁.length ≤ l₂.length
h_1 : l₂.length ≤ l₁.length
inr : Eq (α := ListBlank Γ) (mk l₂) (mk l₁)
⊢ Eq (α := ListBlank Γ) (mk l₁) (mk l₂)

Tactic:
symm
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : 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 Γ)
    (H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1) (h : l₁.length ≤ l₂.length),
    Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
h : ¬l₁.length ≤ l₂.length
inr : l₁.length ≤ l₂.length → Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
inr₁ : l₂.length ≤ l₁.length → Eq (α := ListBlank Γ) (mk l₂) (mk l₁)
⊢ Eq (α := ListBlank Γ) (mk l₁) (mk l₂)

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

Premises used: le_total, List.length
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : 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 Γ)
    (H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1) (h : l₁.length ≤ l₂.length),
    Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
h : ¬l₁.length ≤ l₂.length
h_1 : l₁.length ≤ l₂.length
inr inr₁ : ListBlank Γ
inr₂ : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1
inr₃ : l₁.length ≤ l₂.length
⊢ Eq (α := ListBlank Γ) (mk l₁) (mk l₂)

Tactic:
apply this
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : 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 Γ)
    (H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1) (h : l₁.length ≤ l₂.length),
    Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
h : ¬l₁.length ≤ l₂.length
h_1 : l₂.length ≤ l₁.length
inr inr₁ : ListBlank Γ
inr₂ : ∀ (i_1 : ℕ), nth (mk l₂) i_1 = nth (mk l₁) i_1
inr₃ : l₂.length ≤ l₁.length
⊢ Eq (α := ListBlank Γ) (mk l₂) (mk l₁)

Tactic:
apply this
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : 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 Γ)
    (H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1) (h : l₁.length ≤ l₂.length),
    Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
h : ¬l₁.length ≤ l₂.length
h_1 : l₁.length ≤ l₂.length
⊢ ListBlank Γ

Tactic:
assumption
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : 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 Γ)
    (H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1) (h : l₁.length ≤ l₂.length),
    Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
h : ¬l₁.length ≤ l₂.length
h_1 : l₁.length ≤ l₂.length
⊢ ListBlank Γ

Tactic:
try assumption
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : 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 Γ)
    (H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1) (h : l₁.length ≤ l₂.length),
    Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
h : ¬l₁.length ≤ l₂.length
h_1 : l₁.length ≤ l₂.length
⊢ ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1

Tactic:
assumption
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : 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 Γ)
    (H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1) (h : l₁.length ≤ l₂.length),
    Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
h : ¬l₁.length ≤ l₂.length
h_1 : l₁.length ≤ l₂.length
⊢ ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1

Tactic:
try assumption
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : 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 Γ)
    (H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1) (h : l₁.length ≤ l₂.length),
    Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
h : ¬l₁.length ≤ l₂.length
h_1 : l₁.length ≤ l₂.length
⊢ l₁.length ≤ l₂.length

Tactic:
assumption
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : 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 Γ)
    (H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1) (h : l₁.length ≤ l₂.length),
    Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
h : ¬l₁.length ≤ l₂.length
h_1 : l₁.length ≤ l₂.length
⊢ l₁.length ≤ l₂.length

Tactic:
try assumption
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : 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 Γ)
    (H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1) (h : l₁.length ≤ l₂.length),
    Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
h : ¬l₁.length ≤ l₂.length
h_1 : l₂.length ≤ l₁.length
⊢ ListBlank Γ

Tactic:
assumption
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : 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 Γ)
    (H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1) (h : l₁.length ≤ l₂.length),
    Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
h : ¬l₁.length ≤ l₂.length
h_1 : l₂.length ≤ l₁.length
⊢ ListBlank Γ

Tactic:
try assumption
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : 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 Γ)
    (H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1) (h : l₁.length ≤ l₂.length),
    Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
h : ¬l₁.length ≤ l₂.length
h_1 : l₂.length ≤ l₁.length
⊢ l₂.length ≤ l₁.length

Tactic:
assumption
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : 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 Γ)
    (H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1) (h : l₁.length ≤ l₂.length),
    Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
h : ¬l₁.length ≤ l₂.length
h_1 : l₂.length ≤ l₁.length
⊢ l₂.length ≤ l₁.length

Tactic:
try assumption
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_2 : ℕ), nth (mk l₁) i_2 = nth (mk l₂) i_2
this :
  ∀ {Γ : Type u_1} [i : Inhabited Γ] {L₁ L₂ : ListBlank Γ} (l₁ l₂ : List Γ)
    (H : ∀ (i_2 : ℕ), nth (mk l₁) i_2 = nth (mk l₂) i_2) (h : l₁.length ≤ l₂.length),
    Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
h : ¬l₁.length ≤ l₂.length
h_1 : l₂.length ≤ l₁.length
i_1 : ℕ
inr inr₁ : nth (mk l₂) i_1 = nth (mk l₂) i_1
⊢ nth (mk l₂) i_1 = nth (mk l₁) i_1

Tactic:
rw [H]
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : 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 : l₁.length ≤ l₂.length
⊢ Eq (α := ListBlank Γ) (mk l₁) (mk l₂)

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

Premises used: Quotient.sound', Turing.ListBlank.mk, HSub.hSub, Exists.intro, Turing.ListBlank, Or.inl, List.length
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : 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 : l₁.length ≤ l₂.length
refine : l₂ = l₁ ++ List.replicate (l₂.length - l₁.length) default
⊢ Eq (α := ListBlank Γ) (mk l₁) (mk l₂)

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

Premises used: Quotient.sound'
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : 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 : l₁.length ≤ l₂.length
⊢ l₂ = l₁ ++ List.replicate (l₂.length - l₁.length) default

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

Premises used: List.ext_getElem, Eq.symm
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : 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 : l₁.length ≤ l₂.length
refine_1 : l₂.length = (l₁ ++ List.replicate (l₂.length - l₁.length) default).length
refine_2 :
  ∀ (i_1 : ℕ) (h : i_1 < l₂.length) (h₂ : i_1 < (l₁ ++ List.replicate (l₂.length - l₁.length) default).length),
    getElem (valid := fun (as : List Γ) (i : ℕ) ↦ i < as.length) (l₁ ++ List.replicate (l₂.length - l₁.length) default)
        i_1 h₂ =
      getElem (valid := fun (as : List Γ) (i : ℕ) ↦ i < as.length) l₂ i_1 h
⊢ l₂ = l₁ ++ List.replicate (l₂.length - l₁.length) default

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

Premises used: List.ext_getElem, Eq.symm
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : 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 : 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]

Premises used: List.length_append, List.length_replicate, Nat.add_sub_cancel'
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
i_1 : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i : ℕ), l₁.getI i = l₂.getI i
h_1 : l₁.length ≤ l₂.length
i : ℕ
h : i < l₂.length
h₂ : i < (l₁ ++ List.replicate (l₂.length - l₁.length) default).length
refine_2 :
  ∀ (h' : i < l₁.length),
    getElem (valid := fun (as : List Γ) (i : ℕ) ↦ i < as.length) (l₁ ++ List.replicate (l₂.length - l₁.length) default)
        i h₂ =
      getElem (valid := fun (as : List Γ) (i : ℕ) ↦ i < as.length) l₂ i h
refine_2₁ :
  ∀ (h' : l₁.length ≤ i),
    getElem (valid := fun (as : List Γ) (i : ℕ) ↦ i < as.length) (l₁ ++ List.replicate (l₂.length - l₁.length) default)
        i h₂ =
      getElem (valid := fun (as : List Γ) (i : ℕ) ↦ i < as.length) l₂ i h
⊢ getElem (valid := fun (as : List Γ) (i : ℕ) ↦ i < as.length) (l₁ ++ List.replicate (l₂.length - l₁.length) default) i
      h₂ =
    getElem (valid := fun (as : List Γ) (i : ℕ) ↦ i < as.length) l₂ i h

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

Premises used: lt_or_ge, List.length
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
i_1 : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i : ℕ), l₁.getI i = l₂.getI i
h_1 : l₁.length ≤ l₂.length
i : ℕ
h : i < l₂.length
h₂ : i < (l₁ ++ List.replicate (l₂.length - l₁.length) default).length
h' : i < l₁.length
⊢ getElem (valid := fun (as : List Γ) (i : ℕ) ↦ i < as.length) (l₁ ++ List.replicate (l₂.length - l₁.length) default) i
      h₂ =
    getElem (valid := fun (as : List Γ) (i : ℕ) ↦ i < as.length) l₂ i h

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

Premises used: List.getElem_append, List.getI_eq_getElem
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
i_1 : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i : ℕ), l₁.getI i = l₂.getI i
h_1 : l₁.length ≤ l₂.length
i : ℕ
h : i < l₂.length
h₂ : i < (l₁ ++ List.replicate (l₂.length - l₁.length) default).length
h' : l₁.length ≤ i
refine_2 :
  getElem (valid := fun (as : List Γ) (i : ℕ) ↦ i < as.length) (List.replicate (l₂.length - l₁.length) default)
      (i - l₁.length) ⋯ =
    getElem (valid := fun (as : List Γ) (i : ℕ) ↦ i < as.length) l₂ i h
refine_2₁ : default = getElem (valid := fun (as : List Γ) (i : ℕ) ↦ i < as.length) l₂ i h
refine_2₂ : l₁.getI i = getElem (valid := fun (as : List Γ) (i : ℕ) ↦ i < as.length) l₂ i h
refine_2₃ : l₂.getI i = getElem (valid := fun (as : List Γ) (i : ℕ) ↦ i < as.length) l₂ i h
refine_2₄ refine_2₅ :
  getElem (valid := fun (as : List Γ) (i : ℕ) ↦ i < as.length) l₂ i h =
    getElem (valid := fun (as : List Γ) (i : ℕ) ↦ i < as.length) l₂ i h
⊢ getElem (valid := fun (as : List Γ) (i : ℕ) ↦ i < as.length) (l₁ ++ List.replicate (l₂.length - l₁.length) default) i
      h₂ =
    getElem (valid := fun (as : List Γ) (i : ℕ) ↦ i < as.length) l₂ i h

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

Premises used: List.getElem_replicate, List.getI_eq_default, List.getI_eq_getElem, List.getElem_append_right
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
f : Γ → Γ
i : ℕ
L : ListBlank Γ
zero : (modifyNth f 0 L).nth 0 = if Eq (α := ℕ) 0 0 then f (L.nth 0) else L.nth 0
zero₁ : ∀ (n : ℕ), (modifyNth f 0 L).nth (n + 1) = if n + 1 = 0 then f (L.nth (n + 1)) else L.nth (n + 1)
⊢ (modifyNth f 0 L).nth i = if i = 0 then f (L.nth i) else L.nth i

Tactic:
cases i
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
f : Γ → Γ
L : ListBlank Γ
⊢ (modifyNth f 0 L).nth 0 = if Eq (α := ℕ) 0 0 then f (L.nth 0) else L.nth 0

Tactic:
simp only [ListBlank.nth_zero, if_true, ListBlank.head_cons, ListBlank.modifyNth,
      ListBlank.nth_succ, if_false, ListBlank.tail_cons, reduceCtorEq]

Premises used: reduceCtorEq, Turing.ListBlank.modifyNth, Turing.ListBlank.nth_zero, if_true, if_false, Turing.ListBlank.nth_succ, Turing.ListBlank.head_cons, Turing.ListBlank.tail_cons
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
f : Γ → Γ
L : ListBlank Γ
n : ℕ
⊢ (modifyNth f 0 L).nth (n + 1) = if n + 1 = 0 then f (L.nth (n + 1)) else L.nth (n + 1)

Tactic:
simp only [ListBlank.nth_zero, if_true, ListBlank.head_cons, ListBlank.modifyNth,
      ListBlank.nth_succ, if_false, ListBlank.tail_cons, reduceCtorEq]

Premises used: reduceCtorEq, Turing.ListBlank.modifyNth, Turing.ListBlank.nth_zero, if_true, if_false, Turing.ListBlank.nth_succ, Turing.ListBlank.head_cons, Turing.ListBlank.tail_cons
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
f : Γ → Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i
i : ℕ
L : ListBlank Γ
succ : (modifyNth f (n + 1) L).nth 0 = if 0 = n + 1 then f (L.nth 0) else L.nth 0
succ₁ :
  ∀ (n_1 : ℕ), (modifyNth f (n + 1) L).nth (n_1 + 1) = if n_1 + 1 = n + 1 then f (L.nth (n_1 + 1)) else L.nth (n_1 + 1)
⊢ (modifyNth f (n + 1) L).nth i = if i = n + 1 then f (L.nth i) else L.nth i

Tactic:
cases i
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
f : Γ → Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i
L : ListBlank Γ
succ : (modifyNth f (n + 1) L).nth 0 = L.nth 0
⊢ (modifyNth f (n + 1) L).nth 0 = if 0 = n + 1 then f (L.nth 0) else L.nth 0

Tactic:
rw [if_neg (Nat.succ_ne_zero _).symm]

Premises used: Ne.symm, Nat.succ_ne_zero, if_neg
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
f : Γ → Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i
L : ListBlank Γ
⊢ (modifyNth f (n + 1) L).nth 0 = L.nth 0

Tactic:
simp only [ListBlank.nth_zero, ListBlank.head_cons, ListBlank.modifyNth]

Premises used: Turing.ListBlank.modifyNth, Turing.ListBlank.nth_zero, Turing.ListBlank.head_cons
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
f : Γ → Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i
L : ListBlank Γ
n_1 : ℕ
⊢ (modifyNth f (n + 1) L).nth (n_1 + 1) = if n_1 + 1 = n + 1 then f (L.nth (n_1 + 1)) else L.nth (n_1 + 1)

Tactic:
simp only [IH, ListBlank.modifyNth, ListBlank.nth_succ, ListBlank.tail_cons, Nat.succ.injEq]

Premises used: Nat.succ.injEq, Turing.ListBlank.modifyNth, Turing.ListBlank.nth_succ, Turing.ListBlank.tail_cons
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
f : Γ → Γ
n i : ℕ
L : ListBlank Γ
zero : ∀ (i : ℕ) (L : ListBlank Γ), (modifyNth f 0 L).nth i = if i = 0 then f (L.nth i) else L.nth i
succ :
  ∀ (n : ℕ) (IH : ∀ (i : ℕ) (L : ListBlank Γ), (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i) (i : ℕ)
    (L : ListBlank Γ), (modifyNth f (n + 1) L).nth i = if i = n + 1 then f (L.nth i) else L.nth i
⊢ (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i

Tactic:
induction n generalizing i L with
  | zero =>
    cases i <;> simp only [ListBlank.nth_zero, if_true, ListBlank.head_cons, ListBlank.modifyNth,
      ListBlank.nth_succ, if_false, ListBlank.tail_cons, reduceCtorEq]
  | succ n IH =>
    cases i
    · rw [if_neg (Nat.succ_ne_zero _).symm]
      simp only [ListBlank.nth_zero, ListBlank.head_cons, ListBlank.modifyNth]
    · simp only [IH, ListBlank.modifyNth, ListBlank.nth_succ, ListBlank.tail_cons, Nat.succ.injEq]

Premises used: Nat.succ.injEq, reduceCtorEq, Turing.ListBlank.modifyNth, Turing.ListBlank.nth_zero, if_true, if_false, Turing.ListBlank.nth_succ, Ne.symm, Turing.ListBlank.head_cons, Turing.ListBlank.tail_cons, Nat.succ_ne_zero, if_neg
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : Γ → Γ'
pt : f default = default
⊢ { f := f, map_pt' := pt : PointedMap Γ Γ' }.f = f

Tactic:
rfl

Premises used: rfl