ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f g : E →ₗ.[R] F<VAR>h : Disjoint f.domain g.domain<VAR>x : ↥f.domain<VAR>y : ↥g.domain<VAR>hxy : ↑x = ↑y<GOAL>↑f x = ↑g y
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f g : E →ₗ.[R] F<VAR>h : ∀ x ∈ f.domain, x ∈ g.domain → x = 0<VAR>x : ↥f.domain<VAR>y : ↥g.domain<VAR>hxy : ↑x = ↑y<GOAL>↑f x = ↑g y
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f g : E →ₗ.[R] F<VAR>h : ∀ x ∈ f.domain, x ∈ g.domain → x = 0<VAR>x : ↥f.domain<VAR>y : ↥g.domain<VAR>hxy : ↑x = ↑y<VAR>hy : y = 0<GOAL>↑f x = ↑g y
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f g : E →ₗ.[R] F<VAR>h : ∀ x ∈ f.domain, x ∈ g.domain → x = 0<VAR>x : ↥f.domain<VAR>y : ↥g.domain<VAR>hxy : ↑x = ↑y<VAR>hy : y = 0<VAR>hx : x = 0<GOAL>↑f x = ↑g y
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>x : R<VAR>inst✝ : Away x S<VAR>s : S<GOAL>s * (algebraMap R S) (x ^ (sec x s).2) = (algebraMap R S) (sec x s).1
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>x : R<VAR>inst✝ : Away x S<VAR>s : S<GOAL>s * (algebraMap R S) (x ^ Exists.choose ⋯) = s * (algebraMap R S) ↑(IsLocalization.sec (Submonoid.powers x) s).2
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>x : R<VAR>inst✝ : Away x S<VAR>s : S<GOAL>x ^ Exists.choose ⋯ = ↑(IsLocalization.sec (Submonoid.powers x) s).2
<VAR>𝓕 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedGroup E<VAR>inst✝ : SeminormedGroup F<VAR>s : Set E<VAR>a✝ a₁ a₂ b✝ b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>a b c : E<GOAL>dist (a / b) c = dist a (c * b)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring A<VAR>inst✝⁶ : CommSemiring B<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra R B<VAR>inst✝² : Module A M<VAR>inst✝¹ : Module B M<VAR>inst✝ : Module R M<VAR>D D1 D2 : Derivation R A M<VAR>r : R<VAR>a b : A<VAR>s : Set A<VAR>h : Set.EqOn (⇑D1) (⇑D2) s<VAR>x✝ : A<VAR>hx✝ : x✝ ∈ ↑(adjoin R s)<VAR>x y : A<VAR>hx : D1 x = D2 x<VAR>hy : D1 y = D2 y<GOAL>D1 (x + y) = D2 (x + y)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring A<VAR>inst✝⁶ : CommSemiring B<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra R B<VAR>inst✝² : Module A M<VAR>inst✝¹ : Module B M<VAR>inst✝ : Module R M<VAR>D D1 D2 : Derivation R A M<VAR>r : R<VAR>a b : A<VAR>s : Set A<VAR>h : Set.EqOn (⇑D1) (⇑D2) s<VAR>x✝ : A<VAR>hx✝ : x✝ ∈ ↑(adjoin R s)<VAR>x y : A<VAR>hx : D1 x = D2 x<VAR>hy : D1 y = D2 y<GOAL>D1 (x * y) = D2 (x * y)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>x : E<GOAL>x ∈ perfectClosure F E ↔ (minpoly F x).natSepDegree = 1
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>N O n o : ℕ<VAR>hn : n ≤ N<VAR>ho : o ≤ O<GOAL>(revAt (N + O)) (n + o) = (revAt N) n + (revAt O) o
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>O n o : ℕ<VAR>ho : o ≤ O<VAR>n' : ℕ<VAR>hn : n ≤ n + n'<GOAL>(revAt (n + n' + O)) (n + o) = (revAt (n + n')) n + (revAt O) o
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>n o n' : ℕ<VAR>hn : n ≤ n + n'<VAR>o' : ℕ<VAR>ho : o ≤ o + o'<GOAL>(revAt (n + n' + (o + o'))) (n + o) = (revAt (n + n')) n + (revAt (o + o')) o
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>n o n' : ℕ<VAR>hn : n ≤ n + n'<VAR>o' : ℕ<VAR>ho : o ≤ o + o'<GOAL>(revAt (n + n' + (o + o'))) (n + o) = n + n' - n + (o + o' - o)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>n o n' : ℕ<VAR>hn : n ≤ n + n'<VAR>o' : ℕ<VAR>ho : o ≤ o + o'<GOAL>n + o + (n' + o') - (n + o) = n + n' - n + (o + o' - o)
<VAR>α : Type u_1<VAR>s✝ t✝ : Finset α<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>t : Finset α<GOAL>t ∈ (insert a s).powerset ↔ t ∈ s.powerset ∪ image (insert a) s.powerset
<VAR>α : Type u_1<VAR>s✝ t✝ : Finset α<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>t : Finset α<GOAL>t.erase a ⊆ s ↔ t ⊆ s ∨ ∃ a_1 ⊆ s, insert a a_1 = t
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>s : Set ι<VAR>f : ι → Set X<VAR>hs : s.Countable<VAR>hf : ∀ i ∈ s, IsLindelof (f i)<GOAL>IsLindelof (⋃ i ∈ s, f i)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>s : Set ι<VAR>f : ι → Set X<VAR>hs : s.Countable<VAR>hf : ∀ i ∈ s, IsLindelof (f i)<GOAL>∀ {ι_1 : Type u} (U : ι_1 → Set X), (∀ (i : ι_1), IsOpen (U i)) → ⋃ i ∈ s, f i ⊆ ⋃ i, U i → ∃ t, t.Countable ∧ ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, U i
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>s : Set ι<VAR>f : ι → Set X<VAR>hs : s.Countable<VAR>hf : ∀ i ∈ s, IsLindelof (f i)<VAR>i : Type u<VAR>U : i → Set X<VAR>hU : ∀ (i : i), IsOpen (U i)<VAR>hUcover : ⋃ i ∈ s, f i ⊆ ⋃ i, U i<GOAL>∃ t, t.Countable ∧ ⋃ i ∈ s, f i ⊆ ⋃ i_1 ∈ t, U i_1
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>s : Set ι<VAR>f : ι → Set X<VAR>hs : s.Countable<VAR>hf : ∀ i ∈ s, IsLindelof (f i)<VAR>i : Type u<VAR>U : i → Set X<VAR>hU : ∀ (i : i), IsOpen (U i)<VAR>hUcover : ⋃ i ∈ s, f i ⊆ ⋃ i, U i<VAR>hiU : ∀ i_1 ∈ s, f i_1 ⊆ ⋃ i, U i<GOAL>∃ t, t.Countable ∧ ⋃ i ∈ s, f i ⊆ ⋃ i_1 ∈ t, U i_1
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>s : Set ι<VAR>f : ι → Set X<VAR>hs : s.Countable<VAR>hf : ∀ i ∈ s, IsLindelof (f i)<VAR>i : Type u<VAR>U : i → Set X<VAR>hU : ∀ (i : i), IsOpen (U i)<VAR>hUcover : ⋃ i ∈ s, f i ⊆ ⋃ i, U i<VAR>hiU : ∀ i_1 ∈ s, f i_1 ⊆ ⋃ i, U i<VAR>iSets : ∀ i_1 ∈ s, ∃ r, r.Countable ∧ f i_1 ⊆ ⋃ i_2 ∈ r, U i_2<GOAL>∃ t, t.Countable ∧ ⋃ i ∈ s, f i ⊆ ⋃ i_1 ∈ t, U i_1
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>s : Set ι<VAR>f : ι → Set X<VAR>hs : s.Countable<VAR>hf : ∀ i ∈ s, IsLindelof (f i)<VAR>i : Type u<VAR>U : i → Set X<VAR>hU : ∀ (i : i), IsOpen (U i)<VAR>hUcover : ⋃ i ∈ s, f i ⊆ ⋃ i, U i<VAR>hiU : ∀ i_1 ∈ s, f i_1 ⊆ ⋃ i, U i<VAR>r : ι → Set i<VAR>hr : ∀ i_1 ∈ s, (r i_1).Countable ∧ f i_1 ⊆ ⋃ i_2 ∈ r i_1, U i_2<GOAL>∃ t, t.Countable ∧ ⋃ i ∈ s, f i ⊆ ⋃ i_1 ∈ t, U i_1
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>s : Set ι<VAR>f : ι → Set X<VAR>hs : s.Countable<VAR>hf : ∀ i ∈ s, IsLindelof (f i)<VAR>i : Type u<VAR>U : i → Set X<VAR>hU : ∀ (i : i), IsOpen (U i)<VAR>hUcover : ⋃ i ∈ s, f i ⊆ ⋃ i, U i<VAR>hiU : ∀ i_1 ∈ s, f i_1 ⊆ ⋃ i, U i<VAR>r : ι → Set i<VAR>hr : ∀ i_1 ∈ s, (r i_1).Countable ∧ f i_1 ⊆ ⋃ i_2 ∈ r i_1, U i_2<GOAL>(⋃ i_1 ∈ s, r i_1).Countable ∧ ⋃ i ∈ s, f i ⊆ ⋃ i_1 ∈ ⋃ i_2 ∈ s, r i_2, U i_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq β<VAR>f✝ g : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>a✝ : α<VAR>b c : β<VAR>f : α → β<VAR>a : α<VAR>x : β<GOAL>x ∈ image f {a} ↔ x ∈ {f a}
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>A : Set X<GOAL>IsClosed (derivedSet A)
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>A : Set X<GOAL>derivedSet (derivedSet (closure A)) ⊆ derivedSet (closure A)
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>A : Set X<GOAL>derivedSet (closure A) ⊆ closure A
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x✝ y : M<VAR>hv : LinearIndependent R v<VAR>inst✝ : Nontrivial R<VAR>x : ↥(span R (range v))<GOAL>Span.repr R (range v) x = Finsupp.equivMapDomain (Equiv.ofInjective v ⋯) (hv.repr x)
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x✝ y : M<VAR>hv : LinearIndependent R v<VAR>inst✝ : Nontrivial R<VAR>x : ↥(span R (range v))<VAR>p : Finsupp.equivMapDomain (Equiv.ofInjective v ⋯).symm (Span.repr R (range v) x) = hv.repr x<GOAL>Span.repr R (range v) x = Finsupp.equivMapDomain (Equiv.ofInjective v ⋯) (hv.repr x)
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<GOAL>p < A * B
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<GOAL>p < (b ^ (2 * p) - 1) / (b ^ 2 - 1)
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1<GOAL>p < (b ^ (2 * p) - 1) / (b ^ 2 - 1)
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1<GOAL>p * (b ^ 2 - 1) < b ^ (2 * p) - 1
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1<GOAL>p * b ^ 2 - p < (b ^ 2) ^ p - 1
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1<GOAL>p * b ^ 2 - p < (b ^ 2) ^ (p - 1 + 1) - 1
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1<GOAL>p * b ^ 2 - p < (b ^ 2) ^ (p - 1) * b ^ 2 - 1
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1<GOAL>p * b ^ 2 < (b ^ 2) ^ (p - 1) * b ^ 2
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1<GOAL>p < (b ^ 2) ^ (p - 1)
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1<GOAL>p < b ^ (2 * p - 2)
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1<VAR>this : 2 ≤ 2 * p - 2<GOAL>p < b ^ (2 * p - 2)
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1<VAR>this✝ : 2 ≤ 2 * p - 2<VAR>this : 2 + p ≤ 2 * p<GOAL>p < b ^ (2 * p - 2)
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>AB_dvd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1<VAR>this✝¹ : 2 ≤ 2 * p - 2<VAR>this✝ : 2 + p ≤ 2 * p<VAR>this : p ≤ 2 * p - 2<GOAL>p < b ^ (2 * p - 2)
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConcaveOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' (Ioi x) x<GOAL>slope f x y ≤ f'
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁵ : SeminormedAddCommGroup E<VAR>inst✝¹⁴ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹³ : SeminormedAddCommGroup F<VAR>inst✝¹² : SeminormedAddCommGroup Fₗ<VAR>inst✝¹¹ : SeminormedAddCommGroup G<VAR>inst✝¹⁰ : SeminormedAddCommGroup Gₗ<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁴ : NormedSpace 𝕜₂ F<VAR>inst✝³ : NormedSpace 𝕜 Fₗ<VAR>inst✝² : NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝ : FunLike 𝓕 E F<VAR>f : E →SL[σ₁₂] F<VAR>K : ℝ≥0<VAR>hf : LipschitzWith K ⇑f<VAR>x : E<GOAL>‖f x‖ ≤ ↑K * ‖x‖
<VAR>f : ℝ → ℝ<VAR>hf : GrowsPolynomially f<GOAL>GrowsPolynomially fun x => ‖f x‖
<VAR>f : ℝ → ℝ<VAR>hf : GrowsPolynomially f<GOAL>GrowsPolynomially fun x => |f x|
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing S<VAR>inst✝³ : Algebra R S<VAR>P : Type u_3<VAR>inst✝² : CommRing P<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : Monoid.FG ↥M<GOAL>Algebra.FiniteType R S
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing S<VAR>inst✝³ : Algebra R S<VAR>P : Type u_3<VAR>inst✝² : CommRing P<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : Monoid.FG ↥M<VAR>this : Monoid.FG ↥(invSubmonoid M S)<GOAL>Algebra.FiniteType R S
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing S<VAR>inst✝³ : Algebra R S<VAR>P : Type u_3<VAR>inst✝² : CommRing P<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : Monoid.FG ↥M<VAR>this : (invSubmonoid M S).FG<GOAL>Algebra.FiniteType R S
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing S<VAR>inst✝³ : Algebra R S<VAR>P : Type u_3<VAR>inst✝² : CommRing P<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : Monoid.FG ↥M<VAR>s : Finset S<VAR>hs : Submonoid.closure ↑s = invSubmonoid M S<GOAL>Algebra.adjoin R ↑s = ⊤
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing S<VAR>inst✝³ : Algebra R S<VAR>P : Type u_3<VAR>inst✝² : CommRing P<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : Monoid.FG ↥M<VAR>s : Finset S<VAR>hs : Submonoid.closure ↑s = invSubmonoid M S<GOAL>⊤ ≤ Algebra.adjoin R ↑s
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing S<VAR>inst✝³ : Algebra R S<VAR>P : Type u_3<VAR>inst✝² : CommRing P<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : Monoid.FG ↥M<VAR>s : Finset S<VAR>hs : Submonoid.closure ↑s = invSubmonoid M S<VAR>x : S<GOAL>x ∈ ↑(Subalgebra.toSubmodule (Algebra.adjoin R ↑s))
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing S<VAR>inst✝³ : Algebra R S<VAR>P : Type u_3<VAR>inst✝² : CommRing P<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : Monoid.FG ↥M<VAR>s : Finset S<VAR>hs : Submonoid.closure ↑s = invSubmonoid M S<VAR>x : S<GOAL>x ∈ ↑⊤
<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>α : Type v<VAR>β : Type w<VAR>ι : Type u_6<VAR>M : Matrix m n α<VAR>i✝ : m<VAR>j : n<VAR>b : n → α<VAR>c : m → α<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Zero α<VAR>v : n → α<VAR>i : n<VAR>x : α<GOAL>(diagonal v).updateRow i (Pi.single i x) = diagonal (Function.update v i x)
<VAR>x y : ℂ<GOAL>(cexp x).re = Real.exp x.re * Real.cos x.im
<VAR>x y : ℂ<GOAL>(cexp ↑x.re * (cos ↑x.im + sin ↑x.im * I)).re = Real.exp x.re * Real.cos x.im
<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>M : Type u_5<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module A M<VAR>inst✝¹ : IsScalarTower R A M<VAR>inst✝ : NoZeroSMulDivisors A M<VAR>N : Submodule R M<VAR>hN : N ≠ ⊥<VAR>hN' : N.FG<VAR>x : A<VAR>hx : ∀ n ∈ N, x • n ∈ N<GOAL>IsIntegral 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>M : Type u_5<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module A M<VAR>inst✝¹ : IsScalarTower R A M<VAR>inst✝ : NoZeroSMulDivisors A M<VAR>N : Submodule R M<VAR>hN : N ≠ ⊥<VAR>hN' : N.FG<VAR>x : A<VAR>hx : ∀ n ∈ N, x • n ∈ N<VAR>A' : Subalgebra R A := { carrier := {x | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }<GOAL>IsIntegral 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>M : Type u_5<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module A M<VAR>inst✝¹ : IsScalarTower R A M<VAR>inst✝ : NoZeroSMulDivisors A M<VAR>N : Submodule R M<VAR>hN : N ≠ ⊥<VAR>hN' : N.FG<VAR>x : A<VAR>hx : ∀ n ∈ N, x • n ∈ N<VAR>A' : Subalgebra R A := { carrier := {x | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }<VAR>f : ↥A' →ₐ[R] Module.End R ↥N := AlgHom.ofLinearMap { toFun := fun x => (DistribMulAction.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯<GOAL>IsIntegral 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>M : Type u_5<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module A M<VAR>inst✝¹ : IsScalarTower R A M<VAR>inst✝ : NoZeroSMulDivisors A M<VAR>N : Submodule R M<VAR>hN : N ≠ ⊥<VAR>hN' : N.FG<VAR>x : A<VAR>hx : ∀ n ∈ N, x • n ∈ N<VAR>A' : Subalgebra R A := { carrier := {x | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }<VAR>f : ↥A' →ₐ[R] Module.End R ↥N := AlgHom.ofLinearMap { toFun := fun x => (DistribMulAction.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯<VAR>a : M<VAR>ha₁ : a ∈ N<VAR>ha₂ : a ≠ 0<GOAL>IsIntegral 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>M : Type u_5<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module A M<VAR>inst✝¹ : IsScalarTower R A M<VAR>inst✝ : NoZeroSMulDivisors A M<VAR>N : Submodule R M<VAR>hN : N ≠ ⊥<VAR>hN' : N.FG<VAR>x : A<VAR>hx : ∀ n ∈ N, x • n ∈ N<VAR>A' : Subalgebra R A := { carrier := {x | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }<VAR>f : ↥A' →ₐ[R] Module.End R ↥N := AlgHom.ofLinearMap { toFun := fun x => (DistribMulAction.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯<VAR>a : M<VAR>ha₁ : a ∈ N<VAR>ha₂ : a ≠ 0<VAR>this : Function.Injective ⇑f<GOAL>IsIntegral 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>M : Type u_5<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module A M<VAR>inst✝¹ : IsScalarTower R A M<VAR>inst✝ : NoZeroSMulDivisors A M<VAR>N : Submodule R M<VAR>hN : N ≠ ⊥<VAR>hN' : N.FG<VAR>x : A<VAR>hx : ∀ n ∈ N, x • n ∈ N<VAR>A' : Subalgebra R A := { carrier := {x | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }<VAR>f : ↥A' →ₐ[R] Module.End R ↥N := AlgHom.ofLinearMap { toFun := fun x => (DistribMulAction.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯<VAR>a : M<VAR>ha₁ : a ∈ N<VAR>ha₂ : a ≠ 0<VAR>this : Function.Injective ⇑f<GOAL>IsIntegral R (A'.val ⟨x, hx⟩)
<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>M : Type u_5<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module A M<VAR>inst✝¹ : IsScalarTower R A M<VAR>inst✝ : NoZeroSMulDivisors A M<VAR>N : Submodule R M<VAR>hN : N ≠ ⊥<VAR>hN' : N.FG<VAR>x : A<VAR>hx : ∀ n ∈ N, x • n ∈ N<VAR>A' : Subalgebra R A := { carrier := {x | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }<VAR>f : ↥A' →ₐ[R] Module.End R ↥N := AlgHom.ofLinearMap { toFun := fun x => (DistribMulAction.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯<VAR>a : M<VAR>ha₁ : a ∈ N<VAR>ha₂ : a ≠ 0<VAR>this : Function.Injective ⇑f<GOAL>IsIntegral R (f ⟨x, hx⟩)
<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>M : Type u_5<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module A M<VAR>inst✝¹ : IsScalarTower R A M<VAR>inst✝ : NoZeroSMulDivisors A M<VAR>N : Submodule R M<VAR>hN : N ≠ ⊥<VAR>hN' : N.FG<VAR>x : A<VAR>hx : ∀ n ∈ N, x • n ∈ N<VAR>A' : Subalgebra R A := { carrier := {x | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }<VAR>f : ↥A' →ₐ[R] Module.End R ↥N := AlgHom.ofLinearMap { toFun := fun x => (DistribMulAction.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯<VAR>a : M<VAR>ha₁ : a ∈ N<VAR>ha₂ : a ≠ 0<VAR>this✝ : Function.Injective ⇑f<VAR>this : Module.Finite R ↥N<GOAL>IsIntegral R (f ⟨x, hx⟩)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>f✝ : E → F<VAR>φ : E → ℝ<VAR>x₀ : E<VAR>f'✝ : E →L[ℝ] F<VAR>φ' : E →L[ℝ] ℝ<VAR>ι : Type u_3<VAR>inst✝ : Fintype ι<VAR>f : ι → E → ℝ<VAR>f' : ι → E →L[ℝ] ℝ<VAR>hextr : IsLocalExtrOn φ {x | ∀ (i : ι), f i x = f i x₀} x₀<VAR>hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀<VAR>hφ' : HasStrictFDerivAt φ φ' x₀<VAR>this : DecidableEq ι := Classical.decEq ι<GOAL>∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0