mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Haar.OfBasis
Module.Basis.prod_addHaar : ∀ {ι : Type u_1} {ι' : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Fintype ι] [inst_1 : Fintype ι']
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ E] [inst_5 : NormedSpace ℝ F]
  [inst_6 : MeasurableSpace E] [inst_7 : BorelSpace E] [inst_8 : MeasurableSpace F] [inst_9 : BorelSpace F]
  [inst_10 : SecondCountableTopologyEither E F] (v : Module.Basis ι ℝ E) (w : Module.Basis ι' ℝ F),
  (v.prod w).addHaar = v.addHaar.prod w.addHaar
-- Init.Data.Range.Polymorphic.PRange
Std.Roo.instMembershipOfLT : {α : Type u} → [LT α] → Membership α (Std.Roo α)
-- Mathlib.Topology.Defs.Induced
/-- A closed embedding is an embedding with closed image.  -/
Topology.IsClosedEmbedding : {X : Type u_1} → {Y : Type u_2} → [tX : TopologicalSpace X] → [tY : TopologicalSpace Y] → (X → Y) → Prop
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The product of a strictly monotone function and a monotone function is strictly monotone.  -/
StrictMonoOn.mul_monotone' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} {s : Set β}
  [MulLeftMono α] [MulRightStrictMono α], StrictMonoOn f s → MonotoneOn g s → StrictMonoOn (fun x => f x * g x) s
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
FundamentalGroupoid.instGroupoid : {X : Type u_1} → [TopologicalSpace X] → CategoryTheory.Groupoid (FundamentalGroupoid X)
-- Mathlib.Data.Stream.Init
Stream'.coinduction : ∀ {α : Type u} {s₁ s₂ : Stream' α},
  s₁.head = s₂.head → (∀ (β : Type u) (fr : Stream' α → β), fr s₁ = fr s₂ → fr s₁.tail = fr s₂.tail) → s₁ = s₂
-- Mathlib.Combinatorics.Enumerative.Schroder
_private.Mathlib.Combinatorics.Enumerative.Schroder.0.Nat.largeSchroder.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
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetDecl.mk.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {fvarId : Lean.FVarId} {binderName : Lean.Name} {type : Lean.Expr}
  {value : Lean.Compiler.LCNF.LetValue pu} {fvarId_1 : Lean.FVarId} {binderName_1 : Lean.Name} {type_1 : Lean.Expr}
  {value_1 : Lean.Compiler.LCNF.LetValue pu},
  { fvarId := fvarId, binderName := binderName, type := type, value := value } =
      { fvarId := fvarId_1, binderName := binderName_1, type := type_1, value := value_1 } →
    fvarId = fvarId_1 ∧ binderName = binderName_1 ∧ type = type_1 ∧ value = value_1
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
fixingSubmonoid.eq_1 : ∀ (M : Type u_1) {α : Type u_2} [inst : Monoid M] [inst_1 : MulAction M α] (s : Set α),
  fixingSubmonoid M s = { carrier := {ϕ | ∀ (x : ↑s), ϕ • ↑x = ↑x}, mul_mem' := ⋯, one_mem' := ⋯ }
-- Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
/-- The property of objects in the functor category `J ⥤ C`
which preserves finite colimits.  -/
CategoryTheory.ObjectProperty.preservesFiniteColimits : {J : Type u_1} →
  {C : Type u_3} →
    [inst : CategoryTheory.Category.{v_3, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_5, u_3} C] → CategoryTheory.ObjectProperty (CategoryTheory.Functor J C)
-- Mathlib.Topology.Homotopy.Path
Path.Homotopy.coeFn_injective : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ : X} {p₀ p₁ : Path x₀ x₁}, Function.Injective DFunLike.coe
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
UniformSpace.Completion.coeRingHom.eq_1 : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : UniformSpace α] [inst_2 : IsTopologicalRing α]
  [inst_3 : IsUniformAddGroup α],
  UniformSpace.Completion.coeRingHom =
    { toFun := UniformSpace.Completion.coe', map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Geometry.Euclidean.MongePoint
/-- The Monge plane associated with vertices `i₁` and `i₂` equals that
associated with `i₂` and `i₁`.  -/
Affine.Simplex.mongePlane_comm : ∀ {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 : ℕ} (s : Affine.Simplex ℝ P (n + 2)) (i₁ i₂ : Fin (n + 3)),
  s.mongePlane i₁ i₂ = s.mongePlane i₂ i₁
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.L₂'_X₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), S.L₂'.X₁ = S.L₀.X₃
-- Mathlib.Data.Sum.Order
Sum.denselyOrdered_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β],
  DenselyOrdered (α ⊕ β) ↔ DenselyOrdered α ∧ DenselyOrdered β
-- Init.Control.Except
/-- Execute `x` and then execute `finalizer` even if `x` threw an exception  -/
tryFinally : {m : Type u → Type v} → {α β : Type u} → [MonadFinally m] → [Functor m] → m α → m β → m α
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.NormalizePattern.M : Type → Type
-- Mathlib.RingTheory.Congruence.Hom
RingCon.lift.congr_simp : ∀ {M : Type u_1} {P : Type u_3} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring P] (c : RingCon M)
  (f f_1 : M →+* P) (e_f : f = f_1) (H : c ≤ RingCon.ker f), c.lift f H = c.lift f_1 ⋯
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoidHom.instAddCommMonoid.eq_1 : ∀ {M : Type uM} {N : Type uN} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N],
  AddMonoidHom.instAddCommMonoid =
    { toAdd := AddMonoidHom.add, add_assoc := ⋯, toZero := instZeroAddMonoidHom, zero_add := ⋯, add_zero := ⋯,
      toNSMul := NSMul.ofSMul, nsmul_zero := ⋯, nsmul_succ := ⋯, add_comm := ⋯ }
-- Init.Data.SInt.Lemmas
Int64.le_toInt : ∀ (x : Int64), -2 ^ 63 ≤ x.toInt
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.unop_sInf : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : Set (Subalgebra R Aᵐᵒᵖ)), (sInf S).unop = sInf (Subalgebra.op ⁻¹' S)
-- Mathlib.Data.Finset.Powerset
/-- A version of `Finset.decidableForallOfDecidableSSubsets` with a non-dependent `p`.
Typeclass inference cannot find `hu` here, so this is not an instance.  -/
Finset.decidableForallOfDecidableSSubsets' : {α : Type u_1} →
  [DecidableEq α] →
    {s : Finset α} → {p : Finset α → Prop} → ((t : Finset α) → t ⊂ s → Decidable (p t)) → Decidable (∀ t ⊂ s, p t)
-- Mathlib.Topology.NoetherianSpace
TopologicalSpace.instNoetherianSpaceCofiniteTopology : ∀ {α : Type u_3}, TopologicalSpace.NoetherianSpace (CofiniteTopology α)
-- Mathlib.CategoryTheory.Sites.SheafHom
CategoryTheory.sheafHomSectionsEquiv_symm_apply_coe_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {F G : CategoryTheory.Sheaf J A} (φ : F ⟶ G) (X : Cᵒᵖ),
  ↑((CategoryTheory.sheafHomSectionsEquiv F G).symm φ) X = (J.overPullback A (Opposite.unop X)).map φ
-- Mathlib.Algebra.Homology.CochainComplexOpposite
CochainComplex.opEquivalence.eq_1 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C],
  CochainComplex.opEquivalence C =
    (HomologicalComplex.opEquivalence C (ComplexShape.up ℤ)).trans (ChainComplex.cochainComplexEquivalence Cᵒᵖ)
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.iterate_derivative_U_eval_zero_recurrence : ∀ {R : Type u_1} [inst : CommRing R] (n : ℤ) (k : ℕ),
  Polynomial.eval 0 ((⇑Polynomial.derivative)^[k + 2] (Polynomial.Chebyshev.U R n)) =
    -((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.U R n))
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See `le_inv_mul_iff₀` for a version with multiplication on the other side.  -/
le_inv_mul_iff₀' : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀},
  0 < c → (a ≤ c⁻¹ * b ↔ a * c ≤ b)
-- Init.Control.Lawful.Basic
map_bind : ∀ {m : Type u_1 → Type u_2} {β γ α : Type u_1} [inst : Monad m] [LawfulMonad m] (f : β → γ) (x : m α) (g : α → m β),
  f <$> (x >>= g) = do
    let a ← x
    f <$> g a
-- Mathlib.Order.Closure
ClosureOperator.closure_top : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] (c : ClosureOperator α), c ⊤ = ⊤
-- Mathlib.Data.Nat.Digits.Defs
Nat.ofDigits_cons : ∀ {b hd : ℕ} {tl : List ℕ}, Nat.ofDigits b (hd :: tl) = hd + b * Nat.ofDigits b tl
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.mk.sizeOf_spec : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] [inst_2 : SizeOf α]
  [inst_3 : SizeOf β] (toFun : α → β)
  (edist_eq' : ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (toFun x) (toFun y) = ↑r * edist x y),
  sizeOf { toFun := toFun, edist_eq' := edist_eq' } = 1 + sizeOf edist_eq'
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanStaleDependencyParams.mk.inj : ∀ {staleDependency staleDependency_1 : Lean.Lsp.DocumentUri},
  { staleDependency := staleDependency } = { staleDependency := staleDependency_1 } →
    staleDependency = staleDependency_1
-- Mathlib.LinearAlgebra.Matrix.Defs
/-- Cast a function into a matrix.

The two sides of the equivalence are definitionally equal types. We want to use an explicit cast
to distinguish the types because `Matrix` has different instances to pi types (such as `Pi.mul`,
which performs elementwise multiplication, vs `Matrix.mul`).

If you are defining a matrix, in terms of its entries, use `of (fun i j ↦ _)`. The
purpose of this approach is to ensure that terms of the form `(fun i j ↦ _) * (fun i j ↦ _)` do not
appear, as the type of `*` can be misleading.
 -/
Matrix.of : {m : Type u_2} → {n : Type u_3} → {α : Type v} → (m → n → α) ≃ Matrix m n α
-- Mathlib.Algebra.Homology.Embedding.StupidTrunc
/-- The morphism `K.stupidTrunc e ⟶ L.stupidTrunc e` induced by a morphism `K ⟶ L`.  -/
HomologicalComplex.stupidTruncMap : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
                {K L : HomologicalComplex C c'} →
                  (K ⟶ L) → (e : c.Embedding c') → [inst_3 : e.IsRelIff] → K.stupidTrunc e ⟶ L.stupidTrunc e
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- Creates a `LazyEntry` using the current metavariable context.  -/
Lean.Meta.RefinedDiscrTree.mkInitLazyEntry : Bool → Lean.MetaM Lean.Meta.RefinedDiscrTree.LazyEntry
-- Init.Data.Slice.List.Basic
instSliceableListSliceNat : {α : Type u} → Std.Rcc.Sliceable (ListSlice α) ℕ (ListSlice α)
-- Mathlib.Algebra.Group.Prod
MonoidHom.prodMap.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N] {M' : Type u_6} {N' : Type u_7}
  [inst_2 : MulOneClass M'] [inst_3 : MulOneClass N'] (f : M →* M') (g : N →* N'),
  f.prodMap g = (f.comp (MonoidHom.fst M N)).prod (g.comp (MonoidHom.snd M N))
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.instInhabited : {α : Type u_1} → [inst : MeasurableSpace α] → Inhabited (α ≃ᵐ α)
-- Lean.Elab.DeclModifiers
Lean.Elab.Modifiers.isUnsafe : Lean.Elab.Modifiers → Bool
-- Mathlib.Algebra.Module.SpanRank
Submodule.spanFinrank_eq_zero_iff_eq_bot : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {p : Submodule R M},
  p.FG → (p.spanFinrank = 0 ↔ p = ⊥)
-- Mathlib.AlgebraicGeometry.Fiber
/-- The morphism from the fiber of `Spec S ⟶ Spec R` at some prime `p` to `Spec κ(p)`
is isomorphic to the map induced by `κ(p) ⟶ κ(p) ⊗[R] S`.  -/
AlgebraicGeometry.Spec.fiberToSpecResidueFieldIso : (R S : Type u) →
  [inst : CommRing R] →
    [inst_1 : CommRing S] →
      [inst_2 : Algebra R S] →
        (p : PrimeSpectrum R) →
          CategoryTheory.Arrow.mk
              (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField
                (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S))) p) ≅
            CategoryTheory.Arrow.mk
              (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber S))))
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.GoodProducts.maxToGood_injective : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (hC : IsClosed C) (hsC : Profinite.NobelingProof.contained C (Order.succ o))
  (ho : o < Ordinal.type fun x1 x2 => x1 < x2)
  (h₁ :
    ⊤ ≤
      Submodule.span ℤ
        (Set.range
          (Profinite.NobelingProof.GoodProducts.eval
            (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o)))),
  Function.Injective (Profinite.NobelingProof.GoodProducts.MaxToGood C hC hsC ho h₁)
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.basicOpenIsoSpecAway_hom_SpecMap : ∀ {R : CommRingCat} (f : ↑R),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.basicOpenIsoSpecAway f).hom
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away f)))) =
    AlgebraicGeometry.Scheme.Opens.ι (PrimeSpectrum.basicOpen f)
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_image : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : Zero M] {s : Set α} {f : β → M} {g : α → β},
  Function.Injective g → ∀ {x : α}, (g '' s).indicator f (g x) = s.indicator (f ∘ g) x
-- Plausible.Testable
Plausible.Configuration.mk.injEq : ∀ (numInst maxSize numRetries : ℕ) (traceDiscarded traceSuccesses traceShrink traceShrinkCandidates : Bool)
  (randomSeed : Option ℕ) (quiet sorryIfNoTestable : Bool) (numInst_1 maxSize_1 numRetries_1 : ℕ)
  (traceDiscarded_1 traceSuccesses_1 traceShrink_1 traceShrinkCandidates_1 : Bool) (randomSeed_1 : Option ℕ)
  (quiet_1 sorryIfNoTestable_1 : Bool),
  ({ numInst := numInst, maxSize := maxSize, numRetries := numRetries, traceDiscarded := traceDiscarded,
        traceSuccesses := traceSuccesses, traceShrink := traceShrink, traceShrinkCandidates := traceShrinkCandidates,
        randomSeed := randomSeed, quiet := quiet, sorryIfNoTestable := sorryIfNoTestable } =
      { numInst := numInst_1, maxSize := maxSize_1, numRetries := numRetries_1, traceDiscarded := traceDiscarded_1,
        traceSuccesses := traceSuccesses_1, traceShrink := traceShrink_1,
        traceShrinkCandidates := traceShrinkCandidates_1, randomSeed := randomSeed_1, quiet := quiet_1,
        sorryIfNoTestable := sorryIfNoTestable_1 }) =
    (numInst = numInst_1 ∧
      maxSize = maxSize_1 ∧
        numRetries = numRetries_1 ∧
          traceDiscarded = traceDiscarded_1 ∧
            traceSuccesses = traceSuccesses_1 ∧
              traceShrink = traceShrink_1 ∧
                traceShrinkCandidates = traceShrinkCandidates_1 ∧
                  randomSeed = randomSeed_1 ∧ quiet = quiet_1 ∧ sorryIfNoTestable = sorryIfNoTestable_1)
-- Mathlib.Analysis.Convex.Extreme
Convex.mem_extremePoints_iff_mem_sdiff_convexHull_sdiff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [DenselyOrdered 𝕜] [Module.IsTorsionFree 𝕜 E] {A : Set E} {x : E},
  Convex 𝕜 A → (x ∈ Set.extremePoints 𝕜 A ↔ x ∈ A \ (convexHull 𝕜) (A \ {x}))
-- Mathlib.Topology.Algebra.FilterBasis
ModuleFilterBasis.smul_right : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : TopologicalSpace R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] (B : ModuleFilterBasis R M) (m₀ : M) {U : Set M}, U ∈ B → ∀ᶠ (x : R) in nhds 0, x • m₀ ∈ U
-- Init.System.IO
/-- Ensures `a` remains at least alive until the call site by holding a reference to `a`. This can be useful
for unsafe code (such as an FFI) that relies on a Lean object not being freed until after some point
in the program. At runtime, this will be a no-op as the C compiler will optimize away this call.
 -/
Runtime.hold : {α : Sort u_1} → α → BaseIO Unit
-- Mathlib.Analysis.InnerProductSpace.Continuous
ContinuousOn.inner : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {α : Type u_4} [inst_3 : TopologicalSpace α] {f g : α → E} {s : Set α},
  ContinuousOn f s → ContinuousOn g s → ContinuousOn (fun t => inner 𝕜 (f t) (g t)) s
-- Mathlib.Topology.Algebra.AffineSubspace
ContinuousAffineEquiv.affineSubspaceMap_apply : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} {W : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] (e : P ≃ᴬ[R] Q) (s : AffineSubspace R P)
  [inst_9 : Nonempty ↥s] (x : ↥s), ↑((e.affineSubspaceMap s) x) = e ↑x
-- Mathlib.RepresentationTheory.Tannaka
TannakaDuality.FiniteGroup.toRightFDRepComp_in_rightRegular : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Finite G] [IsDomain k]
  (η : CategoryTheory.Aut (TannakaDuality.FiniteGroup.forget k G)),
  ∃ s,
    ModuleCat.Hom.hom (η.hom.hom.app TannakaDuality.FiniteGroup.rightFDRep).hom =
      TannakaDuality.FiniteGroup.rightRegular s
-- Mathlib.Data.Sym.Basic
/-- Function from the symmetric product over `Option` splitting on whether or not
it contains a `none`.  -/
SymOptionSuccEquiv.encode : {α : Type u_1} → {n : ℕ} → [DecidableEq α] → Sym (Option α) n.succ → Sym (Option α) n ⊕ Sym α n.succ
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod.eq_1 : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIcoMod hp a b = b - toIcoDiv hp a b • p
-- Mathlib.Algebra.Homology.ModelCategory.Lifting
/-- The `0`-cochain from `B` to `X` given by the degreewise liftings.  -/
CochainComplex.Lifting.cochain₀ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {A B X Y : CochainComplex C ℤ} →
        {t : A ⟶ X} →
          {i : A ⟶ B} →
            {p : X ⟶ Y} →
              {b : B ⟶ Y} →
                (sq : CategoryTheory.CommSq t i p b) →
                  ((n : ℤ) → ⋯.LiftStruct) → CochainComplex.HomComplex.Cochain B X 0
-- Mathlib.Topology.ContinuousMap.LocallyConstant
LocallyConstant.indicator.congr_simp : ∀ {X : Type u_1} [inst : TopologicalSpace X] {R : Type u_5} [inst_1 : Zero R] {U U_1 : Set X} (e_U : U = U_1)
  (f f_1 : LocallyConstant X R), f = f_1 → ∀ (hU : IsClopen U), f.indicator hU = f_1.indicator ⋯
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Append
Std.Tactic.BVDecide.BVExpr.bitblast.blastAppend : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {newWidth : ℕ} →
        (aig : Std.Sat.AIG α) →
          Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget aig newWidth → Std.Sat.AIG.RefVecEntry α newWidth
-- Mathlib.Analysis.Calculus.TangentCone.Prod
/-- The product of two sets of unique differentiability at points `x` and `y` has unique
differentiability at `(x, y)`.  -/
UniqueDiffWithinAt.prod : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [inst_6 : AddCommGroup F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] {x : E} {s : Set E}
  {y : F} {t : Set F}, UniqueDiffWithinAt 𝕜 s x → UniqueDiffWithinAt 𝕜 t y → UniqueDiffWithinAt 𝕜 (s ×ˢ t) (x, y)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (t.insertMany l).getKey? k = t.getKey? k
-- Mathlib.Algebra.Free
FreeAddMagma.instLawfulTraversable : LawfulTraversable FreeAddMagma
-- Mathlib.Util.CountHeartbeats
/-- Round down the number `n` to the nearest thousand, if `approx` is `true`.
 -/
Mathlib.CountHeartbeats.roundDownIf : ℕ → Bool → String
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.instFunLikeNat : {R : Type u_1} → [inst : Zero R] → FunLike (ArithmeticFunction R) ℕ R
-- Mathlib.Algebra.Group.Pointwise.Set.Card
Set.natCard_div_le : ∀ {G : Type u_1} [inst : Group G] {s t : Set G}, Nat.card ↑(s / t) ≤ Nat.card ↑s * Nat.card ↑t
-- Mathlib.Data.List.Basic
List.head!_eq_head?_getD : ∀ {α : Type u} [inst : Inhabited α] (l : List α), l.head! = l.head?.getD default
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.all.eq_2 : ∀ {α : Type u_1} (p : α → Bool) (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α),
  RBTree.RBNode.all p (RBTree.RBNode.node c l v r) = (p v && RBTree.RBNode.all p l && RBTree.RBNode.all p r)
-- Mathlib.Analysis.Matrix.PosDef
Matrix.eigenvalues_conjTranspose_mul_self_nonneg : ∀ {m : Type u_1} {n : Type u_2} {𝕜 : Type u_3} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : RCLike 𝕜]
  (A : Matrix m n 𝕜) [inst_3 : DecidableEq n] (i : n), 0 ≤ ⋯.eigenvalues i
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_eq_false_iff_exists_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false ↔ ∃ a, a ∈ t
-- Init.Data.Array.Lemmas
Array.mem_singleton : ∀ {α : Type u_1} {a b : α}, a ∈ #[b] ↔ a = b
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instAddGroup.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : AddGroup Y],
  LocallyConstant.instAddGroup = Function.Injective.addGroup DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.Algebra.RingQuot
RingQuot.preLift : {R : Type u_1} →
  [inst : Semiring R] →
    {T : Type u_2} →
      [inst_1 : Semiring T] → {r : R → R → Prop} → {f : R →+* T} → (∀ ⦃x y : R⦄, r x y → f x = f y) → RingQuot r →+* T
-- Mathlib.Algebra.Quaternion
Quaternion.instDivisionRing : {R : Type u_1} → [inst : Field R] → [inst_1 : LinearOrder R] → [IsStrictOrderedRing R] → DivisionRing (Quaternion R)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.Slice.eq_append_of_dropSuffix?_char_eq_some : ∀ {c : Char} {s res : String.Slice}, s.dropSuffix? c = some res → s.copy = res.copy ++ String.singleton c
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
/-- An action groupoid over a free group is free. More generally, one could show that the groupoid
of elements over a free groupoid is free, but this version is easier to prove and suffices for our
purposes.

Analogous to the fact that a covering space of a graph is a graph. (A free groupoid is like a graph,
and a groupoid of elements is like a covering space.)  -/
IsFreeGroupoid.actionGroupoidIsFree : {G A : Type u} →
  [inst : Group G] → [IsFreeGroup G] → [inst_2 : MulAction G A] → IsFreeGroupoid (CategoryTheory.ActionCategory G A)
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.coe_val : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L),
  ⇑S.val = Subtype.val
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeffs_zero : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R], MvPolynomial.coeffs 0 = ∅
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.tilted_eq_withDensity_nnreal : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ℝ),
  μ.tilted f = μ.withDensity fun x => ↑(NNReal.mk (Real.exp (f x) / ∫ (x : α), Real.exp (f x) ∂μ) ⋯)
-- Mathlib.Algebra.Category.Grp.Zero
AddCommGrpCat.isZero_iff_subsingleton : ∀ {G : AddCommGrpCat}, CategoryTheory.Limits.IsZero G ↔ Subsingleton ↑G
-- Aesop.Tree.Data
Aesop.GoalId.toNat : Aesop.GoalId → ℕ
-- Mathlib.GroupTheory.Congruence.Defs
/-- The quotient of a semigroup by a congruence relation is a semigroup.  -/
Con.semigroup : {M : Type u_4} → [inst : Semigroup M] → (c : Con M) → Semigroup c.Quotient
-- Mathlib.Topology.Order.IntermediateValue
Continuous.strictMono_of_inj_boundedOrder : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  [inst_7 : BoundedOrder α] {f : α → δ}, Continuous f → f ⊥ ≤ f ⊤ → Function.Injective f → StrictMono f