mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.hasColimit_of_domain_hasTerminal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  [CategoryTheory.Limits.HasTerminal J] {F : CategoryTheory.Functor J C}, CategoryTheory.Limits.HasColimit F
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Manifold.LocalPresentationAt.domChart_mem_maximalAtlas : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G}
  {M : Type u_10} {N : Type u_12} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop}
  (self : Manifold.LocalPresentationAt I J n f x P), self.domChart ∈ IsManifold.maximalAtlas I n M
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for shift right on `BitVec`.  -/
BitVec.reduceHShiftRight : Lean.Meta.Simp.DSimproc
-- Batteries.Data.Array.Scan
Array.getElem_scanr_zero : ∀ {α : Type u_1} {β : Type u_2} {init : β} {as : Array α} {f : α → β → β},
  (Array.scanr f init as)[0] = Array.foldr f init as
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp}
  [Inhabited α] {k k' : α} {f : β → β} {hc : k' ∈ Std.DTreeMap.Const.modify t k f},
  (Std.DTreeMap.Const.modify t k f).getKey k' hc = if cmp k k' = Ordering.eq then k else t.getKey k' ⋯
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LaxLeftLinear.μₗ_associativity_inv_assoc : ∀ {D : Type u_1} {D' : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} D]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] (F : CategoryTheory.Functor D D') {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C] [inst_3 : CategoryTheory.MonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  [inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'] [inst_6 : F.LaxLeftLinear C] (c c' : C) (d : D)
  {Z : D'}
  (h :
    F.obj
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj
          (CategoryTheory.MonoidalCategoryStruct.tensorObj c c') d) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c
        (CategoryTheory.Functor.LaxLeftLinear.μₗ F c' d))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxLeftLinear.μₗ F c
          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c' d))
        (CategoryTheory.CategoryStruct.comp
          (F.map (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' d).inv) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' (F.obj d)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxLeftLinear.μₗ F (CategoryTheory.MonoidalCategoryStruct.tensorObj c c') d) h)
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
/-- Monoid structure on additive submonoids of a semiring.  -/
AddSubmonoid.monoid : {R : Type u_2} → [inst : Semiring R] → Monoid (AddSubmonoid R)
-- Mathlib.Order.SuccPred.Archimedean
/-- **Alias** of `StrictMono.not_bddAbove_range_of_isSuccArchimedean`. -/
StrictMono.not_bddBelow_range_of_isSuccArchimedean : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [Nonempty α] [inst_2 : Preorder β] {f : α → β} [NoMaxOrder α]
  [inst_4 : SuccOrder β] [IsSuccArchimedean β], StrictMono f → ¬BddAbove (Set.range f)
-- Mathlib.Tactic.Convert
/-- `convert_to t` on a goal `⊢ t'` changes the goal to `⊢ t` and adds new goals for proving the
equality `t' = t` using congruence. The goals are created like `congr!` would.
Any remaining congruence goals come before the main goal.
Like `refine e`, any holes (`?_` or `?x`) in `t` that are not solved by unification are converted
into new goals, using the hole's name, if any, as the goal case name.
Like `congr!`, `convert_to` introduces variables while applying congruence rules. These can be
pattern-matched, like `rintro` would, using the `with` keyword.

`convert e`, where `e` is a term of type `t`, uses `e` to close the new main goal. In other words,
`convert e` works like `convert_to t; refine e`. Both tactics use the same options.

* `convert_to! t` uses default transparency, rather than reducible, when solving side goals.
* `convert_to ty at h` changes the type of the local hypothesis `h` to `ty`. If later local
  hypotheses or the goal depend on `h`, then `convert_to t at h` may leave a copy of `h`.
* `convert_to ← t` creates equality goals in the opposite direction (with the original goal type on
  the right).
* `convert_to t using n`, where `n` is a positive numeral, controls the depth with which congruence
  is applied. For example, if the main goal is `⊢ Prime (n + n + 1)`,
  then `convert_to Prime (2 * n + 1) using 2` results in one goal, `⊢ n + n = 2 * n`, and
  `convert_to Prime (2 * n + 1) using 3` (or more) results in two (impossible) goals
  `⊢ HAdd.hAdd = HMul.hMul` and `⊢ n = 2`.
  The default value for `n` is 1.
* `convert_to t with x ⟨y₁, y₂⟩ (z₁ | z₂)` names or pattern-matches the variables introduced by
  congruence rules, like `rintro x ⟨y₁, y₂⟩ (z₁ | z₂)` would.
* `convert_to (config := cfg) t` uses the configuration options in `cfg` to control the congruence
  rules (see `Congr!.Config`).
 -/
Mathlib.Tactic.convert_to! : Lean.ParserDescr
-- Init.Data.UInt.Lemmas
UInt32.neg_inj : ∀ {a b : UInt32}, -a = -b ↔ a = b
-- Mathlib.Algebra.Group.End
Equiv.swap_inv : ∀ {α : Type u_4} [inst : DecidableEq α] (x y : α), (Equiv.swap x y)⁻¹ = Equiv.swap x y
-- Mathlib.Topology.Order.Hom.Esakia
/-- Copy of an `EsakiaHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities.  -/
EsakiaHom.copy : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : Preorder α] →
        [inst_2 : TopologicalSpace β] →
          [inst_3 : Preorder β] → (f : EsakiaHom α β) → (f' : α → β) → f' = ⇑f → EsakiaHom α β
-- Mathlib.Order.Directed
/-- **Alias** of the forward direction of `directedOn_iff_isCodirectedOrder`. -/
DirectedOn.isCodirectedOrder : ∀ {α : Type u_1} [inst : LE α] {s : Set α}, DirectedOn (fun x1 x2 => x2 ≤ x1) s → IsCodirectedOrder ↑s
-- Mathlib.Data.Set.Finite.Basic
/-- **Alias** of the reverse direction of `Set.infinite_image_iff`. -/
Set.Infinite.image : ∀ {α : Type u} {β : Type v} {s : Set α} {f : α → β}, Set.InjOn f s → s.Infinite → (f '' s).Infinite
-- Init.MetaTypes
Lean.Meta.Command.ReduceConfig : Type
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.prev_π₁ : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} (c₂ : ComplexShape I₂)
  (c₁₂ : ComplexShape I₁₂) [inst : TotalComplexShape c₁ c₂ c₁₂] {i₁ i₁' : I₁},
  c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), c₁₂.prev (c₁.π c₂ c₁₂ (i₁', i₂)) = c₁.π c₂ c₁₂ (i₁, i₂)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
Lean.Meta.Grind.Arith.CommRing.noZeroDivisorsInst? : Lean.Meta.Grind.Arith.CommRing.RingM (Option Lean.Expr)
-- Mathlib.Combinatorics.Enumerative.DyckWord
/-- The semilength of a Dyck word is half of the number of `DyckStep`s in it, or equivalently
its number of `U`s.  -/
DyckWord.semilength : DyckWord → ℕ
-- Mathlib.Topology.Sets.CompactOpenCovered
IsCompactOpenCovered.id_iff_isOpen_and_isCompact : ∀ {S : Type u_1} {U : Set S} [inst : TopologicalSpace S], IsCompactOpenCovered (fun x => id) U ↔ IsOpen U ∧ IsCompact U
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.add_sub_zero : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {p r : R} {s : ↥S},
  p -ₒ s + (r -ₒ 0) = p + r -ₒ s
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.instNonUnitalNonAssocSemiring : {ι : Type u_1} →
  [DecidableEq ι] →
    (A : ι → Type u_2) →
      [inst : Add ι] →
        [inst_1 : (i : ι) → AddCommMonoid (A i)] →
          [DirectSum.GNonUnitalNonAssocSemiring A] → NonUnitalNonAssocSemiring (DirectSum ι fun i => A i)
-- Std.Time.DateTime.PlainDateTime
/-- Creates a new `PlainDateTime` by adjusting the `hour` component of its `time` to the given value.
 -/
Std.Time.PlainDateTime.withHours : Std.Time.PlainDateTime → Std.Time.Hour.Ordinal → Std.Time.PlainDateTime
-- Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
ProbabilityTheory.tendsto_choose_mul_pow_atTop : ∀ {p : ℕ → ℝ} {r : ℝ} (k : ℕ),
  Filter.Tendsto (fun n => ↑n * p n) Filter.atTop (nhds r) →
    Filter.Tendsto (fun n => ↑(n.choose k) * p n ^ k) Filter.atTop (nhds (r ^ k / ↑k.factorial))
-- Mathlib.Algebra.Ring.Defs
Distrib.toAdd : {R : Type u_1} → [self : Distrib R] → Add R
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.lift_eq_beth_natCast : ∀ {c : Cardinal.{u}} {n : ℕ}, Cardinal.lift.{v, u} c = Cardinal.beth ↑n ↔ c = Cardinal.beth ↑n
-- Mathlib.Topology.MetricSpace.Defs
/-- Build a new metric space from an old one where the bundled topological structure is provably
(but typically non-definitionaly) equal to some given topological structure.
See Note [forgetful inheritance].
See Note [reducible non-instances].
 -/
MetricSpace.replaceTopology : {γ : Type u_3} →
  [U : TopologicalSpace γ] →
    (m : MetricSpace γ) → U = PseudoMetricSpace.toUniformSpace.toTopologicalSpace → MetricSpace γ
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.TZif.mk.sizeOf_spec : ∀ (v1 : Std.Time.TimeZone.TZif.TZifV1) (v2 : Option Std.Time.TimeZone.TZif.TZifV2),
  sizeOf { v1 := v1, v2 := v2 } = 1 + sizeOf v1 + sizeOf v2
-- Mathlib.Tactic.MoveAdd
/-- `parseArrows` parses an input of the form `[a, ← b, _ * (1 : ℤ)]`, consisting of a list of
terms, each optionally preceded by the arrow `←`.
It returns an array of triples consisting of
* the `Expr`ession corresponding to the parsed term,
* the `Bool`ean `true` if the arrow is present in front of the term,
* the underlying `Syntax` of the given term.

E.g. convert `[a, ← b, _ * (1 : ℤ)]` to
``[(a, false, `(a)), (b, true, `(b)), (_ * 1, false, `(_ * 1))]``.
 -/
Mathlib.MoveAdd.parseArrows : Lean.TSyntax `Lean.Parser.Tactic.rwRuleSeq → Lean.Elab.TermElabM (Array (Lean.Expr × Bool × Lean.Syntax))
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExBaseNat.brecOn.go : {motive_1 : (e : Q(ℕ)) → Mathlib.Tactic.Ring.Common.ExBaseNat e → Sort u} →
  {motive_2 : (e : Q(ℕ)) → Mathlib.Tactic.Ring.Common.ExProdNat e → Sort u} →
    {motive_3 : (e : Q(ℕ)) → Mathlib.Tactic.Ring.Common.ExSumNat e → Sort u} →
      {e : Q(ℕ)} →
        (t : Mathlib.Tactic.Ring.Common.ExBaseNat e) →
          ((e : Q(ℕ)) → (t : Mathlib.Tactic.Ring.Common.ExBaseNat e) → t.below → motive_1 e t) →
            ((e : Q(ℕ)) → (t : Mathlib.Tactic.Ring.Common.ExProdNat e) → t.below → motive_2 e t) →
              ((e : Q(ℕ)) → (t : Mathlib.Tactic.Ring.Common.ExSumNat e) → t.below → motive_3 e t) →
                motive_1 e t ×' t.below
-- Mathlib.RingTheory.TensorProduct.Maps
/-- The map `LinearMap.lTensorHom` which sends `f ↦ 1 ⊗ f` as a morphism of algebras.  -/
Module.End.lTensorAlgHom : (R : Type u_1) →
  (M : Type u_2) →
    (N : Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommMonoid N] → [inst_4 : Module R N] → Module.End R M →ₐ[R] Module.End R (TensorProduct R N M)
-- Std.Data.TreeMap.Raw.Basic
/-- Transforms a list of mappings into a tree map.  -/
Std.TreeMap.Raw.ofList : {α : Type u} →
  {β : Type v} →
    List (α × β) → (cmp : autoParam (α → α → Ordering) Std.TreeMap.Raw.ofList._auto_1) → Std.TreeMap.Raw α β cmp
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.AreComplementary.fromSum_bijective : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c},
  e₁.AreComplementary e₂ → Function.Bijective (ComplexShape.Embedding.AreComplementary.fromSum e₁ e₂)
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Comma.hasLimitsOfShape : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {A : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  {B : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃}
  [inst_3 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
  [CategoryTheory.Limits.HasLimitsOfShape J A] [CategoryTheory.Limits.HasLimitsOfShape J B]
  [CategoryTheory.Limits.PreservesLimitsOfShape J R],
  CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.Comma L R)
-- Mathlib.Data.Finsupp.Basic
Finsupp.equivMapDomain_symm_apply : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f : α ≃ β) (l : β →₀ M) (a : α),
  (Finsupp.equivMapDomain f.symm l) a = l (f a)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_ofList_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α] {l : List (α × β)}
  {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → (Std.ExtTreeMap.ofList l cmp).getKey! k' = k
-- Mathlib.Data.Sym.Sym2
/-- Constructor for `Sym2`. This is the quotient map `α × α → Sym2 α`.  -/
Sym2.mk : {α : Type u_4} → α → α → Sym2 α
-- Mathlib.Data.Set.Enumerate
_private.Mathlib.Data.Set.Enumerate.0.Set.enumerate.match_1.eq_1 : ∀ {α : Type u_1} (motive : Set α → ℕ → Sort u_2) (s : Set α) (h_1 : (s : Set α) → motive s 0)
  (h_2 : (s : Set α) → (n : ℕ) → motive s n.succ),
  (match s, 0 with
    | s, 0 => h_1 s
    | s, n.succ => h_2 s n) =
    h_1 s
-- Mathlib.RingTheory.RingHom.Locally
/-- If `P` is stable under base change, then so is `Locally P`.  -/
RingHom.locally_isStableUnderBaseChange : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) →
    (RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => P) →
      RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] =>
        RingHom.Locally fun {R S} [CommRing R] [CommRing S] => P
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.colimitHomIsoLimitYoneda'_inv_comp_π_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (F : CategoryTheory.Functor Iᵒᵖ C) [inst_2 : CategoryTheory.Limits.HasColimit F]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape I (Type u₂)] (A : C) (i : I) {Z : Type u₂}
  (h : (F.obj (Opposite.op i) ⟶ A) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitHomIsoLimitYoneda' F A).inv
      (CategoryTheory.CategoryStruct.comp
        (TypeCat.ofHom fun g =>
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F (Opposite.op i)) g)
        h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.rightOp.comp (CategoryTheory.yoneda.obj A)) i)
      h
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
/-- `ofMatrix` bundled as a ring equivalence.  -/
CStarMatrix.ofMatrixRingEquiv : {n : Type u_2} → {A : Type u_5} → [inst : Fintype n] → [inst_1 : Semiring A] → Matrix n n A ≃+* CStarMatrix n n A
-- Mathlib.Dynamics.TopologicalEntropy.Subset
Dynamics.netEntropyEntourage_monotone : ∀ {X : Type u_1} (T : X → X) (U : SetRel X X), Monotone fun F => Dynamics.netEntropyEntourage T F U
-- Mathlib.Algebra.Group.Subgroup.Defs
SubgroupClass.subtype_comp_inclusion : ∀ {G : Type u_1} [inst : Group G] {S : Type u_4} [inst_1 : SetLike S G] [inst_2 : SubgroupClass S G] [inst_3 : LE S]
  [inst_4 : IsConcreteLE S G] {H K : S} (h : H ≤ K), (↑K).comp (SubgroupClass.inclusion h) = ↑H
-- Mathlib.Topology.Subpath
/-- Concatenation of a sequence of paths with compatible endpoints.  -/
Path.concat : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {n : ℕ} → (p : Fin (n + 1) → X) → ((k : Fin n) → Path (p k.castSucc) (p k.succ)) → Path (p 0) (p (Fin.last n))
-- Mathlib.CategoryTheory.Localization.Monoidal.Functor
CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_ε_assoc : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.MonoidalCategory C] [inst_4 : CategoryTheory.MonoidalCategory D]
  [inst_5 : CategoryTheory.MonoidalCategory E] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [inst_6 : L.IsLocalization W] [inst_7 : L.Monoidal] (F : CategoryTheory.Functor D E) (G : CategoryTheory.Functor C E)
  [inst_8 : G.Monoidal] [inst_9 : W.ContainsIdentities] [inst_10 : CategoryTheory.Localization.Lifting L W G F] {Z : E}
  (h : F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε G)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Localization.Lifting.iso L W G F).inv.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
        (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Functor.OplaxMonoidal.η L)) h))
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.cast.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  (f : α →ₘ[μ] β),
  ↑f =
    if h : ∃ b, f = MeasureTheory.AEEqFun.mk (Function.const α b) ⋯ then Function.const α (Classical.choose h)
    else MeasureTheory.AEStronglyMeasurable.mk ↑(Quotient.out f) ⋯
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- This lemma is superseded by `UniformIntegrable.spec` which does not require measurability.  -/
MeasureTheory.UniformIntegrable.spec' : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {p : ENNReal} {f : ι → α → β},
  p ≠ 0 →
    p ≠ ⊤ →
      (∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)) →
        MeasureTheory.UniformIntegrable f p μ →
          ∀ {ε : ℝ},
            0 < ε → ∃ C, ∀ (i : ι), MeasureTheory.eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
-- Lean.Server.References
/-- References provided by the worker.  -/
Lean.Server.TransientWorkerILean.refs : Lean.Server.TransientWorkerILean → Lean.Lsp.ModuleRefs
-- Lean.Elab.BuiltinCommand
_private.Lean.Elab.BuiltinCommand.0.Lean.Elab.Command.addScopes.go : Bool →
  Bool →
    Bool → Bool → List (Lean.TSyntax `Lean.Parser.Term.attrInstance) → Lean.Name → Lean.Elab.Command.CommandElabM Unit
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, (t₁ ∪ t₂)[k]? = t₂[k]?.or t₁[k]?
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.div' : ∀ {G : Type u_2} {α : Type u_3} {β : Type u_4} [inst : MeasurableSpace G] [inst_1 : Div G] {m : MeasurableSpace α}
  {mβ : MeasurableSpace β} [MeasurableDiv₂ G] {f g : α → β → G} {h : α → β},
  Measurable ↿f → Measurable ↿g → Measurable h → Measurable fun a => (f a / g a) (h a)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.WalkingPair.equivBool_symm_apply_false : CategoryTheory.Limits.WalkingPair.equivBool.symm false = CategoryTheory.Limits.WalkingPair.right
-- Mathlib.Analysis.Calculus.Deriv.Inverse
not_differentiableWithinAt_of_local_left_inverse_hasDerivWithinAt_zero : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {f g : 𝕜 → 𝕜} {a : 𝕜} {s t : Set 𝕜},
  a ∈ s →
    UniqueDiffWithinAt 𝕜 s a →
      HasDerivWithinAt f 0 t (g a) → Set.MapsTo g s t → f ∘ g =ᶠ[nhdsWithin a s] id → ¬DifferentiableWithinAt 𝕜 g s a
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.add_of_X_ne : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          P 0 * Q 2 ≠ Q 0 * P 2 →
            W.add P Q =
              W.addZ P Q •
                ![W.toAffine.addX (P 0 / P 2) (Q 0 / Q 2)
                    (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)),
                  W.toAffine.addY (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2)
                    (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)),
                  1]
-- Mathlib.Order.Hom.WithTopBot
/-- **Alias** of `WithBot.coe_toDualTopEquiv`. -/
WithBot.coe_toDualTopEquiv_eq : ∀ {α : Type u_1} [inst : LE α], ⇑WithBot.toDualTopEquiv = ⇑OrderDual.toDual ∘ ⇑WithBot.ofDual
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get_union_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (mem : k ∈ t₂), (t₁ ∪ t₂).get k ⋯ = t₂.get k mem
-- Mathlib.RingTheory.Kaehler.TensorProduct
KaehlerDifferential.map_liftBaseChange_smul : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra A B] [inst_8 : Algebra S B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B]
  [h : Algebra.IsPushout R S A B] (b : B) (x : TensorProduct R S Ω[A⁄R]),
  (LinearMap.liftBaseChange S (↑R (KaehlerDifferential.map R S A B))) (b • x) =
    b • (LinearMap.liftBaseChange S (↑R (KaehlerDifferential.map R S A B))) x
-- Lean.Parser.Syntax
Lean.Parser.Command.catBehavior.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.isScalarTower_of_tower : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {R₁ : Type u_2}
  {R₂ : Type u_3} [inst_3 : CommRing R₁] [inst_4 : CommRing R₂] [inst_5 : Algebra R₁ S] [inst_6 : Algebra R₂ S]
  [inst_7 : SMul R₁ R₂] [inst_8 : SMulCommClass R R₁ S] [inst_9 : SMulCommClass R R₂ S] [IsScalarTower R₁ R₂ S],
  IsScalarTower R₁ R₂ Ω[S⁄R]
-- Lean.AuxRecursor
Lean.NoConfusionInfo.perCtor : ℕ → ℕ → Lean.NoConfusionInfo
-- Mathlib.GroupTheory.Commensurable
Subgroup.Commensurable.commensurable_inv : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) (g : ConjAct G), (g • H).Commensurable H ↔ H.Commensurable (g⁻¹ • H)
-- Mathlib.RingTheory.Ideal.Quotient.Defs
Ideal.Quotient.lift_comp_mk : ∀ {R : Type u} [inst : Ring R] (I : Ideal R) {S : Type v} [inst_1 : I.IsTwoSided] [inst_2 : Semiring S] (f : R →+* S)
  (H : ∀ a ∈ I, f a = 0), (Ideal.Quotient.lift I f H).comp (Ideal.Quotient.mk I) = f
-- Mathlib.Data.Set.Pairwise.Basic
Set.PairwiseDisjoint.eq_or_disjoint : ∀ {α : Type u_1} {ι : Type u_4} [inst : PartialOrder α] [inst_1 : OrderBot α] {s : Set ι} {f : ι → α},
  s.PairwiseDisjoint f → ∀ {i j : ι}, i ∈ s → j ∈ s → i = j ∨ Disjoint (f i) (f j)
-- Mathlib.Data.Fin.SuccPred
Fin.succAbove_castPred_of_le : ∀ {n : ℕ} (p i : Fin (n + 1)), p ≤ i → ∀ (hi : i ≠ Fin.last n), p.succAbove (i.castPred hi) = (i.castPred hi).succ
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.instSemilatticeSup : {α : Type u_1} → [inst : TopologicalSpace α] → SemilatticeSup (TopologicalSpace.CompactOpens α)
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.CompleteType.mem_typesWith_iff : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (φ : (L.withConstants α).Sentence) (p : T.CompleteType α),
  p ∈ T.typesWith φ ↔ φ ∈ p