ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>S' : Type w<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : CommSemiring S'<VAR>inst✝⁶ : Algebra S' R<VAR>inst✝⁵ : Algebra S S'<VAR>inst✝⁴ : IsScalarTower S S' R<VAR>I : Ideal R<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : CommRing A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f : A →ₐ[R] B<GOAL>(RingHom.ker f.toRingHom).cotangentIdeal ≤ RingHom.ker f.kerSquareLift.toRingHom
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝ : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>X : Ω → E<VAR>h : ¬pdf X ℙ μ =ᶠ[ae μ] 0<GOAL>AEMeasurable X ℙ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝ : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>X : Ω → E<VAR>h : ¬AEMeasurable X ℙ<GOAL>pdf X ℙ μ =ᶠ[ae μ] 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<GOAL>U R (-1) = 0
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>inst✝ : IsIrrefl α r<VAR>p : α → Prop<VAR>h : ∀ {a' a : α}, r a' a → p a → p a'<VAR>s' s : Multiset α<GOAL>CutExpand r s' s → (∀ a ∈ s, p a) → ∀ a ∈ s', p a
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝ : Preorder β<VAR>f✝ g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>ι : Type u_3<VAR>f : ι → α → ℝ≥0∞<VAR>h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x<GOAL>LowerSemicontinuousWithinAt (fun x' => ∑' (i : ι), f i x') s x
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝ : Preorder β<VAR>f✝ g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>ι : Type u_3<VAR>f : ι → α → ℝ≥0∞<VAR>h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x<GOAL>LowerSemicontinuousWithinAt (fun x' => ⨆ s, ∑ i ∈ s, f i x') s x
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝ : Preorder β<VAR>f✝ g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>ι : Type u_3<VAR>f : ι → α → ℝ≥0∞<VAR>h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x<VAR>b : Finset ι<GOAL>LowerSemicontinuousWithinAt (fun x' => ∑ i ∈ b, f i x') s x
<VAR>α : Type u<VAR>o n m : ℕ<VAR>m' : Type uₘ<VAR>n' : Type uₙ<VAR>o' : Type uₒ<VAR>a b : ℕ<VAR>inst✝ : Add α<VAR>a₀ a₁ b₀ b₁ : α<GOAL>![a₀, a₁] + ![b₀, b₁] = ![a₀ + b₀, a₁ + b₁]
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r : R<VAR>ε : ℚ<VAR>hε : ε > 0<GOAL>∃ i, ∀ j ≥ i, padicNorm p ((fun n => ↑(nthHom f r n)) j - (fun n => ↑(nthHom f r n)) i) < ε
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r : R<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>k : ℕ<VAR>hk : ↑p ^ (-↑k) < ε<GOAL>∃ i, ∀ j ≥ i, padicNorm p ((fun n => ↑(nthHom f r n)) j - (fun n => ↑(nthHom f r n)) i) < ε
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r : R<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>k : ℕ<VAR>hk : ↑p ^ (-↑k) < ε<GOAL>∀ j ≥ k, padicNorm p ((fun n => ↑(nthHom f r n)) j - (fun n => ↑(nthHom f r n)) k) < ε
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r : R<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>k : ℕ<VAR>hk : ↑p ^ (-↑k) < ε<VAR>j : ℕ<VAR>hj : j ≥ k<GOAL>padicNorm p ((fun n => ↑(nthHom f r n)) j - (fun n => ↑(nthHom f r n)) k) < ε
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r : R<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>k : ℕ<VAR>hk : ↑p ^ (-↑k) < ε<VAR>j : ℕ<VAR>hj : j ≥ k<GOAL>padicNorm p ((fun n => ↑(nthHom f r n)) j - (fun n => ↑(nthHom f r n)) k) ≤ ↑p ^ (-↑k)
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r : R<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>k : ℕ<VAR>hk : ↑p ^ (-↑k) < ε<VAR>j : ℕ<VAR>hj : j ≥ k<GOAL>padicNorm p ↑(nthHom f r j - nthHom f r k) ≤ ↑p ^ (-↑k)
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r : R<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>k : ℕ<VAR>hk : ↑p ^ (-↑k) < ε<VAR>j : ℕ<VAR>hj : j ≥ k<GOAL>↑(p ^ k) ∣ nthHom f r j - nthHom f r k
<VAR>X : Scheme<VAR>inst✝ : IsIntegral X<VAR>U V : X.Opens<VAR>i : U ⟶ V<VAR>H : Nonempty ↑↑(↑U).toPresheafedSpace<GOAL>Function.Injective ⇑(X.presheaf.map i.op)
<VAR>X : Scheme<VAR>inst✝ : IsIntegral X<VAR>U V : X.Opens<VAR>i : U ⟶ V<VAR>H : Nonempty ↑↑(↑U).toPresheafedSpace<GOAL>∀ (a : ↑Γ(X, V)), (X.presheaf.map i.op) a = 0 → a = 0
<VAR>X : Scheme<VAR>inst✝ : IsIntegral X<VAR>U V : X.Opens<VAR>i : U ⟶ V<VAR>H : Nonempty ↑↑(↑U).toPresheafedSpace<VAR>x : ↑Γ(X, V)<VAR>hx : (X.presheaf.map i.op) x = 0<GOAL>x = 0
<VAR>X : Scheme<VAR>inst✝ : IsIntegral X<VAR>U V : X.Opens<VAR>i : U ⟶ V<VAR>H : Nonempty ↑↑(↑U).toPresheafedSpace<VAR>x : ↑Γ(X, V)<VAR>hx : X.basicOpen ((X.presheaf.map i.op) x) = ⊥<GOAL>X.basicOpen x = ⊥
<VAR>X : Scheme<VAR>inst✝ : IsIntegral X<VAR>U V : X.Opens<VAR>i : U ⟶ V<VAR>H : Nonempty ↑↑(↑U).toPresheafedSpace<VAR>x : ↑Γ(X, V)<VAR>hx : U ⊓ X.basicOpen x = ⊥<GOAL>X.basicOpen x = ⊥
<VAR>X : Scheme<VAR>inst✝ : IsIntegral X<VAR>U V : X.Opens<VAR>i : U ⟶ V<VAR>H : Nonempty ↑↑(↑U).toPresheafedSpace<VAR>x : ↑Γ(X, V)<GOAL>U ⊓ X.basicOpen x = ⊥ → X.basicOpen x = ⊥
<VAR>X : Scheme<VAR>inst✝ : IsIntegral X<VAR>U V : X.Opens<VAR>i : U ⟶ V<VAR>H : Nonempty ↑↑(↑U).toPresheafedSpace<VAR>x : ↑Γ(X, V)<GOAL>X.basicOpen x ≠ ⊥ → U ⊓ X.basicOpen x ≠ ⊥
<VAR>X : Scheme<VAR>inst✝ : IsIntegral X<VAR>U V : X.Opens<VAR>i : U ⟶ V<VAR>H : Nonempty ↑↑(↑U).toPresheafedSpace<VAR>x : ↑Γ(X, V)<GOAL>(↑(X.basicOpen x)).Nonempty → (↑(U ⊓ X.basicOpen x)).Nonempty
<VAR>X : Scheme<VAR>inst✝ : IsIntegral X<VAR>U V : X.Opens<VAR>i : U ⟶ V<VAR>H : Nonempty ↑↑(↑U).toPresheafedSpace<VAR>x : ↑Γ(X, V)<GOAL>(↑U).Nonempty
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝ : (i : ι) → CanonicallyOrderedAddCommMonoid (α i)<VAR>f g : Π₀ (i : ι), α i<GOAL>f + g = 0 ↔ f = 0 ∧ g = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : AddCommMonoid M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : CommSemiring R₁<VAR>inst✝¹² : AddCommMonoid M₁<VAR>inst✝¹¹ : Module R₁ M₁<VAR>inst✝¹⁰ : CommSemiring R₂<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : Module R₂ M₂<VAR>I₁ : R₁ →+* R<VAR>I₂ : R₂ →+* R<VAR>I₁' : R₁ →+* R<VAR>inst✝⁷ : AddCommMonoid Mₗ₁<VAR>inst✝⁶ : AddCommMonoid Mₗ₂<VAR>inst✝⁵ : AddCommMonoid Mₗ₁'<VAR>inst✝⁴ : AddCommMonoid Mₗ₂'<VAR>inst✝³ : Module R Mₗ₁<VAR>inst✝² : Module R Mₗ₂<VAR>inst✝¹ : Module R Mₗ₁'<VAR>inst✝ : Module R Mₗ₂'<VAR>B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M<VAR>e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁'<VAR>e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'<VAR>h : B.SeparatingLeft<VAR>x : Mₗ₁'<VAR>hx : ∀ (y : Mₗ₂'), (((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M))) B) x) y = 0<GOAL>x = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : AddCommMonoid M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : CommSemiring R₁<VAR>inst✝¹² : AddCommMonoid M₁<VAR>inst✝¹¹ : Module R₁ M₁<VAR>inst✝¹⁰ : CommSemiring R₂<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : Module R₂ M₂<VAR>I₁ : R₁ →+* R<VAR>I₂ : R₂ →+* R<VAR>I₁' : R₁ →+* R<VAR>inst✝⁷ : AddCommMonoid Mₗ₁<VAR>inst✝⁶ : AddCommMonoid Mₗ₂<VAR>inst✝⁵ : AddCommMonoid Mₗ₁'<VAR>inst✝⁴ : AddCommMonoid Mₗ₂'<VAR>inst✝³ : Module R Mₗ₁<VAR>inst✝² : Module R Mₗ₂<VAR>inst✝¹ : Module R Mₗ₁'<VAR>inst✝ : Module R Mₗ₂'<VAR>B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M<VAR>e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁'<VAR>e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'<VAR>h : B.SeparatingLeft<VAR>x : Mₗ₁'<VAR>hx : ∀ (y : Mₗ₂'), (((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M))) B) x) y = 0<GOAL>e₁.symm x = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : AddCommMonoid M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : CommSemiring R₁<VAR>inst✝¹² : AddCommMonoid M₁<VAR>inst✝¹¹ : Module R₁ M₁<VAR>inst✝¹⁰ : CommSemiring R₂<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : Module R₂ M₂<VAR>I₁ : R₁ →+* R<VAR>I₂ : R₂ →+* R<VAR>I₁' : R₁ →+* R<VAR>inst✝⁷ : AddCommMonoid Mₗ₁<VAR>inst✝⁶ : AddCommMonoid Mₗ₂<VAR>inst✝⁵ : AddCommMonoid Mₗ₁'<VAR>inst✝⁴ : AddCommMonoid Mₗ₂'<VAR>inst✝³ : Module R Mₗ₁<VAR>inst✝² : Module R Mₗ₂<VAR>inst✝¹ : Module R Mₗ₁'<VAR>inst✝ : Module R Mₗ₂'<VAR>B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M<VAR>e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁'<VAR>e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'<VAR>h : B.SeparatingLeft<VAR>x : Mₗ₁'<VAR>y : Mₗ₂<VAR>hx : (((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M))) B) x) (e₂ y) = 0<GOAL>(B (e₁.symm x)) y = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : AddCommMonoid M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : CommSemiring R₁<VAR>inst✝¹² : AddCommMonoid M₁<VAR>inst✝¹¹ : Module R₁ M₁<VAR>inst✝¹⁰ : CommSemiring R₂<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : Module R₂ M₂<VAR>I₁ : R₁ →+* R<VAR>I₂ : R₂ →+* R<VAR>I₁' : R₁ →+* R<VAR>inst✝⁷ : AddCommMonoid Mₗ₁<VAR>inst✝⁶ : AddCommMonoid Mₗ₂<VAR>inst✝⁵ : AddCommMonoid Mₗ₁'<VAR>inst✝⁴ : AddCommMonoid Mₗ₂'<VAR>inst✝³ : Module R Mₗ₁<VAR>inst✝² : Module R Mₗ₂<VAR>inst✝¹ : Module R Mₗ₁'<VAR>inst✝ : Module R Mₗ₂'<VAR>B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M<VAR>e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁'<VAR>e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'<VAR>h : B.SeparatingLeft<VAR>x : Mₗ₁'<VAR>y : Mₗ₂<VAR>hx : (B (e₁.symm x)) y = 0<GOAL>(B (e₁.symm x)) y = 0
<VAR>R : Type u<VAR>inst✝ : Semiring R<VAR>q n : ℕ<VAR>x y : R<VAR>h : Commute x y<VAR>hprime : Nat.Prime q<VAR>hchar✝ : CharP R q<VAR>this : Fact (Nat.Prime q)<GOAL>(x + y) ^ q ^ n = x ^ q ^ n + y ^ q ^ n
<VAR>X : Compactum<VAR>uux : Ultrafilter (Ultrafilter X.A)<GOAL>(β.μ.app X.A ≫ X.a) uux = X.str (Ultrafilter.map X.str uux)
<VAR>X : Compactum<VAR>uux : Ultrafilter (Ultrafilter X.A)<GOAL>(β.map X.a ≫ X.a) uux = X.str (Ultrafilter.map X.str uux)
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 < x<VAR>hy : 0 < y<GOAL>x < y ^ z ↔ log x < z * log y
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N✝ : Type u_5<VAR>inst✝ : Group N✝<VAR>f : G →* N✝<VAR>H N : Subgroup G<VAR>h : H.normalizer ≤ N<GOAL>H.normalizer.subgroupOf N = (H.subgroupOf N).normalizer
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N✝ : Type u_5<VAR>inst✝ : Group N✝<VAR>f : G →* N✝<VAR>H N : Subgroup G<VAR>h : H.normalizer ≤ N<GOAL>Injective ⇑N.subtype
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N✝ : Type u_5<VAR>inst✝ : Group N✝<VAR>f : G →* N✝<VAR>H N : Subgroup G<VAR>h : H.normalizer ≤ N<GOAL>H.normalizer ≤ N.subtype.range
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : Zero β<VAR>inst✝¹ : SMulZeroClass α β<VAR>inst✝ : DecidableEq β<VAR>s✝ : Finset α<VAR>t : Finset β<VAR>a : α<VAR>s : Finset α<GOAL>s • 0 ⊆ 0
<VAR>x✝ y : ℂ<VAR>x : ℝ<GOAL>(starRingEnd ℂ) (cexp ↑x) = cexp ↑x
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : Measure ℝ<VAR>l : Filter ι<VAR>inst✝² : l.NeBot<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>inst✝ : NormedAddCommGroup E<VAR>a b✝ : ι → ℝ<VAR>f : ℝ → E<VAR>I b : ℝ<VAR>hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) b) μ<VAR>ha : Tendsto a l atBot<VAR>h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I<GOAL>IntegrableOn f (Iic b) μ
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : Measure ℝ<VAR>l : Filter ι<VAR>inst✝² : l.NeBot<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>inst✝ : NormedAddCommGroup E<VAR>a b✝ : ι → ℝ<VAR>f : ℝ → E<VAR>I b : ℝ<VAR>hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) b) μ<VAR>ha : Tendsto a l atBot<VAR>h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I<VAR>hφ : AECover (μ.restrict (Iic b)) l fun i => Ioi (a i)<GOAL>IntegrableOn f (Iic b) μ
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : Measure ℝ<VAR>l : Filter ι<VAR>inst✝² : l.NeBot<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>inst✝ : NormedAddCommGroup E<VAR>a b✝ : ι → ℝ<VAR>f : ℝ → E<VAR>I b : ℝ<VAR>hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc (a i) b) μ<VAR>ha : Tendsto a l atBot<VAR>h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I<VAR>hφ : AECover (μ.restrict (Iic b)) l fun i => Ioi (a i)<VAR>hfi : ∀ (i : ι), IntegrableOn f (Ioi (a i)) (μ.restrict (Iic b))<GOAL>IntegrableOn f (Iic b) μ
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : Measure ℝ<VAR>l : Filter ι<VAR>inst✝² : l.NeBot<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>inst✝ : NormedAddCommGroup E<VAR>a b✝ : ι → ℝ<VAR>f : ℝ → E<VAR>I b : ℝ<VAR>hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc (a i) b) μ<VAR>ha : Tendsto a l atBot<VAR>h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I<VAR>hφ : AECover (μ.restrict (Iic b)) l fun i => Ioi (a i)<VAR>hfi : ∀ (i : ι), IntegrableOn f (Ioi (a i)) (μ.restrict (Iic b))<GOAL>∀ᶠ (x : ι) in l, ∫ (x : ℝ) in a x..b, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioi (a x), ‖f x‖ ∂μ.restrict (Iic b) ≤ I
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : Measure ℝ<VAR>l : Filter ι<VAR>inst✝² : l.NeBot<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>inst✝ : NormedAddCommGroup E<VAR>a b✝ : ι → ℝ<VAR>f : ℝ → E<VAR>I b : ℝ<VAR>hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc (a i) b) μ<VAR>ha : Tendsto a l atBot<VAR>h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I<VAR>hφ : AECover (μ.restrict (Iic b)) l fun i => Ioi (a i)<VAR>hfi : ∀ (i : ι), IntegrableOn f (Ioi (a i)) (μ.restrict (Iic b))<VAR>i : ι<VAR>hai : a i ≤ b<GOAL>∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioi (a i), ‖f x‖ ∂μ.restrict (Iic b) ≤ I
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : Measure ℝ<VAR>l : Filter ι<VAR>inst✝² : l.NeBot<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>inst✝ : NormedAddCommGroup E<VAR>a b✝ : ι → ℝ<VAR>f : ℝ → E<VAR>I b : ℝ<VAR>hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc (a i) b) μ<VAR>ha : Tendsto a l atBot<VAR>h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I<VAR>hφ : AECover (μ.restrict (Iic b)) l fun i => Ioi (a i)<VAR>hfi : ∀ (i : ι), IntegrableOn f (Ioi (a i)) (μ.restrict (Iic b))<VAR>i : ι<VAR>hai : a i ≤ b<GOAL>∫ (x : ℝ) in Ioc (a i) b, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioi (a i) ∩ Iic b, ‖f x‖ ∂μ ≤ I
<VAR>R : Type u<VAR>a✝ b✝ : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>a b : R[ℕ]<GOAL>{ toFinsupp := a * b } = Polynomial.mul { toFinsupp := a } { toFinsupp := b }
<VAR>𝕜 : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>x : H<GOAL>map (↑I.symm) (𝓝[range ↑I] ↑I x) = 𝓝 x
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s✝ t : Set α<VAR>f : α → β<VAR>s : Set α<VAR>h_inf : s.Infinite<VAR>h_fin : (f '' s).Finite<GOAL>¬InjOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s✝ t : Set α<VAR>f : α → β<VAR>s : Set α<VAR>h_inf : s.Infinite<VAR>h_fin : (f '' s).Finite<VAR>this : Finite ↑(f '' s)<GOAL>¬InjOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s✝ t : Set α<VAR>f : α → β<VAR>s : Set α<VAR>h_inf : s.Infinite<VAR>h_fin : (f '' s).Finite<VAR>this✝ : Finite ↑(f '' s)<VAR>this : Infinite ↑s<GOAL>¬InjOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s✝ t : Set α<VAR>f : α → β<VAR>s : Set α<VAR>h_inf : s.Infinite<VAR>h_fin : (f '' s).Finite<VAR>this✝ : Finite ↑(f '' s)<VAR>this : Infinite ↑s<VAR>h : ¬Injective (codRestrict (s.restrict f) (f '' s) ⋯)<GOAL>¬InjOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s✝ t : Set α<VAR>f : α → β<VAR>s : Set α<VAR>h_inf : s.Infinite<VAR>h_fin : (f '' s).Finite<VAR>this✝ : Finite ↑(f '' s)<VAR>this : Infinite ↑s<VAR>h : InjOn f s<GOAL>Injective (codRestrict (s.restrict f) (f '' s) ⋯)
<VAR>f g : CircleDeg1Lift<VAR>x : ℝ<VAR>m : ℤ<VAR>h : f x = x + ↑m<VAR>n : ℕ<GOAL>(⇑f)^[n] x = x + ↑n * ↑m
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>I I' : Ideal R<VAR>J J' : Ideal S<GOAL>map (↑RingEquiv.prodComm) (I.prod J) = J.prod I
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>I I' : Ideal R<VAR>J J' : Ideal S<GOAL>(map (RingHom.fst S R) (map (↑RingEquiv.prodComm) (I.prod J))).prod (map (RingHom.snd S R) (map (↑RingEquiv.prodComm) (I.prod J))) = J.prod I
<VAR>X Y B : CompHaus<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<GOAL>pullback.snd f g = ((pullback.isLimit f g).conePointUniqueUpToIso (limit.isLimit (cospan f g))).hom ≫ Limits.pullback.snd f g
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝.Hom Y✝<VAR>H : IsOpenImmersion f✝<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsOpenImmersion f<VAR>U V : X.Opens<VAR>e : V ≤ f ⁻¹ᵁ f ''ᵁ U<GOAL>V ≤ U
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝.Hom Y✝<VAR>H : IsOpenImmersion f✝<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsOpenImmersion f<VAR>U V : X.Opens<VAR>e : V ≤ f ⁻¹ᵁ f ''ᵁ U<GOAL>(appIso f U).inv ≫ appLE f (f ''ᵁ U) V e = X.presheaf.map (homOfLE ⋯).op
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝.Hom Y✝<VAR>H : IsOpenImmersion f✝<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsOpenImmersion f<VAR>U V : X.Opens<VAR>e : V ≤ f ⁻¹ᵁ f ''ᵁ U<GOAL>X.presheaf.map (eqToHom ⋯) ≫ X.presheaf.map (homOfLE e).op = X.presheaf.map (homOfLE ⋯).op
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝.Hom Y✝<VAR>H : IsOpenImmersion f✝<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsOpenImmersion f<VAR>U V : X.Opens<VAR>e : V ≤ f ⁻¹ᵁ f ''ᵁ U<GOAL>X.presheaf.map (eqToHom ⋯ ≫ (homOfLE e).op) = X.presheaf.map (homOfLE ⋯).op
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z✝ z : K<GOAL>|im z| ≤ ‖z‖
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z✝ z : K<GOAL>im z * im z ≤ normSq z
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>X Y : C<VAR>t : IsInitial X<VAR>f : Y ⟶ X<GOAL>Epi f
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>X Y : C<VAR>t : IsInitial X<VAR>f : Y ⟶ X<VAR>this : IsSplitEpi f<GOAL>Epi f
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f : R⟦X⟧<VAR>a b : R<VAR>n : ℕ<GOAL>(coeff R n) ((rescale b) ((rescale a) f)) = (coeff R n) ((rescale (a * b)) f)
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f : R⟦X⟧<VAR>a b : R<VAR>n : ℕ<GOAL>b ^ n * (a ^ n * (coeff R n) f) = (a * b) ^ n * (coeff R n) f
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝ : AddCommMonoid M<VAR>f : α → α<VAR>x : α<VAR>h : IsFixedPt f x<VAR>g : α → M<VAR>n : ℕ<GOAL>birkhoffSum f g n x = n • g x
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>C : VariableChange R<GOAL>(W.variableChange C).c₄ = ↑C.u⁻¹ ^ 4 * W.c₄
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>C : VariableChange R<GOAL>(↑C.u⁻¹ ^ 2 * (W.b₂ + 12 * C.r)) ^ 2 - 24 * (↑C.u⁻¹ ^ 4 * (W.b₄ + C.r * W.b₂ + 6 * C.r ^ 2)) = ↑C.u⁻¹ ^ 4 * (W.b₂ ^ 2 - 24 * W.b₄)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s t : Multiset α<VAR>a : α<VAR>m : Multiset ι<VAR>f g : ι → α<GOAL>(map (fun x => 1) m).prod = 1
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>e : { w // w ≠ w₀ } ≃ Fin (rank K)<GOAL>regulator K = |(Matrix.of fun i => (logEmbedding K) (fundSystem K (e i))).det|
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>e : { w // w ≠ w₀ } ≃ Fin (rank K)<GOAL>|(Matrix.of fun x => ↑((logEmbeddingEquiv K) (Additive.ofMul ⟦fundSystem K (e x)⟧))).det| = |(Matrix.of fun i => (logEmbedding K) (fundSystem K (e i))).det|
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>inst✝ : NeZero μ<VAR>hf : Integrable (fun x => rexp (f x)) μ<GOAL>(μ.tilted f) Set.univ = 1
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>inst✝ : NeZero μ<VAR>hf : Integrable (fun x => rexp (f x)) μ<GOAL>∫⁻ (a : α), ENNReal.ofReal (rexp (f a)) * (ENNReal.ofReal (∫ (x : α), rexp (f x) ∂μ))⁻¹ ∂μ = 1
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>inst✝ : NeZero μ<VAR>hf : Integrable (fun x => rexp (f x)) μ<GOAL>ENNReal.ofReal (∫ (x : α), rexp (f x) ∂μ) ≠ 0
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>inst✝ : NeZero μ<VAR>hf : Integrable (fun x => rexp (f x)) μ<GOAL>ENNReal.ofReal (∫ (x : α), rexp (f x) ∂μ) ≠ ⊤
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>A : Cᵒᵖ ⥤ Type v<VAR>F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>p : YonedaCollection F Y<GOAL>op (CostructuredArrow.mk (yoneda.map f ≫ p.fst)) = op (CostructuredArrow.mk (map₂ F f p).fst)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ b i * ↑n + ↑n / log ↑n ^ 2
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>n : ℕ<VAR>hn : ∀ (i : α), ‖↑(r i n) - b i * ↑n‖ ≤ ↑n / log ↑n ^ 2<GOAL>∀ (i : α), ↑(r i n) ≤ b i * ↑n + ↑n / log ↑n ^ 2
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>n : ℕ<VAR>hn : ∀ (i : α), ‖↑(r i n) - b i * ↑n‖ ≤ ↑n / log ↑n ^ 2<VAR>i : α<GOAL>↑(r i n) ≤ b i * ↑n + ↑n / log ↑n ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : PartialOrder α<VAR>inst✝⁴ : PartialOrder β<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : OrderTopology β<VAR>e : α ≃o β<GOAL>Continuous ⇑e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : PartialOrder α<VAR>inst✝⁴ : PartialOrder β<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : OrderTopology β<VAR>e : α ≃o β<GOAL>∀ s ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}, IsOpen (⇑e ⁻¹' s)
<VAR>α : Type u<VAR>β : Type v<VAR>l l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>h : a ∉ l<VAR>h' : l.Nodup<GOAL>(l.concat a).Nodup
<VAR>α : Type u<VAR>β : Type v<VAR>l l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>h : a ∉ l<VAR>h' : l.Nodup<GOAL>(l ++ [a]).Nodup
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : StrictConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' S y<GOAL>slope f x y < f'