mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Group.End
RelIso.mul_def : ∀ {α : Type u_1} {r : α → α → Prop} (f g : r ≃r r), f * g = g.trans f
-- Init.Data.BitVec.Lemmas
BitVec.toNat_mul_of_not_umulOverflow : ∀ {w : ℕ} {x y : BitVec w}, ¬x.umulOverflow y = true → (x * y).toNat = x.toNat * y.toNat
-- Init.Data.Slice.Operations
Std.Slice.LawfulSliceSize.mk : ∀ {α β : Type u_1} {γ : Type u} [inst : Std.Slice.SliceSize γ] [inst_1 : Std.ToIterator (Std.Slice γ) Id α β]
  [inst_2 : Std.Iterator α Id β],
  (∀ (s : Std.Slice γ), Std.Slice.SliceSize.size s = (Std.ToIterator.iter s).length) → Std.Slice.LawfulSliceSize γ
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
Complex.regularizedGaussHGFun_symm : ∀ (a b c : ℂ), a.regularizedGaussHGFun b c = b.regularizedGaussHGFun a c
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.mk_neg : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : NegMemClass σ A]
  {𝒜 : ι → σ} (x : Submonoid A) (i : HomogeneousLocalization.NumDenSameDeg 𝒜 x),
  HomogeneousLocalization.mk (-i) = -HomogeneousLocalization.mk i
-- Lean.Meta.Sym.Canon
/-- Canonicalize `e : type` where `e` is an instance by trying to resynthesize `type`.
If `report` is `true`, we report an issue when the instance cannot be resynthesized.
 -/
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.canon.canonInstCore : Lean.Expr → Lean.Expr → optParam Bool true → Lean.Meta.Sym.Canon.CanonM✝ Lean.Expr
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_diff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t₁.WF → t₂.WF → ∀ {k : α}, (t₁ \ t₂).get! k = if k ∈ t₂ then default else t₁.get! k
-- Mathlib.Algebra.Order.Hom.Basic
le_map_div_mul_map_div : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : Group α] [inst_2 : Mul β]
  [inst_3 : LE β] [SubmultiplicativeHomClass F α β] (f : F) (a b c : α), f (a / c) ≤ f (a / b) * f (b / c)
-- Plausible.Arbitrary
Plausible.UInt16.Arbitrary : Plausible.Arbitrary UInt16
-- Mathlib.MeasureTheory.Function.LpOrder
MeasureTheory.Lp.instOrderClosedTopologySubtypeAEEqFunMemAddSubgroupOfClosedIciTopology : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal}
  [inst : NormedAddCommGroup E] [inst_1 : PartialOrder E] [IsOrderedAddMonoid E] [inst_3 : Fact (1 ≤ p)]
  [ClosedIciTopology E], OrderClosedTopology ↥(MeasureTheory.Lp E p μ)
-- Mathlib.Order.Filter.Prod
Filter.prod_map_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β → γ) (F : Filter α) (G : Filter β),
  F ×ˢ Filter.map f G = Filter.map (Prod.map id f) (F ×ˢ G)
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
frestrictLe_iterateInduction : ∀ {X : ℕ → Type u_1} {a : ℕ} (x : (i : ↥(Finset.Iic a)) → X ↑i)
  (ind : (n : ℕ) → ((i : ↥(Finset.Iic n)) → X ↑i) → X (n + 1)), Preorder.frestrictLe a (iterateInduction x ind) = x
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.toOrderHom_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  (f : α →𝒄 β), f.toOrderHom = ↑f
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.degree_derivative_lt : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p ≠ 0 → (Polynomial.derivative p).degree < p.degree
-- Mathlib.RingTheory.PowerSeries.NoZeroDivisors
PowerSeries.instNoZeroDivisors : ∀ {R : Type u_1} [inst : Semiring R] [NoZeroDivisors R], NoZeroDivisors (PowerSeries R)
-- Mathlib.CategoryTheory.Preadditive.EilenbergMoore
CategoryTheory.Monad.algebraPreadditive_homGroup_zsmul_f : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (T : CategoryTheory.Monad C) [inst_2 : T.Additive] (F G : T.Algebra) (r : ℤ) (α : F ⟶ G), (r • α).f = r • α.f
-- Lean.Parser.Extra
/-- The parser `num` parses a numeric literal in several bases:

* Decimal: `129`
* Hexadecimal: `0xdeadbeef`
* Octal: `0o755`
* Binary: `0b1101`

This parser has arity 1: it produces a `numLitKind` node containing an atom with the text of the
literal.
You can use `TSyntax.getNat` to extract the number from the resulting syntax object.  -/
Lean.Parser.numLit : Lean.Parser.Parser
-- Lean.Meta.Tactic.Cases
Lean.Meta.ByCasesSubgoal.mk.sizeOf_spec : ∀ (mvarId : Lean.MVarId) (fvarId : Lean.FVarId),
  sizeOf { mvarId := mvarId, fvarId := fvarId } = 1 + sizeOf mvarId + sizeOf fvarId
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
/-- If an additive group `G` acts on `α` by measurable maps, then each element `c : G`
defines a measurable automorphism of `α`.  -/
MeasurableEquiv.vadd : {G : Type u_1} →
  {α : Type u_3} →
    [inst : MeasurableSpace α] →
      [inst_1 : AddGroup G] → [inst_2 : AddAction G α] → [MeasurableConstVAdd G α] → G → α ≃ᵐ α
-- Mathlib.Combinatorics.Graph.Delete
Graph.edgeSet_deleteEdges : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β), (G.deleteEdges F).edgeSet = G.edgeSet \ F
-- Mathlib.RingTheory.FractionalIdeal.Extended
/-- Pointwise compatibility of extension of fractional ideals with composition of ring
homomorphisms. See `FractionalIdeal.extendedHom'_comp` for the corresponding statement as an
equality of homomorphisms.  -/
FractionalIdeal.extended_extended : ∀ {A : Type u_1} [inst : CommRing A] {B : Type u_2} [inst_1 : CommRing B] {f : A →+* B} {K : Type u_3} {M : Submonoid A}
  [inst_2 : CommRing K] [inst_3 : Algebra A K] [inst_4 : IsLocalization M K] (L : Type u_4) {N : Submonoid B}
  [inst_5 : CommRing L] [inst_6 : Algebra B L] [inst_7 : IsLocalization N L] (hf : M ≤ Submonoid.comap f N)
  (I : FractionalIdeal M K) {C : Type u_5} {W : Type u_6} [inst_8 : CommRing C] [inst_9 : CommRing W]
  [inst_10 : Algebra C W] {P : Submonoid C} [inst_11 : IsLocalization P W] {g : B →+* C} (hg : N ≤ Submonoid.comap g P),
  FractionalIdeal.extended W hg (FractionalIdeal.extended L hf I) = FractionalIdeal.extended W ⋯ I
-- Lean.Parser.Term.Basic
Lean.Parser.Term.bracketedBinder.formatter : optParam Bool false → Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.Normed.Module.MStructure
IsLprojection.Subtype.zero : {X : Type u_1} →
  [inst : NormedAddCommGroup X] →
    {M : Type u_2} → [inst_1 : Ring M] → [inst_2 : Module M X] → Zero { P // IsLprojection X P }
-- Mathlib.Topology.Connected.PathConnected
/-- The setoid corresponding the equivalence relation of being joined by a continuous path.  -/
pathSetoid : (X : Type u_1) → [TopologicalSpace X] → Setoid X
-- Batteries.Data.AssocList
Batteries.AssocList.toList_mapKey : ∀ {α : Type u_1} {δ : Type u_2} {β : Type u_3} (f : α → δ) (l : Batteries.AssocList α β),
  (Batteries.AssocList.mapKey f l).toList =
    List.map
      (fun x =>
        match x with
        | (a, b) => (f a, b))
      l.toList
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel_i : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : CategoryTheory.Limits.HasCokernel S.f] (hg : S.g = 0),
  (CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel S hg).i = CategoryTheory.CategoryStruct.id S.X₂
-- Batteries.Tactic.GeneralizeProofs
/-- When `abstract` is `true`, then the tactic will create universally quantified proofs
to account for bound variables.
When it is `false` then such proofs are left alone.  -/
Batteries.Tactic.GeneralizeProofs.Config.abstract : Batteries.Tactic.GeneralizeProofs.Config → Bool
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.rightExactFunctor_le_additiveFunctor : ∀ (C : Type u₁) (D : Type u₂) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D]
  [CategoryTheory.Limits.HasBinaryBiproducts C],
  CategoryTheory.rightExactFunctor C D ≤ CategoryTheory.additiveFunctor C D
-- Mathlib.Algebra.Module.Torsion.Basic
/-- If the `q i` are pairwise coprime, a `∏ i, q i`-torsion module is the internal direct sum of
its `q i`-torsion submodules.  -/
Submodule.torsionBy_isInternal : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_3}
  [inst_3 : DecidableEq ι] {S : Finset ι} {q : ι → R},
  (↑S).Pairwise (Function.onFun IsCoprime q) →
    Module.IsTorsionBy R M (∏ i ∈ S, q i) → DirectSum.IsInternal fun i => Submodule.torsionBy R M (q ↑i)
-- Init.Data.UInt.Bitwise
UInt16.toUSize_and : ∀ (a b : UInt16), (a &&& b).toUSize = a.toUSize &&& b.toUSize
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isEmpty_insertMany_list : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {l : List ((a : α) × β a)}, (↑↑(m.insertMany l)).isEmpty = ((↑m).isEmpty && l.isEmpty)
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- The normal closure of a set `s` is the subgroup closure of all the conjugates of
elements of `s`. It is the smallest normal subgroup containing `s`.  -/
Subgroup.normalClosure : {G : Type u_1} → [inst : Group G] → Set G → Subgroup G
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
_private.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.0.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze.maybeAddBlockImplicit : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.Λ'.write.sizeOf_spec : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : SizeOf Γ] [inst_1 : SizeOf Λ] [inst_2 : SizeOf σ] (a : Γ)
  (a_1 : Turing.TM1.Stmt Γ Λ σ), sizeOf (Turing.TM1to1.Λ'.write a a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.extensionProduct_isoClosure_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P Q : CategoryTheory.ObjectProperty C), P.extensionProduct Q.isoClosure = P.extensionProduct Q
-- Lean.Meta.InferType
/-- Returns `true` iff `e : Sort _` or `e : (forall As, Sort _)`.
Remark: it subsumes `isType`
 -/
Lean.Meta.isTypeFormer : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.coeAddMonoidHom_eq_dfinsuppSum : ∀ {ι : Type v} [inst : DecidableEq ι] {M : Type u_1} {S : Type u_2} [inst_1 : DecidableEq M] [inst_2 : AddCommMonoid M]
  [inst_3 : SetLike S M] [inst_4 : AddSubmonoidClass S M] (A : ι → S) (x : DirectSum ι fun i => ↥(A i)),
  (DirectSum.coeAddMonoidHom A) x = DFinsupp.sum x fun i x => ↑x
-- Mathlib.Algebra.Category.Ring.Basic
/-- The object in the category of rings associated to a type equipped with the appropriate
typeclasses.  -/
RingCat.of : (carrier : Type u) → [ring : Ring carrier] → RingCat
-- Mathlib.Data.List.Sigma
List.keys_kreplace : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (b : β a) (l : List (Sigma β)),
  (List.kreplace a b l).keys = l.keys
-- Lean.Meta.HaveTelescope
Lean.Meta.HaveInfo.mk.inj : ∀ {typeBackDeps valueBackDeps : Std.HashSet ℕ} {decl : Lean.LocalDecl} {level : Lean.Level}
  {typeBackDeps_1 valueBackDeps_1 : Std.HashSet ℕ} {decl_1 : Lean.LocalDecl} {level_1 : Lean.Level},
  { typeBackDeps := typeBackDeps, valueBackDeps := valueBackDeps, decl := decl, level := level } =
      { typeBackDeps := typeBackDeps_1, valueBackDeps := valueBackDeps_1, decl := decl_1, level := level_1 } →
    typeBackDeps = typeBackDeps_1 ∧ valueBackDeps = valueBackDeps_1 ∧ decl = decl_1 ∧ level = level_1
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_erase_le : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, (m.erase k).size ≤ m.size
-- Mathlib.ModelTheory.Definability
FirstOrder.Language.DefinableSet.coe_sup : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {A : Set M} {α : Type u₁} (s t : L.DefinableSet A α),
  ↑(s ⊔ t) = ↑s ∪ ↑t
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_add_compl : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) {A : Set α},
  MeasurableSet A → ∫⁻ (x : α) in A, f x ∂μ + ∫⁻ (x : α) in Aᶜ, f x ∂μ = ∫⁻ (x : α), f x ∂μ
-- Mathlib.Tactic.Linarith.NNRealPreprocessor
/-- `getNNRealComparisons e` returns a list of all subexpressions of `e` of the form `(x : ℝ)`.
 -/
Mathlib.Tactic.Linarith.getNNRealCoes : Lean.Expr → List Lean.Expr
-- Mathlib.Algebra.MvPolynomial.Degrees
/-- The maximal degrees of each variable in a multi-variable polynomial, expressed as a multiset.

(For example, `degrees (x^2 * y + y^3)` would be `{x, x, y, y, y}`.)
 -/
MvPolynomial.degrees : {R : Type u} → {σ : Type u_1} → [inst : CommSemiring R] → MvPolynomial σ R → Multiset σ
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
Matrix.separatingRight_transpose_iff : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : CommSemiring R] {M : Matrix m n R} [inst_1 : Finite m]
  [inst_2 : Finite n], M.transpose.SeparatingRight ↔ M.SeparatingLeft
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFiniteAt.baseChange : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S)
  [inst_3 : p.IsPrime] [Algebra.QuasiFiniteAt R p] {A : Type u_4} [inst_5 : CommRing A] [inst_6 : Algebra R A]
  (q : Ideal (TensorProduct R A S)) [inst_7 : q.IsPrime],
  p = Ideal.comap Algebra.TensorProduct.includeRight.toRingHom q → Algebra.QuasiFiniteAt A q
-- Mathlib.Analysis.Meromorphic.Basic
Meromorphic.pow : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f : 𝕜 → 𝕜'} {n : ℕ}, Meromorphic f → Meromorphic (f ^ n)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
_private.Mathlib.Algebra.SkewMonoidAlgebra.Basic.0.SkewMonoidAlgebra.smul.match_1.eq_1 : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] {S : Type u_4} (motive : S → SkewMonoidAlgebra k G → Sort u_3)
  (s : S) (b : G →₀ k) (h_1 : (s : S) → (b : G →₀ k) → motive s { coeff := b }),
  (match s, { coeff := b } with
    | s, { coeff := b } => h_1 s b) =
    h_1 s b
-- Mathlib.RingTheory.UniqueFactorizationDomain.Defs
UniqueFactorizationMonoid.irreducible_iff_prime : ∀ {α : Type u_2} {inst : CommMonoidWithZero α} [self : UniqueFactorizationMonoid α] {a : α}, Irreducible a ↔ Prime a
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasurableEmbedding.integrable_map_iff : ∀ {α : Type u_1} {δ : Type u_4} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : MeasurableSpace δ] [inst_1 : TopologicalSpace ε] [inst_2 : ContinuousENorm ε] {f : α → δ},
  MeasurableEmbedding f →
    ∀ {g : δ → ε}, MeasureTheory.Integrable g (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.Integrable (g ∘ f) μ
-- Mathlib.RingTheory.Ideal.Over
Ideal.mem_of_liesOver : ∀ {A : Type u_2} [inst : CommSemiring A] {B : Type u_3} [inst_1 : Semiring B] [inst_2 : Algebra A B] (P : Ideal B)
  (p : Ideal A) [P.LiesOver p] (x : A), x ∈ p ↔ (algebraMap A B) x ∈ P
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.nnratCast_def : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → DivisionSemiring (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)]
  (q : ℚ≥0) (i : ι), ↑q = ⟦⟨i, ↑q⟩⟧
-- Init.Data.SInt.Lemmas
ISize.toNat_toBitVec_of_le : ∀ {x : ISize}, 0 ≤ x → x.toBitVec.toNat = x.toNatClampNeg
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.shiftRight.sizeOf_spec : ∀ {m n : ℕ} (lhs : Std.Tactic.BVDecide.BVExpr m) (rhs : Std.Tactic.BVDecide.BVExpr n),
  sizeOf (lhs.shiftRight rhs) = 1 + sizeOf m + sizeOf n + sizeOf lhs + sizeOf rhs
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.Struct.zero : Lean.Meta.Grind.Arith.Linear.Struct → Lean.Expr
-- Init.GrindInstances.ToInt
Lean.Grind.instLTISizeSintNumBits : Lean.Grind.ToInt.LT ISize (Lean.Grind.IntInterval.sint System.Platform.numBits)
-- Init.Data.Subtype.Order
Subtype.instMax : {α : Type u} → [inst : Max α] → [Std.MaxEqOr α] → {P : α → Prop} → Max (Subtype P)
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
/-- Construct on a completely metrizable space a metric (compatible with the topology)
which is complete.  -/
TopologicalSpace.completelyMetrizableMetric : (X : Type u_3) → [inst : TopologicalSpace X] → [h : TopologicalSpace.IsCompletelyMetrizableSpace X] → MetricSpace X
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.all_eq_false_iff_exists_mem_getElem : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α] {p : α → Bool},
  m.WF → (m.all p = false ↔ ∃ a ∈ m, p a = false)
-- Mathlib.Analysis.RCLike.Basic
RCLike.instContinuousStar : ∀ {K : Type u_1} [inst : RCLike K], ContinuousStar K
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.homEquiv_symm_naturality : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F} (h : CategoryTheory.Limits.IsColimit t)
  {W W' : C} (f : F ⟶ (CategoryTheory.Functor.const J).obj W) (g : W ⟶ W'),
  h.homEquiv.symm (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.Functor.const J).map g)) =
    CategoryTheory.CategoryStruct.comp (h.homEquiv.symm f) g
-- Init.Data.BitVec.Lemmas
BitVec.clzAuxRec_le : ∀ {w : ℕ} {x : BitVec w} (n : ℕ), x.clzAuxRec n ≤ ↑w
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- The right extension along the identity.  -/
CategoryTheory.Bicategory.RightExtension.alongId : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a c : B} → (g : a ⟶ c) → CategoryTheory.Bicategory.RightExtension (CategoryTheory.CategoryStruct.id a) g
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.Hom.hom_r : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} {c c' : C}
  {S₁ S₂ : CategoryTheory.Span Wₗ Wᵣ c c'} (self : S₁.Hom S₂), CategoryTheory.CategoryStruct.comp self.hom S₂.r = S₁.r
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.Hom.ext : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} {a b : F.Grothendieck}
  (f g : a ⟶ b) (hfg₁ : f.base = g.base),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f.fiber = g.fiber → f = g
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.containsₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (l : Std.DTreeMap.Internal.Impl α β) (k : α),
  l.containsₘ k = Std.DTreeMap.Internal.Impl.applyCell k l fun c x => c.contains
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.isAcyclic_iff_forall_isBridge : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsAcyclic ↔ ∀ ⦃e : Sym2 V⦄, e ∈ G.edgeSet → G.IsBridge e
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.memLp_iff : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  {p : ENNReal} {f : MeasureTheory.SimpleFunc α E},
  p ≠ 0 → p ≠ ⊤ → (MeasureTheory.MemLp (⇑f) p μ ↔ ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤)
-- Mathlib.Analysis.SpecificLimits.Basic
NNReal.summable_geometric : ∀ {r : NNReal}, r < 1 → Summable fun n => r ^ n
-- Mathlib.Geometry.Euclidean.Altitude
Affine.Simplex.neg_one_lt_inner_vsub_altitudeFoot_div : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : n.AtLeastTwo] (s : Affine.Simplex ℝ P n) (i j : Fin (n + 1)),
  -1 < inner ℝ (s.points i -ᵥ s.altitudeFoot i) (s.points j -ᵥ s.altitudeFoot j) / (s.height i * s.height j)
-- Mathlib.Topology.Sheaves.Flasque
/-- A sheaf is flasque if it is flasque as a presheaf  -/
TopCat.Sheaf.IsFlasque : {X : TopCat} → {C : Type v} → [inst : CategoryTheory.Category.{w, v} C] → TopCat.Sheaf C X → Prop
-- Mathlib.Logic.IsEmpty.Defs
instIsEmptySum : ∀ {α : Type u_1} {β : Type u_2} [IsEmpty α] [IsEmpty β], IsEmpty (α ⊕ β)
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.val_inv : ∀ {R : Type u_1} [inst : Field R] [inst_1 : StarRing R] (x : ↥(selfAdjoint R)), ↑x⁻¹ = (↑x)⁻¹
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.DiagramOfCocones.coconePoints_map : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} (D : CategoryTheory.Limits.DiagramOfCocones F) {X Y : J}
  (f : X ⟶ Y), D.coconePoints.map f = (D.map f).hom
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
/-- **Alias** of `CategoryTheory.NatTrans.Equifibered.of_isIso`. -/
CategoryTheory.NatTrans.equifibered_of_isIso : ∀ {J : Type u_1} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C] {F G : CategoryTheory.Functor J C} (α : F ⟶ G)
  [CategoryTheory.IsIso α], CategoryTheory.NatTrans.Equifibered α
-- Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
CategoryTheory.ObjectProperty.nonempty_top : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [Nonempty C], ⊤.Nonempty
-- Init.Data.List.Basic
List.unzipTR.eq_1 : ∀ {α : Type u} {β : Type v} (l : List (α × β)),
  l.unzipTR =
    List.foldr
      (fun x x_1 =>
        match x with
        | (a, b) =>
          match x_1 with
          | (as, bs) => (a :: as, b :: bs))
      ([], []) l
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.instHasRightHomologyOppositeOpOfHasLeftHomology : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} [S.HasLeftHomology], S.op.HasRightHomology
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of `Left.neg_lt_self`. -/
neg_lt_self : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : Preorder α] [AddLeftStrictMono α] {a : α}, 0 < a → -a < a
-- Mathlib.Analysis.Asymptotics.TVS
/-- **Alias** of the reverse direction of `Asymptotics.isLittleOTVS_iff_tendsto_div`. -/
Asymptotics.IsLittleOTVS.of_tendsto_div : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {f : α → E} {g : α → F} {l : Filter α},
  (∀ U ∈ nhds 0, ∃ V ∈ nhds 0, Filter.Tendsto (fun x => egauge 𝕜 U (f x) / egauge 𝕜 V (g x)) l (nhds 0)) → f =o[𝕜; l] g
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.proj_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (S : D) (T : CategoryTheory.Functor C D) {Y X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) T}
  (f : Y ⟶ X), (CategoryTheory.StructuredArrow.proj S T).map f = f.right
-- Mathlib.Analysis.Normed.Module.TransferInstance
/-- Transfer a `NormedCommGroup` across an `Equiv`  -/
Equiv.normedCommGroup : {α : Type u_1} → {β : Type u_2} → [NormedCommGroup β] → α ≃ β → NormedCommGroup α
-- Mathlib.Data.PFunctor.Univariate.M
/-- The label of the root of the tree for a non-trivial
approximation of the cofix of a pfunctor.
 -/
PFunctor.Approx.head' : {F : PFunctor.{uA, uB}} → {n : ℕ} → PFunctor.Approx.CofixA F n.succ → F.A