ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>s : Set Y<VAR>h : X ≃ₜ Y<GOAL>IsSigmaCompact (⇑h.symm '' s) ↔ IsSigmaCompact s
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type u_2<VAR>inst✝ : MulAction R X<VAR>r : X<VAR>s s' : ↥S<GOAL>↑(s' * s) ∈ S
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : TopologicalSpace H<VAR>inst✝⁷ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>inst✝⁴ : TopologicalSpace H'<VAR>inst✝³ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : I.Boundaryless<VAR>x : M<GOAL>(extChartAt I x).target ∈ 𝓝 (↑(extChartAt I x) x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : TopologicalSpace H<VAR>inst✝⁷ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>inst✝⁴ : TopologicalSpace H'<VAR>inst✝³ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : I.Boundaryless<VAR>x : M<GOAL>𝓝 (↑(extChartAt I x) x) = 𝓝[range ↑I] ↑(extChartAt I x) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y z✝ : E<VAR>s : Set E<VAR>hs : StarConvex 𝕜 x s<VAR>z : E<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<VAR>y' : E<VAR>hy' : y' ∈ s<GOAL>(fun x => x + z) (a • x + b • y') = a • (x + z) + b • (fun x => x + z) y'
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>I✝ I : Ideal R<VAR>r : R<VAR>h : r - 1 ∈ I.jacobson<GOAL>∃ s, s * r - 1 ∈ I
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>I✝ I : Ideal R<VAR>r : R<VAR>h : r - 1 ∈ I.jacobson<VAR>s : R<VAR>hs : s * 1 * (r - 1) + s - 1 ∈ I<GOAL>∃ s, s * r - 1 ∈ I
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>I✝ I : Ideal R<VAR>r : R<VAR>h : r - 1 ∈ I.jacobson<VAR>s : R<VAR>hs : s * 1 * (r - 1) + s - 1 ∈ I<GOAL>s * r - 1 ∈ I
<VAR>n : ℕ<GOAL>n.size = 0 ↔ n = 0
<VAR>m e : Nat<GOAL>(if true = true then normalize (↑m) (10 ^ e) ⋯ else ↑(m * 10 ^ e)) = mkRat (↑m) (10 ^ e)
<VAR>m e : Nat<GOAL>(if true = true then mkRat (↑m) (10 ^ e) else ↑(m * 10 ^ e)) = mkRat (↑m) (10 ^ e)
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x - a) '' Ico b c = Ico (b - a) (c - a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s t : Set α<VAR>ht : t.Finite<VAR>hsub : s ⊂ t<VAR>this : Fintype ↑t<GOAL>Nat.card ↑s < Nat.card ↑t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s t : Set α<VAR>ht : t.Finite<VAR>hsub : s ⊂ t<VAR>this✝ : Fintype ↑t<VAR>this : Fintype ↑s<GOAL>Nat.card ↑s < Nat.card ↑t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s t : Set α<VAR>ht : t.Finite<VAR>hsub : s ⊂ t<VAR>this✝ : Fintype ↑t<VAR>this : Fintype ↑s<GOAL>Fintype.card ↑s < Fintype.card ↑t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : AddMonoidWithOne α<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : ZeroLEOneClass α<VAR>inst✝ : NeZero 1<VAR>n : ℕ<GOAL>0 < ↑n + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : AddMonoidWithOne α<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : ZeroLEOneClass α<VAR>inst✝ : NeZero 1<VAR>n : ℕ<GOAL>1 ≤ ↑n + 1
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace α'<VAR>inst✝² : One β<VAR>inst✝¹ : One γ<VAR>inst✝ : One δ<VAR>g : β → γ<VAR>f : α → β<VAR>f₂ : α → γ<VAR>m : β → γ → δ<VAR>x : α<GOAL>x ∉ mulTSupport f ↔ f =ᶠ[𝓝 x] 1
<VAR>α : Type u_1<VAR>inst✝⁷ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : SecondCountableTopology α<VAR>inst✝⁴ : BorelSpace α<VAR>inst✝³ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝² : IsLocallyFiniteMeasure ρ<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : α → E<VAR>hf : LocallyIntegrable f μ<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun a => ⨍ (y : α) in a, f y ∂μ) (v.filterAt x) (𝓝 (f x))
<VAR>α : Type u_1<VAR>inst✝⁷ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : SecondCountableTopology α<VAR>inst✝⁴ : BorelSpace α<VAR>inst✝³ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝² : IsLocallyFiniteMeasure ρ<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : α → E<VAR>hf : LocallyIntegrable f μ<VAR>x : α<VAR>hx : Tendsto (fun a => ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)<VAR>h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a<GOAL>Tendsto (fun a => ⨍ (y : α) in a, f y ∂μ) (v.filterAt x) (𝓝 (f x))
<VAR>α : Type u_1<VAR>inst✝⁷ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : SecondCountableTopology α<VAR>inst✝⁴ : BorelSpace α<VAR>inst✝³ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝² : IsLocallyFiniteMeasure ρ<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : α → E<VAR>hf : LocallyIntegrable f μ<VAR>x : α<VAR>hx : Tendsto (fun a => ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)<VAR>h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a<GOAL>Tendsto (fun e => ‖⨍ (y : α) in e, f y ∂μ - f x‖) (v.filterAt x) (𝓝 0)
<VAR>α : Type u_1<VAR>inst✝⁷ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : SecondCountableTopology α<VAR>inst✝⁴ : BorelSpace α<VAR>inst✝³ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝² : IsLocallyFiniteMeasure ρ<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : α → E<VAR>hf : LocallyIntegrable f μ<VAR>x : α<VAR>hx : Tendsto (fun a => ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)<VAR>h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a<GOAL>∀ᶠ (t : Set α) in v.filterAt x, ‖⨍ (y : α) in t, f y ∂μ - f x‖ ≤ ⨍ (y : α) in t, ‖f y - f x‖ ∂μ
<VAR>α : Type u_1<VAR>inst✝⁷ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : SecondCountableTopology α<VAR>inst✝⁴ : BorelSpace α<VAR>inst✝³ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝² : IsLocallyFiniteMeasure ρ<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : α → E<VAR>hf : LocallyIntegrable f μ<VAR>x : α<VAR>hx : Tendsto (fun a => ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)<VAR>h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a<VAR>a : Set α<VAR>ha : 0 < μ a<VAR>h'a : μ a < ⊤<VAR>h''a : IntegrableOn f a μ<GOAL>‖⨍ (y : α) in a, f y ∂μ - f x‖ ≤ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ
<VAR>α : Type u_1<VAR>inst✝⁷ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : SecondCountableTopology α<VAR>inst✝⁴ : BorelSpace α<VAR>inst✝³ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝² : IsLocallyFiniteMeasure ρ<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : α → E<VAR>hf : LocallyIntegrable f μ<VAR>x : α<VAR>hx : Tendsto (fun a => ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)<VAR>h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a<VAR>a : Set α<VAR>ha : 0 < μ a<VAR>h'a : μ a < ⊤<VAR>h''a : IntegrableOn f a μ<GOAL>‖⨍ (y : α) in a, f y ∂μ - ⨍ (x_1 : α) in a, f x ∂μ‖ ≤ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ
<VAR>α : Type u_1<VAR>inst✝⁷ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : SecondCountableTopology α<VAR>inst✝⁴ : BorelSpace α<VAR>inst✝³ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝² : IsLocallyFiniteMeasure ρ<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : α → E<VAR>hf : LocallyIntegrable f μ<VAR>x : α<VAR>hx : Tendsto (fun a => ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)<VAR>h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a<VAR>a : Set α<VAR>ha : 0 < μ a<VAR>h'a : μ a < ⊤<VAR>h''a : IntegrableOn f a μ<GOAL>‖∫ (y : α), f y ∂(μ a)⁻¹ • μ.restrict a - ∫ (x_1 : α), f x ∂(μ a)⁻¹ • μ.restrict a‖ ≤ ∫ (y : α), ‖f y - f x‖ ∂(μ a)⁻¹ • μ.restrict a
<VAR>α : Type u_1<VAR>inst✝⁷ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : SecondCountableTopology α<VAR>inst✝⁴ : BorelSpace α<VAR>inst✝³ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝² : IsLocallyFiniteMeasure ρ<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : α → E<VAR>hf : LocallyIntegrable f μ<VAR>x : α<VAR>hx : Tendsto (fun a => ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)<VAR>h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a<VAR>a : Set α<VAR>ha : 0 < μ a<VAR>h'a : μ a < ⊤<VAR>h''a : IntegrableOn f a μ<GOAL>‖∫ (a : α), f a - f x ∂(μ a)⁻¹ • μ.restrict a‖ ≤ ∫ (y : α), ‖f y - f x‖ ∂(μ a)⁻¹ • μ.restrict a
<VAR>α : Type u_1<VAR>inst✝⁷ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : SecondCountableTopology α<VAR>inst✝⁴ : BorelSpace α<VAR>inst✝³ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝² : IsLocallyFiniteMeasure ρ<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : α → E<VAR>hf : LocallyIntegrable f μ<VAR>x : α<VAR>hx : Tendsto (fun a => ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)<VAR>h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a<VAR>a : Set α<VAR>ha : 0 < μ a<VAR>h'a : μ a < ⊤<VAR>h''a : IntegrableOn f a μ<GOAL>Integrable f ((μ a)⁻¹ • μ.restrict a)
<VAR>α : Type u_1<VAR>inst✝⁷ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : SecondCountableTopology α<VAR>inst✝⁴ : BorelSpace α<VAR>inst✝³ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝² : IsLocallyFiniteMeasure ρ<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : α → E<VAR>hf : LocallyIntegrable f μ<VAR>x : α<VAR>hx : Tendsto (fun a => ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)<VAR>h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a<VAR>a : Set α<VAR>ha : 0 < μ a<VAR>h'a : μ a < ⊤<VAR>h''a : IntegrableOn f a μ<GOAL>Integrable (fun x_1 => f x) ((μ a)⁻¹ • μ.restrict a)
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v : V<VAR>p : G.Walk u v<GOAL>List.map (fun x => x.toProd.1) p.darts = p.support.dropLast
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i j n : ℕ<VAR>ipos : 0 < i<VAR>hin : i ≤ n<VAR>h : xn a1 j ≡ xn a1 i [MOD xn a1 n]<VAR>j' : ℕ := j % (4 * n)<VAR>n4 : 0 < 4 * n<VAR>jl : j' < 4 * n<GOAL>j % (4 * n) = j' % (4 * n)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i j✝ n : ℕ<VAR>ipos : 0 < i<VAR>hin : i ≤ n<VAR>h : xn a1 j✝ ≡ xn a1 i [MOD xn a1 n]<VAR>j' : ℕ := j✝ % (4 * n)<VAR>n4 : 0 < 4 * n<VAR>jl : j' < 4 * n<VAR>jj : j✝ ≡ j' [MOD 4 * n]<VAR>j q : ℕ<VAR>IH : xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]<GOAL>xn a1 (j + 4 * n * (q + 1)) ≡ xn a1 j [MOD xn a1 n]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i j✝ n : ℕ<VAR>ipos : 0 < i<VAR>hin : i ≤ n<VAR>h : xn a1 j✝ ≡ xn a1 i [MOD xn a1 n]<VAR>j' : ℕ := j✝ % (4 * n)<VAR>n4 : 0 < 4 * n<VAR>jl : j' < 4 * n<VAR>jj : j✝ ≡ j' [MOD 4 * n]<VAR>j q : ℕ<VAR>IH : xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]<GOAL>xn a1 (4 * n + (j + 4 * n * q)) ≡ xn a1 j [MOD xn a1 n]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i j n : ℕ<VAR>ipos : 0 < i<VAR>hin : i ≤ n<VAR>h : xn a1 j ≡ xn a1 i [MOD xn a1 n]<VAR>j' : ℕ := j % (4 * n)<VAR>n4 : 0 < 4 * n<VAR>jl : j' < 4 * n<VAR>jj : j ≡ j' [MOD 4 * n]<VAR>this : ∀ (j q : ℕ), xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]<VAR>ji : j' + i = 4 * n<GOAL>4 * n ≡ 0 [MOD 4 * n]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i j n : ℕ<VAR>ipos : 0 < i<VAR>hin : i ≤ n<VAR>h : xn a1 j ≡ xn a1 i [MOD xn a1 n]<VAR>j' : ℕ := j % (4 * n)<VAR>n4 : 0 < 4 * n<VAR>jl : j' < 4 * n<VAR>jj : j ≡ j' [MOD 4 * n]<VAR>this : ∀ (j q : ℕ), xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]<GOAL>xn a1 j ≡ xn a1 j' [MOD xn a1 n]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i j n : ℕ<VAR>ipos : 0 < i<VAR>hin : i ≤ n<VAR>h : xn a1 j ≡ xn a1 i [MOD xn a1 n]<VAR>j' : ℕ := j % (4 * n)<VAR>n4 : 0 < 4 * n<VAR>jl : j' < 4 * n<VAR>jj : j ≡ j' [MOD 4 * n]<VAR>this : ∀ (j q : ℕ), xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]<GOAL>xn a1 (j % (4 * n) + 4 * n * (j / (4 * n))) ≡ xn a1 j' [MOD xn a1 n]
<VAR>α : Sort u_1<VAR>σ : α → Sort u_2<VAR>P Q R : Prop<VAR>inst✝¹ : Decidable P<VAR>inst✝ : Decidable Q<VAR>a b c : α<VAR>A : P → α<VAR>B : ¬P → α<GOAL>(dite P A fun x => b) ≠ b ↔ ∃ h, A h ≠ b
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b✝ c : α<VAR>n : ℤ<VAR>b : α<GOAL>toIcoMod hp 0 b ∈ Set.Ico 0 p
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b✝ c : α<VAR>n : ℤ<VAR>b : α<GOAL>p = 0 + p
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>F : Cᵒᵖ ⥤ Type v₁<VAR>hF : F.Representable<VAR>X : Cᵒᵖ<VAR>f : unop X ⟶ F.reprX<GOAL>(F.reprW.app X).hom f = F.map f.op F.reprx
<VAR>α : Type u_1<VAR>inst✝¹ : StrictOrderedSemiring α<VAR>β : Type u_2<VAR>inst✝ : OrderedRing β<VAR>t : β<VAR>ht : t ∈ Ioo 0 1<GOAL>1 - t ∈ Ioo 0 1
<VAR>α : Type u_1<VAR>inst✝¹ : StrictOrderedSemiring α<VAR>β : Type u_2<VAR>inst✝ : OrderedRing β<VAR>t : β<VAR>ht : 0 < t ∧ t < 1<GOAL>0 < 1 - t ∧ 1 - t < 1
<VAR>α : Type u_1<VAR>inst✝¹ : StrictOrderedSemiring α<VAR>β : Type u_2<VAR>inst✝ : OrderedRing β<VAR>t : β<VAR>ht : 0 < t ∧ t < 1<GOAL>1 - t < 1
<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✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : NonUnitalNonAssocSemiring α<VAR>u v w : m → α<VAR>i : m<GOAL>v ⬝ᵥ diagonal w i = v i * w i
<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✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : NonUnitalNonAssocSemiring α<VAR>u v w : m → α<VAR>i : m<VAR>this : ∀ (j : m), j ≠ i → v j * diagonal w i j = 0<GOAL>v ⬝ᵥ diagonal w i = v i * w i
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝² : Group G<VAR>inst✝¹ : Fintype G<VAR>x✝ : G<VAR>n : ℕ<VAR>inst✝ : DecidableEq G<VAR>x : G<GOAL>x ∈ Finset.image (fun i => x✝ ^ i) (Finset.range (orderOf x✝)) ↔ x ∈ (↑(zpowers x✝)).toFinset
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a✝ : α<VAR>f g : α → β<VAR>inst✝¹ : CommGroup β<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>h : a ∈ s<GOAL>∏ x ∈ s.erase a, f x = (∏ x ∈ s, f x) / f a
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹³ : Ring R<VAR>inst✝¹² : CommRing S<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : AddCommGroup M'<VAR>inst✝⁹ : AddCommGroup M₁<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module R M'<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : StrongRankCondition R<VAR>inst✝⁴ : Module.Free R M<VAR>inst✝³ : (i : η) → AddCommGroup (φ i)<VAR>inst✝² : (i : η) → Module R (φ i)<VAR>inst✝¹ : ∀ (i : η), Module.Free R (φ i)<VAR>inst✝ : Fintype η<VAR>n : ℕ<GOAL>Module.rank R (Fin n → R) = ↑n
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : Monoid M<VAR>a : M<VAR>s : Set M<VAR>p : M → Prop<VAR>hs : closure s = ⊤<VAR>x : M<VAR>one : p 1<VAR>mul : ∀ x ∈ s, ∀ (y : M), p y → p (x * y)<VAR>this : x ∈ closure s<GOAL>p x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>edist (Memℒp.toLp (s.indicator fun x => c) ⋯) (Memℒp.toLp (t.indicator fun x => c) ⋯) = ↑‖Memℒp.toLp ((s ∆ t).indicator fun x => c) ⋯‖₊
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module ℝ E<VAR>s✝ t : Set E<VAR>x✝ : E<VAR>a✝ : ℝ<VAR>α : Type u_4<VAR>inst✝⁶ : LinearOrderedField α<VAR>inst✝⁵ : MulActionWithZero α ℝ<VAR>inst✝⁴ : OrderedSMul α ℝ<VAR>inst✝³ : MulActionWithZero α E<VAR>inst✝² : SMulCommClass α ℝ ℝ<VAR>inst✝¹ : IsScalarTower α ℝ ℝ<VAR>inst✝ : IsScalarTower α ℝ E<VAR>s : Set E<VAR>a : α<VAR>ha : 0 ≤ a<VAR>ha' : 0 < a<VAR>x : E<GOAL>gauge (a • s) x = (a⁻¹ • gauge s) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module ℝ E<VAR>s✝ t : Set E<VAR>x✝ : E<VAR>a✝ : ℝ<VAR>α : Type u_4<VAR>inst✝⁶ : LinearOrderedField α<VAR>inst✝⁵ : MulActionWithZero α ℝ<VAR>inst✝⁴ : OrderedSMul α ℝ<VAR>inst✝³ : MulActionWithZero α E<VAR>inst✝² : SMulCommClass α ℝ ℝ<VAR>inst✝¹ : IsScalarTower α ℝ ℝ<VAR>inst✝ : IsScalarTower α ℝ E<VAR>s : Set E<VAR>a : α<VAR>ha : 0 ≤ a<VAR>ha' : 0 < a<VAR>x : E<GOAL>sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ a • s} = sInf (a⁻¹ • {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ s})
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module ℝ E<VAR>s✝ t : Set E<VAR>x✝ : E<VAR>a✝ : ℝ<VAR>α : Type u_4<VAR>inst✝⁶ : LinearOrderedField α<VAR>inst✝⁵ : MulActionWithZero α ℝ<VAR>inst✝⁴ : OrderedSMul α ℝ<VAR>inst✝³ : MulActionWithZero α E<VAR>inst✝² : SMulCommClass α ℝ ℝ<VAR>inst✝¹ : IsScalarTower α ℝ ℝ<VAR>inst✝ : IsScalarTower α ℝ E<VAR>s : Set E<VAR>a : α<VAR>ha : 0 ≤ a<VAR>ha' : 0 < a<VAR>x : E<VAR>r : ℝ<GOAL>r ∈ {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ a • s} ↔ r ∈ a⁻¹ • {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ s}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module ℝ E<VAR>s✝ t : Set E<VAR>x✝ : E<VAR>a✝ : ℝ<VAR>α : Type u_4<VAR>inst✝⁶ : LinearOrderedField α<VAR>inst✝⁵ : MulActionWithZero α ℝ<VAR>inst✝⁴ : OrderedSMul α ℝ<VAR>inst✝³ : MulActionWithZero α E<VAR>inst✝² : SMulCommClass α ℝ ℝ<VAR>inst✝¹ : IsScalarTower α ℝ ℝ<VAR>inst✝ : IsScalarTower α ℝ E<VAR>s : Set E<VAR>a : α<VAR>ha : 0 ≤ a<VAR>ha' : 0 < a<VAR>x : E<VAR>r : ℝ<GOAL>(r ∈ Ioi 0 ∧ ∃ y ∈ s, a • y = r⁻¹ • x) ↔ ∃ y, (y ∈ Ioi 0 ∧ y⁻¹ • x ∈ s) ∧ a⁻¹ • y = r
<VAR>α : Type u<VAR>β : Type v<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsTrans α r<VAR>inst✝ : IsTrichotomous α r<VAR>a b c : α<VAR>h₁ : r a b<VAR>h₂ : ¬r c b<GOAL>r a c
<VAR>α : Type u<VAR>β : Type v<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsTrans α r<VAR>inst✝ : IsTrichotomous α r<VAR>a b c : α<VAR>h₁ : r a b<VAR>h₂ : ¬r c b<VAR>h₃ : r b c<GOAL>r a c
<VAR>α : Type u<VAR>β : Type v<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsTrans α r<VAR>inst✝ : IsTrichotomous α r<VAR>a b : α<VAR>h₁ : r a b<VAR>h₂ : ¬r b b<GOAL>r a b
<VAR>α : Type u<VAR>β : Type v<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsTrans α r<VAR>inst✝ : IsTrichotomous α r<VAR>a b c : α<VAR>h₁ : r a b<VAR>h₂ : ¬r c b<VAR>h₃ : r c b<GOAL>r a c
<VAR>x y : ℂ<GOAL>cexp (x - y) = cexp x / cexp y
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>h : p.last = q.head<VAR>i : Fin p.length<GOAL>(p.smash q h).toFun (Fin.castAdd q.length i).succ = p.toFun i.succ
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>h : p.last = q.head<VAR>i : Fin p.length<GOAL>(if H : ↑(Fin.castAdd q.length i).succ < p.length then p.toFun ⟨↑(Fin.castAdd q.length i).succ, ⋯⟩ else q.toFun ⟨↑(Fin.castAdd q.length i).succ - p.length, ⋯⟩) = p.toFun i.succ
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → ℝ<VAR>s : Set α<VAR>h : BoundedVariationOn f s<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>f x - f y ≤ (eVariationOn f s).toReal
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → ℝ<VAR>s : Set α<VAR>h : BoundedVariationOn f s<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>|f x - f y| ≤ (eVariationOn f s).toReal
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → ℝ<VAR>s : Set α<VAR>h : BoundedVariationOn f s<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>dist (f x) (f y) ≤ (eVariationOn f s).toReal
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>h : c < b<GOAL>(a * b + c) % b = c
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v✝ v : ι → R<VAR>i : ι<VAR>hi : i ∈ s<GOAL>nodal s v = (X - C (v i)) * ?m.116050
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>f✝ : X → Y<VAR>s : Set X<VAR>f : X → Y<VAR>hf : Inducing f<GOAL>IsLocallyClosed s ↔ ∃ s', IsLocallyClosed s' ∧ f ⁻¹' s' = s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>f✝ : X → Y<VAR>s : Set X<VAR>f : X → Y<VAR>hf : Inducing f<GOAL>(∃ U Z, (∃ t, IsOpen t ∧ f ⁻¹' t = U) ∧ (∃ t, IsClosed t ∧ f ⁻¹' t = Z) ∧ s = U ∩ Z) ↔ ∃ s', (∃ U Z, IsOpen U ∧ IsClosed Z ∧ s' = U ∩ Z) ∧ f ⁻¹' s' = s
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₀ p₁ p₂ p1 p2 p3 : P<VAR>h : ∠ p1 p2 p3 = π<GOAL>dist p1 p3 = dist p1 p2 + dist p3 p2
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₀ p₁ p₂ p1 p2 p3 : P<VAR>h : ∠ p1 p2 p3 = π<GOAL>‖p1 -ᵥ ?p₃ - (p3 -ᵥ ?p₃)‖ = ‖p1 -ᵥ p2‖ + ‖p3 -ᵥ p2‖
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₀ p₁ p₂ p1 p2 p3 : P<VAR>h : ∠ p1 p2 p3 = π<GOAL>P
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : SemilatticeSup α<VAR>s✝ : Finset β<VAR>H : s✝.Nonempty<VAR>f : β → α<VAR>inst✝ : DecidableEq β<VAR>s : Finset γ<VAR>Hs : s.Nonempty<VAR>t : γ → Finset β<VAR>Ht : ∀ (b : γ), (t b).Nonempty<VAR>c : α<GOAL>(s.biUnion t).sup' ⋯ f ≤ c ↔ (s.sup' Hs fun b => (t b).sup' ⋯ f) ≤ c
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Fintype R<VAR>R' : Type v<VAR>inst✝ : CommRing R'<VAR>p : ℕ<VAR>fp : Fact (Nat.Prime p)<VAR>hch : CharP R' p<VAR>χ : MulChar R R'<VAR>ψ : AddChar R R'<GOAL>gaussSum χ ψ ^ p = gaussSum (χ ^ p) (ψ ^ p)
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Fintype R<VAR>R' : Type v<VAR>inst✝ : CommRing R'<VAR>p : ℕ<VAR>fp : Fact (Nat.Prime p)<VAR>hch : CharP R' p<VAR>χ : MulChar R R'<VAR>ψ : AddChar R R'<GOAL>∑ x : R, (frobenius R' p) (χ x * ψ x) = ∑ a : R, (χ ^ p) a * (ψ ^ p) a
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Fintype R<VAR>R' : Type v<VAR>inst✝ : CommRing R'<VAR>p : ℕ<VAR>fp : Fact (Nat.Prime p)<VAR>hch : CharP R' p<VAR>χ : MulChar R R'<VAR>ψ : AddChar R R'<GOAL>∑ x : R, χ x ^ p * ψ x ^ p = ∑ x : R, χ x ^ p * (ψ ^ p) x