ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>x : X<VAR>inst✝¹ : DecidableEq N<VAR>inst✝ : Nonempty N<VAR>i : N<VAR>p : ↑(Ω^ N X x)<GOAL>(loopHomeo (Classical.arbitrary N)).symm (Path.symm ((loopHomeo (Classical.arbitrary N)).toEquiv p)) ≈ fromLoop (Classical.arbitrary N) (Path.symm (toLoop (Classical.arbitrary N) p))
<VAR>F : Type u_1<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : NonUnitalNonAssocSemiring A<VAR>inst✝⁸ : Module R A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>inst✝⁶ : SMulCommClass R A A<VAR>inst✝⁵ : NonUnitalNonAssocSemiring B<VAR>inst✝⁴ : Module R B<VAR>inst✝³ : IsScalarTower R B B<VAR>inst✝² : SMulCommClass R B B<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : NonUnitalAlgHomClass F R A B<VAR>f : A →ₙₐ[R] B<GOAL>↑(NonUnitalSubalgebra.map f ⊥) = ↑⊥
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝³ : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝¹ : (i : ι) → PartialOrder (α i)<VAR>inst✝ : ∀ (i : ι), NoAtoms (μ i)<VAR>f : (i : ι) → α i<GOAL>(univ.pi fun i => Ioi (f i)) =ᶠ[ae (Measure.pi μ)] Ici f
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝³ : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝¹ : (i : ι) → PartialOrder (α i)<VAR>inst✝ : ∀ (i : ι), NoAtoms (μ i)<VAR>f : (i : ι) → α i<GOAL>(univ.pi fun i => Ioi (f i)) =ᶠ[ae (Measure.pi μ)] univ.pi fun i => Ici (f i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a b c : α<VAR>inst✝ : DecidableEq α<VAR>h : a < b<GOAL>insert b (Ioo a b) = Ioc a b
<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>x y : E<GOAL>re ⟪x, y⟫_𝕜 = (‖x + y‖ * ‖x + y‖ - ‖x‖ * ‖x‖ - ‖y‖ * ‖y‖) / 2
<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>x y : E<GOAL>re ⟪x, y⟫_𝕜 = (‖x‖ * ‖x‖ + 2 * re ⟪x, y⟫_𝕜 + ‖y‖ * ‖y‖ - ‖x‖ * ‖x‖ - ‖y‖ * ‖y‖) / 2
<VAR>o : ONote<VAR>h : o.fundamentalSequence = Sum.inl none<GOAL>o.fastGrowing = Nat.succ
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E✝ : Type u<VAR>inst✝⁷ : NormedAddCommGroup E✝<VAR>inst✝⁶ : NormedSpace 𝕜 E✝<VAR>F : Type v<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>ι✝ : Type u_2<VAR>E : ι✝ → Type u_3<VAR>inst✝³ : (i : ι✝) → NormedAddCommGroup (E i)<VAR>inst✝² : (i : ι✝) → NormedSpace 𝕜 (E i)<VAR>inst✝¹ : Fintype ι✝<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>n✝ : ℕ∞<VAR>x : (i : ι✝) → E i<VAR>ι : Type u_4<VAR>inst✝ : DecidableEq ι<VAR>n : ℕ<VAR>e : Fin (n + 1) ↪ ι<VAR>j : Fin (n + 1)<VAR>h'k : e j ∈ Set.range ⇑((Equiv.embeddingFinSucc n ι) e).fst<VAR>hj : j ≠ 0<GOAL>(((Equiv.embeddingFinSucc n ι) e).fst.toEquivRange.symm ⟨e j, h'k⟩).succ = e.toEquivRange.symm ⟨e j, ⋯⟩
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E✝ : Type u<VAR>inst✝⁷ : NormedAddCommGroup E✝<VAR>inst✝⁶ : NormedSpace 𝕜 E✝<VAR>F : Type v<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>ι✝ : Type u_2<VAR>E : ι✝ → Type u_3<VAR>inst✝³ : (i : ι✝) → NormedAddCommGroup (E i)<VAR>inst✝² : (i : ι✝) → NormedSpace 𝕜 (E i)<VAR>inst✝¹ : Fintype ι✝<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>n✝ : ℕ∞<VAR>x : (i : ι✝) → E i<VAR>ι : Type u_4<VAR>inst✝ : DecidableEq ι<VAR>n : ℕ<VAR>e : Fin (n + 1) ↪ ι<VAR>j : Fin (n + 1)<VAR>h'k : e j ∈ Set.range ⇑((Equiv.embeddingFinSucc n ι) e).fst<VAR>hj : j ≠ 0<GOAL>(((Equiv.embeddingFinSucc n ι) e).fst.toEquivRange.symm ⟨e j, h'k⟩).succ = j
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E✝ : Type u<VAR>inst✝⁷ : NormedAddCommGroup E✝<VAR>inst✝⁶ : NormedSpace 𝕜 E✝<VAR>F : Type v<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>ι✝ : Type u_2<VAR>E : ι✝ → Type u_3<VAR>inst✝³ : (i : ι✝) → NormedAddCommGroup (E i)<VAR>inst✝² : (i : ι✝) → NormedSpace 𝕜 (E i)<VAR>inst✝¹ : Fintype ι✝<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>n✝ : ℕ∞<VAR>x : (i : ι✝) → E i<VAR>ι : Type u_4<VAR>inst✝ : DecidableEq ι<VAR>n : ℕ<VAR>e : Fin (n + 1) ↪ ι<VAR>j : Fin (n + 1)<VAR>h'k : e j ∈ Set.range ⇑((Equiv.embeddingFinSucc n ι) e).fst<VAR>hj : j ≠ 0<VAR>this : e j = ((Equiv.embeddingFinSucc n ι) e).fst (j.pred hj)<GOAL>(((Equiv.embeddingFinSucc n ι) e).fst.toEquivRange.symm ⟨((Equiv.embeddingFinSucc n ι) e).fst (j.pred hj), ⋯⟩).succ = j
<VAR>α : Type u_1<VAR>f : α → α<VAR>head✝ : α<VAR>l : List α<VAR>m : Nat<GOAL>(modifyNth f 0 (head✝ :: l))[m + 1]? = (fun a => if 0 = m + 1 then f a else a) <$> (head✝ :: l)[m + 1]?
<VAR>α : Type u_1<VAR>f : α → α<VAR>n : Nat<VAR>a : α<VAR>l : List α<VAR>m : Nat<GOAL>(modifyNth f (n + 1) (a :: l))[m + 1]? = (fun a => if n + 1 = m + 1 then f a else a) <$> (a :: l)[m + 1]?
<VAR>α : Type u_1<VAR>f : α → α<VAR>n : Nat<VAR>a : α<VAR>l : List α<VAR>m : Nat<GOAL>(modifyNth f n l)[m]? = Option.map (fun a => if n = m then f a else a) l[m]?
<VAR>α : Type u_1<VAR>f : α → α<VAR>n : Nat<VAR>a : α<VAR>l : List α<VAR>m : Nat<GOAL>(fun a => if n = m then f a else a) <$> l[m]? = Option.map (fun a => if n = m then f a else a) l[m]?
<VAR>x y : ℂ<VAR>hx₀ : x ≠ 0<VAR>hy₀ : y ≠ 0<GOAL>log (x * y) = log x + log y ↔ x.arg + y.arg ∈ Set.Ioc (-π) π
<VAR>x y : ℂ<VAR>hx₀ : x ≠ 0<VAR>hy₀ : y ≠ 0<GOAL>(log (x * y)).re = (log x + log y).re ∧ (log (x * y)).im = (log x + log y).im ↔ (x * y).arg = x.arg + y.arg
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r r' : α → α → Prop<VAR>inst✝ : IsStrictOrder α r<VAR>s t : Set α<VAR>hs : s.WellFoundedOn r<VAR>ht : t.WellFoundedOn r<GOAL>(s ∪ t).WellFoundedOn r
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r r' : α → α → Prop<VAR>inst✝ : IsStrictOrder α r<VAR>s t : Set α<VAR>hs : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), f n ∈ s<VAR>ht : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), f n ∈ t<GOAL>∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), f n ∈ s ∪ t
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r r' : α → α → Prop<VAR>inst✝ : IsStrictOrder α r<VAR>s t : Set α<VAR>hs : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), f n ∈ s<VAR>ht : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), f n ∈ t<VAR>f : (fun x x_1 => x > x_1) ↪r r<VAR>hf : ∀ (n : ℕ), f n ∈ s ∪ t<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r r' : α → α → Prop<VAR>inst✝ : IsStrictOrder α r<VAR>s t : Set α<VAR>hs : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), f n ∈ s<VAR>ht : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), f n ∈ t<VAR>f : (fun x x_1 => x > x_1) ↪r r<VAR>hf : ∀ (n : ℕ), f n ∈ s ∪ t<VAR>g : ℕ ↪o ℕ<VAR>hg : ∀ (n : ℕ), f (g n) ∈ s<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r r' : α → α → Prop<VAR>inst✝ : IsStrictOrder α r<VAR>s t : Set α<VAR>hs : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), f n ∈ s<VAR>ht : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), f n ∈ t<VAR>f : (fun x x_1 => x > x_1) ↪r r<VAR>hf : ∀ (n : ℕ), f n ∈ s ∪ t<VAR>g : ℕ ↪o ℕ<VAR>hg : ∀ (n : ℕ), f (g n) ∈ t<GOAL>False
<VAR>E : Type u_1<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : T2Space E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>x : E<VAR>r : ℝ<GOAL>IsCompact (closedBall x r)
<VAR>E : Type u_1<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : T2Space E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>x : E<VAR>r : ℝ<GOAL>IsCompact (⇑toEuclidean.symm '' Metric.closedBall (toEuclidean x) r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝² : FunLike F (Set α) ℝ≥0∞<VAR>inst✝¹ : OuterMeasureClass F α<VAR>μ : F<VAR>s✝ t : Set α<VAR>M : Type u_4<VAR>inst✝ : One M<VAR>f : α → M<VAR>s : Set α<GOAL>s.mulIndicator f =ᶠ[ae μ] 1 ↔ μ (s ∩ Function.mulSupport f) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝² : FunLike F (Set α) ℝ≥0∞<VAR>inst✝¹ : OuterMeasureClass F α<VAR>μ : F<VAR>s✝ t : Set α<VAR>M : Type u_4<VAR>inst✝ : One M<VAR>f : α → M<VAR>s : Set α<GOAL>μ {a | a ∈ s ∧ ¬f a = 1} = 0 ↔ μ (s ∩ Function.mulSupport f) = 0
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>l : List α<GOAL>map singleton ⟦l⟧ ≤ powerset ⟦l⟧
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>l : List α<GOAL>List.map singleton l <+~ List.map ofList l.sublists
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>l : List α<GOAL>List.map (ofList ∘ pure) l <+~ List.map ofList l.sublists
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>l : List α<GOAL>List.map ofList (List.map pure l) <+~ List.map ofList l.sublists
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : LinearOrder β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>i : ι<VAR>i_s : i ∈ s<VAR>b : β<VAR>hb : ∀ (a : β), (∀ᶠ (x : β) in Filter.map (F i) f, (fun x x_1 => x ≤ x_1) x a) → (fun x x_1 => x ≤ x_1) b a<GOAL>IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun a => s.sup' hs fun i => F i a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : LinearOrder β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>i : ι<VAR>i_s : i ∈ s<VAR>b : β<VAR>hb : ∀ (a : β), (∀ᶠ (x : β) in Filter.map (F i) f, (fun x x_1 => x ≤ x_1) x a) → (fun x x_1 => x ≤ x_1) b a<GOAL>∀ (a : β), (∀ᶠ (x : β) in Filter.map (fun a => s.sup' hs fun i => F i a) f, (fun x x_1 => x ≤ x_1) x a) → (fun x x_1 => x ≤ x_1) b a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : LinearOrder β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>i : ι<VAR>i_s : i ∈ s<VAR>b : β<VAR>hb : ∀ (a : β), (∀ᶠ (x : β) in Filter.map (F i) f, (fun x x_1 => x ≤ x_1) x a) → (fun x x_1 => x ≤ x_1) b a<VAR>c : β<VAR>hc : ∀ᶠ (x : β) in Filter.map (fun a => s.sup' hs fun i => F i a) f, (fun x x_1 => x ≤ x_1) x c<GOAL>∀ᶠ (x : β) in Filter.map (F i) f, (fun x x_1 => x ≤ x_1) x c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : LinearOrder β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>i : ι<VAR>i_s : i ∈ s<VAR>b : β<VAR>hb : ∀ (a : β), (∀ᶠ (x : β) in Filter.map (F i) f, (fun x x_1 => x ≤ x_1) x a) → (fun x x_1 => x ≤ x_1) b a<VAR>c : β<VAR>hc : ∀ᶠ (a : α) in f, (fun x x_1 => x ≤ x_1) (s.sup' hs fun i => F i a) c<GOAL>∀ᶠ (a : α) in f, (fun x x_1 => x ≤ x_1) (F i a) c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : LinearOrder β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>i : ι<VAR>i_s : i ∈ s<VAR>b : β<VAR>hb : ∀ (a : β), (∀ᶠ (x : β) in Filter.map (F i) f, (fun x x_1 => x ≤ x_1) x a) → (fun x x_1 => x ≤ x_1) b a<VAR>c : β<VAR>hc : ∀ᶠ (a : α) in f, (fun x x_1 => x ≤ x_1) (s.sup' hs fun i => F i a) c<VAR>a : α<VAR>h : (fun x x_1 => x ≤ x_1) (s.sup' hs fun i => F i a) c<GOAL>(fun x x_1 => x ≤ x_1) (F i a) c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : LinearOrder β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>i : ι<VAR>i_s : i ∈ s<VAR>b : β<VAR>hb : ∀ (a : β), (∀ᶠ (x : β) in Filter.map (F i) f, (fun x x_1 => x ≤ x_1) x a) → (fun x x_1 => x ≤ x_1) b a<VAR>c : β<VAR>hc : ∀ᶠ (a : α) in f, (fun x x_1 => x ≤ x_1) (s.sup' hs fun i => F i a) c<VAR>a : α<VAR>h : ∀ b ∈ s, F b a ≤ c<GOAL>F i a ≤ c
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : CommMonoidWithZero R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : ZeroLEOneClass R<VAR>inst✝ : PosMulMono R<VAR>f g : ι → R<VAR>s t : Finset ι<VAR>h0 : ∀ i ∈ s, 0 ≤ f i<VAR>h1 : ∀ i ∈ s, f i ≤ g i<GOAL>∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : CommMonoidWithZero R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : ZeroLEOneClass R<VAR>inst✝ : PosMulMono R<VAR>f g : ι → R<VAR>s t : Finset ι<VAR>h0 : ∀ i ∈ ∅, 0 ≤ f i<VAR>h1 : ∀ i ∈ ∅, f i ≤ g i<GOAL>∏ i ∈ ∅, f i ≤ ∏ i ∈ ∅, g i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : CommMonoidWithZero R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : ZeroLEOneClass R<VAR>inst✝ : PosMulMono R<VAR>f g : ι → R<VAR>s✝ t : Finset ι<VAR>a : ι<VAR>s : Finset ι<VAR>has : a ∉ s<VAR>ih : (∀ i ∈ s, 0 ≤ f i) → (∀ i ∈ s, f i ≤ g i) → ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i<VAR>h0 : ∀ i ∈ cons a s has, 0 ≤ f i<VAR>h1 : ∀ i ∈ cons a s has, f i ≤ g i<GOAL>∏ i ∈ cons a s has, f i ≤ ∏ i ∈ cons a s has, g i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Preorder β<VAR>inst✝³ : OrderTop α<VAR>inst✝² : OrderBot β<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : LocallyFiniteOrder β<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<GOAL>Ioo (inlₗ a₁) (inlₗ a₂) = map (Embedding.inl.trans toLex.toEmbedding) (Ioo a₁ a₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Preorder β<VAR>inst✝³ : OrderTop α<VAR>inst✝² : OrderBot β<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : LocallyFiniteOrder β<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<GOAL>Ioo (inlₗ a₁) (inlₗ a₂) = map toLex.toEmbedding (map Embedding.inl (Ioo a₁ a₂))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c : ℝ<VAR>f : ↥(Lp E p μ)<VAR>g : ↥(Lp F p μ)<VAR>h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ c * ‖↑↑g x‖<GOAL>‖f‖ ≤ c * ‖g‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c : ℝ<VAR>f : ↥(Lp E p μ)<VAR>g : ↥(Lp F p μ)<VAR>h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ c * ‖↑↑g x‖<VAR>hc : 0 ≤ c<GOAL>‖f‖ ≤ c * ‖g‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c : ℝ<VAR>f : ↥(Lp E p μ)<VAR>g : ↥(Lp F p μ)<VAR>h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ c * ‖↑↑g x‖<VAR>hc : c < 0<GOAL>‖f‖ ≤ c * ‖g‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r : α → α → Prop<VAR>f✝ g : Filter α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : IsDirected β fun x x_1 => x ≤ x_1<VAR>f : ℕ → β<VAR>hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop f<GOAL>BddAbove (range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r : α → α → Prop<VAR>f✝ g : Filter α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : IsDirected β fun x x_1 => x ≤ x_1<VAR>f : ℕ → β<VAR>hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) cofinite f<GOAL>BddAbove (range f)
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u_1<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>x : A<VAR>r : R<VAR>y : A<GOAL>x * ((algebraMap R A) r * y) = (algebraMap R A) r * (x * y)
<VAR>κ μ : Cardinal.{u}<VAR>H1✝ : ℵ₀ ≤ κ<VAR>H2 : μ < ℵ₀<VAR>n : ℕ<VAR>H3 : μ = ↑n<VAR>α : Type u<VAR>H1 : ℵ₀ ≤ ⟦α⟧<GOAL>⟦α⟧ ^ ↑Nat.zero < ℵ₀
<VAR>κ μ : Cardinal.{u}<VAR>H1✝ : ℵ₀ ≤ κ<VAR>H2 : μ < ℵ₀<VAR>n : ℕ<VAR>H3 : μ = ↑n<VAR>α : Type u<VAR>H1 : ℵ₀ ≤ ⟦α⟧<GOAL>1 < ℵ₀
<VAR>κ μ : Cardinal.{u}<VAR>H1✝ : ℵ₀ ≤ κ<VAR>H2 : μ < ℵ₀<VAR>n✝ : ℕ<VAR>H3 : μ = ↑n✝<VAR>α : Type u<VAR>H1 : ℵ₀ ≤ ⟦α⟧<VAR>n : ℕ<VAR>ih : ⟦α⟧ ^ ↑n ≤ ⟦α⟧<GOAL>⟦α⟧ ^ ↑n.succ ≤ ⟦α⟧ * ⟦α⟧
<VAR>κ μ : Cardinal.{u}<VAR>H1✝ : ℵ₀ ≤ κ<VAR>H2 : μ < ℵ₀<VAR>n✝ : ℕ<VAR>H3 : μ = ↑n✝<VAR>α : Type u<VAR>H1 : ℵ₀ ≤ ⟦α⟧<VAR>n : ℕ<VAR>ih : ⟦α⟧ ^ ↑n ≤ ⟦α⟧<GOAL>⟦α⟧ ^ ↑n * ⟦α⟧ ≤ ⟦α⟧ * ⟦α⟧
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivisionMonoid α<VAR>a✝ b c d a : α<VAR>n : ℤ<GOAL>(1 / a) ^ n = 1 / a ^ n
<VAR>R : Type u<VAR>σ : Type v<VAR>a a' a₁ a₂ : R<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : DecidableEq σ<VAR>i j : σ<GOAL>(pderiv i) (X j) = Pi.single i 1 j
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddZeroClass G<VAR>f : k[G]<VAR>r : k<VAR>x a : G<GOAL>0 + a = x ↔ a = x
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>h : f ≠ 0<GOAL>((finSuccEquiv R n) f).support.Nonempty
<VAR>X : Type u<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>Y : Type v<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<GOAL>⟦NonemptyCompacts.kuratowskiEmbedding X⟧ = ⟦NonemptyCompacts.kuratowskiEmbedding Y⟧ → Nonempty (X ≃ᵢ Y)
<VAR>X : Type u<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>Y : Type v<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<GOAL>NonemptyCompacts.kuratowskiEmbedding X ≈ NonemptyCompacts.kuratowskiEmbedding Y → Nonempty (X ≃ᵢ Y)
<VAR>X : Type u<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>Y : Type v<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y)<VAR>I : (↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y)) = (↑(range (kuratowskiEmbedding X)) ≃ᵢ ↑(range (kuratowskiEmbedding Y)))<GOAL>Nonempty (X ≃ᵢ Y)
<VAR>X : Type u<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>Y : Type v<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y)<VAR>I : (↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y)) = (↑(range (kuratowskiEmbedding X)) ≃ᵢ ↑(range (kuratowskiEmbedding Y)))<VAR>f : X ≃ᵢ ↑(range (kuratowskiEmbedding X))<GOAL>Nonempty (X ≃ᵢ Y)
<VAR>X : Type u<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>Y : Type v<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y)<VAR>I : (↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y)) = (↑(range (kuratowskiEmbedding X)) ≃ᵢ ↑(range (kuratowskiEmbedding Y)))<VAR>f : X ≃ᵢ ↑(range (kuratowskiEmbedding X))<VAR>g : ↑(range (kuratowskiEmbedding Y)) ≃ᵢ Y<GOAL>Nonempty (X ≃ᵢ Y)
<VAR>X : Type u<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>Y : Type v<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>e : X ≃ᵢ Y<GOAL>toGHSpace X = toGHSpace Y
<VAR>X : Type u<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>Y : Type v<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>e : X ≃ᵢ Y<GOAL>⟦NonemptyCompacts.kuratowskiEmbedding X⟧ = ⟦NonemptyCompacts.kuratowskiEmbedding Y⟧
<VAR>X : Type u<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>Y : Type v<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>e : X ≃ᵢ Y<VAR>f : ↑(range (kuratowskiEmbedding X)) ≃ᵢ X<GOAL>⟦NonemptyCompacts.kuratowskiEmbedding X⟧ = ⟦NonemptyCompacts.kuratowskiEmbedding Y⟧
<VAR>X : Type u<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>Y : Type v<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>e : X ≃ᵢ Y<VAR>f : ↑(range (kuratowskiEmbedding X)) ≃ᵢ X<VAR>g : Y ≃ᵢ ↑(range (kuratowskiEmbedding Y))<GOAL>⟦NonemptyCompacts.kuratowskiEmbedding X⟧ = ⟦NonemptyCompacts.kuratowskiEmbedding Y⟧
<VAR>X : Type u<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>Y : Type v<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>e : X ≃ᵢ Y<VAR>f : ↑(range (kuratowskiEmbedding X)) ≃ᵢ X<VAR>g : Y ≃ᵢ ↑(range (kuratowskiEmbedding Y))<VAR>I : (↑(range (kuratowskiEmbedding X)) ≃ᵢ ↑(range (kuratowskiEmbedding Y))) = (↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y))<GOAL>⟦NonemptyCompacts.kuratowskiEmbedding X⟧ = ⟦NonemptyCompacts.kuratowskiEmbedding Y⟧
<VAR>X : Type u<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>Y : Type v<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>e : X ≃ᵢ Y<VAR>f : ↑(range (kuratowskiEmbedding X)) ≃ᵢ X<VAR>g : Y ≃ᵢ ↑(range (kuratowskiEmbedding Y))<VAR>I : (↑(range (kuratowskiEmbedding X)) ≃ᵢ ↑(range (kuratowskiEmbedding Y))) = (↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y))<GOAL>NonemptyCompacts.kuratowskiEmbedding X ≈ NonemptyCompacts.kuratowskiEmbedding Y
<VAR>α : Type u_1<GOAL>ofNat' (0 + 1) = ofNat' 0 + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝² : ConditionallyCompleteLattice α<VAR>inst✝¹ : ConditionallyCompleteLattice β<VAR>inst✝ : Nonempty ι<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>f : ι → α<VAR>hf : BddAbove (range f)<GOAL>l (⨆ i, f i) = ⨆ i, l (f i)
<VAR>α : Type u_1<VAR>r✝ r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>s : Set (Set α)<VAR>h₁ : Unbounded r (⋃₀ s)<VAR>h₂ : #↑s < StrictOrder.cof r<GOAL>∃ x ∈ s, Unbounded r x
<VAR>α : Type u_1<VAR>r✝ r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>s : Set (Set α)<VAR>h₁ : Unbounded r (⋃₀ s)<VAR>h₂ : #↑s < StrictOrder.cof r<VAR>h : ∀ x ∈ s, ¬Unbounded r x<GOAL>False
<VAR>α : Type u_1<VAR>r✝ r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>s : Set (Set α)<VAR>h₁ : Unbounded r (⋃₀ s)<VAR>h₂ : #↑s < StrictOrder.cof r<VAR>h : ∀ x ∈ s, Bounded r x<GOAL>False
<VAR>α : Type u_1<VAR>r✝ r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>s : Set (Set α)<VAR>h₁ : Unbounded r (⋃₀ s)<VAR>h₂ : #↑s < StrictOrder.cof r<VAR>h : ∀ x ∈ s, Bounded r x<VAR>f : ↑s → α := fun x => ⋯.sup ↑x ⋯<GOAL>False
<VAR>α : Type u_1<VAR>r✝ r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>s : Set (Set α)<VAR>h₁ : Unbounded r (⋃₀ s)<VAR>h₂ : #↑s < StrictOrder.cof r<VAR>h : ∀ x ∈ s, Bounded r x<VAR>f : ↑s → α := fun x => ⋯.sup ↑x ⋯<VAR>x : α<GOAL>∃ b ∈ range f, swap rᶜ x b
<VAR>α : Type u_1<VAR>r✝ r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>s : Set (Set α)<VAR>h₁ : Unbounded r (⋃₀ s)<VAR>h₂ : #↑s < StrictOrder.cof r<VAR>h : ∀ x ∈ s, Bounded r x<VAR>f : ↑s → α := fun x => ⋯.sup ↑x ⋯<VAR>x y : α<VAR>hxy : ¬r y x<VAR>c : Set α<VAR>hc : c ∈ s<VAR>hy : y ∈ c<GOAL>∃ b ∈ range f, swap rᶜ x b
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommMonoid M'<VAR>inst✝¹ : Module R M'<VAR>b✝ b₁ : Basis ι R M<VAR>i : ι<VAR>c✝ : R<VAR>x✝ : M<VAR>inst✝ : NoZeroDivisors R<VAR>b : Basis ι R M<VAR>c : R<VAR>x : M<VAR>hcx : c • x = 0<GOAL>c = 0 ∨ x = 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n✝ : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x y : 𝕎 R<VAR>n : ℕ<GOAL>init n (x + y) = init n (init n x + init n y)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : FirstCountableTopology X<VAR>Z : Type u_3<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝¹ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝ : ∀ (i : ι), T2Space (π i)<VAR>s : Set ((i : ι) → π i)<GOAL>IsCompact (closure s) ↔ ∀ (i : ι), IsCompact (closure (eval i '' s))