mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
HomotopyCategory.Pretriangulated.distinguished_cocone_triangle : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X Y : HomotopyCategory C (ComplexShape.up ℤ)} (f : X ⟶ Y),
  ∃ Z g h, CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.exists_eq_append_singleton_of_ne_startPos : ∀ {t₁ t₂ : String} {s : String.Slice} {p : s.Pos} (hp : p ≠ s.startPos),
  p.Splits t₁ t₂ → ∃ t₁', t₁ = t₁' ++ String.singleton ((p.prev hp).get ⋯)
-- Mathlib.RingTheory.Perfection
Perfection.instCommSemiring : (R : Type u_1) →
  [inst : CommSemiring R] → (p : ℕ) → [hp : Fact (Nat.Prime p)] → [CharP R p] → CommSemiring (Perfection R p)
-- Mathlib.Data.Vector3
/-- "Curried" exists, i.e. `∃ x₁ ... xₙ, f [x₁, ..., xₙ]`.  -/
VectorEx : {α : Type u_1} → (k : ℕ) → (Vector3 α k → Prop) → Prop
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.const_toFun : ∀ (ms : Tactic.ComputeAsymptotics.MultiseriesExpansion []), ms.toFun = fun x => ms.toReal
-- Init.Data.Fin.Lemmas
_private.Init.Data.Fin.Lemmas.0.Fin.reverseInduction.go.match_1.eq_1 : ∀ {n : ℕ} {motive : Fin (n + 1) → Sort u_2} (i : Fin (n + 1))
  (motive_1 : (j : ℕ) → (h : j < n + 1) → ↑i ≤ j → motive ⟨j, h⟩ → ¬↑i = j → Sort u_1) (h : 0 < n + 1) (h2 : ↑i ≤ 0)
  (x : motive ⟨0, h⟩) (hi : ¬↑i = 0)
  (h_1 : (h : 0 < n + 1) → (h2 : ↑i ≤ 0) → (x : motive ⟨0, h⟩) → (hi : ¬↑i = 0) → motive_1 0 h h2 x hi)
  (h_2 :
    (j : ℕ) →
      (h : j + 1 < n + 1) →
        (h2 : ↑i ≤ j + 1) → (x : motive ⟨j + 1, h⟩) → (hi : ¬↑i = j + 1) → motive_1 j.succ h h2 x hi),
  (match 0, h, h2, x, hi with
    | 0, h, h2, x, hi => h_1 h h2 x hi
    | j.succ, h, h2, x, hi => h_2 j h h2 x hi) =
    h_1 h h2 x hi
-- Init.Internal.Order.Basic
/-- A chain-complete partial order (CCPO) is a partial order where every chain has a least upper bound.

This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used
otherwise.
 -/
Lean.Order.CCPO : Sort u → Sort (max 1 u)
-- Init.Data.Array.Sort.Lemmas
List.mergeSort.fun_cases_unfolding : ∀ {α : Type u_1} (motive : List α → (α → α → Bool) → List α → Prop),
  (∀ (x : α → α → Bool), motive [] x []) →
    (∀ (a : α) (x : α → α → Bool), motive [a] x [a]) →
      (∀ (a b : α) (xs : List α) (le : α → α → Bool),
          have lr := List.MergeSort.Internal.splitInTwo ⟨a :: b :: xs, ⋯⟩;
          (↑(List.MergeSort.Internal.splitInTwo ⟨a :: b :: xs, ⋯⟩).2).length = (xs.length + 1 + 1) / 2 →
            (↑(List.MergeSort.Internal.splitInTwo ⟨a :: b :: xs, ⋯⟩).1).length = (xs.length + 1 + 1 + 1) / 2 →
              motive (a :: b :: xs) le (((↑lr.1).mergeSort le).merge ((↑lr.2).mergeSort le) le)) →
        ∀ (x : List α) (x_1 : α → α → Bool), motive x x_1 (x.mergeSort x_1)
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.CompletionClientCapabilities.mk.injEq : ∀ (completionItem? completionItem?_1 : Option Lean.Lsp.CompletionItemCapabilities),
  ({ completionItem? := completionItem? } = { completionItem? := completionItem?_1 }) =
    (completionItem? = completionItem?_1)
-- Mathlib.LinearAlgebra.AffineSpace.Centroid
Finset.centroid_univ : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : Finset P), Finset.centroid k Finset.univ Subtype.val = Finset.centroid k s id
-- Mathlib.Topology.Coherent
/-- If each point of the space has a neighborhood from the family `S`,
then the topology is generated by its restrictions to the sets of `S`.  -/
Topology.IsCoherentWith.of_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] {S : Set (Set X)},
  (∀ (x : X), ∃ s ∈ S, s ∈ nhds x) → Topology.IsCoherentWith S
-- Lean.Compiler.IR.Basic
Lean.IR.getUnboxOpName : Lean.IR.IRType → String
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.IsPushout.inl_isoPushout_hom_whiskerRight : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {Z X Y P : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : CategoryTheory.IsPushout f g inl inr)
  [inst_2 : CategoryTheory.Limits.HasPushout f g] {Q : C},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight inl Q)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight hP.isoPushout.hom Q) =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.pushout.inl f g) Q
-- Mathlib.CategoryTheory.Limits.Opposites
/-- The colimit of `F.op` is the opposite of `limit F`.  -/
CategoryTheory.Limits.colimitOpIsoOpLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        (F : CategoryTheory.Functor J C) →
          [inst_2 : CategoryTheory.Limits.HasLimit F] →
            CategoryTheory.Limits.colimit F.op ≅ Opposite.op (CategoryTheory.Limits.limit F)
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.commMonoid : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    {I : ModelWithCorners 𝕜 E H} →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {N : Type u_6} →
                              [inst_7 : TopologicalSpace N] →
                                [inst_8 : ChartedSpace H N] →
                                  {n : WithTop ℕ∞} →
                                    {G : Type u_10} →
                                      [inst_9 : CommMonoid G] →
                                        [inst_10 : TopologicalSpace G] →
                                          [inst_11 : ChartedSpace H' G] →
                                            [ContMDiffMul I' n G] → CommMonoid (ContMDiffMap I I' N G n)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- If a continuous linear map stabilizes a submodule, then it stabilizes its topological
closure.  -/
Submodule.topologicalClosure_mem_invtSubmodule : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] [inst_4 : TopologicalSpace R₁] [inst_5 : ContinuousSMul R₁ M₁] [inst_6 : ContinuousAdd M₁]
  {f : M₁ →L[R₁] M₁} {s : Submodule R₁ M₁},
  s ∈ Module.End.invtSubmodule ↑f → s.topologicalClosure ∈ Module.End.invtSubmodule ↑f
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
AlgebraicGeometry.isFinite_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.IsFinite f ↔
    AlgebraicGeometry.IsAffineHom f ∧
      ∀ (U : Y.Opens),
        AlgebraicGeometry.IsAffineOpen U → (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.app f U)).Finite
-- Mathlib.RingTheory.Ideal.UFD
UniqueFactorizationMonoid.of_forall_isPrincipal_of_height_eq_one : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] [IsNoetherianRing R],
  (∀ (p : Ideal R) [p.IsPrime], p.height = 1 → Submodule.IsPrincipal p) → UniqueFactorizationMonoid R
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
/-- The Archimedean Gamma factor: `Gammaℝ s` if `χ` is even, and `Gammaℝ (s + 1)` otherwise.  -/
DirichletCharacter.gammaFactor : {N : ℕ} → DirichletCharacter ℂ N → ℂ → ℂ
-- Mathlib.AlgebraicTopology.DoldKan.Decomposition
AlgebraicTopology.DoldKan.MorphComponents.preComp_φ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X X' : CategoryTheory.SimplicialObject C} {n : ℕ} {Z : C} (f : AlgebraicTopology.DoldKan.MorphComponents X n Z)
  (g : X' ⟶ X), (f.preComp g).φ = CategoryTheory.CategoryStruct.comp (g.app (Opposite.op { len := n + 1 })) f.φ
-- Init.Data.Nat.Lemmas
/-- Tail-recursive runtime replacement for `decidableBallLT`.  -/
Nat.decidableBallLTTR : (n : ℕ) →
  (P : (k : ℕ) → k < n → Prop) →
    [(n_1 : ℕ) → (h : n_1 < n) → Decidable (P n_1 h)] → Decidable (∀ (n_1 : ℕ) (h : n_1 < n), P n_1 h)
-- Std.Time.Zoned.Database.TZdb
/-- Returns the first path in `searchPaths` joined with `rel` that exists on disk, or `none`.
 -/
Std.Time.Database.TZdb.findInPaths : Array System.FilePath → String → IO (Option System.FilePath)
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheorems.mk.inj : ∀ {pre post : Lean.Meta.SimpTheoremTree} {lemmaNames : Lean.PHashSet Lean.Meta.Origin}
  {toUnfold : Lean.PHashSet Lean.Name} {erased : Lean.PHashSet Lean.Meta.Origin}
  {toUnfoldThms : Lean.PHashMap Lean.Name (Array Lean.Name)} {pre_1 post_1 : Lean.Meta.SimpTheoremTree}
  {lemmaNames_1 : Lean.PHashSet Lean.Meta.Origin} {toUnfold_1 : Lean.PHashSet Lean.Name}
  {erased_1 : Lean.PHashSet Lean.Meta.Origin} {toUnfoldThms_1 : Lean.PHashMap Lean.Name (Array Lean.Name)},
  { pre := pre, post := post, lemmaNames := lemmaNames, toUnfold := toUnfold, erased := erased,
        toUnfoldThms := toUnfoldThms } =
      { pre := pre_1, post := post_1, lemmaNames := lemmaNames_1, toUnfold := toUnfold_1, erased := erased_1,
        toUnfoldThms := toUnfoldThms_1 } →
    pre = pre_1 ∧
      post = post_1 ∧
        lemmaNames = lemmaNames_1 ∧ toUnfold = toUnfold_1 ∧ erased = erased_1 ∧ toUnfoldThms = toUnfoldThms_1
-- Init.Data.UInt.Lemmas
UInt32.le_zero_iff : ∀ {a : UInt32}, a ≤ 0 ↔ a = 0
-- Mathlib.Algebra.Group.Subgroup.Actions
/-- The action by a subgroup is the action by the underlying group.  -/
Subgroup.instDistribMulActionSubtypeMem : {G : Type u_1} →
  {α : Type u_2} →
    [inst : Group G] → [inst_1 : AddMonoid α] → [DistribMulAction G α] → (S : Subgroup G) → DistribMulAction (↥S) α
-- Mathlib.Combinatorics.SimpleGraph.Dart
/-- Two darts are said to be adjacent if they could be consecutive
darts in a walk -- that is, the first dart's second vertex is equal to
the second dart's first vertex.  -/
SimpleGraph.DartAdj : {V : Type u_1} → (G : SimpleGraph V) → G.Dart → G.Dart → Prop
-- Mathlib.Analysis.RCLike.ContinuousMap
ContinuousMap.rclikeToReal_monotone : ∀ (X : Type u_1) (𝕜 : Type u_2) [inst : TopologicalSpace X] [inst_1 : RCLike 𝕜], Monotone ContinuousMap.rclikeToReal
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.σ₀Iter_succ_assoc : ∀ (i : ℕ) {n m : ℕ} (h : n + (i + 1) = m) {Z : SimplexCategory} (h_1 : { len := n } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SimplexCategory.σ₀Iter (i + 1) h) h_1 =
    CategoryTheory.CategoryStruct.comp (SimplexCategory.σ₀Iter i ⋯)
      (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ 0) h_1)
-- Init.ShareCommon
ShareCommon.StateFactoryBuilder.mapFind? : (self : ShareCommon.StateFactoryBuilder) →
  {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → self.Map α β → α → Option β
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.instIsTransModEq : ∀ {M : Type u_1} [inst : AddCommMonoid M] {p : M}, IsTrans M (AddCommGroup.ModEq p)
-- Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma
HomotopicalAlgebra.bijective_rightHomotopyClassToHom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {H : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} H] (L : CategoryTheory.Functor C H)
  [inst_3 : L.IsLocalization (HomotopicalAlgebra.weakEquivalences C)] (X Y : C) [HomotopicalAlgebra.IsCofibrant X]
  [HomotopicalAlgebra.IsFibrant Y], Function.Bijective (HomotopicalAlgebra.rightHomotopyClassToHom L)
-- Lean.Parser.Syntax
Lean.Parser.Syntax.sepBy.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `HasFDerivAtFilter.const_smul` -/
HasFDerivAtFilter.fun_const_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {L : Filter (E × E)} {R : Type u_4} [inst_5 : Monoid R] [inst_6 : DistribMulAction R F]
  [inst_7 : SMulCommClass 𝕜 R F] [inst_8 : ContinuousConstSMul R F],
  HasFDerivAtFilter f f' L → ∀ (c : R), HasFDerivAtFilter (fun i => c • f i) (c • f') L
-- Mathlib.Data.Matrix.Basic
RingEquiv.mopMatrix_apply : ∀ {m : Type u_2} [inst : Fintype m] {α : Type u_14} [inst_1 : Mul α] [inst_2 : AddCommMonoid α] (M : Matrix m m αᵐᵒᵖ),
  RingEquiv.mopMatrix M = MulOpposite.op (M.transpose.map MulOpposite.unop)
-- Mathlib.CategoryTheory.Products.Basic
/-- Analogue of `Prod.mk.injEq` in this setting.  -/
CategoryTheory.Prod.mkHom_eq : ∀ {C : Type u₁} [inst : CategoryTheory.CategoryStruct.{v₁, u₁} C] {D : Type u₂}
  [inst_1 : CategoryTheory.CategoryStruct.{v₂, u₂} D] {X₁ X₂ : C} {Y₁ Y₂ : D} (f f' : X₁ ⟶ X₂) (g g' : Y₁ ⟶ Y₂),
  CategoryTheory.Prod.mkHom f g = CategoryTheory.Prod.mkHom f' g' ↔ f = f' ∧ g = g'
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.succMany_add_one_eq_succMany_succ : ∀ {n : ℕ} {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.PRange.InfinitelyUpwardEnumerable α] {a : α},
  Std.PRange.succMany (n + 1) a = Std.PRange.succMany n (Std.PRange.succ a)
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.toTruncated_id : ∀ {X : SSet} (x₀ : X.obj (Opposite.op { len := 0 })), (SSet.Edge.id x₀).toTruncated = SSet.Truncated.Edge.id x₀
-- Mathlib.RingTheory.Regular.Category
ModuleCat.smulShortComplex.eq_1 : ∀ {R : Type u} [inst : CommRing R] (M : ModuleCat R) (r : R),
  M.smulShortComplex r = ModuleCat.shortComplexOfCompEqZero ((LinearMap.lsmul R ↑M) r) (r • ⊤).mkQ ⋯
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.insertMany_list_singleton : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β},
  m.WF → ∀ {k : α} {v : β}, Std.DHashMap.Raw.Const.insertMany m [(k, v)] = m.insert k v
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.map_comp : ∀ {k : Type u_1} {V : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} {P : Type u_5} {P₂ : Type u_6} {P₃ : Type u_7}
  [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : AddCommGroup V₂] [inst_3 : AddCommGroup V₃] [inst_4 : Module k V]
  [inst_5 : Module k V₂] [inst_6 : Module k V₃] [inst_7 : AddTorsor V P] [inst_8 : AddTorsor V₂ P₂]
  [inst_9 : AddTorsor V₃ P₃] {n : ℕ} (s : Affine.Simplex k P n) (f : P →ᵃ[k] P₂) (hf : Function.Injective ⇑f)
  (g : P₂ →ᵃ[k] P₃) (hg : Function.Injective ⇑g), s.map (g.comp f) ⋯ = (s.map f hf).map g hg
-- Lean.Environment
Lean.Environment.setMainModule : Lean.Environment → Lean.Name → Lean.Environment
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- Up to a factor 2, `Q.polar` is the associated bilinear map for a quadratic map `Q`.

Source of this name: https://en.wikipedia.org/wiki/Quadratic_form#Generalization
 -/
QuadraticMap.polar : {M : Type u_4} → {N : Type u_5} → [AddCommGroup M] → [AddCommGroup N] → (M → N) → M → M → N
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.homEquiv_naturality_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {X : C} {Y Y' : D} (f : F.obj X ⟶ Y)
  (g : Y ⟶ Y'),
  (adj.homEquiv X Y') (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp ((adj.homEquiv X Y) f) (G.map g)
-- Mathlib.Data.Set.Finite.Lattice
Set.finite_subset_iUnion : ∀ {α : Type u} {s : Set α}, s.Finite → ∀ {ι : Type u_1} {t : ι → Set α}, s ⊆ ⋃ i, t i → ∃ I, I.Finite ∧ s ⊆ ⋃ i ∈ I, t i
-- Mathlib.Algebra.Homology.HomotopyCategory
CategoryTheory.Functor.mapHomotopyCategory_map : ∀ {ι : Type u_2} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {W : Type u_3} [inst_2 : CategoryTheory.Category.{v_1, u_3} W] [inst_3 : CategoryTheory.Preadditive W]
  (F : CategoryTheory.Functor V W) [inst_4 : F.Additive] {c : ComplexShape ι} {K L : HomologicalComplex V c}
  (f : K ⟶ L),
  (F.mapHomotopyCategory c).map ((HomotopyCategory.quotient V c).map f) =
    (HomotopyCategory.quotient W c).map ((F.mapHomologicalComplex c).map f)
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
/-- If `H₁ ≃g H₂`, then `extremalNumber n H₁` equals `extremalNumber n H₂`.  -/
SimpleGraph.extremalNumber_congr : ∀ {n₁ n₂ : ℕ} {W₁ : Type u_4} {W₂ : Type u_5} {H₁ : SimpleGraph W₁} {H₂ : SimpleGraph W₂},
  n₁ = n₂ → ∀ (e : H₁ ≃g H₂), SimpleGraph.extremalNumber n₁ H₁ = SimpleGraph.extremalNumber n₂ H₂
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The composition of two applications of `map₂` is naturally isomorphic to a single such one.  -/
CategoryTheory.StructuredArrow.map₂CompMap₂Iso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {A : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} A] →
            {B : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} B] →
                {L : D} →
                  {R : CategoryTheory.Functor C D} →
                    {L' : B} →
                      {R' : CategoryTheory.Functor A B} →
                        {F : CategoryTheory.Functor C A} →
                          {G : CategoryTheory.Functor D B} →
                            (α : L' ⟶ G.obj L) →
                              (β : R.comp G ⟶ F.comp R') →
                                {C' : Type u₆} →
                                  [inst_4 : CategoryTheory.Category.{v₆, u₆} C'] →
                                    {D' : Type u₅} →
                                      [inst_5 : CategoryTheory.Category.{v₅, u₅} D'] →
                                        {L'' : D'} →
                                          {R'' : CategoryTheory.Functor C' D'} →
                                            {F' : CategoryTheory.Functor C' C} →
                                              {G' : CategoryTheory.Functor D' D} →
                                                (α' : L ⟶ G'.obj L'') →
                                                  (β' : R''.comp G' ⟶ F'.comp R) →
                                                    (CategoryTheory.StructuredArrow.map₂ α' β').comp
                                                        (CategoryTheory.StructuredArrow.map₂ α β) ≅
                                                      CategoryTheory.StructuredArrow.map₂
                                                        (CategoryTheory.CategoryStruct.comp α (G.map α'))
                                                        (CategoryTheory.CategoryStruct.comp (R''.associator G' G).inv
                                                          (CategoryTheory.CategoryStruct.comp
                                                            (CategoryTheory.Functor.whiskerRight β' G)
                                                            (CategoryTheory.CategoryStruct.comp (F'.associator R G).hom
                                                              (CategoryTheory.CategoryStruct.comp (F'.whiskerLeft β)
                                                                (F'.associator F R').inv))))
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- If `E` is a pre-`1`-hypercover and `F` a presheaf, the induced equalizer of
the single object covering obtained from `E` by taking coproducts is limiting
if and only if the induced multiequalizer of `E` is limiting.  -/
CategoryTheory.PreOneHypercover.isLimitSigmaOfIsColimitEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} A] →
        {S : C} →
          (E : CategoryTheory.PreOneHypercover S) →
            {c : CategoryTheory.Limits.Cofan E.X} →
              (hc : CategoryTheory.Limits.IsColimit c) →
                {d : CategoryTheory.Limits.Cofan E.Y'} →
                  (hd : CategoryTheory.Limits.IsColimit d) →
                    (F : CategoryTheory.Functor Cᵒᵖ A) →
                      [CategoryTheory.Limits.PreservesLimit
                            (CategoryTheory.Discrete.functor fun i => Opposite.op (E.X i)) F] →
                        [CategoryTheory.Limits.PreservesLimit
                              (CategoryTheory.Discrete.functor fun i => Opposite.op (E.Y' i)) F] →
                          CategoryTheory.Limits.IsLimit ((E.sigmaOfIsColimit hc hd).multifork F) ≃
                            CategoryTheory.Limits.IsLimit (E.multifork F)
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.AffineCover.cover_f : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.AffineCover P X) (j : 𝒰.I₀), 𝒰.cover.f j = 𝒰.f j
-- Mathlib.Analysis.Complex.Isometry
LinearIsometry.im_apply_eq_im_or_neg_of_re_apply_eq_re : ∀ {f : ℂ →ₗᵢ[ℝ] ℂ}, (∀ (z : ℂ), (f z).re = z.re) → ∀ (z : ℂ), (f z).im = z.im ∨ (f z).im = -z.im
-- Std.Do.WP.SimpLemmas
Std.Do.WP.monadMap_OptionT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} [Monad m] [inst : Std.Do.WP m ps] (f : {β : Type u} → m β → m β)
  {α : Type u} (x : OptionT m α) (Q : Std.Do.PostCond α (Std.Do.PostShape.except PUnit.{u + 1} ps)),
  (Std.Do.wp (MonadFunctor.monadMap (fun {β} => f) x)).apply Q =
    (Std.Do.wp (f x.run)).apply (fun o => Option.casesOn o (Q.2.1 PUnit.unit) Q.1, Q.2.2)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey!_insert_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {v : β}, t.isEmpty = true → (t.insert k v).minKey! = k
-- Lean.PrettyPrinter.Delaborator.SubExpr
Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator.mk.sizeOf_spec : ∀ (curr top : ℕ), sizeOf { curr := curr, top := top } = 1 + sizeOf curr + sizeOf top
-- Mathlib.Algebra.Free
/-- The tail of the element  -/
FreeSemigroup.tail : {α : Type u} → FreeSemigroup α → List α
-- Init.Data.Zero
Zero.ofOfNat0 : {α : Type u_1} → [OfNat α 0] → Zero α
-- Std.Data.TreeMap.Raw.Lemmas
/-- Variant of `getD_map` that holds without `LawfulEqCmp`.  -/
Std.TreeMap.Raw.getD_map' : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}
  [inst : Std.TransCmp cmp] {f : α → β → γ} {k : α} {fallback : γ} (h : t.WF),
  (Std.TreeMap.Raw.map f t).getD k fallback = (Option.pmap (fun v h => f (t.getKey k h) v) t[k]? ⋯).getD fallback
-- Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
_private.Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities.0.MvPolynomial.NewtonIdentities.sum_filter_pairs_eq_sum_filter_antidiagonal_powersetCard_sum : ∀ (σ : Type u_1) (R : Type u_2) [inst : CommRing R] [inst_1 : DecidableEq σ] [inst_2 : Fintype σ] (k : ℕ)
  (f : Finset σ × σ → MvPolynomial σ R),
  ∑ t ∈ MvPolynomial.NewtonIdentities.pairs✝ σ k with t.1.card < k, f t =
    ∑ a ∈ Finset.HasAntidiagonal.antidiagonal k with a.1 < k, ∑ A ∈ Finset.powersetCard a.1 Finset.univ, ∑ j, f (A, j)
-- Mathlib.MeasureTheory.Measure.Prod
/-- Note: the converse is not true. For a counterexample, see
Walter Rudin *Real and Complex Analysis*, example (c) in section 8.9. It is true if the set is
measurable, see `ae_prod_mem_iff_ae_ae_mem`.  -/
MeasureTheory.Measure.ae_ae_of_ae_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {p : α × β → Prop},
  (∀ᵐ (z : α × β) ∂μ.prod ν, p z) → ∀ᵐ (x : α) ∂μ, ∀ᵐ (y : β) ∂ν, p (x, y)
-- Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
AddSubgroup.Commensurable.properlyDiscontinuousVAdd_iff : ∀ {Γ : Type u_1} {α : Type u_2} [inst : AddGroup Γ] [inst_1 : TopologicalSpace α] [inst_2 : AddAction Γ α]
  [ContinuousConstVAdd Γ α] {G H : AddSubgroup Γ},
  G.Commensurable H → (ProperlyDiscontinuousVAdd (↥G) α ↔ ProperlyDiscontinuousVAdd (↥H) α)