mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Antisymmetrization
/-- **Alias** of `AntisymmRel.of_eq`. -/
Eq.antisymmRel : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Refl r] {a b : α}, a = b → AntisymmRel r a b
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
linearIndepOn_biUnion_of_directed : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {η : Type u_6} {s : Set η} {t : η → Set ι},
  DirectedOn (t ⁻¹'o fun x1 x2 => x1 ⊆ x2) s → (∀ a ∈ s, LinearIndepOn R v (t a)) → LinearIndepOn R v (⋃ a ∈ s, t a)
-- Mathlib.Data.WSeq.Basic
/-- Turn a stream into a weak sequence  -/
Stream'.WSeq.ofStream : {α : Type u} → Stream' α → Stream'.WSeq α
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.Theory.isSatisfiable_directed_union_iff : ∀ {L : FirstOrder.Language} {ι : Type u_1} [Nonempty ι] {T : ι → L.Theory},
  Directed (fun x1 x2 => x1 ⊆ x2) T →
    (FirstOrder.Language.Theory.IsSatisfiable (⋃ i, T i) ↔ ∀ (i : ι), (T i).IsSatisfiable)
-- Mathlib.Logic.IsEmpty.Basic
isEmpty_psum : ∀ {α : Sort u_4} {β : Sort u_5}, IsEmpty (α ⊕' β) ↔ IsEmpty α ∧ IsEmpty β
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Closeds.uniformContinuous_sup : ∀ {α : Type u_1} [inst : UniformSpace α], UniformContinuous fun x => x.1 ⊔ x.2
-- Mathlib.Analysis.Convex.Side
AffineSubspace.sOppSide_lineMap_right : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P}, x ∈ s → y ∉ s → ∀ {t : R}, t < 0 → s.SOppSide y ((AffineMap.lineMap x y) t)
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.right_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {A B : CategoryTheory.Mon C} (self : Bimod A B),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft self.X CategoryTheory.MonObj.mul) self.actRight =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator self.X B.X B.X).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight self.actRight B.X)
        self.actRight)
-- Mathlib.Algebra.LinearRecurrence
/-- `E.mkSol` indeed gives solutions to `E`.  -/
LinearRecurrence.is_sol_mkSol : ∀ {R : Type u_1} [inst : CommSemiring R] (E : LinearRecurrence R) (init : Fin E.order → R), E.IsSolution (E.mkSol init)
-- Mathlib.Data.W.Constructions
WType.instInhabitedListβCons : (γ : Type u) → (hd : γ) → Inhabited (WType.Listβ γ (WType.Listα.cons hd))
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- Measures are partially ordered.  -/
MeasureTheory.Measure.instPartialOrder : {α : Type u_1} → {x : MeasurableSpace α} → PartialOrder (MeasureTheory.Measure α)
-- Mathlib.Data.Set.Basic
Set.union_eq_union_iff_right : ∀ {α : Type u} {s t u : Set α}, s ∪ u = t ∪ u ↔ s ⊆ t ∪ u ∧ t ⊆ s ∪ u
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.leftOp_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C Dᵒᵖ) {X Y : Cᵒᵖ} (f : X ⟶ Y), F.leftOp.map f = (F.map f.unop).unop
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instAddRightCancelMonoid : {α : Type u_1} → [AddRightCancelMonoid α] → AddRightCancelMonoid αᵒᵈ
-- Mathlib.RingTheory.Ideal.Height
/-- The height of the maximal ideal equals the Krull dimension in a local ring.  -/
IsLocalRing.maximalIdeal_height_eq_ringKrullDim : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R], ↑(IsLocalRing.maximalIdeal R).height = ringKrullDim R
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- Cache for diagonal-tail certificates, keyed by recursion index and lower bound.  -/
Mathlib.Tactic.Determinant.CertCache.diagCache : {u : Lean.Level} →
  {α : Q(Type u)} →
    {rα : Q(CommRing «$α»)} →
      Mathlib.Tactic.Determinant.CertCache rα → Std.HashMap (ℕ × ℕ) (Mathlib.Tactic.Determinant.Cert rα)
-- Mathlib.Data.ENNReal.Operations
ENNReal.iSup_natCast : ⨆ n, ↑n = ⊤
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
/-- The interior of a simplex is the set of points that can be expressed as an affine combination
of the vertices with weights strictly between 0 and 1. This is equivalent to the intrinsic
interior of the convex hull of the vertices.  -/
Affine.Simplex.interior : {k : Type u_1} →
  {V : Type u_2} →
    {P : Type u_4} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module k V] → [inst_3 : AddTorsor V P] → [PartialOrder k] → {n : ℕ} → Affine.Simplex k P n → Set P
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.finrank_corootSpanIn : ∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] (K : Type u_7)
  {L : Type u_8} [inst_2 : Field K] [inst_3 : Field L] [inst_4 : Algebra K L] [inst_5 : Module L M]
  [inst_6 : Module L N] [inst_7 : Module K M] [inst_8 : Module K N] [IsScalarTower K L M] [IsScalarTower K L N]
  (Q : RootPairing ι L M N) [Q.IsRootSystem] [Q.IsValuedIn K], Module.finrank K ↥(Q.corootSpan K) = Module.finrank L N
-- Mathlib.RingTheory.Algebraic.StronglyTranscendental
/-- We say that `x : S` is strongly transcendental over `R` if
forall `u : S` and all `p : R[X]`, `p(x) * u = 0 → p * u = 0`.
If `S` is a domain, and `R ⊆ S`, this is equivalent to the image of `x` in `Frac(S)` being
transcendental over `R`. See `IsStronglyTranscendental.iff_of_isFractionRing`.
 -/
IsStronglyTranscendental : (R : Type u_1) → {S : Type u_2} → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → S → Prop
-- Mathlib.Computability.Primrec.List
_private.Mathlib.Computability.Primrec.List.0.list_casesOn' : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  (H : Nat.Primrec fun n => Encodable.encode (Encodable.decode n)) {f : α → List β} {g : α → σ}
  {h : α → β × List β → σ},
  Primrec f → Primrec g → Primrec₂ h → Primrec fun a => List.casesOn (f a) (g a) fun b l => h a (b, l)
-- Mathlib.Order.Preorder.Chain
IsMaxChain.nonempty_iff : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, IsMaxChain r s → (Nonempty α ↔ s.Nonempty)
-- Mathlib.GroupTheory.Exponent
Monoid.exponent_eq_zero_iff : ∀ {G : Type u} [inst : Monoid G], Monoid.exponent G = 0 ↔ ¬Monoid.ExponentExists G
-- Mathlib.Data.Set.Constructions
FiniteInter.finiteInterClosure.univ : ∀ {α : Type u_1} {S : Set (Set α)}, FiniteInter.finiteInterClosure S Set.univ
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.SymmetricCategory.tensorμ_braid_swap_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.SymmetricCategory C] (X Y : C) {Z : C}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
        (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ X X Y Y)
      (CategoryTheory.CategoryStruct.comp
        (β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
            (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).hom
        h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (β_ X X).hom (β_ Y Y).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ X X Y Y) h)
-- Mathlib.Data.Finsupp.Order
Finsupp.instSMulPosReflectLT : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Zero α] [inst_1 : PartialOrder α] [inst_2 : Zero β]
  [inst_3 : PartialOrder β] [inst_4 : SMulWithZero α β] [SMulPosReflectLT α β], SMulPosReflectLT α (ι →₀ β)
-- Mathlib.Algebra.Ring.Basic
AddHom.mulLeft_apply : ∀ {R : Type u_1} [inst : Distrib R] (r : R), ⇑(AddHom.mulLeft r) = fun x => r * x
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.inv_hom_apply : ∀ (R : Type u) [inst : CommRing R] {A B : AlgCat R} (e : A ≅ B) (x : ↑A),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
-- Init.Data.Int.DivMod.Bootstrap
Int.ediv.eq_3 : ∀ (a : ℕ), (Int.negSucc a).ediv 0 = 0
-- Lean.Meta.Tactic.Grind.Types
/-- Macro similar to `trace[...]`, but it includes the trace message `trace[grind] "working on <current goal>"`
if the tag has changed since the last trace message.
 -/
Lean.Meta.Grind.«doElemTrace_goal[_]__» : Lean.ParserDescr
-- Lean.Data.Lsp.Window
Lean.Lsp.MessageType.log.sizeOf_spec : sizeOf Lean.Lsp.MessageType.log = 1
-- Init.Data.List.Find
List.isSome_findFinIdx? : ∀ {α : Type u_1} {l : List α} {p : α → Bool}, (List.findFinIdx? p l).isSome = l.any p
-- Init.Data.Order.FactoriesExtra
/-- Creates an `LE α` instance from an `Ord α` instance.

`OrientedOrd α` must be satisfied so that the resulting `LE α` instance faithfully represents
the `Ord α` instance.
 -/
LE.ofOrd : (α : Type u) → [Ord α] → LE α
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k k' : α}
  [hi : Inhabited β] {f : β → β},
  (t.modify k f)[k']! = if cmp k k' = Ordering.eq then (Option.map f t[k]?).get! else t[k']!
-- Mathlib.Topology.Instances.AddCircle.Real
AddCircle.pathConnectedSpace : ∀ (p : ℝ), PathConnectedSpace (AddCircle p)
-- Mathlib.Probability.Martingale.BorelCantelli
MeasureTheory.StronglyAdapted.isStoppingTime_leastGE : ∀ {ι : Type u_1} {Ω : Type u_2} {β : Type u_3} {m0 : MeasurableSpace Ω} [inst : ConditionallyCompleteLinearOrderBot ι]
  {ℱ : MeasureTheory.Filtration ι m0} [WellFoundedLT ι] [Countable ι] [inst_3 : TopologicalSpace β]
  [inst_4 : Preorder β] [ClosedIciTopology β] [TopologicalSpace.PseudoMetrizableSpace β] [inst_7 : MeasurableSpace β]
  [BorelSpace β] {f : ι → Ω → β} (r : β),
  MeasureTheory.StronglyAdapted ℱ f → MeasureTheory.IsStoppingTime ℱ (MeasureTheory.leastGE f r)
-- Init.Data.Range.Basic
_private.Init.Data.Range.Basic.0.Std.Legacy.Range.forIn'.loop.match_1.eq_2 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.yield b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_2 b
-- Mathlib.CategoryTheory.Products.Unitor
/-- The equivalence of categories expressing right unity of products of categories.  -/
CategoryTheory.prod.rightUnitorEquivalence : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → C × CategoryTheory.Discrete PUnit.{w + 1} ≌ C
-- Mathlib.Analysis.Normed.Operator.Basic
/-- Continuous linear maps are locally bounded. In other words, they map bounded sets to bounded sets.
 -/
ContinuousLinearMap.instLocallyBoundedMapClass : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂],
  LocallyBoundedMapClass (E →SL[σ₁₂] F) E F
-- Mathlib.CategoryTheory.Endomorphism
CategoryTheory.End.inhabited : {C : Type u} → [inst : CategoryTheory.CategoryStruct.{v, u} C] → (X : C) → Inhabited (CategoryTheory.End X)
-- Std.Async.DNS
Std.Async.DNS.NameInfo.mk.injEq : ∀ (host service host_1 service_1 : String),
  ({ host := host, service := service } = { host := host_1, service := service_1 }) =
    (host = host_1 ∧ service = service_1)
-- Mathlib.Order.Filter.CountablyGenerated
Filter.IsCountablyGenerated.mk : ∀ {α : Type u_1} {f : Filter α}, (∃ s, s.Countable ∧ f = Filter.generate s) → f.IsCountablyGenerated
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.iExs.congr_simp : ∀ {L : FirstOrder.Language} {α : Type u'} (β : Type v') [inst : Finite β] (φ φ_1 : L.Formula (α ⊕ β)),
  φ = φ_1 → FirstOrder.Language.Formula.iExs β φ = FirstOrder.Language.Formula.iExs β φ_1
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.restr_eqOnSource_of_eqOn : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e e' : OpenPartialHomeomorph X Y} {s : Set X},
  Set.EqOn (↑e) (↑e') (e'.source ∩ interior s) →
    e'.source ∩ interior s ⊆ e.source → e.restr (e'.source ∩ interior s) ≈ e'.restr s
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.orbitRel.Quotient.mem_orbit : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {a : α}
  {x : AddAction.orbitRel.Quotient G α}, a ∈ x.orbit ↔ Quotient.mk'' a = x
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.containsThenInsert.size : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → ℕ
-- Init.Data.Stream
Std.Stream.forIn : {ρ : Type u_1} →
  {α : Type u_2} →
    {m : Type u_3 → Type u_4} → {β : Type u_3} → [Std.Stream ρ α] → [Monad m] → ρ → β → (α → β → m (ForInStep β)) → m β
-- Mathlib.Analysis.Convex.Gauge
self_subset_setOfPred_gauge_le_one : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E}, s ⊆ {x | gauge s x ≤ 1}
-- Mathlib.Analysis.Complex.Harmonic.MeanValue
/-- **Alias** of `InnerProductSpace.HarmonicContOnCl.circleAverage_eq`.

---

The Mean Value Property of harmonic functions: If f : ℂ → F is harmonic on a disc of radius
|R| and center c and continuous on its closure, then the circle average circleAverage f c R
equals f c.
 -/
HarmonicContOnCl.circleAverage_eq : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] [CompleteSpace F] {f : ℂ → F} {c : ℂ} {R : ℝ},
  InnerProductSpace.HarmonicContOnCl f (Metric.ball c |R|) → Real.circleAverage f c R = f c
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.mk'_linear : ∀ {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 → P2) (f' : V1 →ₗ[k] V2) (p : P1)
  (h : ∀ (p' : P1), f p' = f' (p' -ᵥ p) +ᵥ f p), (AffineMap.mk' f f' p h).linear = f'
-- Mathlib.Algebra.Group.Commute.Units
AddUnits.nsmul_ofNSMulEqZero : ∀ {M : Type u_1} [inst : AddMonoid M] {n : ℕ} {a : M} (ha : n • a = 0) (hn : n ≠ 0),
  n • AddUnits.ofNSMulEqZero a n ha hn = 0
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- Lax functoriality.  -/
CategoryTheory.Lax.LaxTrans.naturality_comp_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (self : CategoryTheory.Lax.LaxTrans F G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c)
  {Z : F.obj a ⟶ G.obj c}
  (h : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CategoryStruct.comp f g)) (self.app c) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapComp f g))
      (CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.comp f g)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (self.app a) (G.map f) (G.map g)).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.naturality f) (G.map g))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (self.app b) (G.map g)).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.naturality g))
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (self.app c)).inv
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (self.app c))
                h)))))
-- Mathlib.Topology.LocallyClosed
coborder_eq_univ_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, coborder s = Set.univ ↔ IsClosed s
-- Mathlib.RingTheory.Etale.Basic
Algebra.FormallyEtale.instFormallySmooth : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.FormallyEtale R A], Algebra.FormallySmooth R A
-- Lean.Meta.WrapInstance
_private.Lean.Meta.WrapInstance.0.Lean.Meta.getFieldOrigin : Lean.Name → Lean.Name → Lean.MetaM (Lean.Name × Lean.StructureFieldInfo)
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
List.cycleType_formPerm : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α}, l.Nodup → 2 ≤ l.length → l.attach.formPerm.cycleType = {l.length}
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.mem_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  m₁.Equiv m₂ → (k ∈ m₁ ↔ k ∈ m₂)
-- Mathlib.CategoryTheory.SmallRepresentatives
/-- objects  -/
CategoryTheory.SmallCategoryOfSet.obj : {Ω : Type w} → CategoryTheory.SmallCategoryOfSet Ω → Set Ω
-- Init.Omega.Int
Lean.Omega.Int.le_of_not_gt : ∀ {x y : ℤ}, ¬y > x → y ≤ x
-- Std.Data.TreeSet.Raw.WF
Std.TreeSet.Raw.WF.diff : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {t₁ t₂ : Std.TreeSet.Raw α cmp}, t₁.WF → (t₁ \ t₂).WF
-- Plausible.Gen
/-- Lift `BoundedRandom.randomR` to the `Gen` monad.  -/
Plausible.Gen.choose : (α : Type u) →
  [inst : LE α] → [Plausible.BoundedRandom Id α] → (lo hi : α) → lo ≤ hi → Plausible.Gen { a // lo ≤ a ∧ a ≤ hi }
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.fract.congr_simp : ∀ {ι : Type u_3} {s s_1 : Set (ι → ℕ)} (e_s : s = s_1) (hs : IsProperLinearSet s) [inst : Finite ι] (x x_1 : ι → ℕ),
  x = x_1 → ∀ (a a_1 : ι), a = a_1 → IsProperLinearSet.fract✝ hs x a = IsProperLinearSet.fract✝ ⋯ x_1 a_1
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgCat.toCoalgHom_id : ∀ {R : Type u} [inst : CommRing R] {M : CoalgCat R},
  CoalgCat.Hom.toCoalgHom (CategoryTheory.CategoryStruct.id M) = CoalgHom.id R ↑M.toModuleCat
-- Mathlib.Analysis.Complex.PhragmenLindelof
/-- **Phragmen-Lindelöf principle** in the first quadrant. Let `f g : ℂ → E` be functions such that

* `f` and `g` are differentiable in the open first quadrant and are continuous on its closure;
* `‖f z‖` and `‖g z‖` are bounded from above by `A * exp(B * ‖z‖ ^ c)` on the open first
  quadrant for some `A`, `B`, and `c < 2`;
* `f` is equal to `g` on the boundary of the first quadrant.

Then `f` is equal to `g` on the closed first quadrant.  -/
PhragmenLindelof.eqOn_quadrant_I : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : ℂ → E},
  DiffContOnCl ℂ f (Set.Ioi 0 ×ℂ Set.Ioi 0) →
    (∃ c < 2,
        ∃ B, f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Ioi 0 ×ℂ Set.Ioi 0)] fun z => Real.exp (B * ‖z‖ ^ c)) →
      DiffContOnCl ℂ g (Set.Ioi 0 ×ℂ Set.Ioi 0) →
        (∃ c < 2,
            ∃ B,
              g =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Ioi 0 ×ℂ Set.Ioi 0)] fun z => Real.exp (B * ‖z‖ ^ c)) →
          (∀ (x : ℝ), 0 ≤ x → f ↑x = g ↑x) →
            (∀ (x : ℝ), 0 ≤ x → f (↑x * Complex.I) = g (↑x * Complex.I)) → Set.EqOn f g {z | 0 ≤ z.re ∧ 0 ≤ z.im}
-- Mathlib.Analysis.Distribution.DerivNotation
ContinuousLineDeriv.mk : ∀ {V : Type u} {E : Type v} {F : outParam (Type w)} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace F]
  [inst_2 : LineDeriv V E F], (∀ (v : V), Continuous (LineDeriv.lineDerivOp v)) → ContinuousLineDeriv V E F
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- If `Y` has a left dual `ᘁY`, then it is a closed object, with the internal hom functor `Y ⟶[C] -`
given by left tensoring by `ᘁY`.
This has to be a definition rather than an instance to avoid diamonds, for example between
`category_theory.monoidal_closed.functor_closed` and
`CategoryTheory.Monoidal.functorHasLeftDual`. Moreover, in concrete applications there is often
a more useful definition of the internal hom object than `ᘁY ⊗ X`, in which case the closed
structure shouldn't come from `HasLeftDual` (e.g. in the category `FinVect k`, it is more
convenient to define the internal hom as `Y →ₗ[k] X` rather than `ᘁY ⊗ X` even though these are
naturally isomorphic).
 -/
CategoryTheory.closedOfHasLeftDual : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → (Y : C) → [CategoryTheory.HasLeftDual Y] → CategoryTheory.Closed Y
-- Mathlib.Geometry.Manifold.Immersion
/-- If `f` is an immersion, it is an immersion at each point.  -/
Manifold.IsImmersionOfComplement.isImmersionAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M]
  {N : Type u_13} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N},
  Manifold.IsImmersionOfComplement F I J n f → ∀ (x : M), Manifold.IsImmersionAtOfComplement F I J n f x
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.eq_C_of_derivative_eq_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} [IsAddTorsionFree R],
  Polynomial.derivative p = 0 → p = Polynomial.C (p.coeff 0)
-- Mathlib.RingTheory.Congruence.Hom
RingCon.quotientQuotientEquivQuotient_coe_coe : ∀ {M : Type u_1} [inst : NonAssocSemiring M] (c d : RingCon M) (h : c ≤ d) (x : M),
  (c.quotientQuotientEquivQuotient d h) ↑↑x = ↑x
-- Mathlib.Algebra.Order.Hom.Monoid
/-- The identity map as an ordered monoid isomorphism.  -/
OrderMonoidIso.refl : (α : Type u_2) → [inst : Preorder α] → [inst_1 : Mul α] → α ≃*o α
-- Mathlib.Topology.OmegaCompletePartialOrder
Scott.IsωSup.eq_1 : ∀ {α : Type u} [inst : Preorder α] (c : OmegaCompletePartialOrder.Chain α) (x : α),
  Scott.IsωSup c x = ((∀ (i : ℕ), c i ≤ x) ∧ ∀ (y : α), (∀ (i : ℕ), c i ≤ y) → x ≤ y)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_eq_default : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {a : α}, a ∉ m → m.getKey! a = default
-- Mathlib.LinearAlgebra.SymplecticGroup
SymplecticGroup.mem_iff' : ∀ {l : Type u_1} {R : Type u_2} [inst : DecidableEq l] [inst_1 : Fintype l] [inst_2 : CommRing R]
  {A : Matrix (l ⊕ l) (l ⊕ l) R}, A ∈ Matrix.symplecticGroup l R ↔ A.transpose * Matrix.J l R * A = Matrix.J l R
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.baseChange_negPolynomial : ∀ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : CommRing B] {W' : WeierstrassCurve.Affine R} [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B),
  (W'.baseChange B).negPolynomial = Polynomial.map (Polynomial.mapRingHom ↑f) (W'.baseChange A).negPolynomial
-- Mathlib.RingTheory.DedekindDomain.Instances
instIsScalarTowerAtPrimeFractionRing : ∀ {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] {P : Ideal R} [inst_5 : P.IsPrime] [inst_6 : FaithfulSMul R S],
  IsScalarTower (Localization.AtPrime P) (FractionRing R) (FractionRing S)
-- Mathlib.RingTheory.MvPowerSeries.Inverse
MvPowerSeries.inv_eq_zero : ∀ {σ : Type u_1} {k : Type u_3} [inst : Field k] {φ : MvPowerSeries σ k}, φ⁻¹ = 0 ↔ MvPowerSeries.constantCoeff φ = 0
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.mul_add_div_left : ∀ {R : Type u} [inst : EuclideanDomain R] (x y z : R), z ≠ 0 → z ∣ y → (z * x + y) / z = x + y / z
-- Mathlib.Tactic.Attr.Register
/-- Simplification procedure  -/
Parser.Attr.zify_simps_proc : Lean.ParserDescr
-- Init.Data.Array.Erase
Array.getElem_eraseIdx_of_lt : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} (w : i < xs.size) {j : ℕ} (h : j < (xs.eraseIdx i w).size) (h' : j < i),
  (xs.eraseIdx i w)[j] = xs[j]