ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : NonUnitalSemiring A<VAR>inst✝¹³ : StarRing A<VAR>inst✝¹² : Module R A<VAR>inst✝¹¹ : IsScalarTower R A A<VAR>inst✝¹⁰ : SMulCommClass R A A<VAR>inst✝⁹ : StarModule R A<VAR>inst✝⁸ : NonUnitalSemiring B<VAR>inst✝⁷ : StarRing B<VAR>inst✝⁶ : Module R B<VAR>inst✝⁵ : IsScalarTower R B B<VAR>inst✝⁴ : SMulCommClass R B B<VAR>inst✝³ : StarModule R B<VAR>inst✝² : FunLike F A B<VAR>inst✝¹ : NonUnitalAlgHomClass F R A B<VAR>inst✝ : NonUnitalStarAlgHomClass F R A B<VAR>S : Set (NonUnitalStarSubalgebra R A)<VAR>x : A<GOAL>x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>n m : ℕ<VAR>h : n ≠ m<GOAL>(Disjoint on MeasureTheory.SignedMeasure.restrictNonposSeq s i) n m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>n m : ℕ<VAR>h : n ≠ m<GOAL>MeasureTheory.SignedMeasure.restrictNonposSeq s i n ∩ MeasureTheory.SignedMeasure.restrictNonposSeq s i m = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>n m : ℕ<VAR>h✝ : n ≠ m<VAR>h : n < m<GOAL>MeasureTheory.SignedMeasure.restrictNonposSeq s i n ∩ MeasureTheory.SignedMeasure.restrictNonposSeq s i m = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>n m : ℕ<VAR>h✝ : n ≠ m<VAR>h : n > m<GOAL>MeasureTheory.SignedMeasure.restrictNonposSeq s i n ∩ MeasureTheory.SignedMeasure.restrictNonposSeq s i m = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s✝ : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>s : Set (α × β)<GOAL>s ∈ f ×ˢ 𝓟 t ↔ {a | ∀ b ∈ t, (a, b) ∈ s} ∈ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s✝ : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>s : Set (α × β)<GOAL>(∃ t₁ ∈ f, ∃ t₂ ∈ 𝓟 t, t₁ ×ˢ t₂ ⊆ s) ↔ ∃ t_1 ∈ f, t_1 ⊆ {a | ∀ b ∈ t, (a, b) ∈ s}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s✝ : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>s : Set (α × β)<VAR>u : Set α<GOAL>(∃ t₂ ∈ 𝓟 t, u ×ˢ t₂ ⊆ s) → u ⊆ {a | ∀ b ∈ t, (a, b) ∈ s}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s✝ : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>s : Set (α × β)<VAR>u : Set α<VAR>h : u ⊆ {a | ∀ b ∈ t, (a, b) ∈ s}<GOAL>u ×ˢ t ⊆ s
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>𝒢 : Set Cᵒᵖ<GOAL>IsCodetecting 𝒢.unop ↔ IsDetecting 𝒢
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n✝ : ℤ<VAR>γ✝ γ₁ γ₂ : Cochain K L n✝<VAR>n' a : ℤ<VAR>γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'<VAR>n : ℤ<VAR>hn : n' + a = n<VAR>x : R<GOAL>(rightShiftLinearEquiv R K L n a n' hn).symm (x • γ) = x • γ.rightUnshift n hn
<VAR>α : Type u<VAR>β : Type v<VAR>x✝ x y : FreeMagma α<VAR>hx : (toFreeSemigroup x).length = x.length<VAR>hy : (toFreeSemigroup y).length = y.length<GOAL>(toFreeSemigroup (x * y)).length = (x * y).length
<VAR>α : Type u<VAR>β : Type v<VAR>x✝ x y : FreeMagma α<VAR>hx : (toFreeSemigroup x).length = x.length<VAR>hy : (toFreeSemigroup y).length = y.length<GOAL>x.length + y.length = (x * y).length
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>g✝ : P →ₗ[R] Q<VAR>f✝ : N →ₗ[R] P<VAR>f : M →ₗ[R] P<VAR>g : N →ₗ[R] Q<VAR>f' : S →ₗ[R] M<GOAL>map f g ∘ₗ rTensor N f' = map (f ∘ₗ f') g
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>boxes : Finset (WithBot (Box ι))<VAR>le_of_mem : ∀ J ∈ boxes, J ≤ ↑I<VAR>pairwise_disjoint : (↑boxes).Pairwise Disjoint<GOAL>⋃ J, ⋃ (_ : ↑J ∈ boxes), ↑J = ⋃ J ∈ boxes, ↑J
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x✝ y z : E<VAR>δ ε : ℝ<VAR>hε : 0 ≤ ε<VAR>hδ : 0 ≤ δ<VAR>s : Set E<VAR>x : E<GOAL>x ∈ cthickening (ε + δ) s → x ∈ cthickening ε (cthickening δ s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x✝ y z : E<VAR>δ ε : ℝ<VAR>hε : 0 ≤ ε<VAR>hδ : 0 ≤ δ<VAR>s : Set E<VAR>x : E<GOAL>infEdist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ → infEdist x s - ENNReal.ofReal δ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>F : Filter R<VAR>inst✝¹ : LinearOrder R<VAR>inst✝ : LinearOrder S<VAR>l : R<VAR>freq_ge : ∃ᶠ (x : R) in F, l ≤ x<VAR>lbot : ¬IsBot l<GOAL>IsCobounded (fun x x_1 => x ≤ x_1) F
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>F : Filter R<VAR>inst✝¹ : LinearOrder R<VAR>inst✝ : LinearOrder S<VAR>l : R<VAR>freq_ge : ∃ᶠ (x : R) in F, l ≤ x<VAR>lbot : ¬IsBot l<VAR>l' : R<VAR>hl' : l' < l<GOAL>IsCobounded (fun x x_1 => x ≤ x_1) F
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>F : Filter R<VAR>inst✝¹ : LinearOrder R<VAR>inst✝ : LinearOrder S<VAR>l : R<VAR>freq_ge : ∃ᶠ (x : R) in F, l ≤ x<VAR>lbot : ¬IsBot l<VAR>l' : R<VAR>hl' : l' < l<VAR>u : R<VAR>hu : ∀ᶠ (x : R) in F, (fun x x_1 => x ≤ x_1) x u<GOAL>l' ≤ u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>F : Filter R<VAR>inst✝¹ : LinearOrder R<VAR>inst✝ : LinearOrder S<VAR>l : R<VAR>freq_ge : ∃ᶠ (x : R) in F, l ≤ x<VAR>lbot : ¬IsBot l<VAR>l' : R<VAR>hl' : l' < l<VAR>u : R<VAR>hu : ∀ᶠ (x : R) in F, (fun x x_1 => x ≤ x_1) x u<VAR>key : ∃ᶠ (x : R) in F, l ≤ x ∧ x ≤ u<GOAL>l' ≤ u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>F : Filter R<VAR>inst✝¹ : LinearOrder R<VAR>inst✝ : LinearOrder S<VAR>l : R<VAR>freq_ge : ∃ᶠ (x : R) in F, l ≤ x<VAR>lbot : ¬IsBot l<VAR>l' : R<VAR>hl' : l' < l<VAR>u : R<VAR>hu : ∀ᶠ (x : R) in F, (fun x x_1 => x ≤ x_1) x u<VAR>key : ∃ᶠ (x : R) in F, l ≤ x ∧ x ≤ u<VAR>w : R<VAR>l_le_w : l ≤ w<VAR>w_le_u : w ≤ u<GOAL>l' ≤ u
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝ : CommRing R<VAR>f✝ f : R[X]<GOAL>eval₂ (of f) (root f) f = 0
<VAR>α✝ : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : MeasurableSpace M<VAR>inst✝ : MeasurableMul₂ M<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : ι → α → M<VAR>s : Finset ι<VAR>hf : ∀ i ∈ s, AEMeasurable (f i) μ<GOAL>AEMeasurable (fun a => ∏ i ∈ s, f i a) μ
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<GOAL>W.ΨSq 0 = 0
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>s t : Set α<VAR>a x y : α<GOAL>a ∈ exterior s ↔ ∀ (U : Set α), IsOpen U → s ⊆ U → a ∈ U
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>N' : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : AddCommGroup N'<VAR>inst✝¹ : Module R N'<VAR>S : Submonoid R<VAR>f : N →ₗ[R] N'<VAR>inst✝ : IsLocalizedModule S f<VAR>hM : Finite R M<VAR>g₁ g₂ : M →ₗ[R] N<VAR>h : f ∘ₗ g₁ = f ∘ₗ g₂<GOAL>∃ s, s • g₁ = s • g₂
<VAR>a✝ b c n a : ℕ<GOAL>image (fun x => x % a) (Ico n (n + a)) = range a
<VAR>a b c n : ℕ<GOAL>image (fun x => x % 0) (Ico n (n + 0)) = range 0
<VAR>a✝ b c n a : ℕ<VAR>ha : a ≠ 0<GOAL>image (fun x => x % a) (Ico n (n + a)) = range a
<VAR>a✝ b c n a : ℕ<VAR>ha : a ≠ 0<VAR>i : ℕ<GOAL>i ∈ image (fun x => x % a) (Ico n (n + a)) ↔ i ∈ range a
<VAR>a✝ b c n a : ℕ<VAR>ha : a ≠ 0<VAR>i : ℕ<GOAL>(∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) ↔ i < a
<VAR>a✝ b c n a : ℕ<VAR>ha : a ≠ 0<VAR>i : ℕ<VAR>hia : i < a<GOAL>∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
<VAR>a✝ b c n a : ℕ<VAR>ha : a ≠ 0<VAR>i : ℕ<VAR>hia : i < a<VAR>hn : n % a + a * (n / a) = n<GOAL>∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
<VAR>a✝ b c n a : ℕ<VAR>ha : a ≠ 0<VAR>i : ℕ<VAR>hia : i < a<VAR>hn : n % a + a * (n / a) = n<VAR>hi : i < n % a<GOAL>∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
<VAR>a✝ b c n a : ℕ<VAR>ha : a ≠ 0<VAR>i : ℕ<VAR>hia : i < a<VAR>hn : n % a + a * (n / a) = n<VAR>hi : n % a ≤ i<GOAL>∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
<VAR>x : ℝ<VAR>h : 1 < x<GOAL>2 * arctan x = arctan (2 * x / (1 - x ^ 2)) + π
<VAR>x : ℝ<VAR>h : 1 < x<GOAL>arctan ((x + x) / (1 - x * x)) + π = arctan (2 * x / (1 - x ^ 2)) + π
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FreeAddMonoid (𝕜 × ((i : ι) → E i))<GOAL>0 ≤ projectiveSeminormAux p
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FreeAddMonoid (𝕜 × ((i : ι) → E i))<GOAL>0 ≤ (List.map (fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) p).sum
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FreeAddMonoid (𝕜 × ((i : ι) → E i))<GOAL>∀ x ∈ List.map (fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) p, 0 ≤ x
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FreeAddMonoid (𝕜 × ((i : ι) → E i))<VAR>a : ℝ<GOAL>a ∈ List.map (fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) p → 0 ≤ a
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FreeAddMonoid (𝕜 × ((i : ι) → E i))<VAR>a : ℝ<GOAL>∀ (x : 𝕜) (x_1 : (i : ι) → E i), (x, x_1) ∈ p → ‖x‖ * ∏ x : ι, ‖x_1 x‖ = a → 0 ≤ a
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FreeAddMonoid (𝕜 × ((i : ι) → E i))<VAR>a : ℝ<VAR>x : 𝕜<VAR>m : (i : ι) → E i<VAR>a✝ : (x, m) ∈ p<VAR>h : ‖x‖ * ∏ x : ι, ‖m x‖ = a<GOAL>0 ≤ ‖x‖ * ∏ x : ι, ‖m x‖
<VAR>a x z✝ z : ℂ<GOAL>|z.arg| ≤ π / 2 ↔ 0 ≤ z.re
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>β✝ : Type u_3<VAR>γ✝ : Type u_4<VAR>κ : ι → Type u_5<VAR>π : ι → Set (Set Ω)<VAR>m : ι → MeasurableSpace Ω<VAR>x✝ : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>S : Finset ι<VAR>s : ι → Set Ω<VAR>β : Type u_6<VAR>γ : Type u_7<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>f : Ω → β<VAR>g : Ω → γ<VAR>μ : Measure Ω<GOAL>IndepFun f g μ ↔ ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → μ (t1 ∩ t2) = μ t1 * μ t2
<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✝³ : AddCancelCommMonoid E<VAR>inst✝² : OrderedAddCommMonoid β<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : StrictConvexOn 𝕜 s f<VAR>c : E<GOAL>StrictConvexOn 𝕜 ((fun z => c + z) ⁻¹' s) (f ∘ fun z => z + c)
<VAR>α β : Type u<VAR>β' : Type v<GOAL>#↑{f | Surjective f} = 0 ↔ #α < #β ∨ #α ≠ 0 ∧ #β = 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>X Y : C<VAR>t : BinaryBicone X Y<VAR>ht : IsColimit t.toCocone<GOAL>t.snd = ht.desc (BinaryCofan.mk 0 (𝟙 Y))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>X Y : C<VAR>t : BinaryBicone X Y<VAR>ht : IsColimit t.toCocone<GOAL>∀ (j : Discrete WalkingPair), t.toCocone.ι.app j ≫ t.snd = (BinaryCofan.mk 0 (𝟙 Y)).ι.app j
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>f g : Arrow C<VAR>inst✝³ : HasImage f.hom<VAR>inst✝² : HasImage g.hom<VAR>sq : f ⟶ g<VAR>inst✝¹ : HasImageMap sq<VAR>inst✝ : HasImageMap (𝟙 f)<GOAL>HasImageMap.imageMap (𝟙 f) = imageMapId f
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>H : Type u_5<VAR>inst✝ : Group H<VAR>f : G ≃* H<VAR>sg : Subgroup H<GOAL>Subgroup.comap (↑f.symm) (Subgroup.comap (↑f) sg) = sg
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>H : Type u_5<VAR>inst✝ : Group H<VAR>f : G ≃* H<VAR>sh : Subgroup G<GOAL>Subgroup.comap (↑f) (Subgroup.comap (↑f.symm) sh) = sh
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>H : Type u_5<VAR>inst✝ : Group H<VAR>f : G ≃* H<VAR>sg1 sg2 : Subgroup H<VAR>h : { toFun := Subgroup.comap ↑f, invFun := Subgroup.comap ↑f.symm, left_inv := ⋯, right_inv := ⋯ } sg1 ≤ { toFun := Subgroup.comap ↑f, invFun := Subgroup.comap ↑f.symm, left_inv := ⋯, right_inv := ⋯ } sg2<GOAL>sg1 ≤ sg2
<VAR>n : ℕ<VAR>h0 : n ≠ 0<GOAL>Squarefree n ↔ n.primeFactorsList.Nodup
<VAR>n : ℕ<VAR>h0 : n ≠ 0<GOAL>(↑n.primeFactorsList).Nodup ↔ n.primeFactorsList.Nodup
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>T : Monad C<VAR>inst✝ : T.Additive<VAR>F G : T.Algebra<VAR>α β : F ⟶ G<GOAL>T.map (α.f + β.f) ≫ G.a = F.a ≫ (α.f + β.f)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>T : Monad C<VAR>inst✝ : T.Additive<VAR>F G : T.Algebra<GOAL>T.map 0 ≫ G.a = F.a ≫ 0
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>T : Monad C<VAR>inst✝ : T.Additive<VAR>F G : T.Algebra<VAR>n : ℕ<VAR>α : F ⟶ G<GOAL>T.map (n • α.f) ≫ G.a = F.a ≫ (n • α.f)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>T : Monad C<VAR>inst✝ : T.Additive<VAR>F G : T.Algebra<VAR>α : F ⟶ G<GOAL>T.map (-α.f) ≫ G.a = F.a ≫ (-α.f)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>T : Monad C<VAR>inst✝ : T.Additive<VAR>F G : T.Algebra<VAR>α β : F ⟶ G<GOAL>T.map (α.f - β.f) ≫ G.a = F.a ≫ (α.f - β.f)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>T : Monad C<VAR>inst✝ : T.Additive<VAR>F G : T.Algebra<VAR>r : ℤ<VAR>α : F ⟶ G<GOAL>T.map (r • α.f) ≫ G.a = F.a ≫ (r • α.f)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>T : Monad C<VAR>inst✝ : T.Additive<VAR>F G : T.Algebra<VAR>a✝ b✝ c✝ : F ⟶ G<GOAL>(a✝ + b✝ + c✝).f = (a✝ + (b✝ + c✝)).f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>T : Monad C<VAR>inst✝ : T.Additive<VAR>F G : T.Algebra<VAR>a✝ : F ⟶ G<GOAL>(0 + a✝).f = a✝.f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>T : Monad C<VAR>inst✝ : T.Additive<VAR>F G : T.Algebra<VAR>a✝ : F ⟶ G<GOAL>(a✝ + 0).f = a✝.f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>T : Monad C<VAR>inst✝ : T.Additive<VAR>F G : T.Algebra<VAR>x✝ : F ⟶ G<GOAL>((fun n α => { f := n • α.f, h := ⋯ }) 0 x✝).f = Algebra.Hom.f 0
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>T : Monad C<VAR>inst✝ : T.Additive<VAR>F G : T.Algebra<VAR>n✝ : ℕ<VAR>x✝ : F ⟶ G<GOAL>((fun n α => { f := n • α.f, h := ⋯ }) (n✝ + 1) x✝).f = ((fun n α => { f := n • α.f, h := ⋯ }) n✝ x✝ + x✝).f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>T : Monad C<VAR>inst✝ : T.Additive<VAR>F G : T.Algebra<VAR>a✝ b✝ : F ⟶ G<GOAL>(a✝ - b✝).f = (a✝ + -b✝).f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>T : Monad C<VAR>inst✝ : T.Additive<VAR>F G : T.Algebra<VAR>a✝ : F ⟶ G<GOAL>((fun r α => { f := r • α.f, h := ⋯ }) 0 a✝).f = Algebra.Hom.f 0
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>T : Monad C<VAR>inst✝ : T.Additive<VAR>F G : T.Algebra<VAR>n✝ : ℕ<VAR>a✝ : F ⟶ G<GOAL>↑(n✝ + 1) • a✝.f = ({ f := ↑n✝ • a✝.f, h := ⋯ } + a✝).f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>T : Monad C<VAR>inst✝ : T.Additive<VAR>F G : T.Algebra<VAR>n✝ : ℕ<VAR>a✝ : F ⟶ G<GOAL>n✝ • a✝.f + a✝.f = ({ f := n✝ • a✝.f, h := ⋯ } + a✝).f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>T : Monad C<VAR>inst✝ : T.Additive<VAR>F G : T.Algebra<VAR>n✝ : ℕ<VAR>a✝ : F ⟶ G<GOAL>((fun r α => { f := r • α.f, h := ⋯ }) (Int.negSucc n✝) a✝).f = (-(fun r α => { f := r • α.f, h := ⋯ }) (↑n✝.succ) a✝).f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>T : Monad C<VAR>inst✝ : T.Additive<VAR>F G : T.Algebra<VAR>a✝ : F ⟶ G<GOAL>(-a✝ + a✝).f = Algebra.Hom.f 0
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>T : Monad C<VAR>inst✝ : T.Additive<VAR>F G : T.Algebra<VAR>a✝ b✝ : F ⟶ G<GOAL>(a✝ + b✝).f = (b✝ + a✝).f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>T : Monad C<VAR>inst✝ : T.Additive<VAR>P✝ Q✝ R✝ : T.Algebra<VAR>f✝ f'✝ : P✝ ⟶ Q✝<VAR>g✝ : Q✝ ⟶ R✝<GOAL>((f✝ + f'✝) ≫ g✝).f = (f✝ ≫ g✝ + f'✝ ≫ g✝).f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>T : Monad C<VAR>inst✝ : T.Additive<VAR>P✝ Q✝ R✝ : T.Algebra<VAR>f✝ : P✝ ⟶ Q✝<VAR>g✝ g'✝ : Q✝ ⟶ R✝<GOAL>(f✝ ≫ (g✝ + g'✝)).f = (f✝ ≫ g✝ + f✝ ≫ g'✝).f
<VAR>x y : ℝ<GOAL>ContinuousAt log x ↔ x ≠ 0
<VAR>x y : ℝ<GOAL>ContinuousAt log x → x ≠ 0
<VAR>y : ℝ<VAR>h : ContinuousAt log 0<GOAL>False
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp E 2 μ)<GOAL>eLpNorm (↑↑↑((condexpL2 E 𝕜 hm) f)) 2 μ ≤ eLpNorm (↑↑f) 2 μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp E 2 μ)<GOAL>‖(condexpL2 E 𝕜 hm) f‖ ≤ ‖f‖
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : C<VAR>f g : X ⟶ Y<VAR>h : Y ⟶ Z<VAR>inst✝ : IsIso f<GOAL>inv (inv f) = f
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : C<VAR>f g : X ⟶ Y<VAR>h : Y ⟶ Z<VAR>inst✝ : IsIso f<GOAL>inv f ≫ f = 𝟙 Y
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ inst✝ : CommSemiring R<VAR>p : MvPolynomial σ R<GOAL>p.totalDegree = 0 ↔ ∀ m ∈ p.support, ∀ (x : σ), m x = 0
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ inst✝ : CommSemiring R<VAR>p : MvPolynomial σ R<GOAL>NonTorsionWeight 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Monoid M<VAR>a b c : M<VAR>m✝ n m : ℕ<VAR>ha : a ^ n = 1<GOAL>a ^ m = a ^ (m % n)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>r : ℝ<VAR>hs : s.Nonempty<GOAL>infDist x s < r ↔ ∃ y ∈ s, dist x y < r
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : ConditionallyCompleteLinearOrder R<VAR>inst✝ : Fintype S<VAR>f : S → Tropical (WithTop R)<GOAL>untrop (∑ i : S, f i) = ⨅ i, untrop (f i)
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>inst✝¹ : Category.{u, v} C<VAR>A : C<VAR>inst✝ : HasTerminal C<VAR>y : ↑X<VAR>h : p₀ ⤳ y<VAR>U V : (OpenNhds y)ᵒᵖ<VAR>inc : U ⟶ V<GOAL>(if h : p₀ ∈ unop ((OpenNhds.inclusion y).op.obj V) then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from ((fun U => if p₀ ∈ unop U then A else ⊤_ C) ((OpenNhds.inclusion y).op.obj U))) ≫ (fun U => eqToHom ⋯) V = (fun U => eqToHom ⋯) U ≫ ((Functor.const (OpenNhds y)ᵒᵖ).obj A).map inc
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>inst✝¹ : Category.{u, v} C<VAR>A : C<VAR>inst✝ : HasTerminal C<VAR>y : ↑X<VAR>h : p₀ ⤳ y<VAR>U V : (OpenNhds y)ᵒᵖ<VAR>inc : U ⟶ V<GOAL>eqToHom ⋯ ≫ (fun U => eqToHom ⋯) V = (fun U => eqToHom ⋯) U ≫ ((Functor.const (OpenNhds y)ᵒᵖ).obj A).map inc
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>inst✝¹ : Category.{u, v} C<VAR>A : C<VAR>inst✝ : HasTerminal C<VAR>y : ↑X<VAR>h : p₀ ⤳ y<VAR>U V : (OpenNhds y)ᵒᵖ<VAR>inc : U ⟶ V<GOAL>p₀ ∈ unop ((OpenNhds.inclusion y).op.obj V)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝¹ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>inst✝ : TopologicalSpace α<VAR>f : α →ᵤ[𝔖] β<VAR>x : α<VAR>h𝔖 : ∃ V ∈ 𝔖, V ∈ 𝓝 x<VAR>hc : ContinuousAt ((toFun 𝔖) f) x<GOAL>ContinuousAt (fun fx => (toFun 𝔖) fx.1 fx.2) (f, x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝¹ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>inst✝ : TopologicalSpace α<VAR>f : α →ᵤ[𝔖] β<VAR>x : α<VAR>h𝔖 : ∃ V ∈ 𝔖, V ∈ 𝓝 x<VAR>hc : ContinuousAt ((toFun 𝔖) f) x<GOAL>∀ s ∈ 𝓤 β, ∀ᶠ (a : (α →ᵤ[𝔖] β) × α) in 𝓝 (f, x), (Prod.mk ((toFun 𝔖) (f, x).1 (f, x).2) ∘ fun fx => (toFun 𝔖) fx.1 fx.2) a ∈ s ○ s