English
In the mirrored setting, if a relation H respects f1,f2 and a1 relates to a2 via tr, and b2 is reachable from a2 via f2, then there exist c1,c2 with b2 reached via f2 and c1,c2 related by tr and a1 reaches c1 via f1.
Русский
В зеркальном окружении, если H сохраняет f1,f2 и a1 связан с a2 через tr, и b2 достижим из a2 через f2, то существуют c1,c2, такие что b2 достигает c2 через f2 и c1,c2 связаны через tr и a1 достигает c1 через f1.
LaTeX
$$$\\forall {f_1 f_2 tr} (H : Respects f_1 f_2 tr) \\forall {a_1 a_2}, tr\\ a_1 a_2 \\to \\forall {b_2}, Reaches f_2 a_2 b_2 \\to \\exists c_1 c_2, Reaches f_2 b_2 c_2 \\wedge tr c_1 c_2 \\wedge Reaches f_1 a_1 c_1$$$
Lean4
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₁ := by
induction ab with
| refl => exact ⟨_, _, ReflTransGen.refl, aa, ReflTransGen.refl⟩
| tail _ cd IH =>
rcases IH with ⟨e₁, e₂, ce, ee, ae⟩
rcases ReflTransGen.cases_head ce with (rfl | ⟨d', cd', de⟩)
· have := H ee
revert this
rcases eg : f₁ e₁ with - | g₁ <;> simp only [and_imp, exists_imp]
· intro c0
cases cd.symm.trans c0
· intro g₂ gg cg
rcases TransGen.head'_iff.1 cg with ⟨d', cd', dg⟩
cases Option.mem_unique cd cd'
exact ⟨_, _, dg, gg, ae.tail eg⟩
· cases Option.mem_unique cd cd'
exact ⟨_, _, de, ee, ae⟩
