mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Basic
/-- `StrongHomClass L F M N` states that `F` is a type of `L`-homomorphisms which preserve
relations in both directions.  -/
FirstOrder.Language.StrongHomClass : (L : outParam FirstOrder.Language) →
  (F : Type u_3) →
    (M : outParam (Type u_4)) → (N : outParam (Type u_5)) → [FunLike F M N] → [L.Structure M] → [L.Structure N] → Prop
-- Mathlib.NumberTheory.LSeries.Linearity
LSeries.term_sub : ∀ (f g : ℕ → ℂ) (s : ℂ), LSeries.term (f - g) s = LSeries.term f s - LSeries.term g s
-- Mathlib.Data.Subtype
Subtype.heq_iff_coe_heq : ∀ {α β : Sort u_4} {p : α → Prop} {q : β → Prop} {a : { x // p x }} {b : { y // q y }},
  α = β → p ≍ q → (a ≍ b ↔ ↑a ≍ ↑b)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
add_neg_le_iff_le_add : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddRightMono α] {a b c : α}, a + -b ≤ c ↔ a ≤ c + b
-- Mathlib.CategoryTheory.Monoidal.Internal.Module
/-- The category of internal monoid objects in `ModuleCat R`
is equivalent to the category of "native" bundled `R`-algebras.
 -/
ModuleCat.monModuleEquivalenceAlgebra : {R : Type u} → [inst : CommRing R] → CategoryTheory.Mon (ModuleCat R) ≌ AlgCat R
-- Mathlib.Logic.Encodable.Basic
/-- Explicit encoding function for `Sigma γ`  -/
Encodable.encodeSigma : {α : Type u_1} → {γ : α → Type u_3} → [Encodable α] → [(a : α) → Encodable (γ a)] → Sigma γ → ℕ
-- Mathlib.Analysis.Fourier.AddCircleMulti
UnitAddTorus.mFourier_zero : ∀ {d : Type u_1} [inst : Fintype d], UnitAddTorus.mFourier 0 = 1
-- Mathlib.Order.GaloisConnection.Defs
/-- A constructor for a Galois insertion with the trivial `choice` function.  -/
GaloisInsertion.monotoneIntro : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        {l : α → β} →
          {u : β → α} →
            Monotone u → Monotone l → (∀ (a : α), a ≤ u (l a)) → (∀ (b : β), l (u b) = b) → GaloisInsertion l u
-- Mathlib.Order.SuccPred.Relation
/-- For `m < n`, `(n, m)` is in the transitive closure of a relation `~` for `n ≠ m` if `i ~ pred i`
for all `i` between `n` and `m`.  -/
transGen_of_pred_of_gt : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] [IsPredArchimedean α] (r : α → α → Prop) {n m : α},
  (∀ i ∈ Set.Ioc m n, r i (Order.pred i)) → m < n → Relation.TransGen r n m
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- Transfer preservation of limits of shape along a natural isomorphism in the functor.  -/
CategoryTheory.Limits.preservesLimitsOfShape_of_natIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {F G : CategoryTheory.Functor C D} (h : F ≅ G)
  [CategoryTheory.Limits.PreservesLimitsOfShape J F], CategoryTheory.Limits.PreservesLimitsOfShape J G
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.val_smul_eq_evalₐ_smul : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (n : ℕ) (r : AdicCompletion I R) (x : M ⧸ I ^ n • ⊤), ↑r n • x = (AdicCompletion.evalₐ I n) r • x
-- Mathlib.Order.Monotone.Basic
/-- **Alias** of the reverse direction of `strictMonoOn_dual_iff`. -/
StrictMonoOn.dual : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictMonoOn f s → StrictMonoOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s
-- Mathlib.Algebra.Order.Algebra
isOrderedModule_iff_algebraMap_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : CommSemiring α] [inst_1 : PartialOrder α] [inst_2 : Semiring β]
  [inst_3 : PartialOrder β] [inst_4 : Algebra α β] [ZeroLEOneClass β] [PosMulMono β] [MulPosMono β],
  IsOrderedModule α β ↔ Monotone ⇑(algebraMap α β)
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
/-- Euler's integral for the `Γ` function (of a complex variable `s`), defined as
`∫ x in Ioi 0, exp (-x) * x ^ (s - 1)`.

See `Complex.GammaIntegral_convergent` for a proof of the convergence of the integral for
`0 < re s`.  -/
Complex.GammaIntegral : ℂ → ℂ
-- Init.Data.List.Find
List.IsInfix.findSome?_eq_none : ∀ {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α} {f : α → Option β},
  l₁ <:+: l₂ → List.findSome? f l₂ = none → List.findSome? f l₁ = none
-- Init.Data.Rat.Lemmas
Rat.floor_le : ∀ (a : ℚ), ↑a.floor ≤ a
-- Mathlib.Topology.UniformSpace.Defs
tendsto_swap_uniformity : ∀ {α : Type ua} [inst : UniformSpace α], Filter.Tendsto Prod.swap (uniformity α) (uniformity α)
-- Mathlib.Combinatorics.Derangements.Finite
numDerangements_zero : numDerangements 0 = 1
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.edges_nodup_of_support_nodup : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, p.support.Nodup → p.edges.Nodup
-- Mathlib.CategoryTheory.Sites.Subsheaf
/-- The sheafification of a subpresheaf as a subpresheaf.
Note that this is a sheaf only when the whole presheaf is a sheaf.  -/
CategoryTheory.Subfunctor.sheafify : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.GrothendieckTopology C →
      {F : CategoryTheory.Functor Cᵒᵖ (Type w)} → CategoryTheory.Subfunctor F → CategoryTheory.Subfunctor F
-- Init.Data.UInt.Lemmas
UInt16.add_right_neg : ∀ (a : UInt16), a + -a = 0
-- Mathlib.CategoryTheory.ComposableArrows.Basic
Fin.succFunctor_obj : ∀ (n : ℕ) (i : Fin n), (Fin.succFunctor n).obj i = i.succ
-- Mathlib.Logic.Equiv.Prod
/-- The product `Bool × α` is equivalent to `α ⊕ α`.  -/
Equiv.boolProdEquivSum : (α : Type u_9) → Bool × α ≃ α ⊕ α
-- Mathlib.Topology.Order
le_nhdsAdjoint_iff : ∀ {α : Type u_1} (a : α) (f : Filter α) (t : TopologicalSpace α),
  t ≤ nhdsAdjoint a f ↔ nhds a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → IsOpen {b}
-- Mathlib.Topology.Algebra.ConstMulAction
Prod.continuousConstVAdd : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : VAdd M α] [ContinuousConstVAdd M α]
  [inst_3 : TopologicalSpace β] [inst_4 : VAdd M β] [ContinuousConstVAdd M β], ContinuousConstVAdd M (α × β)
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.coe_mk : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Top α] [inst_2 : Min β] [inst_3 : Top β] (f : InfHom α β)
  (hf : f.toFun ⊤ = ⊤), ⇑{ toInfHom := f, map_top' := hf } = ⇑f
-- Mathlib.Data.Num.Bitwise
/-- `a.testBit n` is `true` iff the `n`-th bit (starting from the LSB) in the binary representation
of `a` is active. If the size of `a` is less than `n`, this evaluates to `false`.  -/
Num.testBit : Num → ℕ → Bool
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- The map `F.obj' i ⟶ G.obj' i` induced on `i`th objects by a morphism `F ⟶ G`
in `ComposableArrows C n` when `i` is a natural number such that `i ≤ n`.  -/
CategoryTheory.ComposableArrows.app' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {n : ℕ} →
      {F G : CategoryTheory.ComposableArrows C n} →
        (F ⟶ G) →
          (i : ℕ) → (hi : autoParam (i ≤ n) CategoryTheory.ComposableArrows.app'._auto_1) → F.obj' i hi ⟶ G.obj' i hi
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.mk.sizeOf_spec : ∀ {α : Type u} [inst : Group α] [inst_1 : SizeOf α] (toTopologicalSpace : TopologicalSpace α)
  (toIsTopologicalGroup : IsTopologicalGroup α),
  sizeOf { toTopologicalSpace := toTopologicalSpace, toIsTopologicalGroup := toIsTopologicalGroup } =
    1 + sizeOf toTopologicalSpace + sizeOf toIsTopologicalGroup
-- Mathlib.Algebra.Group.Even
Even.nsmul_right : ∀ {α : Type u_2} [inst : AddMonoid α] {a : α} (n : ℕ), Even a → Even (n • a)
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
/-- Second derivative of q-ary entropy.  -/
Real.deriv2_qaryEntropy : ∀ {q : ℕ} {p : ℝ}, deriv^[2] (Real.qaryEntropy q) p = -1 / (p * (1 - p))
-- Init.Data.Option.Monadic
Option.bindM.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Pure m] (f : α → m (Option β)),
  Option.bindM f none = pure none
-- Mathlib.Analysis.LocallyConvex.AbsConvex
zero_mem_absConvexHull : ∀ {𝕜 : Type u_1} {E : Type u_2} {s : Set E} [inst : SeminormedRing 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜 E] [Nonempty ↑s], 0 ∈ (absConvexHull 𝕜) s
-- Mathlib.Analysis.Calculus.FDeriv.Affine
ContinuousAffineMap.hasFDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E →ᴬ[𝕜] F)
  {x : E}, HasFDerivAt (⇑f) f.contLinear x
-- Mathlib.GroupTheory.GroupAction.Hom
/-- If actions of `M` and `N` on `α` commute,
then for `c : M`, `(c • · : α → α)` is an `N`-action homomorphism.  -/
SMulCommClass.toMulActionHom : {M : Type u_11} →
  (N : Type u_9) → (α : Type u_10) → [inst : SMul M α] → [inst_1 : SMul N α] → [SMulCommClass M N α] → M → α →ₑ[id] α
-- Init.Grind.ToInt
/-- The interval `[-2^(n-1), 2^(n-1))`.  -/
Lean.Grind.IntInterval.sint : ℕ → Lean.Grind.IntInterval
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.getVert_eq_end_iff : ∀ {V : Type u} {G : SimpleGraph V} {u w : V} {i : ℕ} {p : G.Walk u w},
  p.IsPath → i ≤ p.length → (p.getVert i = w ↔ i = p.length)
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.fundCocircuit_subset_insert_compl : ∀ {α : Type u_1} (M : Matroid α) (e : α) (B : Set α), M.fundCocircuit e B ⊆ insert e (M.E \ B)
-- Mathlib.CategoryTheory.Sites.LocalSite
CategoryTheory.GrothendieckTopology.IsLocalSite.instIsRightAdjointSheafCoconstantSheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] [inst_2 : J.IsLocalSite] (A : Type u')
  [inst_3 : CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  [inst_5 : CategoryTheory.Limits.HasProducts A] [CategoryTheory.HasWeakSheafify J A],
  (CategoryTheory.GrothendieckTopology.IsLocalSite.coconstantSheaf J A).IsRightAdjoint
-- Mathlib.GroupTheory.OrderOfElement
orderOf_apply_dvd_orderOf : ∀ {ι : Type u_6} {α : ι → Type u_7} [inst : (i : ι) → Monoid (α i)] {x : (i : ι) → α i} (i : ι),
  orderOf (x i) ∣ orderOf x
-- Lean.Elab.PatternVar
_private.Lean.Elab.PatternVar.0.Lean.Elab.Term.CollectPatternVars.getNextParam : Lean.Elab.Term.CollectPatternVars.Context → (Lean.Name × Lean.BinderInfo) × Lean.Elab.Term.CollectPatternVars.Context
-- Mathlib.RingTheory.Valuation.Extension
Valuation.HasExtension.mk : ∀ {R : Type u_1} {A : Type u_2} {ΓR : Type u_3} {ΓA : Type u_4} [inst : CommRing R] [inst_1 : Ring A]
  [inst_2 : LinearOrderedCommMonoidWithZero ΓR] [inst_3 : LinearOrderedCommMonoidWithZero ΓA] [inst_4 : Algebra R A]
  {vR : Valuation R ΓR} {vA : Valuation A ΓA}, vR.IsEquiv (Valuation.comap (algebraMap R A) vA) → vR.HasExtension vA
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.del.eq_def : ∀ {α : Type u_1} (x : RBTree.RBNode.Path α) (x_1 : RBTree.RBNode α) (x_2 : RBTree.RBColor),
  x.del x_1 x_2 =
    match x, x_1, x_2 with
    | RBTree.RBNode.Path.root, t, x => t.setBlack
    | RBTree.RBNode.Path.left c parent y b, a, RBTree.RBColor.red =>
      parent.del (RBTree.RBNode.node RBTree.RBColor.red a y b) c
    | RBTree.RBNode.Path.right c a y parent, b, RBTree.RBColor.red =>
      parent.del (RBTree.RBNode.node RBTree.RBColor.red a y b) c
    | RBTree.RBNode.Path.left c parent y b, a, RBTree.RBColor.black => parent.del (a.balLeft y b) c
    | RBTree.RBNode.Path.right c a y parent, b, RBTree.RBColor.black => parent.del (a.balRight y b) c
-- Mathlib.Algebra.GroupWithZero.Action.Defs
MulZeroClass.toSMulWithZero : (M₀ : Type u_2) → [inst : MulZeroClass M₀] → SMulWithZero M₀ M₀
-- Mathlib.Topology.Separation.Connected
IsPreconnected.infinite_of_nontrivial : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {s : Set X}, IsPreconnected s → s.Nontrivial → s.Infinite
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Directed.le_ciInf_iff : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompletePartialOrderInf α] [Nonempty ι] {f : ι → α} {a : α},
  Directed (fun x1 x2 => x2 ≤ x1) f → BddBelow (Set.range f) → (a ≤ iInf f ↔ ∀ (i : ι), a ≤ f i)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.Algebra.lift_comp_of : ∀ {R : Type u_1} {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : CommSemiring R]
  [inst_5 : (i : ι) → Semiring (G i)] [inst_6 : (i : ι) → Algebra R (G i)]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)] [inst_8 : Nonempty ι] (P : Type u_7)
  [inst_9 : Semiring P] [inst_10 : Algebra R P] (g : (i : ι) → G i →ₐ[R] P)
  (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) {i : ι},
  (DirectLimit.Algebra.lift G f P g Hg).comp (DirectLimit.Algebra.of G f i) = g i
-- Mathlib.Algebra.Group.Pi.Lemmas
Set.piecewise_mul : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Mul (f i)] (s : Set I) [inst_1 : (i : I) → Decidable (i ∈ s)]
  (f₁ f₂ g₁ g₂ : (i : I) → f i), s.piecewise (f₁ * f₂) (g₁ * g₂) = s.piecewise f₁ g₁ * s.piecewise f₂ g₂
-- Mathlib.RingTheory.TwoSidedIdeal.Lattice
TwoSidedIdeal.instSemilatticeSup : (R : Type u_1) → [inst : NonUnitalNonAssocRing R] → SemilatticeSup (TwoSidedIdeal R)
-- Mathlib.Topology.Order.CountableSeparating
HasCountableSeparatingOn.range_Ici : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : LinearOrder X] [OrderTopology X] [SecondCountableTopology X]
  {s : Set X}, HasCountableSeparatingOn X (fun x => x ∈ Set.range Set.Ici) s
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.zeta_mul_mu : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : Ring 𝕜] [inst_1 : PartialOrder α] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : DecidableEq α] [inst_4 : DecidableLE α], IncidenceAlgebra.zeta 𝕜 * IncidenceAlgebra.mu 𝕜 = 1
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
HomologicalComplex.restriction.sc'Iso_inv_τ₁ : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsRelIff] (i j k : ι) {i' j' k' : ι'}
  (hi' : e.f i = i') (hj' : e.f j = j') (hk' : e.f k = k') (hi'' : c'.prev j' = i') (hk'' : c'.next j' = k'),
  (HomologicalComplex.restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'').inv.τ₁ = (K.restrictionXIso e hi').inv
-- Aesop.Script.StructureDynamic
Aesop.Script.DynStructureM.State : Type
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
/-- The canonical inclusion from the pith of `B` to `B`, as a Pseudofunctor.  -/
CategoryTheory.Bicategory.Pith.inclusion : (B : Type u₁) → [inst : CategoryTheory.Bicategory B] → CategoryTheory.Pseudofunctor (CategoryTheory.Bicategory.Pith B) B
-- Mathlib.Combinatorics.SimpleGraph.LapMatrix
SimpleGraph.isSymm_lapMatrix : ∀ {V : Type u_1} (R : Type u_2) [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj]
  [inst_2 : DecidableEq V] [inst_3 : AddGroupWithOne R], (SimpleGraph.lapMatrix R G).IsSymm
-- Mathlib.Algebra.Order.GroupWithZero.Defs
mul_le_mul_of_nonneg_left : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c : α} [PosMulMono α],
  b ≤ c → 0 ≤ a → a * b ≤ a * c
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.proj.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (typeName : Lean.Name) (idx : ℕ) (struct : Lean.FVarId)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.LetValue._auto_1),
  sizeOf (Lean.Compiler.LCNF.LetValue.proj typeName idx struct h) =
    1 + sizeOf typeName + sizeOf idx + sizeOf struct + sizeOf h
-- Mathlib.Analysis.Calculus.FDeriv.Comp
/-- Eta-expanded form of `fderivWithin_comp_of_eq` -/
fderivWithin_fun_comp_of_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} (x : E) {s : Set E} {g : F → G} {t : Set F}
  {y : F},
  DifferentiableWithinAt 𝕜 g t y →
    DifferentiableWithinAt 𝕜 f s x →
      Set.MapsTo f s t →
        UniqueDiffWithinAt 𝕜 s x →
          f x = y → fderivWithin 𝕜 (fun x => g (f x)) s x = fderivWithin 𝕜 g t (f x) ∘SL fderivWithin 𝕜 f s x
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.exists.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasImages C]
  (f f_1 : X ⟶ Y), f = f_1 → CategoryTheory.Subobject.exists f = CategoryTheory.Subobject.exists f_1
-- Mathlib.GroupTheory.OrderOfElement
pow_card_eq_one : ∀ {G : Type u_1} [inst : Group G] [inst_1 : Fintype G] {x : G}, x ^ Fintype.card G = 1
-- Mathlib.Algebra.Order.Floor.Defs
/-- A `FloorRing` is a linear ordered ring over `α` with a function
`floor : α → ℤ` satisfying `∀ (z : ℤ) (a : α), z ≤ floor a ↔ (z : α) ≤ a)`.
 -/
FloorRing : (α : Type u_4) → [Ring α] → [LinearOrder α] → Type u_4
-- Mathlib.Computability.TuringMachine.Tape
Turing.PointedMap.map_pt' : ∀ {Γ : Type u} {Γ' : Type v} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] (self : Turing.PointedMap Γ Γ'),
  self.f default = default
-- Init.Data.String.Pattern.Pred
String.Slice.Pattern.CharPred.Decidable.instStrictForwardPatternForallCharProp : ∀ {p : Char → Prop} [inst : DecidablePred p], String.Slice.Pattern.StrictForwardPattern p
-- Mathlib.Algebra.Group.Even
Even.add_self : ∀ {α : Type u_2} [inst : Add α] (r : α), Even (r + r)
-- Mathlib.Data.ENNReal.Basic
ENNReal.toReal_one : ENNReal.toReal 1 = 1
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.norm_bv_add_mul' : ∀ {w : ℕ} {x y : BitVec w}, ~~~(~~~y * x) + 1#w = x + y * x
-- Mathlib.Algebra.Ring.BooleanRing
BooleanRing.inf_comm : ∀ {α : Type u_1} [inst : BooleanRing α] (a b : α), a ⊓ b = b ⊓ a
-- Lean.DocString.Types
Lean.Doc.Inline.code.sizeOf_spec : ∀ {i : Type u} [inst : SizeOf i] (string : String), sizeOf (Lean.Doc.Inline.code string) = 1 + sizeOf string
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_inter_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  (m₁ ∩ m₂).isEmpty = true ↔ ∀ k ∈ m₁, k ∉ m₂
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.sum_adj_inl : ∀ {V : Type u_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W} {v v' : V},
  (G ⊕g H).Adj (Sum.inl v) (Sum.inl v') ↔ G.Adj v v'
-- Mathlib.CategoryTheory.Monoidal.Conv
/-- The morphisms in `C` between the underlying objects of a pair of bimonoids in `C` naturally have a
(set-theoretic) monoid structure.  -/
CategoryTheory.Conv : {C : Type u₁} → [CategoryTheory.Category.{v₁, u₁} C] → C → C → Type v₁
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey_le_maxKey_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {v : β k} {he : l.isEmpty = false},
      (compare (Std.Internal.List.maxKey l he)
            (Std.Internal.List.maxKey (Std.Internal.List.insertEntryIfNew k v l) ⋯)).isLE =
        true
-- Mathlib.Data.Fin.Tuple.Reflection
FinVec.prod.eq_3 : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : One α] (n : ℕ) (v : Fin (n + 2) → α),
  FinVec.prod v = (FinVec.prod fun i => v i.castSucc) * v (Fin.last (n + 1))
-- Lean.Widget.UserWidget
Lean.Widget.instToJsonWidgetSource : Lean.ToJson Lean.Widget.WidgetSource
-- Mathlib.LinearAlgebra.StdBasis
Module.piEquiv.eq_1 : ∀ (ι : Type u_1) (R : Type u_2) (M : Type u_3) [inst : Finite ι] [inst_1 : CommSemiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M], Module.piEquiv ι R M = (Pi.basisFun R ι).constr R
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.proetalePrecoverage.eq_1 : AlgebraicGeometry.Scheme.proetalePrecoverage = AlgebraicGeometry.Scheme.propQCPrecoverage @AlgebraicGeometry.WeaklyEtale
-- Init.Data.String.Slice
String.Slice.RevSplitIterator.instFiniteIdOfSearchStep : ∀ {ρ : Type} {ρ_1 : ρ} {σ : String.Slice → Type}
  [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  [inst_1 : String.Slice.Pattern.ToBackwardSearcher ρ_1 σ] {s : String.Slice} [Std.Iterators.Finite (σ s) Id],
  Std.Iterators.Finite (String.Slice.RevSplitIterator ρ_1 s) Id
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_union_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k fallback : α},
  k ∉ t₂ → (t₁ ∪ t₂).getD k fallback = t₁.getD k fallback
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.smul : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {𝕜 : Type u_7} [inst_1 : NormedAddCommGroup 𝕜] [inst_2 : SMulZeroClass 𝕜 β] [IsBoundedSMul 𝕜 β] (c : 𝕜) {f : α → β},
  MeasureTheory.HasFiniteIntegral f μ → MeasureTheory.HasFiniteIntegral (c • f) μ
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- A family `f` of parallel morphisms has a wide equalizer if the diagram `parallelFamily f` has a
limit.  -/
CategoryTheory.Limits.HasWideEqualizer : {J : Type w} → {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (J → (X ⟶ Y)) → Prop
-- Mathlib.CategoryTheory.Skeletal
/-- When `e : C ≌ α` is a categorical equivalence from a thin category `C` to some partial order `α`,
the `ThinSkeleton C` is order isomorphic to `α`.
 -/
CategoryTheory.Equivalence.thinSkeletonOrderIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {α : Type u_1} → [inst_1 : PartialOrder α] → [Quiver.IsThin C] → (C ≌ α) → CategoryTheory.ThinSkeleton C ≃o α
-- Mathlib.Topology.Algebra.Group.Basic
/-- The connected component of 1 is a subgroup of `G`.  -/
Subgroup.connectedComponentOfOne : (G : Type u_1) → [inst : TopologicalSpace G] → [inst_1 : Group G] → [IsTopologicalGroup G] → Subgroup G
-- Mathlib.Algebra.Group.Pi.Basic
Pi.instIsRightCancelMul : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → Mul (f i)] [∀ (i : I), IsRightCancelMul (f i)],
  IsRightCancelMul ((i : I) → f i)
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.re_add : ∀ {R : Type u_1} {a b : R} [inst : Add R] (z w : QuadraticAlgebra R a b), (z + w).re = z.re + w.re
-- Mathlib.Topology.VectorBundle.Basic
/-- A mixin class for `Bundle.Trivialization`, stating that a trivialization is fiberwise linear
with respect to given module structures on its fibers and the model fiber.  -/
Bundle.Trivialization.IsLinear : (R : Type u_1) →
  {B : Type u_2} →
    {F : Type u_3} →
      {E : B → Type u_4} →
        [inst : Semiring R] →
          [inst_1 : TopologicalSpace F] →
            [inst_2 : TopologicalSpace B] →
              [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] →
                [inst_4 : AddCommMonoid F] →
                  [Module R F] →
                    [inst_6 : (x : B) → AddCommMonoid (E x)] →
                      [(x : B) → Module R (E x)] → Bundle.Trivialization F Bundle.TotalSpace.proj → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- `Arrow (WalkingParallelFamily J)` identifies to the type obtained
by adding two elements to `T`.  -/
CategoryTheory.Limits.WalkingParallelFamily.arrowEquiv : (J : Type w) → CategoryTheory.Arrow (CategoryTheory.Limits.WalkingParallelFamily J) ≃ Option (Option J)
-- Init.Data.BitVec.Bitblast
BitVec.getLsbD_sdiv : ∀ {w i : ℕ} {x y : BitVec w},
  (x.sdiv y).getLsbD i =
    match x.msb, y.msb with
    | false, false => (x / y).getLsbD i
    | false, true => (-(x / -y)).getLsbD i
    | true, false => (-(-x / y)).getLsbD i
    | true, true => (-x / -y).getLsbD i
-- Mathlib.Util.WithWeakNamespace
/-- Adds the name to the namespace, `_root_`-aware.
```
resolveNamespace `A `B.b == `A.B.b
resolveNamespace `A `_root_.B.c == `B.c
```
 -/
Lean.Elab.Command.resolveNamespace : Lean.Name → Lean.Name → Lean.Name
-- Mathlib.Order.Heyting.Hom
HeytingHomClass.toBoundedLatticeHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : HeytingAlgebra α] {x : HeytingAlgebra β}
  [HeytingHomClass F α β], BoundedLatticeHomClass F α β