ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r✝ r' : ℝ≥0∞<VAR>n m : ℕ<VAR>hf : HasFiniteFPowerSeriesAt f pf x n<VAR>hg : HasFiniteFPowerSeriesAt g pg x m<VAR>r : ℝ≥0∞<VAR>hr : HasFiniteFPowerSeriesOnBall f pf x n r ∧ HasFiniteFPowerSeriesOnBall g pg x m r<GOAL>HasFiniteFPowerSeriesAt (f + g) (pf + pg) x (max n m)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s✝ t✝ : Set α<VAR>x : α<VAR>δ : ℝ<VAR>s t : Set α<GOAL>thickening δ (s ∪ t) = thickening δ s ∪ thickening δ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : Countable ι<VAR>t : ι → TopologicalSpace α<VAR>ht : ∀ (i : ι), PolishSpace α<VAR>i₀ : ι<VAR>hi₀ : ∀ (i : ι), t i ≤ t i₀<GOAL>PolishSpace α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : Countable ι<VAR>t : ι → TopologicalSpace α<VAR>ht : ∀ (i : ι), PolishSpace α<VAR>i₀ : ι<VAR>hi₀ : ∀ (i : ι), t i ≤ t i₀<VAR>u : UniformSpace α<VAR>hcomp : CompleteSpace α<VAR>hcount : (𝓤 α).IsCountablyGenerated<VAR>htop : UniformSpace.toTopologicalSpace = ⨅ i, t i<GOAL>PolishSpace α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : Countable ι<VAR>t : ι → TopologicalSpace α<VAR>ht : ∀ (i : ι), PolishSpace α<VAR>i₀ : ι<VAR>hi₀ : ∀ (i : ι), t i ≤ t i₀<VAR>u : UniformSpace α<VAR>hcomp : CompleteSpace α<VAR>hcount : (𝓤 α).IsCountablyGenerated<VAR>htop : UniformSpace.toTopologicalSpace = ⨅ i, t i<VAR>this : SecondCountableTopology α<GOAL>PolishSpace α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : Countable ι<VAR>t : ι → TopologicalSpace α<VAR>ht : ∀ (i : ι), PolishSpace α<VAR>i₀ : ι<VAR>hi₀ : ∀ (i : ι), t i ≤ t i₀<VAR>u : UniformSpace α<VAR>hcomp : CompleteSpace α<VAR>hcount : (𝓤 α).IsCountablyGenerated<VAR>htop : UniformSpace.toTopologicalSpace = ⨅ i, t i<VAR>this✝ : SecondCountableTopology α<VAR>this : T1Space α<GOAL>PolishSpace α
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>S' : Type u_1<VAR>inst✝ : CommSemiring S'<VAR>f : R →+* S<VAR>a✝ : PrimeSpectrum R<VAR>x✝ : R<GOAL>x✝ ∈ ((comap (RingHom.id R)) a✝).asIdeal ↔ x✝ ∈ ((ContinuousMap.id (PrimeSpectrum R)) a✝).asIdeal
<VAR>Q : Type u_1<VAR>inst✝¹ : Quandle Q<VAR>G : Type u_2<VAR>inst✝ : Group G<VAR>x y : Conj G<GOAL>x * y * x⁻¹ = y → y * x * y⁻¹ = x
<VAR>Q : Type u_1<VAR>inst✝¹ : Quandle Q<VAR>G : Type u_2<VAR>inst✝ : Group G<VAR>x y : Conj G<GOAL>y * x * y⁻¹ = x → x * y * x⁻¹ = y
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.247016, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>f g : ComposableArrows C 3<VAR>app₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯<VAR>app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯<VAR>app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯<VAR>app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯<VAR>w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁ = app₀ ≫ g.map' 0 1 ⋯ ⋯<VAR>w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂ = app₁ ≫ g.map' 1 2 ⋯ ⋯<VAR>w₂ : f.map' 2 3 ⋯ ⋯ ≫ app₃ = app₂ ≫ g.map' 2 3 ⋯ ⋯<GOAL>2 < 3 + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁✝ a₂✝ : α<VAR>b✝ b₁ b₂ : β<VAR>γ : Type u_3<VAR>inst✝⁸ : Zero α<VAR>inst✝⁷ : Preorder α<VAR>inst✝⁶ : Zero β<VAR>inst✝⁵ : Preorder β<VAR>inst✝⁴ : Zero γ<VAR>inst✝³ : Preorder γ<VAR>inst✝² : SMul α β<VAR>inst✝¹ : SMul α γ<VAR>f : β → γ<VAR>inst✝ : SMulPosStrictMono α γ<VAR>hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂<VAR>smul : ∀ (a : α) (b : β), f (a • b) = a • f b<VAR>zero : f 0 = 0<VAR>b : β<VAR>hb : 0 < b<VAR>a₁ a₂ : α<VAR>ha : a₁ < a₂<GOAL>a₁ • b < a₂ • b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁✝ a₂✝ : α<VAR>b✝ b₁ b₂ : β<VAR>γ : Type u_3<VAR>inst✝⁸ : Zero α<VAR>inst✝⁷ : Preorder α<VAR>inst✝⁶ : Zero β<VAR>inst✝⁵ : Preorder β<VAR>inst✝⁴ : Zero γ<VAR>inst✝³ : Preorder γ<VAR>inst✝² : SMul α β<VAR>inst✝¹ : SMul α γ<VAR>f : β → γ<VAR>inst✝ : SMulPosStrictMono α γ<VAR>hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂<VAR>b : β<VAR>a₁ a₂ : α<VAR>ha : a₁ < a₂<VAR>smul : α → β → True<VAR>zero : True<VAR>hb : 0 < f b<GOAL>a₁ • f b < a₂ • f b
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>A : Type u_2<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>M : Type u_3<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module A M<VAR>inst✝³ : Module R M<VAR>D✝ D1 D2 : Derivation R A M<VAR>r : R<VAR>a✝ b : A<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Module K M<VAR>inst✝ : Algebra R K<VAR>D : Derivation R K M<VAR>a : K<VAR>n : ℤ<VAR>hn : ¬n = 0<VAR>ha : ¬a = 0<GOAL>D (a ^ n) = n • a ^ (n - 1) • D a
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>A : Type u_2<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>M : Type u_3<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module A M<VAR>inst✝³ : Module R M<VAR>D✝ D1 D2 : Derivation R A M<VAR>r : R<VAR>a✝ b : A<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Module K M<VAR>inst✝ : Algebra R K<VAR>D : Derivation R K M<VAR>a : K<VAR>n : ℤ<VAR>hn : ¬n = 0<VAR>ha : ¬a = 0<VAR>h : n = ↑n.natAbs<GOAL>D (a ^ n) = n • a ^ (n - 1) • D a
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>A : Type u_2<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>M : Type u_3<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module A M<VAR>inst✝³ : Module R M<VAR>D✝ D1 D2 : Derivation R A M<VAR>r : R<VAR>a✝ b : A<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Module K M<VAR>inst✝ : Algebra R K<VAR>D : Derivation R K M<VAR>a : K<VAR>n : ℤ<VAR>hn : ¬n = 0<VAR>ha : ¬a = 0<VAR>h : n = -↑n.natAbs<GOAL>D (a ^ n) = n • a ^ (n - 1) • D a
<VAR>α : Type u_1<VAR>inst✝ : Mul α<VAR>a x y : αᵐᵒᵖ<GOAL>SemiconjBy (unop a) (unop y) (unop x) ↔ SemiconjBy a x y
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : DecidableEq α<VAR>P : Finset α → Prop<VAR>s : Finset α<VAR>hP : ∀ ⦃s t : Finset α⦄, P s → s ⊆ t → P t<GOAL>s ∈ minimals (fun x x_1 => x ⊆ x_1) {t | P t} ↔ P s ∧ ∀ x ∈ s, ¬P (s.erase x)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : DecidableEq α<VAR>P : Finset α → Prop<VAR>s : Finset α<VAR>hP : ∀ ⦃s t : Finset α⦄, P s → s ⊆ t → P t<GOAL>P s → ((∀ ⦃y : Finset α⦄, P y → y ⊆ s → s = y) ↔ ∀ x ∈ s, ¬P (s.erase x))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : DecidableEq α<VAR>P : Finset α → Prop<VAR>s : Finset α<VAR>hP : ∀ ⦃s t : Finset α⦄, P s → s ⊆ t → P t<VAR>x✝ : P s<VAR>h : ∀ ⦃y : Finset α⦄, P y → y ⊆ s → s = y<VAR>x : α<VAR>hx : x ∈ s<VAR>hxs : P (s.erase x)<GOAL>False
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : DecidableEq α<VAR>P : Finset α → Prop<VAR>s : Finset α<VAR>hP : ∀ ⦃s t : Finset α⦄, P s → s ⊆ t → P t<VAR>x✝ : P s<VAR>h : ∀ x ∈ s, ¬P (s.erase x)<VAR>t : Finset α<VAR>ht : P t<VAR>hst : t ⊆ s<VAR>x : α<VAR>hxs : x ∈ s<GOAL>x ∈ t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<GOAL>Tendsto Int.cast Filter.cofinite (cocompact ℝ)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<GOAL>DiscreteTopology ↥(castAddHom ℝ).range
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<GOAL>DiscreteTopology ↥(AddSubgroup.zmultiples 1)
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>n : ℕ<VAR>hp : ∀ n' < n, ¬p n'<GOAL>count p n = 0
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>n : ℕ<VAR>hp : ∀ n' < n, ¬p n'<GOAL>∀ x ∈ range n, ¬p x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>r : ℚ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>inst✝ : IsFiniteMeasure ρ<GOAL>∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst = (ρ.IicSnd ↑r) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>r : ℚ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>inst✝ : IsFiniteMeasure ρ<VAR>this : ∀ (r : ℚ), ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst = ∫⁻ (x : α) in s, (preCDF ρ r * 1) x ∂ρ.fst<GOAL>∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst = (ρ.IicSnd ↑r) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>r : ℚ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>inst✝ : IsFiniteMeasure ρ<VAR>this : ∀ (r : ℚ), ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst = ∫⁻ (x : α) in s, (preCDF ρ r * 1) x ∂ρ.fst<GOAL>∫⁻ (x : α) in s, 1 x ∂ρ.fst.withDensity (preCDF ρ r) = (ρ.IicSnd ↑r) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>r : ℚ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>inst✝ : IsFiniteMeasure ρ<VAR>this : ∀ (r : ℚ), ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst = ∫⁻ (x : α) in s, (preCDF ρ r * 1) x ∂ρ.fst<GOAL>Measurable 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Mul G<VAR>inst✝ : Mul H<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>h : UniqueMul (map { toFun := op, inj' := ⋯ } B) (map { toFun := op, inj' := ⋯ } A) (op b0) (op a0)<VAR>a b : G<VAR>aA : a ∈ A<VAR>bB : b ∈ B<VAR>ab : a * b = a0 * b0<GOAL>a = a0 ∧ b = b0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : Semiring R<VAR>a : Rˣ<VAR>b : R<GOAL>↑a + b = ↑a * (1 + ↑a⁻¹ * b)
<VAR>n : ℕ<VAR>x r : ℝ<GOAL>expNear (n + 1) x r = expNear n x (1 + x / (↑n + 1) * r)
<VAR>n : ℕ<VAR>x r : ℝ<GOAL>x ^ n * x * ((↑n.factorial)⁻¹ * (↑n + 1)⁻¹) * r = x ^ n * (↑n.factorial)⁻¹ * (x * (↑n + 1)⁻¹ * r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>h : InjOn f s<VAR>x✝¹ x✝ : ↑s<VAR>x : α<VAR>hx : x ∈ s<VAR>y : α<VAR>hy : y ∈ s<VAR>h' : imageFactorization f s ⟨x, hx⟩ = imageFactorization f s ⟨y, hy⟩<GOAL>⟨x, hx⟩ = ⟨y, hy⟩
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n l : ℕ<VAR>φ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v : α → M<VAR>xs : Fin l → M<GOAL>(φ ⇔ ψ).Realize v xs ↔ (φ.Realize v xs ↔ ψ.Realize v xs)
<VAR>R : Type u<GOAL>√2 ^ 4 = √2 * (√2)⁻¹ * 4
<VAR>R : Type u<GOAL>√2 ^ 4 = 1 * 4
<VAR>a b c : ℕ<VAR>r : ℤ<VAR>ha : a % 2 = 0<VAR>hb : b % 8 = 5<VAR>hc : a / 2 = c<VAR>hr : jacobiSymNat c b = r<GOAL>jacobiSymNat a b = -r
<VAR>a b c : ℕ<VAR>r : ℤ<VAR>ha : a % 2 = 0<VAR>hb : b % 8 = 5<VAR>hc : a / 2 = c<VAR>hr : jacobiSymNat c b = r<GOAL>jacobiSym (↑a) b = -jacobiSym (↑a / 2) b
<VAR>a b c : ℕ<VAR>r : ℤ<VAR>ha : a % 2 = 0<VAR>hb : b % 8 = 5<VAR>hc : a / 2 = c<VAR>hr : jacobiSymNat c b = r<GOAL>b % 2 = 1
<VAR>a b c : ℕ<VAR>r : ℤ<VAR>ha : a % 2 = 0<VAR>hb : b % 8 = 5<VAR>hc : a / 2 = c<VAR>hr : jacobiSymNat c b = r<GOAL>2 ∣ 8
<VAR>α : Type u_1<VAR>inst✝ : CompleteLattice α<VAR>u : ℕ → α<VAR>n : ℕ<GOAL>⨆ k, ⨆ (_ : k < n + 1), u k = (⨆ k, ⨆ (_ : k < n), u k) ⊔ u n
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : CoreHomEquiv F G<VAR>X' X : C<VAR>Y Y' : D<VAR>f : X' ⟶ X<VAR>g : F.obj X ⟶ Y<GOAL>(adj.homEquiv X' (F.obj X)) (F.map f) ≫ G.map g = f ≫ (adj.homEquiv X Y) g
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t✝ : Set α<VAR>t : Set ↑s<VAR>hs : NullMeasurableSet s μ<VAR>ht : MeasurableSet t<GOAL>NullMeasurableSet (Subtype.val '' t) μ
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t✝ : Set α<VAR>t : Set ↑s<VAR>hs : NullMeasurableSet s μ<VAR>ht : MeasurableSet t<GOAL>∀ t ∈ {t | ∃ s', MeasurableSet s' ∧ Subtype.val ⁻¹' s' = t}, (fun t => NullMeasurableSet (Subtype.val '' t) μ) t
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t✝ : Set α<VAR>t : Set ↑s<VAR>hs : NullMeasurableSet s μ<VAR>ht : MeasurableSet t<GOAL>(fun t => NullMeasurableSet (Subtype.val '' t) μ) ∅
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t✝ : Set α<VAR>t : Set ↑s<VAR>hs : NullMeasurableSet s μ<VAR>ht : MeasurableSet t<GOAL>∀ (t : Set ↑s), (fun t => NullMeasurableSet (Subtype.val '' t) μ) t → (fun t => NullMeasurableSet (Subtype.val '' t) μ) tᶜ
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t✝ : Set α<VAR>t : Set ↑s<VAR>hs : NullMeasurableSet s μ<VAR>ht : MeasurableSet t<GOAL>∀ (f : ℕ → Set ↑s), (∀ (n : ℕ), (fun t => NullMeasurableSet (Subtype.val '' t) μ) (f n)) → (fun t => NullMeasurableSet (Subtype.val '' t) μ) (⋃ i, f i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Monoid N<VAR>inst✝ : Monoid P<VAR>l l₁ l₂ : List M<VAR>a : M<VAR>h : l₁ ~ l₂<VAR>hc : Pairwise Commute l₁<GOAL>l₁.prod = l₂.prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Monoid N<VAR>inst✝ : Monoid P<VAR>l l₁ l₂ : List M<VAR>a : M<VAR>h : l₁ ~ l₂<VAR>hc : Pairwise Commute l₁<GOAL>∀ x ∈ l₁, ∀ y ∈ l₁, ∀ (z : M), z * x * y = z * y * x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Monoid N<VAR>inst✝ : Monoid P<VAR>l l₁ l₂ : List M<VAR>a : M<VAR>h : l₁ ~ l₂<VAR>hc : Pairwise Commute l₁<GOAL>Symmetric fun x y => ∀ (z : M), z * x * y = z * y * x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Monoid N<VAR>inst✝ : Monoid P<VAR>l l₁ l₂ : List M<VAR>a : M<VAR>h : l₁ ~ l₂<VAR>hc : Pairwise Commute l₁<GOAL>∀ x ∈ l₁, ∀ (z : M), z * x * x = z * x * x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Monoid N<VAR>inst✝ : Monoid P<VAR>l l₁ l₂ : List M<VAR>a : M<VAR>h : l₁ ~ l₂<VAR>hc : Pairwise Commute l₁<GOAL>Pairwise (fun x y => ∀ (z : M), z * x * y = z * y * x) l₁
<VAR>F : Type u_1<VAR>inst✝ : NormedField F<VAR>n : ℕ<VAR>χ : DirichletCharacter F n<VAR>a : (ZMod n)ˣ<GOAL>‖χ ↑a‖ = 1
<VAR>F : Type u_1<VAR>inst✝ : NormedField F<VAR>n : ℕ<VAR>χ : DirichletCharacter F n<VAR>a : (ZMod n)ˣ<GOAL>‖χ ↑a‖ ^ Nat.card (ZMod n)ˣ = 1
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n✝ : ℕ<VAR>inst✝ : Monoid G<VAR>n : ℕ<VAR>A : Rep k G<VAR>f g : (Fin n → G) → CoeSort.coe A<VAR>x : Fin (n + 1) → G<GOAL>(fun f g => (A.ρ (g 0)) (f fun i => g i.succ) + ∑ j : Fin (n + 1), (-1) ^ (↑j + 1) • f (j.contractNth (fun x x_1 => x * x_1) g)) (f + g) x = ((fun f g => (A.ρ (g 0)) (f fun i => g i.succ) + ∑ j : Fin (n + 1), (-1) ^ (↑j + 1) • f (j.contractNth (fun x x_1 => x * x_1) g)) f + (fun f g => (A.ρ (g 0)) (f fun i => g i.succ) + ∑ j : Fin (n + 1), (-1) ^ (↑j + 1) • f (j.contractNth (fun x x_1 => x * x_1) g)) g) x
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n✝ : ℕ<VAR>inst✝ : Monoid G<VAR>n : ℕ<VAR>A : Rep k G<VAR>r : k<VAR>f : (Fin n → G) → CoeSort.coe A<VAR>x : Fin (n + 1) → G<GOAL>{ toFun := fun f g => (A.ρ (g 0)) (f fun i => g i.succ) + ∑ j : Fin (n + 1), (-1) ^ (↑j + 1) • f (j.contractNth (fun x x_1 => x * x_1) g), map_add' := ⋯ }.toFun (r • f) x = ((RingHom.id k) r • { toFun := fun f g => (A.ρ (g 0)) (f fun i => g i.succ) + ∑ j : Fin (n + 1), (-1) ^ (↑j + 1) • f (j.contractNth (fun x x_1 => x * x_1) g), map_add' := ⋯ }.toFun f) x
<VAR>n : Type u_1<VAR>inst✝⁴ : Fintype n<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>b : Basis n R M<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n R<VAR>hA : IsUnit A.det<VAR>x : M<GOAL>((toLin b b) A⁻¹) ({ toFun := ⇑((toLin b b) A), map_add' := ⋯, map_smul' := ⋯ }.toFun x) = x
<VAR>n : Type u_1<VAR>inst✝⁴ : Fintype n<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>b : Basis n R M<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n R<VAR>hA : IsUnit A.det<VAR>x : M<GOAL>{ toFun := ⇑((toLin b b) A), map_add' := ⋯, map_smul' := ⋯ }.toFun (((toLin b b) A⁻¹) x) = x
<VAR>R : Type u<VAR>ι : Type v<VAR>n : ℕ<VAR>M✝ : Fin n.succ → Type w<VAR>M₁ : ι → Type w₁<VAR>M₁' : ι → Type w₁'<VAR>M₂ : Type w₂<VAR>M₃ : Type w₃<VAR>M₄ : Type w₄<VAR>M : Type u_1<VAR>inst✝⁷ : Fintype ι<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ContinuousMul R<VAR>inst✝ : ContinuousSMul R M<VAR>z₁ z₂ : M<GOAL>ContinuousMultilinearMap.mkPiRing R ι z₁ = ContinuousMultilinearMap.mkPiRing R ι z₂ ↔ z₁ = z₂
<VAR>R : Type u<VAR>ι : Type v<VAR>n : ℕ<VAR>M✝ : Fin n.succ → Type w<VAR>M₁ : ι → Type w₁<VAR>M₁' : ι → Type w₁'<VAR>M₂ : Type w₂<VAR>M₃ : Type w₃<VAR>M₄ : Type w₄<VAR>M : Type u_1<VAR>inst✝⁷ : Fintype ι<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ContinuousMul R<VAR>inst✝ : ContinuousSMul R M<VAR>z₁ z₂ : M<GOAL>(ContinuousMultilinearMap.mkPiRing R ι z₁).toMultilinearMap = (ContinuousMultilinearMap.mkPiRing R ι z₂).toMultilinearMap ↔ z₁ = z₂
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝¹ : TopologicalSpace X<VAR>R : Type u_5<VAR>inst✝ : One R<VAR>U : Set X<VAR>f : LocallyConstant X R<VAR>hU : IsClopen U<VAR>s : Set R<GOAL>IsOpen (U.mulIndicator ⇑f ⁻¹' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝¹ : TopologicalSpace X<VAR>R : Type u_5<VAR>inst✝ : One R<VAR>U : Set X<VAR>f : LocallyConstant X R<VAR>hU : IsClopen U<VAR>s : Set R<GOAL>IsOpen (⇑f ⁻¹' s ∩ U ∪ 1 ⁻¹' s ∩ Uᶜ)
<VAR>x✝ y x : ℂ<GOAL>cexp (↑0 * x) = cexp x ^ 0
<VAR>x✝ y x : ℂ<VAR>n : ℕ<GOAL>cexp (↑n.succ * x) = cexp x ^ n.succ
<VAR>R : Type u_1<VAR>inst✝⁸ : CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : AddCommMonoid P<VAR>inst✝⁴ : AddCommMonoid Q<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R N<VAR>inst✝¹ : Module R P<VAR>inst✝ : Module R Q<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>this : g = (range g).subtype ∘ₗ g.rangeRestrict<GOAL>range (lTensor Q ((range g).subtype ∘ₗ g.rangeRestrict)) = range (lTensor Q (range g).subtype)
<VAR>R : Type u_1<VAR>inst✝⁸ : CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : AddCommMonoid P<VAR>inst✝⁴ : AddCommMonoid Q<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R N<VAR>inst✝¹ : Module R P<VAR>inst✝ : Module R Q<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>this : g = (range g).subtype ∘ₗ g.rangeRestrict<GOAL>range (lTensor Q (range g).subtype ∘ₗ lTensor Q g.rangeRestrict) = range (lTensor Q (range g).subtype)
<VAR>R : Type u_1<VAR>inst✝⁸ : CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : AddCommMonoid P<VAR>inst✝⁴ : AddCommMonoid Q<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R N<VAR>inst✝¹ : Module R P<VAR>inst✝ : Module R Q<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>this : g = (range g).subtype ∘ₗ g.rangeRestrict<GOAL>range (lTensor Q g.rangeRestrict) = ⊤
<VAR>R : Type u_1<VAR>inst✝⁸ : CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : AddCommMonoid P<VAR>inst✝⁴ : AddCommMonoid Q<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R N<VAR>inst✝¹ : Module R P<VAR>inst✝ : Module R Q<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>this : g = (range g).subtype ∘ₗ g.rangeRestrict<GOAL>Function.Surjective ⇑(lTensor Q g.rangeRestrict)
<VAR>R : Type u_1<VAR>inst✝⁸ : CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : AddCommMonoid P<VAR>inst✝⁴ : AddCommMonoid Q<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R N<VAR>inst✝¹ : Module R P<VAR>inst✝ : Module R Q<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>this : g = (range g).subtype ∘ₗ g.rangeRestrict<GOAL>Function.Surjective ⇑g.rangeRestrict
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 2<VAR>φ : R₁ ⟶ R₂<VAR>hR₂ : R₂.Exact<VAR>hR₁' : Epi (R₁.map' 1 2 ⋯ ⋯)<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₁ : Epi (app' φ 2 ⋯)<GOAL>Epi (app' φ 1 ⋯)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 2<VAR>φ : R₁ ⟶ R₂<VAR>hR₂ : R₂.Exact<VAR>hR₁' : Epi (R₁.map' 1 2 ⋯ ⋯)<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₁ : Epi (app' φ 2 ⋯)<VAR>ψ : mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 ⟶ mk₃ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 := homMk₃ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) (𝟙 ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).obj' 3 ⋯)) ⋯ ⋯ ⋯<GOAL>Epi (app' φ 1 ⋯)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 2<VAR>φ : R₁ ⟶ R₂<VAR>hR₂ : R₂.Exact<VAR>hR₁' : Epi (R₁.map' 1 2 ⋯ ⋯)<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₁ : Epi (app' φ 2 ⋯)<VAR>ψ : mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 ⟶ mk₃ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 := homMk₃ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) (𝟙 ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).obj' 3 ⋯)) ⋯ ⋯ ⋯<GOAL>(ShortComplex.mk ((mk₂ ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 1 2 ⋯ ⋯) ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 2 3 ⋯ ⋯)).map' 0 1 ⋯ ⋯) ((mk₂ ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 1 2 ⋯ ⋯) ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 2 3 ⋯ ⋯)).map' 1 2 ⋯ ⋯) ⋯).Exact
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 2<VAR>φ : R₁ ⟶ R₂<VAR>hR₂ : R₂.Exact<VAR>hR₁' : Epi (R₁.map' 1 2 ⋯ ⋯)<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₁ : Epi (app' φ 2 ⋯)<VAR>ψ : mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 ⟶ mk₃ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 := homMk₃ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) (𝟙 ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).obj' 3 ⋯)) ⋯ ⋯ ⋯<GOAL>Epi (ShortComplex.mk ((mk₂ ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 1 2 ⋯ ⋯) ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 2 3 ⋯ ⋯)).map' 0 1 ⋯ ⋯) ((mk₂ ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 1 2 ⋯ ⋯) ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 2 3 ⋯ ⋯)).map' 1 2 ⋯ ⋯) ⋯).f
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>proj : Z → B<VAR>e : Pretrivialization F proj<VAR>x✝ x : Z<VAR>ex : x ∈ e.source<GOAL>↑e.symm (proj x, (↑e x).2) = x
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>C : 𝕜<VAR>hC : 0 < C<VAR>hf : Tendsto f l atTop<VAR>hg : Tendsto g l (𝓝 C)<GOAL>Tendsto (fun x => f x * g x) l atTop
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>C : 𝕜<VAR>hC : 0 < C<VAR>hf : Tendsto f l atTop<VAR>hg : Tendsto g l (𝓝 C)<GOAL>(fun x => f x * (C / 2)) ≤ᶠ[l] fun x => f x * g x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_4, u_1} C<VAR>inst✝ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>F : D ⥤ C<VAR>A B : C<VAR>X Y : D<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>u : A ⟶ F.obj X<VAR>v : B ⟶ F.obj Y<VAR>sq : CommSq u i (F.map p) v<VAR>adj : G ⊣ F<GOAL>⋯.HasLift ↔ sq.HasLift