mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Sigma.Order
Sigma.Lex.le_def : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LT ι] [inst_1 : (i : ι) → LE (α i)] {a b : Σₗ (i : ι), α i},
  a ≤ b ↔ a.fst < b.fst ∨ ∃ (h : a.fst = b.fst), h ▸ a.snd ≤ b.snd
-- Mathlib.Analysis.Calculus.Rademacher
/-- *Rademacher's theorem*: a function between finite-dimensional real vector spaces which is
Lipschitz on a set is differentiable almost everywhere in this set.  -/
LipschitzOnWith.ae_differentiableWithinAt_of_mem : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {F : Type u_2} [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace ℝ F] {C : NNReal} {s : Set E}
  {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] [μ.IsAddHaarMeasure] {f : E → F},
  LipschitzOnWith C f s → ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.instPartialOrder : {E : Type u_3} → [inst : Group E] → PartialOrder (GroupSeminorm E)
-- Mathlib.Topology.Algebra.ProperConstSMul
/-- The preimage of a compact set under `(c • ·)` is a compact set.  -/
IsCompact.preimage_smul : ∀ {M : Type u_1} {X : Type u_2} [inst : SMul M X] [inst_1 : TopologicalSpace X] [ProperConstSMul M X] {s : Set X},
  IsCompact s → ∀ (c : M), IsCompact ((fun x => c • x) ⁻¹' s)
-- ProofWidgets.Data.Html
ProofWidgets.Jsx.jsxText.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_diff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, (m₁ \ m₂).getKey? k = if k ∈ m₂ then none else m₁.getKey? k
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
/-- Constructor for morphisms from `X.opcycles`.  -/
CategoryTheory.Abelian.SpectralObject.descOpcycles : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          (X : CategoryTheory.Abelian.SpectralObject C ι) →
            {i j k : ι} →
              (f : i ⟶ j) →
                (g : j ⟶ k) →
                  (n₀ n₁ : ℤ) →
                    (hn₁ : n₀ + 1 = n₁) →
                      {A : C} →
                        (x : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f) ⟶ A) →
                          CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) x = 0 → (X.opcycles f g n₁ ⟶ A)
-- Mathlib.Data.Nat.Bits
/-- `bxor` denotes the `xor` function i.e. the exclusive-or function on type `Bool`.  -/
_private.Mathlib.Data.Nat.Bits.0.termBxor : Lean.ParserDescr
-- Mathlib.Algebra.Group.Prod
MonoidHom.snd_comp_inr : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  (MonoidHom.snd M N).comp (MonoidHom.inr M N) = MonoidHom.id N
-- Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
/-- `convexCombPair` in an affine space is the affine line map.  -/
AddTorsor.convexCombPair_eq_lineMap : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] (s t : R)
  (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : P),
  Convexity.convexCombPair s t hs ht h x y = (AffineMap.lineMap y x) s
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.baseChange_equation : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R) {S : Type s} [inst_1 : CommRing S] {A : Type u}
  [inst_2 : CommRing A] {B : Type v} [inst_3 : CommRing B] [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  {f : A →ₐ[S] B},
  Function.Injective ⇑f → ∀ (P : Fin 3 → A), (W'.baseChange B).Equation (⇑f ∘ P) ↔ (W'.baseChange A).Equation P
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- The functor `(f : α → C) ↦ ∏ᶜ f`.  -/
CategoryTheory.Limits.Pi.functor : (α : Type w₂) →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [CategoryTheory.Limits.HasProductsOfShape α C] → CategoryTheory.Functor (α → C) C
-- Lean.Elab.InfoTree.Types
Lean.Elab.ChoiceInfo.mk.injEq : ∀ (toElabInfo toElabInfo_1 : Lean.Elab.ElabInfo),
  ({ toElabInfo := toElabInfo } = { toElabInfo := toElabInfo_1 }) = (toElabInfo = toElabInfo_1)
-- Mathlib.Control.LawfulFix
Pi.monotoneUncurry_coe : ∀ (α : Type u_1) (β : α → Type u_2) (γ : (a : α) → β a → Type u_3) [inst : (x : α) → (y : β x) → Preorder (γ x y)]
  (f : (x : α) → (y : β x) → γ x y) (x : Sigma β), (Pi.monotoneUncurry α β γ) f x = Sigma.uncurry f x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getEntryGE!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited (α × β)] {k : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getEntryGE! k = t₂.getEntryGE! k
-- Init.Control.Lawful.MonadLift.Instances
ExceptT.instLawfulMonadLift : ∀ {m : Type u → Type v} [inst : Monad m] [LawfulMonad m] {ε : Type u}, LawfulMonadLift m (ExceptT ε m)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.Normal.of_conjugate_fixed : ∀ {G : Type u_2} [inst : Group G] {H : Subgroup G}, (∀ (g : G), MulAut.conj g • H = H) → H.Normal
-- Lean.Elab.Do.Legacy
/-- `pullExitPointsAux rs c` auxiliary method for `pullExitPoints`, `rs` is the set of update variable in the current path.   -/
Lean.Elab.Term.Do.pullExitPointsAux : Lean.Elab.Term.Do.VarSet →
  Lean.Elab.Term.Do.Code →
    StateRefT' IO.RealWorld (Array Lean.Elab.Term.Do.JPDecl) Lean.Elab.TermElabM Lean.Elab.Term.Do.Code
-- Mathlib.Data.Nat.Cast.Defs
AddMonoidWithOne.toOne : {R : Type u_2} → [self : AddMonoidWithOne R] → One R
-- Mathlib.Data.Finset.Image
Finset.coe_image : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α}, ↑(Finset.image f s) = f '' ↑s
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.cancel_right : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {σ : Type u_6} {τ : Type u_7} {ψ : Type u_8}
  [inst : Semiring A] [inst_1 : Semiring B] [inst_2 : Semiring C] [inst_3 : SetLike σ A] [inst_4 : SetLike τ B]
  [inst_5 : SetLike ψ C] {𝒜 : ι → σ} {ℬ : ι → τ} {𝒞 : ι → ψ} {g₁ g₂ : ℬ →+*ᵍ 𝒞} {f : 𝒜 →+*ᵍ ℬ},
  Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.RepresentationTheory.Basic
Representation.asGroupHom_apply : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring k] [inst_1 : Group G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρ : Representation k G V) (g : G), ↑(ρ.asGroupHom g) = ρ g
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.coe_comp' : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  {C : Type u_4} [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : TopologicalSpace C] (h : B →A[R] C)
  (f : A →A[R] B), ⇑(h.comp f) = ⇑h ∘ ⇑f
-- Init.Data.UInt.Bitwise
UInt16.and_lt_add_one : ∀ {b c : UInt16}, c ≠ -1 → b &&& c < c + 1
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.closedBall_sdiff_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, Metric.closedBall x ε \ Metric.ball x ε = Metric.sphere x ε
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
QuaternionGroup.instInhabited : {n : ℕ} → Inhabited (QuaternionGroup n)
-- Mathlib.Order.WellFoundedSet
Finset.isPWO : ∀ {α : Type u_2} [inst : Preorder α] (s : Finset α), (↑s).IsPWO
-- Std.Time.Date.Unit.Year
/-- Converts the `Year` offset to a `Month` offset.
 -/
Std.Time.Year.Offset.toMonths : Std.Time.Year.Offset → Std.Time.Month.Offset
-- Mathlib.Data.Finsupp.Pointwise
Finsupp.coe_pointwise_smul : ∀ {α : Type u₁} {β : Type u₂} [inst : Semiring β] (f : α → β) (g : α →₀ β), ⇑(f • g) = f • ⇑g
-- Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
SSet.instFiniteCoprod : ∀ (X Y : SSet) [X.Finite] [Y.Finite], (X ⨿ Y).Finite
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [inst_2 : Std.LawfulBEqCmp cmp] (h : t.WF) {l : List (α × β)} {k : α}
  (contains : (List.map Prod.fst l).contains k = false) {h' : k ∈ t.insertMany l}, (t.insertMany l)[k] = t.get k ⋯
-- Mathlib.LinearAlgebra.Matrix.HadamardMatrix
/-- The transpose of a Hadamard matrix is Hadamard.

Unlike `IsHadamard.conjTranspose` this requires commutativity: over a noncommutative ring the
transpose of a Hadamard matrix need not be Hadamard.  -/
Matrix.IsHadamard.transpose : ∀ {n : Type u_2} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R]
  [inst_3 : StarRing R] {A : Matrix n n R}, A.IsHadamard → A.transpose.IsHadamard
-- Mathlib.Probability.Martingale.OptionalStopping
/-- The converse direction of the optional stopping theorem, i.e. a strongly adapted integrable
process `f` is a submartingale if for all bounded stopping times `τ` and `π` such that `τ ≤ π`, the
stopped value of `f` at `τ` has expectation smaller than its stopped value at `π`.  -/
MeasureTheory.submartingale_of_expected_stoppedValue_mono : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration ℕ m0}
  {f : ℕ → Ω → ℝ} [MeasureTheory.SigmaFiniteFiltration μ 𝒢],
  MeasureTheory.StronglyAdapted 𝒢 f →
    (∀ (i : ℕ), MeasureTheory.Integrable (f i) μ) →
      (∀ (τ π : Ω → ℕ∞),
          MeasureTheory.IsStoppingTime 𝒢 τ →
            MeasureTheory.IsStoppingTime 𝒢 π →
              τ ≤ π →
                (∃ N, ∀ (ω : Ω), π ω ≤ ↑N) →
                  ∫ (x : Ω), MeasureTheory.stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), MeasureTheory.stoppedValue f π x ∂μ) →
        MeasureTheory.Submartingale f 𝒢 μ
-- Mathlib.Order.Category.Frm
Frm.Iso.mk_hom : ∀ {α β : Frm} (e : ↑α ≃o ↑β),
  (Frm.Iso.mk e).hom = Frm.ofHom { toFun := ⇑e, map_inf' := ⋯, map_top' := ⋯, map_sSup' := ⋯ }
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {P Q : CategoryTheory.Functor Cᵒᵖ A} (g : P ⟶ Q)
  (X : C) (x : Φ.fiber.obj X) {Z : A} (h : Φ.presheafFiber.obj Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x P)
      (CategoryTheory.CategoryStruct.comp (Φ.presheafFiber.map g) h) =
    CategoryTheory.CategoryStruct.comp (g.app (Opposite.op X))
      (CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x Q) h)
-- Mathlib.Data.PNat.Interval
PNat.card_fintype_Ioc : ∀ (a b : ℕ+), Fintype.card ↑(Set.Ioc a b) = ↑b - ↑a
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
/-- The equivalence between functors out of `AugmentedSimplexCategory` and augmented
cosimplicial objects.  -/
AugmentedSimplexCategory.equivAugmentedCosimplicialObject : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.Functor AugmentedSimplexCategory C ≌ CategoryTheory.CosimplicialObject.Augmented C
-- Mathlib.Order.Interval.Finset.Basic
BddBelow.finite : ∀ {α : Type u_2} [inst : Preorder α] [LocallyFiniteOrderTop α] {s : Set α}, BddBelow s → s.Finite
-- Mathlib.Topology.Category.TopCat.Opens
/-- An inducing map `f : X ⟶ Y` induces an adjunction between `Opens Y` and `Opens X`.  -/
Topology.IsInducing.adjunction : {X Y : TopCat} →
  {f : X ⟶ Y} →
    (hf : Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f)) → TopologicalSpace.Opens.map f ⊣ hf.functor
-- Mathlib.Order.Hom.Basic
Equiv.toOrderIso_toEquiv : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃ β) (h₁ : Monotone ⇑e)
  (h₂ : Monotone ⇑e.symm), (e.toOrderIso h₁ h₂).toEquiv = e
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.congr_fun : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] {f g : P1 →ᵃ[k] P2}, f = g → ∀ (x : P1), f x = g x
-- Mathlib.RepresentationTheory.Semisimple
Representation.isSemisimpleModule_iff_isSemisimpleRepresentation_ofModule : ∀ {k : Type u_1} {G : Type u_2} [inst : Monoid G] [inst_1 : Field k] (M : Type u_4) [inst_2 : AddCommGroup M]
  [inst_3 : Module (MonoidAlgebra k G) M],
  IsSemisimpleModule (MonoidAlgebra k G) M ↔ (Representation.ofModule M).IsSemisimpleRepresentation
-- Init.Control.Lawful.Instances
ReaderT.run_restoreM : ∀ {m : Type u_1 → Type u_2} {ρ α : Type u_1} [inst : Monad m] (x : stM m (ReaderT ρ m) α) (ctx : ρ),
  (restoreM x).run ctx = pure x
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.instMul : {R : Type u_1} →
  {M : Type u_4} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Mul (Module.End R M)
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- The colimit of a diagram `F : J ⥤ K ⥤ C` is isomorphic to the functor given by
the individual colimits on objects.  -/
CategoryTheory.Limits.colimitIsoFlipCompColim : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} J] →
        {K : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} K] →
            [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C] →
              (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) →
                CategoryTheory.Limits.colimit F ≅ F.flip.comp CategoryTheory.Limits.colim
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- The right inclusion `K ⟶ K.cylinder`.  -/
HomologicalComplex.cylinder.ι₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) →
            [inst_2 : DecidableRel c.Rel] →
              [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] →
                [inst_4 : K.HasCylinder] → K ⟶ K.cylinder
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
/-- Obtain a measure by giving a countably additive function that sends `∅` to `0`.  -/
MeasureTheory.Measure.ofMeasurable : {α : Type u_1} →
  [inst : MeasurableSpace α] →
    (m : (s : Set α) → MeasurableSet s → ENNReal) →
      m ∅ ⋯ = 0 →
        (∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
            Pairwise (Function.onFun Disjoint f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) →
          MeasureTheory.Measure α
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- `⊓` commutes with map.  -/
CategoryTheory.Subobject.inf_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X Y : C}
  (g : Y ⟶ X) [inst_2 : CategoryTheory.Mono g] (f₁ f₂ : CategoryTheory.Subobject Y),
  (CategoryTheory.Subobject.map g).obj (f₁ ⊓ f₂) =
    (CategoryTheory.Subobject.map g).obj f₁ ⊓ (CategoryTheory.Subobject.map g).obj f₂
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.IsImage.image_eq : ∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β},
  e.IsImage s t → ↑e '' (e.source ∩ s) = e.target ∩ t
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
complEDS'.eq_2 : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (k : ℤ), complEDS' b c d k 1 = 1
-- Mathlib.CategoryTheory.Comma.Over.Pullback
/-- Note that the binary products assumption is necessary: the existence of a right adjoint to
`Over.forget X` is equivalent to the existence of each binary product `X ⨯ -`.  -/
CategoryTheory.Over.instIsLeftAdjointForget : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C],
  (CategoryTheory.Over.forget X).IsLeftAdjoint
-- Mathlib.CategoryTheory.GlueData
/-- A gluing datum consists of
1. An index type `J`
2. An object `U i` for each `i : J`.
3. An object `V i j` for each `i j : J`.
4. A monomorphism `f i j : V i j ⟶ U i` for each `i j : J`.
5. A transition map `t i j : V i j ⟶ V j i` for each `i j : J`.

such that
6. `f i i` is an isomorphism.
7. `t i i` is the identity.
8. The pullback for `f i j` and `f i k` exists.
9. `V i j ×[U i] V i k ⟶ V i j ⟶ V j i` factors through `V j k ×[U j] V j i ⟶ V j i` via some
    `t' : V i j ×[U i] V i k ⟶ V j k ×[U j] V j i`.
10. `t' i j k ≫ t' j k i ≫ t' k i j = 𝟙 _`.
 -/
CategoryTheory.GlueData : (C : Type u₁) → [CategoryTheory.Category.{v, u₁} C] → Type (max u₁ (v + 1))
-- Init.Grind.Module.Basic
Lean.Grind.AddCommGroup.neg_eq_iff : ∀ {M : Type u} [inst : Lean.Grind.AddCommGroup M] (a b : M), -a = b ↔ a = -b
-- Mathlib.NumberTheory.ModularForms.Cusps
Subgroup.strictWidthInfty_eq_one_of_T_mem : ∀ {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)},
  ModularGroup.T ∈ Γ → (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ).strictWidthInfty = 1
-- Init.Control.Lawful.Basic
/-- `pure` before `seq` is equivalent to `Functor.map`.

This means that `pure` really is pure when occurring immediately prior to `seq`.
 -/
LawfulApplicative.pure_seq : ∀ {f : Type u → Type v} {inst : Applicative f} [self : LawfulApplicative f] {α β : Type u} (g : α → β) (x : f α),
  pure g <*> x = g <$> x
-- Mathlib.Data.Prod.Lex
lexOrd_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : Ord α] [inst_1 : Ord β], lexOrd = Prod.Lex.instOrdLexProd
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.instInhabitedSimprocDeclExtState.default : Lean.Meta.Simp.SimprocDeclExtState
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- The image of the closed interval `[0, p]` under the quotient map `𝕜 → AddCircle p` is the
entire space.  -/
AddCircle.coe_image_Icc_eq : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) [inst_1 : LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)]
  (a : 𝕜) [Archimedean 𝕜], QuotientAddGroup.mk '' Set.Icc a (a + p) = Set.univ
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.neg_mem_range_coroot_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) {x : N},
  -x ∈ Set.range ⇑P.coroot ↔ x ∈ Set.range ⇑P.coroot
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.GrindTacticM.run : {α : Type} →
  Lean.Elab.Tactic.Grind.GrindTacticM α →
    Lean.Elab.Tactic.Grind.Context →
      Lean.Elab.Tactic.Grind.State → Lean.Elab.TermElabM (α × Lean.Elab.Tactic.Grind.State)
-- Mathlib.Analysis.Convex.Mul
/-- `x^m`, `m : ℤ` is convex on `(0, +∞)` for all `m`.  -/
convexOn_zpow : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (n : ℤ),
  ConvexOn 𝕜 (Set.Ioi 0) fun x => x ^ n
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.linearMapEquivDerivation_symm_apply : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {M : Type u_1}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
  (D : Derivation R S M), (KaehlerDifferential.linearMapEquivDerivation R S).symm D = D.liftKaehlerDifferential
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_inter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α}, (m₁.inter! m₂).get? k = if Std.DTreeMap.Internal.Impl.contains k m₂ = true then m₁.get? k else none
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- If `f` is a power-multiplicative `K`-algebra norm on `L`, then `f`
is bounded above by `spectralNorm K L`.  -/
norm_le_spectralNorm : ∀ {K : Type u_2} [inst : NormedField K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L] {f : AlgebraNorm K L},
  IsPowMul ⇑f → IsNonarchimedean ⇑f → ∀ {x : L}, IsAlgebraic K x → f x ≤ spectralNorm K L x
-- Mathlib.Algebra.Star.MonoidHom
StarMonoidHom.mk.inj : ∀ {A : Type u_6} {B : Type u_7} {inst : Monoid A} {inst_1 : Star A} {inst_2 : Monoid B} {inst_3 : Star B}
  {toMonoidHom : A →* B} {map_star' : ∀ (a : A), (↑toMonoidHom).toFun (star a) = star ((↑toMonoidHom).toFun a)}
  {toMonoidHom_1 : A →* B} {map_star'_1 : ∀ (a : A), (↑toMonoidHom_1).toFun (star a) = star ((↑toMonoidHom_1).toFun a)},
  { toMonoidHom := toMonoidHom, map_star' := map_star' } = { toMonoidHom := toMonoidHom_1, map_star' := map_star'_1 } →
    toMonoidHom = toMonoidHom_1
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- The relation between the two arrows.  -/
CategoryTheory.GrothendieckTopology.Cover.Relation.r : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      {J : CategoryTheory.GrothendieckTopology C} → {S : J.Cover X} → (self : S.Relation) → self.fst.Relation self.snd
-- Mathlib.Combinatorics.Graph.Basic
Graph.bouquet_inc : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} (v : α) (edgeSet : Set β),
  (Graph.bouquet v edgeSet).Inc e x ↔ e ∈ edgeSet ∧ x = v
-- Mathlib.CategoryTheory.Preadditive.OfBiproducts
_private.Mathlib.CategoryTheory.Preadditive.OfBiproducts.0.CategoryTheory.SemiadditiveOfBinaryBiproducts.«term_+ₗ_» : Lean.TrailingParserDescr
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- The circumsphere of a simplex.  -/
Affine.Simplex.circumsphere : {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 : ℕ} → Affine.Simplex ℝ P n → EuclideanGeometry.Sphere P
-- Mathlib.Analysis.Normed.Module.Connected
Metric.isConnected_ball : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ℝ}, 0 < r → IsConnected (Metric.ball x r)
-- Init.Data.UInt.Lemmas
UInt32.ofNatClamp_uInt16ToNat : ∀ (n : UInt16), UInt32.ofNatClamp n.toNat = n.toUInt32
-- Mathlib.Topology.Maps.Strict.Basic
/-- **Alias** of `IsClosedMap.isStrictMap`.

---

A closed continuous map is a strict map.  -/
Topology.IsClosedMap.isStrictMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsClosedMap f → Continuous f → Topology.IsStrictMap f
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.sum_nsmul : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] (s : Finset ι) (n : ℕ) (f : ι → M),
  ∑ x ∈ s, n • f x = n • ∑ x ∈ s, f x
-- Mathlib.Data.Int.GCD
Nat.xgcd_zero_left : ∀ {s t : ℤ} {r' : ℕ} {s' t' : ℤ}, Nat.xgcdAux 0 s t r' s' t' = (r', s', t')
-- Init.Data.BitVec.Basic
/-- Multiplies two bitvectors. This can be interpreted as either signed or unsigned multiplication
modulo `2^n`. Usually accessed via the `*` operator.

SMT-LIB name: `bvmul`.
 -/
BitVec.mul : {n : ℕ} → BitVec n → BitVec n → BitVec n
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctor.id_mapComp_inv : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  ((CategoryTheory.StrictlyUnitaryPseudofunctor.id B).mapComp f g).inv =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g)