mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
CategoryTheory.Functor.mapEnd.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) {D : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} D] (f : CategoryTheory.Functor C D),
  CategoryTheory.Functor.mapEnd X f = { toFun := f.map, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
LiouvilleNumber.remainder_summable : ∀ {m : ℝ}, 1 < m → ∀ (k : ℕ), Summable fun i => 1 / m ^ (i + (k + 1)).factorial
-- Mathlib.Topology.MetricSpace.HausdorffDimension
dimH_subsingleton : ∀ {X : Type u_2} [inst : EMetricSpace X] {s : Set X}, s.Subsingleton → dimH s = 0
-- Init.Data.BitVec.Lemmas
BitVec.le_of_eq : ∀ {w : ℕ} {x y : BitVec w}, x = y → x ≤ y
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKeyD_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF → ∀ {k : α} {f : β k → β k} {fallback : α}, (t.modify k f).minKeyD fallback = t.minKeyD fallback
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_maxKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false}, t.contains (t.maxKey he) = true
-- Init.Data.Iterators.Combinators.Monadic.Take
/-- Internal implementation detail of the iterator library.
This proof term ensures that a `take` always produces a finite iterator from a productive one.
 -/
Std.Iterators.Types.Take.finite : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] (self : Std.Iterators.Types.Take α m),
  self.countdown > 0 ∨ Std.Iterators.Finite α m
-- Mathlib.Algebra.CharP.Lemmas
add_pow_char_pow_of_commute : ∀ {R : Type u_1} [inst : Semiring R] {x y : R} (p n : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p],
  Commute x y → (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
-- Lean.MetavarContext
Lean.MetavarContext.LevelMVarToParam.instMonadMCtxM : Lean.MonadMCtx Lean.MetavarContext.LevelMVarToParam.M
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.subsingleton_of_isZero : ∀ {R : Type u} [inst : Semiring R] {M : SemimoduleCat R}, CategoryTheory.Limits.IsZero M → Subsingleton ↑M
-- Init.Data.Int.OfNat
Nat.ToInt.le_eq : ∀ {a b : ℕ} {a' b' : ℤ}, ↑a = a' → ↑b = b' → (a ≤ b) = (a' ≤ b')
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.Away.map_map : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ}
  [inst_5 : GradedRing 𝒜] {B : Type u_4} {τ : Type u_5} [inst_6 : CommRing B] [inst_7 : SetLike τ B]
  [inst_8 : AddSubgroupClass τ B] {ℬ : ι → τ} [inst_9 : GradedRing ℬ] {C : Type u_6} {ψ : Type u_7}
  [inst_10 : CommRing C] [inst_11 : SetLike ψ C] [inst_12 : AddSubgroupClass ψ C] {𝒞 : ι → ψ} [inst_13 : GradedRing 𝒞]
  (f : 𝒜 →+*ᵍ ℬ) (g : ℬ →+*ᵍ 𝒞) (s : A) (x : HomogeneousLocalization.Away 𝒜 s),
  (HomogeneousLocalization.Away.map g (f s)) ((HomogeneousLocalization.Away.map f s) x) =
    (HomogeneousLocalization.Away.map (g.comp f) s) x
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.map_sup : ∀ {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (H₁ H₂ : G.Subgraph),
  SimpleGraph.Subgraph.map f (H₁ ⊔ H₂) = SimpleGraph.Subgraph.map f H₁ ⊔ SimpleGraph.Subgraph.map f H₂
-- Mathlib.Data.Nat.SuccPred
Fin.coe_covBy_iff : ∀ {n : ℕ} {a b : Fin n}, ↑a ⋖ ↑b ↔ a ⋖ b
-- Mathlib.LinearAlgebra.Matrix.Basis
linearMap_toMatrix_mul_basis_toMatrix : ∀ {ι : Type u_1} {ι' : Type u_2} {κ' : Type u_4} {R : Type u_5} {M : Type u_6} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_9} [inst_3 : AddCommMonoid N] [inst_4 : Module R N]
  (b : Module.Basis ι R M) (b' : Module.Basis ι' R M) (c' : Module.Basis κ' R N) (f : M →ₗ[R] N) [inst_5 : Fintype ι']
  [inst_6 : Fintype ι] [inst_7 : Finite κ'] [inst_8 : DecidableEq ι] [inst_9 : DecidableEq ι'],
  (LinearMap.toMatrix b' c') f * b'.toMatrix ⇑b = (LinearMap.toMatrix b c') f
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.decompAffineEquiv_symm_contLinear : ∀ (R : Type u_1) (S : Type u_2) (V : Type u_3) {W : Type u_4} (Q : Type u_5) [inst : Ring S] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : TopologicalSpace V] [inst_5 : IsTopologicalAddGroup V]
  [inst_6 : AddCommGroup W] [inst_7 : Module R W] [inst_8 : TopologicalSpace W] [inst_9 : Module S W]
  [inst_10 : SMulCommClass R S W] [inst_11 : ContinuousConstSMul S W] [inst_12 : AddTorsor W Q]
  [inst_13 : TopologicalSpace Q] [inst_14 : IsTopologicalAddGroup W] [inst_15 : IsTopologicalAddTorsor Q]
  (p : Q × (V →L[R] W)), ((ContinuousAffineMap.decompAffineEquiv R S V Q).symm p).contLinear = p.2
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.ColimitOfShape.prop_diag_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] {X : C} (self : P.ColimitOfShape J X) (j : J), P (self.diag.obj j)
-- Mathlib.Order.Birkhoff
OrderEmbedding.ofIsEmpty.congr_simp : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : IsEmpty α],
  OrderEmbedding.ofIsEmpty = OrderEmbedding.ofIsEmpty
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
_private.Mathlib.RingTheory.Bialgebra.MonoidAlgebra.0.MonoidAlgebra.single_mapDomainOfBialgHomFun_one : ∀ {R : Type u_1} {G : Type u_5} {H : Type u_6} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : Group G]
  [inst_3 : Group H] (f : MonoidAlgebra R G →ₐc[R] MonoidAlgebra R H) (g : G),
  MonoidAlgebra.single (MonoidAlgebra.mapDomainOfBialgHomFun✝ f g) 1 = f (MonoidAlgebra.single g 1)
-- Init.Data.Char.Ordinal
Char.ordinal_inj : ∀ {c d : Char}, c.ordinal = d.ordinal ↔ c = d
-- Mathlib.CategoryTheory.Subobject.Basic
/-- If we construct a `Subobject Y` from an explicit `f : X ⟶ Y` with `[Mono f]`,
then pick an arbitrary choice of underlying object `(Subobject.mk f : C)` back in `C`,
it is isomorphic (in `C`) to the original `X`.
 -/
CategoryTheory.Subobject.underlyingIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      (f : X ⟶ Y) →
        [inst_1 : CategoryTheory.Mono f] → CategoryTheory.Subobject.underlying.obj (CategoryTheory.Subobject.mk f) ≅ X
-- Mathlib.Dynamics.TopologicalEntropy.Subset
Dynamics.coverEntropyEntourage_closure : ∀ {X : Type u_1} {T : X → X} {V : SetRel X X} [inst : UniformSpace X],
  Continuous T →
    ∀ (F : Set X) (U : SetRel X X),
      V ∈ uniformity X → Dynamics.coverEntropyEntourage T (closure F) (V.comp U) ≤ Dynamics.coverEntropyEntourage T F U
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_add_nat_mul_pi : ∀ (x : ℝ) (n : ℕ), Real.cos (x + ↑n * Real.pi) = (-1) ^ n * Real.cos x
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- `L₀.X₂` is the kernel of `v₁₂.τ₂ : L₁.X₂ ⟶ L₂.X₂`.  -/
CategoryTheory.ShortComplex.SnakeInput.h₀τ₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (S : CategoryTheory.ShortComplex.SnakeInput C) →
        CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι S.v₀₁.τ₂ ⋯)
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.Position.mk.inj : ∀ {line character line_1 character_1 : ℕ},
  { line := line, character := character } = { line := line_1, character := character_1 } →
    line = line_1 ∧ character = character_1
-- Init.Data.BitVec.Bitblast
BitVec.intMin_sdiv_neg_one : ∀ {w : ℕ}, (BitVec.intMin w).sdiv (-1#w) = BitVec.intMin w
-- Init.Data.Stream
Std.instToStreamStringRaw : Std.ToStream String Substring.Raw
-- Mathlib.Topology.Homeomorph.Defs
HomeomorphClass.toHomeomorph_injective : ∀ {F : Type u_5} {α : Type u_6} {β : Type u_7} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : EquivLike F α β] [inst_3 : HomeomorphClass F α β], Function.Injective HomeomorphClass.toHomeomorph
-- Init.Data.UInt.Lemmas
UInt16.ne_of_lt : ∀ {a b : UInt16}, a < b → a ≠ b
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.mkOfAdjoinEqTop'_root : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : Module.Finite R S] [inst_4 : Module.Free R S] {α : S} (hα : R[α] = ⊤),
  (IsAdjoinRootMonic.mkOfAdjoinEqTop' hα).root = α
-- Init.Data.Float.Model.Float32
/-- Unpack a `Float32.Model` into the corresponding `UnpackedFloat`.  -/
Float32.Model.unpack : Float32.Model → Float.Model.UnpackedFloat
-- Mathlib.GroupTheory.Coxeter.Inversion
/-- The left inversion sequence of `ω`. The left inversion sequence of a word
$s_{i_1} \cdots s_{i_\ell}$ is the sequence
$$s_{i_1}, s_{i_1}s_{i_2}s_{i_1}, s_{i_1}s_{i_2}s_{i_3}s_{i_2}s_{i_1}, \ldots,
    s_{i_1}\cdots s_{i_\ell}\cdots s_{i_1}.$$
 -/
CoxeterSystem.leftInvSeq : {B : Type u_1} → {W : Type u_2} → [inst : Group W] → {M : CoxeterMatrix B} → CoxeterSystem M W → List B → List W
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_filter!_key_eq_false_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] {f : α → Bool},
  t.WF →
    ((Std.DTreeMap.Internal.Impl.filter! (fun a x => f a) t).isEmpty = false ↔
      ∃ k, ∃ (h : Std.DTreeMap.Internal.Impl.contains k t = true), f (t.getKey k h) = true)
-- Mathlib.Order.CompleteLattice.Basic
iSup_subtype : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {p : ι → Prop} {f : Subtype p → α},
  iSup f = ⨆ i, ⨆ (h : p i), f ⟨i, h⟩
-- Mathlib.Analysis.InnerProductSpace.Completion
Inner.inner.eq_1 : ∀ (𝕜 : Type u_4) (E : Type u_5) [self : Inner 𝕜 E], inner 𝕜 = self.1
-- Init.Tactics
/-- Syntax for trying to clear the values of all local definitions.
 -/
Lean.Parser.Tactic.clearValueStar : Lean.ParserDescr
-- Mathlib.Order.Minimal
Set.maximal_iff_forall_ssuperset : ∀ {α : Type u_2} {P : Set α → Prop} {s : Set α}, Maximal P s ↔ P s ∧ ∀ ⦃t : Set α⦄, s ⊂ t → ¬P t
-- Init.Data.String.Lemmas.Pattern.Pred
_private.Init.Data.String.Slice.0.String.Slice.Pos.skipWhile.match_1.congr_eq_2 : ∀ {s : String.Slice} (motive : Option s.Pos → Sort u_1) (x : Option s.Pos)
  (h_1 : (nextCurr : s.Pos) → motive (some nextCurr)) (h_2 : Unit → motive none),
  x = none →
    (match x with
      | some nextCurr => h_1 nextCurr
      | none => h_2 ()) ≍
      h_2 ()
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
CategoryTheory.BicategoricalCoherence.tensorRight_iso : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} (f : a ⟶ b) (g : b ⟶ b)
  [inst_1 : CategoryTheory.BicategoricalCoherence (CategoryTheory.CategoryStruct.id b) g],
  CategoryTheory.BicategoricalCoherence.iso =
    (CategoryTheory.Bicategory.rightUnitor f).symm ≪≫
      CategoryTheory.Bicategory.whiskerLeftIso f CategoryTheory.BicategoricalCoherence.iso
-- Mathlib.CategoryTheory.Limits.Connected
/-- The obvious cone of a constant functor.  -/
CategoryTheory.Limits.constCone : (J : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C] →
        (X : C) → CategoryTheory.Limits.Cone ((CategoryTheory.Functor.const J).obj X)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.equation_add_iff : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} (x₁ x₂ y₁ ℓ : R),
  W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ) ↔
    Polynomial.eval (W'.addX x₁ x₂ ℓ) (W'.addPolynomial x₁ y₁ ℓ) = 0
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.sup_eq_closure : ∀ {G : Type u_1} [inst : Group G] (H H' : Subgroup G), H ⊔ H' = Subgroup.closure (↑H ∪ ↑H')
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Manifold.LiftSourceTargetPropertyAt.codChart.congr_simp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I I_1 : ModelWithCorners 𝕜 E H} (e_I : I = I_1)
  {J J_1 : ModelWithCorners 𝕜 F G} (e_J : J = J_1) {M : Type u_10} {N : Type u_12} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n n_1 : WithTop ℕ∞}
  (e_n : n = n_1) {f f_1 : M → N} (e_f : f = f_1) {x x_1 : M} (e_x : x = x_1)
  {P P_1 : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop} (e_P : P = P_1)
  (h : Manifold.LiftSourceTargetPropertyAt I J n f x P), h.codChart = ⋯.codChart
-- Mathlib.Data.ENNReal.Operations
ENNReal.mul_pos : ∀ {a b : ENNReal}, a ≠ 0 → b ≠ 0 → 0 < a * b
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
/-- Evaluation of power series at adequate elements, as an `AlgHom`  -/
MvPowerSeries.aeval : {σ : Type u_1} →
  {R : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : UniformSpace R] →
        {S : Type u_3} →
          [inst_2 : CommRing S] →
            [inst_3 : UniformSpace S] →
              {a : σ → S} →
                [IsTopologicalSemiring R] →
                  [IsUniformAddGroup R] →
                    [IsUniformAddGroup S] →
                      [CompleteSpace S] →
                        [T2Space S] →
                          [IsTopologicalRing S] →
                            [IsLinearTopology S S] →
                              [inst_11 : Algebra R S] →
                                [ContinuousSMul R S] → MvPowerSeries.HasEval a → MvPowerSeries σ R →ₐ[R] S
-- Mathlib.Condensed.Discrete.Colimit
Condensed.lanPresheafNatIso.eq_1 : ∀ {F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))}
  (hF : (S : Profinite) → CategoryTheory.Limits.IsColimit (F.mapCocone S.asLimitCone.op)),
  Condensed.lanPresheafNatIso hF =
    CategoryTheory.NatIso.ofComponents
      (fun x =>
        match x with
        | Opposite.op S => Condensed.lanPresheafIso (hF S))
      ⋯
-- Mathlib.Analysis.Convex.Topology
isClosed_closedConvexHull : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] {s : Set E}, IsClosed ((closedConvexHull 𝕜) s)
-- Mathlib.Analysis.RCLike.Sqrt
Complex.sqrt_eq_real_add_ite : ∀ {a : ℂ}, a.sqrt = ↑√((‖a‖ + a.re) / 2) + (if 0 ≤ a.im then 1 else -1) * ↑√((‖a‖ - a.re) / 2) * Complex.I
-- Mathlib.Data.Stream.Init
Stream'.cycle_singleton : ∀ {α : Type u} (a : α), Stream'.cycle [a] ⋯ = Stream'.const a
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_eq_tprod_of_ne_one_bij : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {g : γ → α} (i : ↑(Function.mulSupport g) → β),
  Function.Injective i →
    Function.mulSupport f ⊆ Set.range i →
      (∀ (x : ↑(Function.mulSupport g)), f (i x) = g ↑x) → ∏' (x : β), f x = ∏' (y : γ), g y
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.WalkingParallelPair.zero.sizeOf_spec : sizeOf CategoryTheory.Limits.WalkingParallelPair.zero = 1
-- Init.Data.List.Lemmas
List.getLast_eq_head_reverse : ∀ {α : Type u_1} {l : List α} (h : l ≠ []), l.getLast h = l.reverse.head ⋯
-- Mathlib.LinearAlgebra.Finsupp.Pi
Finsupp.LinearEquiv.finsuppUnique_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Semiring R] [inst_2 : Module R M] (α : Type u_5)
  [inst_3 : Unique α] (f : α →₀ M), (Finsupp.LinearEquiv.finsuppUnique R M α) f = f default
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.compLinearMap_apply : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {M₂ : Type u_10} [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] (f : M [⋀^ι]→ₗ[R] N) (g : M₂ →ₗ[R] M) (v : ι → M₂), (f.compLinearMap g) v = f fun i => g (v i)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.instHasPullbacksAgainstOfHasPullbacks : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) [P.HasPullbacks]
  (P' : CategoryTheory.MorphismProperty C), P.HasPullbacksAgainst P'
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.genWrapper.build : Lean.Name → ℕ → Array Lean.Doc.ArgSpec✝ → Array Lean.Expr → Option Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Category.Grp.Limits
/-- The categorical kernel of a morphism in `AddCommGrpCat`
agrees with the usual group-theoretical kernel.
 -/
AddCommGrpCat.kernelIsoKer : {G H : AddCommGrpCat} → (f : G ⟶ H) → CategoryTheory.Limits.kernel f ≅ AddCommGrpCat.of ↥(AddCommGrpCat.Hom.hom f).ker
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.exradius_pos : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs → 0 < s.exradius signs
-- Mathlib.SetTheory.Cardinal.Cofinality.Enum
IsRegularCardinalOrder.congr_simp : ∀ (α : Type u_2) [inst : LinearOrder α] [inst_1 : WellFoundedLT α], IsRegularCardinalOrder α = IsRegularCardinalOrder α
-- Mathlib.Analysis.Analytic.Constructions
AnalyticOnNhd.div_const : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {s : Set E}
  {f : E → 𝕝}, AnalyticOnNhd 𝕜 f s → ∀ {c : 𝕝}, AnalyticOnNhd 𝕜 (fun x => f x / c) s
-- Mathlib.Algebra.Group.Hom.Instances
MonoidHom.zpow_apply : ∀ {M : Type uM} {N : Type uN} [inst : MulOneClass M] [inst_1 : CommGroup N] (f : M →* N) (z : ℤ) (x : M),
  (f ^ z) x = f x ^ z
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.reduce.eq_1 : ∀ {n : ℕ} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
  (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment),
  c.reduce assignments =
    List.foldl (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.reduce_fold_fn assignments)
      Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty c.clause
-- Mathlib.Topology.Algebra.Support
tsupport_binop_subset : ∀ {X : Type u_1} {α : Type u_2} {β : Type u_4} {γ : Type u_5} [inst : Zero α] [inst_1 : TopologicalSpace X]
  [inst_2 : Zero β] [inst_3 : Zero γ] (op : α → β → γ),
  op 0 0 = 0 → ∀ (f : X → α) (g : X → β), (tsupport fun x => op (f x) (g x)) ⊆ tsupport f ∪ tsupport g
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
norm_jacobiTheta₂_term_fderiv_ge : ∀ (n : ℤ) (z τ : ℂ), Real.pi * ↑|n| ^ 2 * ‖jacobiTheta₂_term n z τ‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
-- Mathlib.CategoryTheory.Sites.Types
/-- Given a presheaf `P` on the category of types, construct
a map `P(α) → (α → P(*))` for all type `α`.  -/
CategoryTheory.eval : (P : CategoryTheory.Functor Type uᵒᵖ (Type u)) →
  (α : Type u) → P.obj (Opposite.op α) → (α ⟶ P.obj (Opposite.op PUnit.{u + 1}))
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.residue_eq_zero_iff_sMod_eq_zero : ∀ (p : ℕ), 1 < p → (lucasLehmerResidue p = 0 ↔ LucasLehmer.sMod p (p - 2) = 0)
-- Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
InnerProductSpace.HarmonicContOnCl.sub : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f₁ f₂ : E → F} {s : Set E},
  InnerProductSpace.HarmonicContOnCl f₁ s →
    InnerProductSpace.HarmonicContOnCl f₂ s → InnerProductSpace.HarmonicContOnCl (f₁ - f₂) s
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.posPart_natCast : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Algebra ℝ A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [T2Space A] (n : ℕ), (↑n)⁺ = ↑n
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.sum_nodalWeight_mul_inv_sub_ne_zero : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} {x : F},
  Set.InjOn v ↑s → (∀ i ∈ s, x ≠ v i) → s.Nonempty → ∑ i ∈ s, Lagrange.nodalWeight s v i * (x - v i)⁻¹ ≠ 0
-- Mathlib.Algebra.Star.Subsemiring
StarSubsemiring.toSubsemiring_inj : ∀ {R : Type v} [inst : NonAssocSemiring R] [inst_1 : StarRing R] {S U : StarSubsemiring R},
  S.toSubsemiring = U.toSubsemiring ↔ S = U
-- Mathlib.Algebra.Polynomial.Roots
/-- `roots p` noncomputably gives a multiset containing all the roots of `p`,
including their multiplicities.  -/
Polynomial.roots : {R : Type u} → [inst : CommRing R] → [IsDomain R] → Polynomial R → Multiset R
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.withDensity_inv_same_le : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  AEMeasurable f μ → (μ.withDensity f).withDensity f⁻¹ ≤ μ
-- Init.Data.SInt.Lemmas
Int64.ofIntTruncate_iSizeToInt : ∀ (x : ISize), Int64.ofIntClamp x.toInt = x.toInt64
-- Mathlib.Algebra.Ring.BooleanRing
Bool.neg_eq_id : ∀ (b : Bool), -b = b
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.entryAtIdx_eq : ∀ {α : Type u} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} (htb : t.Balanced) {i : ℕ} {h : i < t.size},
  Std.DTreeMap.Internal.Impl.Const.entryAtIdx t htb i h = ((t.entryAtIdx htb i h).fst, (t.entryAtIdx htb i h).snd)
-- Mathlib.MeasureTheory.Integral.Layercake
/-- An auxiliary version of the layer cake formula (Cavalieri's principle, tail probability
formula), with a measurability assumption that would also essentially follow from the
integrability assumptions, and a sigma-finiteness assumption.

See `MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul` and
`MeasureTheory.lintegral_comp_eq_lintegral_meas_lt_mul` for the main formulations of the layer
cake formula.  -/
MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul_of_measurable_of_sigmaFinite : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℝ} {g : ℝ → ℝ} (μ : MeasureTheory.Measure α)
  [MeasureTheory.SFinite μ],
  0 ≤ f →
    Measurable f →
      (∀ t > 0, IntervalIntegrable g MeasureTheory.volume 0 t) →
        Measurable g →
          (∀ t > 0, 0 ≤ g t) →
            ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
              ∫⁻ (t : ℝ) in Set.Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
-- Mathlib.AlgebraicTopology.DoldKan.Decomposition
/-- A `MorphComponents` can be postcomposed with a morphism.  -/
AlgebraicTopology.DoldKan.MorphComponents.postComp : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : CategoryTheory.SimplicialObject C} →
      {n : ℕ} →
        {Z Z' : C} →
          AlgebraicTopology.DoldKan.MorphComponents X n Z → (Z ⟶ Z') → AlgebraicTopology.DoldKan.MorphComponents X n Z'
-- Mathlib.Data.Finset.Insert
Finset.consPiProd.eq_1 : ∀ {α : Type u_1} {s : Finset α} {a : α} (f : α → Type u_3) (has : a ∉ s) (x : (i : α) → i ∈ Finset.cons a s has → f i),
  Finset.consPiProd f has x = (x a ⋯, fun i hi => x i ⋯)
-- Mathlib.Topology.Category.CompHausLike.Basic
/-- Construct a homeomorphism from an isomorphism.  -/
CompHausLike.homeoOfIso : {P : TopCat → Prop} → {X Y : CompHausLike P} → (X ≅ Y) → ↑X.toTop ≃ₜ ↑Y.toTop
-- Mathlib.Computability.Language
Language.add_iSup : ∀ {α : Type u_1} {ι : Sort v} [Nonempty ι] (l : ι → Language α) (m : Language α), m + ⨆ i, l i = ⨆ i, m + l i
-- Mathlib.RingTheory.Regular.LinearMap
IsSMulRegular.linearMap_subsingleton_of_mem_annihilator : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] {r : R},
  IsSMulRegular M r → r ∈ Module.annihilator R N → Subsingleton (N →ₗ[R] M)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.exists_pos : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
  {g' : α → F'} {l : Filter α}, f =O[l] g' → ∃ c > 0, Asymptotics.IsBigOWith c l f g'
-- Init.Data.Array.Lemmas
Array.append_singleton : ∀ {α : Type u_1} {a : α} {as : Array α}, as ++ #[a] = as.push a