ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>h : G.IsSRGWith n k ℓ μ<VAR>v w : V<VAR>hn : v ≠ w<VAR>hna : v ≠ w → G.Adj v w<VAR>h2' : G.Adj v w<GOAL>((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ).card = n - (2 * k - ℓ)
<VAR>α : Type u<VAR>l✝ l' l : List α<VAR>h : l ≠ []<GOAL>l.cyclicPermutations = (zipWith (fun x x_1 => x ++ x_1) l.tails l.inits).dropLast
<VAR>α : Type u<VAR>l l' : List α<VAR>hd : α<VAR>tl : List α<VAR>h : hd :: tl ≠ []<GOAL>(hd :: tl).cyclicPermutations = (zipWith (fun x x_1 => x ++ x_1) (hd :: tl).tails (hd :: tl).inits).dropLast
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<GOAL>W.Nonsingular 0 0 ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : CountableOrCountablyGenerated α β<VAR>ρ : Measure (β × Ω)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>f : β × Ω → ℝ≥0∞<VAR>hf : Measurable f<VAR>t : Set Ω<VAR>ht : MeasurableSet t<GOAL>∫⁻ (b : β), ∫⁻ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫⁻ (x : β × Ω) in Set.univ ×ˢ t, f x ∂ρ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : CountableOrCountablyGenerated α β<VAR>ρ : Measure (β × Ω)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>f : β × Ω → ℝ≥0∞<VAR>hf : Measurable f<VAR>t : Set Ω<VAR>ht : MeasurableSet t<GOAL>∫⁻ (b : β), ∫⁻ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫⁻ (b : β) in Set.univ, ∫⁻ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J J₁ J₂ : LieIdeal R L'<GOAL>⁅comap f J₁, comap f J₂⁆ ≤ comap f ⁅J₁, J₂⁆
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J J₁ J₂ : LieIdeal R L'<GOAL>map f ⁅comap f J₁, comap f J₂⁆ ≤ ⁅J₁, J₂⁆
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>‖↑p‖ < 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>(↑p)⁻¹ < 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>1 < ↑p
<VAR>m n a b c d : ℤ<GOAL>-a ≡ -b [ZMOD n] ↔ a ≡ b [ZMOD n]
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>deriv (fun x => x * log x) x = log x + 1
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>deriv (fun x => x) x * log x + x * deriv log x = log x + 1
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>x * x⁻¹ = 1
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>r : R<GOAL>toLaurent (Polynomial.C r * X ^ n) = C r * T ↑n
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<VAR>a : ℝ<VAR>ha : 0 < a<GOAL>∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) • f (a * t) = ↑a ^ (-s) • ∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) • f t
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<VAR>a : ℝ<VAR>ha : 0 < a<VAR>this : EqOn (fun t => ↑t ^ (s - 1) • f (a * t)) (fun t => ↑a ^ (1 - s) • (fun u => ↑u ^ (s - 1) • f u) (a * t)) (Ioi 0)<GOAL>∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) • f (a * t) = ↑a ^ (-s) • ∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) • f t
<VAR>n m : ℕ<VAR>a b : Fin (n + 1)<VAR>ha : a.succ ≠ last (n + 1)<GOAL>a.succ.castPred ha ≤ b ↔ a < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝ : TopologicalSpace δ<VAR>f : γ → α<VAR>g : γ → δ<VAR>h : δ → β<VAR>di : DenseInducing i<VAR>b : β<VAR>s : Set β<VAR>hs : s ∈ 𝓝 b<GOAL>∃ a, i a ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝ : TopologicalSpace δ<VAR>f : γ → α<VAR>g : γ → δ<VAR>h : δ → β<VAR>di : DenseInducing i<VAR>b : β<VAR>s : Set β<VAR>hs : s ∈ 𝓝 b<VAR>a : α<VAR>ha : i a ∈ s<GOAL>∃ a, i a ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>inst✝² : Fintype β<VAR>inst✝¹ : DecidableEq α<VAR>f : β → Set α<VAR>inst✝ : (w : β) → Fintype ↑(f w)<VAR>v : α<GOAL>v ∈ (⋃ x, f x).toFinset ↔ v ∈ Finset.univ.biUnion fun x => (f x).toFinset
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>inst✝ : Nontrivial R<VAR>x : R<GOAL>(C (X - C x)).natDegree < W.polynomial.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>inst✝ : Nontrivial R<VAR>x : R<GOAL>0 < 2
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>h : MDifferentiableWithinAt I I' f s x<GOAL>mfderivWithin I I' f s x = fderivWithin 𝕜 (writtenInExtChartAt I I' x f) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)
<VAR>α : Type u_1<VAR>inst✝⁶ : MetricSpace α<VAR>inst✝⁵ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁴ : IsUnifLocDoublingMeasure μ<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>E : Type u_2<VAR>inst✝ : NormedAddCommGroup E<VAR>S : Set α<VAR>K : ℝ<GOAL>∀ᵐ (x : α) ∂μ.restrict S, ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ), Tendsto δ l (𝓝[>] 0) → (∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)) → Tendsto (fun j => μ (S ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : BEq α<VAR>inst✝ : Hashable α<VAR>rank : α → Nat<VAR>l : List (α × β)<VAR>i : Nat<VAR>hl₁ : ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α], List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) l<VAR>hl₂ : ∀ (x : α × β), x ∈ l → rank x.fst = i<VAR>target : Buckets α β<VAR>ht₁ : target.WF<VAR>ht₂ : ∀ (bucket : AssocList α β), bucket ∈ target.val.data → AssocList.All (fun k x => rank k ≤ i ∧ ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α] (x : α × β), x ∈ l → ¬(x.fst == k) = true) bucket<GOAL>(List.foldl (fun d x => reinsertAux d x.fst x.snd) target l).WF ∧ ∀ (bucket : AssocList α β), bucket ∈ (List.foldl (fun d x => reinsertAux d x.fst x.snd) target l).val.data → AssocList.All (fun k x => rank k ≤ i) bucket
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra R A<VAR>θ : ℂ<VAR>n : ℤ<GOAL>eval (cos θ) (U ℂ n) * sin θ = sin ((↑n + 1) * θ)
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v w : V<VAR>e : Sym2 V<VAR>G₁ G₂ : SimpleGraph V<VAR>x✝ : Sym2 V<VAR>x y : V<GOAL>Quot.mk (Sym2.Rel V) (x, y) ∈ (G₁ \ G₂).edgeSet ↔ Quot.mk (Sym2.Rel V) (x, y) ∈ G₁.edgeSet \ G₂.edgeSet
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>x : α<VAR>y : ℤ<GOAL>round (x + ↑y) = round x + y
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : 0 < c → c < b → a ≠ ⊤<GOAL>a * (b - c) = a * b - a * c
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : 0 < c → c < b → a ≠ ⊤<GOAL>(b - c) * a = b * a - c * a
<VAR>n✝ m n : ℕ<VAR>p : Fin n<VAR>i : Fin (n + 1)<GOAL>(p.predAbove i).rev = p.rev.predAbove i.rev
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>p : ℝ≥0∞<VAR>G : Type u_5<VAR>F' : Type u_6<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedAddCommGroup F'<VAR>inst✝⁴ : NormedSpace ℝ F'<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : SMulCommClass ℝ 𝕜 E<VAR>ν : Measure α<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) (μ + ν)<GOAL>integral (μ + ν) f = integral μ f + integral ν f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>p : ℝ≥0∞<VAR>G : Type u_5<VAR>F' : Type u_6<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedAddCommGroup F'<VAR>inst✝⁴ : NormedSpace ℝ F'<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : SMulCommClass ℝ 𝕜 E<VAR>ν : Measure α<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) (μ + ν)<GOAL>setToSimpleFunc (weightedSMul (μ + ν)) f = setToSimpleFunc (weightedSMul μ) f + setToSimpleFunc (weightedSMul ν) f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>p : ℝ≥0∞<VAR>G : Type u_5<VAR>F' : Type u_6<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedAddCommGroup F'<VAR>inst✝⁴ : NormedSpace ℝ F'<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : SMulCommClass ℝ 𝕜 E<VAR>ν : Measure α<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) (μ + ν)<VAR>s : Set α<VAR>x✝ : MeasurableSet s<VAR>hμνs : (μ + ν) s < ⊤<GOAL>weightedSMul (μ + ν) s = weightedSMul μ s + weightedSMul ν s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>p : ℝ≥0∞<VAR>G : Type u_5<VAR>F' : Type u_6<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedAddCommGroup F'<VAR>inst✝⁴ : NormedSpace ℝ F'<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : SMulCommClass ℝ 𝕜 E<VAR>ν : Measure α<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) (μ + ν)<VAR>s : Set α<VAR>x✝ : MeasurableSet s<VAR>hμνs : μ s ≠ ⊤ ∧ ν s ≠ ⊤<GOAL>weightedSMul (μ + ν) s = weightedSMul μ s + weightedSMul ν s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>κ : ι → Sort u_1<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>e : α ≃o β<VAR>s : Set β<GOAL>BddAbove (⇑e ⁻¹' s) ↔ BddAbove s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Set α<VAR>a✝ a : α<VAR>ha : a ∈ t<GOAL>t \ {a} ⋖ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t u v : Finset α<VAR>a✝ b a : α<VAR>s : Finset α<VAR>h : a ∉ s<GOAL>(insert a s).val = a ::ₘ s.val
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l₁ xs ys : List α<GOAL>List.filter p l₁ <:+: List.filter p (xs ++ l₁ ++ ys)
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l₁ xs ys : List α<GOAL>List.filter p l₁ <:+: List.filter p xs ++ List.filter p l₁ ++ List.filter p ys
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>H : T ∈ distinguishedTriangles<GOAL>T.mor₃ ≫ (shiftFunctor C 1).map T.mor₁ = 0
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>H : T ∈ distinguishedTriangles<VAR>H₂ : T.rotate.rotate ∈ distinguishedTriangles<GOAL>T.mor₃ ≫ (shiftFunctor C 1).map T.mor₁ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f : α → β<VAR>s✝ t✝ s : Set α<VAR>hs : s.Nonempty<VAR>t : Set β<VAR>a : β<GOAL>s ⊆ (fun x => a) ⁻¹' t ↔ a ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>π : δ → Type u_6<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : (a : δ) → MeasurableSpace (π a)<VAR>inst✝¹ : MeasurableSpace γ<VAR>a : δ<VAR>inst✝ : DecidableEq δ<GOAL>Measurable fun p => update p.1 a p.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>π : δ → Type u_6<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : (a : δ) → MeasurableSpace (π a)<VAR>inst✝¹ : MeasurableSpace γ<VAR>a : δ<VAR>inst✝ : DecidableEq δ<GOAL>∀ (a_1 : δ), Measurable fun x => update x.1 a x.2 a_1
<VAR>a b✝ : ℤ<VAR>n✝ : ℕ<VAR>b : Bool<VAR>n : ℤ<GOAL>(bit b n).div2 = n
<VAR>a b✝ : ℤ<VAR>n✝ : ℕ<VAR>b : Bool<VAR>n : ℤ<GOAL>(bif b then 1 else 0) / 2 = 0
<VAR>a b✝ : ℤ<VAR>n✝ : ℕ<VAR>b : Bool<VAR>n : ℤ<GOAL>2 ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>f : ℕ → α<VAR>k : ℕ<GOAL>liminf (f ∘ fun x => x + k) atTop = liminf f atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>l✝ : List α<VAR>x : α<VAR>inst✝ : Fintype α<VAR>l : List α<VAR>h : l.Nodup<VAR>h' : ∀ (x : α), l ≠ [x]<GOAL>l.formPerm.support = l.toFinset
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>l✝ : List α<VAR>x : α<VAR>inst✝ : Fintype α<VAR>l : List α<VAR>h : l.Nodup<VAR>h' : ∀ (x : α), l ≠ [x]<GOAL>↑l.formPerm.support = ↑l.toFinset
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>l✝ : List α<VAR>x : α<VAR>inst✝ : Fintype α<VAR>l : List α<VAR>h : l.Nodup<VAR>h' : ∀ (x : α), l ≠ [x]<GOAL>↑l.formPerm.support = {x | l.formPerm x ≠ x}
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y : α<GOAL>Inseparable x y ↔ dist x y = 0
<VAR>M : Type u_1<VAR>inst✝² : CommMonoidWithZero M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoidWithZero N<VAR>P : Type u_3<VAR>inst✝ : CommMonoidWithZero P<VAR>f : S.LocalizationMap N<GOAL>f.toMap (f.sec 0).1 = 0
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : a ≠ ⊤ ∨ b ≠ ⊤<GOAL>a - b < c → a < b + c
<VAR>a c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : a ≠ ⊤ ∨ ⊤ ≠ ⊤<GOAL>a - ⊤ < c → a < ⊤ + c
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : a ≠ ⊤ ∨ b ≠ ⊤<VAR>hb : b ≠ ⊤<GOAL>a - b < c → a < b + c
<VAR>n✝ n : ℕ<VAR>n1 : n ≠ 1<VAR>n0 : ¬n = 0<GOAL>Nat.minFacProp n n.minFac
<VAR>n✝ n : ℕ<VAR>n1 : n ≠ 1<VAR>n0 : ¬n = 0<VAR>n2 : 2 ≤ n<GOAL>Nat.minFacProp n n.minFac
<VAR>n✝ n : ℕ<VAR>n1 : n ≠ 1<VAR>n0 : ¬n = 0<VAR>n2 : 2 ≤ n<GOAL>Nat.minFacProp n (if 2 ∣ n then 2 else n.minFacAux 3)
<VAR>z : ℂ<VAR>hz : z = 0<GOAL>|z.im / abs z| ≤ 1
<VAR>z : ℂ<VAR>hz : ¬z = 0<GOAL>|z.im / abs z| ≤ 1
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>ClusterPt x (𝓟 s) ↔ ∃ᶠ (y : X) in 𝓝 x, y ∈ s
<VAR>α β γ : Type u<VAR>t : Type u → Type u<VAR>inst✝² : Traversable t<VAR>inst✝¹ : LawfulTraversable t<VAR>inst✝ : Monoid γ<VAR>f : α → β<VAR>g : β → γ<VAR>xs : t α<GOAL>foldMap g (f <$> xs) = foldMap (g ∘ f) xs
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>cosZeta (-a) s = cosZeta a s
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p✝ q✝ p q : R[X]<VAR>h2 : p * q ≠ 0<GOAL>p.natDegree ≤ (p * q).natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p✝ q✝ p q : R[X]<VAR>h2 : p ≠ 0 ∧ q ≠ 0<GOAL>p.natDegree ≤ (p * q).natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p✝ q✝ p q : R[X]<VAR>h2 : p ≠ 0 ∧ q ≠ 0<GOAL>p.natDegree ≤ p.natDegree + q.natDegree
<VAR>α : Type u_1<VAR>inst✝² : BooleanAlgebra α<VAR>inst✝¹ : Nontrivial α<VAR>inst✝ : Fintype α<VAR>s : Finset α<VAR>hs : (↑s).Intersecting<GOAL>(∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t) ↔ 2 * s.card = Fintype.card α
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>A B C : Set α<VAR>D E : Set ↑A<VAR>S : Set (Set α)<VAR>T : Set (Set ↑A)<VAR>s : ι → Set α<VAR>t : ι → Set ↑A<GOAL>↑(⋃₀ T) = ⋃₀ {x | ∃ B ∈ T, ↑B = x}
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<GOAL>¬λ ^ 2 ∣ S.a + ↑η * S.b
<VAR>η✝ : Type u_1<VAR>α✝ : Type u_2<VAR>ι✝ : Type u_3<VAR>κ✝ : Type u_4<VAR>η : Type u_5<VAR>α : Type u_6<VAR>ι : Type u_7<VAR>κ : Type u_8<VAR>l✝ : Subspace η α ι<VAR>x : η → α<VAR>i✝ : ι<VAR>a : α<VAR>e : η<VAR>inst✝ : Nontrivial α<VAR>l m : Subspace η α ι<VAR>hlm : ↑l = ↑m<VAR>i : ι<GOAL>l.idxFun i = m.idxFun i
<VAR>η✝ : Type u_1<VAR>α✝ : Type u_2<VAR>ι✝ : Type u_3<VAR>κ✝ : Type u_4<VAR>η : Type u_5<VAR>α : Type u_6<VAR>ι : Type u_7<VAR>κ : Type u_8<VAR>l✝ : Subspace η α ι<VAR>x : η → α<VAR>i✝ : ι<VAR>a : α<VAR>e : η<VAR>inst✝ : Nontrivial α<VAR>l m : Subspace η α ι<VAR>i : ι<VAR>hlm : ∀ (a : η → α) (a_1 : ι), ↑l a a_1 = ↑m a a_1<GOAL>l.idxFun i = m.idxFun i
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>P : Type w₂<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : LieRing L<VAR>inst✝¹² : LieAlgebra R L<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : AddCommGroup N<VAR>inst✝⁹ : AddCommGroup P<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module R N<VAR>inst✝⁶ : Module R P<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieRingModule L N<VAR>inst✝³ : LieRingModule L P<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : LieModule R L N<VAR>inst✝ : LieModule R L P<VAR>f : M →ₗ⁅R,L⁆ N →ₗ[R] P<VAR>x : L<VAR>m : M<VAR>n : N<GOAL>⁅x, (f m) n⁆ = (f ⁅x, m⁆) n + (f m) ⁅x, n⁆
<VAR>o : Ordinal.{u_1}<VAR>ho : Principal (fun x x_1 => x * x_1) o<VAR>ho₂ : o ≠ 2<GOAL>Principal (fun x x_1 => x + x_1) o
<VAR>o : Ordinal.{u_1}<VAR>ho : Principal (fun x x_1 => x * x_1) o<VAR>ho₂ : o ≠ 2<VAR>ho₁ : o < 2<GOAL>Principal (fun x x_1 => x + x_1) o
<VAR>o : Ordinal.{u_1}<VAR>ho : Principal (fun x x_1 => x * x_1) o<VAR>ho₂✝ : o ≠ 2<VAR>ho₂ : o > 2<GOAL>Principal (fun x x_1 => x + x_1) o
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>f : F[X]<VAR>q : ℕ<VAR>inst✝ : ExpChar F q<VAR>hm : f.Monic<VAR>hi : Irreducible f<GOAL>f.natSepDegree = 1 ↔ ∃ n y, f = X ^ q ^ n - C y
<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PredOrder α<VAR>a b : α<VAR>C : α → Sort u_2<GOAL>¬IsPredLimit a ↔ ∃ b, ¬IsMin b ∧ pred b = a
<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PredOrder α<VAR>a b : α<VAR>C : α → Sort u_2<GOAL>¬IsSuccLimit (toDual a) ↔ ∃ b, ¬IsMin b ∧ pred b = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<GOAL>(μ + ν).toENNRealVectorMeasure = μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>↑(μ + ν).toENNRealVectorMeasure i = ↑(μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure) i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>K : Type u_5<VAR>inst✝¹ : Zero β<VAR>inst✝ : Zero γ<VAR>g : β → γ<VAR>hg : g 0 = 0<VAR>f : α →ₛ β<VAR>s : Set α<VAR>x : α<VAR>hs : MeasurableSet s<GOAL>↑(map g (f.restrict s)) x = ↑((map g f).restrict s) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>K : Type u_5<VAR>inst✝¹ : Zero β<VAR>inst✝ : Zero γ<VAR>g : β → γ<VAR>hg : g 0 = 0<VAR>f : α →ₛ β<VAR>s : Set α<VAR>x : α<VAR>hs : ¬MeasurableSet s<GOAL>↑(map g (f.restrict s)) x = ↑((map g f).restrict s) x
<VAR>q a b c : ℚ<GOAL>a + b = b + a
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n m : ℕ<GOAL>0 < orderOf x ↔ IsOfFinOrder x
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝¹¹ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝¹⁰ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁹ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>E : Type u_9<VAR>inst✝⁶ : AddCommMonoid E<VAR>inst✝⁵ : Module R E<VAR>F : Type u_10<VAR>inst✝⁴ : AddCommMonoid F<VAR>t : ι → Type u_11<VAR>t' : ι → Type u_12<VAR>inst✝³ : (i : ι) → AddCommMonoid (t i)<VAR>inst✝² : (i : ι) → Module R (t i)<VAR>inst✝¹ : (i : ι) → AddCommMonoid (t' i)<VAR>inst✝ : (i : ι) → Module R (t' i)<VAR>g : (i : ι) → t i →ₗ[R] t' i<VAR>f : (i : ι) → s i →ₗ[R] t i<VAR>x✝ : (i : ι) → s i<GOAL>((map fun i => LinearMap.id).compMultilinearMap (tprod R)) x✝ = (LinearMap.id.compMultilinearMap (tprod R)) x✝
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>s : Set ℝ<VAR>l : ℝ≥0<VAR>h : HasConstantSpeedOnWith f s l<VAR>x y : ℝ<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>BoundedVariationOn f (s ∩ Icc x y)
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>map (LinearMap.fst R M M₂) (snd R M M₂) = ⊥
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>map (LinearMap.fst R M M₂) (snd R M M₂) ≤ ⊥
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<VAR>x : M<GOAL>x ∈ map (LinearMap.fst R M M₂) (snd R M M₂) → x ∈ ⊥
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ s : Multiset α<VAR>f : α → β<VAR>x : { x // x ∈ s }<GOAL>map (fun j => f ↑j) (s.attach.erase x) = map f (s.erase ↑x)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ s : Multiset α<VAR>f : α → β<VAR>x : { x // x ∈ s }<GOAL>map (fun x => (f ∘ val) x) (s.attach.erase x) = map f (s.erase ↑x)
<VAR>R : Type u<VAR>a✝ b : R<VAR>m n✝ : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q p : R[X]<VAR>n : ℕ<VAR>a : R<VAR>inst✝ : Decidable (a = 0)<GOAL>(p.update n a).support = if a = 0 then p.support.erase n else insert n p.support
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁶ : Ring k<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module k V<VAR>inst✝³ : AffineSpace V P<VAR>ι : Type u_4<VAR>V₂ : Type u_5<VAR>P₂ : Type u_6<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module k V₂<VAR>inst✝ : AffineSpace V₂ P₂<VAR>p : ι → P<VAR>hai : AffineIndependent k p<VAR>f : P →ᵃ[k] P₂<VAR>hf : Injective ⇑f<GOAL>AffineIndependent k (⇑f ∘ p)