mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Parser.Term
/-- The *anonymous constructor* `⟨e, ...⟩` is equivalent to `c e ...` if the
expected type is an inductive type with a single constructor `c`.
If more terms are given than `c` has parameters, the remaining arguments
are turned into a new anonymous constructor application. For example,
`⟨a, b, c⟩ : α × (β × γ)` is equivalent to `⟨a, ⟨b, c⟩⟩`.
 -/
Lean.Parser.Term.anonymousCtor : Lean.Parser.Parser
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- Given two formal multilinear series `q` and `p` and a composition `c` of `n`, one may
form a continuous multilinear map in `n` variables by applying the right coefficient of `p` to each
block of the composition, and then applying `q c.length` to the resulting vector. It is
called `q.compAlongComposition p c`.  -/
FormalMultilinearSeries.compAlongOrderedFinpartition : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_3} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                {G : Type u_4} →
                  [inst_5 : NormedAddCommGroup G] →
                    [inst_6 : NormedSpace 𝕜 G] →
                      {n : ℕ} →
                        FormalMultilinearSeries 𝕜 F G →
                          FormalMultilinearSeries 𝕜 E F → OrderedFinpartition n → E [×n]→L[𝕜] G
-- Mathlib.Topology.Order.SuccPred
SuccOrder.isSuccLimit_of_mem_frontier : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] [SuccOrder α] [NoMaxOrder α]
  {a : α} {s : Set α}, a ∈ frontier s → Order.IsSuccLimit a
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
/-- Isomorphisms are closed immersions.  -/
AlgebraicGeometry.IsClosedImmersion.instOfIsIsoScheme : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f], AlgebraicGeometry.IsClosedImmersion f
-- Mathlib.Topology.UniformSpace.Cauchy
Cauchy.mono_uniformSpace : ∀ {β : Type v} {u v : UniformSpace β} {F : Filter β}, u ≤ v → Cauchy F → Cauchy F
-- Lean.Parser.Basic
/-- `notFollowedBy(p, "foo")` succeeds iff `p` fails;
if `p` succeeds then it fails with the message `"unexpected foo"`.

This parser has arity 0 - it does not capture anything.  -/
Lean.Parser.notFollowedBy : Lean.Parser.Parser → String → Lean.Parser.Parser
-- Mathlib.Analysis.Normed.Group.Bounded
/-- A helper lemma used to prove that the (scalar or usual) product of a function that
tends to zero and a bounded function tends to zero. This lemma is formulated for any binary
operation `op : E → F → G` with an estimate `‖op x y‖ ≤ ‖x‖ * ‖y‖` instead of multiplication so
that it can be applied to `(*)`, `flip (*)`, `(•)`, and `flip (•)`.  -/
Filter.Tendsto.op_zero_isBoundedUnder_le : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : SeminormedAddGroup E]
  [inst_1 : SeminormedAddGroup F] [inst_2 : SeminormedAddGroup G] {f : α → E} {g : α → F} {l : Filter α},
  Filter.Tendsto f l (nhds 0) →
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ g) →
      ∀ (op : E → F → G),
        (∀ (x : E) (y : F), ‖op x y‖ ≤ ‖x‖ * ‖y‖) → Filter.Tendsto (fun x => op (f x) (g x)) l (nhds 0)
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPExplicit : Lean.Options → Bool
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.wordProd_concat : ∀ {B : Type u_1} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) (ω : List B),
  cs.wordProd (ω.concat i) = cs.wordProd ω * cs.simple i
-- Mathlib.Order.OrdContinuous
LeftOrdContinuous.le_iff : ∀ {α : Type u} {β : Type v} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] {f : α → β},
  LeftOrdContinuous f → Function.Injective f → ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₃₂.ι₀_desc_assoc : ∀ {X : SSet} (f₀ f₁ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X)
  (h₀₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₁ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₃)
  (h₁₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃)
  (h₂₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₁)
  {Z : SSet} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp SSet.horn₃₂.ι₀
      (CategoryTheory.CategoryStruct.comp (SSet.horn₃₂.desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃) h) =
    CategoryTheory.CategoryStruct.comp f₀ h
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.stabilizer_add_eq_left : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : AddGroup α]
  [VAddAssocClass G α α] (a b : α), AddAction.stabilizer G (a + b) = AddAction.stabilizer G a
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.surj : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (x : R)
  [IsLocalization.Away x S] (z : S), ∃ n a, z * (algebraMap R S) x ^ n = (algebraMap R S) a
-- Mathlib.Data.Fin.Rev
/-- `rev` commutes with `succAbove`.  -/
Fin.rev_succAbove : ∀ {n : ℕ} (p : Fin (n + 1)) (i : Fin n), (p.succAbove i).rev = p.rev.succAbove i.rev
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.centerToMulOpposite_apply_coe : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (r : ↥(Subsemigroup.center R)),
  ↑(NonUnitalSubring.centerToMulOpposite r) = MulOpposite.op ↑r
-- Mathlib.Algebra.Group.Defs
inv_eq_of_mul_eq_one_left : ∀ {G : Type u_1} [inst : DivisionMonoid G] {a b : G}, a * b = 1 → b⁻¹ = a
-- Mathlib.Topology.Sets.Compacts
/-- `TopologicalSpace.NonemptyCompacts.toCompacts` as an order embedding.  -/
TopologicalSpace.NonemptyCompacts.toCompactsOrderEmbedding : {α : Type u_1} → [inst : TopologicalSpace α] → TopologicalSpace.NonemptyCompacts α ↪o TopologicalSpace.Compacts α
-- Aesop.Forward.Match.Types
Aesop.instInhabitedMatch.default : Aesop.Match
-- Mathlib.CategoryTheory.ObjectProperty.Extensions
CategoryTheory.ObjectProperty.prop_X₂_of_shortExact : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [P.IsClosedUnderExtensions] {S : CategoryTheory.ShortComplex C},
  S.ShortExact → P S.X₁ → P S.X₃ → P S.X₂
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey!_of_perm : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l l' : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l → l.Perm l' → Std.Internal.List.maxKey! l = Std.Internal.List.maxKey! l'
-- Init.Data.Int.Linear
Int.Internal.Linear.instBEqExpr.beq : Int.Internal.Linear.Expr → Int.Internal.Linear.Expr → Bool
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Submodule.eq_top_of_disjoint : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [FiniteDimensional K V] (s t : Submodule K V),
  Module.finrank K V ≤ Module.finrank K ↥s + Module.finrank K ↥t → Disjoint s t → s ⊔ t = ⊤
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k : α} {fallback : β k},
      (List.map Sigma.fst l).contains k = false → (t.insertMany l).getD k fallback = t.getD k fallback
-- Mathlib.Topology.Algebra.Module.Equiv
/-- Continuous linear equivalence between vectors in `M² = Fin 2 → M` and `M × M`.  -/
ContinuousLinearEquiv.finTwoArrow : (R : Type u_2) →
  (M : Type u_3) →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → [inst_3 : TopologicalSpace M] → (Fin 2 → M) ≃L[R] M × M
-- Init.Data.List.Attach
_private.Init.Data.List.Attach.0.List.findSome?.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match none with
    | some b => h_1 b
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.CategoryTheory.Adjunction.Parametrized
CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_three_assoc : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ : C₁} {X₂ : C₂} {X₃ Y₃ : C₃}
  (f₃ : X₃ ⟶ Y₃) (g : (F.obj X₁).obj X₂ ⟶ X₃) {Z : C₂} (h : (G.obj (Opposite.op X₁)).obj Y₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (adj₂.homEquiv (CategoryTheory.CategoryStruct.comp g f₃)) h =
    CategoryTheory.CategoryStruct.comp (adj₂.homEquiv g)
      (CategoryTheory.CategoryStruct.comp ((G.obj (Opposite.op X₁)).map f₃) h)
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
IsSymmetricAlgebra.equiv.congr_simp : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] {f f_1 : M →ₗ[R] A} (e_f : f = f_1) (h : IsSymmetricAlgebra f),
  h.equiv = ⋯.equiv
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.monomial_sum_index : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {α : Type u_2} (s : Finset α) (f : α → σ →₀ ℕ) (a : R),
  (MvPolynomial.monomial (∑ i ∈ s, f i)) a = MvPolynomial.C a * ∏ i ∈ s, (MvPolynomial.monomial (f i)) 1
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast_insertEntry_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.getValueCast k (Std.Internal.List.insertEntry k v l) ⋯ = v
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKeyD_alter_eq_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : Option β → Option β},
  t.alter k f ≠ ∅ →
    ∀ {fallback : α}, (t.alter k f).maxKeyD fallback = k ↔ (f t[k]?).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.Order.Filter.Map
Filter.comap_principal : ∀ {α : Type u_1} {β : Type u_2} {m : α → β} {t : Set β},
  Filter.comap m (Filter.principal t) = Filter.principal (m ⁻¹' t)
-- Mathlib.Order.Directed
OrderBot.instIsCodirectedOrder : ∀ {α : Type u_1} [inst : LE α] [OrderBot α], IsCodirectedOrder α
-- Mathlib.InformationTheory.Hamming
Hamming.instDist : {ι : Type u_2} → {β : ι → Type u_3} → [Fintype ι] → [(i : ι) → DecidableEq (β i)] → Dist (Hamming β)
-- Mathlib.MeasureTheory.Measure.Count
MeasureTheory.Measure.count_apply_lt_top' : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α},
  MeasurableSet s → (MeasureTheory.Measure.count s < ⊤ ↔ s.Finite)
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanModule : Type
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
/-- If `J` is an ideal of `A`, then `I⬝J` is a sub-dp-ideal of `I`.
See [P. Berthelot, *Cohomologie cristalline des schémas de caractéristique $p$ > 0*,
(Proposition 1.6.1 (i))][Berthelot-1974]  -/
DividedPowers.SubDPIdeal.prod : {A : Type u_1} → [inst : CommSemiring A] → {I : Ideal A} → {hI : DividedPowers I} → Ideal A → hI.SubDPIdeal
-- Mathlib.Analysis.Normed.Group.Continuity
ContinuousWithinAt.enorm : ∀ {E : Type u_7} [inst : TopologicalSpace E] [inst_1 : ContinuousENorm E] {X : Type u_8} [inst_2 : TopologicalSpace X]
  {f : X → E} {s : Set X} {a : X}, ContinuousWithinAt f s a → ContinuousWithinAt (fun x => ‖f x‖ₑ) s a
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- the projection from `S.X₂`  -/
CategoryTheory.ShortComplex.RightHomologyData.p : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} → (self : S.RightHomologyData) → S.X₂ ⟶ self.Q
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.top_boxes : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι}, ⊤.boxes = {I}
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.FinMeasAdditive.smul : ∀ {α : Type u_1} {𝕜 : Type u_6} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} {T : Set α → β}
  [inst : AddMonoid β] [inst_1 : DistribSMul 𝕜 β],
  MeasureTheory.FinMeasAdditive μ T → ∀ (c : 𝕜), MeasureTheory.FinMeasAdditive μ fun s => c • T s
-- Mathlib.CategoryTheory.Presentable.Dense
CategoryTheory.IsCardinalAccessibleCategory.instIsDenseFullSubcategoryIsCardinalPresentableι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalAccessibleCategory C κ], (CategoryTheory.isCardinalPresentable C κ).ι.IsDense
-- Init.Data.SInt.Bitwise
ISize.toInt16_and : ∀ (a b : ISize), (a &&& b).toInt16 = a.toInt16 &&& b.toInt16
-- Mathlib.Topology.Order.IsLUB
upperClosure_eq_Ici_csInf : ∀ {α : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  {s : Set α}, s.Nonempty → BddBelow s → IsClosed s → ↑(upperClosure s) = Set.Ici (sInf s)
-- Lean.Meta.Sym.Arith.Poly
_private.Lean.Meta.Sym.Arith.Poly.0.Lean.Grind.CommRing.Mon.sharesVar.match_1.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) → (Unit → motive Ordering.eq) → (Unit → motive Ordering.lt) → (Unit → motive Ordering.gt) → motive x
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.PolyDerivation.input : Lean.Grind.CommRing.Poly → Lean.Meta.Grind.Arith.CommRing.PolyDerivation
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.LaxTrans.instInhabited : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F : CategoryTheory.LaxFunctor B C} → Inhabited (CategoryTheory.Lax.LaxTrans F F)
-- Init.SizeOf
Lean.MacroScopesView.mk.sizeOf_spec : ∀ (name imported ctx : Lean.Name) (scopes : List Lean.MacroScope),
  sizeOf { name := name, imported := imported, ctx := ctx, scopes := scopes } =
    1 + sizeOf name + sizeOf imported + sizeOf ctx + sizeOf scopes
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- Take a convex combination of two points.  -/
Convexity.convexCombPair : {R : Type u_1} →
  {M : Type u_3} →
    [inst : PartialOrder R] →
      [inst_1 : Semiring R] →
        [inst_2 : IsStrictOrderedRing R] →
          [Convexity.ConvexSpace R M] → (s t : R) → 0 ≤ s → 0 ≤ t → s + t = 1 → M → M → M
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRank_eq_top_iff : ∀ {α : Type u_1} (M : Matroid α), M.eRank = ⊤ ↔ M.RankInfinite
-- Mathlib.Order.Filter.Defs
Filter.mem_mk : ∀ {α : Type u_1} {s : Set α} {t : Set (Set α)} {h₁ : Set.univ ∈ t} {h₂ : ∀ {x y : Set α}, x ∈ t → x ⊆ y → y ∈ t}
  {h₃ : ∀ {x y : Set α}, x ∈ t → y ∈ t → x ∩ y ∈ t},
  s ∈ { sets := t, univ_sets := h₁, sets_of_superset := h₂, inter_sets := h₃ } ↔ s ∈ t
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of `SimpleGraph.Walk.darts_bypass_subset_darts`. -/
SimpleGraph.Walk.darts_bypass_subset : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] (p : G.Walk u v), p.bypass.darts ⊆ p.darts
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.Basis.j_self : ∀ (R : Type u_1) [inst : CommRing R] {c₁ c₂ c₃ : R},
  (QuaternionAlgebra.Basis.self R).j = { re := 0, imI := 0, imJ := 1, imK := 0 }
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.restrictScalars_adjoin_eq_sup : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (K : IntermediateField F E)
  (S : Set E), IntermediateField.restrictScalars F (IntermediateField.adjoin (↥K) S) = K ⊔ IntermediateField.adjoin F S
-- Std.Async.Signal
/-- Real-time timer expired.
 -/
Std.Async.Signal.sigalrm : Std.Async.Signal
-- Mathlib.Probability.ProbabilityMassFunction.Monad
PMF.bind_pure : ∀ {α : Type u_1} (p : PMF α), p.bind PMF.pure = p
-- Init.PropLemmas
ite_else_decide_not_self : ∀ (p : Prop) [h : Decidable p] {w : Decidable p} (q : Bool), (if p then q else !decide p) = (!decide p || q)
-- Init.Data.SInt.Lemmas
Int16.sub_left_inj : ∀ {a b : Int16} (c : Int16), a - c = b - c ↔ a = b
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.addEquivBiprod_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y₁ Y₂ : C} {n : ℕ}
  (e : CategoryTheory.Abelian.Ext X Y₁ n × CategoryTheory.Abelian.Ext X Y₂ n),
  CategoryTheory.Abelian.Ext.addEquivBiprod.symm e =
    e.1.comp (CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.Limits.biprod.inl) ⋯ +
      e.2.comp (CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.Limits.biprod.inr) ⋯
-- Lean.Parser.Types
Lean.Parser.instInhabitedParserFn : Inhabited Lean.Parser.ParserFn
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.all_toList : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [LawfulHashable α] [EquivBEq α]
  {p : α → Bool}, m.WF → m.toList.all p = m.all p
-- Init.Tactics
/-- The left hand side of an induction arm, `| foo a b c` or `| @foo a b c`
where `foo` is a constructor of the inductive type and `a b c` are the arguments
to the constructor.
 -/
Lean.Parser.Tactic.inductionAltLHS : Lean.ParserDescr
-- Mathlib.RingTheory.Coalgebra.GroupLike
/-- A group-like element in a coalgebra is an element `a` such that `ε(a) = 1` and `Δ(a) = a ⊗ₜ a`,
where `ε` and `Δ` are the counit and comultiplication respectively.  -/
IsGroupLikeElem : (R : Type u_2) →
  {A : Type u_3} →
    [inst : CommSemiring R] → [inst_1 : AddCommMonoid A] → [inst_2 : Module R A] → [Coalgebra R A] → A → Prop
-- Init.Meta.Defs
Lean.Syntax.copyHeadTailInfoFrom : Lean.Syntax → Lean.Syntax → Lean.Syntax
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.findSomeM?_eq_match_step : ∀ {α β : Type w} {γ : Type x} {m : Type x → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α Id β]
  [inst_2 : Std.IteratorLoop α Id m] [LawfulMonad m] [Std.Iterators.Finite α Id] [Std.LawfulIteratorLoop α Id m]
  {it : Std.Iter β} {f : β → m (Option γ)},
  it.findSomeM? f =
    match ↑it.step with
    | Std.IterStep.yield it' out => do
      let __do_lift ← f out
      match __do_lift with
        | none => it'.findSomeM? f
        | some fx => pure (some fx)
    | Std.IterStep.skip it' => it'.findSomeM? f
    | Std.IterStep.done => pure none
-- Mathlib.Algebra.FreeMonoid.Symbols
/-- the set of unique symbols in a free monoid element  -/
FreeMonoid.symbols : {α : Type u_1} → [DecidableEq α] → FreeMonoid α → Finset α
-- Init.Data.Iterators.Producers.Monadic.List
_private.Init.Data.Iterators.Producers.Monadic.List.0.Std.Iterators.Types.ListIterator.instFinitenessRelation : {α : Type w} →
  {m : Type w → Type w'} → [inst : Pure m] → Std.Iterators.FinitenessRelation (Std.Iterators.Types.ListIterator α) m
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.matchesAt_iff_matchesAt_ofSliceFrom : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {base : s.Pos}
  {pos : (s.sliceFrom base).Pos},
  String.Slice.Pattern.Model.MatchesAt pat pos ↔
    String.Slice.Pattern.Model.MatchesAt pat (String.Slice.Pos.ofSliceFrom pos)
-- Mathlib.Analysis.Meromorphic.Basic
/-- If `f` is meromorphic, then so is its logarithmic derivative.  -/
Meromorphic.logDeriv : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] [CompleteSpace 𝕜'] {f : 𝕜 → 𝕜'}, Meromorphic f → Meromorphic (logDeriv f)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.map_equiv_congr : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β),
  (↑m₁).Equiv ↑m₂ →
    ∀ {f : (a : α) → β a → γ a}, (↑(Std.DHashMap.Internal.Raw₀.map f m₁)).Equiv ↑(Std.DHashMap.Internal.Raw₀.map f m₂)
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.dual_coindep_iff : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M✶.Coindep X ↔ M.Indep X
-- Mathlib.Analysis.Complex.Convex
Complex.isConnected_of_lowerHalfPlane : ∀ {r : ℝ} {s : Set ℂ}, {z | z.im < r} ⊆ s → s ⊆ {z | z.im ≤ r} → IsConnected s
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Defs
/-- The norm of a vector measure is σ-subadditive on measurable sets.  -/
MeasureTheory.VectorMeasure.isSigmaSubadditiveSetFun_enorm : ∀ {X : Type u_1} {mX : MeasurableSpace X} {V : Type u_2} [inst : TopologicalSpace V] [inst_1 : ENormedAddCommMonoid V]
  [T2Space V] (μ : MeasureTheory.VectorMeasure X V), MeasureTheory.IsSigmaSubadditiveSetFun fun x => ‖μ x‖ₑ
-- Mathlib.Data.Finset.Basic
Finset.filter_and_not : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α) (p q : α → Prop) [inst_1 : DecidablePred p]
  [inst_2 : DecidablePred q], {a ∈ s | p a ∧ ¬q a} = Finset.filter p s \ Finset.filter q s
-- Mathlib.Algebra.Polynomial.Div
/-- See `Polynomial.eq_leadingCoeff_mul_of_monic_of_dvd_of_natDegree_le`
for the other multiplication order. That version, unlike this one, requires commutativity.  -/
Polynomial.eq_mul_leadingCoeff_of_monic_of_dvd_of_natDegree_le : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R},
  p.Monic → p ∣ q → q.natDegree ≤ p.natDegree → q = p * Polynomial.C q.leadingCoeff
-- Mathlib.LinearAlgebra.Multilinear.Pi
/-- `MultilinearMap.piFamily` as a linear map.  -/
MultilinearMap.piFamilyₗ : {ι : Type uι} →
  {κ : ι → Type uκ} →
    {R : Type uR} →
      {M : (i : ι) → κ i → Type uM} →
        {N : ((i : ι) → κ i) → Type uN} →
          [inst : CommSemiring R] →
            [inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)] →
              [inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)] →
                [inst_3 : (i : ι) → (k : κ i) → Module R (M i k)] →
                  [inst_4 : (p : (i : ι) → κ i) → Module R (N p)] →
                    ((p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)) →ₗ[R]
                      MultilinearMap R (fun i => (j : κ i) → M i j) ((t : (i : ι) → κ i) → N t)
-- Mathlib.Algebra.DirectSum.Internal
/-- The commutative semiring `A 0` inherited from `R` in the presence of
`SetLike.GradedMonoid A`.  -/
SetLike.GradeZero.instCommSemiring : {ι : Type u_1} →
  {σ : Type u_2} →
    {R : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : AddMonoid ι] →
          [inst_2 : SetLike σ R] →
            [AddSubmonoidClass σ R] → (A : ι → σ) → [SetLike.GradedMonoid A] → CommSemiring ↥(A 0)
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_eq_neg_one_of_neg_of_le : ∀ {a b : ℤ}, a < 0 → -a ≤ b → a / b = -1
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.image_eq_range : ∀ {X Y : SSet} (A : X.Subcomplex) (f : X ⟶ Y),
  A.image f = SSet.Subcomplex.range (CategoryTheory.CategoryStruct.comp A.ι f)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- The `top` subgraph is `G` as a subgraph of itself.  -/
SimpleGraph.Subgraph.instTop : {V : Type u} → {G : SimpleGraph V} → Top G.Subgraph
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.IsBilimit.mk.sizeOf_spec : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} {b : CategoryTheory.Limits.BinaryBicone P Q} [inst_2 : SizeOf C]
  (isLimit : CategoryTheory.Limits.IsLimit b.toCone) (isColimit : CategoryTheory.Limits.IsColimit b.toCocone),
  sizeOf { isLimit := isLimit, isColimit := isColimit } = 1 + sizeOf isLimit + sizeOf isColimit
-- Init.Data.Bool
Bool.lt_asymm : ∀ {x y : Bool}, x < y → ¬y < x
-- Mathlib.Combinatorics.Derangements.Basic
derangements.Equiv.RemoveNone.fiber.congr_simp : ∀ {α : Type u_1} {inst : DecidableEq α} [inst_1 : DecidableEq α] (a a_1 : Option α),
  a = a_1 →
    ∀ (a_2 a_3 : Equiv.Perm α),
      a_2 = a_3 → derangements.Equiv.RemoveNone.fiber a a_2 = derangements.Equiv.RemoveNone.fiber a_1 a_3
-- Mathlib.Topology.MetricSpace.Gluing
Metric.toGlueR.eq_1 : ∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : Nonempty Z] [inst_1 : MetricSpace Z] [inst_2 : MetricSpace X]
  [inst_3 : MetricSpace Y] {Φ : Z → X} {Ψ : Z → Y} (hΦ : Isometry Φ) (hΨ : Isometry Ψ) (y : Y),
  Metric.toGlueR hΦ hΨ y = Quotient.mk'' (Sum.inr y)