mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Algebraic.Integral
Algebra.isAlgebraic_iff_isIntegral : ∀ {K : Type u} {A : Type v} [inst : Field K] [inst_1 : Ring A] [inst_2 : Algebra K A],
  Algebra.IsAlgebraic K A ↔ Algebra.IsIntegral K A
-- Mathlib.RingTheory.Conductor
adjoin_eq_top_of_conductor_eq_top : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S},
  conductor R x = ⊤ → R[x] = ⊤
-- Init.Data.List.Zip
List.unzip_zip_right : ∀ {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β}, l₂.length ≤ l₁.length → (l₁.zip l₂).unzip.2 = l₂
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.isStrictlyLE_shift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : CochainComplex C ℤ) (n : ℤ) [K.IsStrictlyLE n] (a n' : ℤ),
  a + n' = n → ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).IsStrictlyLE n'
-- Mathlib.Analysis.Normed.Module.Ball.Action
continuousSMul_closedBall_closedBall : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {r : ℝ}, ContinuousSMul ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 r)
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.TransvectionStruct.mk.sizeOf_spec : ∀ {n : Type u_1} {R : Type u₂} [inst : SizeOf n] [inst_1 : SizeOf R] (i j : n) (hij : i ≠ j) (c : R),
  sizeOf { i := i, j := j, hij := hij, c := c } = 1 + sizeOf i + sizeOf j + sizeOf c
-- Mathlib.RingTheory.Ideal.Operations
Ideal.range_mul' : ∀ {R : Type u} [inst : CommSemiring R] (a : R), ((LinearMap.mul R R) a).range = Ideal.span {a}
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
/-- `LinearEquiv.prodProdProdComm` is isometric.  -/
QuadraticMap.IsometryEquiv.prodProdProdComm : {R : Type u_2} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      {N₁ : Type u_5} →
        {N₂ : Type u_6} →
          {P : Type u_7} →
            [inst : CommSemiring R] →
              [inst_1 : AddCommMonoid M₁] →
                [inst_2 : AddCommMonoid M₂] →
                  [inst_3 : AddCommMonoid N₁] →
                    [inst_4 : AddCommMonoid N₂] →
                      [inst_5 : AddCommMonoid P] →
                        [inst_6 : Module R M₁] →
                          [inst_7 : Module R M₂] →
                            [inst_8 : Module R N₁] →
                              [inst_9 : Module R N₂] →
                                [inst_10 : Module R P] →
                                  (Q₁ : QuadraticMap R M₁ P) →
                                    (Q₂ : QuadraticMap R M₂ P) →
                                      (Q₃ : QuadraticMap R N₁ P) →
                                        (Q₄ : QuadraticMap R N₂ P) →
                                          ((Q₁.prod Q₂).prod (Q₃.prod Q₄)).IsometryEquiv
                                            ((Q₁.prod Q₃).prod (Q₂.prod Q₄))
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.dblX_smul : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R) (u : R),
  W'.dblX (u • P) = u ^ 4 * W'.dblX P
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapCycles₂_id_comp_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B C : Rep.{u, u, u} k G} (φ : A ⟶ B) (ψ : B ⟶ C)
  {Z : ModuleCat k} (h : ModuleCat.of k ↥(groupHomology.cycles₂ C) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (groupHomology.mapCycles₂ (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ)) h =
    CategoryTheory.CategoryStruct.comp (groupHomology.mapCycles₂ (MonoidHom.id G) φ)
      (CategoryTheory.CategoryStruct.comp (groupHomology.mapCycles₂ (MonoidHom.id G) ψ) h)
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.map_bot : ∀ {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup M']
  [inst_6 : Module R M'] [inst_7 : LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'}, LieSubmodule.map f ⊥ = ⊥
-- Mathlib.Tactic.TermCongr
/-- Key for congruence hole metadata.
For a `Bool` recording whether this hole is for the LHS elaboration.  -/
_private.Mathlib.Tactic.TermCongr.0.Mathlib.Tactic.TermCongr.congrHoleForLhsKey : Lean.Name
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.ShiftMkCore.shiftFunctorAdd_eq : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  (h : CategoryTheory.ShiftMkCore C A) (a b : A), CategoryTheory.shiftFunctorAdd C a b = h.add a b
-- Mathlib.Algebra.Group.Submonoid.MulAction
AddSubmonoid.instVAddCommClassSubtypeMem : ∀ {M' : Type u_1} {α : Type u_2} {β : Type u_3} {S' : Type u_4} [inst : SetLike S' M'] (s : S') [inst_1 : VAdd M' β]
  [inst_2 : VAdd α β] [VAddCommClass M' α β], VAddCommClass (↥s) α β
-- Mathlib.NumberTheory.NumberField.Units.Basic
NumberField.Units.even_torsionOrder : ∀ (K : Type u_1) [inst : Field K] [NumberField K], Even (NumberField.Units.torsionOrder K)
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.BitVec.append_congr : ∀ (lw rw : ℕ) (lhs lhs' : BitVec lw) (rhs rhs' : BitVec rw), lhs' = lhs → rhs' = rhs → lhs' ++ rhs' = lhs ++ rhs
-- Mathlib.Data.List.Lex
List.Lex.append_left : ∀ {α : Type u} (R : α → α → Prop) {t₁ t₂ : List α}, List.Lex R t₁ t₂ → ∀ (s : List α), List.Lex R (s ++ t₁) (s ++ t₂)
-- Mathlib.Algebra.Free
/-- Length of an element of free additive semigroup  -/
FreeAddSemigroup.length : {α : Type u} → FreeAddSemigroup α → ℕ
-- Mathlib.Algebra.Colimit.Ring
Ring.DirectLimit.of_f : ∀ {ι : Type u_1} [inst : Preorder ι] {G : ι → Type u_2} [inst_1 : (i : ι) → CommRing (G i)]
  {f : (i j : ι) → i ≤ j → G i → G j} {i j : ι} (hij : i ≤ j) (x : G i),
  (Ring.DirectLimit.of G f j) (f i j hij x) = (Ring.DirectLimit.of G f i) x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.functorEquiv_unitIso_hom_app_app_fst : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  (X_1 : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)) (X_2 : X),
  (((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).unitIso.hom.app X_1).app X_2).fst =
    CategoryTheory.CategoryStruct.id (X_1.obj X_2).fst
-- Mathlib.Order.Filter.ZeroAndBoundedAtFilter
Filter.BoundedAtFilter.add : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedAddCommGroup β] {l : Filter α} {f g : α → β},
  l.BoundedAtFilter f → l.BoundedAtFilter g → l.BoundedAtFilter (f + g)
-- Lean.Server.GoTo
_private.Lean.Server.GoTo.0.Lean.Server.locationLinksDefault.defaultDeclNames : Lean.Server.GoToM (Array Lean.Name)
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.term_atom_pfg : ∀ {α : Type u_1} [inst : AddCommGroup α] (x x' : α), x = x' → x = Mathlib.Tactic.Abel.termg 1 x' 0
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.cells_sup : ∀ (μ ν : YoungDiagram), (μ ⊔ ν).cells = μ.cells ∪ ν.cells
-- Lean.Meta.Tactic.Grind.MatchDiscrOnly
Lean.Meta.Grind.isSimpMatchDiscrsOnly : Lean.Expr → Bool
-- Mathlib.Data.ZMod.Basic
ZMod.inv_neg_one : ∀ (n : ℕ), (-1)⁻¹ = -1
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- The functor `LeftExtension L' F ⥤ LeftExtension L F`
induced by a natural transformation `L' ⟶ L ⋙ G'`.  -/
CategoryTheory.Functor.LeftExtension.postcomp₁ : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      {D' : Type u_5} →
        [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] →
              [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] →
                {L : CategoryTheory.Functor C D} →
                  {L' : CategoryTheory.Functor C D'} →
                    (G : CategoryTheory.Functor D D') →
                      (L' ⟶ L.comp G) →
                        (F : CategoryTheory.Functor C H) →
                          CategoryTheory.Functor (L'.LeftExtension F) (L.LeftExtension F)
-- Mathlib.LinearAlgebra.Projection
LinearMap.surjective_comp_subtype_of_isComplemented : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p : Submodule R E}
  {M : Type u_6} [inst_3 : AddCommMonoid M],
  IsComplemented p → ∀ [inst_4 : Module R M], Function.Surjective fun f => f ∘ₗ p.subtype
-- Init.Data.Array.Monadic
Array.foldrM_filter : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {start : ℕ} [inst : Monad m] [LawfulMonad m] {p : α → Bool}
  {g : α → β → m β} {xs : Array α} {init : β} {w : start = (Array.filter p xs).size},
  Array.foldrM g init (Array.filter p xs) start = Array.foldrM (fun x y => if p x = true then g x y else pure y) init xs
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousLinearMap.continuousMultilinearMapOption_apply_eq_self : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] {F : Type u_1} {G : Type u_2}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F] [inst_6 : NormedAddCommGroup G] [inst_7 : NormedSpace 𝕜 G]
  (B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F) (a : G) (v : (i : ι) → E i),
  (B.continuousMultilinearMapOption fun x => (a, v)) = (B a) v
-- Mathlib.RingTheory.Smooth.Fiber
Algebra.Smooth.of_formallySmooth_fiber : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Module.Flat R S]
  [Algebra.FinitePresentation R S],
  (∀ (I : Ideal R) [inst_5 : I.IsPrime], Algebra.FormallySmooth I.ResidueField (I.Fiber S)) → Algebra.Smooth R S
-- Mathlib.Data.Finset.NoncommProd
/-- The non-commutative version of `Finset.sum_union`  -/
Finset.noncommSum_union_of_disjoint : ∀ {α : Type u_3} {β : Type u_4} [inst : AddMonoid β] [inst_1 : DecidableEq α] {s t : Finset α},
  Disjoint s t →
    ∀ (f : α → β) (comm : (↑(s ∪ t)).Pairwise (Function.onFun AddCommute f)),
      (s ∪ t).noncommSum f comm = s.noncommSum f ⋯ + t.noncommSum f ⋯
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.d_comp_d' : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (self : HomologicalComplex V c) (i j k : ι),
  c.Rel i j → c.Rel j k → CategoryTheory.CategoryStruct.comp (self.d i j) (self.d j k) = 0
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.ofAlgHom.eq_1 : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {I : Type u_1}
  (f : MvPolynomial I R →ₐ[R] S) (h : Function.Surjective ⇑f),
  Algebra.Generators.ofAlgHom f h = Algebra.Generators.ofSurjective (⇑f ∘ MvPolynomial.X) ⋯
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.intermediateFieldEquivSubgroup_symm_apply : ∀ (G : Type u_1) (K : Type u_3) (L : Type u_4) [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] [hGKL : IsGaloisGroup G K L] [inst_5 : Finite G]
  {H : (Subgroup G)ᵒᵈ},
  (IsGaloisGroup.intermediateFieldEquivSubgroup G K L).symm H = FixedPoints.intermediateField ↥(OrderDual.ofDual H)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.toList_keysArray : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β}, t.keysArray.toList = t.keys
-- Mathlib.Algebra.Lie.SerreConstruction
/-- The exceptional split Lie algebra of type e₆.  -/
LieAlgebra.e₆ : (R : Type u) → [CommRing R] → Type u
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Real.binEntropy_pos : ∀ {p : ℝ}, 0 < p → p < 1 → 0 < Real.binEntropy p
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
/-- The `n`th group homology of a `k`-linear `G`-representation `A` is isomorphic to
`Hₙ((A ⊗ P)_G)`, where `P` is any projective resolution of `k` as a trivial `k`-linear
`G`-representation.  -/
groupHomologyIso : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [DecidableEq G] →
        (A : Rep.{u, u, u} k G) →
          (n : ℕ) →
            (P : CategoryTheory.ProjectiveResolution (Rep.trivial k G k)) →
              groupHomology A n ≅ HomologicalComplex.homology (HomologicalComplex.coinvariantsTensorObj A P.complex) n
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
/-- **Alias** of `SimpleGraph.Walk.length_takeUntil_le_length`. -/
SimpleGraph.Walk.length_takeUntil_le : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u v w : V} (p : G.Walk v w) (h : u ∈ p.support),
  (p.takeUntil u h).length ≤ p.length
-- Mathlib.Combinatorics.Matroid.IndepAxioms
Matroid.ofExistsFiniteIsBase_rankFinite : ∀ {α : Type u_1} (E : Set α) (IsBase : Set α → Prop) (exists_finite_base : ∃ B, IsBase B ∧ B.Finite)
  (isBase_exchange : Matroid.ExchangeProperty IsBase) (subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E),
  (Matroid.ofExistsFiniteIsBase E IsBase exists_finite_base isBase_exchange subset_ground).RankFinite
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.unopComp_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ)
  (G : CategoryTheory.Functor Dᵒᵖ Eᵒᵖ) (X : C),
  (F.unopComp G).hom.app X = CategoryTheory.CategoryStruct.id (Opposite.unop (G.obj (F.obj (Opposite.op X))))
-- Mathlib.Algebra.Homology.SpectralObject.Page
_private.Mathlib.Algebra.Homology.SpectralObject.Page.0.CategoryTheory.ComposableArrows.Precomp.map.match_1.eq_3 : ∀ {n : ℕ} (motive : (x x_1 : Fin (n + 1 + 1)) → x ≤ x_1 → Sort u_1) (isLt : 0 < n + 1 + 1) (j : ℕ)
  (hj : j + 2 < n + 1 + 1) (x : ⟨0, isLt⟩ ≤ ⟨j + 2, hj⟩)
  (h_1 : (isLt isLt_1 : 0 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨0, isLt_1⟩) → motive ⟨0, isLt⟩ ⟨0, isLt_1⟩ x)
  (h_2 :
    (isLt : 0 < n + 1 + 1) → (isLt_1 : 1 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨1, isLt_1⟩) → motive ⟨0, isLt⟩ ⟨1, isLt_1⟩ x)
  (h_3 :
    (isLt : 0 < n + 1 + 1) →
      (j : ℕ) → (hj : j + 2 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨j + 2, hj⟩) → motive ⟨0, isLt⟩ ⟨j.succ.succ, hj⟩ x)
  (h_4 :
    (i : ℕ) →
      (hi : i + 1 < n + 1 + 1) →
        (j : ℕ) → (hj : j + 1 < n + 1 + 1) → (hij : ⟨i + 1, hi⟩ ≤ ⟨j + 1, hj⟩) → motive ⟨i.succ, hi⟩ ⟨j.succ, hj⟩ hij),
  (match ⟨0, isLt⟩, ⟨j.succ.succ, hj⟩, x with
    | ⟨0, isLt⟩, ⟨0, isLt_1⟩, x => h_1 isLt isLt_1 x
    | ⟨0, isLt⟩, ⟨1, isLt_1⟩, x => h_2 isLt isLt_1 x
    | ⟨0, isLt⟩, ⟨j.succ.succ, hj⟩, x => h_3 isLt j hj x
    | ⟨i.succ, hi⟩, ⟨j.succ, hj⟩, hij => h_4 i hi j hj hij) =
    h_3 isLt j hj x
-- Mathlib.NumberTheory.Dioph
Poly.instAddGroupWithOne : {α : Type u_1} → AddGroupWithOne (Poly α)
-- Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
/-- For an additive functor `F : C ⥤ D` between abelian categories, the following are equivalent:
- `F` preserves short exact sequences on the right-hand side, i.e. if `0 ⟶ A ⟶ B ⟶ C ⟶ 0` is
  exact then `F(A) ⟶ F(B) ⟶ F(C) ⟶ 0` is exact.
- `F` preserves exact sequences on the right-hand side, i.e. if `A ⟶ B ⟶ C` is exact where `B ⟶ C`
  is epi, then `F(A) ⟶ F(B) ⟶ F(C) ⟶ 0` is exact and `F(B) ⟶ F(C)` is epi as well.
- `F` preserves cokernels.
- `F` preserves finite colimits.
 -/
CategoryTheory.Functor.preservesFiniteColimits_tfae : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Abelian C]
  [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_4 : F.Additive],
  [∀ (S : CategoryTheory.ShortComplex C), S.ShortExact → (S.map F).Exact ∧ CategoryTheory.Epi (F.map S.g),
      ∀ (S : CategoryTheory.ShortComplex C),
        S.Exact ∧ CategoryTheory.Epi S.g → (S.map F).Exact ∧ CategoryTheory.Epi (F.map S.g),
      ∀ ⦃X Y : C⦄ (f : X ⟶ Y), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F,
      CategoryTheory.Limits.PreservesFiniteColimits F].TFAE
-- Init.Data.Vector.Lemmas
Vector.getElem_set_ne : ∀ {α : Type u_1} {n i j : ℕ} {xs : Vector α n} {x : α} (hi : i < n) (hj : j < n), i ≠ j → (xs.set i x hi)[j] = xs[j]
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicofork.IsColimit.desc.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  {I : CategoryTheory.Limits.MultispanIndex J C} {K : CategoryTheory.Limits.Multicofork I}
  (hK hK_1 : CategoryTheory.Limits.IsColimit K),
  hK = hK_1 →
    ∀ {T : C} (k k_1 : (a : J.R) → I.right a ⟶ T) (e_k : k = k_1)
      (hk :
        ∀ (b : J.L),
          CategoryTheory.CategoryStruct.comp (I.fst b) (k (J.fst b)) =
            CategoryTheory.CategoryStruct.comp (I.snd b) (k (J.snd b))),
      CategoryTheory.Limits.Multicofork.IsColimit.desc hK k hk =
        CategoryTheory.Limits.Multicofork.IsColimit.desc hK_1 k_1 ⋯
-- Mathlib.Order.Interval.Set.Basic
Set.Ioc_eq_empty_of_le : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ≤ b → Set.Ioc b a = ∅
-- Mathlib.Topology.Sheaves.Presheaf
/-- The pullback and pushforward along a continuous map are adjoint to each other.  -/
TopCat.Presheaf.pullbackPushforwardAdjunction : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasColimits C] →
      {X Y : TopCat} → (f : X ⟶ Y) → TopCat.Presheaf.pullback C f ⊣ TopCat.Presheaf.pushforward C f
-- Std.Sat.AIG.Relabel
Std.Sat.AIG.Decl.relabel.eq_1 : ∀ {α β : Type} (r : α → β), Std.Sat.AIG.Decl.relabel r Std.Sat.AIG.Decl.false = Std.Sat.AIG.Decl.false
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
/-- A conditionally complete linear order is a linear order in which
every nonempty subset which is bounded above has a supremum, and
every nonempty subset which is bounded below has an infimum.
Typical examples are real numbers or natural numbers.

To differentiate the statements from the corresponding statements in (unconditional)
complete linear orders, we prefix `sInf` and `sSup` by a `c` everywhere. The same statements should
hold in both worlds, sometimes with additional assumptions of nonemptiness or
boundedness.  -/
ConditionallyCompleteLinearOrder : Type u_5 → Type u_5
-- Mathlib.Topology.WithTopology
WithTopology.ofTopology_inj : ∀ {X : Type u_1} (t : TopologicalSpace X) {x y : WithTopology X t}, x.ofTopology = y.ofTopology ↔ x = y
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.prod_filter_bne_one : ∀ {M : Type u_4} [inst : Monoid M] [inst_1 : BEq M] [LawfulBEq M] (l : List M),
  (List.filter (fun x => x != 1) l).prod = l.prod
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit.eq_1 : ∀ {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} {F : CategoryTheory.PreOneHypercover S} (f : E.Hom F)
  (P : CategoryTheory.Functor Cᵒᵖ A) {c : CategoryTheory.Limits.Multifork (E.multicospanIndex P)}
  (hc : CategoryTheory.Limits.IsLimit c) (d : CategoryTheory.Limits.Multifork (F.multicospanIndex P)),
  f.mapMultiforkOfIsLimit P hc d =
    CategoryTheory.Limits.Multifork.IsLimit.lift hc
      (fun a => CategoryTheory.CategoryStruct.comp (d.ι (f.s₀ a)) (P.map (f.h₀ a).op)) ⋯
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ServerCapabilities.inlayHintProvider? : Lean.Lsp.ServerCapabilities → Option Lean.Lsp.InlayHintOptions
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.order_eq_zero_iff' : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E] [inst_6 : AddCommMonoid F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F] [inst_10 : ContinuousConstSMul 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F}, p.order = 0 ↔ p = 0 ∨ p 0 ≠ 0
-- Mathlib.CategoryTheory.Limits.VanKampen
CategoryTheory.isVanKampenColimit_of_evaluation : ∀ {J : Type v'} [inst : CategoryTheory.Category.{u', v'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasPullbacks D]
  [CategoryTheory.Limits.HasColimitsOfShape J D] (F : CategoryTheory.Functor J (CategoryTheory.Functor C D))
  (c : CategoryTheory.Limits.Cocone F),
  (∀ (x : C), CategoryTheory.IsVanKampenColimit (((CategoryTheory.evaluation C D).obj x).mapCocone c)) →
    CategoryTheory.IsVanKampenColimit c
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.continuous_map₂ : ∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] {γ : Type u_3}
  [inst_2 : UniformSpace γ] {δ : Type u_4} [inst_3 : TopologicalSpace δ] {f : α → β → γ}
  {a : δ → UniformSpace.Completion α} {b : δ → UniformSpace.Completion β},
  Continuous a → Continuous b → Continuous fun d => UniformSpace.Completion.map₂ f (a d) (b d)
-- Mathlib.Topology.Connected.TotallyDisconnected
connectedComponent_eq_singleton : ∀ {α : Type u} [inst : TopologicalSpace α] [TotallyDisconnectedSpace α] (x : α), connectedComponent x = {x}
-- Mathlib.Order.InitialSeg
InitialSeg.toRelEmbedding : {α : Type u_4} → {β : Type u_5} → {r : α → α → Prop} → {s : β → β → Prop} → InitialSeg r s → r ↪r s
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Embedding.comp_codRestrict : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} {P : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
  [inst_2 : L.Structure P] (f : L.Embedding M N) (g : L.Embedding N P) (p : L.Substructure P) (h : ∀ (b : N), g b ∈ p),
  (FirstOrder.Language.Embedding.codRestrict p g h).comp f = FirstOrder.Language.Embedding.codRestrict p (g.comp f) ⋯
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.algebraMap_inj : ∀ {R : Type u_1} {a b : R} [inst : CommSemiring R] {x y : R},
  (algebraMap R (QuadraticAlgebra R a b)) x = (algebraMap R (QuadraticAlgebra R a b)) y ↔ x = y
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.MethodSpecs
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.MethodSpecs.0.reduceMethod : String → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step
-- Mathlib.Data.ZMod.Basic
ZMod.exists : ∀ {n : ℕ} {P : ZMod n → Prop}, (∃ x, P x) ↔ ∃ x, P ↑x
-- Mathlib.Data.Nat.Dist
Nat.dist_pos_of_ne : ∀ {i j : ℕ}, i ≠ j → 0 < i.dist j
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxc.Iterator.instIteratorLoop.loop.congr_simp : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] {inst_2 : DecidableLE α} [inst_3 : DecidableLE α]
  [inst_4 : Std.PRange.LawfulUpwardEnumerable α] [inst_5 : Std.PRange.LawfulUpwardEnumerableLE α] {n : Type u → Type w}
  [inst_6 : Monad n] (γ : Type u) (Pl : α → γ → ForInStep γ → Prop) (LargeEnough : α → Prop)
  (hl : ∀ (a b : α), a ≤ b → LargeEnough a → LargeEnough b) (upperBound : α) (acc acc_1 : γ),
  acc = acc_1 →
    ∀ (next next_1 : α) (e_next : next = next_1) (h : LargeEnough next)
      (f f_1 : (out : α) → LargeEnough out → out ≤ upperBound → (c : γ) → n (Subtype (Pl out c))),
      f = f_1 →
        Std.Rxc.Iterator.instIteratorLoop.loop γ Pl LargeEnough hl upperBound acc next h f =
          Std.Rxc.Iterator.instIteratorLoop.loop γ Pl LargeEnough hl upperBound acc_1 next_1 ⋯ f_1
-- Mathlib.Algebra.Star.Unitary
Unitary.instGroupSubtypeMemSubmonoidUnitary : {R : Type u_1} → [inst : Monoid R] → [inst_1 : StarMul R] → Group ↥(unitary R)
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Rco.count_iter : ∀ {α : Type u_1} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerableLT α] [Std.Rxo.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] [inst_6 : Std.Rxo.HasSize α] [Std.Rxo.LawfulHasSize α] {r : Std.Rco α},
  r.iter.length = r.size
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.apply_lt_nfpFamily : ∀ {ι : Type u_1} {f : ι → Ordinal.{u} → Ordinal.{u}} [Small.{u, u_1} ι],
  (∀ (i : ι), Order.IsNormal (f i)) →
    ∀ {a b : Ordinal.{u}}, b < Ordinal.nfpFamily f a → ∀ (i : ι), f i b < Ordinal.nfpFamily f a