case intro.intro
σ₁ σ₂ : Type u_1
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
H : Respects f₁ f₂ fun a b => tr a = b
a₁ : σ₁
b₂ : σ₂
h : b₂ ∈ tr <$> eval f₁ a₁
b₁ : σ₁
ab : b₁ ∈ eval f₁ a₁
bb : tr b₁ = b₂
⊢ b₂ ∈ eval f₂ (tr a₁)
σ₁ σ₂ : Type u_1
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
H : Respects f₁ f₂ fun a b => tr a = b
a₁ : σ₁
b₂ : σ₂
h : b₂ ∈ tr <$> eval f₁ a₁
⊢ b₂ ∈ eval f₂ (tr a₁)
rcases(Part.mem_map_iff _).1 h with ⟨b₁, ab, bb⟩
case intro.intro.intro.intro
σ₁ σ₂ : Type u_1
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
H : Respects f₁ f₂ fun a b => tr a = b
a₁ : σ₁
b₂ : σ₂
h✝ : b₂ ∈ tr <$> eval f₁ a₁
b₁ : σ₁
ab : b₁ ∈ eval f₁ a₁
bb : tr b₁ = b₂
h : tr b₁ ∈ eval f₂ (tr a₁)
⊢ b₂ ∈ eval f₂ (tr a₁)
case intro.intro
σ₁ σ₂ : Type u_1
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
H : Respects f₁ f₂ fun a b => tr a = b
a₁ : σ₁
b₂ : σ₂
h : b₂ ∈ tr <$> eval f₁ a₁
b₁ : σ₁
ab : b₁ ∈ eval f₁ a₁
bb : tr b₁ = b₂
⊢ b₂ ∈ eval f₂ (tr a₁)
rcases tr_eval H rfl ab with ⟨_, rfl, h⟩
no goals
case intro.intro.intro.intro
σ₁ σ₂ : Type u_1
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
H : Respects f₁ f₂ fun a b => tr a = b
a₁ : σ₁
b₂ : σ₂
h✝ : b₂ ∈ tr <$> eval f₁ a₁
b₁ : σ₁
ab : b₁ ∈ eval f₁ a₁
bb : tr b₁ = b₂
h : tr b₁ ∈ eval f₂ (tr a₁)
⊢ b₂ ∈ eval f₂ (tr a₁)
rwa [bb] at h