ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : ℝ × ℝ → E<VAR>f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E<VAR>a b : ℝ × ℝ<VAR>hle : a ≤ b<VAR>s : Set (ℝ × ℝ)<VAR>hs : s.Countable<VAR>Hcf : ContinuousOn f (Set.Icc a b)<VAR>Hcg : ContinuousOn g (Set.Icc a b)<VAR>Hdf : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x<VAR>Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x<VAR>Hi : IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) volume<VAR>e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := (ContinuousLinearEquiv.finTwoArrow ℝ ℝ).symm<VAR>this : ∀ (a b : Fin 1 → ℝ) (f : (Fin 1 → ℝ) → E), ∫ (x : Fin 1 → ℝ) in Set.Icc a b, f x = ∫ (x : ℝ) in Set.Icc (a 0) (b 0), f fun x_1 => x<GOAL>∑ i : Fin 2, ((∫ (x : Fin 1 → ℝ) in Set.Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove), ![f, g] i (e.symm (i.insertNth (e b i) x))) - ∫ (x : Fin 1 → ℝ) in Set.Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove), ![f, g] i (e.symm (i.insertNth (e a i) x))) = ((∫ (y : ℝ) in Set.Icc a.2 b.2, f (b.1, y)) - ∫ (y : ℝ) in Set.Icc a.2 b.2, f (a.1, y)) + ((∫ (x : ℝ) in Set.Icc a.1 b.1, g (x, b.2)) - ∫ (x : ℝ) in Set.Icc a.1 b.1, g (x, a.2))
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : ℝ × ℝ → E<VAR>f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E<VAR>a b : ℝ × ℝ<VAR>hle : a ≤ b<VAR>s : Set (ℝ × ℝ)<VAR>hs : s.Countable<VAR>Hcf : ContinuousOn f (Set.Icc a b)<VAR>Hcg : ContinuousOn g (Set.Icc a b)<VAR>Hdf : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x<VAR>Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x<VAR>Hi : IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) volume<VAR>e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := (ContinuousLinearEquiv.finTwoArrow ℝ ℝ).symm<VAR>this : ∀ (a b : Fin 1 → ℝ) (f : (Fin 1 → ℝ) → E), ∫ (x : Fin 1 → ℝ) in Set.Icc a b, f x = ∫ (x : ℝ) in Set.Icc (a 0) (b 0), f fun x_1 => x<GOAL>((∫ (x : ℝ) in Set.Icc ((e a ∘ Fin.succAbove 0) 0) ((e b ∘ Fin.succAbove 0) 0), ![f, g] 0 (e.symm (Fin.insertNth 0 (e b 0) fun x_1 => x))) - ∫ (x : ℝ) in Set.Icc ((e a ∘ Fin.succAbove 0) 0) ((e b ∘ Fin.succAbove 0) 0), ![f, g] 0 (e.symm (Fin.insertNth 0 (e a 0) fun x_1 => x))) + ((∫ (x : ℝ) in Set.Icc ((e a ∘ Fin.succAbove 1) 0) ((e b ∘ Fin.succAbove 1) 0), ![f, g] 1 (e.symm (Fin.insertNth 1 (e b 1) fun x_1 => x))) - ∫ (x : ℝ) in Set.Icc ((e a ∘ Fin.succAbove 1) 0) ((e b ∘ Fin.succAbove 1) 0), ![f, g] 1 (e.symm (Fin.insertNth 1 (e a 1) fun x_1 => x))) = ((∫ (y : ℝ) in Set.Icc a.2 b.2, f (b.1, y)) - ∫ (y : ℝ) in Set.Icc a.2 b.2, f (a.1, y)) + ((∫ (x : ℝ) in Set.Icc a.1 b.1, g (x, b.2)) - ∫ (x : ℝ) in Set.Icc a.1 b.1, g (x, a.2))
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : ℝ × ℝ → E<VAR>f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E<VAR>a b : ℝ × ℝ<VAR>hle : a ≤ b<VAR>s : Set (ℝ × ℝ)<VAR>hs : s.Countable<VAR>Hcf : ContinuousOn f (Set.Icc a b)<VAR>Hcg : ContinuousOn g (Set.Icc a b)<VAR>Hdf : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x<VAR>Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x<VAR>Hi : IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) volume<VAR>e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := (ContinuousLinearEquiv.finTwoArrow ℝ ℝ).symm<GOAL>((∫ (y : ℝ) in Set.Icc a.2 b.2, f (b.1, y)) - ∫ (y : ℝ) in Set.Icc a.2 b.2, f (a.1, y)) + ((∫ (x : ℝ) in Set.Icc a.1 b.1, g (x, b.2)) - ∫ (x : ℝ) in Set.Icc a.1 b.1, g (x, a.2)) = (((∫ (x : ℝ) in a.1 ..b.1, g (x, b.2)) - ∫ (x : ℝ) in a.1 ..b.1, g (x, a.2)) + ∫ (y : ℝ) in a.2 ..b.2, f (b.1, y)) - ∫ (y : ℝ) in a.2 ..b.2, f (a.1, y)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : ℝ × ℝ → E<VAR>f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E<VAR>a b : ℝ × ℝ<VAR>hle : a ≤ b<VAR>s : Set (ℝ × ℝ)<VAR>hs : s.Countable<VAR>Hcf : ContinuousOn f (Set.Icc a b)<VAR>Hcg : ContinuousOn g (Set.Icc a b)<VAR>Hdf : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x<VAR>Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x<VAR>Hi : IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) volume<VAR>e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := (ContinuousLinearEquiv.finTwoArrow ℝ ℝ).symm<GOAL>((∫ (y : ℝ) in Set.Icc a.2 b.2, f (b.1, y)) - ∫ (y : ℝ) in Set.Icc a.2 b.2, f (a.1, y)) + ((∫ (x : ℝ) in Set.Icc a.1 b.1, g (x, b.2)) - ∫ (x : ℝ) in Set.Icc a.1 b.1, g (x, a.2)) = (((∫ (x : ℝ) in Set.Icc a.1 b.1, g (x, b.2)) - ∫ (x : ℝ) in Set.Icc a.1 b.1, g (x, a.2)) + ∫ (y : ℝ) in Set.Icc a.2 b.2, f (b.1, y)) - ∫ (y : ℝ) in Set.Icc a.2 b.2, f (a.1, y)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Nontrivial R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>f : M →ₗ[R] M<GOAL>(aeval f) f.charpoly = 0
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Nontrivial R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>f : M →ₗ[R] M<GOAL>(algEquivMatrix (chooseBasis R M)).toLinearEquiv ((aeval f) f.charpoly) = 0
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Nontrivial R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>f : M →ₗ[R] M<GOAL>(aeval (↑(algEquivMatrix (chooseBasis R M)) f)) ((toMatrix (chooseBasis R M) (chooseBasis R M)) f).charpoly = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g✝ : α → β<VAR>c c₁ c₂ x✝ : α<VAR>inst✝¹ : Add α<VAR>inst✝ : Add γ<VAR>h : Periodic f c<VAR>g : AddHom γ α<VAR>g_inv : α → γ<VAR>hg : RightInverse g_inv ⇑g<VAR>x : γ<GOAL>(f ∘ ⇑g) (x + g_inv c) = (f ∘ ⇑g) x
<VAR>n : ℕ<VAR>A : Type u_1<VAR>R : Type u_2<VAR>inst✝² : AddGroup A<VAR>inst✝¹ : Ring R<VAR>α : Type u_3<VAR>inst✝ : Group α<VAR>a : α<GOAL>Nat.card ↥(zpowers a) = orderOf a
<VAR>n : ℕ<VAR>A : Type u_1<VAR>R : Type u_2<VAR>inst✝² : AddGroup A<VAR>inst✝¹ : Ring R<VAR>α : Type u_3<VAR>inst✝ : Group α<VAR>a : α<VAR>this : Nat.card ↑(MulAction.orbit (↥(zpowers a)) 1) = Nat.card (ZMod (Function.minimalPeriod (fun x => a • x) 1))<GOAL>Nat.card ↥(zpowers a) = orderOf a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : CompleteLattice α<VAR>f g✝ : Filter β<VAR>p q : β → Prop<VAR>u v : β → α<VAR>inst✝ : CompleteLattice γ<VAR>g : sSupHom α γ<GOAL>g (blimsup u f p) ≤ blimsup (⇑g ∘ u) f p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : CompleteLattice α<VAR>f g✝ : Filter β<VAR>p q : β → Prop<VAR>u v : β → α<VAR>inst✝ : CompleteLattice γ<VAR>g : sSupHom α γ<GOAL>g (⨅ s ∈ f, ⨆ b, ⨆ (_ : p b ∧ b ∈ s), u b) ≤ ⨅ s ∈ f, ⨆ b, ⨆ (_ : p b ∧ b ∈ s), g (u b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : CompleteLattice α<VAR>f g✝ : Filter β<VAR>p q : β → Prop<VAR>u v : β → α<VAR>inst✝ : CompleteLattice γ<VAR>g : sSupHom α γ<GOAL>⨅ i ∈ f, g (⨆ b, ⨆ (_ : p b ∧ b ∈ i), u b) ≤ ⨅ s ∈ f, ⨆ b, ⨆ (_ : p b ∧ b ∈ s), g (u b)
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>a : ℝ<GOAL>(Summable fun n => rexp (↑n * a)) ↔ a < 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>x y : E<VAR>s t : Set E<VAR>α : Type u_5<VAR>l : Filter α<VAR>c : α → 𝕜<VAR>d : α → E<VAR>hc : Tendsto (fun n => ‖c n‖) l atTop<VAR>hd : Tendsto (fun n => c n • d n) l (𝓝 y)<GOAL>Tendsto d l (𝓝 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>x y : E<VAR>s t : Set E<VAR>α : Type u_5<VAR>l : Filter α<VAR>c : α → 𝕜<VAR>d : α → E<VAR>hc : Tendsto (fun n => ‖c n‖) l atTop<VAR>hd : Tendsto (fun n => c n • d n) l (𝓝 y)<VAR>A : Tendsto (fun n => ‖c n‖⁻¹) l (𝓝 0)<GOAL>Tendsto d l (𝓝 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>x y : E<VAR>s t : Set E<VAR>α : Type u_5<VAR>l : Filter α<VAR>c : α → 𝕜<VAR>d : α → E<VAR>hc : Tendsto (fun n => ‖c n‖) l atTop<VAR>hd : Tendsto (fun n => c n • d n) l (𝓝 y)<VAR>A : Tendsto (fun n => ‖c n‖⁻¹) l (𝓝 0)<VAR>B : Tendsto (fun n => ‖c n • d n‖) l (𝓝 ‖y‖)<GOAL>Tendsto d l (𝓝 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>x y : E<VAR>s t : Set E<VAR>α : Type u_5<VAR>l : Filter α<VAR>c : α → 𝕜<VAR>d : α → E<VAR>hc : Tendsto (fun n => ‖c n‖) l atTop<VAR>hd : Tendsto (fun n => c n • d n) l (𝓝 y)<VAR>A : Tendsto (fun n => ‖c n‖⁻¹) l (𝓝 0)<VAR>B : Tendsto (fun n => ‖c n • d n‖) l (𝓝 ‖y‖)<VAR>C : Tendsto (fun n => ‖c n‖⁻¹ * ‖c n • d n‖) l (𝓝 (0 * ‖y‖))<GOAL>Tendsto d l (𝓝 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>x y : E<VAR>s t : Set E<VAR>α : Type u_5<VAR>l : Filter α<VAR>c : α → 𝕜<VAR>d : α → E<VAR>hc : Tendsto (fun n => ‖c n‖) l atTop<VAR>hd : Tendsto (fun n => c n • d n) l (𝓝 y)<VAR>A : Tendsto (fun n => ‖c n‖⁻¹) l (𝓝 0)<VAR>B : Tendsto (fun n => ‖c n • d n‖) l (𝓝 ‖y‖)<VAR>C : Tendsto (fun n => ‖c n‖⁻¹ * ‖c n • d n‖) l (𝓝 0)<GOAL>Tendsto d l (𝓝 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>x y : E<VAR>s t : Set E<VAR>α : Type u_5<VAR>l : Filter α<VAR>c : α → 𝕜<VAR>d : α → E<VAR>hc : Tendsto (fun n => ‖c n‖) l atTop<VAR>hd : Tendsto (fun n => c n • d n) l (𝓝 y)<VAR>A : Tendsto (fun n => ‖c n‖⁻¹) l (𝓝 0)<VAR>B : Tendsto (fun n => ‖c n • d n‖) l (𝓝 ‖y‖)<VAR>C : Tendsto (fun n => ‖c n‖⁻¹ * ‖c n • d n‖) l (𝓝 0)<VAR>this : ∀ᶠ (n : α) in l, ‖c n‖⁻¹ * ‖c n • d n‖ = ‖d n‖<GOAL>Tendsto d l (𝓝 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>x y : E<VAR>s t : Set E<VAR>α : Type u_5<VAR>l : Filter α<VAR>c : α → 𝕜<VAR>d : α → E<VAR>hc : Tendsto (fun n => ‖c n‖) l atTop<VAR>hd : Tendsto (fun n => c n • d n) l (𝓝 y)<VAR>A : Tendsto (fun n => ‖c n‖⁻¹) l (𝓝 0)<VAR>B : Tendsto (fun n => ‖c n • d n‖) l (𝓝 ‖y‖)<VAR>C : Tendsto (fun n => ‖c n‖⁻¹ * ‖c n • d n‖) l (𝓝 0)<VAR>this : ∀ᶠ (n : α) in l, ‖c n‖⁻¹ * ‖c n • d n‖ = ‖d n‖<VAR>D : Tendsto (fun n => ‖d n‖) l (𝓝 0)<GOAL>Tendsto d l (𝓝 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>x y : E<VAR>s t : Set E<VAR>α : Type u_5<VAR>l : Filter α<VAR>c : α → 𝕜<VAR>d : α → E<VAR>hc : Tendsto (fun n => ‖c n‖) l atTop<VAR>hd : Tendsto (fun n => c n • d n) l (𝓝 y)<VAR>A : Tendsto (fun n => ‖c n‖⁻¹) l (𝓝 0)<VAR>B : Tendsto (fun n => ‖c n • d n‖) l (𝓝 ‖y‖)<VAR>C : Tendsto (fun n => ‖c n‖⁻¹ * ‖c n • d n‖) l (𝓝 0)<VAR>this : ∀ᶠ (n : α) in l, ‖c n‖⁻¹ * ‖c n • d n‖ = ‖d n‖<VAR>D : Tendsto (fun n => ‖d n‖) l (𝓝 0)<GOAL>Tendsto (fun x => ‖d x‖) l (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝ : DivisionSemiring α<VAR>a✝ b✝ c d a b : α<VAR>hc : c ≠ 0<GOAL>(a + b / c) * c = a * c + b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>s t : Set α<VAR>a b : α<VAR>p : Prop<VAR>f : p → α<VAR>hp : ¬p<GOAL>(range fun h => f h) = ∅
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p : R[X]<GOAL>p.nextCoeff = 0 ↔ p.natDegree = 0 ∨ 0 < p.natDegree ∧ p.coeff (p.natDegree - 1) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p : R[X]<GOAL>¬p.natDegree = 0 → p.coeff (p.natDegree - 1) = 0 ↔ ¬p.natDegree = 0 → ¬p.natDegree = 0 ∧ p.coeff (p.natDegree - 1) = 0
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>α : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝⁴ : FunLike F M N<VAR>inst✝³ : FunLike G N M<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Monoid N<VAR>inst✝ : MonoidHomClass F M N<VAR>f : F<VAR>y : Mˣ<GOAL>IsUnit (f ↑y)
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>γ : α → Type u_2<VAR>δ : α → Type u_3<VAR>s : (a : α) → Finset (γ a)<VAR>t : (a : α) → Finset (δ a)<VAR>a : α<VAR>inst✝ : DecidableEq (δ a)<VAR>ht : ∀ (b : α), a ≠ b → (t b).Nonempty<GOAL>image (fun f => f a) (piFinset t) = t a
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>γ : α → Type u_2<VAR>δ : α → Type u_3<VAR>s : (a : α) → Finset (γ a)<VAR>t : (a : α) → Finset (δ a)<VAR>a : α<VAR>inst✝ : DecidableEq (δ a)<VAR>ht : ∀ (b : α), a ≠ b → (t b).Nonempty<VAR>x : δ a<VAR>h : x ∈ t a<GOAL>∃ a_1 ∈ piFinset t, a_1 a = x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f✝ : α → β<VAR>s t : Set α<VAR>a : α<VAR>inst✝ : IsRefl α r<VAR>hs : s.Finite<VAR>f : ℕ → α<VAR>hf : ∀ (n : ℕ), f n ∈ s<GOAL>∃ m n, m < n ∧ r (f m) (f n)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f✝ : α → β<VAR>s t : Set α<VAR>a : α<VAR>inst✝ : IsRefl α r<VAR>hs : s.Finite<VAR>f : ℕ → α<VAR>hf : ∀ (n : ℕ), f n ∈ s<VAR>m n : ℕ<VAR>hmn : m < n<VAR>h : f m = f n<GOAL>∃ m n, m < n ∧ r (f m) (f n)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x y : F<GOAL>⟪x + y, x + y⟫_𝕜 = ⟪x, x⟫_𝕜 + ⟪x, y⟫_𝕜 + ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x y : F<GOAL>⟪x, x⟫_𝕜 + ⟪y, x⟫_𝕜 + (⟪x, y⟫_𝕜 + ⟪y, y⟫_𝕜) = ⟪x, x⟫_𝕜 + ⟪x, y⟫_𝕜 + ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p : K[X]<GOAL>((algebraMap K[X] (RatFunc K)) p).intDegree = ↑p.natDegree
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>1 ≤ a / b ↔ b ≤ a
<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>ι : Type u_6<VAR>𝔸 : Type u_7<VAR>𝔸' : Type u_8<VAR>inst✝⁴ : NormedRing 𝔸<VAR>inst✝³ : NormedCommRing 𝔸'<VAR>inst✝² : NormedAlgebra 𝕜 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>f : ι → E → 𝔸<VAR>f' : ι → E →L[𝕜] 𝔸<VAR>g : ι → E → 𝔸'<VAR>g' : ι → E →L[𝕜] 𝔸'<VAR>inst✝ : Fintype ι<VAR>l : List ι<VAR>x : ι → 𝔸<GOAL>HasStrictFDerivAt (fun x => (List.map x l).prod) (∑ i : Fin l.length, (List.map x (List.take (↑i) l)).prod • (proj (l.get i)).smulRight (List.map x (List.drop (↑i).succ l)).prod) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>hf : IsOpenMap f<VAR>finv : β → α<VAR>hleft : LeftInverse finv f<GOAL>ContinuousOn finv (range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>hf : IsOpenMap f<VAR>finv : β → α<VAR>hleft : LeftInverse finv f<GOAL>ContinuousOn finv (f '' univ)
<VAR>xl xr : Type u<VAR>x y : PGame<GOAL>-y < x ↔ -x < y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>f : ArithmeticFunction M<VAR>x : ℕ<GOAL>(↑ζ • f) x = ∑ i ∈ x.divisors, f i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>f : ArithmeticFunction M<VAR>x : ℕ<GOAL>∑ x ∈ x.divisorsAntidiagonal, ↑ζ x.1 • f x.2 = ∑ i ∈ x.divisors, f i
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R✝ I J X Y R : Set α<VAR>hR : R ⊆ M.E<VAR>hI : (M ↾ R).Basis I X<GOAL>M.Basis I X
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : IsCofiltered C<VAR>O : Finset C<VAR>H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))<VAR>J : Type w<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : FinCategory J<VAR>F : J ⥤ C<GOAL>Nonempty (Cone F)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ∠ p₁ p₂ p₃ = π / 2<VAR>h0 : p₁ = p₂ ∨ p₃ ≠ p₂<GOAL>Real.tan (∠ p₂ p₃ p₁) * dist p₃ p₂ = dist p₁ p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫_ℝ = 0<VAR>h0 : p₁ = p₂ ∨ p₃ ≠ p₂<GOAL>Real.tan (∠ p₂ p₃ p₁) * dist p₃ p₂ = dist p₁ p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫_ℝ = 0<VAR>h0 : p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ = 0<GOAL>Real.tan (∠ p₂ p₃ p₁) * dist p₃ p₂ = dist p₁ p₂
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝¹³ : CommRing A<VAR>inst✝¹² : CommRing B<VAR>inst✝¹¹ : Algebra A B<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : Algebra A K<VAR>inst✝⁷ : IsFractionRing A K<VAR>inst✝⁶ : Algebra B L<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : Algebra A L<VAR>inst✝³ : IsScalarTower A B L<VAR>inst✝² : IsScalarTower A K L<VAR>inst✝¹ : IsIntegralClosure B A L<VAR>inst✝ : FiniteDimensional K L<VAR>σ : L →ₐ[K] L<VAR>x : B<GOAL>(algebraMap B L) (((galRestrictHom A K L B) σ) x) = σ ((algebraMap B L) x)
<VAR>M : Type u_1<VAR>inst✝ : OrderedAddCommMonoid M<VAR>f : ℕ → M<VAR>u : ℕ → ℕ<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>hu : Monotone u<VAR>n : ℕ<GOAL>∑ k ∈ range (u n), f k ≤ ∑ k ∈ range (u 0), f k + ∑ k ∈ range n, (u (k + 1) - u k) • f (u k)
<VAR>M : Type u_1<VAR>inst✝ : OrderedAddCommMonoid M<VAR>f : ℕ → M<VAR>u : ℕ → ℕ<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>hu : Monotone u<VAR>n : ℕ<GOAL>∑ k ∈ range (u n), f k = ∑ k ∈ range (u 0), f k + ∑ k ∈ Ico (u 0) (u n), f k
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<GOAL>LeftInverse ⇑trunc ⇑toLaurent
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<GOAL>∀ (p q : R[X]), trunc (toLaurent p) = p → trunc (toLaurent q) = q → trunc (toLaurent (p + q)) = p + q
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<GOAL>∀ (n : ℕ) (a : R), trunc (toLaurent ((monomial n) a)) = (monomial n) a
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X : C<VAR>inst✝¹ : HasTerminal C<VAR>inst✝ : PreservesLimit (Functor.empty C) G<VAR>F : Discrete PEmpty.{1} ⥤ D<GOAL>HasLimit F
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X : C<VAR>inst✝¹ : HasTerminal C<VAR>inst✝ : PreservesLimit (Functor.empty C) G<VAR>F : Discrete PEmpty.{1} ⥤ D<VAR>this : HasLimit (Functor.empty D)<GOAL>HasLimit F
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I✝ : Ideal R<VAR>F F' : I✝.Filtration M<VAR>I : Ideal R<VAR>N : Submodule R M<GOAL>(I.stableFiltration N).Stable
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I✝ : Ideal R<VAR>F F' : I✝.Filtration M<VAR>I : Ideal R<VAR>N : Submodule R M<GOAL>∀ n ≥ 0, I • (I.stableFiltration N).N n = (I.stableFiltration N).N (n + 1)
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I✝ : Ideal R<VAR>F F' : I✝.Filtration M<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>n : ℕ<VAR>a✝ : n ≥ 0<GOAL>I • I ^ n • N = I ^ (n + 1) • N
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f✝ : R[X]<VAR>N : ℕ<VAR>f : R[X]<GOAL>reflect N f = 0 ↔ f = 0
<VAR>R : Type u<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n : ℕ<VAR>toFinsupp✝ : R[ℕ]<GOAL>((monomial n) ({ toFinsupp := toFinsupp✝ }.coeff n) + erase n { toFinsupp := toFinsupp✝ }).toFinsupp = { toFinsupp := toFinsupp✝ }.toFinsupp
<VAR>R : Type u<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n : ℕ<VAR>toFinsupp✝ : R[ℕ]<GOAL>Finsupp.single n ((match (motive := R[X] → ℕ → R) { toFinsupp := toFinsupp✝ } with | { toFinsupp := p } => ⇑p) n) + Finsupp.erase n { toFinsupp := toFinsupp✝ }.toFinsupp = { toFinsupp := toFinsupp✝ }.toFinsupp
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a p : α<VAR>ha0 : a ≠ 0<VAR>hp : Irreducible p<VAR>hd : p ∣ a<GOAL>⟨Associates.mk p, ⋯⟩ ∈ factors' a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a p : α<VAR>ha0 : a ≠ 0<VAR>hp : Irreducible p<VAR>hd : p ∣ a<VAR>q : α<VAR>hq : q ∈ UniqueFactorizationMonoid.factors a<VAR>hpq : p ~ᵤ q<GOAL>⟨Associates.mk p, ⋯⟩ ∈ factors' a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a p : α<VAR>ha0 : a ≠ 0<VAR>hp : Irreducible p<VAR>hd : p ∣ a<VAR>q : α<VAR>hq : q ∈ UniqueFactorizationMonoid.factors a<VAR>hpq : p ~ᵤ q<GOAL>∃ a_1, ∃ (h : a_1 ∈ UniqueFactorizationMonoid.factors a), ⟨Associates.mk a_1, ⋯⟩ = ⟨Associates.mk p, ⋯⟩
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a p : α<VAR>ha0 : a ≠ 0<VAR>hp : Irreducible p<VAR>hd : p ∣ a<VAR>q : α<VAR>hq : q ∈ UniqueFactorizationMonoid.factors a<VAR>hpq : p ~ᵤ q<GOAL>∃ (h : q ∈ UniqueFactorizationMonoid.factors a), ⟨Associates.mk q, ⋯⟩ = ⟨Associates.mk p, ⋯⟩
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a p : α<VAR>ha0 : a ≠ 0<VAR>hp : Irreducible p<VAR>hd : p ∣ a<VAR>q : α<VAR>hq : q ∈ UniqueFactorizationMonoid.factors a<VAR>hpq : p ~ᵤ q<GOAL>⟨Associates.mk q, ⋯⟩ = ⟨Associates.mk p, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace α<VAR>inst✝ : PolishSpace α<VAR>s : ℕ → Set α<VAR>m : ℕ → TopologicalSpace α<VAR>mt : ∀ (n : ℕ), m n ≤ t<VAR>m_polish : ∀ (n : ℕ), PolishSpace α<VAR>h✝ : ∀ (n : ℕ), IsClosed (s n)<VAR>m_open : ∀ (n : ℕ), IsOpen (s n)<GOAL>IsClopenable (⋃ n, s n)