mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
/-- `InducedBicategory.Hom X Y` is a type-alias for morphisms between `X Y : B` viewed as objects
of `B` with the induced bicategory structure. This is given a `CategoryStruct` instance below,
where the identity and composition is induced from `C`.  -/
CategoryTheory.Bicategory.InducedBicategory.Hom : {B : Type u_1} →
  {C : Type u_2} →
    [CategoryTheory.Bicategory C] →
      {F : B → C} →
        CategoryTheory.Bicategory.InducedBicategory C F → CategoryTheory.Bicategory.InducedBicategory C F → Type u_4
-- Mathlib.Analysis.Matrix.Normed
Matrix.linfty_opNNNorm_replicateCol : ∀ {m : Type u_3} {α : Type u_5} {ι : Type u_7} [inst : Fintype m] [inst_1 : Unique ι]
  [inst_2 : SeminormedAddCommGroup α] (v : m → α), ‖Matrix.replicateCol ι v‖₊ = ‖v‖₊
-- Mathlib.Data.Real.Sign
Real.sign_inv : ∀ (r : ℝ), r⁻¹.sign = r.sign
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.opow_eq_one_iff : ∀ {a b : Ordinal.{u_1}}, a ^ b = 1 ↔ a = 1 ∨ b = 0
-- Mathlib.LinearAlgebra.Charpoly.Basic
LinearMap.isIntegral : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Free R M]
  [Module.Finite R M] (f : M →ₗ[R] M), IsIntegral R f
-- Mathlib.Algebra.Algebra.Spectrum.Basic
/-- **Alias** of the forward direction of `spectrum.zero_mem_iff`. -/
spectrum.not_isUnit_of_zero_mem : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {a : A},
  0 ∈ spectrum R a → ¬IsUnit a
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
/-- Reinterpret an element of a type of positive linear maps as a positive linear map.  -/
PositiveLinearMap.ofClass : {F : Type u_1} →
  {R : Type u_2} →
    {E₁ : Type u_3} →
      {E₂ : Type u_4} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid E₁] →
            [inst_2 : PartialOrder E₁] →
              [inst_3 : AddCommMonoid E₂] →
                [inst_4 : PartialOrder E₂] →
                  [inst_5 : Module R E₁] →
                    [inst_6 : Module R E₂] →
                      [inst_7 : FunLike F E₁ E₂] →
                        [LinearMapClass F R E₁ E₂] → [OrderHomClass F E₁ E₂] → F → E₁ →ₚ[R] E₂
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.den_zero : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] {𝒜 : ι → σ} (x : Submonoid A) [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι]
  [inst_5 : GradedRing 𝒜], ↑(HomogeneousLocalization.NumDenSameDeg.den 0) = 1
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.DirectLimit.partialEquivLimit_comp_inclusion : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] {ι : Type u_1}
  [inst_2 : Preorder ι] [inst_3 : Nonempty ι] [inst_4 : IsDirectedOrder ι] (S : ι →o L.PartialEquiv M N) {i : ι},
  (FirstOrder.Language.DirectLimit.partialEquivLimit S).toEquiv.toEmbedding.comp
      (FirstOrder.Language.Substructure.inclusion ⋯) =
    (FirstOrder.Language.Substructure.inclusion ⋯).comp (S i).toEquiv.toEmbedding
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.replaceEntry.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (k : α) (v : β k) (k_1 : α) (v_1 : β k_1) (l : List ((a : α) × β a)),
  Std.Internal.List.replaceEntry k v (⟨k_1, v_1⟩ :: l) =
    bif k_1 == k then ⟨k, v⟩ :: l else ⟨k_1, v_1⟩ :: Std.Internal.List.replaceEntry k v l
-- Mathlib.SetTheory.ZFC.PSet
PSet.lt_def : ∀ (x y : PSet.{u_1}), x ⊂ y ↔ x ⊂ y
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
_private.Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate.0.RootPairing.linearIndepOn_coroot_iff_aux : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Field R] [inst_4 : Module R M] [inst_5 : Module R N] (P : RootPairing ι R M N)
  [P.IsAnisotropic] [P.IsRootSystem] [NeZero 2] {s : Set ι}, LinearIndepOn R (⇑P.root) s → LinearIndepOn R (⇑P.coroot) s
-- Mathlib.Topology.LocallyConstant.Basic
/-- Pull back of locally constant maps under a continuous map, by pre-composition.  -/
LocallyConstant.comap : {X : Type u_1} →
  {Y : Type u_2} →
    {Z : Type u_3} →
      [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → C(X, Y) → LocallyConstant Y Z → LocallyConstant X Z
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
/-- In conditionally complete orders with a bottom element, the nonempty condition can be omitted
from `csSup_le_iff`.  -/
csSup_le_iff' : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {s : Set α},
  BddAbove s → ∀ {a : α}, sSup s ≤ a ↔ ∀ x ∈ s, x ≤ a
-- Mathlib.AlgebraicTopology.DoldKan.NCompGamma
AlgebraicTopology.DoldKan.instIsIsoFunctorSimplicialObjectKaroubiNatTrans : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C], CategoryTheory.IsIso AlgebraicTopology.DoldKan.Γ₂N₁.natTrans
-- Mathlib.Order.WithBot
WithTop.decidableLT.eq_3 : ∀ {α : Type u_1} [inst : LT α] [inst_1 : DecidableLT α] (a_1 b_1 : α),
  WithTop.decidableLT (some b_1) (some a_1) = decidable_of_iff' (b_1 < a_1) ⋯
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
_private.Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangle_map_ext'_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {t : CategoryTheory.Triangulated.TStructure C} {n : ℤ} {X Y : C}
  {f₁ f₂ :
    CategoryTheory.Triangulated.TStructure.TruncAux.triangle✝ t n X ⟶
      CategoryTheory.Triangulated.TStructure.TruncAux.triangle✝ t n Y},
  f₁ = f₂ ↔ autoParam (f₁.hom₂ = f₂.hom₂) CategoryTheory.Triangulated.TStructure.TruncAux.triangle_map_ext'._auto_1✝
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Manifold.LocalPresentationAt.mk.sizeOf_spec : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G}
  {M : Type u_10} {N : Type u_12} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop} [inst_11 : SizeOf 𝕜] [inst_12 : SizeOf E]
  [inst_13 : SizeOf F] [inst_14 : SizeOf H] [inst_15 : SizeOf G] [inst_16 : SizeOf M] [inst_17 : SizeOf N]
  [inst_18 : (a : M → N) → (a_1 : OpenPartialHomeomorph M H) → (a_2 : OpenPartialHomeomorph N G) → SizeOf (P a a_1 a_2)]
  (domChart : OpenPartialHomeomorph M H) (codChart : OpenPartialHomeomorph N G)
  (mem_domChart_source : x ∈ domChart.source) (mem_codChart_source : f x ∈ codChart.source)
  (domChart_mem_maximalAtlas : domChart ∈ IsManifold.maximalAtlas I n M)
  (codChart_mem_maximalAtlas : codChart ∈ IsManifold.maximalAtlas J n N)
  (source_subset_preimage_source : domChart.source ⊆ f ⁻¹' codChart.source) (property : P f domChart codChart),
  sizeOf
      { domChart := domChart, codChart := codChart, mem_domChart_source := mem_domChart_source,
        mem_codChart_source := mem_codChart_source, domChart_mem_maximalAtlas := domChart_mem_maximalAtlas,
        codChart_mem_maximalAtlas := codChart_mem_maximalAtlas,
        source_subset_preimage_source := source_subset_preimage_source, property := property } =
    1 + sizeOf domChart + sizeOf codChart + sizeOf mem_domChart_source + sizeOf mem_codChart_source + sizeOf property
-- Mathlib.CategoryTheory.Bicategory.SingleObj
CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence_unitIso : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  (CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence C).unitIso =
    CategoryTheory.Iso.refl
      (CategoryTheory.Functor.id (CategoryTheory.EndMonoidal (CategoryTheory.MonoidalSingleObj.star C)))
-- Lean.Meta.Sym.Offset
/-- Returns `some offset` if `e` is an offset term. That is, it is of the form
- `Nat.succ a`, OR
- `a + k` where `k` is a numeral.

Assumption: standard instances are used for `OfNat Nat n` and `HAdd Nat Nat Nat`
 -/
Lean.Meta.Sym.isOffset? : Lean.Expr → OptionT Id Lean.Meta.Sym.Offset
-- Mathlib.LinearAlgebra.RootSystem.Defs
/-- Given two perfectly-paired `R`-modules `M` and `N`, a root pairing with indexing set `ι`
is the data of an `ι`-indexed subset of `M` ("the roots"), an `ι`-indexed subset of `N`
("the coroots"), and an `ι`-indexed set of permutations of `ι`, such that each root-coroot pair
evaluates to `2`, and the permutation attached to each element of `ι` is compatible with the
reflections on the corresponding roots and coroots.

It exists to allow for a convenient unification of the theories of root systems and root data.  -/
RootPairing : Type u_1 →
  (R : Type u_2) →
    (M : Type u_3) →
      (N : Type u_4) →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [Module R M] → [inst_3 : AddCommGroup N] → [Module R N] → Type (max (max (max u_1 u_2) u_3) u_4)
-- Batteries.Data.BinomialHeap.Basic
_private.Batteries.Data.BinomialHeap.Basic.0.Batteries.BinomialHeap.Imp.Heap.realSize_findMin : ∀ {α : Type u_1} {k : Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α} {n : ℕ} {le : α → α → Bool}
  {res : Batteries.BinomialHeap.Imp.FindMin α} {s : Batteries.BinomialHeap.Imp.Heap α} (m : ℕ),
  (∀ (s : Batteries.BinomialHeap.Imp.Heap α), (k s).realSize = m + s.realSize) →
    n = m + s.realSize →
      Batteries.BinomialHeap.Imp.FindMin.HasSize✝ res n →
        Batteries.BinomialHeap.Imp.FindMin.HasSize✝ (Batteries.BinomialHeap.Imp.Heap.findMin le k s res) n
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.sup_inf_distrib_left : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] (a b c : CauSeq α abs),
  a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c)
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.coe_neg : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) (x : ↥H), ↑(-x) = -↑x
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
CategoryTheory.ShortComplex.leftHomologyπ.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology], S.leftHomologyπ = S.leftHomologyData.π
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_eq_some_getD : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {a : α}
  {fallback : β a}, a ∈ m → m.get? a = some (m.getD a fallback)
-- Mathlib.GroupTheory.Perm.Cycle.Type
/-- Given a vector `v` of length `n` whose product is 1, make a vector of length `n - 1`,
by deleting the last entry of `v`.  -/
Equiv.Perm.VectorsProdEqOne.equivVector : (G : Type u_2) → [inst : Group G] → (n : ℕ) → ↑(Equiv.Perm.vectorsProdEqOne G n) ≃ List.Vector G (n - 1)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.mergeWith.congr_simp : ∀ {α : Type u} {β : Type v} [inst : Ord α] (mergeFn mergeFn_1 : α → β → β → β),
  mergeFn = mergeFn_1 →
    ∀ (t₁ t₁_1 : Std.DTreeMap.Internal.Impl α fun x => β) (e_t₁ : t₁ = t₁_1)
      (t₂ t₂_1 : Std.DTreeMap.Internal.Impl α fun x => β),
      t₂ = t₂_1 →
        ∀ (ht₁ : t₁.Balanced),
          Std.DTreeMap.Internal.Impl.Const.mergeWith mergeFn t₁ t₂ ht₁ =
            Std.DTreeMap.Internal.Impl.Const.mergeWith mergeFn_1 t₁_1 t₂_1 ⋯
-- Init.Data.Vector.Lemmas
Vector.toList_mapFinIdx : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {f : (i : ℕ) → α → i < n → β} {xs : Vector α n},
  (xs.mapFinIdx f).toList = xs.toList.mapFinIdx fun i a h => f i a ⋯
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.inl_normalizationCoprodIso_hom_fromNormalization : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {U V : AlgebraicGeometry.Scheme} {iU : U ⟶ X} {iV : V ⟶ X}
  (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV))
  [inst_2 : AlgebraicGeometry.QuasiCompact iU] [inst_3 : AlgebraicGeometry.QuasiSeparated iU]
  [inst_4 : AlgebraicGeometry.QuasiCompact iV] [inst_5 : AlgebraicGeometry.QuasiSeparated iV],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso f e).hom
        (AlgebraicGeometry.Scheme.Hom.fromNormalization f)) =
    AlgebraicGeometry.Scheme.Hom.fromNormalization (CategoryTheory.CategoryStruct.comp iU f)
-- Init.Data.Iterators.Lemmas.Combinators.ULift
_private.Init.Data.Iterators.Lemmas.Combinators.ULift.0.Std.Iter.step_uLift.match_1.splitter : {α β : Type u_1} →
  [inst : Std.Iterator α Id β] →
    {it : Std.Iter β} →
      (motive : it.Step → Sort u_2) →
        (x : it.Step) →
          ((it' : Std.Iter β) →
              (out : β) →
                (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
            ((it' : Std.Iter β) →
                (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
              ((h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.fromArrowArrowFunctor_obj_X₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)),
  (CategoryTheory.Square.fromArrowArrowFunctor.obj f).X₃ = f.left.right
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.card_infinitePlace_eq_card_infinitePlace : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [NumberField.IsCMField K] [inst_3 : NumberField K],
  Fintype.card (NumberField.InfinitePlace ↥(NumberField.maximalRealSubfield K)) =
    Fintype.card (NumberField.InfinitePlace K)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get!_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} [inst_2 : Inhabited β], k ∉ m₁ → (m₁ ∩ m₂).get! k = default
-- Mathlib.RingTheory.Coalgebra.GroupLike
GroupLike.val_valEquiv_symm_apply : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] (a : Subtype (IsGroupLikeElem R)), ↑(GroupLike.valEquiv.symm a) = ↑a
-- Mathlib.AlgebraicTopology.DoldKan.Projections
AlgebraicTopology.DoldKan.P_idem : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (q : ℕ),
  CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.P q) (AlgebraicTopology.DoldKan.P q) =
    AlgebraicTopology.DoldKan.P q
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.nnrealPart_add_le_add_nnrealPart : ∀ {α : Type u_2} [inst : TopologicalSpace α] (f g : CompactlySupportedContinuousMap α ℝ),
  (f + g).nnrealPart ≤ f.nnrealPart + g.nnrealPart
-- Init.Data.Array.Find
Array.findIdx_push : ∀ {α : Type u_1} {xs : Array α} {a : α} {p : α → Bool},
  Array.findIdx p (xs.push a) =
    if Array.findIdx p xs < xs.size then Array.findIdx p xs else xs.size + if p a = true then 0 else 1
-- Mathlib.Geometry.Manifold.Instances.Real
Icc_chartedSpaceChartAt_of_top_le : ∀ {x y : ℝ} [hxy : Fact (x < y)] {z : ↑(Set.Icc x y)}, y ≤ ↑z → chartAt (EuclideanHalfSpace 1) z = IccRightChart x y
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.IsBilimit.mk : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} →
        {b : CategoryTheory.Limits.BinaryBicone P Q} →
          CategoryTheory.Limits.IsLimit b.toCone → CategoryTheory.Limits.IsColimit b.toCocone → b.IsBilimit
-- Lean.ReducibilityAttrs
Lean.reducibilityCoreExt : Lean.PersistentEnvExtension (Lean.Name × Lean.ReducibilityStatus) (Lean.Name × Lean.ReducibilityStatus)
  (Lean.NameMap Lean.ReducibilityStatus)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.copy_eq : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {S : L.Substructure M} {s : Set M} (hs : s = ↑S),
  S.copy s hs = S
-- Init.Data.UInt.Bitwise
UInt32.not_eq_comm : ∀ {a b : UInt32}, ~~~a = b ↔ a = ~~~b
-- Std.Sync.Broadcast
/-- `for msg in ch.sync do ...` receives all messages in the channel until it is closed.  -/
Std.Broadcast.Sync.Receiver.instForInOfInhabitedOfMonadOfMonadLiftTBaseIO : {α : Type} →
  {m : Type → Type u_1} → [Inhabited α] → [Monad m] → [MonadLiftT BaseIO m] → ForIn m (Std.Broadcast.Sync.Receiver α) α
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.inl_v_triangle_mor₃_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) (p q : ℤ)
  (hpq : p + -1 = q),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v p q hpq)
      ((CochainComplex.mappingCone.triangle φ).mor₃.f q) =
    -(K.shiftFunctorObjXIso 1 q p ⋯).inv
-- Mathlib.Algebra.Order.Quantale
/-- Multiplication is distributive over join in a quantale  -/
IsQuantale.mul_sSup_distrib : ∀ {α : Type u_1} {inst : Semigroup α} {inst_1 : CompleteLattice α} [self : IsQuantale α] (x : α) (s : Set α),
  x * sSup s = ⨆ y ∈ s, x * y
-- Mathlib.Algebra.Star.MonoidHom
StarMonoidHom.ext : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Star A] [inst_2 : Monoid B] [inst_3 : Star B]
  {f g : A →⋆* B}, (∀ (x : A), f x = g x) → f = g
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.commRingNorm.injEq : ∀ (c : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr) (e : Lean.Meta.Grind.Arith.CommRing.RingExpr)
  (p : Lean.Grind.CommRing.Poly) (c_1 : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr)
  (e_1 : Lean.Meta.Grind.Arith.CommRing.RingExpr) (p_1 : Lean.Grind.CommRing.Poly),
  (Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.commRingNorm c e p =
      Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.commRingNorm c_1 e_1 p_1) =
    (c = c_1 ∧ e = e_1 ∧ p = p_1)
-- Mathlib.Topology.MetricSpace.Lipschitz
LipschitzWith.min : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {f g : α → ℝ} {Kf Kg : NNReal},
  LipschitzWith Kf f → LipschitzWith Kg g → LipschitzWith (max Kf Kg) fun x => min (f x) (g x)
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Prequotient.mul.injEq : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] {F : CategoryTheory.Functor J MonCat}
  (a a_1 a_2 a_3 : MonCat.Colimits.Prequotient F), (a.mul a_1 = a_2.mul a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.ker_map : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (A : Type u_2)
  (B : Type u_3) [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra A B]
  [inst_7 : Algebra S B] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B]
  [inst_11 : SMulCommClass S A B],
  (KaehlerDifferential.map R S A B).ker =
    Submodule.map (Finsupp.linearCombination A ⇑(KaehlerDifferential.D R A))
      (Submodule.comap (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B))
        (Submodule.restrictScalars A (KaehlerDifferential.kerTotal S B)))
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preBeth_mono : Monotone Cardinal.preBeth
-- Mathlib.Algebra.Group.Pi.Basic
Sum.elim_add_add : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a a' : α → γ) (b b' : β → γ) [inst : Add γ],
  Sum.elim (a + a') (b + b') = Sum.elim a b + Sum.elim a' b'
-- Mathlib.Analysis.Convex.Basic
convex_Ioi : ∀ {𝕜 : Type u_1} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [IsOrderedCancelAddMonoid β] [inst_5 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] (r : β),
  Convex 𝕜 (Set.Ioi r)
-- Lean.Server.References
Lean.Server.DirectImports.mk.inj : ∀ {ordered : Array Lean.Server.ModuleImport} {index : Lean.Server.ModuleImportIndex}
  {ordered_1 : Array Lean.Server.ModuleImport} {index_1 : Lean.Server.ModuleImportIndex},
  { ordered := ordered, index := index } = { ordered := ordered_1, index := index_1 } →
    ordered = ordered_1 ∧ index = index_1
-- Mathlib.CategoryTheory.Iso
/-- Inverse isomorphism.  -/
CategoryTheory.Iso.symm : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (X ≅ Y) → (Y ≅ X)
-- Mathlib.Data.List.Map2
List.map₂Left_nil_right : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : α → Option β → γ) (as : List α),
  List.map₂Left f as [] = List.map (fun a => f a none) as
-- Mathlib.Data.Set.Equitable
Set.equitableOn_iff_exists_image_subset_icc : ∀ {α : Type u_1} {s : Set α} {f : α → ℕ}, s.EquitableOn f ↔ ∃ b, f '' s ⊆ Set.Icc b (b + 1)
-- Lean.Meta.Tactic.Grind.Core
/-- Updates the modification time to `gmt` for the parents of `root`.
The modification time is used to decide which terms are considered during e-matching.
 -/
_private.Lean.Meta.Tactic.Grind.Core.0.Lean.Meta.Grind.updateMT : Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Order.TeichmullerTukey
/-- A family of sets $F$ is of finite character iff for every set $X$, $X ∈ F$ iff every finite
subset of $X$ is in $F$  -/
Order.IsOfFiniteCharacter : {α : Type u_1} → Set (Set α) → Prop
-- Mathlib.LinearAlgebra.Multilinear.Basis
Basis.multilinearMap.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] {M : ι → Type u_3} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] {κ : ι → Type u_5} (b b_1 : (i : ι) → Module.Basis (κ i) R (M i)),
  b = b_1 →
    ∀ {ι' : Type u_6} {N : Type u_7} [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (b' b'_1 : Module.Basis ι' R N),
      b' = b'_1 →
        ∀ [inst_5 : Finite ι] [inst_6 : ∀ (i : ι), Finite (κ i)],
          Basis.multilinearMap b b' = Basis.multilinearMap b_1 b'_1
-- Std.Internal.Do.Order.Basic
/-- `⊤ ⊑ g` for a function `g` follows from pointwise `⊤ ⊑ g s`.  -/
Lean.Order.top_le_of_forall_top_le : ∀ {σ α : Type u} [inst : Lean.Order.CompleteLattice α] {g : σ → α},
  (∀ (s : σ), Lean.Order.PartialOrder.rel Lean.Order.top (g s)) → Lean.Order.PartialOrder.rel Lean.Order.top g
-- Mathlib.CategoryTheory.Generator.Preadditive
CategoryTheory.Preadditive.isCoseparator_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (G : C),
  CategoryTheory.IsCoseparator G ↔
    ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : Y ⟶ G), CategoryTheory.CategoryStruct.comp f h = 0) → f = 0
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
/-- Given a set of outer measures, we define a new function that on a set `s` is defined to be the
infimum of `μ(s)` for the outer measures `μ` in the collection. We ensure that this
function is defined to be `0` on `∅`, even if the collection of outer measures is empty.
The outer measure generated by this function is the infimum of the given outer measures.  -/
MeasureTheory.OuterMeasure.sInfGen : {α : Type u_1} → Set (MeasureTheory.OuterMeasure α) → Set α → ENNReal
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.restrict_mono : ∀ {α : Type u_1} {s t : Set α},
  s ⊆ t →
    ∀ {m m' : MeasureTheory.OuterMeasure α},
      m ≤ m' → (MeasureTheory.OuterMeasure.restrict s) m ≤ (MeasureTheory.OuterMeasure.restrict t) m'