mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Idempotents.Biproducts
CategoryTheory.Idempotents.Karoubi.instHasBinaryBiproductComplement : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (P : CategoryTheory.Idempotents.Karoubi C), CategoryTheory.Limits.HasBinaryBiproduct P P.complement
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.tensorRightUnmopIso_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ)
  (X_1 : C),
  X.tensorRightUnmopIso.inv.app X_1 =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X_1 X.unmop)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Submonoid.powers_le_zpowers : ∀ {G : Type u_2} [inst : Group G] (g : G), Submonoid.powers g ≤ (Subgroup.zpowers g).toSubmonoid
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.instContainsIdentitiesDiagonalOfRespectsIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {P : CategoryTheory.MorphismProperty C} [P.ContainsIdentities] [P.RespectsIso], P.diagonal.ContainsIdentities
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_erase_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {fallback : β}, Std.DTreeMap.Const.getD (t.erase k) k fallback = fallback
-- Mathlib.GroupTheory.Index
AddSubgroup.IsFiniteRelIndex.to_finiteIndex_addSubgroupOf : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} [H.IsFiniteRelIndex K], (H.addSubgroupOf K).FiniteIndex
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.not_mem_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, k ∉ t₁ → k ∉ t₁ \ t₂
-- Init.Data.Repr
instReprAtomInt : ReprAtom ℤ
-- Mathlib.Logic.Equiv.Fin.Basic
isRight_finSumNatEquiv_symm_apply : ∀ {n : ℕ} (i : ℕ), ((finSumNatEquiv n).symm i).isRight = decide (n ≤ i)
-- Mathlib.Tactic.CategoryTheory.CancelIso
/-- Version of `IsIso.hom_inv_id` for internal use of the `cancelIso` simproc. Do not use.  -/
Mathlib.Tactic.CategoryTheory.CancelIso.hom_inv_id_of_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {x y : C} (f : x ⟶ y) [inst_1 : CategoryTheory.IsIso f]
  (g : y ⟶ x), CategoryTheory.inv f = g → CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.id x
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.laxMonoidalPi'_ε : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {D : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : (i : I) → CategoryTheory.Functor D (C i)) [inst_4 : (i : I) → (F i).LaxMonoidal] (i : I),
  CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Functor.pi' F) i = CategoryTheory.Functor.LaxMonoidal.ε (F i)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.walkingSpanOpEquiv_inverse_obj : ∀ (X : CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair),
  CategoryTheory.Limits.walkingSpanOpEquiv.inverse.obj X = Opposite.op X
-- Lean.Server.Rpc.Basic
Lean.Server.ReferencedObject.mk.sizeOf_spec : ∀ (obj : Dynamic) (id : USize) (rc : ℕ),
  sizeOf { obj := obj, id := id, rc := rc } = 1 + sizeOf obj + sizeOf id + sizeOf rc
-- Mathlib.Order.Filter.IsBounded
/-- In linear orders, frequent boundedness from above implies coboundedness for `≥`.  -/
Filter.IsCobounded.of_frequently_le : ∀ {α : Type u_1} {f : Filter α} [inst : LinearOrder α] {l : α},
  (∃ᶠ (x : α) in f, x ≤ l) → Filter.IsCobounded (fun x1 x2 => x2 ≤ x1) f
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.nodal_empty : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_2} {v : ι → R}, Lagrange.nodal ∅ v = 1
-- Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.le_isCardinalPresentable : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {κ : Cardinal.{w}}
  [inst_1 : Fact κ.IsRegular], P.IsCardinalFilteredGenerator κ → P ≤ CategoryTheory.isCardinalPresentable C κ
-- Aesop.Builder.Basic
Aesop.RuleBuilder : Type
-- Mathlib.Probability.Kernel.Composition.MapComap
/-- The pushforward of a kernel along a measurable function. This is an implementation detail,
use `map κ f` instead.  -/
ProbabilityTheory.Kernel.mapOfMeasurable : {α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      {mβ : MeasurableSpace β} →
        {γ : Type u_4} →
          {mγ : MeasurableSpace γ} →
            ProbabilityTheory.Kernel α β → (f : β → γ) → Measurable f → ProbabilityTheory.Kernel α γ
-- Mathlib.CategoryTheory.Action.Limits
Action.instHasFiniteLimits : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [CategoryTheory.Limits.HasFiniteLimits V], CategoryTheory.Limits.HasFiniteLimits (Action V G)
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.BalancedAtRoot.adjust_right : ∀ {l r r' : ℕ},
  Std.DTreeMap.Internal.Impl.BalancedAtRoot l r →
    r - 1 ≤ r' →
      r' ≤ r + 1 →
        Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l r' ∨ Std.DTreeMap.Internal.Impl.BalanceLErasePrecond r' l
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.lift_apply : ∀ {α : Type u_1} {M : Type u_4} [inst : Monoid M] (f : α → M) (l : FreeMonoid α),
  (FreeMonoid.lift f) l = (List.map f (FreeMonoid.toList l)).prod
-- Mathlib.RingTheory.Finiteness.Cofinite
/-- A submodule that contains a CoFG submodule is CoFG.  -/
Submodule.CoFG.of_le : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {S T : Submodule R M},
  S ≤ T → S.CoFG → T.CoFG
-- Init.MethodSpecsSimp
AndThen.andThen_eq_hAndThen : ∀ {α : Type u_1} [inst : AndThen α], AndThen.andThen = HAndThen.hAndThen
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the angle between three points is `-π / 2`, the first and third points are not equal.  -/
EuclideanGeometry.left_ne_right_of_oangle_eq_neg_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(-Real.pi / 2) → p₁ ≠ p₃
-- Mathlib.Data.List.AList
AList.perm_lookup : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {s₁ s₂ : AList β},
  s₁.entries.Perm s₂.entries → AList.lookup a s₁ = AList.lookup a s₂
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.inverse.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] (f : ZeroHom M N) (g : N → M)
  (h₁ : Function.LeftInverse g ⇑f), f.inverse g h₁ = { toFun := g, map_zero' := ⋯ }
-- Batteries.Data.Fin.Fold
Fin.dfoldrM_loop_succ : ∀ {m : Type u_1 → Type u_2} {n : ℕ} {α : Fin (n + 1) → Type u_1} {i : ℕ} {h : i + 1 < n + 1} [inst : Monad m]
  (f : (i : Fin n) → α i.succ → m (α i.castSucc)) (x : α ⟨i + 1, h⟩),
  Fin.dfoldrM.loop n α f (i + 1) h x = f ⟨i, ⋯⟩ x >>= Fin.dfoldrM.loop n α f i ⋯
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- A version of `liftExpand` used to simultaneously lift functions with two arguments
in `X[S⁻¹]`.  -/
OreLocalization.lift₂Expand : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {X : Type u_3} →
          [inst_2 : MulAction R X] →
            {C : Sort u_2} →
              (P : X → ↥S → X → ↥S → C) →
                (∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ * ↑s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ * ↑s₂ ∈ S),
                    P r₁ s₁ r₂ s₂ = P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩ (t₂ • r₂) ⟨t₂ * ↑s₂, ht₂⟩) →
                  OreLocalization S X → OreLocalization S X → C
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.compl_compl : ∀ {α : Type u_1} [inst : LE α] (s : LowerSet α), s.compl.compl = s
-- Init.Data.SInt.Lemmas
Int16.sub_zero : ∀ (a : Int16), a - 0 = a
-- Mathlib.Algebra.GroupWithZero.Hom
/-- `MonoidWithZeroHom` down-cast to a `MonoidHom`, forgetting the 0-preserving property.  -/
MonoidWithZeroHom.coeToMonoidHom : {α : Type u_2} → {β : Type u_3} → [inst : MulZeroOneClass α] → [inst_1 : MulZeroOneClass β] → Coe (α →*₀ β) (α →* β)
-- Std.Http.Internal.IndexMultiMap
/-- Gets the number of entries in the map.
 -/
Std.Internal.IndexMultiMap.size : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Std.Internal.IndexMultiMap α β → ℕ
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.isPath_map_iff_of_injective : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u v : V} {p : G.Walk u v},
  Function.Injective ⇑f → ((SimpleGraph.Walk.map f p).IsPath ↔ p.IsPath)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.get?_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α], t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ {k : α}, t₁.get? k = t₂.get? k
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.isMulCommutative_iSup : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {ι : Sort u_2} [Nonempty ι] {S : ι → NonUnitalSubsemiring R}
  [hS : ∀ (i : ι), IsMulCommutative ↥(S i)], Directed (fun x1 x2 => x1 ≤ x2) S → IsMulCommutative ↥(⨆ i, S i)
-- Mathlib.Algebra.Group.Units.Basic
LeftCancelMonoid.mul_ne_one : ∀ {α : Type u} [inst : LeftCancelMonoid α] [Subsingleton αˣ] {a b : α}, a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1
-- Init.Data.List.Sublist
List.head_filter_mem : ∀ {α : Type u_1} (xs : List α) (p : α → Bool) (h : List.filter p xs ≠ []), (List.filter p xs).head h ∈ xs
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.IsTree.coe_subgraphOfAdj : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V} (h : G.Adj u v), (G.subgraphOfAdj h).coe.IsTree
-- Mathlib.Algebra.Star.TransferInstance
/-- Transfer `StarMul` across an `Equiv`. See note [reducible non-instances].  -/
Equiv.starMul : {R : Type u_1} → {S : Type u_2} → (e : R ≃ S) → [inst : Mul S] → [StarMul S] → StarMul R
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.addCommGroup : {R : Type u_1} → [inst : NonUnitalNonAssocRing R] → (I : TwoSidedIdeal R) → AddCommGroup ↥I
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.simpleFunc_bot' : ∀ {β : Type u_2} {α : Type u_5} [Nonempty β] (f : MeasureTheory.SimpleFunc α β),
  ∃ c, f = MeasureTheory.SimpleFunc.const α c
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
/-- The only divisors of prime powers are prime powers.  -/
Associates.eq_pow_find_of_dvd_irreducible_pow : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [UniqueFactorizationMonoid α] {a p : Associates α},
  Irreducible p → ∀ [inst_2 : (n : ℕ) → Decidable (a ∣ p ^ n)] {n : ℕ} (h : a ∣ p ^ n), a = p ^ Nat.find ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.app_zero_eq_ι : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (t : CategoryTheory.Limits.Fork f g),
  t.π.app CategoryTheory.Limits.WalkingParallelPair.zero = t.ι
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.AreComplementary.Boundary.congr_simp : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {e₁ e₁_1 : c₁.Embedding c} (e_e₁ : e₁ = e₁_1) {e₂ e₂_1 : c₂.Embedding c} (e_e₂ : e₂ = e₂_1)
  (x : e₁.AreComplementary e₂) (i₁ i₁_1 : ι₁),
  i₁ = i₁_1 → ∀ (i₂ i₂_1 : ι₂), i₂ = i₂_1 → x.Boundary i₁ i₂ = ⋯.Boundary i₁_1 i₂_1
-- Mathlib.Tactic.ClickSuggestions.Apply
/-- Generate the suggestion for applying `lem`.  -/
Mathlib.Tactic.ClickSuggestions.ApplyLemma.try : Mathlib.Tactic.ClickSuggestions.ApplyLemma →
  Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM
    (Mathlib.Tactic.ClickSuggestions.Result Mathlib.Tactic.ClickSuggestions.ApplyKey)
-- Lean.Environment
Lean.Kernel.Exception.exprTypeMismatch.injEq : ∀ (env : Lean.Kernel.Environment) (lctx : Lean.LocalContext) (expr expectedType : Lean.Expr)
  (env_1 : Lean.Kernel.Environment) (lctx_1 : Lean.LocalContext) (expr_1 expectedType_1 : Lean.Expr),
  (Lean.Kernel.Exception.exprTypeMismatch env lctx expr expectedType =
      Lean.Kernel.Exception.exprTypeMismatch env_1 lctx_1 expr_1 expectedType_1) =
    (env = env_1 ∧ lctx = lctx_1 ∧ expr = expr_1 ∧ expectedType = expectedType_1)
-- Mathlib.Data.Finset.Defs
Finset.Subset.refl : ∀ {α : Type u_1} (s : Finset α), s ⊆ s
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.HasPullbacksOfInclusions.hasPullbackInl : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C}
  [self : CategoryTheory.HasPullbacksOfInclusions C] {X Y Z : C} (f : Z ⟶ X ⨿ Y),
  CategoryTheory.Limits.HasPullback CategoryTheory.Limits.coprod.inl f
-- Mathlib.Tactic.ClickSuggestions
/-- Rpc function for the `#click_suggestions` widget.  -/
Mathlib.Tactic.ClickSuggestions.rpc : ProofWidgets.PanelWidgetProps → Lean.Server.RequestM (Lean.Server.RequestTask ProofWidgets.Html)
-- Mathlib.Topology.ClusterPt
/-- If `x` is an accumulation point of `F` and `F ≤ G`, then
`x` is an accumulation point of `G`.  -/
AccPt.mono : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {F G : Filter X}, AccPt x F → F ≤ G → AccPt x G
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.hom_ext_iff : ∀ {X Y : NonemptyFinLinOrd} {f g : X ⟶ Y}, f = g ↔ LinOrd.Hom.hom f.hom = LinOrd.Hom.hom g.hom
-- Lean.Parser.Types
Lean.Parser.FirstTokens.instToString : ToString Lean.Parser.FirstTokens
-- Mathlib.Data.PNat.Factors
PNat.factorMultiset_mul : ∀ (n m : ℕ+), (n * m).factorMultiset = n.factorMultiset + m.factorMultiset
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
inhomogeneousCochains.d_hom_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Monoid G] (A : Rep.{u_1, u, u} k G) (n : ℕ) (f : (Fin n → G) → ↑A)
  (g : Fin (n + 1) → G),
  (ModuleCat.Hom.hom (inhomogeneousCochains.d A n)) f g =
    (A.ρ (g 0)) (f fun i => g i.succ) + ∑ j, (-1) ^ (↑j + 1) • f (j.contractNth (fun x1 x2 => x1 * x2) g)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.instHasForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteGrpCatMonoidHomCarrier.eq_1 : ProfiniteGrp.instHasForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteGrpCatMonoidHomCarrier =
  {
    forget₂ :=
      { obj := fun P => GrpCat.of ↑P.toProfinite.toTop,
        map := fun {X Y} f => GrpCat.ofHom (ProfiniteGrp.Hom.hom f).toMonoidHom,
        map_id :=
          ProfiniteGrp.instHasForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteGrpCatMonoidHomCarrier._proof_1,
        map_comp :=
          @ProfiniteGrp.instHasForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteGrpCatMonoidHomCarrier._proof_2 },
    forget_comp :=
      ProfiniteGrp.instHasForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteGrpCatMonoidHomCarrier._proof_4 }
-- Mathlib.Combinatorics.Matroid.Minor.Contract
/-- **Alias** of `Matroid.IsCocircuit.delete_sdiff_isCocircuit`. -/
Matroid.IsCocircuit.delete_diff_isCocircuit : ∀ {α : Type u_1} {M : Matroid α} {K X : Set α}, M.IsCocircuit K → X ⊆ K → X.Nonempty → (M.delete (K \ X)).IsCocircuit X
-- Mathlib.Algebra.BigOperators.Group.List.Lemmas
List.alternatingProd_reverse : ∀ {G : Type u_7} [inst : CommGroup G] (l : List G),
  l.reverse.alternatingProd = l.alternatingProd ^ (-1) ^ (l.length + 1)
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerMap_submatrix_right : ∀ {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12}
  {n' : Type u_17} {p' : Type u_18} (f : α → β → γ) (A : Matrix l m α) (B : Matrix n p β) (r : n' → n) (c : p' → p),
  Matrix.kroneckerMap f A (B.submatrix r c) = (Matrix.kroneckerMap f A B).submatrix (Prod.map id r) (Prod.map id c)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_left_inj : ∀ {x y z : ℝ}, 0 ≤ x → 0 ≤ y → z ≠ 0 → (x ^ z = y ^ z ↔ x = y)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_add_of_le_of_pos : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftStrictMono α] {a b c : α},
  b ≤ c → 0 < a → b < c + a
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
CategoryTheory.Abelian.Pseudoelement.eq_zero_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q),
  f = 0 ↔ ∀ (a : CategoryTheory.Abelian.Pseudoelement P), CategoryTheory.Abelian.Pseudoelement.pseudoApply f a = 0
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.instOrderBot : {k : Type u_1} →
  {K : Type u_2} →
    [inst : Field k] → [inst_1 : Field K] → [inst_2 : Algebra k K] → OrderBot (FiniteGaloisIntermediateField k K)
-- Mathlib.Topology.Algebra.Group.Basic
Filter.map_divRight_nhdsLT : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : CommGroup H] [IsTopologicalGroup H] [inst_3 : PartialOrder H]
  [IsOrderedMonoid H] {c a : H},
  Filter.map (fun x => x / c) (nhdsWithin a (Set.Iio a)) = nhdsWithin (a / c) (Set.Iio (a / c))
-- Mathlib.Order.Filter.Germ.Basic
/-- If a germ `f : Germ l β` is constant, where `l : Filter α`,
and a function `g : γ → α` tends to `l` along `lc : Filter γ`,
the germ of the composition `f ∘ g` is also constant.  -/
Filter.Germ.isConstant_compTendsto : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} {f : l.Germ β} {lc : Filter γ} {g : γ → α},
  f.IsConstant → ∀ (hg : Filter.Tendsto g lc l), (f.compTendsto g hg).IsConstant
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.exists_ae_eq_isMarkovKernel : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  {μ : MeasureTheory.Measure α},
  (∀ᵐ (a : α) ∂μ, MeasureTheory.IsProbabilityMeasure (κ a)) →
    μ ≠ 0 → ∃ η, ⇑κ =ᵐ[μ] ⇑η ∧ ProbabilityTheory.IsMarkovKernel η
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
/-- **Alias** of `ContinuousLinearMap.precompUniformConvergenceCLM`.

---

Pre-composition by a *fixed* continuous linear map as a continuous linear map for the uniform
convergence topology.  -/
ContinuousLinearMap.precomp_uniformConvergenceCLM : {𝕜₁ : Type u_6} →
  {𝕜₂ : Type u_7} →
    {𝕜₃ : Type u_8} →
      [inst : NormedField 𝕜₁] →
        [inst_1 : NormedField 𝕜₂] →
          [inst_2 : NormedField 𝕜₃] →
            {σ : 𝕜₁ →+* 𝕜₂} →
              {τ : 𝕜₂ →+* 𝕜₃} →
                {ρ : 𝕜₁ →+* 𝕜₃} →
                  [RingHomCompTriple σ τ ρ] →
                    {E : Type u_9} →
                      {F : Type u_10} →
                        (G : Type u_11) →
                          [inst_4 : AddCommGroup E] →
                            [inst_5 : Module 𝕜₁ E] →
                              [inst_6 : AddCommGroup F] →
                                [inst_7 : Module 𝕜₂ F] →
                                  [inst_8 : AddCommGroup G] →
                                    [inst_9 : Module 𝕜₃ G] →
                                      [inst_10 : TopologicalSpace E] →
                                        [inst_11 : TopologicalSpace F] →
                                          [inst_12 : TopologicalSpace G] →
                                            (𝔖 : Set (Set E)) →
                                              (𝔗 : Set (Set F)) →
                                                [inst_13 : IsTopologicalAddGroup G] →
                                                  [inst_14 : ContinuousConstSMul 𝕜₃ G] →
                                                    (L : E →SL[σ] F) →
                                                      Set.MapsTo (fun x => ⇑L '' x) 𝔖 𝔗 →
                                                        UniformConvergenceCLM τ G 𝔗 →L[𝕜₃] UniformConvergenceCLM ρ G 𝔖
-- Mathlib.CategoryTheory.Shift.Localization
CategoryTheory.MorphismProperty.IsCompatibleWithShift.shiftFunctor_comp_inverts : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] {A : Type w}
  [inst_3 : AddMonoid A] [inst_4 : CategoryTheory.HasShift C A] [W.IsCompatibleWithShift A] (a : A),
  W.IsInvertedBy ((CategoryTheory.shiftFunctor C a).comp L)
-- Mathlib.Algebra.Order.GroupWithZero.Defs
posMulStrictMono_iff_posMulReflectLE : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : LinearOrder α], PosMulStrictMono α ↔ PosMulReflectLE α
-- Std.Tactic.BVDecide.LRAT.Actions
Std.Tactic.BVDecide.LRAT.Action.addRat.injEq : ∀ {β : Type u} {α : Type v} (id : ℕ) (c : β) (pivot : Std.Sat.Literal α) (rupHints : Array ℕ)
  (ratHints : Array (ℕ × Array ℕ)) (id_1 : ℕ) (c_1 : β) (pivot_1 : Std.Sat.Literal α) (rupHints_1 : Array ℕ)
  (ratHints_1 : Array (ℕ × Array ℕ)),
  (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints =
      Std.Tactic.BVDecide.LRAT.Action.addRat id_1 c_1 pivot_1 rupHints_1 ratHints_1) =
    (id = id_1 ∧ c = c_1 ∧ pivot = pivot_1 ∧ rupHints = rupHints_1 ∧ ratHints = ratHints_1)
-- Mathlib.Analysis.Normed.Group.Uniform
MonoidHomClass.lipschitz_of_bound_nnnorm : ∀ {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F]
  [inst_2 : FunLike 𝓕 E F] [MonoidHomClass 𝓕 E F] (f : 𝓕) (C : NNReal),
  (∀ (x : E), ‖f x‖₊ ≤ C * ‖x‖₊) → LipschitzWith C ⇑f
-- Mathlib.Control.Functor.Multivariate
/-- Multivariate map, if `f : α ⟹ β` and `x : F α` then `f <$$> x : F β`.  -/
MvFunctor.map : {n : ℕ} → {F : TypeVec.{u_2} n → Type u_1} → [self : MvFunctor F] → {α β : TypeVec.{u_2} n} → α.Arrow β → F α → F β
-- Init.Data.Order.Ord
Std.instReflOrdProd : ∀ {α : Type u_1} {β : Type u_2} [inst : Ord α] [inst_1 : Ord β] [Std.ReflOrd α] [Std.ReflOrd β], Std.ReflOrd (α × β)
-- Mathlib.Algebra.QuaternionBasis
/-- Transform a `QuaternionAlgebra.Basis` through an `AlgHom`.  -/
QuaternionAlgebra.Basis.compHom : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : Ring A] →
          [inst_2 : Ring B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] →
                {c₁ c₂ c₃ : R} → QuaternionAlgebra.Basis A c₁ c₂ c₃ → (A →ₐ[R] B) → QuaternionAlgebra.Basis B c₁ c₂ c₃
-- Init.Data.List.Basic
/-- If the first list is a suffix of the second, returns the result of dropping the suffix from the
second.

In other words, `isSuffixOf? l₁ l₂` returns `some t` when `l₂ == t ++ l₁`.

Examples:
 * `[2, 3].isSuffixOf? [1, 2, 3] = some [1]`
 * `[2, 3].isSuffixOf? [1, 2, 3, 4] = none`
 * `[2, 3].isSuffixOf? [1, 2] = none`
 * `[2, 3].isSuffixOf? [1, 1, 2, 3] = some [1, 1]`
 -/
List.isSuffixOf? : {α : Type u} → [BEq α] → List α → List α → Option (List α)
-- Mathlib.Algebra.Group.Subsemigroup.Basic
Subsemigroup.mem_iSup : ∀ {M : Type u_1} [inst : Mul M] {ι : Sort u_3} (p : ι → Subsemigroup M) {m : M},
  m ∈ ⨆ i, p i ↔ ∀ (N : Subsemigroup M), (∀ (i : ι), p i ≤ N) → m ∈ N
-- Mathlib.Topology.Order.UpperLowerSetTopology
/-- `toLowerSet` as an `OrderIso`  -/
Topology.WithLowerSet.toLowerSetOrderIso : {α : Type u_1} → [inst : Preorder α] → α ≃o Topology.WithLowerSet α
-- Mathlib.NumberTheory.Cyclotomic.Basic
CyclotomicRing.instAlgebraCyclotomicField : (n : ℕ) →
  (A : Type u) →
    (K : Type w) →
      [inst : CommRing A] →
        [inst_1 : Field K] → [inst_2 : Algebra A K] → Algebra (CyclotomicRing n A K) (CyclotomicField n K)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mapIso_counitIso_inv_app_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S S' : D} {T : CategoryTheory.Functor C D} (i : S ≅ S')
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S') T),
  ((CategoryTheory.StructuredArrow.mapIso i).counitIso.inv.app X).right = CategoryTheory.CategoryStruct.id X.right