mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Finiteness
Monoid.FG.fg_top : ∀ {M : Type u_1} {inst : Monoid M} [self : Monoid.FG M], ⊤.FG
-- Mathlib.RingTheory.Valuation.Extension
Valuation.HasExtension.maximalIdeal_comap_algebraMap_eq_maximalIdeal : ∀ {K : outParam (Type u_5)} {L : outParam (Type u_6)} {Γ₀ : outParam (Type u_7)} {Γ₁ : outParam (Type u_8)}
  [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [inst_3 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_4 : LinearOrderedCommGroupWithZero Γ₁] (vK : Valuation K Γ₀) (vL : Valuation L Γ₁)
  [inst_5 : vK.HasExtension vL],
  Ideal.comap (algebraMap ↥vK.valuationSubring ↥vL.valuationSubring) (IsLocalRing.maximalIdeal ↥vL.valuationSubring) =
    IsLocalRing.maximalIdeal ↥vK.valuationSubring
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.instZero : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {X : Type u_2} → [Zero X] → [inst_3 : MulAction R X] → Zero (OreLocalization S X)
-- Mathlib.Algebra.BigOperators.Fin
List.alternatingSum.eq_3 : ∀ {G : Type u_4} [inst : Zero G] [inst_1 : Add G] [inst_2 : Neg G] (g h : G) (t : List G),
  (g :: h :: t).alternatingSum = g + -h + t.alternatingSum
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.get!ₘ_eq_getValueCast! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : Std.LawfulEqOrd α] [inst_3 : BEq α]
  [inst_4 : Std.LawfulBEqOrd α] {k : α} [inst_5 : Inhabited (β k)] {t : Std.DTreeMap.Internal.Impl α β},
  t.Ordered → t.get!ₘ k = Std.Internal.List.getValueCast! k t.toListModel
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.StackEntry.star.sizeOf_spec : sizeOf Lean.Meta.RefinedDiscrTree.StackEntry.star = 1
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.inv_eq_inv_aux : ∀ {k : Type u_2} [inst : Field k] (φ : PowerSeries k), φ⁻¹ = PowerSeries.inv.aux (PowerSeries.constantCoeff φ)⁻¹ φ
-- Init.Data.BitVec.Lemmas
BitVec.toNat_concat : ∀ {w : ℕ} (x : BitVec w) (b : Bool), (x.concat b).toNat = x.toNat * 2 + b.toNat
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
derivWithin_cexp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra 𝕜 ℂ] {f : 𝕜 → ℂ} {x : 𝕜} {s : Set 𝕜},
  DifferentiableWithinAt 𝕜 f s x →
    UniqueDiffWithinAt 𝕜 s x → derivWithin (fun x => Complex.exp (f x)) s x = Complex.exp (f x) * derivWithin f s x
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.triangleCategory_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (A : CategoryTheory.Pretriangulated.Triangle C),
  CategoryTheory.CategoryStruct.id A = CategoryTheory.Pretriangulated.triangleMorphismId A
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_insertIfNew : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF →
    ∀ {k a : α} [inst_3 : Inhabited (β a)] {v : β k},
      (m.insertIfNew k v).get! a = if h : (k == a) = true ∧ k ∉ m then cast ⋯ v else m.get! a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.size_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap α (fun x => Unit) cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List α},
  List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
    (∀ a ∈ t, l.contains a = false) → (Std.DTreeMap.Const.insertManyIfNewUnit t l).size = t.size + l.length
-- Mathlib.AlgebraicGeometry.Geometrically.Integral
/-- If `X` is geometrically integral and flat and universally open over `S` and `Y` is integral
and locally noetherian, then `X ×ₛ Y` is integral.  -/
AlgebraicGeometry.instIsIntegralPullbackSchemeOfGeometricallyIntegralOfFlatOfUniversallyOpenOfIsLocallyNoetherian : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.GeometricallyIntegral f]
  [AlgebraicGeometry.Flat f] [AlgebraicGeometry.UniversallyOpen f] [AlgebraicGeometry.IsIntegral Y]
  [AlgebraicGeometry.IsLocallyNoetherian Y], AlgebraicGeometry.IsIntegral (CategoryTheory.Limits.pullback f g)
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.beq : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] →
      [LawfulBEq α] →
        [Hashable α] → [(k : α) → BEq (β k)] → Std.DHashMap.Internal.Raw₀ α β → Std.DHashMap.Internal.Raw₀ α β → Bool
-- Init.Data.Array.Bootstrap
Array.append_assoc : ∀ {α : Type u_1} {xs ys zs : Array α}, xs ++ ys ++ zs = xs ++ (ys ++ zs)
-- Mathlib.Topology.Algebra.ProperAction.Basic
AddAction.properVAdd_of_proper_orbitMap : ∀ {G : Type u_1} {X : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G X] [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace X] [ContinuousVAdd G X] [IsTopologicalAddGroup G] [AddAction.IsPretransitive G X] {x : X},
  (IsProperMap fun g => g +ᵥ x) → ProperVAdd G X
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey?_unitOfList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  l.contains k = false → (Std.DTreeMap.Const.unitOfList l cmp).getKey? k = none
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.self_le_maxKey?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {kmi : α}, (t.insertIfNew k v).maxKey?.get ⋯ = kmi → (cmp k kmi).isLE = true
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Presieve.preZeroHypercover_I₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (R : CategoryTheory.Presieve S),
  R.preZeroHypercover.I₀ = ↑R.uncurry
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicCompletionV : ∀ {K : Type u_1} [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  Valued.v.IsRankOneDiscrete
-- Mathlib.CategoryTheory.Limits.Cones
/-- Extending a cone by the identity does nothing.  -/
CategoryTheory.Limits.Cone.extendId : {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.extend (CategoryTheory.CategoryStruct.id s.pt) ≅ s
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.vanishingIdeal_singleton : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] (x : ProjectiveSpectrum 𝒜), ProjectiveSpectrum.vanishingIdeal {x} = x.asHomogeneousIdeal
-- Mathlib.GroupTheory.OrderOfElement
zsmul_eq_zero_iff_modEq : ∀ {G : Type u_1} [inst : AddGroup G] {x : G} {n : ℤ}, n • x = 0 ↔ n ≡ 0 [ZMOD ↑(addOrderOf x)]
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.of_injective_iff : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Function.Injective ⇑(AdicCompletion.of I M) ↔ IsHausdorff I M
-- Mathlib.Algebra.Lie.TransferInstance
AddEquiv.bracket_def : ∀ {M : Type u_2} {L : Type u_3} [inst : AddCommGroup M] [inst_1 : LieRing L] (e : M ≃+ L) (x y : M),
  ⁅x, y⁆ = e.symm ⁅e x, e y⁆
-- Init.Data.Nat.Gcd
Nat.eq_zero_of_gcd_eq_zero_left : ∀ {m n : ℕ}, m.gcd n = 0 → m = 0
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_castAdd_Ici : ∀ {n : ℕ} (m : ℕ) [inst : NeZero m] (i : Fin n),
  Finset.image (Fin.castAdd m) (Finset.Ici i) = Finset.Ico (Fin.castAdd m i) (Fin.natAdd n 0)
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.State.isExported : Lean.ParseImports.State → Bool
-- Aesop.Script.Step
/-- A nonempty list of tactic builders. During script generation, Aesop tries to
execute the builders from left to right. It then uses the first builder that
succceds (in the sense that when run in `preState` on `preGoal` it produces
the `postState` and `postGoals`). The last builder must succeed and is used
unconditionally.
 -/
Aesop.Script.LazyStep.tacticBuilders : Aesop.Script.LazyStep → Array Aesop.Script.TacticBuilder
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- A simplicial set `X` satisfies the strict Segal condition if its simplices
are uniquely determined by their spine.  -/
SSet.StrictSegal : SSet → Type u
-- Mathlib.Data.FP.Basic
FP.Float.instNeg : [C : FP.FloatCfg] → Neg FP.Float
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  [inst : Inhabited β], (t₁ \ t₂)[k]! = if k ∈ t₂ then default else t₁[k]!
-- Mathlib.Algebra.Order.Monoid.ToMulBot
/-- Making an additive monoid multiplicative then adding a zero is the same as adding a bottom
element then making it multiplicative.  -/
WithZero.toMulBot : {α : Type u} → [inst : Add α] → WithZero (Multiplicative α) ≃* Multiplicative (WithBot α)
-- Init.System.ST
ST.Out.mk : {σ α : Type} → α → Void σ → ST.Out σ α
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.forgetAdjToOver.homEquiv_symm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X : C} (Z : CategoryTheory.Over X) (A : C) (f : Z ⟶ (CategoryTheory.toOver X).obj A),
  ((CategoryTheory.forgetAdjToOver X).homEquiv Z A).symm f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left f)
      (CategoryTheory.SemiCartesianMonoidalCategory.fst A X)
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.continuous_negMulLog : Continuous Real.negMulLog
-- Lean.MetavarContext
Lean.instInhabitedLocalInstance.default : Lean.LocalInstance
-- Lean.Server.FileSource
Lean.Lsp.instFileSourceDocumentSymbolParams : Lean.Lsp.FileSource Lean.Lsp.DocumentSymbolParams
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min!_eq_iff_get?_eq_self_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {km : α}, t.min! = km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Sigma.uncurry.eq_1 : ∀ {α : Type u_1} {β : α → Type u_4} {γ : (a : α) → β a → Type u_7} (f : (x : α) → (y : β x) → γ x y) (x : Sigma β),
  Sigma.uncurry f x = f x.fst x.snd
-- Mathlib.Algebra.Order.Hom.Basic
/-- the image of any element is nonnegative.  -/
NonnegHomClass.apply_nonneg : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} {inst : Zero β} {inst_1 : LE β}
  {inst_2 : FunLike F α β} [self : NonnegHomClass F α β] (f : F) (a : α), 0 ≤ f a
-- Mathlib.Order.Hom.Basic
OrderHom.instDecidableEqOfForall : {α : Type u_6} →
  (β : Type u_7) → [inst : PartialOrder α] → [inst_1 : PartialOrder β] → [DecidableEq (α → β)] → DecidableEq (α →o β)
-- Lean.Elab.PreDefinition.PartialFixpoint.Induction
/-- Unfolds an appropriate `PartialOrder` instance on predicates to quantifications and implications.
I.e. `ImplicationOrder.instPartialOrder.rel P Q` becomes
`∀ x y, P x y → Q x y`.
In the premise of the Park induction principle (`lfp_le_of_le_monotone`) we use a monotone map defining the predicate in the eta expanded form. In such a case, besides desugaring the predicate, we need to perform a weak head reduction.
The optional parameter `reducePremise` (false by default) indicates whether we need to perform this reduction.
 -/
_private.Lean.Elab.PreDefinition.PartialFixpoint.Induction.0.Lean.Elab.PartialFixpoint.unfoldPredRel : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Elab.PartialFixpointType → optParam Bool false → Lean.MetaM Lean.Expr
-- Mathlib.MeasureTheory.Group.FoelnerFilter
/-- The constant sequence `X` is Følner if `X` has finite measure.  -/
IsAddFoelner.univ_of_isFiniteMeasure : ∀ {G : Type u_1} {X : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : AddGroup G]
  [inst_2 : AddAction G X] {ι : Type u_3} {l : Filter ι} [NeZero μ] [MeasureTheory.IsFiniteMeasure μ],
  IsAddFoelner G μ l fun x => Set.univ
-- Mathlib.Data.Finset.Basic
Finset.disjoint_or_nonempty_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), Disjoint s t ∨ (s ∩ t).Nonempty
-- Mathlib.CategoryTheory.Adjunction.Limits
/-- auxiliary construction for `coconesIso`  -/
CategoryTheory.Adjunction.coconesIsoComponentInv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (F ⊣ G) →
              {J : Type u} →
                [inst_2 : CategoryTheory.Category.{v, u} J] →
                  {K : CategoryTheory.Functor J C} →
                    (Y : D) →
                      (G.comp ((CategoryTheory.cocones J C).obj (Opposite.op K))).obj Y →
                        ((CategoryTheory.cocones J D).obj (Opposite.op (K.comp F))).obj Y
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.le_of_le_le : ∀ {d : ℕ} {x y z w : ℤ}, x ≤ z → y ≤ w → { re := x, im := y } ≤ { re := z, im := w }
-- Std.Time.Format.Modifier
Std.Time.Modifier.Y.injEq : ∀ (presentation presentation_1 : Std.Time.Year),
  (Std.Time.Modifier.Y presentation = Std.Time.Modifier.Y presentation_1) = (presentation = presentation_1)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD_empty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp]
  {a : α} {fallback : β a}, ∅.getD a fallback = fallback
-- Lean.Elab.Tactic.RCases
Lean.Elab.Tactic.RCases.RCasesPatt.one.injEq : ∀ (ref : Lean.Syntax) (a : Lean.Name) (ref_1 : Lean.Syntax) (a_1 : Lean.Name),
  (Lean.Elab.Tactic.RCases.RCasesPatt.one ref a = Lean.Elab.Tactic.RCases.RCasesPatt.one ref_1 a_1) =
    (ref = ref_1 ∧ a = a_1)
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.offset_of_isLongestRevMatchAt : ∀ {pat : String} {s : String.Slice} {pos₁ pos₂ : s.Pos},
  pat ≠ "" →
    String.Slice.Pattern.Model.IsLongestRevMatchAt pat pos₁ pos₂ → pos₂.offset = pos₁.offset.increaseBy pat.utf8ByteSize
-- Mathlib.Order.BoundedOrder.Basic
Pi.instTopForall : {ι : Type u_1} → {α' : ι → Type u_2} → [(i : ι) → Top (α' i)] → Top ((i : ι) → α' i)
-- Init.Control.StateCps
StateCpsT.run_eq : ∀ {α σ : Type u} {m : Type u → Type v} [inst : Monad m] (x : StateCpsT σ m α) (s : σ),
  x.run s = x.runK s fun a s => pure (a, s)
-- Mathlib.Analysis.Convex.Side
AffineSubspace.SOppSide.not_wSameSide : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P}, s.SOppSide x y → ¬s.WSameSide x y
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.IsHermitian.inv : ∀ {α : Type u_1} {m : Type u_3} [inst : CommRing α] [inst_1 : StarRing α] [inst_2 : Fintype m] [inst_3 : DecidableEq m]
  {A : Matrix m m α}, A.IsHermitian → A⁻¹.IsHermitian
-- Batteries.Data.Fin.Coding
Fin.decodeSubtype.eq_1 : ∀ (x : Fin 0 → Prop) (x_1 : DecidablePred x) (val : ℕ) (h : val < Fin.countP fun x_2 => decide (x x_2)),
  Fin.decodeSubtype x ⟨val, h⟩ = ⋯.elim
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.ofNat_fin_three : ∀ {α : Type u} [inst : AddMonoidWithOne α] (n : ℕ) [inst_1 : n.AtLeastTwo],
  OfNat.ofNat n = !![OfNat.ofNat n, 0, 0; 0, OfNat.ofNat n, 0; 0, 0, OfNat.ofNat n]
-- Mathlib.NumberTheory.LSeries.Basic
LSeries.norm_term_le_of_re_le_re : ∀ (f : ℕ → ℂ) {s s' : ℂ}, s.re ≤ s'.re → ∀ (n : ℕ), ‖LSeries.term f s' n‖ ≤ ‖LSeries.term f s n‖
-- Lean.Data.Lsp.Basic
Lean.Lsp.ChangeAnnotation.mk.sizeOf_spec : ∀ (label : String) (needsConfirmation : Bool) (description? : Option String),
  sizeOf { label := label, needsConfirmation := needsConfirmation, description? := description? } =
    1 + sizeOf label + sizeOf needsConfirmation + sizeOf description?
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- One line equals another differing in the second point if the second point of the first line is
contained in the second line and does not equal the first point.  -/
affineSpan_pair_eq_of_right_mem_of_ne : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p₁ p₂ p₃ : P}, p₁ ∈ line[k, p₂, p₃] → p₁ ≠ p₂ → line[k, p₂, p₁] = line[k, p₂, p₃]
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.prod_left_fst : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [inst : SeminormedAddCommGroup E']
  [inst_1 : SeminormedAddCommGroup F'] [inst_2 : SeminormedAddCommGroup G'] {f' : α → E'} {g' : α → F'} {k' : α → G'}
  {l : Filter α}, (fun x => (f' x, g' x)) =O[l] k' → f' =O[l] k'
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.cycleFactorsFinset_eq_empty_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {f : Equiv.Perm α}, f.cycleFactorsFinset = ∅ ↔ f = 1
-- Mathlib.Order.Partition.Finpartition
Finpartition.exists_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (P : Finpartition s) {a : α}, a ∈ s → ∃ t ∈ P.parts, a ∈ t
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
/-- tactic for proof by bisimulation  -/
Mathlib.Tactic.MvBisim.tacticMv_bisim___With___ : Lean.ParserDescr
-- Mathlib.Topology.MetricSpace.Contracting
/-- If a map `f` has a contracting iterate `f^[n]`, then the fixed point of `f^[n]` is also a fixed
point of `f`.  -/
ContractingWith.isFixedPt_fixedPoint_iterate : ∀ {α : Type u_1} [inst : MetricSpace α] {K : NNReal} {f : α → α} [inst_1 : Nonempty α] [inst_2 : CompleteSpace α]
  {n : ℕ} (hf : ContractingWith K f^[n]), Function.IsFixedPt f (ContractingWith.fixedPoint f^[n] hf)
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
_private.Mathlib.Analysis.SpecialFunctions.BinaryEntropy.0.Real.qaryEntropy.eq_1 : ∀ (q : ℕ) (p : ℝ), Real.qaryEntropy q p = p * Real.log ↑(↑q - 1) + Real.binEntropy p
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_apply : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (M : Matrix n n R),
  M.det = ∑ σ, Equiv.Perm.sign σ • ∏ i, M (σ i) i
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
IsAddIndecomposable.pairwise_baseOf_sub_notMem : ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : AddCommGroup G] [inst_1 : LinearOrder S]
  [inst_2 : InvolutiveNeg ι] [inst_3 : AddCommGroup S] [IsOrderedAddMonoid S] (v : ι → G),
  (∀ (i : ι), v (-i) = -v i) →
    ∀ (f : G →+ S),
      (∀ (i : ι), f (v i) ≠ 0) → (IsAddIndecomposable.baseOf v f).Pairwise fun i j => v i - v j ∉ Set.range v
-- Mathlib.Algebra.Category.MonCat.Basic
_private.Mathlib.Algebra.Category.MonCat.Basic.0.CommMonCat.Hom.mk : {A B : CommMonCat} → (↑A →* ↑B) → A.Hom B
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.presieve₀_singleton : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S T : C} (f : S ⟶ T),
  (CategoryTheory.PreZeroHypercover.singleton f).presieve₀ = CategoryTheory.Presieve.singleton f
-- Init.Data.Array.Lemmas
Array.getElem_filter : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool} {i : ℕ} (h : i < (Array.filter p xs).size),
  p (Array.filter p xs)[i] = true
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.coe_period : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜), ↑p = 0
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.blockTriangular_single : ∀ {α : Type u_1} {m : Type u_3} {R : Type v} {b : m → α} [inst : Preorder α] [inst_1 : Zero R] [inst_2 : DecidableEq m]
  {i j : m}, b i ≤ b j → ∀ (c : R), (Matrix.single i j c).BlockTriangular b
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
CategoryTheory.Functor.IsDense.iff_of_iso : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (e : F ≅ G), F.IsDense ↔ G.IsDense
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.toProp.eq_2 : ∀ (K : Type u_2) [inst : Add K] [inst_1 : Mul K] [inst_2 : Neg K] [inst_3 : Zero K] [inst_4 : One K],
  FirstOrder.Field.FieldAxiom.toProp K FirstOrder.Field.FieldAxiom.zeroAdd = ∀ (x : K), 0 + x = x
-- Mathlib.Topology.Algebra.UniformConvergence
instAddUniformOnFun : {α : Type u_1} → {β : Type u_2} → {𝔖 : Set (Set α)} → [Add β] → Add (UniformOnFun α β 𝔖)
-- Mathlib.Analysis.Calculus.ContDiff.Operations
iteratedFDeriv_sum : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {ι : Type u_3}
  {f : ι → E → F} {u : Finset ι} {i : ℕ},
  (∀ j ∈ u, ContDiff 𝕜 (↑i) (f j)) → (iteratedFDeriv 𝕜 i fun x => ∑ j ∈ u, f j x) = ∑ j ∈ u, iteratedFDeriv 𝕜 i (f j)
-- Mathlib.LinearAlgebra.Dual.Basis
Module.DualBases.mk : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {e : ι → M} {ε : ι → Module.Dual R M},
  (∀ (i : ι), (ε i) (e i) = 1) →
    (Pairwise fun i j => (ε i) (e j) = 0) →
      (∀ {m₁ m₂ : M}, (∀ (i : ι), (ε i) m₁ = (ε i) m₂) → m₁ = m₂) →
        autoParam (∀ (m : M), {i | (ε i) m ≠ 0}.Finite) Module.DualBases.finite._autoParam → Module.DualBases e ε
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrpObj.η_whiskerRight_addCommutator : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {G : C}
  [inst_2 : CategoryTheory.AddGrpObj G],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.zero G)
      (CategoryTheory.AddGrpObj.addCommutator G) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.SemiCartesianMonoidalCategory.toUnit
        (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) G))
      CategoryTheory.AddMonObj.zero
-- Mathlib.LinearAlgebra.Matrix.Circulant
Matrix.Fin.circulant_isSymm_apply : ∀ {α : Type u_1} {n : ℕ} {v : Fin n → α}, (Matrix.circulant v).IsSymm → ∀ (i : Fin n), v (-i) = v i
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.unop_f₃₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square Cᵒᵖ), sq.unop.f₃₄ = sq.f₁₃.unop
-- Std.Http.Protocol.H1
/-- Returns `true` when `pullBody` is currently expected to make progress.
 -/
Std.Http.Protocol.H1.Machine.canPullBodyNow : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Bool
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.instPathConnectedSpace : PathConnectedSpace Circle
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.comm : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp}, t₁.Equiv t₂ ↔ t₂.Equiv t₁
-- Mathlib.Topology.Maps.Basic
Topology.IsClosedEmbedding.isClosed_iff_preimage_isClosed : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsClosedEmbedding f → ∀ {s : Set Y}, s ⊆ Set.range f → (IsClosed s ↔ IsClosed (f ⁻¹' s))
-- Mathlib.Order.SuccPred.InitialSeg
PrincipalSeg.isSuccLimit_apply_iff : ∀ {α : Type u_1} {β : Type u_2} {a : α} [inst : PartialOrder α] [inst_1 : PartialOrder β] (f : α <i β),
  Order.IsSuccLimit (f.toRelEmbedding a) ↔ Order.IsSuccLimit a
-- Std.Data.DHashMap.Raw
/-- Transforms the hash map into a list of mappings in some order.  -/
Std.DHashMap.Raw.Const.toList : {α : Type u} → {β : Type v} → (Std.DHashMap.Raw α fun x => β) → List (α × β)
-- Init.Data.Array.Basic
/-- Computes the product of the elements of an array.

Examples:
* `#[a, b, c].prod = a * (b * (c * 1))`
* `#[1, 2, 5].prod = 10`
 -/
Array.prod : {α : Type u_1} → [Mul α] → [One α] → Array α → α
-- Std.Http.Data.Chunk
Std.Http.Chunk.ExtensionValue.instToString : ToString Std.Http.Chunk.ExtensionValue