ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : DiscreteTopology β<VAR>hA : VanishingDiam A<VAR>x : ℕ → β<VAR>hx : x ∈ (inducedMap A).fst<VAR>ε : ℝ<VAR>ε_pos : ε > 0<VAR>n : ℕ<VAR>hn : ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε<GOAL>IsOpen (cylinder x n)
<VAR>d : ℕ<VAR>a : ℤ√↑d<VAR>n : ℕ<VAR>ha : a.Nonneg<GOAL>(↑n * a).Nonneg
<VAR>d : ℕ<VAR>a : ℤ√↑d<VAR>n : ℕ<VAR>ha : a.Nonneg<GOAL>(↑↑n * a).Nonneg
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<GOAL>⁅I, N ⊔ N'⁆ = ⁅I, N⁆ ⊔ ⁅I, N'⁆
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>h : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆<GOAL>⁅I, N ⊔ N'⁆ = ⁅I, N⁆ ⊔ ⁅I, N'⁆
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>h : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆<GOAL>⁅I, N ⊔ N'⁆ ≤ ⁅I, N⁆ ⊔ ⁅I, N'⁆
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>h : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆<GOAL>{m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑(⁅I, N⁆ ⊔ ⁅I, N'⁆)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>h✝ : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆<VAR>m : M<VAR>x : ↥I<VAR>n : M<VAR>hn : n ∈ N ⊔ N'<VAR>h : ⁅↑x, ↑⟨n, hn⟩⁆ = m<GOAL>m ∈ ↑(⁅I, N⁆ ⊔ ⁅I, N'⁆)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>h✝ : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆<VAR>m : M<VAR>x : ↥I<VAR>n : M<VAR>hn : n ∈ N ⊔ N'<VAR>h : ⁅↑x, ↑⟨n, hn⟩⁆ = m<GOAL>∃ y ∈ ⁅I, N⁆, ∃ z ∈ ⁅I, N'⁆, y + z = m
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>h✝ : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆<VAR>m : M<VAR>x : ↥I<VAR>n : M<VAR>hn✝ : n ∈ N ⊔ N'<VAR>hn : ∃ y ∈ N, ∃ z ∈ N', y + z = n<VAR>h : ⁅↑x, ↑⟨n, hn✝⟩⁆ = m<GOAL>∃ y ∈ ⁅I, N⁆, ∃ z ∈ ⁅I, N'⁆, y + z = m
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>h✝ : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆<VAR>m : M<VAR>x : ↥I<VAR>n : M<VAR>hn : n ∈ N ⊔ N'<VAR>h : ⁅↑x, ↑⟨n, hn⟩⁆ = m<VAR>n₁ : M<VAR>hn₁ : n₁ ∈ N<VAR>n₂ : M<VAR>hn₂ : n₂ ∈ N'<VAR>hn' : n₁ + n₂ = n<GOAL>∃ y ∈ ⁅I, N⁆, ∃ z ∈ ⁅I, N'⁆, y + z = m
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>h✝ : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆<VAR>m : M<VAR>x : ↥I<VAR>n : M<VAR>hn : n ∈ N ⊔ N'<VAR>h : ⁅↑x, ↑⟨n, hn⟩⁆ = m<VAR>n₁ : M<VAR>hn₁ : n₁ ∈ N<VAR>n₂ : M<VAR>hn₂ : n₂ ∈ N'<VAR>hn' : n₁ + n₂ = n<GOAL>⁅↑x, ↑⟨n₁, hn₁⟩⁆ ∈ ⁅I, N⁆ ∧ ∃ z ∈ ⁅I, N'⁆, ⁅↑x, ↑⟨n₁, hn₁⟩⁆ + z = m
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>h✝ : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆<VAR>m : M<VAR>x : ↥I<VAR>n : M<VAR>hn : n ∈ N ⊔ N'<VAR>h : ⁅↑x, ↑⟨n, hn⟩⁆ = m<VAR>n₁ : M<VAR>hn₁ : n₁ ∈ N<VAR>n₂ : M<VAR>hn₂ : n₂ ∈ N'<VAR>hn' : n₁ + n₂ = n<GOAL>∃ z ∈ ⁅I, N'⁆, ⁅↑x, ↑⟨n₁, hn₁⟩⁆ + z = m
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>h✝ : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆<VAR>m : M<VAR>x : ↥I<VAR>n : M<VAR>hn : n ∈ N ⊔ N'<VAR>h : ⁅↑x, ↑⟨n, hn⟩⁆ = m<VAR>n₁ : M<VAR>hn₁ : n₁ ∈ N<VAR>n₂ : M<VAR>hn₂ : n₂ ∈ N'<VAR>hn' : n₁ + n₂ = n<GOAL>⁅↑x, ↑⟨n₂, hn₂⟩⁆ ∈ ⁅I, N'⁆ ∧ ⁅↑x, ↑⟨n₁, hn₁⟩⁆ + ⁅↑x, ↑⟨n₂, hn₂⟩⁆ = m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t : Set α<VAR>hf : EqOn f 1 s<GOAL>∏ᶠ (i : α) (_ : i ∈ s), f i = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t : Set α<VAR>hf : EqOn f 1 s<GOAL>∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (i : α) (_ : i ∈ s), 1
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>hp : p.coeff 0 = 0<GOAL>p.nextCoeffUp = p.coeff (p.natTrailingDegree + 1)
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>hp : coeff 0 0 = 0<GOAL>nextCoeffUp 0 = coeff 0 (natTrailingDegree 0 + 1)
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>hp : p.coeff 0 = 0<VAR>hp₀ : p ≠ 0<GOAL>p.nextCoeffUp = p.coeff (p.natTrailingDegree + 1)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>s : Set (X × X)<VAR>x : X<VAR>hx : s ∈ 𝓝 (x, x)<GOAL>∃ U, IsOpen U ∧ x ∈ U ∧ U ×ˢ U ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : EDist α<VAR>x y : α<VAR>s : Set α<GOAL>s.infsep = 0 ↔ s.einfsep = 0 ∨ s.einfsep = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : MulOneClass M<VAR>inst✝² : MulOneClass N<VAR>inst✝¹ : MulOneClass P<VAR>S : Submonoid M<VAR>A : Type u_4<VAR>inst✝ : SetLike A M<VAR>hA : SubmonoidClass A M<VAR>S' : A<GOAL>(∀ (x : M), x ∈ S ↔ x ∈ ⊥) ↔ ∀ x ∈ S, x = 1
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => a - x) '' Icc b c = Icc (a - c) (a - b)
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<VAR>this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)<GOAL>(fun x => a - x) '' Icc b c = Icc (a - c) (a - b)
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<VAR>this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)<GOAL>(fun x => a - x) '' Icc b c = Icc (a - c) (a - b)
<VAR>ι✝ : Sort u_1<VAR>f✝ g : ι✝ → ℝ≥0∞<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>ι : Sort u_2<VAR>inst✝ : Nonempty ι<VAR>f : ι → ℝ≥0∞<VAR>x : ℝ≥0∞<VAR>h : x ≠ ⊤<GOAL>x * iInf f = ⨅ i, x * f i
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a✝ a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>s : Finset ι<VAR>f a : ι → E<VAR>d : ι → ℝ<VAR>h : ∀ b ∈ s, dist (f b) (a b) ≤ d b<GOAL>dist (∏ b ∈ s, f b) (∏ b ∈ s, a b) ≤ ∑ b ∈ s, d b
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a✝ a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>s : Finset ι<VAR>f a : ι → E<VAR>d : ι → ℝ<VAR>h : ∀ b ∈ s, ‖f b / a b‖ ≤ d b<GOAL>‖∏ x ∈ s, f x / a x‖ ≤ ∑ b ∈ s, d b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ : α<VAR>n : ℕ<VAR>a : α<GOAL>fract (↑n + a) = fract a
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>A : SL(2, R)<GOAL>det ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]] = 1
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>A : SL(2, R)<GOAL>![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]] 1 1 * ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]] 0 0 - ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]] 0 1 * ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]] 1 0 = 1
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>A : SL(2, R)<GOAL>↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0 = 1
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>A : SL(2, R)<VAR>this : (↑A).det = 1<GOAL>↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0 = 1
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>A : SL(2, R)<VAR>this : ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0 = 1<GOAL>↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0 = 1
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i j : N<VAR>f g : ↑(Ω^ N X x)<GOAL>⟦transAt i f g⟧ = ⟦transAt j f g⟧
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i j : N<VAR>f g : ↑(Ω^ N X x)<GOAL>⟦fromLoop i (Path.trans (toLoop i f) (toLoop i g))⟧ = ⟦fromLoop j (Path.trans (toLoop j f) (toLoop j g))⟧
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i j : N<VAR>f g : ↑(Ω^ N X x)<VAR>m : (G : Type ?u.630838) → Group G → G → G → G := fun G x x_1 x_2 => x_1 * x_2<GOAL>⟦fromLoop i (Path.trans (toLoop i f) (toLoop i g))⟧ = ⟦fromLoop j (Path.trans (toLoop j f) (toLoop j g))⟧
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>v : E<VAR>U : Set E<VAR>hU : U ∈ p.basisSets<GOAL>∀ᶠ (x : 𝕜) in 𝓝 0, x • v ∈ U
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>v : E<VAR>U : Set E<VAR>hU✝ : U ∈ p.basisSets<VAR>s : Finset ι<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hU : U = (s.sup p).ball 0 r<GOAL>∀ᶠ (x : 𝕜) in 𝓝 0, x • v ∈ U
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>v : E<VAR>U : Set E<VAR>hU✝ : U ∈ p.basisSets<VAR>s : Finset ι<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hU : U = (s.sup p).ball 0 r<GOAL>{x | x • v ∈ (s.sup p).ball 0 r} ∈ 𝓝 0
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>v : E<VAR>U : Set E<VAR>hU✝ : U ∈ p.basisSets<VAR>s : Finset ι<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hU : U = (s.sup p).ball 0 r<GOAL>{x | ‖x‖ * (s.sup p) v < r} ∈ 𝓝 0
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>v : E<VAR>U : Set E<VAR>hU✝ : U ∈ p.basisSets<VAR>s : Finset ι<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hU : U = (s.sup p).ball 0 r<VAR>h : ¬0 < (s.sup p) v<GOAL>{x | ‖x‖ * (s.sup p) v < r} ∈ 𝓝 0
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>v : E<VAR>U : Set E<VAR>hU✝ : U ∈ p.basisSets<VAR>s : Finset ι<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hU : U = (s.sup p).ball 0 r<VAR>h : ¬0 < (s.sup p) v<GOAL>{x | True} ∈ 𝓝 0
<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>k : Type u_7<VAR>R : Type u_8<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : OrderedCommMonoid N<VAR>f : M → N<VAR>p : M → Prop<VAR>h_one : f 1 = 1<VAR>h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y<VAR>hp_mul : ∀ (x y : M), p x → p y → p (x * y)<VAR>g : ι → M<VAR>s : Finset ι<VAR>hs : ∀ i ∈ s, p (g i)<GOAL>f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)
<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>k : Type u_7<VAR>R : Type u_8<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : OrderedCommMonoid N<VAR>f : M → N<VAR>p : M → Prop<VAR>h_one : f 1 = 1<VAR>h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y<VAR>hp_mul : ∀ (x y : M), p x → p y → p (x * y)<VAR>g : ι → M<VAR>hs : ∀ i ∈ ∅, p (g i)<GOAL>f (∏ i ∈ ∅, g i) ≤ ∏ i ∈ ∅, f (g i)
<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>k : Type u_7<VAR>R : Type u_8<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : OrderedCommMonoid N<VAR>f : M → N<VAR>p : M → Prop<VAR>h_one : f 1 = 1<VAR>h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y<VAR>hp_mul : ∀ (x y : M), p x → p y → p (x * y)<VAR>g : ι → M<VAR>s : Finset ι<VAR>hs : ∀ i ∈ s, p (g i)<VAR>hs_nonempty : s.Nonempty<GOAL>f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)
<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₂ : P<VAR>x : P × P × P<VAR>hx12 : x.1 ≠ x.2.1<VAR>hx32 : x.2.2 ≠ x.2.1<VAR>f : P × P × P → V × V := fun y => (y.1 -ᵥ y.2.1, y.2.2 -ᵥ y.2.1)<VAR>hf1 : (f x).1 ≠ 0<VAR>hf2 : (f x).2 ≠ 0<GOAL>ContinuousAt (fun y => ∠ y.1 y.2.1 y.2.2) x
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a b c d : G₀<VAR>m n : ℕ<GOAL>a / b = 0 ↔ a = 0 ∨ b = 0
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x y : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>hr : Valid' (↑y) r o₂<VAR>s : ℕ<VAR>ml : Ordnode α<VAR>z : α<VAR>mr : Ordnode α<VAR>hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y<VAR>Hm : 0 < (Ordnode.node s ml z mr).size<VAR>H : l.size = 0 ∧ (Ordnode.node s ml z mr).size = 1 ∧ r.size ≤ 1 ∨ 0 < l.size ∧ ratio * r.size ≤ (Ordnode.node s ml z mr).size ∧ delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size ∧ 3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9 ∧ (Ordnode.node s ml z mr).size ≤ delta * r.size<GOAL>Valid' o₁ (l.node4L x (Ordnode.node s ml z mr) y r) o₂
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x y : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>hr : Valid' (↑y) r o₂<VAR>s : ℕ<VAR>ml : Ordnode α<VAR>z : α<VAR>mr : Ordnode α<VAR>hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y<VAR>Hm : 0 < (Ordnode.node s ml z mr).size<VAR>H : l.size = 0 ∧ (Ordnode.node s ml z mr).size = 1 ∧ r.size ≤ 1 ∨ 0 < l.size ∧ ratio * r.size ≤ (Ordnode.node s ml z mr).size ∧ delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size ∧ 3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9 ∧ (Ordnode.node s ml z mr).size ≤ delta * r.size<GOAL>BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
<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>s t : Set E<VAR>x y : E<GOAL>((convexHull 𝕜) s).Nonempty ↔ s.Nonempty
<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>s t : Set E<VAR>x y : E<GOAL>¬(convexHull 𝕜) s = ∅ ↔ ¬s = ∅
<VAR>R : Type u_1<VAR>inst✝³ : NonAssocRing R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : BinomialRing R<VAR>inst✝ : NatPowAssoc R<VAR>n : ℕ<GOAL>multichoose (-↑n) (n + 1) = 0
<VAR>R : Type u_1<VAR>inst✝³ : NonAssocRing R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : BinomialRing R<VAR>inst✝ : NatPowAssoc R<VAR>n : ℕ<GOAL>(fun x => (n + 1).factorial • x) (multichoose (-↑n) (n + 1)) = (fun x => (n + 1).factorial • x) 0
<VAR>R : Type u_1<VAR>inst✝³ : NonAssocRing R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : BinomialRing R<VAR>inst✝ : NatPowAssoc R<VAR>n : ℕ<GOAL>(n + 1).factorial • multichoose (-↑n) (n + 1) = 0
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<GOAL>(pderiv 0) (X 1 ^ 2 * X 2 + C W.a₁ * X 0 * X 1 * X 2 + C W.a₃ * X 1 * X 2 ^ 2 - (X 0 ^ 3 + C W.a₂ * X 0 ^ 2 * X 2 + C W.a₄ * X 0 * X 2 ^ 2 + C W.a₆ * X 2 ^ 3)) = C W.a₁ * X 1 * X 2 - (C 3 * X 0 ^ 2 + C (2 * W.a₂) * X 0 * X 2 + C W.a₄ * X 2 ^ 2)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<GOAL>↑2 * X 1 ^ (2 - 1) * 0 * X 2 + X 1 ^ 2 * 0 + (((0 * X 0 + C W.a₁ * 1) * X 1 + C W.a₁ * X 0 * 0) * X 2 + C W.a₁ * X 0 * X 1 * 0) + ((0 * X 1 + C W.a₃ * 0) * X 2 ^ 2 + C W.a₃ * X 1 * (↑2 * X 2 ^ (2 - 1) * 0)) - (↑3 * X 0 ^ (3 - 1) * 1 + ((0 * X 0 ^ 2 + C W.a₂ * (↑2 * X 0 ^ (2 - 1) * 1)) * X 2 + C W.a₂ * X 0 ^ 2 * 0) + ((0 * X 0 + C W.a₄ * 1) * X 2 ^ 2 + C W.a₄ * X 0 * (↑2 * X 2 ^ (2 - 1) * 0)) + (0 * X 2 ^ 3 + C W.a₆ * (↑3 * X 2 ^ (3 - 1) * 0))) = C W.a₁ * X 1 * X 2 - (3 * X 0 ^ 2 + 2 * C W.a₂ * X 0 * X 2 + C W.a₄ * X 2 ^ 2)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w : ι → k<VAR>p : ι → P<VAR>b : P<VAR>pred : ι → Prop<VAR>inst✝ : DecidablePred pred<VAR>h : ∀ i ∈ s, w i ≠ 0 → pred i<GOAL>((filter pred s).weightedVSubOfPoint p b) w = (s.weightedVSubOfPoint p b) w
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w : ι → k<VAR>p : ι → P<VAR>b : P<VAR>pred : ι → Prop<VAR>inst✝ : DecidablePred pred<VAR>h : ∀ i ∈ s, w i ≠ 0 → pred i<GOAL>∀ x ∈ s, w x • (p x -ᵥ b) ≠ 0 → pred x
<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✝² : Monoid G<VAR>x : G<VAR>n : ℕ<VAR>inst✝¹ : Fintype G<VAR>inst✝ : DecidableEq G<VAR>hn : n ≠ 0<VAR>x✝ : ℕ<VAR>a✝² : x✝ ∈ Finset.filter (fun x => x ∣ n) (Finset.range n.succ)<VAR>y✝ : ℕ<VAR>a✝¹ : y✝ ∈ Finset.filter (fun x => x ∣ n) (Finset.range n.succ)<VAR>a✝ : x✝ ≠ y✝<GOAL>Disjoint (Finset.filter (fun x => orderOf x = x✝) Finset.univ) (Finset.filter (fun x => orderOf x = y✝) Finset.univ)
<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✝² : Monoid G<VAR>x : G<VAR>n : ℕ<VAR>inst✝¹ : Fintype G<VAR>inst✝ : DecidableEq G<VAR>hn : n ≠ 0<VAR>x✝ : ℕ<VAR>a✝² : x✝ ∈ Finset.filter (fun x => x ∣ n) (Finset.range n.succ)<VAR>y✝ : ℕ<VAR>a✝¹ : y✝ ∈ Finset.filter (fun x => x ∣ n) (Finset.range n.succ)<VAR>a✝ : x✝ ≠ y✝<GOAL>∀ x ∈ Finset.univ, orderOf x = x✝ → ¬orderOf x = y✝
<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✝² : Monoid G<VAR>x✝ : G<VAR>n : ℕ<VAR>inst✝¹ : Fintype G<VAR>inst✝ : DecidableEq G<VAR>hn : n ≠ 0<VAR>x : G<GOAL>(x ∈ (Finset.filter (fun x => x ∣ n) (Finset.range n.succ)).biUnion fun m => Finset.filter (fun x => orderOf x = m) Finset.univ) ↔ x ∈ Finset.filter (fun x => x ^ n = 1) Finset.univ
<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✝² : Monoid G<VAR>x✝ : G<VAR>n : ℕ<VAR>inst✝¹ : Fintype G<VAR>inst✝ : DecidableEq G<VAR>hn : n ≠ 0<VAR>x : G<GOAL>orderOf x ≤ n ∧ orderOf x ∣ n ↔ x ^ n = 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>l : List α<GOAL>(a :: l).sublists' ~ l.sublists ++ map (cons a) l.sublists
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>l : List α<GOAL>l.sublists' ++ map (cons a) l.sublists' ~ l.sublists ++ map (cons a) l.sublists
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n p : R<VAR>k a b : ℕ<VAR>hab : a.Coprime b<GOAL>Finset.filter IsPrimePow (a * b).divisors = Finset.filter IsPrimePow (a.divisors ∪ b.divisors)
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n p : R<VAR>k b : ℕ<VAR>hab : Coprime 0 b<GOAL>Finset.filter IsPrimePow (0 * b).divisors = Finset.filter IsPrimePow (divisors 0 ∪ b.divisors)
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n p : R<VAR>k a b : ℕ<VAR>hab : a.Coprime b<VAR>ha : a ≠ 0<GOAL>Finset.filter IsPrimePow (a * b).divisors = Finset.filter IsPrimePow (a.divisors ∪ b.divisors)
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n p : R<VAR>k a : ℕ<VAR>ha : a ≠ 0<VAR>hab : a.Coprime 0<GOAL>Finset.filter IsPrimePow (a * 0).divisors = Finset.filter IsPrimePow (a.divisors ∪ divisors 0)