English
For any relation r, the map (s1,s2) ↦ s1 + s2 is a fibration from the product GameAdd(CutExpand r, CutExpand r) to CutExpand r.
Русский
Для любого r отображение (s1,s2) ↦ s1 + s2 является фибрацией от произведения GameAdd(CutExpand r, CutExpand r) к CutExpand r.
LaTeX
$$$\\text{Fibration}(\\mathrm{GameAdd}(\\mathrm{CutExpand}(r),\\mathrm{CutExpand}(r)), \\mathrm{CutExpand}(r))\\; (s \\mapsto s_1 + s_2)$$$
Lean4
/-- For any relation `r` on `α`, multiset addition `Multiset α × Multiset α → Multiset α` is a
fibration between the game sum of `CutExpand r` with itself and `CutExpand r` itself. -/
theorem cutExpand_fibration (r : α → α → Prop) :
Fibration (GameAdd (CutExpand r) (CutExpand r)) (CutExpand r) fun s ↦ s.1 + s.2 :=
by
rintro ⟨s₁, s₂⟩ s ⟨t, a, hr, he⟩; dsimp at he ⊢
classical
obtain ⟨ha, rfl⟩ := add_singleton_eq_iff.1 he
rw [add_assoc, mem_add] at ha
obtain h | h := ha
· refine ⟨(s₁.erase a + t, s₂), GameAdd.fst ⟨t, a, hr, ?_⟩, ?_⟩
· rw [add_comm, ← add_assoc, singleton_add, cons_erase h]
· rw [add_assoc s₁, erase_add_left_pos _ h, add_right_comm, add_assoc]
· refine ⟨(s₁, (s₂ + t).erase a), GameAdd.snd ⟨t, a, hr, ?_⟩, ?_⟩
· rw [add_comm, singleton_add, cons_erase h]
· rw [add_assoc, erase_add_right_pos _ h]
