mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Basic
Lean.Meta.ExprParamInfo.mk.inj : ∀ {name : Lean.Name} {type : Lean.Expr} {binderInfo : Lean.BinderInfo} {name_1 : Lean.Name} {type_1 : Lean.Expr}
  {binderInfo_1 : Lean.BinderInfo},
  { name := name, type := type, binderInfo := binderInfo } =
      { name := name_1, type := type_1, binderInfo := binderInfo_1 } →
    name = name_1 ∧ type = type_1 ∧ binderInfo = binderInfo_1
-- Init.Data.Function
/-- A function `f : α → β` is called surjective if every `b : β` is equal to `f a`
for some `a : α`.  -/
Function.Surjective : {α : Sort u_1} → {β : Sort u_2} → (α → β) → Prop
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.String.toBitVec_getElem_utf8EncodeChar_one_of_utf8Size_eq_three : ∀ {c : Char} (h : c.utf8Size = 3), (String.utf8EncodeChar c)[1].toBitVec = 2#2 ++ BitVec.extractLsb' 6 6 c.val.toBitVec
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes right covariance.
The lemma assuming left covariance is `Left.mul_lt_one'`.  -/
Right.mul_lt_one' : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulRightMono α] {a b : α}, a < 1 → b < 1 → a * b < 1
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
/-- **Alias** of `FunLike.coe_smul`. -/
SlashInvariantForm.coe_smul : ∀ {M : Type u_1} {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : SMul M F]
  [inst_2 : SMul M β] [IsSMulApply M F α β] (n : M) (f : F), ⇑(n • f) = n • ⇑f
-- Std.Data.HashMap.Raw
/-- Inserts multiple keys with the value `()` into the hash map by iterating over the given collection
and calling `insertIfNew`. If the same key appears multiple times, the first occurrence takes
precedence.

This is mainly useful to implement `HashSet.insertMany`, so if you are considering using this,
`HashSet` or `HashSet.Raw` might be a better fit for you.
 -/
Std.HashMap.Raw.insertManyIfNewUnit : {α : Type u} →
  [BEq α] → [Hashable α] → {ρ : Type w} → [ForIn Id ρ α] → Std.HashMap.Raw α Unit → ρ → Std.HashMap.Raw α Unit
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.braiding_naturality_right_assoc : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.BraidedCategory C] (X : C) {Y Z : C} (f : Y ⟶ Z) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Z X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f)
      (CategoryTheory.CategoryStruct.comp (β_ X Z).hom h) =
    CategoryTheory.CategoryStruct.comp (β_ X Y).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X) h)
-- Mathlib.Data.Part
Part.sub_def : ∀ {α : Type u_1} [inst : Sub α] (a b : Part α),
  a - b = do
    let y ← a
    Part.map (fun x => y - x) b
-- Mathlib.Order.Filter.AtTopBot.Tendsto
Filter.Tendsto.eventually_gt_atTop : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder β] [NoTopOrder β] {f : α → β} {l : Filter α},
  Filter.Tendsto f l Filter.atTop → ∀ (c : β), ∀ᶠ (x : α) in l, c < f x
-- Mathlib.Analysis.SpecialFunctions.Arsinh
/-- The function `Real.arsinh` is real analytic.  -/
Real.analyticAt_arsinh : ∀ {x : ℝ}, AnalyticAt ℝ Real.arsinh x
-- Mathlib.AlgebraicTopology.SimplexCategory.Truncated
/-- Abbreviation for face maps in the 2-truncated simplex category.  -/
SimplexCategory.Truncated.δ₂ : {n : ℕ} →
  Fin (n + 2) →
    (hn : autoParam ({ len := n }.len ≤ 2) SimplexCategory.Truncated.δ₂._auto_1) →
      (hn' : autoParam ({ len := n + 1 }.len ≤ 2) SimplexCategory.Truncated.δ₂._auto_3) →
        { obj := { len := n }, property := hn } ⟶ { obj := { len := n + 1 }, property := hn' }
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.count_eq_zero_of_ne : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α]
  [inst_2 : DecidableEq (Associates α)] [inst_3 : (p : Associates α) → Decidable (Irreducible p)] {p q : Associates α},
  Irreducible p → Irreducible q → p ≠ q → p.count q.factors = 0
-- Mathlib.Analysis.PSeries
/-- Test for convergence of the `p`-series: the real-valued series `∑' n : ℕ, 1 / n ^ p` converges
if and only if `1 < p`.  -/
Real.summable_one_div_nat_rpow : ∀ {p : ℝ}, (Summable fun n => 1 / ↑n ^ p) ↔ 1 < p
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.NormalizePattern.PatternArgKind : Type
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.mk : {R : Type u} →
  {S : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring S] →
        [inst_2 : Algebra R S] → {f : Polynomial R} → IsAdjoinRoot S f → f.Monic → IsAdjoinRootMonic S f
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
/-- Left-right `wrap` cancellation theorem of the form
```
toInt a = i.wrap a' → toInt b = i.wrap b' → toInt (a ⊞ b) = i.wrap (a' ⊞ b')
```
 -/
Lean.Meta.Grind.Arith.Cutsat.ToIntThms.c_ww? : Lean.Meta.Grind.Arith.Cutsat.ToIntThms → Option Lean.Expr
-- Mathlib.Data.Set.NAry
Set.image2_inter_subset_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s s' : Set α} {t : Set β},
  Set.image2 f (s ∩ s') t ⊆ Set.image2 f s t ∩ Set.image2 f s' t
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.IsIso.instMonoidalOppositeMop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f],
  CategoryTheory.IsIso f.mop
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
ComplexShape.Embedding.liftExtend.f.eq_1 : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {e : c.Embedding c'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {K : HomologicalComplex C c'} {L : HomologicalComplex C c}
  [inst_3 : e.IsRelIff] (φ : K.restriction e ⟶ L) (i' : ι'),
  ComplexShape.Embedding.liftExtend.f φ i' =
    if hi' : ∃ i, e.f i = i' then
      CategoryTheory.CategoryStruct.comp (K.restrictionXIso e ⋯).inv
        (CategoryTheory.CategoryStruct.comp (φ.f hi'.choose) (L.extendXIso e ⋯).inv)
    else 0
-- Mathlib.Order.Defs.Unbundled
asymm_of : ∀ {α : Sort u_1} (r : α → α → Prop) {a b : α} [Std.Asymm r], r a b → ¬r b a
-- Init.Data.Option.Lemmas
Option.guard_or_guard : ∀ {α : Type u_1} {p : α → Bool} {a : α} {q : α → Bool},
  (Option.guard p a).or (Option.guard q a) = Option.guard (fun x => p x || q x) a
-- Init.Data.Int.Gcd
Int.gcd_zero_right : ∀ (a : ℤ), a.gcd 0 = a.natAbs
-- Mathlib.Data.Fin.Tuple.Basic
Fin.repeat_succ : ∀ {n : ℕ} {α : Sort u_1} (a : Fin n → α) (m : ℕ), Fin.repeat m.succ a = Fin.append a (Fin.repeat m a) ∘ Fin.cast ⋯
-- Lean.Level
Lean.Level.getParamSubst : List Lean.Name → List Lean.Level → Lean.Name → Option Lean.Level
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.instModule : {Γ : Type u_1} →
  {R : Type u_3} →
    {V : Type u_6} →
      [inst : PartialOrder Γ] →
        [inst_1 : Semiring R] → [inst_2 : AddCommMonoid V] → [Module R V] → Module R (HahnSeries Γ V)
-- Mathlib.Topology.Separation.CompletelyRegular
t35Space_iff_isEmbedding_stoneCechUnit : ∀ {X : Type u} [inst : TopologicalSpace X], T35Space X ↔ Topology.IsEmbedding stoneCechUnit
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.le_of_eqLocus_ge : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] {f g : E →ₛₗ.[σ] F},
  f.domain ≤ f.eqLocus g → f ≤ g
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.adj_toSubgraph_iff_mem_edges : ∀ {V : Type u} {G : SimpleGraph V} {u v u' v' : V} {p : G.Walk u v}, p.toSubgraph.Adj u' v' ↔ s(u', v') ∈ p.edges
-- Std.Async.UDP
_private.Std.Async.UDP.0.Std.Async.UDP.Socket.ofNative : Std.Internal.UV.UDP.Socket → Std.Async.UDP.Socket
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- The property that a morphism property `W` is stable under limits
indexed by a category `J`.  -/
CategoryTheory.MorphismProperty.IsStableUnderLimitsOfShape : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.MorphismProperty C → (J : Type u_1) → [CategoryTheory.Category.{v_1, u_1} J] → Prop
-- Lean.Meta.Tactic.SplitIf
/-- Checks whether `e` is a candidate for `split`.
Returns `some e'` if a prefix is a candidate.
Example: suppose `e` is `(if b then f else g) x`, then
the result is `some e'` where `e'` is the subterm `(if b then f else g)`
 -/
_private.Lean.Meta.Tactic.SplitIf.0.Lean.Meta.FindSplitImpl.isCandidate? : Lean.Environment → Lean.Meta.FindSplitImpl.Context → Lean.Expr → Option Lean.Expr
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.r_trans : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] {a b c : α × α},
  Lean.Grind.IntModule.OfNatModule.r α a b →
    Lean.Grind.IntModule.OfNatModule.r α b c → Lean.Grind.IntModule.OfNatModule.r α a c
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.deleteEdges_inter_edgeSet_left_eq : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (s : Set (Sym2 V)),
  G'.deleteEdges (G'.edgeSet ∩ s) = G'.deleteEdges s
-- Mathlib.Lean.Expr.Basic
/-- Counts the immediate depth of a nested `let` expression.  -/
Lean.Expr.letDepth : Lean.Expr → ℕ
-- Mathlib.Order.Heyting.Basic
Function.Injective.heytingAlgebra.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Min α] [inst_2 : LE α] [inst_3 : LT α] [inst_4 : Top α]
  [inst_5 : Bot α] [inst_6 : Compl α] [inst_7 : HImp α] [inst_8 : HeytingAlgebra β] (f : α → β)
  (hf : Function.Injective f) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y)
  (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_top : f ⊤ = ⊤)
  (map_bot : f ⊥ = ⊥) (map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ) (map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b),
  Function.Injective.heytingAlgebra f hf le lt map_sup map_inf map_top map_bot map_compl map_himp =
    {
      toGeneralizedHeytingAlgebra :=
        Function.Injective.generalizedHeytingAlgebra f hf ⋯ ⋯ map_sup map_inf map_top map_himp,
      toBot := inst_5, bot_le := ⋯, toCompl := inst_6, himp_bot := ⋯ }
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.OrderIso.toCompleteLatticeHom_toFun : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : α ≃o β) (a : α),
  (CompleteLatticeHom.OrderIso.toCompleteLatticeHom f) a = f a
-- Mathlib.Data.Tree.Basic
BinaryTree.nil : {α : Type u} → BinaryTree α
-- Init.Data.Array.Lemmas
Array.map_eq_push_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} {ys : Array β} {b : β},
  Array.map f xs = ys.push b ↔ ∃ zs a, xs = zs.push a ∧ Array.map f zs = ys ∧ f a = b
-- Mathlib.LinearAlgebra.Projection
LinearMap.ofIsComplProd.congr_simp : ∀ {E : Type u_2} [inst : AddCommGroup E] {F : Type u_3} [inst_1 : AddCommGroup F] {R₁ : Type u_7} [inst_2 : CommRing R₁]
  [inst_3 : Module R₁ E] [inst_4 : Module R₁ F] {p q : Submodule R₁ E} (h : IsCompl p q),
  LinearMap.ofIsComplProd h = LinearMap.ofIsComplProd h
-- Mathlib.Combinatorics.Hindman
/-- Addition of ultrafilters given by `∀ᶠ m in U+V, p m ↔ ∀ᶠ m in U, ∀ᶠ m' in V, p (m+m')`.  -/
Ultrafilter.add : {M : Type u_1} → [Add M] → Add (Ultrafilter M)
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
le_tsub_iff_le_tsub : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α], a ≤ b → c ≤ b → (a ≤ b - c ↔ c ≤ b - a)
-- Mathlib.LinearAlgebra.Dimension.Constructions
Module.Basis.sumQuot_repr_left : ∀ {R : Type u_2} {V : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {W : Submodule R V}
  {m : Type u_4} {n : Type u_5} (bW : Module.Basis m R ↥W) (bQ : Module.Basis n R (V ⧸ W)) (i : m),
  (bW.sumQuot bQ).repr ↑(bW i) = fun₀ | Sum.inl i => 1
-- Mathlib.FieldTheory.IsPerfectClosure
/-- If `i : K →+* L` is `p`-radical, then for any perfect ring `M` of exponential characteristic
`p`, the map `(L →+* M) → (K →+* M)` induced by `i` is injective.
A special case of `IsPRadical.injective_comp_of_pNilradical_eq_bot`.  -/
IsPRadical.injective_comp_of_perfect : ∀ {K : Type u_1} {L : Type u_2} (M : Type u_3) [inst : CommRing K] [inst_1 : CommRing L] [inst_2 : CommRing M]
  (i : K →+* L) (p : ℕ) [ExpChar M p] [IsPRadical i p] [PerfectRing M p], Function.Injective fun f => f.comp i
-- Mathlib.Order.Hom.WithTopBot
SupHom.withBot.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] (f : SupHom α β),
  f.withBot = { toFun := WithBot.map ⇑f, map_sup' := ⋯, map_bot' := ⋯ }
-- Mathlib.Order.Filter.Bases.Basic
FilterBasis.generate : ∀ {α : Type u_1} (B : FilterBasis α), Filter.generate B.sets = B.filter
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Poly.mulMon : Nat.Internal.SOM.Poly → ℕ → Nat.Internal.SOM.Mon → Nat.Internal.SOM.Poly
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.norm_int_le_pow_iff_dvd : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (k : ℤ) (n : ℕ), ‖↑k‖ ≤ ↑p ^ (-↑n) ↔ ↑p ^ n ∣ k
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
/-- The function `Real.sin` is real analytic.  -/
Real.analyticWithinAt_sin : ∀ {x : ℝ} {s : Set ℝ}, AnalyticWithinAt ℝ Real.sin s x
-- Mathlib.Analysis.Convex.Side
AffineSubspace.wOppSide_self_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x : P}, s.WOppSide x x ↔ x ∈ s
-- Mathlib.Topology.Order.LocalExtr
isLocalMinOn_univ_iff : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {a : α},
  IsLocalMinOn f Set.univ a ↔ IsLocalMin f a
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.toList_toArray : ∀ {α : Type u} {r : Std.Ric α} [inst : Std.PRange.Least? α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α], r.toArray.toList = r.toList
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.isFiniteMeasureRestrict : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : Set α)
  [h : MeasureTheory.IsFiniteMeasure μ], MeasureTheory.IsFiniteMeasure (μ.restrict s)
-- Std.Data.Iterators.Lemmas.Producers.Monadic.List
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.List.0.Std.Iterators.Types.ListIterator.instIterator.match_1.eq_3 : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} (motive : Std.IterStep (Std.IterM m α) α → Sort u_3)
  (h_1 : (it' : Std.IterM m α) → (out : α) → motive (Std.IterStep.yield it' out))
  (h_2 : (it : Std.IterM m α) → motive (Std.IterStep.skip it)) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it => h_2 it
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.GroupTheory.DoubleCoset
/-- Create a double coset out of an element of `H \ G / K`  -/
DoubleCoset.quotToDoubleCoset : {G : Type u_1} → [inst : Group G] → (H K : Subgroup G) → DoubleCoset.Quotient ↑H ↑K → Set G
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.Hom.comp_val : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P : Algebra.Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [inst_3 : CommRing R']
  [inst_4 : CommRing S'] [inst_5 : Algebra R' S'] {P' : Algebra.Generators R' S' ι'} {R'' : Type u_4} {S'' : Type u_5}
  {ι'' : Type u_6} [inst_6 : CommRing R''] [inst_7 : CommRing S''] [inst_8 : Algebra R'' S'']
  {P'' : Algebra.Generators R'' S'' ι''} [inst_9 : Algebra R' R''] [inst_10 : Algebra R' S''] [inst_11 : Algebra S S']
  [inst_12 : Algebra S' S''] [inst_13 : Algebra S S''] [inst_14 : IsScalarTower R' R'' S'']
  [inst_15 : IsScalarTower R' S' S''] [inst_16 : IsScalarTower S S' S''] (f : P'.Hom P'') (g : P.Hom P') (x : ι),
  (f.comp g).val x = (MvPolynomial.aeval f.val) (g.val x)
-- Mathlib.Algebra.Polynomial.Eval.Degree
Polynomial.eval₂_comp : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p q : Polynomial R} [inst_1 : CommSemiring S] (f : R →+* S) {x : S},
  Polynomial.eval₂ f x (p.comp q) = Polynomial.eval₂ f (Polynomial.eval₂ f x q) p
-- Lean.Meta.Tactic.Simp.SimpCongrTheorems
Lean.Meta.mkSimpCongrTheorem : Lean.Name → ℕ → Lean.MetaM Lean.Meta.SimpCongrTheorem
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
skewAdjointMatricesSubmodule.eq_1 : ∀ {R : Type u_1} {n : Type u_11} [inst : CommRing R] [inst_1 : Fintype n] (J : Matrix n n R) [inst_2 : DecidableEq n],
  skewAdjointMatricesSubmodule J = pairSelfAdjointMatricesSubmodule (-J) J
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycle.exists_zpow_eq : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.IsCycle → f x ≠ x → f y ≠ y → ∃ i, (f ^ i) x = y
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
/-- If `X` is a simplicial object and `n + i = m`, this is the morphism
`X _⦋n⦌ ⟶ X _⦋m⦌` obtained by iterating `i` times the degeneracy map `X.σ 0`.  -/
CategoryTheory.SimplicialObject.σ₀Iter : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (X : CategoryTheory.SimplicialObject C) →
      {n m : ℕ} →
        (i : ℕ) →
          autoParam (n + i = m) CategoryTheory.SimplicialObject.σ₀Iter._auto_1 →
            (X.obj (Opposite.op { len := n }) ⟶ X.obj (Opposite.op { len := m }))
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
/-- There is a noncomputable embedding of `α`-colorings to `β`-colorings if
`β` has at least as large a cardinality as `α`.  -/
SimpleGraph.recolorOfCardLE : {V : Type u} →
  (G : SimpleGraph V) →
    {α : Type u_4} →
      {β : Type u_5} →
        [inst : Fintype α] → [inst_1 : Fintype β] → Fintype.card α ≤ Fintype.card β → G.Coloring α ↪ G.Coloring β
-- Mathlib.Analysis.Calculus.FDeriv.Defs
HasFDerivAtFilter.isLittleOTVS : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {L : Filter (E × E)},
  HasFDerivAtFilter f f' L → (fun p => f p.1 - f p.2 - f' (p.1 - p.2)) =o[𝕜; L] fun p => p.1 - p.2
-- Mathlib.Analysis.Normed.Module.MStructure
IsLprojection.coe_one : ∀ {X : Type u_1} [inst : NormedAddCommGroup X] {M : Type u_2} [inst_1 : Ring M] [inst_2 : Module M X], ↑1 = 1
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthInf_comp_nonneg : ∀ {u : ℕ → ENNReal} {v : ℕ → ℕ},
  Monotone u → u ≠ 0 → Filter.Tendsto v Filter.atTop Filter.atTop → 0 ≤ ExpGrowth.expGrowthInf (u ∘ v)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_alter_of_beq_eq_false : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k k' : α}
  {f : Option (β k) → Option (β k)}, (k == k') = false → (k' ∈ m.alter k f ↔ k' ∈ m)
-- Mathlib.Algebra.Polynomial.Degree.Units
Polynomial.not_isUnit_of_degree_pos : ∀ {R : Type u} [inst : Semiring R] [NoZeroDivisors R] (p : Polynomial R), 0 < p.degree → ¬IsUnit p
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_le_toNNReal_iff' : ∀ {r p : ℝ}, r.toNNReal ≤ p.toNNReal ↔ r ≤ p ∨ r ≤ 0
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.toList_filterMapWithPostcondition_filterMapWithPostcondition : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {m : Type w → Type w'} {n : Type w → Type w''}
  {δ : Type w} [inst_1 : Monad m] [LawfulMonad m] [inst_3 : Monad n] [LawfulMonad n] [inst_5 : MonadLiftT m n]
  [LawfulMonadLiftT m n] [Std.Iterators.Finite α Id] {f : β → Std.Iterators.PostconditionT m (Option γ)}
  {g : γ → Std.Iterators.PostconditionT n (Option δ)},
  (Std.IterM.filterMapWithPostcondition g (Std.Iter.filterMapWithPostcondition f it)).toList =
    (Std.Iter.filterMapWithPostcondition
        (fun b => do
          let __do_lift ← liftM (f b)
          match __do_lift with
            | none => pure none
            | some fb => g fb)
        it).toList
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.insertMany!_eq_foldl : ∀ {α : Type u} {β : Type v} {x : Ord α} {l : List (α × β)} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  ↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l) =
    List.foldl
      (fun acc x_1 =>
        match x_1 with
        | (k, v) => Std.DTreeMap.Internal.Impl.insert! k v acc)
      t l
-- Lean.EnvExtension
Lean.MapDeclarationExtension.insert : {α : Type} → Lean.MapDeclarationExtension α → Lean.Environment → Lean.Name → α → Lean.Environment
-- Mathlib.RingTheory.Ideal.Quotient.PowTransition
Submodule.factorPow_comp_powSMulQuotInclusion : ∀ {R : Type u_3} [inst : CommRing R] (I : Ideal R) {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {a b c d e : ℕ} (h : c = b + a) (h' : e = d + c),
  Submodule.factorPow I M ⋯ ∘ₗ Submodule.powSMulQuotInclusion I M ⋯ ⊤ =
    Submodule.powSMulQuotInclusion I M h ⊤ ∘ₗ Submodule.factorPow I ↥(I ^ a • ⊤) ⋯
-- Mathlib.LinearAlgebra.BilinearForm.Basic
LinearMap.BilinForm.zero_left : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M} (x : M), (B 0) x = 0
-- Init.Data.Ord.Basic
Ordering.isLE_iff_ne_gt : ∀ {o : Ordering}, o.isLE = true ↔ ¬o = Ordering.gt
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
/-- `one` is Sorted.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.one_sorted : ∀ {basis : Tactic.ComputeAsymptotics.Basis}, Tactic.ComputeAsymptotics.MultiseriesExpansion.one.Sorted
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.isIso₂_truncGE_map_of_isLE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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) [CategoryTheory.IsTriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ (n₀ n₁ : ℤ), n₀ + 1 = n₁ → t.IsLE T.obj₁ n₀ → CategoryTheory.IsIso ((t.truncGE n₁).map T.mor₂)
-- Mathlib.Data.Fintype.Quotient
/-- Choice-free induction principle for quotients indexed by a finite type.
See `Quotient.induction_on_pi` for the general version assuming `Classical.choice`.  -/
Quotient.ind_fintype_pi : ∀ {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ι → Sort u_2} {S : (i : ι) → Setoid (α i)}
  {C : ((i : ι) → Quotient (S i)) → Prop},
  (∀ (a : (i : ι) → α i), C fun x => ⟦a x⟧) → ∀ (q : (i : ι) → Quotient (S i)), C q
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.ne_bot_iff : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β}, G ≠ ⊥ ↔ G.vertexSet.Nonempty
-- Mathlib.Data.NNRat.Defs
NNRat.coe_lt_coe : ∀ {p q : ℚ≥0}, ↑p < ↑q ↔ p < q
-- Mathlib.Data.Fintype.Basic
Fin.univ_image_getElem' : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (l : List α) (f : α → β),
  Finset.image (fun i => f l[↑i]) Finset.univ = (List.map f l).toFinset
-- Init.Data.UInt.Lemmas
UInt8.ofNatClamp_toNat : ∀ (n : UInt8), UInt8.ofNatClamp n.toNat = n
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- If a submodule is contained in a finite-dimensional
submodule with the same dimension, they are equal.  -/
Submodule.eq_of_le_of_finrank_eq : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {S₁ S₂ : Submodule K V} [FiniteDimensional K ↥S₂], S₁ ≤ S₂ → Module.finrank K ↥S₁ = Module.finrank K ↥S₂ → S₁ = S₂
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.fibration_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C],
  HomotopicalAlgebra.Fibration f ↔ HomotopicalAlgebra.fibrations C f
-- Mathlib.Data.Finset.Powerset
Finset.powersetCard_eq_empty : ∀ {α : Type u_1} {n : ℕ} {s : Finset α}, Finset.powersetCard n s = ∅ ↔ s.card < n
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.not_isSuccLimit_zero : ¬Order.IsSuccLimit 0