mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.coe_vadd : ∀ {G : Type u_1} [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α] [inst_2 : DecidableEq α] {n : ℕ} {g : G}
  {s : ↑(Set.powersetCard α n)}, ↑(g +ᵥ s) = g +ᵥ ↑s
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_sum_right' : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ}
  {s : Finset ι} [MeasureTheory.IsFiniteMeasure μ],
  (∀ i ∈ s, MeasureTheory.MemLp (X i) 2 μ) →
    MeasureTheory.MemLp Y 2 μ →
      ProbabilityTheory.covariance Y (∑ i ∈ s, X i) μ = ∑ i ∈ s, ProbabilityTheory.covariance Y (X i) μ
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.IsReproducing.of_span_eq_top : ∀ {R : Type u_7} {M : Type u_8} [inst : Ring R] [inst_1 : LinearOrder R] [AddLeftStrictMono R] [inst_3 : AddCommGroup M]
  [Nontrivial M] [inst_5 : Module R M] {C : ConvexCone R M}, Submodule.span R ↑C = ⊤ → C.IsReproducing
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteMulSupport.mul : ∀ {α : Type u_1} {M : Type u_3} [inst : MulOneClass M] {f g : α → M},
  Function.HasFiniteMulSupport f → Function.HasFiniteMulSupport g → Function.HasFiniteMulSupport (f * g)
-- Init.ShareCommon
ShareCommon.StateFactoryBuilder.Map : ShareCommon.StateFactoryBuilder → (α : Type) → Type → [BEq α] → [Hashable α] → Type
-- Mathlib.Topology.Homeomorph.Lemmas
/-- `Set.univ X` is homeomorphic to `X`.  -/
Homeomorph.Set.univ : (X : Type u_7) → [inst : TopologicalSpace X] → ↑Set.univ ≃ₜ X
-- Mathlib.NumberTheory.NumberField.Units.Basic
NumberField.Units.coe_neg_one : ∀ {K : Type u_1} [inst : Field K], (algebraMap (NumberField.RingOfIntegers K) K) ↑(-1) = -1
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If the second of three points is strictly between the other two, the angle at that point
is π.  -/
Sbtw.angle₁₂₃_eq_pi : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P}, Sbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi
-- Mathlib.Algebra.GroupWithZero.Submonoid.Instances
MonoidWithZeroHom.mker_inverse : ∀ {H : Type u_2} [inst : CommGroupWithZero H], MonoidHom.mker MonoidWithZero.inverse = ⊥
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalAddGroup.IsSES.integrate.eq_1 : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [inst : AddGroup A] [inst_1 : AddGroup B]
  [inst_2 : AddGroup C] [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C]
  {φ : A →+ B} {ψ : B →+ C} (H : TopologicalAddGroup.IsSES φ ψ) [inst_6 : IsTopologicalAddGroup A]
  [inst_7 : IsTopologicalAddGroup B] [inst_8 : NormedAddCommGroup E] [inst_9 : MeasurableSpace A]
  [inst_10 : BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsAddHaarMeasure] [inst_11 : NormedSpace ℝ E]
  [inst_12 : IsTopologicalAddGroup C] [inst_13 : LocallyCompactSpace B] [inst_14 : MeasurableSpace C]
  [inst_15 : BorelSpace C] (μC : MeasureTheory.Measure C) [hμC : μC.IsAddHaarMeasure],
  H.integrate μA μC = { toFun := fun f => ∫ (c : C), ((H.pushforward μA) f) c ∂μC, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.coe_eval₂Hom : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
  (g : σ → S₁), ⇑(MvPolynomial.eval₂Hom f g) = MvPolynomial.eval₂ f g
-- Init.Data.Nat.Basic
Nat.mul_pred : ∀ (n m : ℕ), n * m.pred = n * m - n
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
/-- An integrability criterion for the continuous functional calculus.
For a version with stronger assumptions which in practice are often easier to verify, see
`integrable_cfc`.  -/
integrable_cfc' : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : MeasurableSpace X]
  {μ : MeasureTheory.Measure X} [inst_2 : NormedRing A] [inst_3 : StarRing A] [inst_4 : NormedAlgebra 𝕜 A]
  [inst_5 : ContinuousFunctionalCalculus 𝕜 A p] [inst_6 : CompleteSpace A] (f : X → 𝕜 → 𝕜) (a : A),
  MeasureTheory.Integrable (fun x => ContinuousMap.mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) μ →
    autoParam (p a) integrable_cfc'._auto_1 → MeasureTheory.Integrable (fun x => cfc (f x) a) μ
-- Mathlib.Data.Fin.Tuple.Basic
Fin.comp_contractNth : ∀ {n : ℕ} {α : Sort u_1} {β : Sort u_2} (opα : α → α → α) (opβ : β → β → β) {f : α → β},
  (∀ (x y : α), f (opα x y) = opβ (f x) (f y)) →
    ∀ (j : Fin (n + 1)) (g : Fin (n + 1) → α), f ∘ j.contractNth opα g = j.contractNth opβ (f ∘ g)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightIso_unitIso_hom_app_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ : CategoryTheory.Functor B T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : R₁ ≅ R₂) (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapRightIso L e).unitIso.hom.app X).left =
    CategoryTheory.CategoryStruct.id X.left
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryLTD.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) (t : Std.DTreeMap.Internal.Impl α fun x => β) (fallback : α × β),
  Std.DTreeMap.Internal.Impl.Const.getEntryLTD k t fallback =
    (Std.DTreeMap.Internal.Impl.Const.getEntryLT? k t).getD fallback
-- Mathlib.Analysis.Calculus.ContDiff.WithLp
contDiff_piLp' : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup H] [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_4 : NormedSpace 𝕜 H] [inst_5 : Fintype ι] (p : ENNReal) [inst_6 : Fact (1 ≤ p)] {n : WithTop ℕ∞}
  {f : H → PiLp p E}, (∀ (i : ι), ContDiff 𝕜 n fun x => (f x).ofLp i) → ContDiff 𝕜 n f
-- Mathlib.Probability.Moments.Variance
/-- The `ℝ≥0∞`-valued variance of the real-valued random variable `X` according to the measure `μ`.

This is defined as the Lebesgue integral of `(X - 𝔼[X])^2`.  -/
ProbabilityTheory.«termEVar[_;_]» : Lean.ParserDescr
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.reflectionPerm_eq_reflectionPerm_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [P.IsRootSystem]
  (i j : ι), P.reflectionPerm i = P.reflectionPerm j ↔ P.reflection i = P.reflection j
-- Mathlib.Order.Defs.LinearOrder
min_eq_left : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a ≤ b → min a b = a
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.toMonoidHom_injective : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N],
  Function.Injective Submonoid.LocalizationMap.toMonoidHom
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.prod_map_div : ∀ {ι : Type u_2} {G : Type u_4} [inst : DivisionCommMonoid G] {m : Multiset ι} {f g : ι → G},
  (Multiset.map (fun i => f i / g i) m).prod = (Multiset.map f m).prod / (Multiset.map g m).prod
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.coreflection_image_eq : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i : ι),
  ⇑(P.coreflection i) '' Set.range ⇑P.coroot = Set.range ⇑P.coroot
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
cyclotomicCharacter.toFun.eq_1 : ∀ {L : Type u} [inst : CommRing L] [inst_1 : IsDomain L] (p : ℕ) [inst_2 : Fact (Nat.Prime p)] (g : L ≃+* L),
  cyclotomicCharacter.toFun p g =
    if H : ∀ (i : ℕ), ∃ ζ, IsPrimitiveRoot ζ (p ^ i) then
      PadicInt.ofIntSeq (fun n => modularCyclotomicCharacter.aux g (p ^ n)) ⋯
    else 1
-- Lean.Structure
/-- Gets the name for a structure constructor where the fields have been fully flattened.
This constructor simulates a flat representation for structures,
and it is used by structure instance notation when elaborating structure fields
and for organizing the fields into subobjects.

The body of the flat constructor has the following properties (recursively):
- the fields come in order
- for subobject fields, the value is the unfolded flat constructor for that field
- for standard fields, the value is one of the flat constructor parameters
 -/
Lean.mkFlatCtorOfStructCtorName : Lean.Name → Lean.Name
-- Lean.Expr
/-- Return `true` if `e` is a non-dependent arrow.
Remark: the following function assumes `e` does not have loose bound variables.
 -/
Lean.Expr.isArrow : Lean.Expr → Bool
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- The `ShortComplex` in `C` associated to a short complex in `Cᵒᵖ`.  -/
CategoryTheory.ShortComplex.unop : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      CategoryTheory.ShortComplex Cᵒᵖ → CategoryTheory.ShortComplex C
-- Lean.Meta.Tactic.Induction
Lean.Meta.AltVarNames.varNames : Lean.Meta.AltVarNames → List Lean.Name
-- Mathlib.CategoryTheory.ObjectProperty.Ind
CategoryTheory.ObjectProperty.instNonemptyInd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} [P.Nonempty],
  P.ind.Nonempty
-- Mathlib.Data.Fin.Basic
Fin.last_pos' : ∀ {n : ℕ} [NeZero n], 0 < Fin.last n
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.comap_zero : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [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₂}
  (q : Submodule R₂ M₂), Submodule.comap 0 q = ⊤
-- Mathlib.Algebra.Order.Module.Defs
PosMulMono.toPosSMulMono : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : Mul α] [inst_2 : Preorder α] [PosMulMono α], PosSMulMono α α
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.isMulLeftInvariant_haarMeasure : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (K₀ : TopologicalSpace.PositiveCompacts G),
  (MeasureTheory.Measure.haarMeasure K₀).IsMulLeftInvariant
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.index_extendMiddle_zero : ∀ {n : ℕ} (c : OrderedFinpartition n) (i : Fin c.length), (c.extendMiddle i).index 0 = i
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- See note [custom simps projection].  -/
ContDiffMapSupportedIn.Simps.coe : {E : Type u_2} →
  {F : Type u_3} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] →
          [inst_3 : NormedSpace ℝ F] →
            {n : ℕ∞} → {K : TopologicalSpace.Compacts E} → ContDiffMapSupportedIn E F n K → E → F
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_insertListConst_of_mem : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k k' : α},
      (k == k') = true →
        List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert →
          k ∈ List.map Prod.fst toInsert →
            Std.Internal.List.getKey? k' (Std.Internal.List.insertListConst l toInsert) = some k
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.isLeftKanExtension_iff_isIso : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  {F' F'' : CategoryTheory.Functor D H} (φ : F' ⟶ F'') {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : F ⟶ L.comp F') (α' : F ⟶ L.comp F''),
  CategoryTheory.CategoryStruct.comp α (L.whiskerLeft φ) = α' →
    ∀ [F'.IsLeftKanExtension α], F''.IsLeftKanExtension α' ↔ CategoryTheory.IsIso φ
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
/-- A sequence of functions `Fₙ` converges locally uniformly to a limiting function `f` with respect
to a filter `p` if, for any entourage of the diagonal `u`, for any `x`, one has `p`-eventually
`(f y, Fₙ y) ∈ u` for all `y` in a neighborhood of `x`.  -/
TendstoLocallyUniformly : {α : Type u_1} →
  {β : Type u_2} → {ι : Type u_4} → [TopologicalSpace α] → [UniformSpace β] → (ι → α → β) → (α → β) → Filter ι → Prop
-- Init.Data.Int.Linear
Int.Internal.Linear.div_eq' : ∀ (a b b' k : ℤ), b = b' → (k == a / b') = true → a / b = k
-- Mathlib.NumberTheory.Cyclotomic.Gal
IsCyclotomicExtension.fromZetaAut.congr_simp : ∀ {n n_1 : ℕ} (e_n : n = n_1) [inst : NeZero n] {K : Type u_1} [inst_1 : Field K] {L : Type u_2} {μ μ_1 : L}
  (e_μ : μ = μ_1) [inst_2 : CommRing L] [inst_3 : IsDomain L] (hμ : IsPrimitiveRoot μ n) [inst_4 : Algebra K L]
  [inst_5 : IsCyclotomicExtension {n} K L] (h : Irreducible (Polynomial.cyclotomic n K)),
  IsCyclotomicExtension.fromZetaAut hμ h = IsCyclotomicExtension.fromZetaAut ⋯ ⋯
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- The product of a family of triangles.  -/
CategoryTheory.Pretriangulated.productTriangle : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      {J : Type u_1} →
        (T : J → CategoryTheory.Pretriangulated.Triangle C) →
          [CategoryTheory.Limits.HasProduct fun j => (T j).obj₁] →
            [CategoryTheory.Limits.HasProduct fun j => (T j).obj₂] →
              [CategoryTheory.Limits.HasProduct fun j => (T j).obj₃] →
                [CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁] →
                  CategoryTheory.Pretriangulated.Triangle C
-- Mathlib.MeasureTheory.Measure.AEDisjoint
/-- **Alias** of `MeasureTheory.AEDisjoint.sdiff_ae_eq_right`. -/
MeasureTheory.AEDisjoint.diff_ae_eq_right : ∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.AEDisjoint μ s t → t \ s =ᵐ[μ] t
-- Mathlib.Algebra.Group.InjSurj
/-- A type has an involutive inversion if it admits a surjective map that preserves `⁻¹` to a type
which has an involutive inversion. See note [reducible non-instances]  -/
Function.Injective.involutiveInv : {M₂ : Type u_2} →
  {M₁ : Type u_3} →
    [inst : Inv M₁] →
      [inst_1 : InvolutiveInv M₂] →
        (f : M₁ → M₂) → Function.Injective f → (∀ (x : M₁), f x⁻¹ = (f x)⁻¹) → InvolutiveInv M₁
-- Init.Tactics
/-- Lifts `let` and `have` expressions within a term as far out as possible.
It is like `extract_lets +lift`, but the top-level lets at the end of the procedure
are not extracted as local hypotheses.

- `lift_lets` lifts let expressions in the target.
- `lift_lets at h` lifts let expressions at the given local hypothesis.

For example,
```lean
example : (let x := 1; x) = 1 := by
  lift_lets
  -- ⊢ let x := 1; x = 1
  ...
```
 -/
Lean.Parser.Tactic.liftLets : Lean.ParserDescr
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Tries different modifiers, logs info messages with modifiers that worked, but returns just the first one that worked.
 -/
Lean.Meta.Grind.mkEMatchTheoremAndSuggest : Lean.Syntax →
  Lean.Name → Lean.Meta.Grind.SymbolPriorities → Bool → optParam Bool false → Lean.MetaM Lean.Meta.Grind.EMatchTheorem
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Syntax.decodeScientificLitVal?.decode : String → String.Pos.Raw → ℕ → Option (ℕ × Bool × ℕ)
-- Init.Data.Order.Lemmas
Classical.Order.instMin : {α : Type u} → [LE α] → Min α
-- Mathlib.Computability.Partrec
/-- Find the smallest `n` satisfying `p n`, where all `p k` for `k < n` are defined as false.
Returns a subtype.  -/
Nat.rfindX : (p : ℕ →. Bool) → (∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom) → { n // true ∈ p n ∧ ∀ m < n, false ∈ p m }
-- Lean.Syntax
Lean.Syntax.getAntiquotTerm : Lean.Syntax → Lean.Syntax
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.isPrimitive_def : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n), χ.IsPrimitive ↔ χ.conductor = n
-- Mathlib.Data.ZMod.Basic
ZMod.val_pow_le : ∀ {m n : ℕ} [Fact (1 < n)] {a : ZMod n}, (a ^ m).val ≤ a.val ^ m
-- Init.Data.List.Count
List.count_tail : ∀ {α : Type u_1} [inst : BEq α] {l : List α} {a : α},
  List.count a l.tail = List.count a l - if (l.head? == some a) = true then 1 else 0
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.toCLM_one : ∀ {𝕜₂ : Type u_2} [inst : NormedField 𝕜₂] {F : Type u_4} [inst_1 : AddCommGroup F] [inst_2 : TopologicalSpace F]
  [inst_3 : Module 𝕜₂ F] [inst_4 : IsTopologicalAddGroup F], ContinuousLinearMapWOT.toCLM 1 = 1
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : ChainComplex C ℕ) [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] {Δ Δ' : SimplexCategoryᵒᵖ}
  (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ) (θ : Δ ⟶ Δ') {Δ'' : SimplexCategory}
  {e : Opposite.unop Δ' ⟶ Δ''} {i : Δ'' ⟶ Opposite.unop A.fst} [inst_3 : CategoryTheory.Epi e]
  [inst_4 : CategoryTheory.Mono i],
  CategoryTheory.CategoryStruct.comp e i = CategoryTheory.CategoryStruct.comp θ.unop A.e →
    ∀ {Z : C} (h : (AlgebraicTopology.DoldKan.Γ₀.obj K).obj Δ' ⟶ Z),
      CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan Δ).inj A)
          (CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.Γ₀.obj K).map θ) h) =
        CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i)
          (CategoryTheory.CategoryStruct.comp
            (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan Δ').inj
              (CategoryTheory.SimplicialObject.Splitting.IndexSet.mk e))
            h)
-- Mathlib.CategoryTheory.Limits.ExactFunctor
/-- Whiskering a left exact functor by a left exact functor yields a left exact functor.  -/
CategoryTheory.LeftExactFunctor.whiskeringLeft : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (E : Type u₃) →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            CategoryTheory.Functor (C ⥤ₗ D) (CategoryTheory.Functor (D ⥤ₗ E) (C ⥤ₗ E))
-- Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
/-- If `n ≥ 5`, then the alternating group on `n` letters is perfect  -/
commutator_alternatingGroup_eq_top : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α], 5 ≤ Nat.card α → commutator ↥(alternatingGroup α) = ⊤
-- Mathlib.Order.Defs.LinearOrder
min_eq_right_of_lt : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, b < a → min a b = b
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.instEDist : {X : Type u_1} → {α : ℝ} → {hα₀ : 0 < α} → {hα₁ : α ≤ 1} → [EDist X] → EDist (Metric.Snowflaking X α hα₀ hα₁)
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the smallest key in the tree map, returning `fallback` if the tree map is empty.
 -/
Std.ExtTreeMap.minKeyD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α → α
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Closure
SubMulAction.mem_closure_of_mem : ∀ {R : Type u_1} {M : Type u_2} [inst : SMul R M] {s : Set M} {x : M}, x ∈ s → x ∈ SubMulAction.closure R s
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_inter_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [inst : Inhabited α] [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → (t₁ ∩ t₂).get! k = default
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.inf_imp_right : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ ψ : L.BoundedFormula α n), T.Imp (φ ⊓ ψ) ψ
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.State.mk.injEq : ∀ {α : Type} (producers : Std.Queue (IO.Promise Bool))
  (consumers : Std.Queue (Std.CloseableChannel.Bounded.Consumer✝ α)) (capacity : ℕ)
  (buf : Vector (IO.Ref (Option α)) capacity) (bufCount sendIdx : ℕ) (hsend : sendIdx < capacity) (recvIdx : ℕ)
  (hrecv : recvIdx < capacity) (closed : Bool) (producers_1 : Std.Queue (IO.Promise Bool))
  (consumers_1 : Std.Queue (Std.CloseableChannel.Bounded.Consumer✝ α)) (capacity_1 : ℕ)
  (buf_1 : Vector (IO.Ref (Option α)) capacity_1) (bufCount_1 sendIdx_1 : ℕ) (hsend_1 : sendIdx_1 < capacity_1)
  (recvIdx_1 : ℕ) (hrecv_1 : recvIdx_1 < capacity_1) (closed_1 : Bool),
  ({ producers := producers, consumers := consumers, capacity := capacity, buf := buf, bufCount := bufCount,
        sendIdx := sendIdx, hsend := hsend, recvIdx := recvIdx, hrecv := hrecv, closed := closed } =
      { producers := producers_1, consumers := consumers_1, capacity := capacity_1, buf := buf_1,
        bufCount := bufCount_1, sendIdx := sendIdx_1, hsend := hsend_1, recvIdx := recvIdx_1, hrecv := hrecv_1,
        closed := closed_1 }) =
    (producers = producers_1 ∧
      consumers = consumers_1 ∧
        capacity = capacity_1 ∧
          buf ≍ buf_1 ∧ bufCount = bufCount_1 ∧ sendIdx = sendIdx_1 ∧ recvIdx = recvIdx_1 ∧ closed = closed_1)
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- An equivalence between the "proxy type" `Affine.Simplex.PointsWithCircumcenterIndex.proxyType` and `Affine.Simplex.PointsWithCircumcenterIndex`. The proxy type is a reducible definition that represents the inductive type using `Unit`, `PLift`, `Sigma`, `Empty`, and `Sum` (and whatever other inductive types appear within the inductive type), and the intended use is to define typeclass instances uses pre-existing instances on these. (Generated by the `proxy_equiv%` elaborator.) -/
Affine.Simplex.PointsWithCircumcenterIndex.proxyTypeEquiv : (n : ℕ) → Fin (n + 1) ⊕ Unit ≃ Affine.Simplex.PointsWithCircumcenterIndex n
-- Mathlib.GroupTheory.Torsion
MulEquiv.map_torsion : ∀ {G : Type u_1} {H : Type u_2} [inst : CommGroup G] [inst_1 : CommGroup H] (e : G ≃* H),
  Subgroup.map (↑e) (CommGroup.torsion G) = CommGroup.torsion H
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_diff_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, k ∉ m₁ → (m₁ \ m₂).get? k = none
-- Lean.Meta.DiscrTree.Main
_private.Lean.Meta.DiscrTree.Main.0.Lean.Meta.DiscrTree.getUnify.process : {α : Type} → ℕ → Array Lean.Expr → Lean.Meta.DiscrTree.Trie α → Array α → Lean.MetaM (Array α)
-- Mathlib.GroupTheory.GroupAction.Primitive
/-- A pretransitive action is preprimitive
iff the stabilizer of any point is a maximal subgroup (Wielandt, th. 7.5)  -/
AddAction.isCoatom_stabilizer_iff_preprimitive : ∀ (G : Type u_3) [inst : AddGroup G] {X : Type u_4} [inst_1 : AddAction G X] [AddAction.IsPretransitive G X]
  [Nontrivial X] (a : X), IsCoatom (AddAction.stabilizer G a) ↔ AddAction.IsPreprimitive G X
-- Lean.Meta.Tactic.LibrarySearch
/-- A "modifier" for a declaration.
* `none` indicates the original declaration,
* `mp` indicates that (possibly after binders) the declaration is an `↔`,
  and we want to consider the forward direction,
* `mpr` similarly, but for the backward direction.
 -/
Lean.Meta.LibrarySearch.DeclMod : Type
-- Lean.Meta.Tactic.LibrarySearch
_private.Lean.Meta.Tactic.LibrarySearch.0.Lean.Meta.LibrarySearch.addImport : Lean.Name →
  Lean.AsyncConstantInfo →
    Lean.MetaM (Array (Lean.Meta.LazyDiscrTree.InitEntry (Lean.Name × Lean.Meta.LibrarySearch.DeclMod)))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_map : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w} [Std.TransOrd α]
  {f : (a : α) → β a → γ a} {k : α}, t.WF → (Std.DTreeMap.Internal.Impl.map f t).getKey? k = t.getKey? k