mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.ofRestrict_invApp_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : AlgebraicGeometry.SheafedSpace C) {Y : TopCat}
  {f : Y ⟶ TopCat.of ↑↑X.toPresheafedSpace} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f))
  (U : TopologicalSpace.Opens ↑↑(X.restrict h).toPresheafedSpace) {F : C → C → Type uF} {carrier : C → Type w_1}
  {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst_1 : CategoryTheory.ConcreteCategory C F]
  (x : carrier ((X.restrict h).presheaf.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp (X.ofRestrict h) U)) x =
    (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.CategoryStruct.id ((X.restrict h).presheaf.obj (Opposite.op U))))
      x
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get_eq_get! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {a : α}
  {h : a ∈ t}, t.get a h = t.get! a
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.opCoproductIsoProduct_hom_comp_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct Z] (i : α),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opCoproductIsoProduct Z).hom
      (CategoryTheory.Limits.Pi.π (fun x => Opposite.op (Z x)) i) =
    (CategoryTheory.Limits.Sigma.ι Z i).op
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanImportKind : Type
-- Mathlib.Analysis.Distribution.Sobolev
TemperedDistribution.besselPotential.congr_simp : ∀ (E : Type u_1) (F : Type u_2) [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : NormedSpace ℂ F] (s s_1 : ℝ),
  s = s_1 → TemperedDistribution.besselPotential E F s = TemperedDistribution.besselPotential E F s_1
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.sz : ∀ {α : Type u_1} [inst : Preorder α] {lo : WithBot α} {t : Ordnode α} {hi : WithTop α}, Ordnode.Valid' lo t hi → t.Sized
-- Init.Data.List.MinMaxOn
List.maxOn.congr_simp : ∀ {β : Type u_1} {α : Type u_2} [i : LE β] {inst : DecidableLE β} [inst_1 : DecidableLE β] (f f_1 : α → β),
  f = f_1 → ∀ (l l_1 : List α) (e_l : l = l_1) (h : l ≠ []), List.maxOn f l h = List.maxOn f_1 l_1 ⋯
-- Init.Data.Vector.Attach
Vector.pmap_empty : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} {f : (a : α) → P a → β}, Vector.pmap f #v[] ⋯ = #v[]
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RioSliceData.mk.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : SizeOf α] [inst_2 : (a : α) → SizeOf (β a)]
  (treeMap : Std.DTreeMap.Internal.Impl α β) (range : Std.Rio α),
  sizeOf { treeMap := treeMap, range := range } = 1 + sizeOf treeMap + sizeOf range
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
AlgebraicIndependent.to_subtype_range' : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  AlgebraicIndependent R x → ∀ {t : Set A}, Set.range x = t → AlgebraicIndependent R Subtype.val
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.restrict_mass : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (A : Set Ω), (μ.restrict A).mass = μ A
-- Mathlib.Algebra.Group.Units.Defs
/-- The element of the additive group of additive units, corresponding to an element of
an additive monoid which is an additive unit. As opposed to `IsAddUnit.addUnit`, the negation is
computable and comes from the negation on `α`. This is useful to transfer properties of negation
in `AddUnits α` to `α`. See also `toAddUnits`.  -/
IsAddUnit.addUnit' : {α : Type u} → [inst : SubtractionMonoid α] → {a : α} → IsAddUnit a → AddUnits α
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_inter_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α}, k ∈ m₂ → Std.DHashMap.Const.get? (m₁.inter m₂) k = Std.DHashMap.Const.get? m₁ k
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.findSomeM?.eq_def : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)) (x : List α),
  List.findSomeM? f x =
    match x with
    | [] => pure none
    | a :: as => do
      let __do_lift ← f a
      match __do_lift with
        | some b => pure (some b)
        | none => List.findSomeM? f as
-- Mathlib.Data.Finset.Sort
/-- Given a finset `s` of cardinality `k` in a linear order `α`, the map `orderIsoOfFin s h`
is the increasing bijection between `Fin k` and `s` as an `OrderIso`. Here, `h` is a proof that
the cardinality of `s` is `k`. We use this instead of an iso `Fin s.card ≃o s` to avoid
casting issues in further uses of this function.  -/
Finset.orderIsoOfFin : {α : Type u_1} → [inst : LinearOrder α] → (s : Finset α) → {k : ℕ} → s.card = k → Fin k ≃o ↥s
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
/-- A category `C` has the `w`-IPC property it satisfies the IPC-property for every `ι : Type w`.  -/
CategoryTheory.Limits.IsIPC : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Limits.HasProducts C] →
      [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, u_3, v_1, u_1} C] → Prop
-- Mathlib.NumberTheory.LSeries.Basic
LSeries.term_of_ne_zero : ∀ {n : ℕ}, n ≠ 0 → ∀ (f : ℕ → ℂ) (s : ℂ), LSeries.term f s n = f n / ↑n ^ s
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- The seminorm is invariant under negation.  -/
NonarchAddGroupSeminormClass.map_neg_eq_map' : ∀ {F : Type u_6} {α : outParam (Type u_7)} {inst : AddGroup α} {inst_1 : FunLike F α ℝ}
  [self : NonarchAddGroupSeminormClass F α] (f : F) (a : α), f (-a) = f a
-- Init.MetaTypes
Lean.Meta.EtaStructMode.none.sizeOf_spec : sizeOf Lean.Meta.EtaStructMode.none = 1
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.projectiveDimension_eq_zero_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C),
  CategoryTheory.projectiveDimension X = 0 ↔ CategoryTheory.Projective X ∧ ¬CategoryTheory.Limits.IsZero X
-- Mathlib.CategoryTheory.ObjectProperty.Orthogonal
/-- In a category with zero morphisms, the right orthogonal of a property of objects `P`
is the property of objects `Y` such that any map `X ⟶ Y` vanishes when `P X` holds.  -/
CategoryTheory.ObjectProperty.rightOrthogonal : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasZeroMorphisms C] → CategoryTheory.ObjectProperty C → CategoryTheory.ObjectProperty C
-- Init.Data.List.TakeDrop
List.dropWhile_cons_of_neg : ∀ {α : Type u_1} {p : α → Bool} {a : α} {l : List α}, ¬p a = true → List.dropWhile p (a :: l) = a :: l
-- Mathlib.Logic.Function.Iterate
Function.iterate_id : ∀ {α : Type u} (n : ℕ), id^[n] = id
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- shift right arithmetically by another BitVec expression. For constant shifts there exists a `BVUnop`.
 -/
Std.Tactic.BVDecide.BVExpr.arithShiftRight : {m n : ℕ} → Std.Tactic.BVDecide.BVExpr m → Std.Tactic.BVDecide.BVExpr n → Std.Tactic.BVDecide.BVExpr m
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.foldl_toList : ∀ {m : Type w → Type u_1} {γ α β : Type w} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β}
  {f : γ → β → γ} {init : γ}, (fun x => List.foldl f init x) <$> it.toList = Std.IterM.fold f init it
-- Mathlib.Data.Sigma.Order
Sigma.instLT_mathlib : {ι : Type u_1} → {α : ι → Type u_2} → [(i : ι) → LT (α i)] → LT ((i : ι) × α i)
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.compl_bot : ∀ {α : Type u_1} [inst : LE α], ⊥.compl = ⊥
-- Mathlib.Data.QPF.Univariate.Basic
QPF.mk : {F : Type u → Type v} →
  [toFunctor : Functor F] →
    (P : PFunctor.{u, u'}) →
      (abs : {α : Type u} → ↑P α → F α) →
        (repr : {α : Type u} → F α → ↑P α) →
          (∀ {α : Type u} (x : F α), abs (repr x) = x) →
            (∀ {α β : Type u} (f : α → β) (p : ↑P α), abs (P.map f p) = f <$> abs p) → QPF F
-- Qq.Macro
Qq.Impl.UnquoteState.mk : List (Lean.Expr × Qq.Impl.MVarSynth) →
  Std.HashMap Lean.Expr Lean.Level →
    Std.HashMap Lean.Expr Lean.Expr →
      Lean.LocalContext →
        Std.HashMap Lean.Expr Qq.Impl.ExprBackSubstResult →
          Std.HashMap Lean.Level Lean.Expr → Array Lean.FVarId → List Lean.Name → Bool → Qq.Impl.UnquoteState
-- Lean.Meta.CompletionName
/-- Return true if completion is allowed for name.
 -/
Lean.Meta.allowCompletion : Lean.Environment → Lean.Name → Bool
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.FunctionTheorems.mk : Std.TreeMap Lean.Name (Std.TreeMap Lean.Name (Array Mathlib.Meta.FunProp.FunctionTheorem) Lean.Name.quickCmp)
    Lean.Name.quickCmp →
  Mathlib.Meta.FunProp.FunctionTheorems
-- Mathlib.Tactic.Linarith.Datatypes
/-- Given a goal, and a list of hypotheses,
produce a list of pairs (consisting of a goal and list of hypotheses).  -/
Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor.transform : Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor →
  Lean.MVarId → List Lean.Expr → Lean.MetaM (List Mathlib.Tactic.Linarith.Branch)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.neg.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Linear.DiseqCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.neg c) = 1 + sizeOf c
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.rangeRestrict.eq_1 : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N),
  f.rangeRestrict = f.codRestrict f.range ⋯
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.IsLocalizationMap.map_addUnits : ∀ {M : Type u_1} [inst : AddCommMonoid M] {N : Type u_2} [inst_1 : AddCommMonoid N] {S : AddSubmonoid M} {f : M → N},
  S.IsLocalizationMap f → ∀ (y : ↥S), IsAddUnit (f ↑y)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_modify_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF → ∀ {k : α} [inst_1 : Inhabited (β k)] {f : β k → β k}, (t.modify k f).get! k = (Option.map f (t.get? k)).get!
-- Mathlib.Tactic.Order.ToInt
Mathlib.Tactic.Order.ToInt.toInt_eq_toInt : ∀ {α : Type u_1} [inst : LinearOrder α] {n : ℕ} (val : Fin n → α) (i j : Fin n),
  Mathlib.Tactic.Order.ToInt.toInt val i = Mathlib.Tactic.Order.ToInt.toInt val j ↔ val i = val j
-- Std.Time.DateTime.WallTime
_private.Std.Time.DateTime.WallTime.0.Std.Time.WallTime.mk.sizeOf_spec : ∀ (val : Std.Time.Duration), sizeOf { val := val } = 1 + sizeOf val
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.mulActionHom_singleton_bijective : ∀ (G : Type u_1) [inst : Group G] (α : Type u_2) [inst_1 : MulAction G α] [inst_2 : DecidableEq α],
  Function.Bijective ⇑(Set.powersetCard.mulActionHom_singleton G α)
-- Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
/-- The naturality for the horizontal composition.  -/
Mathlib.Tactic.BicategoryLike.MonadNormalizeNaturality.mkNaturalityHorizontalComp : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadNormalizeNaturality m] →
    Mathlib.Tactic.BicategoryLike.NormalizedHom →
      Mathlib.Tactic.BicategoryLike.NormalizedHom →
        Mathlib.Tactic.BicategoryLike.NormalizedHom →
          Mathlib.Tactic.BicategoryLike.Mor₁ →
            Mathlib.Tactic.BicategoryLike.Mor₁ →
              Mathlib.Tactic.BicategoryLike.Mor₁ →
                Mathlib.Tactic.BicategoryLike.Mor₁ →
                  Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                    Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                      Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                        Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                          Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                            Mathlib.Tactic.BicategoryLike.Mor₂Iso → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
/-- A variant of `ProjRestrict` with domain of the form `π C K`  -/
Profinite.NobelingProof.ProjRestricts : {I : Type u} →
  (C : Set (I → Bool)) →
    {J K : I → Prop} →
      [inst : (i : I) → Decidable (J i)] →
        [inst_1 : (i : I) → Decidable (K i)] →
          (∀ (i : I), J i → K i) → ↑(Profinite.NobelingProof.π C K) → ↑(Profinite.NobelingProof.π C J)
-- Lean.Linter.Init
Lean.Linter.LinterSetsState.merged : Lean.Linter.LinterSetsState → Lean.Linter.LinterSets
-- Mathlib.Data.Set.Prod
Set.pi_eq_empty_iff' : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t : (i : ι) → Set (α i)} [∀ (i : ι), Nonempty (α i)],
  s.pi t = ∅ ↔ ∃ i ∈ s, t i = ∅
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork_inverse_obj_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.Limits.MulticospanShape)
  [inst_1 : Unique J.L] [inst_2 : Unique J.R] {X Y : C} (f g : X ⟶ Y) (c : CategoryTheory.Limits.Fork f g) (a : J.L),
  ((CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork J f g).inverse.obj c).ι a = c.ι
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.vadd_sub_zero : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {X : Type u_2}
  [inst_2 : AddAction R X] {p : R} {r : X} {s : ↥S}, (p -ₒ s) +ᵥ r -ₒ 0 = (p +ᵥ r) -ₒ s
-- Mathlib.Order.OmegaCompletePartialOrder
/-- An example of a `Chain` constructed from an ordered pair.  -/
OmegaCompletePartialOrder.Chain.pair : {α : Type u_2} → [inst : Preorder α] → (a b : α) → a ≤ b → OmegaCompletePartialOrder.Chain α
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k a : α} {fallback : β a} {v : β k},
      (t.insert k v).getD a fallback = if h : cmp k a = Ordering.eq then cast ⋯ v else t.getD a fallback
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
CategoryTheory.bicategoricalIsoComp.eq_1 : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g h i : a ⟶ b}
  [inst_1 : CategoryTheory.BicategoricalCoherence g h] (η : f ≅ g) (θ : h ≅ i),
  CategoryTheory.bicategoricalIsoComp η θ = η ≪≫ CategoryTheory.BicategoricalCoherence.iso ≪≫ θ
-- Mathlib.Topology.DerivedSet
closure_eq_self_union_derivedSet : ∀ {X : Type u_1} [inst : TopologicalSpace X] (A : Set X), closure A = A ∪ derivedSet A
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_mul : ∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {p q : Polynomial R}
  (x : A), (Polynomial.aeval x) (p * q) = (Polynomial.aeval x) p * (Polynomial.aeval x) q
-- Lean.Meta.CongrTheorems
/-- Returns `true` if `kinds` contains `.cast` or `.subsingletonInst`  -/
_private.Lean.Meta.CongrTheorems.0.Lean.Meta.hasCastLike : Array Lean.Meta.CongrArgKind → Bool
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.rightHomologyMap'_congr : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂)
  (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData),
  CategoryTheory.ShortComplex.rightHomologyMap' φ₁ h₁ h₂ = CategoryTheory.ShortComplex.rightHomologyMap' φ₂ h₁ h₂
-- Mathlib.CategoryTheory.Opposites
/-- The "unopposite" of a natural transformation.  -/
CategoryTheory.NatTrans.unop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} → (F ⟶ G) → (G.unop ⟶ F.unop)
-- Lean.Message
/-- A naming context is the information needed to shorten names in pretty printing.

It gives the current namespace and the list of open declarations.
 -/
Lean.NamingContext : Type
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
/-- Populate a `context` object for evaluating `e`.  -/
Mathlib.Tactic.Monoidal.mkContext? : Lean.Expr → Lean.MetaM (Option Mathlib.Tactic.Monoidal.Context)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_filter_containsKey_of_containsKey_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₁ = false →
      Std.Internal.List.getKey? k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) = none
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.isFlat_closure : ∀ {α : Type u_2} {M : Matroid α} (X : Set α), M.IsFlat (M.closure X)
-- Init.Prelude
/-- If `n ≤ m`, then `n ≤ m + 1`.  -/
Nat.le.step : ∀ {n m : ℕ}, n.le m → n.le m.succ
-- Mathlib.Order.Iterate
/-- If `f` is a strictly antitone map and `f x < x` at some point `x`, then the iterates `f^[n] x`
form a strictly antitone sequence.  -/
StrictMono.strictAnti_iterate_of_map_lt : ∀ {α : Type u_1} [inst : Preorder α] {f : α → α} {x : α}, StrictMono f → f x < x → StrictAnti fun n => f^[n] x
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
/-- A normal monomorphism is a morphism which is the kernel of some morphism.  -/
CategoryTheory.NormalMono.w : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {X Y : C}
  {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} {f : X ⟶ Y} [self : CategoryTheory.NormalMono f],
  CategoryTheory.CategoryStruct.comp f CategoryTheory.NormalMono.g = 0
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.parallelFamily_obj_one : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : J → (X ⟶ Y)),
  (CategoryTheory.Limits.parallelFamily f).obj CategoryTheory.Limits.WalkingParallelFamily.one = Y
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem_toList_roc : ∀ {m n i : ℕ} (_h : i < (m<...=n).toList.length), (m<...=n).toList[i] = m + 1 + i
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
/-- Polynomial whose roots are the fixed points of `g` considered as a Möbius transformation.

See `Matrix.GeneralLinearGroup.fixpointPolynomial_aeval_eq_zero_iff`.  -/
Matrix.GeneralLinearGroup.fixpointPolynomial : {R : Type u_1} → [inst : CommRing R] → GL (Fin 2) R → Polynomial R
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mapIso_counitIso_hom_app_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T T' : D} {S : CategoryTheory.Functor C D} (i : T ≅ T')
  (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T')),
  ((CategoryTheory.CostructuredArrow.mapIso i).counitIso.hom.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LitValue.uint16 : UInt16 → Lean.Compiler.LCNF.LitValue
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.addValuation_apply : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : CommRing R] [inst_2 : IsStrictOrderedRing R] (a : R),
  (ArchimedeanClass.addValuation R) a = ArchimedeanClass.mk a
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.add_union : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {s t₁ t₂ : Finset α}, s + (t₁ ∪ t₂) = s + t₁ ∪ (s + t₂)
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.Hom.mk.sizeOf_spec : ∀ {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] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] {F G : CategoryTheory.SingleFunctors C D A} [inst_4 : SizeOf C]
  [inst_5 : SizeOf D] [inst_6 : SizeOf A] (hom : (a : A) → F.functor a ⟶ G.functor a)
  (comm :
    autoParam
      (∀ (n a a' : A) (ha' : n + a = a'),
        CategoryTheory.CategoryStruct.comp (F.shiftIso n a a' ha').hom (hom a) =
          CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Functor.whiskerRight (hom a') (CategoryTheory.shiftFunctor D n))
            (G.shiftIso n a a' ha').hom)
      CategoryTheory.SingleFunctors.Hom.comm._autoParam),
  sizeOf { hom := hom, comm := comm } = 1
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
IsUniformGroup.cauchy_map_iff_tendsto : ∀ {ι : Type u_3} {G : Type u_4} [inst : Group G] [inst_1 : UniformSpace G] [IsUniformGroup G] (𝓕 : Filter ι)
  (f : ι → G), Cauchy (Filter.map f 𝓕) ↔ 𝓕.NeBot ∧ Filter.Tendsto (fun p => f p.1 / f p.2) (𝓕 ×ˢ 𝓕) (nhds 1)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.keys_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool},
  (Std.DTreeMap.filter f t).keys =
    (List.filter
        (fun x =>
          match x with
          | ⟨x, h'⟩ => f x (t.get x ⋯))
        t.keys.attach).unattach
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
_private.Mathlib.LinearAlgebra.PiTensorProduct.Basic.0.PiTensorProduct.map_add_smul_aux : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {t : ι → Type u_11} [inst_3 : (i : ι) → AddCommMonoid (t i)]
  [inst_4 : (i : ι) → Module R (t i)] (f : (i : ι) → s i →ₗ[R] t i) [inst_5 : DecidableEq ι] (i : ι) (x : (i : ι) → s i)
  (u : s i →ₗ[R] t i), (fun j => (Function.update f i u j) (x j)) = Function.update (fun j => (f j) (x j)) i (u (x i))
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.maximal_connected_induce_supp : ∀ {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent),
  Maximal (fun x => (SimpleGraph.induce x G).Connected) C.supp
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.divCoeffs.injEq : ∀ (c c_1 : Lean.Meta.Grind.Arith.Cutsat.EqCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.divCoeffs c = Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.divCoeffs c_1) =
    (c = c_1)
-- Mathlib.Algebra.Category.ModuleCat.ExteriorPower
ModuleCat.exteriorPower.iso₀_hom_naturality : ∀ {R : Type u} [inst : CommRing R] {M N : ModuleCat R} (f : M ⟶ N),
  CategoryTheory.CategoryStruct.comp (ModuleCat.exteriorPower.map f 0) (ModuleCat.exteriorPower.iso₀ N).hom =
    (ModuleCat.exteriorPower.iso₀ M).hom
-- Mathlib.CategoryTheory.Limits.ExactFunctor
/-- An exact functor is in particular a functor.  -/
CategoryTheory.ExactFunctor.forget : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor (C ⥤ₑ D) (CategoryTheory.Functor C D)
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxc.Iterator.instIteratorAccess : {α : Type u} →
  [inst : Std.PRange.UpwardEnumerable α] →
    [inst_1 : LE α] →
      [inst_2 : DecidableLE α] →
        [Std.PRange.LawfulUpwardEnumerable α] →
          [Std.PRange.LawfulUpwardEnumerableLE α] → Std.IteratorAccess (Std.Rxc.Iterator α) Id
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.ordCompare_minKeyD_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] {t : Std.DTreeMap α (fun x => β) compare} {k : α}
  {f : β → β} {fallback : α},
  compare ((Std.DTreeMap.Const.modify t k f).minKeyD fallback) (t.minKeyD fallback) = Ordering.eq
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instAddLeftCancelSemigroup : {α : Type u_1} → [AddLeftCancelSemigroup α] → AddLeftCancelSemigroup αᵒᵈ
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicofork.isoOfπ_inv_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  {I : CategoryTheory.Limits.MultispanIndex J C} (t : CategoryTheory.Limits.Multicofork I),
  t.isoOfπ.inv.hom = CategoryTheory.CategoryStruct.id t.pt
-- Init.Data.Int.Order
Int.negSucc_not_nonneg : ∀ (n : ℕ), 0 ≤ Int.negSucc n ↔ False