-- Mathlib/Computability/EpsilonNFA.lean
theorem isPath_append {x y : List (Option α)} :
    M.IsPath s u (x ++ y) ↔ ∃ t, M.IsPath s t x ∧ M.IsPath t u y where
  mp

Proof state:
case cons
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
x : Option α
a : List (Option α)
ih : ∀ {s : σ}, M.IsPath s u (a ++ y) → ∃ t, M.IsPath s t a ∧ M.IsPath t u y
s : σ
⊢ M.IsPath s u (x :: a ++ y) → ∃ t, M.IsPath s t (x :: a) ∧ M.IsPath t u y

Tactic:
rintro (_ | ⟨t, _, _, _, _, _, h⟩)

Result:
case cons.cons
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
x : Option α
a : List (Option α)
ih : ∀ {s : σ}, M.IsPath s u (a ++ y) → ∃ t, M.IsPath s t a ∧ M.IsPath t u y
s t : σ
a✝ : t ∈ M.step s x
h : M.IsPath t u (a.append y)
⊢ ∃ t, M.IsPath s t (x :: a) ∧ M.IsPath t u y

Proof state:
case cons.cons
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
x : Option α
a : List (Option α)
ih : ∀ {s : σ}, M.IsPath s u (a ++ y) → ∃ t, M.IsPath s t a ∧ M.IsPath t u y
s t : σ
a✝ : t ∈ M.step s x
h : ∃ t_1, M.IsPath t t_1 a ∧ M.IsPath t_1 u y
⊢ ∃ t, M.IsPath s t (x :: a) ∧ M.IsPath t u y

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u
σ : Type v
M : εNFA α σ
s u : σ
x y : List (Option α)
⊢ (∃ t, M.IsPath s t x ∧ M.IsPath t u y) → M.IsPath s u (x ++ y)

Tactic:
intro ⟨t, hx, _⟩

Result:
α : Type u
σ : Type v
M : εNFA α σ
s u : σ
x y : List (Option α)
t : σ
hx : M.IsPath s t x
right✝ : M.IsPath t u y
⊢ M.IsPath s u (x ++ y)

Proof state:
case nil
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
s : σ
⊢ M.IsPath s u y → ∃ t, M.IsPath s t [] ∧ M.IsPath t u y

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u
σ : Type v
M : εNFA α σ
s u : σ
x y : List (Option α)
t : σ
hx : M.IsPath s t x
right✝ : M.IsPath t u y
⊢ M.IsPath s u (x ++ y)

Tactic:
induction x generalizing s <;> cases hx <;> tauto

Result:
no goals

Proof state:
case cons.cons
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
x : Option α
a : List (Option α)
ih : ∀ {s : σ}, M.IsPath s u (a ++ y) → ∃ t, M.IsPath s t a ∧ M.IsPath t u y
s t : σ
a✝ : t ∈ M.step s x
h : M.IsPath t u (a.append y)
⊢ ∃ t, M.IsPath s t (x :: a) ∧ M.IsPath t u y

Tactic:
apply ih at h

Result:
case cons.cons
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
x : Option α
a : List (Option α)
ih : ∀ {s : σ}, M.IsPath s u (a ++ y) → ∃ t, M.IsPath s t a ∧ M.IsPath t u y
s t : σ
a✝ : t ∈ M.step s x
h : ∃ t_1, M.IsPath t t_1 a ∧ M.IsPath t_1 u y
⊢ ∃ t, M.IsPath s t (x :: a) ∧ M.IsPath t u y

Proof state:
case nil
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
s : σ
⊢ M.IsPath s u ([] ++ y) → ∃ t, M.IsPath s t [] ∧ M.IsPath t u y

Tactic:
rw [List.nil_append]

Result:
case nil
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
s : σ
⊢ M.IsPath s u y → ∃ t, M.IsPath s t [] ∧ M.IsPath t u y

Proof state:
α : Type u
σ : Type v
M : εNFA α σ
s u : σ
x y : List (Option α)
⊢ M.IsPath s u (x ++ y) → ∃ t, M.IsPath s t x ∧ M.IsPath t u y

Tactic:
induction' x with x a ih generalizing s

Result:
case nil
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
s : σ
⊢ M.IsPath s u ([] ++ y) → ∃ t, M.IsPath s t [] ∧ M.IsPath t u y

case cons
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
x : Option α
a : List (Option α)
ih : ∀ {s : σ}, M.IsPath s u (a ++ y) → ∃ t, M.IsPath s t a ∧ M.IsPath t u y
s : σ
⊢ M.IsPath s u (x :: a ++ y) → ∃ t, M.IsPath s t (x :: a) ∧ M.IsPath t u y