mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicoequalizer.desc.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) [inst_1 : CategoryTheory.Limits.HasMulticoequalizer I] (W : C)
  (k k_1 : (b : J.R) → I.right b ⟶ W) (e_k : k = k_1)
  (h :
    ∀ (a : J.L),
      CategoryTheory.CategoryStruct.comp (I.fst a) (k (J.fst a)) =
        CategoryTheory.CategoryStruct.comp (I.snd a) (k (J.snd a))),
  CategoryTheory.Limits.Multicoequalizer.desc I W k h = CategoryTheory.Limits.Multicoequalizer.desc I W k_1 ⋯
-- Mathlib.Computability.Primrec.List
/-- `List.set` is primitive recursive.  -/
Primrec.list_set : ∀ {α : Type u_1} [inst : Primcodable α], Primrec₂ fun l p => l.set p.1 p.2
-- Mathlib.CategoryTheory.Sites.Coherent.Basic
/-- The condition `Precoherent C` is essentially the minimal condition required to define the
coherent coverage on `C`.
 -/
CategoryTheory.Precoherent : (C : Type u_1) → [CategoryTheory.Category.{v_1, u_1} C] → Prop
-- Mathlib.Order.UpperLower.CompleteLattice
/-- See Note [custom simps projection].  -/
LowerSet.Simps.coe : {α : Type u_1} → [inst : LE α] → LowerSet α → Set α
-- Aesop.Tree.ExtractProof
_private.Aesop.Tree.ExtractProof.0.Aesop.extractProofMVarCluster : Lean.Environment → Aesop.MVarCluster → Lean.MetaM Unit
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toArray_rco : ∀ {m n : ℤ} {i : ℕ}, (m...n).toArray[i]! = if i < (n - m).toNat then m + ↑i else 0
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.comp_f : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  {L L' L'' : Φ.LeftResolution X₂} (φ : L ⟶ L') (ψ : L' ⟶ L''),
  (CategoryTheory.CategoryStruct.comp φ ψ).f = CategoryTheory.CategoryStruct.comp φ.f ψ.f
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.rightAngleRotation_map' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace ℝ F]
  [inst_5 : Fact (Module.finrank ℝ F = 2)] (φ : E ≃ₗᵢ[ℝ] F),
  ((Orientation.map (Fin 2) φ.toLinearEquiv) o).rightAngleRotation = (φ.symm.trans o.rightAngleRotation).trans φ
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement'.isCompl : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H.IsComplement' K → IsCompl H K
-- Init.Control.Id
Id.instLawfulMonadAttach : LawfulMonadAttach Id
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.bdd_below_bdd_above_iff_subset_uIcc : ∀ {α : Type u_1} [inst : Lattice α] (s : Set α), BddBelow s ∧ BddAbove s ↔ ∃ a b, s ⊆ Set.uIcc a b
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.iSup_coe_eapprox : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ENNReal},
  Measurable f → ⨆ n, ⇑(MeasureTheory.SimpleFunc.eapprox f n) = f
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.instIsAddLeftInvariantForallVolumeOfMeasurableAddOfSigmaFinite : ∀ {ι : Type u_1} [inst : Fintype ι] {G : ι → Type u_4} [inst_1 : (i : ι) → AddGroup (G i)]
  [inst_2 : (i : ι) → MeasureTheory.MeasureSpace (G i)] [∀ (i : ι), MeasurableAdd (G i)]
  [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume] [∀ (i : ι), MeasureTheory.volume.IsAddLeftInvariant],
  MeasureTheory.volume.IsAddLeftInvariant
-- Mathlib.Condensed.Discrete.Basic
/-- Discreteness is left adjoint to the forgetful functor. When `C` is `Type*`, this is analogous to
`TopCat.adj₁ : TopCat.discrete ⊣ forget TopCat`.
 -/
LightCondensed.discreteUnderlyingAdj : (C : Type w) →
  [inst : CategoryTheory.Category.{u, w} C] →
    [inst_1 : CategoryTheory.HasSheafify (CategoryTheory.coherentTopology LightProfinite) C] →
      LightCondensed.discrete C ⊣ LightCondensed.underlying C
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.ne_zero_of_mem_of_unit : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {a : Aˣ} {r : R},
  r ∈ spectrum R ↑a → r ≠ 0
-- Mathlib.Data.EReal.Basic
instIsOrderedAddMonoidEReal : IsOrderedAddMonoid EReal
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.isColimitCoconeLeftOpOfCone_desc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c)
  (s : CategoryTheory.Limits.Cocone F.leftOp),
  (CategoryTheory.Limits.isColimitCoconeLeftOpOfCone F hc).desc s =
    (hc.lift (CategoryTheory.Limits.coneOfCoconeLeftOp s)).unop
-- Mathlib.LinearAlgebra.TensorProduct.Basis
Module.Basis.tensorProduct.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [inst : CommSemiring R]
  [inst_1 : Semiring S] [inst_2 : Algebra R S] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M]
  [inst_6 : IsScalarTower R S M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] (b : Module.Basis ι S M)
  (c : Module.Basis κ R N),
  b.tensorProduct c =
    Finsupp.basisSingleOne.map
      (TensorProduct.AlgebraTensorModule.congr b.repr c.repr ≪≫ₗ
          (finsuppTensorFinsupp R S S R ι κ ≪≫ₗ
            Finsupp.lcongr (Equiv.refl (ι × κ)) (TensorProduct.AlgebraTensorModule.rid R S S))).symm
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.ker_traceForm_eq_bot_of_isCartanSubalgebra : ∀ (R : Type u_1) (L : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [LieAlgebra.IsKilling R L] [IsNoetherian R L] [IsArtinian R L] (H : LieSubalgebra R L) [H.IsCartanSubalgebra],
  LinearMap.ker (LieModule.traceForm R (↥H) L) = ⊥
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
integral_Ioi_cpow_of_lt : ∀ {a : ℂ}, a.re < -1 → ∀ {c : ℝ}, 0 < c → ∫ (t : ℝ) in Set.Ioi c, ↑t ^ a = -↑c ^ (a + 1) / (a + 1)
-- Mathlib.Algebra.Order.Module.HahnEmbedding
LinearPMap.sSup.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] (c c_1 : Set (E →ₛₗ.[σ] F))
  (e_c : c = c_1) (hc : DirectedOn (fun x1 x2 => x1 ≤ x2) c), LinearPMap.sSup c hc = LinearPMap.sSup c_1 ⋯
-- Mathlib.Algebra.GradedMonoid
/-- Multiplication is associative  -/
GradedMonoid.GMonoid.mul_assoc : ∀ {ι : Type u_1} {A : ι → Type u_2} {inst : AddMonoid ι} [self : GradedMonoid.GMonoid A] (a b c : GradedMonoid A),
  a * b * c = a * (b * c)
-- Mathlib.Topology.Separation.Basic
instR0SpaceProd : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [R0Space X] [inst_2 : TopologicalSpace Y] [R0Space Y],
  R0Space (X × Y)
-- Std.Data.ByteSlice
_private.Std.Data.ByteSlice.0.Std.Slice.Internal.ByteSliceData.mk : (byteArray : ByteArray) → (start stop : ℕ) → start ≤ stop → stop ≤ byteArray.size → Std.Slice.Internal.ByteSliceData
-- Init.Data.Option.Attach
Option.any_attachWith : ∀ {α : Type u_1} {p : α → Bool} {o : Option α} {r : α → Prop} (hr : ∀ (x : α), o = some x → r x)
  {q : { x // r x } → Bool}, (∀ (x : α) (h : r x), q ⟨x, h⟩ = p x) → Option.any q (o.attachWith r hr) = Option.any p o
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.aeval_val_surjective : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Generators R S ι), Function.Surjective ⇑(MvPolynomial.aeval P.val)
-- Mathlib.RingTheory.Polynomial.HilbertPoly
/-- The key property of Hilbert polynomials. If `F` is a field with characteristic `0`, `p : F[X]` and
`d : ℕ`, then for any large enough `n : ℕ`, `(Polynomial.hilbertPoly p d).eval (n : F)` equals the
coefficient of `Xⁿ` in the power series expansion of `p/(1 - X)ᵈ`.
 -/
Polynomial.coeff_mul_invOneSubPow_eq_hilbertPoly_eval : ∀ {F : Type u_1} [inst : Field F] [CharZero F] {p : Polynomial F} (d : ℕ) {n : ℕ},
  p.natDegree < n →
    (PowerSeries.coeff n) (↑p * ↑(PowerSeries.invOneSubPow F d)) = Polynomial.eval (↑n) (p.hilbertPoly d)
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
/-- Transports an edge between `x₀` and `x₁` to an edge between `y₀` and `y₁`, given `x₀ = y₀`
and `x₁ = y₁`.  -/
SSet.Edge.ofEq : {X : SSet} → {x₀ x₁ y₀ y₁ : X.obj (Opposite.op { len := 0 })} → SSet.Edge x₀ x₁ → x₀ = y₀ → x₁ = y₁ → SSet.Edge y₀ y₁
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_rel_mulIndicator : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] {s : Set α} {f g : α → M} {a : α} {r : M → M → Prop},
  r 1 1 → (a ∈ s → r (f a) (g a)) → r (s.mulIndicator f a) (s.mulIndicator g a)
-- Mathlib.Data.Nat.Totient
Nat.neZero_totient : ∀ {n : ℕ} [NeZero n], NeZero n.totient
-- Mathlib.Order.Cover
WCovBy.refl : ∀ {α : Type u_1} [inst : Preorder α] (a : α), a ⩿ a
-- Lean.Meta.Tactic.SolveByElim
/-- Returns the list of tactics corresponding to applying the available lemmas to the goal.  -/
Lean.Meta.SolveByElim.applyLemmas : Lean.Meta.SolveByElim.SolveByElimConfig →
  List (Lean.Elab.TermElabM Lean.Expr) →
    (Lean.Meta.SolveByElim.SolveByElimConfig → Lean.Elab.TermElabM (List Lean.Expr)) →
      Lean.MVarId → Lean.MetaM (Lean.Meta.Iterator (List Lean.MVarId))
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctorCore.map₂_comp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.StrictlyUnitaryPseudofunctorCore B C) {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
  self.map₂ (CategoryTheory.CategoryStruct.comp η θ) = CategoryTheory.CategoryStruct.comp (self.map₂ η) (self.map₂ θ)
-- Mathlib.NumberTheory.ModularForms.SlashActions
ModularForm.«term_∣[_]_» : Lean.TrailingParserDescr
-- Lean.Meta.CongrTheorems
Lean.Meta.CongrArgKind.fixed.sizeOf_spec : sizeOf Lean.Meta.CongrArgKind.fixed = 1
-- Mathlib.Order.Lattice
Subtype.coe_sup : ∀ {α : Type u} [inst : SemilatticeSup α] {P : α → Prop} (Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)) (x y : Subtype P),
  ↑(x ⊔ y) = ↑x ⊔ ↑y
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
IsStrictlyPositive.nnrpow : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] (a : A) (y : NNReal),
  y ≠ 0 → autoParam (IsStrictlyPositive a) IsStrictlyPositive.nnrpow._auto_1 → IsStrictlyPositive (a ^ y)
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sum_add_index : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddCommMonoid (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : AddCommMonoid γ] {f g : Π₀ (i : ι), β i}
  {h : (i : ι) → β i → γ},
  (∀ (i : ι), h i 0 = 0) →
    (∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ + h i b₂) → (f + g).sum h = f.sum h + g.sum h
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_eq_some_iff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {v : β}, m[k]? = some v ↔ ∃ (h : k ∈ m), m[k] = v
-- Mathlib.Algebra.Homology.ExactSequenceFour
CategoryTheory.ComposableArrows.IsComplex.cokerToKer'.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.IsComplex) (k : ℕ) (hk : k ≤ n)
  (cc : CategoryTheory.Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯))
  (kf : CategoryTheory.Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)) (hcc hcc_1 : CategoryTheory.Limits.IsColimit cc),
  hcc = hcc_1 →
    ∀ (hkf hkf_1 : CategoryTheory.Limits.IsLimit kf),
      hkf = hkf_1 → hS.cokerToKer' k hk cc kf hcc hkf = hS.cokerToKer' k hk cc kf hcc_1 hkf_1
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey?_modify_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : β → β},
  (Std.ExtDHashMap.Const.modify m k f).getKey? k = if k ∈ m then some k else none
-- Init.Data.BitVec.Basic
/-- Auxiliary function for `rotateLeft`, which does not take into account the case where
the rotation amount is greater than the bitvector width.  -/
BitVec.rotateLeftAux : {w : ℕ} → BitVec w → ℕ → BitVec w
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_get_MonadStateOf_lift_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m n : Type u → Type v} [inst : MonadLift m n]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : (α : Type u) → Std.Internal.Do.WP (n α) α Pred EPred] {σ : Type u} {post : σ → Pred} {epost : EPred}
  [inst_4 : MonadStateOf σ m],
  Std.Internal.Do.wp MonadStateOf.get post epost = Std.Internal.Do.wp (MonadLift.monadLift MonadStateOf.get) post epost
-- Mathlib.RingTheory.Localization.Away.Lemmas
IsLocalization.Away.mulNumerator.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] (s : Set R) {Rₜ : ↑s → Type u_2} [inst_1 : (t : ↑s) → CommRing (Rₜ t)]
  [inst_2 : (t : ↑s) → Algebra R (Rₜ t)] [inst_3 : ∀ (t : ↑s), IsLocalization.Away (↑t) (Rₜ t)]
  (p : (t : ↑s) → Set (Rₜ t)) (x x_1 : (t : ↑s) × ↑(p t)),
  x = x_1 → IsLocalization.Away.mulNumerator s p x = IsLocalization.Away.mulNumerator s p x_1
-- Mathlib.Order.Basic
Decidable.le_iff_eq_or_lt' : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α} [DecidableLE α], b ≤ a ↔ a = b ∨ b < a
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.leftShift_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L M : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a n' : ℤ) (hn' : n + a = n')
  {m t t' : ℤ} (γ' : CochainComplex.HomComplex.Cochain L M m) (h : n + m = t) (ht' : t + a = t'),
  (γ.comp γ' h).leftShift a t' ht' = (a * m).negOnePow • (γ.leftShift a n' hn').comp γ' ⋯
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciInf_and : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {p q : Prop} {f : p ∧ q → α},
  ⨅ (ih : p ∧ q), f ih = ⨅ (h₁ : p), ⨅ (h₂ : q), f ⋯
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.truncatedSup_union_of_notMem : ∀ {α : Type u_1} [inst : SemilatticeSup α] {s t : Finset α} {a : α} [inst_1 : DecidableLE α] [inst_2 : OrderTop α]
  [inst_3 : DecidableEq α], a ∉ lowerClosure ↑s → a ∉ lowerClosure ↑t → (s ∪ t).truncatedSup a = ⊤
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.le : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [P.IsProper] (x : ↑P.II), ↑x ≤ ↑(P.p x)
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.mk_eq_zero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] (f : Γ → R) (h : (Function.support f).IsPWO),
  { coeff := f, isPWO_support' := h } = 0 ↔ f = 0
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.toCLM_zero : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [inst_8 : IsTopologicalAddGroup F],
  ContinuousLinearMapWOT.toCLM 0 = 0
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.modify_eq_empty_iff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : β → β}, m.modify k f = ∅ ↔ m = ∅
-- Mathlib.Computability.RegularExpressions
RegularExpression.mul_rmatch_iff : ∀ {α : Type u_1} [inst : DecidableEq α] (P Q : RegularExpression α) (x : List α),
  (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
-- Mathlib.Algebra.Homology.CochainComplexOpposite
/-- The embedding of the complex shape `up ℤ` in `down ℤ` given by `n ↦ -n`.  -/
ComplexShape.embeddingUpIntDownInt : (ComplexShape.up ℤ).Embedding (ComplexShape.down ℤ)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.functorialityEquivalence_functor : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (e : C ≌ D),
  (CategoryTheory.Limits.Cone.functorialityEquivalence F e).functor =
    CategoryTheory.Limits.Cone.functoriality F e.functor
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.closure_le_centralizer_centralizer : ∀ {R : Type u_1} [inst : Ring R] (s : Set R), Subring.closure s ≤ Subring.centralizer ↑(Subring.centralizer s)
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
CategoryTheory.ShortComplex.FunctorEquivalence.unitIso_hom_app_τ₁_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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (X : CategoryTheory.ShortComplex (CategoryTheory.Functor J C)) (X_1 : J),
  ((CategoryTheory.ShortComplex.FunctorEquivalence.unitIso J C).hom.app X).τ₁.app X_1 =
    CategoryTheory.CategoryStruct.id (X.X₁.obj X_1)
-- Lean.DocString.Types
Lean.Doc.Inline.math.sizeOf_spec : ∀ {i : Type u} [inst : SizeOf i] (mode : Lean.Doc.MathMode) (string : String),
  sizeOf (Lean.Doc.Inline.math mode string) = 1 + sizeOf mode + sizeOf string
-- Mathlib.Order.Interval.Set.Basic
Set.Ioc_subset_Icc_self : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioc a b ⊆ Set.Icc a b
-- Init.Data.String.Basic
String.Pos.Raw.isValidForSlice_sliceTo : ∀ {s : String.Slice} {p : s.Pos} {off : String.Pos.Raw},
  String.Pos.Raw.IsValidForSlice (s.sliceTo p) off ↔ off ≤ p.offset ∧ String.Pos.Raw.IsValidForSlice s off
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.Bicategory.leftUnitor_hom_τr : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} (α : a ⟶ b),
  (CategoryTheory.Bicategory.Adj.Bicategory.leftUnitor α).hom.τr = (CategoryTheory.Bicategory.rightUnitor α.r).inv
-- Mathlib.NumberTheory.MulChar.Lemmas
/-- There is a character of order `n` on `F` if `#F ≡ 1 mod n` and the target contains
a primitive `n`th root of unity.  -/
MulChar.exists_mulChar_orderOf : ∀ (F : Type u_1) [inst : Field F] [inst_1 : Fintype F] {R : Type u_2} [inst_2 : CommRing R] {n : ℕ},
  n ∣ Fintype.card F - 1 → ∀ {ζ : R}, IsPrimitiveRoot ζ n → ∃ χ, orderOf χ = n
-- Mathlib.Algebra.Star.Unitary
Unitary.inv_mem : ∀ {G : Type u_2} [inst : Group G] [inst_1 : StarMul G] {g : G}, g ∈ unitary G → g⁻¹ ∈ unitary G
-- Lean.Expr
/-- Given `a b : Int`, returns `a < b`  -/
Lean.mkIntLT : Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- Additivity of a multilinear map along all coordinates at the same time,
writing `f (m + m')` as the sum of `f (s.piecewise m m')` over all sets `s`.  -/
MultilinearMap.map_add_univ : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) [inst_5 : DecidableEq ι] [inst_6 : Fintype ι]
  (m m' : (i : ι) → M₁ i), f (m + m') = ∑ s, f (s.piecewise m m')
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cocone.toCostructuredArrow_comp_toOver_comp_forget : ∀ {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.Cocone F),
  c.toCostructuredArrow.comp ((CategoryTheory.CostructuredArrow.toOver F c.pt).comp (CategoryTheory.Over.forget c.pt)) =
    F
-- Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
/-- When `j` is a limit element, this is the element in `Φ.Iteration j`
that is constructed from elements in `Φ.Iteration i` for all `i < j`.  -/
CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {Φ : CategoryTheory.SmallObject.SuccStruct C} →
      {J : Type u} →
        [inst_1 : LinearOrder J] →
          [inst_2 : OrderBot J] →
            [inst_3 : SuccOrder J] →
              [inst_4 : WellFoundedLT J] →
                [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C] →
                  {j : J} → Order.IsSuccLimit j → ((i : J) → i < j → Φ.Iteration i) → Φ.Iteration j
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
/-- All objects that are binary products of objects in `P`.  -/
CategoryTheory.ObjectProperty.binaryProductsClosure : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.ObjectProperty C → CategoryTheory.ObjectProperty C
-- Lean.Elab.Exception
Lean.Elab.isAutoBoundImplicitLocalException? : Lean.Exception → Option Lean.Name
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntInfo.rangeExpr : Lean.Meta.Grind.Arith.Cutsat.ToIntInfo → Lean.Expr
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instNonAssocSemiringQuotient : {R : Type u_1} → [inst : NonAssocSemiring R] → (c : RingCon R) → NonAssocSemiring c.Quotient
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.coe_toEquiv : ∀ {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₂),
  ⇑e.toEquiv = ⇑e
-- Mathlib.Analysis.Convex.PathConnected
Path.segment.congr_simp : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [inst_3 : ContinuousAdd E]
  [inst_4 : ContinuousSMul ℝ E] (a b : E), Path.segment a b = Path.segment a b
-- Mathlib.Analysis.Meromorphic.Divisor
/-- Divisors are invariant under translation, special case where the set is a closed ball.  -/
MeromorphicOn.divisor_closedBall_comp_sub_const_eq_divisor_closedBall : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {z : 𝕜} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {c : 𝕜} {R : ℝ} {f : 𝕜 → E},
  (MeromorphicOn.divisor (f ∘ fun x => x - c) (Metric.closedBall c R)) (z + c) =
    (MeromorphicOn.divisor f (Metric.closedBall 0 R)) z
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- If `N` is boundaryless, `∂(M×N) = ∂M × N`.  -/
ModelWithCorners.boundary_of_boundaryless_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {N : Type u_7}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H' N] {J : ModelWithCorners 𝕜 E' H'} [BoundarylessManifold J N],
  ModelWithCorners.boundary (M × N) = (ModelWithCorners.boundary M).prod Set.univ
-- Mathlib.Data.List.Intervals
List.Ico.length : ∀ (n m : ℕ), (List.Ico n m).length = m - n
-- Mathlib.Probability.Distributions.Exponential
ProbabilityTheory.stronglyMeasurable_exponentialPDFReal : ∀ (r : ℝ), MeasureTheory.StronglyMeasurable (ProbabilityTheory.exponentialPDFReal r)