ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v w : V<VAR>p : G.Walk u v<VAR>hp : p.IsPath<VAR>hp' : ¬p.Nil<GOAL>(p.tail hp').IsPath
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v w : V<VAR>p : G.Walk u v<VAR>hp : p.support.Nodup<VAR>hp' : ¬p.Nil<GOAL>(p.tail hp').support.Nodup
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v w : V<VAR>p : G.Walk u v<VAR>hp' : ¬p.Nil<VAR>hp : u ∉ (p.tail hp').support ∧ (p.tail hp').support.Nodup<GOAL>(p.tail hp').support.Nodup
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>S✝ R : Sieve X<VAR>J : GrothendieckTopology C<VAR>S : Sieve X<VAR>f : Y ⟶ X<GOAL>⊥.Covers S f ↔ S.arrows f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>α : Type u_6<VAR>inst✝ : AddCommMonoid α<VAR>m M N : ℕ<VAR>f : (n : ℕ) × (Fin n → ℕ) → α<VAR>g : (n : ℕ) × Composition n → α<VAR>h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)<GOAL>∑ e ∈ compPartialSumSource m M N, f e = ∑ e ∈ compPartialSumTarget m M N, g e
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>α : Type u_6<VAR>inst✝ : AddCommMonoid α<VAR>m M N : ℕ<VAR>f : (n : ℕ) × (Fin n → ℕ) → α<VAR>g : (n : ℕ) × Composition n → α<VAR>h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)<GOAL>∀ (a : (n : ℕ) × (Fin n → ℕ)) (ha : a ∈ compPartialSumSource m M N), compChangeOfVariables m M N a ha ∈ compPartialSumTarget m M N
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>α : Type u_6<VAR>inst✝ : AddCommMonoid α<VAR>m M N : ℕ<VAR>f : (n : ℕ) × (Fin n → ℕ) → α<VAR>g : (n : ℕ) × Composition n → α<VAR>h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)<GOAL>∀ (a₁ : (n : ℕ) × (Fin n → ℕ)) (ha₁ : a₁ ∈ compPartialSumSource m M N) (a₂ : (n : ℕ) × (Fin n → ℕ)) (ha₂ : a₂ ∈ compPartialSumSource m M N), compChangeOfVariables m M N a₁ ha₁ = compChangeOfVariables m M N a₂ ha₂ → a₁ = a₂
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>α : Type u_6<VAR>inst✝ : AddCommMonoid α<VAR>m M N : ℕ<VAR>f : (n : ℕ) × (Fin n → ℕ) → α<VAR>g : (n : ℕ) × Composition n → α<VAR>h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)<GOAL>∀ b ∈ compPartialSumTarget m M N, ∃ a, ∃ (ha : a ∈ compPartialSumSource m M N), compChangeOfVariables m M N a ha = b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>α : Type u_6<VAR>inst✝ : AddCommMonoid α<VAR>m M N : ℕ<VAR>f : (n : ℕ) × (Fin n → ℕ) → α<VAR>g : (n : ℕ) × Composition n → α<VAR>h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)<GOAL>∀ (a : (n : ℕ) × (Fin n → ℕ)) (ha : a ∈ compPartialSumSource m M N), f a = g (compChangeOfVariables m M N a ha)
<VAR>b n : ℕ<GOAL>log b n = 1 ↔ b ≤ n ∧ n < b * b
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>u : β → α<GOAL>CauchySeq u ↔ Tendsto (fun n => dist (u n.1) (u n.2)) atTop (𝓝 0)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>u : β → α<GOAL>Tendsto (fun x => dist (Prod.map u u x).1 (Prod.map u u x).2) atTop (𝓝 0) ↔ Tendsto (fun n => dist (u n.1) (u n.2)) atTop (𝓝 0)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ<VAR>p q : ℝ<VAR>hp : 1 ≤ p<GOAL>(∑ i ∈ s, |f i|) ^ p ≤ ↑s.card ^ (p - 1) * ∑ i ∈ s, |f i| ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ<VAR>p q : ℝ<VAR>hp : 1 ≤ p<VAR>this : ↑((∑ i ∈ s, (fun i => ⟨|f i|, ⋯⟩) i) ^ p) ≤ ↑(↑s.card ^ (p - 1) * ∑ i ∈ s, (fun i => ⟨|f i|, ⋯⟩) i ^ p)<GOAL>(∑ i ∈ s, |f i|) ^ p ≤ ↑s.card ^ (p - 1) * ∑ i ∈ s, |f i| ^ p
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>k r : ℕ<GOAL>t ∈ ∂ 𝒜 ↔ ∃ s ∈ 𝒜, ∃ a ∈ s, s.erase a = t
<VAR>l : Type u_1<VAR>m✝ : Type u_2<VAR>n✝ : Type u_3<VAR>o : Type u_4<VAR>p✝ : Type u_5<VAR>q✝ : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝¹ : CommRing R<VAR>m : Type u_14<VAR>n : Type u_15<VAR>k✝ : Type u_16<VAR>inst✝ : Fintype n<VAR>p : m → Prop<VAR>q : k✝ → Prop<VAR>A : Matrix m n R<VAR>B : Matrix n k✝ R<VAR>i : { a // p a }<VAR>k : { a // q a }<GOAL>(A * B).toBlock p q i k = (A.toBlock p ⊤ * B.toBlock ⊤ q) i k
<VAR>l : Type u_1<VAR>m✝ : Type u_2<VAR>n✝ : Type u_3<VAR>o : Type u_4<VAR>p✝ : Type u_5<VAR>q✝ : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝¹ : CommRing R<VAR>m : Type u_14<VAR>n : Type u_15<VAR>k✝ : Type u_16<VAR>inst✝ : Fintype n<VAR>p : m → Prop<VAR>q : k✝ → Prop<VAR>A : Matrix m n R<VAR>B : Matrix n k✝ R<VAR>i : { a // p a }<VAR>k : { a // q a }<GOAL>∑ j : n, A (↑i) j * B j ↑k = ∑ x : { a // ⊤ a }, A ↑i ↑x * B ↑x ↑k
<VAR>l : Type u_1<VAR>m✝ : Type u_2<VAR>n✝ : Type u_3<VAR>o : Type u_4<VAR>p✝ : Type u_5<VAR>q✝ : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝¹ : CommRing R<VAR>m : Type u_14<VAR>n : Type u_15<VAR>k✝ : Type u_16<VAR>inst✝ : Fintype n<VAR>p : m → Prop<VAR>q : k✝ → Prop<VAR>A : Matrix m n R<VAR>B : Matrix n k✝ R<VAR>i : { a // p a }<VAR>k : { a // q a }<GOAL>∀ (x : n), x ∈ Finset.univ ↔ ⊤ x
<VAR>K : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝³ : DivisionRing K<VAR>inst✝² : DivisionRing L<VAR>inst✝¹ : DivisionRing M<VAR>S : Type u_1<VAR>inst✝ : SetLike S K<VAR>h : SubfieldClass S K<VAR>x : K<VAR>s : S<VAR>q : ℚ≥0<GOAL>↑q ∈ s
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : StrictOrderedSemiring R<VAR>a x y : R<VAR>n✝ m : ℕ<VAR>h : x < y<VAR>hx : 0 ≤ x<VAR>n : ℕ<VAR>x✝ : n + 1 ≠ 0<GOAL>x ^ (n + 1) < y ^ (n + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>g : α → ℝ≥0∞<GOAL>∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>g : α → ℝ≥0∞<GOAL>∫⁻ (a : α), f a + g a ∂μ ≤ ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>g φ : α → ℝ≥0∞<VAR>hφm : Measurable φ<VAR>hφ_le : φ ≤ fun a => f a + g a<VAR>hφ_eq : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), φ a ∂μ<GOAL>∫⁻ (a : α), f a + g a ∂μ ≤ ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x✝ y z : α<VAR>ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>inst✝ : WeaklyLocallyCompactSpace α<VAR>x : α<GOAL>∃ r, 0 < r ∧ IsCompact (closedBall x r)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x✝ y z : α<VAR>ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>inst✝ : WeaklyLocallyCompactSpace α<VAR>x : α<VAR>this : ∀ᶠ (r : ℝ) in 𝓝[>] 0, IsCompact (closedBall x r)<GOAL>∃ r, 0 < r ∧ IsCompact (closedBall x r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : CommGroup G<VAR>a b c d : G<GOAL>a / b = c / d ↔ a / c = b / d
<VAR>α : Type u_1<VAR>α₁ : Type u_2<VAR>α₂ : Type u_3<VAR>β : α → Type u_4<VAR>β₁ : α₁ → Type u_5<VAR>β₂ : α₂ → Type u_6<VAR>fst✝¹ : α<VAR>snd✝¹ : β fst✝¹<VAR>fst✝ : α<VAR>snd✝ : β fst✝<GOAL>⟨fst✝¹, snd✝¹⟩ = ⟨fst✝, snd✝⟩ ↔ ⟨fst✝¹, snd✝¹⟩.fst = ⟨fst✝, snd✝⟩.fst ∧ HEq ⟨fst✝¹, snd✝¹⟩.snd ⟨fst✝, snd✝⟩.snd
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝³ : Semiring R<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>inst✝ : DecidableEq ι<VAR>p : ι → Submodule R N<GOAL>iSup p = LinearMap.range ((lsum ℕ) fun i => (p i).subtype)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝³ : Semiring R<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>inst✝ : DecidableEq ι<VAR>p : ι → Submodule R N<GOAL>iSup p ≤ LinearMap.range ((lsum ℕ) fun i => (p i).subtype)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝³ : Semiring R<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>inst✝ : DecidableEq ι<VAR>p : ι → Submodule R N<GOAL>LinearMap.range ((lsum ℕ) fun i => (p i).subtype) ≤ iSup p
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : PseudoEMetricSpace α✝<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>s : Set α<GOAL>IsClosed {f | LipschitzOnWith K f s}
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : PseudoEMetricSpace α✝<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>s : Set α<GOAL>IsClosed (⋂ i ∈ s, ⋂ i_1 ∈ s, {x | edist (x i) (x i_1) ≤ ↑K * edist i i_1})
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : PseudoEMetricSpace α✝<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>s : Set α<VAR>x : α<VAR>x✝¹ : x ∈ s<VAR>y : α<VAR>x✝ : y ∈ s<GOAL>Continuous fun x_1 => edist (x_1 x) (x_1 y)
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : PseudoEMetricSpace α✝<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>s : Set α<VAR>x : α<VAR>x✝¹ : x ∈ s<VAR>y : α<VAR>x✝ : y ∈ s<GOAL>Continuous fun x_1 => ↑K * edist x y
<VAR>k : ℕ<VAR>hk0 : k ≠ 0<GOAL>∃ᶠ (p : ℕ) in atTop, Prime p ∧ p ≡ 1 [MOD k]
<VAR>k : ℕ<VAR>hk0 : k ≠ 0<VAR>n : ℕ<GOAL>∃ b ≥ n, Prime b ∧ b ≡ 1 [MOD k]
<VAR>k : ℕ<VAR>hk0 : k ≠ 0<VAR>n p : ℕ<VAR>hp : Prime p ∧ n < p ∧ p ≡ 1 [MOD k]<GOAL>∃ b ≥ n, Prime b ∧ b ≡ 1 [MOD k]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Finset α<VAR>a : α<GOAL>a ∉ ∅
<VAR>p : ℝ<VAR>x✝ : AddCircle p<VAR>hp : p ≠ 0<VAR>x : ℝ<GOAL>‖↑x‖ ≤ |p| / 2
<VAR>p : ℝ<VAR>x✝ : AddCircle p<VAR>hp : p ≠ 0<VAR>x : ℝ<GOAL>|p⁻¹ * x - ↑(round (p⁻¹ * x))| ≤ 1 / 2
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : ConditionallyCompleteLinearOrderBot α<VAR>f : ι → α<VAR>s : Set α<VAR>x : α<VAR>hbdd : BddAbove s<VAR>hlim : ¬IsSuccLimit (sSup s)<GOAL>sSup s ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : ConditionallyCompleteLinearOrderBot α<VAR>f : ι → α<VAR>x : α<VAR>hbdd : BddAbove ∅<VAR>hlim : ¬IsSuccLimit (sSup ∅)<GOAL>sSup ∅ ∈ ∅
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : ConditionallyCompleteLinearOrderBot α<VAR>f : ι → α<VAR>s : Set α<VAR>x : α<VAR>hbdd : BddAbove s<VAR>hlim : ¬IsSuccLimit (sSup s)<VAR>hs : s.Nonempty<GOAL>sSup s ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g s✝ t✝ : ι → α<VAR>a b : α<VAR>f : β → γ → α<VAR>s : Set β<VAR>t : Set γ<GOAL>sInf (image2 f s t) = ⨅ a ∈ s, ⨅ b ∈ t, f a b
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>σ : Type u_2<VAR>s : Multiset σ<VAR>r : σ → R<VAR>k : ℕ<VAR>h : k ≤ card s<GOAL>(map (fun i => X + C (r i)) s).prod.coeff k = (map r s).esymm (card s - k)
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>σ : Type u_2<VAR>s : Multiset σ<VAR>r : σ → R<VAR>k : ℕ<VAR>h : k ≤ card s<GOAL>k ≤ card s
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CommRing T<VAR>α : Type u_4<VAR>β : Type u_5<VAR>f : R →+* S<VAR>x✝ y : 𝕎 R<VAR>z : ℤ<VAR>x : 𝕎 R<GOAL>mapFun (⇑f) (z • x) = z • mapFun (⇑f) x
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Semiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module Rᵐᵒᵖ M<VAR>r : R<VAR>m : M<GOAL>0 •> 0 + m <• r = m <• r
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>r✝ : ℝ≥0∞<VAR>n✝ : ℕ<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>h : CPolynomialOn 𝕜 f s<VAR>y : E<VAR>hy : y ∈ s<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℕ<VAR>n : ℝ≥0∞<VAR>hp : HasFiniteFPowerSeriesOnBall f p y r n<GOAL>CPolynomialAt 𝕜 (_root_.fderiv 𝕜 f) y
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>x y z : R<VAR>H : IsCoprime x y<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>f : R →+* S<VAR>a b : R<VAR>h : a * x + b * y = 1<GOAL>f a * f x + f b * f y = 1
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝² : Category.{?u.46478, u_1} C<VAR>inst✝¹ : Category.{?u.46482, u_2} D<VAR>inst✝ : Category.{?u.46486, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>E E' : L.RightExtension F<VAR>Y : D<VAR>g₁ g₂ : StructuredArrow Y L<VAR>φ : g₁ ⟶ g₂<GOAL>𝟙 (E.left.obj Y) ≫ E.left.map g₂.hom ≫ E.hom.app g₂.right = (E.left.map g₁.hom ≫ E.hom.app g₁.right) ≫ F.map φ.right
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝² : Category.{?u.46478, u_1} C<VAR>inst✝¹ : Category.{?u.46482, u_2} D<VAR>inst✝ : Category.{?u.46486, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>E E' : L.RightExtension F<VAR>Y : D<VAR>g₁ g₂ : StructuredArrow Y L<VAR>φ : g₁ ⟶ g₂<GOAL>E.left.map g₁.hom ≫ E.left.map (L.map φ.right) ≫ E.hom.app g₂.right = E.left.map g₁.hom ≫ E.hom.app g₁.right ≫ F.map φ.right
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝² : Category.{?u.46478, u_1} C<VAR>inst✝¹ : Category.{?u.46482, u_2} D<VAR>inst✝ : Category.{?u.46486, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>E E' : L.RightExtension F<VAR>Y : D<VAR>g₁ g₂ : StructuredArrow Y L<VAR>φ : g₁ ⟶ g₂<GOAL>E.left.map (L.map φ.right) ≫ E.hom.app g₂.right = E.hom.app g₁.right ≫ F.map φ.right
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v, u₂} D<VAR>S : C ⥤ D<VAR>T : D<VAR>inst✝¹ : HasColimits C<VAR>inst✝ : PreservesColimits S<VAR>A : CostructuredArrow S T<VAR>P : (CostructuredArrow S T)ᵒᵖ<VAR>f : P ⟶ op A<VAR>hf : Mono f<VAR>q : S.obj (unop (Subobject.underlying.obj (projectQuotient (Subobject.mk f)))) ⟶ (Functor.fromPUnit T).obj A.right<VAR>hq : S.map (projectQuotient (Subobject.mk f)).arrow.unop ≫ q = A.hom<GOAL>liftQuotient (projectQuotient (Subobject.mk f)) hq = Subobject.mk f
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v, u₂} D<VAR>S : C ⥤ D<VAR>T : D<VAR>inst✝¹ : HasColimits C<VAR>inst✝ : PreservesColimits S<VAR>A : CostructuredArrow S T<VAR>P : (CostructuredArrow S T)ᵒᵖ<VAR>f : P ⟶ op A<VAR>hf : Mono f<VAR>q : S.obj (unop (Subobject.underlying.obj (projectQuotient (Subobject.mk f)))) ⟶ (Functor.fromPUnit T).obj A.right<VAR>hq : S.map (projectQuotient (Subobject.mk f)).arrow.unop ≫ q = A.hom<GOAL>op (mk q) ≅ P
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v, u₂} D<VAR>S : C ⥤ D<VAR>T : D<VAR>inst✝¹ : HasColimits C<VAR>inst✝ : PreservesColimits S<VAR>A : CostructuredArrow S T<VAR>P : (CostructuredArrow S T)ᵒᵖ<VAR>f : P ⟶ op A<VAR>hf : Mono f<VAR>q : S.obj (unop (Subobject.underlying.obj (projectQuotient (Subobject.mk f)))) ⟶ (Functor.fromPUnit T).obj A.right<VAR>hq : S.map (projectQuotient (Subobject.mk f)).arrow.unop ≫ q = A.hom<GOAL>?i.hom ≫ f = (homMk (projectQuotient (Subobject.mk f)).arrow.unop hq).op
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G✝ : SimpleGraph V<VAR>a b c u v w : V<VAR>e✝ : Sym2 V<VAR>G₁ G₂ G : SimpleGraph V<VAR>s : Set (Sym2 V)<VAR>e : Sym2 V<GOAL>e ∈ G.edgeSet \ (s \ {e | e.IsDiag}) ↔ e ∈ G.edgeSet \ s
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G✝ : SimpleGraph V<VAR>a b c u v w : V<VAR>e✝ : Sym2 V<VAR>G₁ G₂ G : SimpleGraph V<VAR>s : Set (Sym2 V)<VAR>e : Sym2 V<GOAL>e ∈ G.edgeSet → (e ∈ s → e.IsDiag ↔ e ∉ s)
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G✝ : SimpleGraph V<VAR>a b c u v w : V<VAR>e✝ : Sym2 V<VAR>G₁ G₂ G : SimpleGraph V<VAR>s : Set (Sym2 V)<VAR>e : Sym2 V<VAR>h : e ∈ G.edgeSet<GOAL>e ∈ s → e.IsDiag ↔ e ∉ s
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>HasSum (fun n => (-1) ^ (n + 1) * z ^ n / ↑n) (log (1 + z))
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>Summable fun i => ‖(-1) ^ (i + 1) * z ^ i / ↑i‖
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ (i + 1) * z ^ i / ↑i) atTop (nhds (log (1 + z)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>l l' : List α<VAR>a✝ : α<VAR>a b : List α<GOAL>a.toFinset = b.toFinset ↔ ∀ (x : α), x ∈ a ↔ x ∈ b
<VAR>K : Type u<VAR>inst✝³ : CommRing K<VAR>inst✝² : IsReduced K<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : CharP K p<VAR>x y : ℕ × K<VAR>x✝ : ∃ z, (⇑(frobenius K p))^[y.1 + z] x.2 = (⇑(frobenius K p))^[x.1 + z] y.2<VAR>z : ℕ<VAR>H : (⇑(frobenius K p))^[y.1 + z] x.2 = (⇑(frobenius K p))^[x.1 + z] y.2<GOAL>(⇑(frobenius K p))^[z] ((⇑(frobenius K p))^[y.1] x.2) = (⇑(frobenius K p))^[z] ((⇑(frobenius K p))^[x.1] y.2)
<VAR>x y : ℝ<VAR>n : ℕ<GOAL>log ↑n = n.factorization.sum fun p t => ↑t * log ↑p
<VAR>x y : ℝ<GOAL>log ↑0 = (Nat.factorization 0).sum fun p t => ↑t * log ↑p
<VAR>x y : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>log ↑n = n.factorization.sum fun p t => ↑t * log ↑p
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L✝ : V →L[ℝ] W →L[ℝ] ℝ<VAR>f✝ : V → E<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>v : V<GOAL>‖L v‖ ≤ ‖L‖ * ‖v‖
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i j : A<GOAL>(shiftAdd X i j).inv ≫ (shiftFunctor C (i + j)).map f ≫ (shiftAdd Y i j).hom = (shiftFunctor C j).map ((shiftFunctor C i).map f)
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i j : A<GOAL>(shiftFunctorAdd C i j).inv.app X ≫ (shiftFunctor C (i + j)).map f ≫ (shiftAdd Y i j).hom = (shiftFunctor C i ⋙ shiftFunctor C j).map f
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b✝ l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hf : ContDiff ℝ 1 f<VAR>h2f : HasCompactSupport f<VAR>b : ℝ<GOAL>∫ (x : ℝ) in Ioi b, deriv f x = -f b
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b✝ l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hf : ContDiff ℝ 1 f<VAR>h2f : HasCompactSupport f<VAR>b : ℝ<VAR>this : ∀ x ∈ Ioi b, HasDerivAt f (deriv f x) x<GOAL>∫ (x : ℝ) in Ioi b, deriv f x = -f b
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b✝ l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hf : ContDiff ℝ 1 f<VAR>h2f : HasCompactSupport f<VAR>b : ℝ<VAR>this : ∀ x ∈ Ioi b, HasDerivAt f (deriv f x) x<GOAL>IntegrableOn (deriv f) (Ioi b) volume
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b✝ l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hf : ContDiff ℝ 1 f<VAR>h2f : HasCompactSupport f<VAR>b : ℝ<VAR>this : ∀ x ∈ Ioi b, HasDerivAt f (deriv f x) x<GOAL>Tendsto f atTop (𝓝 0)
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b✝ l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hf : ContDiff ℝ 1 f<VAR>h2f : f =ᶠ[cocompact ℝ] 0<VAR>b : ℝ<VAR>this : ∀ x ∈ Ioi b, HasDerivAt f (deriv f x) x<GOAL>Tendsto f atTop (𝓝 0)
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x✝ y : M<VAR>hv : LinearIndependent R v<VAR>l : ι →₀ R<VAR>x : ↥(span R (range v))<VAR>eq : (Finsupp.total ι M R v) l = ↑x<VAR>this : ↑(↑hv.totalEquiv l) = (Finsupp.total ι M R v) l<GOAL>hv.repr x = l
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x✝ y : M<VAR>hv : LinearIndependent R v<VAR>l : ι →₀ R<VAR>x : ↥(span R (range v))<VAR>eq : (Finsupp.total ι M R v) l = ↑x<VAR>this✝ : ↑(↑hv.totalEquiv l) = (Finsupp.total ι M R v) l<VAR>this : ↑hv.totalEquiv l = x<GOAL>hv.repr x = l
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x✝ y : M<VAR>hv : LinearIndependent R v<VAR>l : ι →₀ R<VAR>x : ↥(span R (range v))<VAR>eq : (Finsupp.total ι M R v) l = ↑x<VAR>this✝ : ↑(↑hv.totalEquiv l) = (Finsupp.total ι M R v) l<VAR>this : ↑hv.totalEquiv l = x<GOAL>hv.repr x = hv.totalEquiv.symm (hv.totalEquiv l)
<VAR>a : ↥circle<GOAL>LinearEquiv.det (rotation a).toLinearEquiv = 1
<VAR>C : Type ?u.25950<VAR>inst✝¹ : Category.{?u.25954, ?u.25950} C<VAR>r : HomRel C<VAR>D : Type ?u.25982<VAR>inst✝ : Category.{?u.25986, ?u.25982} D<VAR>F✝ : C ⥤ D<VAR>H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F✝.map f₁ = F✝.map f₂<VAR>F G : Quotient r ⥤ D<VAR>τ : functor r ⋙ F ≅ functor r ⋙ G<GOAL>natTransLift r τ.hom ≫ natTransLift r τ.inv = 𝟙 F
<VAR>C : Type ?u.25950<VAR>inst✝¹ : Category.{?u.25954, ?u.25950} C<VAR>r : HomRel C<VAR>D : Type ?u.25982<VAR>inst✝ : Category.{?u.25986, ?u.25982} D<VAR>F✝ : C ⥤ D<VAR>H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F✝.map f₁ = F✝.map f₂<VAR>F G : Quotient r ⥤ D<VAR>τ : functor r ⋙ F ≅ functor r ⋙ G<GOAL>natTransLift r τ.inv ≫ natTransLift r τ.hom = 𝟙 G
<VAR>x y : ℝ*<VAR>r s : ℝ<VAR>hxr : x.IsSt r<VAR>hys : y.IsSt s<VAR>hrs : r < s<GOAL>x < y