ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s t : Finset α<VAR>h : Disjoint s t<GOAL>Finset.filter p (s.disjUnion t h) = (Finset.filter p s).disjUnion (Finset.filter p t) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α → β<VAR>s : Set β<VAR>t : Finset α<GOAL>s.PairwiseDisjoint fun x => Finset.filter (fun x_1 => f x_1 = x) t
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>a : α<VAR>s : Finset α<VAR>ha : a ∉ s<GOAL>Finset.filter p (Finset.cons a s ha) = (if p a then {a} else ∅).disjUnion (Finset.filter p s) ⋯
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>DecidableEq α<VAR>s₁ s₂ : Finset α<GOAL>Finset.filter p (s₁ ∪ s₂) = Finset.filter p s₁ ∪ Finset.filter p s₂
<VAR>α : Type u_1<VAR>p q : α → Prop<VAR>DecidablePred p<VAR>DecidablePred q<VAR>DecidableEq α<VAR>s : Finset α<GOAL>Finset.filter p s ∪ Finset.filter q s = Finset.filter (fun x => p x ∨ q x) s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>(i : α) → Decidable (i ∈ t)<GOAL>Finset.filter (fun i => i ∈ t) s = s ∩ t
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>Finset.filter p (s ∩ t) = Finset.filter p s ∩ Finset.filter p t
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>Finset.filter p s ∩ t = Finset.filter p (s ∩ t)
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>s ∩ Finset.filter p t = Finset.filter p (s ∩ t)
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>Finset.filter p (insert a s) = if p a then insert a (Finset.filter p s) else Finset.filter p s
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>Finset.filter p (s.erase a) = (Finset.filter p s).erase a
<VAR>α : Type u_1<VAR>p q : α → Prop<VAR>DecidablePred p<VAR>DecidablePred q<VAR>DecidableEq α<VAR>s : Finset α<GOAL>Finset.filter (fun a => p a ∨ q a) s = Finset.filter p s ∪ Finset.filter q s
<VAR>α : Type u_1<VAR>p q : α → Prop<VAR>DecidablePred p<VAR>DecidablePred q<VAR>DecidableEq α<VAR>s : Finset α<GOAL>Finset.filter (fun a => p a ∧ q a) s = Finset.filter p s ∩ Finset.filter q s
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>DecidableEq α<VAR>s : Finset α<GOAL>Finset.filter (fun a => ¬p a) s = s \ Finset.filter p s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>p q : α → Prop<VAR>DecidablePred p<VAR>DecidablePred q<GOAL>Finset.filter (fun a => p a ∧ ¬q a) s = Finset.filter p s \ Finset.filter q s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s₁ s₂ : Finset α<GOAL>s₁ \ s₂ = Finset.filter (fun x => x ∉ s₂) s₁
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s₁ s₂ : Finset α<GOAL>s₁ \ s₂ = s₁ ↔ s₁ ∩ s₂ ⊆ ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>t₁ t₂ : Set α<VAR>h : ↑s ⊆ t₁ ∪ t₂<GOAL>∃ s₁ s₂, s₁ ∪ s₂ = s ∧ ↑s₁ ⊆ t₁ ∧ ↑s₂ ⊆ t₂ \ t₁
<VAR>β : Type u_2<VAR>DecidableEq β<VAR>s : Finset β<VAR>b : β<GOAL>Finset.filter (Eq b) s = if b ∈ s then {b} else ∅
<VAR>β : Type u_2<VAR>DecidableEq β<VAR>s : Finset β<VAR>b : β<GOAL>Finset.filter (fun a => a = b) s = if b ∈ s then {b} else ∅
<VAR>β : Type u_2<VAR>DecidableEq β<VAR>s : Finset β<VAR>b : β<GOAL>Finset.filter (fun a => b ≠ a) s = s.erase b
<VAR>β : Type u_2<VAR>DecidableEq β<VAR>s : Finset β<VAR>b : β<GOAL>Finset.filter (fun a => a ≠ b) s = s.erase b
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>Finset.filter p s ∩ Finset.filter (fun a => ¬p a) t = ∅
<VAR>α : Type u_1<VAR>p q : α → Prop<VAR>DecidablePred p<VAR>DecidablePred q<VAR>DecidableEq α<VAR>s : Finset α<VAR>h : Codisjoint p q<GOAL>Finset.filter p s ∪ Finset.filter q s = s
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>DecidableEq α<VAR>(x : α) → Decidable ¬p x<VAR>s : Finset α<GOAL>Finset.filter p s ∪ Finset.filter (fun a => ¬p a) s = s
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s t : Finset α<GOAL>Finset.filter p s = Finset.filter p t ↔ ∀ ⦃a : α⦄, p a → (a ∈ s ↔ a ∈ t)
<VAR>α : Type u_1<VAR>p q : α → Prop<VAR>DecidablePred p<VAR>DecidablePred q<VAR>s : Finset α<GOAL>Finset.filter p s = Finset.filter q s ↔ ∀ ⦃a : α⦄, a ∈ s → (p a ↔ q a)
<VAR>n : ℕ<GOAL>(Finset.range n).val = Multiset.range n
<VAR>n m : ℕ<GOAL>m ∈ Finset.range n ↔ m < n
<VAR>n : ℕ<GOAL>↑(Finset.range n) = Set.Iio n
<VAR>n : ℕ<GOAL>Finset.range n.succ = insert n (Finset.range n)
<VAR>n : ℕ<GOAL>Finset.range (n + 1) = insert n (Finset.range n)
<VAR>n : ℕ<GOAL>n ∉ Finset.range n
<VAR>n : ℕ<GOAL>n ∈ Finset.range (n + 1)
<VAR>n m : ℕ<GOAL>Finset.range n ⊆ Finset.range m ↔ n ≤ m
<VAR>a b : ℕ<GOAL>a ∈ Finset.range b.succ ↔ a ≤ b
<VAR>n x : ℕ<VAR>hx : x ∈ Finset.range n<GOAL>x ≤ n
<VAR>n x : ℕ<VAR>hx : x ∈ Finset.range n<GOAL>n - x ≠ 0
<VAR>n : ℕ<GOAL>(Finset.range n).Nonempty ↔ n ≠ 0
<VAR>n : ℕ<GOAL>Finset.range n = ∅ ↔ n = 0
<VAR>n : ℕ<GOAL>(Finset.range (n + 1)).Nonempty
<VAR>n m : ℕ<GOAL>Finset.filter (fun x => x = m) (Finset.range n) = if m < n then {m} else ∅
<VAR>n : ℕ<VAR>hn : 1 < n<GOAL>(Finset.range n).Nontrivial
<VAR>α : Type u_1<VAR>p : α → Prop<GOAL>(∃ x ∈ ∅, p x) ↔ False
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>p : α → Prop<GOAL>(∃ x ∈ insert a s, p x) ↔ p a ∨ ∃ x ∈ s, p x
<VAR>α : Type u_1<VAR>p : α → Prop<GOAL>(∀ x ∈ ∅, p x) ↔ True
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>p : α → Prop<GOAL>(∀ x ∈ insert a s, p x) ↔ p a ∧ ∀ x ∈ s, p x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>p : α → Prop<VAR>a : α<VAR>s : Finset α<VAR>H : ∀ x ∈ insert a s, p x<VAR>x : α<VAR>h : x ∈ s<GOAL>p x
<VAR>k : ℕ<GOAL>⇑(notMemRangeEquiv k) = fun i => ↑i - k
<VAR>k : ℕ<GOAL>⇑(notMemRangeEquiv k).symm = fun j => ⟨j + k, ⋯⟩
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>s.toFinset.val = s.dedup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<VAR>n : s.Nodup<GOAL>{ val := s, nodup := n } = s.toFinset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l l' : Multiset α<VAR>hl : l.Nodup<VAR>hl' : l'.Nodup<VAR>h : l.toFinset = l'.toFinset<GOAL>l = l'
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>a ∈ s.toFinset ↔ a ∈ s
<VAR>α : Type u_1<VAR>DecidableEq α<GOAL>Multiset.toFinset 0 = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>(a ::ₘ s).toFinset = insert a s.toFinset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<GOAL>{a}.toFinset = {a}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>(s + t).toFinset = s.toFinset ∪ t.toFinset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<VAR>n : ℕ<GOAL>n ≠ 0 → (n • s).toFinset = s.toFinset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<VAR>a : α<GOAL>s.toFinset = {a} ↔ Multiset.card s ≠ 0 ∧ s = Multiset.card s • {a}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>(s ∩ t).toFinset = s.toFinset ∩ t.toFinset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>(s ∪ t).toFinset = s.toFinset ∪ t.toFinset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m : Multiset α<GOAL>m.toFinset = ∅ ↔ m = 0
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>s.toFinset.Nonempty ↔ s ≠ 0
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>s.toFinset ⊆ t.toFinset ↔ s ⊆ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Multiset α<GOAL>s.toFinset ⊂ t.toFinset ↔ s ⊂ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m : Multiset α<GOAL>m.dedup.toFinset = m.toFinset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<VAR>p : α → Prop<VAR>DecidablePred p<GOAL>(Multiset.filter p s).toFinset = Finset.filter p s.toFinset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>s.val.toFinset = s
<VAR>α : Type u_1<VAR>a : Finset α<VAR>b : Multiset α<GOAL>a.val ≤ b ↔ a.val ⊆ b
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<GOAL>l.toFinset.val = ↑l.dedup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>n : l.Nodup<GOAL>{ val := ↑l, nodup := n } = l.toFinset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>a : α<GOAL>a ∈ l.toFinset ↔ a ∈ l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<GOAL>↑l.toFinset = {a | a ∈ l}
<VAR>α : Type u_1<VAR>DecidableEq α<GOAL>[].toFinset = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>a : α<GOAL>(a :: l).toFinset = insert a l.toFinset
<VAR>α : Type u_1<VAR>DecidableEq α<GOAL>Set.SurjOn List.toFinset {l | l.Nodup} Set.univ
<VAR>α : Type u_1<VAR>DecidableEq α<GOAL>Function.Surjective List.toFinset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l l' : List α<GOAL>l.toFinset = l'.toFinset ↔ l.dedup.Perm l'.dedup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : List α<GOAL>a.toFinset = b.toFinset ↔ ∀ (x : α), x ∈ a ↔ x ∈ b
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l l' : List α<GOAL>(∀ (x : α), x ∈ l ↔ x ∈ l') → l.toFinset = l'.toFinset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l l' : List α<VAR>h : l.Perm l'<GOAL>l.toFinset = l'.toFinset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l l' : List α<VAR>hl : l.Nodup<VAR>hl' : l'.Nodup<VAR>h : l.toFinset = l'.toFinset<GOAL>l.Perm l'
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l l' : List α<GOAL>(l ++ l').toFinset = l.toFinset ∪ l'.toFinset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<GOAL>l.reverse.toFinset = l.toFinset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>(List.replicate n a).toFinset = {a}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l l' : List α<GOAL>(l ∪ l').toFinset = l.toFinset ∪ l'.toFinset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l l' : List α<GOAL>(l ∩ l').toFinset = l.toFinset ∩ l'.toFinset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<GOAL>l.toFinset = ∅ ↔ l = []
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<GOAL>l.toFinset.Nonempty ↔ l ≠ []
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : List α<VAR>p : α → Bool<GOAL>(List.filter p s).toFinset = Finset.filter (fun x => p x = true) s.toFinset
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s.toList.Nodup
<VAR>α : Type u_1<VAR>a : α<VAR>s : Finset α<GOAL>a ∈ s.toList ↔ a ∈ s
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s.toList = [] ↔ s = ∅
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s.toList.isEmpty = true ↔ s = ∅
<VAR>α : Type u_1<GOAL>∅.toList = []
<VAR>α : Type u_1<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>s.toList ≠ []
<VAR>α : Type u_1<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>¬s.toList.isEmpty = true
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>↑s.toList = s.val
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>s.toList.toFinset = s
<VAR>α : Type u_1<VAR>a : α<VAR>s : Finset α<GOAL>s.toList = [a] ↔ s = {a}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>∃ l, l.Nodup ∧ l.toFinset = s
<VAR>α : Type u_1<VAR>a : α<VAR>s : Finset α<VAR>h : a ∉ s<GOAL>(Finset.cons a s h).toList.Perm (a :: s.toList)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>h : a ∉ s<GOAL>(insert a s).toList.Perm (a :: s.toList)
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>l : Finset α<VAR>hp : ∃! a, a ∈ l ∧ p a<GOAL>Finset.choose p l hp ∈ l ∧ p (Finset.choose p l hp)
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>l : Finset α<VAR>hp : ∃! a, a ∈ l ∧ p a<GOAL>Finset.choose p l hp ∈ l
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>l : Finset α<VAR>hp : ∃! a, a ∈ l ∧ p a<GOAL>p (Finset.choose p l hp)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>r : β → β → Prop<VAR>f : α → β<GOAL>Pairwise (r on fun x => f ↑x) ↔ (↑s).Pairwise (r on f)
<VAR>α : Type u_1<VAR>s : Finset α<VAR>r : α → α → Prop<GOAL>Pairwise (r on fun x => ↑x) ↔ (↑s).Pairwise r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>a : α<VAR>ha : a ∉ s<VAR>r : β → β → Prop<VAR>f : α → β<GOAL>Pairwise (r on fun a_1 => f ↑a_1) ↔ Pairwise (r on fun a => f ↑a) ∧ ∀ b ∈ s, r (f a) (f b) ∧ r (f b) (f a)
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<VAR>ha : a ∉ s<VAR>r : α → α → Prop<GOAL>Pairwise (r on fun a_1 => ↑a_1) ↔ Pairwise (r on fun a => ↑a) ∧ ∀ b ∈ s, r a b ∧ r b a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>h : Disjoint s t<VAR>x : { x // x ∈ s }<GOAL>(Equiv.Finset.union s t h) (Sum.inl x) = ⟨↑x, ⋯⟩
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>h : Disjoint s t<VAR>y : { x // x ∈ t }<GOAL>(Equiv.Finset.union s t h) (Sum.inr y) = ⟨↑y, ⋯⟩
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m1 m2 : Multiset α<GOAL>Disjoint m1.toFinset m2.toFinset ↔ m1.Disjoint m2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l l' : List α<GOAL>Disjoint l.toFinset l'.toFinset ↔ l.Disjoint l'
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>α : Type u_3<VAR>Fintype n<VAR>DecidableEq n<VAR>Semiring α<VAR>A : Matrix n n α<VAR>B : Matrix n m α<VAR>Invertible A<GOAL>⅟A * (A * B) = B
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>α : Type u_3<VAR>Fintype n<VAR>DecidableEq n<VAR>Semiring α<VAR>A : Matrix n n α<VAR>B : Matrix n m α<VAR>Invertible A<GOAL>A * (⅟A * B) = B
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>α : Type u_3<VAR>Fintype n<VAR>DecidableEq n<VAR>Semiring α<VAR>A : Matrix m n α<VAR>B : Matrix n n α<VAR>Invertible B<GOAL>A * ⅟B * B = A
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>α : Type u_3<VAR>Fintype n<VAR>DecidableEq n<VAR>Semiring α<VAR>A : Matrix m n α<VAR>B : Matrix n n α<VAR>Invertible B<GOAL>A * B * ⅟B = A
<VAR>n : Type u_2<VAR>α : Type u_3<VAR>Fintype n<VAR>DecidableEq n<VAR>Semiring α<VAR>StarRing α<VAR>A : Matrix n n α<VAR>Invertible A<VAR>Invertible Aᴴ<GOAL>(⅟A)ᴴ = ⅟Aᴴ
<VAR>n : Type u_2<VAR>α : Type u_3<VAR>Fintype n<VAR>DecidableEq n<VAR>Semiring α<VAR>StarRing α<VAR>A : Matrix n n α<GOAL>IsUnit Aᴴ ↔ IsUnit A
<VAR>n : Type u_2<VAR>α : Type u_3<VAR>Fintype n<VAR>DecidableEq n<VAR>CommSemiring α<VAR>A : Matrix n n α<VAR>Invertible A<VAR>Invertible Aᵀ<GOAL>(⅟A)ᵀ = ⅟Aᵀ
<VAR>n : Type u_2<VAR>α : Type u_3<VAR>Fintype n<VAR>DecidableEq n<VAR>CommSemiring α<VAR>A : Matrix n n α<VAR>Invertible Aᵀ<GOAL>A.transposeInvertibleEquivInvertible inst✝ = A.invertibleOfInvertibleTranspose
<VAR>n : Type u_2<VAR>α : Type u_3<VAR>Fintype n<VAR>DecidableEq n<VAR>CommSemiring α<VAR>A : Matrix n n α<VAR>Invertible A<GOAL>A.transposeInvertibleEquivInvertible.symm inst✝ = A.invertibleTranspose
<VAR>n : Type u_2<VAR>α : Type u_3<VAR>Fintype n<VAR>DecidableEq n<VAR>CommSemiring α<VAR>A : Matrix n n α<GOAL>IsUnit Aᵀ ↔ IsUnit A
<VAR>R n : Type<VAR>CommSemiring R<VAR>Fintype n<VAR>DecidableEq n<VAR>d : DualNumber (Matrix n n R)<GOAL>Matrix.dualNumberEquiv.symm d = Matrix.of fun i j => (TrivSqZeroExt.fst d i j, TrivSqZeroExt.snd d i j)
<VAR>R n : Type<VAR>CommSemiring R<VAR>Fintype n<VAR>DecidableEq n<VAR>A : Matrix n n (DualNumber R)<GOAL>Matrix.dualNumberEquiv A = (Matrix.of fun i j => TrivSqZeroExt.fst (A i j), Matrix.of fun i j => TrivSqZeroExt.snd (A i j))
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>M : (i : ι) → Matroid (α i)<VAR>I : Set ((i : ι) × α i)<GOAL>(Matroid.sigma M).Indep I ↔ ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>M : (i : ι) → Matroid (α i)<VAR>B : Set ((i : ι) × α i)<GOAL>(Matroid.sigma M).Base B ↔ ∀ (i : ι), (M i).Base (Sigma.mk i ⁻¹' B)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>M : (i : ι) → Matroid (α i)<GOAL>(Matroid.sigma M).E = Set.univ.sigma fun i => (M i).E
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>M : (i : ι) → Matroid (α i)<VAR>h : ∀ (i : ι), (M i).Finitary<GOAL>(Matroid.sigma M).Finitary
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>M : ι → Matroid α<GOAL>(Matroid.sum' M).E = ⋃ i, Prod.mk i '' (M i).E
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>M : ι → Matroid α<VAR>I X : Set (ι × α)<GOAL>(Matroid.sum' M).Basis I X ↔ ∀ (i : ι), (M i).Basis (Prod.mk i ⁻¹' I) (Prod.mk i ⁻¹' X)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>M : ι → Matroid α<VAR>h : Pairwise (Disjoint on fun i => (M i).E)<GOAL>(Matroid.disjointSigma M h).E = ⋃ i, (M i).E
<VAR>α : Type u<VAR>β : Type v<VAR>M : Matroid α<VAR>N : Matroid β<GOAL>(M.sum N).E = Sum.inl '' M.E ∪ Sum.inr '' N.E
<VAR>α : Type u<VAR>β : Type v<VAR>M : Matroid α<VAR>N : Matroid β<VAR>I : Set (α ⊕ β)<GOAL>(M.sum N).Indep I ↔ M.Indep (Sum.inl ⁻¹' I) ∧ N.Indep (Sum.inr ⁻¹' I)
<VAR>α : Type u<VAR>β : Type v<VAR>M : Matroid α<VAR>N : Matroid β<VAR>B : Set (α ⊕ β)<GOAL>(M.sum N).Base B ↔ M.Base (Sum.inl ⁻¹' B) ∧ N.Base (Sum.inr ⁻¹' B)
<VAR>α : Type u<VAR>β : Type v<VAR>M : Matroid α<VAR>N : Matroid β<VAR>I X : Set (α ⊕ β)<GOAL>(M.sum N).Basis I X ↔ M.Basis (Sum.inl ⁻¹' I) (Sum.inl ⁻¹' X) ∧ N.Basis (Sum.inr ⁻¹' I) (Sum.inr ⁻¹' X)
<VAR>α : Type u_1<VAR>M N : Matroid α<VAR>h : Disjoint M.E N.E<GOAL>(M.disjointSum N h).E = M.E ∪ N.E
<VAR>α : Type u_1<VAR>m n : ℕ<VAR>P : Matrix (Fin m) (Fin n) α → Prop<GOAL>Matrix.Forall P ↔ ∀ (x : Matrix (Fin m) (Fin n) α), P x
<VAR>α : Type u_1<VAR>m n : ℕ<VAR>P : Matrix (Fin m) (Fin n) α → Prop<GOAL>Matrix.Exists P ↔ ∃ x, P x
<VAR>α : Type u_1<VAR>m n : ℕ<VAR>A : Matrix (Fin m) (Fin n) α<GOAL>A.transposeᵣ = Aᵀ
<VAR>α : Type u_1<VAR>Mul α<VAR>AddCommMonoid α<VAR>m : ℕ<VAR>a b : Fin m → α<GOAL>Matrix.dotProductᵣ a b = a ⬝ᵥ b
<VAR>l m n : ℕ<VAR>α : Type u_1<VAR>Mul α<VAR>AddCommMonoid α<VAR>A : Matrix (Fin l) (Fin m) α<VAR>B : Matrix (Fin m) (Fin n) α<GOAL>A.mulᵣ B = A * B
<VAR>l m : ℕ<VAR>α : Type u_1<VAR>NonUnitalNonAssocSemiring α<VAR>A : Matrix (Fin l) (Fin m) α<VAR>v : Fin m → α<GOAL>A.mulVecᵣ v = A *ᵥ v
<VAR>l m : ℕ<VAR>α : Type u_1<VAR>NonUnitalNonAssocSemiring α<VAR>v : Fin l → α<VAR>A : Matrix (Fin l) (Fin m) α<GOAL>Matrix.vecMulᵣ v A = v ᵥ* A
<VAR>α : Type u_1<VAR>m n : ℕ<VAR>A : Matrix (Fin m) (Fin n) α<GOAL>A.etaExpand = A
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>DecidableEq m<VAR>DecidableEq n<VAR>Semiring α<VAR>SMulZeroClass R α<VAR>r : R<VAR>i : m<VAR>j : n<VAR>a : α<GOAL>r • Matrix.stdBasisMatrix i j a = Matrix.stdBasisMatrix i j (r • a)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_5<VAR>DecidableEq m<VAR>DecidableEq n<VAR>Semiring α<VAR>i : m<VAR>j : n<GOAL>Matrix.stdBasisMatrix i j 0 = 0
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_5<VAR>DecidableEq m<VAR>DecidableEq n<VAR>Semiring α<VAR>i : m<VAR>j : n<VAR>a b : α<GOAL>Matrix.stdBasisMatrix i j (a + b) = Matrix.stdBasisMatrix i j a + Matrix.stdBasisMatrix i j b
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_5<VAR>DecidableEq m<VAR>DecidableEq n<VAR>Semiring α<VAR>Fintype m<VAR>i : n<VAR>j : m<VAR>c : α<VAR>x : m → α<GOAL>(Matrix.stdBasisMatrix i j c).mulVec x = Function.update 0 i (c * x j)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_5<VAR>DecidableEq m<VAR>DecidableEq n<VAR>Semiring α<VAR>Fintype m<VAR>Fintype n<VAR>x : Matrix m n α<GOAL>x = ∑ i : m, ∑ j : n, Matrix.stdBasisMatrix i j (x i j)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_5<VAR>DecidableEq m<VAR>DecidableEq n<VAR>Semiring α<VAR>i : m<VAR>j : n<GOAL>Matrix.stdBasisMatrix i j 1 = Matrix.vecMulVec (fun i' => if i = i' then 1 else 0) fun j' => if j = j' then 1 else 0
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_5<VAR>DecidableEq m<VAR>DecidableEq n<VAR>Semiring α<VAR>Finite m<VAR>Finite n<VAR>P : Matrix m n α → Prop<VAR>M : Matrix m n α<VAR>h_zero : P 0<VAR>h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)<VAR>h_std_basis : ∀ (i : m) (j : n) (x : α), P (Matrix.stdBasisMatrix i j x)<GOAL>P M
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_5<VAR>DecidableEq m<VAR>DecidableEq n<VAR>Semiring α<VAR>Finite m<VAR>Finite n<VAR>Nonempty m<VAR>Nonempty n<VAR>P : Matrix m n α → Prop<VAR>M : Matrix m n α<VAR>h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)<VAR>h_std_basis : ∀ (i : m) (j : n) (x : α), P (Matrix.stdBasisMatrix i j x)<GOAL>P M
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_5<VAR>DecidableEq m<VAR>DecidableEq n<VAR>Semiring α<VAR>i : m<VAR>j : n<VAR>c : α<GOAL>Matrix.stdBasisMatrix i j c i j = c
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_5<VAR>DecidableEq m<VAR>DecidableEq n<VAR>Semiring α<VAR>i : m<VAR>j : n<VAR>c : α<VAR>i' : m<VAR>j' : n<VAR>h : ¬(i = i' ∧ j = j')<GOAL>Matrix.stdBasisMatrix i j c i' j' = 0
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_5<VAR>DecidableEq m<VAR>DecidableEq n<VAR>Semiring α<VAR>i i' : m<VAR>hi : i ≠ i'<VAR>j j' : n<VAR>a : α<GOAL>Matrix.stdBasisMatrix i j a i' j' = 0
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_5<VAR>DecidableEq m<VAR>DecidableEq n<VAR>Semiring α<VAR>i i' : m<VAR>j j' : n<VAR>hj : j ≠ j'<VAR>a : α<GOAL>Matrix.stdBasisMatrix i j a i' j' = 0
<VAR>n : Type u_3<VAR>α : Type u_5<VAR>DecidableEq n<VAR>Semiring α<VAR>i j : n<VAR>c : α<VAR>h : j ≠ i<GOAL>(Matrix.stdBasisMatrix i j c).diag = 0
<VAR>n : Type u_3<VAR>α : Type u_5<VAR>DecidableEq n<VAR>Semiring α<VAR>i : n<VAR>c : α<GOAL>(Matrix.stdBasisMatrix i i c).diag = Pi.single i c
<VAR>n : Type u_3<VAR>α : Type u_5<VAR>DecidableEq n<VAR>Semiring α<VAR>i j : n<VAR>c : α<VAR>Fintype n<VAR>h : j ≠ i<GOAL>(Matrix.stdBasisMatrix i j c).trace = 0
<VAR>n : Type u_3<VAR>α : Type u_5<VAR>DecidableEq n<VAR>Semiring α<VAR>i : n<VAR>c : α<VAR>Fintype n<GOAL>(Matrix.stdBasisMatrix i i c).trace = c
<VAR>n : Type u_3<VAR>α : Type u_5<VAR>DecidableEq n<VAR>Semiring α<VAR>i j : n<VAR>c : α<VAR>Fintype n<VAR>b : n<VAR>M : Matrix n n α<GOAL>(Matrix.stdBasisMatrix i j c * M) i b = c * M j b
<VAR>n : Type u_3<VAR>α : Type u_5<VAR>DecidableEq n<VAR>Semiring α<VAR>i j : n<VAR>c : α<VAR>Fintype n<VAR>a : n<VAR>M : Matrix n n α<GOAL>(M * Matrix.stdBasisMatrix i j c) a j = M a i * c
<VAR>n : Type u_3<VAR>α : Type u_5<VAR>DecidableEq n<VAR>Semiring α<VAR>i j : n<VAR>c : α<VAR>Fintype n<VAR>a b : n<VAR>h : a ≠ i<VAR>M : Matrix n n α<GOAL>(Matrix.stdBasisMatrix i j c * M) a b = 0
<VAR>n : Type u_3<VAR>α : Type u_5<VAR>DecidableEq n<VAR>Semiring α<VAR>i j : n<VAR>c : α<VAR>Fintype n<VAR>a b : n<VAR>hbj : b ≠ j<VAR>M : Matrix n n α<GOAL>(M * Matrix.stdBasisMatrix i j c) a b = 0
<VAR>n : Type u_3<VAR>α : Type u_5<VAR>DecidableEq n<VAR>Semiring α<VAR>i j : n<VAR>c : α<VAR>Fintype n<VAR>k : n<VAR>d : α<GOAL>Matrix.stdBasisMatrix i j c * Matrix.stdBasisMatrix j k d = Matrix.stdBasisMatrix i k (c * d)
<VAR>n : Type u_3<VAR>α : Type u_5<VAR>DecidableEq n<VAR>Semiring α<VAR>i j : n<VAR>c : α<VAR>Fintype n<VAR>k l : n<VAR>h : j ≠ k<VAR>d : α<GOAL>Matrix.stdBasisMatrix i j c * Matrix.stdBasisMatrix k l d = 0
<VAR>n : Type u_3<VAR>α : Type u_5<VAR>DecidableEq n<VAR>Semiring α<VAR>Fintype n<VAR>i j k : n<VAR>M : Matrix n n α<VAR>hM : Commute (Matrix.stdBasisMatrix i j 1) M<VAR>hkj : k ≠ j<GOAL>M j k = 0
<VAR>n : Type u_3<VAR>α : Type u_5<VAR>DecidableEq n<VAR>Semiring α<VAR>Fintype n<VAR>i j k : n<VAR>M : Matrix n n α<VAR>hM : Commute (Matrix.stdBasisMatrix i j 1) M<VAR>hki : k ≠ i<GOAL>M k i = 0
<VAR>n : Type u_3<VAR>α : Type u_5<VAR>DecidableEq n<VAR>Semiring α<VAR>Fintype n<VAR>i j : n<VAR>M : Matrix n n α<VAR>hM : Commute (Matrix.stdBasisMatrix i j 1) M<GOAL>M i i = M j j
<VAR>n : Type u_3<VAR>α : Type u_5<VAR>DecidableEq n<VAR>Semiring α<VAR>Fintype n<VAR>M : Matrix n n α<VAR>hM : Pairwise fun i j => Commute (Matrix.stdBasisMatrix i j 1) M<GOAL>M ∈ Set.range ⇑(Matrix.scalar n)
<VAR>n : Type u_3<VAR>α : Type u_5<VAR>DecidableEq n<VAR>Semiring α<VAR>Fintype n<VAR>M : Matrix n n α<GOAL>M ∈ Set.range ⇑(Matrix.scalar n) ↔ ∀ (i j : n), i ≠ j → Commute (Matrix.stdBasisMatrix i j 1) M
<VAR>n : Type u_3<VAR>α : Type u_5<VAR>DecidableEq n<VAR>Semiring α<VAR>Fintype n<VAR>M : Matrix n n α<GOAL>M ∈ Set.range ⇑(Matrix.scalar n) ↔ ∀ (i j : n), Commute (Matrix.stdBasisMatrix i j 1) M
<VAR>n : ℕ<VAR>A : Type u<VAR>α : TypeVec.{u} n<VAR>x : MvQPF.Const n A α<GOAL>MvQPF.Const.mk x.get = x
<VAR>n : ℕ<VAR>A : Type u<VAR>α : TypeVec.{u} n<VAR>x : A<GOAL>(MvQPF.Const.mk x).get = x
<VAR>n : ℕ<VAR>A : Type u<VAR>α β : TypeVec.{u} n<VAR>f : α.Arrow β<VAR>x : A<GOAL>MvFunctor.map f (MvQPF.Const.mk x) = MvQPF.Const.mk x
<VAR>n : ℕ<VAR>A : Type u<VAR>α β : TypeVec.{u} n<VAR>f : α.Arrow β<VAR>x : MvQPF.Const n A α<GOAL>(MvFunctor.map f x).get = x.get
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a : α<VAR>v : Vector3 α n<GOAL>Vector3.cons a v Fin2.fz = a
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a : α<VAR>v : Vector3 α n<VAR>i : Fin2 n<GOAL>Vector3.cons a v i.fs = v i
<VAR>α : Type u_1<VAR>v : Vector3 α 0<GOAL>v = []
<VAR>α : Type u_1<VAR>n : ℕ<VAR>v : Vector3 α (n + 1)<GOAL>Vector3.cons v.head v.tail = v
<VAR>α : Type u_1<VAR>n : ℕ<VAR>C : Vector3 α (n + 1) → Sort u_2<VAR>H : (a : α) → (t : Vector3 α n) → C (Vector3.cons a t)<VAR>a : α<VAR>t : Vector3 α n<GOAL>Vector3.consElim H (Vector3.cons a t) = H a t
<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)<GOAL>[].recOn H0 Hs = H0