mathlib-initiative/mathlib-types huggingface dataset:
-- 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(N) ⟶ Ker(N)/Im(ρ(g) - Id(A)) ≅ Hⁱ(G, A)` for any odd `i`.  -/
Rep.FiniteCyclicGroup.groupCohomologyπOdd : {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 : ℕ) → Odd i → (ModuleCat.of k ↥(Rep.Hom.hom A.norm).ker ⟶ groupCohomology A i)
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.mem_ae_iff_prob_eq_one₀ : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}
  [MeasureTheory.IsProbabilityMeasure μ], MeasureTheory.NullMeasurableSet s μ → (s ∈ MeasureTheory.ae μ ↔ μ s = 1)
-- Init.Data.Iterators.Consumers.Loop
/-- Steps through the whole iterator, counting the number of outputs emitted.

**Performance**:

This function's runtime is linear in the number of steps taken by the iterator.
 -/
Std.Iter.Partial.count : {α β : Type w} → [inst : Std.Iterator α Id β] → [Std.IteratorLoop α Id Id] → Std.Iter.Partial β → ℕ
-- Mathlib.GroupTheory.EckmannHilton
/-- If a type carries a group structure that distributes over a unital binary operation,
then the group is commutative.  -/
EckmannHilton.commGroup : {X : Type u} →
  {m₁ : X → X → X} →
    {e₁ : X} →
      EckmannHilton.IsUnital m₁ e₁ →
        [G : Group X] → (∀ (a b c d : X), m₁ (a * b) (c * d) = m₁ a c * m₁ b d) → CommGroup X
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Finset.stronglyMeasurable_prod : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousMul M]
  {m : MeasurableSpace α} {ι : Type u_6} {f : ι → α → M} (s : Finset ι),
  (∀ i ∈ s, MeasureTheory.StronglyMeasurable (f i)) → MeasureTheory.StronglyMeasurable (∏ i ∈ s, f i)
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.addAssoc.sizeOf_spec : sizeOf FirstOrder.Field.FieldAxiom.addAssoc = 1
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instIsScalarTower : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {R : Type u_5}
  [inst_2 : Semiring R] [inst_3 : NonUnitalNonAssocSemiring β] [inst_4 : IsTopologicalSemiring β] [inst_5 : Module R β]
  [inst_6 : ContinuousConstSMul R β] [IsScalarTower R β β],
  IsScalarTower R (CompactlySupportedContinuousMap α β) (CompactlySupportedContinuousMap α β)
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.types_comp : ∀ {X Y Z : Type u} (f : X ⟶ Y) (g : Y ⟶ Z),
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.anyM_toArray : ∀ {α β : Type w} {m : Type → Type w'} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m] {it : Std.Iter β} {p : β → m Bool},
  Array.anyM p it.toArray = Std.Iter.anyM p it
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.rightUnitor_comp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.comp f g)).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.id c)).hom
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.rightUnitor g).hom)
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.instIsScalarTower_1 : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  IsScalarTower R (AdicCompletion I R) (AdicCompletion I M)
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.threeShortAddTwoLong.eq_1 : ∀ {ι : 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)
  [inst_5 : P.EmbeddedG2],
  RootPairing.EmbeddedG2.threeShortAddTwoLong P =
    (P.reflectionPerm (RootPairing.EmbeddedG2.long P))
      ((P.reflectionPerm (RootPairing.EmbeddedG2.short P)) (RootPairing.EmbeddedG2.long P))
-- Mathlib.Algebra.Group.Ext
LeftCancelMonoid.ext : ∀ {M : Type u} ⦃m₁ m₂ : LeftCancelMonoid M⦄, HMul.hMul = HMul.hMul → m₁ = m₂
-- Init.Data.List.Sublist
_private.Init.Data.List.Sublist.0.List.isSublist.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (hd₁ : α) (tl₁ : List α) (hd₂ : α) (tl₂ : List α)
  (h_1 : (x : List α) → motive [] x) (h_2 : (x : List α) → motive x [])
  (h_3 :
    (l₁ : List α) →
      (hd₁ : α) → (tl₁ : List α) → l₁ = hd₁ :: tl₁ → (hd₂ : α) → (tl₂ : List α) → motive (hd₁ :: tl₁) (hd₂ :: tl₂)),
  (match hd₁ :: tl₁, hd₂ :: tl₂ with
    | [], x => h_1 x
    | x, [] => h_2 x
    | l₁@h:(hd₁ :: tl₁), hd₂ :: tl₂ => h_3 l₁ hd₁ tl₁ h hd₂ tl₂) =
    h_3 (hd₁ :: tl₁) hd₁ tl₁ ⋯ hd₂ tl₂
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.forall : ∀ {α : Type u_1} {p : CategoryTheory.Discrete α → Prop},
  (∀ (a : CategoryTheory.Discrete α), p a) ↔ ∀ (a' : α), p { as := a' }
-- Batteries.Data.AssocList
Batteries.instInhabitedAssocList : {a : Type u_1} → {a_1 : Type u_2} → Inhabited (Batteries.AssocList a a_1)
-- Mathlib.NumberTheory.NumberField.Units.Regulator
NumberField.Units.regOfFamily_of_isMaxRank : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  {u : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ} (hu : NumberField.Units.IsMaxRank u),
  NumberField.Units.regOfFamily u =
    ZLattice.covolume (Submodule.span ℤ (Set.range ⇑(NumberField.Units.basisOfIsMaxRank hu))) MeasureTheory.volume
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.instZeroHom : {R : Type u} → [inst : Semiring R] → {M N : SemimoduleCat R} → Zero (M ⟶ N)
-- Mathlib.Analysis.Calculus.DiffContOnCl
Differentiable.comp_diffContOnCl : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {g : G → E} {t : Set G},
  Differentiable 𝕜 f → DiffContOnCl 𝕜 g t → DiffContOnCl 𝕜 (f ∘ g) t
-- Mathlib.Data.Nat.Cast.Defs
Nat.cast_zero : ∀ {R : Type u_1} [inst : AddMonoidWithOne R], ↑0 = 0
-- Mathlib.Tactic.FieldSimp
/-- Given a proof of the nonzeroness, strict positivity, etc. (as specified by the value of
`DenomCondition`) of a field-simp-normal-form expression `L` (a product of powers of atoms),
construct a corresponding proof for `((r, e), i) :: L`.

In this version we also expose the proof of nonzeroness of `e`.  -/
Mathlib.Tactic.FieldSimp.mkDenomConditionProofSucc : {v : Lean.Level} →
  {M : Q(Type v)} →
    {iM : Q(CommGroupWithZero «$M»)} →
      ({u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) →
        {cond : Mathlib.Tactic.FieldSimp.DenomCondition q(inferInstance)} →
          {L : Mathlib.Tactic.FieldSimp.qNF M} →
            Mathlib.Tactic.FieldSimp.DenomCondition.proof L cond →
              (e : Q(«$M»)) →
                (r : ℤ) →
                  (i : ℕ) →
                    Lean.MetaM (Q(«$e» ≠ 0) × Mathlib.Tactic.FieldSimp.DenomCondition.proof (((r, e), i) :: L) cond)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.isUnramified_or_isRamified : ∀ (k : Type u_1) [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
  (w : NumberField.InfinitePlace K),
  NumberField.InfinitePlace.IsUnramified k w ∨ NumberField.InfinitePlace.IsRamified k w
-- Mathlib.LinearAlgebra.TensorPower.Basic
TensorPower.cast_cast : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {i j k : ℕ}
  (h : i = j) (h' : j = k) (a : TensorPower R i M),
  (TensorPower.cast R M h') ((TensorPower.cast R M h) a) = (TensorPower.cast R M ⋯) a
-- Mathlib.Order.Closure
ClosureOperator.isClosed_closure : ∀ {α : Type u_1} [inst : Preorder α] (c : ClosureOperator α) (x : α), c.IsClosed (c x)
-- Lean.Elab.Term.TermElabM
/-- When `true` we skip TC failures. We use this option when processing patterns.  -/
Lean.Elab.Term.Context.ignoreTCFailures : Lean.Elab.Term.Context → Bool
-- Mathlib.Topology.MetricSpace.DilationEquiv
IsometryEquiv.toDilationEquiv_symm : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (e : X ≃ᵢ Y),
  e.symm.toDilationEquiv = e.toDilationEquiv.symm
-- Mathlib.Algebra.Order.Group.Synonym
ofDual_vadd : ∀ {β : Type u_2} {α : Type u_1} [inst : VAdd β α] (b : β) (a : αᵒᵈ), OrderDual.ofDual (b +ᵥ a) = b +ᵥ OrderDual.ofDual a
-- Mathlib.Probability.Kernel.Composition.MeasureComp
MeasureTheory.Measure.instSFiniteBindCoeKernelOfIsSFiniteKernel : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ],
  MeasureTheory.SFinite (μ.bind ⇑κ)
-- Mathlib.Topology.LocallyFinsupp
/-- Represent a function (of locally finite support) that in fact has finite support as a `finsum` of
singleton indicator functions.
 -/
Function.locallyFinsuppWithin.sum_apply_smul_single_eq_self_on_univ : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : DecidableEq X] {D : Function.locallyFinsupp X ℤ}
  (h : (Function.locallyFinsuppWithin.support D).Finite),
  ∑ z ∈ h.toFinset, Function.locallyFinsuppWithin.single z (D z) = D
-- Lean.Parser.Extra
Lean.Parser.suppressInsideQuot.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.Data.Set.Lattice
Set.iInter_subtype : ∀ {α : Type u_1} {β : Type u_2} (p : α → Prop) (s : { x // p x } → Set β), ⋂ x, s x = ⋂ x, ⋂ (hx : p x), s ⟨x, hx⟩
-- Mathlib.LinearAlgebra.Matrix.Transvection
/-- Associating to a `transvection_struct` the corresponding transvection matrix.  -/
Matrix.TransvectionStruct.toMatrix : {n : Type u_1} → {R : Type u₂} → [DecidableEq n] → [CommRing R] → Matrix.TransvectionStruct n R → Matrix n n R
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instZero : {E : Type u_5} →
  {F : Type u_6} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] → [inst_2 : NormedAddCommGroup F] → [inst_3 : NormedSpace ℝ F] → Zero (SchwartzMap E F)
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁)
  (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃)
  (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
  (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f),
  CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).hom
      (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ ⋯).hom) =
    CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃))
        (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` is continuous
from the left or from the right at `b`, then `u ↦ ∫ x in a..u, f x` has left (resp., right)
derivative `f b` at `b`.  -/
intervalIntegral.integral_hasDerivWithinAt_right : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b →
    ∀ {s t : Set ℝ} [intervalIntegral.FTCFilter b (nhdsWithin b s) (nhdsWithin b t)],
      StronglyMeasurableAtFilter f (nhdsWithin b t) MeasureTheory.volume →
        ContinuousWithinAt f t b → HasDerivWithinAt (fun u => ∫ (x : ℝ) in a..u, f x) (f b) s b
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.alternatingSum_cons' : ∀ {G : Type u_7} [inst : AddCommGroup G] (a : G) (l : List G), (a :: l).alternatingSum = a + -l.alternatingSum
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.natDegree_derivative : ∀ {R : Type u} [inst : Semiring R] [IsAddTorsionFree R] (p : Polynomial R),
  (Polynomial.derivative p).natDegree = p.natDegree - 1
-- Mathlib.NumberTheory.Divisors
Nat.mem_divisors : ∀ {n m : ℕ}, n ∈ m.divisors ↔ n ∣ m ∧ m ≠ 0
-- Std.Async.TCP
/-- Enables TCP keep-alive with a specified delay for the client socket.
 -/
Std.Async.TCP.Socket.Client.keepAlive : Std.Async.TCP.Socket.Client →
  Bool →
    (delay : Std.Time.Second.Offset) → autoParam (delay.val ≥ 0) Std.Async.TCP.Socket.Client.keepAlive._auto_1 → IO Unit
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsClosedSubgraph.adj_congr : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {G H : Graph α β},
  x ∈ H.vertexSet → H.IsClosedSubgraph G → (H.Adj x y ↔ G.Adj x y)
-- Mathlib.CategoryTheory.Limits.Creates
/-- a cone in the source category of the functor  -/
CategoryTheory.LiftableCone.liftedCone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                {c : CategoryTheory.Limits.Cone (K.comp F)} →
                  CategoryTheory.LiftableCone K F c → CategoryTheory.Limits.Cone K
-- Mathlib.Data.List.Basic
List.filter_eq_foldr : ∀ {α : Type u} (p : α → Bool) (l : List α),
  List.filter p l = List.foldr (fun a out => bif p a then a :: out else out) [] l
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.maxEntry?.eq_1 : ∀ {α : Type u} {β : Type v}, Std.DTreeMap.Internal.Impl.Const.maxEntry? Std.DTreeMap.Internal.Impl.leaf = none
-- Mathlib.Order.Irreducible
supIrred_iff_not_isMin : ∀ {α : Type u_2} [inst : LinearOrder α] {a : α}, SupIrred a ↔ ¬IsMin a
-- Std.Do.WP.SimpLemmas
Std.Do.WP.throw_lift_ExceptT : ∀ {m : Type u → Type v} {sh : Std.Do.PostShape} {ε ε' α : Type u} {e : ε}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.except ε' sh)} [inst : Std.Do.WP m sh] [Monad m]
  [inst_2 : MonadExceptOf ε m],
  (Std.Do.wp (MonadExceptOf.throw e)).apply Q =
    (Std.Do.wp (MonadExceptOf.throw e)).apply (fun e => Except.casesOn e Q.2.1 Q.1, Q.2.2)
-- Mathlib.RingTheory.Ideal.Over
Ideal.Quotient.ker_stabilizerHom : ∀ {A : Type u_3} {B : Type u_4} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (P : Ideal B)
  (p : Ideal A) [inst_3 : P.LiesOver p] (G : Type u_6) [inst_4 : Group G] [inst_5 : MulSemiringAction G B]
  [inst_6 : SMulCommClass G A B],
  (Ideal.Quotient.stabilizerHom P p G).ker = Ideal.inertia (↥(MulAction.stabilizer G P)) P
-- Lean.Elab.Import
Lean.Elab.printImportSrcs : String → Option String → IO Unit
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.toPoly'.go.eq_5 : ∀ (coeff : ℤ) (k : ℕ) (a : Lean.Grind.Linarith.Expr),
  Lean.Grind.Linarith.Expr.toPoly'.go coeff (Lean.Grind.Linarith.Expr.natMul k a) =
    bif k == 0 then id else Lean.Grind.Linarith.Expr.toPoly'.go (coeff.mul ↑k) a
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
ArithmeticFunction.coe_zeta_mul_apply : ∀ {R : Type u_1} [inst : Semiring R] {f : ArithmeticFunction R} {x : ℕ},
  (↑ArithmeticFunction.zeta * f) x = ∑ i ∈ x.divisors, f i
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isClique_univ : ∀ {α : Type u_1} {G : SimpleGraph α}, G.IsClique Set.univ ↔ G = ⊤
-- Mathlib.RingTheory.HahnSeries.PowerSeries
HahnSeries.ofPowerSeries_injective : ∀ {Γ : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : Semiring Γ] [inst_2 : PartialOrder Γ]
  [inst_3 : IsStrictOrderedRing Γ], Function.Injective ⇑(HahnSeries.ofPowerSeries Γ R)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- The equivalence `LeftExtension L F ≌ LeftExtension L' F` induced by
a natural isomorphism `L ≅ L'`.  -/
CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁ : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            {L L' : CategoryTheory.Functor C D} →
              (L ≅ L') → (F : CategoryTheory.Functor C H) → L.LeftExtension F ≌ L'.LeftExtension F
-- Mathlib.Algebra.LinearRecurrence
/-- The function that maps a solution `u` of `E` to its first
`E.order` terms as a `LinearEquiv`.  -/
LinearRecurrence.toInit : {R : Type u_1} → [inst : CommSemiring R] → (E : LinearRecurrence R) → ↥E.solSpace ≃ₗ[R] Fin E.order → R
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.map_s : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] {S : CategoryTheory.ShortComplex C} (s : S.Splitting)
  (F : CategoryTheory.Functor C D) [inst_4 : F.Additive], (s.map F).s = F.map s.s
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.left_U_subset_right_C : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (c : Urysohns.CU P), c.left.U ⊆ c.right.C
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.functorL₀_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y),
  CategoryTheory.ShortComplex.SnakeInput.functorL₀.map f = f.f₀
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.tendsto_atTop_sumCoeffsExp : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r), Filter.Tendsto (fun p => ∑ i, a i * b i ^ p) Filter.atBot Filter.atTop
-- Lean.Meta.AppBuilder
Lean.Meta.mkForallCongr : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.point_notMem_finset_logSizeBallSeq_add_one : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [inst_1 : DecidableEq T] (hJ : J.Nonempty)
  (i : ℕ), (PairReduction.logSizeBallSeq J hJ a c i).point ∉ (PairReduction.logSizeBallSeq J hJ a c (i + 1)).finset
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instNeg.eq_1 : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Neg G] [inst_2 : ContinuousNeg G],
  SeparationQuotient.instNeg = { neg := Quotient.map' (fun x => -x) ⋯ }
-- Lean.Log
/-- Return the current reference syntax being used to provide position information.  -/
Lean.MonadLog.getRef : {m : Type → Type} → [self : Lean.MonadLog m] → m Lean.Syntax
-- Std.Data.DTreeMap.Internal.Model
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.applyCell_eq_applyPartition : ∀ {α : Type u} {β : α → Type v} {δ : Type w} [inst : Ord α] (k : α) (l : Std.DTreeMap.Internal.Impl α β)
  (f :
    (c : Std.DTreeMap.Internal.Cell α β (compare k)) →
      (Std.DTreeMap.Internal.Impl.contains' (compare k) l = true → c.contains = true) → δ),
  Std.DTreeMap.Internal.Impl.applyCell k l f =
    Std.DTreeMap.Internal.Impl.applyPartition (compare k) l fun x c hc x_1 => f c hc
-- Batteries.Data.List.Lemmas
List.length_tail_add_one : ∀ {α : Type u_1} (l : List α), 0 < l.length → l.tail.length + 1 = l.length
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.tr_ret_cons₂ : ∀ (k : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.ret k.cons₂) =
    Turing.TM2.Stmt.goto fun x => Turing.PartrecToTM2.head Turing.PartrecToTM2.K'.stack (Turing.PartrecToTM2.Λ'.ret k)
-- Init.Control.Lawful.Basic
Id.run_bind : ∀ {α β : Type u_1} (x : Id α) (f : α → Id β), (x >>= f).run = (f x.run).run
-- Mathlib.CategoryTheory.Profunctor.Basic
/-- Whisker a profunctor from `C` to `D` with functors into `C` and `D`.  -/
CategoryTheory.Profunctor.whiskerLeft₂ : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {A : Type u_1} →
          {B : Type u_2} →
            [inst_2 : CategoryTheory.Category.{v_1, u_1} A] →
              [inst_3 : CategoryTheory.Category.{v_2, u_2} B] →
                CategoryTheory.Profunctor.{w, v₁, v₂, u₁, u₂} C D →
                  CategoryTheory.Functor A C →
                    CategoryTheory.Functor B D → CategoryTheory.Profunctor.{w, v_1, v_2, u_1, u_2} A B
-- Mathlib.Topology.MetricSpace.Holder
HolderWith.nndist_le_of_le : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoMetricSpace X] [inst_1 : PseudoMetricSpace Y] {C r : NNReal} {f : X → Y},
  HolderWith C r f → ∀ {x y : X} {d : NNReal}, nndist x y ≤ d → nndist (f x) (f y) ≤ C * d ^ ↑r
-- Mathlib.Data.Finsupp.Lex
Finsupp.Colex.single_lt_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, ((toColex fun₀ | a => 1) < toColex fun₀ | b => 1) ↔ a < b
-- Mathlib.LinearAlgebra.Span.Basic
LinearMap.toSpanSingleton_apply : ∀ (R : Type u_1) (M : Type u_4) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M) (b : R),
  (LinearMap.toSpanSingleton R M x) b = b • x
-- Mathlib.Order.Filter.Extr
/-- If `f` is antitone on `Ioc a b` and monotone on `Icc b c`, then the minimum of `f` on
`Ioc a c` is attained at `b`.  -/
isMinOn_Ioc_of_anti_mono : ∀ {α : Type u} {β : Type u_1} [inst : LinearOrder α] [inst_1 : Preorder β] {a b c : α} {f : α → β},
  AntitoneOn f (Set.Ioc a b) → MonotoneOn f (Set.Icc b c) → IsMinOn f (Set.Ioc a c) b
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.one_lt_card : ∀ {o : Ordinal.{u_1}}, 1 < o.card ↔ 1 < o
-- Mathlib.CategoryTheory.Retract
CategoryTheory.Retract.splitEpi.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Retract X Y),
  h.splitEpi = { section_ := h.i, id := ⋯ }
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
EisensteinSeries.gammaSet.eq_1 : ∀ (N r : ℕ) (a : Fin 2 → ZMod N), EisensteinSeries.gammaSet N r a = {v | Int.cast ∘ v = a ∧ (v 0).gcd (v 1) = r}
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch.needlePos_le_stackPos : ∀ {pat s : ByteArray} {needlePos stackPos : ℕ},
  String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat s needlePos stackPos → needlePos ≤ stackPos
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
tendsto_log_div_rpow_nhdsGT_zero : ∀ {r : ℝ}, r < 0 → Filter.Tendsto (fun x => Real.log x / x ^ r) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
-- Mathlib.Logic.Equiv.Basic
/-- Let `f : α → β` be a function on index types. A family of equivalences, indexed by `b : β`,
between the product over the fiber of `b` under `f` given as
`∀ (σ : { a : α // f a = b }) → γ₁ σ.1) ≃ γ₂ b` lifts to an equivalence over the products
`∀ a, γ₁ a ≃ ∀ b, γ₂ b`.  -/
Equiv.piCongrFiberwise : {α : Type u_9} →
  {β : Type u_10} →
    {γ₁ : α → Type u_11} →
      {γ₂ : β → Type u_12} →
        {f : α → β} → ((b : β) → ((σ : { a // f a = b }) → γ₁ ↑σ) ≃ γ₂ b) → ((a : α) → γ₁ a) ≃ ((b : β) → γ₂ b)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cocycle.equivHomShift'_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (n m : ℤ) (h : m + n = 0)
  (a : (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K ⟶ L),
  (CochainComplex.HomComplex.Cocycle.equivHomShift' n m h) a =
    (CochainComplex.HomComplex.Cocycle.ofHom a).leftUnshift m h