mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.mapDomainLinearMap.eq_1 : ∀ (R : Type u_1) (S : Type u_2) {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Module R S] (f : M → N),
  AddMonoidAlgebra.mapDomainLinearMap R S f =
    ↑(AddMonoidAlgebra.coeffLinearEquiv R).symm ∘ₗ Finsupp.lmapDomain S R f ∘ₗ ↑(AddMonoidAlgebra.coeffLinearEquiv R)
-- Std.Tactic.BVDecide.LRAT.Internal.Entails
Std.Tactic.BVDecide.LRAT.Internal.Liff.refl : ∀ {α : Type u} {σ : Type v} [inst : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ] (f : σ),
  Std.Tactic.BVDecide.LRAT.Internal.Liff α f f
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.mapHomologicalComplexXIso'_hom : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v, u_1} C]
  [inst_1 : CategoryTheory.Category.{v', u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] {F G : CochainComplex C ℤ} (φ : F ⟶ G)
  [inst_4 : HomologicalComplex.HasHomotopyCofiber φ] (H : CategoryTheory.Functor C D) [inst_5 : H.Additive]
  [inst_6 : HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)] (n m : ℤ)
  (hnm : n + 1 = m),
  (CochainComplex.mappingCone.mapHomologicalComplexXIso' φ H n m hnm).hom =
    CategoryTheory.CategoryStruct.comp (H.map ((↑(CochainComplex.mappingCone.fst φ)).v n m ⋯))
        ((CochainComplex.mappingCone.inl ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v m n ⋯) +
      CategoryTheory.CategoryStruct.comp (H.map ((CochainComplex.mappingCone.snd φ).v n n ⋯))
        ((CochainComplex.mappingCone.inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).f n)
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
CategoryTheory.Sheaf.functorH.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (n n_1 : ℕ),
  n = n_1 → CategoryTheory.Sheaf.functorH J n = CategoryTheory.Sheaf.functorH J n_1
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.PenroseVar.mk.inj : ∀ {ident : String} {indices : List ℕ} {e : Lean.Expr} {ident_1 : String} {indices_1 : List ℕ} {e_1 : Lean.Expr},
  { ident := ident, indices := indices, e := e } = { ident := ident_1, indices := indices_1, e := e_1 } →
    ident = ident_1 ∧ indices = indices_1 ∧ e = e_1
-- Mathlib.Algebra.Ring.Parity
neg_one_zpow_eq_ite : ∀ {α : Type u_2} [inst : DivisionMonoid α] [inst_1 : HasDistribNeg α] {n : ℤ}, (-1) ^ n = if Even n then 1 else -1
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.coe_inj : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_5} [inst_1 : CommRing K] [inst_2 : Algebra R K] [IsFractionRing R K]
  {a b : R}, ↑a = ↑b ↔ a = b
-- Mathlib.GroupTheory.GroupAction.Basic
isCancelSMul_iff_stabilizer_eq_bot : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
  IsCancelSMul G α ↔ ∀ (a : α), MulAction.stabilizer G a = ⊥
-- Mathlib.RingTheory.KrullDimension.LocalRing
ringKrullDim_eq_one_iff_of_isLocalRing_isDomain : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R] [IsDomain R],
  ringKrullDim R = 1 ↔ ¬IsField R ∧ ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical
-- Init.Meta.Defs
Lean.Syntax.instCoeIdentTSyntaxConsSyntaxNodeKindMkStr4Nil : Coe Lean.Ident (Lean.TSyntax `Lean.Parser.Command.declId)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.GetLsbD
Std.Tactic.BVDecide.BVPred.GetLsbDTarget.mk.inj : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {aig : Std.Sat.AIG α} {w : ℕ} {vec : aig.RefVec w}
  {idx w_1 : ℕ} {vec_1 : aig.RefVec w_1} {idx_1 : ℕ},
  { w := w, vec := vec, idx := idx } = { w := w_1, vec := vec_1, idx := idx_1 } → w = w_1 ∧ vec ≍ vec_1 ∧ idx = idx_1
-- Mathlib.Algebra.Homology.HomologySequenceLemmas
HomologicalComplex.cyclesFunctor.congr_simp : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i i_1 : ι),
  i = i_1 →
    ∀ [inst_2 : CategoryTheory.CategoryWithHomology C],
      HomologicalComplex.cyclesFunctor C c i = HomologicalComplex.cyclesFunctor C c i_1
-- Mathlib.Analysis.InnerProductSpace.LaxMilgram
IsCoercive.antilipschitz : ∀ {V : Type u} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : CompleteSpace V]
  {B : V →L[ℝ] V →L[ℝ] ℝ},
  IsCoercive B → ∃ C, 0 < C ∧ AntilipschitzWith C ⇑(InnerProductSpace.continuousLinearMapOfBilin B)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List α}
  {k : α}, (Std.ExtTreeMap.unitOfList l cmp)[k]? = if l.contains k = true then some () else none
-- Mathlib.Data.TypeVec
TypeVec.appendFun_inj : ∀ {n : ℕ} {α : TypeVec.{u_1} n} {α' : TypeVec.{u_2} n} {β : Type u_1} {β' : Type u_2} {f f' : α.Arrow α'}
  {g g' : β → β'}, (f ::: g) = (f' ::: g') → f = f' ∧ g = g'
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- Note that subgraphs do not form a Boolean algebra, because of `verts`.  -/
SimpleGraph.Subgraph.instCompletelyDistribLattice : {V : Type u} → {G : SimpleGraph V} → CompletelyDistribLattice G.Subgraph
-- Mathlib.Topology.Category.UniformSpace
UniformSpaceCat.of.injEq : ∀ (carrier : Type u) [str : UniformSpace carrier] (carrier_1 : Type u) (str_1 : UniformSpace carrier_1),
  ({ carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 }) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.lift_id : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (x : S), (IsLocalization.lift ⋯) x = x
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Basic.0.Std.Tactic.BVDecide.BVExpr.toString.match_1.eq_5 : ∀ (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) (w : ℕ) (op : Std.Tactic.BVDecide.BVUnOp)
  (operand : Std.Tactic.BVDecide.BVExpr w) (h_1 : (w idx : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var idx))
  (h_2 : (w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val))
  (h_3 :
    (len w start : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w) → motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr))
  (h_4 :
    (w : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinOp) → (rhs : Std.Tactic.BVDecide.BVExpr w) → motive w (lhs.bin op rhs))
  (h_5 :
    (w : ℕ) →
      (op : Std.Tactic.BVDecide.BVUnOp) →
        (operand : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op operand))
  (h_6 :
    (w l r : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr l) →
        (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h))
  (h_7 :
    (w w_1 n : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w_1) →
        (h : w = w_1 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h))
  (h_8 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs))
  (h_9 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs))
  (h_10 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)),
  (match w, Std.Tactic.BVDecide.BVExpr.un op operand with
    | w, Std.Tactic.BVDecide.BVExpr.var idx => h_1 w idx
    | w, Std.Tactic.BVDecide.BVExpr.const val => h_2 w val
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr => h_3 len w start expr
    | w, lhs.bin op rhs => h_4 w lhs op rhs
    | w, Std.Tactic.BVDecide.BVExpr.un op operand => h_5 w op operand
    | w, lhs.append rhs h => h_6 w l r lhs rhs h
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h => h_7 w w_1 n expr h
    | w, lhs.shiftLeft rhs => h_8 w n lhs rhs
    | w, lhs.shiftRight rhs => h_9 w n lhs rhs
    | w, lhs.arithShiftRight rhs => h_10 w n lhs rhs) =
    h_5 w op operand
-- Mathlib.GroupTheory.Nilpotent
/-- An auxiliary type-theoretic definition defining both the upper central series of
an additive group, and a proof that it is characteristic, all in one go.  -/
AddSubgroup.upperCentralSeriesAux : (G : Type u_2) → [inst : AddGroup G] → ℕ → (H : AddSubgroup G) ×' H.Characteristic
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun_congr' : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : ι → Type u_8}
  {mβ : (i : ι) → MeasurableSpace (β i)} {f g : (i : ι) → Ω → β i},
  (∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᵐ[κ a] g i) →
    (ProbabilityTheory.Kernel.iIndepFun f κ μ ↔ ProbabilityTheory.Kernel.iIndepFun g κ μ)
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
/-- Introduction rule to prove that `b` is the infimum of `f`: it suffices to check that `b`
is smaller than `f i` for all `i`, and that this is not the case of any `w>b`.
See `iInf_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in complete lattices.  -/
Directed.ciInf_eq_of_forall_ge_of_forall_gt_exists_lt : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompletePartialOrderInf α] {b : α} [Nonempty ι] {f : ι → α},
  Directed (fun x1 x2 => x2 ≤ x1) f → (∀ (i : ι), b ≤ f i) → (∀ (w : α), b < w → ∃ i, f i < w) → ⨅ i, f i = b
-- Mathlib.Order.Basic
Subtype.partialOrder : {α : Type u_2} → [PartialOrder α] → (p : α → Prop) → PartialOrder (Subtype p)
-- Lean.Elab.PreDefinition.FixedParams
Lean.Elab.FixedParams.Info.mk.inj : ∀ {graph : Array (Array (Option (Array (Option ℕ))))} {revDeps : Array (Array (Array ℕ))}
  {graph_1 : Array (Array (Option (Array (Option ℕ))))} {revDeps_1 : Array (Array (Array ℕ))},
  { graph := graph, revDeps := revDeps } = { graph := graph_1, revDeps := revDeps_1 } →
    graph = graph_1 ∧ revDeps = revDeps_1
-- Mathlib.CategoryTheory.Category.Basic
/-- `f : X ⟶ Y` is an epimorphism iff for all `Z`, composition of morphisms `Y ⟶ Z` with `f`
is injective.  -/
CategoryTheory.epi_iff_forall_injective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.Epi f ↔ ∀ (Z : C), Function.Injective fun g => CategoryTheory.CategoryStruct.comp f g
-- Mathlib.GroupTheory.SpecificGroups.Alternating
nat_card_alternatingGroup : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] [Nontrivial α],
  Nat.card ↥(alternatingGroup α) = (Nat.card α).factorial / 2
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_insertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α Unit} [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {l : List α} {k : α}, k ∈ m.insertManyIfNewUnit l ↔ k ∈ m ∨ l.contains k = true
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
instIsRightCancelMulOfMulRightReflectLE : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : PartialOrder α] [MulRightReflectLE α], IsRightCancelMul α
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_g : ∀ {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₀.g =
    CategoryTheory.Limits.kernel.map (CategoryTheory.CategoryStruct.comp f g) g f (CategoryTheory.CategoryStruct.id Z) ⋯
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommSum_cons' : ∀ {α : Type u_3} [inst : AddMonoid α] (s : Multiset α) (a : α) (comm : {x | x ∈ a ::ₘ s}.Pairwise AddCommute),
  (a ::ₘ s).noncommSum comm = s.noncommSum ⋯ + a
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.instAdditiveAddCommGrpCatExtFunctorObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (X : C) (n : ℕ), (CategoryTheory.Abelian.extFunctorObj X n).Additive
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint.eq_1 : ∀ {n : ℕ} (clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n))) (id : ℕ)
  (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment)
  (derivedLits : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))
  (derivedEmpty encounteredError : Bool),
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint clauses
      (assignments, derivedLits, derivedEmpty, encounteredError) id =
    if (encounteredError || derivedEmpty) = true then (assignments, derivedLits, derivedEmpty, encounteredError)
    else
      match clauses[id]? with
      | some (some c) =>
        match c.reduce assignments with
        | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth => (assignments, derivedLits, true, false)
        | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty => (assignments, derivedLits, true, false)
        | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit (l, b) =>
          if Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment b assignments[↑l]! = true then
            (assignments, derivedLits, false, false)
          else
            (assignments.modify (↑l) (Std.Tactic.BVDecide.LRAT.Internal.Assignment.addAssignment b),
              (l, b) :: derivedLits, false, false)
        | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit => (assignments, derivedLits, false, true)
      | some none => (assignments, derivedLits, false, true)
      | none => (assignments, derivedLits, false, true)
-- Mathlib.CategoryTheory.Filtered.Basic
/-- `coeq f f'`, for morphisms `f f' : j ⟶ j'`, is an arbitrary choice of object
which admits a morphism `coeqHom f f' : j' ⟶ coeq f f'` such that
`coeq_condition : f ≫ coeqHom f f' = f' ≫ coeqHom f f'`.
Its existence is ensured by `IsFiltered`.
 -/
CategoryTheory.IsFiltered.coeq : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.IsFilteredOrEmpty C] → {j j' : C} → (j ⟶ j') → (j ⟶ j') → C
-- Mathlib.Algebra.Group.Subgroup.Order
MulEquiv.strictMono_subsemigroupCongr : ∀ {G : Type u_1} [inst : CommMonoid G] [inst_1 : Preorder G] {S T : Subsemigroup G} (h : S = T),
  StrictMono ⇑(MulEquiv.subsemigroupCongr h)
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddModObj.regular.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : C)
  [inst_2 : CategoryTheory.AddMonObj M],
  CategoryTheory.AddModObj.regular M = { vadd := CategoryTheory.AddMonObj.add, zero_vadd := ⋯, add_vadd := ⋯ }
-- Mathlib.GroupTheory.Sylow
Sylow.characteristic_of_subsingleton : ∀ {G : Type u} [inst : Group G] {p : ℕ} [Subsingleton (Sylow p G)] (P : Sylow p G), (↑P).Characteristic
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
CategoryTheory.LaxFunctor.instInhabited : {B : Type u₁} → [inst : CategoryTheory.Bicategory B] → Inhabited (CategoryTheory.LaxFunctor B B)
-- Mathlib.Topology.Algebra.Monoid
continuousAdd_of_discreteTopology : ∀ {N : Type u_4} [inst : TopologicalSpace N] [inst_1 : Add N] [DiscreteTopology N], ContinuousAdd N
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.total_d : ∀ {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₁₂), (K.total c₁₂).d i₁₂ i₁₂' = K.D₁ c₁₂ i₁₂ i₁₂' + K.D₂ c₁₂ i₁₂ i₁₂'
-- Mathlib.RingTheory.HopfAlgebra.GroupLike
GroupLike.instInv : {R : Type u_1} →
  {A : Type u_2} → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : HopfAlgebra R A] → Inv (GroupLike R A)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
SchwartzMap.instFourierTransformInv : {E : Type u_2} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℂ E] →
      {V : Type u_3} →
        [inst_2 : NormedAddCommGroup V] →
          [inst_3 : InnerProductSpace ℝ V] →
            [FiniteDimensional ℝ V] →
              [inst_5 : MeasurableSpace V] → [BorelSpace V] → FourierTransformInv (SchwartzMap V E) (SchwartzMap V E)
-- Std.Http.Transport
/-- Generic HTTP interface that abstracts over different transport mechanisms.
 -/
Std.Http.Transport : Type → Type
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.hom₂_ext : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Pith B} {x y : a ⟶ b}
  {f g : x ⟶ y}, f.iso.hom = g.iso.hom → f = g
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeUnopOppositeOfIsClosedUnderLimitsOfShape : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J] (Q : CategoryTheory.ObjectProperty Cᵒᵖ)
  [Q.IsClosedUnderLimitsOfShape J], Q.unop.IsClosedUnderColimitsOfShape Jᵒᵖ
-- Mathlib.Algebra.Order.Group.Cone
/-- The cone of non-negative elements.  -/
AddGroupCone.nonneg : (H : Type u_1) → [inst : AddCommGroup H] → [inst_1 : PartialOrder H] → [IsOrderedAddMonoid H] → AddGroupCone H
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Real.binEntropy_nonneg : ∀ {p : ℝ}, 0 ≤ p → p ≤ 1 → 0 ≤ Real.binEntropy p
-- Mathlib.Data.Prod.TProd
List.TProd.snd_mk : ∀ {ι : Type u} {α : ι → Type v} (i : ι) (l : List ι) (f : (i : ι) → α i),
  (List.TProd.mk (i :: l) f).2 = List.TProd.mk l f
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Icc.instOne : {R : Type u_1} → [inst : Semiring R] → [inst_1 : PartialOrder R] → [IsOrderedRing R] → One ↑(Set.Icc 0 1)
-- Mathlib.Topology.UniformSpace.Defs
/-- If `s ∈ uniformity`, then `Prod.swap ⁻¹' s ∈ uniformity`.  -/
UniformSpace.symm : ∀ {α : Type u} [self : UniformSpace α], Filter.Tendsto Prod.swap UniformSpace.uniformity UniformSpace.uniformity
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.map_left_cancel : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) {x y : M} {c : ↥S}, f (x * ↑c) = f (y * ↑c) → f x = f y
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.ofBraided_μ_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : C),
  (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Center.ofBraided C) X Y).f =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.Center.ofBraided C).obj X)
          ((CategoryTheory.Center.ofBraided C).obj Y)).fst
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
/-- The non-adjacency setoid over the vertices of a Turán-maximal graph
induced by `equivalence_not_adj`.  -/
SimpleGraph.IsTuranMaximal.setoid : {V : Type u_1} →
  [inst : Fintype V] → {G : SimpleGraph V} → [inst_1 : DecidableRel G.Adj] → {r : ℕ} → G.IsTuranMaximal r → Setoid V
-- Mathlib.Tactic.GCongr.Core
/-- A collection of `GCongrLemma`, to be stored in the environment extension.  -/
Mathlib.Tactic.GCongr.GCongrLemmas : Type
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey?_eq_some_iff_mem_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {km : α}, t.maxKey? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Geometry.Convex.Cone.TensorProduct
/-- `minTensorProduct` is functorial: the image of a minimal tensor product under
`TensorProduct.map f g` is contained in the minimal tensor product of the images.  -/
PointedCone.minTensorProduct_map_le : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {G : Type u_2}
  [inst_3 : AddCommGroup G] [inst_4 : Module R G] {H : Type u_3} [inst_5 : AddCommGroup H] [inst_6 : Module R H]
  {G' : Type u_4} {H' : Type u_5} [inst_7 : AddCommGroup G'] [inst_8 : Module R G'] [inst_9 : AddCommGroup H']
  [inst_10 : Module R H'] (f : G →ₗ[R] G') (g : H →ₗ[R] H') (C₁ : PointedCone R G) (C₂ : PointedCone R H),
  PointedCone.map (TensorProduct.map f g) (C₁.minTensorProduct C₂) ≤
    (PointedCone.map f C₁).minTensorProduct (PointedCone.map g C₂)
-- Mathlib.MeasureTheory.Order.Group.Lattice
Measurable.mabs : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : Group α] [inst_2 : MeasurableSpace α]
  [inst_3 : MeasurableSpace β] {f : β → α} [MeasurableInv α] [MeasurableSup₂ α],
  Measurable f → Measurable fun x => |f x|ₘ
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isSome_maxKey?_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insert k v).maxKey?.isSome = true
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f]
  (U : TopologicalSpace.Opens ↑X.toTopCat),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp f U)
      (f.c.app (Opposite.op ((AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.opensFunctor f).obj U))) =
    X.presheaf.map (CategoryTheory.eqToHom ⋯)
-- Mathlib.CategoryTheory.Localization.Bousfield
CategoryTheory.ObjectProperty.isLocalization_isColocal : ∀ {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} {G : CategoryTheory.Functor D C}
  (adj : G ⊣ F) [G.Full] [G.Faithful],
  F.IsLocalization (CategoryTheory.ObjectProperty.isColocal fun x => x ∈ Set.range G.obj)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
neg_of_div_neg_right : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : LinearOrder G₀] {a b : G₀} [PosMulMono G₀],
  a / b < 0 → 0 ≤ a → b < 0
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
CategoryTheory.Abelian.Ext.mapExactFunctor_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive] [inst_5 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteColimits F] [inst_7 : HasDerivedCategory C]
  [inst_8 : HasDerivedCategory D] [inst_9 : CategoryTheory.HasExt C] [inst_10 : CategoryTheory.HasExt D] {X Y : C}
  {n : ℕ} (e : CategoryTheory.Abelian.Ext X Y n),
  (CategoryTheory.Abelian.Ext.mapExactFunctor F e).hom =
    CategoryTheory.CategoryStruct.comp ((F.mapDerivedCategorySingleFunctor 0).inv.app X)
      (CategoryTheory.CategoryStruct.comp (e.hom.map F.mapDerivedCategory)
        ((CategoryTheory.shiftFunctor (DerivedCategory D) ↑n).map ((F.mapDerivedCategorySingleFunctor 0).hom.app Y)))
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isSome_get?_eq_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {a : α}, (t.get? a).isSome = t.contains a
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
SimpleGraph.IsUniform.symm : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] {G : SimpleGraph α}
  [inst_2 : DecidableRel G.Adj] {ε : 𝕜} {s t : Finset α}, G.IsUniform ε s t → G.IsUniform ε t s
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
/-- **Alias** of `SimpleGraph.Walk.support_subset_support_append_left`. -/
SimpleGraph.Walk.subset_support_append_left : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (q : G.Walk v w), p.support ⊆ (p.append q).support