ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Finite β<VAR>Nonempty α<VAR>Preorder α<VAR>IsDirected α fun x x_1 => x ≥ x_1<VAR>f : β → α<GOAL>∃ M, ∀ (i : β), M ≤ f i
<VAR>α : Type u_1<VAR>Nonempty α<VAR>Preorder α<VAR>IsDirected α fun x x_1 => x ≤ x_1<VAR>s : Set α<VAR>hs : s.Finite<GOAL>∃ M, ∀ i ∈ s, i ≤ M
<VAR>α : Type u_1<VAR>Nonempty α<VAR>Preorder α<VAR>IsDirected α fun x x_1 => x ≥ x_1<VAR>s : Set α<VAR>hs : s.Finite<GOAL>∃ M, ∀ i ∈ s, M ≤ i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Finite β<VAR>Nonempty α<VAR>Preorder α<VAR>IsDirected α fun x x_1 => x ≤ x_1<VAR>f : β → α<GOAL>BddAbove (Set.range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Finite β<VAR>Nonempty α<VAR>Preorder α<VAR>IsDirected α fun x x_1 => x ≥ x_1<VAR>f : β → α<GOAL>BddBelow (Set.range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Unique α<VAR>Fintype β<VAR>Fintype (α ↪ β)<GOAL>‖α ↪ β‖ = ‖β‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>emb : Fintype (α ↪ β)<GOAL>‖α ↪ β‖ = ‖β‖.descFactorial ‖α‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Infinite α<VAR>Fintype β<VAR>Fintype (α ↪ β)<GOAL>‖α ↪ β‖ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>Fintype ↑s<VAR>Fintype ↑t<VAR>Fintype ↑(s ×ˢ t)<GOAL>(s ×ˢ t).toFinset = s.toFinset ×ˢ t.toFinset
<VAR>α : Type u_1<VAR>s : Set α<VAR>DecidableEq α<VAR>Fintype ↑s<VAR>Fintype ↑s.offDiag<GOAL>s.offDiag.toFinset = s.toFinset.offDiag
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<GOAL>Finset.univ ×ˢ Finset.univ = Finset.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>s : Finset α<VAR>t : Finset β<VAR>Nonempty α<VAR>Nonempty β<GOAL>s ×ˢ t = Finset.univ ↔ s = Finset.univ ∧ t = Finset.univ
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>Fintype α<VAR>Fintype β<GOAL>Fintype.card (α × β) = Fintype.card α * Fintype.card β
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Infinite (α × β) ↔ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β
<VAR>ι : Sort u_4<VAR>π : ι → Sort u_5<VAR>i : ι<VAR>Infinite (π i)<VAR>∀ (i : ι), Nonempty (π i)<GOAL>Infinite ((i : ι) → π i)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>δ : α → Type u_3<VAR>t : (a : α) → Finset (δ a)<VAR>f : (a : α) → δ a<GOAL>f ∈ Fintype.piFinset t ↔ ∀ (a : α), f a ∈ t a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>δ : α → Type u_3<VAR>t : (a : α) → Finset (δ a)<GOAL>↑(Fintype.piFinset t) = Set.univ.pi fun a => ↑(t a)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>δ : α → Type u_3<VAR>t₁ t₂ : (a : α) → Finset (δ a)<VAR>h : ∀ (a : α), t₁ a ⊆ t₂ a<GOAL>Fintype.piFinset t₁ ⊆ Fintype.piFinset t₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>δ : α → Type u_3<VAR>Nonempty α<GOAL>(Fintype.piFinset fun x => ∅) = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>γ : α → Type u_2<VAR>s : (a : α) → Finset (γ a)<GOAL>(Fintype.piFinset s).Nonempty ↔ ∀ (a : α), (s a).Nonempty
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>Fintype ι<VAR>DecidableEq ι<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>(Fintype.piFinset fun x => s).Nonempty
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>γ : α → Type u_2<VAR>IsEmpty α<VAR>s : (a : α) → Finset (γ a)<GOAL>Fintype.piFinset s = Finset.univ
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>δ : α → Type u_3<VAR>f : (i : α) → δ i<GOAL>(Fintype.piFinset fun i => {f i}) = {f}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>δ : α → Type u_3<VAR>f : (i : α) → Finset (δ i)<VAR>hf : ∀ (i : α), (↑(f i)).Subsingleton<GOAL>(↑(Fintype.piFinset f)).Subsingleton
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>δ : α → Type u_3<VAR>t₁ t₂ : (a : α) → Finset (δ a)<VAR>a : α<VAR>h : Disjoint (t₁ a) (t₂ a)<GOAL>Disjoint (Fintype.piFinset t₁) (Fintype.piFinset t₂)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>γ : α → Type u_2<VAR>δ : α → Type u_3<VAR>(a : α) → DecidableEq (δ a)<VAR>f : (a : α) → γ a → δ a<VAR>s : (a : α) → Finset (γ a)<GOAL>(Fintype.piFinset fun a => Finset.image (f a) (s a)) = Finset.image (fun b a => f a (b a)) (Fintype.piFinset s)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>δ : α → Type u_3<VAR>t : (a : α) → Finset (δ a)<VAR>a : α<VAR>DecidableEq (δ a)<GOAL>Finset.image (fun f => f a) (Fintype.piFinset t) ⊆ t a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>δ : α → Type u_3<VAR>t : (a : α) → Finset (δ a)<VAR>a : α<VAR>DecidableEq (δ a)<VAR>ht : ∀ (b : α), a ≠ b → (t b).Nonempty<GOAL>Finset.image (fun f => f a) (Fintype.piFinset t) = t a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>β : Type u_4<VAR>DecidableEq β<VAR>t : Finset β<VAR>a : α<GOAL>Finset.image (fun f => f a) (Fintype.piFinset fun _i => t) = t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>δ : α → Type u_3<VAR>(a : α) → DecidableEq (δ a)<VAR>t : (a : α) → Finset (δ a)<VAR>a : α<VAR>x : δ a<VAR>hx : x ∉ t a<GOAL>Finset.filter (fun x_1 => x_1 a = x) (Fintype.piFinset t) = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>δ : α → Type u_3<VAR>(a : α) → DecidableEq (δ a)<VAR>s : (i : α) → Finset (δ i)<VAR>i : α<VAR>t : Finset (δ i)<VAR>hts : t ⊆ s i<GOAL>Fintype.piFinset (Function.update s i t) = Finset.filter (fun f => f i ∈ t) (Fintype.piFinset s)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>δ : α → Type u_3<VAR>(a : α) → DecidableEq (δ a)<VAR>s : (i : α) → Finset (δ i)<VAR>i : α<VAR>a : δ i<VAR>ha : a ∈ s i<GOAL>Fintype.piFinset (Function.update s i {a}) = Finset.filter (fun f => f i = a) (Fintype.piFinset s)
<VAR>α : Type u_2<VAR>β : α → Type u_3<VAR>DecidableEq α<VAR>Fintype α<VAR>(a : α) → Fintype (β a)<GOAL>(Fintype.piFinset fun a => Finset.univ) = Finset.univ
<VAR>α : Type u_2<VAR>β : α → Type u_3<VAR>DecidableEq α<VAR>Fintype α<VAR>(a : α) → Fintype (β a)<GOAL>(Finset.univ.pi fun a => Finset.univ) = Finset.univ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>DecidableEq (ι → α)<VAR>s : Finset α<VAR>DecidableEq ι<VAR>Fintype ι<GOAL>Finset.filter (fun x => ∃ a ∈ s, Function.const ι a = x) (Fintype.piFinset fun x => s) = s.piDiag ι
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>DecidableEq (ι → α)<VAR>s : Finset α<VAR>DecidableEq ι<VAR>Fintype ι<GOAL>s.piDiag ι ⊆ Fintype.piFinset fun x => s
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_12<VAR>Fintype m<VAR>Fintype n<VAR>Mul α<VAR>AddCommMonoid α<VAR>v w : m ⊕ n → α<GOAL>v ⬝ᵥ w = v ∘ Sum.inl ⬝ᵥ w ∘ Sum.inl + v ∘ Sum.inr ⬝ᵥ w ∘ Sum.inr
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>A : Matrix n l α<VAR>B : Matrix n m α<VAR>C : Matrix o l α<VAR>D : Matrix o m α<VAR>i : n<VAR>j : l<GOAL>Matrix.fromBlocks A B C D (Sum.inl i) (Sum.inl j) = A i j
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>A : Matrix n l α<VAR>B : Matrix n m α<VAR>C : Matrix o l α<VAR>D : Matrix o m α<VAR>i : n<VAR>j : m<GOAL>Matrix.fromBlocks A B C D (Sum.inl i) (Sum.inr j) = B i j
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>A : Matrix n l α<VAR>B : Matrix n m α<VAR>C : Matrix o l α<VAR>D : Matrix o m α<VAR>i : o<VAR>j : l<GOAL>Matrix.fromBlocks A B C D (Sum.inr i) (Sum.inl j) = C i j
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>A : Matrix n l α<VAR>B : Matrix n m α<VAR>C : Matrix o l α<VAR>D : Matrix o m α<VAR>i : o<VAR>j : m<GOAL>Matrix.fromBlocks A B C D (Sum.inr i) (Sum.inr j) = D i j
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>M : Matrix (n ⊕ o) (l ⊕ m) α<GOAL>Matrix.fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ = M
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>A : Matrix n l α<VAR>B : Matrix n m α<VAR>C : Matrix o l α<VAR>D : Matrix o m α<GOAL>(Matrix.fromBlocks A B C D).toBlocks₁₁ = A
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>A : Matrix n l α<VAR>B : Matrix n m α<VAR>C : Matrix o l α<VAR>D : Matrix o m α<GOAL>(Matrix.fromBlocks A B C D).toBlocks₁₂ = B
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>A : Matrix n l α<VAR>B : Matrix n m α<VAR>C : Matrix o l α<VAR>D : Matrix o m α<GOAL>(Matrix.fromBlocks A B C D).toBlocks₂₁ = C
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>A : Matrix n l α<VAR>B : Matrix n m α<VAR>C : Matrix o l α<VAR>D : Matrix o m α<GOAL>(Matrix.fromBlocks A B C D).toBlocks₂₂ = D
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>A B : Matrix (n ⊕ o) (l ⊕ m) α<GOAL>A = B ↔ A.toBlocks₁₁ = B.toBlocks₁₁ ∧ A.toBlocks₁₂ = B.toBlocks₁₂ ∧ A.toBlocks₂₁ = B.toBlocks₂₁ ∧ A.toBlocks₂₂ = B.toBlocks₂₂
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>A : Matrix n l α<VAR>B : Matrix n m α<VAR>C : Matrix o l α<VAR>D : Matrix o m α<VAR>A' : Matrix n l α<VAR>B' : Matrix n m α<VAR>C' : Matrix o l α<VAR>D' : Matrix o m α<GOAL>Matrix.fromBlocks A B C D = Matrix.fromBlocks A' B' C' D' ↔ A = A' ∧ B = B' ∧ C = C' ∧ D = D'
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>β : Type u_13<VAR>A : Matrix n l α<VAR>B : Matrix n m α<VAR>C : Matrix o l α<VAR>D : Matrix o m α<VAR>f : α → β<GOAL>(Matrix.fromBlocks A B C D).map f = Matrix.fromBlocks (A.map f) (B.map f) (C.map f) (D.map f)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>A : Matrix n l α<VAR>B : Matrix n m α<VAR>C : Matrix o l α<VAR>D : Matrix o m α<GOAL>(Matrix.fromBlocks A B C D)ᵀ = Matrix.fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>Star α<VAR>A : Matrix n l α<VAR>B : Matrix n m α<VAR>C : Matrix o l α<VAR>D : Matrix o m α<GOAL>(Matrix.fromBlocks A B C D)ᴴ = Matrix.fromBlocks Aᴴ Cᴴ Bᴴ Dᴴ
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>α : Type u_12<VAR>A : Matrix n l α<VAR>B : Matrix n m α<VAR>C : Matrix o l α<VAR>D : Matrix o m α<VAR>f : p → l ⊕ m<GOAL>(Matrix.fromBlocks A B C D).submatrix Sum.swap f = (Matrix.fromBlocks C D A B).submatrix id f
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>α : Type u_12<VAR>A : Matrix n l α<VAR>B : Matrix n m α<VAR>C : Matrix o l α<VAR>D : Matrix o m α<VAR>f : p → n ⊕ o<GOAL>(Matrix.fromBlocks A B C D).submatrix f Sum.swap = (Matrix.fromBlocks B A D C).submatrix f id
<VAR>l : Type u_14<VAR>m : Type u_15<VAR>n : Type u_16<VAR>o : Type u_17<VAR>α : Type u_18<VAR>A : Matrix n l α<VAR>B : Matrix n m α<VAR>C : Matrix o l α<VAR>D : Matrix o m α<GOAL>(Matrix.fromBlocks A B C D).submatrix Sum.swap Sum.swap = Matrix.fromBlocks D C B A
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_12<VAR>M : Matrix m n α<VAR>p : m → Prop<VAR>q : n → Prop<VAR>i : { a // p a }<VAR>j : { a // q a }<GOAL>M.toBlock p q i j = M ↑i ↑j
<VAR>m : Type u_2<VAR>α : Type u_12<VAR>M : Matrix m m α<VAR>p : m → Prop<GOAL>M.toSquareBlockProp p = Matrix.of fun i j => M ↑i ↑j
<VAR>m : Type u_2<VAR>α : Type u_12<VAR>β : Type u_13<VAR>M : Matrix m m α<VAR>b : m → β<VAR>k : β<GOAL>M.toSquareBlock b k = Matrix.of fun i j => M ↑i ↑j
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_10<VAR>α : Type u_12<VAR>SMul R α<VAR>x : R<VAR>A : Matrix n l α<VAR>B : Matrix n m α<VAR>C : Matrix o l α<VAR>D : Matrix o m α<GOAL>x • Matrix.fromBlocks A B C D = Matrix.fromBlocks (x • A) (x • B) (x • C) (x • D)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_10<VAR>Neg R<VAR>A : Matrix n l R<VAR>B : Matrix n m R<VAR>C : Matrix o l R<VAR>D : Matrix o m R<GOAL>-Matrix.fromBlocks A B C D = Matrix.fromBlocks (-A) (-B) (-C) (-D)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>Zero α<GOAL>Matrix.fromBlocks 0 0 0 0 = 0
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>Add α<VAR>A : Matrix n l α<VAR>B : Matrix n m α<VAR>C : Matrix o l α<VAR>D : Matrix o m α<VAR>A' : Matrix n l α<VAR>B' : Matrix n m α<VAR>C' : Matrix o l α<VAR>D' : Matrix o m α<GOAL>Matrix.fromBlocks A B C D + Matrix.fromBlocks A' B' C' D' = Matrix.fromBlocks (A + A') (B + B') (C + C') (D + D')
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>α : Type u_12<VAR>Fintype l<VAR>Fintype m<VAR>NonUnitalNonAssocSemiring α<VAR>A : Matrix n l α<VAR>B : Matrix n m α<VAR>C : Matrix o l α<VAR>D : Matrix o m α<VAR>A' : Matrix l p α<VAR>B' : Matrix l q α<VAR>C' : Matrix m p α<VAR>D' : Matrix m q α<GOAL>Matrix.fromBlocks A B C D * Matrix.fromBlocks A' B' C' D' = Matrix.fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D')
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>Fintype l<VAR>Fintype m<VAR>NonUnitalNonAssocSemiring α<VAR>A : Matrix n l α<VAR>B : Matrix n m α<VAR>C : Matrix o l α<VAR>D : Matrix o m α<VAR>x : l ⊕ m → α<GOAL>Matrix.fromBlocks A B C D *ᵥ x = Sum.elim (A *ᵥ x ∘ Sum.inl + B *ᵥ x ∘ Sum.inr) (C *ᵥ x ∘ Sum.inl + D *ᵥ x ∘ Sum.inr)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>Fintype n<VAR>Fintype o<VAR>NonUnitalNonAssocSemiring α<VAR>A : Matrix n l α<VAR>B : Matrix n m α<VAR>C : Matrix o l α<VAR>D : Matrix o m α<VAR>x : n ⊕ o → α<GOAL>x ᵥ* Matrix.fromBlocks A B C D = Sum.elim (x ∘ Sum.inl ᵥ* A + x ∘ Sum.inr ᵥ* C) (x ∘ Sum.inl ᵥ* B + x ∘ Sum.inr ᵥ* D)
<VAR>m : Type u_2<VAR>α : Type u_12<VAR>DecidableEq m<VAR>Zero α<VAR>d : m → α<VAR>p : m → Prop<GOAL>(Matrix.diagonal d).toBlock p p = Matrix.diagonal fun i => d ↑i
<VAR>m : Type u_2<VAR>α : Type u_12<VAR>DecidableEq m<VAR>Zero α<VAR>d : m → α<VAR>p q : m → Prop<VAR>hpq : Disjoint p q<GOAL>(Matrix.diagonal d).toBlock p q = 0
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>α : Type u_12<VAR>DecidableEq l<VAR>DecidableEq m<VAR>Zero α<VAR>d₁ : l → α<VAR>d₂ : m → α<GOAL>Matrix.fromBlocks (Matrix.diagonal d₁) 0 0 (Matrix.diagonal d₂) = Matrix.diagonal (Sum.elim d₁ d₂)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>α : Type u_12<VAR>DecidableEq l<VAR>DecidableEq m<VAR>Zero α<VAR>v : l ⊕ m → α<GOAL>(Matrix.diagonal v).toBlocks₁₁ = Matrix.diagonal fun i => v (Sum.inl i)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>α : Type u_12<VAR>DecidableEq l<VAR>DecidableEq m<VAR>Zero α<VAR>v : l ⊕ m → α<GOAL>(Matrix.diagonal v).toBlocks₂₂ = Matrix.diagonal fun i => v (Sum.inr i)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>α : Type u_12<VAR>DecidableEq l<VAR>DecidableEq m<VAR>Zero α<VAR>v : l ⊕ m → α<GOAL>(Matrix.diagonal v).toBlocks₁₂ = 0
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>α : Type u_12<VAR>DecidableEq l<VAR>DecidableEq m<VAR>Zero α<VAR>v : l ⊕ m → α<GOAL>(Matrix.diagonal v).toBlocks₂₁ = 0
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>α : Type u_12<VAR>DecidableEq l<VAR>DecidableEq m<VAR>Zero α<VAR>One α<GOAL>Matrix.fromBlocks 1 0 0 1 = 1
<VAR>m : Type u_2<VAR>α : Type u_12<VAR>DecidableEq m<VAR>Zero α<VAR>One α<VAR>p : m → Prop<GOAL>Matrix.toBlock 1 p p = 1
<VAR>m : Type u_2<VAR>α : Type u_12<VAR>DecidableEq m<VAR>Zero α<VAR>One α<VAR>p q : m → Prop<VAR>hpq : Disjoint p q<GOAL>Matrix.toBlock 1 p q = 0
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>DecidableEq o<VAR>Zero α<VAR>M : o → Matrix m n α<VAR>i : m<VAR>k : o<VAR>j : n<VAR>k' : o<GOAL>Matrix.blockDiagonal M (i, k) (j, k') = if k = k' then M k i j else 0
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>DecidableEq o<VAR>Zero α<VAR>M : o → Matrix m n α<VAR>ik : m × o<VAR>jk : n × o<GOAL>Matrix.blockDiagonal M ik jk = if ik.2 = jk.2 then M ik.2 ik.1 jk.1 else 0
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>DecidableEq o<VAR>Zero α<VAR>M : o → Matrix m n α<VAR>i : m<VAR>j : n<VAR>k : o<GOAL>Matrix.blockDiagonal M (i, k) (j, k) = M k i j
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>DecidableEq o<VAR>Zero α<VAR>M : o → Matrix m n α<VAR>i : m<VAR>j : n<VAR>k k' : o<VAR>h : k ≠ k'<GOAL>Matrix.blockDiagonal M (i, k) (j, k') = 0
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>β : Type u_13<VAR>DecidableEq o<VAR>Zero α<VAR>Zero β<VAR>M : o → Matrix m n α<VAR>f : α → β<VAR>hf : f 0 = 0<GOAL>(Matrix.blockDiagonal M).map f = Matrix.blockDiagonal fun k => (M k).map f
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>DecidableEq o<VAR>Zero α<VAR>M : o → Matrix m n α<GOAL>(Matrix.blockDiagonal M)ᵀ = Matrix.blockDiagonal fun k => (M k)ᵀ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>DecidableEq o<VAR>α : Type u_14<VAR>AddMonoid α<VAR>StarAddMonoid α<VAR>M : o → Matrix m n α<GOAL>(Matrix.blockDiagonal M)ᴴ = Matrix.blockDiagonal fun k => (M k)ᴴ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>DecidableEq o<VAR>Zero α<GOAL>Matrix.blockDiagonal 0 = 0
<VAR>m : Type u_2<VAR>o : Type u_4<VAR>α : Type u_12<VAR>DecidableEq o<VAR>Zero α<VAR>DecidableEq m<VAR>d : o → m → α<GOAL>(Matrix.blockDiagonal fun k => Matrix.diagonal (d k)) = Matrix.diagonal fun ik => d ik.2 ik.1
<VAR>m : Type u_2<VAR>o : Type u_4<VAR>α : Type u_12<VAR>DecidableEq o<VAR>Zero α<VAR>DecidableEq m<VAR>One α<GOAL>Matrix.blockDiagonal 1 = 1
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>DecidableEq o<VAR>AddZeroClass α<VAR>M N : o → Matrix m n α<GOAL>Matrix.blockDiagonal (M + N) = Matrix.blockDiagonal M + Matrix.blockDiagonal N
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>DecidableEq o<VAR>AddZeroClass α<VAR>M : o → Matrix m n α<GOAL>(Matrix.blockDiagonalAddMonoidHom m n o α) M = Matrix.blockDiagonal M
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>DecidableEq o<VAR>AddGroup α<VAR>M : o → Matrix m n α<GOAL>Matrix.blockDiagonal (-M) = -Matrix.blockDiagonal M
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>DecidableEq o<VAR>AddGroup α<VAR>M N : o → Matrix m n α<GOAL>Matrix.blockDiagonal (M - N) = Matrix.blockDiagonal M - Matrix.blockDiagonal N
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>α : Type u_12<VAR>DecidableEq o<VAR>Fintype n<VAR>Fintype o<VAR>NonUnitalNonAssocSemiring α<VAR>M : o → Matrix m n α<VAR>N : o → Matrix n p α<GOAL>(Matrix.blockDiagonal fun k => M k * N k) = Matrix.blockDiagonal M * Matrix.blockDiagonal N
<VAR>m : Type u_2<VAR>o : Type u_4<VAR>α : Type u_12<VAR>DecidableEq o<VAR>DecidableEq m<VAR>Fintype o<VAR>Fintype m<VAR>NonAssocSemiring α<VAR>M : o → Matrix m m α<GOAL>(Matrix.blockDiagonalRingHom m o α) M = Matrix.blockDiagonal M
<VAR>m : Type u_2<VAR>o : Type u_4<VAR>α : Type u_12<VAR>DecidableEq o<VAR>DecidableEq m<VAR>Fintype o<VAR>Fintype m<VAR>Semiring α<VAR>M : o → Matrix m m α<VAR>n : ℕ<GOAL>Matrix.blockDiagonal (M ^ n) = Matrix.blockDiagonal M ^ n
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>DecidableEq o<VAR>R : Type u_14<VAR>Monoid R<VAR>AddMonoid α<VAR>DistribMulAction R α<VAR>x : R<VAR>M : o → Matrix m n α<GOAL>Matrix.blockDiagonal (x • M) = x • Matrix.blockDiagonal M
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>M : Matrix (m × o) (n × o) α<VAR>k : o<VAR>i : m<VAR>j : n<GOAL>M.blockDiag k i j = M (i, k) (j, k)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>β : Type u_13<VAR>M : Matrix (m × o) (n × o) α<VAR>f : α → β<GOAL>(M.map f).blockDiag = fun k => (M.blockDiag k).map f
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>M : Matrix (m × o) (n × o) α<VAR>k : o<GOAL>Mᵀ.blockDiag k = (M.blockDiag k)ᵀ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_14<VAR>AddMonoid α<VAR>StarAddMonoid α<VAR>M : Matrix (m × o) (n × o) α<VAR>k : o<GOAL>Mᴴ.blockDiag k = (M.blockDiag k)ᴴ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>Zero α<GOAL>Matrix.blockDiag 0 = 0
<VAR>m : Type u_2<VAR>o : Type u_4<VAR>α : Type u_12<VAR>Zero α<VAR>DecidableEq o<VAR>DecidableEq m<VAR>d : m × o → α<VAR>k : o<GOAL>(Matrix.diagonal d).blockDiag k = Matrix.diagonal fun i => d (i, k)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>Zero α<VAR>DecidableEq o<VAR>M : o → Matrix m n α<GOAL>(Matrix.blockDiagonal M).blockDiag = M
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>Zero α<VAR>DecidableEq o<GOAL>Function.Injective Matrix.blockDiagonal
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>Zero α<VAR>DecidableEq o<VAR>M N : o → Matrix m n α<GOAL>Matrix.blockDiagonal M = Matrix.blockDiagonal N ↔ M = N
<VAR>m : Type u_2<VAR>o : Type u_4<VAR>α : Type u_12<VAR>Zero α<VAR>DecidableEq o<VAR>DecidableEq m<VAR>One α<GOAL>Matrix.blockDiag 1 = 1
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>AddZeroClass α<VAR>M N : Matrix (m × o) (n × o) α<GOAL>(M + N).blockDiag = M.blockDiag + N.blockDiag
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>AddZeroClass α<VAR>M : Matrix (m × o) (n × o) α<VAR>k : o<GOAL>(Matrix.blockDiagAddMonoidHom m n o α) M k = M.blockDiag k
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>AddGroup α<VAR>M : Matrix (m × o) (n × o) α<GOAL>(-M).blockDiag = -M.blockDiag
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>AddGroup α<VAR>M N : Matrix (m × o) (n × o) α<GOAL>(M - N).blockDiag = M.blockDiag - N.blockDiag
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>R : Type u_14<VAR>Monoid R<VAR>AddMonoid α<VAR>DistribMulAction R α<VAR>x : R<VAR>M : Matrix (m × o) (n × o) α<GOAL>(x • M).blockDiag = x • M.blockDiag
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>α : Type u_12<VAR>DecidableEq o<VAR>Zero α<VAR>M : (i : o) → Matrix (m' i) (n' i) α<VAR>k : o<VAR>i : m' k<VAR>k' : o<VAR>j : n' k'<GOAL>Matrix.blockDiagonal' M ⟨k, i⟩ ⟨k', j⟩ = if h : k = k' then M k i (cast ⋯ j) else 0
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>DecidableEq o<VAR>Zero α<VAR>M : o → Matrix m n α<VAR>k k' : o<VAR>i : m<VAR>j : n<GOAL>Matrix.blockDiagonal M (i, k) (j, k') = Matrix.blockDiagonal' M ⟨k, i⟩ ⟨k', j⟩
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type u_12<VAR>DecidableEq o<VAR>Zero α<VAR>M : o → Matrix m n α<GOAL>(Matrix.blockDiagonal' M).submatrix (Prod.toSigma ∘ Prod.swap) (Prod.toSigma ∘ Prod.swap) = Matrix.blockDiagonal M
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>α : Type u_12<VAR>DecidableEq o<VAR>Zero α<VAR>M : (i : o) → Matrix (m' i) (n' i) α<VAR>ik : (i : o) × m' i<VAR>jk : (i : o) × n' i<GOAL>Matrix.blockDiagonal' M ik jk = if h : ik.fst = jk.fst then M ik.fst ik.snd (cast ⋯ jk.snd) else 0
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>α : Type u_12<VAR>DecidableEq o<VAR>Zero α<VAR>M : (i : o) → Matrix (m' i) (n' i) α<VAR>k : o<VAR>i : m' k<VAR>j : n' k<GOAL>Matrix.blockDiagonal' M ⟨k, i⟩ ⟨k, j⟩ = M k i j
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>α : Type u_12<VAR>DecidableEq o<VAR>Zero α<VAR>M : (i : o) → Matrix (m' i) (n' i) α<VAR>k k' : o<VAR>i : m' k<VAR>j : n' k'<VAR>h : k ≠ k'<GOAL>Matrix.blockDiagonal' M ⟨k, i⟩ ⟨k', j⟩ = 0
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>α : Type u_12<VAR>β : Type u_13<VAR>DecidableEq o<VAR>Zero α<VAR>Zero β<VAR>M : (i : o) → Matrix (m' i) (n' i) α<VAR>f : α → β<VAR>hf : f 0 = 0<GOAL>(Matrix.blockDiagonal' M).map f = Matrix.blockDiagonal' fun k => (M k).map f
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>α : Type u_12<VAR>DecidableEq o<VAR>Zero α<VAR>M : (i : o) → Matrix (m' i) (n' i) α<GOAL>(Matrix.blockDiagonal' M)ᵀ = Matrix.blockDiagonal' fun k => (M k)ᵀ
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>DecidableEq o<VAR>α : Type u_14<VAR>AddMonoid α<VAR>StarAddMonoid α<VAR>M : (i : o) → Matrix (m' i) (n' i) α<GOAL>(Matrix.blockDiagonal' M)ᴴ = Matrix.blockDiagonal' fun k => (M k)ᴴ
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>α : Type u_12<VAR>DecidableEq o<VAR>Zero α<GOAL>Matrix.blockDiagonal' 0 = 0
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>α : Type u_12<VAR>DecidableEq o<VAR>Zero α<VAR>(i : o) → DecidableEq (m' i)<VAR>d : (i : o) → m' i → α<GOAL>(Matrix.blockDiagonal' fun k => Matrix.diagonal (d k)) = Matrix.diagonal fun ik => d ik.fst ik.snd