mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLin_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  {M₁ : Type u_5} {M₂ : Type u_6} [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R M₁]
  [inst_6 : Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) [inst_7 : Fintype m] (M : Matrix m n R)
  (v : M₁), ((Matrix.toLin v₁ v₂) M) v = ∑ j, M.mulVec (⇑(v₁.repr v)) j • v₂ j
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
/-- The functional equation for the Jacobi theta function: `jacobiTheta₂ z τ` is an explicit factor
times `jacobiTheta₂ (z / τ) (-1 / τ)`. This is the key lemma behind the proof of the functional
equation for L-series of even Dirichlet characters.  -/
jacobiTheta₂_functional_equation : ∀ (z τ : ℂ),
  jacobiTheta₂ z τ =
    1 / (-Complex.I * τ) ^ (1 / 2) * Complex.exp (-↑Real.pi * Complex.I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.instUnique.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Subsingleton R],
  AddMonoidAlgebra.instUnique = { default := AddMonoidAlgebra.coeffEquiv.symm default, uniq := ⋯ }
-- Lean.Parser.Term
Lean.Parser.Tactic.quotSeq : Lean.Parser.Parser
-- Mathlib.Analysis.Seminorm
/-- **Alias** of `FunLike.coeAddMonoidHom_injective`. -/
Seminorm.coeFnAddMonoidHom_injective : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : AddZero F] [inst_2 : AddZeroClass β]
  [inst_3 : IsZeroApply F α β] [inst_4 : IsAddApply F α β], Function.Injective ⇑(FunLike.coeAddMonoidHom F α β)
-- Mathlib.GroupTheory.IsSubnormal
/-- If the subgroup `H` of a group `G` is trivial, then it is subnormal.  -/
Subgroup.IsSubnormal.of_subsingleton : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} [Subsingleton ↥H], H.IsSubnormal
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
HomotopicalAlgebra.AttachCells.reindex_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a}
  {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : HomotopicalAlgebra.AttachCells g f) {ι' : Type w'} (e : ι' ≃ c.ι), (c.reindex e).ι = ι'
-- Mathlib.NumberTheory.FLT.Basic
FermatLastTheoremWith.fermatLastTheoremWith' : ∀ {R : Type u_2} [inst : CommSemiring R] {n : ℕ}, FermatLastTheoremWith R n → FermatLastTheoremWith' R n
-- Batteries.Data.UnionFind.Basic
/-- Array of nodes  -/
Batteries.UnionFind.FindAux.s : {n : ℕ} → Batteries.UnionFind.FindAux n → Array Batteries.UFNode
-- Mathlib.Algebra.Homology.TotalComplexShift
HomologicalComplex₂.D₂_totalShift₁XIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [inst_2 : K.HasTotal (ComplexShape.up ℤ)]
  (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + x = n₀') (h₁ : n₁ + x = n₁'),
  CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₁ C x).obj K).D₂ (ComplexShape.up ℤ) n₀ n₁)
      (K.totalShift₁XIso x n₁ n₁' h₁).hom =
    x.negOnePow •
      CategoryTheory.CategoryStruct.comp (K.totalShift₁XIso x n₀ n₀' h₀).hom (K.D₂ (ComplexShape.up ℤ) n₀' n₁')
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.spanExt_app_one : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z')
  {f : X ⟶ Y} {g : X ⟶ Z} {f' : X' ⟶ Y'} {g' : X' ⟶ Z'}
  (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom)
  (wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom),
  (CategoryTheory.Limits.spanExt iX iY iZ wf wg).app CategoryTheory.Limits.WalkingSpan.zero = iX
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.contains.match_1.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.lt with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_1 ()
-- Mathlib.Analysis.Normed.Algebra.Exponential
IsSelfAdjoint.exp : ∀ {𝔸 : Type u_2} [inst : Ring 𝔸] [inst_1 : TopologicalSpace 𝔸] [inst_2 : IsTopologicalRing 𝔸] [T2Space 𝔸]
  [inst_4 : StarRing 𝔸] [ContinuousStar 𝔸] {x : 𝔸}, IsSelfAdjoint x → IsSelfAdjoint (NormedSpace.exp x)
-- Mathlib.Data.Matrix.Diagonal
Matrix.instIntCastOfZero : {n : Type u_3} → {α : Type v} → [DecidableEq n] → [Zero α] → [IntCast α] → IntCast (Matrix n n α)
-- Mathlib.Order.Filter.FilterProduct
Filter.Germ.const_min : ∀ {α : Type u} {β : Type v} {φ : Ultrafilter α} [inst : LinearOrder β] (x y : β), ↑(min x y) = min ↑x ↑y
-- Mathlib.Topology.Order.OrderClosed
continuous_min : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α],
  Continuous fun p => min p.1 p.2
-- Mathlib.CategoryTheory.MorphismProperty.Representable
/-- If `P : MorphismProperty C` is stable under base change, `F` is fully faithful and preserves
pullbacks, and `C` has all pullbacks, then for any `f : a ⟶ b` in `C`, `F.map f` satisfies
`P.relative` if `f` satisfies `P`.  -/
CategoryTheory.MorphismProperty.relative_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {P : CategoryTheory.MorphismProperty C} [F.Faithful] [F.Full]
  [CategoryTheory.Limits.HasPullbacks C] [P.IsStableUnderBaseChange] {a b : C} {f : a ⟶ b}
  [∀ (c : C) (g : c ⟶ b), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) F],
  P f → CategoryTheory.MorphismProperty.relative F P (F.map f)
-- Mathlib.Data.BitVec
BitVec.toFin_zsmul : ∀ {w : ℕ} (z : ℤ) (x : BitVec w), (z • x).toFin = z • x.toFin
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.instMulActionWithZeroSubtypeMem : {R' : Type u_1} →
  {α : Type u_2} →
    [inst : Semiring R'] →
      {S' : Type u_5} →
        [inst_1 : SetLike S' R'] →
          [inst_2 : SubsemiringClass S' R'] →
            (s : S') → [inst_3 : Zero α] → [MulActionWithZero R' α] → MulActionWithZero (↥s) α
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.tan_sub' : ∀ {x y : ℝ},
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * Real.pi / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * Real.pi / 2) →
    Real.tan (x - y) = (Real.tan x - Real.tan y) / (1 + Real.tan x * Real.tan y)
-- Std.Time.Date.Unit.Day
Std.Time.Day.instSubOffset : Sub Std.Time.Day.Offset
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.prodComparisonIso.congr_simp : ∀ {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) (A B : C)
  [inst_4 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) F],
  CategoryTheory.CartesianMonoidalCategory.prodComparisonIso F A B =
    CategoryTheory.CartesianMonoidalCategory.prodComparisonIso F A B
-- Mathlib.RingTheory.Length
Module.length_eq_top_iff_infiniteDimensionalOrder : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.length R M = ⊤ ↔ InfiniteDimensionalOrder (Submodule R M)
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.Measure.QuasiMeasurePreserving.preimage_iterate_ae_eq : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → α},
  MeasureTheory.Measure.QuasiMeasurePreserving f μ μ → ∀ (k : ℕ), f ⁻¹' s =ᵐ[μ] s → f^[k] ⁻¹' s =ᵐ[μ] s
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.le_orderTop_of_leadingCoeff_eq : ∀ {R : Type u_3} [inst : AddGroup R] {Γ : Type u_8} [inst_1 : LinearOrder Γ] {x y : HahnSeries Γ R} {g : Γ},
  x.orderTop = ↑g → y.orderTop = ↑g → x.leadingCoeff = y.leadingCoeff → ↑g < (x - y).orderTop
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.ElementaryEmbedding.map_rel : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
  (φ : L.ElementaryEmbedding M N) {n : ℕ} (r : L.Relations n) (x : Fin n → M),
  FirstOrder.Language.Structure.RelMap r (⇑φ ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x
-- Lean.Parser.Extra
Lean.Parser.hygieneInfo.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Order.Monotone.Basic
strictMono_dual_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  StrictMono (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) ↔ StrictMono f
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.arrowCongrₗ_symm_apply : ∀ {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8} {V₄ : Type u_9}
  [inst : AddCommGroup V₁] [inst_1 : AddCommGroup V₂] [inst_2 : AddCommGroup V₃] [inst_3 : AddCommGroup V₄]
  [inst_4 : AddTorsor V₁ P₁] [inst_5 : AddTorsor V₂ P₂] {R : Type u_10} [inst_6 : CommRing R] [inst_7 : Module R V₁]
  [inst_8 : Module R V₂] [inst_9 : Module R V₃] [inst_10 : Module R V₄] (e₁ : P₁ ≃ᵃ[R] P₂) (e₂ : V₃ ≃ₗ[R] V₄)
  (f : P₂ →ᵃ[R] V₄) (x : P₁), ((e₁.arrowCongrₗ e₂).symm f) x = e₂.symm (f (e₁ x))
-- Mathlib.MeasureTheory.VectorMeasure.Integral
Topology.IsClosedEmbedding.integral_map_vectorMeasure : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {β : Type u_9}
  [inst_6 : MeasurableSpace β] {φ : X → β} [inst_7 : TopologicalSpace X] [BorelSpace X] [inst_9 : TopologicalSpace β]
  [BorelSpace β],
  Topology.IsClosedEmbedding φ → ∀ {f : β → E}, ∫ᵛ (y : β), f y ∂[B; μ.map φ] = ∫ᵛ (x : X), f (φ x) ∂[B; μ]
-- Mathlib.Topology.Order.LocalExtr
IsExtrOn.isLocalExtr : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsExtrOn f s a → s ∈ nhds a → IsLocalExtr f a
-- Mathlib.Data.ZMod.Basic
/-- Any ring homomorphism into `ZMod n` is surjective.  -/
ZMod.ringHom_surjective : ∀ {n : ℕ} {R : Type u_1} [inst : NonAssocRing R] (f : R →+* ZMod n), Function.Surjective ⇑f
-- Mathlib.Data.Sum.Basic
Sum.update_inr_apply_inr : ∀ {α : Type u} {β : Type v} {γ : Type u_1} [inst : DecidableEq β] [inst_1 : DecidableEq (α ⊕ β)] {f : α ⊕ β → γ}
  {i j : β} {x : γ}, Function.update f (Sum.inr i) x (Sum.inr j) = Function.update (f ∘ Sum.inr) i x j
-- Mathlib.Data.Sign.Basic
/-- `SignType.cast` as a `MulWithZeroHom`.  -/
SignType.castHom : {α : Type u_1} → [inst : MulZeroOneClass α] → [HasDistribNeg α] → SignType →*₀ α
-- Init.Data.Float.Model.Float32
Float32.Model.mk.inj : ∀ {toBits : UInt32} {valid : Float.Model.Format.binary32.Valid toBits.toBitVec} {toBits_1 : UInt32}
  {valid_1 : Float.Model.Format.binary32.Valid toBits_1.toBitVec},
  { toBits := toBits, valid := valid } = { toBits := toBits_1, valid := valid_1 } → toBits = toBits_1
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.instMonadBacktrackSavedStateTacticM : Lean.MonadBacktrack Lean.Elab.Tactic.SavedState Lean.Elab.Tactic.TacticM
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_apply_one : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {f : R → R},
  cfc f 1 = (algebraMap R A) (f 1)
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.EffectiveEquivalenceRelation.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R A : C} {p₁ p₂ : R ⟶ A}
  (toEquivalenceRelation : CategoryTheory.EquivalenceRelation p₁ p₂) (B : C) (π : A ⟶ B)
  (isKernelPair : CategoryTheory.IsKernelPair π p₁ p₂) (isPushout : CategoryTheory.IsPushout p₁ p₂ π π)
  (toEquivalenceRelation_1 : CategoryTheory.EquivalenceRelation p₁ p₂) (B_1 : C) (π_1 : A ⟶ B_1)
  (isKernelPair_1 : CategoryTheory.IsKernelPair π_1 p₁ p₂) (isPushout_1 : CategoryTheory.IsPushout p₁ p₂ π_1 π_1),
  ({ toEquivalenceRelation := toEquivalenceRelation, B := B, π := π, isKernelPair := isKernelPair,
        isPushout := isPushout } =
      { toEquivalenceRelation := toEquivalenceRelation_1, B := B_1, π := π_1, isKernelPair := isKernelPair_1,
        isPushout := isPushout_1 }) =
    (toEquivalenceRelation = toEquivalenceRelation_1 ∧ B = B_1 ∧ π ≍ π_1)
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinAddOrder.prod_mk : ∀ {α : Type u_4} {β : Type u_5} [inst : AddMonoid α] [inst_1 : AddMonoid β] {a : α} {b : β},
  IsOfFinAddOrder a → IsOfFinAddOrder b → IsOfFinAddOrder (a, b)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
CategoryTheory.Functor.pushforward_cover_iff_cover_pullback : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D)
  (K : CategoryTheory.GrothendieckTopology D) [G.LocallyCoverDense K] [G.Full] [G.Faithful] {X : C}
  (S : CategoryTheory.Sieve X),
  CategoryTheory.Sieve.functorPushforward G S ∈ K (G.obj X) ↔ ∃ T, CategoryTheory.Sieve.functorPullback G ↑T = S
-- Lean.Level
Lean.Level.getOffsetAux : Lean.Level → ℕ → ℕ
-- Mathlib.Util.AtomM
/-- The reducibility setting for definitional equality of atoms  -/
Mathlib.Tactic.AtomM.Context.red : Mathlib.Tactic.AtomM.Context → Lean.Meta.TransparencyMode
-- Init.Data.Ord.Basic
Ordering.noConfusionType : Sort v✝ → Ordering → Ordering → Sort v✝
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.sInter_vadd_subset : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] (S : Set (Set α)) (t : Set β), ⋂₀ S +ᵥ t ⊆ ⋂ s ∈ S, s +ᵥ t
-- Mathlib.Analysis.RCLike.Basic
_private.Mathlib.Analysis.RCLike.Basic.0.RCLike.termNormSqR : Lean.ParserDescr
-- Lean.Elab.InfoTree.Main
Lean.Elab.FVarAliasInfo.format : Lean.Elab.FVarAliasInfo → Std.Format
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.homologyData_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [inst_2 : CategoryTheory.Limits.HasZeroObject C] (s : S.Splitting),
  s.homologyData.iso = CategoryTheory.Iso.refl 0
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- From a natural transformation of functors `C ⥤ D`, the induced natural transformation
of functors `WithInitial C ⥤ WithInitial D`.  -/
CategoryTheory.WithInitial.map₂ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        {F G : CategoryTheory.Functor C D} →
          (F ⟶ G) → (CategoryTheory.WithInitial.map F ⟶ CategoryTheory.WithInitial.map G)
-- Mathlib.Probability.Kernel.Composition.Lemmas
/-- The composition of two product kernels `(ξ ×ₖ η') ∘ₖ (ζ ×ₖ κ)` is the product of the
compositions, `(ξ ∘ₖ (ζ ×ₖ κ)) ×ₖ (η' ∘ₖ (ζ ×ₖ κ))`, if `ζ` is deterministic (of the form
`.deterministic f hf`) and `η'` does not depend on the output of `κ`.
That is, `η'` has the form `η.prodMkRight β` for a kernel `η`.

If `κ` was deterministic, this would be true even if `η.prodMkRight β` was a more general
kernel since `Kernel.deterministic f hf ×ₖ κ` would be deterministic and commute with copying.
Here `κ` is not deterministic, but it is discarded in one branch of the copy.  -/
ProbabilityTheory.Kernel.prod_prodMkRight_comp_deterministic_prod : ∀ {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
  {mδ : MeasurableSpace δ} {β' : Type u_5} {ε : Type u_6} {mβ' : MeasurableSpace β'} {mε : MeasurableSpace ε}
  (κ : ProbabilityTheory.Kernel γ β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel ε β')
  [ProbabilityTheory.IsSFiniteKernel η] (ξ : ProbabilityTheory.Kernel (ε × β) δ) [ProbabilityTheory.IsSFiniteKernel ξ]
  {f : γ → ε} (hf : Measurable f),
  (ξ.prod (ProbabilityTheory.Kernel.prodMkRight β η)).comp ((ProbabilityTheory.Kernel.deterministic f hf).prod κ) =
    (ξ.comp ((ProbabilityTheory.Kernel.deterministic f hf).prod κ)).prod
      (η.comp (ProbabilityTheory.Kernel.deterministic f hf))
-- Mathlib.CategoryTheory.Action
/-- The projection from the action category to the monoid, mapping a morphism to its
label.  -/
CategoryTheory.ActionCategory.π : (M : Type u_1) →
  [inst : Monoid M] →
    (X : Type u) →
      [inst_1 : MulAction M X] → CategoryTheory.Functor (CategoryTheory.ActionCategory M X) (CategoryTheory.SingleObj M)
-- Mathlib.Algebra.Quandle
Rack.left_cancel_inv : ∀ {R : Type u_1} [inst : Rack R] (x : R) {y y' : R}, Rack.invAct x y = Rack.invAct x y' ↔ y = y'
-- Batteries.Data.Float.Lemmas
_private.Batteries.Data.Float.Lemmas.0.Float.Model.UnpackedFloat.isNaN.match_1.eq_1 : ∀ (motive : Float.Model.UnpackedFloat → Sort u_1) (h_1 : Unit → motive Float.Model.UnpackedFloat.notANumber)
  (h_2 : (x : Float.Model.UnpackedFloat) → motive x),
  (match Float.Model.UnpackedFloat.notANumber with
    | Float.Model.UnpackedFloat.notANumber => h_1 ()
    | x => h_2 x) =
    h_1 ()
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.le_opNorm_of_le : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F)
  {c : ℝ} {x : E}, ‖x‖ ≤ c → ‖f x‖ ≤ ‖f‖ * c
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
IsClub.isNormal_enum : ∀ {α : Type v} [inst : LinearOrder α] [inst_1 : WellFoundedLT α] [inst_2 : IsRegularCardinalOrder α] {s : Set α}
  (hs : IsClub s), Order.IsNormal (Subtype.val ∘ ⇑(Order.enum s ⋯))
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
/-- The topology of weak convergence on `MeasureTheory.ProbabilityMeasure Ω`. This is inherited
(induced) from the topology of weak convergence of finite measures via the inclusion
`MeasureTheory.ProbabilityMeasure.toFiniteMeasure`.  -/
MeasureTheory.ProbabilityMeasure.instTopologicalSpace : {Ω : Type u_1} →
  [inst : MeasurableSpace Ω] →
    [inst_1 : TopologicalSpace Ω] → [OpensMeasurableSpace Ω] → TopologicalSpace (MeasureTheory.ProbabilityMeasure Ω)
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Hom.id_apply : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (x : M), (FirstOrder.Language.Hom.id L M) x = x
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofIsIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y)
  [CategoryTheory.IsIso f], AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f
-- Mathlib.Algebra.Group.TypeTags.Basic
instInhabitedMultiplicative : {α : Type u} → [Inhabited α] → Inhabited (Multiplicative α)
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
/-- The units of the fundamental system and the torsion of `K` generate the full group of units of `K`.
 -/
NumberField.Units.closure_fundSystem_sup_torsion_eq_top : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  Subgroup.closure (Set.range (NumberField.Units.fundSystem K)) ⊔ NumberField.Units.torsion K = ⊤
-- Mathlib.Topology.Algebra.Group.Basic
Filter.map_divLeft_nhdsLT : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : CommGroup H] [IsTopologicalGroup H] [inst_3 : PartialOrder H]
  [IsOrderedMonoid H] {c a : H},
  Filter.map (fun x => c / x) (nhdsWithin a (Set.Iio a)) = nhdsWithin (c / a) (Set.Ioi (c / a))
-- Mathlib.Topology.Algebra.UniformConvergence
instOneUniformFun : {α : Type u_1} → {β : Type u_2} → [One β] → One (UniformFun α β)
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepSets_singleton_iff : ∀ {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  (hm' : m' ≤ mΩ) (s : ι → Set Ω),
  (∀ (i : ι), MeasurableSet (s i)) →
    ∀ (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
      ProbabilityTheory.iCondIndepSets m' hm' (fun i => {s i}) μ ↔
        ∀ (S : Finset ι), μ[(⋂ i ∈ S, s i).indicator fun ω => 1 | m'] =ᵐ[μ] ∏ i ∈ S, μ[(s i).indicator fun ω => 1 | m']
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.le_lift_iff : ∀ {a : Ordinal.{u}} {b : Ordinal.{max u v}}, b ≤ Ordinal.lift.{v, u} a ↔ ∃ a' ≤ a, Ordinal.lift.{v, u} a' = b
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
PiTensorProduct.injectiveSeminorm_tprod_le : ∀ {ι : Type uι} [inst : Fintype ι] {𝕜 : Type u𝕜} [inst_1 : NontriviallyNormedField 𝕜] {E : ι → Type uE}
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] (m : (i : ι) → E i),
  PiTensorProduct.injectiveSeminorm (⨂ₜ[𝕜] (i : ι), m i) ≤ ∏ i, ‖m i‖
-- Init.Data.Float.Float32
/-- Converts a floating-point number to a string.

This function does not reduce in the kernel.
 -/
Float32.toString : Float32 → String
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_const_preimage : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] (U : Set α) (s : Set M) (a : M),
  (U.mulIndicator fun x => a) ⁻¹' s ∈ {Set.univ, U, Uᶜ, ∅}
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S T : C}
  [inst_1 : J.IsStableUnderBaseChange] (f : S ⟶ T) (E : J.ZeroHypercover T)
  [inst_2 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)],
  (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f E).toPreZeroHypercover =
    CategoryTheory.PreZeroHypercover.pullback₁ f E.toPreZeroHypercover
-- Mathlib.GroupTheory.Sylow
Sylow.normalizer_normalizer : ∀ {G : Type u} [inst : Group G] {p : ℕ} [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G),
  Subgroup.normalizer ↑(Subgroup.normalizer ↑P) = Subgroup.normalizer ↑P
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- Endowing the space `PiLp p α` with the `L^p` pseudometric structure. This definition is not
satisfactory, as it does not register the fact that the topology, the uniform structure, and the
bornology coincide with the product ones. Therefore, we do not register it as an instance. Using
this as a temporary pseudoemetric space instance, we will show that the uniform structure is equal
(but not defeq) to the product one, and then register an instance in which we replace the uniform
structure and the bornology by the product ones using this pseudometric space,
`PseudoMetricSpace.replaceUniformity`, and `PseudoMetricSpace.replaceBornology`.

See note [reducible non-instances]  -/
PiLp.pseudoMetricAux : (p : ENNReal) →
  {ι : Type u_2} →
    (α : ι → Type u_3) →
      [Fact (1 ≤ p)] → [(i : ι) → PseudoMetricSpace (α i)] → [Fintype ι] → PseudoMetricSpace (PiLp p α)
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
CategoryTheory.Limits.Types.Pushout.equivalence_rel' : ∀ {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) [CategoryTheory.Mono f],
  Equivalence (CategoryTheory.Limits.Types.Pushout.Rel' f g)
-- Mathlib.Analysis.SumIntegralComparisons
/-- The sum of a nonnegative, antitone function is bounded below by its integral.  -/
AntitoneOn.integral_le_tsum : ∀ {f : ℝ → ℝ},
  AntitoneOn f (Set.Ici 0) →
    (Summable fun n => f ↑n) → (∀ t ∈ Set.Ioi 0, 0 ≤ f t) → ∫ (x : ℝ) in Set.Ioi 0, f x ≤ ∑' (n : ℕ), f ↑n
-- Mathlib.RingTheory.Ideal.Operations
Submodule.map_le_smul_top : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (I : Ideal R)
  (f : R →ₗ[R] M), Submodule.map f I ≤ I • ⊤
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.GetLsbD
Std.Tactic.BVDecide.BVPred.GetLsbDTarget.mk.sizeOf_spec : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} [inst_2 : SizeOf α] {w : ℕ}
  (vec : aig.RefVec w) (idx : ℕ), sizeOf { w := w, vec := vec, idx := idx } = 1 + sizeOf w + sizeOf vec + sizeOf idx