ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>c_pos : 0 < c<VAR>hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ<VAR>A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)<VAR>Y : ℕ → Ω → ℝ := fun n => truncation (X n) ↑n<VAR>S : ℕ → Ω → ℝ := fun n => ∑ i ∈ range n, Y i<VAR>hS : S = fun n => ∑ i ∈ range n, Y i<VAR>u : ℕ → ℕ := fun n => ⌊c ^ n⌋₊<VAR>u_mono : Monotone u<VAR>I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * variance (Y j) ℙ ≤ 2 * ∫ (a : Ω), X 0 a<VAR>C : ℝ := c ^ 5 * (c - 1)⁻¹ ^ 3 * (2 * ∫ (a : Ω), X 0 a)<VAR>I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * variance (S (u i)) ℙ ≤ C<VAR>I3 : ∀ (N : ℕ), ∑ i ∈ range N, ℙ {ω | ↑(u i) * ε ≤ |S (u i) ω - ∫ (a : Ω), S (u i) a|} ≤ ENNReal.ofReal (ε⁻¹ ^ 2 * C)<VAR>I4 : ∑' (i : ℕ), ℙ {ω | ↑(u i) * ε ≤ |S (u i) ω - ∫ (a : Ω), S (u i) a|} < ⊤<GOAL>∀ᵐ (ω : Ω), ∀ᶠ (n : ℕ) in atTop, |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (range ⌊c ^ n⌋₊).sum Y a| < ε * ↑⌊c ^ n⌋₊
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>c_pos : 0 < c<VAR>hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ<VAR>A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)<VAR>Y : ℕ → Ω → ℝ := fun n => truncation (X n) ↑n<VAR>S : ℕ → Ω → ℝ := fun n => ∑ i ∈ range n, Y i<VAR>hS : S = fun n => ∑ i ∈ range n, Y i<VAR>u : ℕ → ℕ := fun n => ⌊c ^ n⌋₊<VAR>u_mono : Monotone u<VAR>I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * variance (Y j) ℙ ≤ 2 * ∫ (a : Ω), X 0 a<VAR>C : ℝ := c ^ 5 * (c - 1)⁻¹ ^ 3 * (2 * ∫ (a : Ω), X 0 a)<VAR>I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * variance (S (u i)) ℙ ≤ C<VAR>I3 : ∀ (N : ℕ), ∑ i ∈ range N, ℙ {ω | ↑(u i) * ε ≤ |S (u i) ω - ∫ (a : Ω), S (u i) a|} ≤ ENNReal.ofReal (ε⁻¹ ^ 2 * C)<VAR>I4 : ∑' (i : ℕ), ℙ {ω | ↑(u i) * ε ≤ |S (u i) ω - ∫ (a : Ω), S (u i) a|} < ⊤<VAR>ω : Ω<VAR>hω : ∀ᶠ (n : ℕ) in atTop, ¬↑(u n) * ε ≤ |S (u n) ω - ∫ (a : Ω), S (u n) a|<GOAL>∀ᶠ (n : ℕ) in atTop, |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (range ⌊c ^ n⌋₊).sum Y a| < ε * ↑⌊c ^ n⌋₊
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>c_pos : 0 < c<VAR>hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ<VAR>A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)<VAR>Y : ℕ → Ω → ℝ := fun n => truncation (X n) ↑n<VAR>S : ℕ → Ω → ℝ := fun n => ∑ i ∈ range n, Y i<VAR>hS : S = fun n => ∑ i ∈ range n, Y i<VAR>u : ℕ → ℕ := fun n => ⌊c ^ n⌋₊<VAR>u_mono : Monotone u<VAR>I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * variance (Y j) ℙ ≤ 2 * ∫ (a : Ω), X 0 a<VAR>C : ℝ := c ^ 5 * (c - 1)⁻¹ ^ 3 * (2 * ∫ (a : Ω), X 0 a)<VAR>I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * variance (S (u i)) ℙ ≤ C<VAR>I3 : ∀ (N : ℕ), ∑ i ∈ range N, ℙ {ω | ↑(u i) * ε ≤ |S (u i) ω - ∫ (a : Ω), S (u i) a|} ≤ ENNReal.ofReal (ε⁻¹ ^ 2 * C)<VAR>I4 : ∑' (i : ℕ), ℙ {ω | ↑(u i) * ε ≤ |S (u i) ω - ∫ (a : Ω), S (u i) a|} < ⊤<VAR>ω : Ω<VAR>hω : ∀ᶠ (n : ℕ) in atTop, |∑ c ∈ range (u n), Y c ω - ∫ (a : Ω), ∑ c ∈ range (u n), Y c a| < ε * ↑(u n)<GOAL>∀ᶠ (n : ℕ) in atTop, |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (range ⌊c ^ n⌋₊).sum Y a| < ε * ↑⌊c ^ n⌋₊
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>c_pos : 0 < c<VAR>hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ<VAR>A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)<VAR>Y : ℕ → Ω → ℝ := fun n => truncation (X n) ↑n<VAR>S : ℕ → Ω → ℝ := fun n => ∑ i ∈ range n, Y i<VAR>hS : S = fun n => ∑ i ∈ range n, Y i<VAR>u : ℕ → ℕ := fun n => ⌊c ^ n⌋₊<VAR>u_mono : Monotone u<VAR>I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * variance (Y j) ℙ ≤ 2 * ∫ (a : Ω), X 0 a<VAR>C : ℝ := c ^ 5 * (c - 1)⁻¹ ^ 3 * (2 * ∫ (a : Ω), X 0 a)<VAR>I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * variance (S (u i)) ℙ ≤ C<VAR>I3 : ∀ (N : ℕ), ∑ i ∈ range N, ℙ {ω | ↑(u i) * ε ≤ |S (u i) ω - ∫ (a : Ω), S (u i) a|} ≤ ENNReal.ofReal (ε⁻¹ ^ 2 * C)<VAR>I4 : ∑' (i : ℕ), ℙ {ω | ↑(u i) * ε ≤ |S (u i) ω - ∫ (a : Ω), S (u i) a|} < ⊤<VAR>ω : Ω<VAR>hω : ∀ᶠ (n : ℕ) in atTop, |∑ c ∈ range (u n), Y c ω - ∫ (a : Ω), ∑ c ∈ range (u n), Y c a| < ε * ↑(u n)<VAR>x✝¹ : ℕ<VAR>x✝ : Ω<GOAL>(range ⌊c ^ x✝¹⌋₊).sum Y x✝ = ∑ c ∈ range (u x✝¹), Y c x✝
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<VAR>P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)<VAR>μ ν : Measure ((i : ι) → α i)<VAR>hμ : IsProjectiveLimit μ P<VAR>I : Finset ι<GOAL>μ univ = (P I) univ
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : Group M<VAR>a b : M<VAR>ha : a ∈ S.centralizer<VAR>hb : b ∈ S.centralizer<GOAL>a / b ∈ S.centralizer
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b t₀ εf εg δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t<VAR>hfs : ∀ t ∈ Ioc a b, f t ∈ s t<VAR>hg : ContinuousOn g (Icc a b)<VAR>hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t<VAR>hgs : ∀ t ∈ Ioc a b, g t ∈ s t<VAR>hb : f b = g b<GOAL>EqOn f g (Icc a b)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b t₀ εf εg δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t<VAR>hfs : ∀ t ∈ Ioc a b, f t ∈ s t<VAR>hg : ContinuousOn g (Icc a b)<VAR>hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t<VAR>hgs : ∀ t ∈ Ioc a b, g t ∈ s t<VAR>hb : f b = g b<VAR>hv' : ∀ (t : ℝ), LipschitzOnWith K (Neg.neg ∘ v (-t)) (s (-t))<GOAL>EqOn f g (Icc a b)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b t₀ εf εg δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t<VAR>hfs : ∀ t ∈ Ioc a b, f t ∈ s t<VAR>hg : ContinuousOn g (Icc a b)<VAR>hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t<VAR>hgs : ∀ t ∈ Ioc a b, g t ∈ s t<VAR>hb : f b = g b<VAR>hv' : ∀ (t : ℝ), LipschitzOnWith K (Neg.neg ∘ v (-t)) (s (-t))<VAR>hmt1 : MapsTo Neg.neg (Icc (-b) (-a)) (Icc a b)<GOAL>EqOn f g (Icc a b)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b t₀ εf εg δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t<VAR>hfs : ∀ t ∈ Ioc a b, f t ∈ s t<VAR>hg : ContinuousOn g (Icc a b)<VAR>hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t<VAR>hgs : ∀ t ∈ Ioc a b, g t ∈ s t<VAR>hb : f b = g b<VAR>hv' : ∀ (t : ℝ), LipschitzOnWith K (Neg.neg ∘ v (-t)) (s (-t))<VAR>hmt1 : MapsTo Neg.neg (Icc (-b) (-a)) (Icc a b)<VAR>hmt2 : MapsTo Neg.neg (Ico (-b) (-a)) (Ioc a b)<GOAL>EqOn f g (Icc a b)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b t₀ εf εg δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t<VAR>hfs : ∀ t ∈ Ioc a b, f t ∈ s t<VAR>hg : ContinuousOn g (Icc a b)<VAR>hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t<VAR>hgs : ∀ t ∈ Ioc a b, g t ∈ s t<VAR>hb : f b = g b<VAR>hv' : ∀ (t : ℝ), LipschitzOnWith K (Neg.neg ∘ v (-t)) (s (-t))<VAR>hmt1 : MapsTo Neg.neg (Icc (-b) (-a)) (Icc a b)<VAR>hmt2 : MapsTo Neg.neg (Ico (-b) (-a)) (Ioc a b)<VAR>hmt3 : ∀ (t : ℝ), MapsTo Neg.neg (Ici t) (Iic (-t))<GOAL>EqOn f g (Icc a b)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b t₀ εf εg δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t<VAR>hfs : ∀ t ∈ Ioc a b, f t ∈ s t<VAR>hg : ContinuousOn g (Icc a b)<VAR>hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t<VAR>hgs : ∀ t ∈ Ioc a b, g t ∈ s t<VAR>hb : f b = g b<VAR>hv' : ∀ (t : ℝ), LipschitzOnWith K (Neg.neg ∘ v (-t)) (s (-t))<VAR>hmt1 : MapsTo Neg.neg (Icc (-b) (-a)) (Icc a b)<VAR>hmt2 : MapsTo Neg.neg (Ico (-b) (-a)) (Ioc a b)<VAR>hmt3 : ∀ (t : ℝ), MapsTo Neg.neg (Ici t) (Iic (-t))<GOAL>EqOn (f ∘ Neg.neg) (g ∘ Neg.neg) (Icc (-b) (-a))
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b t₀ εf εg δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t<VAR>hfs : ∀ t ∈ Ioc a b, f t ∈ s t<VAR>hg : ContinuousOn g (Icc a b)<VAR>hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t<VAR>hgs : ∀ t ∈ Ioc a b, g t ∈ s t<VAR>hb : f b = g b<VAR>hv' : ∀ (t : ℝ), LipschitzOnWith K (Neg.neg ∘ v (-t)) (s (-t))<VAR>hmt1 : MapsTo Neg.neg (Icc (-b) (-a)) (Icc a b)<VAR>hmt2 : MapsTo Neg.neg (Ico (-b) (-a)) (Ioc a b)<VAR>hmt3 : ∀ (t : ℝ), MapsTo Neg.neg (Ici t) (Iic (-t))<GOAL>∀ t ∈ Ico (-b) (-a), HasDerivWithinAt (f ∘ Neg.neg) ((Neg.neg ∘ v (-t)) ((f ∘ Neg.neg) t)) (Ici t) t
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b t₀ εf εg δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t<VAR>hfs : ∀ t ∈ Ioc a b, f t ∈ s t<VAR>hg : ContinuousOn g (Icc a b)<VAR>hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t<VAR>hgs : ∀ t ∈ Ioc a b, g t ∈ s t<VAR>hb : f b = g b<VAR>hv' : ∀ (t : ℝ), LipschitzOnWith K (Neg.neg ∘ v (-t)) (s (-t))<VAR>hmt1 : MapsTo Neg.neg (Icc (-b) (-a)) (Icc a b)<VAR>hmt2 : MapsTo Neg.neg (Ico (-b) (-a)) (Ioc a b)<VAR>hmt3 : ∀ (t : ℝ), MapsTo Neg.neg (Ici t) (Iic (-t))<GOAL>∀ t ∈ Ico (-b) (-a), HasDerivWithinAt (g ∘ Neg.neg) ((Neg.neg ∘ v (-t)) ((g ∘ Neg.neg) t)) (Ici t) t
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : Semiring A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R B<VAR>S : Subalgebra R A<VAR>ι : Type u_4<VAR>inst✝ : Nonempty ι<VAR>K : ι → Subalgebra R A<VAR>dir : Directed (fun x x_1 => x ≤ x_1) K<VAR>f : (i : ι) → ↥(K i) →ₐ[R] B<VAR>hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)<VAR>T : Subalgebra R A<VAR>hT : T = iSup K<VAR>i : ι<VAR>x : ↥T<VAR>hx : ↑x ∈ K i<GOAL>Set.iUnionLift (fun i => ↑(K i)) (fun i x => (f i) x) ⋯ ↑T ⋯ x = (f i) ⟨↑x, hx⟩
<VAR>n m : ℕ<VAR>i : Fin 2<VAR>hi : i ≠ 0<GOAL>i = 0 ↔ 1 = 0
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>f : Perm α<GOAL>sign f = (-1) ^ (f.cycleType.sum + card f.cycleType)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>f : Perm α<GOAL>(Multiset.map (fun n => -(-1) ^ n) f.cycleType).prod = (-1) ^ (f.cycleType.sum + card f.cycleType)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>f : Perm α<GOAL>(Multiset.map (fun n => -(-1) ^ n) 0).prod = (-1) ^ (Multiset.sum 0 + card 0)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>f : Perm α<VAR>a : ℕ<VAR>s : Multiset ℕ<VAR>ihs : (Multiset.map (fun n => -(-1) ^ n) s).prod = (-1) ^ (s.sum + card s)<GOAL>(Multiset.map (fun n => -(-1) ^ n) (a ::ₘ s)).prod = (-1) ^ ((a ::ₘ s).sum + card (a ::ₘ s))
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>inst✝¹ : Finite G<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H<GOAL>N.IsCommutative
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>inst✝¹ : Finite G<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H<VAR>this : Nontrivial ↥N<GOAL>N.IsCommutative
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>inst✝¹ : Finite G<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H<VAR>this✝ : Nontrivial ↥N<VAR>this : Fact (Nat.Prime (Nat.card ↥N).minFac)<GOAL>N.IsCommutative
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u t s s' : Set α<GOAL>t.ite s s' ∩ tᶜ = s' ∩ tᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>inst✝ : IsFiniteKernel κ<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Monotone seq<VAR>hseq_iUnion : ⋃ i, seq i = univ<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<GOAL>∀ᵐ (x : γ) ∂κ.fst a, Tendsto (fun m => κ.density κ.fst a x (seq m)) atTop (𝓝 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>inst✝ : IsFiniteKernel κ<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Monotone seq<VAR>hseq_iUnion : ⋃ i, seq i = univ<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<GOAL>∀ (n : ℕ), Integrable (fun x => κ.density κ.fst a x (seq n)) (κ.fst a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>inst✝ : IsFiniteKernel κ<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Monotone seq<VAR>hseq_iUnion : ⋃ i, seq i = univ<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<GOAL>Tendsto (fun i => ∫ (a_1 : γ), κ.density κ.fst a a_1 (seq i) ∂κ.fst a) atTop (𝓝 (∫ (a : γ), 1 ∂κ.fst a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>inst✝ : IsFiniteKernel κ<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Monotone seq<VAR>hseq_iUnion : ⋃ i, seq i = univ<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<GOAL>∀ᵐ (a_1 : γ) ∂κ.fst a, Monotone fun i => κ.density κ.fst a a_1 (seq i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>inst✝ : IsFiniteKernel κ<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Monotone seq<VAR>hseq_iUnion : ⋃ i, seq i = univ<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<GOAL>∀ᵐ (a_1 : γ) ∂κ.fst a, ∀ (i : ℕ), κ.density κ.fst a a_1 (seq i) ≤ 1
<VAR>s b : ℝ<VAR>hb : 0 < b<GOAL>Tendsto (fun x => x ^ s / rexp (b * x)) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n : ℤ<VAR>h : a = b * c⁻¹<GOAL>a * c = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n : ℤ<VAR>h : a * c = b<GOAL>a = b * c⁻¹
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : Archimedean α<VAR>x✝ y ε x : α<VAR>x0 : 0 < x<GOAL>∃ q, 0 < q ∧ ↑q < x
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<VAR>h : angle x y = 0<GOAL>⟪x, y⟫_ℝ = ‖x‖ * ‖y‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>C : E<GOAL>C = 0 ∨ (μ.restrict s) univ < ⊤ ↔ C = 0 ∨ μ s < ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CoheytingAlgebra α<VAR>a b c : α<GOAL>￢a ≤ b ↔ ￢b ≤ a
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>i✝ j✝ : n<GOAL>adjugate 1 i✝ j✝ = 1 i✝ j✝
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜<VAR>h𝒜₀ : ∅ ∉ 𝒜<GOAL>∑ s ∈ 𝒜, (↑((card α).choose s.card))⁻¹ ≤ infSum 𝒜
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜<VAR>h𝒜₀ : ∅ ∉ 𝒜<GOAL>∑ s ∈ 𝒜, (↑((card α).choose s.card))⁻¹ = ∑ s ∈ 𝒜, ↑(𝒜.truncatedInf s).card / (↑s.card * ↑((card α).choose s.card))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s✝ : Finset α<VAR>h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜<VAR>h𝒜₀ : ∅ ∉ 𝒜<VAR>s : Finset α<VAR>hs : s ∈ 𝒜<GOAL>(↑((card α).choose s.card))⁻¹ = ↑(𝒜.truncatedInf s).card / (↑s.card * ↑((card α).choose s.card))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s✝ : Finset α<VAR>h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜<VAR>h𝒜₀ : ∅ ∉ 𝒜<VAR>s : Finset α<VAR>hs : s ∈ 𝒜<GOAL>↑s.card ≠ 0
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s✝ : Finset α<VAR>h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜<VAR>h𝒜₀ : ∅ ∉ 𝒜<VAR>s : Finset α<VAR>hs : s ∈ 𝒜<VAR>this : 0 < s.card<GOAL>↑s.card ≠ 0
<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝ : QuasiSeparated (f ≫ g)<VAR>𝒰 : Y.OpenCover := (Z.affineCover.pullbackCover g).bind fun x => ((Z.affineCover.pullbackCover g).obj x).affineCover<VAR>this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)<GOAL>QuasiSeparated f
<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝ : QuasiSeparated (f ≫ g)<VAR>𝒰 : Y.OpenCover := (Z.affineCover.pullbackCover g).bind fun x => ((Z.affineCover.pullbackCover g).obj x).affineCover<VAR>this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)<GOAL>∀ (i : (((Z.affineCover.pullbackCover g).bind fun x => ((Z.affineCover.pullbackCover g).obj x).affineCover).pullbackCover f).J), QuasiSeparatedSpace ↑↑((((Z.affineCover.pullbackCover g).bind fun x => ((Z.affineCover.pullbackCover g).obj x).affineCover).pullbackCover f).obj i).toPresheafedSpace
<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝ : QuasiSeparated (f ≫ g)<VAR>𝒰 : Y.OpenCover := (Z.affineCover.pullbackCover g).bind fun x => ((Z.affineCover.pullbackCover g).obj x).affineCover<VAR>this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)<VAR>i : Z.affineCover.J<VAR>j : (pullback g (Z.affineCover.map i)).affineCover.J<GOAL>QuasiSeparatedSpace ↑↑((((Z.affineCover.pullbackCover g).bind fun x => ((Z.affineCover.pullbackCover g).obj x).affineCover).pullbackCover f).obj ⟨i, j⟩).toPresheafedSpace
<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝ : QuasiSeparated (f ≫ g)<VAR>𝒰 : Y.OpenCover := (Z.affineCover.pullbackCover g).bind fun x => ((Z.affineCover.pullbackCover g).obj x).affineCover<VAR>this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)<VAR>i : Z.affineCover.J<VAR>j : (pullback g (Z.affineCover.map i)).affineCover.J<GOAL>(((Z.affineCover.pullbackCover g).bind fun x => ((Z.affineCover.pullbackCover g).obj x).affineCover).pullbackCover f).obj ⟨i, j⟩ ⟶ pullback (f ≫ g) (Z.affineCover.map i)
<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝ : QuasiSeparated (f ≫ g)<VAR>𝒰 : Y.OpenCover := (Z.affineCover.pullbackCover g).bind fun x => ((Z.affineCover.pullbackCover g).obj x).affineCover<VAR>this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)<VAR>i : Z.affineCover.J<VAR>j : (pullback g (Z.affineCover.map i)).affineCover.J<GOAL>QuasiSeparated ?mk.refine_1
<VAR>n d : PosNum<VAR>q r : Num<VAR>h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n<VAR>h₂ : ↑r < 2 * ↑d<GOAL>↑(match Num.ofZNum' (r.sub' (Num.pos d)) with | some r' => (q.bit1, r') | none => (q.bit0, r)).2 + ↑d * ↑(match Num.ofZNum' (r.sub' (Num.pos d)) with | some r' => (q.bit1, r') | none => (q.bit0, r)).1 = ↑n ∧ ↑(match Num.ofZNum' (r.sub' (Num.pos d)) with | some r' => (q.bit1, r') | none => (q.bit0, r)).2 < ↑d
<VAR>n d : PosNum<VAR>q r : Num<VAR>h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n<VAR>h₂ : ↑r < 2 * ↑d<VAR>this : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d<GOAL>↑(match Num.ofZNum' (r.sub' (Num.pos d)) with | some r' => (q.bit1, r') | none => (q.bit0, r)).2 + ↑d * ↑(match Num.ofZNum' (r.sub' (Num.pos d)) with | some r' => (q.bit1, r') | none => (q.bit0, r)).1 = ↑n ∧ ↑(match Num.ofZNum' (r.sub' (Num.pos d)) with | some r' => (q.bit1, r') | none => (q.bit0, r)).2 < ↑d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : OpensMeasurableSpace α<VAR>e : ℕ → α<VAR>N : ℕ<VAR>x : α<GOAL>↑(nearestPtInd e (N + 1)) x = if ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x then N + 1 else ↑(nearestPtInd e N) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : OpensMeasurableSpace α<VAR>e : ℕ → α<VAR>N : ℕ<VAR>x : α<GOAL>(if x ∈ ⋂ k, ⋂ (_ : k ≤ N), {x | edist (e (N + 1)) x < edist (e k) x} then ↑(const α (N + 1)) x else ↑(nearestPtInd e N) x) = if ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x then N + 1 else ↑(nearestPtInd e N) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ι : Type u_6<VAR>f✝ : α →. β<VAR>p : β → Prop<VAR>f : α → β<VAR>a : α<VAR>b : Subtype p<GOAL>b ∈ toSubtype p f a ↔ ↑b = f a
<VAR>M : Type u_1<VAR>G : Type u_2<VAR>inst✝ : Monoid M<VAR>a : M<VAR>x y : Mˣ<VAR>h : SemiconjBy a ↑x ↑y<GOAL>a * ↑x⁻¹ = ↑y⁻¹ * (↑y * a) * ↑x⁻¹
<VAR>M : Type u_1<VAR>G : Type u_2<VAR>inst✝ : Monoid M<VAR>a : M<VAR>x y : Mˣ<VAR>h : SemiconjBy a ↑x ↑y<GOAL>↑y⁻¹ * (↑y * a) * ↑x⁻¹ = ↑y⁻¹ * a