mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Independence.Integration
/-- A continuous bilinear map applied to two independent and integrable random variables
is integrable.  -/
ProbabilityTheory.IndepFun.integrable_bilin : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_5} {F : Type u_6} {G : Type u_7}
  {𝕜 : Type u_8} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : MeasurableSpace E] [OpensMeasurableSpace E] [inst_5 : SeminormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F]
  [inst_7 : MeasurableSpace F] [OpensMeasurableSpace F] [inst_9 : SeminormedAddCommGroup G] [inst_10 : NormedSpace 𝕜 G]
  {X : Ω → E} {Y : Ω → F},
  ProbabilityTheory.IndepFun X Y μ →
    MeasureTheory.Integrable X μ →
      MeasureTheory.Integrable Y μ → ∀ (B : E →L[𝕜] F →L[𝕜] G), MeasureTheory.Integrable (fun ω => (B (X ω)) (Y ω)) μ
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Initial.hasLimit_comp_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E}, CategoryTheory.Limits.HasLimit (F.comp G) ↔ CategoryTheory.Limits.HasLimit G
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.removeNegAssignment.eq_1 : Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos.removeNegAssignment = Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos
-- Mathlib.Algebra.Group.Submonoid.Saturation
Submonoid.saturation_top : ∀ {M : Type u_1} [inst : MulOneClass M], ⊤.saturation = ⊤
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- Every cokernel of `f` induces a cokernel of `g ≫ f` if `g` is epi.  -/
CategoryTheory.Limits.isCokernelEpiComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          {c : CategoryTheory.Limits.CokernelCofork f} →
            CategoryTheory.Limits.IsColimit c →
              {W : C} →
                (g : W ⟶ X) →
                  [hg : CategoryTheory.Epi g] →
                    {h : W ⟶ Y} →
                      (hh : h = CategoryTheory.CategoryStruct.comp g f) →
                        CategoryTheory.Limits.IsColimit
                          (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.Cofork.π c) ⋯)
-- Mathlib.Algebra.Module.SpanRank
/-- Constructs a generating finset with cardinality equal to the `spanFinrank` of the submodule
when the submodule is finitely generated.  -/
Submodule.FG.exists_span_finset_card_eq_spanFinrank : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {p : Submodule R M},
  p.FG → ∃ s, s.card = p.spanFinrank ∧ Submodule.span R ↑s = p
-- Mathlib.Algebra.Group.Subgroup.Pointwise
vadd_coe_set : ∀ {G : Type u_2} {S : Type u_4} [inst : AddGroup G] [inst_1 : SetLike S G] [AddSubgroupClass S G] {s : S} {a : G},
  a ∈ s → a +ᵥ ↑s = ↑s
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
/-- The bicategory instance.  -/
Mathlib.Tactic.Bicategory.Context.instBicategory : (self : Mathlib.Tactic.Bicategory.Context) → Q(CategoryTheory.Bicategory unknown_1)
-- Init.Data.Dyadic.Basic
Dyadic.toDyadic_toRat : ∀ (x : Dyadic) (prec : ℤ), x.toRat.toDyadic prec = x.roundDown prec
-- Mathlib.Order.KrullDimension
Order.height_mono : ∀ {α : Type u_1} [inst : Preorder α], Monotone Order.height
-- Batteries.Data.Fin.Coding
Fin.decodeSum_encodeSum : ∀ {n m : ℕ} (x : Fin n ⊕ Fin m), Fin.decodeSum (Fin.encodeSum x) = x
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.faceOpposite.congr_simp : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s s_1 : Affine.Simplex k P n),
  s = s_1 → ∀ (i i_1 : Fin (n + 1)), i = i_1 → s.faceOpposite i = s_1.faceOpposite i_1
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.uniqueLinearEquiv.eq_1 : ∀ (R : Type u_1) {S : Type u_2} (M : Type u_3) [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  [inst_3 : One M] [inst_4 : Subsingleton M],
  MonoidAlgebra.uniqueLinearEquiv R M =
    { toFun := (MonoidAlgebra.coeffAddEquiv.trans (Finsupp.uniqueAddEquiv 1)).toFun, map_add' := ⋯, map_smul' := ⋯,
      invFun := (MonoidAlgebra.coeffAddEquiv.trans (Finsupp.uniqueAddEquiv 1)).invFun, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.LineGraph
SimpleGraph.Copy.lineGraph.eq_1 : ∀ {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G.Copy G'),
  f.lineGraph = f.toLineGraphEmbedding.toCopy
-- Lean.Meta.InferType
/-- `isArrowProposition type n` is an "approximate" predicate which returns `LBool.true`
if `type` is of the form `A_1 → ... → A_n → B`, where `B` is a proposition.

Remark: `type` can be a dependent arrow.
 -/
_private.Lean.Meta.InferType.0.Lean.Meta.isArrowProposition : Lean.Expr → ℕ → Lean.MetaM Lean.LBool
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.instInhabitedLeapSecond.default : Std.Time.TimeZone.TZif.LeapSecond
-- Mathlib.Topology.Defs.Sequences
FrechetUrysohnSpace.mk : ∀ {X : Type u_1} [inst : TopologicalSpace X], (∀ (s : Set X), closure s ⊆ seqClosure s) → FrechetUrysohnSpace X
-- Mathlib.Combinatorics.Quiver.Path.Vertices
/-- Split a path at the *last* occurrence of a vertex.  -/
Quiver.Path.exists_eq_comp_and_notMem_tail_of_mem_vertices : ∀ {V : Type u_1} [inst : Quiver V] {a b : V} (p : Quiver.Path a b) {v : V},
  v ∈ p.vertices → ∃ p₁ p₂, p = p₁.comp p₂ ∧ v ∉ p₂.vertices.tail
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.map_ratCast : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K) (x : ℚ), v ↑x = ‖x‖
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
/-- If `0 < n`, then `r i` has order `n / gcd n i`.
 -/
DihedralGroup.orderOf_r : ∀ {n : ℕ} [NeZero n] (i : ZMod n), orderOf (DihedralGroup.r i) = n / n.gcd i.val
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.cancelBaseChange_self_eq_lid : ∀ (R : Type uR) (A : Type uA) {N : Type uN} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N],
  TensorProduct.AlgebraTensorModule.cancelBaseChange R A A A N = TensorProduct.lid A (TensorProduct R A N)
-- Mathlib.Analysis.Normed.MulAction
NormSMulClass.toIsBoundedSMul : ∀ {α : Type u_1} {β : Type u_2} [inst : SeminormedRing α] [inst_1 : SeminormedAddCommGroup β] [inst_2 : Module α β]
  [NormSMulClass α β], IsBoundedSMul α β
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The scalar multiplication of `C^n` function within a set at a point and a constant and is `C^n`
within this set at this point.  -/
ContDiffWithinAt.smul_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {A : Type u_4} [inst_5 : NormedRing A] [inst_6 : NormedAlgebra 𝕜 A] [inst_7 : Module A F] [IsScalarTower 𝕜 A F]
  [IsBoundedSMul A F] {s : Set E} {f : E → A} {x : E},
  ContDiffWithinAt 𝕜 n f s x → ∀ (v : F), ContDiffWithinAt 𝕜 n (fun y => f y • v) s x
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.monthPairs : Vector String 12 → Array (String × Std.Time.Month.Ordinal)
-- Mathlib.Topology.Category.Profinite.AsLimit
/-- The isomorphism between `X` and the explicit limit of `X.diagram`,
induced by lifting `X.asLimitCone`.
 -/
Profinite.isoAsLimitConeLift : (X : Profinite) → X ≅ (Profinite.limitCone X.diagram).pt
-- Mathlib.NumberTheory.NumberField.House
/-- `c₁ K` is the product of `finrank ℚ K` and  `c₂ K` and depends on `K`.  -/
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.c₁ : (K : Type u_1) → [inst : Field K] → [NumberField K] → [DecidableEq (K →+* ℂ)] → ℝ
-- Mathlib.Topology.CWComplex.Classical.Subcomplex
/-- **Alias** of `Topology.RelCWComplex.Subcomplex.cellFrontier_subset_of_mem`. -/
Topology.CWComplex.Subcomplex.cellFrontier_subset_of_mem : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [inst : Topology.RelCWComplex C D]
  (E : Topology.RelCWComplex.Subcomplex C) {n : ℕ} {i : Topology.RelCWComplex.cell C n},
  i ∈ E.I n → Topology.RelCWComplex.cellFrontier n i ⊆ ↑E
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_filter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Bool} {k : α} (h : m.WF),
  Std.DHashMap.Raw.Const.get? (Std.DHashMap.Raw.filter f m) k =
    (Std.DHashMap.Raw.Const.get? m k).pfilter fun x h' => f (m.getKey k ⋯) x
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.instHasFrameAndPureAnd : ∀ {φ ψ : Prop} (σs : List (Type u_1)) (P Q : Std.Do.SPred σs) [Std.Do.SPred.Tactic.HasFrame P Q ψ],
  Std.Do.SPred.Tactic.HasFrame spred(⌜φ⌝ ∧ P) Q (φ ∧ ψ)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes left covariance.
The lemma assuming right covariance is `Right.one_le_mul`.  -/
Left.one_le_mul : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftMono α] {a b : α}, 1 ≤ a → 1 ≤ b → 1 ≤ a * b
-- Init.Data.String.Defs
ByteArray.isValidUTF8_empty : ByteArray.empty.IsValidUTF8
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsBasis.contract_indep_iff : ∀ {α : Type u_1} {M : Matroid α} {I J X : Set α},
  M.IsBasis I X → ((M.contract X).Indep J ↔ M.Indep (J ∪ I) ∧ Disjoint X J)
-- Mathlib.Analysis.Normed.Module.FiniteDimension
AffineMap.continuous_of_finiteDimensional : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type w} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace 𝕜]
  {PE : Type u_1} {PF : Type u_2} [inst_6 : MetricSpace PE] [inst_7 : NormedAddTorsor E PE] [inst_8 : MetricSpace PF]
  [inst_9 : NormedAddTorsor F PF] [FiniteDimensional 𝕜 E] (f : PE →ᵃ[𝕜] PF), Continuous ⇑f
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.zero_apply : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] (i : ι), 0 i = 0
-- Lean.Data.Lsp.Internal
/-- Whether the module is being imported via `import all`.  -/
Lean.Lsp.ImportInfo.isAll : Lean.Lsp.ImportInfo → Bool
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instAddCommSemigroup : {X : Type u_1} →
  {Y : Type u_2} → [inst : TopologicalSpace X] → [AddCommSemigroup Y] → AddCommSemigroup (LocallyConstant X Y)
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.ae_eq_set_symmDiff : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s t s' t' : Set α}, s =ᵐ[μ] t → s' =ᵐ[μ] t' → symmDiff s s' =ᵐ[μ] symmDiff t t'
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Alternative constructor for `IsColimit`,
providing a morphism of cocones rather than a morphism between the cocone points
and separately the factorisation condition.
 -/
CategoryTheory.Limits.IsColimit.mkCoconeMorphism : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cocone F} →
            (desc : (s : CategoryTheory.Limits.Cocone F) → t ⟶ s) →
              (∀ (s : CategoryTheory.Limits.Cocone F) (m : t ⟶ s), m = desc s) → CategoryTheory.Limits.IsColimit t
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.indicatorConst.congr_simp : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] (p : ENNReal)
  {μ : MeasureTheory.Measure α} {s s_1 : Set α} (e_s : s = s_1) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (c c_1 : E),
  c = c_1 → MeasureTheory.Lp.simpleFunc.indicatorConst p hs hμs c = MeasureTheory.Lp.simpleFunc.indicatorConst p ⋯ ⋯ c_1
-- Mathlib.Topology.MetricSpace.Basic
/-- One gets a metric space from an emetric space if the edistance
is everywhere finite, by pushing the edistance to reals. We set it up so that the edist and the
uniformity are defeq in the metric space and the emetric space. In this definition, the distance
is given separately, to be able to prescribe some expression which is not defeq to the push-forward
of the edistance to reals.  -/
EMetricSpace.toMetricSpaceOfDist : {α : Type u} →
  [inst : EMetricSpace α] →
    (dist : α → α → ℝ) →
      (∀ (x y : α), 0 ≤ dist x y) → (∀ (x y : α), edist x y = ENNReal.ofReal (dist x y)) → MetricSpace α
-- Mathlib.RingTheory.LocalRing.RingHom.Basic
isLocalHom_toRingHom : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] {F : Type u_4} [inst_2 : FunLike F R S]
  [inst_3 : RingHomClass F R S] (f : F) [IsLocalHom f], IsLocalHom ↑f
-- Mathlib.FieldTheory.Galois.Basic
MulSemiringAction.toAlgAut.congr_simp : ∀ (G : Type u_2) (R : Type u_3) (A : Type u_4) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Group G] [inst_4 : MulSemiringAction G A] [inst_5 : SMulCommClass G R A],
  MulSemiringAction.toAlgAut G R A = MulSemiringAction.toAlgAut G R A
-- Init.Data.Vector.Lemmas
Vector.foldl_hom : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} {n : ℕ} (f : α₁ → α₂) {g₁ : α₁ → β → α₁} {g₂ : α₂ → β → α₂}
  {xs : Vector β n} {init : α₁},
  (∀ (x : α₁) (y : β), g₂ (f x) y = f (g₁ x y)) → Vector.foldl g₂ (f init) xs = f (Vector.foldl g₁ init xs)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ReferenceParams.toTextDocumentPositionParams : Lean.Lsp.ReferenceParams → Lean.Lsp.TextDocumentPositionParams
-- Init.Data.Nat.Mod
Nat.mod_mul_left_mod : ∀ (a b c : ℕ), a % (b * c) % c = a % c
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.monic_prod_of_monic : ∀ {R : Type u} {ι : Type y} [inst : CommSemiring R] (s : Finset ι) (f : ι → Polynomial R),
  (∀ i ∈ s, (f i).Monic) → (∏ i ∈ s, f i).Monic
-- Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
le_rank_iff_exists_linearIndependent : ∀ {K : Type u} {V : Type v} [inst : Ring K] [StrongRankCondition K] [inst_2 : AddCommGroup V] [inst_3 : Module K V]
  [Module.Free K V] {c : Cardinal.{v}}, c ≤ Module.rank K V ↔ ∃ s, Cardinal.mk ↑s = c ∧ LinearIndepOn K id s
-- Mathlib.NumberTheory.Padics.PadicNorm
/-- The `p`-adic norm of `p` is less than `1` if `1 < p`.

See also `padicNorm.padicNorm_p_lt_one_of_prime` for a version assuming `p` is prime.  -/
padicNorm.padicNorm_p_lt_one : ∀ {p : ℕ}, 1 < p → padicNorm p ↑p < 1
-- Mathlib.Order.Interval.Finset.Basic
/-- **Alias** of the reverse direction of `Finset.Iio_eq_empty`. -/
IsMin.finsetIio_eq : ∀ {α : Type u_2} {a : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α], IsMin a → Finset.Iio a = ∅
-- Mathlib.RingTheory.WittVector.Defs
/-- The polynomials used for defining repeated addition of the ring of Witt vectors.  -/
WittVector.wittZSMul : (p : ℕ) → [hp : Fact (Nat.Prime p)] → ℤ → ℕ → MvPolynomial (Fin 1 × ℕ) ℤ
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point.0.WeierstrassCurve.Affine.Point.add_eq_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] (P Q : W.Point),
  P + Q = 0 ↔ P = -Q
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.π₁_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (T : CategoryTheory.Pretriangulated.Triangle C), CategoryTheory.Pretriangulated.Triangle.π₁.obj T = T.obj₁
-- Std.Sync.Channel
/-- Creates a `Selector` that resolves once `ch` has data available and provides that data.
 -/
Std.Channel.recvSelector : {α : Type} → [Inhabited α] → Std.Channel α → Std.Async.Selector α
-- Aesop.RuleTac.ElabRuleTerm
Aesop.runTacticMAsTermElabM : {α : Type} → Lean.MVarId → Lean.Elab.Tactic.TacticM α → Lean.Elab.TermElabM α
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
ThreeAPFree.mono : ∀ {α : Type u_2} [inst : AddMonoid α] {s t : Set α}, t ⊆ s → ThreeAPFree s → ThreeAPFree t
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
measure_closure_of_null_frontier : ∀ {α' : Type u_6} [inst : TopologicalSpace α'] [inst_1 : MeasurableSpace α'] {μ : MeasureTheory.Measure α'}
  {s : Set α'}, μ (frontier s) = 0 → μ (closure s) = μ s
-- Mathlib.RingTheory.Ideal.IsPrincipal
Ideal.associatesNonZeroDivisorsEquivIsPrincipal_apply : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (x : ↥(nonZeroDivisors R)),
  ↑↑((Ideal.associatesNonZeroDivisorsEquivIsPrincipal R) (Associates.mk x)) = Ideal.span {↑x}
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.sqLe_smul : ∀ {c d x y : ℕ} (n : ℕ), Zsqrtd.SqLe x c y d → Zsqrtd.SqLe (n * x) c (n * y) d
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.toCLM_injective : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} [inst : Fintype m] [inst_1 : NonUnitalCStarAlgebra A],
  Function.Injective ⇑CStarMatrix.toCLM
-- Mathlib.Algebra.Order.Group.Abs
mabs_eq_self : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] {a : G}, |a|ₘ = a ↔ 1 ≤ a
-- Mathlib.Algebra.Group.ULift
ULift.smul : {α : Type u} → {β : Type v} → [SMul β α] → SMul β (ULift.{u_1, u} α)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
/-- The composition of exponentiable morphisms is exponentiable.  -/
CategoryTheory.ExponentiableMorphism.comp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I J K : C} →
      (f : I ⟶ J) →
        (g : J ⟶ K) →
          [inst_1 : CategoryTheory.ChosenPullbacksAlong f] →
            [inst_2 : CategoryTheory.ChosenPullbacksAlong g] →
              [inst_3 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.comp f g)] →
                [CategoryTheory.ExponentiableMorphism f] →
                  [CategoryTheory.ExponentiableMorphism g] →
                    CategoryTheory.ExponentiableMorphism (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.instIsAddLeftInvariantCount : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd G],
  MeasureTheory.Measure.count.IsAddLeftInvariant
-- Mathlib.Topology.Maps.OpenQuotient
isEmbedding_of_isOpenQuotientMap_of_isInducing : ∀ {A : Type u_4} {B : Type u_5} {C : Type u_6} {D : Type u_7} [inst : TopologicalSpace A] [inst_1 : TopologicalSpace B]
  [inst_2 : TopologicalSpace C] [inst_3 : TopologicalSpace D] (f : A → B) (g : C → D) (p : A → C) (q : B → D),
  g ∘ p = q ∘ f →
    Topology.IsInducing f →
      Topology.IsQuotientMap p →
        IsOpenQuotientMap q → Function.Injective g → q ⁻¹' q '' Set.range f ⊆ Set.range f → Topology.IsEmbedding g
-- Mathlib.Tactic.TacticAnalysis
Mathlib.TacticAnalysis.instOrdEntry : Ord Mathlib.TacticAnalysis.Entry
-- Mathlib.Data.Sym.Sym2
Sym2.mem_iff : ∀ {α : Type u_1} {a b c : α}, a ∈ s(b, c) ↔ a = b ∨ a = c
-- Mathlib.Order.Closure
ClosureOperator.closure_min : ∀ {α : Type u_1} [inst : Preorder α] {c : ClosureOperator α} {x y : α}, x ≤ y → c.IsClosed y → c x ≤ y
-- Mathlib.Data.Finset.Basic
Finset.erase_insert : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Finset α}, a ∉ s → (insert a s).erase a = s
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.MorphismProperty.relative.property_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X Y : D} {P : CategoryTheory.MorphismProperty C} {f : X ⟶ Y}
  (hf : CategoryTheory.MorphismProperty.relative F P f) {a : C} (g : F.obj a ⟶ Y), P (⋯.snd g)
-- Mathlib.ModelTheory.Fraisse
/-- The age of a direct limit of structures is the union of the ages of the structures.  -/
FirstOrder.Language.age_directLimit : ∀ {L : FirstOrder.Language} {ι : Type w} [inst : Preorder ι] [inst_1 : IsDirectedOrder ι] [inst_2 : Nonempty ι]
  (G : ι → Type (max w w')) [inst_3 : (i : ι) → L.Structure (G i)] (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j))
  [inst_4 : DirectedSystem G fun i j h => ⇑(f i j h)], L.age (FirstOrder.Language.DirectLimit G f) = ⋃ i, L.age (G i)
-- Mathlib.Algebra.Star.StarProjection
IsStarProjection.mk : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Star R] {p : R}, IsIdempotentElem p → IsSelfAdjoint p → IsStarProjection p
-- Mathlib.Order.RelIso.Set
/-- Restrict the codomain of a relation embedding.  -/
RelEmbedding.codRestrict : {α : Type u_1} →
  {β : Type u_2} →
    {r : α → α → Prop} →
      {s : β → β → Prop} → (p : Set β) → (f : r ↪r s) → (∀ (a : α), f a ∈ p) → r ↪r Subrel s fun x => x ∈ p
-- Mathlib.CategoryTheory.Preadditive.OfBiproducts
CategoryTheory.SemiadditiveOfBinaryBiproducts.isUnital_rightAdd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] (X Y : C),
  EckmannHilton.IsUnital (fun x1 x2 => CategoryTheory.SemiadditiveOfBinaryBiproducts.rightAdd X Y x1 x2) 0
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.K'.elim_rev : ∀ (a b c d : List Turing.PartrecToTM2.Γ'), Turing.PartrecToTM2.K'.elim a b c d Turing.PartrecToTM2.K'.rev = b
-- Mathlib.CategoryTheory.Sites.CoverPreserving
CategoryTheory.CoverPreserving.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {G : CategoryTheory.Functor C D},
  (∀ {U : C} {S : CategoryTheory.Sieve U}, S ∈ J U → CategoryTheory.Sieve.functorPushforward G S ∈ K (G.obj U)) →
    CategoryTheory.CoverPreserving J K G
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.pointwiseLeftKanExtension_map : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [inst_3 : L.HasPointwiseLeftKanExtension F]
  {Y₁ Y₂ : D} (f : Y₁ ⟶ Y₂),
  (L.pointwiseLeftKanExtension F).map f =
    CategoryTheory.Limits.colimit.desc ((CategoryTheory.CostructuredArrow.proj L Y₁).comp F)
      { pt := CategoryTheory.Limits.colimit ((CategoryTheory.CostructuredArrow.proj L Y₂).comp F),
        ι :=
          {
            app := fun g =>
              CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.proj L Y₂).comp F)
                ((CategoryTheory.CostructuredArrow.map f).obj g),
            naturality := ⋯ } }
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast_append_of_containsKey_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l l' : List ((a : α) × β a)} {a : α}
  {h : Std.Internal.List.containsKey a (l ++ l') = true} (hl' : Std.Internal.List.containsKey a l' = false),
  Std.Internal.List.getValueCast a (l ++ l') h = Std.Internal.List.getValueCast a l ⋯
-- Init.Data.String.Lemmas.FindPos
String.le_posLT_iff : ∀ {s : String} {p : String.Pos.Raw} {h : 0 < p} {q : s.Pos}, q ≤ s.posLT p h ↔ q.offset < p
-- Mathlib.Algebra.Lie.Basis.Basic
/-- The Cartan matrix.  -/
LieAlgebra.Basis.A : {ι : Type u_1} →
  {R : Type u_2} →
    {L : Type u_3} →
      [inst : Finite ι] →
        [inst_1 : CommRing R] →
          [inst_2 : LieRing L] →
            [inst_3 : LieAlgebra R L] → {H : LieSubalgebra R L} → LieAlgebra.Basis ι H → Matrix ι ι ℤ
-- Mathlib.Topology.ContinuousMap.Polynomial
polynomialFunctions_coe : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : TopologicalSpace R] [inst_2 : IsTopologicalSemiring R] (X : Set R),
  ↑(polynomialFunctions X) = Set.range ⇑(Polynomial.toContinuousMapOnAlgHom X)