mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Util.ForEachExprWhere
/-- Set of visited subterms that satisfy the predicate `p`.
We have to use this set to make sure `f` is applied at most once of each subterm that satisfies `p`.
 -/
Lean.ForEachExprWhere.State.checked : Lean.ForEachExprWhere.State → Std.HashSet Lean.Expr
-- Mathlib.Order.Monotone.Basic
strictAntiOn_comp_ofDual_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictAntiOn (f ∘ ⇑OrderDual.ofDual) s ↔ StrictMonoOn f s
-- Mathlib.Algebra.Polynomial.Basic
/-- Prefer putting constants to the left of `X ^ n`.

This lemma is the loop-avoiding `simp` version of `X_pow_mul`.  -/
Polynomial.X_pow_mul_C : ∀ {R : Type u} [inst : Semiring R] (r : R) (n : ℕ),
  Polynomial.X ^ n * Polynomial.C r = Polynomial.C r * Polynomial.X ^ n
-- Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
/-- The convex combination of points in an affine space, given a probability distribution.  -/
AddTorsor.convexCombination : {R : Type u_1} →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : Ring R] →
        [inst_1 : PartialOrder R] →
          [inst_2 : AddCommGroup V] → [Module R V] → [AddTorsor V P] → Convexity.StdSimplex R P → P
-- Mathlib.Probability.Distributions.Fernique
/-- If a measure `μ` is such that `μ.prod μ` is invariant by rotation of angle `-π/4` then
`μ {x | ‖x‖ ≤ a} * μ {x | b < ‖x‖} ≤ μ {x | (b - a) / √2 < ‖x‖} ^ 2`.  -/
ProbabilityTheory.measure_le_mul_measure_gt_le_of_map_rotation_eq_self : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [SecondCountableTopology E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.SFinite μ],
  MeasureTheory.Measure.map (⇑(ContinuousLinearMap.rotation (-(Real.pi / 4)))) (μ.prod μ) = μ.prod μ →
    ∀ (a b : ℝ), μ {x | ‖x‖ ≤ a} * μ {x | b < ‖x‖} ≤ μ {x | (b - a) / √2 < ‖x‖} ^ 2
-- Mathlib.Order.SuccPred.Basic
Order.pred.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α], Order.pred = PredOrder.pred
-- Mathlib.Analysis.Calculus.ImplicitFunction.Bivariate
eventually_apply_implicitFunctionOfBivariate : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : IsRCLikeNormedField 𝕜] {E₁ : Type u_2}
  [inst_2 : NormedAddCommGroup E₁] [inst_3 : NormedSpace 𝕜 E₁] [inst_4 : CompleteSpace E₁] {E₂ : Type u_3}
  [inst_5 : NormedAddCommGroup E₂] [inst_6 : NormedSpace 𝕜 E₂] [inst_7 : CompleteSpace E₂] {F : Type u_4}
  [inst_8 : NormedAddCommGroup F] [inst_9 : NormedSpace 𝕜 F] [inst_10 : CompleteSpace F] {u : E₁ × E₂} {f : E₁ → E₂ → F}
  {f₁ : E₁ → E₂ → E₁ →L[𝕜] F} {f₂ : E₁ → E₂ → E₂ →L[𝕜] F}
  (df₁ : ∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun x => f x v.2) (f₁ v.1 v.2) v.1)
  (df₂ : ∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun x => f v.1 x) (f₂ v.1 v.2) v.2) (cf₁ : ContinuousAt (↿f₁) u)
  (cf₂ : ContinuousAt (↿f₂) u) (if₂u : (f₂ u.1 u.2).IsInvertible),
  ∀ᶠ (x : E₁) in nhds u.1, f x (implicitFunctionOfBivariate df₁ df₂ cf₁ cf₂ if₂u x) = f u.1 u.2
-- Init.Grind.AC
Lean.Grind.AC.Seq.sort' : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq
-- Mathlib.NumberTheory.LucasLehmer
strictMono_mersenne : StrictMono mersenne
-- Mathlib.Analysis.InnerProductSpace.GramMatrix
Matrix.gram_eq_one_iff_orthonormal : ∀ {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : DecidableEq n] {v : n → E}, Matrix.gram 𝕜 v = 1 ↔ Orthonormal 𝕜 v
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.ReflectsEpimorphisms.of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} [F.ReflectsEpimorphisms] (α : F ≅ G), G.ReflectsEpimorphisms
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C}
  (S : J.Cover X) (f : S.Arrow), S.preOneHypercover.f f = f.f
-- Mathlib.Algebra.Notation.Prod
Prod.pow_swap : ∀ {E : Type u_8} {α : Type u_9} {β : Type u_10} [inst : Pow α E] [inst_1 : Pow β E] (p : α × β) (c : E),
  (p ^ c).swap = p.swap ^ c
-- Lean.DocString.Markdown
_private.Lean.DocString.Markdown.0.Lean.Doc.inlineRendererForUnsafe : Lean.Name → Lean.CoreM (Option Lean.Doc.InlineMdRenderer)
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f_aux : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} {adj : F ⊣ G}
  [inst_2 : ∀ (A : adj.toMonad.Algebra), CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))]
  (A : adj.toMonad.Algebra),
  ((CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction adj).unit.app A).f =
    (adj.homEquiv A.A (CategoryTheory.Limits.coequalizer (F.map A.a) (adj.counit.app (F.obj A.A))))
      (CategoryTheory.Limits.coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.uliftFunctor.eq_1 : AddCommMonCat.uliftFunctor =
  { obj := fun X => AddCommMonCat.of (ULift.{u, v} ↑X),
    map := fun {x x_1} f =>
      AddCommMonCat.ofHom
        (AddEquiv.ulift.symm.toAddMonoidHom.comp ((AddCommMonCat.Hom.hom f).comp AddEquiv.ulift.toAddMonoidHom)),
    map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.map : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C},
  S.Exact →
    ∀ (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S]
      [F.PreservesRightHomologyOf S], (S.map F).Exact
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.instAwayObjOppositeOpensCarrierTopObjFunctorTypeIsSheafGrothendieckTopologyStructureSheafInTypeOpBasicOpenToOpenₗ : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : R),
  IsLocalizedModule.Away f (AlgebraicGeometry.StructureSheaf.toOpenₗ R M (PrimeSpectrum.basicOpen f))
-- Init.Data.Int.Linear
Int.Internal.Linear.cdiv_add_cmod : ∀ (a b : ℤ), b * Int.Internal.Linear.cdiv a b + Int.Internal.Linear.cmod a b = a
-- Mathlib.Analysis.SpecialFunctions.Sqrt
HasStrictFDerivAt.sqrt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {f' : StrongDual ℝ E},
  HasStrictFDerivAt f f' x → f x ≠ 0 → HasStrictFDerivAt (fun y => √(f y)) ((1 / (2 * √(f x))) • f') x
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.takeUntil_eq_take : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V] (p : G.Walk u v) (h : w ∈ p.support),
  p.takeUntil w h = (p.take (List.idxOf w p.support)).copy ⋯ ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- If `F` is an equivalence, then applying `F` to a diagram indexing a (co)kernel of `f` yields
the diagram indexing the (co)kernel of `F.map f`.  -/
CategoryTheory.Limits.compNatIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          {D : Type u'} →
            [inst_2 : CategoryTheory.Category.{v, u'} D] →
              [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
                (F : CategoryTheory.Functor C D) →
                  [F.IsEquivalence] →
                    (CategoryTheory.Limits.parallelPair f 0).comp F ≅ CategoryTheory.Limits.parallelPair (F.map f) 0
-- Mathlib.Order.Partition.Finpartition
Finpartition.biUnion_filter_atomise : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {F : Finset (Finset α)},
  t ∈ F → t ⊆ s → {u ∈ (Finpartition.atomise s F).parts | u ⊆ t ∧ u.Nonempty}.biUnion id = t
-- Mathlib.Combinatorics.Enumerative.Composition
List.flatten_splitWrtCompositionAux : ∀ {α : Type u_1} {ns : List ℕ} {l : List α}, ns.sum = l.length → (l.splitWrtCompositionAux ns).flatten = l
-- Mathlib.CategoryTheory.Idempotents.Basic
/-- A category is idempotent complete iff all idempotent endomorphisms `p`
split as a composition `p = e ≫ i` with `i ≫ e = 𝟙 _`  -/
CategoryTheory.IsIdempotentComplete : (C : Type u_1) → [CategoryTheory.Category.{v_1, u_1} C] → Prop
-- Mathlib.NumberTheory.Height.Basic
/-- Consider a finite family `x : (a : α) → ι a → K` of tuples. Then the logarithmic height
of the "multiplication table" `fun (I : (a : α) → ι a ↦ ∏ a, x a (I a))` is the sum
of the logarithmic heights of all the `x a`.  -/
Height.logHeight_fun_prod_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {α : Type u} [inst_2 : Fintype α]
  {ι : α → Type v} [∀ (a : α), Finite (ι a)] {x : (a : α) → ι a → K},
  (∀ (a : α), x a ≠ 0) → (Height.logHeight fun I => ∏ a, x a (I a)) = ∑ a, Height.logHeight (x a)
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b : EInt) (hab : a ≤ b),
  (t.eTruncGEIsoGEGE a b hab).hom = t.eTruncGEToGEGE a b
-- Mathlib.FieldTheory.Galois.Profinite
AlgEquiv.liftNormal.congr_simp : ∀ {F : Type u_1} [inst : Field F] {K₁ : Type u_3} {K₂ : Type u_4} [inst_1 : Field K₁] [inst_2 : Field K₂]
  [inst_3 : Algebra F K₁] [inst_4 : Algebra F K₂] (χ χ_1 : K₁ ≃ₐ[F] K₂),
  χ = χ_1 →
    ∀ (E : Type u_6) [inst_5 : Field E] [inst_6 : Algebra F E] [inst_7 : Algebra K₁ E] [inst_8 : Algebra K₂ E]
      [inst_9 : IsScalarTower F K₁ E] [inst_10 : IsScalarTower F K₂ E] [inst_11 : Normal F E],
      χ.liftNormal E = χ_1.liftNormal E
-- Mathlib.RingTheory.Finiteness.Basic
RingHom.Finite.id : ∀ (A : Type u_1) [inst : CommRing A], (RingHom.id A).Finite
-- Mathlib.RingTheory.ClassGroup.Basic
ClassGroup.mk0_integralRep : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDedekindDomain R]
  (I : (FractionalIdeal (nonZeroDivisors R) (FractionRing R))ˣ),
  ClassGroup.mk0 ⟨ClassGroup.integralRep ↑I, ⋯⟩ = (ClassGroup.mk (FractionRing R)) I
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.map₂_associator : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.Pseudofunctor B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
  self.map₂ (CategoryTheory.Bicategory.associator f g h).hom =
    CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapComp f g).hom (self.map h))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.associator (self.map f) (self.map g) (self.map h)).hom
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapComp g h).inv)
            (self.mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv)))
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.contains_diff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (t₁ \ t₂).contains k = (t₁.contains k && !t₂.contains k)
-- Mathlib.Data.Semiquot
/-- Replace `s` in a `Semiquot` with a superset.  -/
Semiquot.blur' : {α : Type u_1} → (q : Semiquot α) → {s : Set α} → q.s ⊆ s → Semiquot α
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Path.Homotopy.transAssocReparamAux_zero : Path.Homotopy.transAssocReparamAux 0 = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.isZero_kernel_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [CategoryTheory.Mono f] [inst_3 : CategoryTheory.Limits.HasKernel f],
  CategoryTheory.Limits.IsZero (CategoryTheory.Limits.kernel f)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Power : Type
-- Lean.Elab.Syntax
/-- Expand `optional «precedence»` where
«precedence» := leading_parser " : " >> precedenceParser  -/
Lean.Elab.Term.expandOptPrecedence : Lean.Syntax → Lean.MacroM (Option ℕ)
-- Mathlib.RingTheory.Finiteness.Finsupp
LinearMap.finsuppLinearMap_apply_apply_apply : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} (S : Type u_5) [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N]
  [inst_5 : Semiring S] [inst_6 : Module S N] [inst_7 : SMulCommClass R S N] (m : ι →₀ M →ₗ[R] N) (m_1 : M) (a : ι),
  (((LinearMap.finsuppLinearMap S) m) m_1) a = (m a) m_1
-- Mathlib.Data.Set.NAry
Set.image2_swap : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} (f : α → β → γ) (s : Set α) (t : Set β),
  Set.image2 f s t = Set.image2 (fun a b => f b a) t s
-- Mathlib.CategoryTheory.Abelian.Transfer
CategoryTheory.ShrinkHoms.abelian : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v_1, u_1} C] →
      [CategoryTheory.Abelian C] → CategoryTheory.Abelian (CategoryTheory.ShrinkHoms.{u_1} C)
-- Mathlib.RingTheory.ClassGroup.ExtendedHom
ClassGroup.extendedHom_eq_one_of_forall_isPrincipal : ∀ (A : Type u_1) (B : Type u_2) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : Module.IsTorsionFree A B] [inst_4 : IsDedekindDomain A] [inst_5 : IsDedekindDomain B],
  (∀ (I : Ideal A), Submodule.IsPrincipal (Ideal.map (algebraMap A B) I)) → ClassGroup.extendedHom A B = 1
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.mk'.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.HasShift C ℤ} {obj₁ obj₂ obj₃ : C}
  {mor₁ : obj₁ ⟶ obj₂} {mor₂ : obj₂ ⟶ obj₃} {mor₃ : obj₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj obj₁}
  {obj₁_1 obj₂_1 obj₃_1 : C} {mor₁_1 : obj₁_1 ⟶ obj₂_1} {mor₂_1 : obj₂_1 ⟶ obj₃_1}
  {mor₃_1 : obj₃_1 ⟶ (CategoryTheory.shiftFunctor C 1).obj obj₁_1},
  { obj₁ := obj₁, obj₂ := obj₂, obj₃ := obj₃, mor₁ := mor₁, mor₂ := mor₂, mor₃ := mor₃ } =
      { obj₁ := obj₁_1, obj₂ := obj₂_1, obj₃ := obj₃_1, mor₁ := mor₁_1, mor₂ := mor₂_1, mor₃ := mor₃_1 } →
    obj₁ = obj₁_1 ∧ obj₂ = obj₂_1 ∧ obj₃ = obj₃_1 ∧ mor₁ ≍ mor₁_1 ∧ mor₂ ≍ mor₂_1 ∧ mor₃ ≍ mor₃_1
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.trStmts₁_run : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {k : K} {s : Turing.TM2to1.StAct K Γ σ k}
  {q : Turing.TM2.Stmt Γ Λ σ},
  Turing.TM2to1.trStmts₁ (Turing.TM2to1.stRun s q) =
    {Turing.TM2to1.Λ'.go k s q, Turing.TM2to1.Λ'.ret q} ∪ Turing.TM2to1.trStmts₁ q
-- Mathlib.GroupTheory.Sylow
Sylow.card_dvd_index : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G),
  Nat.card (Sylow p G) ∣ (↑P).index
-- Mathlib.GroupTheory.Perm.ConjAct
/-- A permutation `c` is a cycle of `g` iff `k • c` is a cycle of `k • g`  -/
Equiv.Perm.mem_cycleFactorsFinset_conj' : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (k : ConjAct (Equiv.Perm α)) (g c : Equiv.Perm α),
  k • c ∈ (k • g).cycleFactorsFinset ↔ c ∈ g.cycleFactorsFinset
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Stmt.pop.injEq : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (k : K) (a : σ → Option (Γ k) → σ)
  (a_1 : Turing.TM2.Stmt Γ Λ σ) (k_1 : K) (a_2 : σ → Option (Γ k_1) → σ) (a_3 : Turing.TM2.Stmt Γ Λ σ),
  (Turing.TM2.Stmt.pop k a a_1 = Turing.TM2.Stmt.pop k_1 a_2 a_3) = (k = k_1 ∧ a ≍ a_2 ∧ a_1 = a_3)
-- Init.Data.String.Basic
String.Pos.Raw.IsValid.exists : ∀ {s : String} {p : String.Pos.Raw},
  String.Pos.Raw.IsValid s p → ∃ m₁ m₂, m₁.utf8Encode = s.toByteArray.extract 0 p.byteIdx ∧ String.ofList (m₁ ++ m₂) = s
-- Init.Data.String.Iterate
String.Slice.PosIterator.currPos : {s : String.Slice} → s.PosIterator → s.Pos
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
addOrderOf_eq_card_of_zmultiples_eq_top : ∀ {G : Type u_2} [inst : AddGroup G] {g : G}, AddSubgroup.zmultiples g = ⊤ → addOrderOf g = Nat.card G
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Submodule.IsAssociatedPrime.toIsPrime : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M} {I : Ideal R}, N.IsAssociatedPrime I → I.IsPrime
-- Lean.Meta.TryThis
/-- Style the same way as an inaccessible hypothesis appearing in the infoview.  -/
Lean.Meta.Tactic.TryThis.SuggestionStyle.asInaccessible : Lean.Meta.Tactic.TryThis.SuggestionStyle
-- Mathlib.Data.Finset.Sigma
biInf_finsetSigma : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} [inst : CompleteLattice β] (s : Finset ι)
  (t : (i : ι) → Finset (α i)) (f : Sigma α → β), ⨅ ij ∈ s.sigma t, f ij = ⨅ i ∈ s, ⨅ j ∈ t i, f ⟨i, j⟩
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.Presheaf.isSheaf_bot : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  (P : CategoryTheory.Functor Cᵒᵖ A), CategoryTheory.Presheaf.IsSheaf ⊥ P
-- Mathlib.ModelTheory.Basic
/-- An embedding of first-order structures is an embedding that commutes with the
interpretations of functions and relations.  -/
FirstOrder.Language.Embedding : (L : FirstOrder.Language) → (M : Type w) → (N : Type w') → [L.Structure M] → [L.Structure N] → Type (max w w')
-- Mathlib.RingTheory.IsGaloisGroup.Defs
IsGaloisGroup.ringEquiv.eq_1 : ∀ (G : Type u_1) (A : Type u_2) (A' : Type u_3) (B : Type u_4) [inst : Group G] [inst_1 : CommSemiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra A B] [inst_4 : MulSemiringAction G B] [hA : IsGaloisGroup G A B]
  [inst_5 : FaithfulSMul A B] [inst_6 : CommSemiring A'] [inst_7 : Algebra A' B] [inst_8 : FaithfulSMul A' B]
  [hA' : IsGaloisGroup G A' B],
  IsGaloisGroup.ringEquiv G A A' B =
    (IsGaloisGroup.ringEquivFixedPoints G A B).trans (IsGaloisGroup.ringEquivFixedPoints G A' B).symm
-- Init.Data.Nat.Lemmas
_private.Init.Data.Nat.Lemmas.0.Nat.allLTTR.loop.eq_1 : ∀ (n : ℕ) (f : (i : ℕ) → i < n → Bool) (x_2 : 0 ≤ n), Nat.allLTTR.loop✝ n f 0 x_2 = true
-- Mathlib.Topology.VectorBundle.Basic
/-- Local homeomorphism version of the trivialization change.  -/
VectorBundleCore.trivChange : {R : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField R] →
        [inst_1 : NormedAddCommGroup F] →
          [inst_2 : NormedSpace R F] →
            [inst_3 : TopologicalSpace B] →
              {ι : Type u_5} → VectorBundleCore R B F ι → ι → ι → OpenPartialHomeomorph (B × F) (B × F)
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.nonnegg_cases_right : ∀ {c d a : ℕ} {b : ℤ}, (∀ (x : ℕ), b = -↑x → Zsqrtd.SqLe x c a d) → Zsqrtd.Nonnegg c d (↑a) b
-- Mathlib.Combinatorics.SimpleGraph.Tutte
/-- A set certifying non-existence of a perfect matching  -/
SimpleGraph.IsTutteViolator : {V : Type u_1} → SimpleGraph V → Set V → Prop
-- Mathlib.Algebra.Category.Grp.Ulift
/-- The universe lift functor for commutative groups is full.  -/
CommGrpCat.instFullUliftFunctor : CommGrpCat.uliftFunctor.Full
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.ae_eq_empty : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s : Set α}, s =ᵐ[μ] ∅ ↔ μ s = 0
-- Init.System.IO
/-- The path of the file indicated by the directory entry.  -/
IO.FS.DirEntry.path : IO.FS.DirEntry → System.FilePath
-- Init.Task
/-- Creates a task that, when all `tasks` have finished, computes the result of `f` applied to their
results.
 -/
Task.mapList : {α : Type u_1} →
  {β : Type u_2} →
    (List α → β) → List (Task α) → optParam Task.Priority Task.Priority.default → optParam Bool false → Task β
-- Mathlib.Order.CompleteLattice.Basic
biSup_lt_eq_iSup : ∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Type u_8} [inst_1 : LT ι] [NoMaxOrder ι] {f : ι → α},
  ⨆ i, ⨆ j, ⨆ (_ : j < i), f j = ⨆ i, f i
-- Init.Data.List.Erase
List.length_erase_of_mem : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l : List α}, a ∈ l → (l.erase a).length = l.length - 1
-- Mathlib.Data.Multiset.Bind
Multiset.sigma_singleton : ∀ {α : Type u_1} {β : Type v} (a : α) (b : α → β), ({a}.sigma fun a => {b a}) = {⟨a, b a⟩}
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
/-- A class of morphisms `W : MorphismProperty C` is stable under transfinite compositions
of shape `J` if for any well-order-continuous functor `F : J ⥤ C` such that
`F.obj j ⟶ F.obj (Order.succ j)` is in `W`, then `F.obj ⊥ ⟶ c.pt` is in `W`
for any colimit cocone `c : Cocone F`.  -/
CategoryTheory.MorphismProperty.IsStableUnderTransfiniteCompositionOfShape : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.MorphismProperty C →
      (J : Type w) → [inst : LinearOrder J] → [SuccOrder J] → [OrderBot J] → [WellFoundedLT J] → Prop
-- Std.Data.DTreeMap.Basic
/-- Modifies in place the value associated with a given key,
allowing creating new values and deleting values via an `Option` valued replacement function.

This function ensures that the value is used linearly.
 -/
Std.DTreeMap.alter : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.LawfulEqCmp cmp] → Std.DTreeMap α β cmp → (a : α) → (Option (β a) → Option (β a)) → Std.DTreeMap α β cmp
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.coprodMk_inr : ∀ (X Y : AlgebraicGeometry.Scheme) (x : ↥Y),
  (AlgebraicGeometry.coprodMk X Y) (Sum.inr x) = CategoryTheory.Limits.coprod.inr x
-- Lean.Language.Basic
/-- The base class of all snapshots: all the generic information the language server needs about a
snapshot.  -/
Lean.Language.Snapshot : Type
-- Mathlib.Order.SetAccumulate
Set.exists_accumulate_eq_univ_iff_of_directed : ∀ {α : Type u_1} {s : ℕ → Set α},
  Directed (fun x1 x2 => x1 ⊆ x2) s → ((∃ n, Set.accumulate s n = Set.univ) ↔ ∃ n, s n = Set.univ)
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
HomogeneousIdeal.map_id : ∀ {A : Type u_1} {σ : Type u_4} {ι : Type u_7} [inst : Semiring A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] {𝒜 : ι → σ} [inst_5 : GradedRing 𝒜]
  {I : HomogeneousIdeal 𝒜}, HomogeneousIdeal.map (GradedRingHom.id 𝒜) I = I
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.norm_eq_one_iff' : ∀ {d : ℤ}, d ≤ 0 → ∀ (z : ℤ√d), z.norm = 1 ↔ IsUnit z
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.CasesTypes.casesMap : Lean.Meta.Grind.CasesTypes → Lean.PHashMap Lean.Name Bool
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.colimitHomIsoLimitYoneda_hom_comp_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (F : CategoryTheory.Functor I C) [inst_2 : CategoryTheory.Limits.HasColimit F]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type u₂)] (A : C) (i : I),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitHomIsoLimitYoneda F A).hom
      (CategoryTheory.Limits.limit.π (F.op.comp (CategoryTheory.yoneda.obj A)) (Opposite.op i)) =
    (CategoryTheory.yoneda.obj A).map (CategoryTheory.Limits.colimit.ι F i).op
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_list_le_max : ∀ (α : Type u), Cardinal.mk (List α) ≤ max Cardinal.aleph0 (Cardinal.mk α)
-- Lean.Meta.Sym.InstantiateS
_private.Lean.Meta.Sym.InstantiateS.0.Lean.Meta.Sym.instantiateRevBetaS'.visitBVar : Array Lean.Expr → Lean.Expr → ℕ → ℕ → Lean.Meta.Sym.M✝ Lean.Expr
-- Mathlib.Order.Interval.Multiset
Multiset.Ico_cons_right : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α},
  a ≤ b → b ::ₘ Multiset.Ico a b = Multiset.Icc a b