mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Action.Monoidal
Action.FunctorCategoryEquivalence.functor_η : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.MonoidalCategory V],
  CategoryTheory.Functor.OplaxMonoidal.η Action.FunctorCategoryEquivalence.functor =
    CategoryTheory.CategoryStruct.id
      (Action.FunctorCategoryEquivalence.functor.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action V G)))
-- Mathlib.Analysis.Normed.Group.Hom
/-- The identity as a continuous normed group hom.  -/
NormedAddGroupHom.id : (V : Type u_1) → [inst : SeminormedAddCommGroup V] → NormedAddGroupHom V V
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.IsFiltered.coeq₃_condition₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {j₁ j₂ : C}
  (f g h : j₁ ⟶ j₂),
  CategoryTheory.CategoryStruct.comp g (CategoryTheory.IsFiltered.coeq₃Hom f g h) =
    CategoryTheory.CategoryStruct.comp h (CategoryTheory.IsFiltered.coeq₃Hom f g h)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey?_erase_le_maxKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k km kme : α} (hkme : (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.maxKey? = some kme),
  t.maxKey?.get ⋯ = km → (compare kme km).isLE = true
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.isEmpty_diff_iff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (m₁ \ m₂).isEmpty = true ↔ ∀ k ∈ m₁, k ∈ m₂
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
RootPairing.Base.cartanMatrixIn_nondegenerate : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (S : Type u_5) [inst_5 : CommRing S]
  [inst_6 : Algebra S R] [IsDomain R] [NeZero 2] [FaithfulSMul S R] [IsDomain S] {P : RootPairing ι R M N}
  [P.IsRootSystem] [inst_12 : P.IsValuedIn S] [inst_13 : Fintype ι] [P.IsAnisotropic] (b : P.Base),
  (RootPairing.Base.cartanMatrixIn S b).Nondegenerate
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- Constructor for natural isomorphisms between functors from `V.HomotopyCategory`.  -/
SSet.Truncated.HomotopyCategory.mkNatIso : {V : SSet.Truncated 2} →
  {D : Type u_1} →
    [inst : CategoryTheory.Category.{v_1, u_1} D] →
      {F G : CategoryTheory.Functor V.HomotopyCategory D} →
        (iso :
            (x : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })) →
              F.obj (SSet.Truncated.HomotopyCategory.mk x) ≅ G.obj (SSet.Truncated.HomotopyCategory.mk x)) →
          autoParam
              (∀ ⦃x y : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })⦄
                (e : SSet.Truncated.Edge x y),
                CategoryTheory.CategoryStruct.comp (F.map (SSet.Truncated.HomotopyCategory.homMk e)) (iso y).hom =
                  CategoryTheory.CategoryStruct.comp (iso x).hom (G.map (SSet.Truncated.HomotopyCategory.homMk e)))
              _auto_148✝ →
            (F ≅ G)
-- Mathlib.RingTheory.MvPolynomial.Ideal
/-- The ideal spanned by all variables.  -/
MvPolynomial.idealOfVars : (σ : Type u_1) → (R : Type u_2) → [inst : CommSemiring R] → Ideal (MvPolynomial σ R)
-- Lean.Data.Lsp.Workspace
Lean.Lsp.FileChangeType : Type
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.le_def : ∀ {α : Type u_3} {a b : MeasurableSpace.DynkinSystem α}, a ≤ b ↔ a.Has ≤ b.Has
-- Mathlib.Algebra.Ring.Submonoid.Basic
/-- The product of an element of the additive closure of a multiplicative subsemigroup `M`
and an element of `M` is contained in the additive closure of `M`.  -/
MulMemClass.mul_right_mem_add_closure : ∀ {M : Type u_1} {R : Type u_2} [inst : NonUnitalNonAssocSemiring R] [inst_1 : SetLike M R] [MulMemClass M R] {S : M}
  {a b : R}, a ∈ AddSubmonoid.closure ↑S → b ∈ S → a * b ∈ AddSubmonoid.closure ↑S
-- Mathlib.CategoryTheory.FintypeCat
/-- The equivalence between `FintypeCat.Skeleton` and `FintypeCat`.  -/
FintypeCat.Skeleton.equivalence : FintypeCat.Skeleton ≌ FintypeCat
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
Finsupp.DegLex.instIsOrderedCancelAddMonoidDegLexNat : ∀ {α : Type u_1} [inst : LinearOrder α], IsOrderedCancelAddMonoid (DegLex (α →₀ ℕ))
-- Mathlib.Algebra.Ring.InjSurj
/-- Pullback a `Semiring` instance along an injective function.  -/
Function.Injective.semiring : {R : Type u_1} →
  {S : Type u_2} →
    (f : S → R) →
      Function.Injective f →
        [inst : Add S] →
          [inst_1 : Mul S] →
            [inst_2 : Zero S] →
              [inst_3 : One S] →
                [inst_4 : SMul ℕ S] →
                  [inst_5 : Pow S ℕ] →
                    [inst_6 : NatCast S] →
                      [inst_7 : Semiring R] →
                        f 0 = 0 →
                          f 1 = 1 →
                            (∀ (x y : S), f (x + y) = f x + f y) →
                              (∀ (x y : S), f (x * y) = f x * f y) →
                                (∀ (n : ℕ) (x : S), f (n • x) = n • f x) →
                                  (∀ (x : S) (n : ℕ), f (x ^ n) = f x ^ n) → (∀ (n : ℕ), f ↑n = ↑n) → Semiring S
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
List.aestronglyMeasurable_fun_sum : ∀ {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [inst : AddMonoid M]
  [inst_1 : TopologicalSpace M] [ContinuousAdd M] (l : List (α → M)),
  (∀ f ∈ l, MeasureTheory.AEStronglyMeasurable f μ) →
    MeasureTheory.AEStronglyMeasurable (fun x => (List.map (fun f => f x) l).sum) μ
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.Fin
/-- `Fin.last n` is a terminal object in `Fin (n + 1)`.  -/
Fin.isTerminalLast : (n : ℕ) → CategoryTheory.Limits.IsTerminal (Fin.last n)
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.instHasTerminal : CategoryTheory.Limits.HasTerminal SimplexCategory
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.affineCombination_mem_interior_face_iff_mem_Ioo : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : PartialOrder k] {n : ℕ} (s : Affine.Simplex k P n) {fs : Finset (Fin (n + 1))}
  {m : ℕ} (h : fs.card = m + 1) {w : Fin (n + 1) → k},
  ∑ i, w i = 1 →
    ((Finset.affineCombination k Finset.univ s.points) w ∈ (s.face h).interior ↔
      (∀ i ∈ fs, w i ∈ Set.Ioo 0 1) ∧ ∀ i ∉ fs, w i = 0)
-- Std.Data.Internal.List.Associative
Std.Internal.List.List.getValue_filter_containsKey : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    ∀ {h₁ : Std.Internal.List.containsKey k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) = true}
      {h₂ : Std.Internal.List.containsKey k l₁ = true},
      Std.Internal.List.getValue k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) h₁ =
        Std.Internal.List.getValue k l₁ h₂
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.equiv_iff_toList_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (t₁.Equiv t₂ ↔ t₁.toList = t₂.toList)
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.localizationAway_map : ∀ {R : Type u} (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (r : R)
  [inst_3 : IsLocalization.Away r S] (x : Unit), (Algebra.PreSubmersivePresentation.localizationAway S r).map x = ()
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveView.mk.injEq : ∀ (ref declId : Lean.Syntax) (modifiers : Lean.Elab.Modifiers) (isClass allowIndices allowSortPolymorphism : Bool)
  (shortDeclName declName : Lean.Name) (levelNames : List Lean.Name) (binders : Lean.Syntax)
  (type? : Option Lean.Syntax) (ctors : Array Lean.Elab.Command.CtorView)
  (computedFields : Array Lean.Elab.Command.ComputedFieldView) (derivingClasses : Array Lean.Elab.DerivingClassView)
  (docString? : Option (Lean.TSyntax `Lean.Parser.Command.docComment)) (isCoinductive : Bool)
  (ref_1 declId_1 : Lean.Syntax) (modifiers_1 : Lean.Elab.Modifiers)
  (isClass_1 allowIndices_1 allowSortPolymorphism_1 : Bool) (shortDeclName_1 declName_1 : Lean.Name)
  (levelNames_1 : List Lean.Name) (binders_1 : Lean.Syntax) (type?_1 : Option Lean.Syntax)
  (ctors_1 : Array Lean.Elab.Command.CtorView) (computedFields_1 : Array Lean.Elab.Command.ComputedFieldView)
  (derivingClasses_1 : Array Lean.Elab.DerivingClassView)
  (docString?_1 : Option (Lean.TSyntax `Lean.Parser.Command.docComment)) (isCoinductive_1 : Bool),
  ({ ref := ref, declId := declId, modifiers := modifiers, isClass := isClass, allowIndices := allowIndices,
        allowSortPolymorphism := allowSortPolymorphism, shortDeclName := shortDeclName, declName := declName,
        levelNames := levelNames, binders := binders, type? := type?, ctors := ctors, computedFields := computedFields,
        derivingClasses := derivingClasses, docString? := docString?, isCoinductive := isCoinductive } =
      { ref := ref_1, declId := declId_1, modifiers := modifiers_1, isClass := isClass_1,
        allowIndices := allowIndices_1, allowSortPolymorphism := allowSortPolymorphism_1,
        shortDeclName := shortDeclName_1, declName := declName_1, levelNames := levelNames_1, binders := binders_1,
        type? := type?_1, ctors := ctors_1, computedFields := computedFields_1, derivingClasses := derivingClasses_1,
        docString? := docString?_1, isCoinductive := isCoinductive_1 }) =
    (ref = ref_1 ∧
      declId = declId_1 ∧
        modifiers = modifiers_1 ∧
          isClass = isClass_1 ∧
            allowIndices = allowIndices_1 ∧
              allowSortPolymorphism = allowSortPolymorphism_1 ∧
                shortDeclName = shortDeclName_1 ∧
                  declName = declName_1 ∧
                    levelNames = levelNames_1 ∧
                      binders = binders_1 ∧
                        type? = type?_1 ∧
                          ctors = ctors_1 ∧
                            computedFields = computedFields_1 ∧
                              derivingClasses = derivingClasses_1 ∧
                                docString? = docString?_1 ∧ isCoinductive = isCoinductive_1)
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_monotone : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : Type w) [inst_1 : LinearOrder J] [inst_2 : SuccOrder J]
  [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J], Monotone fun W => W.transfiniteCompositionsOfShape J
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toList_roo_eq_some_iff : ∀ {k m n : ℤ} {i : ℕ}, (m<...n).toList[i]? = some k ↔ i < (n - (m + 1)).toNat ∧ m + 1 + ↑i = k
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_emptyWithCapacity : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : Inhabited α] {a : α} {c : ℕ},
  (Std.HashMap.emptyWithCapacity c).getKey! a = default
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.copy_rfl_rfl : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.copy ⋯ ⋯ = p
-- Mathlib.FieldTheory.SeparablyGenerated
/-- Suppose `k` has characteristic `p` and `K/k` is finitely generated.
Suppose furthermore that if `{ sᵢ } ⊆ K` is an arbitrary `k`-linearly independent set,
`{ sᵢᵖ } ⊆ K` is also `k`-linearly independent (which is true when `K ⊗ₖ k^{1/p}` is reduced).

Then `K/k` is finite separably generated.

TODO: show that this is an if and only if.
 -/
exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_essFiniteType : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] (p : ℕ),
  Nat.Prime p →
    (∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x => x ^ p) ↑s) →
      ∀ [ExpChar k p] [Algebra.EssFiniteType k K],
        ∃ s, IsTranscendenceBasis k Subtype.val ∧ Algebra.IsSeparable (↥(IntermediateField.adjoin k ↑s)) K
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- The pre-`0`-hypercover associated to a presieve `R`. It is indexed by the morphisms in `R`.  -/
CategoryTheory.Presieve.preZeroHypercover : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {S : C} → CategoryTheory.Presieve S → CategoryTheory.PreZeroHypercover S
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            {A : C} →
              [inst_4 : CategoryTheory.AddMonObj A] →
                (X : D) → [addMod : CategoryTheory.AddModObj A X] → CategoryTheory.AddMod D A
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.encard_le_of_isSeparated : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {A C : Set X} {ε : NNReal},
  C ⊆ A → Metric.IsSeparated (↑ε) C → Metric.packingNumber ε A ≠ ⊤ → C.encard ≤ (Metric.maximalSeparatedSet ε A).encard
-- Lean.Util.Trace
/-- Convert an `Except` to a `TraceResult` using the `ExceptToTraceResult` instance.  -/
Lean.Except.toTraceResult : {α ε : Type} → [Lean.ExceptToTraceResult ε α] → Except ε α → Lean.TraceResult
-- Init.Data.Order.Factories
/-- This lemma characterizes in terms of `LE α` when a `Min α` instance "behaves like an infimum
operator".
 -/
Std.LawfulOrderInf.of_le : ∀ {α : Type u} [inst : Min α] [inst_1 : LE α], (∀ (a b c : α), a ≤ b ⊓ c ↔ a ≤ b ∧ a ≤ c) → Std.LawfulOrderInf α
-- Mathlib.Data.Multiset.Interval
Multiset.card_Ioc : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α),
  (Finset.Ioc s t).card = ∏ i ∈ s.toFinset ∪ t.toFinset, (Multiset.count i t + 1 - Multiset.count i s) - 1
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.mem_copy : ∀ {R : Type u_1} [inst : CommRing R] (P : RingPreordering R) (S : Set R) (hS : S = ↑P) {x : R}, x ∈ P.copy S hS ↔ x ∈ S
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- The action fulfils a normality condition on summands that lie in `H`.
This ensures that the action descends to an action on the quotient `G ⧸ H`.  -/
AddAction.QuotientAction.inv_mul_mem : ∀ {G : Type u} {X : Type v} {inst : AddGroup G} {inst_1 : AddMonoid X} {inst_2 : AddAction X G} {H : AddSubgroup G}
  [self : AddAction.QuotientAction X H] (x : X) {g g' : G}, -g + g' ∈ H → -(x +ᵥ g) + (x +ᵥ g') ∈ H
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.mk.sizeOf_spec : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}}
  {D : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ} {e : J} [inst_1 : SizeOf J]
  (prop_id : D.W (CategoryTheory.CategoryStruct.id e)) (lift : {j : J} → D.P j → (j ⟶ e))
  (hlift : ∀ {j : J} (hj : D.P j), D.W (lift hj)) (uniq : ∀ {j : J} (hj : D.P j) {φ : j ⟶ e}, D.W φ → lift hj = φ)
  (comm : ∀ {i j : J} (f : i ⟶ j) (hf : D.W f), CategoryTheory.CategoryStruct.comp f (lift ⋯) = lift ⋯),
  sizeOf { prop_id := prop_id, lift := lift, hlift := hlift, uniq := uniq, comm := comm } = 1 + sizeOf prop_id
-- Mathlib.Analysis.Normed.Group.Hom
/-- The kernel of a bounded group homomorphism. Naturally endowed with a
`SeminormedAddCommGroup` instance.  -/
NormedAddGroupHom.ker : {V₁ : Type u_3} →
  {V₂ : Type u_4} →
    [inst : SeminormedAddCommGroup V₁] → [inst_1 : SeminormedAddCommGroup V₂] → NormedAddGroupHom V₁ V₂ → AddSubgroup V₁
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
VectorBundle.injective_eval_mdifferentiableAt_sec : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] (F : Type u_5) [inst_6 : NormedAddCommGroup F]
  (V : M → Type u_6) [inst_7 : TopologicalSpace (Bundle.TotalSpace F V)] [inst_8 : (x : M) → AddCommGroup (V x)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : NormedSpace 𝕜 F]
  [inst_12 : (x : M) → Module 𝕜 (V x)] (W : Type u_7) [inst_13 : AddCommGroup W] [inst_14 : Module 𝕜 W]
  [inst_15 : TopologicalSpace W] (x : M), Function.Injective fun A Z x_1 => A (Z x)
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- The `fixingSubgroup` of a finite subset of cardinal `d`
in an `n`-transitive additive action acts `n-d`-transitively on the complement.  -/
SubAddAction.ofFixingAddSubgroup.isMultiplyPretransitive : ∀ (G : Type u_1) {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {m n : ℕ}
  [Hn : AddAction.IsMultiplyPretransitive G α n] (s : Set α) [Finite ↑s],
  s.ncard + m = n →
    AddAction.IsMultiplyPretransitive (↥(fixingAddSubgroup G s)) (↥(SubAddAction.ofFixingAddSubgroup G s)) m
-- Mathlib.Data.Finset.Sups
Finset.card_infs_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] (s t : Finset α),
  (s ⊼ t).card = s.card * t.card ↔ Set.InjOn (fun x => x.1 ⊓ x.2) (↑s ×ˢ ↑t)
-- Mathlib.Algebra.Order.Module.Defs
/-- An ordered module is a module with a partial order such that scalar multiplication by a
positive scalar and of a positive vector are both strictly monotone.  -/
IsStrictOrderedModule : (α : Type u_1) → (β : Type u_2) → [SMul α β] → [Preorder α] → [Preorder β] → [Zero α] → [Zero β] → Prop
-- Mathlib.Algebra.Group.Finsupp
Finsupp.mapRange_sub : ∀ {ι : Type u_1} {G : Type u_6} {H : Type u_7} [inst : SubNegZeroMonoid G] [inst_1 : SubNegZeroMonoid H] {f : G → H}
  {hf : f 0 = 0},
  (∀ (x y : G), f (x - y) = f x - f y) →
    ∀ (v₁ v₂ : ι →₀ G), Finsupp.mapRange f hf (v₁ - v₂) = Finsupp.mapRange f hf v₁ - Finsupp.mapRange f hf v₂
-- Mathlib.Algebra.Ring.Ext
NonUnitalSemiring.ext : ∀ {R : Type u} ⦃inst₁ inst₂ : NonUnitalSemiring R⦄, HAdd.hAdd = HAdd.hAdd → HMul.hMul = HMul.hMul → inst₁ = inst₂
-- Mathlib.Order.GaloisConnection.Defs
/-- A constructive choice function for images of `l`.  -/
GaloisInsertion.choice : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] → {l : α → β} → {u : β → α} → GaloisInsertion l u → (x : α) → u (l x) ≤ x → β
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_erase_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k fallback : α}, (m.erase k).getKeyD k fallback = fallback
-- Mathlib.Order.Bounds.Image
/-- **Alias** of `BddBelow.range_comp_left`. -/
BddBelow.range_comp : ∀ {α : Type u} {β : Type v} {γ : Type u_1} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {g : β → γ},
  BddBelow (Set.range f) → Monotone g → BddBelow (Set.range fun x => g (f x))
-- Mathlib.Order.Category.PartOrd
PartOrd.dual_map : ∀ {X Y : PartOrd} (f : X ⟶ Y), PartOrd.dual.map f = PartOrd.ofHom (OrderHom.dual (PartOrd.Hom.hom f))
-- Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
AlgebraicGeometry.WeaklyEtale.instIsZariskiLocalAtSource : AlgebraicGeometry.IsZariskiLocalAtSource @AlgebraicGeometry.WeaklyEtale
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.OplaxTrans.isoMk_inv_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (app : (a : B) → η.app a ≅ θ.app a)
  (naturality :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b).hom)
            (θ.naturality f) =
          CategoryTheory.CategoryStruct.comp (η.naturality f)
            (CategoryTheory.Bicategory.whiskerRight (app a).hom (G.map f)))
      CategoryTheory.Oplax.OplaxTrans.isoMk._auto_1)
  (a : B), (CategoryTheory.Oplax.OplaxTrans.isoMk app naturality).inv.as.app a = (app a).inv
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.not_mem_inter_of_not_mem_right : ∀ {α : 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₂
-- Mathlib.CategoryTheory.Join.Basic
/-- Join.edge c d is the unique morphism from c to d.  -/
CategoryTheory.Join.edge : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (c : C) → (d : D) → CategoryTheory.Join.left c ⟶ CategoryTheory.Join.right d
-- Mathlib.Algebra.GroupWithZero.Defs
/-- If `α` has no zero divisors, then the product of two elements equals zero iff one of them
equals zero.  -/
zero_eq_mul : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] [NoZeroDivisors M₀] {a b : M₀}, 0 = a * b ↔ a = 0 ∨ b = 0
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instReprCompletionItemTag.repr : Lean.Lsp.CompletionItemTag → ℕ → Std.Format
-- Mathlib.RingTheory.PicardGroup
LinearEquiv.congrRight.eq_1 : ∀ {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} {M₃ : Type u_8} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] (f : M₂ ≃ₗ[R] M₃), f.congrRight = (LinearEquiv.refl R M).arrowCongr f
-- Lean.Meta.Tactic.Grind.Types
/-- `ctor := true` if the head symbol is a constructor application.  -/
Lean.Meta.Grind.ENode.ctor : Lean.Meta.Grind.ENode → Bool
-- Mathlib.Order.Hom.Lex
/-- A linear order is isomorphic to the lexicographic sum of elements less than `x` and elements
greater or equal to `x`.  -/
OrderIso.sumLexIioIci : {α : Type u_1} → [inst : LinearOrder α] → (x : α) → ↑(Set.Iio x) ⊕ₗ ↑(Set.Ici x) ≃o α
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.rangeRestrict_injective_iff : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N},
  Function.Injective ⇑f.rangeRestrict ↔ Function.Injective ⇑f
-- Mathlib.LinearAlgebra.Matrix.Swap
/-- Multiplying with `swap R i j` on the right swaps the `j`-th column with the `i`-th column.  -/
Matrix.mul_swap_apply_right : ∀ {R : Type u_1} {n : Type u_2} {m : Type u_3} [inst : Semiring R] [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  (i j : n) (a : m) (g : Matrix m n R), (g * Matrix.swap R i j) a j = g a i
-- Std.Time.DateTime.Timestamp
Std.Time.instDecidableLeTimestamp : {x y : Std.Time.Timestamp} → Decidable (x ≤ y)
-- Mathlib.Algebra.Order.Rearrangement
/-- **Rearrangement Inequality**: Pointwise scalar multiplication of `f` and `g` is maximized when
`f` and `g` monovary together on `s`. Stated by permuting the entries of `g`.  -/
MonovaryOn.sum_smul_comp_perm_le_sum_smul : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [ExistsAddOfLE α] [inst_4 : AddCommMonoid β] [inst_5 : LinearOrder β] [IsOrderedCancelAddMonoid β]
  [inst_7 : Module α β] [PosSMulMono α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β},
  MonovaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → ∑ i ∈ s, f i • g (σ i) ≤ ∑ i ∈ s, f i • g i
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.GrothendieckTopology.toSheafify_sheafifyLift_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D}
  (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) {Z : CategoryTheory.Functor Cᵒᵖ D} (h : Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp (J.toSheafify P) (CategoryTheory.CategoryStruct.comp (J.sheafifyLift η hQ) h) =
    CategoryTheory.CategoryStruct.comp η h