ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_4<VAR>m : Type u_9<VAR>n : Type u_10<VAR>CommRing R<VAR>CommRing α<VAR>CommRing β<VAR>Algebra R α<VAR>Algebra R β<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq m<VAR>DecidableEq n<VAR>A : Matrix m m α<VAR>B : Matrix n n β<GOAL>(Matrix.kroneckerMap (TensorProduct.tmul R) A B).det = (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Fintype α<VAR>CompleteLattice β<VAR>f : α → β<GOAL>Finset.univ.sup f = iSup f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Fintype α<VAR>CompleteLattice β<VAR>f : α → β<GOAL>Finset.univ.inf f = iInf f
<VAR>α : Type u_2<VAR>Fintype α<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>a : α<GOAL>Finset.fold (fun x x_1 => x ⊓ x_1) a (fun x => x) Finset.univ = ⊥
<VAR>α : Type u_2<VAR>Fintype α<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>a : α<GOAL>Finset.fold (fun x x_1 => x ⊔ x_1) a (fun x => x) Finset.univ = ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Fintype α<VAR>DecidableEq α<VAR>s : Finset ι<VAR>f : ι → Finset α<VAR>a : α<GOAL>a ∈ s.inf f ↔ ∀ i ∈ s, a ∈ f i
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Finite α<VAR>Nonempty α<VAR>LinearOrder β<VAR>f : α → β<GOAL>∃ x₀, ∀ (x : α), f x ≤ f x₀
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Finite α<VAR>Nonempty α<VAR>LinearOrder β<VAR>f : α → β<GOAL>∃ x₀, ∀ (x : α), f x₀ ≤ f x
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>self : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : F α<GOAL>MvQPF.abs (MvQPF.repr x) = x
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>self : MvQPF F<VAR>α β : TypeVec.{u} n<VAR>f : α ⟹ β<VAR>p : ↑(MvQPF.P F) α<GOAL>MvQPF.abs (f <$$> p) = f <$$> MvQPF.abs p
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>p : ⦃i : Fin2 n⦄ → α i → Prop<VAR>x : F α<GOAL>MvFunctor.LiftP p x ↔ ∃ a f, x = MvQPF.abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (MvQPF.P F).B a i), p (f i j)
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>r : {i : Fin2 n} → α i → α i → Prop<VAR>x y : F α<GOAL>MvFunctor.LiftR (fun {i} => r) x y ↔ ∃ a f₀ f₁, x = MvQPF.abs ⟨a, f₀⟩ ∧ y = MvQPF.abs ⟨a, f₁⟩ ∧ ∀ (i : Fin2 n) (j : (MvQPF.P F).B a i), r (f₀ i j) (f₁ i j)
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : F α<VAR>i : Fin2 n<VAR>u : α i<GOAL>u ∈ MvFunctor.supp x i ↔ ∀ (a : (MvQPF.P F).A) (f : (MvQPF.P F).B a ⟹ α), MvQPF.abs ⟨a, f⟩ = x → u ∈ f i '' Set.univ
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>i : Fin2 n<VAR>x : F α<GOAL>MvFunctor.supp x i = {u | ∀ (a : (MvQPF.P F).A) (f : (MvQPF.P F).B a ⟹ α), MvQPF.abs ⟨a, f⟩ = x → u ∈ f i '' Set.univ}
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : F α<GOAL>(∀ (p : (i : Fin2 n) → α i → Prop), MvFunctor.LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ MvFunctor.supp x i, p i u) ↔ ∃ a f, MvQPF.abs ⟨a, f⟩ = x ∧ ∀ (i : Fin2 n) (a' : (MvQPF.P F).A) (f' : (MvQPF.P F).B a' ⟹ α), MvQPF.abs ⟨a', f'⟩ = x → f i '' Set.univ ⊆ f' i '' Set.univ
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>h : MvQPF.IsUniform<VAR>α : TypeVec.{u} n<VAR>a : (MvQPF.P F).A<VAR>f : (MvQPF.P F).B a ⟹ α<VAR>i : Fin2 n<GOAL>MvFunctor.supp (MvQPF.abs ⟨a, f⟩) i = f i '' Set.univ
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>h : MvQPF.IsUniform<VAR>α : TypeVec.{u} n<VAR>x : F α<VAR>p : (i : Fin2 n) → α i → Prop<GOAL>MvFunctor.LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ MvFunctor.supp x i, p i u
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>h : MvQPF.IsUniform<VAR>α β : TypeVec.{u} n<VAR>g : α ⟹ β<VAR>x : F α<VAR>i : Fin2 n<GOAL>MvFunctor.supp (g <$$> x) i = g i '' MvFunctor.supp x i
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<GOAL>MvQPF.SuppPreservation ↔ MvQPF.IsUniform
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<GOAL>MvQPF.SuppPreservation ↔ MvQPF.LiftPPreservation
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<GOAL>MvQPF.LiftPPreservation ↔ MvQPF.IsUniform
<VAR>n : ℕ<GOAL>Finset.map Fin.valEmbedding Finset.univ = Finset.Iio n
<VAR>n : ℕ<GOAL>Finset.Ioi 0 = Finset.map (Fin.succEmb n) Finset.univ
<VAR>n : ℕ<GOAL>Finset.Iio (Fin.last n) = Finset.map Fin.castSuccEmb Finset.univ
<VAR>n : ℕ<VAR>i : Fin n<GOAL>Finset.Ioi i.succ = Finset.map (Fin.succEmb n) (Finset.Ioi i)
<VAR>n : ℕ<VAR>i : Fin n<GOAL>Finset.Iio i.castSucc = Finset.map Fin.castSuccEmb (Finset.Iio i)
<VAR>n : ℕ<VAR>p : Fin (n + 1) → Prop<VAR>DecidablePred p<GOAL>(Finset.filter p Finset.univ).card = (if p 0 then 1 else 0) + (Finset.filter (p ∘ Fin.succ) Finset.univ).card
<VAR>n : ℕ<VAR>p : Fin (n + 1) → Prop<VAR>DecidablePred p<GOAL>(Finset.filter p Finset.univ).card = if p 0 then (Finset.filter (p ∘ Fin.succ) Finset.univ).card + 1 else (Finset.filter (p ∘ Fin.succ) Finset.univ).card
<VAR>α : Type u_1<VAR>n : ℕ<VAR>DecidableEq α<VAR>a : α<VAR>v : Mathlib.Vector α n<GOAL>(Finset.filter (fun i => a = v.get i) Finset.univ).card = List.count a v.toList
<VAR>α : Type u<VAR>m : ℕ<VAR>n' : Type uₙ<VAR>v : n' → α<VAR>B : Fin m → n' → α<VAR>i : Fin m.succ<VAR>j : n'<GOAL>Matrix.vecCons v B i j = Matrix.vecCons (v j) (fun i => B i j) i
<VAR>α : Type u<VAR>m : ℕ<VAR>n' : Type uₙ<VAR>B : Fin m.succ → n' → α<VAR>j : n'<GOAL>(Matrix.vecHead fun i => B i j) = Matrix.vecHead B j
<VAR>α : Type u<VAR>m : ℕ<VAR>n' : Type uₙ<VAR>B : Fin m.succ → n' → α<VAR>j : n'<GOAL>(Matrix.vecTail fun i => B i j) = fun i => Matrix.vecTail B i j
<VAR>α : Type u<VAR>AddCommMonoid α<VAR>Mul α<VAR>v w : Fin 0 → α<GOAL>Matrix.dotProduct v w = 0
<VAR>α : Type u<VAR>n : ℕ<VAR>AddCommMonoid α<VAR>Mul α<VAR>x : α<VAR>v : Fin n → α<VAR>w : Fin n.succ → α<GOAL>Matrix.dotProduct (Matrix.vecCons x v) w = x * Matrix.vecHead w + Matrix.dotProduct v (Matrix.vecTail w)
<VAR>α : Type u<VAR>n : ℕ<VAR>AddCommMonoid α<VAR>Mul α<VAR>v : Fin n.succ → α<VAR>x : α<VAR>w : Fin n → α<GOAL>Matrix.dotProduct v (Matrix.vecCons x w) = Matrix.vecHead v * x + Matrix.dotProduct (Matrix.vecTail v) w
<VAR>α : Type u<VAR>n : ℕ<VAR>AddCommMonoid α<VAR>Mul α<VAR>x : α<VAR>v : Fin n → α<VAR>y : α<VAR>w : Fin n → α<GOAL>Matrix.dotProduct (Matrix.vecCons x v) (Matrix.vecCons y w) = x * y + Matrix.dotProduct v w
<VAR>α : Type u<VAR>ι : Type u_1<VAR>v : Fin 0 → α<GOAL>Matrix.col ι v = ![]
<VAR>α : Type u<VAR>m : ℕ<VAR>ι : Type u_1<VAR>x : α<VAR>u : Fin m → α<GOAL>Matrix.col ι (Matrix.vecCons x u) = Matrix.of (Matrix.vecCons (fun x_1 => x) (Matrix.col ι u))
<VAR>α : Type u<VAR>ι : Type u_1<GOAL>Matrix.row ι ![] = Matrix.of fun x => ![]
<VAR>α : Type u<VAR>m : ℕ<VAR>ι : Type u_1<VAR>x : α<VAR>u : Fin m → α<GOAL>Matrix.row ι (Matrix.vecCons x u) = Matrix.of fun x_1 => Matrix.vecCons x u
<VAR>α : Type u<VAR>m' : Type uₘ<VAR>A : Matrix m' (Fin 0) α<GOAL>A.transpose = Matrix.of ![]
<VAR>α : Type u<VAR>m' : Type uₘ<VAR>A : Matrix (Fin 0) m' α<GOAL>A.transpose = Matrix.of fun x => ![]
<VAR>α : Type u<VAR>m : ℕ<VAR>n' : Type uₙ<VAR>v : n' → α<VAR>A : Matrix (Fin m) n' α<GOAL>(Matrix.of (Matrix.vecCons v A)).transpose = Matrix.of fun i => Matrix.vecCons (v i) (A.transpose i)
<VAR>α : Type u<VAR>n : ℕ<VAR>m' : Type uₘ<VAR>A : Matrix m' (Fin n.succ) α<GOAL>Matrix.vecHead (Matrix.of.symm A.transpose) = Matrix.vecHead ∘ Matrix.of.symm A
<VAR>α : Type u<VAR>n : ℕ<VAR>m' : Type uₘ<VAR>A : Matrix m' (Fin n.succ) α<GOAL>Matrix.vecTail (Matrix.of.symm A.transpose) = Matrix.transpose (Matrix.vecTail ∘ A)
<VAR>α : Type u<VAR>n' : Type uₙ<VAR>o' : Type uₒ<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype n'<VAR>A : Matrix (Fin 0) n' α<VAR>B : Matrix n' o' α<GOAL>A * B = Matrix.of ![]
<VAR>α : Type u<VAR>m' : Type uₘ<VAR>o' : Type uₒ<VAR>NonUnitalNonAssocSemiring α<VAR>A : Matrix m' (Fin 0) α<VAR>B : Matrix (Fin 0) o' α<GOAL>A * B = 0
<VAR>α : Type u<VAR>m' : Type uₘ<VAR>n' : Type uₙ<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype n'<VAR>A : Matrix m' n' α<VAR>B : Matrix n' (Fin 0) α<GOAL>A * B = Matrix.of fun x => ![]
<VAR>α : Type u<VAR>m : ℕ<VAR>n' : Type uₙ<VAR>o' : Type uₒ<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype n'<VAR>A : Matrix (Fin m.succ) n' α<VAR>B : Matrix n' o' α<VAR>i : Fin m<VAR>j : o'<GOAL>(A * B) i.succ j = (Matrix.of (Matrix.vecTail (Matrix.of.symm A)) * B) i j
<VAR>α : Type u<VAR>m : ℕ<VAR>n' : Type uₙ<VAR>o' : Type uₒ<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype n'<VAR>v : n' → α<VAR>A : Fin m → n' → α<VAR>B : Matrix n' o' α<GOAL>Matrix.of (Matrix.vecCons v A) * B = Matrix.of (Matrix.vecCons (Matrix.vecMul v B) (Matrix.of.symm (Matrix.of A * B)))
<VAR>α : Type u<VAR>o' : Type uₒ<VAR>NonUnitalNonAssocSemiring α<VAR>v : Fin 0 → α<VAR>B : Matrix (Fin 0) o' α<GOAL>Matrix.vecMul v B = 0
<VAR>α : Type u<VAR>n' : Type uₙ<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype n'<VAR>v : n' → α<VAR>B : Matrix n' (Fin 0) α<GOAL>Matrix.vecMul v B = ![]
<VAR>α : Type u<VAR>n : ℕ<VAR>o' : Type uₒ<VAR>NonUnitalNonAssocSemiring α<VAR>x : α<VAR>v : Fin n → α<VAR>B : Fin n.succ → o' → α<GOAL>Matrix.vecMul (Matrix.vecCons x v) (Matrix.of B) = x • Matrix.vecHead B + Matrix.vecMul v (Matrix.of (Matrix.vecTail B))
<VAR>α : Type u<VAR>n : ℕ<VAR>o' : Type uₒ<VAR>NonUnitalNonAssocSemiring α<VAR>v : Fin n.succ → α<VAR>w : o' → α<VAR>B : Fin n → o' → α<GOAL>Matrix.vecMul v (Matrix.of (Matrix.vecCons w B)) = Matrix.vecHead v • w + Matrix.vecMul (Matrix.vecTail v) (Matrix.of B)
<VAR>α : Type u<VAR>n : ℕ<VAR>o' : Type uₒ<VAR>NonUnitalNonAssocSemiring α<VAR>x : α<VAR>v : Fin n → α<VAR>w : o' → α<VAR>B : Fin n → o' → α<GOAL>Matrix.vecMul (Matrix.vecCons x v) (Matrix.of (Matrix.vecCons w B)) = x • w + Matrix.vecMul v (Matrix.of B)
<VAR>α : Type u<VAR>n' : Type uₙ<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype n'<VAR>A : Matrix (Fin 0) n' α<VAR>v : n' → α<GOAL>A.mulVec v = ![]
<VAR>α : Type u<VAR>m' : Type uₘ<VAR>NonUnitalNonAssocSemiring α<VAR>A : Matrix m' (Fin 0) α<VAR>v : Fin 0 → α<GOAL>A.mulVec v = 0
<VAR>α : Type u<VAR>m : ℕ<VAR>n' : Type uₙ<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype n'<VAR>v : n' → α<VAR>A : Fin m → n' → α<VAR>w : n' → α<GOAL>(Matrix.of (Matrix.vecCons v A)).mulVec w = Matrix.vecCons (Matrix.dotProduct v w) ((Matrix.of A).mulVec w)
<VAR>n : ℕ<VAR>m' : Type uₘ<VAR>α : Type u_1<VAR>CommSemiring α<VAR>A : m' → Fin n.succ → α<VAR>x : α<VAR>v : Fin n → α<GOAL>(Matrix.of A).mulVec (Matrix.vecCons x v) = x • Matrix.vecHead ∘ A + (Matrix.of (Matrix.vecTail ∘ A)).mulVec v
<VAR>α : Type u<VAR>n' : Type uₙ<VAR>NonUnitalNonAssocSemiring α<VAR>v : Fin 0 → α<VAR>w : n' → α<GOAL>Matrix.vecMulVec v w = ![]
<VAR>α : Type u<VAR>m' : Type uₘ<VAR>NonUnitalNonAssocSemiring α<VAR>v : m' → α<VAR>w : Fin 0 → α<GOAL>Matrix.vecMulVec v w = Matrix.of fun x => ![]
<VAR>α : Type u<VAR>m : ℕ<VAR>n' : Type uₙ<VAR>NonUnitalNonAssocSemiring α<VAR>x : α<VAR>v : Fin m → α<VAR>w : n' → α<GOAL>Matrix.vecMulVec (Matrix.vecCons x v) w = Matrix.vecCons (x • w) (Matrix.vecMulVec v w)
<VAR>α : Type u<VAR>n : ℕ<VAR>m' : Type uₘ<VAR>NonUnitalNonAssocSemiring α<VAR>v : m' → α<VAR>x : α<VAR>w : Fin n → α<GOAL>Matrix.vecMulVec v (Matrix.vecCons x w) = Matrix.of fun i => v i • Matrix.vecCons x w
<VAR>α : Type u<VAR>NonUnitalNonAssocSemiring α<VAR>m' : Type u_1<VAR>x : α<VAR>A : Fin 0 → m' → α<GOAL>x • A = ![]
<VAR>α : Type u<VAR>m : ℕ<VAR>n' : Type uₙ<VAR>NonUnitalNonAssocSemiring α<VAR>x : α<VAR>v : n' → α<VAR>A : Fin m → n' → α<GOAL>x • Matrix.vecCons v A = Matrix.vecCons (x • v) (x • A)
<VAR>α : Type u<VAR>m' : Type uₘ<VAR>n' : Type uₙ<VAR>o' : Type uₒ<VAR>A : Matrix m' n' α<VAR>row : Fin 0 → m'<VAR>col : o' → n'<GOAL>A.submatrix row col = ![]
<VAR>α : Type u<VAR>m : ℕ<VAR>m' : Type uₘ<VAR>n' : Type uₙ<VAR>o' : Type uₒ<VAR>A : Matrix m' n' α<VAR>i : m'<VAR>row : Fin m → m'<VAR>col : o' → n'<GOAL>A.submatrix (Matrix.vecCons i row) col = Matrix.vecCons (fun j => A i (col j)) (A.submatrix row col)
<VAR>α : Type u<VAR>m : ℕ<VAR>n' : Type uₙ<VAR>o' : Type uₒ<VAR>A : Matrix (Fin m.succ) n' α<VAR>v : n' → α<VAR>f : o' → n'<VAR>i : Fin m.succ<GOAL>(A.updateRow i v).submatrix i.succAbove f = A.submatrix i.succAbove f
<VAR>α : Type u<VAR>n : ℕ<VAR>m' : Type uₘ<VAR>o' : Type uₒ<VAR>A : Matrix m' (Fin n.succ) α<VAR>v : m' → α<VAR>f : o' → m'<VAR>i : Fin n.succ<GOAL>(A.updateColumn i v).submatrix f i.succAbove = A.submatrix f i.succAbove
<VAR>α : Type u<VAR>Zero α<VAR>One α<GOAL>1 = !![1, 0; 0, 1]
<VAR>α : Type u<VAR>Zero α<VAR>One α<GOAL>1 = !![1, 0, 0; 0, 1, 0; 0, 0, 1]
<VAR>α : Type u<VAR>AddMonoidWithOne α<VAR>n : ℕ<GOAL>↑n = !![↑n, 0; 0, ↑n]
<VAR>α : Type u<VAR>AddMonoidWithOne α<VAR>n : ℕ<GOAL>↑n = !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n]
<VAR>α : Type u<VAR>AddMonoidWithOne α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>OfNat.ofNat n = !![OfNat.ofNat n, 0; 0, OfNat.ofNat n]
<VAR>α : Type u<VAR>AddMonoidWithOne α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>OfNat.ofNat n = !![OfNat.ofNat n, 0, 0; 0, OfNat.ofNat n, 0; 0, 0, OfNat.ofNat n]
<VAR>α : Type u<VAR>A : Matrix (Fin 2) (Fin 2) α<GOAL>A = !![A 0 0, A 0 1; A 1 0, A 1 1]
<VAR>α : Type u<VAR>A : Matrix (Fin 3) (Fin 3) α<GOAL>A = !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2]
<VAR>α : Type u<VAR>AddCommMonoid α<VAR>Mul α<VAR>a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α<GOAL>!![a₁₁, a₁₂; a₂₁, a₂₂] * !![b₁₁, b₁₂; b₂₁, b₂₂] = !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]
<VAR>α : Type u<VAR>AddCommMonoid α<VAR>Mul α<VAR>a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α<GOAL>!![a₁₁, a₁₂, a₁₃; a₂₁, a₂₂, a₂₃; a₃₁, a₃₂, a₃₃] * !![b₁₁, b₁₂, b₁₃; b₂₁, b₂₂, b₂₃; b₃₁, b₃₂, b₃₃] = !![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃; a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃; a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]
<VAR>α : Type u<VAR>a₀ a₁ b₀ b₁ : α<VAR>h₀ : a₀ = b₀<VAR>h₁ : a₁ = b₁<GOAL>![a₀, a₁] = ![b₀, b₁]
<VAR>α : Type u<VAR>a₀ a₁ a₂ b₀ b₁ b₂ : α<VAR>h₀ : a₀ = b₀<VAR>h₁ : a₁ = b₁<VAR>h₂ : a₂ = b₂<GOAL>![a₀, a₁, a₂] = ![b₀, b₁, b₂]
<VAR>α : Type u<VAR>Add α<VAR>a₀ a₁ b₀ b₁ : α<GOAL>![a₀, a₁] + ![b₀, b₁] = ![a₀ + b₀, a₁ + b₁]
<VAR>α : Type u<VAR>Add α<VAR>a₀ a₁ a₂ b₀ b₁ b₂ : α<GOAL>![a₀, a₁, a₂] + ![b₀, b₁, b₂] = ![a₀ + b₀, a₁ + b₁, a₂ + b₂]
<VAR>α : Type u<VAR>R : Type u_1<VAR>SMul R α<VAR>x : R<VAR>a₀ a₁ : α<GOAL>x • ![a₀, a₁] = ![x • a₀, x • a₁]
<VAR>α : Type u<VAR>R : Type u_1<VAR>SMul R α<VAR>x : R<VAR>a₀ a₁ a₂ : α<GOAL>x • ![a₀, a₁, a₂] = ![x • a₀, x • a₁, x • a₂]
<VAR>α : Type u<VAR>AddCommMonoid α<VAR>Mul α<VAR>a₀ a₁ b₀ b₁ : α<GOAL>Matrix.dotProduct ![a₀, a₁] ![b₀, b₁] = a₀ * b₀ + a₁ * b₁
<VAR>α : Type u<VAR>AddCommMonoid α<VAR>Mul α<VAR>v w : Fin 2 → α<GOAL>Matrix.dotProduct v w = v 0 * w 0 + v 1 * w 1
<VAR>α : Type u<VAR>AddCommMonoid α<VAR>Mul α<VAR>a₀ a₁ a₂ b₀ b₁ b₂ : α<GOAL>Matrix.dotProduct ![a₀, a₁, a₂] ![b₀, b₁, b₂] = a₀ * b₀ + a₁ * b₁ + a₂ * b₂
<VAR>α : Type u<VAR>AddCommMonoid α<VAR>Mul α<VAR>v w : Fin 3 → α<GOAL>Matrix.dotProduct v w = v 0 * w 0 + v 1 * w 1 + v 2 * w 2
<VAR>α : Type u_1<VAR>GroupWithZero α<VAR>Fintype α<VAR>DecidableEq α<GOAL>Fintype.card α = Fintype.card αˣ + 1
<VAR>α : Type u_1<VAR>GroupWithZero α<VAR>Finite α<GOAL>Nat.card α = Nat.card αˣ + 1
<VAR>α : Type u_1<VAR>GroupWithZero α<VAR>Fintype α<VAR>DecidableEq α<GOAL>Fintype.card αˣ = Fintype.card α - 1
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>α : ι → Type u_2<VAR>S : (i : ι) → Setoid (α i)<VAR>l : List ι<VAR>f : (i : ι) → i ∈ l → α i<GOAL>(Quotient.finChoiceAux l fun i h => ⟦f i h⟧) = ⟦f⟧
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>Fintype ι<VAR>α : ι → Type u_2<VAR>(i : ι) → Setoid (α i)<VAR>f : (i : ι) → α i<GOAL>(Quotient.finChoice fun i => ⟦f i⟧) = ⟦f⟧
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>Fintype ι<VAR>α : ι → Type u_2<VAR>f : (i : ι) → α i<GOAL>(Trunc.finChoice fun i => Trunc.mk (f i)) = Trunc.mk f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Fintype α<VAR>Fintype β<GOAL>Finset.univ.disjSum Finset.univ = Finset.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<GOAL>Fintype.card (α ⊕ β) = Fintype.card α + Fintype.card β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>DecidableEq β<VAR>k : β<VAR>b : α → β<GOAL>Finset.image (fun i => b ↑i) Finset.univ = (Finset.image b Finset.univ).erase k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>DecidableEq β<VAR>k : β<VAR>b : α → β<VAR>hk : k ∈ Finset.image b Finset.univ<VAR>p : β → Prop<VAR>DecidablePred p<VAR>hp : ¬p k<GOAL>Finset.image (fun i => b ↑i) Finset.univ ⊂ Finset.image b Finset.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>DecidableEq β<VAR>t : Finset β<VAR>hαt : Fintype.card α = t.card<VAR>s : Finset α<VAR>f : α → β<VAR>hfst : Finset.image f s ⊆ t<VAR>hfs : Set.InjOn f ↑s<GOAL>∃ g, ∀ i ∈ s, ↑(g i) = f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>t : Finset β<VAR>hαt : Fintype.card α = t.card<VAR>s : Set α<VAR>f : α → β<VAR>hfst : Set.MapsTo f s ↑t<VAR>hfs : Set.InjOn f s<GOAL>∃ g, ∀ i ∈ s, ↑(g i) = f i
<VAR>α : Type u_1<VAR>p q : α → Prop<VAR>Fintype { x // p x }<VAR>Fintype { x // q x }<VAR>Fintype { x // p x ∨ q x }<GOAL>Fintype.card { x // p x ∨ q x } ≤ Fintype.card { x // p x } + Fintype.card { x // q x }
<VAR>α : Type u_1<VAR>p q : α → Prop<VAR>h : Disjoint p q<VAR>Fintype { x // p x }<VAR>Fintype { x // q x }<VAR>Fintype { x // p x ∨ q x }<GOAL>Fintype.card { x // p x ∨ q x } = Fintype.card { x // p x } + Fintype.card { x // q x }
<VAR>a : UInt64<VAR>n : ℕ<GOAL>a ^ n = { val := a.val ^ n }
<VAR>z : ℤ<VAR>a : USize<GOAL>z • a = { val := z • a.val }
<VAR>n : ℕ<GOAL>↑n = { val := ↑n }
<VAR>a : USize<GOAL>-a = { val := -a.val }
<VAR>a : UInt16<VAR>n : ℕ<GOAL>a ^ n = { val := a.val ^ n }
<VAR>a : UInt8<VAR>n : ℕ<GOAL>a ^ n = { val := a.val ^ n }
<VAR>z : ℤ<VAR>a : UInt64<GOAL>z • a = { val := z • a.val }
<VAR>z : ℤ<GOAL>↑z = { val := ↑z }
<VAR>a : UInt32<VAR>n : ℕ<GOAL>a ^ n = { val := a.val ^ n }
<VAR>n : ℕ<VAR>a : UInt16<GOAL>n • a = { val := n • a.val }
<VAR>n : ℕ<VAR>a : UInt64<GOAL>n • a = { val := n • a.val }
<VAR>a : UInt32<GOAL>-a = { val := -a.val }
<VAR>a : UInt16<GOAL>-a = { val := -a.val }
<VAR>z : ℤ<VAR>a : UInt8<GOAL>z • a = { val := z • a.val }
<VAR>n : ℕ<VAR>a : UInt8<GOAL>n • a = { val := n • a.val }
<VAR>n : ℕ<VAR>a : UInt32<GOAL>n • a = { val := n • a.val }
<VAR>z : ℤ<VAR>a : UInt16<GOAL>z • a = { val := z • a.val }
<VAR>a : USize<VAR>n : ℕ<GOAL>a ^ n = { val := a.val ^ n }
<VAR>a : UInt8<GOAL>-a = { val := -a.val }
<VAR>a : UInt64<GOAL>-a = { val := -a.val }
<VAR>n : ℕ<VAR>a : USize<GOAL>n • a = { val := n • a.val }
<VAR>z : ℤ<VAR>a : UInt32<GOAL>z • a = { val := z • a.val }
<VAR>α : Type u<VAR>β : α → Type v<VAR>l : List (Sigma β)<GOAL>(↑l).keys = ↑l.keys
<VAR>α : Type u<VAR>β : α → Type v<VAR>l : List (Sigma β)<GOAL>(↑l).NodupKeys ↔ l.NodupKeys
<VAR>α : Type u<VAR>β : α → Type v<VAR>m : Multiset ((a : α) × β a)<GOAL>m.keys.Nodup ↔ m.NodupKeys
<VAR>α : Type u<VAR>β : α → Type v<VAR>m : Multiset ((a : α) × β a)<VAR>h : m.NodupKeys<GOAL>m.Nodup
<VAR>α : Type u<VAR>β : α → Type v<VAR>self : Finmap β<GOAL>self.entries.NodupKeys
<VAR>α : Type u<VAR>β : α → Type v<VAR>s₁ s₂ : AList β<GOAL>⟦s₁⟧ = ⟦s₂⟧ ↔ s₁.entries ~ s₂.entries
<VAR>α : Type u<VAR>β : α → Type v<VAR>s : AList β<GOAL>⟦s⟧.entries = ↑s.entries
<VAR>α : Type u<VAR>β : α → Type v<VAR>f : Finmap β<GOAL>f.entries.Nodup
<VAR>α : Type u<VAR>β : α → Type v<VAR>γ : Type u_1<VAR>s : AList β<VAR>f : AList β → γ<VAR>H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b<GOAL>⟦s⟧.liftOn f H = f s
<VAR>α : Type u<VAR>β : α → Type v<VAR>γ : Type u_1<VAR>s₁ s₂ : AList β<VAR>f : AList β → AList β → γ<VAR>H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries ~ a₂.entries → b₁.entries ~ b₂.entries → f a₁ b₁ = f a₂ b₂<GOAL>⟦s₁⟧.liftOn₂ ⟦s₂⟧ f H = f s₁ s₂
<VAR>α : Type u<VAR>β : α → Type v<VAR>C : Finmap β → Prop<VAR>s : Finmap β<VAR>H : ∀ (a : AList β), C ⟦a⟧<GOAL>C s
<VAR>α : Type u<VAR>β : α → Type v<VAR>C : Finmap β → Finmap β → Prop<VAR>s₁ s₂ : Finmap β<VAR>H : ∀ (a₁ a₂ : AList β), C ⟦a₁⟧ ⟦a₂⟧<GOAL>C s₁ s₂
<VAR>α : Type u<VAR>β : α → Type v<VAR>C : Finmap β → Finmap β → Finmap β → Prop<VAR>s₁ s₂ s₃ : Finmap β<VAR>H : ∀ (a₁ a₂ a₃ : AList β), C ⟦a₁⟧ ⟦a₂⟧ ⟦a₃⟧<GOAL>C s₁ s₂ s₃
<VAR>α : Type u<VAR>β : α → Type v<VAR>s t : Finmap β<GOAL>s.entries = t.entries → s = t
<VAR>α : Type u<VAR>β : α → Type v<VAR>s t : Finmap β<GOAL>s = t ↔ s.entries = t.entries
<VAR>α : Type u<VAR>β : α → Type v<VAR>s t : Finmap β<GOAL>s.entries = t.entries ↔ s = t
<VAR>α : Type u<VAR>β : α → Type v<VAR>a : α<VAR>s : Finmap β<GOAL>a ∈ s ↔ a ∈ s.entries.keys
<VAR>α : Type u<VAR>β : α → Type v<VAR>a : α<VAR>s : AList β<GOAL>a ∈ ⟦s⟧ ↔ a ∈ s
<VAR>α : Type u<VAR>β : α → Type v<VAR>s : AList β<GOAL>⟦s⟧.keys.val = ↑s.keys
<VAR>α : Type u<VAR>β : α → Type v<VAR>s₁ s₂ : AList β<GOAL>⟦s₁⟧.keys = ⟦s₂⟧.keys ↔ s₁.keys ~ s₂.keys
<VAR>α : Type u<VAR>β : α → Type v<VAR>a : α<VAR>s : Finmap β<GOAL>a ∈ s.keys ↔ a ∈ s
<VAR>α : Type u<VAR>β : α → Type v<GOAL>⟦∅⟧ = ∅
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<GOAL>[].toFinmap = ∅
<VAR>α : Type u<VAR>β : α → Type v<GOAL>∅.keys = ∅
<VAR>α : Type u<VAR>β : α → Type v<VAR>a : α<VAR>b : β a<GOAL>(Finmap.singleton a b).keys = {a}
<VAR>α : Type u<VAR>β : α → Type v<VAR>x y : α<VAR>b : β y<GOAL>x ∈ Finmap.singleton y b ↔ x = y
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>s : AList β<GOAL>Finmap.lookup a ⟦s⟧ = AList.lookup a s
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>s : List (Sigma β)<GOAL>Finmap.lookup a s.toFinmap = List.dlookup a s
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<GOAL>Finmap.lookup a ∅ = none
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>s : Finmap β<GOAL>(Finmap.lookup a s).isSome = true ↔ a ∈ s
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>s : Finmap β<GOAL>Finmap.lookup a s = none ↔ a ∉ s
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>s : Finmap β<VAR>a : α<VAR>b : β a<GOAL>b ∈ Finmap.lookup a s ↔ ⟨a, b⟩ ∈ s.entries
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>s : Finmap β<VAR>a : α<VAR>b : β a<GOAL>Finmap.lookup a s = some b ↔ ⟨a, b⟩ ∈ s.entries
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>s : Finmap β<GOAL>(s.keys.sigma fun i => (Finmap.lookup i s).toFinset) = { val := s.entries, nodup := ⋯ }
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<GOAL>Finmap.lookup a (Finmap.singleton a b) = some b
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>s : Finmap β<GOAL>a ∈ s ↔ ∃ b, Finmap.lookup a s = some b
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>s : Finmap β<VAR>h : Finmap.lookup a s = some b<GOAL>a ∈ s
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>s₁ s₂ : Finmap β<GOAL>(∀ (x : α), Finmap.lookup x s₁ = Finmap.lookup x s₂) → s₁ = s₂
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>s : Finmap β<GOAL>(↑(Finmap.keysLookupEquiv s)).1 = s.keys
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>s : Finmap β<VAR>i : α<GOAL>(↑(Finmap.keysLookupEquiv s)).2 i = Finmap.lookup i s
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>f : { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }<GOAL>(Finmap.keysLookupEquiv.symm f).keys = (↑f).1
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>f : { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }<VAR>a : α<GOAL>Finmap.lookup a (Finmap.keysLookupEquiv.symm f) = (↑f).2 a
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>s : AList β<GOAL>Finmap.replace a b ⟦s⟧ = ⟦AList.replace a b s⟧
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>s : Finmap β<GOAL>(Finmap.replace a b s).keys = s.keys
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a a' : α<VAR>b : β a<VAR>s : Finmap β<GOAL>a' ∈ Finmap.replace a b s ↔ a' ∈ s
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>s : AList β<GOAL>Finmap.erase a ⟦s⟧ = ⟦AList.erase a s⟧
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>s : AList β<GOAL>⟦AList.erase a s⟧.keys = ⟦s⟧.keys.erase a
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>s : Finmap β<GOAL>(Finmap.erase a s).keys = s.keys.erase a
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a a' : α<VAR>s : Finmap β<GOAL>a' ∈ Finmap.erase a s ↔ a' ≠ a ∧ a' ∈ s
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>s : Finmap β<GOAL>a ∉ Finmap.erase a s
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>s : Finmap β<GOAL>Finmap.lookup a (Finmap.erase a s) = none