ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A<VAR>s : Set G<VAR>p : (x : G) → x ∈ closure s → Prop<VAR>one : p 1 ⋯<VAR>mul_right : ∀ (x : G) (hx : x ∈ closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y) ⋯<VAR>mul_right_inv : ∀ (x : G) (hx : x ∈ closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y⁻¹) ⋯<VAR>x : G<VAR>h : x ∈ closure s<GOAL>{ unop' := x } ∈ closure (MulOpposite.unop ⁻¹' s)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p q : R[X]<VAR>hp : p.IsPrimitive<VAR>hq : q ≠ 0<GOAL>p ∣ q.primPart ↔ p ∣ q
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p q : R[X]<VAR>hp : p.IsPrimitive<VAR>hq : q ≠ 0<VAR>h : p ∣ q<GOAL>p ∣ q.primPart
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>hp : p.IsPrimitive<VAR>r : R[X]<VAR>hq : p * r ≠ 0<GOAL>p ∣ (p * r).primPart
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>hp : p.IsPrimitive<VAR>r : R[X]<VAR>hq : p * r ≠ 0<GOAL>p * ?m.99628 = (p * r).primPart
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>hp : p.IsPrimitive<VAR>r : R[X]<VAR>hq : p * r ≠ 0<GOAL>R[X]
<VAR>x✝ y x : ℝ<GOAL>π / 2 - arcsin x ≤ π
<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✝¹¹ : StrongRankCondition R<VAR>inst✝¹⁰ : StrongRankCondition S<VAR>inst✝⁹ : Module S M<VAR>inst✝⁸ : Module.Free S M<VAR>inst✝⁷ : Module S M'<VAR>inst✝⁶ : Module.Free S M'<VAR>inst✝⁵ : Module S M₁<VAR>inst✝⁴ : Module.Free S M₁<VAR>inst✝³ : Algebra S R<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsScalarTower S R M<VAR>inst✝ : Module.Free R M<GOAL>Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} (Module.rank R M) * Cardinal.lift.{v, v'} (Module.rank S M')
<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✝¹¹ : StrongRankCondition R<VAR>inst✝¹⁰ : StrongRankCondition S<VAR>inst✝⁹ : Module S M<VAR>inst✝⁸ : Module.Free S M<VAR>inst✝⁷ : Module S M'<VAR>inst✝⁶ : Module.Free S M'<VAR>inst✝⁵ : Module S M₁<VAR>inst✝⁴ : Module.Free S M₁<VAR>inst✝³ : Algebra S R<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsScalarTower S R M<VAR>inst✝ : Module.Free R M<VAR>fst✝ : Type v<VAR>bM : Basis fst✝ R M<GOAL>Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} (Module.rank R M) * Cardinal.lift.{v, v'} (Module.rank S M')
<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✝¹¹ : StrongRankCondition R<VAR>inst✝¹⁰ : StrongRankCondition S<VAR>inst✝⁹ : Module S M<VAR>inst✝⁸ : Module.Free S M<VAR>inst✝⁷ : Module S M'<VAR>inst✝⁶ : Module.Free S M'<VAR>inst✝⁵ : Module S M₁<VAR>inst✝⁴ : Module.Free S M₁<VAR>inst✝³ : Algebra S R<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsScalarTower S R M<VAR>inst✝ : Module.Free R M<VAR>fst✝¹ : Type v<VAR>bM : Basis fst✝¹ R M<VAR>fst✝ : Type v'<VAR>bN : Basis fst✝ S M'<GOAL>Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} (Module.rank R M) * Cardinal.lift.{v, v'} (Module.rank S M')
<VAR>α : Type u<VAR>σ σ' : Type v<VAR>M : NFA α σ<VAR>x : List α<GOAL>x ∈ M.toDFA.accepts ↔ x ∈ M.accepts
<VAR>α : Type u<VAR>σ σ' : Type v<VAR>M : NFA α σ<VAR>x : List α<GOAL>M.toDFA.eval x ∈ M.toDFA.accept ↔ ∃ S ∈ M.accept, S ∈ M.evalFrom M.start x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : StrictOrderedSemiring α<VAR>inst✝ : Archimedean α<VAR>y x : α<VAR>hy : 0 < y<VAR>this : 0 ≤ 1 + y<VAR>n : ℕ<VAR>h : x ≤ n • y<GOAL>(1 + y) ^ n = (y + 1) ^ n
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : MulOneClass M<VAR>ι : Sort u_4<VAR>S : ι → Submonoid M<VAR>C : M → Prop<VAR>x : M<VAR>hx : x ∈ ⨆ i, S i<VAR>mem : ∀ (i : ι), ∀ x ∈ S i, C x<VAR>one : C 1<VAR>mul : ∀ (x y : M), C x → C y → C (x * y)<GOAL>C x
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : MulOneClass M<VAR>ι : Sort u_4<VAR>S : ι → Submonoid M<VAR>C : M → Prop<VAR>x : M<VAR>hx : x ∈ closure (⋃ i, ↑(S i))<VAR>mem : ∀ (i : ι), ∀ x ∈ S i, C x<VAR>one : C 1<VAR>mul : ∀ (x y : M), C x → C y → C (x * y)<GOAL>C x
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : MulOneClass M<VAR>ι : Sort u_4<VAR>S : ι → Submonoid M<VAR>C : M → Prop<VAR>x✝ : M<VAR>hx✝ : x✝ ∈ closure (⋃ i, ↑(S i))<VAR>mem : ∀ (i : ι), ∀ x ∈ S i, C x<VAR>one : C 1<VAR>mul : ∀ (x y : M), C x → C y → C (x * y)<VAR>x : M<VAR>hx : x ∈ ⋃ i, ↑(S i)<GOAL>C x
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : MulOneClass M<VAR>ι : Sort u_4<VAR>S : ι → Submonoid M<VAR>C : M → Prop<VAR>x✝ : M<VAR>hx✝ : x✝ ∈ closure (⋃ i, ↑(S i))<VAR>mem : ∀ (i : ι), ∀ x ∈ S i, C x<VAR>one : C 1<VAR>mul : ∀ (x y : M), C x → C y → C (x * y)<VAR>x : M<VAR>hx : x ∈ ⋃ i, ↑(S i)<VAR>i : ι<VAR>hi : x ∈ ↑(S i)<GOAL>C x
<VAR>M : Type u_1<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝² : CommGroup G<VAR>g g' : G<VAR>inst✝¹ : T2Space M<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : ContinuousMul M<VAR>f : ℕ → M<VAR>hf : Multipliable fun n => f (n + 1)<GOAL>∏' (b : ℕ), f b = f 0 * ∏' (b : ℕ), f (b + 1)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>A : Type u_1<VAR>inst✝¹ : Category.{?u.20343, u_1} A<VAR>J : GrothendieckTopology C<VAR>S : C<VAR>E : J.OneHypercover S<VAR>i₁ i₂ : E.I₀<VAR>inst✝ : HasPullback (E.f i₁) (E.f i₂)<GOAL>E.sieve₁' i₁ i₂ ∈ J.sieves (Limits.pullback (E.f i₁) (E.f i₂))
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>A : Type u_1<VAR>inst✝¹ : Category.{?u.20343, u_1} A<VAR>J : GrothendieckTopology C<VAR>S : C<VAR>E : J.OneHypercover S<VAR>i₁ i₂ : E.I₀<VAR>inst✝ : HasPullback (E.f i₁) (E.f i₂)<GOAL>E.sieve₁ (pullback.fst (E.f i₁) (E.f i₂)) (pullback.snd (E.f i₁) (E.f i₂)) ∈ J.sieves (Limits.pullback (E.f i₁) (E.f i₂))
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>P : MorphismProperty C<VAR>inst✝¹ : HasPushouts C<VAR>inst✝ : P.RespectsIso<VAR>hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B), P f → P (pushout.inr f g)<VAR>A A' B B' : C<VAR>f : A ⟶ A'<VAR>g : A ⟶ B<VAR>f' : B ⟶ B'<VAR>g' : A' ⟶ B'<VAR>sq : IsPushout g f f' g'<VAR>hf : P f<GOAL>P f'
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>P : MorphismProperty C<VAR>inst✝¹ : HasPushouts C<VAR>inst✝ : P.RespectsIso<VAR>hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B), P f → P (pushout.inr f g)<VAR>A A' B B' : C<VAR>f : A ⟶ A'<VAR>g : A ⟶ B<VAR>f' : B ⟶ B'<VAR>g' : A' ⟶ B'<VAR>sq : IsPushout g f f' g'<VAR>hf : P f<VAR>e : B' ≅ pushout f g := ⋯.isoPushout<GOAL>P f'
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>P : MorphismProperty C<VAR>inst✝¹ : HasPushouts C<VAR>inst✝ : P.RespectsIso<VAR>hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B), P f → P (pushout.inr f g)<VAR>A A' B B' : C<VAR>f : A ⟶ A'<VAR>g : A ⟶ B<VAR>f' : B ⟶ B'<VAR>g' : A' ⟶ B'<VAR>sq : IsPushout g f f' g'<VAR>hf : P f<VAR>e : B' ≅ pushout f g := ⋯.isoPushout<GOAL>P (pushout.inr f g)
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>I : Ideal R<VAR>M✝ : Type u_2<VAR>inst✝¹¹ : AddCommGroup M✝<VAR>inst✝¹⁰ : Module R M✝<VAR>N : Type u_3<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>P : Type u_4<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>T : Type u_5<VAR>inst✝⁵ : AddCommGroup T<VAR>inst✝⁴ : Module (AdicCompletion I R) T<VAR>ι : Type u_6<VAR>inst✝³ : DecidableEq ι<VAR>M : ι → Type u_7<VAR>inst✝² : (i : ι) → AddCommGroup (M i)<VAR>inst✝¹ : (i : ι) → Module R (M i)<VAR>inst✝ : Fintype ι<VAR>x : AdicCompletion I (⨁ (j : ι), M j)<VAR>j : ι<GOAL>((sumInv I M) x) j = (map I (component R ι M j)) x
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>I : Ideal R<VAR>M✝ : Type u_2<VAR>inst✝¹¹ : AddCommGroup M✝<VAR>inst✝¹⁰ : Module R M✝<VAR>N : Type u_3<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>P : Type u_4<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>T : Type u_5<VAR>inst✝⁵ : AddCommGroup T<VAR>inst✝⁴ : Module (AdicCompletion I R) T<VAR>ι : Type u_6<VAR>inst✝³ : DecidableEq ι<VAR>M : ι → Type u_7<VAR>inst✝² : (i : ι) → AddCommGroup (M i)<VAR>inst✝¹ : (i : ι) → Module R (M i)<VAR>inst✝ : Fintype ι<VAR>x✝ : AdicCompletion I (⨁ (j : ι), M j)<VAR>j : ι<VAR>x : AdicCauchySequence I (⨁ (j : ι), M j)<GOAL>((sumInv I M) ((mk I (⨁ (j : ι), M j)) x)) j = (map I (component R ι M j)) ((mk I (⨁ (j : ι), M j)) x)
<VAR>x₀ : ℝ<VAR>a b : ℕ<VAR>f : ℝ → ℝ<VAR>hf : MonotoneOn f (Icc x₀ (x₀ + ↑a))<GOAL>∑ i ∈ Finset.range a, f (x₀ + ↑i) ≤ ∫ (x : ℝ) in x₀..x₀ + ↑a, f x
<VAR>x₀ : ℝ<VAR>a b : ℕ<VAR>f : ℝ → ℝ<VAR>hf : MonotoneOn f (Icc x₀ (x₀ + ↑a))<GOAL>∫ (x : ℝ) in x₀..x₀ + ↑a, -f x ≤ ∑ x ∈ Finset.range a, -f (x₀ + ↑x)
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsSplittingField K L (X ^ n - C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<VAR>σ : L ≃ₐ[K] L<GOAL>σ (rootOfSplitsXPowSubC hn a L) = (autEquivRootsOfUnity hζ hn H L) σ • rootOfSplitsXPowSubC hn a L
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsSplittingField K L (X ^ n - C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<VAR>η : ↥(rootsOfUnity ⟨n, hn⟩ K)<GOAL>((autEquivRootsOfUnity hζ hn H L).symm η) (rootOfSplitsXPowSubC hn a L) = (autEquivRootsOfUnity hζ hn H L) ((autEquivRootsOfUnity hζ hn H L).symm η) • rootOfSplitsXPowSubC hn a L
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsSplittingField K L (X ^ n - C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<VAR>η : ↥(rootsOfUnity ⟨n, hn⟩ K)<GOAL>(((adjoinRootXPowSubCEquiv hζ H ⋯).symm.autCongr.trans (autAdjoinRootXPowSubCEquiv hζ hn H).symm).symm η) (rootOfSplitsXPowSubC hn a L) = η • rootOfSplitsXPowSubC hn a L
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsSplittingField K L (X ^ n - C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<VAR>η : ↥(rootsOfUnity ⟨n, hn⟩ K)<GOAL>↑↑η • rootOfSplitsXPowSubC hn a L = η • rootOfSplitsXPowSubC hn a L
<VAR>k : Type u<VAR>inst✝⁴ : Field k<VAR>K : Type v<VAR>inst✝³ : Field K<VAR>inst✝² : IsSepClosed k<VAR>inst✝¹ : Algebra k K<VAR>inst✝ : Algebra.IsSeparable k K<VAR>x : K<GOAL>(algebraMap k K) (-(minpoly k x).coeff 0) = x
<VAR>k : Type u<VAR>inst✝⁴ : Field k<VAR>K : Type v<VAR>inst✝³ : Field K<VAR>inst✝² : IsSepClosed k<VAR>inst✝¹ : Algebra k K<VAR>inst✝ : Algebra.IsSeparable k K<VAR>x : K<VAR>hq : (minpoly k x).leadingCoeff = 1<GOAL>(algebraMap k K) (-(minpoly k x).coeff 0) = x
<VAR>k : Type u<VAR>inst✝⁴ : Field k<VAR>K : Type v<VAR>inst✝³ : Field K<VAR>inst✝² : IsSepClosed k<VAR>inst✝¹ : Algebra k K<VAR>inst✝ : Algebra.IsSeparable k K<VAR>x : K<VAR>hq : (minpoly k x).leadingCoeff = 1<VAR>hsep : IsSeparable k x<GOAL>(algebraMap k K) (-(minpoly k x).coeff 0) = x
<VAR>k : Type u<VAR>inst✝⁴ : Field k<VAR>K : Type v<VAR>inst✝³ : Field K<VAR>inst✝² : IsSepClosed k<VAR>inst✝¹ : Algebra k K<VAR>inst✝ : Algebra.IsSeparable k K<VAR>x : K<VAR>hq : (minpoly k x).leadingCoeff = 1<VAR>hsep : IsSeparable k x<VAR>h : (minpoly k x).degree = 1<GOAL>(algebraMap k K) (-(minpoly k x).coeff 0) = x
<VAR>k : Type u<VAR>inst✝⁴ : Field k<VAR>K : Type v<VAR>inst✝³ : Field K<VAR>inst✝² : IsSepClosed k<VAR>inst✝¹ : Algebra k K<VAR>inst✝ : Algebra.IsSeparable k K<VAR>x : K<VAR>hq : (minpoly k x).leadingCoeff = 1<VAR>hsep : IsSeparable k x<VAR>h : (minpoly k x).degree = 1<VAR>this : (aeval x) (minpoly k x) = 0<GOAL>(algebraMap k K) (-(minpoly k x).coeff 0) = x
<VAR>k : Type u<VAR>inst✝⁴ : Field k<VAR>K : Type v<VAR>inst✝³ : Field K<VAR>inst✝² : IsSepClosed k<VAR>inst✝¹ : Algebra k K<VAR>inst✝ : Algebra.IsSeparable k K<VAR>x : K<VAR>hq : (minpoly k x).leadingCoeff = 1<VAR>hsep : IsSeparable k x<VAR>h : (minpoly k x).degree = 1<VAR>this : x = -(algebraMap k K) ((minpoly k x).coeff 0)<GOAL>(algebraMap k K) (-(minpoly k x).coeff 0) = x
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : HasContDiffBump E<VAR>inst✝⁵ : MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x✝ : E<VAR>n : ℕ∞<VAR>μ : Measure E<VAR>inst✝⁴ : BorelSpace E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : IsLocallyFiniteMeasure μ<VAR>inst✝¹ : μ.IsOpenPosMeasure<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>K : ℝ<VAR>h : f.rOut ≤ K * f.rIn<VAR>x : E<GOAL>f.normed μ x ≤ K ^ finrank ℝ E / (μ (closedBall c f.rOut)).toReal
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : HasContDiffBump E<VAR>inst✝⁵ : MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x✝ : E<VAR>n : ℕ∞<VAR>μ : Measure E<VAR>inst✝⁴ : BorelSpace E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : IsLocallyFiniteMeasure μ<VAR>inst✝¹ : μ.IsOpenPosMeasure<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>K : ℝ<VAR>h : f.rOut ≤ K * f.rIn<VAR>x : E<VAR>K_pos : 0 < K<GOAL>f.normed μ x ≤ K ^ finrank ℝ E / (μ (closedBall c f.rOut)).toReal
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : HasContDiffBump E<VAR>inst✝⁵ : MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x✝ : E<VAR>n : ℕ∞<VAR>μ : Measure E<VAR>inst✝⁴ : BorelSpace E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : IsLocallyFiniteMeasure μ<VAR>inst✝¹ : μ.IsOpenPosMeasure<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>K : ℝ<VAR>h : f.rOut ≤ K * f.rIn<VAR>x : E<VAR>K_pos : 0 < K<VAR>this : ↑f x / ∫ (y : E), ↑f y ∂μ ≤ 1 / ∫ (y : E), ↑f y ∂μ<GOAL>1 / ∫ (y : E), ↑f y ∂μ ≤ K ^ finrank ℝ E / (μ (closedBall c f.rOut)).toReal
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : HasContDiffBump E<VAR>inst✝⁵ : MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x✝ : E<VAR>n : ℕ∞<VAR>μ : Measure E<VAR>inst✝⁴ : BorelSpace E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : IsLocallyFiniteMeasure μ<VAR>inst✝¹ : μ.IsOpenPosMeasure<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>K : ℝ<VAR>h : f.rOut ≤ K * f.rIn<VAR>x : E<VAR>K_pos : 0 < K<VAR>this : ↑f x / ∫ (y : E), ↑f y ∂μ ≤ 1 / ∫ (y : E), ↑f y ∂μ<GOAL>(μ (closedBall c f.rOut)).toReal / K ^ finrank ℝ E ≤ ∫ (x : E), ↑f x ∂μ
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : HasContDiffBump E<VAR>inst✝⁵ : MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x✝ : E<VAR>n : ℕ∞<VAR>μ : Measure E<VAR>inst✝⁴ : BorelSpace E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : IsLocallyFiniteMeasure μ<VAR>inst✝¹ : μ.IsOpenPosMeasure<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>K : ℝ<VAR>h : f.rOut ≤ K * f.rIn<VAR>x : E<VAR>K_pos : 0 < K<VAR>this : ↑f x / ∫ (y : E), ↑f y ∂μ ≤ 1 / ∫ (y : E), ↑f y ∂μ<GOAL>0 < (μ (closedBall c f.rOut)).toReal
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Ring R<VAR>p✝ p q : R[X]<VAR>hp : p.Monic<VAR>hpq : q.degree < p.degree<GOAL>(p - q).Monic
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Ring R<VAR>p✝ p q : R[X]<VAR>hp : p.Monic<VAR>hpq : q.degree < p.degree<GOAL>(p + -q).Monic
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Ring R<VAR>p✝ p q : R[X]<VAR>hp : p.Monic<VAR>hpq : q.degree < p.degree<GOAL>(-q).degree < p.degree
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>x : ↑(F.obj X)<VAR>h : F.map f x = F.map g x<GOAL>((Types.equalizerIso (F.map f) (F.map g)).inv ≫ (PreservesEqualizer.iso (F ⋙ FintypeCat.incl) f g).inv ≫ (F ⋙ FintypeCat.incl).map (equalizer.ι f g)) ⟨x, h⟩ = x
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<GOAL>finrank ℤ ↥↑↑I = finrank ℤ (𝓞 K)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : Fintype m<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Nontrivial R<VAR>h_det : (mvPolynomialX m m R).det = 0<GOAL>False
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : Fintype m<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Nontrivial R<VAR>h_det : (mvPolynomialX m m R).det = 0<VAR>this : ((MvPolynomial.eval fun p => 1 p.1 p.2).mapMatrix (mvPolynomialX m m R)).det = det 1<GOAL>False
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : Fintype m<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Nontrivial R<VAR>h_det : (mvPolynomialX m m R).det = 0<VAR>this : 0 = 1<GOAL>False
<VAR>R : Type u<VAR>inst₁ inst₂ : AddMonoidWithOne R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_one : One.one = One.one<VAR>h_monoid : toAddMonoid = toAddMonoid<VAR>h_zero' : AddMonoid.toZero = AddMonoid.toZero<GOAL>inst₁ = inst₂
<VAR>R : Type u<VAR>inst₁ inst₂ : AddMonoidWithOne R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_one : One.one = One.one<VAR>h_monoid : toAddMonoid = toAddMonoid<VAR>h_zero' : AddMonoid.toZero = AddMonoid.toZero<VAR>h_one' : toOne = toOne<GOAL>inst₁ = inst₂
<VAR>R : Type u<VAR>inst₁ inst₂ : AddMonoidWithOne R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_one : One.one = One.one<VAR>h_monoid : toAddMonoid = toAddMonoid<VAR>h_zero' : AddMonoid.toZero = AddMonoid.toZero<VAR>h_one' : toOne = toOne<VAR>h_natCast : NatCast.natCast = NatCast.natCast<GOAL>inst₁ = inst₂
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs : IsLindelof s<VAR>f : Filter X<VAR>inst✝ : CountableInterFilter f<VAR>hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f<GOAL>sᶜ ∈ f
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs : IsLindelof s<VAR>f : Filter X<VAR>inst✝ : CountableInterFilter f<VAR>hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f<VAR>x : X<VAR>hx : x ∈ s<GOAL>sᶜ ∈ 𝓝 x ⊓ f
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs : IsLindelof s<VAR>f : Filter X<VAR>inst✝ : CountableInterFilter f<VAR>hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f<VAR>x : X<VAR>hx : x ∈ s<GOAL>∃ i ∈ 𝓝 x ⊓ 𝓟 s, (id i)ᶜ ∈ f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : CommMonoid M<VAR>ψ : AddChar R M<VAR>n : ℕ<VAR>x : R<GOAL>(ψ.mulShift ↑n) x = ψ x ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Sort u_5<VAR>f : Filter α<VAR>inst✝ : f.IsCountablyGenerated<VAR>x : ℕ → Set α<VAR>hx : f.HasAntitoneBasis x<GOAL>∀ {s : Set α}, s ∈ f ↔ ∃ i, x i ⊆ s
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝³ : Monoid N<VAR>inst✝² : Nontrivial ι<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>a : ι → G<VAR>α : Type u_4<VAR>inst✝ : MulAction G α<VAR>X Y : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)<VAR>hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)<VAR>hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i<VAR>hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i<VAR>this : FreeGroup.lift a = (lift fun i => FreeGroup.lift fun x => a i).comp freeGroupEquivCoprodI.toMonoidHom<GOAL>Function.Injective ⇑(FreeGroup.lift a)
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝³ : Monoid N<VAR>inst✝² : Nontrivial ι<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>a : ι → G<VAR>α : Type u_4<VAR>inst✝ : MulAction G α<VAR>X Y : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)<VAR>hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)<VAR>hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i<VAR>hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i<VAR>this : FreeGroup.lift a = (lift fun i => FreeGroup.lift fun x => a i).comp freeGroupEquivCoprodI.toMonoidHom<GOAL>Function.Injective (⇑(lift fun i => FreeGroup.lift fun x => a i) ∘ ⇑freeGroupEquivCoprodI.toMonoidHom)
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝³ : Monoid N<VAR>inst✝² : Nontrivial ι<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>a : ι → G<VAR>α : Type u_4<VAR>inst✝ : MulAction G α<VAR>X Y : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)<VAR>hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)<VAR>hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i<VAR>hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i<GOAL>Function.Injective (⇑(lift fun i => FreeGroup.lift fun x => a i) ∘ ⇑freeGroupEquivCoprodI.toMonoidHom)
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝³ : Monoid N<VAR>inst✝² : Nontrivial ι<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>a : ι → G<VAR>α : Type u_4<VAR>inst✝ : MulAction G α<VAR>X Y : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)<VAR>hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)<VAR>hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i<VAR>hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i<GOAL>Function.Injective ⇑(lift fun i => FreeGroup.lift fun x => a i)
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝³ : Monoid N<VAR>inst✝² : Nontrivial ι<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>a : ι → G<VAR>α : Type u_4<VAR>inst✝ : MulAction G α<VAR>X Y : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)<VAR>hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)<VAR>hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i<VAR>hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i<VAR>H : ι → Type := fun _i => FreeGroup Unit<VAR>f : (i : ι) → H i →* G := fun i => FreeGroup.lift fun x => a i<VAR>X' : ι → Set α := fun i => X i ∪ Y i<GOAL>Function.Injective ⇑(lift fun i => FreeGroup.lift fun x => a i)
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝³ : Monoid N<VAR>inst✝² : Nontrivial ι<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>a : ι → G<VAR>α : Type u_4<VAR>inst✝ : MulAction G α<VAR>X Y : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)<VAR>hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)<VAR>hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i<VAR>hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i<VAR>H : ι → Type := fun _i => FreeGroup Unit<VAR>f : (i : ι) → H i →* G := fun i => FreeGroup.lift fun x => a i<VAR>X' : ι → Set α := fun i => X i ∪ Y i<GOAL>∀ (i : ι), (X' i).Nonempty