mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- The product comparison morphism from `F(A ⊗ -)` to `FA ⊗ F-`, whose components are given by
`prodComparison`.  -/
CategoryTheory.CartesianMonoidalCategory.prodComparisonNatTrans : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₁} →
        [inst_2 : CategoryTheory.Category.{v₁, u₁} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            (F : CategoryTheory.Functor C D) →
              (A : C) →
                ((CategoryTheory.MonoidalCategory.curriedTensor C).obj A).comp F ⟶
                  F.comp ((CategoryTheory.MonoidalCategory.curriedTensor D).obj (F.obj A))
-- Mathlib.Algebra.Group.Defs
AddCommGroup.toAddGroup : {G : Type u} → [self : AddCommGroup G] → AddGroup G
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.diag2_coe' : ∀ {F : Type u_1} [inst : Field F] {a : F} (ha : a ≠ 0), ↑(Matrix.SpecialLinearGroup.diag2 a ha) = !![a, 0; 0, a⁻¹]
-- Lean.Message
/-- `withContext ctx d` specifies the pretty printing context `(env, mctx, lctx, opts)` for the nested expressions in `d`.  -/
Lean.MessageData.withContext : Lean.MessageDataContext → Lean.MessageData → Lean.MessageData
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Mon.hom_one : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Mon C) [inst_3 : CategoryTheory.IsCommMonObj M.X],
  CategoryTheory.MonObj.one.hom = CategoryTheory.MonObj.one
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
FiberBundle.extChartAt_target : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E] (x : Bundle.TotalSpace F E),
  (extChartAt (IB.prod (modelWithCornersSelf 𝕜 F)) x).target =
    ((extChartAt IB x.proj).target ∩ ↑(extChartAt IB x.proj).symm ⁻¹' (trivializationAt F E x.proj).baseSet) ×ˢ Set.univ
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
_private.Mathlib.AlgebraicTopology.SimplexCategory.Basic.0.SimplexCategory.mkOfLe.match_1.splitter : (motive : Fin (1 + 1) → Sort u_1) → (x : Fin (1 + 1)) → (Unit → motive 0) → (Unit → motive 1) → motive x
-- Lean.Data.Lsp.Extra
Lean.Lsp.WaitForILeans : Type
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_eq_some_iff : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {k k' : α}, m.getKey? k = some k' ↔ ∃ (h : m.contains k = true), m.getKey k h = k'
-- Mathlib.Topology.Constructions.SumProd
Filter.Eventually.prodMk_nhds : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {px : X → Prop} {x : X},
  (∀ᶠ (x : X) in nhds x, px x) →
    ∀ {py : Y → Prop} {y : Y}, (∀ᶠ (y : Y) in nhds y, py y) → ∀ᶠ (p : X × Y) in nhds (x, y), px p.1 ∧ py p.2
-- Mathlib.Algebra.Homology.Bifunctor
HomologicalComplex.mapBifunctor.hom_ext_iff : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] {K₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂}
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)} [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] {c : ComplexShape J} [inst_8 : TotalComplexShape c₁ c₂ c]
  [inst_9 : K₁.HasMapBifunctor K₂ F c] [inst_10 : DecidableEq J] {Y : D} {j : J}
  {f g : (K₁.mapBifunctor K₂ F c).X j ⟶ Y},
  f = g ↔
    ∀ (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c (i₁, i₂) = j),
      CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h) f =
        CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h) g
-- Mathlib.Data.Vector3
Vector3.eq_nil : ∀ {α : Type u_1} (v : Vector3 α 0), v = []
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
LieRinehartRing.lie_smul_eq_mul' : ∀ {A : Type u_1} {L : Type u_2} {inst : CommRing A} {inst_1 : LieRing L} {inst_2 : Module A L}
  {inst_3 : LieRingModule L A} [self : LieRinehartRing A L] (a b : A) (x : L), ⁅a • x, b⁆ = a * ⁅x, b⁆
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
/-- A measurable function `α → StieltjesFunction ℝ` with limits 0 at -∞ and 1 at +∞ gives a
measurable function `α → Measure ℝ` by taking `StieltjesFunction.measure` at each point.  -/
StieltjesFunction.measurable_measure : ∀ {α : Type u_1} {x : MeasurableSpace α} {f : α → StieltjesFunction ℝ},
  (∀ (q : ℝ), Measurable fun a => ↑(f a) q) →
    (∀ (a : α), Filter.Tendsto (↑(f a)) Filter.atBot (nhds 0)) →
      (∀ (a : α), Filter.Tendsto (↑(f a)) Filter.atTop (nhds 1)) → Measurable fun a => (f a).measure
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.gluedCover_V : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.I₀ × 𝒰.I₀),
  (AlgebraicGeometry.Scheme.Cover.gluedCover 𝒰).V x =
    match x with
    | (x, y) => CategoryTheory.Limits.pullback (𝒰.f x) (𝒰.f y)
-- Mathlib.GroupTheory.Coset.Basic
mem_leftCoset_leftCoset : ∀ {α : Type u_1} [inst : Monoid α] (s : Submonoid α) {a : α}, a • ↑s = ↑s → a ∈ s
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k k' : α} {f : Option (β k) → Option (β k)},
  (t.alter k f).contains k' = if cmp k k' = Ordering.eq then (f (t.get? k)).isSome else t.contains k'
-- Mathlib.Analysis.MeanInequalities
Real.geom_mean_le_arith_mean4_weighted : ∀ {w₁ w₂ w₃ w₄ p₁ p₂ p₃ p₄ : ℝ},
  0 ≤ w₁ →
    0 ≤ w₂ →
      0 ≤ w₃ →
        0 ≤ w₄ →
          0 ≤ p₁ →
            0 ≤ p₂ →
              0 ≤ p₃ →
                0 ≤ p₄ →
                  w₁ + w₂ + w₃ + w₄ = 1 → p₁ ^ w₁ * p₂ ^ w₂ * p₃ ^ w₃ * p₄ ^ w₄ ≤ w₁ * p₁ + w₂ * p₂ + w₃ * p₃ + w₄ * p₄
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
/-- The sets `primitiveRoots k R` are pairwise disjoint.  -/
IsPrimitiveRoot.disjoint : ∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R] {k l : ℕ},
  k ≠ l → Disjoint (primitiveRoots k R) (primitiveRoots l R)
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.comap_iInf : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] {ι : Sort u_1} (f : R →+* S)
  (s : ι → Subring S), Subring.comap f (iInf s) = ⨅ i, Subring.comap f (s i)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.instEpiModuleCatH2π : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.Epi (groupCohomology.H2π A)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.bounded_iteratedFDeriv : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} (f : ContDiffMapSupportedIn E F n K) {i : ℕ},
  ↑i ≤ n → ∃ C, ∀ (x : E), ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C
-- Mathlib.RingTheory.Localization.Away.Basic
selfZPow_mul_neg : ∀ {R : Type u_1} [inst : CommSemiring R] (x : R) (B : Type u_2) [inst_1 : CommSemiring B] [inst_2 : Algebra R B]
  [inst_3 : IsLocalization.Away x B] (d : ℤ), selfZPow x B d * selfZPow x B (-d) = 1
-- Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
CochainComplex.mappingConeCompTriangle_mor₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃),
  (CochainComplex.mappingConeCompTriangle f g).mor₁ =
    CochainComplex.mappingCone.map f (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id X₁) g ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
CategoryTheory.Limits.CoproductDisjoint.isPullback_of_isInitial : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : ι → C}
  [CategoryTheory.Limits.CoproductDisjoint X] {c : CategoryTheory.Limits.Cofan X}
  (hc : CategoryTheory.Limits.IsColimit c) {Y : C} (hY : CategoryTheory.Limits.IsInitial Y) {i j : ι}
  [CategoryTheory.Limits.HasPullback (c.inj i) (c.inj j)],
  i ≠ j → CategoryTheory.IsPullback (hY.to (X i)) (hY.to (X j)) (c.inj i) (c.inj j)
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.lift_le_beth_natCast : ∀ {c : Cardinal.{u}} {n : ℕ}, Cardinal.lift.{v, u} c ≤ Cardinal.beth ↑n ↔ c ≤ Cardinal.beth ↑n
-- Mathlib.Data.Sum.Basic
Sum.map_bijective : ∀ {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {f : α → γ} {g : β → δ},
  Function.Bijective (Sum.map f g) ↔ Function.Bijective f ∧ Function.Bijective g
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.toArray_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {f : α → β → γ},
  (Std.TreeMap.map f t).toArray = Array.map (fun p => (p.1, f p.1 p.2)) t.toArray
-- Mathlib.Order.Height
Set.chainHeight_eq_top_iff : ∀ {α : Type u_1} (s : Set α) (r : α → α → Prop), s.chainHeight r = ⊤ ↔ ∀ (n : ℕ), ∃ t ⊆ s, t.encard = ↑n ∧ IsChain r t
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.option.inj : ∀ {stx stx_1 : Lean.Syntax}, Lean.Elab.CompletionInfo.option stx = Lean.Elab.CompletionInfo.option stx_1 → stx = stx_1
-- Init.Data.Array.GetLit
Array.toListLitAux.eq_2 : ∀ {α : Type u_1} (xs : Array α) (n : ℕ) (hsz : xs.size = n) (x : List α) (i : ℕ) (hi : i + 1 ≤ xs.size),
  xs.toListLitAux n hsz i.succ hi x = xs.toListLitAux n hsz i ⋯ (xs.getLit i hsz ⋯ :: x)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
/-- the condition that the denominator belongs to the given morphism property  -/
CategoryTheory.MorphismProperty.LeftFraction₃.hs : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (self : W.LeftFraction₃ X Y), W self.s
-- Lean.Util.Recognizers
/-- Checks if an expression is a `Name` literal, and if so returns the name.
 -/
Lean.Expr.name? : Lean.Expr → Option Lean.Name
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Measurable.coe_real_ereal : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → ℝ}, Measurable f → Measurable fun x => ↑(f x)
-- Mathlib.Algebra.Star.SelfAdjoint
IsStarNormal.one_sub : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : StarRing R] {a : R} [ha : IsStarNormal a], IsStarNormal (1 - a)
-- Mathlib.Computability.NFA
NFA.evalFrom_append : ∀ {α : Type u} {σ : Type v} (M : NFA α σ) (S : Set σ) (x y : List α),
  M.evalFrom S (x ++ y) = M.evalFrom (M.evalFrom S x) y
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtendTarget.mk.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {outWidth w : ℕ} (x x_1 : aig.RefVec w),
  x = x_1 → ∀ (h : outWidth = w * w), { w := w, x := x, h := h } = { w := w, x := x_1, h := h }
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.not_mem_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → k ∉ t₁ \ t₂
-- Mathlib.GroupTheory.Coprod.Basic
/-- The natural projection `M ∗ N →* M`.  -/
Monoid.Coprod.fst : {M : Type u_1} → {N : Type u_2} → [inst : Monoid M] → [inst_1 : Monoid N] → Monoid.Coprod M N →* M
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_add_eq_nnnorm_right : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] {x : E} (y : E), ‖x‖₊ = 0 → ‖x + y‖₊ = ‖y‖₊
-- Batteries.Data.AssocList
Batteries.AssocList.findEntryP?.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (p : α → β → Bool), Batteries.AssocList.findEntryP? p Batteries.AssocList.nil = none
-- Mathlib.Algebra.Order.Interval.Basic
instOneNonemptyInterval : {α : Type u_2} → [inst : Preorder α] → [One α] → One (NonemptyInterval α)
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.integral_comp_mul_right_Ioi : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (g : ℝ → E) (a : ℝ) {b : ℝ},
  0 < b → ∫ (x : ℝ) in Set.Ioi a, g (x * b) = b⁻¹ • ∫ (x : ℝ) in Set.Ioi (a * b), g x
-- Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Units.chartAt_source : ∀ {R : Type u_1} [inst : NormedRing R] [inst_1 : CompleteSpace R] {a : Rˣ}, (chartAt R a).source = Set.univ
-- Mathlib.LinearAlgebra.Dual.Basis
/-- `(h : DualBases e ε).basis` shows the family of vectors `e` forms a basis.  -/
Module.DualBases.basis : {R : Type u_1} →
  {M : Type u_2} →
    {ι : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] → {e : ι → M} → {ε : ι → Module.Dual R M} → Module.DualBases e ε → Module.Basis ι R M
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.coe_comp : ∀ {X Y Z : ProfiniteGrp.{u_1}} (f : X ⟶ Y) (g : Y ⟶ Z),
  ⇑(ProfiniteGrp.Hom.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(ProfiniteGrp.Hom.hom g) ∘ ⇑(ProfiniteGrp.Hom.hom f)
-- Init.Data.Option.Attach
Option.toArray_pmap : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {o : Option α} {f : (a : α) → p a → β} (h : ∀ (a : α), o = some a → p a),
  (Option.pmap f o h).toArray = Array.map (fun x => f ↑x ⋯) o.attach.toArray
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- A commuting square of isomorphisms induces an isomorphism of cokernels.  -/
CategoryTheory.Limits.cokernel.mapIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Limits.HasCokernel f] →
            {X' Y' : C} →
              (f' : X' ⟶ Y') →
                [inst_3 : CategoryTheory.Limits.HasCokernel f'] →
                  (p : X ≅ X') →
                    (q : Y ≅ Y') →
                      CategoryTheory.CategoryStruct.comp f q.hom = CategoryTheory.CategoryStruct.comp p.hom f' →
                        (CategoryTheory.Limits.cokernel f ≅ CategoryTheory.Limits.cokernel f')
-- Mathlib.Data.Finite.Vector
instFiniteSym : ∀ {α : Type u_1} [Finite α] {n : ℕ}, Finite (Sym α n)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.extendScalars_self : ∀ {K : Type u_1} [inst : Field K] {L : Type u_2} [inst_1 : Field L] [inst_2 : Algebra K L] (F : IntermediateField K L),
  IntermediateField.extendScalars ⋯ = ⊥
-- Init.Core
/-- Auxiliary definition for generating compact `noConfusion` for enumeration types  -/
noConfusionTypeEnum : {α : Sort u} → {β : Sort v} → [inst : DecidableEq β] → (α → β) → Sort w → α → α → Sort w
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.SimpCacheKey.mk.injEq : ∀ (variant : Lean.Name) (extras : Array Lean.Elab.Tactic.Grind.ExtraTheorem) (variant_1 : Lean.Name)
  (extras_1 : Array Lean.Elab.Tactic.Grind.ExtraTheorem),
  ({ variant := variant, extras := extras } = { variant := variant_1, extras := extras_1 }) =
    (variant = variant_1 ∧ extras = extras_1)
-- Mathlib.AlgebraicGeometry.Fiber
AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberι_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↥X) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.asFiberHom f x)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.fiberι f (f x)) h) =
    CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField x) h
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.leanSorryLike : Lean.Lsp.SemanticTokenType
-- Mathlib.CategoryTheory.Limits.Cones
/-- Extending a cocone by a composition is the same as extending the cone twice.  -/
CategoryTheory.Limits.Cocone.extendComp : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (s : CategoryTheory.Limits.Cocone F) →
            {X Y : C} →
              (g : s.pt ⟶ Y) → (f : Y ⟶ X) → s.extend (CategoryTheory.CategoryStruct.comp g f) ≅ (s.extend g).extend f
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.mem_iff_isSome_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, a ∈ t ↔ (Std.DTreeMap.Raw.Const.get? t a).isSome = true
-- Mathlib.GroupTheory.Congruence.Defs
/-- Two elements are related by an additive congruence relation `c` iff
they are represented by the same element of the quotient by `c`.  -/
AddCon.eq : ∀ {M : Type u_1} [inst : Add M] (c : AddCon M) {a b : M}, ↑a = ↑b ↔ c a b
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.insertListIfNew.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l : List ((a : α) × β a)) (k : α) (v : β k)
  (l_1 : List ((a : α) × β a)),
  Std.Internal.List.insertListIfNew l (⟨k, v⟩ :: l_1) =
    Std.Internal.List.insertListIfNew (Std.Internal.List.insertEntryIfNew k v l) l_1
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.isoHomologyι_hom_inv_id_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) (hj : c.next i = j) (h : K.d i j = 0)
  [inst_2 : K.HasHomology i] {Z : C} (h_1 : K.homology i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.homologyι i)
      (CategoryTheory.CategoryStruct.comp (K.isoHomologyι i j hj h).inv h_1) =
    h_1
-- Mathlib.RingTheory.Localization.Away.Basic
Units.liftRight.congr_simp : ∀ {M : Type u} {N : Type v} [inst : Monoid M] [inst_1 : Monoid N] (f f_1 : M →* N) (e_f : f = f_1) (g g_1 : M → Nˣ)
  (e_g : g = g_1) (h : ∀ (x : M), ↑(g x) = f x), Units.liftRight f g h = Units.liftRight f_1 g_1 ⋯
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.mem_orbit_symm : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {a₁ a₂ : α},
  a₁ ∈ AddAction.orbit G a₂ ↔ a₂ ∈ AddAction.orbit G a₁
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.keysArray_filter_key : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {f : α → Bool} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter (fun k x => f k) t ⋯).impl.keysArray = Array.filter f t.keysArray
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
/-- Reformulation of `ZetaAsymptotics.termTSum_of_lt` which is useful for some computations
below.  -/
ZetaAsymptotics.zeta_limit_aux1 : ∀ {s : ℝ}, 1 < s → ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1) = 1 - s * ZetaAsymptotics.termTSum s
-- Mathlib.Analysis.Convex.Basic
coe_convexAddSubmonoid : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E], ↑(convexAddSubmonoid 𝕜 E) = {s | Convex 𝕜 s}
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.cmpEq_iff : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x y : α} [Std.TransCmp cmp],
  RBTree.RBNode.cmpEq cmp x y ↔ cmp x y = Ordering.eq
-- Init.Data.List.Nat.Basic
List.max?_eq_some_iff' : ∀ {a : ℕ} {xs : List ℕ}, xs.max? = some a ↔ a ∈ xs ∧ ∀ b ∈ xs, b ≤ a
-- Std.Async.UDP
/-- Binds the UDP socket to the given address. Address reuse is enabled to allow rebinding the
same address.
 -/
Std.Async.UDP.Socket.bind : Std.Async.UDP.Socket → Std.Net.SocketAddress → IO Unit
-- Mathlib.Data.Int.Log
Int.clog_zero_left : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] (r : R), Int.clog 0 r = 0
-- Mathlib.CategoryTheory.Limits.Indization.Category
CategoryTheory.instCreatesFiniteLimitsIndFunctorOppositeTypeInclusionOfHasFiniteLimits : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasFiniteLimits C] →
      CategoryTheory.Limits.CreatesFiniteLimits (CategoryTheory.Ind.inclusion C)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get?_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, (t₁ \ t₂).get? k = if k ∈ t₂ then none else t₁.get? k
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.finitary_iff_forall_isCircuit_finite : ∀ {α : Type u_1} {M : Matroid α}, M.Finitary ↔ ∀ (C : Set α), M.IsCircuit C → C.Finite
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicoequalizer.condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) [inst_1 : CategoryTheory.Limits.HasMulticoequalizer I] (a : J.L),
  CategoryTheory.CategoryStruct.comp (I.fst a) (CategoryTheory.Limits.Multicoequalizer.π I (J.fst a)) =
    CategoryTheory.CategoryStruct.comp (I.snd a) (CategoryTheory.Limits.Multicoequalizer.π I (J.snd a))
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.reindex_trans : ∀ {ι : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7}
  [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] (e : ι ≃ ι₂) (e' : ι₂ ≃ ι₃),
  PiTensorProduct.reindex R s e ≪≫ₗ PiTensorProduct.reindex R (fun i => s (e.symm i)) e' =
    PiTensorProduct.reindex R s (e.trans e')
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.mul_two : ∀ (o : Ordinal.{u_4}), o * 2 = o + o
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.Gal.instUniqueOfFactSplits : {F : Type u_1} → [inst : Field F] → (p : Polynomial F) → [h : Fact p.Splits] → Unique p.Gal
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.loopyOn_isBasis_iff : ∀ {α : Type u_1} {E I X : Set α}, (Matroid.loopyOn E).IsBasis I X ↔ I = ∅ ∧ X ⊆ E
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.zero_subset : ∀ {α : Type u_2} [inst : Zero α] {s : Set α}, 0 ⊆ s ↔ 0 ∈ s
-- Lean.Server.FileWorker.RequestHandling
Lean.Server.FileWorker.NamespaceEntry.selection : Lean.Server.FileWorker.NamespaceEntry → Lean.Syntax
-- Mathlib.Topology.Algebra.Group.Matrix
Topology.IsEmbedding.specialLinearGroup_map : ∀ {n : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  [inst_3 : TopologicalSpace R] [inst_4 : CommRing S] [inst_5 : TopologicalSpace S] {f : R →+* S},
  Topology.IsEmbedding ⇑f → Topology.IsEmbedding ⇑(Matrix.SpecialLinearGroup.map f)
-- Mathlib.NumberTheory.LSeries.ZMod
/-- First form of functional equation for completed L-functions (even case).

Private because it is superseded by `completedLFunction_one_sub_even` below, which is valid for a
much wider range of `s`.
 -/
_private.Mathlib.NumberTheory.LSeries.ZMod.0.ZMod.completedLFunction_one_sub_of_one_lt_even : ∀ {N : ℕ} [inst : NeZero N] {Φ : ZMod N → ℂ},
  Function.Even Φ →
    ∀ {s : ℂ}, 1 < s.re → ZMod.completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * ZMod.completedLFunction (ZMod.dft Φ) s
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHom.toPseudoEpimorphism : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : Preorder α] →
        [inst_2 : TopologicalSpace β] → [inst_3 : Preorder β] → EsakiaHom α β → PseudoEpimorphism α β