-- Mathlib/Computability/PostTuringMachine.lean
theorem tr_reaches_rev {σ₁ σ₂ f₁ f₂} {tr : σ₁ → σ₂ → Prop} (H : Respects f₁ f₂ tr) {a₁ a₂}
    (aa : tr a₁ a₂) {b₂} (ab : Reaches f₂ a₂ b₂) :
    ∃ c₁ c₂, Reaches f₂ b₂ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Proof state:
case refl
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ : σ₂
⊢ ∃ c₁ c₂, Reaches f₂ a₂ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
exact ⟨_, _, ReflTransGen.refl, aa, ReflTransGen.refl⟩

Result:
no goals

Proof state:
case tail.intro.intro.intro.intro.inl.some
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ c₂ d₂ : σ₂
a✝ : ReflTransGen (fun a b => b ∈ f₂ a) a₂ c₂
cd : d₂ ∈ f₂ c₂
e₁ : σ₁
ae : Reaches f₁ a₁ e₁
ce : Reaches f₂ c₂ c₂
ee : tr e₁ c₂
g₁ : σ₁
eg : f₁ e₁ = some g₁
g₂ : σ₂
gg : tr g₁ g₂
cg : Reaches₁ f₂ c₂ g₂
⊢ ∃ c₁ c₂, Reaches f₂ d₂ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
rcases TransGen.head'_iff.1 cg with ⟨d', cd', dg⟩

Result:
case tail.intro.intro.intro.intro.inl.some.intro.intro
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ c₂ d₂ : σ₂
a✝ : ReflTransGen (fun a b => b ∈ f₂ a) a₂ c₂
cd : d₂ ∈ f₂ c₂
e₁ : σ₁
ae : Reaches f₁ a₁ e₁
ce : Reaches f₂ c₂ c₂
ee : tr e₁ c₂
g₁ : σ₁
eg : f₁ e₁ = some g₁
g₂ : σ₂
gg : tr g₁ g₂
cg : Reaches₁ f₂ c₂ g₂
d' : σ₂
cd' : d' ∈ f₂ c₂
dg : ReflTransGen (fun a b => b ∈ f₂ a) d' g₂
⊢ ∃ c₁ c₂, Reaches f₂ d₂ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Proof state:
case tail.intro.intro.intro.intro
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ c₂ d₂ : σ₂
a✝ : ReflTransGen (fun a b => b ∈ f₂ a) a₂ c₂
cd : d₂ ∈ f₂ c₂
e₁ : σ₁
e₂ : σ₂
ce : Reaches f₂ c₂ e₂
ee : tr e₁ e₂
ae : Reaches f₁ a₁ e₁
⊢ ∃ c₁ c₂, Reaches f₂ d₂ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
rcases ReflTransGen.cases_head ce with (rfl | ⟨d', cd', de⟩)

Result:
case tail.intro.intro.intro.intro.inl
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ c₂ d₂ : σ₂
a✝ : ReflTransGen (fun a b => b ∈ f₂ a) a₂ c₂
cd : d₂ ∈ f₂ c₂
e₁ : σ₁
ae : Reaches f₁ a₁ e₁
ce : Reaches f₂ c₂ c₂
ee : tr e₁ c₂
⊢ ∃ c₁ c₂, Reaches f₂ d₂ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

case tail.intro.intro.intro.intro.inr.intro.intro
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ c₂ d₂ : σ₂
a✝ : ReflTransGen (fun a b => b ∈ f₂ a) a₂ c₂
cd : d₂ ∈ f₂ c₂
e₁ : σ₁
e₂ : σ₂
ce : Reaches f₂ c₂ e₂
ee : tr e₁ e₂
ae : Reaches f₁ a₁ e₁
d' : σ₂
cd' : d' ∈ f₂ c₂
de : ReflTransGen (fun a b => b ∈ f₂ a) d' e₂
⊢ ∃ c₁ c₂, Reaches f₂ d₂ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Proof state:
case tail.intro.intro.intro.intro.inl.none
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ c₂ d₂ : σ₂
a✝ : ReflTransGen (fun a b => b ∈ f₂ a) a₂ c₂
cd : d₂ ∈ f₂ c₂
e₁ : σ₁
ae : Reaches f₁ a₁ e₁
ce : Reaches f₂ c₂ c₂
ee : tr e₁ c₂
eg : f₁ e₁ = none
c0 : f₂ c₂ = none
⊢ ∃ c₁ c₂, Reaches f₂ d₂ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
cases cd.symm.trans c0

Result:
no goals

Proof state:
case tail.intro.intro.intro.intro.inl.some
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ c₂ d₂ : σ₂
a✝ : ReflTransGen (fun a b => b ∈ f₂ a) a₂ c₂
cd : d₂ ∈ f₂ c₂
e₁ : σ₁
ae : Reaches f₁ a₁ e₁
ce : Reaches f₂ c₂ c₂
ee : tr e₁ c₂
g₁ : σ₁
eg : f₁ e₁ = some g₁
⊢ ∀ (x : σ₂), tr g₁ x → Reaches₁ f₂ c₂ x → ∃ c₁ c₂, Reaches f₂ d₂ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
intro g₂ gg cg

Result:
case tail.intro.intro.intro.intro.inl.some
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ c₂ d₂ : σ₂
a✝ : ReflTransGen (fun a b => b ∈ f₂ a) a₂ c₂
cd : d₂ ∈ f₂ c₂
e₁ : σ₁
ae : Reaches f₁ a₁ e₁
ce : Reaches f₂ c₂ c₂
ee : tr e₁ c₂
g₁ : σ₁
eg : f₁ e₁ = some g₁
g₂ : σ₂
gg : tr g₁ g₂
cg : Reaches₁ f₂ c₂ g₂
⊢ ∃ c₁ c₂, Reaches f₂ d₂ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Proof state:
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ : σ₂
ab : Reaches f₂ a₂ b₂
⊢ ∃ c₁ c₂, Reaches f₂ b₂ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
induction' ab with c₂ d₂ _ cd IH

Result:
case refl
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ : σ₂
⊢ ∃ c₁ c₂, Reaches f₂ a₂ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

case tail
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ c₂ d₂ : σ₂
a✝ : ReflTransGen (fun a b => b ∈ f₂ a) a₂ c₂
cd : d₂ ∈ f₂ c₂
IH : ∃ c₁ c₂_1, Reaches f₂ c₂ c₂_1 ∧ tr c₁ c₂_1 ∧ Reaches f₁ a₁ c₁
⊢ ∃ c₁ c₂, Reaches f₂ d₂ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Proof state:
case tail.intro.intro.intro.intro.inl.none
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ c₂ d₂ : σ₂
a✝ : ReflTransGen (fun a b => b ∈ f₂ a) a₂ c₂
cd : d₂ ∈ f₂ c₂
e₁ : σ₁
ae : Reaches f₁ a₁ e₁
ce : Reaches f₂ c₂ c₂
ee : tr e₁ c₂
eg : f₁ e₁ = none
⊢ f₂ c₂ = none → ∃ c₁ c₂, Reaches f₂ d₂ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
intro c0

Result:
case tail.intro.intro.intro.intro.inl.none
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ c₂ d₂ : σ₂
a✝ : ReflTransGen (fun a b => b ∈ f₂ a) a₂ c₂
cd : d₂ ∈ f₂ c₂
e₁ : σ₁
ae : Reaches f₁ a₁ e₁
ce : Reaches f₂ c₂ c₂
ee : tr e₁ c₂
eg : f₁ e₁ = none
c0 : f₂ c₂ = none
⊢ ∃ c₁ c₂, Reaches f₂ d₂ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁