ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜₁<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>inst✝¹⁰ : RingHomIsometric σ₁₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁹ : TopologicalSpace M₁<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : TopologicalSpace M₂<VAR>inst✝⁶ : AddCommGroup M₂<VAR>inst✝⁵ : Module 𝕜₁ M₁<VAR>inst✝⁴ : Module 𝕜₂ M₂<VAR>inst✝³ : TopologicalAddGroup M₁<VAR>inst✝² : ContinuousConstSMul 𝕜₁ M₁<VAR>inst✝¹ : TopologicalAddGroup M₂<VAR>inst✝ : ContinuousSMul 𝕜₂ M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>this✝ : UniformSpace M₂ := TopologicalAddGroup.toUniformSpace M₂<VAR>this : UniformAddGroup M₂<VAR>U : Set M₂<VAR>hU : U ∈ 𝓝 0<VAR>K : Set M₂<VAR>hK : IsCompact K<VAR>hKf : ⇑f ⁻¹' K ∈ 𝓝 0<GOAL>U ∈ map (⇑f) (𝓝 0)
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜₁<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>inst✝¹⁰ : RingHomIsometric σ₁₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁹ : TopologicalSpace M₁<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : TopologicalSpace M₂<VAR>inst✝⁶ : AddCommGroup M₂<VAR>inst✝⁵ : Module 𝕜₁ M₁<VAR>inst✝⁴ : Module 𝕜₂ M₂<VAR>inst✝³ : TopologicalAddGroup M₁<VAR>inst✝² : ContinuousConstSMul 𝕜₁ M₁<VAR>inst✝¹ : TopologicalAddGroup M₂<VAR>inst✝ : ContinuousSMul 𝕜₂ M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>this✝ : UniformSpace M₂ := TopologicalAddGroup.toUniformSpace M₂<VAR>this : UniformAddGroup M₂<VAR>U : Set M₂<VAR>hU : U ∈ 𝓝 0<VAR>K : Set M₂<VAR>hK : IsCompact K<VAR>hKf : ⇑f ⁻¹' K ∈ 𝓝 0<VAR>r : ℝ<VAR>hr : r > 0<VAR>hrU : ∀ (c : 𝕜₂), r ≤ ‖c‖ → K ⊆ c • U<GOAL>U ∈ map (⇑f) (𝓝 0)
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜₁<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>inst✝¹⁰ : RingHomIsometric σ₁₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁹ : TopologicalSpace M₁<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : TopologicalSpace M₂<VAR>inst✝⁶ : AddCommGroup M₂<VAR>inst✝⁵ : Module 𝕜₁ M₁<VAR>inst✝⁴ : Module 𝕜₂ M₂<VAR>inst✝³ : TopologicalAddGroup M₁<VAR>inst✝² : ContinuousConstSMul 𝕜₁ M₁<VAR>inst✝¹ : TopologicalAddGroup M₂<VAR>inst✝ : ContinuousSMul 𝕜₂ M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>this✝ : UniformSpace M₂ := TopologicalAddGroup.toUniformSpace M₂<VAR>this : UniformAddGroup M₂<VAR>U : Set M₂<VAR>hU : U ∈ 𝓝 0<VAR>K : Set M₂<VAR>hK : IsCompact K<VAR>hKf : ⇑f ⁻¹' K ∈ 𝓝 0<VAR>r : ℝ<VAR>hr : r > 0<VAR>hrU : ∀ (c : 𝕜₂), r ≤ ‖c‖ → K ⊆ c • U<VAR>c : 𝕜₁<VAR>hc : r < ‖c‖<GOAL>U ∈ map (⇑f) (𝓝 0)
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜₁<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>inst✝¹⁰ : RingHomIsometric σ₁₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁹ : TopologicalSpace M₁<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : TopologicalSpace M₂<VAR>inst✝⁶ : AddCommGroup M₂<VAR>inst✝⁵ : Module 𝕜₁ M₁<VAR>inst✝⁴ : Module 𝕜₂ M₂<VAR>inst✝³ : TopologicalAddGroup M₁<VAR>inst✝² : ContinuousConstSMul 𝕜₁ M₁<VAR>inst✝¹ : TopologicalAddGroup M₂<VAR>inst✝ : ContinuousSMul 𝕜₂ M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>this✝ : UniformSpace M₂ := TopologicalAddGroup.toUniformSpace M₂<VAR>this : UniformAddGroup M₂<VAR>U : Set M₂<VAR>hU : U ∈ 𝓝 0<VAR>K : Set M₂<VAR>hK : IsCompact K<VAR>hKf : ⇑f ⁻¹' K ∈ 𝓝 0<VAR>r : ℝ<VAR>hr : r > 0<VAR>hrU : ∀ (c : 𝕜₂), r ≤ ‖c‖ → K ⊆ c • U<VAR>c : 𝕜₁<VAR>hc : r < ‖c‖<VAR>hcnz : c ≠ 0<GOAL>U ∈ map (⇑f) (𝓝 0)
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜₁<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>inst✝¹⁰ : RingHomIsometric σ₁₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁹ : TopologicalSpace M₁<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : TopologicalSpace M₂<VAR>inst✝⁶ : AddCommGroup M₂<VAR>inst✝⁵ : Module 𝕜₁ M₁<VAR>inst✝⁴ : Module 𝕜₂ M₂<VAR>inst✝³ : TopologicalAddGroup M₁<VAR>inst✝² : ContinuousConstSMul 𝕜₁ M₁<VAR>inst✝¹ : TopologicalAddGroup M₂<VAR>inst✝ : ContinuousSMul 𝕜₂ M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>this✝ : UniformSpace M₂ := TopologicalAddGroup.toUniformSpace M₂<VAR>this : UniformAddGroup M₂<VAR>U : Set M₂<VAR>hU : U ∈ 𝓝 0<VAR>K : Set M₂<VAR>hK : IsCompact K<VAR>hKf : ⇑f ⁻¹' K ∈ 𝓝 0<VAR>r : ℝ<VAR>hr : r > 0<VAR>hrU : ∀ (c : 𝕜₂), r ≤ ‖c‖ → K ⊆ c • U<VAR>c : 𝕜₁<VAR>hc : r < ‖c‖<VAR>hcnz : c ≠ 0<GOAL>σ₁₂ c⁻¹ • K ⊆ U
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜₁<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>inst✝¹⁰ : RingHomIsometric σ₁₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁹ : TopologicalSpace M₁<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : TopologicalSpace M₂<VAR>inst✝⁶ : AddCommGroup M₂<VAR>inst✝⁵ : Module 𝕜₁ M₁<VAR>inst✝⁴ : Module 𝕜₂ M₂<VAR>inst✝³ : TopologicalAddGroup M₁<VAR>inst✝² : ContinuousConstSMul 𝕜₁ M₁<VAR>inst✝¹ : TopologicalAddGroup M₂<VAR>inst✝ : ContinuousSMul 𝕜₂ M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>this✝ : UniformSpace M₂ := TopologicalAddGroup.toUniformSpace M₂<VAR>this : UniformAddGroup M₂<VAR>U : Set M₂<VAR>hU : U ∈ 𝓝 0<VAR>K : Set M₂<VAR>hK : IsCompact K<VAR>hKf : ⇑f ⁻¹' K ∈ 𝓝 0<VAR>r : ℝ<VAR>hr : r > 0<VAR>hrU : ∀ (c : 𝕜₂), r ≤ ‖c‖ → K ⊆ c • U<VAR>c : 𝕜₁<VAR>hc : r < ‖c‖<VAR>hcnz : c ≠ 0<GOAL>K ⊆ σ₁₂ c • U
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜₁<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>inst✝¹⁰ : RingHomIsometric σ₁₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁹ : TopologicalSpace M₁<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : TopologicalSpace M₂<VAR>inst✝⁶ : AddCommGroup M₂<VAR>inst✝⁵ : Module 𝕜₁ M₁<VAR>inst✝⁴ : Module 𝕜₂ M₂<VAR>inst✝³ : TopologicalAddGroup M₁<VAR>inst✝² : ContinuousConstSMul 𝕜₁ M₁<VAR>inst✝¹ : TopologicalAddGroup M₂<VAR>inst✝ : ContinuousSMul 𝕜₂ M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>this✝ : UniformSpace M₂ := TopologicalAddGroup.toUniformSpace M₂<VAR>this : UniformAddGroup M₂<VAR>U : Set M₂<VAR>hU : U ∈ 𝓝 0<VAR>K : Set M₂<VAR>hK : IsCompact K<VAR>hKf : ⇑f ⁻¹' K ∈ 𝓝 0<VAR>r : ℝ<VAR>hr : r > 0<VAR>hrU : ∀ (c : 𝕜₂), r ≤ ‖c‖ → K ⊆ c • U<VAR>c : 𝕜₁<VAR>hc : r < ‖c‖<VAR>hcnz : c ≠ 0<GOAL>r ≤ ‖σ₁₂ c‖
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜₁<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>inst✝¹⁰ : RingHomIsometric σ₁₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁹ : TopologicalSpace M₁<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : TopologicalSpace M₂<VAR>inst✝⁶ : AddCommGroup M₂<VAR>inst✝⁵ : Module 𝕜₁ M₁<VAR>inst✝⁴ : Module 𝕜₂ M₂<VAR>inst✝³ : TopologicalAddGroup M₁<VAR>inst✝² : ContinuousConstSMul 𝕜₁ M₁<VAR>inst✝¹ : TopologicalAddGroup M₂<VAR>inst✝ : ContinuousSMul 𝕜₂ M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>this✝ : UniformSpace M₂ := TopologicalAddGroup.toUniformSpace M₂<VAR>this : UniformAddGroup M₂<VAR>U : Set M₂<VAR>hU : U ∈ 𝓝 0<VAR>K : Set M₂<VAR>hK : IsCompact K<VAR>hKf : ⇑f ⁻¹' K ∈ 𝓝 0<VAR>r : ℝ<VAR>hr : r > 0<VAR>hrU : ∀ (c : 𝕜₂), r ≤ ‖c‖ → K ⊆ c • U<VAR>c : 𝕜₁<VAR>hc : r < ‖c‖<VAR>hcnz : c ≠ 0<GOAL>r ≤ ‖c‖
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u t s s' : Set α<GOAL>tᶜ.ite s s' = t.ite s' s
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : S[X]<VAR>n : ℕ<VAR>h : p ∈ lifts f<GOAL>erase n p ∈ lifts f
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : S[X]<VAR>n : ℕ<VAR>h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS<GOAL>∀ (n_1 : ℕ), (erase n p).coeff n_1 ∈ f.rangeS
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : S[X]<VAR>n : ℕ<VAR>h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS<VAR>k : ℕ<VAR>hk : ¬k = n<VAR>i : R<VAR>hi : f i = p.coeff k<GOAL>(erase n p).coeff k ∈ f.rangeS
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : S[X]<VAR>n : ℕ<VAR>h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS<VAR>k : ℕ<VAR>hk : ¬k = n<VAR>i : R<VAR>hi : f i = p.coeff k<GOAL>f i = (erase n p).coeff k
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<GOAL>(cthickening δ s)⁻¹ = cthickening δ s⁻¹
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<GOAL>{x | EMetric.infEdist x s ≤ ENNReal.ofReal δ}⁻¹ = {x | EMetric.infEdist x⁻¹ s ≤ ENNReal.ofReal δ}
<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✝ : SupSet α<VAR>f✝ g✝ : ι → α<VAR>g : β → α<VAR>f : ι → β<GOAL>⨆ b, g ↑b = ⨆ i, g (f i)
<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✝ : SupSet α<VAR>f✝ g✝ : ι → α<VAR>g : β → α<VAR>f : ι → β<GOAL>sSup (range (g ∘ f)) = sSup (range fun i => g (f i))
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>inst✝ : CharZero k<VAR>n : ℕ<VAR>s : Simplex k P n<VAR>fs₁ fs₂ : Finset (Fin (n + 1))<VAR>m₁ m₂ : ℕ<VAR>h₁ : fs₁.card = m₁ + 1<VAR>h₂ : fs₂.card = m₂ + 1<GOAL>centroid k univ (s.face h₁).points = centroid k univ (s.face h₂).points ↔ fs₁ = fs₂
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>inst✝ : CharZero k<VAR>n : ℕ<VAR>s : Simplex k P n<VAR>fs₁ fs₂ : Finset (Fin (n + 1))<VAR>m₁ m₂ : ℕ<VAR>h₁ : fs₁.card = m₁ + 1<VAR>h₂ : fs₂.card = m₂ + 1<GOAL>centroid k fs₁ s.points = centroid k fs₂ s.points ↔ fs₁ = fs₂
<VAR>α✝ : Type u<VAR>α : Type u_1<VAR>inst✝ : CommRing α<VAR>x : α<VAR>n : ℕ<GOAL>∑ i ∈ range n, x ^ i * x ^ (n - 1 - i) = ∑ i ∈ range n, x ^ (i + (n - 1 - i))
<VAR>α✝ : Type u<VAR>α : Type u_1<VAR>inst✝ : CommRing α<VAR>x : α<VAR>n : ℕ<GOAL>(range n).card • x ^ (n - 1) = ↑n * x ^ (n - 1)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsArtinian R M<VAR>inst✝ : IsNoetherian R M<VAR>f : M →ₗ[R] M<GOAL>IsCompl (⨆ n, ker (f ^ n)) (⨅ n, range (f ^ n))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsArtinian R M<VAR>inst✝ : IsNoetherian R M<VAR>f : M →ₗ[R] M<VAR>k : ℕ<VAR>hk : ∀ b ≥ k, IsCompl (ker (f ^ b)) (range (f ^ b)) ∧ ⨅ m, range (f ^ m) = range (f ^ b) ∧ ⨆ m, ker (f ^ m) = ker (f ^ b)<GOAL>IsCompl (⨆ n, ker (f ^ n)) (⨅ n, range (f ^ n))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsArtinian R M<VAR>inst✝ : IsNoetherian R M<VAR>f : M →ₗ[R] M<VAR>k : ℕ<VAR>hk : ∀ b ≥ k, IsCompl (ker (f ^ b)) (range (f ^ b)) ∧ ⨅ m, range (f ^ m) = range (f ^ b) ∧ ⨆ m, ker (f ^ m) = ker (f ^ b)<VAR>h₁ : IsCompl (ker (f ^ k)) (range (f ^ k))<VAR>h₂ : ⨅ m, range (f ^ m) = range (f ^ k)<VAR>h₃ : ⨆ m, ker (f ^ m) = ker (f ^ k)<GOAL>IsCompl (⨆ n, ker (f ^ n)) (⨅ n, range (f ^ n))
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : MulOneClass M<VAR>s : Set M<VAR>inst✝ : AddZeroClass A<VAR>t : Set A<VAR>S✝ : Submonoid M<VAR>ι : Sort u_4<VAR>S : ι → Submonoid M<VAR>x : M<GOAL>x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : CommRing A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsDomain B<VAR>p : A[X]<VAR>f : A →+* B<VAR>h : map f p ≠ 0<GOAL>Multiset.map (⇑f) p.roots ≤ (map f p).roots
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R✝ : Type u<VAR>S : Type v<VAR>r : R✝<VAR>e : ℕ<VAR>n m : σ<VAR>inst✝¹ : CommSemiring R✝<VAR>p q : MvPolynomial σ R✝<VAR>s t : Set σ<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>F : MvPolynomial σ ℤ<VAR>hF : ↑F.vars ⊆ s<GOAL>∃ f, ∀ (x : σ → R), f (x ∘ Subtype.val) = (aeval x) F
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R✝ : Type u<VAR>S : Type v<VAR>r : R✝<VAR>e : ℕ<VAR>n m : σ<VAR>inst✝¹ : CommSemiring R✝<VAR>p q : MvPolynomial σ R✝<VAR>s t : Set σ<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>F : MvPolynomial σ ℤ<VAR>hF : ∃ x, (rename Subtype.val) x = F<GOAL>∃ f, ∀ (x : σ → R), f (x ∘ Subtype.val) = (aeval x) F
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R✝ : Type u<VAR>S : Type v<VAR>r : R✝<VAR>e : ℕ<VAR>n m : σ<VAR>inst✝¹ : CommSemiring R✝<VAR>p q : MvPolynomial σ R✝<VAR>s t : Set σ<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>F : MvPolynomial σ ℤ<VAR>F' : MvPolynomial { x // x ∈ s } ℤ<VAR>hF' : (rename Subtype.val) F' = F<GOAL>∃ f, ∀ (x : σ → R), f (x ∘ Subtype.val) = (aeval x) F
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R✝ : Type u<VAR>S : Type v<VAR>r : R✝<VAR>e : ℕ<VAR>n m : σ<VAR>inst✝¹ : CommSemiring R✝<VAR>p q : MvPolynomial σ R✝<VAR>s t : Set σ<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>F : MvPolynomial σ ℤ<VAR>F' : MvPolynomial { x // x ∈ s } ℤ<VAR>hF' : (rename Subtype.val) F' = F<GOAL>∀ (x : σ → R), (aeval (x ∘ Subtype.val)) F' = (aeval x) F
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R✝ : Type u<VAR>S : Type v<VAR>r : R✝<VAR>e : ℕ<VAR>n m : σ<VAR>inst✝¹ : CommSemiring R✝<VAR>p q : MvPolynomial σ R✝<VAR>s t : Set σ<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>F : MvPolynomial σ ℤ<VAR>F' : MvPolynomial { x // x ∈ s } ℤ<VAR>hF' : (rename Subtype.val) F' = F<VAR>x : σ → R<GOAL>(aeval (x ∘ Subtype.val)) F' = (aeval x) F
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>inst✝² : CanonicallyOrderedCommMonoid α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderClosedTopology α<VAR>f : ι → α<VAR>a : α<VAR>hf : Multipliable f<GOAL>∏' (i : ι), f i = 1 ↔ ∀ (x : ι), f x = 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² : OrderedCommRing S<VAR>inst✝¹ : Ring R<VAR>abv : AbsoluteValue R S<VAR>inst✝ : NoZeroDivisors S<VAR>a b : R<GOAL>abv a - abv b ≤ abv (a + b)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 0<VAR>hc : P.c = 0<GOAL>P.toPoly = C P.d
<VAR>x : SimplexCategory<VAR>i : x ⟶ x<VAR>inst✝ : Mono i<GOAL>i = 𝟙 x
<VAR>x : SimplexCategory<VAR>i : x ⟶ x<VAR>inst✝ : Mono i<GOAL>IsIso i
<VAR>x : SimplexCategory<VAR>i : x ⟶ x<VAR>inst✝ : Mono i<GOAL>Function.Bijective (Hom.toOrderHom i).toFun
<VAR>x : SimplexCategory<VAR>i : x ⟶ x<VAR>inst✝ : Mono i<GOAL>Function.Bijective ⇑(Hom.toOrderHom i)
<VAR>x : SimplexCategory<VAR>i : x ⟶ x<VAR>inst✝ : Mono i<GOAL>Mono i
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>x y : M × ↥S<GOAL>(r S) x y ↔ Setoid.r x y
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>x y : M × ↥S<GOAL>(∃ a ∈ S, a * (↑y.2 * x.1) = a * (↑x.2 * y.1)) ↔ ∃ a ∈ S, ∃ v, a * y.1 = v * x.1 ∧ a * ↑y.2 = v * ↑x.2
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>inst✝⁷ : HasZeroObject C<VAR>inst✝⁶ : HasShift C ℤ<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>J : Type u_1<VAR>T : J → Triangle C<VAR>hT : ∀ (j : J), T j ∈ distinguishedTriangles<VAR>inst✝³ : HasProduct fun j => (T j).obj₁<VAR>inst✝² : HasProduct fun j => (T j).obj₂<VAR>inst✝¹ : HasProduct fun j => (T j).obj₃<VAR>inst✝ : HasProduct fun j => (shiftFunctor C 1).obj (T j).obj₁<VAR>f₁ : (∏ᶜ fun j => (T j).obj₁) ⟶ ∏ᶜ fun j => (T j).obj₂ := Pi.map fun j => (T j).mor₁<GOAL>productTriangle T ∈ distinguishedTriangles
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>inst✝⁷ : HasZeroObject C<VAR>inst✝⁶ : HasShift C ℤ<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>J : Type u_1<VAR>T : J → Triangle C<VAR>hT : ∀ (j : J), T j ∈ distinguishedTriangles<VAR>inst✝³ : HasProduct fun j => (T j).obj₁<VAR>inst✝² : HasProduct fun j => (T j).obj₂<VAR>inst✝¹ : HasProduct fun j => (T j).obj₃<VAR>inst✝ : HasProduct fun j => (shiftFunctor C 1).obj (T j).obj₁<VAR>f₁ : (∏ᶜ fun j => (T j).obj₁) ⟶ ∏ᶜ fun j => (T j).obj₂ := Pi.map fun j => (T j).mor₁<VAR>Z : C<VAR>f₂ : (∏ᶜ fun j => (T j).obj₂) ⟶ Z<VAR>f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j => (T j).obj₁)<VAR>hT' : Triangle.mk f₁ f₂ f₃ ∈ distinguishedTriangles<GOAL>productTriangle T ∈ distinguishedTriangles
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>inst✝⁷ : HasZeroObject C<VAR>inst✝⁶ : HasShift C ℤ<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>J : Type u_1<VAR>T : J → Triangle C<VAR>hT : ∀ (j : J), T j ∈ distinguishedTriangles<VAR>inst✝³ : HasProduct fun j => (T j).obj₁<VAR>inst✝² : HasProduct fun j => (T j).obj₂<VAR>inst✝¹ : HasProduct fun j => (T j).obj₃<VAR>inst✝ : HasProduct fun j => (shiftFunctor C 1).obj (T j).obj₁<VAR>f₁ : (∏ᶜ fun j => (T j).obj₁) ⟶ ∏ᶜ fun j => (T j).obj₂ := Pi.map fun j => (T j).mor₁<VAR>Z : C<VAR>f₂ : (∏ᶜ fun j => (T j).obj₂) ⟶ Z<VAR>f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j => (T j).obj₁)<VAR>T' : Triangle C := Triangle.mk f₁ f₂ f₃<VAR>hT' : T' ∈ distinguishedTriangles<VAR>φ : (j : J) → T' ⟶ T j := fun j => completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j => (T j).obj₁) j) (Pi.π (fun j => (T j).obj₂) j) ⋯<VAR>φ' : T' ⟶ productTriangle T := productTriangle.lift T φ<VAR>h₁ : φ'.hom₁ = 𝟙 T'.obj₁<VAR>h₂ : φ'.hom₂ = 𝟙 T'.obj₂<VAR>this✝ : IsIso φ'.hom₁<VAR>this : IsIso φ'.hom₂<GOAL>productTriangle T ∈ distinguishedTriangles
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>inst✝⁷ : HasZeroObject C<VAR>inst✝⁶ : HasShift C ℤ<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>J : Type u_1<VAR>T : J → Triangle C<VAR>hT : ∀ (j : J), T j ∈ distinguishedTriangles<VAR>inst✝³ : HasProduct fun j => (T j).obj₁<VAR>inst✝² : HasProduct fun j => (T j).obj₂<VAR>inst✝¹ : HasProduct fun j => (T j).obj₃<VAR>inst✝ : HasProduct fun j => (shiftFunctor C 1).obj (T j).obj₁<VAR>f₁ : (∏ᶜ fun j => (T j).obj₁) ⟶ ∏ᶜ fun j => (T j).obj₂ := Pi.map fun j => (T j).mor₁<VAR>Z : C<VAR>f₂ : (∏ᶜ fun j => (T j).obj₂) ⟶ Z<VAR>f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j => (T j).obj₁)<VAR>T' : Triangle C := Triangle.mk f₁ f₂ f₃<VAR>hT' : T' ∈ distinguishedTriangles<VAR>φ : (j : J) → T' ⟶ T j := fun j => completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j => (T j).obj₁) j) (Pi.π (fun j => (T j).obj₂) j) ⋯<VAR>φ' : T' ⟶ productTriangle T := productTriangle.lift T φ<VAR>h₁ : φ'.hom₁ = 𝟙 T'.obj₁<VAR>h₂ : φ'.hom₂ = 𝟙 T'.obj₂<VAR>this✝ : IsIso φ'.hom₁<VAR>this : IsIso φ'.hom₂<GOAL>IsIso φ'.hom₃
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>inst✝⁷ : HasZeroObject C<VAR>inst✝⁶ : HasShift C ℤ<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>J : Type u_1<VAR>T : J → Triangle C<VAR>hT : ∀ (j : J), T j ∈ distinguishedTriangles<VAR>inst✝³ : HasProduct fun j => (T j).obj₁<VAR>inst✝² : HasProduct fun j => (T j).obj₂<VAR>inst✝¹ : HasProduct fun j => (T j).obj₃<VAR>inst✝ : HasProduct fun j => (shiftFunctor C 1).obj (T j).obj₁<VAR>f₁ : (∏ᶜ fun j => (T j).obj₁) ⟶ ∏ᶜ fun j => (T j).obj₂ := Pi.map fun j => (T j).mor₁<VAR>Z : C<VAR>f₂ : (∏ᶜ fun j => (T j).obj₂) ⟶ Z<VAR>f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j => (T j).obj₁)<VAR>T' : Triangle C := Triangle.mk f₁ f₂ f₃<VAR>hT' : T' ∈ distinguishedTriangles<VAR>φ : (j : J) → T' ⟶ T j := fun j => completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j => (T j).obj₁) j) (Pi.π (fun j => (T j).obj₂) j) ⋯<VAR>φ' : T' ⟶ productTriangle T := productTriangle.lift T φ<VAR>h₁ : φ'.hom₁ = 𝟙 T'.obj₁<VAR>h₂ : φ'.hom₂ = 𝟙 T'.obj₂<VAR>this✝ : IsIso φ'.hom₁<VAR>this : IsIso φ'.hom₂<VAR>A : C<GOAL>Function.Injective fun x => x ≫ φ'.hom₃
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>inst✝⁷ : HasZeroObject C<VAR>inst✝⁶ : HasShift C ℤ<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>J : Type u_1<VAR>T : J → Triangle C<VAR>hT : ∀ (j : J), T j ∈ distinguishedTriangles<VAR>inst✝³ : HasProduct fun j => (T j).obj₁<VAR>inst✝² : HasProduct fun j => (T j).obj₂<VAR>inst✝¹ : HasProduct fun j => (T j).obj₃<VAR>inst✝ : HasProduct fun j => (shiftFunctor C 1).obj (T j).obj₁<VAR>f₁ : (∏ᶜ fun j => (T j).obj₁) ⟶ ∏ᶜ fun j => (T j).obj₂ := Pi.map fun j => (T j).mor₁<VAR>Z : C<VAR>f₂ : (∏ᶜ fun j => (T j).obj₂) ⟶ Z<VAR>f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j => (T j).obj₁)<VAR>T' : Triangle C := Triangle.mk f₁ f₂ f₃<VAR>hT' : T' ∈ distinguishedTriangles<VAR>φ : (j : J) → T' ⟶ T j := fun j => completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j => (T j).obj₁) j) (Pi.π (fun j => (T j).obj₂) j) ⋯<VAR>φ' : T' ⟶ productTriangle T := productTriangle.lift T φ<VAR>h₁ : φ'.hom₁ = 𝟙 T'.obj₁<VAR>h₂ : φ'.hom₂ = 𝟙 T'.obj₂<VAR>this✝ : IsIso φ'.hom₁<VAR>this : IsIso φ'.hom₂<VAR>A : C<GOAL>Function.Surjective fun x => x ≫ φ'.hom₃
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : T1Space E<VAR>hs : Absorbent ℝ s<VAR>hb : Bornology.IsVonNBounded ℝ s<GOAL>gauge s x = 0 ↔ x = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : T1Space E<VAR>hs : Absorbent ℝ s<VAR>hb : Bornology.IsVonNBounded ℝ s<VAR>h₀ : gauge s x = 0<VAR>hne : x ≠ 0<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : T1Space E<VAR>hs : Absorbent ℝ s<VAR>hb : Bornology.IsVonNBounded ℝ s<VAR>h₀ : gauge s x = 0<VAR>hne : x ≠ 0<VAR>this : {x}ᶜ ∈ comap (gauge s) (𝓝 0)<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : T1Space E<VAR>hs : Absorbent ℝ s<VAR>hb : Bornology.IsVonNBounded ℝ s<VAR>h₀ : gauge s x = 0<VAR>hne : x ≠ 0<VAR>this : {x}ᶜ ∈ comap (gauge s) (𝓝 0)<VAR>r : ℝ<VAR>hr₀ : 0 < r<VAR>hr : gauge s ⁻¹' {b | |b| < r} ⊆ {x}ᶜ<GOAL>False
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : PartialOrder R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : RCLike 𝕜<VAR>A B : Matrix m m R<VAR>hA : A.PosSemidef<VAR>hB : B.PosDef<VAR>x : m → R<VAR>hx : x ≠ 0<GOAL>0 < star x ⬝ᵥ (A + B) *ᵥ x
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : PartialOrder R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : RCLike 𝕜<VAR>A B : Matrix m m R<VAR>hA : A.PosSemidef<VAR>hB : B.PosDef<VAR>x : m → R<VAR>hx : x ≠ 0<GOAL>0 < star x ⬝ᵥ A *ᵥ x + star x ⬝ᵥ B *ᵥ x
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f : E → F<VAR>s : Set E<VAR>x : E<GOAL>HasLineDerivAt 𝕜 f 0 x 0
<VAR>α : Type u_1<VAR>inst✝⁵ : Mul α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝¹ : CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>inst✝ : LocallyFiniteOrderTop α<VAR>a b : α<GOAL>↑(Ici a * Ioi b) ⊆ ↑(Ioi (a * b))
<VAR>a : ℤ<VAR>b : ℕ<VAR>ha2 : a % 2 = 0<VAR>hb2 : b % 2 = 1<GOAL>(if b % 8 = 3 ∨ b % 8 = 5 then -J(a / 2 | b) else J(a / 2 | b)) = J(a | b)
<VAR>b : ℕ<VAR>hb2 : b % 2 = 1<VAR>a : ℤ<VAR>ha2 : 2 * a % 2 = 0<GOAL>(if b % 8 = 3 ∨ b % 8 = 5 then -J(2 * a / 2 | b) else J(2 * a / 2 | b)) = J(2 * a | b)
<VAR>b : ℕ<VAR>hb2 : b % 2 = 1<VAR>a : ℤ<VAR>ha2 : 2 * a % 2 = 0<GOAL>(if b % 8 = 3 ∨ b % 8 = 5 then -J(a | b) else J(a | b)) = (if b % 8 = 1 ∨ b % 8 = 7 then 1 else -1) * J(a | b)
<VAR>b : ℕ<VAR>hb2 : b % 2 = 1<VAR>a : ℤ<VAR>ha2 : 2 * a % 2 = 0<VAR>this : b % 8 < 8<GOAL>(if b % 8 = 3 ∨ b % 8 = 5 then -J(a | b) else J(a | b)) = (if b % 8 = 1 ∨ b % 8 = 7 then 1 else -1) * J(a | b)
<VAR>x : ℂ<GOAL>sin (x - ↑π / 2) = -cos x