mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.DList.Lemmas
Batteries.DList.singleton_eq_ofThunk : ∀ {α : Type u_1} {a : α}, Batteries.DList.singleton a = Batteries.DList.ofThunk { fn := fun x => [a] }
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.sum_sq_norm_inner_left : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (x : E),
  ∑ i, ‖inner 𝕜 x (b i)‖ ^ 2 = ‖x‖ ^ 2
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the reverse direction of `Asymptotics.isBigOWith_norm_left`. -/
Asymptotics.IsBigOWith.norm_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {c : ℝ} {g : α → F}
  {f' : α → E'} {l : Filter α}, Asymptotics.IsBigOWith c l f' g → Asymptotics.IsBigOWith c l (fun x => ‖f' x‖) g
-- Mathlib.LinearAlgebra.Basis.Defs
/-- Two elements are equal iff their coordinates are equal.  -/
Module.Basis.ext_elem_iff : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) {x y : M}, x = y ↔ ∀ (i : ι), (b.repr x) i = (b.repr y) i
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Differentiable.rpow_const : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {p : ℝ},
  Differentiable ℝ f → (∀ (x : E), f x ≠ 0 ∨ 1 ≤ p) → Differentiable ℝ fun x => f x ^ p
-- Mathlib.MeasureTheory.Measure.AEMeasurable
MeasureTheory.Measure.map_mono_of_aemeasurable : ∀ {α : Type u_2} {δ : Type u_5} {m0 : MeasurableSpace α} [inst : MeasurableSpace δ] {μ ν : MeasureTheory.Measure α}
  {f : α → δ}, μ ≤ ν → AEMeasurable f ν → MeasureTheory.Measure.map f μ ≤ MeasureTheory.Measure.map f ν
-- Init.System.IO
/-- Replaces the standard error stream of the current thread and returns its previous value.

Use `IO.getStderr` to get the current standard error stream.
 -/
IO.setStderr : IO.FS.Stream → BaseIO IO.FS.Stream
-- Mathlib.Tactic.Order
/-- Using the `≤`-graph `g`, find a contradiction with some `≰`-fact.  -/
Mathlib.Tactic.Order.findContradictionWithNle : Mathlib.Tactic.Order.Graph → Array Mathlib.Tactic.Order.AtomicFact → Mathlib.Tactic.AtomM (Option Lean.Expr)
-- Aesop.Tree.Data
Aesop.GoalState.isProvenByNormalization : Aesop.GoalState → Bool
-- Mathlib.Data.Seq.Basic
Stream'.Seq.length_take_of_le_length : ∀ {α : Type u} {s : Stream'.Seq α} {n : ℕ}, (∀ (h : s.Terminates), n ≤ s.length h) → (Stream'.Seq.take n s).length = n
-- Std.Time.Format.Basic
/-- A string literal.
 -/
Std.Time.FormatPart.string : String → Std.Time.FormatPart
-- Init.Prelude
/-- Compose two proofs by transitivity, generalized over the relations involved.  -/
Trans.trans : {α : Sort u_1} →
  {β : Sort u_2} →
    {γ : Sort u_3} →
      {r : α → β → Sort u} →
        {s : β → γ → Sort v} →
          {t : outParam (α → γ → Sort w)} → [self : Trans r s t] → {a : α} → {b : β} → {c : γ} → r a b → s b c → t a c
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderivWithin_comp_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {s : Set E} (a : E), fderivWithin 𝕜 (fun x => f (x - a)) s x = fderivWithin 𝕜 f (-a +ᵥ s) (x - a)
-- Mathlib.SetTheory.Ordinal.Notation
ONote.NFBelow.brecOn : ∀ {motive : (a : ONote) → (a_1 : Ordinal.{0}) → a.NFBelow a_1 → Prop} {a : ONote} {a_1 : Ordinal.{0}}
  (t : a.NFBelow a_1),
  (∀ (a : ONote) (a_2 : Ordinal.{0}) (t : a.NFBelow a_2), ONote.NFBelow.below t → motive a a_2 t) → motive a a_1 t
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- **Alias** of the reverse direction of `hasFDerivWithinAt_add_const_iff`. -/
HasFDerivWithinAt.add_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} {s : Set E} (c : F), HasFDerivWithinAt f f' s x → HasFDerivWithinAt (fun x => f x + c) f' s x
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
CategoryTheory.EffectiveEpi.uniq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y W : C} (f : Y ⟶ X)
  [inst_1 : CategoryTheory.EffectiveEpi f] (e : Y ⟶ W)
  (h :
    ∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
      CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
        CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e)
  (m : X ⟶ W), CategoryTheory.CategoryStruct.comp f m = e → m = CategoryTheory.EffectiveEpi.desc f e ⋯
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.MeasurePreserving.add_left : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Add G] [MeasurableAdd G] (μ : MeasureTheory.Measure G)
  [μ.IsAddLeftInvariant] (g : G) {X : Type u_3} [inst_4 : MeasurableSpace X] {μ' : MeasureTheory.Measure X} {f : X → G},
  MeasureTheory.MeasurePreserving f μ' μ → MeasureTheory.MeasurePreserving (fun x => g + f x) μ' μ
-- Std.Http.Data.URI.Encoding
_private.Std.Http.Data.URI.Encoding.0.ByteArray.push.match_1.eq_1 : ∀ (motive : ByteArray → UInt8 → Sort u_1) (bs : Array UInt8) (b : UInt8)
  (h_1 : (bs : Array UInt8) → (b : UInt8) → motive { data := bs } b),
  (match { data := bs }, b with
    | { data := bs }, b => h_1 bs b) =
    h_1 bs b
-- Mathlib.RingTheory.NormalClosure
Ring.instFaithfulSMulNormalClosure : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : IsDomain S]
  [inst_4 : Algebra R S] [inst_5 : Module.IsTorsionFree R S], FaithfulSMul R (Ring.NormalClosure R S)
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.div.eq_def : ∀ (k : ℤ) (x : Int.Internal.Linear.Poly),
  Int.Internal.Linear.Poly.div k x =
    match x with
    | Int.Internal.Linear.Poly.num k' => Int.Internal.Linear.Poly.num (Int.Internal.Linear.cdiv k' k)
    | Int.Internal.Linear.Poly.add k' x p => Int.Internal.Linear.Poly.add (k' / k) x (Int.Internal.Linear.Poly.div k p)
-- Mathlib.GroupTheory.QuotientGroup.Defs
AddSubgroup.orderIsoAddCon_symm_apply_coe : ∀ {G : Type u_1} [inst : AddGroup G] (c : AddCon G), ↑((RelIso.symm AddSubgroup.orderIsoAddCon) c) = c.addSubgroup
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Finpartition.card_parts_equitabilise : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {m a b : ℕ} (P : Finpartition s)
  (h : a * m + b * (m + 1) = s.card), m ≠ 0 → (Finpartition.equitabilise h).parts.card = a + b
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.toOrderedAdd : ∀ {R : Type u} {inst : Lean.Grind.Semiring R} {inst_1 : LE R} {inst_2 : LT R} {inst_3 : Std.IsPreorder R}
  [self : Lean.Grind.OrderedRing R], Lean.Grind.OrderedAdd R
-- Mathlib.Topology.Algebra.Group.Pointwise
subset_interior_vadd : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace β] [inst_1 : AddGroup α] [inst_2 : AddAction α β]
  [ContinuousConstVAdd α β] {s : Set α} {t : Set β} [inst_4 : TopologicalSpace α],
  interior s +ᵥ interior t ⊆ interior (s +ᵥ t)
-- Mathlib.Tactic.FunProp.Theorems
/-- Environment extension for transition theorems.  -/
Mathlib.Meta.FunProp.transitionTheoremsExt : Mathlib.Meta.FunProp.GeneralTheoremsExt
-- Mathlib.RingTheory.Valuation.Discrete.RankOne
Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply_zero : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {R : Type u_2} [inst_1 : Ring R] (v : Valuation R Γ)
  [hv : v.IsRankOneDiscrete], (Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt v) 0 = 0
-- Lean.Util.MonadCache
Lean.MonadCacheT.instMonadRef : {ω α β : Type} →
  {m : Type → Type} →
    [inst : STWorld ω m] →
      [inst_1 : BEq α] → [inst_2 : Hashable α] → [Lean.MonadRef m] → Lean.MonadRef (Lean.MonadCacheT α β m)
-- Lean.Log
/-- Log the error message "unknown declaration"  -/
Lean.logUnknownDecl : {m : Type → Type} →
  [Monad m] → [Lean.MonadLog m] → [Lean.AddMessageContext m] → [Lean.MonadOptions m] → Lean.Name → m Unit
-- Init.Meta.Defs
/-- Expand macros in the given syntax.
A node with kind `k` is visited only if `p k` is true.

Note that the default value for `p` returns false for `by ...` nodes.
This is a "hack". The tactic framework abuses the macro system to implement extensible tactics.
For example, one can define
```lean
syntax "my_trivial" : tactic -- extensible tactic

macro_rules | `(tactic| my_trivial) => `(tactic| decide)
macro_rules | `(tactic| my_trivial) => `(tactic| assumption)
```
When the tactic evaluator finds the tactic `my_trivial`, it tries to evaluate the `macro_rule` expansions
until one "works", i.e., the macro expansion is evaluated without producing an exception.
We say this solution is a bit hackish because the term elaborator may invoke `expandMacros` with `(p := fun _ => true)`,
and expand the tactic macros as just macros. In the example above, `my_trivial` would be replaced with `assumption`,
`decide` would not be tried if `assumption` fails at tactic evaluation time.

We are considering two possible solutions for this issue:
1- A proper extensible tactic feature that does not rely on the macro system.

2- Typed macros that know the syntax categories they're working in. Then, we would be able to select which
   syntactic categories are expanded by `expandMacros`.
 -/
Lean.expandMacros : Lean.Syntax → (optParam (Lean.SyntaxNodeKind → Bool) fun k => k != `Lean.Parser.Term.byTactic) → Lean.MacroM Lean.Syntax
-- Init.Data.BitVec.Lemmas
BitVec.shiftConcat.eq_1 : ∀ {n : ℕ} (x : BitVec n) (b : Bool), x.shiftConcat b = BitVec.truncate n (x.concat b)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensor_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C × C),
  (CategoryTheory.MonoidalCategory.tensor C).obj X = CategoryTheory.MonoidalCategoryStruct.tensorObj X.1 X.2
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_pow_of_ne_zero : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Monoid α] [inst_1 : Monoid β] [inst_2 : FunLike F α β]
  [MulHomClass F α β] {n : ℕ}, n ≠ 0 → ∀ (f : F) (s : Set α), ⇑f '' s ^ n = (⇑f '' s) ^ n
-- Mathlib.Topology.Homotopy.Contractible
ContractibleSpace.hequiv_unit : ∀ (X : Type u_1) [inst : TopologicalSpace X] [ContractibleSpace X], Nonempty (ContinuousMap.HomotopyEquiv X Unit)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidal_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.AddMon C),
  (CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidal C).obj A =
    CategoryTheory.LaxMonoidalFunctor.of (CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidalObj A)
-- Lean.Expr
/-- Polymorphic operation for generating unique/fresh universe metavariable identifiers.
It is available in any monad `m` that implements the interface `MonadNameGenerator`.
 -/
Lean.mkFreshLMVarId : {m : Type → Type} → [Monad m] → [Lean.MonadNameGenerator m] → m Lean.LMVarId
-- Mathlib.CategoryTheory.Limits.Fubini
/-- Given a functor `F : J ⥤ K ⥤ C`, with all needed limits,
we can construct a diagram consisting of the limit cone over each functor `F.obj j`,
and the universal cone morphisms between these.
 -/
CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) →
              [CategoryTheory.Limits.HasLimitsOfShape K C] → CategoryTheory.Limits.DiagramOfCones F
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- The triangle consisting of the two natural transformations and `hom` commutes  -/
CategoryTheory.Limits.BiconeMorphism.wι_assoc : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {A B : CategoryTheory.Limits.Bicone F}
  (self : CategoryTheory.Limits.BiconeMorphism A B) (j : J) {Z : C} (h : B.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (A.ι j) (CategoryTheory.CategoryStruct.comp self.hom h) =
    CategoryTheory.CategoryStruct.comp (B.ι j) h
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.addSubmonoidComap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N) (N' : AddSubmonoid N),
  f.addSubmonoidComap N' = { toFun := fun x => ⟨f ↑x, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }
-- Lean.Data.Lsp.Basic
/-- [reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#workDoneProgressOptions)  -/
Lean.Lsp.WorkDoneProgressOptions : Type
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_hom_apply_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] (X : (CategoryTheory.Sheaf J A)ᵒᵖ) (X_1 : CategoryTheory.Sheaf J A)
  (a :
    (((CategoryTheory.sheafToPresheaf J A).op.comp
              (CategoryTheory.coyoneda.comp
                ((CategoryTheory.Functor.whiskeringLeft (CategoryTheory.Sheaf J A) (CategoryTheory.Functor Cᵒᵖ A)
                      (Type (max u₁ v₂))).obj
                  (CategoryTheory.sheafToPresheaf J A)))).obj
          X).obj
      X_1),
  ((CategoryTheory.ConcreteCategory.hom
          ((CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf.hom.app X).app X_1))
        a).hom =
    (Equiv.ulift.toIso.inv.hom' a).down
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.count_mul : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α]
  [inst_2 : DecidableEq (Associates α)] [inst_3 : (p : Associates α) → Decidable (Irreducible p)] {a : Associates α},
  a ≠ 0 →
    ∀ {b : Associates α},
      b ≠ 0 → ∀ {p : Associates α}, Irreducible p → p.count (a * b).factors = p.count a.factors + p.count b.factors
-- Mathlib.LinearAlgebra.Dimension.Constructions
/-- The dimension of a submodule is bounded by the dimension of the ambient space.  -/
Submodule.finrank_le : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Finite R M] (s : Submodule R M), Module.finrank R ↥s ≤ Module.finrank R M
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.inv_aeval_X_g : ∀ {R : Type u_1} [inst : CommRing R] (P : StandardEtalePair R),
  ↑⋯.unit⁻¹ = (Ideal.Quotient.mk (Ideal.span {Polynomial.C P.f, Polynomial.X * Polynomial.C P.g - 1})) Polynomial.X
-- Mathlib.Data.Complex.Basic
Complex.one_re : Complex.re 1 = 1
-- Init.Grind.Ring.CommSemiringAdapter
_private.Init.Grind.Ring.CommSemiringAdapter.0.Lean.Grind.CommRing.Poly.denoteS.match_1.eq_2 : ∀ (motive : Lean.Grind.CommRing.Poly → Sort u_1) (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Poly.num k))
  (h_2 :
    (k : ℤ) →
      (m : Lean.Grind.CommRing.Mon) → (p : Lean.Grind.CommRing.Poly) → motive (Lean.Grind.CommRing.Poly.add k m p)),
  (match Lean.Grind.CommRing.Poly.add k m p with
    | Lean.Grind.CommRing.Poly.num k => h_1 k
    | Lean.Grind.CommRing.Poly.add k m p => h_2 k m p) =
    h_2 k m p
-- Std.Sat.AIG.Basic
Std.Sat.AIG.ExtendTarget.mk.sizeOf_spec : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {newWidth : ℕ} [inst_2 : SizeOf α]
  (w : ℕ) (vec : aig.RefVec w), sizeOf { w := w, vec := vec } = 1 + sizeOf w + sizeOf vec
-- Init.Data.Order.Classes
Std.LawfulOrderBEq.mk : ∀ {α : Type u} [inst : BEq α] [inst_1 : LE α], (∀ (a b : α), (a == b) = true ↔ a ≤ b ∧ b ≤ a) → Std.LawfulOrderBEq α
-- Init.Prelude
/-- The implementation of `a ^^^ b : α`. See `HXor`.  -/
XorOp.xor : {α : Type u} → [self : XorOp α] → α → α → α
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.mkInitialTacticInfo : Lean.Syntax → Lean.Elab.Tactic.TacticM (Lean.Elab.Tactic.TacticM Lean.Elab.Info)
-- Mathlib.RingTheory.Valuation.Basic
/-- **Alias** of `Valuation.IsEquiv.eq_iff`. -/
Valuation.IsEquiv.val_eq : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀},
  v₁.IsEquiv v₂ → ∀ {r s : R}, v₁ r = v₁ s ↔ v₂ r = v₂ s
-- Mathlib.Logic.Basic
dite_prop_iff_and : ∀ {P : Prop} [inst : Decidable P] {Q : P → Prop} {R : ¬P → Prop}, dite P Q R ↔ (∀ (h : P), Q h) ∧ ∀ (h : ¬P), R h
-- Mathlib.Algebra.Category.Ring.Under.Basic
CommRingCat.mkUnder_ext : ∀ {R : CommRingCat} {A : Type u} [inst : CommRing A] [inst_1 : Algebra (↑R) A] {B : CategoryTheory.Under R}
  {f g : R.mkUnder A ⟶ B},
  (∀ (a : A),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Under.Hom.right f)) a =
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Under.Hom.right g)) a) →
    f = g
-- Lean.Meta.Sym.Arith.Types
/-- Classification state for a type with a `CommSemiring` instance.
Recall that `CommSemiring` types are normalized using the `OfSemiring.Q` envelope.
 -/
Lean.Meta.Sym.Arith.CommSemiring : Type
-- Mathlib.CategoryTheory.Limits.Chosen.End
CategoryTheory.Limits.chosenEnd.map_comp_assoc : ∀ {J : Type u_3} {C : Type u_4} [inst : CategoryTheory.Category.{v_3, u_4} C]
  [inst_1 : CategoryTheory.Category.{v_4, u_3} J] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  [inst_2 : CategoryTheory.Limits.ChosenEndsOfShape J C] {G H : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  (f : F ⟶ G) (g : G ⟶ H) {Z : C} (h : CategoryTheory.Limits.chosenEnd H ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenEnd.map f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenEnd.map g) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenEnd.map (CategoryTheory.CategoryStruct.comp f g)) h
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackProdSndIsoProd_inv_fst_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct Z Y] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Z X]
  [inst_3 : CategoryTheory.Limits.HasPullback CategoryTheory.Limits.prod.snd f],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdSndIsoProd f Z).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.prod.snd f)
        CategoryTheory.Limits.prod.fst) =
    CategoryTheory.Limits.prod.fst
-- Mathlib.Analysis.Normed.Order.UpperLower
IsLowerSet.thickening' : ∀ {α : Type u_1} [inst : NormedCommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α] {s : Set α},
  IsLowerSet s → ∀ (ε : ℝ), IsLowerSet (Metric.thickening ε s)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0to1.Λ'.normal : {Γ : Type u_1} → {Λ : Type u_2} → Λ → Turing.TM0to1.Λ' Γ Λ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, t.isEmpty = true → t.getKey? a = none
-- Mathlib.Topology.Order.OrderClosed
continuous_max : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α],
  Continuous fun p => max p.1 p.2
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- **Alias** of `QuadraticForm.discr'_smul`. -/
QuadraticForm.QuadraticMap.discr_smul : ∀ {R : Type u_3} {n : Type w} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] [inst_3 : Invertible 2]
  {Q : QuadraticForm R (n → R)} (a : R), (a • Q).discr' = a ^ Fintype.card n * Q.discr'
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel.instLawfulUpwardEnumerable : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] {β : Type v} [inst_2 : LE β] [inst_3 : LT β]
  [inst_4 : Std.PRange.UpwardEnumerable β] [inst_5 : Std.PRange.LawfulUpwardEnumerable β]
  [inst_6 : Std.PRange.LawfulUpwardEnumerableLE β] [inst_7 : Std.PRange.LawfulUpwardEnumerableLT β] [m : HasModel✝ α β],
  Std.PRange.LawfulUpwardEnumerable α
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.coordChange.eq_1 : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e₁ e₂ : Bundle.Trivialization F proj) (b : B) (x : F),
  e₁.coordChange e₂ b x = (↑e₂ (↑e₁.symm (b, x))).2
-- Init.Data.Int.Lemmas
Int.eq_one_of_mul_eq_self_left : ∀ {a b : ℤ}, a ≠ 0 → b * a = a → b = 1
-- Mathlib.Data.List.Perm.Basic
List.Perm.flatMap_left : ∀ {α : Type u_1} {β : Type u_2} (l : List α) {f g : α → List β},
  (∀ a ∈ l, (f a).Perm (g a)) → (List.flatMap f l).Perm (List.flatMap g l)
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.smul_finset_inter_subset : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s₁ s₂ : Finset β} {a : α},
  a • (s₁ ∩ s₂) ⊆ a • s₁ ∩ a • s₂
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey?_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insert k v).maxKey? = some (t.maxKey?.elim k fun k' => if (cmp k' k).isLE = true then k else k')
-- Mathlib.RingTheory.SimpleModule.Isotypic
OrderIso.setIsotypicComponents.eq_1 : ∀ {R : Type u_2} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsSemisimpleModule R M],
  OrderIso.setIsotypicComponents =
    { toFun := fun s => ⨆ c ∈ s, ⟨↑c, ⋯⟩, invFun := fun m => {c | ↑c ≤ ↑m}, left_inv := ⋯, right_inv := ⋯,
      map_rel_iff' := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- A split mono `f` equalizes `(retraction f ≫ f)` and `(𝟙 Y)`.
 -/
CategoryTheory.Limits.isSplitMonoEqualizes : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (f : X ⟶ Y) →
        [inst_1 : CategoryTheory.IsSplitMono f] →
          CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneOfIsSplitMono f)
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
circleMap_sub_center : ∀ (c : ℂ) (R θ : ℝ), circleMap c R θ - c = circleMap 0 R θ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_alter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k k' : α} {f : Option (β k) → Option (β k)},
  m.WF →
    (m.alter k f).getKey? k' =
      if (k == k') = true then if (f (m.get? k)).isSome = true then some k else none else m.getKey? k'
-- Mathlib.Order.Hom.Basic
/-- Diagonal embedding of `α` into `α × α` as an `OrderHom`.  -/
OrderHom.diag : {α : Type u_2} → [inst : Preorder α] → α →o α × α
-- Mathlib.NumberTheory.PellMatiyasevic
_private.Mathlib.NumberTheory.PellMatiyasevic.0.Pell.d : {a : ℕ} → 1 < a → ℕ
-- Init.Data.String.Lemmas.Order
String.Pos.ofSlice_ne_endPos : ∀ {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos},
  p ≠ (s.slice p₀ p₁ h).endPos → String.Pos.ofSlice p ≠ s.endPos
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.invRev_cons : ∀ {α : Type u} {L : List (α × Bool)} {a : α × Bool},
  FreeGroup.invRev (a :: L) = FreeGroup.invRev L ++ FreeGroup.invRev [a]
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
ContinuousMap.toLp_comp_toContinuousMap : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} (μ : MeasureTheory.Measure α)
  [inst : TopologicalSpace α] [inst_1 : BorelSpace α] [inst_2 : NormedAddCommGroup E]
  [inst_3 : SecondCountableTopologyEither α E] [inst_4 : CompactSpace α] [inst_5 : MeasureTheory.IsFiniteMeasure μ]
  {𝕜 : Type u_3} [inst_6 : Fact (1 ≤ p)] [inst_7 : NormedRing 𝕜] [inst_8 : Module 𝕜 E] [inst_9 : IsBoundedSMul 𝕜 E]
  (f : BoundedContinuousFunction α E),
  (ContinuousMap.toLp p μ 𝕜) f.toContinuousMap = (BoundedContinuousFunction.toLp p μ 𝕜) f