mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given Localization maps `f : M →* N, k : P →* Q` for Submonoids `S, T` respectively, if a
`CommMonoid` homomorphism `g : M →* P` induces a `f.map hy k : N →* Q`, then for all `z : N`,
`u : Q`, we have `f.map hy k z = u ↔ k (g x) = k (g y) * u` where `x : M, y ∈ S` are such that
`z * f y = f x`.  -/
Submonoid.LocalizationMap.map_spec : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} {T : Submonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T)
  {Q : Type u_4} [inst_3 : CommMonoid Q] {k : T.LocalizationMap Q} (z : N) (u : Q),
  (f.map hy k) z = u ↔ k (g (f.sec z).1) = k (g ↑(f.sec z).2) * u
-- Mathlib.Topology.Algebra.Support
HasCompactMulSupport.isCompact : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : One β] {f : α → β},
  HasCompactMulSupport f → IsCompact (mulTSupport f)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.d₀₁_comp_d₁₂ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{max u u_1, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupCohomology.d₀₁ A) (groupCohomology.d₁₂ A) = 0
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
AlgebraicIndependent.matroid_isBasis_iff_of_subsingleton : ∀ {R : Type u_1} {A : Type w} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : FaithfulSMul R A] [inst_4 : Subsingleton A] {s t : Set A},
  (AlgebraicIndependent.matroid R A).IsBasis s t ↔ s = t
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constEntryAtIdx?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {i : ℕ}, t₁.Equiv t₂ → Std.DTreeMap.Const.entryAtIdx? t₁ i = Std.DTreeMap.Const.entryAtIdx? t₂ i
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint.match_1.eq_1 : ∀ {n : ℕ}
  (motive : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Sort u_1)
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty)
  (h_3 :
    (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) →
      (b : Bool) → motive (Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit (l, b)))
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit),
  (match Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth with
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty => h_2 ()
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit (l, b) => h_3 l b
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit => h_4 ()) =
    h_1 ()
-- Mathlib.Order.RelClasses
instTrichotomousLt : ∀ {α : Type u} [inst : LinearOrder α], Std.Trichotomous fun x1 x2 => x1 < x2
-- Mathlib.Order.Ideal
/-- A union of a nonempty chain of ideals of sets is an ideal.  -/
Order.isIdeal_sUnion_of_isChain : ∀ {P : Type u_1} [inst : LE P] {C : Set (Set P)},
  (∀ I ∈ C, Order.IsIdeal I) → IsChain (fun x1 x2 => x1 ⊆ x2) C → C.Nonempty → Order.IsIdeal (⋃₀ C)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.RotateLeft
Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastRotateLeft : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (target : aig.ShiftTarget w)
  (assign : α → Bool) (idx : ℕ) (hidx : idx < w),
  ⟦assign,
      { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateLeft aig target).aig,
        ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateLeft aig target).vec.get idx hidx }⟧ =
    if hidx2 : idx < target.distance % w then
      ⟦assign, { aig := aig, ref := target.vec.get (w - target.distance % w + idx) ⋯ }⟧
    else ⟦assign, { aig := aig, ref := target.vec.get (idx - target.distance % w) ⋯ }⟧
-- Mathlib.Data.Finmap
/-- Replace a key with a given value in a finite map.
If the key is not present it does nothing.  -/
Finmap.replace : {α : Type u} → {β : α → Type v} → [DecidableEq α] → (a : α) → β a → Finmap β → Finmap β
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.rootSetFintype : {T : Type w} →
  [inst : CommRing T] →
    (p : Polynomial T) →
      (S : Type u_1) → [inst_1 : CommRing S] → [inst_2 : IsDomain S] → [inst_3 : Algebra T S] → Fintype ↑(p.rootSet S)
-- Aesop.Util.UnionFind
Aesop.UnionFind.add : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → α → Aesop.UnionFind α → Aesop.UnionFind α
-- Std.Do.WP.SimpLemmas
Std.Do.WP.withReader_ReaderT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ρ α : Type u} {f : ρ → ρ} {x : ReaderT ρ m α}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.arg ρ ps)} [inst : Std.Do.WP m ps],
  (Std.Do.wp (MonadWithReaderOf.withReader f x)).apply Q = fun r => (Std.Do.wp x).apply (fun a x => Q.1 a r, Q.2) (f r)
-- Mathlib.Combinatorics.SimpleGraph.LapMatrix
SimpleGraph.mem_ker_toLin'_lapMatrix_of_connectedComponent : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] {G : SimpleGraph V} [inst_2 : DecidableRel G.Adj]
  [inst_3 : DecidableEq G.ConnectedComponent] (c : G.ConnectedComponent),
  (fun i => if G.connectedComponentMk i = c then 1 else 0) ∈ (Matrix.toLin' (SimpleGraph.lapMatrix ℝ G)).ker
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.isCompactElement_lieSpan_singleton : ∀ (R : Type u) (L : Type v) {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (m : M), IsCompactElement (LieSubmodule.lieSpan R L {m})
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.reverse_eq_single : ∀ {n : ℕ} {hn : 0 < n} {c : Composition n}, c.reverse = Composition.single n hn ↔ c = Composition.single n hn
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.HasSubst.X : ∀ {σ : Type u_1} {S : Type u_5} [inst : CommRing S], MvPowerSeries.HasSubst fun s => MvPowerSeries.X s
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.IsTriangulatedClosed₂.mk' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderIsomorphisms],
  (∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, P T.obj₁ → P T.obj₃ → P T.obj₂) →
    P.IsTriangulatedClosed₂
-- Mathlib.Order.OrderDual
/-- `ofDual` is the identity function from the `OrderDual` of a linear order.  -/
OrderDual.ofDual : {α : Type u_1} → αᵒᵈ ≃ α
-- Mathlib.Algebra.MonoidAlgebra.Opposite
MonoidAlgebra.opRingEquiv.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : Mul M],
  MonoidAlgebra.opRingEquiv =
    {
      toEquiv :=
        (MulOpposite.opAddEquiv.symm.trans
            ((MonoidAlgebra.mapDomainAddEquiv R MulOpposite.opEquiv).trans
              (MonoidAlgebra.mapAddEquiv Mᵐᵒᵖ MulOpposite.opAddEquiv))).toEquiv,
      map_mul' := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.homLinearEquiv_apply : ∀ {R : Type u} [inst : Semiring R] {M N : SemimoduleCat R} {S : Type u_1} [inst_1 : Semiring S] [inst_2 : Module S ↑N]
  [inst_3 : SMulCommClass R S ↑N] (a : M ⟶ N), SemimoduleCat.homLinearEquiv a = SemimoduleCat.homAddEquiv.toFun a
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.toStream.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α → RBTree.RBNode.Stream α → Sort u_2) →
    (x : RBTree.RBNode α) →
      (x_1 : RBTree.RBNode.Stream α) →
        ((acc : RBTree.RBNode.Stream α) → motive RBTree.RBNode.nil acc) →
          ((c : RBTree.RBColor) →
              (l : RBTree.RBNode α) →
                (v : α) →
                  (r : RBTree.RBNode α) → (acc : RBTree.RBNode.Stream α) → motive (RBTree.RBNode.node c l v r) acc) →
            motive x x_1
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
/-- The square of the quadratic character on nonzero arguments is `1`.  -/
quadraticChar_sq_one : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F] {a : F},
  a ≠ 0 → (quadraticChar F) a ^ 2 = 1
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
CategoryTheory.Limits.WeightedCone.w : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {W : CategoryTheory.Functor J (Type w)} {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.WeightedCone W F)
  {i j : J} (x : W.obj i) (f : i ⟶ j),
  CategoryTheory.CategoryStruct.comp (c.π x) (F.map f) = c.π ((CategoryTheory.ConcreteCategory.hom (W.map f)) x)
-- Init.Data.Ord.Basic
Ordering.then_assoc : ∀ (o₁ o₂ o₃ : Ordering), (o₁.then o₂).then o₃ = o₁.then (o₂.then o₃)
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.lift_comp_comm_eq : ∀ (R : Type u_1) {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} (M : Type u_7)
  (N : Type u_8) {P₂ : Type u_17} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : AddCommMonoid P₂]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R₂ P₂] (f : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂),
  TensorProduct.lift f ∘ₛₗ ↑(TensorProduct.comm R N M) = TensorProduct.lift f.flip
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.le_infEDist`. -/
EMetric.le_infEdist : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s : Set α} {d : ENNReal},
  d ≤ Metric.infEDist x s ↔ ∀ y ∈ s, d ≤ edist x y
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.pre_obj_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {B : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C)
  (G : CategoryTheory.Functor C D) (S : D) (X : CategoryTheory.Comma (F.comp G) (CategoryTheory.Functor.fromPUnit S)),
  ((CategoryTheory.CostructuredArrow.pre F G S).obj X).left = F.obj X.left
-- Mathlib.Order.Interval.Set.InitialSeg
/-- If `i ≤ j`, then `Iio i` is a principal segment of `Iic j`.  -/
Set.principalSegIioIicOfLE : {α : Type u_1} → [inst : Preorder α] → {i j : α} → i ≤ j → ↑(Set.Iio i) <i ↑(Set.Iic j)
-- Std.Do.WP.Monad
Std.Do.ReaderT.instWPMonad : {m : Type u → Type v} →
  {ps : Std.Do.PostShape} →
    {ρ : Type u} → [inst : Monad m] → [Std.Do.WPMonad m ps] → Std.Do.WPMonad (ReaderT ρ m) (Std.Do.PostShape.arg ρ ps)
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.HandlerTrie.brecOn_3.eq : ∀ {motive_1 : Lean.Elab.ConfigEval.HandlerTrie✝ → Sort u}
  {motive_2 : Array (String × Lean.Elab.ConfigEval.HandlerTrie✝) → Sort u}
  {motive_3 : List (String × Lean.Elab.ConfigEval.HandlerTrie✝) → Sort u}
  {motive_4 : String × Lean.Elab.ConfigEval.HandlerTrie✝ → Sort u} (t : String × Lean.Elab.ConfigEval.HandlerTrie✝)
  (F_1 : (t : Lean.Elab.ConfigEval.HandlerTrie✝) → Lean.Elab.ConfigEval.HandlerTrie.below✝ t → motive_1 t)
  (F_2 :
    (t : Array (String × Lean.Elab.ConfigEval.HandlerTrie✝)) → Lean.Elab.ConfigEval.HandlerTrie.below_1✝ t → motive_2 t)
  (F_3 :
    (t : List (String × Lean.Elab.ConfigEval.HandlerTrie✝)) → Lean.Elab.ConfigEval.HandlerTrie.below_2✝ t → motive_3 t)
  (F_4 : (t : String × Lean.Elab.ConfigEval.HandlerTrie✝) → Lean.Elab.ConfigEval.HandlerTrie.below_3✝ t → motive_4 t),
  Lean.Elab.ConfigEval.HandlerTrie.brecOn_3✝ t F_1 F_2 F_3 F_4 =
    F_4 t (Lean.Elab.ConfigEval.HandlerTrie.brecOn_3.go✝ t F_1 F_2 F_3 F_4).2
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Path.Homotopy.transReflReparamAux_mem_I : ∀ (t : ↑unitInterval), Path.Homotopy.transReflReparamAux t ∈ unitInterval
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.continuous : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞} (f : TestFunction Ω F n), Continuous ⇑f
-- Mathlib.Logic.Equiv.Defs
/-- A family of equivalences `Π a, β₁ a ≃ β₂ a` generates an equivalence between `Σ a, β₁ a` and
`Σ a, β₂ a`.  -/
Equiv.sigmaCongrRight : {α : Type u_3} → {β₁ : α → Type u_1} → {β₂ : α → Type u_2} → ((a : α) → β₁ a ≃ β₂ a) → (a : α) × β₁ a ≃ (a : α) × β₂ a
-- Mathlib.Analysis.Normed.Module.Basic
instNormedCommRingRestrictScalars : {𝕜 : Type u_1} → {𝕜' : Type u_2} → {E : Type u_3} → [I : NormedCommRing E] → NormedCommRing (RestrictScalars 𝕜 𝕜' E)
-- Init.PropLemmas
Decidable.imp_iff_or_not : ∀ {b a : Prop} [Decidable b], b → a ↔ a ∨ ¬b
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- The refinement morphisms between objects in the coverings of `S`.  -/
CategoryTheory.PreZeroHypercover.Hom.h₀ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E : CategoryTheory.PreZeroHypercover S} →
        {F : CategoryTheory.PreZeroHypercover S} → (self : E.Hom F) → (i : E.I₀) → E.X i ⟶ F.X (self.s₀ i)
-- Mathlib.Order.RelIso.Basic
RelIso.coe_fn_mk : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : α ≃ β)
  (o : ∀ ⦃a b : α⦄, s (f a) (f b) ↔ r a b), ⇑{ toEquiv := f, map_rel_iff' := o } = ⇑f
-- Mathlib.RingTheory.RootsOfUnity.Basic
instFiniteMonoidHomUnits : ∀ {R : Type u_4} [inst : CommRing R] [IsDomain R] {L : Type u_7} [inst_2 : LeftCancelMonoid L] [Finite L],
  Finite (L →* Rˣ)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Cofan.mk_pt : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : β → C} (P : C) (p : (b : β) → f b ⟶ P),
  (CategoryTheory.Limits.Cofan.mk P p).pt = P
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- Transport the structure of a monoidal functor along a natural isomorphism of functors.
 -/
CategoryTheory.Functor.Monoidal.transport : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F G : CategoryTheory.Functor C D} → [F.Monoidal] → (F ≅ G) → G.Monoidal
-- Mathlib.Data.Set.Basic
/-- **Alias** of the reverse direction of `Set.ofPred_subset_ofPred`. -/
Set.ofPred_subset_ofPred_of_imp : ∀ {α : Type u} {p q : α → Prop}, (∀ (a : α), p a → q a) → {a | p a} ⊆ {a | q a}
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.p_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.PrepathObject A)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct A A],
  CategoryTheory.CategoryStruct.comp P.p CategoryTheory.Limits.prod.snd = P.p₁
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.coe_sInf : ∀ {G : Type u_1} [inst : Group G] (H : Set (Subgroup G)), ↑(sInf H) = ⋂ s ∈ H, ↑s
-- Mathlib.NumberTheory.Multiplicity
emultiplicity_pow_prime_pow_sub_pow_prime_pow : ∀ {R : Type u_1} [inst : CommRing R] {x y : R} {p : ℕ} [IsDomain R],
  Prime ↑p →
    Odd p →
      ↑p ∣ x - y → ¬↑p ∣ x → ∀ (a : ℕ), emultiplicity (↑p) (x ^ p ^ a - y ^ p ^ a) = emultiplicity (↑p) (x - y) + ↑a
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coeIdeal_top : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P],
  ↑⊤ = 1
-- Mathlib.Algebra.Ring.Subring.Defs
SubringClass.coe_natCast : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : SetLike S R] [hSR : SubringClass S R] (s : S) (n : ℕ),
  ↑↑n = ↑n
-- Std.Data.DHashMap.Internal.AssocList.Iterator
_private.Std.Data.DHashMap.Internal.AssocList.Iterator.0.Std.DHashMap.Internal.AssocList.instIteratorAssocListIteratorIdSigma.match_1.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Std.IterStep (Std.IterM Id ((a : α) × β a)) ((a : α) × β a) → Sort u_3)
  (it' : Std.IterM Id ((a : α) × β a)) (out : (a : α) × β a)
  (h_1 : (it' : Std.IterM Id ((a : α) × β a)) → (out : (a : α) × β a) → motive (Std.IterStep.yield it' out))
  (h_2 : (it : Std.IterM Id ((a : α) × β a)) → motive (Std.IterStep.skip it)) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it => h_2 it
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Mathlib.Order.Filter.Basic
Filter.eventually_iSup : ∀ {α : Type u} {ι : Sort x} {p : α → Prop} {fs : ι → Filter α},
  (∀ᶠ (x : α) in ⨆ b, fs b, p x) ↔ ∀ (b : ι), ∀ᶠ (x : α) in fs b, p x
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_mul_const_uIcc : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (a b c : α),
  (fun x => x * a) '' Set.uIcc b c = Set.uIcc (b * a) (c * a)
-- Init.Data.List.Lemmas
List.map_inj_left : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f g : α → β}, List.map f l = List.map g l ↔ ∀ a ∈ l, f a = g a
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.mkBin : Lean.Name →
  Lean.Expr →
    Lean.Expr → ℚ × Lean.Expr → ℚ × Lean.Expr → (ℚ → ℚ → ℚ) → Lean.Meta.Grind.Arith.FieldNormNum.M✝ (ℚ × Lean.Expr)
-- Mathlib.Topology.Algebra.Support
/-- A function `f` *has compact support* or is *compactly supported* if the closure of
the support of `f` is compact. In a T₂ space this is equivalent to `f` being equal to `0` outside a
compact set.  -/
HasCompactSupport : {α : Type u_2} → {β : Type u_4} → [TopologicalSpace α] → [Zero β] → (α → β) → Prop
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.LogConfig.mk.sizeOf_spec : ∀ (logDir? : Option System.FilePath) (allowedMethods? disallowedMethods? : Option (Std.HashSet String)),
  sizeOf { logDir? := logDir?, allowedMethods? := allowedMethods?, disallowedMethods? := disallowedMethods? } =
    1 + sizeOf logDir? + sizeOf allowedMethods? + sizeOf disallowedMethods?
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Hom.image_neighborSet_subset : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (v : V) (f : G →g G'),
  ⇑f '' G.neighborSet v ⊆ G'.neighborSet (f v)
-- Mathlib.Analysis.Convex.Birkhoff
/-- If M is a positive scalar multiple of a doubly stochastic matrix, then there is a permutation matrix
whose support is contained in the support of M.
 -/
_private.Mathlib.Analysis.Convex.Birkhoff.0.exists_perm_eq_zero_implies_eq_zero : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semifield R]
  [inst_3 : LinearOrder R] [inst_4 : IsStrictOrderedRing R] {M : Matrix n n R} {s : R},
  0 < s → (∃ M' ∈ doublyStochastic R n, M = s • M') → ∃ σ, ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0
-- Aesop.Search.Expansion
Aesop.SafeRulesResult.failed.inj : ∀ {postponed postponed_1 : Array Aesop.PostponedSafeRule},
  Aesop.SafeRulesResult.failed postponed = Aesop.SafeRulesResult.failed postponed_1 → postponed = postponed_1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_modify : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k k' : α} {f : β k → β k}, m.WF → (m.modify k f).contains k' = m.contains k'
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.localTrivAsPartialEquiv_source : ∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F) (i : ι), (Z.localTrivAsPartialEquiv i).source = (Z.localTriv i).source
-- Mathlib.Data.Finset.Lattice.Fold
/-- A version of `Finset.inf'_image` with LHS and RHS reversed.
Also, this lemma assumes that `s` is nonempty instead of assuming that its image is nonempty.  -/
Finset.inf'_comp_eq_image : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeInf α] [inst_1 : DecidableEq β] {s : Finset γ}
  {f : γ → β} (hs : s.Nonempty) (g : β → α), s.inf' hs (g ∘ f) = (Finset.image f s).inf' ⋯ g
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the smallest key that is greater than the given key,
panicking if no such key exists.
 -/
Std.TreeMap.Raw.getKeyGT! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeMap.Raw α β cmp → α → α
-- Mathlib.Data.Nat.ModEq
Dvd.dvd.modEq_zero_nat : ∀ {n a : ℕ}, n ∣ a → a ≡ 0 [MOD n]
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.coe_bot : ∀ {α : Type u_1}, ⊥ = 0
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.compl_iSup : ∀ {α : Type u_1} {ι : Sort u_4} [inst : LE α] (f : ι → LowerSet α), (⨆ i, f i).compl = ⨆ i, (f i).compl
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.instIsSubApplySet : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommGroup M] [inst_1 : TopologicalSpace M]
  [inst_2 : IsTopologicalAddGroup M], IsSubApply (MeasureTheory.VectorMeasure α M) (Set α) M
-- Mathlib.Data.List.Basic
List.getLast?_flatten_replicate : ∀ {α : Type u} {n : ℕ}, n ≠ 0 → ∀ (l : List α), (List.replicate n l).flatten.getLast? = l.getLast?
-- Mathlib.Algebra.Lie.Semisimple.Basic
LieAlgebra.HasTrivialRadical.eq_bot_of_isSolvable : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [LieAlgebra.HasTrivialRadical R L] (I : LieIdeal R L) [hI : LieAlgebra.IsSolvable ↥I], I = ⊥
-- Mathlib.Data.ENNReal.Inv
ENNReal.le_inv_iff_le_inv : ∀ {a b : ENNReal}, a ≤ b⁻¹ ↔ b ≤ a⁻¹
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The category of multiforks is equivalent to the category of forks over `∏ᶜ I.left ⇉ ∏ᶜ I.right`.
It then follows from `CategoryTheory.IsLimit.ofPreservesConeTerminal` (or `reflects`) that it
preserves and reflects limit cones.
 -/
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MulticospanShape} →
      (I : CategoryTheory.Limits.MulticospanIndex J C) →
        [inst_1 : CategoryTheory.Limits.HasProduct I.left] →
          [inst_2 : CategoryTheory.Limits.HasProduct I.right] →
            CategoryTheory.Limits.Multifork I ≌ CategoryTheory.Limits.Fork I.fstPiMap I.sndPiMap
-- Init.Prelude
/-- A helper theorem to deduce `False` from `a = b` when `f a ≠ f b` for some function `f : α → Nat`
(typically `.ctorIdx`). Used as a simpler alternative to the no-confusion theorems.
 -/
noConfusion_of_Nat : ∀ {α : Sort u} (f : α → ℕ) {a b : α}, a = b → Bool.rec False True ((f a).beq (f b))
-- Lean.Elab.Do.Basic
Lean.Elab.Do.instInhabitedDoOps.default : Lean.Elab.Do.DoOps
-- Mathlib.Logic.Equiv.List
Encodable.decode_list_zero : ∀ {α : Type u_1} [inst : Encodable α], Encodable.decode 0 = some []
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
CategoryTheory.Monoidal.whiskerRight : ∀ {A B : CategoryTheory.Cat} (f : A ⟶ B) (X : CategoryTheory.Cat),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight f X = (f.toFunctor.prod (CategoryTheory.Functor.id ↑X)).toCatHom
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.stabilizer_inf_stabilizer_le_stabilizer_sdiff : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] {s t : Set α},
  MulAction.stabilizer G s ⊓ MulAction.stabilizer G t ≤ MulAction.stabilizer G (s \ t)
-- Mathlib.Tactic.ClickSuggestions.ApplyAt
/-- The total length of the new goals when printed.  -/
Mathlib.Tactic.ClickSuggestions.ApplyAtKey.replacementSize : Mathlib.Tactic.ClickSuggestions.ApplyAtKey → ℕ