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>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsFiniteKernel η<VAR>hs : MeasurableSet s<GOAL>Measurable fun a => ∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ s} ∂κ a
<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>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsFiniteKernel η<VAR>hs : MeasurableSet s<VAR>h_meas : Measurable (Function.uncurry fun a b => (η (a, b)) {c | (b, c) ∈ s})<GOAL>Measurable fun a => ∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ s} ∂κ a
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝¹ : CompactSpace X<VAR>f : Filter X<VAR>inst✝ : f.NeBot<GOAL>∃ x, ClusterPt x f
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>D✝ D1 D2 : LieDerivation R L M<VAR>a✝ b✝ : L<VAR>D : LieDerivation R L L<VAR>a b : L<GOAL>D ⁅a, b⁆ = ⁅a, D b⁆ + ⁅D a, b⁆
<VAR>q : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>x : ℝ<GOAL>Irrational (↑m * x) ↔ m ≠ 0 ∧ Irrational x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : Set α<VAR>t : (i : ι) → κ i → Set β<GOAL>s ×ˢ ⋃ i, ⋃ j, t i j = ⋃ i, ⋃ j, s ×ˢ t i j
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a : α<GOAL>⌈a⌉ ≤ ⌊a⌋ + 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a : α<GOAL>a ≤ ↑⌊a⌋ + 1
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : β → Sort v<VAR>f : α → β<VAR>g : β → α<VAR>h : LeftInverse g f<VAR>C : (a : α) → γ (f a)<VAR>a : α<GOAL>cast ⋯ (C (g (f a))) = C a
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A<VAR>s : Set G<VAR>p : (x : G) → x ∈ closure s → Prop<VAR>one : p 1 ⋯<VAR>mul_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ closure s), p y hy → p (x * y) ⋯<VAR>mul_left_inv : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ closure s), p y hy → p (x⁻¹ * y) ⋯<VAR>x : G<GOAL>∀ (h : x ∈ closure s), p x h
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A<VAR>s : Set G<VAR>p : (x : G) → x ∈ closure s → Prop<VAR>one : p 1 ⋯<VAR>x : G<VAR>mul_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Submonoid.closure (s ∪ s⁻¹)), p y ⋯ → p (x * y) ⋯<VAR>mul_left_inv : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Submonoid.closure (s ∪ s⁻¹)), p y ⋯ → p (x⁻¹ * y) ⋯<GOAL>∀ (h : x ∈ Submonoid.closure (s ∪ s⁻¹)), p x ⋯
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A<VAR>s : Set G<VAR>p : (x : G) → x ∈ closure s → Prop<VAR>one : p 1 ⋯<VAR>x : G<VAR>mul_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Submonoid.closure (s ∪ s⁻¹)), p y ⋯ → p (x * y) ⋯<VAR>mul_left_inv : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Submonoid.closure (s ∪ s⁻¹)), p y ⋯ → p (x⁻¹ * y) ⋯<VAR>h : x ∈ Submonoid.closure (s ∪ s⁻¹)<GOAL>p x ⋯
<VAR>V : Type u<VAR>G✝ : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G✝.Coloring α<VAR>G : SimpleGraph V<VAR>inst✝ : Subsingleton V<GOAL>G.chromaticNumber ≤ 1
<VAR>V : Type u<VAR>G✝ : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G✝.Coloring α<VAR>G : SimpleGraph V<VAR>inst✝ : Subsingleton V<GOAL>G.Colorable 1
<VAR>V : Type u<VAR>G✝ : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G✝.Coloring α<VAR>G : SimpleGraph V<VAR>inst✝ : Subsingleton V<VAR>v w : V<GOAL>G.Adj v w → (fun x => 0) v ≠ (fun x => 0) w
<VAR>V : Type u<VAR>G✝ : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G✝.Coloring α<VAR>G : SimpleGraph V<VAR>inst✝ : Subsingleton V<VAR>v : V<GOAL>G.Adj v v → (fun x => 0) v ≠ (fun x => 0) v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<GOAL>Memℒp (↑↑(condexpIndSMul hm hs hμs x)) 1 μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<GOAL>Integrable (↑↑(condexpIndSMul hm hs hμs x)) μ
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝³ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ : Ω → ι<VAR>inst✝² : TopologicalSpace ι<VAR>inst✝¹ : OrderTopology ι<VAR>inst✝ : FirstCountableTopology ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<GOAL>MeasurableSet {ω | τ ω < i}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝³ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ : Ω → ι<VAR>inst✝² : TopologicalSpace ι<VAR>inst✝¹ : OrderTopology ι<VAR>inst✝ : FirstCountableTopology ι<VAR>hτ : IsStoppingTime f τ<VAR>i i' : ι<VAR>hi'_lub : IsLUB (Set.Iio i) i'<GOAL>MeasurableSet {ω | τ ω < i}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝³ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ : Ω → ι<VAR>inst✝² : TopologicalSpace ι<VAR>inst✝¹ : OrderTopology ι<VAR>inst✝ : FirstCountableTopology ι<VAR>hτ : IsStoppingTime f τ<VAR>i i' : ι<VAR>hi'_lub : IsLUB (Set.Iio i) i'<VAR>hi'_eq_i : i' = i<GOAL>MeasurableSet {ω | τ ω < i}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝³ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ : Ω → ι<VAR>inst✝² : TopologicalSpace ι<VAR>inst✝¹ : OrderTopology ι<VAR>inst✝ : FirstCountableTopology ι<VAR>hτ : IsStoppingTime f τ<VAR>i i' : ι<VAR>hi'_lub : IsLUB (Set.Iio i) i'<VAR>h_Iio_eq_Iic : Set.Iio i = Set.Iic i'<GOAL>MeasurableSet {ω | τ ω < i}
<VAR>x✝ y✝ z : ℝ<VAR>n✝ : ℕ<VAR>x : ℝ<VAR>hx : x ≠ 0<VAR>y : ℝ<VAR>n : ℕ<GOAL>x ^ (y - ↑n) = x ^ y / x ^ n
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t u : Finset α<VAR>P : Finpartition s<VAR>a : α<GOAL>s.card % P.parts.card ≤ P.parts.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t u : Finset α<VAR>P : Finpartition s<VAR>a : α<VAR>h : P.parts.card = 0<GOAL>s.card % P.parts.card ≤ P.parts.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t u : Finset α<VAR>P : Finpartition s<VAR>a : α<VAR>h : P.parts.card > 0<GOAL>s.card % P.parts.card ≤ P.parts.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>f : α → PMF β<VAR>g : β → PMF γ<VAR>s : Set β<GOAL>(p.bind f).toOuterMeasure s = ∑' (b : β), if b ∈ s then ∑' (a : α), p a * (f a) b else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>f : α → PMF β<VAR>g : β → PMF γ<VAR>s : Set β<VAR>a : α<GOAL>(p a * ∑' (b : β), if b ∈ s then (f a) b else 0) = p a * (f a).toOuterMeasure s
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>x y : ℝ<GOAL>(√(2 * π * ↑v))⁻¹ * rexp (-(x - y - μ) ^ 2 / (2 * ↑v)) = (√(2 * π * ↑v))⁻¹ * rexp (-(x - (μ + y)) ^ 2 / (2 * ↑v))
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>n : ℕ<VAR>inst✝ : CompleteSpace E<VAR>I : Box (Fin (n + 1))<VAR>i : Fin (n + 1)<VAR>f : (Fin (n + 1) → ℝ) → E<VAR>f' : (Fin (n + 1) → ℝ) →L[ℝ] E<VAR>hfc : ContinuousOn f (Box.Icc I)<VAR>x : Fin (n + 1) → ℝ<VAR>hxI : x ∈ Box.Icc I<VAR>a : E<VAR>ε : ℝ<VAR>h0 : 0 < ε<VAR>hε : ∀ y ∈ Box.Icc I, ‖f y - a - f' (y - x)‖ ≤ ε * ‖y - x‖<VAR>c : ℝ≥0<VAR>hc : I.distortion ≤ c<VAR>e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth<GOAL>‖(∏ j : Fin (n + 1), (I.upper j - I.lower j)) • f' (Pi.single i 1) - (integral (I.face i) ⊥ (f ∘ e (I.upper i)) BoxAdditiveMap.volume - integral (I.face i) ⊥ (f ∘ e (I.lower i)) BoxAdditiveMap.volume)‖ ≤ 2 * ε * ↑c * ∏ j : Fin (n + 1), (I.upper j - I.lower j)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>n : ℕ<VAR>inst✝ : CompleteSpace E<VAR>I : Box (Fin (n + 1))<VAR>i : Fin (n + 1)<VAR>f : (Fin (n + 1) → ℝ) → E<VAR>f' : (Fin (n + 1) → ℝ) →L[ℝ] E<VAR>hfc : ContinuousOn f (Box.Icc I)<VAR>x : Fin (n + 1) → ℝ<VAR>hxI : x ∈ Box.Icc I<VAR>a : E<VAR>ε : ℝ<VAR>h0 : 0 < ε<VAR>hε : ∀ y ∈ Box.Icc I, ‖f y - a - f' (y - x)‖ ≤ ε * ‖y - x‖<VAR>c : ℝ≥0<VAR>hc : I.distortion ≤ c<VAR>e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth<VAR>Hl : I.lower i ∈ Set.Icc (I.lower i) (I.upper i)<GOAL>‖(∏ j : Fin (n + 1), (I.upper j - I.lower j)) • f' (Pi.single i 1) - (integral (I.face i) ⊥ (f ∘ e (I.upper i)) BoxAdditiveMap.volume - integral (I.face i) ⊥ (f ∘ e (I.lower i)) BoxAdditiveMap.volume)‖ ≤ 2 * ε * ↑c * ∏ j : Fin (n + 1), (I.upper j - I.lower j)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>n : ℕ<VAR>inst✝ : CompleteSpace E<VAR>I : Box (Fin (n + 1))<VAR>i : Fin (n + 1)<VAR>f : (Fin (n + 1) → ℝ) → E<VAR>f' : (Fin (n + 1) → ℝ) →L[ℝ] E<VAR>hfc : ContinuousOn f (Box.Icc I)<VAR>x : Fin (n + 1) → ℝ<VAR>hxI : x ∈ Box.Icc I<VAR>a : E<VAR>ε : ℝ<VAR>h0 : 0 < ε<VAR>hε : ∀ y ∈ Box.Icc I, ‖f y - a - f' (y - x)‖ ≤ ε * ‖y - x‖<VAR>c : ℝ≥0<VAR>hc : I.distortion ≤ c<VAR>e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth<VAR>Hl : I.lower i ∈ Set.Icc (I.lower i) (I.upper i)<VAR>Hu : I.upper i ∈ Set.Icc (I.lower i) (I.upper i)<GOAL>‖(∏ j : Fin (n + 1), (I.upper j - I.lower j)) • f' (Pi.single i 1) - (integral (I.face i) ⊥ (f ∘ e (I.upper i)) BoxAdditiveMap.volume - integral (I.face i) ⊥ (f ∘ e (I.lower i)) BoxAdditiveMap.volume)‖ ≤ 2 * ε * ↑c * ∏ j : Fin (n + 1), (I.upper j - I.lower j)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>n : ℕ<VAR>inst✝ : CompleteSpace E<VAR>I : Box (Fin (n + 1))<VAR>i : Fin (n + 1)<VAR>f : (Fin (n + 1) → ℝ) → E<VAR>f' : (Fin (n + 1) → ℝ) →L[ℝ] E<VAR>hfc : ContinuousOn f (Box.Icc I)<VAR>x : Fin (n + 1) → ℝ<VAR>hxI : x ∈ Box.Icc I<VAR>a : E<VAR>ε : ℝ<VAR>h0 : 0 < ε<VAR>hε : ∀ y ∈ Box.Icc I, ‖f y - a - f' (y - x)‖ ≤ ε * ‖y - x‖<VAR>c : ℝ≥0<VAR>hc : I.distortion ≤ c<VAR>e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth<VAR>Hl : I.lower i ∈ Set.Icc (I.lower i) (I.upper i)<VAR>Hu : I.upper i ∈ Set.Icc (I.lower i) (I.upper i)<VAR>Hi : ∀ x ∈ Set.Icc (I.lower i) (I.upper i), Integrable (I.face i) ⊥ (f ∘ e x) BoxAdditiveMap.volume<GOAL>‖(∏ j : Fin (n + 1), (I.upper j - I.lower j)) • f' (Pi.single i 1) - (integral (I.face i) ⊥ (f ∘ e (I.upper i)) BoxAdditiveMap.volume - integral (I.face i) ⊥ (f ∘ e (I.lower i)) BoxAdditiveMap.volume)‖ ≤ 2 * ε * ↑c * ∏ j : Fin (n + 1), (I.upper j - I.lower j)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁷ : NormedField 𝕜<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜 E<VAR>inst✝⁴ : NormedField 𝕜₂<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : TopologicalSpace F<VAR>hι : Nonempty ι<VAR>q : SeminormFamily 𝕜₂ F ι<VAR>hq : WithSeminorms q<VAR>f : E →ₛₗ[σ₁₂] F<GOAL>WithSeminorms (q.comp f)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁷ : NormedField 𝕜<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜 E<VAR>inst✝⁴ : NormedField 𝕜₂<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : TopologicalSpace F<VAR>hι : Nonempty ι<VAR>q : SeminormFamily 𝕜₂ F ι<VAR>hq : WithSeminorms q<VAR>f : E →ₛₗ[σ₁₂] F<VAR>this : TopologicalAddGroup F<GOAL>WithSeminorms (q.comp f)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁷ : NormedField 𝕜<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜 E<VAR>inst✝⁴ : NormedField 𝕜₂<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : TopologicalSpace F<VAR>hι : Nonempty ι<VAR>q : SeminormFamily 𝕜₂ F ι<VAR>hq : WithSeminorms q<VAR>f : E →ₛₗ[σ₁₂] F<VAR>this : TopologicalAddGroup F<VAR>x✝ : TopologicalSpace E := TopologicalSpace.induced (⇑f) inferInstance<GOAL>WithSeminorms (q.comp f)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁷ : NormedField 𝕜<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜 E<VAR>inst✝⁴ : NormedField 𝕜₂<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : TopologicalSpace F<VAR>hι : Nonempty ι<VAR>q : SeminormFamily 𝕜₂ F ι<VAR>hq : WithSeminorms q<VAR>f : E →ₛₗ[σ₁₂] F<VAR>this✝ : TopologicalAddGroup F<VAR>x✝ : TopologicalSpace E := TopologicalSpace.induced (⇑f) inferInstance<VAR>this : TopologicalAddGroup E<GOAL>WithSeminorms (q.comp f)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁷ : NormedField 𝕜<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜 E<VAR>inst✝⁴ : NormedField 𝕜₂<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : TopologicalSpace F<VAR>hι : Nonempty ι<VAR>q : SeminormFamily 𝕜₂ F ι<VAR>hq : WithSeminorms q<VAR>f : E →ₛₗ[σ₁₂] F<VAR>this✝ : TopologicalAddGroup F<VAR>x✝ : TopologicalSpace E := TopologicalSpace.induced (⇑f) inferInstance<VAR>this : TopologicalAddGroup E<GOAL>⨅ i, comap (⇑f) (comap (⇑(q i)) (𝓝 0)) = ⨅ i, comap (⇑(q.comp f i)) (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁷ : NormedField 𝕜<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜 E<VAR>inst✝⁴ : NormedField 𝕜₂<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : TopologicalSpace F<VAR>hι : Nonempty ι<VAR>q : SeminormFamily 𝕜₂ F ι<VAR>hq : WithSeminorms q<VAR>f : E →ₛₗ[σ₁₂] F<VAR>this✝ : TopologicalAddGroup F<VAR>x✝ : TopologicalSpace E := TopologicalSpace.induced (⇑f) inferInstance<VAR>this : TopologicalAddGroup E<VAR>i : ι<GOAL>comap (⇑f) (comap (⇑(q i)) (𝓝 0)) = comap (⇑(q.comp f i)) (𝓝 0)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : SeminormedAddCommGroup F<VAR>f : ι → E<GOAL>(CauchySeq fun s => ∑ i ∈ s, f i) ↔ ∀ ε > 0, ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, f i‖ < ε
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : SeminormedAddCommGroup F<VAR>f : ι → E<GOAL>(∀ (i : ℝ), 0 < i → ∃ s, ∀ (t : Finset ι), Disjoint t s → ∑ b ∈ t, f b ∈ ball 0 i) ↔ ∀ ε > 0, ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, f i‖ < ε
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : SeminormedAddCommGroup F<VAR>f : ι → E<GOAL>∀ ⦃s t : Set E⦄, s ⊆ t → (∃ s_1, ∀ (t : Finset ι), Disjoint t s_1 → ∑ b ∈ t, f b ∈ s) → ∃ s, ∀ (t_1 : Finset ι), Disjoint t_1 s → ∑ b ∈ t_1, f b ∈ t
<VAR>f g : CircleDeg1Lift<VAR>n : ℤ<GOAL>Function.Commute ⇑f fun x => x - ↑n
<VAR>a b c d a' b' c' : Ordinal.{u}<VAR>ha : a' < a<VAR>hb : b' < b<VAR>hc : c' < c<GOAL>a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' < a ⨳ b ⨳ c ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>a b : α<VAR>n : ℕ<VAR>h : a ∉ s<VAR>m : { x // x ∈ (insert a s).sym n }<GOAL>(Sym.filterNe a ↑m).snd ∈ s.sym (n - ↑(Sym.filterNe a ↑m).fst)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>a b : α<VAR>n : ℕ<VAR>h : a ∉ s<VAR>m : { x // x ∈ (insert a s).sym n }<GOAL>s = (insert a s).erase a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>a b : α<VAR>n : ℕ<VAR>h : a ∉ s<VAR>x✝ : (i : Fin (n + 1)) × { x // x ∈ s.sym (n - ↑i) }<VAR>i : Fin (n + 1)<VAR>m : Sym α (n - ↑i)<VAR>hm : m ∈ s.sym (n - ↑i)<GOAL>(fun m => ⟨(Sym.filterNe a ↑m).fst, ⟨(Sym.filterNe a ↑m).snd, ⋯⟩⟩) ((fun m => ⟨Sym.fill a m.fst ↑m.snd, ⋯⟩) ⟨i, ⟨m, hm⟩⟩) = ⟨i, ⟨m, hm⟩⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>a b : α<VAR>n : ℕ<VAR>h : a ∉ s<VAR>x✝ : (i : Fin (n + 1)) × { x // x ∈ s.sym (n - ↑i) }<VAR>i : Fin (n + 1)<VAR>m : Sym α (n - ↑i)<VAR>hm : m ∈ s.sym (n - ↑i)<GOAL>Fin (n + 1) → Type ?u.79991
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>a b : α<VAR>n : ℕ<VAR>h : a ∉ s<VAR>x✝ : (i : Fin (n + 1)) × { x // x ∈ s.sym (n - ↑i) }<VAR>i : Fin (n + 1)<VAR>m : Sym α (n - ↑i)<VAR>hm : m ∈ s.sym (n - ↑i)<GOAL>(a : Fin (n + 1)) → { x // x ∈ s.sym (n - ↑a) } → ?refine_1 (id a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>a b : α<VAR>n : ℕ<VAR>h : a ∉ s<VAR>x✝ : (i : Fin (n + 1)) × { x // x ∈ s.sym (n - ↑i) }<VAR>i✝ : Fin (n + 1)<VAR>m : Sym α (n - ↑i✝)<VAR>hm : m ∈ s.sym (n - ↑i✝)<VAR>i : Fin (n + 1)<GOAL>Function.Injective (?refine_2 i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>a b : α<VAR>n : ℕ<VAR>h : a ∉ s<VAR>x✝ : (i : Fin (n + 1)) × { x // x ∈ s.sym (n - ↑i) }<VAR>i : Fin (n + 1)<VAR>m : Sym α (n - ↑i)<VAR>hm : m ∈ s.sym (n - ↑i)<GOAL>Sigma.map id ?refine_2 ((fun m => ⟨(Sym.filterNe a ↑m).fst, ⟨(Sym.filterNe a ↑m).snd, ⋯⟩⟩) ((fun m => ⟨Sym.fill a m.fst ↑m.snd, ⋯⟩) ⟨i, ⟨m, hm⟩⟩)) = Sigma.map id ?refine_2 ⟨i, ⟨m, hm⟩⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>a b : α<VAR>n : ℕ<VAR>h : a ∉ s<VAR>x✝ : (i : Fin (n + 1)) × { x // x ∈ s.sym (n - ↑i) }<VAR>i : Fin (n + 1)<VAR>m : Sym α (n - ↑i)<VAR>hm : m ∈ s.sym (n - ↑i)<GOAL>Sigma.map id (fun i a => ↑a) ((fun m => ⟨(Sym.filterNe a ↑m).fst, ⟨(Sym.filterNe a ↑m).snd, ⋯⟩⟩) ((fun m => ⟨Sym.fill a m.fst ↑m.snd, ⋯⟩) ⟨i, ⟨m, hm⟩⟩)) = Sigma.map id (fun i a => ↑a) ⟨i, ⟨m, hm⟩⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>a b : α<VAR>n : ℕ<VAR>h : a ∉ s<VAR>x✝ : (i : Fin (n + 1)) × { x // x ∈ s.sym (n - ↑i) }<VAR>i : Fin (n + 1)<VAR>m : Sym α (n - ↑i)<VAR>hm : m ∈ s.sym (n - ↑i)<GOAL>Sigma.map id (fun i a => ↑a) ((fun m => ⟨(Sym.filterNe a ↑m).fst, ⟨(Sym.filterNe a ↑m).snd, ⋯⟩⟩) ((fun m => ⟨Sym.fill a m.fst ↑m.snd, ⋯⟩) ⟨i, ⟨m, hm⟩⟩)) = Sym.filterNe a (Sym.fill a (Sigma.map id (fun i a => ↑a) ⟨i, ⟨m, hm⟩⟩).fst (Sigma.map id (fun i a => ↑a) ⟨i, ⟨m, hm⟩⟩).snd)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>a b : α<VAR>n : ℕ<VAR>h : a ∉ s<VAR>x✝ : (i : Fin (n + 1)) × { x // x ∈ s.sym (n - ↑i) }<VAR>i : Fin (n + 1)<VAR>m : Sym α (n - ↑i)<VAR>hm : m ∈ s.sym (n - ↑i)<GOAL>a ∉ (Sigma.map id (fun i a => ↑a) ⟨i, ⟨m, hm⟩⟩).snd
<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>b' : Basis ι' R M'<VAR>i : ι ⊕ ι'<GOAL>(b.prod b') i = Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') i
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>m : Multiset E<GOAL>‖m.prod‖ ≤ (Multiset.map toReal (Multiset.map (fun x => ‖x‖₊) m)).sum
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>m : Multiset E<GOAL>‖m.prod‖ ≤ (Multiset.map (toReal ∘ fun x => ‖x‖₊) m).sum
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f✝ f : R →+* S<VAR>s : S<VAR>h : s ∈ Set.range ⇑f<GOAL>C s ∈ lifts f
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f✝ f : R →+* S<VAR>r : R<VAR>h : f r ∈ Set.range ⇑f<GOAL>C (f r) ∈ lifts f
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f✝ f : R →+* S<VAR>r : R<VAR>h : f r ∈ Set.range ⇑f<GOAL>(mapRingHom f) (C r) = C (f r)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CancelCommMonoid α<VAR>inst✝ : CancelCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hf : IsMulFreimanIso n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = m<VAR>ht : card t = m<GOAL>(map f s).prod = (map f t).prod ↔ s.prod = t.prod
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CancelCommMonoid α<VAR>inst✝ : CancelCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>n : ℕ<VAR>hf : IsMulFreimanIso n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hmn : 0 ≤ n<VAR>hs : card s = 0<VAR>ht : card t = 0<GOAL>(map f s).prod = (map f t).prod ↔ s.prod = t.prod
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CancelCommMonoid α<VAR>inst✝ : CancelCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hf : IsMulFreimanIso n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = m<VAR>ht : card t = m<VAR>hm : m > 0<GOAL>(map f s).prod = (map f t).prod ↔ s.prod = t.prod
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CancelCommMonoid α<VAR>inst✝ : CancelCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hf : IsMulFreimanIso n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = m<VAR>ht : card t = m<VAR>hm : ∃ a, a ∈ s<GOAL>(map f s).prod = (map f t).prod ↔ s.prod = t.prod
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CancelCommMonoid α<VAR>inst✝ : CancelCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hf : IsMulFreimanIso n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = m<VAR>ht : card t = m<VAR>a : α<VAR>ha : a ∈ s<GOAL>(map f s).prod = (map f t).prod ↔ s.prod = t.prod