mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Algebra
/-- Continuous algebra homomorphisms between algebras. We only put the type classes that are
necessary for the definition, although in applications `M` and `B` will be topological algebras
over the topological ring `R`.  -/
ContinuousAlgHom : (R : Type u_3) →
  [inst : CommSemiring R] →
    (A : Type u_4) →
      [inst_1 : Semiring A] →
        [TopologicalSpace A] →
          (B : Type u_5) →
            [inst_3 : Semiring B] → [TopologicalSpace B] → [Algebra R A] → [Algebra R B] → Type (max u_4 u_5)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roo_succ_succ : ∀ {m n : ℕ}, ((m + 1)<...n + 1).toArray = Array.map (fun x => x + 1) (m<...n).toArray
-- Lean.Widget.TaggedText
_private.Lean.Widget.TaggedText.0.Lean.Widget.TaggedText.TaggedState.mk : Lean.Widget.TaggedText (ℕ × ℕ) → List (ℕ × ℕ × Lean.Widget.TaggedText (ℕ × ℕ)) → ℕ → Lean.Widget.TaggedText.TaggedState✝
-- Mathlib.Data.List.Pairwise
/-- **Alias** of the forward direction of `List.pairwise_reverse`. -/
List.Pairwise.of_reverse : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α}, List.Pairwise R l.reverse → List.Pairwise (fun a b => R b a) l
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instAdd.eq_1 : ∀ {α : Type u_1} [inst : Add α], Colex.instAdd = inst
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Expr.toPolyN.eq_def : ∀ (x : Lean.Grind.Linarith.Expr),
  x.toPolyN =
    match x with
    | a.sub b => Lean.Grind.Linarith.Poly.nil
    | a.neg => Lean.Grind.Linarith.Poly.nil
    | Lean.Grind.Linarith.Expr.intMul k a => Lean.Grind.Linarith.Poly.nil
    | Lean.Grind.Linarith.Expr.zero => Lean.Grind.Linarith.Poly.nil
    | Lean.Grind.Linarith.Expr.var v => Lean.Grind.Linarith.Poly.add 1 v Lean.Grind.Linarith.Poly.nil
    | a.add b => a.toPolyN.combine b.toPolyN
    | Lean.Grind.Linarith.Expr.natMul k a => a.toPolyN.mul ↑k
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.Sheaf.cond : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] (F : CategoryTheory.Sheaf J A), CategoryTheory.Presheaf.IsSheaf J F.obj
-- Mathlib.Data.Finsupp.SMul
Finsupp.distribMulActionHom_ext'_iff : ∀ {α : Type u_1} {M : Type u_3} {N : Type u_4} {R : Type u_6} [inst : Monoid R] [inst_1 : AddMonoid M]
  [inst_2 : AddMonoid N] [inst_3 : DistribMulAction R M] [inst_4 : DistribMulAction R N] {f g : (α →₀ M) →+[R] N},
  f = g ↔ ∀ (a : α), f.comp (Finsupp.DistribMulActionHom.single a) = g.comp (Finsupp.DistribMulActionHom.single a)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKeyD_erase_eq_of_not_compare_maxKeyD_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k fallback : α},
  t.erase k ≠ ∅ → ¬cmp k (t.maxKeyD fallback) = Ordering.eq → (t.erase k).maxKeyD fallback = t.maxKeyD fallback
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
/-- If `SheafConditionEqualizerProducts.fork` is an equalizer,
then `F.mapCone (cone U)` is a limit cone.
 -/
TopCat.Presheaf.SheafConditionPairwiseIntersections.isLimitMapConeOfIsLimitSheafConditionFork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasProducts C] →
      {X : TopCat} →
        (F : TopCat.Presheaf C X) →
          {ι : Type v'} →
            (U : ι → TopologicalSpace.Opens ↑X) →
              CategoryTheory.Limits.IsLimit (TopCat.Presheaf.SheafConditionEqualizerProducts.fork F U) →
                CategoryTheory.Limits.IsLimit (CategoryTheory.Functor.mapCone F (CategoryTheory.Pairwise.cocone U).op)
-- Init.Prelude
/-- The number `val` is strictly less than the bound `n`.
 -/
Fin.isLt : ∀ {n : ℕ} (self : Fin n), ↑self < n
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.comp_assoc : ∀ {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst : AddGroup E] [inst_1 : AddGroup F] [inst_2 : AddGroup G]
  (p : AddGroupSeminorm E) (g : F →+ E) (f : G →+ F), p.comp (g.comp f) = (p.comp g).comp f
-- Init.Grind.Config
/-- When `true` (default: `true`), performs zeta reduction of let expressions during normalization.
That is, `let x := v; e[x]` reduces to `e[v]`. See also `zetaDelta`.
 -/
Lean.Grind.Config.zeta : Lean.Grind.Config → Bool
-- Batteries.Recycling.RBTree.Lemmas
/-- A statement of the least-ness of the result of `upperBound?`. If `x` is the return value of
`upperBound?` and it is strictly greater than the cut, then any other `y < x` in the tree is in fact
strictly less than the cut (so there is no exact match, and nothing closer to the cut).
 -/
RBTree.RBNode.Ordered.upperBound?_least : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBTree.RBNode α} {x y : α} [Std.TransCmp cmp]
  [RBTree.RBNode.IsCut cmp cut],
  RBTree.RBNode.Ordered cmp t →
    RBTree.RBNode.upperBound? cut t = some x → y ∈ t → cmp y x = Ordering.lt → cut x = Ordering.lt → cut y = Ordering.gt
-- Init.Data.Order.Factories
/-- The `LE α` instance obtained from an asymmetric `LT α` instance is compatible with said
`LT α` instance.
 -/
Std.LawfulOrderLT.of_lt : ∀ {α : Type u} [inst : LT α] [i : Std.Asymm fun x1 x2 => x1 < x2], Std.LawfulOrderLT α
-- Std.Do.WP.Monad
_private.Std.Do.WP.Monad.0.EStateM.run_bind.match_1.eq_2 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (e : ε) (s : σ)
  (h_1 : (x : α) → (s : σ) → motive (EStateM.Result.ok x s))
  (h_2 : (e : ε) → (s : σ) → motive (EStateM.Result.error e s)),
  (match EStateM.Result.error e s with
    | EStateM.Result.ok x s => h_1 x s
    | EStateM.Result.error e s => h_2 e s) =
    h_2 e s
-- Lean.Expr
Lean.Expr.letE.inj : ∀ {declName : Lean.Name} {type value body : Lean.Expr} {nondep : Bool} {declName_1 : Lean.Name}
  {type_1 value_1 body_1 : Lean.Expr} {nondep_1 : Bool},
  Lean.Expr.letE declName type value body nondep = Lean.Expr.letE declName_1 type_1 value_1 body_1 nondep_1 →
    declName = declName_1 ∧ type = type_1 ∧ value = value_1 ∧ body = body_1 ∧ nondep = nondep_1
-- Std.Async.Basic
Std.Async.instMonadAsyncStateTOfMonadOfFunctor : {m t : Type → Type} →
  {s : Type} → [Monad m] → [Functor t] → [inst : Std.Async.MonadAsync t m] → Std.Async.MonadAsync t (StateT s m)
-- Mathlib.Analysis.CStarAlgebra.Classes
instNonUnitalCStarAlgebraForall : {ι : Type u_1} →
  {A : ι → Type u_2} → [Fintype ι] → [(i : ι) → NonUnitalCStarAlgebra (A i)] → NonUnitalCStarAlgebra ((i : ι) → A i)
-- Mathlib.Order.BooleanAlgebra.Defs
/-- `⊤` is the greatest element  -/
BooleanAlgebra.le_top : ∀ {α : Type u} [self : BooleanAlgebra α] (a : α), a ≤ ⊤
-- Mathlib.Topology.QuasiSeparated
/-- The intersection of two open compact subsets of a quasi-separated space is compact.  -/
QuasiSeparatedSpace.inter_isCompact : ∀ {α : Type u_3} {inst : TopologicalSpace α} [self : QuasiSeparatedSpace α] (U V : Set α),
  IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)
-- Mathlib.Analysis.SpecificLimits.Normed
tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded : ∀ {α : Type u_1} {R : Type u_4} {K : Type u_5} [inst : NormedRing K] [IsDomain K] [inst_2 : NormedAddCommGroup R]
  [inst_3 : Module K R] [Module.IsTorsionFree K R] [NormSMulClass K R] {f : α → K} {g : α → R} {l : Filter α},
  (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖f x • g x‖) →
    Filter.Tendsto f l (Bornology.cobounded K) → Filter.Tendsto g l (nhds 0)
-- Mathlib.Order.Filter.Pointwise
Filter.neg_le_iff_le_neg : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {f g : Filter α}, -f ≤ g ↔ f ≤ -g
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.num_ne_zero : ∀ {K : Type u} [inst : Field K] {x : RatFunc K}, x ≠ 0 → x.num ≠ 0
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Pushforward a distributive multiplicative action along a surjective additive monoid
homomorphism.
See note [reducible non-instances].  -/
Function.Surjective.distribMulAction : {M : Type u_1} →
  {A : Type u_7} →
    {B : Type u_9} →
      [inst : Monoid M] →
        [inst_1 : AddMonoid A] →
          [inst_2 : DistribMulAction M A] →
            [inst_3 : AddMonoid B] →
              [inst_4 : SMul M B] →
                (f : A →+ B) → Function.Surjective ⇑f → (∀ (c : M) (x : A), f (c • x) = c • f x) → DistribMulAction M B
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.coe_toBoundedLatticeHom : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : CompleteLatticeHom α β),
  ⇑f.toBoundedLatticeHom = ⇑f
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
mvfderivWithin_univ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {f : M → F}, d[Set.univ] f = d% f
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.instInhabited : {R : Type u} → {M : Type v} → [inst : SMul R M] → Inhabited (SubMulAction R M)
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquivClass.toMulEquivClass : ∀ {F : Type u_1} {R : outParam (Type u_2)} {A : outParam (Type u_3)} {B : outParam (Type u_4)} {inst : CommSemiring R}
  {inst_1 : Semiring A} {inst_2 : Semiring B} {inst_3 : Algebra R A} {inst_4 : Algebra R B}
  {inst_5 : CoalgebraStruct R A} {inst_6 : CoalgebraStruct R B} {inst_7 : EquivLike F A B}
  [self : BialgEquivClass F R A B], MulEquivClass F A B
-- Mathlib.CategoryTheory.Limits.Yoneda
/-- The cone of `F` corresponding to an element in `(F ⋙ coyoneda.obj X).sections`.  -/
CategoryTheory.Limits.coneOfSectionCompCoyoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{t, w} J] →
        (F : CategoryTheory.Functor J C) →
          (X : Cᵒᵖ) → ↑(F.comp (CategoryTheory.coyoneda.obj X)).sections → CategoryTheory.Limits.Cone F
-- Mathlib.Data.NNRat.Defs
Rat.coe_nnabs : ∀ (x : ℚ), ↑(Rat.nnabs x) = |x|
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.Monomial.mk.sizeOf_spec : ∀ (coef : ℝ) (unit : Tactic.ComputeAsymptotics.UnitMonomial),
  sizeOf { coef := coef, unit := unit } = 1 + sizeOf coef + sizeOf unit
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.homMkSucc.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} {F G : CategoryTheory.ComposableArrows C (n + 1)}
  (α α_1 : F.obj' 0 ⋯ ⟶ G.obj' 0 ⋯) (e_α : α = α_1) (β β_1 : F.δ₀ ⟶ G.δ₀) (e_β : β = β_1)
  (w :
    CategoryTheory.CategoryStruct.comp (F.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 ⋯)
        (CategoryTheory.ComposableArrows.app' β 0 ⋯) =
      CategoryTheory.CategoryStruct.comp α (G.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 ⋯)),
  CategoryTheory.ComposableArrows.homMkSucc α β w = CategoryTheory.ComposableArrows.homMkSucc α_1 β_1 ⋯
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- `spineToSimplex` is a right inverse to `spine X n`.  -/
SSet.StrictSegal.spine_spineToSimplex : ∀ {X : SSet} (self : X.StrictSegal) (n : ℕ), X.spine n ∘ self.spineToSimplex = id
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.ofNat.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.CategoryTheory.Category.Cat.CartesianClosed
CategoryTheory.Cat.ihom_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{u, u} C] (D : Type u) [inst_1 : CategoryTheory.Category.{u, u} D],
  (CategoryTheory.Cat.of C ⟹ CategoryTheory.Cat.of D) = CategoryTheory.Cat.of (CategoryTheory.Functor C D)
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuousOn_inv_iff : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} {s : Set α} [inst_1 : PartialOrder β]
  [inst_2 : CommGroup β] [IsOrderedMonoid β], UpperSemicontinuousOn f⁻¹ s ↔ LowerSemicontinuousOn f s
-- Lean.Meta.Tactic.Grind.MatchCond
_private.Lean.Meta.Tactic.Grind.MatchCond.0.Lean.Meta.Grind.collectMatchCondLhssAndAbstract.go.eq_def : ∀ (e : Lean.Expr) (lhssαs : Array (Lean.Expr × Option Lean.Expr)) (i : ℕ) (xs : Array Lean.Expr)
  (tys : Array (Option Lean.Expr)) (tysxs args : Array Lean.Expr),
  Lean.Meta.Grind.collectMatchCondLhssAndAbstract.go✝ e lhssαs i xs tys tysxs args =
    if h : i < lhssαs.size then
      match lhssαs[i] with
      | (lhs, α?) =>
        match α? with
        | some α => do
          let __do_lift ← liftM (Lean.Meta.inferType α)
          Lean.Meta.withLocalDeclD (`ty.appendIndexAfter i) __do_lift fun ty =>
              Lean.Meta.withLocalDeclD (`x.appendIndexAfter i) ty fun x =>
                Lean.Meta.Grind.collectMatchCondLhssAndAbstract.go✝ e lhssαs (i + 1) (xs.push x) (tys.push (some ty))
                  ((tysxs.push ty).push x) ((args.push α).push lhs)
        | x => do
          let __do_lift ← liftM (Lean.Meta.inferType lhs)
          Lean.Meta.withLocalDeclD (`x.appendIndexAfter i) __do_lift fun x =>
              Lean.Meta.Grind.collectMatchCondLhssAndAbstract.go✝ e lhssαs (i + 1) (xs.push x) (tys.push none)
                (tysxs.push x) (args.push lhs)
    else
      have eAbst := Lean.Meta.Grind.collectMatchCondLhssAndAbstract.go.replaceLhss✝ xs tys e 0;
      do
      let eLam ← liftM (Lean.Meta.mkLambdaFVars tysxs eAbst)
      have e' : Lean.Expr := Lean.mkAppN eLam args
      let __do_lift ← liftM (Lean.Meta.Sym.shareCommon e')
      pure (args, __do_lift)
-- Init.Data.List.Monadic
List.foldrM_filter : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {p : α → Bool}
  {g : α → β → m β} {l : List α} {init : β},
  List.foldrM g init (List.filter p l) = List.foldrM (fun x y => if p x = true then g x y else pure y) init l
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.eq_of_revlexFuel : ∀ {fuel : ℕ} {m₁ m₂ : Lean.Grind.CommRing.Mon}, Lean.Grind.CommRing.Mon.revlexFuel fuel m₁ m₂ = Ordering.eq → m₁ = m₂
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U),
  CategoryTheory.CategoryStruct.comp U.toSpecΓ hU.isoSpec.inv = CategoryTheory.CategoryStruct.id ↑U
-- Mathlib.Algebra.Category.MonCat.Limits
AddCommMonCat.forget_createsLimitsOfSize.eq_1 : AddCommMonCat.forget_createsLimitsOfSize =
  { CreatesLimitsOfShape := fun {J} [CategoryTheory.Category.{w, v} J] => inferInstance }
-- Mathlib.Data.FunLike.IsApply
FunLike.coe_smul : ∀ {M : Type u_1} {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : SMul M F]
  [inst_2 : SMul M β] [IsSMulApply M F α β] (n : M) (f : F), ⇑(n • f) = n • ⇑f
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.map_coord_zero : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) {m : ι → M} (i : ι),
  m i = 0 → f m = 0
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
/-- Given an `f` with non-zero and non-infinite sum, get a `PMF` by normalizing `f` by its `tsum`.
 -/
PMF.normalize : {α : Type u_1} → (f : α → ENNReal) → tsum f ≠ 0 → tsum f ≠ ⊤ → PMF α
-- Mathlib.Tactic.Module
Mathlib.Tactic.Module.NF.sub_eq_eval₂ : ∀ {R : Type u_2} {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (r₁ r₂ : R) (x : M)
  {l₁ l₂ l : Mathlib.Tactic.Module.NF R M},
  l₁.eval - l₂.eval = l.eval → ((r₁, x) ::ᵣ l₁).eval - ((r₂, x) ::ᵣ l₂).eval = ((r₁ - r₂, x) ::ᵣ l).eval
-- Init.Data.Rat.Lemmas
Rat.abs_of_nonneg : ∀ {x : ℚ}, 0 ≤ x → x.abs = x
-- Lean.Parser.Command
Lean.Parser.Command.structParent.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Util.Delaborators
/-- Delaborator for existential quantifier, including extended binders.  -/
exists_delab : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Geometry.Manifold.Instances.Real
/-- The model space used to define `n`-dimensional real manifolds with boundary.  -/
Manifold.«term𝓡∂_» : Lean.ParserDescr
-- Mathlib.Algebra.Group.Hom.Defs
/-- If `M` and `N` have multiplications, `f : M →ₙ* N` is a surjective multiplicative map,
and `M` is commutative, then `N` is commutative.  -/
Function.Surjective.mul_comm : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] {f : M →ₙ* N},
  Function.Surjective ⇑f → IsMulCommutative M → IsMulCommutative N
-- Mathlib.Algebra.Group.Defs
add_ne_add_left : ∀ {G : Type u_1} [inst : Add G] [IsRightCancelAdd G] (a : G) {b c : G}, b + a ≠ c + a ↔ b ≠ c
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.monomial_smul_eq : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (e : σ →₀ ℕ) (p : ℕ) (r : R),
  (MvPowerSeries.monomial (p • e)) r = MvPowerSeries.C r * e.prod fun s e => (MvPowerSeries.X s ^ p) ^ e
-- Mathlib.Topology.Algebra.Monoid.Defs
ContinuousAt.mul_const : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M] [SeparatelyContinuousMul M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f : X → M} {x : X}, ContinuousAt f x → ∀ (b : M), ContinuousAt (fun x => f x * b) x
-- Mathlib.MeasureTheory.Constructions.Pi
/-- An upper bound for the measure in a finite product space.
It is defined by taking the image of the set under all projections, and taking the product
of the measures of these images.
For measurable boxes it is equal to the correct measure.  -/
MeasureTheory.piPremeasure : {ι : Type u_1} →
  {α : ι → Type u_3} → [Fintype ι] → ((i : ι) → MeasureTheory.OuterMeasure (α i)) → Set ((i : ι) → α i) → ENNReal
-- Mathlib.Topology.Algebra.Monoid
AddHom.isClosed_range_coe : ∀ (M₁ : Type u_6) (M₂ : Type u_7) [inst : TopologicalSpace M₂] [T2Space M₂] [inst_2 : Add M₁] [inst_3 : Add M₂]
  [ContinuousAdd M₂], IsClosed (Set.range DFunLike.coe)
-- Init.Data.Vector.Range
Vector.getElem_range : ∀ {n i : ℕ} (hi : i < n), (Vector.range n)[i] = i
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instCancelCommMonoid.eq_1 : ∀ {α : Type u_1} [inst : CancelCommMonoid α],
  Lex.instCancelCommMonoid = { toCommMonoid := Lex.instCommMonoid, toIsLeftCancelMul := ⋯ }
-- Init.Data.List.Find
List.IsPrefix.find?_eq_none : ∀ {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool}, l₁ <+: l₂ → List.find? p l₂ = none → List.find? p l₁ = none
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
OrdinalApprox.lfpApprox_mono_mid : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α), Monotone (OrdinalApprox.lfpApprox f)
-- Std.Data.Internal.List.Associative
Std.Internal.List.congr_filter_containsKey_of_perm : ∀ {α : Type u} {β : α → Type v} {l₁ l₂ l₃ l₄ : List ((a : α) × β a)} [inst : BEq α] [EquivBEq α],
  l₁.Perm l₃ →
    l₂.Perm l₄ →
      Std.Internal.List.DistinctKeys l₃ →
        (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁).Perm
          (List.filter (fun p => Std.Internal.List.containsKey p.fst l₄) l₃)
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.forIn.visit.match_1.eq_1 : ∀ {α : Type u_1} {σ : Type u_3} (motive : RBTree.RBNode α → σ → Sort u_2) (b : σ)
  (h_1 : (b : σ) → motive RBTree.RBNode.nil b)
  (h_2 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → (b : σ) → motive (RBTree.RBNode.node c l v r) b),
  (match RBTree.RBNode.nil, b with
    | RBTree.RBNode.nil, b => h_1 b
    | RBTree.RBNode.node c l v r, b => h_2 c l v r b) =
    h_1 b
-- Lean.Elab.MutualDef
/-- Returns true if `k` is a theorem, option `debug.proofAsSorry` is set to true, and the environment contains the axiom `sorryAx`.  -/
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.useProofAsSorry : Lean.Elab.DefKind → Lean.CoreM Bool
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.isIso_app : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f],
  ∀ V ≤ AlgebraicGeometry.Scheme.Hom.opensRange f, CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.app f V)
-- Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
/-- Implementation: This is a construction which will be used in the proof that
the sieve generated by a family of arrows is effective epimorphic if and only if
the family is an effective epi.
 -/
CategoryTheory.effectiveEpiFamilyStructOfIsColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {B : C} →
      {α : Type u_1} →
        (X : α → C) →
          (π : (a : α) → X a ⟶ B) →
            CategoryTheory.Limits.IsColimit (CategoryTheory.Sieve.generateFamily X π).arrows.cocone →
              CategoryTheory.EffectiveEpiFamilyStruct X π
-- Mathlib.Topology.Inseparable
stableUnderGeneralization_sUnion : ∀ {X : Type u_1} [inst : TopologicalSpace X] (S : Set (Set X)),
  (∀ s ∈ S, StableUnderGeneralization s) → StableUnderGeneralization (⋃₀ S)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.idealFactorsFunOfQuotHom_comp : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : IsDedekindDomain A] {I : Ideal R}
  {J : Ideal A} {B : Type u_4} [inst_3 : CommRing B] [inst_4 : IsDedekindDomain B] {L : Ideal B} {f : R ⧸ I →+* A ⧸ J}
  {g : A ⧸ J →+* B ⧸ L} (hf : Function.Surjective ⇑f) (hg : Function.Surjective ⇑g),
  (IsDedekindDomain.idealFactorsFunOfQuotHom hg).comp (IsDedekindDomain.idealFactorsFunOfQuotHom hf) =
    IsDedekindDomain.idealFactorsFunOfQuotHom ⋯
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.filter_key_equiv_self_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → Bool},
  t.WF → ((Std.DTreeMap.Raw.filter (fun k x => f k) t).Equiv t ↔ ∀ (k : α) (h : k ∈ t), f (t.getKey k h) = true)
-- Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
MvPolynomial.irreducible_sumSMulXSMulY : ∀ {n : Type u_1} {R : Type u_2} [inst : CommRing R] (c : n →₀ R) [IsDomain R],
  c.support.Nontrivial → (∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r) → Irreducible (MvPolynomial.sumSMulXSMulY c)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {h_mem : k ∈ m₁ ∩ m₂}, (m₁ ∩ m₂).getKey k h_mem = m₁.getKey k ⋯
-- Mathlib.Data.Set.Basic
Set.nonempty_of_ssubset' : ∀ {α : Type u} {s t : Set α}, s ⊂ t → t.Nonempty
-- Mathlib.CategoryTheory.Galois.EssSurj
_private.Mathlib.CategoryTheory.Galois.EssSurj.0.CategoryTheory.PreGaloisCategory.quotientDiag : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    {F : CategoryTheory.Functor C FintypeCat} →
      [inst_1 : CategoryTheory.GaloisCategory C] →
        [CategoryTheory.PreGaloisCategory.FiberFunctor F] →
          (V : OpenSubgroup (CategoryTheory.Aut F)) →
            {U : OpenSubgroup (CategoryTheory.Aut F)} →
              (h : (↑U).Normal) →
                {A : C} →
                  ((CategoryTheory.PreGaloisCategory.functorToAction F).obj A ≅
                      Action.FintypeCat.ofMulAction (CategoryTheory.Aut F)
                        (FintypeCat.of (CategoryTheory.Aut F ⧸ ↑U))) →
                    CategoryTheory.Functor (CategoryTheory.SingleObj (↥↑V ⧸ (↑U).subgroupOf ↑V)) C
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.mk.congr_simp : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (toFun toFun_1 : G → H)
  (e_toFun : toFun = toFun_1) (map_add_const' : ∀ (x : G), toFun (x + a) = toFun x + b),
  { toFun := toFun, map_add_const' := map_add_const' } = { toFun := toFun_1, map_add_const' := ⋯ }
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.Entry.token : Lean.Parser.Token → Lean.Parser.ParserExtension.Entry
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.instCanonicallyOverToScheme : {X : AlgebraicGeometry.Scheme} → (U : X.Opens) → (↑U).CanonicallyOver X
-- Mathlib.Algebra.Category.Grp.Yoneda
/-- The `CommGrpCat`-valued coyoneda embedding composed with the forgetful functor is the usual
coyoneda embedding.  -/
CommGrpCat.coyonedaForget : CommGrpCat.coyoneda.comp
    ((CategoryTheory.Functor.whiskeringRight CommGrpCat CommGrpCat (Type u_1)).obj (CategoryTheory.forget CommGrpCat)) ≅
  CategoryTheory.coyoneda