case intro.intro
σ : Type u_1
f : σ → Option σ
a b c : σ
h₁ : Reaches₁ f a c
h₂ : b ∈ f a
b' : σ
hab : b' ∈ f a
hbc : ReflTransGen (fun a b => b ∈ f a) b' c
⊢ Reaches f b c
σ : Type u_1
f : σ → Option σ
a b c : σ
h₁ : Reaches₁ f a c
h₂ : b ∈ f a
⊢ Reaches f b c
rcases TransGen.head'_iff.1 h₁ with ⟨b', hab, hbc⟩
case intro.intro.refl
σ : Type u_1
f : σ → Option σ
a b c : σ
h₁ : Reaches₁ f a c
h₂ hab : b ∈ f a
hbc : ReflTransGen (fun a b => b ∈ f a) b c
⊢ Reaches f b c
case intro.intro
σ : Type u_1
f : σ → Option σ
a b c : σ
h₁ : Reaches₁ f a c
h₂ : b ∈ f a
b' : σ
hab : b' ∈ f a
hbc : ReflTransGen (fun a b => b ∈ f a) b' c
⊢ Reaches f b c
cases Option.mem_unique hab h₂
no goals
case intro.intro.refl
σ : Type u_1
f : σ → Option σ
a b c : σ
h₁ : Reaches₁ f a c
h₂ hab : b ∈ f a
hbc : ReflTransGen (fun a b => b ∈ f a) b c
⊢ Reaches f b c
exact hbc