mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Slice.Array.Iterator
/-- The implementation of `ForIn.forIn` for `Subarray`, which allows it to be used with `for` loops in
`do`-notation.
 -/
Subarray.forIn : {α : Type u} → {β : Type v} → {m : Type v → Type w} → [Monad m] → Subarray α → β → (α → β → m (ForInStep β)) → m β
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.SeparatingLeft.toMatrix : ∀ {R₂ : Type u_3} {M₂ : Type u_4} [inst : CommRing R₂] [inst_1 : AddCommGroup M₂] [inst_2 : Module R₂ M₂] {ι : Type u_6}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] {B : LinearMap.BilinForm R₂ M₂},
  LinearMap.SeparatingLeft B → ∀ (b : Module.Basis ι R₂ M₂), ((LinearMap.BilinForm.toMatrix b) B).SeparatingLeft
-- Mathlib.Algebra.Lie.Abelian
TrivialLieModule.instModule : (R : Type u_1) →
  (L : Type u_2) →
    (M : Type u_3) → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [Module R M] → Module R (TrivialLieModule R L M)
-- Mathlib.Order.Bounds.Image
/-- An antitone map sends a greatest element of a set to a least element of its image.  -/
AntitoneOn.map_isGreatest : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {t : Set α} {a : α},
  AntitoneOn f t → IsGreatest t a → IsLeast (f '' t) (f a)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.extendId.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone F),
  s.extendId =
    CategoryTheory.Limits.Cone.ext (CategoryTheory.Iso.refl (s.extend (CategoryTheory.CategoryStruct.id s.pt)).pt) ⋯
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
CategoryTheory.Limits.pullbackObjIso_hom_comp_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Limits.HasPullbacks C] (f : F ⟶ H) (g : G ⟶ H) (d : D),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackObjIso f g d).hom
      (CategoryTheory.Limits.pullback.fst (f.app d) (g.app d)) =
    (CategoryTheory.Limits.pullback.fst f g).app d
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.isSubwalk_rfl : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.IsSubwalk p
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence_exact : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z), (CategoryTheory.kernelCokernelCompSequence f g).Exact
-- Mathlib.Algebra.Ring.Subsemiring.Basic
RingHom.rangeS_toSubmonoid : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S),
  f.rangeS.toSubmonoid = { carrier := Set.range ⇑f, mul_mem' := ⋯, one_mem' := ⋯ }
-- Mathlib.FieldTheory.Relrank
IntermediateField.finrank_bot_mul_relfinrank : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E},
  A ≤ B → Module.finrank F ↥A * A.relfinrank B = Module.finrank F ↥B
-- Mathlib.Order.Defs.PartialOrder
Preorder.le_trans : ∀ {α : Type u_2} [self : Preorder α] (a b c : α), a ≤ b → b ≤ c → a ≤ c
-- Mathlib.Combinatorics.Graph.Simple
Graph.Loopless.not_isLoopAt : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β} [self : G.Loopless] (e : β) (x : α), ¬G.IsLoopAt e x
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.add_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Y : C}
  (a b : X ⟶ Y), a + b = a - -b
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Methods : Type
-- Lean.Server.Requests
Lean.Server.instMonadLiftCancellableMRequestM : MonadLift Lean.Server.CancellableM Lean.Server.RequestM
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
VAdd.ofStabilizer.eq_1 : ∀ (G : Type u_1) [inst : AddGroup G] (α : Type u_2) [inst_1 : AddAction G α] (s : Set α),
  VAdd.ofStabilizer G α s = { vadd := fun g x => ⟨g +ᵥ ↑x, ⋯⟩ }
-- Mathlib.Order.WithBot
WithTop.map₂_top_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : WithTop α), WithTop.map₂ f a ⊤ = ⊤
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.yn_succ_succ : ∀ {a : ℕ} (a1 : 1 < a) (n : ℕ), Pell.yn a1 (n + 2) + Pell.yn a1 n = 2 * a * Pell.yn a1 (n + 1)
-- Lean.ScopedEnvExtension
Lean.SimpleScopedEnvExtension.Descr.addEntry : {α σ : Type} → Lean.SimpleScopedEnvExtension.Descr α σ → σ → α → σ
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- Use the axiom of choice to extract explicit `BiproductData F` from `HasBiproduct F`.  -/
CategoryTheory.Limits.getBiproductData : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (F : J → C) → [CategoryTheory.Limits.HasBiproduct F] → CategoryTheory.Limits.LimitBicone F
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.MutuallySingular.zero_left : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M]
  [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid N] [inst_3 : TopologicalSpace N]
  {w : MeasureTheory.VectorMeasure α N}, MeasureTheory.VectorMeasure.MutuallySingular 0 w
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.instInhabitedWalkingReflexivePair.default : CategoryTheory.Limits.WalkingReflexivePair
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙHom_of_cfcHom.eq_1 : ∀ (R : Type u_1) {A : Type u_2} {p : A → Prop} [inst : Semifield R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Ring A] [inst_6 : StarRing A]
  [inst_7 : TopologicalSpace A] [inst_8 : Algebra R A] [inst_9 : ContinuousFunctionalCalculus R A p] {a : A} (ha : p a),
  cfcₙHom_of_cfcHom R ha =
    (↑(cfcHom ha)).comp
      ((↑(ContinuousMap.compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ })).comp
        ContinuousMapZero.toContinuousMapHom)
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.IsLocallyDirected.V.eq_1 : ∀ {J : Type w} [inst : CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme)
  [inst_1 : ∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)] (i j : J),
  AlgebraicGeometry.Scheme.IsLocallyDirected.V F i j = ⨆ k, AlgebraicGeometry.Scheme.Hom.opensRange (F.map k.snd.1)
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological_i₀ : ∀ (r : ℤ) (pq : ℤ × ℤ) (hr : 2 ≤ r),
  CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological.i₀ r pq hr = WithBotTop.coe (pq.2 - r + 2)
-- Init.Internal.Order.Basic
Lean.Order.instPartialOrderPProd : {α : Sort u} →
  {β : Sort v} → [Lean.Order.PartialOrder α] → [Lean.Order.PartialOrder β] → Lean.Order.PartialOrder (α ×' β)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Normal
/-- If `φ` is mono, it is a normal group homomorphism if and only if for all `X` the image of
`H(X)` in `G(X)` is a normal subgroup.  -/
CategoryTheory.IsMonHom.normal_iff_normal_monoidHom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H : C} [inst_2 : CategoryTheory.GrpObj G] [inst_3 : CategoryTheory.GrpObj H] {φ : H ⟶ G}
  [inst_4 : CategoryTheory.IsMonHom φ] [CategoryTheory.Mono φ],
  CategoryTheory.IsMonHom.Normal φ ↔ ∀ (X : C), (CategoryTheory.IsMonHom.monoidHom φ X).range.Normal
-- Std.Data.DTreeMap.Raw.Basic
/-- Two tree maps are equivalent in the sense of Equiv iff all the keys and values are equal.  -/
Std.DTreeMap.Raw.«term_~m_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.add_mem : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M)
  {x y : M}, x ∈ p → y ∈ p → x + y ∈ p
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
HasFDerivAt.ccos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {f' : StrongDual ℂ E} {x : E},
  HasFDerivAt f f' x → HasFDerivAt (fun x => Complex.cos (f x)) (-Complex.sin (f x) • f') x
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toList_rcc_eq_none_iff : ∀ {m n i : ℕ}, (m...=n).toList[i]? = none ↔ n + 1 ≤ i + m
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExBaseNat.atom.inj : ∀ {e : Q(ℕ)} {id id_1 : ℕ},
  Mathlib.Tactic.Ring.Common.ExBaseNat.atom id = Mathlib.Tactic.Ring.Common.ExBaseNat.atom id_1 → id = id_1
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.IsBilimit.mk.inj : ∀ {C : Type uC} {inst : CategoryTheory.Category.{uC', uC} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  {P Q : C} {b : CategoryTheory.Limits.BinaryBicone P Q} {isLimit : CategoryTheory.Limits.IsLimit b.toCone}
  {isColimit : CategoryTheory.Limits.IsColimit b.toCocone} {isLimit_1 : CategoryTheory.Limits.IsLimit b.toCone}
  {isColimit_1 : CategoryTheory.Limits.IsColimit b.toCocone},
  { isLimit := isLimit, isColimit := isColimit } = { isLimit := isLimit_1, isColimit := isColimit_1 } →
    isLimit = isLimit_1 ∧ isColimit = isColimit_1
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.inverse'_comp : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : SMul M X] {Y : Type u_6} [inst_1 : SMul N Y]
  {φ' : N → M} {f : X →ₑ[φ] Y} {g : Y → X} {k₂ : Function.RightInverse φ' φ} {h₁ : Function.LeftInverse g ⇑f}
  {h₂ : Function.RightInverse g ⇑f}, f.comp (f.inverse' g k₂ h₁ h₂) = MulActionHom.id N
-- Init.Grind.Interactive
/-- `linarith` linear arithmetic.  -/
Lean.Parser.Tactic.Grind.linarith : Lean.ParserDescr
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- This is basically just `yoneda.obj η : (Over A)ᵒᵖ ⥤ Type (max u v)` restricted along the
forgetful functor `CostructuredArrow yoneda A ⥤ Over A`, but done in a way that we land in a
smaller universe.  -/
CategoryTheory.OverPresheafAux.restrictedYonedaObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      (F ⟶ A) → CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.map_inv : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {S : Type u_1}
  [inst_3 : CommRing S] (f : R →+* S) (g : GL n R),
  (Matrix.GeneralLinearGroup.map f) g⁻¹ = ((Matrix.GeneralLinearGroup.map f) g)⁻¹
-- Mathlib.Order.Filter.AtTopBot.Defs
/-- `atBot` is the filter representing the limit `→ -∞` on an ordered set.
It is generated by the collection of down-sets `{b | b ≤ a}`.
(The preorder need not have a bottom element for this to be well defined,
and indeed is trivial when a bottom element `x` exists, i.e., it coincides with `pure x`.)  -/
Filter.atBot : {α : Type u_3} → [Preorder α] → Filter α
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_filterMap_eq_true : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : LawfulBEq α]
  {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ((List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l).isEmpty = true ↔
      ∀ (k : α) (h : Std.Internal.List.containsKey k l = true), f k (Std.Internal.List.getValueCast k l h) = none)
-- Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
SSet.innerFibration_iff : ∀ {X Y : SSet} (q : X ⟶ Y), SSet.InnerFibration q ↔ SSet.innerFibrations q
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
HasMFDerivAt.inv' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {z : M} {F' : Type u_21} [inst_6 : NormedDivisionRing F']
  [inst_7 : NormedAlgebra 𝕜 F'] {p : M → F'} {p' : TangentSpace I z →L[𝕜] F'},
  HasMFDerivAt% p z p' → p z ≠ 0 → HasMFDerivAt% p⁻¹ z (-(MulOpposite.op (p z)⁻¹ • (p z)⁻¹ • p'))
-- Mathlib.Order.RelClasses
instIsTransLe : ∀ {α : Type u} [inst : Preorder α], IsTrans α fun x1 x2 => x1 ≤ x2
-- Mathlib.Topology.MetricSpace.Polish
TopologicalSpace.Opens.CompleteCopy.inst : {α : Type u_1} → [inst : MetricSpace α] → {s : TopologicalSpace.Opens α} → TopologicalSpace s.CompleteCopy
-- Init.Grind.AC
Lean.Grind.AC.Seq.eraseDup_k : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
range_cfcₙHom_le : ∀ (𝕜 : Type u_1) {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A]
  [inst_3 : Module 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A] [inst_6 : TopologicalSpace A]
  [inst_7 : ContinuousConstSMul 𝕜 A] [inst_8 : StarModule 𝕜 A] [inst_9 : IsTopologicalRing A]
  [inst_10 : ContinuousStar A] [inst_11 : NonUnitalContinuousFunctionalCalculus 𝕜 A p] {a : A} (ha : p a),
  NonUnitalStarAlgHom.range (cfcₙHom ha) ≤ NonUnitalStarAlgebra.elemental 𝕜 a
-- Plausible.Arbitrary
Plausible.USize.Arbitrary : Plausible.Arbitrary USize
-- Mathlib.Topology.Algebra.StarSubalgebra
StarAlgebra.elemental.isClosed : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace A]
  [inst_3 : Semiring A] [inst_4 : StarRing A] [inst_5 : IsSemitopologicalSemiring A] [inst_6 : ContinuousStar A]
  [inst_7 : Algebra R A] [inst_8 : StarModule R A] (x : A), IsClosed ↑(StarAlgebra.elemental R x)
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeGroup.reduceCyclically.isCyclicallyReduced : ∀ {α : Type u} {L : List (α × Bool)} [inst : DecidableEq α],
  FreeGroup.IsReduced L → FreeGroup.IsCyclicallyReduced (FreeGroup.reduceCyclically L)
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.instCommSemiring : {ι : Type u_1} →
  {R : Type u_3} →
    {A : ι → Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : (i : ι) → CommSemiring (A i)] →
          [inst_2 : (i : ι) → Algebra R (A i)] → CommSemiring (PiTensorProduct R fun i => A i)
-- Mathlib.Combinatorics.Matroid.Loop
/-- Two distinct nonloops with the same closure form a circuit.  -/
Matroid.IsNonloop.closure_eq_closure_iff_isCircuit_of_ne : ∀ {α : Type u_1} {M : Matroid α} {e f : α}, M.IsNonloop e → e ≠ f → (M.closure {e} = M.closure {f} ↔ M.IsCircuit {e, f})
-- Mathlib.Algebra.Group.Basic
pow_natAbs_eq_one : ∀ {G : Type u_3} [inst : Group G] {a : G} {n : ℤ}, a ^ n.natAbs = 1 ↔ a ^ n = 1
-- Lean.Elab.Declaration
/-- Return `some name` if `stx` is a declaration named `name`  -/
_private.Lean.Elab.Declaration.0.Lean.Elab.Command.getDeclName? : Lean.Syntax → Option Lean.Name
-- Batteries.Util.ProofWanted
_private.Batteries.Util.ProofWanted.0.defWantedCmd : WantedCmdKind✝
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
NonUnitalIsometricContinuousFunctionalCalculus.congr_simp : ∀ (R : Type u_1) (A : Type u_2) (p p_1 : A → Prop),
  p = p_1 →
    ∀ [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R] [inst_3 : MetricSpace R]
      [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A] [inst_7 : StarRing A]
      [inst_8 : MetricSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A] [inst_11 : SMulCommClass R A A],
      NonUnitalIsometricContinuousFunctionalCalculus R A p = NonUnitalIsometricContinuousFunctionalCalculus R A p_1
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.ne_startPos_of_singleton : ∀ {t₁ : String} {c : Char} {t₂ s : String} {p : s.Pos}, p.Splits (t₁ ++ String.singleton c) t₂ → p ≠ s.startPos
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
/-- Auxiliary function used in studying zeta-function asymptotics.  -/
ZetaAsymptotics.term : ℕ → ℝ → ℝ
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.mk.injEq : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : Zero Y] (toFun : X → Y)
  (supportWithinDomain' : Function.support toFun ⊆ U)
  (supportLocallyFiniteWithinDomain' : ∀ z ∈ U, ∃ t ∈ nhds z, (t ∩ Function.support toFun).Finite) (toFun_1 : X → Y)
  (supportWithinDomain'_1 : Function.support toFun_1 ⊆ U)
  (supportLocallyFiniteWithinDomain'_1 : ∀ z ∈ U, ∃ t ∈ nhds z, (t ∩ Function.support toFun_1).Finite),
  ({ toFun := toFun, supportWithinDomain' := supportWithinDomain',
        supportLocallyFiniteWithinDomain' := supportLocallyFiniteWithinDomain' } =
      { toFun := toFun_1, supportWithinDomain' := supportWithinDomain'_1,
        supportLocallyFiniteWithinDomain' := supportLocallyFiniteWithinDomain'_1 }) =
    (toFun = toFun_1)
-- Mathlib.CategoryTheory.Action.Continuous
Action.instHasForget₂HomSubtypeVTopCatContinuousMapCarrier : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {FV : V → V → Type u_2} →
      {CV : V → Type u_3} →
        [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory V FV] →
            [CategoryTheory.HasForget₂ V TopCat] →
              (G : Type u_4) → [inst_4 : Monoid G] → CategoryTheory.HasForget₂ (Action V G) TopCat
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.esymm_isSymmetric : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ] (n : ℕ),
  (MvPolynomial.esymm σ R n).IsSymmetric
-- Init.Data.UInt.Bitwise
UInt16.toUInt8_shiftLeft_mod : ∀ (a b : UInt16), (a <<< (b % 8)).toUInt8 = a.toUInt8 <<< b.toUInt8
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Sized.rotateL : ∀ {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α}, l.Sized → r.Sized → (l.rotateL x r).Sized
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.MonoOver.isIso_hom_left_iff_subobjectMk_eq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {P Q : CategoryTheory.MonoOver X} (f : P ⟶ Q),
  CategoryTheory.IsIso (CategoryTheory.Over.Hom.left f.hom) ↔
    CategoryTheory.Subobject.mk P.obj.hom = CategoryTheory.Subobject.mk Q.obj.hom
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- If `f` is integrable, then for any `c < 0` the set `{x | f x ≤ c}` has finite
measure.  -/
MeasureTheory.Integrable.measure_le_lt_top : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f : α → β} [inst_1 : Lattice β] [HasSolidNorm β] [AddLeftMono β],
  MeasureTheory.Integrable f μ → ∀ {c : β}, c < 0 → μ {a | f a ≤ c} < ⊤
-- Mathlib.NumberTheory.JacobiSum.Basic
/-- If `χ` and `φ` are multiplicative characters on a finite field `F` satisfying `χ^n = φ^n = 1`
and with values in an integral domain `R`, and `μ` is a primitive `n`th root of unity in `R`,
then the Jacobi sum `J(χ,φ)` is in `ℤ[μ] ⊆ R`.  -/
jacobiSum_mem_algebraAdjoin_of_pow_eq_one : ∀ {F : Type u_1} {R : Type u_2} [inst : Field F] [inst_1 : CommRing R] [IsDomain R] [inst_3 : Fintype F] {n : ℕ}
  [NeZero n] {χ φ : MulChar F R}, χ ^ n = 1 → φ ^ n = 1 → ∀ {μ : R}, IsPrimitiveRoot μ n → jacobiSum χ φ ∈ ℤ[μ]
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_eq_none_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α}, m.contains a = false → m.getKey? a = none
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.intro : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : Zero β] {f : α → β} {K : Set α} [R1Space α],
  IsCompact K → (∀ x ∉ K, f x = 0) → HasCompactSupport f
-- Mathlib.Algebra.Category.FGModuleCat.Basic
FGModuleCat.Iso.conj_eq_conj : ∀ (R : Type u) [inst : CommRing R] {V W : FGModuleCat R} (i : V ≅ W) (f : CategoryTheory.End V),
  i.conj f = FGModuleCat.ofHom ((FGModuleCat.isoToLinearEquiv i).conj (ModuleCat.Hom.hom f.hom))
-- Mathlib.Data.Nat.Choose.Basic
_private.Mathlib.Data.Nat.Choose.Basic.0.Nat.choose.match_1.eq_1 : ∀ (motive : ℕ → ℕ → Sort u_1) (x : ℕ) (h_1 : (x : ℕ) → motive x 0) (h_2 : (n : ℕ) → motive 0 n.succ)
  (h_3 : (n k : ℕ) → motive n.succ k.succ),
  (match x, 0 with
    | x, 0 => h_1 x
    | 0, n.succ => h_2 n
    | n.succ, k.succ => h_3 n k) =
    h_1 x
-- Mathlib.Algebra.BigOperators.Finprod
/-- A more general version of `AddMonoidHom.map_finsum_mem` that requires
`s ∩ support f` rather than `s` to be finite.  -/
AddMonoidHom.map_finsum_mem' : ∀ {α : Type u_1} {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] {s : Set α}
  {f : α → M} (g : M →+ N),
  (s ∩ Function.support f).Finite → g (∑ᶠ (j : α) (_ : j ∈ s), f j) = ∑ᶠ (i : α) (_ : i ∈ s), g (f i)
-- Mathlib.Data.Set.Lattice.Image
Set.preimage_iUnion : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : α → β} {s : ι → Set β}, f ⁻¹' ⋃ i, s i = ⋃ i, f ⁻¹' s i
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Subgroup.isCyclic_zpowers : ∀ {G : Type u_2} [inst : Group G] (g : G), IsCyclic ↥(Subgroup.zpowers g)
-- Std.Data.Internal.List.Associative
Std.Internal.List.foldrM_eq_foldrM_toProd : ∀ {α : Type u} {β : Type v} {δ : Type w} {m' : Type w → Type w'} [inst : Monad m'] [LawfulMonad m']
  {l : List ((_ : α) × β)} {f : α → β → δ → m' δ} {init : δ},
  List.foldrM (fun a b => f a.fst a.snd b) init l =
    List.foldrM (fun a b => f a.1 a.2 b) init (List.map (fun x => (x.fst, x.snd)) l)
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalTerm.evalNatStx : Lean.Term → Lean.Elab.TermElabM (ℕ × Lean.Expr)
-- Mathlib.GroupTheory.Torsion
/-- The torsion additive submonoid of an additive commutative monoid.  -/
AddCommMonoid.addTorsion : (G : Type u_1) → [inst : AddCommMonoid G] → AddSubmonoid G
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatIso.removeOp_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F.op ≅ G.op),
  (CategoryTheory.NatIso.removeOp α).inv = CategoryTheory.NatTrans.removeOp α.inv
-- Mathlib.Algebra.Category.Semigrp.Basic
_private.Mathlib.Algebra.Category.Semigrp.Basic.0.Semigrp.Hom.mk.sizeOf_spec : ∀ {A B : Semigrp} (hom' : ↑A →ₙ* ↑B), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Mathlib.Order.OmegaCompletePartialOrder
Part.mem_ωSup : ∀ {α : Type u_2} (x : α) (c : OmegaCompletePartialOrder.Chain (Part α)),
  x ∈ OmegaCompletePartialOrder.ωSup c ↔ Part.some x ∈ c
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- If a short complex `S` is such that `S.g = 0` and that the cokernel of `S.f` is preserved
by a functor `F`, then `F` preserves the right homology of `S`.  -/
CategoryTheory.Functor.preservesRightHomology_of_zero_g : ∀ {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] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] (S : CategoryTheory.ShortComplex C),
  S.g = 0 →
    ∀ [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair S.f 0) F],
      F.PreservesRightHomologyOf S
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
HomogeneousIdeal.gc_map_comap : ∀ {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} {ι : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] [inst_4 : AddSubmonoidClass σ A] [inst_5 : AddSubmonoidClass τ B]
  [inst_6 : DecidableEq ι] [inst_7 : AddMonoid ι] {𝒜 : ι → σ} {ℬ : ι → τ} [inst_8 : GradedRing 𝒜]
  [inst_9 : GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ), GaloisConnection (HomogeneousIdeal.map f) (HomogeneousIdeal.comap f)
-- Mathlib.Topology.EMetricSpace.Defs
PseudoEMetricSpace.edist_comm : ∀ {α : Type u} [self : PseudoEMetricSpace α] (x y : α), edist x y = edist y x
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.isEmpty_diff_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ((m₁ \ m₂).isEmpty = true ↔ ∀ k ∈ m₁, k ∈ m₂)