mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.Subring.Basic
/-- Restriction of a ring homomorphism to its range interpreted as a subsemiring.

This is the bundled version of `Set.rangeFactorization`.  -/
RingHom.rangeRestrict : {R : Type u} → {S : Type v} → [inst : NonAssocRing R] → [inst_1 : NonAssocRing S] → (f : R →+* S) → R →+* ↥f.range
-- Init.Data.String.Basic
ByteArray.utf8Decode?_empty : ByteArray.empty.utf8Decode? = some #[]
-- Mathlib.Probability.Kernel.Disintegration.Unique
/-- An s-finite kernel which satisfies the disintegration property of the given measure `ρ` is
almost everywhere equal to the disintegration kernel of `ρ` when evaluated on a measurable set.

This theorem in the case of finite kernels is weaker than `eq_condKernel_of_measure_eq_compProd`
which asserts that the kernels are equal almost everywhere and not just on a given measurable
set.  -/
ProbabilityTheory.eq_condKernel_of_measure_eq_compProd' : ∀ {α : Type u_1} {Ω : Type u_3} {mα : MeasurableSpace α} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {ρ : MeasureTheory.Measure (α × Ω)} [inst_3 : MeasureTheory.IsFiniteMeasure ρ]
  (κ : ProbabilityTheory.Kernel α Ω) [ProbabilityTheory.IsSFiniteKernel κ],
  ρ = ρ.fst.compProd κ → ∀ {s : Set Ω}, MeasurableSet s → ∀ᵐ (x : α) ∂ρ.fst, (κ x) s = (ρ.condKernel x) s
-- Mathlib.Topology.Inseparable
instTopologicalSpaceSeparationQuotient : (X : Type u_1) → [inst : TopologicalSpace X] → TopologicalSpace (SeparationQuotient X)
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.isMillerPatternArgs.go : Lean.Expr → ℕ → Lean.LocalContext → Lean.Expr → Bool
-- Lean.Meta.DiscrTree.Util
/-- Monadically fold the values stored in a `Trie`.
 -/
Lean.Meta.DiscrTree.Trie.foldValuesM : {m : Type u_1 → Type u_2} →
  {σ : Type u_1} → {α : Type} → [Monad m] → (σ → α → m σ) → σ → Lean.Meta.DiscrTree.Trie α → m σ
-- Mathlib.Topology.Algebra.UniformConvergence
instNSMulUniformOnFun : {α : Type u_1} → {β : Type u_2} → {𝔖 : Set (Set α)} → {M : Type u_5} → [SMul M β] → SMul M (UniformOnFun α β 𝔖)
-- Lean.Parser.Term
Lean.Parser.Term.binrel_no_prop.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.CotangentSpace.map_comp_apply : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u'} {S' : Type v'} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] [inst_8 : Algebra R S']
  [inst_9 : IsScalarTower R R' S'] {R'' : Type u''} {S'' : Type v''} [inst_10 : CommRing R''] [inst_11 : CommRing S'']
  [inst_12 : Algebra R'' S''] {P'' : Algebra.Extension R'' S''} [inst_13 : Algebra R R''] [inst_14 : Algebra S S'']
  [inst_15 : Algebra R S''] [inst_16 : IsScalarTower R R'' S''] [inst_17 : Algebra R' R''] [inst_18 : Algebra S' S'']
  [inst_19 : Algebra R' S''] [inst_20 : IsScalarTower R' R'' S''] [inst_21 : IsScalarTower R R' R'']
  [inst_22 : IsScalarTower S S' S''] (f : P.Hom P') (g : P'.Hom P'') (x : P.CotangentSpace),
  (Algebra.Extension.CotangentSpace.map (g.comp f)) x =
    (Algebra.Extension.CotangentSpace.map g) ((Algebra.Extension.CotangentSpace.map f) x)
-- Init.Data.String.Termination
String.Pos.Down.mk : {s : String} → s.Pos → String.Pos.Down s
-- Mathlib.NumberTheory.Harmonic.EulerMascheroni
/-- The Euler-Mascheroni constant `γ`.  -/
Real.eulerMascheroniConstant : ℝ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_of_mem_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t.keysArray → k ∈ t
-- Mathlib.Data.Matrix.Block
Matrix.vecMul_fromBlocks : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [inst : Fintype n] [inst_1 : Fintype o]
  [inst_2 : NonUnitalNonAssocSemiring α] (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α)
  (x : n ⊕ o → α),
  Matrix.vecMul x (Matrix.fromBlocks A B C D) =
    Sum.elim (Matrix.vecMul (x ∘ Sum.inl) A + Matrix.vecMul (x ∘ Sum.inr) C)
      (Matrix.vecMul (x ∘ Sum.inl) B + Matrix.vecMul (x ∘ Sum.inr) D)
-- Mathlib.Analysis.Normed.Module.Ray
norm_injOn_ray_left : ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {x : F},
  x ≠ 0 → Set.InjOn norm {y | SameRay ℝ x y}
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.idemSnd_compl : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedAddCommGroup α] [inst_1 : SeminormedAddCommGroup β] {p : ENNReal},
  1 - WithLp.idemSnd = WithLp.idemFst
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.add_of_X_ne' : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₁ x₂ y₁ y₂ : F}
  {h₁ : W.Nonsingular x₁ y₁} {h₂ : W.Nonsingular x₂ y₂} (hx : x₁ ≠ x₂),
  WeierstrassCurve.Affine.Point.some x₁ y₁ h₁ + WeierstrassCurve.Affine.Point.some x₂ y₂ h₂ =
    -WeierstrassCurve.Affine.Point.some (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
        ⋯
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : LawfulBEq α]
  [inst_1 : Inhabited γ] {f : α → β → γ} {k : α}, (Std.ExtHashMap.map f m)[k]! = (Option.map (f k) m[k]?).get!
-- Mathlib.Order.WellFoundedSet
Set.WellFoundedOn.prod_lex_of_wellFoundedOn_fiber : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {rα : α → α → Prop} {rβ : β → β → Prop} {f : γ → α} {g : γ → β}
  {s : Set γ},
  s.WellFoundedOn (Function.onFun rα f) →
    (∀ (a : α), (s ∩ f ⁻¹' {a}).WellFoundedOn (Function.onFun rβ g)) →
      s.WellFoundedOn (Function.onFun (Prod.Lex rα rβ) fun c => (f c, g c))
-- Mathlib.NumberTheory.LucasLehmer
/-- The recurrence `s (i+1) = (s i)^2 - 2` in `ZMod (2^p - 1)`.  -/
LucasLehmer.sZMod : (p : ℕ) → ℕ → ZMod (2 ^ p - 1)
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.s.eq_def : ∀ (x : ℕ),
  LucasLehmer.s x =
    match x with
    | 0 => 4
    | i.succ => LucasLehmer.s i ^ 2 - 2
-- Mathlib.GroupTheory.Coset.Basic
AddSubgroup.quotientiInfAddSubgroupOfEmbedding.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α) (H : AddSubgroup α),
  AddSubgroup.quotientiInfAddSubgroupOfEmbedding f H =
    { toFun := fun q i => AddSubgroup.quotientAddSubgroupOfMapOfLE H ⋯ q, inj' := ⋯ }
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- The categorical data that is involved in a `0`-hypercover of an object `S`. This
consists of a family of morphisms `f i : X i ⟶ S` for `i : I₀`.  -/
CategoryTheory.PreZeroHypercover : {C : Type u} → [CategoryTheory.Category.{v, u} C] → C → Type (max (max u v) (w + 1))
-- Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
MvPowerSeries.instNoZeroDivisors : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] [NoZeroDivisors R], NoZeroDivisors (MvPowerSeries σ R)
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.length_one : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W), cs.length 1 = 0
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.ofArchimedean_stdPart : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] {x : K} (f : ℝ →+*o K)
  (hx : 0 ≤ ArchimedeanClass.mk x),
  (ArchimedeanClass.FiniteResidueField.ofArchimedean f) (ArchimedeanClass.stdPart x) =
    ArchimedeanClass.FiniteResidueField.mk (ArchimedeanClass.FiniteElement.mk x hx)
-- Mathlib.GroupTheory.OreLocalization.OreSet
/-- The Ore denominator of a fraction.  -/
OreLocalization.OreSet.oreDenom : {R : Type u_1} → {inst : Monoid R} → {S : Submonoid R} → [self : OreLocalization.OreSet S] → R → ↥S → ↥S
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- The heterobasic version of `mk` coincides with the regular version.  -/
TensorProduct.AlgebraTensorModule.mk_eq : ∀ {R : Type uR} {M : Type uM} {N : Type uN} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N],
  TensorProduct.AlgebraTensorModule.mk R R M N = TensorProduct.mk R M N
-- Init.Data.Iterators.Combinators.Monadic.Attach
Std.Iterators.Types.Attach.inner : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} → [inst : Std.Iterator α m β] → {P : β → Prop} → Std.Iterators.Types.Attach α m P → Std.IterM m β
-- Init.Data.SInt.Lemmas
Int16.le_or_lt : ∀ (a b : Int16), a ≤ b ∨ b < a
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.orderIsoMapComapOfBijective_symm_apply : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (hf : Function.Bijective ⇑f) (p : Submodule R₂ M₂),
  (RelIso.symm (Submodule.orderIsoMapComapOfBijective f hf)) p = Submodule.comap f p
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_modify : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : β k → β k}, (m.modify k f).size = m.size
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.xn_add : ∀ {a : ℕ} (a1 : 1 < a) (m n : ℕ),
  Pell.xn a1 (m + n) = Pell.xn a1 m * Pell.xn a1 n + Pell.d✝ a1 * Pell.yn a1 m * Pell.yn a1 n
-- Init.Data.Array.Find
_private.Init.Data.Array.Find.0.Array.of_findIdx?_eq_some.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match some a with
    | some a => h_1 a
    | none => h_2 ()) =
    h_1 a
-- Mathlib.Data.Nat.Factorization.Root
Nat.floorRoot_zero_right : ∀ (n : ℕ), n.floorRoot 0 = 0
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.add_seq : ∀ {α β : Type u} (f g : FreeAbelianGroup (α → β)) (x : FreeAbelianGroup α), f + g <*> x = (f <*> x) + (g <*> x)
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBMap.alter.adapt.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((v : β) → motive (some v)) → motive x
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.symm_mapDomainAddEquiv : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Add M] [inst_2 : Add N] (e : M ≃ N),
  (AddMonoidAlgebra.mapDomainAddEquiv R e).symm = AddMonoidAlgebra.mapDomainAddEquiv R e.symm
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.contains_filterMap!_iff : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [Std.TransOrd α] {f : α → β → Option γ} {k : α},
  t.WF →
    (Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.filterMap! f t) = true ↔
      ∃ (h' : Std.DTreeMap.Internal.Impl.contains k t = true),
        (f (t.getKey k h') (Std.DTreeMap.Internal.Impl.Const.get t k h')).isSome = true)
-- Init.TacticsExtra
/-- `iterate n tac` runs `tac` exactly `n` times.
`iterate tac` runs `tac` repeatedly until failure.

`iterate`'s argument is a tactic sequence,
so multiple tactics can be run using `iterate n (tac₁; tac₂; ⋯)` or
```lean
iterate n
  tac₁
  tac₂
  ⋯
```
 -/
Lean.Parser.Tactic.tacticIterate____ : Lean.ParserDescr
-- Mathlib.Data.NNRat.Defs
NNRat.nonpos_iff_eq_zero : ∀ (q : ℚ≥0), q ≤ 0 ↔ q = 0
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.singleton_mul : ∀ {α : Type u_2} [inst : Mul α] [inst_1 : DecidableEq α] {s : Finset α} (a : α), {a} * s = a • s
-- Mathlib.Topology.UniformSpace.Equicontinuity
UniformFun.topologicalSpace.eq_1 : ∀ (α : Type u_1) (β : Type u_2) [inst : UniformSpace β], UniformFun.topologicalSpace α β = inferInstance
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.coe_list_prod : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] (s : List (Finset α)),
  ↑s.prod = (List.map SetLike.coe s).prod
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_zero_succ : ∀ (k : ℕ), Nat.choose 0 k.succ = 0
-- Mathlib.RingTheory.UniqueFactorizationDomain.Moebius
UniqueFactorizationMonoid.moebius_zero : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] [Nontrivial α],
  UniqueFactorizationMonoid.moebius 0 = 0
-- Mathlib.NumberTheory.Dioph
Poly.instSub : {α : Type u_1} → Sub (Poly α)
-- Init.Data.String.Substring
/-- Retains only the longest suffix of a substring in which a Boolean predicate returns `true` for all
characters by moving the substring's start position towards its end position.
 -/
Substring.Raw.takeRightWhile : Substring.Raw → (Char → Bool) → Substring.Raw
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.kernelSequenceCycles_X₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceCycles._auto_1),
  (X.kernelSequenceCycles f g n₀ n₁ hn₁).X₁ = X.cycles f g n₀
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
subset_Icc_csInf_csSup : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α},
  BddBelow s → BddAbove s → s ⊆ Set.Icc (sInf s) (sSup s)
-- Std.Internal.Do.Order.Basic
/-- Pointwise characterization of `CompleteLattice.sup` on function lattices:
`(sup c) s = sup (fun y => ∃ f, c f ∧ f s = y)`.  -/
Lean.Order.sup_apply : ∀ {σ : Type v} {β : σ → Type w} [inst : (s : σ) → Lean.Order.CompleteLattice (β s)] (c : ((s : σ) → β s) → Prop)
  (s : σ), Lean.Order.CompleteLattice.sup c s = Lean.Order.CompleteLattice.sup fun y => ∃ f, c f ∧ f s = y
-- Mathlib.Order.Height
Set.chainHeight_flip : ∀ {α : Type u_1} (s : Set α) (r : α → α → Prop), s.chainHeight (flip r) = s.chainHeight r
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getEntryGT?.go.match_1.eq_2 : ∀ (motive : Ordering → Sort u_1) (x : Ordering) (h_1 : Unit → motive Ordering.lt) (h_2 : (x : Ordering) → motive x),
  (x = Ordering.lt → False) →
    (match x with
      | Ordering.lt => h_1 ()
      | x => h_2 x) =
      h_2 x
-- Std.Async.Basic
Std.Async.MaybeTask.pure.injEq : ∀ {α : Type} (a a_1 : α), (Std.Async.MaybeTask.pure a = Std.Async.MaybeTask.pure a_1) = (a = a_1)
-- Mathlib.LinearAlgebra.TensorProduct.Map
/-- Given submodules `p ⊆ P` and `q ⊆ Q`, this is the natural map: `p ⊗ q → P ⊗ Q`.  -/
TensorProduct.mapIncl : {R : Type u_1} →
  [inst : CommSemiring R] →
    {P : Type u_9} →
      {Q : Type u_10} →
        [inst_1 : AddCommMonoid P] →
          [inst_2 : AddCommMonoid Q] →
            [inst_3 : Module R P] →
              [inst_4 : Module R Q] →
                (p : Submodule R P) → (q : Submodule R Q) → TensorProduct R ↥p ↥q →ₗ[R] TensorProduct R P Q
-- Mathlib.Algebra.Group.Semiconj.Basic
/-- **Alias** of the reverse direction of `SemiconjBy.inv_right_iff`. -/
SemiconjBy.inv_right : ∀ {G : Type u_1} [inst : Group G] {a x y : G}, SemiconjBy a x y → SemiconjBy a x⁻¹ y⁻¹
-- Mathlib.LinearAlgebra.AffineSpace.Slope
slope_vadd_const : ∀ {k : Type u_1} {E : Type u_2} {PE : Type u_3} [inst : Field k] [inst_1 : AddCommGroup E] [inst_2 : Module k E]
  [inst_3 : AddTorsor E PE] (f : k → E) (c : PE), (slope fun x => f x +ᵥ c) = slope f
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.any_eq_not_all_not : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {p : (a : α) → β a → Bool},
  (↑m).any p = !(↑m).all fun a b => !p a b
-- Batteries.Data.BitVec.Basic
/-- `ofFnBE f` returns the `BitVec n` whose `i`th bit is `f i` with big endian ordering.  -/
BitVec.ofFnBE : {n : ℕ} → (Fin n → Bool) → BitVec n
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.id_tensorHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C)
  {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂),
  CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X) f =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.restrict_biInf : ∀ {α : Type u_1} {ι : Type u_2} {I : Set ι},
  I.Nonempty →
    ∀ (s : Set α) (m : ι → MeasureTheory.OuterMeasure α),
      (MeasureTheory.OuterMeasure.restrict s) (⨅ i ∈ I, m i) = ⨅ i ∈ I, (MeasureTheory.OuterMeasure.restrict s) (m i)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.sinh_add_pi_mul_I : ∀ (z : ℂ), Complex.sinh (z + ↑Real.pi * Complex.I) = -Complex.sinh z
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- How to present the basic measure in the table header, possibly abbreviated.  -/
Lean.Elab.WF.GuessLex.measureHeader : Lean.Elab.WF.GuessLex.BasicMeasure → StateT (ℕ × String) Lean.MetaM String
-- Lean.Linter.Deprecated
Lean.Linter.DeprecationEntry : Type
-- Mathlib.Data.Set.Monotone
strictMonoOn_insert_iff_of_forall_le : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α} {a : α},
  (∀ x ∈ s, x ≤ a) → (StrictMonoOn f (insert a s) ↔ (∀ b ∈ s, b < a → f b < f a) ∧ StrictMonoOn f s)
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instOne.eq_1 : ∀ {α : Type u_1} [inst : One α], Lex.instOne = inst
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
ContDiffPointwiseHolderAt.prodMk : ∀ {E : Type u_1} {F : Type u_2} {G : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  {k : ℕ} {α : ↑unitInterval} {f : E → F} {a : E} {g : E → G},
  ContDiffPointwiseHolderAt k α f a →
    ContDiffPointwiseHolderAt k α g a → ContDiffPointwiseHolderAt k α (fun x => (f x, g x)) a
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.toCocycles_comp_isoCocycles₁_hom_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : ModuleCat.of k ↥(groupCohomology.cocycles₁ A) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupCohomology.toCocycles A 0 1)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.isoCocycles₁ A).hom h) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₀ A).hom
      (CategoryTheory.CategoryStruct.comp (groupCohomology.shortComplexH1 A).moduleCatLeftHomologyData.f' h)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Class
Std.Tactic.BVDecide.LRAT.Internal.Formula.rupAdd_result : ∀ {α : outParam (Type u)} {β : outParam (Type v)} {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} {σ : Type w}
  {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ]
  (f : σ) (c : β) (rupHints : Array ℕ) (f' : σ),
  Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd f →
    Std.Tactic.BVDecide.LRAT.Internal.Formula.performRupAdd f c rupHints = (f', true) →
      f' = Std.Tactic.BVDecide.LRAT.Internal.Formula.insert f c
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
/-- [Stacks Tag 0CKM](https://stacks.math.columbia.edu/tag/0CKM) -/
linearIndependent_algHom_toLinearMap : ∀ (K : Type u_6) (M : Type u_7) (L : Type u_8) [inst : CommSemiring K] [inst_1 : Semiring M] [inst_2 : Algebra K M]
  [inst_3 : CommRing L] [IsDomain L] [inst_5 : Algebra K L], LinearIndependent L AlgHom.toLinearMap
-- Mathlib.Data.ENNReal.Inv
/-- See `ENNReal.mul_div_cancel` for a simpler version assuming `a ≠ 0`, `a ≠ ∞`.  -/
ENNReal.mul_div_cancel' : ∀ {a b : ENNReal}, (a = 0 → b = 0) → (a = ⊤ → b = 0) → a * (b / a) = b
-- Mathlib.CategoryTheory.Galois.Basic
/-- `C` has finite coproducts (G2).  -/
CategoryTheory.PreGaloisCategory.hasFiniteCoproducts : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{u₂, u₁} C} [self : CategoryTheory.PreGaloisCategory C],
  CategoryTheory.Limits.HasFiniteCoproducts C
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
extChartAt_image_nhds_mem_nhds_of_mem_interior_range : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] {x y : M},
  y ∈ (extChartAt I x).source →
    ↑(extChartAt I x) y ∈ interior (Set.range ↑I) →
      ∀ {s : Set M}, s ∈ nhds y → ↑(extChartAt I x) '' s ∈ nhds (↑(extChartAt I x) y)
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.rightOp : C ⥤ Dᵒᵖ` creates colimits, then `F : Cᵒᵖ ⥤ D` creates limits.  -/
CategoryTheory.Limits.createsLimitsOfRightOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor Cᵒᵖ D) → [CategoryTheory.CreatesColimits F.rightOp] → CategoryTheory.CreatesLimits F
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.Presentation.map_generators_I : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C']
  {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat}
  [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat]
  {M : SheafOfModules R} (P : M.Presentation) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S))
  [inst_6 :
    CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁,
        max (max (u + 1) u₂) v₂}
      F]
  (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)), (P.map F η).generators.I = P.generators.I
-- Mathlib.Combinatorics.Configuration
Configuration.HasLines.existsUnique_line : ∀ (P : Type u_1) (L : Type u_2) [inst : Membership P L] [Configuration.HasLines P L] (p₁ p₂ : P),
  p₁ ≠ p₂ → ∃! l, p₁ ∈ l ∧ p₂ ∈ l
-- Batteries.Data.Random.MersenneTwister
/-- Inner loop for Mersenne Twister initalization.  -/
_private.Batteries.Data.Random.MersenneTwister.0.Batteries.Random.MersenneTwister.Config.init.loop : (cfg : Batteries.Random.MersenneTwister.Config) →
  BitVec cfg.wordSize →
    (v : Array (BitVec cfg.wordSize)) → v.size ≤ cfg.stateSize → Vector (BitVec cfg.wordSize) cfg.stateSize
-- Mathlib.Algebra.Star.CHSH
IsCHSHTuple.B₀_inv : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {A₀ A₁ B₀ B₁ : R}, IsCHSHTuple A₀ A₁ B₀ B₁ → B₀ ^ 2 = 1
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.lintegral_zero : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}, MeasureTheory.AEEqFun.lintegral 0 = 0
-- Std.Data.HashMap.Basic
/-- Checks whether a key is present in a map and inserts a value for the key if it was not found.

If the returned `Bool` is `true`, then the returned map is unaltered. If the `Bool` is `false`, then
the returned map has a new value inserted.

Equivalent to (but potentially faster than) calling `contains` followed by `insertIfNew`.
 -/
Std.HashMap.containsThenInsertIfNew : {α : Type u} → {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → α → β → Bool × Std.HashMap α β
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
intervalIntegral.tsum_intervalIntegral_eq_of_summable_norm : ∀ {ι : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} [Countable ι]
  {f : ι → C(ℝ, E)},
  (Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := Set.uIcc a b, isCompact' := ⋯ }) (f i)‖) →
    ∑' (i : ι), ∫ (x : ℝ) in a..b, (f i) x = ∫ (x : ℝ) in a..b, ∑' (i : ι), (f i) x