ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_2<VAR>inst✝⁵ : Category.{u_1, u_2} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>S₁ S₂ S₃ S₄ : ShortComplex C<VAR>inst✝³ : S₁.HasHomology<VAR>inst✝² : S₂.HasHomology<VAR>inst✝¹ : S₃.HasHomology<VAR>inst✝ : S₄.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>φ' : S₂ ⟶ S₃<VAR>hφ' : IsIso (homologyMap φ')<VAR>hφφ' : IsIso (homologyMap φ ≫ homologyMap φ')<GOAL>IsIso (homologyMap φ)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<GOAL>¬MonotoneOn f s ∧ ¬AntitoneOn f s ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
<VAR>ι : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>hom : Type u_4<VAR>inst✝⁷ : UniformSpace G<VAR>inst✝⁶ : UniformSpace M<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group M<VAR>inst✝³ : UniformGroup G<VAR>inst✝² : UniformGroup M<VAR>inst✝¹ : FunLike hom G M<VAR>inst✝ : MonoidHomClass hom G M<VAR>F : ι → hom<VAR>hf : EquicontinuousAt (DFunLike.coe ∘ F) 1<GOAL>UniformEquicontinuous (DFunLike.coe ∘ F)
<VAR>ι : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>hom : Type u_4<VAR>inst✝⁷ : UniformSpace G<VAR>inst✝⁶ : UniformSpace M<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group M<VAR>inst✝³ : UniformGroup G<VAR>inst✝² : UniformGroup M<VAR>inst✝¹ : FunLike hom G M<VAR>inst✝ : MonoidHomClass hom G M<VAR>F : ι → hom<VAR>hf : EquicontinuousAt (DFunLike.coe ∘ F) 1<GOAL>UniformContinuous (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F))
<VAR>ι : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>hom : Type u_4<VAR>inst✝⁷ : UniformSpace G<VAR>inst✝⁶ : UniformSpace M<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group M<VAR>inst✝³ : UniformGroup G<VAR>inst✝² : UniformGroup M<VAR>inst✝¹ : FunLike hom G M<VAR>inst✝ : MonoidHomClass hom G M<VAR>F : ι → hom<VAR>hf : ContinuousAt (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F)) 1<GOAL>UniformContinuous (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F))
<VAR>ι : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>hom : Type u_4<VAR>inst✝⁷ : UniformSpace G<VAR>inst✝⁶ : UniformSpace M<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group M<VAR>inst✝³ : UniformGroup G<VAR>inst✝² : UniformGroup M<VAR>inst✝¹ : FunLike hom G M<VAR>inst✝ : MonoidHomClass hom G M<VAR>F : ι → hom<VAR>hf : ContinuousAt (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F)) 1<VAR>φ : G →* ι →ᵤ M := { toFun := swap (DFunLike.coe ∘ F), map_one' := ⋯, map_mul' := ⋯ }<GOAL>UniformContinuous (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F))
<VAR>E : Type u_1<VAR>inst✝ : MeasurableSpace E<VAR>m μ : Measure E<VAR>Ω : Type u_2<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>X : Ω → E<VAR>s : Set E<VAR>hns : μ s ≠ 0<VAR>hnt : μ s ≠ ⊤<VAR>hu : IsUniform X s ℙ μ<GOAL>ℙ Set.univ = 1
<VAR>E : Type u_1<VAR>inst✝ : MeasurableSpace E<VAR>m μ : Measure E<VAR>Ω : Type u_2<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>X : Ω → E<VAR>s : Set E<VAR>hns : μ s ≠ 0<VAR>hnt : μ s ≠ ⊤<VAR>hu : IsUniform X s ℙ μ<VAR>this : X ⁻¹' Set.univ = Set.univ<GOAL>ℙ Set.univ = 1
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>D : Derivation R S M<VAR>a : S<GOAL>(D.liftKaehlerDifferential.compDer (KaehlerDifferential.D R S)) a = D a
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>D : Derivation R S M<VAR>a : S<GOAL>D.liftKaehlerDifferential ((KaehlerDifferential.ideal R S).toCotangent ⟨1 ⊗ₜ[R] a - a ⊗ₜ[R] 1, ⋯⟩) = D a
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>D : Derivation R S M<VAR>a : S<GOAL>D.tensorProductTo ↑⟨1 ⊗ₜ[R] a - a ⊗ₜ[R] 1, ⋯⟩ = D a
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝² : Semiring α<VAR>inst✝¹ : LinearOrder α<VAR>a b c d : α<VAR>inst✝ : PosMulStrictMono α<VAR>h : 0 < c<GOAL>0 ≤ c * b ↔ 0 ≤ b
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝² : Semiring α<VAR>inst✝¹ : LinearOrder α<VAR>a b c d : α<VAR>inst✝ : PosMulStrictMono α<VAR>h : 0 < c<GOAL>0 = c * 0
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : AddCommMonoid B<VAR>inst✝² : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s✝ : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝¹ : Zero M<VAR>inst✝ : CommMonoid N<VAR>s : Finset α<VAR>f : (a : α) → a ∈ s → M<VAR>h : α → M → N<VAR>h_zero : ∀ a ∈ s, h a 0 = 1<GOAL>(indicator s f).prod h = ∏ x ∈ s.attach, h (↑x) (f ↑x ⋯)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : AddCommMonoid B<VAR>inst✝² : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s✝ : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝¹ : Zero M<VAR>inst✝ : CommMonoid N<VAR>s : Finset α<VAR>f : (a : α) → a ∈ s → M<VAR>h : α → M → N<VAR>h_zero : ∀ a ∈ s, h a 0 = 1<GOAL>∏ x ∈ s.attach, h (↑x) ((indicator s f) ↑x) = ∏ x ∈ s.attach, h (↑x) (f ↑x ⋯)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : AddCommMonoid B<VAR>inst✝² : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s✝ : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝¹ : Zero M<VAR>inst✝ : CommMonoid N<VAR>s : Finset α<VAR>f : (a : α) → a ∈ s → M<VAR>h : α → M → N<VAR>h_zero : ∀ a ∈ s, h a 0 = 1<VAR>x✝¹ : { x // x ∈ s }<VAR>x✝ : x✝¹ ∈ s.attach<GOAL>h (↑x✝¹) ((indicator s f) ↑x✝¹) = h (↑x✝¹) (f ↑x✝¹ ⋯)
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>u v : V<VAR>huv : G.Adj u v<GOAL>(⊤.induce {u, v}).Connected
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>u v : V<VAR>huv : G.Adj u v<GOAL>(G.subgraphOfAdj huv).Connected
<VAR>α : Type u<VAR>inst✝ : LinearOrderedField α<VAR>x : α<VAR>hx : 0 ≤ x<VAR>h'x : x < 1<VAR>m n : ℕ<GOAL>∑ i ∈ Ico m n, x ^ i ≤ x ^ m / (1 - x)
<VAR>α : Type u<VAR>inst✝ : LinearOrderedField α<VAR>x : α<VAR>hx : 0 ≤ x<VAR>h'x : x < 1<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>∑ i ∈ Ico m n, x ^ i ≤ x ^ m / (1 - x)
<VAR>α : Type u<VAR>inst✝ : LinearOrderedField α<VAR>x : α<VAR>hx : 0 ≤ x<VAR>h'x : x < 1<VAR>m n : ℕ<VAR>hmn : n < m<GOAL>∑ i ∈ Ico m n, x ^ i ≤ x ^ m / (1 - x)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x y : 𝕎 R<GOAL>truncateFun n (x + y) = truncateFun n x + truncateFun n y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : SigmaCompactSpace X<VAR>K : CompactExhaustion X<VAR>x : X<GOAL>¬K.shiftr.find x ≤ K.find x
<VAR>α β ι : Type u<VAR>hι : Nonempty ι<VAR>f : ι → Cardinal.{v}<VAR>hf : BddAbove (range f)<VAR>ω : Cardinal.{v}<VAR>hω : ¬ω.IsLimit<VAR>h : ⨆ i, f i = ω<VAR>e : ¬ω ≠ 0<GOAL>f hι.some = ω
<VAR>α β ι : Type u<VAR>hι : Nonempty ι<VAR>f : ι → Cardinal.{v}<VAR>hf : BddAbove (range f)<VAR>hω : ¬IsLimit 0<VAR>h : ⨆ i, f i = 0<VAR>e : ¬0 ≠ 0<GOAL>f hι.some = 0
<VAR>α β ι : Type u<VAR>hι : Nonempty ι<VAR>f : ι → Cardinal.{v}<VAR>hf : BddAbove (range f)<VAR>hω : ¬IsLimit 0<VAR>h : ⨆ i, f i ≤ 0<VAR>e : ¬0 ≠ 0<GOAL>f hι.some ≤ 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{?u.16591, u_2} D<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>inst✝² : S.HasHomology<VAR>inst✝¹ : HasKernel S.g<VAR>inst✝ : HasCokernel S.f<GOAL>S.Exact ↔ kernel.ι S.g ≫ cokernel.π S.f = 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{?u.16591, u_2} D<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>inst✝² : S.HasHomology<VAR>inst✝¹ : HasKernel S.g<VAR>inst✝ : HasCokernel S.f<VAR>this : HasCokernel (kernel.lift S.g S.f ⋯)<GOAL>S.Exact ↔ kernel.ι S.g ≫ cokernel.π S.f = 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{?u.16591, u_2} D<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>inst✝² : S.HasHomology<VAR>inst✝¹ : HasKernel S.g<VAR>inst✝ : HasCokernel S.f<VAR>this✝ : HasCokernel (kernel.lift S.g S.f ⋯)<VAR>this : HasKernel (cokernel.desc S.f S.g ⋯)<GOAL>S.Exact ↔ kernel.ι S.g ≫ cokernel.π S.f = 0
<VAR>a : ℤ<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<GOAL>J(a | p) = -1 ↔ ¬IsSquare ↑a
<VAR>a : ℤ<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<GOAL>legendreSym p a = -1 ↔ ¬IsSquare ↑a
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℤ<VAR>a : R<VAR>a0 : a ≠ 0<GOAL>(C a * T n).support.max = ↑n
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℤ<VAR>a : R<VAR>a0 : a ≠ 0<VAR>this : (C a * T n).support = {n}<GOAL>(C a * T n).support.max = ↑n
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℤ<VAR>a : R<VAR>a0 : a ≠ 0<VAR>this : (C a * T n).support = {n}<GOAL>{n}.max = ↑n
<VAR>Γ : Type u_1<VAR>inst✝³ : Inhabited Γ<VAR>Γ' : Type u_2<VAR>inst✝² : Inhabited Γ'<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>Λ' : Type u_4<VAR>inst✝ : Inhabited Λ'<VAR>M : Machine Γ Λ<VAR>f₁ : PointedMap Γ Γ'<VAR>f₂ : PointedMap Γ' Γ<VAR>g₁ : Λ → Λ'<VAR>g₂ : Λ' → Λ<VAR>S : Set Λ<VAR>f₂₁ : Function.RightInverse f₁.f f₂.f<VAR>g₂₁ : ∀ q ∈ S, g₂ (g₁ q) = q<VAR>q : Λ<VAR>T : Tape Γ<VAR>h : { q := q, Tape := T }.q ∈ S<GOAL>Option.map (fun x => match x with | { q := q, Tape := T } => { q := g₁ q, Tape := Tape.map f₁ T }) (match { q := q, Tape := T } with | { q := q, Tape := T } => Option.map (fun x => match x with | (q', a) => { q := q', Tape := match a with | Stmt.move d => Tape.move d T | Stmt.write a => Tape.write a T }) (M q T.head)) = match match { q := q, Tape := T } with | { q := q, Tape := T } => { q := g₁ q, Tape := Tape.map f₁ T } with | { q := q, Tape := T } => Option.map (fun x => match x with | (q', a) => { q := q', Tape := match a with | Stmt.move d => Tape.move d T | Stmt.write a => Tape.write a T }) (match q, T.head with | q, l => Option.map (Prod.map g₁ (Stmt.map f₁)) (M (g₂ q) (f₂.f l)))
<VAR>Γ : Type u_1<VAR>inst✝³ : Inhabited Γ<VAR>Γ' : Type u_2<VAR>inst✝² : Inhabited Γ'<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>Λ' : Type u_4<VAR>inst✝ : Inhabited Λ'<VAR>M : Machine Γ Λ<VAR>f₁ : PointedMap Γ Γ'<VAR>f₂ : PointedMap Γ' Γ<VAR>g₁ : Λ → Λ'<VAR>g₂ : Λ' → Λ<VAR>S : Set Λ<VAR>f₂₁ : Function.RightInverse f₁.f f₂.f<VAR>g₂₁ : ∀ q ∈ S, g₂ (g₁ q) = q<VAR>q : Λ<VAR>T : Tape Γ<VAR>h : { q := q, Tape := T }.q ∈ S<GOAL>Option.map (fun x => { q := g₁ x.q, Tape := Tape.map f₁ x.Tape }) (Option.map (fun x => { q := x.1, Tape := match x.2 with | Stmt.move d => Tape.move d T | Stmt.write a => Tape.write a T }) (M q T.head)) = Option.map (fun x => { q := x.1, Tape := match x.2 with | Stmt.move d => Tape.move d (Tape.map f₁ T) | Stmt.write a => Tape.write a (Tape.map f₁ T) }) (Option.map (Prod.map g₁ (Stmt.map f₁)) (M q T.head))
<VAR>k : ℕ<GOAL>derivative (bernoulli k) = ↑k * bernoulli (k - 1)
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Monoid K<VAR>inst✝³ : (i : ι) → Group (G i)<VAR>inst✝² : Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Transversal φ<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (G i)<VAR>g : PushoutI φ<VAR>w : NormalWord d<GOAL>(g • w).prod = g * w.prod
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t : Set M<VAR>s : Submodule R M<VAR>v₀ : M<GOAL>s ≤ span R {v₀} ↔ ∀ v ∈ s, ∃ r, r • v₀ = v
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a : α<VAR>ha : a ≠ 0<VAR>b c : α<GOAL>(fun x => a * x) ⁻¹' [[b, c]] = [[b / a, c / a]]
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>inst✝ : PseudoMetricSpace α<VAR>g : α → ι → ℝ<VAR>K : ℝ≥0<VAR>hg : ∀ (i : ι), LipschitzWith K fun x => g x i<VAR>a₀ a : α<VAR>M : ℝ<VAR>hM : M ∈ upperBounds (Set.range fun i => ‖g a₀ i‖)<GOAL>Memℓp (g a) ⊤
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>inst✝ : PseudoMetricSpace α<VAR>g : α → ι → ℝ<VAR>K : ℝ≥0<VAR>hg : ∀ (i : ι), LipschitzWith K fun x => g x i<VAR>a₀ a : α<VAR>M : ℝ<VAR>hM : M ∈ upperBounds (Set.range fun i => ‖g a₀ i‖)<GOAL>↑K * dist a a₀ + M ∈ upperBounds (Set.range fun i => ‖g a i‖)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F G H : C ⥤ Dᵒᵖ<VAR>α : F.leftOp ⟶ G.leftOp<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(G.map f ≫ (fun X => (α.app (op X)).op) Y).unop = ((fun X => (α.app (op X)).op) X ≫ F.map f).unop
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g h : Y ⟶ Z<GOAL>f ≫ (g - h) = f ≫ g - f ≫ h
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : NormedLinearOrderedField 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : LinearMap.CompatibleSMul E E 𝕜 ℝ<VAR>h : StrictConvex 𝕜 (closedBall 0 1)<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>StrictConvex 𝕜 (closedBall 0 r)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : NormedSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>inst✝ : FiniteDimensional ℝ V<VAR>s : Set V<VAR>hs : Convex ℝ s<GOAL>(interior s).Nonempty ↔ affineSpan ℝ s = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>R : Type u_12<VAR>R' : Type u_13<VAR>𝕜 : Type u_14<VAR>𝕜' : Type u_15<VAR>inst✝¹² : Norm E<VAR>inst✝¹¹ : Norm F<VAR>inst✝¹⁰ : Norm G<VAR>inst✝⁹ : SeminormedAddCommGroup E'<VAR>inst✝⁸ : SeminormedAddCommGroup F'<VAR>inst✝⁷ : SeminormedAddCommGroup G'<VAR>inst✝⁶ : NormedAddCommGroup E''<VAR>inst✝⁵ : NormedAddCommGroup F''<VAR>inst✝⁴ : NormedAddCommGroup G''<VAR>inst✝³ : SeminormedRing R<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedField 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>l l' : Filter α<VAR>h : (fun x => ‖f x‖) =ᶠ[l] fun x => ‖g x‖<GOAL>∀ᶠ (x : α) in l, ‖f x‖ ≤ 1 * ‖g x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>R : Type u_12<VAR>R' : Type u_13<VAR>𝕜 : Type u_14<VAR>𝕜' : Type u_15<VAR>inst✝¹² : Norm E<VAR>inst✝¹¹ : Norm F<VAR>inst✝¹⁰ : Norm G<VAR>inst✝⁹ : SeminormedAddCommGroup E'<VAR>inst✝⁸ : SeminormedAddCommGroup F'<VAR>inst✝⁷ : SeminormedAddCommGroup G'<VAR>inst✝⁶ : NormedAddCommGroup E''<VAR>inst✝⁵ : NormedAddCommGroup F''<VAR>inst✝⁴ : NormedAddCommGroup G''<VAR>inst✝³ : SeminormedRing R<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedField 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>l l' : Filter α<VAR>h : (fun x => ‖f x‖) =ᶠ[l] fun x => ‖g x‖<GOAL>∀ᶠ (x : α) in l, ‖g x‖ ≤ 1 * ‖f x‖
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>t : Cone F<VAR>h : IsLimit t<VAR>W : C<VAR>f f' : W ⟶ t.pt<VAR>w : ∀ (j : J), f ≫ t.π.app j = f' ≫ t.π.app j<GOAL>f = f'
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>t : Cone F<VAR>h : IsLimit t<VAR>W : C<VAR>f f' : W ⟶ t.pt<VAR>w : ∀ (j : J), f ≫ t.π.app j = f' ≫ t.π.app j<GOAL>h.lift { pt := W, π := { app := fun b => f ≫ t.π.app b, naturality := ⋯ } } = h.lift { pt := W, π := { app := fun b => f' ≫ t.π.app b, naturality := ⋯ } }
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>t : Cone F<VAR>h : IsLimit t<VAR>W : C<VAR>f f' : W ⟶ t.pt<VAR>w : ∀ (j : J), f ≫ t.π.app j = f' ≫ t.π.app j<GOAL>(fun b => f ≫ t.π.app b) = fun b => f' ≫ t.π.app b
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : Filter X<VAR>s t s₁ s₂ t₁ t₂ : Set X<VAR>x : X<GOAL>𝓝ˢ ∅ = ⊥
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : {i : ι} → β i → β i → Prop<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝ : (i : ι) → PartialOrder (β i)<VAR>x y : (i : ι) → β i<VAR>i : ι<VAR>a : β i<GOAL>toLex (update x i a) ≤ toLex x ↔ a ≤ x i
<VAR>m n r : ℤ<GOAL>r ∈ m.range n ↔ m ≤ r ∧ r < n
<VAR>m n r : ℤ<GOAL>(∃ a, m + ↑a < n ∧ m + ↑a = r) ↔ m ≤ r ∧ r < n
<VAR>G : Type u_1<VAR>inst✝⁴ : Group G<VAR>A : Type u_2<VAR>inst✝³ : AddGroup A<VAR>η : Type u_3<VAR>f : η → Type u_4<VAR>inst✝² : (i : η) → Group (f i)<VAR>inst✝¹ : Finite η<VAR>inst✝ : DecidableEq η<VAR>H : Subgroup ((i : η) → f i)<VAR>x : (i : η) → f i<VAR>h : ∀ (i : η), Pi.mulSingle i (x i) ∈ H<GOAL>x ∈ H
<VAR>G : Type u_1<VAR>inst✝⁴ : Group G<VAR>A : Type u_2<VAR>inst✝³ : AddGroup A<VAR>η : Type u_3<VAR>f : η → Type u_4<VAR>inst✝² : (i : η) → Group (f i)<VAR>inst✝¹ : Finite η<VAR>inst✝ : DecidableEq η<VAR>H : Subgroup ((i : η) → f i)<VAR>x : (i : η) → f i<VAR>h : ∀ (i : η), Pi.mulSingle i (x i) ∈ H<VAR>val✝ : Fintype η<GOAL>x ∈ H
<VAR>α : Type u<VAR>inst✝ : MetricSpace α<VAR>x : α<VAR>s t : NonemptyCompacts α<GOAL>infDist x ↑s ≤ infDist x ↑t + dist s t
<VAR>α : Type u<VAR>inst✝ : MetricSpace α<VAR>x : α<VAR>s t : NonemptyCompacts α<GOAL>infDist x ↑s ≤ infDist x ↑t + dist t s
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F G : C ⥤ Type w<VAR>a : C<VAR>z w : (F ⨯ G).obj a<VAR>h1 : Limits.prod.fst.app a z = Limits.prod.fst.app a w<VAR>h2 : Limits.prod.snd.app a z = Limits.prod.snd.app a w<GOAL>z = w
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F G : C ⥤ Type w<VAR>a : C<VAR>z w : (F ⨯ G).obj a<VAR>h1 : Limits.prod.fst.app a z = Limits.prod.fst.app a w<VAR>h2 : Limits.prod.snd.app a z = Limits.prod.snd.app a w<GOAL>(binaryProductEquiv F G a) z = (binaryProductEquiv F G a) w
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>x : X<GOAL>μH[0] {x} = 1
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>x : X<GOAL>μH[0] {x} ≤ 1
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>x : X<GOAL>1 ≤ μH[0] {x}
<VAR>ι : Sort u_1<VAR>c : ι → Set ↑I<VAR>hc₁ : ∀ (i : ι), IsOpen (c i)<VAR>hc₂ : univ ⊆ ⋃ i, c i<GOAL>∃ t, t 0 = 0 ∧ Monotone t ∧ (∃ n, ∀ m ≥ n, t m = 1) ∧ ∀ (n : ℕ), ∃ i, Icc (t n) (t (n + 1)) ⊆ c i
<VAR>ι : Sort u_1<VAR>c : ι → Set ↑I<VAR>hc₁ : ∀ (i : ι), IsOpen (c i)<VAR>hc₂ : univ ⊆ ⋃ i, c i<GOAL>∃ t, ↑(t 0) = ↑0 ∧ Monotone t ∧ (∃ n, ∀ m ≥ n, ↑(t m) = ↑1) ∧ ∀ (n : ℕ), ∃ i, Icc (t n) (t (n + 1)) ⊆ c i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Preorder α<VAR>inst✝³ : AddCommSemigroup α<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>a b c d : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a + b - c ≤ a - c + b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Preorder α<VAR>inst✝³ : AddCommSemigroup α<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>a b c d : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>b + a - c ≤ b + (a - c)
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>s : σ<VAR>x : List α<GOAL>x ∈ M.acceptsFrom s ↔ M.evalFrom s x ∈ M.accept
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>r : R<VAR>rs : List R<GOAL>⊤ = Ideal.ofList (r :: rs) • ⊤ ↔ ⊤ = Ideal.ofList rs • ⊤
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>r : R<VAR>rs : List R<GOAL>Subsingleton (M ⧸ Ideal.ofList (r :: rs) • ⊤) ↔ Subsingleton (QuotSMulTop r M ⧸ Ideal.ofList rs • ⊤)
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>inst✝ : Category.{v₄, u₄} D<VAR>F : J ⥤ C<VAR>X✝ Y✝ : CostructuredArrow (const J) F<VAR>f : X✝ ⟶ Y✝<VAR>j : J<GOAL>f.left ≫ ((fun c => { pt := c.left, π := c.hom }) Y✝).π.app j = ((fun c => { pt := c.left, π := c.hom }) X✝).π.app j
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>inst✝ : Category.{v₄, u₄} D<VAR>F : J ⥤ C<VAR>X✝ Y✝ : CostructuredArrow (const J) F<VAR>f : X✝ ⟶ Y✝<VAR>j : J<VAR>e_1✝ : (((fun c => { pt := c.left, π := c.hom }) X✝).pt ⟶ F.obj j) = (((const J).obj X✝.left).obj j ⟶ ((fromPUnit F).obj Y✝.right).obj j)<VAR>e_6✝ : F = (fromPUnit F).obj Y✝.right<GOAL>((fun c => { pt := c.left, π := c.hom }) X✝).π = X✝.hom ≫ (fromPUnit F).map f.right
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>a b : 𝕜<VAR>s : Set 𝕜<GOAL>ContinuousAt (dslope f a) a ↔ DifferentiableAt 𝕜 f a
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring S<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>α' : Type u_7<VAR>M' : Type u_8<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>v : α → M<VAR>v' : α' → M'<VAR>s : Set α<VAR>x : M<GOAL>x ∈ span R (v '' s) ↔ ∃ l ∈ supported R R s, (Finsupp.total α M R v) l = x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring S<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>α' : Type u_7<VAR>M' : Type u_8<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>v : α → M<VAR>v' : α' → M'<VAR>s : Set α<VAR>x : M<GOAL>x ∈ map (Finsupp.total α M R v) (supported R R s) ↔ ∃ l ∈ supported R R s, (Finsupp.total α M R v) l = x