mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
CategoryTheory.Functor.IsLocallyFaithful.ext : ∀ {C : Type uC} [inst : CategoryTheory.Category.{vC, uC} C] {D : Type uD} [inst_1 : CategoryTheory.Category.{vD, uD} D]
  {K : CategoryTheory.GrothendieckTopology D} (G : CategoryTheory.Functor C D) [G.IsLocallyFaithful K]
  (ℱ : CategoryTheory.Sheaf K (Type u_2)) {X Y : C} (i₁ i₂ : X ⟶ Y),
  G.map i₁ = G.map i₂ →
    ∀ {s t : ℱ.obj.obj (Opposite.op (G.obj X))},
      (∀ ⦃Z : C⦄ (j : Z ⟶ X),
          CategoryTheory.CategoryStruct.comp j i₁ = CategoryTheory.CategoryStruct.comp j i₂ →
            (CategoryTheory.ConcreteCategory.hom (ℱ.obj.map (G.map j).op)) s =
              (CategoryTheory.ConcreteCategory.hom (ℱ.obj.map (G.map j).op)) t) →
        s = t
-- Mathlib.Order.SuccPred.Limit
/-- **Alias** of the reverse direction of `Order.isPredPrelimit_toDual_iff`. -/
Order.IsSuccPrelimit.dual : ∀ {α : Type u_1} {a : α} [inst : LT α], Order.IsSuccPrelimit a → Order.IsPredPrelimit (OrderDual.toDual a)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_inter_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α} {fallback : β k},
      Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.inter m₂ ⋯).getD k fallback = fallback
-- Mathlib.RingTheory.LocalProperties.InjectiveDimension
ModuleCat.hasInjectiveDimensionLE_iff_forall_primeSpectrum : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] [IsNoetherianRing R] (n : ℕ) (M : ModuleCat R),
  CategoryTheory.HasInjectiveDimensionLE M n ↔
    ∀ (p : PrimeSpectrum R), CategoryTheory.HasInjectiveDimensionLE (M.localizedModule p.asIdeal.primeCompl) n
-- Mathlib.RingTheory.Smooth.AdicCompletion
DoubleQuot.quotQuotEquivQuotOfLEₐ.congr_simp : ∀ (R : Type u) {A : Type u_1} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {I J : Ideal A}
  (h : I ≤ J), DoubleQuot.quotQuotEquivQuotOfLEₐ R h = DoubleQuot.quotQuotEquivQuotOfLEₐ R h
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- Construct an affine subspace from a point and a direction.  -/
AffineSubspace.mk' : {k : Type u_1} →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module k V] → [inst_3 : AddTorsor V P] → P → Submodule k V → AffineSubspace k P
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.coe_of : ∀ (M : Type u) [inst : Monoid M], ↑(MonCat.of M) = M
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.symm : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp}, t₁.Equiv t₂ → t₂.Equiv t₁
-- Mathlib.Logic.Equiv.Defs
/-- If `f` is a bijective function, then its domain is equivalent to its codomain.  -/
Equiv.ofBijective : {α : Sort u} → {β : Sort v} → (f : α → β) → Function.Bijective f → α ≃ β
-- Batteries.Data.List.Lemmas
List.prod_flatten : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : One α] [Std.LawfulIdentity (fun x1 x2 => x1 * x2) 1]
  [Std.Associative fun x1 x2 => x1 * x2] {l : List (List α)}, l.flatten.prod = (List.map List.prod l).prod
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegral_fun_sub : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E}
  {ω₁ ω₂ : E → E →L[𝕜] F} {γ : Path a b},
  CurveIntegrable ω₁ γ →
    CurveIntegrable ω₂ γ → ∫ᶜ (x : E) in γ, (ω₁ x - ω₂ x) = ∫ᶜ (x : E) in γ, ω₁ x - ∫ᶜ (x : E) in γ, ω₂ x
-- Mathlib.Data.Nat.Init
_private.Mathlib.Data.Nat.Init.0.Nat.strongSubRecursion.match_1.eq_1 : ∀ (motive : ℕ → ℕ → Sort u_1) (n m : ℕ) (h_1 : (n m : ℕ) → motive n m),
  (match n, m with
    | n, m => h_1 n m) =
    h_1 n m
-- Mathlib.RingTheory.Noetherian.Defs
isNoetherian_submodule : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M}, IsNoetherian R ↥N ↔ ∀ s ≤ N, s.FG
-- Mathlib.MeasureTheory.Measure.PreVariation
MeasureTheory.preVariation.sum_le_preVariationFun_iUnion' : ∀ {X : Type u_1} [inst : MeasurableSpace X] (f : Set X → ENNReal) {s : ℕ → Set X} (hs : ∀ (i : ℕ), MeasurableSet (s i)),
  Pairwise (Function.onFun Disjoint s) →
    ∀ (P : (i : ℕ) → Finpartition ⟨s i, ⋯⟩) (n : ℕ),
      ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f ↑p ≤ MeasureTheory.preVariationFun f (⋃ i, s i)
-- Mathlib.CategoryTheory.Join.Basic
/-- The left inclusion is fully faithful.  -/
CategoryTheory.Join.inclLeftFullyFaithful : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (CategoryTheory.Join.inclLeft C D).FullyFaithful
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_inter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, (m₁.inter m₂).getKey? k = if m₂.contains k = true then m₁.getKey? k else none
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_functor : ∀ {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),
  (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv F U).functor =
    TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor F U
-- Mathlib.Tactic.Linter.FlexibleLinter
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.Stained.name.sizeOf_spec : ∀ (a : Lean.Name), sizeOf (Mathlib.Linter.Flexible.Stained.name✝ a) = 1 + sizeOf a
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.inner_smul_ofReal_left : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] (x y : F) {t : ℝ}, inner 𝕜 (↑t • x) y = inner 𝕜 x y * ↑t
-- Mathlib.Data.Fin.Basic
Fin.natCast_zero : ∀ {n : ℕ} [inst : NeZero n], ↑0 = 0
-- Std.Data.HashMap.Iterator
/-- Returns a finite iterator over the entries of a hash map.
The iterator yields the elements of the map in order and then terminates.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Std.HashMap.iter : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Std.HashMap α β → Std.Iter (α × β)
-- Mathlib.Logic.Equiv.Nat
Equiv.boolProdNatEquivNat_apply : ∀ (a : Bool × ℕ), Equiv.boolProdNatEquivNat a = Function.uncurry Nat.bit a
-- Mathlib.RingTheory.PolynomialLaw.Basic
_private.Mathlib.RingTheory.PolynomialLaw.Basic.0.PolynomialLaw.π.match_1.eq_1 : ∀ (R : Type u_1) [inst : CommSemiring R] (M : Type u_3) [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (S : Type u_2)
  (motive : PolynomialLaw.lifts R M S → Sort u_4) (s : Finset S) (p : TensorProduct R (MvPolynomial (Fin s.card) R) M)
  (h_1 : (s : Finset S) → (p : TensorProduct R (MvPolynomial (Fin s.card) R) M) → motive ⟨s, p⟩),
  (match ⟨s, p⟩ with
    | ⟨s, p⟩ => h_1 s p) =
    h_1 s p
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Real.arsinh_inj : ∀ {x y : ℝ}, Real.arsinh x = Real.arsinh y ↔ x = y
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Extract
Std.Tactic.BVDecide.BVExpr.bitblast.ExtractTarget.w : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} → {len : ℕ} → Std.Tactic.BVDecide.BVExpr.bitblast.ExtractTarget aig len → ℕ
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- A factorisation of a morphism `f = e ≫ m`, with `m` monic.  -/
CategoryTheory.Limits.MonoFactorisation.fac_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  (self : CategoryTheory.Limits.MonoFactorisation f) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.e (CategoryTheory.CategoryStruct.comp self.m h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.mem_iInf : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {ι : Sort u_1}
  {S : ι → Subalgebra R A} {x : A}, x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
-- Mathlib.CategoryTheory.Category.Factorisation
/-- The forgetful functor from `Factorisation f` to the underlying category `C`.  -/
CategoryTheory.Factorisation.forget : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → {f : X ⟶ Y} → CategoryTheory.Functor (CategoryTheory.Factorisation f) C
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
ProfiniteGrp.ProfiniteCompletion.lift_unique : ∀ {G : GrpCat} {P : ProfiniteGrp.{u}} (f g : ProfiniteGrp.ProfiniteCompletion.completion G ⟶ P),
  CategoryTheory.CategoryStruct.comp (ProfiniteGrp.ProfiniteCompletion.eta G)
        ((CategoryTheory.forget₂ ProfiniteGrp.{u} GrpCat).map f) =
      CategoryTheory.CategoryStruct.comp (ProfiniteGrp.ProfiniteCompletion.eta G)
        ((CategoryTheory.forget₂ ProfiniteGrp.{u} GrpCat).map g) →
    f = g
-- Mathlib.Order.Interval.Basic
NonemptyInterval.coe_pure : ∀ {α : Type u_1} [inst : PartialOrder α] (a : α), ↑(NonemptyInterval.pure a) = {a}
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.sum_le_card_nsmul : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : Preorder α] [AddLeftMono α] (s : Multiset α) (n : α),
  (∀ x ∈ s, x ≤ n) → s.sum ≤ s.card • n
-- Mathlib.Algebra.Group.Equiv.Opposite
MulOpposite.opMulEquiv_apply : ∀ {M : Type u_1} [inst : CommMonoid M] (a : M), MulOpposite.opMulEquiv a = MulOpposite.op a
-- Lean.Expr
Lean.Expr.forallDomain : (a : Lean.Expr) → a.isForall = true → Lean.Expr
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.uniqueToTypeOne : Unique (Ordinal.ToType 1)
-- Mathlib.Analysis.Normed.Order.Lattice
norm_sup_sub_sup_le_add_norm : ∀ {α : Type u_1} [inst : NormedAddCommGroup α] [inst_1 : Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α]
  (a b c d : α), ‖a ⊔ b - c ⊔ d‖ ≤ ‖a - c‖ + ‖b - d‖
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.homologyFunctorSingleIso_hom_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  [inst_4 : CategoryTheory.CategoryWithHomology C] (X : C),
  (HomologicalComplex.homologyFunctorSingleIso C c j).hom.app X =
    (HomologicalComplex.singleObjHomologySelfIso c j X).hom
-- Std.Http.Data.Headers.Name
Std.Http.Header.Name.mk.injEq : ∀ (value : String)
  (isValidHeaderValue :
    autoParam (Std.Http.Header.IsValidHeaderName value) Std.Http.Header.Name.isValidHeaderValue._autoParam)
  (isLowerCase : autoParam (Std.Http.Internal.IsLowerCase value) Std.Http.Header.Name.isLowerCase._autoParam)
  (value_1 : String)
  (isValidHeaderValue_1 :
    autoParam (Std.Http.Header.IsValidHeaderName value_1) Std.Http.Header.Name.isValidHeaderValue._autoParam)
  (isLowerCase_1 : autoParam (Std.Http.Internal.IsLowerCase value_1) Std.Http.Header.Name.isLowerCase._autoParam),
  ({ value := value, isValidHeaderValue := isValidHeaderValue, isLowerCase := isLowerCase } =
      { value := value_1, isValidHeaderValue := isValidHeaderValue_1, isLowerCase := isLowerCase_1 }) =
    (value = value_1)
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.val_neg_eq_neg_val : ∀ {α : Type u} [inst : SubtractionMonoid α] (u : AddUnits α), ↑(-u) = -↑u
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- If the arguments are linearly dependent then the result is `0`.  -/
AlternatingMap.map_linearDependent : ∀ {ι : Type u_7} {K : Type u_12} {M : Type u_13} {N : Type u_14} [inst : Ring K] [IsDomain K] [inst_2 : AddCommGroup M]
  [inst_3 : Module K M] [inst_4 : AddCommGroup N] [inst_5 : Module K N] [Module.IsTorsionFree K N] (f : M [⋀^ι]→ₗ[K] N)
  (v : ι → M), ¬LinearIndependent K v → f v = 0
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.IsTotallyReal.nrComplexPlaces_eq_zero : ∀ (K : Type u_2) [inst : Field K] [inst_1 : NumberField K] [h : NumberField.IsTotallyReal K],
  NumberField.InfinitePlace.nrComplexPlaces K = 0
-- Mathlib.Tactic.Check
/-- Like `checkCore`, but logs different messages depending on whether `showImplicit` is
true. Note that this differs from `checkCore` only in that it modifies the constructed message,
lowers to `TermElabM`, and always takes `ignoreStuckTC := true` (as `#check` ultimately does).

This declaration may realize constants, and so should be run without modifying the environment.

Info messages are placed at `tk`. If there are several resolved names for `term`, shows
information only for the first of them instead of failing.  -/
_private.Mathlib.Tactic.Check.0.Mathlib.Tactic.checkCoreAux : Lean.Syntax → Lean.Term → Bool → Lean.Elab.TermElabM Unit
-- Mathlib.Topology.Instances.Matrix
Summable.matrix_blockDiagonal' : ∀ {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l → Type u_9} {n' : l → Type u_10} [inst : AddCommMonoid R]
  [inst_1 : TopologicalSpace R] {L : SummationFilter X} [inst_2 : DecidableEq l]
  {f : X → (i : l) → Matrix (m' i) (n' i) R}, Summable f L → Summable (fun x => Matrix.blockDiagonal' (f x)) L
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesAt.eventually_hasSum_sub : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E},
  HasFPowerSeriesAt f p x → ∀ᶠ (y : E) in nhds x, HasSum (fun n => (p n) fun x_1 => y - x) (f y)
-- Lean.Meta.Tactic.Grind.SimpUtil
Lean.Meta.Grind.reduceCtorEqCheap : Lean.Meta.Simp.Simproc
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.single_zsmul : ∀ {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst_1 : (i : I) → AddGroup (f i)] (i : I) (x : f i) (n : ℤ),
  Pi.single i (n • x) = n • Pi.single i x
-- Aesop.RuleTac.Forward
Aesop.RuleTac.ForwardM.State.usedHyps : Aesop.RuleTac.ForwardM.State → Std.HashSet Lean.FVarId
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.instMonadGrindTacticM : Monad Lean.Elab.Tactic.Grind.GrindTacticM
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.infinite_of_infinite : ∀ {α : Type u_1} {M : Matroid α} {B B₁ : Set α}, M.IsBase B → B.Infinite → M.IsBase B₁ → B₁.Infinite
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.aeval_equivPolynomial : ∀ {R : Type u_2} [inst : CommRing R] {S : Type u_8} [inst_1 : CommRing S] [inst_2 : Algebra S R]
  (f : PolynomialModule S S) (x : R),
  (Polynomial.aeval x) (PolynomialModule.equivPolynomial f) =
    (PolynomialModule.eval x) ((PolynomialModule.map R (Algebra.linearMap S R)) f)
-- Mathlib.Analysis.Normed.Lp.lpHolder
/-- `lp.holder` as a bilinear map.  -/
lp.holderₗ : {ι : Type u_1} →
  {𝕜 : Type u_2} →
    {E : ι → Type u_3} →
      {F : ι → Type u_4} →
        {G : ι → Type u_5} →
          [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)] →
                    [inst_5 : (i : ι) → NormedAddCommGroup (G i)] →
                      [inst_6 : (i : ι) → NormedSpace 𝕜 (G i)] →
                        {p q : ENNReal} →
                          (r : ENNReal) →
                            [hpqr : p.HolderTriple q r] →
                              (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) →
                                {K : ℝ} → (∀ (i : ι), ‖B i‖ ≤ K) → ↥(lp E p) →ₗ[𝕜] ↥(lp F q) →ₗ[𝕜] ↥(lp G r)
-- Mathlib.Algebra.Order.Module.Rat
LinearOrderedSemifield.toPosSMulStrictMono_rat : ∀ {α : Type u_1} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α], PosSMulStrictMono ℚ≥0 α
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- The `n` weighted homogeneous component of a polynomial is weighted homogeneous of
weighted degree `n`.  -/
MvPolynomial.weightedHomogeneousComponent_isWeightedHomogeneous : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {w : σ → M} (n : M)
  (φ : MvPolynomial σ R), MvPolynomial.IsWeightedHomogeneous w ((MvPolynomial.weightedHomogeneousComponent w n) φ) n
-- Mathlib.Data.Fintype.OfMap
Fintype.instEmpty : Fintype Empty
-- Lean.Meta.Tactic.Grind.Simp
Lean.Meta.Grind.pushNewFact' : Lean.Expr → Lean.Expr → optParam ℕ 0 → Lean.Meta.Grind.GoalM Unit
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.norm_le_norm_mul_left : ∀ (x : GaussianInt) {y : GaussianInt}, y ≠ 0 → (Zsqrtd.norm x).natAbs ≤ (Zsqrtd.norm (x * y)).natAbs
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int8.succMany?_eq_maxValueSealed : ∀ {n : ℕ} {i : Int8},
  Std.PRange.succMany? n i =
    have this := ⋯;
    if h : i.toInt + ↑n ≤ Int8.maxValueSealed✝.toInt then some (Int8.ofIntLE (i.toInt + ↑n) ⋯ ⋯) else none
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
le_mabs : ∀ {α : Type u_1} [inst : Group α] [inst_1 : LinearOrder α] {a b : α}, a ≤ |b|ₘ ↔ a ≤ b ∨ a ≤ b⁻¹
-- Mathlib.MeasureTheory.Group.Convolution
/-- Convolution of the zero measure with a measure μ returns the zero measure.  -/
MeasureTheory.Measure.zero_mconv : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : MeasurableSpace M] (μ : MeasureTheory.Measure M),
  MeasureTheory.Measure.mconv 0 μ = 0
-- Mathlib.Algebra.Ring.Subsemiring.Pointwise
Subsemiring.instCovariantClassHSMulLe : ∀ {M : Type u_1} {R : Type u_2} [inst : Monoid M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R],
  CovariantClass M (Subsemiring R) HSMul.hSMul LE.le
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.le_inf_sub : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : Sub α] [inst_2 : SemilatticeInf β]
  [inst_3 : OrderTop β] {s t : Finset α} {f : α → β} {a : β}, a ≤ (s - t).inf f ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ f (x - y)
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.univ_inter : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (s : Finset α), Finset.univ ∩ s = s
-- Mathlib.Data.Rat.Floor
Rat.isNat_intFract_of_isInt : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorRing R] (r : R)
  (m : ℤ), Mathlib.Meta.NormNum.IsInt r m → Mathlib.Meta.NormNum.IsNat (Int.fract r) 0
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The cokernel of an epimorphism is isomorphic to the zero object  -/
CategoryTheory.Limits.cokernel.ofEpi : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
            [inst_3 : CategoryTheory.Limits.HasCokernel f] →
              [CategoryTheory.Epi f] → CategoryTheory.Limits.cokernel f ≅ 0
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.then.eq_1 : Turing.ToPartrec.Cont.halt.then = fun k' => k'
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.Iter.forIn'_eq_match_step.match_3.eq_1 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it : Std.Iter β} (motive : it.Step → Sort u_2) (it' : Std.Iter β)
  (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.Iter β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_1 it' out h
-- Mathlib.Order.CompleteLattice.Finset
Finset.set_biUnion_finset_image : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : DecidableEq α] {f : γ → α} {g : α → Set β} {s : Finset γ},
  ⋃ x ∈ Finset.image f s, g x = ⋃ y ∈ s, g (f y)
-- Lean.Expr
Lean.Expr.mvar.injEq : ∀ (mvarId mvarId_1 : Lean.MVarId), (Lean.Expr.mvar mvarId = Lean.Expr.mvar mvarId_1) = (mvarId = mvarId_1)
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.grindPatternCnstrs : Lean.Parser.Parser
-- Init.Data.Array.Lex.Lemmas
Array.lex_eq_true_iff_lt : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] [inst_2 : LT α] [inst_3 : DecidableLT α] {xs ys : Array α},
  (xs.lex ys fun x1 x2 => decide (x1 < x2)) = true ↔ xs < ys
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
/-- The data of a Fredholm package for `u` determines a canonical quasi-inverse of `u`.  -/
ContinuousLinearMap.FredholmPackage.isQuasiInverse : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E]
  [inst_6 : TopologicalSpace F] {u : E →L[𝕜] F} (pkg : u.FredholmPackage), (↑pkg.quasiInverse).IsQuasiInverse ↑u
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.unique : {m : Type u_2} → {n : Type u_3} → {α : Type v} → [Unique α] → Unique (Matrix m n α)
-- Mathlib.Data.DFinsupp.Lex
/-- The less-or-equal relation for the lexicographic ordering is decidable.  -/
DFinsupp.Lex.decidableLE : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : (i : ι) → Zero (α i)] →
      [inst_1 : LinearOrder ι] → [inst_2 : (i : ι) → LinearOrder (α i)] → DecidableLE (Lex (Π₀ (i : ι), α i))
-- Mathlib.Data.Finset.Card
Multiset.toFinset_card_le : ∀ {α : Type u_1} [inst : DecidableEq α] (m : Multiset α), m.toFinset.card ≤ m.card
-- Lean.Server.Completion.SyntheticCompletion
_private.Lean.Server.Completion.SyntheticCompletion.0.Lean.Server.Completion.isSyntheticTacticCompletion.isCompletionAfterSemicolon : Lean.FileMap → String.Pos.Raw → Lean.Syntax → Bool
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
/-- Each differential of a `C^n` diffeomorphism of Banach manifolds (`n ≠ 0`)
is a linear equivalence.  -/
Diffeomorph.mfderivToContinuousLinearEquiv : {𝕜 : 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] →
                {H₁ : Type u_5} →
                  [inst_5 : TopologicalSpace H₁] →
                    {H₂ : Type u_6} →
                      [inst_6 : TopologicalSpace H₂] →
                        {I : ModelWithCorners 𝕜 E H₁} →
                          {J : ModelWithCorners 𝕜 F H₂} →
                            {M : Type u_8} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H₁ M] →
                                  {N : Type u_9} →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace H₂ N] →
                                        {n : WithTop ℕ∞} →
                                          (Φ : Diffeomorph I J M N n) →
                                            n ≠ 0 → (x : M) → TangentSpace I x ≃L[𝕜] TangentSpace J (Φ x)
-- Init.Data.Array.Lemmas
Array.append_eq_replicate_iff : ∀ {α : Type u_1} {n : ℕ} {xs ys : Array α} {a : α},
  xs ++ ys = Array.replicate n a ↔
    xs.size + ys.size = n ∧ xs = Array.replicate xs.size a ∧ ys = Array.replicate ys.size a
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.lowerBound?_eq_find? : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x y : α} {t : RBTree.RBSet α cmp},
  t.find? x = some y → t.lowerBound? x = some y
-- Mathlib.CategoryTheory.Category.Preorder
/-- Express an inequality as a morphism in the corresponding preorder category.  -/
CategoryTheory.homOfLE : {X : Type u} → [inst : Preorder X] → {x y : X} → x ≤ y → (x ⟶ y)
-- Mathlib.Topology.Algebra.Support
HasCompactMulSupport.intro : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : One β] {f : α → β} {K : Set α} [R1Space α],
  IsCompact K → (∀ x ∉ K, f x = 1) → HasCompactMulSupport f