ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>β : Type u_7<VAR>inst✝² : Group β<VAR>inst✝¹ : LE β<VAR>inst✝ : CovariantClass β β (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>f g : α → β<VAR>h : f ≤ᶠ[ae μ] g<VAR>a : α<VAR>ha : f a ≤ g a<GOAL>1 a ≤ (g / f) a
<GOAL>|rexp 1 - 363916618873 / 133877442384| ≤ 1 / 10 ^ 20
<GOAL>|rexp 1 - expNear 0 1 (363916618873 / 133877442384)| ≤ |1| ^ 0 / ↑(Nat.factorial 0) * (1 / 10 ^ 20)
<GOAL>|rexp 1 - expNear 21 1 ((((((((((((((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) * 8 - 1) * 9 - 1) * 10 - 1) * 11 - 1) * 12 - 1) * 13 - 1) * 14 - 1) * 15 - 1) * 16 - 1) * 17 - 1) * 18 - 1) * 19 - 1) * 20 - 1) * 21)| ≤ |1| ^ 21 / ↑(Nat.factorial 21) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15 * 16 * 17 * 18 * 19 * 20 * 21)
<GOAL>|rexp 1 - expNear 21 1 (36295539 / 44271641)| ≤ |1| ^ 21 / ↑(Nat.factorial 21) * (311834363841 / 610351562500)
<GOAL>|1 - 36295539 / 44271641| ≤ 311834363841 / 610351562500 - |1| / 22 * ((22 + 1) / 22)
<VAR>G : Type u_1<VAR>inst✝⁴ : Group G<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : TopologicalGroup G<VAR>inst✝¹ : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>K₀ : PositiveCompacts G<GOAL>(haarMeasure K₀) (closure ↑K₀) = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>M : Type u_4<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : Fintype α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>f : α → M<GOAL>∏ a ∈ {x | p x}.toFinset, f a = ∏ a : Subtype p, f ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>M : Type u_4<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : Fintype α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>f : α → M<GOAL>∀ (x : α), x ∈ {x | p x}.toFinset ↔ p x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>M : Type u_4<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : Fintype α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>f : α → M<GOAL>∀ (x : α), x ∈ {x | p x} ↔ p x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>M : Type u_4<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : Fintype α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>f : α → M<VAR>x✝ : α<GOAL>x✝ ∈ {x | p x} ↔ p x✝
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : SemilatticeSup α<VAR>a✝ b✝ c✝ d a b c : α<GOAL>a ⊔ (b ⊔ c) = a ⊔ b ⊔ (a ⊔ c)
<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✝¹⁷ : SeminormedRing 𝕜₂<VAR>inst✝¹⁶ : SeminormedRing 𝕜₃<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹⁵ : RingHomIsometric σ₁₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>inst✝¹⁴ : RingHomIsometric σ₂₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝¹³ : RingHomIsometric σ₁₃<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : AddCommGroup E₂<VAR>inst✝¹⁰ : AddCommGroup E₃<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : AddCommGroup G<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜₂ E₂<VAR>inst✝⁵ : Module 𝕜₃ E₃<VAR>inst✝⁴ : Module 𝕜 F<VAR>inst✝³ : Module 𝕜 G<VAR>inst✝² : SMul R ℝ<VAR>inst✝¹ : SMul R ℝ≥0<VAR>inst✝ : IsScalarTower R ℝ≥0 ℝ<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>x : E<GOAL>(s.sup p) x = ↑(s.sup fun i => ⟨(p i) x, ⋯⟩)
<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✝¹⁷ : SeminormedRing 𝕜₂<VAR>inst✝¹⁶ : SeminormedRing 𝕜₃<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹⁵ : RingHomIsometric σ₁₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>inst✝¹⁴ : RingHomIsometric σ₂₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝¹³ : RingHomIsometric σ₁₃<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : AddCommGroup E₂<VAR>inst✝¹⁰ : AddCommGroup E₃<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : AddCommGroup G<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜₂ E₂<VAR>inst✝⁵ : Module 𝕜₃ E₃<VAR>inst✝⁴ : Module 𝕜 F<VAR>inst✝³ : Module 𝕜 G<VAR>inst✝² : SMul R ℝ<VAR>inst✝¹ : SMul R ℝ≥0<VAR>inst✝ : IsScalarTower R ℝ≥0 ℝ<VAR>p : ι → Seminorm 𝕜 E<VAR>x : E<GOAL>(∅.sup p) x = ↑(∅.sup fun i => ⟨(p i) x, ⋯⟩)
<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✝¹⁷ : SeminormedRing 𝕜₂<VAR>inst✝¹⁶ : SeminormedRing 𝕜₃<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹⁵ : RingHomIsometric σ₁₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>inst✝¹⁴ : RingHomIsometric σ₂₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝¹³ : RingHomIsometric σ₁₃<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : AddCommGroup E₂<VAR>inst✝¹⁰ : AddCommGroup E₃<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : AddCommGroup G<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜₂ E₂<VAR>inst✝⁵ : Module 𝕜₃ E₃<VAR>inst✝⁴ : Module 𝕜 F<VAR>inst✝³ : Module 𝕜 G<VAR>inst✝² : SMul R ℝ<VAR>inst✝¹ : SMul R ℝ≥0<VAR>inst✝ : IsScalarTower R ℝ≥0 ℝ<VAR>p : ι → Seminorm 𝕜 E<VAR>x : E<VAR>a : ι<VAR>s : Finset ι<VAR>ha : a ∉ s<VAR>ih : (s.sup p) x = ↑(s.sup fun i => ⟨(p i) x, ⋯⟩)<GOAL>((Finset.cons a s ha).sup p) x = ↑((Finset.cons a s ha).sup fun i => ⟨(p i) x, ⋯⟩)
<VAR>α : Type u_1<VAR>inst✝¹ : Ring α<VAR>inst✝ : CharZero α<VAR>num✝¹ num✝ : ℤ<VAR>denom✝¹ denom✝ : ℕ<VAR>inv✝¹ : Invertible ↑denom✝¹<VAR>inv✝ : Invertible ↑denom✝<VAR>h : decide (num✝¹.mul (Int.ofNat denom✝) = num✝.mul (Int.ofNat denom✝¹)) = false<GOAL>¬↑num✝¹ * ⅟↑denom✝¹ = ↑num✝ * ⅟↑denom✝
<VAR>α : Type u_1<VAR>inst✝¹ : Ring α<VAR>inst✝ : CharZero α<VAR>num✝¹ num✝ : ℤ<VAR>denom✝¹ denom✝ : ℕ<VAR>inv✝¹ : Invertible ↑denom✝¹<VAR>inv✝ : Invertible ↑denom✝<VAR>h : decide (num✝¹.mul (Int.ofNat denom✝) = num✝.mul (Int.ofNat denom✝¹)) = false<GOAL>¬↑num✝¹ * ↑denom✝ = ↑num✝ * ↑denom✝¹
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>ha : 0 < a<GOAL>a⁻¹ < b ↔ 1 < a * b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>ha : 0 < a<GOAL>1 / a < b ↔ 1 < a * b
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X Y : TopCat<VAR>homeo : ↑(X ⨯ Y) ≃ₜ ↑(of (↑X × ↑Y)) := homeoOfIso (X.prodIsoProd Y)<GOAL>(X ⨯ Y).str = induced (⇑prod.fst) X.str ⊓ induced (⇑prod.snd) Y.str
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X Y : TopCat<VAR>homeo : ↑(X ⨯ Y) ≃ₜ ↑(of (↑X × ↑Y)) := homeoOfIso (X.prodIsoProd Y)<GOAL>induced (⇑homeo) (of (↑X × ↑Y)).topologicalSpace_coe = induced (⇑prod.fst) X.str ⊓ induced (⇑prod.snd) Y.str
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X Y : TopCat<VAR>homeo : ↑(X ⨯ Y) ≃ₜ ↑(of (↑X × ↑Y)) := homeoOfIso (X.prodIsoProd Y)<GOAL>induced (⇑homeo) (induced Prod.fst X.topologicalSpace_coe ⊓ induced Prod.snd Y.topologicalSpace_coe) = induced (⇑prod.fst) X.str ⊓ induced (⇑prod.snd) Y.str
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X Y : TopCat<VAR>homeo : ↑(X ⨯ Y) ≃ₜ ↑(of (↑X × ↑Y)) := homeoOfIso (X.prodIsoProd Y)<GOAL>induced (Prod.fst ∘ ⇑homeo) X.topologicalSpace_coe ⊓ induced (Prod.snd ∘ ⇑homeo) Y.topologicalSpace_coe = induced (⇑prod.fst) X.str ⊓ induced (⇑prod.snd) Y.str
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x✝ : (i : ↑↑s) → β ↑i<VAR>i✝ : ι<VAR>p : ι → Prop<VAR>inst✝ : DecidablePred p<VAR>i : ι<VAR>x : β i<VAR>h : p i<GOAL>filter p (single i x) = single i x
<VAR>a : UnitAddCircle<GOAL>Tendsto (fun s => (s - 1) * hurwitzZetaEven a s + (s - 1) * hurwitzZetaOdd a s) (𝓝[≠] 1) (𝓝 (1 + (1 - 1) * hurwitzZetaOdd a 1))
<VAR>a : UnitAddCircle<GOAL>Tendsto (fun s => s - 1) (𝓝 1) (𝓝 (1 - 1))
<VAR>a : UnitAddCircle<GOAL>Tendsto (hurwitzZetaOdd a) (𝓝 1) (𝓝 (hurwitzZetaOdd a 1))
<VAR>α✝ β✝ : Type u_1<VAR>a✝¹ : α✝ → PGame<VAR>a✝ : β✝ → PGame<VAR>i : (mk α✝ β✝ a✝¹ a✝).LeftMoves<GOAL>((mk α✝ β✝ a✝¹ a✝).moveLeft i).birthday < max (lsub fun i => (a✝¹ i).birthday) (lsub fun i => (a✝ i).birthday)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>c : ℂ<VAR>R θ : ℝ<GOAL>deriv (circleMap c R) θ = 0 ↔ R = 0
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>R : Type u_5<VAR>M : Type u_6<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>r s✝ : R<VAR>x y : M<VAR>s : Multiset R<VAR>t : Multiset M<GOAL>s.sum • t.sum = (map (fun p => p.1 • p.2) (s ×ˢ t)).sum
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>R : Type u_5<VAR>M : Type u_6<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>r s : R<VAR>x y : M<VAR>t : Multiset M<GOAL>sum 0 • t.sum = (map (fun p => p.1 • p.2) (0 ×ˢ t)).sum
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>R : Type u_5<VAR>M : Type u_6<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>r s✝ : R<VAR>x y : M<VAR>t : Multiset M<VAR>a : R<VAR>s : Multiset R<VAR>ih : s.sum • t.sum = (map (fun p => p.1 • p.2) (s ×ˢ t)).sum<GOAL>(a ::ₘ s).sum • t.sum = (map (fun p => p.1 • p.2) ((a ::ₘ s) ×ˢ t)).sum
<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✝³ : StrictOrderedCommRing R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x z : P<VAR>t : R<VAR>left✝ : 0 ≤ t<VAR>ht1 : t ≤ 1<GOAL>SameRay R (z -ᵥ x) (z -ᵥ (lineMap x z) t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>0 < ∫⁻ (a : α), f a ∂μ ↔ 0 < μ (support f)
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝⁷ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝¹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>inst✝ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P : Cᵒᵖ ⥤ D<GOAL>((𝟙 (J.plusObj (J.plusObj (P ⋙ F))) ≫ J.plusMap (J.plusCompIso F P).inv ≫ 𝟙 (J.plusObj (J.plusObj P ⋙ F))) ≫ (J.plusCompIso F (J.plusObj P)).inv) ≫ 𝟙 (J.plusObj (J.plusObj P) ⋙ F) = J.plusMap (J.plusCompIso F P).inv ≫ (J.plusCompIso F (J.plusObj P)).inv
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝⁷ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝¹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>inst✝ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P : Cᵒᵖ ⥤ D<GOAL>(𝟙 (J.plusObj (J.plusObj (P ⋙ F))) ≫ J.plusMap (J.plusCompIso F P).inv) ≫ (J.plusCompIso F (J.plusObj P)).inv = J.plusMap (J.plusCompIso F P).inv ≫ (J.plusCompIso F (J.plusObj P)).inv
<VAR>u : Level<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>n : ℕ<VAR>inst : CharP α n<VAR>b : α<VAR>a : ℕ<VAR>a' : α<VAR>p : IsNat (↑n - 1) a<VAR>pa : ↑a = a'<GOAL>-b = a' * b
<VAR>u : Level<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>n : ℕ<VAR>inst : CharP α n<VAR>b : α<VAR>a : ℕ<VAR>a' : α<VAR>p : IsNat (↑n - 1) a<VAR>pa : ↑a = a'<GOAL>-1 * b = (↑n - 1) * b
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>φ ψ : R⟦X⟧<VAR>m : ℕ<GOAL>(trunc n (φ + ψ)).coeff m = (trunc n φ + trunc n ψ).coeff m
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>φ ψ : R⟦X⟧<VAR>m : ℕ<GOAL>(if m < n then (coeff R m) (φ + ψ) else 0) = (if m < n then (coeff R m) φ else 0) + if m < n then (coeff R m) ψ else 0
<VAR>α : Type u<VAR>L✝ L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>β : Type v<VAR>inst✝ : Group β<VAR>f : α → β<VAR>x y : FreeGroup α<VAR>s : Subgroup β<VAR>H : Set.range f ⊆ ↑s<VAR>w✝ : FreeGroup α<VAR>L : List (α × Bool)<GOAL>(lift f) (Quot.mk Red.Step L) ∈ s
<VAR>M : Type u_1<VAR>inst✝¹ : Monoid M<VAR>s : Set M<VAR>A : Type u_2<VAR>inst✝ : AddMonoid A<VAR>t : Set A<VAR>x y z : M<VAR>x✝¹ : y ∈ powers x<VAR>x✝ : z ∈ powers x<VAR>n₁ : ℕ<VAR>h₁ : x ^ n₁ = y<VAR>n₂ : ℕ<VAR>h₂ : x ^ n₂ = z<GOAL>x ^ (n₁ + n₂) = y * z
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : LinearOrderedCommGroup α<VAR>n : ℤ<VAR>a b : α<VAR>hn : n ≠ 0<GOAL>Injective fun x => x ^ n
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : LinearOrderedCommGroup α<VAR>n : ℤ<VAR>a b : α<VAR>hn✝ : n ≠ 0<VAR>hn : n < 0<GOAL>Injective fun x => x ^ n
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : LinearOrderedCommGroup α<VAR>n : ℤ<VAR>a b : α<VAR>hn✝ : n ≠ 0<VAR>hn : 0 < n<GOAL>Injective fun x => x ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>f✝ g : α → β<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ContinuousMul M<VAR>f : α → M<VAR>l : List (α → M)<VAR>ihl : (∀ f ∈ l, AEStronglyMeasurable f μ) → AEStronglyMeasurable l.prod μ<VAR>hl : ∀ f_1 ∈ f :: l, AEStronglyMeasurable f_1 μ<GOAL>AEStronglyMeasurable (f :: l).prod μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>f✝ g : α → β<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ContinuousMul M<VAR>f : α → M<VAR>l : List (α → M)<VAR>ihl : (∀ f ∈ l, AEStronglyMeasurable f μ) → AEStronglyMeasurable l.prod μ<VAR>hl : AEStronglyMeasurable f μ ∧ ∀ x ∈ l, AEStronglyMeasurable x μ<GOAL>AEStronglyMeasurable (f :: l).prod μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>f✝ g : α → β<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ContinuousMul M<VAR>f : α → M<VAR>l : List (α → M)<VAR>ihl : (∀ f ∈ l, AEStronglyMeasurable f μ) → AEStronglyMeasurable l.prod μ<VAR>hl : AEStronglyMeasurable f μ ∧ ∀ x ∈ l, AEStronglyMeasurable x μ<GOAL>AEStronglyMeasurable (f * l.prod) μ
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝¹⁰ : Category.{u_6, u_1} C<VAR>inst✝⁹ : Category.{u_7, u_2} D<VAR>inst✝⁸ : Category.{?u.82739, u_3} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : AddMonoid A<VAR>inst✝⁶ : AddCommMonoid B<VAR>inst✝⁵ : HasShift C A<VAR>inst✝⁴ : HasShift D A<VAR>inst✝³ : HasShift E A<VAR>inst✝² : HasShift C B<VAR>inst✝¹ : HasShift D B<VAR>inst✝ : F.CommShift A<VAR>X : C<VAR>a b : A<VAR>h : a + b = 0<GOAL>F.map ((shiftFunctorAdd' C a b 0 h).inv.app X ≫ (shiftFunctorZero C A).hom.app X) = (F.commShiftIso b).hom.app ((shiftFunctor C a).obj X) ≫ (shiftFunctor D b).map ((F.commShiftIso a).hom.app X) ≫ (shiftFunctorAdd' D a b 0 h).inv.app (F.obj X) ≫ (shiftFunctorZero D A).hom.app (F.obj X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝¹⁰ : Category.{u_6, u_1} C<VAR>inst✝⁹ : Category.{u_7, u_2} D<VAR>inst✝⁸ : Category.{?u.82739, u_3} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : AddMonoid A<VAR>inst✝⁶ : AddCommMonoid B<VAR>inst✝⁵ : HasShift C A<VAR>inst✝⁴ : HasShift D A<VAR>inst✝³ : HasShift E A<VAR>inst✝² : HasShift C B<VAR>inst✝¹ : HasShift D B<VAR>inst✝ : F.CommShift A<VAR>X : C<VAR>a b : A<VAR>h : a + b = 0<VAR>eq : (F.commShiftIso 0).hom.app X = (CommShift.isoAdd' h (F.commShiftIso a) (F.commShiftIso b)).hom.app X<GOAL>F.map ((shiftFunctorAdd' C a b 0 h).inv.app X ≫ (shiftFunctorZero C A).hom.app X) = (F.commShiftIso b).hom.app ((shiftFunctor C a).obj X) ≫ (shiftFunctor D b).map ((F.commShiftIso a).hom.app X) ≫ (shiftFunctorAdd' D a b 0 h).inv.app (F.obj X) ≫ (shiftFunctorZero D A).hom.app (F.obj X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝¹⁰ : Category.{u_6, u_1} C<VAR>inst✝⁹ : Category.{u_7, u_2} D<VAR>inst✝⁸ : Category.{?u.82739, u_3} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : AddMonoid A<VAR>inst✝⁶ : AddCommMonoid B<VAR>inst✝⁵ : HasShift C A<VAR>inst✝⁴ : HasShift D A<VAR>inst✝³ : HasShift E A<VAR>inst✝² : HasShift C B<VAR>inst✝¹ : HasShift D B<VAR>inst✝ : F.CommShift A<VAR>X : C<VAR>a b : A<VAR>h : a + b = 0<VAR>eq : F.map ((shiftFunctorZero C A).hom.app X) ≫ (shiftFunctorZero D A).inv.app (F.obj X) = F.map ((shiftFunctorAdd' C a b 0 h).hom.app X) ≫ (F.commShiftIso b).hom.app ((shiftFunctor C a).obj X) ≫ (shiftFunctor D b).map ((F.commShiftIso a).hom.app X) ≫ (shiftFunctorAdd' D a b 0 h).inv.app (F.obj X)<GOAL>F.map ((shiftFunctorAdd' C a b 0 h).inv.app X ≫ (shiftFunctorZero C A).hom.app X) = (F.commShiftIso b).hom.app ((shiftFunctor C a).obj X) ≫ (shiftFunctor D b).map ((F.commShiftIso a).hom.app X) ≫ (shiftFunctorAdd' D a b 0 h).inv.app (F.obj X) ≫ (shiftFunctorZero D A).hom.app (F.obj X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝¹⁰ : Category.{u_6, u_1} C<VAR>inst✝⁹ : Category.{u_7, u_2} D<VAR>inst✝⁸ : Category.{?u.82739, u_3} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : AddMonoid A<VAR>inst✝⁶ : AddCommMonoid B<VAR>inst✝⁵ : HasShift C A<VAR>inst✝⁴ : HasShift D A<VAR>inst✝³ : HasShift E A<VAR>inst✝² : HasShift C B<VAR>inst✝¹ : HasShift D B<VAR>inst✝ : F.CommShift A<VAR>X : C<VAR>a b : A<VAR>h : a + b = 0<VAR>eq : F.map ((shiftFunctorZero C A).hom.app X) ≫ (shiftFunctorZero D A).inv.app (F.obj X) = F.map ((shiftFunctorAdd' C a b 0 h).hom.app X) ≫ (F.commShiftIso b).hom.app ((shiftFunctor C a).obj X) ≫ (shiftFunctor D b).map ((F.commShiftIso a).hom.app X) ≫ (shiftFunctorAdd' D a b 0 h).inv.app (F.obj X)<GOAL>F.map ((shiftFunctorAdd' C a b 0 h).hom.app X) ≫ F.map ((shiftFunctorAdd' C a b 0 h).inv.app X) ≫ F.map ((shiftFunctorZero C A).hom.app X) = F.map ((shiftFunctorZero C A).hom.app X) ≫ (shiftFunctorZero D A).inv.app (F.obj X) ≫ (shiftFunctorZero D A).hom.app (F.obj X)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>δ : ℝ<VAR>δ_nn : 0 ≤ δ<VAR>E : Set α<GOAL>cthickening δ E = ⋂ ε, ⋂ (_ : δ < ε), thickening ε E
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>δ : ℝ<VAR>δ_nn : 0 ≤ δ<VAR>E : Set α<GOAL>∀ (ε : ℝ), δ < ε → (Ioi δ ∩ Ioc δ ε).Nonempty
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>δ : ℝ<VAR>δ_nn : 0 ≤ δ<VAR>E : Set α<GOAL>∀ (ε : ℝ), δ < ε → (Ioc δ ε).Nonempty
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B' I J D X : Set α<VAR>e f : α<VAR>hX : autoParam (X ⊆ M.E) _auto✝<GOAL>¬M.Dep X ↔ M.Indep X
<VAR>V : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>f g : NormedAddGroupHom V₁ V₂<VAR>c : ℝ<VAR>x : V₁<VAR>h : ‖x‖ ≤ c<GOAL>0 ≤ ‖f‖
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁵ : CommSemiring R<VAR>inst✝¹⁴ : AddCommMonoid M<VAR>inst✝¹³ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹² : CommRing R₁<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : AddCommGroup V<VAR>inst✝⁷ : Module K V<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>inst✝⁶ : AddCommMonoid M'✝<VAR>inst✝⁵ : AddCommMonoid M''<VAR>inst✝⁴ : Module R M'✝<VAR>inst✝³ : Module R M''<VAR>B : BilinForm R M<VAR>B₁✝ : BilinForm R₁ M₁<VAR>M' : Type u_9<VAR>inst✝² : AddCommMonoid M'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : FiniteDimensional K V<VAR>B₁ B₂ : BilinForm K V<VAR>b₂ : B₂.Nondegenerate<VAR>v : V<GOAL>B₂ ((↑(B₂.toDual b₂).symm ∘ₗ B₁) v) = B₁ v
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁵ : CommSemiring R<VAR>inst✝¹⁴ : AddCommMonoid M<VAR>inst✝¹³ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹² : CommRing R₁<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : AddCommGroup V<VAR>inst✝⁷ : Module K V<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>inst✝⁶ : AddCommMonoid M'✝<VAR>inst✝⁵ : AddCommMonoid M''<VAR>inst✝⁴ : Module R M'✝<VAR>inst✝³ : Module R M''<VAR>B : BilinForm R M<VAR>B₁✝ : BilinForm R₁ M₁<VAR>M' : Type u_9<VAR>inst✝² : AddCommMonoid M'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : FiniteDimensional K V<VAR>B₁ B₂ : BilinForm K V<VAR>b₂ : B₂.Nondegenerate<VAR>v : V<GOAL>B₂ ((B₂.toDual b₂).symm (B₁ v)) = B₁ v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : CommGroup α<VAR>inst✝² : CommGroup β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>s t u : Finset α<VAR>a : α<VAR>d : ℕ<VAR>ht : t ⊆ s<VAR>hu : u ⊆ s<GOAL>∏ a ∈ s, a ^ ((↑t).indicator 1 - (↑u).indicator 1) a = (∏ a ∈ t, a) / ∏ a ∈ u, a
<VAR>R : Type u<VAR>S : Type v<VAR>a b c✝ d : R<VAR>n m : ℕ<VAR>inst✝² : Nontrivial R<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>c : S<VAR>a✝ : Nontrivial S<GOAL>(X + C c).nextCoeff = c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Computation α<VAR>h : s.Terminates<GOAL>s.think.length = s.length + 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Computation α<VAR>h : s.Terminates<GOAL>s.think.length ≤ s.length + 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Computation α<VAR>h : s.Terminates<GOAL>s.length + 1 ≤ s.think.length
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α → G<VAR>C : ℝ<VAR>h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C<GOAL>∫ (x : α), C ∂μ = C * (μ univ).toReal
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : MeasurableSpace X<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f✝ g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : X → E<VAR>p : ℝ≥0∞<VAR>hf : Memℒp f p μ<VAR>hp : 1 ≤ p<VAR>x : X<GOAL>IntegrableAtFilter f (𝓝 x) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : MeasurableSpace X<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f✝ g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : X → E<VAR>p : ℝ≥0∞<VAR>hf : Memℒp f p μ<VAR>hp : 1 ≤ p<VAR>x : X<VAR>U : Set X<VAR>hU : U ∈ 𝓝 x<VAR>h'U : μ U < ⊤<GOAL>IntegrableAtFilter f (𝓝 x) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : MeasurableSpace X<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f✝ g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : X → E<VAR>p : ℝ≥0∞<VAR>hf : Memℒp f p μ<VAR>hp : 1 ≤ p<VAR>x : X<VAR>U : Set X<VAR>hU : U ∈ 𝓝 x<VAR>h'U : μ U < ⊤<VAR>this : Fact (μ U < ⊤)<GOAL>IntegrableOn f U μ