awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : List Γ
⊢ BlankExtends l (head (Quotient.mk'' l) :: l.tail)
have h : BlankExtends.{u_1} (Γ := Γ) [] (head (Quotient.mk'' []) :: List.tail [])
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : List Γ
h : BlankExtends.{u_1} (Γ := Γ) [] (head (Quotient.mk'' []) :: List.tail [])
⊢ BlankExtends l (head (Quotient.mk'' l) :: l.tail)
have h₁ : ∀ (head : Γ) (tail : List Γ), BlankExtends (head :: tail) (head :: tail)
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
n : ℕ
⊢ Γ
have apply : ∀ (a b : List Γ), BlankExtends a b → a.getI n = b.getI n
Tactic: apply l.liftOn (fun l ↦ List.getI l n)
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l_1 : ListBlank Γ
n : ℕ
l : List Γ
i : ℕ
⊢ l.getI n = (l ++ List.replicate i default).getI n
have inl : ∀ (h : n < l.length), l.getI n = (l ++ List.replicate i default).getI n
Tactic: rcases lt_or_ge n _ with h | h
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l_1 : ListBlank Γ
n : ℕ
l : List Γ
i : ℕ
inl : ∀ (h : n < l.length), l.getI n = (l ++ List.replicate i default).getI n
⊢ l.getI n = (l ++ List.replicate i default).getI n
have inr : ∀ (h : l.length ≤ n), l.getI n = (l ++ List.replicate i default).getI n
Tactic: rcases lt_or_ge n _ with h | h
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l_1 : ListBlank Γ
n : ℕ
l : List Γ
i : ℕ
h : n < l.length
⊢ l.getI n = (l ++ List.replicate i default).getI n
have inl : l.getI n = l.getI n
Tactic: rw [List.getI_append _ _ _ h]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l_1 : ListBlank Γ
n : ℕ
l : List Γ
i : ℕ
h : l.length ≤ n
⊢ l.getI n = (l ++ List.replicate i default).getI n
have inr : default = (l ++ List.replicate i default).getI n
Tactic: rw [List.getI_eq_default _ h]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l_1 : ListBlank Γ
n : ℕ
l : List Γ
i : ℕ
h : l.length ≤ n
⊢ default = (l ++ List.replicate i default).getI n
have inr : ∀ (h₂ : (l ++ List.replicate i default).length ≤ n), default = (l ++ List.replicate i default).getI n
Tactic: rcases le_or_gt _ n with h₂ | h₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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
⊢ default = (l ++ List.replicate i default).getI n
have inr₁ : ∀ (h₂ : n < (l ++ List.replicate i default).length), default = (l ++ List.replicate i default).getI n
Tactic: rcases le_or_gt _ n with h₂ | h₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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
⊢ default = (l ++ List.replicate i default).getI n
have inr : Eq.{u_1 + 1} (α := Γ) default default
Tactic: rw [List.getI_eq_default _ h₂]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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
⊢ default = (l ++ List.replicate i default).getI n
have inr : default = getElem (valid := fun (as : List Γ) (i : ℕ) ↦ i < as.length) (l ++ List.replicate i default) n h₂
Tactic: rw [List.getI_eq_getElem _ h₂, List.getElem_append_right h, List.getElem_replicate]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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₂
⊢ default = (l ++ List.replicate i default).getI n
have inr₁ : default = getElem (valid := fun (as : List Γ) (i : ℕ) ↦ i < as.length) (List.replicate i default) (n - l.length) sorry
Tactic: rw [List.getI_eq_getElem _ h₂, List.getElem_append_right h, List.getElem_replicate]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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) ⋯
⊢ default = (l ++ List.replicate i default).getI n
have inr₂ : Eq.{u_1 + 1} (α := Γ) default default
Tactic: rw [List.getI_eq_getElem _ h₂, List.getElem_append_right h, List.getElem_replicate]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
⊢ l.nth 0 = l.head
have rw : (cons l.head l.tail).nth 0 = (cons l.head l.tail).head
Tactic: rw [← ListBlank.cons_head_tail l]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
⊢ (cons l.head l.tail).nth 0 = (cons l.head l.tail).head
have h : ∀ (a : List Γ), nth (cons l.head (Quotient.mk'' a)) 0 = head (cons l.head (Quotient.mk'' a))
Tactic: induction l.tail using Quotient.inductionOn'
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
n : ℕ
⊢ l.nth (n + 1) = l.tail.nth n
have rw : (cons l.head l.tail).nth (n + 1) = (cons l.head l.tail).tail.nth n
Tactic: rw [← ListBlank.cons_head_tail l]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
n : ℕ
⊢ (cons l.head l.tail).nth (n + 1) = (cons l.head l.tail).tail.nth n
have h : ∀ (a : List Γ), nth (cons l.head (Quotient.mk'' a)) (n + 1) = nth (tail (cons l.head (Quotient.mk'' a))) n
Tactic: induction l.tail using Quotient.inductionOn'
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
⊢ (∀ (i_1 : ℕ), L₁.nth i_1 = L₂.nth i_1) → L₁ = L₂
have refine : ∀ (l₁ l₂ : List Γ) (H : ∀ (i_1 : ℕ), nth (mk l₁) i_1 = nth (mk l₂) i_1), Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
Tactic: refine ListBlank.induction_on L₁ fun l₁ ↦ ListBlank.induction_on L₂ fun l₂ H ↦ ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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
⊢ Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
have 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₂)
Tactic: wlog h : l₁.length ≤ l₂.length
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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₂)
⊢ Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
have 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₂)
Tactic: wlog h : l₁.length ≤ l₂.length
Cleared hypotheses: Γ, i, L₁, L₂, l₁, l₂, H
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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
⊢ Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
have inr : l₁.length ≤ l₂.length → Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
Tactic: cases le_total l₁.length l₂.length
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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₂)
⊢ Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
have inr₁ : l₂.length ≤ l₁.length → Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
Tactic: cases le_total l₁.length l₂.length
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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
⊢ Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
have inr : Eq (α := ListBlank Γ) (mk l₂) (mk l₁)
Tactic: symm
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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
⊢ Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
have inr : l₁.length ≤ l₂.length → Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
Tactic: cases le_total l₁.length l₂.length <;> [skip; symm]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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₂)
⊢ Eq (α := ListBlank Γ) (mk l₁) (mk l₂)
have inr₁ : l₂.length ≤ l₁.length → Eq (α := ListBlank Γ) (mk l₂) (mk l₁)
Tactic: cases le_total l₁.length l₂.length <;> [skip; symm]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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 Γ
⊢ Eq (α := ListBlank Γ) (mk l₂) (mk l₁)
have inr₂ : ∀ (i_1 : ℕ), nth (mk l₂) i_1 = nth (mk l₁) i_1
Tactic: apply this
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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 : ℕ
⊢ nth (mk l₂) i_1 = nth (mk l₁) i_1
have inr : nth (mk l₂) i_1 = nth (mk l₂) i_1
Tactic: rw [H]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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₂)
have refine : l₂ = l₁ ++ List.replicate (l₂.length - l₁.length) default
Tactic: refine Quotient.sound' (Or.inl ⟨l₂.length - l₁.length, ?_⟩)
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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
have refine_1 : l₂.length = (l₁ ++ List.replicate (l₂.length - l₁.length) default).length
Tactic: refine List.ext_getElem ?_ fun i h h₂ ↦ Eq.symm ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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
⊢ l₂ = l₁ ++ List.replicate (l₂.length - l₁.length) default
have 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
Tactic: refine List.ext_getElem ?_ fun i h h₂ ↦ Eq.symm ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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
⊢ 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
have 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
Tactic: rcases lt_or_ge i l₁.length with h' | h'
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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
⊢ 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
have 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
Tactic: rcases lt_or_ge i l₁.length with h' | h'
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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
⊢ 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
have refine_2 : getElem (valid := fun (as : List Γ) (i : ℕ) ↦ i < as.length) (List.replicate (l₂.length - l₁.length) default)
    (i - l₁.length) sorry =
  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]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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
⊢ 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
have refine_2₁ : default = 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]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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
⊢ 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
have refine_2₂ : l₁.getI i = 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]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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
⊢ 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
have refine_2₃ : l₂.getI i = 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]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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
⊢ 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
have 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
Tactic: rw [List.getElem_append_right h', List.getElem_replicate,
      ← List.getI_eq_default _ h', H, List.getI_eq_getElem _ h]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
f : Γ → Γ
i : ℕ
L : ListBlank Γ
⊢ (modifyNth f 0 L).nth i = if i = 0 then f (L.nth i) else L.nth i
have zero : (modifyNth f 0 L).nth 0 = if Eq (α := ℕ) 0 0 then f (L.nth 0) else L.nth 0
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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
⊢ (modifyNth f 0 L).nth i = if i = 0 then f (L.nth i) else L.nth i
have zero₁ : ∀ (n : ℕ), (modifyNth f 0 L).nth (n + 1) = if n + 1 = 0 then f (L.nth (n + 1)) else L.nth (n + 1)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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 Γ
⊢ (modifyNth f (n + 1) L).nth i = if i = n + 1 then f (L.nth i) else L.nth i
have succ : (modifyNth f (n + 1) L).nth 0 = if 0 = n + 1 then f (L.nth 0) else L.nth 0
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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
⊢ (modifyNth f (n + 1) L).nth i = if i = n + 1 then f (L.nth i) else L.nth i
have 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)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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 = if 0 = n + 1 then f (L.nth 0) else L.nth 0
have succ : (modifyNth f (n + 1) L).nth 0 = L.nth 0
Tactic: rw [if_neg (Nat.succ_ne_zero _).symm]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
f : Γ → Γ
n i : ℕ
L : ListBlank Γ
⊢ (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i
have zero : ∀ (i : ℕ) (L : ListBlank Γ), (modifyNth f 0 L).nth i = if i = 0 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]
Cleared hypotheses: n, i, L