mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.opcyclesMap_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
  (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) [inst_2 : S₁.HasRightHomology]
  [inst_3 : S₂.HasRightHomology],
  CategoryTheory.ShortComplex.opcyclesMap φ =
    CategoryTheory.CategoryStruct.comp h₁.opcyclesIso.hom (CategoryTheory.CategoryStruct.comp γ.φQ h₂.opcyclesIso.inv)
-- Init.Control.Lawful.MonadLift.Instances
ExceptT.lift_bind : ∀ {m : Type u → Type v} [inst : Monad m] [LawfulMonad m] {α β ε : Type u} (ma : m α) (f : α → m β),
  ExceptT.lift (ma >>= f) = do
    let a ← ExceptT.lift ma
    ExceptT.lift (f a)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- Assumes left strict covariance.  -/
Left.mul_lt_mul_of_nonneg : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b c d : α} [inst_1 : Preorder α] [PosMulStrictMono α] [MulPosMono α],
  a < b → c < d → 0 ≤ a → 0 ≤ c → a * c < b * d
-- Lean.Parser.Term
/-- Logs an error, tagging the message as a named error with the specified name and validating that an
associated error explanation exists. The message may be passed as an interpolated string or a
`MessageData` term. The result of `getRef` is used as position information.
 -/
Lean.Parser.Term.logNamedErrorMacro : Lean.Parser.Parser
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.indepSets_zero_right : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω}
  {s1 s2 : Set (Set Ω)}, ProbabilityTheory.Kernel.IndepSets s1 s2 κ 0
-- Mathlib.Analysis.InnerProductSpace.Reproducing
/-- The span of the kernel functions is dense.  -/
RKHS.kerFun_dense : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] (H : Type u_4) [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace 𝕜 H]
  [inst_5 : RKHS 𝕜 H X V] [inst_6 : CompleteSpace H] [inst_7 : CompleteSpace V],
  (Submodule.span 𝕜 {x | ∃ x_1 v, (RKHS.kerFun H x_1) v = x}).topologicalClosure = ⊤
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Hom.addEquivCongrRight_symm_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N : C} [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.AddMonObj N] (e : M ≅ N)
  [inst_4 : CategoryTheory.IsAddMonHom e.hom] (X : C)
  (a : ↑((CategoryTheory.yonedaAddMon.obj { X := N, addMon := inst_3 }).obj (Opposite.op X))),
  (CategoryTheory.Hom.addEquivCongrRight e X).symm a =
    (AddMonCat.Hom.hom (AddMonCat.ofHom (CategoryTheory.IsAddMonHom.addMonoidHom e.inv X))) a
-- Std.Http.Internal.IndexMultiMap
/-- Invariant: every key in `indexes` maps to a non-empty array of valid indices into `entries`.
 -/
Std.Internal.IndexMultiMap.validity : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (self : Std.Internal.IndexMultiMap α β) (k : α)
  (p : k ∈ self.indexes),
  let idx := self.indexes.get k p;
  idx.size > 0 ∧ ∀ i ∈ idx, i < self.entries.size
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.t_fst_snd_assoc : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i j : 𝒰.I₀)
  {Z_1 : AlgebraicGeometry.Scheme} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t 𝒰 f g i j)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) (𝒰.f j))
          (𝒰.f i))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
        (𝒰.f j))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) h)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.IterM.fold_filterMapM : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {ps : Std.Do.PostShape} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Monad n] [inst_5 : MonadAttach n]
  [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_8 : Std.Do.WPMonad n ps] [inst_9 : Std.IteratorLoop α m n]
  [Std.LawfulIteratorLoop α m n] [inst_11 : MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → n (Option γ)}
  {g : δ → γ → δ} {init : δ} {it : Std.IterM m β} {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps},
  ⦃P⦄
      Std.IterM.foldM
        (fun d b => do
          let __x ← f b
          match __x with
            | some c => pure (g d c)
            | x => pure d)
        init it ⦃Q⦄ →
    ⦃P⦄ Std.IterM.fold g init (Std.IterM.filterMapM f it) ⦃Q⦄
-- Init.Grind.ToInt
Lean.Grind.IntInterval.wrap.eq_3 : ∀ (x hi : ℤ), (Lean.Grind.IntInterval.io hi).wrap x = min x (hi - 1)
-- Mathlib.Data.Vector.Basic
List.Vector.mmap_nil : ∀ {m : Type u_6 → Type u_7} [inst : Monad m] {α : Type u_8} {β : Type u_6} (f : α → m β),
  List.Vector.mmap f List.Vector.nil = pure List.Vector.nil
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- `Res(a, g) = a ^ deg g`  -/
Polynomial.resultant_C_zero_right : ∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R) (m : ℕ) (r : R), f.resultant (Polynomial.C r) m 0 = r ^ m
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
/-- The opposite of a map `L.obj X ⟶ L.obj Y` when `L : C ⥤ D` is a localization
functor, `C` is preadditive and there is a left calculus of fractions.  -/
CategoryTheory.Localization.Preadditive.neg' : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [CategoryTheory.Preadditive C] →
          {L : CategoryTheory.Functor C D} →
            (W : CategoryTheory.MorphismProperty C) →
              [L.IsLocalization W] →
                [W.HasLeftCalculusOfFractions] → {X Y : C} → (L.obj X ⟶ L.obj Y) → (L.obj X ⟶ L.obj Y)
-- Mathlib.Algebra.Algebra.Tower
IsScalarTower.Algebra.ext : ∀ {S : Type u} {A : Type v} [inst : CommSemiring S] [inst_1 : Semiring A] (h1 h2 : Algebra S A),
  (∀ (r : S) (x : A),
      (have I := h1;
        r • x) =
        r • x) →
    h1 = h2
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_inter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited α] {k : α}, (m₁ ∩ m₂).getKey! k = if k ∈ m₂ then m₁.getKey! k else default
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
_private.Mathlib.CategoryTheory.Sites.Descent.Precoverage.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.sieve.exists_fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S}
  {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S} {i : ι} {Z : C} {q : Z ⟶ X i},
  (CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.sieve✝ f f' i).arrows (CategoryTheory.Over.homMk q ⋯) →
    ∃ j a, CategoryTheory.CategoryStruct.comp a (f' j) = CategoryTheory.CategoryStruct.comp q (f i)
-- Mathlib.NumberTheory.NumberField.Basic
/-- A basis of `K` over `ℚ` that is also a basis of `𝓞 K` over `ℤ`.  -/
NumberField.integralBasis : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] → Module.Basis (Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K)) ℚ K
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A bicone over `P Q : C`, which is both a limit cone and a colimit cocone.  -/
CategoryTheory.Limits.BinaryBiproductData.isBilimit : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} → (self : CategoryTheory.Limits.BinaryBiproductData P Q) → self.bicone.IsBilimit
-- Mathlib.LinearAlgebra.Matrix.Hermitian
/-- A matrix is Hermitian if it is equal to its conjugate transpose. On the reals, this definition
captures symmetric matrices.  -/
Matrix.IsHermitian : {α : Type u_1} → {n : Type u_4} → [Star α] → Matrix n n α → Prop
-- Mathlib.Dynamics.BirkhoffSum.Basic
birkhoffSum_succ : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] (f : α → α) (g : α → M) (n : ℕ) (x : α),
  birkhoffSum f g (n + 1) x = birkhoffSum f g n x + g (f^[n] x)
-- Mathlib.Tactic.Ring.PNat
Mathlib.Tactic.Ring.instCSLiftValPNatNatHAdd : ∀ {n : ℕ+} {n' : ℕ} {k : ℕ+} {k' : ℕ} [h1 : Mathlib.Tactic.Ring.CSLiftVal n n']
  [h2 : Mathlib.Tactic.Ring.CSLiftVal k k'], Mathlib.Tactic.Ring.CSLiftVal (n + k) (n' + k')
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.filter : {α : Type u} →
  {β : α → Type v} → ((a : α) → β a → Bool) → Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList α β
-- Mathlib.Data.Int.Init
Int.div_lt_div_iff_of_dvd_of_neg_of_pos : ∀ {a b c d : ℤ}, b < 0 → 0 < d → b ∣ a → d ∣ c → (a / b < c / d ↔ c * b < d * a)
-- Mathlib.Probability.Distributions.Gaussian.Fernique
/-- For a centered Gaussian measure `μ`, the product measure `μ.prod μ` is invariant under
rotation.  -/
ProbabilityTheory.IsGaussian.map_rotation_eq_self : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] [CompleteSpace E] [SecondCountableTopology E],
  ∫ (x : E), id x ∂μ = 0 →
    ∀ (θ : ℝ), MeasureTheory.Measure.map (⇑(ContinuousLinearMap.rotation θ)) (μ.prod μ) = μ.prod μ
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.prod_withDensity_left : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_2} {mβ : MeasurableSpace β}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {f : α → ENNReal},
  Measurable f → (μ.withDensity f).prod ν = (μ.prod ν).withDensity fun z => f z.1
-- Init.Omega.Constraint
/-- Normalize a constraint, by dividing through by the GCD.

Return `none` if there is nothing to do, to avoid adding unnecessary steps to the proof term.
 -/
Lean.Omega.normalize? : Lean.Omega.Constraint × Lean.Omega.Coeffs → Option (Lean.Omega.Constraint × Lean.Omega.Coeffs)
-- Mathlib.MeasureTheory.Measure.Haar.Quotient
_private.Mathlib.MeasureTheory.Measure.Haar.Quotient.0.termμ_𝓕_1 : Lean.ParserDescr
-- Lean.Meta.InferType
/-- Status of the expression is unknown,
and `inferType` must be used.
 -/
_private.Lean.Meta.InferType.0.Lean.Meta.ArrowPropResult.undef : Lean.Meta.ArrowPropResult✝
-- Mathlib.Topology.Algebra.IsOpenUnits
instIsOpenUnitsOfDiscreteTopology : ∀ (M : Type u_1) [inst : Monoid M] [inst_1 : TopologicalSpace M] [DiscreteTopology M], IsOpenUnits M
-- Mathlib.Data.Fintype.EquivFin
Infinite.nonempty : ∀ (α : Type u_4) [Infinite α], Nonempty α
-- Init.Data.Array.MinMax
/-- Returns the largest element of the array if it is not empty, or `none` if it is empty.

Examples:
* `#[].max? = none`
* `#[4].max? = some 4`
* `#[1, 4, 2, 10, 6].max? = some 10`
 -/
Array.max? : {α : Type u_1} → [Max α] → Array α → Option α
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.val_toZMod_eq_zmodRepr : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]), (PadicInt.toZMod x).val = x.zmodRepr
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.dist_eq_iff_eq_sinh : ∀ {z w : UpperHalfPlane} {r : ℝ}, dist z w = r ↔ dist ↑z ↑w / (2 * √(z.im * w.im)) = Real.sinh (r / 2)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.counitIso_hom_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (adj : F ⊣ G)
  (X : CategoryTheory.Endofunctor.Coalgebra G),
  ((CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.counitIso adj).hom.app X).f =
    CategoryTheory.CategoryStruct.id X.V
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
/-- If the terminal comparison map for `G` is an isomorphism, then `G` preserves terminal objects.
 -/
CategoryTheory.Limits.PreservesTerminal.of_iso_comparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) [inst_2 : CategoryTheory.Limits.HasTerminal C]
  [inst_3 : CategoryTheory.Limits.HasTerminal D]
  [i : CategoryTheory.IsIso (CategoryTheory.Limits.terminalComparison G)],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k fallback : α}, (m₁ \ m₂).getKeyD k fallback = if k ∈ m₂ then fallback else m₁.getKeyD k fallback
-- Mathlib.Algebra.Order.Group.Synonym
toLex_vadd : ∀ {β : Type u_2} {α : Type u_1} [inst : VAdd β α] (b : β) (a : α), toLex (b +ᵥ a) = b +ᵥ toLex a
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.compFlipUncurryIso_hom_app : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  {D : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor B D)
  (G : CategoryTheory.Functor D (CategoryTheory.Functor C E)) (X : C × B),
  (F.compFlipUncurryIso G).hom.app X = CategoryTheory.CategoryStruct.id ((G.obj (F.obj X.2)).obj X.1)
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.toSubalgebra_lt_toSubalgebra : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  {S S' : IntermediateField K L}, S.toSubalgebra < S'.toSubalgebra ↔ S < S'
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.Try.TacticResult : Type → Type
-- Mathlib.Algebra.Order.Interval.Basic
Interval.bot_nsmul : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : Preorder α] [inst_2 : IsOrderedAddMonoid α] {n : ℕ},
  n ≠ 0 → n • ⊥ = ⊥
-- Mathlib.Algebra.Group.Subgroup.Order
AddSubsemigroup.strictMono_topEquiv : ∀ {G : Type u_1} [inst : AddCommMonoid G] [inst_1 : Preorder G], StrictMono ⇑AddSubsemigroup.topEquiv
-- Mathlib.Data.ENNReal.Inv
ENNReal.mulLeftOrderIso_symm_apply : ∀ (a : ENNReal) (ha : IsUnit a) (x : ENNReal), (RelIso.symm (a.mulLeftOrderIso ha)) x = ↑ha.unit⁻¹ * x
-- Mathlib.Algebra.Lie.Basic
LieHom.mk.inj : ∀ {R : Type u_1} {L : Type u_2} {L' : Type u_3} {inst : CommRing R} {inst_1 : LieRing L} {inst_2 : LieAlgebra R L}
  {inst_3 : LieRing L'} {inst_4 : LieAlgebra R L'} {toLinearMap : L →ₗ[R] L'}
  {map_lie' : ∀ {x y : L}, toLinearMap.toFun ⁅x, y⁆ = ⁅toLinearMap.toFun x, toLinearMap.toFun y⁆}
  {toLinearMap_1 : L →ₗ[R] L'}
  {map_lie'_1 : ∀ {x y : L}, toLinearMap_1.toFun ⁅x, y⁆ = ⁅toLinearMap_1.toFun x, toLinearMap_1.toFun y⁆},
  { toLinearMap := toLinearMap, map_lie' := map_lie' } = { toLinearMap := toLinearMap_1, map_lie' := map_lie'_1 } →
    toLinearMap = toLinearMap_1
-- Mathlib.Order.Lattice.Nat
Nat.notMem_of_lt_sInf : ∀ {s : Set ℕ} {m : ℕ}, m < sInf s → m ∉ s
-- Init.Data.BitVec.Folds
_private.Init.Data.BitVec.Folds.0.BitVec.iunfoldr.eq_test : ∀ {w : ℕ} {α : Type u_1} {f : Fin w → α → α × Bool} (state : ℕ → α) (value : BitVec w) (a : α),
  state 0 = a →
    (∀ (i : Fin w), f i (state ↑i) = (state (↑i + 1), value.getLsbD ↑i)) →
      BitVec.iunfoldr f a = (state w, BitVec.truncate w value)
-- Mathlib.FieldTheory.IntermediateField.Basic
Subfield.extendScalars.congr_simp : ∀ {L : Type u_2} [inst : Field L] {F E E_1 : Subfield L} (e_E : E = E_1) (h : F ≤ E),
  Subfield.extendScalars h = Subfield.extendScalars ⋯
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.insertMany_nil : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m.insertMany [] = m
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- An object `X` is (right) closed if `(X ⊗ -)` is a left adjoint.  -/
CategoryTheory.Closed : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.MonoidalCategory C] → C → Type (max u v)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_insert_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {a : α} {b : β a}, (t.insert a b).getKey! a = a
-- Mathlib.Algebra.Module.Submodule.Range
Submodule.map_comap_eq_self : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {q : Submodule R₂ M₂},
  q ≤ f.range → Submodule.map f (Submodule.comap f q) = q
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.sum_C_index : ∀ {R : Type u_1} [inst : Semiring R] {a : R} {β : Type u_5} [inst_1 : AddCommMonoid β] {f : ℕ → R → β},
  f 0 0 = 0 → (SkewPolynomial.C a).sum f = f 0 a
-- Mathlib.Dynamics.OmegaLimit
omegaLimit_image_eq : ∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (s : Set α) {α' : Type u_5} (ϕ : τ → α' → β)
  (f : Filter τ) (g : α → α'), omegaLimit f ϕ (g '' s) = omegaLimit f (fun t x => ϕ t (g x)) s
-- Init.SimpLemmas
bne_iff_ne : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a b : α}, (a != b) = true ↔ a ≠ b
-- Init.Data.String.Basic
String.Slice.Pos.prevAux.eq_1 : ∀ {s : String.Slice} (pos : s.Pos) (h : pos ≠ s.startPos),
  pos.prevAux h = String.Slice.Pos.prevAux.go (pos.offset.byteIdx - 1) ⋯
-- Mathlib.Order.Irreducible
infIrred_iff_not_isMax : ∀ {α : Type u_2} [inst : LinearOrder α] {a : α}, InfIrred a ↔ ¬IsMax a
-- Mathlib.Data.Nat.ModEq
Nat.modEq_iff_dvd : ∀ {n a b : ℕ}, a ≡ b [MOD n] ↔ ↑n ∣ ↑b - ↑a
-- Lean.Exception
Lean.Exception.internal.inj : ∀ {id : Lean.InternalExceptionId} {extra : Lean.KVMap} {id_1 : Lean.InternalExceptionId} {extra_1 : Lean.KVMap},
  Lean.Exception.internal id extra = Lean.Exception.internal id_1 extra_1 → id = id_1 ∧ extra = extra_1
-- Mathlib.Algebra.CubicDiscriminant
Cubic.natDegree_of_a_eq_zero : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.a = 0 → P.toPoly.natDegree ≤ 2
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
ClosedSubmodule.mem_iff : ∀ {H : Type u_1} [inst : NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H] (S : ClosedSubmodule ℝ H) {x : H},
  x ∈ S ↔ x ∈ (↑S).carrier
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.whiskerRight : {C : Type u} →
  {X₁ X₂ : CategoryTheory.FreeMonoidalCategory C} →
    X₁.Hom X₂ → (Y : CategoryTheory.FreeMonoidalCategory C) → (X₁.tensor Y).Hom (X₂.tensor Y)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.mk.sizeOf_spec : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂}
  [inst_3 : SizeOf C₁] [inst_4 : SizeOf C₂] [inst_5 : SizeOf C₃] (pt : C₃) (inl : (F.obj Y₁).obj X₂ ⟶ pt)
  (inr : (F.obj X₁).obj Y₂ ⟶ pt) (isPushout : CategoryTheory.IsPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂) inl inr)
  (ι : pt ⟶ (F.obj Y₁).obj Y₂)
  (inl_ι :
    autoParam (CategoryTheory.CategoryStruct.comp inl ι = (F.obj Y₁).map f₂)
      CategoryTheory.Functor.PushoutObjObj.inl_ι._autoParam)
  (inr_ι :
    autoParam (CategoryTheory.CategoryStruct.comp inr ι = (F.map f₁).app Y₂)
      CategoryTheory.Functor.PushoutObjObj.inr_ι._autoParam),
  sizeOf { pt := pt, inl := inl, inr := inr, isPushout := isPushout, ι := ι, inl_ι := inl_ι, inr_ι := inr_ι } =
    1 + sizeOf pt + sizeOf inl + sizeOf inr + sizeOf isPushout + sizeOf ι + sizeOf inl_ι + sizeOf inr_ι
-- Mathlib.Data.Vector.Basic
/-- Variant of `List.Vector.prod_set` that multiplies by the inverse of the replaced element  -/
List.Vector.prod_set' : ∀ {α : Type u_1} {n : ℕ} [inst : CommGroup α] (v : List.Vector α n) (i : Fin n) (a : α),
  (v.set i a).toList.prod = v.toList.prod * (v.get i)⁻¹ * a
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.isClosed_C' : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}},
  IsClosed C → ∀ (ho : o < Ordinal.type fun x1 x2 => x1 < x2), IsClosed (Profinite.NobelingProof.C' C ho)
-- Mathlib.Data.EReal.Operations
EReal.toReal_add : ∀ {x y : EReal}, x ≠ ⊤ → x ≠ ⊥ → y ≠ ⊤ → y ≠ ⊥ → (x + y).toReal = x.toReal + y.toReal
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_bot : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (s : Finset β), (s.sup fun x => ⊥) = ⊥
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
/-- For `K < 1` and `S ⊆ G` finite and nonempty, the value of connectivity is attained by a
nonempty finite subset of `G`. That is, a fragment for given `K` and `S` exists.  -/
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.exists_nonempty_isFragment : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {K : ℝ} {S : Finset G},
  K < 1 → S.Nonempty → ∃ A, A.Nonempty ∧ Finset.IsFragment✝ K S A
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- Given a commutative diagram
```
    X --f--> Y --g--> Z
    |        |        |
    |        |        |
    v        v        v
    X' -f'-> Y' -g'-> Z'
```
with horizontal arrows composing to zero,
then we obtain a commutative square
```
   cokernel f ---> Z
   |               |
   | cokernel.map  |
   |               |
   v               v
   cokernel f' --> Z'
```
 -/
CategoryTheory.Limits.cokernel.map_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y Z X' Y' Z' : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCokernel f] (g : Y ⟶ Z)
  (w : CategoryTheory.CategoryStruct.comp f g = 0) (f' : X' ⟶ Y') [inst_3 : CategoryTheory.Limits.HasCokernel f']
  (g' : Y' ⟶ Z') (w' : CategoryTheory.CategoryStruct.comp f' g' = 0) (p : X ⟶ X') (q : Y ⟶ Y') (r : Z ⟶ Z')
  (h₁ : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p f'),
  CategoryTheory.CategoryStruct.comp g r = CategoryTheory.CategoryStruct.comp q g' →
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.map f f' p q h₁)
        (CategoryTheory.Limits.cokernel.desc f' g' w') =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.desc f g w) r
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.whiskering_obj_obj_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (D : Type u_1) [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (H : CategoryTheory.Functor C D) (F : CategoryTheory.Functor SimplexCategory C) {X Y : SimplexCategory} (f : X ⟶ Y),
  (((CategoryTheory.CosimplicialObject.whiskering C D).obj H).obj F).map f = H.map (F.map f)
-- Mathlib.LinearAlgebra.Dimension.Constructions
/-- The rank of a set of vectors as a natural number.  -/
Set.finrank : (R : Type u) → {M : Type v} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Set M → ℕ
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsCofiltered.instSmallCategorySmallCofilteredIntermediate : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] →
      {D : Type u₁} →
        [inst_2 : CategoryTheory.Category.{v₁, u₁} D] →
          (F : CategoryTheory.Functor D C) →
            CategoryTheory.SmallCategory (CategoryTheory.IsCofiltered.SmallCofilteredIntermediate F)