ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hab✝ : a ≤ b<VAR>hf✝ : IntervalIntegrable f μ a b<VAR>hg : IntervalIntegrable g μ a b<VAR>c d : ℝ<VAR>hca : c ≤ a<VAR>hab : a ≤ b<VAR>hbd : b ≤ d<VAR>hf : 0 ≤ᶠ[ae (μ.restrict (Ioc c d))] f<VAR>hfi : IntervalIntegrable f μ c d<GOAL>∫ (x : ℝ) in Ioc a b, f x ∂μ ≤ ∫ (x : ℝ) in Ioc c d, f x ∂μ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>a ∆ b ∆ (a ⊓ b) = a ⊔ b
<VAR>x y : SimplexCategory<VAR>f : x ⟶ y<GOAL>Continuous (toTopMap f)
<VAR>x y : SimplexCategory<VAR>f : x ⟶ y<VAR>i : (forget SimplexCategory).obj y<GOAL>Continuous fun a => ∑ j ∈ Finset.filter (fun x_1 => f x_1 = i) Finset.univ, ↑a j
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → α<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>f ∘ f^[n.pred] = f^[n]
<VAR>a✝ b✝ c d m n a b : ℤ<VAR>h : a ≤ b<GOAL>a.toNat ≤ b.toNat
<VAR>a✝ b✝ c d m n a b : ℤ<VAR>h : a ≤ b<GOAL>a ≤ ↑b.toNat
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype o<VAR>inst✝¹ : CommRing R<VAR>inst✝ : StrongRankCondition R<VAR>A : Matrix m n R<VAR>B : Matrix n o R<GOAL>(A * B).rank ≤ A.rank
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype o<VAR>inst✝¹ : CommRing R<VAR>inst✝ : StrongRankCondition R<VAR>A : Matrix m n R<VAR>B : Matrix n o R<GOAL>finrank R ↥(LinearMap.range (A.mulVecLin ∘ₗ B.mulVecLin)) ≤ finrank R ↥(LinearMap.range A.mulVecLin)
<VAR>ι : Type uι<VAR>R : Type uR<VAR>A : Type uA<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : CommSemiring A<VAR>inst✝⁸ : AddCommMonoid M₁<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : Module A M₁<VAR>inst✝³ : SMulCommClass R A M₁<VAR>inst✝² : SMulCommClass A R M₁<VAR>inst✝¹ : IsScalarTower R A M₁<VAR>inst✝ : Module R M₂<VAR>B₁ : BilinMap A M₁ A<VAR>B₂ : BilinMap R M₂ R<VAR>hB₁ : IsSymm B₁<VAR>hB₂ : IsSymm B₂<GOAL>IsSymm (B₁.tmul B₂)
<VAR>ι : Type uι<VAR>R : Type uR<VAR>A : Type uA<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : CommSemiring A<VAR>inst✝⁸ : AddCommMonoid M₁<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : Module A M₁<VAR>inst✝³ : SMulCommClass R A M₁<VAR>inst✝² : SMulCommClass A R M₁<VAR>inst✝¹ : IsScalarTower R A M₁<VAR>inst✝ : Module R M₂<VAR>B₁ : BilinMap A M₁ A<VAR>B₂ : BilinMap R M₂ R<VAR>hB₁ : IsSymm B₁<VAR>hB₂ : IsSymm B₂<GOAL>B₁.tmul B₂ = flip (B₁.tmul B₂)
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>ι : Type v<VAR>inst✝⁶ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : (i : ι) → AddCommGroup (G i)<VAR>f : (i j : ι) → i ≤ j → G i →+ G j<VAR>P : Type u₁<VAR>inst✝³ : AddCommGroup P<VAR>g : (i : ι) → G i →+ P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>G' : ι → Type v'<VAR>inst✝² : (i : ι) → AddCommGroup (G' i)<VAR>f' : (i j : ι) → i ≤ j → G' i →+ G' j<VAR>G'' : ι → Type v''<VAR>inst✝¹ : (i : ι) → AddCommGroup (G'' i)<VAR>f'' : (i j : ι) → i ≤ j → G'' i →+ G'' j<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>g₁ : (i : ι) → G i →+ G' i<VAR>g₂ : (i : ι) → G' i →+ G'' i<VAR>hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i)<VAR>hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)<VAR>i j : ι<VAR>h : i ≤ j<GOAL>((fun i => (g₂ i).comp (g₁ i)) j).comp (f i j h) = (f'' i j h).comp ((fun i => (g₂ i).comp (g₁ i)) i)
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>γ : α → Type u_2<VAR>δ : α → Type u_3<VAR>s✝ : (a : α) → Finset (γ a)<VAR>inst✝ : (a : α) → DecidableEq (δ a)<VAR>f : (a : α) → γ a → δ a<VAR>s : (a : α) → Finset (γ a)<VAR>a✝ : (a : α) → δ a<GOAL>(a✝ ∈ piFinset fun a => image (f a) (s a)) ↔ a✝ ∈ image (fun b a => f a (b a)) (piFinset s)
<VAR>a x z✝ z : ℂ<VAR>hz : z.im < 0<GOAL>z.arg = -Real.arccos (z.re / abs z)
<VAR>a x z✝ z : ℂ<VAR>hz : z.im < 0<VAR>h₀ : z ≠ 0<GOAL>z.arg = -Real.arccos (z.re / abs z)
<VAR>a x z✝ z : ℂ<VAR>hz : z.im < 0<VAR>h₀ : z ≠ 0<GOAL>0 ≤ -z.arg
<VAR>a x z✝ z : ℂ<VAR>hz : z.im < 0<VAR>h₀ : z ≠ 0<GOAL>-z.arg ≤ π
<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>StrictAntiOn (fun x => 1 / log x) (Set.Ioi 1)
<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>StrictAntiOn (fun x => (log x)⁻¹) (Set.Ioi 1)
<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>StrictMonoOn log (Set.Ioi 1)
<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>x : ℝ<VAR>hx : x ∈ Set.Ioi 1<GOAL>x ∈ Set.Ioi 0
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝⁶ : TopologicalSpace F<VAR>inst✝⁵ : TopologicalSpace (TotalSpace F E)<VAR>inst✝⁴ : (x : B) → TopologicalSpace (E x)<VAR>HB : Type u_7<VAR>inst✝³ : TopologicalSpace HB<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : ChartedSpace HB B<VAR>inst✝ : FiberBundle F E<VAR>x : TotalSpace F E<VAR>y : ModelProd HB F<VAR>hy : y ∈ (chartAt (ModelProd HB F) x).target<GOAL>(↑(chartAt (ModelProd HB F) x).symm y).proj = ↑(chartAt HB x.proj).symm y.1
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝⁶ : TopologicalSpace F<VAR>inst✝⁵ : TopologicalSpace (TotalSpace F E)<VAR>inst✝⁴ : (x : B) → TopologicalSpace (E x)<VAR>HB : Type u_7<VAR>inst✝³ : TopologicalSpace HB<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : ChartedSpace HB B<VAR>inst✝ : FiberBundle F E<VAR>x : TotalSpace F E<VAR>y : ModelProd HB F<VAR>hy : y ∈ (chartAt HB x.proj).target ×ˢ univ ∧ ↑((chartAt HB x.proj).prod (PartialEquiv.refl F)).symm y ∈ (trivializationAt F E x.proj).target<GOAL>(↑(trivializationAt F E x.proj).symm (↑((chartAt HB x.proj).prod (PartialHomeomorph.refl F)).symm y)).proj = ↑(chartAt HB x.proj).symm y.1
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>inst✝⁴ : FiniteDimensional F E<VAR>inst✝³ : Algebra.IsSeparable F E<VAR>K : Type u_3<VAR>inst✝² : Field K<VAR>inst✝¹ : IsAlgClosed K<VAR>inst✝ : Algebra F K<GOAL>Fintype.card (E →ₐ[F] K) = finrank F E
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : HasShift C ℤ<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>T : Triangle Cᵒᵖ<GOAL>T ∈ distinguishedTriangles ↔ Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ distinguishedTriangles
<VAR>x y : ℂ<GOAL>sin (x + y) = sin x * cos y + cos x * sin y
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>g : G<VAR>P : Sylow p G<VAR>h : (↑P).Normal<GOAL>g • P = P
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>f : ι → R[X]<VAR>t : Multiset R[X]<VAR>h : ∀ i ∈ s, f i ≠ 0<VAR>a✝ : Nontrivial R<GOAL>(∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>f : ι → R[X]<VAR>t : Multiset R[X]<VAR>h : ∀ i ∈ s, f i ≠ 0<VAR>a✝ : Nontrivial R<GOAL>∏ i ∈ s, (f i).leadingCoeff ≠ 0
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>f : ι → R[X]<VAR>t : Multiset R[X]<VAR>h : ∀ i ∈ s, f i ≠ 0<VAR>a✝ : Nontrivial R<GOAL>∀ a ∈ s, (f a).leadingCoeff ≠ 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>h : f.eraseLead = 0<VAR>hpz : ¬f = 0<GOAL>f.support.card ≤ 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f : α → β<VAR>ι : Sort u_2<VAR>t₁ : TopologicalSpace α<VAR>t₂ : ι → TopologicalSpace β<GOAL>Continuous f ↔ ∀ (i : ι), Continuous f
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>F : ι → X → α<VAR>S : Set X<VAR>x₀ : X<GOAL>EquicontinuousWithinAt F S x₀ ↔ ContinuousWithinAt (⇑UniformFun.ofFun ∘ swap F) S x₀
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>F : ι → X → α<VAR>S : Set X<VAR>x₀ : X<GOAL>EquicontinuousWithinAt F S x₀ ↔ ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[S] x₀, (⇑UniformFun.ofFun ∘ swap F) x ∈ {g | ((⇑UniformFun.ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α i}
<VAR>α : Type u_1<VAR>R✝ : Type u_2<VAR>k : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>ι : Type u_8<VAR>R : Type u_9<VAR>inst✝ : NonAssocRing R<VAR>m : ℤ<GOAL>m • 1 = ↑m
<VAR>α : Type u_1<VAR>l : List α<VAR>is : List (Fin l.length)<VAR>h : Pairwise (fun x x_1 => ↑x < ↑x_1) is<VAR>n : Nat<VAR>l' : List α<VAR>hl' : l' = drop n l<VAR>his : ∀ (i : Fin l.length), i ∈ is → n ≤ ↑i<GOAL>map l.get is <+ l'
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : AddCommMonoid α<VAR>inst✝ : LT α<VAR>s : Finset ι<VAR>f : ι → WithTop α<GOAL>∑ i ∈ s, f i = ⊤ ↔ ∃ i ∈ s, f i = ⊤
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>a x y : E<VAR>h : IsLocalMinOn f s a<VAR>hf : HasFDerivWithinAt f f' s a<VAR>hy : y ∈ posTangentConeAt s a<VAR>hy' : -y ∈ posTangentConeAt s a<GOAL>f' y = 0
<VAR>p : ℕ<VAR>a : ZMod p<VAR>ha : a ^ (p - 1) = 1<VAR>hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1<GOAL>Nat.Prime p
<VAR>p : ℕ<VAR>a : ZMod p<VAR>ha : a ^ (p - 1) = 1<VAR>hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1<VAR>h0 : p ≠ 0<GOAL>Nat.Prime p
<VAR>p : ℕ<VAR>a : ZMod p<VAR>ha : a ^ (p - 1) = 1<VAR>hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1<VAR>h0 : p ≠ 0<VAR>h1 : p ≠ 1<GOAL>Nat.Prime p
<VAR>p : ℕ<VAR>a : ZMod p<VAR>ha : a ^ (p - 1) = 1<VAR>hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1<VAR>h0 : p ≠ 0<VAR>h1 : p ≠ 1<VAR>hp1 : 1 < p<GOAL>Nat.Prime p
<VAR>p : ℕ<VAR>a : ZMod p<VAR>ha : a ^ (p - 1) = 1<VAR>hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1<VAR>h0 : p ≠ 0<VAR>h1 : p ≠ 1<VAR>hp1 : 1 < p<VAR>order_of_a : orderOf a = p - 1<GOAL>Nat.Prime p
<VAR>p : ℕ<VAR>a : ZMod p<VAR>ha : a ^ (p - 1) = 1<VAR>hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1<VAR>h0 : p ≠ 0<VAR>h1 : p ≠ 1<VAR>hp1 : 1 < p<VAR>order_of_a : orderOf a = p - 1<VAR>this : NeZero p<GOAL>Nat.Prime p
<VAR>p : ℕ<VAR>a : ZMod p<VAR>ha : a ^ (p - 1) = 1<VAR>hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1<VAR>h0 : p ≠ 0<VAR>h1 : p ≠ 1<VAR>hp1 : 1 < p<VAR>order_of_a : orderOf a = p - 1<VAR>this : NeZero p<GOAL>Fintype.card (ZMod p)ˣ = p - 1
<VAR>p : ℕ<VAR>a : ZMod p<VAR>ha : a ^ (p - 1) = 1<VAR>hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1<VAR>h0 : p ≠ 0<VAR>h1 : p ≠ 1<VAR>hp1 : 1 < p<VAR>order_of_a : orderOf a = p - 1<VAR>this : NeZero p<GOAL>p - 1 ≤ Fintype.card (ZMod p)ˣ
<VAR>p : ℕ<VAR>a : ZMod p<VAR>ha : a ^ (p - 1) = 1<VAR>hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1<VAR>h0 : p ≠ 0<VAR>h1 : p ≠ 1<VAR>hp1 : 1 < p<VAR>order_of_a : orderOf a = p - 1<VAR>this : NeZero p<VAR>hp' : p - 2 + 1 = p - 1<GOAL>p - 1 ≤ Fintype.card (ZMod p)ˣ
<VAR>p : ℕ<VAR>a : ZMod p<VAR>ha : a ^ (p - 1) = 1<VAR>hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1<VAR>h0 : p ≠ 0<VAR>h1 : p ≠ 1<VAR>hp1 : 1 < p<VAR>order_of_a : orderOf a = p - 1<VAR>this : NeZero p<VAR>hp' : p - 2 + 1 = p - 1<VAR>a' : (ZMod p)ˣ := Units.mkOfMulEqOne a (a ^ (p - 2)) ⋯<GOAL>p - 1 ≤ Fintype.card (ZMod p)ˣ
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : α → β<GOAL>UniformEmbedding f ↔ Injective f ∧ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
<VAR>b p : ℕ<VAR>x✝ : 2 ≤ b<VAR>hp : Odd p<GOAL>(b ^ p - 1) / (b - 1) * ((b ^ p + 1) / (b + 1)) = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
<VAR>b p : ℕ<VAR>x✝ : 2 ≤ b<VAR>hp : Odd p<VAR>q₁ : b - 1 ∣ b ^ p - 1<GOAL>(b ^ p - 1) / (b - 1) * ((b ^ p + 1) / (b + 1)) = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
<VAR>b p : ℕ<VAR>x✝ : 2 ≤ b<VAR>hp : Odd p<VAR>q₁ : b - 1 ∣ b ^ p - 1<VAR>q₂ : b + 1 ∣ b ^ p + 1<GOAL>(b ^ p - 1) / (b - 1) * ((b ^ p + 1) / (b + 1)) = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
<VAR>b p : ℕ<VAR>x✝ : 2 ≤ b<VAR>hp : Odd p<VAR>q₁ : b - 1 ∣ b ^ p - 1<VAR>q₂ : b + 1 ∣ b ^ p + 1<GOAL>b ^ (2 * p) - 1 = (b ^ p) ^ 2 - 1 ^ 2
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n✝ m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>hf : Adapted ℱ f<VAR>n : ℕ<GOAL>StronglyMeasurable fun ω => ∑ k ∈ Finset.range N, ({n | lowerCrossingTime a b f N k ω ≤ n} ∩ {n | n < upperCrossingTime a b f N (k + 1) ω}).indicator 1 n
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n✝ m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>hf : Adapted ℱ f<VAR>n i : ℕ<VAR>x✝ : i ∈ Finset.range N<GOAL>MeasurableSet fun ω => {n | n < upperCrossingTime a b f N (i + 1) ω} n
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n✝ m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>hf : Adapted ℱ f<VAR>n i : ℕ<VAR>x✝ : i ∈ Finset.range N<GOAL>MeasurableSet fun ω => {n | ¬upperCrossingTime a b f N (i + 1) ω ≤ n} n
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>r : R<GOAL>v.valuation ((algebraMap R K) r) = v.intValuation r
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T✝ T'✝ T'' : Set α → E →L[ℝ] F<VAR>C✝ C'✝ C'' : ℝ<VAR>T T' : Set α → E →L[ℝ] F<VAR>C C' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT' : DominatedFinMeasAdditive μ T' C'<VAR>h : T = T'<VAR>f : ↥(Lp E 1 μ)<GOAL>setToL1 hT = setToL1 hT'
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T✝ T'✝ T'' : Set α → E →L[ℝ] F<VAR>C✝ C'✝ C'' : ℝ<VAR>T T' : Set α → E →L[ℝ] F<VAR>C C' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT' : DominatedFinMeasAdditive μ T' C'<VAR>h : T = T'<VAR>f : ↥(Lp E 1 μ)<GOAL>(setToL1 hT').comp (coeToLp α E ℝ) = setToL1SCLM α E μ hT
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T✝ T'✝ T'' : Set α → E →L[ℝ] F<VAR>C✝ C'✝ C'' : ℝ<VAR>T T' : Set α → E →L[ℝ] F<VAR>C C' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT' : DominatedFinMeasAdditive μ T' C'<VAR>h : T = T'<VAR>f✝ : ↥(Lp E 1 μ)<VAR>f : ↥(simpleFunc E 1 μ)<GOAL>(setToL1 hT') ↑f = (setToL1SCLM α E μ hT) f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T✝ T'✝ T'' : Set α → E →L[ℝ] F<VAR>C✝ C'✝ C'' : ℝ<VAR>T T' : Set α → E →L[ℝ] F<VAR>C C' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT' : DominatedFinMeasAdditive μ T' C'<VAR>h : T = T'<VAR>f✝ : ↥(Lp E 1 μ)<VAR>f : ↥(simpleFunc E 1 μ)<GOAL>(setToL1SCLM α E μ hT') f = (setToL1SCLM α E μ hT) f
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>δ K ε x a : ℝ<GOAL>HasDerivAt (fun y => gronwallBound δ K ε (y - a)) (K * gronwallBound δ K ε (x - a) + ε) x
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>δ K ε x a : ℝ<GOAL>K * gronwallBound δ K ε (x - a) + ε = (K * gronwallBound δ K ε (id x - a) + ε) * 1
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>μ : ℝ<VAR>T : E →ₗ[𝕜] E<VAR>hμ : HasEigenvalue T ↑μ<VAR>hnn : ∀ (x : E), 0 < RCLike.re ⟪x, T x⟫_𝕜<GOAL>0 < μ
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>μ : ℝ<VAR>T : E →ₗ[𝕜] E<VAR>hμ : HasEigenvalue T ↑μ<VAR>hnn : ∀ (x : E), 0 < RCLike.re ⟪x, T x⟫_𝕜<VAR>v : E<VAR>hv : HasEigenvector T (↑μ) v<GOAL>0 < μ
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>μ : ℝ<VAR>T : E →ₗ[𝕜] E<VAR>hμ : HasEigenvalue T ↑μ<VAR>hnn : ∀ (x : E), 0 < RCLike.re ⟪x, T x⟫_𝕜<VAR>v : E<VAR>hv : HasEigenvector T (↑μ) v<VAR>hpos : 0 < ‖v‖ ^ 2<GOAL>0 < μ
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>μ : ℝ<VAR>T : E →ₗ[𝕜] E<VAR>hμ : HasEigenvalue T ↑μ<VAR>hnn : ∀ (x : E), 0 < RCLike.re ⟪x, T x⟫_𝕜<VAR>v : E<VAR>hv : HasEigenvector T (↑μ) v<VAR>hpos : 0 < ‖v‖ ^ 2<VAR>this : RCLike.re ⟪v, T v⟫_𝕜 = μ * ‖v‖ ^ 2<GOAL>0 < μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a a' : α<VAR>s : Set α<GOAL>(pure a).toOuterMeasure s = if a ∈ s then 1 else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a a' : α<VAR>s : Set α<GOAL>∑' (x : α), s.indicator (⇑(pure a)) x = if a ∈ s then 1 else 0
<VAR>R : Type u<VAR>inst₁ inst₂ : AddGroupWithOne R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_one : One.one = One.one<GOAL>inst₁ = inst₂
<VAR>R : Type u<VAR>inst₁ inst₂ : AddGroupWithOne R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_one : One.one = One.one<VAR>this : toAddMonoidWithOne = toAddMonoidWithOne<GOAL>inst₁ = inst₂
<VAR>R : Type u<VAR>inst₁ inst₂ : AddGroupWithOne R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_one : One.one = One.one<VAR>this✝ : toAddMonoidWithOne = toAddMonoidWithOne<VAR>this : AddMonoidWithOne.toNatCast = AddMonoidWithOne.toNatCast<VAR>toAddMonoid_eq✝ : AddMonoidWithOne.toAddMonoid = AddMonoidWithOne.toAddMonoid<VAR>toNeg_eq✝ : toNeg = toNeg<VAR>toSub_eq✝ : toSub = toSub<VAR>zsmul_eq✝ : AddGroupWithOne.zsmul = AddGroupWithOne.zsmul<GOAL>inst₁ = inst₂
<VAR>R : Type u<VAR>inst₁ inst₂ : AddGroupWithOne R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_one : One.one = One.one<VAR>this✝¹ : toAddMonoidWithOne = toAddMonoidWithOne<VAR>this✝ : AddMonoidWithOne.toNatCast = AddMonoidWithOne.toNatCast<VAR>toAddMonoid_eq✝ : AddMonoidWithOne.toAddMonoid = AddMonoidWithOne.toAddMonoid<VAR>toNeg_eq✝ : toNeg = toNeg<VAR>toSub_eq✝ : toSub = toSub<VAR>zsmul_eq✝ : AddGroupWithOne.zsmul = AddGroupWithOne.zsmul<VAR>this : IntCast.intCast = IntCast.intCast<GOAL>inst₁ = inst₂
<VAR>R : Type u_1<VAR>inst✝⁸ : CommSemiring R<VAR>S : Type u_2<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Algebra R S<VAR>N : Type u_3<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : Module S N<VAR>inst✝² : IsScalarTower R S N<VAR>ι : Type u_4<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>x : N<VAR>i : ι<GOAL>(TensorProduct.piScalarRightInv R S N ι) (Pi.single i x) = x ⊗ₜ[R] Pi.single i 1
<VAR>k : Type u_1<VAR>inst✝⁷ : Field k<VAR>K : Type u_2<VAR>inst✝⁶ : Field K<VAR>F : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : NumberField K<VAR>inst✝³ : Algebra k K<VAR>inst✝² : Algebra k F<VAR>inst✝¹ : Algebra K F<VAR>inst✝ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>φ : K →+* ℂ<VAR>h : ComplexEmbedding.IsConj φ σ<GOAL>IsUnramified k (mk φ) ↔ σ = 1
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>inst✝ : Field k<VAR>r : k<GOAL>((C σ k) r)⁻¹ = (C σ k) r⁻¹
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>inst✝ : Field k<GOAL>((C σ k) 0)⁻¹ = (C σ k) 0⁻¹
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>inst✝ : Field k<VAR>r : k<VAR>hr : r ≠ 0<GOAL>((C σ k) r)⁻¹ = (C σ k) r⁻¹
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>inst✝ : Field k<VAR>r : k<VAR>hr : r ≠ 0<GOAL>(constantCoeff σ k) ((C σ k) r) ≠ 0
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>D : Type u_5<VAR>E : Type u_6<VAR>inst✝¹² : Monoid A<VAR>inst✝¹¹ : Monoid B<VAR>inst✝¹⁰ : Monoid C<VAR>inst✝⁹ : Monoid D<VAR>inst✝⁸ : CommGroup E<VAR>inst✝⁷ : TopologicalSpace A<VAR>inst✝⁶ : TopologicalSpace B<VAR>inst✝⁵ : TopologicalSpace C<VAR>inst✝⁴ : TopologicalSpace D<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : TopologicalGroup E<VAR>inst✝¹ : ContinuousMul B<VAR>inst✝ : T2Space B<GOAL>IsClosed (Set.range toContinuousMap)
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>D : Type u_5<VAR>E : Type u_6<VAR>inst✝¹² : Monoid A<VAR>inst✝¹¹ : Monoid B<VAR>inst✝¹⁰ : Monoid C<VAR>inst✝⁹ : Monoid D<VAR>inst✝⁸ : CommGroup E<VAR>inst✝⁷ : TopologicalSpace A<VAR>inst✝⁶ : TopologicalSpace B<VAR>inst✝⁵ : TopologicalSpace C<VAR>inst✝⁴ : TopologicalSpace D<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : TopologicalGroup E<VAR>inst✝¹ : ContinuousMul B<VAR>inst✝ : T2Space B<GOAL>IsClosed ({a | a 1 = 1} ∩ ⋂ i, ⋂ i_1, {x | x (i * i_1) = x i * x i_1})
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>D : Type u_5<VAR>E : Type u_6<VAR>inst✝¹² : Monoid A<VAR>inst✝¹¹ : Monoid B<VAR>inst✝¹⁰ : Monoid C<VAR>inst✝⁹ : Monoid D<VAR>inst✝⁸ : CommGroup E<VAR>inst✝⁷ : TopologicalSpace A<VAR>inst✝⁶ : TopologicalSpace B<VAR>inst✝⁵ : TopologicalSpace C<VAR>inst✝⁴ : TopologicalSpace D<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : TopologicalGroup E<VAR>inst✝¹ : ContinuousMul B<VAR>inst✝ : T2Space B<VAR>x y : A<GOAL>IsClosed {x_1 | x_1 (x * y) = x_1 x * x_1 y}
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F✝ G✝ : C ⥤ D<VAR>X Y : C<VAR>F G : C ⥤ D<VAR>H I : D ⥤ E<VAR>α : F ≅ G<VAR>β : H ≅ I<VAR>x✝ : C<GOAL>((α.inv ◫ β.inv) ≫ α.hom ◫ β.hom).app x✝ = (𝟙 (G ⋙ I)).app x✝