mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- The identity acts trivially.  -/
CategoryTheory.ModObj.one_smul : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {M : C} {inst_4 : CategoryTheory.MonObj M} (X : D) [self : CategoryTheory.ModObj M X],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.MonObj.one X)
      CategoryTheory.ModObj.smul =
    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom
-- Mathlib.Algebra.Category.CommHopfAlgCat
/-- The underlying bialgebra map.  -/
CommHopfAlgCat.Hom.hom' : {R : Type u} → [inst : CommRing R] → {A B : CommHopfAlgCat R} → A.Hom B → ↑A →ₐc[R] ↑B
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h : m.WF) {l : List ((a : α) × β a)} {k : α}
  (contains_eq_false : (List.map Sigma.fst l).contains k = false) {h' : k ∈ m.insertMany l},
  (m.insertMany l).getKey k h' = m.getKey k ⋯
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Algebra.intNorm_ne_zero : ∀ {A : Type u_1} {B : Type u_6} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : IsIntegrallyClosed A] [inst_4 : IsDomain A] [inst_5 : IsDomain B] [inst_6 : IsIntegrallyClosed B]
  [inst_7 : Algebra.IsIntegral A B] [inst_8 : Module.IsTorsionFree A B]
  [FiniteDimensional (FractionRing A) (FractionRing B)] {x : B}, (Algebra.intNorm A B) x ≠ 0 ↔ x ≠ 0
-- Mathlib.Logic.Basic
/-- **Alias** of the forward direction of `or_rotate`. -/
Or.rotate : ∀ {a b c : Prop}, a ∨ b ∨ c → b ∨ c ∨ a
-- Mathlib.Algebra.EuclideanDomain.Defs
/-- Division by zero should always give zero by convention.  -/
EuclideanDomain.quotient_zero : ∀ {R : Type u} [self : EuclideanDomain R] (a : R), EuclideanDomain.quotient a 0 = 0
-- Mathlib.Analysis.Normed.Module.Bases
/-- The `n`-th projection `P_n = b.proj (Finset.range n)`, given by:
`P_n x = ∑ i ∈ Finset.range n, b.coord i x • b i`  -/
SchauderBasis.proj : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {X : Type u_2} → [inst_1 : NormedAddCommGroup X] → [inst_2 : NormedSpace 𝕜 X] → SchauderBasis 𝕜 X → ℕ → X →L[𝕜] X
-- Init.Data.Iterators.Lemmas.Combinators.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Take.0.Std.Iter.toArray_eq_match_step.match_1.splitter : {α β : Type u_1} →
  (motive : Std.IterStep (Std.Iter β) β → Sort u_2) →
    (x : Std.IterStep (Std.Iter β) β) →
      ((it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out)) →
        ((it' : Std.Iter β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sign_neg_coe_nonpos_of_nonneg_of_le_pi : ∀ {θ : ℝ}, 0 ≤ θ → θ ≤ Real.pi → (-↑θ).sign ≤ 0
-- Mathlib.CategoryTheory.MorphismProperty.Local
CategoryTheory.MorphismProperty.of_zeroHypercover_source : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  {K : CategoryTheory.Precoverage C} [P.IsLocalAtSource K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover X) [𝒰.Small],
  (∀ (i : 𝒰.I₀), P (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)) → P f
-- Mathlib.Analysis.Calculus.Deriv.Basic
DifferentiableAt.hasDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜}, DifferentiableAt 𝕜 f x → HasDerivAt f (deriv f x) x
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.isSolvable_iff_int : ∀ (L : Type v) [inst : LieRing L], LieAlgebra.IsSolvable L ↔ ∃ k, LieAlgebra.derivedSeries ℤ L k = ⊥
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.instMonoidalFunctorSymmOfInverse : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] → (e : C ≌ D) → [e.inverse.Monoidal] → e.symm.functor.Monoidal
-- Mathlib.Data.Nat.Cast.Basic
eq_natCast' : ∀ {A : Type u_3} {F : Type u_5} [inst : FunLike F ℕ A] [inst_1 : AddMonoidWithOne A] [AddMonoidHomClass F ℕ A] (f : F),
  f 1 = 1 → ∀ (n : ℕ), f n = ↑n
-- Mathlib.Computability.RecursiveIn
RecursiveIn.eq_1 : ∀ {α : Type u_5} {σ : Type u_6} [inst : Primcodable α] [inst_1 : Primcodable σ] (O : Set (ℕ →. ℕ)) (f : α →. σ),
  RecursiveIn O f = Nat.RecursiveIn O fun n => (↑(Encodable.decode n)).bind fun a => Part.map Encodable.encode (f a)
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
/-- The functoriality map between divided power algebras associated with a linear equivalence of
the underlying modules. Given an `R`-algebra `S`, an `S`-module `N` and an `R`-linear equivalence
`f : M →ₗ[R] N`, this is the map `DividedPowerAlgebra R M →ₐ[R] DividedPowerAlgebra S N`
sending `dp R n m` to `dp S n (f m)`.  -/
DividedPowerAlgebra.mapEquiv : {R : Type u_2} →
  {M : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_5} →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] → (M ≃ₗ[R] N) → DividedPowerAlgebra R M ≃ₐ[R] DividedPowerAlgebra R N
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.left_quotientAction : ∀ {G : Type u} [inst : AddGroup G] (H : AddSubgroup G), AddAction.QuotientAction G H
-- Mathlib.Data.Finset.Basic
Finset.erase_inter_comm : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α) (a : α), s.erase a ∩ t = s ∩ t.erase a
-- Lean.Parser.Basic
Lean.Parser.optionalFn : Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_filterMap_eq_size_iff : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {f : α → β → Option γ},
  (Std.TreeMap.filterMap f t).size = t.size ↔ ∀ (k : α) (h : k ∈ t), (f (t.getKey k h) t[k]).isSome = true
-- Mathlib.Condensed.Basic
/-- **Alias** of `Condensed.id_hom`. -/
Condensed.id_val : ∀ {C : Type w} [inst : CategoryTheory.Category.{v, w} C] (X : Condensed C),
  (CategoryTheory.CategoryStruct.id X).hom = CategoryTheory.CategoryStruct.id X.obj
-- Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
CategoryTheory.Functor.mapDerivedCategorySingleFunctor_inv_app_mapDerivedCategoryFactors_hom_app_assoc : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] [inst_1 : CategoryTheory.Abelian C₁]
  [inst_2 : HasDerivedCategory C₁] {C₂ : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C₂]
  [inst_4 : CategoryTheory.Abelian C₂] [inst_5 : HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂)
  [inst_6 : F.Additive] [inst_7 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_8 : CategoryTheory.Limits.PreservesFiniteColimits F] (X : C₁) {Z : DerivedCategory C₂}
  (h :
    DerivedCategory.Q.obj
        ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj
          ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj X)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp ((F.mapDerivedCategorySingleFunctor 0).inv.app X)
      (CategoryTheory.CategoryStruct.comp
        (F.mapDerivedCategoryFactors.hom.app ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj X)) h) =
    CategoryTheory.CategoryStruct.comp (DerivedCategory.Q.map ((F.mapCochainComplexSingleFunctor 0).inv.app X)) h
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.instIsLocallyFiniteMeasureProdVolume : ∀ {X : Type u_4} {Y : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {m : MeasureTheory.MeasureSpace X} [MeasureTheory.IsLocallyFiniteMeasure MeasureTheory.volume]
  {m' : MeasureTheory.MeasureSpace Y} [MeasureTheory.IsLocallyFiniteMeasure MeasureTheory.volume],
  MeasureTheory.IsLocallyFiniteMeasure MeasureTheory.volume
-- Lean.Elab.Term.TermElabM
/-- During elaboration we track the current context for adding auto-bound
implicit variables. (We mark the entry to such a region with
`withAutoBoundImplicit` and leave it with `withoutAutoBoundImplicit`.)

When the `autoImplicit` option is `false`, this context is only used to
affect error messages. When `autoImplicit` is `true` and an identifier is
unbound and potentially an auto-bound implicit, an internal exception is
thrown and caught at the closest surrounding `withAutoBoundImplicit`,
which adds an implicit declaration for the unbound variable and tries
again.
 -/
Lean.Elab.Term.Context.autoBoundImplicitContext : Lean.Elab.Term.Context → Option Lean.Elab.AutoBoundImplicitContext
-- Lean.ProjFns
Lean.ProjectionFunctionInfo.mk.sizeOf_spec : ∀ (ctorName : Lean.Name) (numParams i : ℕ) (fromClass : Bool),
  sizeOf { ctorName := ctorName, numParams := numParams, i := i, fromClass := fromClass } =
    1 + sizeOf ctorName + sizeOf numParams + sizeOf i + sizeOf fromClass
-- Init.Data.SInt.Bitwise
Int64.toBitVec_and : ∀ (a b : Int64), (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.HorizontalComp.cons.injEq : ∀ (e : Mathlib.Tactic.BicategoryLike.Mor₂) (η : Mathlib.Tactic.BicategoryLike.WhiskerRight)
  (ηs : Mathlib.Tactic.BicategoryLike.HorizontalComp) (e_1 : Mathlib.Tactic.BicategoryLike.Mor₂)
  (η_1 : Mathlib.Tactic.BicategoryLike.WhiskerRight) (ηs_1 : Mathlib.Tactic.BicategoryLike.HorizontalComp),
  (Mathlib.Tactic.BicategoryLike.HorizontalComp.cons e η ηs =
      Mathlib.Tactic.BicategoryLike.HorizontalComp.cons e_1 η_1 ηs_1) =
    (e = e_1 ∧ η = η_1 ∧ ηs = ηs_1)
-- Std.Http.Data.URI.Encoding
/-- Encodes a raw string into an `EncodedQueryString` with automatic proof construction. Unreserved characters
are kept as-is, spaces are encoded as '+', and all other characters are percent-encoded.
 -/
Std.Http.URI.EncodedQueryString.encode : String → (r : optParam (UInt8 → Bool) Std.Http.Internal.Char.isQueryChar) → Std.Http.URI.EncodedQueryString r
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙHom_eq_of_continuous_of_map_id : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [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 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] {a : A} (ha : p a)
  [ContinuousMapZero.UniqueHom R A] (φ : ContinuousMapZero (↑(quasispectrum R a)) R →⋆ₙₐ[R] A),
  Continuous ⇑φ → φ (ContinuousMapZero.id (quasispectrum R a)) = a → cfcₙHom ha = φ
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.coe_div : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K) (x y : ↥s), ↑(x / y) = ↑x / ↑y
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.SplitCandidateAnchors.mk : Array Lean.Meta.Grind.SplitCandidateWithAnchor → ℕ → Lean.Meta.Grind.SplitCandidateAnchors
-- Lean.Meta.AbstractNestedProofs
Lean.Meta.AbstractNestedProofs.Context.cache : Lean.Meta.AbstractNestedProofs.Context → Bool
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.limsup_mul_le : ∀ {α : Type u_3} {f : Filter α} {u v : α → EReal},
  (∃ᶠ (x : α) in f, 0 ≤ u x) →
    0 ≤ᶠ[f] v →
      Filter.limsup u f ≠ 0 ∨ Filter.limsup v f ≠ ⊤ →
        Filter.limsup u f ≠ ⊤ ∨ Filter.limsup v f ≠ 0 → Filter.limsup (u * v) f ≤ Filter.limsup u f * Filter.limsup v f
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.range_subtype : ∀ {R : Type u} [inst : NonAssocRing R] (s : Subring R), s.subtype.range = s
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.prodComm_symm : ∀ (k : Type u_1) (P₁ : Type u_2) (P₂ : Type u_3) {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂],
  (AffineEquiv.prodComm k P₁ P₂).symm = AffineEquiv.prodComm k P₂ P₁
-- Mathlib.Data.Set.Image
/-- **Alias** of `Set.compl_image_ofPred`. -/
Set.compl_image_set_of : ∀ {α : Type u_1} {p : Set α → Prop}, compl '' {s | p s} = {s | p sᶜ}
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
/-- Left homotopy is closed under composition (on the right).  -/
CategoryTheory.Arrow.LeftHomotopy.compRight : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {u v w : CategoryTheory.Arrow V} →
        {e f : u ⟶ v} →
          CategoryTheory.Arrow.LeftHomotopy e f →
            (g : v ⟶ w) →
              CategoryTheory.Arrow.LeftHomotopy (CategoryTheory.CategoryStruct.comp e g)
                (CategoryTheory.CategoryStruct.comp f g)
-- Aesop.Rule
Aesop.instInhabitedSafeRuleInfo.default : Aesop.SafeRuleInfo
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.Colex.total_le : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : LinearOrder ι]
  [inst_2 : (i : ι) → LinearOrder (α i)], Std.Total fun x1 x2 => x1 ≤ x2
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey!_alter_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited α] (h : t.WF) {k : α} {f : Option β → Option β},
  (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.getKey! k =
    if (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true then k else default
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.evaluation_ne_zero_iff_mem_basicOpen : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens} (x : ↥X) (hx : x ∈ U) (f : ↑(X.presheaf.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom (X.evaluation U x hx)) f ≠ 0 ↔ x ∈ X.basicOpen f
-- Mathlib.Data.Finsupp.Weight
Finsupp.le_weight_of_ne_zero' : ∀ {σ : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedAddMonoid M]
  [CanonicallyOrderedAdd M] (w : σ → M) {s : σ} {f : σ →₀ ℕ}, f s ≠ 0 → w s ≤ (Finsupp.weight w) f
-- Init.Prelude
/-- The elimination principle for `Nonempty α`. If `Nonempty α`, and we can
prove `p` given any element `x : α`, then `p` holds. Note that it is essential
that `p` is a `Prop` here; the version with `p` being a `Sort u` is equivalent
to `Classical.choice`.
 -/
Nonempty.elim : ∀ {α : Sort u} {p : Prop}, Nonempty α → (∀ (a : α), p) → p
-- Mathlib.Data.Set.PowersetCard
/-- The coercion of a finite set to its corresponding element of `Set.powersetCard`.  -/
Set.powersetCard.ofCard : {α : Type u_1} → {n : ℕ} → {s : Finset α} → s.card = n → ↑(Set.powersetCard α n)
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
/-- If `‖v‖^n * ‖f v‖` is integrable for all `n ≤ N`, then the `n`-th derivative of the Fourier
transform of `f` is the Fourier transform of `fourierPowSMulRight L f v n`,
i.e., `(L v ⬝) ^ n • f v`.  -/
VectorFourier.iteratedFDeriv_fourierIntegral : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} {W : Type u_3}
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : NormedAddCommGroup W] [inst_5 : NormedSpace ℝ W]
  (L : V →L[ℝ] W →L[ℝ] ℝ) {f : V → E} [inst_6 : MeasurableSpace V] [BorelSpace V] {μ : MeasureTheory.Measure V}
  [SecondCountableTopology V] {N : ℕ∞},
  (∀ (n : ℕ), ↑n ≤ N → MeasureTheory.Integrable (fun v => ‖v‖ ^ n * ‖f v‖) μ) →
    MeasureTheory.AEStronglyMeasurable f μ →
      ∀ {n : ℕ},
        ↑n ≤ N →
          iteratedFDeriv ℝ n
              (VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ L) f) =
            VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ L) fun v =>
              VectorFourier.fourierPowSMulRight L f v n
-- Mathlib.Data.Multiset.AddSub
Multiset.cons_add : ∀ {α : Type u_1} (a : α) (s t : Multiset α), a ::ₘ s + t = a ::ₘ (s + t)
-- Mathlib.Data.FunLike.Equiv
/-- The coercions are right inverses.  -/
EquivLike.right_inv : ∀ {E : Sort u_1} {α : outParam (Sort u_2)} {β : outParam (Sort u_3)} [self : EquivLike E α β] (e : E),
  Function.RightInverse (EquivLike.inv e) (EquivLike.coe e)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Reify
_private.Lean.Meta.Tactic.Grind.Arith.Linear.Reify.0.Lean.Meta.Grind.Arith.Linear.reify?.toVar : ℕ → Lean.Expr → Lean.Meta.Grind.Arith.Linear.LinearM Lean.Meta.Grind.Arith.Linear.LinExpr
-- Mathlib.MeasureTheory.Measure.Doubling
/-- A variant of `IsUnifLocDoublingMeasure.doublingConstant` which allows for scaling the
radius by values other than `2`.  -/
IsUnifLocDoublingMeasure.scalingConstantOf : {α : Type u_1} →
  [inst : PseudoMetricSpace α] →
    [inst_1 : MeasurableSpace α] → (μ : MeasureTheory.Measure α) → [IsUnifLocDoublingMeasure μ] → ℝ → NNReal
-- Std.Internal.Do.WP.Lemmas
_private.Std.Internal.Do.WP.Lemmas.0.OptionT.orElse.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : (a : α) → motive (some a))
  (h_2 : (x : Option α) → motive x),
  (match some a with
    | some a => h_1 a
    | x => h_2 x) =
    h_1 a
-- Init.Data.Int.DivMod.Lemmas
Int.sign_eq_fdiv_abs : ∀ (a : ℤ), a.sign = a.fdiv ↑a.natAbs
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Under.pushout_obj_right : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T)
  [inst_1 : Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [inst_2 : P.HasPushoutsAlong f]
  [inst_3 : P.IsStableUnderCobaseChangeAlong f] [inst_4 : Q.IsStableUnderCobaseChange] (A : P.Under Q X),
  ((CategoryTheory.MorphismProperty.Under.pushout P Q f).obj A).right = CategoryTheory.Limits.pushout A.hom f
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Path.isPath : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Path u v), (↑p).IsPath
-- Batteries.Tactic.Congr
/-- Apply congruence (recursively) to goals of the form `⊢ f as = f bs` and `⊢ f as ≍ f bs`.
The optional parameter is the depth of the recursive applications.
This is useful when `congr` is too aggressive in breaking down the goal.
For example, given `⊢ f (g (x + y)) = f (g (y + x))`,
`congr` produces the goals `⊢ x = y` and `⊢ y = x`,
while `congr 2` produces the intended `⊢ x + y = y + x`.
 -/
Batteries.Tactic.congrConfig : Lean.ParserDescr
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.Weight.mk.congr_simp : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (toFun toFun_1 : L → R) (e_toFun : toFun = toFun_1)
  (genWeightSpace_ne_bot' : LieModule.genWeightSpace M toFun ≠ ⊥),
  { toFun := toFun, genWeightSpace_ne_bot' := genWeightSpace_ne_bot' } =
    { toFun := toFun_1, genWeightSpace_ne_bot' := ⋯ }
-- Init.Data.List.Lemmas
List.filterMap_flatMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : List α} {g : α → List β} {f : β → Option γ},
  List.filterMap f (List.flatMap g l) = List.flatMap (fun a => List.filterMap f (g a)) l
-- Init.Grind.ToInt
Lean.Grind.IntInterval.io.sizeOf_spec : ∀ (hi : ℤ), sizeOf (Lean.Grind.IntInterval.io hi) = 1 + sizeOf hi
-- Mathlib.Order.WithBot
WithBot.ge_of_forall_gt_iff_ge : ∀ {α : Type u_1} [inst : LinearOrder α] {x y : WithBot α} [DenselyOrdered α] [NoMinOrder α],
  (∀ (z : α), ↑z < x → ↑z ≤ y) ↔ x ≤ y
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Lean.Meta.Grind.Arith.Cutsat.getVar : Int.Internal.Linear.Var → Lean.Meta.Grind.GoalM Lean.Expr
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_eq_some : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α],
  m.WF → ∀ {k : α}, k ∈ m → m.getKey? k = some k
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get?.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeMap α β cmp),
  t = t_1 → ∀ (a a_1 : α), a = a_1 → t.get? a = t_1.get? a_1
-- Mathlib.LinearAlgebra.Basis.VectorSpace
/-- Auxiliary definition: the index for the new basis vectors in `Basis.sumExtend`.

The specific value of this definition should be considered an implementation detail.  -/
Module.Basis.sumExtendIndex : {ι : Type u_1} →
  {K : Type u_3} →
    {V : Type u_4} →
      [inst : DivisionRing K] →
        [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → {v : ι → V} → LinearIndependent K v → Set V
-- Mathlib.Algebra.Opposites
MulOpposite.exists : ∀ {α : Type u_1} {p : αᵐᵒᵖ → Prop}, (∃ a, p a) ↔ ∃ a, p (MulOpposite.op a)
-- Mathlib.SetTheory.Cardinal.Order
/-- **Alias** of `Cardinal.IsStrongLimit.isStrongPrelimit`. -/
Cardinal.IsStrongLimit.two_power_lt : ∀ {c : Cardinal.{u_1}}, c.IsStrongLimit → c.IsStrongPrelimit
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.sum_eq_foldr : ∀ {M : Type u_3} [inst : AddCommMonoid M] (s : Multiset M), s.sum = Multiset.foldr (fun x1 x2 => x1 + x2) 0 s
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
DirectedOn.le_csInf_iff : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderInf α] {s : Set α} {a : α},
  DirectedOn (fun x1 x2 => x2 ≤ x1) s → BddBelow s → s.Nonempty → (a ≤ sInf s ↔ ∀ b ∈ s, a ≤ b)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The tangent of an angle in a right-angled triangle multiplied by the adjacent side equals
the opposite side.  -/
EuclideanGeometry.tan_oangle_left_mul_dist_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.oangle p₃ p₁ p₂).tan * dist p₁ p₂ = dist p₃ p₂
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isLittleO_norm_pow_id : ∀ {E' : Type u_6} [inst : SeminormedAddCommGroup E'] {n : ℕ}, 1 < n → (fun x => ‖x‖ ^ n) =o[nhds 0] fun x => x
-- Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
/-- Given an `n`-th primitive root of unity `ζ`, where `1 < n`, we have that `ζ - 1` divides `n`.
In particular, if `ζ` is a `p`-th primitive root of unity with `p` prime, then `ζ - 1` divides
`p`.  -/
IsPrimitiveRoot.sub_one_dvd_natCast : ∀ {n : ℕ} {A : Type u_1} {ζ : A} [inst : CommRing A] [IsDomain A], IsPrimitiveRoot ζ n → 1 < n → ζ - 1 ∣ ↑n
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.refl : ∀ {n : ℕ} (a : ℕ), a ≡ a [MOD n]
-- Mathlib.Data.List.Pairwise
List.Pairwise.rel_head_tail : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α} {a : α}, List.Pairwise R l → ∀ (ha : a ∈ l.tail), R (l.head ⋯) a
-- Mathlib.LinearAlgebra.Matrix.Permutation
/-- The determinant of a permutation matrix equals its sign.  -/
Matrix.det_permutation : ∀ {n : Type u_1} {R : Type u_2} [inst : DecidableEq n] (σ : Equiv.Perm n) [inst_1 : Fintype n] [inst_2 : CommRing R],
  (Equiv.Perm.permMatrix R σ).det = ↑↑(Equiv.Perm.sign σ)
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.blsub_eq_blsub : ∀ {ι : Type u} (r r' : ι → ι → Prop) [inst : IsWellOrder ι r] [inst_1 : IsWellOrder ι r'] (f : ι → Ordinal.{max u v}),
  (Ordinal.type r).blsub (Ordinal.bfamilyOfFamily' r f) = (Ordinal.type r').blsub (Ordinal.bfamilyOfFamily' r' f)
-- Mathlib.CategoryTheory.WithTerminal.FinCategory
CategoryTheory.WithTerminal.instFintype : (C : Type u) → [Fintype C] → Fintype (CategoryTheory.WithTerminal C)
-- Mathlib.Analysis.Convex.Function
/-- A function `-f` is strictly concave iff `f` is strictly convex.  -/
neg_strictConcaveOn_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  {s : Set E} {f : E → β}, StrictConcaveOn 𝕜 s (-f) ↔ StrictConvexOn 𝕜 s f
-- Init.Data.List.MinMaxIdx
List.lt_length_of_maxIdxOn?_eq_some : ∀ {β : Type u_1} {α : Type u_2} {i : ℕ} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α},
  List.maxIdxOn? f xs = some i → i < xs.length