mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Filter.Cocardinal
/-- The filter defined by all sets that have a complement with at most cardinality `c`. For a union
of `c` sets of `c` elements to have `c` elements, we need that `c` is a regular cardinal.  -/
Filter.cocardinal : (α : Type u) → {c : Cardinal.{u}} → c.IsRegular → Filter α
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
/-- For any subsemiring `R`, not necessarily homogeneous, `R.homogeneousCore 𝒜` is the largest
homogeneous subsemiring contained in `R`.  -/
Subsemiring.homogeneousCore : {ι : Type u_1} →
  {σ : Type u_2} →
    {A : Type u_3} →
      [inst : AddMonoid ι] →
        [inst_1 : Semiring A] →
          [inst_2 : SetLike σ A] →
            [inst_3 : AddSubmonoidClass σ A] →
              (𝒜 : ι → σ) →
                [inst_4 : DecidableEq ι] → [inst_5 : GradedRing 𝒜] → Subsemiring A → HomogeneousSubsemiring 𝒜
-- Mathlib.RingTheory.Smooth.Kaehler
sectionOfRetractionKerToTensor_algebraMap : ∀ {R : Type u_1} {P : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing P] [inst_2 : CommRing S]
  [inst_3 : Algebra R P] [inst_4 : Algebra P S] (l : TensorProduct P S Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S)))
  (hl : l ∘ₗ KaehlerDifferential.kerToTensor R P S = LinearMap.id) [inst_5 : Algebra R S] [inst_6 : IsScalarTower R P S]
  (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥) (hf : Function.Surjective ⇑(algebraMap P S)) (x : P),
  (sectionOfRetractionKerToTensor l hl hf' hf) ((algebraMap P S) x) = x - ↑(l (1 ⊗ₜ[P] (KaehlerDifferential.D R P) x))
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_eq_some_iff_exists_beq_and_mem_toList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {k : α} {v : β},
      Std.DHashMap.Raw.Const.get? m k = some v ↔ ∃ k', (k == k') = true ∧ (k', v) ∈ Std.DHashMap.Raw.Const.toList m
-- Lean.Widget.Commands
Lean.Widget.showWidgetSpec : Lean.ParserDescr
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.isMonicOfDegree_zero_iff : ∀ {R : Type u_1} [inst : Semiring R] {p : Polynomial R}, p.IsMonicOfDegree 0 ↔ p = 1
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.sum_mk : ∀ {α : Type u} {L : List (α × Bool)} [inst : AddGroup α],
  FreeAddGroup.sum (FreeAddGroup.mk L) = (List.map (fun x => bif x.2 then x.1 else -x.1) L).sum
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionHom : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {c c' : Cᵒᵖ} {d d' : Dᵒᵖ} (f : c ⟶ c') (g : d ⟶ d'),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f g =
    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f.unop g.unop).op
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.IsZero.of_epi_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C)
  [CategoryTheory.Epi 0], CategoryTheory.Limits.IsZero Y
-- Init.Data.BitVec.Bitblast
BitVec.intMin_udiv_eq_intMin_iff : ∀ {w : ℕ} (x : BitVec w), BitVec.intMin w / x = BitVec.intMin w ↔ x = 1#w
-- Mathlib.RingTheory.Extension.Cotangent.BaseChange
_private.Mathlib.RingTheory.Extension.Cotangent.BaseChange.0.Algebra.Extension.tensorCotangentOfFlat.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S) (T : Type u_3) [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Module.Flat R T],
  P.tensorCotangentOfFlat T =
    (((TensorProduct.AlgebraTensorModule.congr (LinearEquiv.refl T T)
                  (LinearEquiv.restrictScalars R Algebra.Extension.cotangentEquivCotangentKer)).trans
              (Ideal.tensorCotangentEquiv R T P.ker)).trans
          (LinearEquiv.restrictScalars T
            (Ideal.Cotangent.equivOfEq (Ideal.map Algebra.TensorProduct.includeRight.toRingHom P.ker) P.baseChange.ker
              ⋯))).trans
      (LinearEquiv.restrictScalars T Algebra.Extension.cotangentEquivCotangentKer.symm)
-- Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
MeasureTheory.measure_sigmaFiniteSetGE_le : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [inst : MeasureTheory.IsFiniteMeasure ν]
  (n : ℕ),
  ν (μ.sigmaFiniteSetGE ν n) ≤ ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : MeasureTheory.SigmaFinite (μ.restrict s)), ν s
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.support_of_subset : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] {i : ι} {b : β i}, DFinsupp.support ((DirectSum.of β i) b) ⊆ {i}
-- Mathlib.Topology.Algebra.Group.Basic
/-- If `G` is a group with topological `⁻¹`, then it is homeomorphic to its units.  -/
toUnits_homeomorph : {G : Type w} → [inst : Group G] → [inst_1 : TopologicalSpace G] → [ContinuousInv G] → G ≃ₜ Gˣ
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpInd_of_measurable : ∀ {α : Type u_1} {G : Type u_4} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s : Set α} [inst_1 : NormedSpace ℝ G] {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)]
  (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (c : G),
  (MeasureTheory.condExpInd G hm μ s) c = MeasureTheory.indicatorConstLp 1 ⋯ hμs c
-- Init.Data.Array.Zip
_private.Init.Data.Array.Zip.0.Array.zip.eq_1 : ∀ {α : Type u} {β : Type u_1} (as : Array α) (bs : Array β), as.zip bs = Array.zipWith Prod.mk as bs
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.ext_iff : ∀ {N : Type u_1} {G : Type u_2} {inst : Group N} {inst_1 : Group G} {φ : G →* MulAut N} {x y : N ⋊[φ] G},
  x = y ↔ x.left = y.left ∧ x.right = y.right
-- Mathlib.CategoryTheory.Presentable.Adjunction
CategoryTheory.Adjunction.hasCardinalFilteredGenerator : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v', u'} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (κ : Cardinal.{w})
  [inst_2 : Fact κ.IsRegular] [CategoryTheory.HasCardinalFilteredGenerator C κ] [G.IsCardinalAccessible κ] [G.Full]
  [G.Faithful], CategoryTheory.HasCardinalFilteredGenerator D κ
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.mk.injEq : ∀ {T : Type u_1} (NT : Type) (initial : NT) (rules : Finset (ContextFreeRule T NT)) (NT_1 : Type) (initial_1 : NT_1)
  (rules_1 : Finset (ContextFreeRule T NT_1)),
  ({ NT := NT, initial := initial, rules := rules } = { NT := NT_1, initial := initial_1, rules := rules_1 }) =
    (NT = NT_1 ∧ initial ≍ initial_1 ∧ rules ≍ rules_1)
-- Mathlib.RingTheory.Ideal.Operations
Ideal.mul_mono_right : ∀ {R : Type u} [inst : Semiring R] {I J K : Ideal R}, J ≤ K → I * J ≤ I * K
-- Lean.LibrarySuggestions.Basic
_private.Lean.LibrarySuggestions.Basic.0.Lean.Expr.FoldRelevantConstantsImpl.foldUnsafe : {α : Type} → Lean.Expr → α → (Lean.Name → α → Lean.MetaM α) → Lean.MetaM α
-- Mathlib.Tactic.TacticAnalysis
Mathlib.TacticAnalysis.Config.mk : (Array Mathlib.TacticAnalysis.TacticNode → Lean.Elab.Command.CommandElabM Unit) → Mathlib.TacticAnalysis.Config
-- Batteries.Data.Array.Pairwise
/-- **Alias** of `Array.pairwise_iff_getElem`. -/
Array.pairwise_iff_get : ∀ {α : Type u_1} {R : α → α → Prop} {as : Array α},
  Array.Pairwise R as ↔ ∀ (i j : ℕ) (x : i < as.size) (x_1 : j < as.size), i < j → R as[i] as[j]
-- Init.Data.List.Pairwise
List.pairwise_filter : ∀ {α : Type u_1} {R : α → α → Prop} {p : α → Bool} {l : List α},
  List.Pairwise R (List.filter p l) ↔ List.Pairwise (fun x y => p x = true → p y = true → R x y) l
-- Mathlib.SetTheory.Ordinal.FundamentalSequence
Ordinal.IsFundamentalSequence.zero : ∀ {f : (b : Ordinal.{u_1}) → b < 0 → Ordinal.{u_1}}, Ordinal.IsFundamentalSequence 0 0 f
-- Mathlib.Data.PFunctor.Multivariate.M
MvPFunctor.M.Path.child.sizeOf_spec : ∀ {n : ℕ} {P : MvPFunctor.{u} (n + 1)} (x : P.last.M) (a : P.A) (f : P.last.B a → P.last.M) (h : x.dest = ⟨a, f⟩)
  (j : P.last.B a) (i : Fin2 n) (c : MvPFunctor.M.Path P (f j) i),
  sizeOf (MvPFunctor.M.Path.child x a f h j i c) = 1 + sizeOf x + sizeOf a + sizeOf h + sizeOf j + sizeOf i + sizeOf c
-- Init.Data.Nat.Bitwise.Lemmas
Nat.shiftLeft_eq_zero_iff : ∀ {a n : ℕ}, a <<< n = 0 ↔ a = 0
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.instSmallHomDerivedCategoryObjSingleFunctorOfHasExt : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] [CategoryTheory.HasExt C]
  (X Y : C) (a b : ℤ) [inst_3 : HasDerivedCategory C],
  Small.{w, w'} ((DerivedCategory.singleFunctor C a).obj X ⟶ (DerivedCategory.singleFunctor C b).obj Y)
-- Mathlib.Algebra.Lie.TransferInstance
/-- Transfer `LieRing` across an `Equiv`  -/
Equiv.lieRing : {L' : Type u_2} → {L : Type u_3} → [LieRing L] → L' ≃ L → LieRing L'
-- Mathlib.Order.Basic
Function.const_le_const : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [Nonempty β] {a b : α},
  Function.const β a ≤ Function.const β b ↔ a ≤ b
-- Mathlib.Computability.MyhillNerode
Language.IsRegular.of_finite_range_leftQuotient : ∀ {α : Type u} {L : Language α}, (Set.range L.leftQuotient).Finite → L.IsRegular
-- Mathlib.Logic.Function.Defs
Function.IsFixedPt.of_subsingleton : ∀ {α : Type u₁} [Subsingleton α] (f : α → α) (x : α), Function.IsFixedPt f x
-- Mathlib.GroupTheory.Perm.Closure
Equiv.Perm.closure_prime_cycle_swap : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {σ τ : Equiv.Perm α},
  Nat.Prime (Fintype.card α) → σ.IsCycle → σ.support = Finset.univ → τ.IsSwap → Subgroup.closure {σ, τ} = ⊤
-- Mathlib.Order.Interval.Finset.Defs
/-- The finset $(a, b)$ of elements `x` such that `a < x` and `x < b`. Basically `Set.Ioo a b` as a
finset.  -/
Finset.Ioo : {α : Type u_1} → [inst : Preorder α] → [LocallyFiniteOrder α] → α → α → Finset α
-- Init.Data.Fin.Basic
Fin.instOrOp : {n : ℕ} → OrOp (Fin n)
-- Std.Tactic.BVDecide.LRAT.Actions
Std.Tactic.BVDecide.LRAT.instBEqAction : {β : Type u_1} → {α : Type u_2} → [BEq β] → [BEq α] → BEq (Std.Tactic.BVDecide.LRAT.Action β α)
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.neg_norm_le_apply : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] (f : C(α, ℝ)) (x : α), -‖f‖ ≤ f x
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.w_mk : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {X Y X' Y' : T} {f : X ⟶ Y} {g : X' ⟶ Y'}
  (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left sq) g =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.Arrow.Hom.right sq)
-- Aesop.RuleSet
/-- The simp theorems array must contain at least one `SimpTheorems` structure.
When a simp theorem is added to a `LocalRuleSet`, it is stored in this first
`SimpTheorems` structure.
 -/
Aesop.LocalRuleSet.simpTheoremsArrayNonempty : ∀ (self : Aesop.LocalRuleSet), 0 < self.simpTheoremsArray.size
-- Mathlib.Tactic.DeriveEncodable
_private.Mathlib.Tactic.DeriveEncodable.0.Mathlib.Deriving.Encodable.mkToSMatch : Lean.Elab.Deriving.Context →
  Lean.Elab.Deriving.Header → Lean.InductiveVal → Array Lean.Name → Lean.Elab.TermElabM Lean.Term
-- Mathlib.RingTheory.Localization.Finiteness
/-- If `M` is an `R' = S⁻¹R` module, and `x ∈ span R' s`,
then `t • x ∈ span R s` for some `t : S`.  -/
multiple_mem_span_of_mem_localization_span : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (R' : Type u_3) [inst_1 : CommSemiring R']
  [inst_2 : Algebra R R'] {N : Type u_5} [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : Module R' N]
  [IsScalarTower R R' N] [IsLocalization M R'] (s : Set N), ∀ x ∈ Submodule.span R' s, ∃ t, t • x ∈ Submodule.span R s
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.cliqueSet_eq_image : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) [inst : DecidableEq α] [inst_1 : DecidableEq β]
  [inst_2 : DecidableEq γ] [SimpleGraph.TripartiteFromTriangles.NoAccidental t],
  (SimpleGraph.TripartiteFromTriangles.graph t).cliqueSet 3 = ⇑SimpleGraph.TripartiteFromTriangles.toTriangle '' ↑t
-- Mathlib.Topology.Connected.PathConnected
mem_pathComponent_self : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x : X), x ∈ pathComponent x
-- Mathlib.Data.Set.Image
Set.range_inr_union_range_inl : ∀ {α : Type u_1} {β : Type u_2}, Set.range Sum.inr ∪ Set.range Sum.inl = Set.univ
-- Mathlib.Data.Num.Lemmas
PosNum.cmp.eq_def : ∀ (x x_1 : PosNum),
  x.cmp x_1 =
    match x, x_1 with
    | PosNum.one, PosNum.one => Ordering.eq
    | x, PosNum.one => Ordering.gt
    | PosNum.one, x => Ordering.lt
    | a.bit0, b.bit0 => a.cmp b
    | a.bit0, b.bit1 => Ordering.casesOn (a.cmp b) Ordering.lt Ordering.lt Ordering.gt
    | a.bit1, b.bit0 => Ordering.casesOn (a.cmp b) Ordering.lt Ordering.gt Ordering.gt
    | a.bit1, b.bit1 => a.cmp b
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- If `G` acts transitively on `X`, and the orbit map of a point in `X` is a proper map, then the
action is proper.  -/
MulAction.properSMul_of_proper_orbitMap : ∀ {G : Type u_1} {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X] [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace X] [ContinuousSMul G X] [IsTopologicalGroup G] [MulAction.IsPretransitive G X] {x : X},
  (IsProperMap fun g => g • x) → ProperSMul G X
-- Mathlib.Probability.HasLaw
ProbabilityTheory.HasLaw.covariance_comp : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {μ : MeasureTheory.Measure 𝓧} {P : MeasureTheory.Measure Ω},
  ProbabilityTheory.HasLaw X μ P →
    ∀ {f g : 𝓧 → ℝ},
      AEMeasurable f μ →
        AEMeasurable g μ → ProbabilityTheory.covariance (f ∘ X) (g ∘ X) P = ProbabilityTheory.covariance f g μ
-- Mathlib.Data.Fintype.Basic
/-- Embed `Fin n` into `Fin (n + 1)` by inserting
around a specified pivot `p : Fin (n + 1)` into the `univ`  -/
Fin.univ_succAbove : ∀ (n : ℕ) (p : Fin (n + 1)), Finset.univ = Finset.cons p (Finset.map p.succAboveEmb Finset.univ) ⋯
-- Mathlib.Algebra.Lie.TraceForm
LieIdeal.le_killingCompl_top_of_isLieAbelian : ∀ (R : Type u_1) (L : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L)
  [Module.Free R L] [Module.Finite R L] [IsDomain R] [IsPrincipalIdealRing R] [IsLieAbelian ↥I],
  I ≤ LieIdeal.killingCompl R L ⊤
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.volume_pi : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasureTheory.MeasureSpace (α i)],
  MeasureTheory.volume = MeasureTheory.Measure.pi fun x => MeasureTheory.volume
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.isGE_iff_isIso_truncGEπ_app : ∀ {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 : C),
  t.IsGE X n ↔ CategoryTheory.IsIso ((t.truncGEπ n).app X)
-- Std.Time.DateTime.WallTime
Std.Time.instToStringWallTime : ToString Std.Time.WallTime
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- The type of arrows for the shape indexing a wide pushout.  -/
CategoryTheory.Limits.WidePushoutShape.Hom : {J : Type w} → CategoryTheory.Limits.WidePushoutShape J → CategoryTheory.Limits.WidePushoutShape J → Type w
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.Hom.equivAlgHom_apply_coe : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P : Algebra.Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [inst_3 : CommRing R']
  [inst_4 : CommRing S'] [inst_5 : Algebra R' S'] {P' : Algebra.Generators R' S' ι'} [inst_6 : Algebra R R']
  [inst_7 : Algebra S S'] [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S']
  (f : P.Hom P'), ↑(Algebra.Generators.Hom.equivAlgHom f) = f.toAlgHom
-- Init.Data.List.Basic
List.decidableLex : {α : Type u} →
  [DecidableEq α] → (r : α → α → Prop) → [h : DecidableRel r] → (l₁ l₂ : List α) → Decidable (List.Lex r l₁ l₂)
-- Init.Data.Int.Order
Int.le_max_right : ∀ (a b : ℤ), b ≤ max a b
-- Init.Data.Iterators.Lemmas.Combinators.Attach
Std.Iter.toListRev_attachWith : ∀ {α β : Type u_1} {P : β → Prop} [inst : Std.Iterator α Id β] {it : Std.Iter β}
  {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out} [inst_1 : Std.Iterators.Finite α Id],
  (it.attachWith P hP).toListRev = it.toListRev.attachWith P ⋯
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.FunctorPushforwardStructure.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} {X : C} {S : CategoryTheory.Presieve X} {Y : D} {f : Y ⟶ F.obj X} {preobj : C}
  {premap : preobj ⟶ X} {lift : Y ⟶ F.obj preobj} {cover : S premap}
  {fac : f = CategoryTheory.CategoryStruct.comp lift (F.map premap)} {preobj_1 : C} {premap_1 : preobj_1 ⟶ X}
  {lift_1 : Y ⟶ F.obj preobj_1} {cover_1 : S premap_1}
  {fac_1 : f = CategoryTheory.CategoryStruct.comp lift_1 (F.map premap_1)},
  { preobj := preobj, premap := premap, lift := lift, cover := cover, fac := fac } =
      { preobj := preobj_1, premap := premap_1, lift := lift_1, cover := cover_1, fac := fac_1 } →
    preobj = preobj_1 ∧ premap ≍ premap_1 ∧ lift ≍ lift_1
-- Init.Data.Array.Lemmas
/-- `map_id'` differs from `map_id` by representing the identity function as a lambda, rather than `id`.  -/
Array.map_id' : ∀ {α : Type u_1} (xs : Array α), Array.map (fun a => a) xs = xs
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.ofEpiOfIsIsoOfMono_φK : ∀ {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₁.LeftHomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.LeftHomologyMapData.ofEpiOfIsIsoOfMono φ h).φK = CategoryTheory.CategoryStruct.id h.K
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.sum_zero : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [inst : Countable ι],
  (ProbabilityTheory.Kernel.sum fun x => 0) = 0
-- Mathlib.Data.FunLike.Equiv
/-- The class `EquivLike E α β` expresses that terms of type `E` have an
injective coercion to bijections between `α` and `β`.

Note that this does not directly extend `FunLike`, nor take `FunLike` as a parameter,
so we can state `coe_injective'` in a nicer way.

This typeclass is used in the definition of the isomorphism (or equivalence) typeclasses,
such as `ZeroEquivClass`, `MulEquivClass`, `MonoidEquivClass`, ....
 -/
EquivLike : Sort u_1 → outParam (Sort u_2) → outParam (Sort u_3) → Sort (max (max (max 1 u_1) u_2) u_3)
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.derivedSeriesOfIdeal_antitone : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L)
  {k l : ℕ}, l ≤ k → LieAlgebra.derivedSeriesOfIdeal R L k I ≤ LieAlgebra.derivedSeriesOfIdeal R L l I
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- Every connected graph has a spanning tree.  -/
SimpleGraph.Connected.exists_isTree_le : ∀ {V : Type u_1} {G : SimpleGraph V}, G.Connected → ∃ T ≤ G, T.IsTree
-- Mathlib.RingTheory.Flat.Basic
IsSMulRegular.of_flat_of_isBaseChange : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [Module.Flat R S] [inst_4 : AddCommMonoid M] [inst_5 : Module R M] [inst_6 : AddCommMonoid N]
  [inst_7 : Module R N] [inst_8 : Module S N] [inst_9 : IsScalarTower R S N] {f : M →ₗ[R] N},
  IsBaseChange S f → ∀ {x : R}, IsSMulRegular M x → IsSMulRegular N ((algebraMap R S) x)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_diff_le_size_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (m₁ \ m₂).size ≤ m₁.size
-- Init.Data.Nat.Lemmas
Nat.dvd_add_left : ∀ {a b c : ℕ}, a ∣ c → (a ∣ b + c ↔ a ∣ b)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.ExprCnstr : Type
-- Init.Data.List.Sublist
List.infix_refl : ∀ {α : Type u_1} (l : List α), l <:+: l
-- Mathlib.Algebra.Homology.ConcreteCategory
/-- Constructor for cycles of a homological complex in a concrete category.  -/
HomologicalComplex.cyclesMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_1} →
      {CC : C → Type v} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory C FC] →
            [inst_3 : CategoryTheory.HasForget₂ C Ab] →
              [inst_4 : CategoryTheory.Abelian C] →
                [inst_5 : (CategoryTheory.forget₂ C Ab).Additive] →
                  [(CategoryTheory.forget₂ C Ab).PreservesHomology] →
                    {ι : Type u_2} →
                      {c : ComplexShape ι} →
                        (K : HomologicalComplex C c) →
                          {i : ι} →
                            (x : ↑((CategoryTheory.forget₂ C Ab).obj (K.X i))) →
                              (j : ι) →
                                c.next i = j →
                                  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map (K.d i j)))
                                        x =
                                      0 →
                                    ↑((CategoryTheory.forget₂ C Ab).obj (K.cycles i))
-- Mathlib.Data.List.Defs
List.permutations'.eq_def : ∀ {α : Type u_1} (x : List α),
  x.permutations' =
    match x with
    | [] => [[]]
    | t :: ts => List.flatMap (List.permutations'Aux t) ts.permutations'
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unmop_rightUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).unmop = CategoryTheory.MonoidalCategoryStruct.leftUnitor X.unmop
-- Mathlib.Algebra.Order.GroupWithZero.Basic
Right.neg_of_mul_neg_left : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b : α} [inst_1 : LinearOrder α] [MulPosMono α], a * b < 0 → 0 ≤ b → a < 0
-- Mathlib.Computability.TuringMachine.StackTuringMachine
/-- The TM2 statement corresponding to a stack action.  -/
Turing.TM2to1.stRun : {K : Type u_1} →
  {Γ : K → Type u_2} →
    {Λ : Type u_3} →
      {σ : Type u_4} → {k : K} → Turing.TM2to1.StAct K Γ σ k → Turing.TM2.Stmt Γ Λ σ → Turing.TM2.Stmt Γ Λ σ
-- Mathlib.CategoryTheory.Limits.Preserves.Limits
CategoryTheory.ι_preservesColimitIso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J]
  (F : CategoryTheory.Functor J C) [inst_3 : CategoryTheory.Limits.PreservesColimit F G]
  [inst_4 : CategoryTheory.Limits.HasColimit F] (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.comp G) j)
      (CategoryTheory.preservesColimitIso G F).inv =
    G.map (CategoryTheory.Limits.colimit.ι F j)
-- Mathlib.Topology.MetricSpace.Closeds
TopologicalSpace.Compacts.isometry_singleton : ∀ {α : Type u_1} [inst : EMetricSpace α], Isometry fun x => {x}
-- Mathlib.FieldTheory.Relrank
Subfield.relrank_eq_one_iff : ∀ {E : Type v} [inst : Field E] {A B : Subfield E}, A.relrank B = 1 ↔ B ≤ A
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.BitVec.xor_beq_zero_iff : ∀ {w : ℕ} (a b : BitVec w), (a ^^^ b == 0#w) = (a == b)
-- Lean.Declaration
_private.Lean.Declaration.0.Lean.RecursorVal.getMajorInduct.go : ℕ → Lean.Expr → Lean.Name