ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>inst✝¹⁶ : TopologicalSpace α<VAR>inst✝¹⁵ : AddCommGroup α<VAR>inst✝¹⁴ : TopologicalAddGroup α<VAR>inst✝¹³ : TopologicalSpace β<VAR>inst✝¹² : AddCommGroup β<VAR>inst✝¹¹ : TopologicalAddGroup β<VAR>inst✝¹⁰ : TopologicalSpace γ<VAR>inst✝⁹ : AddCommGroup γ<VAR>inst✝⁸ : TopologicalAddGroup γ<VAR>inst✝⁷ : TopologicalSpace δ<VAR>inst✝⁶ : AddCommGroup δ<VAR>inst✝⁵ : TopologicalAddGroup δ<VAR>inst✝⁴ : UniformSpace G<VAR>inst✝³ : AddCommGroup G<VAR>inst✝² : UniformAddGroup G<VAR>inst✝¹ : T0Space G<VAR>inst✝ : CompleteSpace G<VAR>e : β →+ α<VAR>de : DenseInducing ⇑e<VAR>f : δ →+ γ<VAR>df : DenseInducing ⇑f<VAR>φ : β →+ δ →+ G<VAR>hφ : Continuous fun p => (φ p.1) p.2<VAR>W' : Set G<VAR>W'_nhd : W' ∈ 𝓝 0<VAR>x₀ : α<VAR>y₀ : γ<VAR>ee : β × β → α × α := fun u => (e u.1, e u.2)<VAR>ff : δ × δ → γ × γ := fun u => (f u.1, f u.2)<VAR>lim_φ : Tendsto (fun p => (φ p.1) p.2) (𝓝 (0, 0)) (𝓝 0)<VAR>lim_φ_sub_sub : Tendsto (fun p => (fun p => (φ p.1) p.2) (p.1.2 - p.1.1, p.2.2 - p.2.1)) (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0)<VAR>W : Set G<VAR>W_nhd : W ∈ 𝓝 0<VAR>W4 : ∀ {v w s t : G}, v ∈ W → w ∈ W → s ∈ W → t ∈ W → v + w + s + t ∈ W'<VAR>U₁ : Set β<VAR>U₁_nhd : U₁ ∈ comap (⇑e) (𝓝 x₀)<VAR>V₁ : Set δ<VAR>V₁_nhd : V₁ ∈ comap (⇑f) (𝓝 y₀)<VAR>H : ∀ x ∈ U₁, ∀ x' ∈ U₁, ∀ y ∈ V₁, ∀ y' ∈ V₁, (fun p => (φ p.1) p.2) (x' - x, y' - y) ∈ W<VAR>x₁ : β<VAR>x₁_in : x₁ ∈ U₁<VAR>y₁ : δ<VAR>y₁_in : y₁ ∈ V₁<VAR>cont_flip : Continuous fun p => (φ.flip p.1) p.2<GOAL>∃ U ∈ comap (⇑e) (𝓝 x₀), ∃ V ∈ comap (⇑f) (𝓝 y₀), ∀ x ∈ U, ∀ x' ∈ U, ∀ y ∈ V, ∀ y' ∈ V, (fun p => (φ p.1) p.2) (x', y') - (fun p => (φ p.1) p.2) (x, y) ∈ W'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>inst✝¹⁶ : TopologicalSpace α<VAR>inst✝¹⁵ : AddCommGroup α<VAR>inst✝¹⁴ : TopologicalAddGroup α<VAR>inst✝¹³ : TopologicalSpace β<VAR>inst✝¹² : AddCommGroup β<VAR>inst✝¹¹ : TopologicalAddGroup β<VAR>inst✝¹⁰ : TopologicalSpace γ<VAR>inst✝⁹ : AddCommGroup γ<VAR>inst✝⁸ : TopologicalAddGroup γ<VAR>inst✝⁷ : TopologicalSpace δ<VAR>inst✝⁶ : AddCommGroup δ<VAR>inst✝⁵ : TopologicalAddGroup δ<VAR>inst✝⁴ : UniformSpace G<VAR>inst✝³ : AddCommGroup G<VAR>inst✝² : UniformAddGroup G<VAR>inst✝¹ : T0Space G<VAR>inst✝ : CompleteSpace G<VAR>e : β →+ α<VAR>de : DenseInducing ⇑e<VAR>f : δ →+ γ<VAR>df : DenseInducing ⇑f<VAR>φ : β →+ δ →+ G<VAR>hφ : Continuous fun p => (φ p.1) p.2<VAR>W' : Set G<VAR>W'_nhd : W' ∈ 𝓝 0<VAR>x₀ : α<VAR>y₀ : γ<VAR>ee : β × β → α × α := fun u => (e u.1, e u.2)<VAR>ff : δ × δ → γ × γ := fun u => (f u.1, f u.2)<VAR>lim_φ : Tendsto (fun p => (φ p.1) p.2) (𝓝 (0, 0)) (𝓝 0)<VAR>lim_φ_sub_sub : Tendsto (fun p => (fun p => (φ p.1) p.2) (p.1.2 - p.1.1, p.2.2 - p.2.1)) (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0)<VAR>W : Set G<VAR>W_nhd : W ∈ 𝓝 0<VAR>W4 : ∀ {v w s t : G}, v ∈ W → w ∈ W → s ∈ W → t ∈ W → v + w + s + t ∈ W'<VAR>U₁ : Set β<VAR>U₁_nhd : U₁ ∈ comap (⇑e) (𝓝 x₀)<VAR>V₁ : Set δ<VAR>V₁_nhd : V₁ ∈ comap (⇑f) (𝓝 y₀)<VAR>H : ∀ x ∈ U₁, ∀ x' ∈ U₁, ∀ y ∈ V₁, ∀ y' ∈ V₁, (fun p => (φ p.1) p.2) (x' - x, y' - y) ∈ W<VAR>x₁ : β<VAR>x₁_in : x₁ ∈ U₁<VAR>y₁ : δ<VAR>y₁_in : y₁ ∈ V₁<VAR>cont_flip : Continuous fun p => (φ.flip p.1) p.2<VAR>U₂ : Set β<VAR>U₂_nhd : U₂ ∈ comap (⇑e) (𝓝 x₀)<VAR>HU : ∀ x ∈ U₂, ∀ x' ∈ U₂, (fun p => (φ p.1) p.2) (x' - x, y₁) ∈ W<GOAL>∃ U ∈ comap (⇑e) (𝓝 x₀), ∃ V ∈ comap (⇑f) (𝓝 y₀), ∀ x ∈ U, ∀ x' ∈ U, ∀ y ∈ V, ∀ y' ∈ V, (fun p => (φ p.1) p.2) (x', y') - (fun p => (φ p.1) p.2) (x, y) ∈ W'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>inst✝¹⁶ : TopologicalSpace α<VAR>inst✝¹⁵ : AddCommGroup α<VAR>inst✝¹⁴ : TopologicalAddGroup α<VAR>inst✝¹³ : TopologicalSpace β<VAR>inst✝¹² : AddCommGroup β<VAR>inst✝¹¹ : TopologicalAddGroup β<VAR>inst✝¹⁰ : TopologicalSpace γ<VAR>inst✝⁹ : AddCommGroup γ<VAR>inst✝⁸ : TopologicalAddGroup γ<VAR>inst✝⁷ : TopologicalSpace δ<VAR>inst✝⁶ : AddCommGroup δ<VAR>inst✝⁵ : TopologicalAddGroup δ<VAR>inst✝⁴ : UniformSpace G<VAR>inst✝³ : AddCommGroup G<VAR>inst✝² : UniformAddGroup G<VAR>inst✝¹ : T0Space G<VAR>inst✝ : CompleteSpace G<VAR>e : β →+ α<VAR>de : DenseInducing ⇑e<VAR>f : δ →+ γ<VAR>df : DenseInducing ⇑f<VAR>φ : β →+ δ →+ G<VAR>hφ : Continuous fun p => (φ p.1) p.2<VAR>W' : Set G<VAR>W'_nhd : W' ∈ 𝓝 0<VAR>x₀ : α<VAR>y₀ : γ<VAR>ee : β × β → α × α := fun u => (e u.1, e u.2)<VAR>ff : δ × δ → γ × γ := fun u => (f u.1, f u.2)<VAR>lim_φ : Tendsto (fun p => (φ p.1) p.2) (𝓝 (0, 0)) (𝓝 0)<VAR>lim_φ_sub_sub : Tendsto (fun p => (fun p => (φ p.1) p.2) (p.1.2 - p.1.1, p.2.2 - p.2.1)) (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0)<VAR>W : Set G<VAR>W_nhd : W ∈ 𝓝 0<VAR>W4 : ∀ {v w s t : G}, v ∈ W → w ∈ W → s ∈ W → t ∈ W → v + w + s + t ∈ W'<VAR>U₁ : Set β<VAR>U₁_nhd : U₁ ∈ comap (⇑e) (𝓝 x₀)<VAR>V₁ : Set δ<VAR>V₁_nhd : V₁ ∈ comap (⇑f) (𝓝 y₀)<VAR>H : ∀ x ∈ U₁, ∀ x' ∈ U₁, ∀ y ∈ V₁, ∀ y' ∈ V₁, (fun p => (φ p.1) p.2) (x' - x, y' - y) ∈ W<VAR>x₁ : β<VAR>x₁_in : x₁ ∈ U₁<VAR>y₁ : δ<VAR>y₁_in : y₁ ∈ V₁<VAR>cont_flip : Continuous fun p => (φ.flip p.1) p.2<VAR>U₂ : Set β<VAR>U₂_nhd : U₂ ∈ comap (⇑e) (𝓝 x₀)<VAR>HU : ∀ x ∈ U₂, ∀ x' ∈ U₂, (fun p => (φ p.1) p.2) (x' - x, y₁) ∈ W<VAR>V₂ : Set δ<VAR>V₂_nhd : V₂ ∈ comap (⇑f) (𝓝 y₀)<VAR>HV : ∀ x ∈ V₂, ∀ x' ∈ V₂, (fun p => (φ.flip p.1) p.2) (x' - x, x₁) ∈ W<GOAL>∃ U ∈ comap (⇑e) (𝓝 x₀), ∃ V ∈ comap (⇑f) (𝓝 y₀), ∀ x ∈ U, ∀ x' ∈ U, ∀ y ∈ V, ∀ y' ∈ V, (fun p => (φ p.1) p.2) (x', y') - (fun p => (φ p.1) p.2) (x, y) ∈ W'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>inst✝¹⁶ : TopologicalSpace α<VAR>inst✝¹⁵ : AddCommGroup α<VAR>inst✝¹⁴ : TopologicalAddGroup α<VAR>inst✝¹³ : TopologicalSpace β<VAR>inst✝¹² : AddCommGroup β<VAR>inst✝¹¹ : TopologicalAddGroup β<VAR>inst✝¹⁰ : TopologicalSpace γ<VAR>inst✝⁹ : AddCommGroup γ<VAR>inst✝⁸ : TopologicalAddGroup γ<VAR>inst✝⁷ : TopologicalSpace δ<VAR>inst✝⁶ : AddCommGroup δ<VAR>inst✝⁵ : TopologicalAddGroup δ<VAR>inst✝⁴ : UniformSpace G<VAR>inst✝³ : AddCommGroup G<VAR>inst✝² : UniformAddGroup G<VAR>inst✝¹ : T0Space G<VAR>inst✝ : CompleteSpace G<VAR>e : β →+ α<VAR>de : DenseInducing ⇑e<VAR>f : δ →+ γ<VAR>df : DenseInducing ⇑f<VAR>φ : β →+ δ →+ G<VAR>hφ : Continuous fun p => (φ p.1) p.2<VAR>W' : Set G<VAR>W'_nhd : W' ∈ 𝓝 0<VAR>x₀ : α<VAR>y₀ : γ<VAR>ee : β × β → α × α := fun u => (e u.1, e u.2)<VAR>ff : δ × δ → γ × γ := fun u => (f u.1, f u.2)<VAR>lim_φ : Tendsto (fun p => (φ p.1) p.2) (𝓝 (0, 0)) (𝓝 0)<VAR>lim_φ_sub_sub : Tendsto (fun p => (fun p => (φ p.1) p.2) (p.1.2 - p.1.1, p.2.2 - p.2.1)) (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0)<VAR>W : Set G<VAR>W_nhd : W ∈ 𝓝 0<VAR>W4 : ∀ {v w s t : G}, v ∈ W → w ∈ W → s ∈ W → t ∈ W → v + w + s + t ∈ W'<VAR>U₁ : Set β<VAR>U₁_nhd : U₁ ∈ comap (⇑e) (𝓝 x₀)<VAR>V₁ : Set δ<VAR>V₁_nhd : V₁ ∈ comap (⇑f) (𝓝 y₀)<VAR>H : ∀ x ∈ U₁, ∀ x' ∈ U₁, ∀ y ∈ V₁, ∀ y' ∈ V₁, (fun p => (φ p.1) p.2) (x' - x, y' - y) ∈ W<VAR>x₁ : β<VAR>x₁_in : x₁ ∈ U₁<VAR>y₁ : δ<VAR>y₁_in : y₁ ∈ V₁<VAR>cont_flip : Continuous fun p => (φ.flip p.1) p.2<VAR>U₂ : Set β<VAR>U₂_nhd : U₂ ∈ comap (⇑e) (𝓝 x₀)<VAR>HU : ∀ x ∈ U₂, ∀ x' ∈ U₂, (fun p => (φ p.1) p.2) (x' - x, y₁) ∈ W<VAR>V₂ : Set δ<VAR>V₂_nhd : V₂ ∈ comap (⇑f) (𝓝 y₀)<VAR>HV : ∀ x ∈ V₂, ∀ x' ∈ V₂, (fun p => (φ.flip p.1) p.2) (x' - x, x₁) ∈ W<GOAL>∀ x ∈ U₁ ∩ U₂, ∀ x' ∈ U₁ ∩ U₂, ∀ y ∈ V₁ ∩ V₂, ∀ y' ∈ V₁ ∩ V₂, (fun p => (φ p.1) p.2) (x', y') - (fun p => (φ p.1) p.2) (x, y) ∈ W'
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝⁷ : NonAssocSemiring α<VAR>inst✝⁶ : Preorder α<VAR>inst✝⁵ : NonAssocSemiring β<VAR>inst✝⁴ : Preorder β<VAR>inst✝³ : NonAssocSemiring γ<VAR>inst✝² : Preorder γ<VAR>inst✝¹ : NonAssocSemiring δ<VAR>inst✝ : Preorder δ<VAR>f : β →+*o γ<VAR>g₁ g₂ : α →+*o β<VAR>hf : Injective ⇑f<VAR>h : f.comp g₁ = f.comp g₂<VAR>a : α<GOAL>f (g₁ a) = f (g₂ a)
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁶ : Fintype l<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Unique ι<VAR>inst✝² : NontriviallyNormedField α<VAR>inst✝¹ : NormedAlgebra ℝ α<VAR>inst✝ : DecidableEq n<VAR>f : (n → α) →L[α] m → α<GOAL>‖LinearMap.toMatrix' ↑f‖₊ = ‖f‖₊
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁶ : Fintype l<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Unique ι<VAR>inst✝² : NontriviallyNormedField α<VAR>inst✝¹ : NormedAlgebra ℝ α<VAR>inst✝ : DecidableEq n<VAR>f : (n → α) →L[α] m → α<GOAL>‖{ toLinearMap := (LinearMap.toMatrix' ↑f).mulVecLin, cont := ⋯ }‖₊ = ‖f‖₊
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>a b : R<VAR>h : a % b = 0<GOAL>b ∣ a
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>a b : R<VAR>h : a % b = 0<GOAL>b ∣ b * (a / b)
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>a b : R<VAR>x✝ : b ∣ a<VAR>c : R<VAR>e : a = b * c<GOAL>a % b = 0
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>a b : R<VAR>x✝ : b ∣ a<VAR>c : R<VAR>e : a = b * c<GOAL>b * c = b * (b * c / b)
<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 : V<VAR>p : G.Walk u v<VAR>h : p.support.Nodup<GOAL>p.darts.Nodup
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype o<VAR>inst✝¹ : LinearOrderedField R<VAR>inst✝ : Finite m<VAR>A : Matrix m n R<GOAL>A.rank = finrank R ↥(Submodule.span R (Set.range A))
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype o<VAR>inst✝¹ : LinearOrderedField R<VAR>inst✝ : Finite m<VAR>A : Matrix m n R<VAR>val✝ : Fintype m<GOAL>A.rank = finrank R ↥(Submodule.span R (Set.range A))
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>ha : Polynomial.eval a F = 0<VAR>z' : ℤ_[p]<VAR>hz' : Polynomial.eval z' F = 0<VAR>hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖<VAR>h : ℤ_[p] := z' - a<VAR>q : ℤ_[p]<VAR>hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (Polynomial.derivative F) * h + q * h ^ 2<GOAL>0 = Polynomial.eval (a + (z' - a)) F
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>ha : Polynomial.eval a F = 0<VAR>z' : ℤ_[p]<VAR>hz' : Polynomial.eval z' F = 0<VAR>hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖<VAR>h : ℤ_[p] := z' - a<VAR>q : ℤ_[p]<VAR>hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (Polynomial.derivative F) * h + q * h ^ 2<GOAL>0 = Polynomial.eval (z' - a + a) F
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>ha : Polynomial.eval a F = 0<VAR>z' : ℤ_[p]<VAR>hz' : Polynomial.eval z' F = 0<VAR>hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖<VAR>h : ℤ_[p] := z' - a<VAR>q : ℤ_[p]<VAR>hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (Polynomial.derivative F) * h + q * h ^ 2<GOAL>Polynomial.eval (a + h) F = Polynomial.eval a (Polynomial.derivative F) * h + q * h ^ 2
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>ha : Polynomial.eval a F = 0<VAR>z' : ℤ_[p]<VAR>hz' : Polynomial.eval z' F = 0<VAR>hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖<VAR>h : ℤ_[p] := z' - a<VAR>q : ℤ_[p]<VAR>hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (Polynomial.derivative F) * h + q * h ^ 2<GOAL>Polynomial.eval a (Polynomial.derivative F) * h + q * h ^ 2 = (Polynomial.eval a (Polynomial.derivative F) + q * h) * h
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>ha : Polynomial.eval a F = 0<VAR>z' : ℤ_[p]<VAR>hz' : Polynomial.eval z' F = 0<VAR>hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖<VAR>h : ℤ_[p] := z' - a<VAR>q : ℤ_[p]<VAR>hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (Polynomial.derivative F) * h + q * h ^ 2<VAR>this✝ : (Polynomial.eval a (Polynomial.derivative F) + q * h) * h = 0<VAR>hne : ¬h = 0<VAR>this : Polynomial.eval a (Polynomial.derivative F) + q * h = 0<GOAL>Polynomial.eval a (Polynomial.derivative F) = -q * h
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>ha : Polynomial.eval a F = 0<VAR>z' : ℤ_[p]<VAR>hz' : Polynomial.eval z' F = 0<VAR>hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖<VAR>h : ℤ_[p] := z' - a<VAR>q : ℤ_[p]<VAR>hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (Polynomial.derivative F) * h + q * h ^ 2<VAR>this✝¹ : (Polynomial.eval a (Polynomial.derivative F) + q * h) * h = 0<VAR>hne : ¬h = 0<VAR>this✝ : Polynomial.eval a (Polynomial.derivative F) + q * h = 0<VAR>this : Polynomial.eval a (Polynomial.derivative F) = -q * h<GOAL>‖q‖ ≤ 1
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q p : R[X]<VAR>ha : a ≠ 0<GOAL>(C a * p).roots = p.roots
<VAR>θ : ℝ<GOAL>cos θ ≠ 0 → (tan θ = 0 ↔ ∃ k, ↑k * π = θ)
<VAR>n : ℕ<VAR>n_large : 512 ≤ n<GOAL>∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n
<VAR>n : ℕ<VAR>n_large : 512 ≤ n<VAR>no_prime : ¬∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n<GOAL>False
<VAR>n : ℕ<VAR>n_large : 512 ≤ n<VAR>no_prime : ¬∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n<VAR>H1 : n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n<GOAL>False
<VAR>n : ℕ<VAR>n_large : 512 ≤ n<VAR>no_prime : ¬∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n<VAR>H1 : n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n<VAR>H2 : 4 ^ n < n * n.centralBinom<GOAL>False
<VAR>n : ℕ<VAR>n_large : 512 ≤ n<VAR>no_prime : ¬∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n<VAR>H1 : n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n<VAR>H2 : 4 ^ n < n * n.centralBinom<VAR>H3 : n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)<GOAL>False
<VAR>n : ℕ<VAR>n_large : 512 ≤ n<VAR>no_prime : ¬∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n<VAR>H1 : n * ((2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)) ≤ 4 ^ n<VAR>H2 : 4 ^ n < n * n.centralBinom<VAR>H3 : n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)<GOAL>False
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<GOAL>LiftPPreservation ↔ IsUniform
<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>inst✝¹ : PartialOrder α<VAR>inst✝ : OrderTop α<GOAL>atTop = pure ⊤
<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>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x₀ : E<VAR>hf : HasFDerivAt f f' x₀<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖<GOAL>‖f'‖ ≤ C
<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>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x₀ : E<VAR>hf : HasFDerivAt f f' x₀<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖<VAR>ε : ℝ<VAR>ε0 : 0 < ε<GOAL>0 ≤ C + ε
<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>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x₀ : E<VAR>hf : HasFDerivAt f f' x₀<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖<VAR>ε : ℝ<VAR>ε0 : 0 < ε<GOAL>∀ᶠ (x : E) in 𝓝 0, ‖f' x‖ ≤ (C + ε) * ‖x‖
<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>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x₀ : E<VAR>hf : HasFDerivAt f f' x₀<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>hlip : ∀ᶠ (a : E) in 𝓝 0, ‖f (x₀ + a) - f x₀‖ ≤ C * ‖x₀ + a - x₀‖<VAR>ε : ℝ<VAR>ε0 : 0 < ε<GOAL>∀ᶠ (x : E) in 𝓝 0, ‖f' x‖ ≤ (C + ε) * ‖x‖
<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>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x₀ : E<VAR>hf : HasFDerivAt f f' x₀<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>hlip : ∀ᶠ (a : E) in 𝓝 0, ‖f (x₀ + a) - f x₀‖ ≤ C * ‖x₀ + a - x₀‖<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>y : E<VAR>hy : ‖f (x₀ + y) - f x₀ - f' y‖ ≤ ε * ‖y‖<VAR>hyC : ‖f (x₀ + y) - f x₀‖ ≤ C * ‖x₀ + y - x₀‖<GOAL>‖f' y‖ ≤ (C + ε) * ‖y‖
<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>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x₀ : E<VAR>hf : HasFDerivAt f f' x₀<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>hlip : ∀ᶠ (a : E) in 𝓝 0, ‖f (x₀ + a) - f x₀‖ ≤ C * ‖x₀ + a - x₀‖<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>y : E<VAR>hy : ‖f (x₀ + y) - f x₀ - f' y‖ ≤ ε * ‖y‖<VAR>hyC : ‖f (x₀ + y) - f x₀‖ ≤ C * ‖y‖<GOAL>‖f' y‖ ≤ (C + ε) * ‖y‖
<VAR>x✝ y x : ℝ<VAR>h : x ∈ Ioo (-(π / 2)) (π / 2)<GOAL>sin x ∈ Ioo (-1) 1
<VAR>k : ℕ+<VAR>q : ℕ<VAR>x✝ : ¬(0 = 0 ∧ q + 1 = 0)<GOAL>↑k + ↑k * (q + 1).pred = 0 + ↑k * (q + 1)
<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>f✝ : E × F → G<VAR>f : E →L[𝕜] F →L[𝕜] G<VAR>x : E<VAR>y : F<GOAL>‖f‖ * ‖x‖ * ‖y‖ ≤ max ‖f‖ 1 * ‖x‖ * ‖y‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoidWithZero α<VAR>p x : α<VAR>hx : ¬IsUnit x<GOAL>¬IsUnit (p * x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : SMul 𝕜 E<VAR>inst✝ : SMul 𝕜 F<VAR>s✝ : Set E<VAR>x✝ : E<VAR>ι : Sort u_5<VAR>s : ι → Set E<VAR>hdir : Directed (fun x x_1 => x ⊆ x_1) s<VAR>hc : ∀ ⦃i : ι⦄, Convex 𝕜 (s i)<VAR>x : E<VAR>hx : x ∈ ⋃ i, s i<VAR>y : E<VAR>hy : y ∈ ⋃ i, s i<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a • x + b • y ∈ ⋃ i, s i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : SMul 𝕜 E<VAR>inst✝ : SMul 𝕜 F<VAR>s✝ : Set E<VAR>x✝ : E<VAR>ι : Sort u_5<VAR>s : ι → Set E<VAR>hdir : Directed (fun x x_1 => x ⊆ x_1) s<VAR>hc : ∀ ⦃i : ι⦄, Convex 𝕜 (s i)<VAR>x : E<VAR>hx : ∃ i, x ∈ s i<VAR>y : E<VAR>hy : ∃ i, y ∈ s i<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>∃ i, a • x + b • y ∈ s i
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : LieAlgebra.IsNilpotent R L<VAR>χ₁ χ₂ : L → R<VAR>p q : ℤ<VAR>inst✝² : NoZeroSMulDivisors ℤ R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : IsNoetherian R M<VAR>hχ₁ : χ₁ ≠ 0<GOAL>∃ p < 0, ∃ q > 0, weightSpace M (p • χ₁ + χ₂) = ⊥ ∧ weightSpace M (q • χ₁ + χ₂) = ⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : LieAlgebra.IsNilpotent R L<VAR>χ₁ χ₂ : L → R<VAR>p q✝ : ℤ<VAR>inst✝² : NoZeroSMulDivisors ℤ R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : IsNoetherian R M<VAR>hχ₁ : χ₁ ≠ 0<VAR>q : ℕ<VAR>hq₀ : q > 0<VAR>hq : weightSpace M (q • χ₁ + χ₂) = ⊥<GOAL>∃ p < 0, ∃ q > 0, weightSpace M (p • χ₁ + χ₂) = ⊥ ∧ weightSpace M (q • χ₁ + χ₂) = ⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : LieAlgebra.IsNilpotent R L<VAR>χ₁ χ₂ : L → R<VAR>p✝ q✝ : ℤ<VAR>inst✝² : NoZeroSMulDivisors ℤ R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : IsNoetherian R M<VAR>hχ₁ : χ₁ ≠ 0<VAR>q : ℕ<VAR>hq₀ : q > 0<VAR>hq : weightSpace M (q • χ₁ + χ₂) = ⊥<VAR>p : ℕ<VAR>hp₀ : p > 0<VAR>hp : weightSpace M (p • -χ₁ + χ₂) = ⊥<GOAL>∃ p < 0, ∃ q > 0, weightSpace M (p • χ₁ + χ₂) = ⊥ ∧ weightSpace M (q • χ₁ + χ₂) = ⊥
<VAR>R : Type u_1<VAR>S✝ : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S✝<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S✝ M<VAR>inst✝¹ : SMul S✝ R<VAR>inst✝ : IsScalarTower S✝ R M<VAR>p q S T : Submodule R M<GOAL>∀ {x : M}, x ∈ T → x ∈ S ⊔ T
<VAR>R : Type u_1<VAR>S✝ : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S✝<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S✝ M<VAR>inst✝¹ : SMul S✝ R<VAR>inst✝ : IsScalarTower S✝ R M<VAR>p q S T : Submodule R M<VAR>this : T ≤ S ⊔ T<GOAL>∀ {x : M}, x ∈ T → x ∈ S ⊔ T
<VAR>𝕜 : Type u_1<VAR>S : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁸ : Field 𝕜<VAR>inst✝¹⁷ : CharZero 𝕜<VAR>inst✝¹⁶ : CommRing R<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Algebra 𝕜 R<VAR>inst✝¹³ : Module 𝕜 M<VAR>inst✝¹² : Module R M<VAR>inst✝¹¹ : Module Rᵐᵒᵖ M<VAR>inst✝¹⁰ : IsCentralScalar R M<VAR>inst✝⁹ : IsScalarTower 𝕜 R M<VAR>inst✝⁸ : TopologicalSpace R<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : TopologicalRing R<VAR>inst✝⁵ : TopologicalAddGroup M<VAR>inst✝⁴ : ContinuousSMul R M<VAR>inst✝³ : ContinuousSMul Rᵐᵒᵖ M<VAR>inst✝² : T2Space R<VAR>inst✝¹ : T2Space M<VAR>x : tsze R M<VAR>inst✝ : Invertible x.fst<GOAL>x = x.fst • exp 𝕜 (⅟x.fst • inr x.snd)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<GOAL>M.LinearDisjoint N ↔ (equivOpposite.symm (MulOpposite.op N)).LinearDisjoint (equivOpposite.symm (MulOpposite.op M))