ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>Q : Type uQ<VAR>P' : Type uP'<VAR>Q' : Type uQ'<VAR>inst✝³¹ : CommSemiring R<VAR>inst✝³⁰ : Semiring A<VAR>inst✝²⁹ : Semiring B<VAR>inst✝²⁸ : Algebra R A<VAR>inst✝²⁷ : Algebra R B<VAR>inst✝²⁶ : AddCommMonoid M<VAR>inst✝²⁵ : Module R M<VAR>inst✝²⁴ : Module A M<VAR>inst✝²³ : Module B M<VAR>inst✝²² : IsScalarTower R A M<VAR>inst✝²¹ : IsScalarTower R B M<VAR>inst✝²⁰ : SMulCommClass A B M<VAR>inst✝¹⁹ : AddCommMonoid N<VAR>inst✝¹⁸ : Module R N<VAR>inst✝¹⁷ : AddCommMonoid P<VAR>inst✝¹⁶ : Module R P<VAR>inst✝¹⁵ : Module A P<VAR>inst✝¹⁴ : Module B P<VAR>inst✝¹³ : IsScalarTower R A P<VAR>inst✝¹² : IsScalarTower R B P<VAR>inst✝¹¹ : SMulCommClass A B P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : Module R Q<VAR>inst✝⁸ : AddCommMonoid P'<VAR>inst✝⁷ : Module R P'<VAR>inst✝⁶ : Module A P'<VAR>inst✝⁵ : Module B P'<VAR>inst✝⁴ : IsScalarTower R A P'<VAR>inst✝³ : IsScalarTower R B P'<VAR>inst✝² : SMulCommClass A B P'<VAR>inst✝¹ : AddCommMonoid Q'<VAR>inst✝ : Module R Q'<VAR>r : R<VAR>f : M →ₗ[A] P<VAR>g : N →ₗ[R] Q<VAR>x✝¹ : M<VAR>x✝ : N<GOAL>((curry (map f (r • g))) x✝¹) x✝ = ((curry (r • map f g)) x✝¹) x✝
<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.CliqueFree (r + 1) ∧ ∀ (H : SimpleGraph V) [inst : DecidableRel H.Adj], H.CliqueFree (r + 1) → H.edgeFinset.card ≤ G.edgeFinset.card<VAR>hn : ¬G.Adj s t<GOAL>G.degree s = G.degree t
<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>hn : ¬G.Adj s t<VAR>h : G.degree s ≠ G.degree t<GOAL>G.CliqueFree (r + 1) → ∃ 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>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>s t : V<VAR>hn : ¬G.Adj s t<VAR>h : G.degree s ≠ G.degree t<VAR>cf : G.CliqueFree (r + 1)<VAR>hd : G.degree t < G.degree s<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>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>s t : V<VAR>hn : ¬G.Adj s t<VAR>h : G.degree s ≠ G.degree t<VAR>cf : G.CliqueFree (r + 1)<VAR>hd : G.degree t < G.degree s<GOAL>G.edgeFinset.card < (G.replaceVertex s t).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>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>s t : V<VAR>hn : ¬G.Adj s t<VAR>h : G.degree s ≠ G.degree t<VAR>cf : G.CliqueFree (r + 1)<VAR>hd : G.degree t < G.degree s<VAR>this : (G.replaceVertex s t).edgeFinset.card = G.edgeFinset.card + G.degree s - G.degree t<GOAL>G.edgeFinset.card < (G.replaceVertex s t).edgeFinset.card
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>k : Type u_2<VAR>inst✝¹ : Field k<VAR>inst✝ : Algebra k K<VAR>φ : K →+* ℂ<VAR>σ : K ≃ₐ[k] K<VAR>h : IsConj φ σ<VAR>x : k<GOAL>(star (φ.comp (algebraMap k K))) x = (φ.comp (algebraMap k K)) x
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : Epi f<VAR>Z : D<VAR>g h : F.obj Y ⟶ Z<VAR>H : (adj.homEquiv X Z) (F.map f ≫ g) = (adj.homEquiv X Z) (F.map f ≫ h)<GOAL>g = h
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : MeasurableSpace Ω'<VAR>inst✝³ : TopologicalSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω'<VAR>inst✝ : BorelSpace Ω'<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>νs : ι → ProbabilityMeasure Ω<VAR>ν : ProbabilityMeasure Ω<VAR>lim : Tendsto νs L (𝓝 ν)<VAR>f : Ω → Ω'<VAR>f_cont : Continuous f<GOAL>Tendsto (fun i => (νs i).map ⋯) L (𝓝 (ν.map ⋯))
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : MeasurableSpace Ω'<VAR>inst✝³ : TopologicalSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω'<VAR>inst✝ : BorelSpace Ω'<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>νs : ι → ProbabilityMeasure Ω<VAR>ν : ProbabilityMeasure Ω<VAR>lim : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ∫⁻ (ω : Ω), ↑(f ω) ∂↑(νs i)) L (𝓝 (∫⁻ (ω : Ω), ↑(f ω) ∂↑ν))<VAR>f : Ω → Ω'<VAR>f_cont : Continuous f<GOAL>∀ (f_1 : Ω' →ᵇ ℝ≥0), Tendsto (fun i => ∫⁻ (ω : Ω'), ↑(f_1 ω) ∂↑((νs i).map ⋯)) L (𝓝 (∫⁻ (ω : Ω'), ↑(f_1 ω) ∂↑(ν.map ⋯)))
<VAR>α : Sort u_1<VAR>n : Nat<VAR>f : α → Fin n → α<VAR>x : α<GOAL>foldl.loop n f x n = x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<GOAL>ContDiff 𝕜 n f ↔ ∀ (x : E), ContDiffAt 𝕜 n f x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>y : M<GOAL>x ∈ span R (insert y s) ↔ ∃ a, ∃ z ∈ span R s, x = a • y + z
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R M<VAR>N O : Submodule R M<VAR>hNO : N ≤ O<VAR>ϕ : ↥O →ₗ[R] R<VAR>inst✝ : (ϕ.submoduleImage N).IsPrincipal<VAR>x : M<VAR>hx : x ∈ N<GOAL>generator (ϕ.submoduleImage N) ∣ ϕ ⟨x, ⋯⟩
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R M<VAR>N O : Submodule R M<VAR>hNO : N ≤ O<VAR>ϕ : ↥O →ₗ[R] R<VAR>inst✝ : (ϕ.submoduleImage N).IsPrincipal<VAR>x : M<VAR>hx : x ∈ N<GOAL>∃ y, ∃ (yN : y ∈ N), ϕ ⟨y, ⋯⟩ = ϕ ⟨x, ⋯⟩
<VAR>T : Type u<VAR>inst✝² : Category.{v, u} T<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X✝ Y✝ : Arrow C<VAR>f : X✝ ⟶ Y✝<GOAL>(𝟭 D).map (F.map f.left) ≫ ((fun a => { left := F.obj a.left, right := F.obj a.right, hom := F.map a.hom }) Y✝).hom = ((fun a => { left := F.obj a.left, right := F.obj a.right, hom := F.map a.hom }) X✝).hom ≫ (𝟭 D).map (F.map f.right)
<VAR>T : Type u<VAR>inst✝² : Category.{v, u} T<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X✝ Y✝ : Arrow C<VAR>f : X✝ ⟶ Y✝<VAR>w : (𝟭 C).map f.left ≫ Y✝.hom = X✝.hom ≫ (𝟭 C).map f.right := f.w<GOAL>(𝟭 D).map (F.map f.left) ≫ ((fun a => { left := F.obj a.left, right := F.obj a.right, hom := F.map a.hom }) Y✝).hom = ((fun a => { left := F.obj a.left, right := F.obj a.right, hom := F.map a.hom }) X✝).hom ≫ (𝟭 D).map (F.map f.right)
<VAR>T : Type u<VAR>inst✝² : Category.{v, u} T<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X✝ Y✝ : Arrow C<VAR>f : X✝ ⟶ Y✝<VAR>w : f.left ≫ Y✝.hom = X✝.hom ≫ f.right := f.w<GOAL>(𝟭 D).map (F.map f.left) ≫ ((fun a => { left := F.obj a.left, right := F.obj a.right, hom := F.map a.hom }) Y✝).hom = ((fun a => { left := F.obj a.left, right := F.obj a.right, hom := F.map a.hom }) X✝).hom ≫ (𝟭 D).map (F.map f.right)
<VAR>T : Type u<VAR>inst✝² : Category.{v, u} T<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X✝ Y✝ : Arrow C<VAR>f : X✝ ⟶ Y✝<VAR>w : f.left ≫ Y✝.hom = X✝.hom ≫ f.right := f.w<GOAL>F.map f.left ≫ F.map Y✝.hom = F.map X✝.hom ≫ F.map f.right
<VAR>α : Type u<VAR>inst✝¹ : DecidableEq α<VAR>β : Type v<VAR>inst✝ : Fintype α<VAR>s : Perm α →* ℤˣ<VAR>hs : Surjective ⇑s<VAR>f : Perm α<VAR>x✝ : f.IsSwap<VAR>x y : α<VAR>hxy : x ≠ y<VAR>hxy' : f = swap x y<VAR>h : ¬s (swap x y) = -1<GOAL>False
<VAR>α : Type u<VAR>inst✝¹ : DecidableEq α<VAR>β : Type v<VAR>inst✝ : Fintype α<VAR>s : Perm α →* ℤˣ<VAR>hs : Surjective ⇑s<VAR>f : Perm α<VAR>x✝ : f.IsSwap<VAR>x y : α<VAR>hxy : x ≠ y<VAR>hxy' : f = swap x y<VAR>h : ¬s (swap x y) = -1<VAR>this : ∀ (f : Perm α), f.IsSwap → s f = 1<GOAL>False
<VAR>α : Type u<VAR>inst✝¹ : DecidableEq α<VAR>β : Type v<VAR>inst✝ : Fintype α<VAR>s : Perm α →* ℤˣ<VAR>hs : Surjective ⇑s<VAR>f : Perm α<VAR>x✝ : f.IsSwap<VAR>x y : α<VAR>hxy : x ≠ y<VAR>hxy' : f = swap x y<VAR>h : ¬s (swap x y) = -1<VAR>this : ∀ (f : Perm α), f.IsSwap → s f = 1<VAR>g : Perm α<VAR>hg : s g = -1<VAR>l : List (Perm α)<VAR>hl : l.prod = g ∧ ∀ g ∈ l, g.IsSwap<GOAL>False
<VAR>α : Type u<VAR>inst✝¹ : DecidableEq α<VAR>β : Type v<VAR>inst✝ : Fintype α<VAR>s : Perm α →* ℤˣ<VAR>hs : Surjective ⇑s<VAR>f : Perm α<VAR>x✝ : f.IsSwap<VAR>x y : α<VAR>hxy : x ≠ y<VAR>hxy' : f = swap x y<VAR>h : ¬s (swap x y) = -1<VAR>this✝ : ∀ (f : Perm α), f.IsSwap → s f = 1<VAR>g : Perm α<VAR>hg : s g = -1<VAR>l : List (Perm α)<VAR>hl : l.prod = g ∧ ∀ g ∈ l, g.IsSwap<VAR>this : ∀ a ∈ List.map (⇑s) l, a = 1<GOAL>False
<VAR>α : Type u<VAR>inst✝¹ : DecidableEq α<VAR>β : Type v<VAR>inst✝ : Fintype α<VAR>s : Perm α →* ℤˣ<VAR>hs : Surjective ⇑s<VAR>f : Perm α<VAR>x✝ : f.IsSwap<VAR>x y : α<VAR>hxy : x ≠ y<VAR>hxy' : f = swap x y<VAR>h : ¬s (swap x y) = -1<VAR>this✝¹ : ∀ (f : Perm α), f.IsSwap → s f = 1<VAR>g : Perm α<VAR>hg : s g = -1<VAR>l : List (Perm α)<VAR>hl : l.prod = g ∧ ∀ g ∈ l, g.IsSwap<VAR>this✝ : ∀ a ∈ List.map (⇑s) l, a = 1<VAR>this : s l.prod = 1<GOAL>False
<VAR>α : Type u<VAR>inst✝¹ : DecidableEq α<VAR>β : Type v<VAR>inst✝ : Fintype α<VAR>s : Perm α →* ℤˣ<VAR>hs : Surjective ⇑s<VAR>f : Perm α<VAR>x✝ : f.IsSwap<VAR>x y : α<VAR>hxy : x ≠ y<VAR>hxy' : f = swap x y<VAR>h : ¬s (swap x y) = -1<VAR>this✝¹ : ∀ (f : Perm α), f.IsSwap → s f = 1<VAR>g : Perm α<VAR>hg : s g = -1<VAR>l : List (Perm α)<VAR>hl : l.prod = g ∧ ∀ g ∈ l, g.IsSwap<VAR>this✝ : ∀ a ∈ List.map (⇑s) l, a = 1<VAR>this : -1 = 1<GOAL>False
<VAR>α : Type u<VAR>inst✝¹ : DecidableEq α<VAR>β : Type v<VAR>inst✝ : Fintype α<VAR>s : Perm α →* ℤˣ<VAR>hs : Surjective ⇑s<VAR>this : ∀ {f : Perm α}, f.IsSwap → s f = -1<VAR>f : Perm α<VAR>l : List (Perm α)<VAR>hl₁ : l.prod = f<VAR>hl₂ : ∀ g ∈ l, g.IsSwap<GOAL>s f = sign f
<VAR>α : Type u<VAR>inst✝¹ : DecidableEq α<VAR>β : Type v<VAR>inst✝ : Fintype α<VAR>s : Perm α →* ℤˣ<VAR>hs : Surjective ⇑s<VAR>this : ∀ {f : Perm α}, f.IsSwap → s f = -1<VAR>f : Perm α<VAR>l : List (Perm α)<VAR>hl₁ : l.prod = f<VAR>hl₂ : ∀ g ∈ l, g.IsSwap<VAR>hsl : ∀ a ∈ List.map (⇑s) l, a = -1<GOAL>s f = sign f
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>c : ℤ → ℂ := fun n => -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2<GOAL>HasSum (fun n => (s + 1).Gammaℝ * -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (completedSinZeta (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>c : ℤ → ℂ := fun n => -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2<VAR>hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2<GOAL>HasSum (fun n => (s + 1).Gammaℝ * -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (completedSinZeta (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>c : ℤ → ℂ := fun n => -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2<VAR>hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2<VAR>hF : ∀ (t : ℝ), 0 < t → HasSum (fun n => c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)<GOAL>HasSum (fun n => (s + 1).Gammaℝ * -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (completedSinZeta (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>c : ℤ → ℂ := fun n => -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2<VAR>hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2<VAR>hF : ∀ (t : ℝ), 0 < t → HasSum (fun n => c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)<VAR>h_sum : Summable fun i => ‖c i‖ / |↑i| ^ s.re<GOAL>HasSum (fun n => (s + 1).Gammaℝ * -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (completedSinZeta (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>c : ℤ → ℂ := fun n => -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2<VAR>hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2<VAR>hF : ∀ (t : ℝ), 0 < t → HasSum (fun n => c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)<VAR>h_sum : Summable fun i => ‖c i‖ / |↑i| ^ s.re<VAR>n : ℤ<GOAL>(s + 1).Gammaℝ * -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2 = (s + 1).Gammaℝ * c n * ↑(SignType.sign ↑n) / ↑|↑n| ^ s
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>c : ℤ → ℂ := fun n => -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2<VAR>hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2<VAR>hF : ∀ (t : ℝ), 0 < t → HasSum (fun n => c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)<VAR>h_sum : Summable fun i => ‖c i‖ / |↑i| ^ s.re<VAR>n : ℤ<GOAL>(s + 1).Gammaℝ * -I * ↑(SignType.sign n) * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2 = (s + 1).Gammaℝ * c n * ↑(SignType.sign n) / ↑|n| ^ s
<VAR>n : ℕ<GOAL>fib n ≤ fib (n + 1)
<VAR>n : ℕ<VAR>z : ℂ<GOAL>HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝ : CancelCommMonoid α<VAR>s : Set α<VAR>a : α<VAR>hs : ThreeGPFree (a • s)<VAR>b : α<VAR>hb : b ∈ s<VAR>c : α<VAR>hc : c ∈ s<VAR>d : α<VAR>hd : d ∈ s<VAR>h : b * d = c * c<GOAL>a • b * a • d = a * c * (a * c)
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>r : ℝ<VAR>r_nonneg : 0 ≤ r<VAR>x : E<VAR>hx : x ≠ 0<VAR>this : ‖x‖ ≠ 0<GOAL>‖(↑r * (↑‖x‖)⁻¹) • x‖ = r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E✝ I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>E B I : Set α<VAR>h : BijOn f E N.E<GOAL>(N.comapOn E f).Base B ↔ N.Base (f '' B) ∧ B ⊆ E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E✝ I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>E B I : Set α<VAR>h : BijOn f E N.E<GOAL>B ⊆ E → ((N.comapOn E f).Base B ↔ N.Base (f '' B))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E✝ I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>E B I : Set α<VAR>h : BijOn f E N.E<GOAL>B ⊆ E → InjOn f B
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>p : Submodule K V<VAR>f : End K V<VAR>inst✝ : FiniteDimensional K V<VAR>h : ∀ x ∈ p, f x ∈ p<VAR>h' : ⨆ μ, ⨆ k, (f.genEigenspace μ) k = ⊤<GOAL>⨆ μ, ⨆ k, (genEigenspace (LinearMap.restrict f h) μ) k = ⊤
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>p : Submodule K V<VAR>f : End K V<VAR>inst✝ : FiniteDimensional K V<VAR>h : ∀ x ∈ p, f x ∈ p<VAR>h' : ⨆ μ, ⨆ k, (f.genEigenspace μ) k = ⊤<VAR>this : Submodule.comap p.subtype p = Submodule.comap p.subtype (⨆ μ, ⨆ k, p ⊓ (f.genEigenspace μ) k)<GOAL>⨆ μ, ⨆ k, (genEigenspace (LinearMap.restrict f h) μ) k = ⊤
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>p : Submodule K V<VAR>f : End K V<VAR>inst✝ : FiniteDimensional K V<VAR>h : ∀ x ∈ p, f x ∈ p<VAR>h' : ⨆ μ, ⨆ k, (f.genEigenspace μ) k = ⊤<VAR>this : Submodule.comap p.subtype p = Submodule.comap p.subtype (⨆ μ, ⨆ k, p ⊓ (f.genEigenspace μ) k)<VAR>h_inj : Injective ⇑p.subtype<GOAL>⨆ μ, ⨆ k, (genEigenspace (LinearMap.restrict f h) μ) k = ⊤
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>p : Submodule K V<VAR>f : End K V<VAR>inst✝ : FiniteDimensional K V<VAR>h : ∀ x ∈ p, f x ∈ p<VAR>h' : ⨆ μ, ⨆ k, (f.genEigenspace μ) k = ⊤<VAR>h_inj : Injective ⇑p.subtype<VAR>this : ⊤ = ⨆ i, ⨆ i_1, (genEigenspace (LinearMap.restrict f h) i) i_1<GOAL>⨆ μ, ⨆ k, (genEigenspace (LinearMap.restrict f h) μ) k = ⊤
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>x : α<VAR>y : ℤ<GOAL>round (↑y + x) = y + round x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra R T<VAR>ι κ : Type w<VAR>inst✝ : Fintype ι<VAR>b : Basis ι R S<VAR>x : R<VAR>this : DecidableEq ι<GOAL>(trace R S) ((algebraMap R S) x) = Fintype.card ι • x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra R T<VAR>ι κ : Type w<VAR>inst✝ : Fintype ι<VAR>b : Basis ι R S<VAR>x : R<VAR>this : DecidableEq ι<GOAL>∑ i : ι, ((toMatrix b b) ((lmul R S) ((algebraMap R S) x))).diag i = Fintype.card ι • x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra R T<VAR>ι κ : Type w<VAR>inst✝ : Fintype ι<VAR>b : Basis ι R S<VAR>x : R<VAR>this : DecidableEq ι<VAR>x✝ : ι<VAR>a✝ : x✝ ∈ Finset.univ<GOAL>((toMatrix b b) ((lmul R S) ((algebraMap R S) x))).diag x✝ = x
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F F₁ F₂ : C ⥤ Type w<VAR>α : F₁ ⟶ F₂<VAR>t₁ t₂ : F₁.Elements<VAR>k : t₁ ⟶ t₂<GOAL>F₂.map (↑k) ((fun t => ⟨t.fst, α.app t.fst t.snd⟩) t₁).snd = ((fun t => ⟨t.fst, α.app t.fst t.snd⟩) t₂).snd
<VAR>M₀ : Type u_1<VAR>G₀ : Type u_2<VAR>M₀' : Type u_3<VAR>G₀' : Type u_4<VAR>inst✝⁴ : Mul M₀<VAR>inst✝³ : Zero M₀<VAR>inst✝² : Mul M₀'<VAR>inst✝¹ : Zero M₀'<VAR>f : M₀ → M₀'<VAR>hf : Injective f<VAR>zero : f 0 = 0<VAR>mul : ∀ (x y : M₀), f (x * y) = f x * f y<VAR>inst✝ : IsLeftCancelMulZero M₀'<VAR>a✝ b✝ c✝ : M₀<VAR>Hne : a✝ ≠ 0<VAR>He : a✝ * b✝ = a✝ * c✝<VAR>this : f a✝ * f b✝ = f a✝ * f c✝<GOAL>b✝ = c✝
<VAR>n : ℕ<VAR>i j : Fin n.succ<VAR>h : j = i<GOAL>i.cycleRange j = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>la : Filter α<VAR>pa : ι → Prop<VAR>sa : ι → Set α<VAR>lb : Filter β<VAR>pb : ι' → Prop<VAR>sb : ι' → Set β<VAR>f : α → β<VAR>hlb : lb.HasBasis pb sb<GOAL>Tendsto f la lb ↔ ∀ (i : ι'), pb i → ∀ᶠ (x : α) in la, f x ∈ sb i
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t u : Set E<VAR>x y a b c : E<GOAL>convexJoin 𝕜 (segment 𝕜 a b) {c} = (convexHull 𝕜) {a, b, c}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Rel α β<VAR>I I' : Set β<VAR>h : I' ∈ R.rightFixedPoints<VAR>h₁ : I ≤ I'<GOAL>R.leftDual (R.rightDual I) ≤ R.leftDual (R.rightDual I')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Rel α β<VAR>I I' : Set β<VAR>h : I' ∈ R.rightFixedPoints<VAR>h₁ : I ≤ I'<GOAL>R.rightDual I' ≤ R.rightDual I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Rel α β<VAR>I I' : Set β<VAR>h : I' ∈ R.rightFixedPoints<VAR>h₁ : I ≤ I'<GOAL>I' ≤ I
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t : Set M<VAR>s : Set (Submodule R M)<VAR>z : M<VAR>hs : s.Nonempty<VAR>hdir : DirectedOn (fun x x_1 => x ≤ x_1) s<GOAL>z ∈ sSup s ↔ ∃ y ∈ s, z ∈ y
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t : Set M<VAR>s : Set (Submodule R M)<VAR>z : M<VAR>hs : s.Nonempty<VAR>hdir : DirectedOn (fun x x_1 => x ≤ x_1) s<VAR>this : Nonempty ↑s<GOAL>z ∈ sSup s ↔ ∃ y ∈ s, z ∈ y
<VAR>R : Type u<VAR>I : Type v<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>s : I → R<VAR>t : Finset I<GOAL>IsCoprime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsCoprime (s i) x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>K : Type u_3<VAR>inst✝¹ : Field K<VAR>inst✝ : Module K M<VAR>f g : End K M<VAR>t : K<VAR>ht : t ≠ 0<GOAL>(t • f).IsSemisimple ↔ f.IsSemisimple
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>inst✝⁹ : Monoid R<VAR>inst✝⁸ : NonUnitalNonAssocSemiring A<VAR>inst✝⁷ : DistribMulAction R A<VAR>inst✝⁶ : Star A<VAR>inst✝⁵ : NonUnitalNonAssocSemiring B<VAR>inst✝⁴ : DistribMulAction R B<VAR>inst✝³ : Star B<VAR>inst✝² : NonUnitalNonAssocSemiring C<VAR>inst✝¹ : DistribMulAction R C<VAR>inst✝ : Star C<VAR>f : A →⋆ₙₐ[R] B<VAR>g : A →⋆ₙₐ[R] C<VAR>x : A<GOAL>__src✝.toFun (star x) = star (__src✝.toFun x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Ring S<VAR>inst✝⁸ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K F<VAR>ι : Type w<VAR>E : Type u_7<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra K E<VAR>inst✝ : Algebra R F<VAR>pb : PowerBasis R S<VAR>hE : Splits (algebraMap R F) (minpoly R pb.gen)<VAR>hfx : IsSeparable R pb.gen<VAR>this : DecidableEq F := Classical.decEq F<GOAL>(algebraMap R F) ((norm R) pb.gen) = ∏ σ : S →ₐ[R] F, σ pb.gen
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Ring S<VAR>inst✝⁸ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K F<VAR>ι : Type w<VAR>E : Type u_7<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra K E<VAR>inst✝ : Algebra R F<VAR>pb : PowerBasis R S<VAR>hE : Splits (algebraMap R F) (minpoly R pb.gen)<VAR>hfx : IsSeparable R pb.gen<VAR>this : DecidableEq F := Classical.decEq F<GOAL>((minpoly R pb.gen).aroots F).prod = ∏ σ : S →ₐ[R] F, σ pb.gen
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Ring S<VAR>inst✝⁸ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K F<VAR>ι : Type w<VAR>E : Type u_7<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra K E<VAR>inst✝ : Algebra R F<VAR>pb : PowerBasis R S<VAR>hE : Splits (algebraMap R F) (minpoly R pb.gen)<VAR>hfx : IsSeparable R pb.gen<VAR>this : DecidableEq F := Classical.decEq F<GOAL>((minpoly R pb.gen).aroots F).prod = ∏ x : { y // y ∈ (minpoly R pb.gen).aroots F }, ↑x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Ring S<VAR>inst✝⁸ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K F<VAR>ι : Type w<VAR>E : Type u_7<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra K E<VAR>inst✝ : Algebra R F<VAR>pb : PowerBasis R S<VAR>hE : Splits (algebraMap R F) (minpoly R pb.gen)<VAR>hfx : IsSeparable R pb.gen<VAR>this : DecidableEq F := Classical.decEq F<GOAL>∀ (x : S →ₐ[R] F), (fun σ => σ pb.gen) x = (fun x => ↑x) (pb.liftEquiv' x)
<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>n : ℕ<VAR>s : Simplex ℝ P (n + 2)<VAR>i₁ : Fin (n + 3)<VAR>p : P<VAR>h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂<GOAL>p = s.mongePoint