English
Characterization of membership in sumLift₂: an element c belongs to sumLift₂ f g a b precisely in the four cases corresponding to the four case splits of a and b.
Русский
Характеризация членства в sumLift₂: элемент c принадлежит sumLift₂ f g a b ровно четырьмя случаями согласно разбиению a и b.
LaTeX
$$c ∈ sumLift₂ f g a b ⇔ (∃ a1 b1 c1, a = inl a1 ∧ b = inl b1 ∧ c = inl c1 ∧ c1 ∈ f a1 b1) ∨ (∃ a1 b2 c1, a = inl a1 ∧ b = inr b2 ∧ c = inl c1 ∧ c1 ∈ g1 a1 b2) ∨ (∃ a1 b2 c2, a = inl a1 ∧ b = inr b2 ∧ c = inr c2 ∧ c2 ∈ g2 a1 b2) ∨ (∃ a2 b2 c2, a = inr a2 ∧ b = inr b2 ∧ c = inr c2 ∧ c2 ∈ f2 a2 b2)$$
Lean4
theorem mem_sumLift₂ :
c ∈ sumLift₂ f g a b ↔
(∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂ :=
by
constructor
· rcases a with a | a <;> rcases b with b | b
· rw [sumLift₂, mem_map]
rintro ⟨c, hc, rfl⟩
exact Or.inl ⟨a, b, c, rfl, rfl, rfl, hc⟩
· refine fun h ↦ (notMem_empty _ h).elim
· refine fun h ↦ (notMem_empty _ h).elim
· rw [sumLift₂, mem_map]
rintro ⟨c, hc, rfl⟩
exact Or.inr ⟨a, b, c, rfl, rfl, rfl, hc⟩
· rintro (⟨a, b, c, rfl, rfl, rfl, h⟩ | ⟨a, b, c, rfl, rfl, rfl, h⟩) <;> exact mem_map_of_mem _ h
