case mk.intro.intro.intro
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = (fun s => s.fst + s.snd) (s₁, s₂) + t
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ (fun s => s.fst + s.snd) a' = s
α : Type u_1
r✝ r : α → α → Prop
⊢ Fibration (GameAdd (CutExpand r) (CutExpand r)) (CutExpand r) fun s => s.fst + s.snd
rintro ⟨s₁, s₂⟩ s ⟨t, a, hr, he⟩
case mk.intro.intro.intro
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.fst + a'.snd = s
case mk.intro.intro.intro
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = (fun s => s.fst + s.snd) (s₁, s₂) + t
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ (fun s => s.fst + s.snd) a' = s
dsimp at he ⊢
case mk.intro.intro.intro.intro
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
ha : a ∈ s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.fst + a'.snd = s
case mk.intro.intro.intro
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.fst + a'.snd = s
obtain ⟨ha, hb⟩ := add_singleton_eq_iff.1 he
case mk.intro.intro.intro.intro
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
ha : a ∈ s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.fst + a'.snd = erase (s₁ + s₂ + t) a

α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
⊢ DecidableEq α
case mk.intro.intro.intro.intro
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
ha : a ∈ s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.fst + a'.snd = s
rw [hb]
case mk.intro.intro.intro.intro
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
ha : a ∈ s₁ ∨ a ∈ s₂ + t
hb : s = erase (s₁ + s₂ + t) a
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.fst + a'.snd = erase (s₁ + s₂ + t) a

α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
⊢ DecidableEq α
case mk.intro.intro.intro.intro
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
ha : a ∈ s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.fst + a'.snd = erase (s₁ + s₂ + t) a

α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
⊢ DecidableEq α
rw [add_assoc, mem_add] at ha
case mk.intro.intro.intro.intro.inl
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
h : a ∈ s₁
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.fst + a'.snd = erase (s₁ + s₂ + t) a

case mk.intro.intro.intro.intro.inr
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
h : a ∈ s₂ + t
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.fst + a'.snd = erase (s₁ + s₂ + t) a

α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
⊢ DecidableEq α
case mk.intro.intro.intro.intro
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
ha : a ∈ s₁ ∨ a ∈ s₂ + t
hb : s = erase (s₁ + s₂ + t) a
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.fst + a'.snd = erase (s₁ + s₂ + t) a

α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
⊢ DecidableEq α
obtain h | h := ha
case mk.intro.intro.intro.intro.inl.refine'_1
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
h : a ∈ s₁
⊢ erase s₁ a + t + {a} = s₁ + t

case mk.intro.intro.intro.intro.inl.refine'_2
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
h : a ∈ s₁
⊢ (erase s₁ a + t, s₂).fst + (erase s₁ a + t, s₂).snd = erase (s₁ + s₂ + t) a
case mk.intro.intro.intro.intro.inl
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
h : a ∈ s₁
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.fst + a'.snd = erase (s₁ + s₂ + t) a
refine' ⟨(s₁.erase a + t, s₂), GameAdd.fst ⟨t, a, hr, _⟩, _⟩
no goals
case mk.intro.intro.intro.intro.inl.refine'_1
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
h : a ∈ s₁
⊢ erase s₁ a + t + {a} = s₁ + t
rw [add_comm, ← add_assoc, singleton_add, cons_erase h]
no goals
case mk.intro.intro.intro.intro.inl.refine'_2
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
h : a ∈ s₁
⊢ (erase s₁ a + t, s₂).fst + (erase s₁ a + t, s₂).snd = erase (s₁ + s₂ + t) a
rw [add_assoc s₁, erase_add_left_pos _ h, add_right_comm, add_assoc]
case mk.intro.intro.intro.intro.inr.refine'_1
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
h : a ∈ s₂ + t
⊢ erase (s₂ + t) a + {a} = s₂ + t

case mk.intro.intro.intro.intro.inr.refine'_2
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
h : a ∈ s₂ + t
⊢ (s₁, erase (s₂ + t) a).fst + (s₁, erase (s₂ + t) a).snd = erase (s₁ + s₂ + t) a
case mk.intro.intro.intro.intro.inr
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
h : a ∈ s₂ + t
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.fst + a'.snd = erase (s₁ + s₂ + t) a
refine' ⟨(s₁, (s₂ + t).erase a), GameAdd.snd ⟨t, a, hr, _⟩, _⟩
no goals
case mk.intro.intro.intro.intro.inr.refine'_1
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
h : a ∈ s₂ + t
⊢ erase (s₂ + t) a + {a} = s₂ + t
rw [add_comm, singleton_add, cons_erase h]
no goals
case mk.intro.intro.intro.intro.inr.refine'_2
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
h : a ∈ s₂ + t
⊢ (s₁, erase (s₂ + t) a).fst + (s₁, erase (s₂ + t) a).snd = erase (s₁ + s₂ + t) a
rw [add_assoc, erase_add_right_pos _ h]