mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Polynomial.Chebyshev.integrable_measureT : ∀ {f : ℝ → ℝ}, ContinuousOn f (Set.Icc (-1) 1) → MeasureTheory.Integrable f Polynomial.Chebyshev.measureT
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_roo_eq_singleton : ∀ {m n : ℤ}, n = m + 2 → (m<...n).toList = [m + 1]
-- Std.Internal.Do.Triple.SpecLemmas
_private.Std.Internal.Do.Triple.SpecLemmas.0.List.forIn'_cons.match_1.splitter : {β : Type u_1} →
  (motive : ForInStep β → Sort u_2) →
    (x : ForInStep β) → ((b : β) → motive (ForInStep.done b)) → ((b : β) → motive (ForInStep.yield b)) → motive x
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_of_mem_keys : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {a : α},
  a ∈ Std.Internal.List.keys l → Std.Internal.List.containsKey a l = true
-- Mathlib.CategoryTheory.Endomorphism
CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_apply_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {f : CategoryTheory.Functor C D} (hf : f.FullyFaithful) (X : C) (i : X ≅ X),
  ((hf.autMulEquivOfFullyFaithful X) i).hom = f.map i.hom
-- Mathlib.Analysis.Convex.Segment
openSegment_subset_iff_segment_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [ZeroLEOneClass 𝕜] [inst_4 : Module 𝕜 E] {s : Set E} {x y : E},
  x ∈ s → y ∈ s → (openSegment 𝕜 x y ⊆ s ↔ segment 𝕜 x y ⊆ s)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.isEmpty_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α fun x => Unit} [EquivBEq α] [LawfulHashable α]
  {l : List α}, (Std.DHashMap.Const.insertManyIfNewUnit m l).isEmpty = (m.isEmpty && l.isEmpty)
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.IsUniformizer.val_ne_zero : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : Ring A] {v : Valuation A Γ}
  [hv : v.IsRankOneDiscrete] {π : A}, v.IsUniformizer π → v π ≠ 0
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imJ_zero : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : Zero R], QuaternionAlgebra.imJ 0 = 0
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Returns `ULift.up true` if the monadic predicate `p` returns `ULift.up true` for
all elements emitted by the iterator `it`.

`O(|it|)`. Short-circuits upon encountering the first mismatch. The outputs of `it` are
examined in order of iteration.

This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `IterM.allM`.
 -/
Std.IterM.Total.allM : {α β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α m β] →
        [Std.IteratorLoop α m m] →
          [Std.Iterators.Finite α m] → (β → m (ULift.{w, 0} Bool)) → Std.IterM.Total m β → m (ULift.{w, 0} Bool)
-- Mathlib.Order.WithBotTop
/-- The type of extended integers `[-∞, ∞]`, constructed as `WithBot (WithTop ℤ)`.  -/
EInt : Type
-- Mathlib.NumberTheory.Modular
/-- Given `coprime_pair` `p=(c,d)`, the matrix `[[a,b],[*,*]]` is sent to `a*c+b*d`.
This is the linear map version of this operation.
 -/
ModularGroup.lcRow0 : (Fin 2 → ℤ) → Matrix (Fin 2) (Fin 2) ℝ →ₗ[ℝ] ℝ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.inter_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ m₃ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₃.WF → m₂.Equiv m₃ → (m₁ ∩ m₂).Equiv (m₁ ∩ m₃)
-- Mathlib.Order.Filter.Lift
Filter.lift'_mono' : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {h₁ h₂ : Set α → Set β}, (∀ s ∈ f, h₁ s ⊆ h₂ s) → f.lift' h₁ ≤ f.lift' h₂
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.foldl_toArray : ∀ {m : Type w → Type u_1} {γ α β : Type w} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β}
  {f : γ → β → γ} {init : γ}, (fun x => Array.foldl f init x) <$> it.toArray = Std.IterM.fold f init it
-- Mathlib.Algebra.Order.SuccPred
monotoneOn_of_sub_one_le : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : Sub α] [inst_3 : One α]
  [inst_4 : PredSubOrder α] [IsPredArchimedean α] {s : Set α} {f : α → β},
  s.OrdConnected → (∀ (a : α), ¬IsMin a → a ∈ s → a - 1 ∈ s → f (a - 1) ≤ f a) → MonotoneOn f s
-- Mathlib.RingTheory.FreeCommRing
FreeCommRing.isSupported_int : ∀ {α : Type u} {i : ℤ} {s : Set α}, (↑i).IsSupported s
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.ker_orthogonalProjectionOnto : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection], (↑K.orthogonalProjectionOnto).ker = Kᗮ
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.mem_sInf_iff : ∀ {α : Type u_1} [inst : LE α] {S : Set (LowerSet α)} {a : α}, a ∈ sInf S ↔ ∀ s ∈ S, a ∈ s
-- Mathlib.Order.Concept
Concept.extent_injective : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop}, Function.Injective Concept.extent
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.polar_smul_left : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticMap R M N) (a : R) (x y : M),
  QuadraticMap.polar (⇑Q) (a • x) y = a • QuadraticMap.polar (⇑Q) x y
-- Lean.Parser.Term
/-- Useful for syntax quotations. Note that generic patterns such as `` `(matchAltExpr| | ... => $rhs) `` should also
work with other `rhsParser`s (of arity 1).  -/
Lean.Parser.Term.matchAltExpr : Lean.Parser.Parser
-- Mathlib.Order.RelSeries
RelSeries.mem_snoc : ∀ {α : Type u_1} {r : SetRel α α} {p : RelSeries r} {newLast : α} {rel : (p.last, newLast) ∈ r} {x : α},
  x ∈ p.snoc newLast rel ↔ x ∈ p ∨ x = newLast
-- Init.Data.BitVec.Lemmas
BitVec.toInt_neg_of_ne_intMin : ∀ {w : ℕ} {x : BitVec w}, x ≠ BitVec.intMin w → (-x).toInt = -x.toInt
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex_p : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex._auto_3),
  (X.rightHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).p = X.pOpcycles f₂ f₃ n₁
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.instReprOverlaps.repr : Lean.Meta.Match.Overlaps → ℕ → Std.Format
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.instPartialOrder : {G : Type u_1} → [inst : Group G] → PartialOrder (Subgroup G)
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Continuous.const_cpow : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℂ} {b : ℂ},
  Continuous f → (b ≠ 0 ∨ ∀ (a : α), f a ≠ 0) → Continuous fun x => b ^ f x
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The product of an antitone function and a strictly antitone function is strictly antitone.  -/
Antitone.mul_strictAnti' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] [MulLeftStrictMono α]
  [MulRightMono α] {f g : β → α}, Antitone f → StrictAnti g → StrictAnti fun x => f x * g x
-- Batteries.Recycling.MonadSatisfying.Basic
/-- Lift a `SatisfiesM` predicate to a monadic value.  -/
MonadSatisfying.satisfying : {m : Type u → Type v} →
  {inst : Functor m} →
    {inst_1 : LawfulFunctor m} →
      [self : MonadSatisfying m] → {α : Type u} → {p : α → Prop} → {x : m α} → SatisfiesM p x → m { a // p a }
-- Mathlib.MeasureTheory.Covering.Besicovitch
/-- Radii of the balls  -/
Besicovitch.SatelliteConfig.r : {α : Type u_1} → [inst : MetricSpace α] → {N : ℕ} → {τ : ℝ} → Besicovitch.SatelliteConfig α N τ → Fin N.succ → ℝ
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- A typeclass for when an `AddAction X G` descends to the quotient `G ⧸ H`.  -/
AddAction.QuotientAction : {G : Type u} → (X : Type v) → [inst : AddGroup G] → [inst_1 : AddMonoid X] → [AddAction X G] → AddSubgroup G → Prop
-- Mathlib.Data.Finset.Card
/-- **Pigeonhole principle** for two finsets inside an ambient finset.  -/
Finset.inter_nonempty_of_card_lt_card_add_card : ∀ {α : Type u_1} {s t u : Finset α} [inst : DecidableEq α], t ⊆ s → u ⊆ s → s.card < t.card + u.card → (t ∩ u).Nonempty
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.resultant_succ_left_deg : ∀ {R : Type u_1} [inst : CommRing R] (f g : Polynomial R) (m n : ℕ),
  f.natDegree ≤ m → f.resultant g (m + 1) n = (-1) ^ n * g.coeff n * f.resultant g m n
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.XIsoOfEq_hom_comp_XIsoOfEq_hom_assoc : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι}
  (h₁₂ : p₁ = p₂) (h₂₃ : p₂ = p₃) {Z : V} (h : K.X p₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₁₂).hom (CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₂₃).hom h) =
    CategoryTheory.CategoryStruct.comp (K.XIsoOfEq ⋯).hom h
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.algebraMap_apply' : ∀ {σ : Type u_1} {R : Type u_2} (A : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  (p : MvPolynomial σ R),
  (algebraMap (MvPolynomial σ R) (MvPowerSeries σ A)) p = (MvPowerSeries.map (algebraMap R A)) ↑p
-- Mathlib.Data.List.TakeDrop
List.takeI_nil : ∀ {α : Type u} [inst : Inhabited α] (n : ℕ), List.takeI n [] = List.replicate n default
-- Mathlib.Algebra.Order.Group.Abs
mabs_min_le_max_mabs_mabs : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] {a b : G}, |min a b|ₘ ≤ max |a|ₘ |b|ₘ
-- Batteries.Data.List.Lemmas
List.idxOfNth_mono : ∀ {α : Type u_1} {n m : ℕ} {x : α} [inst : BEq α] {xs : List α}, n ≤ m → List.idxOfNth x xs n ≤ List.idxOfNth x xs m
-- Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_
CommGrpTypeEquivalenceCommGrp.inverse_obj_mul : ∀ {A : CommGrpCat}
  {p :
    (fun X => X)
      (CategoryTheory.MonoidalCategoryStruct.tensorObj (CommGrpTypeEquivalenceCommGrp.inverse.obj A).X
        (CommGrpTypeEquivalenceCommGrp.inverse.obj A).X)},
  (CategoryTheory.ConcreteCategory.hom CategoryTheory.MonObj.mul) p = p.1 * p.2
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.instDist : (p : ℕ) → [inst : Fact (Nat.Prime p)] → Dist ℚ_[p]
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.Hom.birationalOver : ∀ {X U S : AlgebraicGeometry.Scheme} (f : U ⟶ X) [AlgebraicGeometry.IsOpenImmersion f] [AlgebraicGeometry.IsDominant f]
  (sX : X ⟶ S) (sU : U ⟶ S),
  CategoryTheory.CategoryStruct.comp f sX = sU → AlgebraicGeometry.Scheme.BirationalOver sU sX
-- Mathlib.Tactic.Push
/-- `push_neg` rewrites the goal by pushing negations deeper into an expression.
For instance, the goal `¬ ∀ x, ∃ y, x ≤ y` will be transformed by `push_neg` into
`∃ x, ∀ y, y < x`. Binder names are preserved (contrary to what would happen with `simp`
using the relevant lemmas). `push_neg` works as both a tactic and a conv tactic.

`push_neg` is a special case of the more general `push` tactic, namely `push Not`.
The `push` tactic can be extended using the `@[push]` attribute. `push` has special-casing
built in for `push Not`.

Tactics that introduce a negation usually have a version that automatically calls `push_neg` on
that negation. These include `by_cases!`, `contrapose!` and `by_contra!`.

* `push_neg at l1 l2 ...` rewrites at the given locations.
* `push_neg at *` rewrites at each hypothesis and the goal.
* `push_neg +distrib` rewrites `¬ (p ∧ q)` into `¬ p ∨ ¬ q` (by default, the tactic rewrites it
  into `p → ¬ q` instead).

Example:

```lean
example (h : ¬ ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - y₀| ≤ ε) :
    ∃ ε > 0, ∀ δ > 0, ∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀| := by
  push_neg at h
  -- Now we have the hypothesis `h : ∃ ε > 0, ∀ δ > 0, ∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|`
  exact h
```
 -/
Mathlib.Tactic.Push.push_neg : Lean.ParserDescr
-- Mathlib.Data.EReal.Operations
/-- `-a ≤ b` if and only if `-b ≤ a` on `EReal`.  -/
EReal.neg_le : ∀ {a b : EReal}, -a ≤ b ↔ -b ≤ a
-- Mathlib.Data.Fintype.Perm
card_perms_of_finset : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), (permsOfFinset s).card = s.card.factorial
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.length_edges : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.edges.length = p.length
-- Lean.Meta.CongrTheorems
Lean.Meta.congrKindsExt : Lean.MapDeclarationExtension (Array Lean.Meta.CongrArgKind)
-- Lean.Widget.TaggedText
/-- The minimal structure needed to represent "string with interesting (tagged) substrings".
Much like Lean 3 [`sf`](https://github.com/leanprover-community/mathlib/blob/bfa6bbbce69149792cc009ab7f9bc146181dc051/src/tactic/interactive_expr.lean#L38),
but with indentation already stringified.  -/
Lean.Widget.TaggedText : Type u → Type u
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.brecOn.go : {L : FirstOrder.Language} →
  {α : Type u'} →
    {motive : L.Term α → Sort u_1} →
      (t : L.Term α) →
        ((t : L.Term α) → FirstOrder.Language.Term.below t → motive t) → motive t ×' FirstOrder.Language.Term.below t
-- Aesop.Search.Queue.Class
Aesop.Queue.mk : {Q : Type} → BaseIO Q → (Q → Array Aesop.GoalRef → BaseIO Q) → (Q → BaseIO (Option Aesop.GoalRef × Q)) → Aesop.Queue Q
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_keysArray : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → t.keysArray.size = t.size
-- Mathlib.RingTheory.IntegralClosure.GoingDown
Polynomial.coeff_mem_radical_span_coeff_of_dvd : ∀ {R : Type u_1} [inst : CommRing R] (p q : Polynomial R),
  p.Monic →
    q.Monic →
      q ∣ p → ∀ (i : ℕ), i ≠ q.natDegree → q.coeff i ∈ (Ideal.span {x | ∃ i < p.natDegree, p.coeff i = x}).radical
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentColorParams.mk.inj : ∀ {toWorkDoneProgressParams : Lean.Lsp.WorkDoneProgressParams} {toPartialResultParams : Lean.Lsp.PartialResultParams}
  {textDocument : Lean.Lsp.TextDocumentIdentifier} {toWorkDoneProgressParams_1 : Lean.Lsp.WorkDoneProgressParams}
  {toPartialResultParams_1 : Lean.Lsp.PartialResultParams} {textDocument_1 : Lean.Lsp.TextDocumentIdentifier},
  { toWorkDoneProgressParams := toWorkDoneProgressParams, toPartialResultParams := toPartialResultParams,
        textDocument := textDocument } =
      { toWorkDoneProgressParams := toWorkDoneProgressParams_1, toPartialResultParams := toPartialResultParams_1,
        textDocument := textDocument_1 } →
    toWorkDoneProgressParams = toWorkDoneProgressParams_1 ∧
      toPartialResultParams = toPartialResultParams_1 ∧ textDocument = textDocument_1
-- Mathlib.CategoryTheory.Bicategory.Coherence
CategoryTheory.FreeBicategory.normalizeAux.eq_3 : ∀ {B : Type u} [inst : Quiver B] {a : B} (x x_1 : B) (x_2 : Quiver.Path a x) (b : B)
  (f : CategoryTheory.FreeBicategory.Hom x b) (g : CategoryTheory.FreeBicategory.Hom b x_1),
  CategoryTheory.FreeBicategory.normalizeAux x_2 (f.comp g) =
    CategoryTheory.FreeBicategory.normalizeAux (CategoryTheory.FreeBicategory.normalizeAux x_2 f) g
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- The configuration of a TM1 machine is given by the currently
evaluating statement, the variable store value, and the tape.  -/
Turing.TM1.Cfg : (Γ : Type u_1) → Type u_2 → Type u_3 → [Inhabited Γ] → Type (max (max u_1 u_2) u_3)
-- Lean.KeyedDeclsAttribute
/-- Name of a declaration stored in the environment which has type `mkConst Def.valueTypeName`.  -/
Lean.KeyedDeclsAttribute.OLeanEntry.declName : Lean.KeyedDeclsAttribute.OLeanEntry → Lean.Name
-- Init.Control.Option
instMonadControlOptionTOfMonad : {m : Type u_1 → Type u_2} → [Monad m] → MonadControl m (OptionT m)
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
/-- If a simplicial object `X` in an additive category is split,
then `PInfty` vanishes on all the summands of `X _⦋n⦌` which do
not correspond to the identity of `⦋n⦌`.  -/
CategoryTheory.SimplicialObject.Splitting.cofan_inj_comp_PInfty_eq_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (s : X.Splitting) {n : ℕ}
  (A : CategoryTheory.SimplicialObject.Splitting.IndexSet (Opposite.op { len := n })),
  ¬A.EqId →
    CategoryTheory.CategoryStruct.comp ((s.cofan (Opposite.op { len := n })).inj A)
        (AlgebraicTopology.DoldKan.PInfty.f n) =
      0
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.op.eq_1 : ∀ {M : Type u_2} [inst : Add M] (x : AddSubsemigroup M), x.op = { carrier := AddOpposite.unop ⁻¹' ↑x, add_mem' := ⋯ }
-- Mathlib.Algebra.Order.Monovary
MonovaryOn.mul_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : CommGroup β] [inst_2 : LinearOrder β]
  [IsOrderedMonoid β] {s : Set ι} {f : ι → α} {g₁ g₂ : ι → β},
  MonovaryOn f g₁ s → MonovaryOn f g₂ s → MonovaryOn f (g₁ * g₂) s
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.toLinearMap_ofLinearMap : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂}
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (f : M →ₛₗ[σ₁₂] M₂)
  (g : M₂ →ₛₗ[σ₂₁] M) (h₁ : f ∘ₛₗ g = LinearMap.id) (h₂ : g ∘ₛₗ f = LinearMap.id),
  ↑(LinearEquiv.ofLinearMap f g h₁ h₂) = f
-- Mathlib.Topology.Sion
/-- `sublevelLeft X f b z` is contained in either
`sublevelLeft X f b y` or in `sublevelLeft X f b y'`.

The hypotheses imply that `sublevelLeft X f b z` is connected,
and that the two other are disjoint.  -/
_private.Mathlib.Topology.Sion.0.Sion.sublevelLeft_subset_or : ∀ {E : Type u_1} {F : Type u_2} {β : Type u_3} [inst : LinearOrder β] {X : Set E} {Y : Set F} {f : E → F → β}
  [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup E] [IsTopologicalAddGroup E] [inst_4 : Module ℝ E]
  [ContinuousSMul ℝ E] [inst_6 : AddCommGroup F] [inst_7 : Module ℝ F],
  (∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y) →
    (∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X) →
      (∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y) →
        Convex ℝ Y →
          ∀ (a : E) (b : β) (y y' : ↑Y),
            (∀ x ∈ X, max (f a ↑y) (f a ↑y') ≤ max (f x ↑y) (f x ↑y')) →
              b < max (f a ↑y) (f a ↑y') →
                ∀ (z : ↑(segment ℝ ↑y ↑y')),
                  Sion.sublevelLeft✝ X f b ↑z ⊆ Sion.sublevelLeft✝ X f b ↑y ∨
                    Sion.sublevelLeft✝ X f b ↑z ⊆ Sion.sublevelLeft✝ X f b ↑y'
-- Mathlib.Order.Bounded
Set.unbounded_ge_univ : ∀ {α : Type u_1} [inst : LE α] [NoBotOrder α], Set.Unbounded (fun x1 x2 => x1 ≥ x2) Set.univ
-- Init.Data.UInt.Lemmas
UInt32.ofInt_neg_one : UInt32.ofInt (-1) = -1
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.map_ofInv_hom_id_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (W : CategoryTheory.MorphismProperty C) {X Y : C} (s : Y ⟶ X)
  (hs : W s) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L) {Z : D} (h : L.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.LeftFraction.ofInv s hs).map L hL)
      (CategoryTheory.CategoryStruct.comp (L.map s) h) =
    h
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
_private.Mathlib.Analysis.CStarAlgebra.CStarMatrix.0.CStarMatrix.normedAddCommGroupAux : {m : Type u_1} →
  {n : Type u_2} →
    {A : Type u_3} →
      [Fintype m] →
        [Fintype n] →
          [inst : NonUnitalCStarAlgebra A] →
            [inst_1 : PartialOrder A] → [StarOrderedRing A] → NormedAddCommGroup (CStarMatrix m n A)
-- Mathlib.RingTheory.PowerSeries.Order
PowerSeries.coeff_mul_one_sub_of_lt_order : ∀ {R : Type u_2} [inst : Ring R] {φ ψ : PowerSeries R} (n : ℕ),
  ↑n < ψ.order → (PowerSeries.coeff n) (φ * (1 - ψ)) = (PowerSeries.coeff n) φ
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.imageAddHom_apply : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : Add α] [inst_2 : Add β]
  [inst_3 : FunLike F α β] [inst_4 : AddHomClass F α β] (f : F) [inst_5 : DecidableEq β] (s : Finset α),
  (Finset.imageAddHom f) s = Finset.image (⇑f) s
-- Mathlib.RingTheory.FractionalIdeal.Inverse
FractionalIdeal.mul_inv_cancel_iff : ∀ (K : Type u_3) [inst : Field K] {R₁ : Type u_4} [inst_1 : CommRing R₁] [inst_2 : IsDomain R₁] [inst_3 : Algebra R₁ K]
  [inst_4 : IsFractionRing R₁ K] {I : FractionalIdeal (nonZeroDivisors R₁) K}, I * I⁻¹ = 1 ↔ ∃ J, I * J = 1
-- Lean.Elab.App
Lean.Elab.Term.elabPipeProj : Lean.Elab.Term.TermElab
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
/-- The `S`-span of coroots.  -/
RootPairing.corootSpan : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_4} →
      {N : Type u_5} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  RootPairing ι R M N → (S : Type u_6) → [inst : CommRing S] → [inst_5 : Module S N] → Submodule S N
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.isZero_H_obj_mk₁_i₀_le' : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ}
  (X : CategoryTheory.Abelian.SpectralObject C ι)
  (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) [X.HasSpectralSequence data] (r r' : ℤ)
  (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq : κ),
  (∀ (pq' : κ), ¬(c r).Rel pq pq') →
    ∀ (n : ℤ),
      n = data.deg pq + 1 →
        ∀ (i₀' i₀ : ι) (hi₀' : i₀' = data.i₀ r' pq ⋯) (hi₀ : i₀ = data.i₀ r pq ⋯),
          CategoryTheory.Limits.IsZero ((X.H n).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE ⋯)))
-- Init.Data.List.Basic
List.dropWhile_nil : ∀ {α : Type u} {p : α → Bool}, List.dropWhile p [] = []
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.coe_sInf : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] (S : Set (StarSubalgebra R A)),
  ↑(sInf S) = ⋂ s ∈ S, ↑s
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.pos_iff : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  (abv : AbsoluteValue R S) {x : R}, 0 < abv x ↔ x ≠ 0
-- Mathlib.Data.Multiset.Powerset
Multiset.powersetCardAux_nil : ∀ {α : Type u_1} (n : ℕ), Multiset.powersetCardAux (n + 1) [] = []
-- Mathlib.Analysis.Convex.Body
ConvexBody.instSMulNat : {V : Type u_1} →
  [inst : TopologicalSpace V] →
    [inst_1 : AddCommGroup V] → [inst_2 : Module ℝ V] → [ContinuousAdd V] → SMul ℕ (ConvexBody V)
-- Mathlib.Algebra.BigOperators.Expect
Finset.card_smul_expect : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] (s : Finset ι) (f : ι → M),
  (s.card • s.expect fun i => f i) = ∑ i ∈ s, f i
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_subset_compl : ∀ {α : Type u_1} (s t : Set α), s \ t ⊆ tᶜ