ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>x : EReal<VAR>h : x < 0<GOAL>⊥ * x = ⊤
<VAR>x : EReal<VAR>h : x < 0<GOAL>x * ⊥ = ⊤
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α γ : TypeVec.{u} n<VAR>g : α ⟹ γ<VAR>a : P.A<VAR>f' : P.drop.B a ⟹ α<VAR>f : P.last.B a → P.W α<GOAL>(g ::: P.wMap g) <$$> P.objAppend1 a f' f = P.objAppend1 a (g ⊚ f') fun x => P.wMap g (f x)
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α γ : TypeVec.{u} n<VAR>g : α ⟹ γ<VAR>a : P.A<VAR>f' : P.drop.B a ⟹ α<VAR>f : P.last.B a → P.W α<GOAL>⟨a, splitFun (g ⊚ f') (P.wMap g ∘ f)⟩ = ⟨a, splitFun (g ⊚ f') fun x => P.wMap g (f x)⟩
<VAR>C : Type u_1<VAR>inst✝¹⁰ : Category.{u_6, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝⁹ : Category.{u_5, u_2} A<VAR>inst✝⁸ : HasWeakSheafify J A<VAR>inst✝⁷ : (constantSheaf J A).Faithful<VAR>inst✝⁶ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>D : Type u_3<VAR>inst✝⁵ : Category.{u_4, u_3} D<VAR>K : GrothendieckTopology D<VAR>inst✝⁴ : HasWeakSheafify K A<VAR>G : C ⥤ D<VAR>inst✝³ : ∀ (X : Dᵒᵖ), HasLimitsOfShape (StructuredArrow X G.op) A<VAR>inst✝² : IsDenseSubsite J K G<VAR>ht' : IsTerminal (G.obj t)<VAR>inst✝¹ : (constantSheaf J A).Faithful<VAR>inst✝ : (constantSheaf J A).Full<VAR>F : Sheaf K A<VAR>e : Sheaf J A ≌ Sheaf K A := sheafEquiv G J K A<GOAL>IsDiscrete J ht (e.inverse.obj F) ↔ IsDiscrete K ht' F
<VAR>C : Type u_1<VAR>inst✝¹⁰ : Category.{u_6, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝⁹ : Category.{u_5, u_2} A<VAR>inst✝⁸ : HasWeakSheafify J A<VAR>inst✝⁷ : (constantSheaf J A).Faithful<VAR>inst✝⁶ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>D : Type u_3<VAR>inst✝⁵ : Category.{u_4, u_3} D<VAR>K : GrothendieckTopology D<VAR>inst✝⁴ : HasWeakSheafify K A<VAR>G : C ⥤ D<VAR>inst✝³ : ∀ (X : Dᵒᵖ), HasLimitsOfShape (StructuredArrow X G.op) A<VAR>inst✝² : IsDenseSubsite J K G<VAR>ht' : IsTerminal (G.obj t)<VAR>inst✝¹ : (constantSheaf J A).Faithful<VAR>inst✝ : (constantSheaf J A).Full<VAR>F : Sheaf K A<VAR>e : Sheaf J A ≌ Sheaf K A := sheafEquiv G J K A<VAR>this : (constantSheaf K A).Faithful<GOAL>IsDiscrete J ht (e.inverse.obj F) ↔ IsDiscrete K ht' F
<VAR>C : Type u_1<VAR>inst✝¹⁰ : Category.{u_6, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝⁹ : Category.{u_5, u_2} A<VAR>inst✝⁸ : HasWeakSheafify J A<VAR>inst✝⁷ : (constantSheaf J A).Faithful<VAR>inst✝⁶ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>D : Type u_3<VAR>inst✝⁵ : Category.{u_4, u_3} D<VAR>K : GrothendieckTopology D<VAR>inst✝⁴ : HasWeakSheafify K A<VAR>G : C ⥤ D<VAR>inst✝³ : ∀ (X : Dᵒᵖ), HasLimitsOfShape (StructuredArrow X G.op) A<VAR>inst✝² : IsDenseSubsite J K G<VAR>ht' : IsTerminal (G.obj t)<VAR>inst✝¹ : (constantSheaf J A).Faithful<VAR>inst✝ : (constantSheaf J A).Full<VAR>F : Sheaf K A<VAR>e : Sheaf J A ≌ Sheaf K A := sheafEquiv G J K A<VAR>this✝ : (constantSheaf K A).Faithful<VAR>this : (constantSheaf K A).Full<GOAL>IsDiscrete J ht (e.inverse.obj F) ↔ IsDiscrete K ht' F
<VAR>C : Type u_1<VAR>inst✝¹⁰ : Category.{u_6, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝⁹ : Category.{u_5, u_2} A<VAR>inst✝⁸ : HasWeakSheafify J A<VAR>inst✝⁷ : (constantSheaf J A).Faithful<VAR>inst✝⁶ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>D : Type u_3<VAR>inst✝⁵ : Category.{u_4, u_3} D<VAR>K : GrothendieckTopology D<VAR>inst✝⁴ : HasWeakSheafify K A<VAR>G : C ⥤ D<VAR>inst✝³ : ∀ (X : Dᵒᵖ), HasLimitsOfShape (StructuredArrow X G.op) A<VAR>inst✝² : IsDenseSubsite J K G<VAR>ht' : IsTerminal (G.obj t)<VAR>inst✝¹ : (constantSheaf J A).Faithful<VAR>inst✝ : (constantSheaf J A).Full<VAR>F : Sheaf K A<VAR>e : Sheaf J A ≌ Sheaf K A := sheafEquiv G J K A<VAR>this✝ : (constantSheaf K A).Faithful<VAR>this : (constantSheaf K A).Full<GOAL>e.inverse.obj F ∈ (constantSheaf J A).essImage ↔ F ∈ (constantSheaf K A).essImage
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f f₁ : E → F<VAR>f' f₀' f₁' : F<VAR>s t : Set E<VAR>x v : E<GOAL>HasLineDerivAt 𝕜 f f' x v ↔ Tendsto (fun t => t⁻¹ • (f (x + t • v) - f x)) (𝓝[≠] 0) (𝓝 f')
<VAR>y : ℝ<VAR>hy : 0 < y<GOAL>Tendsto (fun x => x ^ y) (𝓝 ⊤) (𝓝 ⊤)
<VAR>y : ℝ<VAR>hy : 0 < y<GOAL>∀ (x : ℝ≥0), ∀ᶠ (a : ℝ≥0∞) in 𝓝 ⊤, ↑x < a ^ y
<VAR>y : ℝ<VAR>hy : 0 < y<VAR>x : ℝ≥0<GOAL>∀ᶠ (a : ℝ≥0∞) in 𝓝 ⊤, ↑x < a ^ y
<VAR>y : ℝ<VAR>hy : 0 < y<VAR>x c : ℝ≥0<VAR>left✝ : True<VAR>hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x<GOAL>∀ᶠ (a : ℝ≥0∞) in 𝓝 ⊤, ↑x < a ^ y
<VAR>y : ℝ<VAR>hy : 0 < y<VAR>x c : ℝ≥0<VAR>left✝ : True<VAR>hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x<VAR>hc' : Set.Ioi ↑c ∈ 𝓝 ⊤<GOAL>∀ᶠ (a : ℝ≥0∞) in 𝓝 ⊤, ↑x < a ^ y
<VAR>y : ℝ<VAR>hy : 0 < y<VAR>x c : ℝ≥0<VAR>left✝ : True<VAR>hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x<VAR>hc' : Set.Ioi ↑c ∈ 𝓝 ⊤<VAR>a : ℝ≥0∞<VAR>ha : a ∈ Set.Ioi ↑c<GOAL>↑x < a ^ y
<VAR>y : ℝ<VAR>hy : 0 < y<VAR>x c : ℝ≥0<VAR>left✝ : True<VAR>hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x<VAR>hc' : Set.Ioi ↑c ∈ 𝓝 ⊤<VAR>a : ℝ≥0<VAR>ha : ↑a ∈ Set.Ioi ↑c<GOAL>↑x < ↑a ^ y
<VAR>y : ℝ<VAR>hy : 0 < y<VAR>x c : ℝ≥0<VAR>left✝ : True<VAR>hc' : Set.Ioi ↑c ∈ 𝓝 ⊤<VAR>a : ℝ≥0<VAR>ha : c < a<VAR>hc : ∀ (x_1 : ℝ≥0), c < x_1 → x < x_1 ^ y<GOAL>↑x < ↑a ^ y
<VAR>y : ℝ<VAR>hy : 0 < y<VAR>x c : ℝ≥0<VAR>left✝ : True<VAR>hc' : Set.Ioi ↑c ∈ 𝓝 ⊤<VAR>a : ℝ≥0<VAR>ha : c < a<VAR>hc : ∀ (x_1 : ℝ≥0), c < x_1 → x < x_1 ^ y<GOAL>↑x < ↑(a ^ y)
<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<GOAL>G.edgeSet.Nonempty ↔ G ≠ ⊥
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Field K<VAR>inst✝ : Fintype K<VAR>i : ℕ<VAR>h : i < q - 1<VAR>hi : ¬i = 0<GOAL>∑ x : K, x ^ i = 0
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : MulOneClass M<VAR>ι : Sort u_4<VAR>hι : Nonempty ι<VAR>S : ι → Submonoid M<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : M<GOAL>x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : MulOneClass M<VAR>ι : Sort u_4<VAR>hι : Nonempty ι<VAR>S : ι → Submonoid M<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : M<GOAL>x ∈ ⨆ i, S i → ∃ i, x ∈ S i
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : MulOneClass M<VAR>ι : Sort u_4<VAR>hι : Nonempty ι<VAR>S : ι → Submonoid M<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : M<GOAL>x ∈ closure (⋃ i, ↑(S i)) → ∃ i, x ∈ S i
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : MulOneClass M<VAR>ι : Sort u_4<VAR>hι : Nonempty ι<VAR>S : ι → Submonoid M<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : M<VAR>hx : x ∈ closure (⋃ i, ↑(S i))<GOAL>∃ i, 1 ∈ S i
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : MulOneClass M<VAR>ι : Sort u_4<VAR>hι : Nonempty ι<VAR>S : ι → Submonoid M<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : M<VAR>hx : x ∈ closure (⋃ i, ↑(S i))<GOAL>∀ (x y : M), (∃ i, x ∈ S i) → (∃ i, y ∈ S i) → ∃ i, x * y ∈ S i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>s : Multiset α<GOAL>(∀ r ∈ 0, Prime r) → p ∣ Multiset.prod 0 → ∃ q ∈ 0, p ~ᵤ q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>s✝ : Multiset α<VAR>a : α<VAR>s : Multiset α<VAR>ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q<VAR>hs : ∀ r ∈ a ::ₘ s, Prime r<VAR>hps : p ∣ (a ::ₘ s).prod<GOAL>∃ q ∈ a ::ₘ s, p ~ᵤ q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>s✝ : Multiset α<VAR>a : α<VAR>s : Multiset α<VAR>ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q<VAR>hs : ∀ r ∈ a ::ₘ s, Prime r<VAR>hps : p ∣ a * s.prod<GOAL>∃ q ∈ a ::ₘ s, p ~ᵤ q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>s✝ : Multiset α<VAR>a : α<VAR>s : Multiset α<VAR>ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q<VAR>hs : ∀ r ∈ a ::ₘ s, Prime r<VAR>hps : p ∣ a * s.prod<VAR>h : p ∣ a<GOAL>∃ q ∈ a ::ₘ s, p ~ᵤ q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>s✝ : Multiset α<VAR>a : α<VAR>s : Multiset α<VAR>ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q<VAR>hs : ∀ r ∈ a ::ₘ s, Prime r<VAR>hps : p ∣ a * s.prod<VAR>h : p ∣ s.prod<GOAL>∃ q ∈ a ::ₘ s, p ~ᵤ q
<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>N : Type u_5<VAR>inst✝ : Group N<VAR>H : Subgroup N<VAR>hH : H.Normal<VAR>f : G →* N<VAR>x✝ : G<GOAL>x✝ ∈ Subgroup.comap f H → ∀ (g : G), g * x✝ * g⁻¹ ∈ Subgroup.comap f H
<VAR>a x : ℝ<GOAL>↑(sinKernel (↑a) x) = jacobiTheta₂' (↑a) (I * ↑x) / (-2 * ↑π)
<VAR>a x : ℝ<GOAL>(jacobiTheta₂' (↑a) (I * ↑x) / (-2 * ↑π) + jacobiTheta₂' ((starRingEnd ℂ) ↑a) (-(starRingEnd ℂ) (I * ↑x)) / (starRingEnd ℂ) (-2 * ↑π)) / 2 = jacobiTheta₂' (↑a) (I * ↑x) / (-2 * ↑π)
<VAR>ι✝ : Type u_1<VAR>κ✝ : Type u_2<VAR>α✝ : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α✝<VAR>a : α✝<VAR>f✝ g : α✝ → β<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>inst✝³ : Fintype ι<VAR>inst✝² : Fintype κ<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>f : (j : ι) → j = i → α<GOAL>(∏ j : ι, if h : j = i then f j h else 1) = f i ⋯
<VAR>J : Type w<VAR>C : Type uC<VAR>inst✝⁴ : Category.{uC', uC} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>F : J → C<VAR>G : C ⥤ D<VAR>inst✝ : G.PreservesZeroMorphisms<VAR>A : Bicone F<VAR>i j : J<GOAL>G.map (A.ι i ≫ A.π j) = if h : i = j then eqToHom ⋯ else 0
<VAR>J : Type w<VAR>C : Type uC<VAR>inst✝⁴ : Category.{uC', uC} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>F : J → C<VAR>G : C ⥤ D<VAR>inst✝ : G.PreservesZeroMorphisms<VAR>A : Bicone F<VAR>i j : J<GOAL>G.map (if h : i = j then eqToHom ⋯ else 0) = if h : i = j then eqToHom ⋯ else 0
<VAR>J : Type w<VAR>C : Type uC<VAR>inst✝⁴ : Category.{uC', uC} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>F : J → C<VAR>G : C ⥤ D<VAR>inst✝ : G.PreservesZeroMorphisms<VAR>X✝ Y✝ : Bicone F<VAR>f : X✝ ⟶ Y✝<VAR>j : J<GOAL>G.map f.hom ≫ ((fun A => { pt := G.obj A.pt, π := fun j => G.map (A.π j), ι := fun j => G.map (A.ι j), ι_π := ⋯ }) Y✝).π j = ((fun A => { pt := G.obj A.pt, π := fun j => G.map (A.π j), ι := fun j => G.map (A.ι j), ι_π := ⋯ }) X✝).π j
<VAR>J : Type w<VAR>C : Type uC<VAR>inst✝⁴ : Category.{uC', uC} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>F : J → C<VAR>G : C ⥤ D<VAR>inst✝ : G.PreservesZeroMorphisms<VAR>X✝ Y✝ : Bicone F<VAR>f : X✝ ⟶ Y✝<VAR>j : J<GOAL>((fun A => { pt := G.obj A.pt, π := fun j => G.map (A.π j), ι := fun j => G.map (A.ι j), ι_π := ⋯ }) X✝).ι j ≫ G.map f.hom = ((fun A => { pt := G.obj A.pt, π := fun j => G.map (A.π j), ι := fun j => G.map (A.ι j), ι_π := ⋯ }) Y✝).ι j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>hs : autoParam s.Finite _auto✝<GOAL>s.ncard ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b
<VAR>α : Type u_1<VAR>inst✝ : Semigroup α<VAR>s : Set α<VAR>a b : α<GOAL>op b • a • s = a • op b • s
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>l : List α<GOAL>map Prod.snd l.revzip = l.reverse
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : NormedLinearOrderedField 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : StrictConvexSpace ℝ E<VAR>x y z : E<VAR>a b r : ℝ<VAR>hx : x ∈ closedBall z r<VAR>hy : y ∈ closedBall z r<VAR>hne : x ≠ y<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>a • x + b • y ∈ ball z r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : NormedLinearOrderedField 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : StrictConvexSpace ℝ E<VAR>x y z : E<VAR>a b : ℝ<VAR>hne : x ≠ y<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>hx : x ∈ closedBall z 0<VAR>hy : y ∈ closedBall z 0<GOAL>a • x + b • y ∈ ball z 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : NormedLinearOrderedField 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : StrictConvexSpace ℝ E<VAR>x y z : E<VAR>a b r : ℝ<VAR>hx : x ∈ closedBall z r<VAR>hy : y ∈ closedBall z r<VAR>hne : x ≠ y<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>hr : r ≠ 0<GOAL>a • x + b • y ∈ ball z r
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : StrictOrderedCommRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<GOAL>s.SOppSide x y ↔ s.SOppSide y x
<VAR>α : Sort u_1<VAR>σ : α → Sort u_2<VAR>P Q R : Prop<VAR>inst✝¹ : Decidable P<VAR>inst✝ : Decidable Q<VAR>a b c : α<VAR>A : P → α<VAR>B : ¬P → α<GOAL>(∃ h, a ≠ b) ↔ P ∧ a ≠ b
<VAR>a b c : EReal<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>c * (a + b) = c * a + c * b
<VAR>a b c : EReal<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>(a + b) * c = c * a + c * b
<VAR>a b c : EReal<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>(a + b) * c = a * c + c * b
<VAR>a b c : EReal<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>(a + b) * c = a * c + b * c
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : Zero α<VAR>inst✝¹ : Zero β<VAR>inst✝ : SMulWithZero α β<VAR>s✝ : Set α<VAR>t s : Set β<VAR>h : s.Nonempty<GOAL>0 • s = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ : List α<VAR>a✝ : α<VAR>inst✝¹ : DecidableEq α<VAR>P : α → Prop<VAR>inst✝ : DecidablePred P<VAR>l : List α<VAR>a : α<GOAL>count a l = count a (filter (fun b => decide (P b)) l) + count a (filter (fun x => decide ¬P x) l)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ : List α<VAR>a✝ : α<VAR>inst✝¹ : DecidableEq α<VAR>P : α → Prop<VAR>inst✝ : DecidablePred P<VAR>l : List α<VAR>a x✝ : α<GOAL>(decide ¬P x✝) = !decide (P x✝)
<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>s : Set α<GOAL>supported R R s = span R ((fun i => single i 1) '' s)
<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>s : Set α<GOAL>(fun i => single i 1) '' s ⊆ ↑(supported R R s)
<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>s : Set α<VAR>l : α →₀ R<VAR>hl : l ∈ supported R R s<GOAL>l ∈ span R ((fun i => single i 1) '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<GOAL>totalVariation 0 = 0
<VAR>a b : ℕ<GOAL>(range ⇑castOrderEmbedding).OrdConnected
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>x : α × β<VAR>r : ℝ<GOAL>sphere x r = sphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>x : α × β<VAR>r : ℝ<VAR>hr : r < 0<GOAL>sphere x r = sphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>x : α × β<GOAL>sphere x 0 = sphere x.1 0 ×ˢ closedBall x.2 0 ∪ closedBall x.1 0 ×ˢ sphere x.2 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>x : α × β<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>sphere x r = sphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>h✝ h : α ≃ᵢ β<VAR>x : α<VAR>r : ℝ<GOAL>⇑h '' Metric.ball x r = Metric.ball (h x) r
<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>ι' : Type x'<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>inst✝⁴ : Module R M₃<VAR>φ : ι → Type i<VAR>inst✝³ : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝² : (i : ι) → Module R (φ i)<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>f : (ι → R) →ₗ[R] M₂<VAR>x : ι → R<GOAL>f x = ∑ i : ι, x i • f fun j => if i = j then 1 else 0
<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>ι' : Type x'<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>inst✝⁴ : Module R M₃<VAR>φ : ι → Type i<VAR>inst✝³ : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝² : (i : ι) → Module R (φ i)<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>f : (ι → R) →ₗ[R] M₂<VAR>x : ι → R<GOAL>∑ x_1 : ι, f (x x_1 • fun j => if x_1 = j then 1 else 0) = ∑ i : ι, x i • f fun j => if i = j then 1 else 0
<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>ι' : Type x'<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>inst✝⁴ : Module R M₃<VAR>φ : ι → Type i<VAR>inst✝³ : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝² : (i : ι) → Module R (φ i)<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>f : (ι → R) →ₗ[R] M₂<VAR>x : ι → R<VAR>x✝¹ : ι<VAR>x✝ : x✝¹ ∈ Finset.univ<GOAL>f (x x✝¹ • fun j => if x✝¹ = j then 1 else 0) = x x✝¹ • f fun j => if x✝¹ = j then 1 else 0
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>p n : ℕ<VAR>inst✝ : ExpChar R p<VAR>f : R[X]<VAR>r : R<GOAL>rootMultiplicity r ((expand R p) f) = p * rootMultiplicity (r ^ p) f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K✝ : ℝ≥0<VAR>f : α → β<VAR>x✝ y✝ : α<VAR>r : ℝ≥0∞<VAR>b : β<VAR>K : ℝ≥0<VAR>x y : α<GOAL>edist ((fun x => b) x) ((fun x => b) y) ≤ ↑K * edist x y
<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✝ : DecidablePred fun x => x ≠ 0<VAR>f : α →ₛ F<VAR>s : Finset F<VAR>hs : filter (fun x => x ≠ 0) f.range ⊆ s<GOAL>integral μ f = ∑ x ∈ s, (μ (↑f ⁻¹' {x})).toReal • 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✝⁵ : 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✝ : DecidablePred fun x => x ≠ 0<VAR>f : α →ₛ F<VAR>s : Finset F<VAR>hs : filter (fun x => x ≠ 0) f.range ⊆ s<GOAL>∀ x ∈ s, x ∉ filter (fun x => x ≠ 0) f.range → (μ (↑f ⁻¹' {x})).toReal • x = 0
<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✝ : DecidablePred fun x => x ≠ 0<VAR>f : α →ₛ F<VAR>s : Finset F<VAR>hs : filter (fun x => x ≠ 0) f.range ⊆ s<VAR>x : F<VAR>hx : x ∉ filter (fun x => x ≠ 0) f.range<GOAL>(μ (↑f ⁻¹' {x})).toReal • x = 0
<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✝ : DecidablePred fun x => x ≠ 0<VAR>f : α →ₛ F<VAR>s : Finset F<VAR>hs : filter (fun x => x ≠ 0) f.range ⊆ s<VAR>x : F<VAR>hx : x ∉ f.range ∨ x = 0<GOAL>(μ (↑f ⁻¹' {x})).toReal • x = 0
<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✝ : DecidablePred fun x => x ≠ 0<VAR>f : α →ₛ F<VAR>s : Finset F<VAR>hs : filter (fun x => x ≠ 0) f.range ⊆ s<VAR>hx : 0 ∉ f.range ∨ 0 = 0<GOAL>(μ (↑f ⁻¹' {0})).toReal • 0 = 0
<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✝ : DecidablePred fun x => x ≠ 0<VAR>f : α →ₛ F<VAR>s : Finset F<VAR>hs : filter (fun x => x ≠ 0) f.range ⊆ s<VAR>x : F<VAR>hx✝ : x ∉ f.range ∨ x = 0<VAR>hx : x ∉ f.range<GOAL>(μ (↑f ⁻¹' {x})).toReal • x = 0
<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✝ : DecidablePred fun x => x ≠ 0<VAR>f : α →ₛ F<VAR>s : Finset F<VAR>hs : filter (fun x => x ≠ 0) f.range ⊆ s<VAR>x : F<VAR>hx✝ : x ∉ f.range ∨ x = 0<VAR>hx : x ∉ Set.range ↑f<GOAL>(μ (↑f ⁻¹' {x})).toReal • x = 0
<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✝ : DecidablePred fun x => x ≠ 0<VAR>f : α →ₛ F<VAR>s : Finset F<VAR>hs : filter (fun x => x ≠ 0) f.range ⊆ s<VAR>x : F<VAR>hx✝ : x ∉ f.range ∨ x = 0<VAR>hx : ∀ (x_1 : α), ¬↑f x_1 = x<GOAL>(μ (↑f ⁻¹' {x})).toReal • x = 0
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup F<VAR>f : α → ℝ<VAR>hf : AEStronglyMeasurable f μ<GOAL>Memℒp f 2 μ ↔ Integrable (fun x => f x ^ 2) μ
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup F<VAR>f : α → ℝ<VAR>hf : AEStronglyMeasurable f μ<VAR>x✝ : α<GOAL>f x✝ ^ 2 = ‖f x✝‖ ^ 2
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>x : K<VAR>hx : IsIntegral A x<VAR>I : FractionalIdeal A⁰ K := adjoinIntegral A⁰ x hx<VAR>hI : IsUnit I<GOAL>I = 1