ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>f✝ : (a : α) → a ∈ p.support → PMF β<VAR>a : α<VAR>f : (a' : α) → a' ∈ (pure a).support → PMF β<VAR>b : β<VAR>a' : α<GOAL>((if a' = a then 1 else 0) * if h : (if a' = a then 1 else 0) = 0 then 0 else (f a' h) b) = if a' = a then (f a ⋯) b else 0
<VAR>K₁ K₂ S : Finset Λ'<GOAL>Supports (K₁ ∪ K₂) S ↔ Supports K₁ S ∧ Supports K₂ S
<VAR>R : Type u<VAR>inst✝¹ : AddMonoid R<VAR>inst✝ : StarAddMonoid R<VAR>x : R<GOAL>star x ≠ 0 ↔ x ≠ 0
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F✝<VAR>F F' : Sheaf J (Type w)<VAR>f : F ⟶ F'<GOAL>Presheaf.IsSheaf J (Subpresheaf.sheafify J (imagePresheaf f.val)).toPresheaf
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F✝<VAR>F F' : Sheaf J (Type w)<VAR>f : F ⟶ F'<GOAL>Presieve.IsSheaf J (Subpresheaf.sheafify J (imagePresheaf f.val)).toPresheaf
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F✝<VAR>F F' : Sheaf J (Type w)<VAR>f : F ⟶ F'<GOAL>Presieve.IsSheaf J F'.val
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F✝<VAR>F F' : Sheaf J (Type w)<VAR>f : F ⟶ F'<GOAL>Presheaf.IsSheaf J F'.val
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hf : Inducing f<VAR>s : Set X<GOAL>IsOpen s ↔ ∃ t, IsOpen t ∧ f ⁻¹' t = s
<VAR>a b c : Prop<GOAL>((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝² : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>U V W X✝ Y✝ Z X Y : C<GOAL>X ◁ (λ_ Y).inv ≫ (α_ X (𝟙_ C) Y).inv = (ρ_ X).inv ▷ Y
<VAR>V : Type u_1<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>P : Type u_2<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c d p : P<VAR>h : Cospherical {a, b, c, d}<VAR>hapb : ∃ k₁, k₁ ≠ 1 ∧ b -ᵥ p = k₁ • (a -ᵥ p)<VAR>hcpd : ∃ k₂, k₂ ≠ 1 ∧ d -ᵥ p = k₂ • (c -ᵥ p)<GOAL>dist a p * dist b p = dist c p * dist d p
<VAR>V : Type u_1<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>P : Type u_2<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c d p : P<VAR>h : Cospherical {a, b, c, d}<VAR>hapb : ∃ k₁, k₁ ≠ 1 ∧ b -ᵥ p = k₁ • (a -ᵥ p)<VAR>hcpd : ∃ k₂, k₂ ≠ 1 ∧ d -ᵥ p = k₂ • (c -ᵥ p)<VAR>q : P<VAR>r : ℝ<VAR>h' : ∀ p ∈ {a, b, c, d}, dist p q = r<GOAL>dist a p * dist b p = dist c p * dist d p
<VAR>V : Type u_1<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>P : Type u_2<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c d p : P<VAR>h : Cospherical {a, b, c, d}<VAR>hapb : ∃ k₁, k₁ ≠ 1 ∧ b -ᵥ p = k₁ • (a -ᵥ p)<VAR>hcpd : ∃ k₂, k₂ ≠ 1 ∧ d -ᵥ p = k₂ • (c -ᵥ p)<VAR>q : P<VAR>r : ℝ<VAR>h' : ∀ p ∈ {a, b, c, d}, dist p q = r<VAR>ha : dist a q = dist b q<VAR>hb : dist b q = r<VAR>hc : dist c q = dist d q<VAR>hd : dist d q = r<GOAL>dist a p * dist b p = dist c p * dist d p
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → PartialOrder (α i)<VAR>f : (i : ι) → α i<VAR>i : ι<VAR>a b : α i<GOAL>update f i '' Ioo a b = Ioo (update f i a) (update f i b)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>b c d : R<VAR>n : ℕ<GOAL>normEDS b c d ↑n = preNormEDS' (b ^ 4) c d n * if Even n then b else 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β<VAR>hf : Bijective f<VAR>s : (i : ι) → κ i → Set α<GOAL>f '' ⋂ i, ⋂ j, s i j = ⋂ i, ⋂ j, f '' s i j
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x : E<VAR>y₁ y₂ : F<GOAL>(fun y => (x, y)) '' [y₁-[𝕜]y₂] = [(x, y₁)-[𝕜](x, y₂)]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x : E<VAR>y₁ y₂ : F<GOAL>(fun x_1 => (x, x_1.1 • y₁ + x_1.2 • y₂)) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1} = (fun p => p.1 • (x, y₁) + p.2 • (x, y₂)) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x : E<VAR>y₁ y₂ : F<VAR>a : 𝕜 × 𝕜<VAR>ha : a ∈ {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}<GOAL>(x, a.1 • y₁ + a.2 • y₂) = a.1 • (x, y₁) + a.2 • (x, y₂)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁹ : CommRing R₁<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>B : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>inst✝³ : AddCommMonoid M'<VAR>inst✝² : AddCommMonoid M''<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>e : M ≃ₗ[R] M'<VAR>x✝¹ : BilinForm R M'<VAR>x✝ y✝ : M<GOAL>(((congr e).symm x✝¹) x✝) y✝ = (((congr e.symm) x✝¹) x✝) y✝
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁹ : CommRing R₁<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>B : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>inst✝³ : AddCommMonoid M'<VAR>inst✝² : AddCommMonoid M''<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>e : M ≃ₗ[R] M'<VAR>x✝¹ : BilinForm R M'<VAR>x✝ y✝ : M<GOAL>(((congr e).symm x✝¹) x✝) y✝ = (x✝¹ (e x✝)) (e y✝)
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>a x y : E<VAR>h : IsLocalMinOn f s a<VAR>hy : y ∈ posTangentConeAt s a<VAR>hy' : -y ∈ posTangentConeAt s a<VAR>hf : ¬DifferentiableWithinAt ℝ f s a<GOAL>(fderivWithin ℝ f s a) y = 0
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>a x y : E<VAR>h : IsLocalMinOn f s a<VAR>hy : y ∈ posTangentConeAt s a<VAR>hy' : -y ∈ posTangentConeAt s a<VAR>hf : ¬DifferentiableWithinAt ℝ f s a<GOAL>0 y = 0
<VAR>α : Type u_1<VAR>p q : α → Bool<VAR>n : Nat<VAR>l : List α<GOAL>countP.go p l n = n + countP.go p l 0
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>J : Type w<VAR>inst✝² : Category.{w', w} J<VAR>F : J ⥤ C<VAR>inst✝¹ : PreservesColimit F G<VAR>inst✝ : HasColimit F<VAR>t : Cocone F<VAR>j✝ : J<GOAL>colimit.ι (F ⋙ G) j✝ ≫ (preservesColimitIso G F).inv ≫ G.map (colimit.desc F t) = colimit.ι (F ⋙ G) j✝ ≫ colimit.desc (F ⋙ G) (G.mapCocone t)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝²⁴ : CommRing R<VAR>inst✝²³ : CommRing S<VAR>inst✝²² : CommRing T<VAR>inst✝²¹ : Algebra R S<VAR>inst✝²⁰ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁹ : Field K<VAR>inst✝¹⁸ : Field L<VAR>inst✝¹⁷ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹⁶ : Fintype ι<VAR>F : Type u_6<VAR>inst✝¹⁵ : Field F<VAR>inst✝¹⁴ : Algebra R L<VAR>inst✝¹³ : Algebra L F<VAR>inst✝¹² : Algebra R F<VAR>inst✝¹¹ : IsScalarTower R L F<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>inst✝¹⁰ : CommRing A<VAR>inst✝⁹ : CommRing B<VAR>inst✝⁸ : Algebra A B<VAR>inst✝⁷ : CommRing C<VAR>inst✝⁶ : Algebra A C<VAR>E : Type z<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra K E<VAR>inst✝³ : Module.Finite K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsAlgClosed E<VAR>b : κ → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Fintype κ<VAR>e : κ ≃ (L →ₐ[K] E)<GOAL>(traceMatrix K b).map ⇑(algebraMap K E) = embeddingsMatrixReindex K E b e * (embeddingsMatrixReindex K E b e)ᵀ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝ : T1Space Y<GOAL>IsProperMap f ↔ Continuous f ∧ IsClosedMap f ∧ Tendsto f (cocompact X) cofinite
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝ : T1Space Y<GOAL>(Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})) ↔ Continuous f ∧ IsClosedMap f ∧ ∀ (x : Y), (f ⁻¹' {x})ᶜ ∈ cocompact X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝ : T1Space Y<VAR>f_cont : Continuous f<VAR>x✝ : IsClosedMap f<VAR>H : ∀ (x : Y), (f ⁻¹' {x})ᶜ ∈ cocompact X<VAR>y : Y<GOAL>IsCompact (f ⁻¹' {y})
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝ : T1Space Y<VAR>f_cont : Continuous f<VAR>x✝ : IsClosedMap f<VAR>H : ∀ (x : Y), (f ⁻¹' {x})ᶜ ∈ cocompact X<VAR>y : Y<VAR>K : Set X<VAR>hK : IsCompact K<VAR>hKy : Kᶜ ⊆ (f ⁻¹' {y})ᶜ<GOAL>IsCompact (f ⁻¹' {y})
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>cs.IsRightDescent w i ↔ ¬cs.IsRightDescent (w * cs.simple i) i
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>cs.length (w * cs.simple i) + 1 = cs.length w ↔ cs.length w = cs.length (w * cs.simple i) + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>𝓕 : Filter ι<VAR>a : α<GOAL>blimsup s cofinite p = {x | {n | p n ∧ x ∈ s n}.Infinite}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>𝓕 : Filter ι<VAR>a : α<GOAL>⋂₀ {a | {x | p x ∧ ¬s x ⊆ a}.Finite} = {x | {n | p n ∧ x ∈ s n}.Infinite}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>𝓕 : Filter ι<VAR>a x : α<GOAL>x ∈ ⋂₀ {a | {x | p x ∧ ¬s x ⊆ a}.Finite} ↔ x ∈ {x | {n | p n ∧ x ∈ s n}.Infinite}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>𝓕 : Filter ι<VAR>a x : α<VAR>h : x ∉ {x | {n | p n ∧ x ∈ s n}.Infinite}<GOAL>x ∉ ⋂₀ {a | {x | p x ∧ ¬s x ⊆ a}.Finite}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>𝓕 : Filter ι<VAR>a x : α<VAR>hx : x ∈ {x | {n | p n ∧ x ∈ s n}.Infinite}<VAR>t : Set α<VAR>h : x ∉ t<GOAL>t ∉ {a | {x | p x ∧ ¬s x ⊆ a}.Finite}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>r : ℝ≥0∞<VAR>inst✝ : Infinite ι<VAR>s : ι → Set α<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<VAR>hr₀ : r ≠ 0<VAR>hr : ∀ (i : ι), r ≤ μ (s i)<GOAL>∃ t, t.Infinite ∧ ∀ ⦃u : Set ι⦄, u ⊆ t → u.Finite → 0 < μ (⋂ i ∈ u, s i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>r : ℝ≥0∞<VAR>inst✝ : Infinite ι<VAR>s : ι → Set α<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<VAR>hr₀ : r ≠ 0<VAR>hr : ∀ (i : ι), r ≤ μ (s i)<VAR>t : Set ℕ<VAR>ht : t.Infinite<VAR>h : ∀ ⦃u : Set ℕ⦄, u ⊆ t → u.Finite → 0 < μ (⋂ n ∈ u, s ((Infinite.natEmbedding ι) n))<GOAL>∃ t, t.Infinite ∧ ∀ ⦃u : Set ι⦄, u ⊆ t → u.Finite → 0 < μ (⋂ i ∈ u, s i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>r : ℝ≥0∞<VAR>inst✝ : Infinite ι<VAR>s : ι → Set α<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<VAR>hr₀ : r ≠ 0<VAR>hr : ∀ (i : ι), r ≤ μ (s i)<VAR>t : Set ℕ<VAR>ht : t.Infinite<VAR>h : ∀ ⦃u : Set ℕ⦄, u ⊆ t → u.Finite → 0 < μ (⋂ n ∈ u, s ((Infinite.natEmbedding ι) n))<VAR>u : Set ι<VAR>hut : u ⊆ ⇑(Infinite.natEmbedding ι) '' t<VAR>hu : u.Finite<VAR>i : ι<VAR>hi : i ∈ u<GOAL>⋂ n ∈ ⇑(Infinite.natEmbedding ι) ⁻¹' u, s ((Infinite.natEmbedding ι) n) ⊆ s i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>r : ℝ≥0∞<VAR>inst✝ : Infinite ι<VAR>s : ι → Set α<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<VAR>hr₀ : r ≠ 0<VAR>hr : ∀ (i : ι), r ≤ μ (s i)<VAR>t : Set ℕ<VAR>ht : t.Infinite<VAR>h : ∀ ⦃u : Set ℕ⦄, u ⊆ t → u.Finite → 0 < μ (⋂ n ∈ u, s ((Infinite.natEmbedding ι) n))<VAR>u : Set ι<VAR>hut : u ⊆ ⇑(Infinite.natEmbedding ι) '' t<VAR>hu : u.Finite<VAR>n : ℕ<VAR>hi : (Infinite.natEmbedding ι) n ∈ u<GOAL>⋂ n ∈ ⇑(Infinite.natEmbedding ι) ⁻¹' u, s ((Infinite.natEmbedding ι) n) ⊆ s ((Infinite.natEmbedding ι) n)
<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 : V<GOAL>-(o.rotation ↑(-π / 2)) x = (o.rotation ↑(π / 2)) x
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Finset ι<GOAL>cylinder s univ = univ
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>p q : Submodule R E<VAR>S : Type u_5<VAR>inst✝² : Semiring S<VAR>M : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module S M<VAR>m : Submodule S M<VAR>h : IsCompl p q<VAR>φ : ↥p →ₗ[R] F<VAR>ψ : ↥q →ₗ[R] F<VAR>χ : E →ₗ[R] F<VAR>hφ : ∀ (u : ↥p), φ u = χ ↑u<VAR>hψ : ∀ (u : ↥q), ψ u = χ ↑u<VAR>x : E<GOAL>(ofIsCompl h φ ψ) x = χ x
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>p q : Submodule R E<VAR>S : Type u_5<VAR>inst✝² : Semiring S<VAR>M : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module S M<VAR>m : Submodule S M<VAR>h : IsCompl p q<VAR>φ : ↥p →ₗ[R] F<VAR>ψ : ↥q →ₗ[R] F<VAR>χ : E →ₗ[R] F<VAR>hφ : ∀ (u : ↥p), φ u = χ ↑u<VAR>hψ : ∀ (u : ↥q), ψ u = χ ↑u<VAR>w✝¹ : ↥p<VAR>w✝ : ↥q<VAR>right✝ : ∀ (r : ↥p) (s : ↥q), ↑r + ↑s = ↑w✝¹ + ↑w✝ → r = w✝¹ ∧ s = w✝<GOAL>(ofIsCompl h φ ψ) (↑w✝¹ + ↑w✝) = χ (↑w✝¹ + ↑w✝)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>G : C<GOAL>IsSeparator G ↔ (preadditiveCoyoneda.obj (op G)).Faithful
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>G : C<GOAL>(preadditiveCoyoneda.obj (op G) ⋙ forget AddCommGrp).Faithful ↔ (preadditiveCoyoneda.obj (op G)).Faithful
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>m : ι → MeasurableSpace α<VAR>S : Set ι<VAR>pt : Finset ι<VAR>hpt : ↑pt ⊆ S<VAR>ft : ι → Set α<VAR>ht_m : ∀ x ∈ pt, ft x ∈ (fun n => {s | MeasurableSet s}) x<GOAL>MeasurableSet (⋂ x ∈ pt, ft x)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>m : ι → MeasurableSpace α<VAR>S : Set ι<VAR>pt : Finset ι<VAR>hpt : ↑pt ⊆ S<VAR>ft : ι → Set α<VAR>ht_m : ∀ x ∈ pt, ft x ∈ (fun n => {s | MeasurableSet s}) x<VAR>i : ι<VAR>hi : i ∈ pt<GOAL>MeasurableSet (ft i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>m : ι → MeasurableSpace α<VAR>S : Set ι<VAR>pt : Finset ι<VAR>hpt : ↑pt ⊆ S<VAR>ft : ι → Set α<VAR>ht_m : ∀ x ∈ pt, ft x ∈ (fun n => {s | MeasurableSet s}) x<VAR>i : ι<VAR>hi : i ∈ pt<VAR>hi' : i ∈ S<GOAL>m i ≤ ⨆ i ∈ S, m i
<VAR>n m : ℕ<VAR>p i : Fin (n + 1)<VAR>h : p ≤ i<VAR>hp : p ≠ 0<VAR>hi : optParam (i ≠ 0) ⋯<GOAL>(p.pred hp).predAbove i = i.pred hi
<VAR>k✝ G✝ : Type u<VAR>inst✝⁷ : CommRing k✝<VAR>inst✝⁶ : Monoid G✝<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝⁵ : CommRing k<VAR>inst✝⁴ : Monoid G<VAR>V : Type u_3<VAR>W : Type u_4<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup W<VAR>inst✝¹ : Module k V<VAR>inst✝ : Module k W<VAR>ρ : G →* V →ₗ[k] V<VAR>σ : G →* W →ₗ[k] W<VAR>f : V →ₗ[k] W<VAR>w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f<VAR>r : MonoidAlgebra k G<VAR>x : V<GOAL>f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) r) x) = (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) r) (f x)
<VAR>k✝ G✝ : Type u<VAR>inst✝⁷ : CommRing k✝<VAR>inst✝⁶ : Monoid G✝<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝⁵ : CommRing k<VAR>inst✝⁴ : Monoid G<VAR>V : Type u_3<VAR>W : Type u_4<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup W<VAR>inst✝¹ : Module k V<VAR>inst✝ : Module k W<VAR>ρ : G →* V →ₗ[k] V<VAR>σ : G →* W →ₗ[k] W<VAR>f : V →ₗ[k] W<VAR>w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f<VAR>r : MonoidAlgebra k G<VAR>x : V<GOAL>∀ (g : G), f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) ((MonoidAlgebra.of k G) g)) x) = (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) ((MonoidAlgebra.of k G) g)) (f x)
<VAR>k✝ G✝ : Type u<VAR>inst✝⁷ : CommRing k✝<VAR>inst✝⁶ : Monoid G✝<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝⁵ : CommRing k<VAR>inst✝⁴ : Monoid G<VAR>V : Type u_3<VAR>W : Type u_4<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup W<VAR>inst✝¹ : Module k V<VAR>inst✝ : Module k W<VAR>ρ : G →* V →ₗ[k] V<VAR>σ : G →* W →ₗ[k] W<VAR>f : V →ₗ[k] W<VAR>w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f<VAR>r : MonoidAlgebra k G<VAR>x : V<GOAL>∀ (f_1 g : MonoidAlgebra k G), f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) f_1) x) = (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) f_1) (f x) → f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) g) x) = (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) g) (f x) → f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) (f_1 + g)) x) = (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) (f_1 + g)) (f x)
<VAR>k✝ G✝ : Type u<VAR>inst✝⁷ : CommRing k✝<VAR>inst✝⁶ : Monoid G✝<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝⁵ : CommRing k<VAR>inst✝⁴ : Monoid G<VAR>V : Type u_3<VAR>W : Type u_4<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup W<VAR>inst✝¹ : Module k V<VAR>inst✝ : Module k W<VAR>ρ : G →* V →ₗ[k] V<VAR>σ : G →* W →ₗ[k] W<VAR>f : V →ₗ[k] W<VAR>w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f<VAR>r : MonoidAlgebra k G<VAR>x : V<GOAL>∀ (r : k) (f_1 : MonoidAlgebra k G), f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) f_1) x) = (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) f_1) (f x) → f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) (r • f_1)) x) = (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) (r • f_1)) (f x)
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>l' : List (Multiset α)<VAR>H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l<GOAL>l'.revzip = List.map (fun x => (x, ↑l - x)) l'
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>l' : List (Multiset α)<VAR>H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l<VAR>this : Forall₂ (fun p s => p = (s, ↑l - s)) l'.revzip (List.map Prod.fst l'.revzip)<GOAL>l'.revzip = List.map (fun x => (x, ↑l - x)) l'
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>l' : List (Multiset α)<VAR>H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l<VAR>this : Forall₂ (fun p s => p = (s, ↑l - s)) l'.revzip (List.map Prod.fst l'.revzip)<GOAL>Forall₂ (fun a c => a = (c, ↑l - c)) l'.revzip l'
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>hw : w ≠ 1<GOAL>∃ i, cs.IsRightDescent w i
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>hw : w ≠ 1<GOAL>∃ i, cs.IsLeftDescent w⁻¹ i
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>hw : w ≠ 1<GOAL>w⁻¹ ≠ 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>s t : Seq α<GOAL>(corec (fun x => match x.1.destruct with | none => match x.2.destruct with | none => none | some (a, b) => some (a, nil, b) | some (a, s₁') => some (a, s₁', x.2)) (cons a s, t)).destruct = some (a, corec (fun x => match x.1.destruct with | none => match x.2.destruct with | none => none | some (a, b) => some (a, nil, b) | some (a, s₁') => some (a, s₁', x.2)) (s, t))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>s t : Seq α<GOAL>omap (corec fun x => match x.1.destruct with | none => match x.2.destruct with | none => none | some (a, b) => some (a, nil, b) | some (a, s₁') => some (a, s₁', x.2)) (match (cons a s, t).1.destruct with | none => match (cons a s, t).2.destruct with | none => none | some (a, b) => some (a, nil, b) | some (a_1, s₁') => some (a_1, s₁', (cons a s, t).2)) = some (a, corec (fun x => match x.1.destruct with | none => match x.2.destruct with | none => none | some (a, b) => some (a, nil, b) | some (a, s₁') => some (a, s₁', x.2)) (s, t))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>s t : Seq α<GOAL>(match match (cons a s).destruct with | none => match t.destruct with | none => none | some (a, b) => some (a, nil, b) | some (a, s₁') => some (a, s₁', t) with | none => none | some (a, b) => some (a, corec (fun x => match x.1.destruct with | none => match x.2.destruct with | none => none | some (a, b) => some (a, nil, b) | some (a, s₁') => some (a, s₁', x.2)) b)) = some (a, corec (fun x => match x.1.destruct with | none => match x.2.destruct with | none => none | some (a, b) => some (a, nil, b) | some (a, s₁') => some (a, s₁', x.2)) (s, t))
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : (𝓞 K)ˣ<GOAL>|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) ↑x)| = 1
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : Archimedean α<VAR>a : α<GOAL>⋃ n, Ioc (a + ↑n) (a + ↑n + 1) = univ
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : Monoid γ<VAR>inst✝ : FunLike F β γ<VAR>s : Finset α<VAR>f g : α → β<VAR>comm_ff : (↑s).Pairwise fun x y => Commute (f x) (f y)<VAR>comm_gg : (↑s).Pairwise fun x y => Commute (g x) (g y)<VAR>comm_gf : (↑s).Pairwise fun x y => Commute (g x) (f y)<GOAL>s.noncommProd (f * g) ⋯ = s.noncommProd f comm_ff * s.noncommProd g comm_gg
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : Monoid γ<VAR>inst✝ : FunLike F β γ<VAR>f g : α → β<VAR>comm_ff : (↑∅).Pairwise fun x y => Commute (f x) (f y)<VAR>comm_gg : (↑∅).Pairwise fun x y => Commute (g x) (g y)<VAR>comm_gf : (↑∅).Pairwise fun x y => Commute (g x) (f y)<GOAL>∅.noncommProd (f * g) ⋯ = ∅.noncommProd f comm_ff * ∅.noncommProd g comm_gg
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : Monoid γ<VAR>inst✝ : FunLike F β γ<VAR>f g : α → β<VAR>x : α<VAR>s : Finset α<VAR>hnmem : x ∉ s<VAR>ih : ∀ (comm_ff : (↑s).Pairwise fun x y => Commute (f x) (f y)) (comm_gg : (↑s).Pairwise fun x y => Commute (g x) (g y)) (comm_gf : (↑s).Pairwise fun x y => Commute (g x) (f y)), s.noncommProd (f * g) ⋯ = s.noncommProd f comm_ff * s.noncommProd g comm_gg<VAR>comm_ff : (↑(cons x s hnmem)).Pairwise fun x y => Commute (f x) (f y)<VAR>comm_gg : (↑(cons x s hnmem)).Pairwise fun x y => Commute (g x) (g y)<VAR>comm_gf : (↑(cons x s hnmem)).Pairwise fun x y => Commute (g x) (f y)<GOAL>(cons x s hnmem).noncommProd (f * g) ⋯ = (cons x s hnmem).noncommProd f comm_ff * (cons x s hnmem).noncommProd g comm_gg