mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.tsupport_extend_zero_subset : ∀ {α : Type u_2} {α' : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace α']
  [inst_2 : Zero β] {f : α → β} [T2Space α'],
  HasCompactSupport f → ∀ {g : α → α'}, Continuous g → tsupport (Function.extend g f 0) ⊆ g '' tsupport f
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.WF.getThenInsertIfNew?! : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [Std.TransOrd α] [inst : Std.LawfulEqOrd α] {k : α} {v : β k}
  {t : Std.DTreeMap.Internal.Impl α β}, t.WF → (t.getThenInsertIfNew?! k v).2.WF
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt_apply : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) {X : ModuleCat R}
  {Y : ModuleCat S} (s : S) (g : X ⟶ (ModuleCat.restrictScalars f).obj Y) (x : ↑X),
  (ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g) x = s • (CategoryTheory.ConcreteCategory.hom g) x
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.restrictScalars_inf : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type u_3)
  [inst_3 : Field K] [inst_4 : Algebra K E] [inst_5 : Algebra K F] [inst_6 : IsScalarTower K F E]
  (L L' : IntermediateField F E),
  IntermediateField.restrictScalars K L ⊓ IntermediateField.restrictScalars K L' =
    IntermediateField.restrictScalars K (L ⊓ L')
-- Batteries.Data.MLList.Basic
/-- The empty `MLList`.  -/
MLList.nil : {m : Type u_1 → Type u_1} → {α : Type u_1} → MLList m α
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.zero_def : ∀ {M : Type u_4} [inst : AddZeroClass M] (S : AddSubmonoid M), 0 = ⟨0, ⋯⟩
-- Lean.Message
Lean.instToMessageDataTSyntax : {k : Lean.SyntaxNodeKinds} → Lean.ToMessageData (Lean.TSyntax k)
-- Init.Data.UInt.Lemmas
USize.ofFin_bitVecToFin : ∀ (n : BitVec System.Platform.numBits), USize.ofFin n.toFin = { toBitVec := n }
-- Mathlib.Algebra.Ring.Associator
/-- The multiplication `x * (y * z)` of three elements of a (non-associative)
(semi)-ring is an `AddMonoidHom` in each argument.  -/
AddMonoidHom.mulRight₃ : {R : Type u_1} → [inst : NonUnitalNonAssocSemiring R] → R →+ R →+ R →+ R
-- Mathlib.CategoryTheory.Preadditive.EilenbergMoore
CategoryTheory.Monad.algebraPreadditive_homGroup_nsmul_f : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (T : CategoryTheory.Monad C) [inst_2 : T.Additive] (F G : T.Algebra) (n : ℕ) (α : F ⟶ G), (n • α).f = n • α.f
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel_K : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : CategoryTheory.Limits.HasKernel S.g]
  [inst_3 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.lift S.g S.f ⋯)],
  (CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel S).K = CategoryTheory.Limits.kernel S.g
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- If a function is at least `C^1`, its bundled derivative (mapping `(x, v)` to `Df(x) v`) is
continuous.  -/
ContDiff.continuous_fderiv_apply : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : WithTop ℕ∞}, ContDiff 𝕜 n f → n ≠ 0 → Continuous fun p => (fderiv 𝕜 f p.1) p.2
-- Mathlib.Order.Interval.Finset.Nat
Nat.instLocallyFiniteOrder : LocallyFiniteOrder ℕ
-- Lean.Data.NameMap.Basic
Lean.NameHashSet.instEmptyCollection : EmptyCollection Lean.NameHashSet
-- Mathlib.Order.OrderDual
OrderDual.instLE : (α : Type u_2) → [h : LE α] → LE αᵒᵈ
-- Mathlib.GroupTheory.Order.Min
AddMonoid.minOrder_le_natCard : ∀ {G : Type u_1} [inst : AddGroup G] {s : AddSubgroup G}, s ≠ ⊥ → (↑s).Finite → AddMonoid.minOrder G ≤ ↑(Nat.card ↥s)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.IsInner.ne_zero : ∀ {X : SSet} {A : X.Subcomplex} {h : A.PairingCore} [self : h.IsInner] (s : h.ι), h.index s ≠ 0
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
/-- If `g : ℝ → ℝ` is periodic with period `T > 0`, then for any `t : ℝ`, the function
`t ↦ ∫ x in 0..t, g x` is bounded above by `t ↦ X + ⌊t/T⌋ • Y` for appropriate constants `X` and
`Y`.  -/
Function.Periodic.integral_le_sSup_add_zsmul_of_pos : ∀ {T : ℝ} {g : ℝ → ℝ},
  Function.Periodic g T →
    IntervalIntegrable g MeasureTheory.volume 0 T →
      0 < T →
        ∀ (t : ℝ),
          ∫ (x : ℝ) in 0..t, g x ≤
            sSup ((fun t => ∫ (x : ℝ) in 0..t, g x) '' Set.Icc 0 T) + ⌊t / T⌋ • ∫ (x : ℝ) in 0..T, g x
-- Mathlib.LinearAlgebra.Contraction
/-- A linear equivalence between `Dual M ⊗ Dual N` and `Dual (M ⊗ N)` when `M` and `N` are finite free
modules. It sends `f ⊗ g` to the composition of `TensorProduct.map f g` with the natural
isomorphism `R ⊗ R ≃ R`.
 -/
TensorProduct.dualDistribEquiv : (R : Type u_7) →
  (M : Type u_8) →
    (N : Type u_9) →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : Module R M] →
              [inst_4 : Module R N] →
                [Module.Finite R M] →
                  [Module.Finite R N] →
                    [Module.Free R M] →
                      [Module.Free R N] →
                        TensorProduct R (Module.Dual R M) (Module.Dual R N) ≃ₗ[R] Module.Dual R (TensorProduct R M N)
-- Mathlib.Order.Monotone.Basic
Nat.pow_self_mono : Monotone fun n => n ^ n
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.inl_comp_pushoutComparison_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_2 : CategoryTheory.Limits.HasPushout f g] [inst_3 : CategoryTheory.Limits.HasPushout (G.map f) (G.map g)]
  {Z_1 : D} (h : G.obj (CategoryTheory.Limits.pushout f g) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (G.map f) (G.map g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutComparison G f g) h) =
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pushout.inl f g)) h
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.UniversallyEffectiveEquivalenceRelation.universally_effectiveEpi_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R A : C} {p₁ p₂ : R ⟶ A}
  (self : CategoryTheory.UniversallyEffectiveEquivalenceRelation p₁ p₂),
  CategoryTheory.MorphismProperty.universally (fun x x_1 f => CategoryTheory.EffectiveEpi f) self.π
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
CategoryTheory.Limits.hasCountableProducts_of_hasCountableLimits : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCountableLimits C],
  CategoryTheory.Limits.HasCountableProducts C
-- Mathlib.Algebra.Group.Equiv.TypeTags
/-- `Additive (G × H)` is equivalent to `Additive G × Additive H`.  -/
AddEquiv.prodAdditive : (G : Type u_2) → (H : Type u_3) → [inst : Mul G] → [inst_1 : Mul H] → Additive (G × H) ≃+ Additive G × Additive H
-- Mathlib.Algebra.Order.Disjointed
partialSups_add_one_eq_sup_disjointed : ∀ {α : Type u_1} {ι : Type u_2} [inst : GeneralizedBooleanAlgebra α] [inst_1 : LinearOrder ι]
  [inst_2 : LocallyFiniteOrderBot ι] [inst_3 : Add ι] [inst_4 : One ι] [SuccAddOrder ι] (f : ι → α) (i : ι),
  (partialSups f) (i + 1) = (partialSups f) i ⊔ disjointed f (i + 1)
-- Mathlib.Topology.Order.IntermediateValue
/-- If a preconnected set contains endpoints of an interval, then it includes the whole interval.  -/
IsPreconnected.Icc_subset : ∀ {α : Type v} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {s : Set α},
  IsPreconnected s → ∀ {a b : α}, a ∈ s → b ∈ s → Set.Icc a b ⊆ s
-- Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
Continuous.continuousGeneratedBy : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [inst_1 : TopologicalSpace Y]
  {Z : Type v'} [inst_2 : TopologicalSpace Z] {g : Y → Z}, Continuous g → Topology.ContinuousGeneratedBy X g
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.instInhabitedMethods : Inhabited Lean.Meta.Sym.Simp.Methods
-- Mathlib.CategoryTheory.Sites.CompatibleSheafification
CategoryTheory.GrothendieckTopology.toSheafify_comp_sheafifyCompIso_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  (F : CategoryTheory.Functor D E)
  [inst_3 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [inst_4 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [inst_5 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E]
  [inst_7 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F]
  [inst_8 :
    ∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F]
  (P : CategoryTheory.Functor Cᵒᵖ D) {Z : CategoryTheory.Functor Cᵒᵖ E} (h : (J.sheafify P).comp F ⟶ Z),
  CategoryTheory.CategoryStruct.comp (J.toSheafify (P.comp F))
      (CategoryTheory.CategoryStruct.comp (J.sheafifyCompIso F P).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (J.toSheafify P) F) h
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
TopCat.isEmbedding_pullback_to_prod : ∀ {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z),
  Topology.IsEmbedding
    ⇑(CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.pullback.fst f g)
          (CategoryTheory.Limits.pullback.snd f g)))
-- Mathlib.RingTheory.IsGaloisGroup.Basic
IsGaloisGroup.mulSemiringActionQuotient_smul_def : ∀ (G : Type u_1) [inst : Group G] (B : Type u_3) (C : Type u_4) [inst_1 : Semiring C] [inst_2 : MulSemiringAction G C]
  (N : Subgroup G) [inst_3 : CommSemiring B] [inst_4 : Algebra B C] [inst_5 : FaithfulSMul B C]
  [inst_6 : MulSemiringAction G B] [SMulDistribClass G B C] [inst_8 : IsGaloisGroup (↥N) B C] [inst_9 : N.Normal]
  (g : G) (b : B), ↑g • b = g • b
-- Mathlib.Algebra.Order.Sub.Defs
tsub_le_tsub_left : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b : α}
  [AddLeftMono α], a ≤ b → ∀ (c : α), c - b ≤ c - a
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.log_le_log_iff : ∀ {x y : ENNReal}, x.log ≤ y.log ↔ x ≤ y
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instNonUnitalSemiring : {X : Type u_1} →
  {Y : Type u_2} → [inst : TopologicalSpace X] → [NonUnitalSemiring Y] → NonUnitalSemiring (LocallyConstant X Y)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The quotient of a ring by he zero ideal is isomorphic to the ring itself.  -/
RingEquiv.quotientBot : (R : Type u_1) → [inst : Ring R] → R ⧸ ⊥ ≃+* R
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.mk_eq_zero : ∀ {z : ℂ} (hz : ‖z‖ < 1), Complex.UnitDisc.mk z hz = 0 ↔ z = 0
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.symm_trans_apply : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (e₁ : M ≃+ N)
  (e₂ : N ≃+ P) (p : P), (e₁.trans e₂).symm p = e₁.symm (e₂.symm p)
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.toSpanSingletonLIE_apply : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (x : E),
  (ContinuousLinearMap.toSpanSingletonLIE 𝕜 E) x = ContinuousLinearMap.toSpanSingleton 𝕜 x
-- Mathlib.CategoryTheory.ShrinkYoneda
/-- If a functor `F : C ⥤ Type w'` is `w`-small, this is the functor `C ⥤ Type w`
obtained by shrinking `F.obj X` for all `X : C`.  -/
CategoryTheory.FunctorToTypes.shrink : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor C (Type w')) →
      [CategoryTheory.FunctorToTypes.Small.{w, w', v, u} F] → CategoryTheory.Functor C (Type w)
-- Mathlib.Topology.Order
/-- **Alias** of the reverse direction of `TopologicalSpace.nontrivial_iff_exists_not_inseparable`. -/
NontrivialTopology.of_exists_not_inseparable : ∀ {α : Type u} {t : TopologicalSpace α}, (∃ x y, ¬Inseparable x y) → NontrivialTopology α
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.coproductIsCoproduct.eq_1 : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : β → C)
  [inst_1 : CategoryTheory.Limits.HasCoproduct f],
  CategoryTheory.Limits.coproductIsCoproduct f =
    (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor f)).ofIsoColimit
      (CategoryTheory.Limits.Cocone.ext
        (CategoryTheory.Iso.refl (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Discrete.functor f)).pt) ⋯)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.erase0.inj : ∀ {c c_1 : Lean.Meta.Grind.AC.DiseqCnstr},
  Lean.Meta.Grind.AC.DiseqCnstrProof.erase0 c = Lean.Meta.Grind.AC.DiseqCnstrProof.erase0 c_1 → c = c_1
-- Std.Data.HashSet.Lemmas
Std.HashSet.size_inter_eq_size_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  (∀ a ∈ m₂, a ∈ m₁) → (m₁ ∩ m₂).size = m₂.size
-- Mathlib.Topology.Path
/-- Given a path in `X` and a path in `Y`, we can take their pointwise product to get a path in
`X × Y`.  -/
Path.prod : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → {a₁ a₂ : X} → {b₁ b₂ : Y} → Path a₁ a₂ → Path b₁ b₂ → Path (a₁, b₁) (a₂, b₂)
-- Mathlib.Algebra.Polynomial.Lifts
/-- If `(r : R)`, then `C (f r)` lifts.  -/
Polynomial.C_mem_lifts : ∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] (f : R →+* S) (r : R),
  Polynomial.C (f r) ∈ Polynomial.lifts f
-- Lean.Meta.AbstractMVars
Lean.Meta.AbstractMVars.State.mk.sizeOf_spec : ∀ (ngen : Lean.NameGenerator) (lctx : Lean.LocalContext) (mctx : Lean.MetavarContext) (nextParamIdx : ℕ)
  (paramNames : Array Lean.Name) (fvars mvars : Array Lean.Expr) (lmap : Std.HashMap Lean.LMVarId Lean.Level)
  (emap : Std.HashMap Lean.MVarId Lean.Expr) (abstractLevels : Bool),
  sizeOf
      { ngen := ngen, lctx := lctx, mctx := mctx, nextParamIdx := nextParamIdx, paramNames := paramNames,
        fvars := fvars, mvars := mvars, lmap := lmap, emap := emap, abstractLevels := abstractLevels } =
    1 + sizeOf ngen + sizeOf lctx + sizeOf mctx + sizeOf nextParamIdx + sizeOf paramNames + sizeOf fvars +
            sizeOf mvars +
          sizeOf lmap +
        sizeOf emap +
      sizeOf abstractLevels
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Iic_add_Iio_subset : ∀ {α : Type u_1} [inst : Add α] [inst_1 : PartialOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] (a b : α),
  Set.Iic a + Set.Iio b ⊆ Set.Iio (a + b)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_attach : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] (s : Finset ι) (f : ι → M), ∑ x ∈ s.attach, f ↑x = ∑ x ∈ s, f x
-- Mathlib.Analysis.Complex.Norm
Complex.norm_eq_sqrt_sq_add_sq : ∀ (z : ℂ), ‖z‖ = √(z.re ^ 2 + z.im ^ 2)
-- Mathlib.Order.ULift
ULift.up_le : ∀ {α : Type u} [inst : LE α] {a b : α}, { down := a } ≤ { down := b } ↔ a ≤ b
-- Mathlib.Data.Finset.SDiff
Finset.union_sdiff_self : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), (s ∪ t) \ t = s \ t
-- Init.Meta.Defs
Lean.Name.capitalize : Lean.Name → Lean.Name
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.RecCallWithContext.mk.inj : ∀ {ref : Lean.Syntax} {caller : ℕ} {params : Array Lean.Expr} {callee : ℕ} {args : Array Lean.Expr}
  {ctxt : Lean.Elab.WF.GuessLex.SavedLocalContext} {ref_1 : Lean.Syntax} {caller_1 : ℕ} {params_1 : Array Lean.Expr}
  {callee_1 : ℕ} {args_1 : Array Lean.Expr} {ctxt_1 : Lean.Elab.WF.GuessLex.SavedLocalContext},
  { ref := ref, caller := caller, params := params, callee := callee, args := args, ctxt := ctxt } =
      { ref := ref_1, caller := caller_1, params := params_1, callee := callee_1, args := args_1, ctxt := ctxt_1 } →
    ref = ref_1 ∧ caller = caller_1 ∧ params = params_1 ∧ callee = callee_1 ∧ args = args_1 ∧ ctxt = ctxt_1
-- Mathlib.Combinatorics.SimpleGraph.Maps
Equiv.symm_simpleGraph : ∀ {V : Type u_1} {W : Type u_2} (e : V ≃ W), e.simpleGraph.symm = e.symm.simpleGraph
-- Init.Data.List.MapIdx
List.mapIdx_eq_nil_iff : ∀ {α : Type u_1} {α_1 : Type u_2} {f : ℕ → α → α_1} {l : List α}, List.mapIdx f l = [] ↔ l = []
-- Mathlib.Algebra.Group.Nat.Even
Nat.not_even_iff : ∀ {n : ℕ}, ¬Even n ↔ n % 2 = 1
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The map `K.opcycles i ⟶ K.X j` induced by the differential `K.d i j`.  -/
HomologicalComplex.fromOpcycles : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) → (i j : ι) → [inst_2 : K.HasHomology i] → K.opcycles i ⟶ K.X j
-- Mathlib.Topology.UniformSpace.Cauchy
totallyBounded_empty : ∀ {α : Type u} [uniformSpace : UniformSpace α], TotallyBounded ∅
-- Mathlib.Order.Atoms
IsCoatom.eq_1 : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : OrderTop α] (a : α), IsCoatom a = (a ≠ ⊤ ∧ ∀ (b : α), a < b → b = ⊤)
-- Mathlib.Algebra.Category.MonCat.Basic
/-- Universe lift functor for commutative monoids.  -/
CommMonCat.uliftFunctor : CategoryTheory.Functor CommMonCat CommMonCat
-- Lean.Elab.MutualInductive
Lean.Elab.Command.instInhabitedInductiveElabStep2.default : Lean.Elab.Command.InductiveElabStep2
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.equiv_mul_left_of_mem : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {T : Set G} (hHT : Subgroup.IsComplement (↑H) T) {h g : G}
  (hh : h ∈ H), hHT.equiv (h * g) = (⟨h, hh⟩ * (hHT.equiv g).1, (hHT.equiv g).2)
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.mapPresheaf_app : ∀ {X : AlgebraicGeometry.Scheme} {M N : X.Modules} (φ : M ⟶ N) (U : (TopologicalSpace.Opens ↥X)ᵒᵖ),
  (AlgebraicGeometry.Scheme.Modules.Hom.mapPresheaf φ).app U =
    AlgebraicGeometry.Scheme.Modules.Hom.app φ (Opposite.unop U)
-- Mathlib.Combinatorics.SimpleGraph.Partition
SimpleGraph.Partition.mem_partOfVertex : ∀ {V : Type u} {G : SimpleGraph V} (P : G.Partition) (v : V), v ∈ P.partOfVertex v
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pos.revSkip?_congr : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s t : String.Slice} (hst : s.copy = t.copy) {pos : s.Pos},
  pos.revSkip? pat = Option.map (fun x => x.cast ⋯) ((pos.cast hst).revSkip? pat)
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthInf_biInf : ∀ {α : Type u_1} (u : α → ℕ → EReal) {s : Set α},
  s.Finite → LinearGrowth.linearGrowthInf (⨅ x ∈ s, u x) = ⨅ x ∈ s, LinearGrowth.linearGrowthInf (u x)
-- Init.Data.Int.DivMod.Lemmas
_private.Init.Data.Int.DivMod.Lemmas.0.Int.fdiv.match_1.eq_6 : ∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (x : ℤ) → motive 0 x)
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n)) (h_3 : (m n : ℕ) → motive (Int.ofNat m.succ) (Int.negSucc n))
  (h_4 : (a : ℕ) → motive (Int.negSucc a) 0) (h_5 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n.succ))
  (h_6 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match Int.negSucc m, Int.negSucc n with
    | 0, x => h_1 x
    | Int.ofNat m, Int.ofNat n => h_2 m n
    | Int.ofNat m.succ, Int.negSucc n => h_3 m n
    | Int.negSucc a, 0 => h_4 a
    | Int.negSucc m, Int.ofNat n.succ => h_5 m n
    | Int.negSucc m, Int.negSucc n => h_6 m n) =
    h_6 m n
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.match_1.eq_5 : ∀ (motive : ByteArray.utf8DecodeChar?.FirstByte → Sort u_1)
  (h_1 :
    ByteArray.utf8DecodeChar?.FirstByte.threeMore = ByteArray.utf8DecodeChar?.FirstByte.invalid →
      motive ByteArray.utf8DecodeChar?.FirstByte.invalid)
  (h_2 :
    ByteArray.utf8DecodeChar?.FirstByte.threeMore = ByteArray.utf8DecodeChar?.FirstByte.done →
      motive ByteArray.utf8DecodeChar?.FirstByte.done)
  (h_3 :
    ByteArray.utf8DecodeChar?.FirstByte.threeMore = ByteArray.utf8DecodeChar?.FirstByte.oneMore →
      motive ByteArray.utf8DecodeChar?.FirstByte.oneMore)
  (h_4 :
    ByteArray.utf8DecodeChar?.FirstByte.threeMore = ByteArray.utf8DecodeChar?.FirstByte.twoMore →
      motive ByteArray.utf8DecodeChar?.FirstByte.twoMore)
  (h_5 :
    ByteArray.utf8DecodeChar?.FirstByte.threeMore = ByteArray.utf8DecodeChar?.FirstByte.threeMore →
      motive ByteArray.utf8DecodeChar?.FirstByte.threeMore),
  (match h : ByteArray.utf8DecodeChar?.FirstByte.threeMore with
    | ByteArray.utf8DecodeChar?.FirstByte.invalid => h_1 h
    | ByteArray.utf8DecodeChar?.FirstByte.done => h_2 h
    | ByteArray.utf8DecodeChar?.FirstByte.oneMore => h_3 h
    | ByteArray.utf8DecodeChar?.FirstByte.twoMore => h_4 h
    | ByteArray.utf8DecodeChar?.FirstByte.threeMore => h_5 h) =
    h_5 ⋯
-- Mathlib.Combinatorics.Additive.FreimanHom
IsAddFreimanIso.subset : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {A₁ A₂ : Set α} {B₁ B₂ : Set β}
  {f : α → β} {n : ℕ}, A₁ ⊆ A₂ → IsAddFreimanIso n A₂ B₂ f → Set.BijOn f A₁ B₁ → IsAddFreimanIso n A₁ B₁ f
-- Init.Data.List.Perm
_private.Init.Data.List.Perm.0.List.getLast?.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectLimit.relMap_equiv_unify : ∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] (G : ι → Type w) [inst_1 : (i : ι) → L.Structure (G i)]
  (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) [inst_2 : IsDirectedOrder ι]
  [DirectedSystem G fun i j h => ⇑(f i j h)] [inst_4 : Nonempty ι] {n : ℕ} (R : L.Relations n)
  (x : Fin n → FirstOrder.Language.Structure.Sigma f) (i : ι) (hi : i ∈ upperBounds (Set.range (Sigma.fst ∘ x))),
  FirstOrder.Language.Structure.RelMap R x =
    FirstOrder.Language.Structure.RelMap R (FirstOrder.Language.DirectLimit.unify f x i hi)
-- Mathlib.Algebra.DirectSum.Module
DirectSum.IsInternal.ofBijective_coeLinearMap_of_ne : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {A : ι → Submodule R M} (h : DirectSum.IsInternal A) {i j : ι},
  i ≠ j → ∀ (x : ↥(A i)), ((LinearEquiv.ofBijective (DirectSum.coeLinearMap A) h).symm ↑x) j = 0
-- Mathlib.GroupTheory.MonoidLocalization.Away
Submonoid.LocalizationMap.AwayMap.lift_eq : ∀ {M : Type u_1} [inst : CommMonoid M] {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3} [inst_2 : CommMonoid P]
  {g : M →* P} (x : M) (F : Submonoid.LocalizationMap.AwayMap x N) (hg : IsUnit (g x)) (a : M),
  (Submonoid.LocalizationMap.AwayMap.lift x F hg) (F a) = g a
-- Init.Data.List.Control
_private.Init.Data.List.Control.0.List.findM?.eq_1 : ∀ {m : Type → Type u} [inst : Monad m] {α : Type} (p : α → m Bool), List.findM? p [] = pure none
-- Mathlib.Topology.Order.OrderClosed
/-- If `α` is a topological space and a preorder, `ClosedIicTopology α` means that `Iic a` is
closed for all `a : α`.  -/
ClosedIicTopology : (α : Type u_1) → [TopologicalSpace α] → [Preorder α] → Prop