mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Action.Pi
/-- If `α i` has a faithful additive action for a given `i`, then
so does `Π i, α i`. This is not an instance as `i` cannot be inferred  -/
Pi.faithfulVAdd_at : ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [inst : (i : ι) → VAdd M (α i)] [∀ (i : ι), Nonempty (α i)] (i : ι)
  [FaithfulVAdd M (α i)], FaithfulVAdd M ((i : ι) → α i)
-- Init.Data.UInt.Lemmas
UInt64.lt_iff_toNat_lt : ∀ {a b : UInt64}, a < b ↔ a.toNat < b.toNat
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.Kind.none : Mathlib.Tactic.Widget.StringDiagram.Kind
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.subtype_apply_coe : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {p : X → Prop} {q : Y → Prop}
  (h : X ≃ₜ Y) (h_iff : ∀ (x : X), p x ↔ q (h x)) (a : { a // p a }), ↑((h.subtype h_iff) a) = h ↑a
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `monovary_inv₀`. -/
Monovary.of_inv₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : Semifield β] [inst_4 : LinearOrder β] [IsStrictOrderedRing β] {f : ι → α} {g : ι → β},
  StrongLT 0 f → StrongLT 0 g → Monovary f⁻¹ g⁻¹ → Monovary f g
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasStrictFDerivAt.hasFDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E}, HasStrictFDerivAt f f' x → HasFDerivAt f f' x
-- Mathlib.Order.CompleteLattice.Group
le_iInf₂_mul : ∀ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [inst : CompleteLattice α] [inst_1 : Mul α] [MulLeftMono α]
  [MulRightMono α] (u v : (i : ι) → κ i → α), (⨅ i, ⨅ j, u i j) * ⨅ i, ⨅ j, v i j ≤ ⨅ i, ⨅ j, u i j * v i j
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_union_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [inst : Inhabited α] [Std.TransCmp cmp] {k : α},
  k ∉ t₁ → (t₁ ∪ t₂).get! k = t₂.get! k
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.BitVec.not_eq_comm' : ∀ {w : ℕ} (a b : BitVec w), (a == ~~~b) = (b == ~~~a)
-- Init.Control.StateRef
/-- Applies a function to the current state that both computes a new state and a value. The new state
replaces the current state, and the value is returned.

It is equivalent to a `get` followed by a `set`. However, using `modifyGet` may lead to higher
performance because it doesn't add a new reference to the state value. Additional references can
inhibit in-place updates of data.
 -/
StateRefT'.modifyGet : {ω σ : Type} → {m : Type → Type} → {α : Type} → [MonadLiftT (ST ω) m] → (σ → α × σ) → StateRefT' ω σ m α
-- Mathlib.Order.Heyting.Hom
map_bihimp : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : HeytingAlgebra α]
  [inst_2 : HeytingAlgebra β] [HeytingHomClass F α β] (f : F) (a b : α), f (bihimp a b) = bihimp (f a) (f b)
-- Mathlib.GroupTheory.CosetCover
AddSubgroup.leftCoset_cover_filter_FiniteIndex_aux : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_2} {H : ι → AddSubgroup G} {g : ι → G} {s : Finset ι},
  ⋃ i ∈ s, g i +ᵥ ↑(H i) = Set.univ →
    ∀ [inst_1 : DecidablePred AddSubgroup.FiniteIndex],
      ⋃ k ∈ {i ∈ s | (H i).FiniteIndex}, g k +ᵥ ↑(H k) = Set.univ ∧
        1 ≤ ∑ i ∈ s, (↑(H i).index)⁻¹ ∧
          (∑ i ∈ s, (↑(H i).index)⁻¹ = 1 → (↑({i ∈ s | (H i).FiniteIndex})).PairwiseDisjoint fun i => g i +ᵥ ↑(H i))
-- Mathlib.SetTheory.Ordinal.Arithmetic
/-- **Alias** of `Ordinal.isSuccLimit_mul_right`. -/
Ordinal.isSuccLimit_mul : ∀ {a b : Ordinal.{u_4}}, 0 < a → Order.IsSuccLimit b → Order.IsSuccLimit (a * b)
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.State.mk : ℕ →
  Lean.SubExpr.PosMap Lean.Elab.Info →
    Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator → Lean.PrettyPrinter.Delaborator.State
-- Init.Data.Nat.Lemmas
Nat.pred_eq_succ_iff : ∀ {n m : ℕ}, n - 1 = m + 1 ↔ n = m + 2
-- Mathlib.Logic.Equiv.PartialEquiv
/-- Two equivalent partial equivs have the same target.  -/
PartialEquiv.EqOnSource.target_eq : ∀ {α : Type u_1} {β : Type u_2} {e e' : PartialEquiv α β}, e ≈ e' → e.target = e'.target
-- Mathlib.Order.Nucleus
Nucleus.mk_le_mk : ∀ {X : Type u_1} [inst : SemilatticeInf X] (toInfHom₁ toInfHom₂ : InfHom X X)
  (le_apply₁ : ∀ (x : X), toInfHom₁.toFun (toInfHom₁.toFun x) ≤ toInfHom₁.toFun x)
  (le_apply₂ : ∀ (x : X), toInfHom₂.toFun (toInfHom₂.toFun x) ≤ toInfHom₂.toFun x)
  (idempotent₁ : ∀ (x : X), x ≤ toInfHom₁.toFun x) (idempotent₂ : ∀ (x : X), x ≤ toInfHom₂.toFun x),
  { toInfHom := toInfHom₁, idempotent' := le_apply₁, le_apply' := idempotent₁ } ≤
      { toInfHom := toInfHom₂, idempotent' := le_apply₂, le_apply' := idempotent₂ } ↔
    toInfHom₁ ≤ toInfHom₂
-- Mathlib.Data.Vector.Basic
List.Vector.mOfFn_pure : ∀ {m : Type u_6 → Type u_7} [inst : Monad m] [LawfulMonad m] {α : Type u_6} {n : ℕ} (f : Fin n → α),
  (List.Vector.mOfFn fun i => pure (f i)) = pure (List.Vector.ofFn f)
-- Mathlib.Topology.Sheaves.Stalks
/-- If two sections have the same germ at `x`,
then their restrictions to some open neighborhood `W` of `x` are equal.  -/
TopCat.Presheaf.germ_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {FC : C → C → Type u_1} {CC : C → Type v} [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
  [instCC : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] (F : TopCat.Presheaf C X)
  {U V : TopologicalSpace.Opens ↑X} (x : ↑X) (mU : x ∈ U) (mV : x ∈ V)
  (s : CategoryTheory.ToType (F.obj (Opposite.op U))) (t : CategoryTheory.ToType (F.obj (Opposite.op V))),
  (CategoryTheory.ConcreteCategory.hom (F.germ U x mU)) s = (CategoryTheory.ConcreteCategory.hom (F.germ V x mV)) t →
    ∃ W,
      ∃ (_ : x ∈ W),
        ∃ iU iV,
          (CategoryTheory.ConcreteCategory.hom (F.map iU.op)) s = (CategoryTheory.ConcreteCategory.hom (F.map iV.op)) t
-- Mathlib.RingTheory.GradedAlgebra.Basic
GradedRing.proj_apply : ∀ {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : Semiring A]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_5 : GradedRing 𝒜] (i : ι) (r : A),
  (GradedRing.proj 𝒜 i) r = ↑(((DirectSum.decompose 𝒜) r) i)
-- Aesop.Rule
Aesop.RegularRule.name : Aesop.RegularRule → Aesop.RuleName
-- Mathlib.Topology.Algebra.Group.GroupTopology
/-- Group topologies on `γ` form a complete lattice, with `⊥` the discrete topology and `⊤` the
indiscrete topology.

The infimum of a collection of group topologies is the topology generated by all their open sets
(which is a group topology).

The supremum of two group topologies `s` and `t` is the infimum of the family of all group
topologies contained in the intersection of `s` and `t`.  -/
GroupTopology.instCompleteSemilatticeInf : {α : Type u} → [inst : Group α] → CompleteSemilatticeInf (GroupTopology α)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The (right) homology map `S₁.rightHomology ⟶ S₂.rightHomology` induced by a morphism
`S₁ ⟶ S₂` of short complexes.  -/
CategoryTheory.ShortComplex.rightHomologyMap : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        [inst_2 : S₁.HasRightHomology] →
          [inst_3 : S₂.HasRightHomology] → (S₁ ⟶ S₂) → (S₁.rightHomology ⟶ S₂.rightHomology)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.insertMax.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (r' : Std.DTreeMap.Internal.Impl α β) →
      (motive : Std.DTreeMap.Internal.Impl.Tree α β (r'.size + 1) → Sort u_3) →
        (x : Std.DTreeMap.Internal.Impl.Tree α β (r'.size + 1)) →
          ((r'' : Std.DTreeMap.Internal.Impl α β) →
              (hr''₁ : r''.Balanced) →
                (hr''₂ : r''.size = r'.size + 1) → motive { impl := r'', balanced_impl := hr''₁, size_impl := hr''₂ }) →
            motive x
-- Mathlib.NumberTheory.ModularForms.Basic
/-- **Alias** of `FunLike.coe_smul`. -/
CuspForm.coe_smul : ∀ {M : Type u_1} {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : SMul M F]
  [inst_2 : SMul M β] [IsSMulApply M F α β] (n : M) (f : F), ⇑(n • f) = n • ⇑f
-- Aesop.Tree.TreeM
Aesop.TreeM.Context.mk.sizeOf_spec : ∀ (currentIteration : Aesop.Iteration) (ruleSet : Aesop.LocalRuleSet),
  sizeOf { currentIteration := currentIteration, ruleSet := ruleSet } = 1 + sizeOf currentIteration + sizeOf ruleSet
-- Init.Data.List.Find
List.IsInfix.lookup_eq_none : ∀ {α : Type u_2} [inst : BEq α] {β : Type u_1} {k : α} {l₁ l₂ : List (α × β)},
  l₁ <:+: l₂ → List.lookup k l₂ = none → List.lookup k l₁ = none
-- Mathlib.Data.Finsupp.Defs
Finsupp.unique_ext : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] [inst_1 : Unique α] {f g : α →₀ M}, f default = g default → f = g
-- Lean.Compiler.NameMangling
Lean.mkPackageSymbolPrefix : Option Lean.PkgId → String
-- Mathlib.SetTheory.Ordinal.Notation
ONote.instRepr : Repr ONote
-- Lean.Data.Lsp.Extra
/-- Never build dependencies.  -/
Lean.Lsp.DependencyBuildMode.never : Lean.Lsp.DependencyBuildMode
-- Mathlib.Data.Set.Lattice.Image
Set.preimage_iInter₂ : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_8} {f : α → β} {s : (i : ι) → κ i → Set β},
  f ⁻¹' ⋂ i, ⋂ j, s i j = ⋂ i, ⋂ j, f ⁻¹' s i j
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
add_le_mul_two_add : ∀ {R : Type u} [inst : Semiring R] [inst_1 : Preorder R] {a b : R} [ZeroLEOneClass R] [MulPosMono R] [AddLeftMono R],
  2 ≤ a → 0 ≤ b → a + (2 + b) ≤ a * (2 + b)
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Comma.mapLeft.eq_1 : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ : CategoryTheory.Functor A T} (l : L₁ ⟶ L₂)
  (hl :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
      P (CategoryTheory.CategoryStruct.comp (l.app X.left) X.hom)),
  CategoryTheory.MorphismProperty.Comma.mapLeft R l hl =
    CategoryTheory.MorphismProperty.Comma.lift
      ((CategoryTheory.MorphismProperty.Comma.forget L₂ R P Q W).comp (CategoryTheory.Comma.mapLeft R l)) hl ⋯ ⋯
-- Init.Data.Array.Lemmas
Array.flatten_replicate_singleton : ∀ {n : ℕ} {α : Type u_1} {a : α}, (Array.replicate n #[a]).flatten = Array.replicate n a
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological_i₃ : ∀ (r : ℤ) (pq : ℤ × ℤ) (hr : 2 ≤ r),
  CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological.i₃ r pq hr = WithBotTop.coe (pq.2 + r - 1)
-- Mathlib.Algebra.BigOperators.Fin
Fin.partialProd_succ : ∀ {M : Type u_2} [inst : Monoid M] {n : ℕ} (f : Fin n → M) (j : Fin n),
  Fin.partialProd f j.succ = Fin.partialProd f j.castSucc * f j
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- Uniform integrability is preserved by restriction of the functions to a set.  -/
MeasureTheory.UnifIntegrable.indicator : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {f : ι → α → β} {p : ENNReal},
  MeasureTheory.UnifIntegrable f p μ → ∀ (E : Set α), MeasureTheory.UnifIntegrable (fun i => E.indicator (f i)) p μ
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- Composition of lax functors.  -/
CategoryTheory.LaxFunctor.comp : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {D : Type u₃} →
          [inst_2 : CategoryTheory.Bicategory D] →
            CategoryTheory.LaxFunctor B C → CategoryTheory.LaxFunctor C D → CategoryTheory.LaxFunctor B D
-- Mathlib.CategoryTheory.Abelian.Transfer
CategoryTheory.ShrinkHoms.instAdditiveFunctor : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.LocallySmall.{w, v_1, u_1} C]
  [inst_2 : CategoryTheory.Preadditive C], (CategoryTheory.ShrinkHoms.functor C).Additive
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.instInhabitedRuleExpr : Inhabited Aesop.Frontend.RuleExpr
-- Mathlib.RingTheory.HopfAlgebra.Basic
HopfAlgebra.sum_antipode_mul_eq_smul : ∀ {R : Type u} {A : Type v} {ι : Type u_1} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : HopfAlgebra R A]
  {a : A} (repr : Coalgebra.Repr R a ι),
  ∑ i ∈ repr.index, (HopfAlgebraStruct.antipode R) (repr.left i) * repr.right i = CoalgebraStruct.counit a • 1
-- Init.GrindInstances.Ring.BitVec
Lean.Grind.instPowBitVecUint : ∀ {w : ℕ}, Lean.Grind.ToInt.Pow (BitVec w) (Lean.Grind.IntInterval.uint w)
-- Mathlib.Algebra.Group.Defs
NPow.toPow.eq_1 : ∀ {M : Type u_2} [inst : NPow M], NPow.toPow = { pow := fun x n => NPow.npow n x }
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
IsAddCyclic.exists_generator : ∀ {α : Type u_1} [inst : AddGroup α] [IsAddCyclic α], ∃ g, ∀ (x : α), x ∈ AddSubgroup.zmultiples g
-- Init.Data.Slice.List.Lemmas
instSliceableListSliceNat_2.eq_1 : ∀ {α : Type u},
  instSliceableListSliceNat_2 =
    {
      mkSlice := fun xs range =>
        match xs.internalRepresentation.stop with
        | none => Std.Rci.Sliceable.mkSlice xs.internalRepresentation.list range.lower...*
        | some stop => Std.Rco.Sliceable.mkSlice xs.internalRepresentation.list range.lower...stop }
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mfderiv_snd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {x : M × M'},
  mfderiv% Prod.snd x = ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)
-- Lean.Elab.PatternVar
_private.Lean.Elab.PatternVar.0.Lean.Elab.Term.CollectPatternVars.collect.processCtorAppCore : Lean.Syntax →
  Array Lean.Elab.Term.NamedArg → Array Lean.Elab.Term.Arg → Bool → Lean.Elab.Term.CollectPatternVars.M Lean.Syntax
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
AlgebraicTopology.DoldKan.QInfty_f_idem : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (n : ℕ),
  CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.QInfty.f n) (AlgebraicTopology.DoldKan.QInfty.f n) =
    AlgebraicTopology.DoldKan.QInfty.f n
-- Mathlib.Order.SuccPred.Basic
Order.pred_bot : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] [inst_2 : OrderBot α], Order.pred ⊥ = ⊥
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- A nonzero weighted-homogeneous polynomial of weighted degree `n` has weighted total degree
`n`.  -/
MvPolynomial.IsWeightedHomogeneous.weighted_total_degree : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {φ : MvPolynomial σ R}
  {n : M} [inst_2 : SemilatticeSup M] {w : σ → M},
  MvPolynomial.IsWeightedHomogeneous w φ n → φ ≠ 0 → MvPolynomial.weightedTotalDegree' w φ = ↑n
-- Aesop.Tree.Data
Aesop.Goal.isExhausted : Aesop.Goal → BaseIO Bool
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_diff_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {fallback : β},
  k ∉ m₂ → Std.ExtDHashMap.Const.getD (m₁ \ m₂) k fallback = Std.ExtDHashMap.Const.getD m₁ k fallback
-- Mathlib.NumberTheory.DirichletCharacter.Basic
/-- The fact that `d` divides `n` when `χ` factors through a Dirichlet character at level `d`  -/
DirichletCharacter.FactorsThrough.dvd : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} {χ : DirichletCharacter R n} {d : ℕ}, χ.FactorsThrough d → d ∣ n
-- Init.Data.Int.Gcd
Int.gcd_add_left_left_of_dvd : ∀ {m k : ℤ} (n : ℤ), m ∣ k → (k + n).gcd m = n.gcd m
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.denote : {α : Type u_1} → [Lean.Grind.IntModule α] → Lean.Grind.Linarith.Context α → Lean.Grind.Linarith.Poly → α
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
MonotoneOn.intervalIntegrable : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ]
  [inst_2 : ConditionallyCompleteLinearOrder E] [OrderTopology E] [SecondCountableTopology E] {u : ℝ → E} {a b : ℝ},
  MonotoneOn u (Set.uIcc a b) → IntervalIntegrable u μ a b
-- Mathlib.Topology.UniformSpace.Basic
Uniform.continuousOn_iff'_left : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : TopologicalSpace β] {f : β → α} {s : Set β},
  ContinuousOn f s ↔ ∀ b ∈ s, Filter.Tendsto (fun x => (f x, f b)) (nhdsWithin b s) (uniformity α)
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
/-- The orbit of the fixing subgroup of `sᶜ` (i.e. the moving subgroup of `s`) is a subset of `s`  -/
orbit_fixingSubgroup_compl_subset : ∀ (M : Type u_1) (α : Type u_2) [inst : Group M] [inst_1 : MulAction M α] {s : Set α} {a : α},
  a ∈ s → MulAction.orbit (↥(fixingSubgroup M sᶜ)) a ⊆ s
-- Mathlib.Analysis.InnerProductSpace.GramMatrix
Matrix.gram_single : ∀ {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : DecidableEq n] (i : n) (x : E),
  Matrix.gram 𝕜 (Pi.single i x) = Matrix.single i i (inner 𝕜 x x)
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- Return the rewrite tactic that performs the rewrite.  -/
Mathlib.Tactic.LibraryRewrite.tacticSyntax : Mathlib.Tactic.LibraryRewrite.Rewrite → Option ℕ → Option Lean.Name → Lean.MetaM (Lean.TSyntax `tactic)
-- Mathlib.FieldTheory.Relrank
Subfield.relrank_inf_mul_relrank_of_le : ∀ {E : Type v} [inst : Field E] {A B : Subfield E} (C : Subfield E),
  A ≤ B → A.relrank (B ⊓ C) * B.relrank C = A.relrank C
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate : ∀ {R : Type u_1} {A : Type u_2} {p : outParam (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} [self : NonUnitalContinuousFunctionalCalculus R A p]
  (a : A),
  p a →
    ∃ φ,
      Continuous ⇑φ ∧
        Function.Injective ⇑φ ∧
          φ { toContinuousMap := ContinuousMap.restrict (quasispectrum R a) (ContinuousMap.id R), map_zero' := ⋯ } = a ∧
            (∀ (f : ContinuousMapZero (↑(quasispectrum R a)) R), quasispectrum R (φ f) = Set.range ⇑f) ∧
              ∀ (f : ContinuousMapZero (↑(quasispectrum R a)) R), p (φ f)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicofork.π_comp_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  {I : CategoryTheory.Limits.MultispanIndex J C} (K₁ K₂ : CategoryTheory.Limits.Multicofork I) (f : K₁ ⟶ K₂) (b : J.R),
  CategoryTheory.CategoryStruct.comp (K₁.π b) f.hom = K₂.π b
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
contMDiffOn_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] {s : Set M} {n : WithTop ℕ∞}
  [inst_11 : Zero M'], ContMDiffOn I I' n 0 s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Real.tan_ne_zero_iff : ∀ {θ : ℝ}, Real.tan θ ≠ 0 ↔ ∀ (k : ℤ), ↑k * Real.pi / 2 ≠ θ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.of_forall_getKey?_unit_eq : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {t₁ t₂ : Std.TreeMap α Unit cmp},
  (∀ (k : α), t₁.getKey? k = t₂.getKey? k) → t₁.Equiv t₂
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.Scheme.Hom.surjective : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Surjective f], Function.Surjective ⇑f
-- Mathlib.Analysis.Normed.Group.Hom
/-- A `NormedAddGroupHom` is *norm-nonincreasing* if `‖f v‖ ≤ ‖v‖` for all `v`.  -/
NormedAddGroupHom.NormNoninc : {V : Type u_1} →
  {W : Type u_2} →
    [inst : SeminormedAddCommGroup V] → [inst_1 : SeminormedAddCommGroup W] → NormedAddGroupHom V W → Prop
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.isCompact_closedCell`. -/
Topology.CWComplex.isCompact_closedCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] {n : ℕ}
  {i : Topology.RelCWComplex.cell C n}, IsCompact (Topology.RelCWComplex.closedCell n i)
-- Std.Data.Iterators.Producers.Repeat
Std.Iterators.Types.RepeatIterator.mk.inj : ∀ {α : Type u} {f : α → α} {next next_1 : α}, { next := next } = { next := next_1 } → next = next_1
-- Mathlib.Topology.Order.Completion
/-- A continuous embedding of `α` into `Fill α`.  -/
Order.Fill.some : {α : Type u_1} → [inst : LinearOrder α] → α ↪o Order.Fill α
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.addRightMono : AddRightMono Cardinal.{u_1}
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.IsCharNeTwoNF.a₃ : ∀ {R : Type u_1} {inst : CommRing R} {W : WeierstrassCurve R} [self : W.IsCharNeTwoNF], W.a₃ = 0
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.IsAdmissible.getElem_lt : ∀ {m : ℕ} {L : List ℕ}, SimplexCategoryGenRel.IsAdmissible m L → ∀ {k : ℕ} {hk : k < L.length}, L[k] < m + L.length
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the smallest key in the tree map, returning `none` if the
map is empty.
 -/
Std.DTreeMap.Raw.Const.minEntry? : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap.Raw α (fun x => β) cmp → Option (α × β)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.splitAtPred.match_3.congr_eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (x : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)) (a : α) (as : List α),
  x = a :: as →
    (match x with
      | [] => h_1 ()
      | a :: as => h_2 a as) ≍
      h_2 a as
-- Std.Time.Notation
/-- Defines a syntax for zoned datetime values. It expects a string representing a datetime and a
timezone information as a term.

Example:
`zoned("2024-10-13T15:00:00", timezone)`
 -/
Std.Time.«termZoned(_,_)» : Lean.ParserDescr
-- Mathlib.Data.Set.Lattice
Set.nonempty_of_union_eq_top_of_nonempty : ∀ {α : Type u_1} {ι : Type u_12} (t : Set ι) (s : ι → Set α), Nonempty α → ⋃ i ∈ t, s i = ⊤ → t.Nonempty