mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.OreLocalization.Basic
OreLocalization.add_zero : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : AddMonoid X] [inst_3 : DistribMulAction R X] (x : OreLocalization S X), x + 0 = x
-- Mathlib.Order.UpperLower.Basic
isLowerSet_iUnion₂ : ∀ {α : Type u_1} {ι : Sort u_3} {κ : ι → Sort u_4} [inst : LE α] {f : (i : ι) → κ i → Set α},
  (∀ (i : ι) (j : κ i), IsLowerSet (f i j)) → IsLowerSet (⋃ i, ⋃ j, f i j)
-- Mathlib.Order.LiminfLimsup
/-- Same as `limsup_const` applied to `⊥` but without the `NeBot f` assumption  -/
Filter.limsup_const_bot : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β}, Filter.limsup (fun x => ⊥) f = ⊥
-- Mathlib.NumberTheory.LSeries.Nonvanishing
DirichletCharacter.LFunction_isBigO_horizontal : ∀ {N : ℕ} (χ : DirichletCharacter ℂ N) [inst : NeZero N] {y : ℝ},
  y ≠ 0 ∨ χ ≠ 1 →
    (fun x => DirichletCharacter.LFunction χ (1 + ↑x + Complex.I * ↑y)) =O[nhdsWithin 0 (Set.Ioi 0)] fun x => 1
-- Mathlib.FieldTheory.Finite.Basic
/-- **Fermat's Little Theorem**: for all `a : ℤ` coprime to `p`, we have
`a ^ (p - 1) ≡ 1 [ZMOD p]`.  -/
Int.ModEq.pow_card_sub_one_eq_one : ∀ {p : ℕ}, Nat.Prime p → ∀ {n : ℤ}, IsCoprime n ↑p → n ^ (p - 1) ≡ 1 [ZMOD ↑p]
-- Mathlib.Analysis.Calculus.FDeriv.Add
differentiableAt_comp_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} (a : E), DifferentiableAt 𝕜 (fun x => f (x - a)) x ↔ DifferentiableAt 𝕜 f (x - a)
-- Mathlib.Algebra.Ring.Opposite
AddOpposite.instIntCast.eq_1 : ∀ {R : Type u_1} [inst : IntCast R], AddOpposite.instIntCast = { intCast := fun n => AddOpposite.op ↑n }
-- Mathlib.RingTheory.HopfAlgebra.GroupLike
GroupLike.val_inv_toUnits_apply : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : HopfAlgebra R A]
  (a : GroupLike R A), ↑((GroupLike.toUnits R) a)⁻¹ = (HopfAlgebraStruct.antipode R) ↑a
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- A constructor for isomorphisms in the category `ShortComplex C`  -/
CategoryTheory.ShortComplex.isoMk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (e₁ : S₁.X₁ ≅ S₂.X₁) →
          (e₂ : S₁.X₂ ≅ S₂.X₂) →
            (e₃ : S₁.X₃ ≅ S₂.X₃) →
              autoParam
                  (CategoryTheory.CategoryStruct.comp e₁.hom S₂.f = CategoryTheory.CategoryStruct.comp S₁.f e₂.hom)
                  CategoryTheory.ShortComplex.isoMk._auto_1 →
                autoParam
                    (CategoryTheory.CategoryStruct.comp e₂.hom S₂.g = CategoryTheory.CategoryStruct.comp S₁.g e₃.hom)
                    CategoryTheory.ShortComplex.isoMk._auto_3 →
                  (S₁ ≅ S₂)
-- Mathlib.Data.Matrix.PEquiv
PEquiv.mul_toMatrix_apply : ∀ {l : Type u_2} {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : NonAssocSemiring α]
  [inst_2 : DecidableEq n] (M : Matrix l m α) (f : m ≃. n) (i : l) (j : n),
  (M * f.toMatrix) i j = Option.casesOn (f.symm j) 0 (M i)
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- `Scheme.Γ.rightOp : Scheme ⥤ CommRingCatᵒᵖ` preserves limits of diagrams consisting of
affine schemes.  -/
AlgebraicGeometry.preservesLimit_rightOp_Γ : ∀ {I : Type w} [inst : CategoryTheory.Category.{v, w} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme)
  [∀ (i : I), AlgebraicGeometry.IsAffine (D.obj i)],
  CategoryTheory.Limits.PreservesLimit D AlgebraicGeometry.Scheme.Γ.rightOp
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.instSub : {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → AddGroup (β i)] → Sub (Π₀ (i : ι), β i)
-- Mathlib.NumberTheory.ModularForms.Basic
/-- **Alias** of `add_apply`. -/
ModularForm.add_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Add β}
  {inst_2 : Add F} [self : IsAddApply F α β] (f g : F) (x : α), (f + g) x = f x + g x
-- Mathlib.NumberTheory.ClassNumber.Finite
/-- We can approximate `a / b : L` with `q / r`, where `r` has finitely many options for `L`.  -/
ClassGroup.exists_mem_finsetApprox : ∀ {R : Type u_1} {S : Type u_2} [inst : EuclideanDomain R] [inst_1 : CommRing S] [inst_2 : IsDomain S]
  [inst_3 : Algebra R S] {abv : AbsoluteValue R ℤ} {ι : Type u_5} [inst_4 : DecidableEq ι] [inst_5 : Fintype ι]
  (bS : Module.Basis ι R S) (adm : abv.IsAdmissible) [inst_6 : Infinite R] [inst_7 : DecidableEq R] (a : S) {b : R},
  b ≠ 0 →
    ∃ q,
      ∃ r ∈ ClassGroup.finsetApprox bS adm,
        abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))
-- Std.Data.ExtDTreeMap.Basic
/-- Folds the given monadic function over the mappings in the map in ascending order.  -/
Std.ExtDTreeMap.foldlM : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      {δ : Type w} →
        {m : Type w → Type w₂} →
          [inst : Monad m] →
            [LawfulMonad m] → [Std.TransCmp cmp] → (δ → (a : α) → β a → m δ) → δ → Std.ExtDTreeMap α β cmp → m δ
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- Pull back a `HasExactColimitsOfShape J` along a functor which preserves and reflects finite limits
and preserves colimits of shape `J`
 -/
CategoryTheory.HasExactColimitsOfShape.domain_of_functor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} (J : Type u_2)
  [inst_1 : CategoryTheory.Category.{v_1, u_2} J] [inst_2 : CategoryTheory.Category.{v_2, u_1} D]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C] [inst_4 : CategoryTheory.Limits.HasColimitsOfShape J D]
  [CategoryTheory.HasExactColimitsOfShape J D] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.ReflectsFiniteLimits F]
  [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.PreservesColimitsOfShape J F],
  CategoryTheory.HasExactColimitsOfShape J C
-- Mathlib.Data.Matrix.Basic
LinearEquiv.entryLinearMap_comp_mapMatrix : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {α : Type u_11} {β : Type u_12} [inst : Semiring R]
  [inst_1 : Semiring S] [inst_2 : AddCommMonoid α] [inst_3 : AddCommMonoid β] [inst_4 : Module R α]
  [inst_5 : Module S β] {σᵣₛ : R →+* S} {σₛᵣ : S →+* R} [inst_6 : RingHomInvPair σᵣₛ σₛᵣ]
  [inst_7 : RingHomInvPair σₛᵣ σᵣₛ] (f : α ≃ₛₗ[σᵣₛ] β) (i : m) (j : n),
  Matrix.entryLinearMap S β i j ∘ₛₗ ↑f.mapMatrix = ↑f ∘ₛₗ Matrix.entryLinearMap R α i j
-- Std.Time.Date.Basic
/-- Convert `Week.Offset` into `Millisecond.Offset`.
 -/
Std.Time.Millisecond.Offset.ofWeeks : Std.Time.Week.Offset → Std.Time.Millisecond.Offset
-- Mathlib.Algebra.Ring.Parity
Nat.one_add_div_two_mul_two_of_odd : ∀ {n : ℕ}, Odd n → 1 + n / 2 * 2 = n
-- Aesop.Search.Queue
Aesop.BestFirstQueue.ActiveGoal.priority : Aesop.BestFirstQueue.ActiveGoal → Aesop.Percent
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.ensureInsideFor : Lean.Elab.Term.Do.ToCodeBlock.M Unit
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.homologyData_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [inst_2 : CategoryTheory.Limits.HasZeroObject C] (s : S.Splitting),
  s.homologyData.left = s.leftHomologyData
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.Hom.mk.inj : ∀ {A : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} A} {B : Type u_2}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} B} {T : Type u_3} {inst_2 : CategoryTheory.Category.{v_3, u_3} T}
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B}
  {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W}
  {toCommaMorphism : CategoryTheory.CommaMorphism X.toComma Y.toComma} {prop_hom_left : Q toCommaMorphism.left}
  {prop_hom_right : W toCommaMorphism.right} {toCommaMorphism_1 : CategoryTheory.CommaMorphism X.toComma Y.toComma}
  {prop_hom_left_1 : Q toCommaMorphism_1.left} {prop_hom_right_1 : W toCommaMorphism_1.right},
  { toCommaMorphism := toCommaMorphism, prop_hom_left := prop_hom_left, prop_hom_right := prop_hom_right } =
      { toCommaMorphism := toCommaMorphism_1, prop_hom_left := prop_hom_left_1, prop_hom_right := prop_hom_right_1 } →
    toCommaMorphism = toCommaMorphism_1
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
_private.Mathlib.Combinatorics.SimpleGraph.FiveWheelLike.0.SimpleGraph.IsNClique.insert_insert : ∀ {α : Type u_1} {a b : α} {s : Finset α} {G : SimpleGraph α} {r : ℕ} [inst : DecidableEq α],
  G.IsNClique r (insert a s) →
    G.IsNClique r (insert b s) → b ∉ s → G.Adj a b → G.IsNClique (r + 1) (insert b (insert a s))
-- Mathlib.Algebra.Group.Basic
add_add_neg_add_cancel : ∀ {G : Type u_3} [inst : AddGroup G] (a b c : G), a + b + (-b + c) = a + c
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.Const.alter!.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Sort u_3) (sz : ℕ) (k' : α)
  (v' : β) (l' r' : Std.DTreeMap.Internal.Impl α fun x => β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (sz : ℕ) →
      (k' : α) →
        (v' : β) →
          (l' r' : Std.DTreeMap.Internal.Impl α fun x => β) → motive (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r')),
  (match Std.DTreeMap.Internal.Impl.inner sz k' v' l' r' with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner sz k' v' l' r' => h_2 sz k' v' l' r') =
    h_2 sz k' v' l' r'
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k fallback : α},
  Std.Internal.List.containsKey k l = false →
    toInsert.contains k = false →
      Std.Internal.List.getKeyD k (Std.Internal.List.insertListIfNewUnit l toInsert) fallback = fallback
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
GradedTensorProduct.instAlgebra : {R : Type u_1} →
  {ι : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : CommSemiring ι] →
          [inst_1 : DecidableEq ι] →
            [inst_2 : CommRing R] →
              [inst_3 : Ring A] →
                [inst_4 : Ring B] →
                  [inst_5 : Algebra R A] →
                    [inst_6 : Algebra R B] →
                      (𝒜 : ι → Submodule R A) →
                        (ℬ : ι → Submodule R B) →
                          [inst_7 : GradedAlgebra 𝒜] →
                            [inst_8 : GradedAlgebra ℬ] →
                              [inst_9 : Module ι (Additive ℤˣ)] → Algebra R (GradedTensorProduct R 𝒜 ℬ)
-- Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
CategoryTheory.MonoidalCategory.externalProductFlip_hom_app_app_app_app : ∀ (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [inst : CategoryTheory.Category.{v₁, u₁} J₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  [inst_3 : CategoryTheory.MonoidalCategory C] [inst_4 : CategoryTheory.BraidedCategory C]
  (X : CategoryTheory.Functor J₁ C) (X_1 : CategoryTheory.Functor J₂ C) (X_2 : J₂) (X_3 : J₁),
  ((((CategoryTheory.MonoidalCategory.externalProductFlip J₁ J₂ C).hom.app X).app X_1).app X_2).app X_3 =
    (β_ (X.obj X_3) (X_1.obj X_2)).hom
-- Init.Data.List.ToArray
Array.toList_swap : ∀ {α : Type u_1} (xs : Array α) (i j : ℕ) (hi : i < xs.size) (hj : j < xs.size),
  (xs.swap i j hi hj).toList = (xs.toList.set i xs[j]).set j xs[i]
-- Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic
/-- Derive a unit-distance embedding of `H` from a unit-distance embedding of `G` containing `H`.  -/
SimpleGraph.UnitDistEmbedding.copy : {V : Type u_1} →
  {W : Type u_2} →
    {G : SimpleGraph V} →
      {H : SimpleGraph W} →
        {E : Type u_3} → [inst : MetricSpace E] → G.UnitDistEmbedding E → H.Copy G → H.UnitDistEmbedding E
-- Mathlib.RingTheory.MatrixAlgebra
Matrix.toAlgEquiv_kroneckerStarAlgEquiv : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_5) [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  [inst_3 : Fintype m] [inst_4 : DecidableEq m] [inst_5 : StarRing R],
  (Matrix.kroneckerStarAlgEquiv m n R).toAlgEquiv = Matrix.kroneckerAlgEquiv m n R
-- Mathlib.RingTheory.Localization.AtPrime.Basic
IsLocalization.AtPrime.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (P P_1 : Ideal R) (e_P : P = P_1) [hp : P.IsPrime], IsLocalization.AtPrime S P = IsLocalization.AtPrime S P_1
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.coe_bot : ∀ {α : Type u_2} [inst : BooleanAlgebra α], ↑⊥ = {⊥, ⊤}
-- Mathlib.Order.Filter.FilterProduct
Filter.Germ.instSemifield : {α : Type u} → {β : Type v} → {φ : Ultrafilter α} → [Semifield β] → Semifield ((↑φ).Germ β)
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.unop_sSup : ∀ {M : Type u_2} [inst : Add M] (S : Set (AddSubsemigroup Mᵃᵒᵖ)), (sSup S).unop = sSup (AddSubsemigroup.op ⁻¹' S)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.canonicalEmbedding.integerLattice.inter_ball_finite : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (r : ℝ),
  (↑(NumberField.canonicalEmbedding.integerLattice K) ∩ Metric.closedBall 0 r).Finite
-- Mathlib.NumberTheory.ModularForms.Derivative
Derivative.normalizedDerivOfComplex_smul : ∀ (c : ℂ) (F : UpperHalfPlane → ℂ),
  MDiff F → Derivative.normalizedDerivOfComplex (c • F) = c • Derivative.normalizedDerivOfComplex F
-- Lean.Expr
Lean.Expr.letName! : Lean.Expr → Lean.Name
-- Mathlib.Tactic.ClickSuggestions.TryPremises
/-- Combine the results of looking up in various discrimination trees into an Array
of sections of candidates, where each section corresponds to one kind of match with the
discrimination tree.  -/
_private.Mathlib.Tactic.ClickSuggestions.TryPremises.0.Mathlib.Tactic.ClickSuggestions.getCandidatesAux : Lean.Expr →
  Lean.Expr →
    Array Mathlib.Tactic.ClickSuggestions.GrwPos →
      Mathlib.Tactic.ClickSuggestions.RwKind →
        Option Lean.Expr →
          (String → BaseIO Unit) →
            (Lean.Expr → Lean.MetaM (Lean.Meta.RefinedDiscrTree.MatchResult Mathlib.Tactic.ClickSuggestions.RwLemma)) →
              (Lean.Expr →
                  Lean.MetaM (Lean.Meta.RefinedDiscrTree.MatchResult Mathlib.Tactic.ClickSuggestions.GrwLemma)) →
                (Lean.Expr →
                    Lean.MetaM (Lean.Meta.RefinedDiscrTree.MatchResult Mathlib.Tactic.ClickSuggestions.ApplyLemma)) →
                  (Lean.Expr →
                      Lean.MetaM
                        (Lean.Meta.RefinedDiscrTree.MatchResult Mathlib.Tactic.ClickSuggestions.ApplyAtLemma)) →
                    Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM
                      (Array Mathlib.Tactic.ClickSuggestions.Candidates✝)
-- Mathlib.Data.ENat.Basic
/-- **Alias** of `ENat.natCast_add`. -/
ENat.coe_add : ∀ (m n : ℕ), ↑(m + n) = ↑m + ↑n
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
HomologicalComplex.instHasFiniteColimits : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteColimits C],
  CategoryTheory.Limits.HasFiniteColimits (HomologicalComplex C c)
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.exists_inverse : ∀ {n : ℕ} (c : OrderedFinpartition n) (j : Fin n), ∃ p, c.emb p.fst p.snd = j
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.getCast : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] →
      [LawfulBEq α] →
        (a : α) → (l : Std.DHashMap.Internal.AssocList α β) → Std.DHashMap.Internal.AssocList.contains a l = true → β a
-- Init.Data.Int.ToString
Int.repr_eq_if : ∀ {a : ℤ}, a.repr = if 0 ≤ a then a.toNat.repr else "-" ++ (-a).toNat.repr
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.inl_ι_assoc : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂}
  (self : F.PushoutObjObj f₁ f₂) {Z : C₃} (h : (F.obj Y₁).obj Y₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.inl (CategoryTheory.CategoryStruct.comp self.ι h) =
    CategoryTheory.CategoryStruct.comp ((F.obj Y₁).map f₂) h
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_
CategoryTheory.comonEquiv_inverse : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.comonEquiv.inverse = CategoryTheory.cartesianComon C
-- Init.Data.List.Attach
List.unattach_attach : ∀ {α : Type u_1} {l : List α}, l.attach.unattach = l
-- Batteries.Data.HashMap.Basic
/-- `HashMap α β` is a key-value map which stores elements in an array using a hash function
to find the values. This allows it to have very good performance for lookups
(average `O(1)` for a perfectly random hash function), but it is not a persistent data structure,
meaning that one should take care to use the map linearly when performing updates.
Copies are `O(n)`.
 -/
Batteries.HashMap : (α : Type u) → Type v → [BEq α] → [Hashable α] → Type (max u v)
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ioc.instCancelMonoid : {R : Type u_2} →
  [inst : Ring R] → [inst_1 : PartialOrder R] → [IsStrictOrderedRing R] → [IsDomain R] → CancelMonoid ↑(Set.Ioc 0 1)
-- Mathlib.Data.PFun
PFun.fixInduction.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {C : α → Sort u_7} {f : α →. β ⊕ α} {b : β} {a : α} (h : b ∈ f.fix a)
  (H H_1 : (a' : α) → b ∈ f.fix a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'),
  H = H_1 → PFun.fixInduction h H = PFun.fixInduction h H_1
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearEquiv.congrRight_symm : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N₁ : Type u_9}
  {N₂ : Type u_10} [inst_3 : AddCommMonoid N₁] [inst_4 : AddCommMonoid N₂] [inst_5 : Module R N₁] [inst_6 : Module R N₂]
  (e : N₁ ≃ₗ[R] N₂), e.congrRight₂.symm = e.symm.congrRight₂
-- Mathlib.Control.Basic
/-- Computations performed first on `a : α` and then on `b : β` are equal to those performed in
the reverse order.  -/
CommApplicative.commutative_prod : ∀ {m : Type u → Type v} {inst : Applicative m} [self : CommApplicative m] {α β : Type u} (a : m α) (b : m β),
  Prod.mk <$> a <*> b = (fun b a => (a, b)) <$> b <*> a
-- Mathlib.Algebra.Order.Ring.NNRat
NNRat.instIsStrictOrderedRing : IsStrictOrderedRing ℚ≥0
-- Mathlib.Tactic.NormNum.IsSquare
Mathlib.Meta.NormNum.iff_isSquare_of_isNat_rat : ∀ (a : ℚ) (n : ℕ), Mathlib.Meta.NormNum.IsNat a n → (IsSquare n ↔ IsSquare a)
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.dot.inj : ∀ {termInfo : Lean.Elab.TermInfo} {expectedType? : Option Lean.Expr} {termInfo_1 : Lean.Elab.TermInfo}
  {expectedType?_1 : Option Lean.Expr},
  Lean.Elab.CompletionInfo.dot termInfo expectedType? = Lean.Elab.CompletionInfo.dot termInfo_1 expectedType?_1 →
    termInfo = termInfo_1 ∧ expectedType? = expectedType?_1
-- Init.Data.AC
_private.Init.Data.AC.0.Lean.Data.AC.removeNeutrals.match_1.eq_1 : ∀ (motive : List ℕ → Sort u_1) (h_1 : Unit → motive []) (h_2 : (ys : List ℕ) → motive ys),
  (match [] with
    | [] => h_1 ()
    | ys => h_2 ys) =
    h_1 ()
-- Lean.DocString.Extension
Lean.VersoModuleDocs : Type
-- Mathlib.Data.Finset.Lattice.Fold
Finset.lt_inf'_iff : ∀ {α : Type u_2} {ι : Type u_5} [inst : LinearOrder α] {s : Finset ι} (H : s.Nonempty) {f : ι → α} {a : α},
  a < s.inf' H f ↔ ∀ i ∈ s, a < f i
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_mul_X_pow : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n d : ℕ), (p * Polynomial.X ^ n).coeff (d + n) = p.coeff d
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Over.pullbackComp_inv_app_left : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T}
  [inst_1 : Q.IsMultiplicative] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) [inst_2 : P.IsStableUnderBaseChangeAlong f]
  [inst_3 : P.IsStableUnderBaseChangeAlong g] [inst_4 : P.HasPullbacksAlong f] [inst_5 : P.HasPullbacksAlong g]
  [inst_6 : Q.RespectsIso] [inst_7 : Q.IsStableUnderBaseChange]
  (fg : optParam (X ⟶ Z) (CategoryTheory.CategoryStruct.comp f g))
  (hfg :
    autoParam (fg = CategoryTheory.CategoryStruct.comp f g) CategoryTheory.MorphismProperty.Over.pullbackComp._auto_1)
  (X_1 : P.Over Q Z),
  ((CategoryTheory.MorphismProperty.Over.pullbackComp f g fg hfg).inv.app X_1).left =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackLeftPullbackSndIso X_1.hom g f).hom
      (CategoryTheory.Limits.pullback.map X_1.hom (CategoryTheory.CategoryStruct.comp f g) X_1.hom fg
        (CategoryTheory.CategoryStruct.id X_1.left) (CategoryTheory.CategoryStruct.id X)
        (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯)
-- Mathlib.NumberTheory.LSeries.ZetaZeros
isClosed_riemannZetaZeros : IsClosed riemannZetaZeros
-- Std.Do.WP.SimpLemmas
Std.Do.WP.monadMap_ReaderT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ρ : Type u} [Monad m] [inst : Std.Do.WP m ps]
  (f : {β : Type u} → m β → m β) {α : Type u} (x : ReaderT ρ m α) (Q : Std.Do.PostCond α (Std.Do.PostShape.arg ρ ps)),
  (Std.Do.wp (MonadFunctor.monadMap (fun {β} => f) x)).apply Q = fun s =>
    (Std.Do.wp (f (x.run s))).apply (fun a => Q.1 a s, Q.2)
-- Mathlib.RingTheory.Localization.AtPrime.Basic
IsLocalization.AtPrime.under_map_of_isMaximal : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : p.IsPrime] (Sₚ : Type u_5) [inst_4 : CommSemiring Sₚ] [inst_5 : Algebra S Sₚ]
  [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] (P : Ideal S) [P.IsMaximal] [P.LiesOver p],
  Ideal.under S (Ideal.map (algebraMap S Sₚ) P) = P
-- Mathlib.Data.Vector.Basic
/-- The empty `Vector` is a `Subsingleton`.  -/
List.Vector.zero_subsingleton : ∀ {α : Type u_1}, Subsingleton (List.Vector α 0)
-- Mathlib.Algebra.Polynomial.Div
Polynomial.X_pow_dvd_iff : ∀ {R : Type u} [inst : Semiring R] {f : Polynomial R} {n : ℕ}, Polynomial.X ^ n ∣ f ↔ ∀ d < n, f.coeff d = 0
-- Mathlib.Analysis.Distribution.TestFunction
/-- **Alias** of `FunLike.coe_zero`. -/
TestFunction.coe_zero : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Zero F] [inst_2 : Zero β]
  [IsZeroApply F α β], ⇑0 = 0
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey_union_of_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (mem : k ∈ m₂), (m₁ ∪ m₂).getKey k ⋯ = m₂.getKey k mem
-- Mathlib.Dynamics.PeriodicPts.Defs
/-- Minimal period of a point `x` under an endomorphism `f`. If `x` is not a periodic point of `f`,
then `minimalPeriod f x = 0`.  -/
Function.minimalPeriod : {α : Type u_1} → (α → α) → α → ℕ
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation.const : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  {s : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl},
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation fun x => s
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.OneHypercover.isoMk_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {S : C}
  {E F : J.OneHypercover S} (f : E.toPreOneHypercover ≅ F.toPreOneHypercover),
  (CategoryTheory.GrothendieckTopology.OneHypercover.isoMk f).inv = f.inv