ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>ν✝ : Measure α<VAR>ι : Type u_7<VAR>m : MeasurableSpace α<VAR>f : α → G<VAR>μ : ι → Measure α<VAR>hfi : ∀ (i : ι), Integrable f (μ i)<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ↑ε<VAR>hf_lt : ∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ < ⊤<VAR>hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ), ∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ < y + ↑ε<VAR>s : Finset ι<VAR>hs : ∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ < ∑ b ∈ s, (fun i => ∫⁻ (a : α), ↑‖f a‖₊ ∂μ i) b + ↑ε<VAR>ν : Measure α<VAR>hf : Integrable f (∑ i ∈ s, μ i) ∧ Integrable f ν<VAR>hν : ∑ i ∈ s, μ i + ν = Measure.sum μ<GOAL>↑(nndist (∫ (a : α), f a ∂∑ i ∈ s, μ i) (∫ (a : α), f a ∂(∑ i ∈ s, μ i + ν))) < ↑ε
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>ν✝ : Measure α<VAR>ι : Type u_7<VAR>m : MeasurableSpace α<VAR>f : α → G<VAR>μ : ι → Measure α<VAR>hfi : ∀ (i : ι), Integrable f (μ i)<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ↑ε<VAR>hf_lt : ∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ < ⊤<VAR>hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ), ∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ < y + ↑ε<VAR>s : Finset ι<VAR>hs : ∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ < ∑ b ∈ s, (fun i => ∫⁻ (a : α), ↑‖f a‖₊ ∂μ i) b + ↑ε<VAR>ν : Measure α<VAR>hf : Integrable f (∑ i ∈ s, μ i) ∧ Integrable f ν<VAR>hν : ∑ i ∈ s, μ i + ν = Measure.sum μ<GOAL>∫⁻ (x : α), ↑‖f x‖₊ ∂ν < ↑ε
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>ν✝ : Measure α<VAR>ι : Type u_7<VAR>m : MeasurableSpace α<VAR>f : α → G<VAR>μ : ι → Measure α<VAR>hfi : ∀ (i : ι), Integrable f (μ i)<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ↑ε<VAR>hf_lt : ∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ < ⊤<VAR>hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ), ∫⁻ (x : α), ↑‖f x‖₊ ∂Measure.sum μ < y + ↑ε<VAR>s : Finset ι<VAR>ν : Measure α<VAR>hs : ∑ i ∈ s, ∫⁻ (a : α), ↑‖f a‖₊ ∂μ i + ∫⁻ (a : α), ↑‖f a‖₊ ∂ν < ∑ b ∈ s, (fun i => ∫⁻ (a : α), ↑‖f a‖₊ ∂μ i) b + ↑ε<VAR>hf : Integrable f (∑ i ∈ s, μ i) ∧ Integrable f ν<VAR>hν : ∑ i ∈ s, μ i + ν = Measure.sum μ<GOAL>∫⁻ (x : α), ↑‖f x‖₊ ∂ν < ↑ε
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : HasShift C ℤ<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>T₁ : Triangle Cᵒᵖ<VAR>hT₁ : T₁ ∈ distinguishedTriangles C<VAR>T₂ : Triangle Cᵒᵖ<VAR>e : T₂ ≅ T₁<GOAL>T₂ ∈ distinguishedTriangles C
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : HasShift C ℤ<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>T₁ T₂ : Triangle Cᵒᵖ<VAR>e : T₂ ≅ T₁<VAR>hT₁ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁) ∈ Pretriangulated.distinguishedTriangles<GOAL>Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂) ∈ Pretriangulated.distinguishedTriangles
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Seq α<GOAL>nil.append s = s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Seq α<GOAL>∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = nil.append s ∧ s2 = s) (nil.append s).destruct s.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s✝ s : Seq α<GOAL>match (corec (fun x => match x.1.destruct with | none => match x.2.destruct with | none => none | some (a, b) => some (a, nil, b) | some (a, s₁') => some (a, s₁', x.2)) (nil, s)).destruct, s.destruct with | none, none => True | some (a, s), some (a', s') => a = a' ∧ ∃ s_1, s = corec (fun x => match x.1.destruct with | none => match x.2.destruct with | none => none | some (a, b) => some (a, nil, b) | some (a, s₁') => some (a, s₁', x.2)) (nil, s_1) ∧ s' = s_1 | x, x_1 => False
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s✝ s : Seq α<GOAL>match omap (corec fun x => match x.1.destruct with | none => match x.2.destruct with | none => none | some (a, b) => some (a, nil, b) | some (a, s₁') => some (a, s₁', x.2)) (match (nil, s).1.destruct with | none => match (nil, s).2.destruct with | none => none | some (a, b) => some (a, nil, b) | some (a, s₁') => some (a, s₁', (nil, s).2)), s.destruct with | none, none => True | some (a, s), some (a', s') => a = a' ∧ ∃ s_1, s = corec (fun x => match x.1.destruct with | none => match x.2.destruct with | none => none | some (a, b) => some (a, nil, b) | some (a, s₁') => some (a, s₁', x.2)) (nil, s_1) ∧ s' = s_1 | x, x_1 => False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoid α<VAR>a : α<GOAL>IsUnit (Associates.mk a) ↔ a ~ᵤ 1
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3<GOAL>W.dblY P / W.dblZ P ^ 3 = W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁷ : OrderedSemiring 𝕜<VAR>inst✝⁶ : AddCommMonoid E<VAR>inst✝⁵ : AddCommMonoid F<VAR>inst✝⁴ : OrderedAddCommMonoid α<VAR>inst✝³ : OrderedAddCommMonoid β<VAR>inst✝² : SMul 𝕜 E<VAR>inst✝¹ : SMul 𝕜 α<VAR>inst✝ : SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>g✝ : β → α<VAR>g : E → β<VAR>hf : ConcaveOn 𝕜 s f<VAR>hfg : EqOn f g s<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a • g x + b • g y ≤ g (a • x + b • y)
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>inst✝ : Monoid M<VAR>a✝ b c : M<VAR>m✝ n✝ : ℕ<VAR>a : M<VAR>m n : ℕ<GOAL>a ^ m * a ^ n = a ^ n * a ^ m
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>ι' : Sort u_1<VAR>inst✝ : Inv G<VAR>t₁ t₂ : TopologicalSpace G<VAR>h₁ : ContinuousInv G<VAR>h₂ : ContinuousInv G<GOAL>ContinuousInv G
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>ι' : Sort u_1<VAR>inst✝ : Inv G<VAR>t₁ t₂ : TopologicalSpace G<VAR>h₁ : ContinuousInv G<VAR>h₂ : ContinuousInv G<VAR>b : Bool<GOAL>ContinuousInv G
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDedekindDomain R<VAR>inst✝⁴ : Module.Free ℤ R<VAR>inst✝³ : Module.Finite ℤ R<VAR>K : Type u_2<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>I : FractionalIdeal R⁰ K<VAR>a : ↥R⁰<VAR>I₀ : Ideal R<VAR>h : a • ↑I = Submodule.map (Algebra.linearMap R K) I₀<GOAL>↑(Ideal.absNorm I.num) / ↑|(Algebra.norm ℤ) ↑I.den| = ↑(Ideal.absNorm I₀) / ↑|(Algebra.norm ℤ) ↑a|
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDedekindDomain R<VAR>inst✝⁴ : Module.Free ℤ R<VAR>inst✝³ : Module.Finite ℤ R<VAR>K : Type u_2<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>I : FractionalIdeal R⁰ K<VAR>a : ↥R⁰<VAR>I₀ : Ideal R<VAR>h : a • ↑I = Submodule.map (Algebra.linearMap R K) I₀<GOAL>↑(Ideal.absNorm I.num) * ↑|(Algebra.norm ℤ) ↑a| = ↑(Ideal.absNorm I₀) * ↑|(Algebra.norm ℤ) ↑I.den|
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDedekindDomain R<VAR>inst✝⁴ : Module.Free ℤ R<VAR>inst✝³ : Module.Finite ℤ R<VAR>K : Type u_2<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>I : FractionalIdeal R⁰ K<VAR>a : ↥R⁰<VAR>I₀ : Ideal R<VAR>h : a • ↑I = Submodule.map (Algebra.linearMap R K) I₀<GOAL>↑|(Algebra.norm ℤ) ↑I.den| ≠ 0
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDedekindDomain R<VAR>inst✝⁴ : Module.Free ℤ R<VAR>inst✝³ : Module.Finite ℤ R<VAR>K : Type u_2<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>I : FractionalIdeal R⁰ K<VAR>a : ↥R⁰<VAR>I₀ : Ideal R<VAR>h : a • ↑I = Submodule.map (Algebra.linearMap R K) I₀<GOAL>↑|(Algebra.norm ℤ) ↑a| ≠ 0
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → α<VAR>a : α<VAR>l : List α<GOAL>modifyLast f (l ++ [a]) = l ++ [f a]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Inter α<VAR>a b : α<GOAL>some a ∩ some b = some (a ∩ b)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.127177, u_1} C<VAR>inst✝³ : Category.{?u.127181, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>h : S.Splitting<VAR>inst✝ : HasBinaryBiproduct S.X₁ S.X₃<GOAL>biprod.lift h.r S.g ≫ biprod.desc S.f h.s = 𝟙 S.X₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α →. σ ⊕ α<VAR>hf : Partrec f<VAR>F : α → ℕ →. σ ⊕ α := fun a n => Nat.rec (Part.some (Sum.inr a)) (fun x IH => IH.bind fun s => Sum.casesOn s (fun x => Part.some s) f) n<GOAL>Partrec f.fix
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α →. σ ⊕ α<VAR>hf : Partrec f<VAR>F : α → ℕ →. σ ⊕ α := fun a n => Nat.rec (Part.some (Sum.inr a)) (fun x IH => IH.bind fun s => Sum.casesOn s (fun x => Part.some s) f) n<VAR>hF : Partrec₂ F<GOAL>Partrec f.fix
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α →. σ ⊕ α<VAR>hf : Partrec f<VAR>F : α → ℕ →. σ ⊕ α := fun a n => Nat.rec (Part.some (Sum.inr a)) (fun x IH => IH.bind fun s => Sum.casesOn s (fun x => Part.some s) f) n<VAR>hF : Partrec₂ F<VAR>p : α → ℕ → Part Bool := fun a n => Part.map (fun s => Sum.casesOn s (fun x => true) fun x => false) (F a n)<GOAL>Partrec f.fix
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α →. σ ⊕ α<VAR>hf : Partrec f<VAR>F : α → ℕ →. σ ⊕ α := fun a n => Nat.rec (Part.some (Sum.inr a)) (fun x IH => IH.bind fun s => Sum.casesOn s (fun x => Part.some s) f) n<VAR>hF : Partrec₂ F<VAR>p : α → ℕ → Part Bool := fun a n => Part.map (fun s => Sum.casesOn s (fun x => true) fun x => false) (F a n)<VAR>hp : Partrec₂ p<GOAL>Partrec f.fix
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort u_6<VAR>s t u : Set α<VAR>m : MeasurableSpace α<VAR>inst✝ : Countable ι<VAR>f : ι → Set α<VAR>h : ∀ (b : ι), MeasurableSet (f b)<GOAL>MeasurableSet (⋂ b, f b)ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort u_6<VAR>s t u : Set α<VAR>m : MeasurableSpace α<VAR>inst✝ : Countable ι<VAR>f : ι → Set α<VAR>h : ∀ (b : ι), MeasurableSet (f b)<GOAL>MeasurableSet (⋃ i, (f i)ᶜ)
<VAR>x y r : ℕ<VAR>hr : y * y + r = x<VAR>hle : r.ble (2 * y) = true<GOAL>x.sqrt = y
<VAR>x y r : ℕ<VAR>hr : y * y + r = x<VAR>hle : r.ble (2 * y) = true<GOAL>(y ^ 2 + r).sqrt = y
<VAR>x y r : ℕ<VAR>hr : y * y + r = x<VAR>hle : r.ble (y + y) = true<GOAL>(y ^ 2 + r).sqrt = y
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>o : ℕ<VAR>pn : p.natDegree ≤ n<VAR>mno : m * n ≤ o<GOAL>(p ^ m).coeff o = if o = m * n then p.coeff n ^ m else 0
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>pn : p.natDegree ≤ n<VAR>mno : m * n ≤ m * n<GOAL>(p ^ m).coeff (m * n) = if m * n = m * n then p.coeff n ^ m else 0
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>o : ℕ<VAR>pn : p.natDegree ≤ n<VAR>mno : m * n ≤ o<VAR>h : o ≠ m * n<GOAL>(p ^ m).coeff o = if o = m * n then p.coeff n ^ m else 0
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<VAR>inst✝ : Fintype α<VAR>h𝒜 : IsUpperSet ↑𝒜<VAR>hℬ : IsUpperSet ↑ℬ<GOAL>𝒜.card * ℬ.card ≤ 2 ^ Fintype.card α * (𝒜 ∩ ℬ).card
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<VAR>inst✝ : Fintype α<VAR>h𝒜 : IsLowerSet ↑𝒜ᶜ<VAR>hℬ : IsUpperSet ↑ℬ<GOAL>𝒜.card * ℬ.card ≤ 2 ^ Fintype.card α * (𝒜 ∩ ℬ).card
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<VAR>inst✝ : Fintype α<VAR>h𝒜 : IsLowerSet ↑𝒜ᶜ<VAR>hℬ : IsUpperSet ↑ℬ<VAR>this : 2 ^ Fintype.card α * (𝒜ᶜ ∩ ℬ).card ≤ 𝒜ᶜ.card * ℬ.card<GOAL>𝒜.card * ℬ.card ≤ 2 ^ Fintype.card α * (𝒜 ∩ ℬ).card
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<VAR>inst✝ : Fintype α<VAR>h𝒜 : IsLowerSet ↑𝒜ᶜ<VAR>hℬ : IsUpperSet ↑ℬ<VAR>this : 2 ^ Fintype.card α * (𝒜ᶜ ∩ ℬ).card ≤ 2 ^ Fintype.card α * ℬ.card - 𝒜.card * ℬ.card<GOAL>2 ^ Fintype.card α * (𝒜ᶜ ∩ ℬ).card ≤ 2 ^ Fintype.card α * ℬ.card
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<VAR>inst✝ : Fintype α<VAR>h𝒜 : IsLowerSet ↑𝒜ᶜ<VAR>hℬ : IsUpperSet ↑ℬ<VAR>this : 2 ^ Fintype.card α * (𝒜ᶜ ∩ ℬ).card ≤ 2 ^ Fintype.card α * ℬ.card - 𝒜.card * ℬ.card<GOAL>𝒜.card * ℬ.card ≤ 2 ^ Fintype.card α * ℬ.card
<VAR>α : Type u_1<VAR>inst✝³ : GeneralizedBooleanAlgebra α<VAR>inst✝² : DecidableRel Disjoint<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s✝ : Finset α<VAR>u✝ v✝ a b : α<VAR>inst✝ : DecidableEq α<VAR>u v : α<VAR>s : Finset α<GOAL>(𝓒 u v s).card = s.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>π : β → Type u_3<VAR>inst✝¹ : Fintype β<VAR>inst✝ : (b : β) → PseudoMetricSpace (π b)<VAR>f g : (b : β) → π b<VAR>r : ℝ≥0<VAR>hr : 0 < ↑r<GOAL>dist f g < ↑r ↔ ∀ (b : β), dist (f b) (g b) < ↑r
<VAR>d : ℤ<VAR>a₁ : Solution₁ d<VAR>h : IsFundamental a₁<VAR>a : Solution₁ d<VAR>hay : 0 ≤ a.y<VAR>ax : ℕ<VAR>hax' : ↑ax = a.x<VAR>hax : 0 < ↑ax<GOAL>∃ n, a = a₁ ^ n
<VAR>d : ℤ<VAR>a₁ : Solution₁ d<VAR>h : IsFundamental a₁<VAR>x : ℕ<VAR>ih : ∀ m < x, ∀ {a : Solution₁ d}, 0 ≤ a.y → ↑m = a.x → 0 < ↑m → ∃ n, a = a₁ ^ n<VAR>a : Solution₁ d<VAR>hay : 0 ≤ a.y<VAR>hax' : ↑x = a.x<VAR>hax : 0 < ↑x<GOAL>∃ n, a = a₁ ^ n
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring S<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>α' : Type u_7<VAR>M' : Type u_8<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>v : α → M<VAR>v' : α' → M'<VAR>s : Finset α<VAR>f : α → R<VAR>g : α → M<VAR>hf : ∀ (a : α), f a ≠ 0 → a ∈ s<GOAL>(Finsupp.total α M R g) (onFinset s f hf) = ∑ x ∈ s, f x • g x
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>u : β → α<VAR>a : α<GOAL>(∀ (ib : ℝ), 0 < ib → ∃ ia, True ∧ ∀ x ∈ Ici ia, u x ∈ ball a ib) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>f : Fin n → α<VAR>σ : Equiv.Perm (Fin n)<GOAL>sort f = Equiv.refl (Fin n) ↔ Monotone f
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>f : Fin n → α<VAR>σ : Equiv.Perm (Fin n)<GOAL>(Monotone f ∧ ∀ (i j : Fin n), i < j → f (id i) = f (id j) → id i < id j) ↔ Monotone f
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>f : Fin n → α<VAR>σ : Equiv.Perm (Fin n)<GOAL>Monotone f → ∀ (i j : Fin n), i < j → f i = f j → i < j
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hb : 0 < b<GOAL>a / b < c ↔ a < c * b
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>inst✝ : MulOneClass M<VAR>s : Set Mᵐᵒᵖ<GOAL>(closure s).unop = closure (MulOpposite.op ⁻¹' s)
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>inst✝ : MulOneClass M<VAR>s : Set Mᵐᵒᵖ<GOAL>sInf {a | s ⊆ MulOpposite.unop ⁻¹' ↑a} = sInf {S | MulOpposite.op ⁻¹' s ⊆ ↑S}
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>inst✝ : MulOneClass M<VAR>s : Set Mᵐᵒᵖ<VAR>a : Submonoid M<GOAL>a ∈ {a | s ⊆ MulOpposite.unop ⁻¹' ↑a} ↔ a ∈ {S | MulOpposite.op ⁻¹' s ⊆ ↑S}
<VAR>m n : ℤ<VAR>k : ℕ<GOAL>(m.xor n).testBit k = xor (m.testBit k) (n.testBit k)
<VAR>x y : EReal<VAR>hx : x ≠ ⊤<VAR>hy : y ≠ ⊤<GOAL>x + y < ⊤
<VAR>x y : EReal<VAR>hx : x ≠ ⊤<VAR>hy : y ≠ ⊤<GOAL>x + y < ⊤ + ⊤
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s : Set Ω<VAR>hs : s.Finite<VAR>hs' : s.Nonempty<GOAL>(condCount s) Set.univ = 1
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s : Set Ω<VAR>hs : s.Finite<VAR>hs' : s.Nonempty<GOAL>Measure.count s ≠ 0
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s : Set Ω<VAR>hs : s.Finite<VAR>hs' : s.Nonempty<GOAL>Measure.count s ≠ ⊤
<VAR>θ : Angle<VAR>h : θ.sign ≤ 0<GOAL>-↑|θ.toReal| = θ
<VAR>θ : Angle<VAR>h : θ.sign = -1 ∨ θ.sign = 0<GOAL>-↑|θ.toReal| = θ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t✝ : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>f : β → α<VAR>hl : l.HasBasis p s<VAR>t : Set β<GOAL>t ∈ Filter.comap f l ↔ ∃ i, p i ∧ f ⁻¹' s i ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t✝ : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>f : β → α<VAR>hl : l.HasBasis p s<VAR>t : Set β<GOAL>(∃ i, p i ∧ s i ⊆ {y | ∀ ⦃x : β⦄, f x = y → x ∈ t}) ↔ ∃ i, p i ∧ f ⁻¹' s i ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t✝ : Set α<VAR>i✝ : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>f : β → α<VAR>hl : l.HasBasis p s<VAR>t : Set β<VAR>i : ι<GOAL>s i ⊆ {y | ∀ ⦃x : β⦄, f x = y → x ∈ t} ↔ f ⁻¹' s i ⊆ t
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>M'' : Type u_5<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : AddCommGroup M''<VAR>inst✝ : Module R M''<VAR>N : Submodule R M<VAR>r : R<GOAL>(∀ (x : M), r • N.mkQ x = 0 → N.mkQ x = 0) ↔ ∀ (x : M), r • x ∈ N → x ∈ N
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Finset α<VAR>a b : α<GOAL>s.sym2.Nonempty ↔ s.Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Finset α<VAR>a b : α<GOAL>¬s.sym2.Nonempty ↔ ¬s.Nonempty
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.20231, u_1} C<VAR>inst✝ : Preadditive C<VAR>P Q : Karoubi C<VAR>f g : P ⟶ Q<GOAL>f.f + g.f = P.p ≫ (f.f + g.f) ≫ Q.p
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype ↑C.colorClasses<VAR>this : Fintype ↑(Setoid.ker ⇑C).classes<GOAL>card ↑(Setoid.ker ⇑C).classes ≤ card α
<VAR>M : Type w<VAR>A : Set M<VAR>L : Language<VAR>inst✝ : L.Structure M<VAR>α : Type u₁<VAR>β : Type u_1<VAR>B : Set M<VAR>s : Set (α → M)<VAR>f : α → β<VAR>φ : L[[↑A]].Formula α<VAR>x✝ : β → M<GOAL>x✝ ∈ (fun g => g ∘ f) ⁻¹' setOf φ.Realize ↔ x✝ ∈ setOf (Formula.relabel f φ).Realize
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<GOAL>prod.fst ⊚ prod.diag = id
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<VAR>i : Fin2 n<GOAL>(prod.fst ⊚ prod.diag) i = id i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>k : ℕ<VAR>h : s.card = k<VAR>f : Fin k → α<VAR>hfs : ∀ (x : Fin k), f x ∈ s<VAR>hmono : StrictMono f<GOAL>f = ⇑(s.orderEmbOfFin h)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>k : ℕ<VAR>h : s.card = k<VAR>f : Fin k → α<VAR>hfs : ∀ (x : Fin k), f x ∈ s<VAR>hmono : StrictMono f<GOAL>Set.range f = Set.range ⇑(s.orderEmbOfFin h)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>k : ℕ<VAR>h : s.card = k<VAR>f : Fin k → α<VAR>hfs : ∀ (x : Fin k), f x ∈ s<VAR>hmono : StrictMono f<GOAL>image f univ = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>k : ℕ<VAR>h : s.card = k<VAR>f : Fin k → α<VAR>hfs : ∀ (x : Fin k), f x ∈ s<VAR>hmono : StrictMono f<VAR>x : α<VAR>hx : x ∈ image f univ<GOAL>x ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>k : ℕ<VAR>h : s.card = k<VAR>f : Fin k → α<VAR>hfs : ∀ (x : Fin k), f x ∈ s<VAR>hmono : StrictMono f<GOAL>s.card ≤ (image f univ).card
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Abelian C<VAR>inst✝¹ : HasPullbacks C<VAR>W X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : Epi f<VAR>s : PullbackCone f g<VAR>hs : IsLimit s<VAR>this : Epi ((limit.cone (cospan f g)).π.app WalkingCospan.right)<GOAL>Epi s.snd
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π π₁✝ π₂✝ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>π₁ π₂ : Prepartition I<VAR>Hle : π₁ ≤ π₂<GOAL>π₁.restrict J ≤ π₂.restrict J
<VAR>ι : Type u_1<VAR>I J J₁✝ J₂ : Box ι<VAR>π π₁✝ π₂✝ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>π₁ π₂ : Prepartition I<VAR>Hle : π₁ ≤ π₂<VAR>J₁ : WithBot (Box ι)<VAR>hJ₁ : J₁ ∈ Finset.image (fun J' => ↑J ⊓ ↑J') π₁.boxes<VAR>hne : J₁ ≠ ⊥<GOAL>∃ J' ∈ Finset.image (fun J' => ↑J ⊓ ↑J') π₂.boxes, J₁ ≤ J'
<VAR>ι : Type u_1<VAR>I J J₁✝ J₂ : Box ι<VAR>π π₁✝ π₂✝ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>π₁ π₂ : Prepartition I<VAR>Hle : π₁ ≤ π₂<VAR>J₁ : WithBot (Box ι)<VAR>hJ₁ : ∃ a ∈ π₁.boxes, ↑J ⊓ ↑a = J₁<VAR>hne : J₁ ≠ ⊥<GOAL>∃ J' ∈ Finset.image (fun J' => ↑J ⊓ ↑J') π₂.boxes, J₁ ≤ J'
<VAR>ι : Type u_1<VAR>I J J₁✝ J₂✝ : Box ι<VAR>π π₁✝ π₂✝ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>π₁ π₂ : Prepartition I<VAR>Hle : π₁ ≤ π₂<VAR>J₁ : Box ι<VAR>hJ₁ : J₁ ∈ π₁.boxes<VAR>hne : ↑J ⊓ ↑J₁ ≠ ⊥<VAR>J₂ : Box ι<VAR>hJ₂ : J₂ ∈ π₂<VAR>hle : J₁ ≤ J₂<GOAL>∃ J' ∈ Finset.image (fun J' => ↑J ⊓ ↑J') π₂.boxes, ↑J ⊓ ↑J₁ ≤ J'
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>x p : ℝ<VAR>hp : 1 < p<GOAL>HasDerivAt (fun x => ‖x‖ ^ p) (p * ‖x‖ ^ (p - 2) * x) x
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>x p : ℝ<VAR>hp : 1 < p<GOAL>p * ‖x‖ ^ (p - 2) * x = ((p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x) 1
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>n : Type w<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Invertible 2<VAR>m : Type w<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : Fintype m<VAR>Q : QuadraticMap R (n → R) R<VAR>f : (n → R) →ₗ[R] n → R<GOAL>(Q.comp f).discr = (LinearMap.toMatrix' f).det * (LinearMap.toMatrix' f).det * Q.discr