ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>ι : Type u_17<VAR>A : ι → α → E'<VAR>C : ι → ℝ<VAR>s : Finset ι<VAR>h : ∀ i ∈ s, IsBigOWith (C i) l (A i) g<GOAL>IsBigOWith (∑ i ∈ s, C i) l (fun x => ∑ i ∈ s, A i x) g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>ι : Type u_17<VAR>A : ι → α → E'<VAR>C : ι → ℝ<VAR>s : Finset ι<VAR>h : ∀ i ∈ ∅, IsBigOWith (C i) l (A i) g<GOAL>IsBigOWith (∑ i ∈ ∅, C i) l (fun x => ∑ i ∈ ∅, A i x) g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>ι : Type u_17<VAR>A : ι → α → E'<VAR>C : ι → ℝ<VAR>s✝ : Finset ι<VAR>i : ι<VAR>s : Finset ι<VAR>is : i ∉ s<VAR>IH : (∀ i ∈ s, IsBigOWith (C i) l (A i) g) → IsBigOWith (∑ i ∈ s, C i) l (fun x => ∑ i ∈ s, A i x) g<VAR>h : ∀ i_1 ∈ insert i s, IsBigOWith (C i_1) l (A i_1) g<GOAL>IsBigOWith (∑ i ∈ insert i s, C i) l (fun x => ∑ i ∈ insert i s, A i x) g
<VAR>α : Type u_1<VAR>inst✝ : CoheytingAlgebra α<VAR>a✝ b a : α<GOAL>￢￢a ⊔ ∂ a = a
<VAR>α : Type u_1<VAR>inst✝ : CoheytingAlgebra α<VAR>a✝ b a : α<GOAL>￢￢a ≤ a
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type u_3<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>x : AdicCompletion I M<GOAL>∃ a, (mk I M) a = x
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type u_3<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>x : AdicCompletion I M<VAR>a : ℕ → M<VAR>ha : ∀ (n : ℕ), Submodule.Quotient.mk (a n) = ↑x n<GOAL>∃ a, (mk I M) a = x
<VAR>G : Type u_1<VAR>inst✝⁵ : TopologicalSpace G<VAR>inst✝⁴ : Group G<VAR>inst✝³ : TopologicalGroup G<VAR>inst✝² : MeasurableSpace G<VAR>inst✝¹ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝ : μ.IsHaarMeasure<VAR>hG : LocallyCompactSpace G<GOAL>μ.haarScalarFactor μ = 1
<VAR>G : Type u_1<VAR>inst✝⁵ : TopologicalSpace G<VAR>inst✝⁴ : Group G<VAR>inst✝³ : TopologicalGroup G<VAR>inst✝² : MeasurableSpace G<VAR>inst✝¹ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝ : μ.IsHaarMeasure<VAR>hG : LocallyCompactSpace G<VAR>g : G → ℝ<VAR>g_cont : Continuous g<VAR>g_comp : HasCompactSupport ⇑{ toFun := g, continuous_toFun := g_cont }<VAR>g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont }<VAR>g_one : { toFun := g, continuous_toFun := g_cont } 1 ≠ 0<GOAL>μ.haarScalarFactor μ = 1
<VAR>G : Type u_1<VAR>inst✝⁵ : TopologicalSpace G<VAR>inst✝⁴ : Group G<VAR>inst✝³ : TopologicalGroup G<VAR>inst✝² : MeasurableSpace G<VAR>inst✝¹ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝ : μ.IsHaarMeasure<VAR>hG : LocallyCompactSpace G<VAR>g : G → ℝ<VAR>g_cont : Continuous g<VAR>g_comp : HasCompactSupport ⇑{ toFun := g, continuous_toFun := g_cont }<VAR>g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont }<VAR>g_one : { toFun := g, continuous_toFun := g_cont } 1 ≠ 0<VAR>int_g_ne_zero : ∫ (x : G), g x ∂μ ≠ 0<GOAL>μ.haarScalarFactor μ = 1
<VAR>G : Type u_1<VAR>inst✝⁵ : TopologicalSpace G<VAR>inst✝⁴ : Group G<VAR>inst✝³ : TopologicalGroup G<VAR>inst✝² : MeasurableSpace G<VAR>inst✝¹ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝ : μ.IsHaarMeasure<VAR>hG : LocallyCompactSpace G<VAR>g : G → ℝ<VAR>g_cont : Continuous g<VAR>g_comp : HasCompactSupport ⇑{ toFun := g, continuous_toFun := g_cont }<VAR>g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont }<VAR>g_one : { toFun := g, continuous_toFun := g_cont } 1 ≠ 0<VAR>int_g_ne_zero : ∫ (x : G), g x ∂μ ≠ 0<GOAL>↑(μ.haarScalarFactor μ) = ↑1
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasureSpace Ω<VAR>inst✝⁵ : IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>X : ℕ → Ω → E<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<GOAL>∀ᵐ (ω : Ω), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasureSpace Ω<VAR>inst✝⁵ : IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>X : ℕ → Ω → E<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>A : ∀ (i : ℕ), Integrable (X i) ℙ<GOAL>∀ᵐ (ω : Ω), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasureSpace Ω<VAR>inst✝⁵ : IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>X : ℕ → Ω → E<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>A : ∀ (i : ℕ), Integrable (X i) ℙ<VAR>Y : ℕ → Ω → E := fun i => AEStronglyMeasurable.mk (X i) ⋯<GOAL>∀ᵐ (ω : Ω), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasureSpace Ω<VAR>inst✝⁵ : IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>X : ℕ → Ω → E<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>A : ∀ (i : ℕ), Integrable (X i) ℙ<VAR>Y : ℕ → Ω → E := fun i => AEStronglyMeasurable.mk (X i) ⋯<VAR>B : ∀ᵐ (ω : Ω), ∀ (n : ℕ), X n ω = Y n ω<GOAL>∀ᵐ (ω : Ω), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasureSpace Ω<VAR>inst✝⁵ : IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>X : ℕ → Ω → E<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>A : ∀ (i : ℕ), Integrable (X i) ℙ<VAR>Y : ℕ → Ω → E := fun i => AEStronglyMeasurable.mk (X i) ⋯<VAR>B : ∀ᵐ (ω : Ω), ∀ (n : ℕ), X n ω = Y n ω<VAR>Yint : Integrable (Y 0) ℙ<GOAL>∀ᵐ (ω : Ω), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasureSpace Ω<VAR>inst✝⁵ : IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>X : ℕ → Ω → E<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>A : ∀ (i : ℕ), Integrable (X i) ℙ<VAR>Y : ℕ → Ω → E := fun i => AEStronglyMeasurable.mk (X i) ⋯<VAR>B : ∀ᵐ (ω : Ω), ∀ (n : ℕ), X n ω = Y n ω<VAR>Yint : Integrable (Y 0) ℙ<VAR>C : ∀ᵐ (ω : Ω), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (a : Ω), Y 0 a))<GOAL>∀ᵐ (ω : Ω), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasureSpace Ω<VAR>inst✝⁵ : IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>X : ℕ → Ω → E<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>A : ∀ (i : ℕ), Integrable (X i) ℙ<VAR>Y : ℕ → Ω → E := fun i => AEStronglyMeasurable.mk (X i) ⋯<VAR>B : ∀ᵐ (ω : Ω), ∀ (n : ℕ), X n ω = Y n ω<VAR>Yint : Integrable (Y 0) ℙ<VAR>C : ∀ᵐ (ω : Ω), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (a : Ω), Y 0 a))<VAR>ω : Ω<VAR>h₁ : ∀ (n : ℕ), X n ω = Y n ω<VAR>h₂ : Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (a : Ω), Y 0 a))<GOAL>Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasureSpace Ω<VAR>inst✝⁵ : IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>X : ℕ → Ω → E<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>A : ∀ (i : ℕ), Integrable (X i) ℙ<VAR>Y : ℕ → Ω → E := fun i => AEStronglyMeasurable.mk (X i) ⋯<VAR>B : ∀ᵐ (ω : Ω), ∀ (n : ℕ), X n ω = Y n ω<VAR>Yint : Integrable (Y 0) ℙ<VAR>C : ∀ᵐ (ω : Ω), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (a : Ω), Y 0 a))<VAR>ω : Ω<VAR>h₁ : ∀ (n : ℕ), X n ω = Y n ω<VAR>h₂ : Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (a : Ω), Y 0 a))<VAR>this : ∫ (a : Ω), X 0 a = ∫ (a : Ω), Y 0 a<GOAL>Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasureSpace Ω<VAR>inst✝⁵ : IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>X : ℕ → Ω → E<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>A : ∀ (i : ℕ), Integrable (X i) ℙ<VAR>Y : ℕ → Ω → E := fun i => AEStronglyMeasurable.mk (X i) ⋯<VAR>B : ∀ᵐ (ω : Ω), ∀ (n : ℕ), X n ω = Y n ω<VAR>Yint : Integrable (Y 0) ℙ<VAR>C : ∀ᵐ (ω : Ω), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (a : Ω), Y 0 a))<VAR>ω : Ω<VAR>h₁ : ∀ (n : ℕ), X n ω = Y n ω<VAR>h₂ : Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (a : Ω), Y 0 a))<VAR>this : ∫ (a : Ω), X 0 a = ∫ (a : Ω), Y 0 a<GOAL>Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (a : Ω), Y 0 a))
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasureSpace Ω<VAR>inst✝⁵ : IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>X : ℕ → Ω → E<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>A : ∀ (i : ℕ), Integrable (X i) ℙ<VAR>Y : ℕ → Ω → E := fun i => AEStronglyMeasurable.mk (X i) ⋯<VAR>B : ∀ᵐ (ω : Ω), ∀ (n : ℕ), X n ω = Y n ω<VAR>Yint : Integrable (Y 0) ℙ<VAR>C : ∀ᵐ (ω : Ω), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (a : Ω), Y 0 a))<VAR>ω : Ω<VAR>h₁ : ∀ (n : ℕ), X n ω = Y n ω<VAR>h₂ : Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (a : Ω), Y 0 a))<VAR>this : ∫ (a : Ω), X 0 a = ∫ (a : Ω), Y 0 a<VAR>n : ℕ<GOAL>(↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω = (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasureSpace Ω<VAR>inst✝⁵ : IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>X : ℕ → Ω → E<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>A : ∀ (i : ℕ), Integrable (X i) ℙ<VAR>Y : ℕ → Ω → E := fun i => AEStronglyMeasurable.mk (X i) ⋯<VAR>B : ∀ᵐ (ω : Ω), ∀ (n : ℕ), X n ω = Y n ω<VAR>Yint : Integrable (Y 0) ℙ<VAR>C : ∀ᵐ (ω : Ω), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (a : Ω), Y 0 a))<VAR>ω : Ω<VAR>h₁ : ∀ (n : ℕ), X n ω = Y n ω<VAR>h₂ : Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (a : Ω), Y 0 a))<VAR>this : ∫ (a : Ω), X 0 a = ∫ (a : Ω), Y 0 a<VAR>n i : ℕ<GOAL>Y i ω = X i ω
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hb : b ≠ 0<GOAL>a / b ≠ 0 ↔ b ≤ a
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝²¹ : NormedAddCommGroup E<VAR>inst✝²⁰ : NormedAddCommGroup F<VAR>inst✝¹⁹ : NormedAddCommGroup G<VAR>inst✝¹⁸ : NormedAddCommGroup Fₗ<VAR>inst✝¹⁷ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜₂<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜₃<VAR>inst✝¹⁴ : NormedSpace 𝕜 E<VAR>inst✝¹³ : NormedSpace 𝕜₂ F<VAR>inst✝¹² : NormedSpace 𝕜₃ G<VAR>inst✝¹¹ : NormedSpace 𝕜 Fₗ<VAR>c✝ : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>𝕜₂' : Type u_11<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₂'<VAR>F' : Type u_12<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜₂' F'<VAR>σ₂' : 𝕜₂' →+* 𝕜₂<VAR>σ₂'' : 𝕜₂ →+* 𝕜₂'<VAR>σ₂₃' : 𝕜₂' →+* 𝕜₃<VAR>inst✝⁷ : RingHomInvPair σ₂' σ₂''<VAR>inst✝⁶ : RingHomInvPair σ₂'' σ₂'<VAR>inst✝⁵ : RingHomCompTriple σ₂' σ₂₃ σ₂₃'<VAR>inst✝⁴ : RingHomCompTriple σ₂'' σ₂₃' σ₂₃<VAR>inst✝³ : RingHomIsometric σ₂₃<VAR>inst✝² : RingHomIsometric σ₂'<VAR>inst✝¹ : RingHomIsometric σ₂''<VAR>inst✝ : RingHomIsometric σ₂₃'<VAR>c : E →L[𝕜] 𝕜<VAR>f : Fₗ<GOAL>‖c.smulRight f‖ = ‖c‖ * ‖f‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝²¹ : NormedAddCommGroup E<VAR>inst✝²⁰ : NormedAddCommGroup F<VAR>inst✝¹⁹ : NormedAddCommGroup G<VAR>inst✝¹⁸ : NormedAddCommGroup Fₗ<VAR>inst✝¹⁷ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜₂<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜₃<VAR>inst✝¹⁴ : NormedSpace 𝕜 E<VAR>inst✝¹³ : NormedSpace 𝕜₂ F<VAR>inst✝¹² : NormedSpace 𝕜₃ G<VAR>inst✝¹¹ : NormedSpace 𝕜 Fₗ<VAR>c✝ : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>𝕜₂' : Type u_11<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₂'<VAR>F' : Type u_12<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜₂' F'<VAR>σ₂' : 𝕜₂' →+* 𝕜₂<VAR>σ₂'' : 𝕜₂ →+* 𝕜₂'<VAR>σ₂₃' : 𝕜₂' →+* 𝕜₃<VAR>inst✝⁷ : RingHomInvPair σ₂' σ₂''<VAR>inst✝⁶ : RingHomInvPair σ₂'' σ₂'<VAR>inst✝⁵ : RingHomCompTriple σ₂' σ₂₃ σ₂₃'<VAR>inst✝⁴ : RingHomCompTriple σ₂'' σ₂₃' σ₂₃<VAR>inst✝³ : RingHomIsometric σ₂₃<VAR>inst✝² : RingHomIsometric σ₂'<VAR>inst✝¹ : RingHomIsometric σ₂''<VAR>inst✝ : RingHomIsometric σ₂₃'<VAR>c : E →L[𝕜] 𝕜<VAR>f : Fₗ<GOAL>‖c.smulRight f‖ ≤ ‖c‖ * ‖f‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝²¹ : NormedAddCommGroup E<VAR>inst✝²⁰ : NormedAddCommGroup F<VAR>inst✝¹⁹ : NormedAddCommGroup G<VAR>inst✝¹⁸ : NormedAddCommGroup Fₗ<VAR>inst✝¹⁷ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜₂<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜₃<VAR>inst✝¹⁴ : NormedSpace 𝕜 E<VAR>inst✝¹³ : NormedSpace 𝕜₂ F<VAR>inst✝¹² : NormedSpace 𝕜₃ G<VAR>inst✝¹¹ : NormedSpace 𝕜 Fₗ<VAR>c✝ : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>𝕜₂' : Type u_11<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₂'<VAR>F' : Type u_12<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜₂' F'<VAR>σ₂' : 𝕜₂' →+* 𝕜₂<VAR>σ₂'' : 𝕜₂ →+* 𝕜₂'<VAR>σ₂₃' : 𝕜₂' →+* 𝕜₃<VAR>inst✝⁷ : RingHomInvPair σ₂' σ₂''<VAR>inst✝⁶ : RingHomInvPair σ₂'' σ₂'<VAR>inst✝⁵ : RingHomCompTriple σ₂' σ₂₃ σ₂₃'<VAR>inst✝⁴ : RingHomCompTriple σ₂'' σ₂₃' σ₂₃<VAR>inst✝³ : RingHomIsometric σ₂₃<VAR>inst✝² : RingHomIsometric σ₂'<VAR>inst✝¹ : RingHomIsometric σ₂''<VAR>inst✝ : RingHomIsometric σ₂₃'<VAR>c : E →L[𝕜] 𝕜<VAR>f : Fₗ<GOAL>‖c‖ * ‖f‖ ≤ ‖c.smulRight f‖
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a✝ a b c : α<VAR>h : c < 0<GOAL>(fun x => x * c) ⁻¹' Ioo a b = Ioo (b / c) (a / c)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>l : Filter α<VAR>hl : l.NeBot<GOAL>Cauchy l ↔ l ×ˢ l ≤ 𝓤 α
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>o.oangle x y = 0 ∨ o.oangle x y = ↑π ↔ ¬LinearIndependent ℝ ![x, y]
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ a : ℝ<VAR>ha : a ≠ 0<GOAL>IsIntegralCurve γ v ↔ IsIntegralCurve (γ ∘ fun x => x * a) (a • v)
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ a : ℝ<VAR>ha : a ≠ 0<VAR>hγ : IsIntegralCurve (γ ∘ fun x => x * a) (a • v)<GOAL>IsIntegralCurve γ v
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ a : ℝ<VAR>ha : a ≠ 0<VAR>hγ : IsIntegralCurve (γ ∘ fun x => x * a) (a • v)<GOAL>γ = (γ ∘ fun x => x * a) ∘ fun x => x * a⁻¹
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ a : ℝ<VAR>ha : a ≠ 0<VAR>hγ : IsIntegralCurve (γ ∘ fun x => x * a) (a • v)<GOAL>v = a⁻¹ • a • v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>g : β → γ → δ<VAR>hg : Continuous (uncurry g)<VAR>f₁ : α →ₘ[μ] β<VAR>f₂ : α →ₘ[μ] γ<GOAL>comp₂ g hg f₁ f₂ = mk (fun a => g (↑f₁ a) (↑f₂ a)) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>g : β → γ → δ<VAR>hg : Continuous (uncurry g)<VAR>f₁ : α →ₘ[μ] β<VAR>f₂ : α →ₘ[μ] γ<GOAL>mk (uncurry g ∘ fun x => (↑f₁ x, ↑f₂ x)) ⋯ = mk (fun a => g (↑f₁ a) (↑f₂ a)) ⋯
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>W X Y Z X₁ X₂ X₃ Z₁ Z₂ : C<VAR>g₁ : Z₁ ⟶ X₁<VAR>g₂ : Z₁ ⟶ X₂<VAR>g₃ : Z₂ ⟶ X₂<VAR>g₄ : Z₂ ⟶ X₃<VAR>inst✝³ : HasPushout g₁ g₂<VAR>inst✝² : HasPushout g₃ g₄<VAR>inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄<VAR>inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)<GOAL>pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄) ≫ (pushoutAssoc g₁ g₂ g₃ g₄).inv = pushout.inl g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>s s₁ s₂ : Finset β<VAR>f : β → α<VAR>a : α<GOAL>a ∣ s.gcd f ↔ ∀ b ∈ s, a ∣ f b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>s s₁ s₂ : Finset β<VAR>f : β → α<VAR>a : α<GOAL>(∀ b ∈ Multiset.map f s.val, a ∣ b) ↔ ∀ b ∈ s, a ∣ f b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>s s₁ s₂ : Finset β<VAR>f : β → α<VAR>a : α<GOAL>(∀ (b : α), ∀ x ∈ s.val, f x = b → a ∣ b) ↔ ∀ b ∈ s, a ∣ f b
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>c₁ c₂ : R<VAR>q : Basis A c₁ c₂<GOAL>q.i * q.k = c₁ • q.j
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝³ : Monoid N<VAR>hnontriv : Nontrivial ι<VAR>G : Type u_4<VAR>inst✝² : Group G<VAR>H : ι → Type u_5<VAR>inst✝¹ : (i : ι) → Group (H i)<VAR>f : (i : ι) → H i →* G<VAR>hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)<VAR>α : Type u_6<VAR>inst✝ : MulAction G α<VAR>X : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i<VAR>i j k : ι<VAR>w : NeWord H i j<VAR>hhead : k ≠ i<VAR>hlast : k ≠ j<VAR>heq1 : (lift f) w.prod = 1<GOAL>False
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝³ : Monoid N<VAR>hnontriv : Nontrivial ι<VAR>G : Type u_4<VAR>inst✝² : Group G<VAR>H : ι → Type u_5<VAR>inst✝¹ : (i : ι) → Group (H i)<VAR>f : (i : ι) → H i →* G<VAR>hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)<VAR>α : Type u_6<VAR>inst✝ : MulAction G α<VAR>X : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i<VAR>i j k : ι<VAR>w : NeWord H i j<VAR>hhead : k ≠ i<VAR>hlast : k ≠ j<VAR>heq1 : (lift f) w.prod = 1<VAR>this : X k ⊆ X i<GOAL>False