mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.FiniteDimension
Submodule.ClosedComplemented.of_disjoint_of_finiteDimensional_quotient : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] [inst_5 : Module 𝕜 E] [ContinuousSMul 𝕜 E]
  {A B : Submodule 𝕜 E} [B_cofg : FiniteDimensional 𝕜 (E ⧸ B)], IsClosed ↑B → Disjoint A B → A.ClosedComplemented
-- Mathlib.Data.Int.ModEq
Int.modEq_modulus_mul_add_iff : ∀ {n a b c : ℤ}, a ≡ n * b + c [ZMOD n] ↔ a ≡ c [ZMOD n]
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
CategoryTheory.Limits.HasStrictInitialObjects.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (∀ {I A : C} (f : A ⟶ I) (a : CategoryTheory.Limits.IsInitial I), CategoryTheory.IsIso f) →
    CategoryTheory.Limits.HasStrictInitialObjects C
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.equivPolynomial_symm_monomial : ∀ {R : Type u_2} [inst : CommRing R] {S : Type u_6} [inst_1 : CommRing S] [inst_2 : Algebra R S] (n : ℕ) (x : S),
  PolynomialModule.equivPolynomial.symm ((Polynomial.monomial n) x) = PolynomialModule.single R n x
-- Mathlib.Probability.Kernel.Disintegration.Integral
MeasureTheory.Integrable.norm_integral_condKernel : ∀ {α : Type u_1} {Ω : Type u_2} {E : Type u_3} {mα : MeasurableSpace α} [inst : MeasurableSpace Ω]
  [inst_1 : StandardBorelSpace Ω] [inst_2 : Nonempty Ω] [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace ℝ E]
  {ρ : MeasureTheory.Measure (α × Ω)} [inst_5 : MeasureTheory.IsFiniteMeasure ρ] {f : α × Ω → E},
  MeasureTheory.Integrable f ρ → MeasureTheory.Integrable (fun x => ‖∫ (y : Ω), f (x, y) ∂ρ.condKernel x‖) ρ.fst
-- Batteries.Data.Fin.Coding
Fin.getRepr_getRepr : ∀ {n : ℕ} (s : Setoid (Fin n)) [inst : DecidableRel ⇑s] (x : Fin n), Fin.getRepr s (Fin.getRepr s x) = Fin.getRepr s x
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.lift_le : ∀ {a b : Ordinal.{v}}, Ordinal.lift.{u, v} a ≤ Ordinal.lift.{u, v} b ↔ a ≤ b
-- Mathlib.CategoryTheory.Join.Basic
/-- A pair of functors `F : C ⥤ E, G : D ⥤ E` as well as a natural transformation
`α : (Prod.fst C D) ⋙ F ⟶ (Prod.snd C D) ⋙ G` defines a functor out of `C ⋆ D`.
This is the main entry point to define functors out of a join of categories.  -/
CategoryTheory.Join.mkFunctor : {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] →
            (F : CategoryTheory.Functor C E) →
              (G : CategoryTheory.Functor D E) →
                ((CategoryTheory.Prod.fst C D).comp F ⟶ (CategoryTheory.Prod.snd C D).comp G) →
                  CategoryTheory.Functor (CategoryTheory.Join C D) E
-- Mathlib.Data.Rat.Encodable
Rat.instEncodable : Encodable ℚ
-- Init.Data.String.Iterate
String.Slice.PosIterator.mk.sizeOf_spec : ∀ {s : String.Slice} (currPos : s.Pos), sizeOf { currPos := currPos } = 1 + sizeOf currPos
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.cons_tail_dropLast_concat : ∀ {p : DyckWord}, p ≠ 0 → DyckStep.U :: (↑p).dropLast.tail ++ [DyckStep.D] = ↑p
-- Mathlib.Data.List.Duplicate
List.Duplicate.not_nodup : ∀ {α : Type u_1} {l : List α} {x : α}, List.Duplicate x l → ¬l.Nodup
-- Mathlib.LinearAlgebra.SymplecticGroup
/-- Given square matrices `A` and `C` over a field, if the only vector annihilated by both of
them is 0, and `Aᵀ * C = Cᵀ * A`, then one can construct a symmetric matrix `X` such that
`A + X * C` is invertible.

This lemma, together with the one after, is used to turn the upper-left block into invertible
matrix in the main proof, so that we can use the previous lemma to calculate the determinant.  -/
_private.Mathlib.LinearAlgebra.SymplecticGroup.0.SymplecticGroup.exists_symmetric_X_invertible_add_mul_of_ker_inter_eq_bot : ∀ {l : Type u_1} [inst : DecidableEq l] [inst_1 : Fintype l] {R : Type u_3} [inst_2 : Field R] {A C : Matrix l l R},
  (∀ (x : l → R), A • x = 0 → C • x = 0 → x = 0) →
    A.transpose * C = C.transpose * A → ∃ X, X.IsSymm ∧ IsUnit (A + X * C)
-- Lean.Setup
Lean.instReprModuleArtifacts : Repr Lean.ModuleArtifacts
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.equivalence₀_functor : ∀ {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] [inst_2 : CategoryTheory.Category.{v_4, u_4} B'] (eA : A ≌ A')
  (e' : A' ≌ B'), (AlgebraicTopology.DoldKan.Compatibility.equivalence₀ eA e').functor = eA.functor.comp e'.functor
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t t_1 : Std.TreeMap α β cmp) (e_t : t = t_1)
  (h : t.isEmpty = false), t.minKey h = t_1.minKey ⋯
-- Qq.Match
/-- A floated-out auxiliary binding: `let $name : $type := $value`.  -/
_private.Qq.Match.0.Qq.Lift : Type
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.comp_continuous_iff : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : FunLike F α β] [DilationClass F α β] (f : F) {γ : Type u_5} [inst_4 : TopologicalSpace γ] {g : γ → α},
  Continuous (⇑f ∘ g) ↔ Continuous g
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
EisensteinSeries.summable_right_one_div_linear_sub_one_div_linear_succ : ∀ (z : UpperHalfPlane) (m : ℤ), Summable fun b => 1 / (↑m * ↑z + ↑b) - 1 / (↑m * ↑z + ↑b + 1)
-- Mathlib.CategoryTheory.Profunctor.Basic
/-- Custom structure to construct natural transformations between profunctors, see
`CategoryTheory.Profunctor.ofHom`.  -/
CategoryTheory.ProfunctorCore.Hom : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D →
          CategoryTheory.ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D → Type (max (max u₁ u₂) w)
-- Mathlib.Computability.Primrec.List
/-- Checking if every element of a list satisfies a decidable predicate is primitive recursive.  -/
PrimrecPred.forall_mem_list : ∀ {α : Type u_1} {p : α → Prop} [inst : Primcodable α], PrimrecPred p → PrimrecPred fun L => ∀ a ∈ L, p a
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.subseq_forall_of_frequently : ∀ {ι : Type u_6} {x : ℕ → ι} {p : ι → Prop} {l : Filter ι},
  Filter.Tendsto x Filter.atTop l →
    (∃ᶠ (n : ℕ) in Filter.atTop, p (x n)) →
      ∃ ns, Filter.Tendsto (fun n => x (ns n)) Filter.atTop l ∧ ∀ (n : ℕ), p (x (ns n))
-- Lean.CoreM
/-- Auxiliary datastructure for converting `String.Pos` into Line/Column number.  -/
Lean.Core.Context.fileMap : Lean.Core.Context → Lean.FileMap
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_set_mem : ∀ {α : Type u_1} (a : α), Measurable fun s => a ∈ s
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.foldr_eq_foldr_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} {δ : Type w} [inst : Std.TransCmp cmp]
  {f : α → β → δ → δ} {init : δ}, Std.ExtTreeMap.foldr f init t = List.foldr (fun a b => f a.1 a.2 b) init t.toList
-- Mathlib.Data.Fintype.Defs
Bool.fintype : Fintype Bool
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteElement.mk_zero : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K],
  ArchimedeanClass.FiniteElement.mk 0 ⋯ = 0
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.mem_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp] {k : α},
  k ∈ t.toList ↔ k ∈ t
-- Mathlib.Topology.Compactness.Lindelof
isLindelof_iff_countable : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} [DiscreteTopology X], IsLindelof s ↔ s.Countable
-- Init.GrindInstances.Ring.UInt
USize.natCast : NatCast USize
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
/-- A function is `C^k` on a union of open sets `s i` iff it is `C^k` on each `s i`.  -/
contMDiffOn_iUnion_iff_of_isOpen : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] {f : M → M'}
  {n : WithTop ℕ∞} {ι : Type u_11} {s : ι → Set M},
  (∀ (i : ι), IsOpen (s i)) → (ContMDiffOn I I' n f (⋃ i, s i) ↔ ∀ (i : ι), ContMDiffOn I I' n f (s i))
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.left_neg : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  (X : C) [self : CategoryTheory.AddGrpObj X],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift CategoryTheory.AddGrpObj.neg (CategoryTheory.CategoryStruct.id X))
      CategoryTheory.AddMonObj.add =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X)
      CategoryTheory.AddMonObj.zero
-- Mathlib.Data.Set.Function
Set.bijOn_id : ∀ {α : Type u_1} (s : Set α), Set.BijOn id s s
-- Mathlib.Topology.Algebra.InfiniteSum.Group
summable_congr_atTop : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α] [IsTopologicalAddGroup α] {f₁ g₁ : ℕ → α},
  f₁ =ᶠ[Filter.atTop] g₁ → (Summable f₁ ↔ Summable g₁)
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.piTensorHomMapFun₂_add : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {t : ι → Type u_11} {t' : ι → Type u_12} [inst_3 : (i : ι) → AddCommMonoid (t i)]
  [inst_4 : (i : ι) → Module R (t i)] [inst_5 : (i : ι) → AddCommMonoid (t' i)] [inst_6 : (i : ι) → Module R (t' i)]
  (φ ψ : PiTensorProduct R fun i => s i →ₗ[R] t i →ₗ[R] t' i),
  (φ + ψ).piTensorHomMapFun₂ = φ.piTensorHomMapFun₂ + ψ.piTensorHomMapFun₂
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.log_conj : ∀ (x : ℂ), x.arg ≠ Real.pi → Complex.log ((starRingEnd ℂ) x) = (starRingEnd ℂ) (Complex.log x)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.pullbackId_hom_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.id X)],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.whiskerRight (CategoryTheory.ChosenPullbacksAlong.pullbackId X).hom
        (CategoryTheory.Over.map (CategoryTheory.CategoryStruct.id X)))
      (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.CategoryStruct.id X)).counit =
    (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.CategoryStruct.id X)).counit
-- Batteries.Tactic.Lint.Simp
Batteries.Tactic.Lint.SimpTheoremInfo.mk.sizeOf_spec : ∀ (hyps : Array Lean.Expr) (lhs rhs : Lean.Expr),
  sizeOf { hyps := hyps, lhs := lhs, rhs := rhs } = 1 + sizeOf hyps + sizeOf lhs + sizeOf rhs
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.dirac_apply_of_notMem : ∀ {β : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [inst_2 : MeasurableSpace β]
  {x : β} {v : M} {s : Set β}, x ∉ s → (MeasureTheory.VectorMeasure.dirac x v) s = 0
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- If `F.cocones` is corepresented by `X`, any cocone is the extension of the colimit cocone by the
corresponding morphism.  -/
CategoryTheory.Limits.IsColimit.OfNatIso.cocone_fac : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {X : C} (h : F.cocones.CorepresentableBy X) (s : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Limits.IsColimit.OfNatIso.colimitCocone h).extend
      (CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone h s) =
    s
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.smul_apply : ∀ {α : Type u} {β : Type v} {𝕜 : Type u_2} [inst : PseudoMetricSpace 𝕜] [inst_1 : TopologicalSpace α]
  [inst_2 : PseudoMetricSpace β] [inst_3 : Zero 𝕜] [inst_4 : Zero β] [inst_5 : SMul 𝕜 β] [inst_6 : IsBoundedSMul 𝕜 β]
  (c : 𝕜) (f : BoundedContinuousFunction α β) (x : α), (c • f) x = c • f x
-- Init.Data.Nat.Bitwise.Lemmas
Nat.and_le_right : ∀ {n m : ℕ}, n &&& m ≤ m
-- Init.Data.Array.MinMax
_private.Init.Data.Array.MinMax.0.Array.max_singleton : ∀ {α : Type u_1} [inst : Max α] {x : α}, #[x].max ⋯ = x
-- Mathlib.RingTheory.LocalRing.Pullback
RingHom.isUnit_pullback_mk_iff : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : Ring R] [inst_1 : Ring S] [inst_2 : Semiring T] (f : R →+* T)
  (g : S →+* T) {a : R × S} (a_in : a ∈ f.pullback g), IsUnit ⟨a, a_in⟩ ↔ IsUnit a.1 ∧ IsUnit a.2
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.CommShiftCore.shift_app : ∀ {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] {F₁ F₂ : CategoryTheory.Functor C D} (τ : F₁ ⟶ F₂) {A : Type u_5}
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F₁.CommShift A] [inst_6 : F₂.CommShift A] {a : A},
  CategoryTheory.NatTrans.CommShiftCore τ a →
    ∀ (X : C),
      (CategoryTheory.shiftFunctor D a).map (τ.app X) =
        CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F₁ a).inv.app X)
          (CategoryTheory.CategoryStruct.comp (τ.app ((CategoryTheory.shiftFunctor C a).obj X))
            ((CategoryTheory.Functor.commShiftIso F₂ a).hom.app X))
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.alternatingProd_singleton : ∀ {G : Type u_7} [inst : One G] [inst_1 : Mul G] [inst_2 : Inv G] (a : G), [a].alternatingProd = a
-- Init.Data.String.Search
String.revPosOfAux : String → Char → String.Pos.Raw → Option String.Pos.Raw
-- Lean.DocString.Types
Lean.Doc.Inline.text.sizeOf_spec : ∀ {i : Type u} [inst : SizeOf i] (string : String), sizeOf (Lean.Doc.Inline.text string) = 1 + sizeOf string
-- Mathlib.RingTheory.Ideal.Pure
Ideal.Pure.of_isIdempotentElem : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R}, I.FG → IsIdempotentElem I → I.Pure
-- Std.Sat.AIG.Basic
/-- The empty AIG is a DAG.
 -/
Std.Sat.AIG.IsDAG.empty : ∀ {α : Type}, Std.Sat.AIG.IsDAG α #[Std.Sat.AIG.Decl.false]
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.coe_mk : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (f : M ≃ N) (hf : ∀ (x y : M), f (x + y) = f x + f y),
  ⇑{ toEquiv := f, map_add' := hf } = ⇑f
-- Mathlib.Topology.Algebra.Monoid
continuous_finsum_cond : ∀ {ι : Type u_1} {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M]
  [inst_2 : AddCommMonoid M] [ContinuousAdd M] {f : ι → X → M} {p : ι → Prop},
  (∀ (i : ι), p i → Continuous (f i)) →
    (LocallyFinite fun i => Function.support (f i)) → Continuous fun x => ∑ᶠ (i : ι) (_ : p i), f i x
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- Technical lemma stating how `c.applyOrderedFinpartition` commutes with updating variables. This
will be the key point to show that functions constructed from `applyOrderedFinpartition` retain
multilinearity.  -/
OrderedFinpartition.applyOrderedFinpartition_update_right : ∀ {𝕜 : 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] {n : ℕ}
  (c : OrderedFinpartition n) (p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F) (j : Fin n) (v : Fin n → E) (z : E),
  c.applyOrderedFinpartition p (Function.update v j z) =
    Function.update (c.applyOrderedFinpartition p v) (c.index j)
      ((p (c.index j)) (Function.update (v ∘ c.emb (c.index j)) (c.invEmbedding j) z))
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.genEigenspace_mem_invtSubmodule : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Module.End R M)
  (μ : R) (n : ℕ∞), (f.genEigenspace μ) n ∈ f.invtSubmodule
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- In the specific case of multilinear maps on spaces indexed by `Fin (n+1)`, where one can build
an element of `∀ (i : Fin (n+1)), M i` using `snoc`, one can express directly the additivity of a
multilinear map along the first variable.  -/
MultilinearMap.snoc_add : ∀ {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
  [inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂] (f : MultilinearMap R M M₂)
  (m : (i : Fin n) → M i.castSucc) (x y : M (Fin.last n)), f (Fin.snoc m (x + y)) = f (Fin.snoc m x) + f (Fin.snoc m y)
-- Aesop.Percent
Aesop.Percent.instOrd : Ord Aesop.Percent
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
CategoryTheory.Limits.KernelFork.map_condition : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  {X Y : C} {f : X ⟶ Y} (c : CategoryTheory.Limits.KernelFork f) (G : CategoryTheory.Functor C D)
  [G.PreservesZeroMorphisms], CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.Fork.ι c)) (G.map f) = 0
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
HasFibers.Fib.isoMk_hom : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} [inst_2 : HasFibers p] {S : 𝒮} {a b : HasFibers.Fib p S}
  (Φ : (HasFibers.ι S).obj a ≅ (HasFibers.ι S).obj b) (hΦ : p.IsHomLift (CategoryTheory.CategoryStruct.id S) Φ.hom),
  (HasFibers.Fib.isoMk Φ hΦ).hom = HasFibers.Fib.homMk Φ.hom
-- Mathlib.Topology.Bases
/-- A topological basis is one that satisfies the necessary conditions so that
it suffices to take unions of the basis sets to get a topology (without taking
finite intersections as well).  -/
TopologicalSpace.IsTopologicalBasis : {α : Type u} → [t : TopologicalSpace α] → Set (Set α) → Prop
-- Mathlib.Computability.Primrec.List
List.lookup.eq_2 : ∀ {α : Type u} {β : Type v} [inst : BEq α] (x k : α) (b : β) (as : List (α × β)),
  List.lookup x ((k, b) :: as) =
    match x == k with
    | true => some b
    | false => List.lookup x as
-- Mathlib.Topology.Bornology.Basic
Bornology.isCobounded_iInter : ∀ {ι : Type u_1} {α : Type u_2} [inst : Bornology α] [Finite ι] {f : ι → Set α},
  Bornology.IsCobounded (⋂ i, f i) ↔ ∀ (i : ι), Bornology.IsCobounded (f i)
-- Init.Data.Array.Find
Array.findIdx_append : ∀ {α : Type u_1} {p : α → Bool} {xs ys : Array α},
  Array.findIdx p (xs ++ ys) = if Array.findIdx p xs < xs.size then Array.findIdx p xs else Array.findIdx p ys + xs.size
-- Lean.Expr
Lean.Expr.letE.injEq : ∀ (declName : Lean.Name) (type value body : Lean.Expr) (nondep : Bool) (declName_1 : Lean.Name)
  (type_1 value_1 body_1 : Lean.Expr) (nondep_1 : Bool),
  (Lean.Expr.letE declName type value body nondep = Lean.Expr.letE declName_1 type_1 value_1 body_1 nondep_1) =
    (declName = declName_1 ∧ type = type_1 ∧ value = value_1 ∧ body = body_1 ∧ nondep = nondep_1)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodySumFun_smul : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (c : ℝ) (x : NumberField.mixedEmbedding.mixedSpace K),
  NumberField.mixedEmbedding.convexBodySumFun (c • x) = |c| * NumberField.mixedEmbedding.convexBodySumFun x
-- Mathlib.RingTheory.NormalClosure
Ring.instAlgebraNormalClosure_1 : (R : Type u_1) →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : IsDomain R] →
          [inst_3 : IsDomain S] →
            [inst_4 : Algebra R S] → [inst_5 : Module.IsTorsionFree R S] → Algebra R (Ring.NormalClosure R S)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.restrictScalars_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] {A : Type u_5}
  [inst_2 : CommSemiring A] [inst_3 : Algebra R A] [inst_4 : Module R M] (S : Submonoid R) {N : Type u_6}
  [inst_5 : AddCommMonoid N] [inst_6 : Module R N] [inst_7 : Module A M] [inst_8 : Module A N]
  [inst_9 : IsScalarTower R A M] [inst_10 : IsScalarTower R A N] (f : M →ₗ[A] N),
  IsLocalizedModule (Algebra.algebraMapSubmonoid A S) f ↔ IsLocalizedModule S (↑R f)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
/-- The pullback of `f, g` is also the pullback of `f ≫ i, g ≫ i` for any mono `i`.  -/
CategoryTheory.Limits.pullbackIsPullbackOfCompMono : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} →
      (f : X ⟶ W) →
        (g : Y ⟶ W) →
          (i : W ⟶ Z) →
            [inst_1 : CategoryTheory.Mono i] →
              [inst_2 : CategoryTheory.Limits.HasPullback f g] →
                CategoryTheory.Limits.IsLimit
                  (CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.Limits.pullback.fst f g)
                    (CategoryTheory.Limits.pullback.snd f g) ⋯)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cochain.fromSingleMk_v_eq_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ}
  (h : p + n = q) (p' q' : ℤ) (hpq' : p' + n = q'),
  p' ≠ p → (CochainComplex.HomComplex.Cochain.fromSingleMk f h).v p' q' hpq' = 0
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- An equivalence of the index set defines an equivalence between the spaces of continuous
multilinear maps. In case of normed spaces, this is a linear isometric equivalence, see
`ContinuousMultilinearMap.domDomCongrₗᵢ`.  -/
ContinuousMultilinearMap.domDomCongrEquiv : {R : Type u} →
  {ι : Type v} →
    {M₂ : Type w₂} →
      {M₃ : Type w₃} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M₂] →
            [inst_2 : AddCommMonoid M₃] →
              [inst_3 : Module R M₂] →
                [inst_4 : Module R M₃] →
                  [inst_5 : TopologicalSpace M₂] →
                    [inst_6 : TopologicalSpace M₃] →
                      {ι' : Type u_1} →
                        ι ≃ ι' →
                          ContinuousMultilinearMap R (fun x => M₂) M₃ ≃ ContinuousMultilinearMap R (fun x => M₂) M₃
-- Mathlib.Algebra.Field.Subfield.Basic
/-- The image under a ring homomorphism of the subfield generated by a set equals
the subfield generated by the image of the set.  -/
RingHom.map_field_closure : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] (f : K →+* L) (s : Set K),
  Subfield.map f (Subfield.closure s) = Subfield.closure (⇑f '' s)
-- Mathlib.Topology.MetricSpace.Closeds
TopologicalSpace.NonemptyCompacts.isometry_singleton : ∀ {α : Type u_1} [inst : EMetricSpace α], Isometry fun x => {x}
-- Lean.Syntax
Lean.Syntax.Traverser.mk : Lean.Syntax → Array Lean.Syntax → Array ℕ → Lean.Syntax.Traverser
-- Init.Data.String.OrderInstances
String.Pos.Raw.instTotalLe : Std.Total fun x1 x2 => x1 ≤ x2
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_erase : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α},
  (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.isEmpty =
    (t.isEmpty || decide (t.size = 1) && Std.DTreeMap.Internal.Impl.contains k t)
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.neg_toAddSubmonoid : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (S : Submodule R M),
  (-S).toAddSubmonoid = -S.toAddSubmonoid
-- Lean.Parser.Term
Lean.Parser.Term.argument : Lean.Parser.Parser
-- Lean.Server.FileWorker.SemanticHighlighting
/-- Semantic token information with absolute LSP positions.  -/
Lean.Server.FileWorker.AbsoluteLspSemanticToken : Type