ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{?u.230, u_2} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies<VAR>inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies<VAR>inst✝³ : F.EffectivelyEnough<VAR>inst✝² : Precoherent D<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>B₁ B₂ : C<VAR>f : B₂ ⟶ B₁<VAR>α : Type<VAR>x✝¹ : Finite α<VAR>X₁ : α → C<VAR>π₁ : (a : α) → X₁ a ⟶ B₁<VAR>x✝ : EffectiveEpiFamily X₁ π₁<VAR>β : Type<VAR>w✝ : Finite β<VAR>Y₂ : β → D<VAR>τ₂ : (b : β) → Y₂ b ⟶ F.obj B₂<VAR>H : EffectiveEpiFamily Y₂ τ₂<VAR>i : β → α<VAR>ι : (b : β) → Y₂ b ⟶ F.obj (X₁ (i b))<VAR>hh : ∀ (b : β), ι b ≫ F.map (π₁ (i b)) = τ₂ b ≫ F.map f<GOAL>EffectiveEpiFamily (fun a => F.obj ⋯.some.p) fun a => F.map (F.preimage (F.effectiveEpiOver (Y₂ a) ≫ τ₂ a))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{?u.230, u_2} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies<VAR>inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies<VAR>inst✝³ : F.EffectivelyEnough<VAR>inst✝² : Precoherent D<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>B₁ B₂ : C<VAR>f : B₂ ⟶ B₁<VAR>α : Type<VAR>x✝¹ : Finite α<VAR>X₁ : α → C<VAR>π₁ : (a : α) → X₁ a ⟶ B₁<VAR>x✝ : EffectiveEpiFamily X₁ π₁<VAR>β : Type<VAR>w✝ : Finite β<VAR>Y₂ : β → D<VAR>τ₂ : (b : β) → Y₂ b ⟶ F.obj B₂<VAR>H : EffectiveEpiFamily Y₂ τ₂<VAR>i : β → α<VAR>ι : (b : β) → Y₂ b ⟶ F.obj (X₁ (i b))<VAR>hh : ∀ (b : β), ι b ≫ F.map (π₁ (i b)) = τ₂ b ≫ F.map f<GOAL>∀ (b : β), (fun b => F.preimage (F.effectiveEpiOver (Y₂ b) ≫ ι b)) b ≫ π₁ (i b) = (fun b => F.preimage (F.effectiveEpiOver (Y₂ b) ≫ τ₂ b)) b ≫ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>inst✝ : Group G<VAR>s t : Set α<VAR>f✝ g : α → G<VAR>a : α<VAR>h : s ⊆ t<VAR>f : α → G<GOAL>(t \ s).mulIndicator f = t.mulIndicator f / s.mulIndicator f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x : α<VAR>h : l.formPerm x ≠ x<GOAL>x ∈ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>hl : l.HasBasis p s<VAR>hl' : l'.HasBasis p' s'<GOAL>¬Disjoint l l' ↔ ¬∃ i, p i ∧ ∃ i', p' i' ∧ Disjoint (s i) (s' i')
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h✝ h : G.IsTuranMaximal r<GOAL>Nonempty (G ≃g turanGraph (Fintype.card V) r)
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h✝ h : G.IsTuranMaximal r<VAR>zm : { x // x ∈ univ } ≃ Fin univ.card<VAR>zp : ∀ (a b : { x // x ∈ univ }), h.finpartition.part ↑a = h.finpartition.part ↑b ↔ ↑(zm a) % h.finpartition.parts.card = ↑(zm b) % h.finpartition.parts.card<GOAL>Nonempty (G ≃g turanGraph (Fintype.card V) r)
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h✝ h : G.IsTuranMaximal r<VAR>zm : { x // x ∈ univ } ≃ Fin univ.card<VAR>zp : ∀ (a b : { x // x ∈ univ }), h.finpartition.part ↑a = h.finpartition.part ↑b ↔ ↑(zm a) % h.finpartition.parts.card = ↑(zm b) % h.finpartition.parts.card<GOAL>∀ {a b : V}, (turanGraph (Fintype.card V) r).Adj (((Equiv.subtypeUnivEquiv ⋯).symm.trans zm) a) (((Equiv.subtypeUnivEquiv ⋯).symm.trans zm) b) ↔ G.Adj a b
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h✝ h : G.IsTuranMaximal r<VAR>zm : { x // x ∈ univ } ≃ Fin univ.card<VAR>zp : ∀ (a b : { x // x ∈ univ }), h.finpartition.part ↑a = h.finpartition.part ↑b ↔ ↑(zm a) % h.finpartition.parts.card = ↑(zm b) % h.finpartition.parts.card<VAR>a b : V<GOAL>(turanGraph (Fintype.card V) r).Adj (((Equiv.subtypeUnivEquiv ⋯).symm.trans zm) a) (((Equiv.subtypeUnivEquiv ⋯).symm.trans zm) b) ↔ G.Adj a b
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h✝ h : G.IsTuranMaximal r<VAR>zm : { x // x ∈ univ } ≃ Fin univ.card<VAR>zp : ∀ (a b : { x // x ∈ univ }), h.finpartition.part ↑a = h.finpartition.part ↑b ↔ ↑(zm a) % h.finpartition.parts.card = ↑(zm b) % h.finpartition.parts.card<VAR>a b : V<GOAL>↑(zm ⟨a, ⋯⟩) % r ≠ ↑(zm ⟨b, ⋯⟩) % r ↔ G.Adj a b
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h✝ h : G.IsTuranMaximal r<VAR>zm : { x // x ∈ univ } ≃ Fin univ.card<VAR>zp : ∀ (a b : { x // x ∈ univ }), h.finpartition.part ↑a = h.finpartition.part ↑b ↔ ↑(zm a) % h.finpartition.parts.card = ↑(zm b) % h.finpartition.parts.card<VAR>a b : V<VAR>this : h.finpartition.part ↑⟨a, ⋯⟩ = h.finpartition.part ↑⟨b, ⋯⟩ ↔ ↑(zm ⟨a, ⋯⟩) % h.finpartition.parts.card = ↑(zm ⟨b, ⋯⟩) % h.finpartition.parts.card<GOAL>↑(zm ⟨a, ⋯⟩) % r ≠ ↑(zm ⟨b, ⋯⟩) % r ↔ G.Adj a b
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h✝ h : G.IsTuranMaximal r<VAR>zm : { x // x ∈ univ } ≃ Fin univ.card<VAR>zp : ∀ (a b : { x // x ∈ univ }), h.finpartition.part ↑a = h.finpartition.part ↑b ↔ ↑(zm a) % h.finpartition.parts.card = ↑(zm b) % h.finpartition.parts.card<VAR>a b : V<VAR>this : ¬G.Adj ↑⟨a, ⋯⟩ ↑⟨b, ⋯⟩ ↔ ↑(zm ⟨a, ⋯⟩) % h.finpartition.parts.card = ↑(zm ⟨b, ⋯⟩) % h.finpartition.parts.card<GOAL>↑(zm ⟨a, ⋯⟩) % r ≠ ↑(zm ⟨b, ⋯⟩) % r ↔ G.Adj a b
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h✝ h : G.IsTuranMaximal r<VAR>zm : { x // x ∈ univ } ≃ Fin univ.card<VAR>zp : ∀ (a b : { x // x ∈ univ }), h.finpartition.part ↑a = h.finpartition.part ↑b ↔ ↑(zm a) % h.finpartition.parts.card = ↑(zm b) % h.finpartition.parts.card<VAR>a b : V<VAR>this : ¬G.Adj ↑⟨a, ⋯⟩ ↑⟨b, ⋯⟩ ↔ ↑(zm ⟨a, ⋯⟩) % h.finpartition.parts.card = ↑(zm ⟨b, ⋯⟩) % h.finpartition.parts.card<GOAL>↑(zm ⟨a, ⋯⟩) % r = ↑(zm ⟨b, ⋯⟩) % r ↔ ↑(zm ⟨a, ⋯⟩) % min (Fintype.card V) r = ↑(zm ⟨b, ⋯⟩) % min (Fintype.card V) r
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h✝ h : G.IsTuranMaximal r<VAR>zm : { x // x ∈ univ } ≃ Fin univ.card<VAR>zp : ∀ (a b : { x // x ∈ univ }), h.finpartition.part ↑a = h.finpartition.part ↑b ↔ ↑(zm a) % h.finpartition.parts.card = ↑(zm b) % h.finpartition.parts.card<VAR>a b : V<VAR>this : ¬G.Adj ↑⟨a, ⋯⟩ ↑⟨b, ⋯⟩ ↔ ↑(zm ⟨a, ⋯⟩) % h.finpartition.parts.card = ↑(zm ⟨b, ⋯⟩) % h.finpartition.parts.card<VAR>c : r ≤ Fintype.card V<GOAL>↑(zm ⟨a, ⋯⟩) % r = ↑(zm ⟨b, ⋯⟩) % r ↔ ↑(zm ⟨a, ⋯⟩) % min (Fintype.card V) r = ↑(zm ⟨b, ⋯⟩) % min (Fintype.card V) r
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h✝ h : G.IsTuranMaximal r<VAR>zm : { x // x ∈ univ } ≃ Fin univ.card<VAR>zp : ∀ (a b : { x // x ∈ univ }), h.finpartition.part ↑a = h.finpartition.part ↑b ↔ ↑(zm a) % h.finpartition.parts.card = ↑(zm b) % h.finpartition.parts.card<VAR>a b : V<VAR>this : ¬G.Adj ↑⟨a, ⋯⟩ ↑⟨b, ⋯⟩ ↔ ↑(zm ⟨a, ⋯⟩) % h.finpartition.parts.card = ↑(zm ⟨b, ⋯⟩) % h.finpartition.parts.card<VAR>c : Fintype.card V < r<GOAL>↑(zm ⟨a, ⋯⟩) % r = ↑(zm ⟨b, ⋯⟩) % r ↔ ↑(zm ⟨a, ⋯⟩) % min (Fintype.card V) r = ↑(zm ⟨b, ⋯⟩) % min (Fintype.card V) r
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<GOAL>LiouvilleWith p (↑r + x) ↔ LiouvilleWith p x
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ g f : Perm α<VAR>x y a✝ : α<GOAL>a✝ ∈ f.support \ {x, y} → a✝ ∈ (swap x y * f).support
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ g f : Perm α<VAR>x y a✝ : α<GOAL>¬f a✝ = a✝ → ¬(a✝ = x ∨ a✝ = y) → ¬(swap x y) (f a✝) = a✝
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ g f : Perm α<VAR>x y a✝ : α<VAR>ha : f a✝ ≠ a✝<VAR>hx : a✝ ≠ x<VAR>hy : a✝ ≠ y<VAR>H : (swap x y) (f a✝) = a✝<GOAL>False
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ g f : Perm α<VAR>x y a✝ : α<VAR>ha : f a✝ ≠ a✝<VAR>hx : a✝ ≠ x<VAR>hy : a✝ ≠ y<VAR>H : f a✝ = a✝<GOAL>False
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : β → α → β<VAR>b : β<VAR>v✝ : Vector α n<VAR>v : Vector α 1<GOAL>scanl f b v = b ::ᵥ f b v.head ::ᵥ nil
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : β → α → β<VAR>b : β<VAR>v✝ : Vector α n<VAR>v : Vector α 1<GOAL>scanl f b (v.head ::ᵥ v.tail) = b ::ᵥ f b (v.head ::ᵥ v.tail).head ::ᵥ nil
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>f : R[X]<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Nontrivial S<VAR>h : IsAdjoinRootMonic S f<GOAL>h.coeff 1 = Pi.single 0 1
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I B✝ X : Set α<VAR>M : Matroid α<VAR>B : Set α<VAR>h : B ⊆ M.E<GOAL>M✶✶.Base B ↔ M.Base B
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x y z : P<VAR>v : V<GOAL>Sbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z) ↔ Sbtw R x y z
<VAR>α : Type u_1<VAR>inst✝² : CanonicallyOrderedAddCommMonoid α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<GOAL>a - b = 0 ↔ a ≤ b
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n : A<VAR>p q : Submodule R Aᵐᵒᵖ<GOAL>{ toFun := fun p => op (comap (↑(opLinearEquiv R)) p), invFun := fun p => comap (↑(opLinearEquiv R).symm) (unop p), left_inv := ⋯, right_inv := ⋯ }.toFun (p + q) = { toFun := fun p => op (comap (↑(opLinearEquiv R)) p), invFun := fun p => comap (↑(opLinearEquiv R).symm) (unop p), left_inv := ⋯, right_inv := ⋯ }.toFun p + { toFun := fun p => op (comap (↑(opLinearEquiv R)) p), invFun := fun p => comap (↑(opLinearEquiv R).symm) (unop p), left_inv := ⋯, right_inv := ⋯ }.toFun q
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e : I → R<VAR>he : OrthogonalIdempotents e<VAR>inst✝ : Fintype I<GOAL>IsIdempotentElem (∑ i : I, e i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>p : α → Prop<VAR>x y z : α<GOAL>f.SameCycle x y → (g * f * g⁻¹).SameCycle (g x) (g y)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>hf : Integrable f μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<GOAL>f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>hf : Integrable f μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>hf_Lp : Memℒp f 1 μ<GOAL>f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>hf : Integrable f μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>hf_Lp : Memℒp f 1 μ<VAR>f_Lp : ↥(Lp E 1 μ) := Memℒp.toLp f hf_Lp<GOAL>f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>hf : Integrable f μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>hf_Lp : Memℒp f 1 μ<VAR>f_Lp : ↥(Lp E 1 μ) := Memℒp.toLp f hf_Lp<VAR>hf_f_Lp : f =ᶠ[ae μ] ↑↑f_Lp<GOAL>f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>hf : Integrable f μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>hf_Lp : Memℒp f 1 μ<VAR>f_Lp : ↥(Lp E 1 μ) := Memℒp.toLp f hf_Lp<VAR>hf_f_Lp : f =ᶠ[ae μ] ↑↑f_Lp<GOAL>↑↑f_Lp =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>hf : Integrable f μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>hf_Lp : Memℒp f 1 μ<VAR>f_Lp : ↥(Lp E 1 μ) := Memℒp.toLp f hf_Lp<VAR>hf_f_Lp : f =ᶠ[ae μ] ↑↑f_Lp<GOAL>∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑f_Lp) s μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>hf : Integrable f μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>hf_Lp : Memℒp f 1 μ<VAR>f_Lp : ↥(Lp E 1 μ) := Memℒp.toLp f hf_Lp<VAR>hf_f_Lp : f =ᶠ[ae μ] ↑↑f_Lp<GOAL>∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑f_Lp x ∂μ = 0
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : GroupWithZero G₀<VAR>a✝ b c a : G₀<VAR>h : a ≠ 0<GOAL>1 / a ≠ 0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁✝ a₂✝ b c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>s : Set G<VAR>hs : IsSubgroup s<VAR>a₁ a₂ : H<VAR>x✝¹ : a₁ ∈ f '' s<VAR>x✝ : a₂ ∈ f '' s<VAR>b₁ : G<VAR>hb₁ : b₁ ∈ s<VAR>eq₁ : f b₁ = a₁<VAR>b₂ : G<VAR>hb₂ : b₂ ∈ s<VAR>eq₂ : f b₂ = a₂<GOAL>f (b₁ * b₂) = a₁ * a₂
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a✝ a₁ a₂ b✝ c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>s : Set G<VAR>hs : IsSubgroup s<VAR>a : H<VAR>x✝ : a ∈ f '' s<VAR>b : G<VAR>hb : b ∈ s<VAR>Eq : f b = a<GOAL>f b⁻¹ = a⁻¹
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a✝ a₁ a₂ b✝ c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>s : Set G<VAR>hs : IsSubgroup s<VAR>a : H<VAR>x✝ : a ∈ f '' s<VAR>b : G<VAR>hb : b ∈ s<VAR>Eq : f b = a<GOAL>(f b)⁻¹ = a⁻¹
<VAR>a✝ b✝ c✝ p q : ℚ<VAR>a b c d : ℤ<VAR>b_pos : 0 < b<VAR>d_pos : 0 < d<GOAL>↑a / ↑b < ↑c / ↑d ↔ a * d < c * b
<VAR>a✝ b✝ c✝ p q : ℚ<VAR>a b c d : ℤ<VAR>b_pos : 0 < b<VAR>d_pos : 0 < d<GOAL>↑a / ↑b ≤ ↑c / ↑d ∧ ¬↑c / ↑d ≤ ↑a / ↑b ↔ a * d ≤ c * b ∧ ¬c * b ≤ a * d
<VAR>a✝ b✝ c✝ p q : ℚ<VAR>a b c d : ℤ<VAR>b_pos : 0 < b<VAR>d_pos : 0 < d<GOAL>↑a / ↑b ≤ ↑c / ↑d ↔ a * d ≤ c * b
<VAR>a✝ b✝ c✝ p q : ℚ<VAR>a b c d : ℤ<VAR>b_pos : 0 < b<VAR>d_pos : 0 < d<GOAL>¬↑c / ↑d ≤ ↑a / ↑b ↔ ¬c * b ≤ a * d
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S✝<VAR>inst✝ : Ring T<VAR>ι : Sort u_1<VAR>S : ι → Subring R<GOAL>↑(⨅ i, S i) = ⋂ i, ↑(S i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x : F<GOAL>⟪x, x⟫_ℝ = ‖x‖ ^ 2
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<GOAL>legendreSym p 0 = 0
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>f✝ : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : OpensMeasurableSpace E<VAR>inst✝⁴ : CompleteSpace F<VAR>inst✝³ : MeasurableSpace 𝕜<VAR>inst✝² : OpensMeasurableSpace 𝕜<VAR>inst✝¹ : MeasurableSpace F<VAR>inst✝ : BorelSpace F<VAR>f : 𝕜 → F<GOAL>Measurable (deriv f)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>A B X X' Y Y' Z : C<VAR>inst✝¹ : HasFiniteProducts C<VAR>inst✝ : Exponentiable A<VAR>I : C<VAR>t : IsInitial I<VAR>f : A ⟶ I<GOAL>IsIso f
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>A B X X' Y Y' Z : C<VAR>inst✝¹ : HasFiniteProducts C<VAR>inst✝ : Exponentiable A<VAR>I : C<VAR>t : IsInitial I<VAR>f : A ⟶ I<VAR>this : Mono (prod.lift (𝟙 A) f ≫ (zeroMul t).hom)<GOAL>IsIso f
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>A B X X' Y Y' Z : C<VAR>inst✝¹ : HasFiniteProducts C<VAR>inst✝ : Exponentiable A<VAR>I : C<VAR>t : IsInitial I<VAR>f : A ⟶ I<VAR>this : Mono f<GOAL>IsIso f
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>A B X X' Y Y' Z : C<VAR>inst✝¹ : HasFiniteProducts C<VAR>inst✝ : Exponentiable A<VAR>I : C<VAR>t : IsInitial I<VAR>f : A ⟶ I<VAR>this✝ : Mono f<VAR>this : IsSplitEpi f<GOAL>IsIso f
<VAR>R : Type u_1<VAR>inst✝⁶ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra R S<VAR>P : Type u_3<VAR>inst✝³ : CommSemiring P<VAR>A : Type u_4<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>inst✝ : IsLocalization.AtPrime S I<VAR>x : R<VAR>h : optParam (LocalRing S) ⋯<GOAL>(algebraMap R S) x ∉ LocalRing.maximalIdeal S ↔ x ∉ I
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A✝ B✝ C✝ A B C : Finset α<GOAL>(A / C).card * B.card ≤ (A / B).card * (B / C).card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A✝ B✝ C✝ A B C : Finset α<GOAL>(A / C).card * B.card ≤ ((A / B) ×ˢ (B / C)).card * 1
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A✝ B✝ C✝ A B C : Finset α<VAR>x : α<VAR>hx : x ∈ A / C<GOAL>B.card ≤ (bipartiteAbove (fun b ac => ac.1 * ac.2 = b) ((A / B) ×ˢ (B / C)) x).card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A✝ B✝ C✝ A B C : Finset α<VAR>x : α × α<VAR>x✝ : x ∈ (A / B) ×ˢ (B / C)<VAR>a✝ b✝ : α<VAR>hu : a✝ ∈ bipartiteBelow (fun b ac => ac.1 * ac.2 = b) (A / C) x<VAR>hv : b✝ ∈ bipartiteBelow (fun b ac => ac.1 * ac.2 = b) (A / C) x<GOAL>x.1 * x.2 = b✝
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>p : κ → Prop<VAR>s : κ → Set X<VAR>F : ι → X → α<VAR>S : Set X<VAR>x₀ : X<VAR>hX : (𝓝[S] x₀).HasBasis p s<GOAL>EquicontinuousWithinAt F S x₀ ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x ∈ s k, ∀ (i : ι), (F i x₀, F i x) ∈ U
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>p : κ → Prop<VAR>s : κ → Set X<VAR>F : ι → X → α<VAR>S : Set X<VAR>x₀ : X<VAR>hX : (𝓝[S] x₀).HasBasis p s<GOAL>(∀ ib ∈ 𝓤 α, ∃ ia, p ia ∧ ∀ x ∈ s ia, (⇑UniformFun.ofFun ∘ swap F) x ∈ {g | ((⇑UniformFun.ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α ib}) ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x ∈ s k, ∀ (i : ι), (F i x₀, F i x) ∈ U
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α →. β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<VAR>h : f.Dom ∈ l₁<GOAL>PTendsto f l₁ l₂ → PTendsto' f l₁ l₂
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α →. β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<VAR>h : f.Dom ∈ l₁<GOAL>(∀ s ∈ l₂, f.core s ∈ l₁) → ∀ s ∈ l₂, f.preimage s ∈ l₁
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α →. β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<VAR>h : f.Dom ∈ l₁<VAR>h' : ∀ s ∈ l₂, f.core s ∈ l₁<VAR>s : Set β<VAR>sl₂ : s ∈ l₂<GOAL>f.preimage s ∈ l₁
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α →. β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<VAR>h : f.Dom ∈ l₁<VAR>h' : ∀ s ∈ l₂, f.core s ∈ l₁<VAR>s : Set β<VAR>sl₂ : s ∈ l₂<GOAL>f.core s ∩ f.Dom ∈ l₁
<VAR>Γ✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ✝<VAR>inst✝¹ : Zero R<VAR>a b : Γ✝<VAR>r : R<VAR>Γ : Type u_3<VAR>inst✝ : LinearOrder Γ<VAR>x : HahnSeries Γ R<VAR>g : Γ<VAR>h : x.coeff g ≠ 0<GOAL>x.orderTop ≤ ↑g
<VAR>Γ✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ✝<VAR>inst✝¹ : Zero R<VAR>a b : Γ✝<VAR>r : R<VAR>Γ : Type u_3<VAR>inst✝ : LinearOrder Γ<VAR>x : HahnSeries Γ R<VAR>g : Γ<VAR>h : x.coeff g ≠ 0<GOAL>⋯.min ⋯ ≤ g
<VAR>α✝ : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>s : Set α<VAR>ha : a ∈ s<VAR>hb : b ∉ s<GOAL>BijOn (⇑(swap a b)) s (insert b (s \ {a}))
<VAR>α✝ : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>s : Set α<VAR>ha : a ∈ s<VAR>hb : b ∉ s<VAR>x : α<VAR>hx : x ∈ s<GOAL>(swap a b) x ∈ insert b (s \ {a})
<VAR>α✝ : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>s : Set α<VAR>ha : a ∈ s<VAR>hb : b ∉ s<VAR>x : α<VAR>hx : x ∈ insert b (s \ {a})<GOAL>x ∈ ⇑(swap a b) '' s
<VAR>α✝ : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : Set α<VAR>ha : a ∈ s<VAR>x : α<VAR>hb : x ∉ s<VAR>hx : x ∈ insert x (s \ {a})<GOAL>x ∈ ⇑(swap a x) '' s
<VAR>α✝ : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>s : Set α<VAR>ha : a ∈ s<VAR>hb : b ∉ s<VAR>x : α<VAR>hx : x ∈ insert b (s \ {a})<VAR>hxb : x ≠ b<GOAL>x ∈ ⇑(swap a b) '' s
<VAR>α✝ : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>s : Set α<VAR>ha : a ∈ s<VAR>hb : b ∉ s<VAR>x : α<VAR>hxb : x ≠ b<VAR>hx : x ∈ s ∧ ¬x = a<GOAL>x ∈ ⇑(swap a b) '' s
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : Lattice α<VAR>inst✝³ : BoundedOrder α<VAR>inst✝² : IsModularLattice α<VAR>inst✝¹ : ComplementedLattice α<VAR>inst✝ : IsAtomic α<VAR>a b : α<VAR>hab : a < b<GOAL>∃ x, a ⋖ x ∧ x ≤ b
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : Lattice α<VAR>inst✝³ : BoundedOrder α<VAR>inst✝² : IsModularLattice α<VAR>inst✝¹ : ComplementedLattice α<VAR>inst✝ : IsAtomic α<VAR>a b : α<VAR>hab : a < b<VAR>a' : α<VAR>ha'b : a' ≤ b<VAR>ha' : IsCompl ⟨a, ⋯⟩ ⟨a', ha'b⟩<GOAL>∃ x, a ⋖ x ∧ x ≤ b
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : Lattice α<VAR>inst✝³ : BoundedOrder α<VAR>inst✝² : IsModularLattice α<VAR>inst✝¹ : ComplementedLattice α<VAR>inst✝ : IsAtomic α<VAR>a b : α<VAR>hab : a < b<VAR>ha'b : ⊥ ≤ b<VAR>ha' : IsCompl ⟨a, ⋯⟩ ⟨⊥, ha'b⟩<GOAL>∃ x, a ⋖ x ∧ x ≤ b
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : Lattice α<VAR>inst✝³ : BoundedOrder α<VAR>inst✝² : IsModularLattice α<VAR>inst✝¹ : ComplementedLattice α<VAR>inst✝ : IsAtomic α<VAR>a b : α<VAR>hab : a < b<VAR>a' : α<VAR>ha'b : a' ≤ b<VAR>ha' : IsCompl ⟨a, ⋯⟩ ⟨a', ha'b⟩<VAR>d : α<VAR>hd : IsAtom d ∧ d ≤ a'<GOAL>∃ x, a ⋖ x ∧ x ≤ b
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : Lattice α<VAR>inst✝³ : BoundedOrder α<VAR>inst✝² : IsModularLattice α<VAR>inst✝¹ : ComplementedLattice α<VAR>inst✝ : IsAtomic α<VAR>a b : α<VAR>hab : a < b<VAR>a' : α<VAR>ha'b : a' ≤ b<VAR>ha' : IsCompl ⟨a, ⋯⟩ ⟨a', ha'b⟩<VAR>d : α<VAR>hd : IsAtom d ∧ d ≤ a'<GOAL>d ⊓ a ⋖ d
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : Lattice α<VAR>inst✝³ : BoundedOrder α<VAR>inst✝² : IsModularLattice α<VAR>inst✝¹ : ComplementedLattice α<VAR>inst✝ : IsAtomic α<VAR>a b : α<VAR>hab : a < b<VAR>a' : α<VAR>ha'b : a' ≤ b<VAR>ha' : IsCompl ⟨a, ⋯⟩ ⟨a', ha'b⟩<VAR>d : α<VAR>hd : IsAtom d ∧ d ≤ a'<GOAL>d ⊓ a = ⊥