mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Metrizable.Basic
/-- If a set `s` is separable in a pseudo metrizable space, then it admits a countable dense
subset. This is not obvious, as the countable set whose closure covers `s` given by the definition
of separability does not need in general to be contained in `s`.  -/
TopologicalSpace.IsSeparable.exists_countable_dense_subset : ∀ {X : Type u_2} [inst : TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] {s : Set X},
  TopologicalSpace.IsSeparable s → ∃ t ⊆ s, t.Countable ∧ s ⊆ closure t
-- Mathlib.Analysis.Complex.Trigonometric
Real.cos_sq_le_one : ∀ (x : ℝ), Real.cos x ^ 2 ≤ 1
-- Mathlib.Algebra.Lie.Subalgebra
/-- A Lie subalgebra forms a new Lie ring.  -/
LieSubalgebra.lieRing : (R : Type u) →
  (L : Type v) →
    [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → (L' : LieSubalgebra R L) → LieRing ↥L'
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
FDerivMeasurableAux.B.eq_1 : ∀ {𝕜 : 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 : E → F)
  (K : Set (E →L[𝕜] F)) (r s ε : ℝ),
  FDerivMeasurableAux.B f K r s ε = ⋃ L ∈ K, FDerivMeasurableAux.A f L r ε ∩ FDerivMeasurableAux.A f L s ε
-- Mathlib.Algebra.Group.Units.Hom
/-- A local homomorphism `f : R ⟶ S` will send nonunits of `R` to nonunits of `S`.  -/
IsLocalHom.map_nonunit : ∀ {R : Type u_2} {S : Type u_3} {F : Type u_5} {inst : Monoid R} {inst_1 : Monoid S} {inst_2 : FunLike F R S} {f : F}
  [self : IsLocalHom f] (a : R), IsUnit (f a) → IsUnit a
-- Mathlib.Data.Set.Sups
Set.iUnion_image_inf_right : ∀ {α : Type u_2} [inst : SemilatticeInf α] (s t : Set α), ⋃ b ∈ t, (fun x => x ⊓ b) '' s = s ⊼ t
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.universalAddHom_apply : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {T : Type u_2}
  [inst_2 : AddMonoid T] (f : R →+ T) (fS : ↥S →+ AddUnits T) (hf : ∀ (s : ↥S), f ↑s = ↑(fS s)) {r : R} {s : ↥S},
  (AddOreLocalization.universalAddHom f fS hf) (r -ₒ s) = ↑(-fS s) + f r
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.instAddCommGroupCotangent : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → [inst_2 : Algebra R S] → (P : Algebra.Extension R S) → AddCommGroup P.Cotangent
-- Mathlib.Data.FunLike.Embedding
EmbeddingLike.injective : ∀ {F : Sort u_1} {α : Sort u_2} {β : Sort u_3} [inst : FunLike F α β] [i : EmbeddingLike F α β] (f : F),
  Function.Injective ⇑f
-- Mathlib.RingTheory.PicardGroup
TensorProduct.liftAux.eq_1 : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {P₂ : Type u_17} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : AddCommMonoid P₂]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R₂ P₂] (f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂),
  TensorProduct.liftAux f' = TensorProduct.liftAddHom (LinearMap.toAddMonoidHom'.comp f'.toAddMonoidHom) ⋯
-- Mathlib.Data.Sym.Card
Sym2.card_subtype_not_diag : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α],
  Fintype.card { a // ¬a.IsDiag } = (Fintype.card α).choose 2
-- Mathlib.Algebra.Group.Subgroup.Map
AddEquiv.coe_comapAddSubgroup : ∀ {G : Type u_1} [inst : AddGroup G] {H : Type u_5} [inst_1 : AddGroup H] (e : G ≃+ H),
  ⇑e.comapAddSubgroup = AddSubgroup.comap e.toAddMonoidHom
-- Mathlib.Order.MinMax
max_lt_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, max b c < a ↔ b < a ∧ c < a
-- Lean.ErrorExplanation
Lean.ErrorExplanation.Metadata.mk.inj : ∀ {summary sinceVersion : String} {severity : Lean.MessageSeverity} {removedVersion? : Option String}
  {summary_1 sinceVersion_1 : String} {severity_1 : Lean.MessageSeverity} {removedVersion?_1 : Option String},
  { summary := summary, sinceVersion := sinceVersion, severity := severity, removedVersion? := removedVersion? } =
      { summary := summary_1, sinceVersion := sinceVersion_1, severity := severity_1,
        removedVersion? := removedVersion?_1 } →
    summary = summary_1 ∧ sinceVersion = sinceVersion_1 ∧ severity = severity_1 ∧ removedVersion? = removedVersion?_1
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_congr_nnnorm_ae : ∀ {α : Type u_1} {F : Type u_5} {G : Type u_6} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F] [inst_1 : NormedAddCommGroup G] {f : α → F} {g : α → G},
  (∀ᵐ (x : α) ∂μ, ‖f x‖₊ = ‖g x‖₊) → MeasureTheory.eLpNorm f p μ = MeasureTheory.eLpNorm g p μ
-- Mathlib.Topology.Category.TopPair
/-- A pair of topological spaces consists of an embedding `f : A ⟶ X` in `TopCat`.  -/
TopPair : Type (u_1 + 1)
-- Mathlib.Computability.RegularExpressions
RegularExpression.brecOn.go : {α : Type u} →
  {motive : RegularExpression α → Sort u_1} →
    (t : RegularExpression α) →
      ((t : RegularExpression α) → RegularExpression.below t → motive t) → motive t ×' RegularExpression.below t
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.compNatIsoDiscrete_hom_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {D : Type u₃}
  [inst_1 : CategoryTheory.Category.{v₃, u₃} D] (F : I → C) (G : CategoryTheory.Functor C D)
  (X : CategoryTheory.Discrete I),
  (CategoryTheory.Discrete.compNatIsoDiscrete F G).hom.app X = CategoryTheory.CategoryStruct.id (G.obj (F X.as))
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.tendsto_pow_atTop_nhds_zero : ∀ (z : Complex.UnitDisc), Filter.Tendsto (fun n => z ^ n) Filter.atTop (nhds 0)
-- Mathlib.Algebra.Homology.HomotopyCategory
/-- The quotient functor from complexes to the homotopy category.  -/
HomotopyCategory.quotient : {ι : Type u_2} →
  (V : Type u) →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        (c : ComplexShape ι) → CategoryTheory.Functor (HomologicalComplex V c) (HomotopyCategory V c)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.reverse_isTrail_iff : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.reverse.IsTrail ↔ p.IsTrail
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.var.injEq : ∀ (i i_1 : Lean.Grind.Linarith.Var), (Lean.Grind.Linarith.Expr.var i = Lean.Grind.Linarith.Expr.var i_1) = (i = i_1)
-- Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
SimplexCategory.toMk₁_apply : ∀ {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)),
  (CategoryTheory.ConcreteCategory.hom (SimplexCategory.toMk₁ i)) j = if j.castSucc < i then 0 else 1
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
/-- The volume of the region between two almost everywhere measurable functions on a measurable set
can be represented as a Lebesgue integral.  -/
volume_regionBetween_eq_lintegral : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ} {s : Set α}
  [MeasureTheory.SFinite μ],
  AEMeasurable f (μ.restrict s) →
    AEMeasurable g (μ.restrict s) →
      MeasurableSet s →
        (μ.prod MeasureTheory.volume) (regionBetween f g s) = ∫⁻ (y : α) in s, ENNReal.ofReal ((g - f) y) ∂μ
-- Mathlib.Data.Nat.Prime.Basic
Nat.not_prime_of_dvd_of_lt : ∀ {m n : ℕ}, m ∣ n → 2 ≤ m → m < n → ¬Nat.Prime n
-- Mathlib.Algebra.Ring.CentroidHom
/-- Commutativity of centroid homomorphisms with right multiplication.  -/
CentroidHom.map_mul_right' : ∀ {α : Type u_6} [inst : NonUnitalNonAssocSemiring α] (self : CentroidHom α) (a b : α),
  (↑self.toAddMonoidHom).toFun (a * b) = (↑self.toAddMonoidHom).toFun a * b
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.constantCoeff_surj : ∀ {R : Type u_1} [inst : Semiring R], Function.Surjective ⇑PowerSeries.constantCoeff
-- Mathlib.Algebra.Order.Group.Cone
AddGroupCone.instAddGroupConeClass : ∀ (G : Type u_1) [inst : AddCommGroup G], AddGroupConeClass (AddGroupCone G) G
-- Mathlib.AlgebraicTopology.SimplicialSet.Op
/-- The covariant involution `opFunctor : SSet ⥤ SSet`,
as an equivalence of categories.  -/
SSet.opEquivalence : SSet ≌ SSet
-- Mathlib.FieldTheory.SeparableClosure
/-- An intermediate field of `E / F` is contained in the separable closure of `F` in `E`
if and only if it is separable over `F`.  -/
le_separableClosure_iff : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (L : IntermediateField F E),
  L ≤ separableClosure F E ↔ Algebra.IsSeparable F ↥L
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
ContinuousLinearMap.IsFredholm.of_isQuasiInverse : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E]
  [inst_6 : TopologicalSpace F] [CompleteSpace 𝕜] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [T2Space E] [T2Space F] {u : E →L[𝕜] F} {v : F →L[𝕜] E},
  (↑v).IsQuasiInverse ↑u → u.IsFredholm
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.finset_card_lt_aleph0 : ∀ {α : Type u} (s : Finset α), Cardinal.mk ↑↑s < Cardinal.aleph0
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.intCast_def : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : IntCast M] (n : ℤ), (↑fun x => ↑n) = ↑n
-- Mathlib.Algebra.Ring.Parity
Function.Involutive.iterate_eq_self : ∀ {α : Type u_4} {f : α → α} {n : ℕ}, Function.Involutive f → f ≠ id → (f^[n] = f ↔ Odd n)
-- Mathlib.Algebra.BigOperators.Finprod
/-- See `finprod_comp`, `Fintype.prod_bijective` and `Finset.prod_bij`.  -/
finprod_eq_of_bijective : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {g : β → M} (e : α → β),
  Function.Bijective e → (∀ (x : α), f x = g (e x)) → ∏ᶠ (i : α), f i = ∏ᶠ (j : β), g j
-- Std.Sat.AIG.Basic
Std.Sat.AIG.toGraphviz.go.eq_def : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : ToString α] [inst_2 : Hashable α] (acc : String)
  (decls : Array (Std.Sat.AIG.Decl α)) (hinv : Std.Sat.AIG.IsDAG α decls) (idx : ℕ) (hidx : idx < decls.size),
  Std.Sat.AIG.toGraphviz.go acc decls hinv idx hidx =
    have fidx := ⟨idx, hidx⟩;
    do
    let __do_lift ← get
    if __do_lift.contains fidx = true then pure acc
      else do
        modify fun s => s.insert fidx
        match elem : decls[idx] with
          | Std.Sat.AIG.Decl.false => pure acc
          | Std.Sat.AIG.Decl.atom idx_1 => pure acc
          | Std.Sat.AIG.Decl.gate lhs rhs =>
            let lidx := lhs.gate;
            have linv := lhs.invert;
            let ridx := rhs.gate;
            have rinv := rhs.invert;
            have curr :=
              toString idx ++ toString " -> " ++ toString lidx ++ toString (Std.Sat.AIG.toGraphviz.invEdgeStyle linv) ++
                          toString "; " ++
                        toString idx ++
                      toString " -> " ++
                    toString ridx ++
                  toString (Std.Sat.AIG.toGraphviz.invEdgeStyle rinv) ++
                toString ";";
            have hlr := ⋯;
            do
            let laig ← Std.Sat.AIG.toGraphviz.go (acc ++ curr) decls hinv lidx ⋯
            Std.Sat.AIG.toGraphviz.go laig decls hinv ridx ⋯
-- Lean.Linter.Init
Lean.Linter.LinterOptions.get? : {α : Type} → [Lean.KVMap.Value α] → Lean.Linter.LinterOptions → Lean.Name → Option α
-- Aesop.ElabM
Aesop.ElabM.Context.forAdditionalRules : Lean.MVarId → Aesop.ElabM.Context
-- Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
/-- A presheaf `(opens X)ᵒᵖ ⥤ C` on a topological space `X` is a sheaf on the site `opens X` iff
it satisfies the `IsSheafOpensLeCover` sheaf condition. The latter is not the
official definition of sheaves on spaces, but has the advantage that it does not
require `has_products C`.  -/
TopCat.Presheaf.isSheaf_iff_isSheafOpensLeCover : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : TopCat} (F : TopCat.Presheaf C X),
  F.IsSheaf ↔ F.IsSheafOpensLeCover
-- Lean.Meta.CongrTheorems
/-- `lhs` and `rhs` are `Decidable` instances which should have the same type after
we have applied other type casting operations. We use the helper theorem `Decidable.eq`
to perform the type cast operation.
 -/
_private.Lean.Meta.CongrTheorems.0.Lean.Meta.EqInfo.decSubsingleton : Lean.FVarId → Lean.FVarId → Lean.Meta.EqInfo✝
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
CategoryTheory.NatTrans.instRespectsIsoFunctorEquifibered : ∀ {J : Type u_1} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C], CategoryTheory.NatTrans.Equifibered.RespectsIso
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
/-- A scheme morphism as a partial map.  -/
AlgebraicGeometry.Scheme.Hom.toPartialMap : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → X.PartialMap Y
-- Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
InnerProductSpace.HarmonicContOnCl.neg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {s : Set E},
  InnerProductSpace.HarmonicContOnCl f s → InnerProductSpace.HarmonicContOnCl (-f) s
-- Init.Coe
CoeHTC.mk : {α : Sort u} → {β : Sort v} → (α → β) → CoeHTC α β
-- Mathlib.Topology.Order.Category.FrameAdjunction
/-- Characterization of when a subset of the space of points is open.  -/
Locale.PT.isOpen_iff : ∀ (L : Type u_1) [inst : CompleteLattice L] (U : Set (Locale.PT L)), IsOpen U ↔ ∃ u, {x | x u} = U
-- Lean.Expr
/-- Similar to `appFn`, but also applies `cleanupAnnotations` to resulting function.
This function is used compile the `match_expr` term.
 -/
Lean.Expr.appFnCleanup : (e : Lean.Expr) → e.isApp = true → Lean.Expr
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc.0.CategoryTheory.Limits.termF₁ : Lean.ParserDescr
-- Mathlib.Algebra.Category.ModuleCat.Ulift
/-- The universe lift functor for `R`-module is fully faithful.  -/
ModuleCat.fullyFaithfulUliftFunctor : (R : Type u) → [inst : Ring R] → (ModuleCat.uliftFunctor.{u_2, u_1, u} R).FullyFaithful
-- Mathlib.CategoryTheory.CatCommSq
CategoryTheory.CatCommSq.vComp_iso_inv_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₅ : Type u_5} {C₆ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₅] [inst_5 : CategoryTheory.Category.{v_6, u_6} C₆]
  (L₁ : CategoryTheory.Functor C₁ C₂) (L₂ : CategoryTheory.Functor C₂ C₃) (H₁ : CategoryTheory.Functor C₁ C₄)
  (H₂ : CategoryTheory.Functor C₂ C₅) (H₃ : CategoryTheory.Functor C₃ C₆) (R₁ : CategoryTheory.Functor C₄ C₅)
  (R₂ : CategoryTheory.Functor C₅ C₆) [inst_6 : CategoryTheory.CatCommSq H₁ L₁ R₁ H₂]
  [inst_7 : CategoryTheory.CatCommSq H₂ L₂ R₂ H₃] (X : C₁),
  (CategoryTheory.CatCommSq.iso H₁ (L₁.comp L₂) (R₁.comp R₂) H₃).inv.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso H₂ L₂ R₂ H₃).inv.app (L₁.obj X))
      (R₂.map ((CategoryTheory.CatCommSq.iso H₁ L₁ R₁ H₂).inv.app X))
-- Init.System.IO
IO.FS.instInhabitedSystemTime.default : IO.FS.SystemTime
-- Mathlib.Computability.StateTransition
StateTransition.tr_reaches_rev : ∀ {σ₁ : Type u_1} {σ₂ : Type u_2} {f₁ : σ₁ → Option σ₁} {f₂ : σ₂ → Option σ₂} {tr : σ₁ → σ₂ → Prop},
  StateTransition.Respects f₁ f₂ tr →
    ∀ {a₁ : σ₁} {a₂ : σ₂},
      tr a₁ a₂ →
        ∀ {b₂ : σ₂},
          StateTransition.Reaches f₂ a₂ b₂ →
            ∃ c₁ c₂, StateTransition.Reaches f₂ b₂ c₂ ∧ tr c₁ c₂ ∧ StateTransition.Reaches f₁ a₁ c₁
-- Mathlib.CategoryTheory.Limits.FullSubcategory
CategoryTheory.Limits.hasLimit_of_closedUnderLimits : ∀ (J : Type w) [inst : CategoryTheory.Category.{w', w} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderLimitsOfShape J]
  (F : CategoryTheory.Functor J P.FullSubcategory) [CategoryTheory.Limits.HasLimit (F.comp P.ι)],
  CategoryTheory.Limits.HasLimit F
-- Lean.Meta.Closure
_private.Lean.Meta.Closure.0.Lean.Meta.Closure.TopoSort.newDecls : Lean.Meta.Closure.TopoSort✝ → Array Lean.LocalDecl
-- Mathlib.Control.Monad.Cont
instMonadContWriterTOfMonadOfEmptyCollection : {m : Type u → Type v} → (ω : Type u) → [Monad m] → [EmptyCollection ω] → [MonadCont m] → MonadCont (WriterT ω m)
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Summable.tendsto_atTop_of_pos : ∀ {α : Type u_3} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : TopologicalSpace α]
  [OrderTopology α] {f : ℕ → α}, Summable f⁻¹ → (∀ (n : ℕ), 0 < f n) → Filter.Tendsto f Filter.atTop Filter.atTop
-- Init.Data.String.Basic
String.Pos.slice_inj : ∀ {s : String} {p₀ p₁ pos pos' : s.Pos} {h₁ : p₀ ≤ pos} {h₁' : p₀ ≤ pos'} {h₂ : pos ≤ p₁} {h₂' : pos' ≤ p₁},
  pos.slice p₀ p₁ h₁ h₂ = pos'.slice p₀ p₁ h₁' h₂' ↔ pos = pos'
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.Hom.mk.sizeOf_spec : ∀ {M N : SemiNormedGrp₁} (hom' : NormedAddGroupHom M.carrier N.carrier) (normNoninc : hom'.NormNoninc),
  sizeOf { hom' := hom', normNoninc := normNoninc } = 1 + sizeOf hom'
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.nsmul_hom : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {A B : Rep.{w, u, v} k G} (f : A ⟶ B) (n : ℕ),
  Rep.Hom.hom (n • f) = n • Rep.Hom.hom f
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.instHashableExpr_lean.hash : Lean.Grind.AC.Expr → UInt64
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.foldM_eq_foldlM_toArray : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {δ : Type w}
  {m' : Type w → Type w'} [inst : Monad m'] [LawfulMonad m'] {f : δ → (a : α) → β a → m' δ} {init : δ},
  Std.DHashMap.foldM f init m = Array.foldlM (fun a b => f a b.fst b.snd) init m.toArray
-- Mathlib.CategoryTheory.LiftingProperties.Adjunction
/-- When we have an adjunction `G ⊣ F`, any commutative square where the left
map is of the form `G.map i` and the right map is `p` has an "adjoint" commutative
square whose left map is `i` and whose right map is `F.map p`.  -/
CategoryTheory.CommSq.right_adjoint : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {G : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C}
  {A B : C} {X Y : D} {i : A ⟶ B} {p : X ⟶ Y} {u : G.obj A ⟶ X} {v : G.obj B ⟶ Y},
  CategoryTheory.CommSq u (G.map i) p v →
    ∀ (adj : G ⊣ F), CategoryTheory.CommSq ((adj.homEquiv A X) u) i (F.map p) ((adj.homEquiv B Y) v)
-- Mathlib.ModelTheory.DirectLimit
/-- The directed limit glues together the structures along the embeddings.  -/
FirstOrder.Language.DirectLimit.setoid : {L : FirstOrder.Language} →
  {ι : Type v} →
    [inst : Preorder ι] →
      (G : ι → Type w) →
        [inst_1 : (i : ι) → L.Structure (G i)] →
          (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) →
            [DirectedSystem G fun i j h => ⇑(f i j h)] →
              [IsDirectedOrder ι] → Setoid (FirstOrder.Language.Structure.Sigma f)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.EqResult : Type
-- Mathlib.Algebra.Category.Grp.Basic
GrpMaxAux.eq_1 : GrpMaxAux = AddGrpCat
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
/-- the morphism between left adjoints  -/
CategoryTheory.Bicategory.Adj.Hom₂.τl : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : CategoryTheory.Bicategory.Adj B} → {α β : a ⟶ b} → CategoryTheory.Bicategory.Adj.Hom₂ α β → (α.l ⟶ β.l)
-- Mathlib.Analysis.SpecialFunctions.Arcosh
/-- The function `Real.arcosh` is real analytic.  -/
Real.analyticOn_arcosh : ∀ {s : Set ℝ}, s ⊆ Set.Ioi 1 → AnalyticOn ℝ Real.arcosh s
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.support_indicator : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Zero β] {s : Set α} (hs : MeasurableSet s)
  (f : MeasureTheory.SimpleFunc α β),
  Function.support ⇑(MeasureTheory.SimpleFunc.piecewise s hs f (MeasureTheory.SimpleFunc.const α 0)) =
    s ∩ Function.support ⇑f
-- Mathlib.Algebra.RingQuot
_private.Mathlib.Algebra.RingQuot.0.RingQuot.instMul.eq_1 : ∀ {R : Type uR} [inst : Semiring R] (r : R → R → Prop),
  RingQuot.instMul r =
    {
      mul := fun x x_1 =>
        match x with
        | { toQuot := a } =>
          match x_1 with
          | { toQuot := b } => { toQuot := Quot.map₂ (fun x1 x2 => x1 * x2) ⋯ ⋯ a b } }
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupNorm.instSemilatticeSup : {E : Type u_3} → [inst : AddGroup E] → SemilatticeSup (NonarchAddGroupNorm E)
-- Init.System.IO
IO.instReprTaskState : Repr IO.TaskState
-- Std.Data.DTreeMap.Internal.WF.Defs
/-- `inter` preserves well-formedness. Later shown to be subsumed by `.wf`.  -/
Std.DTreeMap.Internal.Impl.WF.inter : ∀ {α : Type u} [inst : Ord α] {x : α → Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α x} {h : t₁.Balanced},
  t₁.WF → (t₁.inter t₂ h).WF
-- Mathlib.FieldTheory.SeparableDegree
/-- A monic irreducible polynomial over a field `F` of exponential characteristic `q` has
separable degree one if and only if it is of the form `X ^ (q ^ n) - C y`
for some `n : ℕ` and `y : F`.  -/
Irreducible.natSepDegree_eq_one_iff_of_monic : ∀ {F : Type u} [inst : Field F] {f : Polynomial F} (q : ℕ) [ExpChar F q],
  f.Monic → Irreducible f → (f.natSepDegree = 1 ↔ ∃ n y, f = Polynomial.X ^ q ^ n - Polynomial.C y)
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- **Alias** of `LinearMap.IsSymm.eq_iff`. -/
LinearMap.IsSymm.ortho_comm : ∀ {R : Type u_1} {M : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {I : R →+* R}
  {B : M →ₛₗ[I] M →ₗ[R] R}, B.IsSymm → ∀ {x y : M}, (B x) y = 0 ↔ (B y) x = 0
-- Mathlib.Order.Concept
Concept.instInfSet : {α : Type u_2} → {β : Type u_3} → {r : α → β → Prop} → InfSet (Concept α β r)
-- Mathlib.Algebra.Algebra.Unitization
Unitization.inl_sub : ∀ {R : Type u_3} (A : Type u_4) [inst : AddGroup R] [inst_1 : AddGroup A] (r₁ r₂ : R),
  Unitization.inl (r₁ - r₂) = Unitization.inl r₁ - Unitization.inl r₂
-- Mathlib.Data.Fin.VecNotation
Matrix.empty_vecAlt0 : ∀ (α : Type u_1) {h : 0 = 0 + 0}, Matrix.vecAlt0 h ![] = ![]
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.SimpleFunc.negPart_map_norm : ∀ {α : Type u_1} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α ℝ),
  MeasureTheory.SimpleFunc.map norm f.negPart = f.negPart
-- Batteries.Recycling.RBTree.Basic
/-- `O(log n)`. Returns the entry `a` such that `a ≤ k` for all keys in the RBSet.  -/
RBTree.RBSet.min? : {α : Type u_1} → {cmp : α → α → Ordering} → RBTree.RBSet α cmp → Option α
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
/-- Functor translating a functor into the category of monoid objects
to a monoid object in the functor category
 -/
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          CategoryTheory.Functor (CategoryTheory.Functor C (CategoryTheory.Mon D))
            (CategoryTheory.Mon (CategoryTheory.Functor C D))
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
/-- Use `head_darts_eq_firstDart` to rewrite in the reverse direction.  -/
SimpleGraph.Walk.firstDart_eq_head_darts : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hnil : ¬p.Nil), p.firstDart hnil = p.darts.head ⋯
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.ofSign_disjoint : ∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α], Disjoint (Equiv.Perm.ofSign 1) (Equiv.Perm.ofSign (-1))
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_of_mem_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k a : α}
  {v : β k}, a ∈ t.insertIfNew k v → cmp k a ≠ Ordering.eq → a ∈ t