awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
Goal:
l : Type ul
m : Type um
n : Type un
R : Type uR
inst : Fintype n
inst_1 : Field R
inst_2 : Finite l
inst_3 : Fintype m
A : Matrix l m R
B : Matrix m n R
hAB : A * B = 0
let let₁ let₂ let₃ let₄ : A.rank + B.rank ≤ Fintype.card m
let₅ :
  let el : Basis l R (l → R) := Pi.basisFun R l;
  let em : Basis m R (m → R) := Pi.basisFun R m;
  let en : Basis n R (n → R) := Pi.basisFun R n;
  finrank R
      ↥(LinearMap.range (R := R) (M := n → R) (τ₁₂ := RingHom.id R)
          ((toLin en em : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) B)) ≤
    finrank R
      ↥(LinearMap.ker (R₂ := R) (M₂ := l → R) (τ₁₂ := RingHom.id R)
          ((toLin em el : (a : Matrix l m R) → (m → R) →ₗ[R] l → R) A))
⊢ A.rank + B.rank ≤ Fintype.card m
have hst : let el : Basis l R (l → R) := Pi.basisFun R l;
let em : Basis m R (m → R) := Pi.basisFun R m;
let en : Basis n R (n → R) := Pi.basisFun R n;
LE.le (α := Submodule R (m → R))
  (LinearMap.range (R := R) (M := n → R) (τ₁₂ := RingHom.id R)
    ((toLin en em : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) B))
  (LinearMap.ker (R₂ := R) (M₂ := l → R) (τ₁₂ := RingHom.id R)
    ((toLin em el : (a : Matrix l m R) → (m → R) →ₗ[R] l → R) A))
Tactic: classical
  let el : Basis l R (l → R) := Pi.basisFun R l
  let em : Basis m R (m → R) := Pi.basisFun R m
  let en : Basis n R (n → R) := Pi.basisFun R n
  rw [Matrix.rank_eq_finrank_range_toLin A el em,
      Matrix.rank_eq_finrank_range_toLin B em en,
      ← Module.finrank_fintype_fun_eq_card R,
      ← LinearMap.finrank_range_add_finrank_ker (Matrix.toLin em el A),
      add_le_add_iff_left]
  apply Submodule.finrank_mono
  rw [LinearMap.range_le_ker_iff, ← Matrix.toLin_mul, hAB, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (hypothesis)
Goal:
K m n : Type u
inst : CommRing K
inst_1 : Fintype n
inst_2 : DecidableEq n
w : m → K
v : n → K
⊢ LinearMap.rank (K := K) (V := n → K) (V' := m → K)
      ((toLin' : (a : Matrix m n K) → (n → K) →ₗ[K] m → K) (vecMulVec w v)) ≤
    1
have a : Nontrivial K
Tactic: nontriviality K
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ LinearMap.rank (K := K) (V := n → K) (V' := m → K)
      ((toLin' : (a : Matrix m n K) → (n → K) →ₗ[K] m → K) (vecMulVec w v)) ≤
    1
have rw : LinearMap.rank (V := n → K) (V' := m → K)
    ((toLin' : (a : Matrix m (Fin 1) K) → (Fin 1 → K) →ₗ[K] m → K) (replicateCol (Fin 1) w) ∘ₗ
      (toLin' : (a : Matrix (Fin 1) n K) → (n → K) →ₗ[K] Fin 1 → K) (replicateRow (Fin 1) v)) ≤
  1
Tactic: rw [Matrix.vecMulVec_eq (Fin 1), Matrix.toLin'_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ LinearMap.rank (V := n → K) (V' := m → K)
      ((toLin' : (a : Matrix m (Fin 1) K) → (Fin 1 → K) →ₗ[K] m → K) (replicateCol (Fin 1) w) ∘ₗ
        (toLin' : (a : Matrix (Fin 1) n K) → (n → K) →ₗ[K] Fin 1 → K) (replicateRow (Fin 1) v)) ≤
    1
have refine : 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 le_trans (LinearMap.rank_comp_le_left _ _) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ 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
have refine : Module.rank K (Fin 1 → K) = 1
Tactic: refine (LinearMap.rank_le_domain _).trans_eq ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ Module.rank K (Fin 1 → K) = 1
have rw : Eq.{u + 2} (α := Cardinal.{u}) (↑(Fintype.card (Fin 1)) : Cardinal.{u}) 1
Tactic: rw [rank_fun', Fintype.card_ofSubsingleton, Nat.cast_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ Module.rank K (Fin 1 → K) = 1
have rw₁ : Eq.{u + 2} (α := Cardinal.{u}) (↑1 : Cardinal.{u}) 1
Tactic: rw [rank_fun', Fintype.card_ofSubsingleton, Nat.cast_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Rank (goal)
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
⊢ Module.rank K (Fin 1 → K) = 1
have rw₂ : Eq.{u + 2} (α := Cardinal.{u}) 1 1
Tactic: rw [rank_fun', Fintype.card_ofSubsingleton, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Logic.Hydra (hypothesis)
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
⊢ InvImage (β := α →₀ ℕ) (Finsupp.Lex (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2) fun (x1 x2 : ℕ) ↦ x1 < x2)
    (⇑toFinsupp : (a : Multiset α) → α →₀ ℕ) s t
have hr₁ : ∀ (a' : α) (h₂ : ¬r a' a), a' ∉ u
Tactic: replace hr := fun a' ↦ mt (hr a')
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
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
have 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 : ℕ)
Tactic: refine ⟨a, fun b h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
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 : ℕ)
⊢ InvImage (β := α →₀ ℕ) (Finsupp.Lex (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2) fun (x1 x2 : ℕ) ↦ x1 < x2)
    (⇑toFinsupp : (a : Multiset α) → α →₀ ℕ) s t
have refine_2 : (@fun {i : α} (x1 x2 : ℕ) ↦ x1 < x2) a ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) s : α →₀ ℕ) : (a : α) → ℕ) a)
  ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) t : α →₀ ℕ) : (a : α) → ℕ) a)
Tactic: refine ⟨a, fun b h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
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
⊢ Eq (α := (@fun {i : α} ↦ ℕ) b) ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) s : α →₀ ℕ) : (a : α) → ℕ) b : ℕ)
    ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) t : α →₀ ℕ) : (a : α) → ℕ) b : ℕ)
have refine_1 : count b s = count b t
Tactic: simp_rw [toFinsupp_apply]
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
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
⊢ (@fun {i : α} (x1 x2 : ℕ) ↦ x1 < x2) a ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) s : α →₀ ℕ) : (a : α) → ℕ) a)
    ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) t : α →₀ ℕ) : (a : α) → ℕ) a)
have refine_2 : count a s < count a t
Tactic: simp_rw [toFinsupp_apply]
-- Lean 4 proof step from Mathlib.Logic.Hydra (hypothesis)
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 = count b t
have he₁ : count b (s + {a}) = count b (t + u)
Tactic: apply_fun count b at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Logic.Hydra (hypothesis)
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 < count a t
have he₁ : count a (s + {a}) = count a (t + u)
Tactic: apply_fun count a at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Logic.Hydra (hypothesis)
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 < count a t
have he₁ : 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
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
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
have 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 : ℕ)
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 _
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
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 : ℕ)
⊢ InvImage (β := α →₀ ℕ) (Finsupp.Lex (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2) fun (x1 x2 : ℕ) ↦ x1 < x2)
    (⇑toFinsupp : (a : Multiset α) → α →₀ ℕ) s t
have refine_2 : (@fun {i : α} (x1 x2 : ℕ) ↦ x1 < x2) a ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) s : α →₀ ℕ) : (a : α) → ℕ) a)
  ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) t : α →₀ ℕ) : (a : α) → ℕ) a)
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 _
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
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)
⊢ InvImage (β := α →₀ ℕ) (Finsupp.Lex (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2) fun (x1 x2 : ℕ) ↦ x1 < x2)
    (⇑toFinsupp : (a : Multiset α) → α →₀ ℕ) s t
have refine_1₄ : ∀ (b : α) (h : (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2) b a), count b s = count b 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 _
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
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
⊢ InvImage (β := α →₀ ℕ) (Finsupp.Lex (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2) fun (x1 x2 : ℕ) ↦ x1 < x2)
    (⇑toFinsupp : (a : Multiset α) → α →₀ ℕ) s t
have refine_2₄ : count a s < count a 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 _
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : Type u_1
r : α → α → Prop
t u s x : Multiset α
x_1 : α
⊢ s + t + {x_1} = s + u + x ↔ t + {x_1} = u + x
have rw : s + (t + {x_1}) = s + u + x ↔ t + {x_1} = u + x
Tactic: rw [add_assoc, add_assoc, add_left_cancel_iff]
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
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
⊢ s + t + {x_1} = s + u + x ↔ t + {x_1} = u + x
have rw₁ : s + (t + {x_1}) = s + (u + x) ↔ t + {x_1} = u + x
Tactic: rw [add_assoc, add_assoc, add_left_cancel_iff]
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
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
⊢ s + t + {x_1} = s + u + x ↔ t + {x_1} = u + x
have rw₂ : t + {x_1} = u + x ↔ t + {x_1} = u + x
Tactic: rw [add_assoc, add_assoc, add_left_cancel_iff]
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : Type u_1
r : α → α → Prop
s' s t : Multiset α
⊢ CutExpand r (s' + t) (s + t) ↔ CutExpand r s' s
have h : s' + t = t + s'
Tactic: convert! cutExpand_add_left t using 2
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : Type u_1
r : α → α → Prop
s' s t : Multiset α
h : s' + t = t + s'
⊢ CutExpand r (s' + t) (s + t) ↔ CutExpand r s' s
have h₁ : s + t = t + s
Tactic: convert! cutExpand_add_left t using 2
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableEq α
inst_1 : Std.Irrefl r
s' s : Multiset α
⊢ CutExpand r s' s ↔ ∃ (t : Multiset α) (a : α), (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t
have 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
Tactic: simp_rw [CutExpand, add_singleton_eq_iff]
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
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
have 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
Tactic: refine exists₂_congr fun t a ↦ ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
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
⊢ (∃ (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
have 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
Tactic: refine exists₂_congr fun t a ↦ ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
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
⊢ (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ (s + t).erase a = s.erase a + t
have refine_1 : ∀ (h : a ∈ s), (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ (s + t).erase a = s.erase a + t
Tactic: obtain h | h := mem_add.1 ha
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
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
⊢ (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ (s + t).erase a = s.erase a + t
have refine_1₁ : ∀ (h : 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
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
s : Multiset α
⊢ ¬CutExpand r s 0
have rw : ¬∃ (t : Multiset α) (a : α), (∀ a' ∈ t, r a' a) ∧ Membership.mem (γ := Multiset α) 0 a ∧ s = erase 0 a + t
Tactic: rw [cutExpand_iff]
-- Lean 4 proof step from Mathlib.Logic.Hydra (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
s : Multiset α
⊢ ¬CutExpand r s 0
have rw : ¬∃ (t : Multiset α) (a : α), (∀ a' ∈ t, r a' a) ∧ Membership.mem (γ := Multiset α) 0 a ∧ s = erase 0 a + t
Tactic: classical
  rw [cutExpand_iff]
  rintro ⟨_, _, _, ⟨⟩, _⟩
-- 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: obtain ⟨ha, rfl⟩ := add_singleton_eq_iff.1 he
Cleared hypotheses: s, he
-- Lean 4 proof step from Mathlib.Logic.Hydra (hypothesis)
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' : Multiset α × Multiset α),
    GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = (s₁ + s₂ + t).erase a
have ha₁ : a ∈ s₁ ∨ a ∈ s₂ + t
Tactic: rw [add_assoc, mem_add] at ha
Cleared hypotheses: ha, he
-- 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
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
have inl : ∀ (h : a ∈ s₁),
  ∃ (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
Cleared hypotheses: ha
-- 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
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
⊢ ∃ (a' : Multiset α × Multiset α),
    GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = (s₁ + s₂ + t).erase a
have 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
Tactic: obtain h | h := ha
Cleared hypotheses: ha
-- 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₁
⊢ ∃ (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 + {a} = s₁ + t
Tactic: refine ⟨(s₁.erase a + t, s₂), GameAdd.fst ⟨t, a, hr, ?_⟩, ?_⟩