-- Mathlib/Logic/Hydra.lean
theorem cutExpand_fibration (r : α → α → Prop) :
    Fibration (GameAdd (CutExpand r) (CutExpand r)) (CutExpand r) fun s ↦ s.1 + s.2

Proof state:
case mk.intro.intro.intro
α : Type u_1
r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : s + {a} = s₁ + s₂ + t
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = s

Tactic:
obtain ⟨ha, rfl⟩ := add_singleton_eq_iff.1 he

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

Proof state:
case mk.intro.intro.intro.intro.inr.refine_2
α : Type u_1
r : α → α → Prop
s₁ s₂ t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t
h : a ∈ s₂ + t
⊢ (s₁, (s₂ + t).erase a).1 + (s₁, (s₂ + t).erase a).2 = (s₁ + s₂ + t).erase a

Tactic:
rw [add_assoc, erase_add_right_pos _ h]

Result:
no goals

Proof state:
case mk.intro.intro.intro
α : Type u_1
r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : s + {a} = (fun s => s.1 + s.2) (s₁, s₂) + t
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ (fun s => s.1 + s.2) a' = s

Tactic:
dsimp at he ⊢

Result:
case mk.intro.intro.intro
α : Type u_1
r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : s + {a} = s₁ + s₂ + t
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = s

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

Tactic:
obtain h | h := ha

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

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

Proof state:
α : Type u_1
r : α → α → Prop
⊢ Fibration (GameAdd (CutExpand r) (CutExpand r)) (CutExpand r) fun s => s.1 + s.2

Tactic:
rintro ⟨s₁, s₂⟩ s ⟨t, a, hr, he⟩

Result:
case mk.intro.intro.intro
α : Type u_1
r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : s + {a} = (fun s => s.1 + s.2) (s₁, s₂) + t
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ (fun s => s.1 + s.2) a' = s

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

Tactic:
rw [add_assoc, mem_add] at ha

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

Proof state:
case mk.intro.intro.intro.intro.inl.refine_2
α : Type u_1
r : α → α → Prop
s₁ s₂ t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t
h : a ∈ s₁
⊢ (s₁.erase a + t, s₂).1 + (s₁.erase a + t, s₂).2 = (s₁ + s₂ + t).erase a

Tactic:
rw [add_assoc s₁, erase_add_left_pos _ h, add_right_comm, add_assoc]

Result:
no goals

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

Tactic:
refine ⟨(s₁, (s₂ + t).erase a), GameAdd.snd ⟨t, a, hr, ?_⟩, ?_⟩

Result:
case mk.intro.intro.intro.intro.inr.refine_1
α : Type u_1
r : α → α → Prop
s₁ s₂ t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t
h : a ∈ s₂ + t
⊢ (s₂ + t).erase a + {a} = s₂ + t

case mk.intro.intro.intro.intro.inr.refine_2
α : Type u_1
r : α → α → Prop
s₁ s₂ t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t
h : a ∈ s₂ + t
⊢ (s₁, (s₂ + t).erase a).1 + (s₁, (s₂ + t).erase a).2 = (s₁ + s₂ + t).erase a

Proof state:
case mk.intro.intro.intro.intro.inr.refine_1
α : Type u_1
r : α → α → Prop
s₁ s₂ t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t
h : a ∈ s₂ + t
⊢ (s₂ + t).erase a + {a} = s₂ + t

Tactic:
rw [add_comm, singleton_add, cons_erase h]

Result:
no goals

Proof state:
case mk.intro.intro.intro.intro.inl
α : Type u_1
r : α → α → Prop
s₁ s₂ t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t
h : a ∈ s₁
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = (s₁ + s₂ + t).erase a

Tactic:
refine ⟨(s₁.erase a + t, s₂), GameAdd.fst ⟨t, a, hr, ?_⟩, ?_⟩

Result:
case mk.intro.intro.intro.intro.inl.refine_1
α : Type u_1
r : α → α → Prop
s₁ s₂ t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t
h : a ∈ s₁
⊢ s₁.erase a + t + {a} = s₁ + t

case mk.intro.intro.intro.intro.inl.refine_2
α : Type u_1
r : α → α → Prop
s₁ s₂ t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t
h : a ∈ s₁
⊢ (s₁.erase a + t, s₂).1 + (s₁.erase a + t, s₂).2 = (s₁ + s₂ + t).erase a

Proof state:
case mk.intro.intro.intro.intro.inl.refine_1
α : Type u_1
r : α → α → Prop
s₁ s₂ t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t
h : a ∈ s₁
⊢ s₁.erase a + t + {a} = s₁ + t

Tactic:
rw [add_comm, ← add_assoc, singleton_add, cons_erase h]

Result:
no goals