mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Environment
/-- Creates environment object from imports and frees compacted regions after calling `act`. No live
references to the environment object or imported objects may exist after `act` finishes. As this
cannot be ruled out after loading environment extensions, `importModules`'s `loadExts` is always
unset using this function.
 -/
Lean.withImportModules : {α : Type} → Array Lean.Import → Lean.Options → (Lean.Environment → IO α) → optParam UInt32 0 → IO α
-- Init.Data.Nat.MinMax
Nat.le_min_of_le_of_le : ∀ {a b c : ℕ}, a ≤ b → a ≤ c → a ≤ min b c
-- Std.Data.ExtTreeMap.Basic
/-- Given a proof that the tree map is not empty, retrieves the smallest key.
 -/
Std.ExtTreeMap.minKey : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → (t : Std.ExtTreeMap α β cmp) → t ≠ ∅ → α
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.id_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  (x : F.DescentData' sq sq₃) (x_1 : ι),
  (CategoryTheory.CategoryStruct.id x).hom x_1 = CategoryTheory.CategoryStruct.id (x.obj x_1)
-- Mathlib.Algebra.Group.Units.Hom
AddUnits.val_zsmul_eq_zsmul_val : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (u : AddUnits α) (n : ℤ), ↑(n • u) = n • ↑u
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem_alter_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : Option β → Option β} {hc : k ∈ t.alter k f}, (t.alter k f)[k] = (f t[k]?).get ⋯
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.fst_prodMkRight : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) (δ : Type u_5) [inst : MeasurableSpace δ],
  (ProbabilityTheory.Kernel.prodMkRight δ κ).fst = ProbabilityTheory.Kernel.prodMkRight δ κ.fst
-- Mathlib.Algebra.Homology.Opposite
/-- The canonical isomorphism `K.op.cycles i ≅ op (K.opcycles i)`.  -/
HomologicalComplex.cyclesOpIso : {ι : Type u_1} →
  {V : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} V] →
      {c : ComplexShape ι} →
        [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
          (K : HomologicalComplex V c) →
            (i : ι) → [inst_2 : K.HasHomology i] → K.op.cycles i ≅ Opposite.op (K.opcycles i)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.le_translationNumber_of_add_le : ∀ (f : CircleDeg1Lift) {z : ℝ}, (∀ (x : ℝ), x + z ≤ f x) → z ≤ f.translationNumber
-- Mathlib.AlgebraicTopology.ModelCategory.Opposite
HomotopicalAlgebra.instHasTwoOutOfThreePropertyOppositeWeakEquivalences : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  [(HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty],
  (HomotopicalAlgebra.weakEquivalences Cᵒᵖ).HasTwoOutOfThreeProperty
-- Mathlib.Algebra.Homology.DerivedCategory.TStructure
DerivedCategory.instIsGEObjCochainComplexIntQOfIsGE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (K : CochainComplex C ℤ) (n : ℤ) [K.IsGE n], (DerivedCategory.Q.obj K).IsGE n
-- Mathlib.Algebra.Torsor.Defs
/-- Adding a group element to a point, then subtracting another point,
produces the same result as subtracting the points then adding the group element.  -/
vadd_vsub_assoc : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] (g : G) (p₁ p₂ : P),
  (g +ᵥ p₁) -ᵥ p₂ = g + (p₁ -ᵥ p₂)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.hom_ext₂_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 2}
  {φ φ' : f ⟶ g},
  φ = φ' ↔
    CategoryTheory.ComposableArrows.app' φ 0 _proof_245✝ = CategoryTheory.ComposableArrows.app' φ' 0 _proof_245✝ ∧
      CategoryTheory.ComposableArrows.app' φ 1 _proof_246✝ = CategoryTheory.ComposableArrows.app' φ' 1 _proof_246✝ ∧
        CategoryTheory.ComposableArrows.app' φ 2 _proof_247✝ = CategoryTheory.ComposableArrows.app' φ' 2 _proof_247✝
-- Lean.ToExpr
Lean.instToExprUInt16 : Lean.ToExpr UInt16
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] {f g : α →*₀ β},
  f = g ↔ ∀ (x : α), f x = g x
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
CategoryTheory.Equivalence.sheafCongrPrecoherent_functor_obj_obj_map : ∀ {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.Precoherent C] (A : Type u_3)
  [inst_3 : CategoryTheory.Category.{v_3, u_3} A] (e : C ≌ D)
  (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A) {X_1 Y : Dᵒᵖ} (f : X_1 ⟶ Y),
  ((CategoryTheory.Equivalence.sheafCongrPrecoherent A e).functor.obj X).obj.map f = X.obj.map (e.inverse.map f.unop).op
-- Mathlib.Algebra.Order.GroupWithZero.Basic
div_le_div_iff₀ : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b c d : G₀},
  0 < b → 0 < d → (a / b ≤ c / d ↔ a * d ≤ c * b)
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.instT1Space : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} {𝓕 : Filter ι} [inst : (i : ι) → TopologicalSpace (R i)]
  [∀ (i : ι), T1Space (R i)], T1Space (RestrictedProduct (fun i => R i) (fun i => A i) 𝓕)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
_private.Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme.0.AlgebraicGeometry.Scheme.IdealSheafData.glueDataT'Aux_snd_ι : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U V W U₀ : ↑X.affineOpens) (hU₀ : ↑U ⊓ ↑W ≤ ↑U₀),
  CategoryTheory.CategoryStruct.comp (I.glueDataT'Aux U V W U₀ hU₀)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (I.glueDataObjι V) (X.homOfLE ⋯))
        (↑V ⊓ ↑U₀).ι) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯))
        (CategoryTheory.Limits.pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯))
        (CategoryTheory.CategoryStruct.comp (I.glueDataObjι U) (↑U).ι))
-- Mathlib.Probability.Moments.Tilted
ProbabilityTheory.integral_tilted_mul_eq_cgf : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} {E : Type u_2}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (g : Ω → E),
  MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ →
    (∫ (ω : Ω), g ω ∂μ.tilted fun x => t * X x) = ∫ (ω : Ω), Real.exp (t * X ω - ProbabilityTheory.cgf X μ t) • g ω ∂μ
-- Mathlib.Algebra.NoZeroSMulDivisors.Defs
instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [IsDomain R] [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [NoZeroSMulDivisors R M], Module.IsTorsionFree R M
-- Mathlib.Topology.Category.TopPair
TopPair.Homotopy.mk.inj : ∀ {X Y : TopPair} {f g : X ⟶ Y} {fst : TopCat.Homotopy (TopPair.Hom.fst f) (TopPair.Hom.fst g)}
  {snd : TopCat.Homotopy (TopPair.Hom.snd f) (TopPair.Hom.snd g)}
  {w :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight TopPair.map TopCat.I)
          fst.h =
        CategoryTheory.CategoryStruct.comp snd.h TopPair.map)
      TopPair.Homotopy.w._autoParam}
  {fst_1 : TopCat.Homotopy (TopPair.Hom.fst f) (TopPair.Hom.fst g)}
  {snd_1 : TopCat.Homotopy (TopPair.Hom.snd f) (TopPair.Hom.snd g)}
  {w_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight TopPair.map TopCat.I)
          fst_1.h =
        CategoryTheory.CategoryStruct.comp snd_1.h TopPair.map)
      TopPair.Homotopy.w._autoParam},
  { fst := fst, snd := snd, w := w } = { fst := fst_1, snd := snd_1, w := w_1 } → fst = fst_1 ∧ snd = snd_1
-- Mathlib.Algebra.FiveLemma
/-- A special case of one four lemma such that the right-most term is zero in terms of (additive)
groups. For a diagram explaining the variables, see the module docstring.  -/
LinearMap.injective_of_surjective_of_injective_of_right_exact : ∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} {N₁ : Type u_7} {N₂ : Type u_8}
  {N₃ : Type u_9} [inst_1 : AddCommGroup M₁] [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup M₃]
  [inst_4 : Module R M₁] [inst_5 : Module R M₂] [inst_6 : Module R M₃] [inst_7 : AddCommGroup N₁]
  [inst_8 : AddCommGroup N₂] [inst_9 : AddCommGroup N₃] [inst_10 : Module R N₁] [inst_11 : Module R N₂]
  [inst_12 : Module R N₃] (f₁ : M₁ →ₗ[R] M₂) (f₂ : M₂ →ₗ[R] M₃) (g₁ : N₁ →ₗ[R] N₂) (g₂ : N₂ →ₗ[R] N₃) (i₁ : M₁ →ₗ[R] N₁)
  (i₂ : M₂ →ₗ[R] N₂) (i₃ : M₃ →ₗ[R] N₃),
  g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁ →
    g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂ →
      Function.Exact ⇑f₁ ⇑f₂ →
        Function.Exact ⇑g₁ ⇑g₂ →
          Function.Surjective ⇑i₁ → Function.Injective ⇑i₂ → Function.Surjective ⇑f₂ → Function.Injective ⇑i₃
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.homogenize_C_mul : ∀ {R : Type u_1} [inst : CommSemiring R] (c : R) (p : Polynomial R) (n : ℕ),
  (Polynomial.C c * p).homogenize n = MvPolynomial.C c * p.homogenize n
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal_add : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [inst : DecidableEq o] [inst_1 : AddZeroClass α]
  (M N : o → Matrix m n α), Matrix.blockDiagonal (M + N) = Matrix.blockDiagonal M + Matrix.blockDiagonal N
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.revMatchesAt_iff_splits : ∀ {pat : String} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.RevMatchesAt pat pos ↔ ∃ t₁ t₂, pos.Splits (t₁ ++ pat) t₂
-- Mathlib.Order.Interval.Set.WithBotTop
WithBot.preimage_coe_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, WithBot.some ⁻¹' Set.Iic ↑a = Set.Iic a
-- Init.Internal.Order.MonadTail
Lean.Order.instMonadTailOptionT : {m : Type u → Type v} → [inst : Monad m] → [Lean.Order.MonadTail m] → Lean.Order.MonadTail (OptionT m)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
cfc_mem_elemental : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : Ring A] [inst_2 : StarRing A]
  [inst_3 : Algebra 𝕜 A] [inst_4 : TopologicalSpace A] [inst_5 : StarModule 𝕜 A]
  [inst_6 : ContinuousFunctionalCalculus 𝕜 A p] [inst_7 : IsTopologicalRing A] [inst_8 : ContinuousStar A] (f : 𝕜 → 𝕜)
  (a : A), cfc f a ∈ StarAlgebra.elemental 𝕜 a
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.insertListₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β),
  m.insertListₘ [] = m
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_comp_exp : Real.log ∘ Real.exp = id
-- Mathlib.Algebra.GroupWithZero.Action.Defs
AddGroup.intSMulWithZero : {A : Type u_7} → [inst : AddGroup A] → SMulWithZero ℤ A
-- Mathlib.Data.Nat.Digits.Defs
Nat.digitsAux_zero : ∀ (b : ℕ) (h : 2 ≤ b), b.digitsAux h 0 = []
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.coe_op : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : Subalgebra R A), ↑S.op = MulOpposite.unop ⁻¹' ↑S
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.isFirstVarDoneTransition : Lean.Meta.Match.Problem → Bool
-- Lean.Parser.Basic
/-- Raw strings have the syntax `r##...#"..."#...##` with zero or more `#`'s.
If we are looking at a valid start to a raw string (`r##...#"`),
returns true.
We assume `i` begins at the position immediately after `r`.
 -/
Lean.Parser.isRawStrLitStart : Lean.Parser.ParserContext → String.Pos.Raw → Bool
-- Mathlib.Algebra.Opposites
MulOpposite.forall : ∀ {α : Type u_1} {p : αᵐᵒᵖ → Prop}, (∀ (a : αᵐᵒᵖ), p a) ↔ ∀ (a : α), p (MulOpposite.op a)
-- Init.SizeOf
Lean.SourceInfo.original.sizeOf_spec : ∀ (leading : Substring.Raw) (pos : String.Pos.Raw) (trailing : Substring.Raw) (endPos : String.Pos.Raw),
  sizeOf (Lean.SourceInfo.original leading pos trailing endPos) =
    1 + sizeOf leading + sizeOf pos + sizeOf trailing + sizeOf endPos
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.ExtraTheorem.fvar.sizeOf_spec : ∀ (fvarId : Lean.FVarId), sizeOf (Lean.Elab.Tactic.Grind.ExtraTheorem.fvar fvarId) = 1 + sizeOf fvarId
-- Init.Prelude
/-- Extracts a wrapped value from a universe-lifted type.  -/
ULift.down : {α : Type s} → ULift.{r, s} α → α
-- Mathlib.Data.Set.Order
Set.monotoneOn_iff_monotone : ∀ {α : Type u} {β : Type v} {s : Set α} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  MonotoneOn f s ↔ Monotone fun a => f ↑a
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_sub_nat' : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {b : H} [inst_1 : AddGroupWithOne G]
  [inst_2 : AddGroup H] [AddConstMapClass F G H 1 b] (f : F) (x : G) (n : ℕ), f (x - ↑n) = f x - n • b
-- Qq.Macro
Qq.Impl.makeZetaReduce : Lean.FVarId → Lean.Expr → Lean.MetaM (Option Lean.LocalContext)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.compare_getKey_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (h' : k ∈ t), cmp (t.getKey k h') k = Ordering.eq
-- Batteries.Util.ProofWanted
_private.Batteries.Util.ProofWanted.0.WantedCmdKind.mk : String → Lean.Name → Bool → Bool → WantedCmdKind✝
-- Mathlib.Algebra.Polynomial.RingDivision
Irreducible.aeval_ne_zero_of_natDegree_ne_one : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [IsDomain R] [inst_2 : Ring S] [inst_3 : Algebra R S] [FaithfulSMul R S]
  {p : Polynomial R},
  Irreducible p → p.natDegree ≠ 1 → ∀ {x : S}, x ∈ (algebraMap R S).range → (Polynomial.aeval x) p ≠ 0
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
MulAction.isPreprimitive_of_fixingSubgroup_empty_iff : ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α],
  MulAction.IsPreprimitive ↥(fixingSubgroup G ∅) ↥(SubMulAction.ofFixingSubgroup G ∅) ↔ MulAction.IsPreprimitive G α
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_union_Ico : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] {a b c d : α},
  min a b ≤ max c d → min c d ≤ max a b → Finset.Ico a b ∪ Finset.Ico c d = Finset.Ico (min a c) (max b d)
-- Lean.Elab.Quotation
/-- Adapt alternatives that do not introduce new discriminants in `doMatch`, but are covered by those that do so.  -/
_private.Lean.Elab.Quotation.0.Lean.Elab.Term.Quotation.noOpMatchAdaptPats : Lean.Elab.Term.Quotation.HeadCheck → Lean.Elab.Term.Quotation.Alt → Lean.Elab.Term.Quotation.Alt
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- If the right extension defined by `α : F₀ ⟶ L ⋙ F₁` is universal,
then for every `L' : D ⥤ D'`, `F₁ : D ⥤ H`, if an extension
`b : L'.LeftExtension F₁` is universal, so is the "pasted" extension
`(LeftExtension.precomp₂ L' α).obj b`.  -/
CategoryTheory.Functor.LeftExtension.isUniversalPrecomp₂ : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      {D' : Type u_5} →
        [inst : CategoryTheory.Category.{v_1, u_1} C] →
          [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
            [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
              [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] →
                {L : CategoryTheory.Functor C D} →
                  {L' : CategoryTheory.Functor D D'} →
                    {F₀ : CategoryTheory.Functor C H} →
                      {F₁ : CategoryTheory.Functor D H} →
                        (α : F₀ ⟶ L.comp F₁) →
                          CategoryTheory.StructuredArrow.IsUniversal (CategoryTheory.Functor.LeftExtension.mk F₁ α) →
                            {b : L'.LeftExtension F₁} →
                              CategoryTheory.StructuredArrow.IsUniversal b →
                                CategoryTheory.StructuredArrow.IsUniversal
                                  ((CategoryTheory.Functor.LeftExtension.precomp₂ L' α).obj b)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.rightHomologyι_descOpcycles_π_eq_zero_of_boundary_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) {A : C} (k : S.X₂ ⟶ A) [inst_2 : S.HasRightHomology] (x : S.X₃ ⟶ A)
  (hx : k = CategoryTheory.CategoryStruct.comp S.g x) {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.rightHomologyι (CategoryTheory.CategoryStruct.comp (S.descOpcycles k ⋯) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
/-- The dimension `c.dim` of a cell `c` of a rank function for a
pairing `P` of a subcomplex of a simplicial set. This is defined
as the dimension of the corresponding type (II) simplex.
(In the case `P` is proper, the corresponding type (I) simplex
will be of dimension `c.dim + 1`.)  -/
SSet.Subcomplex.Pairing.RankFunction.Cell.dim : {X : SSet} →
  {A : X.Subcomplex} →
    {P : A.Pairing} → {ι : Type v} → [inst : LinearOrder ι] → {f : P.RankFunction ι} → {i : ι} → f.Cell i → ℕ
-- Mathlib.Data.Nat.Count
/-- Count the number of naturals `k < n` satisfying `p k`.  -/
Nat.count : (p : ℕ → Prop) → [DecidablePred p] → ℕ → ℕ
-- Mathlib.Algebra.Order.Ring.Synonym
Lex.instNonUnitalRing : {R : Type u_1} → [NonUnitalRing R] → NonUnitalRing (Lex R)
-- Mathlib.Data.ENat.Basic
ENat.WithBot.one_add_cancel : ∀ {a b : WithBot ℕ∞}, 1 + a = 1 + b ↔ a = b
-- Lean.Language.Lean.Types
Lean.Language.Lean.instNonemptyCommandElaboratingSnapshot : Nonempty Lean.Language.Lean.CommandElaboratingSnapshot
-- Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
/-- The infinite adele ring is locally compact.  -/
NumberField.InfiniteAdeleRing.locallyCompactSpace : ∀ (K : Type u_1) [inst : Field K] [NumberField K], LocallyCompactSpace (NumberField.InfiniteAdeleRing K)
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.restrict_iInf : ∀ {α : Type u_1} {ι : Sort u_2} [Nonempty ι] (s : Set α) (m : ι → MeasureTheory.OuterMeasure α),
  (MeasureTheory.OuterMeasure.restrict s) (⨅ i, m i) = ⨅ i, (MeasureTheory.OuterMeasure.restrict s) (m i)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_diff_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α} {fallback : β}, k ∉ m₁ → (m₁ \ m₂).getD k fallback = fallback
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.disjoint_toSubmodule : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {N N' : LieSubmodule R L M}, Disjoint ↑N ↑N' ↔ Disjoint N N'
-- Mathlib.Data.Set.Card
Set.inj_on_of_surj_on_of_ncard_le : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (f : (a : α) → a ∈ s → β),
  (∀ (a : α) (ha : a ∈ s), f a ha ∈ t) →
    (∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b) →
      s.ncard ≤ t.ncard →
        ∀ ⦃a₁ : α⦄ (ha₁ : a₁ ∈ s) ⦃a₂ : α⦄ (ha₂ : a₂ ∈ s),
          f a₁ ha₁ = f a₂ ha₂ → autoParam s.Finite Set.inj_on_of_surj_on_of_ncard_le._auto_1 → a₁ = a₂
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
RingSeminorm.eq_zero_iff : ∀ {R : Type u_1} [inst : NonUnitalRing R] {p : RingSeminorm R}, p = 0 ↔ ∀ (x : R), p x = 0
-- Mathlib.Algebra.Order.Group.Cone
Submonoid.oneLE.congr_simp : ∀ (M : Type u_1) [inst : Monoid M] [inst_1 : Preorder M] [inst_2 : MulLeftMono M], Submonoid.oneLE M = Submonoid.oneLE M
-- Mathlib.Topology.MetricSpace.Holder
HolderOnWith.comp_holderWith : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y]
  [inst_2 : PseudoEMetricSpace Z] {Cg rg : NNReal} {g : Y → Z} {t : Set Y},
  HolderOnWith Cg rg g t →
    ∀ {Cf rf : NNReal} {f : X → Y},
      HolderWith Cf rf f → (∀ (x : X), f x ∈ t) → HolderWith (Cg * Cf ^ ↑rg) (rg * rf) (g ∘ f)
-- Mathlib.Logic.Basic
forall₂_imp : ∀ {α : Sort u_1} {β : α → Sort u_2} {p q : (a : α) → β a → Prop},
  (∀ (a : α) (b : β a), p a b → q a b) → (∀ (a : α) (b : β a), p a b) → ∀ (a : α) (b : β a), q a b
-- Mathlib.Order.WithBot
/-- A version of `bot_lt_iff_ne_bot` for `WithBot` that only requires `LT α`, not
`PartialOrder α`.  -/
WithBot.bot_lt_iff_ne_bot : ∀ {α : Type u_1} [inst : LT α] {x : WithBot α}, ⊥ < x ↔ x ≠ ⊥
-- Lean.DocString.Formatter
_private.Lean.DocString.Formatter.0.Lean.Doc.Parser.versoSyntaxToString'.nl : ReaderT ℕ (StateM String) Unit
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.DirectLimit.instDirectedSystemSubtypeMemSubstructureDomCoeOrderHomPartialEquivEmbeddingInclusion : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] {ι : Type u_1}
  [inst_2 : Preorder ι] (S : ι →o L.PartialEquiv M N),
  DirectedSystem (fun i => ↥(S i).dom) fun x x_1 h => ⇑(FirstOrder.Language.Substructure.inclusion ⋯)
-- Init.Data.Float.Model.Format.Basic
Float.Model.Format.mk.inj : ∀ {mantissaBitsWithoutImplicit : ℕ} {hm : autoParam (0 < mantissaBitsWithoutImplicit) Float.Model.Format.hm._autoParam}
  {exponentBits : ℕ} {he : autoParam (0 < exponentBits) Float.Model.Format.he._autoParam}
  {mantissaBitsWithoutImplicit_1 : ℕ}
  {hm_1 : autoParam (0 < mantissaBitsWithoutImplicit_1) Float.Model.Format.hm._autoParam} {exponentBits_1 : ℕ}
  {he_1 : autoParam (0 < exponentBits_1) Float.Model.Format.he._autoParam},
  { mantissaBitsWithoutImplicit := mantissaBitsWithoutImplicit, hm := hm, exponentBits := exponentBits, he := he } =
      { mantissaBitsWithoutImplicit := mantissaBitsWithoutImplicit_1, hm := hm_1, exponentBits := exponentBits_1,
        he := he_1 } →
    mantissaBitsWithoutImplicit = mantissaBitsWithoutImplicit_1 ∧ exponentBits = exponentBits_1
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- The contravariant functor turning comonoid objects into monoid objects in the opposite category.
 -/
CategoryTheory.Comon.ComonToMonOpOp : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.Functor (CategoryTheory.Comon C) (CategoryTheory.Mon Cᵒᵖ)ᵒᵖ
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- The restriction of a module along an open immersion.  -/
AlgebraicGeometry.Scheme.Modules.restrict : {X Y : AlgebraicGeometry.Scheme} → Y.Modules → (f : X ⟶ Y) → [AlgebraicGeometry.IsOpenImmersion f] → X.Modules
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.insertManyIfNewUnit_list_equiv_foldl : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α Unit} {l : List α},
  m.WF → (m.insertManyIfNewUnit l).Equiv (List.foldl (fun acc a => acc.insertIfNew a ()) m l)
-- Mathlib.Data.Num.ZNum
ZNum.pred.eq_2 : ∀ (a : PosNum), (ZNum.pos a).pred = a.pred'.toZNum
-- Mathlib.RingTheory.IntegralDomain
/-- A finite subgroup of the unit group of an integral domain is cyclic.  -/
isCyclic_of_injective_ringHom : ∀ {R : Type u_1} {G : Type u_2} [inst : CommRing R] [IsDomain R] [inst_2 : Group G] [Finite G] (f : G →* R),
  Function.Injective ⇑f → IsCyclic G
-- Mathlib.Algebra.Regular.SMul
/-- One is always `M`-regular.  -/
IsSMulRegular.one : ∀ {R : Type u_1} (M : Type u_3) [inst : Monoid R] [inst_1 : MulAction R M], IsSMulRegular M 1
-- Mathlib.Data.Finset.Defs
Finset.Subset.rfl : ∀ {α : Type u_1} {s : Finset α}, s ⊆ s