mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.ExtraTheorem.const.inj : ∀ {declName declName_1 : Lean.Name},
  Lean.Elab.Tactic.Grind.ExtraTheorem.const declName = Lean.Elab.Tactic.Grind.ExtraTheorem.const declName_1 →
    declName = declName_1
-- Mathlib.Algebra.Order.Group.Basic
zsmul_le_zsmul_left : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {m n : ℤ} {a : α},
  0 ≤ a → m ≤ n → m • a ≤ n • a
-- Lean.Meta.Tactic.Cases
Lean.Meta.GeneralizeIndicesSubgoal.fvarId : Lean.Meta.GeneralizeIndicesSubgoal → Lean.FVarId
-- Lean.EnvExtension
Lean.MapDeclarationExtension.find? : {α : Type} →
  [Inhabited α] →
    (ext : Lean.MapDeclarationExtension α) →
      Lean.Environment →
        Lean.Name →
          optParam Lean.EnvExtension.AsyncMode ext.toEnvExtension.asyncMode →
            optParam Lean.OLeanLevel Lean.OLeanLevel.exported → Option α
-- Mathlib.RingTheory.Coalgebra.Basic
/-- Transfer `CoalgebraStruct` across an `Equiv`.  -/
Equiv.coalgebraStruct : (R : Type u_1) →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid B] → [inst_2 : Module R B] → [CoalgebraStruct R B] → (e : A ≃ B) → CoalgebraStruct R A
-- Mathlib.Analysis.CStarAlgebra.Basic
/-- `star` bundled as a linear isometric equivalence  -/
starₗᵢ : (𝕜 : Type u_1) →
  {E : Type u_2} →
    [inst : CommSemiring 𝕜] →
      [inst_1 : StarRing 𝕜] →
        [inst_2 : SeminormedAddCommGroup E] →
          [inst_3 : StarAddMonoid E] → [NormedStarGroup E] → [inst_5 : Module 𝕜 E] → [StarModule 𝕜 E] → E ≃ₗᵢ⋆[𝕜] E
-- Mathlib.Topology.Algebra.Group.Pointwise
MulAction.isClosedMap_quotient : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Group α]
  [inst_3 : MulAction α β] [ContinuousInv α] [ContinuousSMul α β] [CompactSpace α], IsClosedMap Quotient.mk'
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.withDensity_tsum : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_2} [Countable ι]
  {f : ι → α → ENNReal},
  (∀ (i : ι), Measurable (f i)) →
    μ.withDensity (∑' (n : ι), f n) = MeasureTheory.Measure.sum fun n => μ.withDensity (f n)
-- Mathlib.Order.Filter.Prod
Filter.compl_diagonal_mem_prod : ∀ {α : Type u_1} {l₁ l₂ : Filter α}, (Set.diagonal α)ᶜ ∈ l₁ ×ˢ l₂ ↔ Disjoint l₁ l₂
-- Init.Data.List.Count
List.count_tail_le : ∀ {α : Type u_1} [inst : BEq α] {a : α} {l : List α}, List.count a l.tail ≤ List.count a l
-- Mathlib.Analysis.Normed.Group.Continuity
tendsto_iff_enorm_neg_add_tendsto_zero : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedAddGroup E] {f : α → E} {a : Filter α} {b : E},
  Filter.Tendsto f a (nhds b) ↔ Filter.Tendsto (fun e => ‖-f e + b‖ₑ) a (nhds 0)
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.toMeasure_mk : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (h : MeasureTheory.IsFiniteMeasure μ),
  ↑⟨μ, h⟩ = μ
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_diff_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α}, k ∉ t₂ → (t₁ \ t₂).get? k = t₁.get? k
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
_private.Mathlib.Combinatorics.Enumerative.IncidenceAlgebra.0.IncidenceAlgebra.muFun.congr_simp : ∀ (𝕜 : Type u_2) {α : Type u_5} [inst : AddCommGroup 𝕜] [inst_1 : One 𝕜] [inst_2 : Preorder α]
  [inst_3 : LocallyFiniteOrder α] {inst_4 : DecidableEq α} [inst_5 : DecidableEq α] (a a_1 : α),
  a = a_1 → ∀ (a_2 a_3 : α), a_2 = a_3 → IncidenceAlgebra.muFun✝ 𝕜 a a_2 = IncidenceAlgebra.muFun✝ 𝕜 a_1 a_3
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.isMonicOfDegree_X : ∀ (R : Type u_1) [inst : Semiring R] [Nontrivial R], Polynomial.X.IsMonicOfDegree 1
-- Lean.Parser.Extra
Lean.Parser.symbol.formatter : String → Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Trident.app_zero : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)}
  (s : CategoryTheory.Limits.Trident f) (j : J),
  CategoryTheory.CategoryStruct.comp (s.π.app CategoryTheory.Limits.WalkingParallelFamily.zero) (f j) =
    s.π.app CategoryTheory.Limits.WalkingParallelFamily.one
-- Mathlib.Data.Set.Image
Set.preimage_singleton_nonempty : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {y : β}, (f ⁻¹' {y}).Nonempty ↔ y ∈ Set.range f
-- Mathlib.Topology.MetricSpace.ProperSpace
/-- A proper pseudometric space is sigma compact, and therefore second countable.  -/
secondCountable_of_proper : ∀ {α : Type u} [inst : PseudoMetricSpace α] [ProperSpace α], SecondCountableTopology α
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- Together `Matrix.submatrixEquivInvertible` and
`Matrix.invertibleOfSubmatrixEquivInvertible` form an equivalence, although both sides of the
equiv are subsingleton anyway.  -/
Matrix.submatrixEquivInvertibleEquivInvertible : {m : Type u} →
  {n : Type u'} →
    {α : Type v} →
      [inst : Fintype n] →
        [inst_1 : DecidableEq n] →
          [inst_2 : CommRing α] →
            [inst_3 : Fintype m] →
              [inst_4 : DecidableEq m] →
                (A : Matrix m m α) → (e₁ e₂ : n ≃ m) → Invertible (A.submatrix ⇑e₁ ⇑e₂) ≃ Invertible A
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.instInhabited : {ι : Type u_1} → (I : BoxIntegral.Box ι) → Inhabited (BoxIntegral.TaggedPrepartition I)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- Vertical composition of oplax transformations.  -/
CategoryTheory.Lax.OplaxTrans.vComp : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G H : CategoryTheory.LaxFunctor B C} →
          CategoryTheory.Lax.OplaxTrans F G → CategoryTheory.Lax.OplaxTrans G H → CategoryTheory.Lax.OplaxTrans F H
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.mk.sizeOf_spec : ∀ (carrier : Type u) [str : AddSemigroup carrier],
  sizeOf { carrier := carrier, str := str } = 1 + sizeOf carrier + sizeOf str
-- Mathlib.Tactic.GRewrite.Core
Mathlib.Tactic.GRewrite.GRewriteResult.mk.inj : ∀ {eNew impProof : Lean.Expr} {mvarIds : List Lean.MVarId} {lctx? : Option Lean.LocalContext}
  {eNew_1 impProof_1 : Lean.Expr} {mvarIds_1 : List Lean.MVarId} {lctx?_1 : Option Lean.LocalContext},
  { eNew := eNew, impProof := impProof, mvarIds := mvarIds, lctx? := lctx? } =
      { eNew := eNew_1, impProof := impProof_1, mvarIds := mvarIds_1, lctx? := lctx?_1 } →
    eNew = eNew_1 ∧ impProof = impProof_1 ∧ mvarIds = mvarIds_1 ∧ lctx? = lctx?_1
-- Init.Data.List.MinMaxOn
List.minOn_singleton : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {x : α} {f : α → β}, List.minOn f [x] ⋯ = x
-- Mathlib.Order.DirectedInverseSystem
/-- A copy of `DirectedSystem.map_map` specialized to FunLike, as otherwise the
`fun i j h ↦ f i j h` can confuse the simplifier.  -/
DirectedSystem.map_map' : ∀ {ι : Type u_1} [inst : Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
  (f : (i j : ι) → (h : i ≤ j) → T h) [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
  [DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] ⦃i j k : ι⦄ (hij : i ≤ j) (hjk : j ≤ k) (x : F i),
  (f j k hjk) ((f i j hij) x) = (f i k ⋯) x
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.one_fst : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A],
  (DoubleCentralizer.toProd 1).1 = 1
-- Mathlib.Order.Hom.Basic
instFunLikeOrderEmbedding : (α : Type u_6) → (β : Type u_7) → [inst : LE α] → [inst_1 : LE β] → FunLike (α ↪o β) α β
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.homTensorHomMap_apply : ∀ {R : Type uR} {A : Type uA} {B : Type uB} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ}
  [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B]
  [inst_5 : AddCommMonoid M] [inst_6 : Module R M] [inst_7 : Module A M] [inst_8 : IsScalarTower R A M]
  [inst_9 : AddCommMonoid N] [inst_10 : Module R N] [inst_11 : AddCommMonoid P] [inst_12 : Module R P]
  [inst_13 : Module A P] [inst_14 : IsScalarTower R A P] [inst_15 : AddCommMonoid Q] [inst_16 : Module R Q]
  [inst_17 : Module B P] [inst_18 : IsScalarTower R B P] [inst_19 : SMulCommClass A B P] (f : M →ₗ[A] P)
  (g : N →ₗ[R] Q),
  (TensorProduct.AlgebraTensorModule.homTensorHomMap R A B M N P Q) (f ⊗ₜ[R] g) =
    TensorProduct.AlgebraTensorModule.map f g
-- Init.Tactics
/-- Introduces one or more hypotheses, optionally naming and/or pattern-matching them.
For each hypothesis to be introduced, the remaining main goal's target type must
be a `let` or function type.

* `intro` by itself introduces one anonymous hypothesis, which can be accessed
  by e.g. `assumption`. It is equivalent to `intro _`.
* `intro x y` introduces two hypotheses and names them. Individual hypotheses
  can be anonymized via `_`, given a type ascription, or matched against a pattern:
  ```lean
  -- ... ⊢ α × β → ...
  intro (a, b)
  -- ..., a : α, b : β ⊢ ...
  ```
* `intro rfl` is short for `intro h; subst h`, if `h` is an equality where the left-hand or right-hand side
  is a variable.
* Alternatively, `intro` can be combined with pattern matching much like `fun`:
  ```lean
  intro
  | n + 1, 0 => tac
  | ...
  ```
 -/
Lean.Parser.Tactic.intro : Lean.ParserDescr
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
CategoryTheory.Equalizer.Presieve.Arrows.firstMap.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C} {I : Type t}
  [inst_1 : Small.{w, t} I] (X : I → C) (π : (i : I) → X i ⟶ B)
  [inst_2 : (CategoryTheory.Presieve.ofArrows X π).HasPairwisePullbacks],
  CategoryTheory.Equalizer.Presieve.Arrows.firstMap P X π =
    CategoryTheory.Limits.Pi.lift fun x =>
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun i => P.obj (Opposite.op (X i))) x.1)
        (P.map (CategoryTheory.Limits.pullback.fst (π x.1) (π x.2)).op)
-- Mathlib.Topology.Order
continuous_id_of_le : ∀ {α : Type u} {t t' : TopologicalSpace α}, t ≤ t' → Continuous id
-- Lean.Data.Lsp.Internal
Lean.Lsp.instToJsonLeanModuleQuery.toJson : Lean.Lsp.LeanModuleQuery → Lean.Json
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_eq_of_equiv : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β)
  [inst_2 : LawfulBEq α],
  (↑m₁).WF → (↑m₂).WF → (↑m₁).Equiv ↑m₂ → ∀ {k : α} [inst_3 : Inhabited (β k)], m₁.get! k = m₂.get! k
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.zero_mem : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M),
  0 ∈ p
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.map_le_iff_le_comap : ∀ {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (H : G.Subgraph) (H' : G'.Subgraph),
  SimpleGraph.Subgraph.map f H ≤ H' ↔ H ≤ SimpleGraph.Subgraph.comap f H'
-- Mathlib.Algebra.Quandle
Rack.mk : {α : Type u} →
  [toShelf : Shelf α] →
    (invAct : α → α → α) →
      (∀ (x : α), Function.LeftInverse (invAct x) (Shelf.act x)) →
        (∀ (x : α), Function.RightInverse (invAct x) (Shelf.act x)) → Rack α
-- Std.Data.ExtHashMap.Lemmas
/-- Variant of `getElem!_map` that holds with `EquivBEq` (i.e. without `LawfulBEq`).  -/
Std.ExtHashMap.getElem!_map' : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited γ] {f : α → β → γ} {k : α},
  (Std.ExtHashMap.map f m)[k]! = (Option.pmap (fun v h => f (m.getKey k h) v) m[k]? ⋯).get!
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_perm_eq_two_power : ∀ {α : Type u} [Infinite α], Cardinal.mk (Equiv.Perm α) = 2 ^ Cardinal.mk α
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
/-- The map `idealSetMap` is actually an equiv between `idealSet K J` and the elements of
`integerSet K` whose preimage lies in `J`.  -/
NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      (J : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) →
        ↑(NumberField.mixedEmbedding.fundamentalCone.idealSet K J) ≃
          ↑{a | ↑(NumberField.mixedEmbedding.fundamentalCone.preimageOfMemIntegerSet a) ∈ ↑↑J}
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves colimits of shape `Jᵒᵖ`, then `F.unop : C ⥤ D` preserves limits of
shape `J`.  -/
CategoryTheory.Limits.preservesLimitsOfShape_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ)
  [CategoryTheory.Limits.PreservesColimitsOfShape Jᵒᵖ F], CategoryTheory.Limits.PreservesLimitsOfShape J F.unop
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
ENNReal.measurable_log : Measurable ENNReal.log
-- Mathlib.Order.UpperLower.Principal
LowerSet.bot_lt_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, ⊥ < LowerSet.Iic a
-- Mathlib.Tactic.Positivity.Core
_private.Mathlib.Tactic.Positivity.Core.0.Mathlib.Meta.Positivity.OrderRel.noConfusionType : Sort v✝ → Mathlib.Meta.Positivity.OrderRel✝ → Mathlib.Meta.Positivity.OrderRel✝ → Sort v✝
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.OuterMeasure.mkMetric_top : ∀ {X : Type u_2} [inst : EMetricSpace X], (MeasureTheory.OuterMeasure.mkMetric fun x => ⊤) = ⊤
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
MeasurableSet.setOfPred_infinite : ∀ {α : Type u_1} [Countable α], MeasurableSet {s | s.Infinite}
-- Init.Data.Range.Basic
Std.Legacy.Range.forIn' : {m : Type u_1 → Type u_2} →
  {β : Type u_1} → [Monad m] → (range : Std.Legacy.Range) → β → ((i : ℕ) → i ∈ range → β → m (ForInStep β)) → m β
-- Init.Data.List.Perm
_private.Init.Data.List.Perm.0.List.reverseAux.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (r : List α) (h_1 : (r : List α) → motive [] r)
  (h_2 : (a : α) → (l r : List α) → motive (a :: l) r),
  (match [], r with
    | [], r => h_1 r
    | a :: l, r => h_2 a l r) =
    h_1 r
-- Mathlib.Combinatorics.Quiver.Path
/-- Every non-empty path can be decomposed as an initial path plus a final edge.  -/
Quiver.Path.length_ne_zero_iff_eq_cons : ∀ {V : Type u_1} [inst : Quiver V] {a b : V} (p : Quiver.Path a b), p.length ≠ 0 ↔ ∃ c p' e, p = p'.cons e
-- Mathlib.Algebra.Ring.Idempotent
/-- If idempotent `a` and element `b` anti-commute, then they commute.
So anti-commutativity implies commutativity when one of them is idempotent.  -/
IsIdempotentElem.commute_of_anticommute : ∀ {R : Type u_1} {a b : R} [inst : NonUnitalSemiring R] [IsAddTorsionFree R],
  IsIdempotentElem a → a * b + b * a = 0 → Commute a b
-- Lean.Meta.WHNF
_private.Lean.Meta.WHNF.0.Lean.Meta.smartUnfoldingReduce?.go : Lean.Expr → OptionT Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sup_add_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {β : Type u_5} [inst_2 : SemilatticeSup β]
  [inst_3 : OrderBot β] (s t : Finset α) (f : α → β), (s + t).sup f = t.sup fun y => s.sup fun x => f (x + y)
-- Mathlib.Data.Set.Basic
Set.univ_eq_empty_iff : ∀ {α : Type u}, Set.univ = ∅ ↔ IsEmpty α
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Helper function for reducing `(x <<< i) <<< j` (and `(x >>> i) >>> j`) where `i` and `j` are
natural number literals.
 -/
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec.0.BitVec.reduceShiftShift : Lean.Name → Lean.Name → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits
SheafOfModules.Finite.evaluationPreservesFiniteLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  (R : CategoryTheory.Sheaf J RingCat) (X : Cᵒᵖ),
  CategoryTheory.Limits.PreservesFiniteLimits (SheafOfModules.evaluation R X)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.ofNat_ne_bot : ∀ {α : Type u} [inst : AddMonoidWithOne α] (n : ℕ) [inst_1 : n.AtLeastTwo], OfNat.ofNat n ≠ ⊥
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
CategoryTheory.Limits.isColimitOfHasPushoutOfPreservesColimit.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y)
  [inst_2 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G]
  [i : CategoryTheory.Limits.HasPushout f g],
  CategoryTheory.Limits.isColimitOfHasPushoutOfPreservesColimit G f g =
    CategoryTheory.Limits.isColimitOfHasPushoutOfPreservesColimit G f g
-- Init.Data.Nat.Bitwise.Lemmas
Nat.or_assoc : ∀ (x y z : ℕ), x ||| y ||| z = x ||| (y ||| z)
-- Mathlib.LinearAlgebra.Trace
LinearMap.trace_transpose' : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Free R M]
  [Module.Finite R M] (f : M →ₗ[R] M),
  (LinearMap.trace R (Module.Dual R M)) (Module.Dual.transpose f) = (LinearMap.trace R M) f
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.reduce_fold_fn : {n : ℕ} →
  Array Std.Tactic.BVDecide.LRAT.Internal.Assignment →
    Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) →
      Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) →
        Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.equivOfTensorIsoUnit_inverse : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) (m n : M)
  (h₁ : CategoryTheory.MonoidalCategoryStruct.tensorObj m n ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit M)
  (h₂ : CategoryTheory.MonoidalCategoryStruct.tensorObj n m ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit M)
  (H :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight h₁.hom m)
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor m).hom =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator m n m).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft m h₂.hom)
          (CategoryTheory.MonoidalCategoryStruct.rightUnitor m).hom))
  [inst_3 : F.Monoidal], (CategoryTheory.equivOfTensorIsoUnit F m n h₁ h₂ H).inverse = F.obj n
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.liftRel_iff_coeFn : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] {r : β → γ → Prop} {f : α →ₘ[μ] β} {g : α →ₘ[μ] γ},
  MeasureTheory.AEEqFun.LiftRel r f g ↔ ∀ᵐ (a : α) ∂μ, r (↑f a) (↑g a)
-- Mathlib.NumberTheory.Chebyshev
/-- `|ψ x - θ x| ≤ c √ x log x` with an explicit constant c.  To remove the log, see
`psi_sub_theta_le_mul_sqrt`.  -/
Chebyshev.abs_psi_sub_theta_le_sqrt_mul_log : ∀ {x : ℝ}, 1 ≤ x → |Chebyshev.psi x - Chebyshev.theta x| ≤ 2 * √x * Real.log x
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.RightExtension.precomp_obj_right : ∀ {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C'] [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H)
  (G : CategoryTheory.Functor C' C)
  (X : CategoryTheory.Comma ((CategoryTheory.Functor.whiskeringLeft C D H).obj L) (CategoryTheory.Functor.fromPUnit F)),
  ((CategoryTheory.Functor.RightExtension.precomp L F G).obj X).right = X.right
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidalObj_μ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.AddMon C) (X Y : CategoryTheory.Discrete PUnit.{u_1 + 1}),
  CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidalObj A) X
      Y =
    CategoryTheory.AddMonObj.add
-- Init.Data.Int.Gcd
Int.gcd_eq_left : ∀ {a b : ℤ}, 0 ≤ a → a ∣ b → ↑(a.gcd b) = a
-- Mathlib.GroupTheory.Commensurable
AddSubgroup.Commensurable.comm : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, H.Commensurable K ↔ K.Commensurable H
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Fan.IsLimit.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type u_1} {F : I → C} {c : CategoryTheory.Limits.Fan F}
  (hc : CategoryTheory.Limits.IsLimit c) {A : C} (f g : A ⟶ c.pt),
  (∀ (i : I), CategoryTheory.CategoryStruct.comp f (c.proj i) = CategoryTheory.CategoryStruct.comp g (c.proj i)) → f = g
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.type_eq_one_iff_unique : ∀ {α : Type u} {r : α → α → Prop} [inst : IsWellOrder α r], Ordinal.type r = 1 ↔ Nonempty (Unique α)
-- Init.Data.List.Erase
List.eraseIdx_replicate : ∀ {α : Type u_1} {n : ℕ} {a : α} {k : ℕ},
  (List.replicate n a).eraseIdx k = if k < n then List.replicate (n - 1) a else List.replicate n a
-- Mathlib.Algebra.Polynomial.Eval.Defs
/-- `eval₂` as a `RingHom` for noncommutative rings  -/
Polynomial.eval₂RingHom' : {R : Type u} →
  {S : Type v} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] → (f : R →+* S) → (x : S) → (∀ (a : R), Commute (f a) x) → Polynomial R →+* S
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.inv_hom_s₀_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreOneHypercover S} (e : E ≅ F)
  (i : F.I₀), e.hom.s₀ (e.inv.s₀ i) = i
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
/-- a map `I₁₂ × I₃ → J`  -/
CategoryTheory.GradedObject.BifunctorComp₁₂IndexData.q : {I₁ : Type u_7} →
  {I₂ : Type u_8} →
    {I₃ : Type u_9} →
      {J : Type u_10} →
        {r : I₁ × I₂ × I₃ → J} → (self : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) → self.I₁₂ × I₃ → J
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α} [inst_1 : Inhabited (β k)], k ∉ m₂ → (m₁ ∪ m₂).get! k = m₁.get! k
-- Mathlib.CategoryTheory.Action
CategoryTheory.ActionCategory.back_coe : ∀ {M : Type u_1} [inst : Monoid M] {X : Type u} [inst_1 : MulAction M X] (x : CategoryTheory.ActionCategory M X),
  ⟨(), x.back⟩ = x
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {k : α},
  k ∉ m₂ → Std.ExtDHashMap.Const.get! (m₁.union m₂) k = Std.ExtDHashMap.Const.get! m₁ k
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.mem_restrict : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {F E : IntermediateField K L}
  (h : F ≤ E) (x : ↥E), x ∈ IntermediateField.restrict h ↔ ↑x ∈ F
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.ring : {R : Type u} → [inst : Ring R] → Ring (Polynomial R)
-- Mathlib.RingTheory.FractionalIdeal.Basic
IsFractional.pow : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {I : Submodule R P}, IsFractional S I → ∀ (n : ℕ), IsFractional S (I ^ n)
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleRange.eq_1 : ∀ {n : ℕ} (i : Fin n), i.cycleRange = (finRotate (↑i + 1)).extendDomain (Fin.castLEEmb ⋯).toEquivRange