mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.MonoidAlgebra.Grading
AddMonoidAlgebra.gradeBy_id : ∀ {M : Type u_1} (R : Type u_3) [inst : CommSemiring R], AddMonoidAlgebra.gradeBy R id = AddMonoidAlgebra.grade R
-- Mathlib.Topology.Algebra.Affine
Homeomorph.vaddConst.congr_simp : ∀ {V : Type u_1} {P : Type u_2} [inst : AddGroup V] [inst_1 : TopologicalSpace V] [inst_2 : AddTorsor V P]
  [inst_3 : TopologicalSpace P] [inst_4 : IsTopologicalAddTorsor P] (p p_1 : P),
  p = p_1 → Homeomorph.vaddConst p = Homeomorph.vaddConst p_1
-- Mathlib.Algebra.Group.InjSurj
/-- A type has an involutive inversion if it admits a surjective map that preserves `⁻¹` to a type
which has an involutive inversion. See note [reducible non-instances]  -/
Function.Surjective.involutiveInv : {M₁ : Type u_1} →
  {M₂ : Type u_3} →
    [inst : Inv M₂] →
      [inst_1 : InvolutiveInv M₁] →
        (f : M₁ → M₂) → Function.Surjective f → (∀ (x : M₁), f x⁻¹ = (f x)⁻¹) → InvolutiveInv M₂
-- Init.Data.SInt.Lemmas
Int32.toUInt32_mul : ∀ (a b : Int32), (a * b).toUInt32 = a.toUInt32 * b.toUInt32
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_diff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, (m₁ \ m₂).getKey? k = if k ∈ m₂ then none else m₁.getKey? k
-- Std.Data.HashSet.Lemmas
Std.HashSet.get!_eq_default_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : Inhabited α] [EquivBEq α] [LawfulHashable α]
  {a : α}, m.contains a = false → m.get! a = default
-- Mathlib.RingTheory.ChainOfDivisors
emultiplicity_prime_le_emultiplicity_image_by_factor_orderIso : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {N : Type u_2} [inst_2 : CommMonoidWithZero N]
  [UniqueFactorizationMonoid N] [inst_4 : UniqueFactorizationMonoid M] {m p : Associates M} {n : Associates N}
  (hp : p ∈ UniqueFactorizationMonoid.normalizedFactors m) (d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)),
  emultiplicity p m ≤ emultiplicity (↑(d ⟨p, ⋯⟩)) n
-- Mathlib.Combinatorics.SetFamily.Kleitman
/-- **Kleitman's theorem**. An intersecting family on `n` elements contains at most `2ⁿ⁻¹` sets, and
each further intersecting family takes at most half of the sets that are in no previous family.  -/
Finset.card_biUnion_le_of_intersecting : ∀ {ι : Type u_1} {α : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq α] [Nonempty α] (s : Finset ι)
  (f : ι → Finset (Finset α)),
  (∀ i ∈ s, (↑(f i)).Intersecting) → (s.biUnion f).card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - s.card)
-- Mathlib.RingTheory.IsTensorProduct
IsBaseChange.algHom_ext : ∀ {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  [inst_2 : CommSemiring R] [inst_3 : CommSemiring S] [inst_4 : Algebra R S] [inst_5 : Module R M] [inst_6 : Module R N]
  [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] {f : M →ₗ[R] N},
  IsBaseChange S f →
    ∀ {Q : Type u_3} [inst_9 : AddCommMonoid Q] [inst_10 : Module S Q] (g₁ g₂ : N →ₗ[S] Q),
      (∀ (x : M), g₁ (f x) = g₂ (f x)) → g₁ = g₂
-- Mathlib.LinearAlgebra.QuadraticForm.Isometry
QuadraticMap.Isometry.comp_assoc : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {M₃ : Type u_5} {M₄ : Type u_6} {N : Type u_7} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M₁] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : AddCommMonoid M₄]
  [inst_5 : AddCommMonoid N] [inst_6 : Module R M₁] [inst_7 : Module R M₂] [inst_8 : Module R M₃] [inst_9 : Module R M₄]
  [inst_10 : Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} {Q₃ : QuadraticMap R M₃ N}
  {Q₄ : QuadraticMap R M₄ N} (h : Q₃ →qᵢ Q₄) (g : Q₂ →qᵢ Q₃) (f : Q₁ →qᵢ Q₂), (h.comp g).comp f = h.comp (g.comp f)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.ker_Pi_Quotient_mk : ∀ {R : Type u} [inst : Ring R] {ι : Type u_1} (I : ι → Ideal R) [inst_1 : ∀ (i : ι), (I i).IsTwoSided],
  RingHom.ker (RingHom.pi fun i => Ideal.Quotient.mk (I i)) = ⨅ i, I i
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.algebraMap_leftInverse : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R],
  Function.LeftInverse ⇑FreeAlgebra.algebraMapInv ⇑(algebraMap R (FreeAlgebra R X))
-- Mathlib.Data.Set.Piecewise
Set.le_piecewise : ∀ {α : Type u_1} {δ : α → Type u_8} [inst : (i : α) → Preorder (δ i)] {s : Set α} [inst_1 : (j : α) → Decidable (j ∈ s)]
  {f₁ f₂ g : (i : α) → δ i}, (∀ i ∈ s, g i ≤ f₁ i) → (∀ i ∉ s, g i ≤ f₂ i) → g ≤ s.piecewise f₁ f₂
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.iCycles_g_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology] {Z : C} (h : S.X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.iCycles (CategoryTheory.CategoryStruct.comp S.g h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Analysis.Normed.Group.Basic
enorm_eq_iff_norm_eq : ∀ {E : Type u_5} {F : Type u_6} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F] {x : E} {y : F},
  ‖x‖ₑ = ‖y‖ₑ ↔ ‖x‖ = ‖y‖
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.addSemigroup : {α : Type u} → [AddSemigroup α] → AddSemigroup (WithBot α)
-- Mathlib.Order.Defs.Unbundled
irrefl_of : ∀ {α : Sort u_1} (r : α → α → Prop) [Std.Irrefl r] (a : α), ¬r a a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getEntryLE_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α} {h' : ∃ a ∈ t₁, (cmp a k).isLE = true} (h : t₁.Equiv t₂), t₁.getEntryLE k h' = t₂.getEntryLE k ⋯
-- Mathlib.Algebra.Category.Ring.Under.Property
RingHom.HasFiniteProducts.isClosedUnderLimitsOfShape : ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) →
    (RingHom.HasFiniteProducts fun {R S} [CommRing R] [CommRing S] => Q) →
      ∀ (R : CommRingCat),
        (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => Q).underObj.IsClosedUnderFiniteProducts
-- Aesop.Search.Main
Aesop.expandNextGoal : {Q : Type} → [inst : Aesop.Queue Q] → Aesop.SearchM Q Unit
-- Mathlib.Algebra.Group.Indicator
Set.indicator_sdiff : ∀ {α : Type u_1} {G : Type u_6} [inst : AddGroup G] {s t : Set α},
  s ⊆ t → ∀ (f : α → G), (t \ s).indicator f = t.indicator f - s.indicator f
-- Mathlib.LinearAlgebra.Dual.Defs
LinearEquiv.dualMap_symm : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] {f : M₁ ≃ₗ[R] M₂},
  f.dualMap.symm = f.symm.dualMap
-- Mathlib.Data.ZMod.Basic
ZMod.inv_eq_of_mul_eq_one : ∀ (n : ℕ) (a b : ZMod n), a * b = 1 → a⁻¹ = b
-- Mathlib.Algebra.CubicDiscriminant
Cubic.equiv_symm_apply_c : ∀ {R : Type u_1} [inst : Semiring R] (f : { p // p.degree ≤ 3 }), (Cubic.equiv.symm f).c = (↑f).coeff 1
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.subtype_comp_inclusion : ∀ {M : Type u_1} [inst : AddZeroClass M] {S T : AddSubmonoid M} (h : S ≤ T),
  T.subtype.comp (AddSubmonoid.inclusion h) = S.subtype
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.interface.sizeOf_spec : sizeOf Lean.Lsp.CompletionItemKind.interface = 1
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min?_le_min?_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k km kme : α}
  (hkme : (t.erase k).min? = some kme), t.min?.get ⋯ = km → (cmp km kme).isLE = true
-- Mathlib.RingTheory.LaurentSeries
/-- Two Laurent series whose difference has small valuation have the same coefficients for
small enough indices.  -/
LaurentSeries.eq_coeff_of_valuation_sub_lt : ∀ (K : Type u_2) [inst : Field K] {d n : ℤ} {f g : LaurentSeries K},
  Valued.v (g - f) ≤ WithZero.exp (-d) → n < d → g.coeff n = f.coeff n
-- Mathlib.Data.List.Sort
StrictAnti.sortedLE_listMap : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {l : List α},
  StrictAnti f → ((List.map f l).SortedLE ↔ l.SortedGE)
-- Init.Data.Int.Gcd
Int.lcm_zero : ∀ {a : ℤ}, a.lcm 0 = 0
-- Mathlib.Tactic.Linarith.Datatypes
/-- The main datatype for FM elimination.
Variables are represented by natural numbers, each of which has an integer coefficient.
Index 0 is reserved for constants, i.e. `coeffs.find 0` is the coefficient of 1.
The represented term is `coeffs.sum (fun ⟨k, v⟩ ↦ v * Var[k])`.
str determines the strength of the comparison -- is it < 0, ≤ 0, or = 0?
 -/
Mathlib.Tactic.Linarith.Comp : Type
-- Mathlib.NumberTheory.NumberField.Ideal.Asymptotics
_private.Mathlib.NumberTheory.NumberField.Ideal.Asymptotics.0.NumberField.Ideal.tendsto_norm_le_and_mk_eq_div_atTop_aux₂ : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      {J : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))} →
        {s : ℝ} →
          ↑({x |
                  x ∈
                      ⇑(NumberField.mixedEmbedding.euclidean.toMixed K) ⁻¹'
                        NumberField.mixedEmbedding.fundamentalCone K ∧
                    NumberField.mixedEmbedding.norm ((NumberField.mixedEmbedding.euclidean.toMixed K) x) ≤ s} ∩
                ↑(ZLattice.comap ℝ (NumberField.mixedEmbedding.idealLattice K ((FractionalIdeal.mk0 K) J))
                    ↑↑(NumberField.mixedEmbedding.euclidean.toMixed K))) ≃
            { a // NumberField.mixedEmbedding.norm ↑a ≤ s }
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
/-- Define what it means for a functor `F : C ⥤ D` to reflect isomorphisms: for any
morphism `f : A ⟶ B`, if `F.map f` is an isomorphism then `f` is as well.
Note that we do not assume or require that `F` is faithful.
 -/
CategoryTheory.Functor.ReflectsIsomorphisms : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} → [inst_1 : CategoryTheory.Category.{v_2, u_2} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.FinMeasSupp.lintegral_lt_top : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α ENNReal},
  f.FinMeasSupp μ → (∀ᵐ (a : α) ∂μ, f a ≠ ⊤) → f.lintegral μ < ⊤
-- Mathlib.Order.WellFoundedSet
Set.partiallyWellOrderedOn_singleton : ∀ {α : Type u_2} {r : α → α → Prop} [Std.Refl r] (a : α), {a}.PartiallyWellOrderedOn r
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.mem_Icc_algebraMap_iff_nnnorm_le : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {x : A} {r : NNReal},
  x ∈ Set.Icc 0 ((algebraMap NNReal A) r) ↔ 0 ≤ x ∧ ‖x‖₊ ≤ r
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIso.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIso C =
    CategoryTheory.NatIso.ofComponents
      (fun F => CategoryTheory.Mon.mkIso (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux C F) ⋯ ⋯) ⋯
-- Mathlib.Topology.Instances.Rat
NNRat.instIsTopologicalSemiring : IsTopologicalSemiring ℚ≥0
-- Mathlib.LinearAlgebra.AnnihilatingPolynomial
/-- The generator of the annihilating ideal has minimal degree among
the non-zero members of the annihilating ideal  -/
Polynomial.degree_annIdealGenerator_le_of_mem : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] (a : A),
  ∀ p ∈ Polynomial.annIdeal 𝕜 a, p ≠ 0 → (Polynomial.annIdealGenerator 𝕜 a).degree ≤ p.degree
-- Std.Sat.AIG.RefVecOperator.Fold
Std.Sat.AIG.RefVec.fold.go.eq_def : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (acc : aig.Ref) (idx len : ℕ)
  (input : aig.RefVec len) (f : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α)
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f],
  Std.Sat.AIG.RefVec.fold.go aig acc idx len input f =
    if hidx : idx < len then
      let res := f aig { lhs := acc, rhs := input.get idx hidx };
      let aig_1 := res.aig;
      have newAcc := res.ref;
      have input := input.cast ⋯;
      Std.Sat.AIG.RefVec.fold.go aig_1 newAcc (idx + 1) len input f
    else { aig := aig, ref := acc }
-- Mathlib.Algebra.Quandle
/-- The composition of shelf homomorphisms  -/
ShelfHom.comp : {S₁ : Type u_1} →
  {S₂ : Type u_2} →
    {S₃ : Type u_3} →
      [inst : Shelf S₁] → [inst_1 : Shelf S₂] → [inst_2 : Shelf S₃] → ShelfHom S₂ S₃ → ShelfHom S₁ S₂ → ShelfHom S₁ S₃
-- Std.Data.DHashMap.Internal.AssocList.Iterator
Std.DHashMap.Internal.AssocList.AssocListIterator.mk : {α : Type u} →
  {β : α → Type v} → Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList.AssocListIterator α β
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
AlgebraicTopology.DoldKan.PInfty_f_comp_QInfty_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (n : ℕ) {Z : C}
  (h : (AlgebraicTopology.AlternatingFaceMapComplex.obj X).X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n)
      (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.QInfty.f n) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rio_eq_append : ∀ {n : ℕ}, 0 < n → (*...n).toList = (*...n - 1).toList ++ [n - 1]
-- Mathlib.Topology.Order.LeftRightLim
leftLim_eq_of_isBot : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace β] {f : α → β} {a : α},
  IsBot a → Function.leftLim f a = f a
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.ElementaryEmbedding.mk : {L : FirstOrder.Language} →
  {M : Type u_1} →
    {N : Type u_2} →
      [inst : L.Structure M] →
        [inst_1 : L.Structure N] →
          (toFun : M → N) →
            autoParam (∀ ⦃n : ℕ⦄ (φ : L.Formula (Fin n)) (x : Fin n → M), φ.Realize (toFun ∘ x) ↔ φ.Realize x)
                FirstOrder.Language.ElementaryEmbedding.map_formula'._autoParam →
              L.ElementaryEmbedding M N
-- Init.Data.Iterators.Consumers.Loop
/-- Steps through the whole iterator, counting the number of outputs emitted.

**Performance**:

This function's runtime is linear in the number of steps taken by the iterator.
 -/
Std.Iter.count : {α β : Type u_1} → [inst : Std.Iterator α Id β] → [Std.IteratorLoop α Id Id] → Std.Iter β → ℕ
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.fromCols_toCols : ∀ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ ⊕ n₂) R),
  A.toCols₁.fromCols A.toCols₂ = A
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
FundamentalGroupoidFunctor.projLeft_map : ∀ (A : TopCat) (B : TopCat) (x₀ x₁ : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of (↑A × ↑B))))
  (p : x₀ ⟶ x₁), (FundamentalGroupoidFunctor.projLeft A B).map p = Path.Homotopic.projLeft p
-- Mathlib.Algebra.Exact.Basic
Function.Exact.addMonoidHom_comp_eq_zero : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : AddGroup M] [inst_1 : AddGroup N] [inst_2 : AddGroup P]
  {f : M →+ N} {g : N →+ P}, Function.Exact ⇑f ⇑g → g.comp f = 0
-- Mathlib.Tactic.Convert
_private.Mathlib.Tactic.Convert.0.Convert.elabCheapConfig.evalConfigItem : Lean.Elab.ConfigEval.EvalConfigItem Convert.CheapConfig
-- ProofWidgets.Component.Basic
ProofWidgets.InteractiveExprProps.expr : ProofWidgets.InteractiveExprProps → Lean.Server.WithRpcRef ProofWidgets.ExprWithCtx
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.variable.sizeOf_spec : sizeOf Lean.Lsp.CompletionItemKind.variable = 1
-- Mathlib.Dynamics.FixedPoints.Basic
Function.IsFixedPt.perm_zpow : ∀ {α : Type u_1} {x : α} {e : Equiv.Perm α}, Function.IsFixedPt (⇑e) x → ∀ (n : ℤ), Function.IsFixedPt (⇑(e ^ n)) x
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.eq_bot_of_subsingleton : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [Subsingleton ↥H], H = ⊥
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.map_smulₛₗ : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f : M →ₛₗ[σ] M₃) (c : R) (x : M), f (c • x) = σ c • f x
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.ReflectsColimitsOfSize.reflectsColimitsOfShape : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} [self : CategoryTheory.Limits.ReflectsColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J], CategoryTheory.Limits.ReflectsColimitsOfShape J F
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.coconeOfPredicateSet_pt : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] {J : CategoryTheory.CardinalDirectedPoset κ} (P : Set ↑J.obj → Prop)
  [inst_1 : ∀ (S : Subtype P), CategoryTheory.IsCardinalFiltered (↑↑S) κ],
  (CategoryTheory.CardinalDirectedPoset.coconeOfPredicateSet P).pt = J
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.fun.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (decl : Lean.Compiler.LCNF.FunDecl pu) (k : Lean.Compiler.LCNF.Code pu)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.Alt._auto_5),
  sizeOf (Lean.Compiler.LCNF.Code.fun decl k h) = 1 + sizeOf decl + sizeOf k + sizeOf h
-- Aesop.Stats.Basic
Aesop.instMonadStatsOfMonadOptionsOfMonadStateOfStats : {m : Type → Type} → [Lean.MonadOptions m] → [MonadStateOf Aesop.Stats m] → Aesop.MonadStats m
-- Mathlib.Data.List.Rotate
List.length_cyclicPermutations_of_ne_nil : ∀ {α : Type u} (l : List α), l ≠ [] → l.cyclicPermutations.length = l.length
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.mk_coe' : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) (f : M₂ → M)
  (h₁ : ∀ (x y : M₂), f (x + y) = f x + f y)
  (h₂ :
    ∀ (m : S) (x : M₂), { toFun := f, map_add' := h₁ }.toFun (m • x) = σ' m • { toFun := f, map_add' := h₁ }.toFun x)
  (h₃ : Function.LeftInverse ⇑e { toFun := f, map_add' := h₁, map_smul' := h₂ }.toFun)
  (h₄ : Function.RightInverse ⇑e { toFun := f, map_add' := h₁, map_smul' := h₂ }.toFun),
  { toFun := f, map_add' := h₁, map_smul' := h₂, invFun := ⇑e, left_inv := h₃, right_inv := h₄ } = e.symm
-- Mathlib.Order.Monotone.Basic
strictMono_toDual_comp_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  StrictMono (⇑OrderDual.toDual ∘ f) ↔ StrictAnti f
-- Init.Data.SInt.Basic
/-- Converts 8-bit signed integers to 32-bit signed integers that denote the same number.

This function is overridden at runtime with an efficient implementation.
 -/
Int16.toInt32 : Int16 → Int32
-- Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Ideal.minimalPrimes_isPrime : ∀ {R : Type u_1} [inst : CommSemiring R] {p : Ideal R}, p ∈ minimalPrimes R → p.IsPrime
-- Lean.Elab.Tactic.Grind.Param
Lean.Meta.Grind.ExtensionStateArray.find : Lean.Meta.Grind.ExtensionStateArray → Lean.Meta.Grind.Origin → List Lean.Meta.Grind.EMatchTheorem
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.obj.σ_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.LaxMonoidal] (X : C) [inst_5 : CategoryTheory.AddMonObj X],
  CategoryTheory.AddMonObj.add =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X X) (F.map CategoryTheory.AddMonObj.add)
-- Mathlib.Logic.Relation
Relation.equivalence_join_reflTransGen : ∀ {α : Type u_1} {r : α → α → Prop},
  (∀ (a b c : α), r a b → r a c → ∃ d, Relation.ReflGen r b d ∧ Relation.ReflTransGen r c d) →
    Equivalence (Relation.Join (Relation.ReflTransGen r))
-- Init.Omega.Constraint
/-- Scale a constraint by multiplying by an integer.
* If `k = 0` this is either impossible, if the original constraint was impossible,
  or the `= 0` exact constraint.
* If `k` is positive this takes `[x, y]` to `[k * x, k * y]`
* If `k` is negative this takes `[x, y]` to `[k * y, k * x]`.
 -/
Lean.Omega.Constraint.scale : ℤ → Lean.Omega.Constraint → Lean.Omega.Constraint
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.isEmpty_toList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α], (Std.DHashMap.Const.toList m).isEmpty = m.isEmpty
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.IsVeryGood.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] {P : HomotopicalAlgebra.Cylinder A}
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A A] [inst_3 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_4 : HomotopicalAlgebra.CategoryWithFibrations C] [toIsGood : P.IsGood],
  autoParam (HomotopicalAlgebra.Fibration P.π) HomotopicalAlgebra.Cylinder.IsVeryGood.fibration_π._autoParam →
    P.IsVeryGood
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.WorkGroup.mk : Std.Format.FlattenAllowability → Std.Format.FlattenBehavior → List Std.Format.WorkItem✝ → Std.Format.WorkGroup✝
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_eq_some_get! : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF → ∀ {a : α} [inst_3 : Inhabited (β a)], m.contains a = true → m.get? a = some (m.get! a)
-- Mathlib.Data.Bool.Basic
/-- **Kaminski's Equation**  -/
Bool.apply_apply_apply : ∀ (f : Bool → Bool) (x : Bool), f (f (f x)) = f x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.e_hom_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X),
  (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.e F G X).hom.app X_1 = X_1.iso.hom
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.Discrete.eqToIso'.congr_simp : ∀ {α : Type u₁} {a b : α} (h : a = b), CategoryTheory.Discrete.eqToIso' h = CategoryTheory.Discrete.eqToIso' h
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.WF.containsThenInsert : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} {a : α} {b : β},
  m.WF → (m.containsThenInsert a b).2.WF
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
/-- Special case of `Topology.IsClosedEmbedding.map_tsum`, logically weaker but
possibly easier to apply in practice.  -/
Function.LeftInverse.map_tsum : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
  {L : SummationFilter β} {G : Type u_4} (f : β → α) [inst_2 : AddCommMonoid γ] [inst_3 : TopologicalSpace γ]
  [T2Space γ] {g : G} [inst_5 : FunLike G α γ] [AddMonoidHomClass G α γ],
  Continuous ⇑g →
    ∀ {g' : γ → α}, Continuous g' → Function.LeftInverse g' ⇑g → g (∑'[L] (b : β), f b) = ∑'[L] (b : β), g (f b)
-- Mathlib.Topology.Inseparable
inseparable_pi : ∀ {ι : Type u_5} {A : ι → Type u_6} [inst : (i : ι) → TopologicalSpace (A i)] {f g : (i : ι) → A i},
  Inseparable f g ↔ ∀ (i : ι), Inseparable (f i) (g i)