ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>m : Type u_2<VAR>R : Type u_5<VAR>α : Type v<VAR>ι : Type u_6<VAR>SMul R α<VAR>x : R<VAR>v : m → α<GOAL>Matrix.row ι (x • v) = x • Matrix.row ι v
<VAR>m : Type u_2<VAR>α : Type v<VAR>ι : Type u_6<VAR>v : m → α<GOAL>(Matrix.col ι v).transpose = Matrix.row ι v
<VAR>m : Type u_2<VAR>α : Type v<VAR>ι : Type u_6<VAR>v : m → α<GOAL>(Matrix.row ι v).transpose = Matrix.col ι v
<VAR>m : Type u_2<VAR>α : Type v<VAR>ι : Type u_6<VAR>Star α<VAR>v : m → α<GOAL>(Matrix.col ι v).conjTranspose = Matrix.row ι (star v)
<VAR>m : Type u_2<VAR>α : Type v<VAR>ι : Type u_6<VAR>Star α<VAR>v : m → α<GOAL>(Matrix.row ι v).conjTranspose = Matrix.col ι (star v)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>ι : Type u_6<VAR>Fintype m<VAR>NonUnitalNonAssocSemiring α<VAR>M : Matrix m n α<VAR>v : m → α<GOAL>Matrix.row ι (Matrix.vecMul v M) = Matrix.row ι v * M
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>ι : Type u_6<VAR>Fintype m<VAR>NonUnitalNonAssocSemiring α<VAR>M : Matrix m n α<VAR>v : m → α<GOAL>Matrix.col ι (Matrix.vecMul v M) = (Matrix.row ι v * M).transpose
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>ι : Type u_6<VAR>Fintype n<VAR>NonUnitalNonAssocSemiring α<VAR>M : Matrix m n α<VAR>v : n → α<GOAL>Matrix.col ι (M.mulVec v) = M * Matrix.col ι v
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>ι : Type u_6<VAR>Fintype n<VAR>NonUnitalNonAssocSemiring α<VAR>M : Matrix m n α<VAR>v : n → α<GOAL>Matrix.row ι (M.mulVec v) = (M * Matrix.col ι v).transpose
<VAR>m : Type u_2<VAR>α : Type v<VAR>ι : Type u_6<VAR>Fintype m<VAR>Mul α<VAR>AddCommMonoid α<VAR>v w : m → α<VAR>i j : ι<GOAL>(Matrix.row ι v * Matrix.col ι w) i j = Matrix.dotProduct v w
<VAR>n : Type u_3<VAR>α : Type v<VAR>ι : Type u_6<VAR>Mul α<VAR>AddCommMonoid α<VAR>Unique ι<VAR>a b : n → α<GOAL>(Matrix.col ι a * Matrix.row ι b).diag = a * b
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>ι : Type u_6<VAR>Mul α<VAR>AddCommMonoid α<VAR>Unique ι<VAR>w : m → α<VAR>v : n → α<GOAL>Matrix.vecMulVec w v = Matrix.col ι w * Matrix.row ι v
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>M : Matrix m n α<VAR>i : m<VAR>b : n → α<VAR>DecidableEq m<GOAL>M.updateRow i b i = b
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>M : Matrix m n α<VAR>i : m<VAR>j : n<VAR>c : m → α<VAR>DecidableEq n<GOAL>M.updateColumn j c i j = c i
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>M : Matrix m n α<VAR>i : m<VAR>b : n → α<VAR>DecidableEq m<VAR>i' : m<VAR>i_ne : i' ≠ i<GOAL>M.updateRow i b i' = M i'
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>M : Matrix m n α<VAR>i : m<VAR>j : n<VAR>c : m → α<VAR>DecidableEq n<VAR>j' : n<VAR>j_ne : j' ≠ j<GOAL>M.updateColumn j c i j' = M i j'
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>M : Matrix m n α<VAR>i : m<VAR>j : n<VAR>b : n → α<VAR>DecidableEq m<VAR>i' : m<GOAL>M.updateRow i b i' j = if i' = i then b j else M i' j
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>M : Matrix m n α<VAR>i : m<VAR>j : n<VAR>c : m → α<VAR>DecidableEq n<VAR>j' : n<GOAL>M.updateColumn j c i j' = if j' = j then c i else M i j'
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_5<VAR>Subsingleton n<VAR>A : Matrix m n R<VAR>i : n<VAR>b : m → R<GOAL>A.updateColumn i b = (Matrix.col (Fin 1) b).submatrix id (Function.const n 0)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_5<VAR>Subsingleton m<VAR>A : Matrix m n R<VAR>i : m<VAR>b : n → R<GOAL>A.updateRow i b = (Matrix.row (Fin 1) b).submatrix (Function.const m 0) id
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>β : Type w<VAR>M : Matrix m n α<VAR>i : m<VAR>b : n → α<VAR>DecidableEq m<VAR>f : α → β<GOAL>(M.updateRow i b).map f = (M.map f).updateRow i (f ∘ b)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>β : Type w<VAR>M : Matrix m n α<VAR>j : n<VAR>c : m → α<VAR>DecidableEq n<VAR>f : α → β<GOAL>(M.updateColumn j c).map f = (M.map f).updateColumn j (f ∘ c)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>M : Matrix m n α<VAR>j : n<VAR>c : m → α<VAR>DecidableEq n<GOAL>M.transpose.updateRow j c = (M.updateColumn j c).transpose
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>M : Matrix m n α<VAR>i : m<VAR>b : n → α<VAR>DecidableEq m<GOAL>M.transpose.updateColumn i b = (M.updateRow i b).transpose
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>M : Matrix m n α<VAR>j : n<VAR>c : m → α<VAR>DecidableEq n<VAR>Star α<GOAL>M.conjTranspose.updateRow j (star c) = (M.updateColumn j c).conjTranspose
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>M : Matrix m n α<VAR>i : m<VAR>b : n → α<VAR>DecidableEq m<VAR>Star α<GOAL>M.conjTranspose.updateColumn i (star b) = (M.updateRow i b).conjTranspose
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq m<VAR>A : Matrix m n α<VAR>i : m<GOAL>A.updateRow i (A i) = A
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>A : Matrix m n α<VAR>i : n<GOAL>(A.updateColumn i fun j => A j i) = A
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>v : n → α<VAR>i : n<VAR>x : α<GOAL>(Matrix.diagonal v).updateColumn i (Pi.single i x) = Matrix.diagonal (Function.update v i x)
<VAR>n : Type u_3<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>v : n → α<VAR>i : n<VAR>x : α<GOAL>(Matrix.diagonal v).updateRow i (Pi.single i x) = Matrix.diagonal (Function.update v i x)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>DecidableEq l<VAR>DecidableEq m<VAR>A : Matrix m n α<VAR>i : l<VAR>r : o → α<VAR>e : l ≃ m<VAR>f : o ≃ n<GOAL>(A.submatrix ⇑e ⇑f).updateRow i r = (A.updateRow (e i) fun j => r (f.symm j)).submatrix ⇑e ⇑f
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>DecidableEq l<VAR>DecidableEq m<VAR>A : Matrix m n α<VAR>i : m<VAR>r : n → α<VAR>e : l ≃ m<VAR>f : o ≃ n<GOAL>(A.updateRow i r).submatrix ⇑e ⇑f = (A.submatrix ⇑e ⇑f).updateRow (e.symm i) fun i => r (f i)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>DecidableEq o<VAR>DecidableEq n<VAR>A : Matrix m n α<VAR>j : o<VAR>c : l → α<VAR>e : l ≃ m<VAR>f : o ≃ n<GOAL>(A.submatrix ⇑e ⇑f).updateColumn j c = (A.updateColumn (f j) fun i => c (e.symm i)).submatrix ⇑e ⇑f
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>DecidableEq o<VAR>DecidableEq n<VAR>A : Matrix m n α<VAR>j : n<VAR>c : m → α<VAR>e : l ≃ m<VAR>f : o ≃ n<GOAL>(A.updateColumn j c).submatrix ⇑e ⇑f = (A.submatrix ⇑e ⇑f).updateColumn (f.symm j) fun i => c (e i)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>DecidableEq l<VAR>DecidableEq m<VAR>A : Matrix m n α<VAR>i : l<VAR>r : o → α<VAR>e : m ≃ l<VAR>f : n ≃ o<GOAL>((Matrix.reindex e f) A).updateRow i r = (Matrix.reindex e f) (A.updateRow (e.symm i) fun j => r (f j))
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>DecidableEq l<VAR>DecidableEq m<VAR>A : Matrix m n α<VAR>i : m<VAR>r : n → α<VAR>e : m ≃ l<VAR>f : n ≃ o<GOAL>(Matrix.reindex e f) (A.updateRow i r) = ((Matrix.reindex e f) A).updateRow (e i) fun i => r (f.symm i)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>DecidableEq o<VAR>DecidableEq n<VAR>A : Matrix m n α<VAR>j : o<VAR>c : l → α<VAR>e : m ≃ l<VAR>f : n ≃ o<GOAL>((Matrix.reindex e f) A).updateColumn j c = (Matrix.reindex e f) (A.updateColumn (f.symm j) fun i => c (e i))
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>DecidableEq o<VAR>DecidableEq n<VAR>A : Matrix m n α<VAR>j : n<VAR>c : m → α<VAR>e : m ≃ l<VAR>f : n ≃ o<GOAL>(Matrix.reindex e f) (A.updateColumn j c) = ((Matrix.reindex e f) A).updateColumn (f j) fun i => c (e.symm i)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : m → n → Type v<VAR>M N : DMatrix m n α<GOAL>(∀ (i : m) (j : n), M i j = N i j) ↔ M = N
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : m → n → Type v<VAR>M N : DMatrix m n α<GOAL>(∀ (i : m) (j : n), M i j = N i j) → M = N
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : m → n → Type v<VAR>M : DMatrix m n α<VAR>β : m → n → Type w<VAR>f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j<VAR>i : m<VAR>j : n<GOAL>M.map f i j = f (M i j)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : m → n → Type v<VAR>M : DMatrix m n α<VAR>β : m → n → Type w<VAR>γ : m → n → Type z<VAR>f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j<VAR>g : ⦃i : m⦄ → ⦃j : n⦄ → β i j → γ i j<GOAL>(M.map f).map g = M.map fun i j x => g (f x)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : m → n → Type v<VAR>(i : m) → (j : n) → Zero (α i j)<VAR>i : m<VAR>j : n<GOAL>0 i j = 0
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : m → n → Type v<VAR>(i : m) → (j : n) → Neg (α i j)<VAR>M : DMatrix m n α<VAR>i : m<VAR>j : n<GOAL>(-M) i j = -M i j
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : m → n → Type v<VAR>(i : m) → (j : n) → Add (α i j)<VAR>M N : DMatrix m n α<VAR>i : m<VAR>j : n<GOAL>(M + N) i j = M i j + N i j
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : m → n → Type v<VAR>(i : m) → (j : n) → Sub (α i j)<VAR>M N : DMatrix m n α<VAR>i : m<VAR>j : n<GOAL>(M - N) i j = M i j - N i j
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : m → n → Type v<VAR>(i : m) → (j : n) → Zero (α i j)<VAR>β : m → n → Type w<VAR>(i : m) → (j : n) → Zero (β i j)<VAR>f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j<VAR>h : ∀ (i : m) (j : n), f 0 = 0<GOAL>DMatrix.map 0 f = 0
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : m → n → Type v<VAR>(i : m) → (j : n) → AddMonoid (α i j)<VAR>β : m → n → Type w<VAR>(i : m) → (j : n) → AddMonoid (β i j)<VAR>f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j<VAR>M N : DMatrix m n α<GOAL>((M + N).map fun i j => ⇑f) = (M.map fun i j => ⇑f) + N.map fun i j => ⇑f
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : m → n → Type v<VAR>(i : m) → (j : n) → AddGroup (α i j)<VAR>β : m → n → Type w<VAR>(i : m) → (j : n) → AddGroup (β i j)<VAR>f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j<VAR>M N : DMatrix m n α<GOAL>((M - N).map fun i j => ⇑f) = (M.map fun i j => ⇑f) - N.map fun i j => ⇑f
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : m → n → Type v<VAR>(i : m) → (j : n) → AddMonoid (α i j)<VAR>β : m → n → Type w<VAR>(i : m) → (j : n) → AddMonoid (β i j)<VAR>f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j<VAR>M : DMatrix m n α<GOAL>(AddMonoidHom.mapDMatrix f) M = M.map fun i j => ⇑f
<VAR>α : Type u_1<GOAL>Ordnode.nil.size = 0
<VAR>α : Type u_1<VAR>sz : ℕ<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<GOAL>(Ordnode.node sz l x r).size = sz
<VAR>α : Type u_1<VAR>l : List α<GOAL>⟦l⟧ = ↑l
<VAR>α : Type u_1<VAR>l : List α<GOAL>Quot.mk (fun x x_1 => x ≈ x_1) l = ↑l
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>x : List α<VAR>f : List α → β<VAR>h : ∀ (a b : List α), a ≈ b → f a = f b<GOAL>Quotient.lift f h ↑x = f x
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<GOAL>↑l₁ = ↑l₂ ↔ l₁ ~ l₂
<VAR>α : Type u_1<VAR>l : List α<GOAL>↑l = 0 ↔ l = []
<VAR>α : Type u_1<VAR>l : List α<GOAL>↑l = 0 ↔ l.isEmpty = true
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>a ::ₘ ↑l = ↑(a :: l)
<VAR>α : Type u_1<VAR>a b : α<VAR>s : Multiset α<GOAL>a ::ₘ s = b ::ₘ s ↔ a = b
<VAR>α : Type u_1<VAR>a : α<VAR>s t : Multiset α<GOAL>a ::ₘ s = a ::ₘ t ↔ s = t
<VAR>α : Type u_1<VAR>p : Multiset α → Prop<VAR>empty : p 0<VAR>cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)<VAR>s : Multiset α<GOAL>p s
<VAR>α : Type u_1<VAR>p : Multiset α → Prop<VAR>s : Multiset α<VAR>empty : p 0<VAR>cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)<GOAL>p s
<VAR>α : Type u_1<VAR>a b : α<VAR>s : Multiset α<GOAL>a ::ₘ b ::ₘ s = b ::ₘ a ::ₘ s
<VAR>α : Type u_1<VAR>C : Multiset α → Sort u_3<VAR>C_0 : C 0<VAR>C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)<VAR>C_cons_heq : ∀ (a a' : α) (m : Multiset α) (b : C m), HEq (C_cons a (a' ::ₘ m) (C_cons a' m b)) (C_cons a' (a ::ₘ m) (C_cons a m b))<GOAL>Multiset.recOn 0 C_0 C_cons C_cons_heq = C_0
<VAR>α : Type u_1<VAR>C : Multiset α → Sort u_3<VAR>C_0 : C 0<VAR>C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)<VAR>C_cons_heq : ∀ (a a' : α) (m : Multiset α) (b : C m), HEq (C_cons a (a' ::ₘ m) (C_cons a' m b)) (C_cons a' (a ::ₘ m) (C_cons a m b))<VAR>a : α<VAR>m : Multiset α<GOAL>(a ::ₘ m).recOn C_0 C_cons C_cons_heq = C_cons a m (m.recOn C_0 C_cons C_cons_heq)
<VAR>α : Type u_1<VAR>a b : α<VAR>s : Multiset α<GOAL>a ∈ b ::ₘ s ↔ a = b ∨ a ∈ s
<VAR>α : Type u_1<VAR>a b : α<VAR>s : Multiset α<VAR>h : a ∈ s<GOAL>a ∈ b ::ₘ s
<VAR>α : Type u_1<VAR>a : α<VAR>s : Multiset α<GOAL>a ∈ a ::ₘ s
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>a : α<VAR>s : Multiset α<GOAL>(∀ x ∈ a ::ₘ s, p x) ↔ p a ∧ ∀ x ∈ s, p x
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>a : α<GOAL>a ∈ s → ∃ t, s = a ::ₘ t
<VAR>α : Type u_1<VAR>a : α<GOAL>a ∉ 0
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>(∀ (x : α), x ∉ s) → s = 0
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>s = 0 ↔ ∀ (a : α), a ∉ s
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>s ≠ 0 → ∃ a, a ∈ s
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>s = 0 ∨ ∃ a, a ∈ s
<VAR>α : Type u_1<VAR>a : α<VAR>m : Multiset α<GOAL>0 ≠ a ::ₘ m
<VAR>α : Type u_1<VAR>a : α<VAR>m : Multiset α<GOAL>a ::ₘ m ≠ 0
<VAR>α : Type u_1<VAR>a b : α<VAR>as bs : Multiset α<GOAL>a ::ₘ as = b ::ₘ bs ↔ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
<VAR>α : Type u_1<VAR>a : α<GOAL>a ::ₘ 0 = {a}
<VAR>α : Type u_1<VAR>a : α<GOAL>↑[a] = {a}
<VAR>α : Type u_1<VAR>a b : α<GOAL>b ∈ {a} ↔ b = a
<VAR>α : Type u_1<VAR>a : α<GOAL>a ∈ {a}
<VAR>α : Type u_1<VAR>a b : α<GOAL>{a} = {b} ↔ a = b
<VAR>α : Type u_1<VAR>l : List α<VAR>a : α<GOAL>↑l = {a} ↔ l = [a]
<VAR>α : Type u_1<VAR>a b : α<VAR>m : Multiset α<GOAL>{a} = b ::ₘ m ↔ a = b ∧ m = 0
<VAR>α : Type u_1<VAR>x y : α<GOAL>{x, y} = {y, x}
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<GOAL>↑l₁ ⊆ ↑l₂ ↔ l₁ ⊆ l₂
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>s ⊆ s
<VAR>α : Type u_1<VAR>s t u : Multiset α<GOAL>s ⊆ t → t ⊆ u → s ⊆ u
<VAR>α : Type u_1<VAR>s t : Multiset α<GOAL>s ⊆ t ↔ ∀ ⦃x : α⦄, x ∈ s → x ∈ t
<VAR>α : Type u_1<VAR>s t : Multiset α<VAR>a : α<VAR>h : s ⊆ t<GOAL>a ∈ s → a ∈ t
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>0 ⊆ s
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>a : α<GOAL>s ⊆ a ::ₘ s
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>a : α<VAR>ha : a ∉ s<GOAL>s ⊂ a ::ₘ s
<VAR>α : Type u_1<VAR>a : α<VAR>s t : Multiset α<GOAL>a ::ₘ s ⊆ t ↔ a ∈ t ∧ s ⊆ t
<VAR>α : Type u_1<VAR>a : α<VAR>s t : Multiset α<GOAL>s ⊆ t → a ::ₘ s ⊆ a ::ₘ t
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>h : s ⊆ 0<GOAL>s = 0
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>s ⊆ 0 ↔ s = 0
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>0 ⊂ s ↔ s ≠ 0
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>a : α<GOAL>{a} ⊆ s ↔ a ∈ s
<VAR>α : Type u_1<VAR>p : Multiset α → Prop<VAR>S : Multiset α<VAR>h₁ : p 0<VAR>h₂ : ∀ {a : α} {s : Multiset α}, a ∈ S → s ⊆ S → p s → p (insert a s)<GOAL>p S
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>↑s.toList = s
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>s.toList = [] ↔ s = 0
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>s.toList.isEmpty = true ↔ s = 0
<VAR>α : Type u_1<GOAL>Multiset.toList 0 = []
<VAR>α : Type u_1<VAR>a : α<VAR>s : Multiset α<GOAL>a ∈ s.toList ↔ a ∈ s
<VAR>α : Type u_1<VAR>a : α<VAR>m : Multiset α<GOAL>m.toList = [a] ↔ m = {a}
<VAR>α : Type u_1<VAR>a : α<GOAL>{a}.toList = [a]
<VAR>α : Type u_1<VAR>s t : Multiset α<GOAL>s ≤ t → s ⊆ t
<VAR>α : Type u_1<VAR>s t : Multiset α<VAR>a : α<VAR>h : s ≤ t<GOAL>a ∈ s → a ∈ t
<VAR>α : Type u_1<VAR>s t : Multiset α<VAR>a : α<VAR>h : s ⊆ t<GOAL>a ∉ t → a ∉ s
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<GOAL>↑l₁ ≤ ↑l₂ ↔ l₁ <+~ l₂
<VAR>α : Type u_1<VAR>C : Multiset α → Multiset α → Prop<VAR>s t : Multiset α<VAR>h : s ≤ t<VAR>H : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → C ↑l₁ ↑l₂<GOAL>C s t
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>0 ≤ s
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>s ≤ 0 ↔ s = 0
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>a : α<GOAL>s < a ::ₘ s
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>a : α<GOAL>s ≤ a ::ₘ s
<VAR>α : Type u_1<VAR>s t : Multiset α<VAR>a : α<GOAL>a ::ₘ s ≤ a ::ₘ t ↔ s ≤ t
<VAR>α : Type u_1<VAR>s t : Multiset α<VAR>a : α<GOAL>s ≤ t → a ::ₘ s ≤ a ::ₘ t
<VAR>α : Type u_1<VAR>s t : Multiset α<VAR>a : α<GOAL>a ::ₘ s < a ::ₘ t ↔ s < t
<VAR>α : Type u_1<VAR>s t : Multiset α<VAR>a : α<VAR>h : s < t<GOAL>a ::ₘ s < a ::ₘ t
<VAR>α : Type u_1<VAR>s t : Multiset α<VAR>a : α<VAR>m : a ∉ s<GOAL>s ≤ a ::ₘ t ↔ s ≤ t
<VAR>α : Type u_1<VAR>a : α<GOAL>{a} ≠ 0
<VAR>α : Type u_1<VAR>a : α<VAR>s : Multiset α<GOAL>{a} ≤ s ↔ a ∈ s
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>a : α<GOAL>s ≤ {a} ↔ s = 0 ∨ s = {a}
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>a : α<GOAL>s < {a} ↔ s = 0
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>a : α<GOAL>s ⊂ {a} ↔ s = 0
<VAR>α : Type u_1<VAR>s t : List α<GOAL>↑s + ↑t = ↑(s ++ t)
<VAR>α : Type u_1<VAR>a : α<VAR>s : Multiset α<GOAL>{a} + s = a ::ₘ s
<VAR>α : Type u_1<VAR>s t u : Multiset α<GOAL>s + t ≤ s + u ↔ t ≤ u
<VAR>α : Type u_1<VAR>s t : Multiset α<GOAL>s ≤ s + t
<VAR>α : Type u_1<VAR>s t : Multiset α<GOAL>s ≤ t + s
<VAR>α : Type u_1<VAR>s t : Multiset α<GOAL>s ≤ t ↔ ∃ u, t = s + u
<VAR>α : Type u_1<VAR>a : α<VAR>s t : Multiset α<GOAL>a ::ₘ s + t = a ::ₘ (s + t)
<VAR>α : Type u_1<VAR>a : α<VAR>s t : Multiset α<GOAL>s + a ::ₘ t = a ::ₘ (s + t)
<VAR>α : Type u_1<VAR>a : α<VAR>s t : Multiset α<GOAL>a ∈ s + t ↔ a ∈ s ∨ a ∈ t
<VAR>α : Type u_1<VAR>a : α<VAR>s : Multiset α<VAR>n : ℕ<VAR>h : a ∈ n • s<GOAL>a ∈ s
<VAR>α : Type u_1<VAR>a : α<VAR>s : Multiset α<VAR>n : ℕ<GOAL>a ∈ n • s ↔ n ≠ 0 ∧ a ∈ s
<VAR>α : Type u_1<VAR>a : α<VAR>s : Multiset α<VAR>n : ℕ<VAR>h0 : n ≠ 0<GOAL>a ∈ n • s ↔ a ∈ s
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>n : ℕ<VAR>a : α<GOAL>n • (a ::ₘ s) = n • {a} + n • s
<VAR>α : Type u_1<VAR>l : List α<GOAL>Multiset.card ↑l = l.length
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>s.toList.length = Multiset.card s
<VAR>α : Type u_1<GOAL>Multiset.card 0 = 0
<VAR>α : Type u_1<VAR>s t : Multiset α<GOAL>Multiset.card (s + t) = Multiset.card s + Multiset.card t
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>n : ℕ<GOAL>Multiset.card (n • s) = n * Multiset.card s
<VAR>α : Type u_1<VAR>a : α<VAR>s : Multiset α<GOAL>Multiset.card (a ::ₘ s) = Multiset.card s + 1
<VAR>α : Type u_1<VAR>a : α<GOAL>Multiset.card {a} = 1
<VAR>α : Type u_1<VAR>a b : α<GOAL>Multiset.card {a, b} = 2
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>Multiset.card s = 1 ↔ ∃ a, s = {a}
<VAR>α : Type u_1<VAR>s t : Multiset α<VAR>h : s ≤ t<GOAL>Multiset.card s ≤ Multiset.card t
<VAR>α : Type u_1<GOAL>Monotone ⇑Multiset.card
<VAR>α : Type u_1<VAR>s t : Multiset α<VAR>h : s ≤ t<GOAL>Multiset.card t ≤ Multiset.card s → s = t
<VAR>α : Type u_1<VAR>s t : Multiset α<VAR>h : s < t<GOAL>Multiset.card s < Multiset.card t
<VAR>α : Type u_1<GOAL>StrictMono ⇑Multiset.card
<VAR>α : Type u_1<VAR>s t : Multiset α<GOAL>s < t ↔ ∃ a, a ::ₘ s ≤ t
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>Multiset.card s = 0 ↔ s = 0
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>0 < Multiset.card s ↔ s ≠ 0
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>0 < Multiset.card s ↔ ∃ a, a ∈ s
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>Multiset.card s = 2 ↔ ∃ x y, s = {x, y}
<VAR>α : Type u_1<VAR>s : Multiset α<GOAL>Multiset.card s = 3 ↔ ∃ x y z, s = {x, y, z}
<VAR>α : Type u_1<VAR>p : Multiset α → Sort u_3<VAR>s : Multiset α<VAR>H : (s : Multiset α) → ((t : Multiset α) → t < s → p t) → p s<GOAL>s.strongInductionOn H = H s fun t _h => t.strongInductionOn H
<VAR>α : Type u_1<VAR>p : Multiset α → Prop<VAR>s : Multiset α<VAR>h₀ : p 0<VAR>h₁ : ∀ (a : α) (s : Multiset α), (∀ t ≤ s, p t) → p (a ::ₘ s)<GOAL>p s
<VAR>α : Type u_1<VAR>p : Multiset α → Sort u_3<VAR>n : ℕ<VAR>H : (t₁ : Multiset α) → ({t₂ : Multiset α} → Multiset.card t₂ ≤ n → t₁ < t₂ → p t₂) → Multiset.card t₁ ≤ n → p t₁<VAR>s : Multiset α<GOAL>Multiset.strongDownwardInduction H s = H s fun {t₂} ht _hst => Multiset.strongDownwardInduction H t₂ ht
<VAR>α : Type u_1<VAR>p : Multiset α → Sort u_3<VAR>s : Multiset α<VAR>n : ℕ<VAR>H : (t₁ : Multiset α) → ({t₂ : Multiset α} → Multiset.card t₂ ≤ n → t₁ < t₂ → p t₂) → Multiset.card t₁ ≤ n → p t₁<GOAL>(fun a => s.strongDownwardInductionOn H a) = H s fun {t} ht _h => t.strongDownwardInductionOn H ht
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a : α<GOAL>↑(List.replicate n a) = Multiset.replicate n a
<VAR>α : Type u_1<VAR>a : α<GOAL>Multiset.replicate 0 a = 0
<VAR>α : Type u_1<VAR>a : α<VAR>n : ℕ<GOAL>Multiset.replicate (n + 1) a = a ::ₘ Multiset.replicate n a
<VAR>α : Type u_1<VAR>m n : ℕ<VAR>a : α<GOAL>Multiset.replicate (m + n) a = Multiset.replicate m a + Multiset.replicate n a
<VAR>α : Type u_1<VAR>a : α<VAR>n : ℕ<GOAL>(Multiset.replicateAddMonoidHom a) n = Multiset.replicate n a
<VAR>α : Type u_1<VAR>a : α<GOAL>Multiset.replicate 1 a = {a}
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a : α<GOAL>Multiset.card (Multiset.replicate n a) = n
<VAR>α : Type u_1<VAR>a b : α<VAR>n : ℕ<GOAL>b ∈ Multiset.replicate n a ↔ n ≠ 0 ∧ b = a
<VAR>α : Type u_1<VAR>a b : α<VAR>n : ℕ<GOAL>b ∈ Multiset.replicate n a → b = a
<VAR>α : Type u_1<VAR>a : α<VAR>s : Multiset α<GOAL>s = Multiset.replicate (Multiset.card s) a ↔ ∀ b ∈ s, b = a
<VAR>α : Type u_1<VAR>a : α<VAR>n : ℕ<VAR>s : Multiset α<GOAL>s = Multiset.replicate n a ↔ Multiset.card s = n ∧ ∀ b ∈ s, b = a
<VAR>α : Type u_1<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>Function.Injective (Multiset.replicate n)
<VAR>α : Type u_1<VAR>a b : α<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>Multiset.replicate n a = Multiset.replicate n b ↔ a = b
<VAR>α : Type u_1<VAR>a : α<GOAL>Function.Injective fun x => Multiset.replicate x a
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a : α<GOAL>Multiset.replicate n a ⊆ {a}
<VAR>α : Type u_1<VAR>a : α<VAR>n : ℕ<VAR>l : List α<GOAL>Multiset.replicate n a ≤ ↑l ↔ List.replicate n a <+ l
<VAR>α : Type u_1<VAR>a : α<VAR>n m : ℕ<GOAL>n • Multiset.replicate m a = Multiset.replicate (n * m) a
<VAR>α : Type u_1<VAR>a : α<VAR>n : ℕ<GOAL>n • {a} = Multiset.replicate n a
<VAR>α : Type u_1<VAR>a : α<VAR>k n : ℕ<GOAL>Multiset.replicate k a ≤ Multiset.replicate n a ↔ k ≤ n
<VAR>α : Type u_1<VAR>m : Multiset α<VAR>a : α<VAR>n : ℕ<GOAL>m ≤ Multiset.replicate n a ↔ ∃ k ≤ n, m = Multiset.replicate k a
<VAR>α : Type u_1<VAR>m : Multiset α<VAR>x : α<VAR>n : ℕ<GOAL>m < Multiset.replicate (n + 1) x ↔ m ≤ Multiset.replicate n x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>a : α<GOAL>(↑l).erase a = ↑(l.erase a)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<GOAL>Multiset.erase 0 a = 0
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>(a ::ₘ s).erase a = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<VAR>s : Multiset α<VAR>h : b ≠ a<GOAL>(b ::ₘ s).erase a = b ::ₘ s.erase a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<GOAL>{a}.erase a = 0
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>a ∉ s → s.erase a = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<VAR>a : α<GOAL>a ∈ s → a ::ₘ s.erase a = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<VAR>a b : α<VAR>h : a ∈ s<GOAL>(b ::ₘ s).erase a = b ::ₘ s.erase a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<VAR>a : α<GOAL>s ≤ a ::ₘ s.erase a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<VAR>a : α<GOAL>s + {a} = t ↔ a ∈ t ∧ s = t.erase a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<VAR>t : Multiset α<GOAL>a ∈ s → (s + t).erase a = s.erase a + t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<VAR>t : Multiset α<VAR>h : a ∈ t<GOAL>(s + t).erase a = s + t.erase a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<VAR>t : Multiset α<GOAL>a ∉ s → (s + t).erase a = s + t.erase a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<VAR>t : Multiset α<VAR>h : a ∉ t<GOAL>(s + t).erase a = s.erase a + t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>s.erase a ≤ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>s.erase a < s ↔ a ∈ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>s.erase a ⊆ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<VAR>s : Multiset α<VAR>ab : a ≠ b<GOAL>a ∈ s.erase b ↔ a ∈ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<VAR>s : Multiset α<GOAL>a ∈ s.erase b → a ∈ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<VAR>a b : α<GOAL>(s.erase a).erase b = (s.erase b).erase a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<VAR>a : α<VAR>h : s ≤ t<GOAL>s.erase a ≤ t.erase a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<VAR>a : α<GOAL>s.erase a ≤ t ↔ s ≤ a ::ₘ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>a ∈ s → Multiset.card (s.erase a) = (Multiset.card s).pred