ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.RightHomologyData<VAR>A : C<VAR>k : S.X₂ ⟶ A<VAR>hk : S.f ≫ k = 0<VAR>inst✝ : S.HasRightHomology<GOAL>S.g = S.g ≫ 𝟙 S.X₃
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → ℂ<VAR>x : ℂ<VAR>h₁ : DifferentiableAt ℂ f x<VAR>h₂ : f x ∈ slitPlane<GOAL>deriv (log ∘ f) x = logDeriv f x
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → ℂ<VAR>x : ℂ<VAR>h₁ : DifferentiableAt ℂ f x<VAR>h₂ : f x ∈ slitPlane<VAR>A : deriv (fun t => log (f t)) x = deriv f x / f x<GOAL>deriv (log ∘ f) x = logDeriv f x
<VAR>𝕜✝ : Type u_1<VAR>inst✝⁵ : NontriviallyNormedField 𝕜✝<VAR>E✝ : Type u_2<VAR>inst✝⁴ : SeminormedAddCommGroup E✝<VAR>inst✝³ : NormedSpace 𝕜✝ E✝<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>polar 𝕜 (closedBall 0 r) = closedBall 0 r⁻¹
<VAR>𝕜✝ : Type u_1<VAR>inst✝⁵ : NontriviallyNormedField 𝕜✝<VAR>E✝ : Type u_2<VAR>inst✝⁴ : SeminormedAddCommGroup E✝<VAR>inst✝³ : NormedSpace 𝕜✝ E✝<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>polar 𝕜 (closedBall 0 r) ⊆ closedBall 0 r⁻¹
<VAR>𝕜✝ : Type u_1<VAR>inst✝⁵ : NontriviallyNormedField 𝕜✝<VAR>E✝ : Type u_2<VAR>inst✝⁴ : SeminormedAddCommGroup E✝<VAR>inst✝³ : NormedSpace 𝕜✝ E✝<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>r : ℝ<VAR>hr : 0 < r<VAR>x' : Dual 𝕜 E<VAR>h : x' ∈ polar 𝕜 (closedBall 0 r)<GOAL>x' ∈ closedBall 0 r⁻¹
<VAR>𝕜✝ : Type u_1<VAR>inst✝⁵ : NontriviallyNormedField 𝕜✝<VAR>E✝ : Type u_2<VAR>inst✝⁴ : SeminormedAddCommGroup E✝<VAR>inst✝³ : NormedSpace 𝕜✝ E✝<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>r : ℝ<VAR>hr : 0 < r<VAR>x' : Dual 𝕜 E<VAR>h : x' ∈ polar 𝕜 (closedBall 0 r)<GOAL>‖x'‖ ≤ r⁻¹
<VAR>𝕜✝ : Type u_1<VAR>inst✝⁵ : NontriviallyNormedField 𝕜✝<VAR>E✝ : Type u_2<VAR>inst✝⁴ : SeminormedAddCommGroup E✝<VAR>inst✝³ : NormedSpace 𝕜✝ E✝<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>r : ℝ<VAR>hr : 0 < r<VAR>x' : Dual 𝕜 E<VAR>h : x' ∈ polar 𝕜 (closedBall 0 r)<VAR>z : E<VAR>x✝ : z ∈ ball 0 r<GOAL>‖x' z‖ ≤ r⁻¹ * ‖z‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>K : Type u_4<VAR>inst✝ : NormedDivisionRing K<VAR>ξ : K<GOAL>(Summable fun n => ξ ^ n) ↔ ‖ξ‖ < 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>K : Type u_4<VAR>inst✝ : NormedDivisionRing K<VAR>ξ : K<VAR>h : Summable fun n => ξ ^ n<GOAL>‖ξ‖ < 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>K : Type u_4<VAR>inst✝ : NormedDivisionRing K<VAR>ξ : K<VAR>h : Summable fun n => ξ ^ n<VAR>k : ℕ<VAR>hk : dist (ξ ^ k) 0 < 1<GOAL>‖ξ‖ < 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>K : Type u_4<VAR>inst✝ : NormedDivisionRing K<VAR>ξ : K<VAR>h : Summable fun n => ξ ^ n<VAR>k : ℕ<VAR>hk : ‖ξ‖ ^ k < 1<GOAL>‖ξ‖ < 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>K : Type u_4<VAR>inst✝ : NormedDivisionRing K<VAR>ξ : K<VAR>h : Summable fun n => ξ ^ n<VAR>k : ℕ<VAR>hk : ‖ξ‖ ^ k < 1 ^ k<GOAL>‖ξ‖ < 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>a : α<VAR>b : β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>x : α<VAR>y : β<GOAL>(x, y) ∈ s ×ˢ (t ∩ t') ↔ (x, y) ∈ s ×ˢ t ∩ s ×ˢ t'
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁷ : OrderedSemiring 𝕜<VAR>inst✝⁶ : AddCommMonoid E<VAR>inst✝⁵ : AddCommMonoid F<VAR>inst✝⁴ : OrderedAddCommMonoid α<VAR>inst✝³ : OrderedAddCommMonoid β<VAR>inst✝² : SMul 𝕜 E<VAR>inst✝¹ : SMul 𝕜 α<VAR>inst✝ : SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>g✝ : β → α<VAR>g : E → β<VAR>hf : StrictConcaveOn 𝕜 s f<VAR>hfg : EqOn f g s<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>a • g x + b • g y < g (a • x + b • y)
<VAR>E : Type u_1<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup V<VAR>inst✝⁸ : InnerProductSpace ℝ V<VAR>inst✝⁷ : MeasurableSpace V<VAR>inst✝⁶ : BorelSpace V<VAR>inst✝⁵ : FiniteDimensional ℝ V<VAR>W : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : InnerProductSpace ℝ W<VAR>inst✝² : MeasurableSpace W<VAR>inst✝¹ : BorelSpace W<VAR>inst✝ : FiniteDimensional ℝ W<VAR>f : V → E<GOAL>𝓕 (𝓕⁻ f) = 𝓕⁻ (𝓕 f)
<VAR>E : Type u_1<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup V<VAR>inst✝⁸ : InnerProductSpace ℝ V<VAR>inst✝⁷ : MeasurableSpace V<VAR>inst✝⁶ : BorelSpace V<VAR>inst✝⁵ : FiniteDimensional ℝ V<VAR>W : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : InnerProductSpace ℝ W<VAR>inst✝² : MeasurableSpace W<VAR>inst✝¹ : BorelSpace W<VAR>inst✝ : FiniteDimensional ℝ W<VAR>f : V → E<GOAL>𝓕 (𝓕⁻ f) = 𝓕 fun x => 𝓕 f (-x)
<VAR>p : ℝ × ℝ<VAR>hp_fst : p.1 < 0<GOAL>(fun x => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => rexp (log x.1 * x.2) * cos (x.2 * π)
<VAR>p : ℝ × ℝ<VAR>hp_fst : p.1 < 0<GOAL>∀ᶠ (x : ℝ × ℝ) in 𝓝 p, x.1 < 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>y : E<GOAL>HasFDerivWithinAt f f' (s \ {y}) x ↔ HasFDerivWithinAt f f' s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R S T : α → α → Prop<VAR>a : α<VAR>l : List α<VAR>hR : Symmetric R<VAR>hl : Pairwise R l<GOAL>∀ ⦃a : α⦄, a ∈ l → ∀ ⦃b : α⦄, b ∈ l → a ≠ b → R a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R S T : α → α → Prop<VAR>a : α<VAR>l : List α<VAR>hR : Symmetric R<VAR>hl : Pairwise R l<GOAL>Symmetric fun x y => x ≠ y → R x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R S T : α → α → Prop<VAR>a : α<VAR>l : List α<VAR>hR : Symmetric R<VAR>hl : Pairwise R l<GOAL>∀ (x : α), x ∈ l → x ≠ x → R x x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R S T : α → α → Prop<VAR>a : α<VAR>l : List α<VAR>hR : Symmetric R<VAR>hl : Pairwise R l<GOAL>Pairwise (fun x y => x ≠ y → R x y) l
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>G : Type u_3<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x : 𝕜<VAR>r : ℝ<VAR>hf' : UniformCauchySeqOn f' l (Metric.ball x r)<VAR>hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasDerivAt (f n) (f' n y) y<VAR>hfg : Cauchy (map (fun n => f n x) l)<GOAL>UniformCauchySeqOn f l (Metric.ball x r)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>G : Type u_3<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x : 𝕜<VAR>r : ℝ<VAR>hf' : UniformCauchySeqOn f' l (Metric.ball x r)<VAR>hfg : Cauchy (map (fun n => f n x) l)<VAR>hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (ContinuousLinearMap.smulRight 1 (f' n y)) y<GOAL>UniformCauchySeqOn f l (Metric.ball x r)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>G : Type u_3<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x : 𝕜<VAR>r : ℝ<VAR>hf' : UniformCauchySeqOnFilter f' l (𝓟 (Metric.ball x r))<VAR>hfg : Cauchy (map (fun n => f n x) l)<VAR>hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (ContinuousLinearMap.smulRight 1 (f' n y)) y<GOAL>UniformCauchySeqOn f l (Metric.ball x r)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>G : Type u_3<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x : 𝕜<VAR>r : ℝ<VAR>hf'✝ : UniformCauchySeqOnFilter f' l (𝓟 (Metric.ball x r))<VAR>hfg : Cauchy (map (fun n => f n x) l)<VAR>hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (ContinuousLinearMap.smulRight 1 (f' n y)) y<VAR>hf' : UniformCauchySeqOn (fun n z => ContinuousLinearMap.smulRight 1 (f' n z)) l (Metric.ball x r)<GOAL>UniformCauchySeqOn f l (Metric.ball x r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ ν μ : Measure α<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite μ<VAR>r : ℝ≥0<GOAL>(r • ν).rnDeriv μ =ᶠ[ae μ] r • ν.rnDeriv μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ ν μ : Measure α<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite μ<VAR>r : ℝ≥0<GOAL>μ.withDensity ((r • ν).rnDeriv μ) = μ.withDensity (r • ν.rnDeriv μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ ν μ : Measure α<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite μ<VAR>r : ℝ≥0<GOAL>AEMeasurable ((r • ν).rnDeriv μ) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ ν μ : Measure α<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite μ<VAR>r : ℝ≥0<GOAL>AEMeasurable (r • ν.rnDeriv μ) μ
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b c : α<VAR>hab : IsUnit (gcd a b)<VAR>k : ℕ<VAR>h : a * b = c ^ k<GOAL>∃ d, Associated (d ^ k) a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b c : α<VAR>hab : IsUnit (gcd a b)<VAR>k : ℕ<VAR>h : a * b = c ^ k<VAR>h✝ : Subsingleton α<GOAL>∃ d, Associated (d ^ k) a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b c : α<VAR>hab : IsUnit (gcd a b)<VAR>k : ℕ<VAR>h : a * b = c ^ k<VAR>h✝ : Nontrivial α<GOAL>∃ d, Associated (d ^ k) a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b c : α<VAR>hab : IsUnit (gcd a b)<VAR>k : ℕ<VAR>h : a * b = c ^ k<VAR>h✝ : Nontrivial α<VAR>ha : ¬a = 0<VAR>hb : ¬b = 0<GOAL>∃ d, Associated (d ^ k) a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b c : α<VAR>hab : IsUnit (gcd a b)<VAR>h✝ : Nontrivial α<VAR>ha : ¬a = 0<VAR>hb : ¬b = 0<VAR>h : a * b = c ^ 0<GOAL>∃ d, Associated (d ^ 0) a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b c : α<VAR>hab : IsUnit (gcd a b)<VAR>k : ℕ<VAR>h : a * b = c ^ k<VAR>h✝ : Nontrivial α<VAR>ha : ¬a = 0<VAR>hb : ¬b = 0<VAR>hk : k > 0<GOAL>∃ d, Associated (d ^ k) a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b c : α<VAR>hab : IsUnit (gcd a b)<VAR>k : ℕ<VAR>h : a * b = c ^ k<VAR>h✝ : Nontrivial α<VAR>ha : ¬a = 0<VAR>hb : ¬b = 0<VAR>hk : k > 0<VAR>hc : c ∣ a * b<GOAL>∃ d, Associated (d ^ k) a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b c : α<VAR>hab : IsUnit (gcd a b)<VAR>k : ℕ<VAR>h : a * b = c ^ k<VAR>h✝ : Nontrivial α<VAR>ha : ¬a = 0<VAR>hb : ¬b = 0<VAR>hk : k > 0<VAR>hc✝ : c ∣ a * b<VAR>d₁ d₂ : α<VAR>hd₁ : d₁ ∣ a<VAR>hd₂ : d₂ ∣ b<VAR>hc : c = d₁ * d₂<GOAL>∃ d, Associated (d ^ k) a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b c : α<VAR>hab : IsUnit (gcd a b)<VAR>k : ℕ<VAR>h : a * b = c ^ k<VAR>h✝ : Nontrivial α<VAR>ha : ¬a = 0<VAR>hb : ¬b = 0<VAR>hk : k > 0<VAR>hc✝ : c ∣ a * b<VAR>d₁ d₂ : α<VAR>hd₁ : d₁ ∣ a<VAR>hd₂ : d₂ ∣ b<VAR>hc : c = d₁ * d₂<GOAL>Associated (d₁ ^ k) a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b c : α<VAR>hab : IsUnit (gcd a b)<VAR>k : ℕ<VAR>h : a * b = c ^ k<VAR>h✝ : Nontrivial α<VAR>ha : ¬a = 0<VAR>hb : ¬b = 0<VAR>hk : k > 0<VAR>hc✝ : c ∣ a * b<VAR>d₁ d₂ : α<VAR>hd₁ : d₁ ∣ a<VAR>hd₂ : d₂ ∣ b<VAR>hc : c = d₁ * d₂<VAR>h0₁ : d₁ ^ k ≠ 0<VAR>a' : α<VAR>ha' : a = d₁ ^ k * a'<GOAL>Associated (d₁ ^ k) a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b c : α<VAR>hab : IsUnit (gcd a b)<VAR>k : ℕ<VAR>h : b * a = c ^ k<VAR>h✝ : Nontrivial α<VAR>ha : ¬a = 0<VAR>hb : ¬b = 0<VAR>hk : k > 0<VAR>hc✝ : c ∣ a * b<VAR>d₁ d₂ : α<VAR>hd₁ : d₁ ∣ a<VAR>hd₂ : d₂ ∣ b<VAR>hc : c = d₂ * d₁<VAR>h0₁ : d₁ ^ k ≠ 0<VAR>a' : α<VAR>ha' : a = d₁ ^ k * a'<GOAL>Associated (d₁ ^ k) a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b c : α<VAR>hab : IsUnit (gcd b a)<VAR>k : ℕ<VAR>h : b * a = c ^ k<VAR>h✝ : Nontrivial α<VAR>ha : ¬a = 0<VAR>hb : ¬b = 0<VAR>hk : k > 0<VAR>hc✝ : c ∣ a * b<VAR>d₁ d₂ : α<VAR>hd₁ : d₁ ∣ a<VAR>hd₂ : d₂ ∣ b<VAR>hc : c = d₂ * d₁<VAR>h0₁ : d₁ ^ k ≠ 0<VAR>a' : α<VAR>ha' : a = d₁ ^ k * a'<GOAL>Associated (d₁ ^ k) a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b c : α<VAR>hab : IsUnit (gcd b a)<VAR>k : ℕ<VAR>h : b * a = c ^ k<VAR>h✝ : Nontrivial α<VAR>ha : ¬a = 0<VAR>hb : ¬b = 0<VAR>hk : k > 0<VAR>hc✝ : c ∣ a * b<VAR>d₁ d₂ : α<VAR>hd₁ : d₁ ∣ a<VAR>hd₂ : d₂ ∣ b<VAR>hc : c = d₂ * d₁<VAR>h0₁ : d₁ ^ k ≠ 0<VAR>a' : α<VAR>ha' : a = d₁ ^ k * a'<VAR>h0₂ : d₂ ^ k ≠ 0<VAR>b' : α<VAR>hb' : b = d₂ ^ k * b'<GOAL>Associated (d₁ ^ k) a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b c : α<VAR>hab : IsUnit (gcd b a)<VAR>k : ℕ<VAR>h✝ : Nontrivial α<VAR>ha : ¬a = 0<VAR>hb : ¬b = 0<VAR>hk : k > 0<VAR>hc✝ : c ∣ a * b<VAR>d₁ d₂ : α<VAR>hd₁ : d₁ ∣ a<VAR>hd₂ : d₂ ∣ b<VAR>hc : c = d₂ * d₁<VAR>h0₁ : d₁ ^ k ≠ 0<VAR>a' : α<VAR>ha' : a = d₁ ^ k * a'<VAR>h0₂ : d₂ ^ k ≠ 0<VAR>b' : α<VAR>h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k<VAR>hb' : b = d₂ ^ k * b'<GOAL>Associated (d₁ ^ k) a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b c : α<VAR>hab : IsUnit (gcd b a)<VAR>k : ℕ<VAR>h✝ : Nontrivial α<VAR>ha : ¬a = 0<VAR>hb : ¬b = 0<VAR>hk : k > 0<VAR>hc✝ : c ∣ a * b<VAR>d₁ d₂ : α<VAR>hd₁ : d₁ ∣ a<VAR>hd₂ : d₂ ∣ b<VAR>hc : c = d₂ * d₁<VAR>h0₁ : d₁ ^ k ≠ 0<VAR>a' : α<VAR>ha' : a = d₁ ^ k * a'<VAR>h0₂ : d₂ ^ k ≠ 0<VAR>b' : α<VAR>h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k<VAR>hb' : b = d₂ ^ k * b'<VAR>h' : a' * b' = 1<GOAL>Associated (d₁ ^ k) a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b c : α<VAR>hab : IsUnit (gcd b a)<VAR>k : ℕ<VAR>h✝ : Nontrivial α<VAR>ha : ¬a = 0<VAR>hb : ¬b = 0<VAR>hk : k > 0<VAR>hc✝ : c ∣ a * b<VAR>d₁ d₂ : α<VAR>hd₁ : d₁ ∣ a<VAR>hd₂ : d₂ ∣ b<VAR>hc : c = d₂ * d₁<VAR>h0₁ : d₁ ^ k ≠ 0<VAR>a' : α<VAR>ha' : a = d₁ ^ k * a'<VAR>h0₂ : d₂ ^ k ≠ 0<VAR>b' : α<VAR>h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k<VAR>hb' : b = d₂ ^ k * b'<VAR>h' : a' * b' = 1<GOAL>d₁ ^ k * ↑(Units.mkOfMulEqOne a' b' h') = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq α<VAR>a a✝ : α<GOAL>(toFinsupp {a}) a✝ = (Finsupp.single a 1) a✝
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x✝ y z : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>s : Set E<VAR>x : E<GOAL>infEdist x (thickening δ s) = infEdist x s - ENNReal.ofReal δ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x✝ y z : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>s : Set E<VAR>x : E<VAR>hs : infEdist x s < ENNReal.ofReal δ<GOAL>infEdist x (thickening δ s) = infEdist x s - ENNReal.ofReal δ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x✝ y z : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>s : Set E<VAR>x : E<VAR>hs : ENNReal.ofReal δ ≤ infEdist x s<GOAL>infEdist x (thickening δ s) = infEdist x s - ENNReal.ofReal δ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x✝ y z : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>s : Set E<VAR>x : E<VAR>hs : ENNReal.ofReal δ ≤ infEdist x s<GOAL>infEdist x (thickening δ s) ≤ infEdist x s - ENNReal.ofReal δ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x✝ y z : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>s : Set E<VAR>x : E<VAR>hs : ENNReal.ofReal δ ≤ infEdist x s<GOAL>infEdist x (thickening δ s) + ENNReal.ofReal δ ≤ infEdist x s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x✝ y z✝ : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>s : Set E<VAR>x : E<VAR>hs : ENNReal.ofReal δ ≤ infEdist x s<VAR>z : E<VAR>hz : z ∈ s<VAR>r : ℝ≥0∞<VAR>h : edist x z < r<GOAL>infEdist x (thickening δ s) + ENNReal.ofReal δ < r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x✝ y z✝ : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>s : Set E<VAR>x : E<VAR>hs : ENNReal.ofReal δ ≤ infEdist x s<VAR>z : E<VAR>hz : z ∈ s<VAR>r : NNReal<VAR>h : edist x z < ↑r<GOAL>infEdist x (thickening δ s) + ENNReal.ofReal δ < ↑r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x✝ y z✝ : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>s : Set E<VAR>x : E<VAR>hs : ENNReal.ofReal δ ≤ infEdist x s<VAR>z : E<VAR>hz : z ∈ s<VAR>r : NNReal<VAR>h : edist x z < ↑r<VAR>hr : 0 < ↑r - δ<GOAL>infEdist x (thickening δ s) + ENNReal.ofReal δ < ↑r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x✝ y z✝ : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>s : Set E<VAR>x : E<VAR>hs : ENNReal.ofReal δ ≤ infEdist x s<VAR>z : E<VAR>hz : z ∈ s<VAR>r : NNReal<VAR>h : dist x z < δ + (↑r - δ)<VAR>hr : 0 < ↑r - δ<GOAL>infEdist x (thickening δ s) + ENNReal.ofReal δ < ↑r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x✝ y✝ z✝ : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>s : Set E<VAR>x : E<VAR>hs : ENNReal.ofReal δ ≤ infEdist x s<VAR>z : E<VAR>hz : z ∈ s<VAR>r : NNReal<VAR>h : dist x z < δ + (↑r - δ)<VAR>hr : 0 < ↑r - δ<VAR>y : E<VAR>hxy : dist x y < ↑r - δ<VAR>hyz : dist y z < δ<GOAL>infEdist x (thickening δ s) + ENNReal.ofReal δ < ↑r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x✝ y✝ z✝ : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>s : Set E<VAR>x : E<VAR>hs : ENNReal.ofReal δ ≤ infEdist x s<VAR>z : E<VAR>hz : z ∈ s<VAR>r : NNReal<VAR>h : dist x z < δ + (↑r - δ)<VAR>hr : 0 < ↑r - δ<VAR>y : E<VAR>hxy : dist x y < ↑r - δ<VAR>hyz : dist y z < δ<GOAL>ENNReal.ofReal (↑r - δ) + ENNReal.ofReal δ ≤ ↑r
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasZeroObject C<VAR>ι : Type u_1<VAR>inst✝ : DecidableEq ι<VAR>c : ComplexShape ι<VAR>j : ι<VAR>A : C<GOAL>(singleObjCyclesSelfIso c j A).hom ≫ (singleObjHomologySelfIso c j A).inv = ((single C c j).obj A).homologyπ j
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>f : α → α<VAR>h : id ≤ f<VAR>n : ℕ<GOAL>id ≤ f^[n]
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v s t : Finset α<VAR>hA : A.Nonempty<VAR>hε : 0 < ε<VAR>hP : P.IsEquipartition<VAR>hG : P.IsUniform G ε<GOAL>∑ i ∈ P.nonUniforms G ε, ↑i.1.card * ↑i.2.card < ε * (↑A.card + ↑P.parts.card) ^ 2
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v s t : Finset α<VAR>hA : A.Nonempty<VAR>hε : 0 < ε<VAR>hP : P.IsEquipartition<VAR>hG : P.IsUniform G ε<GOAL>∀ x ∈ P.nonUniforms G ε, ↑x.1.card * ↑x.2.card ≤ ↑(A.card / P.parts.card + 1) ^ 2
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v s t : Finset α<VAR>hA : A.Nonempty<VAR>hε : 0 < ε<VAR>hP : P.IsEquipartition<VAR>hG : P.IsUniform G ε<GOAL>↑(P.parts.card * (P.parts.card - 1)) * ε * ↑(A.card / P.parts.card + 1) ^ 2 < ε * (↑A.card + ↑P.parts.card) ^ 2
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s✝ s₁ s₂ : Set ι<VAR>t✝ t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<VAR>s : Set ι<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>t : (i : ι) → Set (α i)<VAR>x✝ : (i : ι) → α i<GOAL>(x✝ ∈ univ.pi fun i => if i ∈ s then t i else univ) ↔ x✝ ∈ s.pi t
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s✝ s₁ s₂ : Set ι<VAR>t✝ t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<VAR>s : Set ι<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>t : (i : ι) → Set (α i)<VAR>x✝ : (i : ι) → α i<GOAL>(∀ i ∈ univ, x✝ i ∈ if i ∈ s then t i else univ) ↔ ∀ i ∈ s, x✝ i ∈ t i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s✝ s₁ s₂ : Set ι<VAR>t✝ t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<VAR>s : Set ι<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>t : (i : ι) → Set (α i)<VAR>x✝ : (i : ι) → α i<GOAL>∀ (a : ι), (a ∈ univ → x✝ a ∈ if a ∈ s then t a else univ) ↔ a ∈ s → x✝ a ∈ t a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>h : (s ∩ t).Finite<GOAL>s.encard < t.encard ↔ (s \ t).encard < (t \ s).encard
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Category.{?u.76393, u_1} C<VAR>inst✝ : Abelian C<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>IsLimit (ShortComplex.π₁.mapCone (KernelFork.ofι (S.mapNatTrans (natTransHomologyι C c i)) ⋯))
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Category.{?u.76393, u_1} C<VAR>inst✝ : Abelian C<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>IsLimit (ShortComplex.π₂.mapCone (KernelFork.ofι (S.mapNatTrans (natTransHomologyι C c i)) ⋯))
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Category.{?u.76393, u_1} C<VAR>inst✝ : Abelian C<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>IsLimit (ShortComplex.π₃.mapCone (KernelFork.ofι (S.mapNatTrans (natTransHomologyι C c i)) ⋯))
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Category.{?u.76393, u_1} C<VAR>inst✝ : Abelian C<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>IsColimit (ShortComplex.π₁.mapCocone (CokernelCofork.ofπ (S.mapNatTrans (natTransHomologyπ C c j)) ⋯))
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Category.{?u.76393, u_1} C<VAR>inst✝ : Abelian C<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>IsColimit (ShortComplex.π₂.mapCocone (CokernelCofork.ofπ (S.mapNatTrans (natTransHomologyπ C c j)) ⋯))
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Category.{?u.76393, u_1} C<VAR>inst✝ : Abelian C<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>IsColimit (ShortComplex.π₃.mapCocone (CokernelCofork.ofπ (S.mapNatTrans (natTransHomologyπ C c j)) ⋯))
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Category.{?u.76393, u_1} C<VAR>inst✝ : Abelian C<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>((opcyclesFunctor C c i).mapShortComplex.obj S).Exact