mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi
cfc_map_pi : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {A : ι → Type u_4} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : CommRing S]
  [inst_6 : Algebra R S] [inst_7 : (i : ι) → Ring (A i)] [inst_8 : (i : ι) → Algebra S (A i)]
  [inst_9 : (i : ι) → Algebra R (A i)] [∀ (i : ι), IsScalarTower R S (A i)] [hinst : IsScalarTower R S ((i : ι) → A i)]
  [inst_11 : (i : ι) → StarRing (A i)] [inst_12 : (i : ι) → TopologicalSpace (A i)] {p : ((i : ι) → A i) → Prop}
  {q : (i : ι) → A i → Prop} [inst_13 : ContinuousFunctionalCalculus R ((i : ι) → A i) p]
  [inst_14 : ∀ (i : ι), ContinuousFunctionalCalculus R (A i) (q i)] [∀ (i : ι), ContinuousMap.UniqueHom R (A i)]
  (f : R → R) (a : (i : ι) → A i),
  autoParam (ContinuousOn f (⋃ i, spectrum R (a i))) cfc_map_pi._auto_1 →
    autoParam (p a) cfc_map_pi._auto_3 →
      autoParam (∀ (i : ι), q i (a i)) cfc_map_pi._auto_5 → cfc f a = fun i => cfc f (a i)
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Arrow.hasColimit : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {T : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} T]
  (F : CategoryTheory.Functor J (CategoryTheory.Arrow T))
  [i₁ : CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.Arrow.leftFunc)]
  [i₂ : CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.Arrow.rightFunc)], CategoryTheory.Limits.HasColimit F
-- Mathlib.Analysis.Calculus.LHopital
/-- **L'Hôpital's rule** for approaching a real from the right, `deriv` version  -/
deriv.lhopital_zero_nhdsGT : ∀ {a : ℝ} {l : Filter ℝ} {f g : ℝ → ℝ},
  (∀ᶠ (x : ℝ) in nhdsWithin a (Set.Ioi a), DifferentiableAt ℝ f x) →
    (∀ᶠ (x : ℝ) in nhdsWithin a (Set.Ioi a), deriv g x ≠ 0) →
      Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds 0) →
        Filter.Tendsto g (nhdsWithin a (Set.Ioi a)) (nhds 0) →
          Filter.Tendsto (fun x => deriv f x / deriv g x) (nhdsWithin a (Set.Ioi a)) l →
            Filter.Tendsto (fun x => f x / g x) (nhdsWithin a (Set.Ioi a)) l
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.sum_measure_singleton : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Finset α} [MeasurableSingletonClass α],
  ∑ x ∈ s, μ {x} = μ ↑s
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.getD_diff_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k fallback : α}, k ∈ m₂ → (m₁ \ m₂).getD k fallback = fallback
-- Mathlib.CategoryTheory.Action.Monoidal
/-- Given an object `X` isomorphic to the tensor unit of `V`, `X` equipped with the trivial action
is isomorphic to the tensor unit of `Action V G`.  -/
Action.tensorUnitIso : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} →
      [inst_1 : Monoid G] →
        [inst_2 : CategoryTheory.MonoidalCategory V] →
          {X : V} →
            (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ≅ X) →
              (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action V G) ≅ { V := X, ρ := 1 })
-- Mathlib.Data.List.Forall2
List.rel_filter : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {p : α → Bool} {q : β → Bool},
  (Relator.LiftFun R (fun x1 x2 => x1 ↔ x2) (fun x => p x = true) fun x => q x = true) →
    Relator.LiftFun (List.Forall₂ R) (List.Forall₂ R) (List.filter p) (List.filter q)
-- Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures
CategoryTheory.Limits.Concrete.colimit_rep_eq_zero : ∀ (R : Type u_1) [inst : Ring R] {J : Type w} [inst_1 : CategoryTheory.Category.{r, w} J]
  (F : CategoryTheory.Functor J (ModuleCat R))
  [CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget (ModuleCat R))] [CategoryTheory.IsFiltered J]
  [inst_4 : CategoryTheory.Limits.HasColimit F] (j : J) (x : ↑(F.obj j)),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) x = 0 →
    ∃ j' i, (ModuleCat.Hom.hom (F.map i)) x = 0
-- Mathlib.Analysis.Normed.Lp.LpEquiv
coe_equiv_lpPiLp_symm : ∀ {α : Type u_1} {E : α → Type u_2} [inst : (i : α) → NormedAddCommGroup (E i)] {p : ENNReal} [inst_1 : Finite α]
  (f : PiLp p E), ↑(Equiv.lpPiLp.symm f) = f.ofLp
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Circle.eq_1 : Circle = ↥(Submonoid.unitSphere ℂ)
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.IsPath.nil : ∀ {F : PFunctor.{uA, uB}} (x : F.M), PFunctor.M.IsPath [] x
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.ImportErrorData.mk : IO.Ref (Array Lean.Meta.RefinedDiscrTree.ImportFailure✝) → Lean.Meta.RefinedDiscrTree.ImportErrorData✝
-- Lean.Meta.Tactic.Grind.Attr
_private.Lean.Meta.Tactic.Grind.Attr.0.Lean.Meta.Grind.Extension.addCasesAttr : Lean.Meta.Grind.Extension → Lean.Name → Bool → Lean.AttributeKind → Lean.CoreM Unit
-- Mathlib.Data.Set.NAry
Set.image2_subset_iff : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {u : Set γ},
  Set.image2 f s t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, f x y ∈ u
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- A function is meromorphic in normal form at a point iff it is meromorphic in normal form after
composition with an analytic function of nonvanishing derivative, such as translation.
 -/
meromorphicNFAt_comp_iff_of_deriv_ne_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} [CompleteSpace 𝕜] [CharZero 𝕜] {x : 𝕜} {g : 𝕜 → 𝕜},
  AnalyticAt 𝕜 g x → deriv g x ≠ 0 → (MeromorphicNFAt (f ∘ g) x ↔ MeromorphicNFAt f (g x))
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.periodicOrbit_chain : ∀ {α : Type u_1} (r : α → α → Prop) {f : α → α} {x : α},
  Cycle.Chain r (Function.periodicOrbit f x) ↔ ∀ n < Function.minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instBEqLeanDiagnosticTag : BEq Lean.Lsp.LeanDiagnosticTag
-- Mathlib.SetTheory.Ordinal.Arithmetic
_private.Mathlib.SetTheory.Ordinal.Arithmetic.0.Ordinal.add_mul_limit_aux : ∀ {a b c : Ordinal.{u_4}},
  b + a = a → Order.IsSuccLimit c → (∀ c' < c, (a + b) * Order.succ c' = a * Order.succ c' + b) → (a + b) * c = a * c
-- Batteries.Lean.AttributeExtra
Lean.ParametricAttributeExtra.mk.inj : ∀ {α : Type} {attr : Lean.ParametricAttribute α} {base : Std.HashMap Lean.Name α} {attr_1 : Lean.ParametricAttribute α}
  {base_1 : Std.HashMap Lean.Name α},
  { attr := attr, base := base } = { attr := attr_1, base := base_1 } → attr = attr_1 ∧ base = base_1
-- Mathlib.Algebra.Category.MonCat.Basic
_private.Mathlib.Algebra.Category.MonCat.Basic.0.AddMonCat.Hom.mk.injEq : ∀ {A B : AddMonCat} (hom' hom'_1 : ↑A →+ ↑B), ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Mathlib.RingTheory.Coprime.Lemmas
IsRelPrime.pow_iff : ∀ {α : Type u_1} [inst : CommMonoid α] [DecompositionMonoid α] {x y : α} {m n : ℕ},
  0 < m → 0 < n → (IsRelPrime (x ^ m) (y ^ n) ↔ IsRelPrime x y)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.getKey?_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, m₁.WF → m₂.WF → m₁.Equiv m₂ → m₁.getKey? k = m₂.getKey? k
-- Batteries.Data.List.Basic
/-- List of all sections through a list of lists. A section
of `[L₁, L₂, ..., Lₙ]` is a list whose first element comes from
`L₁`, whose second element comes from `L₂`, and so on.
 -/
List.sections : {α : Type u_1} → List (List α) → List (List α)
-- Mathlib.Data.Prod.Lex
Prod.Lex.orderTop : {α : Type u_1} →
  {β : Type u_2} →
    [inst : PartialOrder α] → [inst_1 : Preorder β] → [OrderTop α] → [OrderTop β] → OrderTop (Lex (α × β))
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.instIsNontrivialWithZeroMultiplicativeIntIntValuation : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R),
  v.intValuation.IsNontrivial
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_insertMany_of_contains : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] {ρ : Type w}
  [inst_2 : ForIn Id ρ ((a : α) × β a)] [EquivBEq α] [LawfulHashable α],
  (↑m).WF → ∀ {l : ρ} {k : α}, m.contains k = true → (↑(m.insertMany l)).contains k = true
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_ofList_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' : α},
  (k == k') = true →
    ∀ {v fallback : β},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l →
        (k, v) ∈ l → Std.DHashMap.Raw.Const.getD (Std.DHashMap.Raw.Const.ofList l) k' fallback = v
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getKeyLE!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getKeyLE! k = t₂.getKeyLE! k
-- Mathlib.Analysis.Normed.Lp.ProdLp
_private.Mathlib.Analysis.Normed.Lp.ProdLp.0.WithLp.prod_cobounded_aux : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : PseudoMetricSpace α]
  [inst_1 : PseudoMetricSpace β], Bornology.cobounded (WithLp p (α × β)) = Bornology.cobounded (WithLp p (α × β))
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel.rel : ∀ {R : Type u} [inst : Rack R] {a b : Rack.PreEnvelGroup R} (r : Rack.PreEnvelGroupRel' R a b),
  Rack.PreEnvelGroupRel R a b
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.one_lt_rootMultiplicity_iff_isRoot : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R} {t : R},
  p ≠ 0 → (1 < Polynomial.rootMultiplicity t p ↔ p.IsRoot t ∧ (Polynomial.derivative p).IsRoot t)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whisker_exchange : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z : C}
  (f : W ⟶ X) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W g)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y)
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g)
-- Mathlib.Algebra.Group.Submonoid.Units
/-- The equivalence between the coercion of a subgroup `S` of `Mˣ` to a submonoid of `M` and
the subgroup itself as a type.  -/
Subgroup.ofUnitsEquivType : {M : Type u_1} → [inst : Monoid M] → (S : Subgroup Mˣ) → ↥S.ofUnits ≃* ↥S
-- Lean.LocalContext
Lean.LocalContext.fvarIdToDecl : Lean.LocalContext → Lean.PersistentHashMap Lean.FVarId Lean.LocalDecl
-- Std.Time.Time.Unit.Minute
Std.Time.Minute.instInhabitedOrdinal : Inhabited Std.Time.Minute.Ordinal
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of the forward direction of `SimpleGraph.Walk.isPath_mapLe`. -/
SimpleGraph.Walk.IsPath.of_mapLe : ∀ {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} {p : G.Walk u v},
  (SimpleGraph.Walk.mapLe h p).IsPath → p.IsPath
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.IsPresentationCore.mk.sizeOf_spec : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {solution : relations.Solution M} [inst_3 : SizeOf A] [inst_4 : SizeOf M]
  (desc : {N : Type w'} → [inst_5 : AddCommGroup N] → [inst_6 : Module A N] → relations.Solution N → M →ₗ[A] N)
  (postcomp_desc :
    ∀ {N : Type w'} [inst_5 : AddCommGroup N] [inst_6 : Module A N] (s : relations.Solution N),
      solution.postcomp (desc s) = s)
  (postcomp_injective :
    ∀ {N : Type w'} [inst_5 : AddCommGroup N] [inst_6 : Module A N] {f f' : M →ₗ[A] N},
      solution.postcomp f = solution.postcomp f' → f = f'),
  sizeOf { desc := desc, postcomp_desc := postcomp_desc, postcomp_injective := postcomp_injective } = 1
-- Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
CategoryTheory.Pretriangulated.mem_distTriang_op_iff' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (T : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ),
  T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔
    ∃ T',
      ∃ (_ : T' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles),
        Nonempty (T ≅ (CategoryTheory.Pretriangulated.triangleOpEquivalence C).functor.obj (Opposite.op T'))
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.imp.injEq : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (f₁ f₂ f₁_1 f₂_1 : L.BoundedFormula α n),
  (f₁.imp f₂ = f₁_1.imp f₂_1) = (f₁ = f₁_1 ∧ f₂ = f₂_1)
-- Mathlib.CategoryTheory.Sums.Basic
/-- The functor exchanging two direct summand categories.  -/
CategoryTheory.Sum.swap : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor (C ⊕ D) (D ⊕ C)
-- Mathlib.Analysis.Normed.Operator.Banach
/-- Convert a bijective continuous linear map `f : E →SL[σ] F` from a Banach space to a normed space
to a continuous linear equivalence.  -/
ContinuousLinearEquiv.ofBijective : {𝕜 : Type u_1} →
  {𝕜' : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NontriviallyNormedField 𝕜'] →
        {σ : 𝕜 →+* 𝕜'} →
          {E : Type u_3} →
            [inst_2 : NormedAddCommGroup E] →
              [inst_3 : NormedSpace 𝕜 E] →
                {F : Type u_4} →
                  [inst_4 : NormedAddCommGroup F] →
                    [inst_5 : NormedSpace 𝕜' F] →
                      {σ' : 𝕜' →+* 𝕜} →
                        [inst_6 : RingHomInvPair σ σ'] →
                          [RingHomIsometric σ] →
                            [RingHomIsometric σ'] →
                              [CompleteSpace F] →
                                [CompleteSpace E] →
                                  [inst_11 : RingHomInvPair σ' σ] →
                                    (f : E →SL[σ] F) → (↑f).ker = ⊥ → (↑f).range = ⊤ → E ≃SL[σ] F
-- Mathlib.Tactic.LinearCombination
Mathlib.Tactic.LinearCombination.Expanded.proof.inj : ∀ {rel : Mathlib.Ineq} {pf : Lean.Term} {rel_1 : Mathlib.Ineq} {pf_1 : Lean.Term},
  Mathlib.Tactic.LinearCombination.Expanded.proof rel pf = Mathlib.Tactic.LinearCombination.Expanded.proof rel_1 pf_1 →
    rel = rel_1 ∧ pf = pf_1
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.coe_linear_mk : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (f : M →ₗ[R] N)
  (h : ∀ {x : L} {m : M}, f.toFun ⁅x, m⁆ = ⁅x, f.toFun m⁆), ↑{ toLinearMap := f, map_lie' := h } = f
-- Init.Data.Order.Ord
/-- If two values compare equal, then they are logically equal.  -/
Std.LawfulEqCmp.eq_of_compare : ∀ {α : Type u} {cmp : α → α → Ordering} [self : Std.LawfulEqCmp cmp] {a b : α}, cmp a b = Ordering.eq → a = b
-- Std.Data.Internal.List.Associative
Std.Internal.List.le_minKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {he : l.isEmpty = false},
      (compare k (Std.Internal.List.minKey l he)).isLE = true ↔
        ∀ (k' : α), Std.Internal.List.containsKey k' l = true → (compare k k').isLE = true
-- Mathlib.Data.Matrix.DMatrix
DMatrix.map_apply : ∀ {m : Type u_1} {n : Type u_2} {α : m → n → Type v} {M : DMatrix m n α} {β : m → n → Type w}
  {f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j} {i : m} {j : n}, M.map f i j = f (M i j)
-- Std.Data.DTreeMap.Raw.Basic
/-- Removes all mappings of the map for which the given function returns `false`.  -/
Std.DTreeMap.Raw.filter : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → ((a : α) → β a → Bool) → Std.DTreeMap.Raw α β cmp → Std.DTreeMap.Raw α β cmp
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.instTop : {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → Top (L.BoundedFormula α n)
-- Mathlib.Order.Interval.Set.ProjIcc
Set.monotone_projIic : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α}, Monotone (Set.projIic a)
-- Mathlib.Analysis.Normed.Module.Ball.Action
continuousSMul_sphere_ball : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {r : ℝ}, ContinuousSMul ↑(Metric.sphere 0 1) ↑(Metric.ball 0 r)
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- Construct a left lift from a 1-morphism and a 2-morphism.  -/
CategoryTheory.Bicategory.LeftLift.mk : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} →
          (h : c ⟶ b) → (g ⟶ CategoryTheory.CategoryStruct.comp h f) → CategoryTheory.Bicategory.LeftLift f g
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
CategoryTheory.Functor.IsDense.of_iso : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (e : F ≅ G) [F.IsDense], G.IsDense
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.measurable_polarSpaceCoord_symm : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  Measurable ↑(NumberField.mixedEmbedding.polarSpaceCoord K).symm
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.const_sup : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [inst : Max β] (a b : β), ↑(a ⊔ b) = ↑a ⊔ ↑b
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
/-- If a bifunctor preserves separately colimits of `K₁` in the first variable and colimits
of `K₂` in the second variable, then it preserves colimit of the pair `K₁, K₂`.  -/
CategoryTheory.Limits.PreservesColimit₂.of_preservesColimits_in_each_variable : ∀ {J₁ : Type u_1} {J₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] {C₁ : Type u_3} {C₂ : Type u_4} {C : Type u_5}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] {K₁ : CategoryTheory.Functor J₁ C₁}
  {K₂ : CategoryTheory.Functor J₂ C₂} (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C))
  [∀ (x : C₂), CategoryTheory.Limits.PreservesColimit K₁ (G.flip.obj x)]
  [∀ (x : C₁), CategoryTheory.Limits.PreservesColimit K₂ (G.obj x)], CategoryTheory.Limits.PreservesColimit₂ K₁ K₂ G
-- Mathlib.Data.List.Duplicate
/-- The contrapositive of `List.nodup_iff_sublist`.  -/
List.duplicate_iff_sublist : ∀ {α : Type u_1} {l : List α} {x : α}, List.Duplicate x l ↔ [x, x].Sublist l
-- Mathlib.Algebra.Group.Subsemigroup.Defs
MulMemClass.mk : ∀ {S : Type u_3} {M : outParam (Type u_4)} [inst : Mul M] [inst_1 : SetLike S M],
  (∀ {s : S} {a b : M}, a ∈ s → b ∈ s → a * b ∈ s) → MulMemClass S M
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.subtype_apply_coe : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] {p : α → Prop} {q : β → Prop}
  (e : α ≃ᵤ β) (h : ∀ (a : α), p a ↔ q (e a)) (a : { a // p a }), ↑((e.subtype h) a) = e ↑a
-- Mathlib.MeasureTheory.OuterMeasure.Basic
MeasureTheory.measure_iUnion_fintype_le : ∀ {α : Type u_1} {ι : Type u_2} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α]
  [inst_2 : Fintype ι] (μ : F) (s : ι → Set α), μ (⋃ i, s i) ≤ ∑ i, μ (s i)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
/-- the condition that the denominator belongs to the given morphism property  -/
CategoryTheory.MorphismProperty.LeftFraction₂.hs : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (self : W.LeftFraction₂ X Y), W self.s
-- Lean.Elab.ConfigEval.Types
/-- The `option` identifier split into components, without macro scopes.
This allows us to pull off components one at a time if we have hierarchical configuration options.  -/
Lean.Elab.ConfigEval.ConfigItem.optionComps : Lean.Elab.ConfigEval.ConfigItem → List Lean.Syntax
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.addSemigroup.eq_1 : ∀ {M : Type u_4} [inst : AddSemigroup M] (c : AddCon M), c.addSemigroup = { toAdd := c.hasAdd, add_assoc := ⋯ }
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.isNormal' : ∀ {G : Type u_1} [inst : Group G] (self : FiniteIndexNormalSubgroup G), self.Normal
-- Mathlib.FieldTheory.Normal.Defs
Normal.of_equiv_equiv : ∀ {F : Type u_1} [inst : Field F] {E : Type u_3} [inst_1 : Field E] [inst_2 : Algebra F E] {M : Type u_5} {N : Type u_6}
  [inst_3 : Field N] [inst_4 : Field M] [inst_5 : Algebra M N] [h : Normal F E] {f : F ≃+* M} {g : E ≃+* N},
  (algebraMap M N).comp ↑f = (↑g).comp (algebraMap F E) → Normal M N
-- Mathlib.RingTheory.Polynomial.IntegralNormalization
/-- If `p : R[X]` is a nonzero polynomial with root `z`, `integralNormalization p` is
a monic polynomial with root `leadingCoeff f * z`.

Moreover, `integralNormalization 0 = 0`.
 -/
Polynomial.integralNormalization : {R : Type u} → [inst : Semiring R] → Polynomial R → Polynomial R
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Internal.iter_roi_eq_iter_rci_of_isSome_succ? : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] {lo : α}
  (h : (Std.PRange.succ? lo).isSome = true),
  Std.Roi.Internal.iter lo<...* = Std.Rci.Internal.iter ((Std.PRange.succ? lo).get h)...*
-- Mathlib.Analysis.CStarAlgebra.Basic
CStarRing.norm_star_mul_self : ∀ {E : Type u_2} [inst : NonUnitalNormedRing E] [inst_1 : StarRing E] [CStarRing E] {x : E}, ‖star x * x‖ = ‖x‖ * ‖x‖
-- Std.Sat.AIG.CachedLemmas
_private.Std.Sat.AIG.CachedLemmas.0.Std.Sat.AIG.mkAtomCached.match_1.splitter : {α : Type} →
  (decls : Array (Std.Sat.AIG.Decl α)) →
    (decl : Std.Sat.AIG.Decl α) →
      (motive : Option (Std.Sat.AIG.CacheHit decls decl) → Sort u_1) →
        (x : Option (Std.Sat.AIG.CacheHit decls decl)) →
          ((hit : Std.Sat.AIG.CacheHit decls decl) → motive (some hit)) → (Unit → motive none) → motive x
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
CategoryTheory.Presieve.FamilyOfElements.isCompatible_map_smul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ R : CategoryTheory.Functor Cᵒᵖ RingCat} (α : R₀ ⟶ R) [CategoryTheory.Presheaf.IsLocallyInjective J α]
  {M₀ : PresheafOfModules R₀} {A : CategoryTheory.Functor Cᵒᵖ AddCommGrpCat} (φ : M₀.presheaf ⟶ A)
  [CategoryTheory.Presheaf.IsLocallyInjective J φ],
  CategoryTheory.Presheaf.IsSeparated J A →
    ∀ {X : C} (r : ↑(R.obj (Opposite.op X))) (m : ↑(A.obj (Opposite.op X))) {P : CategoryTheory.Presieve X}
      (r₀ : CategoryTheory.Presieve.FamilyOfElements (R₀.comp (CategoryTheory.forget RingCat)) P)
      (m₀ : CategoryTheory.Presieve.FamilyOfElements (M₀.presheaf.comp (CategoryTheory.forget Ab)) P),
      (r₀.map (CategoryTheory.Functor.whiskerRight α (CategoryTheory.forget RingCat))).IsAmalgamation r →
        (m₀.map (CategoryTheory.Functor.whiskerRight φ (CategoryTheory.forget Ab))).IsAmalgamation m →
          ((r₀.smul m₀).map (CategoryTheory.Functor.whiskerRight φ (CategoryTheory.forget Ab))).Compatible
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
/-- Union of two tagged prepartitions with disjoint unions of boxes.  -/
BoxIntegral.TaggedPrepartition.disjUnion : {ι : Type u_1} →
  {I : BoxIntegral.Box ι} →
    (π₁ π₂ : BoxIntegral.TaggedPrepartition I) → Disjoint π₁.iUnion π₂.iUnion → BoxIntegral.TaggedPrepartition I
-- Mathlib.Order.Atoms
IsCoatomic.exists_coatom : ∀ (α : Type u_2) [inst : PartialOrder α] [inst_1 : OrderTop α] [Nontrivial α] [IsCoatomic α], ∃ a, IsCoatom a