ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>AddCommGroup α<VAR>s : Finset α<VAR>t : Finset α<VAR>ht : t.Nonempty<GOAL>∃ u, u.card * t.card ≤ (s + t).card ∧ s ⊆ u + t - t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>CommGroup α<VAR>s : Finset α<VAR>t : Finset α<VAR>ht : t.Nonempty<GOAL>∃ u, u.card * t.card ≤ (s * t).card ∧ s ⊆ u * t / t
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>s t : Set α<VAR>hs : s.Finite<VAR>ht' : t.Finite<VAR>ht : t.Nonempty<GOAL>∃ u, Nat.card ↑u * Nat.card ↑t ≤ Nat.card ↑(s + t) ∧ s ⊆ u + t - t ∧ u.Finite
<VAR>α : Type u_1<VAR>CommGroup α<VAR>s t : Set α<VAR>hs : s.Finite<VAR>ht' : t.Finite<VAR>ht : t.Nonempty<GOAL>∃ u, Nat.card ↑u * Nat.card ↑t ≤ Nat.card ↑(s * t) ∧ s ⊆ u * t / t ∧ u.Finite
<VAR>α : Type u_1<VAR>G : SimpleGraph α<GOAL>G.LocallyLinear → G.EdgeDisjointTriangles
<VAR>α : Type u_1<VAR>G H : SimpleGraph α<VAR>h : G ≤ H<VAR>hH : H.EdgeDisjointTriangles<GOAL>G.EdgeDisjointTriangles
<VAR>α : Type u_1<GOAL>⊥.EdgeDisjointTriangles
<VAR>α : Type u_1<GOAL>⊥.LocallyLinear
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>f : α ↪ β<VAR>hG : G.EdgeDisjointTriangles<GOAL>(SimpleGraph.map f G).EdgeDisjointTriangles
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>f : α ↪ β<VAR>hG : G.LocallyLinear<GOAL>(SimpleGraph.map f G).LocallyLinear
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph β<VAR>e : α ≃ β<GOAL>(SimpleGraph.comap (⇑e) G).LocallyLinear ↔ G.LocallyLinear
<VAR>α : Type u_1<VAR>G : SimpleGraph α<GOAL>G.EdgeDisjointTriangles ↔ ∀ ⦃e : Sym2 α⦄, ¬e.IsDiag → {s | s ∈ G.cliqueSet 3 ∧ e ∈ s.sym2}.Subsingleton
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>DecidableEq α<VAR>Fintype α<VAR>DecidableRel G.Adj<VAR>hG : G.EdgeDisjointTriangles<GOAL>3 * (G.cliqueFinset 3).card ≤ G.edgeFinset.card
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>DecidableEq α<VAR>Fintype α<VAR>DecidableRel G.Adj<VAR>hG : G.LocallyLinear<GOAL>G.edgeFinset.card = 3 * (G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>𝕜 : Type u_3<VAR>LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>ε : 𝕜<VAR>Fintype α<VAR>DecidableRel G.Adj<GOAL>G.FarFromTriangleFree ε ↔ ∀ ⦃H : SimpleGraph α⦄ [inst : DecidableRel H.Adj], H ≤ G → H.CliqueFree 3 → ε * ↑(Fintype.card α ^ 2) ≤ ↑G.edgeFinset.card - ↑H.edgeFinset.card
<VAR>α : Type u_1<VAR>𝕜 : Type u_3<VAR>LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>ε δ : 𝕜<VAR>Fintype α<VAR>DecidableRel G.Adj<VAR>hε : G.FarFromTriangleFree ε<VAR>h : δ ≤ ε<GOAL>G.FarFromTriangleFree δ
<VAR>α : Type u_1<VAR>𝕜 : Type u_3<VAR>LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε : 𝕜<VAR>Fintype α<VAR>DecidableRel G.Adj<VAR>DecidableRel H.Adj<VAR>DecidableEq α<VAR>hH : H ≤ G<VAR>hG : G.FarFromTriangleFree ε<VAR>hcard : ↑G.edgeFinset.card - ↑H.edgeFinset.card < ε * ↑(Fintype.card α ^ 2)<GOAL>(H.cliqueFinset 3).Nonempty
<VAR>α : Type u_1<VAR>G H : SimpleGraph α<VAR>Fintype α<VAR>DecidableRel G.Adj<VAR>DecidableRel H.Adj<VAR>DecidableEq α<VAR>tris : Finset (Finset α)<VAR>htris : tris ⊆ G.cliqueFinset 3<VAR>pd : (↑tris).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton<VAR>hHG : H ≤ G<VAR>hH : H.CliqueFree 3<GOAL>tris.card ≤ G.edgeFinset.card - H.edgeFinset.card
<VAR>α : Type u_1<VAR>𝕜 : Type u_3<VAR>LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>ε : 𝕜<VAR>Fintype α<VAR>DecidableRel G.Adj<VAR>DecidableEq α<VAR>tris : Finset (Finset α)<VAR>htris : tris ⊆ G.cliqueFinset 3<VAR>pd : (↑tris).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton<VAR>tris_big : ε * ↑(Fintype.card α ^ 2) ≤ ↑tris.card<GOAL>G.FarFromTriangleFree ε
<VAR>α : Type u_1<VAR>𝕜 : Type u_3<VAR>LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>ε : 𝕜<VAR>Fintype α<VAR>DecidableRel G.Adj<VAR>DecidableEq α<VAR>hG : G.EdgeDisjointTriangles<VAR>tris_big : ε * ↑(Fintype.card α ^ 2) ≤ ↑(G.cliqueFinset 3).card<GOAL>G.FarFromTriangleFree ε
<VAR>α : Type u_1<VAR>𝕜 : Type u_3<VAR>LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>ε : 𝕜<VAR>Fintype α<VAR>DecidableRel G.Adj<VAR>Nonempty α<VAR>hG : G.FarFromTriangleFree ε<GOAL>ε < 2⁻¹
<VAR>α : Type u_1<VAR>𝕜 : Type u_3<VAR>LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>ε : 𝕜<VAR>Fintype α<VAR>DecidableRel G.Adj<VAR>Nonempty α<VAR>hG : G.FarFromTriangleFree ε<GOAL>ε < 1
<VAR>α : Type u_1<VAR>𝕜 : Type u_3<VAR>LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>ε : 𝕜<VAR>Fintype α<VAR>DecidableRel G.Adj<VAR>Nonempty α<VAR>h₀ : G.FarFromTriangleFree ε<VAR>h₁ : G.CliqueFree 3<GOAL>ε ≤ 0
<VAR>α : Type u_1<VAR>𝕜 : Type u_3<VAR>LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>ε : 𝕜<VAR>Fintype α<VAR>DecidableRel G.Adj<VAR>Nonempty α<VAR>hG : G.CliqueFree 3<VAR>hε : 0 < ε<GOAL>¬G.FarFromTriangleFree ε
<VAR>α : Type u_1<VAR>𝕜 : Type u_3<VAR>LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>ε : 𝕜<VAR>Fintype α<VAR>DecidableRel G.Adj<VAR>Nonempty α<VAR>hG : G.FarFromTriangleFree ε<VAR>hε : 0 < ε<GOAL>¬G.CliqueFree 3
<VAR>α : Type u_1<VAR>𝕜 : Type u_3<VAR>LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>ε : 𝕜<VAR>Fintype α<VAR>DecidableRel G.Adj<VAR>Nonempty α<VAR>DecidableEq α<VAR>hG : G.FarFromTriangleFree ε<VAR>hε : 0 < ε<GOAL>(G.cliqueFinset 3).Nonempty
<VAR>η : Type u_5<VAR>α : Type u_6<VAR>ι : Type u_7<VAR>self : Combinatorics.Subspace η α ι<VAR>e : η<GOAL>∃ i, self.idxFun i = Sum.inr e
<VAR>η : Type u_5<VAR>α : Type u_6<VAR>ι : Type u_7<VAR>l : Combinatorics.Subspace η α ι<VAR>x : η → α<VAR>i : ι<GOAL>↑l x i = Sum.elim id x (l.idxFun i)
<VAR>η : Type u_5<VAR>α : Type u_6<VAR>ι : Type u_7<VAR>Nontrivial α<GOAL>Function.Injective Combinatorics.Subspace.toFun
<VAR>η : Type u_5<VAR>α : Type u_6<VAR>ι : Type u_7<VAR>l : Combinatorics.Subspace η α ι<VAR>x : η → α<VAR>i : ι<VAR>a : α<VAR>h : l.idxFun i = Sum.inl a<GOAL>↑l x i = a
<VAR>η : Type u_5<VAR>α : Type u_6<VAR>ι : Type u_7<VAR>l : Combinatorics.Subspace η α ι<VAR>x : η → α<VAR>i : ι<VAR>e : η<VAR>h : l.idxFun i = Sum.inr e<GOAL>↑l x i = x e
<VAR>η : Type u_5<VAR>α : Type u_6<VAR>ι : Type u_7<VAR>η' : Type u_9<VAR>α' : Type u_10<VAR>ι' : Type u_11<VAR>l : Combinatorics.Subspace η α ι<VAR>eη : η ≃ η'<VAR>eα : α ≃ α'<VAR>eι : ι ≃ ι'<VAR>x : η' → α'<VAR>i : ι'<GOAL>↑(l.reindex eη eα eι) x i = eα (↑l (⇑eα.symm ∘ x ∘ ⇑eη) (eι.symm i))
<VAR>η : Type u_5<VAR>α : Type u_6<VAR>ι : Type u_7<VAR>κ : Type u_8<VAR>l : Combinatorics.Subspace η α ι<VAR>η' : Type u_9<VAR>α' : Type u_10<VAR>ι' : Type u_11<VAR>eη : η ≃ η'<VAR>eα : α ≃ α'<VAR>eι : ι ≃ ι'<VAR>C : (ι' → α') → κ<GOAL>Combinatorics.Subspace.IsMono C (l.reindex eη eα eι) ↔ Combinatorics.Subspace.IsMono (fun x => C (⇑eα ∘ x ∘ ⇑eι.symm)) l
<VAR>η : Type u_5<VAR>α : Type u_6<VAR>ι : Type u_7<VAR>κ : Type u_8<VAR>l : Combinatorics.Subspace η α ι<VAR>η' : Type u_9<VAR>α' : Type u_10<VAR>ι' : Type u_11<VAR>eη : η ≃ η'<VAR>eα : α ≃ α'<VAR>eι : ι ≃ ι'<VAR>C : (ι → α) → κ<VAR>hl : Combinatorics.Subspace.IsMono C l<GOAL>Combinatorics.Subspace.IsMono (fun x => C (⇑eα.symm ∘ x ∘ ⇑eι)) (l.reindex eη eα eι)
<VAR>α : Type u_5<VAR>ι : Type u_6<VAR>self : Combinatorics.Line α ι<GOAL>∃ i, self.idxFun i = none
<VAR>α : Type u_2<VAR>ι : Type u_3<VAR>l : Combinatorics.Line α ι<VAR>x : α<VAR>i : ι<GOAL>(fun x i => (l.idxFun i).getD x) x i = (l.idxFun i).getD x
<VAR>α : Type u_2<VAR>ι : Type u_3<VAR>Nontrivial α<GOAL>Function.Injective fun x x_1 i => (x.idxFun i).getD x_1
<VAR>α : Type u_2<VAR>ι : Type u_3<VAR>l : Combinatorics.Line α ι<VAR>a : Unit → α<GOAL>↑l.toSubspaceUnit a = (fun x i => (l.idxFun i).getD x) (a ())
<VAR>α : Type u_2<VAR>ι : Type u_3<VAR>κ : Type u_4<VAR>l : Combinatorics.Line α ι<VAR>C : (ι → α) → κ<GOAL>Combinatorics.Subspace.IsMono C l.toSubspaceUnit ↔ Combinatorics.Line.IsMono C l
<VAR>η : Type u_1<VAR>α : Type u_2<VAR>ι : Type u_3<VAR>l : Combinatorics.Line (η → α) ι<VAR>a : η → α<VAR>ie : ι × η<GOAL>↑l.toSubspace a ie = (fun x i => (l.idxFun i).getD x) a ie.1 ie.2
<VAR>η : Type u_1<VAR>α : Type u_2<VAR>ι : Type u_3<VAR>κ : Type u_4<VAR>l : Combinatorics.Line (η → α) ι<VAR>C : (ι × η → α) → κ<GOAL>Combinatorics.Subspace.IsMono C l.toSubspace ↔ Combinatorics.Line.IsMono (fun x => C fun x_1 => match x_1 with | (i, e) => x i e) l
<VAR>α : Type u_5<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>C : (ι → Option α) → κ<VAR>self : Combinatorics.Line.AlmostMono C<VAR>x : α<GOAL>C ((fun x i => (self.line.idxFun i).getD x) (some x)) = self.color
<VAR>α : Type u_5<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>C : (ι → Option α) → κ<VAR>self : Combinatorics.Line.ColorFocused C<GOAL>(Multiset.map Combinatorics.Line.AlmostMono.color self.lines).Nodup
<VAR>α : Type u_5<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>C : (ι → Option α) → κ<VAR>self : Combinatorics.Line.ColorFocused C<VAR>p : Combinatorics.Line.AlmostMono C<GOAL>p ∈ self.lines → (fun x i => (p.line.idxFun i).getD x) none = self.focus
<VAR>α : Type u_2<VAR>ι : Type u_3<VAR>l : Combinatorics.Line α ι<VAR>x : α<GOAL>(fun x i => (l.idxFun i).getD x) x = fun i => (l.idxFun i).getD x
<VAR>α : Type u_5<VAR>ι : Type u_6<VAR>l : Combinatorics.Line α ι<VAR>x : α<VAR>i : ι<VAR>h : l.idxFun i = none<GOAL>(fun x i => (l.idxFun i).getD x) x i = x
<VAR>α : Type u_2<VAR>ι : Type u_3<VAR>l : Combinatorics.Line α ι<VAR>i : ι<VAR>a x : α<VAR>h : l.idxFun i = some a<GOAL>(fun x i => (l.idxFun i).getD x) x i = a
<VAR>α : Type u_5<VAR>α' : Type u_6<VAR>ι : Type u_7<VAR>f : α → α'<VAR>l : Combinatorics.Line α ι<VAR>x : α<GOAL>(fun x i => ((Combinatorics.Line.map f l).idxFun i).getD x) (f x) = f ∘ (fun x i => (l.idxFun i).getD x) x
<VAR>α : Type u_5<VAR>ι : Type u_6<VAR>ι' : Type u_7<VAR>v : ι → α<VAR>l : Combinatorics.Line α ι'<VAR>x : α<GOAL>(fun x i => ((Combinatorics.Line.vertical v l).idxFun i).getD x) x = Sum.elim v ((fun x i => (l.idxFun i).getD x) x)
<VAR>α : Type u_5<VAR>ι : Type u_6<VAR>ι' : Type u_7<VAR>l : Combinatorics.Line α ι<VAR>v : ι' → α<VAR>x : α<GOAL>(fun x i => ((l.horizontal v).idxFun i).getD x) x = Sum.elim ((fun x i => (l.idxFun i).getD x) x) v
<VAR>α : Type u_5<VAR>ι : Type u_6<VAR>ι' : Type u_7<VAR>l : Combinatorics.Line α ι<VAR>l' : Combinatorics.Line α ι'<VAR>x : α<GOAL>(fun x i => ((l.prod l').idxFun i).getD x) x = Sum.elim ((fun x i => (l.idxFun i).getD x) x) ((fun x i => (l'.idxFun i).getD x) x)
<VAR>α : Type u_5<VAR>ι : Type u_6<VAR>Nonempty ι<VAR>x : α<GOAL>(fun x i => ((Combinatorics.Line.diagonal α ι).idxFun i).getD x) x = fun x_1 => x
<VAR>α : Type u<VAR>Finite α<VAR>κ : Type (max v u)<VAR>Finite κ<GOAL>∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, Combinatorics.Line.IsMono C l
<VAR>α : Type u<VAR>Finite α<VAR>κ : Type v<VAR>Finite κ<GOAL>∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, Combinatorics.Line.IsMono C l
<VAR>M : Type u_5<VAR>κ : Type u_6<VAR>AddCommMonoid M<VAR>S : Finset M<VAR>Finite κ<VAR>C : M → κ<GOAL>∃ a > 0, ∃ b c, ∀ s ∈ S, C (a • s + b) = c
<VAR>α : Type u_5<VAR>κ : Type u_6<VAR>η : Type u_7<VAR>Finite α<VAR>Finite κ<VAR>Finite η<GOAL>∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, Combinatorics.Subspace.IsMono C l
<VAR>α : Type u_5<VAR>κ : Type u_6<VAR>η : Type u_7<VAR>Finite α<VAR>Finite κ<VAR>Finite η<GOAL>∃ n, ∀ (C : (Fin n → α) → κ), ∃ l, Combinatorics.Subspace.IsMono C l
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>Membership P L<VAR>self : Configuration.Nondegenerate P L<VAR>l : L<GOAL>∃ p, p ∉ l
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>Membership P L<VAR>self : Configuration.Nondegenerate P L<VAR>p₁ p₂ : P<VAR>l₁ l₂ : L<GOAL>p₁ ∈ l₁ → p₂ ∈ l₁ → p₁ ∈ l₂ → p₂ ∈ l₂ → p₁ = p₂ ∨ l₁ = l₂
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>Membership P L<VAR>self : Configuration.Nondegenerate P L<VAR>p : P<GOAL>∃ l, p ∉ l
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>Membership P L<VAR>self : Configuration.HasPoints P L<VAR>l₁ l₂ : L<VAR>h : l₁ ≠ l₂<GOAL>Configuration.HasPoints.mkPoint h ∈ l₁ ∧ Configuration.HasPoints.mkPoint h ∈ l₂
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>Membership P L<VAR>self : Configuration.HasLines P L<VAR>p₁ p₂ : P<VAR>h : p₁ ≠ p₂<GOAL>p₁ ∈ Configuration.HasLines.mkLine h ∧ p₂ ∈ Configuration.HasLines.mkLine h
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>Membership P L<VAR>Configuration.HasPoints P L<VAR>l₁ l₂ : L<VAR>hl : l₁ ≠ l₂<GOAL>∃! p, p ∈ l₁ ∧ p ∈ l₂
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>Membership P L<VAR>Configuration.HasLines P L<VAR>p₁ p₂ : P<VAR>hp : p₁ ≠ p₂<GOAL>∃! l, p₁ ∈ l ∧ p₂ ∈ l
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>Membership P L<VAR>Configuration.Nondegenerate P L<VAR>Fintype P<VAR>Fintype L<VAR>h : Fintype.card L ≤ Fintype.card P<GOAL>∃ f, Function.Injective f ∧ ∀ (l : L), f l ∉ l
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>Membership P L<VAR>Fintype P<VAR>Fintype L<GOAL>∑ p : P, Configuration.lineCount L p = ∑ l : L, Configuration.pointCount P l
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>Membership P L<VAR>Configuration.HasLines P L<VAR>p : P<VAR>l : L<VAR>h : p ∉ l<VAR>Finite { l // p ∈ l }<GOAL>Configuration.pointCount P l ≤ Configuration.lineCount L p
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>Membership P L<VAR>Configuration.HasPoints P L<VAR>p : P<VAR>l : L<VAR>h : p ∉ l<VAR>hf : Finite { p // p ∈ l }<GOAL>Configuration.lineCount L p ≤ Configuration.pointCount P l
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>Membership P L<VAR>Configuration.HasLines P L<VAR>Fintype P<VAR>Fintype L<GOAL>Fintype.card P ≤ Fintype.card L
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>Membership P L<VAR>Configuration.HasPoints P L<VAR>Fintype P<VAR>Fintype L<GOAL>Fintype.card L ≤ Fintype.card P
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>Membership P L<VAR>Configuration.HasLines P L<VAR>Fintype P<VAR>Fintype L<VAR>h : Fintype.card P = Fintype.card L<GOAL>∃ f, Function.Bijective f ∧ ∀ (l : L), Configuration.pointCount P l = Configuration.lineCount L (f l)
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>Membership P L<VAR>Configuration.HasLines P L<VAR>Fintype P<VAR>Fintype L<VAR>hPL : Fintype.card P = Fintype.card L<VAR>p : P<VAR>l : L<VAR>hpl : p ∉ l<GOAL>Configuration.lineCount L p = Configuration.pointCount P l
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>Membership P L<VAR>Configuration.HasPoints P L<VAR>Fintype P<VAR>Fintype L<VAR>hPL : Fintype.card P = Fintype.card L<VAR>p : P<VAR>l : L<VAR>hpl : p ∉ l<GOAL>Configuration.lineCount L p = Configuration.pointCount P l
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>Membership P L<VAR>self : Configuration.ProjectivePlane P L<GOAL>∃ p₁ p₂ p₃ l₁ l₂ l₃, p₁ ∉ l₂ ∧ p₁ ∉ l₃ ∧ p₂ ∉ l₁ ∧ p₂ ∈ l₂ ∧ p₂ ∈ l₃ ∧ p₃ ∉ l₁ ∧ p₃ ∈ l₂ ∧ p₃ ∉ l₃
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>Membership P L<VAR>Configuration.ProjectivePlane P L<VAR>Fintype P<VAR>Fintype L<GOAL>Fintype.card P = Fintype.card L
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>Membership P L<VAR>Configuration.ProjectivePlane P L<VAR>Finite P<VAR>Finite L<VAR>p q : P<GOAL>Configuration.lineCount L p = Configuration.lineCount L q
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>Membership P L<VAR>Configuration.ProjectivePlane P L<VAR>Finite P<VAR>Finite L<VAR>l m : L<GOAL>Configuration.pointCount P l = Configuration.pointCount P m
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>Membership P L<VAR>Configuration.ProjectivePlane P L<VAR>Finite P<VAR>Finite L<VAR>p : P<VAR>l : L<GOAL>Configuration.lineCount L p = Configuration.pointCount P l
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>Membership P L<VAR>Configuration.ProjectivePlane P L<VAR>Finite P<VAR>Finite L<GOAL>Configuration.ProjectivePlane.order (Configuration.Dual L) (Configuration.Dual P) = Configuration.ProjectivePlane.order P L
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>Membership P L<VAR>Configuration.ProjectivePlane P L<VAR>Finite P<VAR>Finite L<VAR>p : P<GOAL>Configuration.lineCount L p = Configuration.ProjectivePlane.order P L + 1
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>Membership P L<VAR>Configuration.ProjectivePlane P L<VAR>Finite P<VAR>Finite L<VAR>l : L<GOAL>Configuration.pointCount P l = Configuration.ProjectivePlane.order P L + 1
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>Membership P L<VAR>Configuration.ProjectivePlane P L<VAR>Finite P<VAR>Finite L<GOAL>1 < Configuration.ProjectivePlane.order P L
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>Membership P L<VAR>Configuration.ProjectivePlane P L<VAR>Finite P<VAR>Finite L<VAR>p : P<GOAL>2 < Configuration.lineCount L p
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>Membership P L<VAR>Configuration.ProjectivePlane P L<VAR>Finite P<VAR>Finite L<VAR>l : L<GOAL>2 < Configuration.pointCount P l
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>Membership P L<VAR>Configuration.ProjectivePlane P L<VAR>Fintype P<VAR>Finite L<GOAL>Fintype.card P = Configuration.ProjectivePlane.order P L ^ 2 + Configuration.ProjectivePlane.order P L + 1
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>Membership P L<VAR>Configuration.ProjectivePlane P L<VAR>Finite P<VAR>Fintype L<GOAL>Fintype.card L = Configuration.ProjectivePlane.order P L ^ 2 + Configuration.ProjectivePlane.order P L + 1
<VAR>A : Set ℕ<VAR>DecidablePred fun x => x ∈ A<GOAL>0 ≤ schnirelmannDensity A
<VAR>A : Set ℕ<VAR>DecidablePred fun x => x ∈ A<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>schnirelmannDensity A ≤ ↑(Finset.filter (fun x => x ∈ A) (Finset.Ioc 0 n)).card / ↑n
<VAR>A : Set ℕ<VAR>DecidablePred fun x => x ∈ A<VAR>n : ℕ<GOAL>schnirelmannDensity A * ↑n ≤ ↑(Finset.filter (fun x => x ∈ A) (Finset.Ioc 0 n)).card
<VAR>A : Set ℕ<VAR>DecidablePred fun x => x ∈ A<VAR>x : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hx : ↑(Finset.filter (fun x => x ∈ A) (Finset.Ioc 0 n)).card / ↑n ≤ x<GOAL>schnirelmannDensity A ≤ x
<VAR>A : Set ℕ<VAR>DecidablePred fun x => x ∈ A<GOAL>schnirelmannDensity A ≤ 1
<VAR>A : Set ℕ<VAR>DecidablePred fun x => x ∈ A<VAR>k : ℕ<VAR>hk : k ∉ A<GOAL>schnirelmannDensity A ≤ 1 - (↑k)⁻¹
<VAR>A : Set ℕ<VAR>DecidablePred fun x => x ∈ A<VAR>h : 1 ∉ A<GOAL>schnirelmannDensity A = 0
<VAR>A : Set ℕ<VAR>DecidablePred fun x => x ∈ A<VAR>B : Set ℕ<VAR>DecidablePred fun x => x ∈ B<VAR>h : A ⊆ B<GOAL>schnirelmannDensity A ≤ schnirelmannDensity B
<VAR>A : Set ℕ<VAR>DecidablePred fun x => x ∈ A<GOAL>schnirelmannDensity A = 1 ↔ {0}ᶜ ⊆ A
<VAR>A : Set ℕ<VAR>DecidablePred fun x => x ∈ A<VAR>hA : 0 ∈ A<GOAL>schnirelmannDensity A = 1 ↔ A = Set.univ
<VAR>A : Set ℕ<VAR>DecidablePred fun x => x ∈ A<VAR>x : ℝ<GOAL>x ≤ schnirelmannDensity A ↔ ∀ (n : ℕ), 0 < n → x ≤ ↑(Finset.filter (fun x => x ∈ A) (Finset.Ioc 0 n)).card / ↑n
<VAR>A : Set ℕ<VAR>DecidablePred fun x => x ∈ A<VAR>x : ℝ<GOAL>schnirelmannDensity A < x ↔ ∃ n, 0 < n ∧ ↑(Finset.filter (fun x => x ∈ A) (Finset.Ioc 0 n)).card / ↑n < x
<VAR>A : Set ℕ<VAR>DecidablePred fun x => x ∈ A<VAR>x : ℝ<GOAL>schnirelmannDensity A ≤ x ↔ ∀ (ε : ℝ), 0 < ε → ∃ n, 0 < n ∧ ↑(Finset.filter (fun x => x ∈ A) (Finset.Ioc 0 n)).card / ↑n < x + ε
<VAR>A : Set ℕ<VAR>DecidablePred fun x => x ∈ A<VAR>B : Set ℕ<VAR>DecidablePred fun x => x ∈ B<VAR>h : ∀ n > 0, n ∈ A ↔ n ∈ B<GOAL>schnirelmannDensity A = schnirelmannDensity B
<VAR>A : Set ℕ<VAR>DecidablePred fun x => x ∈ A<VAR>DecidablePred fun x => x ∈ insert 0 A<GOAL>schnirelmannDensity (insert 0 A) = schnirelmannDensity A
<VAR>A : Set ℕ<VAR>DecidablePred fun x => x ∈ A<VAR>DecidablePred fun x => x ∈ A \ {0}<GOAL>schnirelmannDensity (A \ {0}) = schnirelmannDensity A
<VAR>A : Set ℕ<VAR>DecidablePred fun x => x ∈ A<VAR>B : Set ℕ<VAR>DecidablePred fun x => x ∈ B<VAR>h : A = B<GOAL>schnirelmannDensity A = schnirelmannDensity B
<VAR>A : Set ℕ<VAR>DecidablePred fun x => x ∈ A<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hA : schnirelmannDensity A = 0<GOAL>∃ n, 0 < n ∧ ↑(Finset.filter (fun x => x ∈ A) (Finset.Ioc 0 n)).card / ↑n < ε
<VAR>A : Set ℕ<VAR>DecidablePred fun x => x ∈ A<VAR>hA : A.Finite<GOAL>schnirelmannDensity A = 0
<GOAL>schnirelmannDensity (setOf Nat.Prime) = 0
<VAR>α : Type u_1<VAR>CommGroup α<VAR>s : Set α<GOAL>MulDissociated s ↔ ∀ (a : α), {t | ↑t ⊆ s ∧ ∏ x ∈ t, x = a}.Subsingleton
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>s : Set α<GOAL>AddDissociated s ↔ ∀ (a : α), {t | ↑t ⊆ s ∧ ∑ x ∈ t, x = a}.Subsingleton
<VAR>α : Type u_1<VAR>CommGroup α<VAR>s t : Set α<VAR>hst : s ⊆ t<VAR>ht : MulDissociated t<GOAL>MulDissociated s
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>s t : Set α<VAR>hst : s ⊆ t<VAR>ht : AddDissociated t<GOAL>AddDissociated s
<VAR>α : Type u_1<VAR>CommGroup α<GOAL>MulDissociated ∅
<VAR>α : Type u_1<VAR>AddCommGroup α<GOAL>AddDissociated ∅
<VAR>α : Type u_1<VAR>CommGroup α<VAR>a : α<GOAL>MulDissociated {a} ↔ a ≠ 1
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>a : α<GOAL>AddDissociated {a} ↔ a ≠ 0
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>s : Set α<GOAL>¬AddDissociated s ↔ ∃ t, ↑t ⊆ s ∧ ∃ u, ↑u ⊆ s ∧ t ≠ u ∧ ∑ x ∈ t, x = ∑ x ∈ u, x
<VAR>α : Type u_1<VAR>CommGroup α<VAR>s : Set α<GOAL>¬MulDissociated s ↔ ∃ t, ↑t ⊆ s ∧ ∃ u, ↑u ⊆ s ∧ t ≠ u ∧ ∏ x ∈ t, x = ∏ x ∈ u, x
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>s : Set α<GOAL>¬AddDissociated s ↔ ∃ t u, ↑t ⊆ s ∧ ↑u ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ ∑ a ∈ t, a = ∑ a ∈ u, a
<VAR>α : Type u_1<VAR>CommGroup α<VAR>s : Set α<GOAL>¬MulDissociated s ↔ ∃ t u, ↑t ⊆ s ∧ ↑u ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>AddCommGroup β<VAR>s : Set α<VAR>e : β ≃+ α<GOAL>AddDissociated (⇑e ⁻¹' s) ↔ AddDissociated s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>CommGroup β<VAR>s : Set α<VAR>e : β ≃* α<GOAL>MulDissociated (⇑e ⁻¹' s) ↔ MulDissociated s
<VAR>α : Type u_1<VAR>CommGroup α<VAR>s : Set α<GOAL>MulDissociated s⁻¹ ↔ MulDissociated s
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>s : Set α<GOAL>AddDissociated (-s) ↔ AddDissociated s
<VAR>α : Type u_1<VAR>CommGroup α<VAR>DecidableEq α<VAR>Fintype α<VAR>s : Finset α<VAR>a : α<GOAL>a ∈ s.mulSpan ↔ ∃ ε, (∀ (a : α), ε a = -1 ∨ ε a = 0 ∨ ε a = 1) ∧ ∏ a ∈ s, a ^ ε a = a
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>DecidableEq α<VAR>Fintype α<VAR>s : Finset α<VAR>a : α<GOAL>a ∈ s.addSpan ↔ ∃ ε, (∀ (a : α), ε a = -1 ∨ ε a = 0 ∨ ε a = 1) ∧ ∑ a ∈ s, ε a • a = a
<VAR>α : Type u_1<VAR>CommGroup α<VAR>DecidableEq α<VAR>Fintype α<VAR>s : Finset α<GOAL>s ⊆ s.mulSpan
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>DecidableEq α<VAR>Fintype α<VAR>s : Finset α<GOAL>s ⊆ s.addSpan
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>DecidableEq α<VAR>Fintype α<VAR>s t u : Finset α<VAR>ht : t ⊆ s<VAR>hu : u ⊆ s<GOAL>∑ a ∈ t, a - ∑ a ∈ u, a ∈ s.addSpan
<VAR>α : Type u_1<VAR>CommGroup α<VAR>DecidableEq α<VAR>Fintype α<VAR>s t u : Finset α<VAR>ht : t ⊆ s<VAR>hu : u ⊆ s<GOAL>(∏ a ∈ t, a) / ∏ a ∈ u, a ∈ s.mulSpan
<VAR>α : Type u_1<VAR>CommGroup α<VAR>DecidableEq α<VAR>Fintype α<VAR>s : Finset α<VAR>d : ℕ<VAR>hs : ∀ s' ⊆ s, MulDissociated ↑s' → s'.card ≤ d<GOAL>∃ s' ⊆ s, s'.card ≤ d ∧ s ⊆ s'.mulSpan
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>DecidableEq α<VAR>Fintype α<VAR>s : Finset α<VAR>d : ℕ<VAR>hs : ∀ s' ⊆ s, AddDissociated ↑s' → s'.card ≤ d<GOAL>∃ s' ⊆ s, s'.card ≤ d ∧ s ⊆ s'.addSpan
<VAR>ι : Type u<VAR>α : Type v<VAR>DecidableEq α<VAR>t : ι → Finset α<VAR>Fintype ι<VAR>x : ι<VAR>a : α<VAR>ha : ∀ (s : Finset ι), s.Nonempty → s ≠ Finset.univ → s.card < (s.biUnion t).card<VAR>s' : Finset ↑{x' | x' ≠ x}<GOAL>s'.card ≤ (s'.biUnion fun x' => (t ↑x').erase a).card
<VAR>ι : Type u<VAR>α : Type v<VAR>DecidableEq α<VAR>t : ι → Finset α<VAR>Fintype ι<VAR>n : ℕ<VAR>hn : Fintype.card ι = n + 1<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>ih : ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α), Fintype.card ι' ≤ n → (∀ (s' : Finset ι'), s'.card ≤ (s'.biUnion t').card) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x<VAR>ha : ∀ (s : Finset ι), s.Nonempty → s ≠ Finset.univ → s.card < (s.biUnion t).card<GOAL>∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
<VAR>α : Type v<VAR>DecidableEq α<VAR>ι : Type u<VAR>t : ι → Finset α<VAR>s : Finset ι<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>s' : Finset ↑↑s<GOAL>s'.card ≤ (s'.biUnion fun a' => t ↑a').card
<VAR>α : Type v<VAR>DecidableEq α<VAR>ι : Type u<VAR>t : ι → Finset α<VAR>s : Finset ι<VAR>hus : s.card = (s.biUnion t).card<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>s' : Finset ↑(↑s)ᶜ<GOAL>s'.card ≤ (s'.biUnion fun x' => t ↑x' \ s.biUnion t).card
<VAR>ι : Type u<VAR>α : Type v<VAR>DecidableEq α<VAR>t : ι → Finset α<VAR>Fintype ι<VAR>n : ℕ<VAR>hn : Fintype.card ι = n + 1<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>ih : ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α), Fintype.card ι' ≤ n → (∀ (s' : Finset ι'), s'.card ≤ (s'.biUnion t').card) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>hns : s ≠ Finset.univ<VAR>hus : s.card = (s.biUnion t).card<GOAL>∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
<VAR>ι : Type u<VAR>α : Type v<VAR>DecidableEq α<VAR>t : ι → Finset α<VAR>Finite ι<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<GOAL>∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Finite ι<VAR>DecidableEq α<VAR>t : ι → Finset α<GOAL>(∀ (s : Finset ι), s.card ≤ (s.biUnion t).card) ↔ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x