English
Liftr r x y holds exactly when x and y decompose over the same root a and child maps f0, f1 with pointwise r on all children.
Русский
Liftr r x y выполняется тогда и только тогда, когда x и y распадаются на общий корень a и карты-потомки f0, f1, причём для каждого i выполняется r (f0 i) (f1 i).
LaTeX
$$$ Liftr\ r\ x\ y \iff \exists a\ f_0\ f_1, x = \langle a, f_0\rangle \land y = \langle a, f_1\rangle \land \forall i, r (f_0 i) (f_1 i).$$$
Lean4
theorem liftr_iff {α : Type u} (r : α → α → Prop) (x y : P α) :
Liftr r x y ↔ ∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ i, r (f₀ i) (f₁ i) :=
by
constructor
· rintro ⟨u, xeq, yeq⟩
rcases h : u with ⟨a, f⟩
use a, fun i => (f i).val.fst, fun i => (f i).val.snd
constructor
· rw [← xeq, h]
rfl
constructor
· rw [← yeq, h]
rfl
intro i
exact (f i).property
rintro ⟨a, f₀, f₁, xeq, yeq, h⟩
use ⟨a, fun i => ⟨(f₀ i, f₁ i), h i⟩⟩
constructor
· rw [xeq]
rfl
rw [yeq]; rfl
