ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a a' : α<VAR>s : Finmap β<VAR>h : a ≠ a'<GOAL>Finmap.lookup a (Finmap.erase a' s) = Finmap.lookup a s
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a a' : α<VAR>s : Finmap β<GOAL>Finmap.erase a (Finmap.erase a' s) = Finmap.erase a' (Finmap.erase a s)
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>s : AList β<GOAL>Finmap.insert a b ⟦s⟧ = ⟦AList.insert a b s⟧
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>s : Finmap β<GOAL>a ∉ s → (Finmap.insert a b s).entries = ⟨a, b⟩ ::ₘ s.entries
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a a' : α<VAR>b' : β a'<VAR>s : Finmap β<GOAL>a ∈ Finmap.insert a' b' s ↔ a = a' ∨ a ∈ s
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>s : Finmap β<GOAL>Finmap.lookup a (Finmap.insert a b s) = some b
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a a' : α<VAR>b : β a<VAR>s : Finmap β<VAR>h : a' ≠ a<GOAL>Finmap.lookup a' (Finmap.insert a b s) = Finmap.lookup a' s
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b b' : β a<VAR>s : Finmap β<GOAL>Finmap.insert a b' (Finmap.insert a b s) = Finmap.insert a b' s
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a a' : α<VAR>b : β a<VAR>b' : β a'<VAR>s : Finmap β<VAR>h : a ≠ a'<GOAL>Finmap.insert a' b' (Finmap.insert a b s) = Finmap.insert a b (Finmap.insert a' b' s)
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>xs : List (Sigma β)<GOAL>(⟨a, b⟩ :: xs).toFinmap = Finmap.insert a b xs.toFinmap
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>xs : List (Sigma β)<GOAL>a ∈ xs.toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ xs
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b b' : β a<GOAL>Finmap.insert a b (Finmap.singleton a b') = Finmap.singleton a b
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>s : Finmap β<GOAL>Finmap.extract a s = (Finmap.lookup a s, Finmap.erase a s)
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>s₁ s₂ : Finmap β<GOAL>a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ ∨ a ∈ s₂
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>s₁ s₂ : AList β<GOAL>⟦s₁⟧ ∪ ⟦s₂⟧ = ⟦s₁ ∪ s₂⟧
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>s₁ s₂ : Finmap β<GOAL>(s₁ ∪ s₂).keys = s₁.keys ∪ s₂.keys
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>s₁ s₂ : Finmap β<GOAL>a ∈ s₁ → Finmap.lookup a (s₁ ∪ s₂) = Finmap.lookup a s₁
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>s₁ s₂ : Finmap β<GOAL>a ∉ s₁ → Finmap.lookup a (s₁ ∪ s₂) = Finmap.lookup a s₂
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>s₁ s₂ : Finmap β<VAR>h : a ∉ s₂<GOAL>Finmap.lookup a (s₁ ∪ s₂) = Finmap.lookup a s₁
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>s₁ s₂ : Finmap β<GOAL>b ∈ Finmap.lookup a (s₁ ∪ s₂) ↔ b ∈ Finmap.lookup a s₁ ∨ a ∉ s₁ ∧ b ∈ Finmap.lookup a s₂
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>s₁ s₂ s₃ : Finmap β<GOAL>b ∈ Finmap.lookup a (s₁ ∪ s₃) → a ∉ s₂ → b ∈ Finmap.lookup a (s₁ ∪ s₂ ∪ s₃)
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>s₁ s₂ : Finmap β<GOAL>Finmap.insert a b (s₁ ∪ s₂) = Finmap.insert a b s₁ ∪ s₂
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>s₁ s₂ s₃ : Finmap β<GOAL>s₁ ∪ s₂ ∪ s₃ = s₁ ∪ (s₂ ∪ s₃)
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>s₁ : Finmap β<GOAL>∅ ∪ s₁ = s₁
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>s₁ : Finmap β<GOAL>s₁ ∪ ∅ = s₁
<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>Finmap.erase a s ∪ Finmap.singleton a b = s
<VAR>α : Type u<VAR>β : α → Type v<VAR>x : Finmap β<GOAL>∅.Disjoint x
<VAR>α : Type u<VAR>β : α → Type v<VAR>x y : Finmap β<VAR>h : x.Disjoint y<GOAL>y.Disjoint x
<VAR>α : Type u<VAR>β : α → Type v<VAR>x y : Finmap β<GOAL>x.Disjoint y ↔ y.Disjoint x
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>x y z : Finmap β<GOAL>(x ∪ y).Disjoint z ↔ x.Disjoint z ∧ y.Disjoint z
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>x y z : Finmap β<GOAL>x.Disjoint (y ∪ z) ↔ x.Disjoint y ∧ x.Disjoint z
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>s₁ s₂ : Finmap β<GOAL>s₁.Disjoint s₂ → s₁ ∪ s₂ = s₂ ∪ s₁
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>s₁ s₂ s₃ : Finmap β<VAR>h : s₁.Disjoint s₃<VAR>h' : s₂.Disjoint s₃<GOAL>s₁ ∪ s₃ = s₂ ∪ s₃ ↔ s₁ = s₂
<VAR>α : Type u_2<VAR>self : IndepMatroid α<VAR>I B : Set α<GOAL>self.Indep I → I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | self.Indep I} → B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | self.Indep I} → ∃ x ∈ B \ I, self.Indep (insert x I)
<VAR>α : Type u_2<VAR>self : IndepMatroid α<GOAL>self.Indep ∅
<VAR>α : Type u_2<VAR>self : IndepMatroid α<VAR>I : Set α<GOAL>self.Indep I → I ⊆ self.E
<VAR>α : Type u_2<VAR>self : IndepMatroid α<VAR>X : Set α<GOAL>X ⊆ self.E → Matroid.ExistsMaximalSubsetProperty self.Indep X
<VAR>α : Type u_2<VAR>self : IndepMatroid α<VAR>I J : Set α<GOAL>self.Indep J → I ⊆ J → self.Indep I
<VAR>α : Type u_1<VAR>M : IndepMatroid α<GOAL>M.matroid.E = M.E
<VAR>α : Type u_1<VAR>M : IndepMatroid α<GOAL>∀ (x : Set α), M.matroid.Base x = (x ∈ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I})
<VAR>α : Type u_1<VAR>M : IndepMatroid α<GOAL>∀ (a : Set α), M.matroid.Indep a = M.Indep a
<VAR>α : Type u_1<VAR>M : IndepMatroid α<VAR>I : Set α<GOAL>M.matroid.Indep I ↔ M.Indep I
<VAR>α : Type u_1<VAR>E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<GOAL>(IndepMatroid.ofFinitary E Indep indep_empty indep_subset indep_aug indep_compact subset_ground).E = E
<VAR>α : Type u_1<VAR>E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<GOAL>(IndepMatroid.ofFinitary E Indep indep_empty indep_subset indep_aug indep_compact subset_ground).Indep = Indep
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>hP : ∃ n, ∀ (Y : Set α), P Y → Y.encard ≤ ↑n<VAR>X : Set α<GOAL>Matroid.ExistsMaximalSubsetProperty P X
<VAR>α : Type u_1<VAR>E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I B : Set α⦄, Indep I → I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | Indep I} → B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | Indep I} → ∃ x ∈ B \ I, Indep (insert x I)<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>indep_bdd : ∃ n, ∀ (I : Set α), Indep I → I.encard ≤ ↑n<GOAL>(IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground indep_bdd).E = E
<VAR>α : Type u_1<VAR>E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I B : Set α⦄, Indep I → I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | Indep I} → B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | Indep I} → ∃ x ∈ B \ I, Indep (insert x I)<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>h_bdd : ∃ n, ∀ (I : Set α), Indep I → I.encard ≤ ↑n<GOAL>(IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground h_bdd).Indep = Indep
<VAR>α : Type u_1<VAR>E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_bdd : ∃ n, ∀ (I : Set α), Indep I → I.encard ≤ ↑n<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<GOAL>(IndepMatroid.ofBddAugment E Indep indep_empty indep_subset indep_aug indep_bdd subset_ground).E = E
<VAR>α : Type u_1<VAR>E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_bdd : ∃ n, ∀ (I : Set α), Indep I → I.encard ≤ ↑n<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<GOAL>(IndepMatroid.ofBddAugment E Indep indep_empty indep_subset indep_aug indep_bdd subset_ground).Indep = Indep
<VAR>α : Type u_1<VAR>E : Set α<VAR>hE : E.Finite<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>subset_ground : ∀ ⦃I : Set α⦄, Indep I → I ⊆ E<GOAL>(IndepMatroid.ofFinite hE Indep indep_empty indep_subset indep_aug subset_ground).E = E
<VAR>α : Type u_1<VAR>E : Set α<VAR>hE : E.Finite<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>subset_ground : ∀ ⦃I : Set α⦄, Indep I → I ⊆ E<GOAL>(IndepMatroid.ofFinite hE Indep indep_empty indep_subset indep_aug subset_ground).Indep = Indep
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>E : Set α<VAR>Indep : Finset α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>subset_ground : ∀ ⦃I : Finset α⦄, Indep I → ↑I ⊆ E<GOAL>(IndepMatroid.ofFinset E Indep indep_empty indep_subset indep_aug subset_ground).E = E
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>E : Set α<VAR>Indep : Finset α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>subset_ground : ∀ ⦃I : Finset α⦄, Indep I → ↑I ⊆ E<VAR>I : Finset α<GOAL>(IndepMatroid.ofFinset E Indep indep_empty indep_subset indep_aug subset_ground).Indep ↑I ↔ Indep I
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>E : Set α<VAR>Indep : Finset α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>subset_ground : ∀ ⦃I : Finset α⦄, Indep I → ↑I ⊆ E<VAR>I : Set α<GOAL>(IndepMatroid.ofFinset E Indep indep_empty indep_subset indep_aug subset_ground).Indep I ↔ ∀ (J : Finset α), ↑J ⊆ I → Indep J
<VAR>α : Type u_1<VAR>E : Set α<VAR>Indep : Set α → Prop<VAR>hM : ∃ M, E = M.E ∧ ∀ (I : Set α), M.Indep I ↔ Indep I<GOAL>(Matroid.ofExistsMatroid E Indep hM).E = E
<VAR>α : Type u_1<VAR>E : Set α<VAR>Base : Set α → Prop<VAR>exists_base : ∃ B, Base B<VAR>base_exchange : Matroid.ExchangeProperty Base<VAR>maximality : ∀ X ⊆ E, Matroid.ExistsMaximalSubsetProperty (fun x => ∃ B, Base B ∧ x ⊆ B) X<VAR>subset_ground : ∀ (B : Set α), Base B → B ⊆ E<GOAL>(Matroid.ofBase E Base exists_base base_exchange maximality subset_ground).E = E
<VAR>α : Type u_1<VAR>E : Set α<VAR>Base : Set α → Prop<VAR>exists_finite_base : ∃ B, Base B ∧ B.Finite<VAR>base_exchange : Matroid.ExchangeProperty Base<VAR>subset_ground : ∀ (B : Set α), Base B → B ⊆ E<GOAL>(Matroid.ofExistsFiniteBase E Base exists_finite_base base_exchange subset_ground).E = E
<VAR>α : Type u_1<VAR>E : Set α<VAR>Base : Set α → Prop<VAR>exists_finite_base : ∃ B, Base B ∧ B.Finite<VAR>base_exchange : Matroid.ExchangeProperty Base<VAR>subset_ground : ∀ (B : Set α), Base B → B ⊆ E<GOAL>(Matroid.ofExistsFiniteBase E Base exists_finite_base base_exchange subset_ground).Base = Base
<VAR>α : Type u_1<VAR>E : Set α<VAR>hE : E.Finite<VAR>Base : Set α → Prop<VAR>exists_base : ∃ B, Base B<VAR>base_exchange : Matroid.ExchangeProperty Base<VAR>subset_ground : ∀ (B : Set α), Base B → B ⊆ E<GOAL>(Matroid.ofBaseOfFinite hE Base exists_base base_exchange subset_ground).E = E
<VAR>α : Type u_1<VAR>E : Set α<VAR>hE : E.Finite<VAR>Base : Set α → Prop<VAR>exists_base : ∃ B, Base B<VAR>base_exchange : Matroid.ExchangeProperty Base<VAR>subset_ground : ∀ (B : Set α), Base B → B ⊆ E<GOAL>(Matroid.ofBaseOfFinite hE Base exists_base base_exchange subset_ground).Base = Base
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<GOAL>(↑l).lists = l.permutations.toFinset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<VAR>l : List α<GOAL>l ∈ s.lists ↔ s = ⟦l⟧
<VAR>α : Type u_1<VAR>AddCommMonoid α<VAR>f : Bool → α<GOAL>∑ b : Bool, f b = f true + f false
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>f : Bool → α<GOAL>∏ b : Bool, f b = f true * f false
<VAR>α : Type u_4<VAR>Fintype α<GOAL>Fintype.card α = ∑ _a : α, 1
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>AddCommMonoid α<VAR>s : Finset ι<VAR>f : ι → α<GOAL>(∑ i : ι, if i ∈ s then f i else 0) = ∑ i ∈ s, f i
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>CommMonoid α<VAR>s : Finset ι<VAR>f : ι → α<GOAL>(∏ i : ι, if i ∈ s then f i else 1) = ∏ i ∈ s, f i
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Fintype α<VAR>AddCommMonoid M<VAR>f : α → M<VAR>h : ∀ (a : α), f a = 0<GOAL>∑ a : α, f a = 0
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Fintype α<VAR>CommMonoid M<VAR>f : α → M<VAR>h : ∀ (a : α), f a = 1<GOAL>∏ a : α, f a = 1
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Fintype α<VAR>CommMonoid M<VAR>f g : α → M<VAR>h : ∀ (a : α), f a = g a<GOAL>∏ a : α, f a = ∏ a : α, g a
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Fintype α<VAR>AddCommMonoid M<VAR>f g : α → M<VAR>h : ∀ (a : α), f a = g a<GOAL>∑ a : α, f a = ∑ a : α, g a
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Fintype α<VAR>AddCommMonoid M<VAR>f : α → M<VAR>a : α<VAR>h : ∀ (x : α), x ≠ a → f x = 0<GOAL>∑ x : α, f x = f a
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Fintype α<VAR>CommMonoid M<VAR>f : α → M<VAR>a : α<VAR>h : ∀ (x : α), x ≠ a → f x = 1<GOAL>∏ x : α, f x = f a
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Fintype α<VAR>AddCommMonoid M<VAR>f : α → M<VAR>a b : α<VAR>h₁ : a ≠ b<VAR>h₂ : ∀ (x : α), x ≠ a ∧ x ≠ b → f x = 0<GOAL>∑ x : α, f x = f a + f b
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Fintype α<VAR>CommMonoid M<VAR>f : α → M<VAR>a b : α<VAR>h₁ : a ≠ b<VAR>h₂ : ∀ (x : α), x ≠ a ∧ x ≠ b → f x = 1<GOAL>∏ x : α, f x = f a * f b
<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>ι : Type u_5<VAR>Subsingleton ι<VAR>s : Finset ι<VAR>f : ι → M<VAR>b : M<VAR>h : ∑ i ∈ s, f i = b<VAR>i : ι<GOAL>i ∈ s → f i = b
<VAR>M : Type u_4<VAR>CommMonoid M<VAR>ι : Type u_5<VAR>Subsingleton ι<VAR>s : Finset ι<VAR>f : ι → M<VAR>b : M<VAR>h : ∏ i ∈ s, f i = b<VAR>i : ι<GOAL>i ∈ s → f i = b
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Fintype α<VAR>AddCommMonoid M<VAR>f : Option α → M<GOAL>∑ i : Option α, f i = f none + ∑ i : α, f (some i)
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>Fintype α<VAR>CommMonoid M<VAR>f : Option α → M<GOAL>∏ i : Option α, f i = f none * ∏ i : α, f (some i)
<VAR>ι : Type u_4<VAR>α : ι → Type u_6<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>t : (i : ι) → Finset (α i)<GOAL>(s.pi t).card = ∏ i ∈ s, (t i).card
<VAR>ι : Type u_4<VAR>α : ι → Type u_6<VAR>DecidableEq ι<VAR>Fintype ι<VAR>s : (i : ι) → Finset (α i)<GOAL>(Fintype.piFinset s).card = ∏ i : ι, (s i).card
<VAR>α : Type u_7<VAR>s : Finset α<VAR>n : ℕ<GOAL>(Fintype.piFinset fun x => s).card = s.card ^ n
<VAR>ι : Type u_4<VAR>α : ι → Type u_6<VAR>Fintype ι<VAR>DecidableEq ι<VAR>(i : ι) → Fintype (α i)<GOAL>Fintype.card ((i : ι) → α i) = ∏ i : ι, Fintype.card (α i)
<VAR>α : Type u_7<VAR>Fintype α<VAR>n : ℕ<GOAL>Fintype.card (Fin n → α) = Fintype.card α ^ n
<VAR>ι : Type u_4<VAR>α : ι → Type u_6<VAR>Fintype ι<VAR>(i : ι) → Fintype (α i)<GOAL>Fintype.card (Sigma α) = ∑ i : ι, Fintype.card (α i)
<VAR>ι : Type u_4<VAR>α : ι → Type u_6<VAR>DecidableEq ι<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (α i)<VAR>s : (i : ι) → Finset (α i)<VAR>i : ι<VAR>a : α i<VAR>ha : a ∈ s i<GOAL>(Finset.filter (fun f => f i = a) (Fintype.piFinset s)).card = ∏ j ∈ Finset.univ.erase i, (s j).card
<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>DecidableEq ι<VAR>DecidableEq κ<VAR>Fintype ι<VAR>s : Finset κ<VAR>i : ι<VAR>x : κ<VAR>hx : x ∈ s<GOAL>(Finset.filter (fun f => f i = x) (Fintype.piFinset fun x => s)).card = s.card ^ (Fintype.card ι - 1)
<VAR>ι : Type u_4<VAR>α : ι → Type u_6<VAR>DecidableEq ι<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (α i)<VAR>s : (i : ι) → Finset (α i)<VAR>i : ι<VAR>a : α i<GOAL>(Finset.filter (fun f => f i = a) (Fintype.piFinset s)).card = if a ∈ s i then ∏ b ∈ Finset.univ.erase i, (s b).card else 0
<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>DecidableEq ι<VAR>DecidableEq κ<VAR>Fintype ι<VAR>s : Finset κ<VAR>i : ι<VAR>j : κ<GOAL>(Finset.filter (fun f => f i = j) (Fintype.piFinset fun x => s)).card = if j ∈ s then s.card ^ (Fintype.card ι - 1) else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq α<VAR>Fintype α<VAR>Fintype β<GOAL>Fintype.card (α → β) = Fintype.card β ^ Fintype.card α
<VAR>α : Type u_1<VAR>Fintype α<VAR>n : ℕ<GOAL>Fintype.card (Mathlib.Vector α n) = Fintype.card α ^ n
<VAR>α : Type u_1<VAR>AddCommMonoid α<VAR>f : ℕ → α<VAR>n : ℕ<GOAL>∑ i : Fin n, f ↑i = ∑ i ∈ Finset.range n, f i
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>f : ℕ → α<VAR>n : ℕ<GOAL>∏ i : Fin n, f ↑i = ∏ i ∈ Finset.range n, f i
<VAR>β : Type u_2<VAR>AddCommMonoid β<VAR>n : ℕ<VAR>c : Fin n → β<GOAL>∑ i : Fin n, c i = ∑ i ∈ Finset.range n, if h : i < n then c ⟨i, h⟩ else 0
<VAR>β : Type u_2<VAR>CommMonoid β<VAR>n : ℕ<VAR>c : Fin n → β<GOAL>∏ i : Fin n, c i = ∏ i ∈ Finset.range n, if h : i < n then c ⟨i, h⟩ else 1
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>CommMonoid M<VAR>Fintype α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : α → M<GOAL>∏ a ∈ {x | p x}.toFinset, f a = ∏ a : Subtype p, f ↑a
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>Fintype α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : α → M<GOAL>∑ a ∈ {x | p x}.toFinset, f a = ∑ a : Subtype p, f ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>CommMonoid β<VAR>f : (a : α) → p a → β<VAR>g : (a : α) → ¬p a → β<GOAL>∏ a : α, dite (p a) (f a) (g a) = (∏ a : { a // p a }, f ↑a ⋯) * ∏ a : { a // ¬p a }, g ↑a ⋯
<VAR>α₁ : Type u_4<VAR>α₂ : Type u_5<VAR>M : Type u_6<VAR>Fintype α₁<VAR>Fintype α₂<VAR>CommMonoid M<VAR>f : α₁ → M<VAR>g : α₂ → M<GOAL>∏ x : α₁ ⊕ α₂, Sum.elim f g x = (∏ a₁ : α₁, f a₁) * ∏ a₂ : α₂, g a₂
<VAR>α₁ : Type u_4<VAR>α₂ : Type u_5<VAR>M : Type u_6<VAR>Fintype α₁<VAR>Fintype α₂<VAR>AddCommMonoid M<VAR>f : α₁ → M<VAR>g : α₂ → M<GOAL>∑ x : α₁ ⊕ α₂, Sum.elim f g x = ∑ a₁ : α₁, f a₁ + ∑ a₂ : α₂, g a₂
<VAR>α₁ : Type u_4<VAR>α₂ : Type u_5<VAR>M : Type u_6<VAR>Fintype α₁<VAR>Fintype α₂<VAR>CommMonoid M<VAR>f : α₁ ⊕ α₂ → M<GOAL>∏ x : α₁ ⊕ α₂, f x = (∏ a₁ : α₁, f (Sum.inl a₁)) * ∏ a₂ : α₂, f (Sum.inr a₂)
<VAR>α₁ : Type u_4<VAR>α₂ : Type u_5<VAR>M : Type u_6<VAR>Fintype α₁<VAR>Fintype α₂<VAR>AddCommMonoid M<VAR>f : α₁ ⊕ α₂ → M<GOAL>∑ x : α₁ ⊕ α₂, f x = ∑ a₁ : α₁, f (Sum.inl a₁) + ∑ a₂ : α₂, f (Sum.inr a₂)
<VAR>γ : Type u_3<VAR>α₁ : Type u_4<VAR>α₂ : Type u_5<VAR>Fintype α₁<VAR>Fintype α₂<VAR>CommMonoid γ<VAR>f : α₁ × α₂ → γ<GOAL>∏ x : α₁ × α₂, f x = ∏ x : α₁, ∏ y : α₂, f (x, y)
<VAR>γ : Type u_3<VAR>α₁ : Type u_4<VAR>α₂ : Type u_5<VAR>Fintype α₁<VAR>Fintype α₂<VAR>AddCommMonoid γ<VAR>f : α₁ × α₂ → γ<GOAL>∑ x : α₁ × α₂, f x = ∑ x : α₁, ∑ y : α₂, f (x, y)
<VAR>γ : Type u_3<VAR>α₁ : Type u_4<VAR>α₂ : Type u_5<VAR>Fintype α₁<VAR>Fintype α₂<VAR>AddCommMonoid γ<VAR>f : α₁ → α₂ → γ<GOAL>∑ x : α₁ × α₂, f x.1 x.2 = ∑ x : α₁, ∑ y : α₂, f x y
<VAR>γ : Type u_3<VAR>α₁ : Type u_4<VAR>α₂ : Type u_5<VAR>Fintype α₁<VAR>Fintype α₂<VAR>CommMonoid γ<VAR>f : α₁ → α₂ → γ<GOAL>∏ x : α₁ × α₂, f x.1 x.2 = ∏ x : α₁, ∏ y : α₂, f x y
<VAR>γ : Type u_3<VAR>α₁ : Type u_4<VAR>α₂ : Type u_5<VAR>Fintype α₁<VAR>Fintype α₂<VAR>CommMonoid γ<VAR>f : α₁ × α₂ → γ<GOAL>∏ x : α₁ × α₂, f x = ∏ y : α₂, ∏ x : α₁, f (x, y)
<VAR>γ : Type u_3<VAR>α₁ : Type u_4<VAR>α₂ : Type u_5<VAR>Fintype α₁<VAR>Fintype α₂<VAR>AddCommMonoid γ<VAR>f : α₁ × α₂ → γ<GOAL>∑ x : α₁ × α₂, f x = ∑ y : α₂, ∑ x : α₁, f (x, y)
<VAR>γ : Type u_3<VAR>α₁ : Type u_4<VAR>α₂ : Type u_5<VAR>Fintype α₁<VAR>Fintype α₂<VAR>CommMonoid γ<VAR>f : α₁ → α₂ → γ<GOAL>∏ x : α₁ × α₂, f x.1 x.2 = ∏ y : α₂, ∏ x : α₁, f x y
<VAR>γ : Type u_3<VAR>α₁ : Type u_4<VAR>α₂ : Type u_5<VAR>Fintype α₁<VAR>Fintype α₂<VAR>AddCommMonoid γ<VAR>f : α₁ → α₂ → γ<GOAL>∑ x : α₁ × α₂, f x.1 x.2 = ∑ y : α₂, ∑ x : α₁, f x y
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>LinearOrder α<VAR>m n : ℕ<VAR>s : Finset α<VAR>hm : s.card = m<VAR>hn : sᶜ.card = n<VAR>i : Fin m<GOAL>(finSumEquivOfFinset hm hn) (Sum.inl i) = (s.orderEmbOfFin hm) i
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>LinearOrder α<VAR>m n : ℕ<VAR>s : Finset α<VAR>hm : s.card = m<VAR>hn : sᶜ.card = n<VAR>i : Fin n<GOAL>(finSumEquivOfFinset hm hn) (Sum.inr i) = (sᶜ.orderEmbOfFin hn) i
<VAR>l : List Bool<VAR>b : Bool<GOAL>List.count (!b) l + List.count b l = l.length
<VAR>l : List Bool<VAR>b : Bool<GOAL>List.count b l + List.count (!b) l = l.length
<VAR>l : List Bool<GOAL>List.count false l + List.count true l = l.length
<VAR>l : List Bool<GOAL>List.count true l + List.count false l = l.length
<VAR>b : Bool<VAR>l : List Bool<GOAL>List.Chain (fun x x_1 => x ≠ x_1) b l → List.count (!b) l = List.count b l + l.length % 2
<VAR>l : List Bool<VAR>hl : List.Chain' (fun x x_1 => x ≠ x_1) l<VAR>h2 : Even l.length<VAR>b : Bool<GOAL>List.count (!b) l = List.count b l
<VAR>l : List Bool<VAR>hl : List.Chain' (fun x x_1 => x ≠ x_1) l<VAR>h2 : Even l.length<GOAL>List.count false l = List.count true l
<VAR>l : List Bool<VAR>hl : List.Chain' (fun x x_1 => x ≠ x_1) l<VAR>b : Bool<GOAL>List.count (!b) l ≤ List.count b l + 1
<VAR>l : List Bool<VAR>hl : List.Chain' (fun x x_1 => x ≠ x_1) l<GOAL>List.count false l ≤ List.count true l + 1
<VAR>l : List Bool<VAR>hl : List.Chain' (fun x x_1 => x ≠ x_1) l<GOAL>List.count true l ≤ List.count false l + 1
<VAR>l : List Bool<VAR>hl : List.Chain' (fun x x_1 => x ≠ x_1) l<VAR>h2 : Even l.length<VAR>b : Bool<GOAL>2 * List.count b l = l.length
<VAR>l : List Bool<VAR>hl : List.Chain' (fun x x_1 => x ≠ x_1) l<VAR>b : Bool<GOAL>2 * List.count b l = if Even l.length then l.length else if (some b == l.head?) = true then l.length + 1 else l.length - 1
<VAR>l : List Bool<VAR>hl : List.Chain' (fun x x_1 => x ≠ x_1) l<VAR>b : Bool<GOAL>l.length - 1 ≤ 2 * List.count b l
<VAR>l : List Bool<VAR>hl : List.Chain' (fun x x_1 => x ≠ x_1) l<VAR>b : Bool<GOAL>l.length / 2 ≤ List.count b l
<VAR>l : List Bool<VAR>hl : List.Chain' (fun x x_1 => x ≠ x_1) l<VAR>b : Bool<GOAL>2 * List.count b l ≤ l.length + 1
<VAR>α : Type u_1<VAR>Fintype α<GOAL>Fintype.card (Finset α) = 2 ^ Fintype.card α
<VAR>α : Type u_1<VAR>Fintype α<GOAL>Finset.univ.powerset = Finset.univ
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>s : Finset α<GOAL>Finset.filter (fun t => t ⊆ s) Finset.univ = s.powerset
<VAR>α : Type u_1<VAR>Fintype α<VAR>s : Finset α<GOAL>s.powerset = Finset.univ ↔ s = Finset.univ
<VAR>α : Type u_1<VAR>Fintype α<VAR>s : Finset α<VAR>k : ℕ<GOAL>s ∈ Finset.powersetCard k Finset.univ ↔ s.card = k
<VAR>α : Type u_1<VAR>Fintype α<VAR>k : ℕ<GOAL>Finset.filter (fun s => s.card = k) Finset.univ = Finset.powersetCard k Finset.univ
<VAR>α : Type u_1<VAR>Fintype α<VAR>k : ℕ<GOAL>Fintype.card { s // s.card = k } = (Fintype.card α).choose k
<VAR>α : Type u_1<VAR>Fintype α<GOAL>Fintype.card (Set α) = 2 ^ Fintype.card α
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsTrans α r<VAR>γ : Type u_3<VAR>Nonempty γ<VAR>f : γ → α<VAR>D : Directed r f<VAR>s : Set γ<VAR>hs : s.Finite<GOAL>∃ z, ∀ i ∈ s, r (f i) (f z)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsTrans α r<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Nonempty γ<VAR>f : γ → α<VAR>Finite β<VAR>D : Directed r f<VAR>g : β → γ<GOAL>∃ z, ∀ (i : β), r (f (g i)) (f z)
<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 : β), f i ≤ M