mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.scalarRestriction.eq_1 : ∀ {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.MonoidalLeftAction C D]
  {A B : C} [inst_4 : CategoryTheory.MonObj A] [inst_5 : CategoryTheory.MonObj B] (f : A ⟶ B)
  [inst_6 : CategoryTheory.IsMonHom f] (M : D) [inst_7 : CategoryTheory.ModObj B M],
  CategoryTheory.Mod.scalarRestriction f M =
    {
      smul :=
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f M)
          CategoryTheory.ModObj.smul,
      one_smul := ⋯, mul_smul := ⋯ }
-- Lean.Expr
Lean.Literal.strVal.inj : ∀ {val val_1 : String}, Lean.Literal.strVal val = Lean.Literal.strVal val_1 → val = val_1
-- Mathlib.Topology.FiberBundle.Basic
Bundle.Trivialization.symm.congr_simp : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : ∀ (x : B), Nonempty (E x)]
  (e e_1 : Bundle.Trivialization F Bundle.TotalSpace.proj),
  e = e_1 → ∀ (b : B) (y y_1 : F), y = y_1 → e.symm b y = e_1.symm b y_1
-- Std.Data.Iterators.Lemmas.Combinators.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Zip.0.Std.IterM.step_intermediateZip.match_3.eq_1 : ∀ {α₁ β₁ : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α₁ m β₁]
  (motive : Option { out // ∃ it, it.IsPlausibleOutput out } → Sort u_3) (h_1 : Unit → motive none)
  (h_2 : (out₁ : { out // ∃ it, it.IsPlausibleOutput out }) → motive (some out₁)),
  (match none with
    | none => h_1 ()
    | some out₁ => h_2 out₁) =
    h_1 ()
-- Mathlib.MeasureTheory.Measure.Haar.Quotient
/-- If `μ` satisfies `AddQuotientMeasureEqMeasurePreimage` relative to a both left-
and right-invariant measure `ν` on `G`, then it is a `G` invariant measure on `G ⧸ Γ`.  -/
MeasureTheory.AddQuotientMeasureEqMeasurePreimage.vaddInvariantMeasure_quotient : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] (ν : MeasureTheory.Measure G) {Γ : AddSubgroup G}
  {μ : MeasureTheory.Measure (G ⧸ Γ)} [MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ]
  [inst_3 : TopologicalSpace G] [IsTopologicalAddGroup G] [BorelSpace G] [PolishSpace G] [T2Space (G ⧸ Γ)]
  [SecondCountableTopology (G ⧸ Γ)] [ν.IsAddLeftInvariant] [hasFun : MeasureTheory.HasAddFundamentalDomain (↥Γ.op) G ν],
  MeasureTheory.VAddInvariantMeasure G (G ⧸ Γ) μ
-- Lean.Meta.Tactic.Grind.Injective
/-- Set of Injective theorems.  -/
Lean.Meta.Grind.InjectiveTheorems : Type
-- Mathlib.RingTheory.Extension.Presentation.Submersive
/-- The Jacobian of the composition of presentations is the product of the Jacobians.  -/
Algebra.PreSubmersivePresentation.comp_jacobian_eq_jacobian_smul_jacobian : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (Q : Algebra.PreSubmersivePresentation S T ι' σ')
  (P : Algebra.PreSubmersivePresentation R S ι σ) [inst_7 : Finite σ] [inst_8 : Finite σ'],
  (Q.comp P).jacobian = P.jacobian • Q.jacobian
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The undirected angle between two vectors. If either vector is 0,
this is π/2. See `Orientation.oangle` for the corresponding oriented angle
definition.  -/
InnerProductGeometry.angle : {V : Type u_1} → [inst : NormedAddCommGroup V] → [InnerProductSpace ℝ V] → V → V → ℝ
-- Mathlib.Data.Tree.Basic
BinaryTree.height.eq_2 : ∀ {α : Type u} (a : α) (l r : BinaryTree α), (BinaryTree.node a l r).height = max l.height r.height + 1
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `Differentiable.sub_iff_right` -/
Differentiable.fun_sub_iff_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F},
  Differentiable 𝕜 f → ((Differentiable 𝕜 fun i => f i - g i) ↔ Differentiable 𝕜 g)
-- Mathlib.Data.Nat.Nth
/-- Find the `n`-th natural number satisfying `p` (indexed from `0`, so `nth p 0` is the first
natural number satisfying `p`), or `0` if there is no such number. See also
`Subtype.orderIsoOfNat` for the order isomorphism with ℕ when `p` is infinitely often true.  -/
Nat.nth : (ℕ → Prop) → ℕ → ℕ
-- Mathlib.Combinatorics.Quiver.Cast
Quiver.Path.cast_eq_iff_heq : ∀ {U : Type u_1} [inst : Quiver U] {u v u' v' : U} (hu : u = u') (hv : v = v') (p : Quiver.Path u v)
  (p' : Quiver.Path u' v'), Quiver.Path.cast hu hv p = p' ↔ p ≍ p'
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.OplaxTrans.Modification.mk.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} [inst_2 : SizeOf B] [inst_3 : SizeOf C]
  (app : (a : B) → η.app a ⟶ θ.app a)
  (naturality :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b)) (θ.naturality f) =
          CategoryTheory.CategoryStruct.comp (η.naturality f)
            (CategoryTheory.Bicategory.whiskerRight (app a) (G.map f)))
      CategoryTheory.Oplax.OplaxTrans.Modification.naturality._autoParam),
  sizeOf { app := app, naturality := naturality } = 1
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.EqResult.false.sizeOf_spec : ∀ (p : Lean.Expr), sizeOf (Nat.EqResult.false✝ p) = 1 + sizeOf p
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The affine span of a nonempty set is nonempty.  -/
instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P} [Nonempty ↑s], Nonempty ↥(affineSpan k s)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The affine span, converted to a set, is `spanPoints`.  -/
coe_affineSpan : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : Set P), ↑(affineSpan k s) = spanPoints k s
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.IsLocallyDirected.instIsOpenImmersionι : ∀ {J : Type w} [inst : CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme)
  [inst_1 : ∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)]
  [inst_2 : (F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] [inst_3 : Quiver.IsThin J]
  [inst_4 : Small.{u, w} J] (i : J), AlgebraicGeometry.IsOpenImmersion (CategoryTheory.Limits.colimit.ι F i)
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.of_mem_append : ∀ {α : Type u} {s₁ s₂ : Stream'.WSeq α} {a : α}, a ∈ s₁.append s₂ → a ∈ s₁ ∨ a ∈ s₂
-- Mathlib.Topology.Compactification.OnePoint.Basic
/-- A constructor for continuous maps out of a one point compactification of a discrete space, given a
map from the underlying space and a limit value at infinity.
 -/
OnePoint.continuousMapMkDiscrete : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {Y : Type u_3} →
      [inst_1 : TopologicalSpace Y] →
        [DiscreteTopology X] → (f : X → Y) → (y : Y) → Filter.Tendsto f Filter.cofinite (nhds y) → C(OnePoint X, Y)
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.instAddCommGroupWithOne : {Γ : Type u_1} →
  {R : Type u_3} →
    [Zero Γ] → [inst : PartialOrder Γ] → [inst_1 : AddCommGroupWithOne R] → AddCommGroupWithOne (HahnSeries Γ R)
-- Std.Http.Data.Body.Stream
/-- Builds a response with a streaming body generator.
 -/
Std.Http.Response.Builder.stream : Std.Http.Response.Builder →
  (Std.Http.Body.Stream → Std.Async.Async Unit) → Std.Async.Async (Std.Http.Response Std.Http.Body.Stream)
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesOnBall.unshift : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → E →L[𝕜] F}
  {pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)} {x : E} {r : ENNReal} {z : F},
  HasFPowerSeriesOnBall f pf x r → HasFPowerSeriesOnBall (fun y => z + (f y) (y - x)) (pf.unshift z) x r
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.hom_ext_iff : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₃ Y₃ : C₃}
  {f₃ : X₃ ⟶ Y₃} {sq : G.PullbackObjObj f₁ f₃} {X₂ : C₂} {f g : X₂ ⟶ sq.pt},
  f = g ↔
    CategoryTheory.CategoryStruct.comp f sq.fst = CategoryTheory.CategoryStruct.comp g sq.fst ∧
      CategoryTheory.CategoryStruct.comp f sq.snd = CategoryTheory.CategoryStruct.comp g sq.snd
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.discreteTopology : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [DiscreteTopology X]
  (h : X ≃ₜ Y), DiscreteTopology Y
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
/-- The recurrence relation for the `Γ` function.  -/
Complex.Gamma_add_one : ∀ (s : ℂ), s ≠ 0 → Complex.Gamma (s + 1) = s * Complex.Gamma s
-- Init.Data.String.Search
/-- Interprets a string as the decimal representation of a natural number, returning it. Returns
`none` if the slice does not contain a decimal natural number.

A slice can be interpreted as a decimal natural number if it is not empty and all the characters in
it are digits.

Use `isNat` to check whether `toNat?` would return `some`.
`toNat!` is an alternative that panics instead of
returning `none` when the slice is not a natural number.

Examples:

* `"".toNat? = none`

* `"0".toNat? = some 0`

* `"5".toNat? = some 5`

* `"587".toNat? = some 587`

* `"-587".toNat? = none`

* `" 5".toNat? = none`

* `"2+3".toNat? = none`

* `"0xff".toNat? = none`
 -/
String.toNat? : String → Option ℕ
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Bounded.State.mk : {α : Type} →
  Std.Queue (IO.Promise Bool) →
    Std.Queue (Std.Broadcast.Consumer✝ α) →
      (capacity : { x // 0 < x }) →
        ℕ →
          Vector (IO.Ref (Std.Slot✝ α)) ↑capacity →
            Fin ↑capacity → Fin ↑capacity → Std.TreeMap ℕ ℕ compare → ℕ → Bool → ℕ → Std.Bounded.State✝ α
-- Mathlib.Analysis.Asymptotics.Defs
/-- Similar to `IsBigOWith.sum_congr` except the index set can change in the sum. This requires the
constant in `hAB` to be independent of the index `i` and also the big-O relationship to "kick in"
at the same point along the running variable. Hence the `⊤` in `⊤ ×ˢ l`.  -/
Asymptotics.IsBigOWith.sum_congr' : ∀ {α : Type u_1} {E' : Type u_6} [inst : SeminormedAddCommGroup E'] {l : Filter α} {ι : Type u_18} {A : ι → α → E'}
  {B : ι → α → ℝ} {C : ℝ} {i : α → Finset ι},
  Asymptotics.IsBigOWith C (⊤ ×ˢ l) (Function.uncurry A) (Function.uncurry B) →
    Asymptotics.IsBigOWith C l (fun H => ∑ j ∈ i H, A j H) fun H => ∑ j ∈ i H, ‖B j H‖
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.pushforward_union : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X} (S R : CategoryTheory.Sieve Y),
  CategoryTheory.Sieve.pushforward f (S ⊔ R) =
    CategoryTheory.Sieve.pushforward f S ⊔ CategoryTheory.Sieve.pushforward f R
-- Std.Do.WP.Basic
/-- An unexpander for the `wp⟦...⟧` notation, causing it to be shown correctly in the pretty printer.
 -/
Std.Do.unexpandWP : Lean.PrettyPrinter.Unexpander
-- Lean.Parser.Extension
Lean.Parser.AliasValue.unary : {α : Type} → (α → α) → Lean.Parser.AliasValue α
-- Mathlib.Data.Num.ZNum
ZNum.bit0.eq_2 : ∀ (a : PosNum), (ZNum.pos a).bit0 = ZNum.pos a.bit0
-- Mathlib.Algebra.Order.Archimedean.IndicatorCard
Set.infinite_iff_tendsto_sum_indicator_atTop : ∀ {R : Type u_1} [inst : AddCommMonoid R] [inst_1 : PartialOrder R] [IsOrderedAddMonoid R] [AddLeftStrictMono R]
  [Archimedean R] {r : R},
  0 < r →
    ∀ {s : Set ℕ},
      s.Infinite ↔ Filter.Tendsto (fun n => ∑ k ∈ Finset.range n, s.indicator (fun x => r) k) Filter.atTop Filter.atTop
-- Mathlib.Algebra.Module.Congruence.Defs
SMulCon.instSMulQuotient.eq_1 : ∀ {S : Type u_2} (M : Type u_3) [inst : SMul S M] (c : SMulCon S M),
  SMulCon.instSMulQuotient M c = { smul := fun s => Quotient.map (fun x => s • x) ⋯ }
-- Mathlib.Analysis.Seminorm
Seminorm.bound_of_shell_sup : ∀ {𝕜 : Type u_3} {E : Type u_7} {ι : Type u_11} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p : ι → Seminorm 𝕜 E) (s : Finset ι) (q : Seminorm 𝕜 E) {ε : ℝ} {C : NNReal},
  0 < ε →
    ∀ {c : 𝕜},
      1 < ‖c‖ →
        (∀ (x : E), (∀ i ∈ s, (p i) x < ε) → ∀ j ∈ s, ε / ‖c‖ ≤ (p j) x → q x ≤ (C • p j) x) →
          ∀ {x : E}, (∃ j ∈ s, (p j) x ≠ 0) → q x ≤ (C • s.sup p) x
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.getD_inter_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k fallback : α}, k ∉ m₁ → (m₁ ∩ m₂).getD k fallback = fallback
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.mul_subset_iff_right : ∀ {α : Type u_2} [inst : Mul α] [inst_1 : DecidableEq α] {s t u : Finset α},
  s * t ⊆ u ↔ ∀ b ∈ t, MulOpposite.op b • s ⊆ u
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
Lean.Meta.Simp.Arith.Nat.instReprExprCnstr_lean : Repr Nat.Internal.Linear.ExprCnstr
-- Mathlib.Tactic.Translate.Core
Mathlib.Tactic.Translate.TranslationInfo.mk.inj : ∀ {translation : Lean.Name} {reorder : Mathlib.Tactic.Translate.Reorder}
  {relevantArg : Mathlib.Tactic.Translate.RelevantArg} {translation_1 : Lean.Name}
  {reorder_1 : Mathlib.Tactic.Translate.Reorder} {relevantArg_1 : Mathlib.Tactic.Translate.RelevantArg},
  { translation := translation, reorder := reorder, relevantArg := relevantArg } =
      { translation := translation_1, reorder := reorder_1, relevantArg := relevantArg_1 } →
    translation = translation_1 ∧ reorder = reorder_1 ∧ relevantArg = relevantArg_1
-- Init.Data.List.Basic
List.length_eq_lengthTR : @List.length = @List.lengthTR
-- Mathlib.RingTheory.TwoSidedIdeal.Lattice
TwoSidedIdeal.top_ringCon : ∀ (R : Type u_1) [inst : NonUnitalNonAssocRing R], ⊤.ringCon = ⊤
-- Init.Data.Nat.Bitwise.Lemmas
/-- An induction principle for the natural numbers with two cases:
* `n = 0`, and the motive is satisfied for `0`
* `n > 0`, and the motive should be satisfied for `n` on the assumption that it is satisfied for
  `n / 2`.
 -/
Nat.div2Induction : {motive : ℕ → Sort u} → (n : ℕ) → ((n : ℕ) → (n > 0 → motive (n / 2)) → motive n) → motive n
-- Lean.DocString.Parser
Lean.Doc.Parser.instReprOrderedListType : Repr Lean.Doc.Parser.OrderedListType
-- Init.Prelude
/-- Gets the substring representing the trailing whitespace of a `SourceInfo`, if available.
 -/
Lean.SourceInfo.getTrailing? : Lean.SourceInfo → Option Substring.Raw
-- Init.Control.Lawful.MonadLift.Lemmas
monadLift_seq : ∀ {m : Type u → Type v} {n : Type u → Type w} [inst : Monad m] [inst_1 : Monad n] [inst_2 : MonadLiftT m n]
  [LawfulMonadLiftT m n] {α β : Type u} [LawfulMonad m] [LawfulMonad n] (mf : m (α → β)) (ma : m α),
  monadLift (mf <*> ma) = monadLift mf <*> monadLift ma
-- Mathlib.Topology.MetricSpace.IsometricSMul
ediam_vadd : ∀ {M : Type u} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : VAdd M X] [IsIsometricVAdd M X] (c : M) (s : Set X),
  Metric.ediam (c +ᵥ s) = Metric.ediam s
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.center_toNonUnitalSubsemiring : ∀ (R : Type u) [inst : NonUnitalNonAssocRing R],
  (NonUnitalSubring.center R).toNonUnitalSubsemiring = NonUnitalSubsemiring.center R
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.rightUnitor_inv_toNatTrans : ∀ {B C : CategoryTheory.Cat} (F : B ⟶ C),
  (CategoryTheory.Bicategory.rightUnitor F).inv.toNatTrans = F.toFunctor.rightUnitor.inv
-- Mathlib.Topology.Constructions
Topology.IsEmbedding.restrict : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsEmbedding f →
    ∀ {s : Set X} {t : Set Y} (H : Set.MapsTo f s t), Topology.IsEmbedding (Set.MapsTo.restrict f s t H)
-- Mathlib.Order.Filter.Defs
/-- The forward map of a filter  -/
Filter.map : {α : Type u_1} → {β : Type u_2} → (α → β) → Filter α → Filter β
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.keys_map : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {γ : α → Type w}
  {f : (a : α) → β a → γ a}, m.WF → (Std.DHashMap.Raw.map f m).keys.Perm m.keys
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
/-- The equivalence between the noncomputable multiequalizer and
the concrete multiequalizer.  -/
CategoryTheory.Limits.Concrete.multiequalizerEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_1} →
      {CC : C → Type s} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory C FC] →
            {J : CategoryTheory.Limits.MulticospanShape} →
              (I : CategoryTheory.Limits.MulticospanIndex J C) →
                [inst_3 : CategoryTheory.Limits.HasMultiequalizer I] →
                  [CategoryTheory.Limits.PreservesLimit I.multicospan (CategoryTheory.forget C)] →
                    CategoryTheory.ToType (CategoryTheory.Limits.multiequalizer I) ≃
                      { x //
                        ∀ (i : J.R),
                          (CategoryTheory.ConcreteCategory.hom (I.fst i)) (x (J.fst i)) =
                            (CategoryTheory.ConcreteCategory.hom (I.snd i)) (x (J.snd i)) }
-- Mathlib.LinearAlgebra.TensorProduct.Tower
Submodule.coe_toBaseChange_tmul : ∀ {R : Type u_1} {M : Type u_2} (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (p : Submodule R M) (a : A) (x : ↥p),
  ↑((Submodule.toBaseChange A p) (a ⊗ₜ[R] x)) = a ⊗ₜ[R] ↑x
-- Mathlib.Algebra.Group.Units.Hom
Units.map.eq_1 : ∀ {M : Type u} {N : Type v} [inst : Monoid M] [inst_1 : Monoid N] (f : M →* N),
  Units.map f = MonoidHom.mk' (fun u => { val := f ↑u, inv := f u.inv, val_inv := ⋯, inv_val := ⋯ }) ⋯
-- Mathlib.Logic.Equiv.Defs
/-- The left summand of `α ⊕ β` is equivalent to `α`.  -/
Equiv.sumIsLeft : {α : Type u_1} → {β : Type u_2} → { x // x.isLeft = true } ≃ α
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
CategoryTheory.Functor.IsDense.leftKanExtensionUnit_leftKanExtensionIso_hom : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.IsDense],
  CategoryTheory.CategoryStruct.comp (F.leftKanExtensionUnit F)
      (F.whiskerLeft (CategoryTheory.Functor.IsDense.leftKanExtensionIso F).hom) =
    F.rightUnitor.inv
-- Mathlib.RingTheory.DedekindDomain.Basic
Ideal.IsPrime.isMaximal : ∀ {R : Type u_4} [inst : CommRing R] [Ring.DimensionLEOne R] {p : Ideal R}, p.IsPrime → p ≠ ⊥ → p.IsMaximal
-- Mathlib.Data.Fin.Tuple.Embedding
/-- Append a `Fin n ↪ α` at the end of a `Fin m ↪ α` if their ranges are disjoint.  -/
Fin.Embedding.append : {α : Type u_1} →
  {m n : ℕ} → {x : Fin m ↪ α} → {y : Fin n ↪ α} → Disjoint (Set.range ⇑x) (Set.range ⇑y) → Fin (m + n) ↪ α
-- Mathlib.CategoryTheory.Yoneda
/-- The obvious bijection `F.CorepresentableBy X ≃ (yoneda.obj Y ≅ F)`
when `F : C ⥤ Type v₁` and `[Category.{v₁} C]`.  -/
CategoryTheory.Functor.corepresentableByEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F : CategoryTheory.Functor C (Type v₁)} →
      {X : C} → F.CorepresentableBy X ≃ (CategoryTheory.coyoneda.obj (Opposite.op X) ≅ F)
-- Mathlib.Tactic.ClickSuggestions.GRewrite
/-- The key that is used for sorting and deduplicating `grw` lemmas.  -/
Mathlib.Tactic.ClickSuggestions.GrwKey : Type
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
/-- If `U, V` are disjoint, then `F(U ⊔ V) = F(U) × F(V)`.  -/
TopCat.Sheaf.isProductOfDisjoint : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : TopCat} →
      (F : TopCat.Sheaf C X) →
        (U V : TopologicalSpace.Opens ↑X) →
          U ⊓ V = ⊥ →
            CategoryTheory.Limits.IsLimit
              (CategoryTheory.Limits.BinaryFan.mk (F.obj.map (CategoryTheory.homOfLE ⋯).op)
                (F.obj.map (CategoryTheory.homOfLE ⋯).op))
-- Mathlib.Tactic.TacticAnalysis
/-- Constructor for a `Config` which breaks the pass up into multiple pieces.  -/
Mathlib.TacticAnalysis.Config.ofComplex : Mathlib.TacticAnalysis.ComplexConfig → Mathlib.TacticAnalysis.Config
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.uncurry_obj_injective : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  {D : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} D]
  {F₁ F₂ : CategoryTheory.Functor B (CategoryTheory.Functor C D)},
  CategoryTheory.Functor.uncurry.obj F₁ = CategoryTheory.Functor.uncurry.obj F₂ → F₁ = F₂
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
ProbabilityTheory.instIsProbabilityMeasureCondCDF : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α),
  MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.condCDF ρ a).measure
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
SSet.Subcomplex.Pairing.innerAnodyneExtensions : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [inst : P.IsRegular] [P.IsInner], SSet.innerAnodyneExtensions A.ι
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inl_mul_eq_smul : ∀ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : AddMonoid M] [inst_2 : DistribMulAction R M]
  [inst_3 : DistribMulAction Rᵐᵒᵖ M] (r : R) (x : TrivSqZeroExt R M), TrivSqZeroExt.inl r * x = r • x
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instInhabitedCode.default_1 : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Code pu
-- Mathlib.Data.Rat.Defs
Rat.semigroup : Semigroup ℚ
-- Mathlib.Order.Closure
LowerAdjoint.gc : ∀ {α : Type u_1} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {u : β → α} (l : LowerAdjoint u),
  GaloisConnection l.toFun u
-- Mathlib.Algebra.Lie.Matrix
/-- An invertible matrix induces a Lie algebra equivalence from the space of matrices to itself.  -/
Matrix.lieConj : {R : Type u} →
  [inst : CommRing R] →
    {n : Type w} →
      [inst_1 : DecidableEq n] →
        [inst_2 : Fintype n] → (P : Matrix n n R) → Invertible P → Matrix n n R ≃ₗ⁅R⁆ Matrix n n R
-- Init.Data.Array.Lemmas
/-- Variant of `all_map` with a side condition for the `stop` argument.  -/
Array.all_map' : ∀ {α : Type u_1} {β : Type u_2} {stop : ℕ} {f : α → β} {xs : Array α} {p : β → Bool},
  stop = xs.size → (Array.map f xs).all p 0 stop = xs.all (p ∘ f)