ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>x : α<VAR>S : Set α<VAR>V : Set (α × α)<VAR>x_in : x ∈ S<VAR>V_in : V ∈ 𝓤 α ⊓ 𝓟 (S ×ˢ S)<GOAL>∃ t ∈ 𝓤 α ⊓ 𝓟 (S ×ˢ S), Prod.mk x ⁻¹' t ⊆ ball x V
<VAR>r : ℕ+<VAR>H : 1 < sumInv {2, 3, r}<VAR>h6 : 0 < 6<GOAL>r < 6
<VAR>r : ℕ+<VAR>h6 : 0 < 6<VAR>H : 6 ≤ r<GOAL>sumInv {2, 3, r} ≤ 1
<VAR>r : ℕ+<VAR>h6 : 0 < 6<VAR>H : 6 ≤ r<GOAL>(↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑r)⁻¹ ≤ 1
<VAR>r : ℕ+<VAR>h6 : 0 < 6<VAR>H : 6 ≤ r<VAR>hr : (↑↑r)⁻¹ ≤ 6⁻¹<GOAL>(↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑r)⁻¹ ≤ 1
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>X Y : SimplicialObject C<VAR>s : Splitting X<VAR>Z : C<VAR>Δ : SimplexCategoryᵒᵖ<VAR>F : (A : IndexSet Δ) → s.N (unop A.fst).len ⟶ Z<VAR>A : IndexSet Δ<GOAL>(s.cofan Δ).inj A ≫ s.desc Δ F = F A
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x y z : P<GOAL>Wbtw R x y z ↔ SameRay R (y -ᵥ x) (z -ᵥ y)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x y z : P<VAR>h : SameRay R (y -ᵥ x) (z -ᵥ y)<GOAL>Wbtw R x y z
<VAR>z : ℂ<VAR>hz : z = 0<GOAL>|z.re / abs z| ≤ 1
<VAR>z : ℂ<VAR>hz : ¬z = 0<GOAL>|z.re / abs z| ≤ 1
<VAR>cf cg : Code<GOAL>encode cf < encode (cf.comp cg) ∧ encode cg < encode (cf.comp cg)
<VAR>cf cg : Code<VAR>this : encode (cf.pair cg) < encode (cf.comp cg)<GOAL>encode cf < encode (cf.comp cg) ∧ encode cg < encode (cf.comp cg)
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>ι : Sort u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : BaireSpace X<VAR>s t : Set X<VAR>ts : t ⊆ s<VAR>ho : IsGδ t<VAR>hd : Dense t<GOAL>s ∈ residual X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f : α → β<VAR>s t : Set α<VAR>p : Set β → Prop<GOAL>(∀ t ⊆ f '' s, p t) ↔ ∀ t ⊆ s, p (f '' t)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>s : Set ℂ<VAR>f : ℂ → E<VAR>z : ℂ<VAR>hd : DifferentiableOn ℂ f s<VAR>hz : s ∈ 𝓝 z<GOAL>AnalyticAt ℂ f z
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>s : Set ℂ<VAR>f : ℂ → E<VAR>z : ℂ<VAR>hd : DifferentiableOn ℂ f s<VAR>hz : s ∈ 𝓝 z<VAR>R : ℝ<VAR>hR0 : 0 < R<VAR>hRs : closedBall z R ⊆ s<GOAL>AnalyticAt ℂ f z
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>s : Set ℂ<VAR>f : ℂ → E<VAR>z : ℂ<VAR>hd : DifferentiableOn ℂ f s<VAR>hz : s ∈ 𝓝 z<VAR>R : ℝ≥0<VAR>hR0 : 0 < ↑R<VAR>hRs : closedBall z ↑R ⊆ s<GOAL>AnalyticAt ℂ f z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Fintype α<VAR>s t : Finset α<VAR>inst✝ : DecidableEq α<VAR>a x : α<GOAL>insert x {x}ᶜ = univ
<VAR>𝕜 : Type u<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁶ : AddCommGroup F'<VAR>inst✝⁵ : Module 𝕜 F'<VAR>inst✝⁴ : TopologicalSpace F'<VAR>inst✝³ : TopologicalAddGroup F'<VAR>inst✝² : ContinuousSMul 𝕜 F'<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>v : Basis ι 𝕜 E<VAR>u : E →L[𝕜] F<VAR>M : ℝ<VAR>hM : 0 ≤ M<VAR>hu : ∀ (i : ι), ‖u (v i)‖ ≤ M<GOAL>‖u‖ ≤ Fintype.card ι • ‖↑v.equivFunL‖ * M
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>f : α → β<VAR>a : Filter α<VAR>b : β<GOAL>Tendsto f a (pure b) ↔ ∀ᶠ (x : α) in a, f x = b
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>M : Type u_6<VAR>inst✝ : CommGroup M<VAR>f : ℕ → M<VAR>n : ℕ<GOAL>f n = f 0 * ∏ i ∈ range n, f (i + 1) / f i
<VAR>a b c : ℤ<VAR>h : Fermat42 a b c<GOAL>∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0
<VAR>a b c : ℤ<VAR>h : Fermat42 a b c<VAR>a0 b0 c0 : ℤ<VAR>hf : Minimal a0 b0 c0<VAR>hc : a0 % 2 = 1<GOAL>∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0
<VAR>a b c : ℤ<VAR>h : Fermat42 a b c<VAR>a0 b0 c0 : ℤ<VAR>hf : Minimal a0 b0 c0<VAR>hc : a0 % 2 = 1<VAR>h1 : 0 < c0<GOAL>∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0
<VAR>a b c : ℤ<VAR>h : Fermat42 a b c<VAR>a0 b0 c0 : ℤ<VAR>hf : Minimal a0 b0 c0<VAR>hc : a0 % 2 = 1<VAR>h1 : 0 = c0<GOAL>∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0
<VAR>a b c : ℤ<VAR>h : Fermat42 a b c<VAR>a0 b0 c0 : ℤ<VAR>hf : Minimal a0 b0 c0<VAR>hc : a0 % 2 = 1<VAR>h1 : c0 < 0<GOAL>∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>f : ℝ → E<VAR>g : ℝ → F<VAR>k : Set ℝ<VAR>l : Filter ℝ<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : TendstoIxxClass Icc l l<VAR>hl : k ∈ l<VAR>hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x<VAR>hf : Tendsto (fun x => ‖f x‖) l atTop<VAR>hfg : deriv f =O[l] g<VAR>a : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ<VAR>f' : ℝ → UniformSpace.Completion E := ⇑a ∘ f<GOAL>¬IntegrableOn g k volume
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>f : ℝ → E<VAR>g : ℝ → F<VAR>k : Set ℝ<VAR>l : Filter ℝ<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : TendstoIxxClass Icc l l<VAR>hl : k ∈ l<VAR>hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x<VAR>hf : Tendsto (fun x => ‖f x‖) l atTop<VAR>hfg : deriv f =O[l] g<VAR>a : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ<VAR>f' : ℝ → UniformSpace.Completion E := ⇑a ∘ f<VAR>h'd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f' x<GOAL>¬IntegrableOn g k volume
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>f : ℝ → E<VAR>g : ℝ → F<VAR>k : Set ℝ<VAR>l : Filter ℝ<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : TendstoIxxClass Icc l l<VAR>hl : k ∈ l<VAR>hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x<VAR>hf : Tendsto (fun x => ‖f x‖) l atTop<VAR>hfg : deriv f =O[l] g<VAR>a : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ<VAR>f' : ℝ → UniformSpace.Completion E := ⇑a ∘ f<VAR>h'd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f' x<VAR>h'f : Tendsto (fun x => ‖f' x‖) l atTop<GOAL>¬IntegrableOn g k volume
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>f : ℝ → E<VAR>g : ℝ → F<VAR>k : Set ℝ<VAR>l : Filter ℝ<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : TendstoIxxClass Icc l l<VAR>hl : k ∈ l<VAR>hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x<VAR>hf : Tendsto (fun x => ‖f x‖) l atTop<VAR>hfg : deriv f =O[l] g<VAR>a : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ<VAR>f' : ℝ → UniformSpace.Completion E := ⇑a ∘ f<VAR>h'd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f' x<VAR>h'f : Tendsto (fun x => ‖f' x‖) l atTop<VAR>h'fg : deriv f' =O[l] g<GOAL>¬IntegrableOn g k volume
<VAR>p q : ℚ<GOAL>0 < q.toNNRat ↔ 0 < q
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>s : Cofork f g<GOAL>s.ι.app zero = f ≫ s.π
<VAR>α : Type u_1<VAR>n : ℕ<GOAL>(↑(n + 1)).toZNumNeg = -↑(n + 1)
<VAR>α : Type u_1<VAR>n : ℕ<GOAL>(↑n).toZNum.succ = (↑n).succ
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f : M →ₗ[R] A<VAR>x : M<GOAL>((lift R) f) ((ι R) x) = f x
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f : M →ₗ[R] A<VAR>x : M<GOAL>((lift R) f) ((ι R) x) = (((lift R) f).toLinearMap ∘ₗ ι R) x
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : Module R S<VAR>inst✝² : Module S A<VAR>inst✝¹ : Module R A<VAR>inst✝ : IsScalarTower R S A<VAR>s : Set S<VAR>hs : span R s = ⊤<VAR>t : Set A<VAR>k : S<VAR>x : A<VAR>hx : x ∈ span R t<GOAL>k • x ∈ span R (s • t)
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : Module R S<VAR>inst✝² : Module S A<VAR>inst✝¹ : Module R A<VAR>inst✝ : IsScalarTower R S A<VAR>s : Set S<VAR>hs : span R s = ⊤<VAR>t : Set A<VAR>k : S<VAR>x : A<VAR>hx : x ∈ span R t<GOAL>k • x ∈ restrictScalars R (span S t)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>N : Type u_9<VAR>f : N → H<VAR>g : N → H'<VAR>ϕ : N → E →L[𝕜] E'<VAR>x₀ : N<GOAL>inTangentCoordinates I I' f g ϕ x₀ = ϕ
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>h : Disjoint π₁.iUnion π₂.iUnion<GOAL>(π₁.disjUnion π₂ h).iUnion = π₁.iUnion ∪ π₂.iUnion
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x y : (P F).W α<GOAL>abs ((P F).wDest' x) = abs ((P F).wDest' y) → WEquiv x y
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x y : (P F).W α<GOAL>∀ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f : (P F).last.B a → (P F).W α), abs ((P F).wDest' ((P F).wMk a f' f)) = abs ((P F).wDest' y) → WEquiv ((P F).wMk a f' f) y
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x y : (P F).W α<VAR>a₀ : (P F).A<VAR>f'₀ : (P F).drop.B a₀ ⟹ α<VAR>f₀ : (P F).last.B a₀ → (P F).W α<GOAL>abs ((P F).wDest' ((P F).wMk a₀ f'₀ f₀)) = abs ((P F).wDest' y) → WEquiv ((P F).wMk a₀ f'₀ f₀) y
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x y : (P F).W α<VAR>a₀ : (P F).A<VAR>f'₀ : (P F).drop.B a₀ ⟹ α<VAR>f₀ : (P F).last.B a₀ → (P F).W α<GOAL>∀ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f : (P F).last.B a → (P F).W α), abs ((P F).wDest' ((P F).wMk a₀ f'₀ f₀)) = abs ((P F).wDest' ((P F).wMk a f' f)) → WEquiv ((P F).wMk a₀ f'₀ f₀) ((P F).wMk a f' f)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>X : SimplicialObject C<VAR>s : Splitting X<VAR>inst✝ : Preadditive C<VAR>j k : ℕ<VAR>A : IndexSet (op [j])<VAR>hA : ¬A.EqId<GOAL>(s.cofan (op [j])).inj A ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op [k])) = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>X : SimplicialObject C<VAR>s : Splitting X<VAR>inst✝ : Preadditive C<VAR>j k : ℕ<VAR>A : IndexSet (op [j])<VAR>hA : ¬Mono A.e<GOAL>(s.cofan (op [j])).inj A ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op [k])) = 0
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : CommRing R<VAR>x : V → R<GOAL>x ⬝ᵥ degMatrix R G *ᵥ x = ∑ i : V, ↑(G.degree i) * x i * x i
<VAR>n m : Nat<VAR>h : n ≤ m<GOAL>ofNat n ≤ ofNat m
<VAR>n m : Nat<VAR>h : n ≤ m<GOAL>(!decide (n = 0)) ≤ !decide (m = 0)
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>inst✝⁷ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} D<VAR>inst✝⁵ : HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>inst✝⁴ : G.PreservesZeroMorphisms<VAR>X' Y' : C<VAR>inst✝³ : HasKernel f<VAR>inst✝² : HasKernel (G.map f)<VAR>g : X' ⟶ Y'<VAR>inst✝¹ : HasKernel g<VAR>inst✝ : HasKernel (G.map g)<VAR>p : X ⟶ X'<VAR>q : Y ⟶ Y'<VAR>hpq : f ≫ q = p ≫ g<GOAL>G.map f ≫ G.map q = G.map p ≫ G.map g
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>inst✝⁷ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} D<VAR>inst✝⁵ : HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>inst✝⁴ : G.PreservesZeroMorphisms<VAR>X' Y' : C<VAR>inst✝³ : HasKernel f<VAR>inst✝² : HasKernel (G.map f)<VAR>g : X' ⟶ Y'<VAR>inst✝¹ : HasKernel g<VAR>inst✝ : HasKernel (G.map g)<VAR>p : X ⟶ X'<VAR>q : Y ⟶ Y'<VAR>hpq : f ≫ q = p ≫ g<GOAL>G.map (kernel.ι f) ≫ G.map f = 0
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>inst✝⁷ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} D<VAR>inst✝⁵ : HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>inst✝⁴ : G.PreservesZeroMorphisms<VAR>X' Y' : C<VAR>inst✝³ : HasKernel f<VAR>inst✝² : HasKernel (G.map f)<VAR>g : X' ⟶ Y'<VAR>inst✝¹ : HasKernel g<VAR>inst✝ : HasKernel (G.map g)<VAR>p : X ⟶ X'<VAR>q : Y ⟶ Y'<VAR>hpq : f ≫ q = p ≫ g<GOAL>G.map (kernel.ι g) ≫ G.map g = 0
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>inst✝⁷ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} D<VAR>inst✝⁵ : HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>inst✝⁴ : G.PreservesZeroMorphisms<VAR>X' Y' : C<VAR>inst✝³ : HasKernel f<VAR>inst✝² : HasKernel (G.map f)<VAR>g : X' ⟶ Y'<VAR>inst✝¹ : HasKernel g<VAR>inst✝ : HasKernel (G.map g)<VAR>p : X ⟶ X'<VAR>q : Y ⟶ Y'<VAR>hpq : f ≫ q = p ≫ g<GOAL>G.map (kernel.ι f) ≫ G.map p = G.map (kernel.map f g p q hpq) ≫ G.map (kernel.ι g)
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>inst✝⁷ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} D<VAR>inst✝⁵ : HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>inst✝⁴ : G.PreservesZeroMorphisms<VAR>X' Y' : C<VAR>inst✝³ : HasKernel f<VAR>inst✝² : HasKernel (G.map f)<VAR>g : X' ⟶ Y'<VAR>inst✝¹ : HasKernel g<VAR>inst✝ : HasKernel (G.map g)<VAR>p : X ⟶ X'<VAR>q : Y ⟶ Y'<VAR>hpq : f ≫ q = p ≫ g<GOAL>G.map (kernel.ι f ≫ p) = G.map (kernel.map f g p q hpq ≫ kernel.ι g)
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<GOAL>IsUnit A ↔ IsUnit A.det
<VAR>α : Type u_1<VAR>inst✝ : PartialOrder α<VAR>s : Set α<VAR>x✝ y✝ : α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) s<VAR>x : α<VAR>hx : x ∈ s<VAR>y : α<VAR>hy : y ∈ s<VAR>z : α<VAR>hz : z ∈ Icc x y<GOAL>z ∈ s
<VAR>α : Type u_1<VAR>inst✝ : PartialOrder α<VAR>s : Set α<VAR>x✝ y : α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) s<VAR>x : α<VAR>hx : x ∈ s<VAR>z : α<VAR>hy : x ∈ s<VAR>hz : z ∈ Icc x x<GOAL>z ∈ s
<VAR>α : Type u_1<VAR>inst✝ : PartialOrder α<VAR>s : Set α<VAR>x✝ y : α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) s<VAR>x : α<VAR>hx : x ∈ s<VAR>z : α<VAR>hy : x ∈ s<VAR>hz : z = x<GOAL>z ∈ s
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>val✝¹ : List I<VAR>property✝¹ : List.Chain' (fun x x_1 => x > x_1) val✝¹<VAR>val✝ : List I<VAR>property✝ : List.Chain' (fun x x_1 => x > x_1) val✝<GOAL>⟨val✝¹, property✝¹⟩ < ⟨val✝, property✝⟩ ↔ List.Lex (fun x x_1 => x < x_1) ↑⟨val✝¹, property✝¹⟩ ↑⟨val✝, property✝⟩
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>val✝¹ : List I<VAR>property✝¹ : List.Chain' (fun x x_1 => x > x_1) val✝¹<VAR>val✝ : List I<VAR>property✝ : List.Chain' (fun x x_1 => x > x_1) val✝<GOAL>val✝¹ < val✝ ↔ List.Lex (fun x x_1 => x < x_1) ↑⟨val✝¹, property✝¹⟩ ↑⟨val✝, property✝⟩
<VAR>V : Type u<VAR>inst✝¹ : Quiver V<VAR>a✝ b c✝ d : V<VAR>inst✝ : ∀ (a b : V), Subsingleton (a ⟶ b)<VAR>a x✝ c : V<VAR>p : Path a c<VAR>f : c ⟶ x✝<VAR>C : Path a c<VAR>D : c ⟶ x✝<VAR>hAC : p.toList = C.toList<GOAL>p.cons f = C.cons D
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>C₂₃ : Type u_6<VAR>inst✝⁸ : Category.{u_14, u_1} C₁<VAR>inst✝⁷ : Category.{u_13, u_2} C₂<VAR>inst✝⁶ : Category.{u_12, u_3} C₃<VAR>inst✝⁵ : Category.{u_11, u_4} C₄<VAR>inst✝⁴ : Category.{?u.275553, u_5} C₁₂<VAR>inst✝³ : Category.{u_15, u_6} C₂₃<VAR>F✝ F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄<VAR>F : C₁ ⥤ C₂₃ ⥤ C₄<VAR>G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>r : I₁ × I₂ × I₃ → J<VAR>ρ₂₃ : BifunctorComp₂₃IndexData r<VAR>X₁ : GradedObject I₁ C₁<VAR>X₂ : GradedObject I₂ C₂<VAR>X₃ : GradedObject I₃ C₃<VAR>inst✝² : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p<VAR>inst✝¹ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q<VAR>H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃<VAR>F₁₂ : ?m.277908<VAR>G : ?m.277911<VAR>ρ₁₂ : ?m.277914<VAR>inst✝ : ((((mapTrifunctor (bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<VAR>j : J<VAR>h : r (i₁, i₂, i₃) = j<GOAL>ιMapTrifunctorMapObj (bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ (CofanMapObjFun.iso (isColimitCofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j)).inv = ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>K : Type u_3<VAR>inst✝ : Group K<VAR>f : G →* K<VAR>g : H →* K<GOAL>(lift f g).range = f.range ⊔ g.range
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq N<VAR>inst✝ : AddGroup N<VAR>f f₁ f₂ g g₁ g₂ : α →₀ N<GOAL>(-f).neLocus g = f.neLocus (-g)
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 ≤ x<VAR>hxy : x < y<VAR>hz : 0 < z<GOAL>x ^ z < y ^ z
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 = x ∨ 0 < x<VAR>hxy : x < y<VAR>hz : 0 < z<GOAL>x ^ z < y ^ z
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : MetricSpace E<VAR>f✝ : ℕ → α → E<VAR>g✝ : α → E<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>f : ι → α → E<VAR>g : α → E<VAR>hfg : TendstoInMeasure μ f u g<GOAL>∃ ns, TendstoInMeasure μ (fun n => f (ns n)) atTop g
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : MetricSpace E<VAR>f✝ : ℕ → α → E<VAR>g✝ : α → E<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>f : ι → α → E<VAR>g : α → E<VAR>hfg : TendstoInMeasure μ f u g<VAR>ns : ℕ → ι<VAR>h_tendsto_ns : Tendsto ns atTop u<GOAL>∃ ns, TendstoInMeasure μ (fun n => f (ns n)) atTop g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>c : ℝ≥0∞<GOAL>∑ x ∈ (const α c).range, x * μ (↑(const α c) ⁻¹' {x}) = c * μ univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>c : ℝ≥0∞<VAR>h✝ : IsEmpty α<GOAL>∑ x ∈ (const α c).range, x * μ (↑(const α c) ⁻¹' {x}) = c * μ univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>c : ℝ≥0∞<VAR>h✝ : Nonempty α<GOAL>∑ x ∈ (const α c).range, x * μ (↑(const α c) ⁻¹' {x}) = c * μ univ
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Nonempty ι<VAR>inst✝¹ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : T1Space E<VAR>hp : WithSeminorms p<VAR>x : E<VAR>hx : x ≠ 0<GOAL>∃ i, (p i) x ≠ 0
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Nonempty ι<VAR>inst✝¹ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : T1Space E<VAR>hp : WithSeminorms p<VAR>x : E<VAR>hx : x ≠ 0<VAR>this : ∀ ⦃x y : E⦄, x ⤳ y → x = y<GOAL>∃ i, (p i) x ≠ 0
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Nonempty ι<VAR>inst✝¹ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : T1Space E<VAR>hp : WithSeminorms p<VAR>x : E<VAR>hx : x ≠ 0<VAR>this : ∀ ⦃x y : E⦄, x ⤳ y → x = y<VAR>h : ∀ (i : ι), (p i) x = 0<GOAL>False
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Nonempty ι<VAR>inst✝¹ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : T1Space E<VAR>hp : WithSeminorms p<VAR>x : E<VAR>hx : x ≠ 0<VAR>this : ∀ ⦃x y : E⦄, x ⤳ y → x = y<VAR>h : ∀ (i : ι), (p i) x = 0<GOAL>x ⤳ 0
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Nonempty ι<VAR>inst✝¹ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : T1Space E<VAR>hp : WithSeminorms p<VAR>x : E<VAR>hx : x ≠ 0<VAR>this : ∀ ⦃x y : E⦄, x ⤳ y → x = y<VAR>h : ∀ (i : ι), (p i) x = 0<GOAL>∀ (i : Finset ι × ℝ), 0 < i.2 → x ∈ (i.1.sup p).ball 0 i.2
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Nonempty ι<VAR>inst✝¹ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : T1Space E<VAR>hp : WithSeminorms p<VAR>x : E<VAR>hx : x ≠ 0<VAR>this : ∀ ⦃x y : E⦄, x ⤳ y → x = y<VAR>h : ∀ (i : ι), (p i) x = 0<VAR>s : Finset ι<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>x ∈ ((s, r).1.sup p).ball 0 (s, r).2
<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>𝕜' : Type u_6<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>c : E → 𝕜'<VAR>c' : E →L[𝕜] 𝕜'<VAR>hc : HasStrictFDerivAt c c' x<VAR>f : F<GOAL>HasStrictFDerivAt (fun y => c y • f) (c'.smulRight f) x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>y : R<VAR>n : ↥N<GOAL>↑(N.lTensorOne' ((algebraMap R ↥⊥) y ⊗ₜ[R] n)) = ↑(y • n)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>y : R<VAR>n : ↥N<GOAL>(mulMap 1 N) ((algebraMap R ↥⊥) y ⊗ₜ[R] n) = (algebraMap R S) y * ↑n
<VAR>ι : Type u_1<VAR>inst✝ : Countable ι<VAR>a : ι → ℂ<VAR>r : ι → ℝ<VAR>F : ℝ → ℂ<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)<VAR>h_sum : Summable fun i => ‖a i‖ / |r i| ^ s.re<GOAL>HasSum (fun i => (s + 1).Gammaℝ * a i * ↑(SignType.sign (r i)) / ↑|r i| ^ s) (mellin F ((s + 1) / 2))
<VAR>ι : Type u_1<VAR>inst✝ : Countable ι<VAR>a : ι → ℂ<VAR>r : ι → ℝ<VAR>F : ℝ → ℂ<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)<VAR>h_sum : Summable fun i => ‖a i‖ / |r i| ^ s.re<VAR>hs₁ : s ≠ 0<GOAL>HasSum (fun i => (s + 1).Gammaℝ * a i * ↑(SignType.sign (r i)) / ↑|r i| ^ s) (mellin F ((s + 1) / 2))