ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : SeminormedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p✝ p : Seminorm 𝕜 E<VAR>r₁ r₂ : ℝ<VAR>a : 𝕜<VAR>ha : ‖a‖ ≤ r₁<VAR>b : E<VAR>hb : p b ≤ r₂<GOAL>0 ≤ r₁
<VAR>z : ℂ<GOAL>z.im ^ 2 ≤ normSq z
<VAR>z : ℂ<GOAL>z.im ^ 2 ≤ z.re ^ 2 + z.im ^ 2
<VAR>q : ℍ<VAR>hq : q.re = 0<VAR>c s : ℝ<VAR>hc : HasSum (fun n => (-1) ^ n * ‖q‖ ^ (2 * n) / ↑(2 * n)!) c<VAR>hs : HasSum (fun n => (-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)!) s<GOAL>HasSum (fun n => (expSeries ℝ ℍ n) fun x => q) (↑c + (s / ‖q‖) • q)
<VAR>q : ℍ<VAR>hq : q.re = 0<VAR>c s : ℝ<VAR>hs : HasSum (fun n => (-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1)!) s<VAR>hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c<GOAL>HasSum (fun n => (expSeries ℝ ℍ n) fun x => q) (↑c + (s / ‖q‖) • q)
<VAR>q : ℍ<VAR>hq : q.re = 0<VAR>c s : ℝ<VAR>hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c<VAR>hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)<GOAL>HasSum (fun n => (expSeries ℝ ℍ n) fun x => q) (↑c + (s / ‖q‖) • q)
<VAR>q : ℍ<VAR>hq : q.re = 0<VAR>c s : ℝ<VAR>hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c<VAR>hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)<GOAL>HasSum (fun k => (expSeries ℝ ℍ (2 * k)) fun x => q) ↑c
<VAR>q : ℍ<VAR>hq : q.re = 0<VAR>c s : ℝ<VAR>hc : HasSum (fun a => ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c<VAR>hs : HasSum (fun z => ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)<GOAL>HasSum (fun k => (expSeries ℝ ℍ (2 * k + 1)) fun x => q) ((s / ‖q‖) • q)
<VAR>α : Type<VAR>d : ℕ<VAR>ds ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝¹ : Monoid α<VAR>inst✝ : AddMonoid α<VAR>n : ℕ<VAR>x y : Holor α ds<VAR>hx : CPRankMax 0 x<VAR>hy : CPRankMax n y<GOAL>CPRankMax (0 + n) (x + y)
<VAR>α : Type<VAR>d : ℕ<VAR>ds ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝¹ : Monoid α<VAR>inst✝ : AddMonoid α<VAR>m n : ℕ<VAR>y x₁ x₂ : Holor α ds<VAR>hx₁ : x₁.CPRankMax1<VAR>hx₂ : CPRankMax m x₂<VAR>hy : CPRankMax n y<GOAL>CPRankMax (m + 1 + n) (x₁ + x₂ + y)
<VAR>α : Type<VAR>d : ℕ<VAR>ds ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝¹ : Monoid α<VAR>inst✝ : AddMonoid α<VAR>m n : ℕ<VAR>y x₁ x₂ : Holor α ds<VAR>hx₁ : x₁.CPRankMax1<VAR>hx₂ : CPRankMax m x₂<VAR>hy : CPRankMax n y<GOAL>CPRankMax (n + (m + 1)) (x₁ + (x₂ + y))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>s : Set α<GOAL>diam (closure s) = diam s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ closure s<VAR>y : α<VAR>hy : y ∈ closure s<GOAL>edist x y ≤ diam s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ closure s<VAR>y : α<VAR>hy : y ∈ closure s<VAR>this : edist x y ∈ closure (Iic (diam s))<GOAL>edist x y ≤ diam s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>s : Set E<VAR>r : ℝ<VAR>x✝ x : E<GOAL>gauge (ball 0 1) x = ‖x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝¹ : Lattice α<VAR>inst✝ : OrderBot α<VAR>s t : Finset ι<VAR>f : ι → α<VAR>i : ι<GOAL>(s.attach.SupIndep fun a => f ↑a) ↔ s.SupIndep f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝¹ : Lattice α<VAR>inst✝ : OrderBot α<VAR>s t✝ : Finset ι<VAR>f : ι → α<VAR>i✝ : ι<VAR>h : s.attach.SupIndep fun a => f ↑a<VAR>t : Finset ι<VAR>ht : t ⊆ s<VAR>i : ι<VAR>his : i ∈ s<VAR>hit : i ∉ t<GOAL>Disjoint (f i) (t.sup f)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>H : ∀ (x : α), ∃ n, x < ↑n<VAR>x y : α<VAR>y0 : 0 < y<VAR>n : ℕ<VAR>h : x / y < ↑n<GOAL>x < n • y
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i : ι<VAR>b : B<VAR>a : F<VAR>p : Z.TotalSpace<GOAL>↑(Z.localTrivAt p.proj) p = (p.proj, p.snd)
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i : ι<VAR>b : B<VAR>a : F<VAR>p : Z.TotalSpace<GOAL>p.proj ∈ Z.baseSet (Z.indexAt p.proj)
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>ha : a ≠ 0<GOAL>(C a * X).degree = 1
<VAR>α : Type u_1<VAR>inst✝¹ : BEq α<VAR>inst✝ : LawfulBEq α<VAR>a : α<VAR>l : List α<VAR>h : a ∈ l<GOAL>∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l.erase a = l₁ ++ l₂
<VAR>α : Type u_1<VAR>inst✝¹ : BEq α<VAR>inst✝ : LawfulBEq α<VAR>a : α<VAR>l : List α<VAR>h : a ∈ l<VAR>w✝ : α<VAR>l₁ l₂ : List α<VAR>h₁ : ∀ (b : α), b ∈ l₁ → ¬(a == b) = true<VAR>e : (a == w✝) = true<VAR>h₂ : l = l₁ ++ w✝ :: l₂<VAR>h₃ : eraseP (BEq.beq a) l = l₁ ++ l₂<GOAL>∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l.erase a = l₁ ++ l₂
<VAR>α : Type u_1<VAR>inst✝¹ : BEq α<VAR>inst✝ : LawfulBEq α<VAR>a : α<VAR>l : List α<VAR>h : a ∈ l<VAR>w✝ : α<VAR>l₁ l₂ : List α<VAR>h₁ : ∀ (b : α), b ∈ l₁ → ¬(a == b) = true<VAR>e : (a == w✝) = true<VAR>h₂ : l = l₁ ++ w✝ :: l₂<VAR>h₃ : eraseP (BEq.beq a) l = l₁ ++ l₂<GOAL>∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁ ++ a :: l₂ ∧ eraseP (fun x => a == x) l = l₁ ++ l₂
<VAR>M : Type u_1<VAR>inst✝ : OrderedAddCommMonoid M<VAR>f : ℕ → M<VAR>u : ℕ → ℕ<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<VAR>n : ℕ<GOAL>∑ k ∈ Ico 1 (2 ^ n), f k ≤ ∑ k ∈ range n, 2 ^ k • f (2 ^ k)
<VAR>M : Type u_1<VAR>inst✝ : OrderedAddCommMonoid M<VAR>f : ℕ → M<VAR>u : ℕ → ℕ<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<VAR>n x✝ : ℕ<VAR>a✝ : x✝ ∈ range n<GOAL>2 ^ x✝ • f (2 ^ x✝) = (2 ^ (x✝ + 1) - 2 ^ x✝) • f (2 ^ x✝)
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>hμm this : SigmaFinite (μ.trim hm)<GOAL>StronglyMeasurable (μ[f|m])
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>hμm this : SigmaFinite (μ.trim hm)<GOAL>StronglyMeasurable (if Integrable f μ then if StronglyMeasurable f then f else AEStronglyMeasurable'.mk ↑↑(condexpL1 hm μ f) ⋯ else 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : α → β<VAR>s✝ t✝ : Set α<VAR>f : α → β<VAR>s t : Set α<GOAL>f '' s \ f '' t ⊆ f '' (s \ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : α → β<VAR>s✝ t✝ : Set α<VAR>f : α → β<VAR>s t : Set α<GOAL>f '' s ⊆ f '' (t ∪ s)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f✝ : α → ℝ<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ<GOAL>0 ≤ᶠ[ae μ] f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f✝ : α → ℝ<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ<GOAL>∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ᵐ (x : α) ∂μ.restrict s, 0 x ≤ f x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f✝ : α → ℝ<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ<VAR>t : Set α<VAR>t_meas : MeasurableSet t<VAR>t_lt_top : μ t < ⊤<GOAL>∀ᵐ (x : α) ∂μ.restrict t, 0 x ≤ f x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f✝ : α → ℝ<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ<VAR>t : Set α<VAR>t_meas : MeasurableSet t<VAR>t_lt_top : μ t < ⊤<GOAL>∀ (s : Set α), MeasurableSet s → μ (s ∩ t) < ⊤ → 0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t✝ : Set α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f✝ : α → ℝ<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ<VAR>t : Set α<VAR>t_meas : MeasurableSet t<VAR>t_lt_top : μ t < ⊤<VAR>s : Set α<VAR>s_meas : MeasurableSet s<VAR>a✝ : μ (s ∩ t) < ⊤<GOAL>0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₀ p₁ p₂ : P<VAR>v v₁ v₂ v₃ : V<GOAL>∠ (v - v₁) (v - v₂) (v - v₃) = ∠ v₁ v₂ v₃
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Fintype F<VAR>inst✝ : DecidableEq F<GOAL>(quadraticChar F) 0 = 0
<VAR>α : Type u<VAR>l : List α<GOAL>l.rotate' l.length = l
<VAR>α : Type u<VAR>l : List α<GOAL>drop l.length l ++ take l.length l = l
<VAR>X Y Z : RelCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>x : X<VAR>z : Z<GOAL>(f ≫ g) x z ↔ ∃ y, f x y ∧ g y z
<VAR>ι : Type uι<VAR>R : Type uR<VAR>A : ι → Type uA<VAR>B : Type uB<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (A i)<VAR>inst✝⁵ : (i : ι) → Module R (A i)<VAR>inst✝⁴ : AddMonoid ι<VAR>inst✝³ : GSemiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : GAlgebra R A<VAR>inst✝ : Algebra R B<VAR>i j : ι<VAR>a : A i<VAR>r : R<VAR>x : A j<GOAL>{ toFun := fun b => GradedMonoid.GMul.mul a b, map_add' := ⋯ }.toFun (r • x) = (RingHom.id R) r • { toFun := fun b => GradedMonoid.GMul.mul a b, map_add' := ⋯ }.toFun x
<VAR>ι : Type uι<VAR>R : Type uR<VAR>A : ι → Type uA<VAR>B : Type uB<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (A i)<VAR>inst✝⁵ : (i : ι) → Module R (A i)<VAR>inst✝⁴ : AddMonoid ι<VAR>inst✝³ : GSemiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : GAlgebra R A<VAR>inst✝ : Algebra R B<VAR>i j : ι<VAR>r : R<VAR>x : A i<VAR>y : A j<GOAL>({ toFun := fun a => { toFun := fun b => GradedMonoid.GMul.mul a b, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯ }.toFun (r • x)) y = ((RingHom.id R) r • { toFun := fun a => { toFun := fun b => GradedMonoid.GMul.mul a b, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯ }.toFun x) y
<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✝¹ : AddCommMonoid M✝<VAR>v v₁ v₂ : α →₀ M✝<VAR>M : Type u_13<VAR>inst✝ : AddCommMonoid M<VAR>f : α ≃ β<VAR>l : α →₀ M<VAR>x : β<GOAL>(equivMapDomain f l) x = (mapDomain (⇑f) l) x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁹ : Category.{u_4, u_1} C<VAR>inst✝⁸ : Category.{u_6, u_2} D<VAR>F : C ⥤ D<VAR>ι : Type u_3<VAR>c : ComplexShape ι<VAR>inst✝⁷ : Preadditive C<VAR>inst✝⁶ : Preadditive D<VAR>inst✝⁵ : CategoryWithHomology C<VAR>inst✝⁴ : CategoryWithHomology D<VAR>inst✝³ : (HomologicalComplex.quasiIso C c).HasLocalization<VAR>inst✝² : (HomologicalComplex.quasiIso D c).HasLocalization<VAR>inst✝¹ : F.Additive<VAR>inst✝ : F.PreservesHomology<GOAL>(HomologicalComplex.quasiIso C c).IsInvertedBy (F.mapHomologicalComplex c ⋙ HomologicalComplexUpToQuasiIso.Q)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s✝ t✝ : Multiset α<VAR>a✝ : α<VAR>inst✝ : DecidableEq α<VAR>s t : Multiset α<VAR>x✝ : s.Nodup ∧ t.Nodup<VAR>h₁ : s.Nodup<VAR>h₂ : t.Nodup<VAR>a : α<GOAL>count a (s ∪ t) ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s✝ t✝ : Multiset α<VAR>a✝ : α<VAR>inst✝ : DecidableEq α<VAR>s t : Multiset α<VAR>x✝ : s.Nodup ∧ t.Nodup<VAR>h₁ : s.Nodup<VAR>h₂ : t.Nodup<VAR>a : α<GOAL>max (count a s) (count a t) ≤ 1
<VAR>x✝ y z x : ℝ<VAR>n : ℕ<GOAL>x ^ ↑n = x ^ n
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.41028, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<GOAL>S.v₁₂.τ₃ ≫ S.v₂₃.τ₃ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n : ℕ<VAR>s : Finset α<VAR>h : G.CliqueFree n<VAR>v w : α<GOAL>(G ⊔ edge v w).CliqueFree (n + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n : ℕ<VAR>s : Finset α<VAR>v w : α<VAR>h : ¬(G ⊔ edge v w).CliqueFree (n + 1)<GOAL>¬G.CliqueFree n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n : ℕ<VAR>s : Finset α<VAR>v w : α<VAR>h : ¬(G ⊔ edge v w).CliqueFree (n + 1)<VAR>f : Fin (n + 1) ↪ α<VAR>ha : ∀ {a b : Fin (n + 1)}, (G ⊔ edge v w).Adj (f a) (f b) ↔ ⊤.Adj a b<GOAL>¬G.CliqueFree n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n : ℕ<VAR>s : Finset α<VAR>v w : α<VAR>h : ¬(G ⊔ edge v w).CliqueFree (n + 1)<VAR>f : Fin (n + 1) ↪ α<VAR>ha : ∀ {a b : Fin (n + 1)}, (G ⊔ edge v w).Adj (f a) (f b) ↔ ¬a = b<GOAL>¬G.CliqueFree n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n : ℕ<VAR>s : Finset α<VAR>v w : α<VAR>h : ¬(G ⊔ edge v w).CliqueFree (n + 1)<VAR>f : Fin (n + 1) ↪ α<VAR>ha : ∀ {a b : Fin (n + 1)}, (G ⊔ edge v w).Adj (f a) (f b) ↔ ¬a = b<GOAL>Nonempty (⊤ ↪g G)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>i : ι<VAR>hi : ¬c.Rel i (c.next i)<GOAL>((if hi : c.Rel i (c.next i) then (XIsoBiprod φ i (c.next i) hi).hom ≫ biprod.snd else (XIso φ i hi).hom) ≫ if hi : c.Rel i (c.next i) then biprod.inr ≫ (XIsoBiprod φ i (c.next i) hi).inv else (XIso φ i hi).inv) = 𝟙 (X φ i)
<VAR>a n : ℕ<GOAL>(filter a.Coprime (Ico n (n + a))).card = φ a
<VAR>a n : ℕ<GOAL>Function.Periodic a.Coprime a
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : Ring R'<VAR>inst✝³ : AddZeroClass A<VAR>inst✝² : SemilatticeInf T<VAR>inst✝¹ : Add T<VAR>inst✝ : OrderTop T<VAR>D : A → T<VAR>s : R[A]<VAR>hs : s.support.Nonempty<GOAL>s.support.inf (WithTop.some ∘ D) = ↑(s.support.inf D)
<VAR>R : Type u_1<VAR>inst✝¹ : AddGroupWithOne R<VAR>p : ℕ<VAR>inst✝ : CharP R p<VAR>a b : ℤ<GOAL>↑a = ↑b ↔ a ≡ b [ZMOD ↑p]
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝³ : Mul α<VAR>inst✝² : IsSymmOp α α fun x x_1 => x * x_1<VAR>inst✝¹ : Zero α<VAR>inst✝ : Preorder α<GOAL>PosMulReflectLT α ↔ MulPosReflectLT α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivInvMonoid G<VAR>a b c x : G<GOAL>x⁻¹ = 1 / x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c d : α<GOAL>a ∆ (b ∆ c) = b ∆ (a ∆ c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>e : α ≃ᵐ β<GOAL>MeasurableSet (⇑e '' s) ↔ MeasurableSet s
<VAR>α : Type u_1<VAR>inst✝⁴ : Fintype α<VAR>inst✝³ : DecidableEq α<VAR>β : Type u_2<VAR>inst✝² : Fintype β<VAR>inst✝¹ : DecidableEq β<VAR>p : β → Prop<VAR>inst✝ : DecidablePred p<VAR>f : α ≃ Subtype p<VAR>g : Perm α<GOAL>(g.extendDomain f).cycleType = g.cycleType
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ✝ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ✝<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ✝<VAR>inst✝² : NormedAddCommGroup E<VAR>γ : Type u_7<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : TopologicalSpace γ<VAR>f : α × β → γ<VAR>hf : AEStronglyMeasurable f (μ.prod ν)<GOAL>∀ᵐ (x : α) ∂μ, AEStronglyMeasurable (fun y => f (x, y)) ν
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ✝ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ✝<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ✝<VAR>inst✝² : NormedAddCommGroup E<VAR>γ : Type u_7<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : TopologicalSpace γ<VAR>f : α × β → γ<VAR>hf : AEStronglyMeasurable f (μ.prod ν)<VAR>x : α<VAR>hx : ∀ᵐ (y : β) ∂ν, f (x, y) = AEStronglyMeasurable.mk f hf (x, y)<GOAL>AEStronglyMeasurable (fun y => f (x, y)) ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : DenselyOrdered α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : T2Space β<VAR>f : α → β<VAR>a b : α<VAR>la : β<VAR>hab : a < b<VAR>ha : Tendsto f (𝓝[>] a) (𝓝 la)<GOAL>extendFrom (Ioo a b) f a = la
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : DenselyOrdered α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : T2Space β<VAR>f : α → β<VAR>a b : α<VAR>la : β<VAR>hab : a < b<VAR>ha : Tendsto f (𝓝[>] a) (𝓝 la)<GOAL>a ∈ closure (Ioo a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : DenselyOrdered α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : T2Space β<VAR>f : α → β<VAR>a b : α<VAR>la : β<VAR>hab : a < b<VAR>ha : Tendsto f (𝓝[>] a) (𝓝 la)<GOAL>Tendsto f (𝓝[Ioo a b] a) (𝓝 la)
<VAR>α : Type u<VAR>c : Cardinal.{v}<GOAL>toPartENat (lift.{u, v} c) = toPartENat c
<VAR>C : Type u_2<VAR>inst✝⁵ : Category.{u_1, u_2} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>S₁ S₂ S₃ S₄ : ShortComplex C<VAR>inst✝³ : S₁.HasHomology<VAR>inst✝² : S₂.HasHomology<VAR>inst✝¹ : S₃.HasHomology<VAR>inst✝ : S₄.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>φ' : S₂ ⟶ S₃<VAR>hφ : QuasiIso φ<VAR>hφφ' : QuasiIso (φ ≫ φ')<GOAL>QuasiIso φ'
<VAR>C : Type u_2<VAR>inst✝⁵ : Category.{u_1, u_2} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>S₁ S₂ S₃ S₄ : ShortComplex C<VAR>inst✝³ : S₁.HasHomology<VAR>inst✝² : S₂.HasHomology<VAR>inst✝¹ : S₃.HasHomology<VAR>inst✝ : S₄.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>φ' : S₂ ⟶ S₃<VAR>hφ : IsIso (homologyMap φ)<VAR>hφφ' : IsIso (homologyMap (φ ≫ φ'))<GOAL>IsIso (homologyMap φ')
<VAR>C : Type u_2<VAR>inst✝⁵ : Category.{u_1, u_2} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>S₁ S₂ S₃ S₄ : ShortComplex C<VAR>inst✝³ : S₁.HasHomology<VAR>inst✝² : S₂.HasHomology<VAR>inst✝¹ : S₃.HasHomology<VAR>inst✝ : S₄.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>φ' : S₂ ⟶ S₃<VAR>hφ : IsIso (homologyMap φ)<VAR>hφφ' : IsIso (homologyMap φ ≫ homologyMap φ')<GOAL>IsIso (homologyMap φ')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g✝ : Filter β<VAR>f₁ f₂ : Filter α<VAR>g : Filter β<GOAL>(f₁ ⊔ f₂).prod g = f₁.prod g ⊔ f₂.prod g
<VAR>G : Type u_1<VAR>inst✝² : SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup H<VAR>K : Type u_3<VAR>inst✝ : SeminormedAddCommGroup K<VAR>f : NormedAddGroupHom G H<VAR>C : ℝ<VAR>h : f.SurjectiveOnWith f.range C<GOAL>↑f.completion.ker = closure ↑(toCompl.comp (incl f.ker)).range
<VAR>G : Type u_1<VAR>inst✝² : SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup H<VAR>K : Type u_3<VAR>inst✝ : SeminormedAddCommGroup K<VAR>f : NormedAddGroupHom G H<VAR>C : ℝ<VAR>h : f.SurjectiveOnWith f.range C<GOAL>↑f.completion.ker ≤ closure ↑(toCompl.comp (incl f.ker)).range
<VAR>G : Type u_1<VAR>inst✝² : SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup H<VAR>K : Type u_3<VAR>inst✝ : SeminormedAddCommGroup K<VAR>f : NormedAddGroupHom G H<VAR>C : ℝ<VAR>h : f.SurjectiveOnWith f.range C<VAR>hatg : Completion G<VAR>hatg_in : f.completion hatg = 0<GOAL>hatg ∈ closure ↑(toCompl.comp (incl f.ker)).range
<VAR>G : Type u_1<VAR>inst✝² : SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup H<VAR>K : Type u_3<VAR>inst✝ : SeminormedAddCommGroup K<VAR>f : NormedAddGroupHom G H<VAR>C : ℝ<VAR>h : f.SurjectiveOnWith f.range C<VAR>hatg : Completion G<VAR>hatg_in : f.completion hatg = 0<GOAL>∀ (ε : ℝ), 0 < ε → ∃ b ∈ ↑(toCompl.comp (incl f.ker)).range, ‖hatg - b‖ < ε
<VAR>G : Type u_1<VAR>inst✝² : SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup H<VAR>K : Type u_3<VAR>inst✝ : SeminormedAddCommGroup K<VAR>f : NormedAddGroupHom G H<VAR>C : ℝ<VAR>h : f.SurjectiveOnWith f.range C<VAR>hatg : Completion G<VAR>hatg_in : f.completion hatg = 0<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<GOAL>∃ b ∈ ↑(toCompl.comp (incl f.ker)).range, ‖hatg - b‖ < ε
<VAR>G : Type u_1<VAR>inst✝² : SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup H<VAR>K : Type u_3<VAR>inst✝ : SeminormedAddCommGroup K<VAR>f : NormedAddGroupHom G H<VAR>C : ℝ<VAR>h : f.SurjectiveOnWith f.range C<VAR>hatg : Completion G<VAR>hatg_in : f.completion hatg = 0<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>C' : ℝ<VAR>C'_pos : C' > 0<VAR>hC' : f.SurjectiveOnWith f.range C'<GOAL>∃ b ∈ ↑(toCompl.comp (incl f.ker)).range, ‖hatg - b‖ < ε
<VAR>G : Type u_1<VAR>inst✝² : SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup H<VAR>K : Type u_3<VAR>inst✝ : SeminormedAddCommGroup K<VAR>f : NormedAddGroupHom G H<VAR>C : ℝ<VAR>h : f.SurjectiveOnWith f.range C<VAR>hatg : Completion G<VAR>hatg_in : f.completion hatg = 0<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>C' : ℝ<VAR>C'_pos : C' > 0<VAR>hC' : f.SurjectiveOnWith f.range C'<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>hδ : (1 + C' * ‖f‖) * δ < ε<GOAL>∃ b ∈ ↑(toCompl.comp (incl f.ker)).range, ‖hatg - b‖ < ε
<VAR>G : Type u_1<VAR>inst✝² : SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup H<VAR>K : Type u_3<VAR>inst✝ : SeminormedAddCommGroup K<VAR>f : NormedAddGroupHom G H<VAR>C : ℝ<VAR>h : f.SurjectiveOnWith f.range C<VAR>hatg : Completion G<VAR>hatg_in : f.completion hatg = 0<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>C' : ℝ<VAR>C'_pos : C' > 0<VAR>hC' : f.SurjectiveOnWith f.range C'<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>hδ : (1 + C' * ‖f‖) * δ < ε<VAR>g : G<VAR>hg : ‖hatg - ↑G g‖ < δ<GOAL>∃ b ∈ ↑(toCompl.comp (incl f.ker)).range, ‖hatg - b‖ < ε
<VAR>G : Type u_1<VAR>inst✝² : SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup H<VAR>K : Type u_3<VAR>inst✝ : SeminormedAddCommGroup K<VAR>f : NormedAddGroupHom G H<VAR>C : ℝ<VAR>h : f.SurjectiveOnWith f.range C<VAR>hatg : Completion G<VAR>hatg_in : f.completion hatg = 0<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>C' : ℝ<VAR>C'_pos : C' > 0<VAR>hC' : f.SurjectiveOnWith f.range C'<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>hδ : (1 + C' * ‖f‖) * δ < ε<VAR>g : G<VAR>hg : ‖hatg - ↑G g‖ < δ<VAR>g' : G<VAR>hgg' : f g' = f g<VAR>hfg : ‖g'‖ ≤ C' * ‖f g‖<GOAL>∃ b ∈ ↑(toCompl.comp (incl f.ker)).range, ‖hatg - b‖ < ε