ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : DivisionMonoid α<VAR>a b c : α<VAR>h : IsUnit b<GOAL>b / (a * b) = 1 / a
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>g : Perm (Fin 5)<VAR>ha : g ∈ alternatingGroup (Fin 5)<VAR>h1 : g ≠ 1<VAR>h2 : ∀ n ∈ g.cycleType, n = 2<GOAL>IsConj (swap 0 4 * swap 1 3) g
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>g : Perm (Fin 5)<VAR>ha : g ∈ alternatingGroup (Fin 5)<VAR>h1 : g ≠ 1<VAR>h2 : ∀ n ∈ g.cycleType, n = 2<VAR>h : g.support.card ≤ card (Fin 5)<GOAL>IsConj (swap 0 4 * swap 1 3) g
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>g : Perm (Fin 5)<VAR>ha : g ∈ alternatingGroup (Fin 5)<VAR>h1 : g ≠ 1<VAR>h2 : g.cycleType = Multiset.replicate (Multiset.card g.cycleType) 2<VAR>h : g.support.card ≤ card (Fin 5)<GOAL>IsConj (swap 0 4 * swap 1 3) g
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>g : Perm (Fin 5)<VAR>ha : g ∈ alternatingGroup (Fin 5)<VAR>h1 : g ≠ 1<VAR>h2 : g.cycleType = Multiset.replicate (Multiset.card g.cycleType) 2<VAR>h : Multiset.card g.cycleType * 2 ≤ card (Fin 5)<GOAL>IsConj (swap 0 4 * swap 1 3) g
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>g : Perm (Fin 5)<VAR>ha : g ∈ alternatingGroup (Fin 5)<VAR>h1 : g ≠ 1<VAR>h2 : g.cycleType = Multiset.replicate (Multiset.card g.cycleType) 2<VAR>h✝ : Multiset.card g.cycleType * 2 ≤ card (Fin 5)<VAR>h : Multiset.card g.cycleType ≤ 3<GOAL>IsConj (swap 0 4 * swap 1 3) g
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>g : Perm (Fin 5)<VAR>ha : (-1) ^ ((Multiset.replicate (Multiset.card g.cycleType) 2).sum + Multiset.card (Multiset.replicate (Multiset.card g.cycleType) 2)) = 1<VAR>h1 : g ≠ 1<VAR>h2 : g.cycleType = Multiset.replicate (Multiset.card g.cycleType) 2<VAR>h✝ : Multiset.card g.cycleType * 2 ≤ card (Fin 5)<VAR>h : Multiset.card g.cycleType ≤ 3<GOAL>IsConj (swap 0 4 * swap 1 3) g
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>g : Perm (Fin 5)<VAR>h1 : g ≠ 1<VAR>h2 : g.cycleType = Multiset.replicate (Multiset.card g.cycleType) 2<VAR>h✝ : Multiset.card g.cycleType * 2 ≤ card (Fin 5)<VAR>h : Multiset.card g.cycleType ≤ 3<VAR>ha : (-1) ^ (Multiset.card g.cycleType * 2 + Multiset.card g.cycleType) = 1<GOAL>IsConj (swap 0 4 * swap 1 3) g
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>g : Perm (Fin 5)<VAR>h1 : g ≠ 1<VAR>h2 : g.cycleType = Multiset.replicate (Multiset.card g.cycleType) 2<VAR>h✝ : Multiset.card g.cycleType * 2 ≤ card (Fin 5)<VAR>h : Multiset.card g.cycleType ≤ 3<VAR>ha : Even (Multiset.card g.cycleType)<GOAL>IsConj (swap 0 4 * swap 1 3) g
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>g : Perm (Fin 5)<VAR>h1 : g ≠ 1<VAR>h2 : g.cycleType = Multiset.replicate (Multiset.card g.cycleType) 2<VAR>h✝ : Multiset.card g.cycleType * 2 ≤ card (Fin 5)<VAR>h : Multiset.card g.cycleType ≤ 3<VAR>ha : (-1) ^ Multiset.card g.cycleType = 1<GOAL>-1 ≠ 1
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>g : Perm (Fin 5)<VAR>h1 : g ≠ 1<VAR>h2 : g.cycleType = Multiset.replicate (Multiset.card g.cycleType) 2<VAR>h✝ : Multiset.card g.cycleType * 2 ≤ card (Fin 5)<VAR>h : Multiset.card g.cycleType ≤ 3<VAR>ha : Even (Multiset.card g.cycleType)<GOAL>(swap 0 4 * swap 1 3).cycleType = Multiset.replicate (Multiset.card g.cycleType) 2
<VAR>f g : CircleDeg1Lift<GOAL>Tendsto (fun n => (⇑1)^[n] 0 / ↑n) atTop (𝓝 0)
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Category.{?u.126215, u_1} C<VAR>inst✝ : Abelian C<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.ShortExact<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>HomologicalComplex.homologyMap S.f i ≫ HomologicalComplex.homologyMap S.g i = 0
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝² : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq δ<VAR>s t : Finset δ<VAR>f✝ g : ((i : δ) → π i) → ℝ≥0∞<VAR>x y : (i : δ) → π i<VAR>i✝ : δ<VAR>f : ((i : δ) → π i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>i : δ<VAR>hi : i ∉ s<GOAL>∫⋯∫⁻_insert i s, f ∂μ = ∫⋯∫⁻_s, fun x => ∫⁻ (xᵢ : π i), f (update x i xᵢ) ∂μ i ∂μ
<VAR>x✝ y✝ x y : ℝ<GOAL>x / √x = √x
<VAR>x✝ y✝ x y : ℝ<VAR>h : x ≤ 0<GOAL>x / √x = √x
<VAR>x✝ y✝ x y : ℝ<VAR>h : 0 < x<GOAL>x / √x = √x
<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>i j : ι<VAR>h : c.Rel i j<GOAL>c.next i = j
<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>i j : ι<VAR>h : c.Rel i j<GOAL>c.Rel i (c.next i)
<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>i j : ι<VAR>h : c.Rel i j<GOAL>c.Rel i (if h : ∃ j, c.Rel i j then h.choose else i)
<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>i j : ι<VAR>h : c.Rel i j<GOAL>c.Rel i ?hc.choose
<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>i j : ι<VAR>h : c.Rel i j<GOAL>∃ j, c.Rel i j
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring S<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>α' : Type u_7<VAR>M' : Type u_8<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>v : α → M<VAR>v' : α' → M'<VAR>f : α ↪ α'<VAR>l : α →₀ R<GOAL>(Finsupp.total α' M' R v') (embDomain f l) = (Finsupp.total α M' R (v' ∘ ⇑f)) l
<VAR>α β : Type u<VAR>A : α → PSet<VAR>B : β → PSet<VAR>αβ : ∀ (a : α), ∃ b, (A a).Equiv (B b)<VAR>a : (PSet.mk α A).Type<VAR>c✝ : ((PSet.mk α A).Func a).Type<VAR>b : β<VAR>γ : Type u<VAR>Γ : γ → PSet<VAR>A_ih✝¹ : ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c✝⟩).Equiv ((⋃₀ PSet.mk β B).Func b)<VAR>ea : A a = PSet.mk γ Γ<VAR>δ : Type u<VAR>Δ : δ → PSet<VAR>A_ih✝ : ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c✝⟩).Equiv ((⋃₀ PSet.mk β B).Func b)<VAR>eb : B b = PSet.mk δ Δ<VAR>γδ : ∀ (a : γ), ∃ b, (Γ a).Equiv (Δ b)<VAR>δγ : ∀ (b : δ), ∃ a, (Γ a).Equiv (Δ b)<VAR>c : (A a).Type := c✝<VAR>d : δ<VAR>hd : (Γ (⋯.mp c)).Equiv (Δ d)<GOAL>∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c✝⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
<VAR>α β : Type u<VAR>A : α → PSet<VAR>B : β → PSet<VAR>αβ : ∀ (a : α), ∃ b, (A a).Equiv (B b)<VAR>a : (PSet.mk α A).Type<VAR>c✝ : ((PSet.mk α A).Func a).Type<VAR>b : β<VAR>γ : Type u<VAR>Γ : γ → PSet<VAR>A_ih✝¹ : ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c✝⟩).Equiv ((⋃₀ PSet.mk β B).Func b)<VAR>ea : A a = PSet.mk γ Γ<VAR>δ : Type u<VAR>Δ : δ → PSet<VAR>A_ih✝ : ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c✝⟩).Equiv ((⋃₀ PSet.mk β B).Func b)<VAR>eb : B b = PSet.mk δ Δ<VAR>γδ : ∀ (a : γ), ∃ b, (Γ a).Equiv (Δ b)<VAR>δγ : ∀ (b : δ), ∃ a, (Γ a).Equiv (Δ b)<VAR>c : (A a).Type := c✝<VAR>d : δ<VAR>hd : (Γ (⋯.mp c)).Equiv (Δ d)<GOAL>((⋃₀ PSet.mk α A).Func ⟨a, c✝⟩).Equiv ((⋃₀ PSet.mk β B).Func ⟨b, ⋯ ▸ d⟩)
<VAR>α β : Type u<VAR>A : α → PSet<VAR>B : β → PSet<VAR>αβ : ∀ (a : α), ∃ b, (A a).Equiv (B b)<VAR>a : (PSet.mk α A).Type<VAR>c✝ : ((PSet.mk α A).Func a).Type<VAR>b : β<VAR>γ : Type u<VAR>Γ : γ → PSet<VAR>A_ih✝¹ : ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c✝⟩).Equiv ((⋃₀ PSet.mk β B).Func b)<VAR>ea : A a = PSet.mk γ Γ<VAR>δ : Type u<VAR>Δ : δ → PSet<VAR>A_ih✝ : ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c✝⟩).Equiv ((⋃₀ PSet.mk β B).Func b)<VAR>eb : B b = PSet.mk δ Δ<VAR>γδ : ∀ (a : γ), ∃ b, (Γ a).Equiv (Δ b)<VAR>δγ : ∀ (b : δ), ∃ a, (Γ a).Equiv (Δ b)<VAR>c : (A a).Type := c✝<VAR>d : δ<VAR>hd : (Γ (⋯.mp c)).Equiv (Δ d)<GOAL>((A a).Func c).Equiv ((B b).Func (⋯ ▸ d))
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.651, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>j : ℕ<VAR>hj : j + 1 = 0<GOAL>False
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.651, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>j : ℕ<VAR>hj : j + 1 = 0<GOAL>j.succ ≤ 0
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : DecidableEq (K →+* ℂ)<VAR>α : K<VAR>i : K →+* ℂ<GOAL>(canonicalEmbedding K) α i = ((basisMatrix K)ᵀ *ᵥ fun i => ↑((((integralBasis K).reindex (equivReindex K).symm).repr α) i)) i
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : DecidableEq (K →+* ℂ)<VAR>α : K<VAR>i : K →+* ℂ<GOAL>(∑ i : K →+* ℂ, ((latticeBasis K).repr ((canonicalEmbedding K) α)) ((equivReindex K) i) • (latticeBasis K) ((equivReindex K) i)) i = ((basisMatrix K)ᵀ *ᵥ fun i => ↑((((integralBasis K).reindex (equivReindex K).symm).repr α) i)) i
<VAR>G : Type u_1<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : LocallyCompactSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : IsFiniteMeasureOnCompacts μ<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>g : G → E<VAR>hg : Continuous g<VAR>h'g : HasCompactSupport g<VAR>k : Set G := tsupport g<VAR>k_comp : IsCompact k<GOAL>Continuous fun x => ∫ (y : G), g (y⁻¹ * x) ∂μ
<VAR>G : Type u_1<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : LocallyCompactSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : IsFiniteMeasureOnCompacts μ<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>g : G → E<VAR>hg : Continuous g<VAR>h'g : HasCompactSupport g<VAR>k : Set G := tsupport g<VAR>k_comp : IsCompact k<VAR>x₀ : G<GOAL>ContinuousAt (fun x => ∫ (y : G), g (y⁻¹ * x) ∂μ) x₀
<VAR>G : Type u_1<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : LocallyCompactSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : IsFiniteMeasureOnCompacts μ<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>g : G → E<VAR>hg : Continuous g<VAR>h'g : HasCompactSupport g<VAR>k : Set G := tsupport g<VAR>k_comp : IsCompact k<VAR>x₀ : G<VAR>t : Set G<VAR>t_comp : IsCompact t<VAR>ht : t ∈ 𝓝 x₀<GOAL>ContinuousAt (fun x => ∫ (y : G), g (y⁻¹ * x) ∂μ) x₀
<VAR>G : Type u_1<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : LocallyCompactSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : IsFiniteMeasureOnCompacts μ<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>g : G → E<VAR>hg : Continuous g<VAR>h'g : HasCompactSupport g<VAR>k : Set G := tsupport g<VAR>k_comp : IsCompact k<VAR>x₀ : G<VAR>t : Set G<VAR>t_comp : IsCompact t<VAR>ht : t ∈ 𝓝 x₀<VAR>k' : Set G := t • k⁻¹<GOAL>ContinuousAt (fun x => ∫ (y : G), g (y⁻¹ * x) ∂μ) x₀
<VAR>G : Type u_1<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : LocallyCompactSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : IsFiniteMeasureOnCompacts μ<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>g : G → E<VAR>hg : Continuous g<VAR>h'g : HasCompactSupport g<VAR>k : Set G := tsupport g<VAR>k_comp : IsCompact k<VAR>x₀ : G<VAR>t : Set G<VAR>t_comp : IsCompact t<VAR>ht : t ∈ 𝓝 x₀<VAR>k' : Set G := t • k⁻¹<VAR>k'_comp : IsCompact k'<GOAL>ContinuousAt (fun x => ∫ (y : G), g (y⁻¹ * x) ∂μ) x₀
<VAR>G : Type u_1<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : LocallyCompactSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : IsFiniteMeasureOnCompacts μ<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>g : G → E<VAR>hg : Continuous g<VAR>h'g : HasCompactSupport g<VAR>k : Set G := tsupport g<VAR>k_comp : IsCompact k<VAR>x₀ : G<VAR>t : Set G<VAR>t_comp : IsCompact t<VAR>ht : t ∈ 𝓝 x₀<VAR>k' : Set G := t • k⁻¹<VAR>k'_comp : IsCompact k'<VAR>A : ContinuousOn (fun x => ∫ (y : G), g (y⁻¹ * x) ∂μ) t<GOAL>ContinuousAt (fun x => ∫ (y : G), g (y⁻¹ * x) ∂μ) x₀
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>(o.areaForm x) y ≤ ‖x‖ * ‖y‖
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁹ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : InnerProductSpace ℝ F'<VAR>n : Type u_8<VAR>inst✝ : Fintype n<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>x : EuclideanSpace ℝ n<GOAL>x ∈ Metric.sphere 0 r ↔ x ∈ {x | ∑ i : n, x i ^ 2 = r ^ 2}
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁹ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : InnerProductSpace ℝ F'<VAR>n : Type u_8<VAR>inst✝ : Fintype n<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>x : EuclideanSpace ℝ n<VAR>this : 0 ≤ ∑ i : n, x i ^ 2<GOAL>x ∈ Metric.sphere 0 r ↔ x ∈ {x | ∑ i : n, x i ^ 2 = r ^ 2}
<VAR>S : Type u'<VAR>T : Type u''<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p p' : SubMulAction R M<VAR>r : R<VAR>x y : M<VAR>hx : x ∈ p<GOAL>-x ∈ p
<VAR>S : Type u'<VAR>T : Type u''<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p p' : SubMulAction R M<VAR>r : R<VAR>x y : M<VAR>hx : x ∈ p<GOAL>-1 • x ∈ p
<VAR>α : Type u<VAR>n i : ℕ<VAR>h : i < (finRange n).length<GOAL>(finRange n)[i] = ⟨i, ⋯⟩
<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 : E<VAR>f✝ : α → E<VAR>hf : AEStronglyMeasurable f✝ μ<VAR>s : Set α<VAR>f : α → F<VAR>hs : MeasurableSet s<VAR>hp_zero : ¬p = 0<VAR>hp_top : ¬p = ⊤<GOAL>eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)
<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 : E<VAR>f✝ : α → E<VAR>hf : AEStronglyMeasurable f✝ μ<VAR>s : Set α<VAR>f : α → F<VAR>hs : MeasurableSet s<VAR>hp_zero : ¬p = 0<VAR>hp_top : ¬p = ⊤<GOAL>(∫⁻ (x : α), ↑‖s.indicator f x‖₊ ^ p.toReal ∂μ) ^ (1 / p.toReal) = (∫⁻ (x : α) in s, ↑‖f x‖₊ ^ p.toReal ∂μ) ^ (1 / p.toReal)
<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 : E<VAR>f✝ : α → E<VAR>hf : AEStronglyMeasurable f✝ μ<VAR>s : Set α<VAR>f : α → F<VAR>hs : MeasurableSet s<VAR>hp_zero : ¬p = 0<VAR>hp_top : ¬p = ⊤<GOAL>∫⁻ (x : α), ↑‖s.indicator f x‖₊ ^ p.toReal ∂μ = ∫⁻ (x : α) in s, ↑‖f x‖₊ ^ p.toReal ∂μ
<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 : E<VAR>f✝ : α → E<VAR>hf : AEStronglyMeasurable f✝ μ<VAR>s : Set α<VAR>f : α → F<VAR>hs : MeasurableSet s<VAR>hp_zero : ¬p = 0<VAR>hp_top : ¬p = ⊤<GOAL>∫⁻ (x : α), ↑‖s.indicator f x‖₊ ^ p.toReal ∂μ = ∫⁻ (a : α), s.indicator (fun x => ↑‖f x‖₊ ^ p.toReal) 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 : E<VAR>f✝ : α → E<VAR>hf : AEStronglyMeasurable f✝ μ<VAR>s : Set α<VAR>f : α → F<VAR>hs : MeasurableSet s<VAR>hp_zero : ¬p = 0<VAR>hp_top : ¬p = ⊤<GOAL>(fun x => ↑‖s.indicator f x‖₊ ^ p.toReal) = fun a => s.indicator (fun x => ↑‖f x‖₊ ^ p.toReal) 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 : E<VAR>f✝ : α → E<VAR>hf : AEStronglyMeasurable f✝ μ<VAR>s : Set α<VAR>f : α → F<VAR>hs : MeasurableSet s<VAR>hp_zero : ¬p = 0<VAR>hp_top : ¬p = ⊤<GOAL>(fun x => s.indicator (fun x => ↑‖f x‖₊) x ^ p.toReal) = fun a => s.indicator (fun x => ↑‖f x‖₊ ^ p.toReal) 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 : E<VAR>f✝ : α → E<VAR>hf : AEStronglyMeasurable f✝ μ<VAR>s : Set α<VAR>f : α → F<VAR>hs : MeasurableSet s<VAR>hp_zero : ¬p = 0<VAR>hp_top : ¬p = ⊤<VAR>h_zero : (fun x => x ^ p.toReal) 0 = 0<GOAL>(fun x => s.indicator (fun x => ↑‖f x‖₊) x ^ p.toReal) = fun a => s.indicator (fun x => ↑‖f x‖₊ ^ p.toReal) a
<VAR>f : ℕ → ℝ<VAR>h_bdd : BddBelow (range f)<VAR>h_ant : Antitone f<GOAL>∃ r, Tendsto f atTop (𝓝 r)
<VAR>f : ℕ → ℝ<VAR>h_bdd : BddBelow (range f)<VAR>h_ant : Antitone f<VAR>B : ℝ<VAR>hB : IsGLB (range f) B<GOAL>∃ r, Tendsto f atTop (𝓝 r)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>f g : ↥(Lp E 2 μ)<VAR>r : 𝕜<GOAL>⟪r • f, g⟫_𝕜 = (starRingEnd 𝕜) r * ⟪f, g⟫_𝕜
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>f g : ↥(Lp E 2 μ)<VAR>r : 𝕜<GOAL>∫ (a : α), ⟪↑↑(r • f) a, ↑↑g a⟫_𝕜 ∂μ = ∫ (a : α), (starRingEnd 𝕜) r • ⟪↑↑f a, ↑↑g a⟫_𝕜 ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>f g : ↥(Lp E 2 μ)<VAR>r : 𝕜<VAR>x : α<VAR>hx : ↑↑(r • f) x = (r • ↑↑f) x<GOAL>(fun a => ⟪↑↑(r • f) a, ↑↑g a⟫_𝕜) x = (fun a => (starRingEnd 𝕜) r • ⟪↑↑f a, ↑↑g a⟫_𝕜) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>f g : ↥(Lp E 2 μ)<VAR>r : 𝕜<VAR>x : α<VAR>hx : ↑↑(r • f) x = (r • ↑↑f) x<GOAL>⟪↑↑(r • f) x, ↑↑g x⟫_𝕜 = (starRingEnd 𝕜) r • ⟪↑↑f x, ↑↑g x⟫_𝕜
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Group α<VAR>g : GroupTopology α<VAR>this✝ : TopologicalSpace α := g.toTopologicalSpace<VAR>this : TopologicalGroup α<GOAL>Continuous fun p => p.1 * p.2
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>x \ y = x ↔ x \ y = x \ ⊥
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>x ⊓ y = x ⊓ ⊥ ↔ Disjoint y x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder β<VAR>f✝ : α → β<VAR>l✝ : List α<VAR>o : Option α<VAR>a✝ m : α<VAR>f : α → β<VAR>a : α<VAR>l hd : List α<VAR>tl : α<VAR>ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a<GOAL>argmax f (a :: (hd ++ [tl])) = Option.casesOn (argmax f (hd ++ [tl])) (some a) fun c => if f a < f c then some c else some a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder β<VAR>f✝ : α → β<VAR>l✝ : List α<VAR>o : Option α<VAR>a✝ m : α<VAR>f : α → β<VAR>a : α<VAR>l hd : List α<VAR>tl : α<VAR>ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a<GOAL>(Option.casesOn (Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a) (some tl) fun c => if f c < f tl then some tl else some c) = Option.casesOn (Option.casesOn (argmax f hd) (some tl) fun c => if f c < f tl then some tl else some c) (some a) fun c => if f a < f c then some c else some a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder β<VAR>f✝ : α → β<VAR>l✝ : List α<VAR>o : Option α<VAR>a✝ m✝ : α<VAR>f : α → β<VAR>a : α<VAR>l hd : List α<VAR>tl : α<VAR>ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a<VAR>m : α<VAR>h : argmax f hd = some m<GOAL>Option.rec (some tl) (fun val => if f val < f tl then some tl else some val) (if f a < f m then some m else some a) = Option.rec (some a) (fun val => if f a < f val then some val else some a) (if f m < f tl then some tl else some m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder β<VAR>f✝ : α → β<VAR>l✝ : List α<VAR>o : Option α<VAR>a✝ m✝ : α<VAR>f : α → β<VAR>a : α<VAR>l hd : List α<VAR>tl : α<VAR>ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a<VAR>m : α<VAR>h : argmax f hd = some m<GOAL>Option.rec (some tl) (fun val => if f val < f tl then some tl else some val) (some (if f a < f m then m else a)) = Option.rec (some a) (fun val => if f a < f val then some val else some a) (some (if f m < f tl then tl else m))
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : Monoid M<VAR>a : M<VAR>s : Set M<VAR>p : (m : M) → m ∈ closure s → Prop<VAR>one : p 1 ⋯<VAR>mul_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ closure s), p y hy → p (x * y) ⋯<VAR>x : M<VAR>h : x ∈ closure s<GOAL>p x h
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : Monoid M<VAR>a : M<VAR>s : Set M<VAR>p : (m : M) → m ∈ closure s → Prop<VAR>one : p 1 ⋯<VAR>mul_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ closure s), p y hy → p (x * y) ⋯<VAR>x : M<VAR>h✝ : x ∈ closure s<VAR>h : x ∈ mrange (FreeMonoid.lift Subtype.val)<GOAL>p x h✝
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q : R[X]<VAR>hp : p.Monic<GOAL>Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q : R[X]<VAR>hp : p.Monic<GOAL>(p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0) ↔ p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q : R[X]<VAR>hp : p.Monic<GOAL>(∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0) ↔ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : Ring R<VAR>a b : R<VAR>n : ℕ<GOAL>(-1) ^ n * a = 0 ↔ a = 0
<VAR>α β : Type u<VAR>β' : Type v<VAR>inst✝ : Infinite α<VAR>lle : lift.{u, v} #β' ≤ lift.{v, u} #α<GOAL>#(β' → α) ≤ #(β' ↪ α)
<VAR>α β : Type u<VAR>β' : Type v<VAR>inst✝ : Infinite α<VAR>lle : lift.{u, v} #β' ≤ lift.{v, u} #α<GOAL>#(β' → α) ≤ #(β' ↪ α × α)
<VAR>α β : Type u<VAR>β' : Type v<VAR>inst✝ : Infinite α<VAR>lle : lift.{u, v} #β' ≤ lift.{v, u} #α<VAR>e : β' ↪ α<GOAL>#(β' → α) ≤ #(β' ↪ α × α)
<VAR>G : Type w<VAR>inst✝ : TopologicalSpace G<VAR>μ : Content G<GOAL>(fun s => ↑(μ.toFun s)) ⊥ = 0
<VAR>G : Type w<VAR>inst✝ : TopologicalSpace G<VAR>μ : Content G<VAR>this : Disjoint ↑⊥ ↑⊥ → IsClosed ↑⊥ → IsClosed ↑⊥ → μ.toFun (⊥ ⊔ ⊥) = μ.toFun ⊥ + μ.toFun ⊥<GOAL>(fun s => ↑(μ.toFun s)) ⊥ = 0
<VAR>z : ℂ<VAR>hz : 1 - z ∈ slitPlane<GOAL>log (1 - z)⁻¹ = z * ∫ (t : ℝ) in 0 ..1, (1 - t • z)⁻¹