ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M✝ M N : Comon_ C<VAR>f : M.X ≅ N.X<VAR>f_counit : autoParam (f.hom ≫ N.counit = M.counit) _auto✝<VAR>f_comul : autoParam (f.hom ≫ N.comul = M.comul ≫ (f.hom ⊗ f.hom)) _auto✝<GOAL>f.hom ≫ f.inv ≫ M.comul = (M.comul ≫ (f.hom ⊗ f.hom)) ≫ (f.inv ⊗ f.inv)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : OrderedSemiring R<VAR>a b x y : R<VAR>n m : ℕ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>a ^ n + b ^ n ≤ 2 * (a + b) ^ n
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : OrderedSemiring R<VAR>a b x y : R<VAR>n m : ℕ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>a ^ n + b ^ n ≤ (a + b) ^ n + (a + b) ^ n
<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>s : Finset α<VAR>f : α → β<VAR>comm : (↑s).Pairwise fun a b => Commute (f a) (f b)<GOAL>{x | x ∈ Multiset.map f s.val}.Pairwise Commute
<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>s : Finset α<VAR>f : α → β<VAR>comm : (↑s).Pairwise fun a b => Commute (f a) (f b)<GOAL>{x | ∃ a ∈ s.val, f a = x}.Pairwise Commute
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>inst✝ : IsNoetherian R M<VAR>f : ℕ → Submodule R M<VAR>h : ∀ (n : ℕ), Disjoint ((partialSups f) n) (f (n + 1))<GOAL>∃ n, ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>inst✝ : IsNoetherian R M<VAR>f : ℕ → Submodule R M<VAR>h : ∀ (n : ℕ), Disjoint ((partialSups f) n) (f (n + 1))<VAR>n : ℕ<VAR>w : ∀ (m : ℕ), n ≤ m → (partialSups f) n = (partialSups f) m<GOAL>∃ n, ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>R : Type u_3<VAR>α : Type u_4<VAR>inst✝³ : DivisionSemiring α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSemiring α<VAR>f g : ι → α<VAR>a a₁ a₂ : α<VAR>inst✝ : T2Space α<GOAL>∑' (x : ι), f x / a = (∑' (x : ι), f x) / a
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w : K<VAR>x y : ℝ<GOAL>↑x ≤ ↑y ↔ x ≤ y
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w : K<VAR>x y : ℝ<GOAL>re ↑x ≤ re ↑y ∧ im ↑x = im ↑y ↔ x ≤ y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : SeminormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>𝕜' : Type u_3<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' E<VAR>inst✝ : IsScalarTower 𝕜 𝕜' E<VAR>x : E<GOAL>‖toSpanSingleton 𝕜 x‖ = ‖x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : SeminormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>𝕜' : Type u_3<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' E<VAR>inst✝ : IsScalarTower 𝕜 𝕜' E<VAR>x✝ : E<VAR>x : 𝕜<GOAL>‖(toSpanSingleton 𝕜 x✝) x‖ ≤ ‖x✝‖ * ‖x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : SeminormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>𝕜' : Type u_3<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' E<VAR>inst✝ : IsScalarTower 𝕜 𝕜' E<VAR>x : E<VAR>N : ℝ<VAR>x✝ : N ≥ 0<VAR>h : ∀ (x_1 : 𝕜), ‖(toSpanSingleton 𝕜 x) x_1‖ ≤ N * ‖x_1‖<GOAL>‖x‖ ≤ N
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>μ : OuterMeasure α<GOAL>μ ≤ boundedBy m ↔ ∀ (s : Set α), μ s ≤ m s
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>μ : OuterMeasure α<GOAL>∀ (a : Set α), μ a ≤ ⨆ (_ : a.Nonempty), m a ↔ μ a ≤ m a
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>μ : OuterMeasure α<VAR>s : Set α<GOAL>μ s ≤ ⨆ (_ : s.Nonempty), m s ↔ μ s ≤ m s
<VAR>θ : Angle<GOAL>(θ + ↑π).sign = -θ.sign
<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 X' Y Y' Z Z' : C<VAR>f : X ⟶ X'<VAR>g : Y ⟶ Y'<VAR>h : Z ⟶ Z'<GOAL>f ⊗ g ⊗ h = (α_ X Y Z).inv ≫ ((f ⊗ g) ⊗ h) ≫ (α_ X' Y' Z').hom
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticForm R M<VAR>f : M →ₗ[R] N →ₗ[R] N<VAR>hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x<VAR>n : N<VAR>r : R<GOAL>((foldl Q f hf) n) ((algebraMap R (CliffordAlgebra Q)) r) = r • n
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l : Filter α<VAR>inst✝ : CountableInterFilter l<VAR>g : Set (Set α)<VAR>f : Filter α<VAR>fct : CountableInterFilter f<VAR>hf : g ⊆ f.sets<GOAL>f ≤ countableGenerate g
<VAR>x : ℂ<GOAL>∃ a, cos a = x
<VAR>x w : ℂ<VAR>w₀ : w ≠ 0<VAR>hw : 1 * w * w + -2 * x * w + 1 = 0<GOAL>∃ a, cos a = x
<VAR>x w : ℂ<VAR>w₀ : w ≠ 0<VAR>hw : 1 * w * w + -2 * x * w + 1 = 0<GOAL>cexp (log w / I * I) ^ 2 - 2 * x * cexp (log w / I * I) + 1 = 0
<VAR>x w : ℂ<VAR>w₀ : w ≠ 0<VAR>hw : 1 * w * w + -2 * x * w + 1 = 0<GOAL>w ^ 2 - 2 * x * w + 1 = 0
<VAR>x✝ y✝ x : ℝ<VAR>hx : 0 ≤ x<VAR>y : ℝ<GOAL>√(x * y) = √x * √y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Fintype α<VAR>s : Set α<VAR>inst✝ : Fintype ↑s<GOAL>Fintype.card ↑s = Fintype.card α ↔ s = Set.univ
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι'<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module ℝ F<VAR>v : ι → E<GOAL>Convex ℝ (parallelepiped v)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι'<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module ℝ F<VAR>v : ι → E<GOAL>Convex ℝ (∑ i : ι, segment ℝ 0 (v i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>la : Filter α<VAR>pa : ι → Prop<VAR>sa : ι → Set α<VAR>lb : Filter β<VAR>pb : ι' → Prop<VAR>sb : ι' → Set β<VAR>f : α → β<VAR>hla : la.HasBasis pa sa<VAR>hlb : lb.HasBasis pb sb<GOAL>Tendsto f la lb ↔ ∀ (ib : ι'), pb ib → ∃ ia, pa ia ∧ ∀ x ∈ sa ia, f x ∈ sb ib
<GOAL>comap cexp (𝓝[≠] 0) = comap re atBot
<VAR>this : (cexp ⁻¹' {0})ᶜ = Set.univ<GOAL>comap cexp (𝓝[≠] 0) = comap re atBot
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<GOAL>∑ᶠ (x : ConjClasses G), x.carrier.ncard = Nat.card G
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>f g : α → δ<GOAL>f =ᶠ[ae (μ.restrict (⋃ i, s i))] g ↔ ∀ (i : ι), f =ᶠ[ae (μ.restrict (s i))] g
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hz : ¬0 < z<GOAL>h.IsPrimitiveClassified
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hz : ¬0 < z<VAR>h' : PythagoreanTriple x y (-z)<GOAL>h.IsPrimitiveClassified
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hz : ¬0 < z<VAR>h' : PythagoreanTriple x y (-z)<GOAL>0 < -z
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hz : ¬0 < z<VAR>h' : PythagoreanTriple x y (-z)<GOAL>0 ≤ -z
<VAR>α✝ : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>inst✝ : Subsingleton α<VAR>e : Perm α<GOAL>⇑e = id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort u_6<VAR>s t u : Set α<VAR>m : MeasurableSpace α<VAR>inst✝ : Countable ι<VAR>f : ι → Set α<VAR>h : ∀ (b : ι), MeasurableSet (f b)<GOAL>MeasurableSet (⋃ b, f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort u_6<VAR>s t u : Set α<VAR>m : MeasurableSpace α<VAR>inst✝ : Countable ι<VAR>f : ι → Set α<VAR>h : ∀ (b : ι), MeasurableSet (f b)<VAR>h✝ : IsEmpty ι<GOAL>MeasurableSet (⋃ b, f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort u_6<VAR>s t u : Set α<VAR>m : MeasurableSpace α<VAR>inst✝ : Countable ι<VAR>f : ι → Set α<VAR>h : ∀ (b : ι), MeasurableSet (f b)<VAR>h✝ : Nonempty ι<GOAL>MeasurableSet (⋃ b, f b)
<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>liminf s cofinite = {x | {n | x ∉ s n}.Finite}
<VAR>α : Type u<VAR>m n o : ℕ<VAR>m' : Type u_1<VAR>n' : Type u_2<VAR>o' : Type u_3<VAR>x : α<VAR>u : Fin n → α<VAR>y : α<GOAL>y ∈ Set.range (vecCons x u) ↔ y ∈ {x} ∪ Set.range u
<VAR>q✝ a b c q : ℚ<VAR>hq : q.den = 1<GOAL>↑q.num = q
<VAR>q✝ a b c q : ℚ<VAR>hq : q.den = 1<GOAL>↑q.num = q.num /. ↑1
<VAR>q✝ a b c q : ℚ<VAR>hq : q.den = 1<GOAL>q.num /. 1 = q.num /. ↑1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSingletonClass α<VAR>a : α → ℝ≥0<VAR>a_mble : Measurable a<VAR>a_summable : Summable a<VAR>c : ℝ≥0<VAR>tsum_le_c : ∑' (i : α), a i ≤ c<VAR>ε : ℝ≥0<VAR>ε_ne_zero : ε ≠ 0<GOAL>count {i | ε ≤ a i} ≤ ↑c / ↑ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSingletonClass α<VAR>a : α → ℝ≥0<VAR>a_mble : Measurable a<VAR>a_summable : Summable a<VAR>c : ℝ≥0<VAR>tsum_le_c : ∑' (i : α), a i ≤ c<VAR>ε : ℝ≥0<VAR>ε_ne_zero : ε ≠ 0<GOAL>count {i | ↑ε ≤ (ofNNReal ∘ a) i} ≤ ↑c / ↑ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSingletonClass α<VAR>a : α → ℝ≥0<VAR>a_mble : Measurable a<VAR>a_summable : Summable a<VAR>c : ℝ≥0<VAR>tsum_le_c : ∑' (i : α), a i ≤ c<VAR>ε : ℝ≥0<VAR>ε_ne_zero : ε ≠ 0<GOAL>∑' (i : α), (ofNNReal ∘ a) i ≤ ↑c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSingletonClass α<VAR>a : α → ℝ≥0<VAR>a_mble : Measurable a<VAR>a_summable : Summable a<VAR>c : ℝ≥0<VAR>tsum_le_c : ∑' (i : α), a i ≤ c<VAR>ε : ℝ≥0<VAR>ε_ne_zero : ε ≠ 0<GOAL>∑' (i : α), (ofNNReal ∘ a) i = ↑(∑' (i : α), a i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSingletonClass α<VAR>a : α → ℝ≥0<VAR>a_mble : Measurable a<VAR>a_summable : Summable a<VAR>c : ℝ≥0<VAR>tsum_le_c : ∑' (i : α), a i ≤ c<VAR>ε : ℝ≥0<VAR>ε_ne_zero : ε ≠ 0<GOAL>∑' (i : α), ↑(a i) = ↑(∑' (i : α), a i)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z✝ : ℤ<VAR>a✝ : α<VAR>z : ℤ<VAR>a : α<GOAL>⌊↑z + a⌋ = z + ⌊a⌋
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>m : ℤ<VAR>n : ℕ<GOAL>T m ^ n = T (↑n * m)
<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>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>h : a ∈ s<VAR>f : α → β<VAR>comm : (↑s).Pairwise fun a b => Commute (f a) (f b)<VAR>comm' : optParam (∀ x ∈ ↑(s.erase a), ∀ y ∈ ↑(s.erase a), x ≠ y → (fun a b => Commute (f a) (f b)) x y) ⋯<GOAL>f a * (s.erase a).noncommProd f comm' = s.noncommProd f comm
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>t : TStructure C<VAR>H : ℕ → Prop := fun a => ∀ (n : ℤ), t.GE (n + ↑a) ≤ t.GE n<GOAL>Antitone t.GE
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>t : TStructure C<VAR>H : ℕ → Prop := fun a => ∀ (n : ℤ), t.GE (n + ↑a) ≤ t.GE n<GOAL>∀ (a : ℕ), H a
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>t : TStructure C<VAR>H : ℕ → Prop := fun a => ∀ (n : ℤ), t.GE (n + ↑a) ≤ t.GE n<VAR>H_zero : H 0<GOAL>∀ (a : ℕ), H a
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>t : TStructure C<VAR>H : ℕ → Prop := fun a => ∀ (n : ℤ), t.GE (n + ↑a) ≤ t.GE n<VAR>H_zero : H 0<VAR>H_one : H 1<GOAL>∀ (a : ℕ), H a
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>t : TStructure C<VAR>H : ℕ → Prop := fun a => ∀ (n : ℤ), t.GE (n + ↑a) ≤ t.GE n<VAR>H_zero : H 0<VAR>H_one : H 1<VAR>H_add : ∀ (a b c : ℕ), a + b = c → H a → H b → H c<GOAL>∀ (a : ℕ), H a
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : PartialOrder Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : VAdd Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : AddCommMonoid V<VAR>inst✝¹ : AddCommMonoid R<VAR>inst✝ : SMulWithZero R V<VAR>x y : HahnSeries Γ R<VAR>z : HahnModule Γ' R V<VAR>h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u<VAR>a : Γ'<GOAL>((of R).symm ((x + y) • z)).coeff a = ((of R).symm (x • z + y • z)).coeff a
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : PartialOrder Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : VAdd Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : AddCommMonoid V<VAR>inst✝¹ : AddCommMonoid R<VAR>inst✝ : SMulWithZero R V<VAR>x y : HahnSeries Γ R<VAR>z : HahnModule Γ' R V<VAR>h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u<VAR>a : Γ'<VAR>hwf : (x.support ∪ y.support).IsPWO<GOAL>((of R).symm ((x + y) • z)).coeff a = ((of R).symm (x • z + y • z)).coeff a
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : PartialOrder Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : VAdd Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : AddCommMonoid V<VAR>inst✝¹ : AddCommMonoid R<VAR>inst✝ : SMulWithZero R V<VAR>x y : HahnSeries Γ R<VAR>z : HahnModule Γ' R V<VAR>h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u<VAR>a : Γ'<VAR>hwf : (x.support ∪ y.support).IsPWO<GOAL>∑ ij ∈ VAddAntidiagonal hwf ⋯ a, (x.coeff + y.coeff) ij.1 • ((of R).symm z).coeff ij.2 = ((of R).symm (x • z) + (of R).symm (y • z)).coeff a
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : PartialOrder Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : VAdd Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : AddCommMonoid V<VAR>inst✝¹ : AddCommMonoid R<VAR>inst✝ : SMulWithZero R V<VAR>x y : HahnSeries Γ R<VAR>z : HahnModule Γ' R V<VAR>h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u<VAR>a : Γ'<VAR>hwf : (x.support ∪ y.support).IsPWO<GOAL>(x + y).support ⊆ x.support ∪ y.support
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : PartialOrder Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : VAdd Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : AddCommMonoid V<VAR>inst✝¹ : AddCommMonoid R<VAR>inst✝ : SMulWithZero R V<VAR>x y : HahnSeries Γ R<VAR>z : HahnModule Γ' R V<VAR>h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u<VAR>a : Γ'<VAR>hwf : (x.support ∪ y.support).IsPWO<GOAL>∑ x_1 ∈ VAddAntidiagonal hwf ⋯ a, (x.coeff x_1.1 • ((of R).symm z).coeff x_1.2 + y.coeff x_1.1 • ((of R).symm z).coeff x_1.2) = ((of R).symm (x • z)).coeff a + ((of R).symm (y • z)).coeff a
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : PartialOrder Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : VAdd Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : AddCommMonoid V<VAR>inst✝¹ : AddCommMonoid R<VAR>inst✝ : SMulWithZero R V<VAR>x y : HahnSeries Γ R<VAR>z : HahnModule Γ' R V<VAR>h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u<VAR>a : Γ'<VAR>hwf : (x.support ∪ y.support).IsPWO<GOAL>∑ x_1 ∈ VAddAntidiagonal hwf ⋯ a, (x.coeff x_1.1 • ((of R).symm z).coeff x_1.2 + y.coeff x_1.1 • ((of R).symm z).coeff x_1.2) = ∑ ij ∈ VAddAntidiagonal hwf ⋯ a, x.coeff ij.1 • ((of R).symm z).coeff ij.2 + ∑ ij ∈ VAddAntidiagonal hwf ⋯ a, y.coeff ij.1 • ((of R).symm z).coeff ij.2
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>[a] <+ l ↔ a ∈ l
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<VAR>h : a ∈ l<GOAL>[a] <+ l
<VAR>α : Type u_1<VAR>a : α<VAR>w✝¹ w✝ : List α<VAR>h : a ∈ w✝¹ ++ a :: w✝<GOAL>[a] <+ w✝¹ ++ a :: w✝
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>M : Matrix n n R<GOAL>matPolyEquiv (M.map ⇑C) = C M
<VAR>x : ℝ<GOAL>sInf (norm '' {m | ↑m = ↑x}) = min (fract x) (1 - fract x)
<VAR>x : ℝ<VAR>h₁ : BddBelow (abs '' {m | ↑m = ↑x})<GOAL>sInf (norm '' {m | ↑m = ↑x}) = min (fract x) (1 - fract x)
<VAR>x : ℝ<VAR>h₁ : BddBelow (abs '' {m | ↑m = ↑x})<VAR>h₂ : (abs '' {m | ↑m = ↑x}).Nonempty<GOAL>sInf (norm '' {m | ↑m = ↑x}) = min (fract x) (1 - fract x)
<VAR>x : ℝ<VAR>h₁ : BddBelow (abs '' {m | ↑m = ↑x})<VAR>h₂ : (abs '' {m | ↑m = ↑x}).Nonempty<GOAL>sInf (norm '' {m | ↑m = ↑x}) ≤ min (fract x) (1 - fract x)
<VAR>x : ℝ<VAR>h₁ : BddBelow (abs '' {m | ↑m = ↑x})<VAR>h₂ : (abs '' {m | ↑m = ↑x}).Nonempty<GOAL>min (fract x) (1 - fract x) ≤ sInf (norm '' {m | ↑m = ↑x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α → Option β<VAR>h : ∀ (a : α), (f a).isSome = true<VAR>hf : Primrec f<GOAL>Primrec fun a => (f a).get ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α → Option β<VAR>h : ∀ (a : α), (f a).isSome = true<VAR>hf : Primrec f<VAR>n : ℕ<GOAL>(encode (Option.map f (decode n))).pred = encode (Option.map (fun a => (f a).get ⋯) (decode n))
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>P : Ideal R[X]<GOAL>((Quotient.mk (map (mapRingHom (Quotient.mk (comap C P))) P)).comp C).comp (Quotient.mk (comap C P)) = (quotientMap (map (mapRingHom (Quotient.mk (comap C P))) P) (mapRingHom (Quotient.mk (comap C P))) ⋯).comp ((Quotient.mk P).comp C)
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>P : Ideal R[X]<VAR>x : R<GOAL>(((Quotient.mk (map (mapRingHom (Quotient.mk (comap C P))) P)).comp C).comp (Quotient.mk (comap C P))) x = ((quotientMap (map (mapRingHom (Quotient.mk (comap C P))) P) (mapRingHom (Quotient.mk (comap C P))) ⋯).comp ((Quotient.mk P).comp C)) x
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>P : Ideal R[X]<VAR>x : R<GOAL>(Quotient.mk (map (mapRingHom (Quotient.mk (comap C P))) P)) (C ((Quotient.mk (comap C P)) x)) = (quotientMap (map (mapRingHom (Quotient.mk (comap C P))) P) (mapRingHom (Quotient.mk (comap C P))) ⋯) ((Quotient.mk P) (C x))
<VAR>R L : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing L<VAR>inst✝³ : IsDomain L<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : NoZeroSMulDivisors R L<VAR>inst✝ : Algebra.IsAlgebraic R L<GOAL>#((p : R[X]) × { x // x ∈ p.aroots L }) = sum fun p => #↑{x | x ∈ p.aroots L}
<VAR>R L : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing L<VAR>inst✝³ : IsDomain L<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : NoZeroSMulDivisors R L<VAR>inst✝ : Algebra.IsAlgebraic R L<GOAL>#((p : R[X]) × { x // x ∈ p.aroots L }) = #((i : R[X]) × ↑{x | x ∈ i.aroots L})
<VAR>R L : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing L<VAR>inst✝³ : IsDomain L<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : NoZeroSMulDivisors R L<VAR>inst✝ : Algebra.IsAlgebraic R L<GOAL>max (max (max #R ℵ₀) ℵ₀) ℵ₀ = max #R ℵ₀
<VAR>R✝ : Type u<VAR>S : Type v<VAR>F : Type w<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : Semiring S<VAR>ι✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CommRing R<VAR>ι : Type u_3<VAR>inst✝ : Finite ι<VAR>I : ι → Ideal R<VAR>hI : Pairwise fun i j => IsCoprime (I i) (I j)<VAR>x : ι → R<GOAL>∃ r, ∀ (i : ι), r - x i ∈ I i
<VAR>R✝ : Type u<VAR>S : Type v<VAR>F : Type w<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : Semiring S<VAR>ι✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CommRing R<VAR>ι : Type u_3<VAR>inst✝ : Finite ι<VAR>I : ι → Ideal R<VAR>hI : Pairwise fun i j => IsCoprime (I i) (I j)<VAR>x : ι → R<VAR>y : R<VAR>hy : ∀ (i : ι), (Quotient.mk (I i)) y = (Quotient.mk (I i)) (x i)<GOAL>∃ r, ∀ (i : ι), r - x i ∈ I i
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>h : α ≃ᵢ β<GOAL>EMetric.diam univ = EMetric.diam univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s : Set α<VAR>hs : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → edist x y = ⊤<GOAL>s.Subsingleton
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>s t : Set Ω<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<GOAL>CondIndepSets m' hm' {s} {t} μ ↔ μ[(s ∩ t).indicator fun ω => 1|m'] =ᶠ[ae μ] μ[s.indicator fun ω => 1|m'] * μ[t.indicator fun ω => 1|m']
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>s t : Set Ω<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<GOAL>(∀ (t1 t2 : Set Ω), t1 ∈ {s} → t2 ∈ {t} → μ[(t1 ∩ t2).indicator fun ω => 1|m'] =ᶠ[ae μ] μ[t1.indicator fun ω => 1|m'] * μ[t2.indicator fun ω => 1|m']) ↔ μ[(s ∩ t).indicator fun ω => 1|m'] =ᶠ[ae μ] μ[s.indicator fun ω => 1|m'] * μ[t.indicator fun ω => 1|m']
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>s t : Set Ω<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<GOAL>∀ s_1 ∈ {s}, MeasurableSet s_1
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>s t : Set Ω<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<GOAL>∀ s ∈ {t}, MeasurableSet s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<GOAL>Iic b \ Iic a = Ioc a b
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : MulZeroOneClass α<VAR>inst✝¹ : Nontrivial α<VAR>A : Matrix V V α<VAR>h : A.IsAdjMatrix<VAR>inst✝ : DecidableEq α<VAR>i j : V<GOAL>adjMatrix α h.toGraph i j = A i j
<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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>(∡ p₃ p₁ p₂).sin * dist p₁ p₃ = dist p₃ p₂
<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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<VAR>hs : (∡ p₃ p₁ p₂).sign = 1<GOAL>(∡ p₃ p₁ p₂).sin * dist p₁ p₃ = dist p₃ p₂