awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
p : σ → Bool
q₁ q₂ : TM2.Stmt Γ Λ σ
IH₁ :
  TM2.SupportsStmt (Γ := Γ) S q₁ →
    (∀ x ∈ trStmts₁ (Γ := Γ) q₁, x ∈ trSupp (Γ := Γ) M S) →
      TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₁) ∧
        ∀ l' ∈ trStmts₁ (Γ := Γ) q₁, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
IH₂ :
  TM2.SupportsStmt (Γ := Γ) S q₂ →
    (∀ x ∈ trStmts₁ (Γ := Γ) q₂, x ∈ trSupp (Γ := Γ) M S) →
      TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₂) ∧
        ∀ l' ∈ trStmts₁ (Γ := Γ) q₂, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
ss' : TM2.SupportsStmt (Γ := Γ) S (TM2.Stmt.branch (Γ := Γ) p q₁ q₂)
sub : ∀ x ∈ trStmts₁ (Γ := Γ) q₁ ∪ trStmts₁ (Γ := Γ) q₂, x ∈ trSupp (Γ := Γ) M S
IH₁₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₁)
IH₁₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₁, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
IH₂₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₂)
IH₂₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₂, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.branch (Γ := Γ) p q₁ q₂)) ∧
    ∀ l' ∈ trStmts₁ (Γ := Γ) (TM2.Stmt.branch (Γ := Γ) p q₁ q₂),
      TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
have refine_3 : ∀ (l : Λ' K Γ Λ σ) (h : l ∈ trStmts₁ (Γ := Γ) (TM2.Stmt.branch (Γ := Γ) p q₁ q₂)),
  TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)
Tactic: refine ⟨⟨IH₁₁, IH₂₁⟩, fun l h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (hypothesis)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
p : σ → Bool
q₁ q₂ : TM2.Stmt Γ Λ σ
IH₁ :
  TM2.SupportsStmt (Γ := Γ) S q₁ →
    (∀ x ∈ trStmts₁ (Γ := Γ) q₁, x ∈ trSupp (Γ := Γ) M S) →
      TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₁) ∧
        ∀ l' ∈ trStmts₁ (Γ := Γ) q₁, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
IH₂ :
  TM2.SupportsStmt (Γ := Γ) S q₂ →
    (∀ x ∈ trStmts₁ (Γ := Γ) q₂, x ∈ trSupp (Γ := Γ) M S) →
      TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₂) ∧
        ∀ l' ∈ trStmts₁ (Γ := Γ) q₂, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
ss' : TM2.SupportsStmt (Γ := Γ) S (TM2.Stmt.branch (Γ := Γ) p q₁ q₂)
sub : ∀ x ∈ trStmts₁ (Γ := Γ) q₁ ∪ trStmts₁ (Γ := Γ) q₂, x ∈ trSupp (Γ := Γ) M S
IH₁₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₁)
IH₁₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₁, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
IH₂₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₂)
IH₂₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₂, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
l : Λ' K Γ Λ σ
h : l ∈ trStmts₁ (Γ := Γ) (TM2.Stmt.branch (Γ := Γ) p q₁ q₂)
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)
have h₁ : l ∈ trStmts₁ (Γ := Γ) q₁ ∪ trStmts₁ (Γ := Γ) q₂
Tactic: rw [trStmts₁] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
p : σ → Bool
q₁ q₂ : TM2.Stmt Γ Λ σ
IH₁ :
  TM2.SupportsStmt (Γ := Γ) S q₁ →
    (∀ x ∈ trStmts₁ (Γ := Γ) q₁, x ∈ trSupp (Γ := Γ) M S) →
      TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₁) ∧
        ∀ l' ∈ trStmts₁ (Γ := Γ) q₁, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
IH₂ :
  TM2.SupportsStmt (Γ := Γ) S q₂ →
    (∀ x ∈ trStmts₁ (Γ := Γ) q₂, x ∈ trSupp (Γ := Γ) M S) →
      TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₂) ∧
        ∀ l' ∈ trStmts₁ (Γ := Γ) q₂, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
ss' : TM2.SupportsStmt (Γ := Γ) S (TM2.Stmt.branch (Γ := Γ) p q₁ q₂)
sub : ∀ x ∈ trStmts₁ (Γ := Γ) q₁ ∪ trStmts₁ (Γ := Γ) q₂, x ∈ trSupp (Γ := Γ) M S
IH₁₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₁)
IH₁₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₁, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
IH₂₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₂)
IH₂₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₂, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
l : Λ' K Γ Λ σ
h : l ∈ trStmts₁ (Γ := Γ) q₁ ∪ trStmts₁ (Γ := Γ) q₂
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)
have refine_3 : ∀ (h : l ∈ trStmts₁ (Γ := Γ) q₁), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)
Tactic: rcases Finset.mem_union.1 h with (h | h)
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
p : σ → Bool
q₁ q₂ : TM2.Stmt Γ Λ σ
IH₁ :
  TM2.SupportsStmt (Γ := Γ) S q₁ →
    (∀ x ∈ trStmts₁ (Γ := Γ) q₁, x ∈ trSupp (Γ := Γ) M S) →
      TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₁) ∧
        ∀ l' ∈ trStmts₁ (Γ := Γ) q₁, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
IH₂ :
  TM2.SupportsStmt (Γ := Γ) S q₂ →
    (∀ x ∈ trStmts₁ (Γ := Γ) q₂, x ∈ trSupp (Γ := Γ) M S) →
      TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₂) ∧
        ∀ l' ∈ trStmts₁ (Γ := Γ) q₂, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
ss' : TM2.SupportsStmt (Γ := Γ) S (TM2.Stmt.branch (Γ := Γ) p q₁ q₂)
sub : ∀ x ∈ trStmts₁ (Γ := Γ) q₁ ∪ trStmts₁ (Γ := Γ) q₂, x ∈ trSupp (Γ := Γ) M S
IH₁₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₁)
IH₁₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₁, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
IH₂₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₂)
IH₂₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₂, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
l : Λ' K Γ Λ σ
h : l ∈ trStmts₁ (Γ := Γ) q₁ ∪ trStmts₁ (Γ := Γ) q₂
refine_3 : ∀ (h : l ∈ trStmts₁ (Γ := Γ) q₁), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)
have refine_3₁ : ∀ (h : l ∈ trStmts₁ (Γ := Γ) q₂), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)
Tactic: rcases Finset.mem_union.1 h with (h | h)
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
p : σ → Bool
q₁ q₂ : TM2.Stmt Γ Λ σ
IH₁ :
  TM2.SupportsStmt (Γ := Γ) S q₁ →
    (∀ x ∈ trStmts₁ (Γ := Γ) q₁, x ∈ trSupp (Γ := Γ) M S) →
      TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₁) ∧
        ∀ l' ∈ trStmts₁ (Γ := Γ) q₁, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
IH₂ :
  TM2.SupportsStmt (Γ := Γ) S q₂ →
    (∀ x ∈ trStmts₁ (Γ := Γ) q₂, x ∈ trSupp (Γ := Γ) M S) →
      TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₂) ∧
        ∀ l' ∈ trStmts₁ (Γ := Γ) q₂, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
ss' : TM2.SupportsStmt (Γ := Γ) S (TM2.Stmt.branch (Γ := Γ) p q₁ q₂)
sub : ∀ x ∈ trStmts₁ (Γ := Γ) q₁ ∪ trStmts₁ (Γ := Γ) q₂, x ∈ trSupp (Γ := Γ) M S
IH₁₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₁)
IH₁₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₁, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
IH₂₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₂)
IH₂₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₂, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
l : Λ' K Γ Λ σ
h : l ∈ trStmts₁ (Γ := Γ) q₁ ∪ trStmts₁ (Γ := Γ) q₂
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)
have refine_3 : ∀ (h : l ∈ trStmts₁ (Γ := Γ) q₁), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)
Tactic: rcases Finset.mem_union.1 h with (h | h) <;> [exact IH₁₂ _ h; exact IH₂₂ _ h]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
p : σ → Bool
q₁ q₂ : TM2.Stmt Γ Λ σ
IH₁ :
  TM2.SupportsStmt (Γ := Γ) S q₁ →
    (∀ x ∈ trStmts₁ (Γ := Γ) q₁, x ∈ trSupp (Γ := Γ) M S) →
      TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₁) ∧
        ∀ l' ∈ trStmts₁ (Γ := Γ) q₁, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
IH₂ :
  TM2.SupportsStmt (Γ := Γ) S q₂ →
    (∀ x ∈ trStmts₁ (Γ := Γ) q₂, x ∈ trSupp (Γ := Γ) M S) →
      TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₂) ∧
        ∀ l' ∈ trStmts₁ (Γ := Γ) q₂, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
ss' : TM2.SupportsStmt (Γ := Γ) S (TM2.Stmt.branch (Γ := Γ) p q₁ q₂)
sub : ∀ x ∈ trStmts₁ (Γ := Γ) q₁ ∪ trStmts₁ (Γ := Γ) q₂, x ∈ trSupp (Γ := Γ) M S
IH₁₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₁)
IH₁₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₁, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
IH₂₁ : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₂)
IH₂₂ : ∀ l' ∈ trStmts₁ (Γ := Γ) q₂, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
l : Λ' K Γ Λ σ
h : l ∈ trStmts₁ (Γ := Γ) q₁ ∪ trStmts₁ (Γ := Γ) q₂
refine_3 : ∀ (h : l ∈ trStmts₁ (Γ := Γ) q₁), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)
have refine_3₁ : ∀ (h : l ∈ trStmts₁ (Γ := Γ) q₂), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l)
Tactic: rcases Finset.mem_union.1 h with (h | h) <;> [exact IH₁₂ _ h; exact IH₂₂ _ h]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
l : σ → Λ
ss' : TM2.SupportsStmt (Γ := Γ) S (TM2.Stmt.goto (Γ := Γ) l)
h :
  ∀ (x : Λ' K Γ Λ σ),
    Membership.mem (γ := Finset (Λ' K Γ Λ σ)) (trStmts₁ (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l)) x → x ∈ trSupp (Γ := Γ) M S
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l)) ∧
    ∀ (l' : Λ' K Γ Λ σ),
      Membership.mem (γ := Finset (Λ' K Γ Λ σ)) (trStmts₁ (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l)) l' →
        TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
have refine_4 : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l)) ∧
  ∀ (l' : Λ' K Γ Λ σ), False → TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
Tactic: simp only [trStmts₁, Finset.notMem_empty]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
l : σ → Λ
ss' : TM2.SupportsStmt (Γ := Γ) S (TM2.Stmt.goto (Γ := Γ) l)
h :
  ∀ (x : Λ' K Γ Λ σ),
    Membership.mem (γ := Finset (Λ' K Γ Λ σ)) (trStmts₁ (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l)) x → x ∈ trSupp (Γ := Γ) M S
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l)) ∧
    ∀ (l' : Λ' K Γ Λ σ), False → TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
have refine_4 : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l))
Tactic: refine ⟨?_, fun _ ↦ False.elim⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.StackTuringMachine (goal)
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
h : TM2.SupportsStmt.{u_1, u_2, u_3, u_4} (Γ := Γ) (σ := σ) S (TM2.Stmt.halt (Γ := Γ))
h_1 :
  ∀ (x : Λ' K Γ Λ σ),
    Membership.mem (γ := Finset (Λ' K Γ Λ σ)) (trStmts₁ (Γ := Γ) (TM2.Stmt.halt (Γ := Γ))) x → x ∈ trSupp (Γ := Γ) M S
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.halt (Γ := Γ))) ∧
    ∀ (l' : Λ' K Γ Λ σ),
      Membership.mem (γ := Finset (Λ' K Γ Λ σ)) (trStmts₁ (Γ := Γ) (TM2.Stmt.halt (Γ := Γ))) l' →
        TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
have refine_5 : TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.halt (Γ := Γ))) ∧
  ∀ (l' : Λ' K Γ Λ σ), False → TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
Tactic: simp only [trStmts₁, Finset.notMem_empty]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : List Γ
i j : ℕ
h : (l ++ List.replicate i default).length ≤ (l ++ List.replicate j default).length
⊢ BlankExtends (l ++ List.replicate i default) (l ++ List.replicate j default)
have h₁ : l ++ List.replicate j default = l ++ List.replicate i default ++ List.replicate (j - i) default
Tactic: use j - i
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (hypothesis)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : List Γ
i j : ℕ
h : (l ++ List.replicate i default).length ≤ (l ++ List.replicate j default).length
⊢ l ++ List.replicate j default = l ++ List.replicate i default ++ List.replicate (j - i) default
have h₁ : i ≤ j
Tactic: simp only [List.length_append, Nat.add_le_add_iff_left, List.length_replicate] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : l₁.length ≤ l₂.length
⊢ BlankExtends l₁ l₂
have h₁ : l₂ = l₁ ++ List.replicate (i - j) default
Tactic: use i - j
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : l₁.length ≤ l₂.length
⊢ l₂ = l₁ ++ List.replicate (i - j) default
have h₁ : l₁ ++ List.replicate i default = l₁ ++ List.replicate (i - j) default ++ List.replicate j default
Tactic: refine List.append_cancel_right (e.symm.trans ?_)
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : l₁.length ≤ l₂.length
⊢ l₁ ++ List.replicate i default = l₁ ++ List.replicate (i - j) default ++ List.replicate j default
have h₁ : j ≤ i
Tactic: rw [List.append_assoc, ← List.replicate_add, Nat.sub_add_cancel]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (hypothesis)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : l₁.length ≤ l₂.length
⊢ j ≤ i
have e₁ : (l₁ ++ List.replicate i default).length = (l₂ ++ List.replicate j default).length
Tactic: apply_fun List.length at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (hypothesis)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
h : l₁.length ≤ l₂.length
e : (l₁ ++ List.replicate i default).length = (l₂ ++ List.replicate j default).length
⊢ j ≤ i
have e₁ : l₁.length + i = l₂.length + j
Tactic: simp only [List.length_append, List.length_replicate] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
h : l₁.length ≤ l₂.length
e : l₁.length + i = l₂.length + j
⊢ j ≤ i
have h₁ : l₁.length + j ≤ l₁.length + i
Tactic: rwa [← Nat.add_le_add_iff_left, e, Nat.add_le_add_iff_right]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
h : l₁.length ≤ l₂.length
e : l₁.length + i = l₂.length + j
h₁ : l₁.length + j ≤ l₁.length + i
rwa : ℕ
⊢ j ≤ i
have h₂ : l₁.length + j ≤ l₂.length + j
Tactic: rwa [← Nat.add_le_add_iff_left, e, Nat.add_le_add_iff_right]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
h : BlankRel l₁ l₂
⊢ { l : List Γ // BlankExtends l₁ l ∧ BlankExtends l₂ l }
have refine_1 : ∀ (hl : l₁.length ≤ l₂.length) (h' : BlankExtends l₂ l₁), BlankExtends l₁ l₂
Tactic: refine
    if hl : l₁.length ≤ l₂.length then ⟨l₂, Or.elim h id fun h' ↦ ?_, BlankExtends.refl _⟩
    else ⟨l₁, BlankExtends.refl _, Or.elim h (fun h' ↦ ?_) id⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
h : BlankRel l₁ l₂
refine_1 : ∀ (hl : l₁.length ≤ l₂.length) (h' : BlankExtends l₂ l₁), BlankExtends l₁ l₂
⊢ { l : List Γ // BlankExtends l₁ l ∧ BlankExtends l₂ l }
have refine_2 : ∀ (hl : ¬l₁.length ≤ l₂.length) (h' : BlankExtends l₁ l₂), BlankExtends l₂ l₁
Tactic: refine
    if hl : l₁.length ≤ l₂.length then ⟨l₂, Or.elim h id fun h' ↦ ?_, BlankExtends.refl _⟩
    else ⟨l₁, BlankExtends.refl _, Or.elim h (fun h' ↦ ?_) id⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
h : BlankRel l₁ l₂
⊢ { l : List Γ // BlankExtends l l₁ ∧ BlankExtends l l₂ }
have refine_1 : ∀ (hl : l₁.length ≤ l₂.length) (h' : BlankExtends l₂ l₁), BlankExtends l₁ l₂
Tactic: refine
    if hl : l₁.length ≤ l₂.length then ⟨l₁, BlankExtends.refl _, Or.elim h id fun h' ↦ ?_⟩
    else ⟨l₂, Or.elim h (fun h' ↦ ?_) id, BlankExtends.refl _⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
h : BlankRel l₁ l₂
refine_1 : ∀ (hl : l₁.length ≤ l₂.length) (h' : BlankExtends l₂ l₁), BlankExtends l₁ l₂
⊢ { l : List Γ // BlankExtends l l₁ ∧ BlankExtends l l₂ }
have refine_2 : ∀ (hl : ¬l₁.length ≤ l₂.length) (h' : BlankExtends l₁ l₂), BlankExtends l₂ l₁
Tactic: refine
    if hl : l₁.length ≤ l₂.length then ⟨l₁, BlankExtends.refl _, Or.elim h id fun h' ↦ ?_⟩
    else ⟨l₂, Or.elim h (fun h' ↦ ?_) id, BlankExtends.refl _⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
⊢ Γ
have apply : ∀ (a b : List Γ), BlankExtends a b → a.headI = b.headI
Tactic: apply l.liftOn List.headI
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
a : List Γ
i : ℕ
⊢ a.headI = (a ++ List.replicate i default).headI
have nil : List.headI [] = (HAppend.hAppend (α := List Γ) [] (List.replicate i default)).headI
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
a : List Γ
i : ℕ
nil : List.headI [] = (HAppend.hAppend (α := List Γ) [] (List.replicate i default)).headI
⊢ a.headI = (a ++ List.replicate i default).headI
have cons : ∀ (head : Γ) (tail : List Γ), (head :: tail).headI = (head :: tail ++ List.replicate i default).headI
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
i : ℕ
⊢ List.headI [] = (HAppend.hAppend (α := List Γ) [] (List.replicate i default)).headI
have nil : List.headI [] = (HAppend.hAppend (α := List Γ) [] (List.replicate 0 default)).headI
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
i : ℕ
nil : List.headI [] = (HAppend.hAppend (α := List Γ) [] (List.replicate 0 default)).headI
⊢ List.headI [] = (HAppend.hAppend (α := List Γ) [] (List.replicate i default)).headI
have nil₁ : ∀ (n : ℕ), List.headI [] = (HAppend.hAppend (α := List Γ) [] (List.replicate (n + 1) default)).headI
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
⊢ ListBlank Γ
have apply : ∀ (a b : List Γ), BlankExtends a b → Eq (α := ListBlank Γ) (mk a.tail) (mk b.tail)
Tactic: apply l.liftOn (fun l ↦ ListBlank.mk l.tail)
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
a : List Γ
i : ℕ
⊢ Eq (α := ListBlank Γ) (mk a.tail) (mk (a ++ List.replicate i default).tail)
have refine : BlankExtends a.tail (a ++ List.replicate i default).tail
Tactic: refine Quotient.sound' (Or.inl ?_)
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
a : List Γ
i : ℕ
⊢ BlankExtends a.tail (a ++ List.replicate i default).tail
have nil : BlankExtends (List.tail []) (HAppend.hAppend (α := List Γ) [] (List.replicate i default)).tail
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
a : List Γ
i : ℕ
nil : BlankExtends (List.tail []) (HAppend.hAppend (α := List Γ) [] (List.replicate i default)).tail
⊢ BlankExtends a.tail (a ++ List.replicate i default).tail
have cons : ∀ (head : Γ) (tail : List Γ), BlankExtends (head :: tail).tail (head :: tail ++ List.replicate i default).tail
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
i : ℕ
⊢ BlankExtends (List.tail []) (HAppend.hAppend (α := List Γ) [] (List.replicate i default)).tail
have nil : BlankExtends (List.tail []) (HAppend.hAppend (α := List Γ) [] (List.replicate 0 default)).tail
Tactic: rcases i with - | i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
i : ℕ
nil : BlankExtends (List.tail []) (HAppend.hAppend (α := List Γ) [] (List.replicate 0 default)).tail
⊢ BlankExtends (List.tail []) (HAppend.hAppend (α := List Γ) [] (List.replicate i default)).tail
have nil₁ : ∀ (i : ℕ), BlankExtends (List.tail []) (HAppend.hAppend (α := List Γ) [] (List.replicate (i + 1) default)).tail
Tactic: rcases i with - | i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
i : ℕ
⊢ BlankExtends (List.tail []) (HAppend.hAppend (α := List Γ) [] (List.replicate i default)).tail
have nil : BlankExtends (List.tail []) (HAppend.hAppend (α := List Γ) [] (List.replicate 0 default)).tail
Tactic: rcases i with - | i <;> [exact ⟨0, rfl⟩; exact ⟨i, rfl⟩]
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
i : ℕ
nil : BlankExtends (List.tail []) (HAppend.hAppend (α := List Γ) [] (List.replicate 0 default)).tail
⊢ BlankExtends (List.tail []) (HAppend.hAppend (α := List Γ) [] (List.replicate i default)).tail
have nil₁ : ∀ (i : ℕ), BlankExtends (List.tail []) (HAppend.hAppend (α := List Γ) [] (List.replicate (i + 1) default)).tail
Tactic: rcases i with - | i <;> [exact ⟨0, rfl⟩; exact ⟨i, rfl⟩]
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
a : Γ
l : ListBlank Γ
⊢ ListBlank Γ
have apply : ∀ (a_1 b : List Γ), BlankExtends a_1 b → Eq (α := ListBlank Γ) (mk (a :: a_1)) (mk (a :: b))
Tactic: apply l.liftOn (fun l ↦ ListBlank.mk (List.cons a l))
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
⊢ ∀ (l : ListBlank Γ), cons l.head l.tail = l
have h : ∀ (a : List Γ), Eq (α := ListBlank Γ) (cons (head (Quotient.mk'' a)) (tail (Quotient.mk'' a))) (Quotient.mk'' a)
Tactic: apply Quotient.ind'
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
⊢ ∀ (a : List Γ), Eq (α := ListBlank Γ) (cons (head (Quotient.mk'' a)) (tail (Quotient.mk'' a))) (Quotient.mk'' a)
have h : ∀ (l : List Γ), BlankExtends l (head (Quotient.mk'' l) :: l.tail)
Tactic: refine fun l ↦ Quotient.sound' (Or.inr ?_)