ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>H✝ : Type uH<VAR>inst✝³ : TopologicalSpace H✝<VAR>I : ModelWithCorners ℝ E H✝<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H✝ M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>f : SmoothPartitionOfUnity ι I M s<VAR>n : ℕ∞<VAR>x : M<VAR>hx : x ∈ s<VAR>h : ∀ (i : ι), (f i) x ≤ 0<VAR>H : ∀ (i : ι), (f i) x = 0<VAR>this : ∑ᶠ (i : ι), (f i) x = 1<GOAL>False
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>a b : α<VAR>x : WithTop α<GOAL>x ∈ range some ↔ x ∈ Iio ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁵ : MeasurableSpace δ<VAR>inst✝⁴ : NormedAddCommGroup β<VAR>inst✝³ : NormedAddCommGroup γ<VAR>𝕜 : Type u_5<VAR>inst✝² : NormedRing 𝕜<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : BoundedSMul 𝕜 β<VAR>f : α → 𝕜<VAR>hf : Integrable f μ<VAR>g : α → β<VAR>g_aestronglyMeasurable : AEStronglyMeasurable g μ<VAR>ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤<GOAL>Integrable (fun x => f x • g x) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁵ : MeasurableSpace δ<VAR>inst✝⁴ : NormedAddCommGroup β<VAR>inst✝³ : NormedAddCommGroup γ<VAR>𝕜 : Type u_5<VAR>inst✝² : NormedRing 𝕜<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : BoundedSMul 𝕜 β<VAR>f : α → 𝕜<VAR>hf : Memℒp f 1 μ<VAR>g : α → β<VAR>g_aestronglyMeasurable : AEStronglyMeasurable g μ<VAR>ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤<GOAL>Memℒp (fun x => f x • g x) 1 μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁵ : MeasurableSpace δ<VAR>inst✝⁴ : NormedAddCommGroup β<VAR>inst✝³ : NormedAddCommGroup γ<VAR>𝕜 : Type u_5<VAR>inst✝² : NormedRing 𝕜<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : BoundedSMul 𝕜 β<VAR>f : α → 𝕜<VAR>hf : Memℒp f 1 μ<VAR>g : α → β<VAR>g_aestronglyMeasurable : AEStronglyMeasurable g μ<VAR>ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤<GOAL>eLpNorm (fun x => f x • g x) 1 μ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁵ : MeasurableSpace δ<VAR>inst✝⁴ : NormedAddCommGroup β<VAR>inst✝³ : NormedAddCommGroup γ<VAR>𝕜 : Type u_5<VAR>inst✝² : NormedRing 𝕜<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : BoundedSMul 𝕜 β<VAR>f : α → 𝕜<VAR>hf : Memℒp f 1 μ<VAR>g : α → β<VAR>g_aestronglyMeasurable : AEStronglyMeasurable g μ<VAR>ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤<VAR>h : 1 / 1 = 1 / 1 + 1 / ⊤<GOAL>eLpNorm (fun x => f x • g x) 1 μ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁵ : MeasurableSpace δ<VAR>inst✝⁴ : NormedAddCommGroup β<VAR>inst✝³ : NormedAddCommGroup γ<VAR>𝕜 : Type u_5<VAR>inst✝² : NormedRing 𝕜<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : BoundedSMul 𝕜 β<VAR>f : α → 𝕜<VAR>hf : Memℒp f 1 μ<VAR>g : α → β<VAR>g_aestronglyMeasurable : AEStronglyMeasurable g μ<VAR>ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤<VAR>h : 1 / 1 = 1 / 1 + 1 / ⊤<VAR>hg' : eLpNorm g ⊤ μ ≠ ⊤<GOAL>eLpNorm (fun x => f x • g x) 1 μ < ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>n : ℕ<VAR>hdeg : n < f.natDegree<VAR>a✝ : Nontrivial R<GOAL>h.modByMonicHom (h.root ^ n) = X ^ n
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>n : ℕ<VAR>hdeg : n < f.natDegree<VAR>a✝ : Nontrivial R<GOAL>↑n < f.degree
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>n : ℕ<VAR>a✝ : Nontrivial R<VAR>hdeg : f.degree ≤ ↑n<GOAL>f.natDegree ≤ n
<VAR>F : Type u_1<VAR>inst✝ : NormedAddCommGroup F<VAR>g : ℝ → F<VAR>R : ℝ<VAR>hR : R ≠ 0<GOAL>Integrable (fun x => g (x * R)) volume ↔ Integrable g volume
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s : Set E<VAR>hs : Convex ℝ s<GOAL>μ (frontier s) = 0
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s : Set E<VAR>hs : Convex ℝ s<VAR>hspan : affineSpan ℝ s ≠ ⊤<GOAL>μ (frontier s) = 0
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s : Set E<VAR>hs : Convex ℝ s<VAR>hspan : affineSpan ℝ s = ⊤<GOAL>μ (frontier s) = 0
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s : Set E<VAR>hs : Convex ℝ s<VAR>hspan : (interior s).Nonempty<GOAL>μ (frontier s) = 0
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s : Set E<VAR>hs : Convex ℝ s<VAR>x : E<VAR>hx : x ∈ interior s<GOAL>μ (frontier s) = 0
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s : Set E<VAR>hs : Convex ℝ s<VAR>x : E<VAR>hx : x ∈ interior s<GOAL>∀ (t : Set E), Convex ℝ t → x ∈ interior t → Bornology.IsBounded t → μ (frontier t) = 0
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s✝ : Set E<VAR>hs✝ : Convex ℝ s✝<VAR>x : E<VAR>hx✝ : x ∈ interior s✝<VAR>s : Set E<VAR>hs : Convex ℝ s<VAR>hx : x ∈ interior s<VAR>hb : Bornology.IsBounded s<GOAL>μ (frontier s) = 0
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s✝ : Set E<VAR>hs✝ : Convex ℝ s✝<VAR>x : E<VAR>hx✝ : x ∈ interior s✝<VAR>s : Set E<VAR>hs : Convex ℝ s<VAR>hx : x ∈ interior s<VAR>hb : μ (interior s) ≠ ⊤<GOAL>μ (frontier s) = 0
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s✝ : Set E<VAR>hs✝ : Convex ℝ s✝<VAR>x : E<VAR>hx✝ : x ∈ interior s✝<VAR>s : Set E<VAR>hs : Convex ℝ s<VAR>hx : x ∈ interior s<VAR>hb : μ (interior s) ≠ ⊤<GOAL>μ (closure s) ≤ μ (interior s)
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s✝ : Set E<VAR>hs✝ : Convex ℝ s✝<VAR>x : E<VAR>hx✝ : x ∈ interior s✝<VAR>s : Set E<VAR>hs : Convex ℝ s<VAR>hx : x ∈ interior s<VAR>hb : μ (interior s) ≠ ⊤<VAR>d : ℕ := finrank ℝ E<GOAL>μ (closure s) ≤ μ (interior s)
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s✝ : Set E<VAR>hs✝ : Convex ℝ s✝<VAR>x : E<VAR>hx✝ : x ∈ interior s✝<VAR>s : Set E<VAR>hs : Convex ℝ s<VAR>hx : x ∈ interior s<VAR>hb : μ (interior s) ≠ ⊤<VAR>d : ℕ := finrank ℝ E<VAR>this : ∀ (r : ℝ≥0), 1 < r → μ (closure s) ≤ ↑(r ^ d) * μ (interior s)<GOAL>μ (closure s) ≤ μ (interior s)
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s✝ : Set E<VAR>hs✝ : Convex ℝ s✝<VAR>x : E<VAR>hx✝ : x ∈ interior s✝<VAR>s : Set E<VAR>hs : Convex ℝ s<VAR>hx : x ∈ interior s<VAR>hb : μ (interior s) ≠ ⊤<VAR>d : ℕ := finrank ℝ E<VAR>this✝ : ∀ (r : ℝ≥0), 1 < r → μ (closure s) ≤ ↑(r ^ d) * μ (interior s)<VAR>this : ∀ᶠ (r : ℝ≥0) in 𝓝[>] 1, μ (closure s) ≤ ↑(r ^ d) * μ (interior s)<GOAL>μ (closure s) ≤ μ (interior s)
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s✝ : Set E<VAR>hs✝ : Convex ℝ s✝<VAR>x : E<VAR>hx✝ : x ∈ interior s✝<VAR>s : Set E<VAR>hs : Convex ℝ s<VAR>hx : x ∈ interior s<VAR>hb : μ (interior s) ≠ ⊤<VAR>d : ℕ := finrank ℝ E<VAR>this✝ : ∀ (r : ℝ≥0), 1 < r → μ (closure s) ≤ ↑(r ^ d) * μ (interior s)<VAR>this : ∀ᶠ (r : ℝ≥0) in 𝓝[>] 1, μ (closure s) ≤ ↑(r ^ d) * μ (interior s)<GOAL>Tendsto (fun c => ↑(c ^ d) * μ (interior s)) (𝓝[>] 1) (𝓝 (μ (interior s)))
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s✝ : Set E<VAR>hs✝ : Convex ℝ s✝<VAR>x : E<VAR>hx✝ : x ∈ interior s✝<VAR>s : Set E<VAR>hs : Convex ℝ s<VAR>hx : x ∈ interior s<VAR>hb : μ (interior s) ≠ ⊤<VAR>d : ℕ := finrank ℝ E<VAR>this✝ : ∀ (r : ℝ≥0), 1 < r → μ (closure s) ≤ ↑(r ^ d) * μ (interior s)<VAR>this : ∀ᶠ (r : ℝ≥0) in 𝓝[>] 1, μ (closure s) ≤ ↑(r ^ d) * μ (interior s)<GOAL>((fun x => x * μ (interior s)) ∘ ENNReal.ofNNReal ∘ fun a => a ^ d) 1 = μ (interior s)
<VAR>R : Type u_1<VAR>inst✝³ : CommMonoid R<VAR>R' : Type u_2<VAR>inst✝² : CommRing R'<VAR>R'' : Type u_3<VAR>inst✝¹ : CommRing R''<VAR>χ : MulChar R R'<VAR>hχ : χ.IsQuadratic<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CharP R' p<VAR>x : Rˣ<GOAL>(χ ^ p) ↑x = χ ↑x
<VAR>R : Type u_1<VAR>inst✝³ : CommMonoid R<VAR>R' : Type u_2<VAR>inst✝² : CommRing R'<VAR>R'' : Type u_3<VAR>inst✝¹ : CommRing R''<VAR>χ : MulChar R R'<VAR>hχ : χ.IsQuadratic<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CharP R' p<VAR>x : Rˣ<GOAL>χ ↑x ^ p = χ ↑x
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A✝ B✝ C✝ A B C : Finset α<GOAL>(A * C).card * B.card ≤ (A * B).card * (B * C).card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A✝ B C✝ A C : Finset α<GOAL>(A * C).card * ∅.card ≤ (A * ∅).card * (∅ * C).card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A✝ B✝ C✝ A B C : Finset α<VAR>hB : B.Nonempty<GOAL>(A * C).card * B.card ≤ (A * B).card * (B * C).card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A✝ B✝ C✝ A B C : Finset α<VAR>hB : B.Nonempty<VAR>hB' : B ∈ B.powerset.erase ∅<GOAL>(A * C).card * B.card ≤ (A * B).card * (B * C).card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A✝ B✝ C✝ A B C : Finset α<VAR>hB : B.Nonempty<VAR>hB' : B ∈ B.powerset.erase ∅<VAR>U : Finset α<VAR>hU : U ∈ B.powerset.erase ∅<VAR>hUA : ∀ x' ∈ B.powerset.erase ∅, ↑(U * A).card / ↑U.card ≤ ↑(x' * A).card / ↑x'.card<GOAL>(A * C).card * B.card ≤ (A * B).card * (B * C).card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A✝ B✝ C✝ A B C : Finset α<VAR>hB : B.Nonempty<VAR>hB' : B ∈ B.powerset.erase ∅<VAR>U : Finset α<VAR>hU : U.Nonempty ∧ U ⊆ B<VAR>hUA : ∀ x' ∈ B.powerset.erase ∅, ↑(U * A).card / ↑U.card ≤ ↑(x' * A).card / ↑x'.card<GOAL>(A * C).card * B.card ≤ (A * B).card * (B * C).card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A✝ B✝ C✝ A B C : Finset α<VAR>hB : B.Nonempty<VAR>hB' : B ∈ B.powerset.erase ∅<VAR>U : Finset α<VAR>hU : U.Nonempty ∧ U ⊆ B<VAR>hUA : ∀ x' ∈ B.powerset.erase ∅, ↑(U * A).card / ↑U.card ≤ ↑(x' * A).card / ↑x'.card<GOAL>↑((A * C).card * B.card) ≤ ↑((A * B).card * (B * C).card)
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A✝ B✝ C✝ A B C : Finset α<VAR>hB : B.Nonempty<VAR>hB' : B ∈ B.powerset.erase ∅<VAR>U : Finset α<VAR>hU : U.Nonempty ∧ U ⊆ B<VAR>hUA : ∀ x' ∈ B.powerset.erase ∅, ↑(U * A).card / ↑U.card ≤ ↑(x' * A).card / ↑x'.card<GOAL>↑(A * C).card * ↑B.card ≤ ↑(A * B).card * ↑(B * C).card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A✝ B✝ C✝ A B C : Finset α<VAR>hB : B.Nonempty<VAR>hB' : B ∈ B.powerset.erase ∅<VAR>U : Finset α<VAR>hU : U.Nonempty ∧ U ⊆ B<VAR>hUA : ∀ x' ∈ B.powerset.erase ∅, ↑(U * A).card / ↑U.card ≤ ↑(x' * A).card / ↑x'.card<GOAL>↑(A * C).card ≤ ↑(A * B).card * ↑(B * C).card / ↑B.card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A✝ B✝ C✝ A B C : Finset α<VAR>hB : B.Nonempty<VAR>hB' : B ∈ B.powerset.erase ∅<VAR>U : Finset α<VAR>hU : U.Nonempty ∧ U ⊆ B<VAR>hUA : ∀ x' ∈ B.powerset.erase ∅, ↑(U * A).card / ↑U.card ≤ ↑(x' * A).card / ↑x'.card<GOAL>↑(A * C).card ≤ ↑(B * A).card / ↑B.card * ↑(B * C).card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A✝ B✝ C✝ A B C : Finset α<VAR>hB : B.Nonempty<VAR>hB' : B ∈ B.powerset.erase ∅<VAR>U : Finset α<VAR>hU : U.Nonempty ∧ U ⊆ B<VAR>hUA : ∀ x' ∈ B.powerset.erase ∅, ↑(U * A).card / ↑U.card ≤ ↑(x' * A).card / ↑x'.card<GOAL>↑(U * (A * C)).card ≤ ↑(B * A).card / ↑B.card * ↑(B * C).card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A✝ B✝ C✝ A B C : Finset α<VAR>hB : B.Nonempty<VAR>hB' : B ∈ B.powerset.erase ∅<VAR>U : Finset α<VAR>hU : U.Nonempty ∧ U ⊆ B<VAR>hUA : ∀ x' ∈ B.powerset.erase ∅, ↑(U * A).card / ↑U.card ≤ ↑(x' * A).card / ↑x'.card<GOAL>↑(U * (A * C)).card ≤ ↑(U * A).card / ↑U.card * ↑(U * C).card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A✝ B✝ C✝ A B C : Finset α<VAR>hB : B.Nonempty<VAR>hB' : B ∈ B.powerset.erase ∅<VAR>U : Finset α<VAR>hU : U.Nonempty ∧ U ⊆ B<VAR>hUA : ∀ x' ∈ B.powerset.erase ∅, ↑(U * A).card / ↑U.card ≤ ↑(x' * A).card / ↑x'.card<GOAL>↑(U * A * C).card ≤ ↑(U * A).card * ↑(U * C).card / ↑U.card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A✝ B✝ C✝ A B C : Finset α<VAR>hB : B.Nonempty<VAR>hB' : B ∈ B.powerset.erase ∅<VAR>U : Finset α<VAR>hU : U.Nonempty ∧ U ⊆ B<VAR>hUA : ∀ x' ∈ B.powerset.erase ∅, ↑(U * A).card / ↑U.card ≤ ↑(x' * A).card / ↑x'.card<GOAL>↑(U * A * C).card * ↑U.card ≤ ↑(U * A).card * ↑(U * C).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>inst✝ : Group G<VAR>s✝ t : Set α<VAR>f✝ g : α → G<VAR>a : α<VAR>s : Set α<VAR>f : α → G<GOAL>sᶜ.mulIndicator f = f / s.mulIndicator f
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>ha : a ≠ 0<GOAL>(C b).degree < (C a * X).degree
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : CosimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>j : Fin (n + 1)<VAR>H : j.castSucc < i<GOAL>X.map (SimplexCategory.δ i.succ) ≫ X.map (SimplexCategory.σ j.castSucc) = X.map (SimplexCategory.σ j) ≫ X.map (SimplexCategory.δ i)
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<GOAL>P4 x₁ x₂ y ↔ P4 (-x₂) (-x₁) y
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Zero R<VAR>inst✝¹ : LinearOrder Γ<VAR>inst✝ : LocallyFiniteOrder Γ<VAR>f : Γ → R<VAR>n : Γ<VAR>hn : ∀ m < n, f m = 0<GOAL>∃ x, x ∈ {x | ∀ ⦃a : Γ⦄, a ∈ Function.support f → x ≤ a}
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Zero R<VAR>inst✝¹ : LinearOrder Γ<VAR>inst✝ : LocallyFiniteOrder Γ<VAR>f : Γ → R<VAR>n : Γ<VAR>hn : ∀ m < n, f m = 0<GOAL>n ∈ {x | ∀ ⦃a : Γ⦄, a ∈ Function.support f → x ≤ a}
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Zero R<VAR>inst✝¹ : LinearOrder Γ<VAR>inst✝ : LocallyFiniteOrder Γ<VAR>f : Γ → R<VAR>n : Γ<VAR>hn : ∀ m < n, f m = 0<VAR>m : Γ<VAR>hm : m ∈ Function.support f<GOAL>n ≤ m
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Zero R<VAR>inst✝¹ : LinearOrder Γ<VAR>inst✝ : LocallyFiniteOrder Γ<VAR>f : Γ → R<VAR>n : Γ<VAR>hn : ∀ m < n, f m = 0<VAR>m : Γ<VAR>hm : ¬f m = 0<GOAL>n ≤ m
<VAR>s : Set ℝ<VAR>h₁ : BddBelow s<VAR>h₂ : BddAbove s<GOAL>sInf s ≤ sSup s
<VAR>h₁ : BddBelow ∅<VAR>h₂ : BddAbove ∅<GOAL>sInf ∅ ≤ sSup ∅
<VAR>s : Set ℝ<VAR>h₁ : BddBelow s<VAR>h₂ : BddAbove s<VAR>hne : s.Nonempty<GOAL>sInf s ≤ sSup s
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>hg : HasDerivWithinAt g₁ g₁' s' (h x)<VAR>hh : HasDerivAt h h' x<VAR>hs : ∀ (x : 𝕜), h x ∈ s'<VAR>hy : y = h x<GOAL>HasDerivAt (g₁ ∘ h) (h' • g₁') x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : Group α<VAR>inst✝¹ : UniformGroup α<VAR>inst✝ : UniformSpace β<VAR>f : β → α<VAR>hf : UniformContinuous f<GOAL>UniformContinuous fun x => f x ^ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : Group α<VAR>inst✝¹ : UniformGroup α<VAR>inst✝ : UniformSpace β<VAR>f : β → α<VAR>hf : UniformContinuous f<GOAL>UniformContinuous fun x => 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : Group α<VAR>inst✝¹ : UniformGroup α<VAR>inst✝ : UniformSpace β<VAR>f : β → α<VAR>hf : UniformContinuous f<VAR>n : ℕ<GOAL>UniformContinuous fun x => f x ^ (n + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : Group α<VAR>inst✝¹ : UniformGroup α<VAR>inst✝ : UniformSpace β<VAR>f : β → α<VAR>hf : UniformContinuous f<VAR>n : ℕ<GOAL>UniformContinuous fun x => f x * f x ^ n
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : LinearOrderedCancelAddCommMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>hI : IsHomogeneous 𝒜 I<VAR>I_ne_top : I ≠ ⊤<VAR>homogeneous_mem_or_mem : ∀ {x y : A}, Homogeneous 𝒜 x → Homogeneous 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I<VAR>x y : A<VAR>hxy : x * y ∈ I<GOAL>x ∈ I ∨ y ∈ I
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : LinearOrderedCancelAddCommMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>hI : IsHomogeneous 𝒜 I<VAR>I_ne_top : I ≠ ⊤<VAR>homogeneous_mem_or_mem : ∀ {x y : A}, Homogeneous 𝒜 x → Homogeneous 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I<VAR>x y : A<VAR>hxy : x * y ∈ I<VAR>rid : x ∉ I ∧ y ∉ I<GOAL>False
<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>n : ℕ<VAR>A : Matrix (Fin n.succ) (Fin n.succ) α<VAR>i j : Fin n.succ<GOAL>A.adjugate i j = (-1) ^ (↑j + ↑i) * (A.submatrix j.succAbove i.succAbove).det
<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>n : ℕ<VAR>A : Matrix (Fin n.succ) (Fin n.succ) α<VAR>i j : Fin n.succ<GOAL>∑ x : Fin n.succ, (-1) ^ (↑j + ↑x) * Pi.single i 1 x * (A.submatrix j.succAbove x.succAbove).det = (-1) ^ (↑j + ↑i) * (A.submatrix j.succAbove i.succAbove).det
<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>n : ℕ<VAR>A : Matrix (Fin n.succ) (Fin n.succ) α<VAR>i j h : Fin n.succ<VAR>hjk : h ≠ i<GOAL>(-1) ^ (↑j + ↑h) * Pi.single i 1 h * (A.submatrix j.succAbove h.succAbove).det = 0
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring S<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>α' : Type u_7<VAR>M' : Type u_8<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>v : α → M<VAR>v' : α' → M'<VAR>f : α ≃ α'<VAR>l : α →₀ R<GOAL>(Finsupp.total α' M' R v') (equivMapDomain f l) = (Finsupp.total α M' R (v' ∘ ⇑f)) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<GOAL>ThreeAPFree ↑(image (⇑(map (2 * d - 1))) (sphere n d k))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<GOAL>ThreeAPFree (⇑(map (2 * d - 1)) '' ↑(sphere n d k))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<GOAL>↑(sphere n d k) + ↑(sphere n d k) ⊆ {x | ∀ (i : Fin n), x i < 2 * d - 1}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<GOAL>Fin n → ℕ
<VAR>n✝ m n : ℕ<VAR>hn : n ≠ 0<VAR>hmn : m ∣ n<GOAL>filter (fun x => x ∣ m) n.primeFactors = m.primeFactors
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : StarMul R<VAR>inst✝⁵ : TrivialStar R<VAR>inst✝⁴ : AddCommGroup A<VAR>inst✝³ : Module R A<VAR>inst✝² : StarAddMonoid A<VAR>inst✝¹ : StarModule R A<VAR>inst✝ : Invertible 2<VAR>x : A<GOAL>↑((selfAdjointPart R) x) + ↑((skewAdjointPart R) x) = x
<VAR>d : ℕ<VAR>dnsq : Nonsquare d<VAR>x y : ℕ<VAR>e : (x + 1) * (x + 1) = d * (y + 1) * (y + 1)<GOAL>False
<VAR>d : ℕ<VAR>dnsq : Nonsquare d<VAR>x y : ℕ<VAR>e : (x + 1) * (x + 1) = d * (y + 1) * (y + 1)<VAR>t : x + 1 = 0<GOAL>False
<VAR>n p : ℕ<VAR>inst✝ : Fact (Prime p)<GOAL>p % 2 = 1 ↔ p ≠ 2
<VAR>n p : ℕ<VAR>inst✝ : Fact (Prime p)<VAR>h : p % 2 = 1<VAR>hf : p = 2<GOAL>False
<VAR>α : Type u_1<VAR>f : ℕ → Set α<VAR>n : ℕ<GOAL>(memPartition f n).Finite
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝¹³ : CommRing A<VAR>inst✝¹² : CommRing B<VAR>inst✝¹¹ : Algebra A B<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : Algebra A K<VAR>inst✝⁷ : IsFractionRing A K<VAR>inst✝⁶ : Algebra B L<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : Algebra A L<VAR>inst✝³ : IsScalarTower A B L<VAR>inst✝² : IsScalarTower A K L<VAR>inst✝¹ : IsIntegralClosure B A L<VAR>inst✝ : FiniteDimensional K L<VAR>σ : B →ₐ[A] B<VAR>x : B<GOAL>((galRestrictHom A K L B).symm σ) ((algebraMap B L) x) = (algebraMap B L) (σ x)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝¹³ : CommRing A<VAR>inst✝¹² : CommRing B<VAR>inst✝¹¹ : Algebra A B<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : Algebra A K<VAR>inst✝⁷ : IsFractionRing A K<VAR>inst✝⁶ : Algebra B L<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : Algebra A L<VAR>inst✝³ : IsScalarTower A B L<VAR>inst✝² : IsScalarTower A K L<VAR>inst✝¹ : IsIntegralClosure B A L<VAR>inst✝ : FiniteDimensional K L<VAR>σ : B →ₐ[A] B<VAR>x : B<VAR>this : IsDomain A<GOAL>((galRestrictHom A K L B).symm σ) ((algebraMap B L) x) = (algebraMap B L) (σ x)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝¹³ : CommRing A<VAR>inst✝¹² : CommRing B<VAR>inst✝¹¹ : Algebra A B<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : Algebra A K<VAR>inst✝⁷ : IsFractionRing A K<VAR>inst✝⁶ : Algebra B L<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : Algebra A L<VAR>inst✝³ : IsScalarTower A B L<VAR>inst✝² : IsScalarTower A K L<VAR>inst✝¹ : IsIntegralClosure B A L<VAR>inst✝ : FiniteDimensional K L<VAR>σ : B →ₐ[A] B<VAR>x : B<VAR>this✝ : IsDomain A<VAR>this : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L<GOAL>((galRestrictHom A K L B).symm σ) ((algebraMap B L) x) = (algebraMap B L) (σ x)
<VAR>a : Ordinal.{u_1}<VAR>h : 1 < a<VAR>a0 : 0 < a<VAR>b : Ordinal.{u_1}<GOAL>(fun x => a ^ x) b < (fun x => a ^ x) (succ b)