mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.Hom.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {X Y : AlgebraicGeometry.PresheafedSpace C}
  {base : ↑X ⟶ ↑Y} {c : Y.presheaf ⟶ (TopCat.Presheaf.pushforward C base).obj X.presheaf} {base_1 : ↑X ⟶ ↑Y}
  {c_1 : Y.presheaf ⟶ (TopCat.Presheaf.pushforward C base_1).obj X.presheaf},
  { base := base, c := c } = { base := base_1, c := c_1 } → base = base_1 ∧ c ≍ c_1
-- Mathlib.Topology.Algebra.Monoid
exists_open_nhds_one_split : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : MulOneClass M] [ContinuousMul M] {s : Set M},
  s ∈ nhds 1 → ∃ V, IsOpen V ∧ 1 ∈ V ∧ ∀ v ∈ V, ∀ w ∈ V, v * w ∈ s
-- Init.Data.Bool
Bool.ite_eq_cond_iff : ∀ {α : Sort u_1} {p : Prop} {a : Bool} [h : Decidable p] {x y u v : α},
  ((if p then x else y) = bif a then u else v) ↔ (if p then x else y) = if a = true then u else v
-- Mathlib.Analysis.RCLike.Inner
RCLike.wInner_one_eq_inner : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : Fintype ι] [inst_1 : RCLike 𝕜] (f g : ι → 𝕜),
  ⟪f, g⟫_[𝕜] = inner 𝕜 (WithLp.toLp 2 f) (WithLp.toLp 2 g)
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- The `AddSubgroup` generated by an element of an `AddGroup` equals the set of
natural number multiples of the element.  -/
AddSubgroup.mem_closure_singleton : ∀ {G : Type u_1} [inst : AddGroup G] {x y : G}, y ∈ AddSubgroup.closure {x} ↔ ∃ n, n • x = y
-- Mathlib.Probability.Density
MeasureTheory.setLIntegral_pdf_le_map : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {m : MeasurableSpace Ω} (X : Ω → E)
  (ℙ : MeasureTheory.Measure Ω) (μ : autoParam (MeasureTheory.Measure E) MeasureTheory.setLIntegral_pdf_le_map._auto_1)
  (s : Set E), ∫⁻ (x : E) in s, MeasureTheory.pdf X ℙ μ x ∂μ ≤ (MeasureTheory.Measure.map X ℙ) s
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.weights_inj : ∀ {R : Type u} [inst : PartialOrder R] [inst_1 : Semiring R] {M : Type u_9} {f g : Convexity.StdSimplex R M},
  f.weights = g.weights ↔ f = g
-- Lean.Elab.DefView
Lean.Elab.DefView.isInstance : Lean.Elab.DefView → Bool
-- Mathlib.Data.Finset.Card
Finset.card_inter_add_card_union : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), (s ∩ t).card + (s ∪ t).card = s.card + t.card
-- Init.Data.SInt.Lemmas
Int8.lt_of_le_of_ne : ∀ {a b : Int8}, a ≤ b → a ≠ b → a < b
-- Mathlib.Dynamics.BirkhoffSum.QuasiMeasurePreserving
/-- If observables `φ` and `ψ` are `μ`-a.e. equal then the corresponding `birkhoffAverage` are
`μ`-a.e. equal.  -/
MeasureTheory.Measure.QuasiMeasurePreserving.birkhoffAverage_ae_eq_of_ae_eq : ∀ {α : Type u_1} {M : Type u_2} [inst : MeasurableSpace α] [inst_1 : AddCommMonoid M] {f : α → α}
  {μ : MeasureTheory.Measure α} {φ ψ : α → M} (R : Type u_3) [inst_2 : DivisionSemiring R] [inst_3 : Module R M],
  MeasureTheory.Measure.QuasiMeasurePreserving f μ μ →
    φ =ᵐ[μ] ψ → ∀ (n : ℕ), birkhoffAverage R f φ n =ᵐ[μ] birkhoffAverage R f ψ n
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.antilipschitzWith_ofLp : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [hp : Fact (1 ≤ p)] [inst : Fintype ι]
  [inst_1 : (i : ι) → PseudoEMetricSpace (β i)], AntilipschitzWith (↑(Fintype.card ι) ^ (1 / p).toReal) WithLp.ofLp
-- Mathlib.Data.List.Nodup
List.Nodup.set : ∀ {α : Type u} {l : List α} {n : ℕ} {a : α}, l.Nodup → a ∉ l → (l.set n a).Nodup
-- Mathlib.Algebra.Group.Defs
/-- Any `CancelMonoid G` satisfies `IsCancelMul G`.  -/
CancelMonoid.toIsCancelMul : ∀ (M : Type u) [inst : CancelMonoid M], IsCancelMul M
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.singleton_eq_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {p : (a : α) × β a}, {p} = ∅.insert p.fst p.snd
-- Mathlib.Tactic.Explode.Datatypes
/-- Add a pre-existing entry to the `ExprMap` for an additional expression.
This is used by `let` bindings where `expr` is an fvar.  -/
Mathlib.Explode.Entries.addSynonym : Mathlib.Explode.Entries → Lean.Expr → Mathlib.Explode.Entry → Mathlib.Explode.Entries
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.IsNat.of_raw : ∀ (α : Type u_1) [inst : AddMonoidWithOne α] (n : ℕ), Mathlib.Meta.NormNum.IsNat n.rawCast n
-- Mathlib.Tactic.Positivity.Basic
/-- Extension for `PNat.val`.  -/
Mathlib.Meta.Positivity.evalPNatVal : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Order.ModularLattice
infIccOrderIsoIccSup'_apply_coe : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : IsModularLattice α] (a b : α) (a_1 : ↑(Set.Icc (a ⊓ b) b)),
  ↑((infIccOrderIsoIccSup' a b) a_1) = ↑a_1 ⊔ a
-- Lean.Meta.InferType
_private.Lean.Meta.InferType.0.Lean.Meta.inferTypeImp.infer : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Order.Filter.Pointwise
Filter.pureZeroHom.eq_1 : ∀ {α : Type u_2} [inst : Zero α], Filter.pureZeroHom = { toFun := pure, map_zero' := ⋯ }
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_map : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w} [EquivBEq α]
  [LawfulHashable α] {f : (a : α) → β a → γ a} {k fallback : α},
  (Std.DHashMap.map f m).getKeyD k fallback = m.getKeyD k fallback
-- Mathlib.RepresentationTheory.Rep.Basic
/-- The natural isomorphism between the representations on `k[G¹]` and `k[G]` induced by left
multiplication in `G`.  -/
Rep.diagonalOneIsoLeftRegular : (k : Type u) → (G : Type v) → [inst : Ring k] → [inst_1 : Monoid G] → Rep.diagonal k G 1 ≅ Rep.leftRegular k G
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.opNorm_pi : ∀ {𝕜 : Type u} {E : Type wE} {ι : Type v} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : Fintype ι] {ι' : Type u_1} [inst_4 : Fintype ι'] {F : ι' → Type u_2}
  [inst_5 : (i' : ι') → SeminormedAddCommGroup (F i')] [inst_6 : (i' : ι') → NormedSpace 𝕜 (F i')]
  (f : (i' : ι') → E [⋀^ι]→L[𝕜] F i'), ‖ContinuousAlternatingMap.pi f‖ = ‖f‖
-- Lean.Meta.Constructions.SparseCasesOn
Lean.Meta.getSparseCasesOnInfoCore : Lean.Environment → Lean.Name → Option Lean.Meta.SparseCasesOnInfo
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Structure.FG.out : ∀ {L : FirstOrder.Language} {M : Type u_1} {inst : L.Structure M} [self : FirstOrder.Language.Structure.FG L M], ⊤.FG
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.abs_sin_eq_sin_abs_of_abs_le_pi : ∀ {x : ℝ}, |x| ≤ Real.pi → |Real.sin x| = Real.sin |x|
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsExtTangent.symm : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s₁ s₂ : EuclideanGeometry.Sphere P}, s₁.IsExtTangent s₂ → s₂.IsExtTangent s₁
-- Lean.Parser.Extra
Lean.Parser.notSymbol : String → Lean.Parser.Parser
-- Lean.ResolveName
_private.Lean.ResolveName.0.Lean.ResolveName.resolveGlobalName.loop : Lean.Environment →
  Lean.Options →
    Lean.Name → List Lean.OpenDecl → Lean.MacroScopesView → Lean.Name → List String → List (Lean.Name × List String)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- The map from the `mixedSpace K` to `realSpace K` that sends each component to its norm.
 -/
NumberField.mixedEmbedding.normAtAllPlaces : {K : Type u_1} → [inst : Field K] → NumberField.mixedEmbedding.mixedSpace K → NumberField.mixedEmbedding.realSpace K
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.indexEquiv_inv : ∀ {ι : 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] {P : RootPairing ι R M N} (g : P.Aut),
  (↑g⁻¹).indexEquiv = ((RootPairing.Equiv.indexHom P) g)⁻¹
-- Lean.Parser.Basic
Lean.Parser.withAntiquotSpliceAndSuffix : Lean.SyntaxNodeKind → Lean.Parser.Parser → Lean.Parser.Parser → Lean.Parser.Parser
-- Batteries.Data.Array.Lemmas
Array.idxOf?_toList : ∀ {α : Type u_1} [inst : BEq α] {a : α} {l : Array α}, List.idxOf? a l.toList = l.idxOf? a
-- Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky
_private.Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky.0.UniqueFactorizationMonoid.span_notMem_kaplanskySet : ∀ {R : Type u_1} [inst : CommSemiring R] [IsDomain R] {a : R},
  a ≠ 0 →
    (∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x) →
      Ideal.span {a} ∉ UniqueFactorizationMonoid.kaplanskySet✝ (Submonoid.closure {r | Prime r}).toSubsemigroup
-- Init.Data.ByteArray.Lemmas
ByteArray.append_inj_left : ∀ {xs₁ xs₂ ys₁ ys₂ : ByteArray}, xs₁ ++ ys₁ = xs₂ ++ ys₂ → xs₁.size = xs₂.size → xs₁ = xs₂
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_C_mul_X : ∀ {R : Type u} [inst : Semiring R] (a : R), Polynomial.derivative (Polynomial.C a * Polynomial.X) = Polynomial.C a
-- Mathlib.GroupTheory.ArchimedeanDensely
/-- In two linearly ordered groups, the closure of an element of one group
is isomorphic (and order-isomorphic) to the closure of an element in the other group.  -/
LinearOrderedCommGroup.closure_equiv_closure : {G : Type u_1} →
  {G' : Type u_2} →
    [inst : CommGroup G] →
      [inst_1 : LinearOrder G] →
        [IsOrderedMonoid G] →
          [inst_3 : CommGroup G'] →
            [inst_4 : LinearOrder G'] →
              [IsOrderedMonoid G'] →
                (x : G) → (y : G') → (x = 1 ↔ y = 1) → ↥(Subgroup.closure {x}) ≃*o ↥(Subgroup.closure {y})
-- Aesop.Util.Basic
_private.Aesop.Util.Basic.0.Aesop.elabPattern.adjustCtx : Lean.Elab.Term.Context → Lean.Elab.Term.Context
-- Mathlib.GroupTheory.Rank
AddGroup.rank_eq_zero_iff : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : AddGroup.FG G], AddGroup.rank G = 0 ↔ Subsingleton G
-- Init.Data.String.Slice
/-- Checks whether a slice only consists of matches of the pattern `pat`, starting from the back
of the string.

Short-circuits at the first pattern mis-match.

This function is generic over all currently supported patterns.

For many types of patterns, this function can be expected to return the same result as
`Slice.all`. If mismatches are expected to occur close to the end of the string, this function
might be more efficient.

For some types of patterns, this function will return a different result than `Slice.all`.
Consider, for example, a pattern that matches the longest string at the given position that matches
the regular expression `"a|aa|ab"`. Then, given the input string `"aab"`, performing
`Slice.all` will greedily match the prefix `"aa"` and then get stuck on the remainder
`"b"`, causing it to return `false`. On the other hand, `Slice.revAll` will match
the suffix `"ab"` and then match the remainder `"a"`, so it will return `true`.

Examples:

* `"brown".toSlice.revAll Char.isLower = true`

* `"brown and orange".toSlice.revAll Char.isLower = false`

* `"aaaaaa".toSlice.revAll 'a' = true`

* `"aaaaaa".toSlice.revAll "aa" = true`

* `"aaaaaaa".toSlice.revAll "aa" = false`
 -/
String.Slice.revAll : {ρ : Type} → String.Slice → (pat : ρ) → [String.Slice.Pattern.BackwardPattern pat] → Bool
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
SimpleGraph.LocallyLinear.map : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} (f : α ↪ β),
  G.LocallyLinear → (SimpleGraph.map (⇑f) G).LocallyLinear
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.leftInvSeq_singleton : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B),
  cs.leftInvSeq [i] = [cs.simple i]
-- Mathlib.Data.Set.NAry
/-- If `b` is a right identity for `f : α → β → α`, then `{b}` is a right identity for
`Set.image2 f`.  -/
Set.image2_right_identity : ∀ {α : Type u_1} {β : Type u_3} {f : α → β → α} {b : β}, (∀ (a : α), f a b = a) → ∀ (s : Set α), Set.image2 f s {b} = s
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearMap.transvection.comp_of_right_eq_apply : ∀ {R : Type u_1} {V : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid V] [inst_2 : Module R V]
  {f g : Module.Dual R V} {v x : V},
  f v = 0 → (LinearMap.transvection f v) ((LinearMap.transvection g v) x) = (LinearMap.transvection (f + g) v) x
-- Init.Data.Iterators.Consumers.Monadic.Collect
/-- Traverses the given iterator and stores the emitted values in reverse order in a list. Because
lists are prepend-only, this `toListRev` is usually more efficient that `toList`.

If the iterator is not finite, this function might run forever. The variant
`it.ensureTermination.toListRev` always terminates after finitely many steps.
 -/
Std.IterM.toListRev : {α : Type w} → {m : Type w → Type w'} → [Monad m] → {β : Type w} → [Std.Iterator α m β] → Std.IterM m β → m (List β)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.forInStep_eq_foldlM.match_1.splitter : {δ : Type u_1} →
  (motive : ForInStep δ → Sort u_2) →
    (x : ForInStep δ) → ((d : δ) → motive (ForInStep.yield d)) → ((d : δ) → motive (ForInStep.done d)) → motive x
-- Mathlib.Data.Fin.Tuple.Curry
/-- `Equiv.curry` for n-ary functions.  -/
Function.OfArity.curryEquiv : {α β : Type u} → (n : ℕ) → ((Fin n → α) → β) ≃ Function.OfArity α β n
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.coe_mapRingHom : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddMonoid M]
  (f : R →+* S), ⇑(AddMonoidAlgebra.mapRingHom M f) = AddMonoidAlgebra.map ↑f
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.tensorHomEquiv_apply : ∀ {k : Type u} [inst : CommRing k] {G : Type v} [inst_1 : Group G] (A B C : Rep.{u, u, v} k G)
  (f : CategoryTheory.MonoidalCategoryStruct.tensorObj A B ⟶ C),
  (A.tensorHomEquiv B C) f =
    Rep.ofHom { toLinearMap := (TensorProduct.curry (Rep.Hom.hom f).toLinearMap).flip, isIntertwining' := ⋯ }
-- Mathlib.Order.DirSupClosed
/-- **Alias** of the forward direction of `dirSupInacc_compl`. -/
DirSupClosed.of_compl : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α], DirSupInacc sᶜ → DirSupClosed s
-- Mathlib.FieldTheory.AbelRuffini
isSolvable_gal_minpoly : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {x : E},
  x ∈ solvableByRad F E → Group.IsSolvable (minpoly F x).Gal
-- Mathlib.Data.Sym.Sym2
Sym2.instNontrivial : ∀ {α : Type u_1} [Nontrivial α], Nontrivial (Sym2 α)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_of_perm : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l l' : List ((a : α) × β a)} {a : α},
  Std.Internal.List.DistinctKeys l →
    l.Perm l' → Std.Internal.List.getValueCast? a l = Std.Internal.List.getValueCast? a l'
-- Lean.Data.Position
Lean.instToJsonPosition : Lean.ToJson Lean.Position
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
/-- `a ↦ a ^ p` is operator monotone for `p ∈ [0,1]`.  -/
CFC.monotone_nnrpow : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A] {p : NNReal},
  p ∈ Set.Icc 0 1 → Monotone fun a => a ^ p
-- Lean.Data.PrefixTree
Lean.PrefixTree.foldMatchingM : {m : Type u_1 → Type u_2} →
  {α : Type u_3} →
    {β : Type u_4} →
      {p : α → α → Ordering} → {σ : Type u_1} → [Monad m] → Lean.PrefixTree α β p → List α → σ → (β → σ → m σ) → m σ
-- Init.Data.SInt.Lemmas
Int8.toInt_le : ∀ (x : Int8), x.toInt ≤ Int8.maxValue.toInt
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.ofNatIsoLeft.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D C} (adj : F ⊣ H) (iso : F ≅ G),
  adj.ofNatIsoLeft iso =
    { unit := CategoryTheory.CategoryStruct.comp adj.unit (CategoryTheory.Functor.whiskerRight iso.hom H),
      counit := CategoryTheory.CategoryStruct.comp (H.whiskerLeft iso.inv) adj.counit, left_triangle_components := ⋯,
      right_triangle_components := ⋯ }
-- Batteries.Data.List.Lemmas
List.min!_nil : ∀ {α : Type u_1} [inst : Inhabited α] [inst_1 : Min α], [].min! = default
-- Mathlib.Tactic.NormNum.Inv
Mathlib.Meta.NormNum.isNNRat_divNat : ∀ {a na n b nb d : ℕ},
  Mathlib.Meta.NormNum.IsNat a na →
    Mathlib.Meta.NormNum.IsNat b nb →
      Mathlib.Meta.NormNum.IsNNRat (↑na / ↑nb) n d → Mathlib.Meta.NormNum.IsNNRat (NNRat.divNat a b) n d
-- Mathlib.CategoryTheory.Sites.Point.Monoidal
CategoryTheory.GrothendieckTopology.Point.instIsIsoηFunctorOppositePresheafFiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.MonoidalCategory A]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A],
  CategoryTheory.IsIso (CategoryTheory.Functor.OplaxMonoidal.η Φ.presheafFiber)
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.CompletionItemCapabilities.mk.injEq : ∀ (insertReplaceSupport? insertReplaceSupport?_1 : Option Bool),
  ({ insertReplaceSupport? := insertReplaceSupport? } = { insertReplaceSupport? := insertReplaceSupport?_1 }) =
    (insertReplaceSupport? = insertReplaceSupport?_1)
-- Mathlib.CategoryTheory.MorphismProperty.Representable
/-- A morphism `f : X ⟶ Y` in `D` is said to be relatively representable if for any
`g : F.obj a ⟶ Y`, there exists a pullback square of the following form
```
F.obj b --F.map snd--> F.obj a
    |                     |
   fst                    g
    |                     |
    v                     v
    X ------- f --------> Y
```
 -/
CategoryTheory.Functor.relativelyRepresentable : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → CategoryTheory.MorphismProperty D
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.evalAddMonoidHom_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : AddZeroClass Y] (x : X)
  (x_1 : LocallyConstant X Y), (LocallyConstant.evalAddMonoidHom x) x_1 = x_1 x
-- Mathlib.Data.Analysis.Topology
Ctop.coe_mk : ∀ {α : Type u_1} {σ : Type u_3} (f : σ → Set α) (T : α → σ) (h₁ : ∀ (x : α), x ∈ f (T x))
  (I : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ) (h₂ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (I a b x h))
  (h₃ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (I a b x h) ⊆ f a ∩ f b) (a : σ),
  { f := f, top := T, top_mem := h₁, inter := I, inter_mem := h₂, inter_sub := h₃ }.f a = f a
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_keysArray : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m.keysArray.isEmpty = m.isEmpty
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.homMk'_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {Y' : C} {S : CategoryTheory.Functor C D} (f : CategoryTheory.CostructuredArrow S T) (g : Y' ⟶ f.left),
  (f.homMk' g).left = g
-- Mathlib.Algebra.Lie.Basic
lie_jacobi : ∀ {L : Type v} [inst : LieRing L] (x y z : L), ⁅x, ⁅y, z⁆⁆ + ⁅y, ⁅z, x⁆⁆ + ⁅z, ⁅x, y⁆⁆ = 0
-- Init.Data.Array.Lemmas
List.allM_toArray : ∀ {m : Type → Type u_1} {α : Type u_2} [inst : Monad m] [LawfulMonad m] {p : α → m Bool} {l : List α},
  Array.allM p l.toArray = List.allM p l
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.IsMonicOfDegree.natDegree_sub_X_pow : ∀ {R : Type u_1} [inst : Ring R] {p : Polynomial R} {n : ℕ},
  n ≠ 0 → p.IsMonicOfDegree n → (p - Polynomial.X ^ n).natDegree < n
-- Mathlib.Data.Part
Part.right_dom_of_append_dom : ∀ {α : Type u_1} [inst : Append α] {a b : Part α}, (a ++ b).Dom → b.Dom
-- Init.Data.List.Basic
List.foldl_cons : ∀ {α : Type u} {β : Type v} {a : α} {l : List α} {f : β → α → β} {b : β},
  List.foldl f b (a :: l) = List.foldl f (f b a) l
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Zipper.prependMapGT : {α : Type u} →
  {β : α → Type v} →
    [Ord α] → Std.DTreeMap.Internal.Impl α β → α → Std.DTreeMap.Internal.Zipper α β → Std.DTreeMap.Internal.Zipper α β
-- Init.Data.Iterators.Combinators.Monadic.Attach
Std.Iterators.Types.Attach.mk.injEq : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] {P : β → Prop} (inner : Std.IterM m β)
  (invariant : ∀ (out : β), inner.IsPlausibleIndirectOutput out → P out) (inner_1 : Std.IterM m β)
  (invariant_1 : ∀ (out : β), inner_1.IsPlausibleIndirectOutput out → P out),
  ({ inner := inner, invariant := invariant } = { inner := inner_1, invariant := invariant_1 }) = (inner = inner_1)
-- Mathlib.Algebra.Free
FreeSemigroup.lift_comp_of' : ∀ {α : Type u} {β : Type v} [inst : Semigroup β] (f : FreeSemigroup α →ₙ* β),
  FreeSemigroup.lift (⇑f ∘ FreeSemigroup.of) = f
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey?_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {l : List (α × β)} {k k' : α},
      cmp k k' = Ordering.eq →
        List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
          k ∈ List.map Prod.fst l → (Std.DTreeMap.Raw.Const.insertMany t l).getKey? k' = some k
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.mk.injEq : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] (toAddSubgroup : AddSubgroup G)
  (isOpen' : IsOpen toAddSubgroup.carrier) (toAddSubgroup_1 : AddSubgroup G)
  (isOpen'_1 : IsOpen toAddSubgroup_1.carrier),
  ({ toAddSubgroup := toAddSubgroup, isOpen' := isOpen' } =
      { toAddSubgroup := toAddSubgroup_1, isOpen' := isOpen'_1 }) =
    (toAddSubgroup = toAddSubgroup_1)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Atom.mk.sizeOf_spec : ∀ (e : Lean.Expr) (src tgt : Mathlib.Tactic.BicategoryLike.Mor₁),
  sizeOf { e := e, src := src, tgt := tgt } = 1 + sizeOf e + sizeOf src + sizeOf tgt
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.IsZero.eq_zero_of_tgt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C},
  CategoryTheory.Limits.IsZero Y → ∀ (f : X ⟶ Y), f = 0
-- Mathlib.CategoryTheory.Sites.PreservesSheafification
CategoryTheory.sheafComposeIso_hom_fac_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1}
  {B : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_1} A] [inst_2 : CategoryTheory.Category.{v_2, u_2} B]
  (F : CategoryTheory.Functor A B) [inst_3 : CategoryTheory.HasWeakSheafify J A]
  [inst_4 : CategoryTheory.HasWeakSheafify J B] [inst_5 : J.HasSheafCompose F] [inst_6 : J.PreservesSheafification F]
  (P : CategoryTheory.Functor Cᵒᵖ A) {Z : CategoryTheory.Functor Cᵒᵖ B} (h : (CategoryTheory.sheafify J P).comp F ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J (P.comp F))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyComposeIso J F P).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.toSheafify J P) F) h
-- Mathlib.Data.Set.Basic
Set.ssubset_of_subset_of_ssubset : ∀ {α : Type u} {s₁ s₂ s₃ : Set α}, s₁ ⊆ s₂ → s₂ ⊂ s₃ → s₁ ⊂ s₃
-- Mathlib.Order.Directed
/-- A class for an `IsDirected` relation `≥`.  -/
IsCodirectedOrder : (α : Type u_5) → [LE α] → Prop
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.lift_spec_mul_add : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {g : R →+* P}
  (hg : ∀ (y : ↥M), IsUnit (g ↑y)) (z : S) (w w' v : P),
  ((IsLocalization.toLocalizationMap M S).lift hg) z * w + w' = v ↔
    g ((IsLocalization.toLocalizationMap M S).sec z).1 * w + g ↑((IsLocalization.toLocalizationMap M S).sec z).2 * w' =
      g ↑((IsLocalization.toLocalizationMap M S).sec z).2 * v
-- Mathlib.Topology.CompactOpen
ContinuousMap.homeoFnOfDiscrete_apply : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : DiscreteTopology X]
  (f : C(X, Y)) (a : X), ContinuousMap.homeoFnOfDiscrete f a = f a