mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂)
  (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
  (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f)
  (X : ↑(F.obj b₀)) {Z : ↑(F.obj b₃)} (h : (F.map f₂₃).toFunctor.obj ((F.map f₀₂).toFunctor.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₂ f₂₃ f ⋯).hom.toNatTrans.app X) h =
    CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₁ f₁₃ f ⋯).hom.toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp
        ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom.toNatTrans.app ((F.map f₀₁).toFunctor.obj X))
        (CategoryTheory.CategoryStruct.comp
          ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv.toNatTrans.app X)) h))
-- Aesop.RuleTac.Basic
Aesop.CasesTarget.decl.sizeOf_spec : ∀ (decl : Lean.Name), sizeOf (Aesop.CasesTarget.decl decl) = 1 + sizeOf decl
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instTheoremLikeInjectiveTheorem : Lean.Meta.Grind.TheoremLike Lean.Meta.Grind.InjectiveTheorem
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
nullMeasurableSet_lt' : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : LinearOrder α]
  [SecondCountableTopology α] [OrderClosedTopology α] {μ : MeasureTheory.Measure (α × α)},
  MeasureTheory.NullMeasurableSet {p | p.1 < p.2} μ
-- Lean.Setup
Lean.ModuleArtifacts.oleanServer? : Lean.ModuleArtifacts → Option System.FilePath
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0.Cfg.mk : {Γ : Type u_1} → {Λ : Type u_2} → [inst : Inhabited Γ] → Λ → Turing.Tape Γ → Turing.TM0.Cfg Γ Λ
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.instBEqPoly.beq_spec_2 : ∀ (a : ℤ) (a_1 : Lean.Grind.Linarith.Var) (a_2 : Lean.Grind.Linarith.Poly) (b : ℤ) (b_1 : Lean.Grind.Linarith.Var)
  (b_2 : Lean.Grind.Linarith.Poly),
  (Lean.Grind.Linarith.Poly.add a a_1 a_2 == Lean.Grind.Linarith.Poly.add b b_1 b_2) =
    (a == b && (a_1 == b_1 && a_2 == b_2))
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- The canonical isomorphism `(homotopyCofiber φ).X i ≅ F.X j ⊞ G.X i` when `c.Rel i j`.  -/
HomologicalComplex.homotopyCofiber.XIsoBiprod : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          {F G : HomologicalComplex C c} →
            (φ : F ⟶ G) →
              [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
                [inst_3 : DecidableRel c.Rel] →
                  (i j : ι) →
                    c.Rel i j →
                      [inst_4 : CategoryTheory.Limits.HasBinaryBiproduct (F.X j) (G.X i)] →
                        HomologicalComplex.homotopyCofiber.X φ i ≅ F.X j ⊞ G.X i
-- Mathlib.Algebra.GroupWithZero.Action.Pi
Pi.single_smul : ∀ {I : Type u} {f : I → Type v} {α : Type u_1} [inst : Monoid α] [inst_1 : (i : I) → AddMonoid (f i)]
  [inst_2 : (i : I) → DistribMulAction α (f i)] [inst_3 : DecidableEq I] (i : I) (r : α) (x : f i),
  Pi.single i (r • x) = r • Pi.single i x
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.coindep_iff_closure_compl_eq_ground : ∀ {α : Type u_2} {M : Matroid α} {X : Set α},
  autoParam (X ⊆ M.E) Matroid.coindep_iff_closure_compl_eq_ground._auto_1 → (M.Coindep X ↔ M.closure (M.E \ X) = M.E)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.foldRev_eq_foldr_toListModel : ∀ {α : Type u} {β : α → Type v} {γ : Type w} {l : Std.DHashMap.Raw α β} {f : γ → (a : α) → β a → γ} {init : γ},
  Std.DHashMap.Raw.Internal.foldRev f init l =
    List.foldr (fun a b => f b a.fst a.snd) init (Std.DHashMap.Internal.toListModel l.buckets)
-- Mathlib.Order.Category.LinOrd
LinOrd.Hom.ext_iff : ∀ {X Y : LinOrd} {x y : X.Hom Y}, x = y ↔ x.hom' = y.hom'
-- Mathlib.Combinatorics.Enumerative.Composition
List.splitWrtCompositionAux.eq_1 : ∀ {α : Type u_1} (x : List α), x.splitWrtCompositionAux [] = []
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_le_size_alter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k : α} {f : Option β → Option β}, m.WF → m.size - 1 ≤ (m.alter k f).size
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.commRing : {R : Type u} → [inst : CommRing R] → (self : CommBialgCat R) → CommRing ↑self
-- Mathlib.Analysis.Normed.Operator.NormedSpace
ContinuousLinearMap.norm_inl_le_one : ∀ (𝕜 : Type u_9) [inst : NontriviallyNormedField 𝕜] (E : Type u_10) (F : Type u_11) [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F],
  ‖ContinuousLinearMap.inl 𝕜 E F‖ ≤ 1
-- Init.Coe
/-- Auxiliary class implementing `CoeOut* Coe*`.
Users should generally not implement this directly.
 -/
CoeOTC : Sort u → Sort v → Sort (max (max 1 u) v)
-- Mathlib.Analysis.Complex.Norm
Complex.norm_sub_one_sq_eqOn_sphere : Set.EqOn (fun x => ‖x - 1‖ ^ 2) (fun z => 2 * (1 - z.re)) (Metric.sphere 0 1)
-- Std.Time.Date.Unit.Month
/-- The ordinal value representing the month of July.
 -/
Std.Time.Month.Ordinal.july : Std.Time.Month.Ordinal
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.case : Turing.ToPartrec.Code → Turing.ToPartrec.Code → Turing.ToPartrec.Code
-- Mathlib.Order.SuccPred.Limit
Order.not_isPredPrelimit_iff_mem_range_pred : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : PredOrder α] [NoMinOrder α],
  ¬Order.IsPredPrelimit a ↔ a ∈ Set.range Order.pred
-- Init.Data.SInt.Lemmas
Int16.minValue_div_neg_one : Int16.minValue / -1 = Int16.minValue
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.FinMeasSupp.of_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} [inst : Zero β] [inst_1 : Zero γ]
  {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α β} {g : β → γ},
  (MeasureTheory.SimpleFunc.map g f).FinMeasSupp μ → (∀ (b : β), g b = 0 → b = 0) → f.FinMeasSupp μ
-- Mathlib.Data.PFunctor.Multivariate.Basic
MvPFunctor.mk.inj : ∀ {n : ℕ} {A : Type u} {B : A → TypeVec.{u} n} {A_1 : Type u} {B_1 : A_1 → TypeVec.{u} n},
  { A := A, B := B } = { A := A_1, B := B_1 } → A = A_1 ∧ B ≍ B_1
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.ιTotalOrZero_eq_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂), c₁.π c₂ c₁₂ (i₁, i₂) ≠ i₁₂ → K.ιTotalOrZero c₁₂ i₁ i₂ i₁₂ = 0
-- Mathlib.Combinatorics.SetFamily.Compression.Down
/-- `a`-down-compressing `𝒜` means removing `a` from the elements of `𝒜` that contain it, when the
resulting Finset is not already in `𝒜`.  -/
FinsetFamily.term𝓓 : Lean.ParserDescr
-- Mathlib.Combinatorics.Configuration
Configuration.ProjectivePlane.instDual : (P : Type u_1) →
  (L : Type u_2) →
    [inst : Membership P L] →
      [Configuration.ProjectivePlane P L] → Configuration.ProjectivePlane (Configuration.Dual L) (Configuration.Dual P)
-- Lean.Data.Lsp.Extra
/-- `$/lean/plainGoal` client<-server reply.  -/
Lean.Lsp.PlainGoal : Type
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Impl.pruneLE.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (lowerBound : α) (sz : ℕ) (k : α) (v : β k)
  (l r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.pruneLE✝ (Std.DTreeMap.Internal.Impl.inner sz k v l r) lowerBound =
    match compare lowerBound k with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.inner sz k v (Std.DTreeMap.Internal.Impl.pruneLE✝ l lowerBound) r
    | Ordering.eq => Std.DTreeMap.Internal.Impl.inner sz k v Std.DTreeMap.Internal.Impl.leaf r
    | Ordering.gt => Std.DTreeMap.Internal.Impl.pruneLE✝ r lowerBound
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.snakeInput_L₂_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z), (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).L₂.f = CategoryTheory.Limits.biprod.inl
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.congr_nhdsWithin : ∀ {H : Type u_1} {H' : Type u_3} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace H'] {G : StructureGroupoid H}
  {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop},
  G.LocalInvariantProp G' P →
    ∀ {s : Set H} {x : H} {f g : H → H'}, f =ᶠ[nhdsWithin x s] g → f x = g x → P f s x → P g s x
-- Init.Data.Int.LemmasAux
Int.sub_min_sub_left : ∀ (a b c : ℤ), min (a - b) (a - c) = a - max b c
-- Init.Data.String.Lemmas.Splits
_private.Init.Data.String.Lemmas.Splits.0.String.Pos.Splits.rotateRight.eq_1 : ∀ {s : String} {p : s.Pos} {t₁ t₂ t₃ : String} (h : p.Splits t₁ (t₂ ++ t₃)),
  h.rotateRight = String.Pos.ofToSlice ⋯.rotateRight
-- Lean.ReducibilityAttrs
/-- Return `true` if the given declaration has been marked as `[instance_reducible]`
(automatically applied by the `instance` command and by subobject class projections).  -/
Lean.isInstanceReducible : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m Bool
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.Limits.inl_comp_pushoutSymmetry_hom_whiskerRight_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasPushouts C] {Q X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.Limits.pushout g f) Q ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.pushout.inl f g) Q)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.pushoutSymmetry f g).hom Q) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.pushout.inr g f) Q) h
-- Mathlib.Algebra.Ring.Idempotent
IsIdempotentElem.add_sub_mul : ∀ {R : Type u_1} [inst : CommRing R] {a b : R},
  IsIdempotentElem a → IsIdempotentElem b → IsIdempotentElem (a + b - a * b)
-- Mathlib.Topology.Sober
/-- Any R1 space is a quasi-sober space because any irreducible set is
contained in the closure of a singleton.
 -/
R1Space.quasiSober : ∀ {α : Type u_1} [inst : TopologicalSpace α] [R1Space α], QuasiSober α
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.apply_sum_inl_eq_zero_of_mem_span_h : ∀ {ι : 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] {P : RootPairing ι R M N}
  [inst_5 : P.IsCrystallographic] {b : P.Base} (i : ↥b.support) (j : ↥b.support ⊕ ι)
  {x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R},
  x ∈ Submodule.span R (Set.range RootPairing.GeckConstruction.h) → x j (Sum.inl i) = 0
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Augmented.w_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.CosimplicialObject.Augmented C}
  {η : X ⟶ Y} {n : SimplexCategory} {Z : C} (h : Y.right.obj n ⟶ Z),
  CategoryTheory.CategoryStruct.comp η.left (CategoryTheory.CategoryStruct.comp (Y.hom.app n) h) =
    CategoryTheory.CategoryStruct.comp (X.hom.app n) (CategoryTheory.CategoryStruct.comp (η.right.app n) h)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.SupportsStmt.eq_6 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (S : Finset Λ), Turing.TM1.SupportsStmt S Turing.TM1.Stmt.halt = True
-- Lean.Meta.Tactic.Injection
Lean.Meta.InjectionResult.subgoal.injEq : ∀ (mvarId : Lean.MVarId) (newEqs : Array Lean.FVarId) (remainingNames : List Lean.Name) (mvarId_1 : Lean.MVarId)
  (newEqs_1 : Array Lean.FVarId) (remainingNames_1 : List Lean.Name),
  (Lean.Meta.InjectionResult.subgoal mvarId newEqs remainingNames =
      Lean.Meta.InjectionResult.subgoal mvarId_1 newEqs_1 remainingNames_1) =
    (mvarId = mvarId_1 ∧ newEqs = newEqs_1 ∧ remainingNames = remainingNames_1)
-- Init.Data.String.Basic
/-- Given a slice and a valid position within the slice, obtain a new slice on the same underlying
string by replacing the end of the slice with the given position.  -/
String.Slice.sliceTo : (s : String.Slice) → s.Pos → String.Slice
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.union_eq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β}, m₁.union m₂ = m₁ ∪ m₂
-- Lean.Meta.ArgsPacker.Basic
/-- Variable names to use when unpacking a packed argument.

Crucially, the size of this array also indicates the number of functions to pack, and
the length of each array the arity.
 -/
Lean.Meta.ArgsPacker.varNamess : Lean.Meta.ArgsPacker → Array (Array Lean.Name)
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.Meq.equiv.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [inst_3 : CategoryTheory.ConcreteCategory D FD]
  [inst_4 :
    ∀ {X : C} (S : J.Cover X),
      CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
        (CategoryTheory.forget D)]
  {X : C} (P : CategoryTheory.Functor Cᵒᵖ D) (S : J.Cover X)
  [inst_5 : CategoryTheory.Limits.HasMultiequalizer (S.index P)],
  CategoryTheory.Meq.equiv P S = CategoryTheory.Meq.equiv P S
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.equiv_iff_keys_unit_perm : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {m₁ m₂ : Std.DHashMap α fun x => Unit},
  m₁.Equiv m₂ ↔ m₁.keys.Perm m₂.keys
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get!_diff_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [inst_2 : Inhabited α] [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ \ m₂).get! k = m₁.get! k
-- Std.Tactic.BVDecide.LRAT.Internal.Entails
/-- `f1` logically implies `f2`  -/
Std.Tactic.BVDecide.LRAT.Internal.Limplies : (α : Type u) →
  {σ1 : Type v} →
    {σ2 : Type w} →
      [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ1] →
        [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ2] → σ1 → σ2 → Prop
-- Init.Data.Nat.Bitwise.Lemmas
Nat.or_and_distrib_right : ∀ (x y z : ℕ), x &&& y ||| z = (x ||| z) &&& (y ||| z)
-- Mathlib.Order.Sublattice
/-- Copy of a sublattice with a new `carrier` equal to the old one. Useful to fix definitional
equalities.  -/
Sublattice.copy : {α : Type u_2} → [inst : Lattice α] → (L : Sublattice α) → (s : Set α) → s = ↑L → Sublattice α
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.C_eval_neg_two : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ), Polynomial.eval (-2) (Polynomial.Chebyshev.C R n) = 2 * ↑↑n.negOnePow
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get_insert_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {v : β}, Std.DTreeMap.Const.get (t.insert k v) k ⋯ = v
-- Mathlib.Data.Finset.Insert
Finset.eq_of_mem_cons_of_notMem : ∀ {α : Type u_1} {s : Finset α} {a b : α} (has : a ∉ s), b ∈ Finset.cons a s has → b ∉ s → b = a
-- Mathlib.RingTheory.Polynomial.Basic
mem_span_C_coeff : ∀ {R : Type u} [inst : Semiring R] {f : Polynomial R}, f ∈ Ideal.span {g | ∃ i, g = Polynomial.C (f.coeff i)}
-- Mathlib.Tactic.FieldSimp
/-- Constraints on denominators which may need to be considered in `field_simp`: no condition,
nonzeroness, or strict positivity.  -/
Mathlib.Tactic.FieldSimp.DenomCondition : {v : Lean.Level} → {M : Q(Type v)} → Q(GroupWithZero «$M») → Type
-- Lean.Meta.ReduceEval
Lean.Meta.instReduceEvalNat : Lean.Meta.ReduceEval ℕ
-- Mathlib.Order.Filter.Bases.Basic
/-- We say that a filter `l` has a basis `s : ι → Set α` bounded by `p : ι → Prop`,
if `t ∈ l` if and only if `t` includes `s i` for some `i` such that `p i`.  -/
Filter.HasBasis : {α : Type u_1} → {ι : Sort u_4} → Filter α → (ι → Prop) → (ι → Set α) → Prop
-- Mathlib.Combinatorics.Hindman
Hindman.FP.singleton : ∀ {M : Type u_1} [inst : Semigroup M] (a : Stream' M) (i : ℕ), a.get i ∈ Hindman.FP a
-- Mathlib.RingTheory.Finiteness.Basic
Module.Finite.ulift : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Finite R M], Module.Finite R (ULift.{u_6, u_4} M)
-- Init.Data.BitVec.Bitblast
BitVec.getElem_add_add_bool : ∀ {w i : ℕ} (i_lt : i < w) (x y : BitVec w) (c : Bool),
  (x + y + BitVec.setWidth w (BitVec.ofBool c))[i] = (x[i] ^^ (y[i] ^^ BitVec.carry i x y c))
-- Mathlib.Analysis.CStarAlgebra.Basic
/-- A normed star group is a normed group with a compatible `star` which is isometric.  -/
NormedStarGroup : (E : Type u_1) → [inst : SeminormedAddCommGroup E] → [StarAddMonoid E] → Prop
-- Mathlib.Topology.Algebra.UniformConvergence
instAddCommGroupUniformFun : {α : Type u_1} → {β : Type u_2} → [AddCommGroup β] → AddCommGroup (UniformFun α β)
-- Mathlib.Topology.Order.WithTop
WithBot.continuous_unbot : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι],
  Continuous fun x => (↑x).unbot ⋯
-- Mathlib.CategoryTheory.Sites.Plus
CategoryTheory.GrothendieckTopology.isoToPlus_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  (P : CategoryTheory.Functor Cᵒᵖ D) [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  (hP : CategoryTheory.Presheaf.IsSheaf J P),
  (J.isoToPlus P hP).inv = J.plusLift (CategoryTheory.CategoryStruct.id P) hP
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.instCoeSortType : CoeSort GrpCat (Type u)
-- Mathlib.Topology.UniformSpace.Completion
CauchyFilter.separated_pureCauchy_injective : ∀ {α : Type u_1} [inst : UniformSpace α] [T0Space α],
  Function.Injective fun a => SeparationQuotient.mk (CauchyFilter.pureCauchy a)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach.0.Std.Iterators.Types.Attach.Monadic.modifyStep.match_1.eq_3 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {P : β → Prop}
  (it : Std.IterM m { out // P out }) (motive : it.internalState.inner.Step → Sort u_3)
  (property : it.internalState.inner.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) →
        (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out)) →
          motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 :
    (it' : Std.IterM m β) →
      (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.internalState.inner.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.done, property⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_3 property
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgResult.star.sizeOf_spec : sizeOf Lean.Elab.Tactic.ElabSimpArgResult.star = 1
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.lt_rpow_inv_iff_of_neg : ∀ {x : NNReal} {z : ℝ} {y : NNReal}, 0 < x → 0 < y → z < 0 → (x < y ^ z⁻¹ ↔ y < x ^ z)
-- Mathlib.Algebra.Category.Grp.Colimits
/-- The additive equivalence between `Quot F` and `Quot (F ⋙ uliftFunctor.{u'})`.
 -/
AddCommGrpCat.Colimits.quotQuotUliftAddEquiv : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    (F : CategoryTheory.Functor J AddCommGrpCat) →
      [inst_1 : DecidableEq J] →
        AddCommGrpCat.Colimits.Quot F ≃+ AddCommGrpCat.Colimits.Quot (F.comp AddCommGrpCat.uliftFunctor)
-- Mathlib.CategoryTheory.GuitartExact.Opposite
/-- Auxiliary definition for `structuredArrowRightwardsOpEquivalence`.  -/
CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.functor : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : Type u₄} →
        [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                {T : CategoryTheory.Functor C₁ C₂} →
                  {L : CategoryTheory.Functor C₁ C₃} →
                    {R : CategoryTheory.Functor C₂ C₄} →
                      {B : CategoryTheory.Functor C₃ C₄} →
                        (w : CategoryTheory.TwoSquare T L R B) →
                          {X₃ : C₃ᵒᵖ} →
                            {X₂ : C₂ᵒᵖ} →
                              (g : B.op.obj X₃ ⟶ R.op.obj X₂) →
                                CategoryTheory.Functor (w.op.StructuredArrowRightwards g)ᵒᵖ
                                  (w.CostructuredArrowDownwards g.unop)
-- Mathlib.Algebra.Homology.HomotopyCategory
HomotopyCategory.instEssSurjHomologicalComplexQuotient : ∀ {ι : Type u_2} (V : Type u) [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  (c : ComplexShape ι), (HomotopyCategory.quotient V c).EssSurj
-- Mathlib.Data.Matrix.Diagonal
Matrix.submatrix_one : ∀ {l : Type u_1} {m : Type u_2} {α : Type v} [inst : Zero α] [inst_1 : One α] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq l] (e : l → m), Function.Injective e → Matrix.submatrix 1 e e = 1
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapAddMonFunctor_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (D : Type u₂)
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.LaxMonoidalFunctor C D), (CategoryTheory.Functor.mapAddMonFunctor C D).obj F = F.mapAddMon
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Nat.nthRoot_zero_right : ∀ {n : ℕ}, n ≠ 0 → n.nthRoot 0 = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.fan_mk_proj : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : β → C} (P : C) (p : (b : β) → P ⟶ f b),
  (CategoryTheory.Limits.Fan.mk P p).proj = p
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- Every `BinaryFan` is isomorphic to an application of `BinaryFan.mk`.  -/
CategoryTheory.Limits.isoBinaryCofanMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → (c : CategoryTheory.Limits.BinaryCofan X Y) → c ≅ CategoryTheory.Limits.BinaryCofan.mk c.inl c.inr
-- Mathlib.CategoryTheory.SmallRepresentatives
CategoryTheory.CoreSmallCategoryOfSet.smallCategoryOfSet_obj : ∀ {Ω : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (h : CategoryTheory.CoreSmallCategoryOfSet Ω C),
  h.smallCategoryOfSet.obj = h.obj