ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁✝ c₂✝ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f₁ f₂ : α → R<VAR>g₁ g₂ : α → 𝕜<VAR>c₁ c₂ : ℝ<VAR>h₁ : IsBigOWith c₁ l f₁ g₁<VAR>h₂ : IsBigOWith c₂ l f₂ g₂<GOAL>IsBigOWith (c₁ * c₂) l (fun x => f₁ x * f₂ x) fun x => g₁ x * g₂ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁✝ c₂✝ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f₁ f₂ : α → R<VAR>g₁ g₂ : α → 𝕜<VAR>c₁ c₂ : ℝ<VAR>h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖<VAR>h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖<GOAL>∀ᶠ (x : α) in l, ‖f₁ x * f₂ x‖ ≤ c₁ * c₂ * ‖g₁ x * g₂ x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁✝ c₂✝ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f₁ f₂ : α → R<VAR>g₁ g₂ : α → 𝕜<VAR>c₁ c₂ : ℝ<VAR>h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖<VAR>h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖<VAR>a✝ : α<VAR>hx₁ : ‖f₁ a✝‖ ≤ c₁ * ‖g₁ a✝‖<VAR>hx₂ : ‖f₂ a✝‖ ≤ c₂ * ‖g₂ a✝‖<GOAL>‖f₁ a✝ * f₂ a✝‖ ≤ c₁ * c₂ * ‖g₁ a✝ * g₂ a✝‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁✝ c₂✝ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f₁ f₂ : α → R<VAR>g₁ g₂ : α → 𝕜<VAR>c₁ c₂ : ℝ<VAR>h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖<VAR>h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖<VAR>a✝ : α<VAR>hx₁ : ‖f₁ a✝‖ ≤ c₁ * ‖g₁ a✝‖<VAR>hx₂ : ‖f₂ a✝‖ ≤ c₂ * ‖g₂ a✝‖<GOAL>‖f₁ a✝‖ * ‖f₂ a✝‖ ≤ c₁ * c₂ * ‖g₁ a✝ * g₂ a✝‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁✝ c₂✝ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f₁ f₂ : α → R<VAR>g₁ g₂ : α → 𝕜<VAR>c₁ c₂ : ℝ<VAR>h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖<VAR>h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖<VAR>a✝ : α<VAR>hx₁ : ‖f₁ a✝‖ ≤ c₁ * ‖g₁ a✝‖<VAR>hx₂ : ‖f₂ a✝‖ ≤ c₂ * ‖g₂ a✝‖<GOAL>c₁ * c₂ * ‖g₁ a✝ * g₂ a✝‖ = c₁ * ‖g₁ a✝‖ * (c₂ * ‖g₂ a✝‖)
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>s : Finset I<VAR>a : I<VAR>as : List I<VAR>ha : List.Chain' (fun x x_1 => x > x_1) (a :: as)<VAR>c : Products I →₀ ℤ<VAR>hc : ↑c.support ⊆ {m | ↑m ≤ as}<GOAL>(c.sum fun a_1 b => e (π C fun x => x ∈ s) a * b • Products.eval (π C fun x => x ∈ s) a_1) ∈ Submodule.span ℤ (Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ a :: as})
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>s : Finset I<VAR>a : I<VAR>as : List I<VAR>ha : List.Chain' (fun x x_1 => x > x_1) (a :: as)<VAR>c : Products I →₀ ℤ<VAR>hc : ↑c.support ⊆ {m | ↑m ≤ as}<GOAL>∀ (c_1 : Products I), c c_1 ≠ 0 → e (π C fun x => x ∈ s) a * c c_1 • Products.eval (π C fun x => x ∈ s) c_1 ∈ Submodule.span ℤ (Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ a :: as})
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>s : Finset I<VAR>a : I<VAR>as : List I<VAR>ha : List.Chain' (fun x x_1 => x > x_1) (a :: as)<VAR>c : Products I →₀ ℤ<VAR>hc : ↑c.support ⊆ {m | ↑m ≤ as}<VAR>m : Products I<VAR>hm : c m ≠ 0<VAR>hsm : ∀ (c : ℤ) (x : LocallyConstant ↑(π C fun x => x ∈ s) ℤ), e (π C fun x => x ∈ s) a * c • x = c • (e (π C fun x => x ∈ s) a * x)<GOAL>c m • (e (π C fun x => x ∈ s) a * Products.eval (π C fun x => x ∈ s) m) ∈ Submodule.span ℤ (Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ a :: as})
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>s : Finset I<VAR>a : I<VAR>as : List I<VAR>ha : List.Chain' (fun x x_1 => x > x_1) (a :: as)<VAR>c : Products I →₀ ℤ<VAR>hc : ↑c.support ⊆ {m | ↑m ≤ as}<VAR>m : Products I<VAR>hm : c m ≠ 0<VAR>hsm : ∀ (c : ℤ) (x : LocallyConstant ↑(π C fun x => x ∈ s) ℤ), e (π C fun x => x ∈ s) a * c • x = c • (e (π C fun x => x ∈ s) a * x)<GOAL>e (π C fun x => x ∈ s) a * Products.eval (π C fun x => x ∈ s) m ∈ Submodule.span ℤ (Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ a :: as})
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>s : Finset I<VAR>a : I<VAR>as : List I<VAR>ha : List.Chain' (fun x x_1 => x > x_1) (a :: as)<VAR>c : Products I →₀ ℤ<VAR>hc : ↑c.support ⊆ {m | ↑m ≤ as}<VAR>m : Products I<VAR>hm : c m ≠ 0<VAR>hsm : ∀ (c : ℤ) (x : LocallyConstant ↑(π C fun x => x ∈ s) ℤ), e (π C fun x => x ∈ s) a * c • x = c • (e (π C fun x => x ∈ s) a * x)<GOAL>e (π C fun x => x ∈ s) a * Products.eval (π C fun x => x ∈ s) m ∈ Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ a :: as}
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>s : Finset I<VAR>a : I<VAR>as : List I<VAR>ha : List.Chain' (fun x x_1 => x > x_1) (a :: as)<VAR>c : Products I →₀ ℤ<VAR>hc : ↑c.support ⊆ {m | ↑m ≤ as}<VAR>m : Products I<VAR>hm : c m ≠ 0<VAR>hsm : ∀ (c : ℤ) (x : LocallyConstant ↑(π C fun x => x ∈ s) ℤ), e (π C fun x => x ∈ s) a * c • x = c • (e (π C fun x => x ∈ s) a * x)<VAR>hmas : ↑m ≤ as<GOAL>e (π C fun x => x ∈ s) a * Products.eval (π C fun x => x ∈ s) m ∈ Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ a :: as}
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>s : Finset I<VAR>a : I<VAR>as : List I<VAR>ha : List.Chain' (fun x x_1 => x > x_1) (a :: as)<VAR>c : Products I →₀ ℤ<VAR>hc : ↑c.support ⊆ {m | ↑m ≤ as}<VAR>m : Products I<VAR>hm : c m ≠ 0<VAR>hsm : ∀ (c : ℤ) (x : LocallyConstant ↑(π C fun x => x ∈ s) ℤ), e (π C fun x => x ∈ s) a * c • x = c • (e (π C fun x => x ∈ s) a * x)<VAR>hmas : ↑m ≤ as<GOAL>Products.eval (π C fun x => x ∈ s) ⟨a :: ↑m, ⋯⟩ = e (π C fun x => x ∈ s) a * Products.eval (π C fun x => x ∈ s) m
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>H K : Subgroup G<VAR>N : Type u_5<VAR>inst✝ : Group N<GOAL>NormalizerCondition G ↔ ∀ (H : Subgroup G), H.normalizer = H → H = ⊤
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>H K : Subgroup G<VAR>N : Type u_5<VAR>inst✝ : Group N<GOAL>∀ (a : Subgroup G), a < ⊤ → a < a.normalizer ↔ a.normalizer = a → a = ⊤
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>H✝ K : Subgroup G<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>H : Subgroup G<GOAL>H < ⊤ → H < H.normalizer ↔ H.normalizer = H → H = ⊤
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>H✝ K : Subgroup G<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>H : Subgroup G<GOAL>¬H = ⊤ → ¬H = H.normalizer ↔ H.normalizer = H → H = ⊤
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<VAR>n : ℕ<GOAL>term (f ⍟ g) s n = ∑ p ∈ n.divisorsAntidiagonal, term f s p.1 * term g s p.2
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<GOAL>term (f ⍟ g) s 0 = ∑ p ∈ divisorsAntidiagonal 0, term f s p.1 * term g s p.2
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>term (f ⍟ g) s n = ∑ p ∈ n.divisorsAntidiagonal, term f s p.1 * term g s p.2
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>∑ i ∈ n.divisorsAntidiagonal, f i.1 * g i.2 / ↑n ^ s = ∑ p ∈ n.divisorsAntidiagonal, term f s p.1 * term g s p.2
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>p : ℕ × ℕ<VAR>hp : p ∈ n.divisorsAntidiagonal<GOAL>f p.1 * g p.2 / ↑n ^ s = term f s p.1 * term g s p.2
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>p : ℕ × ℕ<VAR>hp : p ∈ n.divisorsAntidiagonal<VAR>hp₁ : p.1 ≠ 0<VAR>hp₂ : p.2 ≠ 0<GOAL>f p.1 * g p.2 / ↑n ^ s = term f s p.1 * term g s p.2
<VAR>n : ℕ<VAR>c✝ c : Composition n<GOAL>c = ones n ↔ n ≤ c.length
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>f : α → β → β<VAR>H : LeftCommutative f<VAR>x : β<VAR>q : α → Prop<VAR>p : β → Prop<VAR>s : Multiset α<VAR>hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)<VAR>px : p x<VAR>q_s : ∀ a ∈ s, q a<GOAL>p (foldr f H x s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>mδ : MeasurableSpace δ<VAR>f✝ : β → γ<VAR>g✝ : γ → α<VAR>κ : Kernel β γ<VAR>f : α → β<VAR>g : γ → δ<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>x : α<VAR>s : Set δ<VAR>a✝ : MeasurableSet s<GOAL>(((κ.map g hg).comap f hf) x) s = (((κ.comap f hf).map g hg) x) s
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t u : Finset α<VAR>P : Finpartition s<VAR>a : α<VAR>ha : a ∈ s<GOAL>P.part a ∈ P.parts
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Ring α<VAR>inst✝⁴ : LinearOrder α<VAR>a b : α<VAR>inst✝³ : MulPosStrictMono α<VAR>inst✝² : PosMulStrictMono α<VAR>inst✝¹ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
<VAR>V : Type u<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>v w : V<VAR>h : G.IsSRGWith n k ℓ μ<VAR>hne : v ≠ w<VAR>ha : ¬G.Adj v w<GOAL>(G.neighborFinset v ∪ G.neighborFinset w).card = 2 * k - μ
<VAR>V : Type u<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>v w : V<VAR>h : G.IsSRGWith n k ℓ μ<VAR>hne : v ≠ w<VAR>ha : ¬G.Adj v w<GOAL>(G.neighborFinset v ∪ G.neighborFinset w).card = 2 * k - Fintype.card ↑(G.commonNeighbors v w)
<VAR>U : Type u_1<VAR>inst✝ : Quiver U<VAR>u v u' v' : U<VAR>hu : u = u'<VAR>hv : v = v'<VAR>e : u ⟶ v<VAR>e' : u' ⟶ v'<GOAL>cast hu hv e = e' ↔ HEq e e'
<VAR>U : Type u_1<VAR>inst✝ : Quiver U<VAR>u v u' v' : U<VAR>hu : u = u'<VAR>hv : v = v'<VAR>e : u ⟶ v<VAR>e' : u' ⟶ v'<GOAL>_root_.cast ⋯ e = e' ↔ HEq e e'
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R✝ I J X Y : Set α<VAR>hI : M.Basis I X<VAR>R : Set α<VAR>hR : R ⊆ M.E<VAR>hX : X ⊆ (M ↾ R).E<GOAL>(M ↾ R).Basis I X
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B : ℝ<GOAL>IsCompact (convexBodySum K B)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B : ℝ<GOAL>IsClosed (convexBodySum K B) ∧ Bornology.IsBounded (convexBodySum K B)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B : ℝ<GOAL>IsClosed (convexBodySum K B)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B : ℝ<GOAL>convexBodySum K B = convexBodySumFun ⁻¹' Set.Icc 0 B
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B : ℝ<VAR>x✝ : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>x✝ ∈ convexBodySum K B ↔ x✝ ∈ convexBodySumFun ⁻¹' Set.Icc 0 B
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h₁ : c ≤ b<VAR>h₂ : a ≤ d<VAR>x : α<GOAL>x ∈ Ico a b ∪ Ico c d ↔ x ∈ Ico (min a c) (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h₁ : c ≤ b<VAR>h₂ : a ≤ d<VAR>x : α<GOAL>a ≤ x ∧ x < b ∨ c ≤ x ∧ x < d ↔ (a ≤ x ∨ c ≤ x) ∧ (x < b ∨ x < d)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>x : R<VAR>hx : ∀ (y : R), f (x * y) ≤ f x * f y<VAR>h_one : f 1 ≤ 1<GOAL>⨆ y, f (x * y) / f y = f x
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>x : R<VAR>hx : ∀ (y : R), f (x * y) ≤ f x * f y<VAR>h_one : f 1 ≤ 1<GOAL>⨆ y, f (x * y) / f y ≤ f x
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>x : R<VAR>hx : ∀ (y : R), f (x * y) ≤ f x * f y<VAR>h_one : f 1 ≤ 1<GOAL>f x ≤ ⨆ y, f (x * y) / f y
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>𝓕 : Type u_3<VAR>inst✝⁴ : SeminormedAddGroup E<VAR>inst✝³ : SeminormedAddCommGroup F<VAR>inst✝² : FunLike 𝓕 E F<VAR>inst✝¹ : ZeroAtInftyContinuousMapClass 𝓕 E F<VAR>inst✝ : ProperSpace E<VAR>f : E → F<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε<GOAL>Tendsto f (cocompact E) (𝓝 0)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>𝓕 : Type u_3<VAR>inst✝⁴ : SeminormedAddGroup E<VAR>inst✝³ : SeminormedAddCommGroup F<VAR>inst✝² : FunLike 𝓕 E F<VAR>inst✝¹ : ZeroAtInftyContinuousMapClass 𝓕 E F<VAR>inst✝ : ProperSpace E<VAR>f : E → F<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε<GOAL>Tendsto (fun x => ‖f x‖) (cocompact E) (𝓝 0)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>𝓕 : Type u_3<VAR>inst✝⁴ : SeminormedAddGroup E<VAR>inst✝³ : SeminormedAddCommGroup F<VAR>inst✝² : FunLike 𝓕 E F<VAR>inst✝¹ : ZeroAtInftyContinuousMapClass 𝓕 E F<VAR>inst✝ : ProperSpace E<VAR>f : E → F<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε<VAR>s : Set ℝ<VAR>hs : s ∈ 𝓝 0<GOAL>s ∈ map (fun x => ‖f x‖) (cocompact E)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>𝓕 : Type u_3<VAR>inst✝⁴ : SeminormedAddGroup E<VAR>inst✝³ : SeminormedAddCommGroup F<VAR>inst✝² : FunLike 𝓕 E F<VAR>inst✝¹ : ZeroAtInftyContinuousMapClass 𝓕 E F<VAR>inst✝ : ProperSpace E<VAR>f : E → F<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε<VAR>s : Set ℝ<VAR>hs : s ∈ 𝓝 0<GOAL>∃ r, (Metric.closedBall 0 r)ᶜ ⊆ (fun x => ‖f x‖) ⁻¹' s
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>𝓕 : Type u_3<VAR>inst✝⁴ : SeminormedAddGroup E<VAR>inst✝³ : SeminormedAddCommGroup F<VAR>inst✝² : FunLike 𝓕 E F<VAR>inst✝¹ : ZeroAtInftyContinuousMapClass 𝓕 E F<VAR>inst✝ : ProperSpace E<VAR>f : E → F<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε<VAR>s : Set ℝ<VAR>hs : ∃ ε > 0, Metric.ball 0 ε ⊆ s<GOAL>∃ r, (Metric.closedBall 0 r)ᶜ ⊆ (fun x => ‖f x‖) ⁻¹' s
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>𝓕 : Type u_3<VAR>inst✝⁴ : SeminormedAddGroup E<VAR>inst✝³ : SeminormedAddCommGroup F<VAR>inst✝² : FunLike 𝓕 E F<VAR>inst✝¹ : ZeroAtInftyContinuousMapClass 𝓕 E F<VAR>inst✝ : ProperSpace E<VAR>f : E → F<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε<VAR>s : Set ℝ<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>hs : Metric.ball 0 ε ⊆ s<VAR>r : ℝ<VAR>hr : ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε<GOAL>∃ r, (Metric.closedBall 0 r)ᶜ ⊆ (fun x => ‖f x‖) ⁻¹' s
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>𝓕 : Type u_3<VAR>inst✝⁴ : SeminormedAddGroup E<VAR>inst✝³ : SeminormedAddCommGroup F<VAR>inst✝² : FunLike 𝓕 E F<VAR>inst✝¹ : ZeroAtInftyContinuousMapClass 𝓕 E F<VAR>inst✝ : ProperSpace E<VAR>f : E → F<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε<VAR>s : Set ℝ<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>hs : Metric.ball 0 ε ⊆ s<VAR>r : ℝ<VAR>hr : ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε<GOAL>(Metric.closedBall 0 r)ᶜ ⊆ (fun x => ‖f x‖) ⁻¹' s
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>hz : z ≤ y<VAR>hx : x ≤ y<GOAL>z ⊓ y \ x = ⊥ ↔ z ≤ x
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>hz : z ≤ y<VAR>hx : x ≤ y<GOAL>Disjoint z (y \ x) ↔ z ≤ x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : ContDiffAt 𝕜 n f x<VAR>hn : 1 ≤ n<GOAL>DifferentiableAt 𝕜 f x
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f✝ : ℕ → Ω → ℝ<VAR>ω✝ : Ω<VAR>f : ℕ → Ω → ℝ<VAR>π : Ω → ℕ<VAR>r : ℝ<VAR>n : ℕ<VAR>hπn : ∀ (ω : Ω), π ω ≤ n<VAR>ω : Ω<GOAL>f (leastGE f r (π ω) ω) ω = f (min (π ω) (leastGE f r n ω)) ω
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : CommSemiring R<VAR>f : R[X]<VAR>n m : ℕ<VAR>c : R<VAR>hm : m ≠ 0<GOAL>↑n ∣ eval c ((⇑derivative)^[m] (f ^ n))
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : CommSemiring R<VAR>f : R[X]<VAR>n : ℕ<VAR>c : R<VAR>m : ℕ<VAR>hm : m.succ ≠ 0<GOAL>↑n ∣ eval c ((⇑derivative)^[m.succ] (f ^ n))
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : CommSemiring R<VAR>f : R[X]<VAR>n : ℕ<VAR>c : R<VAR>m : ℕ<VAR>hm : m.succ ≠ 0<GOAL>↑n ∣ ↑n * eval c ((⇑derivative)^[m] (f ^ (n - 1) * derivative f))
<VAR>u : ℤˣ<VAR>n : ℕ<GOAL>u ^ n = u ^ (n % 2)
<VAR>x : Cardinal.{v}<VAR>m : ℕ∞<GOAL>lift.{u, v} x ≤ ↑m ↔ x ≤ ↑m
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x - a) '' Ioi b = Ioi (b - a)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>inst✝ : DecidableRel G.Adj<VAR>v : V<VAR>h : Odd (G.degree v)<GOAL>Odd (filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ).card
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>inst✝ : DecidableRel G.Adj<VAR>v : V<VAR>h : Odd (G.degree v)<VAR>k : ℕ<VAR>hg : (filter (fun v => Odd (G.degree v)) univ).card = k + k<GOAL>Odd (filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ).card
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>inst✝ : DecidableRel G.Adj<VAR>v : V<VAR>h : Odd (G.degree v)<VAR>k : ℕ<VAR>hg : (filter (fun v => Odd (G.degree v)) univ).card = k + k<VAR>hk : 0 < k<GOAL>Odd (filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ).card
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>inst✝ : DecidableRel G.Adj<VAR>v : V<VAR>h : Odd (G.degree v)<VAR>k : ℕ<VAR>hg : (filter (fun v => Odd (G.degree v)) univ).card = k + k<VAR>hk : 0 < k<VAR>hc : (fun w => w ≠ v ∧ Odd (G.degree w)) = fun w => Odd (G.degree w) ∧ w ≠ v<GOAL>Odd (filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ).card
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>inst✝ : DecidableRel G.Adj<VAR>v : V<VAR>h : Odd (G.degree v)<VAR>k : ℕ<VAR>hg : (filter (fun v => Odd (G.degree v)) univ).card = k + k<VAR>hk : 0 < k<VAR>hc : (fun w => w ≠ v ∧ Odd (G.degree w)) = fun w => Odd (G.degree w) ∧ w ≠ v<GOAL>Odd (filter (fun w => Odd (G.degree w) ∧ w ≠ v) univ).card
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>inst✝ : DecidableRel G.Adj<VAR>v : V<VAR>h : Odd (G.degree v)<VAR>k : ℕ<VAR>hg : (filter (fun v => Odd (G.degree v)) univ).card = k + k<VAR>hk : 0 < k<VAR>hc : (fun w => w ≠ v ∧ Odd (G.degree w)) = fun w => Odd (G.degree w) ∧ w ≠ v<GOAL>Odd ((filter (fun w => Odd (G.degree w)) univ).card - 1)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>inst✝ : DecidableRel G.Adj<VAR>v : V<VAR>h : Odd (G.degree v)<VAR>k : ℕ<VAR>hg : (filter (fun v => Odd (G.degree v)) univ).card = k + k<VAR>hk : 0 < k<VAR>hc : (fun w => w ≠ v ∧ Odd (G.degree w)) = fun w => Odd (G.degree w) ∧ w ≠ v<GOAL>v ∈ filter (fun w => Odd (G.degree w)) univ
<VAR>x : ℂ<GOAL>-π < (log x).im
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>h : lowerCrossingTime a b f N n ω ≠ N<GOAL>stoppedValue f (lowerCrossingTime a b f N n) ω ≤ a
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>h : lowerCrossingTime a b f N n ω ≠ N<VAR>j : ℕ<VAR>hj₁ : j ∈ Set.Icc (upperCrossingTime a b f N n ω) (lowerCrossingTime a b f N n ω)<VAR>hj₂ : f j ω ∈ Set.Iic a<GOAL>stoppedValue f (lowerCrossingTime a b f N n) ω ≤ a
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.323542, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>f g : ComposableArrows C 4<VAR>app₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯<VAR>app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯<VAR>app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯<VAR>app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯<VAR>app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯<VAR>w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁ = app₀ ≫ g.map' 0 1 ⋯ ⋯<VAR>w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂ = app₁ ≫ g.map' 1 2 ⋯ ⋯<VAR>w₂ : f.map' 2 3 ⋯ ⋯ ≫ app₃ = app₂ ≫ g.map' 2 3 ⋯ ⋯<VAR>w₃ : f.map' 3 4 ⋯ ⋯ ≫ app₄ = app₃ ≫ g.map' 3 4 ⋯ ⋯<GOAL>4 < 4 + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<VAR>L : List (List α)<GOAL>(l :: L).join = [] ↔ ∀ (l_1 : List α), l_1 ∈ l :: L → l_1 = []