mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeMap.Raw.Basic
Std.TreeMap.Raw.instMembership : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Membership α (Std.TreeMap.Raw α β cmp)
-- Mathlib.RingTheory.FiniteType
/-- If a set `S` generates, as algebra, `R[M]`, then the set of supports of
elements of `S` generates `R[M]`.  -/
AddMonoidAlgebra.support_gen_of_gen : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddMonoid M] {S : Set (AddMonoidAlgebra R M)},
  Algebra.adjoin R S = ⊤ → Algebra.adjoin R (⋃ f ∈ S, AddMonoidAlgebra.of' R M '' ↑f.coeff.support) = ⊤
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.single_eq_of_ne : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] {i i' : ι} {b : β i},
  i' ≠ i → (fun₀ | i => b) i' = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
SSet.prodStdSimplex.nonDegenerate_max_dim_iff : ∀ {p q n : ℕ}
  (z :
    (CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := p })
          (SSet.stdSimplex.obj { len := q })).obj
      (Opposite.op { len := n }))
  (hn : autoParam (p + q = n) SSet.prodStdSimplex.nonDegenerate_max_dim_iff._auto_1),
  z ∈
      (CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := p })
            (SSet.stdSimplex.obj { len := q })).nonDegenerate
        n ↔
    SSet.prodStdSimplex.orderHomOfSimplex z hn = OrderHom.id
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.sectR_apply : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ) (b : β) (a : α), (κ.sectR a) b = κ (a, b)
-- Mathlib.NumberTheory.SumFourSquares
/-- Lagrange's **four squares theorem** for a prime number. Use `Nat.sum_four_squares` instead.  -/
Nat.Prime.sum_four_squares : ∀ {p : ℕ}, Nat.Prime p → ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = p
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.map_add : ∀ {F : Type u} {K : Type v} [inst : Field F] [inst_1 : Field K] {W : WeierstrassCurve.Projective F} (f : F →+* K)
  {P Q : Fin 3 → F}, W.Nonsingular P → W.Nonsingular Q → (W.map f).add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W.add P Q
-- Mathlib.Topology.CompactOpen
ContinuousMap.curry_apply : ∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (f : C(X × Y, Z)) (a : X) (b : Y), (f.curry a) b = f (a, b)
-- Mathlib.Combinatorics.Digraph.Basic
/-- Constructor for digraphs using a Boolean function.
This is useful for creating a digraph with a decidable `Adj` relation,
and it's used in the construction of the `Fintype (Digraph V)` instance.
 -/
Digraph.mk' : {V : Type u_1} → (V → V → Bool) ↪ Digraph V
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.get!_eq_get!ₘ : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) [inst_1 : Inhabited β] (l : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.get! l k = Std.DTreeMap.Internal.Impl.Const.get!ₘ l k
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.commRing.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : CommRing R] [inst_1 : AddCommMonoid M],
  AddMonoidAlgebra.commRing = { toRing := AddMonoidAlgebra.ring, mul_comm := ⋯ }
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.str : (self : CommGrpCat) → CommGroup ↑self
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocyclesMk₀_eq : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (x : ↥A.ρ.invariants),
  groupCohomology.cocyclesMk ((CategoryTheory.ConcreteCategory.hom (groupCohomology.cochainsIso₀ A).inv) ↑x) ⋯ =
    (CategoryTheory.ConcreteCategory.hom (groupCohomology.cocyclesIso₀ A).inv) x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey_eq_back_keysArray : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {he : t.isEmpty = false}, t.maxKey he = t.keysArray.back ⋯
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.isLeftKanExtension_along_uliftYoneda_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ]
  {A : CategoryTheory.Functor C ℰ} [CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A]
  (L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) ℰ)
  (α : A ⟶ CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp L),
  L.IsLeftKanExtension α ↔
    CategoryTheory.IsIso α ∧
      CategoryTheory.Limits.PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
          max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
        L
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
InnerProductSpace.gramSchmidt_def' : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι] (f : ι → E)
  (n : ι),
  f n = InnerProductSpace.gramSchmidt 𝕜 f n + ∑ i < n, (𝕜 ∙ InnerProductSpace.gramSchmidt 𝕜 f i).starProjection (f n)
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq : Int64.instRxcHasSize = HasModel.instRxcHasSize✝
-- Mathlib.Algebra.Ring.Commute
Commute.neg_right_iff : ∀ {R : Type u} [inst : Mul R] [inst_1 : HasDistribNeg R] {a b : R}, Commute a (-b) ↔ Commute a b
-- Mathlib.AlgebraicGeometry.Geometrically.Irreducible
AlgebraicGeometry.GeometricallyIrreducible.comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.GeometricallyIrreducible f]
  [AlgebraicGeometry.GeometricallyIrreducible g] [AlgebraicGeometry.UniversallyOpen f]
  [AlgebraicGeometry.UniversallyOpen g],
  AlgebraicGeometry.GeometricallyIrreducible (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Data.Finset.Range
Finset.range_mono : Monotone Finset.range
-- Std.Http.Data.Request
Std.Http.Request.mk.injEq : ∀ {t : Type} (line : Std.Http.Request.Head) (body : t) (extensions : Std.Http.Extensions)
  (line_1 : Std.Http.Request.Head) (body_1 : t) (extensions_1 : Std.Http.Extensions),
  ({ line := line, body := body, extensions := extensions } =
      { line := line_1, body := body_1, extensions := extensions_1 }) =
    (line = line_1 ∧ body = body_1 ∧ extensions = extensions_1)
-- Lean.Attributes
Lean.instInhabitedAttributeExtensionState.default : Lean.AttributeExtensionState
-- Mathlib.Analysis.InnerProductSpace.Coalgebra
/-- A finite-dimensional inner product space with a coalgebra structure induces an algebra
structure, where `x * y = (adjoint comul) (x ⊗ₜ y)`, `1 = (adjoint counit) 1` and
`algebraMap = adjoint counit`.

See note [reducible non-instances].  -/
InnerProductSpace.algebraOfCoalgebra : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] → [inst_3 : FiniteDimensional 𝕜 E] → [inst_4 : Coalgebra 𝕜 E] → Algebra 𝕜 E
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.scalar_commute : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (u : Rˣ) (A : GL n R),
  (Matrix.GeneralLinearGroup.scalar n) u * A = A * (Matrix.GeneralLinearGroup.scalar n) u
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.FullyFaithful.mapMon_preimage_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] (hF : F.FullyFaithful) {X Y : CategoryTheory.Mon C}
  (f : F.mapMon.obj X ⟶ F.mapMon.obj Y), (hF.mapMon.preimage f).hom = hF.preimage f.hom
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.size_unitOfList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α},
  List.Pairwise (fun a b => (a == b) = false) l → (Std.DHashMap.Raw.Const.unitOfList l).size = l.length
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.forget_faithful : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C},
  (CategoryTheory.Endofunctor.Algebra.forget F).Faithful
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.linearCombination_embDomain : ∀ {α : Type u_1} (R : Type u_5) [inst : Semiring R] {α' : Type u_7} {M' : Type u_8} [inst_1 : AddCommMonoid M']
  [inst_2 : Module R M'] {v' : α' → M'} (f : α ↪ α') (l : α →₀ R),
  (Finsupp.linearCombination R v') (Finsupp.embDomain f l) = (Finsupp.linearCombination R (v' ∘ ⇑f)) l
-- Mathlib.Analysis.Normed.Field.WithAbs
WithAbs.normedField : {R : Type u_1} → [inst : Field R] → (v : AbsoluteValue R ℝ) → NormedField (WithAbs v)
-- Mathlib.Order.Filter.AtTopBot.Defs
Filter.Iio_mem_atBot : ∀ {α : Type u_3} [inst : Preorder α] [NoBotOrder α] (x : α), Set.Iio x ∈ Filter.atBot
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_filter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  {f : (a : α) → β a → Bool} {k : α},
  (Std.DHashMap.filter f m).getKey? k = (m.getKey? k).pfilter fun x_2 h' => f x_2 (m.get x_2 ⋯)
-- Mathlib.Analysis.Normed.Group.Basic
norm_sub_norm_le : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] (a b : E), ‖a‖ - ‖b‖ ≤ ‖a - b‖
-- Init.Data.BitVec.Bitblast
/-- If the division equation `d.toNat * q.toNat + r.toNat = n.toNat` holds,
then `n.udiv d = q`.  -/
BitVec.udiv_eq_of_mul_add_toNat : ∀ {w : ℕ} {d n q r : BitVec w}, 0 < d → r < d → d.toNat * q.toNat + r.toNat = n.toNat → n / d = q
-- Mathlib.Topology.Algebra.Module.UniformConvergence
/-- Let `E` be a TVS, `𝔖 : Set (Set α)` and `H` a submodule of `α →ᵤ[𝔖] E`. If the image of any
`S ∈ 𝔖` by any `u ∈ H` is bounded (in the sense of `Bornology.IsVonNBounded`), then `H`,
equipped with the topology of `𝔖`-convergence, is a TVS.

If you have a hard time using this lemma, try the one above instead.  -/
UniformOnFun.continuousSMul_submodule_of_image_bounded : ∀ (𝕜 : Type u_1) (α : Type u_2) (E : Type u_3) [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : UniformSpace E] [IsUniformAddGroup E] [ContinuousSMul 𝕜 E] {𝔖 : Set (Set α)}
  (H : Submodule 𝕜 (UniformOnFun α E 𝔖)), (∀ u ∈ H, ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 (u '' s)) → ContinuousSMul 𝕜 ↥H
-- Mathlib.Data.Finsupp.MonomialOrder
MonomialOrder.mk : {σ : Type u_1} →
  (syn : Type u_2) →
    (addCommMonoidSyn : autoParam (AddCommMonoid syn) MonomialOrder.addCommMonoidSyn._autoParam) →
      (linearOrderSyn : autoParam (LinearOrder syn) MonomialOrder.linearOrderSyn._autoParam) →
        autoParam (IsOrderedAddMonoid syn) MonomialOrder.isOrderedAddMonoid_syn._autoParam →
          (toSyn : (σ →₀ ℕ) ≃+ syn) →
            Monotone ⇑toSyn → autoParam (WellFoundedLT syn) MonomialOrder.wellFoundedLT_syn._autoParam → MonomialOrder σ
-- ImportGraph.Graph.TransitiveClosure
/-- Compute the transitive closure of an import graph.
 -/
Lean.NameMap.transitiveClosure : Lean.NameMap (Array Lean.Name) → Lean.NameMap Lean.NameSet
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift.0.Std.IterM.toArray_eq_match_step.match_1.eq_2 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (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.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Mathlib.CategoryTheory.Monoidal.Limits.Preserves
CategoryTheory.MonoidalCategory.Limits.preservesLimit_curriedTensor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {J : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} J] (F : CategoryTheory.Functor J C)
  [h : ∀ (c : C), CategoryTheory.Limits.PreservesLimit F (CategoryTheory.MonoidalCategory.tensorRight c)],
  CategoryTheory.Limits.PreservesLimit F (CategoryTheory.MonoidalCategory.curriedTensor C)
-- Mathlib.Tactic.Ring.Basic
Mathlib.Tactic.Ring.smul_eq_mul : ∀ {α : Type u_2} [inst : Mul α] {a a' : α}, a = a' → ∀ (b : α), a • b = a' * b
-- Mathlib.Algebra.Category.Grp.Limits
/-- If `J` is `u`-small, `AddCommGrpCat.{u}` has limits of shape `J`.  -/
AddCommGrpCat.hasLimitsOfShape : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] [Small.{u, v} J],
  CategoryTheory.Limits.HasLimitsOfShape J AddCommGrpCat
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubringClass.addSubgroupClass : ∀ (S : Type u_1) (R : Type u) [inst : SetLike S R] [inst_1 : NonUnitalNonAssocRing R] [h : NonUnitalSubringClass S R],
  AddSubgroupClass S R
-- Mathlib.Probability.Distributions.Gaussian.Real
MeasurableEquiv.gaussianReal_map_symm_apply : ∀ {μ : ℝ} {v : NNReal},
  v ≠ 0 →
    ∀ (f : ℝ ≃ᵐ ℝ) {f' : ℝ → ℝ},
      (∀ (x : ℝ), HasDerivAt (⇑f) (f' x) x) →
        ∀ {s : Set ℝ},
          MeasurableSet s →
            (MeasureTheory.Measure.map (⇑f.symm) (ProbabilityTheory.gaussianReal μ v)) s =
              ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * ProbabilityTheory.gaussianPDFReal μ v (f x))
-- Mathlib.Topology.Connected.Basic
IsPreconnected.lt_of_ne : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] {s : Set α} [inst_1 : LinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {b : β},
  IsPreconnected s → ContinuousOn f s → (∀ x ∈ s, f x ≠ b) → (∃ x ∈ s, b < f x) → ∀ {x : α}, x ∈ s → b < f x
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Real.differentiable_rpow_const : ∀ {p : ℝ}, 1 ≤ p → Differentiable ℝ fun x => x ^ p
-- Mathlib.Order.Filter.Prod
Filter.Eventually.image_of_prod : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} {y : α → β} {r : α → β → Prop},
  Filter.Tendsto y f g → (∀ᶠ (p : α × β) in f ×ˢ g, r p.1 p.2) → ∀ᶠ (x : α) in f, r x (y x)
-- Init.Prelude
EStateM.instInhabitedResult : {ε σ α : Type u} → [Inhabited ε] → [Inhabited σ] → Inhabited (EStateM.Result ε σ α)
-- Aesop.Rule.Name
Aesop.BuilderName.instOrd : Ord Aesop.BuilderName
-- Mathlib.NumberTheory.Padics.PadicNumbers
/-- The p-adic valuation on rationals, sending `p` to `(exp (-1) : ℤᵐ⁰)`  -/
Rat.padicValuation : (p : ℕ) → [Fact (Nat.Prime p)] → Valuation ℚ (WithZero (Multiplicative ℤ))
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
/-- Any `IsPathGraph3Compl` in `G` gives rise to a graph embedding of the complement of the path graph
 -/
SimpleGraph.IsPathGraph3Compl.pathGraph3ComplEmbedding : {α : Type u} → {G : SimpleGraph α} → {v w₁ w₂ : α} → G.IsPathGraph3Compl v w₁ w₂ → (SimpleGraph.pathGraph 3)ᶜ ↪g G
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- A version of `contDiffWithinAt_succ_iff_hasFDerivWithinAt` where all derivatives
are taken within the same set.  -/
contDiffWithinAt_succ_iff_hasFDerivWithinAt' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : WithTop ℕ∞},
  n ≠ ↑⊤ →
    (ContDiffWithinAt 𝕜 (n + 1) f s x ↔
      ∃ u ∈ nhdsWithin x (insert x s),
        u ⊆ insert x s ∧
          (n = ⊤ → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) s x) ∧ ContDiffWithinAt 𝕜 n f' s x)
-- Mathlib.Topology.DenseEmbedding
IsDenseInducing.extend_unique_at : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β}
  [inst_2 : TopologicalSpace γ] [T2Space γ] {b : β} {f : α → γ} {g : β → γ} (di : IsDenseInducing i),
  (∀ᶠ (x : α) in Filter.comap i (nhds b), g (i x) = f x) → ContinuousAt g b → di.extend f b = g b
-- Mathlib.Algebra.Homology.HomologicalComplex
ChainComplex.next_nat_zero : (ComplexShape.down ℕ).next 0 = 0
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Cell.Const.get?.match_1.splitter : {α : Type u_2} →
  {β : Type u_1} →
    (motive : Option ((_ : α) × β) → Sort u_3) →
      (x : Option ((_ : α) × β)) → (Unit → motive none) → ((p : (_ : α) × β) → motive (some p)) → motive x
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.Struct.id : Lean.Meta.Grind.Arith.Linear.Struct → ℕ
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.ExtensionState.erased : {γ : Type} → Lean.KeyedDeclsAttribute.ExtensionState γ → Lean.PHashSet Lean.Name
-- Mathlib.Data.Set.Finite.Basic
Set.finite_image_iff : ∀ {α : Type u} {β : Type v} {s : Set α} {f : α → β}, Set.InjOn f s → ((f '' s).Finite ↔ s.Finite)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.size_toArray_roo : ∀ {a b : ℤ}, (a<...b).toArray.size = (b - a - 1).toNat
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
IsKleinFour.mulEquiv.eq_1 : ∀ {G₁ : Type u_2} {G₂ : Type u_3} [inst : Group G₁] [inst_1 : Group G₂] [inst_2 : IsKleinFour G₁]
  [inst_3 : IsKleinFour G₂] (e : G₁ ≃ G₂) (he : e 1 = 1), IsKleinFour.mulEquiv e he = IsKleinFour.mulEquiv' e he ⋯
-- Mathlib.Tactic.Positivity.Basic
/-- Extension for `Nat.factorial`.  -/
Mathlib.Meta.Positivity.evalFactorial : Mathlib.Meta.Positivity.PositivityExt
-- Init.Data.Nat.Compare
Nat.compare_eq_gt : ∀ {a b : ℕ}, compare a b = Ordering.gt ↔ b < a
-- Mathlib.GroupTheory.Exponent
AddMonoid.exponent_dvd_iff_forall_nsmul_eq_zero : ∀ {G : Type u} [inst : AddMonoid G] {n : ℕ}, AddMonoid.exponent G ∣ n ↔ ∀ (g : G), n • g = 0
-- Mathlib.Logic.Equiv.Prod
Equiv.sigmaEquivProd_sigmaCongrRight : ∀ {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂),
  (Equiv.sigmaEquivProd α₁ β₁).symm.trans (Equiv.sigmaCongrRight e) =
    (Equiv.prodCongrRight e).trans (Equiv.sigmaEquivProd α₁ β₂).symm
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.hasHomology_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K L : HomologicalComplex C c} (iso : K ≅ L) (i : ι) [K.HasHomology i],
  L.HasHomology i
-- Mathlib.MeasureTheory.Function.LpOrder
MeasureTheory.Lp.coeFn_inf : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal}
  [inst : NormedAddCommGroup E] [inst_1 : Lattice E] [inst_2 : HasSolidNorm E] [inst_3 : IsOrderedAddMonoid E]
  (f g : ↥(MeasureTheory.Lp E p μ)), ↑↑(f ⊓ g) =ᵐ[μ] ↑↑f ⊓ ↑↑g
-- Lean.MetavarContext
Lean.instMonadMCtxStateMMetavarContext : Lean.MonadMCtx (StateM Lean.MetavarContext)
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.instInhabited : {M : Type u_1} → [inst : Add M] → Inhabited (AddCon M)
-- Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Real.Gamma_strictAntiOn_Ioc : StrictAntiOn Real.Gamma (Set.Ioc 0 1)
-- Mathlib.RingTheory.Nakayama
LinearMap.surjective_of_surjective_comp_mkQ : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [Module.Finite R N] (f : M →ₗ[R] N),
  ∀ I ≤ ⊥.jacobson, Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f) → Function.Surjective ⇑f
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ioc.instMonoid : {R : Type u_1} → [inst : Semiring R] → [inst_1 : PartialOrder R] → [IsStrictOrderedRing R] → Monoid ↑(Set.Ioc 0 1)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.var.sizeOf_spec : ∀ (i : Lean.Grind.Linarith.Var), sizeOf (Lean.Grind.Linarith.Expr.var i) = 1 + sizeOf i
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.forget_map : ∀ (R : Type u) [inst : Ring R] {M N : ModuleCat R} (f : M ⟶ N),
  ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget (ModuleCat R)).map f)) =
    ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
/-- Given a finite cyclic group `G` generated by `g` and `A : Rep k G`, this is the quotient map
`Ker(ρ(g) - Id(A)) ⟶ Ker(ρ(g) - Id(A))/Im(N) ≅ Hⁱ(G, A)` for any nonzero even `i`.  -/
Rep.FiniteCyclicGroup.groupCohomologyπEven : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : CommGroup G] →
      [Fintype G] →
        (A : Rep.{u, u, u} k G) →
          (g : G) →
            (∀ (x : G), x ∈ Subgroup.zpowers g) →
              (i : ℕ) →
                [NeZero i] →
                  Even i →
                    (ModuleCat.of k ↥(Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).ker ⟶
                      groupCohomology A i)
-- Mathlib.Algebra.Group.Action.Opposite
op_smul_op_smul : ∀ {α : Type u_3} {β : Type u_4} [inst : Monoid α] [inst_1 : MulAction αᵐᵒᵖ β] (b : β) (a₁ a₂ : α),
  MulOpposite.op a₂ • MulOpposite.op a₁ • b = MulOpposite.op (a₁ * a₂) • b
-- Batteries.Data.RunningStats
Batteries.RunningStats.init.sizeOf_spec : ∀ (count : ℕ) (mean var : Float),
  sizeOf { count := count, mean := mean, var := var } = 1 + sizeOf count + sizeOf mean + sizeOf var
-- Mathlib.Data.EReal.Inv
EReal.sign_mul_abs : ∀ (x : EReal), ↑(SignType.sign x) * ↑x.abs = x
-- Lean.Compiler.IR.Basic
Lean.IR.Alt.default : Lean.IR.FnBody → Lean.IR.Alt
-- Batteries.Data.Stream
Std.Stream.fst_take_succ : ∀ {σ : Type u_1} {α : Type u_2} {n : ℕ} [inst : Std.Stream σ α] (s : σ),
  (Std.Stream.take s (n + 1)).1 =
    match Std.Stream.next? s with
    | none => []
    | some (a, s) => a :: (Std.Stream.take s n).1
-- Mathlib.Order.Filter.SmallSets
Filter.HasAntitoneBasis.tendsto_smallSets : ∀ {α : Type u_1} {l : Filter α} {ι : Type u_4} [inst : Preorder ι] {s : ι → Set α},
  l.HasAntitoneBasis s → Filter.Tendsto s Filter.atTop l.smallSets
-- Mathlib.Algebra.CubicDiscriminant
Cubic.C_mul_prod_X_sub_C_eq : ∀ {S : Type u_2} [inst : CommRing S] {w x y z : S},
  Polynomial.C w * (Polynomial.X - Polynomial.C x) * (Polynomial.X - Polynomial.C y) * (Polynomial.X - Polynomial.C z) =
    { a := w, b := w * -(x + y + z), c := w * (x * y + x * z + y * z), d := w * -(x * y * z) }.toPoly
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.instPreadditiveLocalization' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Preadditive C] →
      (W : CategoryTheory.MorphismProperty C) →
        [W.HasLeftCalculusOfFractions] → [inst_3 : W.HasLocalization] → CategoryTheory.Preadditive W.Localization'
-- Batteries.Data.List.Lemmas
List.foldrIdx_cons : ∀ {α : Type u_1} {x : α} {xs : List α} {α_1 : Type u_2} {f : ℕ → α → α_1 → α_1} {i : α_1} {s : ℕ},
  List.foldrIdx f i (x :: xs) s = f s x (List.foldrIdx f i xs (s + 1))
-- Init.Data.SInt.Lemmas
Int8.zero_lt_one : 0 < 1
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryCofan.IsColimit.inr_desc_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y W : C} {s : CategoryTheory.Limits.BinaryCofan X Y}
  (h : CategoryTheory.Limits.IsColimit s) (f : X ⟶ W) (g : Y ⟶ W) {Z : C} (h_1 : W ⟶ Z),
  CategoryTheory.CategoryStruct.comp s.inr
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryCofan.IsColimit.desc h f g) h_1) =
    CategoryTheory.CategoryStruct.comp g h_1
-- Mathlib.Data.PFun
PFun.dom_iff_graph : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β) (x : α), x ∈ f.Dom ↔ ∃ y, (x, y) ∈ f.graph
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.Tree.mk.congr_simp : ∀ {α : Type u} {β : α → Type v} {size : ℕ} (impl impl_1 : Std.DTreeMap.Internal.Impl α β) (e_impl : impl = impl_1)
  (balanced_impl : impl.Balanced) (size_impl : impl.size = size),
  { impl := impl, balanced_impl := balanced_impl, size_impl := size_impl } =
    { impl := impl_1, balanced_impl := ⋯, size_impl := ⋯ }