mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.comp_assoc : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_10} [inst : MulOne M] [inst_1 : MulOne N] [inst_2 : MulOne P]
  [inst_3 : MulOne Q] (f : M →* N) (g : N →* P) (h : P →* Q), (h.comp g).comp f = h.comp (g.comp f)
-- Init.Data.Int.Order
Int.lt_add_of_sub_left_lt : ∀ {a b c : ℤ}, a - b < c → a < b + c
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.instMulRightMono : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α], MulRightMono (Finset α)
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitSphere.coe_one : ∀ {𝕜 : Type u_1} [inst : SeminormedRing 𝕜] [inst_1 : NormMulClass 𝕜] [inst_2 : NormOneClass 𝕜], ↑1 = 1
-- Init.Data.UInt.Lemmas
UInt64.ofBitVec_ofFin : ∀ (n : Fin (2 ^ 64)), { toBitVec := { toFin := n } } = UInt64.ofFin n
-- Mathlib.Data.Num.Lemmas
PosNum.succ.eq_1 : PosNum.one.succ = PosNum.one.bit0
-- Std.Data.HashSet.Lemmas
Std.HashSet.mem_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {f : α → Bool}
  {k : α}, k ∈ Std.HashSet.filter f m ↔ ∃ (h : k ∈ m), f (m.get k h) = true
-- Mathlib.Data.Num.Bitwise
SNum.instAdd : Add SNum
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.GrothendieckTopology.Plus.toPlus_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD]
  [inst_3 :
    ∀ {X : C} (S : J.Cover X),
      CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
        (CategoryTheory.forget D)]
  [inst_4 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_5 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} (S : J.Cover X) (x : CategoryTheory.Meq P S) (I : S.Arrow),
  (CategoryTheory.ConcreteCategory.hom ((J.toPlus P).app (Opposite.op I.Y))) (↑x I) =
    (CategoryTheory.ConcreteCategory.hom ((J.plusObj P).map I.f.op)) (CategoryTheory.GrothendieckTopology.Plus.mk x)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instCategory : {k : Type u} →
  {G : Type v} →
    [inst : Semiring k] → [inst_1 : Monoid G] → CategoryTheory.Category.{w, max (max (w + 1) v) u} (Rep.{w, u, v} k G)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.affineOpensRestrict_symm_apply_coe : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (V : { V // ↑V ≤ U }),
  ↑((AlgebraicGeometry.affineOpensRestrict U).symm V) = (TopologicalSpace.Opens.map U.ι.base).obj ↑↑V
-- Mathlib.Algebra.Order.Group.Unbundled.Int
Int.abs_sign_of_ne_zero : ∀ {z : ℤ}, z ≠ 0 → |z.sign| = 1
-- Init.Data.Vector.Lemmas
Vector.getD_getElem? : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} {d : α}, xs[i]?.getD d = if p : i < n then xs[i] else d
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.instUniqueHomStar : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : CategoryTheory.WithInitial C} → Unique (CategoryTheory.WithInitial.star ⟶ X)
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.commutator_eq_bot_iff_le_centralizer : ∀ {G : Type u_1} [inst : Group G] {H₁ H₂ : Subgroup G}, ⁅H₁, H₂⁆ = ⊥ ↔ H₁ ≤ Subgroup.centralizer ↑H₂
-- Mathlib.Data.Matrix.Mul
single_one_dotProduct : ∀ {n : Type u_3} {α : Type v} [inst : Fintype n] [inst_1 : NonAssocSemiring α] [inst_2 : DecidableEq n] (i : n)
  (v : n → α), Pi.single i 1 ⬝ᵥ v = v i
-- Mathlib.Algebra.Algebra.Pi
/-- A special case of `Pi.algebra` for non-dependent types. Lean struggles to elaborate
definitions elsewhere in the library without this.  -/
Function.algebra : {R : Type u_1} →
  (ι : Type u_2) → (A : Type u_3) → [inst : CommSemiring R] → [inst_1 : Semiring A] → [Algebra R A] → Algebra R (ι → A)
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.splits_iff_comp_splits_of_degree_eq_one : ∀ {R : Type u_1} [inst : Field R] {f g : Polynomial R}, g.degree = 1 → (f.Splits ↔ (f.comp g).Splits)
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- Right identity of the `L^p` product as a linear isometric equivalence.  -/
LinearIsometryEquiv.withLpProdUnique : (p : ENNReal) →
  (𝕜 : Type u_1) →
    (α : Type u_2) →
      (β : Type u_3) →
        [hp : Fact (1 ≤ p)] →
          [inst : Semiring 𝕜] →
            [inst_1 : SeminormedAddCommGroup α] →
              [inst_2 : Module 𝕜 α] →
                [inst_3 : SeminormedAddCommGroup β] → [inst_4 : Module 𝕜 β] → [Unique β] → WithLp p (α × β) ≃ₗᵢ[𝕜] α
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
CategoryTheory.Equivalence.sheafCongrPrecoherent_inverse_obj_obj_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Precoherent C] (A : Type u_3)
  [inst_3 : CategoryTheory.Category.{v_3, u_3} A] (e : C ≌ D)
  (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology D) A) {X_1 Y : Cᵒᵖ} (f : X_1 ⟶ Y),
  ((CategoryTheory.Equivalence.sheafCongrPrecoherent A e).inverse.obj X).obj.map f = X.obj.map (e.functor.map f.unop).op
-- Mathlib.LinearAlgebra.Dual.Lemmas
/-- **Alias** of `LinearMap.id_nondegenerate`. -/
LinearMap.dualPairing_nondegenerate : ∀ {K : Type u_1} {V : Type u_2} [inst : CommSemiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [Module.Projective K V], LinearMap.id.Nondegenerate
-- Lean.Elab.PreDefinition.PartialFixpoint.Induction
/-- `maskArray mask xs` keeps those `x` where the corresponding entry in `mask` is `true`  -/
_private.Lean.Elab.PreDefinition.PartialFixpoint.Induction.0.Lean.Elab.PartialFixpoint.maskArray : {α : Type u_1} → Array Bool → Array α → Array α
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.DSimpArgs.mk : Array Lean.FVarId → Bool → Lean.Elab.Tactic.Grind.DSimpArgs
-- Mathlib.Order.Filter.Basic
Filter.EventuallyLE.le_inf : ∀ {α : Type u} {β : Type v} [inst : SemilatticeInf β] {l : Filter α} {f g h : α → β},
  h ≤ᶠ[l] f → h ≤ᶠ[l] g → h ≤ᶠ[l] f ⊓ g
-- Init.Data.SInt.Lemmas
ISize.ofIntTruncate_int32ToInt : ∀ (x : Int32), ISize.ofIntClamp x.toInt = x.toISize
-- Batteries.Data.Fin.Coding
Fin.decodePi_encodePi : ∀ {n : ℕ} (f : Fin n → ℕ) (x : (i : Fin n) → Fin (f i)), Fin.decodePi f (Fin.encodePi f x) = x
-- Mathlib.Data.Finsupp.Single
Finsupp.support_subset_singleton' : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {f : α →₀ M} {a : α}, f.support ⊆ {a} ↔ ∃ b, f = fun₀ | a => b
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the oriented angle between three points is `π / 2`, so is the unoriented angle.  -/
EuclideanGeometry.angle_eq_pi_div_two_of_oangle_eq_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) → EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2
-- Mathlib.Topology.Algebra.GroupCompletion
/-- Extension to the completion of a continuous group hom.  -/
AddMonoidHom.extension : {α : Type u_3} →
  {β : Type u_4} →
    [inst : UniformSpace α] →
      [inst_1 : AddGroup α] →
        [inst_2 : IsUniformAddGroup α] →
          [inst_3 : UniformSpace β] →
            [inst_4 : AddGroup β] →
              [IsUniformAddGroup β] →
                [CompleteSpace β] → [T0Space β] → (f : α →+ β) → Continuous ⇑f → UniformSpace.Completion α →+ β
-- Mathlib.RingTheory.Extension.ExtendScalars
Algebra.Extension.h1CotangentExtendScalarsEquiv_toLinearMap : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S),
  ↑P.h1CotangentExtendScalarsEquiv =
    Algebra.Extension.H1Cotangent.map
      (Algebra.Extension.Hom.ofAlgHom (Algebra.ofId P.Ring (Algebra.Generators.self P.Ring S).Ring) ⋯)
-- Mathlib.Analysis.InnerProductSpace.Dual
InnerProductSpace.ext_inner_right_basis : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} {x y : E} (b : Module.Basis ι 𝕜 E), (∀ (i : ι), inner 𝕜 x (b i) = inner 𝕜 y (b i)) → x = y
-- Init.Data.Int.Order
Int.zero_le_neg_iff : ∀ {a : ℤ}, 0 ≤ -a ↔ a ≤ 0
-- Mathlib.CategoryTheory.Action.Basic
/-- The natural isomorphism from the composition of restrictions along homomorphisms
to the restriction along the composition of homomorphism.
 -/
Action.resComp : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_3} →
      {H : Type u_4} →
        {K : Type u_5} →
          [inst_1 : Monoid G] →
            [inst_2 : Monoid H] →
              [inst_3 : Monoid K] →
                (f : G →* H) → (g : H →* K) → (Action.res V g).comp (Action.res V f) ≅ Action.res V (g.comp f)
-- Mathlib.Topology.Algebra.Group.Basic
continuousAt_zsmul : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] (x : G) (z : ℤ),
  ContinuousAt (fun x => z • x) x
-- Mathlib.MeasureTheory.Group.FoelnerFilter
IsFoelner.mono : ∀ {G : Type u_1} {X : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : Group G]
  [inst_2 : MulAction G X] {ι : Type u_3} {l : Filter ι} {F : ι → Set X} {l' : Filter ι},
  IsFoelner G μ l F → l' ≤ l → IsFoelner G μ l' F
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.map_eq : ∀ {X Y : TopCat} (f g : X ⟶ Y), f = g → TopologicalSpace.Opens.map f = TopologicalSpace.Opens.map g
-- Aesop.Tree.Data
Aesop.GoalId.dummy : Aesop.GoalId
-- Mathlib.RingTheory.Smooth.Basic
/-- Formally smooth extensions have isomorphic `H¹(L_P)`.  -/
Algebra.Extension.H1Cotangent.equivOfFormallySmooth : {R : Type u} →
  {A : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing A] →
        [inst_2 : Algebra R A] →
          (P₁ : Algebra.Extension R A) →
            (P₂ : Algebra.Extension R A) →
              [Algebra.FormallySmooth R P₁.Ring] →
                [Algebra.FormallySmooth R P₂.Ring] → P₁.H1Cotangent ≃ₗ[A] P₂.H1Cotangent
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
/-- The algebra norm underlying an multiplicative algebra norm.  -/
MulAlgebraNorm.toAlgebraNorm : {R : outParam (Type u_1)} →
  {S : outParam (Type u_2)} →
    [inst : SeminormedCommRing R] → [inst_1 : Ring S] → [inst_2 : Algebra R S] → MulAlgebraNorm R S → AlgebraNorm R S
-- Mathlib.Topology.Sheaves.Stalks
/-- The morphism `ℱ_{f x} ⟶ (f⁻¹ℱ)ₓ` that factors through `(f_*f⁻¹ℱ)_{f x}`.  -/
TopCat.Presheaf.stalkPullbackHom : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasColimits C] →
      {X Y : TopCat} →
        (f : X ⟶ Y) →
          (F : TopCat.Presheaf C Y) →
            (x : ↑X) →
              F.stalk ((CategoryTheory.ConcreteCategory.hom f) x) ⟶ ((TopCat.Presheaf.pullback C f).obj F).stalk x
-- Lean.Meta.Tactic.Grind.RegisterCommand
Lean.Parser.Command.registerGrindAttr : Lean.ParserDescr
-- Std.Do.Triple.SpecLemmas
List.Cursor.prefix_at : ∀ {α : Type u_1} {n : ℕ} (l : List α), (List.Cursor.at l n).prefix = List.take n l
-- Init.GrindInstances.ToInt
Lean.Grind.instMulInt32SintOfNatNat : Lean.Grind.ToInt.Mul Int32 (Lean.Grind.IntInterval.sint 32)
-- Init.Data.Iterators.Combinators.Monadic.Take
Std.Iterators.Types.Take.Rel.eq_1 : ∀ {α β : Type w} (m : Type w → Type w') [inst : Monad m] [inst_1 : Std.Iterator α m β]
  [inst_2 : Std.Iterators.Productive α m],
  Std.Iterators.Types.Take.Rel m =
    if x : Std.Iterators.Finite α m then
      InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Finite.Rel) fun it =>
        (it.internalState.countdown, it.internalState.inner.finitelyManySteps)
    else
      InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel) fun it =>
        (it.internalState.countdown, it.internalState.inner.finitelyManySkips)
-- Lean.Elab.Tactic.Basic
_private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.expandEval : Lean.Syntax →
  Lean.Elab.Tactic.SavedState →
    List (Lean.KeyedDeclsAttribute.AttributeEntry Lean.Macro) →
      List (Lean.KeyedDeclsAttribute.AttributeEntry Lean.Elab.Tactic.Tactic) →
        Array Lean.Elab.Tactic.EvalTacticFailure → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.commute_of_mul_eq_zero : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] [inst_1 : StarRing R] {a b : R},
  IsSelfAdjoint a → IsSelfAdjoint b → a * b = 0 → Commute a b
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instSub : {α : Type u_1} → [Sub α] → Sub αᵒᵈ
-- Mathlib.Algebra.Order.Archimedean.Basic
MulArchimedean.comap : ∀ {G : Type u_1} {M : Type u_2} [inst : CommMonoid G] [inst_1 : LinearOrder G] [inst_2 : CommMonoid M]
  [inst_3 : PartialOrder M] [MulArchimedean M] (f : G →* M), StrictMono ⇑f → MulArchimedean G
-- Std.Http.Data.Body.Full
_private.Std.Http.Data.Body.Full.0.Std.Http.Body.Full.mk.sizeOf_spec : ∀ (state : Std.Mutex (Option ByteArray)), sizeOf { state := state } = 1 + sizeOf state
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- Copy a subsemigroup replacing `carrier` with a set that is equal to it.  -/
Subsemigroup.copy : {M : Type u_1} → [inst : Mul M] → (S : Subsemigroup M) → (s : Set M) → s = ↑S → Subsemigroup M
-- Init.Control.Basic
MonadControl.mk : {m : semiOutParam (Type u → Type v)} →
  {n : Type u → Type w} →
    (stM : Type u → Type u) →
      ({α : Type u} → (({β : Type u} → n β → m (stM β)) → m α) → n α) →
        ({α : Type u} → m (stM α) → n α) → MonadControl m n
-- Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Dynamics.dynEntourage_mono : ∀ {X : Type u_1} {T : X → X} {U V : SetRel X X} {m n : ℕ},
  U ⊆ V → m ≤ n → Dynamics.dynEntourage T U n ⊆ Dynamics.dynEntourage T V m
-- Mathlib.Analysis.Calculus.LHopital
/-- L'Hôpital's rule for approaching a real from the right, `HasDerivAt` version  -/
HasDerivAt.lhopital_zero_nhdsGT : ∀ {a : ℝ} {l : Filter ℝ} {f f' g g' : ℝ → ℝ},
  (∀ᶠ (x : ℝ) in nhdsWithin a (Set.Ioi a), HasDerivAt f (f' x) x) →
    (∀ᶠ (x : ℝ) in nhdsWithin a (Set.Ioi a), HasDerivAt g (g' x) x) →
      (∀ᶠ (x : ℝ) in nhdsWithin a (Set.Ioi a), g' x ≠ 0) →
        Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds 0) →
          Filter.Tendsto g (nhdsWithin a (Set.Ioi a)) (nhds 0) →
            Filter.Tendsto (fun x => f' x / g' x) (nhdsWithin a (Set.Ioi a)) l →
              Filter.Tendsto (fun x => f x / g x) (nhdsWithin a (Set.Ioi a)) l
-- Mathlib.NumberTheory.FrobeniusNumber
Nat.setGcd_insert_of_dvd : ∀ {s : Set ℕ} {n : ℕ}, Nat.setGcd s ∣ n → Nat.setGcd (insert n s) = Nat.setGcd s
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.isoApp_left_unitor : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {X : (i : I) → C i} {i : I},
  CategoryTheory.Pi.isoApp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X) i =
    CategoryTheory.MonoidalCategoryStruct.leftUnitor (X i)
-- Mathlib.RingTheory.MvPowerSeries.Restricted
MvPowerSeries.isRestricted_one : ∀ {R : Type u_1} [inst : NormedRing R] {σ : Type u_2} (c : σ → ℝ), MvPowerSeries.IsRestricted c 1
-- Init.Core
/-- Notation type class for the strict subset relation `⊂`.  -/
HasSSubset : Type u → Type u
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.denom_ne_zero_of_im : ∀ (g : GL (Fin 2) ℝ) {z : ℂ}, z.im ≠ 0 → UpperHalfPlane.denom g z ≠ 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.fin3_def : ∀ {R : Type r} (P : Fin 3 → R), ![P 0, P 1, P 2] = P
-- Mathlib.Combinatorics.Quiver.Schreier
Quiver.SchreierGraph.equiv_symm_apply : ∀ (V : Type u_1) {M : Type u_2} [inst : SMul M V] {S : Type u_3} (ι : S → M) (self : Quiver.SchreierGraph V ι),
  (Quiver.SchreierGraph.equiv V ι).symm self = self.toVertex
-- Mathlib.Tactic.ClickSuggestions.GRewrite
Mathlib.Tactic.ClickSuggestions.instOrdGrwKey : Ord Mathlib.Tactic.ClickSuggestions.GrwKey
-- Mathlib.Algebra.CubicDiscriminant
Cubic.degree_of_b_eq_zero : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.a = 0 → P.b = 0 → P.toPoly.degree ≤ 1
-- Mathlib.Topology.UniformSpace.Pi
Pi.uniformSpace_eq : ∀ {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)],
  Pi.uniformSpace α = ⨅ i, UniformSpace.comap (Function.eval i) (U i)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.MVarErrorInfo.mk.sizeOf_spec : ∀ (mvarId : Lean.MVarId) (ref : Lean.Syntax) (kind : Lean.Elab.Term.MVarErrorKind),
  sizeOf { mvarId := mvarId, ref := ref, kind := kind } = 1 + sizeOf mvarId + sizeOf ref + sizeOf kind
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.instNontrivialOfNonempty : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] [Nontrivial k] [Nonempty G], Nontrivial (SkewMonoidAlgebra k G)
-- Mathlib.Analysis.SpecialFunctions.Log.InvLog
Real.not_continuousAt_log_log_one : ¬ContinuousAt (fun x => Real.log (Real.log x)) 1
-- Lean.Parser.Command
Lean.Parser.Command.withWeakNamespace.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'_id_comp : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ : B} (f : b₀ ⟶ b₁),
  F.mapComp' (CategoryTheory.CategoryStruct.id b₀) f f ⋯ =
    (CategoryTheory.Bicategory.leftUnitor (F.map f)).symm ≪≫
      CategoryTheory.Bicategory.whiskerRightIso (F.mapId b₀).symm (F.map f)
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.setIntegral_congr_set : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  {s t : Set X} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G]
  {B : E →L[ℝ] F →L[ℝ] G},
  MeasurableSet s → MeasurableSet t → s =ᵐ[μ.variation] t → ∫ᵛ (x : X) in s, f x ∂[B; μ] = ∫ᵛ (x : X) in t, f x ∂[B; μ]
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.contains : {α : Type u_1} → {β : Type u_2} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.PersistentHashMap α β → α → Bool
-- Lean.Elab.Tactic.Omega.OmegaM
Lean.Elab.Tactic.Omega.Context.mk.injEq : ∀ (cfg cfg_1 : Lean.Meta.Omega.OmegaConfig), ({ cfg := cfg } = { cfg := cfg_1 }) = (cfg = cfg_1)
-- Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
BoundedContinuousFunction.lintegral_le_edist_mul : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] (f : BoundedContinuousFunction X NNReal)
  (μ : MeasureTheory.Measure X), ∫⁻ (x : X), ↑(f x) ∂μ ≤ edist 0 f * μ Set.univ
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.isTrivial_of_nilpotencyLength_le_one : ∀ (L : Type v) (M : Type w) [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M]
  [LieModule.IsNilpotent L M], LieModule.nilpotencyLength L M ≤ 1 → LieModule.IsTrivial L M
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.toSubmodule_orderEmbedding_apply : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (self : LieSubmodule R L M),
  (LieSubmodule.toSubmodule_orderEmbedding R L M) self = ↑self
-- Mathlib.Algebra.Category.MonCat.Limits
AddCommMonCat.forget_createsLimits.eq_1 : AddCommMonCat.forget_createsLimits = AddCommMonCat.forget_createsLimitsOfSize
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.Integrable.sub_vectorMeasure : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] {f : X → E} {μ ν : MeasureTheory.VectorMeasure X F},
  μ.Integrable f → ν.Integrable f → (μ - ν).Integrable f
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_neg_eq_zero : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] {x : R},
  Int.fract (-x) = 0 ↔ Int.fract x = 0
-- Init.Data.Array.Erase
_private.Init.Data.Array.Erase.0.Array.eraseP_filterMap.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → ((y : β) → motive (some y)) → (Unit → motive none) → motive x
-- Mathlib.Data.ENat.Basic
ENat.top_sub_ofNat : ∀ (a : ℕ) [inst : a.AtLeastTwo], ⊤ - OfNat.ofNat a = ⊤
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.closedComplemented_bot : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M], ⊥.ClosedComplemented
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.includeRight_surjective : ∀ {R : Type u_1} {S : Type u_3} (T : Type u_4) [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S]
  [inst_3 : Ring T] [inst_4 : Algebra R T],
  Function.Surjective ⇑(algebraMap R S) → Function.Surjective ⇑Algebra.TensorProduct.includeRight
-- Mathlib.LinearAlgebra.AffineSpace.Centroid
/-- The centroid of a single point.  -/
Finset.centroid_singleton : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} (p : ι → P) (i : ι), Finset.centroid k {i} p = p i
-- Init.Data.Array.DecidableEq
Array.isEqv_iff_rel : ∀ {α : Type u_1} {xs ys : Array α} {r : α → α → Bool},
  xs.isEqv ys r = true ↔ ∃ (h : xs.size = ys.size), ∀ (i : ℕ) (h' : i < xs.size), r xs[i] ys[i] = true
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.weightHom_injective : ∀ {ι : 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),
  Function.Injective ⇑(RootPairing.Equiv.weightHom P)
-- Mathlib.CategoryTheory.Monad.Adjunction
/-- A right adjoint functor `R : D ⥤ C` is *monadic* if the comparison functor `Monad.comparison R`
from `D` to the category of Eilenberg-Moore algebras for the adjunction is an equivalence.
 -/
CategoryTheory.MonadicRightAdjoint : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor D C → Type (max (max (max u₁ u₂) v₁) v₂)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.spanCompIso_hom_app_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z),
  (CategoryTheory.Limits.spanCompIso F f g).hom.app CategoryTheory.Limits.WalkingSpan.right =
    CategoryTheory.CategoryStruct.id
      (((CategoryTheory.Limits.span f g).comp F).obj CategoryTheory.Limits.WalkingSpan.right)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_hom_comp_ι_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) [inst_2 : S.HasRightHomology] {Z : C} (h_1 : h.Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.rightHomologyIso.hom (CategoryTheory.CategoryStruct.comp h.ι h_1) =
    CategoryTheory.CategoryStruct.comp S.rightHomologyι (CategoryTheory.CategoryStruct.comp h.opcyclesIso.hom h_1)
-- Mathlib.Combinatorics.Matroid.Minor.Contract
/-- **Alias** of `Matroid.contract_delete_sdiff`. -/
Matroid.contract_delete_diff : ∀ {α : Type u_1} (M : Matroid α) (C D : Set α), (M.contract C).delete D = (M.contract C).delete (D \ C)
-- Mathlib.Data.List.OffDiag
/-- `List.offDiag l` is the product `l.product l` with the diagonal removed.  -/
List.offDiag : {α : Type u_1} → List α → List (α × α)
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_cast_Ioo : ∀ {m n : ℕ} (h : m = n) (i j : Fin n), Fin.cast h ⁻¹' Set.Ioo i j = Set.Ioo (Fin.cast ⋯ i) (Fin.cast ⋯ j)
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
_private.Mathlib.LinearAlgebra.Matrix.FixedDetMatrices.0.FixedDetMatrices.A_a_ne_zero : ∀ {m : ℤ} {A : FixedDetMatrix (Fin 2) ℤ m}, ↑A 1 0 = 0 → m ≠ 0 → ↑A 0 0 ≠ 0