mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Message
Lean.MessageData.tagged.inj : ∀ {a : Lean.Name} {a_1 : Lean.MessageData} {a_2 : Lean.Name} {a_3 : Lean.MessageData},
  Lean.MessageData.tagged a a_1 = Lean.MessageData.tagged a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
Finsupp.DegLex.isStrictOrder : ∀ {α : Type u_1} [inst : LinearOrder α], IsStrictOrder (DegLex (α →₀ ℕ)) fun x1 x2 => x1 < x2
-- Mathlib.LinearAlgebra.TensorProduct.Decomposition
DirectSum.subtype_rTensor_injective : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (ℳ : ι → Submodule R M) (N : Type u_5) [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : DecidableEq ι]
  [DirectSum.Decomposition ℳ] (i : ι), Function.Injective ⇑(LinearMap.rTensor N (ℳ i).subtype)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.MVarErrorKind.implicitArg.inj : ∀ {lctx : Lean.LocalContext} {ctx : Lean.Expr} {lctx_1 : Lean.LocalContext} {ctx_1 : Lean.Expr},
  Lean.Elab.Term.MVarErrorKind.implicitArg lctx ctx = Lean.Elab.Term.MVarErrorKind.implicitArg lctx_1 ctx_1 →
    lctx = lctx_1 ∧ ctx = ctx_1
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α} {fallback : β k}, (m₁ \ m₂).getD k fallback = if k ∈ m₂ then fallback else m₁.getD k fallback
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
/-- Product of two integral algebras is an integral algebra.  -/
Algebra.IsIntegral.prod : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_5} {B : Type u_6} [inst_1 : Ring A] [inst_2 : Algebra R A]
  [inst_3 : Ring B] [inst_4 : Algebra R B] [Algebra.IsIntegral R A] [Algebra.IsIntegral R B],
  Algebra.IsIntegral R (A × B)
-- Init.MetaTypes
/-- When `contextual` is true (default: `false`) and simplification encounters an implication `p → q`
it includes `p` as an additional simp lemma when simplifying `q`.
 -/
Lean.Meta.Simp.Config.contextual : Lean.Meta.Simp.Config → Bool
-- Init.Data.SInt.Lemmas
Int64.ofIntLE_int16ToInt : ∀ (x : Int16), Int64.ofIntLE x.toInt ⋯ ⋯ = x.toInt64
-- Mathlib.Data.Stream.Defs
/-- Elements of a stream with even indices.  -/
Stream'.even : {α : Type u} → Stream' α → Stream' α
-- Init.Data.Nat.Bitwise.Lemmas
Nat.instCommutativeHXor : Std.Commutative fun x1 x2 => x1 ^^^ x2
-- Init.MetaTypes
/-- Typecheck the elaborated term before reducing. Default: `true`.  -/
Lean.Meta.Command.ReduceConfig.check : Lean.Meta.Command.ReduceConfig → Bool
-- Mathlib.Analysis.InnerProductSpace.PiL2
Matrix.toEuclideanLin_apply : ∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {m : Type u_7} {n : Type u_8} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (M : Matrix m n 𝕜) (v : EuclideanSpace 𝕜 n), (Matrix.toEuclideanLin M) v = WithLp.toLp 2 (M.mulVec v.ofLp)
-- Mathlib.Analysis.Calculus.Deriv.Add
deriv_sub : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f g : 𝕜 → F} {x : 𝕜},
  DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 g x → deriv (f - g) x = deriv f x - deriv g x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_alter_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] [Inhabited α]
  {k fallback : α} {f : Option (β k) → Option (β k)},
  (m.alter k f).getKeyD k fallback = if (f (m.get? k)).isSome = true then k else fallback
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.mem_bot : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {x : A}, x ∈ ⊥ ↔ x = 0
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
/-- The functor `CostructuredArrow.pre` induces a natural transformation
`CostructuredArrow.functor (S ⋙ T) ⟶ CostructuredArrow.functor T` for `S : C ⥤ D` and
`T : D ⥤ E`.  -/
CategoryTheory.CostructuredArrow.preFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {E : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} E] →
        {D : Type u₁} →
          [inst_2 : CategoryTheory.Category.{v₁, u₁} D] →
            (S : CategoryTheory.Functor C D) →
              (T : CategoryTheory.Functor D E) →
                CategoryTheory.CostructuredArrow.functor (S.comp T) ⟶ CategoryTheory.CostructuredArrow.functor T
-- Lean.Setup
Lean.instToJsonModuleSetup : Lean.ToJson Lean.ModuleSetup
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
/-- The Bochner integral  -/
MeasureTheory.«term∫_,_∂_» : Lean.ParserDescr
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitSource.existsProp.injEq : ∀ (e e_1 : Lean.Expr),
  (Lean.Meta.Grind.SplitSource.existsProp e = Lean.Meta.Grind.SplitSource.existsProp e_1) = (e = e_1)
-- Init.Data.SInt.Bitwise
instAssociativeISizeHXor : Std.Associative fun x1 x2 => x1 ^^^ x2
-- Init.Data.UInt.Lemmas
UInt8.toUInt64_ofFin : ∀ {n : Fin UInt8.size}, (UInt8.ofFin n).toUInt64 = UInt64.ofNatLT ↑n ⋯
-- Init.Omega.IntList
/-- Get the `i`-th element (interpreted as `0` if the list is not long enough).  -/
Lean.Omega.IntList.get : Lean.Omega.IntList → ℕ → ℤ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbolAux.mk.injEq : ∀ {Self : Type} (name : String) (detail? : Option String) (kind : Lean.Lsp.SymbolKind)
  (range selectionRange : Lean.Lsp.Range) (children? : Option (Array Self)) (name_1 : String)
  (detail?_1 : Option String) (kind_1 : Lean.Lsp.SymbolKind) (range_1 selectionRange_1 : Lean.Lsp.Range)
  (children?_1 : Option (Array Self)),
  ({ name := name, detail? := detail?, kind := kind, range := range, selectionRange := selectionRange,
        children? := children? } =
      { name := name_1, detail? := detail?_1, kind := kind_1, range := range_1, selectionRange := selectionRange_1,
        children? := children?_1 }) =
    (name = name_1 ∧
      detail? = detail?_1 ∧
        kind = kind_1 ∧ range = range_1 ∧ selectionRange = selectionRange_1 ∧ children? = children?_1)
-- Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
/-- If `a : ℂ` has norm one, then the circle average `circleAverage (log ‖· - a‖) 0 1` vanishes.
 -/
circleAverage_log_norm_sub_const₁ : ∀ {a : ℂ}, ‖a‖ = 1 → Real.circleAverage (fun x => Real.log ‖x - a‖) 0 1 = 0
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves colimits of `K.op : Jᵒᵖ ⥤ Cᵒᵖ`, then `F.unop : C ⥤ D` preserves
limits of `K : J ⥤ C`.  -/
CategoryTheory.Limits.preservesLimit_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C)
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesColimit K.op F],
  CategoryTheory.Limits.PreservesLimit K F.unop
-- Init.GrindInstances.ToInt
Lean.Grind.instToIntInt64SintOfNatNat : Lean.Grind.ToInt Int64 (Lean.Grind.IntInterval.sint 64)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.toBoundedContinuousFunctionCLM_injective : ∀ (𝕜 : Type u_2) (E : Type u_5) (F : Type u_6) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : RCLike 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F], Function.Injective ⇑(SchwartzMap.toBoundedContinuousFunctionCLM 𝕜 E F)
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.Nonsingular.eq_1 : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R]
  (A : Matrix n n R), A.Nonsingular = ∀ (a b : R), A.IsDetpBalanced a b → a = b
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.node.formatter : Lean.SyntaxNodeKind → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- For `x : mixedSpace K`, the set `signSet x` is the set of real places `w` s.t. `x w ≤ 0`.  -/
NumberField.mixedEmbedding.signSet : {K : Type u_1} → [inst : Field K] → NumberField.mixedEmbedding.mixedSpace K → Set { w // w.IsReal }
-- Mathlib.Geometry.Manifold.Notation
Manifold.Elab.instInhabitedFindModelResult : Inhabited Manifold.Elab.FindModelResult
-- Mathlib.CategoryTheory.Action.Monoidal
Action.diagonalSuccIsoTensorTrivial.eq_def : ∀ (G : Type u) [inst : Group G] (x : ℕ),
  Action.diagonalSuccIsoTensorTrivial G x =
    match x with
    | 0 =>
      Action.diagonalOneIsoLeftRegular G ≪≫
        (CategoryTheory.MonoidalCategoryStruct.rightUnitor (Action.leftRegular G)).symm ≪≫
          CategoryTheory.MonoidalCategory.tensorIso (CategoryTheory.Iso.refl (Action.leftRegular G))
            (Action.tensorUnitIso (Equiv.ofUnique PUnit.{u + 1} (Fin 0 → G)).toIso)
    | n.succ =>
      Action.diagonalSuccIsoTensorDiagonal G (n + 1) ≪≫
        CategoryTheory.MonoidalCategory.tensorIso (CategoryTheory.Iso.refl (Action.leftRegular G))
            (Action.diagonalSuccIsoTensorTrivial G n) ≪≫
          Action.leftRegularTensorIso G
              (CategoryTheory.MonoidalCategoryStruct.tensorObj (Action.leftRegular G) (Action.trivial G (Fin n → G))) ≪≫
            CategoryTheory.MonoidalCategory.tensorIso (CategoryTheory.Iso.refl (Action.leftRegular G))
              (Action.mkIso (Fin.insertNthEquiv (fun x => G) 0).toIso ⋯)
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.comapₗ_const : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {S : Type u} [inst_3 : CommRing S]
  {N : Type u} [inst_4 : AddCommGroup N] [inst_5 : Module S N] {σ : R →+* S} (f : M →ₛₗ[σ] N)
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top S))
  (hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier) (a : M) (b : R) (hb : U ≤ PrimeSpectrum.basicOpen b),
  (AlgebraicGeometry.StructureSheaf.comapₗ f U V hUV) (AlgebraicGeometry.StructureSheaf.const a b U hb) =
    AlgebraicGeometry.StructureSheaf.const (f a) (σ b) V ⋯
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.not_mem_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → k ∉ t₁ ∩ t₂
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.reinsertAux.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (data : Array (Std.DHashMap.Internal.AssocList α β)) →
      (motive : { u // u.toNat < data.size } → Sort u_3) →
        (x : { u // u.toNat < data.size }) → ((i : USize) → (h : i.toNat < data.size) → motive ⟨i, h⟩) → motive x
-- Mathlib.Data.Matrix.Block
Matrix.blockDiag'_diagonal : ∀ {o : Type u_4} {m' : o → Type u_7} {α : Type u_12} [inst : Zero α] [inst_1 : DecidableEq o]
  [inst_2 : (i : o) → DecidableEq (m' i)] (d : (i : o) × m' i → α) (k : o),
  (Matrix.diagonal d).blockDiag' k = Matrix.diagonal fun i => d ⟨k, i⟩
-- Mathlib.Analysis.Complex.Basic
RCLike.isUniformEmbedding_ofReal : ∀ {𝕜 : Type u_2} [inst : RCLike 𝕜], IsUniformEmbedding RCLike.ofReal
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.Orthogonal.jd_transform : ∀ (l : Type u_4) (R : Type u₂) [inst : DecidableEq l] [inst_1 : CommRing R] [inst_2 : Fintype l],
  (LieAlgebra.Orthogonal.PD l R).transpose * LieAlgebra.Orthogonal.JD l R * LieAlgebra.Orthogonal.PD l R =
    2 • LieAlgebra.Orthogonal.S l R
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.negAddCancel.sizeOf_spec : sizeOf FirstOrder.Field.FieldAxiom.negAddCancel = 1
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α},
  List.Pairwise (fun a b => (a == b) = false) l → (Std.ExtHashMap.unitOfList l).size = l.length
-- Mathlib.CategoryTheory.Functor.TwoSquare
CategoryTheory.TwoSquare.vComp_app : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} {C₇ : Type u₇} {C₈ : Type u₈}
  [inst_4 : CategoryTheory.Category.{v₇, u₇} C₇] [inst_5 : CategoryTheory.Category.{v₈, u₈} C₈]
  {L' : CategoryTheory.Functor C₃ C₇} {R'' : CategoryTheory.Functor C₄ C₈} {B'' : CategoryTheory.Functor C₇ C₈}
  (w : CategoryTheory.TwoSquare T L R B) (w' : CategoryTheory.TwoSquare B L' R'' B'') (X : C₁),
  (w.vComp w').app X = CategoryTheory.CategoryStruct.comp (R''.map (w.natTrans.app X)) (w'.natTrans.app (L.obj X))
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {fallback : β}, k ∉ t₁ → (t₁ ∩ t₂).getD k fallback = fallback
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp.normNoninc_explicitCokernelπ : ∀ {X Y : SemiNormedGrp} (f : X ⟶ Y), (SemiNormedGrp.Hom.hom (SemiNormedGrp.explicitCokernelπ f)).NormNoninc
-- Init.Data.Option.Lemmas
Option.min_eq_left : ∀ {α : Type u_1} [inst : LE α] [inst_1 : Min α],
  (∀ (x y : α), x ≤ y → x ⊓ y = x) → ∀ {a b : Option α}, a ≤ b → a ⊓ b = a
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.preEquivalenceFunctor_map_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G)
  {X Y : CategoryTheory.StructuredArrow f (CategoryTheory.StructuredArrow.pre e F G)} (φ : X ⟶ Y),
  ((CategoryTheory.StructuredArrow.preEquivalenceFunctor F f).map φ).right =
    CategoryTheory.StructuredArrow.Hom.right (CategoryTheory.StructuredArrow.Hom.right φ)
-- Mathlib.Algebra.Homology.HomotopyCategory
HomotopyCategory.instAdditiveHomologyFunctor : ∀ {ι : Type u_2} (V : Type u) [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  (c : ComplexShape ι) [inst_2 : CategoryTheory.CategoryWithHomology V] (i : ι),
  (HomotopyCategory.homologyFunctor V c i).Additive
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.quotient.eq_1 : ∀ {G : Type u} (X : Type v) [inst : AddGroup G] [inst_1 : AddMonoid X] [inst_2 : AddAction X G] (H : AddSubgroup G)
  [inst_3 : AddAction.QuotientAction X H],
  AddAction.quotient X H = { vadd := fun b => Quotient.map' (fun x => b +ᵥ x) ⋯, add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.Order.SuccPred.Limit
/-- **Alias** of the reverse direction of `Order.isSuccPrelimit_toDual_iff`. -/
Order.IsPredPrelimit.dual : ∀ {α : Type u_1} {a : α} [inst : LT α], Order.IsPredPrelimit a → Order.IsSuccPrelimit (OrderDual.toDual a)
-- Mathlib.Data.Num.Basic
PosNum.instMul : Mul PosNum
-- Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
MvPowerSeries.monomial_mem_nonzeroDivisorsRight : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {n : σ →₀ ℕ} {r : R},
  (MvPowerSeries.monomial n) r ∈ nonZeroDivisorsRight (MvPowerSeries σ R) ↔ r ∈ nonZeroDivisorsRight R
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
SimpleGraph.IsEdgeConnected.of_subsingleton : ∀ {V : Type u_1} {G : SimpleGraph V} {k : ℕ} [Subsingleton V], G.IsEdgeConnected k
-- Mathlib.Topology.Category.FinTopCat
/-- The forgetful functor to `TopCat`.  -/
FinTopCat.instHasForget₂ContinuousMapCarrierToTopTopCat : CategoryTheory.HasForget₂ FinTopCat TopCat
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ι_g'_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) {Z : C} (h_1 : S.X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.ι (CategoryTheory.CategoryStruct.comp h.g' h_1) =
    CategoryTheory.CategoryStruct.comp 0 h_1
-- Mathlib.Topology.Covering.Basic
IsEvenlyCovered.comp_subtypeVal : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} (s : Set X)
  {I : Type u_3} [inst_2 : TopologicalSpace I],
  IsOpen s → IsOpen (f ⁻¹' s) → ∀ {x : X}, x ∈ s → IsEvenlyCovered (fun e => f ↑e) x I → IsEvenlyCovered f x I
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.isProbabilityMeasure : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : ι → Type u_10}
  {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i},
  ProbabilityTheory.iIndepFun f μ → MeasureTheory.IsProbabilityMeasure μ
-- Mathlib.Topology.PreorderRestrict
Preorder.continuous_frestrictLe : ∀ {α : Type u_1} [inst : Preorder α] {X : α → Type u_2} [inst_1 : (i : α) → TopologicalSpace (X i)]
  [inst_2 : LocallyFiniteOrderBot α] (a : α), Continuous (Preorder.frestrictLe a)
-- Mathlib.Topology.UniformSpace.Matrix
Matrix.instUniformSpace : (m : Type u_1) → (n : Type u_2) → (𝕜 : Type u_3) → [UniformSpace 𝕜] → UniformSpace (Matrix m n 𝕜)
-- Mathlib.Condensed.Light.Basic
LightCondensed.comp_hom : ∀ {C : Type w} [inst : CategoryTheory.Category.{v, w} C] {X Y Z : LightCondensed C} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Mathlib.Combinatorics.Young.YoungDiagram
_private.Mathlib.Combinatorics.Young.YoungDiagram.0.YoungDiagram.cellsOfRowLens.match_1.eq_2 : ∀ (motive : List ℕ → Sort u_1) (w : ℕ) (ws : List ℕ) (h_1 : Unit → motive [])
  (h_2 : (w : ℕ) → (ws : List ℕ) → motive (w :: ws)),
  (match w :: ws with
    | [] => h_1 ()
    | w :: ws => h_2 w ws) =
    h_2 w ws
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.RefreshState.mk.injEq : ∀ (curr : Thunk ProofWidgets.Html) (idx : ℕ) (next : Task (Option Unit)) (curr_1 : Thunk ProofWidgets.Html) (idx_1 : ℕ)
  (next_1 : Task (Option Unit)),
  ({ curr := curr, idx := idx, next := next } = { curr := curr_1, idx := idx_1, next := next_1 }) =
    (curr = curr_1 ∧ idx = idx_1 ∧ next = next_1)
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalSubgroup.instLatticeOfSeparatelyContinuousMul.eq_1 : ∀ {G : Type u} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : SeparatelyContinuousMul G],
  OpenNormalSubgroup.instLatticeOfSeparatelyContinuousMul =
    { toSemilatticeSup := OpenNormalSubgroup.instSemilatticeSupOpenNormalSubgroup, inf := SemilatticeInf.inf,
      inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }
-- Mathlib.Algebra.Ring.Invertible
AddUnits.neg_mulLeft : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] {x : AddUnits R} {y : R}, -x.mulLeft y = (-x).mulLeft y
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_mono_subtype : ∀ {α : Type u_1} (f : α → ENNReal) {s t : Set α}, s ⊆ t → ∑' (x : ↑s), f ↑x ≤ ∑' (x : ↑t), f ↑x
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.leftRelDecidable.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) [inst_1 : DecidablePred fun x => x ∈ s] (x y : α),
  QuotientAddGroup.leftRelDecidable s x y = ⋯.mpr (inst_1 (-x + y))
-- Mathlib.Topology.Category.TopCommRingCat
TopCommRingCat.coe_of : ∀ (X : Type u) [inst : CommRing X] [inst_1 : TopologicalSpace X] [inst_2 : IsTopologicalRing X],
  (TopCommRingCat.of X).α = X
-- Mathlib.CategoryTheory.Dialectica.Basic
CategoryTheory.Dial.comp_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {x x_1 x_2 : CategoryTheory.Dial C} (F : x.Hom x_1) (G : x_1.Hom x_2),
  (CategoryTheory.CategoryStruct.comp F G).f = CategoryTheory.CategoryStruct.comp F.f G.f
-- Mathlib.Topology.Order.Basic
/-- The topology induced by a strictly monotone function with order-connected range is the preorder
topology.  -/
StrictMono.induced_topology_eq_preorder : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : LinearOrder β] [t : TopologicalSpace β]
  [OrderTopology β] {f : α → β},
  StrictMono f → (Set.range f).OrdConnected → TopologicalSpace.induced f t = Preorder.topology α
-- Init.Control.StateCps
/-- Runs an action from the underlying monad in the monad with state. The state is not modified.

This function is typically implicitly accessed via a `MonadLiftT` instance as part of [automatic
lifting](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=monad-lifting).
 -/
StateCpsT.lift : {α σ : Type u} → {m : Type u → Type v} → [Monad m] → m α → StateCpsT σ m α
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.ext : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {f g : MeasureTheory.SimpleFunc α β},
  (∀ (a : α), f a = g a) → f = g
-- Mathlib.Order.Minimal
maximal_mem_image_monotone_iff : ∀ {α : Type u_2} {β : Type u_3} {a : α} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {f : α → β},
  a ∈ s →
    (∀ ⦃y x : α⦄, y ∈ s → x ∈ s → (f y ≤ f x ↔ y ≤ x)) →
      (Maximal (fun x => x ∈ f '' s) (f a) ↔ Maximal (fun x => x ∈ s) a)
-- Init.Data.List.Perm
List.concat_perm : ∀ {α : Type u_1} (l : List α) (a : α), (l.concat a).Perm (a :: l)
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
/-- The complex exponential is everywhere differentiable, with the derivative `exp x`.  -/
Complex.hasDerivAt_exp : ∀ (x : ℂ), HasDerivAt Complex.exp (Complex.exp x) x
-- Mathlib.Data.PFunctor.Univariate.M
/-- `Path F` provides indices to access internal nodes in `Corec F`  -/
PFunctor.Approx.Path : PFunctor.{uA, uB} → Type (max uA uB)
-- Mathlib.Analysis.Convex.Side
AffineSubspace.sSameSide_smul_vsub_vadd_right : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x p₁ p₂ : P},
  x ∉ s → p₁ ∈ s → p₂ ∈ s → ∀ {t : R}, 0 < t → s.SSameSide x (t • (x -ᵥ p₁) +ᵥ p₂)
-- Mathlib.Algebra.GroupWithZero.Opposite
MulOpposite.isRightCancelMulZero_iff : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α], IsRightCancelMulZero αᵐᵒᵖ ↔ IsLeftCancelMulZero α
-- Init.Data.String.PosRaw
String.Pos.Raw.dec_lt : ∀ {p : String.Pos.Raw}, p ≠ 0 → p.dec < p
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.comp_counit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} {H : CategoryTheory.Functor D E} {I : CategoryTheory.Functor E D} (adj₁ : F ⊣ G)
  (adj₂ : H ⊣ I) (X : E),
  (adj₁.comp adj₂).counit.app X =
    CategoryTheory.CategoryStruct.comp (H.map (adj₁.counit.app (I.obj X))) (adj₂.counit.app X)
-- Mathlib.Topology.Constructions
isOpenMap_toMul : ∀ {X : Type u} [inst : TopologicalSpace X], IsOpenMap ⇑Additive.toMul
-- Mathlib.Topology.Algebra.FilterBasis
AddGroupFilterBasis.add : ∀ {G : Type u} [inst : AddGroup G] {B : AddGroupFilterBasis G} {U : Set G}, U ∈ B → ∃ V ∈ B, V + V ⊆ U
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey?_erase_eq_iff_not_compare_eq_maxKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k).maxKey? = t.maxKey? ↔ ∀ {km : α}, t.maxKey? = some km → ¬cmp k km = Ordering.eq
-- Mathlib.RingTheory.DividedPowers.Basic
DividedPowers.dpow_mem : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (self : DividedPowers I) {n : ℕ} {x : A},
  n ≠ 0 → x ∈ I → self.dpow n x ∈ I