mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.insertMany_list_singleton : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β k}, m.insertMany [⟨k, v⟩] = m.insert k v
-- Mathlib.CategoryTheory.Monoidal.Opposite
/-- The type of objects of the opposite (or "reverse") monoidal category.
Use the notation `Cᴹᵒᵖ`.  -/
CategoryTheory.MonoidalOpposite.«term_ᴹᵒᵖ» : Lean.TrailingParserDescr
-- Mathlib.GroupTheory.Subgroup.Centralizer
Subgroup.centralizer_univ : ∀ {G : Type u_1} [inst : Group G], Subgroup.centralizer Set.univ = Subgroup.center G
-- Mathlib.Probability.StrongLaw
ProbabilityTheory.tsum_prob_mem_Ioi_lt_top : ∀ {Ω : Type u_1} [inst : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
  {X : Ω → ℝ},
  MeasureTheory.Integrable X MeasureTheory.volume → 0 ≤ X → ∑' (j : ℕ), MeasureTheory.volume {ω | X ω ∈ Set.Ioi ↑j} < ⊤
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- **Class formula** : let `G` be a group acting on `X` and let `φ` be a function mapping each
orbit of `X` under this action (that is, each element of the quotient of `G` by the relation
`orbitRel G X`) to an element in this orbit. We provide a  (noncomputable) bijection between `X`
and the disjoint union of `G/Stab(φ(ω))` over all orbits `ω : Ω`. In most cases you'll want `φ`
to be `Quotient.out`, so we provide `MulAction.selfEquivSigmaOrbitsQuotientStabilizer'` as a
special case.  -/
MulAction.selfEquivSigmaOrbitsQuotientStabilizer' : (G : Type u) →
  (X : Type v) →
    [inst : Group G] →
      [inst_1 : MulAction G X] →
        {φ : Quotient (MulAction.orbitRel G X) → X} →
          Function.LeftInverse Quotient.mk'' φ →
            X ≃ (ω : Quotient (MulAction.orbitRel G X)) × G ⧸ MulAction.stabilizer G (φ ω)
-- Lean.Meta.Tactic.SolveByElim
/-- Run `elabTerm`.  -/
_private.Lean.Meta.Tactic.SolveByElim.0.Lean.Meta.SolveByElim.mkAssumptionSet.elab' : Lean.Term → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Data.Finset.Dedup
Multiset.toFinset_val : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α), s.toFinset.val = s.dedup
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.size_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (t.erase k).size = if t.contains k = true then t.size - 1 else t.size
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_map : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → γ}, m.WF → (Std.HashMap.Raw.map f m).isEmpty = m.isEmpty
-- Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C},
  (∀ {X Y : C} (x : X ≅ Y), P X → P Y) → P.IsClosedUnderIsomorphisms
-- Init.Prelude
/-- Get the current value of the `ref`  -/
Lean.MonadRef.getRef : {m : Type → Type} → [self : Lean.MonadRef m] → m Lean.Syntax
-- Init.Data.Stream
Std.instStreamProd : {ρ : Type u_1} →
  {α : Type u_2} → {γ : Type u_3} → {β : Type u_4} → [Std.Stream ρ α] → [Std.Stream γ β] → Std.Stream (ρ × γ) (α × β)
-- Init.Data.UInt.Bitwise
UInt32.and_comm : ∀ (a b : UInt32), a &&& b = b &&& a
-- Mathlib.Algebra.Ring.NegOnePow
Int.negOnePow_succ : ∀ (n : ℤ), (n + 1).negOnePow = -n.negOnePow
-- Mathlib.Data.ZMod.Basic
ZMod.cast_add_eq_ite : ∀ {n : ℕ} (a b : ZMod n), (a + b).cast = if ↑n ≤ a.cast + b.cast then a.cast + b.cast - ↑n else a.cast + b.cast
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.prod_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) (a : C),
  (CategoryTheory.FunctorToTypes.prod F G).obj a = (F.obj a × G.obj a)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_alter : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h : t.WF) {k k' : α} {f : Option β → Option β} {hc : k' ∈ (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl},
  Std.DTreeMap.Internal.Impl.Const.get (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl k' hc =
    if heq : compare k k' = Ordering.eq then (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).get ⋯
    else Std.DTreeMap.Internal.Impl.Const.get t k' ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPullback f g] {Z_1 : C} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry f g).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst g f) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.op_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.HomologyData), h.op.left = h.right.op
-- Mathlib.Order.SuccPred.Basic
/-- Not to be confused with `WithTop.pred_coe`, which is about `WithTop.pred`.  -/
WithTop.orderPred_coe : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderTop α] [inst_2 : PredOrder α] (a : α),
  Order.pred ↑a = ↑(Order.pred a)
-- Mathlib.Analysis.Calculus.FDeriv.Prod
differentiableAt_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {ι : Type u_6} {F' : ι → Type u_7}
  [inst_1 : (i : ι) → NormedAddCommGroup (F' i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (F' i)] (i : ι) (f : (i : ι) → F' i),
  DifferentiableAt 𝕜 (fun f => f i) f
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.monoCLM.eq_1 : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω₁ Ω₂ : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] {n₁ n₂ : ℕ∞} [inst_6 : Algebra ℝ 𝕜]
  [inst_7 : IsScalarTower ℝ 𝕜 F],
  TestFunction.monoCLM 𝕜 =
    TestFunction.limitCLM 𝕜
      (fun f =>
        if h : n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂ then { toFun := ⇑f, contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ }
        else 0)
      (fun K K_sub_Ω₁ =>
        if h : n₂ ≤ n₁ ∧ Ω₁ ≤ Ω₂ then TestFunction.ofSupportedInCLM 𝕜 ⋯ ∘SL ContDiffMapSupportedIn.monoCLM 𝕜 else 0)
      ⋯
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.lineMap_vsub_right : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1] (p₀ p₁ : P1) (c : k), (AffineMap.lineMap p₀ p₁) c -ᵥ p₁ = (1 - c) • (p₀ -ᵥ p₁)
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.val_unitsTypeEquivIsUnitSubmonoid_symm_apply : ∀ {M : Type u_4} [inst : Monoid M] (x : ↥(IsUnit.submonoid M)), ↑(Submonoid.unitsTypeEquivIsUnitSubmonoid.symm x) = ↑x
-- Mathlib.GroupTheory.Nilpotent
AddGroup.IsVirtuallyNilpotent.eq_1 : ∀ (G : Type u_1) [inst : AddGroup G], AddGroup.IsVirtuallyNilpotent G = ∃ N, AddGroup.IsNilpotent ↥N ∧ N.FiniteIndex
-- Mathlib.CategoryTheory.Sites.InducedTopology
CategoryTheory.Functor.inducedTopology_eq_of_iso : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {K : CategoryTheory.GrothendieckTopology D} {F G : CategoryTheory.Functor C D} (e : F ≅ G),
  F.inducedTopology K = G.inducedTopology K
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.instSymmetricCategory : CategoryTheory.SymmetricCategory SFinKer
-- Mathlib.Computability.RecursiveIn
Primrec.computableIn : ∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {f : α → σ} {O : Set (ℕ →. ℕ)},
  Primrec f → ComputableIn O f
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.term_atom : ∀ {α : Type u_1} [inst : AddCommMonoid α] (x : α), x = Mathlib.Tactic.Abel.term 1 x 0
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.mk : ∀ {R : Type u} {M : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Function.Bijective ⇑(contractLeft R M) → Module.Invertible R M
-- Mathlib.Algebra.Order.ToIntervalMod
self_sub_toIcoMod_eq_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R), b - toIcoMod hp a b = ↑(toIcoDiv hp a b) * p
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec64_mod : ∀ {a b : ISize} (h : System.Platform.numBits = 64), (a % b).toBitVec64 h = (a.toBitVec64 h).srem (b.toBitVec64 h)
-- Init.Data.UInt.Lemmas
UInt16.toBitVec_toUInt32 : ∀ (n : UInt16), n.toUInt32.toBitVec = BitVec.setWidth 32 n.toBitVec
-- Lean.Data.Trie
/-- Inserts a value at the given key `s`, overriding an existing value if present.  -/
Lean.Data.Trie.insert : {α : Type} → Lean.Data.Trie α → String → α → Lean.Data.Trie α
-- Lean.Server.Rpc.Basic
Lean.Server.ReferencedObject.rc : Lean.Server.ReferencedObject → ℕ
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
/-- not marked as an instance because it would be a bad one in general, but it can
be useful when working with `ContinuousMapZero` and the non-unital continuous
functional calculus.  -/
Set.zeroOfFactMem : {X : Type u_4} → [inst : Zero X] → (s : Set X) → [Fact (0 ∈ s)] → Zero ↑s
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
nullMeasurableSet_Icc : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : Preorder α]
  {a b : α} {μ : MeasureTheory.Measure α} [OrderClosedTopology α], MeasureTheory.NullMeasurableSet (Set.Icc a b) μ
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.le_of_eq_of_le : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {f g h : CauSeq α abs},
  f ≈ g → g ≤ h → f ≤ h
-- Mathlib.Order.SuccPred.Basic
Order.Ico_pred_left : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α},
  Order.pred b < a → Set.Ico (Order.pred b) a = insert (Order.pred b) (Set.Ico b a)
-- Mathlib.Analysis.InnerProductSpace.Projection.Minimal
_private.Mathlib.Analysis.InnerProductSpace.Projection.Minimal.0.«term⟪_,_⟫» : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLinAlgEquiv'_one : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n],
  Matrix.toLinAlgEquiv' 1 = LinearMap.id
-- Mathlib.Order.Lattice
sup_eq_maxDefault : ∀ {α : Type u} [inst : SemilatticeSup α] [inst_1 : DecidableLE α] [Std.Total fun x1 x2 => x1 ≤ x2],
  (fun x1 x2 => x1 ⊔ x2) = maxDefault
-- Init.Control.Lawful.Basic
Id.instLawfulMonad : LawfulMonad Id
-- Init.Data.Repr
instReprUInt16 : Repr UInt16
-- Mathlib.CategoryTheory.Comma.Arrow
/-- The functor `(C ⥤ D) ⥤ (Arrow C ⥤ Arrow D)` which sends
a functor `F : C ⥤ D` to `F.mapArrow`.  -/
CategoryTheory.Functor.mapArrowFunctor : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor (CategoryTheory.Functor C D)
          (CategoryTheory.Functor (CategoryTheory.Arrow C) (CategoryTheory.Arrow D))
-- Std.Data.Internal.List.Associative
Std.Internal.List.self_le_maxKey?_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  {k kmi : α} {v : β k} {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l),
  (Std.Internal.List.maxKey? (Std.Internal.List.insertEntryIfNew k v l)).get ⋯ = kmi → (compare k kmi).isLE = true
-- Lean.Data.Lsp.Basic
Lean.Lsp.DocumentFilter.scheme? : Lean.Lsp.DocumentFilter → Option String
-- Mathlib.Topology.Compactness.Lindelof
/-- For every open cover of a Lindelöf set, there exists a countable subcover.  -/
IsLindelof.elim_countable_subcover : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {ι : Type v},
  IsLindelof s → ∀ (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_add_le : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a b : R),
  Int.fract (a + b) ≤ Int.fract a + Int.fract b
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.eraseLead_degree_le : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f.eraseLead.degree ≤ f.degree
-- Mathlib.Algebra.Ring.Equiv
/-- Reinterpret a ring equivalence as a non-unital ring homomorphism.  -/
RingEquiv.toNonUnitalRingHom : {R : Type u_4} →
  {S : Type u_5} → [inst : NonUnitalNonAssocSemiring R] → [inst_1 : NonUnitalNonAssocSemiring S] → R ≃+* S → R →ₙ+* S
-- Mathlib.Data.List.MinMax
/-- `argmin f l` returns `some a`, where `f a` is minimal among the elements of `l`, in the sense
that there is no `b ∈ l` with `f b < f a`. If `a`, `b` are such that `f a = f b`, it returns
whichever of `a` or `b` comes first in the list. `argmin f [] = none`.  -/
List.argmin : {α : Type u_1} → {β : Type u_2} → [inst : Preorder β] → [DecidableLT β] → (α → β) → List α → Option α
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.liftIoc_eq_liftIco : ∀ {𝕜 : Type u_1} {B : Type u_2} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  {p a : 𝕜} [hp : Fact (0 < p)] [inst_3 : Archimedean 𝕜] {f : 𝕜 → B},
  f a = f (a + p) → AddCircle.liftIoc p a f = AddCircle.liftIco p a f
-- Mathlib.SetTheory.Cardinal.Free
Cardinal.mk_freeMonoid : ∀ (α : Type u) [Nonempty α], Cardinal.mk (FreeMonoid α) = max (Cardinal.mk α) Cardinal.aleph0
-- Mathlib.Topology.MetricSpace.Polish
/-- A closed subset of a Polish space is also Polish.  -/
IsClosed.polishSpace : ∀ {α : Type u_1} [inst : TopologicalSpace α] [PolishSpace α] {s : Set α}, IsClosed s → PolishSpace ↑s
-- Std.Data.TreeMap.Raw.Slice
Std.TreeMap.Raw.toList_rio : ∀ {α : Type u} {β : Type v} (cmp : autoParam (α → α → Ordering) Std.TreeMap.Raw.toList_rio._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeMap.Raw α β cmp},
  t.WF →
    ∀ {bound : α},
      Std.Slice.toList (Std.Rio.Sliceable.mkSlice t *...bound) = List.filter (fun e => (cmp e.1 bound).isLT) t.toList
-- Init.Data.List.Lemmas
/-- Two lists of sublists are equal iff their flattens coincide, as well as the lengths of the
sublists.  -/
List.eq_iff_flatten_eq : ∀ {α : Type u_1} {L L' : List (List α)},
  L = L' ↔ L.flatten = L'.flatten ∧ List.map List.length L = List.map List.length L'
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
/-- In a non-unital semiring `R`, an element `x : R` satisfies `IsQuasiregular` if it is a unit
under the monoid operation `fun x y ↦ y + x + x * y`.  -/
IsQuasiregular : {R : Type u_1} → [NonUnitalSemiring R] → R → Prop
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.isLongestRevMatchAt_iff_splits : ∀ {pat : String} {s : String.Slice} {pos₁ pos₂ : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAt pat pos₁ pos₂ ↔
    ∃ t₁ t₂, pos₁.Splits t₁ (pat ++ t₂) ∧ pos₂.Splits (t₁ ++ pat) t₂
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.ι_π_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] [inst_3 : CategoryTheory.Mono f]
  (n₀ : ℤ) [inst_4 : K.IsStrictlyGE (n₀ + 1)] [inst_5 : L.IsStrictlyGE (n₀ + 1)] {Z : CochainComplex C ℤ} (h : L ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.ι✝ f n₀)
      (CategoryTheory.CategoryStruct.comp (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.π✝ f n₀) h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.CategoryTheory.Action.Monoidal
/-- If `V` is right rigid, so is `Action V G`.  -/
Action.instRightRigidCategory : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      (H : Type u_3) →
        [inst_2 : Group H] → [CategoryTheory.RightRigidCategory V] → CategoryTheory.RightRigidCategory (Action V H)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_eq_some_get!_of_contains : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {a : α} [inst_1 : Inhabited (β a)], Std.DTreeMap.Internal.Impl.contains a t = true → t.get? a = some (t.get! a)
-- Mathlib.Data.Finsupp.Order
Finsupp.mapDomain_mono : ∀ {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  {f : ι → κ}, Monotone (Finsupp.mapDomain f)
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.coe_comap : ∀ {α : Type u_2} {β : Type u_3} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β] (L : BooleanSubalgebra β)
  (f : BoundedLatticeHom α β), ↑(BooleanSubalgebra.comap f L) = ⇑f ⁻¹' ↑L
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SolverTerms.brecOn.eq : ∀ {motive : Lean.Meta.Grind.SolverTerms → Sort u} (t : Lean.Meta.Grind.SolverTerms)
  (F_1 : (t : Lean.Meta.Grind.SolverTerms) → Lean.Meta.Grind.SolverTerms.below t → motive t),
  Lean.Meta.Grind.SolverTerms.brecOn t F_1 = F_1 t (Lean.Meta.Grind.SolverTerms.brecOn.go t F_1).2
-- Batteries.Data.MLList.Basic
MLList.instForInOfMonadOfMonadLiftT : {m : Type u_1 → Type u_1} →
  {n : Type u_1 → Type u_2} → {α : Type u_1} → [Monad m] → [Monad n] → [MonadLiftT m n] → ForIn n (MLList m α) α
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.leftOp_full : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C Dᵒᵖ} [F.Full], F.leftOp.Full
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ : B} (f : b₀ ⟶ b₁),
  (F.mapComp' f (CategoryTheory.CategoryStruct.id b₁) f ⋯).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (F.map f)).inv
      (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapId b₁).inv)
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
Lean.Elab.Structural.instInhabitedIndGroupInst : Inhabited Lean.Elab.Structural.IndGroupInst
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
/-- The isomorphism
`DerivedCategory.singleFunctors C ≅ (HomotopyCategory.singleFunctors C).postcomp Qh` given
by the definition of `DerivedCategory.singleFunctors`.  -/
DerivedCategory.singleFunctorsPostcompQhIso : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] →
        DerivedCategory.singleFunctors C ≅ (HomotopyCategory.singleFunctors C).postcomp DerivedCategory.Qh
-- Lean.Server.CodeActions.Basic
Lean.Server.instCoeCodeActionLazyCodeAction : Coe Lean.Lsp.CodeAction Lean.Server.LazyCodeAction
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
/-- An object `X` in an abelian category has projective dimension `< n` if
all `Ext X Y i` vanish when `n ≤ i`. See also `HasProjectiveDimensionLE`.
(Do not use the `subsingleton'` field directly. Use the constructor
`HasProjectiveDimensionLT.mk`, and the lemmas `hasProjectiveDimensionLT_iff` and
`Ext.eq_zero_of_hasProjectiveDimensionLT`.)  -/
CategoryTheory.HasProjectiveDimensionLT : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Abelian C] → C → ℕ → Prop
-- Std.Http.Data.Status
Std.Http.Status.badRequest.sizeOf_spec : sizeOf Std.Http.Status.badRequest = 1
-- Mathlib.Logic.Equiv.Fin.Rotate
lt_finRotate_iff_ne_neg_one : ∀ {n : ℕ} [inst : NeZero n] (i : Fin n), i < (finRotate n) i ↔ i ≠ -1
-- Init.Data.SInt.Lemmas
Int32.toInt64_ne_neg_one : ∀ (a : Int32), a ≠ -1 → a.toInt64 ≠ -1
-- Mathlib.Data.List.Infix
List.inits_cons : ∀ {α : Type u_1} (a : α) (l : List α), (a :: l).inits = [] :: List.map (fun t => a :: t) l.inits
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
AlgebraicGeometry.UniversallyOpen.eq : @AlgebraicGeometry.UniversallyOpen = (AlgebraicGeometry.topologically @IsOpenMap).universally
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
iteratedDerivWithin_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {c : F} {s : Set 𝕜} {x : 𝕜},
  iteratedDerivWithin n (fun x => c) s x = if n = 0 then c else 0
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
Char.reduceToLower : Lean.Meta.Simp.DSimproc
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.stabilizer_finite : ∀ {G : Type u_1} [inst : Group G] {s : Set G}, s.Nonempty → s.Finite → (↑(MulAction.stabilizer G s)).Finite
-- Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureCofibrant
HomotopicalAlgebra.CofibrantObject.instIsLeftDerivabilityStructureWeakEquivalencesLocalizerMorphism : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  (HomotopicalAlgebra.CofibrantObject.localizerMorphism C).IsLeftDerivabilityStructure
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.inv_hom_whiskerRight_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f : X ≅ Y) (Z : C) {Z_1 : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.inv Z)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom Z) h) =
    h
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.encodeCode.match_1.eq_5 : ∀ (motive : Nat.Partrec.Code → Sort u_1) (cf cg : Nat.Partrec.Code) (h_1 : Unit → motive Nat.Partrec.Code.zero)
  (h_2 : Unit → motive Nat.Partrec.Code.succ) (h_3 : Unit → motive Nat.Partrec.Code.left)
  (h_4 : Unit → motive Nat.Partrec.Code.right) (h_5 : (cf cg : Nat.Partrec.Code) → motive (cf.pair cg))
  (h_6 : (cf cg : Nat.Partrec.Code) → motive (cf.comp cg)) (h_7 : (cf cg : Nat.Partrec.Code) → motive (cf.prec cg))
  (h_8 : (cf : Nat.Partrec.Code) → motive cf.rfind'),
  (match cf.pair cg with
    | Nat.Partrec.Code.zero => h_1 ()
    | Nat.Partrec.Code.succ => h_2 ()
    | Nat.Partrec.Code.left => h_3 ()
    | Nat.Partrec.Code.right => h_4 ()
    | cf.pair cg => h_5 cf cg
    | cf.comp cg => h_6 cf cg
    | cf.prec cg => h_7 cf cg
    | cf.rfind' => h_8 cf) =
    h_5 cf cg
-- Mathlib.GroupTheory.Complement
/-- Given two subgroups `H' ⊆ H`, there exists a left transversal to `H'` inside `H`.  -/
Subgroup.exists_left_transversal_of_le : ∀ {G : Type u_1} [inst : Group G] {H' H : Subgroup G},
  H' ≤ H → ∃ S, S * ↑H' = ↑H ∧ Nat.card ↑S * Nat.card ↥H' = Nat.card ↥H
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.isoIsPullback_inv_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : C} (X Y : C) {Z : C} {fst : P ⟶ X} {snd : P ⟶ Y}
  {f : X ⟶ Z} {g : Y ⟶ Z} {P' : C} {fst' : P' ⟶ X} {snd' : P' ⟶ Y} (h : CategoryTheory.IsPullback fst snd f g)
  (h' : CategoryTheory.IsPullback fst' snd' f g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.IsPullback.isoIsPullback X Y h h').inv fst = fst'
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k a : α} {v : β k},
  (t.insertIfNew k v).get? a = if h : cmp k a = Ordering.eq ∧ k ∉ t then some (cast ⋯ v) else t.get? a
-- Mathlib.Data.List.MinMax
List.le_maximum_of_mem' : ∀ {α : Type u_1} [inst : LinearOrder α] {l : List α} {a : α}, a ∈ l → ↑a ≤ l.maximum