mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.Cover
/-- A set in a proper metric space admits a finite cover iff it is relatively compact.

[R. Vershynin, *High Dimensional Probability*][vershynin2018high], 4.2.3. Note that the print
edition incorrectly claims that this holds without the `ProperSpace X` assumption.  -/
Metric.isCompact_closure_iff_exists_finite_isCover : ∀ {X : Type u_1} [inst : MetricSpace X] [ProperSpace X] {ε : NNReal} {s : Set X},
  ε ≠ 0 → (IsCompact (closure s) ↔ ∃ N ⊆ s, N.Finite ∧ Metric.IsCover ε s N)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_of_lt_mul_of_le_one_right : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulRightMono α] {a b c : α}, a < b * c → b ≤ 1 → a < c
-- Mathlib.NumberTheory.LucasLehmer
_private.Mathlib.NumberTheory.LucasLehmer.0.LucasLehmer.norm_num_ext.sModNatTR.go.match_1.eq_1 : ∀ (motive : ℕ → ℕ → Sort u_1) (acc : ℕ) (h_1 : (acc : ℕ) → motive 0 acc) (h_2 : (n acc : ℕ) → motive n.succ acc),
  (match 0, acc with
    | 0, acc => h_1 acc
    | n.succ, acc => h_2 n acc) =
    h_1 acc
-- Lean.PrettyPrinter.Delaborator.SubExpr
/-- Uses `xa` to compute the fold across up to `maxArgs` outermost arguments of an application,
where `xf` provides the initial value and is evaluated in the context of the application minus
the arguments being folded across.
 -/
Lean.PrettyPrinter.Delaborator.SubExpr.withBoundedAppFnArgs : {α : Type} →
  {m : Type → Type} →
    [Monad m] → [MonadReaderOf Lean.SubExpr m] → [MonadWithReaderOf Lean.SubExpr m] → ℕ → m α → (α → m α) → m α
-- Mathlib.Order.Antichain
IsAntichain.image_relIso : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α},
  IsAntichain r s → ∀ (φ : r ≃r r'), IsAntichain r' (⇑φ '' s)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.saveEMatchDiagInfo : List Lean.Meta.Grind.EMatchDiagNode → Lean.Meta.Grind.EMatchDiagNode → Lean.Meta.Grind.GrindM Unit
-- Mathlib.CategoryTheory.Galois.Basic
/-- A morphism from an object with non-empty fiber to a connected object is surjective on fibers.  -/
CategoryTheory.PreGaloisCategory.surjective_of_nonempty_fiber_of_isConnected : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] {X A : C}
  [Nonempty (F.obj X).obj] [CategoryTheory.PreGaloisCategory.IsConnected A] (f : X ⟶ A),
  Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (F.map f))
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightEq_inv_app_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ : CategoryTheory.Functor B T} [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso] (r r' : R₁ ⟶ R₂) (h : r = r')
  (hr :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
      P (CategoryTheory.CategoryStruct.comp X.hom (r.app X.right)))
  (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapRightEq L r r' h hr).inv.app X).left =
    CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Order.UpperLower.Principal
LowerSet.Iic_strictMono : ∀ (α : Type u_1) [inst : Preorder α], StrictMono LowerSet.Iic
-- Mathlib.CategoryTheory.FiberedCategory.Fiber
/-- The functor including `Fiber p S` into `𝒳`.  -/
CategoryTheory.Functor.Fiber.fiberInclusion : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        {p : CategoryTheory.Functor 𝒳 𝒮} → {S : 𝒮} → CategoryTheory.Functor (p.Fiber S) 𝒳
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- `HasExactLimitsOfShape (Finset (Discrete J))ᵒᵖ C` implies  `HasExactLimitsOfShape (Discrete J) C`
 -/
CategoryTheory.hasExactLimitsOfShape_discrete_of_hasExactLimitsOfShape_finset_discrete_op : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteColimits C] (J : Type u_1)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete J) C]
  [inst_5 : CategoryTheory.Limits.HasLimitsOfShape (Finset (CategoryTheory.Discrete J))ᵒᵖ C]
  [CategoryTheory.HasExactLimitsOfShape (Finset (CategoryTheory.Discrete J))ᵒᵖ C],
  CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete J) C
-- Lean.Meta.Sym.Pattern
/-- Returns `true` if the `i`th argument / pattern variable is an instance.  -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.Pattern.isInstance : Lean.Meta.Sym.Pattern → ℕ → Bool
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.weight_coweight_transpose : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7}
  [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂] [inst_7 : AddCommGroup N₂] [inst_8 : Module R N₂]
  {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} (self : P.Hom Q),
  self.weightMap.dualMap ∘ₗ ↑Q.flip.toPerfPair = ↑P.flip.toPerfPair ∘ₗ self.coweightMap
-- Mathlib.Algebra.Category.Ring.Basic
/-- The category of commutative semirings.  -/
CommSemiRingCat : Type (u + 1)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.map_lift_equalizerComparison_assoc : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D)
  [inst_2 : CategoryTheory.Limits.HasEqualizer f g] [inst_3 : CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)]
  {Z : C} {h : Z ⟶ X} (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g) {Z_1 : D}
  (h_1 : CategoryTheory.Limits.equalizer (G.map f) (G.map g) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.equalizer.lift h w))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerComparison f g G) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.lift (G.map h) ⋯) h_1
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.iteratedSliceForward_obj : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X)
  (α : CategoryTheory.Over f),
  f.iteratedSliceForward.obj α = CategoryTheory.Over.mk (CategoryTheory.Over.Hom.left α.hom)
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
MeasureTheory.TendstoInMeasure.congr : ∀ {α : Type u_1} {ι : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : EDist E]
  {l : Filter ι} {f f' : ι → α → E} {g g' : α → E},
  (∀ (i : ι), f i =ᵐ[μ] f' i) →
    g =ᵐ[μ] g' → MeasureTheory.TendstoInMeasure μ f l g → MeasureTheory.TendstoInMeasure μ f' l g'
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.setIntegral_compl : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  {s : Set X} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G},
  MeasurableSet s →
    μ.Integrable f → ∫ᵛ (x : X) in sᶜ, f x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X) in s, f x ∂[B; μ]
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.add_sum_Ioo_eq_sum_Ico : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {f : α → M} {a b : α} [inst_1 : PartialOrder α]
  [inst_2 : LocallyFiniteOrder α], a < b → f a + ∑ x ∈ Finset.Ioo a b, f x = ∑ x ∈ Finset.Ico a b, f x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.mem_alter_of_beq_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β},
  m.WF → (k == k') = false → (k' ∈ Std.DHashMap.Raw.Const.alter m k f ↔ k' ∈ m)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the left unitor `λ_ f`.  -/
Mathlib.Tactic.BicategoryLike.StructuralAtom.leftUnitor : Lean.Expr → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.StructuralAtom
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey?_le_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k km : α}
  (hc : t.contains k = true), t.minKey?.get ⋯ = km → (cmp km k).isLE = true
-- Mathlib.Topology.Constructions
Filter.Tendsto.finInit : ∀ {Y : Type v} {n : ℕ} {A : Fin (n + 1) → Type u_9} [inst : (i : Fin (n + 1)) → TopologicalSpace (A i)]
  {f : Y → (j : Fin (n + 1)) → A j} {l : Filter Y} {x : (j : Fin (n + 1)) → A j},
  Filter.Tendsto f l (nhds x) → Filter.Tendsto (fun a => Fin.init (f a)) l (nhds (Fin.init x))
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.lid_comp_map_assoc : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} {M' : Type u_6} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N]
  [inst_5 : AddCommMonoid P] [inst_6 : Module R P] [inst_7 : AddCommMonoid M'] [inst_8 : Module R M'] (f : M →ₗ[R] R)
  (g : N →ₗ[R] M') (h : P →ₗ[R] TensorProduct R M N),
  ↑(TensorProduct.lid R M') ∘ₗ TensorProduct.map f g ∘ₗ h =
    g ∘ₗ ↑(TensorProduct.lid R N) ∘ₗ TensorProduct.map f LinearMap.id ∘ₗ h
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.jacobian_ofAlgEquiv : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.PreSubmersivePresentation R S ι σ) {T : Type u_1} [inst_3 : CommRing T] [inst_4 : Algebra R T]
  (e : S ≃ₐ[R] T) [inst_5 : Finite σ], (P.ofAlgEquiv e).jacobian = e P.jacobian
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMonObj.add_comp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N X : C} [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.AddMonObj N] (f₁ f₂ : X ⟶ M) (g : M ⟶ N)
  [CategoryTheory.IsAddMonHom g] {Z : C} (h : N ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f₁ + f₂) (CategoryTheory.CategoryStruct.comp g h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp f₁ g + CategoryTheory.CategoryStruct.comp f₂ g) h
-- Mathlib.Data.Finset.MulAntidiagonal
Finset.antidiagonal_mono_left : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α] {s t : Set α}
  {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {u : Set α} {hu : u.IsPWO},
  u ⊆ s → Finset.antidiagonal hu ht a ⊆ Finset.antidiagonal hs ht a
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Reachable.of_isUniversal : ∀ {V : Type u} {G : SimpleGraph V} {u : V} (v : V), G.IsUniversal u → G.Reachable u v
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.of_ofAlgEquiv_symm : ∀ {S : Type u_5} [inst : CommRing S] (I : Ideal S) [inst_1 : IsAdicComplete I S] (x : AdicCompletion I S),
  (AdicCompletion.of I S) ((AdicCompletion.ofAlgEquiv I).symm x) = x
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.processArrayLit : Lean.Meta.Match.Problem → Lean.MetaM (Array Lean.Meta.Match.Problem)
-- Lean.Meta.AbstractMVars
Lean.Meta.AbstractMVars.instMonadMCtxM : Lean.MonadMCtx Lean.Meta.AbstractMVars.M
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.cancel_right : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_9} {M₂ : Type u_10} {M₃ : Type u_11} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {f : M₂ →ₛₗ[σ₂₃] M₃}
  {g : M₁ →ₛₗ[σ₁₂] M₂} {f' : M₂ →ₛₗ[σ₂₃] M₃}, Function.Surjective ⇑g → (f ∘ₛₗ g = f' ∘ₛₗ g ↔ f = f')
-- Mathlib.ModelTheory.Syntax
/-- `Formula α` is the type of formulas with free variables indexed by `α` and no bound variables in
scope.  -/
FirstOrder.Language.Formula : FirstOrder.Language → Type u' → Type (max u v u')
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀'_hom_inv_id_assoc : ∀ {C : Type u_1} {ι' : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : Preorder ι'] (X' : CategoryTheory.Abelian.SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁)
  (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ)
  (h : CategoryTheory.Limits.IsZero ((X'.H n₂).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hi₀₁))))
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀'_hom_inv_id._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀'_hom_inv_id._auto_3) {Z : C}
  (h_1 :
    X'.E (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE hi₂₃) (CategoryTheory.homOfLE hi₃₄) n₀ n₁ n₂ hn₁ hn₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂)
      (CategoryTheory.CategoryStruct.comp
        (X'.isoMapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂).inv h_1) =
    h_1
-- Mathlib.Lean.Expr.Basic
Lean.Expr.bvarIdx? : Lean.Expr → Option ℕ
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_mono_measure : ∀ {α : Type u_2} {x : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  μ ≤ ν → ∀ (s : Set α), μ.restrict s ≤ ν.restrict s
-- Batteries.Control.AlternativeMonad
OptionT.instAlternativeMonadOfMonad : (m : Type u_1 → Type u_2) → [Monad m] → AlternativeMonad (OptionT m)
-- Mathlib.RingTheory.Ideal.Cotangent
/-- The map `I/I² → J/J²` if `I ≤ f⁻¹(J)`.  -/
Ideal.mapCotangent : {R : Type u} →
  [inst : CommRing R] →
    {A : Type u_1} →
      {B : Type u_2} →
        [inst_1 : CommRing A] →
          [inst_2 : CommRing B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] →
                (I₁ : Ideal A) →
                  (I₂ : Ideal B) → (f : A →ₐ[R] B) → I₁ ≤ Ideal.comap f I₂ → I₁.Cotangent →ₗ[R] I₂.Cotangent
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- **Riesz's theorem**: if a closed ball with center zero of positive radius is compact in a vector
space, then the space is finite-dimensional.  -/
FiniteDimensional.of_isCompact_closedBall₀ : ∀ (𝕜 : Type u) [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {V : Type u_1} [inst_2 : NormedAddCommGroup V]
  [inst_3 : Module 𝕜 V] [ContinuousSMul 𝕜 V] {r : ℝ}, 0 < r → IsCompact (Metric.closedBall 0 r) → FiniteDimensional 𝕜 V
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.lt_aleph0_iff_finite : ∀ {α : Type u}, Cardinal.mk α < Cardinal.aleph0 ↔ Finite α
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_zero : ∀ (n : Type u_3) (R : Type u_6) [inst : Fintype n] [inst_1 : AddCommMonoid R], Matrix.trace 0 = 0
-- Mathlib.LinearAlgebra.RootSystem.Defs
/-- A parametrized family of vectors, called roots.  -/
RootPairing.root : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] → [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → RootPairing ι R M N → ι ↪ M
-- Mathlib.Computability.TuringMachine.Tape
Turing.ListBlank.tail_mk : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (l : List Γ), (Turing.ListBlank.mk l).tail = Turing.ListBlank.mk l.tail
-- Mathlib.Tactic.FunProp.Theorems
/-- total number of arguments applied to the function  -/
Mathlib.Meta.FunProp.FunctionTheorem.appliedArgs : Mathlib.Meta.FunProp.FunctionTheorem → ℕ
-- Init.Data.Nat.ToString
Nat.one_eq_digitChar : ∀ {n : ℕ}, '1' = n.digitChar ↔ n = 1
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instNSMul : {ι : Type u_1} →
  (R : ι → Type u_2) →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            [inst_1 : (i : ι) → AddMonoid (R i)] →
              [∀ (i : ι), AddSubmonoidClass (S i) (R i)] → SMul ℕ (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)
-- Init.Grind.Lemmas
Lean.Grind.eq_true_of_and_eq_true_right : ∀ {a b : Prop}, (a ∧ b) = True → b = True
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.integral_def : ∀ {α : Type u_5} {E : Type u_6} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E], MeasureTheory.L1.integral = ⇑MeasureTheory.L1.integralCLM
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.cons_transpose : ∀ {α : Type u} {m : ℕ} {n' : Type uₙ} (v : n' → α) (A : Matrix (Fin m) n' α),
  (Matrix.of (Matrix.vecCons v A)).transpose = Matrix.of fun i => Matrix.vecCons (v i) (A.transpose i)
-- Mathlib.Topology.Inseparable
SeparationQuotient.lift₂.congr_simp : ∀ {X : Type u_1} {Y : Type u_2} {α : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (f f_1 : X → Y → α) (e_f : f = f_1)
  (hf : ∀ (a : X) (b : Y) (c : X) (d : Y), Inseparable a c → Inseparable b d → f a b = f c d)
  (a a_1 : SeparationQuotient X),
  a = a_1 →
    ∀ (a_2 a_3 : SeparationQuotient Y),
      a_2 = a_3 → SeparationQuotient.lift₂ f hf a a_2 = SeparationQuotient.lift₂ f_1 ⋯ a_1 a_3
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.mk : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {F : CategoryTheory.Functor C D} →
          {A : Type u_6} →
            [inst_2 : AddMonoid A] →
              [inst_3 : CategoryTheory.HasShift C A] →
                [inst_4 : CategoryTheory.HasShift D A] →
                  (commShiftIso :
                      (a : A) → (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)) →
                    autoParam (commShiftIso 0 = CategoryTheory.Functor.CommShift.isoZero F A)
                        CategoryTheory.Functor.CommShift.commShiftIso_zero._autoParam →
                      autoParam
                          (∀ (a b : A),
                            commShiftIso (a + b) =
                              CategoryTheory.Functor.CommShift.isoAdd (commShiftIso a) (commShiftIso b))
                          CategoryTheory.Functor.CommShift.commShiftIso_add._autoParam →
                        F.CommShift A
-- Init.Data.Int.Cooper
/-- `resolve_left` is nonnegative when `p ≤ a * x`.  -/
Int.Cooper.le_zero_resolve_left : ∀ (a c d p x : ℤ), p ≤ a * x → 0 ≤ Int.Cooper.resolve_left a c d p x
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.zero_def : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} [inst_1 : Nontrivial R],
  0 = { point := ⟦![1, 1, 0]⟧, nonsingular := ⋯ }
-- Std.Http.Data.Method
Std.Http.Method.pri.sizeOf_spec : sizeOf Std.Http.Method.pri = 1
-- Mathlib.CategoryTheory.Abelian.Injective.Ext
/-- If `R` is an injective resolution of `Y`, then `Ext X Y n` identifies
to the type of cohomology classes of degree `n` from `(singleFunctor C 0).obj X`
to `R.cochainComplex`.  -/
CategoryTheory.InjectiveResolution.extEquivCohomologyClass : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.HasExt C] →
        {X Y : C} →
          (R : CategoryTheory.InjectiveResolution Y) →
            {n : ℕ} →
              CategoryTheory.Abelian.Ext X Y n ≃
                CochainComplex.HomComplex.CohomologyClass ((CochainComplex.singleFunctor C 0).obj X) R.cochainComplex ↑n
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.bind_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {T : C} (E : CategoryTheory.PreZeroHypercover T)
  (F : (i : E.I₀) → CategoryTheory.PreZeroHypercover (E.X i)) (ij : (i : E.I₀) × (F i).I₀),
  (E.bind F).f ij = CategoryTheory.CategoryStruct.comp ((F ij.fst).f ij.snd) (E.f ij.fst)
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.instFromJsonClientInfo : Lean.FromJson Lean.Lsp.ClientInfo
-- Init.System.IOError
IO.Error.mkResourceExhaustedFile : String → UInt32 → String → IO.Error
-- Mathlib.GroupTheory.GroupAction.Primitive
MulAction.IsPreprimitive.of_surjective : ∀ {M : Type u_3} [inst : Group M] {α : Type u_4} [inst_1 : MulAction M α] {N : Type u_5} {β : Type u_6}
  [inst_2 : Group N] [inst_3 : MulAction N β] {φ : M → N} {f : α →ₑ[φ] β} [MulAction.IsPreprimitive M α],
  Function.Surjective ⇑f → MulAction.IsPreprimitive N β
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_diff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Raw.Const.get! (m₁ \ m₂) k =
          if m₂.contains k = true then default else Std.DTreeMap.Raw.Const.get! m₁ k
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
abs_sub_sup_add_abs_sub_inf : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddCommGroup α] [AddLeftMono α] (a b c : α),
  |a ⊔ c - b ⊔ c| + |a ⊓ c - b ⊓ c| = |a - b|
-- Mathlib.CategoryTheory.Shift.Pullback
/-- When `b = φ a`, this is the canonical
isomorphism `shiftFunctor (PullbackShift C φ) a ≅ shiftFunctor C b`.  -/
CategoryTheory.pullbackShiftIso : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {A : Type u_2} →
      {B : Type u_3} →
        [inst_1 : AddMonoid A] →
          [inst_2 : AddMonoid B] →
            [inst_3 : CategoryTheory.HasShift C B] →
              (φ : A →+ B) →
                (a : A) →
                  (b : B) →
                    b = φ a →
                      (CategoryTheory.shiftFunctor (CategoryTheory.PullbackShift C φ) a ≅
                        CategoryTheory.shiftFunctor C b)
-- Mathlib.Topology.Connected.Clopen
Sigma.isPreconnected_iff : ∀ {ι : Type u_1} {X : ι → Type u_2} [hι : Nonempty ι] [inst : (i : ι) → TopologicalSpace (X i)]
  {s : Set ((i : ι) × X i)}, IsPreconnected s ↔ ∃ i t, IsPreconnected t ∧ s = Sigma.mk i '' t
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.constr_basis : ∀ {M' : Type u_7} [inst : AddCommMonoid M'] {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst_1 : Semiring R]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] (b : Module.Basis ι R M) [inst_4 : Module R M'] (S : Type u_13)
  [inst_5 : Semiring S] [inst_6 : Module S M'] [inst_7 : SMulCommClass R S M'] (f : ι → M') (i : ι),
  ((b.constr S) f) (b i) = f i
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey!_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α] [inst : Inhabited α]
  (h : t.WF) {l : List α} {k : α},
  k ∈ t → (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l ⋯)).getKey! k = t.getKey! k
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` creates limits of `K.op : Jᵒᵖ ⥤ Cᵒᵖ`, then `F.unop : C ⥤ D` creates
colimits of `K : J ⥤ C`.  -/
CategoryTheory.Limits.createsColimitUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (K : CategoryTheory.Functor J C) →
              (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) →
                [CategoryTheory.CreatesLimit K.op F] → CategoryTheory.CreatesColimit K F.unop