mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- Rotation in an oriented real inner product space of dimension 2 can be evaluated in terms of a
complex-number representation of the space.  -/
Orientation.rotation_map_complex : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle) (f : V ≃ₗᵢ[ℝ] ℂ),
  (Orientation.map (Fin 2) f.toLinearEquiv) o = Complex.orientation →
    ∀ (x : V), f ((o.rotation θ) x) = ↑θ.toCircle * f x
-- Mathlib.Topology.Sheaves.PresheafOfFunctions
TopCat.presheafToType_map : ∀ (X : TopCat) {T : Type u_1} {U V : (TopologicalSpace.Opens ↑X)ᵒᵖ} {i : U ⟶ V}
  {f : (fun X => X) ((X.presheafToType T).obj U)},
  (CategoryTheory.ConcreteCategory.hom ((X.presheafToType T).map i)) f = f ∘ ⇑i.unop
-- Mathlib.Order.Lattice.Nat
Set.biInter_le_succ' : ∀ {α : Type u_1} (u : ℕ → Set α) (n : ℕ), ⋂ k, ⋂ (_ : k ≤ n + 1), u k = u 0 ∩ ⋂ k, ⋂ (_ : k ≤ n), u (k + 1)
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.mk_sub_mk : ∀ {K : Type u_1} [inst : Field K] (x y : K) (hx : x ∈ integralClosure ℤ K) (hy : y ∈ integralClosure ℤ K),
  ⟨x, hx⟩ - ⟨y, hy⟩ = ⟨x - y, ⋯⟩
-- Init.Data.Array.Lemmas
Array.eq_replicate_iff : ∀ {α : Type u_1} {a : α} {n : ℕ} {xs : Array α}, xs = Array.replicate n a ↔ xs.size = n ∧ ∀ b ∈ xs, b = a
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.lTensorOne_symm_apply : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {N : Submodule R S}
  (n : ↥N), N.lTensorOne.symm n = 1 ⊗ₜ[R] n
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.instNeg : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_4} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_5} → [inst_4 : AddCommGroup F] → [inst_5 : Module S F] → Neg (E →ₛₗ.[σ] F)
-- Init.Data.String.Lemmas.Splits
String.Slice.copy_sliceTo_eq_iff_exists_splits : ∀ {s : String.Slice} {p : s.Pos} {t₁ : String}, (s.sliceTo p).copy = t₁ ↔ ∃ t₂, p.Splits t₁ t₂
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.Realize.eq_2 : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} (x : ℕ) (x_1 : α → M) (x_2 : Fin x → M)
  (t₁ t₂ : L.Term (α ⊕ Fin x)),
  (FirstOrder.Language.BoundedFormula.equal t₁ t₂).Realize x_1 x_2 =
    (FirstOrder.Language.Term.realize (Sum.elim x_1 x_2) t₁ = FirstOrder.Language.Term.realize (Sum.elim x_1 x_2) t₂)
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxiHasSize_eq : Int64.instRxiHasSize = HasModel.instRxiHasSize✝
-- Init.Data.UInt.IntToBitVec
USize.eq_iff_toBitVec64_eq : ∀ {a b : USize} (h : System.Platform.numBits = 64), a = b ↔ a.toBitVec64 h = b.toBitVec64 h
-- Mathlib.CategoryTheory.Monoidal.Types.Basic
CategoryTheory.leftUnitor_hom_apply : ∀ {X : Type u} {x : X} {p : PUnit.{u + 1}},
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom) (p, x) = x
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- Eta-expanded form of `fderivWithin_id` -/
fderivWithin_fun_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {x : E} {s : Set E} [ContinuousAdd E] [ContinuousSMul 𝕜 E] [T2Space E],
  UniqueDiffWithinAt 𝕜 s x → fderivWithin 𝕜 (fun x => x) s x = ContinuousLinearMap.id 𝕜 E
-- Init.Data.Order.LemmasExtra
Std.min_eq_if_isLE_compare : ∀ {α : Type u} [inst : Ord α] [inst_1 : LE α] {x : Min α} [Std.LawfulOrderOrd α] [Std.LawfulOrderLeftLeaningMin α]
  {a b : α}, a ⊓ b = if (compare a b).isLE = true then a else b
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
measurableSet_bddAbove_range : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_5}
  [Countable ι] {f : ι → δ → α}, (∀ (i : ι), Measurable (f i)) → MeasurableSet {b | BddAbove (Set.range fun i => f i b)}
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.simplex_fst_min : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N) {d : ℕ}
  (hd : x.dim = d), (x.cast hd).simplex.1 (SSet.prodStdSimplex.pairingCore.min x hd) = k.succ
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
/-- If a function is analytic on a set `s`, so is its Fréchet derivative. See also
`AnalyticOnNhd.fderiv_of_isOpen`, removing the completeness assumption but requiring the set
to be open.  -/
AnalyticOnNhd.fderiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E} [CompleteSpace F], AnalyticOnNhd 𝕜 f s → AnalyticOnNhd 𝕜 (fderiv 𝕜 f) s
-- Mathlib.Algebra.Lie.Weights.Linear
LieModule.shiftedGenWeightSpace.shift_apply : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (χ : L → R) (x : ↥(LieModule.genWeightSpace M χ)),
  (LieModule.shiftedGenWeightSpace.shift R L M χ) x = x
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
IsUnit.integrable_smul_iff : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {𝕜 : Type u_8} [inst_1 : NormedRing 𝕜] [inst_2 : MulActionWithZero 𝕜 β] [IsBoundedSMul 𝕜 β] {c : 𝕜},
  IsUnit c → ∀ (f : α → β), MeasureTheory.Integrable (c • f) μ ↔ MeasureTheory.Integrable f μ
-- Mathlib.Algebra.Lie.IdealOperations
LieSubmodule.map_bracket_eq : ∀ {R : Type u} {L : Type v} {M : Type w} {M₂ : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup M₂]
  [inst_6 : Module R M₂] [inst_7 : LieRingModule L M₂] (N : LieSubmodule R L M) (f : M →ₗ⁅R,L⁆ M₂)
  [inst_8 : LieAlgebra R L] [LieModule R L M₂] (I : LieIdeal R L) [LieModule R L M],
  LieSubmodule.map f ⁅I, N⁆ = ⁅I, LieSubmodule.map f N⁆
-- Mathlib.Data.NNRat.Defs
NNRat.den_pos : ∀ (q : ℚ≥0), 0 < q.den
-- Mathlib.Algebra.Algebra.Operations
Submodule.mul_eq_map₂ : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] {M N : Submodule R A},
  M * N = Submodule.map₂ (LinearMap.mul R A) M N
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
DifferentiableWithinAt.cexp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra 𝕜 ℂ] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : E → ℂ} {x : E} {s : Set E},
  DifferentiableWithinAt 𝕜 f s x → DifferentiableWithinAt 𝕜 (fun x => Complex.exp (f x)) s x
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv_functor : ∀ {V : Type u'} [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {W : Type u''}
  [inst_2 : CategoryTheory.Category.{v'', u''} W] [inst_3 : CategoryTheory.MonoidalCategory W]
  (F : CategoryTheory.Functor V W) [inst_4 : F.LaxMonoidal] (D : Type u) [inst_5 : CategoryTheory.EnrichedCategory V D]
  (e :
    (v : V) →
      (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v))
  (h :
    ∀ (v : V) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v),
      (e v) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map f)),
  (CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv F D e h).functor =
    CategoryTheory.TransportEnrichment.forgetEnrichmentEquivFunctor F D e h
-- Mathlib.Analysis.LocallyConvex.AbsConvex
closedAbsConvexHull_closure_eq_closedAbsConvexHull : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜] [inst_4 : TopologicalSpace E] {s : Set E},
  (closedAbsConvexHull 𝕜) (closure s) = (closedAbsConvexHull 𝕜) s
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.substFunc_term : ∀ {L : FirstOrder.Language} {α : Type u'} (t : L.Term α),
  (t.substFunc fun {n} => FirstOrder.Language.Functions.term) = t
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.associator_hom_app : ∀ {B C D E : CategoryTheory.Cat} (F : B ⟶ C) (G : C ⟶ D) (H : D ⟶ E) (X : ↑B),
  (CategoryTheory.Bicategory.associator F G H).hom.toNatTrans.app X = CategoryTheory.eqToHom ⋯
-- Aesop.Tree.TreeM
Aesop.Tree.mk.sizeOf_spec : ∀ (root : Aesop.MVarClusterRef) (rootMetaState : Lean.Meta.SavedState) (numGoals numRapps : ℕ)
  (nextGoalId : Aesop.GoalId) (nextRappId : Aesop.RappId) (allIntroducedMVars : Std.HashSet Lean.MVarId),
  sizeOf
      { root := root, rootMetaState := rootMetaState, numGoals := numGoals, numRapps := numRapps,
        nextGoalId := nextGoalId, nextRappId := nextRappId, allIntroducedMVars := allIntroducedMVars } =
    1 + sizeOf root + sizeOf rootMetaState + sizeOf numGoals + sizeOf numRapps + sizeOf nextGoalId + sizeOf nextRappId +
      sizeOf allIntroducedMVars
-- Std.Sync.Broadcast
/-- A receiver for a `Broadcast` channel that can asynchronously receive messages.
Each receiver gets a copy of every message sent to the broadcast channel after
the receiver was created. Multiple receivers can exist for the same broadcast,
and each will receive all messages independently.

It's the sync version of `Broadcast.Receiver`.
 -/
Std.Broadcast.Sync.Receiver : Type → Type
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.keys_perm : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β},
  m₁.Equiv m₂ → m₁.keys.Perm m₂.keys
-- Mathlib.Data.Rat.Defs
Rat.den_ne_zero : ∀ (q : ℚ), q.den ≠ 0
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- If two points lie in the affine span of two points, those four points are collinear.  -/
collinear_insert_insert_of_mem_affineSpan_pair : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p₁ p₂ p₃ p₄ : P}, p₁ ∈ line[k, p₃, p₄] → p₂ ∈ line[k, p₃, p₄] → Collinear k {p₁, p₂, p₃, p₄}
-- Mathlib.Algebra.Ring.Subring.Basic
/-- Product of elements of a subring of a `CommRing` indexed by a `Finset` is in the
subring.  -/
Subring.prod_mem : ∀ {R : Type u_1} [inst : CommRing R] (s : Subring R) {ι : Type u_2} {t : Finset ι} {f : ι → R},
  (∀ c ∈ t, f c ∈ s) → ∏ i ∈ t, f i ∈ s
-- Mathlib.Data.Nat.Prime.Defs
Nat.minFac_two : Nat.minFac 2 = 2
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The L-series of the von Mangoldt function `Λ` equals the negative logarithmic derivative
of the L-series of the constant sequence `1` on its domain of convergence `re s > 1`.  -/
ArithmeticFunction.LSeries_vonMangoldt_eq : ∀ {s : ℂ}, 1 < s.re → LSeries (fun n => ↑(ArithmeticFunction.vonMangoldt n)) s = -deriv (LSeries 1) s / LSeries 1 s
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
Finset.uniformContinuous_sum : ∀ {α : Type u_3} {β : Type u_4} {ι : Type u_5} [inst : UniformSpace α] [inst_1 : AddCommGroup α] [IsUniformAddGroup α]
  [inst_3 : UniformSpace β] {f : ι → β → α} (s : Finset ι),
  (∀ i ∈ s, UniformContinuous (f i)) → UniformContinuous fun x => ∑ i ∈ s, f i x
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.natDegree_preΨ_le : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (n : ℤ),
  (W.preΨ n).natDegree ≤ (n.natAbs ^ 2 - if Even n then 4 else 1) / 2
-- Mathlib.Algebra.GroupWithZero.Shrink
instDistribMulActionShrink : {M : Type u_1} →
  {α : Type u_2} →
    [inst : Small.{v, u_2} α] →
      [inst_1 : Monoid M] → [inst_2 : AddCommMonoid α] → [DistribMulAction M α] → DistribMulAction M (Shrink.{v, u_2} α)
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObjCat.forget₂AddMon_map_hom : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y : CategoryTheory.RingObjCat C} (f : X ⟶ Y),
  ((CategoryTheory.RingObjCat.forget₂AddMon C).map f).hom = f.hom
-- Mathlib.Order.Filter.Basic
Filter.eventuallyEq_iff_exists_mem : ∀ {α : Type u} {β : Type v} {l : Filter α} {f g : α → β}, f =ᶠ[l] g ↔ ∃ s ∈ l, Set.EqOn f g s
-- Mathlib.LinearAlgebra.TensorProduct.Basis
TensorProduct.equivFinsuppOfBasisLeft_symm_apply : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : DecidableEq ι]
  (ℬ : Module.Basis ι R M) (b : ι →₀ N), (TensorProduct.equivFinsuppOfBasisLeft ℬ).symm b = b.sum fun i n => ℬ i ⊗ₜ[R] n
-- Mathlib.ModelTheory.ElementarySubstructures
/-- The natural embedding of an `L.Substructure` of `M` into `M`.  -/
FirstOrder.Language.ElementarySubstructure.subtype : {L : FirstOrder.Language} →
  {M : Type u_1} → [inst : L.Structure M] → (S : L.ElementarySubstructure M) → L.ElementaryEmbedding (↥S) M
-- Mathlib.Algebra.Opposites
MulOpposite.instIsLeftCancelAdd : ∀ {α : Type u_1} [inst : Add α] [IsLeftCancelAdd α], IsLeftCancelAdd αᵐᵒᵖ
-- Mathlib.GroupTheory.Focal
/-- **The Focal Subgroup Theorem**

For a Sylow p-subgroup P of a finite group G, `P ∩ G' = P*`,
where `P*` is the focal subgroup of `P`.
 -/
Subgroup.commutator_inf_eq_focalSubgroup : ∀ {G : Type u_1} [inst : Group G] {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G) [(↑P).FiniteIndex],
  commutator G ⊓ ↑P = (↑P).focalSubgroup
-- Mathlib.Order.Heyting.Basic
hnot_hnot_le : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a : α}, ￢￢a ≤ a
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.instUniqueOfSubsingleton.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : Subsingleton G],
  Subgroup.instUniqueOfSubsingleton = { default := ⊥, uniq := ⋯ }
-- Mathlib.Order.CountableSupClosed
countableInfClosure_empty : ∀ {α : Type u_2} [inst : Preorder α], countableInfClosure ∅ = ∅
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.mapRange.addMonoidHom_comp : ∀ {ι : Type u} {β : ι → Type v} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : (i : ι) → AddZeroClass (β i)]
  [inst_1 : (i : ι) → AddZeroClass (β₁ i)] [inst_2 : (i : ι) → AddZeroClass (β₂ i)] (f : (i : ι) → β₁ i →+ β₂ i)
  (f₂ : (i : ι) → β i →+ β₁ i),
  (DFinsupp.mapRange.addMonoidHom fun i => (f i).comp (f₂ i)) =
    (DFinsupp.mapRange.addMonoidHom f).comp (DFinsupp.mapRange.addMonoidHom f₂)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The kernel of `biprod.snd : X ⊞ Y ⟶ Y` is `X`.  -/
CategoryTheory.Limits.kernelBiprodSndIso : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] →
          CategoryTheory.Limits.kernel CategoryTheory.Limits.biprod.snd ≅ X
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.closure_singleton_one : ∀ {G : Type u_1} [inst : Group G], Subgroup.closure {1} = ⊥
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.ordered_prependMap : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {t : Std.DTreeMap.Internal.Impl α β} {ord_t : t.Ordered}
  {z : Std.DTreeMap.Internal.Zipper α β} {ord_z : z.Ordered},
  (∀ k ∈ z.toList, ∀ k' ∈ t.toListModel, compare k'.fst k.fst = Ordering.lt) →
    (Std.DTreeMap.Internal.Zipper.prependMap t z).Ordered
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.superpose.injEq : ∀ (p s c : Lean.Grind.AC.Seq) (c₁ c₂ : Lean.Meta.Grind.AC.EqCnstr) (p_1 s_1 c_1 : Lean.Grind.AC.Seq)
  (c₁_1 c₂_1 : Lean.Meta.Grind.AC.EqCnstr),
  (Lean.Meta.Grind.AC.EqCnstrProof.superpose p s c c₁ c₂ =
      Lean.Meta.Grind.AC.EqCnstrProof.superpose p_1 s_1 c_1 c₁_1 c₂_1) =
    (p = p_1 ∧ s = s_1 ∧ c = c_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1)
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.Ring.id : Lean.Meta.Sym.Arith.Ring → ℕ
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.instInfSet : {L : FirstOrder.Language} → {M : Type w} → [inst : L.Structure M] → InfSet (L.Substructure M)
-- Mathlib.Order.Bounds.Basic
le_of_isLUB_le_isGLB : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a b x y : α}, IsGLB s a → IsLUB s b → b ≤ a → x ∈ s → y ∈ s → x ≤ y
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionObj_mop : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (c : C) (d : D),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d { unmop := c } =
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d
-- Mathlib.Topology.Algebra.Module.Cardinality
Homeomorph.addLeft.congr_simp : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : SeparatelyContinuousAdd G] (a a_1 : G),
  a = a_1 → Homeomorph.addLeft a = Homeomorph.addLeft a_1
-- Mathlib.Order.Monotone.Basic
StrictMono.minimal_of_minimal_image : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β},
  StrictMono f → ∀ {a : α}, (∀ (p : β), f a ≤ p) → ∀ (x : α), a ≤ x
-- Mathlib.Order.Interval.Basic
NonemptyInterval.map_pure : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β) (a : α),
  NonemptyInterval.map f (NonemptyInterval.pure a) = NonemptyInterval.pure (f a)
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.toZModPow_ofIntSeq_of_pow_dvd_sub : ∀ (f : ℕ → ℤ) (p : ℕ) [inst : Fact (Nat.Prime p)] (hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i) (n : ℕ),
  (PadicInt.toZModPow n) (PadicInt.ofIntSeq f ⋯) = ↑(f n)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.mk_zero : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M}, AddLocalization.mk 0 0 = 0
-- Mathlib.Probability.Process.LocalProperty
ProbabilityTheory.Locally.of_prop : ∀ {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [inst : LinearOrder ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} {p : (ι → Ω → E) → Prop}
  [inst_1 : OrderBot ι] [inst_2 : TopologicalSpace ι] [inst_3 : OrderTopology ι] [inst_4 : Zero E],
  p X → ProbabilityTheory.Locally p 𝓕 X P
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
Mathlib.Tactic.Linarith.LinarithData.mk.inj : ∀ {maxVar : ℕ} {comps : Mathlib.Tactic.Linarith.PCompSet} {maxVar_1 : ℕ} {comps_1 : Mathlib.Tactic.Linarith.PCompSet},
  { maxVar := maxVar, comps := comps } = { maxVar := maxVar_1, comps := comps_1 } → maxVar = maxVar_1 ∧ comps = comps_1
-- Lean.Language.Basic
Lean.Language.SnapshotTask.mk.injEq : ∀ {α : Type} (stx? : Option Lean.Syntax) (reportingRange : Lean.Language.SnapshotTask.ReportingRange)
  (cancelTk? : Option IO.CancelToken) (task : Task α) (stx?_1 : Option Lean.Syntax)
  (reportingRange_1 : Lean.Language.SnapshotTask.ReportingRange) (cancelTk?_1 : Option IO.CancelToken)
  (task_1 : Task α),
  ({ stx? := stx?, reportingRange := reportingRange, cancelTk? := cancelTk?, task := task } =
      { stx? := stx?_1, reportingRange := reportingRange_1, cancelTk? := cancelTk?_1, task := task_1 }) =
    (stx? = stx?_1 ∧ reportingRange = reportingRange_1 ∧ cancelTk? = cancelTk?_1 ∧ task = task_1)
-- Mathlib.Analysis.InnerProductSpace.Symmetric
/-- **Alias** of the reverse direction of `Submodule.isSymmetricProjection_projection_iff`. -/
Submodule.isSymmetricProjection_projection_of_isOrtho : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U V : Submodule 𝕜 E} (hUV : IsCompl U V), U ⟂ V → (U.projection V hUV).IsSymmetricProjection
-- Std.Sync.Semaphore
/-- Returns the number of currently available permits.
 -/
Std.Semaphore.availablePermits : Std.Semaphore → BaseIO ℕ
-- Mathlib.Order.SuccPred.Basic
/-- The predecessor of an element. If `a` is not minimal, then `pred a` is the greatest
element less than `a`. If `a` is minimal, then `pred a = a`.  -/
Order.pred : {α : Type u_1} → [inst : Preorder α] → [PredOrder α] → α → α
-- Mathlib.Algebra.Algebra.Equiv
RingEquiv.symm_toIntAlgEquiv : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (f : R ≃+* S),
  f.toIntAlgEquiv.symm = f.symm.toIntAlgEquiv
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
RingHom.isIntegralElem.of_comp : ∀ {R : Type u_1} {S : Type u_4} {T : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  (f : R →+* S) (g : S →+* T) {x : T}, (g.comp f).IsIntegralElem x → g.IsIntegralElem x
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.skipPrefix?_string_empty : ∀ {s : String}, s.skipPrefix? "" = some s.startPos
-- Mathlib.Analysis.Analytic.Order
/-- The order is additive when multiplying analytic functions.  -/
analyticOrderNatAt_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {f g : 𝕜 → 𝕜} {z₀ : 𝕜},
  AnalyticAt 𝕜 f z₀ →
    AnalyticAt 𝕜 g z₀ →
      analyticOrderAt f z₀ ≠ ⊤ →
        analyticOrderAt g z₀ ≠ ⊤ → analyticOrderNatAt (f * g) z₀ = analyticOrderNatAt f z₀ + analyticOrderNatAt g z₀
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
/-- A class for the continuous functional calculus which requires the homomorphisms
`C(spectrum R a, R) → A` to be closed embeddings, as opposed to only continuous and injective.

The primary advantage of this is that one can conclude the range of this map is the closed
star subalgebra generated by `a`. However, unless the topology on `A` is induced by a C⋆-norm,
this is unlikely to occur.  -/
ClosedEmbeddingContinuousFunctionalCalculus : (R : Type u_1) →
  (A : Type u_2) →
    outParam (A → Prop) →
      [inst : CommSemiring R] →
        [inst_1 : StarRing R] →
          [inst_2 : MetricSpace R] →
            [IsTopologicalSemiring R] →
              [ContinuousStar R] → [inst_5 : Ring A] → [StarRing A] → [TopologicalSpace A] → [Algebra R A] → Prop
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ioo.instSemigroup : {R : Type u_1} → [inst : Semiring R] → [inst_1 : PartialOrder R] → [IsStrictOrderedRing R] → Semigroup ↑(Set.Ioo 0 1)
-- Mathlib.RingTheory.Congruence.Basic
/-- Definition of the infimum of two congruence relations.  -/
RingCon.inf_iff_and : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R] {c d : RingCon R} {x y : R}, (c ⊓ d) x y ↔ c x y ∧ d x y
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iInter₂_div_subset : ∀ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : Div α] (s : (i : ι) → κ i → Set α) (t : Set α),
  (⋂ i, ⋂ j, s i j) / t ⊆ ⋂ i, ⋂ j, s i j / t
-- Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
/-- For `𝒮ℒ` modular forms, `IsCuspForm` is equivalent to the q-expansion having vanishing
constant term.  -/
ModularForm.isCuspForm_iff_coeffZero_eq_zero : ∀ {k : ℤ} (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k),
  f.IsCuspForm ↔ (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 ⇑f) = 0
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.instEssentiallySmallLimitsClosureOfSmallOfLocallySmall : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {α : Type t}
  (J : α → Type u') [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)]
  [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [CategoryTheory.LocallySmall.{w, v, u} C]
  [Small.{w, t} α] [∀ (a : α), Small.{w, u'} (J a)] [∀ (a : α), CategoryTheory.LocallySmall.{w, v', u'} (J a)],
  CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} (P.limitsClosure J)
-- Mathlib.RingTheory.RingHom.Flat
RingHom.Flat.comp_iff_of_bijective_right : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  {f : R →+* S} {g : T →+* R}, Function.Bijective ⇑g → ((f.comp g).Flat ↔ f.Flat)