ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<VAR>lastr : a.r (last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>hδ2 : δ ≤ 1<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>ah : Pairwise fun i j => a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j<VAR>δnonneg : 0 ≤ δ<VAR>D : 0 ≤ 1 - δ / 4<VAR>τpos : 0 < τ<VAR>I : (1 - δ / 4) * τ ≤ 1<VAR>J : 1 - δ ≤ 1 - δ / 4<VAR>K : 1 - δ / 4 ≤ τ⁻¹<GOAL>τ⁻¹ ≤ ‖a.c i - a.c j‖
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<VAR>lastr : a.r (last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>hδ2 : δ ≤ 1<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>ah : Pairwise fun i j => a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j<VAR>δnonneg : 0 ≤ δ<VAR>D : 0 ≤ 1 - δ / 4<VAR>τpos : 0 < τ<VAR>I : (1 - δ / 4) * τ ≤ 1<VAR>J : 1 - δ ≤ 1 - δ / 4<VAR>K : 1 - δ / 4 ≤ τ⁻¹<VAR>hτ' : ∀ (k : Fin N.succ), τ⁻¹ ≤ a.r k<GOAL>τ⁻¹ ≤ ‖a.c i - a.c j‖
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>a b : ZMod n<VAR>h : n ≤ a.val + b.val<GOAL>(a + b).val = a.val + b.val - n
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>a b : ZMod n<VAR>h : n ≤ a.val + b.val<GOAL>(a + b).val = (a + b).val + n - n
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>M N : Mon_ C<GOAL>(M.X ⊗ N.X) ◁ (λ_ (𝟙_ C)).inv ≫ (M.X ⊗ N.X) ◁ (M.one ⊗ N.one) ≫ tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul) = (ρ_ (M.X ⊗ N.X)).hom
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>M N : Mon_ C<GOAL>(M.X ⊗ N.X) ◁ (λ_ (𝟙_ C)).inv ≫ (tensor_μ C (M.X, N.X) (𝟙_ C, 𝟙_ C) ≫ (M.X ◁ M.one ⊗ N.X ◁ N.one)) ≫ (M.mul ⊗ N.mul) = (ρ_ (M.X ⊗ N.X)).hom
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>M N : Mon_ C<GOAL>(M.X ⊗ N.X) ◁ (λ_ (𝟙_ C)).inv ≫ tensor_μ C (M.X, N.X) (𝟙_ C, 𝟙_ C) ≫ ((ρ_ M.X).hom ⊗ (ρ_ N.X).hom) = (ρ_ (M.X ⊗ N.X)).hom
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>M N : Mon_ C<GOAL>(ρ_ (M.X ⊗ N.X)).hom = (M.X ⊗ N.X) ◁ (λ_ (𝟙_ C)).inv ≫ tensor_μ C (M.X, N.X) (𝟙_ C, 𝟙_ C) ≫ ((ρ_ M.X).hom ⊗ (ρ_ N.X).hom)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddZeroClass M<VAR>p : (α →₀ M) → Prop<VAR>f✝ : α →₀ M<VAR>h0 : p 0<VAR>ha : ∀ (a : α) (b : M) (f : α →₀ M), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)<VAR>s : Finset α<VAR>f : α →₀ M<VAR>hf : f.support = ∅<GOAL>p f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddZeroClass M<VAR>p : (α →₀ M) → Prop<VAR>f✝ : α →₀ M<VAR>h0 : p 0<VAR>ha : ∀ (a : α) (b : M) (f : α →₀ M), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)<VAR>s✝ : Finset α<VAR>a : α<VAR>s : Finset α<VAR>has : a ∉ s<VAR>ih : ∀ (f : α →₀ M), f.support = s → p f<VAR>f : α →₀ M<VAR>hf : f.support = cons a s has<GOAL>p f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddZeroClass M<VAR>p : (α →₀ M) → Prop<VAR>f✝ : α →₀ M<VAR>h0 : p 0<VAR>ha : ∀ (a : α) (b : M) (f : α →₀ M), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)<VAR>s✝ : Finset α<VAR>a : α<VAR>s : Finset α<VAR>has : a ∉ s<VAR>ih : ∀ (f : α →₀ M), f.support = s → p f<VAR>f : α →₀ M<VAR>hf : f.support = cons a s has<GOAL>p (single a (f a) + erase a f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>hl : l.Subsingleton<GOAL>l.IsCountablyGenerated
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>hl : ⊥.Subsingleton<GOAL>⊥.IsCountablyGenerated
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α<VAR>hl : (pure x).Subsingleton<GOAL>(pure x).IsCountablyGenerated
<VAR>α : Type u_1<VAR>inst✝ : CommMonoid α<VAR>x y : α<VAR>H : IsRelPrime x y<VAR>hy : IsPrimal y<VAR>w : α<VAR>H2 : y ∣ x * w<GOAL>x * y ∣ x * w
<VAR>C✝ : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C✝<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C✝ ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>P : Cᵒᵖ ⥤ Type v₁<VAR>I : Type v₁<VAR>inst✝ : SmallCategory I<VAR>F : I ⥤ C<VAR>c : Cocone (F ⋙ yoneda)<VAR>hc : IsColimit c<GOAL>(c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt).Final
<VAR>C✝ : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C✝<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C✝ ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>P : Cᵒᵖ ⥤ Type v₁<VAR>I : Type v₁<VAR>inst✝ : SmallCategory I<VAR>F : I ⥤ C<VAR>c : Cocone (F ⋙ yoneda)<VAR>hc : IsColimit c<GOAL>IsTerminal (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ yoneda))
<VAR>C✝ : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C✝<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C✝ ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>P : Cᵒᵖ ⥤ Type v₁<VAR>I : Type v₁<VAR>inst✝ : SmallCategory I<VAR>F : I ⥤ C<VAR>c : Cocone (F ⋙ yoneda)<VAR>hc : IsColimit c<VAR>isc : IsColimit ((Over.forget c.pt).mapCocone (colimit.cocone ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))) := PreservesColimit.preserves (colimit.isColimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))<GOAL>Over.mk (𝟙 c.pt) ≅ colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁷ : TopologicalSpace H<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : TopologicalSpace H'<VAR>inst✝³ : TopologicalSpace M'<VAR>inst✝² : ChartedSpace H' M'<VAR>inst✝¹ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x✝ : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG✝ : G.LocalInvariantProp G' P<VAR>inst✝ : HasGroupoid M G<VAR>x : H<VAR>hG : G.LocalInvariantProp G Q<VAR>hQ : ∀ (y : H), Q id univ y<VAR>he : e ∈ maximalAtlas M G<VAR>hx : x ∈ e.target<GOAL>LiftPropAt Q (↑e.symm) x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁷ : TopologicalSpace H<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : TopologicalSpace H'<VAR>inst✝³ : TopologicalSpace M'<VAR>inst✝² : ChartedSpace H' M'<VAR>inst✝¹ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x✝ : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG✝ : G.LocalInvariantProp G' P<VAR>inst✝ : HasGroupoid M G<VAR>x : H<VAR>hG : G.LocalInvariantProp G Q<VAR>hQ : ∀ (y : H), Q id univ y<VAR>he : e ∈ maximalAtlas M G<VAR>hx : x ∈ e.target<GOAL>Q (↑e ∘ ↑e.symm) univ x
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : Fintype V<VAR>inst✝ : NonAssocSemiring α<VAR>v : V<VAR>vec : V → α<GOAL>(adjMatrix α G *ᵥ vec) v = ∑ u ∈ G.neighborFinset v, vec u
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁ l₂ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>b : β a<VAR>l : List (Sigma β)<VAR>nd : l.NodupKeys<VAR>h : ⟨a, b⟩ ∈ l<GOAL>b ∈ dlookup a l
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁ l₂ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>b : β a<VAR>l : List (Sigma β)<VAR>nd : l.NodupKeys<VAR>h : ⟨a, b⟩ ∈ l<VAR>b' : β ⟨a, b⟩.fst<VAR>h' : dlookup ⟨a, b⟩.fst l = some b'<GOAL>b ∈ dlookup a l
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁ l₂ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>b : β a<VAR>l : List (Sigma β)<VAR>nd : l.NodupKeys<VAR>h : ⟨a, b⟩ ∈ l<VAR>h' : dlookup ⟨a, b⟩.fst l = some b<GOAL>b ∈ dlookup a l
<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>c : E<VAR>f : α → E<VAR>hf✝ : AEStronglyMeasurable f μ<VAR>s : Set α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>g : α → E<VAR>hs : MeasurableSet s<VAR>hf : Memℒp f p (μ.restrict s)<VAR>hg : Memℒp g p (μ.restrict sᶜ)<VAR>hp_zero : ¬p = 0<GOAL>Memℒp (s.piecewise f g) p μ
<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>c : E<VAR>f : α → E<VAR>hf✝ : AEStronglyMeasurable f μ<VAR>s : Set α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>g : α → E<VAR>hs : MeasurableSet s<VAR>hf : Memℒp f p (μ.restrict s)<VAR>hg : Memℒp g p (μ.restrict sᶜ)<VAR>hp_zero : ¬p = 0<GOAL>eLpNorm (s.piecewise f g) p μ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>c : E<VAR>f : α → E<VAR>hf✝ : AEStronglyMeasurable f μ<VAR>s : Set α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>g : α → E<VAR>hs : MeasurableSet s<VAR>hf : Memℒp f ⊤ (μ.restrict s)<VAR>hg : Memℒp g ⊤ (μ.restrict sᶜ)<VAR>hp_zero : ¬⊤ = 0<GOAL>eLpNorm (s.piecewise f g) ⊤ μ < ⊤
<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>c : E<VAR>f : α → E<VAR>hf✝ : AEStronglyMeasurable f μ<VAR>s : Set α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>g : α → E<VAR>hs : MeasurableSet s<VAR>hf : Memℒp f p (μ.restrict s)<VAR>hg : Memℒp g p (μ.restrict sᶜ)<VAR>hp_zero : ¬p = 0<VAR>hp_top : p ≠ ⊤<GOAL>eLpNorm (s.piecewise f g) p μ < ⊤
<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>c : E<VAR>f : α → E<VAR>hf✝ : AEStronglyMeasurable f μ<VAR>s : Set α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>g : α → E<VAR>hs : MeasurableSet s<VAR>hf : Memℒp f p (μ.restrict s)<VAR>hg : Memℒp g p (μ.restrict sᶜ)<VAR>hp_zero : ¬p = 0<VAR>hp_top : p ≠ ⊤<GOAL>∫⁻ (x : α) in s, ↑‖s.piecewise f g x‖₊ ^ p.toReal ∂μ < ⊤ ∧ ∫⁻ (x : α) in sᶜ, ↑‖s.piecewise f g x‖₊ ^ p.toReal ∂μ < ⊤
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<GOAL>W.addY P Q = addU P Q ^ 3
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s : ConvexCone ℝ E<VAR>f : E →ₗ.[ℝ] ℝ<VAR>nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x<VAR>dense : ∀ (y : E), ∃ x, ↑x + y ∈ s<GOAL>∃ g, (∀ (x : ↥f.domain), g ↑x = ↑f x) ∧ ∀ x ∈ s, 0 ≤ g x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s : ConvexCone ℝ E<VAR>f : E →ₗ.[ℝ] ℝ<VAR>nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x<VAR>dense : ∀ (y : E), ∃ x, ↑x + y ∈ s<VAR>g : ↥⊤ →ₗ[ℝ] ℝ<VAR>hfg : ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥{ domain := ⊤, toFun := g }.domain⦄, ↑x = ↑y → ↑f x = ↑{ domain := ⊤, toFun := g } y<VAR>hgs : ∀ (x : ↥{ domain := ⊤, toFun := g }.domain), ↑x ∈ s → 0 ≤ ↑{ domain := ⊤, toFun := g } x<GOAL>∃ g, (∀ (x : ↥f.domain), g ↑x = ↑f x) ∧ ∀ x ∈ s, 0 ≤ g x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s : ConvexCone ℝ E<VAR>f : E →ₗ.[ℝ] ℝ<VAR>nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x<VAR>dense : ∀ (y : E), ∃ x, ↑x + y ∈ s<VAR>g : ↥⊤ →ₗ[ℝ] ℝ<VAR>hfg : ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥{ domain := ⊤, toFun := g }.domain⦄, ↑x = ↑y → ↑f x = ↑{ domain := ⊤, toFun := g } y<VAR>hgs : ∀ (x : ↥{ domain := ⊤, toFun := g }.domain), ↑x ∈ s → 0 ≤ ↑{ domain := ⊤, toFun := g } x<GOAL>∀ (x : ↥f.domain), (g ∘ₗ LinearMap.codRestrict ⊤ LinearMap.id ⋯) ↑x = ↑f x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s : ConvexCone ℝ E<VAR>f : E →ₗ.[ℝ] ℝ<VAR>nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x<VAR>dense : ∀ (y : E), ∃ x, ↑x + y ∈ s<VAR>g : ↥⊤ →ₗ[ℝ] ℝ<VAR>hfg : ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥{ domain := ⊤, toFun := g }.domain⦄, ↑x = ↑y → ↑f x = ↑{ domain := ⊤, toFun := g } y<VAR>hgs : ∀ (x : ↥{ domain := ⊤, toFun := g }.domain), ↑x ∈ s → 0 ≤ ↑{ domain := ⊤, toFun := g } x<GOAL>∀ x ∈ s, 0 ≤ (g ∘ₗ LinearMap.codRestrict ⊤ LinearMap.id ⋯) x
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>inst✝⁴ : AddCommMonoid M₄<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module R M₃<VAR>inst✝ : Module R M₄<VAR>s : Set M<VAR>t : Set M₂<GOAL>span R (⇑(inl R M M₂) '' s ∪ ⇑(inr R M M₂) '' t) = (span R s).prod (span R t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>s : Set α<VAR>hs : Dense s<GOAL>inst✝³ = generateFrom (Ioi '' s ∪ Iio '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>s : Set α<VAR>hs : Dense s<GOAL>generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a} = generateFrom (Ioi '' s ∪ Iio '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>s : Set α<VAR>hs : Dense s<GOAL>Ioi '' s ∪ Iio '' s ⊆ {s | ∃ a, s = Ioi a ∨ s = Iio a}
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>s : Set α<VAR>hs : Dense s<GOAL>∀ s_1 ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}, IsOpen s_1
<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>A : Matrix n n α<VAR>b : n → α<VAR>inst✝ : Nontrivial n<VAR>i j : n<GOAL>(cramer 0 ∘ₗ LinearMap.single i) 1 j = (0 ∘ₗ LinearMap.single i) 1 j
<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>A : Matrix n n α<VAR>b : n → α<VAR>inst✝ : Nontrivial n<VAR>i j j' : n<VAR>hj' : j' ≠ j<GOAL>(cramer 0 ∘ₗ LinearMap.single i) 1 j = (0 ∘ₗ LinearMap.single i) 1 j
<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>A : Matrix n n α<VAR>b : n → α<VAR>inst✝ : Nontrivial n<VAR>i j j' : n<VAR>hj' : j' ≠ j<GOAL>∀ (i_1 : n), updateColumn 0 j ((LinearMap.single i) 1) i_1 j' = 0
<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>A : Matrix n n α<VAR>b : n → α<VAR>inst✝ : Nontrivial n<VAR>i j j' : n<VAR>hj' : j' ≠ j<VAR>j'' : n<GOAL>updateColumn 0 j ((LinearMap.single i) 1) j'' j' = 0
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>p : l₁ ~ l₂<GOAL>l₁.length = l₂.length
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>r : R<GOAL>r ∣ p.content ↔ C r ∣ p
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>r : R<GOAL>r ∣ p.content ↔ ∀ (i : ℕ), r ∣ p.coeff i
<VAR>X Y B : Profinite<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<GOAL>pullback.snd f g = ((pullback.isLimit f g).conePointUniqueUpToIso (limit.isLimit (cospan f g))).hom ≫ Limits.pullback.snd f g
<VAR>α : Type u<VAR>a : α<VAR>inst✝¹ : Group α<VAR>inst✝ : Fintype α<VAR>g : α<VAR>hx : ∀ (x : α), x ∈ zpowers g<GOAL>orderOf g = Fintype.card α
<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>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set P<VAR>p : (x : P) → x ∈ affineSpan k s → Prop<VAR>mem : ∀ (y : P) (hys : y ∈ s), p y ⋯<VAR>smul_vsub_vadd : ∀ (c : k) (u : P) (hu : u ∈ affineSpan k s) (v : P) (hv : v ∈ affineSpan k s) (w : P) (hw : w ∈ affineSpan k s), p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) ⋯<VAR>x : P<VAR>h : x ∈ affineSpan k s<GOAL>p x h
<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>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set P<VAR>p : (x : P) → x ∈ affineSpan k s → Prop<VAR>mem : ∀ (y : P) (hys : y ∈ s), p y ⋯<VAR>smul_vsub_vadd : ∀ (c : k) (u : P) (hu : u ∈ affineSpan k s) (v : P) (hv : v ∈ affineSpan k s) (w : P) (hw : w ∈ affineSpan k s), p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) ⋯<VAR>x : P<VAR>h : x ∈ affineSpan k s<GOAL>∃ (x_1 : x ∈ affineSpan k s), p x x_1
<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>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set P<VAR>p : (x : P) → x ∈ affineSpan k s → Prop<VAR>mem : ∀ (y : P) (hys : y ∈ s), p y ⋯<VAR>smul_vsub_vadd : ∀ (c : k) (u : P) (hu : u ∈ affineSpan k s) (v : P) (hv : v ∈ affineSpan k s) (w : P) (hw : w ∈ affineSpan k s), p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) ⋯<VAR>x : P<VAR>h : x ∈ affineSpan k s<GOAL>∀ x ∈ s, (fun y => ∃ (z : y ∈ affineSpan k s), p y z) x
<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>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set P<VAR>p : (x : P) → x ∈ affineSpan k s → Prop<VAR>mem : ∀ (y : P) (hys : y ∈ s), p y ⋯<VAR>smul_vsub_vadd : ∀ (c : k) (u : P) (hu : u ∈ affineSpan k s) (v : P) (hv : v ∈ affineSpan k s) (w : P) (hw : w ∈ affineSpan k s), p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) ⋯<VAR>x : P<VAR>h : x ∈ affineSpan k s<GOAL>∀ (c : k) (u v w : P), (fun y => ∃ (z : y ∈ affineSpan k s), p y z) u → (fun y => ∃ (z : y ∈ affineSpan k s), p y z) v → (fun y => ∃ (z : y ∈ affineSpan k s), p y z) w → (fun y => ∃ (z : y ∈ affineSpan k s), p y z) (c • (u -ᵥ v) +ᵥ w)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>δ : Type u_4<VAR>mδ : MeasurableSpace δ<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>g : γ → α<VAR>κ : Kernel α (β × γ)<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>(κ.swapRight.snd a) s = (κ.fst a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>δ : Type u_4<VAR>mδ : MeasurableSpace δ<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>g : γ → α<VAR>κ : Kernel α (β × γ)<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>(κ a) {p | p.swap ∈ {p | p.2 ∈ s}} = (κ a) {p | p.1 ∈ s}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>δ : Type u_4<VAR>mδ : MeasurableSpace δ<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>g : γ → α<VAR>κ : Kernel α (β × γ)<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>MeasurableSet {p | p.2 ∈ s}
<VAR>α✝ β α : Type u<GOAL>#(Set α) = 2 ^ #α
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>hH : Finite (G ⧸ H)<GOAL>H.index ≠ 0
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>hH : Finite (G ⧸ H)<VAR>val✝ : Fintype (G ⧸ H)<GOAL>H.index ≠ 0
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>hH : Finite (G ⧸ H)<VAR>val✝ : Fintype (G ⧸ H)<GOAL>Nat.card (G ⧸ H) ≠ 0
<VAR>α : Type u_1<VAR>d : DynkinSystem α<VAR>s₁ s₂ : Set α<VAR>h₁ : d.Has s₁<VAR>h₂ : d.Has s₂<VAR>h : Disjoint s₁ s₂<GOAL>d.Has (s₁ ∪ s₂)
<VAR>α : Type u_1<VAR>d : DynkinSystem α<VAR>s₁ s₂ : Set α<VAR>h₁ : d.Has s₁<VAR>h₂ : d.Has s₂<VAR>h : Disjoint s₁ s₂<GOAL>d.Has (⋃ b, bif b then s₁ else s₂)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f pf x r<VAR>hg : HasFPowerSeriesOnBall g pg x r<GOAL>HasFPowerSeriesOnBall (f - g) (pf - pg) x r
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x✝ y✝ z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>x y : α<GOAL>x \ y ⊔ x ⊓ y = x
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s : Set α<VAR>f : α → β<VAR>hs : s.Finite<GOAL>(f '' s).Finite
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s : Set α<VAR>f : α → β<VAR>hs : s.Finite<VAR>this : Finite ↑s<GOAL>(f '' s).Finite
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>A : Cᵒᵖ ⥤ Type v<VAR>Y : C<VAR>η : yoneda.obj Y ⟶ A<VAR>X : C<VAR>s : yoneda.obj X ⟶ A<VAR>p : OverArrows η s<GOAL>yoneda.map p.val ≫ η = s
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>A : Cᵒᵖ ⥤ Type v<VAR>Y : C<VAR>η : yoneda.obj Y ⟶ A<VAR>X : C<VAR>s : yoneda.obj X ⟶ A<VAR>p : OverArrows η s<GOAL>η.app (op (unop (op X))) p.val = yonedaEquiv s
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>a : R<VAR>h0 : p ≠ 0<GOAL>multiplicity.Finite (X - C a) p
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>a : R<VAR>h0 : p ≠ 0<VAR>this : Nontrivial R<GOAL>multiplicity.Finite (X - C a) p
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>a : R<VAR>h0 : p ≠ 0<VAR>this : Nontrivial R<GOAL>0 < (X - C a).degree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>a : R<VAR>h0 : p ≠ 0<VAR>this : Nontrivial R<GOAL>0 < 1
<VAR>G : Type u_1<VAR>inst✝ : DivInvMonoid G<VAR>a✝ b a : G<GOAL>a ^ 1 = a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>inst✝ : Preorder β<VAR>l : Filter α<VAR>f : α → Filter β<GOAL>Tendsto f l (𝓝 atTop) ↔ ∀ (y : β), ∀ᶠ (a : α) in l, Ici y ∈ f a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<GOAL>(∃ p, Prime p) ↔ ∃ x, x ≠ 0 ∧ ¬IsUnit x
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>x✝ : ∃ x, x ≠ 0 ∧ ¬IsUnit x<VAR>x : α<VAR>hx₀ : x ≠ 0<VAR>hxu : ¬IsUnit x<GOAL>∃ p, Prime p
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>x✝ : ∃ x, x ≠ 0 ∧ ¬IsUnit x<VAR>x : α<VAR>hx₀ : x ≠ 0<VAR>hxu : ¬IsUnit x<VAR>f : α<VAR>hf : Irreducible f<GOAL>∃ p, Prime p