mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.norm_le_iff_le_algebraMap : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] (a : A) {r : ℝ},
  0 ≤ r → autoParam (0 ≤ a) CStarAlgebra.norm_le_iff_le_algebraMap._auto_1 → (‖a‖ ≤ r ↔ a ≤ (algebraMap ℝ A) r)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.instUsesSetNotationForOrder : UsesSetNotationForOrder ZFSet.{u}
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPushout.epi_inl_of_epi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P},
  CategoryTheory.IsPushout f g inl inr →
    autoParam (CategoryTheory.Epi g) CategoryTheory.IsPushout.epi_inl_of_epi._auto_1 → CategoryTheory.Epi inl
-- Mathlib.Data.Multiset.FinsetOps
Multiset.mem_ndinsert_self : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Multiset α), a ∈ Multiset.ndinsert a s
-- Mathlib.Order.Defs.LinearOrder
max_eq_left_of_lt : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, b < a → max a b = a
-- Mathlib.CategoryTheory.ObjectProperty.Extensions
CategoryTheory.ObjectProperty.IsClosedUnderExtensions.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C],
  (∀ {S : CategoryTheory.ShortComplex C}, S.ShortExact → P S.X₁ → P S.X₃ → P S.X₂) → P.IsClosedUnderExtensions
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
/-- Given `F : J ⥤ w₀`, `c : F.CoconeTypes` and `G : J' ⥤ J`, this is
the induced cocone in `(G ⋙ F).CoconeTypes`.  -/
CategoryTheory.Functor.CoconeTypes.precomp : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {F : CategoryTheory.Functor J (Type w₀)} →
      F.CoconeTypes →
        {J' : Type u_1} →
          [inst_1 : CategoryTheory.Category.{v_1, u_1} J'] → (G : CategoryTheory.Functor J' J) → (G.comp F).CoconeTypes
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.PositiveCompacts.coe_top : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : Nonempty α], ↑⊤ = Set.univ
-- Mathlib.Tactic.DepRewrite
/-- Apply `rw!` to the goal.  -/
Mathlib.Tactic.DepRewrite.depRwTarget : Lean.Syntax → Bool → optParam Mathlib.Tactic.DepRewrite.Config { } → Lean.Elab.Tactic.TacticM Unit
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.«builder_option(Cases_patterns:=[_])» : Lean.ParserDescr
-- Mathlib.Analysis.Complex.Basic
/-- **Alias** of `Complex.isClosedEmbedding_intCast`. -/
Complex.closedEmbedding_intCast : Topology.IsClosedEmbedding Int.cast
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.fold.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α → Sort u_2) →
    (x : RBTree.RBNode α) →
      (Unit → motive RBTree.RBNode.nil) →
        ((c : RBTree.RBColor) →
            (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.node c l v r)) →
          motive x
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopicWith.refl : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {P : C(X, Y) → Prop}
  (f : C(X, Y)), P f → f.HomotopicWith f P
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
/-- `u` is a **left quasi-inverse** to `v` if `u ∘ₗ v ≈ id` modulo
linear maps with noetherian ranges. Recall that if the scalar ring is noetherian
(e.g a field), then "noetherian range" can be replaced by "finitely generated range".  -/
LinearMap.IsLeftQuasiInverse : {K : Type u_1} →
  {V : Type u_2} →
    {V₂ : Type u_4} →
      [inst : CommRing K] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module K V] →
            [inst_3 : AddCommGroup V₂] → [inst_4 : Module K V₂] → (V →ₗ[K] V₂) → (V₂ →ₗ[K] V) → Prop
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.findFinIdx?.loop : {α : Type u} → (α → Bool) → (as : Array α) → ℕ → Option (Fin as.size)
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
/-- The difference `f m₁ - f m₂` is controlled in terms of `‖f‖` and `‖m₁ - m₂‖`, precise version.
For a less precise but more usable version, see `norm_image_sub_le`. The bound reads
`‖f m - f m'‖ ≤
  ‖f‖ * ‖m 1 - m' 1‖ * max ‖m 2‖ ‖m' 2‖ * max ‖m 3‖ ‖m' 3‖ * ... * max ‖m n‖ ‖m' n‖ + ...`,
where the other terms in the sum are the same products where `1` is replaced by any `i`.  -/
ContinuousAlternatingMap.norm_image_sub_le' : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] (f : E [⋀^ι]→L[𝕜] F) (m₁ m₂ : ι → E),
  ‖f m₁ - f m₂‖ ≤ ‖f‖ * ∑ i, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.add_neg : ∀ {R : Type u_3} [inst : Ring R] (a b : R), a + -b = a - b
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
isTranscendenceBasis_image : ∀ {R : Type u_3} {A : Type u_5} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {ι : Type u_7}
  {s : Set ι} {f : ι → A}, Set.InjOn f s → ((IsTranscendenceBasis R fun x => f ↑x) ↔ IsTranscendenceBasis R fun x => ↑x)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner
/-- The two definitions of the conditional expectation `condExp` and `condLExp` (for Bochner and
Lebesgue integrals respectively) agree almost everywhere.  -/
MeasureTheory.condLExp_enorm : ∀ {𝓧 : Type u_1} (m : MeasurableSpace 𝓧) {m𝓧 : MeasurableSpace 𝓧} {μ : MeasureTheory.Measure 𝓧} {f : 𝓧 → ℝ},
  MeasureTheory.Integrable f μ → 0 ≤ᵐ[μ] f → μ⁻[fun x => ‖f x‖ₑ | m] =ᵐ[μ] fun x => ‖μ[f | m] x‖ₑ
-- Mathlib.CategoryTheory.Adjunction.CompositionIso
CategoryTheory.Adjunction.leftAdjointCompIso_id_comp : ∀ {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₁] {F₀₀' : CategoryTheory.Functor C₀ C₀}
  {F₀'₁ : CategoryTheory.Functor C₀ C₁} {G₀'₀ : CategoryTheory.Functor C₀ C₀} {G₁₀' : CategoryTheory.Functor C₁ C₀}
  (adj₀₀' : F₀₀' ⊣ G₀'₀) (adj₀'₁ : F₀'₁ ⊣ G₁₀') (e₀₀'₁ : G₁₀'.comp G₀'₀ ≅ G₁₀')
  (e₀'₀ : G₀'₀ ≅ CategoryTheory.Functor.id C₀),
  e₀₀'₁ = G₁₀'.isoWhiskerLeft e₀'₀ ≪≫ G₁₀'.rightUnitor →
    adj₀₀'.leftAdjointCompIso adj₀'₁ adj₀'₁ e₀₀'₁ =
      CategoryTheory.Functor.isoWhiskerRight (adj₀₀'.leftAdjointIdIso e₀'₀) F₀'₁ ≪≫ F₀'₁.leftUnitor
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.instCoeFunForallProd : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] → {proj : Z → B} → CoeFun (Bundle.Pretrivialization F proj) fun x => Z → B × F
-- Mathlib.Tactic.FinCases
/-- `fin_cases h` performs case analysis on a hypothesis of the form
`h : A`, where `[Fintype A]` is available, or
`h : a ∈ A`, where `A : Finset X`, `A : Multiset X` or `A : List X`.

As an example, in
```
example (f : ℕ → Prop) (p : Fin 3) (h0 : f 0) (h1 : f 1) (h2 : f 2) : f p.val := by
  fin_cases p; simp
  all_goals assumption
```
after `fin_cases p; simp`, there are three goals, `f 0`, `f 1`, and `f 2`.
 -/
Lean.Elab.Tactic.finCases : Lean.ParserDescr
-- Mathlib.RingTheory.Finiteness.Cofinite
/-- The top submodule is CoFG.  -/
Submodule.CoFG.top : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M], ⊤.CoFG
-- Mathlib.RingTheory.Lasker
InfIrred.isPrimary : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsNoetherian R M]
  {N : Submodule R M}, InfIrred N → N.IsPrimary
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
Matrix.invOf_fromBlocks₂₂_eq : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α)
  (D : Matrix n n α) [inst_5 : Invertible D] [inst_6 : Invertible (A - B * ⅟D * C)]
  [inst_7 : Invertible (Matrix.fromBlocks A B C D)],
  ⅟(Matrix.fromBlocks A B C D) =
    Matrix.fromBlocks (⅟(A - B * ⅟D * C)) (-(⅟(A - B * ⅟D * C) * B * ⅟D)) (-(⅟D * C * ⅟(A - B * ⅟D * C)))
      (⅟D + ⅟D * C * ⅟(A - B * ⅟D * C) * B * ⅟D)
-- Mathlib.CategoryTheory.Enriched.Opposite
/-- Unfold the definition of composition in the enriched opposite category.  -/
CategoryTheory.eComp_op_eq : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V]
  [inst_2 : CategoryTheory.BraidedCategory V] {C : Type u} [inst_3 : CategoryTheory.EnrichedCategory V C] (x y z : Cᵒᵖ),
  CategoryTheory.eComp V z y x =
    CategoryTheory.CategoryStruct.comp
      (β_ (Opposite.unop y ⟶[V] Opposite.unop z) (Opposite.unop x ⟶[V] Opposite.unop y)).hom
      (CategoryTheory.eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z))
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.map_isIso : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : β → C}
  [inst_1 : CategoryTheory.Limits.HasCoproductsOfShape β C] (p : (b : β) → f b ⟶ g b)
  [∀ (b : β), CategoryTheory.IsIso (p b)], CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.map p)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.coe_LpSubmodule : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedRing 𝕜] [inst_2 : Module 𝕜 E] [inst_3 : IsBoundedSMul 𝕜 E],
  (MeasureTheory.Lp.LpSubmodule 𝕜 E p μ).toAddSubgroup = MeasureTheory.Lp E p μ
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.instSemilatticeInfFiniteIndexNormalSubgroup : {G : Type u_1} → [inst : Group G] → SemilatticeInf (FiniteIndexNormalSubgroup G)
-- Mathlib.Analysis.Normed.Group.Ultra
/-- Nonarchimedean norm of a sum is less than or equal to the largest norm of a term
in the sum.  -/
Finset.nnnorm_sum_le_sup_nnnorm : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedAddCommGroup M] [IsUltrametricDist M] (s : Finset ι) (f : ι → M),
  ‖∑ i ∈ s, f i‖₊ ≤ s.sup fun x => ‖f x‖₊
-- Mathlib.Data.Nat.Prime.Basic
Nat.Prime.dvd_of_dvd_pow : ∀ {p m n : ℕ}, Nat.Prime p → p ∣ m ^ n → p ∣ m
-- Mathlib.Data.Set.Card
/-- This is the same as `ncard_sdiff'` but we require `s` to be finite instead.  -/
Set.ncard_sdiff : ∀ {α : Type u_1} {s t : Set α}, s ⊆ t → autoParam s.Finite Set.ncard_sdiff._auto_1 → (t \ s).ncard = t.ncard - s.ncard
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.instSMulInvariantMeasureHausdorffMeasureOfIsIsometricSMul : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {α : Type u_4}
  [inst_3 : Group α] [inst_4 : MulAction α X] [IsIsometricSMul α X] {d : ℝ},
  MeasureTheory.SMulInvariantMeasure α X (MeasureTheory.Measure.hausdorffMeasure d)
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Functor.homObjEquiv_symm_apply_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G A : CategoryTheory.Functor C (Type w))
  (a : CategoryTheory.MonoidalCategoryStruct.tensorObj F A ⟶ G) (X : C) (y : A.obj X),
  ((F.homObjEquiv G A).symm a).app X y = TypeCat.ofHom fun x => (CategoryTheory.ConcreteCategory.hom (a.app X)) (x, y)
-- Mathlib.Analysis.Convex.Side
AffineSubspace.setOfPred_sOppSide_eq_image2 : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x p : P},
  x ∉ s → p ∈ s → {y | s.SOppSide x y} = Set.image2 (fun t q => t • (x -ᵥ p) +ᵥ q) (Set.Iio 0) ↑s
-- Lean.Parser.Term
Lean.Parser.Term.fun : Lean.Parser.Parser
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.vecMulLinear_apply : ∀ {R : Type u_1} [inst : Semiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype m] (M : Matrix m n R) (x : m → R),
  M.vecMulLinear x = Matrix.vecMul x M
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonInlayHintLabel : Lean.FromJson Lean.Lsp.InlayHintLabel
-- Mathlib.CategoryTheory.Limits.Indization.Category
/-- The canonical inclusion of ind-objects into presheaves.  -/
CategoryTheory.Ind.inclusion : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor (CategoryTheory.Ind C) (CategoryTheory.Functor Cᵒᵖ (Type v))
-- Mathlib.InformationTheory.Coding.KraftMcMillan
_private.Mathlib.InformationTheory.Coding.KraftMcMillan.0.InformationTheory.sum_pow_length_filter_eq_le_card_mul : ∀ {α : Type u_1} [inst : Fintype α] {T : Finset (List α)} {s : ℕ},
  ∑ x ∈ T with x.length = s, (1 / ↑(Fintype.card α)) ^ x.length ≤ ↑(Fintype.card α) ^ s * (1 / ↑(Fintype.card α)) ^ s
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.algebraMap_root'In_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_6)
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [inst_7 : Module S N] [inst_8 : IsScalarTower S R N]
  [inst_9 : FaithfulSMul S R] [inst_10 : P.IsValuedIn S] (i : ι) (x : ↥(P.corootSpan S)),
  (algebraMap S R) ((P.root'In S i) x) = (P.root' i) ↑x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_modify_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {fallback : β k} {f : β k → β k},
  (t.modify k f).getD k fallback = (Option.map f (t.get? k)).getD fallback
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.isIso_map_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] [L.IsLocalization P.isoModSerre] [inst_5 : CategoryTheory.Preadditive D] [L.Additive]
  {X Y : C} (f : X ⟶ Y), CategoryTheory.IsIso (L.map f) ↔ P.isoModSerre f
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Iter.toArray_eq_match_step.match_1.splitter : {α β : Type u_1} →
  (motive : Std.IterStep (Std.Iter β) β → Sort u_2) →
    (x : Std.IterStep (Std.Iter β) β) →
      ((it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out)) →
        ((it' : Std.Iter β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.Topology.MetricSpace.Thickening
Metric.frontier_cthickening_disjoint : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (A : Set α),
  Pairwise (Function.onFun Disjoint fun r => frontier (Metric.cthickening (↑r) A))
-- Mathlib.Data.Nat.Factorization.Divisors
Nat.properDivisors_eq_image_Iio_factorization_prod_pow : ∀ {n : ℕ}, n.properDivisors = Finset.image (fun x => x.prod fun x1 x2 => x1 ^ x2) (Finset.Iio n.factorization)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.instIsCancelSMulSubtypeMem : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : SMul R M] [inst_1 : SetLike S M] [hS : SMulMemClass S R M] (s : S)
  [IsCancelSMul R M], IsCancelSMul R ↥s
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Bounded.Receiver.mk : {α : Type} → Std.Mutex (Std.Bounded.State✝ α) → ℕ → Std.Bounded.Receiver✝ α
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey!_alter_eq_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] [inst_1 : Inhabited α] {k : α} {f : Option (β k) → Option (β k)},
  (t.alter k f).isEmpty = false →
    ((t.alter k f).maxKey! = k ↔ (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.polar_add_right : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticMap R M N) (x y y' : M),
  QuadraticMap.polar (⇑Q) x (y + y') = QuadraticMap.polar (⇑Q) x y + QuadraticMap.polar (⇑Q) x y'
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
CategoryTheory.Functor.HasLeftDerivedFunctor.hasRightKanExtension' : ∀ {C : Type u_1} {H : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_5, u_2} H} {F : CategoryTheory.Functor C H}
  {W : CategoryTheory.MorphismProperty C} [self : F.HasLeftDerivedFunctor W], W.Q.HasRightKanExtension F
-- Mathlib.Data.EReal.Inv
EReal.coe_inv : ∀ (x : ℝ), ↑x⁻¹ = (↑x)⁻¹
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.viaFintypeEmbedding_sign : ∀ {α : Type u} [inst : DecidableEq α] {β : Type v} [inst_1 : Fintype α] [inst_2 : Fintype β] [inst_3 : DecidableEq β]
  (e : Equiv.Perm α) (f : α ↪ β), Equiv.Perm.sign (e.viaFintypeEmbedding f) = Equiv.Perm.sign e
-- Init.Data.Array.MinMax
Array.get_max? : ∀ {α : Type u_1} [inst : Max α] {xs : Array α} {h : xs.max?.isSome = true}, xs.max?.get h = xs.max ⋯
-- Mathlib.Data.Int.Init
/-- Inductively define a function on `ℤ` by defining it at `b`, for the `succ` of a number greater
than `b`, and the `pred` of a number less than `b`.  -/
Int.inductionOn' : {motive : ℤ → Sort u_1} →
  (z b : ℤ) →
    motive b → ((k : ℤ) → b ≤ k → motive k → motive (k + 1)) → ((k : ℤ) → k ≤ b → motive k → motive (k - 1)) → motive z
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get!_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → (t₁ ∩ t₂).get! k = default
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.find?.eq_1 : ∀ {α : Type u_1} (cut : α → Ordering), RBTree.RBNode.find? cut RBTree.RBNode.nil = none
-- Mathlib.Topology.Closure
interior_union_of_disjoint_closure : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X},
  Disjoint (closure s) (closure t) → interior (s ∪ t) = interior s ∪ interior t
-- Mathlib.Computability.Partrec
Computable.map_decode_iff : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α → β → σ}, (Computable₂ fun a n => Option.map (f a) (Encodable.decode n)) ↔ Computable₂ f
-- Mathlib.Data.Set.Image
Set.range_quotient_lift_on' : ∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α} {s : Setoid ι} (hf : ∀ (a b : ι), s a b → f a = f b),
  (Set.range fun x => x.liftOn' f hf) = Set.range f
-- Lean.Server.ServerTask
Lean.Server.ServerTask.IO.bindTaskCheap : {α : Type u_1} →
  {β : Type} →
    Lean.Server.ServerTask α →
      (α → IO (Lean.Server.ServerTask (Except IO.Error β))) → BaseIO (Lean.Server.ServerTask (Except IO.Error β))
-- Std.Sync.StreamMap
Std.AnyAsyncStream.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] {t : Type} [inst_1 : Std.Async.IO.AsyncStream t α] (a : t),
  sizeOf (Std.AnyAsyncStream.mk a) = 1 + sizeOf t + sizeOf inst_1 + sizeOf a
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_eq_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : LawfulBEq α]
  {a : α}, Std.ExtDHashMap.Const.get? m a = m.get? a
-- Init.Data.Format.Basic
Std.Format.nil.sizeOf_spec : sizeOf Std.Format.nil = 1
-- Mathlib.Algebra.Polynomial.BigOperators
/-- **Alias** of `Polynomial.natDegree_finsetProd_X_sub_C_eq_card`. -/
Polynomial.natDegree_finset_prod_X_sub_C_eq_card : ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {α : Type u_1} (s : Finset α) (f : α → R),
  (∏ a ∈ s, (Polynomial.X - Polynomial.C (f a))).natDegree = s.card
-- Mathlib.Probability.BrownianMotion.Basic
/-- **Weak Markov property**: If `B` is a pre-Brownian motion, then
`B (t₀ + t) - B t₀` is a pre-Brownian motion which is independent from `(B t, t ≤ t₀)`.
This is the proof of independence, see `IsPreBrownianReal.shift` for the proof
that it is pre-Brownian.  -/
ProbabilityTheory.IsPreBrownianReal.indepFun_shift : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω},
  ProbabilityTheory.IsPreBrownianReal B P →
    ∀ (t₀ : NNReal), ProbabilityTheory.IndepFun (fun ω t => B (t₀ + t) ω - B t₀ ω) (fun ω t => B (↑t) ω) P
-- Aesop.RuleTac.Forward.Basic
Aesop.instInhabitedForwardHypData : Inhabited Aesop.ForwardHypData
-- Lean.DocString.Markdown
/-- Concatenates an array of "block" line arrays into one line array, with a single empty separator line
between adjacent non-empty blocks. Empty input blocks are skipped.
 -/
Lean.Doc.joinBlocks : Array (Array String) → Array String
-- Mathlib.Order.WithBot
WithBot.eq_of_forall_coe_le_iff : ∀ {α : Type u_1} [inst : PartialOrder α] {x y : WithBot α} [NoBotOrder α], (∀ (a : α), ↑a ≤ x ↔ ↑a ≤ y) → x = y
-- Mathlib.CategoryTheory.Monad.Algebra
/-- The coassociativity axiom associated to a coalgebra.  -/
CategoryTheory.Comonad.Coalgebra.coassoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} (self : G.Coalgebra),
  CategoryTheory.CategoryStruct.comp self.a (G.δ.app self.A) = CategoryTheory.CategoryStruct.comp self.a (G.map self.a)
-- Mathlib.Order.Filter.Ultrafilter.Basic
Ultrafilter.eventually_exists_iff : ∀ {α : Type u} {β : Type v} {f : Ultrafilter α} [Finite β] {P : β → α → Prop},
  (∀ᶠ (i : α) in ↑f, ∃ a, P a i) ↔ ∃ a, ∀ᶠ (i : α) in ↑f, P a i
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
CategoryTheory.SpectralSequence.instCategory : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_3, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {κ : Type u_2} →
        {c : ℤ → ComplexShape κ} →
          {r₀ : ℤ} →
            CategoryTheory.Category.{max u_2 u_3, max (max u_3 u_2) u_1} (CategoryTheory.SpectralSequence C c r₀)
-- Mathlib.FieldTheory.Finite.Basic
CharP.sq_add_sq : ∀ (R : Type u_3) [inst : Ring R] [IsDomain R] (p : ℕ) [NeZero p] [CharP R p] (x : ℤ), ∃ a b, ↑a ^ 2 + ↑b ^ 2 = ↑x
-- Mathlib.GroupTheory.Perm.List
List.formPerm_mem_iff_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α} {x : α}, l.formPerm x ∈ l ↔ x ∈ l
-- Mathlib.CategoryTheory.SingleObj
MulEquiv.toSingleObjEquiv_functor_map : ∀ {M : Type u} {N : Type v} [inst : Monoid M] [inst_1 : Monoid N] (e : M ≃* N) {X Y : CategoryTheory.SingleObj M}
  (a : M), e.toSingleObjEquiv.functor.map a = e a
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.subgraphOfAdj_le_iff : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v) (H : G.Subgraph), G.subgraphOfAdj h ≤ H ↔ H.Adj u v
-- Mathlib.Analysis.Convex.Intrinsic
intrinsicClosure_idem : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] (s : Set P),
  intrinsicClosure 𝕜 (intrinsicClosure 𝕜 s) = intrinsicClosure 𝕜 s
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.isTheta_zero_right : ∀ {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} [inst : SeminormedAddCommGroup F'] [inst_1 : NormedAddCommGroup E'']
  {f'' : α → E''} {l : Filter α}, (f'' =Θ[l] fun x => 0) ↔ f'' =ᶠ[l] 0
-- Mathlib.Data.Fin.Tuple.Embedding
Function.Embedding.embFinTwo_apply_zero : ∀ {α : Type u_1} {a b : α} (h : a ≠ b), (Function.Embedding.embFinTwo h) 0 = a
-- Mathlib.NumberTheory.LucasLehmer
/-- Tail-recursive version of `sModNat`.  -/
LucasLehmer.norm_num_ext.sModNatTR : ℕ → ℕ → ℕ
-- Mathlib.CategoryTheory.Monoidal.Ring
/-- The underlying object in the ambient monoidal category  -/
CategoryTheory.CommRingObjCat.X : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.CommRingObjCat C → C
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
/-- The equivalence `ToType (⊤_ C) ≃ PUnit` when `C` is a concrete category.  -/
CategoryTheory.Limits.Concrete.terminalEquiv : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_1} →
      {CC : C → Type w} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory C FC] →
            [inst_3 : CategoryTheory.Limits.HasTerminal C] →
              [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)] →
                CategoryTheory.ToType (⊤_ C) ≃ PUnit.{w + 1}