mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.Jacobian
/-- Change of variable formula for differentiable functions, set version: if a function `f` is
injective and differentiable on a null measurable set `s`, then the pushforward of the measure with
density `|(f' x).det|` on `s` is the Lebesgue measure on the image set.  -/
MeasureTheory.map_withDensity_abs_det_fderiv_eq_addHaar : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
  {f : E → E} {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure],
  MeasureTheory.NullMeasurableSet s μ →
    (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
      Set.InjOn f s →
        MeasureTheory.Measure.map f ((μ.restrict s).withDensity fun x => ENNReal.ofReal |(f' x).det|) =
          μ.restrict (f '' s)
-- Mathlib.Data.ENNReal.Operations
ENNReal.exists_lt_add_of_lt_add : ∀ {x y z : ENNReal}, x < y + z → y ≠ 0 → z ≠ 0 → ∃ y' < y, ∃ z' < z, x < y' + z'
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
/-- The data which allows to construct an `E₂`-cohomological spectral sequence
indexed by `ℤ × ℤ` from a spectral object indexed by `EInt`.  -/
CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore EInt (fun r => ComplexShape.up' (r, 1 - r)) 2
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.IsPresentation.π_desc_apply : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'}
  [inst_3 : AddCommGroup N] [inst_4 : Module A N] (s : relations.Solution N) (x : relations.G →₀ A),
  (h.desc s) (solution.π x) = s.π x
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval.eq_1 : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (f : σ → R),
  MvPolynomial.eval f = MvPolynomial.eval₂Hom (RingHom.id R) f
-- Mathlib.Data.Multiset.Bind
Multiset.rel_bind : ∀ {α : Type u_1} {β : Type v} {γ : Type u_2} {δ : Type u_3} {r : α → β → Prop} {p : γ → δ → Prop} {s : Multiset α}
  {t : Multiset β} {f : α → Multiset γ} {g : β → Multiset δ},
  Relator.LiftFun r (Multiset.Rel p) f g → Multiset.Rel r s t → Multiset.Rel p (s.bind f) (t.bind g)
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.mk_eq_div : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] (p q : Polynomial K),
  RatFunc.mk p q = (algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.RightRigidCategory.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [rightDual : (X : C) → CategoryTheory.HasRightDual X] → CategoryTheory.RightRigidCategory C
-- Mathlib.Control.Traversable.Equiv
Equiv.traverse_def : ∀ {t t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [inst : Traversable t] {m : Type u → Type u}
  [inst_1 : Applicative m] {α β : Type u} (f : α → m β) (x : t' α),
  Equiv.traverse eqv f x = ⇑(eqv β) <$> traverse f ((eqv α).symm x)
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.instFaithfulFunctorOppositeTypeShrinkYoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C],
  CategoryTheory.shrinkYoneda.{w, v, u}.Faithful
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.transport_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  (x : CategoryTheory.Grothendieck F) {c : C} (t : x.base ⟶ c), (x.transport t).base = c
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticWith.fullRange : {α : Type} → Lean.Lsp.DiagnosticWith α → Lean.Lsp.Range
-- Lean.Parser.Do
Lean.Parser.Term.doReassign.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Data.Finsupp.Option
Finsupp.some_embDomain_some : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : α →₀ M), (Finsupp.embDomain Function.Embedding.some f).some = f
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.findRev?TR.eq_1 : ∀ {α : Type u_1} (p : α → Bool) (l : List α), List.findRev?TR p l = List.find? p l.reverse
-- Init.Data.Function
/-- `LeftInverse g f` means that `g` is a left inverse to `f`. That is, `g ∘ f = id`.  -/
Function.LeftInverse : {α : Sort u_1} → {β : Sort u_2} → (β → α) → (α → β) → Prop
-- Mathlib.Algebra.Group.Action.Sum
Sum.smul_def : ∀ {M : Type u_1} {α : Type u_3} {β : Type u_4} [inst : SMul M α] [inst_1 : SMul M β] (a : M) (x : α ⊕ β),
  a • x = Sum.map (fun x => a • x) (fun x => a • x) x
-- Mathlib.FieldTheory.Finite.GaloisField
FiniteField.norm_surjective : ∀ (K : Type u_1) (K' : Type u_2) [inst : Field K] [inst_1 : Field K'] [inst_2 : Algebra K K'] [Finite K'],
  Function.Surjective ⇑(Algebra.norm K)
-- Mathlib.Order.Filter.SmallSets
Filter.frequently_smallSets : ∀ {α : Type u_1} {l : Filter α} {p : Set α → Prop}, (∃ᶠ (s : Set α) in l.smallSets, p s) ↔ ∀ t ∈ l, ∃ s ⊆ t, p s
-- Init.Data.List.Basic
List.rightpad.eq_1 : ∀ {α : Type u} (n : ℕ) (a : α) (l : List α), List.rightpad n a l = l ++ List.replicate (n - l.length) a
-- Batteries.Tactic.OpenPrivate
Lean.instDecidableEqModuleIdx_batteries : DecidableEq Lean.ModuleIdx
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.match_16.splitter : (aig : Std.Sat.AIG ℕ) →
  (upper : ℕ) →
    (h : upper < aig.decls.size) →
      (rstate : Std.Sat.AIG.toCNF.State✝ aig) →
        (motive : { out // Std.Sat.AIG.toCNF.State.IsExtensionBy✝ rstate out upper h } → Sort u_1) →
          (x : { out // Std.Sat.AIG.toCNF.State.IsExtensionBy✝ rstate out upper h }) →
            ((ret : Std.Sat.AIG.toCNF.State✝ aig) →
                (hretstate : Std.Sat.AIG.toCNF.State.IsExtensionBy✝ rstate ret upper h) → motive ⟨ret, hretstate⟩) →
              motive x
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.instAndThenDSimproc : AndThen Lean.Meta.Simp.DSimproc
-- Init.Data.Vector.Lex
Vector.lt_toArray : ∀ {α : Type u_1} {n : ℕ} [inst : LT α] {xs ys : Vector α n}, xs.toArray < ys.toArray ↔ xs < ys
-- Mathlib.Topology.Compactness.SigmaCompact
/-- If `s` is σ-compact and `f` continuous, `f(s)` is σ-compact.  -/
IsSigmaCompact.image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f → ∀ {s : Set X}, IsSigmaCompact s → IsSigmaCompact (f '' s)
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.range_fst : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S),
  Set.range ⇑(CategoryTheory.Limits.pullback.fst f g) = ⇑f ⁻¹' Set.range ⇑g
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.getEntryD : {α : Type u} →
  {β : α → Type v} → [BEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → α → (a : α) × β a → (a : α) × β a
-- Mathlib.Topology.Algebra.Support
HasCompactMulSupport.comp₂_left : ∀ {α : Type u_2} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [inst : TopologicalSpace α] [inst_1 : One β]
  [inst_2 : One γ] [inst_3 : One δ] {f : α → β} {f₂ : α → γ} {m : β → γ → δ},
  HasCompactMulSupport f → HasCompactMulSupport f₂ → m 1 1 = 1 → HasCompactMulSupport fun x => m (f x) (f₂ x)
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.gradedMonoid_eq_of_cast : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {a b : GradedMonoid (ModularForm Γ)} (h : a.fst = b.fst),
  ModularForm.mcast h a.snd ⋯ = b.snd → a = b
-- Mathlib.LinearAlgebra.Basis.VectorSpace
/-- If `f` is injective, then the left inverse composed with `f` is the identity.  -/
LinearMap.leftInverse_apply_of_inj : ∀ {K : Type u_3} {V : Type u_4} {V' : Type u_5} [inst : DivisionRing K] [inst_1 : AddCommGroup V]
  [inst_2 : AddCommGroup V'] [inst_3 : Module K V] [inst_4 : Module K V'] {f : V →ₗ[K] V'},
  f.ker = ⊥ → ∀ (x : V), f.leftInverse (f x) = x
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_add : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (a : A) (f g : R → R),
  autoParam (ContinuousOn f (spectrum R a)) cfc_add._auto_1 →
    autoParam (ContinuousOn g (spectrum R a)) cfc_add._auto_3 → cfc (fun x => f x + g x) a = cfc f a + cfc g a
-- Mathlib.Algebra.Group.Submonoid.Basic
AddSubmonoid.sup_eq_closure : ∀ {M : Type u_1} [inst : AddZeroClass M] (N N' : AddSubmonoid M), N ⊔ N' = AddSubmonoid.closure (↑N ∪ ↑N')
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.map₂Congr_inv_app_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B}
  {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : F.comp U ⟶ S.comp G) (β : G.obj T ⟶ V)
  {F' : CategoryTheory.Functor C A} {G' : CategoryTheory.Functor D B} (e₁ : F ≅ F') (e₂ : G ≅ G')
  (α' : F'.comp U ⟶ S.comp G') (β' : G'.obj T ⟶ V)
  (hα :
    CategoryTheory.CategoryStruct.comp α (S.whiskerLeft e₂.hom) =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight e₁.hom U) α')
  (hβ : β = CategoryTheory.CategoryStruct.comp (e₂.hom.app T) β') (X : CategoryTheory.CostructuredArrow S T),
  ((CategoryTheory.CostructuredArrow.map₂Congr α β e₁ e₂ α' β' hα hβ).inv.app X).left = e₁.inv.app X.left
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.instMul : {R : Type uR} →
  {A : Type uA} →
    {B : Type uB} →
      [inst : CommSemiring R] →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [inst_2 : Module R A] →
            [SMulCommClass R A A] →
              [IsScalarTower R A A] →
                [inst_5 : NonUnitalNonAssocSemiring B] →
                  [inst_6 : Module R B] → [SMulCommClass R B B] → [IsScalarTower R B B] → Mul (TensorProduct R A B)
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.arrowMap_restrictionLE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] {j : J}
  (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {j' : J} (hj' : j' ≤ j) (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂) (h₂ : i₂ ≤ j'),
  CategoryTheory.SmallObject.SuccStruct.arrowMap (CategoryTheory.SmallObject.restrictionLE F hj') i₁ i₂ h₁₂ h₂ =
    CategoryTheory.SmallObject.SuccStruct.arrowMap F i₁ i₂ h₁₂ ⋯
-- Std.Http.Data.URI.Basic
/-- Extracts the query component from a request target, if available.
Returns an empty array for targets without a query.
 -/
Std.Http.RequestTarget.query : Std.Http.RequestTarget → Std.Http.URI.Query
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.hom_ext_iff : ∀ {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.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  {X Y : CategoryTheory.Triangulated.SpectralObject C ι} {α β : X ⟶ Y}, α = β ↔ α.hom = β.hom
-- Mathlib.Analysis.Convex.Topology
Convex.combo_closure_interior_mem_interior : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E},
  Convex 𝕜 s →
    ∀ {x y : E}, x ∈ closure s → y ∈ interior s → ∀ {a b : 𝕜}, 0 ≤ a → 0 < b → a + b = 1 → a • x + b • y ∈ interior s
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.throwEvalAndSuggestFailed : {α : Type} → Lean.Try.Config → Lean.Elab.Tactic.TacticM α
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstrProof.core.injEq : ∀ (a b : Lean.Expr) (lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr) (a_1 b_1 : Lean.Expr)
  (lhs_1 rhs_1 : Lean.Meta.Grind.Arith.Linear.LinExpr),
  (Lean.Meta.Grind.Arith.Linear.EqCnstrProof.core a b lhs rhs =
      Lean.Meta.Grind.Arith.Linear.EqCnstrProof.core a_1 b_1 lhs_1 rhs_1) =
    (a = a_1 ∧ b = b_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1)
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.coe_powers : ∀ {M : Type u_1} [inst : Monoid M] (x : M), ↑(Submonoid.powers x) = Set.range fun n => x ^ n
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- An additive module object for an additive monoid object in a monoidal category acting on the
ambient category.  -/
CategoryTheory.AddMod : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (D : Type u₂) →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            (A : C) → [CategoryTheory.AddMonObj A] → Type (max u₂ v₂)
-- Lean.Meta.Tactic.Contradiction
/-- Given `e` s.t. `isGenDiseq e`, generate a bit-mask `mask` s.t. `mask[i] = true` iff
the `i`-th binder is an equality without forward dependencies.

See `processGenDiseq`
 -/
Lean.Meta.mkGenDiseqMask : Lean.Expr → Array Bool
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.swap_Q₁_natDegree : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)} (h : E ≠ ⊥),
  (Polynomial.Bivariate.swap (RatFunc.Luroth.Q₁✝ h)).natDegree = 0
-- Mathlib.Algebra.Group.Subsemigroup.Basic
Subsemigroup.coe_sInf : ∀ {M : Type u_1} [inst : Mul M] (S : Set (Subsemigroup M)), ↑(sInf S) = ⋂ s ∈ S, ↑s
-- Lean.Parser.Extra
Lean.Parser.many.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Init.Internal.Order.While
/-- `repeatM.body f` is monotone in its `recur` argument whenever `m` admits `MonadTail`.  -/
_private.Init.Internal.Order.While.0.repeatM.body_monotone_of_monadTail : ∀ {α : Type u} {m : Type u → Type v} [inst : Monad m] {β : Type u} [inst_1 : Lean.Order.MonadTail m]
  [inst_2 : Nonempty β] (f : α → m (α ⊕ β)), Lean.Order.monotone (repeatM.body f)
-- Mathlib.Algebra.Lie.Basic
lie_zero : ∀ {L : Type v} {M : Type w} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M] (x : L),
  ⁅x, 0⁆ = 0
-- Mathlib.CategoryTheory.Category.Pairwise
/-- The identity morphism in `CategoryTheory.Pairwise ι`.
 -/
CategoryTheory.Pairwise.id : {ι : Type v} → (o : CategoryTheory.Pairwise ι) → o.Hom o
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.addMonoidHomCongrRightEquiv_apply : ∀ {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [inst : AddZeroClass M] [inst_1 : AddMonoid N₁]
  [inst_2 : AddMonoid N₂] (e : N₁ ≃+ N₂) (hmn : M →+ N₁), e.addMonoidHomCongrRightEquiv hmn = e.toAddMonoidHom.comp hmn
-- Lean.Data.Lsp.Basic
Lean.Lsp.Location.uri : Lean.Lsp.Location → Lean.Lsp.DocumentUri
-- Mathlib.Analysis.Normed.Field.Basic
/-- The distance is induced by the norm.  -/
NormedField.dist_eq : ∀ {α : Type u_5} [self : NormedField α] (x y : α), dist x y = ‖-x + y‖
-- Lean.Parser.Basic
Lean.Parser.sepBy1 : Lean.Parser.Parser →
  (sep : String) → optParam Lean.Parser.Parser (Lean.Parser.symbol sep) → optParam Bool false → Lean.Parser.Parser
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePushout.hom_eq_desc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C}
  (arrows : (j : J) → B ⟶ objs j) [inst_1 : CategoryTheory.Limits.HasWidePushout B objs arrows] {X : C}
  (g : CategoryTheory.Limits.widePushout B objs arrows ⟶ X),
  g =
    CategoryTheory.Limits.WidePushout.desc
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePushout.head arrows) g)
      (fun j => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePushout.ι arrows j) g) ⋯
-- Lean.Meta.Tactic.Grind.EMatch
/-- Matches offset pattern `pArg+k` with term `e` with respect to choice `c`.
 -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.processOffset : Lean.Meta.Grind.EMatch.Choice →
  Option Lean.Meta.Grind.GenPatternInfo → Lean.Expr → ℕ → Lean.Expr → Lean.Meta.Grind.EMatch.M Unit
-- Mathlib.CategoryTheory.Monad.Monadicity
/-- **Beck's monadicity theorem**: if `G` has a left adjoint and creates coequalizers of `G`-split
pairs, then it is monadic.
This is the converse of `createsGSplitCoequalizersOfMonadic`.
 -/
CategoryTheory.Monad.monadicOfCreatesGSplitCoequalizers : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        {G : CategoryTheory.Functor D C} →
          {F : CategoryTheory.Functor C D} →
            (F ⊣ G) → [CategoryTheory.Monad.CreatesColimitOfIsSplitPair G] → CategoryTheory.MonadicRightAdjoint G
-- Init.Data.Nat.Bitwise.Basic
Nat.hasNotBit_eq : ∀ (m n : ℕ), m.hasNotBit n = (1 &&& m >>> n ≠ 1)
-- Mathlib.MeasureTheory.Group.Arithmetic
DiscreteMeasurableSpace.toMeasurableAdd : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : Add α] [DiscreteMeasurableSpace α], MeasurableAdd α
-- Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
CategoryTheory.Triangulated.AbelianSubcategory.mono_ιK : ∀ {C : Type u_1} {A : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_5 : CategoryTheory.Pretriangulated C] [inst_6 : CategoryTheory.Category.{v_2, u_2} A]
  {ι : CategoryTheory.Functor A C},
  (∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (CategoryTheory.shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0) →
    ∀ {X₁ X₂ : A} {f₁ : X₁ ⟶ X₂} {X₃ : C} {f₂ : ι.obj X₂ ⟶ X₃}
      {f₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj (ι.obj X₁)},
      CategoryTheory.Pretriangulated.Triangle.mk (ι.map f₁) f₂ f₃ ∈
          CategoryTheory.Pretriangulated.distinguishedTriangles →
        ∀ {K Q : A} {α : (CategoryTheory.shiftFunctor C 1).obj (ι.obj K) ⟶ X₃} {β : X₃ ⟶ ι.obj Q}
          {γ : ι.obj Q ⟶ (CategoryTheory.shiftFunctor C 1).obj ((CategoryTheory.shiftFunctor C 1).obj (ι.obj K))},
          CategoryTheory.Pretriangulated.Triangle.mk α β γ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
            ∀ [inst_7 : ι.Full] [CategoryTheory.Preadditive A] [ι.Faithful],
              CategoryTheory.Mono (CategoryTheory.Triangulated.AbelianSubcategory.ιK f₃ α)
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
IsBaseChange.basis.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {V : Type u_3}
  [inst_3 : AddCommMonoid V] [inst_4 : Module R V] {W : Type u_4} [inst_5 : AddCommMonoid W] [inst_6 : Module R W]
  [inst_7 : Module S W] [inst_8 : IsScalarTower R S W] {ι : Type u_5} {ε : V →ₗ[R] W} (b : Module.Basis ι R V)
  (ibc : IsBaseChange S ε),
  IsBaseChange.basis b ibc =
    { repr := (ibc.equiv.symm.trans (LinearEquiv.baseChange R S V (ι →₀ R) b.repr)).trans ⋯.equiv }
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_eq_size_eq_zero : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β}, m.isEmpty = (m.size == 0)
-- Init.Data.String.Lemmas.FindPos
String.posGT_eq_iff : ∀ {s : String} {p : String.Pos.Raw} {h : p < s.rawEndPos} {q : s.Pos},
  s.posGT p h = q ↔ p < q.offset ∧ ∀ (q' : s.Pos), p < q'.offset → q ≤ q'
-- Init.Data.Int.Lemmas
Int.negSucc_inj : ∀ {m n : ℕ}, Int.negSucc m = Int.negSucc n ↔ m = n
-- Init.Data.UInt.Basic
instShiftRightUSize : ShiftRight USize
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.instIsIsoExtendHom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {s : CategoryTheory.Limits.Cone F} {X : C} (f : X ⟶ s.pt) [CategoryTheory.IsIso f],
  CategoryTheory.IsIso (s.extendHom f)
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.re_intCast : ∀ {d : ℤ} (n : ℤ), (↑n).re = n
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.Subcomplex.mem_unionProd_iff : ∀ {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) {n : SimplexCategoryᵒᵖ}
  (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj n),
  x ∈ (S.unionProd T).obj n ↔ x.2 ∈ T.obj n ∨ x.1 ∈ S.obj n
-- Mathlib.Order.Irreducible
/-- A sup-irreducible element is a non-bottom element which isn't the supremum of anything smaller.
 -/
SupIrred : {α : Type u_2} → [SemilatticeSup α] → α → Prop
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.excenterWeights_reindex : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {m n : ℕ} [inst_4 : NeZero m] [inst_5 : NeZero n] (s : Affine.Simplex ℝ P n)
  (e : Fin (n + 1) ≃ Fin (m + 1)) (signs : Finset (Fin (m + 1))),
  (s.reindex e).excenterWeights signs = s.excenterWeights (Finset.map e.symm.toEmbedding signs) ∘ ⇑e.symm
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.ComonadIso.mk_hom_toNatTrans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {M N : CategoryTheory.Comonad C}
  (f : M.toFunctor ≅ N.toFunctor)
  (f_ε :
    autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (f.hom.app X) (N.ε.app X) = M.ε.app X)
      CategoryTheory.ComonadIso.mk._auto_1)
  (f_δ :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (f.hom.app X) (N.δ.app X) =
          CategoryTheory.CategoryStruct.comp (M.δ.app X)
            (CategoryTheory.CategoryStruct.comp (f.hom.app (M.obj X)) (N.map (f.hom.app X))))
      CategoryTheory.ComonadIso.mk._auto_3),
  (CategoryTheory.ComonadIso.mk f f_ε f_δ).hom.toNatTrans = f.hom
-- Init.Data.Nat.Coprime
Nat.coprime_mul_iff_left : ∀ {m n k : ℕ}, (m * n).Coprime k ↔ m.Coprime k ∧ n.Coprime k
-- Init.Data.SInt.Lemmas
ISize.ofBitVec_add : ∀ (a b : BitVec System.Platform.numBits), ISize.ofBitVec (a + b) = ISize.ofBitVec a + ISize.ofBitVec b
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
/-- Deligne's archimedean Gamma factor for a real infinite place.

See "Valeurs de fonctions L et périodes d'intégrales" § 5.3. Note that this is not the same as
`Real.Gamma`; in particular it is a function `ℂ → ℂ`.  -/
Complex.Gammaℝ : ℂ → ℂ
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.option.injEq : ∀ (stx stx_1 : Lean.Syntax),
  (Lean.Elab.CompletionInfo.option stx = Lean.Elab.CompletionInfo.option stx_1) = (stx = stx_1)
-- Mathlib.Algebra.Category.Ring.Basic
_private.Mathlib.Algebra.Category.Ring.Basic.0.RingCat.Hom.mk.inj : ∀ {R S : RingCat} {hom' hom'_1 : ↑R →+* ↑S}, { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.hasSubst_iff_hasEval_of_discreteTopology : ∀ {τ : Type u_3} {S : Type u_4} [inst : CommRing S] [inst_1 : TopologicalSpace S] [DiscreteTopology S]
  {a : MvPowerSeries τ S}, PowerSeries.HasSubst a ↔ PowerSeries.HasEval a
-- Lean.DocString.Add
/-- Parses a Verso docstring from its text and elaborates it for the specified declaration. Because the
text carries no source positions, interactive features are disabled and any messages are reported at
the current reference.

`binders` should be the syntax of the parameters to the constant that is being documented, as a null
node that contains a sequence of bracketed binders, or an empty null node when none are available.
 -/
Lean.versoDocStringOfText : Lean.Name → Lean.Syntax → String → Lean.Elab.TermElabM Lean.VersoDocResult
-- Std.Tactic.BVDecide.Syntax
/-- Look at all hypotheses of the form `h : x = true`, if `x` occurs in another hypothesis substitute
it with `true`.
 -/
Lean.Elab.Tactic.BVDecide.BVDecideConfig.embeddedConstraintSubst : Lean.Elab.Tactic.BVDecide.BVDecideConfig → Bool
-- Init.Data.List.Lemmas
List.mem_flatMap_of_mem : ∀ {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : α → List β} {a : α}, a ∈ l → b ∈ f a → b ∈ List.flatMap f l