ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s<VAR>u : ℕ → α<VAR>hu : Monotone u<VAR>us : ∀ (i : ℕ), u i ∈ s<VAR>n : ℕ<VAR>h : x < u n<VAR>exists_N : ∃ N ≤ n, x < u N<VAR>N : ℕ := Nat.find exists_N<VAR>hN : N ≤ n ∧ x < u N<GOAL>∃ v m, Monotone v ∧ (∀ (i : ℕ), v i ∈ s) ∧ x ∈ v '' Iio m ∧ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ ∑ j ∈ Finset.range m, edist (f (v (j + 1))) (f (v j))
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s<VAR>u : ℕ → α<VAR>hu : Monotone u<VAR>us : ∀ (i : ℕ), u i ∈ s<VAR>n : ℕ<VAR>h : x < u n<VAR>exists_N : ∃ N ≤ n, x < u N<VAR>N : ℕ := Nat.find exists_N<VAR>hN : N ≤ n ∧ x < u N<VAR>w : ℕ → α := fun i => if i < N then u i else if i = N then x else u (i - 1)<VAR>ws : ∀ (i : ℕ), w i ∈ s<VAR>hw : Monotone w<GOAL>∃ v m, Monotone v ∧ (∀ (i : ℕ), v i ∈ s) ∧ x ∈ v '' Iio m ∧ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ ∑ j ∈ Finset.range m, edist (f (v (j + 1))) (f (v j))
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s<VAR>u : ℕ → α<VAR>hu : Monotone u<VAR>us : ∀ (i : ℕ), u i ∈ s<VAR>n : ℕ<VAR>h : x < u n<VAR>exists_N : ∃ N ≤ n, x < u N<VAR>N : ℕ := Nat.find exists_N<VAR>hN : N ≤ n ∧ x < u N<VAR>w : ℕ → α := fun i => if i < N then u i else if i = N then x else u (i - 1)<VAR>ws : ∀ (i : ℕ), w i ∈ s<VAR>hw : Monotone w<GOAL>w N = x
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s<VAR>u : ℕ → α<VAR>hu : Monotone u<VAR>us : ∀ (i : ℕ), u i ∈ s<VAR>n : ℕ<VAR>h : x < u n<VAR>exists_N : ∃ N ≤ n, x < u N<VAR>N : ℕ := Nat.find exists_N<VAR>hN : N ≤ n ∧ x < u N<VAR>w : ℕ → α := fun i => if i < N then u i else if i = N then x else u (i - 1)<VAR>ws : ∀ (i : ℕ), w i ∈ s<VAR>hw : Monotone w<GOAL>∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ ∑ j ∈ Finset.range (n + 1), edist (f (w (j + 1))) (f (w j))
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s<VAR>u : ℕ → α<VAR>hu : Monotone u<VAR>us : ∀ (i : ℕ), u i ∈ s<VAR>n : ℕ<VAR>h : x < u n<VAR>exists_N : ∃ N ≤ n, x < u N<VAR>N : ℕ := Nat.find exists_N<VAR>hN : N ≤ n ∧ x < u N<VAR>w : ℕ → α := fun i => if i < N then u i else if i = N then x else u (i - 1)<VAR>ws : ∀ (i : ℕ), w i ∈ s<VAR>hw : Monotone w<VAR>Npos : 0 = N<GOAL>∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ ∑ j ∈ Finset.range (n + 1), edist (f (w (j + 1))) (f (w j))
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s<VAR>u : ℕ → α<VAR>hu : Monotone u<VAR>us : ∀ (i : ℕ), u i ∈ s<VAR>n : ℕ<VAR>h : x < u n<VAR>exists_N : ∃ N ≤ n, x < u N<VAR>N : ℕ := Nat.find exists_N<VAR>hN : N ≤ n ∧ x < u N<VAR>w : ℕ → α := fun i => if i < N then u i else if i = N then x else u (i - 1)<VAR>ws : ∀ (i : ℕ), w i ∈ s<VAR>hw : Monotone w<VAR>Npos : 0 < N<GOAL>∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ ∑ j ∈ Finset.range (n + 1), edist (f (w (j + 1))) (f (w j))
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalSpace B<VAR>inst✝⁵ : TopologicalSpace (TotalSpace F E)<VAR>e✝ : Trivialization F TotalSpace.proj<VAR>x : TotalSpace F E<VAR>b✝ : B<VAR>y✝ : E b✝<VAR>inst✝⁴ : AddCommMonoid F<VAR>inst✝³ : Module R F<VAR>inst✝² : (x : B) → AddCommMonoid (E x)<VAR>inst✝¹ : (x : B) → Module R (E x)<VAR>e : Trivialization F TotalSpace.proj<VAR>inst✝ : Trivialization.IsLinear R e<VAR>b : B<VAR>y : E b<GOAL>(Trivialization.linearMapAt R e b) y = if b ∈ e.baseSet then (↑e { proj := b, snd := y }).2 else 0
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>⟪x, y⟫_ℝ = ‖x‖ * ‖y‖ ↔ angle x y = 0
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h : ⟪x, y⟫_ℝ = ‖x‖ * ‖y‖<GOAL>angle x y = 0
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h : ⟪x, y⟫_ℝ = ‖x‖ * ‖y‖<VAR>h₁ : ‖x‖ * ‖y‖ ≠ 0<GOAL>angle x y = 0
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>X : C<GOAL>L.map (h.unit.app X) ≫ L.map (h.unit.app (R.obj (L.obj X))) = L.map (h.unit.app X) ≫ L.map (R.map (L.map (h.unit.app X)))
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>X✝ Y✝ : C<VAR>f : X✝ ⟶ Y✝<GOAL>L.map (h.unit.app X✝) ≫ L.map (R.map (L.map f)) = L.map f ≫ L.map (h.unit.app Y✝)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>X✝ Y✝ : C<VAR>f : X✝ ⟶ Y✝<GOAL>L.map (h.unit.app X✝ ≫ R.map (L.map f)) = L.map f ≫ L.map (h.unit.app Y✝)
<VAR>α : Type u<VAR>inst✝¹ : Ring α<VAR>inst✝ : Invertible 2<GOAL>2 * (1 - ⅟2) = 2 * ⅟2
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<GOAL>LiouvilleWith p (x + ↑m) ↔ LiouvilleWith p x
<VAR>f g : ℕ →. ℕ<VAR>hf : Partrec f<VAR>hg : Partrec g<GOAL>∃ h, Partrec h ∧ ∀ (a : ℕ), (∀ x ∈ h a, x ∈ f a ∨ x ∈ g a) ∧ ((h a).Dom ↔ (f a).Dom ∨ (g a).Dom)
<VAR>g : ℕ →. ℕ<VAR>hg : Partrec g<VAR>cf : Code<VAR>hf : Partrec cf.eval<GOAL>∃ h, Partrec h ∧ ∀ (a : ℕ), (∀ x ∈ h a, x ∈ cf.eval a ∨ x ∈ g a) ∧ ((h a).Dom ↔ (cf.eval a).Dom ∨ (g a).Dom)
<VAR>cf : Code<VAR>hf : Partrec cf.eval<VAR>cg : Code<VAR>hg : Partrec cg.eval<GOAL>∃ h, Partrec h ∧ ∀ (a : ℕ), (∀ x ∈ h a, x ∈ cf.eval a ∨ x ∈ cg.eval a) ∧ ((h a).Dom ↔ (cf.eval a).Dom ∨ (cg.eval a).Dom)
<VAR>cf : Code<VAR>hf : Partrec cf.eval<VAR>cg : Code<VAR>hg : Partrec cg.eval<VAR>this : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n<GOAL>∃ h, Partrec h ∧ ∀ (a : ℕ), (∀ x ∈ h a, x ∈ cf.eval a ∨ x ∈ cg.eval a) ∧ ((h a).Dom ↔ (cf.eval a).Dom ∨ (cg.eval a).Dom)
<VAR>cf : Code<VAR>hf : Partrec cf.eval<VAR>cg : Code<VAR>hg : Partrec cg.eval<VAR>this✝ : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n<VAR>n : ℕ<VAR>this : ∀ x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun _x => Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n<GOAL>(∀ x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n) ∧ ((rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n).Dom ↔ (cf.eval n).Dom ∨ (cg.eval n).Dom)
<VAR>cf : Code<VAR>hf : Partrec cf.eval<VAR>cg : Code<VAR>hg : Partrec cg.eval<VAR>this✝ : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n<VAR>n : ℕ<VAR>this : ∀ x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun _x => Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n<GOAL>(cf.eval n).Dom ∨ (cg.eval n).Dom → (rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n).Dom
<VAR>cf : Code<VAR>hf : Partrec cf.eval<VAR>cg : Code<VAR>hg : Partrec cg.eval<VAR>this✝ : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n<VAR>n : ℕ<VAR>this : ∀ x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun _x => Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n<VAR>h : (cf.eval n).Dom ∨ (cg.eval n).Dom<GOAL>(rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n).Dom
<VAR>cf : Code<VAR>hf : Partrec cf.eval<VAR>cg : Code<VAR>hg : Partrec cg.eval<VAR>this✝ : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n<VAR>n : ℕ<VAR>this : ∀ x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun _x => Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n<VAR>h : (cf.eval n).Dom ∨ (cg.eval n).Dom<GOAL>∃ n_1 a, a ∈ HOrElse.hOrElse (Code.evaln n_1 cf n) fun x => Code.evaln n_1 cg n
<VAR>cf : Code<VAR>hf : Partrec cf.eval<VAR>cg : Code<VAR>hg : Partrec cg.eval<VAR>this✝ : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n<VAR>n : ℕ<VAR>this : ∀ x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun _x => Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n<VAR>h : (∃ y k, Code.evaln k cf n = Option.some y) ∨ ∃ y k, Code.evaln k cg n = Option.some y<GOAL>∃ n_1 a, a ∈ HOrElse.hOrElse (Code.evaln n_1 cf n) fun x => Code.evaln n_1 cg n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → Seq1 β<VAR>g : β → Seq1 γ<VAR>a : α<VAR>s : Seq α<GOAL>(bind (a, s) f).bind g = bind (a, s) fun x => (f x).bind g
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → Seq1 β<VAR>g : β → Seq1 γ<VAR>a : α<VAR>s : Seq α<GOAL>(join (map g (f a), Seq.map (map g) (Seq.map f s))).join = join ((map g (f a)).join, Seq.map (fun x => (map g (f x)).join) s)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → Seq1 β<VAR>g : β → Seq1 γ<VAR>a : α<VAR>s : Seq α<GOAL>(join (map g (f a), Seq.map (map g ∘ f) s)).join = join ((map g (f a)).join, Seq.map (fun x => (map g (f x)).join) s)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → Seq1 β<VAR>g : β → Seq1 γ<VAR>a : α<VAR>s : Seq α<GOAL>(join (map g (f a), Seq.map (map g ∘ f) s)).join = join ((map g (f a)).join, Seq.map (join ∘ map g ∘ f) s)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → Seq1 β<VAR>g : β → Seq1 γ<VAR>a : α<VAR>s : Seq α<GOAL>(join (map g (f a), Seq.map (map g ∘ f) s)).join = join ((map g (f a)).join, Seq.map join (Seq.map (map g ∘ f) s))
<VAR>α : Type u_1<VAR>l : List α<GOAL>powersetAux l ~ powersetAux' l
<VAR>α : Type u_1<VAR>l : List α<GOAL>List.map ofList l.sublists ~ powersetAux' l
<VAR>α : Type u_1<VAR>inst✝¹ : Zero α<VAR>inst✝ : LinearOrder α<VAR>a : α<GOAL>sign a ≤ 0 ↔ a ≤ 0
<VAR>α : Type u_1<VAR>inst✝¹ : Zero α<VAR>inst✝ : LinearOrder α<VAR>a : α<VAR>h : 0 < a<GOAL>sign a ≤ 0 ↔ a ≤ 0
<VAR>α : Type u_1<VAR>inst✝¹ : Zero α<VAR>inst✝ : LinearOrder α<VAR>a : α<VAR>h : 0 = a<GOAL>sign a ≤ 0 ↔ a ≤ 0
<VAR>α : Type u_1<VAR>inst✝¹ : Zero α<VAR>inst✝ : LinearOrder α<VAR>a : α<VAR>h : a < 0<GOAL>sign a ≤ 0 ↔ a ≤ 0
<VAR>𝓕 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁✝ a₂✝ b b₁✝ b₂✝ : E<VAR>r r₁ r₂ : ℝ<VAR>a₁ a₂ b₁ b₂ : E<GOAL>dist (a₁ * a₂) (b₁ * b₂) ≤ dist a₁ b₁ + dist a₂ b₂
<GOAL>comap re (comap Real.exp (𝓝 0)) = comap re atBot
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : Measure Ω<VAR>μs : ι → Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)<VAR>E : Set Ω<VAR>E_mble : MeasurableSet E<VAR>h : limsup (fun i => (μs i) E) L ≤ μ E<GOAL>μ Eᶜ ≤ liminf (fun i => (μs i) Eᶜ) L
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>ι : Type u_2<VAR>μ : Measure Ω<VAR>μs : ι → Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)<VAR>E : Set Ω<VAR>E_mble : MeasurableSet E<VAR>h : limsup (fun i => (μs i) E) ⊥ ≤ μ E<GOAL>μ Eᶜ ≤ liminf (fun i => (μs i) Eᶜ) ⊥
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : Measure Ω<VAR>μs : ι → Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)<VAR>E : Set Ω<VAR>E_mble : MeasurableSet E<VAR>h : limsup (fun i => (μs i) E) L ≤ μ E<VAR>hne : L.NeBot<GOAL>μ Eᶜ ≤ liminf (fun i => (μs i) Eᶜ) L
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : Measure Ω<VAR>μs : ι → Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)<VAR>E : Set Ω<VAR>E_mble : MeasurableSet E<VAR>h : limsup (fun i => (μs i) E) L ≤ μ E<VAR>hne : L.NeBot<VAR>meas_Ec : μ Eᶜ = 1 - μ E<GOAL>μ Eᶜ ≤ liminf (fun i => (μs i) Eᶜ) L
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : Measure Ω<VAR>μs : ι → Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)<VAR>E : Set Ω<VAR>E_mble : MeasurableSet E<VAR>h : limsup (fun i => (μs i) E) L ≤ μ E<VAR>hne : L.NeBot<VAR>meas_Ec : μ Eᶜ = 1 - μ E<VAR>meas_i_Ec : ∀ (i : ι), (μs i) Eᶜ = 1 - (μs i) E<GOAL>μ Eᶜ ≤ liminf (fun i => (μs i) Eᶜ) L
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : Measure Ω<VAR>μs : ι → Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)<VAR>E : Set Ω<VAR>E_mble : MeasurableSet E<VAR>h : limsup (fun i => (μs i) E) L ≤ μ E<VAR>hne : L.NeBot<VAR>meas_Ec : μ Eᶜ = 1 - μ E<VAR>meas_i_Ec : ∀ (i : ι), (μs i) Eᶜ = 1 - (μs i) E<VAR>obs : liminf (fun i => 1 - (μs i) E) L = liminf ((fun x => 1 - x) ∘ fun i => (μs i) E) L<GOAL>1 - μ E ≤ liminf ((fun x => 1 - x) ∘ fun i => (μs i) E) L
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : Measure Ω<VAR>μs : ι → Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)<VAR>E : Set Ω<VAR>E_mble : MeasurableSet E<VAR>h : limsup (fun i => (μs i) E) L ≤ μ E<VAR>hne : L.NeBot<VAR>meas_Ec : μ Eᶜ = 1 - μ E<VAR>meas_i_Ec : ∀ (i : ι), (μs i) Eᶜ = 1 - (μs i) E<VAR>obs : liminf (fun i => 1 - (μs i) E) L = liminf ((fun x => 1 - x) ∘ fun i => (μs i) E) L<VAR>this : 1 - limsup (fun i => (μs i) E) L = liminf ((fun x => 1 - x) ∘ fun i => (μs i) E) L<GOAL>1 - μ E ≤ liminf ((fun x => 1 - x) ∘ fun i => (μs i) E) L
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : Measure Ω<VAR>μs : ι → Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)<VAR>E : Set Ω<VAR>E_mble : MeasurableSet E<VAR>h : limsup (fun i => (μs i) E) L ≤ μ E<VAR>hne : L.NeBot<VAR>meas_Ec : μ Eᶜ = 1 - μ E<VAR>meas_i_Ec : ∀ (i : ι), (μs i) Eᶜ = 1 - (μs i) E<VAR>obs : liminf (fun i => 1 - (μs i) E) L = liminf ((fun x => 1 - x) ∘ fun i => (μs i) E) L<VAR>this : 1 - limsup (fun i => (μs i) E) L = liminf ((fun x => 1 - x) ∘ fun i => (μs i) E) L<GOAL>1 - μ E ≤ 1 - limsup (fun i => (μs i) E) L
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>inst✝ : OmegaCompletePartialOrder α<VAR>c : Chain α<VAR>x : α<VAR>a✝ : ∀ (i : ℕ), c i ≤ x<GOAL>ωSup c ≤ x
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>P : α → Prop<VAR>a : α<VAR>h₁ : P 0<VAR>h₂ : ∀ (x : α), IsUnit x → P x<VAR>h₃ : ∀ (a p : α), a ≠ 0 → Prime p → P a → P (p * a)<GOAL>P a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>P : α → Prop<VAR>a : α<VAR>h₁ : P 0<VAR>h₂ : ∀ (x : α), IsUnit x → P x<VAR>h₃ : ∀ (a p : α), a ≠ 0 → Irreducible p → P a → P (p * a)<GOAL>P a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁵ : DecidableEq α<VAR>inst✝⁴ : DecidableEq β<VAR>inst✝³ : SemilatticeInf α<VAR>inst✝² : SemilatticeInf β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : InfHomClass F α β<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α<VAR>a b c : α<VAR>f : F<VAR>hf : Injective ⇑f<VAR>s t : Finset α<GOAL>map { toFun := ⇑f, inj' := hf } (s ⊼ t) = map { toFun := ⇑f, inj' := hf } s ⊼ map { toFun := ⇑f, inj' := hf } t
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : Module K V<VAR>inst✝⁴ : Field K₁<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K₁ V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>J : K →+* K<VAR>J₁ J₁' : K₁ →+* K<VAR>B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂<VAR>x : V₁<VAR>hx : ¬B.IsOrtho x x<GOAL>Submodule.span K₁ {x} ⊓ (Submodule.span K₁ {x}).orthogonalBilin B = ⊥
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : Module K V<VAR>inst✝⁴ : Field K₁<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K₁ V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>J : K →+* K<VAR>J₁ J₁' : K₁ →+* K<VAR>B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂<VAR>x : V₁<VAR>hx : ¬B.IsOrtho x x<GOAL>Submodule.span K₁ ↑{x} ⊓ (Submodule.span K₁ ↑{x}).orthogonalBilin B = ⊥
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : Module K V<VAR>inst✝⁴ : Field K₁<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K₁ V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>J : K →+* K<VAR>J₁ J₁' : K₁ →+* K<VAR>B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂<VAR>x : V₁<VAR>hx : ¬B.IsOrtho x x<VAR>y : V₁<VAR>h : y ∈ Submodule.span K₁ ↑{x} ⊓ (Submodule.span K₁ ↑{x}).orthogonalBilin B<GOAL>y ∈ ⊥
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : Module K V<VAR>inst✝⁴ : Field K₁<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K₁ V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>J : K →+* K<VAR>J₁ J₁' : K₁ →+* K<VAR>B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂<VAR>x : V₁<VAR>hx : ¬B.IsOrtho x x<VAR>μ : V₁ → K₁<VAR>h : ∑ i ∈ {x}, μ i • i ∈ Submodule.span K₁ ↑{x} ⊓ (Submodule.span K₁ ↑{x}).orthogonalBilin B<GOAL>∑ i ∈ {x}, μ i • i ∈ ⊥
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : Module K V<VAR>inst✝⁴ : Field K₁<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K₁ V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>J : K →+* K<VAR>J₁ J₁' : K₁ →+* K<VAR>B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂<VAR>x : V₁<VAR>hx : ¬B.IsOrtho x x<VAR>μ : V₁ → K₁<VAR>h : B.IsOrtho x (∑ i ∈ {x}, μ i • i)<GOAL>∑ i ∈ {x}, μ i • i ∈ ⊥
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : Module K V<VAR>inst✝⁴ : Field K₁<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K₁ V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>J : K →+* K<VAR>J₁ J₁' : K₁ →+* K<VAR>B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂<VAR>x : V₁<VAR>hx : ¬B.IsOrtho x x<VAR>μ : V₁ → K₁<VAR>h : B.IsOrtho x (μ x • x)<GOAL>μ x • x ∈ ⊥
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : Module K V<VAR>inst✝⁴ : Field K₁<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K₁ V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>J : K →+* K<VAR>J₁ J₁' : K₁ →+* K<VAR>B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂<VAR>x : V₁<VAR>hx : ¬B.IsOrtho x x<VAR>μ : V₁ → K₁<VAR>h : B.IsOrtho x (μ x • x)<GOAL>μ x = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : Module K V<VAR>inst✝⁴ : Field K₁<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K₁ V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>J : K →+* K<VAR>J₁ J₁' : K₁ →+* K<VAR>B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂<VAR>x : V₁<VAR>hx : ¬B.IsOrtho x x<VAR>μ : V₁ → K₁<VAR>h : J₁' (μ x) • (B x) x = 0<GOAL>μ x = 0
<VAR>X✝ : LocallyRingedSpace<VAR>r : ↑(Γ.obj (op X✝))<VAR>X : LocallyRingedSpace<VAR>s : Set ↑(X.presheaf.obj (op ⊤))<GOAL>⇑X.toΓSpec.val.base ⁻¹' zeroLocus s = ⋂ f ∈ s, (↑(X.toRingedSpace.basicOpen f))ᶜ
<VAR>X✝ : LocallyRingedSpace<VAR>r : ↑(Γ.obj (op X✝))<VAR>X : LocallyRingedSpace<VAR>s : Set ↑(X.presheaf.obj (op ⊤))<VAR>this : ∀ i ∈ s, (X.toRingedSpace.basicOpen i).carrierᶜ = ⇑X.toΓSpec.val.base ⁻¹' (basicOpen i).carrierᶜ<GOAL>⇑X.toΓSpec.val.base ⁻¹' zeroLocus s = ⋂ f ∈ s, (↑(X.toRingedSpace.basicOpen f))ᶜ
<VAR>X✝ : LocallyRingedSpace<VAR>r : ↑(Γ.obj (op X✝))<VAR>X : LocallyRingedSpace<VAR>s : Set ↑(X.presheaf.obj (op ⊤))<VAR>this : ∀ i ∈ s, (X.toRingedSpace.basicOpen i).carrierᶜ = ⇑X.toΓSpec.val.base ⁻¹' (basicOpen i).carrierᶜ<GOAL>⇑X.toΓSpec.val.base ⁻¹' zeroLocus s = ⋂ i ∈ s, ⇑X.toΓSpec.val.base ⁻¹' (basicOpen i).carrierᶜ
<VAR>X✝ : LocallyRingedSpace<VAR>r : ↑(Γ.obj (op X✝))<VAR>X : LocallyRingedSpace<VAR>s : Set ↑(X.presheaf.obj (op ⊤))<VAR>this : ∀ i ∈ s, (X.toRingedSpace.basicOpen i).carrierᶜ = ⇑X.toΓSpec.val.base ⁻¹' (basicOpen i).carrierᶜ<GOAL>⇑X.toΓSpec.val.base ⁻¹' zeroLocus s = ⇑X.toΓSpec.val.base ⁻¹' ⋂ i ∈ s, zeroLocus {i}
<VAR>X✝ : LocallyRingedSpace<VAR>r : ↑(Γ.obj (op X✝))<VAR>X : LocallyRingedSpace<VAR>s : Set ↑(X.presheaf.obj (op ⊤))<VAR>this : ∀ i ∈ s, (X.toRingedSpace.basicOpen i).carrierᶜ = ⇑X.toΓSpec.val.base ⁻¹' (basicOpen i).carrierᶜ<GOAL>⇑X.toΓSpec.val.base ⁻¹' zeroLocus s = ⇑X.toΓSpec.val.base ⁻¹' zeroLocus (⋃ i ∈ s, {i})
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x : M<VAR>b' : Basis ι' R M'<VAR>e : ι ≃ ι'<GOAL>range ⇑(b.reindex e) = range ⇑b
<VAR>α : Type u<VAR>β : Type v<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<GOAL>IsField R ↔ IsSimpleOrder (Ideal R)
<VAR>α : Type u<VAR>β : Type v<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>h✝ : Subsingleton R<GOAL>IsField R ↔ IsSimpleOrder (Ideal R)
<VAR>α : Type u<VAR>β : Type v<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>h✝ : Nontrivial R<GOAL>IsField R ↔ IsSimpleOrder (Ideal R)
<VAR>α : Type u<VAR>β : Type v<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>h✝ : Nontrivial R<GOAL>(¬∃ I, ⊥ < I ∧ I < ⊤) ↔ ¬¬IsSimpleOrder (Ideal R)
<VAR>α : Type u<VAR>β : Type v<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>h✝ : Nontrivial R<GOAL>(∀ (I : Ideal R), ⊥ < I → ¬I < ⊤) ↔ IsSimpleOrder (Ideal R)
<VAR>α : Type u<VAR>β : Type v<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>h✝ : Nontrivial R<GOAL>(∀ (I : Ideal R), I = ⊥ ∨ I = ⊤) ↔ IsSimpleOrder (Ideal R)