mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.MinMaxIdx
List.le_maxIdxOn_of_apply_getElem_lt_apply_getElem : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [inst_2 : LT β] [Std.IsLinearPreorder β]
  [Std.LawfulOrderLT β] {f : α → β} {xs : List α} (h : xs ≠ []) {i : ℕ} (hi : i < xs.length),
  (∀ (j : ℕ) (x : j < i), f xs[j] < f xs[i]) → i ≤ List.maxIdxOn f xs h
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.one_left : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N}, SemidirectProduct.left 1 = 1
-- Mathlib.LinearAlgebra.FreeModule.Basic
/-- If `Module.Free R M` then `chooseBasis : ι → M` is the basis.
Here `ι = ChooseBasisIndex R M`.  -/
Module.Free.chooseBasis : (R : Type u) →
  (M : Type v) →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → [inst_3 : Module.Free R M] → Module.Basis (Module.Free.ChooseBasisIndex R M) R M
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.factor_δ.eq_1 : ∀ {m n : ℕ} (f : { len := m } ⟶ { len := n + 1 }) (j : Fin (n + 2)),
  SimplexCategory.factor_δ f j = CategoryTheory.CategoryStruct.comp f (SimplexCategory.σ (Fin.predAbove 0 j))
-- Mathlib.Order.Filter.Pointwise
Filter.commSemigroup.eq_1 : ∀ {α : Type u_2} [inst : CommSemigroup α], Filter.commSemigroup = { toSemigroup := Filter.semigroup, mul_comm := ⋯ }
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.mker_one : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N], MonoidHom.mker 1 = ⊤
-- Lean.Parser.Command
Lean.Parser.Command.optDeriving.formatter : Lean.PrettyPrinter.Formatter
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Expr.toPolyC.go.match_4.eq_6 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (a b : Lean.Grind.CommRing.Expr)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_3 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)),
  (match a.mul b with
    | Lean.Grind.CommRing.Expr.num k => h_1 k
    | Lean.Grind.CommRing.Expr.natCast k => h_2 k
    | Lean.Grind.CommRing.Expr.intCast k => h_3 k
    | Lean.Grind.CommRing.Expr.var x => h_4 x
    | a.add b => h_5 a b
    | a.mul b => h_6 a b
    | a.neg => h_7 a
    | a.sub b => h_8 a b
    | a.pow k => h_9 a k) =
    h_6 a b
-- Mathlib.Topology.Sets.Order
/-- See Note [custom simps projection].  -/
ClopenUpperSet.Simps.coe : {α : Type u_1} → [inst : TopologicalSpace α] → [inst_1 : LE α] → ClopenUpperSet α → Set α
-- Mathlib.SetTheory.ZFC.PSet
/-- The underlying pre-set family of a pre-set  -/
PSet.Func : (x : PSet.{u_1}) → x.Type → PSet.{u_1}
-- Std.Data.Iterators.Combinators.Monadic.Drop
_private.Std.Data.Iterators.Combinators.Monadic.Drop.0.Std.Iterators.Types.Drop.instFinitenessRelation : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Std.Iterator α m β] →
        [inst_1 : Monad m] →
          [Std.Iterators.Finite α m] → Std.Iterators.FinitenessRelation (Std.Iterators.Types.Drop α m β) m
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
/-- The natural `R`-algebra homomorphism from the unitization of a non-unital subalgebra into
the algebra containing it.  -/
NonUnitalSubalgebra.unitization : {R : Type u_1} →
  {S : Type u_2} →
    {A : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : SetLike S A] →
              [hSA : NonUnitalSubsemiringClass S A] → [hSRA : SMulMemClass S R A] → (s : S) → Unitization R ↥s →ₐ[R] A
-- Mathlib.Order.Category.BddLat
/-- `latToBddLat` is left adjoint to the forgetful functor, meaning it is the free
functor from `Lat` to `BddLat`.  -/
latToBddLatForgetAdjunction : latToBddLat ⊣ CategoryTheory.forget₂ BddLat Lat
-- Init.Data.Ord.Basic
Ordering.instDecidableForallOfDecidablePred : {p : Ordering → Prop} → [DecidablePred p] → Decidable (∀ (o : Ordering), p o)
-- Mathlib.Algebra.Group.Submonoid.Saturation
Submonoid.MulSaturated.iInf : ∀ {M : Type u_1} [inst : MulOneClass M] {ι : Sort u_2} {f : ι → Submonoid M},
  (∀ (i : ι), (f i).MulSaturated) → (iInf f).MulSaturated
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.closure_le_toAddSubmonoid_span : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Set M},
  AddSubmonoid.closure s ≤ (Submodule.span R s).toAddSubmonoid
-- Mathlib.LinearAlgebra.Dimension.Constructions
LinearIndepOn.union_of_quotient : ∀ {R : Type u} {M : Type v} {ι : Type w} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {s t : Set ι}
  {f : ι → M},
  LinearIndepOn R f s → LinearIndepOn R (⇑(Submodule.span R (f '' s)).mkQ ∘ f) t → LinearIndepOn R f (s ∪ t)
-- Mathlib.Logic.Function.ULift
ULift.down_inj : ∀ {α : Type u_1} {a b : ULift.{u_2, u_1} α}, a.down = b.down ↔ a = b
-- Mathlib.Data.List.Permutation
List.mem_permutationsAux_of_perm : ∀ {α : Type u_1} {ts is l : List α},
  l.Perm (is ++ ts) → (∃ is', ∃ (_ : is'.Perm is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux is
-- Mathlib.Probability.Distributions.Gaussian.Multivariate
ProbabilityTheory.variance_dual_stdGaussian : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] (L : StrongDual ℝ E),
  ProbabilityTheory.variance (⇑L) (ProbabilityTheory.stdGaussian E) = ‖L‖ ^ 2
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.liftEquiv_mk : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] (N : Subgroup G) [nN : N.Normal] {φ : G →* H}
  (hφ : Function.Surjective ⇑φ) (HN : N = φ.ker) (g : G), (QuotientGroup.liftEquiv N hφ HN) ↑g = φ g
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instInhabitedLetDecl.default : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.LetDecl pu
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
SimpleGraph.Finsubgraph.instHImp : {V : Type u} → {G : SimpleGraph V} → [Finite V] → HImp G.Finsubgraph
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.triangleIso_assoc : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B)
  (G : CategoryTheory.Functor B C) {Z : CategoryTheory.Functor A C} (h : F.comp G ≅ Z),
  F.associator (CategoryTheory.Functor.id B) G ≪≫ F.isoWhiskerLeft G.leftUnitor ≪≫ h =
    CategoryTheory.Functor.isoWhiskerRight F.rightUnitor G ≪≫ h
-- Mathlib.Algebra.Order.Field.Basic
div_nonneg_iff : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α},
  0 ≤ a / b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
-- Lean.Elab.Parallel
/-- Runs a list of TermElabM computations in parallel and returns:
* a combined cancellation hook for all tasks, and
* an iterator that yields results in completion order (greedily).

The iterator runs in TermElabM, and as it yields each result, it updates the TermElabM state
to reflect the state when that particular task completed. This means the state is
threaded through the iteration in task completion order.

Results are wrapped in `Except Exception α` so that errors in individual tasks don't stop
the iteration - you can observe all results including which tasks failed.

The iterator will terminate after all jobs complete (assuming they all do complete).
 -/
Lean.Elab.Term.TermElabM.parIterGreedyWithCancel : {α : Type} →
  List (Lean.Elab.TermElabM α) →
    Lean.Elab.TermElabM (BaseIO PUnit.{1} × Std.IterM Lean.Elab.TermElabM (Except Lean.Exception α))
-- Mathlib.Geometry.Manifold.Instances.Real
/-- The half-space in `ℝ^n`, used to model manifolds with boundary. We only define it when
`1 ≤ n`, as the definition only makes sense in this case.
 -/
EuclideanHalfSpace : (n : ℕ) → [NeZero n] → Type
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- Endowing the space `PiLp p β` with the `L^p` distance. We register this instance
separate from `pi_Lp.pseudo_metric` since the latter requires the type class hypothesis
`[Fact (1 ≤ p)]` in order to prove the triangle inequality.

Registering this separately allows for a future metric-like structure on `PiLp p β` for `p < 1`
satisfying a relaxed triangle inequality. The terminology for this varies throughout the
literature, but it is sometimes called a *quasi-metric* or *semi-metric*.  -/
PiLp.instDist : (p : ENNReal) → {ι : Type u_2} → (α : ι → Type u_3) → [Fintype ι] → [(i : ι) → Dist (α i)] → Dist (PiLp p α)
-- Mathlib.NumberTheory.FLT.Three
/-- Given `S : Solution`, we let `S.w` be any element such that `S.c = λ ^ S.multiplicity * S.w`  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.w : {K : Type u_1} →
  [inst : Field K] →
    {ζ : K} → {hζ : IsPrimitiveRoot ζ 3} → FermatLastTheoremForThreeGen.Solution✝ hζ → NumberField.RingOfIntegers K
-- Lean.Meta.Sym.Pattern
/-- Context for structural definitional equality (`isDefEqS`).
 -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.DefEqM.Context : Type
-- Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts
CategoryTheory.Limits.pointwiseBinaryBicone_inl_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u_2} [inst_3 : CategoryTheory.Category.{v_2, u_2} D]
  (F G : CategoryTheory.Functor D C) (X : D),
  (CategoryTheory.Limits.pointwiseBinaryBicone F G).inl.app X = CategoryTheory.Limits.biprod.inl
-- Init.Data.BitVec.Lemmas
BitVec.toFin_and : ∀ {v : ℕ} (x y : BitVec v), (x &&& y).toFin = x.toFin &&& y.toFin
-- Init.Data.Array.Range
Array.unzip_zipIdx_eq_prod : ∀ {α : Type u_1} {xs : Array α} {i : ℕ}, (xs.zipIdx i).unzip = (xs, Array.range' i xs.size)
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.ι_naturality_apply : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} (c : F.CoconeTypes)
  {j j' : J} (f : j ⟶ j') (x : F.obj j), c.ι j' ((CategoryTheory.ConcreteCategory.hom (F.map f)) x) = c.ι j x
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.invVeblen₁_zero : Ordinal.invVeblen₁ 0 = 0
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.RootPositiveForm.rootLength_pos : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing S]
  [inst_1 : LinearOrder S] [inst_2 : CommRing R] [inst_3 : Algebra S R] [inst_4 : AddCommGroup M] [inst_5 : Module R M]
  [inst_6 : AddCommGroup N] [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsValuedIn S]
  (B : RootPairing.RootPositiveForm S P) [inst_9 : FaithfulSMul S R] [inst_10 : Module S M]
  [inst_11 : IsScalarTower S R M] (i : ι), 0 < B.rootLength i
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.mk.inj : ∀ {R : Type u} {M : Type v} {N : Type w} {inst : CommSemiring R} {inst_1 : AddCommMonoid M} {inst_2 : Module R M}
  {inst_3 : AddCommMonoid N} {inst_4 : Module R N} {toFun : M → N}
  {toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x}
  {exists_companion' : ∃ B, ∀ (x y : M), toFun (x + y) = toFun x + toFun y + (B x) y} {toFun_1 : M → N}
  {toFun_smul_1 : ∀ (a : R) (x : M), toFun_1 (a • x) = (a * a) • toFun_1 x}
  {exists_companion'_1 : ∃ B, ∀ (x y : M), toFun_1 (x + y) = toFun_1 x + toFun_1 y + (B x) y},
  { toFun := toFun, toFun_smul := toFun_smul, exists_companion' := exists_companion' } =
      { toFun := toFun_1, toFun_smul := toFun_smul_1, exists_companion' := exists_companion'_1 } →
    toFun = toFun_1
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
CategoryTheory.Adjunction.instIsIsoAppCounitOfFullOfFaithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [R.Full] [R.Faithful] (X : D),
  CategoryTheory.IsIso (h.counit.app X)
-- Mathlib.GroupTheory.OrderOfElement
AddRightCancelMonoid.nsmul_inj_iff_of_addOrderOf_eq_zero : ∀ {G : Type u_1} [inst : AddRightCancelMonoid G] {x : G}, addOrderOf x = 0 → ∀ {n m : ℕ}, n • x = m • x ↔ n = m
-- Mathlib.Data.Nat.Cast.Order.Ring
/-- Specialisation of `Nat.cast_nonneg'`, which seems to be easier for Lean to use.  -/
Nat.cast_nonneg : ∀ {α : Type u_3} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α] (n : ℕ), 0 ≤ ↑n
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.bot_arrow : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {B : C}, ⊥.arrow = 0
-- Batteries.Data.List.Lemmas
List.dropPrefix?_nil : ∀ {α : Type u_1} [inst : BEq α] {p : List α}, p.dropPrefix? [] = some p
-- Init.Data.Ord.Array
_private.Init.Data.Ord.Array.0.Array.compareLex.go.induct : ∀ {α : Type u_1} (cmp : α → α → Ordering) (a₁ a₂ : Array α) (motive : ℕ → Prop),
  (∀ (x : ℕ), a₁.size ≤ x → a₂.size ≤ x → motive x) →
    (∀ (x : ℕ), a₁.size ≤ x → ¬a₂.size ≤ x → motive x) →
      (∀ (x : ℕ), ¬a₁.size ≤ x → a₂.size ≤ x → motive x) →
        (∀ (x : ℕ) (h : ¬a₁.size ≤ x) (h_1 : ¬a₂.size ≤ x), cmp a₁[x] a₂[x] = Ordering.lt → motive x) →
          (∀ (x : ℕ) (h : ¬a₁.size ≤ x) (h_1 : ¬a₂.size ≤ x),
              cmp a₁[x] a₂[x] = Ordering.eq → motive (x + 1) → motive x) →
            (∀ (x : ℕ) (h : ¬a₁.size ≤ x) (h_1 : ¬a₂.size ≤ x), cmp a₁[x] a₂[x] = Ordering.gt → motive x) →
              ∀ (i : ℕ), motive i
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.restrictFunctorId_hom_app_app : ∀ {X : AlgebraicGeometry.Scheme} {M : X.Modules} {U : X.Opens},
  AlgebraicGeometry.Scheme.Modules.Hom.app (AlgebraicGeometry.Scheme.Modules.restrictFunctorId.hom.app M) U =
    M.presheaf.map (CategoryTheory.eqToHom ⋯).op
-- Mathlib.Algebra.Group.Subgroup.Basic
AddGroup.addConjugatesOfSet_subset : ∀ {G : Type u_1} [inst : AddGroup G] {s : Set G} {N : AddSubgroup G} [N.Normal],
  s ⊆ ↑N → AddGroup.addConjugatesOfSet s ⊆ ↑N
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Get the first `i` elements of the set, counted from the left.

```
take 2 {a, b, c, d} = {a, b}
take 5 {a, b, c, d} = {a, b, c, d}
```  -/
Ordnode.take : {α : Type u_1} → ℕ → Ordnode α → Ordnode α
-- Mathlib.Data.Ordmap.Invariants
Ordnode.balancedSz_down : ∀ {l r₁ r₂ : ℕ}, r₁ ≤ r₂ → l + r₂ ≤ 1 ∨ l ≤ Ordnode.delta * r₁ → Ordnode.BalancedSz l r₂ → Ordnode.BalancedSz l r₁
-- Mathlib.Order.SupClosed
/-- A set `s` is *sup-closed* if `a ⊔ b ∈ s` for all `a ∈ s`, `b ∈ s`.  -/
SupClosed : {α : Type u_3} → [SemilatticeSup α] → Set α → Prop
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
SzemerediRegularity.initialBound_pos : ∀ (ε : ℝ) (l : ℕ), 0 < SzemerediRegularity.initialBound ε l
-- Init.Grind.Config
Lean.Grind.ConfigInteractive.mk.injEq : ∀ (toConfig toConfig_1 : Lean.Grind.Config),
  ({ toConfig := toConfig } = { toConfig := toConfig_1 }) = (toConfig = toConfig_1)
-- Mathlib.Algebra.Colimit.Finiteness
Module.fgSystem.instIsDirectedOrderSubtypeSubmoduleFG : ∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  IsDirectedOrder { N // N.FG }
-- Mathlib.Data.Nat.Choose.Sum
/-- The **binomial theorem**  -/
add_pow : ∀ {R : Type u_1} [inst : CommSemiring R] (x y : R) (n : ℕ),
  (x + y) ^ n = ∑ m ∈ Finset.range (n + 1), x ^ m * y ^ (n - m) * ↑(n.choose m)
-- Std.Http.Data.Body.Full
/-- Returns `true` when the data has been consumed or the body has been closed.
 -/
Std.Http.Body.Full.isClosed : Std.Http.Body.Full → Std.Async.Async Bool
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz
SimpleGraph.zarankiewicz_of_fintypeCard_eq : ∀ {m n s t : ℕ} {V : Type u_1} {W : Type u_2} {α : Type u_3} {β : Type u_4} [inst : Fintype V] [inst_1 : Fintype W]
  [inst_2 : Fintype α] [inst_3 : Fintype β],
  Fintype.card V = m →
    Fintype.card W = n →
      Fintype.card α = s →
        Fintype.card β = t →
          SimpleGraph.zarankiewicz m n s t =
            {G | G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G}.sup fun x => x.edgeFinset.card
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.apply_apply' : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂] (v : E)
  (f : E →SL[σ₁₂] F), ((ContinuousLinearMap.apply' F σ₁₂) v) f = f v
-- Mathlib.Algebra.Squarefree.Basic
Squarefree.gcd_right : ∀ {α : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] (a : α) {b : α},
  Squarefree b → Squarefree (gcd a b)
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
MonoidHom.map_multiset_prod : ∀ {M : Type u_5} {N : Type u_6} [inst : CommMonoid M] [inst_1 : CommMonoid N] (f : M →* N) (s : Multiset M),
  f s.prod = (Multiset.map (⇑f) s).prod
-- Mathlib.Data.ZMod.Basic
ZMod.cast_intCast' : ∀ {n : ℕ} {R : Type u_1} [inst : Ring R] [CharP R n] (k : ℤ), (↑k).cast = ↑k
-- Init.Data.SInt.Lemmas
Int8.sub_lt : ∀ {a b : Int8}, 0 < b → b ≤ a → a - b < a
-- Mathlib.Analysis.Polynomial.CauchyBound
Polynomial.cauchyBound_X_add_C : ∀ {K : Type u_1} [inst : NormedDivisionRing K] (x : K), (Polynomial.X + Polynomial.C x).cauchyBound = ‖x‖₊ + 1
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
/-- If a property of a germ of function `g` on a pointed set `(s, x)` is invariant under the
structure groupoid (by composition in the source space and in the target space), then
expressing it in charted spaces does not depend on the element of the maximal atlas one uses
both in the source and in the target manifolds, provided they are defined around `x` and `g x`
respectively, and provided `g` is continuous within `s` at `x` (otherwise, the local behavior
of `g` at `x` cannot be captured with a chart in the target). Version where one of the
charts is `chartAt`.  -/
StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_aux' : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
  {e : OpenPartialHomeomorph M H} {f : OpenPartialHomeomorph M' H'} {P : (H → H') → Set H → H → Prop} {g : M → M'}
  {s : Set M} {x : M},
  G.LocalInvariantProp G' P →
    e ∈ StructureGroupoid.maximalAtlas M G →
      x ∈ e.source →
        f ∈ StructureGroupoid.maximalAtlas M' G' →
          g x ∈ f.source →
            ContinuousWithinAt g s x →
              (P (↑(chartAt H' (g x)) ∘ g ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x) ↔
                P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x))
-- Mathlib.Topology.Semicontinuity.Defs
UpperHemicontinuousOn.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace γ]
  [inst_2 : TopologicalSpace β] {f : α → Set β} {s : Set α} {g : γ → α} {t : Set γ},
  UpperHemicontinuousOn f s → ContinuousOn g t → Set.MapsTo g t s → UpperHemicontinuousOn (f ∘ g) t
-- Mathlib.CategoryTheory.Limits.Creates
/-- If `F` reflects isomorphisms and we can lift any colimit cocone to a colimit cocone,
then `F` creates colimits.
In particular here we don't need to assume that F reflects colimits.
 -/
CategoryTheory.createsColimitOfReflectsIso : {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] →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                [F.ReflectsIsomorphisms] →
                  ((c : CategoryTheory.Limits.Cocone (K.comp F)) →
                      (t : CategoryTheory.Limits.IsColimit c) → CategoryTheory.LiftsToColimit K F c t) →
                    CategoryTheory.CreatesColimit K F
-- Mathlib.Data.PNat.Defs
instOnePNat : One ℕ+
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.instDecidableAllOfDecidablePred : {α : Type u_1} → {p : α → Prop} → {t : RBTree.RBNode α} → [DecidablePred p] → Decidable (RBTree.RBNode.All p t)
-- Mathlib.Order.Antisymmetrization
instTransAntisymmRelLe : {α : Type u_1} →
  [inst : Preorder α] → Trans (AntisymmRel fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2
-- Lean.Data.Format
Lean.Std.Format.getWidth : Lean.Options → ℕ
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.ae_restrict_iff' : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {p : α → Prop},
  MeasurableSet s → ((∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → p x)
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
fixingSubgroup.eq_1 : ∀ (M : Type u_1) {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] (s : Set α),
  fixingSubgroup M s = { toSubmonoid := fixingSubmonoid M s, inv_mem' := ⋯ }
-- Mathlib.Algebra.Group.Pi.Lemmas
Function.const_eq_one : ∀ {ι : Type u_1} {α : Type u_2} [inst : One α] [Nonempty ι] {a : α}, Function.const ι a = 1 ↔ a = 1
-- Std.Data.Iterators.Lemmas.Equivalence.StepCongr
/-- This function is used in lemmas about iterator equivalence (`Iter.Equiv` and `IterM.Equiv`).

Returns an `IterStep` from an `IterM.QuotStep`, discarding the `IsPlausibleStep` proof.
It commutes with `IterStep.bundledQuotient` and `Quot.mk _ : it.Step → it.QuotStep`.
 -/
Std.IterM.QuotStep.bundledQuotient : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      [inst : Std.Iterator α m β] →
        [inst_1 : Monad m] →
          [inst_2 : LawfulMonad m] →
            {it : Std.IterM m β} → it.QuotStep → Std.IterStep (Quot (Std.BundledIterM.Equiv m β)) β
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- **Alias** of the forward direction of `orthogonalFamily_iff_pairwise`. -/
OrthogonalFamily.pairwise : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {V : ι → Submodule 𝕜 E},
  (OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ) → Pairwise (Function.onFun (fun x1 x2 => x1 ⟂ x2) V)
-- Mathlib.Topology.Instances.Rat
Rat.dist_cast : ∀ (x y : ℚ), dist ↑x ↑y = dist x y
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wf_diff₀ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m₁ m₂ : Std.DHashMap.Raw α β} {h₁ : 0 < m₁.buckets.size} {h₂ : 0 < m₂.buckets.size},
  m₁.WF → (↑(Std.DHashMap.Internal.Raw₀.diff ⟨m₁, h₁⟩ ⟨m₂, h₂⟩)).WF
-- Mathlib.Data.Tree.Basic
BinaryTree.right.eq_2 : ∀ {α : Type u} (a : α) (l r : BinaryTree α), (BinaryTree.node a l r).right = r
-- Mathlib.Algebra.Algebra.Opposite
MulOpposite.algebraMap_apply : ∀ {R : Type u_1} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (c : R),
  (algebraMap R Aᵐᵒᵖ) c = MulOpposite.op ((algebraMap R A) c)
-- Mathlib.Logic.Equiv.Defs
Equiv.ofBijective_apply : ∀ {α : Sort u} {β : Sort v} (f : α → β) (hf : Function.Bijective f) (a : α), (Equiv.ofBijective f hf) a = f a
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.p_fromOpcycles : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ),
  CategoryTheory.CategoryStruct.comp (X.pOpcycles f g n) (X.fromOpcycles f g fg h n) =
    (X.H n).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)