mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.RightLinear.instIsIsoμᵣ : ∀ {D : Type u_1} {D' : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} D]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] (F : CategoryTheory.Functor D D') {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C] [inst_3 : CategoryTheory.MonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D]
  [inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'] [inst_6 : F.RightLinear C] (c : C) (d : D),
  CategoryTheory.IsIso (CategoryTheory.Functor.LaxRightLinear.μᵣ F d c)
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.rescale_zero : ∀ {R : Type u_1} [inst : CommSemiring R], PowerSeries.rescale 0 = PowerSeries.C.comp PowerSeries.constantCoeff
-- Init.Data.Option.Lemmas
Option.lawfulIdentity_merge : ∀ {α : Type u_1} (f : α → α → α), Std.LawfulIdentity (Option.merge f) none
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.walkingParallelPairHom_id : ∀ (X : CategoryTheory.Limits.WalkingParallelPair),
  CategoryTheory.Limits.WalkingParallelPairHom.id X = CategoryTheory.CategoryStruct.id X
-- Init.Data.List.Lemmas
List.foldr_flip_append_eq_append : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β} {l' : List β},
  List.foldr (fun x ys => ys ++ f x) l' l = l' ++ (List.map f l).reverse.flatten
-- Mathlib.Algebra.Ring.Prod
/-- Product of two rings is a ring.  -/
Prod.instRing : {R : Type u_1} → {S : Type u_3} → [Ring R] → [Ring S] → Ring (R × S)
-- Std.Data.DHashMap.Basic
/-- Computes the union of the given hash maps. If a key appears in both maps, the entry contained in
the second argument will appear in the result.

This function always merges the smaller map into the larger map, so the expected runtime is
`O(min(m₁.size, m₂.size))`.
 -/
Std.DHashMap.union : {α : Type u} →
  {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Std.DHashMap α β → Std.DHashMap α β → Std.DHashMap α β
-- Mathlib.MeasureTheory.Integral.IntegrableOn
StronglyMeasurableAtFilter.filter_mono : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : TopologicalSpace β] {l l' : Filter α} {f : α → β}
  {μ : MeasureTheory.Measure α}, StronglyMeasurableAtFilter f l μ → l' ≤ l → StronglyMeasurableAtFilter f l' μ
-- Mathlib.Algebra.Category.Ring.Under.Limits
/-- `Under.pushout f` preserves finite products.  -/
CommRingCat.Under.instPreservesFiniteProductsUnderPushout : ∀ {R S : CommRingCat} (f : R ⟶ S), CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.Under.pushout f)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_modify : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  (↑m).WF →
    ∀ {k k' : α} {fallback : β} {f : β → β},
      Std.DHashMap.Internal.Raw₀.Const.getD (Std.DHashMap.Internal.Raw₀.Const.modify m k f) k' fallback =
        if (k == k') = true then (Option.map f (Std.DHashMap.Internal.Raw₀.Const.get? m k)).getD fallback
        else Std.DHashMap.Internal.Raw₀.Const.getD m k' fallback
-- Mathlib.Algebra.Order.Hom.Ring
/-- Composition of two `OrderRingHom`s as an `OrderRingHom`.  -/
OrderRingHom.comp : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : NonAssocSemiring α] →
        [inst_1 : Preorder α] →
          [inst_2 : NonAssocSemiring β] →
            [inst_3 : Preorder β] →
              [inst_4 : NonAssocSemiring γ] → [inst_5 : Preorder γ] → β →+*o γ → α →+*o β → α →+*o γ
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.mk_injective : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] (A B : T), Function.Injective CategoryTheory.Arrow.mk
-- Lean.Meta.Sym.Apply
Lean.Meta.Sym.ApplyResult.goals.injEq : ∀ (mvarIds mvarIds_1 : List Lean.MVarId),
  (Lean.Meta.Sym.ApplyResult.goals mvarIds = Lean.Meta.Sym.ApplyResult.goals mvarIds_1) = (mvarIds = mvarIds_1)
-- Mathlib.Order.Compare
cmp_eq_lt_iff : ∀ {α : Type u_1} [inst : LinearOrder α] (x y : α), cmp x y = Ordering.lt ↔ x < y
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.instSMulOfSMulCommClassOfContinuousConstSMul : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        (σ : 𝕜₁ →+* 𝕜₂) →
          {E : Type u_3} →
            (F : Type u_4) →
              [inst_2 : AddCommGroup E] →
                [inst_3 : Module 𝕜₁ E] →
                  [inst_4 : TopologicalSpace E] →
                    [inst_5 : AddCommGroup F] →
                      [inst_6 : Module 𝕜₂ F] →
                        (M : Type u_6) →
                          [inst_7 : Monoid M] →
                            [inst_8 : DistribMulAction M F] →
                              [SMulCommClass 𝕜₂ M F] →
                                [inst_10 : TopologicalSpace F] →
                                  [ContinuousConstSMul M F] → (𝔖 : Set (Set E)) → SMul M (UniformConvergenceCLM σ F 𝔖)
-- Mathlib.Algebra.Algebra.Hom
Algebra.algebraMapSubmonoid_map_eq : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (M : Submonoid R)
  {B : Type w} [inst_3 : Semiring B] [inst_4 : Algebra R B] (f : A →ₐ[R] B),
  Submonoid.map f (Algebra.algebraMapSubmonoid A M) = Algebra.algebraMapSubmonoid B M
-- Std.Data.HashSet.Lemmas
Std.HashSet.get_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α} {h : (m.get? k).isSome = true}, (m.get? k).get h = m.get k ⋯
-- Lean.Parser.Term
Lean.Parser.darrow.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Ring.Prod
RingEquiv.zeroRingProd_apply : ∀ (R : Type u_1) (S : Type u_3) [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] [inst_2 : Subsingleton S]
  (x : R), (RingEquiv.zeroRingProd R S) x = (0, x)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Pos.skip?_bool_eq_none_iff : ∀ {p : Char → Bool} {s : String} {pos : s.Pos}, pos.skip? p = none ↔ ∀ (h : pos ≠ s.endPos), p (pos.get h) = false
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_ssubset_Icc_left : ∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b₁ b₂ : α}, a₂ ≤ b₂ → a₂ < a₁ → b₁ ≤ b₂ → Set.Icc a₁ b₁ ⊂ Set.Icc a₂ b₂
-- Mathlib.CategoryTheory.Dialectica.Monoidal
/-- The functorial action of `X ⊗ Y` in `Dial C`.  -/
CategoryTheory.Dial.tensorHomImpl : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] →
      [inst_2 : CategoryTheory.Limits.HasPullbacks C] →
        {X₁ X₂ Y₁ Y₂ : CategoryTheory.Dial C} → (X₁ ⟶ X₂) → (Y₁ ⟶ Y₂) → (X₁.tensorObjImpl Y₁ ⟶ X₂.tensorObjImpl Y₂)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.eraseMany_list : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ (l : List α), (t₁.eraseMany l).Equiv (t₂.eraseMany l)
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Submodule.cardQuot_eq_one_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {P : Submodule R M},
  P.cardQuot = 1 ↔ P = ⊤
-- Mathlib.Data.ZMod.Basic
ZMod.val_one_eq_one_mod : ∀ (n : ℕ), ZMod.val 1 = 1 % n
-- Init.Data.List.MinMax
List.max?_replicate_of_pos : ∀ {α : Type u_1} [inst : Max α] [Std.MaxEqOr α] {n : ℕ} {a : α}, 0 < n → (List.replicate n a).max? = some a
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.toContinuousMonoidHom.eq_1 : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] {F : Type u_7} [inst_4 : FunLike F A B] [inst_5 : MonoidHomClass F A B]
  [inst_6 : ContinuousMapClass F A B] (f : F), ↑f = { toMonoidHom := ↑f, continuous_toFun := ⋯ }
-- Mathlib.Data.Ordmap.Ordset
_private.Mathlib.Data.Ordmap.Ordset.0.Ordnode.Bounded.match_1.eq_2 : ∀ {α : Type u_1} (motive : Ordnode α → WithBot α → WithTop α → Sort u_2) (x : WithBot α) (x_1 : WithTop α)
  (h_1 : (a b : α) → motive Ordnode.nil (some a) (some b))
  (h_2 : (x : WithBot α) → (x_2 : WithTop α) → motive Ordnode.nil x x_2)
  (h_3 :
    (size : ℕ) →
      (l : Ordnode α) →
        (x : α) → (r : Ordnode α) → (o₁ : WithBot α) → (o₂ : WithTop α) → motive (Ordnode.node size l x r) o₁ o₂),
  (∀ (a b : α), x = some a → x_1 = some b → False) →
    (match Ordnode.nil, x, x_1 with
      | Ordnode.nil, some a, some b => h_1 a b
      | Ordnode.nil, x, x_3 => h_2 x x_3
      | Ordnode.node size l x r, o₁, o₂ => h_3 size l x r o₁ o₂) =
      h_2 x x_1
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndepOn.singleton : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {v : ι → M} {i : ι} [IsDomain R] [Module.IsTorsionFree R M], v i ≠ 0 → LinearIndepOn R v {i}
-- Mathlib.LinearAlgebra.Transvection.Basic
/-- Dilatransvections are linear equivalences `V ≃ₗ[R] V` whose associated linear map are given by
`LinearMap.transvection`, i.e., are of the form `x ↦ x + f x • v` for `f : Dual R V` and `v : V`.

Over a division ring, `LinearEquiv.mem_dilatransvections_iff_rank` shows that they correspond
to the linear equivalences which differ from the identity map by a linear map of rank at most 1.  -/
LinearEquiv.dilatransvections : (R : Type u_1) → (V : Type u_2) → [inst : Ring R] → [inst_1 : AddCommGroup V] → [inst_2 : Module R V] → Set (V ≃ₗ[R] V)
-- Mathlib.MeasureTheory.Function.AEEqFun
/-- Given a relation `r` and equivalence class `[f]` and `[g]`, return true if `r` holds of
`(f a, g a)` for almost all `a`  -/
MeasureTheory.AEEqFun.LiftRel : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      [inst : MeasurableSpace α] →
        {μ : MeasureTheory.Measure α} →
          [inst_1 : TopologicalSpace β] →
            [inst_2 : TopologicalSpace γ] → (β → γ → Prop) → (α →ₘ[μ] β) → (α →ₘ[μ] γ) → Prop
-- Mathlib.Order.Heyting.Basic
compl_inf_self : ∀ {α : Type u_2} [inst : HeytingAlgebra α] (a : α), aᶜ ⊓ a = ⊥
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₁₂.d₃_eq : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₁₂] [inst_9 : CategoryTheory.Preadditive C₄]
  (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [inst_10 : F₁₂.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_12 : G.Additive]
  [inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9}
  {ι₁₂ : Type u_10} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [inst_18 : DecidableEq ι₁₂]
  [inst_19 : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) {i₃ i₃' : ι₃},
  c₃.Rel i₃ i₃' →
    ∀ (j : ι₄),
      HomologicalComplex.mapBifunctor₁₂.d₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j =
        c₁₂.ε₂ c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃) •
          CategoryTheory.CategoryStruct.comp ((G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).map (K₃.d i₃ i₃'))
            (HomologicalComplex.mapBifunctor₁₂.ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃' j)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₂_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C) {Z : C} (h : S.L₃.X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.v₁₂.τ₂ (CategoryTheory.CategoryStruct.comp S.v₂₃.τ₂ h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupNorm.mk.sizeOf_spec : ∀ {G : Type u_6} [inst : AddGroup G] [inst_1 : SizeOf G] (toNonarchAddGroupSeminorm : NonarchAddGroupSeminorm G)
  (eq_zero_of_map_eq_zero' : ∀ (x : G), toNonarchAddGroupSeminorm.toFun x = 0 → x = 0),
  sizeOf
      { toNonarchAddGroupSeminorm := toNonarchAddGroupSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' } =
    1 + sizeOf toNonarchAddGroupSeminorm
-- Mathlib.Topology.Constructions
isClosedMap_ofDual : ∀ {X : Type u} [inst : TopologicalSpace X], IsClosedMap ⇑OrderDual.ofDual
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.IsPartition.iUnion_subset : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I},
  π.IsPartition → ∀ (π₁ : BoxIntegral.Prepartition I), π₁.iUnion ⊆ π.iUnion
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_op_pow : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] (s : Finset α) (n : ℕ),
  Finset.image MulOpposite.op (s ^ n) = Finset.image MulOpposite.op s ^ n
-- Mathlib.FieldTheory.Galois.Basic
IntermediateField.fixingSubgroup_antitone : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E],
  Antitone IntermediateField.fixingSubgroup
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.pre_map_right : ∀ {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] (S : D) (F : CategoryTheory.Functor B C)
  (G : CategoryTheory.Functor C D) {Y X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) (F.comp G)}
  (f : Y ⟶ X), ((CategoryTheory.StructuredArrow.pre S F G).map f).right = F.map f.right
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.δ_zero_mkOfSucc : ∀ {n : ℕ} (i : Fin n),
  CategoryTheory.CategoryStruct.comp (SimplexCategory.δ 0) (SimplexCategory.mkOfSucc i) =
    { len := 0 }.const { len := n } i.succ
-- Mathlib.RingTheory.Valuation.LocalSubring
/-- [Stacks Tag 00IC](https://stacks.math.columbia.edu/tag/00IC) -/
LocalSubring.mem_of_isMax_of_isIntegral : ∀ {K : Type u_3} [inst : Field K] {R : LocalSubring K},
  IsMax R → ∀ {x : K}, IsIntegral (↥R.toSubring) x → x ∈ R.toSubring
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.toMulEquiv : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] → [inst_3 : Algebra R A] → [inst_4 : Algebra R B] → (A ≃ₐ[R] B) → A ≃* B
-- Mathlib.Algebra.Group.TypeTags.Basic
isAddRegular_ofMul : ∀ {α : Type u} [inst : Monoid α] {a : α}, IsAddRegular (Additive.ofMul a) ↔ IsRegular a
-- Aesop.Index.RulePattern
/-- Add a rule pattern to the index.  -/
Aesop.RulePatternIndex.add : Aesop.RuleName → Aesop.RulePattern → Aesop.RulePatternIndex → Aesop.RulePatternIndex
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.σ₀Iter_δ_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  (i : Fin (n + 2)) (j : ℕ) {m : ℕ}
  (h : autoParam (m + (j + 1) = n + 1) CategoryTheory.SimplicialObject.σ₀Iter_δ._auto_1),
  autoParam (↑i ≤ j + 1) CategoryTheory.SimplicialObject.σ₀Iter_δ._auto_3 →
    ∀ {Z : C} (h_1 : X.obj (Opposite.op { len := n }) ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.σ₀Iter (j + 1) h) (CategoryTheory.CategoryStruct.comp (X.δ i) h_1) =
        CategoryTheory.CategoryStruct.comp (X.σ₀Iter j ⋯) h_1
-- Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
/-- Eta-expanded form of `InnerProductSpace.HarmonicContOnCl.add_const` -/
InnerProductSpace.HarmonicContOnCl.fun_add_const : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {s : Set E},
  InnerProductSpace.HarmonicContOnCl f s → ∀ (c : F), InnerProductSpace.HarmonicContOnCl (fun i => f i + c) s
-- Mathlib.Topology.Algebra.Group.Pointwise
IsOpen.add_closure_zero_eq : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {U : Set G},
  IsOpen U → U + closure {0} = U
-- Lean.Compiler.IR.Basic
Lean.IR.AlphaEqv.mk : {α : Type} → (Lean.IR.IndexRenaming → α → α → Bool) → Lean.IR.AlphaEqv α
-- Lean.Structure
_private.Lean.Structure.0.Lean.StructureState.mk.injEq : ∀ (map map_1 : Lean.PersistentHashMap Lean.Name Lean.StructureInfo), ({ map := map } = { map := map_1 }) = (map = map_1)
-- Mathlib.Algebra.Ring.Equiv
/-- Transport dependent functions through an equivalence of the base space.

This is `Equiv.piCongrLeft'` as a `RingEquiv`.  -/
RingEquiv.piCongrLeft' : {ι : Type u_7} →
  {ι' : Type u_8} →
    (R : ι → Type u_9) →
      (e : ι ≃ ι') → [inst : (i : ι) → NonUnitalNonAssocSemiring (R i)] → ((i : ι) → R i) ≃+* ((i : ι') → R (e.symm i))
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- The directed supremum of acyclic graphs is acyclic.  -/
SimpleGraph.isAcyclic_sSup_of_isAcyclic_directedOn : ∀ {V : Type u_1} (Hs : Set (SimpleGraph V)),
  (∀ H ∈ Hs, H.IsAcyclic) → DirectedOn (fun x1 x2 => x1 ≤ x2) Hs → (sSup Hs).IsAcyclic
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.OplaxLeftLinear.δₗ_unitality_hom_assoc : ∀ {D : Type u_1} {D' : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} D]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] (F : CategoryTheory.Functor D D') {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C] [inst_3 : CategoryTheory.MonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  [inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'] [inst_6 : F.OplaxLeftLinear C] (d : D) {Z : D'}
  (h : F.obj d ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxLeftLinear.δₗ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) d)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso (F.obj d)).hom h) =
    CategoryTheory.CategoryStruct.comp
      (F.map (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d).hom) h
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.size_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α},
  List.Pairwise (fun a b => (a == b) = false) l → (Std.DHashMap.Const.unitOfList l).size = l.length
-- Mathlib.Data.Multiset.Powerset
Multiset.powerset_coe : ∀ {α : Type u_1} (l : List α), (↑l).powerset = ↑(List.map Multiset.ofList l.sublists)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.isSemilinearSet_setOfFloorPos : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s) [inst : Finite ι],
  IsSemilinearSet (IsProperLinearSet.setOfFloorPos✝ hs)
-- Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
/-- The functor `DerivedCategory C₁ ⥤ DerivedCategory C₂` induced
by an exact functor `F : C₁ ⥤ C₂` between abelian categories.  -/
CategoryTheory.Functor.mapDerivedCategory : {C₁ : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
    [inst_1 : CategoryTheory.Abelian C₁] →
      [inst_2 : HasDerivedCategory C₁] →
        {C₂ : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_4 : CategoryTheory.Abelian C₂] →
              [inst_5 : HasDerivedCategory C₂] →
                (F : CategoryTheory.Functor C₁ C₂) →
                  [F.Additive] →
                    [CategoryTheory.Limits.PreservesFiniteLimits F] →
                      [CategoryTheory.Limits.PreservesFiniteColimits F] →
                        CategoryTheory.Functor (DerivedCategory C₁) (DerivedCategory C₂)
-- Mathlib.Tactic.ToExpr
Mathlib.instToExprMData_mathlib : Lean.ToExpr Lean.MData
-- Init.Data.Sum.Lemmas
Sum.LiftRel.lex : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {a b : α ⊕ β},
  Sum.LiftRel r s a b → Sum.Lex r s a b
-- Init.Data.Nat.Basic
Nat.add_left_cancel : ∀ {n m k : ℕ}, n + m = n + k → m = k
-- Lean.Server.Snapshots
Lean.Server.Snapshots.Snapshot.mpState : Lean.Server.Snapshots.Snapshot → Lean.Parser.ModuleParserState
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.instHashableSeq_lean.hash : Lean.Grind.AC.Seq → UInt64
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_comp_iff_of_isOpenImmersion : ∀ {X Y Z : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {g : Y ⟶ Z} {x : ↥X} [AlgebraicGeometry.IsOpenImmersion f],
  AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt (CategoryTheory.CategoryStruct.comp f g) x ↔
    AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt g (f x)
-- Mathlib.Data.Set.Equitable
Finset.EquitableOn.le : ∀ {α : Type u_1} {s : Finset α} {f : α → ℕ} {a : α}, (↑s).EquitableOn f → a ∈ s → (∑ i ∈ s, f i) / s.card ≤ f a
-- Mathlib.Order.Restriction
/-- Restrict domain of a function `f` indexed by `α` to elements `≤ a`, seen as a finite set.  -/
Preorder.frestrictLe : {α : Type u_1} →
  [inst : Preorder α] →
    {π : α → Type u_2} → [inst_1 : LocallyFiniteOrderBot α] → (a : α) → ((i : α) → π i) → (i : ↥(Finset.Iic a)) → π ↑i
-- Init.Data.Vector.Basic
/-- Insert an element into a vector using a `Nat` index. Panics if the index is out of bounds.  -/
Vector.insertIdx! : {α : Type u_1} → {n : ℕ} → Vector α n → ℕ → α → Vector α (n + 1)
-- Mathlib.Logic.Relation
Relation.ReflGen.stdSymm : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Symm r], Std.Symm (Relation.ReflGen r)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
pow_pos_iff : ∀ {α : Type u_1} [inst : LinearOrderedCommMonoidWithZero α] {a : α} {n : ℕ} [IsReduced α], n ≠ 0 → (0 < a ^ n ↔ 0 < a)
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk_eq_mk : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a b : M},
  MulArchimedeanClass.mk a = MulArchimedeanClass.mk b ↔ (∃ m, |b|ₘ ≤ |a|ₘ ^ m) ∧ ∃ n, |a|ₘ ≤ |b|ₘ ^ n
-- Mathlib.Data.Multiset.FinsetOps
Multiset.le_ndunion_right : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α), t ≤ s.ndunion t
-- Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
HomotopicalAlgebra.instFibrationFstOfIsFibrant : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_2 : CategoryTheory.Limits.HasTerminal C] (X Y : C) [(HomotopicalAlgebra.fibrations C).IsStableUnderBaseChange]
  [inst_4 : CategoryTheory.Limits.HasBinaryProduct X Y] [hY : HomotopicalAlgebra.IsFibrant Y],
  HomotopicalAlgebra.Fibration CategoryTheory.Limits.prod.fst
-- Init.Data.Array.InsertIdx
Array.getElem_insertIdx : ∀ {α : Type u} {xs : Array α} {x : α} {i k : ℕ} (w : i ≤ xs.size) (h : k < (xs.insertIdx i x w).size),
  (xs.insertIdx i x w)[k] = if h₁ : k < i then xs[k] else if h₂ : k = i then x else xs[k - 1]
-- Mathlib.Algebra.Lie.Basic
/-- It is sometimes useful to regard a `LieRing` as a `NonUnitalNonAssocRing`.  -/
LieRing.toNonUnitalNonAssocRing : (L : Type v) → [LieRing L] → NonUnitalNonAssocRing L
-- Mathlib.Lean.Meta.RefinedDiscrTree.Encode
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Encode.0.Lean.Meta.RefinedDiscrTree.Context.mk.injEq : ∀ (bvars bvars_1 : List Lean.FVarId), ({ bvars := bvars } = { bvars := bvars_1 }) = (bvars = bvars_1)
-- Mathlib.Analysis.Calculus.FDeriv.Add
differentiableOn_const_add_iff : ∀ {𝕜 : 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}
  {s : Set E} (c : F), DifferentiableOn 𝕜 (fun y => c + f y) s ↔ DifferentiableOn 𝕜 f s