mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Coalgebra.Basic
Coalgebra.Repr.mk : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid A] →
        [inst_2 : Module R A] →
          [inst_3 : CoalgebraStruct R A] →
            {a : A} →
              {ι : Type u_1} →
                (index : Finset ι) →
                  (left right : ι → A) →
                    ∑ i ∈ index, left i ⊗ₜ[R] right i = CoalgebraStruct.comul a → Coalgebra.Repr R a ι
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.finMeasSupp_iff_support : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : Zero β] {μ : MeasureTheory.Measure α}
  {f : MeasureTheory.SimpleFunc α β}, f.FinMeasSupp μ ↔ μ (Function.support ⇑f) < ⊤
-- Init.Data.List.Lex
List.instTransLeOfIsLinearOrderOfLawfulOrderLT : {α : Type u_1} →
  [inst : LT α] →
    [inst_1 : LE α] →
      [Std.IsLinearOrder α] →
        [Std.LawfulOrderLT α] → Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.B_diag : ∀ (n : ℕ) (i : Fin n), CartanMatrix.B n i i = 2
-- Mathlib.Data.Sym.Basic
/-- The unique element in `Sym α 0`.  -/
Sym.nil : {α : Type u_1} → Sym α 0
-- Mathlib.CategoryTheory.Shift.Localization
/-- When `L : C ⥤ D` is a localization functor with respect to a morphism property `W`
that is compatible with the shift by a monoid `A` on `C`, this is the induced
shift on the category `D`.  -/
CategoryTheory.HasShift.localized : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            [L.IsLocalization W] →
              (A : Type w) →
                [inst_3 : AddMonoid A] →
                  [inst_4 : CategoryTheory.HasShift C A] → [W.IsCompatibleWithShift A] → CategoryTheory.HasShift D A
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.associator_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) {Z : C} (h : Y₁ ⨯ Y₂ ⨯ Y₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.Limits.prod.map f₁ f₂) f₃)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator Y₁ Y₂ Y₃).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator X₁ X₂ X₃).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f₁ (CategoryTheory.Limits.prod.map f₂ f₃)) h)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
_private.Mathlib.Analysis.SpecialFunctions.Pow.NNReal.0.Mathlib.Meta.Positivity.isFiniteM? : (x : Q(ENNReal)) → Lean.MetaM (Option Q(«$x» ≠ ⊤))
-- Mathlib.Topology.MetricSpace.HausdorffDimension
dimH_countable : ∀ {X : Type u_2} [inst : EMetricSpace X] {s : Set X}, s.Countable → dimH s = 0
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k : α} {h' : k ∈ Std.TreeMap.filter f t}, (Std.TreeMap.filter f t).getKey k h' = t.getKey k ⋯
-- Mathlib.Topology.MetricSpace.Ultra.Basic
IsUltrametricDist.closedBall_subset_trichotomy : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] [IsUltrametricDist X] (x y : X) (r s : ℝ),
  Metric.closedBall x r ⊆ Metric.closedBall y s ∨
    Metric.closedBall y s ⊆ Metric.closedBall x r ∨ Disjoint (Metric.closedBall x r) (Metric.closedBall y s)
-- Mathlib.Topology.NhdsSet
nhdsSet_empty : ∀ {X : Type u_2} [inst : TopologicalSpace X], nhdsSet ∅ = ⊥
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.congr_fun : ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {f g : α →+* β},
  f = g → ∀ (x_2 : α), f x_2 = g x_2
-- Std.Tactic.BVDecide.LRAT.Parser
_private.Std.Tactic.BVDecide.LRAT.Parser.0.Std.Tactic.BVDecide.LRAT.lratProofToBinary.addInt : ByteArray → ℤ → ByteArray
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
/-- Internal implementation detail of the iterator library.  -/
Std.Iterators.Types.FilterMap.inner : {α β γ : Type w} →
  {m : Type w → Type w'} →
    {n : Type w → Type w''} →
      {lift : ⦃α : Type w⦄ → m α → n α} →
        {f : β → Std.Iterators.PostconditionT n (Option γ)} → Std.Iterators.Types.FilterMap α m n lift f → Std.IterM m β
-- Mathlib.Topology.Algebra.IsUniformGroup.Constructions
isUniformAddGroup_iInf : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Sort u_4} {us' : ι → UniformSpace G},
  (∀ (i : ι), IsUniformAddGroup G) → IsUniformAddGroup G
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.ι_range_map_involute : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M),
  Submodule.map CliffordAlgebra.involute.toLinearMap (CliffordAlgebra.ι Q).range = (CliffordAlgebra.ι Q).range
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.fillNones.match_1.splitter : {α : Type u_1} →
  (motive : List (Option α) → List α → Sort u_2) →
    (x : List (Option α)) →
      (x_1 : List α) →
        ((x : List α) → motive [] x) →
          ((a : α) → (as : List (Option α)) → (as' : List α) → motive (some a :: as) as') →
            ((as : List (Option α)) → motive (none :: as) []) →
              ((as : List (Option α)) → (a : α) → (as' : List α) → motive (none :: as) (a :: as')) → motive x x_1
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.PrepathObject.RightHomotopy.h₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {Y : C} {P : HomotopicalAlgebra.PrepathObject Y} {X : C}
  {f g : X ⟶ Y} (self : P.RightHomotopy f g), CategoryTheory.CategoryStruct.comp self.h P.p₁ = g
-- Lean.Elab.Tactic.RCases
/-- A tuple constructor like `⟨p1, p2, p3⟩`  -/
Lean.Elab.Tactic.RCases.RCasesPatt.tuple : Lean.Syntax → List Lean.Elab.Tactic.RCases.RCasesPatt → Lean.Elab.Tactic.RCases.RCasesPatt
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.mk : {R : Type u_1} →
  [inst : CommMonoid R] →
    {R' : Type u_2} →
      [inst_1 : CommMonoidWithZero R'] →
        (toMonoidHom : R →* R') → (∀ (a : R), ¬IsUnit a → (↑toMonoidHom).toFun a = 0) → MulChar R R'
-- Mathlib.Tactic.DeriveEncodable
/-- Constructs a proof that the functions created by `mkFromSFuns` are left inverses
of the ones created by `mkToSFuns`.
 -/
_private.Mathlib.Tactic.DeriveEncodable.0.Mathlib.Deriving.Encodable.mkInjThms : Lean.Elab.Deriving.Context → Array Lean.Name → Array Lean.Name → Lean.Elab.TermElabM (Lean.TSyntax `command)
-- Mathlib.Order.SupClosed
SupClosed.iSup_mem_of_nonempty : ∀ {ι : Sort u_1} {α : Type u_3} [inst : ConditionallyCompleteLattice α] {f : ι → α} {s : Set α} [Finite ι] [Nonempty ι],
  SupClosed s → (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- If we take the path along the spine of the `j`th face of a `spineToSimplex`,
an arrow `i` with `i + 1 > j` can be identified with arrow `i + 1` in the
original path.  -/
SSet.StrictSegal.spine_δ_arrow_gt : ∀ {X : SSet} (sx : X.StrictSegal) {n : ℕ} (f : X.Path (n + 1)) {i : Fin n} {j : Fin (n + 2)},
  j < i.succ.castSucc →
    (X.spine n
            ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X j)) (sx.spineToSimplex f))).arrow
        i =
      f.arrow i.succ
-- Init.Data.Array.Monadic
Array.foldlM_map : ∀ {m : Type u_1 → Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {α : Type u_1} {stop : ℕ} [inst : Monad m] {f : β₁ → β₂}
  {g : α → β₂ → m α} {xs : Array β₁} {init : α} {w : stop = xs.size},
  Array.foldlM g init (Array.map f xs) 0 stop = Array.foldlM (fun x y => g x (f y)) init xs 0 stop
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.S_eval_two : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ), Polynomial.eval 2 (Polynomial.Chebyshev.S R n) = ↑n + 1
-- Mathlib.Algebra.Ring.Periodic
/-- If a function is `antiperiodic` with antiperiod `c`, then it is also `Periodic` with period
`2 • c`.  -/
Function.Antiperiodic.periodic : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddMonoid α] [inst_1 : InvolutiveNeg β],
  Function.Antiperiodic f c → Function.Periodic f (2 • c)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalarsId'App_hom_naturality : ∀ {R : Type u₁} [inst : Ring R] (f : R →+* R) (hf : f = RingHom.id R) {M N : ModuleCat R} (φ : M ⟶ N),
  CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars f).map φ)
      (ModuleCat.restrictScalarsId'App f hf N).hom =
    CategoryTheory.CategoryStruct.comp (ModuleCat.restrictScalarsId'App f hf M).hom φ
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.unitors_equal : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a : B},
  (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.id a)).hom =
    (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.id a)).hom
-- Lean.CoreM
/-- Creates a user-accessible unique name of the following structure:
```
<name prefix>.<infix>_<numeric components>_...
```
Uniqueness is guaranteed for the current branch of elaboration. When entering parallelism and other
branching elaboration steps, `mkChild` must be used (automatically done in `wrapAsync*`).
 -/
Lean.DeclNameGenerator.mkUniqueName : Lean.Environment → Lean.DeclNameGenerator → Lean.Name → Lean.Name × Lean.DeclNameGenerator
-- Mathlib.Algebra.Module.Injective
Module.Baer.extensionOfMax_is_max : ∀ {R : Type u} [inst : Ring R] {Q : Type v} [inst_1 : AddCommGroup Q] [inst_2 : Module R Q] {M : Type u_1}
  {N : Type u_2} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N]
  (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [inst_7 : Fact (Function.Injective ⇑i)] (a : Module.Baer.ExtensionOf i f),
  Module.Baer.extensionOfMax i f ≤ a → a = Module.Baer.extensionOfMax i f
-- Mathlib.MeasureTheory.VectorMeasure.WithDensityVec
MeasureTheory.VectorMeasure.restrict_withDensity : ∀ {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E} {B : E →L[ℝ] F →L[ℝ] G} {s : Set X},
  μ.Integrable f → (μ.withDensity f B).restrict s = (μ.restrict s).withDensity f B
-- Mathlib.Algebra.Order.SuccPred
Order.not_isSuccLimit_natCast : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddMonoidWithOne α] [SuccAddOrder α] [IsBotZeroClass α] (n : ℕ),
  ¬Order.IsSuccLimit ↑n
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Filtered
CategoryTheory.Limits.has_filtered_colimits_op_of_has_cofiltered_limits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [CategoryTheory.Limits.HasCofilteredLimitsOfSize.{v₂, u₂, v₁, u₁} C],
  CategoryTheory.Limits.HasFilteredColimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] {f : (a : α) → β a → γ a} {k : α} {h' : k ∈ Std.DTreeMap.map f t},
  (Std.DTreeMap.map f t).getKey k h' = t.getKey k ⋯
-- Mathlib.Data.Sum.Interval
Sum.Lex.Ico_inl_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : LocallyFiniteOrderTop α] [inst_5 : LocallyFiniteOrderBot β] (a : α) (b : β),
  Finset.Ico (Sum.inlₗ a) (Sum.inrₗ b) = Finset.map toLex.toEmbedding ((Finset.Ici a).disjSum (Finset.Iio b))
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabQuotedName : Lean.Elab.Term.TermElab
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.get?.eq_def : ∀ {α : Type u} {δ : Type w} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α fun x => δ) (k : α),
  Std.DTreeMap.Internal.Impl.Const.get? t k =
    match t with
    | Std.DTreeMap.Internal.Impl.leaf => none
    | Std.DTreeMap.Internal.Impl.inner size k' v' l r =>
      match compare k k' with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.Const.get? l k
      | Ordering.gt => Std.DTreeMap.Internal.Impl.Const.get? r k
      | Ordering.eq => some v'
-- Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Complex.GammaSeq_add_one_left : ∀ (s : ℂ) {n : ℕ}, n ≠ 0 → (s + 1).GammaSeq n / s = ↑n / (↑n + 1 + s) * s.GammaSeq n
-- Mathlib.Analysis.Complex.Exponential
Real.one_le_exp_iff : ∀ {x : ℝ}, 1 ≤ Real.exp x ↔ 0 ≤ x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.constGetD_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {fallback : β},
  m₁.Equiv m₂ → Std.DHashMap.Const.getD m₁ k fallback = Std.DHashMap.Const.getD m₂ k fallback
-- Mathlib.Computability.Primrec.List
Primrec.list_getD : ∀ {α : Type u_1} [inst : Primcodable α] (d : α), Primrec₂ fun l n => l.getD n d
-- Init.Data.String.Defs
String.instAssociativeHAppend : Std.Associative fun x1 x2 => x1 ++ x2
-- Mathlib.Probability.StrongLaw
MeasureTheory.AEStronglyMeasurable.integrable_truncation : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.AEStronglyMeasurable f μ → ∀ {A : ℝ}, MeasureTheory.Integrable (ProbabilityTheory.truncation f A) μ
-- Init.Data.List.Sublist
List.subset_append_left : ∀ {α : Type u_1} (l₁ l₂ : List α), l₁ ⊆ l₁ ++ l₂
-- Mathlib.Tactic.Positivity.Core
Mathlib.Meta.Positivity.Strictness.none.sizeOf_spec : ∀ {u : Lean.Level} {α : Q(Type u)} {zα : Q(Zero «$α»)} {e : Q(«$α»)} {pα? : Option Q(PartialOrder «$α»)},
  sizeOf Mathlib.Meta.Positivity.Strictness.none = 1 + sizeOf pα?
-- Mathlib.Algebra.Group.Action.End
MulAction.coe_toPermHom : ∀ (G : Type u_1) (α : Type u_5) [inst : Group G] [inst_1 : MulAction G α], ⇑(MulAction.toPermHom G α) = MulAction.toPerm
-- Mathlib.MeasureTheory.Function.UniformIntegrable
MeasureTheory.tendsto_indicator_ge : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] (f : α → β) (x : α),
  Filter.Tendsto (fun M => {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) Filter.atTop (nhds 0)
-- Mathlib.Order.WellFoundedSet
Set.IsPWO.exists_minimalFor : ∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] (f : ι → α) (s : Set ι),
  (f '' s).IsPWO → s.Nonempty → ∃ i, MinimalFor (fun x => x ∈ s) f i
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- `mapIdIso` gives rise to the oplax unity constraint  -/
CategoryTheory.OplaxFunctor.PseudoCore.mapIdIso_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F : CategoryTheory.OplaxFunctor B C} (self : F.PseudoCore) {a : B}, (self.mapIdIso a).hom = F.mapId a
-- Mathlib.Algebra.CharP.Defs
/-- The exponential characteristic is positive.  -/
expChar_pos : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (q : ℕ) [ExpChar R q], 0 < q
-- Mathlib.Order.OmegaCompletePartialOrder
/-- Eta-expanded form of `OmegaCompletePartialOrder.ωScottContinuous.const` -/
OmegaCompletePartialOrder.ωScottContinuous.fun_const : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β] {x : β},
  OmegaCompletePartialOrder.ωScottContinuous fun x_1 => x
-- Mathlib.Data.Vector.Basic
/-- Monadic analog of `Vector.ofFn`.
Given a monadic function on `Fin n`, return a `Vector α n` inside the monad.  -/
List.Vector.mOfFn : {m : Type u → Type u_6} → [Monad m] → {α : Type u} → {n : ℕ} → (Fin n → m α) → m (List.Vector α n)
-- Mathlib.Data.Nat.Factorization.Basic
Nat.ordProj_mul_ordCompl_eq_self : ∀ (n p : ℕ), p ^ n.factorization p * (n / p ^ n.factorization p) = n
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_of_contains_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k a : α}
  {v : β k}, (t.insert k v).contains a = true → cmp k a ≠ Ordering.eq → t.contains a = true
-- Mathlib.Topology.UniformSpace.Defs
uniformContinuous_iff_eventually : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  UniformContinuous f ↔ ∀ r ∈ uniformity β, ∀ᶠ (x : α × α) in uniformity α, (f x.1, f x.2) ∈ r
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
CFC.conjSqrt_le_conjSqrt : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [inst_8 : SeparatelyContinuousMul A] {c a b : A},
  a ≤ b → (CFC.conjSqrt c) a ≤ (CFC.conjSqrt c) b
-- Init.Data.String.TakeDrop
/-- Removes leading and trailing whitespace from a string.

“Whitespace” is defined as characters for which `Char.isWhitespace` returns `true`.

Examples:

* `"abc".trimAscii == "abc".toSlice`

* `"   abc".trimAscii == "abc".toSlice`

* `"abc \t  ".trimAscii == "abc".toSlice`

* `"  abc   ".trimAscii == "abc".toSlice`

* `"abc\ndef\n".trimAscii == "abc\ndef".toSlice`
 -/
String.trimAscii : String → String.Slice
-- Mathlib.Topology.Algebra.ConstMulAction
AddOpposite.continuousConstVAdd : ∀ {M : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : VAdd M α] [ContinuousConstVAdd M α],
  ContinuousConstVAdd M αᵃᵒᵖ
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.any_filterMapM : ∀ {α β β' : Type w} {m : Type w → Type w'} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id]
  [inst_2 : Std.IteratorLoop α Id m] [inst_3 : Monad m] [inst_4 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [Std.LawfulIteratorLoop α Id m] {it : Std.Iter β} {f : β → m (Option β')} {p : β' → Bool},
  Std.IterM.any p (Std.Iter.filterMapM f it) =
    Std.IterM.anyM
      (fun x => do
        let __do_lift ← f x
        match __do_lift with
          | some fx => pure { down := p fx }
          | none => pure { down := false })
      (Std.Iter.mapM pure it)
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.ofList_flatten : ∀ {α : Type u_1} (xs : List (List α)), FreeMonoid.ofList xs.flatten = (List.map (⇑FreeMonoid.ofList) xs).prod
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.denoteS.eq_1 : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (k : ℤ),
  Lean.Grind.CommRing.Expr.denoteS ctx (Lean.Grind.CommRing.Expr.num k) = OfNat.ofNat k.natAbs
-- Mathlib.LinearAlgebra.Reflection
Module.preReflection_preReflection : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x : M}
  {f : Module.Dual R M} (y : M) (g : Module.Dual R M),
  f x = 2 →
    Module.preReflection ((Module.preReflection x f) y) ((Module.preReflection f ((Module.Dual.eval R M) x)) g) =
      Module.preReflection x f ∘ₗ Module.preReflection y g ∘ₗ Module.preReflection x f
-- Mathlib.ModelTheory.Semantics
_private.Mathlib.ModelTheory.Semantics.0.FirstOrder.Language.Term.restrictVarLeft.match_1.eq_3 : ∀ {L : FirstOrder.Language} {α : Type u_4} {β : Type u_6} [inst : DecidableEq α] {γ : Type u_3}
  (motive : (x : L.Term (α ⊕ γ)) → (↥x.varFinsetLeft → β) → Sort u_5) (l : ℕ) (F : L.Functions l)
  (ts : Fin l → L.Term (α ⊕ γ)) (f : ↥(FirstOrder.Language.func F ts).varFinsetLeft → β)
  (h_1 :
    (a : α) →
      (f : ↥(FirstOrder.Language.var (Sum.inl a)).varFinsetLeft → β) → motive (FirstOrder.Language.var (Sum.inl a)) f)
  (h_2 :
    (a : γ) →
      (_f : ↥(FirstOrder.Language.var (Sum.inr a)).varFinsetLeft → β) → motive (FirstOrder.Language.var (Sum.inr a)) _f)
  (h_3 :
    (l : ℕ) →
      (F : L.Functions l) →
        (ts : Fin l → L.Term (α ⊕ γ)) →
          (f : ↥(FirstOrder.Language.func F ts).varFinsetLeft → β) → motive (FirstOrder.Language.func F ts) f),
  (match FirstOrder.Language.func F ts, f with
    | FirstOrder.Language.var (Sum.inl a), f => h_1 a f
    | FirstOrder.Language.var (Sum.inr a), _f => h_2 a _f
    | FirstOrder.Language.func F ts, f => h_3 l F ts f) =
    h_3 l F ts f
-- Mathlib.MeasureTheory.Group.Integral
MeasureTheory.integrable_comp_sub_left : ∀ {G : Type u_4} {F : Type u_6} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.Measure G}
  [inst_2 : AddGroup G] [MeasurableAdd G] [MeasurableNeg G] (f : G → F) [μ.IsNegInvariant] [μ.IsAddLeftInvariant]
  (g : G), MeasureTheory.Integrable (fun t => f (g - t)) μ ↔ MeasureTheory.Integrable f μ
-- Mathlib.Order.Irreducible
InfPrime.inf_le : ∀ {α : Type u_2} [inst : SemilatticeInf α] {a b c : α}, InfPrime a → (b ⊓ c ≤ a ↔ b ≤ a ∨ c ≤ a)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.hom_ofHom : ∀ {X Y : Type u} [inst : AddGroup X] [inst_1 : TopologicalSpace X] [inst_2 : IsTopologicalAddGroup X]
  [inst_3 : CompactSpace X] [inst_4 : TotallyDisconnectedSpace X] [inst_5 : AddGroup Y] [inst_6 : TopologicalSpace Y]
  [inst_7 : IsTopologicalAddGroup Y] [inst_8 : CompactSpace Y] [inst_9 : TotallyDisconnectedSpace Y] (f : X →ₜ+ Y),
  ProfiniteAddGrp.Hom.hom (ProfiniteAddGrp.ofHom f) = f
-- Lean.Meta.Match.MatcherApp.Transform
/-- Constructor field fvars, i.e. the proper fvar subset of `args` (see example above).  -/
Lean.Meta.MatcherApp.TransformAltFVars.fields : Lean.Meta.MatcherApp.TransformAltFVars → Array Lean.Expr
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
/-- Divided powers on the codomain `B` of a surjective ring homomorphism `f` are compatible
with `f`.  -/
DividedPowers.Quotient.OfSurjective.dpow_apply' : ∀ {A : Type u_1} [inst : CommRing A] {I : Ideal A} (hI : DividedPowers I) {B : Type u_2} [inst_1 : CommRing B]
  {f : A →+* B},
  hI.IsSubDPIdeal (RingHom.ker f ⊓ I) →
    ∀ {n : ℕ} {a : A}, a ∈ I → DividedPowers.Quotient.OfSurjective.dpow hI f n (f a) = f (hI.dpow n a)
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- The restriction of an extension is the original.  -/
CategoryTheory.Presieve.restrict_extend : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X} {x : CategoryTheory.Presieve.FamilyOfElements P R},
  x.Compatible → CategoryTheory.Presieve.FamilyOfElements.restrict ⋯ x.sieveExtend = x
-- Mathlib.Order.Antisymmetrization
le_iff_lt_or_antisymmRel : ∀ {α : Type u_1} {a b : α} [inst : Preorder α], a ≤ b ↔ a < b ∨ AntisymmRel (fun x1 x2 => x1 ≤ x2) a b
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `A` and `B` are linearly disjoint over `F`, then the `Module.finrank` of
`A ⊔ B` is equal to the product of that of `A` and `B`.  -/
IntermediateField.LinearDisjoint.finrank_sup : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E},
  A.LinearDisjoint ↥B → Module.finrank F ↥(A ⊔ B) = Module.finrank F ↥A * Module.finrank F ↥B
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.CechNerveTerminalFrom.hasWidePullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasTerminal C] (ι : Type w)
  [CategoryTheory.Limits.HasFiniteProducts C] [Finite ι] (X : C),
  CategoryTheory.Limits.HasWidePullback (CategoryTheory.Arrow.mk (CategoryTheory.Limits.terminal.from X)).right
    (fun x => (CategoryTheory.Arrow.mk (CategoryTheory.Limits.terminal.from X)).left) fun x =>
    (CategoryTheory.Arrow.mk (CategoryTheory.Limits.terminal.from X)).hom
-- Std.Sync.CancellationToken
/-- Cancelled due to shutdown
 -/
Std.CancellationReason.shutdown : Std.CancellationReason
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.toLax_mapId' : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {b : B} (f : b ⟶ b)
  (hf : autoParam (f = CategoryTheory.CategoryStruct.id b) CategoryTheory.Pseudofunctor.toLax_mapId'._auto_1),
  F.toLax.mapId' f hf = (F.mapId' f hf).inv
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.opensRange_fromSpec : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U),
  AlgebraicGeometry.Scheme.Hom.opensRange hU.fromSpec = U