mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Dual.BaseChange
IsBaseChange.toDual_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {V : Type u_2} [inst_1 : AddCommMonoid V] [inst_2 : Module R V] {W : Type u_3}
  [inst_3 : AddCommMonoid W] [inst_4 : Module R W] {A : Type u_4} [inst_5 : CommSemiring A] [inst_6 : Algebra R A]
  [inst_7 : Module A W] [inst_8 : IsScalarTower R A W] {j : V →ₗ[R] W} (ibc : IsBaseChange A j) (f : Module.Dual R V),
  ibc.toDual f = (Module.Dual.congr ibc.equiv) ((Module.Dual.baseChange A) f)
-- Mathlib.Combinatorics.KatonaCircle
Fintype.card_numbering : ∀ {X : Type u_1} [inst : Fintype X] [inst_1 : DecidableEq X], Fintype.card (Numbering X) = (Fintype.card X).factorial
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updateFapImp : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.LetValue pu → Lean.Name → Array (Lean.Compiler.LCNF.Arg pu) → Lean.Compiler.LCNF.LetValue pu
-- Mathlib.Data.EReal.Inv
EReal.inv_zero : 0⁻¹ = 0
-- Mathlib.Topology.MetricSpace.HausdorffDimension
dimH_of_hausdorffMeasure_ne_zero_ne_top : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {d : NNReal} {s : Set X},
  (MeasureTheory.Measure.hausdorffMeasure ↑d) s ≠ 0 → (MeasureTheory.Measure.hausdorffMeasure ↑d) s ≠ ⊤ → dimH s = ↑d
-- Mathlib.Algebra.Group.Action.Pi
Pi.addAction : {ι : Type u_1} →
  {α : ι → Type u_4} → (M : Type u_7) → {m : AddMonoid M} → [(i : ι) → AddAction M (α i)] → AddAction M ((i : ι) → α i)
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
/-- The functorial factorization `ιObj I κ f ≫ πObj I κ f.hom = f`
with `ιObj I κ f` in `I.rlp.llp` and `πObj I κ f.hom` in `I.rlp`.  -/
CategoryTheory.SmallObject.functorialFactorizationData : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (I : CategoryTheory.MorphismProperty C) →
      (κ : Cardinal.{w}) →
        [inst_1 : Fact κ.IsRegular] →
          [inst_2 : OrderBot κ.ord.ToType] →
            [I.IsCardinalForSmallObjectArgument κ] → I.rlp.llp.FunctorialFactorizationData I.rlp
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.getD_insertMany_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {l : List α} {k fallback : α}, k ∉ m → l.contains k = false → (m.insertMany l).getD k fallback = fallback
-- Lean.Attributes
Lean.ParametricAttributeImpl.mk : {α : Type} →
  Lean.AttributeImplCore →
    (Lean.Name → Lean.Syntax → Lean.AttrM α) →
      (Lean.Name → α → Lean.AttrM Unit) →
        Bool → (Lean.Environment → Lean.Name → α → Bool) → Lean.ParametricAttributeImpl α
-- Mathlib.Analysis.Real.Cardinality
Cardinal.cantorFunction.eq_1 : ∀ (c : ℝ) (f : ℕ → Bool), Cardinal.cantorFunction c f = ∑' (n : ℕ), Cardinal.cantorFunctionAux c f n
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.ker_projectionOntoL : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} (h : Submodule.IsTopCompl p q), (↑(p.projectionOntoL q h)).ker = q
-- Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
/-- Any simplicial set satisfying `IsStrictSegal` is a `Quasicategory`.  -/
SSet.StrictSegal.quasicategory' : ∀ (X : SSet) [X.IsStrictSegal], X.Quasicategory
-- Lean.ReducibilityAttrs
/-- Set the given declaration as `[reducible]`  -/
Lean.setReducibleAttribute : {m : Type → Type} → [Lean.MonadEnv m] → Lean.Name → m Unit
-- Mathlib.CategoryTheory.Limits.Cones
/-- A map to the vertex of a cone induces a cone by composition.  -/
CategoryTheory.Limits.Cone.extend : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (c : CategoryTheory.Limits.Cone F) → {X : C} → (X ⟶ c.pt) → CategoryTheory.Limits.Cone F
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
/-- A family of `MvPowerSeries` is summable if their weighted order tends to infinity.  -/
MvPowerSeries.WithPiTopology.summable_of_tendsto_weightedOrder_atTop_nhds_top : ∀ {σ : Type u_1} {R : Type u_2} [inst : TopologicalSpace R] [inst_1 : Semiring R] {ι : Type u_3}
  {f : ι → MvPowerSeries σ R} [inst_2 : LinearOrder ι] [LocallyFiniteOrderBot ι] {w : σ → ℕ},
  Filter.Tendsto (fun i => MvPowerSeries.weightedOrder w (f i)) Filter.atTop (nhds ⊤) → Summable f
-- Init.Data.Nat.Bitwise.Lemmas
Nat.xor_self : ∀ (x : ℕ), x ^^^ x = 0
-- Init.Data.Float.Model.Unpacked.Operations.OfNat
/-- Converts an `Int32` to an `UnpackedFloat`, returning positive zero on zero.  -/
Float.Model.UnpackedFloat.ofInt32 : Float.Model.Format → Int32 → Float.Model.UnpackedFloat
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
_private.Mathlib.LinearAlgebra.CliffordAlgebra.Even.0.CliffordAlgebra.even.lift.snd_fFold_fFold : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {A : Type u_3} [inst_3 : Ring A] [inst_4 : Algebra R A] (f : CliffordAlgebra.EvenHom Q A)
  (m₁ m₂ m₃ : M) (x : A × ↥(CliffordAlgebra.even.lift.S✝ f)),
  ↑(((CliffordAlgebra.even.lift.fFold✝ f) m₁) (((CliffordAlgebra.even.lift.fFold✝ f) m₂) x)).2 m₃ =
    (f.bilin m₃) m₁ * ↑x.2 m₂
-- Mathlib.Topology.PartitionOfUnity
PartitionOfUnity.eventually_fintsupport_subset : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (ρ : PartitionOfUnity ι X s) (x₀ : X),
  ∀ᶠ (y : X) in nhds x₀, ρ.fintsupport y ⊆ ρ.fintsupport x₀
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.instOrderIsoClass : ∀ {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst_1 : Add α] [inst_2 : LE α] [inst_3 : Mul β] [inst_4 : Add β]
  [inst_5 : LE β], OrderIsoClass (α ≃+*o β) α β
-- Mathlib.Data.TwoPointing
/-- `fst` and `snd` are distinct terms  -/
TwoPointing.fst_ne_snd : ∀ {α : Type u_3} (self : TwoPointing α), self.toProd.1 ≠ self.toProd.2
-- Mathlib.Order.Disjoint
Disjoint.left_le_of_le_sup_left : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : OrderBot α] {a b c : α}, a ≤ c ⊔ b → Disjoint a c → a ≤ b
-- Mathlib.RingTheory.Valuation.Basic
Valuation.embedding_restrict : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
  (x : R), MonoidWithZeroHom.ValueGroup₀.embedding (v.restrict x) = v x
-- Mathlib.RingTheory.Unramified.LocalRing
Localization.finite_of_primesOver_eq_singleton : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R}
  [inst_3 : p.IsPrime] {q : Ideal S} [inst_4 : q.IsPrime],
  p.primesOver S = {q} →
    ∀ [Module.Finite R S] [inst_6 : q.LiesOver p] [inst_7 : Algebra (Localization.AtPrime p) (Localization.AtPrime q)]
      [Localization.AtPrime.IsLiesOverAlgebra p q], Module.Finite (Localization.AtPrime p) (Localization.AtPrime q)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instInv.eq_1 : ∀ {α : Type u_1} {l : Filter α} {G : Type u_6} [inst : Inv G], Filter.Germ.instInv = { inv := Filter.Germ.map Inv.inv }
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k a : α},
  (t.erase k).getKey? a = if cmp k a = Ordering.eq then none else t.getKey? a
-- Mathlib.Logic.Equiv.Defs
/-- If `α ≃ β` and `β` is inhabited, then so is `α`.  -/
Equiv.inhabited : {α : Sort u} → {β : Sort v} → [Inhabited β] → α ≃ β → Inhabited α
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.ofHom_add : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ₁ φ₂ : F ⟶ G),
  CochainComplex.HomComplex.Cochain.ofHom (φ₁ + φ₂) =
    CochainComplex.HomComplex.Cochain.ofHom φ₁ + CochainComplex.HomComplex.Cochain.ofHom φ₂
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
/-- The natural isomorphism `L ⟶ HoCat.resolution ⋙ HoCat.toLocalization L` when
`L : C ⥤ D` is a localization functor.  -/
HomotopicalAlgebra.FibrantObject.HoCat.resolutionCompToLocalizationNatTrans : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          (L : CategoryTheory.Functor C D) →
            [inst_3 : L.IsLocalization (HomotopicalAlgebra.weakEquivalences C)] →
              L ⟶
                HomotopicalAlgebra.FibrantObject.HoCat.resolution.comp
                  (HomotopicalAlgebra.FibrantObject.HoCat.toLocalization L)
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.XIsoOfEq_inv_comp_XIsoOfEq_inv_assoc : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι}
  (h₂₁ : p₂ = p₁) (h₃₂ : p₃ = p₂) {Z : V} (h : K.X p₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₂₁).inv (CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₃₂).inv h) =
    CategoryTheory.CategoryStruct.comp (K.XIsoOfEq ⋯).hom h
-- Lean.Elab.Tactic.Simp
/-- Extract the arguments from a `dsimpArgs` syntax as an array of syntaxes  -/
Lean.Parser.Tactic.getDSimpArgs? : Lean.Syntax → Option (Array Lean.Syntax)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂.isoInv.sizeOf_spec : ∀ (e : Lean.Expr) (isoLift : Mathlib.Tactic.BicategoryLike.IsoLift) (iso : Mathlib.Tactic.BicategoryLike.Mor₂Iso),
  sizeOf (Mathlib.Tactic.BicategoryLike.Mor₂.isoInv e isoLift iso) = 1 + sizeOf e + sizeOf isoLift + sizeOf iso
-- Mathlib.Order.Filter.AtTopBot.Defs
Filter.eventually_lt_atBot : ∀ {α : Type u_3} [inst : Preorder α] [NoBotOrder α] (a : α), ∀ᶠ (x : α) in Filter.atBot, x < a
-- Lean.Expr
_private.Lean.Expr.0.Lean.intPowNatFn : Lean.Expr
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Complete
CategoryTheory.Functor.instReflectsIsomorphismsDiscreteObjWhiskeringLeftIncl : ∀ (I : Type u₂) [inst : CategoryTheory.Category.{v₂, u₂} I] (C : Type u₁) [inst_1 : CategoryTheory.Category.{v₁, u₁} C],
  ((CategoryTheory.Functor.whiskeringLeft (CategoryTheory.Discrete I) I C).obj
      (CategoryTheory.Functor.incl✝ I)).ReflectsIsomorphisms
-- Mathlib.Topology.Algebra.OpenSubgroup
IsTopologicalGroup.exist_openSubgroup_sub_clopen_nhds_of_one : ∀ {G : Type u_2} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {W : Set G},
  IsClopen W → 1 ∈ W → ∃ H, ↑H ⊆ W
-- Mathlib.CategoryTheory.Pi.Basic
/-- Similar to `pi`, but all functors come from the same category `A`
 -/
CategoryTheory.Functor.pi' : {I : Type w₀} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {A : Type u₃} →
        [inst_1 : CategoryTheory.Category.{v₃, u₃} A] →
          ((i : I) → CategoryTheory.Functor A (C i)) → CategoryTheory.Functor A ((i : I) → C i)
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
SSet.horn.IsCompatible.δ_liftOfKanComplex_assoc : ∀ {X : SSet} {n : ℕ} {i : Fin (n + 2)} {f : (j : Fin (n + 2)) → j ≠ i → (SSet.stdSimplex.obj { len := n } ⟶ X)}
  [inst : X.KanComplex] (hf : SSet.horn.IsCompatible f) (j : Fin (n + 2))
  (hj : autoParam (j ≠ i) SSet.horn.IsCompatible.δ_liftOfKanComplex._auto_1) {Z : SSet} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) (CategoryTheory.CategoryStruct.comp hf.liftOfKanComplex h) =
    CategoryTheory.CategoryStruct.comp (f j hj) h
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_inter_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ ∩ m₂).getKey? k = none
-- Lean.Server.FileWorker.ExampleHover
_private.Lean.Server.FileWorker.ExampleHover.0.Lean.Server.FileWorker.Hover.RWState.nonOutput.inj : ∀ {ticks ticks_1 : ℕ},
  Lean.Server.FileWorker.Hover.RWState.nonOutput✝ ticks = Lean.Server.FileWorker.Hover.RWState.nonOutput✝ ticks_1 →
    ticks = ticks_1
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.Iso.map_hom_inv_id_eval : ∀ {C : Type u_1} {D : Type u_2} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {X Y : CategoryTheory.GradedObject J C} (e : X ≅ Y)
  (F : CategoryTheory.Functor C D) (j : J),
  CategoryTheory.CategoryStruct.comp (F.map (e.hom j)) (F.map (e.inv j)) =
    CategoryTheory.CategoryStruct.id (F.obj (X j))
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.centralizer_toNonUnitalSubring : ∀ {R : Type u_1} [inst : Ring R] (s : Set R),
  (Subring.centralizer s).toNonUnitalSubring = NonUnitalSubring.centralizer s
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.mulCayley_union : ∀ {M : Type u_1} [inst : Mul M] (s₁ s₂ : Set M),
  SimpleGraph.mulCayley (s₁ ∪ s₂) = SimpleGraph.mulCayley s₁ ⊔ SimpleGraph.mulCayley s₂
-- Mathlib.Order.Category.BoolAlg
BoolAlg.of.inj : ∀ {carrier : Type u_1} {str : BooleanAlgebra carrier} {carrier_1 : Type u_1} {str_1 : BooleanAlgebra carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1
-- Mathlib.MeasureTheory.Measure.AddContent
/-- A function which is additive on disjoint elements in a ring of sets `C` defines an
additive content on `C`.  -/
MeasureTheory.IsSetRing.addContent_of_union : {α : Type u_1} →
  {C : Set (Set α)} →
    {G : Type u_2} →
      [inst : AddCommMonoid G] →
        (m : Set α → G) →
          MeasureTheory.IsSetRing C →
            m ∅ = 0 →
              (∀ {s t : Set α}, s ∈ C → t ∈ C → Disjoint s t → m (s ∪ t) = m s + m t) → MeasureTheory.AddContent G C
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.scalar_eq_self_of_mem_center : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R]
  {A : Matrix.SpecialLinearGroup n R},
  A ∈ Subgroup.center (Matrix.SpecialLinearGroup n R) → ∀ (i : n), (Matrix.scalar n) (↑A i i) = ↑A
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- Two cyclic additive groups of the same cardinality are isomorphic.  -/
addEquivOfAddCyclicCardEq : {G : Type u_2} →
  {G' : Type u_3} →
    [inst : AddGroup G] →
      [inst_1 : AddGroup G'] → [hG : IsAddCyclic G] → [hH : IsAddCyclic G'] → Nat.card G = Nat.card G' → G ≃+ G'
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsPrenex.below.ex : ∀ {L : FirstOrder.Language} {α : Type u'} {motive : {n : ℕ} → (a : L.BoundedFormula α n) → a.IsPrenex → Prop} {n : ℕ}
  {φ : L.BoundedFormula α (n + 1)} (h : φ.IsPrenex),
  FirstOrder.Language.BoundedFormula.IsPrenex.below h → motive φ h → FirstOrder.Language.BoundedFormula.IsPrenex.below ⋯
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the forward direction of `lowerHemicontinuous_iff_frequently`. -/
LowerHemicontinuous.frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β},
  LowerHemicontinuous f → ∀ (x : α) (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhds x, f x' ⊆ t) → f x ⊆ t
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey?_le_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k km : α} (hc : k ∈ t), t.minKey?.get ⋯ = km → (cmp km k).isLE = true
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.coe_pow : ∀ {α : Type u} {R : Type u_2} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] [inst_2 : Monoid R]
  [inst_3 : BoundedMul R] [inst_4 : ContinuousMul R] (n : ℕ) (f : BoundedContinuousFunction α R), ⇑(f ^ n) = ⇑f ^ n
-- Mathlib.Data.UInt
UInt32.toBitVec_nsmul : ∀ (n : ℕ) (a : UInt32), (n • a).toBitVec = n • a.toBitVec
-- Mathlib.Analysis.Calculus.Deriv.Add
HasDerivAt.add : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f g : 𝕜 → F} {f' g' : F} {x : 𝕜},
  HasDerivAt f f' x → HasDerivAt g g' x → HasDerivAt (f + g) (f' + g') x
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- The spectral norm is compatible with the action of `K`.  -/
spectralNorm_smul : ∀ {K : Type u_2} [inst : NormedField K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L] [IsUltrametricDist K]
  (k : K) {y : L}, IsAlgebraic K y → spectralNorm K L (k • y) = ↑‖k‖₊ * spectralNorm K L y
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.isEmbedding_coe_of_principal : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [inst : (i : ι) → TopologicalSpace (R i)] {S : Set ι},
  Topology.IsEmbedding DFunLike.coe
-- Mathlib.Data.Prod.Lex
Prod.Lex.monotone_fst_ofLex : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β], Monotone fun x => (ofLex x).1
-- Std.Data.DTreeMap.Internal.Operations
/-- Slower version of `containsThenInsert` which can be used in the absence of balance
information but still assumes the preconditions of `containsThenInsert`, otherwise might panic.
 -/
Std.DTreeMap.Internal.Impl.containsThenInsert! : {α : Type u} →
  {β : α → Type v} → [Ord α] → (k : α) → β k → Std.DTreeMap.Internal.Impl α β → Bool × Std.DTreeMap.Internal.Impl α β
-- Mathlib.Algebra.Group.End
Equiv.Perm.coe_one : ∀ {α : Type u_4}, ⇑1 = id
-- Mathlib.NumberTheory.NumberField.Norm
RingOfIntegers.norm_algebraMap : ∀ {L : Type u_1} (K : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (x : NumberField.RingOfIntegers K),
  (RingOfIntegers.norm K) ((algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) x) =
    x ^ Module.finrank K L
-- Mathlib.Order.Category.PartOrd
PartOrd.comp_apply : ∀ {X Y Z : PartOrd} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonColorInformation : Lean.ToJson Lean.Lsp.ColorInformation
-- Mathlib.Data.W.Constructions
WType.instInhabitedNatα : Inhabited WType.Natα
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup'_induction : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : β → α) {p : α → Prop},
  (∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)) → (∀ b ∈ s, p (f b)) → p (s.sup' H f)
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.Recv.bytes.sizeOf_spec : ∀ {β : Type} [inst : SizeOf β] (x : Option ByteArray), sizeOf (Std.Http.Server.Connection.Recv.bytes✝ x) = 1 + sizeOf x
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- Constructor for morphisms in the category `LaxBraidedFunctor C D`.  -/
CategoryTheory.LaxBraidedFunctor.homMk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.MonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                {F G : CategoryTheory.LaxBraidedFunctor C D} →
                  (f : F.toFunctor ⟶ G.toFunctor) → [CategoryTheory.NatTrans.IsMonoidal f] → F ⟶ G
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.performRatCheck.match_1.eq_2 : ∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → Sort u_1)
  (h_1 : (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → motive (some c)) (h_2 : Unit → motive none),
  (match none with
    | some c => h_1 c
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
rankCondition_iff_matrix : ∀ {R : Type u_1} [inst : Semiring R],
  RankCondition R ↔ ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), g * f = 1 → m ≤ n
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
Filter.Tendsto.nndist : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] {f g : β → α} {x : Filter β} {a b : α},
  Filter.Tendsto f x (nhds a) →
    Filter.Tendsto g x (nhds b) → Filter.Tendsto (fun x => nndist (f x) (g x)) x (nhds (nndist a b))
-- Lean.PrettyPrinter.Delaborator.Metavariable
_private.Lean.PrettyPrinter.Delaborator.Metavariable.0.Lean.PrettyPrinter.Delaborator.describeMVar.absentLCtxVars : ℕ → Lean.MetavarDecl → Lean.MetaM String
-- Mathlib.Analysis.Convex.GaugeRescale
/-- `gaugeRescale` bundled as an `Equiv`.  -/
gaugeRescaleEquiv : {E : Type u_1} →
  [inst : AddCommGroup E] →
    [inst_1 : Module ℝ E] →
      [inst_2 : TopologicalSpace E] →
        [T1Space E] →
          (s t : Set E) →
            Absorbent ℝ s → Bornology.IsVonNBounded ℝ s → Absorbent ℝ t → Bornology.IsVonNBounded ℝ t → E ≃ E
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.nnrpow_eq_pow : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A] {a : A}
  {y : NNReal}, CFC.nnrpow a y = a ^ y
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.module : {R : Type u} → [inst : Semiring R] → {S : Type u_1} → [inst_1 : Semiring S] → [Module S R] → Module S (Polynomial R)
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.ofCoeff_add : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (x y : ℕ →₀ M),
  { coeff := x + y } = { coeff := x } + { coeff := y }
-- Mathlib.CategoryTheory.Limits.Types.Yoneda
CategoryTheory.Limits.compYonedaSectionsEquiv_apply_app : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] (F : CategoryTheory.Functor J Cᵒᵖ) (X : C)
  (s : ↑(F.comp (CategoryTheory.yoneda.obj X)).sections) (j : J),
  ((CategoryTheory.Limits.compYonedaSectionsEquiv F X) s).app j = Quiver.Hom.op (↑s j)
-- Mathlib.Data.Finsupp.Basic
Finsupp.sum_filter_add_sum_filter_not : ∀ {α : Type u_1} {M : Type u_5} {N : Type u_6} [inst : Zero M] (p : α → Prop) [inst_1 : DecidablePred p] (f : α →₀ M)
  [inst_2 : AddCommMonoid N] (g : α → M → N),
  (Finsupp.filter p f).sum g + (Finsupp.filter (fun a => ¬p a) f).sum g = f.sum g
-- Std.Http.Data.URI.Parser
_private.Std.Http.Data.URI.Parser.0.Std.Http.URI.Parser.parseSegment : Std.Http.URI.Config → Std.Internal.Parsec.ByteArray.Parser ByteSlice
-- Mathlib.Data.Finsupp.WellFounded
Finsupp.Lex.wellFounded' : ∀ {α : Type u_1} {N : Type u_2} [inst : Zero N] {r : α → α → Prop} {s : N → N → Prop},
  (∀ ⦃n : N⦄, ¬s n 0) →
    WellFounded s → ∀ [Std.Trichotomous r], WellFounded (Function.swap r) → WellFounded (Finsupp.Lex r s)
-- Mathlib.Tactic.Positivity.Basic
Mathlib.Meta.Positivity.le_min_of_lt_of_le : ∀ {R : Type u_2} [inst : LinearOrder R] {a b c : R}, a < b → a ≤ c → a ≤ min b c
-- Init.System.IOError
IO.Error.mkInappropriateTypeFile : String → UInt32 → String → IO.Error
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.encodeFun.match_1.eq_2 : ∀ {n : ℕ} (motive : (x : ℕ) → (Fin x → Fin n) → Sort u_1) (m : ℕ) (f : Fin (m + 1) → Fin n)
  (h_1 : (x : Fin 0 → Fin n) → motive 0 x) (h_2 : (m : ℕ) → (f : Fin (m + 1) → Fin n) → motive m.succ f),
  (match m.succ, f with
    | 0, x => h_1 x
    | m.succ, f => h_2 m f) =
    h_2 m f
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
SimpleGraph.IsFiveWheelLike.snd_notMem_left : ∀ {α : Type u_1} {s : Finset α} {G : SimpleGraph α} {r k : ℕ} [inst : DecidableEq α] {v w₁ w₂ : α} {t : Finset α},
  G.IsFiveWheelLike r k v w₁ w₂ s t → w₂ ∉ s
-- Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
AlgebraicGeometry.surjectiveOnStalks_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.SurjectiveOnStalks f ↔
    ∀ (x : ↥X), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x))