ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>inst✝⁴ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>R : Type u_3<VAR>inst✝³ : (i : ι) → AddCommMonoid (A i)<VAR>inst✝² : AddMonoid ι<VAR>inst✝¹ : GSemiring A<VAR>inst✝ : Semiring R<VAR>F : (⨁ (i : ι), A i) →+* R<GOAL>(fun f => toSemiring (fun x => ↑f) ⋯ ⋯) ((fun F => ⟨fun {i} => (↑F).comp (of A i), ⋯⟩) F) = F
<VAR>ι : Type u_1<VAR>inst✝⁴ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>R : Type u_3<VAR>inst✝³ : (i : ι) → AddCommMonoid (A i)<VAR>inst✝² : AddMonoid ι<VAR>inst✝¹ : GSemiring A<VAR>inst✝ : Semiring R<VAR>F : (⨁ (i : ι), A i) →+* R<GOAL>(fun f => ↑f) ((fun f => toSemiring (fun x => ↑f) ⋯ ⋯) ((fun F => ⟨fun {i} => (↑F).comp (of A i), ⋯⟩) F)) = (fun f => ↑f) F
<VAR>ι : Type u_1<VAR>inst✝⁴ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>R : Type u_3<VAR>inst✝³ : (i : ι) → AddCommMonoid (A i)<VAR>inst✝² : AddMonoid ι<VAR>inst✝¹ : GSemiring A<VAR>inst✝ : Semiring R<VAR>F : (⨁ (i : ι), A i) →+* R<VAR>xi : ι<VAR>xv : A xi<GOAL>(((fun f => ↑f) ((fun f => toSemiring (fun x => ↑f) ⋯ ⋯) ((fun F => ⟨fun {i} => (↑F).comp (of A i), ⋯⟩) F))).comp (of A xi)) xv = (((fun f => ↑f) F).comp (of A xi)) xv
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>a⁻¹ ≤ b ↔ b⁻¹ ≤ a
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>s : ℕ → Set Ω<VAR>hs : ∀ (n : ℕ), MeasurableSet (s n)<GOAL>∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) atTop atTop ↔ Tendsto (fun n => ∑ k ∈ Finset.range n, (μ[(s (k + 1)).indicator 1|↑ℱ k]) ω) atTop atTop
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>s : ℕ → Set Ω<VAR>hs : ∀ (n : ℕ), MeasurableSet (s n)<VAR>this : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => process s n ω) atTop atTop ↔ Tendsto (fun n => predictablePart (process s) ℱ μ n ω) atTop atTop<GOAL>∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) atTop atTop ↔ Tendsto (fun n => ∑ k ∈ Finset.range n, (μ[(s (k + 1)).indicator 1|↑ℱ k]) ω) atTop atTop
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω✝ : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>s : ℕ → Set Ω<VAR>hs : ∀ (n : ℕ), MeasurableSet (s n)<VAR>ω : Ω<VAR>n : ℕ<GOAL>process s n ω ≤ process s (n + 1) ω
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>s : ℕ → Set Ω<VAR>hs : ∀ (n : ℕ), MeasurableSet (s n)<VAR>this : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => (∑ k ∈ Finset.range n, (s (k + 1)).indicator 1) ω) atTop atTop ↔ Tendsto (fun n => (∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1|↑ℱ k]) ω) atTop atTop<GOAL>∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) atTop atTop ↔ Tendsto (fun n => ∑ k ∈ Finset.range n, (μ[(s (k + 1)).indicator 1|↑ℱ k]) ω) atTop atTop
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>hC : IsClosed C<VAR>f : LocallyConstant ↑C ℤ<GOAL>∃ s g, f = LocallyConstant.comap { toFun := ProjRestrict C fun x => x ∈ s, continuous_toFun := ⋯ } g
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>hC : IsClosed C<VAR>f : LocallyConstant ↑C ℤ<VAR>J : (Finset I)ᵒᵖ<VAR>g : LocallyConstant ↑((spanFunctor ⋯).obj J).toTop ℤ<VAR>h : f = LocallyConstant.comap ((spanCone ⋯).π.app J) g<GOAL>∃ s g, f = LocallyConstant.comap { toFun := ProjRestrict C fun x => x ∈ s, continuous_toFun := ⋯ } g
<VAR>R : Type u_1<VAR>inst✝ : OrderedSemiring R<VAR>a : R<VAR>Hsq : 0 ≤ a * a<VAR>Hsq' : 0 ≤ (1 + a) * (1 + a)<VAR>H : 0 ≤ 2 + a<VAR>n : ℕ<VAR>this : 0 ≤ ↑n * (a * a * (2 + a)) + a * a<GOAL>1 + ↑(n + 2) * a + (↑n * (a * a * (2 + a)) + a * a) = (1 + a) * (1 + a) * (1 + ↑n * a)
<VAR>R : Type u_1<VAR>inst✝ : OrderedSemiring R<VAR>a : R<VAR>Hsq : 0 ≤ a * a<VAR>Hsq' : 0 ≤ (1 + a) * (1 + a)<VAR>H : 0 ≤ 2 + a<VAR>n : ℕ<VAR>this : 0 ≤ ↑n * (a * a * (2 + a)) + a * a<GOAL>1 + (↑n * a + (a + (a + (↑n * (a * a) + (↑n * (a * a) + (↑n * (a * a * a) + a * a)))))) = 1 + (a + (a + (a * a + (↑n * a + (a * (↑n * a) + (a * (↑n * a) + a * a * (↑n * a)))))))
<VAR>R : Type u_1<VAR>inst✝ : OrderedSemiring R<VAR>a : R<VAR>Hsq : 0 ≤ a * a<VAR>Hsq' : 0 ≤ (1 + a) * (1 + a)<VAR>H : 0 ≤ 2 + a<VAR>n : ℕ<VAR>this : 0 ≤ ↑n * (a * a * (2 + a)) + a * a<GOAL>↑n * a + 1 + a + a + ↑n * (a * a) + ↑n * (a * a) + ↑n * (a * a * a) + a * a = ↑n * a + 1 + a + a + a * a + a * (↑n * a) + a * (↑n * a) + a * a * (↑n * a)
<VAR>R : Type u_1<VAR>inst✝ : OrderedSemiring R<VAR>a : R<VAR>Hsq : 0 ≤ a * a<VAR>Hsq' : 0 ≤ (1 + a) * (1 + a)<VAR>H : 0 ≤ 2 + a<VAR>n : ℕ<VAR>this : 0 ≤ ↑n * (a * a * (2 + a)) + a * a<GOAL>↑n * a + (1 + (a + (a + (a * (↑n * a) + (a * (↑n * a) + (a * a * (↑n * a) + a * a)))))) = ↑n * a + (1 + (a + (a + (a * a + (a * (↑n * a) + (a * (↑n * a) + a * a * (↑n * a)))))))
<VAR>R : Type u_1<VAR>inst✝ : OrderedSemiring R<VAR>a : R<VAR>Hsq : 0 ≤ a * a<VAR>Hsq' : 0 ≤ (1 + a) * (1 + a)<VAR>H : 0 ≤ 2 + a<VAR>n : ℕ<VAR>this : 0 ≤ ↑n * (a * a * (2 + a)) + a * a<GOAL>(1 + a) * (1 + a) * (1 + a) ^ n = (1 + a) ^ (n + 2)
<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>f : α ≃ β<VAR>a : α<VAR>b : M<GOAL>equivMapDomain f (single a b) = single (f a) b
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝² : Fintype m<VAR>inst✝¹ : Fintype n<VAR>inst✝ : NonUnitalNonAssocRing α<VAR>u v w : m → α<GOAL>-v ⬝ᵥ -w = v ⬝ᵥ w
<VAR>α : Type<VAR>n : ℕ<VAR>β : Type<VAR>xs : Vector α n<VAR>ys : Vector β n<VAR>σ γ : Type<VAR>f : α → β → σ → σ × γ<VAR>s₀ : σ<VAR>S : Set σ<VAR>h₀ : s₀ ∈ S<VAR>closure : ∀ (a : α) (b : β), ∀ s ∈ S, (f a b s).1 ∈ S<VAR>out : ∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).2 = (f a b s').2<GOAL>(mapAccumr₂ f xs ys s₀).2 = map₂ (fun x x_1 => (f x x_1 s₀).2) xs ys
<VAR>α : Type<VAR>n : ℕ<VAR>β : Type<VAR>xs : Vector α n<VAR>ys : Vector β n<VAR>σ γ : Type<VAR>f : α → β → σ → σ × γ<VAR>s₀ : σ<VAR>S : Set σ<VAR>h₀ : s₀ ∈ S<VAR>closure : ∀ (a : α) (b : β), ∀ s ∈ S, (f a b s).1 ∈ S<VAR>out : ∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).2 = (f a b s').2<GOAL>(mapAccumr₂ f xs ys s₀).2 = (mapAccumr₂ (fun x y x_1 => ((), (f x y s₀).2)) xs ys ()).2
<VAR>α : Type<VAR>n : ℕ<VAR>β : Type<VAR>xs : Vector α n<VAR>ys : Vector β n<VAR>σ γ : Type<VAR>f : α → β → σ → σ × γ<VAR>s₀ : σ<VAR>S : Set σ<VAR>h₀ : s₀ ∈ S<VAR>closure : ∀ (a : α) (b : β), ∀ s ∈ S, (f a b s).1 ∈ S<VAR>out : ∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).2 = (f a b s').2<GOAL>∃ R, R s₀ () ∧ ∀ {s : σ} {q : Unit} (a : α) (b : β), R s q → R (f a b s).1 ((), (f a b s₀).2).1 ∧ (f a b s).2 = ((), (f a b s₀).2).2
<VAR>α : Type<VAR>n : ℕ<VAR>β : Type<VAR>xs : Vector α n<VAR>ys : Vector β n<VAR>σ γ : Type<VAR>f : α → β → σ → σ × γ<VAR>s₀ : σ<VAR>S : Set σ<VAR>h₀ : s₀ ∈ S<VAR>closure : ∀ (a : α) (b : β), ∀ s ∈ S, (f a b s).1 ∈ S<VAR>out : ∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).2 = (f a b s').2<GOAL>∀ {s : σ} {q : Unit} (a : α) (b : β), s ∈ S → (f a b s).1 ∈ S ∧ (f a b s).2 = ((), (f a b s₀).2).2
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : SMul R S<VAR>inst✝² : Module S M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsScalarTower R S M<VAR>h : IsNoetherian R M<GOAL>IsNoetherian S M
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : SMul R S<VAR>inst✝² : Module S M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsScalarTower R S M<VAR>h : WellFounded fun x x_1 => x > x_1<GOAL>WellFounded fun x x_1 => x > x_1
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>inst✝ : Field k<VAR>s : σ<GOAL>(X s)⁻¹ = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : CompleteSpace E<GOAL>Kᗮᗮᗮ = Kᗮ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : CompleteSpace E<GOAL>Kᗮ.topologicalClosure = Kᗮ
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace α'<VAR>inst✝² : One β<VAR>inst✝¹ : One γ<VAR>inst✝ : One δ<VAR>g : β → γ<VAR>f : α → β<VAR>f₂ : α → γ<VAR>m : β → γ → δ<VAR>x : α<VAR>hf : HasCompactMulSupport f<VAR>hf₂ : HasCompactMulSupport f₂<VAR>hm : m 1 1 = 1<GOAL>HasCompactMulSupport fun x => m (f x) (f₂ x)
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace α'<VAR>inst✝² : One β<VAR>inst✝¹ : One γ<VAR>inst✝ : One δ<VAR>g : β → γ<VAR>f : α → β<VAR>f₂ : α → γ<VAR>m : β → γ → δ<VAR>x : α<VAR>hf : f =ᶠ[coclosedCompact α] 1<VAR>hf₂ : f₂ =ᶠ[coclosedCompact α] 1<VAR>hm : m 1 1 = 1<GOAL>(fun x => m (f x) (f₂ x)) =ᶠ[coclosedCompact α] 1
<VAR>n : ℕ<VAR>x✝ : 0 ≤ n<GOAL>(n - 0)! * n.descFactorial 0 = n !
<VAR>k : ℕ<VAR>h : k.succ ≤ 0<GOAL>False
<VAR>n k : ℕ<VAR>h : k.succ ≤ n.succ<GOAL>(n.succ - k.succ)! * n.succ.descFactorial k.succ = n.succ !
<VAR>d : ℤ<VAR>hd : d ≤ 0<VAR>n : ℤ√d<GOAL>0 ≤ -(d * n.im * n.im)
<VAR>d : ℤ<VAR>hd : d ≤ 0<VAR>n : ℤ√d<GOAL>0 ≤ -d * (n.im * n.im)
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁷ : AddCommGroup E<VAR>inst✝¹⁶ : Module 𝕜 E<VAR>inst✝¹⁵ : TopologicalSpace E<VAR>inst✝¹⁴ : TopologicalAddGroup E<VAR>inst✝¹³ : ContinuousSMul 𝕜 E<VAR>F : Type w<VAR>inst✝¹² : AddCommGroup F<VAR>inst✝¹¹ : Module 𝕜 F<VAR>inst✝¹⁰ : TopologicalSpace F<VAR>inst✝⁹ : TopologicalAddGroup F<VAR>inst✝⁸ : ContinuousSMul 𝕜 F<VAR>F' : Type x<VAR>inst✝⁷ : AddCommGroup F'<VAR>inst✝⁶ : Module 𝕜 F'<VAR>inst✝⁵ : TopologicalSpace F'<VAR>inst✝⁴ : TopologicalAddGroup F'<VAR>inst✝³ : ContinuousSMul 𝕜 F'<VAR>inst✝² : CompleteSpace 𝕜<VAR>ι : Type u_1<VAR>inst✝¹ : Finite ι<VAR>inst✝ : T2Space E<VAR>v : Basis ι 𝕜 E<GOAL>Continuous (↑v.equivFun.symm).toFun
<VAR>α : Type u_1<VAR>A : Set α<VAR>β : Type u_2<VAR>inst✝³ : Zero β<VAR>inst✝² : TopologicalSpace β<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>As : ι → Set α<VAR>inst✝¹ : T1Space β<VAR>b : β<VAR>inst✝ : NeZero b<GOAL>Tendsto (fun i => (As i).indicator fun x => b) L (𝓝 (A.indicator fun x => b)) ↔ Tendsto As L (pi fun x => pure (x ∈ A))
<VAR>α : Type u_1<VAR>A : Set α<VAR>β : Type u_2<VAR>inst✝³ : Zero β<VAR>inst✝² : TopologicalSpace β<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>As : ι → Set α<VAR>inst✝¹ : T1Space β<VAR>b : β<VAR>inst✝ : NeZero b<GOAL>(∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), Tendsto (fun x => As x i) L (pure (i ∈ A))
<VAR>α : Type u_1<VAR>A : Set α<VAR>β : Type u_2<VAR>inst✝³ : Zero β<VAR>inst✝² : TopologicalSpace β<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>As : ι → Set α<VAR>inst✝¹ : T1Space β<VAR>b : β<VAR>inst✝ : NeZero b<GOAL>(∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), ∀ᶠ (x : ι) in L, As x i = (i ∈ A)
<VAR>a : ↥circle<VAR>h : rotation a = conjLIE<GOAL>False
<VAR>a : ↥circle<VAR>h : rotation a = conjLIE<VAR>h1 : (rotation a) 1 = (starRingEnd ℂ) 1<GOAL>False
<VAR>a : ↥circle<VAR>h : rotation a = conjLIE<VAR>h1 : (rotation a) 1 = (starRingEnd ℂ) 1<VAR>hI : (rotation a) I = (starRingEnd ℂ) I<GOAL>False
<VAR>a : ↥circle<VAR>h : rotation a = conjLIE<VAR>h1 : ↑a = 1<VAR>hI : (rotation a) I = (starRingEnd ℂ) I<GOAL>False
<VAR>a : ↥circle<VAR>h : rotation a = conjLIE<VAR>h1 : ↑a = 1<VAR>hI : 1 = 0<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>l : List α<VAR>x : α<VAR>xs : List α<VAR>n✝ : ℕ<VAR>d : α<VAR>r n : ℕ<GOAL>(replicate r d)[n]?.getD d = d
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>a b : α<VAR>h : b ≤ a<GOAL>variationOnFromTo f s a b = -(eVariationOn f (s ∩ Icc b a)).toReal
<VAR>x✝¹ y x : ℝ<VAR>x✝ : x ∈ univ<GOAL>log (-rexp x) = x
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>cs.IsLeftDescent w i ↔ ¬cs.IsLeftDescent (cs.simple i * w) i
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>cs.length (cs.simple i * w) + 1 = cs.length w ↔ cs.length w = cs.length (cs.simple i * w) + 1
<VAR>a b m n✝ p✝ p n : ℕ<VAR>IH : (Finset.filter (fun x => p ∣ x) (Ioc 0 n)).card = n / p<VAR>h1 : Ioc 0 n.succ = insert n.succ (Ioc 0 n)<GOAL>(Finset.filter (fun x => p ∣ x) (Ioc 0 (n + 1))).card = (n + 1) / p
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>n m : ℕ<VAR>hc : G.Colorable n<VAR>hm : n < m<GOAL>G.CliqueFree m
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>n m : ℕ<VAR>hc : G.Colorable n<VAR>hm : n < m<VAR>h : ¬G.CliqueFree m<GOAL>False
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>n m : ℕ<VAR>hc : G.Colorable n<VAR>hm : n < m<VAR>h : ∃ x, G.IsClique ↑x ∧ x.card = m<GOAL>False
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>n : ℕ<VAR>hc : G.Colorable n<VAR>s : Finset V<VAR>h : G.IsClique ↑s<VAR>hm : n < s.card<GOAL>False
<VAR>α : Type u_1<VAR>a y : Lists α<VAR>l : Lists' α true<GOAL>a ∈ cons y l ↔ a ~ y ∨ a ∈ l
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s✝ : Set E<VAR>s_conv✝ : Convex ℝ s✝<VAR>f✝ : E → F<VAR>f'✝ : E → E →L[ℝ] F<VAR>f''✝ : E →L[ℝ] E →L[ℝ] F<VAR>hf✝ : ∀ x ∈ interior s✝, HasFDerivAt f✝ (f'✝ x) x<VAR>x✝ : E<VAR>xs✝ : x✝ ∈ s✝<VAR>hx✝ : HasFDerivWithinAt f'✝ f''✝ (interior s✝) x✝<VAR>s : Set E<VAR>s_conv : Convex ℝ s<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x<VAR>x : E<VAR>xs : x ∈ s<VAR>hx : HasFDerivWithinAt f' f'' (interior s) x<VAR>v w y : E<VAR>hy : y ∈ interior s<VAR>z : E<VAR>hz : z = (1 / 4) • (y - x)<GOAL>(f'' v) w = (f'' w) v
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s✝ : Set E<VAR>s_conv✝ : Convex ℝ s✝<VAR>f✝ : E → F<VAR>f'✝ : E → E →L[ℝ] F<VAR>f''✝ : E →L[ℝ] E →L[ℝ] F<VAR>hf✝ : ∀ x ∈ interior s✝, HasFDerivAt f✝ (f'✝ x) x<VAR>x✝ : E<VAR>xs✝ : x✝ ∈ s✝<VAR>hx✝ : HasFDerivWithinAt f'✝ f''✝ (interior s✝) x✝<VAR>s : Set E<VAR>s_conv : Convex ℝ s<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x<VAR>x : E<VAR>xs : x ∈ s<VAR>hx : HasFDerivWithinAt f' f'' (interior s) x<VAR>v w y : E<VAR>hy : y ∈ interior s<VAR>z : E<VAR>hz : z = (1 / 4) • (y - x)<VAR>A : ∀ (m : E), Filter.Tendsto (fun t => x + 4 • (z + t • m)) (𝓝 0) (𝓝 y)<GOAL>(f'' v) w = (f'' w) v
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s✝ : Set E<VAR>s_conv✝ : Convex ℝ s✝<VAR>f✝ : E → F<VAR>f'✝ : E → E →L[ℝ] F<VAR>f''✝ : E →L[ℝ] E →L[ℝ] F<VAR>hf✝ : ∀ x ∈ interior s✝, HasFDerivAt f✝ (f'✝ x) x<VAR>x✝ : E<VAR>xs✝ : x✝ ∈ s✝<VAR>hx✝ : HasFDerivWithinAt f'✝ f''✝ (interior s✝) x✝<VAR>s : Set E<VAR>s_conv : Convex ℝ s<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x<VAR>x : E<VAR>xs : x ∈ s<VAR>hx : HasFDerivWithinAt f' f'' (interior s) x<VAR>v w y : E<VAR>hy : y ∈ interior s<VAR>z : E<VAR>hz : z = (1 / 4) • (y - x)<VAR>A : ∀ (m : E), Filter.Tendsto (fun t => x + 4 • (z + t • m)) (𝓝 0) (𝓝 y)<VAR>B : ∀ (m : E), ∀ᶠ (t : ℝ) in 𝓝[>] 0, x + 4 • (z + t • m) ∈ interior s<GOAL>(f'' v) w = (f'' w) v
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s✝ : Set E<VAR>s_conv✝ : Convex ℝ s✝<VAR>f✝ : E → F<VAR>f'✝ : E → E →L[ℝ] F<VAR>f''✝ : E →L[ℝ] E →L[ℝ] F<VAR>hf✝ : ∀ x ∈ interior s✝, HasFDerivAt f✝ (f'✝ x) x<VAR>x✝ : E<VAR>xs✝ : x✝ ∈ s✝<VAR>hx✝ : HasFDerivWithinAt f'✝ f''✝ (interior s✝) x✝<VAR>s : Set E<VAR>s_conv : Convex ℝ s<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x<VAR>x : E<VAR>xs : x ∈ s<VAR>hx : HasFDerivWithinAt f' f'' (interior s) x<VAR>v w y : E<VAR>hy : y ∈ interior s<VAR>z : E<VAR>hz : z = (1 / 4) • (y - x)<VAR>A : ∀ (m : E), Filter.Tendsto (fun t => x + 4 • (z + t • m)) (𝓝 0) (𝓝 y)<VAR>B : ∀ (m : E), ∀ᶠ (t : ℝ) in 𝓝[>] 0, x + 4 • (z + t • m) ∈ interior s<VAR>t : E → ℝ<VAR>ts : ∀ (m : E), x + 4 • (z + t m • m) ∈ interior s<VAR>tpos : ∀ (m : E), 0 < t m<GOAL>(f'' v) w = (f'' w) v
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s✝ : Set E<VAR>s_conv✝ : Convex ℝ s✝<VAR>f✝ : E → F<VAR>f'✝ : E → E →L[ℝ] F<VAR>f''✝ : E →L[ℝ] E →L[ℝ] F<VAR>hf✝ : ∀ x ∈ interior s✝, HasFDerivAt f✝ (f'✝ x) x<VAR>x✝ : E<VAR>xs✝ : x✝ ∈ s✝<VAR>hx✝ : HasFDerivWithinAt f'✝ f''✝ (interior s✝) x✝<VAR>s : Set E<VAR>s_conv : Convex ℝ s<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x<VAR>x : E<VAR>xs : x ∈ s<VAR>hx : HasFDerivWithinAt f' f'' (interior s) x<VAR>v w y : E<VAR>hy : y ∈ interior s<VAR>z : E<VAR>hz : z = (1 / 4) • (y - x)<VAR>A : ∀ (m : E), Filter.Tendsto (fun t => x + 4 • (z + t • m)) (𝓝 0) (𝓝 y)<VAR>B : ∀ (m : E), ∀ᶠ (t : ℝ) in 𝓝[>] 0, x + 4 • (z + t • m) ∈ interior s<VAR>t : E → ℝ<VAR>ts : ∀ (m : E), x + 4 • (z + t m • m) ∈ interior s<VAR>tpos : ∀ (m : E), 0 < t m<VAR>C : ∀ (m : E), (f'' m) z = (f'' z) m<GOAL>(f'' v) w = (f'' w) v
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s✝ : Set E<VAR>s_conv✝ : Convex ℝ s✝<VAR>f✝ : E → F<VAR>f'✝ : E → E →L[ℝ] F<VAR>f''✝ : E →L[ℝ] E →L[ℝ] F<VAR>hf✝ : ∀ x ∈ interior s✝, HasFDerivAt f✝ (f'✝ x) x<VAR>x✝ : E<VAR>xs✝ : x✝ ∈ s✝<VAR>hx✝ : HasFDerivWithinAt f'✝ f''✝ (interior s✝) x✝<VAR>s : Set E<VAR>s_conv : Convex ℝ s<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x<VAR>x : E<VAR>xs : x ∈ s<VAR>hx : HasFDerivWithinAt f' f'' (interior s) x<VAR>v w y : E<VAR>hy : y ∈ interior s<VAR>z : E<VAR>hz : z = (1 / 4) • (y - x)<VAR>A : ∀ (m : E), Filter.Tendsto (fun t => x + 4 • (z + t • m)) (𝓝 0) (𝓝 y)<VAR>B : ∀ (m : E), ∀ᶠ (t : ℝ) in 𝓝[>] 0, x + 4 • (z + t • m) ∈ interior s<VAR>t : E → ℝ<VAR>ts : ∀ (m : E), x + 4 • (z + t m • m) ∈ interior s<VAR>tpos : ∀ (m : E), 0 < t m<VAR>C : ∀ (m : E), (f'' m) z = (f'' z) m<VAR>this : (f'' (z + t v • v)) (z + t w • w) = (f'' (z + t w • w)) (z + t v • v)<GOAL>(f'' v) w = (f'' w) v
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s✝ : Set E<VAR>s_conv✝ : Convex ℝ s✝<VAR>f✝ : E → F<VAR>f'✝ : E → E →L[ℝ] F<VAR>f''✝ : E →L[ℝ] E →L[ℝ] F<VAR>hf✝ : ∀ x ∈ interior s✝, HasFDerivAt f✝ (f'✝ x) x<VAR>x✝ : E<VAR>xs✝ : x✝ ∈ s✝<VAR>hx✝ : HasFDerivWithinAt f'✝ f''✝ (interior s✝) x✝<VAR>s : Set E<VAR>s_conv : Convex ℝ s<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x<VAR>x : E<VAR>xs : x ∈ s<VAR>hx : HasFDerivWithinAt f' f'' (interior s) x<VAR>v w y : E<VAR>hy : y ∈ interior s<VAR>z : E<VAR>hz : z = (1 / 4) • (y - x)<VAR>A : ∀ (m : E), Filter.Tendsto (fun t => x + 4 • (z + t • m)) (𝓝 0) (𝓝 y)<VAR>B : ∀ (m : E), ∀ᶠ (t : ℝ) in 𝓝[>] 0, x + 4 • (z + t • m) ∈ interior s<VAR>t : E → ℝ<VAR>ts : ∀ (m : E), x + 4 • (z + t m • m) ∈ interior s<VAR>tpos : ∀ (m : E), 0 < t m<VAR>C : ∀ (m : E), (f'' m) z = (f'' z) m<VAR>this : (f'' z) z + t v • (f'' z) v + (t w • (f'' z) w + (t w * t v) • (f'' v) w) = (f'' z) z + t w • (f'' z) w + (t v • (f'' z) v + (t v * t w) • (f'' w) v)<GOAL>(f'' v) w = (f'' w) v
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s✝ : Set E<VAR>s_conv✝ : Convex ℝ s✝<VAR>f✝ : E → F<VAR>f'✝ : E → E →L[ℝ] F<VAR>f''✝ : E →L[ℝ] E →L[ℝ] F<VAR>hf✝ : ∀ x ∈ interior s✝, HasFDerivAt f✝ (f'✝ x) x<VAR>x✝ : E<VAR>xs✝ : x✝ ∈ s✝<VAR>hx✝ : HasFDerivWithinAt f'✝ f''✝ (interior s✝) x✝<VAR>s : Set E<VAR>s_conv : Convex ℝ s<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x<VAR>x : E<VAR>xs : x ∈ s<VAR>hx : HasFDerivWithinAt f' f'' (interior s) x<VAR>v w y : E<VAR>hy : y ∈ interior s<VAR>z : E<VAR>hz : z = (1 / 4) • (y - x)<VAR>A : ∀ (m : E), Filter.Tendsto (fun t => x + 4 • (z + t • m)) (𝓝 0) (𝓝 y)<VAR>B : ∀ (m : E), ∀ᶠ (t : ℝ) in 𝓝[>] 0, x + 4 • (z + t • m) ∈ interior s<VAR>t : E → ℝ<VAR>ts : ∀ (m : E), x + 4 • (z + t m • m) ∈ interior s<VAR>tpos : ∀ (m : E), 0 < t m<VAR>C : ∀ (m : E), (f'' m) z = (f'' z) m<VAR>this : (t v * t w) • (f'' v) w = (t v * t w) • (f'' w) v<GOAL>(f'' v) w = (f'' w) v
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s✝ : Set E<VAR>s_conv✝ : Convex ℝ s✝<VAR>f✝ : E → F<VAR>f'✝ : E → E →L[ℝ] F<VAR>f''✝ : E →L[ℝ] E →L[ℝ] F<VAR>hf✝ : ∀ x ∈ interior s✝, HasFDerivAt f✝ (f'✝ x) x<VAR>x✝ : E<VAR>xs✝ : x✝ ∈ s✝<VAR>hx✝ : HasFDerivWithinAt f'✝ f''✝ (interior s✝) x✝<VAR>s : Set E<VAR>s_conv : Convex ℝ s<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x<VAR>x : E<VAR>xs : x ∈ s<VAR>hx : HasFDerivWithinAt f' f'' (interior s) x<VAR>v w y : E<VAR>hy : y ∈ interior s<VAR>z : E<VAR>hz : z = (1 / 4) • (y - x)<VAR>A : ∀ (m : E), Filter.Tendsto (fun t => x + 4 • (z + t • m)) (𝓝 0) (𝓝 y)<VAR>B : ∀ (m : E), ∀ᶠ (t : ℝ) in 𝓝[>] 0, x + 4 • (z + t • m) ∈ interior s<VAR>t : E → ℝ<VAR>ts : ∀ (m : E), x + 4 • (z + t m • m) ∈ interior s<VAR>tpos : ∀ (m : E), 0 < t m<VAR>C : ∀ (m : E), (f'' m) z = (f'' z) m<VAR>this : (t v * t w) • (f'' v) w = (t v * t w) • (f'' w) v<GOAL>t v * t w ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u}<GOAL>o ≤ lsub (typein fun x x_1 => x < x_1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u}<VAR>h : lsub (typein fun x x_1 => x < x_1) < o<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u}<VAR>h : lsub (typein fun x x_1 => x < x_1) < type fun x x_1 => x < x_1<GOAL>False
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>n : ℤ<VAR>A : M<VAR>h : IsUnit A.det<GOAL>A ^ (-n) * A ^ n = 1
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝³ : Preorder β<VAR>f✝ g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>γ : Type u_3<VAR>inst✝² : LinearOrder γ<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : OrderTopology γ<VAR>f : α → γ<GOAL>ContinuousOn f s ↔ LowerSemicontinuousOn f s ∧ UpperSemicontinuousOn f s