mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Vector.MapLemmas
/-- If an accumulation function `f`, given an initial state `s`, produces `s` as its output state
for all possible input bits, then the state is redundant and can be optimized out.
 -/
List.Vector.mapAccumr_eq_map_of_constant_state : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_5} {n : ℕ} {xs : List.Vector α n} (f : α → σ → σ × β) (s : σ),
  (∀ (a : α), (f a s).1 = s) → List.Vector.mapAccumr f xs s = (s, List.Vector.map (fun x => (f x s).2) xs)
-- Mathlib.Algebra.Category.Semigrp.Basic
MulEquiv.toSemigrpIso.eq_1 : ∀ {X Y : Type u} [inst : Semigroup X] [inst_1 : Semigroup Y] (e : X ≃* Y),
  e.toSemigrpIso =
    { hom := Semigrp.ofHom e.toMulHom, inv := Semigrp.ofHom e.symm.toMulHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.Topology.Category.Profinite.Product
ContinuousMap.precomp.eq_1 : ∀ {I : Type u_5} {X : I → Type u_7} [inst : (i : I) → TopologicalSpace (X i)] {ι : Type u_9} (φ : ι → I),
  ContinuousMap.precomp φ = { toFun := fun f j => f (φ j), continuous_toFun := ⋯ }
-- Mathlib.Data.List.Zip
List.length_revzip : ∀ {α : Type u} (l : List α), l.revzip.length = l.length
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.of_forall_constGet?_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [Std.LawfulEqOrd α],
  t₁.WF →
    t₂.WF →
      (∀ (k : α), Std.DTreeMap.Internal.Impl.Const.get? t₁ k = Std.DTreeMap.Internal.Impl.Const.get? t₂ k) → t₁.Equiv t₂
-- Mathlib.RingTheory.PowerBasis
PowerBasis.algHom_ext : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {S' : Type u_7}
  [inst_3 : Semiring S'] [inst_4 : Algebra R S'] (pb : PowerBasis R S) ⦃f g : S →ₐ[R] S'⦄, f pb.gen = g pb.gen → f = g
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- Auxiliary construction to obtain the additive group structure on the limit of
profinite additive groups.  -/
ProfiniteAddGrp.limitConePtAux : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J ProfiniteAddGrp.{max v u}) → AddSubgroup ((j : J) → ↑(F.obj j).toProfinite.toTop)
-- Mathlib.Data.Matrix.Basis
Matrix.single.eq_1 : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_7} [inst : DecidableEq m] [inst_1 : DecidableEq n] [inst_2 : Zero α] (i : m)
  (j : n) (a : α), Matrix.single i j a = Matrix.of fun i' j' => if i = i' ∧ j = j' then a else 0
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
/-- If `X ⟶ Y` with `Y` being a strict terminal object, then `X` is also a terminal object.  -/
CategoryTheory.Limits.IsTerminal.ofStrict : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasStrictTerminalObjects C] →
      {X Y : C} → (X ⟶ Y) → CategoryTheory.Limits.IsTerminal X → CategoryTheory.Limits.IsTerminal Y
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Cache.WF.brecOn : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α]
  {motive :
    (a : Array (Std.Sat.AIG.Decl α)) → (a_1 : Std.HashMap (Std.Sat.AIG.Decl α) ℕ) → Std.Sat.AIG.Cache.WF a a_1 → Prop}
  {a : Array (Std.Sat.AIG.Decl α)} {a_1 : Std.HashMap (Std.Sat.AIG.Decl α) ℕ} (t : Std.Sat.AIG.Cache.WF a a_1),
  (∀ (a : Array (Std.Sat.AIG.Decl α)) (a_2 : Std.HashMap (Std.Sat.AIG.Decl α) ℕ) (t : Std.Sat.AIG.Cache.WF a a_2),
      Std.Sat.AIG.Cache.WF.below t → motive a a_2 t) →
    motive a a_1 t
-- Mathlib.Algebra.Star.NonUnitalSubsemiring
NonUnitalStarSubsemiring.instNonUnitalSubsemiringClass : ∀ {R : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : StarRing R],
  NonUnitalSubsemiringClass (NonUnitalStarSubsemiring R) R
-- Std.Data.DTreeMap.Internal.Operations
/-- Iterate over `l` and insert all of its elements into `t`.  -/
Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit : {α : Type u} →
  [inst : Ord α] →
    {ρ : Type w} →
      [ForIn Id ρ α] →
        (t : Std.DTreeMap.Internal.Impl α fun x => Unit) →
          ρ → t.Balanced → Std.DTreeMap.Internal.Impl.Const.IteratedUnitInsertionInto t
-- Mathlib.Analysis.Normed.Lp.lpHolder
lp.holder.congr_simp : ∀ {ι : Type u_1} {𝕜 : Type u_2} {E : ι → Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} [inst : RCLike 𝕜]
  [inst_1 : (i : ι) → NormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : (i : ι) → NormedAddCommGroup (F i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F i)]
  [inst_5 : (i : ι) → NormedAddCommGroup (G i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (G i)] {p q : ENNReal} (r : ENNReal)
  [hpqr : p.HolderTriple q r] (B B_1 : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) (e_B : B = B_1) {K K_1 : ℝ} (e_K : K = K_1)
  (hBK : ∀ (i : ι), ‖B i‖ ≤ K) (e e_1 : ↥(lp E p)),
  e = e_1 → ∀ (f f_1 : ↥(lp F q)), f = f_1 → lp.holder r B hBK e f = lp.holder r B_1 ⋯ e_1 f_1
-- Mathlib.Order.SuccPred.Limit
Order.isMax_or_mem_range_pred_or_isPredLimit : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] (a : α),
  IsMax a ∨ a ∈ Set.range Order.pred ∨ Order.IsPredLimit a
-- Init.Data.List.TakeDrop
List.ne_nil_of_drop_ne_nil : ∀ {α : Type u_1} {as : List α} {i : ℕ}, List.drop i as ≠ [] → as ≠ []
-- Lean.Parser.Do
Lean.Parser.Term.doSeqBracketed.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Fin.val.hcongr_2 : ∀ (n n' : ℕ), n = n' → ∀ (self : Fin n) (self' : Fin n'), self ≍ self' → ↑self ≍ ↑self'
-- Std.Async.Timer
_private.Std.Async.Timer.0.Std.Async.Interval.ofNative.sizeOf_spec : ∀ (native : Std.Internal.UV.Timer), sizeOf { native := native } = 1 + sizeOf native
-- Mathlib.Logic.Function.Iterate
Function.iterate_cancel : ∀ {α : Type u} {f : α → α} {m n : ℕ} {a : α}, Function.Injective f → f^[m] a = f^[n] a → f^[m - n] a = a
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.comp_of_natDegree_le_one_of_monic : ∀ {R : Type u_1} [inst : CommSemiring R] {f g : Polynomial R}, f.Splits → g.natDegree ≤ 1 → g.Monic → (f.comp g).Splits
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.beth_ne_zero : ∀ (o : Ordinal.{u_1}), Cardinal.beth o ≠ 0
-- Mathlib.Topology.AlexandrovDiscrete
nhdsKer_mem_nhdsSet : ∀ {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α] {s : Set α}, nhdsKer s ∈ nhdsSet s
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearMap.BilinForm.comp_comp : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type w}
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] {M'' : Type u_7} [inst_5 : AddCommMonoid M'']
  [inst_6 : Module R M''] (B : LinearMap.BilinForm R M'') (l r : M →ₗ[R] M') (l' r' : M' →ₗ[R] M''),
  (B.comp l' r').comp l r = B.comp (l' ∘ₗ l) (r' ∘ₗ r)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_modify_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ [Inhabited α] {k fallback : α} {f : β k → β k}, (t.modify k f).getKeyD k fallback = if k ∈ t then k else fallback
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
CategoryTheory.NormalEpiCategory.preservesMonomorphisms_of_preservesKernels : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasCokernels C]
  [CategoryTheory.IsNormalEpiCategory C] [CategoryTheory.Limits.HasZeroObject C] {D : Type u_2}
  [inst_6 : CategoryTheory.Category.{v_2, u_2} D] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms D]
  [CategoryTheory.Limits.HasZeroObject D] (F : CategoryTheory.Functor D C) [F.PreservesZeroMorphisms]
  [∀ {X Y : D} (f : X ⟶ Y), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F],
  F.PreservesMonomorphisms
-- Aesop.Builder.Basic
Aesop.PhaseSpec.norm.inj : ∀ {info info_1 : Aesop.NormRuleInfo}, Aesop.PhaseSpec.norm info = Aesop.PhaseSpec.norm info_1 → info = info_1
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.rawCh.parenthesizer : Char → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.projectionL_apply_left : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} (h : Submodule.IsTopCompl p q) (x : ↥p), (p.projectionL q h) ↑x = ↑x
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- The inf of two submodules, the second finite-dimensional, is
finite-dimensional.  -/
Submodule.finiteDimensional_inf_right : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (S₁ S₂ : Submodule K V) [FiniteDimensional K ↥S₂], FiniteDimensional K ↥(S₁ ⊓ S₂)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Antitone.const_add : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α} [AddLeftMono α],
  Antitone f → ∀ (a : α), Antitone fun x => a + f x
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RioSliceData.mk.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : SizeOf α] [inst_2 : SizeOf β]
  (treeMap : Std.DTreeMap.Internal.Impl α fun x => β) (range : Std.Rio α),
  sizeOf { treeMap := treeMap, range := range } = 1 + sizeOf treeMap + sizeOf range
-- Mathlib.Tactic.HigherOrder
/-- A user attribute that applies to lemmas of the shape `∀ x, f (g x) = h x`.
It derives an auxiliary lemma of the form `f ∘ g = h` for reasoning about higher-order functions.
 -/
Mathlib.Tactic.higherOrderGetParam : Lean.Name → Lean.Syntax → Lean.AttrM Lean.Name
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- The first projection `Triangle C ⥤ C`.  -/
CategoryTheory.Pretriangulated.Triangle.π₁ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] → CategoryTheory.Functor (CategoryTheory.Pretriangulated.Triangle C) C
-- Std.Http.Transport
/-- Receive data from the client connection, up to the expected size.
Returns None if the connection is closed or no data is available.
 -/
Std.Http.Transport.recv : {α : Type} → [self : Std.Http.Transport α] → α → UInt64 → Std.Async.Async (Option ByteArray)
-- Mathlib.Algebra.Quaternion
Quaternion.algebraMap_injective : ∀ {R : Type u_3} [inst : CommRing R], Function.Injective ⇑(algebraMap R (Quaternion R))
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.IsSwap.sign_eq : ∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α] {f : Equiv.Perm α}, f.IsSwap → Equiv.Perm.sign f = -1
-- Mathlib.RingTheory.Idempotents
_private.Mathlib.RingTheory.Idempotents.0.RingHom.prod_bijective_of_isIdempotentElem.match_1_1.eq_1 : ∀ (motive : Fin 2 → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1),
  (match 0 with
    | 0 => h_1 ()
    | 1 => h_2 ()) =
    h_1 ()
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.sameCycle_iff_cycleOf_eq_of_mem_support : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} {x y : α},
  x ∈ g.support → y ∈ g.support → (g.SameCycle x y ↔ g.cycleOf x = g.cycleOf y)
-- Lean.Expr
/-- If the expression is a constant, return that name.
Otherwise return `Name.anonymous`.
 -/
Lean.Expr.constName : Lean.Expr → Lean.Name
-- Mathlib.Algebra.Order.IsBotOne
IsBotOneClass.isBot_one : ∀ {α : Type u_1} {inst : LE α} {inst_1 : One α} [self : IsBotOneClass α], IsBot 1
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mapNatIso_inverse_obj_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S S' : CategoryTheory.Functor C D} (i : S ≅ S')
  (X : CategoryTheory.Comma S' (CategoryTheory.Functor.fromPUnit T)),
  ((CategoryTheory.CostructuredArrow.mapNatIso i).inverse.obj X).left = X.left
-- Std.Data.DHashMap.AdditionalOperations
/-- Updates the values of the hash map by applying the given function to all mappings, keeping
only those mappings where the function returns `some` value.
 -/
Std.DHashMap.filterMap : {α : Type u} →
  {β : α → Type v} →
    {δ : α → Type w} →
      [inst : BEq α] → [inst_1 : Hashable α] → ((a : α) → β a → Option (δ a)) → Std.DHashMap α β → Std.DHashMap α δ
-- Lean.Parser.Basic
Lean.Parser.CategoryParserFn : Type
-- Mathlib.Algebra.Module.Presentation.Basic
/-- the coefficients of the linear relations that are expected between the generators  -/
Module.Relations.relation : {A : Type u} → [inst : Ring A] → (self : Module.Relations A) → self.R → self.G →₀ A
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Real.differentiableAt_qaryEntropy : ∀ {q : ℕ} {p : ℝ}, p ≠ 0 → p ≠ 1 → DifferentiableAt ℝ (Real.qaryEntropy q) p
-- Mathlib.Data.Set.Basic
Set.instIsEmptyElemEmptyCollection : ∀ (α : Type u), IsEmpty ↑∅
-- Std.Data.TreeMap.AdditionalOperations
/-- Updates the values of the map by applying the given function to all mappings, keeping
only those mappings where the function returns `some` value.
 -/
Std.TreeMap.filterMap : {α : Type u} →
  {β : Type v} →
    {γ : Type w} → {cmp : α → α → Ordering} → (α → β → Option γ) → Std.TreeMap α β cmp → Std.TreeMap α γ cmp
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.distribBaseChange_tmul : ∀ (R : Type uR) (A : Type uA) {N : Type uN} {Q : Type uQ} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : AddCommMonoid Q]
  [inst_6 : Module R Q] (n : N) (q : Q) (a : A),
  (TensorProduct.AlgebraTensorModule.distribBaseChange R A N Q) (a ⊗ₜ[R] (n ⊗ₜ[R] q)) = a ⊗ₜ[R] n ⊗ₜ[A] (1 ⊗ₜ[R] q)
-- Mathlib.Topology.Algebra.Ring.Basic
instIsTopologicalSemiringAddOpposite : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] [inst_1 : TopologicalSpace R] [IsTopologicalSemiring R],
  IsTopologicalSemiring Rᵃᵒᵖ
-- Mathlib.Tactic.GRewrite.Elab
_private.Mathlib.Tactic.GRewrite.Elab.0.Mathlib.Tactic.GRewrite.instEvalExprConfig_mathlib : Lean.Elab.ConfigEval.EvalExpr Lean.Meta.Rewrite.Config
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.instCoeAffineMap : {R : Type u_1} →
  {V : Type u_2} →
    {W : Type u_3} →
      {P : Type u_4} →
        {Q : Type u_5} →
          [inst : Ring R] →
            [inst_1 : AddCommGroup V] →
              [inst_2 : Module R V] →
                [inst_3 : TopologicalSpace P] →
                  [inst_4 : AddTorsor V P] →
                    [inst_5 : AddCommGroup W] →
                      [inst_6 : Module R W] →
                        [inst_7 : TopologicalSpace Q] → [inst_8 : AddTorsor W Q] → Coe (P →ᴬ[R] Q) (P →ᵃ[R] Q)
-- Mathlib.Logic.Nonempty
not_nonempty_iff_imp_false : ∀ {α : Sort u_3}, ¬Nonempty α ↔ ∀ (a : α), False
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.opEquiv_functor : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C],
  (CategoryTheory.ShortComplex.opEquiv C).functor = CategoryTheory.ShortComplex.opFunctor C
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveElabStep3.mk.sizeOf_spec : ∀ (finalize : Lean.Elab.TermElabM Unit), sizeOf { finalize := finalize } = 1
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivAtFilter_natCast : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (L : Filter (𝕜 × 𝕜)) [inst_3 : NatCast F] (n : ℕ), HasDerivAtFilter (↑n) 0 L
-- Mathlib.Topology.Algebra.FilterBasis
ModuleFilterBasis.mk.injEq : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : TopologicalSpace R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] (toAddGroupFilterBasis : AddGroupFilterBasis M)
  (smul' : ∀ {U : Set M}, U ∈ toAddGroupFilterBasis.sets → ∃ V ∈ nhds 0, ∃ W ∈ toAddGroupFilterBasis.sets, V • W ⊆ U)
  (smul_left' :
    ∀ (x₀ : R) {U : Set M},
      U ∈ toAddGroupFilterBasis.sets → ∃ V ∈ toAddGroupFilterBasis.sets, V ⊆ (fun x => x₀ • x) ⁻¹' U)
  (smul_right' : ∀ (m₀ : M) {U : Set M}, U ∈ toAddGroupFilterBasis.sets → ∀ᶠ (x : R) in nhds 0, x • m₀ ∈ U)
  (toAddGroupFilterBasis_1 : AddGroupFilterBasis M)
  (smul'_1 :
    ∀ {U : Set M}, U ∈ toAddGroupFilterBasis_1.sets → ∃ V ∈ nhds 0, ∃ W ∈ toAddGroupFilterBasis_1.sets, V • W ⊆ U)
  (smul_left'_1 :
    ∀ (x₀ : R) {U : Set M},
      U ∈ toAddGroupFilterBasis_1.sets → ∃ V ∈ toAddGroupFilterBasis_1.sets, V ⊆ (fun x => x₀ • x) ⁻¹' U)
  (smul_right'_1 : ∀ (m₀ : M) {U : Set M}, U ∈ toAddGroupFilterBasis_1.sets → ∀ᶠ (x : R) in nhds 0, x • m₀ ∈ U),
  ({ toAddGroupFilterBasis := toAddGroupFilterBasis, smul' := smul', smul_left' := smul_left',
        smul_right' := smul_right' } =
      { toAddGroupFilterBasis := toAddGroupFilterBasis_1, smul' := smul'_1, smul_left' := smul_left'_1,
        smul_right' := smul_right'_1 }) =
    (toAddGroupFilterBasis = toAddGroupFilterBasis_1)
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
/-- The complex consisting of all faces present in either of its arguments.  -/
AbstractSimplicialComplex.instMax : {ι : Type u_1} → Max (AbstractSimplicialComplex ι)
-- Mathlib.Combinatorics.SetFamily.Shatter
_private.Mathlib.Combinatorics.SetFamily.Shatter.0.Finset.aux : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {t : Finset α} {a : α},
  (∀ t ∈ 𝒜, a ∉ t) → 𝒜.Shatters t → a ∉ t
-- Mathlib.Order.Monotone.Defs
monotoneOn_id : ∀ {α : Type u} [inst : Preorder α] {s : Set α}, MonotoneOn id s
-- Std.Http.Data.Headers
Std.Http.Headers.mk.inj : ∀ {map map_1 : Std.Internal.IndexMultiMap Std.Http.Header.Name Std.Http.Header.Value},
  { map := map } = { map := map_1 } → map = map_1
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.comapFun.congr_simp : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {S : Type u} [inst_3 : CommRing S]
  {N : Type u} [inst_4 : AddCommGroup N] [inst_5 : Module S N] {σ : R →+* S} (f f_1 : M →ₛₗ[σ] N),
  f = f_1 →
    ∀ (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
      (V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top S))
      (hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier)
      (s s_1 : (x : ↥U) → AlgebraicGeometry.StructureSheaf.Localizations M ↑x),
      s = s_1 →
        ∀ (y : ↥V),
          AlgebraicGeometry.StructureSheaf.comapFun f U V hUV s y =
            AlgebraicGeometry.StructureSheaf.comapFun f_1 U V hUV s_1 y
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.image_coe : ∀ {G : Type u_1} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal], QuotientAddGroup.mk '' ↑N = 0
-- Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Polynomial.cardPowDegree_nonzero : ∀ {Fq : Type u_1} [inst : Field Fq] [inst_1 : Fintype Fq] (p : Polynomial Fq),
  p ≠ 0 → Polynomial.cardPowDegree p = ↑(Fintype.card Fq) ^ p.natDegree
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.symm_p : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.PathObject A)
  [inst_2 : CategoryTheory.Limits.HasBinaryProducts C],
  P.symm.p = CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.Limits.prod.braiding A A).hom
-- Mathlib.Topology.Algebra.Group.Basic
/-- The (topological-space) closure of an additive subgroup of an additive topological group is
itself an additive subgroup.  -/
AddSubgroup.topologicalClosure : {G : Type w} →
  [inst : TopologicalSpace G] → [inst_1 : AddGroup G] → [IsTopologicalAddGroup G] → AddSubgroup G → AddSubgroup G
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.forget_obj : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  (a : CategoryTheory.Bicategory.InducedBicategory C F), CategoryTheory.Bicategory.InducedBicategory.forget.obj a = F a
-- Mathlib.Geometry.Manifold.ContMDiffMFDeriv
/-- The canonical equivalence between the tangent bundle of a product and the product of
tangent bundles is smooth.  -/
contMDiff_equivTangentBundleProd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] [inst_11 : IsManifold I 1 M]
  [inst_12 : IsManifold I' 1 M'],
  ContMDiff (I.prod I').tangent (I.tangent.prod I'.tangent) n ⇑(equivTangentBundleProd I M I' M')
-- Mathlib.Topology.MetricSpace.Algebra
/-- Eta-expanded form of `TendstoLocallyUniformly.smul₀` -/
TendstoLocallyUniformly.fun_smul₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero α]
  [inst_3 : Zero β] [inst_4 : SMul α β] [IsBoundedSMul α β] {X : Type u_3} {ι : Type u_4} [inst_6 : TopologicalSpace X]
  {F : ι → X → α} {G : ι → X → β} {f : X → α} {g : X → β} {l : Filter ι},
  TendstoLocallyUniformly F f l →
    TendstoLocallyUniformly G g l →
      Continuous f → Continuous g → TendstoLocallyUniformly (fun i i_1 => F i i_1 • G i i_1) (fun i => f i • g i) l
-- Lean.Meta.DiscrTree.Basic
_private.Lean.Meta.DiscrTree.Basic.0.Lean.Meta.DiscrTree.keysAsPattern.next? : StateRefT' IO.RealWorld (List Lean.Meta.DiscrTree.Key) Lean.CoreM (Option Lean.Meta.DiscrTree.Key)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_filterMap_eq_size_iff : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp}
  [Std.TransCmp cmp] [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)},
  t.WF → ((Std.DTreeMap.Raw.filterMap f t).size = t.size ↔ ∀ (a : α) (h : a ∈ t), (f a (t.get a h)).isSome = true)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_insertManyIfNewUnit!_list : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} {l : List α} {k : α}
  {h' : Std.DTreeMap.Internal.Impl.contains k ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l) = true},
  Std.DTreeMap.Internal.Impl.Const.get (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l)) k h' = ()
-- Mathlib.Data.Finset.Pi
/-- **Alias** of the reverse direction of `Finset.pi_nonempty`. -/
Finset.pi_nonempty_of_forall_nonempty : ∀ {α : Type u_1} {β : α → Type u} {s : Finset α} {t : (a : α) → Finset (β a)} [inst : DecidableEq α],
  (∀ a ∈ s, (t a).Nonempty) → (s.pi t).Nonempty
-- Lean.Widget.InteractiveDiagnostic
_private.Lean.Widget.InteractiveDiagnostic.0.Lean.Widget.EmbedFmt.goal.sizeOf_spec : ∀ (ctx : Lean.Elab.ContextInfo) (lctx : Lean.LocalContext) (g : Lean.MVarId),
  sizeOf (Lean.Widget.EmbedFmt.goal✝ ctx lctx g) = 1 + sizeOf ctx + sizeOf lctx + sizeOf g
-- Mathlib.Data.Nat.Factorization.Defs
Nat.factorization_eq_zero_iff : ∀ (n p : ℕ), n.factorization p = 0 ↔ ¬Nat.Prime p ∨ ¬p ∣ n ∨ n = 0
-- Mathlib.Topology.MetricSpace.ProperSpace
instProperSpaceAdditive : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] [ProperSpace X], ProperSpace (Additive X)
-- Mathlib.Data.Int.Init
Int.toNat_pred_coe_of_pos : ∀ {i : ℤ}, 0 < i → ↑(i.toNat - 1) = i - 1
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.deriv_mul_log : ∀ {x : ℝ}, x ≠ 0 → deriv (fun x => x * Real.log x) x = Real.log x + 1
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comp_d : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {P Q : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)} (f : P ⟶ Q) (n : ι),
  CategoryTheory.CategoryStruct.comp (P.p.f n) (f.f.f n) = f.f.f n
-- Mathlib.Data.Holor
Holor.mul.eq_1 : ∀ {α : Type} {ds₁ ds₂ : List ℕ} [inst : Mul α] (x : Holor α ds₁) (y : Holor α ds₂) (t : HolorIndex (ds₁ ++ ds₂)),
  x.mul y t = x t.take * y t.drop