awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : 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₁
inl : s₁.erase a + t + {a} = s₁ + t
⊢ ∃ (a' : Multiset α × Multiset α),
    GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = (s₁ + s₂ + t).erase a
have inl₁ : (s₁.erase a + t, s₂).1 + (s₁.erase a + t, s₂).2 = (s₁ + s₂ + t).erase a
Tactic: refine ⟨(s₁.erase a + t, s₂), GameAdd.fst ⟨t, a, hr, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : 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
have inl : {a} + (s₁.erase a + t) = s₁ + t
Tactic: rw [add_comm, ← add_assoc, singleton_add, cons_erase h]
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : 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₁
inl : {a} + (s₁.erase a + t) = s₁ + t
⊢ s₁.erase a + t + {a} = s₁ + t
have inl₁ : {a} + s₁.erase a + t = s₁ + t
Tactic: rw [add_comm, ← add_assoc, singleton_add, cons_erase h]
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : 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₁
inl : {a} + (s₁.erase a + t) = s₁ + t
inl₁ : {a} + s₁.erase a + t = s₁ + t
⊢ s₁.erase a + t + {a} = s₁ + t
have inl₂ : a ::ₘ s₁.erase a + t = s₁ + t
Tactic: rw [add_comm, ← add_assoc, singleton_add, cons_erase h]
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : 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₁
inl : {a} + (s₁.erase a + t) = s₁ + t
inl₁ : {a} + s₁.erase a + t = s₁ + t
inl₂ : a ::ₘ s₁.erase a + t = s₁ + t
⊢ s₁.erase a + t + {a} = s₁ + t
have inl₃ : s₁ + t = s₁ + t
Tactic: rw [add_comm, ← add_assoc, singleton_add, cons_erase h]
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : 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
have inl : (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]
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : 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₁
inl : (s₁.erase a + t, s₂).1 + (s₁.erase a + t, s₂).2 = (s₁ + (s₂ + t)).erase a
⊢ (s₁.erase a + t, s₂).1 + (s₁.erase a + t, s₂).2 = (s₁ + s₂ + t).erase a
have inl₁ : (s₁.erase a + t, s₂).1 + (s₁.erase a + t, s₂).2 = s₁.erase a + (s₂ + t)
Tactic: rw [add_assoc s₁, erase_add_left_pos _ h, add_right_comm, add_assoc]
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : 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₁
inl : (s₁.erase a + t, s₂).1 + (s₁.erase a + t, s₂).2 = (s₁ + (s₂ + t)).erase a
inl₁ : (s₁.erase a + t, s₂).1 + (s₁.erase a + t, s₂).2 = s₁.erase a + (s₂ + t)
⊢ (s₁.erase a + t, s₂).1 + (s₁.erase a + t, s₂).2 = (s₁ + s₂ + t).erase a
have inl₂ : s₁.erase a + (s₁.erase a + t, s₂).2 + t = s₁.erase a + (s₂ + t)
Tactic: rw [add_assoc s₁, erase_add_left_pos _ h, add_right_comm, add_assoc]
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : 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₁
inl : (s₁.erase a + t, s₂).1 + (s₁.erase a + t, s₂).2 = (s₁ + (s₂ + t)).erase a
inl₁ : (s₁.erase a + t, s₂).1 + (s₁.erase a + t, s₂).2 = s₁.erase a + (s₂ + t)
inl₂ : s₁.erase a + (s₁.erase a + t, s₂).2 + t = s₁.erase a + (s₂ + t)
⊢ (s₁.erase a + t, s₂).1 + (s₁.erase a + t, s₂).2 = (s₁ + s₂ + t).erase a
have inl₃ : s₁.erase a + ((s₁.erase a + t, s₂).2 + t) = s₁.erase a + (s₂ + t)
Tactic: rw [add_assoc s₁, erase_add_left_pos _ h, add_right_comm, add_assoc]
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : 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' : Multiset α × Multiset α),
    GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = (s₁ + s₂ + t).erase a
have inr : (s₂ + t).erase a + {a} = s₂ + t
Tactic: refine ⟨(s₁, (s₂ + t).erase a), GameAdd.snd ⟨t, a, hr, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : 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
inr : (s₂ + t).erase a + {a} = s₂ + t
⊢ ∃ (a' : Multiset α × Multiset α),
    GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = (s₁ + s₂ + t).erase a
have inr₁ : (s₁, (s₂ + t).erase a).1 + (s₁, (s₂ + t).erase a).2 = (s₁ + s₂ + t).erase a
Tactic: refine ⟨(s₁, (s₂ + t).erase a), GameAdd.snd ⟨t, a, hr, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : 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
have inr : {a} + (s₂ + t).erase a = s₂ + t
Tactic: rw [add_comm, singleton_add, cons_erase h]
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : 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
inr : {a} + (s₂ + t).erase a = s₂ + t
⊢ (s₂ + t).erase a + {a} = s₂ + t
have inr₁ : a ::ₘ (s₂ + t).erase a = s₂ + t
Tactic: rw [add_comm, singleton_add, cons_erase h]
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : 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
inr : {a} + (s₂ + t).erase a = s₂ + t
inr₁ : a ::ₘ (s₂ + t).erase a = s₂ + t
⊢ (s₂ + t).erase a + {a} = s₂ + t
have inr₂ : s₂ + t = s₂ + t
Tactic: rw [add_comm, singleton_add, cons_erase h]
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : 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
have inr : (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]
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : 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
inr : (s₁, (s₂ + t).erase a).1 + (s₁, (s₂ + t).erase a).2 = (s₁ + (s₂ + t)).erase a
⊢ (s₁, (s₂ + t).erase a).1 + (s₁, (s₂ + t).erase a).2 = (s₁ + s₂ + t).erase a
have inr₁ : (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]
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : Type u_1
r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : s + {a} = s₁ + s₂ + t
⊢ ∃ (a' : Multiset α × Multiset α), GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = s
have obtain : ∀ (ha : a ∈ s₁ + s₂ + t) (he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t),
  ∃ (a' : Multiset α × Multiset α),
    GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = (s₁ + s₂ + t).erase a
Tactic: 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]
Cleared hypotheses: s, he
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : Type u_1
r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : s + {a} = s₁ + s₂ + t
obtain :
  ∀ (ha : a ∈ s₁ + s₂ + t) (he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t),
    ∃ (a' : Multiset α × Multiset α),
      GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = (s₁ + s₂ + t).erase a
⊢ ∃ (a' : Multiset α × Multiset α), GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = s
have obtain₁ : ∀ (ha : a ∈ s₁ ∨ a ∈ s₂ + t) (he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t),
  ∃ (a' : Multiset α × Multiset α),
    GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = (s₁ + s₂ + t).erase a
Tactic: 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]
Cleared hypotheses: s, he
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : Type u_1
r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : s + {a} = s₁ + s₂ + t
obtain :
  ∀ (ha : a ∈ s₁ + s₂ + t) (he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t),
    ∃ (a' : Multiset α × Multiset α),
      GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = (s₁ + s₂ + t).erase a
obtain₁ :
  ∀ (ha : a ∈ s₁ ∨ a ∈ s₂ + t) (he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t),
    ∃ (a' : Multiset α × Multiset α),
      GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = (s₁ + s₂ + t).erase a
⊢ ∃ (a' : Multiset α × Multiset α), GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = s
have inl : ∀ (he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t) (h : a ∈ s₁),
  ∃ (a' : Multiset α × Multiset α),
    GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = (s₁ + s₂ + t).erase a
Tactic: 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]
Cleared hypotheses: s, he
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : Type u_1
r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : s + {a} = s₁ + s₂ + t
obtain :
  ∀ (ha : a ∈ s₁ + s₂ + t) (he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t),
    ∃ (a' : Multiset α × Multiset α),
      GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = (s₁ + s₂ + t).erase a
obtain₁ :
  ∀ (ha : a ∈ s₁ ∨ a ∈ s₂ + t) (he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t),
    ∃ (a' : Multiset α × Multiset α),
      GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = (s₁ + s₂ + t).erase a
inl :
  ∀ (he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t) (h : a ∈ s₁),
    ∃ (a' : Multiset α × Multiset α),
      GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = (s₁ + s₂ + t).erase a
⊢ ∃ (a' : Multiset α × Multiset α), GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = s
have inr : ∀ (he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t) (h : a ∈ s₂ + t),
  ∃ (a' : Multiset α × Multiset α),
    GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = (s₁ + s₂ + t).erase a
Tactic: 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]
Cleared hypotheses: s, he
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
p : α → Prop
h : ∀ {a' a : α}, r a' a → p a → p a'
s' s : Multiset α
⊢ CutExpand r s' s → (∀ a ∈ s, p a) → ∀ a ∈ s', p a
have rw : (∃ (t : Multiset α) (a : α), (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t) → (∀ a ∈ s, p a) → ∀ a ∈ s', p a
Tactic: rw [cutExpand_iff]
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
p : α → Prop
h : ∀ {a' a : α}, r a' a → p a → p a'
s t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
ha : a ∈ s
hsp : ∀ a ∈ s, p a
a' : α
h' : a' ∈ s.erase a + t
⊢ p a'
have inl : ∀ (h' : a' ∈ s.erase a), p a'
Tactic: obtain (h' | h') := mem_add.1 h'
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
p : α → Prop
h : ∀ {a' a : α}, r a' a → p a → p a'
s t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
ha : a ∈ s
hsp : ∀ a ∈ s, p a
a' : α
h' : a' ∈ s.erase a + t
inl : ∀ (h' : a' ∈ s.erase a), p a'
⊢ p a'
have inr : ∀ (h' : a' ∈ t), p a'
Tactic: obtain (h' | h') := mem_add.1 h'
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
p : α → Prop
h : ∀ {a' a : α}, r a' a → p a → p a'
s' s : Multiset α
⊢ CutExpand r s' s → (∀ a ∈ s, p a) → ∀ a ∈ s', p a
have rw : (∃ (t : Multiset α) (a : α), (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t) → (∀ a ∈ s, p a) → ∀ a ∈ s', p a
Tactic: classical
  rw [cutExpand_iff]
  rintro ⟨t, a, hr, ha, rfl⟩ hsp a' h'
  obtain (h' | h') := mem_add.1 h'
  exacts [hsp a' (mem_of_mem_erase h'), h (hr a' h') (hsp a ha)]
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
p : α → Prop
h : ∀ {a' a : α}, r a' a → p a → p a'
s' s : Multiset α
rw rw₁ rw₂ :
  (∃ (t : Multiset α) (a : α), (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t) → (∀ a ∈ s, p a) → ∀ a ∈ s', p a
⊢ CutExpand r s' s → (∀ a ∈ s, p a) → ∀ a ∈ s', p a
have rw₃ : ∀ (t : Multiset α) (a : α) (hr : ∀ a' ∈ t, r a' a) (ha : a ∈ s) (hsp : ∀ a ∈ s, p a) (a' : α) (h' : a' ∈ s.erase a + t),
  p a'
Tactic: classical
  rw [cutExpand_iff]
  rintro ⟨t, a, hr, ha, rfl⟩ hsp a' h'
  obtain (h' | h') := mem_add.1 h'
  exacts [hsp a' (mem_of_mem_erase h'), h (hr a' h') (hsp a ha)]
Cleared hypotheses: s'
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
p : α → Prop
h : ∀ {a' a : α}, r a' a → p a → p a'
s' s : Multiset α
rw rw₁ rw₂ :
  (∃ (t : Multiset α) (a : α), (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t) → (∀ a ∈ s, p a) → ∀ a ∈ s', p a
rw₃ :
  ∀ (t : Multiset α) (a : α) (hr : ∀ a' ∈ t, r a' a) (ha : a ∈ s) (hsp : ∀ a ∈ s, p a) (a' : α)
    (h' : a' ∈ s.erase a + t), p a'
⊢ CutExpand r s' s → (∀ a ∈ s, p a) → ∀ a ∈ s', p a
have inl : ∀ (t : Multiset α) (a : α) (hr : ∀ a' ∈ t, r a' a) (ha : a ∈ s) (hsp : ∀ a ∈ s, p a) (a' : α) (h' : a' ∈ s.erase a + t)
  (h' : a' ∈ s.erase a), p a'
Tactic: classical
  rw [cutExpand_iff]
  rintro ⟨t, a, hr, ha, rfl⟩ hsp a' h'
  obtain (h' | h') := mem_add.1 h'
  exacts [hsp a' (mem_of_mem_erase h'), h (hr a' h') (hsp a ha)]
Cleared hypotheses: s'
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
p : α → Prop
h : ∀ {a' a : α}, r a' a → p a → p a'
s' s : Multiset α
rw rw₁ rw₂ :
  (∃ (t : Multiset α) (a : α), (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t) → (∀ a ∈ s, p a) → ∀ a ∈ s', p a
rw₃ :
  ∀ (t : Multiset α) (a : α) (hr : ∀ a' ∈ t, r a' a) (ha : a ∈ s) (hsp : ∀ a ∈ s, p a) (a' : α)
    (h' : a' ∈ s.erase a + t), p a'
inl :
  ∀ (t : Multiset α) (a : α) (hr : ∀ a' ∈ t, r a' a) (ha : a ∈ s) (hsp : ∀ a ∈ s, p a) (a' : α)
    (h' : a' ∈ s.erase a + t) (h' : a' ∈ s.erase a), p a'
⊢ CutExpand r s' s → (∀ a ∈ s, p a) → ∀ a ∈ s', p a
have inr : ∀ (t : Multiset α) (a : α) (hr : ∀ a' ∈ t, r a' a) (ha : a ∈ s) (hsp : ∀ a ∈ s, p a) (a' : α) (h' : a' ∈ s.erase a + t)
  (h' : a' ∈ t), p a'
Tactic: classical
  rw [cutExpand_iff]
  rintro ⟨t, a, hr, ha, rfl⟩ hsp a' h'
  obtain (h' | h') := mem_add.1 h'
  exacts [hsp a' (mem_of_mem_erase h'), h (hr a' h') (hsp a ha)]
Cleared hypotheses: s'
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : Type u_1
r : α → α → Prop
a a₁ a₂ : α
h₁ : r a₁ a
h₂ : r a₂ a
⊢ ∀ (x' : α), Membership.mem (γ := Multiset α) {a₁, a₂} x' → r x' a
have simp : r a₁ a ∧ r a₂ a
Tactic: simp only [insert_eq_cons, mem_cons, mem_singleton, forall_eq_or_imp, forall_eq]
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
a : α
s : Multiset α
ihs : ∀ (hs : ∀ a ∈ s, Acc (CutExpand r) {a}), Acc (CutExpand r) s
hs : ∀ a_1 ∈ a ::ₘ s, Acc (CutExpand r) {a_1}
⊢ Acc (CutExpand r) (a ::ₘ s)
have cons : Acc (CutExpand r) ({a} + s)
Tactic: rw [← s.singleton_add a]
-- Lean 4 proof step from Mathlib.Logic.Hydra (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
a : α
s : Multiset α
ihs : ∀ (hs : ∀ a ∈ s, Acc (CutExpand r) {a}), Acc (CutExpand r) s
hs : ∀ a_1 ∈ a ::ₘ s, Acc (CutExpand r) {a_1}
⊢ Acc (CutExpand r) ({a} + s)
have hs₁ : Acc (CutExpand r) {a} ∧ ∀ x ∈ s, Acc (CutExpand r) {x}
Tactic: rw [forall_mem_cons] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
s : Multiset α
hs : ∀ a ∈ s, Acc (CutExpand r) {a}
⊢ Acc (CutExpand r) s
have empty : ∀ (hs : ∀ (a : α), Membership.mem (γ := Multiset α) 0 a → Acc (CutExpand r) {a}), Acc (CutExpand r) 0
Tactic: induction s using Multiset.induction with
  | empty => exact Acc.intro 0 fun s h ↦ (not_cutExpand_zero s h).elim
  | cons a s ihs =>
    rw [← s.singleton_add a]
    rw [forall_mem_cons] at hs
    exact (hs.1.prod_gameAdd <| ihs fun a ha ↦ hs.2 a ha).of_fibration _ (cutExpand_fibration r)
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
s : Multiset α
hs : ∀ a ∈ s, Acc (CutExpand r) {a}
empty : ∀ (hs : ∀ (a : α), Membership.mem (γ := Multiset α) 0 a → Acc (CutExpand r) {a}), Acc (CutExpand r) 0
⊢ Acc (CutExpand r) s
have cons : ∀ (a : α) (s : Multiset α) (ihs : ∀ (hs : ∀ a ∈ s, Acc (CutExpand r) {a}), Acc (CutExpand r) s)
  (hs : ∀ a_1 ∈ a ::ₘ s, Acc (CutExpand r) {a_1}), Acc (CutExpand r) (a ::ₘ s)
Tactic: induction s using Multiset.induction with
  | empty => exact Acc.intro 0 fun s h ↦ (not_cutExpand_zero s h).elim
  | cons a s ihs =>
    rw [← s.singleton_add a]
    rw [forall_mem_cons] at hs
    exact (hs.1.prod_gameAdd <| ihs fun a ha ↦ hs.2 a ha).of_fibration _ (cutExpand_fibration r)
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
a : α
hacc : Acc r a
⊢ Acc (CutExpand r) {a}
have intro : ∀ (a : α) (h : ∀ (y : α), r y a → Acc r y) (ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}), Acc (CutExpand r) {a}
Tactic: induction hacc with | _ a h ih
Cleared hypotheses: hacc
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
a_1 a : α
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
⊢ Acc (CutExpand r) {a}
have intro : ∀ (s : Multiset α), CutExpand r s {a} → Acc (CutExpand r) s
Tactic: refine Acc.intro _ fun s ↦ ?_
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
a_1 a : α
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
s : Multiset α
⊢ CutExpand r s {a} → Acc (CutExpand r) s
have intro : (∃ (t : Multiset α) (a_2 : α), (∀ a' ∈ t, r a' a_2) ∧ a_2 = a ∧ s = erase {a} a_2 + t) → Acc (CutExpand r) s
Tactic: simp only [cutExpand_iff, mem_singleton]
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
a_1 : α
t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
⊢ Acc (CutExpand r) (erase {a} a + t)
have intro : ∀ a' ∈ erase {a} a + t, Acc (CutExpand r) {a'}
Tactic: refine acc_of_singleton fun a' ↦ ?_
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
a_1 : α
t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
a' : α
⊢ a' ∈ erase {a} a + t → Acc (CutExpand r) {a'}
have intro : a' ∈ t → Acc (CutExpand r) {a'}
Tactic: rw [erase_singleton, zero_add]
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
a_1 a : α
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
s : Multiset α
⊢ CutExpand r s {a} → Acc (CutExpand r) s
have intro : (∃ (t : Multiset α) (a_2 : α), (∀ a' ∈ t, r a' a_2) ∧ a_2 = a ∧ s = erase {a} a_2 + t) → Acc (CutExpand r) s
Tactic: classical
  simp only [cutExpand_iff, mem_singleton]
  rintro ⟨t, a, hr, rfl, rfl⟩
  refine acc_of_singleton fun a' ↦ ?_
  rw [erase_singleton, zero_add]
  exact ih a' ∘ hr a'
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
a_1 a : α
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
s : Multiset α
intro : (∃ (t : Multiset α) (a_2 : α), (∀ a' ∈ t, r a' a_2) ∧ a_2 = a ∧ s = erase {a} a_2 + t) → Acc (CutExpand r) s
⊢ CutExpand r s {a} → Acc (CutExpand r) s
have intro₁ : ∀ (t : Multiset α) (a : α) (hr : ∀ a' ∈ t, r a' a) (h : ∀ (y : α), r y a → Acc r y)
  (ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}), Acc (CutExpand r) (erase {a} a + t)
Tactic: classical
  simp only [cutExpand_iff, mem_singleton]
  rintro ⟨t, a, hr, rfl, rfl⟩
  refine acc_of_singleton fun a' ↦ ?_
  rw [erase_singleton, zero_add]
  exact ih a' ∘ hr a'
Cleared hypotheses: a, h, ih, s
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
a_1 a : α
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
s : Multiset α
intro : (∃ (t : Multiset α) (a_2 : α), (∀ a' ∈ t, r a' a_2) ∧ a_2 = a ∧ s = erase {a} a_2 + t) → Acc (CutExpand r) s
intro₁ :
  ∀ (t : Multiset α) (a : α) (hr : ∀ a' ∈ t, r a' a) (h : ∀ (y : α), r y a → Acc r y)
    (ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}), Acc (CutExpand r) (erase {a} a + t)
⊢ CutExpand r s {a} → Acc (CutExpand r) s
have intro₂ : ∀ (t : Multiset α) (a : α) (hr : ∀ a' ∈ t, r a' a) (h : ∀ (y : α), r y a → Acc r y)
  (ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}), ∀ a' ∈ erase {a} a + t, Acc (CutExpand r) {a'}
Tactic: classical
  simp only [cutExpand_iff, mem_singleton]
  rintro ⟨t, a, hr, rfl, rfl⟩
  refine acc_of_singleton fun a' ↦ ?_
  rw [erase_singleton, zero_add]
  exact ih a' ∘ hr a'
Cleared hypotheses: a, h, ih, s
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
a_1 a : α
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
s : Multiset α
intro : (∃ (t : Multiset α) (a_2 : α), (∀ a' ∈ t, r a' a_2) ∧ a_2 = a ∧ s = erase {a} a_2 + t) → Acc (CutExpand r) s
intro₁ :
  ∀ (t : Multiset α) (a : α) (hr : ∀ a' ∈ t, r a' a) (h : ∀ (y : α), r y a → Acc r y)
    (ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}), Acc (CutExpand r) (erase {a} a + t)
intro₂ :
  ∀ (t : Multiset α) (a : α) (hr : ∀ a' ∈ t, r a' a) (h : ∀ (y : α), r y a → Acc r y)
    (ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}), ∀ a' ∈ erase {a} a + t, Acc (CutExpand r) {a'}
⊢ CutExpand r s {a} → Acc (CutExpand r) s
have intro₃ : ∀ (t : Multiset α) (a : α) (hr : ∀ a' ∈ t, r a' a) (h : ∀ (y : α), r y a → Acc r y)
  (ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}), ∀ a' ∈ t, Acc (CutExpand r) {a'}
Tactic: classical
  simp only [cutExpand_iff, mem_singleton]
  rintro ⟨t, a, hr, rfl, rfl⟩
  refine acc_of_singleton fun a' ↦ ?_
  rw [erase_singleton, zero_add]
  exact ih a' ∘ hr a'
Cleared hypotheses: a, h, ih, s