mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
/-- A function `f` continuous on a compact set `K` is integrable on this set with respect to any
locally finite measure.  -/
ContinuousOn.integrableOn_compact' : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {K : Set X} {f : X → E}
  [MeasureTheory.IsFiniteMeasureOnCompacts μ],
  IsCompact K → MeasurableSet K → ContinuousOn f K → MeasureTheory.IntegrableOn f K μ
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.setStack : Array Std.Format → Lean.PrettyPrinter.FormatterM Unit
-- Mathlib.CategoryTheory.Limits.Opposites
/-- Turn a limit for `F : Jᵒᵖ ⥤ C` into a colimit for `F.rightOp : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.isColimitCoconeRightOpOfCone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        (F : CategoryTheory.Functor Jᵒᵖ C) →
          {c : CategoryTheory.Limits.Cone F} →
            CategoryTheory.Limits.IsLimit c →
              CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeRightOpOfCone c)
-- Std.Sat.AIG.Cached
/-- A version of `AIG.mkAtom` that uses the subterm cache in `AIG`. This version is meant for
programming, for proving purposes use `AIG.mkAtom` and equality theorems to this one.
 -/
Std.Sat.AIG.mkAtomCached : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → α → Std.Sat.AIG.Entrypoint α
-- Mathlib.Data.Matrix.Diagonal
Matrix.transpose_eq_ofNat : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : AddMonoidWithOne α] {M : Matrix n n α} {d : ℕ}
  [inst_2 : d.AtLeastTwo], M.transpose = OfNat.ofNat d ↔ M = OfNat.ofNat d
-- Init.Simproc
/-- A user-defined simplification procedure used by the `simp` tactic, and its variants.
Here is an example.
```lean
theorem and_false_eq {p : Prop} (q : Prop) (h : p = False) : (p ∧ q) = False := by simp [*]

open Lean Meta Simp
simproc ↓ shortCircuitAnd (And _ _) := fun e => do
  let_expr And p q := e | return .continue
  let r ← simp p
  let_expr False := r.expr | return .continue
  let proof ← mkAppM ``and_false_eq #[q, (← r.getProof)]
  return .done { expr := r.expr, proof? := some proof }
```
The `simp` tactic invokes `shortCircuitAnd` whenever it finds a term of the form `And _ _`.
The simplification procedures are stored in an (imperfect) discrimination tree.
The procedure should **not** assume the term `e` perfectly matches the given pattern.
The body of a simplification procedure must have type `Simproc`, which is an alias for
`Expr → SimpM Step`
You can instruct the simplifier to apply the procedure before its sub-expressions
have been simplified by using the modifier `↓` before the procedure name.
Simplification procedures can be also scoped or local.
 -/
Lean.Parser.«command__Simproc__[_]_(_):=_» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.rightOp : C ⥤ Dᵒᵖ` reflects limits of `K.leftOp : Jᵒᵖ ⥤ C`, then `F : Cᵒᵖ ⥤ D`
reflects colimits of `K : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.reflectsColimit_of_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J Cᵒᵖ)
  (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.ReflectsLimit K.leftOp F.rightOp],
  CategoryTheory.Limits.ReflectsColimit K F
-- Mathlib.Order.Bounds.Basic
IsCofinalFor.mono_right : ∀ {α : Type u_1} [inst : Preorder α] {s t u : Set α}, t ⊆ u → IsCofinalFor s t → IsCofinalFor s u
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey!_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF →
    ∀ {k : α} {v : β k},
      (t.insertIfNew k v).minKey! = t.minKey?.elim k fun k' => if cmp k k' = Ordering.lt then k else k'
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.OuterMeasure.trim_top : ∀ {α : Type u_1} [inst : MeasurableSpace α], ⊤.trim = ⊤
-- Lean.Parser.Term
/-- `let_delayed x := v; b` is similar to `let x := v; b`, but `b` is elaborated before `v`.
 -/
Lean.Parser.Term.let_delayed : Lean.Parser.Parser
-- Std.Http.Data.Response
/-- Sets the headers for the response being built.
 -/
Std.Http.Response.Builder.headers : Std.Http.Response.Builder → Std.Http.Headers → Std.Http.Response.Builder
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- If a function `f` is strongly measurable w.r.t. a sub-σ-algebra `m` and the measure is σ-finite
on `m`, then there exists spanning measurable sets with finite measure on which `f` has bounded
norm. In particular, `f` is integrable on each of those sets.  -/
MeasureTheory.StronglyMeasurable.exists_spanning_measurableSet_norm_le : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : SeminormedAddCommGroup β] {m m0 : MeasurableSpace α} (hm : m ≤ m0),
  MeasureTheory.StronglyMeasurable f →
    ∀ (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite (μ.trim hm)],
      ∃ s, (∀ (n : ℕ), MeasurableSet (s n) ∧ μ (s n) < ⊤ ∧ ∀ x ∈ s n, ‖f x‖ ≤ ↑n) ∧ ⋃ i, s i = Set.univ
-- Std.Do.SPred.SPred
Std.Do.SPred.bientails_nil : ∀ {P Q : Std.Do.SPred []}, (P ⊣⊢ₛ Q) = (P.down ↔ Q.down)
-- Init.Data.Iterators.Consumers.Total
/-- For an iterator `it`, `it.ensureTermination` provides variants of consumers that always
terminate.
 -/
Std.Iter.ensureTermination : {α β : Type w} → Std.Iter β → Std.Iter.Total β
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.group_smul_head : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} (g : G)
  (w : HNNExtension.NormalWord d), (g • w).head = g * w.head
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_singleton : ∀ {α : Type u} (x : α), Cardinal.mk ↑{x} = 1
-- Mathlib.Data.Int.ModEq
Int.ModEq.sub_right : ∀ {n a b : ℤ} (c : ℤ), a ≡ b [ZMOD n] → a - c ≡ b - c [ZMOD n]
-- Mathlib.RepresentationTheory.Intertwining
/-- A bijective intertwining map is an equivalence of representations.  -/
Representation.IntertwiningMap.ofBijective : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : CommSemiring A] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommMonoid W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] →
                    {ρ : Representation A G V} →
                      {σ : Representation A G W} → (f : ρ.IntertwiningMap σ) → Function.Bijective ⇑f → ρ.Equiv σ
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.slash_action_eqn : ∀ {F : Type u_1} {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [inst : FunLike F UpperHalfPlane ℂ]
  [SlashInvariantFormClass F Γ k] (f : F), ∀ γ ∈ Γ, SlashAction.map k γ ⇑f = ⇑f
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `Submodule.projectionOnto_apply_right`. -/
Submodule.linearProjOfIsCompl_apply_right : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (h : IsCompl p q) (x : ↥q), (p.projectionOnto q h) ↑x = 0
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.rightFraction_fac_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [inst_1 : W.HasRightCalculusOfFractions] {X Y : C} (φ : W.LeftFraction X Y) {Z : C} (h : φ.Y' ⟶ Z),
  CategoryTheory.CategoryStruct.comp φ.rightFraction.s (CategoryTheory.CategoryStruct.comp φ.f h) =
    CategoryTheory.CategoryStruct.comp φ.rightFraction.f (CategoryTheory.CategoryStruct.comp φ.s h)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
lt_neg : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b : α} [AddRightStrictMono α],
  a < -b ↔ b < -a
-- Mathlib.Order.Max
noTopOrder_iff_noMaxOrder : ∀ (α : Type u_3) [inst : LinearOrder α], NoTopOrder α ↔ NoMaxOrder α
-- Mathlib.Tactic.FunProp.Decl
/-- Discrimination tree for function properties.  -/
Mathlib.Meta.FunProp.FunPropDecls : Type
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.encodeSigma.match_1.eq_1 : ∀ (n : ℕ) (f : Fin (n + 1) → ℕ) (motive : Fin (Fin.sum fun x => f x.succ) → Sort u_1) (k : ℕ)
  (hk : k < Fin.sum fun x => f x.succ) (h_1 : (k : ℕ) → (hk : k < Fin.sum fun x => f x.succ) → motive ⟨k, hk⟩),
  (match ⟨k, hk⟩ with
    | ⟨k, hk⟩ => h_1 k hk) =
    h_1 k hk
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.instTopologicalSpaceUnitClosedDisc : TopologicalSpace Complex.UnitClosedDisc
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.intCast_mem : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K) (n : ℤ), ↑n ∈ s
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.IterM.fold_filterMapWithPostcondition : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {ps : Std.Do.PostShape} {n : Type w → Type w''} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Monad n] [LawfulMonad n]
  [inst_6 : Std.Do.WPMonad n ps] [inst_7 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n]
  [inst_9 : MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → Std.Iterators.PostconditionT n (Option γ)} {g : δ → γ → δ}
  {init : δ} {it : Std.IterM m β} {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps},
  ⦃P⦄
      Std.IterM.foldM
        (fun d b => do
          let __x ← (f b).run
          match __x with
            | some c => pure (g d c)
            | x => pure d)
        init it ⦃Q⦄ →
    ⦃P⦄ Std.IterM.fold g init (Std.IterM.filterMapWithPostcondition f it) ⦃Q⦄
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.prodMk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] [inst_1 : NormedAddCommGroup γ] {f : α → β} {g : α → γ},
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable g μ → MeasureTheory.Integrable (fun x => (f x, g x)) μ
-- Mathlib.Algebra.Group.Action.Defs
AddSemiconjBy.vadd_right_iff : ∀ {G : Type u_3} {H : Type u_4} [inst : AddGroup G] [inst_1 : Add H] [inst_2 : AddAction G H] [VAddCommClass G H H]
  [VAddAssocClass G H H] {a b x : H} {r : G}, AddSemiconjBy x (r +ᵥ a) (r +ᵥ b) ↔ AddSemiconjBy x a b
-- Lean.Data.KVMap
Lean.KVMap.getInt : Lean.KVMap → Lean.Name → optParam ℤ 0 → ℤ
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.lcm.eq_1 : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (s : Multiset α),
  s.lcm = Multiset.fold lcm 1 s
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.coeff_X_zero : ∀ {R : Type u_1} [inst : Semiring R], SkewPolynomial.X.coeff 0 = 0
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- The trailing coefficient of the inverse function is the inverse of the trailing coefficient.
 -/
meromorphicTrailingCoeffAt_fun_inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {f : 𝕜 → 𝕜},
  meromorphicTrailingCoeffAt (fun z => (f z)⁻¹) x = (meromorphicTrailingCoeffAt f x)⁻¹
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
/-- The bijection `X.N ≃ Y.N` on nondegenerate simplices of simplicial sets
that is induced by an isomorphism `X ≅ Y`.  -/
SSet.N.orderIsoOfIso : {X Y : SSet} → (X ≅ Y) → X.N ≃o Y.N
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.hasNext_cons_addChar : ∀ (c : Char) (cs : List Char) (i : String.Pos.Raw),
  { s := String.ofList (c :: cs), i := i + c }.hasNext = { s := String.ofList cs, i := i }.hasNext
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyGE.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k k_1 : α) (e_k : k = k_1)
  (t t_1 : Std.DTreeMap.Internal.Impl α β) (e_t : t = t_1) (ho : t.Ordered) (he : ∃ a ∈ t, (compare a k).isGE = true),
  Std.DTreeMap.Internal.Impl.getKeyGE k t ho he = Std.DTreeMap.Internal.Impl.getKeyGE k_1 t_1 ⋯ ⋯
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.toOuterMeasure_toMeasure : ∀ {α : Type u_1} [ms : MeasurableSpace α] {μ : MeasureTheory.Measure α}, μ.toMeasure ⋯ = μ
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- A `c : Bicone F` is:
* an object `c.pt` and
* morphisms `π j : pt ⟶ F j` and `ι j : F j ⟶ pt` for each `j`,
* such that `ι j ≫ π j'` is the identity when `j = j'` and zero otherwise.
 -/
CategoryTheory.Limits.Bicone.ι_π : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (self : CategoryTheory.Limits.Bicone F) (j j' : J),
  CategoryTheory.CategoryStruct.comp (self.ι j) (self.π j') = if h : j = j' then CategoryTheory.eqToHom ⋯ else 0
-- Mathlib.Topology.Compactness.Compact
IsCompact.image_of_continuousOn : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {f : X → Y},
  IsCompact s → ContinuousOn f s → IsCompact (f '' s)
-- Mathlib.Order.Directed
Directed.extend_bot : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : Preorder α] [inst_1 : OrderBot α] {e : ι → β} {f : ι → α},
  Directed (fun x1 x2 => x1 ≤ x2) f → Function.Injective e → Directed (fun x1 x2 => x1 ≤ x2) (Function.extend e f ⊥)
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.map_normalize : ∀ {R : Type u} {S : Type v} [inst : Field R] (p : Polynomial R) [inst_1 : DecidableEq R] [inst_2 : Field S]
  [inst_3 : DecidableEq S] (f : R →+* S), Polynomial.map f (normalize p) = normalize (Polynomial.map f p)
-- Std.Time.Format.Modifier
/-- Short form of zone name (e.g., "PST")
 -/
Std.Time.ZoneName.short : Std.Time.ZoneName
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
right_lt_lineMap_iff_one_lt : ∀ {k : Type u_1} {E : Type u_2} [inst : Ring k] [inst_1 : LinearOrder k] [IsStrictOrderedRing k]
  [inst_3 : AddCommGroup E] [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E]
  [IsStrictOrderedModule k E] {a b : E} {r : k}, a < b → (b < (AffineMap.lineMap a b) r ↔ 1 < r)
-- Mathlib.Order.BoundedOrder.Basic
isBot_iff_eq_bot : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, IsBot a ↔ a = ⊥
-- Mathlib.NumberTheory.DiophantineApproximation.Basic
/-- Given any rational approximation `q` to the irrational real number `ξ`, there is
a good rational approximation `q'` such that `|ξ - q'| < |ξ - q|`.  -/
Real.exists_rat_abs_sub_lt_and_lt_of_irrational : ∀ {ξ : ℝ}, Irrational ξ → ∀ (q : ℚ), ∃ q', |ξ - ↑q'| < 1 / ↑q'.den ^ 2 ∧ |ξ - ↑q'| < |ξ - ↑q|
-- Mathlib.RingTheory.Length
Module.length_le_of_injective : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : N →ₗ[R] M),
  Function.Injective ⇑f → Module.length R N ≤ Module.length R M
-- Mathlib.Data.Set.Image
Set.preimage_empty : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, f ⁻¹' ∅ = ∅
-- Mathlib.Tactic.Sat.FromLRAT
/-- An addition step, with the clause ID, the clause literal list, and the proof trace  -/
Mathlib.Tactic.Sat.LRATStep.add : ℕ → Array ℤ → Array ℤ → Mathlib.Tactic.Sat.LRATStep
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.zmodEquivZPowers_symm_apply_zpow : ∀ {R : Type u_4} {k : ℕ} [inst : CommRing R] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) (i : ℤ),
  h.zmodEquivZPowers.symm (Additive.ofMul ⟨ζ ^ i, ⋯⟩) = ↑i
-- Mathlib.Topology.Algebra.Ring.Ideal
QuotientRing.isOpenMap_coe : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : CommRing R] (N : Ideal R) [IsTopologicalRing R],
  IsOpenMap ⇑(Ideal.Quotient.mk N)
-- Init.Data.Int.DivMod.Lemmas
Int.add_fdiv_of_dvd_left : ∀ {a b c : ℤ}, c ∣ a → (a + b).fdiv c = a.fdiv c + b.fdiv c
-- Mathlib.Logic.Basic
Prop.exists_iff : ∀ {p : Prop → Prop}, (∃ h, p h) ↔ p False ∨ p True
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.prod_map_eq_pow_single : ∀ {ι : Type u_2} {M : Type u_5} [inst : CommMonoid M] {m : Multiset ι} {f : ι → M} [inst_1 : DecidableEq ι] (i : ι),
  (∀ (i' : ι), i' ≠ i → i' ∈ m → f i' = 1) → (Multiset.map f m).prod = f i ^ Multiset.count i m
-- Batteries.Data.List.Interleave
List.Perm.interleave : ∀ {α : Type u_1} {l₁ l₃ l₂ l₄ : List α}, l₁.Perm l₃ → l₂.Perm l₄ → (l₁.interleave l₂).Perm (l₃.interleave l₄)
-- Mathlib.Analysis.Analytic.Order
/-- The order of a sum is at least the minimum of the orders of the summands.  -/
le_analyticOrderAt_add : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f g : 𝕜 → E} {z₀ : 𝕜},
  min (analyticOrderAt f z₀) (analyticOrderAt g z₀) ≤ analyticOrderAt (f + g) z₀
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.congr_one : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N],
  TensorProduct.AlgebraTensorModule.congr 1 1 = 1
-- Mathlib.Order.Category.BddDistLat
BddDistLat.ext : ∀ {X Y : BddDistLat} {f g : X ⟶ Y},
  (∀ (x : ↑X.toDistLat), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) → f = g
-- Lean.Elab.InfoTree.Types
Lean.Elab.instReprDocElabKind.repr : Lean.Elab.DocElabKind → ℕ → Std.Format
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.stabilizer_empty : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α], AddAction.stabilizer G ∅ = ⊤
-- Mathlib.Lean.FoldEnvironment
/-- Fold through all imported constants using `act`.
This uses parallelism, with each thread independently folding over a subset of modules.
The array of tasks is returned, so this function typically returns before all tasks have finished.
The results can then be combined using `Array.foldl`.  -/
Lean.Meta.foldImportedDecls : {α : Type} →
  α →
    Lean.Meta.Config →
      (α → Lean.Name → Lean.ConstantInfo → Lean.MetaM α) →
        optParam ℕ 5000 → Lean.CoreM (Array (Task (Except Lean.Exception α)) × Lean.Meta.FoldDeclErrorRef)
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
inf_eq_bot_of_bot_mem : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderInf α] {s : Set α} [inst_1 : OrderBot α], ⊥ ∈ s → sInf s = ⊥
-- Mathlib.Logic.Nonempty
Classical.nonempty_pi : ∀ {ι : Sort u_4} {α : ι → Sort u_3}, Nonempty ((i : ι) → α i) ↔ ∀ (i : ι), Nonempty (α i)
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The sum of two `C^n` functions within a set at a point is `C^n` within this set
at this point.  -/
ContDiffWithinAt.add : ∀ {𝕜 : 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] {x : E}
  {n : WithTop ℕ∞} {s : Set E} {f g : E → F},
  ContDiffWithinAt 𝕜 n f s x → ContDiffWithinAt 𝕜 n g s x → ContDiffWithinAt 𝕜 n (fun x => f x + g x) s x
-- Mathlib.Combinatorics.Additive.Convolution
Finset.convolution_op_smul_eq_convolution_mul_inv : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (A B : Finset G) (s x : G),
  A.convolution (MulOpposite.op s • B) x = A.convolution B (x * s⁻¹)
-- Init.Data.Int.DivMod.Lemmas
Int.mul_dvd_mul_iff_right : ∀ {a b c : ℤ}, a ≠ 0 → (b * a ∣ c * a ↔ b ∣ c)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.tan_lt_tan_of_nonneg_of_lt_pi_div_two : ∀ {x y : ℝ}, 0 ≤ x → y < Real.pi / 2 → x < y → Real.tan x < Real.tan y
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.splits_mul : ∀ {R : Type u_1} [inst : CommRing R] {f g : Polynomial R} [IsDomain R],
  f ≠ 0 → g ≠ 0 → ((f * g).Splits ↔ f.Splits ∧ g.Splits)
-- Mathlib.Algebra.Ring.Parity
Nat.even_add' : ∀ {m n : ℕ}, Even (m + n) ↔ (Odd m ↔ Odd n)
-- Mathlib.RingTheory.OreLocalization.Basic
OreLocalization.instDistribMulActionOfIsScalarTower : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {X : Type u_2} →
          [inst_2 : AddMonoid X] →
            [inst_3 : DistribMulAction R X] →
              {R₀ : Type u_3} →
                [inst_4 : Monoid R₀] →
                  [inst_5 : MulAction R₀ X] →
                    [inst_6 : MulAction R₀ R] →
                      [IsScalarTower R₀ R X] → [IsScalarTower R₀ R R] → DistribMulAction R₀ (OreLocalization S X)
-- Init.Data.SInt.Lemmas
Int16.zero_sub : ∀ (a : Int16), 0 - a = -a
-- Mathlib.Logic.Function.Conjugate
Function.Semiconj₂.id_left : ∀ {α : Type u_1} (op : α → α → α), Function.Semiconj₂ id op op
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
CategoryTheory.PreOneHypercover.cylinder_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} [inst_1 : CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F)
  (p : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)),
  (CategoryTheory.PreOneHypercover.cylinder f g).f p = CategoryTheory.PreOneHypercover.cylinderf f g p.snd
-- Mathlib.Algebra.Category.Grp.ForgetCorepresentable
AddGrpCat.forget_isCorepresentable : (CategoryTheory.forget AddGrpCat).IsCorepresentable
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.naturality : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U U' : Y.Opens} (i : Opposite.op U' ⟶ Opposite.op U),
  CategoryTheory.CategoryStruct.comp (Y.presheaf.map i) (AlgebraicGeometry.Scheme.Hom.app f U) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f U')
      (X.presheaf.map ((TopologicalSpace.Opens.map f.base).map i.unop).op)
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
/-- If `F ⋙ G` preserves finite colimits and `G` reflects finite colimits, then `F` preserves finite
colimits.
 -/
CategoryTheory.Limits.preservesFiniteColimits_of_reflects_of_preserves : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesFiniteColimits (F.comp G)]
  [CategoryTheory.Limits.ReflectsFiniteColimits G], CategoryTheory.Limits.PreservesFiniteColimits F
-- Lean.Data.NameMap.Basic
Lean.NameSet.contains : Lean.NameSet → Lean.Name → Bool
-- Init.Data.String.Iterate
String.Slice.RevByteIterator : Type
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKeyD_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {fallback : α}, t.maxKeyD fallback ∈ t
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.ext_ring : ∀ {R : Type u_10} [inst : Semiring R] {S : Type u_11} [inst_1 : Semiring S] {N' : Type u_13} [inst_2 : AddMonoid N']
  [inst_3 : DistribMulAction S N'] {σ : R →* S} {f g : R →ₑ+[σ] N'}, f 1 = g 1 → f = g
-- Mathlib.Algebra.Lie.Weights.Killing
/-- The contrapositive of this result is very useful, taking `x` to be the element of `H`
corresponding to a root `α` under the identification between `H` and `H^*` provided by the Killing
form.  -/
LieAlgebra.IsKilling.eq_zero_of_apply_eq_zero_of_mem_corootSpace : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L]
  [LieModule.IsTriangularizable K (↥H) L] [CharZero K] (x : ↥H) (α : ↥H → K),
  α x = 0 → x ∈ LieAlgebra.corootSpace α → x = 0
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int64.reduceMod : Lean.Meta.Simp.DSimproc
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.Δ_integral_of_isIntegral : ∀ (R : Type u_1) [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] (W : WeierstrassCurve K)
  [WeierstrassCurve.IsIntegral R W], ∃ r, (algebraMap R K) r = W.Δ
-- Mathlib.Combinatorics.Derangements.Finite
card_derangements_invariant : ∀ {α : Type u_2} {β : Type u_3} [inst : Fintype α] [inst_1 : DecidableEq α] [inst_2 : Fintype β]
  [inst_3 : DecidableEq β],
  Fintype.card α = Fintype.card β → Fintype.card ↑(derangements α) = Fintype.card ↑(derangements β)