ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹¹ : Group G<VAR>inst✝¹⁰ : Group H<VAR>inst✝⁹ : MulAction G α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : MulAction H β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>s t✝ : Set α<VAR>μ : Measure α<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : MeasurableSMul G α<VAR>inst✝² : SMulInvariantMeasure G α μ<VAR>inst✝¹ : Countable G<VAR>ν : Measure α<VAR>inst✝ : Finite G<VAR>h : IsFundamentalDomain G s μ<VAR>t : Set α<VAR>this : Fintype G<VAR>ht : ∀ (g : G), g • t ∩ s =ᶠ[ae μ] t ∩ s<GOAL>∑' (g : G), μ (g • t ∩ s) = Nat.card G • μ (t ∩ s)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>b c d : R<VAR>n : ℤ<GOAL>f (preNormEDS b c d n) = preNormEDS (f b) (f c) (f d) n
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>A : Matrix (Fin 2) (Fin 2) R<GOAL>A.det = A 0 0 * A 1 1 - A 0 1 * A 1 0
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>A : Matrix (Fin 2) (Fin 2) R<GOAL>(-1) ^ 0 * A 0 0 * A 1 1 + (-1) ^ (0 + 1) * A 0 1 * A 1 0 = A 0 0 * A 1 1 - A 0 1 * A 1 0
<VAR>m✝ n a b c d m : ℤ<VAR>h : a ≡ b [ZMOD m * n]<GOAL>a ≡ b [ZMOD n]
<VAR>m✝ n a b c d m : ℤ<VAR>h : m * n ∣ b - a<GOAL>n ∣ b - a
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x✝ y✝ f' : ℝ<VAR>hfc : ConcaveOn ℝ S f<VAR>hfd : DifferentiableOn ℝ f S<VAR>x : ℝ<VAR>hx : x ∈ S<VAR>y : ℝ<VAR>hy : y ∈ S<VAR>hxy : x ≤ y<GOAL>derivWithin f S y ≤ derivWithin f S x
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x✝ y f' : ℝ<VAR>hfc : ConcaveOn ℝ S f<VAR>hfd : DifferentiableOn ℝ f S<VAR>x : ℝ<VAR>hx hy : x ∈ S<VAR>hxy : x ≤ x<GOAL>derivWithin f S x ≤ derivWithin f S x
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x✝ y✝ f' : ℝ<VAR>hfc : ConcaveOn ℝ S f<VAR>hfd : DifferentiableOn ℝ f S<VAR>x : ℝ<VAR>hx : x ∈ S<VAR>y : ℝ<VAR>hy : y ∈ S<VAR>hxy : x ≤ y<VAR>hxy' : x < y<GOAL>derivWithin f S y ≤ derivWithin f S x
<VAR>z✝ w✝ : ℍ<VAR>r R : ℝ<VAR>z w : ℍ<GOAL>tanh (dist z w / 2) = dist ↑z ↑w / dist (↑z) ((starRingEnd ℂ) ↑w)
<VAR>z✝ w✝ : ℍ<VAR>r R : ℝ<VAR>z w : ℍ<GOAL>2 * √(z.im * w.im) ≠ 0
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)<VAR>a b : Ordinal.{max v u}<VAR>hb : b < o.nfpBFamily f a<VAR>i : Ordinal.{u}<VAR>hi : i < o<GOAL>f i hi b < o.nfpBFamily f a
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)<VAR>a b : Ordinal.{max v u}<VAR>hb : b < o.nfpBFamily f a<VAR>i : Ordinal.{u}<VAR>hi : i < o<GOAL>o.familyOfBFamily f (enum (fun x x_1 => x < x_1) i ⋯) b < o.nfpBFamily f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Multiset α<VAR>h : s.Disjoint t<GOAL>(s + t).dedup = s.dedup + t.dedup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>a✝ b✝ : List α<VAR>h : Disjoint (Quot.mk Setoid.r a✝) (Quot.mk Setoid.r b✝)<GOAL>(Quot.mk Setoid.r a✝ + Quot.mk Setoid.r b✝).dedup = dedup (Quot.mk Setoid.r a✝) + dedup (Quot.mk Setoid.r b✝)
<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>φ : K →+* ℂ<GOAL>mk (ComplexEmbedding.conjugate φ) = mk φ
<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>φ : K →+* ℂ<VAR>x : K<GOAL>(mk (ComplexEmbedding.conjugate φ)) x = (mk φ) x
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>x y : α<VAR>h : Commute x y<VAR>n : ℕ<GOAL>(y - x) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = y ^ n - x ^ n
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>x y : α<VAR>h : Commute x y<VAR>n : ℕ<GOAL>MulOpposite.op ((y - x) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) = MulOpposite.op (y ^ n - x ^ n)
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>x y : α<VAR>h : Commute x y<VAR>n : ℕ<GOAL>MulOpposite.op (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (MulOpposite.op y - MulOpposite.op x) = MulOpposite.op y ^ n - MulOpposite.op x ^ n
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Semiring A<VAR>inst✝⁷ : Semiring B<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : Algebra S B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : IsScalarTower R S A<VAR>inst✝ : IsScalarTower R S B<VAR>x : R<GOAL>(algebraMap R A) x = ((algebraMap S A).comp (algebraMap R S)) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝ : Field K<VAR>a b c : K<VAR>hc : c ≠ 0<GOAL>a / c - b = (a - c * b) / c
<VAR>x : ℝ<VAR>hx : 0 ≤ x<VAR>y : ℝ<GOAL>↑(x ^ y) = ↑x ^ ↑y
<VAR>x : ℝ<VAR>hx : 0 ≤ x<VAR>y : ℝ<GOAL>↑(if x = 0 then if y = 0 then 1 else 0 else rexp (Real.log x * y)) = if x = 0 then if y = 0 then 1 else 0 else cexp (log ↑x * ↑y)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i : B<GOAL>cs.length (cs.simple i) = 1
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i : B<GOAL>cs.length (cs.simple i) ≤ 1
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i : B<GOAL>1 ≤ cs.length (cs.simple i)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup V<VAR>inst✝⁶ : InnerProductSpace ℝ V<VAR>inst✝⁵ : MetricSpace P<VAR>inst✝⁴ : NormedAddTorsor V P<VAR>s₁ s₂ : AffineSubspace ℝ P<VAR>inst✝³ : Nonempty ↥s₁<VAR>inst✝² : Nonempty ↥s₂<VAR>inst✝¹ : HasOrthogonalProjection s₁.direction<VAR>inst✝ : HasOrthogonalProjection s₂.direction<VAR>p : P<GOAL>(reflection s₁) p = (reflection s₂) p ↔ ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) p)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup V<VAR>inst✝⁶ : InnerProductSpace ℝ V<VAR>inst✝⁵ : MetricSpace P<VAR>inst✝⁴ : NormedAddTorsor V P<VAR>s₁ s₂ : AffineSubspace ℝ P<VAR>inst✝³ : Nonempty ↥s₁<VAR>inst✝² : Nonempty ↥s₂<VAR>inst✝¹ : HasOrthogonalProjection s₁.direction<VAR>inst✝ : HasOrthogonalProjection s₂.direction<VAR>p : P<GOAL>↑((orthogonalProjection s₁) p) -ᵥ p +ᵥ ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) p) -ᵥ p +ᵥ ↑((orthogonalProjection s₂) p) ↔ ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) p)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>P : Ideal R<VAR>hP : P.IsPrime<VAR>q : R[X]<VAR>c : (R ⧸ P)[X]<VAR>hq : map (mk P) q = c * X ^ n<VAR>hc0 : c.degree = 0<GOAL>↑n = (map (mk P) q).degree
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommRing R<VAR>p✝ q✝ : MvPolynomial σ R<VAR>inst✝ : DecidableEq σ<VAR>p q : MvPolynomial σ R<GOAL>(p - q).degrees ≤ p.degrees ⊔ q.degrees
<VAR>α : Type u_1<VAR>inst✝ : PartialOrder α<VAR>s : UpperSet α<VAR>a : α<GOAL>InfIrred (Ici a)
<VAR>α : Type u_1<VAR>inst✝ : PartialOrder α<VAR>s✝ : UpperSet α<VAR>a : α<VAR>s t : UpperSet α<VAR>hst : s ⊓ t = Ici a<GOAL>s = Ici a ∨ t = Ici a
<VAR>α : Type u_1<VAR>inst✝ : PartialOrder α<VAR>s✝ : UpperSet α<VAR>a : α<VAR>s t : UpperSet α<VAR>hst : s ⊓ t = Ici a<VAR>this : a ∈ Ici a<GOAL>s = Ici a ∨ t = Ici a
<VAR>α : Type u_1<VAR>inst✝ : PartialOrder α<VAR>s✝ : UpperSet α<VAR>a : α<VAR>s t : UpperSet α<VAR>hst : s ⊓ t = Ici a<VAR>this : a ∈ s ⊓ t<GOAL>s = Ici a ∨ t = Ici a
<VAR>x y : ZFSet<VAR>h : ↑x = ↑y<VAR>z : ZFSet<GOAL>↑x z ↔ ↑y z
<VAR>R : Type u_1<VAR>F : Type u<VAR>inst✝ : Field F<VAR>p q : F[X]<VAR>f✝ g : RatFunc F<VAR>f : F[X]<VAR>hf : f ≠ 0<GOAL>↑f ≠ 0
<VAR>J : Type u<VAR>inst✝ : Category.{v, u} J<VAR>F G : J ⥤ Type w<VAR>φ : F ⟶ G<VAR>x : (fun F => ↑F.sections) F<VAR>j j' : J<VAR>f : j ⟶ j'<GOAL>(F.map f ≫ φ.app j') (↑x j) = (fun j => φ.app j (↑x j)) j'
<VAR>y : ℝ<VAR>hy : 0 < y<GOAL>∀ (b : ℝ≥0), ∃ i, ∀ (a : ℝ≥0), i ≤ a → b ≤ a ^ y
<VAR>y : ℝ<VAR>hy : 0 < y<VAR>b : ℝ≥0<GOAL>∃ i, ∀ (a : ℝ≥0), i ≤ a → b ≤ a ^ y
<VAR>y : ℝ<VAR>hy : 0 < y<VAR>b : ℝ≥0<VAR>c : ℝ<VAR>hc : ∀ (a : ℝ), c ≤ a → ↑b ≤ a ^ y<GOAL>∃ i, ∀ (a : ℝ≥0), i ≤ a → b ≤ a ^ y
<VAR>y : ℝ<VAR>hy : 0 < y<VAR>b : ℝ≥0<VAR>c : ℝ<VAR>hc : ∀ (a : ℝ), c ≤ a → ↑b ≤ a ^ y<GOAL>∀ (a : ℝ≥0), c.toNNReal ≤ a → b ≤ a ^ y
<VAR>y : ℝ<VAR>hy : 0 < y<VAR>b : ℝ≥0<VAR>c : ℝ<VAR>hc : ∀ (a : ℝ), c ≤ a → ↑b ≤ a ^ y<VAR>a : ℝ≥0<VAR>ha : c.toNNReal ≤ a<GOAL>b ≤ a ^ y
<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✝⁷ : Field K<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : Module K V<VAR>inst✝⁴ : Field K₁<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K₁ V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>J : K →+* K<VAR>J₁ J₁' : K₁ →+* K<VAR>B : V →ₗ[K] V →ₗ[K] K<VAR>x : V<VAR>hx : ¬B.IsOrtho x x<GOAL>Submodule.span K {x} ⊔ (Submodule.span K {x}).orthogonalBilin B = ⊤
<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✝⁷ : Field K<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : Module K V<VAR>inst✝⁴ : Field K₁<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K₁ V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>J : K →+* K<VAR>J₁ J₁' : K₁ →+* K<VAR>B : V →ₗ[K] V →ₗ[K] K<VAR>x : V<VAR>hx : ¬B.IsOrtho x x<GOAL>Submodule.span K {x} ⊔ ker (B x) = ⊤
<VAR>ι : Sort u_1<VAR>α✝ : Type u_2<VAR>inst✝¹ : CompleteLattice α✝<VAR>f : ι → α✝<VAR>α : Type u_3<VAR>inst✝ : CompleteLattice α<VAR>k : α<VAR>hk : IsCompactElement k<VAR>s : Set α<VAR>hemp : s.Nonempty<VAR>hdir : DirectedOn (fun x x_1 => x ≤ x_1) s<VAR>hbelow : ∀ x ∈ s, x < k<GOAL>sSup s < k
<VAR>ι : Sort u_1<VAR>α✝ : Type u_2<VAR>inst✝¹ : CompleteLattice α✝<VAR>f : ι → α✝<VAR>α : Type u_3<VAR>inst✝ : CompleteLattice α<VAR>k : α<VAR>hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x<VAR>s : Set α<VAR>hemp : s.Nonempty<VAR>hdir : DirectedOn (fun x x_1 => x ≤ x_1) s<VAR>hbelow : ∀ x ∈ s, x < k<GOAL>sSup s < k
<VAR>ι : Sort u_1<VAR>α✝ : Type u_2<VAR>inst✝¹ : CompleteLattice α✝<VAR>f : ι → α✝<VAR>α : Type u_3<VAR>inst✝ : CompleteLattice α<VAR>k : α<VAR>hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x<VAR>s : Set α<VAR>hemp : s.Nonempty<VAR>hdir : DirectedOn (fun x x_1 => x ≤ x_1) s<VAR>hbelow : ∀ x ∈ s, x < k<VAR>h : ¬sSup s < k<GOAL>False
<VAR>ι : Sort u_1<VAR>α✝ : Type u_2<VAR>inst✝¹ : CompleteLattice α✝<VAR>f : ι → α✝<VAR>α : Type u_3<VAR>inst✝ : CompleteLattice α<VAR>k : α<VAR>hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x<VAR>s : Set α<VAR>hemp : s.Nonempty<VAR>hdir : DirectedOn (fun x x_1 => x ≤ x_1) s<VAR>hbelow : ∀ x ∈ s, x < k<VAR>h : ¬sSup s < k<VAR>sSup' : sSup s ≤ k<GOAL>False
<VAR>ι : Sort u_1<VAR>α✝ : Type u_2<VAR>inst✝¹ : CompleteLattice α✝<VAR>f : ι → α✝<VAR>α : Type u_3<VAR>inst✝ : CompleteLattice α<VAR>k : α<VAR>hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ SupSet.sSup s → ∃ x ∈ s, k ≤ x<VAR>s : Set α<VAR>hemp : s.Nonempty<VAR>hdir : DirectedOn (fun x x_1 => x ≤ x_1) s<VAR>hbelow : ∀ x ∈ s, x < k<VAR>h : ¬SupSet.sSup s < k<VAR>sSup' : SupSet.sSup s ≤ k<VAR>sSup : SupSet.sSup s = k<GOAL>False
<VAR>ι : Sort u_1<VAR>α✝ : Type u_2<VAR>inst✝¹ : CompleteLattice α✝<VAR>f : ι → α✝<VAR>α : Type u_3<VAR>inst✝ : CompleteLattice α<VAR>k : α<VAR>hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ SupSet.sSup s → ∃ x ∈ s, k ≤ x<VAR>s : Set α<VAR>hemp : s.Nonempty<VAR>hdir : DirectedOn (fun x x_1 => x ≤ x_1) s<VAR>hbelow : ∀ x ∈ s, x < k<VAR>h : ¬SupSet.sSup s < k<VAR>sSup' : SupSet.sSup s ≤ k<VAR>sSup : SupSet.sSup s = k<VAR>x : α<VAR>hxs : x ∈ s<VAR>hkx : k ≤ x<GOAL>False
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>inst✝⁷ : Category.{?u.13901, u_1} C<VAR>inst✝⁶ : Category.{?u.13905, u_2} D<VAR>inst✝⁵ : Category.{?u.13909, u_3} E<VAR>inst✝⁴ : Category.{?u.13913, u_4} E'<VAR>A : Type u_5<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : HasShift D A<VAR>inst✝¹ : HasShift E A<VAR>inst✝ : HasShift E' A<VAR>F G H : SingleFunctors C D A<VAR>n m mn : A<VAR>hnm : m + n = mn<VAR>a a' a'' : A<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<GOAL>mn + a = a''
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>inst✝⁷ : Category.{u_7, u_1} C<VAR>inst✝⁶ : Category.{u_6, u_2} D<VAR>inst✝⁵ : Category.{?u.13909, u_3} E<VAR>inst✝⁴ : Category.{?u.13913, u_4} E'<VAR>A : Type u_5<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : HasShift D A<VAR>inst✝¹ : HasShift E A<VAR>inst✝ : HasShift E' A<VAR>F G H : SingleFunctors C D A<VAR>n m a a' a'' : A<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<GOAL>F.shiftIso (m + n) a a'' ⋯ = isoWhiskerLeft (F.functor a'') (shiftFunctorAdd' D m n (m + n) ⋯) ≪≫ ((F.functor a'').associator (shiftFunctor D m) (shiftFunctor D n)).symm ≪≫ isoWhiskerRight (F.shiftIso m a' a'' ha'') (shiftFunctor D n) ≪≫ F.shiftIso n a a' ha'
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<GOAL>∀ᶠ (y : E) in 𝓝 x, HasSum (fun n => (p n) fun x_1 => y - x) (f y)
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F : OplaxFunctor B C<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<GOAL>F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h = F.map₂ (α_ f g h).inv ≫ F.mapComp (f ≫ g) h ≫ F.mapComp f g ▷ F.map h ≫ (α_ (F.map f) (F.map g) (F.map h)).hom
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F : OplaxFunctor B C<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<GOAL>F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h = F.map₂ ((α_ f g h).inv ≫ (α_ f g h).hom) ≫ F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h
<VAR>m n k : ℕ<GOAL>↑m >>> (↑n + ↑k) = ↑m >>> ↑n >>> ↑k
<VAR>m n k : ℕ<GOAL>-[m+1] >>> (↑n + ↑k) = -[m+1] >>> ↑n >>> ↑k
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>p : α → Bool<VAR>l : List α<VAR>x : α<VAR>h : p x = true<GOAL>takeWhile p (x :: l) = x :: takeWhile p l
<VAR>u : ℕ → ℝ<VAR>h : Subadditive u<VAR>L : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hL : u n / ↑n < L<GOAL>∀ᶠ (p : ℕ) in atTop, u p / ↑p < L
<VAR>u : ℕ → ℝ<VAR>h : Subadditive u<VAR>L : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hL : u n / ↑n < L<VAR>r : ℕ<VAR>x✝ : r < n<GOAL>∀ᶠ (a : ℕ) in atTop, u (n * a + r) / ↑(n * a + r) < L
<VAR>u : ℕ → ℝ<VAR>h : Subadditive u<VAR>L : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hL : u n / ↑n < L<VAR>r : ℕ<VAR>x✝ : r < n<VAR>A : Tendsto (fun x => (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 ((u n + 0) / (↑n + 0)))<GOAL>∀ᶠ (a : ℕ) in atTop, u (n * a + r) / ↑(n * a + r) < L
<VAR>u : ℕ → ℝ<VAR>h : Subadditive u<VAR>L : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hL : u n / ↑n < L<VAR>r : ℕ<VAR>x✝ : r < n<VAR>A : Tendsto (fun x => (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 ((u n + 0) / (↑n + 0)))<VAR>B : Tendsto (fun x => (x * u n + u r) / (x * ↑n + ↑r)) atTop (𝓝 (u n / ↑n))<GOAL>∀ᶠ (a : ℕ) in atTop, u (n * a + r) / ↑(n * a + r) < L
<VAR>u : ℕ → ℝ<VAR>h : Subadditive u<VAR>L : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hL : u n / ↑n < L<VAR>r : ℕ<VAR>x✝ : r < n<VAR>A : Tendsto (fun x => (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 ((u n + 0) / (↑n + 0)))<VAR>B : Tendsto (fun x => (x * u n + u r) / (x * ↑n + ↑r)) atTop (𝓝 (u n / ↑n))<VAR>k : ℕ<VAR>hk : ((fun x => (x * u n + u r) / (x * ↑n + ↑r)) ∘ Nat.cast) k < L<GOAL>u (n * k + r) / ↑(n * k + r) < L
<VAR>u : ℕ → ℝ<VAR>h : Subadditive u<VAR>L : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hL : u n / ↑n < L<VAR>r : ℕ<VAR>x✝ : r < n<VAR>A : Tendsto (fun x => (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 ((u n + 0) / (↑n + 0)))<VAR>B : Tendsto (fun x => (x * u n + u r) / (x * ↑n + ↑r)) atTop (𝓝 (u n / ↑n))<VAR>k : ℕ<VAR>hk : ((fun x => (x * u n + u r) / (x * ↑n + ↑r)) ∘ Nat.cast) k < L<GOAL>u (k * n + r) / ↑(k * n + r) < L
<VAR>u : ℕ → ℝ<VAR>h : Subadditive u<VAR>L : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hL : u n / ↑n < L<VAR>r : ℕ<VAR>x✝ : r < n<VAR>A : Tendsto (fun x => (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 ((u n + 0) / (↑n + 0)))<VAR>B : Tendsto (fun x => (x * u n + u r) / (x * ↑n + ↑r)) atTop (𝓝 (u n / ↑n))<VAR>k : ℕ<VAR>hk : ((fun x => (x * u n + u r) / (x * ↑n + ↑r)) ∘ Nat.cast) k < L<GOAL>u (k * n + r) / ↑(k * n + r) ≤ ((fun x => (x * u n + u r) / (x * ↑n + ↑r)) ∘ Nat.cast) k
<VAR>u : ℕ → ℝ<VAR>h : Subadditive u<VAR>L : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hL : u n / ↑n < L<VAR>r : ℕ<VAR>x✝ : r < n<VAR>A : Tendsto (fun x => (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 ((u n + 0) / (↑n + 0)))<VAR>B : Tendsto (fun x => (x * u n + u r) / (x * ↑n + ↑r)) atTop (𝓝 (u n / ↑n))<VAR>k : ℕ<VAR>hk : ((fun x => (x * u n + u r) / (x * ↑n + ↑r)) ∘ Nat.cast) k < L<GOAL>u (k * n + r) / ↑(k * n + r) ≤ (↑k * u n + u r) / ↑(k * n + r)
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>y : ι → ℝ<GOAL>I.splitUpper i x = ↑I ↔ x ≤ I.lower i
<VAR>a b : Rat<VAR>g ad bd : Nat<VAR>hg : g = a.den.gcd b.den<VAR>had : ad = a.den / g<VAR>hbd : bd = b.den / g<GOAL>let den := ad * b.den; let num := a.num * ↑bd - b.num * ↑ad; num.natAbs.gcd g = num.natAbs.gcd den
<VAR>a b : Rat<VAR>g ad bd : Nat<VAR>hg : g = a.den.gcd b.den<VAR>had : ad = a.den / g<VAR>hbd : bd = b.den / g<VAR>this : let den := ad * (-b).den; let num := a.num * ↑bd + (-b).num * ↑ad; num.natAbs.gcd g = num.natAbs.gcd den<GOAL>let den := ad * b.den; let num := a.num * ↑bd - b.num * ↑ad; num.natAbs.gcd g = num.natAbs.gcd den
<VAR>a b : Rat<VAR>g ad bd : Nat<VAR>hg : g = a.den.gcd b.den<VAR>had : ad = a.den / g<VAR>hbd : bd = b.den / g<VAR>this : (a.num * ↑bd + -(b.num * ↑ad)).natAbs.gcd g = (a.num * ↑bd + -(b.num * ↑ad)).natAbs.gcd (ad * (-b).den)<GOAL>let den := ad * b.den; let num := a.num * ↑bd - b.num * ↑ad; num.natAbs.gcd g = num.natAbs.gcd den
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>hf : Function.Injective ⇑f<VAR>x : R<VAR>h : x ∈ Module.annihilator R M'<GOAL>x ∈ Module.annihilator R M
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>hf : Function.Injective ⇑f<VAR>x : R<VAR>h : ∀ (m : M'), x • m = 0<GOAL>∀ (m : M), x • m = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderTopology β<VAR>inst✝ : DenselyOrdered β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : MonotoneOn f s<VAR>hs : s ∈ 𝓝[≥] a<VAR>hfs : closure (f '' s) ∈ 𝓝[≥] f a<GOAL>ContinuousWithinAt f (Ici a) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderTopology β<VAR>inst✝ : DenselyOrdered β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : MonotoneOn f s<VAR>hs : s ∈ 𝓝[≥] a<VAR>hfs : closure (f '' s) ∈ 𝓝[≥] f a<VAR>b : β<VAR>hb : b > f a<GOAL>∃ c ∈ s, f c ∈ Ioo (f a) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderTopology β<VAR>inst✝ : DenselyOrdered β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : MonotoneOn f s<VAR>hs : s ∈ 𝓝[≥] a<VAR>hfs : closure (f '' s) ∈ 𝓝[≥] f a<VAR>b : β<VAR>hb : b > f a<VAR>b' : β<VAR>hb' : Ico (f a) b' ⊆ closure (f '' s)<VAR>hab' : f a < b'<VAR>hbb' : b' ≤ b<GOAL>∃ c ∈ s, f c ∈ Ioo (f a) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderTopology β<VAR>inst✝ : DenselyOrdered β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : MonotoneOn f s<VAR>hs : s ∈ 𝓝[≥] a<VAR>hfs : closure (f '' s) ∈ 𝓝[≥] f a<VAR>b : β<VAR>hb : b > f a<VAR>b' : β<VAR>hb' : Ico (f a) b' ⊆ closure (f '' s)<VAR>hab' : f a < b'<VAR>hbb' : b' ≤ b<VAR>c' : β<VAR>hc' : f a < c' ∧ c' < b'<GOAL>∃ c ∈ s, f c ∈ Ioo (f a) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderTopology β<VAR>inst✝ : DenselyOrdered β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : MonotoneOn f s<VAR>hs : s ∈ 𝓝[≥] a<VAR>hfs : closure (f '' s) ∈ 𝓝[≥] f a<VAR>b : β<VAR>hb : b > f a<VAR>b' : β<VAR>hb' : Ico (f a) b' ⊆ closure (f '' s)<VAR>hab' : f a < b'<VAR>hbb' : b' ≤ b<VAR>c' : β<VAR>hc' : f a < c' ∧ c' < b'<VAR>c : α<VAR>hcs : c ∈ s<VAR>hc : f c ∈ Ioo (f a) b'<GOAL>∃ c ∈ s, f c ∈ Ioo (f a) b
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁷ : SeminormedAddCommGroup E<VAR>inst✝¹⁶ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁵ : SeminormedAddCommGroup F<VAR>inst✝¹⁴ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹³ : SeminormedAddCommGroup G<VAR>inst✝¹² : SeminormedAddCommGroup Gₗ<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁹ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁶ : NormedSpace 𝕜₂ F<VAR>inst✝⁵ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁴ : NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝² : FunLike 𝓕 E F<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>inst✝ : Subsingleton E<GOAL>‖f‖ = 0
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁷ : SeminormedAddCommGroup E<VAR>inst✝¹⁶ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁵ : SeminormedAddCommGroup F<VAR>inst✝¹⁴ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹³ : SeminormedAddCommGroup G<VAR>inst✝¹² : SeminormedAddCommGroup Gₗ<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁹ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁶ : NormedSpace 𝕜₂ F<VAR>inst✝⁵ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁴ : NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝² : FunLike 𝓕 E F<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>inst✝ : Subsingleton E<GOAL>‖f‖ ≤ 0