mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
hasMFDerivWithinAt_const : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] (c : M') (s : Set M) (x : M),
  HasMFDerivAt[s] (fun x => c) x 0
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- The type of morphisms in `AddMagmaCat R`.  -/
AddMagmaCat.Hom : AddMagmaCat → AddMagmaCat → Type u
-- Mathlib.Order.Filter.AtTopBot.BigOperators
/-- Let `g : γ → β` be an injective function and `f : β → α` be a function from the codomain of `g`
to an additive commutative monoid. Suppose that `f x = 0` outside of the range of `g`. Then the
filters `atTop.map (fun s ↦ ∑ i ∈ s, f (g i))` and `atTop.map (fun s ↦ ∑ i ∈ s, f i)` coincide.

This lemma is used to prove the equality `∑' x, f (g x) = ∑' y, f y` under
the same assumptions.  -/
Function.Injective.map_atTop_finsetSum_eq : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] {g : α → β},
  Function.Injective g →
    ∀ {f : β → M},
      (∀ x ∉ Set.range g, f x = 0) →
        Filter.map (fun s => ∑ i ∈ s, f (g i)) Filter.atTop = Filter.map (fun s => ∑ i ∈ s, f i) Filter.atTop
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.natDegree_primPart : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] (p : Polynomial R),
  p.primPart.natDegree = p.natDegree
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.Equiv.mk : ∀ {α : Type u} {β : α → Type v} {t t' : Std.DTreeMap.Internal.Impl α β}, t.toListModel.Perm t'.toListModel → t.Equiv t'
-- Mathlib.Data.Fin.Tuple.Basic
piFinTwoEquiv_apply : ∀ (α : Fin 2 → Type u), ⇑(piFinTwoEquiv α) = fun f => (f 0, f 1)
-- Mathlib.Algebra.Category.Grp.Biproducts
AddCommGrpCat.biproductIsoPi_inv_comp_π_apply : ∀ {J : Type} [inst : Finite J] (f : J → AddCommGrpCat) (j : J) (x : (j : J) → ↑(f j)),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.biproduct.π f j))
      ((CategoryTheory.ConcreteCategory.hom (AddCommGrpCat.biproductIsoPi f).inv) x) =
    x j
-- Mathlib.Algebra.Category.Grp.Ulift
AddGrpCat.uliftFunctor_preservesLimit : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J AddGrpCat),
  CategoryTheory.Limits.PreservesLimit K AddGrpCat.uliftFunctor
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepSet.eq_1 : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} (s : ι → Set Ω) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.iIndepSet s μ =
    ProbabilityTheory.Kernel.iIndepSet s (ProbabilityTheory.Kernel.const Unit μ) (MeasureTheory.Measure.dirac ())
-- Init.Data.UInt.Lemmas
UInt32.toUSize_le : ∀ {a b : UInt32}, a.toUSize ≤ b.toUSize ↔ a ≤ b
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.uncurry_obj_curry_obj_flip_flip : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  {D : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E] {H : Type u₅} [inst_4 : CategoryTheory.Category.{v₅, u₅} H]
  (F₁ : CategoryTheory.Functor B C) (F₂ : CategoryTheory.Functor D E) (G : CategoryTheory.Functor (C × E) H),
  CategoryTheory.Functor.uncurry.obj (F₂.comp (F₁.comp (CategoryTheory.Functor.curry.obj G)).flip).flip =
    (F₁.prod F₂).comp G
-- Mathlib.Analysis.Convex.Side
AffineSubspace.SOppSide.nonempty : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P}, s.SOppSide x y → (↑s).Nonempty
-- Lean.Meta.Tactic.Simp.Rewrite
/-- Return true if `e` is of the form `(x : α) → ... → s = t → ... → False`

Recall that this kind of proposition is generated by Lean when creating equations for
functions and match-expressions with overlapping cases.
Example: the following `match`-expression has overlapping cases.
```
def f (x y : Nat) :=
  match x, y with
  | Nat.succ n, Nat.succ m => ...
  | _, _ => 0
```
The second equation is of the form
```
(x y : Nat) → ((n m : Nat) → x = Nat.succ n → y = Nat.succ m → False) → f x y = 0
```
The hypothesis `(n m : Nat) → x = Nat.succ n → y = Nat.succ m → False` is essentially
saying the first case is not applicable.
 -/
Lean.Meta.Simp.isEqnThmHypothesis : Lean.Expr → Bool
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.neg_comp_neg_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : C) [inst_2 : CategoryTheory.AddGrpObj A] {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.AddGrpObj.neg
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddGrpObj.neg h) =
    h
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.liftTruncLE_ι_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {X Y : C} (f : X ⟶ Y) (n : ℤ) [inst_6 : t.IsLE X n] {Z : C}
  (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (t.liftTruncLE f n) (CategoryTheory.CategoryStruct.comp ((t.truncLEι n).app Y) h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.Tactic.Ring.Common
/-- A sum `a + b` is a polynomial if `a` is a monomial and `b` is another polynomial.  -/
Mathlib.Tactic.Ring.Common.ExSumNat.add : {a b : Q(ℕ)} →
  Mathlib.Tactic.Ring.Common.ExProdNat a →
    Mathlib.Tactic.Ring.Common.ExSumNat b → Mathlib.Tactic.Ring.Common.ExSumNat q(«$a» + «$b»)
-- Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
MeasureTheory.eLpNorm'_lt_top_of_eLpNorm'_lt_top_of_exponent_le : ∀ {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ε}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {p q : ℝ} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.eLpNorm' f q μ < ⊤ → 0 ≤ p → p ≤ q → MeasureTheory.eLpNorm' f p μ < ⊤
-- Mathlib.Order.Category.BddDistLat
BddDistLat.instInhabited : Inhabited BddDistLat
-- Mathlib.CategoryTheory.MorphismProperty.Basic
/-- The family of morphisms indexed by `P.toSet` which corresponds
to `P : MorphismProperty C`, see `MorphismProperty.ofHoms_homFamily`.  -/
CategoryTheory.MorphismProperty.homFamily : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (P : CategoryTheory.MorphismProperty C) → (f : ↑P.toSet) → (↑f).left ⟶ (↑f).right
-- Lean.Elab.Command
/-- The environment linter framework needs to be able to run linters with the same context
as `liftTermElabM`, so we expose that context as a public function here.
 -/
Lean.Elab.Command.mkMetaContext : Lean.Meta.Context
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.liftFromProjective_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S : CategoryTheory.ShortComplex C} (hS : S.Exact) {P : C} (f : P ⟶ S.X₂) [inst_2 : CategoryTheory.Projective P]
  (hf : CategoryTheory.CategoryStruct.comp f S.g = 0),
  CategoryTheory.CategoryStruct.comp (hS.liftFromProjective f hf) S.f = f
-- Mathlib.Data.Stream.Init
Stream'.corec_def : ∀ {α : Type u} {β : Type v} (f : α → β) (g : α → α) (a : α), Stream'.corec f g a = Stream'.map f (Stream'.iterate g a)
-- Init.Grind.Ordered.Order
Lean.Grind.Preorder.le_of_lt : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] {a b : α}, a < b → a ≤ b
-- Init.Data.SInt.Bitwise
Int32.neg_one_shiftLeft_or_shiftLeft : ∀ {a b : Int32}, (-1) <<< b ||| a <<< b = (-1) <<< b
-- Init.Grind.Ordered.Field
Lean.Grind.Field.IsOrdered.inv_pos_iff : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] {a : R}, 0 < a⁻¹ ↔ 0 < a
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- `G.PreservesRightKanExtensions L` asserts that `G` preserves all pointwise right Kan
extensions of `F` along `L` for every `F`.  -/
CategoryTheory.Functor.PreservesPointwiseRightKanExtension : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      {D : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} A] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D] →
                CategoryTheory.Functor B D → CategoryTheory.Functor A B → CategoryTheory.Functor A C → Prop
-- Mathlib.Tactic.GCongr.Core
/-- Index of the right varying argument.  -/
Mathlib.Tactic.GCongr.GCongrHyp.rhsIdx : Mathlib.Tactic.GCongr.GCongrHyp → ℕ
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
CategoryTheory.instEffectiveEpiOfIsIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f],
  CategoryTheory.EffectiveEpi f
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- Taking the cocone of a whiskered bicone results in a cone isomorphic to one gained
by whiskering the cocone and precomposing with a suitable isomorphism.  -/
CategoryTheory.Limits.Bicone.whiskerToCocone : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {K : Type w'} →
          {f : J → C} →
            (c : CategoryTheory.Limits.Bicone f) →
              (g : K ≃ J) →
                (c.whisker g).toCocone ≅
                  (CategoryTheory.Limits.Cocone.precompose (CategoryTheory.Discrete.functorComp f ⇑g).hom).obj
                    (CategoryTheory.Limits.Cocone.whisker
                      (CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ ⇑g)) c.toCocone)
-- Mathlib.Analysis.Real.Pi.Bounds
Real.ceil_pi_eq_four : ⌈Real.pi⌉ = 4
-- Mathlib.SetTheory.ZFC.Basic
/-- Given a predicate `p` on ZFC sets. `Hereditarily p x` means that `x` has property `p` and the
members of `x` are all `Hereditarily p`.  -/
ZFSet.Hereditarily : (ZFSet.{u_1} → Prop) → ZFSet.{u_1} → Prop
-- Mathlib.FieldTheory.Fixed
/-- Let $F$ be a field. Let $G$ be a finite group acting faithfully on $F$.
Then $[F : F^G] = |G|$.  -/
FixedPoints.finrank_eq_card : ∀ (G : Type u_2) (F : Type u_3) [inst : Group G] [inst_1 : Field F] [inst_2 : MulSemiringAction G F]
  [inst_3 : Fintype G] [FaithfulSMul G F], Module.finrank (↥(FixedPoints.subfield G F)) F = Fintype.card G
-- Mathlib.GroupTheory.MonoidLocalization.Order
AddLocalization.mkOrderEmbedding_apply : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α]
  {s : AddSubmonoid α} (b : ↥s) (a : α), (AddLocalization.mkOrderEmbedding b) a = AddLocalization.mk a b
-- Mathlib.Data.Finset.Preimage
Finset.subset_map_iff : ∀ {α : Type u} {β : Type v} {f : α ↪ β} {s : Finset β} {t : Finset α}, s ⊆ Finset.map f t ↔ ∃ u ⊆ t, s = Finset.map f u
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.sMod_lt : ∀ (p : ℕ), p ≠ 0 → ∀ (i : ℕ), LucasLehmer.sMod p i < 2 ^ p - 1
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.center_eq_iff_eq_of_mem : ∀ {P : Type u_2} [inst : MetricSpace P] {s₁ s₂ : EuclideanGeometry.Sphere P} {p : P},
  p ∈ s₁ → p ∈ s₂ → (s₁.center = s₂.center ↔ s₁ = s₂)
-- Std.Data.TreeMap.Raw.WF
Std.TreeMap.Raw.WF.ofArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {a : Array (α × β)},
  (Std.TreeMap.Raw.ofArray a cmp).WF
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeft_obj_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ : CategoryTheory.Functor A T} (l : L₁ ⟶ L₂)
  (hl :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
      P (CategoryTheory.CategoryStruct.comp (l.app X.left) X.hom))
  (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapLeft R l hl).obj X).left = X.left
-- Mathlib.Dynamics.SymbolicDynamics.Basic
SymbolicDynamics.FullShift.Pattern.mk.sizeOf_spec : ∀ {A : Type u_1} {G : Type u_2} [inst : Inhabited A] [inst_1 : SizeOf A] [inst_2 : SizeOf G] (config : G → A)
  (support : Finset G) (condition : ∀ g ∉ support, config g = default),
  sizeOf { config := config, support := support, condition := condition } = 1 + sizeOf support
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.irreducible_pow_sup_of_ge : ∀ {T : Type u_4} [inst : CommRing T] [IsDedekindDomain T] {I J : Ideal T},
  I ≠ ⊥ → Irreducible J → ∀ (n : ℕ), emultiplicity J I ≤ ↑n → J ^ n ⊔ I = J ^ multiplicity J I
-- Init.Sym.Lemmas
Lean.Sym.BitVec.lt_eq_false : ∀ {n : ℕ} (a b : BitVec n), decide (a < b) = false → (a < b) = False
-- Mathlib.RingTheory.Kaehler.Basic
/-- The map `Ω[A⁄R] →ₗ[A] Ω[B⁄S]` given a square
```
A --→ B
↑     ↑
|     |
R --→ S
```
 -/
KaehlerDifferential.map : (R : Type u) →
  (S : Type v) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (A : Type u_2) →
            (B : Type u_3) →
              [inst_3 : CommRing A] →
                [inst_4 : CommRing B] →
                  [inst_5 : Algebra R A] →
                    [inst_6 : Algebra A B] →
                      [inst_7 : Algebra S B] →
                        [inst_8 : Algebra R B] →
                          [IsScalarTower R A B] →
                            [IsScalarTower R S B] → [inst_11 : SMulCommClass S A B] → Ω[A⁄R] →ₗ[A] Ω[B⁄S]
-- Mathlib.Geometry.Manifold.Submersion
Manifold.IsSubmersionAt.codChart_mem_maximalAtlas : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {H : Type u_7} {G : Type u_9} {E : Type u} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  {x : M} (h : Manifold.IsSubmersionAt I J n f x), h.codChart ∈ IsManifold.maximalAtlas J n N
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.instReprOrigin : Repr Lean.Meta.Grind.Origin
-- Aesop.Stats.Extension
Aesop.getStatsArray : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → m Aesop.StatsArray
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.sUnion_neg : ∀ {α : Type u_2} [inst : Neg α] (S : Set (Set α)), -⋃₀ S = ⋃ s ∈ S, -s
-- Mathlib.RingTheory.Finiteness.Basic
Submodule.fg_span : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Set M},
  s.Finite → (Submodule.span R s).FG
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.Pos.skip?_bool_eq_none_iff : ∀ {p : Char → Bool} {s : String.Slice} {pos : s.Pos}, pos.skip? p = none ↔ ∀ (h : pos ≠ s.endPos), p (pos.get h) = false
-- Mathlib.Dynamics.PeriodicPts.Defs
MulAction.pow_mod_period_smul : ∀ {α : Type v} {M : Type u} [inst : Monoid M] [inst_1 : MulAction M α] (n : ℕ) {m : M} {a : α},
  m ^ (n % MulAction.period m a) • a = m ^ n • a
-- Mathlib.CategoryTheory.Adjunction.Triple
/-- For an adjoint triple `F ⊣ G ⊣ H` where `F` and `H` are fully faithful, the natural
transformation `F ⟶ H` is monic at `X` iff the unit of the adjunction `G ⊣ H` is monic
at `F.obj X`.  -/
CategoryTheory.Adjunction.Triple.mono_leftToRight_app_iff_mono_adj₂_unit_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [inst_2 : F.Full] [inst_3 : F.Faithful]
  {X : C}, CategoryTheory.Mono (t.leftToRight.app X) ↔ CategoryTheory.Mono (t.adj₂.unit.app (F.obj X))
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.triangle : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasTerminal C]
  [inst_2 : CategoryTheory.Limits.HasBinaryProducts C] (X Y : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator X (⊤_ C) Y).hom
      (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X)
        (CategoryTheory.Limits.prod.leftUnitor Y).hom) =
    CategoryTheory.Limits.prod.map (CategoryTheory.Limits.prod.rightUnitor X).hom (CategoryTheory.CategoryStruct.id Y)
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.fromRows_ext_iff : ∀ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R)
  (B₁ : Matrix m₁ n R) (B₂ : Matrix m₂ n R), A₁.fromRows A₂ = B₁.fromRows B₂ ↔ A₁ = B₁ ∧ A₂ = B₂
-- Mathlib.Topology.Sheaves.SheafCondition.Sites
compatiblePreserving_opens_map : ∀ {X Y : TopCat} (f : X ⟶ Y),
  CategoryTheory.CompatiblePreserving (Opens.grothendieckTopology ↑X) (TopologicalSpace.Opens.map f)
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformOnFun.topologicalSpace.eq_1 : ∀ (α : Type u_1) (β : Type u_2) [inst : UniformSpace β] (𝔖 : Set (Set α)),
  UniformOnFun.topologicalSpace α β 𝔖 = (UniformOnFun.uniformSpace α β 𝔖).toTopologicalSpace
-- Mathlib.Analysis.Convex.Strong
ConcaveOn.eq_1 : ∀ (𝕜 : Type u_1) {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : SMul 𝕜 E] [inst_6 : SMul 𝕜 β] (s : Set E) (f : E → β),
  ConcaveOn 𝕜 s f =
    (Convex 𝕜 s ∧
      ∀ ⦃x : E⦄,
        x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y))
-- Mathlib.Data.Nat.Dist
Nat.dist_zero_right : ∀ (n : ℕ), n.dist 0 = n
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.domRestrict_le : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.PartialEquiv M N) {A : L.Substructure M} (h : A ≤ f.dom), f.domRestrict h ≤ f
-- Mathlib.GroupTheory.Finiteness
Monoid.fg_of_addMonoid_fg : ∀ {M : Type u_3} [inst : AddMonoid M] [AddMonoid.FG M], Monoid.FG (Multiplicative M)
-- Mathlib.Data.FunLike.Basic
DFunLike.ext'_iff : ∀ {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] {f g : F}, f = g ↔ ⇑f = ⇑g
-- Mathlib.GroupTheory.Submonoid.Centralizer
Submonoid.closureCommMonoidOfComm.eq_1 : ∀ (M : Type u_1) [inst : Monoid M] {s : Set M} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a),
  Submonoid.closureCommMonoidOfComm M hcomm = inferInstance
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.IsRingHom.id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (R : C)
  [inst_2 : CategoryTheory.AddMonObj R] [inst_3 : CategoryTheory.MonObj R],
  CategoryTheory.IsRingHom (CategoryTheory.CategoryStruct.id R)
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.vadd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {c : α} [inst : Add α] [inst_1 : VAdd γ β],
  Function.Periodic f c → ∀ (a : γ), Function.Periodic (a +ᵥ f) c
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.self_comp_symm : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂), ⇑e ∘ ⇑e.symm = id
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.chaar_sup_le : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  {K₀ : TopologicalSpace.PositiveCompacts G} (K₁ K₂ : TopologicalSpace.Compacts G),
  MeasureTheory.Measure.haar.chaar K₀ (K₁ ⊔ K₂) ≤
    MeasureTheory.Measure.haar.chaar K₀ K₁ + MeasureTheory.Measure.haar.chaar K₀ K₂
-- Init.Core
imp_imp_imp : ∀ {a b c d : Prop}, (c → a) → (b → d) → (a → b) → c → d
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.curry_one : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  (F : f₀.Homotopy f₁), F.curry 1 = f₁
-- Mathlib.Topology.Order.Monotone
/-- A monotone function continuous at the infimum of a nonempty set sends this infimum to
the infimum of the image of this set.  -/
MonotoneOn.map_csInf_of_continuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderClosedTopology β]
  {f : α → β} {A : Set α},
  ContinuousWithinAt f A (sInf A) →
    MonotoneOn f A →
      A.Nonempty →
        autoParam (BddBelow A) MonotoneOn.map_csInf_of_continuousWithinAt._auto_1 → f (sInf A) = sInf (f '' A)
-- Init.WFExtrinsicFix
WellFounded.partialExtrinsicFix₂_eq_fix : ∀ {α : Sort u_2} {β : α → Sort u_3} {C₂ : (a : α) → β a → Sort u_1} [inst : ∀ (a : α) (b : β a), Nonempty (C₂ a b)]
  {R : (a : α) ×' β a → (a : α) ×' β a → Prop}
  {F : (a : α) → (b : β a) → ((a' : α) → (b' : β a') → R ⟨a', b'⟩ ⟨a, b⟩ → C₂ a' b') → C₂ a b} (wf : WellFounded R)
  {a : α} {b : β a},
  WellFounded.partialExtrinsicFix₂ R F a b = wf.fix (fun x G => F x.fst x.snd fun a b h => G ⟨a, b⟩ h) ⟨a, b⟩
-- Init.Data.Iterators.Basic
Std.IterM.mk.sizeOf_spec : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : SizeOf α] [inst_1 : (a : Type w) → SizeOf (m a)]
  [inst_2 : SizeOf β] (internalState : α), sizeOf { internalState := internalState } = 1 + sizeOf internalState
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.lift_π_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  {P : C} (p : (b : J) → P ⟶ f b) (j : J) {Z : C} (h : f j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift p)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j) h) =
    CategoryTheory.CategoryStruct.comp (p j) h
-- Mathlib.Algebra.Order.Nonneg.Field
Nonneg.zpow : {α : Type u_1} → [inst : Semifield α] → [inst_1 : LinearOrder α] → [IsStrictOrderedRing α] → Pow { x // 0 ≤ x } ℤ
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.Adjunction.compCounit.eq_1 : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b c : B} {f₁ : a ⟶ b} {g₁ : b ⟶ a} {f₂ : b ⟶ c} {g₂ : c ⟶ b}
  (adj₁ : CategoryTheory.Bicategory.Adjunction f₁ g₁) (adj₂ : CategoryTheory.Bicategory.Adjunction f₂ g₂),
  adj₁.compCounit adj₂ =
    CategoryTheory.bicategoricalComp
      (CategoryTheory.CategoryStruct.id
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp g₂ g₁)
          (CategoryTheory.CategoryStruct.comp f₁ f₂)))
      (CategoryTheory.bicategoricalComp
        (CategoryTheory.Bicategory.whiskerLeft g₂ (CategoryTheory.Bicategory.whiskerRight adj₁.counit f₂)) adj₂.counit)