mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_id_left_hom_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B}
  (f : a ⟶ b) (X : ↑(F.obj a)) {Z : ↑(F.obj b)}
  (h : (F.map f).toFunctor.obj ((F.map (CategoryTheory.CategoryStruct.id a)).toFunctor.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.id a) f).hom.toNatTrans.app X) h =
    CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom).toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.map ((F.mapId a).inv.toNatTrans.app X)) h)
-- Mathlib.AlgebraicGeometry.Scheme
/-- Schemes are a full subcategory of locally ringed spaces.
 -/
AlgebraicGeometry.Scheme.instCategory : CategoryTheory.Category.{u_1, u_1 + 1} AlgebraicGeometry.Scheme
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.zoom.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α → RBTree.RBNode.Path α → Sort u_2) →
    (x : RBTree.RBNode α) →
      (x_1 : RBTree.RBNode.Path α) →
        ((path : RBTree.RBNode.Path α) → motive RBTree.RBNode.nil path) →
          ((c : RBTree.RBColor) →
              (a : RBTree.RBNode α) →
                (y : α) →
                  (b : RBTree.RBNode α) → (path : RBTree.RBNode.Path α) → motive (RBTree.RBNode.node c a y b) path) →
            motive x x_1
-- Mathlib.Order.Category.FinBddDistLat
/-- The category of finite distributive lattices with bounded lattice morphisms.  -/
FinBddDistLat : Type (u_1 + 1)
-- Mathlib.Topology.MetricSpace.HolderNorm
/-- See also `memHolder_const` for the version with the spelling `fun _ ↦ c`.  -/
memHolder_const : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {r : NNReal} {c : Y},
  MemHolder r (Function.const X c)
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.OplaxLeftLinear.δₗ_naturality_left_assoc : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'} [self : F.OplaxLeftLinear C] {c c' : C}
  (f : c ⟶ c') (d : D) {Z : D'}
  (h : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c' (F.obj d) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (F.map (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f d))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxLeftLinear.δₗ F c' d) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxLeftLinear.δₗ F c d)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f (F.obj d)) h)
-- Mathlib.Algebra.Order.Group.Defs
neg_nonpos_of_nonneg : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a : α}, 0 ≤ a → -a ≤ 0
-- Mathlib.Data.Holor
/-- Drop the first elements of a `HolorIndex`.  -/
HolorIndex.drop : {ds₂ ds₁ : List ℕ} → HolorIndex (ds₁ ++ ds₂) → HolorIndex ds₂
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.mul_neg : ∀ {R : Type u_3} [inst : Ring R] (a b : R), a * -b = -(a * b)
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.op_mono_of_epi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : C} (f : B ⟶ A) [CategoryTheory.Epi f],
  CategoryTheory.Mono f.op
-- Mathlib.Order.MinMax
min_le_min_left : ∀ {α : Type u} [inst : LinearOrder α] {a b : α} (c : α), b ≤ a → min c b ≤ min c a
-- Lean.Parser.Term
/-- * `with_decl_name% id e` elaborates `e` in a context while changing the effective
  declaration name to `id`.
* `with_decl_name% ?id e` does the same, but resolves `id` as a new definition name
  (appending the current namespaces).
 -/
Lean.Parser.Term.withDeclName : Lean.Parser.Parser
-- Mathlib.Data.Multiset.Range
Multiset.range_le : ∀ {m n : ℕ}, Multiset.range m ≤ Multiset.range n ↔ m ≤ n
-- Mathlib.Topology.Algebra.Field
IsLocalMin.inv : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : Semifield β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] {f : α → β} {a : α}, IsLocalMin f a → (∀ᶠ (z : α) in nhds a, 0 < f z) → IsLocalMax f⁻¹ a
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_add_nsmul : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} {b : H} [inst_1 : AddMonoid G]
  [inst_2 : AddMonoid H] [AddConstMapClass F G H a b] (f : F) (x : G) (n : ℕ), f (x + n • a) = f x + n • b
-- Init.Control.Lawful.Instances
ExceptT.run.eq_1 : ∀ {ε : Type u} {m : Type u → Type v} {α : Type u} (x : ExceptT ε m α), x.run = x
-- Mathlib.Algebra.Order.Field.Power
Even.zpow_pos_iff : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a : α} {n : ℤ},
  Even n → n ≠ 0 → (0 < a ^ n ↔ a ≠ 0)
-- Mathlib.Order.Interval.Lex
NonemptyInterval.toLex_strictMono : ∀ {α : Type u_1} [inst : PartialOrder α], StrictMono ⇑toLex
-- Mathlib.Probability.ConditionalProbability
ProbabilityTheory.cond_apply_self : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : Set Ω}, μ s ≠ 0 → μ s ≠ ⊤ → μ[s | s] = 1
-- Mathlib.Algebra.Category.MonCat.Colimits
/-- The monoid homomorphism from a given monoid in the diagram to the colimit monoid.  -/
MonCat.Colimits.coconeMorphism : {J : Type v} →
  [inst : CategoryTheory.Category.{u, v} J] →
    (F : CategoryTheory.Functor J MonCat) → (j : J) → F.obj j ⟶ MonCat.Colimits.colimit F
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
CategoryTheory.MonoidalCoherence.refl_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  CategoryTheory.MonoidalCoherence.iso = CategoryTheory.Iso.refl X
-- Mathlib.Topology.Order
IndiscreteTopology.nhds_eq : ∀ {α : Type u} [inst : TopologicalSpace α] [IndiscreteTopology α] (a : α), nhds a = ⊤
-- Mathlib.Logic.Denumerable
/-- If `α` is denumerable, then `α × α` and `α` are equivalent.  -/
Denumerable.pair : {α : Type u_1} → [Denumerable α] → α × α ≃ α
-- Lean.SubExpr
Lean.SubExpr.Pos.pushNthBindingBody : ℕ → Lean.SubExpr.Pos → Lean.SubExpr.Pos
-- Mathlib.CategoryTheory.Subobject.WellPowered
CategoryTheory.WellPowered.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u₁} C],
  autoParam (∀ (X : C), Small.{w, max u₁ v} (CategoryTheory.Subobject X))
      CategoryTheory.WellPowered.subobject_small._autoParam →
    CategoryTheory.WellPowered.{w, v, u₁} C
-- Mathlib.CategoryTheory.Subobject.Limits
/-- Postcomposing by an isomorphism gives an isomorphism between image subobjects.  -/
CategoryTheory.Limits.imageSubobjectCompIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      [CategoryTheory.Limits.HasEqualizers C] →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Limits.HasImage f] →
            {Y' : C} →
              (h : Y ⟶ Y') →
                [inst_3 : CategoryTheory.IsIso h] →
                  CategoryTheory.Subobject.underlying.obj
                      (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp f h)) ≅
                    CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f)
-- Mathlib.Data.Finset.Card
/-- $\#(s \setminus \{a\}) = \#s - 1$ if $a \in s$.  -/
Finset.card_erase_of_mem : ∀ {α : Type u_1} {s : Finset α} {a : α} [inst : DecidableEq α], a ∈ s → (s.erase a).card = s.card - 1
-- Mathlib.LinearAlgebra.BilinearForm.Basic
LinearMap.BilinForm.smul_left : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M} (a : R) (x y : M), (B (a • x)) y = a * (B x) y
-- Mathlib.GroupTheory.Congruence.Basic
Con.instIsCentralScalar : ∀ {α : Type u_4} {M : Type u_5} [inst : MulOneClass M] [inst_1 : SMul α M] [inst_2 : SMul αᵐᵒᵖ M]
  [inst_3 : IsScalarTower α M M] [inst_4 : IsScalarTower αᵐᵒᵖ M M] [IsCentralScalar α M] (c : Con M),
  IsCentralScalar α c.Quotient
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.term_add_constg : ∀ {α : Type u_1} [inst : AddCommGroup α] (n : ℤ) (x a k a' : α),
  a + k = a' → Mathlib.Tactic.Abel.termg n x a + k = Mathlib.Tactic.Abel.termg n x a'
-- Aesop.Rule
Aesop.instInhabitedUnfoldRule : Inhabited Aesop.UnfoldRule
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.pi.eq_1 : ∀ {ι : Type u_4} {M : ι → Type u_5} [inst : (i : ι) → MulOneClass (M i)] (I : Set ι) (S : (i : ι) → Submonoid (M i)),
  Submonoid.pi I S = { carrier := I.pi fun i => (S i).carrier, mul_mem' := ⋯, one_mem' := ⋯ }
-- Mathlib.Analysis.Normed.Group.Uniform
/-- **Alias** of the reverse direction of `antilipschitzWith_neg_iff`. -/
AntilipschitzWith.neg : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedAddCommGroup E] [inst_1 : PseudoEMetricSpace α] {K : NNReal}
  {f : α → E}, AntilipschitzWith K f → AntilipschitzWith K (-f)
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.get_sliceTo : ∀ {s : String.Slice} {p₀ p : s.Pos} {h : p ≤ p₀} {h' : p₀.sliceTo p h ≠ (s.sliceTo p₀).endPos},
  (p₀.sliceTo p h).get h' = p.get ⋯
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.contains.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (size : ℕ) (k' : α) (v : β k')
  (l r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.inner size k' v l r) =
    match compare k k' with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.contains k l
    | Ordering.gt => Std.DTreeMap.Internal.Impl.contains k r
    | Ordering.eq => true
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_insertIfNew_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {v : β}, (m.insertIfNew k v).contains k = true
-- Mathlib.Algebra.CharP.Algebra
/-- If `R →+* A` is injective, then `R` is of characteristic `p` if and only if `A` is also of
characteristic `p`. Similar to `RingHom.charZero_iff`.  -/
RingHom.charP_iff : ∀ {R : Type u_1} {A : Type u_2} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring A] (f : R →+* A),
  Function.Injective ⇑f → ∀ (p : ℕ), CharP R p ↔ CharP A p
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.chainBotCoeff_reflectionPerm_left : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  RootPairing.chainBotCoeff ((P.reflectionPerm i) i) j = RootPairing.chainTopCoeff i j
-- Mathlib.Analysis.Normed.Module.Basic
/-- The action of the original `NormedField` on `RestrictScalars 𝕜 𝕜' E`.
This is not an instance as it would be contrary to the purpose of `RestrictScalars`.
 -/
Module.RestrictScalars.normedSpaceOrig : {𝕜 : Type u_6} →
  {𝕜' : Type u_7} →
    {E : Type u_8} →
      [inst : NormedField 𝕜'] →
        [inst_1 : SeminormedAddCommGroup E] → [I : NormedSpace 𝕜' E] → NormedSpace 𝕜' (RestrictScalars 𝕜 𝕜' E)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.posPart_smul_of_nonpos : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [T2Space A] [StarModule ℝ A] {r : ℝ},
  r ≤ 0 → ∀ {a : A}, (r • a)⁺ = -r • a⁻
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
WeakFEPair.symm.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (P : WeakFEPair E),
  P.symm =
    { f := P.g, g := P.f, k := P.k, ε := P.ε⁻¹, f₀ := P.g₀, g₀ := P.f₀, hf_int := ⋯, hg_int := ⋯, hk := ⋯, hε := ⋯,
      h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ }
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.mapEquiv_symm : ∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] (e : α ≃ᵤ β),
  (UniformSpace.Completion.mapEquiv e).symm = UniformSpace.Completion.mapEquiv e.symm
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.lift_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj : ∀ {B : Type u₁} [inst : Quiver B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] (F : B ⥤q C) (a : B),
  (CategoryTheory.FreeBicategory.lift F).obj a = F.obj a
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.sPolynomial_decomposition' : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : Field R] {d : m.syn} {ι : Type u_3} {B : Finset ι}
  (g : ι → MvPolynomial σ R),
  (∀ b ∈ B, m.toSyn (m.degree (g b)) = d ∨ g b = 0) →
    m.toSyn (m.degree (∑ b ∈ B, g b)) < d →
      ∃ c, ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.locallyIntegrable_const : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} [MeasureTheory.IsLocallyFiniteMeasure μ] (c : E),
  MeasureTheory.LocallyIntegrable (fun x => c) μ
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- Multiplication on `HomotopyGroup N X x` is commutative for nontrivial `N`.
In particular, multiplication on `π_(n+2)` is commutative.  -/
HomotopyGroup.commGroup : {N : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace X] → {x : X} → [DecidableEq N] → [Nontrivial N] → CommGroup (HomotopyGroup N X x)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.single_left_inj : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {r : R} {m₁ m₂ : M},
  r ≠ 0 → (AddMonoidAlgebra.single m₁ r = AddMonoidAlgebra.single m₂ r ↔ m₁ = m₂)
-- Mathlib.CategoryTheory.Groupoid
CategoryTheory.IsGroupoid.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  autoParam (∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.IsIso f) CategoryTheory.IsGroupoid.all_isIso._autoParam →
    CategoryTheory.IsGroupoid C
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.comap_le_comap : ∀ {R : Type u_1} {S : Type u_2} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] {F : Type u_3}
  [inst_2 : FunLike F R S] (f : F) [inst_3 : NonUnitalRingHomClass F R S] {I J : TwoSidedIdeal S},
  I ≤ J → (TwoSidedIdeal.comap f) I ≤ (TwoSidedIdeal.comap f) J
-- ProofWidgets.Presentation.Expr
ProofWidgets.instRpcEncodableExprPresentations : Lean.Server.RpcEncodable ProofWidgets.ExprPresentations
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
Set.ordConnectedComponent_subset : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} {x : α}, s.ordConnectedComponent x ⊆ s
-- Mathlib.Analysis.Normed.Affine.Simplex
/-- A simplex is regular if it is equivalent under an isometry to any reindexing.  -/
Affine.Simplex.Regular : {R : Type u_1} →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : Ring R] →
        [inst_1 : SeminormedAddCommGroup V] →
          [inst_2 : PseudoMetricSpace P] →
            [inst_3 : Module R V] → [inst_4 : NormedAddTorsor V P] → {n : ℕ} → Affine.Simplex R P n → Prop
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coe_mem_one : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (x : R), (algebraMap R P) x ∈ 1
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.sat_and : ∀ {α : Type} {x y : Std.Tactic.BVDecide.BoolExpr α} {a : α → Bool},
  Std.Tactic.BVDecide.BoolExpr.Sat a x →
    Std.Tactic.BVDecide.BoolExpr.Sat a y →
      Std.Tactic.BVDecide.BoolExpr.Sat a (Std.Tactic.BVDecide.BoolExpr.gate Std.Tactic.BVDecide.Gate.and x y)
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
/-- Synonym for the constructor of `Hom₂` where the 1-morphisms `f` and `g` lie in `C`, and not
given in the form `f'.hom`, `g'.hom` for some `f' g' : InducedBicategory.Hom _ _`.  -/
CategoryTheory.Bicategory.InducedBicategory.mkHom₂ : {B : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Bicategory C] →
      {F : B → C} →
        {a b : CategoryTheory.Bicategory.InducedBicategory C F} →
          {f g : F a ⟶ F b} →
            (f ⟶ g) →
              (CategoryTheory.Bicategory.InducedBicategory.mkHom f ⟶
                CategoryTheory.Bicategory.InducedBicategory.mkHom g)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₁.HomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono φ h).iso = h.iso
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
/-- Bijection between a subsemigroup `H` and its opposite.  -/
Subsemigroup.equivOp : {M : Type u_2} → [inst : Mul M] → (H : Subsemigroup M) → ↥H ≃ ↥H.op
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- **Alias** of `LinearMap.IsRefl.eq_iff`. -/
LinearMap.IsRefl.ortho_comm : ∀ {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : CommSemiring R₁] [inst_4 : AddCommMonoid M₁] [inst_5 : Module R₁ M₁]
  {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M}, B.IsRefl → ∀ {x y : M₁}, (B x) y = 0 ↔ (B y) x = 0
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.mapCyclesIso_inv_naturality_assoc : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S₁.HasLeftHomology]
  [inst_6 : S₂.HasLeftHomology] [inst_7 : F.PreservesLeftHomologyOf S₁] [inst_8 : F.PreservesLeftHomologyOf S₂] {Z : D}
  (h : (S₂.map F).cycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.cyclesMap φ))
      (CategoryTheory.CategoryStruct.comp (S₂.mapCyclesIso F).inv h) =
    CategoryTheory.CategoryStruct.comp (S₁.mapCyclesIso F).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap (F.mapShortComplex.map φ)) h)
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.IsCoseparating.isCodetecting : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.ObjectProperty C}
  [CategoryTheory.Balanced C], P.IsCoseparating → P.IsCodetecting
-- Std.Data.DTreeMap.Internal.Operations
/-- Slower version of `insertMax` which can be used in the absence of balance information but
still assumes the preconditions of `insertMax`, otherwise might panic.
 -/
Std.DTreeMap.Internal.Impl.insertMax! : {α : Type u} → {β : α → Type v} → (k : α) → β k → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.pow : ∀ {α : Type u_1} {𝕜 : Type u_14} {𝕜' : Type u_15} [inst : NormedField 𝕜] [inst_1 : NormedField 𝕜'] {l : Filter α}
  {f : α → 𝕜} {g : α → 𝕜'}, f =Θ[l] g → ∀ (n : ℕ), (fun x => f x ^ n) =Θ[l] fun x => g x ^ n
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
_private.Mathlib.NumberTheory.NumberField.Completion.FinitePlace.0.NumberField.HeightOneSpectrum.termKv : Lean.ParserDescr
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.Subcomplex.mem_carrier`. -/
Topology.CWComplex.Subcomplex.mem_carrier : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  {E : Topology.RelCWComplex.Subcomplex C} {x : X}, x ∈ E.carrier ↔ x ∈ ↑E
-- Mathlib.NumberTheory.GaussSum
/-- If the square of the Gauss sum of a quadratic character is `χ(-1) * #R`,
then we get, for all `n : ℕ`, the relation `(χ(-1) * #R) ^ (p^n/2) = χ(p^n)`,
where `p` is the (odd) characteristic of the target ring `R'`.
This version can be used when `R` is not a field, e.g., `ℤ/8ℤ`.  -/
Char.card_pow_char_pow : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Fintype R] {R' : Type v} [inst_2 : CommRing R'] [IsDomain R']
  {χ : MulChar R R'},
  χ.IsQuadratic →
    ∀ (ψ : AddChar R R') (p n : ℕ) [fp : Fact (Nat.Prime p)] [hch : CharP R' p],
      IsUnit ↑p →
        p ≠ 2 → gaussSum χ ψ ^ 2 = χ (-1) * ↑(Fintype.card R) → (χ (-1) * ↑(Fintype.card R)) ^ (p ^ n / 2) = χ (↑p ^ n)
-- Mathlib.Data.Analysis.Filter
instInhabitedCFilter : {α : Type u_1} → [Inhabited α] → [inst : SemilatticeInf α] → Inhabited (CFilter α α)
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.commAlgEquiv_single_one_single : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Monoid M] [inst_4 : Monoid N] (m : M),
  (MonoidAlgebra.commAlgEquiv R) (MonoidAlgebra.single 1 (MonoidAlgebra.single m 1)) = MonoidAlgebra.single m 1
-- Mathlib.Tactic.ClickSuggestions.Util
/-- Print a premise using message data.  -/
Mathlib.Tactic.ClickSuggestions.Premise.toMessageData : Mathlib.Tactic.ClickSuggestions.Premise → Lean.MessageData
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
/-- A continuous linear map between Banach spaces has a continuous left inverse if it is injective,
has closed range and its range has a closed complement.  -/
ContinuousLinearMap.HasLeftInverse.of_injective_of_isClosed_range_of_closedComplement_range : ∀ {R : Type u_7} {E : Type u_8} {F : Type u_9} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace R E] [CompleteSpace E] [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace R F]
  [CompleteSpace F] {f : E →L[R] F},
  Function.Injective ⇑f → IsClosed (Set.range ⇑f) → (↑f).range.ClosedComplemented → f.HasLeftInverse
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
Set.ordConnectedSection_subset : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α}, s.ordConnectedSection ⊆ s
-- Mathlib.Data.List.GetD
List.getD_replicate : ∀ {α : Type u} (x : α) {y : α} {i n : ℕ}, i < n → (List.replicate n x).getD i y = x
-- Mathlib.Data.FunLike.Group
FunLike.subtractionCommMonoid.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Zero F]
  [inst_3 : SMul ℕ F] [inst_4 : Neg F] [inst_5 : Sub F] [inst_6 : SMul ℤ F] [inst_7 : SubtractionCommMonoid β]
  [inst_8 : IsZeroApply F α β] [inst_9 : IsAddApply F α β] [inst_10 : IsNegApply F α β] [inst_11 : IsSubApply F α β]
  [inst_12 : IsSMulApply ℕ F α β] [inst_13 : IsSMulApply ℤ F α β],
  FunLike.subtractionCommMonoid = Function.Injective.subtractionCommMonoid (fun f => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Init.Data.Int.LemmasAux
Int.toNat_sub_of_le : ∀ {a b : ℤ}, b ≤ a → ↑(a - b).toNat = a - b
-- Mathlib.Topology.MetricSpace.IsometricSMul
isometry_inv : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G],
  Isometry Inv.inv
-- Mathlib.CategoryTheory.MorphismProperty.FunctorCategory
CategoryTheory.MorphismProperty.IsStableUnderColimitsOfShape.functorCategory : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {K : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} K] [W.IsStableUnderColimitsOfShape K] (J : Type u'')
  [inst_3 : CategoryTheory.Category.{v'', u''} J] [CategoryTheory.Limits.HasColimitsOfShape K C],
  (W.functorCategory J).IsStableUnderColimitsOfShape K