mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
/-- The map `H^n(fg) ⟶ H^n(g)` factors through `Z^n(f, g)`.  -/
CategoryTheory.Abelian.SpectralObject.toCycles : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          (X : CategoryTheory.Abelian.SpectralObject C ι) →
            {i j k : ι} →
              (f : i ⟶ j) →
                (g : j ⟶ k) →
                  (fg : i ⟶ k) →
                    CategoryTheory.CategoryStruct.comp f g = fg →
                      (n : ℤ) → (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ fg) ⟶ X.cycles f g n
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.vars_monomial_single : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (i : σ) {e : ℕ} {r : R},
  e ≠ 0 → r ≠ 0 → ((MvPolynomial.monomial fun₀ | i => e) r).vars = {i}
-- Mathlib.Topology.Algebra.Monoid
Submonoid.le_topologicalClosure : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Monoid M] [inst_2 : SeparatelyContinuousMul M] (s : Submonoid M),
  s ≤ s.topologicalClosure
-- Mathlib.Order.Basic
lt_update_self_iff : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : DecidableEq ι] [inst_1 : (i : ι) → Preorder (π i)] {x : (i : ι) → π i}
  {i : ι} {a : π i}, x < Function.update x i a ↔ x i < a
-- Mathlib.Topology.Algebra.Module.LocallyConvex
LocallyConvexSpace.toLocallyPathConnectedSpace : ∀ (E : Type u_2) [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [IsTopologicalAddGroup E] [inst_3 : Module ℝ E]
  [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E], LocallyPathConnectedSpace E
-- Mathlib.Order.RelClasses
instIsLinearOrderGe : ∀ {α : Type u} [inst : LinearOrder α], IsLinearOrder α fun x1 x2 => x2 ≤ x1
-- Mathlib.Order.Filter.Map
/-- **Alias** of the reverse direction of `Filter.map_surjOn_Iic_iff_surjOn`. -/
Set.SurjOn.filter_map_Iic : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {m : α → β},
  Set.SurjOn m s t → Set.SurjOn (Filter.map m) (Set.Iic (Filter.principal s)) (Set.Iic (Filter.principal t))
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instToJsonServerCapabilities.toJson : Lean.Lsp.ServerCapabilities → Lean.Json
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.remove_add_cancel : ∀ {assignment : Std.Tactic.BVDecide.LRAT.Internal.Assignment} {b : Bool},
  ¬Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment b assignment = true →
    Std.Tactic.BVDecide.LRAT.Internal.Assignment.removeAssignment b
        (Std.Tactic.BVDecide.LRAT.Internal.Assignment.addAssignment b assignment) =
      assignment
-- Init.Conv
/-- `simp?` takes the same arguments as `simp`, but reports an equivalent call to `simp only`
that would be sufficient to close the goal. See the `simp?` tactic for more information.  -/
Lean.Parser.Tactic.Conv.dsimpTrace : Lean.ParserDescr
-- Mathlib.Algebra.Ring.Action.Invariant
/-- A typeclass for subrings invariant under a `MulSemiringAction`.  -/
IsInvariantSubring : (M : Type u_1) → {R : Type u_2} → [inst : Monoid M] → [inst_1 : Ring R] → [MulSemiringAction M R] → Subring R → Prop
-- Mathlib.Tactic.Linter.Style
/-- The number of lines that the `longFile` linter considers the default.  -/
Mathlib.Linter.linter.style.longFileDefValue : Lean.Option ℕ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_insert! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] (h : t.WF) {k a : α} {v : β k} {h₁ : a ∈ Std.DTreeMap.Internal.Impl.insert! k v t},
  (Std.DTreeMap.Internal.Impl.insert! k v t).get a h₁ = if h₂ : compare k a = Ordering.eq then cast ⋯ v else t.get a ⋯
-- Lean.Data.Lsp.TextSync
Lean.Lsp.DidOpenTextDocumentParams.mk.inj : ∀ {textDocument textDocument_1 : Lean.Lsp.TextDocumentItem},
  { textDocument := textDocument } = { textDocument := textDocument_1 } → textDocument = textDocument_1
-- Std.Data.ByteSlice
/-- Extracts a byte from the byte slice.

The index is relative to the start of the byte slice, rather than the underlying byte array.
 -/
ByteSlice.get : (s : ByteSlice) → Fin s.size → UInt8
-- Mathlib.Topology.UniformSpace.Cauchy
/-- A filter `f` is Cauchy if for every entourage `r`, there exists an
`s ∈ f` such that `s × s ⊆ r`. This is a generalization of Cauchy
sequences, because if `a : ℕ → α` then the filter of sets containing
cofinitely many of the `a n` is Cauchy iff `a` is a Cauchy sequence.  -/
Cauchy : {α : Type u} → [uniformSpace : UniformSpace α] → Filter α → Prop
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
/-- `Γ(𝒪ₓ/I, U) ≅ 𝒪ₓ(U)/I(U)`.  -/
AlgebraicGeometry.Scheme.IdealSheafData.subschemeObjIso : {X : AlgebraicGeometry.Scheme} →
  (I : X.IdealSheafData) →
    (U : ↑X.affineOpens) →
      I.subscheme.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map I.subschemeι.base).obj ↑U)) ≅
        CommRingCat.of (↑(X.presheaf.obj (Opposite.op ↑U)) ⧸ I.ideal U)
-- Mathlib.Order.Heyting.Basic
/-- **Alias** of the forward direction of `hnot_le_comm`. -/
hnot_le_of_hnot_le : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a b : α}, ￢b ≤ a → ￢a ≤ b
-- Mathlib.Analysis.Complex.Trigonometric
Real.tanh_lt_one : ∀ (x : ℝ), Real.tanh x < 1
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.op_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ⟶ G) (X : Cᵒᵖ),
  (CategoryTheory.NatTrans.op α).app X = (α.app (Opposite.unop X)).op
-- Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
CategoryTheory.SimplicialObject.Homotopy.map_homology_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {X Y : CategoryTheory.SimplicialObject C} {f g : X ⟶ Y} [inst_2 : CategoryTheory.CategoryWithHomology C]
  (H : CategoryTheory.SimplicialObject.Homotopy f g) (n : ℕ),
  (HomologicalComplex.homologyFunctor C (ComplexShape.down ℕ) n).map
      ((AlgebraicTopology.alternatingFaceMapComplex C).map f) =
    (HomologicalComplex.homologyFunctor C (ComplexShape.down ℕ) n).map
      ((AlgebraicTopology.alternatingFaceMapComplex C).map g)
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.dist_r_b' : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r),
  ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), ‖↑(r i n) - b i * ↑n‖ ≤ ↑n / Real.log ↑n ^ 2
-- Mathlib.Algebra.Group.Ext
AddGroup.ext_iff : ∀ {G : Type u_1} {g₁ g₂ : AddGroup G}, g₁ = g₂ ↔ HAdd.hAdd = HAdd.hAdd
-- Lean.Elab.Coinductive
/-- Constructor refs from the original `InductiveView` -/
Lean.Elab.Command.CoinductiveElabData.ctorSyntax : Lean.Elab.Command.CoinductiveElabData → Array Lean.Syntax
-- Init.Data.List.Nat.Prod
List.prod_reverse_nat : ∀ (xs : List ℕ), xs.reverse.prod = xs.prod
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.Context.mk.sizeOf_spec : ∀ (insideType : Bool), sizeOf { insideType := insideType } = 1 + sizeOf insideType
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.isPreconnected_finite_subsets : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α}, IsPreconnected s → IsPreconnected {K | (↑K).Finite ∧ ↑K ⊆ s}
-- Mathlib.Probability.Distributions.Pareto
/-- The pdf of the Pareto distribution integrates to `1`.  -/
ProbabilityTheory.lintegral_paretoPDF_eq_one : ∀ {t r : ℝ}, 0 < t → 0 < r → ∫⁻ (x : ℝ), ProbabilityTheory.paretoPDF t r x = 1
-- Mathlib.MeasureTheory.Measure.Haar.OfBasis
instIsAddHaarMeasureVolume : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E], MeasureTheory.volume.IsAddHaarMeasure
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_fst_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) {Z_1 : C} (h : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst f g)
          (CategoryTheory.Limits.pullback.fst f g))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f)
      h
-- Std.Do.WP.SimpLemmas
Std.Do.WP.liftWith_ReaderT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ρ α : Type u} {Q : Std.Do.PostCond α (Std.Do.PostShape.arg ρ ps)}
  [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] (f : ({β : Type u} → ReaderT ρ m β → m β) → m α),
  (Std.Do.wp (MonadControl.liftWith f)).apply Q = fun s =>
    (Std.Do.wp (f fun {β} x => x.run s)).apply (fun a => Q.1 a s, Q.2)
-- Mathlib.Algebra.Group.TypeTags.Finite
Additive.fintype : {α : Type u} → [Fintype α] → Fintype (Additive α)
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.sigma_zero_apply : ∀ (n : ℕ), (ArithmeticFunction.sigma 0) n = n.divisors.card
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.l_hom : {C : Type u} → (X : CategoryTheory.FreeMonoidalCategory C) → (CategoryTheory.FreeMonoidalCategory.unit.tensor X).Hom X
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0to1.Λ'.act.injEq : ∀ {Γ : Type u_1} {Λ : Type u_2} (a : Turing.TM0.Stmt Γ) (a_1 : Λ) (a_2 : Turing.TM0.Stmt Γ) (a_3 : Λ),
  (Turing.TM0to1.Λ'.act a a_1 = Turing.TM0to1.Λ'.act a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Topology.Algebra.InfiniteSum.Order
tprod_le_one : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α}, (∀ (i : ι), f i ≤ 1) → ∏'[L] (i : ι), f i ≤ 1
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableOn.div : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {F' : Type u_21}
  [inst_6 : NormedDivisionRing F'] [inst_7 : NormedAlgebra 𝕜 F'] {p q : M → F'},
  MDiff[s] p → MDiff[s] q → (∀ z ∈ s, q z ≠ 0) → MDiff[s] (p / q)
-- Mathlib.MeasureTheory.Measure.AddContent
_private.Mathlib.MeasureTheory.Measure.AddContent.0.MeasureTheory.AddContent.supClosureFun_apply : ∀ {α : Type u_1} {C : Set (Set α)} {G : Type u_2} [inst : AddCommMonoid G],
  MeasureTheory.IsSetSemiring C →
    ∀ (m : MeasureTheory.AddContent G C) {s : Set α} {J : Finset (Set α)},
      ↑J ⊆ C → (↑J).PairwiseDisjoint id → s = ⋃₀ ↑J → MeasureTheory.AddContent.supClosureFun✝ m s = ∑ s ∈ J, m s
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.measure_iUnion : ∀ {ι : Type u_1} {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {f : ι → Set α},
  Pairwise (Function.onFun Disjoint f) → (∀ (i : ι), MeasurableSet (f i)) → μ (⋃ i, f i) = ∑' (i : ι), μ (f i)
-- Mathlib.CategoryTheory.Limits.IsConnected
CategoryTheory.Limits.Types.pUnitCocone_ι : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.Limits.Types.pUnitCocone C).ι =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.Types.constPUnitFunctor C)
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.map_comp_map : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] (N : Subgroup G) [nN : N.Normal] {I : Type u_5}
  [inst_2 : Group I] (M : Subgroup H) (O : Subgroup I) [inst_3 : M.Normal] [inst_4 : O.Normal] (f : G →* H) (g : H →* I)
  (hf : N ≤ Subgroup.comap f M) (hg : M ≤ Subgroup.comap g O) (hgf : optParam (N ≤ Subgroup.comap (g.comp f) O) ⋯),
  (QuotientGroup.map M O g hg).comp (QuotientGroup.map N M f hf) = QuotientGroup.map N O (g.comp f) hgf
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.balRight.match_1.eq_3 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (l : RBTree.RBNode α)
  (h_1 :
    (a : RBTree.RBNode α) → (x : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.black a x b))
  (h_2 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.black b y c)))
  (h_3 : (l : RBTree.RBNode α) → motive l),
  (∀ (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α), l = RBTree.RBNode.node RBTree.RBColor.black a x b → False) →
    (∀ (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α) (y : α) (c : RBTree.RBNode α),
        l = RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.black b y c) → False) →
      (match l with
        | RBTree.RBNode.node RBTree.RBColor.black a x b => h_1 a x b
        | RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.black b y c) => h_2 a x b y c
        | l => h_3 l) =
        h_3 l
-- Lean.Util.Sorry
/-- Returns `true` if the expression is of the form `sorryAx _ true ..`.  -/
Lean.Expr.isSyntheticSorry : Lean.Expr → Bool
-- Mathlib.RingTheory.HopfAlgebra.GroupLike
GroupLike.val_inv : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : HopfAlgebra R A]
  (a : GroupLike R A), ↑a⁻¹ = (HopfAlgebraStruct.antipode R) ↑a
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.baseChange_a₃ : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve.Affine R) (S : Type s) [inst_1 : CommRing S]
  [inst_2 : Algebra R S], (W.baseChange S).a₃ = (algebraMap R S) W.a₃
-- Mathlib.Data.ENat.Defs
/-- Extended natural numbers `ℕ∞ = WithTop ℕ`.  -/
ENat : Type
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.mono_of_stalk_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {FC : C → C → Type u_1} {CC : C → Type v} [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
  [instCC : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C]
  [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms]
  {F G : TopCat.Sheaf C X} (f : F ⟶ G) [∀ (x : ↑X), CategoryTheory.Mono ((TopCat.Presheaf.stalkFunctor C x).map f.hom)],
  CategoryTheory.Mono f
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_insertEntry_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k fallback : α} {v : β k},
  Std.Internal.List.getKeyD k (Std.Internal.List.insertEntry k v l) fallback = k
-- Mathlib.FieldTheory.Finite.Basic
/-- **Fermat's Little Theorem**: for every unit `a` of `ZMod p`, we have `a ^ (p - 1) = 1`.  -/
ZMod.units_pow_card_sub_one_eq_one : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (a : (ZMod p)ˣ), a ^ (p - 1) = 1
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Option γ} {k : α},
  k ∈ Std.HashMap.filterMap f m ↔ ∃ (h : k ∈ m), (f (m.getKey k h) m[k]).isSome = true
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
aestronglyMeasurable_add_measure_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [TopologicalSpace.PseudoMetrizableSpace β] {ν : MeasureTheory.Measure α},
  MeasureTheory.AEStronglyMeasurable f (μ + ν) ↔
    MeasureTheory.AEStronglyMeasurable f μ ∧ MeasureTheory.AEStronglyMeasurable f ν
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_eq_iff : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) {a b : α} {n : ℤ}, toIcoDiv hp a b = n ↔ b - n • p ∈ Set.Ico a (a + p)
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
AlgebraicGeometry.instIsMultiplicativeSchemeUniversallyClosed : CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.UniversallyClosed
-- Mathlib.NumberTheory.Padics.PadicNorm
padicNorm.int_lt_one_iff : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (m : ℤ), padicNorm p ↑m < 1 ↔ ↑p ∣ m
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.p_fromOpcycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [inst_2 : K.HasHomology i],
  CategoryTheory.CategoryStruct.comp (K.pOpcycles i) (K.fromOpcycles i j) = K.d i j
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.eLpNorm_ne_top : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f : ↥(MeasureTheory.Lp E p μ)), MeasureTheory.eLpNorm (↑↑f) p μ ≠ ⊤
-- Mathlib.Probability.Independence.BoundedContinuousFunction
indepFun_pi_of_bcf : ∀ {Ω : Type u_1} {T : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {F : T → Type u_5} {G : Type u_6}
  [inst : (t : T) → TopologicalSpace (F t)] [inst_1 : (t : T) → MeasurableSpace (F t)] [∀ (t : T), BorelSpace (F t)]
  [∀ (t : T), HasOuterApproxClosed (F t)] [inst_4 : TopologicalSpace G] [inst_5 : MeasurableSpace G] [BorelSpace G]
  [HasOuterApproxClosed G] {Y : (t : T) → Ω → F t} {Z : Ω → G} [MeasureTheory.IsFiniteMeasure P] [Finite T],
  AEMeasurable Z P →
    (∀ (t : T), AEMeasurable (Y t) P) →
      (∀ (f : BoundedContinuousFunction G ℝ) (g : BoundedContinuousFunction ((t : T) → F t) ℝ),
          ∫ (x : Ω), (fun ω => f (Z ω) * g fun x => Y x ω) x ∂P =
            (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (fun ω => g fun x => Y x ω) x ∂P) →
        ProbabilityTheory.IndepFun Z (fun ω t => Y t ω) P
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_hom_comp_i_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) [inst_2 : S.HasLeftHomology] {Z : C} (h_1 : S.X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.cyclesIso.hom (CategoryTheory.CategoryStruct.comp h.i h_1) =
    CategoryTheory.CategoryStruct.comp S.iCycles h_1
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.lift_symm_apply : ∀ {α : Type u} {β : Type v} [inst : Group β] (g : FreeGroup α →* β) (a : α),
  FreeGroup.lift.symm g a = (⇑g ∘ FreeGroup.of) a
-- Init.Data.Array.Basic
/-- Returns a new array that contains the elements at even indices in `as`, starting with the element at
index `0`.

Examples:
* `#[0, 1, 2, 3, 4].getEvenElems = #[0, 2, 4]`
* `#[1, 2, 3, 4].getEvenElems = #[1, 3]`
* `#["red", "green", "blue"].getEvenElems = #["red", "blue"]`
* `(#[] : Array String).getEvenElems = #[]`
 -/
Array.getEvenElems : {α : Type u} → Array α → Array α
-- Mathlib.RingTheory.Valuation.Integers
Valuation.Integers.le_iff_dvd : ∀ {F : Type u} {Γ₀ : Type v} [inst : Field F] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀}
  {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O F],
  v.Integers O → ∀ {x y : O}, v ((algebraMap O F) x) ≤ v ((algebraMap O F) y) ↔ y ∣ x
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.residueFieldCongr_symm : ∀ {X : AlgebraicGeometry.Scheme} {x y : ↥X} (e : x = y),
  (AlgebraicGeometry.Scheme.residueFieldCongr e).symm = AlgebraicGeometry.Scheme.residueFieldCongr ⋯
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.d.eq_2 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L) (n m : ℕ),
  h.d (Int.negSucc n) (Int.negSucc m) = K.d n m
-- Mathlib.Order.SuccPred.WithBot
WithTop.pred_eq_pred : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderTop α] [inst_2 : PredOrder α] (a : WithTop α),
  ↑a.pred = Order.pred a
-- Lean.PrettyPrinter
/-- Turns a `MetaM FormatWithInfos` into a `MessageData.lazy` which will run the monadic value.
 -/
Lean.MessageData.ofFormatWithInfosM : Lean.MetaM Lean.FormatWithInfos → Lean.MessageData
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.intCast_dvd : ∀ {d : ℤ} (z : ℤ) (a : ℤ√d), ↑z ∣ a ↔ z ∣ a.re ∧ z ∣ a.im
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The canonical map `S.rightHomology ⟶ S.opcycles`.  -/
CategoryTheory.ShortComplex.rightHomologyι : {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.HasRightHomology] → S.rightHomology ⟶ S.opcycles
-- Mathlib.LinearAlgebra.RootSystem.BaseExists
RootPairing.baseOf_root_eq_baseOf_coroot : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [inst : AddCommGroup M]
  [inst_1 : AddCommGroup N] [inst_2 : Field R] [CharZero R] [inst_4 : Module R M] [inst_5 : Module R N]
  (P : RootPairing ι R M N) [P.IsRootSystem] [P.IsCrystallographic] [P.IsReduced] (f : M →+ ℚ),
  (∀ (i : ι), f (P.root i) ≠ 0) →
    ∀ (g : N →+ ℚ),
      (∀ (i : ι), g (P.coroot i) ≠ 0) →
        (∀ (i : ι), 0 < f (P.root i) ↔ 0 < g (P.coroot i)) →
          IsAddIndecomposable.baseOf (⇑P.root) f = IsAddIndecomposable.baseOf (⇑P.coroot) g
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblen_pos : ∀ {o a : Ordinal.{u}}, 0 < Ordinal.veblen o a
-- Mathlib.Data.List.Pairwise
List.pairwise_of_reflexive_of_forall_ne : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α} [Std.Refl R], (∀ a ∈ l, ∀ b ∈ l, a ≠ b → R a b) → List.Pairwise R l
-- Init.Data.String.Search
/-- Returns the first character in `s`. If `s` is empty, returns `none`.

Examples:

* `"abc".front? = some 'a'`

* `"".front? = none`
 -/
String.front? : String → Option Char
-- Init.Data.Float.Model.Float32
/-- Negate a `Float32.Model`.
 -/
Float32.Model.neg : Float32.Model → Float32.Model
-- Mathlib.Data.Nat.Prime.Basic
/-- **Alias** of the forward direction of `Nat.coprime_two_right`. -/
Nat.Coprime.odd_of_right : ∀ {n : ℕ}, n.Coprime 2 → Odd n
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.divRight_eq_mulRight_inv : ∀ {G : Type u_5} [inst : Group G] (a : G), Equiv.divRight a = Equiv.mulRight a⁻¹
-- Mathlib.CategoryTheory.Monoidal.Cartesian.GrpLimits
/-- An auxiliary construction in order to prove that `Grp.forget₂Mon` creates limits.  -/
CategoryTheory.Grp.limitAux : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {J : Type w} →
        [inst_2 : CategoryTheory.Category.{u_2, w} J] →
          [CategoryTheory.Limits.HasLimitsOfShape J C] →
            CategoryTheory.Functor J (CategoryTheory.Grp C) → CategoryTheory.Grp C
-- Mathlib.CategoryTheory.Enriched.Basic
/-- A presheaf isomorphic to the Yoneda embedding of
the `V`-object of natural transformations from `F` to `G`.
 -/
CategoryTheory.enrichedNatTransYoneda : {V : Type v} →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₁} →
        [inst_2 : CategoryTheory.EnrichedCategory V C] →
          {D : Type u₂} →
            [inst_3 : CategoryTheory.EnrichedCategory V D] →
              [CategoryTheory.BraidedCategory V] →
                CategoryTheory.EnrichedFunctor V C D →
                  CategoryTheory.EnrichedFunctor V C D → CategoryTheory.Functor Vᵒᵖ (Type (max u₁ w))
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- A morphism in `SimplexCategory` is an epimorphism if and only if it is a surjective function
 -/
SimplexCategory.epi_iff_surjective : ∀ {n m : SimplexCategory} {f : n ⟶ m}, CategoryTheory.Epi f ↔ Function.Surjective ⇑(SimplexCategory.Hom.toOrderHom f)