mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.InfoTree.Types
Lean.Elab.ChoiceInfo.mk.inj : ∀ {toElabInfo toElabInfo_1 : Lean.Elab.ElabInfo},
  { toElabInfo := toElabInfo } = { toElabInfo := toElabInfo_1 } → toElabInfo = toElabInfo_1
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformFun.dist_def : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace β] [inst_1 : BoundedSpace β] (f g : UniformFun α β),
  dist f g = ⨆ x, dist (UniformFun.toFun f x) (UniformFun.toFun g x)
-- Mathlib.Algebra.Free
FreeSemigroup.lift_symm_apply : ∀ {α : Type u} {β : Type v} [inst : Semigroup β] (f : FreeSemigroup α →ₙ* β) (a : α),
  FreeSemigroup.lift.symm f a = (⇑f ∘ FreeSemigroup.of) a
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.Pairwise_cons_nil : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  {R :
    ℝ × Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl →
      ℝ × Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl → Prop}
  {exp : ℝ} {coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl},
  Stream'.Seq.Pairwise R
    (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil)
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
MDifferentiableOn.cle_arrowCongr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F₁ : Type u_14} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_15} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_16} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {F₄ : Type u_17}
  [inst_12 : NormedAddCommGroup F₄] [inst_13 : NormedSpace 𝕜 F₄] {f : M → F₁ ≃L[𝕜] F₂} {g : M → F₃ ≃L[𝕜] F₄}
  {s : Set M},
  (MDiff[s] fun x => ↑(f x).symm) → (MDiff[s] fun x => ↑(g x)) → MDiff[s] fun y => ↑((f y).arrowCongr (g y))
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- `Res(f, a • g) = a ^ {deg f} * Res(f, g)`.  -/
Polynomial.resultant_C_mul_right : ∀ {R : Type u_1} [inst : CommRing R] (f g : Polynomial R) (m n : ℕ) (r : R),
  f.resultant (Polynomial.C r * g) m n = r ^ m * f.resultant g m n
-- Mathlib.Lean.Expr.Basic
/-- Same as `mkConst`, but with fresh level metavariables.  -/
Lean.mkConst' : Lean.Name → Lean.MetaM Lean.Expr
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.Iter.toList_eq_match_step : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {it : Std.Iter β},
  it.toList =
    match ↑it.step with
    | Std.IterStep.yield it' out => out :: it'.toList
    | Std.IterStep.skip it' => it'.toList
    | Std.IterStep.done => []
-- Init.Data.List.Find
List.idxOf_append : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {l₁ l₂ : List α} {a : α},
  List.idxOf a (l₁ ++ l₂) = if a ∈ l₁ then List.idxOf a l₁ else List.idxOf a l₂ + l₁.length
-- Mathlib.Tactic.Order.Preprocessing
/-- Preprocesses facts for preorders. Replaces `x < y` with two equivalent facts: `x ≤ y` and
`¬ (y ≤ x)`. Replaces `x = y` with `x ≤ y`, `y ≤ x` and removes `x ≠ y`.  -/
Mathlib.Tactic.Order.preprocessFactsPreorder : Array Mathlib.Tactic.Order.AtomicFact → Lean.MetaM (Array Mathlib.Tactic.Order.AtomicFact)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.HasStrongEpiImages.congr_simp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasImages C],
  CategoryTheory.Limits.HasStrongEpiImages C = CategoryTheory.Limits.HasStrongEpiImages C
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.add_mem_iff_left : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] {module_M : Module R M} (p : Submodule R M)
  {x y : M}, y ∈ p → (x + y ∈ p ↔ x ∈ p)
-- Init.Data.Option.Lemmas
Option.eq_some_unique : ∀ {α : Type u_1} {o : Option α} {a b : α}, o = some a → o = some b → a = b
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.mk : {γ : Type} →
  Lean.KeyedDeclsAttribute.Def γ →
    IO.Ref (Lean.KeyedDeclsAttribute.Table γ) → Lean.KeyedDeclsAttribute.Extension γ → Lean.KeyedDeclsAttribute γ
-- Mathlib.Algebra.Homology.Embedding.TruncLE
HomologicalComplex.truncLE'XIso.congr_simp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncLE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  {i : ι} {i' : ι'} (hi' : e.f i = i') (hi : ¬e.BoundaryLE i), K.truncLE'XIso e hi' hi = K.truncLE'XIso e hi' hi
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
RootPairing.Base.cartanMatrix_apply_eq_zero_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : P.IsCrystallographic] [CharZero R] [IsDomain R] [Finite ι] {i j : ↥b.support},
  i ≠ j → (b.cartanMatrix i j = 0 ↔ P.root ↑i + P.root ↑j ∉ Set.range ⇑P.root)
-- Mathlib.InformationTheory.KullbackLeibler.KLFun
/-- `klFun` is strongly measurable.  -/
InformationTheory.stronglyMeasurable_klFun : MeasureTheory.StronglyMeasurable InformationTheory.klFun
-- Std.Data.ExtDTreeMap.Basic
/-- Returns the key-value pair with the `n`-th smallest key, or `none` if `n` is at least `t.size`.  -/
Std.ExtDTreeMap.entryAtIdx? : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → ℕ → Option ((a : α) × β a)
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.all_toList : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {p : β → Bool}, it.toList.all p = Std.Iter.all p it
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_union_coe_submodule : ∀ (R : Type uR) {A : Type uA} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A] (s t : Set A),
  Subalgebra.toSubmodule (Algebra.adjoin R (s ∪ t)) =
    Subalgebra.toSubmodule (Algebra.adjoin R s) * Subalgebra.toSubmodule (Algebra.adjoin R t)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_minKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false}, t.getKey? (t.minKey he) = some (t.minKey he)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- The limit cone for the product over an index type with exactly one term.  -/
CategoryTheory.Limits.limitConeOfUnique : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [Unique β] → (f : β → C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Discrete.functor f)
-- Mathlib.CategoryTheory.Category.Quiv
CategoryTheory.Quiv.inv_map_hom_map_of_iso : ∀ {V W : CategoryTheory.Quiv} (e : V ≅ W) {X Y : ↑V} (f : X ⟶ Y), e.inv.map (e.hom.map f) = Quiver.homOfEq f ⋯ ⋯
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mathlib.Tactic.MonTauto.eq_zero_add : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.AddMonObj M],
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.zero
        (CategoryTheory.CategoryStruct.id M))
      CategoryTheory.AddMonObj.add
-- Mathlib.Tactic.GRewrite.Core
Mathlib.Tactic.GRewrite.GRewriteResult.mk.sizeOf_spec : ∀ (eNew impProof : Lean.Expr) (mvarIds : List Lean.MVarId) (lctx? : Option Lean.LocalContext),
  sizeOf { eNew := eNew, impProof := impProof, mvarIds := mvarIds, lctx? := lctx? } =
    1 + sizeOf eNew + sizeOf impProof + sizeOf mvarIds + sizeOf lctx?
-- Mathlib.Analysis.Normed.Module.Basic
/-- Produces a `SeminormedAddCommGroup E` instance from a `SeminormedSpace.Core`. Note that
if this is used to define an instance on a type, it also provides a new distance measure from the
norm.  it must therefore not be used on a type with a preexisting distance measure or topology.
See note [reducible non-instances].  -/
SeminormedAddCommGroup.ofCore : {𝕜 : Type u_6} →
  {E : Type u_7} →
    [inst : NormedField 𝕜] →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Norm E] → [inst_3 : Module 𝕜 E] → SeminormedSpace.Core 𝕜 E → SeminormedAddCommGroup E
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.diagonal_isomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C],
  (CategoryTheory.MorphismProperty.isomorphisms C).diagonal = CategoryTheory.MorphismProperty.monomorphisms C
-- Mathlib.Algebra.Group.ULift
ULift.add : {α : Type u} → [Add α] → Add (ULift.{u_1, u} α)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- If `α` and `β` are two equal natural transformations, then the functors of coalgebras induced by
them are isomorphic.
We define it like this as opposed to using `eq_to_iso` so that the components are nicer to prove
lemmas about.
 -/
CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransEq : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor C C} →
      {α β : F ⟶ G} →
        α = β →
          (CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans α ≅
            CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans β)
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- `A.Free B` means that `B` does not contain a copy of `A`.  -/
SimpleGraph.Free : {α : Type u_4} → {β : Type u_5} → SimpleGraph α → SimpleGraph β → Prop
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
/-- A generalisation of `Seq.eq_of_bisim'` that allows using a friendly operation in the tail
of the sequences.  -/
Tactic.ComputeAsymptotics.Seq.FriendlyOperationClass.eq_of_bisim : ∀ {α : Type u_1} {γ : Type u_3} {s t : Stream'.Seq α} {op : γ → Stream'.Seq α → Stream'.Seq α}
  [Tactic.ComputeAsymptotics.Seq.FriendlyOperationClass op] (motive : Stream'.Seq α → Stream'.Seq α → Prop),
  motive s t →
    (∀ (u v : Stream'.Seq α),
        motive u v →
          u = v ∨ ∃ hd u' v' c, u = Stream'.Seq.cons hd (op c u') ∧ v = Stream'.Seq.cons hd (op c v') ∧ motive u' v') →
      s = t
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.find?_toList_eq_none_iff_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  List.find? (fun x => cmp x.1 k == Ordering.eq) t.toList = none ↔ t.contains k = false
-- Mathlib.Logic.Equiv.Defs
Equiv.symm_mk : ∀ {α : Sort u} {β : Sort v} (f : α → β) (g : β → α) (hl : Function.LeftInverse g f) (hr : Function.RightInverse g f),
  { toFun := f, invFun := g, left_inv := hl, right_inv := hr }.symm =
    { toFun := g, invFun := f, left_inv := hr, right_inv := hl }
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.IsBase.eRk_eq_eRank : ∀ {α : Type u_1} {M : Matroid α} {B : Set α}, M.IsBase B → M.eRk B = M.eRank
-- Mathlib.Topology.Separation.Regular
T5Space.mk : ∀ {X : Type u} [inst : TopologicalSpace X] [toT1Space : T1Space X] [toCompletelyNormalSpace : CompletelyNormalSpace X],
  T5Space X
-- Mathlib.Topology.FiberBundle.Constructions
Equiv.toHomeomorphOfIsInducing.congr_simp : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f f_1 : X ≃ Y)
  (e_f : f = f_1) (hf : Topology.IsInducing ⇑f), f.toHomeomorphOfIsInducing hf = f_1.toHomeomorphOfIsInducing ⋯
-- Lean.Message
/-- Tagged sections. `Name` should be viewed as a "kind", and is used by `MessageData` inspector functions.
Example: an inspector that tries to find "definitional equality failures" may look for the tag "DefEqFailure".  -/
Lean.MessageData.tagged : Lean.Name → Lean.MessageData → Lean.MessageData
-- Mathlib.Data.Fintype.EquivFin
Function.LeftInverse.rightInverse_of_card_le : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] {f : α → β} {g : β → α},
  Function.LeftInverse f g → Fintype.card α ≤ Fintype.card β → Function.RightInverse f g
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.isStableUnderProductsOfShape_fibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)] (J : Type w),
  (HomotopicalAlgebra.fibrations C).IsStableUnderProductsOfShape J
-- Init.Data.Array.Int
Array.sum_le_max_mul_length_of_max?_eq_some_int : ∀ {x : ℤ} {xs : Array ℤ}, xs.max? = some x → xs.sum ≤ x * ↑xs.size
-- Init.Data.Array.Monadic
_private.Init.Data.Array.Monadic.0.Array.foldlM_filterMap.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → ((b : β) → motive (some b)) → (Unit → motive none) → motive x
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.symm_apply_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst_1 : Add α] [inst_2 : LE α] [inst_3 : Mul β] [inst_4 : Add β]
  [inst_5 : LE β] (e : α ≃+*o β) (a : α), e.symm (e a) = a
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.eq_cycleOf_of_mem_cycleFactorsFinset_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] (g c : Equiv.Perm α),
  c ∈ g.cycleFactorsFinset → ∀ (x : α), c = g.cycleOf x ↔ x ∈ c.support
-- Mathlib.Data.ENat.Lattice
ENat.iInf_natCast_lt_top : ∀ {ι : Sort u_1} {f : ι → ℕ}, ⨅ i, ↑(f i) < ⊤ ↔ Nonempty ι
-- Lean.Meta.Diagnostics
Lean.Meta.mkDiagSummaryForUsedInstances : Lean.MetaM Lean.Meta.DiagSummary
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_zsmul_add : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℤ), toIcoDiv hp a (m • p + b) = m + toIcoDiv hp a b
-- Std.Data.DHashMap.Raw
/-- Creates a hash map from a list of mappings. If the same key appears multiple times, the last
occurrence takes precedence.  -/
Std.DHashMap.Raw.Const.ofList : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → List (α × β) → Std.DHashMap.Raw α fun x => β
-- Mathlib.Analysis.InnerProductSpace.l2Space
lp.instInnerProductSpace : {ι : Type u_1} →
  {𝕜 : Type u_2} →
    [inst : RCLike 𝕜] →
      {G : ι → Type u_4} →
        [inst_1 : (i : ι) → NormedAddCommGroup (G i)] →
          [(i : ι) → InnerProductSpace 𝕜 (G i)] → InnerProductSpace 𝕜 ↥(lp G 2)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_17.eq_9 : ∀ (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) (w n : ℕ) (lhs : Std.Tactic.BVDecide.BVExpr w)
  (rhs : Std.Tactic.BVDecide.BVExpr n) (h_1 : (w a : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var a))
  (h_2 : (w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val))
  (h_3 :
    (w : ℕ) →
      (lhsExpr : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinOp) →
          (rhsExpr : Std.Tactic.BVDecide.BVExpr w) → motive w (lhsExpr.bin op rhsExpr))
  (h_4 :
    (w : ℕ) →
      (op : Std.Tactic.BVDecide.BVUnOp) →
        (expr : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op expr))
  (h_5 :
    (w l r : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr l) →
        (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h))
  (h_6 :
    (w w_1 n : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w_1) →
        (h : w = w_1 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h))
  (h_7 :
    (len w start : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w) → motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr))
  (h_8 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs))
  (h_9 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs))
  (h_10 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)),
  (match w, lhs.shiftRight rhs with
    | w, Std.Tactic.BVDecide.BVExpr.var a => h_1 w a
    | w, Std.Tactic.BVDecide.BVExpr.const val => h_2 w val
    | w, lhsExpr.bin op rhsExpr => h_3 w lhsExpr op rhsExpr
    | w, Std.Tactic.BVDecide.BVExpr.un op expr => h_4 w op expr
    | w, lhs.append rhs h => h_5 w l r lhs rhs h
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h => h_6 w w_1 n expr h
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr => h_7 len w start expr
    | w, lhs.shiftLeft rhs => h_8 w n lhs rhs
    | w, lhs.shiftRight rhs => h_9 w n lhs rhs
    | w, lhs.arithShiftRight rhs => h_10 w n lhs rhs) =
    h_9 w n lhs rhs
-- Init.Data.Slice.List.Lemmas
ListSlice.toArray_mkSlice_ric : ∀ {α : Type u_1} {xs : ListSlice α} {hi : ℕ},
  Std.Slice.toArray (Std.Ric.Sliceable.mkSlice xs *...=hi) = (Std.Slice.toArray xs).extract 0 (hi + 1)
-- Std.Data.DTreeMap.Raw.Iterator
Std.DTreeMap.Raw.toList.eq_1 : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Std.DTreeMap.Raw α β cmp), t.toList = t.inner.toList
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
/-- The cocone on `F₁` with apex `A`.  -/
CategoryTheory.IndParallelPairPresentation.ι₁ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} →
      {f g : A ⟶ B} →
        (self : CategoryTheory.IndParallelPairPresentation f g) →
          self.F₁.comp CategoryTheory.yoneda ⟶ (CategoryTheory.Functor.const self.I).obj A
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.neg_apply : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (D : LieDerivation R L M) (a : L), (-D) a = -D a
-- Init.Data.SInt.Lemmas
Int16.ofIntLE_eq_ofIntClamp : ∀ {x : ℤ} {h₁ : Int16.minValue.toInt ≤ x} {h₂ : x ≤ Int16.maxValue.toInt}, Int16.ofIntLE x h₁ h₂ = Int16.ofIntClamp x
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.nodup : ∀ {numVarsSucc : ℕ} (self : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause numVarsSucc), List.Nodup self.clause
-- Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver
/-- Given a Grothendieck topology `J` on a category `C` and a category `A`,
this is the pseudofunctor which sends `X : C` to the categories of
sheaves on `Over X` with values in `A`.  -/
CategoryTheory.GrothendieckTopology.pseudofunctorOver : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.GrothendieckTopology C →
      (A : Type u') →
        [CategoryTheory.Category.{v', u'} A] →
          CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat
-- Mathlib.Algebra.Category.MonCat.Limits
AddMonCat.forget_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget AddMonCat)
-- Mathlib.Order.PrimeIdeal
Order.Ideal.IsPrime.toIsProper : ∀ {P : Type u_1} {inst : Preorder P} {I : Order.Ideal P} [self : I.IsPrime], I.IsProper
-- Mathlib.Topology.Algebra.Monoid
instSeparatelyContinuousMulMultiplicativeOfSeparatelyContinuousAdd : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Add M] [SeparatelyContinuousAdd M],
  SeparatelyContinuousMul (Multiplicative M)
-- Mathlib.Data.Set.Card
Set.encard_ne_zero_of_mem : ∀ {α : Type u_1} {s : Set α} {a : α}, a ∈ s → s.encard ≠ 0
-- Mathlib.RingTheory.Localization.Module
LinearEquiv.extendScalarsOfIsLocalizationEquiv_symm_apply : ∀ {R : Type u_3} [inst : CommSemiring R] (S : Submonoid R) (A : Type u_4) [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : IsLocalization S A] {M : Type u_5} {N : Type u_6} [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : Module A M] [inst_7 : IsScalarTower R A M] [inst_8 : AddCommMonoid N]
  [inst_9 : Module R N] [inst_10 : Module A N] [inst_11 : IsScalarTower R A N] (e : M ≃ₗ[A] N),
  (LinearEquiv.extendScalarsOfIsLocalizationEquiv S A).symm e = LinearEquiv.restrictScalars R e
-- Lean.Meta.Tactic.Simp.Rewrite
/-- Tries to solve `e` using `unifyEq?`.
It assumes that `isEqnThmHypothesis e` is `true`.
 -/
Lean.Meta.Simp.dischargeEqnThmHypothesis? : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Lean.Elab.Tactic.Induction
/-- Elaborated `ElimTargetView`.  -/
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimTargetInfo : Type
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKeyD_of_perm : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l l' : List ((a : α) × β a)} {fallback : α},
  Std.Internal.List.DistinctKeys l →
    l.Perm l' → Std.Internal.List.maxKeyD l fallback = Std.Internal.List.maxKeyD l' fallback
-- Mathlib.Topology.Order.Hom.Esakia
/-- `PseudoEpimorphismClass F α β` states that `F` is a type of `⊔`-preserving morphisms.

You should extend this class when you extend `PseudoEpimorphism`.  -/
PseudoEpimorphismClass : (F : Type u_6) →
  (α : outParam (Type u_7)) → (β : outParam (Type u_8)) → [Preorder α] → [Preorder β] → [FunLike F α β] → Prop
-- Mathlib.AlgebraicTopology.Reedy.Basic
HomotopicalAlgebra.ReedyStructure.prop₁_of_degHom_eq_deg_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [inst_1 : W₁.IsMultiplicative] [inst_2 : W₂.IsMultiplicative] {α : Type u_2} [inst_3 : LinearOrder α]
  [inst_4 : OrderBot α] [inst_5 : SuccOrder α] [inst_6 : WellFoundedLT α]
  (r : HomotopicalAlgebra.ReedyStructure W₁ W₂ α) {X Y : C} {f : X ⟶ Y}, r.degHom f = r.deg Y → W₁ f
-- Mathlib.Logic.Denumerable
Nat.Subtype.lt_succ_iff_le : ∀ {s : Set ℕ} [inst : Infinite ↑s] [inst_1 : DecidablePred fun x => x ∈ s] {x y : ↑s}, x < Nat.Subtype.succ y ↔ x ≤ y
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
/-- Given a finite cyclic group `G` generated by `g` and `A : Rep k G`, `Hⁱ(G, A)` is isomorphic
to the homology of the short complex of `k`-modules `A --N--> A --(ρ(g) - 𝟙)--> A` when `i` is
nonzero and even.  -/
Rep.FiniteCyclicGroup.groupCohomologyIsoEven : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : CommGroup G] →
      [inst_2 : Fintype G] →
        (A : Rep.{u, u, u} k G) →
          (g : G) →
            (∀ (x : G), x ∈ Subgroup.zpowers g) →
              (i : ℕ) →
                [h₀ : NeZero i] → Even i → (groupCohomology A i ≅ (Rep.FiniteCyclicGroup.normHomCompSub A g).homology)
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.instSub : {Γ : Type u_1} →
  {R : Type u_3} →
    {α : Type u_5} → [inst : PartialOrder Γ] → [inst_1 : AddCommGroup R] → Sub (HahnSeries.SummableFamily Γ R α)
-- Mathlib.Order.CompleteLattice.Basic
biInf_le_eq_of_antitone : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : Preorder β] {f : β → α},
  Antitone f → ∀ (b : β), ⨅ b', ⨅ (_ : b' ≤ b), f b' = f b
-- Lean.Meta.Tactic.Grind.Util
/-- Returns `Grind.MatchCond e`.
We have special support for propagating is truth value.
See comment at `MatchCond.lean`.
 -/
Lean.Meta.Grind.markAsMatchCond : Lean.Expr → Lean.Expr
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.ιObj_πObj_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ] {X Y : C}
  (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.ιObj I κ f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.πObj I κ f) h) =
    CategoryTheory.CategoryStruct.comp f h
-- Init.Data.String.Lemmas.Splits
String.Pos.splits_next_right : ∀ {s : String} (p : s.Pos) (hp : p ≠ s.endPos),
  p.Splits (s.sliceTo p).copy (String.singleton (p.get hp) ++ (s.sliceFrom (p.next hp)).copy)