mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {l : List (α × β)} {k k' : α},
      cmp k k' = Ordering.eq →
        ∀ {v : β},
          List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
            (k, v) ∈ l → ∀ {h' : k' ∈ t.insertMany l}, (t.insertMany l)[k'] = v
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.single.congr_simp : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular] (j j_1 : J),
  j = j_1 →
    CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.single j =
      CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.single j_1
-- Init.Data.UInt.Bitwise
UInt16.shiftLeft_and : ∀ {a b c : UInt16}, (a &&& b) <<< c = a <<< c &&& b <<< c
-- Mathlib.Algebra.Lie.CartanSubalgebra
LieSubalgebra.ucs_eq_self_of_isCartanSubalgebra : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (H : LieSubalgebra R L)
  [H.IsCartanSubalgebra] (k : ℕ), LieSubmodule.ucs k H.toLieSubmodule = H.toLieSubmodule
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.simp_middle.injEq : ∀ (lhs : Bool) (s₁ s₂ : Lean.Grind.AC.Seq) (c₁ c₂ : Lean.Meta.Grind.AC.EqCnstr) (lhs_1 : Bool)
  (s₁_1 s₂_1 : Lean.Grind.AC.Seq) (c₁_1 c₂_1 : Lean.Meta.Grind.AC.EqCnstr),
  (Lean.Meta.Grind.AC.EqCnstrProof.simp_middle lhs s₁ s₂ c₁ c₂ =
      Lean.Meta.Grind.AC.EqCnstrProof.simp_middle lhs_1 s₁_1 s₂_1 c₁_1 c₂_1) =
    (lhs = lhs_1 ∧ s₁ = s₁_1 ∧ s₂ = s₂_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1)
-- Init.Data.Int.DivMod.Lemmas
Int.fdiv_sign : ∀ {a b : ℤ}, a.fdiv b.sign = a * b.sign
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasAntidiagonal.sigmaAntidiagonalEquivProd_symm_apply_snd_coe : ∀ {A : Type u_1} [inst : AddMonoid A] [inst_1 : Finset.HasAntidiagonal A] (x : A × A),
  ↑(Finset.HasAntidiagonal.sigmaAntidiagonalEquivProd.symm x).snd = x
-- Mathlib.Topology.Order
discreteTopology_iff_forall_isClosed : ∀ {α : Type u_1} [inst : TopologicalSpace α], DiscreteTopology α ↔ ∀ (s : Set α), IsClosed s
-- Mathlib.Tactic.SuccessIfFailWithMsg
/-- `success_if_fail_with_msg msg tacs` runs `tacs` and succeeds only if they fail with the message
`msg`.

`msg` can be any term that evaluates to an explicit `String`.  -/
Mathlib.Tactic.successIfFailWithMsg : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
_private.Mathlib.CategoryTheory.Limits.Shapes.Reflexive.0.CategoryTheory.Limits.WalkingParallelPair.inclusionWalkingReflexivePair.match_3.eq_2 : ∀ (motive : (Y X : CategoryTheory.Limits.WalkingParallelPair) → (X ⟶ Y) → Sort u_1)
  (h_1 :
    Unit →
      motive CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.WalkingParallelPair.zero
        CategoryTheory.Limits.WalkingParallelPairHom.left)
  (h_2 :
    Unit →
      motive CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.WalkingParallelPair.zero
        CategoryTheory.Limits.WalkingParallelPairHom.right)
  (h_3 :
    (x : CategoryTheory.Limits.WalkingParallelPair) → motive x x (CategoryTheory.Limits.WalkingParallelPairHom.id x)),
  (match CategoryTheory.Limits.WalkingParallelPair.one, CategoryTheory.Limits.WalkingParallelPair.zero,
      CategoryTheory.Limits.WalkingParallelPairHom.right with
    | .(CategoryTheory.Limits.WalkingParallelPair.one), .(CategoryTheory.Limits.WalkingParallelPair.zero),
      CategoryTheory.Limits.WalkingParallelPairHom.left => h_1 ()
    | .(CategoryTheory.Limits.WalkingParallelPair.one), .(CategoryTheory.Limits.WalkingParallelPair.zero),
      CategoryTheory.Limits.WalkingParallelPairHom.right => h_2 ()
    | x, .(x), CategoryTheory.Limits.WalkingParallelPairHom.id .(x) => h_3 x) =
    h_2 ()
-- Init.Data.UInt.Bitwise
UInt32.ofFin_shiftLeft_mod : ∀ (a b : Fin UInt32.size), UInt32.ofFin (a <<< (b % 32)) = UInt32.ofFin a <<< UInt32.ofFin b
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.comp_id : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] (f : P1 →ᵃ[k] P2), f.comp (AffineMap.id k P1) = f
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.ascii_turnstile : Lean.Parser.Parser
-- Init.Omega.Constraint
Lean.Omega.Constraint.scale_sat : ∀ {t : ℤ} {c : Lean.Omega.Constraint} (k : ℤ), c.sat t = true → (Lean.Omega.Constraint.scale k c).sat (k * t) = true
-- Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
/-- **Alias** of `ModuleCat.hasProjectiveDimensionLE_of_linearEquiv`. -/
CategoryTheory.hasProjectiveDimensionLE_of_linearEquiv : ∀ {R : Type u} [inst : Ring R] [Small.{v, u} R] [Small.{v', u} R] {M : ModuleCat R} {N : ModuleCat R} (e : ↑M ≃ₗ[R] ↑N)
  (n : ℕ) [CategoryTheory.HasProjectiveDimensionLE M n], CategoryTheory.HasProjectiveDimensionLE N n
-- Mathlib.Data.FP.Basic
FP.instInhabitedRMode.default : FP.RMode
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
/-- The coercion to function is a monoid homomorphism.  -/
LeftInvariantDerivation.coeFnAddMonoidHom : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              (I : ModelWithCorners 𝕜 E H) →
                (G : Type u_4) →
                  [inst_4 : TopologicalSpace G] →
                    [inst_5 : ChartedSpace H G] →
                      [inst_6 : Monoid G] →
                        [inst_7 : ContMDiffMul I (↑⊤) G] →
                          LeftInvariantDerivation I G →+
                            ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤ →
                              ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
ball_sub_ball : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ ε : ℝ},
  0 < ε → 0 < δ → ∀ (a b : E), Metric.ball a ε - Metric.ball b δ = Metric.ball (a - b) (ε + δ)
-- Mathlib.Algebra.Group.Equiv.Opposite
MulHom.toOpposite_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (hf : ∀ (x y : M), Commute (f x) (f y)),
  ⇑(f.toOpposite hf) = MulOpposite.op ∘ ⇑f
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.translationNumber_eq_rat_iff : ∀ (f : CircleDeg1Lift),
  Continuous ⇑f → ∀ {m : ℤ} {n : ℕ}, 0 < n → (f.translationNumber = ↑m / ↑n ↔ ∃ x, (f ^ n) x = x + ↑m)
-- Mathlib.RepresentationTheory.FDRep
FDRep.Iso.conj_ρ : ∀ {R : Type u} {G : Type v} [inst : CommRing R] [inst_1 : Monoid G] {V W : FDRep R G} (i : V ≅ W) (g : G),
  W.ρ g = (FDRep.isoToLinearEquiv i).conj (V.ρ g)
-- Init.Data.Range.Basic
_private.Init.Data.Range.Basic.0.Std.Legacy.Range.forIn'.loop : {m : Type u_1 → Type u_2} →
  {β : Type u_1} →
    [Monad m] →
      (range : Std.Legacy.Range) →
        ((i : ℕ) → i ∈ range → β → m (ForInStep β)) →
          β →
            (i : ℕ) →
              (i - range.start) % range.step = 0 → autoParam (range.start ≤ i) Std.Legacy.Range.forIn'._auto_1✝ → m β
-- Mathlib.Analysis.PSeries
Finset.le_sum_condensed' : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedAddMonoid M] {f : ℕ → M},
  (∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m) →
    ∀ (n : ℕ), ∑ k ∈ Finset.Ico 1 (2 ^ n), f k ≤ ∑ k ∈ Finset.range n, 2 ^ k • f (2 ^ k)
-- Mathlib.CategoryTheory.Comma.Final
CategoryTheory.Comma.final_fst : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) [R.Final], (CategoryTheory.Comma.fst L R).Final
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.formatDayPeriod : Std.Time.DayPeriodSymbols → Std.Time.DayPeriod → String
-- Mathlib.Order.Minimal
Set.exists_sdiff_singleton_of_not_minimal : ∀ {α : Type u_2} {P : Set α → Prop} {s : Set α},
  (∀ ⦃s t : Set α⦄, P t → t ⊆ s → P s) → P s → ¬Minimal P s → ∃ x ∈ s, P (s \ {x})
-- Mathlib.Order.Sublattice
/-- The inf of two sublattices is their intersection.  -/
Sublattice.instInf : {α : Type u_2} → [inst : Lattice α] → Min (Sublattice α)
-- Lean.CompactedRegion
/-- Reads a compacted region from disk.

`depRegions` are existing compacted regions whose address ranges are needed for cross-region
pointer fixup. The result is the root object reinterpreted at type `α` paired with the new
`CompactedRegion`. Unsafe because `α` is type-erased at the extern boundary: it is the caller's
responsibility to ensure `α` matches the type the data was saved at; mismatched types yield
undefined behavior on use.
 -/
Lean.CompactedRegion.read : {α : Type} → System.FilePath → Array Lean.CompactedRegion → IO (α × Lean.CompactedRegion)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0.step_supports : ∀ {Γ : Type u_1} {Λ : Type u_2} [inst : Inhabited Λ] [inst_1 : Inhabited Γ] (M : Turing.TM0.Machine Γ Λ) {S : Set Λ},
  Turing.TM0.Supports M S → ∀ {c c' : Turing.TM0.Cfg Γ Λ}, c' ∈ Turing.TM0.step M c → c.q ∈ S → c'.q ∈ S
-- Mathlib.Data.Seq.Computation
Computation.orElse_pure : ∀ {α : Type u} (c₁ : Computation α) (a : α), (c₁.think <|> Computation.pure a) = Computation.pure a
-- Lean.Server.Completion.CompletionItemCompression
_private.Lean.Server.Completion.CompletionItemCompression.0.Lean.Lsp.ResolvableCompletionList.compressPositionFast : String → Lean.Lsp.Position → String
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.instAdd : {R : Type u_3} →
  {M : Type u_4} →
    {N : Type u_5} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] → [inst_3 : AddCommMonoid N] → [inst_4 : Module R N] → Add (QuadraticMap R M N)
-- Qq.Macro
Qq.Impl.MVarSynth.level.sizeOf_spec : ∀ (unquotedMVar : Lean.LMVarId), sizeOf (Qq.Impl.MVarSynth.level unquotedMVar) = 1 + sizeOf unquotedMVar
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.MeasurePreserving.integrableOn_image : ∀ {α : Type u_1} {β : Type u_2} {ε : Type u_3} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] [inst_2 : MeasurableSpace β] {e : α → β}
  {ν : MeasureTheory.Measure β},
  MeasureTheory.MeasurePreserving e μ ν →
    MeasurableEmbedding e →
      ∀ {f : β → ε} {s : Set α}, MeasureTheory.IntegrableOn f (e '' s) ν ↔ MeasureTheory.IntegrableOn (f ∘ e) s μ
-- Mathlib.Order.SuccPred.Limit
Order.isPredPrelimit_iff_pred_ne : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : PredOrder α] [NoMinOrder α],
  Order.IsPredPrelimit a ↔ ∀ (b : α), Order.pred b ≠ a
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_eq_natCast : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : NonAssocSemiring α] [inst_2 : StarRing α]
  {M : Matrix n n α} {d : ℕ}, M.conjTranspose = ↑d ↔ M = ↑d
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.DiagramOfCocones.coconePoints_obj : ∀ {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)} (D : CategoryTheory.Limits.DiagramOfCocones F) (j : J),
  D.coconePoints.obj j = (D.obj j).pt
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than or equal to the
given key, returning `none` if no such pair exists.
 -/
Std.TreeMap.Raw.getEntryLE? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α → Option (α × β)
-- Mathlib.GroupTheory.PresentedGroup
PresentedGroup.toGroup.of : ∀ {α : Type u_1} {G : Type u_3} [inst : Group G] {f : α → G} {rels : Set (FreeGroup α)}
  (h : ∀ r ∈ rels, (FreeGroup.lift f) r = 1) {x : α}, (PresentedGroup.toGroup h) (PresentedGroup.of x) = f x
-- Init.Data.Float.Model.Float32
/-- Converts a `Float32.Model` to an `Int32`, truncating after the decimal point, sending `NaN` to
`0` and clamping out-of-range values and infinities.
 -/
Float32.Model.toInt32 : Float32.Model → Int32
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.exact_iff_epi_toCycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology], S.Exact ↔ CategoryTheory.Epi S.toCycles
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.instTrivialStarSubtypeAEEqFunMemAddSubgroup : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {R : Type u_6} [inst : NormedAddCommGroup R]
  [inst_1 : StarAddMonoid R] [inst_2 : NormedStarGroup R] [TrivialStar R] {p : ENNReal},
  TrivialStar ↥(MeasureTheory.Lp R p μ)
-- Lean.Expr
Lean.Expr.sort.sizeOf_spec : ∀ (u : Lean.Level), sizeOf (Lean.Expr.sort u) = 1 + sizeOf u
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
analyticOn_taylorComp : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {t : Set F}
  {q : F → FormalMultilinearSeries 𝕜 F G} {p : E → FormalMultilinearSeries 𝕜 E F},
  (∀ (n : ℕ), AnalyticOn 𝕜 (fun x => q x n) t) →
    (∀ (n : ℕ), AnalyticOn 𝕜 (fun x => p x n) s) →
      ∀ {f : E → F},
        AnalyticOn 𝕜 f s → Set.MapsTo f s t → ∀ (n : ℕ), AnalyticOn 𝕜 (fun x => (q (f x)).taylorComp (p x) n) s
-- Mathlib.Probability.Process.Predictable
/-- A predictable process is adapted.  -/
MeasureTheory.IsStronglyPredictable.stronglyAdapted : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {E : Type u_3} [inst : TopologicalSpace E]
  [inst_1 : LinearOrder ι] [inst_2 : OrderBot ι] [inst_3 : MeasurableSpace ι] [inst_4 : TopologicalSpace ι]
  [OpensMeasurableSpace ι] [OrderClosedTopology ι] {𝓕 : MeasureTheory.Filtration ι m} {u : ι → Ω → E},
  MeasureTheory.IsStronglyPredictable 𝓕 u → MeasureTheory.StronglyAdapted 𝓕 u
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.mkPiRing_apply_one_eq_self : ∀ {R : Type u} {ι : Type v} {M : Type u_1} [inst : Fintype ι] [inst_1 : CommRing R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : TopologicalSpace R] [inst_5 : TopologicalSpace M] [inst_6 : ContinuousMul R]
  [inst_7 : ContinuousSMul R M] (f : ContinuousMultilinearMap R (fun x => R) M),
  ContinuousMultilinearMap.mkPiRing R ι (f fun x => 1) = f
-- Mathlib.Order.Filter.Map
Filter.map_equiv_symm : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) (f : Filter β), Filter.map (⇑e.symm) f = Filter.comap (⇑e) f
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.stmts₁.eq_6 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (a : σ → Λ),
  Turing.TM2.stmts₁ (Turing.TM2.Stmt.goto a) = {Turing.TM2.Stmt.goto a}
-- Lean.Meta.Tactic.Grind.Types
/-- When `e` was added to this equivalence class because of an equality `h : e = target`,
then we store `target` here, and `h` at `proof?`.
 -/
Lean.Meta.Grind.ENode.target? : Lean.Meta.Grind.ENode → Option Lean.Expr
-- Aesop.Stats.Basic
Aesop.profiling : {m : Type → Type} →
  [Monad m] →
    [Aesop.MonadStats m] →
      [MonadLiftT BaseIO m] → {α : Type} → (Aesop.Stats → α → Aesop.Nanos → Aesop.Stats) → m α → m α
-- Mathlib.CategoryTheory.Sites.Continuous
/-- If `F ⊣ G` is an adjunction between continuous functors, the associated
pushforwards on sheaves are adjoint.  -/
CategoryTheory.Adjunction.sheafPushforwardContinuous : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            {F : CategoryTheory.Functor C D} →
              {G : CategoryTheory.Functor D C} →
                (F ⊣ G) →
                  (J : CategoryTheory.GrothendieckTopology C) →
                    (K : CategoryTheory.GrothendieckTopology D) →
                      [inst_3 : F.IsContinuous J K] →
                        [inst_4 : G.IsContinuous K J] →
                          F.sheafPushforwardContinuous E J K ⊣ G.sheafPushforwardContinuous E K J
-- Mathlib.Order.Hom.Set
OrderIso.compl_apply : ∀ (α : Type u_1) [inst : BooleanAlgebra α] (a : α), (OrderIso.compl α) a = (OrderDual.toDual a)ᶜ
-- Mathlib.Order.Basic
/-- Transfer a `LinearOrder` on `β` to a `LinearOrder` on `α` using an injective
function `f : α → β`. This version takes `[Max α]` and `[Min α]` as arguments, then uses
them for `max` and `min` fields. It also takes `[Ord α]` as an argument and uses them for `compare`
fields. See `LinearOrder.lift` for a version that autogenerates `compare` fields, and
`LinearOrder.liftWithOrd'` for one that auto-generates `min` and `max` fields.
fields. See note [reducible non-instances].  -/
LinearOrder.liftWithOrd : {α : Type u_2} →
  {β : Type u_3} →
    [inst : LinearOrder β] →
      [inst_1 : Max α] →
        [inst_2 : Min α] →
          [inst_3 : Ord α] →
            (f : α → β) →
              Function.Injective f →
                (∀ (x y : α), f (x ⊔ y) = max (f x) (f y)) →
                  (∀ (x y : α), f (x ⊓ y) = min (f x) (f y)) →
                    (∀ (a b : α), compare a b = compare (f a) (f b)) → LinearOrder α
-- Mathlib.Logic.Equiv.Defs
EquivLike.coe_symm_apply_apply : ∀ {α : Sort u} {β : Sort v} {F : Sort u_1} [inst : EquivLike F α β] (e : F) (x : α), (↑e).symm (e x) = x
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.truncTotal_pow_eq_truncTotal_truncTotal_pow : ∀ {σ : Type u_1} {R : Type u_2} {n m : ℕ} [inst : Finite σ] [inst_1 : CommSemiring R] (p : MvPowerSeries σ R),
  (MvPowerSeries.truncTotal n) (p ^ m) = (MvPowerSeries.truncTotal n) (↑((MvPowerSeries.truncTotal n) p) ^ m)
-- Mathlib.Analysis.Normed.Group.Quotient
/-- The quotient norm satisfies the triangle inequality.  -/
quotient_norm_add_le : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] (S : AddSubgroup M) (x y : M ⧸ S), ‖x + y‖ ≤ ‖x‖ + ‖y‖
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min?_erase_eq_iff_not_compare_eq_min? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (t.erase k).min? = t.min? ↔ ∀ {km : α}, t.min? = some km → ¬cmp k km = Ordering.eq
-- Mathlib.GroupTheory.Nilpotent
Subgroup.lowerCentralSeries_pi_le : ∀ {η : Type u_2} {Gs : η → Type u_3} [inst : (i : η) → Group (Gs i)] (Ss : (i : η) → Subgroup (Gs i)) (n : ℕ),
  (Subgroup.pi Set.univ Ss).lowerCentralSeries n ≤ Subgroup.pi Set.univ fun i => (Ss i).lowerCentralSeries n
-- Mathlib.Data.Finset.Slice
/-- The `r`-th slice of a set family is the subset of its elements which have cardinality `r`.  -/
Finset.slice : {α : Type u_1} → Finset (Finset α) → ℕ → Finset (Finset α)
-- Mathlib.CategoryTheory.Monoidal.Skeleton
/-- The skeleton of a monoidal category can be viewed as a monoid, where the multiplication is given by
the tensor product, and satisfies the monoid axioms since it is a skeleton.
 -/
CategoryTheory.Skeleton.instMonoid : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.MonoidalCategory C] → Monoid (CategoryTheory.Skeleton C)
-- Mathlib.Algebra.Order.CompleteField
ConditionallyCompleteLinearOrderedField.inducedMap_one : ∀ (α : Type u_2) (β : Type u_3) [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Field β]
  [inst_4 : ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α],
  ConditionallyCompleteLinearOrderedField.inducedMap α β 1 = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- The `∐` functor composed with the pointwise constant functor `Π i, I i ⥤ (α → C)` is isomorphic
to the constant functor with value `∐ X`.  -/
CategoryTheory.Limits.Sigma.constCompSigmaIsoConst : {α : Type w₂} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Limits.HasCoproductsOfShape α C] →
        {I : α → Type u_1} →
          [inst_2 : (i : α) → CategoryTheory.Category.{v_1, u_1} (I i)] →
            (X : α → C) →
              (CategoryTheory.Functor.pi fun i => (CategoryTheory.Functor.const (I i)).obj (X i)).comp
                  (CategoryTheory.Limits.Sigma.functor α) ≅
                (CategoryTheory.Functor.const ((i : α) → I i)).obj (∐ X)
-- Mathlib.LinearAlgebra.Projection
/-- Given an idempotent linear operator `p`, we have
`x ∈ range p` if and only if `p(x) = x` for all `x`.  -/
LinearMap.IsIdempotentElem.mem_range_iff : ∀ {S : Type u_5} [inst : Semiring S] {M : Type u_6} [inst_1 : AddCommMonoid M] [inst_2 : Module S M] {p : M →ₗ[S] M},
  IsIdempotentElem p → ∀ {x : M}, x ∈ p.range ↔ p x = x
-- Mathlib.Order.RelIso.Basic
/-- `Sum.inl` as a relation embedding into `Sum.Lex r s`.  -/
RelEmbedding.sumLexInl : {α : Type u_1} → {β : Type u_2} → (r : α → α → Prop) → (s : β → β → Prop) → r ↪r Sum.Lex r s
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.functorL₁_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), CategoryTheory.ShortComplex.SnakeInput.functorL₁.obj S = S.L₁
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.FreeGroupoid.instIsLocalizationOfTopMorphismProperty : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], (CategoryTheory.FreeGroupoid.of C).IsLocalization ⊤
-- Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
/-- The Yoneda embedding `Grp C ⥤ Cᵒᵖ ⥤ GrpCat.{w}` for a locally `w`-small category `C`.  -/
CategoryTheory.shrinkYonedaGrp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.LocallySmall.{w, v, u} C] →
      [inst_2 : CategoryTheory.CartesianMonoidalCategory C] →
        CategoryTheory.Functor (CategoryTheory.Grp C) (CategoryTheory.Functor Cᵒᵖ GrpCat)
-- Mathlib.Analysis.Normed.Operator.Extend
LinearEquiv.extend_symm_apply : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} {Fₗ : Type u_6}
  [inst : NormedDivisionRing 𝕜] [inst_1 : NormedDivisionRing 𝕜₂] [inst_2 : AddCommGroup E]
  [inst_3 : NormedAddCommGroup Eₗ] [inst_4 : AddCommGroup F] [inst_5 : NormedAddCommGroup Fₗ] [inst_6 : Module 𝕜 E]
  [inst_7 : Module 𝕜 Eₗ] [inst_8 : IsBoundedSMul 𝕜 Eₗ] [inst_9 : Module 𝕜₂ F] [inst_10 : Module 𝕜₂ Fₗ]
  [inst_11 : IsBoundedSMul 𝕜₂ Fₗ] [inst_12 : CompleteSpace Eₗ] [inst_13 : CompleteSpace Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂}
  {σ₂₁ : 𝕜₂ →+* 𝕜} [inst_14 : RingHomInvPair σ₁₂ σ₂₁] [inst_15 : RingHomInvPair σ₂₁ σ₁₂] (f : E ≃ₛₗ[σ₁₂] F)
  (e₁ : E →ₗ[𝕜] Eₗ) (e₂ : F →ₗ[𝕜₂] Fₗ) (h_dense₁ : DenseRange ⇑e₁) (h_norm₁ : ∃ C, ∀ (x : E), ‖e₂ (f x)‖ ≤ C * ‖e₁ x‖)
  (h_dense₂ : DenseRange ⇑e₂) (h_norm₂ : ∃ C, ∀ (x : F), ‖e₁ (f.symm x)‖ ≤ C * ‖e₂ x‖) (x : Fₗ),
  (f.extend e₁ e₂ h_dense₁ h_norm₁ h_dense₂ h_norm₂).symm x = ((e₁ ∘ₛₗ ↑f.symm).extendOfNorm e₂) x