ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>inst✝ : Countable ι<VAR>a : ι → ℂ<VAR>q : ι → ℝ<VAR>F : ℝ → ℂ<VAR>s : ℂ<VAR>hq : ∀ (i : ι), a i = 0 ∨ 0 < q i<VAR>hs : 0 < s.re<VAR>hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-π * q i * t))) (F t)<VAR>h_sum : Summable fun i => ‖a i‖ / q i ^ s.re<VAR>hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i<GOAL>Summable fun i => ‖a i‖ / (π * q i) ^ s.re
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<GOAL>diam univ = diam (range inl ∪ range inr)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<GOAL>diam (range inl) + dist (inl default) (inr default) + diam (range inr) = diam univ + (dist default default + 1 + dist default default) + diam univ
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<GOAL>diam univ + dist (inl default) (inr default) + diam univ = diam univ + (dist default default + 1 + dist default default) + diam univ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>hgi : ∫⁻ (x : α), g x ∂μ ≠ ⊤<VAR>hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ<GOAL>f =ᶠ[ae μ] g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>hgi : ∫⁻ (x : α), g x ∂μ ≠ ⊤<VAR>hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hs' : μ s < ⊤<GOAL>∫ (x : α) in s, (f x).toReal ∂μ = ∫ (x : α) in s, (g x).toReal ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>hgi : ∫⁻ (x : α), g x ∂μ ≠ ⊤<VAR>hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hs' : μ s < ⊤<GOAL>(∫⁻ (a : α) in s, ENNReal.ofReal (f a).toReal ∂μ).toReal = (∫⁻ (a : α) in s, ENNReal.ofReal (g a).toReal ∂μ).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>hgi : ∫⁻ (x : α), g x ∂μ ≠ ⊤<VAR>hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hs' : μ s < ⊤<GOAL>0 ≤ᶠ[ae (μ.restrict s)] fun x => (g x).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>hgi : ∫⁻ (x : α), g x ∂μ ≠ ⊤<VAR>hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hs' : μ s < ⊤<GOAL>AEStronglyMeasurable (fun x => (g x).toReal) (μ.restrict s)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>hgi : ∫⁻ (x : α), g x ∂μ ≠ ⊤<VAR>hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hs' : μ s < ⊤<GOAL>0 ≤ᶠ[ae (μ.restrict s)] fun x => (f x).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>hgi : ∫⁻ (x : α), g x ∂μ ≠ ⊤<VAR>hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hs' : μ s < ⊤<GOAL>AEStronglyMeasurable (fun x => (f x).toReal) (μ.restrict s)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>hp : p.natDegree ≠ 0<GOAL>(derivative p).natDegree < p.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>hp : p.natDegree ≠ 0<VAR>hp' : derivative p = 0<GOAL>(derivative p).natDegree < p.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>hp : p.natDegree ≠ 0<VAR>hp' : derivative p ≠ 0<GOAL>(derivative p).natDegree < p.natDegree
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝¹ : NonUnitalNonAssocSemiring α<VAR>inst✝ : Fintype n<VAR>A : Matrix m n α<VAR>x y : n → α<VAR>x✝ : m<GOAL>(A *ᵥ (x + y)) x✝ = (A *ᵥ x + A *ᵥ y) x✝
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : Finmap β<GOAL>a ∉ erase a s
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : Finmap β<GOAL>a = a ∨ a ∉ s
<VAR>n✝ b n : ℕ<VAR>hb : 1 < b<VAR>hn : n ≠ 0<GOAL>(b.digits n).length = log b n + 1
<VAR>n✝ b : ℕ<VAR>hb : 1 < b<VAR>n : ℕ<VAR>IH : ∀ m < n, m ≠ 0 → (b.digits m).length = log b m + 1<VAR>hn : n ≠ 0<GOAL>(b.digits n).length = log b n + 1
<VAR>n✝ b : ℕ<VAR>hb : 1 < b<VAR>n : ℕ<VAR>IH : ∀ m < n, m ≠ 0 → (b.digits m).length = log b m + 1<VAR>hn : n ≠ 0<GOAL>(b.digits (n / b)).length + 1 = log b n + 1
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>μ : Measure Ω<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : NormedAddCommGroup F<VAR>f : Ω → F<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>Integrable (fun ω => (((condexpKernel μ m) ω) s).toReal) μ
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>μ : Measure Ω<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : NormedAddCommGroup F<VAR>f : Ω → F<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>Integrable (fun ω => ((((condDistrib id id μ).comap id ⋯) ω) s).toReal) μ
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)<VAR>x : 𝕜<VAR>hx : x ∈ s<VAR>z : 𝕜<VAR>hz : z ∈ s<VAR>hxz : x < z<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>y : 𝕜 := a * x + b * z<GOAL>f (a • x + b • z) < a • f x + b • f z
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)<VAR>x : 𝕜<VAR>hx : x ∈ s<VAR>z : 𝕜<VAR>hz : z ∈ s<VAR>hxz : x < z<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>y : 𝕜 := a * x + b * z<VAR>hxy : x < y<GOAL>f (a • x + b • z) < a • f x + b • f z
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)<VAR>x : 𝕜<VAR>hx : x ∈ s<VAR>z : 𝕜<VAR>hz : z ∈ s<VAR>hxz : x < z<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>y : 𝕜 := a * x + b * z<VAR>hxy : x < y<VAR>hyz : y < z<GOAL>f (a • x + b • z) < a • f x + b • f z
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)<VAR>x : 𝕜<VAR>hx : x ∈ s<VAR>z : 𝕜<VAR>hz : z ∈ s<VAR>hxz : x < z<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>y : 𝕜 := a * x + b * z<VAR>hxy : x < y<VAR>hyz : y < z<VAR>this : (f y - f x) * (z - y) < (f z - f y) * (y - x)<GOAL>f (a • x + b • z) < a • f x + b • f z
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)<VAR>x : 𝕜<VAR>hx : x ∈ s<VAR>z : 𝕜<VAR>hz : z ∈ s<VAR>hxz✝ : x < z<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>y : 𝕜 := a * x + b * z<VAR>hxy : x < y<VAR>hyz : y < z<VAR>this : (f y - f x) * (z - y) < (f z - f y) * (y - x)<VAR>hxz : 0 < z - x<GOAL>f (a • x + b • z) < a • f x + b • f z
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)<VAR>x : 𝕜<VAR>hx : x ∈ s<VAR>z : 𝕜<VAR>hz : z ∈ s<VAR>hxz✝ : x < z<VAR>a b : 𝕜<VAR>ha✝ : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>y : 𝕜 := a * x + b * z<VAR>hxy : x < y<VAR>hyz : y < z<VAR>this : (f y - f x) * (z - y) < (f z - f y) * (y - x)<VAR>hxz : 0 < z - x<VAR>ha : (z - y) / (z - x) = a<GOAL>f (a • x + b • z) < a • f x + b • f z
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)<VAR>x : 𝕜<VAR>hx : x ∈ s<VAR>z : 𝕜<VAR>hz : z ∈ s<VAR>hxz✝ : x < z<VAR>a b : 𝕜<VAR>ha✝ : 0 < a<VAR>hb✝ : 0 < b<VAR>hab : a + b = 1<VAR>y : 𝕜 := a * x + b * z<VAR>hxy : x < y<VAR>hyz : y < z<VAR>this : (f y - f x) * (z - y) < (f z - f y) * (y - x)<VAR>hxz : 0 < z - x<VAR>ha : (z - y) / (z - x) = a<VAR>hb : (y - x) / (z - x) = b<GOAL>f (a • x + b • z) < a • f x + b • f z
<VAR>l : Type u_1<VAR>m✝ : Type u_2<VAR>n✝ : Type u_3<VAR>o : Type u_4<VAR>p✝ : Type u_5<VAR>q✝ : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝² : CommRing R<VAR>m : Type u_14<VAR>n : Type u_15<VAR>k : Type u_16<VAR>inst✝¹ : Fintype n<VAR>p : m → Prop<VAR>q : n → Prop<VAR>inst✝ : DecidablePred q<VAR>r : k → Prop<VAR>A : Matrix m n R<VAR>B : Matrix n k R<GOAL>(A * B).toBlock p r = A.toBlock p q * B.toBlock q r + (A.toBlock p fun i => ¬q i) * B.toBlock (fun i => ¬q i) r
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<GOAL>torsionBySet R M Set.univ = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<GOAL>torsionBySet R M Set.univ ≤ torsionBySet R M {1}
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>σ : Type u_1<VAR>inst✝⁴ : DecidableEq σ<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>s : σ<VAR>n : N<VAR>d : σ →₀ ℕ<GOAL>(scalarRTensor (X s ⊗ₜ[R] n)) d = if Finsupp.single s 1 = d then n else 0
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → DecidableEq (α i)<VAR>inst✝¹ : (i : ι) → PartialOrder (α i)<VAR>inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)<VAR>a : (i : ι) → α i<GOAL>(Ioi a).card = ∏ i : ι, (Ici (a i)).card - 1
<VAR>x y : ℤ[i]<GOAL>{ re := round (↑(x * star y).re * (↑(norm y))⁻¹), im := round (↑(x * star y).im * (↑(norm y))⁻¹) } = { re := round (↑(x * star y).re / ↑(norm y)), im := round (↑(x * star y).im / ↑(norm y)) }
<VAR>F : Type u_1<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>inst✝ : CompleteSpace F<GOAL>MeasurableSet {x | DifferentiableWithinAt ℝ f (Ioi x) x}
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 1 < x<VAR>hyz : y < z<GOAL>x ^ y < x ^ z
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 1 < x<VAR>hyz : y < z<GOAL>rexp (log x * y) < rexp (log x * z)
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 1 < x<VAR>hyz : y < z<GOAL>log x * y < log x * z
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_7<VAR>inst✝ : AddCommMonoid β<VAR>T T' : Set α → β<VAR>c : ℝ≥0∞<VAR>hc_ne_top : c ≠ ⊤<VAR>hT : FinMeasAdditive (c • μ) T<GOAL>FinMeasAdditive μ T
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_7<VAR>inst✝ : AddCommMonoid β<VAR>T T' : Set α → β<VAR>c : ℝ≥0∞<VAR>hc_ne_top : c ≠ ⊤<VAR>hT : FinMeasAdditive (c • μ) T<VAR>s : Set α<VAR>x✝ : MeasurableSet s<VAR>hμs : (c • μ) s = ⊤<GOAL>μ s = ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_7<VAR>inst✝ : AddCommMonoid β<VAR>T T' : Set α → β<VAR>c : ℝ≥0∞<VAR>hc_ne_top : c ≠ ⊤<VAR>hT : FinMeasAdditive (c • μ) T<VAR>s : Set α<VAR>x✝ : MeasurableSet s<VAR>hμs : c ≠ 0 ∧ μ s = ⊤ ∨ c = ⊤ ∧ μ s ≠ 0<GOAL>μ s = ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_7<VAR>inst✝ : AddCommMonoid β<VAR>T T' : Set α → β<VAR>c : ℝ≥0∞<VAR>hc_ne_top : c ≠ ⊤<VAR>hT : FinMeasAdditive (c • μ) T<VAR>s : Set α<VAR>x✝ : MeasurableSet s<VAR>hμs : ¬c = 0 ∧ μ s = ⊤<GOAL>μ s = ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Computation α<VAR>h✝ : s.Terminates<VAR>a : α<VAR>h : s.get = a<GOAL>s.get ∈ s
<VAR>e o₁ o₂ : ONote<VAR>n₁ n₂ : ℕ+<VAR>h₁ : (e.oadd n₁ o₁).NF<VAR>h : ↑n₁ < ↑n₂<GOAL>e.oadd n₁ o₁ < e.oadd n₂ o₂
<VAR>e o₁ o₂ : ONote<VAR>n₁ n₂ : ℕ+<VAR>h₁ : (e.oadd n₁ o₁).NF<VAR>h : ↑n₁ < ↑n₂<GOAL>ω ^ e.repr * ↑↑n₁ + o₁.repr < ω ^ e.repr * ↑↑n₂ + o₂.repr
<VAR>e o₁ o₂ : ONote<VAR>n₁ n₂ : ℕ+<VAR>h₁ : (e.oadd n₁ o₁).NF<VAR>h : ↑n₁ < ↑n₂<GOAL>ω ^ e.repr * ↑↑n₁ + ω ^ e.repr ≤ ω ^ e.repr * ↑↑n₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x✝ x y : α<VAR>xs : List α<VAR>h : (x :: y :: xs).Nodup<GOAL>(x :: y :: xs).formPerm x = y
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<GOAL>M ≅[L] N ↔ ∀ (φ : L.Sentence), M ⊨ φ ↔ N ⊨ φ
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : NoMinOrder α<VAR>inst✝ : ClosedIicTopology α<VAR>s : Set α<VAR>hs : s ∈ cocompact α<GOAL>s ∈ atBot
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : NoMinOrder α<VAR>inst✝ : ClosedIicTopology α<VAR>s : Set α<VAR>hs : s ∈ cocompact α<VAR>t : Set α<VAR>ht : IsCompact t<VAR>hts : tᶜ ⊆ s<GOAL>s ∈ atBot
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : NoMinOrder α<VAR>inst✝ : ClosedIicTopology α<VAR>s : Set α<VAR>hs : s ∈ cocompact α<VAR>t : Set α<VAR>ht : IsCompact t<VAR>hts : tᶜ ⊆ s<VAR>h_empty : t = ∅<GOAL>s ∈ atBot
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : NoMinOrder α<VAR>inst✝ : ClosedIicTopology α<VAR>s : Set α<VAR>hs : s ∈ cocompact α<VAR>t : Set α<VAR>ht : IsCompact t<VAR>hts : tᶜ ⊆ s<VAR>h_nonempty : t.Nonempty<GOAL>s ∈ atBot
<VAR>a x z : ℂ<GOAL>abs x = 1 ↔ ∃ θ ∈ Ioc (-π) π, cexp (↑θ * I) = x
<VAR>a x z : ℂ<GOAL>(∃ θ, cexp (↑θ * I) = x) ↔ ∃ θ ∈ Ioc (-π) π, cexp (↑θ * I) = x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K✝ : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁷ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝⁴ : FunLike F M M₂<VAR>inst✝³ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t : Set M<VAR>K : Type u_9<VAR>E : Type u_10<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module K E<VAR>s : Submodule K E<VAR>x : E<GOAL>Disjoint s (span K {x}) ↔ x ∈ s → x = 0
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K✝ : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁷ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝⁴ : FunLike F M M₂<VAR>inst✝³ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t : Set M<VAR>K : Type u_9<VAR>E : Type u_10<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module K E<VAR>s : Submodule K E<VAR>x : E<GOAL>(x ∈ s → x = 0) → ∀ x_1 ∈ s, x_1 ∈ span K {x} → x_1 = 0
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K✝ : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁷ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝⁴ : FunLike F M M₂<VAR>inst✝³ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t : Set M<VAR>K : Type u_9<VAR>E : Type u_10<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module K E<VAR>s : Submodule K E<VAR>x : E<VAR>H : x ∈ s → x = 0<VAR>y : E<VAR>hy : y ∈ s<VAR>hyx : y ∈ span K {x}<GOAL>y = 0
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K✝ : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁷ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝⁴ : FunLike F M M₂<VAR>inst✝³ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t : Set M<VAR>K : Type u_9<VAR>E : Type u_10<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module K E<VAR>s : Submodule K E<VAR>x : E<VAR>H : x ∈ s → x = 0<VAR>c : K<VAR>hy : c • x ∈ s<VAR>hyx : c • x ∈ span K {x}<GOAL>c • x = 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>x : R<VAR>hx : ∀ (y : R), f (x * y) = f x * f y<VAR>y : R<GOAL>Tendsto (seminormFromConst_seq c f (x * y)) atTop (𝓝 (seminormFromConst' hf1 hc hpm x * seminormFromConst' hf1 hc hpm y))
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>x : R<VAR>hx : ∀ (y : R), f (x * y) = f x * f y<VAR>y : R<GOAL>Tendsto (seminormFromConst_seq c f (x * y)) atTop (𝓝 (f x * seminormFromConst' hf1 hc hpm y))
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>x : R<VAR>hx : ∀ (y : R), f (x * y) = f x * f y<VAR>y : R<VAR>hseq : seminormFromConst_seq c f (x * y) = fun n => f x * seminormFromConst_seq c f y n<GOAL>Tendsto (seminormFromConst_seq c f (x * y)) atTop (𝓝 (f x * seminormFromConst' hf1 hc hpm y))
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>A : Set X<VAR>h : derivedSet A ⊆ A<GOAL>IsClosed A
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>A : Set X<VAR>h : derivedSet A ⊆ A<GOAL>∀ (a : X), ClusterPt a (𝓟 A) → a ∈ A
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>A : Set X<VAR>h : derivedSet A ⊆ A<VAR>a : X<VAR>ha : ClusterPt a (𝓟 A)<GOAL>a ∈ A
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>A : Set X<VAR>h : derivedSet A ⊆ A<VAR>a : X<VAR>ha : ClusterPt a (𝓟 A)<VAR>nh : a ∉ A<GOAL>False
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>A : Set X<VAR>h : derivedSet A ⊆ A<VAR>a : X<VAR>ha : ClusterPt a (𝓟 A)<VAR>nh : a ∉ A<VAR>this : A = A \ {a}<GOAL>False
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>A : Set X<VAR>h : derivedSet A ⊆ A<VAR>a : X<VAR>ha : AccPt a (𝓟 A)<VAR>nh : a ∉ A<VAR>this : A = A \ {a}<GOAL>False
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasBinaryBiproducts C<VAR>W X Y Z : C<VAR>f : W ⟶ Y<VAR>g : X ⟶ Z<VAR>inst✝ : IsIso (biprod.map f g)<GOAL>IsIso (biprod.map g f)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasBinaryBiproducts C<VAR>W X Y Z : C<VAR>f : W ⟶ Y<VAR>g : X ⟶ Z<VAR>inst✝ : IsIso (biprod.map f g)<GOAL>IsIso ((biprod.braiding X W).hom ≫ biprod.map f g ≫ (biprod.braiding Y Z).hom)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : Ring k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>inst✝ : Nontrivial k<VAR>p : ι → P<VAR>ha : AffineIndependent k p<VAR>i j : ι<VAR>hij : p i = p j<GOAL>i = j
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : Ring k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>inst✝ : Nontrivial k<VAR>p : ι → P<VAR>i j : ι<VAR>ha : LinearIndependent k fun i => p ↑i -ᵥ p j<VAR>hij : p i = p j<GOAL>i = j
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : Ring k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>inst✝ : Nontrivial k<VAR>p : ι → P<VAR>i j : ι<VAR>ha : LinearIndependent k fun i => p ↑i -ᵥ p j<VAR>hij : p i = p j<VAR>hij' : ¬i = j<GOAL>False
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : Ring k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>inst✝ : Nontrivial k<VAR>p : ι → P<VAR>i j : ι<VAR>ha : LinearIndependent k fun i => p ↑i -ᵥ p j<VAR>hij : p i = p j<VAR>hij' : ¬i = j<GOAL>p ↑⟨i, hij'⟩ = p j