mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Shift.Induced
CategoryTheory.shiftFunctorZero_hom_app_obj_of_induced : ∀ {C : Type u_3} {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} D] (F : CategoryTheory.Functor C D) (A : Type u_2) [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] (s : A → CategoryTheory.Functor D D)
  (i : (a : A) → F.comp (s a) ≅ (CategoryTheory.shiftFunctor C a).comp F)
  [inst_4 : ((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Full]
  [inst_5 : ((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Faithful] (X : C),
  (CategoryTheory.shiftFunctorZero D A).hom.app (F.obj X) =
    CategoryTheory.CategoryStruct.comp ((i 0).hom.app X) (F.map ((CategoryTheory.shiftFunctorZero C A).hom.app X))
-- Mathlib.Algebra.Group.Defs
NegZeroClass.mk : {G : Type u_2} → [toZero : Zero G] → [toNeg : Neg G] → -0 = 0 → NegZeroClass G
-- Mathlib.Analysis.Normed.Ring.Units
Units.oneSub.congr_simp : ∀ {R : Type u_4} [inst : NormedRing R] [inst_1 : HasSummableGeomSeries R] (t t_1 : R) (e_t : t = t_1) (h : ‖t‖ < 1),
  Units.oneSub t h = Units.oneSub t_1 ⋯
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeGroup.reduceCyclically.singleton : ∀ {α : Type u} [inst : DecidableEq α] {a : α × Bool}, FreeGroup.reduceCyclically [a] = [a]
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.add_subset_iff_left : ∀ {α : Type u_2} [inst : Add α] [inst_1 : DecidableEq α] {s t u : Finset α}, s + t ⊆ u ↔ ∀ a ∈ s, a +ᵥ t ⊆ u
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.card_le_of_model_distinctConstantsTheory : ∀ (L : FirstOrder.Language) {α : Type u'} (s : Set α) (M : Type w) [inst : (L.withConstants α).Structure M]
  [h : M ⊨ L.distinctConstantsTheory s], Cardinal.lift.{w, u'} (Cardinal.mk ↑s) ≤ Cardinal.lift.{u', w} (Cardinal.mk M)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_alter_le_size : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α], (↑m).WF → ∀ {k : α} {f : Option (β k) → Option (β k)}, (↑(m.alter k f)).size ≤ (↑m).size + 1
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Continuous.logb : ∀ {α : Type u_1} {b : ℝ} [inst : TopologicalSpace α] {f : α → ℝ},
  Continuous f → (∀ (x : α), f x ≠ 0) → Continuous fun x => Real.logb b (f x)
-- Mathlib.Data.List.Cycle
Cycle.Chain.eq_nil_of_irrefl : ∀ {α : Type u_1} {r : α → α → Prop} {s : Cycle α} [IsTrans α r] [Std.Irrefl r], Cycle.Chain r s → s = Cycle.nil
-- Mathlib.Order.CompleteBooleanAlgebra
Pi.instCompleteBooleanAlgebra : {ι : Type u_1} → {π : ι → Type u_2} → [(i : ι) → CompleteBooleanAlgebra (π i)] → CompleteBooleanAlgebra ((i : ι) → π i)
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Complex.norm_log_one_add_le : ∀ {z : ℂ}, ‖z‖ < 1 → ‖Complex.log (1 + z)‖ ≤ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_diff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α}, Std.DTreeMap.Const.get? (t₁ \ t₂) k = if k ∈ t₂ then none else Std.DTreeMap.Const.get? t₁ k
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullback.mapDesc_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y S T S' : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S)
  (i' : S ⟶ S') [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)]
  [inst_3 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp i i'))
      (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp i i'))]
  [inst_4 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f i) i')
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp g i) i')],
  CategoryTheory.Limits.pullback.mapDesc f g (CategoryTheory.CategoryStruct.comp i i') =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.mapDesc f g i)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.mapDesc (CategoryTheory.CategoryStruct.comp f i)
          (CategoryTheory.CategoryStruct.comp g i) i')
        (CategoryTheory.Limits.pullback.congrHom ⋯ ⋯).hom)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
  {h : Std.Internal.List.containsKey a (Std.Internal.List.insertEntry k v l) = true},
  Std.Internal.List.getValueCast a (Std.Internal.List.insertEntry k v l) h =
    if h' : (k == a) = true then cast ⋯ v else Std.Internal.List.getValueCast a l ⋯
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.isEmpty_alter_eq_isEmpty_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      (Std.DTreeMap.Raw.Const.alter t k f).isEmpty =
        ((t.erase k).isEmpty && (f (Std.DTreeMap.Raw.Const.get? t k)).isNone)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.PreOneHypercoverDenseData.mk : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {S : C} →
            (I₀ : Type w) →
              (X : I₀ → C₀) →
                (f : (i : I₀) → F.obj (X i) ⟶ S) →
                  (I₁ : I₀ → I₀ → Type w) →
                    (Y : ⦃i₁ i₂ : I₀⦄ → I₁ i₁ i₂ → C₀) →
                      (p₁ : ⦃i₁ i₂ : I₀⦄ → (j : I₁ i₁ i₂) → Y j ⟶ X i₁) →
                        (p₂ : ⦃i₁ i₂ : I₀⦄ → (j : I₁ i₁ i₂) → Y j ⟶ X i₂) →
                          (∀ ⦃i₁ i₂ : I₀⦄ (j : I₁ i₁ i₂),
                              CategoryTheory.CategoryStruct.comp (F.map (p₁ j)) (f i₁) =
                                CategoryTheory.CategoryStruct.comp (F.map (p₂ j)) (f i₂)) →
                            F.PreOneHypercoverDenseData S
-- Mathlib.ModelTheory.Types
/-- **Alias** of `FirstOrder.Language.Theory.CompleteType.setOfPred_subset_eq_univ_iff`. -/
FirstOrder.Language.Theory.CompleteType.setOf_subset_eq_univ_iff : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (S : (L.withConstants α).Theory),
  {p | S ⊆ ↑p} = Set.univ ↔ ∀ φ ∈ S, (L.lhomWithConstants α).onTheory T ⊨ᵇ φ
-- Mathlib.Analysis.Convex.StrictConvexBetween
/-- Given three collinear points, two (not equal) with distance `r` from `p` and one with
distance less than `r` from `p`, the third point is strictly between the other two points.  -/
Collinear.sbtw_of_dist_eq_of_dist_lt : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [StrictConvexSpace ℝ V]
  [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] {p p₁ p₂ p₃ : P} {r : ℝ},
  Collinear ℝ {p₁, p₂, p₃} → dist p₁ p = r → dist p₂ p < r → dist p₃ p = r → p₁ ≠ p₃ → Sbtw ℝ p₁ p₂ p₃
-- Mathlib.Order.Bounds.Basic
/-- **Alias** of `le_of_isGLB_Ioi`. -/
le_glb_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {b : α} (a : α), IsGLB (Set.Ioi a) b → a ≤ b
-- Mathlib.Topology.Order.Real
/-- Topology on `ℝ≥0∞`.

Note: this is different from the `EMetricSpace` topology. The `EMetricSpace` topology has
`IsOpen {∞}`, while this topology doesn't have singleton elements.  -/
ENNReal.instTopologicalSpace : TopologicalSpace ENNReal
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.C1.eq_1 : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (ho : o < Ordinal.type fun x1 x2 => x1 < x2),
  Profinite.NobelingProof.C1 C ho = C ∩ {f | f (Profinite.NobelingProof.term I ho) = true}
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multifork.ofι_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) (P : C) (ι : (a : J.L) → P ⟶ I.left a)
  (w :
    ∀ (b : J.R),
      CategoryTheory.CategoryStruct.comp (ι (J.fst b)) (I.fst b) =
        CategoryTheory.CategoryStruct.comp (ι (J.snd b)) (I.snd b)),
  (CategoryTheory.Limits.Multifork.ofι I P ι w).pt = P
-- Mathlib.Data.Multiset.ZeroCons
Multiset.forall_mem_cons : ∀ {α : Type u_1} {p : α → Prop} {a : α} {s : Multiset α}, (∀ x ∈ a ::ₘ s, p x) ↔ p a ∧ ∀ x ∈ s, p x
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.mkAllFunIndStx : Lean.Meta.Try.Info → Lean.TSyntax `tactic → Lean.MetaM (Lean.TSyntax `tactic)
-- Mathlib.Algebra.Group.Pi.Lemmas
Sigma.curry_add : ∀ {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [inst : (a : α) → (b : β a) → Add (γ a b)]
  (x y : (i : (a : α) × β a) → γ i.fst i.snd), Sigma.curry (x + y) = Sigma.curry x + Sigma.curry y
-- Mathlib.RingTheory.RootsOfUnity.Minpoly
/-- If `p` is a prime that does not divide `n`,
then the minimal polynomials of a primitive `n`-th root of unity `μ`
and of `μ ^ p` are the same.  -/
IsPrimitiveRoot.minpoly_eq_pow : ∀ {n : ℕ} {K : Type u_1} [inst : CommRing K] {μ : K},
  IsPrimitiveRoot μ n →
    ∀ [IsDomain K] [CharZero K] {p : ℕ} [hprime : Fact (Nat.Prime p)], ¬p ∣ n → minpoly ℤ μ = minpoly ℤ (μ ^ p)
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.mk₀_bijective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (X Y : C), Function.Bijective CategoryTheory.Abelian.Ext.mk₀
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.IsVonNBounded.restrict_scalars_of_nontrivial : ∀ (𝕜 : Type u_1) {𝕜' : Type u_2} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : NormedRing 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] [Nontrivial 𝕜'] [inst_4 : Zero E] [inst_5 : TopologicalSpace E] [inst_6 : SMul 𝕜 E]
  [inst_7 : MulAction 𝕜' E] [IsScalarTower 𝕜 𝕜' E] {s : Set E},
  Bornology.IsVonNBounded 𝕜' s → Bornology.IsVonNBounded 𝕜 s
-- Lean.Meta.SynthInstance
/-- Target type does not have metavariables.
We use the type to construct the cache key even if the class has output parameters.
Reason: we want to avoid the normalization step in this case.
 -/
_private.Lean.Meta.SynthInstance.0.Lean.Meta.PreprocessKind.noMVars : Lean.Meta.PreprocessKind✝
-- Mathlib.Algebra.Category.Ring.Basic
SemiRingCat.instConcreteCategoryRingHomCarrier : CategoryTheory.ConcreteCategory SemiRingCat fun R S => ↑R →+* ↑S
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.densityProcess.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] (κ κ_1 : ProbabilityTheory.Kernel α (γ × β)),
  κ = κ_1 →
    ∀ (ν ν_1 : ProbabilityTheory.Kernel α γ),
      ν = ν_1 →
        ∀ (n n_1 : ℕ),
          n = n_1 →
            ∀ (a a_1 : α),
              a = a_1 →
                ∀ (x x_1 : γ),
                  x = x_1 →
                    ∀ (s s_1 : Set β), s = s_1 → κ.densityProcess ν n a x s = κ_1.densityProcess ν_1 n_1 a_1 x_1 s_1
-- Mathlib.Algebra.Lie.Solvable
/-- A generalisation of the derived series of a Lie algebra, whose zeroth term is a specified ideal.

It can be more convenient to work with this generalisation when considering the derived series of
an ideal since it provides a type-theoretic expression of the fact that the terms of the ideal's
derived series are also ideals of the enclosing algebra.

See also `LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_comap` and
`LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_map` below.  -/
LieAlgebra.derivedSeriesOfIdeal : (R : Type u) →
  (L : Type v) →
    [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → ℕ → LieIdeal R L → LieIdeal R L
-- Mathlib.Topology.Algebra.PontryaginDual
PontryaginDual.map_mul : ∀ {A : Type u_1} {G : Type u_4} [inst : Monoid A] [inst_1 : CommGroup G] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] (f g : A →ₜ* G),
  PontryaginDual.map (f * g) = PontryaginDual.map f * PontryaginDual.map g
-- Mathlib.Order.Hom.Lattice
SupHom.instTop.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : SemilatticeSup β] [inst_2 : Top β],
  SupHom.instTop = { top := SupHom.const α ⊤ }
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.extend.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) (I : ModelWithCorners 𝕜 E H), f.extend I = f.trans I.toPartialEquiv
-- Mathlib.Data.Multiset.ZeroCons
Multiset.card_eq_card_of_rel : ∀ {α : Type u_1} {β : Type v} {r : α → β → Prop} {s : Multiset α} {t : Multiset β}, Multiset.Rel r s t → s.card = t.card
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.range_familyOfBFamily : ∀ {α : Type u_1} {o : Ordinal.{u_3}} (f : (a : Ordinal.{u_3}) → a < o → α), Set.range (o.familyOfBFamily f) = o.brange f
-- Init.Data.Array.Basic
/-- Removes the first `i` elements of `xs`. If `xs` has fewer than `i` elements, the new array is empty.

The returned array is always a new array, even if it contains the same elements as the input array.

Examples:
* `#["red", "green", "blue"].drop 1 = #["green", "blue"]`
* `#["red", "green", "blue"].drop 2 = #["blue"]`
* `#["red", "green", "blue"].drop 5 = #[]`
 -/
Array.drop : {α : Type u} → Array α → ℕ → Array α
-- Mathlib.GroupTheory.GroupAction.Primitive
/-- If the action is not trivial, then the trivial blocks condition implies preprimitivity
(pretransitivity is automatic)  -/
MulAction.IsPreprimitive.mk' : ∀ {G : Type u_1} {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X],
  MulAction.fixedPoints G X ≠ ⊤ →
    (∀ {B : Set X}, MulAction.IsBlock G B → MulAction.IsTrivialBlock B) → MulAction.IsPreprimitive G X
-- Init.Data.Array.Lemmas
Array.any_append : ∀ {α : Type u_1} {f : α → Bool} {xs ys : Array α}, (xs ++ ys).any f = (xs.any f || ys.any f)
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
QuadraticModuleCat.forget₂_map_associator_hom : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Invertible 2] (X Y Z : QuadraticModuleCat R),
  (CategoryTheory.forget₂ (QuadraticModuleCat R) (ModuleCat R)).map
      (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom =
    (CategoryTheory.MonoidalCategoryStruct.associator X.toModuleCat Y.toModuleCat Z.toModuleCat).hom
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
/-- The functor used to establish the equivalence `grothendieckPrecompFunctorEquivalence` between
the Grothendieck construction on `CostructuredArrow.functor` and the comma category.  -/
CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (L : CategoryTheory.Functor C D) →
              (R : CategoryTheory.Functor E D) →
                CategoryTheory.Functor
                  (CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L)))
                  (CategoryTheory.Comma L R)
-- Batteries.Data.DList.Basic
Batteries.DList.mk.injEq : ∀ {α : Type u} (apply : List α → List α) (invariant : ∀ (l : List α), apply l = apply [] ++ l)
  (apply_1 : List α → List α) (invariant_1 : ∀ (l : List α), apply_1 l = apply_1 [] ++ l),
  ({ apply := apply, invariant := invariant } = { apply := apply_1, invariant := invariant_1 }) = (apply = apply_1)
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.intValuation_uniformizer : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  (π : v.intValuation.Uniformizer), v.intValuation ↑π.val = WithZero.exp (-1)
-- Batteries.Tactic.Lint.Frontend
/-- Formats the linter results as Lean code with comments and `#check` commands.
 -/
Batteries.Tactic.Lint.formatLinterResults : Array (Batteries.Tactic.Lint.NamedLinter × Std.HashMap Lean.Name Lean.MessageData) →
  Array Lean.Name →
    Bool → String → Bool → Batteries.Tactic.Lint.LintVerbosity → ℕ → optParam Bool false → Lean.CoreM Lean.MessageData
-- Batteries.Data.UInt
UInt8.toNat_min : ∀ (x y : UInt8), (x ⊓ y).toNat = min x.toNat y.toNat
-- Mathlib.Order.Grade
Flag.grade_coe : ∀ {𝕆 : Type u_1} {α : Type u_3} [inst : PartialOrder α] {s : Flag α} [inst_1 : Preorder 𝕆] [inst_2 : GradeOrder 𝕆 α]
  (a : ↥s), grade 𝕆 ↑a = grade 𝕆 a
-- Mathlib.Topology.Basic
Set.Finite.isClosed_biUnion : ∀ {X : Type u} {α : Type u_1} [inst : TopologicalSpace X] {s : Set α} {f : α → Set X},
  s.Finite → (∀ i ∈ s, IsClosed (f i)) → IsClosed (⋃ i ∈ s, f i)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.restoreM_OptionT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α : Type u}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.except PUnit.{u + 1} ps)} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  (x : m (Option α)),
  ⦃(Std.Do.wp x).apply (fun e => Option.casesOn e (Q.2.1 PUnit.unit) Q.1, Q.2.2)⦄ MonadControl.restoreM x ⦃Q⦄
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Expr.add.sizeOf_spec : ∀ (a b : Nat.Internal.SOM.Expr), sizeOf (a.add b) = 1 + sizeOf a + sizeOf b
-- Init.Data.Nat.Lemmas
Nat.le_and_le_add_one_iff : ∀ {n m : ℕ}, n ≤ m ∧ m ≤ n + 1 ↔ m = n ∨ m = n + 1
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- `0` in the localization, defined as `0 /ₒ 1`.  -/
OreLocalization.zero : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] → {X : Type u_2} → [Zero X] → [inst_3 : MulAction R X] → OreLocalization S X
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.coe_id : ∀ (α : Type u_1) [inst : TopologicalSpace α], ⇑(ContinuousMap.id α) = id
-- Mathlib.Data.Fintype.Card
Fin.val_eq_val_of_heq : ∀ {k l : ℕ} {i : Fin k} {j : Fin l}, i ≍ j → ↑i = ↑j
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.map_rel : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (W : ℤ → R) {F : Type u_3}
  [inst_2 : FunLike F R S] [RingHomClass F R S] (f : F) (p q r s : ℤ),
  f (IsEllipticNet.rel W p q r s) = IsEllipticNet.rel (⇑f ∘ W) p q r s
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.indicator₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [inst_1 : Zero β],
  MeasureTheory.AEStronglyMeasurable f μ →
    ∀ {s : Set α}, MeasureTheory.NullMeasurableSet s μ → MeasureTheory.AEStronglyMeasurable (s.indicator f) μ
-- Init.Data.String.Basic
String.Slice.toByteArray_str_eq : ∀ {s : String.Slice},
  s.str.toByteArray =
    s.str.toByteArray.extract 0 s.startInclusive.offset.byteIdx ++ s.copy.toByteArray ++
      s.str.toByteArray.extract s.endExclusive.offset.byteIdx s.str.toByteArray.size
-- Mathlib.Algebra.Order.Floor.Ring
Mathlib.Meta.Positivity.int_floor_nonneg_of_pos : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] {a : α}, 0 < a → 0 ≤ ⌊a⌋
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.withDensity_smul' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (r : ENNReal) (f : α → ENNReal),
  r ≠ ⊤ → μ.withDensity (r • f) = r • μ.withDensity f
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.ofInvolutive_apply : ∀ {α : Type u_1} [inst : MeasurableSpace α] (f : α → α) (hf : Function.Involutive f) (hf' : Measurable f) (a : α),
  (MeasurableEquiv.ofInvolutive f hf hf') a = f a
-- Mathlib.ModelTheory.Encoding
/-- Applies `imp` to two elements of `(Σ n, L.BoundedFormula α n)`,
or returns `default` if not possible.  -/
FirstOrder.Language.BoundedFormula.sigmaImp : {L : FirstOrder.Language} →
  {α : Type u'} → (n : ℕ) × L.BoundedFormula α n → (n : ℕ) × L.BoundedFormula α n → (n : ℕ) × L.BoundedFormula α n
-- Init.Data.List.Scan.Lemmas
List.scanl_map : ∀ {β : Type u_1} {γ : Type u_2} {α : Type u_3} {init : β} {f : β → γ → β} {g : α → γ} {as : List α},
  List.scanl f init (List.map g as) = List.scanl (fun acc x => f acc (g x)) init as
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.rotate.congr_simp : ∀ {V : Type u} {G : SimpleGraph V} {v : V} [inst : DecidableEq V] (c c_1 : G.Walk v v) (e_c : c = c_1) (u : V)
  (h : u ∈ c.support), c.rotate u h = c_1.rotate u ⋯
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Relations.realize_reflexive : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {r : L.Relations 2},
  M ⊨ r.reflexive ↔ Std.Refl fun x y => FirstOrder.Language.Structure.RelMap r ![x, y]
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.CompStruct.map_simplex : ∀ {X Y : SSet} {x₀ x₁ x₂ : X.obj (Opposite.op { len := 0 })} {e₀₁ : SSet.Edge x₀ x₁} {e₁₂ : SSet.Edge x₁ x₂}
  {e₀₂ : SSet.Edge x₀ x₂} (h : e₀₁.CompStruct e₁₂ e₀₂) (f : X ⟶ Y),
  (h.map f).simplex = (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := 2 }))) h.simplex
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.aeval_prod : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] [inst_2 : Algebra R S₁]
  (f : σ → S₁) {ι : Type u_2} (s : Finset ι) (φ : ι → MvPolynomial σ R),
  (MvPolynomial.aeval f) (∏ i ∈ s, φ i) = ∏ i ∈ s, (MvPolynomial.aeval f) (φ i)
-- Mathlib.Algebra.Group.Nat.Defs
Nat.instAddMonoid : AddMonoid ℕ
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.sub.injEq : ∀ (a b a_1 b_1 : Lean.Grind.CommRing.Expr), (a.sub b = a_1.sub b_1) = (a = a_1 ∧ b = b_1)
-- Mathlib.CategoryTheory.Limits.FullSubcategory
/-- The essential image of a functor is closed under the limits it preserves.  -/
CategoryTheory.Limits.instIsClosedUnderLimitsOfShapeEssImageOfHasLimitsOfShapeOfPreservesLimitsOfShapeOfFullOfFaithful : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {C : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.PreservesLimitsOfShape J F] [F.Full] [F.Faithful],
  F.essImage.IsClosedUnderLimitsOfShape J
-- Mathlib.Algebra.Group.Basic
mul_pow : ∀ {M : Type u_4} [inst : CommMonoid M] (a b : M) (n : ℕ), (a * b) ^ n = a ^ n * b ^ n
-- Mathlib.FieldTheory.Relrank
IntermediateField.inf_relfinrank_left : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A B : IntermediateField F E),
  (A ⊓ B).relfinrank A = B.relfinrank A
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inrX_desc_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G K : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (α : G ⟶ K) (hα : Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0) (i : ι),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ i)
      ((HomologicalComplex.homotopyCofiber.desc φ α hα).f i) =
    α.f i