-- Mathlib/Computability/EpsilonNFA.lean
theorem mem_εClosure_iff_exists_path {s₁ s₂ : σ} :
    s₂ ∈ M.εClosure {s₁} ↔ ∃ n, M.IsPath s₁ s₂ (.replicate n none) where
  mp h

Proof state:
case h
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure {s₁} s✝
n : ℕ
h✝ : M.IsPath s₁ s✝ (List.replicate n none)
⊢ ∃ t, M.IsPath s₁ t (List.replicate n none) ∧ M.IsPath t t✝ (List.replicate 1 none)

Tactic:
tauto

Result:
no goals

Proof state:
case succ
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
n✝ : ℕ
a✝ : ∀ {s₂ : σ}, M.IsPath s₁ s₂ (List.replicate n✝ none) → s₂ ∈ M.εClosure {s₁}
s₂ : σ
h : ∃ t, M.IsPath s₁ t (List.replicate n✝ none) ∧ s₂ ∈ M.step t none
⊢ s₂ ∈ M.εClosure {s₁}

Tactic:
obtain ⟨t, _, _⟩ := h

Result:
case succ.intro.intro
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
n✝ : ℕ
a✝ : ∀ {s₂ : σ}, M.IsPath s₁ s₂ (List.replicate n✝ none) → s₂ ∈ M.εClosure {s₁}
s₂ t : σ
left✝ : M.IsPath s₁ t (List.replicate n✝ none)
right✝ : s₂ ∈ M.step t none
⊢ s₂ ∈ M.εClosure {s₁}

Proof state:
case succ.intro.intro
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
n✝ : ℕ
a✝ : ∀ {s₂ : σ}, M.IsPath s₁ s₂ (List.replicate n✝ none) → s₂ ∈ M.εClosure {s₁}
s₂ t : σ
left✝ : M.IsPath s₁ t (List.replicate n✝ none)
right✝ : s₂ ∈ M.step t none
⊢ s₂ ∈ M.εClosure {s₁}

Tactic:
solve_by_elim [εClosure.step]

Result:
no goals

Proof state:
case step.intro
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure {s₁} s✝
n : ℕ
h✝ : M.IsPath s₁ s✝ (List.replicate n none)
⊢ ∃ n, M.IsPath s₁ t✝ (List.replicate n none)

Tactic:
use n + 1

Result:
case h
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure {s₁} s✝
n : ℕ
h✝ : M.IsPath s₁ s✝ (List.replicate n none)
⊢ M.IsPath s₁ t✝ (List.replicate (n + 1) none)

Proof state:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
⊢ (∃ n, M.IsPath s₁ s₂ (List.replicate n none)) → s₂ ∈ M.εClosure {s₁}

Tactic:
intro ⟨n, h⟩

Result:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
n : ℕ
h : M.IsPath s₁ s₂ (List.replicate n none)
⊢ s₂ ∈ M.εClosure {s₁}

Proof state:
case succ
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
n✝ : ℕ
a✝ : ∀ {s₂ : σ}, M.IsPath s₁ s₂ (List.replicate n✝ none) → s₂ ∈ M.εClosure {s₁}
s₂ : σ
h : M.IsPath s₁ s₂ (List.replicate (n✝ + 1) none)
⊢ s₂ ∈ M.εClosure {s₁}

Tactic:
simp_rw [List.replicate_add, isPath_append, List.replicate_one, isPath_singleton] at h

Result:
case succ
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
n✝ : ℕ
a✝ : ∀ {s₂ : σ}, M.IsPath s₁ s₂ (List.replicate n✝ none) → s₂ ∈ M.εClosure {s₁}
s₂ : σ
h : ∃ t, M.IsPath s₁ t (List.replicate n✝ none) ∧ s₂ ∈ M.step t none
⊢ s₂ ∈ M.εClosure {s₁}

Proof state:
case zero
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
h : M.IsPath s₁ s₂ (List.replicate 0 none)
⊢ s₂ ∈ M.εClosure {s₁}

Tactic:
rw [List.replicate_zero] at h

Result:
case zero
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
h : M.IsPath s₁ s₂ []
⊢ s₂ ∈ M.εClosure {s₁}

Proof state:
case h
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ t : σ
a✝ : t ∈ {s₁}
⊢ M.IsPath s₁ t (List.replicate 0 none)

Tactic:
subst t

Result:
case h
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
⊢ M.IsPath s₁ s₁ (List.replicate 0 none)

Proof state:
case zero
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
h : M.IsPath s₁ s₂ []
⊢ s₂ ∈ M.εClosure {s₁}

Tactic:
apply IsPath.eq_of_nil at h

Result:
case zero
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
h : s₁ = s₂
⊢ s₂ ∈ M.εClosure {s₁}

Proof state:
case h
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
⊢ M.IsPath s₁ s₁ (List.replicate 0 none)

Tactic:
apply IsPath.nil

Result:
no goals

Proof state:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
n : ℕ
h : M.IsPath s₁ s₂ (List.replicate n none)
⊢ s₂ ∈ M.εClosure {s₁}

Tactic:
induction n generalizing s₂

Result:
case zero
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
h : M.IsPath s₁ s₂ (List.replicate 0 none)
⊢ s₂ ∈ M.εClosure {s₁}

case succ
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
n✝ : ℕ
a✝ : ∀ {s₂ : σ}, M.IsPath s₁ s₂ (List.replicate n✝ none) → s₂ ∈ M.εClosure {s₁}
s₂ : σ
h : M.IsPath s₁ s₂ (List.replicate (n✝ + 1) none)
⊢ s₂ ∈ M.εClosure {s₁}

Proof state:
case zero
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
h : s₁ = s₂
⊢ s₂ ∈ M.εClosure {s₁}

Tactic:
solve_by_elim

Result:
no goals

Proof state:
case h
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure {s₁} s✝
n : ℕ
h✝ : M.IsPath s₁ s✝ (List.replicate n none)
⊢ M.IsPath s₁ t✝ (List.replicate (n + 1) none)

Tactic:
rw [List.replicate_add, isPath_append]

Result:
case h
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure {s₁} s✝
n : ℕ
h✝ : M.IsPath s₁ s✝ (List.replicate n none)
⊢ ∃ t, M.IsPath s₁ t (List.replicate n none) ∧ M.IsPath t t✝ (List.replicate 1 none)

Proof state:
case base
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ t : σ
a✝ : t ∈ {s₁}
⊢ ∃ n, M.IsPath s₁ t (List.replicate n none)

Tactic:
use 0

Result:
case h
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ t : σ
a✝ : t ∈ {s₁}
⊢ M.IsPath s₁ t (List.replicate 0 none)

Proof state:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
h : s₂ ∈ M.εClosure {s₁}
⊢ ∃ n, M.IsPath s₁ s₂ (List.replicate n none)

Tactic:
induction' h with t _ _ _ _ _ ih

Result:
case base
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ t : σ
a✝ : t ∈ {s₁}
⊢ ∃ n, M.IsPath s₁ t (List.replicate n none)

case step
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure {s₁} s✝
ih : ∃ n, M.IsPath s₁ s✝ (List.replicate n none)
⊢ ∃ n, M.IsPath s₁ t✝ (List.replicate n none)

Proof state:
case step
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure {s₁} s✝
ih : ∃ n, M.IsPath s₁ s✝ (List.replicate n none)
⊢ ∃ n, M.IsPath s₁ t✝ (List.replicate n none)

Tactic:
obtain ⟨n, _⟩ := ih

Result:
case step.intro
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure {s₁} s✝
n : ℕ
h✝ : M.IsPath s₁ s✝ (List.replicate n none)
⊢ ∃ n, M.IsPath s₁ t✝ (List.replicate n none)