mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Optimization.ValuedCSP
/-- Cost function admits given fractional operation, i.e., `ω` improves `f` in the `≤` sense.  -/
Function.AdmitsFractional : {D : Type u_1} →
  {C : Type u_2} → [AddCommMonoid C] → [PartialOrder C] → {m n : ℕ} → ((Fin n → D) → C) → FractionalOperation D m → Prop
-- Mathlib.CategoryTheory.Subfunctor.Finite
CategoryTheory.Subfunctor.IsGeneratedBy.image : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)}
  {G : CategoryTheory.Subfunctor F} {ι : Type w'} {X : ι → Cᵒᵖ} {x : (i : ι) → F.obj (X i)},
  G.IsGeneratedBy x →
    ∀ {F' : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : F ⟶ F'),
      (G.image f).IsGeneratedBy fun i => (CategoryTheory.ConcreteCategory.hom (f.app (X i))) (x i)
-- Mathlib.RingTheory.PrincipalIdealDomain
Ideal.IsPrincipal.of_comap : ∀ {R : Type u} {S : Type u_1} {F : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S]
  [inst_3 : RingHomClass F R S] (f : F),
  Function.Surjective ⇑f → ∀ (I : Ideal S) [hI : Submodule.IsPrincipal (Ideal.comap f I)], Submodule.IsPrincipal I
-- Mathlib.CategoryTheory.Sites.Point.Category
CategoryTheory.GrothendieckTopology.Point.Hom.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.GrothendieckTopology C} {Φ₁ Φ₂ : J.Point}
  {x y : Φ₁.Hom Φ₂}, x = y ↔ x.hom = y.hom
-- Init.Data.String.ToSlice
String.instToSliceSlice : String.ToSlice String.Slice
-- Lean.Parser.Term
/-- The `finally` section trailing a `where` opens a tactic block to fill in `?hole`s in the definition body.
 -/
Lean.Parser.Term.whereFinally : Lean.Parser.Parser
-- Mathlib.Geometry.Manifold.Instances.Real
modelWithCornersEuclideanHalfSpace_symm_apply : ∀ {n : ℕ} [inst : NeZero n] (x : EuclideanSpace ℝ (Fin n)),
  ↑(modelWithCornersEuclideanHalfSpace n).symm x = ⟨WithLp.toLp 2 (Function.update x.ofLp 0 (max (x.ofLp 0) 0)), ⋯⟩
-- Mathlib.RingTheory.Valuation.Integers
/-- Let `O` be the integers of the valuation `v` on some commutative ring `R`. For every element `x` in
`O`, `x` is a unit in `O` if and only if the image of `x` in `R` is a unit and has valuation 1.
 -/
Valuation.Integers.isUnit_of_one : ∀ {R : Type u} {Γ₀ : Type v} [inst : CommRing R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀}
  {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O R],
  v.Integers O → ∀ {x : O}, IsUnit ((algebraMap O R) x) → v ((algebraMap O R) x) = 1 → IsUnit x
-- Mathlib.LinearAlgebra.Matrix.HadamardMatrix
/-- A Hadamard matrix over a reduced commutative ring has nonzero determinant, provided the order
is nonzero in `R`.  -/
Matrix.IsHadamard.det_ne_zero : ∀ {n : Type u_2} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] [inst_3 : StarRing R]
  {A : Matrix n n R} [IsReduced R], A.IsHadamard → ↑(Fintype.card n) ≠ 0 → A.det ≠ 0
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
_private.Mathlib.RingTheory.Polynomial.Cyclotomic.Eval.0.Polynomial.cyclotomic_neg_one_pos : ∀ {n : ℕ},
  2 < n →
    ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R],
      0 < Polynomial.eval (-1) (Polynomial.cyclotomic n R)
-- Mathlib.RingTheory.Ideal.Operations
/-- This duplicates the global `smul_eq_mul`, but doesn't have to unfold anywhere near as much to
apply.  -/
Ideal.smul_eq_mul : ∀ {R : Type u} [inst : Semiring R] (I J : Ideal R), I • J = I * J
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.Ring.OfSemiring.of_eq : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α)
  (lhs rhs : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.Expr.denoteS ctx lhs = Lean.Grind.CommRing.Expr.denoteS ctx rhs →
    Lean.Grind.CommRing.Expr.denoteSAsRing ctx lhs = Lean.Grind.CommRing.Expr.denoteSAsRing ctx rhs
-- Mathlib.Data.Finset.Card
/-- **Alias** of the reverse direction of `Finset.card_union_eq_card_add_card`. -/
Finset.card_union_of_disjoint : ∀ {α : Type u_1} {s t : Finset α} [inst : DecidableEq α], Disjoint s t → (s ∪ t).card = s.card + t.card
-- Mathlib.Probability.Moments.MGFAnalytic
ProbabilityTheory.analyticOn_iteratedDeriv_mgf : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (n : ℕ),
  AnalyticOn ℝ (iteratedDeriv n (ProbabilityTheory.mgf X μ)) (interior (ProbabilityTheory.integrableExpSet X μ))
-- Mathlib.Algebra.Order.AddTorsor
instIsOrderedCancelVAddOfIsOrderedAddCancelMonoid : ∀ {G : Type u_1} [inst : AddCommMonoid G] [inst_1 : Preorder G] [IsOrderedCancelAddMonoid G], IsOrderedCancelVAdd G G
-- Mathlib.Topology.Separation.Basic
Set.Subsingleton.isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {s : Set X}, s.Subsingleton → IsClosed s
-- Mathlib.CategoryTheory.MorphismProperty.Descent
CategoryTheory.MorphismProperty.pullback_fst_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.MorphismProperty C} {X Y Z : C}
  {f : X ⟶ Z} {g : Y ⟶ Z} [P.IsStableUnderBaseChange] [P.DescendsAlong Q]
  [inst_3 : CategoryTheory.Limits.HasPullback f g], Q f → (P (CategoryTheory.Limits.pullback.fst f g) ↔ P g)
-- Mathlib.Topology.EMetricSpace.Diam
/-- If two points belong to some set, their edistance is bounded by the diameter of the set  -/
Metric.edist_le_ediam_of_mem : ∀ {X : Type u_2} {s : Set X} {x y : X} [inst : PseudoEMetricSpace X], x ∈ s → y ∈ s → edist x y ≤ Metric.ediam s
-- Init.Data.Array.MapIdx
_private.Init.Data.Array.MapIdx.0.Array.mapFinIdxM.map.match_1.eq_1 : ∀ {α : Type u_1} (as : Array α) (j : ℕ) (motive : (i : ℕ) → i + j = as.size → Sort u_2) (x : 0 + j = as.size)
  (h_1 : (x : 0 + j = as.size) → motive 0 x) (h_2 : (i : ℕ) → (inv : i + 1 + j = as.size) → motive i.succ inv),
  (match 0, x with
    | 0, x => h_1 x
    | i.succ, inv => h_2 i inv) =
    h_1 x
-- Mathlib.Order.Category.BddDistLat
BddDistLat.hom_ext_iff : ∀ {X Y : BddDistLat} {f g : X ⟶ Y}, f = g ↔ BddDistLat.Hom.hom f = BddDistLat.Hom.hom g
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_smul_of_pos : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (v : V) (p q : P) {r : ℝ}, 0 < r → ((signedDist (r • v)) p) q = ((signedDist v) p) q
-- Lean.Elab.Command
Lean.Elab.Command.instMonadInfoTreeCommandElabM : Lean.Elab.MonadInfoTree Lean.Elab.Command.CommandElabM
-- Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
integrable_mulExpNegMulSq_comp : ∀ {E : Type u_1} [inst : TopologicalSpace E] [inst_1 : MeasurableSpace E] [BorelSpace E] {P : MeasureTheory.Measure E}
  [MeasureTheory.IsFiniteMeasure P] {ε : ℝ} (f : C(E, ℝ)),
  0 < ε → MeasureTheory.Integrable (fun x => ε.mulExpNegMulSq (f x)) P
-- Aesop.Util.UnionFind
Aesop.UnionFind.mk.injEq : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : Hashable α] (parents sizes : Array USize) (toRep : Std.HashMap α USize)
  (parents_1 sizes_1 : Array USize) (toRep_1 : Std.HashMap α USize),
  ({ parents := parents, sizes := sizes, toRep := toRep } =
      { parents := parents_1, sizes := sizes_1, toRep := toRep_1 }) =
    (parents = parents_1 ∧ sizes = sizes_1 ∧ toRep = toRep_1)
-- Lean.Data.JsonRpc
Lean.JsonRpc.Response.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (id : Lean.JsonRpc.RequestID) (result : α),
  sizeOf { id := id, result := result } = 1 + sizeOf id + sizeOf result
-- Mathlib.FieldTheory.IsSepClosed
IsSepClosure.isGalois : ∀ {k : Type u} [inst : Field k] {K : Type v} [inst_1 : Field K] [inst_2 : Algebra k K] [IsSepClosure k K], IsGalois k K
-- Mathlib.Topology.UniformSpace.Cauchy
IsComplete.union : ∀ {α : Type u} [uniformSpace : UniformSpace α] {s t : Set α}, IsComplete s → IsComplete t → IsComplete (s ∪ t)
-- Mathlib.Analysis.Calculus.FDeriv.Add
Differentiable.const_sub : ∀ {𝕜 : 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},
  Differentiable 𝕜 f → ∀ (c : F), Differentiable 𝕜 fun y => c - f y
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.colimitHomIsoLimitYoneda'.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (F : CategoryTheory.Functor Iᵒᵖ C) [inst_2 : CategoryTheory.Limits.HasColimit F]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape I (Type u₂)] (A : C),
  CategoryTheory.Limits.colimitHomIsoLimitYoneda' F A = CategoryTheory.Limits.colimitHomIsoLimitYoneda' F A
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.strictConvexOn_mul_log : StrictConvexOn ℝ (Set.Ici 0) fun x => x * Real.log x
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Kernels
/-- A colimit cokernel cofork gives a limit kernel fork in the opposite category  -/
CategoryTheory.Limits.CokernelCofork.IsColimit.ofπOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y Q : C} →
        (p : Y ⟶ Q) →
          {f : X ⟶ Y} →
            (w : CategoryTheory.CategoryStruct.comp f p = 0) →
              CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ p w) →
                CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι p.op ⋯)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.size_eq_match_rcc : ∀ {α : Type u} {r : Std.Roo α} [inst : LT α] [DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.Rxo.HasSize α] [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [Std.Rxo.IsAlwaysFinite α] [Std.Rxo.LawfulHasSize α],
  r.size =
    match Std.PRange.succ? r.lower with
    | none => 0
    | some next => (next...r.upper).size
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.smul_measure : ∀ {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : ENorm ε] {f : α → ε},
  MeasureTheory.HasFiniteIntegral f μ → ∀ {c : ENNReal}, c ≠ ⊤ → MeasureTheory.HasFiniteIntegral f (c • μ)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getD_toArray_rcc : ∀ {m n fallback : ℤ} {i : ℕ}, (m...=n).toArray.getD i fallback = if i < (n + 1 - m).toNat then m + ↑i else fallback
-- Mathlib.Analysis.Convex.Join
mem_convexJoin : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s t : Set E} {x : E}, x ∈ convexJoin 𝕜 s t ↔ ∃ a ∈ s, ∃ b ∈ t, x ∈ segment 𝕜 a b
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.coend.ι_desc : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_2 : CategoryTheory.Limits.HasCoend F] {X : C}
  (f : (j : J) → (F.obj (Opposite.op j)).obj j ⟶ X)
  (hf :
    ∀ ⦃i j : J⦄ (g : i ⟶ j),
      CategoryTheory.CategoryStruct.comp ((F.map g.op).app i) (f i) =
        CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op j)).map g) (f j))
  (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coend.ι F j) (CategoryTheory.Limits.coend.desc f hf) = f j
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_24 : HSub Std.Time.Hour.Offset Std.Time.Nanosecond.Offset Std.Time.Nanosecond.Offset
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_of_eventuallyEq_of_mem : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
  {P : (H → H') → Set H → H → Prop} {g g' : M → M'} {s : Set M} {x : M},
  G.LocalInvariantProp G' P →
    ChartedSpace.LiftPropWithinAt P g s x → g' =ᶠ[nhdsWithin x s] g → x ∈ s → ChartedSpace.LiftPropWithinAt P g' s x
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.inf_eq_map_pullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {A : C}
  (f₁ f₂ : CategoryTheory.Subobject A),
  f₁ ⊓ f₂ = (CategoryTheory.Subobject.map f₁.arrow).obj ((CategoryTheory.Subobject.pullback f₁.arrow).obj f₂)
-- Mathlib.Algebra.Module.Submodule.LinearMap
LinearMap.coe_sum : ∀ {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₂}
  {ι : Type u_10} (t : Finset ι) (f : ι → M →ₛₗ[σ₁₂] M₂), ⇑(∑ i ∈ t, f i) = ∑ i ∈ t, ⇑(f i)
-- Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
CategoryTheory.Limits.SequentialProduct.functorObj_eq_pos : ∀ {C : Type u_1} {M N : ℕ → C} {n m : ℕ}, m < n → (fun i => if x : i < n then M i else N i) m = M m
-- Mathlib.Algebra.GCDMonoid.Basic
lcm_eq_normalize : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {a b c : α},
  lcm a b ∣ c → c ∣ lcm a b → lcm a b = normalize c
-- Mathlib.Data.Finmap
Finmap.Disjoint.symm_iff : ∀ {α : Type u} {β : α → Type v} (x y : Finmap β), x.Disjoint y ↔ y.Disjoint x
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- This holds independent of `p` and does not require `[Fact (1 ≤ p)]`. We keep it separate
from `pi_Lp.pseudo_emetric_space` so it can be used also for `p < 1`.  -/
PiLp.edist_self : ∀ (p : ENNReal) {ι : Type u_2} {β : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → PseudoEMetricSpace (β i)]
  (f : PiLp p β), edist f f = 0
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithLowerSet.map_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (g : β →o γ) (f : α →o β),
  Topology.WithLowerSet.map (g.comp f) = (Topology.WithLowerSet.map g).comp (Topology.WithLowerSet.map f)
-- Batteries.Classes.Order
Std.LawfulBEqCmp.compareOfLessAndEq_of_lt_irrefl : ∀ {α : Type u_1} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : DecidableEq α] [inst_3 : BEq α] [LawfulBEq α],
  (∀ (x : α), ¬x < x) → Std.LawfulBEqCmp fun x1 x2 => compareOfLessAndEq x1 x2
-- Lean.Elab.Syntax
_private.Lean.Elab.Syntax.0.Lean.Elab.Term.withNestedParser : Lean.Elab.Term.ToParserDescr → Lean.Elab.Term.ToParserDescr
-- Mathlib.Topology.Sober
IsGenericPoint.isIrreducible : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {S : Set α}, IsGenericPoint x S → IsIrreducible S
-- Mathlib.RingTheory.KrullDimension.NonZeroDivisors
ringKrullDim_add_enatCard_le_ringKrullDim_mvPolynomial : ∀ {R : Type u_1} [inst : CommRing R] (σ : Type u_3), ringKrullDim R + ↑(ENat.card σ) ≤ ringKrullDim (MvPolynomial σ R)
-- Init.Data.Array.Basic
/-- Inserts an element into an array at the specified index. The array is returned unmodified if the
index is greater than the size of the array.

In other words, the new element is inserted into the array `as` after the first `i` elements of
`as`.

This function takes worst case `O(n)` time because it has to swap the inserted element into place.

Examples:
 * `#["tues", "thur", "sat"].insertIdxIfInBounds 1 "wed" = #["tues", "wed", "thur", "sat"]`
 * `#["tues", "thur", "sat"].insertIdxIfInBounds 2 "wed" = #["tues", "thur", "wed", "sat"]`
 * `#["tues", "thur", "sat"].insertIdxIfInBounds 3 "wed" = #["tues", "thur", "sat", "wed"]`
 * `#["tues", "thur", "sat"].insertIdxIfInBounds 4 "wed" = #["tues", "thur", "sat"]`
 -/
Array.insertIdxIfInBounds : {α : Type u} → Array α → ℕ → α → Array α
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.right : ∀ {α : Type u_1} [inst : Preorder α] {s : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
  Ordnode.Valid' o₁ (Ordnode.node s l x r) o₂ → Ordnode.Valid' (↑x) r o₂
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Priority.percent : Aesop.Percent → Aesop.Frontend.Priority
-- Mathlib.RingTheory.SimpleModule.Isotypic
/-- The endomorphism algebra of a semisimple module is the direct product of the endomorphism
algebras of its isotypic components.  -/
IsSemisimpleModule.endAlgEquiv : (R₀ : Type u_1) →
  (R : Type u_2) →
    (M : Type u) →
      [inst : CommSemiring R₀] →
        [inst_1 : Ring R] →
          [inst_2 : Algebra R₀ R] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [IsSemisimpleModule R M] →
                  [inst_6 : Module R₀ M] →
                    [inst_7 : IsScalarTower R₀ R M] →
                      [DecidableEq ↑(isotypicComponents R M)] →
                        Module.End R M ≃ₐ[R₀] (c : ↑(isotypicComponents R M)) → Module.End R ↥↑c
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extend_d_eq : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c') {i' j' : ι'}
  {i j : ι} (hi : e.f i = i') (hj : e.f j = j'),
  (K.extend e).d i' j' =
    CategoryTheory.CategoryStruct.comp (K.extendXIso e hi).hom
      (CategoryTheory.CategoryStruct.comp (K.d i j) (K.extendXIso e hj).inv)
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformContinuous_monoidHom_of_continuous : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {hom : Type u_3}
  [inst_3 : UniformSpace β] [inst_4 : Group β] [IsUniformGroup β] [inst_6 : FunLike hom α β] [MonoidHomClass hom α β]
  {f : hom}, Continuous ⇑f → UniformContinuous ⇑f
-- Mathlib.Topology.Compactness.Compact
IsCompact.exists_mapClusterPt : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {ι : Type u_2},
  IsCompact s →
    ∀ {f : Filter ι} [f.NeBot] {u : ι → X}, Filter.map u f ≤ Filter.principal s → ∃ x ∈ s, MapClusterPt x f u
-- Std.Http.Data.URI.Encoding
_private.Std.Http.Data.URI.Encoding.0.Std.Http.URI.isEncodedQueryChar.eq_1 : ∀ (rule : UInt8 → Bool) (c : UInt8),
  Std.Http.URI.isEncodedQueryChar rule c = decide (Std.Http.URI.isEncodedChar rule c = true ∨ c = '+'.toUInt8)
-- Mathlib.SetTheory.Ordinal.Basic
/-- Galois connection between `Cardinal.ord` and `Ordinal.card`.  -/
Cardinal.gc_ord_card : GaloisConnection Cardinal.ord Ordinal.card
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.equivWithAbs_symm : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v w : AbsoluteValue R S), (WithAbs.congr v w (RingEquiv.refl R)).symm = WithAbs.congr w v (RingEquiv.refl R).symm
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get_alter_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (h : (↑m).WF) {k : α} {f : Option β → Option β}
  {hc : (Std.DHashMap.Internal.Raw₀.Const.alter m k f).contains k = true},
  Std.DHashMap.Internal.Raw₀.Const.get (Std.DHashMap.Internal.Raw₀.Const.alter m k f) k hc =
    (f (Std.DHashMap.Internal.Raw₀.Const.get? m k)).get ⋯
-- Mathlib.Logic.Function.Conjugate
/-- A map `f` semiconjugates a binary operation `ga` to a binary operation `gb` if
for all `x`, `y` we have `f (ga x y) = gb (f x) (f y)`. E.g., a `MonoidHom`
semiconjugates `(*)` to `(*)`.
 -/
Function.Semiconj₂ : {α : Type u_1} → {β : Type u_2} → (α → β) → (α → α → α) → (β → β → β) → Prop
-- Mathlib.Data.List.Basic
List.get_length_sub_one : ∀ {α : Type u} {l : List α} (h : l.length - 1 < l.length), l.get ⟨l.length - 1, h⟩ = l.getLast ⋯
-- Init.Data.String.Basic
String.Pos.get_eq_get_ofSliceFrom : ∀ {s : String} {p₀ : s.Pos} {pos : (s.sliceFrom p₀).Pos} {h : pos ≠ (s.sliceFrom p₀).endPos},
  pos.get h = (String.Pos.ofSliceFrom pos).get ⋯
-- Lean.Elab.App
/-- Metavariables that we need to set the error context using the application being built.  -/
Lean.Elab.Term.ElabAppArgs.State.toSetErrorCtx : Lean.Elab.Term.ElabAppArgs.State → Array Lean.MVarId
-- Init.Data.Option.Lemmas
Option.map_id_fun' : ∀ {α : Type u}, (Option.map fun a => a) = id
-- Mathlib.CategoryTheory.Preadditive.FunctorCategory
CategoryTheory.NatTrans.app_zero : ∀ {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.Preadditive D]
  {F G : CategoryTheory.Functor C D} (X : C), CategoryTheory.NatTrans.app 0 X = 0
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.isUniformInducing_postcomp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : UniformSpace F] [inst_7 : IsUniformAddGroup F] {G : Type u_5} [inst_8 : AddCommGroup G]
  [inst_9 : UniformSpace G] [inst_10 : IsUniformAddGroup G] [inst_11 : Module 𝕜 G] (g : F →L[𝕜] G),
  IsUniformInducing ⇑g → IsUniformInducing g.compContinuousAlternatingMap
-- Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
/-- If `f` is a continuous `(n + 1)`-multilinear alternating map, `x` is an element of the domain,
and `v` is an `n`-vector, then the value of `f` at `v` with `x` inserted at the `p`th place
equals `(-1) ^ p` times the value of `f` at `v` with `x` prepended.  -/
ContinuousAlternatingMap.map_insertNth : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  (f : E [⋀^Fin (n + 1)]→L[𝕜] F) (p : Fin (n + 1)) (x : E) (v : Fin n → E),
  f (p.insertNth x v) = (-1) ^ ↑p • f (Matrix.vecCons x v)
-- Mathlib.Topology.UnitInterval
/-- Any open cover `c` of a closed interval `[a, b]` in ℝ
can be refined to a finite partition into subintervals.  -/
exists_monotone_Icc_subset_open_cover_Icc : ∀ {ι : Sort u_1} {a b : ℝ},
  a ≤ b →
    ∀ {c : ι → Set ↑(Set.Icc a b)},
      (∀ (i : ι), IsOpen (c i)) →
        Set.univ ⊆ ⋃ i, c i →
          ∃ t, ↑(t 0) = a ∧ Monotone t ∧ (∃ m, ∀ n ≥ m, ↑(t n) = b) ∧ ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ c i
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.sub_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddGroup α],
  Function.Periodic f c → ∀ (x : α), f (x - c) = f x
-- Lean.Parser.Term
Lean.Parser.Term.whereFinally.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.SetTheory.ZFC.Class
instComplClass : Compl Class.{u_1}
-- Init.GrindInstances.ToInt
Lean.Grind.instDivFinCoOfNatIntCast : ∀ {n : ℕ}, Lean.Grind.ToInt.Div (Fin n) (Lean.Grind.IntInterval.co 0 ↑n)
-- Aesop.Tree.ExtractScript
Aesop.ExtractScriptM.State.script : Aesop.ExtractScriptM.State → Aesop.Script.UScript
-- Aesop.Forward.State
/-- The hypothesis, or `none` if this is a rule pattern substitution.  -/
Aesop.Hyp.fvarId? : Aesop.Hyp → Option Lean.FVarId
-- Mathlib.Data.Bool.Basic
Bool.false_eq_true_eq_False : ¬false = true
-- Mathlib.Analysis.Convex.Segment
openSegment.eq_1 : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] (x y : E), openSegment 𝕜 x y = {z | ∃ a b, 0 < a ∧ 0 < b ∧ a + b = 1 ∧ a • x + b • y = z}
-- Init.Data.Vector.Lemmas
Vector.append_singleton : ∀ {α : Type u_1} {n : ℕ} {a : α} {xs : Vector α n}, xs ++ #v[a] = xs.push a
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_union_le_size_add_size : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → (m₁ ∪ m₂).size ≤ m₁.size + m₂.size
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.ofπ_var : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] (π : (relations.G →₀ A) →ₗ[A] M) (hπ : ∀ (r : relations.R), π (relations.relation r) = 0)
  (g : relations.G), (Module.Relations.Solution.ofπ π hπ).var g = π fun₀ | g => 1