mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.yonedaAddMon_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N X Y : C} [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.AddMonObj N]
  (α : CategoryTheory.yonedaAddMonObj M ⟶ CategoryTheory.yonedaAddMonObj N) (f : X ⟶ Y) (g : Y ⟶ M),
  (CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op X))) (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp f ((CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op Y))) g)
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- `s` is the morphism witnessing symmetry  -/
CategoryTheory.EquivalenceRelation.s : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {R X : C} → {p₁ p₂ : R ⟶ X} → CategoryTheory.EquivalenceRelation p₁ p₂ → (R ⟶ R)
-- Mathlib.Algebra.Order.Group.Cone
AddGroupCone.mk : {G : Type u_1} →
  [inst : AddCommGroup G] →
    (toAddSubmonoid : AddSubmonoid G) →
      (∀ {a : G}, a ∈ toAddSubmonoid.carrier → -a ∈ toAddSubmonoid.carrier → a = 0) → AddGroupCone G
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabRco : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
SimpleGraph.isBipartiteWith_comm : ∀ {V : Type u_1} {G : SimpleGraph V} {s t : Set V}, G.IsBipartiteWith s t ↔ G.IsBipartiteWith t s
-- Mathlib.Data.ZMod.QuotientGroup
finite_zmultiples : ∀ {α : Type u_3} [inst : AddGroup α] {a : α}, (↑(AddSubgroup.zmultiples a)).Finite ↔ IsOfFinAddOrder a
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.limitConeIsLimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteAddGrp.{max v u}),
  ProfiniteAddGrp.limitConeIsLimit F =
    {
      lift := fun cone =>
        ProfiniteAddGrp.ofHom
          (let __src :=
            TopCat.Hom.hom
              ((Profinite.limitConeIsLimit (F.comp (CategoryTheory.forget₂ ProfiniteAddGrp.{max u v} Profinite))).lift
                  ((CategoryTheory.forget₂ ProfiniteAddGrp.{max u v} Profinite).mapCone cone)).hom;
          { toFun := __src.toFun, map_zero' := ⋯, map_add' := ⋯, continuous_toFun := ⋯ }),
      fac := ⋯, uniq := ⋯ }
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- Transfer reflection of colimits along a natural isomorphism in the functor.  -/
CategoryTheory.Limits.reflectsColimits_of_natIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (h : F ≅ G)
  [CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} G
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.cancelDen.injEq : ∀ (c : Lean.Meta.Grind.Arith.Linear.RingEqCnstr) (val : ℤ) (x n : Lean.Grind.Linarith.Var)
  (c_1 : Lean.Meta.Grind.Arith.Linear.RingEqCnstr) (val_1 : ℤ) (x_1 n_1 : Lean.Grind.Linarith.Var),
  (Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.cancelDen c val x n =
      Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.cancelDen c_1 val_1 x_1 n_1) =
    (c = c_1 ∧ val = val_1 ∧ x = x_1 ∧ n = n_1)
-- Mathlib.Order.Sublattice
Sublattice.coe_inf' : ∀ {α : Type u_2} [inst : Lattice α] (L M : Sublattice α), ↑(L ⊓ M) = ↑L ∩ ↑M
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.instInhabitedState.default : Lean.Meta.Grind.Arith.Cutsat.State
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.HasSubst.pow : ∀ {σ : Type u_1} {τ : Type u_4} {S : Type u_5} [inst : CommRing S] {n : ℕ},
  n ≠ 0 → ∀ {a : σ → MvPowerSeries τ S}, MvPowerSeries.HasSubst a → MvPowerSeries.HasSubst (a ^ n)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- `sigmaObj f` computes the coproduct of a family of elements `f`.
(It is defined as an abbreviation for `colimit (Discrete.functor f)`,
so for most facts about `sigmaObj f`, you will just use general facts about colimits.)  -/
CategoryTheory.Limits.sigmaObj : {β : Type w} →
  {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (f : β → C) → [CategoryTheory.Limits.HasCoproduct f] → C
-- Mathlib.Topology.Constructions.SumProd
Filter.Eventually.prod_inl_nhds : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {p : X → Prop} {x : X},
  (∀ᶠ (x : X) in nhds x, p x) → ∀ (y : Y), ∀ᶠ (x : X × Y) in nhds (x, y), p x.1
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosDef.eq_1 : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] (M : Matrix n n R),
  M.PosDef = (M.IsHermitian ∧ ∀ ⦃x : n →₀ R⦄, x ≠ 0 → 0 < x.sum fun i xi => x.sum fun j xj => star xi * M i j * xj)
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.Extension.State.mk.sizeOf_spec : ∀ (map : Lean.SMap Lean.Name Lean.Meta.MatcherInfo), sizeOf { map := map } = 1 + sizeOf map
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
/-- An instance of an mutually inductive group of inductives, identified by the `all` array
and the level and expressions parameters.

For example this distinguishes between `List α` and `List β` so that we will not even attempt
mutual structural recursion on such incompatible types.
 -/
Lean.Elab.Structural.IndGroupInst : Type
-- Std.Time.Duration
Std.Time.Duration.instHSubOffset_2 : HSub Std.Time.Duration Std.Time.Hour.Offset Std.Time.Duration
-- Mathlib.RingTheory.FormalGroup.Basic
_private.Mathlib.RingTheory.FormalGroup.Basic.0.termY₀ : Lean.ParserDescr
-- Mathlib.Combinatorics.Derangements.Basic
/-- The set of derangements on `Option α` is equivalent to the union over all `a : α` of
"derangements on `α` ⊕ derangements on `{a}ᶜ`".  -/
derangements.derangementsRecursionEquiv : {α : Type u_1} → [DecidableEq α] → ↑(derangements (Option α)) ≃ (a : α) × (↑(derangements ↑{a}ᶜ) ⊕ ↑(derangements α))
-- Mathlib.Topology.Sober
IsGenericPoint.eq_1 : ∀ {α : Type u_1} [inst : TopologicalSpace α] (x : α) (S : Set α), IsGenericPoint x S = (closure {x} = S)
-- Mathlib.GroupTheory.HNNExtension
/-- A reduced word is a `head`, which is an element of `G`, followed by the product list of pairs.
There should also be no sequences of the form `t^u * g * t^-u`, where `g` is in
`toSubgroup A B u`. This is a less strict condition than required for `NormalWord`.  -/
HNNExtension.NormalWord.ReducedWord : (G : Type u_1) → [inst : Group G] → Subgroup G → Subgroup G → Type u_1
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instCommSemigroupOfMulHomClass : {ι : 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 : (i : ι) → CommSemigroup (G i)] →
                  [∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)] → CommSemigroup (DirectLimit G f)
-- Mathlib.Algebra.Field.Subfield.Defs
/-- A subfield is closed under division.  -/
Subfield.div_mem : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K) {x y : K}, x ∈ s → y ∈ s → x / y ∈ s
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
circleMap_zero_im : ∀ (r θ : ℝ), (circleMap 0 r θ).im = r * Real.sin θ
-- Mathlib.Algebra.Order.Ring.IsNonarchimedean
IsNonarchimedean.finset_powerset_image_add : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {F : Type u_2} {α : Type u_3}
  {β : Type u_4} [inst_3 : CommRing α] [inst_4 : FunLike F α R] [AddGroupSeminormClass F α R] {f : F},
  IsNonarchimedean ⇑f →
    ∀ (s : Finset β) (b : β → α) (m : ℕ),
      ∃ u, f (∑ t ∈ Finset.powersetCard (s.card - m) s, ∏ i ∈ t, -b i) ≤ f (∏ i ∈ ↑u, -b i)
-- Aesop.Tree.Check
_private.Aesop.Tree.Check.0.Aesop.MVarClusterRef.checkAcyclic.go : {α : Type} → IO.Ref (Array (IO.Ref α)) → IO.Ref α → Lean.CoreM Bool
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
/-- A family is a transcendence basis if it is a maximal algebraically independent subset.  -/
IsTranscendenceBasis : {ι : Type u_1} →
  (R : Type u_3) → {A : Type u_5} → [inst : CommRing R] → [inst_1 : CommRing A] → [Algebra R A] → (ι → A) → Prop
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.mem_of_mem_union_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t₁ ∪ t₂ → k ∉ t₂ → k ∈ t₁
-- Mathlib.GroupTheory.Nilpotent
/-- The nilpotency class of an additive subgroup is less or equal to the nilpotency
class of the additive group.  -/
AddSubgroup.nilpotencyClass_le : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [hG : AddGroup.IsNilpotent G],
  AddGroup.nilpotencyClass ↥H ≤ AddGroup.nilpotencyClass G
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_pair_zero : ∀ {α : Type u} [inst : Semiring α] (x : α), Ideal.span {x, 0} = Ideal.span {x}
-- Mathlib.LinearAlgebra.Dimension.RankNullity
/-- Rank-nullity theorem using `finrank`.  -/
Submodule.finrank_quotient_add_finrank : ∀ {R : Type u_1} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [HasRankNullity.{u, u_1} R] [StrongRankCondition R] [Module.Finite R M] (N : Submodule R M),
  Module.finrank R (M ⧸ N) + Module.finrank R ↥N = Module.finrank R M
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
Group.isCyclic_of_coprime_card_range_card_ker : ∀ {M : Type u_4} {N : Type u_5} [inst : CommGroup M] [inst_1 : Group N] (f : M →* N),
  (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range) → ∀ [IsCyclic ↥f.ker] [IsCyclic ↥f.range], IsCyclic M
-- Mathlib.Data.Rel
/-- The identity relation.  -/
SetRel.id : {α : Type u_1} → SetRel α α
-- Aesop.Rule.Name
Aesop.instToJsonScopeName.toJson : Aesop.ScopeName → Lean.Json
-- Mathlib.Data.Int.Cast.Prod
Prod.fst_intCast : ∀ {α : Type u_1} {β : Type u_2} [inst : AddGroupWithOne α] [inst_1 : AddGroupWithOne β] (n : ℤ), (↑n).1 = ↑n
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instRightCancelSemigroup.eq_1 : ∀ {α : Type u_1} [inst : RightCancelSemigroup α],
  OrderDual.instRightCancelSemigroup = { toSemigroup := OrderDual.instSemigroup, toIsRightCancelMul := ⋯ }
-- Mathlib.Data.Stream.Init
Stream'.append_right_inj : ∀ {α : Type u} (x : List α) (a b : Stream' α), x ++ₛ a = x ++ₛ b ↔ a = b
-- Init.Data.UInt.Bitwise
UInt16.not_xor : ∀ {a b : UInt16}, ~~~a ^^^ b = ~~~(a ^^^ b)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.toArray_eq_match_step.match_1.eq_2 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
/-- A countable sequence of sets generating the measurable space.  -/
MeasurableSpace.natGeneratingSequence : (α : Type u_3) → [inst : MeasurableSpace α] → [MeasurableSpace.CountablyGenerated α] → ℕ → Set α
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.coneMorphism.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F] (c : CategoryTheory.Limits.Cone F),
  CategoryTheory.Limits.limit.coneMorphism c = (CategoryTheory.Limits.limit.isLimit F).liftConeMorphism c
-- Lean.Parser.Do
Lean.Parser.Term.nestedAction.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.List.ToArray
List.isEmpty_toArray : ∀ {α : Type u_1} (l : List α), l.toArray.isEmpty = l.isEmpty
-- Mathlib.SetTheory.ZFC.Ordinal
ZFSet.isTransitive_iff_mem_trans : ∀ {z : ZFSet.{u}}, z.IsTransitive ↔ ∀ {x y : ZFSet.{u}}, x ∈ y → y ∈ z → x ∈ z
-- Mathlib.FieldTheory.PurelyInseparable.AdjoinPthRoots
instIsPurelyInseparableAdjoinPthRoots : ∀ {k : Type u_1} [inst : Field k], IsPurelyInseparable k (AdjoinPthRoots k)
-- Lean.Elab.Binders
Lean.Elab.Term.expandExplicitFun : Lean.Macro
-- Mathlib.Analysis.Normed.Lp.lpHolder
lp.norm_dualPairing : ∀ {ι : Type u_1} {𝕜 : Type u_2} {E : ι → Type u_3} {F : ι → Type u_4} [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)] {p q : ENNReal} {H : Type u_6}
  [inst_5 : NormedAddCommGroup H] [inst_6 : NormedSpace 𝕜 H] [inst_7 : CompleteSpace H] [inst_8 : Fact (1 ≤ p)]
  [inst_9 : Fact (1 ≤ q)] [inst_10 : p.HolderConjugate q] (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] H) {K : NNReal}
  (hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K), ‖lp.dualPairing p q B hBK‖ ≤ ↑K
-- Mathlib.CategoryTheory.Dialectica.Basic
CategoryTheory.Dial.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : SizeOf C] (src tgt : C) (rel : CategoryTheory.Subobject (src ⨯ tgt)),
  sizeOf { src := src, tgt := tgt, rel := rel } = 1 + sizeOf src + sizeOf tgt + sizeOf rel
-- Mathlib.Analysis.Calculus.LHopital
deriv.lhopital_zero_left_on_Ioo : ∀ {a b : ℝ} {l : Filter ℝ} {f g : ℝ → ℝ},
  a < b →
    DifferentiableOn ℝ f (Set.Ioo a b) →
      (∀ x ∈ Set.Ioo a b, deriv g x ≠ 0) →
        Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds 0) →
          Filter.Tendsto g (nhdsWithin b (Set.Iio b)) (nhds 0) →
            Filter.Tendsto (fun x => deriv f x / deriv g x) (nhdsWithin b (Set.Iio b)) l →
              Filter.Tendsto (fun x => f x / g x) (nhdsWithin b (Set.Iio b)) l
-- Mathlib.CategoryTheory.Sites.CoverPreserving
/-- A functor `G : (C, J) ⥤ (D, K)` between sites is called compatible preserving if for each
compatible family of elements at `C` and valued in `G.op ⋙ ℱ`, and each commuting diagram
`f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂`, `x g₁` and `x g₂` coincide when restricted via `fᵢ`.
This is actually stronger than merely preserving compatible families because of the definition of
`functorPushforward` used.
 -/
CategoryTheory.CompatiblePreserving : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.GrothendieckTopology D → CategoryTheory.Functor C D → Prop
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.ofIsLeftAdjoint.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (left : CategoryTheory.Functor C D) [inst_2 : left.IsLeftAdjoint],
  CategoryTheory.Adjunction.ofIsLeftAdjoint left = ⋯.some
-- Mathlib.CategoryTheory.Limits.Types.Equalizers
/-- The categorical equalizer in `Type u` is `{x : Y // g x = h x}`.  -/
CategoryTheory.Limits.Types.equalizerIso : {Y Z : Type u} →
  (g h : Y ⟶ Z) →
    CategoryTheory.Limits.equalizer g h ≅
      { x // (CategoryTheory.ConcreteCategory.hom g) x = (CategoryTheory.ConcreteCategory.hom h) x }
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.two_nsmul_toReal_eq_two_mul_add_two_pi : ∀ {θ : Real.Angle}, (2 • θ).toReal = 2 * θ.toReal + 2 * Real.pi ↔ θ.toReal ≤ -Real.pi / 2
-- Init.Data.List.Lemmas
List.any_beq : ∀ {α : Type u_1} [inst : BEq α] {l : List α} {a : α}, (l.any fun x => a == x) = l.contains a
-- Lean.Meta.Tactic.SplitIf
/-- The `Simp.Context` that used to be used with `simpIf` methods. It contains all congruence theorems, but
just the rewriting rules for reducing `if` expressions.
This function is only used when the old `split` tactic behavior is enabled.
 -/
Lean.Meta.SplitIf.getSimpContext : Lean.MetaM Lean.Meta.Simp.Context
-- Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
ChartedSpace.locallyRingedSpaceMap_base : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {EM : Type u_1} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_2} [inst_3 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM}
  {M : Type u} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace HM M] {EN : Type u_3}
  [inst_6 : NormedAddCommGroup EN] [inst_7 : NormedSpace 𝕜 EN] {HN : Type u_4} [inst_8 : TopologicalSpace HN]
  {IN : ModelWithCorners 𝕜 EN HN} {N : Type u} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace HN N] (f : M → N)
  (hf : ContMDiff IM IN (↑⊤) f),
  (ChartedSpace.locallyRingedSpaceMap f hf).base = TopCat.ofHom { toFun := f, continuous_toFun := ⋯ }
-- Std.Sat.AIG.Relabel
Std.Sat.AIG.Decl.relabel_comp : ∀ {α β γ : Type} (decl : Std.Sat.AIG.Decl α) (g : α → β) (h : β → γ),
  Std.Sat.AIG.Decl.relabel (h ∘ g) decl = Std.Sat.AIG.Decl.relabel h (Std.Sat.AIG.Decl.relabel g decl)
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingAfter_empty : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Preorder ι] [inst_1 : InfSet ι] {u : ι → Ω → β} (n : ι),
  MeasureTheory.hittingAfter u ∅ n = fun x => ⊤
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Modify an element in the set with the given function,
doing nothing if the key is not found.
Note that the element returned by `f` must be equivalent to `x`.

```
alter f 0 {1, 2, 3} = {1, 2, 3}     if f none = none
                    = {a, 1, 2, 3}  if f none = some a
alter f 1 {1, 2, 3} = {2, 3}     if f 1 = none
                    = {a, 2, 3}  if f 1 = some a
```  -/
Ordnode.alter : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → (Option α → Option α) → α → Ordnode α → Ordnode α
-- Lean.Elab.PatternVar
_private.Lean.Elab.PatternVar.0.Lean.Elab.Term.CollectPatternVars.throwCtorExpected : {α : Type} → Option Lean.Syntax → Lean.Elab.Term.CollectPatternVars.M α
-- Mathlib.RingTheory.Perfection
/-- The `n`-th coefficient of an element of the perfection of `O/(p)`.  -/
PreTilt.coeff : {O : Type u₂} →
  [inst : CommRing O] →
    {p : ℕ} → [inst_1 : Fact (Nat.Prime p)] → [inst_2 : Fact ¬IsUnit ↑p] → ℕ → PreTilt O p →+* ModP O p
-- Mathlib.Order.Cover
CovBy.Icc_eq : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ⋖ b → Set.Icc a b = {a, b}
-- Mathlib.Data.Set.Sups
upperClosure_sups : ∀ {α : Type u_2} [inst : SemilatticeSup α] (s t : Set α), upperClosure (s ⊻ t) = upperClosure s ⊔ upperClosure t
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey_le_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (hc : k ∈ t), (cmp (t.minKey ⋯) k).isLE = true
-- Mathlib.Analysis.Asymptotics.Defs
/-- Definition of `IsLittleO` in terms of filters.  -/
Asymptotics.isLittleO_iff : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F} {l : Filter α},
  f =o[l] g ↔ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.cliqueNum_induce_le : ∀ {α : Type u_3} {G : SimpleGraph α} [Finite α] (s : Set α), (SimpleGraph.induce s G).cliqueNum ≤ G.cliqueNum
-- Mathlib.Analysis.RCLike.Extend
Module.Dual.im_extendRCLike_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {F : Type u_2} [inst_1 : AddCommGroup F] [inst_2 : Module ℝ F] [inst_3 : Module 𝕜 F]
  [inst_4 : IsScalarTower ℝ 𝕜 F] (g : Module.Dual ℝ F) (x : F), RCLike.im (g.extendRCLike x) = -g (RCLike.I • x)
-- Mathlib.Order.Interval.Basic
NonemptyInterval.ext : ∀ {α : Type u_6} {inst : LE α} {x y : NonemptyInterval α}, x.toProd = y.toProd → x = y
-- Mathlib.CategoryTheory.CommSq
/-- Square has a `LiftStruct`.  -/
CategoryTheory.CommSq.HasLift.exists_lift : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y}
  {g : B ⟶ Y} {sq : CategoryTheory.CommSq f i p g} [self : sq.HasLift], Nonempty sq.LiftStruct
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDerivWithin_comp_const_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜},
  x ∈ s →
    UniqueDiffOn 𝕜 s →
      ∀ {f : 𝕜 → F},
        ContDiffOn 𝕜 (↑n) f s →
          ∀ (c : 𝕜),
            Set.MapsTo (fun x => c * x) s s →
              iteratedDerivWithin n (fun x => f (c * x)) s x = c ^ n • iteratedDerivWithin n f s (c * x)
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_of_fmod_eq_zero : ∀ {a b : ℤ}, b.fmod a = 0 → a ∣ b
-- Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Algebra.GrothendieckAddGroup.lift_symm_apply : ∀ {M : Type u_1} {G : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommGroup G]
  (f : Algebra.GrothendieckAddGroup M →+ G),
  Algebra.GrothendieckAddGroup.lift.symm f = f.comp Algebra.GrothendieckAddGroup.of
-- Lean.Data.Lsp.Internal
Lean.Lsp.instToJsonLeanQueryModuleResponse : Lean.ToJson Lean.Lsp.LeanQueryModuleResponse
-- Mathlib.Algebra.Group.Submonoid.Basic
AddSubmonoid.mem_closure_of_mem : ∀ {M : Type u_1} [inst : AddZeroClass M] {s : Set M} {x : M}, x ∈ s → x ∈ AddSubmonoid.closure s
-- Mathlib.RingTheory.Ideal.Height
Ideal.height_ne_top_of_isPrime : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} [I.FiniteHeight] [I.IsPrime], I.height ≠ ⊤
-- Lean.Attributes
Lean.AttributeKind.global.sizeOf_spec : sizeOf Lean.AttributeKind.global = 1
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.support_rotate : ∀ {V : Type u} {G : SimpleGraph V} {v : V} [inst : DecidableEq V] (c : G.Walk v v) (u : V) (h : u ∈ c.support),
  (c.rotate u h).support.tail ~r c.support.tail
-- Mathlib.Geometry.Euclidean.Sphere.SecondInter
/-- The second intersection of a sphere with a line through a point on that sphere; that point
if it is the only point of intersection of the line with the sphere. The intended use of this
definition is when `p ∈ s`; the definition does not use `s.radius`, so in general it returns
the second intersection with the sphere through `p` and with center `s.center`.  -/
EuclideanGeometry.Sphere.secondInter : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] → [NormedAddTorsor V P] → EuclideanGeometry.Sphere P → P → V → P
-- Init.Data.List.Lemmas
List.not_mem_cons_of_ne_of_not_mem : ∀ {α : Type u_1} {a y : α} {l : List α}, a ≠ y → a ∉ l → a ∉ y :: l
-- Mathlib.Util.GetAllModules
/-- `getAllFiles git ml` takes all `.lean` files in the directory `ml`
(recursing into sub-directories) and returns the `Array` of `String`s
```
#[file₁, ..., fileₙ]
```
of all their file names. These are not sorted in general.

The input `git` is a `Bool`ean flag:
* `true` means that the command uses `git ls-files` to find the relevant files;
* `false` means that the command recursively scans all dirs searching for `.lean` files.
 -/
getAllFiles : Bool → String → IO (Array System.FilePath)
-- Std.Data.DTreeMap.Internal.Cell
Std.DTreeMap.Internal.List.findCell_nil : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α → Ordering),
  Std.DTreeMap.Internal.List.findCell [] k = Std.DTreeMap.Internal.Cell.empty
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubMulAction.ofStabilizer_carrier : ∀ (G : Type u_1) [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] (a : α),
  (SubMulAction.ofStabilizer G a).carrier = {a}ᶜ
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.MsgEmbed.goal.injEq : ∀ (a a_1 : Lean.Widget.InteractiveGoal), (Lean.Widget.MsgEmbed.goal a = Lean.Widget.MsgEmbed.goal a_1) = (a = a_1)
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
CategoryTheory.Equalizer.Presieve.instInhabitedSecondObjBotPresieve : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) →
      {X : C} →
        [inst_1 : CategoryTheory.Limits.HasPullbacks C] → Inhabited (CategoryTheory.Equalizer.Presieve.SecondObj P ⊥)