mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The L-series of the twist of `f` by a Dirichlet character converges at `s` if the L-series
of `f` does.  -/
DirichletCharacter.LSeriesSummable_mul : ∀ {N : ℕ} (χ : DirichletCharacter ℂ N) {f : ℕ → ℂ} {s : ℂ},
  LSeriesSummable f s → LSeriesSummable ((fun n => χ ↑n) * f) s
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.localTriv_symm_apply : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) (i : ι)
  {b : B}, b ∈ (Z.localTriv i).baseSet → ∀ (v : F), (Z.localTriv i).symm b v = (Z.coordChange i (Z.indexAt b) b) v
-- Lean.Environment
Lean.Kernel.Exception.interrupted : Lean.Kernel.Exception
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.instSetLike : {α : Type u_1} → [inst : TopologicalSpace α] → SetLike (TopologicalSpace.CompactOpens α) α
-- Aesop.Search.Expansion
_private.Aesop.Search.Expansion.0.Aesop.expandGoal.fmtUnsafe : {Q : Type} → [inst : Aesop.Queue Q] → Except Lean.Exception Aesop.RuleResult → Aesop.SearchM Q Lean.MessageData
-- Mathlib.Algebra.GroupWithZero.Units.Lemmas
map_ne_zero : ∀ {G₀ : Type u_3} {M₀' : Type u_4} {F : Type u_6} [inst : GroupWithZero G₀] [inst_1 : MulZeroOneClass M₀']
  [Nontrivial M₀'] [inst_3 : FunLike F G₀ M₀'] [MonoidWithZeroHomClass F G₀ M₀'] (f : F) {a : G₀}, f a ≠ 0 ↔ a ≠ 0
-- Mathlib.Order.Partition.Finpartition
Finpartition.copy_parts : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {a b : α} (P : Finpartition a) (h : a = b),
  (P.copy h).parts = P.parts
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
/-- The indexed infimum of a function is bounded above by the value taken at one point  -/
ciInf_le : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {f : ι → α},
  BddBelow (Set.range f) → ∀ (c : ι), iInf f ≤ f c
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.isCompl_orthogonal_iff_disjoint : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [FiniteDimensional K V]
  {B : LinearMap.BilinForm K V} {W : Submodule K V},
  B.IsRefl → (IsCompl W (B.orthogonal W) ↔ Disjoint W (B.orthogonal W))
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.mk.injEq : ∀ {M : Type u_9} {N : Type u_10} [inst : Mul M] [inst_1 : Mul N] (toEquiv : M ≃ N)
  (map_mul' : ∀ (x y : M), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y) (toEquiv_1 : M ≃ N)
  (map_mul'_1 : ∀ (x y : M), toEquiv_1.toFun (x * y) = toEquiv_1.toFun x * toEquiv_1.toFun y),
  ({ toEquiv := toEquiv, map_mul' := map_mul' } = { toEquiv := toEquiv_1, map_mul' := map_mul'_1 }) =
    (toEquiv = toEquiv_1)
-- Init.Grind.AC
Lean.Grind.AC.Seq.cons.inj : ∀ {x : Lean.Grind.AC.Var} {s : Lean.Grind.AC.Seq} {x_1 : Lean.Grind.AC.Var} {s_1 : Lean.Grind.AC.Seq},
  Lean.Grind.AC.Seq.cons x s = Lean.Grind.AC.Seq.cons x_1 s_1 → x = x_1 ∧ s = s_1
-- Mathlib.RingTheory.PowerSeries.Expand
/-- Expand the power series by a factor of p, so `∑ aₙ xⁿ` becomes `∑ aₙ xⁿᵖ`.

See also `PowerSeries.expand`.  -/
PowerSeries.expand : {R : Type u_2} → [inst : CommRing R] → (p : ℕ) → p ≠ 0 → PowerSeries R →ₐ[R] PowerSeries R
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.hasRightResolutions_iff_op : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂),
  Φ.HasRightResolutions ↔ Φ.op.HasLeftResolutions
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.ext_iff : ∀ {Γ : Type u_1} {R : Type u_2} {inst : PartialOrder Γ} {inst_1 : Zero R} {x y : HahnSeries Γ R},
  x = y ↔ x.coeff = y.coeff
-- Mathlib.Order.RelIso.Basic
RelHom.comp_id : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r →r s), f.comp (RelHom.id r) = f
-- Lean.Meta.Eqns
Lean.Meta.unfoldThmSuffix : String
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.mapId_hom_app : ∀ (X : TopCat) (U : TopologicalSpace.Opens ↑X), (TopologicalSpace.Opens.mapId X).hom.app U = CategoryTheory.eqToHom ⋯
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.GenerateMeasurable.empty : ∀ {α : Type u_1} {s : Set (Set α)}, MeasurableSpace.GenerateMeasurable s ∅
-- Mathlib.MeasureTheory.Function.LpSpace.Complete
/-- `Lp` is complete for `1 ≤ p`.  -/
MeasureTheory.Lp.instCompleteSpace : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {E : Type u_3}
  [inst : NormedAddCommGroup E] [CompleteSpace E] [hp : Fact (1 ≤ p)], CompleteSpace ↥(MeasureTheory.Lp E p μ)
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.hasFiniteIntegral_of_dominated_convergence : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {F : ℕ → α → β} {f : α → β} {bound : α → ℝ},
  MeasureTheory.HasFiniteIntegral bound μ →
    (∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a) →
      (∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) Filter.atTop (nhds (f a))) → MeasureTheory.HasFiniteIntegral f μ
-- Mathlib.Data.Finsupp.Basic
/-- On a `Fintype η`, `Finsupp.split` is an equivalence between `(Σ (j : η), ιs j) →₀ α`
and `Π j, (ιs j →₀ α)`.

This is the `Finsupp` version of `Equiv.Pi_curry`.  -/
Finsupp.sigmaFinsuppEquivPiFinsupp : {α : Type u_1} →
  {η : Type u_13} → [Fintype η] → {ιs : η → Type u_14} → [inst : Zero α] → ((j : η) × ιs j →₀ α) ≃ ((j : η) → ιs j →₀ α)
-- Init.Data.Fin.Bitwise
Fin.xor_val_of_two_pow : ∀ {w : ℕ} (a b : Fin (2 ^ w)), ↑(a ^^^ b) = ↑a ^^^ ↑b
-- Mathlib.Data.Matrix.DMatrix
DMatrix.ext : ∀ {m : Type u_1} {n : Type u_2} {α : m → n → Type v} {M N : DMatrix m n α}, (∀ (i : m) (j : n), M i j = N i j) → M = N
-- Mathlib.Topology.Covering.Quotient
isAddQuotientCoveringMap_iff : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] (f : E → X) (G : Type u_3)
  [inst_2 : AddGroup G] [inst_3 : AddAction G E],
  IsAddQuotientCoveringMap f G ↔
    Topology.IsQuotientMap f ∧
      ContinuousConstVAdd G E ∧
        (∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ AddAction.orbit G e₂) ∧
          ∀ (e : E), ∃ U ∈ nhds e, ∀ (g : G), ((fun x => g +ᵥ x) '' U ∩ U).Nonempty → g = 0
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.UnusedSimpArgsInfo.mask : Lean.Elab.Tactic.UnusedSimpArgsInfo → Array Bool
-- Mathlib.Logic.Function.CompTypeclasses
CompTriple.instId_comp : ∀ {M : Type u_1} {N : Type u_2} {φ : M → N} {ψ : N → N} [CompTriple.IsId ψ], CompTriple φ ψ φ
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.getLast.match_1.splitter : {α : Type u_1} →
  (motive : (x : List α) → x ≠ [] → Sort u_2) →
    (x : List α) →
      (x_1 : x ≠ []) →
        ((h : [] ≠ []) → motive [] h) →
          ((a : α) → (x : [a] ≠ []) → motive [a] x) →
            ((head b : α) → (as : List α) → (x : head :: b :: as ≠ []) → motive (head :: b :: as) x) → motive x x_1
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.restrictionToTruncGE'_f_eq_iso_hom_iso_inv : ∀ {ι : 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.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  {i : ι} {i' : ι'} (hi' : e.f i = i') (hi : ¬e.BoundaryGE i),
  (K.restrictionToTruncGE' e).f i =
    CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hi').hom (K.truncGE'XIso e hi' hi).inv
-- Std.Tactic.BVDecide.LRAT.Parser
_private.Std.Tactic.BVDecide.LRAT.Parser.0.Std.Tactic.BVDecide.LRAT.lratProofToBinary.go : Array Std.Tactic.BVDecide.LRAT.IntAction → ℕ → ByteArray → ByteArray
-- Mathlib.Util.Notation3
/-- Assign a variable to the current `SubExpr`, capturing the local context.  -/
Mathlib.Notation3.MatchState.captureSubexpr : Mathlib.Notation3.MatchState → Lean.Name → Lean.PrettyPrinter.Delaborator.DelabM Mathlib.Notation3.MatchState
-- Mathlib.CategoryTheory.Limits.Shapes.End
/-- The end of a functor `F : Jᵒᵖ ⥤ J ⥤ C`.  -/
CategoryTheory.Limits.coend : {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)) → [CategoryTheory.Limits.HasCoend F] → C
-- Mathlib.Data.Fin.SuccPred
Fin.zero_succAbove : ∀ {n : ℕ} (i : Fin n), Fin.succAbove 0 i = i.succ
-- Mathlib.MeasureTheory.Order.Lattice
MeasurableInf₂.to_hasMeasurableInf : ∀ {M : Type u_1} [inst : MeasurableSpace M] [inst_1 : Min M] [MeasurableInf₂ M], MeasurableInf M
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
HomotopyCategory.homologyFunctor_shiftMap_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CategoryWithHomology C] {K L : CochainComplex C ℤ} {n : ℤ}
  (f : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) (a a' : ℤ) (h : n + a = a') {Z : C}
  (h_1 :
    ((HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0).shift a').obj
        ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      ((HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap
        (CategoryTheory.ShiftedHom.map f (HomotopyCategory.quotient C (ComplexShape.up ℤ))) a a' h)
      h_1 =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) a).hom.app K)
        (CategoryTheory.CategoryStruct.comp
          ((HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap f a a' h)
          ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) a').inv.app L)))
      h_1
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.length_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp], t.toList.length = t.size
-- Mathlib.Topology.UniformSpace.Basic
uniformContinuous₂_def : ∀ {α : Type ua} {β : Type ub} {γ : Type uc} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ]
  (f : α → β → γ), UniformContinuous₂ f ↔ UniformContinuous (Function.uncurry f)
-- Mathlib.Data.Multiset.Dedup
/-- `dedup s` removes duplicates from `s`, yielding a `nodup` multiset.  -/
Multiset.dedup : {α : Type u_1} → [DecidableEq α] → Multiset α → Multiset α
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.FamilyOfElements.ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X} {x y : CategoryTheory.Presieve.FamilyOfElements P R},
  x = y ↔ ∀ {Y : C} (f : Y ⟶ X) (hf : R f), x f hf = y f hf
-- Mathlib.Topology.Connected.PathConnected
JoinedIn.inv : ∀ {G : Type u_4} [inst : InvolutiveInv G] [inst_1 : TopologicalSpace G] [ContinuousInv G] {s : Set G} {a b : G},
  JoinedIn s a b → JoinedIn s⁻¹ a⁻¹ b⁻¹
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.var : Lean.Grind.Linarith.Var → Lean.Grind.Linarith.Expr
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.lt_of_mk_lt_mk_of_le_one : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a b : M},
  MulArchimedeanClass.mk a < MulArchimedeanClass.mk b → a ≤ 1 → a < b
-- Mathlib.RingTheory.Smooth.Basic
Algebra.smooth_iff : ∀ (R : Type u_4) [inst : CommRing R] (A : Type u) [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Algebra.Smooth R A ↔
    autoParam (Algebra.FormallySmooth R A) Algebra.Smooth.formallySmooth._autoParam ∧
      autoParam (Algebra.FinitePresentation R A) Algebra.Smooth.finitePresentation._autoParam
-- Lean.Meta.Instances
Lean.Meta.DefaultInstances.mk.injEq : ∀ (defaultInstances : Lean.NameMap (List (Lean.Name × ℕ))) (priorities : Lean.Meta.PrioritySet)
  (defaultInstances_1 : Lean.NameMap (List (Lean.Name × ℕ))) (priorities_1 : Lean.Meta.PrioritySet),
  ({ defaultInstances := defaultInstances, priorities := priorities } =
      { defaultInstances := defaultInstances_1, priorities := priorities_1 }) =
    (defaultInstances = defaultInstances_1 ∧ priorities = priorities_1)
-- Mathlib.Tactic.Linarith.Verification
/-- If our goal is to add together two inequalities `t1 R1 0` and `t2 R2 0`,
`addIneq R1 R2` produces the strength of the inequality in the sum `R`,
along with the name of a lemma to apply in order to conclude `t1 + t2 R 0`.
 -/
Mathlib.Tactic.Linarith.addIneq : Mathlib.Ineq → Mathlib.Ineq → Lean.Name × Mathlib.Ineq
-- Lean.Data.Lsp.Extra
Lean.Lsp.HighlightMatchesOptions.noConfusionType : Sort v✝ → Lean.Lsp.HighlightMatchesOptions → Lean.Lsp.HighlightMatchesOptions → Sort v✝
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.mk.congr_simp : ∀ {𝕜 : Type u_7} {α : Type u_8} [inst : Zero 𝕜] [inst_1 : LE α] (toFun toFun_1 : α → α → 𝕜) (e_toFun : toFun = toFun_1)
  (eq_zero_of_not_le' : ∀ ⦃a b : α⦄, ¬a ≤ b → toFun a b = 0),
  { toFun := toFun, eq_zero_of_not_le' := eq_zero_of_not_le' } = { toFun := toFun_1, eq_zero_of_not_le' := ⋯ }
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.isRkFinite_of_finite : ∀ {α : Type u_1} {X : Set α} (M : Matroid α), X.Finite → M.IsRkFinite X
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- The right lift along the identity.  -/
CategoryTheory.Bicategory.RightLift.alongId : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a c : B} → (g : c ⟶ a) → CategoryTheory.Bicategory.RightLift (CategoryTheory.CategoryStruct.id a) g
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.hasUVar : Lean.Level → Bool
-- Mathlib.Topology.Semicontinuity.Basic
IsOpen.lowerSemicontinuous_indicator : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {s : Set α} {y : β} [inst_1 : Zero β] [inst_2 : Preorder β],
  IsOpen s → 0 ≤ y → LowerSemicontinuous (s.indicator fun _x => y)
-- Mathlib.GroupTheory.Coxeter.Basic
_private.Mathlib.GroupTheory.Coxeter.Basic.0.CoxeterSystem.alternatingWord.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (m : ℕ) (h_1 : Unit → motive 0) (h_2 : (m : ℕ) → motive m.succ),
  (match m.succ with
    | 0 => h_1 ()
    | m.succ => h_2 m) =
    h_2 m
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The sine of an angle in a right-angled triangle as a ratio of sides, version subtracting
vectors.  -/
Orientation.sin_oangle_sub_left_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → (o.oangle (x - y) x).sin = ‖y‖ / ‖x - y‖
-- Mathlib.SetTheory.Ordinal.Notation
ONote.nf_opow : ∀ (o₁ o₂ : ONote) [o₁.NF] [o₂.NF], (o₁ ^ o₂).NF
-- Std.Async.Basic
Std.Async.BaseAsync.instMonadAsyncTask : Std.Async.MonadAsync Task Std.Async.BaseAsync
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.inr_v_desc_f_assoc : ∀ {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 φ] {M : CochainComplex C ℤ}
  (α : CochainComplex.HomComplex.Cochain K M 0) (β : CochainComplex.HomComplex.Cocycle L M 1)
  (hαβ : CochainComplex.HomComplex.δ 0 1 α + (CochainComplex.HomComplex.Cochain.ofHom φ).comp ↑β ⋯ = 0) (p q : ℤ)
  (hpq : p + 1 = q) {Z : C} (h : M.X q ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCocone.inr φ)).v p q hpq)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.desc φ α β hαβ).f q) h) =
    CategoryTheory.CategoryStruct.comp ((↑β).v p q hpq) h
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- Given an isomorphism `e : L ⋙ G ≅ L'`, a right extension of `F` along `L'` is universal
iff the corresponding right extension of `L` along `L` is.  -/
CategoryTheory.Functor.RightExtension.isUniversalPostcomp₁Equiv : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      {D' : Type u_5} →
        [inst : CategoryTheory.Category.{v_1, u_1} C] →
          [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
            [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
              [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] →
                {L : CategoryTheory.Functor C D} →
                  {L' : CategoryTheory.Functor C D'} →
                    (G : CategoryTheory.Functor D D') →
                      [G.IsEquivalence] →
                        (e : L.comp G ≅ L') →
                          (F : CategoryTheory.Functor C H) →
                            (ex : L'.RightExtension F) →
                              CategoryTheory.CostructuredArrow.IsUniversal ex ≃
                                CategoryTheory.CostructuredArrow.IsUniversal
                                  ((CategoryTheory.Functor.RightExtension.postcomp₁ G e.hom F).obj ex)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.isCycle_copy : ∀ {V : Type u} {G : SimpleGraph V} {u u' : V} (p : G.Walk u u) (hu : u = u'), (p.copy hu hu).IsCycle ↔ p.IsCycle
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.iso_eq_iso_refl : ∀ {x : SimplexCategory} (e : x ≅ x), e = CategoryTheory.Iso.refl x
-- Mathlib.Topology.Algebra.Module.Star
skewAdjointPartL_apply_coe : ∀ (R : Type u_1) (A : Type u_2) [inst : Semiring R] [inst_1 : StarMul R] [inst_2 : TrivialStar R]
  [inst_3 : AddCommGroup A] [inst_4 : Module R A] [inst_5 : StarAddMonoid A] [inst_6 : StarModule R A]
  [inst_7 : Invertible 2] [inst_8 : TopologicalSpace A] [inst_9 : ContinuousSub A] [inst_10 : ContinuousStar A]
  [inst_11 : ContinuousConstSMul R A] (x : A), ↑((skewAdjointPartL R A) x) = ⅟2 • (x - star x)
-- Mathlib.RingTheory.Regular.Category
ModuleCat.smulShortComplex_X₁_carrier : ∀ {R : Type u} [inst : CommRing R] (M : ModuleCat R) (r : R), ↑(M.smulShortComplex r).X₁ = ↑M
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullback.diagonal_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullback f f],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.diagonal f)
      (CategoryTheory.Limits.pullback.fst f f) =
    CategoryTheory.CategoryStruct.id X
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.equivIco.congr_simp : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [hp : Fact (0 < p)] (a : 𝕜) [inst_3 : Archimedean 𝕜], AddCircle.equivIco p a = AddCircle.equivIco p a
-- Mathlib.Probability.Process.LocalProperty
_private.Mathlib.Probability.Process.LocalProperty.0.ProbabilityTheory.mkStrictMonoAux.eq_1 : ∀ (x : ℕ → ℕ), ProbabilityTheory.mkStrictMonoAux✝ x 0 = x 0
-- Mathlib.Order.SuccPred.Limit
WithTop.isPredPrelimit_iff : ∀ {α : Type u_1} [inst : Preorder α] {x : WithTop α}, Order.IsPredPrelimit x ↔ x = ⊤ ∨ ∃ y, x = ↑y ∧ Order.IsPredLimit y
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.continuum_power_aleph0 : Cardinal.continuum ^ Cardinal.aleph0 = Cardinal.continuum
-- Std.Data.TreeMap.Basic
/-- Transforms a list of mappings into a tree map.  -/
Std.TreeMap.ofArray : {α : Type u} →
  {β : Type v} → Array (α × β) → (cmp : autoParam (α → α → Ordering) Std.TreeMap.ofArray._auto_1) → Std.TreeMap α β cmp
-- Mathlib.Combinatorics.Derangements.Finite
card_derangements_fin_eq_numDerangements : ∀ {n : ℕ}, Fintype.card ↑(derangements (Fin n)) = numDerangements n
-- Mathlib.GroupTheory.OrderOfElement
Subsingleton.orderOf_eq : ∀ {G : Type u_1} [inst : Monoid G] [Subsingleton G] (x : G), orderOf x = 1
-- Mathlib.Topology.Homotopy.Basic
/-- Given continuous maps `f₀` and `f₁`, we say `f₀` and `f₁` are homotopic relative to a set `S` if
there exists a `HomotopyRel f₀ f₁ S`.
 -/
ContinuousMap.HomotopicRel : {X : Type u} →
  {Y : Type v} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → C(X, Y) → C(X, Y) → Set X → Prop
-- Lean.Meta.AppBuilder
/-- Returns `let_congr h₁ h₂`  -/
Lean.Meta.mkLetCongr : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.Grpd.freeForgetAdjunction_homEquiv_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{u, u} C] {D : Type u} [inst_1 : CategoryTheory.Groupoid D]
  (F : CategoryTheory.Functor C D),
  (CategoryTheory.Grpd.freeForgetAdjunction.homEquiv (CategoryTheory.Cat.of C) (CategoryTheory.Grpd.of D)).symm
      F.toCatHom =
    (CategoryTheory.FreeGroupoid.map F).comp (CategoryTheory.FreeGroupoid.lift (CategoryTheory.Functor.id D))
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- The structure presheaf, valued in `CommRingCat`, constructed by dressing up the `Type`-valued
structure presheaf.  -/
AlgebraicGeometry.structurePresheafInCommRingCat : (R : Type u) → [inst : CommRing R] → TopCat.Presheaf CommRingCat (AlgebraicGeometry.PrimeSpectrum.Top R)
-- Mathlib.Order.ModularLattice
inf_sup_le_assoc_of_le : ∀ {α : Type u_1} [inst : Lattice α] [IsModularLattice α] {x z : α} (y : α), z ≤ x → x ⊓ (y ⊔ z) ≤ x ⊓ y ⊔ z
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.toProd_one : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : One α], NonemptyInterval.toProd 1 = 1
-- Mathlib.Topology.Algebra.Support
tsupport_smul_subset_left : ∀ {X : Type u_1} [inst : TopologicalSpace X] {M : Type u_9} {α : Type u_10} [inst_1 : Zero M] [inst_2 : Zero α]
  [inst_3 : SMulWithZero M α] (f : X → M) (g : X → α), (tsupport fun x => f x • g x) ⊆ tsupport f
-- Lean.Data.KVMap
Lean.DataValue.ofInt : ℤ → Lean.DataValue
-- Std.Tactic.BVDecide.LRAT.Internal.Entails
Std.Tactic.BVDecide.LRAT.Internal.incompatible_of_unsat : ∀ (α : Type u) {σ1 : Type v} {σ2 : Type w} [inst : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ1]
  [inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ2] (f1 : σ1) (f2 : σ2),
  Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable α f1 → Std.Tactic.BVDecide.LRAT.Internal.Incompatible α f1 f2
-- Lean.Server.FileWorker.InlayHints
Lean.Server.FileWorker.InlayHintState : Type
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.toTrivSqZeroExt_ι : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Module Rᵐᵒᵖ M] [inst_4 : IsCentralScalar R M] (x : M),
  ExteriorAlgebra.toTrivSqZeroExt ((ExteriorAlgebra.ι R) x) = TrivSqZeroExt.inr x
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
_private.Mathlib.Algebra.Order.Monoid.Unbundled.WithTop.0.WithTop.addMonoid.match_1.splitter : {α : Type u_1} →
  (motive : WithTop α → ℕ → Sort u_2) →
    (a : WithTop α) →
      (n : ℕ) →
        ((a : α) → (n : ℕ) → motive (some a) n) → (Unit → motive none 0) → ((_n : ℕ) → motive none _n.succ) → motive a n
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.inv_hom_apply : ∀ {X Y : CommGrpCat} (e : X ≅ Y) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.isHomogeneous_zero : ∀ (σ : Type u_1) (R : Type u_3) [inst : CommSemiring R] (n : ℕ), MvPolynomial.IsHomogeneous 0 n
-- Init.Data.String.Basic
String.Slice.Pos.ofCopy_copy : ∀ {s : String.Slice} {pos : s.Pos}, pos.copy.ofCopy = pos
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.instRespectsIsoSchemeTopologicallyGeneralizingMap : (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => GeneralizingMap).RespectsIso
-- Init.Data.Array.Basic
/-- Returns the largest element of the array, as determined by the comparison `lt`, or `none` if
the array is empty.

Examples:
* `(#[] : Array Nat).getMax? (· < ·) = none`
* `#["red", "green", "blue"].getMax? (·.length < ·.length) = some "green"`
* `#["red", "green", "blue"].getMax? (· < ·) = some "red"`
 -/
Array.getMax? : {α : Type u} → Array α → (α → α → Bool) → Option α
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.tan_periodic : Function.Periodic Real.tan Real.pi