case intro
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ b₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
ab✝ : b₁ ∈ eval f₁ a₁
ab : Reaches f₁ a₁ b₁
b0 : f₁ b₁ = none
⊢ ∃ b₂, tr b₁ b₂ ∧ b₂ ∈ eval f₂ a₂
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ b₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
ab : b₁ ∈ eval f₁ a₁
⊢ ∃ b₂, tr b₁ b₂ ∧ b₂ ∈ eval f₂ a₂
cases' mem_eval.1 ab with ab b0
case intro.intro.intro
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ b₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
ab✝¹ : b₁ ∈ eval f₁ a₁
ab✝ : Reaches f₁ a₁ b₁
b0 : f₁ b₁ = none
b₂ : σ₂
bb : tr b₁ b₂
ab : Reaches f₂ a₂ b₂
⊢ ∃ b₂, tr b₁ b₂ ∧ b₂ ∈ eval f₂ a₂
case intro
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ b₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
ab✝ : b₁ ∈ eval f₁ a₁
ab : Reaches f₁ a₁ b₁
b0 : f₁ b₁ = none
⊢ ∃ b₂, tr b₁ b₂ ∧ b₂ ∈ eval f₂ a₂
rcases tr_reaches H aa ab with ⟨b₂, bb, ab⟩
case intro.intro.intro
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ b₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
ab✝¹ : b₁ ∈ eval f₁ a₁
ab✝ : Reaches f₁ a₁ b₁
b0 : f₁ b₁ = none
b₂ : σ₂
bb : tr b₁ b₂
ab : Reaches f₂ a₂ b₂
⊢ f₂ b₂ = none
case intro.intro.intro
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ b₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
ab✝¹ : b₁ ∈ eval f₁ a₁
ab✝ : Reaches f₁ a₁ b₁
b0 : f₁ b₁ = none
b₂ : σ₂
bb : tr b₁ b₂
ab : Reaches f₂ a₂ b₂
⊢ ∃ b₂, tr b₁ b₂ ∧ b₂ ∈ eval f₂ a₂
refine' ⟨_, bb, mem_eval.2 ⟨ab, _⟩⟩
case intro.intro.intro
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ b₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
ab✝¹ : b₁ ∈ eval f₁ a₁
ab✝ : Reaches f₁ a₁ b₁
b0 : f₁ b₁ = none
b₂ : σ₂
bb : tr b₁ b₂
ab : Reaches f₂ a₂ b₂
this :
  match f₁ b₁ with
  | some b₁ => ∃ b₂_1, tr b₁ b₂_1 ∧ Reaches₁ f₂ b₂ b₂_1
  | none => f₂ b₂ = none
⊢ f₂ b₂ = none
case intro.intro.intro
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ b₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
ab✝¹ : b₁ ∈ eval f₁ a₁
ab✝ : Reaches f₁ a₁ b₁
b0 : f₁ b₁ = none
b₂ : σ₂
bb : tr b₁ b₂
ab : Reaches f₂ a₂ b₂
⊢ f₂ b₂ = none
have := H bb
no goals
case intro.intro.intro
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ b₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
ab✝¹ : b₁ ∈ eval f₁ a₁
ab✝ : Reaches f₁ a₁ b₁
b0 : f₁ b₁ = none
b₂ : σ₂
bb : tr b₁ b₂
ab : Reaches f₂ a₂ b₂
this :
  match f₁ b₁ with
  | some b₁ => ∃ b₂_1, tr b₁ b₂_1 ∧ Reaches₁ f₂ b₂ b₂_1
  | none => f₂ b₂ = none
⊢ f₂ b₂ = none
rwa [b0] at this