mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_antitoneOn_of_integrand_ae : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_2 : PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E]
  [ClosedIciTopology E] {β : Type u_6} [inst_6 : Preorder β] {f : α → β → E} {s : Set β},
  (∀ᵐ (x : α) ∂μ, AntitoneOn (f x) s) →
    (∀ a ∈ s, MeasureTheory.Integrable (fun x => f x a) μ) → AntitoneOn (fun b => ∫ (x : α), f x b ∂μ) s
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- **Alias** of `ModelWithCorners.extendCoordChange_source_mem_nhdsWithin'`. -/
OpenPartialHomeomorph.extend_coord_change_source_mem_nhdsWithin' : ∀ {𝕜 : 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} {e e' : OpenPartialHomeomorph M H} {x : M},
  x ∈ e.source →
    x ∈ e'.source → (ModelWithCorners.extendCoordChange e e').source ∈ nhdsWithin (↑(e.extend I) x) (Set.range ↑I)
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_fiberwise : ∀ {β : Type u_2} {γ : Type u_3} (f : β → ENNReal) (g : β → γ), ∑' (x : γ) (b : ↑(g ⁻¹' {x})), f ↑b = ∑' (i : β), f i
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.coe_iSup_of_directed : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Sort u_9}
  [Nonempty ι] (S : ι → Submodule R M), Directed (fun x1 x2 => x1 ≤ x2) S → ↑(iSup S) = ⋃ i, ↑(S i)
-- Mathlib.Algebra.Order.Module.Defs
le_smul_iff_one_le_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Monoid α] [inst_1 : Zero β] [inst_2 : MulAction α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [SMulPosMono α β] [SMulPosReflectLE α β], 0 < b → (b ≤ a • b ↔ 1 ≤ a)
-- Mathlib.CategoryTheory.Sites.CompatiblePlus
CategoryTheory.GrothendieckTopology.plusCompIso_whiskerLeft_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  [inst_3 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [inst_4 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [inst_5 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] {F G : CategoryTheory.Functor D E}
  (η : F ⟶ G) (P : CategoryTheory.Functor Cᵒᵖ D)
  [inst_7 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F]
  [inst_8 :
    ∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F]
  [inst_9 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ G]
  [inst_10 :
    ∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan G]
  {Z : CategoryTheory.Functor Cᵒᵖ E} (h : J.plusObj (P.comp G) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((J.plusObj P).whiskerLeft η)
      (CategoryTheory.CategoryStruct.comp (J.plusCompIso G P).hom h) =
    CategoryTheory.CategoryStruct.comp (J.plusCompIso F P).hom
      (CategoryTheory.CategoryStruct.comp (J.plusMap (P.whiskerLeft η)) h)
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MRefinePat.parse : Lean.TSyntax `mrefinePat → Lean.MacroM Lean.Parser.Tactic.MRefinePat
-- Mathlib.Topology.MetricSpace.CauSeqFilter
/-- A complete normed field is complete as a metric space, as Cauchy sequences converge by
assumption and this suffices to characterize completeness.  -/
completeSpace_of_cauSeq_isComplete : ∀ {β : Type v} [inst : NormedField β] [CauSeq.IsComplete β norm], CompleteSpace β
-- Mathlib.Algebra.Category.Ring.Limits
RingCat.forget₂AddCommGroup_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ RingCat AddCommGrpCat)
-- Mathlib.Algebra.Order.Interval.Basic
instNegNonemptyInterval : {α : Type u_2} → [inst : AddCommGroup α] → [inst_1 : PartialOrder α] → [IsOrderedAddMonoid α] → Neg (NonemptyInterval α)
-- Mathlib.LinearAlgebra.DirectSum.TensorProduct
TensorProduct.directSumLeft_tmul_lof : ∀ (R : Type u) [inst : CommSemiring R] (S : Type u_1) [inst_1 : Semiring S] [inst_2 : Algebra R S] {ι₁ : Type v₁}
  [inst_3 : DecidableEq ι₁] {M₁ : ι₁ → Type w₁} {M₂' : Type w₂'} [inst_4 : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)]
  [inst_5 : AddCommMonoid M₂'] [inst_6 : (i₁ : ι₁) → Module R (M₁ i₁)] [inst_7 : Module R M₂']
  [inst_8 : (i₁ : ι₁) → Module S (M₁ i₁)] [inst_9 : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)] (i : ι₁) (x : M₁ i)
  (y : M₂'),
  (TensorProduct.directSumLeft R S M₁ M₂') ((DirectSum.lof S ι₁ M₁ i) x ⊗ₜ[R] y) =
    (DirectSum.lof S ι₁ (fun i => TensorProduct R (M₁ i) M₂') i) (x ⊗ₜ[R] y)
-- Mathlib.CategoryTheory.Triangulated.Adjunction
CategoryTheory.Equivalence.IsTriangulated.instIsTriangulatedFunctor : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.Limits.HasZeroObject D] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : CategoryTheory.Preadditive D] [inst_6 : CategoryTheory.HasShift C ℤ] [inst_7 : CategoryTheory.HasShift D ℤ]
  [inst_8 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_10 : CategoryTheory.Pretriangulated C]
  [inst_11 : CategoryTheory.Pretriangulated D] (E : C ≌ D) [inst_12 : E.functor.CommShift ℤ]
  [inst_13 : E.inverse.CommShift ℤ] [E.IsTriangulated], E.functor.IsTriangulated
-- Mathlib.Data.Nat.Choose.Multinomial
Multiset.multinomial_nsmul_singleton : ∀ (k n : ℕ), (k • {n}).multinomial = Nat.multinomial (Finset.range k) fun x => n
-- Mathlib.Algebra.Ring.CompTypeclasses
/-- Construct a `RingHomInvPair` from both directions of a ring equiv.

This is not an instance, as for equivalences that are involutions, a better instance
would be `RingHomInvPair e e`.
 -/
RingHomInvPair.of_ringEquiv_symm : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] (e : R₁ ≃+* R₂), RingHomInvPair ↑e.symm ↑e
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The minimal distance to a set is Lipschitz in point with constant 1  -/
Metric.lipschitz_infDist_pt : ∀ {α : Type u} [inst : PseudoMetricSpace α] (s : Set α), LipschitzWith 1 fun x => Metric.infDist x s
-- Mathlib.Algebra.GroupWithZero.Indicator
Set.inter_indicator_one : ∀ {ι : Type u_1} {M₀ : Type u_4} [inst : MulZeroOneClass M₀] {s t : Set ι},
  (s ∩ t).indicator 1 = s.indicator 1 * t.indicator 1
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.instVAdd.eq_1 : ∀ {G : Type u_2} [inst : AddGroup G] (H : AddSubgroup G), H.instVAdd = H.op.vadd
-- Init.Data.Vector.Lemmas
Vector.empty_append : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n}, #v[] ++ xs = Vector.cast ⋯ xs
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.measurable_withDensity : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_2} [inst : MeasurableSpace β]
  {f : β → α → ENNReal} [MeasureTheory.SFinite μ],
  Measurable (Function.uncurry f) → Measurable fun b => μ.withDensity (f b)
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.Uniformizer.ext_iff : ∀ {Γ : Type u_1} {inst : LinearOrderedCommGroupWithZero Γ} {A : Type u_2} {inst_1 : Ring A} {v : Valuation A Γ}
  {hv : v.IsRankOneDiscrete} {x y : v.Uniformizer}, x = y ↔ x.val = y.val
-- Init.Meta.Defs
Lean.instQuoteBoolMkStr1 : Lean.Quote Bool
-- Init.Data.UInt.Lemmas
UInt64.ofFin_sub : ∀ (a b : Fin UInt64.size), UInt64.ofFin (a - b) = UInt64.ofFin a - UInt64.ofFin b
-- Mathlib.Data.Setoid.Basic
Setoid.mk_eq_top : ∀ {α : Type u_1} {r : α → α → Prop} (iseqv : Equivalence r), { r := r, iseqv := iseqv } = ⊤ ↔ r = ⊤
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  {k k' : α} {fallback : β} {f : β → β},
  Std.ExtDTreeMap.Const.getD (Std.ExtDTreeMap.Const.modify t k f) k' fallback =
    if cmp k k' = Ordering.eq then (Option.map f (Std.ExtDTreeMap.Const.get? t k)).getD fallback
    else Std.ExtDTreeMap.Const.getD t k' fallback
-- Lean.Util.Trace
/-- True if the `trace.profiler` data should be retained for export - either to a file
(`trace.profiler.output`) or via the local HTTP server (`trace.profiler.serve`). When true, code
that would otherwise consume the trace state as messages must leave it intact.
 -/
Lean.trace.profiler.isExporting : Lean.Options → Bool
-- Plausible.Shrinkable
Plausible.Fin.shrinkable : {n : ℕ} → Plausible.Shrinkable (Fin n.succ)
-- Mathlib.Data.SetLike.Basic
/-- The partial order induced from a `SetLike` instance by inclusion.

A partial order defined as `.ofSetLike` will automatically make available an instance
of `IsConcreteLE`.
 -/
PartialOrder.ofSetLike : (A : Type u_1) → (B : Type u_2) → [SetLike A B] → PartialOrder A
-- Mathlib.Data.PFunctor.Univariate.M
_private.Mathlib.Data.PFunctor.Univariate.M.0.PFunctor.M.isubtree.match_1.splitter : {F : PFunctor.{u_1, u_2}} →
  (motive : PFunctor.Approx.Path F → F.M → Sort u_3) →
    (x : PFunctor.Approx.Path F) →
      (x_1 : F.M) →
        ((x : F.M) → motive [] x) →
          ((a : F.A) → (i : F.B a) → (ps : List F.Idx) → (x : F.M) → motive (⟨a, i⟩ :: ps) x) → motive x x_1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Replicate
Std.Tactic.BVDecide.BVExpr.bitblast.blastReplicate : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {newWidth : ℕ} →
        (aig : Std.Sat.AIG α) →
          Std.Tactic.BVDecide.BVExpr.bitblast.ReplicateTarget aig newWidth → Std.Sat.AIG.RefVecEntry α newWidth
-- Init.Data.Iterators.Lemmas.Combinators.ULift
_private.Init.Data.Iterators.Lemmas.Combinators.ULift.0.Std.IterM.step_uLift.match_1.eq_2 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it' h
-- Mathlib.Data.Finmap
/-- `Disjoint s₁ s₂` holds if `s₁` and `s₂` have no keys in common.  -/
Finmap.Disjoint : {α : Type u} → {β : α → Type v} → Finmap β → Finmap β → Prop
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `IsDedekindDomain.idealFactorsFunOfQuotHom`.

---

The map from ideals of `R` dividing `I` to the ideals of `A` dividing `J` induced by
a homomorphism `f : R/I →+* A/J`  -/
idealFactorsFunOfQuotHom : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing A] →
        [IsDedekindDomain A] →
          {I : Ideal R} →
            {J : Ideal A} → {f : R ⧸ I →+* A ⧸ J} → Function.Surjective ⇑f → { p // p ∣ I } →o { p // p ∣ J }
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.id_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.OplaxFunctor B C) (a : B),
  (CategoryTheory.Oplax.StrongTrans.id F).app a = (CategoryTheory.Oplax.OplaxTrans.id F).app a
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.upperCentralSeries_eq_top_iff_nilpotencyClass_le`. -/
upperCentralSeries_eq_top_iff_nilpotencyClass_le : ∀ {G : Type u_1} [inst : Group G] [hG : Group.IsNilpotent G] {n : ℕ},
  Subgroup.upperCentralSeries G n = ⊤ ↔ Group.nilpotencyClass G ≤ n
-- Mathlib.Order.ConditionallyCompletePartialOrder.Defs
ConditionallyCompletePartialOrderInf.toPartialOrder : {α : Type u_3} → [self : ConditionallyCompletePartialOrderInf α] → PartialOrder α
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.le_wp_adapt_ExceptT_apply : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ε ε' α : Type u}
  {post : α → Pred} {epost : EPost.Cons✝ (ε' → Pred) EPred} (f : ε → ε') (x : ExceptT ε m α),
  Lean.Order.PartialOrder.rel (Std.Internal.Do.wp x post (EPost.Cons.mk✝ (fun e => epost.head (f e)) epost.tail))
    (Std.Internal.Do.wp (ExceptT.adapt f x) post epost)
-- Init.Data.List.Control
_private.Init.Data.List.Control.0.List.findSome?.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → ((b : β) → motive (some b)) → (Unit → motive none) → motive x
-- Mathlib.LinearAlgebra.TensorProduct.Graded.External
/-- Auxiliary construction used to build `TensorProduct.gradedComm`.

This operates on direct sums of tensors instead of tensors of direct sums.  -/
TensorProduct.gradedCommAux : (R : Type u_1) →
  {ι : Type u_2} →
    [inst : CommSemiring ι] →
      [Module ι (Additive ℤˣ)] →
        [DecidableEq ι] →
          (𝒜 : ι → Type u_3) →
            (ℬ : ι → Type u_4) →
              [inst : CommRing R] →
                [inst_1 : (i : ι) → AddCommGroup (𝒜 i)] →
                  [inst_2 : (i : ι) → AddCommGroup (ℬ i)] →
                    [inst_3 : (i : ι) → Module R (𝒜 i)] →
                      [inst_4 : (i : ι) → Module R (ℬ i)] →
                        (DirectSum (ι × ι) fun i => TensorProduct R (𝒜 i.1) (ℬ i.2)) →ₗ[R]
                          DirectSum (ι × ι) fun i => TensorProduct R (ℬ i.1) (𝒜 i.2)
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.minKeyD_modifyKey : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : β → β},
      (Std.Internal.List.Const.modifyKey k f l).isEmpty = false →
        ∀ {fallback : α},
          Std.Internal.List.minKeyD (Std.Internal.List.Const.modifyKey k f l) fallback =
            if (Std.Internal.List.minKeyD l fallback == k) = true then k else Std.Internal.List.minKeyD l fallback
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.coe_frobeniusAlgEquivOfAlgebraic_iterate : ∀ (K : Type u_1) [inst : Field K] [inst_1 : Fintype K] (L : Type u_3) [inst_2 : Field L] [inst_3 : Algebra K L]
  [inst_4 : Algebra.IsAlgebraic K L] (n : ℕ),
  (⇑(FiniteField.frobeniusAlgEquivOfAlgebraic K L))^[n] = fun x => x ^ Fintype.card K ^ n
-- Mathlib.Analysis.Convex.Cone.Extension
RieszExtension.exists_top : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] (s : PointedCone ℝ E) (p : E →ₗ.[ℝ] ℝ),
  (∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x) →
    (∀ (y : E), ∃ x, ↑x + y ∈ s) → ∃ q ≥ p, q.domain = ⊤ ∧ ∀ (x : ↥q.domain), ↑x ∈ s → 0 ≤ ↑q x
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type with `1` and inverse is an `InvOneClass` if `β` is an `InvOneClass`.  -/
FunLike.invOneClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : One F] →
          [inst_2 : Inv F] → [inst_3 : InvOneClass β] → [IsOneApply F α β] → [IsInvApply F α β] → InvOneClass F
-- Mathlib.CategoryTheory.Retract
/-- A retract of a retract is a retract.  -/
CategoryTheory.Retract.trans : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → CategoryTheory.Retract X Y → {Z : C} → CategoryTheory.Retract Y Z → CategoryTheory.Retract X Z
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normal_addSubgroupOf_iff_le_normalizer : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G},
  H ≤ K → ((H.addSubgroupOf K).Normal ↔ K ≤ AddSubgroup.normalizer ↑H)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
/-- Scales a monomial by a real factor `c`.  -/
Tactic.ComputeAsymptotics.Monomial.smul : Tactic.ComputeAsymptotics.Monomial → ℝ → Tactic.ComputeAsymptotics.Monomial
-- Mathlib.Analysis.Complex.Hadamard
/-- A technical lemma needed in the proof.  -/
_private.Mathlib.Analysis.Complex.Hadamard.0.Complex.HadamardThreeLines.fun_arg_eq : ∀ {l u : ℝ}, l < u → ∀ (z : ℂ), ↑l + (z / (↑u - ↑l) - ↑l / (↑u - ↑l)) * (↑u - ↑l) = z
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_alter_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {f : Option β → Option β}, (m.alter k f).contains k = (f m[k]?).isSome
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.exists_nat_ge_of_mk_nonneg : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : CommRing R] [inst_2 : IsStrictOrderedRing R] {x : R},
  0 ≤ ArchimedeanClass.mk x → ∃ n, x ≤ ↑n
-- Mathlib.Analysis.Calculus.TangentCone.Defs
/-- "Positive" tangent cone to `s` at `x`.  -/
posTangentConeAt : {E : Type v} → [inst : AddCommGroup E] → [Module ℝ E] → [TopologicalSpace E] → Set E → E → Set E
-- Mathlib.Tactic.NormNum.NatLog
/-- Given the natural number literals `eb` and `en`, returns `Nat.clog eb en`
as a natural number literal and an equality proof.
Panics if `ex` or `en` aren't natural number literals.
 -/
Mathlib.Meta.NormNum.proveNatClog : (eb en : Q(ℕ)) → (ek : Q(ℕ)) × Q(Nat.clog «$eb» «$en» = «$ek»)
-- Lean.OriginalConstKind
/-- Checks whether the declaration was originally declared as a theorem; see also
`Lean.getOriginalConstKind?`. Returns `false` if the declaration was not found.
 -/
Lean.wasOriginallyTheorem : Lean.Environment → Lean.Name → Bool
-- Mathlib.Data.Int.GCD
Int.gcd_dvd_iff : ∀ {a b : ℤ} {n : ℕ}, a.gcd b ∣ n ↔ ∃ x y, ↑n = a * x + b * y
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Ordering.then.match_1.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.eq) (h_2 : (a : Ordering) → motive a),
  (match Ordering.eq with
    | Ordering.eq => h_1 ()
    | a => h_2 a) =
    h_1 ()
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- If `F : Cᵒᵖ ⥤ A` is a sheaf for a Grothendieck topology `J` on `C`,
and `S` is a cover of `X : C`, then the multifork `S.multifork F` is limit.  -/
CategoryTheory.Presheaf.IsSheaf.isLimitMultifork : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        {J : CategoryTheory.GrothendieckTopology C} →
          {P : CategoryTheory.Functor Cᵒᵖ A} →
            CategoryTheory.Presheaf.IsSheaf J P →
              {X : C} → (S : J.Cover X) → CategoryTheory.Limits.IsLimit (S.multifork P)
-- Mathlib.Algebra.Lie.Basic
zero_lie : ∀ {L : Type v} {M : Type w} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M] (m : M),
  ⁅0, m⁆ = 0
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The angle between two vectors is zero if and only if they are
nonzero and one is a positive multiple of the other.  -/
InnerProductGeometry.angle_eq_zero_iff : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  InnerProductGeometry.angle x y = 0 ↔ x ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • x
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- **Alias** of `ModelWithCorners.extendCoordChange_source`. -/
OpenPartialHomeomorph.extend_coord_change_source : ∀ {𝕜 : 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} {e e' : OpenPartialHomeomorph M H},
  (ModelWithCorners.extendCoordChange e e').source = ↑I '' (e.symm.trans e').source
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.Step.append_right : ∀ {α : Type u} {L₁ L₂ L₃ : List (α × Bool)}, FreeGroup.Red.Step L₁ L₂ → FreeGroup.Red.Step (L₁ ++ L₃) (L₂ ++ L₃)
-- Init.Grind.Attr
/-- The `=` modifier instructs `grind` to check that the conclusion of the theorem is an equality,
and then uses the left-hand side of the equality as a pattern. This may fail if not all of the arguments appear
in the left-hand side.
 -/
Lean.Parser.Attr.grindEq : Lean.ParserDescr
-- Mathlib.Data.Vector.Mem
List.Vector.mem_of_mem_tail : ∀ {α : Type u_1} {n : ℕ} (a : α) (v : List.Vector α n), a ∈ v.tail.toList → a ∈ v.toList
-- Init.SimpLemmas
decide_eq_true_eq : ∀ {p : Prop} [inst : Decidable p], (decide p = true) = p
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.instInfSet : InfSet ℝ
-- Init.Control.Do
/-- A specialization of `Option.casesOn`.  -/
Continue.runK : {α : Type u} → {β : Type v} → Option α → (Unit → β) → (α → β) → β
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.RightHomotopy.ext : ∀ {V : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} V} {inst_1 : CategoryTheory.Preadditive V}
  {u v : CategoryTheory.Arrow V} {f g : u ⟶ v} {x y : CategoryTheory.Arrow.RightHomotopy f g}, x.hom = y.hom → x = y
-- Lean.Meta.Basic
Lean.Meta.instOrElseMetaM : {α : Type} → OrElse (Lean.MetaM α)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_eq_get? : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : LawfulBEq α], m.WF → ∀ {a : α}, Std.DHashMap.Raw.Const.get? m a = m.get? a
-- Mathlib.Tactic.Algebra.Basic
/-- The type used to store the coefficients of the algebra tactic, which are expressions in `R`
kept in ring normal form and mapped into `A` by the algebraMap.

Note that these are sums, not products!  -/
Mathlib.Tactic.Algebra.BaseType : {u v : Lean.Level} →
  {R : Q(Type u)} →
    {A : Q(Type v)} → {sR : Q(CommSemiring «$R»)} → {sA : Q(CommSemiring «$A»)} → Q(Algebra «$R» «$A») → Q(«$A») → Type
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.prod_top : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  (s : NonUnitalSubsemiring R), s.prod ⊤ = NonUnitalSubsemiring.comap (NonUnitalRingHom.fst R S) s
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.ιTensorObj₃_associator_inv_assoc : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ : CategoryTheory.GradedObject I C) [inst_3 : X₁.HasTensor X₂]
  [inst_4 : (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] [inst_5 : X₂.HasTensor X₃]
  [inst_6 : X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)]
  [inst_7 : X₁.HasGoodTensor₁₂Tensor X₂ X₃] [inst_8 : X₁.HasGoodTensorTensor₂₃ X₂ X₃] (i₁ i₂ i₃ j : I)
  (h : i₁ + i₂ + i₃ = j) {Z : C}
  (h_1 :
    CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃ j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.Monoidal.associator X₁ X₂ X₃).inv j) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (X₁ i₁) (X₂ i₂) (X₃ i₃)).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h) h_1)
-- Mathlib.Analysis.InnerProductSpace.ProdL2
Submodule.coe_quotientEquivOrthogonal : ∀ {𝕜 : Type u_1} {E : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection],
  ⇑K.quotientEquivOrthogonal = ⇑(K.quotientEquivOfIsCompl Kᗮ ⋯)
-- Mathlib.Algebra.Group.Defs
/-- Any `RightCancelSemigroup` satisfies `IsRightCancelMul`.  -/
RightCancelSemigroup.toIsRightCancelMul : ∀ {G : Type u} [self : RightCancelSemigroup G], IsRightCancelMul G