mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
map_complEDS' : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {F : Type u_3} [inst_2 : FunLike F R S]
  [RingHomClass F R S] (f : F) (b c d : R) (k : ℤ) (n : ℕ), f (complEDS' b c d k n) = complEDS' (f b) (f c) (f d) k n
-- Mathlib.GroupTheory.PresentedGroup
/-- Presented groups of isomorphic types are isomorphic.  -/
PresentedGroup.equivPresentedGroup : {α : Type u_1} →
  {β : Type u_2} →
    (rels : Set (FreeGroup α)) →
      (e : α ≃ β) → PresentedGroup rels ≃* PresentedGroup (⇑(FreeGroup.freeGroupCongr e) '' rels)
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_surjective : ∀ {b : ℝ}, 0 < b → b ≠ 1 → Function.Surjective (Real.logb b)
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
/-- The underlying seminormed abelian group.  -/
SemiNormedGrp.carrier : SemiNormedGrp → Type u
-- Mathlib.Tactic.Push.Attr
Mathlib.Tactic.Push.Head.const : Lean.Name → Mathlib.Tactic.Push.Head
-- Mathlib.Topology.Homotopy.HomotopyGroup
HomotopyGroup.transAt_indep : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} [inst_1 : DecidableEq N] {i : N} (j : N)
  (f g : ↑(GenLoop N X x)), ⟦GenLoop.transAt i f g⟧ = ⟦GenLoop.transAt j f g⟧
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braiding_hom_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.BraidedCategory C]
  (X₁ X₂ : CategoryTheory.Arrow C),
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braiding X₁ X₂).hom.left =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pushoutSymmetry (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom)).hom
      (CategoryTheory.Limits.HasColimit.isoOfNatIso
          (CategoryTheory.Limits.spanExt (β_ X₁.left X₂.left) (β_ X₁.left X₂.right) (β_ X₁.right X₂.left) ⋯ ⋯)).hom
-- Mathlib.Logic.Encodable.Basic
Prop.encodable : Encodable Prop
-- Mathlib.Util.SynthesizeUsing
/-- `synthesizeUsing type tacticSyntax` synthesizes an element of type `type` by evaluating the
given tactic syntax.

Example:
```lean
let (gs, e) ← synthesizeUsingTactic ty (← `(tactic| congr!))
```

The tactic `tac` is allowed to leave goals open, and these remain as metavariables in the
returned expression.
 -/
synthesizeUsingTactic : {u : Lean.Level} → (type : Q(Sort u)) → Lean.Syntax → Lean.MetaM (List Lean.MVarId × Q(«$type»))
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- Upgrading a functor `E ⥤ C` to a functor `E ⥤ CostructuredArrow F X` and composing with the
forgetful functor `CostructuredArrow F X ⥤ C` recovers the original functor.  -/
CategoryTheory.Functor.toCostructuredArrowCompProj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (G : CategoryTheory.Functor E C) →
              (F : CategoryTheory.Functor C D) →
                (X : D) →
                  (f : (Y : E) → F.obj (G.obj Y) ⟶ X) →
                    (h : ∀ {Y Z : E} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (F.map (G.map g)) (f Z) = f Y) →
                      (G.toCostructuredArrow F X f ⋯).comp (CategoryTheory.CostructuredArrow.proj F X) ≅ G
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.isVonNBounded_sUnion : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : Zero E]
  [inst_3 : TopologicalSpace E] {S : Set (Set E)},
  S.Finite → (Bornology.IsVonNBounded 𝕜 (⋃₀ S) ↔ ∀ s ∈ S, Bornology.IsVonNBounded 𝕜 s)
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.ι₁_app_fst : ∀ {X : SSet} {m : SimplexCategoryᵒᵖ} (x : X.obj m), ((CategoryTheory.ConcreteCategory.hom (SSet.ι₁.app m)) x).1 = x
-- Mathlib.Topology.UniformSpace.Ultra.Basic
IsTransitiveRel.prod_subset_trans : ∀ {X : Type u_1} {s : SetRel X X} {t u v : Set X} [s.IsTrans], t ×ˢ u ⊆ s → u ×ˢ v ⊆ s → u.Nonempty → t ×ˢ v ⊆ s
-- Mathlib.Algebra.Order.Monoid.Units
AddUnits.instLinearOrder.eq_1 : ∀ {α : Type u_1} [inst : AddMonoid α] [inst_1 : LinearOrder α],
  AddUnits.instLinearOrder = Function.Injective.linearOrder AddUnits.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueSums.of_addHom : ∀ {G : Type u} {H : Type v} [inst : Add G] [inst_1 : Add H] (f : H →ₙ+ G),
  (∀ ⦃a b c d : H⦄, a + b = c + d → f a = f c ∧ f b = f d → a = c ∧ b = d) → ∀ [UniqueSums G], UniqueSums H
-- Init.Prelude
/-- A (named) binary parser, like `orelse` or `andthen`
(written as `p1 <|> p2` and `p1 p2` respectively in `syntax`)  -/
Lean.ParserDescr.binary : Lean.Name → Lean.ParserDescr → Lean.ParserDescr → Lean.ParserDescr
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.ofSliceTo_lt_ofSliceTo_iff : ∀ {s : String.Slice} {p : s.Pos} {q r : (s.sliceTo p).Pos},
  String.Slice.Pos.ofSliceTo q < String.Slice.Pos.ofSliceTo r ↔ q < r
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.add_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : AddCommMonoid α] [inst_1 : Preorder α] [inst_2 : AddCommMonoid β]
  [inst_3 : Preorder β] [inst_4 : AddCommMonoid γ] [inst_5 : Preorder γ] [inst_6 : IsOrderedAddMonoid γ]
  (g₁ g₂ : β →+o γ) (f : α →+o β), (g₁ + g₂).comp f = g₁.comp f + g₂.comp f
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_filter_eq_false_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool},
  t.WF → ((Std.DTreeMap.Raw.filter f t).isEmpty = false ↔ ∃ k, ∃ (h : k ∈ t), f k (t.get k h) = true)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyOutgoingCallsParams.mk : Lean.Lsp.CallHierarchyItem → Lean.Lsp.CallHierarchyOutgoingCallsParams
-- Init.Data.List.Perm
List.Perm.any_eq : ∀ {α : Type u_1} {l₁ l₂ : List α} {f : α → Bool}, l₁.Perm l₂ → l₁.any f = l₂.any f
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.ofLinearEquiv_trans_ofLinearEquiv : ∀ {k : Type u_10} {V : Type u_11} {P : Type u_12} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (A B : V ≃ₗ[k] V) (p₀ p₁ p₂ : P),
  (AffineEquiv.ofLinearEquiv A p₀ p₁).trans (AffineEquiv.ofLinearEquiv B p₁ p₂) =
    AffineEquiv.ofLinearEquiv (A ≪≫ₗ B) p₀ p₂
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.inradius_eq_abs_inv_sum : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n),
  s.inradius = |(∑ i, s.excenterWeightsUnnorm ∅ i)⁻¹|
-- Mathlib.Data.Finset.Range
Finset.range_nontrivial : ∀ {n : ℕ}, 1 < n → (Finset.range n).Nontrivial
-- Init.Data.ByteArray.Lemmas
List.getElem_toByteArray : ∀ {l : List UInt8} {i : ℕ} {h : i < l.toByteArray.size}, l.toByteArray[i] = l[i]
-- Mathlib.Data.ENNReal.Operations
ENNReal.biSup_add : ∀ {a : ENNReal} {ι : Type u_3} {s : Set ι}, s.Nonempty → ∀ (f : ι → ENNReal), (⨆ i ∈ s, f i) + a = ⨆ i ∈ s, f i + a
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.le_zero_iff : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {I : FractionalIdeal S P}, I ≤ 0 ↔ I = 0
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.le_startPos : ∀ {s : String.Slice} (p : s.Pos), p ≤ s.startPos ↔ p = s.startPos
-- Mathlib.RingTheory.TensorProduct.Maps
Module.End.rTensorAlgHom_apply_apply : ∀ (R : Type u_1) (M : Type u_2) (N : Type u_3) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (a : Module.End R M) (a_1 : TensorProduct R M N),
  ((Module.End.rTensorAlgHom R M N) a) a_1 = (TensorProduct.liftAux (TensorProduct.mk R M N ∘ₗ a)) a_1
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.bot_prod_bot : ∀ {N : Type u_2} [inst : AddZeroClass N] {M : Type u_5} [inst_1 : AddZeroClass M], ⊥.prod ⊥ = ⊥
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The functor from augmented objects to arrows.  -/
CategoryTheory.CosimplicialObject.Augmented.toArrow : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor (CategoryTheory.CosimplicialObject.Augmented C) (CategoryTheory.Arrow C)
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Ico_castLE : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n m : ℕ} (h : n ≤ m) (f : Fin m → M) (a b : Fin n),
  ∑ i ∈ Finset.Ico (Fin.castLE h a) (Fin.castLE h b), f i = ∑ i ∈ Finset.Ico a b, f (Fin.castLE h i)
-- Mathlib.Algebra.Notation.Pi.Basic
Pi.single_ne_zero_iff : ∀ {ι : Type u_1} {M : ι → Type u_6} [inst : (i : ι) → Zero (M i)] [inst_1 : DecidableEq ι] {i : ι} {x : M i},
  Pi.single i x ≠ 0 ↔ x ≠ 0
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- A regular epimorphism is a morphism which is the coequalizer of some parallel pair.  -/
CategoryTheory.RegularEpi : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : C} → (X ⟶ Y) → Type (max u₁ v₁)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.DelayedTheoremInstance.thm : Lean.Meta.Grind.DelayedTheoremInstance → Lean.Meta.Grind.EMatchTheorem
-- Mathlib.Data.Fin.Tuple.Basic
Fin.find_pos : ∀ {n : ℕ} {p : Fin (n + 1) → Prop} [inst : DecidablePred p] (h : ∃ i, p i), 0 < Fin.find p h ↔ ¬p 0
-- Mathlib.Data.Bool.Basic
Bool.coe_true : (true = true) = True
-- Init.Data.Range.Polymorphic.UInt
UInt32.rxiHasSize_eq_toBitVec : ∀ {lo : BitVec 32}, Std.Rxi.HasSize.size { toBitVec := lo } = Std.Rxi.HasSize.size lo
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.mem_congr : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x y : α} [Std.TransCmp cmp] {t : RBTree.RBNode α},
  cmp x y = Ordering.eq → (RBTree.RBNode.Mem cmp x t ↔ RBTree.RBNode.Mem cmp y t)
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.of_add : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (c : ↥(LieModule.Cohomology.twoCocycle R L M)) (x y : L × M),
  (LieAlgebra.ofProd c) (x + y) = (LieAlgebra.ofProd c) x + (LieAlgebra.ofProd c) y
-- Mathlib.Algebra.Group.Action.Defs
/-- This cannot be an instance because it can cause infinite loops whenever the `VAdd` arguments
are still metavariables.  -/
VAdd.comp.vaddCommClass : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [inst : VAdd M α] [inst_1 : VAdd β α]
  [VAddCommClass M β α] (g : N → M), VAddCommClass N β α
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.string.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenType.string = 1
-- Mathlib.Algebra.Order.Group.Synonym
isRightRegular_ofDual : ∀ {α : Type u_1} [inst : Monoid α] {a : αᵒᵈ}, IsRightRegular (OrderDual.ofDual a) ↔ IsRightRegular a
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.symmₗ.congr_simp : ∀ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : AddCommMonoid F]
  [inst_5 : Module R F] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module R (E x)]
  (e e_1 : Bundle.Trivialization F Bundle.TotalSpace.proj) (e_e : e = e_1) [inst_8 : Bundle.Trivialization.IsLinear R e]
  (b : B), Bundle.Trivialization.symmₗ R e b = Bundle.Trivialization.symmₗ R e_1 b
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
mulRightMono_of_mulRightStrictMono : ∀ (M : Type u_3) [inst : Mul M] [inst_1 : PartialOrder M] [MulRightStrictMono M], MulRightMono M
-- Init.Data.BEq
EquivBEq.toPartialEquivBEq : ∀ {α : Type u_1} {inst : BEq α} [self : EquivBEq α], PartialEquivBEq α
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Section.rightHom_comp_section : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  {S : GroupExtension N E G} (σ : S.Section), ⇑S.rightHom ∘ ⇑σ = id
-- Mathlib.Topology.MetricSpace.Bounded
/-- If the distance between any two points in a set is bounded by some non-negative constant,
this constant bounds the diameter.  -/
Metric.diam_le_of_forall_dist_le : ∀ {α : Type u} {s : Set α} [inst : PseudoMetricSpace α] {C : ℝ},
  0 ≤ C → (∀ x ∈ s, ∀ y ∈ s, dist x y ≤ C) → Metric.diam s ≤ C
-- Std.Time.Zoned.RecurringRule
Std.Time.TimeZone.TransitionSpec.mwd.inj : ∀ {month : Std.Time.Month.Ordinal} {week : Std.Time.Week.Aligned.Ordinal} {day : Std.Time.Weekday.Ordinal}
  {month_1 : Std.Time.Month.Ordinal} {week_1 : Std.Time.Week.Aligned.Ordinal} {day_1 : Std.Time.Weekday.Ordinal},
  Std.Time.TimeZone.TransitionSpec.mwd month week day = Std.Time.TimeZone.TransitionSpec.mwd month_1 week_1 day_1 →
    month = month_1 ∧ week = week_1 ∧ day = day_1
-- Mathlib.Data.Fintype.List
Multiset.lists_nodup_finset : ∀ {α : Type u_1} (l : Finset α), l.val.lists.Nodup
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.valuation_LaurentSeries_equal_extension : ∀ (K : Type u_2) [inst : Field K], ⋯.extend ⇑Valued.v = ⇑Valued.v
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.aestronglyMeasurable_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : Zero β], MeasureTheory.AEStronglyMeasurable 0 μ
-- Init.Data.String.Slice
String.Slice.RevSplitIterator.atEnd.sizeOf_spec : ∀ {σ : String.Slice → Type} {ρ : Type} {pat : ρ} {s : String.Slice}
  [inst : String.Slice.Pattern.ToBackwardSearcher pat σ] [inst_1 : (a : String.Slice) → SizeOf (σ a)]
  [inst_2 : SizeOf ρ], sizeOf String.Slice.RevSplitIterator.atEnd = 1
-- Lean.Data.Json.Parser
Lean.Json.Parser.str : Std.Internal.Parsec.String.Parser String
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.imp_1eq_cert.eq_1 : ∀ (lhs rhs : Lean.Grind.CommRing.Expr) (p₁ p₂ : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.imp_1eq_cert lhs rhs p₁ p₂ =
    ((lhs.sub rhs).toPoly_k.beq' p₁).and' (p₂.beq' (Lean.Grind.CommRing.Poly.num 0))
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.Functor.OplaxMonoidal.lift_δ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) {X Y Z : C} [inst_4 : F.OplaxMonoidal] (f : X ⟶ Y) (g : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CartesianMonoidalCategory.lift f g))
      (CategoryTheory.Functor.OplaxMonoidal.δ F Y Z) =
    CategoryTheory.CartesianMonoidalCategory.lift (F.map f) (F.map g)
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
LineDifferentiableAt.congr_of_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f f₁ : E → F}
  {x v : E}, LineDifferentiableAt 𝕜 f x v → f₁ =ᶠ[nhds x] f → LineDifferentiableAt 𝕜 f₁ x v
-- Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
/-- If the product `X ⨯ Y` and the equalizer of `π₁ ≫ f` and `π₂ ≫ g` exist, then the
pullback of `f` and `g` exists: It is given by composing the equalizer with the projections.  -/
CategoryTheory.Limits.hasLimit_cospan_of_hasLimit_pair_of_hasLimit_parallelPair : ∀ {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.pair X Y)]
  [CategoryTheory.Limits.HasLimit
      (CategoryTheory.Limits.parallelPair (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst f)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd g))],
  CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan f g)
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instInhabitedPublishDiagnosticsParams.default : Lean.Lsp.PublishDiagnosticsParams
-- Mathlib.Algebra.Group.Indicator
map_mulIndicator : ∀ {α : Type u_1} {M : Type u_6} {N : Type u_7} {F : Type u_8} [inst : One M] [inst_1 : One N] [inst_2 : FunLike F M N]
  [OneHomClass F M N] (f : F) (s : Set α) (g : α → M) (x : α), f (s.mulIndicator g x) = s.mulIndicator (⇑f ∘ g) x
-- Plausible.Random
Plausible.Random.instBoundedRandomInt : {m : Type → Type u_1} → [Monad m] → Plausible.BoundedRandom m ℤ
-- Mathlib.Probability.Distributions.Uniform
PMF.ofMultiset.congr_simp : ∀ {α : Type u_1} (s s_1 : Multiset α) (e_s : s = s_1) (hs : s ≠ 0), PMF.ofMultiset s hs = PMF.ofMultiset s_1 ⋯
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.forM_eq_forM_toListModel : ∀ {α : Type u} {β : α → Type v} {l : Std.DHashMap.Raw α β} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m]
  {f : (a : α) → β a → m PUnit.{w + 1}},
  Std.DHashMap.Raw.forM f l = (Std.DHashMap.Internal.toListModel l.buckets).forM fun a => f a.fst a.snd
-- Mathlib.Algebra.Category.CommBialgCat
_private.Mathlib.Algebra.Category.CommBialgCat.0.CommBialgCat.Hom.mk.sizeOf_spec : ∀ {R : Type u} [inst : CommRing R] {A B : CommBialgCat R} [inst_1 : SizeOf R] (hom' : ↑A →ₐc[R] ↑B),
  sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.map_top_of_surjective : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Function.Surjective f → (MeasureTheory.OuterMeasure.map f) ⊤ = ⊤
-- Lean.Meta.Basic
/-- Set the user-facing name for the given metavariable.
 -/
Lean.MVarId.setUserName : Lean.MVarId → Lean.Name → Lean.MetaM Unit
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
/-- The functor taking a cone over `F` to a cone over `Over.post F : Over i ⥤ Over (F.obj i)`.
This takes limit cones to limit cones when `J` is cofiltered. See `isLimitConePost`  -/
CategoryTheory.Over.conePost : {J : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (F : CategoryTheory.Functor J C) →
          (i : J) →
            CategoryTheory.Functor (CategoryTheory.Limits.Cone F)
              (CategoryTheory.Limits.Cone (CategoryTheory.Over.post F))
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey!_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → ∀ {km : α}, t.maxKey! = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Analysis.SpecialFunctions.Sqrt
HasStrictDerivAt.sqrt : ∀ {f : ℝ → ℝ} {f' x : ℝ}, HasStrictDerivAt f f' x → f x ≠ 0 → HasStrictDerivAt (fun t => √(f t)) (f' / (2 * √(f x))) x
-- Mathlib.LinearAlgebra.Orientation
/-- An equivalence between indices implies an equivalence between orientations.  -/
Orientation.reindex : (R : Type u_1) →
  [inst : CommSemiring R] →
    [inst_1 : PartialOrder R] →
      [inst_2 : IsStrictOrderedRing R] →
        (M : Type u_2) →
          [inst_3 : AddCommMonoid M] →
            [inst_4 : Module R M] → {ι : Type u_4} → {ι' : Type u_5} → ι ≃ ι' → Orientation R M ι ≃ Orientation R M ι'
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.instIsFiniteMeasureSumOfFinite : ∀ {α : Type u_1} {ι : Type u_4} {m0 : MeasurableSpace α} [Finite ι] {μ : ι → MeasureTheory.Measure α}
  [∀ (i : ι), MeasureTheory.IsFiniteMeasure (μ i)], MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.sum μ)
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
/-- The object in the fiber of the base object.  -/
CategoryTheory.Pseudofunctor.CoGrothendieck.fiber : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} →
      (self : F.CoGrothendieck) → ↑(F.obj { as := Opposite.op self.base })
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.instFintypeOfDecidableEq : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] →
      {R : Type v} → [inst_2 : CommRing R] → [Fintype R] → [DecidableEq R] → Fintype (Matrix.SpecialLinearGroup n R)
-- Mathlib.MeasureTheory.Measure.Trim
MeasureTheory.trim_measurableSet_eq : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m ≤ m0),
  MeasurableSet s → (μ.trim hm) s = μ s
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.coe_injective : ∀ {α : Type u}, Function.Injective Ultrafilter.toFilter
-- Mathlib.Analysis.Complex.Periodic
Function.Periodic.qParam_right_inv : ∀ {h : ℝ}, h ≠ 0 → ∀ {q : ℂ}, q ≠ 0 → Function.Periodic.qParam h (Function.Periodic.invQParam h q) = q
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.eRank_toNat_eq_rank : ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Fintype n] [inst_1 : CommSemiring R] (A : Matrix m n R),
  A.eRank.toNat = A.rank
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
measurable_of_isClosed : ∀ {γ : Type u_3} {δ : Type u_5} [inst : TopologicalSpace γ] [inst_1 : MeasurableSpace γ] [BorelSpace γ]
  [inst_3 : MeasurableSpace δ] {f : δ → γ}, (∀ (s : Set γ), IsClosed s → MeasurableSet (f ⁻¹' s)) → Measurable f
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerve.homEquiv_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {x y : CategoryTheory.ComposableArrows C 0}
  (f : CategoryTheory.nerveEquiv x ⟶ CategoryTheory.nerveEquiv y),
  CategoryTheory.nerve.homEquiv.symm f = SSet.Edge.mk (CategoryTheory.ComposableArrows.mk₁ f) ⋯ ⋯
-- Mathlib.Data.Set.Card
Set.encard_le_encard_iff_encard_sdiff_le_encard_sdiff : ∀ {α : Type u_1} {s t : Set α}, (s ∩ t).Finite → (s.encard ≤ t.encard ↔ (s \ t).encard ≤ (t \ s).encard)
-- Mathlib.Algebra.Free
FreeAddMagma.pure_bind : ∀ {α β : Type u} (f : α → FreeAddMagma β) (x : α), pure x >>= f = f x
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- A functor `G : C ⥤ D` sends bicones over `F` to bicones over `G.obj ∘ F` functorially.  -/
CategoryTheory.Limits.Bicones.functoriality : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {D : Type uD} →
          [inst_2 : CategoryTheory.Category.{uD', uD} D] →
            [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
              (F : J → C) →
                (G : CategoryTheory.Functor C D) →
                  [G.PreservesZeroMorphisms] →
                    CategoryTheory.Functor (CategoryTheory.Limits.Bicone F) (CategoryTheory.Limits.Bicone (G.obj ∘ F))
-- Mathlib.ModelTheory.Satisfiability
/-- A complete theory is the `completeTheory` Th(M) of one of its models.  -/
FirstOrder.Language.Theory.IsComplete.eq_complete_theory : ∀ {L : FirstOrder.Language} {T : L.Theory},
  T.IsComplete → ∀ (M : Type u_1) [inst : L.Structure M] [M ⊨ T] [Nonempty M], {φ | T ⊨ᵇ φ} = L.completeTheory M
-- Mathlib.Topology.UniformSpace.Equicontinuity
uniformEquicontinuous_iInf_rng : ∀ {ι : Type u_1} {κ : Type u_2} {α' : Type u_7} {β : Type u_8} [uβ : UniformSpace β] {u : κ → UniformSpace α'}
  {F : ι → β → α'}, UniformEquicontinuous F ↔ ∀ (k : κ), UniformEquicontinuous F
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.DischargeResult.notProved : Lean.Meta.Simp.DischargeResult
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.mkFreshExprMVarImpl : Option Lean.Expr → Lean.MetavarKind → Lean.Name → Lean.MetaM Lean.Expr