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

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₁
⊢ ∃ b₂, tr b₁ b₂ ∧ Reaches₁ f₂ a₂ b₂

Tactic:
induction' ab with c₁ ac c₁ d₁ _ cd IH

Result:
case single
σ₁ : 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₁ : σ₁
ac : c₁ ∈ f₁ a₁
⊢ ∃ b₂, tr c₁ b₂ ∧ Reaches₁ f₂ a₂ b₂

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✝ : TransGen (fun a b => b ∈ f₁ a) a₁ c₁
cd : d₁ ∈ f₁ c₁
IH : ∃ b₂, tr c₁ b₂ ∧ Reaches₁ f₂ a₂ b₂
⊢ ∃ b₂, tr d₁ b₂ ∧ Reaches₁ f₂ a₂ b₂

Proof state:
case tail.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✝ : TransGen (fun a b => b ∈ f₁ a) a₁ c₁
cd : d₁ ∈ f₁ c₁
c₂ : σ₂
cc : tr c₁ c₂
ac₂ : Reaches₁ f₂ a₂ c₂
this :
  match some d₁ with
  | some b₁ => ∃ b₂, tr b₁ b₂ ∧ Reaches₁ f₂ c₂ b₂
  | none => f₂ c₂ = none
⊢ ∃ b₂, tr d₁ b₂ ∧ Reaches₁ f₂ a₂ b₂

Tactic:
rcases this with ⟨d₂, dd, cd₂⟩

Result:
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✝ : TransGen (fun a b => b ∈ f₁ a) a₁ c₁
cd : d₁ ∈ f₁ c₁
c₂ : σ₂
cc : tr c₁ c₂
ac₂ : Reaches₁ f₂ a₂ c₂
d₂ : σ₂
dd : tr d₁ d₂
cd₂ : Reaches₁ f₂ c₂ d₂
⊢ ∃ b₂, tr d₁ b₂ ∧ Reaches₁ f₂ a₂ b₂

Proof state:
case single
σ₁ : 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₁ : σ₁
ac : c₁ ∈ f₁ a₁
this :
  match f₁ a₁ with
  | some b₁ => ∃ b₂, tr b₁ b₂ ∧ Reaches₁ f₂ a₂ b₂
  | none => f₂ a₂ = none
⊢ ∃ b₂, tr c₁ b₂ ∧ Reaches₁ f₂ a₂ b₂

Tactic:
rwa [show f₁ a₁ = _ from ac] at this

Result:
no goals

Proof state:
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✝ : TransGen (fun a b => b ∈ f₁ a) a₁ c₁
cd : d₁ ∈ f₁ c₁
IH : ∃ b₂, tr c₁ b₂ ∧ Reaches₁ f₂ a₂ b₂
⊢ ∃ b₂, tr d₁ b₂ ∧ Reaches₁ f₂ a₂ b₂

Tactic:
rcases IH with ⟨c₂, cc, ac₂⟩

Result:
case tail.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✝ : TransGen (fun a b => b ∈ f₁ a) a₁ c₁
cd : d₁ ∈ f₁ c₁
c₂ : σ₂
cc : tr c₁ c₂
ac₂ : Reaches₁ f₂ a₂ c₂
⊢ ∃ b₂, tr d₁ b₂ ∧ Reaches₁ f₂ a₂ b₂

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✝ : TransGen (fun a b => b ∈ f₁ a) a₁ c₁
cd : d₁ ∈ f₁ c₁
c₂ : σ₂
cc : tr c₁ c₂
ac₂ : Reaches₁ f₂ a₂ c₂
d₂ : σ₂
dd : tr d₁ d₂
cd₂ : Reaches₁ f₂ c₂ d₂
⊢ ∃ b₂, tr d₁ b₂ ∧ Reaches₁ f₂ a₂ b₂

Tactic:
exact ⟨_, dd, ac₂.trans cd₂⟩

Result:
no goals

Proof state:
case single
σ₁ : 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₁ : σ₁
ac : c₁ ∈ f₁ a₁
⊢ ∃ b₂, tr c₁ b₂ ∧ Reaches₁ f₂ a₂ b₂

Tactic:
have := H aa

Result:
case single
σ₁ : 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₁ : σ₁
ac : c₁ ∈ f₁ a₁
this :
  match f₁ a₁ with
  | some b₁ => ∃ b₂, tr b₁ b₂ ∧ Reaches₁ f₂ a₂ b₂
  | none => f₂ a₂ = none
⊢ ∃ b₂, tr c₁ b₂ ∧ Reaches₁ f₂ a₂ b₂

Proof state:
case tail.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✝ : TransGen (fun a b => b ∈ f₁ a) a₁ c₁
cd : d₁ ∈ f₁ c₁
c₂ : σ₂
cc : tr c₁ c₂
ac₂ : Reaches₁ f₂ a₂ c₂
this :
  match f₁ c₁ with
  | some b₁ => ∃ b₂, tr b₁ b₂ ∧ Reaches₁ f₂ c₂ b₂
  | none => f₂ c₂ = none
⊢ ∃ b₂, tr d₁ b₂ ∧ Reaches₁ f₂ a₂ b₂

Tactic:
rw [show f₁ c₁ = _ from cd] at this

Result:
case tail.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✝ : TransGen (fun a b => b ∈ f₁ a) a₁ c₁
cd : d₁ ∈ f₁ c₁
c₂ : σ₂
cc : tr c₁ c₂
ac₂ : Reaches₁ f₂ a₂ c₂
this :
  match some d₁ with
  | some b₁ => ∃ b₂, tr b₁ b₂ ∧ Reaches₁ f₂ c₂ b₂
  | none => f₂ c₂ = none
⊢ ∃ b₂, tr d₁ b₂ ∧ Reaches₁ f₂ a₂ b₂

Proof state:
case tail.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✝ : TransGen (fun a b => b ∈ f₁ a) a₁ c₁
cd : d₁ ∈ f₁ c₁
c₂ : σ₂
cc : tr c₁ c₂
ac₂ : Reaches₁ f₂ a₂ c₂
⊢ ∃ b₂, tr d₁ b₂ ∧ Reaches₁ f₂ a₂ b₂

Tactic:
have := H cc

Result:
case tail.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✝ : TransGen (fun a b => b ∈ f₁ a) a₁ c₁
cd : d₁ ∈ f₁ c₁
c₂ : σ₂
cc : tr c₁ c₂
ac₂ : Reaches₁ f₂ a₂ c₂
this :
  match f₁ c₁ with
  | some b₁ => ∃ b₂, tr b₁ b₂ ∧ Reaches₁ f₂ c₂ b₂
  | none => f₂ c₂ = none
⊢ ∃ b₂, tr d₁ b₂ ∧ Reaches₁ f₂ a₂ b₂