mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_sub_intCast : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R) (z : ℤ),
  ⌈a - ↑z⌉ = ⌈a⌉ - z
-- Aesop.Index.RulePattern
/-- The rule's pattern. We assume that there is at most one pattern per
rule.  -/
Aesop.RulePatternIndex.Entry.pattern : Aesop.RulePatternIndex.Entry → Aesop.RulePattern
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_const_zero : ∀ (R : Type u_1) {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] (a : A),
  cfcₙ (fun x => 0) a = 0
-- Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
ordinaryHypergeometric_zero : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : Field 𝕂] [inst_1 : Ring 𝔸] [inst_2 : Algebra 𝕂 𝔸] [inst_3 : TopologicalSpace 𝔸]
  [inst_4 : IsTopologicalRing 𝔸] (a b c : 𝕂), ₂F₁ a b c 0 = 1
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
isCyclic_of_subsingleton : ∀ {α : Type u_1} [inst : Group α] [Subsingleton α], IsCyclic α
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIcc_of_gt : ∀ {α : Type u_1} [inst : Lattice α] {a b : α}, b < a → Set.uIcc a b = Set.Icc b a
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.List.getLast?.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrict_le_restrict_iUnion : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M]
  [inst_2 : PartialOrder M] [IsOrderedAddMonoid M] [OrderClosedTopology M] (v w : MeasureTheory.VectorMeasure α M)
  {f : ℕ → Set α},
  (∀ (n : ℕ), MeasurableSet (f n)) →
    (∀ (n : ℕ), v.restrict (f n) ≤ w.restrict (f n)) → v.restrict (⋃ n, f n) ≤ w.restrict (⋃ n, f n)
-- Mathlib.Algebra.Ring.Invertible
/-- A version of `inv_add_inv'` for `Ring.inverse`.  -/
Ring.inverse_add_inverse : ∀ {R : Type u_1} [inst : Semiring R] {a b : R},
  (IsUnit a ↔ IsUnit b) → Ring.inverse a + Ring.inverse b = Ring.inverse a * (a + b) * Ring.inverse b
-- Mathlib.Order.Interval.Set.Image
Monotone.image_Iic_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {b : α},
  Monotone f → f '' Set.Iic b ⊆ Set.Iic (f b)
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.uliftEquiv_tmul : ∀ (R : Type u_4) (S : Type u_5) {A : Type u_6} {B : Type u_7} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B] (a : A) (b : B),
  (Algebra.TensorProduct.uliftEquiv R S A B) { down := a ⊗ₜ[R] b } = { down := a } ⊗ₜ[ULift.{u_10, u_4} R] { down := b }
-- Mathlib.RingTheory.Smooth.AdicCompletion
_private.Mathlib.RingTheory.Smooth.AdicCompletion.0.Algebra.FormallySmooth.liftAdicCompletionAux.congr_simp : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {S : Type u_3}
  [inst_3 : CommRing S] [inst_4 : Algebra R S] (I : Ideal S) (f f_1 : A →ₐ[R] S ⧸ I),
  f = f_1 →
    ∀ [inst_5 : Algebra.FormallySmooth R A] (m : ℕ),
      Algebra.FormallySmooth.liftAdicCompletionAux✝ I f m = Algebra.FormallySmooth.liftAdicCompletionAux✝ I f_1 m
-- Mathlib.CategoryTheory.GradedObject.Associator
CategoryTheory.GradedObject.ιMapTrifunctorMapObj.eq_1 : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_7}
  {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} (p : I₁ × I₂ × I₃ → J) (X₁ : CategoryTheory.GradedObject I₁ C₁)
  (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) (i₁ : I₁) (i₂ : I₂) (i₃ : I₃)
  (j : J) (h : p (i₁, i₂, i₃) = j)
  [inst_4 : ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p],
  CategoryTheory.GradedObject.ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h =
    ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).ιMapObj p (i₁, i₂, i₃) j h
-- Mathlib.Probability.Kernel.Posterior
ProbabilityTheory.rnDeriv_posterior_symm : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : ProbabilityTheory.Kernel Ω 𝓧}
  {μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsFiniteMeasure μ] [inst_1 : ProbabilityTheory.IsFiniteKernel κ]
  [inst_2 : StandardBorelSpace Ω] [inst_3 : Nonempty Ω] [inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧],
  (∀ᵐ (ω : Ω) ∂μ, (κ ω).AbsolutelyContinuous (μ.bind ⇑κ)) →
    ∀ᵐ (x : 𝓧) ∂μ.bind ⇑κ,
      ∀ᵐ (ω : Ω) ∂μ,
        (ProbabilityTheory.posterior κ μ).rnDeriv (ProbabilityTheory.Kernel.const 𝓧 μ) x ω =
          κ.rnDeriv (ProbabilityTheory.Kernel.const Ω (μ.bind ⇑κ)) ω x
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_eq_ediv : ∀ {a b : ℤ}, a.tdiv b = a / b + if 0 ≤ a ∨ b ∣ a then 0 else b.sign
-- Lean.Data.KVMap
Lean.KVMap.mk : List (Lean.Name × Lean.DataValue) → Lean.KVMap
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.embedding.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C],
  CategoryTheory.Mat_.embedding C =
    { obj := fun X => { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun x => X }, map := fun {X Y} f x x_1 => f,
      map_id := ⋯, map_comp := ⋯ }
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.genLt : Lean.Parser.Parser
-- Lean.Parser.Basic
_private.Lean.Parser.Basic.0.Lean.Parser.decimalNumberFn.parseOptDot : Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState × Bool
-- Std.Async.System
Std.Async.System.instInhabitedOSInfo : Inhabited Std.Async.System.OSInfo
-- Mathlib.Combinatorics.Enumerative.DoubleCounting
/-- **Double counting** argument.

Considering `r` as a bipartite graph, the LHS is a lower bound on the number of edges while the RHS
is an upper bound.  -/
Finset.card_mul_le_card_mul : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) {s : Finset α} {t : Finset β} {m n : ℕ}
  [inst : (a : α) → (b : β) → Decidable (r a b)],
  (∀ a ∈ s, m ≤ (Finset.bipartiteAbove r t a).card) →
    (∀ b ∈ t, (Finset.bipartiteBelow r s b).card ≤ n) → s.card * m ≤ t.card * n
-- Mathlib.Topology.MetricSpace.ShrinkingLemma
/-- **Shrinking lemma** for coverings by open balls in a proper metric space. A point-finite open
cover of a closed subset of a proper metric space by open balls can be shrunk to a new cover by
open balls so that each of the new balls has strictly smaller radius than the old one. This version
assumes that `fun x ↦ ball (c i) (r i)` is a locally finite covering and provides a covering
indexed by the same type.  -/
exists_subset_iUnion_ball_radius_lt : ∀ {α : Type u} {ι : Type v} [inst : MetricSpace α] [ProperSpace α] {c : ι → α} {s : Set α} {r : ι → ℝ},
  IsClosed s →
    (∀ x ∈ s, {i | x ∈ Metric.ball (c i) (r i)}.Finite) →
      s ⊆ ⋃ i, Metric.ball (c i) (r i) → ∃ r', s ⊆ ⋃ i, Metric.ball (c i) (r' i) ∧ ∀ (i : ι), r' i < r i
-- Mathlib.Order.Monotone.MonovaryOrder
antivary_iff_exists_antitone_monotone : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : ι → α} {g : ι → β},
  Antivary f g ↔ ∃ x, Antitone f ∧ Monotone g
-- Batteries.Recycling.MonadSatisfying.Basic
MonadSatisfying.instEStateM : {ε σ : Type u_1} → MonadSatisfying (EStateM ε σ)
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.pow_subset_pow : ∀ {R : Type u_2} [inst : Semiring R] {s : AddSubmonoid R} {n : ℕ}, ↑s ^ n ⊆ ↑(s ^ n)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.forIn_eq_forIn : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α → β → δ → m (ForInStep δ)} {init : δ},
  Std.TreeMap.Raw.forIn f init t = forIn t init fun a d => f a.1 a.2 d
-- Mathlib.ModelTheory.Topology.Types
FirstOrder.Language.Theory.IsMaximal.eq_1 : ∀ {L : FirstOrder.Language} (T : L.Theory),
  T.IsMaximal = (T.IsSatisfiable ∧ ∀ (φ : L.Sentence), φ ∈ T ∨ FirstOrder.Language.Formula.not φ ∈ T)
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
/-- Use the more general `hasColimit` lemma instead, see also
`hasPointwiseRightDerivedFunctorAt_iff`  -/
CategoryTheory.Functor.HasPointwiseRightDerivedFunctorAt.hasColimit' : ∀ {C : Type u₁} {H : Type u₃} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.Category.{v₃, u₃} H}
  {F : CategoryTheory.Functor C H} {W : CategoryTheory.MorphismProperty C} {X : C}
  [self : F.HasPointwiseRightDerivedFunctorAt W X], W.Q.HasPointwiseLeftKanExtensionAt F (W.Q.obj X)
-- Mathlib.Order.Filter.Pi
Filter.pi_mem_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {s : (i : ι) → Set (α i)} {I : Set ι},
  I.Finite → (∀ i ∈ I, s i ∈ f i) → I.pi s ∈ Filter.pi f
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
/-- The right inclusion in the mapping cone.  -/
CochainComplex.mappingCone.inr : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {F G : CochainComplex C ℤ} →
        (φ : F ⟶ G) → [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] → G ⟶ CochainComplex.mappingCone φ
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_diff_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {k : α}, k ∉ t₂ → Std.ExtDTreeMap.Const.get? (t₁ \ t₂) k = Std.ExtDTreeMap.Const.get? t₁ k
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiff_finsetProd : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {t : Finset ι} {f : ι → M → G},
  (∀ i ∈ t, ContMDiff I' I n (f i)) → ContMDiff I' I n fun x => ∏ i ∈ t, f i x
-- Mathlib.Order.Disjoint
Complementeds.codisjoint_coe : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : BoundedOrder α] {a b : Complementeds α},
  Codisjoint ↑a ↑b ↔ Codisjoint a b
-- Mathlib.CategoryTheory.CofilteredSystem
CategoryTheory.Functor.eventualRange.eq_1 : ∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) (j : J),
  F.eventualRange j = ⋂ i, ⋂ f, Set.range ⇑(CategoryTheory.ConcreteCategory.hom (F.map f))
-- Lean.Parser.Basic
Lean.Parser.instAndThenParser : AndThen Lean.Parser.Parser
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_replaceEntry_of_containsKey_eq_false : ∀ {α : Type u} {β : Type v} [inst : BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β},
  Std.Internal.List.containsKey k l = false →
    Std.Internal.List.getValue? a (Std.Internal.List.replaceEntry k v l) = Std.Internal.List.getValue? a l
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- In a preadditive category, if the coproduct of `X` and `Y` exists, then the
binary biproduct of `X` and `Y` exists.  -/
CategoryTheory.Limits.HasBinaryBiproduct.of_hasBinaryCoproduct : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (X Y : C)
  [CategoryTheory.Limits.HasBinaryCoproduct X Y], CategoryTheory.Limits.HasBinaryBiproduct X Y
-- Mathlib.Algebra.Group.Invertible.Defs
/-- `a` is the inverse of `⅟a`.  -/
invertibleInvOf : {α : Type u} → [inst : One α] → [inst_1 : Mul α] → {a : α} → [inst_2 : Invertible a] → Invertible ⅟a
-- Init.System.IOError
/-- A necessary resource was busy.

This corresponds to POSIX errors `EADDRINUSE`, `EBUSY`, `EDEADLK`, and `ETXTBSY`.
 -/
IO.Error.resourceBusy : UInt32 → String → IO.Error
-- Mathlib.Combinatorics.Matroid.Rank.ENat
/-- If `X` is a finite-rank set, and `I` is a subset of `X` of cardinality
no larger than the rank of `X` that spans `X`, then `I` is a basis for `X`.  -/
Matroid.IsRkFinite.isBasis_of_subset_closure_of_subset_of_encard_le : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α},
  M.IsRkFinite X → X ⊆ M.closure I → I ⊆ X → I.encard ≤ M.eRk X → M.IsBasis I X
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitInfo.hash : Lean.Meta.Grind.SplitInfo → UInt64
-- Mathlib.NumberTheory.Height.MvPolynomial
_private.Mathlib.NumberTheory.Height.MvPolynomial.0.Height.mulHeight_constantCoeff_le_mulHeightBound : ∀ {K : Type u_4} [inst : Field K] {ι : Type u_5} {ι' : Type u_6} [inst_1 : Height.AdmissibleAbsValues K] [Finite ι']
  {p : ι' → MvPolynomial ι K},
  (fun j => MvPolynomial.constantCoeff (p j)) ≠ 0 →
    (Height.mulHeight fun j => MvPolynomial.constantCoeff (p j)) ≤ Height.mulHeightBound p
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
/-- `InducedBicategory.Hom₂ f g` is a type-alias for 2-morphisms between `f g : X ⟶ Y`, where
`f` and `g` are 1-morphisms for the induced bicategory structure on `B`.

This is given a `Category` instance below, induced from the corresponding one in `C`.  -/
CategoryTheory.Bicategory.InducedBicategory.Hom₂ : {B : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Bicategory C] →
      {F : B → C} → {X Y : CategoryTheory.Bicategory.InducedBicategory C F} → (X ⟶ Y) → (X ⟶ Y) → Type u_3
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.symm_symm_apply : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (e : P₁ ≃ᴬ[k] P₂) (x : P₁), e.symm.symm x = e x
-- Mathlib.Data.PFunctor.Multivariate.M
_private.Mathlib.Data.PFunctor.Multivariate.M.0.TypeVec.append1.match_1.eq_1 : ∀ {n : ℕ} (motive : Fin2 (n + 1) → Sort u_1) (i : Fin2 n) (h_1 : (i : Fin2 n) → motive i.fs)
  (h_2 : Unit → motive Fin2.fz),
  (match i.fs with
    | i.fs => h_1 i
    | Fin2.fz => h_2 ()) =
    h_1 i
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
nnnorm_cfcₙ_lt : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A]
  [inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] {f : 𝕜 → 𝕜} {a : A} {c : NNReal},
  (∀ x ∈ quasispectrum 𝕜 a, ‖f x‖₊ < c) → ‖cfcₙ f a‖₊ < c
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
HurwitzKernelBounds.isBigO_atTop_F_int_zero_sub : ∀ (a : UnitAddCircle),
  ∃ p,
    0 < p ∧
      (fun t => HurwitzKernelBounds.F_int 0 a t - if a = 0 then 1 else 0) =O[Filter.atTop] fun t => Real.exp (-p * t)
-- Mathlib.Order.SuccPred.CompleteLinearOrder
sSup_Iio_eq_self_iff_isSuccPrelimit : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrderBot α] {x : α}, sSup (Set.Iio x) = x ↔ Order.IsSuccPrelimit x
-- Init.Data.SInt.Lemmas
ISize.toBitVec_toInt8 : ∀ (x : ISize), x.toInt8.toBitVec = BitVec.signExtend 8 x.toBitVec
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- The fourth simplicial identity  -/
SimplexCategory.δ_comp_σ_of_gt : ∀ {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)},
  j.castSucc < i →
    CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i.succ) (SimplexCategory.σ j.castSucc) =
      CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j) (SimplexCategory.δ i)
-- Mathlib.Data.Set.Operations
/-- We can use the axiom of choice to pick a preimage for every element of `range f`.  -/
Set.rangeSplitting : {α : Type u} → {β : Type v} → (f : α → β) → ↑(Set.range f) → α
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_succEmb_uIcc : ∀ {n : ℕ} (i j : Fin n), Finset.map (Fin.succEmb n) (Finset.uIcc i j) = Finset.uIcc i.succ j.succ
-- Mathlib.Algebra.GroupWithZero.Units.Basic
/-- A variant of `eq_mul_inv_iff_mul_eq₀` that moves the nonzero hypothesis to another variable.  -/
mul_eq_of_eq_mul_inv₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b c : G₀}, a ≠ 0 → a = c * b⁻¹ → a * b = c
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
/-- If a sum of continuous functions `g n` is convergent, and the same sum converges in `Lᵖ` to `h`,
then in fact `g n` converges uniformly to `h`.  -/
ContinuousMap.hasSum_of_hasSum_Lp : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace α] [inst_1 : BorelSpace α] [inst_2 : NormedAddCommGroup E]
  [inst_3 : SecondCountableTopologyEither α E] [inst_4 : CompactSpace α] [inst_5 : MeasureTheory.IsFiniteMeasure μ]
  {𝕜 : Type u_3} [inst_6 : Fact (1 ≤ p)] [inst_7 : NormedRing 𝕜] [inst_8 : Module 𝕜 E] [inst_9 : IsBoundedSMul 𝕜 E]
  {β : Type u_4} [μ.IsOpenPosMeasure] {g : β → C(α, E)} {f : C(α, E)},
  Summable g → HasSum (⇑(ContinuousMap.toLp p μ 𝕜) ∘ g) ((ContinuousMap.toLp p μ 𝕜) f) → HasSum g f
-- Lean.Meta.LetToHave
/-- Finds a pre-existing result in the cache.
Note that the result might have no type, which happens for example if it was visited when `check` is false.
 -/
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.findCache? : Lean.Expr → Lean.Meta.LetToHave.M✝ (Option Lean.Meta.LetToHave.Result✝)
-- Mathlib.Combinatorics.Quiver.Covering
Quiver.starEquivCostar_apply_snd : ∀ {U : Type u_1} [inst : Quiver U] [inst_1 : Quiver.HasInvolutiveReverse U] (u : U) (e : Quiver.Star u),
  ((Quiver.starEquivCostar u) e).snd = Quiver.reverse e.snd
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isIdempotentElemEquivClopens_symm_inf : ∀ {R : Type u} [inst : CommRing R] (s₁ s₂ : TopologicalSpace.Clopens (PrimeSpectrum R)),
  PrimeSpectrum.isIdempotentElemEquivClopens.symm (s₁ ⊓ s₂) =
    ⟨↑(PrimeSpectrum.isIdempotentElemEquivClopens.symm s₁) * ↑(PrimeSpectrum.isIdempotentElemEquivClopens.symm s₂), ⋯⟩
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
/-- Given a finite family of points `v` in an additive monoid `M`, together with a
morphism into a linearly-ordered additive monoid `f : M →+ S`, the submonoid generated by those
points of `v` which lie in the half space where `f > 0` is generated by the subset of such points
which are indecomposable with respect to points in this half space.

If `v` is the set of roots of a crystallographic root system and `S = ℚ`, then this is
[serre1965](Ch. V, §9, Lemma 2) and it may be used to prove that the root system has a base.  -/
AddSubmonoid.closure_image_isAddIndecomposable_baseOf : ∀ {ι : Type u_1} {M : Type u_2} {S : Type u_4} [inst : AddMonoid M] [inst_1 : LinearOrder S] [Finite ι]
  [inst_3 : AddCommMonoid S] [IsOrderedCancelAddMonoid S] (v : ι → M) (f : M →+ S),
  AddSubmonoid.closure (v '' IsAddIndecomposable.baseOf v f) = AddSubmonoid.closure (v '' {i | 0 < f (v i)})
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.Functor.OplaxMonoidal.δ_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.OplaxMonoidal] (X Y : C) {Z : D} (h : F.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X Y)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd (F.obj X) (F.obj Y)) h) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)) h
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `MeromorphicAt.inv` -/
MeromorphicAt.fun_inv : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {x : 𝕜} {f : 𝕜 → 𝕜'}, MeromorphicAt f x → MeromorphicAt (fun i => (f i)⁻¹) x
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.restrictScalars_lTensor : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {Q : Type uQ} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] [inst_9 : AddCommMonoid Q]
  [inst_10 : Module R Q] (f : N →ₗ[R] Q), ↑R ((TensorProduct.AlgebraTensorModule.lTensor A M) f) = LinearMap.lTensor M f
-- Mathlib.CategoryTheory.Adjunction.Limits
/-- auxiliary construction for `conesIso`  -/
CategoryTheory.Adjunction.conesIsoComponentHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (F ⊣ G) →
              {J : Type u} →
                [inst_2 : CategoryTheory.Category.{v, u} J] →
                  {K : CategoryTheory.Functor J D} →
                    (X : Cᵒᵖ) →
                      (F.op.comp ((CategoryTheory.cones J D).obj K)).obj X →
                        ((CategoryTheory.cones J C).obj (K.comp G)).obj X
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
Mathlib.Tactic.Monoidal.structuralIsoOfExpr_whiskerLeft : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (f : C) {g h : C}
  (η : g ⟶ h) (η' : g ≅ h),
  η'.hom = η →
    (CategoryTheory.MonoidalCategory.whiskerLeftIso f η').hom = CategoryTheory.MonoidalCategoryStruct.whiskerLeft f η
-- Mathlib.Topology.Covering.Quotient
Topology.IsQuotientMap.trivializationOfSMulDisjoint_source : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hf : Topology.IsQuotientMap f) [inst_4 : ContinuousConstSMul G E]
  (hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂) [inst_5 : TopologicalSpace G]
  [inst_6 : DiscreteTopology G] (U : Set E) (open_U : IsOpen U)
  (disjoint : ∀ (g : G), ((fun x => g • x) '' U ∩ U).Nonempty → g = 1),
  (hf.trivializationOfSMulDisjoint hfG U open_U disjoint).source = f ⁻¹' f '' U
-- Mathlib.GroupTheory.Congruence.Basic
Con.instSMulCommClass : ∀ {α : Type u_4} {β : Type u_5} {M : Type u_6} [inst : MulOneClass M] [inst_1 : SMul α M] [inst_2 : SMul β M]
  [inst_3 : IsScalarTower α M M] [inst_4 : IsScalarTower β M M] [SMulCommClass α β M] (c : Con M),
  SMulCommClass α β c.Quotient
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
CategoryTheory.ObjectProperty.IsClosedUnderFiniteCoproducts.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C},
  autoParam (∀ (J : Type) [Finite J], P.IsClosedUnderColimitsOfShape (CategoryTheory.Discrete J))
      CategoryTheory.ObjectProperty.IsClosedUnderFiniteCoproducts.isClosedUnderColimitsOfShape._autoParam →
    P.IsClosedUnderFiniteCoproducts
-- Mathlib.Algebra.Algebra.Unitization
/-- The canonical `S`-linear inclusion `A → Unitization R A`.  -/
Unitization.inrHom : (S : Type u_2) →
  (R : Type u_3) →
    (A : Type u_4) →
      [inst : Semiring S] →
        [inst_1 : Semiring R] →
          [inst_2 : AddCommMonoid A] → [inst_3 : Module S R] → [inst_4 : Module S A] → A →ₗ[S] Unitization R A