ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>p : β → Prop<GOAL>(∀ b ∈ image f s, p b) ↔ ∀ a ∈ s, p (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Ord α<VAR>inst✝² : Ord β<VAR>inst✝¹ : OrientedOrd α<VAR>inst✝ : OrientedOrd β<GOAL>OrientedOrd (α × β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Ord α<VAR>inst✝² : Ord β<VAR>inst✝¹ : OrientedOrd α<VAR>inst✝ : OrientedOrd β<GOAL>OrientedCmp (compareLex (compareOn fun x => x.fst) (compareOn fun x => x.snd))
<VAR>R : Type u_1<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : BinomialRing R<VAR>n k : ℕ<GOAL>multichoose (-↑n) (n + k + 1) = 0
<VAR>R : Type u_1<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : BinomialRing R<VAR>n k : ℕ<GOAL>(fun x => (n + k + 1).factorial • x) (multichoose (-↑n) (n + k + 1)) = (fun x => (n + k + 1).factorial • x) 0
<VAR>R : Type u_1<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : BinomialRing R<VAR>n k : ℕ<GOAL>(n + k + 1).factorial • multichoose (-↑n) (n + k + 1) = (n + k + 1).factorial • 0
<VAR>n : ℕ<GOAL>n.descFactorial 0 ≤ n ^ 0
<VAR>n k : ℕ<GOAL>n.descFactorial (k + 1) ≤ n ^ (k + 1)
<VAR>n k : ℕ<GOAL>(n - k) * n.descFactorial k ≤ n * n ^ k
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β✝ : ι → Type u_4<VAR>inst✝² : Fact (1 ≤ p)<VAR>inst✝¹ : Fintype ι<VAR>β : ι → Type u_5<VAR>inst✝ : (i : ι) → SeminormedAddCommGroup (β i)<VAR>x y : PiLp 2 β<GOAL>dist x y = √(∑ i : ι, dist (x i) (y i) ^ 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Set α → Filter β<VAR>f : Filter α<VAR>s : Set α<VAR>hs : s ∈ f<GOAL>f ≤ 𝓟 s
<VAR>m n : ℕ+<GOAL>m ∣ n → m ≤ n
<VAR>m n : ℕ+<GOAL>n.mod m = m → m ≤ n
<VAR>m n : ℕ+<VAR>h : n.mod m = m<GOAL>n.mod m ≤ n
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>T T₁ T₂ : Monad C<VAR>h : T₂ ⟶ T₁<VAR>A : T₁.Algebra<GOAL>T₂.η.app A.A ≫ h.app A.A ≫ A.a = 𝟙 A.A
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>T T₁ T₂ : Monad C<VAR>h : T₂ ⟶ T₁<VAR>A : T₁.Algebra<GOAL>T₂.μ.app A.A ≫ h.app A.A ≫ A.a = T₂.map (h.app A.A ≫ A.a) ≫ h.app A.A ≫ A.a
<VAR>η : Type u_1<VAR>α✝ : Type u_2<VAR>ι✝ : Type u_3<VAR>κ✝ : Type u_4<VAR>l✝ : Line α✝ ι✝<VAR>i : ι✝<VAR>a x✝² : α✝<VAR>α α' : Type u<VAR>e : α ≃ α'<VAR>κ : Type (max v u)<VAR>x✝¹ : Finite κ<VAR>ι : Type<VAR>x✝ : Fintype ι<VAR>h : ∀ (C : (ι → α) → κ), ∃ l, IsMono C l<VAR>C : (ι → α') → κ<VAR>l : Line α ι<VAR>c : κ<VAR>lc : ∀ (x : α), (fun v => C (⇑e ∘ v)) ((fun x i => (l.idxFun i).getD x) x) = c<VAR>x : α<GOAL>C ((fun x i => ((map (⇑e) l).idxFun i).getD x) (e x)) = c
<VAR>η : Type u_1<VAR>α✝ : Type u_2<VAR>ι : Type u_3<VAR>κ✝ : Type u_4<VAR>l : Line α✝ ι<VAR>i : ι<VAR>a x : α✝<VAR>α : Type u<VAR>inst✝¹ : Fintype α<VAR>ihα : ∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l<VAR>κ : Type (max v u)<VAR>inst✝ : Finite κ<GOAL>∃ ι x, ∀ (C : (ι → Option α) → κ), ∃ l, IsMono C l
<VAR>η : Type u_1<VAR>α✝ : Type u_2<VAR>ι : Type u_3<VAR>κ✝ : Type u_4<VAR>l : Line α✝ ι<VAR>i : ι<VAR>a x : α✝<VAR>α : Type u<VAR>inst✝¹ : Fintype α<VAR>ihα : ∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l<VAR>κ : Type (max v u)<VAR>inst✝ : Finite κ<VAR>val✝ : Fintype κ<GOAL>∃ ι x, ∀ (C : (ι → Option α) → κ), ∃ l, IsMono C l
<VAR>η : Type u_1<VAR>α✝ : Type u_2<VAR>ι : Type u_3<VAR>κ✝ : Type u_4<VAR>l : Line α✝ ι<VAR>i : ι<VAR>a x : α✝<VAR>α : Type u<VAR>inst✝¹ : Fintype α<VAR>ihα : ∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l<VAR>κ : Type (max v u)<VAR>inst✝ : Finite κ<VAR>val✝ : Fintype κ<VAR>h : Nonempty α<GOAL>∃ ι x, ∀ (C : (ι → Option α) → κ), ∃ l, IsMono C l
<VAR>η : Type u_1<VAR>α✝ : Type u_2<VAR>ι : Type u_3<VAR>κ✝ : Type u_4<VAR>l : Line α✝ ι<VAR>i : ι<VAR>a x : α✝<VAR>α : Type u<VAR>inst✝¹ : Fintype α<VAR>ihα : ∀ (κ : Type (max v u)) [inst : Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l<VAR>κ : Type (max v u)<VAR>inst✝ : Finite κ<VAR>val✝ : Fintype κ<VAR>h : Nonempty α<GOAL>∀ (r : ℕ), ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, Multiset.card s.lines = r) ∨ ∃ l, IsMono C l
<VAR>η : Type u_1<VAR>α✝ : Type u_2<VAR>ι✝ : Type u_3<VAR>κ✝ : Type u_4<VAR>l : Line α✝ ι✝<VAR>i : ι✝<VAR>a x : α✝<VAR>α : Type u<VAR>inst✝¹ : Fintype α<VAR>κ : Type (max v u)<VAR>inst✝ : Finite κ<VAR>val✝ : Fintype κ<VAR>h : Nonempty α<VAR>r : ℕ<VAR>ι : Type<VAR>_inst✝ : Fintype ι<VAR>hι : ∀ (C : (ι → Option α) → κ), (∃ s, Multiset.card s.lines = r) ∨ ∃ l, IsMono C l<VAR>ι' : Type<VAR>_inst : Fintype ι'<VAR>C : (ι ⊕ ι' → Option α) → κ<VAR>l' : Line α ι'<VAR>C' : (ι → Option α) → κ<VAR>hl' : ∀ (x : α), (fun v' v => C (Sum.elim v (some ∘ v'))) ((fun x i => (l'.idxFun i).getD x) x) = C'<GOAL>(∃ s, Multiset.card s.lines = r + 1) ∨ ∃ l, IsMono C l
<VAR>η : Type u_1<VAR>α✝ : Type u_2<VAR>ι✝ : Type u_3<VAR>κ✝ : Type u_4<VAR>l : Line α✝ ι✝<VAR>i : ι✝<VAR>a x : α✝<VAR>α : Type u<VAR>inst✝¹ : Fintype α<VAR>κ : Type (max v u)<VAR>inst✝ : Finite κ<VAR>val✝ : Fintype κ<VAR>h : Nonempty α<VAR>r : ℕ<VAR>ι : Type<VAR>_inst✝ : Fintype ι<VAR>hι : ∀ (C : (ι → Option α) → κ), (∃ s, Multiset.card s.lines = r) ∨ ∃ l, IsMono C l<VAR>ι' : Type<VAR>_inst : Fintype ι'<VAR>C : (ι ⊕ ι' → Option α) → κ<VAR>l' : Line α ι'<VAR>C' : (ι → Option α) → κ<VAR>hl' : ∀ (x : α), (fun v' v => C (Sum.elim v (some ∘ v'))) ((fun x i => (l'.idxFun i).getD x) x) = C'<VAR>mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l<GOAL>(∃ s, Multiset.card s.lines = r + 1) ∨ ∃ l, IsMono C l
<VAR>n m : ℕ<VAR>α : Sort u_1<VAR>k k' : ℕ<VAR>f g : Fin k → Fin k' → α<GOAL>HEq f g ↔ ∀ (i : Fin k) (j : Fin k'), f i j = g ⟨↑i, ⋯⟩ ⟨↑j, ⋯⟩
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>m n : ℤ<GOAL>T (m + n) = T m * T n
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m✝ n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>m : ℕ<VAR>h : ContDiffWithinAt 𝕜 n f s x<VAR>hmn : ↑m < n<VAR>hs : UniqueDiffOn 𝕜 (insert x s)<GOAL>DifferentiableWithinAt 𝕜 (iteratedFDerivWithin 𝕜 m f s) s x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u✝ : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m✝ n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>m : ℕ<VAR>h : ContDiffWithinAt 𝕜 n f s x<VAR>hmn : ↑m < n<VAR>hs : UniqueDiffOn 𝕜 (insert x s)<VAR>u : Set E<VAR>uo : IsOpen u<VAR>xu : x ∈ u<VAR>hu : ContDiffOn 𝕜 (↑(Add.add (↑m) 1)) f (insert x s ∩ u)<GOAL>DifferentiableWithinAt 𝕜 (iteratedFDerivWithin 𝕜 m f s) s x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t✝ u✝ : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m✝ n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>m : ℕ<VAR>h : ContDiffWithinAt 𝕜 n f s x<VAR>hmn : ↑m < n<VAR>hs : UniqueDiffOn 𝕜 (insert x s)<VAR>u : Set E<VAR>uo : IsOpen u<VAR>xu : x ∈ u<VAR>t : Set E := insert x s ∩ u<VAR>hu : ContDiffOn 𝕜 (↑(Add.add (↑m) 1)) f t<GOAL>DifferentiableWithinAt 𝕜 (iteratedFDerivWithin 𝕜 m f s) s x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t✝ u✝ : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m✝ n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>m : ℕ<VAR>h : ContDiffWithinAt 𝕜 n f s x<VAR>hmn : ↑m < n<VAR>hs : UniqueDiffOn 𝕜 (insert x s)<VAR>u : Set E<VAR>uo : IsOpen u<VAR>xu : x ∈ u<VAR>t : Set E := insert x s ∩ u<VAR>hu : ContDiffOn 𝕜 (↑(Add.add (↑m) 1)) f t<VAR>A : t =ᶠ[𝓝[≠] x] s<GOAL>DifferentiableWithinAt 𝕜 (iteratedFDerivWithin 𝕜 m f s) s x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t✝ u✝ : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m✝ n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>m : ℕ<VAR>h : ContDiffWithinAt 𝕜 n f s x<VAR>hmn : ↑m < n<VAR>hs : UniqueDiffOn 𝕜 (insert x s)<VAR>u : Set E<VAR>uo : IsOpen u<VAR>xu : x ∈ u<VAR>t : Set E := insert x s ∩ u<VAR>hu : ContDiffOn 𝕜 (↑(Add.add (↑m) 1)) f t<VAR>A : t =ᶠ[𝓝[≠] x] s<VAR>B : iteratedFDerivWithin 𝕜 m f s =ᶠ[𝓝 x] iteratedFDerivWithin 𝕜 m f t<GOAL>DifferentiableWithinAt 𝕜 (iteratedFDerivWithin 𝕜 m f s) s x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t✝ u✝ : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m✝ n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>m : ℕ<VAR>h : ContDiffWithinAt 𝕜 n f s x<VAR>hmn : ↑m < n<VAR>hs : UniqueDiffOn 𝕜 (insert x s)<VAR>u : Set E<VAR>uo : IsOpen u<VAR>xu : x ∈ u<VAR>t : Set E := insert x s ∩ u<VAR>hu : ContDiffOn 𝕜 (↑(Add.add (↑m) 1)) f t<VAR>A : t =ᶠ[𝓝[≠] x] s<VAR>B : iteratedFDerivWithin 𝕜 m f s =ᶠ[𝓝 x] iteratedFDerivWithin 𝕜 m f t<VAR>C : DifferentiableWithinAt 𝕜 (iteratedFDerivWithin 𝕜 m f t) t x<GOAL>DifferentiableWithinAt 𝕜 (iteratedFDerivWithin 𝕜 m f s) s x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t✝ u✝ : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m✝ n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>m : ℕ<VAR>h : ContDiffWithinAt 𝕜 n f s x<VAR>hmn : ↑m < n<VAR>hs : UniqueDiffOn 𝕜 (insert x s)<VAR>u : Set E<VAR>uo : IsOpen u<VAR>xu : x ∈ u<VAR>t : Set E := insert x s ∩ u<VAR>hu : ContDiffOn 𝕜 (↑(Add.add (↑m) 1)) f t<VAR>A : t =ᶠ[𝓝[≠] x] s<VAR>B : iteratedFDerivWithin 𝕜 m f s =ᶠ[𝓝 x] iteratedFDerivWithin 𝕜 m f t<VAR>C : DifferentiableWithinAt 𝕜 (iteratedFDerivWithin 𝕜 m f t) s x<GOAL>DifferentiableWithinAt 𝕜 (iteratedFDerivWithin 𝕜 m f s) s x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>N : Type u_6<VAR>inst✝⁷ : Monoid R<VAR>inst✝⁶ : Monoid S<VAR>σ : R → S<VAR>inst✝⁵ : MulAction R M<VAR>inst✝⁴ : MulAction S N<VAR>inst✝³ : MulAction R M₁<VAR>inst✝² : MulAction R M₂<VAR>F : Type u_7<VAR>h : F<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : MulActionSemiHomClass F σ M N<VAR>c : R<VAR>s : Set M<VAR>t : Set N<VAR>hc : IsUnit c<VAR>hc' : IsUnit (σ c)<GOAL>⇑h ⁻¹' (σ c • t) = c • ⇑h ⁻¹' t
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>N : Type u_6<VAR>inst✝⁷ : Monoid R<VAR>inst✝⁶ : Monoid S<VAR>σ : R → S<VAR>inst✝⁵ : MulAction R M<VAR>inst✝⁴ : MulAction S N<VAR>inst✝³ : MulAction R M₁<VAR>inst✝² : MulAction R M₂<VAR>F : Type u_7<VAR>h : F<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : MulActionSemiHomClass F σ M N<VAR>c : R<VAR>s : Set M<VAR>t : Set N<VAR>hc : IsUnit c<VAR>hc' : IsUnit (σ c)<GOAL>Function.Surjective fun m => c • m
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>N : Type u_6<VAR>inst✝⁷ : Monoid R<VAR>inst✝⁶ : Monoid S<VAR>σ : R → S<VAR>inst✝⁵ : MulAction R M<VAR>inst✝⁴ : MulAction S N<VAR>inst✝³ : MulAction R M₁<VAR>inst✝² : MulAction R M₂<VAR>F : Type u_7<VAR>h : F<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : MulActionSemiHomClass F σ M N<VAR>c : R<VAR>s : Set M<VAR>t : Set N<VAR>hc : IsUnit c<VAR>hc' : IsUnit (σ c)<GOAL>Function.Injective fun n => σ c • n
<VAR>r p : ℝ<VAR>hr : 0 < r<GOAL>r.toNNReal ≤ p.toNNReal ↔ r ≤ p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s✝ : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>s : Set (α × β)<GOAL>s ∈ f ×ˢ ⊤ ↔ {a | ∀ (b : β), (a, b) ∈ s} ∈ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s✝ : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>s : Set (α × β)<GOAL>{a | ∀ b ∈ univ, (a, b) ∈ s} ∈ f ↔ {a | ∀ (b : β), (a, b) ∈ s} ∈ f
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>hs : IsLowerSet s<VAR>hx : x ∈ closure s<VAR>h : ∀ (i : ι), y i < x i<GOAL>y ∈ interior s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>hs : IsLowerSet s<VAR>hx : x ∈ closure s<VAR>h : ∀ (i : ι), y i < x i<VAR>val✝ : Fintype ι<GOAL>y ∈ interior s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>hs : IsLowerSet s<VAR>hx : x ∈ closure s<VAR>h : ∀ (i : ι), y i < x i<VAR>val✝ : Fintype ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hxy : ∀ (i : ι), y i + ε < x i<GOAL>y ∈ interior s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>hs : IsLowerSet s<VAR>hx : x ∈ closure s<VAR>h : ∀ (i : ι), y i < x i<VAR>val✝ : Fintype ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hxy : ∀ (i : ι), y i + ε < x i<VAR>z : ι → ℝ<VAR>hz : z ∈ s<VAR>hxz : dist x z < ε<GOAL>y ∈ interior s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>hs : IsLowerSet s<VAR>hx : x ∈ closure s<VAR>h : ∀ (i : ι), y i < x i<VAR>val✝ : Fintype ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hxy : ∀ (i : ι), y i + ε < x i<VAR>z : ι → ℝ<VAR>hz : z ∈ s<VAR>hxz : ∀ (b : ι), dist (x b) (z b) < ε<GOAL>y ∈ interior s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>hs : IsLowerSet s<VAR>hx : x ∈ closure s<VAR>h : ∀ (i : ι), y i < x i<VAR>val✝ : Fintype ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hxy : ∀ (i : ι), y i + ε < x i<VAR>z : ι → ℝ<VAR>hz : z ∈ s<VAR>hxz : ∀ (b : ι), dist (x b) (z b) < ε<VAR>hyz : ∀ (i : ι), y i < z i<GOAL>y ∈ interior s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>hs : IsLowerSet s<VAR>hx : x ∈ closure s<VAR>h : ∀ (i : ι), y i < x i<VAR>val✝ : Fintype ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hxy : ∀ (i : ι), y i + ε < x i<VAR>z : ι → ℝ<VAR>hz : z ∈ s<VAR>hxz : ∀ (b : ι), dist (x b) (z b) < ε<VAR>hyz✝ : ∀ (i : ι), y i < z i<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>hyz : ∀ (i : ι), y i + δ < z i<GOAL>y ∈ interior s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>hs : IsLowerSet s<VAR>hx : x ∈ closure s<VAR>h : ∀ (i : ι), y i < x i<VAR>val✝ : Fintype ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hxy : ∀ (i : ι), y i + ε < x i<VAR>z : ι → ℝ<VAR>hz : z ∈ s<VAR>hxz : ∀ (b : ι), dist (x b) (z b) < ε<VAR>hyz✝ : ∀ (i : ι), y i < z i<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>hyz : ∀ (i : ι), y i + δ < z i<GOAL>ball y δ ⊆ s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>hs : IsLowerSet s<VAR>hx : x ∈ closure s<VAR>h : ∀ (i : ι), y i < x i<VAR>val✝ : Fintype ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hxy : ∀ (i : ι), y i + ε < x i<VAR>z : ι → ℝ<VAR>hz : z ∈ s<VAR>hxz : ∀ (b : ι), dist (x b) (z b) < ε<VAR>hyz✝ : ∀ (i : ι), y i < z i<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>hyz : ∀ (i : ι), y i + δ < z i<VAR>w : ι → ℝ<VAR>hw : w ∈ ball y δ<VAR>i : ι<GOAL>w i ≤ z i
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>hs : IsLowerSet s<VAR>hx : x ∈ closure s<VAR>h : ∀ (i : ι), y i < x i<VAR>val✝ : Fintype ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hxy : ∀ (i : ι), y i + ε < x i<VAR>z : ι → ℝ<VAR>hz : z ∈ s<VAR>hxz : ∀ (b : ι), dist (x b) (z b) < ε<VAR>hyz✝ : ∀ (i : ι), y i < z i<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>hyz : ∀ (i : ι), y i + δ < z i<VAR>w : ι → ℝ<VAR>i : ι<VAR>hw : w ∈ univ.pi fun b => Ioo (y b - δ) (y b + δ)<GOAL>w i ≤ z i
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q : ℕ<VAR>p : R[X]<VAR>hsep : p.Separable<GOAL>Squarefree p
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q : ℕ<VAR>p : R[X]<VAR>hsep : p.Separable<GOAL>∀ (x : R[X]), multiplicity x p ≤ 1 ∨ IsUnit x
<VAR>α : Type u_1<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : SuccOrder α<VAR>a b : α<VAR>C : α → Sort u_2<VAR>inst✝ : NoMaxOrder α<GOAL>¬IsSuccLimit a ↔ a ∈ range succ
<VAR>α : Type u_1<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : SuccOrder α<VAR>a b : α<VAR>C : α → Sort u_2<VAR>inst✝ : NoMaxOrder α<GOAL>(∃ x, succ x = a) ↔ a ∈ range succ
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>i j k : 𝒰.J<GOAL>t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k) ≫ pullback.fst (𝒰.map i ≫ f) g = pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k) ≫ pullback.fst (𝒰.map i ≫ f) g
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>i j k : 𝒰.J<GOAL>(t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k) ≫ pullback.fst (𝒰.map i ≫ f) g) ≫ 𝒰.map i = (pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k) ≫ pullback.fst (𝒰.map i ≫ f) g) ≫ 𝒰.map i
<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>l : β →₀ M<VAR>hf : Set.InjOn f (f ⁻¹' ↑l.support)<VAR>a : α<GOAL>a ∈ l.support.preimage f hf ↔ (fun a => l (f a)) a ≠ 0
<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>l : β →₀ M<VAR>hf : Set.InjOn f (f ⁻¹' ↑l.support)<VAR>a : α<GOAL>f a ∈ l.support ↔ l (f a) ≠ 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝¹ : DivisionSemiring R<VAR>inst✝ : StarRing R<VAR>x : R<VAR>hx : IsSelfAdjoint x<GOAL>IsSelfAdjoint x⁻¹
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Preorder α<VAR>a b✝ c : α<VAR>inst✝ : NoMinOrder α<VAR>b : α<GOAL>⋃ a, Ioc a b = Iic b
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : AddCommMonoid N<VAR>n : ℕ<VAR>f : ℕ × ℕ → M<GOAL>∏ p ∈ antidiagonal (n + 1), f p = f (0, n + 1) * ∏ p ∈ antidiagonal n, f (p.1 + 1, p.2)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : AddCommMonoid N<VAR>n : ℕ<VAR>f : ℕ × ℕ → M<GOAL>f (0, n + 1) * ∏ x ∈ antidiagonal n, f (({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Function.Embedding.refl ℕ)) x) = f (0, n + 1) * ∏ p ∈ antidiagonal n, f (p.1 + 1, p.2)
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>f : α → β<VAR>a : α<VAR>s : Stream' α<GOAL>map f (a :: s) = f a :: map f s
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>f : α → β<VAR>a : α<VAR>s : Stream' α<GOAL>(f (a :: s).head :: map f (a :: s).tail).head :: (f (a :: s).head :: map f (a :: s).tail).tail = f a :: map f s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>inst✝ : Finite α<VAR>C : Set α → Prop<VAR>S0 : Set α<VAR>H0 : C S0<VAR>H1 : ∀ (S : Set α), S ≠ univ → C S → ∃ a ∉ S, C (insert a S)<GOAL>∀ s ⊂ univ, C s → ∃ a ∈ univ \ s, C (insert a s)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹⁸ : CommSemiring R<VAR>inst✝¹⁷ : AddCommMonoid M₁<VAR>inst✝¹⁶ : Module R M₁<VAR>inst✝¹⁵ : AddCommMonoid M₂<VAR>inst✝¹⁴ : Module R M₂<VAR>inst✝¹³ : AddCommMonoid N₂<VAR>inst✝¹² : Module R N₂<VAR>inst✝¹¹ : DecidableEq n<VAR>inst✝¹⁰ : Fintype n<VAR>inst✝⁹ : DecidableEq m<VAR>inst✝⁸ : Fintype m<VAR>b₁✝ : Basis n R M₁<VAR>b₂✝ : Basis m R M₂<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>inst✝⁷ : AddCommMonoid M₁'<VAR>inst✝⁶ : Module R M₁'<VAR>inst✝⁵ : AddCommMonoid M₂'<VAR>inst✝⁴ : Module R M₂'<VAR>b₁' : Basis n' R M₁'<VAR>b₂' : Basis m' R M₂'<VAR>inst✝³ : Fintype n'<VAR>inst✝² : Fintype m'<VAR>inst✝¹ : DecidableEq n'<VAR>inst✝ : DecidableEq m'<VAR>B : M₁ →ₗ[R] M₂ →ₗ[R] R<VAR>l : M₁' →ₗ[R] M₁<VAR>r : M₂' →ₗ[R] M₂<VAR>i : n'<VAR>j : m'<GOAL>(toMatrix₂ b₁' b₂') (B.compl₁₂ l r) i j = (((toMatrix b₁' b₁) l)ᵀ * (toMatrix₂ b₁ b₂) B * (toMatrix b₂' b₂) r) i j
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹⁸ : CommSemiring R<VAR>inst✝¹⁷ : AddCommMonoid M₁<VAR>inst✝¹⁶ : Module R M₁<VAR>inst✝¹⁵ : AddCommMonoid M₂<VAR>inst✝¹⁴ : Module R M₂<VAR>inst✝¹³ : AddCommMonoid N₂<VAR>inst✝¹² : Module R N₂<VAR>inst✝¹¹ : DecidableEq n<VAR>inst✝¹⁰ : Fintype n<VAR>inst✝⁹ : DecidableEq m<VAR>inst✝⁸ : Fintype m<VAR>b₁✝ : Basis n R M₁<VAR>b₂✝ : Basis m R M₂<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>inst✝⁷ : AddCommMonoid M₁'<VAR>inst✝⁶ : Module R M₁'<VAR>inst✝⁵ : AddCommMonoid M₂'<VAR>inst✝⁴ : Module R M₂'<VAR>b₁' : Basis n' R M₁'<VAR>b₂' : Basis m' R M₂'<VAR>inst✝³ : Fintype n'<VAR>inst✝² : Fintype m'<VAR>inst✝¹ : DecidableEq n'<VAR>inst✝ : DecidableEq m'<VAR>B : M₁ →ₗ[R] M₂ →ₗ[R] R<VAR>l : M₁' →ₗ[R] M₁<VAR>r : M₂' →ₗ[R] M₂<VAR>i : n'<VAR>j : m'<GOAL>(B (l (b₁' i))) (r (b₂' j)) = ∑ x : m, ∑ i_1 : n, (b₁.repr (l (b₁' i))) i_1 * (B (b₁ i_1)) (b₂ x) * (b₂.repr (r (b₂' j))) x