ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>n : ℕ<VAR>hs : autoParam s.Finite _auto✝<GOAL>(∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n) → s.ncard = n + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t✝ : Set α<VAR>f : α → β<VAR>hs : autoParam s.Finite _auto✝<VAR>a : α<VAR>t : Set α<VAR>hat : a ∉ t<VAR>h : insert a t = s<GOAL>s.ncard = t.ncard + 1
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<VAR>m : ℤ<GOAL>toIcoMod hp a (m • p + b) = toIcoMod hp a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ✝ : Type u_3<VAR>γ : Type u_4<VAR>f : Part α<VAR>g : α → Part β<VAR>k : β → Part γ<VAR>a : γ<GOAL>a ∈ (f.bind g).bind k ↔ a ∈ f.bind fun x => (g x).bind k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ✝ : Type u_3<VAR>γ : Type u_4<VAR>f : Part α<VAR>g : α → Part β<VAR>k : β → Part γ<VAR>a : γ<GOAL>(∃ a_1, (∃ a ∈ f, a_1 ∈ g a) ∧ a ∈ k a_1) ↔ ∃ a_1 ∈ f, ∃ a_2 ∈ g a_1, a ∈ k a_2
<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>h : ∀ (x : M), ∃ u, IsOpen u ∧ x ∈ u ∧ LiftPropOn P g u<GOAL>LiftProp P g
<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>h : ∀ (x : M), ∃ u, IsOpen u ∧ x ∈ u ∧ LiftPropOn P g u<GOAL>LiftPropOn P g univ
<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>h : ∀ (x : M), ∃ u, IsOpen u ∧ x ∈ u ∧ LiftPropOn P g u<VAR>x : M<VAR>x✝ : x ∈ univ<GOAL>∃ u, IsOpen u ∧ x ∈ u ∧ LiftPropOn P g (univ ∩ u)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : FirstCountableTopology X<VAR>inst✝¹ : R1Space X<VAR>x y : X<VAR>inst✝ : WeaklyLocallyCompactSpace X<VAR>K : Set X<VAR>hK : IsCompact K<GOAL>∃ V, IsOpen V ∧ K ⊆ V ∧ IsCompact (closure V)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : FirstCountableTopology X<VAR>inst✝¹ : R1Space X<VAR>x y : X<VAR>inst✝ : WeaklyLocallyCompactSpace X<VAR>K : Set X<VAR>hK : IsCompact K<VAR>K' : Set X<VAR>hK' : IsCompact K'<VAR>hKK' : K ⊆ interior K'<GOAL>∃ V, IsOpen V ∧ K ⊆ V ∧ IsCompact (closure V)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>hs : s.Countable<GOAL>μ s = 0 ↔ ∀ x ∈ s, μ {x} = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b b₁✝ b₂✝ : β<VAR>inst✝³ : OrderedRing α<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulMono α β<VAR>b₁ b₂ : α<VAR>a d : β<VAR>hba : b₂ ≤ b₁<VAR>hdc : d ≤ a<GOAL>b₁ • d + b₂ • a ≤ b₁ • a + b₂ • d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b b₁✝ b₂✝ : β<VAR>inst✝³ : OrderedRing α<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulMono α β<VAR>b₁ b₂ : α<VAR>a d : β<VAR>hba : b₂ ≤ b₁<VAR>hdc : d ≤ a<GOAL>b₂ • a + b₁ • d ≤ b₂ • d + b₁ • a
<VAR>a b m n✝ p✝ n p : ℕ<VAR>hp : ¬Prime p<GOAL>n / p ^ n.factorization p = n
<VAR>n✝ m a n : ℕ<VAR>inst✝ : NeZero n<GOAL>↑a = 0 ↔ n ∣ a
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>ν : Measure α<VAR>f : α → G<VAR>hμ : Integrable f μ<VAR>hν : Integrable f ν<VAR>hG : CompleteSpace G<GOAL>∫ (x : α), f x ∂(μ + ν) = ∫ (x : α), f x ∂μ + ∫ (x : α), f x ∂ν
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>ν : Measure α<VAR>f : α → G<VAR>hμ : Integrable f μ<VAR>hν : Integrable f ν<VAR>hG : CompleteSpace G<VAR>hfi : Integrable f (μ + ν)<GOAL>∫ (x : α), f x ∂(μ + ν) = ∫ (x : α), f x ∂μ + ∫ (x : α), f x ∂ν
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>ν : Measure α<VAR>f : α → G<VAR>hμ : Integrable f μ<VAR>hν : Integrable f ν<VAR>hG : CompleteSpace G<VAR>hfi : Integrable f (μ + ν)<GOAL>setToFun (μ + ν) (weightedSMul (μ + ν)) ⋯ f = setToFun μ (weightedSMul μ) ⋯ f + setToFun ν (weightedSMul ν) ⋯ f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>ν : Measure α<VAR>f : α → G<VAR>hμ : Integrable f μ<VAR>hν : Integrable f ν<VAR>hG : CompleteSpace G<VAR>hfi : Integrable f (μ + ν)<VAR>hμ_dfma : DominatedFinMeasAdditive (μ + ν) (weightedSMul μ) 1<GOAL>setToFun (μ + ν) (weightedSMul (μ + ν)) ⋯ f = setToFun μ (weightedSMul μ) ⋯ f + setToFun ν (weightedSMul ν) ⋯ f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>ν : Measure α<VAR>f : α → G<VAR>hμ : Integrable f μ<VAR>hν : Integrable f ν<VAR>hG : CompleteSpace G<VAR>hfi : Integrable f (μ + ν)<VAR>hμ_dfma : DominatedFinMeasAdditive (μ + ν) (weightedSMul μ) 1<VAR>hν_dfma : DominatedFinMeasAdditive (μ + ν) (weightedSMul ν) 1<GOAL>setToFun (μ + ν) (weightedSMul (μ + ν)) ⋯ f = setToFun μ (weightedSMul μ) ⋯ f + setToFun ν (weightedSMul ν) ⋯ f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>ν : Measure α<VAR>f : α → G<VAR>hμ : Integrable f μ<VAR>hν : Integrable f ν<VAR>hG : CompleteSpace G<VAR>hfi : Integrable f (μ + ν)<VAR>hμ_dfma : DominatedFinMeasAdditive (μ + ν) (weightedSMul μ) 1<VAR>hν_dfma : DominatedFinMeasAdditive (μ + ν) (weightedSMul ν) 1<GOAL>setToFun (μ + ν) (weightedSMul (μ + ν)) ⋯ f = setToFun (μ + ν) (weightedSMul μ) hμ_dfma f + setToFun (μ + ν) (weightedSMul ν) hν_dfma f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>ν : Measure α<VAR>f : α → G<VAR>hμ : Integrable f μ<VAR>hν : Integrable f ν<VAR>hG : CompleteSpace G<VAR>hfi : Integrable f (μ + ν)<VAR>hμ_dfma : DominatedFinMeasAdditive (μ + ν) (weightedSMul μ) 1<VAR>hν_dfma : DominatedFinMeasAdditive (μ + ν) (weightedSMul ν) 1<VAR>s : Set α<VAR>x✝ : MeasurableSet s<VAR>hμνs : (μ + ν) s < ⊤<GOAL>weightedSMul (μ + ν) s = weightedSMul μ s + weightedSMul ν s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>ν : Measure α<VAR>f : α → G<VAR>hμ : Integrable f μ<VAR>hν : Integrable f ν<VAR>hG : CompleteSpace G<VAR>hfi : Integrable f (μ + ν)<VAR>hμ_dfma : DominatedFinMeasAdditive (μ + ν) (weightedSMul μ) 1<VAR>hν_dfma : DominatedFinMeasAdditive (μ + ν) (weightedSMul ν) 1<VAR>s : Set α<VAR>x✝ : MeasurableSet s<VAR>hμνs : μ s < ⊤ ∧ ν s < ⊤<GOAL>weightedSMul (μ + ν) s = weightedSMul μ s + weightedSMul ν s
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f g : ↑(X.presheaf.obj (op U))<GOAL>Subtype.val '' {x | IsUnit ((X.presheaf.germ x) (f * g))} = Subtype.val '' {x | IsUnit ((X.presheaf.germ x) f)} ∩ Subtype.val '' {x | IsUnit ((X.presheaf.germ x) g)}
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f g : ↑(X.presheaf.obj (op U))<GOAL>Subtype.val '' {x | IsUnit ((X.presheaf.germ x) (f * g))} = (fun a => ↑a) '' ({x | IsUnit ((X.presheaf.germ x) f)} ∩ {x | IsUnit ((X.presheaf.germ x) g)})
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f g : ↑(X.presheaf.obj (op U))<VAR>x : ↑↑X.toPresheafedSpace<GOAL>x ∈ Subtype.val '' {x | IsUnit ((X.presheaf.germ x) (f * g))} ↔ x ∈ (fun a => ↑a) '' ({x | IsUnit ((X.presheaf.germ x) f)} ∩ {x | IsUnit ((X.presheaf.germ x) g)})
<VAR>A : Type u_1<VAR>inst✝³ : AddCommGroup A<VAR>inst✝² : Module ℂ A<VAR>inst✝¹ : StarAddMonoid A<VAR>inst✝ : StarModule ℂ A<VAR>x : A<GOAL>↑((skewAdjointPart ℝ) x) = I • ↑(ℑ x)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>X✝ Y Z : C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>B A₁ A₂ : C<VAR>X : Subobject B<VAR>f : A₁ ⟶ B<VAR>inst✝¹ : Mono f<VAR>g : A₂ ⟶ B<VAR>inst✝ : Mono g<VAR>h₁ : X ≤ mk f<VAR>h₂ : mk f ≤ mk g<GOAL>X.ofLEMk f h₁ ≫ ofMkLEMk f g h₂ = X.ofLEMk g ⋯
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>X✝ Y Z : C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>B A₁ A₂ : C<VAR>X : Subobject B<VAR>f : A₁ ⟶ B<VAR>inst✝¹ : Mono f<VAR>g : A₂ ⟶ B<VAR>inst✝ : Mono g<VAR>h₁ : X ≤ mk f<VAR>h₂ : mk f ≤ mk g<GOAL>underlying.map (h₁.hom ≫ h₂.hom) ≫ (underlyingIso g).hom = underlying.map ⋯.hom ≫ (underlyingIso g).hom
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : DivisionMonoid α<VAR>inst✝ : HasDistribNeg α<VAR>a✝ : α<VAR>c : ℤ<VAR>a : α<GOAL>(-a) ^ (c + c) = a ^ (c + c)
<VAR>u : Level<VAR>α : Q(Type u)<VAR>zα : Q(Zero «$α»)<VAR>pα : Q(PartialOrder «$α»)<VAR>A : Type u_1<VAR>e : A<VAR>n : ℤ<VAR>d : ℕ<VAR>inst✝ : LinearOrderedRing A<VAR>inv : Invertible ↑d<VAR>eq : e = ↑n * ⅟↑d<VAR>h : decide (n = 0) = true<GOAL>0 ≤ e
<VAR>u : Level<VAR>α : Q(Type u)<VAR>zα : Q(Zero «$α»)<VAR>pα : Q(PartialOrder «$α»)<VAR>A : Type u_1<VAR>e : A<VAR>n : ℤ<VAR>d : ℕ<VAR>inst✝ : LinearOrderedRing A<VAR>inv : Invertible ↑d<VAR>eq : e = ↑n * ⅟↑d<VAR>h : decide (n = 0) = true<GOAL>0 ≤ ↑0 * ⅟↑d
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x✝ y✝ : α<VAR>inst✝² : DecidableRel f✝.SameCycle<VAR>inst✝¹ : DecidableRel g.SameCycle<VAR>f : Perm α<VAR>inst✝ : DecidableRel f.SameCycle<VAR>x y : α<GOAL>(f.cycleOf x)⁻¹ y = (f⁻¹.cycleOf x) y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x✝ y✝ : α<VAR>inst✝² : DecidableRel f✝.SameCycle<VAR>inst✝¹ : DecidableRel g.SameCycle<VAR>f : Perm α<VAR>inst✝ : DecidableRel f.SameCycle<VAR>x y : α<GOAL>y = if f.SameCycle x (if f⁻¹.SameCycle x y then f⁻¹ y else y) then f (if f⁻¹.SameCycle x y then f⁻¹ y else y) else if f⁻¹.SameCycle x y then f⁻¹ y else y
<VAR>xl xr : Type u<VAR>x : PGame<GOAL>-x ⧏ 0 ↔ 0 ⧏ x
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝¹ : NonUnitalNonAssocSemiring α<VAR>inst✝ : Fintype m<VAR>L M : Matrix l m α<VAR>N : Matrix m n α<VAR>i✝ : l<VAR>j✝ : n<GOAL>((L + M) * N) i✝ j✝ = (L * N + M * N) i✝ j✝
<VAR>J : Type w<VAR>K : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>f : J → C<VAR>inst✝¹ : HasBiproduct f<VAR>p : J → Prop<VAR>inst✝ : HasBiproduct (Subtype.restrict p f)<VAR>j j✝ : Subtype p<GOAL>ι (Subtype.restrict p f) j✝ ≫ fromSubtype f p ≫ π f ↑j = ι (Subtype.restrict p f) j✝ ≫ π (Subtype.restrict p f) j
<VAR>J : Type w<VAR>K : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>f : J → C<VAR>inst✝¹ : HasBiproduct f<VAR>p : J → Prop<VAR>inst✝ : HasBiproduct (Subtype.restrict p f)<VAR>j j✝ : Subtype p<GOAL>(if h : ↑j✝ = ↑j then eqToHom ⋯ else 0) = if h : j✝ = j then eqToHom ⋯ else 0
<VAR>J : Type w<VAR>K : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>f : J → C<VAR>inst✝¹ : HasBiproduct f<VAR>p : J → Prop<VAR>inst✝ : HasBiproduct (Subtype.restrict p f)<VAR>j j✝ : Subtype p<VAR>h₁ : ↑j✝ = ↑j<VAR>h₂ : j✝ = j<GOAL>eqToHom ⋯ = eqToHom ⋯
<VAR>J : Type w<VAR>K : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>f : J → C<VAR>inst✝¹ : HasBiproduct f<VAR>p : J → Prop<VAR>inst✝ : HasBiproduct (Subtype.restrict p f)<VAR>j j✝ : Subtype p<VAR>h₁ : ↑j✝ = ↑j<VAR>h₂ : ¬j✝ = j<GOAL>eqToHom ⋯ = 0
<VAR>J : Type w<VAR>K : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>f : J → C<VAR>inst✝¹ : HasBiproduct f<VAR>p : J → Prop<VAR>inst✝ : HasBiproduct (Subtype.restrict p f)<VAR>j j✝ : Subtype p<VAR>h₁ : ¬↑j✝ = ↑j<VAR>h₂ : j✝ = j<GOAL>0 = eqToHom ⋯
<VAR>J : Type w<VAR>K : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>f : J → C<VAR>inst✝¹ : HasBiproduct f<VAR>p : J → Prop<VAR>inst✝ : HasBiproduct (Subtype.restrict p f)<VAR>j j✝ : Subtype p<VAR>h₁ : ¬↑j✝ = ↑j<VAR>h₂ : ¬j✝ = j<GOAL>0 = 0
<VAR>𝕜 : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>x : H<GOAL>↑I.symm (↑I x) = x
<VAR>𝕜 : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>x : H<GOAL>x ∈ I.source
<VAR>n : ℕ<VAR>h : IsSquare (-1)<GOAL>∃ x y, n = x ^ 2 + y ^ 2
<VAR>h : IsSquare (-1)<GOAL>∃ x y, 0 = x ^ 2 + y ^ 2
<VAR>h : IsSquare (-1)<GOAL>∃ x y, 1 = x ^ 2 + y ^ 2
<VAR>p n : ℕ<VAR>hpp : Prime p<VAR>ih : IsSquare (-1) → ∃ x y, n = x ^ 2 + y ^ 2<VAR>h : IsSquare (-1)<GOAL>∃ x y, p * n = x ^ 2 + y ^ 2
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>x : M<GOAL>‖↑x‖ = infDist x ↑S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>x : M<GOAL>infDist x (⇑(IsometryEquiv.subLeft x).symm ⁻¹' {m | ↑m = ↑x}) = infDist x ↑S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>x y : M<GOAL>y ∈ ⇑(IsometryEquiv.subLeft x).symm ⁻¹' {m | ↑m = ↑x} ↔ y ∈ ↑S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<GOAL>(∫⁻ (a : α), f a ∂μ) * r ≤ ∫⁻ (a : α), f a * r ∂μ
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>E : Type uE<VAR>F : Type uF<VAR>M : Type uM<VAR>ι : Type uι<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>b : Basis ι R M<VAR>a : A<VAR>i : ι<GOAL>a • (basis A b) i = a ⊗ₜ[R] b i
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>s : Computation α<GOAL>s.bind (pure ∘ f) = map f s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>s : Computation α<GOAL>IsBisimulation fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>s : Computation α<GOAL>s.bind (pure ∘ f) = map f s ∨ ∃ s_1, s.bind (pure ∘ f) = s_1.bind (pure ∘ f) ∧ map f s = map f s_1
<VAR>x y : ℝ<GOAL>0 ≤ arsinh x ↔ 0 ≤ x
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X : Scheme<VAR>U✝ U V : X.Opens<VAR>i : U ⟶ V<VAR>W : (↑V).Opens<GOAL>U.ι ''ᵁ (X.restrictFunctor.map i).left ⁻¹ᵁ W ≤ V.ι ''ᵁ W
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X : Scheme<VAR>U✝ U V : X.Opens<VAR>i : U ⟶ V<VAR>W : (↑V).Opens<GOAL>⇑((Opens.toTopCat ↑X.toPresheafedSpace).map i) ⁻¹' ↑W ⊆ ⇑U.ι.val.base ⁻¹' (⇑V.ι.val.base '' ↑W)
<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℕ<VAR>hroot : (cyclotomic n (ZMod p)).IsRoot ((Nat.castRingHom (ZMod p)) a)<GOAL>orderOf (ZMod.unitOfCoprime a ⋯) ∣ n
<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℕ<VAR>hroot : (cyclotomic n (ZMod p)).IsRoot ((Nat.castRingHom (ZMod p)) a)<GOAL>ZMod.unitOfCoprime a ⋯ ^ n = 1
<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℕ<VAR>hroot : (cyclotomic n (ZMod p)).IsRoot ((Nat.castRingHom (ZMod p)) a)<GOAL>eval ((Nat.castRingHom (ZMod p)) a) (X ^ n - 1) = 0
<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℕ<VAR>hroot : eval ((Nat.castRingHom (ZMod p)) a) (cyclotomic n (ZMod p)) = 0<GOAL>eval ((Nat.castRingHom (ZMod p)) a) (X ^ n - 1) = 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>x✝¹ : NonAssocSemiring α<VAR>x✝ : NonAssocSemiring β<VAR>f : α →+* β<VAR>x y✝ : α<VAR>h : ∀ (x : α), f x = 0<VAR>y : β<VAR>hy : y ∈ {0}<GOAL>f 0 = y
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic F<VAR>inst✝¹ : Field F<VAR>inst✝ : Field K<VAR>φ : F →+* K<VAR>x y z : K<VAR>ha : P.a ≠ 0<VAR>h3 : (map φ P).roots = {x, y, z}<GOAL>P.disc ≠ 0 ↔ x ≠ y ∧ x ≠ z ∧ y ≠ z
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic F<VAR>inst✝¹ : Field F<VAR>inst✝ : Field K<VAR>φ : F →+* K<VAR>x y z : K<VAR>ha : P.a ≠ 0<VAR>h3 : (map φ P).roots = {x, y, z}<GOAL>φ P.a * φ P.a * (x - y) * (x - z) * (y - z) * (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ≠ 0 ↔ x ≠ y ∧ x ≠ z ∧ y ≠ z
<VAR>V : Type (u + 1)<VAR>inst✝¹ : LargeCategory V<VAR>W : Type (u + 1)<VAR>inst✝ : LargeCategory W<VAR>F : V ⥤ W<VAR>G : MonCat<VAR>M : Action V G<GOAL>(fun g => F.map (M.ρ g)) 1 = 1
<VAR>V : Type (u + 1)<VAR>inst✝¹ : LargeCategory V<VAR>W : Type (u + 1)<VAR>inst✝ : LargeCategory W<VAR>F : V ⥤ W<VAR>G : MonCat<VAR>M : Action V G<VAR>g h : ↑G<GOAL>F.map (M.ρ (g * h)) = F.map (M.ρ g) * F.map (M.ρ h)
<VAR>V : Type (u + 1)<VAR>inst✝¹ : LargeCategory V<VAR>W : Type (u + 1)<VAR>inst✝ : LargeCategory W<VAR>F : V ⥤ W<VAR>G : MonCat<VAR>X✝ Y✝ : Action V G<VAR>f : X✝ ⟶ Y✝<VAR>g : ↑G<GOAL>F.map (X✝.ρ g) ≫ F.map f.hom = F.map f.hom ≫ F.map (Y✝.ρ g)
<VAR>V : Type (u + 1)<VAR>inst✝¹ : LargeCategory V<VAR>W : Type (u + 1)<VAR>inst✝ : LargeCategory W<VAR>F : V ⥤ W<VAR>G : MonCat<VAR>M : Action V G<GOAL>({ obj := fun M => { V := F.obj M.V, ρ := { toFun := fun g => F.map (M.ρ g), map_one' := ⋯, map_mul' := ⋯ } }, map := fun {X Y} f => { hom := F.map f.hom, comm := ⋯ } }.map (𝟙 M)).hom = (𝟙 ({ obj := fun M => { V := F.obj M.V, ρ := { toFun := fun g => F.map (M.ρ g), map_one' := ⋯, map_mul' := ⋯ } }, map := fun {X Y} f => { hom := F.map f.hom, comm := ⋯ } }.obj M)).hom
<VAR>V : Type (u + 1)<VAR>inst✝¹ : LargeCategory V<VAR>W : Type (u + 1)<VAR>inst✝ : LargeCategory W<VAR>F : V ⥤ W<VAR>G : MonCat<VAR>X✝ Y✝ Z✝ : Action V G<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<GOAL>({ obj := fun M => { V := F.obj M.V, ρ := { toFun := fun g => F.map (M.ρ g), map_one' := ⋯, map_mul' := ⋯ } }, map := fun {X Y} f => { hom := F.map f.hom, comm := ⋯ } }.map (f ≫ g)).hom = ({ obj := fun M => { V := F.obj M.V, ρ := { toFun := fun g => F.map (M.ρ g), map_one' := ⋯, map_mul' := ⋯ } }, map := fun {X Y} f => { hom := F.map f.hom, comm := ⋯ } }.map f ≫ { obj := fun M => { V := F.obj M.V, ρ := { toFun := fun g => F.map (M.ρ g), map_one' := ⋯, map_mul' := ⋯ } }, map := fun {X Y} f => { hom := F.map f.hom, comm := ⋯ } }.map g).hom
<VAR>B : Type u<VAR>inst✝ : Quiver B<VAR>a b c : B<VAR>f g : Hom b c<VAR>η' : Hom₂ f g<GOAL>(fun p => normalizeAux p f) = fun p => normalizeAux p g
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁✝ : S₁.HomologyData<VAR>h₂✝ : S₂.HomologyData<VAR>h : S.HomologyData<VAR>h₁ : S.LeftHomologyData<VAR>h₂ : S.RightHomologyData<GOAL>leftRightHomologyComparison' h₁ h₂ = leftHomologyMap' (𝟙 S) h₁ h.left ≫ h.iso.hom ≫ rightHomologyMap' (𝟙 S) h.right h₂
<VAR>x✝ y✝ z✝ : ℝ<VAR>n : ℕ<VAR>x : ℝ<VAR>hx : x ≠ 0<VAR>y : ℝ<VAR>hy : y ∈ {y | 0 ≤ y}<VAR>z : ℝ<VAR>hz : z ∈ {y | 0 ≤ y}<VAR>hyz : y ^ x = z ^ x<GOAL>y = z
<VAR>x y : ℝ<VAR>a b : Cauchy abs<GOAL>(Real.mul { cauchy := a } { cauchy := b }).cauchy = { cauchy := a }.cauchy * { cauchy := b }.cauchy