ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂✝ : Finset ι₂<VAR>inst✝ : DecidableEq ι<VAR>s₂ : Finset ι<VAR>h : s₂ ⊆ s<VAR>w : ι → k<VAR>p : ι → P<GOAL>((s \ s₂).weightedVSubOfPoint p (Classical.choice ⋯)) w - (s₂.weightedVSubOfPoint p (Classical.choice ⋯)) (-w) = (s.weightedVSub p) w
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<GOAL>re (⟪x, y⟫_𝕜 * ⟪y, x⟫_𝕜) = ‖⟪x, y⟫_𝕜 * ⟪y, x⟫_𝕜‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<GOAL>re (⟪y, x⟫_𝕜 * (starRingEnd 𝕜) ⟪y, x⟫_𝕜) = ‖⟪y, x⟫_𝕜 * (starRingEnd 𝕜) ⟪y, x⟫_𝕜‖
<VAR>n : ℕ<VAR>q : ℝ<VAR>hn' : 3 ≤ n<VAR>hq' : 1 < q<GOAL>eval q (cyclotomic n ℝ) < (q + 1) ^ φ n
<VAR>n : ℕ<VAR>q : ℝ<VAR>hn' : 3 ≤ n<VAR>hq' : 1 < q<VAR>hn : 0 < n<GOAL>eval q (cyclotomic n ℝ) < (q + 1) ^ φ n
<VAR>n : ℕ<VAR>q : ℝ<VAR>hn' : 3 ≤ n<VAR>hq' : 1 < q<VAR>hn : 0 < n<VAR>hq : 0 < q<GOAL>eval q (cyclotomic n ℝ) < (q + 1) ^ φ n
<VAR>n : ℕ<VAR>q : ℝ<VAR>hn' : 3 ≤ n<VAR>hq' : 1 < q<VAR>hn : 0 < n<VAR>hq : 0 < q<VAR>hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1<VAR>ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)<GOAL>eval q (cyclotomic n ℝ) < (q + 1) ^ φ n
<VAR>n : ℕ<VAR>q : ℝ<VAR>hn' : 3 ≤ n<VAR>hq' : 1 < q<VAR>hn : 0 < n<VAR>hq : 0 < q<VAR>hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1<VAR>ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)<VAR>hζ : IsPrimitiveRoot ζ n<GOAL>eval q (cyclotomic n ℝ) < (q + 1) ^ φ n
<VAR>n : ℕ<VAR>q : ℝ<VAR>hn' : 3 ≤ n<VAR>hq' : 1 < q<VAR>hn : 0 < n<VAR>hq : 0 < q<VAR>hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1<VAR>ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)<VAR>hζ : IsPrimitiveRoot ζ n<VAR>hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1<GOAL>eval q (cyclotomic n ℝ) < (q + 1) ^ φ n
<VAR>n : ℕ<VAR>q : ℝ<VAR>hn' : 3 ≤ n<VAR>hq' : 1 < q<VAR>hn : 0 < n<VAR>hq : 0 < q<VAR>hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1<VAR>ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)<VAR>hζ : IsPrimitiveRoot ζ n<VAR>hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1<VAR>this : ¬eval (↑q) (cyclotomic n ℂ) = 0<GOAL>eval q (cyclotomic n ℝ) < (q + 1) ^ φ n
<VAR>n : ℕ<VAR>q : ℝ<VAR>hn' : 3 ≤ n<VAR>hq' : 1 < q<VAR>hn : 0 < n<VAR>hq : 0 < q<VAR>hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1<VAR>ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)<VAR>hζ : IsPrimitiveRoot ζ n<VAR>hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1<VAR>this : ¬eval (↑q) (cyclotomic n ℂ) = 0<GOAL>Units.mk0 ‖eval (↑q) (cyclotomic n ℂ)‖₊ ⋯ < Units.mk0 (q + 1).toNNReal ⋯ ^ φ n
<VAR>n : ℕ<VAR>q : ℝ<VAR>hn' : 3 ≤ n<VAR>hq' : 1 < q<VAR>hn : 0 < n<VAR>hq : 0 < q<VAR>hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1<VAR>ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)<VAR>hζ : IsPrimitiveRoot ζ n<VAR>hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1<VAR>this : ¬eval (↑q) (cyclotomic n ℂ) = 0<GOAL>∏ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 ‖↑q - ↑i‖₊ ⋯ < Units.mk0 (q + 1).toNNReal ⋯ ^ φ n
<VAR>n : ℕ<VAR>q : ℝ<VAR>hn' : 3 ≤ n<VAR>hq' : 1 < q<VAR>hn : 0 < n<VAR>hq : 0 < q<VAR>hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1<VAR>ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)<VAR>hζ : IsPrimitiveRoot ζ n<VAR>hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1<VAR>this : ¬eval (↑q) (cyclotomic n ℂ) = 0<GOAL>Units.mk0 (q + 1).toNNReal ⋯ ^ φ n = ∏ i ∈ (primitiveRoots n ℂ).attach, ?convert_3 i
<VAR>n : ℕ<VAR>q : ℝ<VAR>hn' : 3 ≤ n<VAR>hq' : 1 < q<VAR>hn : 0 < n<VAR>hq : 0 < q<VAR>hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1<VAR>ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)<VAR>hζ : IsPrimitiveRoot ζ n<VAR>hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1<VAR>this : ¬eval (↑q) (cyclotomic n ℂ) = 0<GOAL>{ x // x ∈ primitiveRoots n ℂ } → NNRealˣ
<VAR>n : ℕ<VAR>q : ℝ<VAR>hn' : 3 ≤ n<VAR>hq' : 1 < q<VAR>hn : 0 < n<VAR>hq : 0 < q<VAR>hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1<VAR>ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)<VAR>hζ : IsPrimitiveRoot ζ n<VAR>hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1<VAR>this : ¬eval (↑q) (cyclotomic n ℂ) = 0<GOAL>∀ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 ‖↑q - ↑i‖₊ ⋯ ≤ ?convert_3 i
<VAR>n : ℕ<VAR>q : ℝ<VAR>hn' : 3 ≤ n<VAR>hq' : 1 < q<VAR>hn : 0 < n<VAR>hq : 0 < q<VAR>hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1<VAR>ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)<VAR>hζ : IsPrimitiveRoot ζ n<VAR>hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1<VAR>this : ¬eval (↑q) (cyclotomic n ℂ) = 0<GOAL>∃ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 ‖↑q - ↑i‖₊ ⋯ < ?convert_3 i
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hp : p.Monic<VAR>hq : q ≠ 0<GOAL>(p * q).natDegree = p.natDegree + q.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hp : p.Monic<VAR>hq : q ≠ 0<GOAL>p.leadingCoeff * q.leadingCoeff ≠ 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Semiring R<VAR>m n✝ : σ →₀ ℕ<VAR>φ ψ : MvPowerSeries σ R<VAR>n : σ →₀ ℕ<GOAL>(coeff R n) (φ * 1) = (coeff R n) φ
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝² : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq δ<VAR>s t : Finset δ<VAR>f✝ g : ((i : δ) → π i) → ℝ≥0∞<VAR>x✝ y : (i : δ) → π i<VAR>i✝ : δ<VAR>f : ((i : δ) → π i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>i : δ<VAR>hi : i ∈ s<VAR>x : (i : δ) → π i<GOAL>(∫⋯∫⁻_s, f ∂μ) x = ∫⁻ (xᵢ : π i), (∫⋯∫⁻_s.erase i, f ∂μ) (update x i xᵢ) ∂μ i
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>a : ℝ<VAR>h : a ≠ 0<GOAL>ContinuousAt (fun p => p.1 * p.2) (⊤, ↑a)
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>a : ℝ<VAR>h : a ≠ 0<VAR>a_neg : a < 0<GOAL>ContinuousAt (fun p => p.1 * p.2) (⊤, ↑a)
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>a : ℝ<VAR>h : a ≠ 0<VAR>a_pos : a > 0<GOAL>ContinuousAt (fun p => p.1 * p.2) (⊤, ↑a)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f g : Filter α<VAR>s✝ t✝ s t : Set α<GOAL>𝓟 s ≤ 𝓟 t ↔ s ⊆ t
<VAR>n : ℕ<VAR>f : Vector ℕ n → ℕ<VAR>hf : Primrec' f<GOAL>Primrec' fun v => (unpair (f v)).1
<VAR>n : ℕ<VAR>f : Vector ℕ n → ℕ<VAR>hf : Primrec' f<VAR>s : Primrec' fun v => (f v).sqrt<GOAL>Primrec' fun v => (unpair (f v)).1
<VAR>n : ℕ<VAR>f : Vector ℕ n → ℕ<VAR>hf : Primrec' f<VAR>s : Primrec' fun v => (f v).sqrt<VAR>fss : Primrec' fun v => f v - (f v).sqrt * (f v).sqrt<GOAL>Primrec' fun v => (unpair (f v)).1
<VAR>n : ℕ<VAR>f : Vector ℕ n → ℕ<VAR>hf : Primrec' f<VAR>s : Primrec' fun v => (f v).sqrt<VAR>fss : Primrec' fun v => f v - (f v).sqrt * (f v).sqrt<VAR>v : Vector ℕ n<GOAL>(if f v - (f v).sqrt * (f v).sqrt < (f v).sqrt then f v - (f v).sqrt * (f v).sqrt else (f v).sqrt) = (unpair (f v)).1
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>fp : Finpartition univ := h.finpartition<GOAL>fp.parts.card = min (Fintype.card V) r
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>fp : Finpartition univ := h.finpartition<GOAL>min univ.card r ≤ fp.parts.card
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>fp : Finpartition univ := h.finpartition<VAR>l : fp.parts.card < min univ.card r<GOAL>False
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>fp : Finpartition univ := h.finpartition<VAR>l : fp.parts.card < univ.card ∧ fp.parts.card < r<GOAL>False
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>fp : Finpartition univ := h.finpartition<VAR>l : fp.parts.card < univ.card ∧ fp.parts.card < r<VAR>x y : V<VAR>hn : x ≠ y<VAR>he : fp.part x = fp.part y<GOAL>False
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>fp : Finpartition univ := h.finpartition<VAR>l : fp.parts.card < univ.card ∧ fp.parts.card < r<VAR>x y : V<VAR>hn : x ≠ y<VAR>he : fp.part x = fp.part y<GOAL>∃ H inst, H.CliqueFree (r + 1) ∧ G.edgeFinset.card < H.edgeFinset.card
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>fp : Finpartition univ := h.finpartition<VAR>l : fp.parts.card < univ.card ∧ fp.parts.card < r<VAR>x y : V<VAR>hn : x ≠ y<VAR>he : fp.part x = fp.part y<VAR>cf : G.CliqueFree r<GOAL>∃ H inst, H.CliqueFree (r + 1) ∧ G.edgeFinset.card < H.edgeFinset.card
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>fp : Finpartition univ := h.finpartition<VAR>l : fp.parts.card < univ.card ∧ fp.parts.card < r<VAR>x y : V<VAR>hn : x ≠ y<VAR>he : fp.part x = fp.part y<VAR>cf : G.CliqueFree r<GOAL>G.edgeFinset.card < (G ⊔ edge x y).edgeFinset.card
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>fp : Finpartition univ := h.finpartition<VAR>l : fp.parts.card < univ.card ∧ fp.parts.card < r<VAR>x y : V<VAR>hn : x ≠ y<VAR>he : fp.part x = fp.part y<VAR>cf : G.CliqueFree r<GOAL>(G ⊔ edge x y).edgeFinset.card = G.edgeFinset.card.succ
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>fp : Finpartition univ := h.finpartition<VAR>l : fp.parts.card < univ.card ∧ fp.parts.card < r<VAR>x y : V<VAR>hn : x ≠ y<VAR>he : fp.part x = fp.part y<VAR>cf : G.CliqueFree r<GOAL>¬G.Adj x y
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>inst✝¹² : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁹ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁸ : TopologicalSpace M'<VAR>inst✝⁷ : ChartedSpace H' M'<VAR>inst✝⁶ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝³ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝² : TopologicalSpace M''<VAR>inst✝¹ : ChartedSpace H'' M''<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s : Set M<VAR>x : M<VAR>hxs : UniqueMDiffWithinAt I s x<GOAL>mfderivWithin I I id s x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>inst✝¹² : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁹ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁸ : TopologicalSpace M'<VAR>inst✝⁷ : ChartedSpace H' M'<VAR>inst✝⁶ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝³ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝² : TopologicalSpace M''<VAR>inst✝¹ : ChartedSpace H'' M''<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s : Set M<VAR>x : M<VAR>hxs : UniqueMDiffWithinAt I s x<GOAL>mfderiv I I id x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v w : V<GOAL>G.edist u w ≤ G.edist u v + G.edist v w
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>huv : G.edist u v = ⊤<GOAL>G.edist u w ≤ G.edist u v + G.edist v w
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>huv : G.edist u v ≠ ⊤<GOAL>G.edist u w ≤ G.edist u v + G.edist v w
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝² : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>U V✝ W✝ X✝ Y✝ Z✝ V W X Y Z : C<VAR>f : V ≅ W<VAR>g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>(f.inv ⊗ g) ≫ (f.hom ⊗ h) = (𝟙 W ⊗ g) ≫ (𝟙 W ⊗ h)
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝² : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>U V✝ W✝ X✝ Y✝ Z✝ V W X Y Z : C<VAR>f : V ≅ W<VAR>g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>𝟙 W ⊗ g ≫ h = (𝟙 W ⊗ g) ≫ (𝟙 W ⊗ h)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝³ : μ.InnerRegularCompactLTTop<VAR>inst✝² : IsLocallyFiniteMeasure μ<VAR>inst✝¹ : R1Space α<VAR>inst✝ : BorelSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ U, IsOpen U ∧ μ U < ⊤ ∧ μ (U ∆ s) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝³ : μ.InnerRegularCompactLTTop<VAR>inst✝² : IsLocallyFiniteMeasure μ<VAR>inst✝¹ : R1Space α<VAR>inst✝ : BorelSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>this : ε / 2 ≠ 0<GOAL>∃ U, IsOpen U ∧ μ U < ⊤ ∧ μ (U ∆ s) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝³ : μ.InnerRegularCompactLTTop<VAR>inst✝² : IsLocallyFiniteMeasure μ<VAR>inst✝¹ : R1Space α<VAR>inst✝ : BorelSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>this : ε / 2 ≠ 0<VAR>K : Set α<VAR>hKs : K ⊆ s<VAR>hKco : IsCompact K<VAR>hKcl : IsClosed K<VAR>hμK : μ (s \ K) < ε / 2<GOAL>∃ U, IsOpen U ∧ μ U < ⊤ ∧ μ (U ∆ s) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝³ : μ.InnerRegularCompactLTTop<VAR>inst✝² : IsLocallyFiniteMeasure μ<VAR>inst✝¹ : R1Space α<VAR>inst✝ : BorelSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>this : ε / 2 ≠ 0<VAR>K : Set α<VAR>hKs : K ⊆ s<VAR>hKco : IsCompact K<VAR>hKcl : IsClosed K<VAR>hμK : μ (s \ K) < ε / 2<VAR>U : Set α<VAR>hKU : K ⊆ U<VAR>hUo : IsOpen U<VAR>hμU : μ U < μ K + ε / 2<GOAL>∃ U, IsOpen U ∧ μ U < ⊤ ∧ μ (U ∆ s) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝³ : μ.InnerRegularCompactLTTop<VAR>inst✝² : IsLocallyFiniteMeasure μ<VAR>inst✝¹ : R1Space α<VAR>inst✝ : BorelSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>this : ε / 2 ≠ 0<VAR>K : Set α<VAR>hKs : K ⊆ s<VAR>hKco : IsCompact K<VAR>hKcl : IsClosed K<VAR>hμK : μ (s \ K) < ε / 2<VAR>U : Set α<VAR>hKU : K ⊆ U<VAR>hUo : IsOpen U<VAR>hμU : μ U < μ K + ε / 2<GOAL>μ (U ∆ s) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝³ : μ.InnerRegularCompactLTTop<VAR>inst✝² : IsLocallyFiniteMeasure μ<VAR>inst✝¹ : R1Space α<VAR>inst✝ : BorelSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>this : ε / 2 ≠ 0<VAR>K : Set α<VAR>hKs : K ⊆ s<VAR>hKco : IsCompact K<VAR>hKcl : IsClosed K<VAR>hμK : μ (s \ K) < ε / 2<VAR>U : Set α<VAR>hKU : K ⊆ U<VAR>hUo : IsOpen U<VAR>hμU : μ U < μ K + ε / 2<GOAL>μ (U \ s) + μ (s \ U) < ε / 2 + ε / 2
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝³ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝² : Monoid N<VAR>inst✝¹ : (i : ι) → DecidableEq (M i)<VAR>inst✝ : DecidableEq ι<VAR>m : CoprodI M<GOAL>∀ (w : Word M), (m • w).prod = m * w.prod
<VAR>p q : ℚ<VAR>s t : Set ℚ<VAR>H : (cocompact ℚ).IsCountablyGenerated<GOAL>False
<VAR>p q : ℚ<VAR>s t : Set ℚ<VAR>H : (cocompact ℚ).IsCountablyGenerated<VAR>x : ℕ → ℚ<VAR>hx : Tendsto x atTop (cocompact ℚ ⊓ 𝓝 0)<GOAL>False
<VAR>p q : ℚ<VAR>s t : Set ℚ<VAR>H : (cocompact ℚ).IsCountablyGenerated<VAR>x : ℕ → ℚ<VAR>hx : Tendsto x atTop (cocompact ℚ) ∧ Tendsto x atTop (𝓝 0)<GOAL>False
<VAR>p q : ℚ<VAR>s t : Set ℚ<VAR>H : (cocompact ℚ).IsCountablyGenerated<VAR>x : ℕ → ℚ<VAR>hxc : Tendsto x atTop (cocompact ℚ)<VAR>hx0 : Tendsto x atTop (𝓝 0)<GOAL>False
<VAR>p q : ℚ<VAR>s t : Set ℚ<VAR>H : (cocompact ℚ).IsCountablyGenerated<VAR>x : ℕ → ℚ<VAR>hxc : Tendsto x atTop (cocompact ℚ)<VAR>hx0 : Tendsto x atTop (𝓝 0)<VAR>n : ℕ<VAR>hn : x n ∉ insert 0 (range x)<GOAL>False
<VAR>R : Type u_1<VAR>inst✝² : Semiring R<VAR>f✝ : R[X]<VAR>S : Type u_2<VAR>inst✝¹ : CommSemiring S<VAR>i : R →+* S<VAR>x : S<VAR>inst✝ : Invertible x<VAR>N : ℕ<VAR>f : R[X]<VAR>hf : f.natDegree ≤ N<GOAL>eval₂ i (⅟x) (reflect N f) = 0 ↔ eval₂ i x f = 0
<VAR>R : Type u_1<VAR>inst✝² : Semiring R<VAR>f✝ : R[X]<VAR>S : Type u_2<VAR>inst✝¹ : CommSemiring S<VAR>i : R →+* S<VAR>x : S<VAR>inst✝ : Invertible x<VAR>N : ℕ<VAR>f : R[X]<VAR>hf : f.natDegree ≤ N<GOAL>eval₂ i (⅟x) (reflect N f) = 0 ↔ eval₂ i (⅟x) (reflect N f) * x ^ N = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : ConditionallyCompleteLinearOrder α<VAR>t : Set α<VAR>a b : α<VAR>s : Finset α<VAR>h : (↑s).Nonempty<GOAL>sSup ↑s ∈ ↑s
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁸ : SeminormedAddCommGroup V<VAR>inst✝⁷ : PseudoMetricSpace P<VAR>inst✝⁶ : NormedAddTorsor V P<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : MetricSpace Q<VAR>inst✝³ : NormedAddTorsor W Q<VAR>𝕜 : Type u_6<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 V<VAR>inst✝ : NormedSpace 𝕜 W<VAR>p₁ p₂ : P<VAR>c : 𝕜<GOAL>dist ((lineMap p₁ p₂) c) p₁ = ‖c‖ * dist p₁ p₂
<VAR>x : ℝ<GOAL>HasStrictDerivAt arctan (1 / (1 + x ^ 2)) x
<VAR>x : ℝ<VAR>A : cos (arctan x) ≠ 0<GOAL>HasStrictDerivAt arctan (1 / (1 + x ^ 2)) x
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : IsNoetherianRing R<VAR>s : Set ↥(maximalIdeal R)<GOAL>Submodule.span (ResidueField R) (⇑(maximalIdeal R).toCotangent '' s) = ⊤ ↔ Submodule.span R s = ⊤
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : IsNoetherianRing R<VAR>s : Set ↥(maximalIdeal R)<GOAL>Submodule.span R (⇑(maximalIdeal R).toCotangent '' s) = Submodule.restrictScalars R ⊤ ↔ Submodule.map (maximalIdeal R).toCotangent (Submodule.span R s) = ⊤
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : IsNoetherianRing R<VAR>s : Set ↥(maximalIdeal R)<GOAL>Function.Surjective ⇑(algebraMap R (ResidueField R))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a : α<GOAL>⌊a⌋ = 0 ↔ a ∈ Ico 0 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort u_6<VAR>κ : ι → Sort u_7<VAR>inst✝⁴ : FunLike F α β<VAR>inst✝³ : SupSet α<VAR>inst✝² : SupSet β<VAR>inst✝¹ : SupSet γ<VAR>inst✝ : SupSet δ<VAR>g : sSupHom β γ<VAR>f₁ f₂ : sSupHom α β<VAR>hg : Injective ⇑g<VAR>h : g.comp f₁ = g.comp f₂<VAR>a : α<GOAL>g (f₁ a) = g (f₂ a)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n + a = n'<VAR>p q : ℤ<VAR>hpq : p + n' = q<VAR>p' : ℤ<VAR>hp' : p' + n = q<GOAL>p' = p + a
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n + a = n'<VAR>p q : ℤ<VAR>hpq : p + n' = q<VAR>hp' : p + a + n = q<GOAL>(mk fun p q hpq => (a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) q ⋯).v p q hpq = (a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) q hp'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq β<VAR>f g : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<VAR>b c : β<GOAL>b ∈ image f s ↔ ∃ a ∈ s, f a = b
<VAR>n : Int<VAR>d : Nat<VAR>z : d ≠ 0<VAR>n' : Int<VAR>d' : Nat<VAR>z' : d' ≠ 0<VAR>c : n'.natAbs.Coprime d'<VAR>h : normalize n d z = { num := n', den := d', den_nz := z', reduced := c }<GOAL>∃ m, m ≠ 0 ∧ n = n' * ↑m ∧ d = d' * m
<VAR>n : Int<VAR>d : Nat<VAR>z : d ≠ 0<VAR>n' : Int<VAR>d' : Nat<VAR>z' : d' ≠ 0<VAR>c : n'.natAbs.Coprime d'<VAR>h : normalize n d z = { num := n', den := d', den_nz := z', reduced := c }<VAR>this : ∃ d_1, d_1 ≠ 0 ∧ n = (normalize n d z).num * ↑d_1 ∧ d = (normalize n d z).den * d_1<GOAL>∃ m, m ≠ 0 ∧ n = n' * ↑m ∧ d = d' * m
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x : ℝ≥0∞<GOAL>x⁻¹ < ⊤ ↔ 0 < x
<VAR>α : Sort u<VAR>β : α → Sort v<VAR>α' : Sort w<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq α'<VAR>f g : (a : α) → β a<VAR>a : α<VAR>b : β a<GOAL>update f a b = f ↔ b = f a
<VAR>s t : ℝ<VAR>ht : 0 < t<GOAL>IntegrableOn (fun x => x ^ s) (Ioi t) volume ↔ s < -1
<VAR>s t : ℝ<VAR>ht : 0 < t<VAR>h : IntegrableOn (fun x => x ^ s) (Ioi t) volume<GOAL>s < -1
<VAR>s t : ℝ<VAR>ht : 0 < t<VAR>h : -1 ≤ s<GOAL>¬IntegrableOn (fun x => x ^ s) (Ioi t) volume
<VAR>s t : ℝ<VAR>ht : 0 < t<VAR>h : -1 ≤ s<VAR>H : IntegrableOn (fun x => x ^ s) (Ioi t) volume<GOAL>False
<VAR>s t : ℝ<VAR>ht : 0 < t<VAR>h : -1 ≤ s<VAR>H : IntegrableOn (fun x => x ^ s) (Ioi t) volume<VAR>H' : IntegrableOn (fun x => x ^ s) (Ioi (max 1 t)) volume<GOAL>False
<VAR>s t : ℝ<VAR>ht : 0 < t<VAR>h : -1 ≤ s<VAR>H : IntegrableOn (fun x => x ^ s) (Ioi t) volume<VAR>H' : IntegrableOn (fun x => x ^ s) (Ioi (max 1 t)) volume<VAR>this : IntegrableOn (fun x => x⁻¹) (Ioi (max 1 t)) volume<GOAL>False
<VAR>a b c d : ℝ≥0∞<VAR>r✝ p q : ℝ≥0<VAR>R : Type u_1<VAR>r : R<VAR>s : ℝ≥0<VAR>inst✝³ : SMul R ℝ≥0<VAR>inst✝² : SMul R ℝ≥0∞<VAR>inst✝¹ : IsScalarTower R ℝ≥0 ℝ≥0<VAR>inst✝ : IsScalarTower R ℝ≥0 ℝ≥0∞<GOAL>↑(r • s) = r • ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a : α<VAR>ha : Finite a a<VAR>x✝ : a ^ (1 + 1) ∣ a<VAR>b : α<VAR>hb : a = a ^ (1 + 1) * b<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a : α<VAR>ha : Finite a a<VAR>x✝ : a ^ (1 + 1) ∣ a<VAR>b : α<VAR>hb : 1 = 1 * (a * 1 * b)<GOAL>False
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>inst✝³ : CompleteSpace E<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : SMulCommClass 𝕜 ℂ E<VAR>a : 𝕜<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<GOAL>(∮ (z : ℂ) in C(c, R), a • f z) = a • ∮ (z : ℂ) in C(c, R), f z
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f : X → ↑F X<VAR>x : ↑F F.M<VAR>n : ℕ<VAR>i : F.B x.fst<GOAL>Agree ((x.snd i).approx n) ((x.snd i).approx (n + 1))
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Finite<VAR>x : ℕ<GOAL>x ∈ nth p '' Set.Iio hf.toFinset.card ↔ x ∈ Set.range ⇑(hf.toFinset.orderEmbOfFin ⋯)
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Finite<GOAL>Set.range ⇑(hf.toFinset.orderEmbOfFin ⋯) = setOf p