awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
K m n : Type u
inst : CommRing K
inst_1 : Fintype n
inst_2 : DecidableEq n
w : m → K
v : n → K
h : Nontrivial K
refine : Module.rank K (Fin 1 → K) = 1
⊢ LinearMap.rank (K := K) (V := Fin 1 → K) (V' := m → K)
      ((toLin' : (a : Matrix m (Fin 1) K) → (Fin 1 → K) →ₗ[K] m → K) (replicateCol (Fin 1) w)) ≤
    1

Tactic:
refine (LinearMap.rank_le_domain _).trans_eq ?_

Premises used: LinearMap.rank_le_domain, LE.le.trans_eq
-- Module: Mathlib.LinearAlgebra.Matrix.Rank
Goal:
K m n : Type u
inst : CommRing K
inst_1 : Fintype n
inst_2 : DecidableEq n
w : m → K
v : n → K
h : Nontrivial K
rw : Eq.{u + 2} (α := Cardinal.{u}) (↑(Fintype.card (Fin 1)) : Cardinal.{u}) 1
rw₁ : Eq.{u + 2} (α := Cardinal.{u}) (↑1 : Cardinal.{u}) 1
rw₂ rw₃ : Eq.{u + 2} (α := Cardinal.{u}) 1 1
⊢ Module.rank K (Fin 1 → K) = 1

Tactic:
rw [rank_fun', Fintype.card_ofSubsingleton, Nat.cast_one]

Premises used: Fintype.card_ofSubsingleton, rank_fun', Nat.cast_one
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableEq α
inst_1 : Std.Irrefl r
s t u : Multiset α
a : α
hr : ∀ a' ∈ u, r a' a
he : s + {a} = t + u
⊢ ∀ (a' : α) (h₂ : ¬r a' a), a' ∉ u

Tactic:
replace hr := fun a' ↦ mt (hr a')
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableEq α
inst_1 : Std.Irrefl r
s t u : Multiset α
a : α
he : s + {a} = t + u
hr : ∀ (a' : α) (h₂ : ¬r a' a), a' ∉ u
⊢ InvImage (β := α →₀ ℕ) (Finsupp.Lex (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2) fun (x1 x2 : ℕ) ↦ x1 < x2)
    (⇑toFinsupp : (a : Multiset α) → α →₀ ℕ) s t

Tactic:
⟨a, fun b h ↦ ?_, ?_⟩

Premises used: InvImage, Pi.Lex, And.intro, Exists.intro, Finsupp.Lex
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableEq α
inst_1 : Std.Irrefl r
s t u : Multiset α
a : α
he : s + {a} = t + u
hr : ∀ (a' : α) (h₂ : ¬r a' a), a' ∉ u
refine_1 :
  ∀ (b : α) (h : (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2) b a),
    Eq (α := (@fun {i : α} ↦ ℕ) b) ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) s : α →₀ ℕ) : (a : α) → ℕ) b : ℕ)
      ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) t : α →₀ ℕ) : (a : α) → ℕ) b : ℕ)
refine_2 :
  (@fun {i : α} (x1 x2 : ℕ) ↦ x1 < x2) a ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) s : α →₀ ℕ) : (a : α) → ℕ) a)
    ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) t : α →₀ ℕ) : (a : α) → ℕ) a)
⊢ InvImage (β := α →₀ ℕ) (Finsupp.Lex (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2) fun (x1 x2 : ℕ) ↦ x1 < x2)
    (⇑toFinsupp : (a : Multiset α) → α →₀ ℕ) s t

Tactic:
refine ⟨a, fun b h ↦ ?_, ?_⟩
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableEq α
inst_1 : Std.Irrefl r
s t u : Multiset α
a : α
he : s + {a} = t + u
hr : ∀ (a' : α) (h₂ : ¬r a' a), a' ∉ u
b : α
h : (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2) b a
refine_1 : count b s = count b t
⊢ Eq (α := (@fun {i : α} ↦ ℕ) b) ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) s : α →₀ ℕ) : (a : α) → ℕ) b : ℕ)
    ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) t : α →₀ ℕ) : (a : α) → ℕ) b : ℕ)

Tactic:
simp_rw [toFinsupp_apply]

Premises used: Multiset.toFinsupp_apply
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableEq α
inst_1 : Std.Irrefl r
s t u : Multiset α
a : α
he : s + {a} = t + u
hr : ∀ (a' : α) (h₂ : ¬r a' a), a' ∉ u
refine_2 : count a s < count a t
⊢ (@fun {i : α} (x1 x2 : ℕ) ↦ x1 < x2) a ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) s : α →₀ ℕ) : (a : α) → ℕ) a)
    ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) t : α →₀ ℕ) : (a : α) → ℕ) a)

Tactic:
simp_rw [toFinsupp_apply]

Premises used: Multiset.toFinsupp_apply
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableEq α
inst_1 : Std.Irrefl r
s t u : Multiset α
a : α
he : s + {a} = t + u
hr : ∀ (a' : α) (h₂ : ¬r a' a), a' ∉ u
b : α
h : (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2) b a
⊢ count b (s + {a}) = count b (t + u)

Tactic:
apply_fun count b at he

Premises used: Multiset.count
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableEq α
inst_1 : Std.Irrefl r
s t u : Multiset α
a : α
hr : ∀ (a' : α) (h₂ : ¬r a' a), a' ∉ u
b : α
h : (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2) b a
he : count b (s + {a}) = count b (t + u)
⊢ count b s = count b t

Tactic:
simpa only [count_add, count_singleton, if_neg h.2, add_zero, count_eq_zero.2 (hr b h.1)]
      using he

Premises used: Iff.mpr, And.right, And.left, Multiset.count_add, Multiset.count_singleton, Multiset.count_eq_zero, add_zero, if_neg
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableEq α
inst_1 : Std.Irrefl r
s t u : Multiset α
a : α
he : s + {a} = t + u
hr : ∀ (a' : α) (h₂ : ¬r a' a), a' ∉ u
⊢ count a (s + {a}) = count a (t + u)

Tactic:
apply_fun count a at he

Premises used: Multiset.count
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableEq α
inst_1 : Std.Irrefl r
s t u : Multiset α
a : α
hr : ∀ (a' : α) (h₂ : ¬r a' a), a' ∉ u
he : count a (s + {a}) = count a (t + u)
⊢ count a s + 1 = count a t

Tactic:
simp only [count_add, count_singleton_self, count_eq_zero.2 (hr _ (irrefl_of r a)),
      add_zero] at he

Premises used: Iff.mpr, irrefl_of, Multiset.count_singleton_self, Multiset.count_add, Multiset.count_eq_zero, add_zero
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableEq α
inst_1 : Std.Irrefl r
s t u : Multiset α
a : α
hr : ∀ (a' : α) (h₂ : ¬r a' a), a' ∉ u
he : count a s + 1 = count a t
⊢ count a s < count a t

Tactic:
he ▸ Nat.lt_succ_self _

Premises used: Eq.rec, Nat.lt_succ_self
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableEq α
inst_1 : Std.Irrefl r
s t u : Multiset α
a : α
hr : ∀ (a' : α) (h₂ : ¬r a' a), a' ∉ u
he : count a s + 1 = count a t
⊢ count a s < count a t

Tactic:
exact he ▸ Nat.lt_succ_self _
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableEq α
inst_1 : Std.Irrefl r
s t u : Multiset α
a : α
he : s + {a} = t + u
hr : ∀ (a' : α) (h₂ : ¬r a' a), a' ∉ u
refine_1 :
  ∀ (b : α) (h : (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2) b a),
    Eq (α := (@fun {i : α} ↦ ℕ) b) ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) s : α →₀ ℕ) : (a : α) → ℕ) b : ℕ)
      ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) t : α →₀ ℕ) : (a : α) → ℕ) b : ℕ)
refine_2 :
  (@fun {i : α} (x1 x2 : ℕ) ↦ x1 < x2) a ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) s : α →₀ ℕ) : (a : α) → ℕ) a)
    ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) t : α →₀ ℕ) : (a : α) → ℕ) a)
refine_1₁ :
  ∀ (b : α) (h : (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2) b a),
    Eq (α := (@fun {i : α} ↦ ℕ) b) ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) s : α →₀ ℕ) : (a : α) → ℕ) b : ℕ)
      ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) t : α →₀ ℕ) : (a : α) → ℕ) b : ℕ)
refine_2₁ :
  (@fun {i : α} (x1 x2 : ℕ) ↦ x1 < x2) a ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) s : α →₀ ℕ) : (a : α) → ℕ) a)
    ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) t : α →₀ ℕ) : (a : α) → ℕ) a)
refine_1₂ :
  ∀ (b : α) (h : (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2) b a),
    Eq (α := (@fun {i : α} ↦ ℕ) b) ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) s : α →₀ ℕ) : (a : α) → ℕ) b : ℕ)
      ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) t : α →₀ ℕ) : (a : α) → ℕ) b : ℕ)
refine_2₂ :
  (@fun {i : α} (x1 x2 : ℕ) ↦ x1 < x2) a ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) s : α →₀ ℕ) : (a : α) → ℕ) a)
    ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) t : α →₀ ℕ) : (a : α) → ℕ) a)
refine_1₃ :
  ∀ (b : α) (h : (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2) b a),
    Eq (α := (@fun {i : α} ↦ ℕ) b) ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) s : α →₀ ℕ) : (a : α) → ℕ) b : ℕ)
      ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) t : α →₀ ℕ) : (a : α) → ℕ) b : ℕ)
refine_2₃ :
  (@fun {i : α} (x1 x2 : ℕ) ↦ x1 < x2) a ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) s : α →₀ ℕ) : (a : α) → ℕ) a)
    ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) t : α →₀ ℕ) : (a : α) → ℕ) a)
refine_1₄ : ∀ (b : α) (h : (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2) b a), count b s = count b t
refine_2₄ refine_2₅ : count a s < count a t
⊢ InvImage (β := α →₀ ℕ) (Finsupp.Lex (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2) fun (x1 x2 : ℕ) ↦ x1 < x2)
    (⇑toFinsupp : (a : Multiset α) → α →₀ ℕ) s t

Tactic:
classical
  refine ⟨a, fun b h ↦ ?_, ?_⟩ <;> simp_rw [toFinsupp_apply]
  · apply_fun count b at he
    simpa only [count_add, count_singleton, if_neg h.2, add_zero, count_eq_zero.2 (hr b h.1)]
      using he
  · apply_fun count a at he
    simp only [count_add, count_singleton_self, count_eq_zero.2 (hr _ (irrefl_of r a)),
      add_zero] at he
    exact he ▸ Nat.lt_succ_self _

Premises used: Iff.mpr, irrefl_of, Multiset.count_singleton_self, Multiset.count, Multiset.toFinsupp_apply, Multiset.count_add, Multiset.count_singleton, Multiset.count_eq_zero, add_zero
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
s : Multiset α
x : α
h : ∀ x' ∈ s, r x' x
⊢ CutExpand r s {x}

Tactic:
⟨s, x, h, add_comm s _⟩

Premises used: Relation.CutExpand, add_comm, And.intro, Exists.intro
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
x' x : α
h_1 : r x' x
a : α
h : Membership.mem (γ := Multiset α) {x'} a
rwa rwa₁ rwa₂ rwa₃ : r x' x
⊢ r a x

Tactic:
rwa [mem_singleton.1 h]

Premises used: Multiset.mem_singleton, Iff.mp
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
t u s x : Multiset α
x_1 : α
rw : s + (t + {x_1}) = s + u + x ↔ t + {x_1} = u + x
rw₁ : s + (t + {x_1}) = s + (u + x) ↔ t + {x_1} = u + x
rw₂ rw₃ : t + {x_1} = u + x ↔ t + {x_1} = u + x
⊢ s + t + {x_1} = s + u + x ↔ t + {x_1} = u + x

Tactic:
rw [add_assoc, add_assoc, add_left_cancel_iff]

Premises used: add_assoc, add_left_cancel_iff
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
s' s t : Multiset α
⊢ CutExpand r (t + s') (t + s) ↔ CutExpand r s' s

Tactic:
cutExpand_add_left t

Premises used: Relation.cutExpand_add_left
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
s' s t : Multiset α
h : s' + t = t + s'
h₁ : s + t = t + s
⊢ CutExpand r (s' + t) (s + t) ↔ CutExpand r s' s

Tactic:
convert! cutExpand_add_left t using 2

Premises used: Relation.cutExpand_add_left
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
s' s t : Multiset α
⊢ s' + t = t + s'

Tactic:
apply add_comm

Premises used: add_comm
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
s' s t : Multiset α
⊢ s + t = t + s

Tactic:
apply add_comm

Premises used: add_comm
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
a' a : α
s : Multiset α
h : r a' a
⊢ CutExpand r (s + {a'}) (s + {a})

Tactic:
(cutExpand_add_left s).2 <| cutExpand_singleton_singleton h

Premises used: Iff.mpr, Relation.cutExpand_add_left, Relation.cutExpand_singleton_singleton
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
a' a : α
h : r a' a
s : Multiset α
⊢ CutExpand r ({a'} + s) ({a} + s)

Tactic:
(cutExpand_add_right s).2 <| cutExpand_singleton_singleton h

Premises used: Iff.mpr, Relation.cutExpand_singleton_singleton, Relation.cutExpand_add_right
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableEq α
inst_1 : Std.Irrefl r
s' s : Multiset α
simp_rw :
  (∃ (t : Multiset α) (a : α), (∀ a' ∈ t, r a' a) ∧ a ∈ s + t ∧ s' = (s + t).erase a) ↔
    ∃ (t : Multiset α) (a : α), (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t
⊢ CutExpand r s' s ↔ ∃ (t : Multiset α) (a : α), (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t

Tactic:
simp_rw [CutExpand, add_singleton_eq_iff]

Premises used: Relation.CutExpand, Multiset.add_singleton_eq_iff
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableEq α
inst_1 : Std.Irrefl r
s' s : Multiset α
⊢ (∃ (t : Multiset α) (a : α), (∀ a' ∈ t, r a' a) ∧ a ∈ s + t ∧ s' = (s + t).erase a) ↔
    ∃ (t : Multiset α) (a : α), (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t

Tactic:
exists₂_congr fun t a ↦ ⟨?_, ?_⟩

Premises used: exists₂_congr, Iff.intro
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableEq α
inst_1 : Std.Irrefl r
s' s : Multiset α
refine_1 :
  ∀ (t : Multiset α) (a : α),
    (∀ a' ∈ t, r a' a) ∧ a ∈ s + t ∧ s' = (s + t).erase a → (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t
refine_2 :
  ∀ (t : Multiset α) (a : α),
    (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t → (∀ a' ∈ t, r a' a) ∧ a ∈ s + t ∧ s' = (s + t).erase a
⊢ (∃ (t : Multiset α) (a : α), (∀ a' ∈ t, r a' a) ∧ a ∈ s + t ∧ s' = (s + t).erase a) ↔
    ∃ (t : Multiset α) (a : α), (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t

Tactic:
refine exists₂_congr fun t a ↦ ⟨?_, ?_⟩

Premises used: exists₂_congr, Iff.intro
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableEq α
inst_1 : Std.Irrefl r
s t : Multiset α
a : α
ht : ∀ a' ∈ t, r a' a
ha : a ∈ s + t
refine_1 : ∀ (h : a ∈ s), (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ (s + t).erase a = s.erase a + t
refine_1₁ : ∀ (h : a ∈ t), (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ (s + t).erase a = s.erase a + t
⊢ (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ (s + t).erase a = s.erase a + t

Tactic:
obtain h | h := mem_add.1 ha

Premises used: Multiset.mem_add, Iff.mp
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableEq α
inst_1 : Std.Irrefl r
s t : Multiset α
a : α
ht : ∀ a' ∈ t, r a' a
ha : a ∈ s + t
h : a ∈ s
⊢ (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ (s + t).erase a = s.erase a + t

Tactic:
⟨ht, h, erase_add_left_pos t h⟩

Premises used: Multiset.erase_add_left_pos, And.intro
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableEq α
inst_1 : Std.Irrefl r
s t : Multiset α
a : α
ht : ∀ a' ∈ t, r a' a
ha : a ∈ s + t
h : a ∈ t
⊢ (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ (s + t).erase a = s.erase a + t

Tactic:
(@irrefl α r _ a (ht a h)).elim

Premises used: irrefl, False.elim
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableEq α
inst_1 : Std.Irrefl r
s t : Multiset α
a : α
ht : ∀ a' ∈ t, r a' a
ha : a ∈ s + t
h : a ∈ s
⊢ (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ (s + t).erase a = s.erase a + t

Tactic:
exacts [⟨ht, h, erase_add_left_pos t h⟩, (@irrefl α r _ a (ht a h)).elim]
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableEq α
inst_1 : Std.Irrefl r
s t : Multiset α
a : α
ht : ∀ a' ∈ t, r a' a
h : a ∈ s
⊢ (∀ a' ∈ t, r a' a) ∧ a ∈ s + t ∧ s.erase a + t = (s + t).erase a

Tactic:
⟨ht, mem_add.2 (Or.inl h), (erase_add_left_pos t h).symm⟩

Premises used: Iff.mpr, Multiset.mem_add, Multiset.erase_add_left_pos, And.intro, Or.inl, Eq.symm
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableEq α
inst_1 : Std.Irrefl r
s t : Multiset α
a : α
ht : ∀ a' ∈ t, r a' a
h : a ∈ s
⊢ (∀ a' ∈ t, r a' a) ∧ a ∈ s + t ∧ s.erase a + t = (s + t).erase a

Tactic:
exact ⟨ht, mem_add.2 (Or.inl h), (erase_add_left_pos t h).symm⟩
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
s : Multiset α
rw : ¬∃ (t : Multiset α) (a : α), (∀ a' ∈ t, r a' a) ∧ Membership.mem (γ := Multiset α) 0 a ∧ s = erase 0 a + t
⊢ ¬CutExpand r s 0

Tactic:
rw [cutExpand_iff]

Premises used: Relation.cutExpand_iff
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
s : Multiset α
rw rw₁ rw₂ : ¬∃ (t : Multiset α) (a : α), (∀ a' ∈ t, r a' a) ∧ Membership.mem (γ := Multiset α) 0 a ∧ s = erase 0 a + t
⊢ ¬CutExpand r s 0

Tactic:
classical
  rw [cutExpand_iff]
  rintro ⟨_, _, _, ⟨⟩, _⟩

Premises used: Relation.cutExpand_iff
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
x : α
⊢ CutExpand r 0 {x}

Tactic:
⟨0, x, nofun, add_comm 0 _⟩

Premises used: Relation.CutExpand, _private.0.Relation.cutExpand_zero.match_1, add_comm, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Logic.Hydra
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

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

Premises used: Iff.mp, Multiset.add_singleton_eq_iff, rfl
-- Module: Mathlib.Logic.Hydra
Goal:
α : 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 ∈ s₁ ∨ a ∈ s₂ + t

Tactic:
rw [add_assoc, mem_add] at ha

Premises used: add_assoc, Multiset.mem_add
-- Module: Mathlib.Logic.Hydra
Goal:
α : 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
ha₁ : a ∈ s₁ ∨ a ∈ s₂ + t
⊢ (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t

Tactic:
rw [add_assoc, mem_add] at ha

Premises used: add_assoc, Multiset.mem_add
-- Module: Mathlib.Logic.Hydra
Goal:
α : 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
inl :
  ∀ (h : a ∈ s₁),
    ∃ (a' : Multiset α × Multiset α),
      GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = (s₁ + s₂ + t).erase a
inr :
  ∀ (h : a ∈ 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₁ + s₂ + t).erase a

Tactic:
obtain h | h := ha
-- Module: Mathlib.Logic.Hydra
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₁
⊢ ∃ (a' : Multiset α × Multiset α),
    GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = (s₁ + s₂ + t).erase a

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

Premises used: Prod.mk, HAdd.hAdd, And.intro, Multiset.erase, Exists.intro, Prod.GameAdd.fst
-- Module: Mathlib.Logic.Hydra
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
inl₁ : (s₁.erase a + t, s₂).1 + (s₁.erase a + t, s₂).2 = (s₁ + s₂ + t).erase a
⊢ ∃ (a' : Multiset α × Multiset α),
    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, ?_⟩, ?_⟩
-- Module: Mathlib.Logic.Hydra
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
inl₃ inl₄ : s₁ + t = s₁ + t
⊢ s₁.erase a + t + {a} = s₁ + t

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

Premises used: Multiset.singleton_add, add_assoc, add_comm, Multiset.cons_erase
-- Module: Mathlib.Logic.Hydra
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)
inl₃ 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

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

Premises used: add_assoc, add_right_comm, Multiset.erase_add_left_pos
-- Module: Mathlib.Logic.Hydra
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

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

Premises used: Prod.mk, Prod.GameAdd.snd, HAdd.hAdd, And.intro, Multiset.erase, Exists.intro
-- Module: Mathlib.Logic.Hydra
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
inr₁ : (s₁, (s₂ + t).erase a).1 + (s₁, (s₂ + t).erase a).2 = (s₁ + s₂ + t).erase a
⊢ ∃ (a' : Multiset α × Multiset α),
    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, ?_⟩, ?_⟩
-- Module: Mathlib.Logic.Hydra
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
inr₂ inr₃ : s₂ + t = s₂ + t
⊢ (s₂ + t).erase a + {a} = s₂ + t

Tactic:
rw [add_comm, singleton_add, cons_erase h]

Premises used: Multiset.singleton_add, add_comm, Multiset.cons_erase
-- Module: Mathlib.Logic.Hydra
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
inr₁ 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

Tactic:
rw [add_assoc, erase_add_right_pos _ h]

Premises used: add_assoc, Multiset.erase_add_right_pos
-- Module: Mathlib.Logic.Hydra
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
inr 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
⊢ ∃ (a' : Multiset α × Multiset α), GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = s

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]

Premises used: Multiset.singleton_add, add_assoc, Multiset.mem_add, add_right_comm, add_comm, Iff.mp, Multiset.add_singleton_eq_iff, rfl
-- Module: Mathlib.Logic.Hydra
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 : (∃ (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

Tactic:
rw [cutExpand_iff]

Premises used: Relation.cutExpand_iff
-- Module: Mathlib.Logic.Hydra
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'
inr : ∀ (h' : a' ∈ t), p a'
⊢ p a'

Tactic:
obtain (h' | h') := mem_add.1 h'

Premises used: Multiset.mem_add, Iff.mp
-- Module: Mathlib.Logic.Hydra
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'_1 : a' ∈ s.erase a + t
h' : a' ∈ s.erase a
⊢ p a'

Tactic:
hsp a' (mem_of_mem_erase h')

Premises used: Multiset.mem_of_mem_erase