ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>γ : α → Type u_2<VAR>δ : α → Type u_3<VAR>s : (a : α) → Finset (γ a)<VAR>f x✝ : (a : α) → δ a<GOAL>(x✝ ∈ piFinset fun i => {f i}) ↔ x✝ ∈ {f}
<VAR>X Y B : Profinite<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<GOAL>pullback.fst f g = ((pullback.isLimit f g).conePointUniqueUpToIso (limit.isLimit (cospan f g))).hom ≫ Limits.pullback.fst f g
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s₁ s₂ : AffineSubspace k P<VAR>p : P<VAR>h₁ : p ∈ s₁<VAR>h₂ : p ∈ s₂<VAR>v : V<GOAL>v ∈ (s₁ ⊓ s₂).direction ↔ v ∈ s₁.direction ⊓ s₂.direction
<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✝² : OpensMeasurableSpace X<VAR>A K : Set X<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : SecondCountableTopologyEither X R<VAR>g g' : X → R<VAR>hg : IntegrableOn g A μ<VAR>hg' : ContinuousOn g' K<VAR>hA : MeasurableSet A<VAR>hK : IsCompact K<VAR>hAK : A ⊆ K<GOAL>IntegrableOn (fun x => g x * g' x) A μ
<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✝² : OpensMeasurableSpace X<VAR>A K : Set X<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : SecondCountableTopologyEither X R<VAR>g g' : X → R<VAR>hg : IntegrableOn g A μ<VAR>hg' : ContinuousOn g' K<VAR>hA : MeasurableSet A<VAR>hK : IsCompact K<VAR>hAK : A ⊆ K<VAR>C : ℝ<VAR>hC : ∀ x ∈ K, ‖g' x‖ ≤ C<GOAL>IntegrableOn (fun x => g x * g' x) A μ
<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✝² : OpensMeasurableSpace X<VAR>A K : Set X<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : SecondCountableTopologyEither X R<VAR>g g' : X → R<VAR>hg : Memℒp g 1 (μ.restrict A)<VAR>hg' : ContinuousOn g' K<VAR>hA : MeasurableSet A<VAR>hK : IsCompact K<VAR>hAK : A ⊆ K<VAR>C : ℝ<VAR>hC : ∀ x ∈ K, ‖g' x‖ ≤ C<GOAL>Memℒp (fun x => g x * g' x) 1 (μ.restrict A)
<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✝² : OpensMeasurableSpace X<VAR>A K : Set X<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : SecondCountableTopologyEither X R<VAR>g g' : X → R<VAR>hg : Memℒp g 1 (μ.restrict A)<VAR>hg' : ContinuousOn g' K<VAR>hA : MeasurableSet A<VAR>hK : IsCompact K<VAR>hAK : A ⊆ K<VAR>C : ℝ<VAR>hC : ∀ x ∈ K, ‖g' x‖ ≤ C<VAR>this : ∀ᵐ (x : X) ∂μ.restrict A, ‖g x * g' x‖ ≤ C * ‖g x‖<GOAL>Memℒp (fun x => g x * g' x) 1 (μ.restrict A)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>U : Set G<VAR>hU : (interior U).Nonempty<VAR>K : Set G<VAR>hK : IsCompact K<VAR>a✝ : { carrier := K, isCompact' := hK } ∈ univ<GOAL>prehaar (↑K₀) U { carrier := K, isCompact' := hK } ∈ (fun K => Icc 0 ↑(index ↑K ↑K₀)) { carrier := K, isCompact' := hK }
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>U : Set G<VAR>hU : (interior U).Nonempty<VAR>K : Set G<VAR>hK : IsCompact K<VAR>a✝ : { carrier := K, isCompact' := hK } ∈ univ<GOAL>0 ≤ prehaar (↑K₀) U { carrier := K, isCompact' := hK } ∧ prehaar (↑K₀) U { carrier := K, isCompact' := hK } ≤ ↑(index ↑{ carrier := K, isCompact' := hK } ↑K₀)
<VAR>α : Type u_1<VAR>inst✝ : OrderedSemiring α<VAR>x : ↑(Icc 0 1)<GOAL>x = 0 ↔ ↑x = 0
<VAR>A : Type u_1<VAR>inst✝³ : Category.{?u.8867, u_1} A<VAR>inst✝² : ConcreteCategory A<VAR>inst✝¹ : ReflectsFiniteLimits (CategoryTheory.forget A)<VAR>F : LightProfiniteᵒᵖ ⥤ A<VAR>inst✝ : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A)<VAR>hF : EqualizerCondition (F ⋙ CategoryTheory.forget A)<GOAL>IsSheaf (coherentTopology LightProfinite) F
<VAR>A : Type u_1<VAR>inst✝³ : Category.{?u.8867, u_1} A<VAR>inst✝² : ConcreteCategory A<VAR>inst✝¹ : ReflectsFiniteLimits (CategoryTheory.forget A)<VAR>F : LightProfiniteᵒᵖ ⥤ A<VAR>inst✝ : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A)<VAR>hF : EqualizerCondition (F ⋙ CategoryTheory.forget A)<GOAL>IsSheaf (coherentTopology LightProfinite) (F ⋙ CategoryTheory.forget A)
<VAR>A : Type u_1<VAR>inst✝³ : Category.{?u.8867, u_1} A<VAR>inst✝² : ConcreteCategory A<VAR>inst✝¹ : ReflectsFiniteLimits (CategoryTheory.forget A)<VAR>F : LightProfiniteᵒᵖ ⥤ A<VAR>inst✝ : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A)<VAR>hF : EqualizerCondition (F ⋙ CategoryTheory.forget A)<GOAL>Nonempty (PreservesFiniteProducts (F ⋙ CategoryTheory.forget A)) ∧ EqualizerCondition (F ⋙ CategoryTheory.forget A)
<VAR>e : ℂ → ℂ<VAR>e' : ℂ<VAR>z : ℝ<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>hf : HasDerivAt e e' ↑z<GOAL>HasDerivAt (fun y => e ↑y) e' z
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V × V<VAR>hx1 : x.1 ≠ 0<VAR>hx2 : x.2 ≠ 0<GOAL>ContinuousAt (fun y => o.oangle y.1 y.2) x
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V × V<VAR>hx1 : x.1 ≠ 0<VAR>hx2 : x.2 ≠ 0<GOAL>(o.kahler x.1) x.2 ≠ 0
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V × V<VAR>hx1 : x.1 ≠ 0<VAR>hx2 : x.2 ≠ 0<GOAL>ContinuousAt (fun y => (o.kahler y.1) y.2) x
<VAR>n m : ℕ<VAR>hm : n ≠ m<GOAL>(2 ^ n).testBit m = false
<VAR>n m : ℕ<VAR>hm : n ≠ m<GOAL>(1 &&& 2 ^ n / 2 ^ m != 0) = false
<VAR>n m : ℕ<VAR>hm✝ : n ≠ m<VAR>hm : n < m<GOAL>(1 &&& 2 ^ n / 2 ^ m != 0) = false
<VAR>n m : ℕ<VAR>hm✝ : n ≠ m<VAR>hm : m < n<GOAL>(1 &&& 2 ^ n / 2 ^ m != 0) = false
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁✝ l₂✝ l₃ : List α<VAR>a✝ b : α<VAR>m n : ℕ<VAR>l₁ l₂ : List α<VAR>a : α<GOAL>l₁ <+: l₂ ++ [a] ↔ l₁ = l₂ ++ [a] ∨ l₁ <+: l₂
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s✝ s t : Multiset α<VAR>h : s ⊆ t<GOAL>s.ndinter t = s
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<VAR>a✝ b✝ : List α<VAR>h : Quot.mk Setoid.r a✝ ⊆ Quot.mk Setoid.r b✝<GOAL>ndinter (Quot.mk Setoid.r a✝) (Quot.mk Setoid.r b✝) = Quot.mk Setoid.r a✝
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>p : PrimeSpectrum R<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>h : Function.Exact ⇑f ⇑g<VAR>hf : Function.Injective ⇑f<VAR>hg : Function.Surjective ⇑g<GOAL>support R N = support R M ∪ support R P
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>p : PrimeSpectrum R<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>h : Function.Exact ⇑f ⇑g<VAR>hf : Function.Injective ⇑f<VAR>hg : Function.Surjective ⇑g<GOAL>support R N ⊆ support R M ∪ support R P
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>p : PrimeSpectrum R<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>h : Function.Exact ⇑f ⇑g<VAR>hf : Function.Injective ⇑f<VAR>hg : Function.Surjective ⇑g<VAR>x : PrimeSpectrum R<GOAL>x ∈ support R N → x ∈ support R M ∪ support R P
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>p : PrimeSpectrum R<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>h : Function.Exact ⇑f ⇑g<VAR>hf : Function.Injective ⇑f<VAR>hg : Function.Surjective ⇑g<VAR>x : PrimeSpectrum R<GOAL>x ∉ support R M ∪ support R P → x ∉ support R N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>p : PrimeSpectrum R<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>h : Function.Exact ⇑f ⇑g<VAR>hf : Function.Injective ⇑f<VAR>hg : Function.Surjective ⇑g<VAR>x : PrimeSpectrum R<GOAL>(∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0) → (∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0) → ∀ (m : N), ∃ r ∉ x.asIdeal, r • m = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>p : PrimeSpectrum R<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>h : Function.Exact ⇑f ⇑g<VAR>hf : Function.Injective ⇑f<VAR>hg : Function.Surjective ⇑g<VAR>x : PrimeSpectrum R<VAR>H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0<VAR>H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0<VAR>m : N<VAR>r : R<VAR>hr : r ∉ x.asIdeal<VAR>e₁ : r • g m = 0<GOAL>∃ r ∉ x.asIdeal, r • m = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>p : PrimeSpectrum R<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>h : Function.Exact ⇑f ⇑g<VAR>hf : Function.Injective ⇑f<VAR>hg : Function.Surjective ⇑g<VAR>x : PrimeSpectrum R<VAR>H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0<VAR>H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0<VAR>m : N<VAR>r : R<VAR>hr : r ∉ x.asIdeal<VAR>e₁ : r • m ∈ Set.range ⇑f<GOAL>∃ r ∉ x.asIdeal, r • m = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>p : PrimeSpectrum R<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>h : Function.Exact ⇑f ⇑g<VAR>hf : Function.Injective ⇑f<VAR>hg : Function.Surjective ⇑g<VAR>x : PrimeSpectrum R<VAR>H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0<VAR>H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0<VAR>m : N<VAR>r : R<VAR>hr : r ∉ x.asIdeal<VAR>m' : M<VAR>hm' : f m' = r • m<VAR>s : R<VAR>hs : s ∉ x.asIdeal<VAR>e₁ : s • m' = 0<GOAL>∃ r ∉ x.asIdeal, r • m = 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>h : HasFDerivAt f f' x<VAR>x✝ : E<GOAL>(fderiv 𝕜 f x) x✝ = f' x✝
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>p₁ p₂ : ℕ<VAR>hp₁ : Fact (Nat.Prime p₁)<VAR>hp₂ : Fact (Nat.Prime p₂)<VAR>hne : p₁ ≠ p₂<VAR>H₁ H₂ : Subgroup G<VAR>hH₁ : IsPGroup p₁ ↥H₁<VAR>hH₂ : IsPGroup p₂ ↥H₂<GOAL>Disjoint H₁ H₂
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>p₁ p₂ : ℕ<VAR>hp₁ : Fact (Nat.Prime p₁)<VAR>hp₂ : Fact (Nat.Prime p₂)<VAR>hne : p₁ ≠ p₂<VAR>H₁ H₂ : Subgroup G<VAR>hH₁ : IsPGroup p₁ ↥H₁<VAR>hH₂ : IsPGroup p₂ ↥H₂<GOAL>∀ {x : G}, x ∈ H₁ → x ∈ H₂ → x = 1
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>p₁ p₂ : ℕ<VAR>hp₁ : Fact (Nat.Prime p₁)<VAR>hp₂ : Fact (Nat.Prime p₂)<VAR>hne : p₁ ≠ p₂<VAR>H₁ H₂ : Subgroup G<VAR>hH₁ : IsPGroup p₁ ↥H₁<VAR>hH₂ : IsPGroup p₂ ↥H₂<VAR>x : G<VAR>hx₁ : x ∈ H₁<VAR>hx₂ : x ∈ H₂<GOAL>x = 1
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>p₁ p₂ : ℕ<VAR>hp₁ : Fact (Nat.Prime p₁)<VAR>hp₂ : Fact (Nat.Prime p₂)<VAR>hne : p₁ ≠ p₂<VAR>H₁ H₂ : Subgroup G<VAR>hH₁ : IsPGroup p₁ ↥H₁<VAR>hH₂ : IsPGroup p₂ ↥H₂<VAR>x : G<VAR>hx₁ : x ∈ H₁<VAR>hx₂ : x ∈ H₂<VAR>n₁ : ℕ<VAR>hn₁ : orderOf ⟨x, hx₁⟩ = p₁ ^ n₁<GOAL>x = 1
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>p₁ p₂ : ℕ<VAR>hp₁ : Fact (Nat.Prime p₁)<VAR>hp₂ : Fact (Nat.Prime p₂)<VAR>hne : p₁ ≠ p₂<VAR>H₁ H₂ : Subgroup G<VAR>hH₁ : IsPGroup p₁ ↥H₁<VAR>hH₂ : IsPGroup p₂ ↥H₂<VAR>x : G<VAR>hx₁ : x ∈ H₁<VAR>hx₂ : x ∈ H₂<VAR>n₁ : ℕ<VAR>hn₁ : orderOf ⟨x, hx₁⟩ = p₁ ^ n₁<VAR>n₂ : ℕ<VAR>hn₂ : orderOf ⟨x, hx₂⟩ = p₂ ^ n₂<GOAL>x = 1
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>p₁ p₂ : ℕ<VAR>hp₁ : Fact (Nat.Prime p₁)<VAR>hp₂ : Fact (Nat.Prime p₂)<VAR>hne : p₁ ≠ p₂<VAR>H₁ H₂ : Subgroup G<VAR>hH₁ : IsPGroup p₁ ↥H₁<VAR>hH₂ : IsPGroup p₂ ↥H₂<VAR>x : G<VAR>hx₁ : x ∈ H₁<VAR>hx₂ : x ∈ H₂<VAR>n₁ : ℕ<VAR>hn₁ : orderOf x = p₁ ^ n₁<VAR>n₂ : ℕ<VAR>hn₂ : orderOf x = p₂ ^ n₂<GOAL>x = 1
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>p₁ p₂ : ℕ<VAR>hp₁ : Fact (Nat.Prime p₁)<VAR>hp₂ : Fact (Nat.Prime p₂)<VAR>hne : p₁ ≠ p₂<VAR>H₁ H₂ : Subgroup G<VAR>hH₁ : IsPGroup p₁ ↥H₁<VAR>hH₂ : IsPGroup p₂ ↥H₂<VAR>x : G<VAR>hx₁ : x ∈ H₁<VAR>hx₂ : x ∈ H₂<VAR>n₁ : ℕ<VAR>hn₁ : orderOf x = p₁ ^ n₁<VAR>n₂ : ℕ<VAR>hn₂ : orderOf x = p₂ ^ n₂<VAR>this : p₁ ^ n₁ = p₂ ^ n₂<GOAL>x = 1
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>p₁ p₂ : ℕ<VAR>hp₁ : Fact (Nat.Prime p₁)<VAR>hp₂ : Fact (Nat.Prime p₂)<VAR>hne : p₁ ≠ p₂<VAR>H₁ H₂ : Subgroup G<VAR>hH₁ : IsPGroup p₁ ↥H₁<VAR>hH₂ : IsPGroup p₂ ↥H₂<VAR>x : G<VAR>hx₁ : x ∈ H₁<VAR>hx₂ : x ∈ H₂<VAR>n₂ : ℕ<VAR>hn₂ : orderOf x = p₂ ^ n₂<VAR>hn₁ : orderOf x = p₁ ^ 0<VAR>this : p₁ ^ 0 = p₂ ^ n₂<GOAL>x = 1
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>p₁ p₂ : ℕ<VAR>hp₁ : Fact (Nat.Prime p₁)<VAR>hp₂ : Fact (Nat.Prime p₂)<VAR>hne : p₁ ≠ p₂<VAR>H₁ H₂ : Subgroup G<VAR>hH₁ : IsPGroup p₁ ↥H₁<VAR>hH₂ : IsPGroup p₂ ↥H₂<VAR>x : G<VAR>hx₁ : x ∈ H₁<VAR>hx₂ : x ∈ H₂<VAR>n₁ : ℕ<VAR>hn₁✝ : orderOf x = p₁ ^ n₁<VAR>n₂ : ℕ<VAR>hn₂ : orderOf x = p₂ ^ n₂<VAR>this : p₁ ^ n₁ = p₂ ^ n₂<VAR>hn₁ : n₁ > 0<GOAL>x = 1
<VAR>σ : Type u_1<VAR>inst✝² : Fintype σ<VAR>inst✝¹ : DecidableEq σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<GOAL>Disjoint (filter (fun t => t.1.card < k) (MvPolynomial.NewtonIdentities.pairs σ k)) (filter (fun t => t.1.card = k) (MvPolynomial.NewtonIdentities.pairs σ k))
<VAR>σ : Type u_1<VAR>inst✝² : Fintype σ<VAR>inst✝¹ : DecidableEq σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<GOAL>∀ x ∈ MvPolynomial.NewtonIdentities.pairs σ k, x.1.card < k → ¬x.1.card = k
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<GOAL>Nonempty (T.CompleteType α) ↔ T.IsSatisfiable
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<GOAL>Nonempty (T.CompleteType α) ↔ ((L.lhomWithConstants α).onTheory T).IsSatisfiable
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<GOAL>{p | ∅ ⊆ ↑p} = ∅ ↔ Set.univ = ∅
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>E : Type<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : AddCircle T → E<VAR>c : ℂ<VAR>n : ℤ<GOAL>fourierCoeff (c • f) n = c • fourierCoeff f n
<VAR>a : ℤ<VAR>b : ℕ<VAR>bN0 : b ≠ 0<VAR>cop : a.natAbs.Coprime b<VAR>h : Liouville ↑{ num := a, den := b, den_nz := bN0, reduced := cop }<GOAL>False
<VAR>a : ℤ<VAR>b : ℕ<VAR>bN0 : b ≠ 0<VAR>cop : a.natAbs.Coprime b<VAR>h : Liouville (↑a / ↑b)<GOAL>False
<VAR>a : ℤ<VAR>b : ℕ<VAR>bN0 : b ≠ 0<VAR>cop : a.natAbs.Coprime b<VAR>h : Liouville (↑a / ↑b)<VAR>p q : ℤ<VAR>q1 : 1 < q<VAR>a0 : ↑a / ↑b ≠ ↑p / ↑q<VAR>a1 : |↑a / ↑b - ↑p / ↑q| < 1 / ↑q ^ (b + 1)<GOAL>False
<VAR>a : ℤ<VAR>b : ℕ<VAR>bN0 : b ≠ 0<VAR>cop : a.natAbs.Coprime b<VAR>h : Liouville (↑a / ↑b)<VAR>p q : ℤ<VAR>q1 : 1 < q<VAR>a0 : ↑a / ↑b ≠ ↑p / ↑q<VAR>a1 : |↑a / ↑b - ↑p / ↑q| < 1 / ↑q ^ (b + 1)<VAR>qR0 : 0 < ↑q<GOAL>False
<VAR>a : ℤ<VAR>b : ℕ<VAR>bN0 : b ≠ 0<VAR>cop : a.natAbs.Coprime b<VAR>h : Liouville (↑a / ↑b)<VAR>p q : ℤ<VAR>q1 : 1 < q<VAR>a0 : ↑a / ↑b ≠ ↑p / ↑q<VAR>a1 : |↑a / ↑b - ↑p / ↑q| < 1 / ↑q ^ (b + 1)<VAR>qR0 : 0 < ↑q<VAR>b0 : ↑b ≠ 0<GOAL>False
<VAR>a : ℤ<VAR>b : ℕ<VAR>bN0 : b ≠ 0<VAR>cop : a.natAbs.Coprime b<VAR>h : Liouville (↑a / ↑b)<VAR>p q : ℤ<VAR>q1 : 1 < q<VAR>a0 : ↑a / ↑b ≠ ↑p / ↑q<VAR>a1 : |↑a / ↑b - ↑p / ↑q| < 1 / ↑q ^ (b + 1)<VAR>qR0 : 0 < ↑q<VAR>b0 : ↑b ≠ 0<VAR>bq0 : 0 < ↑b * ↑q<GOAL>False
<VAR>a : ℤ<VAR>b : ℕ<VAR>bN0 : b ≠ 0<VAR>cop : a.natAbs.Coprime b<VAR>h : Liouville (↑a / ↑b)<VAR>p q : ℤ<VAR>q1 : 1 < q<VAR>a0 : ↑a / ↑b ≠ ↑p / ↑q<VAR>qR0 : 0 < ↑q<VAR>b0 : ↑b ≠ 0<VAR>bq0 : 0 < ↑b * ↑q<VAR>a1 : |a * q - ↑b * p| * q ^ (b + 1) < ↑b * q<GOAL>False
<VAR>a : ℤ<VAR>b : ℕ<VAR>bN0 : b ≠ 0<VAR>cop : a.natAbs.Coprime b<VAR>h : Liouville (↑a / ↑b)<VAR>p q : ℤ<VAR>q1 : 1 < q<VAR>qR0 : 0 < ↑q<VAR>b0 : ↑b ≠ 0<VAR>bq0 : 0 < ↑b * ↑q<VAR>a1 : |a * q - ↑b * p| * q ^ (b + 1) < ↑b * q<VAR>a0 : a * q - ↑b * p ≠ 0<GOAL>False
<VAR>a : ℤ<VAR>b : ℕ<VAR>bN0 : b ≠ 0<VAR>cop : a.natAbs.Coprime b<VAR>h : Liouville (↑a / ↑b)<VAR>p : ℤ<VAR>b0 : ↑b ≠ 0<VAR>q : ℕ<VAR>q1 : 1 < ↑q<VAR>qR0 : 0 < ↑↑q<VAR>bq0 : 0 < ↑b * ↑↑q<VAR>a1 : |a * ↑q - ↑b * p| * ↑q ^ (b + 1) < ↑b * ↑q<VAR>a0 : a * ↑q - ↑b * p ≠ 0<GOAL>False
<VAR>a : ℤ<VAR>b : ℕ<VAR>bN0 : b ≠ 0<VAR>cop : a.natAbs.Coprime b<VAR>h : Liouville (↑a / ↑b)<VAR>p : ℤ<VAR>b0 : ↑b ≠ 0<VAR>q : ℕ<VAR>q1 : 1 < ↑q<VAR>qR0 : 0 < ↑↑q<VAR>bq0 : 0 < ↑b * ↑↑q<VAR>a1 : |a * ↑q - ↑b * p| * ↑q ^ (b + 1) < ↑b * ↑q<VAR>a0 : a * ↑q - ↑b * p ≠ 0<VAR>ap : 0 < |a * ↑q - ↑b * p|<GOAL>False
<VAR>a : ℤ<VAR>b : ℕ<VAR>bN0 : b ≠ 0<VAR>cop : a.natAbs.Coprime b<VAR>h : Liouville (↑a / ↑b)<VAR>p : ℤ<VAR>b0 : ↑b ≠ 0<VAR>q : ℕ<VAR>q1 : 1 < ↑q<VAR>qR0 : 0 < ↑↑q<VAR>bq0 : 0 < ↑b * ↑↑q<VAR>a0 : a * ↑q - ↑b * p ≠ 0<VAR>e : ℕ<VAR>he : ↑e = |a * ↑q - ↑b * p|<VAR>a1✝ a1 : ↑e * ↑q ^ (b + 1) < ↑b * ↑q<VAR>ap✝ ap : 0 < ↑e<GOAL>False
<VAR>a : ℤ<VAR>b : ℕ<VAR>bN0 : b ≠ 0<VAR>cop : a.natAbs.Coprime b<VAR>h : Liouville (↑a / ↑b)<VAR>p : ℤ<VAR>b0 : ↑b ≠ 0<VAR>q : ℕ<VAR>qR0 : 0 < ↑↑q<VAR>bq0 : 0 < ↑b * ↑↑q<VAR>a0 : a * ↑q - ↑b * p ≠ 0<VAR>e : ℕ<VAR>he : ↑e = |a * ↑q - ↑b * p|<VAR>a1✝ : ↑e * ↑q ^ (b + 1) < ↑b * ↑q<VAR>ap✝ : 0 < ↑e<VAR>a1 : e * q ^ (b + 1) < b * q<VAR>ap : 0 < e<VAR>q1 : 1 < q<GOAL>False
<VAR>α : Type u_1<VAR>M : α → Type u_2<VAR>u : Ultrafilter α<VAR>L : Language<VAR>inst✝¹ : (a : α) → L.Structure (M a)<VAR>inst✝ : ∀ (a : α), Nonempty (M a)<VAR>β : Type u_3<VAR>φ : L.Formula β<VAR>x : β → (a : α) → M a<GOAL>(φ.Realize fun i => Quotient.mk' (x i)) ↔ ∀ᶠ (a : α) in ↑u, φ.Realize fun i => x i a
<VAR>α : Type u_1<VAR>M : α → Type u_2<VAR>u : Ultrafilter α<VAR>L : Language<VAR>inst✝¹ : (a : α) → L.Structure (M a)<VAR>inst✝ : ∀ (a : α), Nonempty (M a)<VAR>β : Type u_3<VAR>φ : L.Formula β<VAR>x : β → (a : α) → M a<GOAL>BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) default = BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' fun a => default i
<VAR>a✝ b c d : Ordinal.{u}<VAR>a : Ordinal.{u_1}<GOAL>1 ⨳ a = a
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>inst✝⁷ : MonoidalCategory C<VAR>inst✝⁶ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>inst✝¹ : MonoidalCategory E<VAR>inst✝ : BraidedCategory E<VAR>F : LaxBraidedFunctor C D<VAR>G : LaxBraidedFunctor D E<VAR>X Y : C<GOAL>(G.μ (F.obj X) (F.obj Y) ≫ G.map (F.μ X Y)) ≫ G.map (F.map (β_ X Y).hom) = (β_ (G.obj (F.obj X)) (G.obj (F.obj Y))).hom ≫ G.μ (F.obj Y) (F.obj X) ≫ G.map (F.μ Y X)
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>inst✝⁷ : MonoidalCategory C<VAR>inst✝⁶ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>inst✝¹ : MonoidalCategory E<VAR>inst✝ : BraidedCategory E<VAR>F : LaxBraidedFunctor C D<VAR>G : LaxBraidedFunctor D E<VAR>X Y : C<GOAL>G.μ (F.obj X) (F.obj Y) ≫ G.map (β_ (F.obj X) (F.obj Y)).hom ≫ G.map (F.μ Y X) = (β_ (G.obj (F.obj X)) (G.obj (F.obj Y))).hom ≫ G.μ (F.obj Y) (F.obj X) ≫ G.map (F.μ Y X)
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>inst✝⁷ : MonoidalCategory C<VAR>inst✝⁶ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>inst✝¹ : MonoidalCategory E<VAR>inst✝ : BraidedCategory E<VAR>F : LaxBraidedFunctor C D<VAR>G : LaxBraidedFunctor D E<VAR>X Y : C<GOAL>((β_ (G.obj (F.obj X)) (G.obj (F.obj Y))).hom ≫ G.μ (F.obj Y) (F.obj X)) ≫ G.map (F.μ Y X) = (β_ (G.obj (F.obj X)) (G.obj (F.obj Y))).hom ≫ G.μ (F.obj Y) (F.obj X) ≫ G.map (F.μ Y X)
<VAR>n : ℤ<VAR>z τ : ℂ<GOAL>‖jacobiTheta₂_term_fderiv n z τ‖ ≤ 3 * π * ↑|n| ^ 2 * ‖jacobiTheta₂_term n z τ‖
<VAR>n : ℤ<VAR>z τ : ℂ<VAR>hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖<GOAL>‖jacobiTheta₂_term_fderiv n z τ‖ ≤ 3 * π * ↑|n| ^ 2 * ‖jacobiTheta₂_term n z τ‖
<VAR>n : ℤ<VAR>z τ : ℂ<VAR>hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖<GOAL>‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)‖ * ‖(2 * ↑π * I * ↑n) • ContinuousLinearMap.fst ℂ ℂ ℂ + (↑π * I * ↑n ^ 2) • ContinuousLinearMap.snd ℂ ℂ ℂ‖ ≤ ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)‖ * (2 * π * ↑|n| ^ 2 + 1 * π * ↑|n| ^ 2)
<VAR>n : ℤ<VAR>z τ : ℂ<VAR>hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖<GOAL>‖(2 * ↑π * I * ↑n) • ContinuousLinearMap.fst ℂ ℂ ℂ‖ ≤ 2 * π * ↑|n| ^ 2
<VAR>n : ℤ<VAR>z τ : ℂ<VAR>hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖<GOAL>‖(↑π * I * ↑n ^ 2) • ContinuousLinearMap.snd ℂ ℂ ℂ‖ ≤ 1 * π * ↑|n| ^ 2
<VAR>hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p<VAR>n : ℕ<VAR>h : n ≥ 3<GOAL>FermatLastTheoremFor n
<VAR>hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p<VAR>n : ℕ<VAR>h : n ≥ 3<VAR>hdvd : 4 ∣ n<GOAL>FermatLastTheoremWith ℕ 4
<VAR>hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p<VAR>n : ℕ<VAR>h : n ≥ 3<VAR>p : ℕ<VAR>hpprime : Nat.Prime p<VAR>hdvd : p ∣ n<VAR>hpodd : Odd p<GOAL>FermatLastTheoremWith ℕ p
<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 : α → β<GOAL>1 ≤ᶠ[ae μ] g / f ↔ f ≤ᶠ[ae μ] g
<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 : 1 ≤ᶠ[ae μ] g / f<VAR>a : α<VAR>ha : 1 a ≤ (g / f) a<GOAL>f a ≤ g a