mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.takeListTR.go.match_1.splitter : {α : Type u_1} →
  (motive : List ℕ → List α → Array (List α) → Sort u_2) →
    (x : List ℕ) →
      (x_1 : List α) →
        (x_2 : Array (List α)) →
          ((xs : List α) → (acc : Array (List α)) → motive [] xs acc) →
            ((n : ℕ) → (ns : List ℕ) → (xs : List α) → (acc : Array (List α)) → motive (n :: ns) xs acc) →
              motive x x_1 x_2
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Iic_castSucc : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a : Fin n),
  ∏ i ≤ a.castSucc, f i = ∏ i ≤ a, f i.castSucc
-- Lean.Elab.Do.Legacy
/-- Return `some action` if `doElem` is a `doExpr <action>` -/
Lean.Elab.Term.Do.isDoExpr? : Lean.Syntax → Option Lean.Syntax
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_sdiff' : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet t →
    autoParam (μ s ≠ ⊤) MeasureTheory.measureReal_sdiff'._auto_1 →
      autoParam (μ t ≠ ⊤) MeasureTheory.measureReal_sdiff'._auto_3 → μ.real (s \ t) = μ.real (s ∪ t) - μ.real t
-- Mathlib.Order.Concept
Concept.instSemilatticeSup : {α : Type u_2} → {β : Type u_3} → {r : α → β → Prop} → SemilatticeSup (Concept α β r)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get_diff : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {h_mem : k ∈ m₁ \ m₂}, (m₁ \ m₂).get k h_mem = m₁.get k ⋯
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- The adjoint of a bounded operator `A` from a Hilbert space `E` to another Hilbert space `F`,
denoted as `A†`.  -/
InnerProduct.«term_†» : Lean.TrailingParserDescr
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
QuadraticForm.baseChange.eq_1 : ∀ {R : Type uR} (A : Type uA) {M₂ : Type uM₂} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : AddCommGroup M₂]
  [inst_3 : Algebra R A] [inst_4 : Module R M₂] [inst_5 : Invertible 2] (Q : QuadraticForm R M₂),
  QuadraticForm.baseChange A Q = QuadraticForm.tmul QuadraticMap.sq Q
-- Mathlib.RingTheory.PicardGroup
/-- If `A` is a faithful `R`-algebra, the relative Picard group Pic(A/R) is isomorphic to
the group of the invertible `R`-submodules in `A` modulo the principal submodules.  -/
Submodule.unitsQuotEquivRelPic : (R : Type u) →
  (A : Type u_4) →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring A] →
        [inst_2 : Algebra R A] →
          [FaithfulSMul R A] →
            (Submodule R A)ˣ ⧸ (Units.map ↑(Submodule.spanSingleton R)).range ≃* ↥(CommRing.relPic R A)
-- Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
exists_one_lt_mul_of_lt' : ∀ {α : Type u} [inst : MulOneClass α] [inst_1 : Preorder α] [ExistsMulOfLE α] {a b : α} [MulLeftReflectLT α],
  a < b → ∃ c, 1 < c ∧ a * c = b
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- An `AddSubmonoid` of an `AddMonoid` inherits a zero.  -/
ZeroMemClass.zero : {A : Type u_3} →
  {M₁ : Type u_4} → [inst : SetLike A M₁] → [inst_1 : Zero M₁] → [hA : ZeroMemClass A M₁] → (S' : A) → Zero ↥S'
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_buckets_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} {c : ℕ},
  Std.DHashMap.Internal.toListModel (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity c)).buckets = []
-- Mathlib.LinearAlgebra.Projection
LinearMap.IsIdempotentElem.range_eq_ker : ∀ {S : Type u_5} [inst : Semiring S] {E : Type u_7} [inst_1 : AddCommGroup E] [inst_2 : Module S E] {p : E →ₗ[S] E},
  IsIdempotentElem p → p.range = (LinearMap.id - p).ker
-- Mathlib.Order.CompleteLattice.Finset
/-- Supremum of `s i`, `i : ι`, is equal to the supremum over `t : Finset ι` of suprema
`⨆ i ∈ t, s i`. This version works for `ι : Sort*`. See `iSup_eq_iSup_finset` for a version
that assumes `ι : Type*` but has no `PLift`s.  -/
iSup_eq_iSup_finset' : ∀ {α : Type u_2} {ι' : Sort u_7} [inst : CompleteLattice α] (s : ι' → α), ⨆ i, s i = ⨆ t, ⨆ i ∈ t, s i.down
-- Mathlib.NumberTheory.LSeries.Basic
/-- Congruence for `LSeries` with the evaluation variable `s`.  -/
LSeries_congr : ∀ {f g : ℕ → ℂ}, (∀ {n : ℕ}, n ≠ 0 → f n = g n) → ∀ (s : ℂ), LSeries f s = LSeries g s
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.coe_quotQuotToQuotSupₐ : ∀ (R : Type u) {A : Type u_1} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (I J : Ideal A),
  ⇑(DoubleQuot.quotQuotToQuotSupₐ R I J) = ⇑(DoubleQuot.quotQuotToQuotSup I J)
-- Mathlib.Algebra.Torsor.Defs
Equiv.coe_smulConst : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [inst_1 : Torsor G P] (p : P), ⇑(Equiv.smulConst p) = fun v => v • p
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisorAt.divCoeff.congr_simp : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I)
  (f : PowerSeries A) [inst_1 : IsPrecomplete I A] (i : ℕ), H.divCoeff f i = H.divCoeff f i
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
/-- `Πʳ i, [R i, A i]_[𝓕]` is `RestrictedProduct R A 𝓕`.  -/
RestrictedProduct.«termΠʳ_,[_,_]_[_]» : Lean.ParserDescr
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
TangentBundle.coe_chartAt_fst : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] (p q : TangentBundle I M),
  (↑(chartAt (ModelProd H E) q) p).1 = ↑(chartAt H q.proj) p.proj
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k : α}, k ∈ m → (m.insertManyIfNewUnit l).getKey? k = m.getKey? k
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
HopfAlgCat.forget_reflects_isos : ∀ {R : Type u} [inst : CommRing R], (CategoryTheory.forget (HopfAlgCat R)).ReflectsIsomorphisms
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.instAddSubgroupClass : ∀ {G : Type u_1} [inst : AddGroup G], AddSubgroupClass (FiniteIndexNormalAddSubgroup G) G
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.equivWithAbs_symm_equiv_symm_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  {v w : AbsoluteValue R S} {x : R},
  (WithAbs.congr v w (RingEquiv.refl R)).symm ((WithAbs.equiv w).symm x) = (WithAbs.equiv v).symm x
-- Lean.Meta.Tactic.Grind.Extension
/-- Contains all symbols used in `patterns`.  -/
Lean.Meta.Grind.EMatchTheorem.symbols : Lean.Meta.Grind.EMatchTheorem → List Lean.HeadIndex
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.guardColumn : (ℕ → Bool) → String → Lean.Parser.ParserFn
-- Mathlib.Data.Fintype.Defs
Finset.eq_univ_of_forall : ∀ {α : Type u_1} [inst : Fintype α] {s : Finset α}, (∀ (x : α), x ∈ s) → s = Finset.univ
-- Init.Data.SInt.Basic
instLEInt16 : LE Int16
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.quotientRightRelEquivQuotientLeftRel.eq_1 : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α),
  QuotientGroup.quotientRightRelEquivQuotientLeftRel s =
    { toFun := Quotient.map' (fun g => g⁻¹) ⋯, invFun := Quotient.map' (fun g => g⁻¹) ⋯, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
Homeomorph.toOpenPartialHomeomorph_target : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ₜ Y),
  e.toOpenPartialHomeomorph.target = Set.univ
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instCommGroupOfMonoidHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → CommGroup (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] → CommGroup (DirectLimit G f)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.distinct_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) t.keys
-- Mathlib.LinearAlgebra.Matrix.WithConv
instSemigroupWithConvMatrix : {m : Type u_1} → {n : Type u_2} → {α : Type u_3} → [Semigroup α] → Semigroup (WithConv (Matrix m n α))
-- Mathlib.Order.Comparable
IncompRel.symm : ∀ {α : Type u_1} {a b : α} {r : α → α → Prop}, IncompRel r a b → IncompRel r b a
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.natEnd.match_1.eq_1 : ∀ (motive : Turing.PartrecToTM2.Γ' → Sort u_1) (h_1 : Unit → motive Turing.PartrecToTM2.Γ'.consₗ)
  (h_2 : Unit → motive Turing.PartrecToTM2.Γ'.cons) (h_3 : (x : Turing.PartrecToTM2.Γ') → motive x),
  (match Turing.PartrecToTM2.Γ'.consₗ with
    | Turing.PartrecToTM2.Γ'.consₗ => h_1 ()
    | Turing.PartrecToTM2.Γ'.cons => h_2 ()
    | x => h_3 x) =
    h_1 ()
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.val_step_filterMap.match_3.eq_1 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β) (out : β)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Lean.Attributes
Lean.instInhabitedAttributeImpl.default : Lean.AttributeImpl
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.unop_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex Cᵒᵖ} (h : S.RightHomologyData), h.unop.π = h.ι.unop
-- Mathlib.Analysis.Complex.Exponential
Real.one_sub_le_exp_neg : ∀ (x : ℝ), 1 - x ≤ Real.exp (-x)
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.lt_of_neg_of_archimedean : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : CommRing R] [inst_2 : IsStrictOrderedRing R] {S : Type u_3}
  [inst_3 : LinearOrder S] [inst_4 : CommRing S] [IsStrictOrderedRing S] [Archimedean S] (f : S →+*o R) {x : R},
  0 < ArchimedeanClass.mk x → ∀ {y : S}, y < 0 → f y < x
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.StrictSegal.instIsStrictSegalObjTruncatedHAddNatOfNatTruncationOfIsStrictSegal : ∀ {X : SSet} [X.IsStrictSegal] (n : ℕ), ((SSet.truncation (n + 1)).obj X).IsStrictSegal
-- Mathlib.Algebra.Module.Equiv.Basic
/-- Multiplying by a nonzero element `a` of the field `K` is a linear equivalence.  -/
LinearEquiv.smulOfNeZero : (K : Type u_3) →
  (M : Type u_5) → [inst : Field K] → [inst_1 : AddCommGroup M] → [inst_2 : Module K M] → (a : K) → a ≠ 0 → M ≃ₗ[K] M
-- Mathlib.RingTheory.NoetherNormalization
_private.Mathlib.RingTheory.NoetherNormalization.0.NoetherNormalization.t1_comp_t1_neg : ∀ {k : Type u_1} [inst : Field k] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) k) (c : k),
  (NoetherNormalization.T1 f c).comp (NoetherNormalization.T1 f (-c)) = AlgHom.id k (MvPolynomial (Fin (n + 1)) k)
-- Mathlib.Data.Set.Function
Equiv.bijOn_swap : ∀ {α : Type u_1} {s : Set α} [inst : DecidableEq α] {a b : α}, a ∈ s → b ∈ s → Set.BijOn (⇑(Equiv.swap a b)) s s
-- Mathlib.Analysis.Normed.Lp.WithLp
/-- Lift an equivalence to `WithLp`.  -/
WithLp.congr : (p : ENNReal) → {V : Type u_4} → {V' : Type u_5} → V ≃ V' → WithLp p V ≃ WithLp p V'
-- Mathlib.Algebra.Group.Hom.Defs
/-- Additive group homomorphisms preserve integer scaling.  -/
AddMonoidHom.map_zsmul : ∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : SubtractionMonoid β] (f : α →+ β) (n : ℤ) (g : α),
  f (n • g) = n • f g
-- Lean.Meta.Tactic.Induction
Lean.Meta.AltVarNames.explicit : Lean.Meta.AltVarNames → Bool
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegrable_iff_integrableOn_Ioc_of_le : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] [TopologicalSpace.PseudoMetrizableSpace ε]
  {f : ℝ → ε} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
  a ≤ b → (IntervalIntegrable f μ a b ↔ MeasureTheory.IntegrableOn f (Set.Ioc a b) μ)
-- Init.Data.Bool
Bool.eq_self_or : ∀ {a b : Bool}, a = (a || b) ↔ b = true → a = true
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- The norm squared function for `PreInnerProductSpace.Core` structure.  -/
_private.Mathlib.Analysis.InnerProductSpace.Defs.0.InnerProductSpace.Core.termNormSqF : Lean.ParserDescr
-- Init.Data.String.Extra
_private.Init.Data.String.Extra.0.String.removeNumLeadingSpaces.consumeSpaces.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.pow_apply : ∀ {M : Type u_1} (r : ℕ) (l : Mathlib.Tactic.FieldSimp.NF M),
  l ^ r =
    List.map
      (fun x =>
        match x with
        | (a, x) => (↑r * a, x))
      l
-- Mathlib.Order.BooleanAlgebra.Basic
sdiff_sdiff_right : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], x \ (y \ z) = x \ y ⊔ x ⊓ y ⊓ z
-- Mathlib.Geometry.Manifold.Algebra.Monoid
instFunLikeContMDiffAddMonoidMorphism : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {n : WithTop ℕ∞} →
      {H : Type u_2} →
        [inst_1 : TopologicalSpace H] →
          {E : Type u_3} →
            [inst_2 : NormedAddCommGroup E] →
              [inst_3 : NormedSpace 𝕜 E] →
                {I : ModelWithCorners 𝕜 E H} →
                  {G : Type u_4} →
                    [inst_4 : AddMonoid G] →
                      [inst_5 : TopologicalSpace G] →
                        [inst_6 : ChartedSpace H G] →
                          {H' : Type u_5} →
                            [inst_7 : TopologicalSpace H'] →
                              {E' : Type u_6} →
                                [inst_8 : NormedAddCommGroup E'] →
                                  [inst_9 : NormedSpace 𝕜 E'] →
                                    {I' : ModelWithCorners 𝕜 E' H'} →
                                      {G' : Type u_7} →
                                        [inst_10 : AddMonoid G'] →
                                          [inst_11 : TopologicalSpace G'] →
                                            [inst_12 : ChartedSpace H' G'] →
                                              FunLike (ContMDiffAddMonoidMorphism I I' n G G') G G'
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
/-- If `f` has derivative `f'` a.e. on `[d, b]` and `η` is positive, then there is a collection of
pairwise disjoint closed subintervals of `[a, b]` of total length `b - a` where the slope of `f`
on each subinterval `[x, y]` differs from `f' x` by at most `η`.  -/
exists_dist_slope_lt_pairwiseDisjoint_hasSum : ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {f f' : ℝ → F} {d b η : ℝ},
  d ≤ b →
    (∀ᵐ (x : ℝ), x ∈ Set.Ioo d b → HasDerivAt f (f' x) x) →
      0 < η →
        ∃ u,
          (∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η) ∧
            (u.PairwiseDisjoint fun z => Set.Icc z.1 z.2) ∧ HasSum (fun z => (↑z).2 - (↑z).1) (b - d)
-- Lean.CoreM
Lean.instMonadRuntimeExceptionStateRefT' : {m : Type → Type} → {ω σ : Type} → [Lean.MonadRuntimeException m] → Lean.MonadRuntimeException (StateRefT' ω σ m)
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
ZetaAsymptotics.tendsto_Gamma_term_aux : Filter.Tendsto (fun s => 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)) (nhdsWithin 1 {1}ᶜ)
  (nhds (-(↑Real.eulerMascheroniConstant + Complex.log (4 * ↑Real.pi)) / 2))
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
Lean.Elab.ConfigEval.addConstInfo' : Lean.Syntax → Lean.Name → Lean.Elab.TermElabM Unit
-- Mathlib.Algebra.Field.Subfield.Basic
RingHom.map_fieldRange : ∀ {K : Type u} {L : Type v} {M : Type w} [inst : DivisionRing K] [inst_1 : DivisionRing L] [inst_2 : DivisionRing M]
  (g : L →+* M) (f : K →+* L), Subfield.map g f.fieldRange = (g.comp f).fieldRange
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.mk_repr : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : ι → M} {x : M} (hli : LinearIndependent R v) (hsp : ⊤ ≤ Submodule.span R (Set.range v)),
  (Module.Basis.mk hli hsp).repr x = hli.repr ⟨x, ⋯⟩
-- Mathlib.LinearAlgebra.Matrix.Permutation
Equiv.Perm.permMatrix.eq_1 : ∀ {n : Type u_1} (R : Type u_2) [inst : DecidableEq n] (σ : Equiv.Perm n) [inst_1 : Zero R] [inst_2 : One R],
  Equiv.Perm.permMatrix R σ = (Equiv.toPEquiv σ).toMatrix
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- The oriented angle between two vectors is `π` if and only if the unoriented angle is `π`.  -/
Orientation.oangle_eq_pi_iff_angle_eq_pi : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑Real.pi ↔ InnerProductGeometry.angle x y = Real.pi
-- Mathlib.Analysis.Normed.Module.Complemented
Submodule.coe_continuous_linearProjOfClosedCompl : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {p q : Subspace 𝕜 E} (h : IsCompl p q) (hp : IsClosed ↑p)
  (hq : IsClosed ↑q), ↑(Submodule.linearProjOfClosedCompl p q h hp hq) = Submodule.projectionOnto p q h
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.FinitaryExtensive.vanKampen : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryExtensive C]
  {F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C}
  (c : CategoryTheory.Limits.Cocone F) (hc : CategoryTheory.Limits.IsColimit c), CategoryTheory.IsVanKampenColimit c
-- Mathlib.Analysis.CStarAlgebra.Classes
instNonUnitalCommCStarAlgebraSubtypeMemNonUnitalStarSubalgebraComplexElementalOfIsStarNormal : {A : Type u_1} →
  [inst : NonUnitalCStarAlgebra A] →
    (x : A) → [IsStarNormal x] → NonUnitalCommCStarAlgebra ↥(NonUnitalStarAlgebra.elemental ℂ x)
-- Mathlib.Order.Interval.Set.WithBotTop
WithTop.Icc_coe : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Icc ↑a ↑b = WithTop.some '' Set.Icc a b
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.compHom_domain : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) (g : Y ⟶ Z), (f.compHom g).domain = f.domain
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.PreInstance.mk.sizeOf_spec : ∀ (proof : Lean.Expr) (assignment : Array Lean.Expr),
  sizeOf { proof := proof, assignment := assignment } = 1 + sizeOf proof + sizeOf assignment
-- Mathlib.Analysis.ODE.PicardLindelof
ODE.FunSpace.continuous_compProj : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {r L : NNReal}
  (α : ODE.FunSpace t₀ x₀ r L), Continuous α.compProj
-- Mathlib.LinearAlgebra.Dual.Lemmas
Module.Dual.range_eq_top_of_ne_zero : ∀ {K : Type u_4} {V₁ : Type u_5} [inst : DivisionSemiring K] [inst_1 : AddCommMonoid V₁] [inst_2 : Module K V₁]
  {f : Module.Dual K V₁}, f ≠ 0 → LinearMap.range f = ⊤
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.ι_comp_lift : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] {A : Type u_3} [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (f : X → A), ⇑((FreeAlgebra.lift R) f) ∘ FreeAlgebra.ι R = f
-- Mathlib.Analysis.Normed.Group.Uniform
nndist_mul_mul_le : ∀ {E : Type u_2} [inst : SeminormedCommGroup E] (a₁ a₂ b₁ b₂ : E),
  nndist (a₁ * a₂) (b₁ * b₂) ≤ nndist a₁ b₁ + nndist a₂ b₂
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.subtype_comp_d₀₁_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{max u u_1, u, u} k G) {Z : ModuleCat k}
  (h : ModuleCat.of k (G → ↑A) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom A.ρ.invariants.subtype)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.d₀₁ A) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.instIsIsoToRightDerivedZero' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] {X : C}
  (P : CategoryTheory.InjectiveResolution X), CategoryTheory.IsIso (P.toRightDerivedZero' F)
-- Mathlib.Algebra.Order.Monoid.Defs
nonneg_add_self_iff : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] {a : α}, 0 ≤ a + a ↔ 0 ≤ a
-- Batteries.Data.List.Perm
List.Subperm.cons_self : ∀ {α : Type u_1} {l : List α} {a : α}, l.Subperm (a :: l)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
tangentMap_prod_right : ∀ {𝕜 : 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'] {p : TangentBundle I' M'} {x₀ : M},
  tangentMap I' (I.prod I') (fun y => (x₀, y)) p = ⟨(x₀, p.proj), (0, p.snd)⟩
-- Mathlib.Topology.Algebra.NonUnitalStarAlgebra
NonUnitalStarAlgebra.elemental.le_centralizer_centralizer : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] [inst_8 : TopologicalSpace A] [inst_9 : IsSemitopologicalSemiring A]
  [inst_10 : ContinuousConstSMul R A] [inst_11 : ContinuousStar A] [T2Space A] (x : A),
  NonUnitalStarAlgebra.elemental R x ≤
    NonUnitalStarSubalgebra.centralizer R ↑(NonUnitalStarSubalgebra.centralizer R {x})
-- Mathlib.Topology.EMetricSpace.Defs
MulOpposite.instPseudoEMetricSpace.eq_1 : ∀ {α : Type u_2} [inst : PseudoEMetricSpace α],
  MulOpposite.instPseudoEMetricSpace = PseudoEMetricSpace.induced MulOpposite.unop inst
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coeToSet_coeToSubmodule : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (I : FractionalIdeal S P), ↑↑I = ↑I
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α}
  {v : β}, (t.insertIfNew k v).getKey? a = if cmp k a = Ordering.eq ∧ k ∉ t then some k else t.getKey? a
-- Mathlib.Probability.UniformOn
ProbabilityTheory.uniformOn_apply_finset : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [MeasurableSingletonClass Ω] [inst_2 : DecidableEq Ω] {s t : Finset Ω},
  (ProbabilityTheory.uniformOn ↑s) ↑t = ↑(s ∩ t).card / ↑s.card
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgCat.instCoeSortType : {R : Type u} → [inst : CommRing R] → CoeSort (CoalgCat R) (Type v)
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `IsAddTorsion`.

---

A predicate on an additive monoid saying that all elements are of finite order.  -/
AddMonoid.IsTorsion : (G : Type u_1) → [AddMonoid G] → Prop