ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>C : {n : ℕ} → Vector3 α n → Sort u_2<VAR>H0 : C []<VAR>Hs : {n : ℕ} → (a : α) → (w : Vector3 α n) → C w → C (Vector3.cons a w)<VAR>n : ℕ<VAR>a : α<VAR>v : Vector3 α n<GOAL>(Vector3.cons a v).recOn H0 Hs = Hs a v (v.recOn H0 Hs)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>w : Vector3 α n<GOAL>[].append w = w
<VAR>α : Type u_1<VAR>m n : ℕ<VAR>a : α<VAR>v : Vector3 α m<VAR>w : Vector3 α n<GOAL>(Vector3.cons a v).append w = Vector3.cons a (v.append w)
<VAR>α : Type u_1<VAR>m : ℕ<VAR>i : Fin2 m<VAR>v : Vector3 α m<VAR>n : ℕ<VAR>w : Vector3 α n<GOAL>v.append w (Fin2.left n i) = v i
<VAR>α : Type u_1<VAR>m : ℕ<VAR>v : Vector3 α m<VAR>n : ℕ<VAR>w : Vector3 α n<VAR>i : Fin2 n<GOAL>v.append w (i.add m) = w i
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a : α<VAR>v : Vector3 α n<GOAL>Vector3.insert a v Fin2.fz = Vector3.cons a v
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a b : α<VAR>v : Vector3 α n<VAR>i : Fin2 (n + 1)<GOAL>Vector3.insert a (Vector3.cons b v) i.fs = Vector3.cons b (Vector3.insert a v i)
<VAR>α : Type u_1<VAR>m n : ℕ<VAR>a : α<VAR>t : Vector3 α m<VAR>v : Vector3 α n<VAR>i : Fin2 (n + 1)<VAR>e : n + 1 + m = n + m + 1<GOAL>Vector3.insert a (t.append v) (Eq.recOn e (i.add m)) = Eq.recOn e (t.append (Vector3.insert a v i))
<VAR>α : Type u_1<VAR>f : Vector3 α 0 → Prop<GOAL>Exists f ↔ f []
<VAR>α : Type u_1<VAR>n : ℕ<VAR>f : Vector3 α n.succ → Prop<GOAL>Exists f ↔ ∃ x v, f (Vector3.cons x v)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>f : Vector3 α n → Prop<GOAL>VectorEx n f ↔ Exists f
<VAR>α : Type u_1<VAR>n : ℕ<VAR>f : Vector3 α n → Prop<GOAL>VectorAll n f ↔ ∀ (v : Vector3 α n), f v
<VAR>α : Type u_1<VAR>p : α → Prop<GOAL>VectorAllP p [] = True
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>x : α<GOAL>VectorAllP p [x] = p x
<VAR>α : Type u_1<VAR>n : ℕ<VAR>p : α → Prop<VAR>x : α<VAR>v : Vector3 α n<GOAL>VectorAllP p (Vector3.cons x v) ↔ p x ∧ VectorAllP p v
<VAR>α : Type u_1<VAR>n : ℕ<VAR>p : α → Prop<VAR>v : Vector3 α n<GOAL>VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>p q : α → Prop<VAR>h : ∀ (x : α), p x → q x<VAR>v : Vector3 α n<VAR>al : VectorAllP p v<GOAL>VectorAllP q v
<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>One α<VAR>f : m ≃. n<VAR>i : m<VAR>j : n<GOAL>f.toMatrix i j = if j ∈ f i then 1 else 0
<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type v<VAR>Fintype m<VAR>DecidableEq m<VAR>Semiring α<VAR>f : l ≃. m<VAR>M : Matrix m n α<VAR>i : l<VAR>j : n<GOAL>(f.toMatrix * M) i j = Option.casesOn (f i) 0 fun fi => M fi j
<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type v<VAR>DecidableEq m<VAR>DecidableEq n<VAR>Zero α<VAR>One α<VAR>f : m ≃. n<GOAL>f.symm.toMatrix = f.toMatrix.transpose
<VAR>n : Type u_4<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>One α<GOAL>(PEquiv.refl n).toMatrix = 1
<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type v<VAR>Fintype m<VAR>Semiring α<VAR>DecidableEq n<VAR>M : Matrix l m α<VAR>f : m ≃. n<VAR>i : l<VAR>j : n<GOAL>(M * f.toMatrix) i j = Option.casesOn (f.symm j) 0 fun fj => M i fj
<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type v<VAR>Fintype m<VAR>DecidableEq m<VAR>Semiring α<VAR>f : m ≃ m<VAR>M : Matrix m n α<GOAL>f.toPEquiv.toMatrix * M = M.submatrix (⇑f) id
<VAR>m : Type u_5<VAR>n : Type u_6<VAR>α : Type u_7<VAR>Fintype n<VAR>DecidableEq n<VAR>Semiring α<VAR>f : n ≃ n<VAR>M : Matrix m n α<GOAL>M * f.toPEquiv.toMatrix = M.submatrix id ⇑f.symm
<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type v<VAR>Fintype m<VAR>DecidableEq m<VAR>DecidableEq n<VAR>Semiring α<VAR>f : l ≃. m<VAR>g : m ≃. n<GOAL>(f.trans g).toMatrix = f.toMatrix * g.toMatrix
<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>One α<GOAL>⊥.toMatrix = 0
<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type v<VAR>DecidableEq n<VAR>MonoidWithZero α<VAR>Nontrivial α<GOAL>Function.Injective PEquiv.toMatrix
<VAR>n : Type u_4<VAR>α : Type v<VAR>DecidableEq n<VAR>Ring α<VAR>i j : n<GOAL>(Equiv.toPEquiv (Equiv.swap i j)).toMatrix = 1 - (PEquiv.single i i).toMatrix - (PEquiv.single j j).toMatrix + (PEquiv.single i j).toMatrix + (PEquiv.single j i).toMatrix
<VAR>k : Type u_1<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq k<VAR>DecidableEq m<VAR>DecidableEq n<VAR>Semiring α<VAR>a : m<VAR>b : n<VAR>c : k<GOAL>(PEquiv.single a b).toMatrix * (PEquiv.single b c).toMatrix = (PEquiv.single a c).toMatrix
<VAR>k : Type u_1<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>DecidableEq k<VAR>DecidableEq m<VAR>Semiring α<VAR>b₁ b₂ : n<VAR>hb : b₁ ≠ b₂<VAR>a : m<VAR>c : k<GOAL>(PEquiv.single a b₁).toMatrix * (PEquiv.single b₂ c).toMatrix = 0
<VAR>k : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type v<VAR>Fintype n<VAR>Fintype k<VAR>DecidableEq n<VAR>DecidableEq k<VAR>DecidableEq m<VAR>Semiring α<VAR>a : m<VAR>b : n<VAR>c : k<VAR>M : Matrix k l α<GOAL>(PEquiv.single a b).toMatrix * ((PEquiv.single b c).toMatrix * M) = (PEquiv.single a c).toMatrix * M
<VAR>n : Type u_4<VAR>α : Type v<VAR>DecidableEq n<VAR>Zero α<VAR>One α<VAR>σ : n ≃ n<VAR>i j : n<GOAL>σ.toPEquiv.toMatrix i j = 1 (σ i) j
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I : Set α<GOAL>(M.restrictIndepMatroid R).Indep I = (M.Indep I ∧ I ⊆ R)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R : Set α<GOAL>(M.restrictIndepMatroid R).E = R
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I : Set α<GOAL>(M.restrict R).Indep I ↔ M.Indep I ∧ I ⊆ R
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I : Set α<VAR>h : M.Indep I<VAR>hIR : I ⊆ R<GOAL>(M.restrict R).Indep I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I : Set α<VAR>hI : (M.restrict R).Indep I<GOAL>M.Indep I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R : Set α<GOAL>(M.restrict R).E = R
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R : Set α<VAR>hR : R.Finite<GOAL>(M.restrict R).Finite
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R X : Set α<GOAL>(M.restrict R).Dep X ↔ ¬M.Indep X ∧ X ⊆ R
<VAR>α : Type u_1<VAR>M : Matroid α<GOAL>M.restrict M.E = M
<VAR>α : Type u_1<VAR>R₁ R₂ : Set α<VAR>M : Matroid α<VAR>hR : R₂ ⊆ R₁<GOAL>(M.restrict R₁).restrict R₂ = M.restrict R₂
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R : Set α<GOAL>(M.restrict R).restrict R = M.restrict R
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<VAR>hX : X ⊆ M.E := by aesop_mat<GOAL>(M.restrict X).Base I ↔ M.Basis I X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<GOAL>(M.restrict X).Base I ↔ M.Basis' I X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<VAR>h : M.Basis I X<GOAL>(M.restrict X).Base I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X Y : Set α<VAR>hI : M.Basis I X<VAR>hXY : X ⊆ Y<GOAL>(M.restrict Y).Basis I X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I X : Set α<GOAL>(M.restrict R).Basis' I X ↔ M.Basis' I (X ∩ R) ∧ I ⊆ R
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I X : Set α<GOAL>(M.restrict R).Basis I X ↔ M.Basis I (X ∩ M.E) ∧ X ⊆ R
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I X : Set α<VAR>hR : R ⊆ M.E := by aesop_mat<GOAL>(M.restrict R).Basis I X ↔ M.Basis I X ∧ X ⊆ R
<VAR>α : Type u_1<VAR>M M' : Matroid α<VAR>X : Set α<GOAL>M.restrict X = M'.restrict X ↔ ∀ I ⊆ X, M.Indep I ↔ M'.Indep I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R : Set α<GOAL>M.restrict R = M ↔ R = M.E
<VAR>α : Type u_1<VAR>M₁ M₂ : Matroid.Matroidᵣ α<GOAL>M₁.toMatroid = M₂.toMatroid ↔ M₁ = M₂
<VAR>α : Type u_1<VAR>M M' : Matroid.Matroidᵣ α<GOAL>M ≤ M' ↔ M.toMatroid.Restriction M'.toMatroid
<VAR>α : Type u_1<VAR>M M' : Matroid.Matroidᵣ α<GOAL>M < M' ↔ M.toMatroid.StrictRestriction M'.toMatroid
<VAR>α : Type u_1<VAR>M M' : Matroid α<GOAL>{ toMatroid := M } ≤ { toMatroid := M' } ↔ M.Restriction M'
<VAR>α : Type u_1<VAR>M M' : Matroid α<GOAL>{ toMatroid := M } < { toMatroid := M' } ↔ M.StrictRestriction M'
<VAR>α : Type u_1<VAR>M : Matroid α<GOAL>M.Restriction M
<VAR>α : Type u_1<VAR>M M' : Matroid α<VAR>h : M.Restriction M'<VAR>h' : M'.Restriction M<GOAL>M = M'
<VAR>α : Type u_1<VAR>M₁ M₂ M₃ : Matroid α<VAR>h : M₁.Restriction M₂<VAR>h' : M₂.Restriction M₃<GOAL>M₁.Restriction M₃
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R : Set α<VAR>hR : R ⊆ M.E := by aesop_mat<GOAL>(M.restrict R).Restriction M
<VAR>α : Type u_1<VAR>M N : Matroid α<VAR>h : N.Restriction M<GOAL>M.restrict N.E = N
<VAR>α : Type u_1<VAR>M N : Matroid α<VAR>h : N.Restriction M<GOAL>N.E ⊆ M.E
<VAR>α : Type u_1<VAR>M N : Matroid α<VAR>h : N.Restriction M<GOAL>∃ R ⊆ M.E, N = M.restrict R
<VAR>α : Type u_1<VAR>R R' : Set α<VAR>M : Matroid α<VAR>h : R ⊆ R'<GOAL>(M.restrict R).Restriction (M.restrict R')
<VAR>α : Type u_1<VAR>M N : Matroid α<GOAL>N.Restriction M ↔ ∃ R ⊆ M.E, N = M.restrict R
<VAR>α : Type u_1<VAR>M N : Matroid α<VAR>h : N.StrictRestriction M<GOAL>N.Restriction M
<VAR>α : Type u_1<VAR>M N : Matroid α<VAR>h : N.StrictRestriction M<GOAL>N ≠ M
<VAR>α : Type u_1<VAR>M : Matroid α<GOAL>¬M.StrictRestriction M
<VAR>α : Type u_1<VAR>M N : Matroid α<VAR>h : N.StrictRestriction M<GOAL>N.E ⊂ M.E
<VAR>α : Type u_1<VAR>M N : Matroid α<VAR>h : N.StrictRestriction M<GOAL>M.restrict N.E = N
<VAR>α : Type u_1<VAR>M N : Matroid α<VAR>h : N.StrictRestriction M<GOAL>∃ R ⊂ M.E, N = M.restrict R
<VAR>α : Type u_1<VAR>M N : Matroid α<VAR>h : N.Restriction M<VAR>hne : N ≠ M<GOAL>N.StrictRestriction M
<VAR>α : Type u_1<VAR>M N : Matroid α<VAR>h : N.Restriction M<GOAL>N = M ∨ N.StrictRestriction M
<VAR>α : Type u_1<VAR>R : Set α<VAR>M : Matroid α<VAR>hR : R ⊂ M.E<GOAL>(M.restrict R).StrictRestriction M
<VAR>α : Type u_1<VAR>M N : Matroid α<VAR>h : N.Restriction M<VAR>hne : N.E ≠ M.E<GOAL>N.StrictRestriction M
<VAR>α : Type u_1<VAR>R R' : Set α<VAR>M : Matroid α<VAR>h : R ⊂ R'<GOAL>(M.restrict R).StrictRestriction (M.restrict R')
<VAR>α : Type u_1<VAR>N M : Matroid α<VAR>M.Finite<VAR>h : N.Restriction M<GOAL>N.Finite
<VAR>α : Type u_1<VAR>N M : Matroid α<VAR>M.FiniteRk<VAR>h : N.Restriction M<GOAL>N.FiniteRk
<VAR>α : Type u_1<VAR>N M : Matroid α<VAR>M.Finitary<VAR>h : N.Restriction M<GOAL>N.Finitary
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>M.Finite<GOAL>{N | N.Restriction M}.Finite
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I : Set α<VAR>N : Matroid α<VAR>hI : N.Indep I<VAR>hNM : N.Restriction M<GOAL>M.Indep I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I : Set α<VAR>N : Matroid α<VAR>hI : M.Indep I<VAR>hNM : N.Restriction M<VAR>hIN : I ⊆ N.E<GOAL>N.Indep I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<VAR>N : Matroid α<VAR>hI : M.Basis I X<VAR>hNM : N.Restriction M<VAR>hX : X ⊆ N.E<GOAL>N.Basis I X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<VAR>N : Matroid α<VAR>hI : N.Basis I X<VAR>hNM : N.Restriction M<GOAL>M.Basis I X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I : Set α<VAR>N : Matroid α<VAR>hI : N.Base I<VAR>hNM : N.Restriction M<GOAL>M.Basis I N.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>X : Set α<VAR>N : Matroid α<VAR>hX : N.Dep X<VAR>hNM : N.Restriction M<GOAL>M.Dep X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>X : Set α<VAR>N : Matroid α<VAR>hX : M.Dep X<VAR>hNM : N.Restriction M<VAR>hXE : X ⊆ N.E := by aesop_mat<GOAL>N.Dep X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X Y J : Set α<VAR>hIX : M.Basis I X<VAR>hJX : M.Basis J X<VAR>hXY : X ⊆ Y<VAR>hJY : M.Basis J Y<GOAL>M.Basis I Y
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X Y J : Set α<VAR>hI : M.Basis I X<VAR>hJ : M.Basis J Y<VAR>hJX : J ⊆ X<VAR>hIY : I ⊆ Y<GOAL>M.Basis I Y
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X J : Set α<VAR>hI : M.Indep I<VAR>hIX : I ⊆ X<VAR>hJ : M.Basis J X<GOAL>∃ I', M.Basis I' X ∧ I ⊆ I' ∧ I' ⊆ I ∪ J
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X J : Set α<VAR>hI : M.Indep I<VAR>hIX : I ⊆ X<VAR>hI' : ¬M.Basis I X<VAR>hJ : M.Basis J X<GOAL>∃ e ∈ J \ I, M.Indep (insert e I)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X B : Set α<VAR>hIX : M.Basis I X<VAR>hB : M.Base B<VAR>hBX : B ⊆ X<GOAL>M.Base I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X J : Set α<VAR>e : α<VAR>hIX : M.Basis I X<VAR>hJX : M.Basis J X<VAR>he : e ∈ I \ J<GOAL>∃ f ∈ J \ I, M.Basis (insert f (I \ {e})) X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X J : Set α<VAR>e : α<VAR>hI : M.Basis I X<VAR>hJ : M.Basis J X<VAR>hIJ : I \ J = {e}<GOAL>∃ f ∈ J \ I, J = insert f I \ {e}
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X J : Set α<VAR>hI : M.Basis' I X<VAR>hJ : M.Basis' J X<GOAL>I.encard = J.encard
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X J : Set α<VAR>hI : M.Basis I X<VAR>hJ : M.Basis J X<GOAL>I.encard = J.encard
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I J : Set α<VAR>hI : M.Indep I<VAR>hJ : M.Indep J<VAR>hIJ : I.encard < J.encard<GOAL>∃ e ∈ J \ I, M.Indep (insert e I)
<VAR>R : Type u_1<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n : Type u_5<VAR>A₁ : Matrix m₁ n R<VAR>A₂ : Matrix m₂ n R<VAR>i : m₁<VAR>j : n<GOAL>A₁.fromRows A₂ (Sum.inl i) j = A₁ i j
<VAR>R : Type u_1<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n : Type u_5<VAR>A₁ : Matrix m₁ n R<VAR>A₂ : Matrix m₂ n R<VAR>i : m₂<VAR>j : n<GOAL>A₁.fromRows A₂ (Sum.inr i) j = A₂ i j
<VAR>R : Type u_1<VAR>m : Type u_2<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<VAR>A₁ : Matrix m n₁ R<VAR>A₂ : Matrix m n₂ R<VAR>i : m<VAR>j : n₁<GOAL>A₁.fromColumns A₂ i (Sum.inl j) = A₁ i j
<VAR>R : Type u_1<VAR>m : Type u_2<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<VAR>A₁ : Matrix m n₁ R<VAR>A₂ : Matrix m n₂ R<VAR>i : m<VAR>j : n₂<GOAL>A₁.fromColumns A₂ i (Sum.inr j) = A₂ i j
<VAR>R : Type u_1<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n : Type u_5<VAR>A : Matrix (m₁ ⊕ m₂) n R<VAR>i : m₁<VAR>j : n<GOAL>A.toRows₁ i j = A (Sum.inl i) j
<VAR>R : Type u_1<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n : Type u_5<VAR>A : Matrix (m₁ ⊕ m₂) n R<VAR>i : m₂<VAR>j : n<GOAL>A.toRows₂ i j = A (Sum.inr i) j
<VAR>R : Type u_1<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n : Type u_5<VAR>A₁ : Matrix m₁ n R<VAR>A₂ : Matrix m₂ n R<GOAL>(A₁.fromRows A₂).toRows₁ = A₁
<VAR>R : Type u_1<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n : Type u_5<VAR>A₁ : Matrix m₁ n R<VAR>A₂ : Matrix m₂ n R<GOAL>(A₁.fromRows A₂).toRows₂ = A₂
<VAR>R : Type u_1<VAR>m : Type u_2<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<VAR>A : Matrix m (n₁ ⊕ n₂) R<VAR>i : m<VAR>j : n₁<GOAL>A.toColumns₁ i j = A i (Sum.inl j)
<VAR>R : Type u_1<VAR>m : Type u_2<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<VAR>A : Matrix m (n₁ ⊕ n₂) R<VAR>i : m<VAR>j : n₂<GOAL>A.toColumns₂ i j = A i (Sum.inr j)
<VAR>R : Type u_1<VAR>m : Type u_2<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<VAR>A₁ : Matrix m n₁ R<VAR>A₂ : Matrix m n₂ R<GOAL>(A₁.fromColumns A₂).toColumns₁ = A₁
<VAR>R : Type u_1<VAR>m : Type u_2<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<VAR>A₁ : Matrix m n₁ R<VAR>A₂ : Matrix m n₂ R<GOAL>(A₁.fromColumns A₂).toColumns₂ = A₂
<VAR>R : Type u_1<VAR>m : Type u_2<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<VAR>A : Matrix m (n₁ ⊕ n₂) R<GOAL>A.toColumns₁.fromColumns A.toColumns₂ = A
<VAR>R : Type u_1<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n : Type u_5<VAR>A : Matrix (m₁ ⊕ m₂) n R<GOAL>A.toRows₁.fromRows A.toRows₂ = A
<VAR>R : Type u_1<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n : Type u_5<GOAL>Function.Injective2 Matrix.fromRows
<VAR>R : Type u_1<VAR>m : Type u_2<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<GOAL>Function.Injective2 Matrix.fromColumns
<VAR>R : Type u_1<VAR>m : Type u_2<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<VAR>A₁ : Matrix m n₁ R<VAR>A₂ : Matrix m n₂ R<VAR>B₁ : Matrix m n₁ R<VAR>B₂ : Matrix m n₂ R<GOAL>A₁.fromColumns A₂ = B₁.fromColumns B₂ ↔ A₁ = B₁ ∧ A₂ = B₂
<VAR>R : Type u_1<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n : Type u_5<VAR>A₁ : Matrix m₁ n R<VAR>A₂ : Matrix m₂ n R<VAR>B₁ : Matrix m₁ n R<VAR>B₂ : Matrix m₂ n R<GOAL>A₁.fromRows A₂ = B₁.fromRows B₂ ↔ A₁ = B₁ ∧ A₂ = B₂
<VAR>R : Type u_1<VAR>m : Type u_2<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<VAR>A₁ : Matrix m n₁ R<VAR>A₂ : Matrix m n₂ R<GOAL>(A₁.fromColumns A₂).transpose = A₁.transpose.fromRows A₂.transpose
<VAR>R : Type u_1<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n : Type u_5<VAR>A₁ : Matrix m₁ n R<VAR>A₂ : Matrix m₂ n R<GOAL>(A₁.fromRows A₂).transpose = A₁.transpose.fromColumns A₂.transpose
<VAR>R : Type u_1<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n : Type u_5<VAR>Neg R<VAR>A₁ : Matrix m₁ n R<VAR>A₂ : Matrix m₂ n R<GOAL>-A₁.fromRows A₂ = (-A₁).fromRows (-A₂)
<VAR>R : Type u_1<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n : Type u_5<VAR>Neg R<VAR>A₁ : Matrix n m₁ R<VAR>A₂ : Matrix n m₂ R<GOAL>-A₁.fromColumns A₂ = (-A₁).fromColumns (-A₂)
<VAR>R : Type u_1<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n : Type u_5<VAR>Fintype n<VAR>Semiring R<VAR>A₁ : Matrix m₁ n R<VAR>A₂ : Matrix m₂ n R<VAR>v : n → R<GOAL>(A₁.fromRows A₂).mulVec v = Sum.elim (A₁.mulVec v) (A₂.mulVec v)
<VAR>R : Type u_1<VAR>m : Type u_2<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<VAR>Fintype m<VAR>Semiring R<VAR>B₁ : Matrix m n₁ R<VAR>B₂ : Matrix m n₂ R<VAR>v : m → R<GOAL>Matrix.vecMul v (B₁.fromColumns B₂) = Sum.elim (Matrix.vecMul v B₁) (Matrix.vecMul v B₂)
<VAR>R : Type u_1<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n : Type u_5<VAR>Fintype m₁<VAR>Fintype m₂<VAR>Semiring R<VAR>B₁ : Matrix m₁ n R<VAR>B₂ : Matrix m₂ n R<VAR>v₁ : m₁ → R<VAR>v₂ : m₂ → R<GOAL>Matrix.vecMul (Sum.elim v₁ v₂) (B₁.fromRows B₂) = Matrix.vecMul v₁ B₁ + Matrix.vecMul v₂ B₂
<VAR>R : Type u_1<VAR>m : Type u_2<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<VAR>Fintype n₁<VAR>Fintype n₂<VAR>Semiring R<VAR>A₁ : Matrix m n₁ R<VAR>A₂ : Matrix m n₂ R<VAR>v₁ : n₁ → R<VAR>v₂ : n₂ → R<GOAL>(A₁.fromColumns A₂).mulVec (Sum.elim v₁ v₂) = A₁.mulVec v₁ + A₂.mulVec v₂
<VAR>R : Type u_1<VAR>m : Type u_2<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n : Type u_5<VAR>Fintype n<VAR>Semiring R<VAR>A₁ : Matrix m₁ n R<VAR>A₂ : Matrix m₂ n R<VAR>B : Matrix n m R<GOAL>A₁.fromRows A₂ * B = (A₁ * B).fromRows (A₂ * B)
<VAR>R : Type u_1<VAR>m : Type u_2<VAR>n : Type u_5<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<VAR>Fintype n<VAR>Semiring R<VAR>A : Matrix m n R<VAR>B₁ : Matrix n n₁ R<VAR>B₂ : Matrix n n₂ R<GOAL>A * B₁.fromColumns B₂ = (A * B₁).fromColumns (A * B₂)
<VAR>R : Type u_1<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n : Type u_5<VAR>Semiring R<GOAL>Matrix.fromRows 0 0 = 0
<VAR>R : Type u_1<VAR>m : Type u_2<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<VAR>Semiring R<GOAL>Matrix.fromColumns 0 0 = 0
<VAR>R : Type u_1<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<VAR>B₁₁ : Matrix m₁ n₁ R<VAR>B₁₂ : Matrix m₁ n₂ R<VAR>B₂₁ : Matrix m₂ n₁ R<VAR>B₂₂ : Matrix m₂ n₂ R<GOAL>(B₁₁.fromRows B₂₁).fromColumns (B₁₂.fromRows B₂₂) = Matrix.fromBlocks B₁₁ B₁₂ B₂₁ B₂₂
<VAR>R : Type u_1<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<VAR>B₁₁ : Matrix m₁ n₁ R<VAR>B₁₂ : Matrix m₁ n₂ R<VAR>B₂₁ : Matrix m₂ n₁ R<VAR>B₂₂ : Matrix m₂ n₂ R<GOAL>(B₁₁.fromColumns B₁₂).fromRows (B₂₁.fromColumns B₂₂) = Matrix.fromBlocks B₁₁ B₁₂ B₂₁ B₂₂
<VAR>R : Type u_1<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n : Type u_5<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<VAR>Fintype n<VAR>Semiring R<VAR>A₁ : Matrix m₁ n R<VAR>A₂ : Matrix m₂ n R<VAR>B₁ : Matrix n n₁ R<VAR>B₂ : Matrix n n₂ R<GOAL>A₁.fromRows A₂ * B₁.fromColumns B₂ = Matrix.fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂)
<VAR>R : Type u_1<VAR>m : Type u_2<VAR>n : Type u_5<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<VAR>Fintype n₁<VAR>Fintype n₂<VAR>Semiring R<VAR>A₁ : Matrix m n₁ R<VAR>A₂ : Matrix m n₂ R<VAR>B₁ : Matrix n₁ n R<VAR>B₂ : Matrix n₂ n R<GOAL>A₁.fromColumns A₂ * B₁.fromRows B₂ = A₁ * B₁ + A₂ * B₂
<VAR>R : Type u_1<VAR>m : Type u_2<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<VAR>Fintype m₁<VAR>Fintype m₂<VAR>Semiring R<VAR>A₁ : Matrix m m₁ R<VAR>A₂ : Matrix m m₂ R<VAR>B₁₁ : Matrix m₁ n₁ R<VAR>B₁₂ : Matrix m₁ n₂ R<VAR>B₂₁ : Matrix m₂ n₁ R<VAR>B₂₂ : Matrix m₂ n₂ R<GOAL>A₁.fromColumns A₂ * Matrix.fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ = (A₁ * B₁₁ + A₂ * B₂₁).fromColumns (A₁ * B₁₂ + A₂ * B₂₂)
<VAR>R : Type u_1<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n : Type u_5<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<VAR>Fintype n₁<VAR>Fintype n₂<VAR>Semiring R<VAR>A₁ : Matrix n₁ n R<VAR>A₂ : Matrix n₂ n R<VAR>B₁₁ : Matrix m₁ n₁ R<VAR>B₁₂ : Matrix m₁ n₂ R<VAR>B₂₁ : Matrix m₂ n₁ R<VAR>B₂₂ : Matrix m₂ n₂ R<GOAL>Matrix.fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂ = (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂)
<VAR>R : Type u_1<VAR>n : Type u_5<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<VAR>Fintype n<VAR>Fintype n₁<VAR>Fintype n₂<VAR>DecidableEq n<VAR>DecidableEq n₁<VAR>DecidableEq n₂<VAR>CommRing R<VAR>e : n ≃ n₁ ⊕ n₂<VAR>A₁ : Matrix n n₁ R<VAR>A₂ : Matrix n n₂ R<VAR>B₁ : Matrix n₁ n R<VAR>B₂ : Matrix n₂ n R<GOAL>A₁.fromColumns A₂ * B₁.fromRows B₂ = 1 ↔ B₁.fromRows B₂ * A₁.fromColumns A₂ = 1
<VAR>R : Type u_1<VAR>n : Type u_5<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing R<VAR>p : n → Prop<VAR>DecidablePred p<VAR>A₁ : Matrix n { i // p i } R<VAR>A₂ : Matrix n { i // ¬p i } R<VAR>B₁ : Matrix { i // p i } n R<VAR>B₂ : Matrix { i // ¬p i } n R<GOAL>A₁.fromColumns A₂ * B₁.fromRows B₂ = 1 ↔ B₁.fromRows B₂ * A₁.fromColumns A₂ = 1
<VAR>R : Type u_1<VAR>m : Type u_2<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<VAR>Star R<VAR>A₁ : Matrix m n₁ R<VAR>A₂ : Matrix m n₂ R<GOAL>(A₁.fromColumns A₂).conjTranspose = A₁.conjTranspose.fromRows A₂.conjTranspose
<VAR>R : Type u_1<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n : Type u_5<VAR>Star R<VAR>A₁ : Matrix m₁ n R<VAR>A₂ : Matrix m₂ n R<GOAL>(A₁.fromRows A₂).conjTranspose = A₁.conjTranspose.fromColumns A₂.conjTranspose
<VAR>n m : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>G : Fin2 n → TypeVec.{u} m → Type u<VAR>α : TypeVec.{u} m<VAR>x : MvQPF.Comp F G α<GOAL>MvQPF.Comp.mk x.get = x
<VAR>n m : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>G : Fin2 n → TypeVec.{u} m → Type u<VAR>α : TypeVec.{u} m<VAR>x : F fun i => G i α<GOAL>(MvQPF.Comp.mk x).get = x
<VAR>n m : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>G : Fin2 n → TypeVec.{u} m → Type u<VAR>α β : TypeVec.{u} m<VAR>f : α.Arrow β<VAR>MvFunctor F<VAR>(i : Fin2 n) → MvFunctor (G i)<VAR>x : F fun i => G i α<GOAL>MvFunctor.map f (MvQPF.Comp.mk x) = MvQPF.Comp.mk (MvFunctor.map (fun i x => MvFunctor.map f x) x)
<VAR>n m : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>G : Fin2 n → TypeVec.{u} m → Type u<VAR>α β : TypeVec.{u} m<VAR>f : α.Arrow β<VAR>MvFunctor F<VAR>(i : Fin2 n) → MvFunctor (G i)<VAR>x : MvQPF.Comp F G α<GOAL>(MvFunctor.map f x).get = MvFunctor.map (fun i x => MvFunctor.map f x) x.get
<VAR>α : Type u_1<VAR>self : Matroid α<VAR>I : Set α<GOAL>self.Indep I ↔ ∃ B, self.Base B ∧ I ⊆ B
<VAR>α : Type u_1<VAR>self : Matroid α<GOAL>Matroid.ExchangeProperty self.Base
<VAR>α : Type u_1<VAR>self : Matroid α<VAR>B : Set α<GOAL>self.Base B → B ⊆ self.E
<VAR>α : Type u_1<VAR>self : Matroid α<VAR>X : Set α<GOAL>X ⊆ self.E → Matroid.ExistsMaximalSubsetProperty self.Indep X
<VAR>α : Type u_1<VAR>self : Matroid α<GOAL>∃ B, self.Base B
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>self : M.Finite<GOAL>M.E.Finite
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>self : M.Nonempty<GOAL>M.E.Nonempty
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>M.Nonempty<GOAL>M.E.Nonempty
<VAR>α : Type u_1<VAR>M : Matroid α<GOAL>M.E.Nonempty ↔ M.Nonempty
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>M.Finite<GOAL>M.E.Finite
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>M.Finite<VAR>X : Set α<VAR>hX : X ⊆ M.E := by aesop<GOAL>X.Finite
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>self : M.FiniteRk<GOAL>∃ B, M.Base B ∧ B.Finite
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>self : M.InfiniteRk<GOAL>∃ B, M.Base B ∧ B.Infinite
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>self : M.RkPos<GOAL>¬M.Base ∅
<VAR>α : Type u_1<VAR>M : Matroid α<GOAL>M.RkPos ↔ ¬M.Base ∅
<VAR>α : Type u_1<VAR>Base : Set α → Prop<VAR>exch : Matroid.ExchangeProperty Base<VAR>B B' : Set α<VAR>hB : Base B<VAR>hB' : Base B'<VAR>h : B ⊆ B'<GOAL>B = B'
<VAR>α : Type u_1<VAR>Base : Set α → Prop<VAR>B₁ B₂ : Set α<VAR>exch : Matroid.ExchangeProperty Base<VAR>hB₁ : Base B₁<VAR>hB₂ : Base B₂<GOAL>(B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
<VAR>α : Type u_1<VAR>Base : Set α → Prop<VAR>exch : Matroid.ExchangeProperty Base<VAR>B₁ B₂ : Set α<VAR>hB₁ : Base B₁<VAR>hB₂ : Base B₂<GOAL>(B₁ \ B₂).encard = (B₂ \ B₁).encard
<VAR>α : Type u_1<VAR>Base : Set α → Prop<VAR>exch : Matroid.ExchangeProperty Base<VAR>B₁ B₂ : Set α<VAR>hB₁ : Base B₁<VAR>hB₂ : Base B₂<GOAL>B₁.encard = B₂.encard
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>X Y : Set α<VAR>hX : X ⊆ M.E<GOAL>X ∩ Y ⊆ M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>X Y : Set α<VAR>hX : X ⊆ M.E<GOAL>Y ∩ X ⊆ M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>X Y : Set α<VAR>hX : X ⊆ M.E<GOAL>X \ Y ⊆ M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>X : Set α<GOAL>M.E \ X ⊆ M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>e : α<VAR>he : e ∈ M.E<GOAL>{e} ⊆ M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>X Y : Set α<VAR>hXY : X ⊆ Y<VAR>hY : Y ⊆ M.E<GOAL>X ⊆ M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>X : Set α<VAR>e : α<VAR>hX : X ⊆ M.E<VAR>heX : e ∈ X<GOAL>e ∈ M.E