mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.setLIntegral_piecewise : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ η : ProbabilityTheory.Kernel α β}
  {s : Set α} {hs : MeasurableSet s} [inst : DecidablePred fun x => x ∈ s] (a : α) (g : β → ENNReal) (t : Set β),
  ∫⁻ (b : β) in t, g b ∂(ProbabilityTheory.Kernel.piecewise hs κ η) a =
    if a ∈ s then ∫⁻ (b : β) in t, g b ∂κ a else ∫⁻ (b : β) in t, g b ∂η a
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
ContinuousLinearEquiv.rightInverse_hasRightInverse : ∀ {R : Type u_1} [inst : Semiring R] {E : Type u_2} {F : Type u_4} [inst_1 : TopologicalSpace E]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : TopologicalSpace F] [inst_5 : AddCommMonoid F]
  [inst_6 : Module R F] (f : E ≃L[R] F), ⋯.rightInverse = ↑f.symm
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_uIcc_cast : ∀ {M : Type u_2} [inst : CommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a b : Fin n),
  ∏ i ∈ Finset.uIcc (Fin.cast h a) (Fin.cast h b), f i = ∏ i ∈ Finset.uIcc a b, f (Fin.cast h i)
-- Lean.Meta.Eval
Lean.Meta.evalExpr' : (α : Type) →
  Lean.Name → Lean.Expr → optParam Lean.DefinitionSafety Lean.DefinitionSafety.safe → optParam Bool true → Lean.MetaM α
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_hom_desc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {r s t : CategoryTheory.Limits.Cocone F} (P : CategoryTheory.Limits.IsColimit s)
  (Q : CategoryTheory.Limits.IsColimit t),
  CategoryTheory.CategoryStruct.comp (P.coconePointUniqueUpToIso Q).hom (Q.desc r) = P.desc r
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicOn.inv_iff : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {s : 𝕜 → 𝕜'} {U : Set 𝕜}, MeromorphicOn s⁻¹ U ↔ MeromorphicOn s U
-- Mathlib.Data.Seq.Basic
/-- Map a function on a `Seq1`  -/
Stream'.Seq1.map : {α : Type u} → {β : Type v} → (α → β) → Stream'.Seq1 α → Stream'.Seq1 β
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.Iso.hom_inv_id_app_apply : ∀ {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} (α : F ≅ G) (X : C) {F_1 : D → D → Type uF} {carrier : D → Type w}
  {instFunLike : (X Y : D) → FunLike (F_1 X Y) (carrier X) (carrier Y)} [inst_2 : CategoryTheory.ConcreteCategory D F_1]
  (x : carrier (F.obj X)),
  (CategoryTheory.ConcreteCategory.hom (α.inv.app X)) ((CategoryTheory.ConcreteCategory.hom (α.hom.app X)) x) = x
-- Mathlib.Algebra.GroupWithZero.Defs
mul_div_cancel_right₀ : ∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] [inst_1 : Div M₀] [MulDivCancelClass M₀] (a : M₀) {b : M₀},
  b ≠ 0 → a * b / b = a
-- Mathlib.Algebra.EuclideanDomain.Defs
EuclideanDomain.xgcdAux_rec : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] {r s t r' s' t' : R},
  r ≠ 0 →
    EuclideanDomain.xgcdAux r s t r' s' t' = EuclideanDomain.xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t
-- Lean.Data.Options
Lean.Option.Decl.mk.injEq : ∀ {α : Type} (defValue : α) (descr : String) (deprecation? : Option Lean.OptionDeprecation) (defValue_1 : α)
  (descr_1 : String) (deprecation?_1 : Option Lean.OptionDeprecation),
  ({ defValue := defValue, descr := descr, deprecation? := deprecation? } =
      { defValue := defValue_1, descr := descr_1, deprecation? := deprecation?_1 }) =
    (defValue = defValue_1 ∧ descr = descr_1 ∧ deprecation? = deprecation?_1)
-- Mathlib.CategoryTheory.Elements
/-- The category structure on `F.Elements`, for `F : C ⥤ Type`.
A morphism `(X, x) ⟶ (Y, y)` is a morphism `f : X ⟶ Y` in `C`, so `F.map f` takes `x` to `y`.  -/
CategoryTheory.categoryOfElements : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor C (Type w)) → CategoryTheory.Category.{v, max u w} F.Elements
-- Mathlib.Topology.Filter
Filter.monotone_nhds : ∀ {α : Type u_2}, Monotone nhds
-- Mathlib.Order.Filter.ENNReal
NNReal.isBoundedUnder_ge_toReal : ∀ {ι : Type u_1} {f : Filter ι} {u : ι → NNReal},
  (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f fun i => ↑(u i)) ↔ Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u
-- Mathlib.Data.ENNReal.Inv
ENNReal.mul_lt_of_lt_div' : ∀ {a b c : ENNReal}, a < b / c → c * a < b
-- Init.Grind.AC
Lean.Grind.AC.Seq.sort_k_eq_sort : ∀ (s : Lean.Grind.AC.Seq), s.sort_k = s.sort
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.addConst.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] (A B : Finset G), A.addConst B = ↑(A + B).card / ↑A.card
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `MeromorphicOn.meromorphicOn_comp_add_const_iff_meromorphicOn`

---

`MeromorphicOn` is invariant under translation.  -/
MeromorphicOn.meromorphicOn_fun_comp_add_const_iff_meromorphicOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {c : 𝕜} {U : Set 𝕜},
  MeromorphicOn (fun x => f (x + c)) U ↔ MeromorphicOn f (U + {c})
-- Mathlib.NumberTheory.Multiplicity
padicValNat.pow_add_pow : ∀ {x y p : ℕ} [hp : Fact (Nat.Prime p)],
  Odd p →
    p ∣ x + y → ¬p ∣ x → ∀ {n : ℕ}, Odd n → padicValNat p (x ^ n + y ^ n) = padicValNat p (x + y) + padicValNat p n
-- Mathlib.Algebra.Lie.CartanExists
LieAlgebra.engel_isBot_of_isMin.lieCharpoly_coeff_natDegree : ∀ (R : Type u_2) {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : Module.Finite R L] [inst_8 : Module.Free R L] [inst_9 : Module.Finite R M] [inst_10 : Module.Free R M]
  (x y : L) [Nontrivial R] (i j : ℕ),
  i + j = Module.finrank R M → ((LieAlgebra.engel_isBot_of_isMin.lieCharpoly✝ R M x y).coeff i).natDegree ≤ j
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.mk_of_mem : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] {s : Finset ι}
  {x : (i : ↑↑s) → β ↑i} {i : ι} (hi : i ∈ s), (DFinsupp.mk s x) i = x ⟨i, hi⟩
-- Mathlib.Algebra.Group.Defs
AddZeroClass.mk : {M : Type u} → [toAddZero : AddZero M] → (∀ (a : M), 0 + a = a) → (∀ (a : M), a + 0 = a) → AddZeroClass M
-- Init.Data.UInt.Lemmas
UInt8.toUInt64_le : ∀ {a b : UInt8}, a.toUInt64 ≤ b.toUInt64 ↔ a ≤ b
-- Mathlib.NumberTheory.MulChar.Basic
/-- Composition with a ring homomorphism preserves the property of being a quadratic character.  -/
MulChar.IsQuadratic.comp : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommRing R'] {R'' : Type u_3} [inst_2 : CommRing R'']
  {χ : MulChar R R'}, χ.IsQuadratic → ∀ (f : R' →+* R''), (χ.ringHomComp f).IsQuadratic
-- Mathlib.GroupTheory.Index
AddSubgroup.index_ker : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (f : G →+ G'),
  f.ker.index = Nat.card ↥f.range
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.normalize.congr_simp : ∀ {α : Type u_1} (f f_1 : α → ENNReal) (e_f : f = f_1) (hf0 : tsum f ≠ 0) (hf : tsum f ≠ ⊤),
  PMF.normalize f hf0 hf = PMF.normalize f_1 ⋯ ⋯
-- Mathlib.Combinatorics.SimpleGraph.IncMatrix
/-- Entries of the incidence matrix can be computed given additional decidable instances.  -/
SimpleGraph.incMatrix_apply' : ∀ {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [inst : Zero R] [inst_1 : One R] [inst_2 : DecidableEq α]
  [inst_3 : DecidableRel G.Adj] {a : α} {e : Sym2 α},
  SimpleGraph.incMatrix R G a e = if e ∈ G.incidenceSet a then 1 else 0
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.toCycles_comp_isoCycles₁_hom_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : (Fin 2 → G) →₀ ↑A),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.isoCycles₁ A).hom)
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.toCycles A 2 1)) x) =
    (groupHomology.shortComplexH1 A).moduleCatToCycles
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.chainsIso₂ A).hom) x)
-- Mathlib.Topology.JacobsonSpace
JacobsonSpace.closure_inter_closedPoints : ∀ {X : Type u_1} {inst : TopologicalSpace X} [self : JacobsonSpace X] {Z : Set X},
  IsClosed Z → closure (Z ∩ closedPoints X) = Z
-- Mathlib.Order.RelClasses
/-- Set notation form of `LE.le.lt_of_not_ge` -/
LE.le.ssubset_of_not_superset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b : α}, a ⊆ b → ¬b ⊆ a → a ⊂ b
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
/-- A congruence subgroup is a subgroup of `SL(2, ℤ)` which contains some `Gamma N` for some
`N ≠ 0`.  -/
CongruenceSubgroup.IsCongruenceSubgroup : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ) → Prop
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
/-- The embedding of Lp simple functions into Lp functions, as a continuous linear map.  -/
MeasureTheory.Lp.simpleFunc.coeToLp : (α : Type u_1) →
  (E : Type u_4) →
    (𝕜 : Type u_6) →
      [inst : MeasurableSpace α] →
        [inst_1 : NormedAddCommGroup E] →
          {p : ENNReal} →
            {μ : MeasureTheory.Measure α} →
              [inst_2 : Fact (1 ≤ p)] →
                [inst_3 : NormedRing 𝕜] →
                  [inst_4 : Module 𝕜 E] →
                    [inst_5 : IsBoundedSMul 𝕜 E] → ↥(MeasureTheory.Lp.simpleFunc E p μ) →L[𝕜] ↥(MeasureTheory.Lp E p μ)
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctor.map₂Iso_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.PrelaxFunctor B C) {a b : B} {f g : a ⟶ b} (η : f ≅ g), (F.map₂Iso η).hom = F.map₂ η.hom
-- Mathlib.Order.BooleanAlgebra.Set
Set.ite_univ : ∀ {α : Type u_1} (s s' : Set α), Set.univ.ite s s' = s
-- Mathlib.Probability.Kernel.Deterministic
ProbabilityTheory.Kernel.instIsDeterministicPUnitDiscard : ∀ {α : Type u_1} {mα : MeasurableSpace α}, ProbabilityTheory.IsDeterministic (ProbabilityTheory.Kernel.discard α)
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.card_support_swap : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {x y : α}, x ≠ y → (Equiv.swap x y).support.card = 2
-- Mathlib.Algebra.Algebra.Operations
Submodule.le_pow_toAddSubmonoid : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (M : Submodule R A) {n : ℕ}, M.toAddSubmonoid ^ n ≤ (M ^ n).toAddSubmonoid
-- Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
CategoryTheory.instPreservesFiniteProductsOppositeObjFunctorIsSheafExtensiveTopology : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.FinitaryPreExtensive C]
  [CategoryTheory.FinitaryExtensive C] (F : CategoryTheory.Sheaf (CategoryTheory.extensiveTopology C) D),
  CategoryTheory.Limits.PreservesFiniteProducts F.obj
-- Lean.ToExpr
Lean.instToExprInt16.mkNat : ℕ → Lean.Expr
-- Mathlib.Tactic.LinearCombinationPrime
Mathlib.Tactic.LinearCombinationPrime.mul_pf : ∀ {α : Type u_1} {a₁ a₂ b₁ b₂ : α} [inst : Mul α], a₁ = b₁ → a₂ = b₂ → a₁ * a₂ = b₁ * b₂
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.map_comp_map' : ∀ {β : Type w} {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : α → C} {h : β → C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct f] [inst_2 : CategoryTheory.Limits.HasCoproduct g]
  [inst_3 : CategoryTheory.Limits.HasCoproduct h] (p : α → β) (q : (a : α) → f a ⟶ g a) (q' : (a : α) → g a ⟶ h (p a)),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.map q) (CategoryTheory.Limits.Sigma.map' p q') =
    CategoryTheory.Limits.Sigma.map' p fun a => CategoryTheory.CategoryStruct.comp (q a) (q' a)
-- Mathlib.LinearAlgebra.Matrix.Circulant
/-- `k • circulant v` is another circulant matrix `circulant (k • v)`.  -/
Matrix.circulant_smul : ∀ {α : Type u_1} {n : Type u_3} {R : Type u_4} [inst : Sub n] [inst_1 : SMul R α] (k : R) (v : n → α),
  Matrix.circulant (k • v) = k • Matrix.circulant v
-- Mathlib.Order.Filter.IsBounded
isBoundedUnder_le_finset_sup' : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : LinearOrder β] [Nonempty β] {f : Filter α} {F : ι → α → β}
  {s : Finset ι} (hs : s.Nonempty),
  (∀ i ∈ s, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) →
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => s.sup' hs fun i => F i a
-- Init.Data.List.TakeDrop
_private.Init.Data.List.TakeDrop.0.List.filter.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Mathlib.RingTheory.FractionalIdeal.Inverse
FractionalIdeal.invertible_of_principal : ∀ (K : Type u_3) [inst : Field K] {R₁ : Type u_4} [inst_1 : CommRing R₁] [inst_2 : IsDomain R₁] [inst_3 : Algebra R₁ K]
  [inst_4 : IsFractionRing R₁ K] (I : FractionalIdeal (nonZeroDivisors R₁) K) [(↑I).IsPrincipal], I ≠ 0 → I * I⁻¹ = 1
-- Lean.Compiler.IR.Basic
Lean.IR.LocalContext.getJPBody : Lean.IR.LocalContext → Lean.IR.JoinPointId → Option Lean.IR.FnBody
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.pred_eval : ∀ (v : List ℕ), Turing.ToPartrec.Code.pred.eval v = pure [v.headI.pred]
-- Mathlib.RingTheory.Coalgebra.GroupLike
GroupLike.isGroupLikeElem_val : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] (self : GroupLike R A), IsGroupLikeElem R ↑self
-- Mathlib.Analysis.Calculus.LHopital
/-- L'Hôpital's rule for approaching a real from the left, `HasDerivAt` version  -/
HasDerivAt.lhopital_zero_nhdsLT : ∀ {a : ℝ} {l : Filter ℝ} {f f' g g' : ℝ → ℝ},
  (∀ᶠ (x : ℝ) in nhdsWithin a (Set.Iio a), HasDerivAt f (f' x) x) →
    (∀ᶠ (x : ℝ) in nhdsWithin a (Set.Iio a), HasDerivAt g (g' x) x) →
      (∀ᶠ (x : ℝ) in nhdsWithin a (Set.Iio a), g' x ≠ 0) →
        Filter.Tendsto f (nhdsWithin a (Set.Iio a)) (nhds 0) →
          Filter.Tendsto g (nhdsWithin a (Set.Iio a)) (nhds 0) →
            Filter.Tendsto (fun x => f' x / g' x) (nhdsWithin a (Set.Iio a)) l →
              Filter.Tendsto (fun x => f x / g x) (nhdsWithin a (Set.Iio a)) l
-- Mathlib.Logic.Encodable.Basic
Encodable.encode_ofEquiv : ∀ {α : Type u_3} {β : Type u_4} [inst : Encodable α] (e : β ≃ α) (b : β), Encodable.encode b = Encodable.encode (e b)
-- Lean.Exception
/-- Macro for throwing error exceptions. The argument can be an interpolated string.
It is a convenient way of building `MessageData` objects.
The result of `getRef` is used as position information.
Recall that `getRef` returns the current "reference" syntax.
 -/
Lean.termThrowError__ : Lean.ParserDescr
-- Lean.Meta.Tactic.Rfl
/-- Convert a goal of the form `x ~ y` into the form `x = y`, where `~` is a reflexive
relation, that is, a relation which has a reflexive lemma tagged with the attribute `@[refl]`.
If this can't be done, returns the original `MVarId`.
 -/
Lean.MVarId.liftReflToEq : Lean.MVarId → Lean.MetaM Lean.MVarId
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.card_singleton_add : ∀ {α : Type u_2} [inst : Add α] [IsLeftCancelAdd α] [inst_2 : DecidableEq α] (a : α) (t : Finset α),
  ({a} + t).card = t.card
-- Mathlib.Data.Set.Lattice
Set.iInter_ge_eq_iInter_nat_add : ∀ {α : Type u_1} (u : ℕ → Set α) (n : ℕ), ⋂ i, ⋂ (_ : i ≥ n), u i = ⋂ i, u (i + n)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
PseudoMetricSpace.dist_comm : ∀ {α : Type u} [self : PseudoMetricSpace α] (x y : α), dist x y = dist y x
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.UnifyM.State.mk.injEq : ∀ (eAssignment : Array (Option Lean.Expr)) (uAssignment : Array (Option Lean.Level))
  (ePending : Array (Lean.Expr × Lean.Expr)) (uPending : Array (Lean.Level × Lean.Level))
  (iPending : Array (Lean.Expr × Lean.Expr)) (tPending : Array ℕ) (us : List Lean.Level) (args : Array Lean.Expr)
  (eAssignment_1 : Array (Option Lean.Expr)) (uAssignment_1 : Array (Option Lean.Level))
  (ePending_1 : Array (Lean.Expr × Lean.Expr)) (uPending_1 : Array (Lean.Level × Lean.Level))
  (iPending_1 : Array (Lean.Expr × Lean.Expr)) (tPending_1 : Array ℕ) (us_1 : List Lean.Level)
  (args_1 : Array Lean.Expr),
  ({ eAssignment := eAssignment, uAssignment := uAssignment, ePending := ePending, uPending := uPending,
        iPending := iPending, tPending := tPending, us := us, args := args } =
      { eAssignment := eAssignment_1, uAssignment := uAssignment_1, ePending := ePending_1, uPending := uPending_1,
        iPending := iPending_1, tPending := tPending_1, us := us_1, args := args_1 }) =
    (eAssignment = eAssignment_1 ∧
      uAssignment = uAssignment_1 ∧
        ePending = ePending_1 ∧
          uPending = uPending_1 ∧ iPending = iPending_1 ∧ tPending = tPending_1 ∧ us = us_1 ∧ args = args_1)
-- Mathlib.Data.Set.Restrict
/-- **Alias** of `Set.domRestrict_extend_compl_range`. -/
Set.restrict_extend_compl_range : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : α → γ) (g' : β → γ),
  (Set.range f)ᶜ.domRestrict (Function.extend f g g') = g' ∘ Subtype.val
-- Mathlib.Order.Filter.Pointwise
/-- `Filter α` is an `AddMonoid` under pointwise operations if `α` is.  -/
Filter.addMonoid : {α : Type u_2} → [AddMonoid α] → AddMonoid (Filter α)
-- Lean.Elab.MutualDef
Lean.Elab.Term.warn.classDefReducibility : Lean.Option Bool
-- Mathlib.Algebra.Divisibility.Units
IsRelPrime.isUnit_of_dvd : ∀ {α : Type u_1} [inst : CommMonoid α] {x y : α}, IsRelPrime x y → x ∣ y → IsUnit x
-- Mathlib.Tactic.Translate.Reorder
/-- Return the reorder that reverses the action of the given reorder.  -/
Mathlib.Tactic.Translate.Reorder.reverse : Mathlib.Tactic.Translate.Reorder → Mathlib.Tactic.Translate.Reorder
-- Init.Grind.Interactive
Lean.Parser.Tactic.Grind.«grind_filterGen!=_» : Lean.ParserDescr
-- Init.Omega.Constraint
/-- The value of the new variable introduced when solving a hard equality.  -/
Lean.Omega.bmod_div_term : ℕ → Lean.Omega.Coeffs → Lean.Omega.Coeffs → ℤ
-- Mathlib.Order.CompactlyGenerated.Basic
/-- This property is sometimes referred to as `α` being upper continuous.  -/
DirectedOn.inf_sSup_eq : ∀ {α : Type u_2} [inst : CompleteLattice α] [IsCompactlyGenerated α] {a : α} {s : Set α},
  DirectedOn (fun x1 x2 => x1 ≤ x2) s → a ⊓ sSup s = ⨆ b ∈ s, a ⊓ b
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
/-- Given a diagram of presheafed spaces,
we can push all the presheaves forward to the colimit `X` of the underlying topological spaces,
obtaining a diagram in `(Presheaf C X)ᵒᵖ`.
 -/
AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit : {J : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J TopCat] →
          (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)) →
            CategoryTheory.Functor J
              (TopCat.Presheaf C
                  (CategoryTheory.Limits.colimit (F.comp (AlgebraicGeometry.PresheafedSpace.forget C))))ᵒᵖ
-- Std.Data.HashMap.Lemmas
Std.HashMap.fold_eq_foldl_toList : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {δ : Type w} {f : δ → α → β → δ}
  {init : δ}, Std.HashMap.fold f init m = List.foldl (fun a b => f a b.1 b.2) init m.toList
-- Mathlib.CategoryTheory.Adhesive.Basic
CategoryTheory.adhesive_functor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u''} [inst_1 : CategoryTheory.Category.{v'', u''} D]
  [CategoryTheory.Adhesive C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasPushouts C],
  CategoryTheory.Adhesive (CategoryTheory.Functor D C)
-- Init.Data.UInt.Bitwise
UInt8.not_ne_self : ∀ {a : UInt8}, ~~~a ≠ a
-- Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor_obj_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T}
  {R : CategoryTheory.Functor D T} {C' : Type u₄} [inst_3 : CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅}
  [inst_4 : CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T']
  {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'}
  {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F)
  (β : R.comp F ⟶ F₂.comp R') [inst_6 : CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R')
  (Y : CategoryTheory.StructuredArrow X (CategoryTheory.Comma.map α β)),
  ((CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor α β X).obj Y).hom =
    CategoryTheory.StructuredArrow.homMk Y.right.hom ⋯
-- Lean.Declaration
Lean.QuotKind.ind : Lean.QuotKind
-- Mathlib.CategoryTheory.Limits.Types.Products
/-- The category of types has `PUnit` as a terminal object.  -/
CategoryTheory.Limits.Types.terminalLimitCone : CategoryTheory.Limits.LimitCone (CategoryTheory.Functor.empty (Type u))
-- Std.Time.Format.Basic
/-- Classify a `PlainTime` into an `ExtendedDayPeriod` for the `B` pattern (CLDR flexible periods).  -/
Std.Time.classifyExtendedDayPeriod : Std.Time.Hour.Ordinal → Std.Time.Minute.Ordinal → Std.Time.Second.Ordinal true → Std.Time.ExtendedDayPeriod
-- Mathlib.RingTheory.Coalgebra.Basic
/-- `comul a` is equal to a finite sum of some pure tensors  -/
Coalgebra.Repr.eq : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : CoalgebraStruct R A] {a : A} {ι : Type u_1} (self : Coalgebra.Repr R a ι),
  ∑ i ∈ self.index, self.left i ⊗ₜ[R] self.right i = CoalgebraStruct.comul a
-- Mathlib.GroupTheory.Sylow
Sylow.smul_subtype : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {P : Sylow p G} {H : Subgroup G} (hP : ↑P ≤ H) (h : ↥H),
  h • P.subtype hP = (h • P).subtype ⋯
-- Mathlib.Topology.Algebra.Order.Archimedean
/-- An additive subgroup of an archimedean linear ordered additive commutative group `G`
with order topology either is dense in `G` or is a cyclic subgroup.  -/
AddSubgroup.dense_or_cyclic : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [inst_3 : TopologicalSpace G]
  [OrderTopology G] [Archimedean G] (S : AddSubgroup G), Dense ↑S ∨ ∃ a, S = AddSubgroup.closure {a}
-- Init.Data.Array.Basic
/-- Applies the monadic action `f` to every element in the array, along with the element's index, from
left to right. Returns the array of results.
 -/
Array.mapIdxM : {α : Type u} → {β : Type v} → {m : Type v → Type w} → [Monad m] → (ℕ → α → m β) → Array α → m (Array β)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.keys_perm_keys_of_equiv : ∀ {α : Type u} {β : α → Type v} (m₁ m₂ : Std.DHashMap.Raw α β), m₁.Equiv m₂ → m₁.keys.Perm m₂.keys
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearMap.fpowerSeriesBilinear.eq_4 : ∀ {𝕜 : 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] (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) (x_1 : ℕ),
  (x_1 = 0 → False) → (x_1 = 1 → False) → (x_1 = 2 → False) → f.fpowerSeriesBilinear x x_1 = 0
-- Mathlib.RingTheory.MvPowerSeries.Derivative
MvPowerSeries.pderiv_coe : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {i : σ} (f : MvPolynomial σ R),
  (MvPowerSeries.pderiv R i) ↑f = ↑((MvPolynomial.pderiv i) f)
-- Mathlib.GroupTheory.Divisible
/-- An additive group is `ℤ`-divisible if it is `ℕ`-divisible.  -/
AddGroup.divisibleByIntOfDivisibleByNat : (A : Type u_1) → [inst : AddGroup A] → [DivisibleBy A ℕ] → DivisibleBy A ℤ
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.apply_symm_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β) (y : β),
  e (e.symm y) = y