English
An element x lies in sigmaLift f a b precisely when a and b have the same index and the γ-component x.2 belongs to f(a.2,b.2) (after transporting along the equality).
Русский
Элемент x принадлежит sigmaLift f a b тогда и только тогда, когда индексы a и x совпадают, и компонент x_2 принадлежит f(a_2,b_2) после переноса по равенству.
LaTeX
$$$$ x \in \sigmaLift f a b \iff \exists ha hb,\ x.2 \in f (ha \ ▸ a.2) (hb \ ▸ b.2) $$$$
Lean4
theorem mem_sigmaLift (f : ∀ ⦃i⦄, α i → β i → Finset (γ i)) (a : Sigma α) (b : Sigma β) (x : Sigma γ) :
x ∈ sigmaLift f a b ↔ ∃ (ha : a.1 = x.1) (hb : b.1 = x.1), x.2 ∈ f (ha ▸ a.2) (hb ▸ b.2) :=
by
obtain ⟨⟨i, a⟩, j, b⟩ := a, b
obtain rfl | h := Decidable.eq_or_ne i j
· constructor
· simp_rw [sigmaLift]
simp only [dite_eq_ite, ite_true, mem_map, Embedding.sigmaMk_apply, forall_exists_index, and_imp]
rintro x hx rfl
exact ⟨rfl, rfl, hx⟩
· rintro ⟨⟨⟩, ⟨⟩, hx⟩
rw [sigmaLift, dif_pos rfl, mem_map]
exact ⟨_, hx, by simp⟩
· rw [sigmaLift, dif_neg h]
refine iff_of_false (notMem_empty _) ?_
rintro ⟨⟨⟩, ⟨⟩, _⟩
exact h rfl
