mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
/-- Construct a simplicial complex by removing the empty face for you.  -/
Geometry.SimplicialComplex.ofErase : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : Ring 𝕜] →
      [inst_1 : PartialOrder 𝕜] →
        [inst_2 : AddCommGroup E] →
          [inst_3 : Module 𝕜 E] →
            (faces : Set (Finset E)) →
              (∀ s ∈ faces, AffineIndependent 𝕜 Subtype.val) →
                IsLowerSet faces →
                  (∀ s ∈ faces, ∀ t ∈ faces, (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) (↑s ∩ ↑t)) →
                    Geometry.SimplicialComplex 𝕜 E
-- Mathlib.CategoryTheory.Functor.Derived.Adjunction
CategoryTheory.Adjunction.derived_unit : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁}
  (adj : G ⊣ F) {L₁ : CategoryTheory.Functor C₁ D₁} {L₂ : CategoryTheory.Functor C₂ D₂}
  (W₁ : CategoryTheory.MorphismProperty C₁) (W₂ : CategoryTheory.MorphismProperty C₂) [inst_4 : L₁.IsLocalization W₁]
  [inst_5 : L₂.IsLocalization W₂] {G' : CategoryTheory.Functor D₁ D₂} {F' : CategoryTheory.Functor D₂ D₁}
  (α : L₁.comp G' ⟶ G.comp L₂) (β : F.comp L₁ ⟶ L₂.comp F') [inst_6 : G'.IsLeftDerivedFunctor α W₁]
  [inst_7 : F'.IsRightDerivedFunctor β W₂]
  [inst_8 :
    (G'.comp F').IsLeftDerivedFunctor
      (CategoryTheory.CategoryStruct.comp (L₁.associator G' F').inv (CategoryTheory.Functor.whiskerRight α F')) W₁]
  [inst_9 :
    (F'.comp G').IsRightDerivedFunctor
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight β G') (L₂.associator F' G').hom) W₂],
  (adj.derived W₁ W₂ α β).unit = adj.derivedη W₁ α β
-- Init.Grind.Lemmas
Lean.Grind.eq_false_of_not_eq_true : ∀ {a : Prop}, (¬a) = True → a = False
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.toSubmodule_comap : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : TopologicalSpace M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : TopologicalSpace N]
  [inst_6 : Module R N] (f : M →L[R] N) (s : ClosedSubmodule R N), ↑(ClosedSubmodule.comap f s) = Submodule.comap ↑f ↑s
-- Mathlib.Order.Ideal
/-- Create an element of type `Order.Ideal` from a set satisfying the predicate
`Order.IsIdeal`.  -/
Order.IsIdeal.toIdeal : {P : Type u_1} → [inst : LE P] → {I : Set P} → Order.IsIdeal I → Order.Ideal P
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.subarrayMeasure_toSubarray_eq : ∀ {α : Type u_1} {β : Type u_2} (nes : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))),
  Lean.PersistentHashMap.subarrayMeasure nes.toSubarray = (Lean.PersistentHashMap.Node.entries nes).measure
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
CFC.quasispectrum_zero_eq : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p], quasispectrum R 0 = {0}
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.findSomeRevM?.find.eq_def : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : α → m (Option β)) (as : Array α) (i : ℕ)
  (a : i ≤ as.size),
  Array.findSomeRevM?.find✝ f as i a =
    match i, a with
    | 0, x => pure none
    | i.succ, h =>
      have this := ⋯;
      do
      let r ← f as[i]
      match r with
        | some val => pure r
        | none =>
          have this := ⋯;
          Array.findSomeRevM?.find✝ f as i this
-- ProofWidgets.Component.RefreshComponent
/-- If any updates are available (i.e., the server-side state is more recent than the client's),
immediately return the most recent version of the HTML tree.
Otherwise await the next update.
Returns `none` if the client's state is the last one that should be shown.  -/
ProofWidgets.RefreshComponent.awaitRefresh : ProofWidgets.RefreshComponent.AwaitRefreshParams →
  Lean.Server.RequestM (Lean.Server.RequestTask (Option ProofWidgets.RefreshComponent.VersionedHtml))
-- Mathlib.Probability.Kernel.Invariance
ProbabilityTheory.Kernel.Invariant.comp_const : ∀ {α : Type u_1} {mα : MeasurableSpace α} {κ : ProbabilityTheory.Kernel α α} {μ : MeasureTheory.Measure α},
  κ.Invariant μ → κ.comp (ProbabilityTheory.Kernel.const α μ) = ProbabilityTheory.Kernel.const α μ
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakKernels
CategoryTheory.Limits.weakKernel.condition : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasWeakKernel f],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.weakKernel.ι f) f = 0
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
CliffordAlgebraQuaternion.i_quaternionBasis : ∀ {R : Type u_1} [inst : CommRing R] (c₁ c₂ : R),
  (CliffordAlgebraQuaternion.quaternionBasis c₁ c₂).i = (CliffordAlgebra.ι (CliffordAlgebraQuaternion.Q c₁ c₂)) (1, 0)
-- Mathlib.RingTheory.Adjoin.Field
minpoly_sub_algebraMap_splits : ∀ {K : Type u_2} {L : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {x : L} (r : K),
  (Polynomial.map (algebraMap K L) (minpoly K x)).Splits →
    (Polynomial.map (algebraMap K L) (minpoly K (x - (algebraMap K L) r))).Splits
-- Init.Data.Array.Lemmas
Array.sum_eq_foldr : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Zero α] {xs : Array α}, xs.sum = Array.foldr (fun x1 x2 => x1 + x2) 0 xs
-- Mathlib.Data.List.Cycle
List.isRotated_next_eq : ∀ {α : Type u_1} [inst : DecidableEq α] {l l' : List α} (h : l ~r l'),
  l.Nodup → ∀ {x : α} (hx : x ∈ l), l.next x hx = l'.next x ⋯
-- Init.Data.List.Nat.Erase
List.eraseIdx_length_sub_one : ∀ {α : Type u_1} {l : List α}, l.eraseIdx (l.length - 1) = l.dropLast
-- Mathlib.Tactic.DefEqAbuse
/-- Find the deepest `Meta.isDefEq` transition points: nodes that fail in the strict trace
but whose check string appears as a success in the permissive trace and does NOT also appear
as a failure in the permissive trace (which would indicate the check is context-dependent
rather than transparency-dependent).
A "deepest transition point" has no descendant transition points.
Falls back to `findLeafFailures` behavior when `permSuccesses` is empty.  -/
_private.Mathlib.Tactic.DefEqAbuse.0.Mathlib.Tactic.DefEqAbuse.findTransitionFailures : Std.HashSet String → Std.HashSet String → Lean.MessageData → BaseIO (Array Lean.MessageData)
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.prodAux.eq_2 : ∀ {M : Type u_6} [inst : Monoid M] (x_1 : M) (xs : List M),
  FreeMonoid.prodAux (x_1 :: xs) = List.foldl (fun x1 x2 => x1 * x2) x_1 xs
-- Mathlib.Logic.Hydra
Relation.cutExpand_singleton_singleton : ∀ {α : Type u_1} {r : α → α → Prop} {x' x : α}, r x' x → Relation.CutExpand r {x'} {x}
-- Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
CategoryTheory.LocallyDiscrete.categoryStruct : {C : Type u} →
  [CategoryTheory.CategoryStruct.{v, u} C] → CategoryTheory.CategoryStruct.{v, u} (CategoryTheory.LocallyDiscrete C)
-- Mathlib.GroupTheory.PGroup
IsPGroup.index : ∀ {p : ℕ} {G : Type u_1} [inst : Group G],
  IsPGroup p G → ∀ [hp : Fact (Nat.Prime p)] (H : Subgroup G) [H.FiniteIndex], ∃ n, H.index = p ^ n
-- Mathlib.Data.Finset.Defs
Finset.decidableMem : {α : Type u_1} → [_h : DecidableEq α] → (a : α) → (s : Finset α) → Decidable (a ∈ s)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.skipPrefixWhile_eq_iff : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  (s : String.Slice) (res : s.Pos),
  s.skipPrefixWhile pat = res ↔
    String.Slice.Pattern.Model.IsLongestMatchAtChain pat s.startPos res ∧
      (¬String.Slice.Pattern.Model.MatchesAt pat res ∨ String.Slice.Pattern.Model.IsLongestMatchAt pat res res)
-- Mathlib.Topology.Order.MonotoneConvergence
/-- **Alias** of `tendsto_atTop_of_monotone`. -/
tendsto_of_monotone : ∀ {ι : Type u_3} {α : Type u_4} [inst : Preorder ι] [inst_1 : TopologicalSpace α]
  [inst_2 : ConditionallyCompleteLinearOrder α] [OrderTopology α] {f : ι → α},
  Monotone f → Filter.Tendsto f Filter.atTop Filter.atTop ∨ ∃ l, Filter.Tendsto f Filter.atTop (nhds l)
-- Mathlib.Algebra.Order.Group.OrderIso
inv_le' : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulLeftMono α] [MulRightMono α] {a b : α}, a⁻¹ ≤ b ↔ b⁻¹ ≤ a
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A cokernel cofork for the cokernel of `BinaryBicone.inl`. It consists of the morphism
`BinaryBicone.snd`.  -/
CategoryTheory.Limits.BinaryBicone.inlCokernelCofork : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} → (c : CategoryTheory.Limits.BinaryBicone X Y) → CategoryTheory.Limits.CokernelCofork c.inl
-- Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Polynomial.cardPowDegree_zero : ∀ {Fq : Type u_1} [inst : Field Fq] [inst_1 : Fintype Fq], Polynomial.cardPowDegree 0 = 0
-- Mathlib.Algebra.Star.Basic
/-- `star` skew-distributes over multiplication.  -/
StarMul.star_mul : ∀ {R : Type u} {inst : Mul R} [self : StarMul R] (r s : R), star (r * s) = star s * star r
-- Mathlib.CategoryTheory.Types.Basic
/-- Typecheck a function as a morphism in `Type`.  -/
TypeCat.ofHom : {X Y : Type u} → (X → Y) → (X ⟶ Y)
-- Mathlib.Data.Int.Bitwise
/-- Connection of `HShiftLeft Int Int Int` and `HShiftLeft Int Nat Int`.  -/
Int.shiftLeft_natCast_right : ∀ (m : ℤ) (n : ℕ), m <<< ↑n = m <<< n
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.Functor.isoCopyObj_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (obj : C → D) (e : (X : C) → F.obj X ≅ obj X) (X : C),
  (F.isoCopyObj obj e).hom.app X = (e X).hom
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
/-- **Alias** of the reverse direction of `mdifferentiableWithinAt_iff_differentiableWithinAt`.

---

For maps between vector spaces, `MDifferentiableWithinAt` and `DifferentiableWithinAt`
coincide  -/
DifferentiableWithinAt.mdifferentiableWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {f : E → E'}
  {s : Set E} {x : E}, DifferentiableWithinAt 𝕜 f s x → MDiffAt[s] f x
-- Mathlib.Algebra.Category.MonCat.Colimits
/-- The setoid corresponding to monoid expressions modulo monoid relations and identifications.
 -/
MonCat.Colimits.colimitSetoid : {J : Type v} →
  [inst : CategoryTheory.Category.{u, v} J] →
    (F : CategoryTheory.Functor J MonCat) → Setoid (MonCat.Colimits.Prequotient F)
-- Mathlib.Util.AtLocation
Mathlib.Tactic.instInhabitedBehaviorIfUnchanged.default : Mathlib.Tactic.BehaviorIfUnchanged
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_maxKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.isEmpty = false → ∀ {fallback : α}, t.getKey! (t.maxKeyD fallback) = t.maxKeyD fallback
-- Mathlib.Data.Finset.PImage
Part.toFinset.congr_simp : ∀ {α : Type u_1} (o o_1 : Part α),
  o = o_1 → ∀ {inst : Decidable o.Dom} [inst_1 : Decidable o_1.Dom], o.toFinset = o_1.toFinset
-- Mathlib.Data.Finset.Image
Finset.coe_filterMap : ∀ {α : Type u_1} {β : Type u_2} (f : α → Option β) {s : Finset α} {f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'},
  ↑(Finset.filterMap f s f_inj) = {b | ∃ a ∈ s, f a = some b}
-- Mathlib.Data.Set.Insert
Set.ofPred_eq_eq_singleton : ∀ {α : Type u_1} {a : α}, {n | n = a} = {a}
-- Mathlib.RingTheory.Polynomial.Content
/-- A polynomial is primitive when the only constant polynomials dividing it are units.
Note: This has nothing to do with minimal polynomials of primitive elements in finite fields.  -/
Polynomial.IsPrimitive : {R : Type u_1} → [inst : CommSemiring R] → Polynomial R → Prop
-- Mathlib.Data.DFinsupp.Defs
/-- The support of a dependent function with finite support (aka `DFinsupp`).  -/
DFinsupp.support' : {ι : Type u} →
  {β : ι → Type v} →
    [inst : (i : ι) → Zero (β i)] → (self : DFinsupp β) → Trunc { s // ∀ (i : ι), i ∈ s ∨ self.toFun i = 0 }
-- Mathlib.Topology.UniformSpace.Cauchy
/-- The union of two sets is totally bounded
if and only if each of the two sets is totally bounded.  -/
totallyBounded_union : ∀ {α : Type u} [uniformSpace : UniformSpace α] {s t : Set α},
  TotallyBounded (s ∪ t) ↔ TotallyBounded s ∧ TotallyBounded t
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- An iso `α ≃+ β` can equivalently be viewed as an iso `αᵐᵒᵖ ≃+ βᵐᵒᵖ`.  -/
AddEquiv.mulOp : {α : Type u_3} → {β : Type u_4} → [inst : Add α] → [inst_1 : Add β] → α ≃+ β ≃ (αᵐᵒᵖ ≃+ βᵐᵒᵖ)
-- Mathlib.Order.Interval.Finset.Defs
WithTop.top_mem_insertTop : ∀ {α : Type u_1} {s : Finset α}, ⊤ ∈ WithTop.insertTop s
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.eval_X_toTupleMvPolynomial_zero_eq : ∀ {R : Type u_1} [inst : CommSemiring R] (p : Polynomial R),
  (MvPolynomial.aeval ![Polynomial.X, 1]) (p.toTupleMvPolynomial 0) =
    p * (MvPolynomial.aeval ![Polynomial.X, 1]) (p.toTupleMvPolynomial 1)
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.instInhabitedStdWall : Inhabited Std.Time.TimeZone.StdWall
-- Mathlib.CategoryTheory.Comma.LocallySmall
CategoryTheory.Over.locallySmall : ∀ {T : Type u₃} [inst : CategoryTheory.Category.{v₃, u₃} T] (X : T) [CategoryTheory.LocallySmall.{w, v₃, u₃} T],
  CategoryTheory.LocallySmall.{w, v₃, max u₃ v₃} (CategoryTheory.Over X)
-- Mathlib.Topology.Algebra.AsymptoticCone
Filter.Tendsto.atTop_smul_const_tendsto_asymptoticNhds : ∀ {k : Type u_1} {V : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : TopologicalSpace V] {α : Type u_4} {l : Filter α} [inst_5 : TopologicalSpace k]
  [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] {f : α → k} (v : V),
  Filter.Tendsto f l Filter.atTop → Filter.Tendsto (fun x => f x • v) l (AffineSpace.asymptoticNhds k V v)
-- Mathlib.Order.RelSeries
RelSeries.rel_or_eq_of_le : ∀ {α : Type u_1} {r : SetRel α α} [r.IsTrans] (x : RelSeries r) {i j : Fin (x.length + 1)},
  i ≤ j → (x.toFun i, x.toFun j) ∈ r ∨ x.toFun i = x.toFun j
-- Mathlib.CategoryTheory.Adhesive.Basic
CategoryTheory.Adhesive.isPushout_isPullback_isPullback_hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
  [CategoryTheory.Adhesive C] [CategoryTheory.Mono f],
  CategoryTheory.IsPushout f g h i →
    ∀ {X' Y' Z' : C} {h' : X' ⟶ Z'} {i' : Y' ⟶ Z'} {αX : X' ⟶ X} {αY : Y' ⟶ Y} {αZ : Z' ⟶ Z} {W : C} {f₁ f₂ : Z' ⟶ W},
      CategoryTheory.IsPullback h' αX αZ h →
        CategoryTheory.IsPullback i' αY αZ i →
          CategoryTheory.CategoryStruct.comp h' f₁ = CategoryTheory.CategoryStruct.comp h' f₂ →
            CategoryTheory.CategoryStruct.comp i' f₁ = CategoryTheory.CategoryStruct.comp i' f₂ → f₁ = f₂
-- Mathlib.RingTheory.Noetherian.Basic
/-- If `P × N` embeds into `N` for some nontrivial module `P`, then `N` cannot be a Noetherian
module. Lemma 1.36 of Chapter 1 in [lam_1999].  -/
IsNoetherian.subsingleton_of_injective : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [IsNoetherian R M]
  {P : Type u_5} [inst_4 : AddCommMonoid P] [inst_5 : Module R P] {f : P × M →ₗ[R] M},
  Function.Injective ⇑f → Subsingleton P
-- Mathlib.Order.OrdContinuous
RightOrdContinuous.map_sInf : ∀ {α : Type u} {β : Type v} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] {f : α → β},
  RightOrdContinuous f → ∀ {s : Set α}, s.Nonempty → f (sInf s) = ⨅ x ∈ s, f x
-- Mathlib.Algebra.Order.Group.Synonym
toDual_zero : ∀ {α : Type u_1} [inst : Zero α], OrderDual.toDual 0 = 0
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- The inner product of two unit vectors is greater than or equal to `-1`.  -/
neg_one_le_real_inner_of_norm_eq_one : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x y : F},
  ‖x‖ = 1 → ‖y‖ = 1 → -1 ≤ inner ℝ x y
-- Mathlib.CategoryTheory.Monad.Kleisli
/-- The co-Kleisli category on a comonad `U`.  -/
CategoryTheory.Cokleisli.category : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (U : CategoryTheory.Comonad C) → CategoryTheory.Category.{v, u} (CategoryTheory.Cokleisli U)
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.isUnit_leadingCoeff : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : Field R] {f : MvPolynomial σ R},
  IsUnit (m.leadingCoeff f) ↔ f ≠ 0
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.Fan.op.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C}
  (f : CategoryTheory.Limits.Fan Z), f.op = CategoryTheory.Limits.Cofan.mk (Opposite.op f.pt) fun a => (f.proj a).op
-- Init.Data.String.Termination
String.Pos.Down.mk.injEq : ∀ {s : String} (inner inner_1 : s.Pos), ({ inner := inner } = { inner := inner_1 }) = (inner = inner_1)
-- Mathlib.RingTheory.Extension.Generators
/-- The composition of two homs.  -/
Algebra.Generators.Hom.comp : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            {P : Algebra.Generators R S ι} →
              {R' : Type u_1} →
                {S' : Type u_2} →
                  {ι' : Type u_3} →
                    [inst_3 : CommRing R'] →
                      [inst_4 : CommRing S'] →
                        [inst_5 : Algebra R' S'] →
                          {P' : Algebra.Generators R' S' ι'} →
                            {R'' : Type u_4} →
                              {S'' : Type u_5} →
                                {ι'' : Type u_6} →
                                  [inst_6 : CommRing R''] →
                                    [inst_7 : CommRing S''] →
                                      [inst_8 : Algebra R'' S''] →
                                        {P'' : Algebra.Generators R'' S'' ι''} →
                                          [inst_9 : Algebra R' R''] →
                                            [inst_10 : Algebra R' S''] →
                                              [inst_11 : Algebra S S'] →
                                                [inst_12 : Algebra S' S''] →
                                                  [inst_13 : Algebra S S''] →
                                                    [IsScalarTower R' R'' S''] →
                                                      [IsScalarTower R' S' S''] →
                                                        [IsScalarTower S S' S''] → P'.Hom P'' → P.Hom P' → P.Hom P''
-- Mathlib.CategoryTheory.Filtered.Basic
/-- If Cᵒᵖ is filtered or empty, then C is cofiltered or empty.  -/
CategoryTheory.isCofilteredOrEmpty_of_isFilteredOrEmpty_op : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty Cᵒᵖ],
  CategoryTheory.IsCofilteredOrEmpty C
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- The topology on `α →ᵇ β` is exactly the topology induced by the natural map to `α →ᵤ β`.  -/
BoundedContinuousFunction.isInducing_coeFn : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β],
  Topology.IsInducing (⇑UniformFun.ofFun ∘ DFunLike.coe)
-- Init.Data.UInt.Lemmas
UInt64.neg_inj : ∀ {a b : UInt64}, -a = -b ↔ a = b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.beq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] [inst_1 : (k : α) → BEq (β k)] [∀ (k : α), ReflBEq (β k)],
  m₁.WF → m₂.WF → m₁.Equiv m₂ → m₁.beq m₂ = true
-- Mathlib.AlgebraicTopology.ModelCategory.Over
HomotopicalAlgebra.instHasTwoOutOfThreePropertyOverWeakEquivalences : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (S : C)
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [(HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty],
  (HomotopicalAlgebra.weakEquivalences (CategoryTheory.Over S)).HasTwoOutOfThreeProperty
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend.homologyData_right : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι}
  {i' j' k' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hi' : c'.prev j' = i') (hk : c.next j = k)
  (hk' : c'.next j' = k') (h : (K.sc' i j k).HomologyData),
  (HomologicalComplex.extend.homologyData K e hj' hi hi' hk hk' h).right =
    HomologicalComplex.extend.rightHomologyData K e hj' hi hi' hk hk' h.right
-- Mathlib.Order.BoundedOrder.Basic
bot_lt_iff_ne_bot : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, ⊥ < a ↔ a ≠ ⊥
-- Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
/-- A reformulation of the canonical isomorphism
`toKaroubi (ChainComplex C ℕ) ⋙ Γ₂ ≅ Γ ⋙ toKaroubi (SimplicialObject C)`.  -/
CategoryTheory.Idempotents.DoldKan.isoΓ₀ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.IsIdempotentComplete C] →
        [inst_3 : CategoryTheory.Limits.HasFiniteCoproducts C] →
          (CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex C ℕ)).functor.comp
              CategoryTheory.Preadditive.DoldKan.equivalence.inverse ≅
            CategoryTheory.Idempotents.DoldKan.Γ.comp
              (CategoryTheory.Idempotents.toKaroubiEquivalence (CategoryTheory.SimplicialObject C)).functor
-- Mathlib.CategoryTheory.Dialectica.Basic
CategoryTheory.Dial.congr_simp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C],
  CategoryTheory.Dial C = CategoryTheory.Dial C
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key in the tree map, returning `none` if the
map is empty.
 -/
Std.ExtDTreeMap.minEntry? : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → Option ((a : α) × β a)
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.IsCircuit.isCocircuit_inter_nontrivial : ∀ {α : Type u_1} {M : Matroid α} {C K : Set α}, M.IsCircuit C → M.IsCocircuit K → (C ∩ K).Nonempty → (C ∩ K).Nontrivial
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.Ioc_sub_one_sub_one_eq_Ico_of_not_isMin : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Sub α]
  [PredSubOrder α] {a : α}, ¬IsMin a → ∀ (b : α), Finset.Ioc (a - 1) (b - 1) = Finset.Ico a b
-- Mathlib.Topology.Algebra.Ring.Real
ENNReal.instContinuousAdd : ContinuousAdd ENNReal
-- Mathlib.GroupTheory.Finiteness
/-- Finite product of finitely generated additive monoids is finitely generated.  -/
Pi.instAddMonoidFG : ∀ {ι : Type u_5} [Finite ι] {M : ι → Type u_6} [inst : (i : ι) → AddMonoid (M i)] [∀ (i : ι), AddMonoid.FG (M i)],
  AddMonoid.FG ((i : ι) → M i)
-- Mathlib.Algebra.Order.Group.MinMax
max_sub_sub_left : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] (a b c : α),
  max (a - b) (a - c) = a - min b c
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.ofCoeff_single : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] (a : G) (b : k),
  { coeff := fun₀ | a => b } = SkewMonoidAlgebra.single a b