mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.cyclesMap_comp_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j')
  (g' : j' ⟶ k') {i'' j'' k'' : ι} (f'' : i'' ⟶ j'') (g'' : j'' ⟶ k'')
  (α : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g')
  (α' : CategoryTheory.ComposableArrows.mk₂ f' g' ⟶ CategoryTheory.ComposableArrows.mk₂ f'' g'')
  (α'' : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f'' g'') (n : ℤ),
  autoParam (CategoryTheory.CategoryStruct.comp α α' = α'')
      CategoryTheory.Abelian.SpectralObject.cyclesMap_comp._auto_1 →
    ∀ {Z : C} (h : X.cycles f'' g'' n ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.cyclesMap f g f' g' α n)
          (CategoryTheory.CategoryStruct.comp (X.cyclesMap f' g' f'' g'' α' n) h) =
        CategoryTheory.CategoryStruct.comp (X.cyclesMap f g f'' g'' α'' n) h
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.withBotCoe_inj : ∀ {ι : Type u_1} {I J : WithBot (BoxIntegral.Box ι)}, ↑I = ↑J ↔ I = J
-- Mathlib.CategoryTheory.Limits.Types.Yoneda
/-- A cocone on `F` with cocone point `X` is the same as an element of `lim Hom(F·, X)`.  -/
CategoryTheory.Limits.limitCompYonedaIsoCocone : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (F : CategoryTheory.Functor J C) →
          (X : C) →
            CategoryTheory.Limits.limit (F.op.comp (CategoryTheory.yoneda.obj X)) ≅
              F ⟶ (CategoryTheory.Functor.const J).obj X
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₁₂.d₂_eq : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₁₂] [inst_9 : CategoryTheory.Preadditive C₄]
  (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [inst_10 : F₁₂.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_12 : G.Additive]
  [inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9}
  {ι₁₂ : Type u_10} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [inst_18 : DecidableEq ι₁₂]
  [inst_19 : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) {i₂ i₂' : ι₂},
  c₂.Rel i₂ i₂' →
    ∀ (i₃ : ι₃) (j : ι₄),
      HomologicalComplex.mapBifunctor₁₂.d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j =
        (c₁₂.ε₁ c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₂ c₂ c₁₂ (i₁, i₂)) •
          CategoryTheory.CategoryStruct.comp ((G.map ((F₁₂.obj (K₁.X i₁)).map (K₂.d i₂ i₂'))).app (K₃.X i₃))
            (HomologicalComplex.mapBifunctor₁₂.ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂' i₃ j)
-- Mathlib.RingTheory.Congruence.Defs
RingCon.coe_zsmul : ∀ {R : Type u_1} [inst : AddGroup R] [inst_1 : Mul R] (c : RingCon R) (z : ℤ) (x : R), ↑(z • x) = z • ↑x
-- Mathlib.CategoryTheory.Limits.Types.Limits
CategoryTheory.Limits.Types.Limit.lift_π_apply : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u))
  [inst_1 : CategoryTheory.Limits.HasLimit F] (s : CategoryTheory.Limits.Cone F) (j : J) (x : s.pt),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F j))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.lift F s)) x) =
    (CategoryTheory.ConcreteCategory.hom (s.π.app j)) x
-- Mathlib.Logic.Denumerable
Denumerable.ofNat_nat : ∀ (n : ℕ), Denumerable.ofNat ℕ n = n
-- Batteries.Recycling.RBTree.Depth
/-- A well formed tree has `t.depth ∈ O(log t.size)`, that is, it is well balanced.
This justifies the `O(log n)` bounds on most searching operations of `RBSet`.
 -/
RBTree.RBNode.WF.depth_bound : ∀ {α : Type u_1} {cmp : α → α → Ordering} {t : RBTree.RBNode α},
  RBTree.RBNode.WF cmp t → t.depth ≤ 2 * (t.size + 1).log2
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
Lean.Meta.Grind.Arith.Linear.getNatStructId? : Lean.Expr → Lean.Meta.Grind.GoalM (Option ℕ)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
cfc_comp_norm : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : Ring A] [inst_2 : TopologicalSpace A]
  [inst_3 : StarRing A] [inst_4 : PartialOrder A] [inst_5 : StarOrderedRing A] [inst_6 : Algebra 𝕜 A]
  [inst_7 : ContinuousFunctionalCalculus 𝕜 A p] [inst_8 : Algebra ℝ A] [inst_9 : NonnegSpectrumClass ℝ A]
  [IsTopologicalRing A] [T2Space A] [inst_12 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (f : 𝕜 → 𝕜) (a : A),
  autoParam (p a) cfc_comp_norm._auto_1 →
    autoParam (ContinuousOn f ((fun z => ↑‖z‖) '' spectrum 𝕜 a)) cfc_comp_norm._auto_3 →
      cfc (fun x => f ↑‖x‖) a = cfc f (CFC.abs a)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryLE!_eq_get!_getEntryLE? : ∀ {α : Type u} {β : Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α fun x => β} {k : α}
  [inst_1 : Inhabited (α × β)],
  Std.DTreeMap.Internal.Impl.Const.getEntryLE! k t = (Std.DTreeMap.Internal.Impl.Const.getEntryLE? k t).get!
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- The forgetful functor from group objects to monoid objects is fully faithful.  -/
CategoryTheory.Grp.fullyFaithfulForget₂Mon : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → (CategoryTheory.Grp.forget₂Mon C).FullyFaithful
-- Mathlib.Data.Fin.Basic
Fin.val_add_eq_of_add_lt : ∀ {n : ℕ} {a b : Fin n}, ↑a + ↑b < n → ↑(a + b) = ↑a + ↑b
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.hausdorffMeasure_measurePreserving_piFinTwo : ∀ (α : Fin 2 → Type u_4) [inst : (i : Fin 2) → MeasurableSpace (α i)] [inst_1 : (i : Fin 2) → EMetricSpace (α i)]
  [inst_2 : ∀ (i : Fin 2), BorelSpace (α i)] [inst_3 : ∀ (i : Fin 2), SecondCountableTopology (α i)] (d : ℝ),
  MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piFinTwo α)) (MeasureTheory.Measure.hausdorffMeasure d)
    (MeasureTheory.Measure.hausdorffMeasure d)
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.Monoidal.tensorHom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] {F G F' G' : CategoryTheory.Functor C D} {α : F ⟶ G} {β : F' ⟶ G'}
  {X : C},
  (CategoryTheory.MonoidalCategoryStruct.tensorHom α β).app X =
    CategoryTheory.MonoidalCategoryStruct.tensorHom (α.app X) (β.app X)
-- Init.Data.Array.Lemmas
Array.back_eq_getElem : ∀ {α : Type u_1} {xs : Array α} (h : 0 < xs.size), xs.back h = xs[xs.size - 1]
-- Mathlib.Data.ENNReal.Operations
ENNReal.natCast_sub : ∀ (m n : ℕ), ↑(m - n) = ↑m - ↑n
-- Mathlib.FieldTheory.KrullTopology
/-- If `L/K` is an algebraic extension, then the Krull topology on `Gal(L/K)` is Hausdorff.  -/
krullTopology_t2 : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Algebra.IsIntegral K L],
  T2Space Gal(L/K)
-- Lean.Data.Lsp.Internal
Lean.Lsp.instToJsonModuleRefs : Lean.ToJson Lean.Lsp.ModuleRefs
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Substructure.FG.sup : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] {N₁ N₂ : L.Substructure M},
  N₁.FG → N₂.FG → (N₁ ⊔ N₂).FG
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charpoly_transpose : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R),
  M.transpose.charpoly = M.charpoly
-- Mathlib.Algebra.Category.Ring.Adjunctions
CommRingCat.coyoneda_map_app : ∀ {m n : Type vᵒᵖ} (f : m ⟶ n) (R : CommRingCat),
  (CommRingCat.coyoneda.map f).app R =
    CommRingCat.ofHom
      (RingHom.pi fun x => Pi.evalRingHom (fun a => ↑R) ((CategoryTheory.ConcreteCategory.hom f.unop) x))
-- Mathlib.MeasureTheory.Group.LIntegral
/-- Translating a function by left-addition does not change its Lebesgue integral with
respect to a left-invariant measure.  -/
MeasureTheory.lintegral_add_left_eq_self : ∀ {G : Type u_1} [inst : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_1 : AddGroup G] [MeasurableAdd G]
  [μ.IsAddLeftInvariant] (f : G → ENNReal) (g : G), ∫⁻ (x : G), f (g + x) ∂μ = ∫⁻ (x : G), f x ∂μ
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- A morphism of chain complexes
induces a morphism of arrows of the differentials into each object.
 -/
HomologicalComplex.Hom.sqTo : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        {c : ComplexShape ι} →
          {C₁ C₂ : HomologicalComplex V c} →
            C₁.Hom C₂ → (j : ι) → CategoryTheory.Arrow.mk (C₁.dTo j) ⟶ CategoryTheory.Arrow.mk (C₂.dTo j)
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.commutator_mono : ∀ {G : Type u_1} [inst : Group G] {H₁ H₂ K₁ K₂ : Subgroup G}, H₁ ≤ K₁ → H₂ ≤ K₂ → ⁅H₁, H₂⁆ ≤ ⁅K₁, K₂⁆
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddModObj.add_vadd_self_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : C)
  [inst_2 : CategoryTheory.AddMonObj M] (X : C) [inst_3 : CategoryTheory.AddModObj M X] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.add X)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddModObj.vadd h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M X).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M CategoryTheory.AddModObj.vadd)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.AddModObj.vadd h))
-- Mathlib.Lean.ContextInfo
/-- Run tactic code, given by a piece of syntax, in the context of an infotree node.
The optional `MetaM` argument `m` performs postprocessing on the goals produced.  -/
Lean.Elab.ContextInfo.runTacticCode : Lean.Elab.ContextInfo →
  Lean.Elab.TacticInfo →
    Lean.MVarId →
      Lean.Syntax →
        (m : optParam ((α : Type) × (Lean.MVarId → Lean.MetaM α)) ⟨Lean.MVarId, pure⟩) →
          Lean.Elab.Command.CommandElabM (List m.fst)
-- Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
/-- **Alias** of `MeromorphicOn.circleIntegrable_log_norm`.

---

If `f` is complex meromorphic on a circle in the complex plane, then `log ‖f ·‖` is circle
integrable over that circle.
 -/
circleIntegrable_log_norm_meromorphicOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {c : ℂ} {R : ℝ} {f : ℂ → E},
  MeromorphicOn f (Metric.sphere c |R|) → CircleIntegrable (fun x => Real.log ‖f x‖) c R
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- The natural map from `[a, a + p] ⊂ 𝕜` with endpoints identified to `𝕜 / ℤ • p`, as a
homeomorphism of topological spaces.  -/
AddCircle.homeoIccQuot : {𝕜 : Type u_1} →
  [inst : AddCommGroup 𝕜] →
    [inst_1 : LinearOrder 𝕜] →
      [inst_2 : IsOrderedAddMonoid 𝕜] →
        (p a : 𝕜) →
          [hp : Fact (0 < p)] →
            [Archimedean 𝕜] →
              [inst_4 : TopologicalSpace 𝕜] → [OrderTopology 𝕜] → AddCircle p ≃ₜ Quot (AddCircle.EndpointIdent p a)
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preAleph_zero : Cardinal.preAleph 0 = 0
-- Mathlib.Order.Hom.Bounded
TopHom.instSemilatticeInf.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Top α] [inst_1 : SemilatticeInf β] [inst_2 : OrderTop β],
  TopHom.instSemilatticeInf = Function.Injective.semilatticeInf DFunLike.coe ⋯ ⋯ ⋯ ⋯
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.toFullSubcategory_P_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X : P.FullSubcategory}
  (Q : HomotopicalAlgebra.PrepathObject X.obj) (hQ : P Q.P), (Q.toFullSubcategory hQ).P.obj = Q.P
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.le_rpow_self_of_one_le : ∀ {x : ENNReal} {z : ℝ}, 1 ≤ x → 1 ≤ z → x ≤ x ^ z
-- Mathlib.ModelTheory.Definability
/-- **Alias** of `Set.DefinableFun.ofPred_eq_const`.

---

The preimage of a constant under a definable function is definable.  -/
Set.DefinableFun.setOf_eq_const : ∀ {M : Type u_1} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u_2} {A : Set M} {f : (α → M) → M},
  Set.DefinableFun L A f → ∀ {a : M}, a ∈ A → A.Definable L {v | f v = a}
-- Mathlib.Data.Real.ConjExponents
ENNReal.HolderConjugate.toReal_iff : ∀ {p q : ENNReal}, 1 < p.toReal → (p.toReal.HolderConjugate q.toReal ↔ p.HolderConjugate q)
-- Mathlib.Order.RelIso.Basic
RelHom.map_rel : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r →r s) {a b : α}, r a b → s (f a) (f b)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
CategoryTheory.Functor.Monoidal.tensorHom_app_snd : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.CartesianMonoidalCategory C]
  {F₁ F₁' F₂ F₂' : CategoryTheory.Functor J C} (f : F₁ ⟶ F₁') (g : F₂ ⟶ F₂') (j : J),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorHom f g).app j)
      (CategoryTheory.SemiCartesianMonoidalCategory.snd (F₁'.obj j) (F₂'.obj j)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd (F₁.obj j) (F₂.obj j))
      (g.app j)
-- Std.Data.ExtTreeMap.Basic
/-- Given a proof that such a mapping exists, retrieves the smallest key that is
greater than the given key.
 -/
Std.ExtTreeMap.getKeyGT : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      [inst : Std.TransCmp cmp] → (t : Std.ExtTreeMap α β cmp) → (k : α) → (∃ a ∈ t, cmp a k = Ordering.gt) → α
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiringClass.mk : ∀ {S : Type u_1} {R : outParam (Type u)} [inst : NonUnitalNonAssocSemiring R] [inst_1 : SetLike S R]
  [toAddSubmonoidClass : AddSubmonoidClass S R],
  (∀ {s : S} {a b : R}, a ∈ s → b ∈ s → a * b ∈ s) → NonUnitalSubsemiringClass S R
-- Mathlib.Logic.Embedding.Basic
/-- The identity map as a `Function.Embedding`.  -/
Function.Embedding.refl : (α : Sort u_1) → α ↪ α
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.reachable_deleteEdges_iff_exists_walk : ∀ {V : Type u} {G : SimpleGraph V} {v w v' w' : V}, (G.deleteEdges {s(v, w)}).Reachable v' w' ↔ ∃ p, s(v, w) ∉ p.edges
-- Init.SimpLemmas
instAssociativeOr : Std.Associative Or
-- Std.Data.TreeSet.Basic
/-- Computes the union of the given tree sets. If both maps contain elements that are equal according
to the comparison function, the element contained in the second argument will appear in the result.

This function always merges the smaller set into the larger set.
 -/
Std.TreeSet.union : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → Std.TreeSet α cmp → Std.TreeSet α cmp
-- Init.Meta.Defs
Lean.toolchain : String
-- Init.Data.Order.PackageFactories
Std.Packages.PreorderOfLEArgs.le : {α : Type u} → Std.Packages.PreorderOfLEArgs α → LE α
-- Mathlib.Topology.Algebra.Monoid
/-- **Alias** of `continuousOn_finsetSum`. -/
continuousOn_finset_sum : ∀ {ι : Type u_1} {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M]
  [inst_2 : AddCommMonoid M] [ContinuousAdd M] {f : ι → X → M} (s : Finset ι) {t : Set X},
  (∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun a => ∑ i ∈ s, f i a) t
-- Mathlib.Topology.Bases
TopologicalSpace.IsTopologicalBasis.eq_of_forall_subset_iff : ∀ {α : Type u} [t : TopologicalSpace α] {B : Set (Set α)} {s t_1 : Set α},
  TopologicalSpace.IsTopologicalBasis B → IsOpen s → IsOpen t_1 → (∀ U ∈ B, U ⊆ s ↔ U ⊆ t_1) → s = t_1
-- Mathlib.CategoryTheory.Monoidal.Bimon_
/-- The forgetful functor from bimonoid objects to the underlying category.  -/
CategoryTheory.Bimon.forget : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.Functor (CategoryTheory.Bimon C) C
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
/-- Main theorem of this file. It shows that there exists a function satisfying the corecursive
definition of the form `def foo (x : X) := hd x :: op (foo (tlArg x))` where `f` is friendly.  -/
Tactic.ComputeAsymptotics.Seq.FriendlyOperation.exists_fixed_point : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (F : β → Option (α × γ × β)) (op : γ → Stream'.Seq α → Stream'.Seq α)
  [h : Tactic.ComputeAsymptotics.Seq.FriendlyOperationClass op],
  ∃ f,
    ∀ (b : β),
      match F b with
      | none => f b = Stream'.Seq.nil
      | some (a, c, b') => f b = Stream'.Seq.cons a (op c (f b'))
-- Lean.Parser.Extension
Lean.Parser.ParserAliasInfo.mk.injEq : ∀ (declName : Lean.Name) (stackSz? : Option ℕ) (autoGroupArgs : Bool) (declName_1 : Lean.Name) (stackSz?_1 : Option ℕ)
  (autoGroupArgs_1 : Bool),
  ({ declName := declName, stackSz? := stackSz?, autoGroupArgs := autoGroupArgs } =
      { declName := declName_1, stackSz? := stackSz?_1, autoGroupArgs := autoGroupArgs_1 }) =
    (declName = declName_1 ∧ stackSz? = stackSz?_1 ∧ autoGroupArgs = autoGroupArgs_1)
-- Init.Data.Range.Basic
Std.Legacy.Range.forM : {m : Type u_1 → Type u_2} → [Monad m] → Std.Legacy.Range → (ℕ → m PUnit.{u_1 + 1}) → m PUnit.{u_1 + 1}
-- Mathlib.MeasureTheory.VectorMeasure.WithDensity
MeasureTheory.Measure.withDensityᵥ_absolutelyContinuous : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ℝ),
  (μ.withDensityᵥ f).AbsolutelyContinuous μ.toENNRealVectorMeasure
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_cons_of_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k},
  (k == a) = false → Std.Internal.List.getKey? a (⟨k, v⟩ :: l) = Std.Internal.List.getKey? a l
-- Init.Data.Nat.Basic
Nat.lt_of_succ_lt : ∀ {n m : ℕ}, n.succ < m → n < m
-- Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
alternatingGroup.normal_subgroup_eq_bot_or_eq_top : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α],
  5 ≤ Nat.card α → ∀ {N : Subgroup ↥(alternatingGroup α)} [N.Normal], N = ⊥ ∨ N = ⊤
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
HasFiniteFPowerSeriesOnBall.hasFDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {n : ℕ} {f : E → F} {x : E},
  HasFiniteFPowerSeriesOnBall f p x n r →
    ∀ {y : E}, ↑‖y‖₊ < r → HasFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin y 1)) (x + y)
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
/-- The functor of monoids associated to a functor of submonoids.  -/
CategoryTheory.SubmonoidFunctor.toFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {M : CategoryTheory.Functor C MonCat} → CategoryTheory.SubmonoidFunctor M → CategoryTheory.Functor C MonCat
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_sub : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIocMod hp a (b - p) = toIocMod hp a b
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.PrepareRenameParams.mk.injEq : ∀ (toTextDocumentPositionParams toTextDocumentPositionParams_1 : Lean.Lsp.TextDocumentPositionParams),
  ({ toTextDocumentPositionParams := toTextDocumentPositionParams } =
      { toTextDocumentPositionParams := toTextDocumentPositionParams_1 }) =
    (toTextDocumentPositionParams = toTextDocumentPositionParams_1)
-- Init.Data.Nat.ToString
Nat.length_toDigits_pos : ∀ {b n : ℕ}, 0 < (b.toDigits n).length
-- Mathlib.CategoryTheory.Presentable.ColimitPresentation
/-- Composition of morphisms in the `Total` category.  -/
CategoryTheory.Limits.ColimitPresentation.Total.Hom.comp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u_1} →
      {I : J → Type u_2} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} J] →
          [inst_2 : (j : J) → CategoryTheory.Category.{u_3, u_2} (I j)] →
            {D : CategoryTheory.Functor J C} →
              {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)} →
                {k l m : CategoryTheory.Limits.ColimitPresentation.Total P} → k.Hom l → l.Hom m → k.Hom m
-- Mathlib.Data.Finset.Disjoint
Finset.disjoint_singleton : ∀ {α : Type u_2} {a b : α}, Disjoint {a} {b} ↔ a ≠ b
-- Mathlib.Topology.Algebra.UniformMulAction
IsUniformInducing.uniformContinuousConstVAdd : ∀ {M : Type v} {X : Type x} {Y : Type y} [inst : UniformSpace X] [inst_1 : UniformSpace Y] [inst_2 : VAdd M X]
  [inst_3 : VAdd M Y] [UniformContinuousConstVAdd M Y] {f : X → Y},
  IsUniformInducing f → (∀ (c : M) (x : X), f (c +ᵥ x) = c +ᵥ f x) → UniformContinuousConstVAdd M X
-- Mathlib.Data.Matrix.Diagonal
Matrix.map_intCast : ∀ {n : Type u_3} {α : Type v} {β : Type w} [inst : DecidableEq n] [inst_1 : AddGroupWithOne α] [inst_2 : Zero β]
  {f : α → β}, f 0 = 0 → ∀ (d : ℤ), (↑d).map f = Matrix.diagonal fun x => f ↑d
-- Init.Data.Vector.Lex
Vector.instTransLeOfLawfulOrderLTOfIsLinearOrder : {α : Type u_1} →
  {n : ℕ} →
    [inst : LT α] →
      [inst_1 : LE α] →
        [Std.LawfulOrderLT α] →
          [Std.IsLinearOrder α] → Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2
-- Mathlib.Condensed.Light.TopCatAdjunction
LightCondSet.instEpiTopCatAppCounitTopCatAdjunction : ∀ (X : TopCat), CategoryTheory.Epi (LightCondSet.topCatAdjunction.counit.app X)
-- Mathlib.Geometry.Manifold.ContMDiff.Atlas
/-- The inverse of an atlas member is `C^n` for any `n`.  -/
contMDiffOn_symm_of_mem_maximalAtlas : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} {e : OpenPartialHomeomorph M H},
  e ∈ IsManifold.maximalAtlas I n M → ContMDiffOn I I n (↑e.symm) e.target
-- Mathlib.Data.List.AList
AList.insertRec_insert_mk : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {C : AList β → Sort u_1} (H0 : C ∅)
  (IH : (a : α) → (b : β a) → (l : AList β) → a ∉ l → C l → C (AList.insert a b l)) {a : α} (b : β a) {l : AList β}
  (h : a ∉ l), AList.insertRec H0 IH (AList.insert a b l) = IH a b l h (AList.insertRec H0 IH l)
-- Mathlib.Topology.Algebra.Group.Basic
/-- The connected component of 0 is a subgroup of `G`.  -/
AddSubgroup.connectedComponentOfZero : (G : Type u_1) → [inst : TopologicalSpace G] → [inst_1 : AddGroup G] → [IsTopologicalAddGroup G] → AddSubgroup G
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion_apply : ∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] [inst_1 : Nonempty ι] [inst_2 : IsDirectedOrder ι]
  {M : Type u_1} [inst_3 : L.Structure M] (S : ι →o L.Substructure M) {i : ι} (x : ↥(S i)),
  (FirstOrder.Language.DirectLimit.Equiv_iSup S).symm ((FirstOrder.Language.Substructure.inclusion ⋯) x) =
    (FirstOrder.Language.DirectLimit.of L ι (fun x => ↥(S x))
        (fun x x_1 h => FirstOrder.Language.Substructure.inclusion ⋯) i)
      x