mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Types.Coequalizers
/-- The categorical coequalizer in `Type u` is the quotient by `f g ~ g x`.  -/
CategoryTheory.Limits.Types.coequalizerIso : {X Y : Type u} →
  (f g : X ⟶ Y) →
    CategoryTheory.Limits.coequalizer f g ≅
      Function.Coequalizer ⇑(CategoryTheory.ConcreteCategory.hom f) ⇑(CategoryTheory.ConcreteCategory.hom g)
-- Mathlib.Algebra.CharP.Defs
ringChar.Nat.cast_ringChar : ∀ {R : Type u_1} [inst : NonAssocSemiring R], ↑(ringChar R) = 0
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- additive version of `MeasureTheory.Measure.haar.index`  -/
MeasureTheory.Measure.haar.addIndex : {G : Type u_1} → [AddGroup G] → Set G → Set G → ℕ
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `MeromorphicAt.div` -/
MeromorphicAt.fun_div : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {x : 𝕜} {f g : 𝕜 → 𝕜'},
  MeromorphicAt f x → MeromorphicAt g x → MeromorphicAt (fun i => f i / g i) x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.instSubsingletonBraidedCategory : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  Subsingleton (CategoryTheory.BraidedCategory C)
-- Init.Data.String.Defs
Char.isValidUTF8_toByteArray_utf8EncodeChar : ∀ {c : Char}, (String.utf8EncodeChar c).toByteArray.IsValidUTF8
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.instReflModEq : ∀ {M : Type u_1} [inst : AddCommMonoid M] {p : M}, Std.Refl (AddCommGroup.ModEq p)
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- The length-1 path between a pair of adjacent vertices.  -/
SimpleGraph.Path.singleton : {V : Type u} → {G : SimpleGraph V} → {u v : V} → G.Adj u v → G.Path u v
-- Mathlib.Algebra.Group.Subgroup.Pointwise
AddSubgroup.closure_add_le : ∀ {G : Type u_2} [inst : AddGroup G] (S T : Set G),
  AddSubgroup.closure (S + T) ≤ AddSubgroup.closure S ⊔ AddSubgroup.closure T
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.coe_infNndist : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α}, ↑(Metric.infNndist x s) = Metric.infDist x s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_insertMany!_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k fallback : α},
      (List.map Sigma.fst l).contains k = false → (↑(t.insertMany! l)).getKeyD k fallback = t.getKeyD k fallback
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.inr_v_fst_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (p q : ℤ) (hpq : p + 1 = q),
  CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCocone.inr φ)).v p q hpq)
      ((CochainComplex.mappingCocone.fst φ).f q) =
    0
-- Mathlib.Data.Fintype.Quotient
Trunc.finChoiceEquiv_symm_apply : ∀ {ι : Type u_1} [inst : DecidableEq ι] [inst_1 : Fintype ι] {α : ι → Sort u_2} (q : Trunc ((i : ι) → α i)) (i : ι),
  Trunc.finChoiceEquiv.symm q i = Trunc.map (fun x => x i) q
-- Mathlib.LinearAlgebra.Prod
LinearMap.sup_range_inl_inr : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], (LinearMap.inl R M M₂).range ⊔ (LinearMap.inr R M M₂).range = ⊤
-- Mathlib.RingTheory.SimpleModule.Isotypic
IsIsotypic.of_injective : ∀ {R : Type u_2} {M : Type u} {N : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N],
  IsIsotypic R N → ∀ (f : M →ₗ[R] N), Function.Injective ⇑f → IsIsotypic R M
-- Std.Time.Date.Basic
/-- Convert `Millisecond.Offset` into `Day.Offset`.
 -/
Std.Time.Millisecond.Offset.toDays : Std.Time.Millisecond.Offset → Std.Time.Day.Offset
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.homologySequence_exact₂ : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A)
  [inst_3 : CategoryTheory.Limits.HasZeroObject C] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  [inst_7 : CategoryTheory.Abelian A] [inst_8 : F.IsHomological] [inst_9 : F.ShiftSequence ℤ]
  (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (n₀ : ℤ),
  { X₁ := (F.shift n₀).obj T.obj₁, X₂ := (F.shift n₀).obj T.obj₂, X₃ := (F.shift n₀).obj T.obj₃,
      f := (F.shift n₀).map T.mor₁, g := (F.shift n₀).map T.mor₂, zero := ⋯ }.Exact
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.coe_lt_coe : ∀ {E : Type u_3} [inst : AddGroup E] {p q : AddGroupSeminorm E}, ⇑p < ⇑q ↔ p < q
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_two_eq : ∀ (x : ℤ), x.bmod 2 = -1 ∨ x.bmod 2 = 0
-- Mathlib.Analysis.Complex.Trigonometric
Real.tan_zero : Real.tan 0 = 0
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.imageSubobjectMap.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X}
  [inst_1 : CategoryTheory.Limits.HasImage f] {g : Y ⟶ Z} [inst_2 : CategoryTheory.Limits.HasImage g]
  (sq sq_1 : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) (e_sq : sq = sq_1)
  [inst_3 : CategoryTheory.Limits.HasImageMap sq],
  CategoryTheory.Limits.imageSubobjectMap sq = CategoryTheory.Limits.imageSubobjectMap sq_1
-- Mathlib.Data.Matrix.Basic
/-- `Matrix.diagonal` as an `AlgHom`.  -/
Matrix.diagonalAlgHom : {n : Type u_3} →
  (R : Type u_7) →
    {α : Type u_11} →
      [inst : Fintype n] →
        [inst_1 : DecidableEq n] →
          [inst_2 : CommSemiring R] → [inst_3 : Semiring α] → [inst_4 : Algebra R α] → (n → α) →ₐ[R] Matrix n n α
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsCofiltered.cofilteredClosure.eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] {α : Type w}
  {f : α → C} {j j' : C},
  CategoryTheory.IsCofiltered.cofilteredClosure f j →
    CategoryTheory.IsCofiltered.cofilteredClosure f j' →
      ∀ (f_1 f' : j ⟶ j'), CategoryTheory.IsCofiltered.cofilteredClosure f (CategoryTheory.IsCofiltered.eq f_1 f')
-- Mathlib.Logic.Function.Defs
Function.prod_comp : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} (f : ι → α) (g : ι → β) {κ : Sort u_4} (h : κ → ι),
  Function.prod f g ∘ h = Function.prod (f ∘ h) (g ∘ h)
-- Mathlib.Tactic.Push
/-- `pushNegBuiltin` is a simproc for pushing `¬` in a way that can't be done
using the `@[push]` attribute.
- `¬ (p ∧ q)` turns into `p → ¬ q` or `¬ p ∨ ¬ q`, depending on the `distrib` configuration.
- `¬ ∀ a, p` turns into `∃ a, ¬ p`, where the binder name `a` is preserved.
 -/
_private.Mathlib.Tactic.Push.0.Mathlib.Tactic.Push.pushNegBuiltin : Mathlib.Tactic.Push.Config → Lean.Meta.Simp.Simproc
-- Mathlib.Data.ZMod.QuotientRing
Int.quotientSpanEquivZMod_comp_castRingHom : ∀ (n : ℤ), (↑n.quotientSpanEquivZMod.symm).comp (Int.castRingHom (ZMod n.natAbs)) = Ideal.Quotient.mk (Ideal.span {n})
-- Mathlib.MeasureTheory.Integral.Bochner.Set
/-- If a function vanishes almost everywhere on `sᶜ`, then its integral on `s`
coincides with its integral on the whole space.  -/
MeasureTheory.setIntegral_eq_integral_of_ae_compl_eq_zero : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s : Set X} {μ : MeasureTheory.Measure X},
  (∀ᵐ (x : X) ∂μ, x ∉ s → f x = 0) → ∫ (x : X) in s, f x ∂μ = ∫ (x : X), f x ∂μ
-- Mathlib.FieldTheory.Separable
Polynomial.Separable.unit_mul : ∀ {R : Type u} [inst : CommSemiring R] {f g : Polynomial R}, IsUnit f → g.Separable → (f * g).Separable
-- Mathlib.CategoryTheory.Sites.Whiskering
CategoryTheory.GrothendieckTopology.Cover.multicospanComp_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {B : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} B] {J : CategoryTheory.GrothendieckTopology C}
  (F : CategoryTheory.Functor A B) (P : CategoryTheory.Functor Cᵒᵖ A) {X : C} (S : J.Cover X)
  (X_1 : CategoryTheory.Limits.WalkingMulticospan S.shape),
  (CategoryTheory.GrothendieckTopology.Cover.multicospanComp F P S).inv.app X_1 =
    (match X_1 with
      | CategoryTheory.Limits.WalkingMulticospan.left a => CategoryTheory.Iso.refl (F.obj (P.obj (Opposite.op a.Y)))
      | CategoryTheory.Limits.WalkingMulticospan.right a =>
        CategoryTheory.Iso.refl (F.obj (P.obj (Opposite.op a.r.Z)))).inv
-- Mathlib.Algebra.Category.Ring.Colimits
/-- The function from the colimit ring to the cone point of any other cocone.  -/
RingCat.Colimits.descFun : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J RingCat) →
      (s : CategoryTheory.Limits.Cocone F) → RingCat.Colimits.ColimitType F → ↑s.pt
-- Mathlib.FieldTheory.Minpoly.MinpolyDiv
sum_smul_minpolyDiv_eq_X_pow : ∀ {K : Type u_2} {L : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (E : Type u_1)
  [inst_3 : Field E] [inst_4 : Algebra K E] [IsAlgClosed E] [inst_6 : FiniteDimensional K L] [Algebra.IsSeparable K L]
  {x : L},
  K[x] = ⊤ →
    ∀ {r : ℕ},
      r < Module.finrank K L →
        ∑ σ,
            Polynomial.map (↑σ)
              ((x ^ r / (Polynomial.aeval x) (Polynomial.derivative (minpoly K x))) • minpolyDiv K x) =
          Polynomial.X ^ r
-- Mathlib.Data.Seq.Computation
Computation.not_terminates_empty : ∀ {α : Type u}, ¬(Computation.empty α).Terminates
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pos.revSkip?_eq_map_skipSuffix? : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String.Slice} {pos : s.Pos},
  pos.revSkip? pat = Option.map String.Slice.Pos.ofSliceTo ((s.sliceTo pos).skipSuffix? pat)
-- Std.Time.Time.Unit.Hour
/-- Creates an `Ordinal` from an integer, ensuring the value is within bounds.
 -/
Std.Time.Hour.Ordinal.ofInt : (data : ℤ) → 0 ≤ data ∧ data ≤ 23 → Std.Time.Hour.Ordinal
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.instPrespectralSpaceCarrierCarrierCommRingCat : ∀ {X : AlgebraicGeometry.Scheme}, PrespectralSpace ↥X
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.instSetLike : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : Module R A] → [inst_3 : Star A] → SetLike (NonUnitalStarSubalgebra R A) A
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionAssocIso : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction Cᵒᵖ Dᵒᵖ] (x : D) (x_1 x_2 : C),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso x x_1 x_2 =
    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso (Opposite.op x) (Opposite.op x_1)
          (Opposite.op x_2)).symm.unop
-- Mathlib.Algebra.Group.MinimalAxioms
/-- Define a `Group` structure on a Type by proving `∀ a, a * 1 = a` and
`∀ a, a * a⁻¹ = 1`.
Note that this uses the default definitions for `npow`, `zpow` and `div`.
See note [reducible non-instances].  -/
Group.ofRightAxioms : {G : Type u} →
  [inst : Mul G] →
    [inst_1 : Inv G] →
      [inst_2 : One G] →
        (∀ (a b c : G), a * b * c = a * (b * c)) → (∀ (a : G), a * 1 = a) → (∀ (a : G), a * a⁻¹ = 1) → Group G
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.rightHomologyι_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasRightHomology] [inst_3 : S₂.HasRightHomology] (φ : S₁ ⟶ S₂)
  {Z : C} (h : S₂.opcycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap φ)
      (CategoryTheory.CategoryStruct.comp S₂.rightHomologyι h) =
    CategoryTheory.CategoryStruct.comp S₁.rightHomologyι
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap φ) h)
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.outerMeasure_lt_top_of_isCompact : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] [WeaklyLocallyCompactSpace G]
  {K : Set G}, IsCompact K → μ.outerMeasure K < ⊤
-- Init.Data.Nat.Coprime
Nat.coprime_one_right_eq_true : ∀ (n : ℕ), n.Coprime 1 = True
-- Mathlib.Order.CompleteBooleanAlgebra
/-- Pullback an `Order.Coframe` along an injection.  -/
Function.Injective.coframe : {α : Type u} →
  {β : Type v} →
    [inst : Max α] →
      [inst_1 : Min α] →
        [inst_2 : LE α] →
          [inst_3 : LT α] →
            [inst_4 : SupSet α] →
              [inst_5 : InfSet α] →
                [inst_6 : Top α] →
                  [inst_7 : Bot α] →
                    [inst_8 : HNot α] →
                      [inst_9 : SDiff α] →
                        [inst_10 : Order.Coframe β] →
                          (f : α → β) →
                            Function.Injective f →
                              (∀ {x y : α}, f x ≤ f y ↔ x ≤ y) →
                                (∀ {x y : α}, f x < f y ↔ x < y) →
                                  (∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) →
                                    (∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) →
                                      (∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) →
                                        (∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) →
                                          f ⊤ = ⊤ →
                                            f ⊥ = ⊥ →
                                              (∀ (a : α), f (￢a) = ￢f a) →
                                                (∀ (a b : α), f (a \ b) = f a \ f b) → Order.Coframe α
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKeyD_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β k}
  {fallback : α}, (t.insert k v).minKeyD fallback = t.minKey?.elim k fun k' => if (cmp k k').isLE = true then k else k'
-- Mathlib.CategoryTheory.Adjunction.Lifting.Left
CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv_symm_apply : ∀ {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]
  {U : CategoryTheory.Functor B C} {F : CategoryTheory.Functor C B} (R : CategoryTheory.Functor A B)
  (F' : CategoryTheory.Functor C A) (adj₁ : F ⊣ U) (adj₂ : F' ⊣ R.comp U)
  [inst_3 : CategoryTheory.Limits.HasReflexiveCoequalizers A]
  (h : (X : B) → CategoryTheory.RegularEpi (adj₁.counit.app X)) (Y : A) (X : B) (a : X ⟶ R.obj Y),
  (CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv R F' adj₁ adj₂ h Y X).symm a =
    (CategoryTheory.Limits.Cofork.IsColimit.homIso
          (CategoryTheory.Limits.colimit.isColimit
            (CategoryTheory.Limits.parallelPair (F'.map (U.map (adj₁.counit.app X)))
              (CategoryTheory.LiftLeftAdjoint.otherMap R F' adj₁ adj₂ X)))
          Y).symm
      ⟨(adj₂.homEquiv (U.obj X) Y).symm
          ((adj₁.homEquiv (U.obj X) (R.obj Y))
            ↑((CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.LiftLeftAdjoint.counitCoequalises adj₁ h X)
                  (R.obj Y))
                a)),
        ⋯⟩
-- Init.Data.UInt.Lemmas
instLawfulCommIdentityUInt16HMulOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 * x2) 1
-- Init.PropLemmas
eq_mpr_eq_cast : ∀ {α β : Sort u_1} (h : α = β), h.mpr = cast ⋯
-- Mathlib.Combinatorics.Additive.FreimanHom
isMulFreimanIso_one_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {A : Set α} {B : Set β} {f : α → β},
  IsMulFreimanIso 1 A B f ↔ Set.BijOn f A B
-- Lean.Server.Requests
Lean.Server.RequestContext.mk.sizeOf_spec : ∀ (rpcSessions : Std.TreeMap UInt64 (IO.Ref Lean.Server.FileWorker.RpcSession) compare)
  (doc : Lean.Server.FileWorker.EditableDocument) (hLog : IO.FS.Stream) (initParams : Lean.Lsp.InitializeParams)
  (cancelTk : Lean.Server.RequestCancellationToken) (serverRequestEmitter : Lean.Server.ServerRequestEmitter),
  sizeOf
      { rpcSessions := rpcSessions, doc := doc, hLog := hLog, initParams := initParams, cancelTk := cancelTk,
        serverRequestEmitter := serverRequestEmitter } =
    1 + sizeOf rpcSessions + sizeOf doc + sizeOf hLog + sizeOf initParams + sizeOf cancelTk
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.denote.eq_1 : ∀ (ctx : Int.Internal.Linear.Context) (a b : Int.Internal.Linear.Expr),
  Int.Internal.Linear.Expr.denote ctx (a.add b) =
    Int.Internal.Linear.Expr.denote ctx a + Int.Internal.Linear.Expr.denote ctx b
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
CategoryTheory.Limits.PreservesLimitPair.iso_inv_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) (X Y : C) [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Y]
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct (G.obj X) (G.obj Y)]
  [inst_4 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X Y) G],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesLimitPair.iso G X Y).inv
      (G.map CategoryTheory.Limits.prod.fst) =
    CategoryTheory.Limits.prod.fst
-- Mathlib.Tactic.Linter.AuxLemma
/-- Returns `true` if `s` has the form `pfx ++ digits`, e.g. `"_proof_17"`.  -/
_private.Mathlib.Tactic.Linter.AuxLemma.0.Mathlib.Linter.AuxLemma.matchesAuxPattern : String → String → Bool
-- Mathlib.RingTheory.HahnSeries.Lex
/-- Finite archimedean classes of `Lex R⟦Γ⟧` decompose into lexicographical pairs
of `order` and the finite archimedean class of `leadingCoeff`.  -/
HahnSeries.finiteArchimedeanClassOrderHomLex : (Γ : Type u_1) →
  (R : Type u_2) →
    [inst : LinearOrder Γ] →
      [inst_1 : LinearOrder R] →
        [inst_2 : AddCommGroup R] →
          [inst_3 : IsOrderedAddMonoid R] →
            FiniteArchimedeanClass (Lex (HahnSeries Γ R)) →o Lex (Γ × FiniteArchimedeanClass R)
-- Mathlib.NumberTheory.MulChar.Duality
/-- The cardinality of the dual subgroup of `MulChar M R` associated to a subgroup `H` of `Mˣ`
equals the index of `H` in `Mˣ`.  -/
MulChar.card_subgroupOrderIsoSubgroupMulChar : ∀ {M : Type u_1} {R : Type u_2} [inst : CommMonoid M] [inst_1 : CommRing R] [inst_2 : Finite M]
  [inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)] {H : Subgroup Mˣ},
  Nat.card ↥(OrderDual.ofDual ((MulChar.subgroupOrderIsoSubgroupMulChar M R) H)) = Nat.card (Mˣ ⧸ H)
-- Mathlib.Data.Fintype.Sets
Fintype.coe_finsetOrderIsoSet : ∀ {α : Type u_1} [inst : Fintype α], ⇑Fintype.finsetOrderIsoSet = SetLike.coe
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Submodule.instFiniteDimensionalQuotientMapOfRange : ∀ {K : Type u} {V : Type v} {W : Type v'} [inst : DivisionRing K] [inst_1 : AddCommGroup W] [inst_2 : AddCommGroup V]
  [inst_3 : Module K V] [inst_4 : Module K W] {f : V →ₗ[K] W} (p : Submodule K V) [FiniteDimensional K (V ⧸ p)]
  [FiniteDimensional K (W ⧸ f.range)], FiniteDimensional K (W ⧸ Submodule.map f p)
-- Mathlib.Geometry.Euclidean.PerpBisector
AffineSubspace.perpBisector_ne_bot : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ : P}, AffineSubspace.perpBisector p₁ p₂ ≠ ⊥
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_lt_of_lt_one_left' : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : LT α] [MulRightStrictMono α] (a : α) {b : α}, b < 1 → b * a < a
-- Mathlib.Algebra.Category.AlgCat.TensorAlgebra
AlgCat.instIsRightAdjointModuleCatForget₂AlgHomCarrierLinearMapIdCarrierOfSmall : ∀ (R : Type v) [inst : CommRing R] [Small.{u, v} R], (CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)).IsRightAdjoint
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_union' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α},
  Disjoint s₁ s₂ → MeasurableSet s₁ → μ (s₁ ∪ s₂) = μ s₁ + μ s₂
-- Mathlib.Data.Nat.Multiplicity
Nat.Prime.emultiplicity_choose_prime_pow_add_emultiplicity : ∀ {p n k : ℕ}, Nat.Prime p → k ≤ p ^ n → k ≠ 0 → emultiplicity p ((p ^ n).choose k) + emultiplicity p k = ↑n
-- Mathlib.Tactic.NormNum.Result
/-- The result is `q : ℚ` and `proof : isRat x q`.  -/
Mathlib.Meta.NormNum.Result.isRat : {u : Lean.Level} →
  {α : Q(Type u)} →
    {x : Q(«$α»)} →
      (inst : autoParam Q(DivisionRing «$α») Mathlib.Meta.NormNum.Result.isRat._auto_1) →
        ℚ → (n : Q(ℤ)) → (d : Q(ℕ)) → Q(Mathlib.Meta.NormNum.IsRat «$x» «$n» «$d») → Mathlib.Meta.NormNum.Result x
-- Mathlib.RepresentationTheory.Coinvariants
Rep.instEpiModuleCatAppCoinvariantsMk : ∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Monoid G] (X : Rep.{u_1, u, v} k G),
  CategoryTheory.Epi ((Rep.coinvariantsMk k G).app X)
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type w}
  [inst_1 : CategoryTheory.Limits.HasFiniteCoproducts C] (F F_1 : CategoryTheory.Functor (CategoryTheory.Discrete α) C),
  F = F_1 →
    CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj F =
      CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj F_1
-- Init.Data.List.MapIdx
List.mapIdx_go_length : ∀ {β : Type u_1} {α : Type u_2} {f : ℕ → α → β} {l : List α} {acc : Array β},
  (List.mapIdx.go f l acc).length = l.length + acc.size
-- Mathlib.LinearAlgebra.AffineSpace.Combination
Finset.weightedVSubVSubWeights.eq_1 : ∀ (k : Type u_1) [inst : Ring k] {ι : Type u_4} [inst_1 : DecidableEq ι] (i j : ι),
  Finset.weightedVSubVSubWeights k i j = Pi.single i 1 - Pi.single j 1
-- Mathlib.Topology.Order.Lattice
Continuous.finset_inf'_apply : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] {ι : Type u_3}
  [inst_2 : SemilatticeInf L] [ContinuousInf L] {s : Finset ι} {f : ι → X → L} (hne : s.Nonempty),
  (∀ i ∈ s, Continuous (f i)) → Continuous fun a => s.inf' hne fun x => f x a
-- Mathlib.Algebra.Homology.Homotopy
/-- a variant of `Homotopy.compRight` useful for dealing with homotopy equivalences.  -/
Homotopy.compRightId : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} →
          {C D : HomologicalComplex V c} →
            {f : C ⟶ C} →
              Homotopy f (CategoryTheory.CategoryStruct.id C) →
                (g : C ⟶ D) → Homotopy (CategoryTheory.CategoryStruct.comp f g) g
-- Mathlib.Tactic.FunProp.Theorems
/-- function name  -/
Mathlib.Meta.FunProp.FunctionTheorem.funOrigin : Mathlib.Meta.FunProp.FunctionTheorem → Mathlib.Meta.FunProp.Origin
-- Mathlib.Algebra.Order.Group.Synonym
pow_ofLex : ∀ {α : Type u_1} {β : Type u_2} [inst : Pow α β] (a : α) (b : Lex β), a ^ ofLex b = a ^ b
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubMulAction.nat_card_ofStabilizer_eq : ∀ (G : Type u_1) [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α] (a : α),
  Nat.card ↥(SubMulAction.ofStabilizer G a) = Nat.card α - 1
-- Mathlib.Computability.Primrec.List
_private.Mathlib.Computability.Primrec.List.0.List.lookup.match_1.eq_2 : ∀ {α : Type u_2} {β : Type u_1} (motive : α → List (α × β) → Sort u_3) (a k : α) (b : β) (as : List (α × β))
  (h_1 : (x : α) → motive x []) (h_2 : (a k : α) → (b : β) → (as : List (α × β)) → motive a ((k, b) :: as)),
  (match a, (k, b) :: as with
    | x, [] => h_1 x
    | a, (k, b) :: as => h_2 a k b as) =
    h_2 a k b as
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instMul.eq_1 : ∀ {α : Type u_1} [inst : Mul α], Colex.instMul = inst