ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>inst✝¹ : IsMarkovKernel κ<VAR>η : Kernel α γ<VAR>inst✝ : IsSFiniteKernel η<VAR>x : α<VAR>s✝ : Set γ<VAR>a✝ : MeasurableSet s✝<GOAL>((κ ×ₖ η).snd x) s✝ = (η x) s✝
<VAR>x y : ℝ<GOAL>arccos (-1) = π
<VAR>J : Type v<VAR>inst✝² : Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>inst✝¹ : IsFilteredOrEmpty J<VAR>inst✝ : HasColimit F<VAR>t : Cocone F<VAR>ht : IsColimit t<VAR>i j : J<VAR>xi : F.obj i<VAR>xj : F.obj j<GOAL>t.ι.app i xi = t.ι.app j xj ↔ ∃ k f g, F.map f xi = F.map g xj
<VAR>J : Type v<VAR>inst✝² : Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>inst✝¹ : IsFilteredOrEmpty J<VAR>inst✝ : HasColimit F<VAR>t : Cocone F<VAR>ht : IsColimit t<VAR>i j : J<VAR>xi : F.obj i<VAR>xj : F.obj j<GOAL>t.ι.app i xi = t.ι.app j xj ↔ (colimitCocone F).ι.app i xi = (colimitCocone F).ι.app j xj
<VAR>J : Type v<VAR>inst✝² : Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>inst✝¹ : IsFilteredOrEmpty J<VAR>inst✝ : HasColimit F<VAR>t : Cocone F<VAR>ht : IsColimit t<VAR>i j : J<VAR>xi : F.obj i<VAR>xj : F.obj j<GOAL>(ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)).toEquiv (t.ι.app i xi) = (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)).toEquiv (t.ι.app j xj) ↔ (colimitCocone F).ι.app i xi = (colimitCocone F).ι.app j xj
<VAR>J : Type v<VAR>inst✝² : Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>inst✝¹ : IsFilteredOrEmpty J<VAR>inst✝ : HasColimit F<VAR>t : Cocone F<VAR>ht : IsColimit t<VAR>i j : J<VAR>xi : F.obj i<VAR>xj : F.obj j<VAR>e_1✝ : ((Functor.const J).obj (colimitCocone F).pt).obj i = (colimitCocone F).pt<GOAL>(colimitCocone F).ι.app i xi = (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)).toEquiv (t.ι.app i xi)
<VAR>J : Type v<VAR>inst✝² : Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>inst✝¹ : IsFilteredOrEmpty J<VAR>inst✝ : HasColimit F<VAR>t : Cocone F<VAR>ht : IsColimit t<VAR>i j : J<VAR>xi : F.obj i<VAR>xj : F.obj j<VAR>e_1✝ : ((Functor.const J).obj (colimitCocone F).pt).obj i = (colimitCocone F).pt<GOAL>(colimitCocone F).ι.app j xj = (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)).toEquiv (t.ι.app j xj)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : SemilatticeSup α<VAR>inst✝⁴ : OrderTop α<VAR>inst✝³ : DecidableRel fun x x_1 => x ≤ x_1<VAR>inst✝² : SemilatticeSup β<VAR>inst✝¹ : BoundedOrder β<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s✝ t : Finset α<VAR>a✝ b : α<VAR>e : α ≃o β<VAR>s : Finset α<VAR>a : α<VAR>this : e a ∈ lowerClosure ↑(map e.toEmbedding s) ↔ a ∈ lowerClosure ↑s<GOAL>e (s.truncatedSup a) = (map e.toEmbedding s).truncatedSup (e a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : SemilatticeSup α<VAR>inst✝⁴ : OrderTop α<VAR>inst✝³ : DecidableRel fun x x_1 => x ≤ x_1<VAR>inst✝² : SemilatticeSup β<VAR>inst✝¹ : BoundedOrder β<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s✝ t : Finset α<VAR>a✝ b : α<VAR>e : α ≃o β<VAR>s : Finset α<VAR>a : α<VAR>this : e a ∈ lowerClosure ↑(map e.toEmbedding s) ↔ a ∈ lowerClosure ↑s<GOAL>(if h : a ∈ lowerClosure ↑s then (filter (fun b => a ≤ b) s).sup' ⋯ (⇑e ∘ id) else ⊤) = if h : a ∈ lowerClosure ↑s then (filter (fun b => e a ≤ b) (map e.toEmbedding s)).sup' ⋯ id else ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : SemilatticeSup α<VAR>inst✝⁴ : OrderTop α<VAR>inst✝³ : DecidableRel fun x x_1 => x ≤ x_1<VAR>inst✝² : SemilatticeSup β<VAR>inst✝¹ : BoundedOrder β<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s✝ t : Finset α<VAR>a✝ b : α<VAR>e : α ≃o β<VAR>s : Finset α<VAR>a : α<VAR>this : e a ∈ lowerClosure ↑(map e.toEmbedding s) ↔ a ∈ lowerClosure ↑s<VAR>h : a ∈ lowerClosure ↑s<GOAL>(filter (fun b => a ≤ b) s).sup' ⋯ (⇑e ∘ id) = (filter (fun b => e a ≤ b) (map e.toEmbedding s)).sup' ⋯ id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : SemilatticeSup α<VAR>inst✝⁴ : OrderTop α<VAR>inst✝³ : DecidableRel fun x x_1 => x ≤ x_1<VAR>inst✝² : SemilatticeSup β<VAR>inst✝¹ : BoundedOrder β<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s✝ t : Finset α<VAR>a✝ b : α<VAR>e : α ≃o β<VAR>s : Finset α<VAR>a : α<VAR>this : e a ∈ lowerClosure ↑(map e.toEmbedding s) ↔ a ∈ lowerClosure ↑s<VAR>h : a ∈ lowerClosure ↑s<GOAL>((filter (fun b => a ≤ b) s).sup' ⋯ fun x => e x) = (map e.toEmbedding (filter (fun x => a ≤ x) s)).sup' ⋯ fun x => x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : SemilatticeSup α<VAR>inst✝⁴ : OrderTop α<VAR>inst✝³ : DecidableRel fun x x_1 => x ≤ x_1<VAR>inst✝² : SemilatticeSup β<VAR>inst✝¹ : BoundedOrder β<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s✝ t : Finset α<VAR>a✝ b : α<VAR>e : α ≃o β<VAR>s : Finset α<VAR>a : α<VAR>this : e a ∈ lowerClosure ↑(map e.toEmbedding s) ↔ a ∈ lowerClosure ↑s<VAR>h : a ∈ lowerClosure ↑s<GOAL>((filter (fun b => a ≤ b) s).sup' ⋯ fun x => e x) = (filter (fun x => a ≤ x) s).sup' ⋯ ((fun x => x) ∘ ⇑e.toEmbedding)
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<GOAL>IsCoprime I J ↔ I + J = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>m : Set (Measure α)<VAR>h : ∀ μ' ∈ m, μ ≤ μ'<VAR>this : μ.toOuterMeasure ≤ sInf (toOuterMeasure '' m)<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>μ s ≤ (sInf m) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>m : Set (Measure α)<VAR>h : ∀ μ' ∈ m, μ ≤ μ'<VAR>this : μ.toOuterMeasure ≤ sInf (toOuterMeasure '' m)<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>μ s ≤ (sInf (toOuterMeasure '' m)) s
<VAR>α : Sort u_2<VAR>inst✝ : DecidableEq α<VAR>β : Sort u_1<VAR>v : α → β<VAR>i j : α<VAR>hv : v i = v j<VAR>k : α<VAR>hi : ¬k = i<VAR>hj : ¬k = j<GOAL>v ((swap i j) k) = v k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ ν μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure ν<VAR>inst✝ : ν.HaveLebesgueDecomposition μ<VAR>r : ℝ≥0∞<VAR>hr : r ≠ ⊤<GOAL>(r • ν).rnDeriv μ =ᶠ[ae μ] r • ν.rnDeriv μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ ν μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure ν<VAR>inst✝ : ν.HaveLebesgueDecomposition μ<VAR>r : ℝ≥0∞<VAR>hr : r ≠ ⊤<VAR>h : (r.toNNReal • ν).rnDeriv μ =ᶠ[ae μ] r.toNNReal • ν.rnDeriv μ<GOAL>(r • ν).rnDeriv μ =ᶠ[ae μ] r • ν.rnDeriv μ
<VAR>α : Type u<VAR>α' : Type u_1<VAR>β✝ : Type v<VAR>β' : Type u_2<VAR>γ✝ : Type u_3<VAR>φ : Type u_4<VAR>inst✝⁵ : OmegaCompletePartialOrder α<VAR>inst✝⁴ : OmegaCompletePartialOrder β✝<VAR>inst✝³ : OmegaCompletePartialOrder γ✝<VAR>inst✝² : OmegaCompletePartialOrder φ<VAR>inst✝¹ : OmegaCompletePartialOrder α'<VAR>inst✝ : OmegaCompletePartialOrder β'<VAR>β γ : Type v<VAR>f : α → Part (β → γ)<VAR>g : α → Part β<VAR>hf : Continuous' f<VAR>hg : Continuous' g<GOAL>Continuous' fun x => Seq.seq (f x) fun x_1 => g x
<VAR>α : Type u<VAR>α' : Type u_1<VAR>β✝ : Type v<VAR>β' : Type u_2<VAR>γ✝ : Type u_3<VAR>φ : Type u_4<VAR>inst✝⁵ : OmegaCompletePartialOrder α<VAR>inst✝⁴ : OmegaCompletePartialOrder β✝<VAR>inst✝³ : OmegaCompletePartialOrder γ✝<VAR>inst✝² : OmegaCompletePartialOrder φ<VAR>inst✝¹ : OmegaCompletePartialOrder α'<VAR>inst✝ : OmegaCompletePartialOrder β'<VAR>β γ : Type v<VAR>f : α → Part (β → γ)<VAR>g : α → Part β<VAR>hf : Continuous' f<VAR>hg : Continuous' g<GOAL>Continuous' fun x => do let x_1 ← f x x_1 <$> g x
<VAR>α : Type u<VAR>α' : Type u_1<VAR>β✝ : Type v<VAR>β' : Type u_2<VAR>γ✝ : Type u_3<VAR>φ : Type u_4<VAR>inst✝⁵ : OmegaCompletePartialOrder α<VAR>inst✝⁴ : OmegaCompletePartialOrder β✝<VAR>inst✝³ : OmegaCompletePartialOrder γ✝<VAR>inst✝² : OmegaCompletePartialOrder φ<VAR>inst✝¹ : OmegaCompletePartialOrder α'<VAR>inst✝ : OmegaCompletePartialOrder β'<VAR>β γ : Type v<VAR>f : α → Part (β → γ)<VAR>g : α → Part β<VAR>hf : Continuous' f<VAR>hg : Continuous' g<GOAL>Continuous' fun x x_1 => x_1 <$> g x
<VAR>α : Type u<VAR>α' : Type u_1<VAR>β✝ : Type v<VAR>β' : Type u_2<VAR>γ✝ : Type u_3<VAR>φ : Type u_4<VAR>inst✝⁵ : OmegaCompletePartialOrder α<VAR>inst✝⁴ : OmegaCompletePartialOrder β✝<VAR>inst✝³ : OmegaCompletePartialOrder γ✝<VAR>inst✝² : OmegaCompletePartialOrder φ<VAR>inst✝¹ : OmegaCompletePartialOrder α'<VAR>inst✝ : OmegaCompletePartialOrder β'<VAR>β γ : Type v<VAR>f : α → Part (β → γ)<VAR>g : α → Part β<VAR>hf : Continuous' f<VAR>hg : Continuous' g<GOAL>∀ (x : β → γ), Continuous' fun g_1 => x <$> g g_1
<VAR>α : Type u<VAR>α' : Type u_1<VAR>β✝ : Type v<VAR>β' : Type u_2<VAR>γ✝ : Type u_3<VAR>φ : Type u_4<VAR>inst✝⁵ : OmegaCompletePartialOrder α<VAR>inst✝⁴ : OmegaCompletePartialOrder β✝<VAR>inst✝³ : OmegaCompletePartialOrder γ✝<VAR>inst✝² : OmegaCompletePartialOrder φ<VAR>inst✝¹ : OmegaCompletePartialOrder α'<VAR>inst✝ : OmegaCompletePartialOrder β'<VAR>β γ : Type v<VAR>f : α → Part (β → γ)<VAR>g : α → Part β<VAR>hf : Continuous' f<VAR>hg : Continuous' g<VAR>x✝ : β → γ<GOAL>Continuous' fun g_1 => x✝ <$> g g_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ s₁ s₂ t t₁ t₂ u v : Finset α<VAR>a✝ b a : α<VAR>s : Finset α<VAR>H : a ∉ s<GOAL>∀ (x : α), x ∉ {a} ∩ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ s₁ s₂ t t₁ t₂ u v : Finset α<VAR>a✝ b a : α<VAR>s : Finset α<VAR>H : a ∉ s<GOAL>∀ (x : α), ¬(x = a ∧ x ∈ s)
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : (i : ι) → Zero (β i)<VAR>inst✝⁴ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>inst✝³ : (i : ι) → Zero (β₁ i)<VAR>inst✝² : (i : ι) → Zero (β₂ i)<VAR>inst✝¹ : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)<VAR>inst✝ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)<VAR>f : (i : ι) → β₁ i → β₂ i<VAR>hf : ∀ (i : ι), f i 0 = 0<VAR>g : Π₀ (i : ι), β₁ i<GOAL>(mapRange f hf g).support ⊆ g.support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : CompleteLattice α<VAR>f g : Filter β<VAR>p q : β → Prop<VAR>u v : β → α<VAR>inst✝ : CompleteLattice γ<VAR>e : α ≃o γ<GOAL>e (blimsup u f p) = blimsup (⇑e ∘ u) f p
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>a : 𝕜<GOAL>DifferentiableAt 𝕜 f (-a) ↔ DifferentiableAt 𝕜 (fun x => f (-x)) a
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>a : 𝕜<VAR>H : DifferentiableAt 𝕜 (fun x => f (-x)) a<GOAL>DifferentiableAt 𝕜 f (-a)
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>a : 𝕜<VAR>H : DifferentiableAt 𝕜 (fun x => f (-x)) a<GOAL>f = (fun x => f (-x)) ∘ Neg.neg
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>a : 𝕜<VAR>H : DifferentiableAt 𝕜 (fun x => f (-x)) a<VAR>x✝ : 𝕜<GOAL>f x✝ = ((fun x => f (-x)) ∘ Neg.neg) x✝
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<GOAL>⋃ x ∈ ↑s, f x '' ↑t = image2 f ↑s ↑t
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>inst✝ : Nonempty ι<VAR>H : ∀ (i : ι), IsNormal (f i)<VAR>a b : Ordinal.{max u v}<GOAL>(∃ i, nfpFamily f a ≤ f i b) ↔ nfpFamily f a ≤ b
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>inst✝ : Nonempty ι<VAR>H : ∀ (i : ι), IsNormal (f i)<VAR>a b : Ordinal.{max u v}<GOAL>(¬∃ i, nfpFamily f a ≤ f i b) ↔ ¬nfpFamily f a ≤ b
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>inst✝ : Nonempty ι<VAR>H : ∀ (i : ι), IsNormal (f i)<VAR>a b : Ordinal.{max u v}<GOAL>(∀ (i : ι), f i b < nfpFamily f a) ↔ b < nfpFamily f a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>b : β<VAR>s : Computation α<VAR>h : b ∈ map f s<GOAL>∃ a, a ∈ s ∧ f a = b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>b : β<VAR>s : Computation α<VAR>h : b ∈ s.bind (pure ∘ f)<GOAL>∃ a, a ∈ s ∧ f a = b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>b : β<VAR>s : Computation α<VAR>h : b ∈ s.bind (pure ∘ f)<VAR>a : α<VAR>as : a ∈ s<VAR>fb : b ∈ (pure ∘ f) a<GOAL>∃ a, a ∈ s ∧ f a = b
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁹ : LinearOrderedField R<VAR>inst✝⁸ : LinearOrderedField R'<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : LinearOrderedAddCommGroup α<VAR>inst✝⁴ : Module R E<VAR>inst✝³ : Module R F<VAR>inst✝² : Module R α<VAR>inst✝¹ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>inst✝ : Fintype ι<VAR>f : ι → R<GOAL>(convexHull R) (Set.range fun i j => if i = j then 1 else 0) = stdSimplex R ι
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁹ : LinearOrderedField R<VAR>inst✝⁸ : LinearOrderedField R'<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : LinearOrderedAddCommGroup α<VAR>inst✝⁴ : Module R E<VAR>inst✝³ : Module R F<VAR>inst✝² : Module R α<VAR>inst✝¹ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>inst✝ : Fintype ι<VAR>f : ι → R<GOAL>(Set.range fun i j => if i = j then 1 else 0) ⊆ stdSimplex R ι
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁹ : LinearOrderedField R<VAR>inst✝⁸ : LinearOrderedField R'<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : LinearOrderedAddCommGroup α<VAR>inst✝⁴ : Module R E<VAR>inst✝³ : Module R F<VAR>inst✝² : Module R α<VAR>inst✝¹ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>inst✝ : Fintype ι<VAR>f : ι → R<GOAL>stdSimplex R ι ⊆ (convexHull R) (Set.range fun i j => if i = j then 1 else 0)
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>N : Type u_3<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : Module R N<VAR>ι : Type u_4<VAR>inst✝⁴ : DecidableEq ι<VAR>S : Type u_5<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>i : ι<VAR>m : M<GOAL>(finsuppScalarRight R M ι).symm (Finsupp.single i m) = m ⊗ₜ[R] Finsupp.single i 1
<VAR>L : Language<VAR>α : Type w<VAR>M : Type w'<VAR>n : ℕ<VAR>inst✝³ : L.IsOrdered<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : Preorder M<VAR>inst✝ : L.OrderedStructure M<VAR>t₁ t₂ : L.Term (α ⊕ Fin n)<VAR>v : α → M<VAR>xs : Fin n → M<GOAL>(t₁.lt t₂).Realize v xs ↔ realize (Sum.elim v xs) t₁ < realize (Sum.elim v xs) t₂
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>ι : Sort u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>this : (mulSupport fun x => (fun x => 1) x.down) ⊆ ↑∅<GOAL>∏ᶠ (x : α), 1 = 1
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<VAR>hn : n ≠ 1<VAR>h0 : ¬n = 0<GOAL>bernoulli n = bernoulli' n
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<VAR>hn : n ≠ 1<VAR>h0 : ¬n = 0<GOAL>(-1) ^ (n % 2) * bernoulli' n = bernoulli' n
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<VAR>hn : n ≠ 1<VAR>h0 : ¬n = 0<VAR>h : n % 2 = 0<GOAL>(-1) ^ (n % 2) * bernoulli' n = bernoulli' n
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<VAR>hn : n ≠ 1<VAR>h0 : ¬n = 0<VAR>h : n % 2 = 1<GOAL>(-1) ^ (n % 2) * bernoulli' n = bernoulli' n
<VAR>L : Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Q : Type u_4<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>inst✝ : L.Structure Q<VAR>S : L.ElementarySubstructure M<VAR>T : L.Theory<GOAL>↥S ⊨ T ↔ M ⊨ T
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>h₁ : x₁.Numeric<VAR>h₂ : x₂.Numeric<VAR>h₁₂ : IH24 x₁ x₂ y<VAR>h₂₁ : IH24 x₂ x₁ y<VAR>he : x₁ ≈ x₂<GOAL>x₁ * y ≤ x₂ * y
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>h₁ : x₁.Numeric<VAR>h₂ : x₂.Numeric<VAR>h₁₂ : IH24 x₁ x₂ y<VAR>h₂₁ : IH24 x₂ x₁ y<VAR>he : x₁ ≈ x₂<VAR>he' : -x₁ ≈ -x₂<GOAL>x₁ * y ≤ x₂ * y
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>h₁ : x₁.Numeric<VAR>h₂ : x₂.Numeric<VAR>h₁₂ : IH24 x₁ x₂ y<VAR>h₂₁ : IH24 x₂ x₁ y<VAR>he : x₁ ≈ x₂<VAR>he' : -x₁ ≈ -x₂<GOAL>∀ (i : (x₁ * y).LeftMoves), ⟦(x₁ * y).moveLeft i⟧ < ⟦x₂ * y⟧
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>h₁ : x₁.Numeric<VAR>h₂ : x₂.Numeric<VAR>h₁₂ : IH24 x₁ x₂ y<VAR>h₂₁ : IH24 x₂ x₁ y<VAR>he : x₁ ≈ x₂<VAR>he' : -x₁ ≈ -x₂<GOAL>∀ (j : (x₂ * y).RightMoves), ⟦x₁ * y⟧ < ⟦(x₂ * y).moveRight j⟧
<VAR>f : ℂ → ℂ<VAR>g : ℝ → ℝ<VAR>g' s : ℝ<VAR>hf : DifferentiableAt ℂ f ↑s<VAR>hg : HasDerivAt g g' s<VAR>hfg : ∀ (s : ℝ), f ↑s = ↑(g s)<GOAL>HasDerivAt f ↑g' ↑s
<VAR>f : ℂ → ℂ<VAR>g : ℝ → ℝ<VAR>g' s : ℝ<VAR>hf : DifferentiableAt ℂ f ↑s<VAR>hg : HasDerivAt g g' s<VAR>hfg : ∀ (s : ℝ), f ↑s = ↑(g s)<GOAL>deriv f ↑s = ↑g'
<VAR>f : ℂ → ℂ<VAR>g : ℝ → ℝ<VAR>g' s : ℝ<VAR>hf : DifferentiableAt ℂ f ↑s<VAR>hg : HasDerivAt g g' s<VAR>hfg : ∀ (s : ℝ), f ↑s = ↑(g s)<GOAL>deriv (fun x => ↑(g x)) s = ↑g'
<VAR>α : Type u_1<VAR>s✝ t✝ : Finset α<VAR>n : ℕ<VAR>s t : Finset α<GOAL>powersetCard n s = ∅ ↔ s.card < n
<VAR>α : Type u_1<VAR>s✝ t✝ : Finset α<VAR>n : ℕ<VAR>s t : Finset α<GOAL>powersetCard n s = ∅ → s.card < n
<VAR>α : Type u_1<VAR>s✝ t✝ : Finset α<VAR>n : ℕ<VAR>s t : Finset α<GOAL>n ≤ s.card → powersetCard n s ≠ ∅
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f : { f // ∀ (m : M), f m * f m = (algebraMap R A) (Q m) }<VAR>x y : TensorAlgebra R M<VAR>m✝ : M<GOAL>((TensorAlgebra.lift R) ↑f) ((TensorAlgebra.ι R) m✝ * (TensorAlgebra.ι R) m✝) = ((TensorAlgebra.lift R) ↑f) ((algebraMap R (TensorAlgebra R M)) (Q m✝))
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>F : CliffordAlgebra Q →ₐ[R] A<VAR>m : M<GOAL>(F.toLinearMap ∘ₗ ι Q) m * (F.toLinearMap ∘ₗ ι Q) m = (algebraMap R A) (Q m)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f : { f // ∀ (m : M), f m * f m = (algebraMap R A) (Q m) }<VAR>x : M<GOAL>↑((fun F => ⟨F.toLinearMap ∘ₗ ι Q, ⋯⟩) ((fun f => (RingQuot.liftAlgHom R) ⟨(TensorAlgebra.lift R) ↑f, ⋯⟩) f)) x = ↑f x
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>F : CliffordAlgebra Q →ₐ[R] A<VAR>x : M<GOAL>((((fun f => (RingQuot.liftAlgHom R) ⟨(TensorAlgebra.lift R) ↑f, ⋯⟩) ((fun F => ⟨F.toLinearMap ∘ₗ ι Q, ⋯⟩) F)).comp (RingQuot.mkAlgHom R (Rel Q))).toLinearMap ∘ₗ TensorAlgebra.ι R) x = ((F.comp (RingQuot.mkAlgHom R (Rel Q))).toLinearMap ∘ₗ TensorAlgebra.ι R) x
<VAR>R✝ : Type u<VAR>S : Type v<VAR>a b : R✝<VAR>n✝ m : ℕ<VAR>inst✝¹ : Semiring R✝<VAR>p q r : R✝[X]<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n k : ℕ<GOAL>((X + 1) ^ n).coeff k = ↑(n.choose k)
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>inst✝¹ : MeasurableSpace α<VAR>μ✝ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>β : Type u_6<VAR>inst✝ : MeasurableSpace β<VAR>μ : Measure β<VAR>C : β → Set α → Prop<VAR>s : Set (Set α)<VAR>m : MeasurableSpace α<VAR>h_eq : m = generateFrom s<VAR>h_inter : IsPiSystem s<VAR>h_empty : ∀ᵐ (x : β) ∂μ, C x ∅<VAR>h_basic : ∀ᵐ (x : β) ∂μ, ∀ t ∈ s, C x t<VAR>h_compl : ∀ᵐ (x : β) ∂μ, ∀ (t : Set α), MeasurableSet t → C x t → C x tᶜ<VAR>h_union : ∀ᵐ (x : β) ∂μ, ∀ (f : ℕ → Set α), Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C x (f i)) → C x (⋃ i, f i)<GOAL>∀ᵐ (x : β) ∂μ, ∀ ⦃t : Set α⦄, MeasurableSet t → C x t
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Group G<VAR>a x y : G<VAR>h : SemiconjBy a x y<GOAL>orderOf x = orderOf y
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Group G<VAR>a x y : G<VAR>h : SemiconjBy a x y<GOAL>∀ (n : ℕ), x ^ n = 1 ↔ y ^ n = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Group G<VAR>a x y : G<VAR>h : SemiconjBy a x y<VAR>n : ℕ<GOAL>x ^ n = 1 ↔ y ^ n = 1
<VAR>a b : Ordinal.{u_1}<VAR>h : a < ω ^ b<GOAL>a + ω ^ b = ω ^ b
<VAR>a b : Ordinal.{u_1}<VAR>h : a < ω ^ b<GOAL>a + ω ^ b ≤ ω ^ b
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : ConcreteCategory C<VAR>inst✝ : (forget C).ReflectsIsomorphisms<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>IsIso f ↔ Function.Bijective ((forget C).map f)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : ConcreteCategory C<VAR>inst✝ : (forget C).ReflectsIsomorphisms<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>IsIso f ↔ IsIso ((forget C).map f)
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝ : CommRing R<VAR>g : R[X]<VAR>hg : g.Monic<VAR>i : Fin g.natDegree<GOAL>(powerBasisAux' hg) i = root g ^ ↑i
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝ : CommRing R<VAR>g : R[X]<VAR>hg : g.Monic<VAR>i : Fin g.natDegree<GOAL>(mk g) (∑ i_1 : Fin g.natDegree, (monomial ↑i_1) (Function.update 0 i 1 i_1)) = root g ^ ↑i
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝ : CommRing R<VAR>g : R[X]<VAR>hg : g.Monic<VAR>i : Fin g.natDegree<GOAL>(mk g) ((monomial ↑i) (Function.update 0 i 1 i)) = root g ^ ↑i
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝ : CommRing R<VAR>g : R[X]<VAR>hg : g.Monic<VAR>i : Fin g.natDegree<GOAL>∀ b ∈ Finset.univ, b ≠ i → (monomial ↑b) (Function.update 0 i 1 b) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝ : CommRing R<VAR>g : R[X]<VAR>hg : g.Monic<VAR>i : Fin g.natDegree<GOAL>i ∉ Finset.univ → (monomial ↑i) (Function.update 0 i 1 i) = 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✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>l : ι →₀ 𝕜<VAR>v : ι → E<VAR>x : E<GOAL>⟪x, l.sum fun i a => a • v i⟫_𝕜 = l.sum fun i a => a • ⟪x, v i⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>l : ι →₀ 𝕜<VAR>v : ι → E<VAR>x : E<GOAL>(l.sum fun i a => a • ⟪x, v i⟫_𝕜) = ∑ i ∈ l.support, ⟪x, l i • v i⟫_𝕜