ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>s : ℕ → α<VAR>hs : CauchySeq s<VAR>S : ℕ → Set ℝ := fun N => (fun p => dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}<VAR>hS : ∀ (N : ℕ), ∃ x, ∀ y ∈ S N, y ≤ x<GOAL>∃ b, (∀ (n : ℕ), 0 ≤ b n) ∧ (∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>s : ℕ → α<VAR>hs : CauchySeq s<VAR>S : ℕ → Set ℝ := fun N => (fun p => dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}<VAR>hS : ∀ (N : ℕ), ∃ x, ∀ y ∈ S N, y ≤ x<VAR>ub : ∀ (m n N : ℕ), N ≤ m → N ≤ n → dist (s m) (s n) ≤ sSup (S N)<GOAL>∃ b, (∀ (n : ℕ), 0 ≤ b n) ∧ (∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>s : ℕ → α<VAR>hs : CauchySeq s<VAR>S : ℕ → Set ℝ := fun N => (fun p => dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}<VAR>hS : ∀ (N : ℕ), ∃ x, ∀ y ∈ S N, y ≤ x<VAR>ub : ∀ (m n N : ℕ), N ≤ m → N ≤ n → dist (s m) (s n) ≤ sSup (S N)<VAR>S0m : ∀ (n : ℕ), 0 ∈ S n<GOAL>∃ b, (∀ (n : ℕ), 0 ≤ b n) ∧ (∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>s : ℕ → α<VAR>hs : CauchySeq s<VAR>S : ℕ → Set ℝ := fun N => (fun p => dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}<VAR>hS : ∀ (N : ℕ), ∃ x, ∀ y ∈ S N, y ≤ x<VAR>ub : ∀ (m n N : ℕ), N ≤ m → N ≤ n → dist (s m) (s n) ≤ sSup (S N)<VAR>S0m : ∀ (n : ℕ), 0 ∈ S n<VAR>S0 : ∀ (n : ℕ), 0 ≤ sSup (S n)<GOAL>∃ b, (∀ (n : ℕ), 0 ≤ b n) ∧ (∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>s : ℕ → α<VAR>hs : CauchySeq s<VAR>S : ℕ → Set ℝ := fun N => (fun p => dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}<VAR>hS : ∀ (N : ℕ), ∃ x, ∀ y ∈ S N, y ≤ x<VAR>ub : ∀ (m n N : ℕ), N ≤ m → N ≤ n → dist (s m) (s n) ≤ sSup (S N)<VAR>S0m : ∀ (n : ℕ), 0 ∈ S n<VAR>S0 : ∀ (n : ℕ), 0 ≤ sSup (S n)<VAR>ε : ℝ<VAR>ε0 : ε > 0<GOAL>∃ N, ∀ n ≥ N, dist (sSup (S n)) 0 < ε
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>s : ℕ → α<VAR>hs : CauchySeq s<VAR>S : ℕ → Set ℝ := fun N => (fun p => dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}<VAR>hS : ∀ (N : ℕ), ∃ x, ∀ y ∈ S N, y ≤ x<VAR>ub : ∀ (m n N : ℕ), N ≤ m → N ≤ n → dist (s m) (s n) ≤ sSup (S N)<VAR>S0m : ∀ (n : ℕ), 0 ∈ S n<VAR>S0 : ∀ (n : ℕ), 0 ≤ sSup (S n)<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>N : ℕ<VAR>hN : ∀ m ≥ N, ∀ n ≥ N, dist (s m) (s n) < ε / 2<VAR>n : ℕ<VAR>hn : n ≥ N<GOAL>dist (sSup (S n)) 0 < ε
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>s : ℕ → α<VAR>hs : CauchySeq s<VAR>S : ℕ → Set ℝ := fun N => (fun p => dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}<VAR>hS : ∀ (N : ℕ), ∃ x, ∀ y ∈ S N, y ≤ x<VAR>ub : ∀ (m n N : ℕ), N ≤ m → N ≤ n → dist (s m) (s n) ≤ sSup (S N)<VAR>S0m : ∀ (n : ℕ), 0 ∈ S n<VAR>S0 : ∀ (n : ℕ), 0 ≤ sSup (S n)<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>N : ℕ<VAR>hN : ∀ m ≥ N, ∀ n ≥ N, dist (s m) (s n) < ε / 2<VAR>n : ℕ<VAR>hn : n ≥ N<GOAL>sSup (S n) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>s : ℕ → α<VAR>hs : CauchySeq s<VAR>S : ℕ → Set ℝ := fun N => (fun p => dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}<VAR>hS : ∀ (N : ℕ), ∃ x, ∀ y ∈ S N, y ≤ x<VAR>ub : ∀ (m n N : ℕ), N ≤ m → N ≤ n → dist (s m) (s n) ≤ sSup (S N)<VAR>S0m : ∀ (n : ℕ), 0 ∈ S n<VAR>S0 : ∀ (n : ℕ), 0 ≤ sSup (S n)<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>N : ℕ<VAR>hN : ∀ m ≥ N, ∀ n ≥ N, dist (s m) (s n) < ε / 2<VAR>n : ℕ<VAR>hn : n ≥ N<GOAL>∀ b ∈ S n, b ≤ ε / 2
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>s : ℕ → α<VAR>hs : CauchySeq s<VAR>S : ℕ → Set ℝ := fun N => (fun p => dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}<VAR>hS : ∀ (N : ℕ), ∃ x, ∀ y ∈ S N, y ≤ x<VAR>ub : ∀ (m n N : ℕ), N ≤ m → N ≤ n → dist (s m) (s n) ≤ sSup (S N)<VAR>S0m : ∀ (n : ℕ), 0 ∈ S n<VAR>S0 : ∀ (n : ℕ), 0 ≤ sSup (S n)<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>N : ℕ<VAR>hN : ∀ m ≥ N, ∀ n ≥ N, dist (s m) (s n) < ε / 2<VAR>n : ℕ<VAR>hn : n ≥ N<VAR>m' n' : ℕ<VAR>hm' : (m', n').1 ≥ n<VAR>hn' : (m', n').2 ≥ n<GOAL>(fun p => dist (s p.1) (s p.2)) (m', n') ≤ ε / 2
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s : Subgroup α<GOAL>∀ (a b : α), Setoid.r a b = (b * a⁻¹ ∈ s)
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s : Subgroup α<GOAL>∀ (a b : α), Setoid.r a b ↔ b * a⁻¹ ∈ s
<VAR>L : Type u<VAR>inst✝¹ : CommRing L<VAR>inst✝ : IsDomain L<VAR>n✝ : ℕ+<VAR>g : L ≃+* L<VAR>n : ℕ+<VAR>t : ↥(rootsOfUnity n L)<GOAL>g ↑↑t = ↑(↑t ^ (χ₀ n g).val)
<VAR>L : Type u<VAR>inst✝¹ : CommRing L<VAR>inst✝ : IsDomain L<VAR>n✝ : ℕ+<VAR>g : L ≃+* L<VAR>n : ℕ+<VAR>t : ↥(rootsOfUnity n L)<GOAL>↑↑(t ^ ModularCyclotomicCharacter_aux g n) = ↑(↑t ^ (ModularCyclotomicCharacter_aux g n % ↑(Fintype.card ↥(rootsOfUnity n L))))
<VAR>ι : Type u_1<VAR>R✝ : Type u_2<VAR>S : Type u_3<VAR>inst✝⁷ : Ring R✝<VAR>inst✝⁶ : Ring S<VAR>M : Type u_4<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R✝ M<VAR>m : Submodule R✝ M<VAR>N : Type u_5<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R✝ N<VAR>R : Type u_6<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Module R M<VAR>simple : IsSimpleModule R M<GOAL>(Module.annihilator R M).IsMaximal
<VAR>ι : Type u_1<VAR>R✝ : Type u_2<VAR>S : Type u_3<VAR>inst✝⁷ : Ring R✝<VAR>inst✝⁶ : Ring S<VAR>M : Type u_4<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R✝ M<VAR>m : Submodule R✝ M<VAR>N : Type u_5<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R✝ N<VAR>R : Type u_6<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Module R M<VAR>simple : IsSimpleModule R M<VAR>I : Ideal R<VAR>max : I.IsMaximal<VAR>e : M ≃ₗ[R] R ⧸ I<GOAL>(Module.annihilator R M).IsMaximal
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<GOAL>A.adjugate.det = A.det ^ (Fintype.card n - 1)
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>h_card : Fintype.card n = 0<GOAL>A.adjugate.det = A.det ^ (Fintype.card n - 1)
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>h_card : Fintype.card n > 0<GOAL>A.adjugate.det = A.det ^ (Fintype.card n - 1)
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n<GOAL>A.adjugate.det = A.det ^ (Fintype.card n - 1)
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n<VAR>A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ<GOAL>A.adjugate.det = A.det ^ (Fintype.card n - 1)
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n<VAR>A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ<GOAL>A'.adjugate.det = A'.det ^ (Fintype.card n - 1)
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n<VAR>A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ<GOAL>A'.det * A'.adjugate.det = A'.det * A'.det ^ (Fintype.card n - 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>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>b : E × F → G<VAR>u : Set (E × F)<VAR>h : IsBoundedBilinearMap 𝕜 b<VAR>p : E × F<VAR>hxs : UniqueDiffWithinAt 𝕜 u p<GOAL>fderivWithin 𝕜 b u p = h.deriv p
<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>b : E × F → G<VAR>u : Set (E × F)<VAR>h : IsBoundedBilinearMap 𝕜 b<VAR>p : E × F<VAR>hxs : UniqueDiffWithinAt 𝕜 u p<GOAL>fderiv 𝕜 b p = h.deriv p
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field L'<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra K L'<VAR>S F E : IntermediateField K L<GOAL>F.toSubalgebra = E.toSubalgebra ↔ F = E
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field L'<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra K L'<VAR>S F E : IntermediateField K L<GOAL>(∀ (x : L), x ∈ F.toSubalgebra ↔ x ∈ E.toSubalgebra) ↔ ∀ (x : L), x ∈ ↑F ↔ x ∈ ↑E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivisionMonoid α<VAR>a b c d : α<VAR>h : a / b = 1<GOAL>a * b⁻¹ = 1
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>ι : Sort u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : BaireSpace X<VAR>T : Set (Set X)<VAR>s : Set X<VAR>hs : IsGδ s<VAR>hd : Dense s<VAR>hc : T.Countable<VAR>hc' : ∀ t ∈ T, IsClosed t<VAR>hU : s ⊆ ⋃₀ T<GOAL>s ⊆ ⋃ i ∈ T, i
<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<GOAL>List.map (fun x => x.toProd.2) p.darts = p.support.tail
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : LinearOrderedCommRing 𝕜<VAR>inst✝¹¹ : LinearOrderedCommRing E<VAR>inst✝¹⁰ : LinearOrderedAddCommGroup F<VAR>inst✝⁹ : Module 𝕜 E<VAR>inst✝⁸ : Module 𝕜 F<VAR>inst✝⁷ : Module E F<VAR>inst✝⁶ : IsScalarTower 𝕜 E F<VAR>inst✝⁵ : SMulCommClass 𝕜 E F<VAR>inst✝⁴ : OrderedSMul 𝕜 E<VAR>inst✝³ : OrderedSMul 𝕜 F<VAR>inst✝² : OrderedSMul E F<VAR>s : Set 𝕜<VAR>f✝ : 𝕜 → E<VAR>g✝ : 𝕜 → F<VAR>inst✝¹ : IsScalarTower 𝕜 E E<VAR>inst✝ : SMulCommClass 𝕜 E E<VAR>f g : 𝕜 → E<VAR>hf : ConvexOn 𝕜 s f<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x<GOAL>ConvexOn 𝕜 s (f ^ 0)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : LinearOrderedCommRing 𝕜<VAR>inst✝¹¹ : LinearOrderedCommRing E<VAR>inst✝¹⁰ : LinearOrderedAddCommGroup F<VAR>inst✝⁹ : Module 𝕜 E<VAR>inst✝⁸ : Module 𝕜 F<VAR>inst✝⁷ : Module E F<VAR>inst✝⁶ : IsScalarTower 𝕜 E F<VAR>inst✝⁵ : SMulCommClass 𝕜 E F<VAR>inst✝⁴ : OrderedSMul 𝕜 E<VAR>inst✝³ : OrderedSMul 𝕜 F<VAR>inst✝² : OrderedSMul E F<VAR>s : Set 𝕜<VAR>f✝ : 𝕜 → E<VAR>g✝ : 𝕜 → F<VAR>inst✝¹ : IsScalarTower 𝕜 E E<VAR>inst✝ : SMulCommClass 𝕜 E E<VAR>f g : 𝕜 → E<VAR>hf : ConvexOn 𝕜 s f<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x<VAR>n : ℕ<GOAL>ConvexOn 𝕜 s (f ^ (n + 1))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : LinearOrderedCommRing 𝕜<VAR>inst✝¹¹ : LinearOrderedCommRing E<VAR>inst✝¹⁰ : LinearOrderedAddCommGroup F<VAR>inst✝⁹ : Module 𝕜 E<VAR>inst✝⁸ : Module 𝕜 F<VAR>inst✝⁷ : Module E F<VAR>inst✝⁶ : IsScalarTower 𝕜 E F<VAR>inst✝⁵ : SMulCommClass 𝕜 E F<VAR>inst✝⁴ : OrderedSMul 𝕜 E<VAR>inst✝³ : OrderedSMul 𝕜 F<VAR>inst✝² : OrderedSMul E F<VAR>s : Set 𝕜<VAR>f✝ : 𝕜 → E<VAR>g✝ : 𝕜 → F<VAR>inst✝¹ : IsScalarTower 𝕜 E E<VAR>inst✝ : SMulCommClass 𝕜 E E<VAR>f g : 𝕜 → E<VAR>hf : ConvexOn 𝕜 s f<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x<VAR>n : ℕ<GOAL>ConvexOn 𝕜 s (f * f ^ n)
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁸ : CommRing R✝<VAR>inst✝⁷ : CommRing A✝<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R✝ A✝<VAR>inst✝³ : Algebra R✝ B<VAR>f✝ : R✝ →+* S<VAR>R : Type u_5<VAR>A : Type u_6<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>x : A<VAR>f : R[X]<VAR>hf : f.Monic<VAR>hfx : (aeval x) f = 0<VAR>a✝ : Nontrivial A<GOAL>span R ↑(Finset.image (fun x_1 => x ^ x_1) (Finset.range f.natDegree)) = Subalgebra.toSubmodule (Algebra.adjoin R {x})
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁸ : CommRing R✝<VAR>inst✝⁷ : CommRing A✝<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R✝ A✝<VAR>inst✝³ : Algebra R✝ B<VAR>f✝ : R✝ →+* S<VAR>R : Type u_5<VAR>A : Type u_6<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>x : A<VAR>f : R[X]<VAR>hf : f.Monic<VAR>hfx : (aeval x) f = 0<VAR>a✝ : Nontrivial A<VAR>hf1 : f ≠ 1<GOAL>span R ↑(Finset.image (fun x_1 => x ^ x_1) (Finset.range f.natDegree)) = Subalgebra.toSubmodule (Algebra.adjoin R {x})
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁸ : CommRing R✝<VAR>inst✝⁷ : CommRing A✝<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R✝ A✝<VAR>inst✝³ : Algebra R✝ B<VAR>f✝ : R✝ →+* S<VAR>R : Type u_5<VAR>A : Type u_6<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>x : A<VAR>f : R[X]<VAR>hf : f.Monic<VAR>hfx : (aeval x) f = 0<VAR>a✝ : Nontrivial A<VAR>hf1 : f ≠ 1<VAR>s : A<VAR>hs : s ∈ ↑(Finset.image (fun x_1 => x ^ x_1) (Finset.range f.natDegree))<GOAL>s ∈ ↑(Subalgebra.toSubmodule (Algebra.adjoin R {x}))
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁸ : CommRing R✝<VAR>inst✝⁷ : CommRing A✝<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R✝ A✝<VAR>inst✝³ : Algebra R✝ B<VAR>f✝ : R✝ →+* S<VAR>R : Type u_5<VAR>A : Type u_6<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>x : A<VAR>f : R[X]<VAR>hf : f.Monic<VAR>hfx : (aeval x) f = 0<VAR>a✝ : Nontrivial A<VAR>hf1 : f ≠ 1<VAR>r : A<VAR>hr : r ∈ Subalgebra.toSubmodule (Algebra.adjoin R {x})<GOAL>r ∈ span R ↑(Finset.image (fun x_1 => x ^ x_1) (Finset.range f.natDegree))
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁸ : CommRing R✝<VAR>inst✝⁷ : CommRing A✝<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R✝ A✝<VAR>inst✝³ : Algebra R✝ B<VAR>f✝ : R✝ →+* S<VAR>R : Type u_5<VAR>A : Type u_6<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>x : A<VAR>f : R[X]<VAR>hf : f.Monic<VAR>hfx : (aeval x) f = 0<VAR>a✝ : Nontrivial A<VAR>hf1 : f ≠ 1<VAR>r : A<VAR>hr : r ∈ (aeval x).range<GOAL>r ∈ span R ↑(Finset.image (fun x_1 => x ^ x_1) (Finset.range f.natDegree))
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁸ : CommRing R✝<VAR>inst✝⁷ : CommRing A✝<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R✝ A✝<VAR>inst✝³ : Algebra R✝ B<VAR>f✝ : R✝ →+* S<VAR>R : Type u_5<VAR>A : Type u_6<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>x : A<VAR>f : R[X]<VAR>hf : f.Monic<VAR>hfx : (aeval x) f = 0<VAR>a✝ : Nontrivial A<VAR>hf1 : f ≠ 1<VAR>p : R[X]<VAR>hr : (aeval x) p ∈ (aeval x).range<GOAL>(aeval x) p ∈ span R ↑(Finset.image (fun x_1 => x ^ x_1) (Finset.range f.natDegree))
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁸ : CommRing R✝<VAR>inst✝⁷ : CommRing A✝<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R✝ A✝<VAR>inst✝³ : Algebra R✝ B<VAR>f✝ : R✝ →+* S<VAR>R : Type u_5<VAR>A : Type u_6<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>x : A<VAR>f : R[X]<VAR>hf : f.Monic<VAR>hfx : (aeval x) f = 0<VAR>a✝ : Nontrivial A<VAR>hf1 : f ≠ 1<VAR>p : R[X]<VAR>hr : (aeval x) p ∈ (aeval x).range<GOAL>∑ n ∈ (p %ₘ f).support, eval₂ (algebraMap R A) x (C ((p %ₘ f).coeff n) * X ^ n) ∈ span R ↑(Finset.image (fun x_1 => x ^ x_1) (Finset.range f.natDegree))
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁸ : CommRing R✝<VAR>inst✝⁷ : CommRing A✝<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R✝ A✝<VAR>inst✝³ : Algebra R✝ B<VAR>f✝ : R✝ →+* S<VAR>R : Type u_5<VAR>A : Type u_6<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>x : A<VAR>f : R[X]<VAR>hf : f.Monic<VAR>hfx : (aeval x) f = 0<VAR>a✝ : Nontrivial A<VAR>hf1 : f ≠ 1<VAR>p : R[X]<VAR>hr : (aeval x) p ∈ (aeval x).range<VAR>k : ℕ<VAR>hkq : k ∈ (p %ₘ f).support<GOAL>eval₂ (algebraMap R A) x (C ((p %ₘ f).coeff k) * X ^ k) ∈ span R ↑(Finset.image (fun x_1 => x ^ x_1) (Finset.range f.natDegree))
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁸ : CommRing R✝<VAR>inst✝⁷ : CommRing A✝<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R✝ A✝<VAR>inst✝³ : Algebra R✝ B<VAR>f✝ : R✝ →+* S<VAR>R : Type u_5<VAR>A : Type u_6<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>x : A<VAR>f : R[X]<VAR>hf : f.Monic<VAR>hfx : (aeval x) f = 0<VAR>a✝ : Nontrivial A<VAR>hf1 : f ≠ 1<VAR>p : R[X]<VAR>hr : (aeval x) p ∈ (aeval x).range<VAR>k : ℕ<VAR>hkq : k ∈ (p %ₘ f).support<GOAL>(p %ₘ f).coeff k • x ^ k ∈ span R ↑(Finset.image (fun x_1 => x ^ x_1) (Finset.range f.natDegree))
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>f : ι → α<VAR>hf : ¬BddBelow (range f)<GOAL>⋂ i, Iio (f i) = ∅
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>f : ι → α<VAR>hf : ¬BddBelow (range f)<GOAL>⋂ i, Iio (f i) ⊆ ∅
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>f : ι → α<VAR>hf : ¬BddBelow (range f)<GOAL>⋂ i, Iio (f i) ⊆ ⋂ i, Iic (f i)
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>f : ι → α<VAR>hf : ¬BddBelow (range f)<VAR>i✝ : ι<GOAL>Iio (f i✝) ⊆ Iic (f i✝)
<VAR>x : ℂ<GOAL>cos x = -1 ↔ ∃ k, ↑π + ↑k * (2 * ↑π) = x
<VAR>x : ℂ<GOAL>(∃ k, ↑k * (2 * ↑π) = x - ↑π) ↔ ∃ k, ↑π + ↑k * (2 * ↑π) = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝² : Zero M<VAR>a a' : α<VAR>b : M<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Finite α<VAR>x : α<VAR>m : M<GOAL>equivFunOnFinite.symm (Pi.single x m) = single x m
<VAR>a b c : Prop<GOAL>(a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))
<VAR>n b f : ℕ<GOAL>∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : PerfectRing k p<GOAL>DiscreteValuationRing.HasUnitMulPowIrreducibleFactorization (𝕎 k)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : PerfectRing k p<VAR>x : 𝕎 k<VAR>hx : x ≠ 0<GOAL>∃ n, Associated (↑p ^ n) x
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : PerfectRing k p<VAR>x : 𝕎 k<VAR>hx : x ≠ 0<VAR>n : ℕ<VAR>b : (𝕎 k)ˣ<VAR>hb : x = ↑p ^ n * ↑b<GOAL>∃ n, Associated (↑p ^ n) x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemifield α<VAR>inst✝ : LinearOrderedSemifield β<VAR>s : Set ι<VAR>f f₁ f₂ : ι → α<VAR>g g₁ g₂ : ι → β<VAR>hf : StrongLT 0 f<VAR>hg : StrongLT 0 g<GOAL>Monovary f⁻¹ g⁻¹ ↔ Monovary f g
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : LaxMonoidalFunctor C D<VAR>X : C<GOAL>(λ_ (F.obj X)).inv ≫ F.ε ▷ F.obj X ≫ F.μ (𝟙_ C) X = F.map (λ_ X).inv
<VAR>α : Type u_1<VAR>inst✝ : DivisionSemiring α<VAR>n : ℕ<VAR>hn : ↑n ≠ 0<VAR>k : ℕ<VAR>this : n ≠ 0<GOAL>↑(n * k / n) = ↑(n * k) / ↑n
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : PartialOrder β<VAR>inst✝¹ : OrderTop α<VAR>inst✝ : OrderTop β<VAR>f : α ≃o β<GOAL>IsCoatomic α ↔ IsCoatomic β
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s t : Set α<VAR>a : α<GOAL>(insert a s).IsWF ↔ s.IsWF
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : AddGroup α<VAR>inst✝ : AddGroup β<VAR>h : Antiperiodic f c<VAR>n : ℕ<GOAL>f (x - n • c) = (-1) ^ n • f x
<VAR>X : Type u_1<VAR>f : X →₀ ℤ<GOAL>toFinsupp (toFreeAbelianGroup f) = f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : SMul 𝕜 E<VAR>A B C : Set E<VAR>x : E<VAR>hAB : IsExtreme 𝕜 A B<VAR>hBC : IsExtreme 𝕜 B C<GOAL>IsExtreme 𝕜 A C
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : SMul 𝕜 E<VAR>A B C : Set E<VAR>x✝ : E<VAR>hAB : IsExtreme 𝕜 A B<VAR>hBC : IsExtreme 𝕜 B C<VAR>x₁ : E<VAR>hx₁A : x₁ ∈ A<VAR>x₂ : E<VAR>hx₂A : x₂ ∈ A<VAR>x : E<VAR>hxC : x ∈ C<VAR>hx : x ∈ openSegment 𝕜 x₁ x₂<GOAL>x₁ ∈ C ∧ x₂ ∈ C
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : SMul 𝕜 E<VAR>A B C : Set E<VAR>x✝ : E<VAR>hAB : IsExtreme 𝕜 A B<VAR>hBC : IsExtreme 𝕜 B C<VAR>x₁ : E<VAR>hx₁A : x₁ ∈ A<VAR>x₂ : E<VAR>hx₂A : x₂ ∈ A<VAR>x : E<VAR>hxC : x ∈ C<VAR>hx : x ∈ openSegment 𝕜 x₁ x₂<VAR>hx₁B : x₁ ∈ B<VAR>hx₂B : x₂ ∈ B<GOAL>x₁ ∈ C ∧ x₂ ∈ C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝¹ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>X : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>f : X → α →ᵤ[𝔖] β<GOAL>Continuous f ↔ ∀ s ∈ 𝔖, Continuous (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖) ∘ f)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>s : Set (↥M₁ ⊗[R] ↥N₁)<VAR>hs : s.Finite<GOAL>∃ N', ∃ (hN : N' ≤ N₁), Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.range (LinearMap.lTensor (↥M₁) (inclusion hN)))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>s : Set (↥M₁ ⊗[R] ↥N₁)<VAR>hs : s.Finite<VAR>w✝¹ : Submodule R M<VAR>N' : Submodule R N<VAR>w✝ : w✝¹ ≤ M₁<VAR>hN : N' ≤ N₁<VAR>left✝ : Module.Finite R ↥w✝¹<VAR>hfin : Module.Finite R ↥N'<VAR>h : s ⊆ ↑(LinearMap.range (map (inclusion w✝) (inclusion hN)))<GOAL>∃ N', ∃ (hN : N' ≤ N₁), Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.range (LinearMap.lTensor (↥M₁) (inclusion hN)))