ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>inst✝³ : Fintype ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → MeasurableSpace (A i)<VAR>μ : (i : ι) → Measure (A i)<VAR>inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq ι<VAR>p : ℝ<VAR>hp₀ : 0 ≤ p<VAR>hp : (↑#ι - 1) * p ≤ 1<VAR>f : ((i : ι) → A i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>s : Finset ι<VAR>i : ι<VAR>hi : i ∉ s<GOAL>∫⋯∫⁻_sᶜ, f ∂μ = ∫⋯∫⁻_{i}, ∫⋯∫⁻_(insert i s)ᶜ, f ∂μ ∂μ
<VAR>ι : Type u_1<VAR>inst✝³ : Fintype ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → MeasurableSpace (A i)<VAR>μ : (i : ι) → Measure (A i)<VAR>inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq ι<VAR>p : ℝ<VAR>hp₀ : 0 ≤ p<VAR>hp : (↑#ι - 1) * p ≤ 1<VAR>f : ((i : ι) → A i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>s : Finset ι<VAR>i : ι<VAR>hi : i ∉ s<GOAL>↑s.card * p ≤ 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : InnerProductSpace 𝕜 F<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : CompleteSpace F<VAR>T : E →L[𝕜] E<VAR>hT : T.IsPositive<VAR>x : E<GOAL>0 ≤ re ⟪x, T x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : InnerProductSpace 𝕜 F<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : CompleteSpace F<VAR>T : E →L[𝕜] E<VAR>hT : T.IsPositive<VAR>x : E<GOAL>0 ≤ re ⟪T x, x⟫_𝕜
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C K L : HomologicalComplex V c<VAR>φ : K ⟶ L<VAR>hφ : ∀ (i : ι), Mono (φ.f i)<VAR>Z✝ : HomologicalComplex V c<VAR>g h : Z✝ ⟶ K<VAR>eq : g ≫ φ = h ≫ φ<VAR>i : ι<GOAL>g.f i = h.f i
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C K L : HomologicalComplex V c<VAR>φ : K ⟶ L<VAR>hφ : ∀ (i : ι), Mono (φ.f i)<VAR>Z✝ : HomologicalComplex V c<VAR>g h : Z✝ ⟶ K<VAR>eq : g ≫ φ = h ≫ φ<VAR>i : ι<GOAL>g.f i ≫ φ.f i = h.f i ≫ φ.f i
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : MeasurableSpace H<VAR>inst✝² : Group G<VAR>inst✝¹ : MeasurableMul G<VAR>μ : Measure G<VAR>inst✝ : μ.IsMulRightInvariant<VAR>g : G<VAR>A : Set G<GOAL>(Measure.map (fun h => h * g) μ) A = μ A
<VAR>p q : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Fact (Nat.Prime q)<VAR>hp3 : p % 4 = 3<VAR>hq3 : q % 4 = 3<VAR>hpq : p ≠ q<GOAL>IsSquare ↑q ↔ ¬IsSquare ↑p
<VAR>α : Type v<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>n : ℕ<VAR>m : M<VAR>a : α<GOAL>m ^ n • a = a ↔ period m a ∣ n
<VAR>a : ℝ<GOAL>frontier {z | z.im ≤ a} = {z | z.im = a}
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Nontrivial R<GOAL>Module.rank R M + Module.rank R M₁ ≤ Module.rank R (M × M₁)
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>hf : ¬f ≈ 0<GOAL>0 ≤ f.norm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hs' : μ s ≠ ⊤<VAR>ht' : μ t ≠ ⊤<GOAL>|(μ s).toReal - (μ t).toReal| ≤ (μ (s ∆ t)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hs' : μ s ≠ ⊤<VAR>ht' : μ t ≠ ⊤<VAR>hst : μ (s \ t) ≠ ⊤<GOAL>|(μ s).toReal - (μ t).toReal| ≤ (μ (s ∆ t)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hs' : μ s ≠ ⊤<VAR>ht' : μ t ≠ ⊤<VAR>hst : μ (s \ t) ≠ ⊤<VAR>hts : μ (t \ s) ≠ ⊤<GOAL>|(μ s).toReal - (μ t).toReal| ≤ (μ (s ∆ t)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hs' : μ s ≠ ⊤<VAR>ht' : μ t ≠ ⊤<VAR>hst : μ (s \ t) ≠ ⊤<VAR>hts : μ (t \ s) ≠ ⊤<GOAL>(μ s).toReal - (μ t).toReal = (μ (s \ t)).toReal - (μ (t \ s)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hs' : μ s ≠ ⊤<VAR>ht' : μ t ≠ ⊤<VAR>hst : μ (s \ t) ≠ ⊤<VAR>hts : μ (t \ s) ≠ ⊤<GOAL>(μ s).toReal - (μ t).toReal = (μ (s ∪ t)).toReal - (μ t).toReal - ((μ (s ∪ t)).toReal - (μ s).toReal)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ inst✝ : CommSemiring R<VAR>r : R<GOAL>(C r).IsHomogeneous 0
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ inst✝ : CommSemiring R<VAR>r : R<GOAL>Finsupp.degree 0 = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Semiring S<VAR>f✝ f : R →+* S<VAR>hf : f p.leadingCoeff ≠ 0<GOAL>p.degree ≤ (map f p).degree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Semiring S<VAR>f✝ f : R →+* S<VAR>hf : f p.leadingCoeff ≠ 0<VAR>hp0 : p ≠ 0<GOAL>p.degree ≤ (map f p).degree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Semiring S<VAR>f✝ f : R →+* S<VAR>hf : f p.leadingCoeff ≠ 0<VAR>hp0 : p ≠ 0<GOAL>↑p.natDegree ≤ (map f p).degree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Semiring S<VAR>f✝ f : R →+* S<VAR>hf : f p.leadingCoeff ≠ 0<VAR>hp0 : p ≠ 0<GOAL>(map f p).coeff p.natDegree ≠ 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Semiring S<VAR>f✝ f : R →+* S<VAR>hf : f p.leadingCoeff ≠ 0<VAR>hp0 : p ≠ 0<GOAL>f (p.coeff p.natDegree) ≠ 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : ChosenFiniteProducts C<VAR>X Y Z : C<GOAL>(α_ X Y Z).inv ≫ fst (X ⊗ Y) Z ≫ snd X Y = snd X (Y ⊗ Z) ≫ fst Y Z
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : ChosenFiniteProducts C<VAR>X Y Z : C<GOAL>Limits.BinaryFan.snd (product X (product Y Z).cone.pt).cone ≫ Limits.BinaryFan.fst (product Y Z).cone = snd X (Y ⊗ Z) ≫ fst Y Z
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>p q : α → Prop<VAR>f : Filter α<VAR>hp : ∃ᶠ (x : α) in f, p x<VAR>hq : ∀ᶠ (x : α) in f, q x<GOAL>∃ᶠ (x : α) in f, p x ∧ q x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>p q : α → Prop<VAR>f : Filter α<VAR>hp : ∃ᶠ (x : α) in f, p x<VAR>hq : ∀ᶠ (x : α) in f, q x<VAR>h : ∀ᶠ (x : α) in f, ¬(fun x => p x ∧ q x) x<GOAL>∀ (x : α), ¬(fun x => p x ∧ q x) x → q x → ¬(fun x => p x) x
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : TopCat<VAR>ι : Type u_1<VAR>B : ι → Opens ↑X<VAR>F : Presheaf C X<VAR>F' : Sheaf C X<VAR>h : Opens.IsBasis (Set.range B)<VAR>α β : F ⟶ F'.val<VAR>he : ∀ (i : ι), α.app (op (B i)) = β.app (op (B i))<GOAL>α = β
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : TopCat<VAR>ι : Type u_1<VAR>B : ι → Opens ↑X<VAR>F : Presheaf C X<VAR>F' : Sheaf C X<VAR>h : Opens.IsBasis (Set.range B)<VAR>α β : F ⟶ F'.val<VAR>he : ∀ (i : ι), α.app (op (B i)) = β.app (op (B i))<GOAL>(restrictHomEquivHom F F' h).symm α = (restrictHomEquivHom F F' h).symm β
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : Fintype (Sym2 V)<GOAL>2 * G.edgeFinset.card = (filter (fun x => match x with | (x, y) => G.Adj x y) univ).card
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : Fintype (Sym2 V)<GOAL>univ.card = (filter (fun x => match x with | (x, y) => G.Adj x y) univ).card
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : Ring R'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R' M'<VAR>inst✝ : Module R' M₁<VAR>i : R' → R<VAR>j : M →+ M₁<VAR>hi : ∀ (r : R'), i r = 0 → r = 0<VAR>hj : Injective ⇑j<VAR>hc : ∀ (r : R') (m : M), j (i r • m) = r • j m<GOAL>Module.rank R M ≤ Module.rank R' M₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>mα : MeasurableSpace α<VAR>inst✝ : Countable β<VAR>f : β → α → ℝ≥0∞<VAR>μ : Measure α<VAR>hμ : μ ≠ 0<VAR>hf : ∀ (b : β), Measurable (f b)<VAR>hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ⊤<VAR>h_directed : Directed (fun x x_1 => x ≥ x_1) f<GOAL>∫⁻ (a : α), ⨅ b, f b a ∂μ = ⨅ b, ∫⁻ (a : α), f b a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>mα : MeasurableSpace α<VAR>inst✝ : Countable β<VAR>f : β → α → ℝ≥0∞<VAR>μ : Measure α<VAR>hμ : μ ≠ 0<VAR>hf : ∀ (b : β), Measurable (f b)<VAR>hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ⊤<VAR>h_directed : Directed (fun x x_1 => x ≥ x_1) f<VAR>val✝ : Encodable β<GOAL>∫⁻ (a : α), ⨅ b, f b a ∂μ = ⨅ b, ∫⁻ (a : α), f b a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>mα : MeasurableSpace α<VAR>inst✝ : Countable β<VAR>f : β → α → ℝ≥0∞<VAR>μ : Measure α<VAR>hμ : μ ≠ 0<VAR>hf : ∀ (b : β), Measurable (f b)<VAR>hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ⊤<VAR>h_directed : Directed (fun x x_1 => x ≥ x_1) f<VAR>val✝ : Encodable β<VAR>h✝ : IsEmpty β<GOAL>∫⁻ (a : α), ⨅ b, f b a ∂μ = ⨅ b, ∫⁻ (a : α), f b a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>mα : MeasurableSpace α<VAR>inst✝ : Countable β<VAR>f : β → α → ℝ≥0∞<VAR>μ : Measure α<VAR>hμ : μ ≠ 0<VAR>hf : ∀ (b : β), Measurable (f b)<VAR>hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ⊤<VAR>h_directed : Directed (fun x x_1 => x ≥ x_1) f<VAR>val✝ : Encodable β<VAR>h✝ : Nonempty β<GOAL>∫⁻ (a : α), ⨅ b, f b a ∂μ = ⨅ b, ∫⁻ (a : α), f b a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>mα : MeasurableSpace α<VAR>inst✝ : Countable β<VAR>f : β → α → ℝ≥0∞<VAR>μ : Measure α<VAR>hμ : μ ≠ 0<VAR>hf : ∀ (b : β), Measurable (f b)<VAR>hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ⊤<VAR>h_directed : Directed (fun x x_1 => x ≥ x_1) f<VAR>val✝ : Encodable β<VAR>h✝ : Nonempty β<VAR>inhabited_h : Inhabited β<GOAL>∫⁻ (a : α), ⨅ b, f b a ∂μ = ⨅ b, ∫⁻ (a : α), f b a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>mα : MeasurableSpace α<VAR>inst✝ : Countable β<VAR>f : β → α → ℝ≥0∞<VAR>μ : Measure α<VAR>hμ : μ ≠ 0<VAR>hf : ∀ (b : β), Measurable (f b)<VAR>hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ⊤<VAR>h_directed : Directed (fun x x_1 => x ≥ x_1) f<VAR>val✝ : Encodable β<VAR>h✝ : Nonempty β<VAR>inhabited_h : Inhabited β<VAR>this : ∀ (a : α), ⨅ b, f b a = ⨅ n, f (Directed.sequence f h_directed n) a<GOAL>∫⁻ (a : α), ⨅ b, f b a ∂μ = ⨅ b, ∫⁻ (a : α), f b a ∂μ
<VAR>S : Type u_1<VAR>R R' : Type u<VAR>M : Type v<VAR>inst✝²⁶ : CommSemiring S<VAR>inst✝²⁵ : Semiring R<VAR>inst✝²⁴ : CommSemiring R'<VAR>inst✝²³ : AddCommMonoid M<VAR>inst✝²² : Algebra S R<VAR>inst✝²¹ : Algebra S R'<VAR>inst✝²⁰ : Module S M<VAR>inst✝¹⁹ : Module R M<VAR>inst✝¹⁸ : Module Rᵐᵒᵖ M<VAR>inst✝¹⁷ : SMulCommClass R Rᵐᵒᵖ M<VAR>inst✝¹⁶ : IsScalarTower S R M<VAR>inst✝¹⁵ : IsScalarTower S Rᵐᵒᵖ M<VAR>inst✝¹⁴ : Module R' M<VAR>inst✝¹³ : Module R'ᵐᵒᵖ M<VAR>inst✝¹² : IsCentralScalar R' M<VAR>inst✝¹¹ : IsScalarTower S R' M<VAR>A : Type u_2<VAR>inst✝¹⁰ : Semiring A<VAR>inst✝⁹ : Algebra S A<VAR>inst✝⁸ : Algebra R' A<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁷ : AddCommMonoid N<VAR>inst✝⁶ : Module R' N<VAR>inst✝⁵ : Module R'ᵐᵒᵖ N<VAR>inst✝⁴ : IsCentralScalar R' N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R' P<VAR>inst✝¹ : Module R'ᵐᵒᵖ P<VAR>inst✝ : IsCentralScalar R' P<VAR>f : M →ₗ[R'] N<VAR>x : M<GOAL>(map f) (inr x) = inr (f x)
<VAR>a✝ b c d m n a : ℤ<GOAL>-a.pred = (-a).succ
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NeZero 2<VAR>a b c x✝ : K<VAR>ha : a ≠ 0<VAR>h : discrim a b c = 0<VAR>x : K<GOAL>a * x * x + b * x + c = 0 ↔ x = -b / (2 * a)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NeZero 2<VAR>a b c x✝ : K<VAR>ha : a ≠ 0<VAR>h : discrim a b c = 0<VAR>x : K<VAR>this : discrim a b c = 0 * 0<GOAL>a * x * x + b * x + c = 0 ↔ x = -b / (2 * a)
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K L M : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>ψ : L ⟶ M<VAR>i j k : ι<VAR>inst✝² : K.HasHomology i<VAR>inst✝¹ : L.HasHomology i<VAR>inst✝ : M.HasHomology i<GOAL>ShortComplex.opcyclesMap ((shortComplexFunctor C c i).map (φ ≫ ψ)) = ShortComplex.opcyclesMap ((shortComplexFunctor C c i).map φ) ≫ ShortComplex.opcyclesMap ((shortComplexFunctor C c i).map ψ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t s : Set α<VAR>inst✝ : Fintype ↑s<GOAL>s.ncard = s.toFinset.card
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : SeminormedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p✝ p : Seminorm 𝕜 E<VAR>r₁ r₂ : ℝ<GOAL>Metric.ball 0 r₁ • p.ball 0 r₂ ⊆ p.ball 0 (r₁ * r₂)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : SeminormedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p✝ p : Seminorm 𝕜 E<VAR>r₁ : ℝ<GOAL>Metric.ball 0 r₁ • p.ball 0 0 ⊆ p.ball 0 (r₁ * 0)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : SeminormedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p✝ p : Seminorm 𝕜 E<VAR>r₁ r₂ : ℝ<VAR>hr₂ : r₂ ≠ 0<GOAL>Metric.ball 0 r₁ • p.ball 0 r₂ ⊆ p.ball 0 (r₁ * r₂)
<GOAL>Tendsto (fun s => s * s.Gammaℝ) (𝓝[≠] 0) (𝓝 2)
<VAR>h : Tendsto (fun z => z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)<GOAL>Tendsto (fun s => s * s.Gammaℝ) (𝓝[≠] 0) (𝓝 2)
<VAR>h : Tendsto (fun z => z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)<VAR>h' : Tendsto (fun s => 2 * ↑π ^ (-s / 2)) (𝓝[≠] 0) (𝓝 2)<GOAL>Tendsto (fun s => s * s.Gammaℝ) (𝓝[≠] 0) (𝓝 2)
<VAR>h : Tendsto (fun z => z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)<VAR>h' : Tendsto (fun s => 2 * ↑π ^ (-s / 2)) (𝓝[≠] 0) (𝓝 2)<VAR>z : ℂ<GOAL>z * z.Gammaℝ = 2 * ↑π ^ (-z / 2) * (z / 2 * Gamma (z / 2))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>κ : ι → Sort u_1<VAR>a✝ a₁ a₂ : α<VAR>b✝ b₁ b₂ : β<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>s : Set α<VAR>a : α<VAR>h : IsLUB s a<VAR>b : β<VAR>hb : b ∈ upperBounds (l '' s)<GOAL>u b ∈ upperBounds s
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a : α<VAR>n : ℕ<VAR>l : List α<GOAL>(insertNth n a l).eraseIdx n = l
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a : α<VAR>n : ℕ<VAR>l : List α<GOAL>modifyNthTail (tail ∘ cons a) n l = l
<VAR>s : Finset ℕ<VAR>m✝ n✝ p n m : ℕ<VAR>hn : Squarefree n<VAR>hm : Squarefree m<GOAL>n = m ↔ ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
<VAR>s : Finset ℕ<VAR>m✝ n✝ p✝ n m : ℕ<VAR>hn : Squarefree n<VAR>hm : Squarefree m<VAR>h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)<VAR>p : ℕ<GOAL>n.factorization p = m.factorization p
<VAR>s : Finset ℕ<VAR>m✝ n✝ p✝ n m : ℕ<VAR>hn : Squarefree n<VAR>hm : Squarefree m<VAR>h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)<VAR>p : ℕ<VAR>hp : ¬Prime p<GOAL>n.factorization p = m.factorization p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>a a' : α<VAR>b : M<VAR>x : α<GOAL>(single a b) x ∈ {0, b}
<VAR>n m b : ℕ<GOAL>¬m = 0 → (b + 1 + 1) ^ ((b + 1 + 1).digits m).length ≤ (b + 1 + 1) * m
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>a : A<VAR>i : ℕ<GOAL>f ^ i ∈ 𝒜 (m * i)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>a : A<VAR>i : ℕ<GOAL>f ^ i ∈ 𝒜 (i * m)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>a : A<VAR>i : ℕ<GOAL>Subtype.val ⁻¹' ↑(pbo ↑(((decompose 𝒜) a) i)) = ⇑(toSpec 𝒜 f) ⁻¹' (sbo HomogeneousLocalization.mk { deg := m * i, num := ⟨↑(((decompose 𝒜) a) i) ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }).carrier
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R✝ : ℝ<VAR>z✝ w : ℂ<VAR>R r : ℝ<VAR>hr : r < R<VAR>z : ℂ<VAR>this : ContinuousOn (circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ)<GOAL>ContinuousOn (⇑abs ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ζ : Type u_6<VAR>r✝ : α → β → Prop<VAR>p : β → γ → Prop<VAR>q : γ → δ → Prop<VAR>r : Prop → α → Prop<VAR>this : (fun x x_1 => x ↔ x_1) = fun x x_1 => x = x_1<GOAL>(fun x x_1 => x ↔ x_1) ∘r r = r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>o o' : Ordering<GOAL>o.swap = o' ↔ o = o'.swap
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹⁰ : NormedAddCommGroup D<VAR>inst✝⁹ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝² : NormedAddCommGroup X<VAR>inst✝¹ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>inst✝ : CompleteSpace E<VAR>f : PartialHomeomorph E F<VAR>f₀' : E ≃L[𝕜] F<VAR>a : F<VAR>ha : a ∈ f.target<VAR>hf₀' : HasFDerivAt (↑f) (↑f₀') (↑f.symm a)<VAR>hf : ContDiffAt 𝕜 n (↑f) (↑f.symm a)<GOAL>ContDiffAt 𝕜 n (↑f.symm) a
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹⁰ : NormedAddCommGroup D<VAR>inst✝⁹ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝² : NormedAddCommGroup X<VAR>inst✝¹ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>inst✝ : CompleteSpace E<VAR>f : PartialHomeomorph E F<VAR>f₀' : E ≃L[𝕜] F<VAR>a : F<VAR>ha : a ∈ f.target<VAR>hf₀' : HasFDerivAt (↑f) (↑f₀') (↑f.symm a)<VAR>hf : ContDiffAt 𝕜 0 (↑f) (↑f.symm a)<GOAL>ContDiffAt 𝕜 0 (↑f.symm) a
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹⁰ : NormedAddCommGroup D<VAR>inst✝⁹ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝² : NormedAddCommGroup X<VAR>inst✝¹ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>inst✝ : CompleteSpace E<VAR>f : PartialHomeomorph E F<VAR>f₀' : E ≃L[𝕜] F<VAR>a : F<VAR>ha : a ∈ f.target<VAR>hf₀' : HasFDerivAt (↑f) (↑f₀') (↑f.symm a)<VAR>n : ℕ<VAR>IH : ContDiffAt 𝕜 (↑n) (↑f) (↑f.symm a) → ContDiffAt 𝕜 (↑n) (↑f.symm) a<VAR>hf : ContDiffAt 𝕜 (↑n.succ) (↑f) (↑f.symm a)<GOAL>ContDiffAt 𝕜 (↑n.succ) (↑f.symm) a
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹⁰ : NormedAddCommGroup D<VAR>inst✝⁹ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝² : NormedAddCommGroup X<VAR>inst✝¹ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>inst✝ : CompleteSpace E<VAR>f : PartialHomeomorph E F<VAR>f₀' : E ≃L[𝕜] F<VAR>a : F<VAR>ha : a ∈ f.target<VAR>hf₀' : HasFDerivAt (↑f) (↑f₀') (↑f.symm a)<VAR>Itop : ∀ (n : ℕ), ContDiffAt 𝕜 (↑n) (↑f) (↑f.symm a) → ContDiffAt 𝕜 (↑n) (↑f.symm) a<VAR>hf : ContDiffAt 𝕜 ⊤ (↑f) (↑f.symm a)<GOAL>ContDiffAt 𝕜 ⊤ (↑f.symm) a
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : CompleteLattice β<VAR>f g : α →o β<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous (f ⊔ g)
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : CompleteLattice β<VAR>f g : α →o β<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous (sSup {f, g})
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : CompleteLattice β<VAR>f g : α →o β<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>∀ f_1 ∈ {f, g}, Continuous f_1
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>f : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : AEStronglyMeasurable f μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>h : ¬ε = ⊤<GOAL>μ {x | ε ≤ ↑‖f x‖₊} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>f : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : AEStronglyMeasurable f μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>h : ¬ε = ⊤<VAR>hεpow : ε ^ p.toReal ≠ 0<GOAL>μ {x | ε ≤ ↑‖f x‖₊} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>f : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : AEStronglyMeasurable f μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>h : ¬ε = ⊤<VAR>hεpow : ε ^ p.toReal ≠ 0<VAR>hεpow' : ε ^ p.toReal ≠ ⊤<GOAL>μ {x | ε ≤ ↑‖f x‖₊} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal