mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- A functor `F : C ⥤ D` reflects limits if
whenever the image of a cone over some `K : J ⥤ C` under `F` is a limit cone in `D`,
the cone was already a limit cone in `C`.
Note that we do not assume a priori that `D` actually has any limits.
 -/
CategoryTheory.Limits.ReflectsLimitsOfSize : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.uniqueBaseOn_isBase_iff : ∀ {α : Type u_1} {E B I : Set α}, I ⊆ E → ((Matroid.uniqueBaseOn I E).IsBase B ↔ B = I)
-- Mathlib.RingTheory.Polynomial.Pochhammer
ascPochhammer_zero : ∀ (S : Type u) [inst : Semiring S], ascPochhammer S 0 = 1
-- Mathlib.Combinatorics.Matroid.Basic
/-- This is the same as `Indep.exists_insert_of_not_isBase`, but phrased so that
it is defeq to the augmentation axiom for independent sets.  -/
Matroid.Indep.exists_insert_of_not_maximal : ∀ {α : Type u_1} (M : Matroid α) ⦃I B : Set α⦄,
  M.Indep I → ¬Maximal M.Indep I → Maximal M.Indep B → ∃ x ∈ B \ I, M.Indep (insert x I)
-- Init.PropLemmas
and_imp_left_iff_true : ∀ {P Q : Prop}, P ∧ Q → P ↔ True
-- Mathlib.Algebra.Lie.Weights.Basic
/-- Lie module weight spaces are independent.

See also `LieModule.iSupIndep_genWeightSpace'`.  -/
LieModule.iSupIndep_genWeightSpace : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [IsDomain R] [Module.IsTorsionFree R M],
  iSupIndep fun χ => LieModule.genWeightSpace M χ
-- Mathlib.AlgebraicGeometry.Birational.Composition
/-- Composition of rational maps. Requires `f` to be dominant, so that we may choose
a dominant representative.  -/
AlgebraicGeometry.Scheme.RationalMap.comp : {X Y Z : AlgebraicGeometry.Scheme} →
  [PreirreducibleSpace ↥X] → [Nonempty ↥Y] → (f : X.RationalMap Y) → [f.IsDominant] → Y.RationalMap Z → X.RationalMap Z
-- Mathlib.Analysis.Analytic.Composition
FormalMultilinearSeries.applyComposition_ones : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup E] [inst_8 : ContinuousConstSMul 𝕜 E] [inst_9 : IsTopologicalAddGroup F]
  [inst_10 : ContinuousConstSMul 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ),
  p.applyComposition (Composition.ones n) = fun v i => (p 1) fun x => v (Fin.castLE ⋯ i)
-- Mathlib.Data.Matrix.Block
Matrix.blockDiag_map : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} {β : Type u_13} (M : Matrix (m × o) (n × o) α)
  (f : α → β), (M.map f).blockDiag = fun k => (M.blockDiag k).map f
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.biUnion_op_vadd_finset : ∀ {α : Type u_2} [inst : Add α] [inst_1 : DecidableEq α] (s t : Finset α),
  (t.biUnion fun a => AddOpposite.op a +ᵥ s) = s + t
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- `forbidden F` is the set of configurations that avoid every pattern in `F`.

Formally: `x ∈ forbidden F` if and only if for every pattern `p ∈ F` and every
monoid element `g : G`, the pattern `p` does not occur in `x` at position `g`.

Intuitively, `forbidden F` is the shift space defined by declaring the finite set
(or family) of patterns `F` to be *forbidden*. A configuration belongs to the subshift if and only
it avoids all the forbidden patterns.  -/
SymbolicDynamics.FullShift.forbidden : {A : Type u_1} →
  {G : Type u_2} → [inst : Inhabited A] → [AddMonoid G] → Set (SymbolicDynamics.FullShift.Pattern A G) → Set (G → A)
-- Init.Core
not_of_iff_false : ∀ {p : Prop}, (p ↔ False) → ¬p
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.scaleRoots_dvd_iff : ∀ {R : Type u_1} [inst : CommSemiring R] (p q : Polynomial R) {r : R},
  IsUnit r → (p.scaleRoots r ∣ q.scaleRoots r ↔ p ∣ q)
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.mk.sizeOf_spec : ∀ {V : Type u} [inst : SizeOf V] (Adj : V → V → Prop) (symm : autoParam (Std.Symm Adj) SimpleGraph.symm._autoParam)
  (loopless : autoParam (Std.Irrefl Adj) SimpleGraph.loopless._autoParam),
  sizeOf { Adj := Adj, symm := symm, loopless := loopless } = 1 + sizeOf symm + sizeOf loopless
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.stepAsHetT_filterMapWithPostcondition.match_3.eq_1 : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (out : β) (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- Whiskering a 1-morphism is a functor.  -/
CategoryTheory.Bicategory.LeftLift.whiskering : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} →
          {x : B} →
            (h : x ⟶ c) →
              CategoryTheory.Functor (CategoryTheory.Bicategory.LeftLift f g)
                (CategoryTheory.Bicategory.LeftLift f (CategoryTheory.CategoryStruct.comp h g))
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.liftMetaTacticAux : {α : Type} → (Lean.MVarId → Lean.MetaM (α × List Lean.MVarId)) → Lean.Elab.Tactic.TacticM α
-- Mathlib.Topology.Maps.Basic
/-- An inducing map with an open range is an open map.  -/
Topology.IsInducing.isOpenMap : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsInducing f → IsOpen (Set.range f) → IsOpenMap f
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.whiskerRight_toUnit_comp_leftUnitor_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (X Y : C)
  {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X) Y)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y) h
-- Mathlib.MeasureTheory.Measure.Restrict
/-- Two measures are equal if they are equal on the π-system generating the σ-algebra,
and they are both finite on an increasing spanning sequence of sets in the π-system.
This lemma is formulated using `iUnion`.
`FiniteSpanningSetsIn.ext` is a reformulation of this lemma.  -/
MeasureTheory.Measure.ext_of_generateFrom_of_iUnion : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} (C : Set (Set α)) (B : ℕ → Set α),
  m0 = MeasurableSpace.generateFrom C →
    IsPiSystem C → ⋃ i, B i = Set.univ → (∀ (i : ℕ), B i ∈ C) → (∀ (i : ℕ), μ (B i) ≠ ⊤) → (∀ s ∈ C, μ s = ν s) → μ = ν
-- Mathlib.Probability.Decision.Risk.Countable
ProbabilityTheory.avgRisk_countable : ∀ {Θ : Type u_1} {𝓧 : Type u_3} {𝓨 : Type u_5} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : ProbabilityTheory.Kernel Θ 𝓧} {κ : ProbabilityTheory.Kernel 𝓧 𝓨}
  {π : MeasureTheory.Measure Θ} [Countable Θ] [MeasurableSingletonClass Θ],
  ProbabilityTheory.avgRisk ℓ P κ π = ∑' (θ : Θ), (∫⁻ (y : 𝓨), ℓ θ y ∂(κ.comp P) θ) * π {θ}
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.FunctorialFactorizationData.fac_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  (data : W₁.FunctorialFactorizationData W₂) {f : CategoryTheory.Arrow C},
  CategoryTheory.CategoryStruct.comp (data.i.app f) (data.p.app f) = f.hom
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.mk.inj : ∀ {C : Type u} {I : Type w} {obj : I → C} {I_1 : Type w} {obj_1 : I_1 → C},
  { I := I, obj := obj } = { I := I_1, obj := obj_1 } → I = I_1 ∧ obj ≍ obj_1
-- Mathlib.Topology.LocalAtTarget
/-- Given a continuous map `f : X → Y` between topological spaces.
Suppose we have an open cover `U i` of the range of `f`, and a family of continuous maps `V i → X`
whose images are a cover of `X` that is coarser than the pullback of `U` under `f`.
To check that `f` is an embedding it suffices to check that `V i → Y` is an embedding for all `i`.
 -/
isEmbedding_of_iSup_eq_top_of_preimage_subset_range : ∀ {X : Type u_6} {Y : Type u_7} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
  Continuous f →
    ∀ {ι : Type u_4} (U : ι → TopologicalSpace.Opens Y),
      Set.range f ⊆ ↑(iSup U) →
        ∀ (V : ι → Type u_5) [inst_2 : (i : ι) → TopologicalSpace (V i)] (iV : (i : ι) → V i → X),
          (∀ (i : ι), Continuous (iV i)) →
            (∀ (i : ι), f ⁻¹' ↑(U i) ⊆ Set.range (iV i)) →
              (∀ (i : ι), Topology.IsEmbedding (f ∘ iV i)) → Topology.IsEmbedding f
-- Mathlib.Algebra.Group.Nat.Even
Nat.even_mul : ∀ {m n : ℕ}, Even (m * n) ↔ Even m ∨ Even n
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
/-- A transfinite composition of shape `J` of morphisms in `W` induces a transfinite
composition of shape `Set.Ici j` (for any `j : J`).  -/
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ici : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {J : Type w} →
        [inst_1 : LinearOrder J] →
          [inst_2 : SuccOrder J] →
            [inst_3 : OrderBot J] →
              [inst_4 : WellFoundedLT J] →
                {X Y : C} →
                  {f : X ⟶ Y} →
                    (h : W.TransfiniteCompositionOfShape J f) →
                      (j : J) → W.TransfiniteCompositionOfShape (↑(Set.Ici j)) (h.incl.app j)
-- Mathlib.Order.Preorder.Chain
Flag.maxChain : ∀ {α : Type u_1} [inst : LE α] (s : Flag α), IsMaxChain (fun x1 x2 => x1 ≤ x2) ↑s
-- Std.Data.HashSet.Lemmas
Std.HashSet.erase_emptyWithCapacity : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {a : α} {c : ℕ},
  (Std.HashSet.emptyWithCapacity c).erase a = Std.HashSet.emptyWithCapacity c
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vadd_set_univ_pi : ∀ {M : Type u_5} {ι : Type u_6} {π : ι → Type u_7} [inst : (i : ι) → VAdd M (π i)] (c : M) (s : (i : ι) → Set (π i)),
  c +ᵥ Set.univ.pi s = Set.univ.pi (c +ᵥ s)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.cyclesFunctor_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i : ι) [inst_2 : CategoryTheory.CategoryWithHomology C]
  {X Y : HomologicalComplex C c} (f : X ⟶ Y),
  (HomologicalComplex.cyclesFunctor C c i).map f = HomologicalComplex.cyclesMap f i
-- Mathlib.Logic.Function.Iterate
Function.iterate_zero : ∀ {α : Type u} (f : α → α), f^[0] = id
-- Mathlib.Algebra.Homology.Embedding.Boundary
ComplexShape.Embedding.not_boundaryGE_next' : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsRelIff]
  {j k : ι}, ¬e.BoundaryGE j → c.next j = k → ¬e.BoundaryGE k
-- Mathlib.Topology.Sequences
IsSeqCompact.exists_tendsto_of_frequently_mem : ∀ {X : Type u_1} [inst : UniformSpace X] {s : Set X},
  IsSeqCompact s →
    ∀ {u : ℕ → X}, (∃ᶠ (n : ℕ) in Filter.atTop, u n ∈ s) → CauchySeq u → ∃ x ∈ s, Filter.Tendsto u Filter.atTop (nhds x)
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.Pos.revSkipWhile_string_eq_revSkipWhile_toSlice : ∀ {pat : String} {s : String.Slice} (curr : s.Pos), curr.revSkipWhile pat = curr.revSkipWhile pat.toSlice
-- Init.Data.Range.Polymorphic.IntLemmas
Int.isSome_getElem?_toArray_rco_eq : ∀ {m n : ℤ} {i : ℕ}, ((m...n).toArray[i]?.isSome = true) = (i < (n - m).toNat)
-- Mathlib.Algebra.Order.Monovary
Antivary.div_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : CommGroup β] [inst_2 : LinearOrder β]
  [IsOrderedMonoid β] {f : ι → α} {g₁ g₂ : ι → β}, Antivary f g₁ → Monovary f g₂ → Antivary f (g₁ / g₂)
-- Mathlib.Data.Rat.Cast.Order
Rat.cast_min : ∀ {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ), ↑(min p q) = min ↑p ↑q
-- Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
rexp_neg_quadratic_isLittleO_rpow_atTop : ∀ {a : ℝ}, a < 0 → ∀ (b s : ℝ), (fun x => Real.exp (a * x ^ 2 + b * x)) =o[Filter.atTop] fun x => x ^ s
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.Config.mk : ℕ → ℕ → Mathlib.Meta.FunProp.Config
-- Mathlib.Data.ZMod.Basic
ZMod.val_le : ∀ {n : ℕ} [NeZero n] (a : ZMod n), a.val ≤ n
-- Mathlib.Algebra.Homology.Embedding.TruncLE
HomologicalComplex.truncLE'ToRestriction_naturality : ∀ {ι : 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]
  {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [inst_2 : e.IsTruncLE]
  [inst_3 : ∀ (i' : ι'), K.HasHomology i'] [inst_4 : ∀ (i' : ι'), L.HasHomology i'],
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncLE'Map φ e) (L.truncLE'ToRestriction e) =
    CategoryTheory.CategoryStruct.comp (K.truncLE'ToRestriction e) (HomologicalComplex.restrictionMap φ e)
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
GenContFract.IntFractPair.seq1.eq_1 : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] (v : K),
  GenContFract.IntFractPair.seq1 v =
    (GenContFract.IntFractPair.of v, Stream'.Seq.tail ⟨GenContFract.IntFractPair.stream v, ⋯⟩)
-- Init.WF
Nat.lt_wfRel : WellFoundedRelation ℕ
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.mk_eq_mk_iff_iff : ∀ {basis_hd : ℝ → ℝ} {basis_tl : List (ℝ → ℝ)}
  (ms : Tactic.ComputeAsymptotics.MultiseriesExpansion (basis_hd :: basis_tl))
  (s : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl) (f : ℝ → ℝ),
  Tactic.ComputeAsymptotics.MultiseriesExpansion.mk s f = ms ↔ ms.seq = s ∧ ms.toFun = f
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
instCoeSortProfiniteGrpType : CoeSort ProfiniteGrp.{u} (Type u)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_naturality : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f]
  {U V : (TopologicalSpace.Opens ↑X.toTopCat)ᵒᵖ} (i : U ⟶ V),
  CategoryTheory.CategoryStruct.comp (X.presheaf.map i)
      (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp f (Opposite.unop V)) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp f (Opposite.unop U))
      (Y.presheaf.map ((AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.opensFunctor f).op.map i))
-- Mathlib.Condensed.Light.Module
/-- The condensed version of the free-forgetful adjunction.  -/
LightCondensed.freeForgetAdjunction : (R : Type u) → [inst : Ring R] → LightCondensed.free R ⊣ LightCondensed.forget R
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.contains_of_contains_insertIfNew : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β k},
  (m.insertIfNew k v).contains a = true → (k == a) = false → m.contains a = true
-- Mathlib.Order.KrullDimension
Order.krullDim_int : Order.krullDim ℤ = ⊤
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.support_rename_killCompl_subset : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {p : MvPolynomial τ R} {f : σ → τ}
  (hf : Function.Injective f), ((MvPolynomial.rename f) ((MvPolynomial.killCompl hf) p)).support ⊆ p.support
-- Mathlib.Algebra.DirectSum.Module
/-- The natural linear equivalence between `⨁ _ : ι, M` and `M` when `Unique ι`.  -/
DirectSum.lid : (R : Type u) →
  [inst : Semiring R] →
    (M : Type v) →
      (ι : optParam (Type u_1) PUnit.{u_1 + 1}) →
        [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → [Unique ι] → (DirectSum ι fun x => M) ≃ₗ[R] M
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
/-- Auxiliary lemma for `rnDeriv_withDensity_left`.  -/
MeasureTheory.Measure.rnDeriv_withDensity_withDensity_rnDeriv_left : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → ENNReal} (μ ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν],
  (∀ᵐ (x : α) ∂μ, f x ≠ ⊤) → ((ν.withDensity (μ.rnDeriv ν)).withDensity f).rnDeriv ν =ᵐ[ν] (μ.withDensity f).rnDeriv ν
-- Init.Data.List.ToArray
Array.back.congr_simp : ∀ {α : Type u} (xs xs_1 : Array α) (e_xs : xs = xs_1) (h : 0 < xs.size), xs.back h = xs_1.back ⋯
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.instCommRingAdicCauchySequence : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → CommRing (AdicCompletion.AdicCauchySequence I R)
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
/-- The canonical morphism `S.X₃ ⟶ S.X₁⟦(1 : ℤ)⟧` attached to a degreewise split
short exact sequence of cochain complexes.  -/
CochainComplex.homOfDegreewiseSplit : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) →
        ((n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) →
          (S.X₃ ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj S.X₁)
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuous_biInf : ∀ {α : Type u_1} [inst : TopologicalSpace α] {ι : Sort u_4} {δ : Type u_5} [inst_1 : CompleteLinearOrder δ]
  {p : ι → Prop} {f : (i : ι) → p i → α → δ},
  (∀ (i : ι) (hi : p i), UpperSemicontinuous (f i hi)) → UpperSemicontinuous fun x' => ⨅ i, ⨅ (hi : p i), f i hi x'
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.coeff_mapDomainLinearEquiv : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Module R S] (e : M ≃ N) (x : AddMonoidAlgebra S M),
  ((AddMonoidAlgebra.mapDomainLinearEquiv R S e) x).coeff = Finsupp.equivMapDomain e x.coeff
-- Mathlib.Algebra.Opposites
AddOpposite.instNeg.eq_1 : ∀ {α : Type u_1} [inst : Neg α], AddOpposite.instNeg = { neg := fun x => AddOpposite.op (-AddOpposite.unop x) }
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.one_lt_of_mem_cycleType : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α} {n : ℕ}, n ∈ σ.cycleType → 1 < n
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getKeyD_filter : ∀ {α : Type u} [inst : BEq α] [inst_1 : EquivBEq α] {β : Type v} {f : α → β → Bool} {l : List ((_ : α) × β)}
  {k fallback : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKeyD k (List.filter (fun p => f p.fst p.snd) l) fallback =
      ((Std.Internal.List.getKey? k l).pfilter fun x h => f x (Std.Internal.List.getValue x l ⋯)).getD fallback
-- Init.Data.Nat.Lemmas
Nat.two_pow_pred_mul_two : ∀ {w : ℕ}, 0 < w → 2 ^ (w - 1) * 2 = 2 ^ w
-- Mathlib.Algebra.Order.Hom.Basic
AddGroupNormClass.toAddGroupSeminormClass : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} {inst : AddGroup α} {inst_1 : AddCommMonoid β}
  {inst_2 : PartialOrder β} {inst_3 : FunLike F α β} [self : AddGroupNormClass F α β], AddGroupSeminormClass F α β
-- Mathlib.Data.Sum.Basic
Sum.swap_rightInverse : ∀ {α : Type u} {β : Type v}, Function.RightInverse Sum.swap Sum.swap
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.instSetLike : {R : Type u} → [inst : NonUnitalNonAssocRing R] → SetLike (NonUnitalSubring R) R
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.forIn_filterMapWithPostcondition.match_1.eq_2 : ∀ {β₂ : Type u_1} (motive : Option β₂ → Sort u_2) (h_1 : (c : β₂) → motive (some c)) (h_2 : Unit → motive none),
  (match none with
    | some c => h_1 c
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearEquiv.conjContinuousAlgEquiv_apply_apply : ∀ {𝕜 : Type u_1} {G : Type u_4} {H : Type u_5} [inst : AddCommGroup G] [inst_1 : AddCommGroup H]
  [inst_2 : NormedField 𝕜] [inst_3 : Module 𝕜 G] [inst_4 : Module 𝕜 H] [inst_5 : TopologicalSpace G]
  [inst_6 : TopologicalSpace H] [inst_7 : IsTopologicalAddGroup G] [inst_8 : IsTopologicalAddGroup H]
  [inst_9 : ContinuousConstSMul 𝕜 G] [inst_10 : ContinuousConstSMul 𝕜 H] (e : G ≃L[𝕜] H) (f : G →L[𝕜] G) (x : H),
  (e.conjContinuousAlgEquiv f) x = e (f (e.symm x))
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.toList.eq_1 : ∀ {α : Type u_1}, FreeAddMonoid.toList = Equiv.refl (FreeAddMonoid α)
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.coe_trans : ∀ {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : Mul A] [inst_1 : Mul B] [inst_2 : Mul C] [inst_3 : Star A]
  [inst_4 : Star B] [inst_5 : Star C] (e₁ : A ≃⋆* B) (e₂ : B ≃⋆* C), ⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeft₃ObjObjMap_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [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} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7)
  [inst_6 : CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁)
  (F₂ : CategoryTheory.Functor C₂ D₂) {F₃ F₃' : CategoryTheory.Functor C₃ D₃} (τ₃ : F₃ ⟶ F₃')
  (F : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))),
  (CategoryTheory.Functor.whiskeringLeft₃ObjObjMap E F₁ F₂ τ₃).app F =
    F₁.whiskerLeft (F.whiskerLeft (((CategoryTheory.Functor.whiskeringLeft₂ E).obj F₂).map τ₃))
-- Mathlib.ModelTheory.Order
/-- The class of finite models of the theory of linear orders is Fraïssé.  -/
FirstOrder.Language.isFraisse_finite_linear_order : FirstOrder.Language.IsFraisse {M | Finite ↑M ∧ ↑M ⊨ FirstOrder.Language.order.linearOrderTheory}
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instAddMonoid.eq_1 : ∀ {α : Type u_1} [inst : AddMonoid α],
  Colex.instAddMonoid =
    { toAddSemigroup := Colex.instAddSemigroup, toZero := Colex.instZero, zero_add := ⋯, add_zero := ⋯,
      toNSMul := NSMul.ofSMul, nsmul_zero := ⋯, nsmul_succ := ⋯ }
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.Hom.isIso_iff_isIso_app : ∀ {X : AlgebraicGeometry.Scheme} {M N : X.Modules} {φ : M ⟶ N},
  CategoryTheory.IsIso φ ↔ ∀ (U : X.Opens), CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Modules.Hom.app φ U)
-- Mathlib.CategoryTheory.Category.Quiv
/-- The functor `free : Quiv ⥤ Cat` preserves identities up to natural isomorphism and in fact up
to equality.  -/
CategoryTheory.Cat.freeMapIdIso : (V : Type u_1) →
  [inst : Quiver V] → CategoryTheory.Cat.freeMap (𝟭q V) ≅ CategoryTheory.Functor.id (CategoryTheory.Paths V)
-- Mathlib.CategoryTheory.Limits.Types.Colimits
/-- (internal implementation) the colimit cocone of a functor,
implemented as a quotient of a sigma type
 -/
CategoryTheory.Limits.Types.colimitCocone : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J (Type u)) → [Small.{u, max u v} F.ColimitType] → CategoryTheory.Limits.Cocone F
-- Mathlib.SetTheory.Ordinal.Basic
PrincipalSeg.ordinal_type_lt : ∀ {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder α r] [inst_1 : IsWellOrder β s]
  (h : PrincipalSeg r s), Ordinal.type r < Ordinal.type s