ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : BorelSpace β<VAR>h : μ.InnerRegularCompactLTTop<VAR>f : α → β<VAR>hf : Continuous f<GOAL>∀ (U : Set β), MeasurableSet U ∧ (map f μ) U ≠ ⊤ → MeasurableSet U
<VAR>J : Type w<VAR>K : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>f : J → C<VAR>g : K → C<VAR>e : J ≃ K<VAR>w : (j : J) → g (e j) ≅ f j<VAR>inst✝¹ : HasBiproduct f<VAR>inst✝ : HasBiproduct g<GOAL>(whiskerEquiv e w).inv = lift fun j => π g (e j) ≫ (w j).hom
<VAR>J : Type w<VAR>K : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>f : J → C<VAR>g : K → C<VAR>e : J ≃ K<VAR>w : (j : J) → g (e j) ≅ f j<VAR>inst✝¹ : HasBiproduct f<VAR>inst✝ : HasBiproduct g<GOAL>(desc fun k => eqToHom ⋯ ≫ (w (e.symm k)).hom ≫ ι f (e.symm k)) = lift fun j => π g (e j) ≫ (w j).hom
<VAR>ι : Type u_1<VAR>inst✝ : DecidableEq ι<VAR>α : ι → Type u_2<VAR>S : (i : ι) → Setoid (α i)<VAR>i : ι<VAR>l : List ι<VAR>f : (i_1 : ι) → i_1 ∈ i :: l → α i_1<GOAL>(finChoiceAux (i :: l) fun i_1 h => ⟦f i_1 h⟧) = ⟦f⟧
<VAR>ι : Type u_1<VAR>inst✝ : DecidableEq ι<VAR>α : ι → Type u_2<VAR>S : (i : ι) → Setoid (α i)<VAR>i : ι<VAR>l : List ι<VAR>f : (i_1 : ι) → i_1 ∈ i :: l → α i_1<GOAL>⟦fun j h => if h : j = i then cast ⋯ (f i ⋯) else f j ⋯⟧ = ⟦f⟧
<VAR>ι : Type u_1<VAR>inst✝ : DecidableEq ι<VAR>α : ι → Type u_2<VAR>S : (i : ι) → Setoid (α i)<VAR>i : ι<VAR>l : List ι<VAR>f : (i_1 : ι) → i_1 ∈ i :: l → α i_1<VAR>j : ι<VAR>h : j ∈ i :: l<GOAL>(if h : j = i then cast ⋯ (f i ⋯) else f j ⋯) ≈ f j h
<VAR>ι : Type u_1<VAR>inst✝ : DecidableEq ι<VAR>α : ι → Type u_2<VAR>S : (i : ι) → Setoid (α i)<VAR>i : ι<VAR>l : List ι<VAR>f : (i_1 : ι) → i_1 ∈ i :: l → α i_1<VAR>j : ι<VAR>h : j ∈ i :: l<VAR>e : j = i<GOAL>cast ⋯ (f i ⋯) ≈ f j h
<VAR>ι : Type u_1<VAR>inst✝ : DecidableEq ι<VAR>α : ι → Type u_2<VAR>S : (i : ι) → Setoid (α i)<VAR>i : ι<VAR>l : List ι<VAR>f : (i_1 : ι) → i_1 ∈ i :: l → α i_1<VAR>h : i ∈ i :: l<GOAL>cast ⋯ (f i ⋯) ≈ f i h
<VAR>b : ℝ<VAR>hb : 0 < b<VAR>s : ℝ<GOAL>(fun x => x ^ s * rexp (-b * x ^ 2)) =o[atTop] fun x => rexp (-(1 / 2) * x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Lattice α<VAR>inst✝¹ : Group α<VAR>a : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<GOAL>a⁻ᵐ = 1 ↔ 1 ≤ a
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : NormedLinearOrderedField K<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace K E<VAR>b : Basis ι K E<VAR>inst✝¹ : FloorRing K<VAR>inst✝ : Fintype ι<VAR>m : E<VAR>h : m ∈ span ℤ (Set.range ⇑b)<GOAL>∀ (i : ι), (b.repr ↑(ceil b m)) i = (b.repr m) i
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : NormedLinearOrderedField K<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace K E<VAR>b : Basis ι K E<VAR>inst✝¹ : FloorRing K<VAR>inst✝ : Fintype ι<VAR>m : E<VAR>h : m ∈ span ℤ (Set.range ⇑b)<GOAL>∀ (i : ι), ↑⌈(b.repr m) i⌉ = (b.repr m) i
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : NormedLinearOrderedField K<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace K E<VAR>b : Basis ι K E<VAR>inst✝¹ : FloorRing K<VAR>inst✝ : Fintype ι<VAR>m : E<VAR>h : m ∈ span ℤ (Set.range ⇑b)<VAR>i : ι<GOAL>↑⌈(b.repr m) i⌉ = (b.repr m) i
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : NormedLinearOrderedField K<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace K E<VAR>b : Basis ι K E<VAR>inst✝¹ : FloorRing K<VAR>inst✝ : Fintype ι<VAR>m : E<VAR>h : m ∈ span ℤ (Set.range ⇑b)<VAR>i : ι<VAR>z : ℤ<VAR>hz : (algebraMap ℤ K) z = (b.repr m) i<GOAL>↑⌈(b.repr m) i⌉ = (b.repr m) i
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : NormedLinearOrderedField K<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace K E<VAR>b : Basis ι K E<VAR>inst✝¹ : FloorRing K<VAR>inst✝ : Fintype ι<VAR>m : E<VAR>h : m ∈ span ℤ (Set.range ⇑b)<VAR>i : ι<VAR>z : ℤ<VAR>hz : (algebraMap ℤ K) z = (b.repr m) i<GOAL>↑⌈(algebraMap ℤ K) z⌉ = (algebraMap ℤ K) z
<VAR>s t : Set ℝ<GOAL>closure (s ×ℂ t) = closure s ×ℂ closure t
<VAR>m n : ℕ∞<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>s : Set H<VAR>hs : IsOpen s<GOAL>PartialHomeomorph.ofSet s hs ∈ contDiffGroupoid n I
<VAR>m n : ℕ∞<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>s : Set H<VAR>hs : IsOpen s<GOAL>(contDiffPregroupoid n I).property (↑(PartialHomeomorph.ofSet s hs)) (PartialHomeomorph.ofSet s hs).source ∧ (contDiffPregroupoid n I).property (↑(PartialHomeomorph.ofSet s hs).symm) (PartialHomeomorph.ofSet s hs).target
<VAR>m n : ℕ∞<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>s : Set H<VAR>hs : IsOpen s<GOAL>ContDiffOn 𝕜 n (↑I ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I)
<VAR>m n : ℕ∞<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>s : Set H<VAR>hs : IsOpen s<VAR>this : ContDiffOn 𝕜 n id univ<GOAL>ContDiffOn 𝕜 n (↑I ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I)
<VAR>G : Type u<VAR>inst✝² : LeftCancelMonoid G<VAR>inst✝¹ : Finite G<VAR>inst✝ : Nontrivial G<GOAL>1 < exponent G
<VAR>G : Type u<VAR>inst✝² : LeftCancelMonoid G<VAR>inst✝¹ : Finite G<VAR>inst✝ : Nontrivial G<GOAL>exponent G ≠ 0 ∧ exponent G ≠ 1
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝² : TopologicalSpace H<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>e e' : PartialHomeomorph M H<VAR>h : e' ≈ e<VAR>he : e ∈ maximalAtlas M G<VAR>e'' : PartialHomeomorph M H<VAR>he'' : e'' ∈ atlas H M<GOAL>e'.symm ≫ₕ e'' ∈ G ∧ e''.symm ≫ₕ e' ∈ G
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝² : TopologicalSpace H<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>e e' : PartialHomeomorph M H<VAR>h : e' ≈ e<VAR>he : e ∈ maximalAtlas M G<VAR>e'' : PartialHomeomorph M H<VAR>he'' : e'' ∈ atlas H M<VAR>l : e.symm ≫ₕ e'' ∈ G<VAR>r : e''.symm ≫ₕ e ∈ G<GOAL>e'.symm ≫ₕ e'' ∈ G ∧ e''.symm ≫ₕ e' ∈ G
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>β : Type u<VAR>inst✝ : Nonempty β<VAR>p : TauPackage β α<VAR>i : Ordinal.{u}<VAR>hi : i < p.lastStep<VAR>N : ℕ<VAR>hN : IsEmpty (SatelliteConfig α N p.τ)<GOAL>p.color i < N
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>β : Type u<VAR>inst✝ : Nonempty β<VAR>p : TauPackage β α<VAR>N : ℕ<VAR>hN : IsEmpty (SatelliteConfig α N p.τ)<VAR>i : Ordinal.{u}<VAR>IH : ∀ k < i, k < p.lastStep → p.color k < N<VAR>hi : i < p.lastStep<GOAL>p.color i < N
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>β : Type u<VAR>inst✝ : Nonempty β<VAR>p : TauPackage β α<VAR>N : ℕ<VAR>hN : IsEmpty (SatelliteConfig α N p.τ)<VAR>i : Ordinal.{u}<VAR>IH : ∀ k < i, k < p.lastStep → p.color k < N<VAR>hi : i < p.lastStep<VAR>A : Set ℕ := ⋃ j, ⋃ (_ : (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty), {p.color ↑j}<VAR>color_i : p.color i = sInf (univ \ A)<GOAL>sInf (univ \ A) < N
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>β : Type u<VAR>inst✝ : Nonempty β<VAR>p : TauPackage β α<VAR>N : ℕ<VAR>hN : IsEmpty (SatelliteConfig α N p.τ)<VAR>i : Ordinal.{u}<VAR>IH : ∀ k < i, k < p.lastStep → p.color k < N<VAR>hi : i < p.lastStep<VAR>A : Set ℕ := ⋃ j, ⋃ (_ : (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty), {p.color ↑j}<VAR>color_i : p.color i = sInf (univ \ A)<VAR>N_mem : N ∈ univ \ A<GOAL>sInf (univ \ A) < N
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>β : Type u<VAR>inst✝ : Nonempty β<VAR>p : TauPackage β α<VAR>N : ℕ<VAR>hN : IsEmpty (SatelliteConfig α N p.τ)<VAR>i : Ordinal.{u}<VAR>IH : ∀ k < i, k < p.lastStep → p.color k < N<VAR>hi : i < p.lastStep<VAR>A : Set ℕ := ⋃ j, ⋃ (_ : (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty), {p.color ↑j}<VAR>color_i : p.color i = sInf (univ \ A)<VAR>N_mem : N ∈ univ \ A<VAR>Inf_eq_N : sInf (univ \ A) = N<GOAL>False
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>β : Type u<VAR>inst✝ : Nonempty β<VAR>p : TauPackage β α<VAR>N : ℕ<VAR>hN : IsEmpty (SatelliteConfig α N p.τ)<VAR>i : Ordinal.{u}<VAR>IH : ∀ k < i, k < p.lastStep → p.color k < N<VAR>hi : i < p.lastStep<VAR>A : Set ℕ := ⋃ j, ⋃ (_ : (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty), {p.color ↑j}<VAR>color_i : p.color i = sInf (univ \ A)<VAR>N_mem : N ∈ univ \ A<VAR>Inf_eq_N : sInf (univ \ A) = N<VAR>this : ∀ k < N, ∃ j < i, (closedBall (p.c (p.index j)) (p.r (p.index j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧ k = p.color j<GOAL>False
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>β : Type u<VAR>inst✝ : Nonempty β<VAR>p : TauPackage β α<VAR>N : ℕ<VAR>hN : IsEmpty (SatelliteConfig α N p.τ)<VAR>i : Ordinal.{u}<VAR>IH : ∀ k < i, k < p.lastStep → p.color k < N<VAR>hi : i < p.lastStep<VAR>A : Set ℕ := ⋃ j, ⋃ (_ : (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty), {p.color ↑j}<VAR>color_i : p.color i = sInf (univ \ A)<VAR>N_mem : N ∈ univ \ A<VAR>Inf_eq_N : sInf (univ \ A) = N<VAR>g : ℕ → Ordinal.{u}<VAR>hg : ∀ k < N, g k < i ∧ (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧ k = p.color (g k)<VAR>G : ℕ → Ordinal.{u} := fun n => if n = N then i else g n<VAR>color_G : ∀ n ≤ N, p.color (G n) = n<VAR>G_lt_last : ∀ n ≤ N, G n < p.lastStep<GOAL>False
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>β : Type u<VAR>inst✝ : Nonempty β<VAR>p : TauPackage β α<VAR>N : ℕ<VAR>hN : IsEmpty (SatelliteConfig α N p.τ)<VAR>i : Ordinal.{u}<VAR>IH : ∀ k < i, k < p.lastStep → p.color k < N<VAR>hi : i < p.lastStep<VAR>A : Set ℕ := ⋃ j, ⋃ (_ : (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty), {p.color ↑j}<VAR>color_i : p.color i = sInf (univ \ A)<VAR>N_mem : N ∈ univ \ A<VAR>Inf_eq_N : sInf (univ \ A) = N<VAR>g : ℕ → Ordinal.{u}<VAR>hg : ∀ k < N, g k < i ∧ (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧ k = p.color (g k)<VAR>G : ℕ → Ordinal.{u} := fun n => if n = N then i else g n<VAR>color_G : ∀ n ≤ N, p.color (G n) = n<VAR>G_lt_last : ∀ n ≤ N, G n < p.lastStep<VAR>fGn : ∀ n ≤ N, p.c (p.index (G n)) ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r (p.index (G n))<GOAL>False
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>β : Type u<VAR>inst✝ : Nonempty β<VAR>p : TauPackage β α<VAR>N : ℕ<VAR>hN : IsEmpty (SatelliteConfig α N p.τ)<VAR>i : Ordinal.{u}<VAR>IH : ∀ k < i, k < p.lastStep → p.color k < N<VAR>hi : i < p.lastStep<VAR>A : Set ℕ := ⋃ j, ⋃ (_ : (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty), {p.color ↑j}<VAR>color_i : p.color i = sInf (univ \ A)<VAR>N_mem : N ∈ univ \ A<VAR>Inf_eq_N : sInf (univ \ A) = N<VAR>g : ℕ → Ordinal.{u}<VAR>hg : ∀ k < N, g k < i ∧ (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧ k = p.color (g k)<VAR>G : ℕ → Ordinal.{u} := fun n => if n = N then i else g n<VAR>color_G : ∀ n ≤ N, p.color (G n) = n<VAR>G_lt_last : ∀ n ≤ N, G n < p.lastStep<VAR>fGn : ∀ n ≤ N, p.c (p.index (G n)) ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r (p.index (G n))<VAR>Gab : ∀ (a b : Fin N.succ), G ↑a < G ↑b → p.r (p.index (G ↑a)) ≤ dist (p.c (p.index (G ↑a))) (p.c (p.index (G ↑b))) ∧ p.r (p.index (G ↑b)) ≤ p.τ * p.r (p.index (G ↑a))<VAR>sc : SatelliteConfig α N p.τ := { c := fun k => p.c (p.index (G ↑k)), r := fun k => p.r (p.index (G ↑k)), rpos := ⋯, h := ⋯, hlast := ⋯, inter := ⋯ }<GOAL>False
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>a : R<GOAL>(addVal R) a = ⊤ ↔ a = 0
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>a : R<VAR>hi : Irreducible (Classical.choose ⋯)<GOAL>(addVal R) a = ⊤ ↔ a = 0
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ<VAR>hf : ∀ i ∈ s, 0 ≤ f i<GOAL>ENNReal.ofReal (∑ i ∈ s, f i) = ∑ i ∈ s, ENNReal.ofReal (f i)
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ<VAR>hf : ∀ i ∈ s, 0 ≤ f i<GOAL>(∑ i ∈ s, f i).toNNReal = ∑ a ∈ s, (f a).toNNReal
<VAR>X : Scheme<VAR>P : ↑X.affineOpens → Prop<VAR>ι : Sort u_2<VAR>U : ι → ↑X.affineOpens<VAR>iSup_U : ⨆ i, ↑(U i) = ⊤<VAR>V : ↑X.affineOpens<VAR>basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)<VAR>openCover : ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)), Ideal.span ↑s = ⊤ → (∀ (f : { x // x ∈ s }), P (X.affineBasicOpen ↑f)) → P U<VAR>hU : ∀ (i : ι), P (U i)<GOAL>P V
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>σ : α → Type u_4<VAR>a✝ : α<VAR>s : Multiset α<VAR>t : (a : α) → Multiset (σ a)<VAR>a : α<VAR>b : σ a<GOAL>⟨a, b⟩ ∈ s.sigma t ↔ ⟨a, b⟩.fst ∈ s ∧ ⟨a, b⟩.snd ∈ t ⟨a, b⟩.fst
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : TopologicalGroup G<VAR>inst✝³ : TopologicalSpace α<VAR>f : α → G<VAR>s : Set α<VAR>x : α<VAR>inst✝² : TopologicalSpace H<VAR>inst✝¹ : OrderedCommGroup H<VAR>inst✝ : ContinuousInv H<VAR>a : H<GOAL>Tendsto Inv.inv (𝓝[≤] a⁻¹) (𝓝[≥] a)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<GOAL>∡ (midpoint ℝ p₂ p₁) p₂ p₃ = ∡ p₁ p₂ p₃
<VAR>ι : Sort u_1<VAR>f g : ι → ℝ≥0∞<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>s : Set ℝ≥0∞<VAR>hs : ∀ r ∈ s, r ≠ ⊤<VAR>hf : ∀ (i : { x // x ∈ s }), ↑i ≠ ⊤<GOAL>(sInf s).toNNReal = sInf (ENNReal.toNNReal '' s)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>b : HilbertBasis ι 𝕜 E<VAR>x : E<GOAL>HasSum (fun i => ↑(b.repr x) i • (fun i => b.repr.symm (lp.single 2 i 1)) i) x
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J X Y : Set α<VAR>N : Matroid α<VAR>h : N ≤r M<GOAL>N = M ∨ N <r M
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>m n : ℕ<GOAL>Even (m + n) ↔ (Odd m ↔ Odd n)
<VAR>k : Type u<VAR>inst✝⁴ : Field k<VAR>K : Type v<VAR>inst✝³ : Field K<VAR>inst✝² : IsSepClosed k<VAR>inst✝¹ : Algebra k K<VAR>L : IntermediateField k K<VAR>inst✝ : Algebra.IsSeparable k ↥L<VAR>x : K<VAR>hx : x ∈ L<GOAL>x ∈ ⊥
<VAR>k : Type u<VAR>inst✝⁴ : Field k<VAR>K : Type v<VAR>inst✝³ : Field K<VAR>inst✝² : IsSepClosed k<VAR>inst✝¹ : Algebra k K<VAR>L : IntermediateField k K<VAR>inst✝ : Algebra.IsSeparable k ↥L<VAR>x : K<VAR>hx : x ∈ L<VAR>y : k<VAR>hy : (algebraMap k ↥L) y = ⟨x, hx⟩<GOAL>x ∈ ⊥
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝¹ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>inst✝ : CompleteSpace F<VAR>h : Integrable I l f vol<VAR>π₀ : Prepartition I<GOAL>Tendsto (integralSum f vol) (l.toFilteriUnion I π₀) (𝓝 (∑ J ∈ π₀.boxes, integral J l f vol))
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝¹ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε✝ ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>inst✝ : CompleteSpace F<VAR>h : Integrable I l f vol<VAR>π₀ : Prepartition I<VAR>ε : ℝ<VAR>ε0 : 0 < ε<GOAL>∃ ia, (∀ (c : ℝ≥0), l.RCond (ia c)) ∧ ∀ x ∈ {π | ∃ c, l.MemBaseSet I c (ia c) π ∧ π.iUnion = π₀.iUnion}, integralSum f vol x ∈ closedBall (∑ J ∈ π₀.boxes, integral J l f vol) ε
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝¹ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε✝ ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>inst✝ : CompleteSpace F<VAR>h : Integrable I l f vol<VAR>π₀ : Prepartition I<VAR>ε : ℝ<VAR>ε0 : 0 < ε<GOAL>∀ x ∈ {π | ∃ c, l.MemBaseSet I c (h.convergenceR ε c) π ∧ π.iUnion = π₀.iUnion}, integralSum f vol x ∈ closedBall (∑ J ∈ π₀.boxes, integral J l f vol) ε
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝¹ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε✝ ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>inst✝ : CompleteSpace F<VAR>h : Integrable I l f vol<VAR>π₀ : Prepartition I<VAR>ε : ℝ<VAR>ε0 : 0 < ε<GOAL>∀ (x : TaggedPrepartition I), (∃ c, l.MemBaseSet I c (h.convergenceR ε c) x ∧ x.iUnion = π₀.iUnion) → integralSum f vol x ∈ closedBall (∑ J ∈ π₀.boxes, integral J l f vol) ε
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π✝ : TaggedPrepartition I<VAR>inst✝¹ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c✝ c₁ c₂ : ℝ≥0<VAR>ε✝ ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>inst✝ : CompleteSpace F<VAR>h : Integrable I l f vol<VAR>π₀ : Prepartition I<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>π : TaggedPrepartition I<VAR>c : ℝ≥0<VAR>hc : l.MemBaseSet I c (h.convergenceR ε c) π<VAR>hU : π.iUnion = π₀.iUnion<GOAL>integralSum f vol π ∈ closedBall (∑ J ∈ π₀.boxes, integral J l f vol) ε
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f : ι → E<VAR>h : ¬AffineIndependent 𝕜 f<GOAL>∃ I, ((convexHull 𝕜) (f '' I) ∩ (convexHull 𝕜) (f '' Iᶜ)).Nonempty
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f : ι → E<VAR>h : ¬∀ (s : Finset ι) (w : ι → 𝕜), s.sum w = 0 → ∑ e ∈ s, w e • f e = 0 → ∀ e ∈ s, w e = 0<GOAL>∃ I, ((convexHull 𝕜) (f '' I) ∩ (convexHull 𝕜) (f '' Iᶜ)).Nonempty
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f : ι → E<VAR>s : Finset ι<VAR>w : ι → 𝕜<VAR>h_wsum : s.sum w = 0<VAR>h_vsum : ∑ e ∈ s, w e • f e = 0<VAR>nonzero_w_index : ι<VAR>h1 : nonzero_w_index ∈ s<VAR>h2 : w nonzero_w_index ≠ 0<VAR>I : Finset ι := filter (fun i => 0 ≤ w i) s<VAR>J : Finset ι := filter (fun i => w i < 0) s<VAR>p : E := I.centerMass w f<GOAL>∃ I, ((convexHull 𝕜) (f '' I) ∩ (convexHull 𝕜) (f '' Iᶜ)).Nonempty
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f : ι → E<VAR>s : Finset ι<VAR>w : ι → 𝕜<VAR>h_wsum : s.sum w = 0<VAR>h_vsum : ∑ e ∈ s, w e • f e = 0<VAR>nonzero_w_index : ι<VAR>h1 : nonzero_w_index ∈ s<VAR>h2 : w nonzero_w_index ≠ 0<VAR>I : Finset ι := filter (fun i => 0 ≤ w i) s<VAR>J : Finset ι := filter (fun i => w i < 0) s<VAR>p : E := I.centerMass w f<VAR>hJI : ∑ j ∈ J, w j + ∑ i ∈ I, w i = 0<GOAL>∃ I, ((convexHull 𝕜) (f '' I) ∩ (convexHull 𝕜) (f '' Iᶜ)).Nonempty
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f : ι → E<VAR>s : Finset ι<VAR>w : ι → 𝕜<VAR>h_wsum : s.sum w = 0<VAR>h_vsum : ∑ e ∈ s, w e • f e = 0<VAR>nonzero_w_index : ι<VAR>h1 : nonzero_w_index ∈ s<VAR>h2 : w nonzero_w_index ≠ 0<VAR>I : Finset ι := filter (fun i => 0 ≤ w i) s<VAR>J : Finset ι := filter (fun i => w i < 0) s<VAR>p : E := I.centerMass w f<VAR>hJI : ∑ j ∈ J, w j + ∑ i ∈ I, w i = 0<VAR>hI : 0 < ∑ i ∈ I, w i<GOAL>∃ I, ((convexHull 𝕜) (f '' I) ∩ (convexHull 𝕜) (f '' Iᶜ)).Nonempty
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f : ι → E<VAR>s : Finset ι<VAR>w : ι → 𝕜<VAR>h_wsum : s.sum w = 0<VAR>h_vsum : ∑ e ∈ s, w e • f e = 0<VAR>nonzero_w_index : ι<VAR>h1 : nonzero_w_index ∈ s<VAR>h2 : w nonzero_w_index ≠ 0<VAR>I : Finset ι := filter (fun i => 0 ≤ w i) s<VAR>J : Finset ι := filter (fun i => w i < 0) s<VAR>p : E := I.centerMass w f<VAR>hJI : ∑ j ∈ J, w j + ∑ i ∈ I, w i = 0<VAR>hI : 0 < ∑ i ∈ I, w i<VAR>hp : J.centerMass w f = p<GOAL>∃ I, ((convexHull 𝕜) (f '' I) ∩ (convexHull 𝕜) (f '' Iᶜ)).Nonempty
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f : ι → E<VAR>s : Finset ι<VAR>w : ι → 𝕜<VAR>h_wsum : s.sum w = 0<VAR>h_vsum : ∑ e ∈ s, w e • f e = 0<VAR>nonzero_w_index : ι<VAR>h1 : nonzero_w_index ∈ s<VAR>h2 : w nonzero_w_index ≠ 0<VAR>I : Finset ι := filter (fun i => 0 ≤ w i) s<VAR>J : Finset ι := filter (fun i => w i < 0) s<VAR>p : E := I.centerMass w f<VAR>hJI : ∑ j ∈ J, w j + ∑ i ∈ I, w i = 0<VAR>hI : 0 < ∑ i ∈ I, w i<VAR>hp : J.centerMass w f = p<GOAL>J.centerMass w f ∈ (convexHull 𝕜) (f '' (↑I)ᶜ)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f : ι → E<VAR>s : Finset ι<VAR>w : ι → 𝕜<VAR>h_wsum : s.sum w = 0<VAR>h_vsum : ∑ e ∈ s, w e • f e = 0<VAR>nonzero_w_index : ι<VAR>h1 : nonzero_w_index ∈ s<VAR>h2 : w nonzero_w_index ≠ 0<VAR>I : Finset ι := filter (fun i => 0 ≤ w i) s<VAR>J : Finset ι := filter (fun i => w i < 0) s<VAR>p : E := I.centerMass w f<VAR>hJI : ∑ j ∈ J, w j + ∑ i ∈ I, w i = 0<VAR>hI : 0 < ∑ i ∈ I, w i<VAR>hp : J.centerMass w f = p<GOAL>∑ i ∈ J, w i < 0
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f : ι → E<VAR>s : Finset ι<VAR>w : ι → 𝕜<VAR>h_wsum : s.sum w = 0<VAR>h_vsum : ∑ e ∈ s, w e • f e = 0<VAR>nonzero_w_index : ι<VAR>h1 : nonzero_w_index ∈ s<VAR>h2 : w nonzero_w_index ≠ 0<VAR>I : Finset ι := filter (fun i => 0 ≤ w i) s<VAR>J : Finset ι := filter (fun i => w i < 0) s<VAR>p : E := I.centerMass w f<VAR>hJI : ∑ j ∈ J, w j + ∑ i ∈ I, w i = 0<VAR>hI : 0 < ∑ i ∈ I, w i<VAR>hp : J.centerMass w f = p<VAR>_i : ι<VAR>hi : _i ∈ J<VAR>hi' : _i ∈ ↑I<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁵ : CompleteLattice β<VAR>γ : Type u_3<VAR>mγ : MeasurableSpace γ<VAR>f : α → γ<VAR>g : γ → β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : SecondCountableTopology β<VAR>inst✝¹ : OrderClosedTopology β<VAR>inst✝ : OpensMeasurableSpace β<VAR>hg : Measurable g<VAR>hf : AEMeasurable f μ<GOAL>essSup g (Measure.map f μ) = essSup (g ∘ f) μ